Skip to content

Commit 4101073

Browse files
Th0rgalTh0rgal
authored
Merge pull request #1944 from lfglabs-dev/thomas/foreach-nested-scope-fix
Track forEach counters in body scope to fix nested-loop shadowing
2 parents e0f8e48 + 825b5a7 commit 4101073

4 files changed

Lines changed: 46 additions & 24 deletions

File tree

‎Compiler/CompilationModel/Compile.lean‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,20 @@ private def compileAdtStorageWrite (fields : List Field)
9494
compileAdtFieldWrite (YulExpr.lit slot) idx (YulExpr.lit 0)
9595
pure (payloadBindings ++ tagStores ++ payloadStores ++ clearStores)
9696

97+
/-- Scope visible while compiling a `Stmt.forEach` body. The loop's synthetic
98+
counters `__forEach_idx`/`__forEach_count` are live across the whole body (Yul
99+
for-loop init variables are in scope in the body), so they must be tracked while
100+
compiling it. Otherwise a nested `forEach` re-derives the same names and the inner
101+
`let` collides with the outer one ("Variable name already taken in this scope").
102+
This is defeq to the codegen's inline `idxName :: countName :: varName :: inScopeNames`,
103+
so the generated Yul is unchanged; it exists as a named handle for the proofs. -/
104+
def forEachBodyScope (inScopeNames : List String) (varName : String)
105+
(count : Expr) (body : List Stmt) : List String :=
106+
let forUsedNames := varName :: (inScopeNames ++ collectExprNames count ++ collectStmtListNames body)
107+
let idxName := pickFreshName "__forEach_idx" forUsedNames
108+
let countName := pickFreshName "__forEach_count" (idxName :: forUsedNames)
109+
idxName :: countName :: varName :: inScopeNames
110+
97111
-- Compile statement to Yul (using mutual recursion for lists).
98112
-- When isInternal=true, Stmt.return compiles to `__ret := value; leave` so internal
99113
-- function execution terminates immediately without exiting the outer EVM call.
@@ -262,10 +276,12 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
262276
-- semantics where `count` is evaluated once and `varName` holds the last
263277
-- iteration state after the loop rather than the post-incremented counter.
264278
let countExpr ← compileExpr fields dynamicSource count
265-
let bodyStmts ← compileStmtList fields events errors dynamicSource internalRetNames isInternal (varName :: inScopeNames) adtTypes body
266279
let forUsedNames := varName :: (inScopeNames ++ collectExprNames count ++ collectStmtListNames body)
267280
let idxName := pickFreshName "__forEach_idx" forUsedNames
268281
let countName := pickFreshName "__forEach_count" (idxName :: forUsedNames)
282+
-- Compile the body with the synthetic counters in scope (see `forEachBodyScope`),
283+
-- so a nested `forEach` cannot re-derive colliding `__forEach_idx`/`__forEach_count`.
284+
let bodyStmts ← compileStmtList fields events errors dynamicSource internalRetNames isInternal (forEachBodyScope inScopeNames varName count body) adtTypes body
269285
let initStmts := [
270286
YulStmt.let_ idxName (YulExpr.lit 0),
271287
YulStmt.let_ countName countExpr,

‎Compiler/Proofs/IRGeneration/FunctionBody.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8135,10 +8135,12 @@ private theorem compileStmt_ok_any_scope_aux
81358135
| ok countIR =>
81368136
simp only [hcount] at hir ⊢
81378137
cases hbody1 : CompilationModel.compileStmtList
8138-
fields [] [] .calldata [] false (varName :: scope1) [] body with
8138+
fields [] [] .calldata [] false
8139+
(CompilationModel.forEachBodyScope scope1 varName count body) [] body with
81398140
| error e => simp [hbody1] at hir
81408141
| ok bodyIR1 =>
8141-
rcases ih.2 body (varName :: scope1) (varName :: scope2)
8142+
rcases ih.2 body (CompilationModel.forEachBodyScope scope1 varName count body)
8143+
(CompilationModel.forEachBodyScope scope2 varName count body)
81428144
(by simp [Stmt.forEach.sizeOf_spec] at hlt; omega) ⟨bodyIR1, hbody1⟩
81438145
with ⟨bodyIR2, hbody2⟩
81448146
simp only [hbody2]
@@ -8255,10 +8257,12 @@ private theorem compileStmt_ok_any_scope_with_surface_aux
82558257
| ok countIR =>
82568258
simp only [hcount] at hir ⊢
82578259
cases hbody1 : CompilationModel.compileStmtList
8258-
fields events errors .calldata [] false (varName :: scope1) [] body with
8260+
fields events errors .calldata [] false
8261+
(CompilationModel.forEachBodyScope scope1 varName count body) [] body with
82598262
| error e => simp [hbody1] at hir
82608263
| ok bodyIR1 =>
8261-
rcases ih.2 body (varName :: scope1) (varName :: scope2)
8264+
rcases ih.2 body (CompilationModel.forEachBodyScope scope1 varName count body)
8265+
(CompilationModel.forEachBodyScope scope2 varName count body)
82628266
(by simp [Stmt.forEach.sizeOf_spec] at hlt; omega) ⟨bodyIR1, hbody1⟩
82638267
with ⟨bodyIR2, hbody2⟩
82648268
simp only [hbody2]

‎Compiler/Proofs/IRGeneration/GenericInduction.lean‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1054,7 +1054,7 @@ theorem legacyCompatibleExternalStmtList_of_compileStmt_ok_on_supportedContractS
10541054
simp only [CompilationModel.compileStmt, bind, Except.bind] at hcompile
10551055
cases hbody :
10561056
CompilationModel.compileStmtList fields events errors .calldata [] false
1057-
(varName :: inScopeNames) [] body with
1057+
(CompilationModel.forEachBodyScope inScopeNames varName (Expr.literal 0) body) [] body with
10581058
| error e => simp [CompilationModel.compileExpr, pure, Except.pure, hbody] at hcompile
10591059
| ok loopBodyIR =>
10601060
simp [CompilationModel.compileExpr, hbody] at hcompile
@@ -3620,12 +3620,13 @@ private theorem stmtListScopeCore_of_unsupportedContractSurface_eq_false
36203620
simp only [CompilationModel.compileStmt, bind, Except.bind] at hhead
36213621
cases hbody :
36223622
CompilationModel.compileStmtList fields [] [] .calldata [] false
3623-
(varName :: scope) [] body with
3623+
(CompilationModel.forEachBodyScope scope varName (Expr.literal 0) body) [] body with
36243624
| error e => simp [CompilationModel.compileExpr, pure, Except.pure, hbody] at hhead
36253625
| ok loopBodyIR =>
36263626
exact .forEachLiteralZero
36273627
(stmtListScopeCore_of_unsupportedContractSurface_eq_false
3628-
fields (varName :: scope) body loopBodyIR hbodySurface hbody)
3628+
fields (CompilationModel.forEachBodyScope scope varName (Expr.literal 0) body)
3629+
body loopBodyIR hbodySurface hbody)
36293630
ihRest
36303631
| succ n =>
36313632
cases body with
@@ -3756,12 +3757,13 @@ theorem stmtListScopeCore_prefix_of_compileStmtList_ok_of_stmtListTouchesUnsuppo
37563757
simp only [CompilationModel.compileStmt, bind, Except.bind] at hhead
37573758
cases hbody :
37583759
CompilationModel.compileStmtList fields [] [] .calldata [] false
3759-
(varName :: scope) [] body with
3760+
(CompilationModel.forEachBodyScope scope varName (Expr.literal 0) body) [] body with
37603761
| error e => simp [CompilationModel.compileExpr, pure, Except.pure, hbody] at hhead
37613762
| ok loopBodyIR =>
37623763
exact StmtListScopeCore.forEachLiteralZero
37633764
(stmtListScopeCore_of_unsupportedContractSurface_eq_false
3764-
fields (varName :: scope) body loopBodyIR hbodySurface hbody)
3765+
fields (CompilationModel.forEachBodyScope scope varName (Expr.literal 0) body)
3766+
body loopBodyIR hbodySurface hbody)
37653767
(ih hrestSurface htail)
37663768
| succ n =>
37673769
cases body with
@@ -13708,9 +13710,9 @@ private theorem compiledStmtStep_forEach_literal_zero
1370813710
rcases compileStmtList_ok_of_stmtListGenericCore_early
1370913711
(fields := fields)
1371013712
(scope := varName :: scope)
13711-
(inScopeNames := varName :: scope)
13713+
(inScopeNames := CompilationModel.forEachBodyScope scope varName (Expr.literal 0) body)
1371213714
hbodyGeneric
13713-
FunctionBody.scopeNamesIncluded_refl with
13715+
(fun name hmem => List.mem_cons_of_mem _ (List.mem_cons_of_mem _ hmem)) with
1371413716
⟨bodyIR, hbodyCompile⟩
1371513717
refine ⟨forEachZeroCompiledIR scope varName body bodyIR, ?_⟩
1371613718
refine

