Skip to content

Commit f026ac0

Browse files
Th0rgalTh0rgal
authored
proofs: continue generic layer 2 compiler verification (#1556)
* docs: add generic layer2 implementation plan * proofs: add whole-contract support witnesses * chore: regenerate proof surfaces * Add generic layer2 contract theorem skeleton * isolate compile function table extraction plumbing * Close compile function-table extraction proof * Factor supported Layer2 function interface * Document generic layer2 function axiom * Strengthen IR/source binding invariants * Prove duplicate-name detection matches Nodup * Refine generic layer2 validation interface * Strengthen param name invariants for layer 2 proof * Sync supported function axiom registry * docs: align verification status with current proof boundaries * refactor layer2 proof spine * docs: clarify Layer 1 vs contract spec proofs * Prove generic Layer 2 parameter-state exactness * Prove Layer 2 initial state normalization * Add Layer 2 exact-state expression lemmas * Add bound-name invariants for Layer 2 expressions * Add Layer 2 boolean expression helpers * Add bounded-binding invariants for Layer 2 * Add generic ABI binding invariants for Layer 2 * Add bounded source expression leaf lemmas * Add IR builtin expression proof lemmas * Add compileExpr leaf correctness lemmas * Add compileExpr context leaf correctness lemmas * Add compileExpr boolean shape lemmas * Add compileExpr proofs for eq lt gt * Prove more compiled comparison cases * Add compileExpr arithmetic shape lemmas * Add compileExpr correctness lemmas for add and mul * Add Uint256 Nat bridge lemmas for expression proofs * Add compileExpr correctness for div and mod * prove compileExpr sub semantics * Add logical operator compileExpr proofs * Add recursive compileExpr core proofs * Add core statement execution lemmas * Add recursive compile lemmas for core stmt lists * Add core IR sequencing lemmas * Add core stmt list execution proof * Bypass body axiom for core stmt lists * Add core require shape lemmas * Prove core require statement simulation * Add scoped binding invariants for core stmt proofs * Make pickFreshName provably fresh * Add IR block and if sequencing lemmas * Add terminal core statement-list fragment * Add scoped core expression correctness lemmas * Document nested block fuel gap * Add structural fuel lower bounds for compiled functions * Generalize param-loading proofs to extra fuel * Prove core supported functions with structural fuel * Add terminal-core stmt list compilation theorem * Add terminal ite fuel lower bounds * Strengthen terminal ite size-of fuel bounds * Strengthen terminal ite branch exec fuel bounds * Add terminal core non-continue lemma * Add terminal-core IR non-continue inversions * Add generic IR sequencing fuel lemmas * Add terminal ite block fuel helpers * Add scoped fresh-temp lemmas for terminal ite proofs * Add terminal ite fuel decomposition lemmas * Add terminal-core fuel helpers * Add generic IR eval helpers for terminal ite * Add nonzero-fuel IR execution helpers * Add terminal ite exec fuel facts * Add terminal ite block fuel wrapper * Add symbolic terminal IR fuel helpers * Add terminal ite scope inclusion lemmas * Export terminal fuel list rewrites * Add terminal ite branch-entry wrappers * Factor terminal ite then-branch composition * Add terminal ite else fuel helpers * Add terminal ite else composition lemmas * Add two-cons sizeOf rewrites for terminal proofs * Add terminal core tail exec fuel rewrites * Add step-fuel IR execution wrappers * Add two-head whole fuel rewrite * Add scope transport lemmas for terminal core proof * Add extra-fuel stop bridge * Add extra-fuel terminal return theorem * Extract whole-fuel IR composition wrappers * Extract compileStmtList cons normalization * Add compileStmtList cons inversion lemma * Extract terminal-core compile nonempty lemma * Add append-normalized whole-fuel wrappers * Extract terminal ite source-branch equalities * Add scope-local terminal core eval wrappers * Add then-branch tail fuel rewrite for terminal ite * Extract terminal ite compile inversion lemma * Add terminal ite semantic lift wrappers * Add terminal-core tail inversion lemmas * Add whole-fuel terminal core append lemmas * Add terminal ite compile-list inversion * Add scope-local return whole-fuel helper * Add scope-local whole-fuel core prefix wrappers * Add singleton tail extra-fuel composition helper * Add tail-fuel core prefix wrappers * Add semantic terminal-core head wrappers * Clarify terminal ite spent-fuel blocker * Remove unused dispatch axioms * Fix Yul blob-base-fee alignment and preservation build * Narrow layer3 dispatch axioms * docs: refine buildSwitch axiom blocker * Prove buildSwitch dispatch normalization * docs: narrow switch-case bridge blocker * Narrow layer2 axioms to non-core bodies * Narrow Layer 3 dispatch guard assumptions * Add checked dispatch guard helper lemmas * docs: align layer 3 axiom counts * Narrow the switch-case bridge axiom * proofs: narrow non-core layer2 body axiom
1 parent 5ec6593 commit f026ac0

29 files changed

Lines changed: 14458 additions & 211 deletions

‎AXIOMS.md‎

Lines changed: 310 additions & 50 deletions
Large diffs are not rendered by default.

‎Compiler.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,14 @@ import Compiler.Yul.PatchRules
2828
import Compiler.Proofs.MappingSlot
2929
import Compiler.Proofs.IRGeneration.Expr
3030
import Compiler.Proofs.IRGeneration.IRInterpreter
31+
import Compiler.Proofs.IRGeneration.SupportedFragment
32+
import Compiler.Proofs.IRGeneration.Contract
33+
import Compiler.Proofs.IRGeneration.Dispatch
34+
import Compiler.Proofs.IRGeneration.Function
35+
import Compiler.Proofs.IRGeneration.FunctionBody
36+
import Compiler.Proofs.IRGeneration.ParamLoading
37+
import Compiler.Proofs.IRGeneration.SupportedSpec
38+
import Compiler.Proofs.IRGeneration.SourceSemantics
3139
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter
3240
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas
3341
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeTest

‎Compiler/CompilationModel/Dispatch.lean‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ private def compileSpecialEntrypoint (fields : List Field) (events : List EventD
6868
body := bodyChunks
6969
}
7070

71-
private def pickUniqueFunctionByName (name : String) (funcs : List FunctionSpec) :
71+
def pickUniqueFunctionByName (name : String) (funcs : List FunctionSpec) :
7272
Except String (Option FunctionSpec) :=
7373
match funcs.filter (·.name == name) with
7474
| [] => pure none
@@ -97,7 +97,7 @@ def compileConstructor (fields : List Field) (events : List EventDef) (errors :
9797
-- Use `Compiler.Selector.compileChecked` on caller-provided selector lists.
9898
-- WARNING: Order matters! If selector list is reordered but function list isn't,
9999
-- functions will be mapped to wrong selectors with no runtime error.
100-
def compile (spec : CompilationModel) (selectors : List Nat) : Except String IRContract := do
100+
def validateCompileInputs (spec : CompilationModel) (selectors : List Nat) : Except String Unit := do
101101
validateIdentifierShapes spec
102102
match firstInvalidSlotAliasRange spec.slotAliasRanges with
103103
| some (idx, range) =>
@@ -111,7 +111,6 @@ def compile (spec : CompilationModel) (selectors : List Nat) : Except String IRC
111111
pure ()
112112
let fields := applySlotAliasRanges spec.fields spec.slotAliasRanges
113113
let externalFns := spec.functions.filter (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)
114-
let internalFns := spec.functions.filter (·.isInternal)
115114
match firstInternalDynamicParam spec.functions with
116115
| some (fnName, paramName, ty) =>
117116
throw s!"Compilation error: internal function '{fnName}' parameter '{paramName}' has dynamic type {repr ty}, which is currently unsupported ({issue753Ref}). Internal dynamic ABI lowering is not implemented yet."
@@ -222,8 +221,6 @@ def compile (spec : CompilationModel) (selectors : List Nat) : Except String IRC
222221
pure ()
223222
for err in spec.errors do
224223
validateErrorDef err
225-
let fallbackSpec ← pickUniqueFunctionByName "fallback" spec.functions
226-
let receiveSpec ← pickUniqueFunctionByName "receive" spec.functions
227224
if externalFns.length != selectors.length then
228225
throw s!"Selector count mismatch for {spec.name}: {selectors.length} selectors for {externalFns.length} external functions"
229226
match firstDuplicateSelector selectors with
@@ -232,6 +229,15 @@ def compile (spec : CompilationModel) (selectors : List Nat) : Except String IRC
232229
let nameStr := if names.isEmpty then "<unknown>" else String.intercalate ", " names
233230
throw s!"Selector collision in {spec.name}: {dup} assigned to {nameStr}"
234231
| none => pure ()
232+
233+
def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Except String IRContract := do
234+
let fields := applySlotAliasRanges spec.fields spec.slotAliasRanges
235+
let externalFns := spec.functions.filter (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)
236+
let internalFns := spec.functions.filter (·.isInternal)
237+
let mappingHelpersRequired := usesMapping fields
238+
let arrayHelpersRequired := contractUsesArrayElement spec
239+
let fallbackSpec ← pickUniqueFunctionByName "fallback" spec.functions
240+
let receiveSpec ← pickUniqueFunctionByName "receive" spec.functions
235241
let functions ← (externalFns.zip selectors).mapM fun (fnSpec, sel) =>
236242
compileFunctionSpec fields spec.events spec.errors sel fnSpec
237243
let internalFuncDefs ← internalFns.mapM (compileInternalFunction fields spec.events spec.errors)
@@ -253,4 +259,8 @@ def compile (spec : CompilationModel) (selectors : List Nat) : Except String IRC
253259
internalFunctions := arrayElementHelpers ++ internalFuncDefs
254260
}
255261

262+
def compile (spec : CompilationModel) (selectors : List Nat) : Except String IRContract := do
263+
validateCompileInputs spec selectors
264+
compileValidatedCore spec selectors
265+
256266
end Compiler.CompilationModel

‎Compiler/CompilationModel/InternalNaming.lean‎

Lines changed: 81 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -9,18 +9,90 @@ def internalFunctionPrefix : String := "internal_"
99
def internalFunctionYulName (name : String) : String :=
1010
s!"{internalFunctionPrefix}{name}"
1111

12+
private def usedNamesTotalLength (usedNames : List String) : Nat :=
13+
usedNames.foldl (fun acc name => acc + name.length) 0 + 1
14+
15+
/-- Length budget large enough to make `freshSuffix usedNames` longer than any
16+
individual used name. -/
17+
private abbrev freshSuffixLen (usedNames : List String) : Nat :=
18+
usedNamesTotalLength usedNames
19+
20+
/-- Deterministic suffix whose length alone guarantees freshness against
21+
`usedNames`. -/
22+
private def freshSuffix (usedNames : List String) : String :=
23+
String.mk (List.replicate (freshSuffixLen usedNames) '_')
24+
1225
def pickFreshName (base : String) (usedNames : List String) : String :=
1326
if !usedNames.contains base then
1427
base
1528
else
16-
let rec go (suffix : Nat) (remaining : Nat) : String :=
17-
let candidate := s!"{base}_{suffix}"
18-
if !usedNames.contains candidate then
19-
candidate
20-
else
21-
match remaining with
22-
| 0 => s!"{base}_fresh"
23-
| n + 1 => go (suffix + 1) n
24-
go 1 usedNames.length
29+
base ++ "_" ++ freshSuffix usedNames
30+
31+
private theorem length_lt_usedNamesTotalLength_of_mem
32+
{usedNames : List String}
33+
{queryName : String}
34+
(hmem : queryName ∈ usedNames) :
35+
queryName.length < usedNamesTotalLength usedNames := by
36+
have hfold :
37+
∀ (acc : Nat) (names : List String),
38+
List.foldl (fun total name => total + name.length) acc names =
39+
acc + List.foldl (fun total name => total + name.length) 0 names := by
40+
intro acc names
41+
induction names generalizing acc with
42+
| nil =>
43+
simp [List.foldl]
44+
| cons head tail ih =>
45+
calc
46+
List.foldl (fun total name => total + name.length) (acc + String.length head) tail
47+
= acc + (String.length head + List.foldl (fun total name => total + name.length) 0 tail) := by
48+
simpa [Nat.add_assoc] using ih (acc := acc + String.length head)
49+
_ = acc + List.foldl (fun total name => total + name.length) (String.length head) tail := by
50+
rw [ih (acc := String.length head)]
51+
_ = acc + List.foldl (fun total name => total + name.length) 0 (head :: tail) := by
52+
simp [List.foldl]
53+
unfold usedNamesTotalLength
54+
induction usedNames with
55+
| nil =>
56+
cases hmem
57+
| cons head tail ih =>
58+
simp only [List.mem_cons] at hmem
59+
rcases hmem with rfl | hmem
60+
·
61+
have hsum :
62+
List.foldl (fun acc name => acc + name.length) 0 (queryName :: tail) =
63+
String.length queryName + List.foldl (fun acc name => acc + name.length) 0 tail := by
64+
simpa using hfold (String.length queryName) tail
65+
have hle : String.length queryName ≤
66+
String.length queryName + List.foldl (fun acc name => acc + name.length) 0 tail := by
67+
exact Nat.le_add_right _ _
68+
rw [hsum]
69+
omega
70+
·
71+
have ih' := ih hmem
72+
have hsum :
73+
List.foldl (fun acc name => acc + name.length) 0 (head :: tail) =
74+
String.length head + List.foldl (fun acc name => acc + name.length) 0 tail := by
75+
simpa using hfold (String.length head) tail
76+
rw [hsum]
77+
omega
78+
79+
theorem pickFreshName_not_mem_usedNames
80+
(base : String)
81+
(usedNames : List String) :
82+
pickFreshName base usedNames ∉ usedNames := by
83+
unfold pickFreshName
84+
by_cases hbase : base ∈ usedNames
85+
· intro hmem
86+
simp [hbase] at hmem
87+
have hlenUsed : (base ++ "_" ++ freshSuffix usedNames).length < freshSuffixLen usedNames := by
88+
simpa [freshSuffixLen] using
89+
(length_lt_usedNamesTotalLength_of_mem
90+
(usedNames := usedNames)
91+
(queryName := base ++ "_" ++ freshSuffix usedNames)
92+
hmem)
93+
have hlenFresh : freshSuffixLen usedNames ≤ (base ++ "_" ++ freshSuffix usedNames).length := by
94+
simp [freshSuffix, freshSuffixLen, usedNamesTotalLength]
95+
omega
96+
· simp [hbase]
2597

2698
end Compiler.CompilationModel

‎Compiler/CompilationModel/LayoutValidation.lean‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,96 @@ def firstDuplicateEventParamName
3939
| none => goEvents rest
4040
goEvents events
4141

42+
private theorem firstDuplicateName_go_eq_none_of_nodup
43+
(seen names : List String)
44+
(hseen : seen.Nodup)
45+
(hnames : names.Nodup)
46+
(hdisjoint : ∀ name, name ∈ names → name ∉ seen) :
47+
firstDuplicateName.go seen names = none := by
48+
induction names generalizing seen with
49+
| nil =>
50+
rfl
51+
| cons name rest ih =>
52+
simp only [List.nodup_cons] at hnames
53+
rcases hnames with ⟨hnameRest, hrest⟩
54+
have hnameSeen : name ∉ seen := hdisjoint name (by simp)
55+
have hseen' : (name :: seen).Nodup := List.nodup_cons.mpr ⟨hnameSeen, hseen⟩
56+
have hdisjoint' : ∀ next, next ∈ rest → next ∉ (name :: seen) := by
57+
intro next hnext
58+
have hnextSeen : next ∉ seen := hdisjoint next (by simp [hnext])
59+
have hnextNe : next ≠ name := by
60+
intro hEq
61+
subst hEq
62+
exact hnameRest hnext
63+
simp [hnextNe, hnextSeen]
64+
simp [firstDuplicateName.go, hnameSeen, ih (seen := name :: seen) hseen' hrest hdisjoint']
65+
66+
private theorem nodup_of_firstDuplicateName_go_eq_none
67+
(seen names : List String)
68+
(hseen : seen.Nodup)
69+
(hnone : firstDuplicateName.go seen names = none) :
70+
names.Nodup ∧ ∀ name, name ∈ names → name ∉ seen := by
71+
induction names generalizing seen with
72+
| nil =>
73+
simp
74+
| cons name rest ih =>
75+
simp only [firstDuplicateName.go] at hnone
76+
have hnameSeen : name ∉ seen := by
77+
intro hmem
78+
simp [hmem] at hnone
79+
have hseen' : (name :: seen).Nodup := List.nodup_cons.mpr ⟨hnameSeen, hseen⟩
80+
have hnoneRest : firstDuplicateName.go (name :: seen) rest = none := by
81+
simpa [hnameSeen] using hnone
82+
rcases ih (seen := name :: seen) hseen' hnoneRest with ⟨hrestNodup, hrestDisjoint⟩
83+
refine ⟨?_, ?_⟩
84+
· exact List.nodup_cons.mpr ⟨by
85+
intro hmem
86+
exact hrestDisjoint name hmem (by simp), hrestNodup⟩
87+
· intro next hmem
88+
simp at hmem
89+
rcases hmem with rfl | hrestMem
90+
· exact hnameSeen
91+
· exact fun hseenMem => hrestDisjoint next hrestMem (by simp [hseenMem])
92+
93+
theorem firstDuplicateName_eq_none_of_nodup
94+
(names : List String)
95+
(hnodup : names.Nodup) :
96+
firstDuplicateName names = none := by
97+
simpa [firstDuplicateName] using
98+
firstDuplicateName_go_eq_none_of_nodup [] names List.nodup_nil hnodup
99+
(by intro name hmem; simp)
100+
101+
theorem nodup_of_firstDuplicateName_eq_none
102+
(names : List String)
103+
(hnone : firstDuplicateName names = none) :
104+
names.Nodup := by
105+
simpa [firstDuplicateName] using
106+
(nodup_of_firstDuplicateName_go_eq_none [] names List.nodup_nil (by simpa [firstDuplicateName] using hnone)).1
107+
108+
theorem functionParamNames_nodup_of_firstDuplicateFunctionParamName_eq_none
109+
{fns : List FunctionSpec}
110+
{fn : FunctionSpec}
111+
(hnone : firstDuplicateFunctionParamName fns = none)
112+
(hfn : fn ∈ fns) :
113+
(fn.params.map (·.name)).Nodup := by
114+
unfold firstDuplicateFunctionParamName at hnone
115+
induction fns generalizing fn with
116+
| nil =>
117+
cases hfn
118+
| cons head tail ih =>
119+
simp only [firstDuplicateFunctionParamName.goFns] at hnone
120+
have hmem : fn = head ∨ fn ∈ tail := by
121+
simpa using hfn
122+
cases hdup : firstDuplicateName (head.params.map (·.name)) with
123+
| some dup =>
124+
simp [hdup] at hnone
125+
| none =>
126+
have htailNone : firstDuplicateFunctionParamName.goFns tail = none := by
127+
simpa [hdup] using hnone
128+
rcases hmem with rfl | htail
129+
· exact nodup_of_firstDuplicateName_eq_none _ hdup
130+
· exact ih htailNone htail
131+
42132
def dedupNatPreserve (xs : List Nat) : List Nat :=
43133
let rec go (seen : List Nat) : List Nat → List Nat
44134
| [] => []

‎Compiler/CompilationModel/ParamLoading.lean‎

Lines changed: 20 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ private def genDynamicParamLoads
6969
[offsetLoad, offsetBoundsCheck, absoluteOffsetLoad, absoluteBoundsCheck, lengthLoad, tailHeadEndLoad, tailRemainingLoad]
7070
++ lengthBoundsCheck ++ [dataOffsetLoad]
7171

72-
private def genScalarLoad
72+
def genScalarLoad
7373
(loadWord : YulExpr → YulExpr) (name : String) (ty : ParamType) (offset : Nat) :
7474
List YulStmt :=
7575
let load := loadWord (YulExpr.lit offset)
@@ -122,19 +122,13 @@ private partial def genStaticTypeLoads
122122
go elemTys 0 offset
123123
| _ => []
124124

125-
private def genParamLoadsFrom
125+
def genParamLoadBodyFrom
126126
(loadWord : YulExpr → YulExpr) (sizeExpr : YulExpr)
127-
(headStart : Nat) (baseOffset : Nat) (params : List Param) :
127+
(headSize : Nat) (baseOffset : Nat) (params : List Param) (headOffset : Nat) :
128128
List YulStmt :=
129-
let headSize := (params.map (fun p => paramHeadSize p.ty)).foldl (· + ·) 0
130-
let minInputSizeCheck :=
131-
YulStmt.if_ (YulExpr.call "lt" [sizeExpr, YulExpr.lit (baseOffset + headSize)]) [
132-
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
133-
]
134-
let rec go (paramList : List Param) (headOffset : Nat) : List YulStmt :=
135-
match paramList with
136-
| [] => []
137-
| param :: rest =>
129+
match params with
130+
| [] => []
131+
| param :: rest =>
138132
let stmts := match param.ty with
139133
| ParamType.uint256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
140134
genScalarLoad loadWord param.name param.ty headOffset
@@ -163,8 +157,20 @@ private def genParamLoadsFrom
163157
staticLoads ++ firstAlias
164158
| ParamType.bytes | ParamType.string =>
165159
genDynamicParamLoads loadWord sizeExpr headSize baseOffset param.name param.ty headOffset
166-
stmts ++ go rest (headOffset + paramHeadSize param.ty)
167-
minInputSizeCheck :: go params headStart
160+
stmts ++
161+
genParamLoadBodyFrom loadWord sizeExpr headSize baseOffset rest
162+
(headOffset + paramHeadSize param.ty)
163+
164+
def genParamLoadsFrom
165+
(loadWord : YulExpr → YulExpr) (sizeExpr : YulExpr)
166+
(headStart : Nat) (baseOffset : Nat) (params : List Param) :
167+
List YulStmt :=
168+
let headSize := (params.map (fun p => paramHeadSize p.ty)).foldl (· + ·) 0
169+
let minInputSizeCheck :=
170+
YulStmt.if_ (YulExpr.call "lt" [sizeExpr, YulExpr.lit (baseOffset + headSize)]) [
171+
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
172+
]
173+
minInputSizeCheck :: genParamLoadBodyFrom loadWord sizeExpr headSize baseOffset params headStart
168174

169175
def genParamLoads (params : List Param) : List YulStmt :=
170176
genParamLoadsFrom (fun pos => YulExpr.call "calldataload" [pos]) (YulExpr.call "calldatasize" []) 4 4 params

0 commit comments

Comments
 (0)