Skip to content

Commit 858bc08

Browse files
Th0rgalgithub-actions[bot]
Th0rgal
and
github-actions[bot]
authored
Scaffold proven forEach loop fragment (#1935)
* Add IR for-loop execution lemmas * Add source forEach loop semantics * Align forEach lowering with source semantics * Add bounded forEach fragment scaffolding * chore: auto-refresh derived artifacts * Add forEach source loop helper lemmas * Add reusable Yul for-loop execution lemmas * Add forEach zero-init execution lemma * Prove zero-bound forEach preservation * Split zero-bound forEach proof * chore: auto-refresh derived artifacts * Prove one-iteration forEach preservation * chore: auto-refresh derived artifacts * Prove two-iteration forEach preservation * chore: auto-refresh derived artifacts * Allowlist staged forEach proof shapes * Prove generic empty forEach loops * chore: auto-refresh derived artifacts * Allowlist generalized forEach proof witnesses * Document forEach proof boundary * Trigger proof verification rerun * Clarify forEach proof boundary * Clarify literal forEach fragment comment * Shorten local persistence cache keys * Address forEach proof review findings * chore: auto-refresh derived artifacts * docs: clarify proven forEach fragment --------- Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
1 parent f49a1dc commit 858bc08

21 files changed

Lines changed: 2379 additions & 48 deletions

‎Compiler/CompilationModel/Compile.lean‎

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -246,13 +246,25 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
246246
]]
247247

248248
| Stmt.forEach varName count body => do
249-
-- Bounded loop: for { let i := 0 } lt(i, count) { i := add(i, 1) } { body } (#179)
249+
-- Bounded loop: evaluate `count` once into a cached local, drive iteration
250+
-- with a fresh internal counter, and assign the user-visible `varName` to
251+
-- the current counter at the top of each iteration. This matches the source
252+
-- semantics where `count` is evaluated once and `varName` holds the last
253+
-- iteration state after the loop rather than the post-incremented counter.
250254
let countExpr ← compileExpr fields dynamicSource count
251255
let bodyStmts ← compileStmtList fields events errors dynamicSource internalRetNames isInternal (varName :: inScopeNames) adtTypes body
252-
let initStmts := [YulStmt.let_ varName (YulExpr.lit 0)]
253-
let condExpr := YulExpr.call "lt" [YulExpr.ident varName, countExpr]
254-
let postStmts := [YulStmt.assign varName (YulExpr.call "add" [YulExpr.ident varName, YulExpr.lit 1])]
255-
pure [YulStmt.for_ initStmts condExpr postStmts bodyStmts]
256+
let forUsedNames := varName :: (inScopeNames ++ collectExprNames count ++ collectStmtListNames body)
257+
let idxName := pickFreshName "__forEach_idx" forUsedNames
258+
let countName := pickFreshName "__forEach_count" (idxName :: forUsedNames)
259+
let initStmts := [
260+
YulStmt.let_ idxName (YulExpr.lit 0),
261+
YulStmt.let_ countName countExpr,
262+
YulStmt.let_ varName (YulExpr.lit 0)
263+
]
264+
let condExpr := YulExpr.call "lt" [YulExpr.ident idxName, YulExpr.ident countName]
265+
let postStmts := [YulStmt.assign idxName (YulExpr.call "add" [YulExpr.ident idxName, YulExpr.lit 1])]
266+
let bodyWithBind := YulStmt.assign varName (YulExpr.ident idxName) :: bodyStmts
267+
pure [YulStmt.for_ initStmts condExpr postStmts bodyWithBind]
256268

257269
| Stmt.unsafeBlock _ body => do
258270
-- Unsafe block: transparent wrapper, compile inner body directly (#1728, Axis 6 Step 6a)

‎Compiler/Proofs/EndToEnd.lean‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5291,6 +5291,27 @@ theorem supportedStmtList_safe_of_state_effect_closed
52915291
| setStructMember2Single =>
52925292
simp [stmtListTouchesUnsupportedStateSurface,
52935293
stmtTouchesUnsupportedStateSurface] at hState
5294+
| @forEachLiteralBounded scope varName body _ _ _ =>
5295+
cases body with
5296+
| nil =>
5297+
exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog
5298+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons
5299+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach
5300+
_ _ _
5301+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _)
5302+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
5303+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
5304+
| cons _ _ =>
5305+
simp [stmtListTouchesUnsupportedStateSurface,
5306+
stmtTouchesUnsupportedStateSurface] at hState
5307+
| forEachLiteralEmpty _ =>
5308+
exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog
5309+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons
5310+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach
5311+
_ _ _
5312+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _)
5313+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
5314+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
52945315
| requireClause clause _ ih =>
52955316
simpa using
52965317
Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.append
@@ -5557,6 +5578,28 @@ theorem supportedStmtList_safe_of_state_except_mapping_writes_stmt_safety
55575578
(Compiler.Proofs.YulGeneration.Backends.bridgedSourceExpr_of_exprCompileCore hKey2)
55585579
(Compiler.Proofs.YulGeneration.Backends.bridgedSourceExpr_of_exprCompileCore hValue)
55595580
hMapping2 hMembers hFindMember rfl hZero hSlots
5581+
| @forEachLiteralBounded scope varName body _ _ _ =>
5582+
cases body with
5583+
| nil =>
5584+
exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog
5585+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons
5586+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach
5587+
_ _ _
5588+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _)
5589+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
5590+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
5591+
| cons _ _ =>
5592+
simp [stmtListTouchesUnsupportedStateSurfaceExceptMappingWrites,
5593+
stmtTouchesUnsupportedStateSurfaceExceptMappingWrites,
5594+
stmtTouchesUnsupportedStateSurface] at hState
5595+
| forEachLiteralEmpty _ =>
5596+
exact Compiler.Proofs.YulGeneration.Backends.BridgedSafeStmts.externalRecursiveRawLog
5597+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.cons
5598+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmt.forEach
5599+
_ _ _
5600+
(Compiler.Proofs.YulGeneration.Backends.BridgedSourceExpr.literal _)
5601+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
5602+
Compiler.Proofs.YulGeneration.Backends.BridgedSourceExternalRecursiveBodyWithRawLogStmts.nil)
55605603
| @requireClause scope clause rest _ ih =>
55615604
have hTailSafety :
55625605
∀ stmt ∈ rest, StmtMappingWriteSlotSafe fields stmt := by