‎Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4002,7 +4002,7 @@ theorem compileStmt_forEach_with_bridged_body
40024002
(hCount : BridgedSourceExpr count)
40034003
(hBody : ∀ {out : List YulStmt},
40044004
compileStmtList fields events errors dynamicSource internalRetNames
4005-
isInternal (varName :: inScopeNames) [] body = .ok out →
4005+
isInternal (forEachBodyScope inScopeNames varName count body) [] body = .ok out →
40064006
BridgedStmts out) :
40074007
∀ {out : List YulStmt},
40084008
compileStmt fields events errors dynamicSource internalRetNames isInternal
@@ -4015,7 +4015,7 @@ theorem compileStmt_forEach_with_bridged_body
40154015
| ok countExpr =>
40164016
simp [hCExpr] at hOk
40174017
cases hBodyOk : compileStmtList fields events errors dynamicSource
4018-
internalRetNames isInternal (varName :: inScopeNames) [] body with
4018+
internalRetNames isInternal (forEachBodyScope inScopeNames varName count body) [] body with
40194019
| error err => simp [hBodyOk] at hOk
40204020
| ok bodyOut =>
40214021
simp [hBodyOk, Pure.pure, Except.pure] at hOk
@@ -4128,7 +4128,7 @@ theorem compileStmt_forEach_with_noFuncDefs_body
41284128
(varName : String) (count : Expr) (body : List Stmt)
41294129
(hBody : ∀ {out : List YulStmt},
41304130
compileStmtList fields events errors dynamicSource internalRetNames
4131-
isInternal (varName :: inScopeNames) [] body = .ok out →
4131+
isInternal (forEachBodyScope inScopeNames varName count body) [] body = .ok out →
41324132
Native.yulStmtsContainFuncDef out = false) :
41334133
∀ {out : List YulStmt},
41344134
compileStmt fields events errors dynamicSource internalRetNames isInternal
@@ -4141,7 +4141,7 @@ theorem compileStmt_forEach_with_noFuncDefs_body
41414141
| ok countExpr =>
41424142
simp [hCExpr] at hOk
41434143
cases hBodyOk : compileStmtList fields events errors dynamicSource
4144-
internalRetNames isInternal (varName :: inScopeNames) [] body with
4144+
internalRetNames isInternal (forEachBodyScope inScopeNames varName count body) [] body with
41454145
| error err => simp [hBodyOk] at hOk
41464146
| ok bodyOut =>
41474147
have hBodyNoFunc := hBody hBodyOk
@@ -5595,7 +5595,7 @@ theorem compileStmt_external_forEach_body_with_errors_bridged
55955595
hCount ?_ hOk
55965596
intro bodyOut hBodyOk
55975597
exact compileStmtList_external_body_with_errors_bridged fields events
5598-
errors dynamicSource internalRetNames body (varName :: inScopeNames)
5598+
errors dynamicSource internalRetNames body _
55995599
hBody hBodyOk
56005600

