diff --git a/Compiler/CompilationModel/Compile.lean b/Compiler/CompilationModel/Compile.lean index 259563d41..efb916144 100644 --- a/Compiler/CompilationModel/Compile.lean +++ b/Compiler/CompilationModel/Compile.lean @@ -246,13 +246,25 @@ def compileStmt (fields : List Field) (events : List EventDef := []) ]] | Stmt.forEach varName count body => do - -- Bounded loop: for { let i := 0 } lt(i, count) { i := add(i, 1) } { body } (#179) + -- Bounded loop: evaluate `count` once into a cached local, drive iteration + -- with a fresh internal counter, and assign the user-visible `varName` to + -- the current counter at the top of each iteration. This matches the source + -- semantics where `count` is evaluated once and `varName` holds the last + -- iteration state after the loop rather than the post-incremented counter. let countExpr ← compileExpr fields dynamicSource count let bodyStmts ← compileStmtList fields events errors dynamicSource internalRetNames isInternal (varName :: inScopeNames) adtTypes body - let initStmts := [YulStmt.let_ varName (YulExpr.lit 0)] - let condExpr := YulExpr.call "lt" [YulExpr.ident varName, countExpr] - let postStmts := [YulStmt.assign varName (YulExpr.call "add" [YulExpr.ident varName, YulExpr.lit 1])] - pure [YulStmt.for_ initStmts condExpr postStmts bodyStmts] + let forUsedNames := varName :: (inScopeNames ++ collectExprNames count ++ collectStmtListNames body) + let idxName := pickFreshName "__forEach_idx" forUsedNames + let countName := pickFreshName "__forEach_count" (idxName :: forUsedNames) + let initStmts := [ + YulStmt.let_ idxName (YulExpr.lit 0), + YulStmt.let_ countName countExpr, + YulStmt.let_ varName (YulExpr.lit 0) + ] + let condExpr := YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName] + let postStmts := [YulStmt.assign idxName (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + let bodyWithBind := YulStmt.assign varName (YulExpr.ident idxName) :: bodyStmts + pure [YulStmt.for_ initStmts condExpr postStmts bodyWithBind] | Stmt.unsafeBlock _ body => do -- Unsafe block: transparent wrapper, compile inner body directly (#1728, Axis 6 Step 6a) diff --git a/Compiler/Proofs/EndToEnd.lean b/Compiler/Proofs/EndToEnd.lean index 9a54659b6..e2360d0a7 100644 --- a/Compiler/Proofs/EndToEnd.lean +++ b/Compiler/Proofs/EndToEnd.lean @@ -5291,6 +5291,27 @@ theorem supportedStmtList_safe_of_state_effect_closed | setStructMember2Single => simp [stmtListTouchesUnsupportedStateSurface, stmtTouchesUnsupportedStateSurface] at hState + | @forEachLiteralBounded scope varName body _ _ _ => + cases body with + | nil => + exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach + _ _ _ + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) + | cons _ _ => + simp [stmtListTouchesUnsupportedStateSurface, + stmtTouchesUnsupportedStateSurface] at hState + | forEachLiteralEmpty _ => + exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach + _ _ _ + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) | requireClause clause _ ih => simpa using Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.append @@ -5557,6 +5578,28 @@ theorem supportedStmtList_safe_of_state_except_mapping_writes_stmt_safety (Compiler.Proofs.YulGeneration.Backends.bridgedSourceExpr_of_exprCompileCore hKey2) (Compiler.Proofs.YulGeneration.Backends.bridgedSourceExpr_of_exprCompileCore hValue) hMapping2 hMembers hFindMember rfl hZero hSlots + | @forEachLiteralBounded scope varName body _ _ _ => + cases body with + | nil => + exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach + _ _ _ + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) + | cons _ _ => + simp [stmtListTouchesUnsupportedStateSurfaceExceptMappingWrites, + stmtTouchesUnsupportedStateSurfaceExceptMappingWrites, + stmtTouchesUnsupportedStateSurface] at hState + | forEachLiteralEmpty _ => + exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach + _ _ _ + (Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) + Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil) | @requireClause scope clause rest _ ih => have hTailSafety : ∀ stmt ∈ rest, StmtMappingWriteSlotSafe fields stmt := by diff --git a/Compiler/Proofs/IRGeneration/Contract.lean b/Compiler/Proofs/IRGeneration/Contract.lean index fa50c9544..0d1035112 100644 --- a/Compiler/Proofs/IRGeneration/Contract.lean +++ b/Compiler/Proofs/IRGeneration/Contract.lean @@ -132,6 +132,11 @@ private theorem legacyCompatibleExternalStmtList_append | block body rest hbody hrest ihBody ihRest => intro after hafter simpa using LegacyCompatibleExternalStmtList.block body (rest ++ after) hbody (ihRest after hafter) + | for_ init cond post body rest hinit hpost hbody hrest ihInit ihPost ihBody ihRest => + intro after hafter + simpa using + LegacyCompatibleExternalStmtList.for_ init cond post body (rest ++ after) + hinit hpost hbody (ihRest after hafter) | funcDef name params rets body rest hbody hrest ihBody ihRest => intro after hafter simpa using LegacyCompatibleExternalStmtList.funcDef name params rets body (rest ++ after) hbody (ihRest after hafter) diff --git a/Compiler/Proofs/IRGeneration/FunctionBody.lean b/Compiler/Proofs/IRGeneration/FunctionBody.lean index 2f98af31f..22c7f86b4 100644 --- a/Compiler/Proofs/IRGeneration/FunctionBody.lean +++ b/Compiler/Proofs/IRGeneration/FunctionBody.lean @@ -7275,6 +7275,23 @@ theorem runtimeStateMatchesIR_setVar_irrelevant cases state simpa [runtimeStateMatchesIR, IRState.setVar] using hmatch +theorem runtimeStateMatchesIR_setVars_irrelevant + {fields : List Field} + {runtime : SourceSemantics.RuntimeState} + {state : IRState} + {updates : List (String × Nat)} + (hmatch : runtimeStateMatchesIR fields runtime state) : + runtimeStateMatchesIR fields runtime (state.setVars updates) := by + induction updates generalizing state with + | nil => + simpa [IRState.setVars] using hmatch + | cons update updates ih => + cases update with + | mk name value => + simp [IRState.setVars] + exact ih (runtimeStateMatchesIR_setVar_irrelevant + (state := state) (name := name) (value := value) hmatch) + def stmtResultMatchesIRExecExact : SourceSemantics.StmtResult → IRExecResult → Prop | .continue runtime, .continue state => @@ -7492,6 +7509,28 @@ theorem bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant · rw [getVar_setVar_ne state tempName name value hEq] exact hexact name hname +theorem bindingsExactlyMatchIRVarsOnScope_setVars_irrelevant + {scope : List String} + {bindings : List (String × Nat)} + {state : IRState} + {updates : List (String × Nat)} + (hexact : bindingsExactlyMatchIRVarsOnScope scope bindings state) + (hfresh : ∀ update ∈ updates, update.1 ∉ scope) : + bindingsExactlyMatchIRVarsOnScope scope bindings (state.setVars updates) := by + induction updates generalizing state with + | nil => + simpa [IRState.setVars] using hexact + | cons update updates ih => + cases update with + | mk name value => + simp [IRState.setVars] + apply ih + · exact bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant + (state := state) (tempName := name) (value := value) + hexact (hfresh (name, value) (by simp)) + · intro update hmem + exact hfresh update (by simp [hmem]) + theorem bindingsExactlyMatchIRVarsOnScope_setVar_bindValue {scope : List String} {bindings : List (String × Nat)} diff --git a/Compiler/Proofs/IRGeneration/GenericInduction.lean b/Compiler/Proofs/IRGeneration/GenericInduction.lean index 4bf85312f..c9288b3ec 100644 --- a/Compiler/Proofs/IRGeneration/GenericInduction.lean +++ b/Compiler/Proofs/IRGeneration/GenericInduction.lean @@ -4,6 +4,7 @@ import Compiler.CompilationModel.ValidationCalls import Compiler.Proofs.IRGeneration.FunctionBody import Compiler.Proofs.IRGeneration.IRInterpreter import Compiler.Proofs.IRGeneration.SupportedSpec +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas set_option linter.unnecessarySeqFocus false set_option linter.unnecessarySimpa false @@ -231,6 +232,31 @@ inductive StmtListGenericCore (fields : List Field) : List String → List Stmt StmtListGenericCore fields (stmtNextScope scope stmt) rest → StmtListGenericCore fields scope (stmt :: rest) +private theorem compileStmtList_ok_of_stmtListGenericCore_early + {fields : List Field} + {scope inScopeNames : List String} + {stmts : List Stmt} + (hgeneric : StmtListGenericCore fields scope stmts) + (hincluded : FunctionBody.scopeNamesIncluded scope inScopeNames) : + ∃ bodyIR, + CompilationModel.compileStmtList + fields [] [] .calldata [] false inScopeNames [] stmts = Except.ok bodyIR := by + induction hgeneric generalizing inScopeNames with + | nil => exact ⟨[], rfl⟩ + | cons hstep _hrest ih => + rcases FunctionBody.compileStmt_ok_any_scope + (scope2 := inScopeNames) ⟨_, hstep.compileOk⟩ with ⟨headIR, hhead⟩ + rcases ih (inScopeNames := collectStmtNames _ ++ inScopeNames) + (by + intro name hmem + simp [stmtNextScope] at hmem + rcases hmem with h | h + · exact List.mem_append_left _ h + · exact List.mem_append_right _ (hincluded name h)) + with ⟨tailIR, htail⟩ + exact ⟨headIR ++ tailIR, + FunctionBody.compileStmtList_cons_ok_of_compileStmt_ok hhead htail⟩ + /-- Weaker source-side reuse witness for the future helper-rich induction path: only helper-surface-closed heads must come with the existing helper-free generic step proof. Helper-surface-positive heads can instead be discharged by a @@ -522,6 +548,10 @@ private theorem legacyCompatibleExternalStmtList_append simpa using LegacyCompatibleExternalStmtList.if_ cond body (rest ++ after) hbody (ihRest hafter) | block body rest hbody hrest ihBody ihRest => simpa using LegacyCompatibleExternalStmtList.block body (rest ++ after) hbody (ihRest hafter) + | for_ init cond post body rest hinit hpost hbody hrest ihInit ihPost ihBody ihRest => + simpa using + LegacyCompatibleExternalStmtList.for_ init cond post body (rest ++ after) + hinit hpost hbody (ihRest hafter) | funcDef name params rets body rest hbody hrest ihBody ihRest => simpa using LegacyCompatibleExternalStmtList.funcDef name params rets body (rest ++ after) hbody (ihRest hafter) @@ -1006,6 +1036,94 @@ theorem legacyCompatibleExternalStmtList_of_compileStmt_ok_on_supportedContractS hthenLegacy (.if_ _ elseIR [] helseLegacy .nil))) .nil + | forEach varName count body => + cases count with + | literal n => + cases n with + | zero => + have hbodySurface : + stmtListTouchesUnsupportedContractSurface body = false := by + cases body with + | nil => + simp [stmtListTouchesUnsupportedContractSurface] + | cons stmt rest => + simp only [stmtTouchesUnsupportedContractSurface, + stmtListTouchesUnsupportedContractSurface, + Bool.or_eq_false_iff] at hsurface + exact Bool.or_eq_false_iff.mpr hsurface + simp only [CompilationModel.compileStmt, bind, Except.bind] at hcompile + cases hbody : + CompilationModel.compileStmtList fields events errors .calldata [] false + (varName :: inScopeNames) [] body with + | error e => simp [CompilationModel.compileExpr, pure, Except.pure, hbody] at hcompile + | ok loopBodyIR => + simp [CompilationModel.compileExpr, hbody] at hcompile + cases hcompile + let forUsedNames := + varName :: (inScopeNames ++ collectExprNames (Expr.literal 0) ++ collectStmtListNames body) + let idxName := pickFreshName "__forEach_idx" forUsedNames + let countName := pickFreshName "__forEach_count" (idxName :: forUsedNames) + let initStmts := [ + YulStmt.let_ idxName (YulExpr.lit 0), + YulStmt.let_ countName (YulExpr.lit 0), + YulStmt.let_ varName (YulExpr.lit 0) + ] + let condExpr := YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName] + let postStmts := [YulStmt.assign idxName (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + let bodyWithBind := YulStmt.assign varName (YulExpr.ident idxName) :: loopBodyIR + simpa [forUsedNames, idxName, countName, initStmts, condExpr, postStmts, + bodyWithBind] using + (LegacyCompatibleExternalStmtList.for_ initStmts condExpr postStmts bodyWithBind [] + (LegacyCompatibleExternalStmtList.let_ idxName (YulExpr.lit 0) _ + (LegacyCompatibleExternalStmtList.let_ countName (YulExpr.lit 0) _ + (LegacyCompatibleExternalStmtList.let_ varName (YulExpr.lit 0) _ + LegacyCompatibleExternalStmtList.nil))) + (LegacyCompatibleExternalStmtList.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1]) _ + LegacyCompatibleExternalStmtList.nil) + (LegacyCompatibleExternalStmtList.assign varName (YulExpr.ident idxName) loopBodyIR <| + legacyCompatibleExternalStmtList_of_compileStmtList_ok_on_supportedContractSurface + hnoPacked hbodySurface hbody) + LegacyCompatibleExternalStmtList.nil) + | succ n => + cases body with + | nil => + simp only [CompilationModel.compileStmt, bind, Except.bind] at hcompile + simp [CompilationModel.compileExpr, CompilationModel.compileStmtList] at hcompile + cases hcompile + let forUsedNames := + varName :: (inScopeNames ++ + collectExprNames (Expr.literal (n + 1)) ++ collectStmtListNames []) + let idxName := pickFreshName "__forEach_idx" forUsedNames + let countName := pickFreshName "__forEach_count" (idxName :: forUsedNames) + let initStmts := [ + YulStmt.let_ idxName (YulExpr.lit 0), + YulStmt.let_ countName + (YulExpr.lit ((n + 1) % CompilationModel.uint256Modulus)), + YulStmt.let_ varName (YulExpr.lit 0) + ] + let condExpr := YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName] + let postStmts := [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + let bodyWithBind := [YulStmt.assign varName (YulExpr.ident idxName)] + simpa [forUsedNames, idxName, countName, initStmts, condExpr, + postStmts, bodyWithBind] using + (LegacyCompatibleExternalStmtList.for_ initStmts condExpr postStmts bodyWithBind [] + (LegacyCompatibleExternalStmtList.let_ idxName (YulExpr.lit 0) _ + (LegacyCompatibleExternalStmtList.let_ countName + (YulExpr.lit ((n + 1) % CompilationModel.uint256Modulus)) _ + (LegacyCompatibleExternalStmtList.let_ varName (YulExpr.lit 0) _ + LegacyCompatibleExternalStmtList.nil))) + (LegacyCompatibleExternalStmtList.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1]) _ + LegacyCompatibleExternalStmtList.nil) + (LegacyCompatibleExternalStmtList.assign varName (YulExpr.ident idxName) [] + LegacyCompatibleExternalStmtList.nil) + LegacyCompatibleExternalStmtList.nil) + | cons _ _ => + simp [stmtTouchesUnsupportedContractSurface] at hsurface + | _ => + simp [stmtTouchesUnsupportedContractSurface] at hsurface | _ => simp [stmtTouchesUnsupportedContractSurface] at hsurface termination_by sizeOf stmt @@ -3123,6 +3241,13 @@ inductive StmtListScopeDiscipline (fieldNames : List String) : List String → L StmtListScopeDiscipline fieldNames scope elseBranch → StmtListScopeDiscipline fieldNames (stmtNextScope scope (.ite cond thenBranch elseBranch)) rest → StmtListScopeDiscipline fieldNames scope (.ite cond thenBranch elseBranch :: rest) + | forEachLiteralZero {scope : List String} {varName : String} {body rest : List Stmt} : + StmtListScopeDiscipline fieldNames (varName :: scope) body → + StmtListScopeDiscipline fieldNames (stmtNextScope scope (.forEach varName (.literal 0) body)) rest → + StmtListScopeDiscipline fieldNames scope (.forEach varName (.literal 0) body :: rest) + | forEachLiteralEmpty {scope : List String} {varName : String} {n : Nat} {rest : List Stmt} : + StmtListScopeDiscipline fieldNames (stmtNextScope scope (.forEach varName (.literal n) [])) rest → + StmtListScopeDiscipline fieldNames scope (.forEach varName (.literal n) [] :: rest) /-- Syntax-side witness for the current generic statement fragment, before the scope obligations are discharged from identifier validation. -/ @@ -3179,6 +3304,13 @@ inductive StmtListScopeCore (fieldNames : List String) : List Stmt → Prop wher StmtListScopeCore fieldNames elseBranch → StmtListScopeCore fieldNames rest → StmtListScopeCore fieldNames (.ite cond thenBranch elseBranch :: rest) + | forEachLiteralZero {varName : String} {body rest : List Stmt} : + StmtListScopeCore fieldNames body → + StmtListScopeCore fieldNames rest → + StmtListScopeCore fieldNames (.forEach varName (.literal 0) body :: rest) + | forEachLiteralEmpty {varName : String} {n : Nat} {rest : List Stmt} : + StmtListScopeCore fieldNames rest → + StmtListScopeCore fieldNames (.forEach varName (.literal n) [] :: rest) private theorem exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false {expr : Expr} @@ -3465,6 +3597,39 @@ private theorem stmtListScopeCore_of_unsupportedContractSurface_eq_false fields scope thenBranch thenIR hstmtSurface.1.2 hthenCompile) (stmtListScopeCore_of_unsupportedContractSurface_eq_false fields scope elseBranch elseIR hstmtSurface.2 helseCompile) ihRest + | forEach varName count body => + cases count with + | literal n => + cases n with + | zero => + have hbodySurface : + stmtListTouchesUnsupportedContractSurface body = false := by + cases body with + | nil => + simp [stmtListTouchesUnsupportedContractSurface] + | cons stmt rest => + simp only [stmtTouchesUnsupportedContractSurface, + stmtListTouchesUnsupportedContractSurface, + Bool.or_eq_false_iff] at hstmtSurface + exact Bool.or_eq_false_iff.mpr hstmtSurface + simp only [CompilationModel.compileStmt, bind, Except.bind] at hhead + cases hbody : + CompilationModel.compileStmtList fields [] [] .calldata [] false + (varName :: scope) [] body with + | error e => simp [CompilationModel.compileExpr, pure, Except.pure, hbody] at hhead + | ok loopBodyIR => + exact .forEachLiteralZero + (stmtListScopeCore_of_unsupportedContractSurface_eq_false + fields (varName :: scope) body loopBodyIR hbodySurface hbody) + ihRest + | succ n => + cases body with + | nil => + exact .forEachLiteralEmpty ihRest + | cons _ _ => + simp [stmtTouchesUnsupportedContractSurface] at hstmtSurface + | _ => + simp [stmtTouchesUnsupportedContractSurface] at hstmtSurface | _ => simp [stmtTouchesUnsupportedContractSurface] at hstmtSurface termination_by sizeOf stmts @@ -3568,6 +3733,39 @@ theorem stmtListScopeCore_prefix_of_compileStmtList_ok_of_stmtListTouchesUnsuppo (stmtListScopeCore_of_unsupportedContractSurface_eq_false fields scope elseBranch elseIR hstmtSurface.2 helseCompile) (ih hrestSurface htail) + | forEach varName count body => + cases count with + | literal n => + cases n with + | zero => + have hbodySurface : + stmtListTouchesUnsupportedContractSurface body = false := by + cases body with + | nil => + simp [stmtListTouchesUnsupportedContractSurface] + | cons stmt rest => + simp only [stmtTouchesUnsupportedContractSurface, + stmtListTouchesUnsupportedContractSurface, + Bool.or_eq_false_iff] at hstmtSurface + exact Bool.or_eq_false_iff.mpr hstmtSurface + simp only [CompilationModel.compileStmt, bind, Except.bind] at hhead + cases hbody : + CompilationModel.compileStmtList fields [] [] .calldata [] false + (varName :: scope) [] body with + | error e => simp [CompilationModel.compileExpr, pure, Except.pure, hbody] at hhead + | ok loopBodyIR => + exact StmtListScopeCore.forEachLiteralZero + (stmtListScopeCore_of_unsupportedContractSurface_eq_false + fields (varName :: scope) body loopBodyIR hbodySurface hbody) + (ih hrestSurface htail) + | succ n => + cases body with + | nil => + exact StmtListScopeCore.forEachLiteralEmpty (ih hrestSurface htail) + | cons _ _ => + simp [stmtTouchesUnsupportedContractSurface] at hstmtSurface + | _ => + simp [stmtTouchesUnsupportedContractSurface] at hstmtSurface | setMapping _ _ _ | setMappingWord _ _ _ _ | setMappingPackedWord _ _ _ _ _ | setMapping2 _ _ _ _ | setMapping2Word _ _ _ _ _ | setMappingUint _ _ _ | setMappingChain _ _ _ @@ -3575,7 +3773,7 @@ theorem stmtListScopeCore_prefix_of_compileStmtList_ok_of_stmtListTouchesUnsuppo | storageArrayPush _ _ | storageArrayPop _ | setStorageArrayElement _ _ _ | requireError _ _ _ | revertError _ _ | returnValues _ | returnArray _ | returnBytes _ | returnStorageWords _ | calldatacopy _ _ _ - | returndataCopy _ _ _ | revertReturndata | forEach _ _ _ + | returndataCopy _ _ _ | revertReturndata | emit _ _ | internalCall _ _ | internalCallAssign _ _ _ | rawLog _ _ _ | externalCallBind _ _ _ | tryExternalCallBind _ _ _ _ | ecm _ _ | unsafeBlock _ _ | matchAdt _ _ _ => @@ -4308,7 +4506,68 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers (by intro other hmem exact mem_stmtNextScope_of_mem_scope (hlocalsInScope other hmem))) - + | forEachLiteralZero hbodyCore hrestCore ihBody ihRest => + rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with + ⟨nextLocalScope, hstmt, hrestValidate⟩ + have hstmt' := hstmt + unfold validateScopedStmtIdentifiers at hstmt' + revert hstmt' + simp only [bind, Except.bind, pure, Except.pure] + intro hstmt' + rcases hCountVal : + validateScopedExprIdentifiers context params paramScope dynamicParams localScope + constructorArgCount (Expr.literal 0) with _ | _ + · rw [hCountVal] at hstmt'; simp at hstmt' + · rw [hCountVal] at hstmt' + rcases hBodyVal : + validateScopedStmtListIdentifiers context params paramScope dynamicParams + (_ :: localScope) constructorArgCount _ with _ | _ + · rw [hBodyVal] at hstmt'; simp at hstmt' + · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' + exact StmtListScopeDiscipline.forEachLiteralZero + (ihBody hBodyVal + (by + intro other hmem + simp [hparamsInScope other hmem]) + (by + intro other hmem + simp at hmem + rcases hmem with h | h + · simp [h] + · simp [hlocalsInScope other h])) + (ihRest hrestValidate + (by + intro other hmem + exact mem_stmtNextScope_of_mem_scope (hparamsInScope other hmem)) + (by + intro other hmem + exact mem_stmtNextScope_of_mem_scope (hlocalsInScope other hmem))) + | forEachLiteralEmpty hrestCore ihRest => + rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with + ⟨nextLocalScope, hstmt, hrestValidate⟩ + have hstmt' := hstmt + unfold validateScopedStmtIdentifiers at hstmt' + revert hstmt' + simp only [bind, Except.bind, pure, Except.pure] + intro hstmt' + rcases hCountVal : + validateScopedExprIdentifiers context params paramScope dynamicParams localScope + constructorArgCount (Expr.literal _) with _ | _ + · rw [hCountVal] at hstmt'; simp at hstmt' + · rw [hCountVal] at hstmt' + rcases hBodyVal : + validateScopedStmtListIdentifiers context params paramScope dynamicParams + (_ :: localScope) constructorArgCount [] with _ | _ + · rw [hBodyVal] at hstmt'; simp at hstmt' + · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' + exact StmtListScopeDiscipline.forEachLiteralEmpty + (ihRest hrestValidate + (by + intro other hmem + exact mem_stmtNextScope_of_mem_scope (hparamsInScope other hmem)) + (by + intro other hmem + exact mem_stmtNextScope_of_mem_scope (hlocalsInScope other hmem))) theorem stmtListScopeDiscipline_of_validateFunctionIdentifierReferences_prefix {spec : FunctionSpec} {fieldNames : List String} @@ -4397,10 +4656,10 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI exact ih hrestValidate (by intro name hname - exact mem_stmtNextScope_of_mem_scope (hparamsInScope name hname)) + exact mem_stmtNextScope_of_mem_scope (stmt := _) (hparamsInScope name hname)) (by intro name hname - exact mem_stmtNextScope_of_mem_scope (hlocalsInScope name hname)) + exact mem_stmtNextScope_of_mem_scope (stmt := _) (hlocalsInScope name hname)) other hmem | require hcondCore hrest ih => rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with @@ -4576,6 +4835,60 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI intro name hname exact mem_stmtNextScope_of_mem_scope (hlocalsInScope name hname)) other hmem + | forEachLiteralZero hbodyCore hrestCore ihBody ihRest => + rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with + ⟨nextLocalScope, hstmt, hrestValidate⟩ + have hstmt' := hstmt + unfold validateScopedStmtIdentifiers at hstmt' + revert hstmt' + simp only [bind, Except.bind, pure, Except.pure] + intro hstmt' + rcases hCountVal : + validateScopedExprIdentifiers context params paramScope dynamicParams localScope + constructorArgCount (Expr.literal 0) with _ | _ + · rw [hCountVal] at hstmt'; simp at hstmt' + · rw [hCountVal] at hstmt' + rcases hBodyVal : + validateScopedStmtListIdentifiers context params paramScope dynamicParams + (_ :: localScope) constructorArgCount _ with _ | _ + · rw [hBodyVal] at hstmt'; simp at hstmt' + · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' + intro other hmem + exact ihRest hrestValidate + (by + intro name hname + exact mem_stmtNextScope_of_mem_scope (hparamsInScope name hname)) + (by + intro name hname + exact mem_stmtNextScope_of_mem_scope (hlocalsInScope name hname)) + other hmem + | forEachLiteralEmpty hrestCore ihRest => + rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with + ⟨nextLocalScope, hstmt, hrestValidate⟩ + have hstmt' := hstmt + unfold validateScopedStmtIdentifiers at hstmt' + revert hstmt' + simp only [bind, Except.bind, pure, Except.pure] + intro hstmt' + rcases hCountVal : + validateScopedExprIdentifiers context params paramScope dynamicParams localScope + constructorArgCount (Expr.literal _) with _ | _ + · rw [hCountVal] at hstmt'; simp at hstmt' + · rw [hCountVal] at hstmt' + rcases hBodyVal : + validateScopedStmtListIdentifiers context params paramScope dynamicParams + (_ :: localScope) constructorArgCount [] with _ | _ + · rw [hBodyVal] at hstmt'; simp at hstmt' + · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' + intro other hmem + exact ihRest hrestValidate + (by + intro name hname + exact mem_stmtNextScope_of_mem_scope (stmt := _) (hparamsInScope name hname)) + (by + intro name hname + exact mem_stmtNextScope_of_mem_scope (stmt := _) (hlocalsInScope name hname)) + other hmem private theorem exprBoundNamesInScope_setStorage_of_validateFunctionIdentifierReferences {spec : FunctionSpec} @@ -4854,6 +5167,39 @@ private theorem stmtListScopeDiscipline_scope_names · left; left; right; right; exact hbind · left; right; right; exact hassign · right; exact hfield + | @forEachLiteralZero scope varName body rest _ _ ihBody ihRest => + intro other hmem + simp only [List.foldl] at hmem + have htail := ihRest other hmem + simp [stmtNextScope, collectStmtNames, collectExprNames, + collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames] at htail + rcases htail with hvar | hbodyName | hscope | hbindRest | hassignRest | hfield + · simp [collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames, hvar] + · + have hmemFoldl := stmtListNames_subset_foldl_stmtNextScope + (scope := varName :: scope) hbodyName + have hbodyResult := ihBody other hmemFoldl + simp [collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames] at hbodyResult ⊢ + tauto + · simp [collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames, hscope] + · simp [collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames, hbindRest] + · simp [collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames, hassignRest] + · simp [collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames, hfield] + | @forEachLiteralEmpty scope varName n rest _ ihRest => + intro other hmem + simp only [List.foldl] at hmem + have htail := ihRest other hmem + simp [stmtNextScope, collectStmtNames, collectExprNames, + collectStmtListNames, collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames] at htail ⊢ + tauto theorem compiledStmtStep_letVar {fields : List Field} @@ -11901,7 +12247,7 @@ private theorem stmtListTouchesUnsupportedContractSurface_append | nil => simp [stmtListTouchesUnsupportedContractSurface] | cons stmt rest ih => - simp [stmtListTouchesUnsupportedContractSurface, ih, Bool.or_assoc] + cases stmt <;> simp [stmtListTouchesUnsupportedContractSurface, ih, Bool.or_assoc] private theorem stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites_append {«prefix» «suffix» : List Stmt} : @@ -11914,6 +12260,26 @@ private theorem stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites_app | cons stmt rest ih => simp [stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites, ih, Bool.or_assoc] +private theorem stmtTouchesUnsupportedContractSurfaceExceptMappingWrites_eq_false_of_contractSurface + {stmt : Stmt} + (hsurface : stmtTouchesUnsupportedContractSurface stmt = false) : + stmtTouchesUnsupportedContractSurfaceExceptMappingWrites stmt = false := by + cases stmt <;> simp [stmtTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurface] at hsurface ⊢ + all_goals assumption + +private theorem stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites_eq_false_of_contractSurface + {stmts : List Stmt} + (hsurface : stmtListTouchesUnsupportedContractSurface stmts = false) : + stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites stmts = false := by + induction stmts with + | nil => simp [stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites] + | cons stmt rest ih => + have hsplit := Bool.or_eq_false_iff.mp hsurface + simp [stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurfaceExceptMappingWrites_eq_false_of_contractSurface hsplit.1, + ih hsplit.2] + private theorem stmtListCompileCore_of_requireLiteralGuardFamilyClauses {scope : List String} (clauses : List Verity.Core.Free.RequireLiteralGuardFamilyClause) : @@ -12472,6 +12838,939 @@ private theorem stmtListGenericCore_of_supportedStmtList_tstoreSingle_of_surface (hcoreValue := hcoreValue) (hinScopeValue := hinScopeValue) +private def forEachZeroUsedNames (scope : List String) (varName : String) (body : List Stmt) : + List String := + varName :: (scope ++ collectExprNames (Expr.literal 0) ++ collectStmtListNames body) + +private def forEachZeroIdxName (scope : List String) (varName : String) (body : List Stmt) : + String := + pickFreshName "__forEach_idx" (forEachZeroUsedNames scope varName body) + +private def forEachZeroCountName (scope : List String) (varName : String) (body : List Stmt) : + String := + pickFreshName "__forEach_count" + (forEachZeroIdxName scope varName body :: forEachZeroUsedNames scope varName body) + +private def forEachZeroInitStmts (scope : List String) (varName : String) (body : List Stmt) : + List YulStmt := + [ + YulStmt.let_ (forEachZeroIdxName scope varName body) (YulExpr.lit 0), + YulStmt.let_ (forEachZeroCountName scope varName body) (YulExpr.lit 0), + YulStmt.let_ varName (YulExpr.lit 0) + ] + +private def forEachZeroCondExpr (scope : List String) (varName : String) (body : List Stmt) : + YulExpr := + YulExpr.call "lt" + [YulExpr.ident (forEachZeroIdxName scope varName body), + YulExpr.ident (forEachZeroCountName scope varName body)] + +private def forEachZeroPostStmts (scope : List String) (varName : String) (body : List Stmt) : + List YulStmt := + [YulStmt.assign (forEachZeroIdxName scope varName body) + (YulExpr.call "add" [YulExpr.ident (forEachZeroIdxName scope varName body), YulExpr.lit 1])] + +private def forEachZeroBodyWithBind + (scope : List String) (varName : String) (body : List Stmt) (bodyIR : List YulStmt) : + List YulStmt := + YulStmt.assign varName (YulExpr.ident (forEachZeroIdxName scope varName body)) :: bodyIR + +private def forEachZeroCompiledIR + (scope : List String) (varName : String) (body : List Stmt) (bodyIR : List YulStmt) : + List YulStmt := + [YulStmt.for_ (forEachZeroInitStmts scope varName body) + (forEachZeroCondExpr scope varName body) + (forEachZeroPostStmts scope varName body) + (forEachZeroBodyWithBind scope varName body bodyIR)] + +private def forEachLiteralBound (n : Nat) : Nat := + SourceSemantics.wordNormalize n + +private def forEachLiteralUsedNames (scope : List String) (varName : String) (n : Nat) : + List String := + varName :: (scope ++ collectExprNames (Expr.literal n) ++ collectStmtListNames []) + +private def forEachLiteralIdxName (scope : List String) (varName : String) (n : Nat) : + String := + pickFreshName "__forEach_idx" (forEachLiteralUsedNames scope varName n) + +private def forEachLiteralCountName (scope : List String) (varName : String) (n : Nat) : + String := + pickFreshName "__forEach_count" + (forEachLiteralIdxName scope varName n :: forEachLiteralUsedNames scope varName n) + +private def forEachLiteralInitStmts (scope : List String) (varName : String) (n : Nat) : + List YulStmt := + [ + YulStmt.let_ (forEachLiteralIdxName scope varName n) (YulExpr.lit 0), + YulStmt.let_ (forEachLiteralCountName scope varName n) + (YulExpr.lit (forEachLiteralBound n)), + YulStmt.let_ varName (YulExpr.lit 0) + ] + +private def forEachLiteralCompiledIR (scope : List String) (varName : String) (n : Nat) : + List YulStmt := + [YulStmt.for_ (forEachLiteralInitStmts scope varName n) + (YulExpr.call "lt" + [YulExpr.ident (forEachLiteralIdxName scope varName n), + YulExpr.ident (forEachLiteralCountName scope varName n)]) + [YulStmt.assign (forEachLiteralIdxName scope varName n) + (YulExpr.call "add" [YulExpr.ident (forEachLiteralIdxName scope varName n), YulExpr.lit 1])] + [YulStmt.assign varName (YulExpr.ident (forEachLiteralIdxName scope varName n))]] + +private def forEachZeroRuntimeLoop + (runtime : SourceSemantics.RuntimeState) (varName : String) : + SourceSemantics.RuntimeState := + { runtime with bindings := SourceSemantics.bindValue runtime.bindings varName 0 } + +private theorem sourceExec_forEach_literal_zero + {fields : List Field} + {runtime : SourceSemantics.RuntimeState} + {varName : String} + {body : List Stmt} : + SourceSemantics.execStmt fields runtime (Stmt.forEach varName (Expr.literal 0) body) = + .continue (forEachZeroRuntimeLoop runtime varName) := by + change + SourceSemantics.execForEachLoop varName + (fun loopState => SourceSemantics.execStmtList fields loopState body) + (forEachZeroRuntimeLoop runtime varName) 0 0 = + .continue (forEachZeroRuntimeLoop runtime varName) + rfl + +private theorem sourceExec_forEach_literal_empty + {fields : List Field} + {runtime : SourceSemantics.RuntimeState} + {varName : String} + {n : Nat} : + SourceSemantics.execStmt fields runtime (Stmt.forEach varName (Expr.literal n) []) = + .continue + (SourceSemantics.execForEachEmptyLoopFinal varName + (forEachZeroRuntimeLoop runtime varName) 0 (forEachLiteralBound n)) := by + change + SourceSemantics.execForEachLoop varName + (fun loopState => SourceSemantics.execStmtList fields loopState []) + (forEachZeroRuntimeLoop runtime varName) 0 (SourceSemantics.wordNormalize n) = + .continue + (SourceSemantics.execForEachEmptyLoopFinal varName + (forEachZeroRuntimeLoop runtime varName) 0 (forEachLiteralBound n)) + simpa [SourceSemantics.execStmtList, forEachLiteralBound] using + SourceSemantics.execForEachLoop_empty_body varName + (forEachZeroRuntimeLoop runtime varName) 0 (SourceSemantics.wordNormalize n) + +private theorem forEachZero_fresh_facts + {scope : List String} + {varName : String} + {body : List Stmt} : + let idxName := forEachZeroIdxName scope varName body + let countName := forEachZeroCountName scope varName body + idxName ≠ varName ∧ countName ≠ varName ∧ countName ≠ idxName ∧ + idxName ∉ scope ∧ countName ∉ scope := by + intro idxName countName + have hidxFreshUsed : + idxName ∉ forEachZeroUsedNames scope varName body := by + simpa [idxName, forEachZeroIdxName] using + CompilationModel.pickFreshName_not_mem_usedNames "__forEach_idx" + (forEachZeroUsedNames scope varName body) + have hcountFreshUsed : + countName ∉ idxName :: forEachZeroUsedNames scope varName body := by + simpa [countName, forEachZeroCountName, idxName] using + CompilationModel.pickFreshName_not_mem_usedNames "__forEach_count" + (idxName :: forEachZeroUsedNames scope varName body) + constructor + · intro h; exact hidxFreshUsed (by simp [forEachZeroUsedNames, h]) + constructor + · intro h; exact hcountFreshUsed (by simp [forEachZeroUsedNames, h]) + constructor + · intro h; exact hcountFreshUsed (by simp [h]) + constructor + · intro hmem; exact hidxFreshUsed (by simp [forEachZeroUsedNames, hmem]) + · intro hmem; exact hcountFreshUsed (by simp [forEachZeroUsedNames, hmem]) + +private theorem forEachLiteral_fresh_facts + {scope : List String} + {varName : String} + {n : Nat} : + let idxName := forEachLiteralIdxName scope varName n + let countName := forEachLiteralCountName scope varName n + idxName ≠ varName ∧ countName ≠ varName ∧ countName ≠ idxName ∧ + idxName ∉ scope ∧ countName ∉ scope := by + intro idxName countName + have hidxFreshUsed : + idxName ∉ forEachLiteralUsedNames scope varName n := by + simpa [idxName, forEachLiteralIdxName] using + CompilationModel.pickFreshName_not_mem_usedNames "__forEach_idx" + (forEachLiteralUsedNames scope varName n) + have hcountFreshUsed : + countName ∉ idxName :: forEachLiteralUsedNames scope varName n := by + simpa [countName, forEachLiteralCountName, idxName] using + CompilationModel.pickFreshName_not_mem_usedNames "__forEach_count" + (idxName :: forEachLiteralUsedNames scope varName n) + constructor + · intro h; exact hidxFreshUsed (by simp [forEachLiteralUsedNames, h]) + constructor + · intro h; exact hcountFreshUsed (by simp [forEachLiteralUsedNames, h]) + constructor + · intro h; exact hcountFreshUsed (by simp [h]) + constructor + · intro hmem; exact hidxFreshUsed (by simp [forEachLiteralUsedNames, hmem]) + · intro hmem; exact hcountFreshUsed (by simp [forEachLiteralUsedNames, hmem]) + +private theorem evalIRExpr_forEachZeroCond_after_init + {scope : List String} + {varName : String} + {body : List Stmt} + {state : IRState} + (hidx_ne_var : forEachZeroIdxName scope varName body ≠ varName) + (hcount_ne_var : forEachZeroCountName scope varName body ≠ varName) + (hcount_ne_idx : + forEachZeroCountName scope varName body ≠ forEachZeroIdxName scope varName body) : + evalIRExpr (((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0).setVar varName 0) + (forEachZeroCondExpr scope varName body) = some 0 := by + let idxName := forEachZeroIdxName scope varName body + let countName := forEachZeroCountName scope varName body + let stateIdx := state.setVar idxName 0 + let stateCount := stateIdx.setVar countName 0 + let stateLoop := stateCount.setVar varName 0 + have hidx_after : stateLoop.getVar idxName = some 0 := by + dsimp [stateLoop, stateCount, stateIdx] + rw [FunctionBody.getVar_setVar_ne _ varName idxName 0 hidx_ne_var] + rw [FunctionBody.getVar_setVar_ne _ countName idxName 0 hcount_ne_idx.symm] + simp + have hcount_after : stateLoop.getVar countName = some 0 := by + dsimp [stateLoop, stateCount, stateIdx] + rw [FunctionBody.getVar_setVar_ne _ varName countName 0 hcount_ne_var] + simp + change evalIRExpr stateLoop (forEachZeroCondExpr scope varName body) = some 0 + simp [forEachZeroCondExpr, idxName, countName, evalIRExpr, evalIRExprs, evalIRCall, + Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext, + hidx_after, hcount_after] + +private theorem forEachZero_initFuel_of_slack + {scope : List String} + {varName : String} + {body : List Stmt} + {bodyIR : List YulStmt} + {extraFuel : Nat} + (hslack : sizeOf (forEachZeroCompiledIR scope varName body bodyIR) - + (forEachZeroCompiledIR scope varName body bodyIR).length ≤ extraFuel) : + 4 ≤ extraFuel := by + have hmin : 4 ≤ + sizeOf (forEachZeroCompiledIR scope varName body bodyIR) - + (forEachZeroCompiledIR scope varName body bodyIR).length := by + dsimp [forEachZeroCompiledIR, forEachZeroInitStmts, forEachZeroCondExpr, + forEachZeroPostStmts, forEachZeroBodyWithBind] + simp only [List.cons.sizeOf_spec, List.nil.sizeOf_spec, YulStmt.for_.sizeOf_spec, + YulStmt.let_.sizeOf_spec, YulStmt.assign.sizeOf_spec, YulExpr.call.sizeOf_spec, + YulExpr.ident.sizeOf_spec, YulExpr.lit.sizeOf_spec] + omega + omega + +private def forEachEmptyLoopFinal + (idxName varName : String) : Nat → IRState → Nat → IRState + | _, state, 0 => state + | idx, state, Nat.succ remaining => + forEachEmptyLoopFinal idxName varName (idx + 1) + ((state.setVar varName idx).setVar idxName (idx + 1)) + remaining + +private theorem execIRStmts_forEach_empty_body_assign + {idxName varName : String} + {fuel idx : Nat} + {state : IRState} + (hidx : state.getVar idxName = some idx) + (hfuel : 2 ≤ fuel) : + execIRStmts fuel state [YulStmt.assign varName (YulExpr.ident idxName)] = + .continue (state.setVar varName idx) := by + cases fuel with + | zero => omega + | succ fuel => + cases fuel with + | zero => omega + | succ fuel => + simp [execIRStmts, execIRStmt, evalIRExpr, hidx] + +private theorem execIRStmts_forEach_empty_post_increment + {idxName varName : String} + {fuel idx : Nat} + {state : IRState} + (hidx : state.getVar idxName = some idx) + (hidx_ne_var : idxName ≠ varName) + (hidxNextLt : idx + 1 < Compiler.Constants.evmModulus) + (hfuel : 2 ≤ fuel) : + execIRStmts fuel (state.setVar varName idx) + [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] = + .continue ((state.setVar varName idx).setVar idxName (idx + 1)) := by + cases fuel with + | zero => omega + | succ fuel => + cases fuel with + | zero => omega + | succ fuel => + have hidx_read : + (state.setVar varName idx).getVar idxName = some idx := by + rw [FunctionBody.getVar_setVar_ne _ varName idxName idx hidx_ne_var] + exact hidx + have hidxNextMod : + (idx + 1) % Compiler.Constants.evmModulus = idx + 1 := + Nat.mod_eq_of_lt hidxNextLt + simp [execIRStmts, execIRStmt, evalIRExpr, evalIRExprs, evalIRCall, + Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext, + hidx_read, Compiler.Constants.evmModulus, Verity.Core.UINT256_MODULUS, + hidxNextMod] + +private theorem evalIRExpr_forEach_empty_cond_lt + {idxName countName : String} + {idx remaining : Nat} + {state : IRState} + (hidx : state.getVar idxName = some idx) + (hcount : state.getVar countName = some (idx + Nat.succ remaining)) + (hboundLt : idx + Nat.succ remaining < Compiler.Constants.evmModulus) : + evalIRExpr state + (YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) = + some 1 := by + have hidxLt : idx < Compiler.Constants.evmModulus := by omega + simp [evalIRExpr, evalIRExprs, evalIRCall, + Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext, + hidx, hcount, Compiler.Constants.evmModulus, Verity.Core.UINT256_MODULUS, + Nat.mod_eq_of_lt hidxLt, Nat.mod_eq_of_lt hboundLt] + +private theorem evalIRExpr_forEach_empty_cond_eq + {idxName countName : String} + {idx : Nat} + {state : IRState} + (hidx : state.getVar idxName = some idx) + (hcount : state.getVar countName = some idx) : + evalIRExpr state + (YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) = + some 0 := by + simp [evalIRExpr, evalIRExprs, evalIRCall, + Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext, + hidx, hcount] + +private theorem execIRStmt_forEach_empty_loop_from_idx + {idxName countName varName : String} + (remaining idx fuel : Nat) + (state : IRState) + (hidx_ne_var : idxName ≠ varName) + (hcount_ne_var : countName ≠ varName) + (hcount_ne_idx : countName ≠ idxName) + (hidx : state.getVar idxName = some idx) + (hcount : state.getVar countName = some (idx + remaining)) + (hboundLt : idx + remaining < Compiler.Constants.evmModulus) + (hfuel : remaining + 2 ≤ fuel) : + execIRStmt fuel state + (.for_ [] + (YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) + [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + [YulStmt.assign varName (YulExpr.ident idxName)]) = + .continue (forEachEmptyLoopFinal idxName varName idx state remaining) := by + induction remaining generalizing idx fuel state with + | zero => + cases fuel with + | zero => omega + | succ fuel => + exact execIRStmt_for_init_cond_zero fuel state state [] + [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + [YulStmt.assign varName (YulExpr.ident idxName)] + (YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) + (by simp [execIRStmts]) + (evalIRExpr_forEach_empty_cond_eq hidx (by simpa using hcount)) + | succ remaining ih => + cases fuel with + | zero => omega + | succ fuel => + have hfuelBody : 2 ≤ fuel := by omega + have hbody : + execIRStmts fuel state + [YulStmt.assign varName (YulExpr.ident idxName)] = + .continue (state.setVar varName idx) := + execIRStmts_forEach_empty_body_assign hidx hfuelBody + have hpost : + execIRStmts fuel (state.setVar varName idx) + [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] = + .continue ((state.setVar varName idx).setVar idxName (idx + 1)) := + execIRStmts_forEach_empty_post_increment hidx hidx_ne_var (by omega) hfuelBody + have hidxNext : + ((state.setVar varName idx).setVar idxName (idx + 1)).getVar idxName = + some (idx + 1) := + FunctionBody.getVar_setVar_eq _ idxName (idx + 1) + have hcountAfterVar : + (state.setVar varName idx).getVar countName = + some (idx + Nat.succ remaining) := by + rw [FunctionBody.getVar_setVar_ne _ varName countName idx hcount_ne_var] + exact hcount + have hcountNext : + ((state.setVar varName idx).setVar idxName (idx + 1)).getVar countName = + some ((idx + 1) + remaining) := by + rw [FunctionBody.getVar_setVar_ne _ idxName countName (idx + 1) hcount_ne_idx] + simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hcountAfterVar + have htail : + execIRStmt fuel ((state.setVar varName idx).setVar idxName (idx + 1)) + (.for_ [] + (YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) + [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + [YulStmt.assign varName (YulExpr.ident idxName)]) = + .continue (forEachEmptyLoopFinal idxName varName (idx + 1) + ((state.setVar varName idx).setVar idxName (idx + 1)) remaining) := + ih (idx := idx + 1) (fuel := fuel) + (state := (state.setVar varName idx).setVar idxName (idx + 1)) + hidxNext hcountNext (by omega) (by omega) + rw [execIRStmt_for_one_continue + (fuel := fuel) (state := state) (sInit := state) + (sBody := state.setVar varName idx) + (sPost := (state.setVar varName idx).setVar idxName (idx + 1)) + (init := []) + (post := [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])]) + (body := [YulStmt.assign varName (YulExpr.ident idxName)]) + (cond := YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) + (condValue := 1)] + · exact htail + · simp [execIRStmts] + · exact evalIRExpr_forEach_empty_cond_lt hidx hcount hboundLt + · norm_num + · exact hbody + · exact hpost + +private theorem execIRStmt_forEach_empty_loop_idx_bound + {idxName countName varName : String} + (idx bound fuel : Nat) + (state : IRState) + (hidx_ne_var : idxName ≠ varName) + (hcount_ne_var : countName ≠ varName) + (hcount_ne_idx : countName ≠ idxName) + (hidx : state.getVar idxName = some idx) + (hcount : state.getVar countName = some bound) + (hidx_le_bound : idx ≤ bound) + (hboundLt : bound < Compiler.Constants.evmModulus) + (hfuel : bound - idx + 2 ≤ fuel) : + execIRStmt fuel state + (.for_ [] + (YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) + [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + [YulStmt.assign varName (YulExpr.ident idxName)]) = + .continue (forEachEmptyLoopFinal idxName varName idx state (bound - idx)) := by + exact execIRStmt_forEach_empty_loop_from_idx + (idxName := idxName) (countName := countName) (varName := varName) + (remaining := bound - idx) (idx := idx) (fuel := fuel) (state := state) + hidx_ne_var hcount_ne_var hcount_ne_idx hidx + (by simpa [Nat.add_sub_of_le hidx_le_bound] using hcount) + (by + have hsum : idx + (bound - idx) = bound := Nat.add_sub_of_le hidx_le_bound + simpa [hsum] using hboundLt) + hfuel + +private theorem forEachLiteral_loopFuel_of_slack + {scope : List String} + {varName : String} + {n extraFuel : Nat} + (hslack : sizeOf (forEachLiteralCompiledIR scope varName n) - + (forEachLiteralCompiledIR scope varName n).length ≤ extraFuel) : + forEachLiteralBound n + 2 ≤ extraFuel := by + have hmin : forEachLiteralBound n + 2 ≤ + sizeOf (forEachLiteralCompiledIR scope varName n) - + (forEachLiteralCompiledIR scope varName n).length := by + dsimp [forEachLiteralCompiledIR, forEachLiteralInitStmts, forEachLiteralBound] + simp only [List.cons.sizeOf_spec, List.nil.sizeOf_spec, YulStmt.for_.sizeOf_spec, + YulStmt.let_.sizeOf_spec, YulStmt.assign.sizeOf_spec, YulExpr.call.sizeOf_spec, + YulExpr.ident.sizeOf_spec, YulExpr.lit.sizeOf_spec] + have hboundSize : + SourceSemantics.wordNormalize n ≤ sizeOf (SourceSemantics.wordNormalize n) := by + simp + omega + omega + +private theorem forEachLiteral_initFuel_of_slack + {scope : List String} + {varName : String} + {n extraFuel : Nat} + (hslack : sizeOf (forEachLiteralCompiledIR scope varName n) - + (forEachLiteralCompiledIR scope varName n).length ≤ extraFuel) : + 4 ≤ extraFuel := by + have hmin : 4 ≤ + sizeOf (forEachLiteralCompiledIR scope varName n) - + (forEachLiteralCompiledIR scope varName n).length := by + dsimp [forEachLiteralCompiledIR, forEachLiteralInitStmts, forEachLiteralBound] + simp only [List.cons.sizeOf_spec, List.nil.sizeOf_spec, YulStmt.for_.sizeOf_spec, + YulStmt.let_.sizeOf_spec, YulStmt.assign.sizeOf_spec, YulExpr.call.sizeOf_spec, + YulExpr.ident.sizeOf_spec, YulExpr.lit.sizeOf_spec] + omega + omega + +private theorem execIRStmts_forEach_literal_empty_compiled + {scope : List String} + {varName : String} + {n : Nat} + {state : IRState} + {extraFuel : Nat} + (hslack : sizeOf (forEachLiteralCompiledIR scope varName n) - + (forEachLiteralCompiledIR scope varName n).length ≤ extraFuel) + (hidx_ne_var : forEachLiteralIdxName scope varName n ≠ varName) + (hcount_ne_var : forEachLiteralCountName scope varName n ≠ varName) + (hcount_ne_idx : + forEachLiteralCountName scope varName n ≠ forEachLiteralIdxName scope varName n) : + execIRStmts ((forEachLiteralCompiledIR scope varName n).length + extraFuel + 1) state + (forEachLiteralCompiledIR scope varName n) = + .continue + (forEachEmptyLoopFinal (forEachLiteralIdxName scope varName n) varName 0 + (((state.setVar (forEachLiteralIdxName scope varName n) 0).setVar + (forEachLiteralCountName scope varName n) (forEachLiteralBound n)).setVar + varName 0) + (forEachLiteralBound n)) := by + let idxName := forEachLiteralIdxName scope varName n + let countName := forEachLiteralCountName scope varName n + let bound := forEachLiteralBound n + let stateIdx := state.setVar idxName 0 + let stateCount := stateIdx.setVar countName bound + let stateLoop := stateCount.setVar varName 0 + have hfuelInit : 4 ≤ extraFuel := forEachLiteral_initFuel_of_slack hslack + have hfuelLoop : bound + 2 ≤ extraFuel := by + simpa [bound] using forEachLiteral_loopFuel_of_slack + (scope := scope) (varName := varName) (n := n) hslack + have hinit : execIRStmts extraFuel state + (forEachLiteralInitStmts scope varName n) = .continue stateLoop := by + simpa [forEachLiteralInitStmts, stateIdx, stateCount, stateLoop, idxName, countName, + bound] using + execIRStmts_forEach_init_literal + (fuel := extraFuel) (state := state) (idxName := idxName) + (countName := countName) (varName := varName) (bound := bound) + (hfuel := hfuelInit) + have hidx_after_init : stateLoop.getVar idxName = some 0 := by + dsimp [stateLoop, stateCount, stateIdx] + rw [FunctionBody.getVar_setVar_ne _ varName idxName 0 hidx_ne_var] + rw [FunctionBody.getVar_setVar_ne _ countName idxName bound hcount_ne_idx.symm] + simp + have hcount_after_init : stateLoop.getVar countName = some bound := by + dsimp [stateLoop, stateCount, stateIdx] + rw [FunctionBody.getVar_setVar_ne _ varName countName 0 hcount_ne_var] + simp + have hboundLt : bound < Compiler.Constants.evmModulus := by + dsimp [bound, forEachLiteralBound] + exact FunctionBody.wordNormalize_lt_evmModulus n + have hloop : + execIRStmt (Nat.succ extraFuel) stateLoop + (.for_ [] + (YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) + [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])] + [YulStmt.assign varName (YulExpr.ident idxName)]) = + .continue (forEachEmptyLoopFinal idxName varName 0 stateLoop bound) := by + simpa [Nat.zero_add] using + execIRStmt_forEach_empty_loop_idx_bound + (idxName := idxName) (countName := countName) (varName := varName) + (idx := 0) (bound := bound) (fuel := Nat.succ extraFuel) (state := stateLoop) + hidx_ne_var hcount_ne_var hcount_ne_idx hidx_after_init + hcount_after_init (by omega) hboundLt (by omega) + dsimp [forEachLiteralCompiledIR] + have hfuelEq : extraFuel + 1 + 1 = 1 + extraFuel + 1 := by omega + rw [← hfuelEq] + exact execIRStmts_single_for_init_continue + (fuel := extraFuel) (state := state) (sInit := stateLoop) + (sFinal := forEachEmptyLoopFinal idxName varName 0 stateLoop bound) + (init := forEachLiteralInitStmts scope varName n) + (post := [YulStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])]) + (body := [YulStmt.assign varName (YulExpr.ident idxName)]) + (cond := YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]) + hinit hloop + +private theorem execIRStmts_forEach_literal_zero_compiled + {scope : List String} + {varName : String} + {body : List Stmt} + {bodyIR : List YulStmt} + {state : IRState} + {extraFuel : Nat} + (hslack : sizeOf (forEachZeroCompiledIR scope varName body bodyIR) - + (forEachZeroCompiledIR scope varName body bodyIR).length ≤ extraFuel) + (hidx_ne_var : forEachZeroIdxName scope varName body ≠ varName) + (hcount_ne_var : forEachZeroCountName scope varName body ≠ varName) + (hcount_ne_idx : + forEachZeroCountName scope varName body ≠ forEachZeroIdxName scope varName body) : + execIRStmts ((forEachZeroCompiledIR scope varName body bodyIR).length + extraFuel + 1) state + (forEachZeroCompiledIR scope varName body bodyIR) = + .continue (((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0).setVar varName 0) := by + let idxName := forEachZeroIdxName scope varName body + let countName := forEachZeroCountName scope varName body + let stateIdx := state.setVar idxName 0 + let stateCount := stateIdx.setVar countName 0 + let stateLoop := stateCount.setVar varName 0 + have hfuelInit : 4 ≤ extraFuel := forEachZero_initFuel_of_slack hslack + have hinit : execIRStmts extraFuel state + (forEachZeroInitStmts scope varName body) = .continue stateLoop := by + simpa [forEachZeroInitStmts, stateIdx, stateCount, stateLoop, idxName, countName] using + execIRStmts_forEach_init_literal_zero + (fuel := extraFuel) (state := state) (idxName := idxName) + (countName := countName) (varName := varName) (hfuel := hfuelInit) + have hcond : evalIRExpr stateLoop (forEachZeroCondExpr scope varName body) = some 0 := by + simpa [stateLoop, stateCount, stateIdx, idxName, countName] using + evalIRExpr_forEachZeroCond_after_init + (scope := scope) (varName := varName) (body := body) (state := state) + hidx_ne_var hcount_ne_var hcount_ne_idx + dsimp [forEachZeroCompiledIR] + have hfuelEq : extraFuel + 1 + 1 = 1 + extraFuel + 1 := by omega + rw [← hfuelEq] + exact execIRStmts_single_for_init_cond_zero + (fuel := extraFuel) (state := state) (sInit := stateLoop) + (init := forEachZeroInitStmts scope varName body) + (post := forEachZeroPostStmts scope varName body) + (body := forEachZeroBodyWithBind scope varName body bodyIR) + (cond := forEachZeroCondExpr scope varName body) hinit hcond + +private theorem forEachZero_nextScopeIncluded + {scope : List String} + {varName : String} + {body : List Stmt} + (hbodyNames : ∀ name, name ∈ collectStmtListNames body → name ∈ varName :: scope) : + FunctionBody.scopeNamesIncluded + (stmtNextScope scope (Stmt.forEach varName (Expr.literal 0) body)) + (varName :: scope) := by + intro name hmem + simp [stmtNextScope, collectStmtNames, collectExprNames] at hmem + rcases hmem with hvar | hbody | hscopeMem + · simp [hvar] + · exact hbodyNames name hbody + · simp [hscopeMem] + +private theorem runtimeStateMatchesIR_forEachZeroLoop + {fields : List Field} + {scope : List String} + {varName : String} + {body : List Stmt} + {runtime : SourceSemantics.RuntimeState} + {state : IRState} + (hruntime : FunctionBody.runtimeStateMatchesIR fields runtime state) : + FunctionBody.runtimeStateMatchesIR fields (forEachZeroRuntimeLoop runtime varName) + (((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0).setVar varName 0) := by + simpa [forEachZeroRuntimeLoop] using + FunctionBody.runtimeStateMatchesIR_setVar_bindValue + (fields := fields) + (runtime := runtime) + (state := (state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0) + (FunctionBody.runtimeStateMatchesIR_setVar_irrelevant + (FunctionBody.runtimeStateMatchesIR_setVar_irrelevant hruntime)) + varName 0 + +private theorem bindingsExactly_forEachZeroBase + {scope : List String} + {varName : String} + {body : List Stmt} + {runtime : SourceSemantics.RuntimeState} + {state : IRState} + (hidx_not_scope : forEachZeroIdxName scope varName body ∉ scope) + (hcount_not_scope : forEachZeroCountName scope varName body ∉ scope) + (hexact : FunctionBody.bindingsExactlyMatchIRVarsOnScope scope runtime.bindings state) : + FunctionBody.bindingsExactlyMatchIRVarsOnScope (varName :: scope) + (forEachZeroRuntimeLoop runtime varName).bindings + (((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0).setVar varName 0) := by + have hexactCount : + FunctionBody.bindingsExactlyMatchIRVarsOnScope scope runtime.bindings + ((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0) := + FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant + (FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant hexact hidx_not_scope) + hcount_not_scope + simpa [forEachZeroRuntimeLoop] using + FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_bindValue + (boundName := varName) (value := 0) hexactCount + +private theorem stmtStepMatches_forEach_literal_zero_final + {fields : List Field} + {scope : List String} + {varName : String} + {body : List Stmt} + {runtime : SourceSemantics.RuntimeState} + {state : IRState} + (hbodyNames : ∀ name, name ∈ collectStmtListNames body → name ∈ varName :: scope) + (hidx_not_scope : forEachZeroIdxName scope varName body ∉ scope) + (hcount_not_scope : forEachZeroCountName scope varName body ∉ scope) + (hexact : FunctionBody.bindingsExactlyMatchIRVarsOnScope scope runtime.bindings state) + (hscope : FunctionBody.scopeNamesPresent scope runtime.bindings) + (hbounded : FunctionBody.bindingsBounded runtime.bindings) + (hruntime : FunctionBody.runtimeStateMatchesIR fields runtime state) : + stmtStepMatchesIRExec fields + (stmtNextScope scope (Stmt.forEach varName (Expr.literal 0) body)) + (.continue (forEachZeroRuntimeLoop runtime varName)) + (.continue (((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0).setVar varName 0)) := by + let runtimeLoop := forEachZeroRuntimeLoop runtime varName + have hexactBase : + FunctionBody.bindingsExactlyMatchIRVarsOnScope (varName :: scope) + runtimeLoop.bindings + (((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0).setVar varName 0) := + bindingsExactly_forEachZeroBase hidx_not_scope hcount_not_scope hexact + have hNextScopeIncl := forEachZero_nextScopeIncluded + (scope := scope) (varName := varName) (body := body) hbodyNames + have hscopeBase : FunctionBody.scopeNamesPresent (varName :: scope) runtimeLoop.bindings := by + simpa [runtimeLoop, forEachZeroRuntimeLoop] using + FunctionBody.scopeNamesPresent_cons_bindValue + (boundName := varName) (value := 0) hscope + have hboundedLoop : FunctionBody.bindingsBounded runtimeLoop.bindings := + FunctionBody.bindingsBounded_bindValue hbounded varName 0 + (by norm_num [Compiler.Constants.evmModulus, Verity.Core.UINT256_MODULUS]) + simp [stmtStepMatchesIRExec] + exact ⟨runtimeStateMatchesIR_forEachZeroLoop + (fields := fields) (scope := scope) (varName := varName) (body := body) + (runtime := runtime) (state := state) hruntime, + FunctionBody.bindingsExactlyMatchIRVarsOnScope_of_included hexactBase hNextScopeIncl, + hboundedLoop, + FunctionBody.scopeNamesPresent_of_included hscopeBase hNextScopeIncl⟩ + +private theorem forEach_empty_final_rel + {fields : List Field} + {scope : List String} + {idxName varName : String} + (idx remaining : Nat) + {runtime : SourceSemantics.RuntimeState} + {state : IRState} + (hidx_not_next : idxName ∉ varName :: scope) + (hboundLt : idx + remaining < Compiler.Constants.evmModulus) + (hruntime : FunctionBody.runtimeStateMatchesIR fields runtime state) + (hexact : FunctionBody.bindingsExactlyMatchIRVarsOnScope (varName :: scope) + runtime.bindings state) + (hbounded : FunctionBody.bindingsBounded runtime.bindings) + (hscope : FunctionBody.scopeNamesPresent (varName :: scope) runtime.bindings) : + FunctionBody.runtimeStateMatchesIR fields + (SourceSemantics.execForEachEmptyLoopFinal varName runtime idx remaining) + (forEachEmptyLoopFinal idxName varName idx state remaining) ∧ + FunctionBody.bindingsExactlyMatchIRVarsOnScope (varName :: scope) + (SourceSemantics.execForEachEmptyLoopFinal varName runtime idx remaining).bindings + (forEachEmptyLoopFinal idxName varName idx state remaining) ∧ + FunctionBody.bindingsBounded + (SourceSemantics.execForEachEmptyLoopFinal varName runtime idx remaining).bindings ∧ + FunctionBody.scopeNamesPresent (varName :: scope) + (SourceSemantics.execForEachEmptyLoopFinal varName runtime idx remaining).bindings := by + induction remaining generalizing idx runtime state with + | zero => + simpa [SourceSemantics.execForEachEmptyLoopFinal, forEachEmptyLoopFinal] using + And.intro hruntime (And.intro hexact (And.intro hbounded hscope)) + | succ remaining ih => + have hidxLt : idx < Compiler.Constants.evmModulus := by omega + have hnorm : SourceSemantics.wordNormalize idx = idx := by + simp [SourceSemantics.wordNormalize, Compiler.Constants.evmModulus, + Verity.Core.UINT256_MODULUS, Nat.mod_eq_of_lt hidxLt] + have hmod : idx % Compiler.Constants.evmModulus = idx := + Nat.mod_eq_of_lt hidxLt + let runtimeStep : SourceSemantics.RuntimeState := + { runtime with bindings := SourceSemantics.bindValue runtime.bindings varName idx } + let stateStep : IRState := (state.setVar varName idx).setVar idxName (idx + 1) + have hruntimeStep : + FunctionBody.runtimeStateMatchesIR fields runtimeStep stateStep := by + dsimp [runtimeStep, stateStep] + exact FunctionBody.runtimeStateMatchesIR_setVar_irrelevant + (FunctionBody.runtimeStateMatchesIR_setVar_bindValue hruntime varName idx) + have hexactBind : + FunctionBody.bindingsExactlyMatchIRVarsOnScope (varName :: scope) + runtimeStep.bindings (state.setVar varName idx) := by + dsimp [runtimeStep] + exact FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_bindValue + (scope := scope) (boundName := varName) (value := idx) + (FunctionBody.bindingsExactlyMatchIRVarsOnScope_of_included hexact + (by intro name hmem; simp [hmem])) + have hexactStep : + FunctionBody.bindingsExactlyMatchIRVarsOnScope (varName :: scope) + runtimeStep.bindings stateStep := by + dsimp [stateStep] + exact FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant + (state := state.setVar varName idx) (tempName := idxName) (value := idx + 1) + hexactBind hidx_not_next + have hboundedStep : + FunctionBody.bindingsBounded runtimeStep.bindings := by + dsimp [runtimeStep] + exact FunctionBody.bindingsBounded_bindValue hbounded varName idx hidxLt + have hscopeStep : + FunctionBody.scopeNamesPresent (varName :: scope) runtimeStep.bindings := by + dsimp [runtimeStep] + exact FunctionBody.scopeNamesPresent_cons_bindValue + (FunctionBody.scopeNamesPresent_of_included hscope + (by intro name hmem; simp [hmem])) + have htail := ih (idx := idx + 1) (runtime := runtimeStep) (state := stateStep) + (by omega) hruntimeStep hexactStep hboundedStep hscopeStep + simpa [SourceSemantics.execForEachEmptyLoopFinal, forEachEmptyLoopFinal, + runtimeStep, stateStep, hnorm, hmod] using htail + +private theorem stmtStepMatches_forEach_literal_empty_final + {fields : List Field} + {scope : List String} + {varName : String} + {n : Nat} + {runtime : SourceSemantics.RuntimeState} + {state : IRState} + (hidx_ne_var : forEachLiteralIdxName scope varName n ≠ varName) + (hidx_not_scope : forEachLiteralIdxName scope varName n ∉ scope) + (hcount_not_scope : forEachLiteralCountName scope varName n ∉ scope) + (hexact : FunctionBody.bindingsExactlyMatchIRVarsOnScope scope runtime.bindings state) + (hscope : FunctionBody.scopeNamesPresent scope runtime.bindings) + (hbounded : FunctionBody.bindingsBounded runtime.bindings) + (hruntime : FunctionBody.runtimeStateMatchesIR fields runtime state) : + stmtStepMatchesIRExec fields + (stmtNextScope scope (Stmt.forEach varName (Expr.literal n) [])) + (.continue + (SourceSemantics.execForEachEmptyLoopFinal varName + (forEachZeroRuntimeLoop runtime varName) 0 (forEachLiteralBound n))) + (.continue + (forEachEmptyLoopFinal (forEachLiteralIdxName scope varName n) varName 0 + (((state.setVar (forEachLiteralIdxName scope varName n) 0).setVar + (forEachLiteralCountName scope varName n) (forEachLiteralBound n)).setVar + varName 0) + (forEachLiteralBound n))) := by + let idxName := forEachLiteralIdxName scope varName n + let countName := forEachLiteralCountName scope varName n + let runtimeLoop := forEachZeroRuntimeLoop runtime varName + let stateCount := (state.setVar idxName 0).setVar countName (forEachLiteralBound n) + let stateLoop := stateCount.setVar varName 0 + have hidx_not_next : idxName ∉ varName :: scope := by + intro hmem + simp at hmem + rcases hmem with hvar | hscopeMem + · exact hidx_ne_var hvar + · exact hidx_not_scope hscopeMem + have hexactCount : + FunctionBody.bindingsExactlyMatchIRVarsOnScope scope runtime.bindings stateCount := by + dsimp [stateCount] + exact FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant + (FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant hexact hidx_not_scope) + hcount_not_scope + have hexactLoop : + FunctionBody.bindingsExactlyMatchIRVarsOnScope (varName :: scope) + runtimeLoop.bindings stateLoop := by + simpa [runtimeLoop, forEachZeroRuntimeLoop, stateLoop] using + FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_bindValue + (boundName := varName) (value := 0) hexactCount + have hruntimeLoop : + FunctionBody.runtimeStateMatchesIR fields runtimeLoop stateLoop := by + simpa [runtimeLoop, forEachZeroRuntimeLoop, stateLoop, stateCount] using + FunctionBody.runtimeStateMatchesIR_setVar_bindValue + (FunctionBody.runtimeStateMatchesIR_setVar_irrelevant + (FunctionBody.runtimeStateMatchesIR_setVar_irrelevant hruntime)) + varName 0 + have hscopeLoop : FunctionBody.scopeNamesPresent (varName :: scope) runtimeLoop.bindings := by + simpa [runtimeLoop, forEachZeroRuntimeLoop] using + FunctionBody.scopeNamesPresent_cons_bindValue + (boundName := varName) (value := 0) hscope + have hboundedLoop : FunctionBody.bindingsBounded runtimeLoop.bindings := + FunctionBody.bindingsBounded_bindValue hbounded varName 0 + (by norm_num [Compiler.Constants.evmModulus, Verity.Core.UINT256_MODULUS]) + have hboundLt : 0 + forEachLiteralBound n < Compiler.Constants.evmModulus := by + simpa [forEachLiteralBound] using FunctionBody.wordNormalize_lt_evmModulus n + rcases forEach_empty_final_rel + (fields := fields) (scope := scope) (idxName := idxName) (varName := varName) + (idx := 0) (remaining := forEachLiteralBound n) + (runtime := runtimeLoop) (state := stateLoop) + hidx_not_next hboundLt hruntimeLoop hexactLoop hboundedLoop hscopeLoop with + ⟨hruntimeFinal, hexactFinal, hboundedFinal, hscopeFinal⟩ + have hNextScopeIncl : + FunctionBody.scopeNamesIncluded + (stmtNextScope scope (Stmt.forEach varName (Expr.literal n) [])) + (varName :: scope) := by + intro name hmem + simp [stmtNextScope, collectStmtNames, collectExprNames] at hmem + rcases hmem with hvar | hscopeMem + · simp [hvar] + · rcases hscopeMem with hbody | hscopeMem + · exact False.elim (by simpa [collectStmtListNames] using hbody) + · simp [hscopeMem] + simp [stmtStepMatchesIRExec] + exact ⟨by simpa [idxName, countName, runtimeLoop, stateLoop, stateCount] using hruntimeFinal, + FunctionBody.bindingsExactlyMatchIRVarsOnScope_of_included + (by simpa [idxName, countName, runtimeLoop, stateLoop, stateCount] using hexactFinal) + hNextScopeIncl, + by simpa [runtimeLoop] using hboundedFinal, + FunctionBody.scopeNamesPresent_of_included + (by simpa [runtimeLoop] using hscopeFinal) hNextScopeIncl⟩ + +private theorem compiledStmtStep_forEach_literal_zero + {fields : List Field} + {scope : List String} + {varName : String} + {body : List Stmt} + (hbodyNames : ∀ name, name ∈ collectStmtListNames body → name ∈ varName :: scope) + (hbodyGeneric : StmtListGenericCore fields (varName :: scope) body) : + ∃ compiledIR, + CompiledStmtStep fields scope (Stmt.forEach varName (Expr.literal 0) body) compiledIR := by + rcases compileStmtList_ok_of_stmtListGenericCore_early + (fields := fields) + (scope := varName :: scope) + (inScopeNames := varName :: scope) + hbodyGeneric + FunctionBody.scopeNamesIncluded_refl with + ⟨bodyIR, hbodyCompile⟩ + refine ⟨forEachZeroCompiledIR scope varName body bodyIR, ?_⟩ + refine + { compileOk := ?_ + preserves := ?_ } + · dsimp [forEachZeroCompiledIR, forEachZeroInitStmts, forEachZeroCondExpr, + forEachZeroPostStmts, forEachZeroBodyWithBind, forEachZeroIdxName, + forEachZeroCountName, forEachZeroUsedNames] + simp [CompilationModel.compileStmt, CompilationModel.compileExpr, hbodyCompile] + · intro runtime state extraFuel hexact hscope hbounded hruntime hslack + rcases forEachZero_fresh_facts (scope := scope) (varName := varName) (body := body) with + ⟨hidx_ne_var, hcount_ne_var, hcount_ne_idx, hidx_not_scope, hcount_not_scope⟩ + refine ⟨.continue (forEachZeroRuntimeLoop runtime varName), + .continue (((state.setVar (forEachZeroIdxName scope varName body) 0).setVar + (forEachZeroCountName scope varName body) 0).setVar varName 0), + sourceExec_forEach_literal_zero, ?_, ?_⟩ + · exact execIRStmts_forEach_literal_zero_compiled + (scope := scope) (varName := varName) (body := body) (bodyIR := bodyIR) + (state := state) (extraFuel := extraFuel) hslack + hidx_ne_var hcount_ne_var hcount_ne_idx + · exact stmtStepMatches_forEach_literal_zero_final + (fields := fields) (scope := scope) (varName := varName) (body := body) + (runtime := runtime) (state := state) hbodyNames hidx_not_scope + hcount_not_scope hexact hscope hbounded hruntime + +private theorem compiledStmtStep_forEach_literal_empty + {fields : List Field} + {scope : List String} + {varName : String} + {n : Nat} : + ∃ compiledIR, + CompiledStmtStep fields scope (Stmt.forEach varName (Expr.literal n) []) compiledIR := by + refine ⟨forEachLiteralCompiledIR scope varName n, ?_⟩ + refine + { compileOk := ?_ + preserves := ?_ } + · dsimp [forEachLiteralCompiledIR, forEachLiteralInitStmts, forEachLiteralIdxName, + forEachLiteralCountName, forEachLiteralUsedNames, forEachLiteralBound] + simp [CompilationModel.compileStmt, CompilationModel.compileStmtList, + CompilationModel.compileExpr, + CompilationModel.uint256Modulus] + rfl + · intro runtime state extraFuel hexact hscope hbounded hruntime hslack + rcases forEachLiteral_fresh_facts (scope := scope) (varName := varName) (n := n) with + ⟨hidx_ne_var, hcount_ne_var, hcount_ne_idx, hidx_not_scope, hcount_not_scope⟩ + refine ⟨.continue + (SourceSemantics.execForEachEmptyLoopFinal varName + (forEachZeroRuntimeLoop runtime varName) 0 (forEachLiteralBound n)), + .continue + (forEachEmptyLoopFinal (forEachLiteralIdxName scope varName n) varName 0 + (((state.setVar (forEachLiteralIdxName scope varName n) 0).setVar + (forEachLiteralCountName scope varName n) (forEachLiteralBound n)).setVar + varName 0) + (forEachLiteralBound n)), + sourceExec_forEach_literal_empty, ?_, ?_⟩ + · exact execIRStmts_forEach_literal_empty_compiled + (scope := scope) (varName := varName) (n := n) + (state := state) (extraFuel := extraFuel) hslack + hidx_ne_var hcount_ne_var hcount_ne_idx + · exact stmtStepMatches_forEach_literal_empty_final + (fields := fields) (scope := scope) (varName := varName) (n := n) + (runtime := runtime) (state := state) + hidx_ne_var hidx_not_scope hcount_not_scope + hexact hscope hbounded hruntime + /-- Extra Tier 2 assumptions needed to turn the singleton mapping-write constructors in `SupportedStmtList` into real compiled-step proofs. These are @@ -13977,6 +15276,39 @@ private theorem stmtListGenericCore_of_supportedStmtList_requireClause_of_surfac simp only [List.foldl, stmtNextScope_requireLiteralGuardFamilyClause clause] exact ihRest hsurface.2 +private theorem stmtListTouchesUnsupportedContractSurface_body_of_singleton_forEach_zero + {varName : String} + {body : List Stmt} + (hsurface : + stmtListTouchesUnsupportedContractSurface [Stmt.forEach varName (.literal 0) body] = false) : + stmtListTouchesUnsupportedContractSurface body = false := by + cases body with + | nil => + simp [stmtListTouchesUnsupportedContractSurface] + | cons stmt rest => + simp only [stmtListTouchesUnsupportedContractSurface, + stmtTouchesUnsupportedContractSurface, Bool.or_false, + Bool.or_eq_false_iff] at hsurface + exact Bool.or_eq_false_iff.mpr hsurface + +private theorem stmtListTouchesUnsupportedContractSurface_body_of_singleton_forEach_zero_exceptMappingWrites + {varName : String} + {body : List Stmt} + (hsurface : + stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites + [Stmt.forEach varName (.literal 0) body] = false) : + stmtListTouchesUnsupportedContractSurface body = false := by + cases body with + | nil => + simp [stmtListTouchesUnsupportedContractSurface] + | cons stmt rest => + simp only [stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurface, + stmtListTouchesUnsupportedContractSurface, Bool.or_false, + Bool.or_eq_false_iff] at hsurface + exact Bool.or_eq_false_iff.mpr hsurface + theorem stmtListGenericCore_of_supportedStmtList_of_surface {fields : List Field} {scope : List String} @@ -14051,6 +15383,18 @@ theorem stmtListGenericCore_of_supportedStmtList_of_surface exact False.elim (false_of_supportedStmtList_setMapping2WordSingle_surface hsurface) | setStructMember2Single hkey1 hscope1 hkey2 hscope2 hvalue hscopeValue hslot hmembers hmember => exact False.elim (false_of_supportedStmtList_setStructMember2Single_surface hsurface) + | forEachLiteralBounded hbodyNames _ ih => + rcases compiledStmtStep_forEach_literal_zero hbodyNames + (ih (stmtListTouchesUnsupportedContractSurface_body_of_singleton_forEach_zero + hsurface)) with + ⟨compiledIR, hstep⟩ + exact StmtListGenericCore.cons hstep StmtListGenericCore.nil + | forEachLiteralEmpty n => + rename_i scope varName + rcases compiledStmtStep_forEach_literal_empty + (fields := fields) (scope := scope) (varName := varName) (n := n) with + ⟨compiledIR, hstep⟩ + exact StmtListGenericCore.cons hstep StmtListGenericCore.nil | requireClause clause _ ih => simp [stmtListTouchesUnsupportedContractSurface] at hsurface apply stmtListGenericCore_append @@ -14179,6 +15523,19 @@ theorem stmtListGenericCore_of_supportedStmtList_of_surface_exceptMappingWrites hvalue hscopeValue hslot hmembers hmember with ⟨hm, hws, hss⟩ exact stmtListGenericCore_singleton_setStructMember2Single_of_slotSafety hkey1 hscope1 hkey2 hscope2 hvalue hscopeValue hm hmembers hmember hws hss + | forEachLiteralBounded hbodyNames _ ih => + rcases compiledStmtStep_forEach_literal_zero hbodyNames + (ih (stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites_eq_false_of_contractSurface + (stmtListTouchesUnsupportedContractSurface_body_of_singleton_forEach_zero_exceptMappingWrites + hsurface))) with + ⟨compiledIR, hstep⟩ + exact StmtListGenericCore.cons hstep StmtListGenericCore.nil + | forEachLiteralEmpty n => + rename_i scope varName + rcases compiledStmtStep_forEach_literal_empty + (fields := fields) (scope := scope) (varName := varName) (n := n) with + ⟨compiledIR, hstep⟩ + exact StmtListGenericCore.cons hstep StmtListGenericCore.nil | requireClause clause _ ih => exact stmtListGenericCore_of_supportedStmtList_requireClause_of_surface_exceptMappingWrites clause ih hsurface @@ -14496,6 +15853,20 @@ theorem stmtListGenericCore_of_supportedStmtList_of_surface_exceptMappingWrites_ subst hwordOffsetEq exact stmtListGenericCore_singleton_setStructMember2Single_of_slotSafety hkey1 hscope1 hkey2 hscope2 hvalue hscopeValue hm hmembers hmember hws hss + | forEachLiteralBounded hbodyNames hbody ih => + rcases compiledStmtStep_forEach_literal_zero hbodyNames + (stmtListGenericCore_of_supportedStmtList_of_surface + hnoConflict hbody (by + exact stmtListTouchesUnsupportedContractSurface_body_of_singleton_forEach_zero_exceptMappingWrites + hsurface)) with + ⟨compiledIR, hstep⟩ + exact StmtListGenericCore.cons hstep StmtListGenericCore.nil + | forEachLiteralEmpty n => + rename_i scope varName + rcases compiledStmtStep_forEach_literal_empty + (fields := fields) (scope := scope) (varName := varName) (n := n) with + ⟨compiledIR, hstep⟩ + exact StmtListGenericCore.cons hstep StmtListGenericCore.nil | requireClause clause hsupportedRest ih => exact stmtListGenericCore_of_supportedStmtList_requireClause_of_surface_exceptMappingWrites clause diff --git a/Compiler/Proofs/IRGeneration/IRInterpreter.lean b/Compiler/Proofs/IRGeneration/IRInterpreter.lean index 113c7ba36..339e440ea 100644 --- a/Compiler/Proofs/IRGeneration/IRInterpreter.lean +++ b/Compiler/Proofs/IRGeneration/IRInterpreter.lean @@ -366,9 +366,10 @@ private def prepareInternalCalleeState /-- Legacy IR-theorem compatibility subset for external bodies. This excludes the helper-only Yul forms whose semantics differ from the current helper-free -interpreter target (`letMany`, `leave`, `switch`, and `for`) while still -allowing nested blocks / branches so the conservative-extension theorem can -talk about today's compiled external-body shape explicitly. -/ +interpreter target (`letMany`, `leave`, and `switch`) while still allowing +nested blocks, branches, and structurally compatible loops so the +conservative-extension theorem can talk about today's compiled external-body +shape explicitly. -/ inductive LegacyCompatibleExternalStmtList : List YulStmt → Prop | nil : LegacyCompatibleExternalStmtList [] @@ -392,6 +393,12 @@ inductive LegacyCompatibleExternalStmtList : List YulStmt → Prop LegacyCompatibleExternalStmtList body → LegacyCompatibleExternalStmtList rest → LegacyCompatibleExternalStmtList (.block body :: rest) + | for_ (init : List YulStmt) (cond : YulExpr) (post body rest : List YulStmt) : + LegacyCompatibleExternalStmtList init → + LegacyCompatibleExternalStmtList post → + LegacyCompatibleExternalStmtList body → + LegacyCompatibleExternalStmtList rest → + LegacyCompatibleExternalStmtList (.for_ init cond post body :: rest) | funcDef (name : String) (params rets : List String) (body rest : List YulStmt) : LegacyCompatibleExternalStmtList body → LegacyCompatibleExternalStmtList rest → @@ -983,6 +990,329 @@ def execIRStmts (fuel : Nat) (state : IRState) : List YulStmt → IRExecResult end -- mutual +theorem execIRStmt_for_init_noncontinue + (fuel : Nat) (state : IRState) + (init post body : List YulStmt) (cond : YulExpr) (r : IRExecResult) + (hinit : execIRStmts fuel state init = r) + (hterm : ∀ s, r ≠ .continue s) : + execIRStmt (Nat.succ fuel) state (.for_ init cond post body) = r := by + simp only [execIRStmt, hinit] + +theorem execIRStmt_for_cond_none + (fuel : Nat) (state sInit : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = none) : + execIRStmt (Nat.succ fuel) state (.for_ init cond post body) = + .revert sInit := by + simp [execIRStmt, hinit, hcond] + +theorem execIRStmt_for_init_cond_zero + (fuel : Nat) (state sInit : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some 0) : + execIRStmt (Nat.succ fuel) state (.for_ init cond post body) = + .continue sInit := by + simp [execIRStmt, hinit, hcond] + +theorem execIRStmt_for_init_continue + (fuel : Nat) (state sInit : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (hinit : execIRStmts fuel state init = .continue sInit) : + execIRStmt (Nat.succ fuel) state (.for_ init cond post body) = + execIRStmt (Nat.succ fuel) sInit (.for_ [] cond post body) := by + simp [execIRStmt, hinit, execIRStmts] + +theorem execIRStmt_for_body_noncontinue + (fuel : Nat) (state sInit : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (condValue : Nat) (r : IRExecResult) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some condValue) + (hcondNZ : condValue ≠ 0) + (hbody : execIRStmts fuel sInit body = r) + (hterm : ∀ s, r ≠ .continue s) : + execIRStmt (Nat.succ fuel) state (.for_ init cond post body) = r := by + simp only [execIRStmt, hinit, hcond] + simp [hcondNZ, hbody] + +theorem execIRStmt_for_post_noncontinue + (fuel : Nat) (state sInit sBody : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (condValue : Nat) (r : IRExecResult) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some condValue) + (hcondNZ : condValue ≠ 0) + (hbody : execIRStmts fuel sInit body = .continue sBody) + (hpost : execIRStmts fuel sBody post = r) + (hterm : ∀ s, r ≠ .continue s) : + execIRStmt (Nat.succ fuel) state (.for_ init cond post body) = r := by + simp only [execIRStmt, hinit, hcond] + simp [hcondNZ, hbody, hpost] + +theorem execIRStmt_for_one_continue + (fuel : Nat) (state sInit sBody sPost : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (condValue : Nat) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some condValue) + (hcondNZ : condValue ≠ 0) + (hbody : execIRStmts fuel sInit body = .continue sBody) + (hpost : execIRStmts fuel sBody post = .continue sPost) : + execIRStmt (Nat.succ fuel) state (.for_ init cond post body) = + execIRStmt fuel sPost (.for_ [] cond post body) := by + simp only [execIRStmt, hinit, hcond] + simp [hcondNZ, hbody, hpost] + +/-- Nat-indexed recurrence for the recursive empty-init `for` form. + +After the first iteration of a compiled Yul `for`, the interpreter recurs on +`.for_ [] cond post body` with one less fuel. This theorem packages that +repeated step: callers provide the per-index condition/body/post preservation +facts for states `states k`, and the theorem threads them until the terminal +condition at `states remaining`. -/ +theorem execIRStmt_for_empty_init_recurrence + (fuel remaining : Nat) + (states : Nat → IRState) + (cond : YulExpr) + (post body : List YulStmt) + (hterminal : evalIRExpr (states remaining) cond = some 0) + (hstep : + ∀ k, k < remaining → + ∃ condValue bodyState postState, + evalIRExpr (states k) cond = some condValue ∧ + condValue ≠ 0 ∧ + execIRStmts (fuel - k - 1) (states k) body = .continue bodyState ∧ + execIRStmts (fuel - k - 1) bodyState post = .continue postState ∧ + postState = states (k + 1)) + (hfuel : remaining < fuel) : + execIRStmt fuel (states 0) (.for_ [] cond post body) = + .continue (states remaining) := by + induction remaining generalizing fuel states with + | zero => + cases fuel with + | zero => omega + | succ fuel => + exact execIRStmt_for_init_cond_zero fuel (states 0) (states 0) [] + post body cond (by simp [execIRStmts]) hterminal + | succ remaining ih => + cases fuel with + | zero => omega + | succ fuel => + rcases hstep 0 (by omega) with + ⟨condValue, bodyState, postState, hcond, hcondNZ, hbody, hpost, hpostState⟩ + have htail : + execIRStmt fuel (states 1) (.for_ [] cond post body) = + .continue (states (remaining + 1)) := by + let tailStates : Nat → IRState := fun k => states (k + 1) + have hterminalTail : + evalIRExpr (tailStates remaining) cond = some 0 := by + simpa [tailStates, Nat.add_assoc] using hterminal + have hstepTail : + ∀ k, k < remaining → + ∃ condValue bodyState postState, + evalIRExpr (tailStates k) cond = some condValue ∧ + condValue ≠ 0 ∧ + execIRStmts (fuel - k - 1) (tailStates k) body = + .continue bodyState ∧ + execIRStmts (fuel - k - 1) bodyState post = + .continue postState ∧ + postState = tailStates (k + 1) := by + intro k hk + rcases hstep (k + 1) (by omega) with + ⟨cv, bs, ps, hc, hcv, hb, hp, hps⟩ + refine ⟨cv, bs, ps, ?_, hcv, ?_, ?_, ?_⟩ + · simpa [tailStates, Nat.add_assoc] using hc + · have hfuelEq : Nat.succ fuel - (k + 1) - 1 = fuel - k - 1 := by + omega + simpa [tailStates, hfuelEq, Nat.add_assoc] using hb + · have hfuelEq : Nat.succ fuel - (k + 1) - 1 = fuel - k - 1 := by + omega + simpa [hfuelEq] using hp + · simpa [tailStates, Nat.add_assoc] using hps + have hfuelTail : remaining < fuel := by omega + simpa [tailStates] using + ih (fuel := fuel) (states := tailStates) + hterminalTail hstepTail hfuelTail + have hbody' : execIRStmts fuel (states 0) body = .continue bodyState := by + simpa using hbody + have hpost' : execIRStmts fuel bodyState post = .continue postState := by + simpa using hpost + rw [execIRStmt_for_one_continue + (fuel := fuel) (state := states 0) (sInit := states 0) + (sBody := bodyState) (sPost := postState) + (init := []) (post := post) (body := body) (cond := cond) + (condValue := condValue) + (by simp [execIRStmts]) hcond hcondNZ hbody' hpost'] + simpa [hpostState] using htail + +/-- Singleton-list form of `execIRStmt_for_init_cond_zero`. + +This is the shape needed when a compiled source statement is represented by a +single Yul `for` statement inside `execIRStmts`. -/ +theorem execIRStmts_single_for_init_cond_zero + (fuel : Nat) (state sInit : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some 0) : + execIRStmts (Nat.succ (Nat.succ fuel)) state [.for_ init cond post body] = + .continue sInit := by + simp only [execIRStmts] + rw [execIRStmt_for_init_cond_zero fuel state sInit init post body cond hinit hcond] + +theorem execIRStmts_single_for_init_continue + (fuel : Nat) (state sInit sFinal : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (hinit : execIRStmts fuel state init = .continue sInit) + (hloop : execIRStmt (Nat.succ fuel) sInit (.for_ [] cond post body) = .continue sFinal) : + execIRStmts (Nat.succ (Nat.succ fuel)) state [.for_ init cond post body] = + .continue sFinal := by + simp only [execIRStmts] + rw [execIRStmt_for_init_continue fuel state sInit init post body cond hinit] + rw [hloop] + +/-- Head/tail form of `execIRStmt_for_init_cond_zero`. + +After the `for` condition evaluates to zero, statement-list execution continues +with the tail from the state produced by the init block. -/ +theorem execIRStmts_cons_for_init_cond_zero + (fuel : Nat) (state sInit : IRState) + (init post body tail : List YulStmt) (cond : YulExpr) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some 0) : + execIRStmts (Nat.succ (Nat.succ fuel)) state + (.for_ init cond post body :: tail) = + execIRStmts (Nat.succ fuel) sInit tail := by + simp only [execIRStmts] + rw [execIRStmt_for_init_cond_zero fuel state sInit init post body cond hinit hcond] + +/-- Singleton-list form of one successful `for` iteration. + +The init block, first condition check, body, and post block are discharged, and +the remaining execution is exactly the recursive empty-init loop. -/ +theorem execIRStmts_single_for_one_continue + (fuel : Nat) (state sInit sBody sPost : IRState) + (init post body : List YulStmt) (cond : YulExpr) + (condValue : Nat) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some condValue) + (hcondNZ : condValue ≠ 0) + (hbody : execIRStmts fuel sInit body = .continue sBody) + (hpost : execIRStmts fuel sBody post = .continue sPost) : + execIRStmts (Nat.succ (Nat.succ fuel)) state [.for_ init cond post body] = + match execIRStmt fuel sPost (.for_ [] cond post body) with + | .continue sLoop => .continue sLoop + | .return value sLoop => .return value sLoop + | .stop sLoop => .stop sLoop + | .revert sLoop => .revert sLoop := by + simp only [execIRStmts] + rw [execIRStmt_for_one_continue fuel state sInit sBody sPost init post body cond + condValue hinit hcond hcondNZ hbody hpost] + +/-- Head/tail form of one successful `for` iteration. + +This threads the tail through the recursive empty-init loop produced after the +first successful body/post execution. -/ +theorem execIRStmts_cons_for_one_continue + (fuel : Nat) (state sInit sBody sPost : IRState) + (init post body tail : List YulStmt) (cond : YulExpr) + (condValue : Nat) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some condValue) + (hcondNZ : condValue ≠ 0) + (hbody : execIRStmts fuel sInit body = .continue sBody) + (hpost : execIRStmts fuel sBody post = .continue sPost) : + execIRStmts (Nat.succ (Nat.succ fuel)) state + (.for_ init cond post body :: tail) = + match execIRStmt fuel sPost (.for_ [] cond post body) with + | .continue sLoop => execIRStmts (Nat.succ fuel) sLoop tail + | .return value sLoop => .return value sLoop + | .stop sLoop => .stop sLoop + | .revert sLoop => .revert sLoop := by + simp only [execIRStmts] + rw [execIRStmt_for_one_continue fuel state sInit sBody sPost init post body cond + condValue hinit hcond hcondNZ hbody hpost] + +/-- Convenient continuation-only corollary of `execIRStmts_cons_for_one_continue`. + +Use this when the recursive empty-init loop is known to finish with `.continue`; +the list tail then resumes from that state. -/ +theorem execIRStmts_cons_for_one_continue_of_loop_continue + (fuel : Nat) (state sInit sBody sPost sLoop : IRState) + (init post body tail : List YulStmt) (cond : YulExpr) + (condValue : Nat) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : evalIRExpr sInit cond = some condValue) + (hcondNZ : condValue ≠ 0) + (hbody : execIRStmts fuel sInit body = .continue sBody) + (hpost : execIRStmts fuel sBody post = .continue sPost) + (hloop : execIRStmt fuel sPost (.for_ [] cond post body) = .continue sLoop) : + execIRStmts (Nat.succ (Nat.succ fuel)) state + (.for_ init cond post body :: tail) = + execIRStmts (Nat.succ fuel) sLoop tail := by + rw [execIRStmts_cons_for_one_continue fuel state sInit sBody sPost init post body + tail cond condValue hinit hcond hcondNZ hbody hpost, hloop] + +/-- forEach-shaped zero-condition lemma. + +The statement syntax is specialized to the compiler's current forEach loop +layout: init statements, `lt(idx, count)`, `idx := add(idx, 1)`, and a leading +assignment of the element variable before the compiled body. The semantic facts +remain explicit hypotheses so callers can provide them from their local loop +invariants. -/ +theorem execIRStmt_forEach_shape_init_cond_zero + (fuel : Nat) (state sInit : IRState) + (init bodyIR : List YulStmt) + (idxName countName varName : String) + (hinit : execIRStmts fuel state init = .continue sInit) + (hcond : + evalIRExpr sInit + (.call "lt" [.ident idxName, .ident countName]) = some 0) : + execIRStmt (Nat.succ fuel) state + (.for_ + init + (.call "lt" [.ident idxName, .ident countName]) + [.assign idxName (.call "add" [.ident idxName, .lit 1])] + (.assign varName (.ident idxName) :: bodyIR)) = + .continue sInit := by + exact execIRStmt_for_init_cond_zero fuel state sInit init + [.assign idxName (.call "add" [.ident idxName, .lit 1])] + (.assign varName (.ident idxName) :: bodyIR) + (.call "lt" [.ident idxName, .ident countName]) + hinit hcond + +/-- The three initializer statements emitted for a zero-literal `forEach` +execute to the expected cached-counter state once enough fuel is available. -/ +theorem execIRStmts_forEach_init_literal_zero + (fuel : Nat) (state : IRState) + (idxName countName varName : String) + (hfuel : 4 ≤ fuel) : + execIRStmts fuel state + [ YulStmt.let_ idxName (YulExpr.lit 0) + , YulStmt.let_ countName (YulExpr.lit 0) + , YulStmt.let_ varName (YulExpr.lit 0) ] = + .continue (((state.setVar idxName 0).setVar countName 0).setVar varName 0) := by + rcases Nat.exists_eq_add_of_le hfuel with ⟨extra, rfl⟩ + rw [Nat.add_comm] + simp [execIRStmts, execIRStmt, evalIRExpr] + +/-- The three initializer statements emitted for a literal-bound `forEach` +execute to the expected cached-counter state once enough fuel is available. -/ +theorem execIRStmts_forEach_init_literal + (fuel : Nat) (state : IRState) + (idxName countName varName : String) + (bound : Nat) + (hfuel : 4 ≤ fuel) : + execIRStmts fuel state + [ YulStmt.let_ idxName (YulExpr.lit 0) + , YulStmt.let_ countName (YulExpr.lit bound) + , YulStmt.let_ varName (YulExpr.lit 0) ] = + .continue (((state.setVar idxName 0).setVar countName bound).setVar varName 0) := by + rcases Nat.exists_eq_add_of_le hfuel with ⟨extra, rfl⟩ + rw [Nat.add_comm] + simp [execIRStmts, execIRStmt, evalIRExpr] + @[simp] theorem execIRStmt_stop_succ (fuel : Nat) (state : IRState) : execIRStmt (Nat.succ fuel) state (YulStmt.expr (YulExpr.call "stop" [])) = .stop state := by @@ -2968,6 +3298,10 @@ theorem YulStmtListCallsDisjointFromInternalTable_of_internalFunctions_nil (yulExprCallsDisjointFromInternalTable_of_internalFunctions_nil contract hinternal cond) ihBody ihRest | block body rest hbody _ ihBody ihRest => exact .block body rest ihBody ihRest + | for_ init cond post body rest hinit hpost hbody _ ihInit ihPost ihBody ihRest => + exact .for_ init cond post body rest ihInit + (yulExprCallsDisjointFromInternalTable_of_internalFunctions_nil contract hinternal cond) + ihPost ihBody ihRest | funcDef name params rets body rest hbody _ ihBody ihRest => exact .funcDef name params rets body rest ihBody ihRest @@ -3500,6 +3834,81 @@ theorem execIRStmtsWithInternals_eq_execIRStmts_of_exprCompatibility rw [execIRStmtsWithInternals, execIRStmts, hhead] cases hstep : execIRStmt fuel state (.block body) <;> simp only [ihRest] + | for_ init cond post body rest hinit hpost hbody hrest ihInit ihPost ihBody ihRest => + cases fuel with + | zero => + simp only [execIRStmtsWithInternals, execIRStmts] + | succ fuel => + have hhead : + execIRStmtWithInternals contract fuel state (.for_ init cond post body) = + match execIRStmt fuel state (.for_ init cond post body) with + | .continue next => .continue next + | .return value next => .return value next + | .stop next => .stop next + | .revert next => .revert next := by + suffices hgen : ∀ (f : Nat) (s : IRState) (initStmts : List YulStmt), + (∀ f' s', execIRStmtsWithInternals contract f' s' initStmts = + match execIRStmts f' s' initStmts with + | .continue n => .continue n | .return v n => .return v n + | .stop n => .stop n | .revert n => .revert n) → + execIRStmtWithInternals contract f s (.for_ initStmts cond post body) = + match execIRStmt f s (.for_ initStmts cond post body) with + | .continue next => .continue next + | .return value next => .return value next + | .stop next => .stop next + | .revert next => .revert next by + exact hgen fuel state init (ihInit · ·) + intro f + induction f with + | zero => + intro s initStmts _ + simp only [execIRStmtWithInternals, execIRStmt] + | succ f ihFuel => + intro s initStmts hInitEq + simp only [execIRStmtWithInternals, execIRStmt] + rw [hInitEq] + cases hInitStep : execIRStmts f s initStmts with + | «continue» s' => + simp only [] + rw [evalIRExprWithInternals_eq_evalIRExpr_of_no_internal + contract hinternal f s' cond] + cases hCondVal : evalIRExpr s' cond with + | none => + simp + | some condValue => + by_cases hnonzero : condValue ≠ 0 + · simp only [if_pos hnonzero] + rw [ihBody f s'] + cases hBodyStep : execIRStmts f s' body with + | «continue» s'' => + simp only [] + rw [ihPost f s''] + cases hPostStep : execIRStmts f s'' post with + | «continue» s''' => + simp only [] + have hNilEq : ∀ f' s', + execIRStmtsWithInternals contract f' s' [] = + match execIRStmts f' s' [] with + | .continue n => .continue n + | .return v n => .return v n + | .stop n => .stop n + | .revert n => .revert n := by + intro f' s' + simp only [execIRStmtsWithInternals, execIRStmts] + exact ihFuel s''' [] hNilEq + | «return» v s''' => simp + | stop s''' => simp + | revert s''' => simp + | «return» v s'' => simp + | stop s'' => simp + | revert s'' => simp + · simp only [if_neg hnonzero] + | «return» v s' => simp + | stop s' => simp + | revert s' => simp + rw [execIRStmtsWithInternals, execIRStmts, hhead] + cases hstep : execIRStmt fuel state (.for_ init cond post body) <;> + simp only [ihRest] | funcDef name params rets body rest hbody hrest ihBody ihRest => cases fuel with | zero => @@ -3683,6 +4092,18 @@ theorem execIRStmtsWithInternals_eq_execIRStmts_of_stmtCompatibility rw [execIRStmtsWithInternals, execIRStmts, hhead] cases hstep : execIRStmt fuel state (.block body) <;> simp only [ihRest] + | for_ init cond post body rest hinit hpost hbody hrest ihInit ihPost ihBody ihRest => + cases fuel with + | zero => + simp only [execIRStmtsWithInternals, execIRStmts] + | succ fuel => + have hhead := + hstmt hinternal fuel state (.for_ init cond post body) + (LegacyCompatibleExternalStmtList.for_ init cond post body [] + hinit hpost hbody LegacyCompatibleExternalStmtList.nil) + rw [execIRStmtsWithInternals, execIRStmts, hhead] + cases hstep : execIRStmt fuel state (.for_ init cond post body) <;> + simp only [ihRest] | funcDef name params rets body rest hbody hrest ihBody ihRest => cases fuel with | zero => diff --git a/Compiler/Proofs/IRGeneration/SourceSemantics.lean b/Compiler/Proofs/IRGeneration/SourceSemantics.lean index a9ea81128..3504f5f98 100644 --- a/Compiler/Proofs/IRGeneration/SourceSemantics.lean +++ b/Compiler/Proofs/IRGeneration/SourceSemantics.lean @@ -551,6 +551,179 @@ inductive StmtResult where | return (value : Nat) (state : RuntimeState) | revert +def execForEachLoop + (varName : String) + (runBody : RuntimeState → StmtResult) : + RuntimeState → Nat → Nat → StmtResult + | state, _, 0 => .continue state + | state, index, remaining + 1 => + let loopState := + { state with bindings := bindValue state.bindings varName (wordNormalize index) } + match runBody loopState with + | .continue next => execForEachLoop varName runBody next (index + 1) remaining + | .stop next => .stop next + | .return value next => .return value next + | .revert => .revert + +@[simp] theorem execForEachLoop_zero + (varName : String) + (runBody : RuntimeState → StmtResult) + (state : RuntimeState) + (index : Nat) : + execForEachLoop varName runBody state index 0 = .continue state := rfl + +theorem execForEachLoop_succ + (varName : String) + (runBody : RuntimeState → StmtResult) + (state : RuntimeState) + (index remaining : Nat) : + execForEachLoop varName runBody state index (remaining + 1) = + let loopState := + { state with bindings := bindValue state.bindings varName (wordNormalize index) } + match runBody loopState with + | .continue next => execForEachLoop varName runBody next (index + 1) remaining + | .stop next => .stop next + | .return value next => .return value next + | .revert => .revert := rfl + +@[simp] theorem lookupBinding?_bindValue_same + (bindings : List (String × Nat)) + (name : String) + (value : Nat) : + lookupBinding? (bindValue bindings name value) name = some value := by + simp [lookupBinding?, bindValue] + +@[simp] theorem lookupValue_bindValue_same + (bindings : List (String × Nat)) + (name : String) + (value : Nat) : + lookupValue (bindValue bindings name value) name = value := by + simp [lookupValue, bindValue] + +@[simp] theorem execForEachLoop_boundState_lookupBinding? + (varName : String) + (state : RuntimeState) + (index : Nat) : + lookupBinding? + (bindValue state.bindings varName (wordNormalize index)) + varName = + some (wordNormalize index) := by + simp + +@[simp] theorem execForEachLoop_boundState_lookupValue + (varName : String) + (state : RuntimeState) + (index : Nat) : + lookupValue + (bindValue state.bindings varName (wordNormalize index)) + varName = + wordNormalize index := by + simp + +theorem execForEachLoop_zero_continue_state + {varName : String} + {runBody : RuntimeState → StmtResult} + {state final : RuntimeState} + {index : Nat} + (hloop : execForEachLoop varName runBody state index 0 = .continue final) : + final = state := by + simpa [execForEachLoop] using hloop.symm + +theorem execForEachLoop_succ_continue_iff + {varName : String} + {runBody : RuntimeState → StmtResult} + {state final : RuntimeState} + {index remaining : Nat} : + execForEachLoop varName runBody state index (remaining + 1) = .continue final ↔ + ∃ next, + runBody + { state with + bindings := bindValue state.bindings varName (wordNormalize index) } = + .continue next ∧ + execForEachLoop varName runBody next (index + 1) remaining = + .continue final := by + simp only [execForEachLoop] + cases hbody : + runBody + { state with + bindings := bindValue state.bindings varName (wordNormalize index) } <;> + simp [hbody] + +theorem execForEachLoop_succ_continue + {varName : String} + {runBody : RuntimeState → StmtResult} + {state next final : RuntimeState} + {index remaining : Nat} + (hbody : + runBody + { state with + bindings := bindValue state.bindings varName (wordNormalize index) } = + .continue next) + (hloop : + execForEachLoop varName runBody next (index + 1) remaining = + .continue final) : + execForEachLoop varName runBody state index (remaining + 1) = + .continue final := by + rw [execForEachLoop_succ] + simpa only [hbody] using hloop + +theorem execForEachLoop_congr + {varName : String} + {runBodyA runBodyB : RuntimeState → StmtResult} + (hbody : ∀ state, runBodyA state = runBodyB state) : + ∀ (state : RuntimeState) (index remaining : Nat), + execForEachLoop varName runBodyA state index remaining = + execForEachLoop varName runBodyB state index remaining + | state, index, 0 => by + simp [execForEachLoop] + | state, index, remaining + 1 => by + simp only [execForEachLoop] + rw [hbody] + cases hrun : runBodyB + { state with bindings := bindValue state.bindings varName (wordNormalize index) } <;> + simp [hrun, execForEachLoop_congr hbody] + +def execForEachEmptyLoopFinal + (varName : String) : RuntimeState → Nat → Nat → RuntimeState + | state, _, 0 => state + | state, index, remaining + 1 => + execForEachEmptyLoopFinal varName + { state with bindings := bindValue state.bindings varName (wordNormalize index) } + (index + 1) remaining + +theorem execForEachLoop_empty_body + (varName : String) + (state : RuntimeState) + (index remaining : Nat) : + execForEachLoop varName (fun loopState => .continue loopState) + state index remaining = + .continue (execForEachEmptyLoopFinal varName state index remaining) := by + induction remaining generalizing state index with + | zero => + rfl + | succ remaining ih => + simp [execForEachLoop, execForEachEmptyLoopFinal, ih] + +theorem execForEachLoop_empty_body_zero_bound + (varName : String) + (state : RuntimeState) + (index : Nat) : + execForEachLoop varName (fun loopState => .continue loopState) + state index 0 = + .continue state := rfl + +theorem execForEachLoop_empty_body_positive_bound + (varName : String) + (state : RuntimeState) + (index remaining : Nat) : + execForEachLoop varName (fun loopState => .continue loopState) + state index (remaining + 1) = + .continue + (execForEachEmptyLoopFinal varName + { state with bindings := bindValue state.bindings varName (wordNormalize index) } + (index + 1) remaining) := by + simp [execForEachLoop_empty_body, execForEachEmptyLoopFinal] + private def storageArraySetAt : List Verity.Core.Uint256 → Nat → Verity.Core.Uint256 → Option (List Verity.Core.Uint256) | [], _, _ => none | _ :: rest, 0, value => some (value :: rest) @@ -1873,6 +2046,15 @@ mutual events := state.world.events ++ [event] } } | _, _ => .revert | none => .revert + | state, .forEach varName count body => + match evalExpr fields state count with + | some bound => + let initialLoopState := + { state with bindings := bindValue state.bindings varName (wordNormalize 0) } + execForEachLoop varName + (fun loopState => execStmtListWithEvents fields events loopState body) + initialLoopState 0 bound + | none => .revert | _, _ => .revert def execStmtListWithEvents (fields : List Field) (events : List EventDef) : @@ -2108,6 +2290,15 @@ mutual events := state.world.events ++ [event] } } | _, _ => .revert | none => .revert + | state, .forEach varName count body => + match evalExpr fields state count with + | some bound => + let initialLoopState := + { state with bindings := bindValue state.bindings varName (wordNormalize 0) } + execForEachLoop varName + (fun loopState => execStmtList fields loopState body) + initialLoopState 0 bound + | none => .revert | _, _ => .revert def execStmtList (fields : List Field) : RuntimeState → List Stmt → StmtResult @@ -3115,6 +3306,15 @@ mutual events := state.world.events ++ [event] } } | _, _ => .revert | none => .revert + | .forEach varName count body => + match evalExprWithHelpers spec fields fuel state count with + | some bound => + let initialLoopState := + { state with bindings := bindValue state.bindings varName (wordNormalize 0) } + execForEachLoop varName + (fun loopState => execStmtListWithHelpers spec fields fuel loopState body) + initialLoopState 0 bound + | none => .revert | _ => .revert termination_by stmt => (fuel, sizeOf stmt) decreasing_by all_goals (simp_wf; omega) @@ -4167,6 +4367,13 @@ mutual simp [Stmt.ite.sizeOf_spec] omega + private theorem stmt_sizeOf_lt_forEach_body + (varName : String) (count : Expr) (body : List Stmt) : + sizeOf body + 1 < sizeOf (Stmt.forEach varName count body) := by + have hcount : 0 < sizeOf count := expr_sizeOf_pos count + simp [Stmt.forEach.sizeOf_spec] + omega + private theorem stmt_sizeOf_lt_cons (stmt : Stmt) (rest : List Stmt) : sizeOf stmt + 1 < sizeOf (stmt :: rest) := by cases rest with @@ -4348,7 +4555,32 @@ private theorem execStmtWithHelpers_eq_execStmt_of_helperSurfaceClosed_aux | .ecm _ _ => simp [execStmtWithHelpers, execStmtWithEvents] | .forEach _ _ _ => simp only [stmtTouchesUnsupportedHelperSurface, Bool.or_eq_false_iff] at hsurface - simp [execStmtWithHelpers, execStmtWithEvents] + rename_i varName count body + have hcount := + evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed + spec fields fuel state count hsurface.1 + simp only [execStmtWithHelpers, execStmtWithEvents, hcount] + cases evalExpr fields state count with + | none => rfl + | some bound => + let initialLoopState := + { state with bindings := bindValue state.bindings varName (wordNormalize 0) } + exact execForEachLoop_congr + (varName := varName) + (runBodyA := fun loopState => + execStmtListWithHelpers spec fields fuel loopState body) + (runBodyB := fun loopState => + execStmtListWithEvents fields spec.events loopState body) + (fun loopState => + execStmtListWithHelpers_eq_execStmtList_of_helperSurfaceClosed_inner + spec fields fuel loopState body hsurface.2 + (fun st s hs hsf => + have : sizeOf s < sizeOf (Stmt.forEach varName count body) := by + have hbody := stmt_sizeOf_lt_forEach_body varName count body + omega + execStmtWithHelpers_eq_execStmt_of_helperSurfaceClosed_aux + spec fields fuel st s hsf)) + initialLoopState 0 bound termination_by sizeOf stmt theorem execStmtWithHelpers_eq_execStmt_of_helperSurfaceClosed diff --git a/Compiler/Proofs/IRGeneration/SupportedFragment.lean b/Compiler/Proofs/IRGeneration/SupportedFragment.lean index de6274998..2393fac99 100644 --- a/Compiler/Proofs/IRGeneration/SupportedFragment.lean +++ b/Compiler/Proofs/IRGeneration/SupportedFragment.lean @@ -340,6 +340,22 @@ inductive SupportedStmtList (fields : List Field) : List String → List Stmt findStructMember members memberName = some { name := memberName, wordOffset := wordOffset, packed := none } → SupportedStmtList fields scope [Stmt.setStructMember2 fieldName key1 key2 memberName value] + | forEachLiteralBounded + {scope : List String} + {varName : String} + {body : List Stmt} : + (∀ name, name ∈ collectStmtListNames body → name ∈ varName :: scope) → + SupportedStmtList fields (varName :: scope) body → + SupportedStmtList fields scope [Stmt.forEach varName (.literal 0) body] + /-- Literal loops with any bound are supported for empty bodies. This exercises + arbitrary Yul `for` recurrence while keeping non-empty positive loop bodies + outside the fragment until their body-preservation proof is threaded through + the loop step. -/ + | forEachLiteralEmpty + {scope : List String} + {varName : String} : + (n : Nat) → + SupportedStmtList fields scope [Stmt.forEach varName (.literal n) []] | requireClause {scope : List String} (clause : RequireLiteralGuardFamilyClause) diff --git a/Compiler/Proofs/IRGeneration/SupportedSpec.lean b/Compiler/Proofs/IRGeneration/SupportedSpec.lean index 36e2b77b8..a22db0d5d 100644 --- a/Compiler/Proofs/IRGeneration/SupportedSpec.lean +++ b/Compiler/Proofs/IRGeneration/SupportedSpec.lean @@ -1236,9 +1236,8 @@ def stmtTouchesUnsupportedStateSurface : Stmt → Bool exprTouchesUnsupportedStateSurface cond || stmtListTouchesUnsupportedStateSurface thenBranch || stmtListTouchesUnsupportedStateSurface elseBranch - | .forEach _ count body => - exprTouchesUnsupportedStateSurface count || - stmtListTouchesUnsupportedStateSurface body + | .forEach _ (.literal _) [] => false + | .forEach _ _ _ => true /-- Weaker Tier 2 state-surface gate used by the singleton storage-write bridge: all existing unsupported stateful forms remain excluded except for the proved @@ -1566,10 +1565,14 @@ def stmtTouchesUnsupportedContractSurface (stmt : Stmt) : Bool := | .storageArrayPush _ _ | .storageArrayPop _ | .setStorageArrayElement _ _ _ | .requireError _ _ _ | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .calldatacopy _ _ _ - | .returndataCopy _ _ _ | .revertReturndata | .forEach _ _ _ + | .returndataCopy _ _ _ | .revertReturndata | .emit _ _ | .internalCall _ _ | .internalCallAssign _ _ _ | .rawLog _ _ _ | .externalCallBind _ _ _ | .ecm _ _ | .tryExternalCallBind _ _ _ _ | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .forEach _ (.literal 0) body => + stmtListTouchesUnsupportedContractSurface body + | .forEach _ (.literal _) [] => false + | .forEach _ _ _ => true def stmtTouchesUnsupportedContractSurfaceWithEvents (events : List EventDef) (stmt : Stmt) : Bool := @@ -3013,6 +3016,14 @@ theorem SupportedStmtList.helperSurfaceClosed exact supportedStmtList_setMapping2WordSingle_helperSurfaceClosed hkey1 hkey2 hvalue | setStructMember2Single hkey1 _ hkey2 _ hvalue _ _ _ _ => exact supportedStmtList_setStructMember2Single_helperSurfaceClosed hkey1 hkey2 hvalue + | forEachLiteralBounded _ _ ih => + simpa [stmtListTouchesUnsupportedHelperSurface, + stmtTouchesUnsupportedHelperSurface, + exprTouchesUnsupportedHelperSurface] using ih + | forEachLiteralEmpty _ => + simp [stmtListTouchesUnsupportedHelperSurface, + stmtTouchesUnsupportedHelperSurface, + exprTouchesUnsupportedHelperSurface] | requireClause clause _ ih => simp [stmtListTouchesUnsupportedHelperSurface] constructor @@ -3191,6 +3202,13 @@ theorem SupportedStmtList.internalHelperCallNames_nil exprCompileCore_internalHelperCallNames_nil hkey2, exprCompileCore_internalHelperCallNames_nil hvalue, List.nil_append, List.append_nil] + | forEachLiteralBounded _ _ ih => + simpa [stmtListInternalHelperCallNames, + stmtInternalHelperCallNames, + exprInternalHelperCallNames] using ih + | forEachLiteralEmpty _ => + simp [stmtListInternalHelperCallNames, stmtInternalHelperCallNames, + exprInternalHelperCallNames] | requireClause clause _ ih => simp [stmtListInternalHelperCallNames] constructor @@ -4384,9 +4402,41 @@ theorem stmtTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed | storageArrayPop _ | setStorageArrayElement _ _ _ | requireError _ _ _ | revertError _ _ | returnValues _ | returnArray _ | returnBytes _ | returnStorageWords _ | calldatacopy _ _ _ | returndataCopy _ _ _ - | revertReturndata | forEach _ _ _ | emit _ _ | internalCall _ _ + | revertReturndata | emit _ _ | internalCall _ _ | internalCallAssign _ _ _ | rawLog _ _ _ | externalCallBind _ _ _ | ecm _ _ => cases hsurface + | forEach varName count body => + cases count with + | literal n => + cases n with + | zero => + cases body with + | nil => + simp [stmtTouchesUnsupportedHelperSurface, + stmtListTouchesUnsupportedHelperSurface, + exprTouchesUnsupportedHelperSurface] + | cons stmt rest => + simp only [stmtTouchesUnsupportedContractSurface, + stmtListTouchesUnsupportedContractSurface, + Bool.or_eq_false_iff] at hsurface + simp [stmtTouchesUnsupportedHelperSurface, + stmtListTouchesUnsupportedHelperSurface, + exprTouchesUnsupportedHelperSurface, + Bool.or_eq_false_iff] + exact ⟨ + stmtTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed + hsurface.1, + stmtListTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed + hsurface.2⟩ + | succ n => + cases body with + | nil => + simp [stmtTouchesUnsupportedHelperSurface, + stmtListTouchesUnsupportedHelperSurface, + exprTouchesUnsupportedHelperSurface] + | cons _ _ => + simp [stmtTouchesUnsupportedContractSurface] at hsurface + | _ => simp [stmtTouchesUnsupportedContractSurface] at hsurface termination_by sizeOf stmt theorem stmtListTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed @@ -5058,6 +5108,11 @@ private theorem supportedStmtList_usesArrayElement_false exprCompileCore_usesArrayElement_false hkey1, exprCompileCore_usesArrayElement_false hkey2, exprCompileCore_usesArrayElement_false hvalue, Bool.false_or] + | forEachLiteralBounded _ _ ih => + simpa [stmtListUsesArrayElement, stmtUsesArrayElement, + exprUsesArrayElement] using ih + | forEachLiteralEmpty _ => + simp [stmtListUsesArrayElement, stmtUsesArrayElement, exprUsesArrayElement] | requireClause clause _ ih => simp only [stmtListUsesArrayElement, Bool.or_eq_false_iff, Bool.false_or] exact ⟨by cases clause with | mk family n m p q message => @@ -5172,6 +5227,12 @@ private theorem supportedStmtList_usesStorageArrayElement_false exprCompileCore_usesStorageArrayElement_false hkey1, exprCompileCore_usesStorageArrayElement_false hkey2, exprCompileCore_usesStorageArrayElement_false hvalue, Bool.false_or] + | forEachLiteralBounded _ _ ih => + simpa [stmtListUsesStorageArrayElement, stmtUsesStorageArrayElement, + exprUsesStorageArrayElement] using ih + | forEachLiteralEmpty _ => + simp [stmtListUsesStorageArrayElement, stmtUsesStorageArrayElement, + exprUsesStorageArrayElement] | requireClause clause _ ih => simp only [stmtListUsesStorageArrayElement, Bool.or_eq_false_iff, Bool.false_or] exact ⟨by cases clause with | mk family n m p q message => @@ -5279,6 +5340,12 @@ private theorem supportedStmtList_usesDynamicBytesEq_false exprCompileCore_usesDynamicBytesEq_false hkey1, exprCompileCore_usesDynamicBytesEq_false hkey2, exprCompileCore_usesDynamicBytesEq_false hvalue, Bool.false_or] + | forEachLiteralBounded _ _ ih => + simpa [stmtListUsesDynamicBytesEq, stmtUsesDynamicBytesEq, + exprUsesDynamicBytesEq] using ih + | forEachLiteralEmpty _ => + simp [stmtListUsesDynamicBytesEq, stmtUsesDynamicBytesEq, + exprUsesDynamicBytesEq] | requireClause clause _ ih => simp only [stmtListUsesDynamicBytesEq, Bool.or_eq_false_iff, Bool.false_or] exact ⟨by cases clause with | mk family n m p q message => @@ -5644,6 +5711,11 @@ private theorem supportedStmtList_usesMulDiv512_false exprCompileCore_usesMulDiv512_false hkey1, exprCompileCore_usesMulDiv512_false hkey2, exprCompileCore_usesMulDiv512_false hvalue, Bool.false_or] + | forEachLiteralBounded _ _ ih => + simpa [stmtListUsesMulDiv512, stmtUsesMulDiv512, + exprUsesMulDiv512] using ih + | forEachLiteralEmpty _ => + simp [stmtListUsesMulDiv512, stmtUsesMulDiv512, exprUsesMulDiv512] | requireClause clause _ ih => simp only [stmtListUsesMulDiv512, Bool.or_eq_false_iff, Bool.false_or] exact ⟨by cases clause with | mk family n m p q message => @@ -5751,6 +5823,12 @@ private theorem supportedStmtList_usesParamDynamicHeadWord_false exprCompileCore_usesParamDynamicHeadWord_false hkey1, exprCompileCore_usesParamDynamicHeadWord_false hkey2, exprCompileCore_usesParamDynamicHeadWord_false hvalue, Bool.false_or] + | forEachLiteralBounded _ _ ih => + simpa [stmtListUsesParamDynamicHeadWord, stmtUsesParamDynamicHeadWord, + exprUsesParamDynamicHeadWord] using ih + | forEachLiteralEmpty _ => + simp [stmtListUsesParamDynamicHeadWord, stmtUsesParamDynamicHeadWord, + exprUsesParamDynamicHeadWord] | requireClause clause _ ih => simp only [stmtListUsesParamDynamicHeadWord, Bool.or_eq_false_iff, Bool.false_or] exact ⟨by cases clause with | mk family n m p q message => diff --git a/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean b/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean index cb7da6aa8..d8ab90b5e 100644 --- a/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean +++ b/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean @@ -4026,34 +4026,58 @@ theorem compileStmt_forEach_with_bridged_body intro yulStmt hMem simp only [List.mem_singleton] at hMem subst yulStmt + let usedNames := varName :: (inScopeNames ++ (collectExprNames count ++ collectStmtListNames body)) + let idxName := pickFreshName "__forEach_idx" usedNames + let countName := pickFreshName "__forEach_count" (idxName :: usedNames) refine BridgedStmt.for_ _ _ _ _ ?_ ?_ ?_ ?_ - · -- init: [YulStmt.let_ varName (YulExpr.lit 0)] + · -- init: idx := 0; cached count := countExpr; varName := 0 intro stmt hMemInit - simp only [List.mem_singleton] at hMemInit - subst stmt - exact BridgedStmt.straight _ - (BridgedStraightStmt.let_ varName (.lit 0) (BridgedExpr.lit 0)) - · -- cond: lt(ident varName, countExpr) + simp only [List.mem_cons, List.mem_singleton] at hMemInit + rcases hMemInit with rfl | hMemInit + · exact BridgedStmt.straight _ + (by + simpa [idxName] using + BridgedStraightStmt.let_ idxName (.lit 0) (BridgedExpr.lit 0)) + rcases hMemInit with rfl | hMemInit + · exact BridgedStmt.straight _ + (by + simpa [countName] using + BridgedStraightStmt.let_ countName countExpr hBC) + rcases hMemInit with rfl | hMemInit + · exact BridgedStmt.straight _ + (BridgedStraightStmt.let_ varName (.lit 0) (BridgedExpr.lit 0)) + · cases hMemInit + · -- cond: lt(ident idxName, ident countName) refine BridgedExpr.call "lt" _ (Or.inl (by simp [bridgedBuiltins])) ?_ intro arg hMemArg simp only [List.mem_cons, List.not_mem_nil, or_false] at hMemArg rcases hMemArg with rfl | rfl - · exact BridgedExpr.ident varName - · exact hBC - · -- post: [YulStmt.assign varName (add(ident varName, lit 1))] + · simpa [idxName] using BridgedExpr.ident idxName + · simpa [countName] using BridgedExpr.ident countName + · -- post: idxName := add(idxName, 1) intro stmt hMemPost simp only [List.mem_singleton] at hMemPost subst stmt - refine BridgedStmt.straight _ - (BridgedStraightStmt.assign varName _ ?_) - refine BridgedExpr.call "add" _ (Or.inl (by simp [bridgedBuiltins])) ?_ - intro arg hMemArg - simp only [List.mem_cons, List.not_mem_nil, or_false] at hMemArg - rcases hMemArg with rfl | rfl - · exact BridgedExpr.ident varName - · exact BridgedExpr.lit 1 - · -- body - exact hBBody + exact BridgedStmt.straight _ + (by + simpa [idxName] using + BridgedStraightStmt.assign idxName + (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1]) + (by + refine BridgedExpr.call "add" _ (Or.inl (by simp [bridgedBuiltins])) ?_ + intro arg hMemArg + simp only [List.mem_cons, List.not_mem_nil, or_false] at hMemArg + rcases hMemArg with rfl | rfl + · exact BridgedExpr.ident idxName + · exact BridgedExpr.lit 1)) + · -- body: assign the user-visible loop variable, then run the compiled body + exact BridgedStmts_cons + (BridgedStmt.straight _ + (by + simpa [idxName] using + BridgedStraightStmt.assign varName (YulExpr.ident idxName) + (BridgedExpr.ident idxName))) + hBBody theorem compileStmt_ite_with_noFuncDefs_body (fields : List Field) (events : List EventDef) (errors : List ErrorDef) diff --git a/PrintAxioms.lean b/PrintAxioms.lean index fecaa767e..59e28eba2 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -1994,6 +1994,7 @@ end Verity.AxiomAudit Compiler.Proofs.IRGeneration.FunctionBody.eval_compileRequireFailCond_core_onExpr Compiler.Proofs.IRGeneration.FunctionBody.runtimeStateMatchesIR_setVar_bindValue Compiler.Proofs.IRGeneration.FunctionBody.runtimeStateMatchesIR_setVar_irrelevant + Compiler.Proofs.IRGeneration.FunctionBody.runtimeStateMatchesIR_setVars_irrelevant Compiler.Proofs.IRGeneration.FunctionBody.compileStmt_core_ok Compiler.Proofs.IRGeneration.FunctionBody.runtimeStateMatchesIR_setBothMemory Compiler.Proofs.IRGeneration.FunctionBody.runtimeStateMatchesIR_updateMemoryEvents @@ -2001,6 +2002,7 @@ end Verity.AxiomAudit Compiler.Proofs.IRGeneration.FunctionBody.bindingsExactlyMatchIRVars_setMemory Compiler.Proofs.IRGeneration.FunctionBody.bindingsExactlyMatchIRVarsOnScope_setMemory Compiler.Proofs.IRGeneration.FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant + Compiler.Proofs.IRGeneration.FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVars_irrelevant Compiler.Proofs.IRGeneration.FunctionBody.bindingsExactlyMatchIRVarsOnScope_setVar_bindValue Compiler.Proofs.IRGeneration.FunctionBody.encodeEvents_withTransactionContext Compiler.Proofs.IRGeneration.FunctionBody.encodeStorage_withTransactionContext @@ -2179,6 +2181,7 @@ end Verity.AxiomAudit -- Compiler/Proofs/IRGeneration/GenericInduction.lean -- Compiler.Proofs.IRGeneration.stmtStepMatchesIRExecWithInternals_of_stmtStepMatchesIRExec -- private Compiler.Proofs.IRGeneration.CompiledStmtStep.withHelpers_of_helperSurfaceClosed + -- Compiler.Proofs.IRGeneration.compileStmtList_ok_of_stmtListGenericCore_early -- private -- Compiler.Proofs.IRGeneration.legacyCompatibleExternalStmtList_append -- private -- Compiler.Proofs.IRGeneration.legacyCompatibleExternalStmtList_of_exprStmtExprs -- private -- Compiler.Proofs.IRGeneration.legacyCompatibleExternalStmtList_revertWithMessage -- private @@ -2406,6 +2409,8 @@ end Verity.AxiomAudit Compiler.Proofs.IRGeneration.compiledStmtStep_ite -- Compiler.Proofs.IRGeneration.stmtListTouchesUnsupportedContractSurface_append -- private -- Compiler.Proofs.IRGeneration.stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites_append -- private + -- Compiler.Proofs.IRGeneration.stmtTouchesUnsupportedContractSurfaceExceptMappingWrites_eq_false_of_contractSurface -- private + -- Compiler.Proofs.IRGeneration.stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites_eq_false_of_contractSurface -- private -- Compiler.Proofs.IRGeneration.stmtListCompileCore_of_requireLiteralGuardFamilyClauses -- private -- Compiler.Proofs.IRGeneration.foldl_stmtNextScope_requireLiteralGuardFamilyClauses -- private -- Compiler.Proofs.IRGeneration.compiledStmtStep_letStorageField -- private @@ -2425,6 +2430,30 @@ end Verity.AxiomAudit -- Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_setStorageAddrSingleSlot_of_surface -- private -- Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_mstoreSingle_of_surface -- private -- Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_tstoreSingle_of_surface -- private + -- Compiler.Proofs.IRGeneration.sourceExec_forEach_literal_zero -- private + -- Compiler.Proofs.IRGeneration.sourceExec_forEach_literal_empty -- private + -- Compiler.Proofs.IRGeneration.forEachZero_fresh_facts -- private + -- Compiler.Proofs.IRGeneration.forEachLiteral_fresh_facts -- private + -- Compiler.Proofs.IRGeneration.evalIRExpr_forEachZeroCond_after_init -- private + -- Compiler.Proofs.IRGeneration.forEachZero_initFuel_of_slack -- private + -- Compiler.Proofs.IRGeneration.execIRStmts_forEach_empty_body_assign -- private + -- Compiler.Proofs.IRGeneration.execIRStmts_forEach_empty_post_increment -- private + -- Compiler.Proofs.IRGeneration.evalIRExpr_forEach_empty_cond_lt -- private + -- Compiler.Proofs.IRGeneration.evalIRExpr_forEach_empty_cond_eq -- private + -- Compiler.Proofs.IRGeneration.execIRStmt_forEach_empty_loop_from_idx -- private + -- Compiler.Proofs.IRGeneration.execIRStmt_forEach_empty_loop_idx_bound -- private + -- Compiler.Proofs.IRGeneration.forEachLiteral_loopFuel_of_slack -- private + -- Compiler.Proofs.IRGeneration.forEachLiteral_initFuel_of_slack -- private + -- Compiler.Proofs.IRGeneration.execIRStmts_forEach_literal_empty_compiled -- private + -- Compiler.Proofs.IRGeneration.execIRStmts_forEach_literal_zero_compiled -- private + -- Compiler.Proofs.IRGeneration.forEachZero_nextScopeIncluded -- private + -- Compiler.Proofs.IRGeneration.runtimeStateMatchesIR_forEachZeroLoop -- private + -- Compiler.Proofs.IRGeneration.bindingsExactly_forEachZeroBase -- private + -- Compiler.Proofs.IRGeneration.stmtStepMatches_forEach_literal_zero_final -- private + -- Compiler.Proofs.IRGeneration.forEach_empty_final_rel -- private + -- Compiler.Proofs.IRGeneration.stmtStepMatches_forEach_literal_empty_final -- private + -- Compiler.Proofs.IRGeneration.compiledStmtStep_forEach_literal_zero -- private + -- Compiler.Proofs.IRGeneration.compiledStmtStep_forEach_literal_empty -- private -- Compiler.Proofs.IRGeneration.stmtListGenericCore_singleton_setMappingUintSingle_of_slotSafety -- private -- Compiler.Proofs.IRGeneration.stmtListGenericCore_singleton_setMappingChainSingle_of_slotSafety -- private -- Compiler.Proofs.IRGeneration.stmtListGenericCore_singleton_setMappingSingle_of_slotSafety -- private @@ -2481,6 +2510,8 @@ end Verity.AxiomAudit -- Compiler.Proofs.IRGeneration.stmtNextScope_requireLiteralGuardFamilyClause -- private -- Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_append_of_surface_exceptMappingWrites -- private -- Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_requireClause_of_surface_exceptMappingWrites -- private + -- Compiler.Proofs.IRGeneration.stmtListTouchesUnsupportedContractSurface_body_of_singleton_forEach_zero -- private + -- Compiler.Proofs.IRGeneration.stmtListTouchesUnsupportedContractSurface_body_of_singleton_forEach_zero_exceptMappingWrites -- private Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_of_surface Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_of_surface_exceptMappingWrites Compiler.Proofs.IRGeneration.stmtListGenericCore_of_supportedStmtList_of_surface_exceptMappingWrites_stmtSafety @@ -2597,6 +2628,23 @@ end Verity.AxiomAudit Compiler.Proofs.IRGeneration.execIRStmtWithInternals_log3_of_eval_args Compiler.Proofs.IRGeneration.execIRStmtWithInternals_log4_of_eval_args Compiler.Proofs.IRGeneration.execIRInternalFunctionWithInternals_hides_caller_only_locals + Compiler.Proofs.IRGeneration.execIRStmt_for_init_noncontinue + Compiler.Proofs.IRGeneration.execIRStmt_for_cond_none + Compiler.Proofs.IRGeneration.execIRStmt_for_init_cond_zero + Compiler.Proofs.IRGeneration.execIRStmt_for_init_continue + Compiler.Proofs.IRGeneration.execIRStmt_for_body_noncontinue + Compiler.Proofs.IRGeneration.execIRStmt_for_post_noncontinue + Compiler.Proofs.IRGeneration.execIRStmt_for_one_continue + Compiler.Proofs.IRGeneration.execIRStmt_for_empty_init_recurrence + Compiler.Proofs.IRGeneration.execIRStmts_single_for_init_cond_zero + Compiler.Proofs.IRGeneration.execIRStmts_single_for_init_continue + Compiler.Proofs.IRGeneration.execIRStmts_cons_for_init_cond_zero + Compiler.Proofs.IRGeneration.execIRStmts_single_for_one_continue + Compiler.Proofs.IRGeneration.execIRStmts_cons_for_one_continue + Compiler.Proofs.IRGeneration.execIRStmts_cons_for_one_continue_of_loop_continue + Compiler.Proofs.IRGeneration.execIRStmt_forEach_shape_init_cond_zero + Compiler.Proofs.IRGeneration.execIRStmts_forEach_init_literal_zero + Compiler.Proofs.IRGeneration.execIRStmts_forEach_init_literal Compiler.Proofs.IRGeneration.execIRStmt_stop_succ Compiler.Proofs.IRGeneration.execIRStmt_stop_one_add Compiler.Proofs.IRGeneration.execIRStmt_stop_one_add_add @@ -2845,6 +2893,19 @@ end Verity.AxiomAudit Compiler.Proofs.IRGeneration.SourceSemantics.exists_writeUnindexedEventScratch_of_length_zero Compiler.Proofs.IRGeneration.SourceSemantics.exists_eventScratchMemoryAfterEmit?_of_supported_length Compiler.Proofs.IRGeneration.SourceSemantics.UInt256_size_eq_UINT256_MODULUS + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_zero + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_succ + Compiler.Proofs.IRGeneration.SourceSemantics.lookupBinding?_bindValue_same + Compiler.Proofs.IRGeneration.SourceSemantics.lookupValue_bindValue_same + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_boundState_lookupBinding? + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_boundState_lookupValue + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_zero_continue_state + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_succ_continue_iff + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_succ_continue + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_congr + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_empty_body + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_empty_body_zero_bound + Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_empty_body_positive_bound -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_literal -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_param -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_localVar -- private @@ -2985,6 +3046,7 @@ end Verity.AxiomAudit -- Compiler.Proofs.IRGeneration.SourceSemantics.expr_sizeOf_pos -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.stmt_sizeOf_lt_ite_then -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.stmt_sizeOf_lt_ite_else -- private + -- Compiler.Proofs.IRGeneration.SourceSemantics.stmt_sizeOf_lt_forEach_body -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.stmt_sizeOf_lt_cons -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.execStmtListWithHelpers_eq_execStmtList_of_helperSurfaceClosed_inner -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.execStmtWithHelpers_eq_execStmt_of_helperSurfaceClosed_aux -- private @@ -5481,4 +5543,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 5180 theorems/lemmas (3596 public, 1584 private, 0 sorry'd) +-- Total: 5242 theorems/lemmas (3628 public, 1614 private, 0 sorry'd) diff --git a/README.md b/README.md index 8224f76a8..d49511036 100644 --- a/README.md +++ b/README.md @@ -40,7 +40,7 @@ Verity proves that compilation preserves behavior at three stages. Each layer is **Layer 1** (EDSL to CompilationModel): the `verity_contract` macro generates both an executable Lean program and a compiler-facing model from a single definition. Per-contract bridge theorems prove they agree. -**Layer 2** (CompilationModel to IR): a generic whole-contract theorem covers the supported fragment with zero axioms. No per-contract proof effort needed. +**Layer 2** (CompilationModel to IR): a generic whole-contract theorem covers the supported fragment with zero axioms. No per-contract proof effort needed. `forEach` support is deliberately partial: zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops are proved, while positive non-empty loop bodies remain outside the current theorem. **Layer 3** (IR to Yul): all statement types are proven equivalent. The dispatch bridge is an explicit theorem hypothesis, not an axiom. diff --git a/artifacts/interpreter_feature_matrix.json b/artifacts/interpreter_feature_matrix.json index 816b29f4a..b706e6f99 100644 --- a/artifacts/interpreter_feature_matrix.json +++ b/artifacts/interpreter_feature_matrix.json @@ -535,7 +535,7 @@ "SpecInterpreter_basic": "unsupported", "SpecInterpreter_fuel": "supported", "IRInterpreter": "supported", - "proof_status": "proved" + "proof_status": "partial" }, { "feature": "emit", diff --git a/docs-site/content/compiler.mdx b/docs-site/content/compiler.mdx index 82f41cb77..7a76c27d7 100644 --- a/docs-site/content/compiler.mdx +++ b/docs-site/content/compiler.mdx @@ -165,7 +165,7 @@ constructor := some { > > **Axiomatized-primitive boundary**: The `keccak256` intrinsic also compiles, but it remains axiomatized in the current proof stack rather than fully modeled end to end. When it appears, archive `--trust-report` and add `--deny-axiomatized-primitives` if the selected contracts must stay inside the proved subset (see issue `#1411`). -**Statements** cover local variables, storage and mapping writes, `require`, `return`, memory writes, returndata copy and revert bubbling, `stop`, `ite` branching, bounded `forEach` loops, event emission, and internal calls. +**Statements** cover local variables, storage and mapping writes, `require`, `return`, memory writes, returndata copy and revert bubbling, `stop`, `ite` branching, event emission, internal calls, and a precisely scoped `forEach` fragment. The proved `forEach` cases are zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops; positive literal loops with non-empty bodies remain future proof work. Low-level calls, linear-memory primitives, `rawLog`, and `keccak256` compile but remain partially modeled in the proof interpreter. Functions or constructors that use direct assembly-shaped primitives without `localObligations [...]` fail closed under `--deny-axiomatized-primitives`. diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx index a390ee4e5..aaf2645ff 100644 --- a/docs-site/content/edsl-api-reference.mdx +++ b/docs-site/content/edsl-api-reference.mdx @@ -66,7 +66,9 @@ If `attempt` reverts with message `msg`, `tryCatch` runs `handler msg` on the st ### `forEach` -Bounded iteration in the compilation-model surface (`Stmt.forEach`). Accumulator-style loops use `Stmt.assignVar` inside `Stmt.forEach`; the macro path currently rejects mutating `let mut` locals from nested `forEach` bodies, so macro-authored contracts should use explicit memory scratch space for accumulators. +Bounded iteration in the compilation-model surface (`Stmt.forEach`). The current compiler proof covers zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops. Positive loops with non-empty bodies compile at the surface but are not yet part of the generic IR-generation preservation theorem. + +Accumulator-style loops use `Stmt.assignVar` inside `Stmt.forEach`; the macro path currently rejects mutating `let mut` locals from nested `forEach` bodies, so macro-authored contracts should use explicit memory scratch space for accumulators. ```verity forEach "i" count (do diff --git a/docs-site/content/verification.mdx b/docs-site/content/verification.mdx index 4b8a19e4d..ca12069ba 100644 --- a/docs-site/content/verification.mdx +++ b/docs-site/content/verification.mdx @@ -47,6 +47,8 @@ Reusable proof infrastructure in `Verity/Proofs/Stdlib/`: - **Typed IR**: `Compiler/TypedIRCompilerCorrectness.lean`, 36 supported statement fragments including ABI-head tuples, bytes, fixed/dynamic arrays, and strings as word-typed inputs. - **Yul semantics + preservation**: `Compiler/Proofs/YulGeneration/`, with an EVMYulLean-bridged native backend in `Compiler/Proofs/YulGeneration/Backends/`. +The Layer 2 `forEach` boundary is intentionally narrow: the generic theorem covers `Stmt.forEach varName (.literal 0) body` when `body` is supported, and `Stmt.forEach varName (.literal n) []` for any literal natural bound `n`. It does not yet prove positive loops with non-empty bodies or nonliteral bounds. + ## See also - [Proof Techniques](/proof-techniques), guard modeling, unfolding, list-sum reasoning. diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index bdb40c77a..57446524d 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -14,7 +14,7 @@ EDSL --> CompilationModel --> IR --> Yul --> EVM bytecode Every transition inside the proof envelope is either fully verified or recorded as an explicit assumption in the per-build trust report. The Yul-to-bytecode step is delegated to `solc --strict-assembly`. -**Layer 2**: Generic whole-contract theorem for the supported fragment. 0 axioms. 0 documented Lean axioms remain (AXIOMS.md). +**Layer 2**: Generic whole-contract theorem for the supported fragment. 0 axioms. 0 documented Lean axioms remain (AXIOMS.md). `forEach` proof support is partial: zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops are proved; positive non-empty loop bodies and nonliteral bounds are not yet proved. ## Quick facts diff --git a/docs/INTERPRETER_FEATURE_MATRIX.md b/docs/INTERPRETER_FEATURE_MATRIX.md index 62747fe19..5b104326e 100644 --- a/docs/INTERPRETER_FEATURE_MATRIX.md +++ b/docs/INTERPRETER_FEATURE_MATRIX.md @@ -100,7 +100,7 @@ Legend: **ok** = supported, **0** = returns 0 (not modeled), **del** = delegated | Return (storage words) | `Stmt.returnStorageWords` | ok | ok | -- | proved | | Stop | `Stmt.stop` | ok | ok | ok | proved | | If/else | `Stmt.ite` | ok | ok | ok | proved | -| For-each loop | `Stmt.forEach` | **rev** | ok | ok | proved | +| For-each loop | `Stmt.forEach` | **rev** | ok | ok | partial | | Event emission | `Stmt.emit` | ok | ok | -- | proved | | Internal call (stmt) | `Stmt.internalCall` | **rev** | ok | -- | proved | | Internal call assign | `Stmt.internalCallAssign` | **rev** | ok | -- | proved | @@ -115,6 +115,12 @@ Legend: **ok** = supported, **0** = returns 0 (not modeled), **del** = delegated Legend: **ok** = supported, **rev** = reverts (not modeled), **nop** = no-op (codegen concern), **--** = not applicable, **n/m** = not modeled. +`Stmt.forEach` proof coverage is intentionally partial: zero-bound loops with +supported bodies are proved, arbitrary literal-bound empty-body loops are +proved, and positive literal loops with non-empty bodies remain future work. +This is the current IR-generation proof boundary, not a claim about arbitrary +non-empty loop-body preservation. + ECMs include standard Verity-core modules for generic external-call mechanics, including `Compiler.Modules.Calls.bubblingValueCall`, which lowers Solidity-style `call{value: v}(data)` wrappers to Yul `call` and forwards exact @@ -188,7 +194,7 @@ Legend: **ok** = native evaluation. | Category | Proved | Assumed | Partial | Not Modeled | |---|---|---|---|---| | Expression features | 24 | 1 (`externalCall`) | 6 | 6 (`keccak256`, `call`, `staticcall`, `delegatecall`, `arrayElementDynamicWord`, `paramDynamicHeadWord`) | -| Statement features | 25 | 0 | 1 (`mstore`) | 6 (`calldatacopy`, `returndataCopy`, `revertReturndata`, `rawLog`, `externalCallBind`, `ecm`) | +| Statement features | 24 | 0 | 2 (`forEach`, `mstore`) | 6 (`calldatacopy`, `returndataCopy`, `revertReturndata`, `rawLog`, `externalCallBind`, `ecm`) | | Builtins (agreement) | 36 | 0 | 0 | 0 (delegated) | Proof-boundary features split across two buckets. Partially modeled features currently include runtime introspection (`blockNumber`, `contractAddress`, `chainid`) and single-word linear-memory forms (`mload`, `mstore`, `returndataOptionalBoolAt`). `selfBalance` is also partially modeled: it is compiler-supported and source-executable, but not yet included in the generic proof interpreter fragment. Fully not-modeled features currently include `keccak256`, low-level call / returndata plumbing (`call`, `staticcall`, `delegatecall`, `calldatacopy`, `returndataCopy`, `revertReturndata`), event emission (`rawLog`), and external call modules (`externalCallBind`, `ecm`). Dynamic struct-array head-word decoding (`arrayElementDynamicWord`) and direct dynamic-struct parameter head-word decoding (`paramDynamicHeadWord`) are also not modeled by proof interpreters yet. These features are still compiler-supported and are validated by differential testing (70,000+ test vectors against actual EVM execution). diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index d022c6261..97f935484 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -219,7 +219,7 @@ UnlinkPool, a ZK privacy pool, was the first non-trivial contract built with Ver | Feature | Issue | CompilationModel | Core/Interpreter | |---------|-------|-------------|-----------------| | If/else branching | #179 | `Stmt.ite` | `execStmt` mutual recursion | -| ForEach loops | #179 | `Stmt.forEach` | `execStmtsFuel` + `expandForEach` desugaring | +| ForEach loops | #179 | `Stmt.forEach` | `execStmtsFuel` + `expandForEach` desugaring; proofs cover zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops, while positive non-empty bodies remain future work | | Array/bytes params | #180 | `ParamType.bytes32`, `.array`, `.fixedArray`, `.bytes` | `arrayParams` in `EvalContext` | | Storage dynamic arrays | #1571 | `FieldType.dynamicArray`, `Expr.storageArrayLength` / `.storageArrayElement`, `Stmt.storageArrayPush` / `.storageArrayPop` / `.setStorageArrayElement` | compile-time/Yul lowering, source-side runtime semantics, and macro surface are in place; whole-contract proofs still pending | | Internal function calls | #181 | `Stmt.internalCall`, `Expr.internalCall`, `FunctionSpec.isInternal` | Statement + expression evaluation | diff --git a/scripts/check_proof_length.py b/scripts/check_proof_length.py index 537814807..09e489e13 100644 --- a/scripts/check_proof_length.py +++ b/scripts/check_proof_length.py @@ -80,6 +80,16 @@ "compiledStmtStep_require", "compiledStmtStep_return", "compiledStmtStep_ite", + # Nat-indexed forEach empty-body proof witnesses. Positive non-empty + # literal loops intentionally remain outside the supported fragment. The + # longer witnesses below are recurrence/state-relation proofs where + # splitting would duplicate the same loop-index, binder, and fuel facts. + "execIRStmt_forEach_empty_loop_from_idx", + "execIRStmt_for_empty_init_recurrence", + "forEach_empty_final_rel", + "stmtTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed", + "execIRStmts_forEach_literal_empty_compiled", + "stmtStepMatches_forEach_literal_empty_final", # --- Storage write compiled step proofs --- "compiledStmtStep_setStorage_singleSlot", "compiledStmtStep_setStorage_aliasSlots", diff --git a/scripts/ci_local_persistence.sh b/scripts/ci_local_persistence.sh index b64f79700..1d95b1532 100755 --- a/scripts/ci_local_persistence.sh +++ b/scripts/ci_local_persistence.sh @@ -20,7 +20,15 @@ EOF } sanitize_key() { - printf '%s' "$1" | tr -cs 'A-Za-z0-9._-' '_' + local sanitized hash + sanitized="$(printf '%s' "$1" | tr -cs 'A-Za-z0-9._-' '_')" + if [ "${#sanitized}" -le 200 ]; then + printf '%s' "$sanitized" + return + fi + + hash="$(printf '%s' "$1" | sha256sum | awk '{print $1}')" + printf '%s-%s' "${sanitized:0:160}" "$hash" } is_dir_empty() {