Scaffold proven forEach loop fragment

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)

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

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)

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)}