56015601
/-- External forEach-wrapped with-errors source bodies compile to Yul lists
@@ -5673,7 +5673,7 @@ theorem compileStmt_internal_forEach_body_with_errors_bridged
56735673
hCount ?_ hOk
56745674
intro bodyOut hBodyOk
56755675
exact compileStmtList_internal_body_with_errors_bridged fields events
5676-
errors dynamicSource internalRetNames body (varName :: inScopeNames)
5676+
errors dynamicSource internalRetNames body _
56775677
hBody hBodyOk
56785678

56795679
/-- Internal forEach-wrapped with-errors source bodies compile to Yul lists
@@ -5895,7 +5895,7 @@ mutual
58955895
intro bodyOut hBodyOk
58965896
exact compileStmtList_external_recursive_body_with_errors_bridged fields
58975897
events errors dynamicSource internalRetNames hBody
5898-
(varName :: inScopeNames) hBodyOk
5898+
_ hBodyOk
58995899

59005900
theorem compileStmtList_external_recursive_body_with_errors_bridged
59015901
(fields : List Field) (events : List EventDef) (errors : List ErrorDef)
@@ -6012,7 +6012,7 @@ mutual
60126012
intro bodyOut hBodyOk
60136013
exact compileStmtList_internal_recursive_body_with_errors_bridged fields
60146014
events errors dynamicSource internalRetNames hBody
6015-
(varName :: inScopeNames) hBodyOk
6015+
_ hBodyOk
60166016

