feat: expand proven fragment with assignStorage constructors

Compiler/CompilationModel/Dispatch.lean

@@ -12,10 +12,12 @@ namespace Compiler.CompilationModel
 open Compiler
 open Compiler.Yul
 
-private def pickFreshInternalRetName (usedNames : List String) (idx : Nat) : String :=
+/-- Pick a fresh internal return variable name for the given index. -/
+def pickFreshInternalRetName (usedNames : List String) (idx : Nat) : String :=
   pickFreshName s!"__ret{idx}" usedNames
 
-private def freshInternalRetNames (returns : List ParamType) (usedNames : List String) : List String :=
+/-- Generate fresh internal return variable names for an internal function. -/
+def freshInternalRetNames (returns : List ParamType) (usedNames : List String) : List String :=
   let (_, namesRev) := returns.zipIdx.foldl
     (fun (acc : List String × List String) (_retTy, idx) =>
       let (used, names) := acc
@@ -37,6 +39,118 @@ def compileInternalFunction (fields : List Field) (events : List EventDef) (erro
     (paramNames ++ retNames) spec.body
   pure (YulStmt.funcDef (internalFunctionYulName spec.name) paramNames retNames bodyStmts)
 
+theorem compileInternalFunction_ok_components
+    (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
+    (spec : FunctionSpec) (stmt : YulStmt)
+    (hcompile : compileInternalFunction fields events errors spec = Except.ok stmt) :
+    ∃ returns retNames bodyStmts,
+      validateFunctionSpec spec = Except.ok () ∧
+      functionReturns spec = Except.ok returns ∧
+      compileStmtList fields events errors .calldata retNames true
+        (spec.params.map (·.name) ++ retNames) spec.body = Except.ok bodyStmts ∧
+      stmt = YulStmt.funcDef
+        (internalFunctionYulName spec.name)
+        (spec.params.map (·.name))
+        retNames
+        bodyStmts := by
+  unfold compileInternalFunction at hcompile
+  cases hvalidate : validateFunctionSpec spec
+  · rw [hvalidate] at hcompile
+    cases hcompile
+  case ok _ =>
+    cases hreturns : functionReturns spec
+    · rw [hvalidate, hreturns] at hcompile
+      cases hcompile
+    case ok returns =>
+      rw [hvalidate, hreturns] at hcompile
+      simp only [bind, Except.bind] at hcompile
+      cases hbody :
+          compileStmtList fields events errors .calldata
+            (freshInternalRetNames returns
+              (spec.params.map (·.name) ++ collectStmtListBindNames spec.body))
+            true
+            (spec.params.map (·.name) ++
+              freshInternalRetNames returns
+                (spec.params.map (·.name) ++ collectStmtListBindNames spec.body))
+            spec.body
+      · rw [hbody] at hcompile
+        cases hcompile
+      case ok bodyStmts =>
+        rw [hbody] at hcompile
+        simp only [pure, Except.pure, Except.ok.injEq] at hcompile
+        refine
+          ⟨returns,
+            freshInternalRetNames returns
+              (spec.params.map (·.name) ++ collectStmtListBindNames spec.body),
+            bodyStmts,
+            ?_⟩
+        exact ⟨by simp, by simp,
+          by simpa using hbody, by simpa using hcompile.symm⟩
+
+theorem compileInternalFunction_some_ok_of_components
+    (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
+    (spec : FunctionSpec) (returns : List ParamType) (retNames : List String)
+    (bodyStmts : List YulStmt)
+    (hvalidate : validateFunctionSpec spec = Except.ok ())
+    (hreturns : functionReturns spec = Except.ok returns)
+    (hretNames :
+      retNames =
+        freshInternalRetNames returns
+          (spec.params.map (·.name) ++ collectStmtListBindNames spec.body))
+    (hbody :
+      compileStmtList fields events errors .calldata retNames true
+        (spec.params.map (·.name) ++ retNames) spec.body = Except.ok bodyStmts) :
+    compileInternalFunction fields events errors spec =
+      Except.ok
+        (YulStmt.funcDef
+          (internalFunctionYulName spec.name)
+          (spec.params.map (·.name))
+          retNames
+          bodyStmts) := by
+  have hbody' :
+      compileStmtList fields events errors .calldata
+        (freshInternalRetNames returns
+          (spec.params.map (·.name) ++ collectStmtListBindNames spec.body))
+        true
+        (spec.params.map (·.name) ++
+          freshInternalRetNames returns
+            (spec.params.map (·.name) ++ collectStmtListBindNames spec.body))
+        spec.body = Except.ok bodyStmts := by
+    simpa [hretNames] using hbody
+  let paramNames := spec.params.map (·.name)
+  let compiledName := internalFunctionYulName spec.name
+  have hmap :
+      (YulStmt.funcDef
+          compiledName
+          paramNames
+          (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))) <$>
+        compileStmtList fields events errors .calldata
+          (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
+          true
+          (paramNames ++ freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
+          spec.body =
+      Except.ok
+        (YulStmt.funcDef
+          compiledName
+          paramNames
+          (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
+          bodyStmts) := by
+    simpa [paramNames, compiledName] using
+      congrArg
+        (fun compiledBody =>
+          Except.map
+            (fun compiledStmts =>
+              YulStmt.funcDef
+                compiledName
+                paramNames
+                (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
+                compiledStmts)
+            compiledBody)
+        hbody'
+  unfold compileInternalFunction
+  simp [hvalidate, hreturns]
+  simpa [paramNames, compiledName, hretNames] using hmap
+
 -- Compile function spec to IR function
 def compileFunctionSpec (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
     (selector : Nat) (spec : FunctionSpec) :
@@ -88,7 +202,8 @@ def compileConstructor (fields : List Field) (events : List EventDef) (errors :
   | none => return []
   | some spec =>
     let argLoads := genConstructorArgLoads spec.params
-    let bodyChunks ← compileStmtList fields events errors .memory [] false [] spec.body
+    let bodyChunks ← compileStmtList fields events errors .memory [] false
+      (spec.params.map (·.name)) spec.body
     return argLoads ++ bodyChunks
 
 -- Main compilation function

Compiler/Proofs/IRGeneration/Contract.lean

@@ -394,7 +394,7 @@ private theorem compileValidatedCore_ok_yields_compiled_functions
       "receive" model.functions hSupported.noReceive
   unfold compileValidatedCore at hcore
   rw [hSupported.normalizedFields, hSupported.noEvents, hSupported.noErrors,
-    hSupported.noConstructor, hfallback, hreceive] at hcore
+    hfallback, hreceive] at hcore
   simp only [bind, Except.bind, pure, Except.pure] at hcore
   rcases hmap :
       ((model.functions.filter
@@ -406,21 +406,25 @@ private theorem compileValidatedCore_ok_yields_compiled_functions
         (model.functions.filter (·.isInternal)).mapM
           (compileInternalFunction model.fields [] []) with _ | internalFuncDefs
     · simp [hinternal] at hcore
-    · simp [hinternal, compileConstructor] at hcore
-      have hfunctions : ir.functions = irFns := by
-        injection hcore with hir
-        cases hir
-        rfl
-      have hcompiled :
-          List.Forall₂
-            (fun (entry : FunctionSpec × Nat) irFn =>
-              compileFunctionSpec model.fields [] [] entry.2 entry.1 = Except.ok irFn)
-            ((model.functions.filter
-                (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)).zip selectors)
-            irFns :=
-        compiled_functions_forall₂_of_mapM_ok model.fields [] [] _ _ hmap
-      simpa [SourceSemantics.selectorFunctionPairs, selectorDispatchedFunctions,
-        hSupported.noEvents, hSupported.noErrors, hfunctions] using hcompiled
+    · rcases hctor :
+          compileConstructor model.fields [] [] model.constructor with _ | deployStmts
+      · simp [hinternal, hctor] at hcore
+        cases hcore
+      · simp [hinternal, hctor] at hcore
+        have hfunctions : ir.functions = irFns := by
+          injection hcore with hir
+          cases hir
+          rfl
+        have hcompiled :
+            List.Forall₂
+              (fun (entry : FunctionSpec × Nat) irFn =>
+                compileFunctionSpec model.fields [] [] entry.2 entry.1 = Except.ok irFn)
+              ((model.functions.filter
+                  (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)).zip selectors)
+              irFns :=
+          compiled_functions_forall₂_of_mapM_ok model.fields [] [] _ _ hmap
+        simpa [SourceSemantics.selectorFunctionPairs, selectorDispatchedFunctions,
+          hSupported.noEvents, hSupported.noErrors, hfunctions] using hcompiled
 
 private theorem compileValidatedCore_ok_yields_compiled_functions_except_mapping_writes
     (model : CompilationModel)
@@ -443,7 +447,7 @@ private theorem compileValidatedCore_ok_yields_compiled_functions_except_mapping
       "receive" model.functions hSupported.noReceive
   unfold compileValidatedCore at hcore
   rw [hSupported.normalizedFields, hSupported.noEvents, hSupported.noErrors,
-    hSupported.noConstructor, hfallback, hreceive] at hcore
+    hfallback, hreceive] at hcore
   simp only [bind, Except.bind, pure, Except.pure] at hcore
   rcases hmap :
       ((model.functions.filter
@@ -455,21 +459,25 @@ private theorem compileValidatedCore_ok_yields_compiled_functions_except_mapping
         (model.functions.filter (·.isInternal)).mapM
           (compileInternalFunction model.fields [] []) with _ | internalFuncDefs
     · simp [hinternal] at hcore
-    · simp [hinternal, compileConstructor] at hcore
-      have hfunctions : ir.functions = irFns := by
-        injection hcore with hir
-        cases hir
-        rfl
-      have hcompiled :
-          List.Forall₂
-            (fun (entry : FunctionSpec × Nat) irFn =>
-              compileFunctionSpec model.fields [] [] entry.2 entry.1 = Except.ok irFn)
-            ((model.functions.filter
-                (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)).zip selectors)
-            irFns :=
-        compiled_functions_forall₂_of_mapM_ok model.fields [] [] _ _ hmap
-      simpa [SourceSemantics.selectorFunctionPairs, selectorDispatchedFunctions,
-        hSupported.noEvents, hSupported.noErrors, hfunctions] using hcompiled
+    · rcases hctor :
+          compileConstructor model.fields [] [] model.constructor with _ | deployStmts
+      · simp [hinternal, hctor] at hcore
+        cases hcore
+      · simp [hinternal, hctor] at hcore
+        have hfunctions : ir.functions = irFns := by
+          injection hcore with hir
+          cases hir
+          rfl
+        have hcompiled :
+            List.Forall₂
+              (fun (entry : FunctionSpec × Nat) irFn =>
+                compileFunctionSpec model.fields [] [] entry.2 entry.1 = Except.ok irFn)
+              ((model.functions.filter
+                  (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)).zip selectors)
+              irFns :=
+          compiled_functions_forall₂_of_mapM_ok model.fields [] [] _ _ hmap
+        simpa [SourceSemantics.selectorFunctionPairs, selectorDispatchedFunctions,
+          hSupported.noEvents, hSupported.noErrors, hfunctions] using hcompiled
 
 private theorem filterInternalFunctions_eq_nil_of_all_nonInternal :
     ∀ (fns : List FunctionSpec),
@@ -525,17 +533,21 @@ private theorem compileValidatedCore_ok_yields_internalFunctions_nil
     hSupported.contractUsesDynamicBytesEq_eq_false
   unfold compileValidatedCore at hcore
   rw [hSupported.normalizedFields, hfallback, hreceive, harray, hstorageArray,
-    hdynamicBytesEq, hnoInternalFns, hSupported.noConstructor] at hcore
+    hdynamicBytesEq, hnoInternalFns] at hcore
   simp only [bind, Except.bind, pure, Except.pure, List.mapM_nil] at hcore
   rcases hmap :
       ((model.functions.filter
           (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)).zip selectors).mapM
         (fun x => compileFunctionSpec model.fields model.events model.errors x.2 x.1) with _ | irFns
   · simp [hmap] at hcore
-  · simp [hmap, compileConstructor] at hcore
-    injection hcore with hir
-    cases hir
-    rfl
+  · rcases hctor :
+        compileConstructor model.fields model.events model.errors model.constructor with _ | deployStmts
+    · simp [hmap, hctor] at hcore
+      cases hcore
+    · simp [hmap, hctor] at hcore
+      injection hcore with hir
+      cases hir
+      rfl
 
 theorem supported_params_of_supportedSpec
     (model : CompilationModel)
@@ -750,17 +762,21 @@ theorem compile_ok_yields_internalFunctions_nil_except_mapping_writes
   · simp [hvalidate] at hcompile
     unfold compileValidatedCore at hcompile
     rw [hSupported.normalizedFields, hfallback, hreceive, harray, hstorageArray,
-      hdynamicBytesEq, hnoInternalFns, hSupported.noConstructor] at hcompile
+      hdynamicBytesEq, hnoInternalFns] at hcompile
     simp only [bind, Except.bind, pure, Except.pure, List.mapM_nil] at hcompile
     rcases hmap :
         ((model.functions.filter
             (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)).zip selectors).mapM
           (fun x => compileFunctionSpec model.fields model.events model.errors x.2 x.1) with _ | irFns
     · simp [hmap] at hcompile
-    · simp [hmap, compileConstructor] at hcompile
-      injection hcompile with hir
-      cases hir
-      rfl
+    · rcases hctor :
+          compileConstructor model.fields model.events model.errors model.constructor with _ | deployStmts
+      · simp [hmap, hctor] at hcompile
+        cases hcompile
+      · simp [hmap, hctor] at hcompile
+        injection hcompile with hir
+        cases hir
+        rfl
 
 -- NOTE: compileValidatedCore_ok_yields_supportedRuntimeHelperTableInterface and
 -- compile_ok_yields_supportedRuntimeHelperTableInterface are BLOCKED by missing