‎Compiler/Proofs/IRGeneration/Contract.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,11 @@ private theorem legacyCompatibleExternalStmtList_append
132132
| block body rest hbody hrest ihBody ihRest =>
133133
intro after hafter
134134
simpa using LegacyCompatibleExternalStmtList.block body (rest ++ after) hbody (ihRest after hafter)
135+
| for_ init cond post body rest hinit hpost hbody hrest ihInit ihPost ihBody ihRest =>
136+
intro after hafter
137+
simpa using
138+
LegacyCompatibleExternalStmtList.for_ init cond post body (rest ++ after)
139+
hinit hpost hbody (ihRest after hafter)
135140
| funcDef name params rets body rest hbody hrest ihBody ihRest =>
136141
intro after hafter
137142
simpa using LegacyCompatibleExternalStmtList.funcDef name params rets body (rest ++ after) hbody (ihRest after hafter)

‎Compiler/Proofs/IRGeneration/FunctionBody.lean‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7275,6 +7275,23 @@ theorem runtimeStateMatchesIR_setVar_irrelevant
72757275
cases state
72767276
simpa [runtimeStateMatchesIR, IRState.setVar] using hmatch
72777277

7278+
theorem runtimeStateMatchesIR_setVars_irrelevant
7279+
{fields : List Field}
7280+
{runtime : SourceSemantics.RuntimeState}
7281+
{state : IRState}
7282+
{updates : List (String × Nat)}
7283+
(hmatch : runtimeStateMatchesIR fields runtime state) :
7284+
runtimeStateMatchesIR fields runtime (state.setVars updates) := by
7285+
induction updates generalizing state with
7286+
| nil =>
7287+
simpa [IRState.setVars] using hmatch
7288+
| cons update updates ih =>
7289+
cases update with
7290+
| mk name value =>
7291+
simp [IRState.setVars]
7292+
exact ih (runtimeStateMatchesIR_setVar_irrelevant
7293+
(state := state) (name := name) (value := value) hmatch)
7294+
72787295
def stmtResultMatchesIRExecExact :
72797296
SourceSemantics.StmtResult → IRExecResult → Prop
72807297
| .continue runtime, .continue state =>
@@ -7492,6 +7509,28 @@ theorem bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant
74927509
· rw [getVar_setVar_ne state tempName name value hEq]
74937510
exact hexact name hname
74947511

7512+
theorem bindingsExactlyMatchIRVarsOnScope_setVars_irrelevant
7513+
{scope : List String}
7514+
{bindings : List (String × Nat)}
7515+
{state : IRState}
7516+
{updates : List (String × Nat)}
7517+
(hexact : bindingsExactlyMatchIRVarsOnScope scope bindings state)
7518+
(hfresh : ∀ update ∈ updates, update.1 ∉ scope) :
7519+
bindingsExactlyMatchIRVarsOnScope scope bindings (state.setVars updates) := by
7520+
induction updates generalizing state with
7521+
| nil =>
7522+
simpa [IRState.setVars] using hexact
7523+
| cons update updates ih =>
7524+
cases update with
7525+
| mk name value =>
7526+
simp [IRState.setVars]
7527+
apply ih
7528+
· exact bindingsExactlyMatchIRVarsOnScope_setVar_irrelevant
7529+
(state := state) (tempName := name) (value := value)
7530+
hexact (hfresh (name, value) (by simp))
7531+
· intro update hmem
7532+
exact hfresh update (by simp [hmem])
7533+
74957534
theorem bindingsExactlyMatchIRVarsOnScope_setVar_bindValue
74967535
{scope : List String}
74977536
{bindings : List (String × Nat)}

0 commit comments

Comments
 (0)