60176017
theorem compileStmtList_internal_recursive_body_with_errors_bridged
60186018
(fields : List Field) (events : List EventDef) (errors : List ErrorDef)
@@ -7921,7 +7921,7 @@ mutual
79217921
intro bodyOut hBodyOk
79227922
exact compileStmtList_external_recursive_body_with_raw_log_bridged fields
79237923
events errors dynamicSource internalRetNames hBody
7924-
(varName :: inScopeNames) hBodyOk
7924+
_ hBodyOk
79257925

79267926
theorem compileStmtList_external_recursive_body_with_raw_log_bridged
79277927
(fields : List Field) (events : List EventDef) (errors : List ErrorDef)
@@ -8038,7 +8038,7 @@ mutual
80388038
intro bodyOut hBodyOk
80398039
exact compileStmtList_internal_recursive_body_with_raw_log_bridged fields
80408040
events errors dynamicSource internalRetNames hBody
8041-
(varName :: inScopeNames) hBodyOk
8041+
_ hBodyOk
80428042

80438043
theorem compileStmtList_internal_recursive_body_with_raw_log_bridged
80448044
(fields : List Field) (events : List EventDef) (errors : List ErrorDef)
@@ -8111,7 +8111,7 @@ mutual
81118111
dynamicSource internalRetNames false inScopeNames varName count body ?_ hOk
81128112
exact compileStmtList_external_recursive_body_with_raw_log_noFuncDefs
81138113
fields events errors dynamicSource internalRetNames hBody
8114-
(varName :: inScopeNames)
8114+
_
81158115

81168116
theorem compileStmtList_external_recursive_body_with_raw_log_noFuncDefs
81178117
(fields : List Field) (events : List EventDef) (errors : List ErrorDef)
@@ -8181,7 +8181,7 @@ mutual
81818181
dynamicSource internalRetNames true inScopeNames varName count body ?_ hOk
81828182
exact compileStmtList_internal_recursive_body_with_raw_log_noFuncDefs
81838183
fields events errors dynamicSource internalRetNames hBody
8184-
(varName :: inScopeNames)
8184+
_
81858185

81868186
theorem compileStmtList_internal_recursive_body_with_raw_log_noFuncDefs
81878187
(fields : List Field) (events : List EventDef) (errors : List ErrorDef)

0 commit comments

Comments
 (0)