Skip to content

Commit 8a4182c

Browse files
Th0rgalgithub-actions[bot]
Th0rgal
and
github-actions[bot]
authored
Transient storage fields (#1995) (#2021)
* Add transient storage fields * fix(verity): route transient mapping writes through tstore (#2021) * mask transient address-field writes to match Yul (#1995) * fix(2021): repair transient-storage proofs for task/1995 * fix(2021): repair transient-storage proofs for task/1995 * chore: auto-refresh derived artifacts * fix(2021): complete transient-storage forward-port + registry/lint Recover field-aware frame lemmas left unstaged in the prior merge commit: - Frames.lean: writeUint/AddressFieldSlots_preserves_{storage,address,arrays, calldata} + rewire execStmt_setStorage/setStorageAddr_execution_summary to the field-aware (transient-capable) writers. - DenoteAgreement.lean: writeAddressKeyedMapping2PackedWordFieldSlots_eq. - ExpressionCompile.lean: use the outer resolved field binding for the tload/sload selection (drop redundant re-match); adapt compileExpr_bridgedSource closure proofs accordingly. Regenerate PrintAxioms.lean (5316 thms, 0 sorry'd). Allowlist the long add-wrapped multi-slot bridging closure compileMappingSlotWrite_multiSlot_nonzero_bridged (twin of the already-allowlisted compileMappingSlotWrite_multiSlot_bridged). make check: All checks passed. --------- Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
1 parent 40443e7 commit 8a4182c

23 files changed

Lines changed: 3330 additions & 1580 deletions

File tree

‎Compiler/CompilationModel/Compile.lean‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -169,19 +169,20 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
169169
| Stmt.setStorageWord field wordOffset value =>
170170
match findFieldWithResolvedSlot fields field with
171171
| some (f, slot) => do
172+
let storeBuiltin := if f.isTransient then "tstore" else "sstore"
172173
let valueExpr ← compileExprWithInternals fields dynamicSource internalFunctions value
173174
let slotExpr (baseSlot : Nat) :=
174175
if wordOffset == 0 then YulExpr.lit baseSlot
175176
else YulExpr.call "add" [YulExpr.lit baseSlot, YulExpr.lit wordOffset]
176177
match f.aliasSlots with
177178
| [] =>
178-
pure [YulStmt.expr (YulExpr.call "sstore" [slotExpr slot, valueExpr])]
179+
pure [YulStmt.expr (YulExpr.call storeBuiltin [slotExpr slot, valueExpr])]
179180
| _ =>
180181
pure [
181182
YulStmt.block (
182183
[YulStmt.let_ "__compat_value" valueExpr] ++
183184
(slot :: f.aliasSlots).map (fun writeSlot =>
184-
YulStmt.expr (YulExpr.call "sstore" [
185+
YulStmt.expr (YulExpr.call storeBuiltin [
185186
slotExpr writeSlot,
186187
YulExpr.ident "__compat_value"
187188
]))
@@ -200,19 +201,23 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
200201
(← compileExprWithInternals fields dynamicSource internalFunctions key)
201202
(← compileExprWithInternals fields dynamicSource internalFunctions value)
202203
"setMapping"
204+
0
205+
true
203206
| Stmt.setMappingWord field key wordOffset value => do
204207
compileMappingSlotWrite fields field
205208
(← compileExprWithInternals fields dynamicSource internalFunctions key)
206209
(← compileExprWithInternals fields dynamicSource internalFunctions value)
207210
"setMappingWord"
208211
wordOffset
212+
true
209213
| Stmt.setMappingPackedWord field key wordOffset packed value => do
210214
compileMappingPackedSlotWrite fields field
211215
(← compileExprWithInternals fields dynamicSource internalFunctions key)
212216
(← compileExprWithInternals fields dynamicSource internalFunctions value)
213217
wordOffset
214218
packed
215219
"setMappingPackedWord"
220+
true
216221
| Stmt.setMapping2 field key1 key2 value =>
217222
compileSetMapping2 fields dynamicSource field key1 key2 value internalFunctions
218223
| Stmt.setMapping2Word field key1 key2 wordOffset value =>
@@ -222,6 +227,8 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
222227
(← compileExprWithInternals fields dynamicSource internalFunctions key)
223228
(← compileExprWithInternals fields dynamicSource internalFunctions value)
224229
"setMappingUint"
230+
0
231+
true
225232
| Stmt.setMappingChain field keys value =>
226233
compileSetMappingChain fields dynamicSource field keys value internalFunctions
227234
| Stmt.setStructMember field key memberName value =>

‎Compiler/CompilationModel/ExpressionCompile.lean‎

Lines changed: 27 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -28,11 +28,12 @@ def compileMappingSlotRead (fields : List Field) (field : String) (keyExpr : Yul
2828
if !isMapping fields field then
2929
throw s!"Compilation error: field '{field}' is not a mapping"
3030
else
31-
match findFieldSlot fields field with
32-
| some slot =>
31+
match findFieldWithResolvedSlot fields field with
32+
| some (f, slot) =>
3333
let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, keyExpr]
3434
let finalSlot := if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
35-
pure (YulExpr.call "sload" [finalSlot])
35+
let loadBuiltin := if f.isTransient then "tload" else "sload"
36+
pure (YulExpr.call loadBuiltin [finalSlot])
3637
| none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"
3738

3839
-- Exposed so proof modules can name the exact nested mapping-chain lowering shape.
@@ -191,12 +192,13 @@ def compileExprWithInternals (fields : List Field)
191192
else
192193
match findFieldWithResolvedSlot fields field with
193194
| some (f, slot) =>
195+
let loadBuiltin := if f.isTransient then "tload" else "sload"
194196
match f.packedBits with
195197
| none =>
196-
pure (YulExpr.call "sload" [YulExpr.lit slot])
198+
pure (YulExpr.call loadBuiltin [YulExpr.lit slot])
197199
| some packed =>
198200
pure (YulExpr.call "and" [
199-
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call "sload" [YulExpr.lit slot]],
201+
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call loadBuiltin [YulExpr.lit slot]],
200202
YulExpr.lit (packedMaskNat packed)
201203
])
202204
| none => throw s!"Compilation error: unknown storage field '{field}'"
@@ -206,14 +208,15 @@ def compileExprWithInternals (fields : List Field)
206208
else
207209
match findFieldWithResolvedSlot fields field with
208210
| some (f, slot) =>
211+
let loadBuiltin := if f.isTransient then "tload" else "sload"
209212
match f.ty with
210213
| .address =>
211214
match f.packedBits with
212215
| none =>
213-
pure (YulExpr.call "sload" [YulExpr.lit slot])
216+
pure (YulExpr.call loadBuiltin [YulExpr.lit slot])
214217
| some packed =>
215218
pure (YulExpr.call "and" [
216-
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call "sload" [YulExpr.lit slot]],
219+
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call loadBuiltin [YulExpr.lit slot]],
217220
YulExpr.lit (packedMaskNat packed)
218221
])
219222
| _ =>
@@ -236,36 +239,39 @@ def compileExprWithInternals (fields : List Field)
236239
if !isMapping2 fields field then
237240
throw s!"Compilation error: field '{field}' is not a double mapping"
238241
else
239-
match findFieldSlot fields field with
240-
| some slot => do
242+
match findFieldWithResolvedSlot fields field with
243+
| some (f, slot) => do
244+
let loadBuiltin := if f.isTransient then "tload" else "sload"
241245
let key1Expr ← compileExprWithInternals fields dynamicSource internalFunctions key1
242246
let key2Expr ← compileExprWithInternals fields dynamicSource internalFunctions key2
243247
let innerSlot := YulExpr.call "mappingSlot" [YulExpr.lit slot, key1Expr]
244-
pure (YulExpr.call "sload" [YulExpr.call "mappingSlot" [innerSlot, key2Expr]])
248+
pure (YulExpr.call loadBuiltin [YulExpr.call "mappingSlot" [innerSlot, key2Expr]])
245249
| none => throw s!"Compilation error: unknown mapping field '{field}'"
246250
| Expr.mapping2Word field key1 key2 wordOffset =>
247251
if !isMapping2 fields field then
248252
throw s!"Compilation error: field '{field}' is not a double mapping"
249253
else
250-
match findFieldSlot fields field with
251-
| some slot => do
254+
match findFieldWithResolvedSlot fields field with
255+
| some (f, slot) => do
256+
let loadBuiltin := if f.isTransient then "tload" else "sload"
252257
let key1Expr ← compileExprWithInternals fields dynamicSource internalFunctions key1
253258
let key2Expr ← compileExprWithInternals fields dynamicSource internalFunctions key2
254259
let innerSlot := YulExpr.call "mappingSlot" [YulExpr.lit slot, key1Expr]
255260
let outerSlot := YulExpr.call "mappingSlot" [innerSlot, key2Expr]
256261
let finalSlot := if wordOffset == 0 then outerSlot else YulExpr.call "add" [outerSlot, YulExpr.lit wordOffset]
257-
pure (YulExpr.call "sload" [finalSlot])
262+
pure (YulExpr.call loadBuiltin [finalSlot])
258263
| none => throw s!"Compilation error: unknown mapping field '{field}'"
259264
| Expr.mappingUint field key => do
260265
compileMappingSlotRead fields field (← compileExprWithInternals fields dynamicSource internalFunctions key) "mappingUint"
261266
| Expr.mappingChain field keys =>
262267
if !isMapping fields field then
263268
throw s!"Compilation error: field '{field}' is not a mapping"
264269
else
265-
match findFieldSlot fields field with
266-
| some slot => do
270+
match findFieldWithResolvedSlot fields field with
271+
| some (f, slot) => do
267272
let keyExprs ← compileExprListWithInternals fields dynamicSource internalFunctions keys
268-
pure (YulExpr.call "sload" [compileMappingSlotChain (YulExpr.lit slot) keyExprs])
273+
let loadBuiltin := if f.isTransient then "tload" else "sload"
274+
pure (YulExpr.call loadBuiltin [compileMappingSlotChain (YulExpr.lit slot) keyExprs])
269275
| none => throw s!"Compilation error: unknown mapping field '{field}'"
270276
| Expr.structMember field key memberName => do
271277
if isMapping2 fields field then
@@ -295,19 +301,20 @@ def compileExprWithInternals (fields : List Field)
295301
match findStructMember members memberName with
296302
| none => throw s!"Compilation error: struct field '{field}' has no member '{memberName}'"
297303
| some member =>
298-
match findFieldSlot fields field with
299-
| some slot => do
304+
match findFieldWithResolvedSlot fields field with
305+
| some (f, slot) => do
306+
let loadBuiltin := if f.isTransient then "tload" else "sload"
300307
let key1Expr ← compileExprWithInternals fields dynamicSource internalFunctions key1
301308
let key2Expr ← compileExprWithInternals fields dynamicSource internalFunctions key2
302309
let innerSlot := YulExpr.call "mappingSlot" [YulExpr.lit slot, key1Expr]
303310
let outerSlot := YulExpr.call "mappingSlot" [innerSlot, key2Expr]
304311
let finalSlot := if member.wordOffset == 0 then outerSlot else YulExpr.call "add" [outerSlot, YulExpr.lit member.wordOffset]
305312
match member.packed with
306313
| none =>
307-
pure (YulExpr.call "sload" [finalSlot])
314+
pure (YulExpr.call loadBuiltin [finalSlot])
308315
| some packed =>
309316
pure (YulExpr.call "and" [
310-
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call "sload" [finalSlot]],
317+
YulExpr.call "shr" [YulExpr.lit packed.offset, YulExpr.call loadBuiltin [finalSlot]],
311318
YulExpr.lit (packedMaskNat packed)
312319
])
313320
| none => throw s!"Compilation error: unknown mapping field '{field}'"

‎Compiler/CompilationModel/MappingWrites.lean‎

Lines changed: 63 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -7,48 +7,81 @@ open Compiler
77
open Compiler.Yul
88

99
def compileMappingSlotWrite (fields : List Field) (field : String)
10-
(keyExpr valueExpr : YulExpr) (label : String) (wordOffset : Nat := 0) : Except String (List YulStmt) :=
10+
(keyExpr valueExpr : YulExpr) (label : String) (wordOffset : Nat := 0)
11+
(allowTransient : Bool := false) : Except String (List YulStmt) :=
1112
if !isMapping fields field then
1213
throw s!"Compilation error: field '{field}' is not a mapping"
1314
else
15+
let storeBuiltin :=
16+
if allowTransient then
17+
match findFieldWithResolvedSlot fields field with
18+
| some (f, _) => if f.isTransient then "tstore" else "sstore"
19+
| none => "sstore"
20+
else
21+
"sstore"
1422
match findFieldWriteSlots fields field with
1523
| some slots =>
1624
match slots with
17-
| [] =>
18-
throw s!"Compilation error: internal invariant failure: no write slots for mapping field '{field}' in {label}"
19-
| [slot] =>
20-
let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, keyExpr]
21-
let writeSlot := if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
22-
pure [
23-
YulStmt.expr (YulExpr.call "sstore" [
24-
writeSlot,
25-
valueExpr
26-
])
27-
]
28-
| _ =>
29-
let compatSlotExpr := fun (slot : Nat) =>
30-
let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, YulExpr.ident "__compat_key"]
31-
if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
32-
pure [
33-
YulStmt.block (
34-
[YulStmt.let_ "__compat_key" keyExpr, YulStmt.let_ "__compat_value" valueExpr] ++
35-
slots.map (fun slot =>
25+
| [] =>
26+
throw s!"Compilation error: internal invariant failure: no write slots for mapping field '{field}' in {label}"
27+
| [slot] =>
28+
let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, keyExpr]
29+
let writeSlot := if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
30+
if allowTransient then
31+
match findFieldWithResolvedSlot fields field with
32+
| some (_, _) =>
33+
pure [
34+
YulStmt.expr (YulExpr.call storeBuiltin [
35+
writeSlot,
36+
valueExpr
37+
])
38+
]
39+
| none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"
40+
else
41+
pure [
3642
YulStmt.expr (YulExpr.call "sstore" [
37-
compatSlotExpr slot,
38-
YulExpr.ident "__compat_value"
39-
]))
40-
)
41-
]
43+
writeSlot,
44+
valueExpr
45+
])
46+
]
47+
| _ =>
48+
let compatSlotExpr := fun (slot : Nat) =>
49+
let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, YulExpr.ident "__compat_key"]
50+
if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
51+
pure [
52+
YulStmt.block (
53+
[YulStmt.let_ "__compat_key" keyExpr, YulStmt.let_ "__compat_value" valueExpr] ++
54+
slots.map (fun slot =>
55+
YulStmt.expr (YulExpr.call storeBuiltin [
56+
compatSlotExpr slot,
57+
YulExpr.ident "__compat_value"
58+
]))
59+
)
60+
]
4261
| none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"
4362

4463
def compileMappingPackedSlotWrite (fields : List Field) (field : String)
4564
(keyExpr valueExpr : YulExpr) (wordOffset : Nat) (packed : PackedBits)
46-
(label : String) : Except String (List YulStmt) :=
65+
(label : String) (allowTransient : Bool := false) : Except String (List YulStmt) :=
4766
if !isMapping fields field then
4867
throw s!"Compilation error: field '{field}' is not a mapping"
4968
else if !packedBitsValid packed then
5069
throw s!"Compilation error: {label} for field '{field}' has invalid packed range offset={packed.offset} width={packed.width}. Require 0 < width <= 256, offset < 256, and offset + width <= 256."
5170
else
71+
let loadBuiltin :=
72+
if allowTransient then
73+
match findFieldWithResolvedSlot fields field with
74+
| some (f, _) => if f.isTransient then "tload" else "sload"
75+
| none => "sload"
76+
else
77+
"sload"
78+
let storeBuiltin :=
79+
if allowTransient then
80+
match findFieldWithResolvedSlot fields field with
81+
| some (f, _) => if f.isTransient then "tstore" else "sstore"
82+
| none => "sstore"
83+
else
84+
"sstore"
5285
match findFieldWriteSlots fields field with
5386
| some slots =>
5487
match slots with
@@ -63,12 +96,12 @@ def compileMappingPackedSlotWrite (fields : List Field) (field : String)
6396
YulStmt.block [
6497
YulStmt.let_ "__compat_value" valueExpr,
6598
YulStmt.let_ "__compat_packed" (YulExpr.call "and" [YulExpr.ident "__compat_value", YulExpr.lit maskNat]),
66-
YulStmt.let_ "__compat_slot_word" (YulExpr.call "sload" [writeSlot]),
99+
YulStmt.let_ "__compat_slot_word" (YulExpr.call loadBuiltin [writeSlot]),
67100
YulStmt.let_ "__compat_slot_cleared" (YulExpr.call "and" [
68101
YulExpr.ident "__compat_slot_word",
69102
YulExpr.call "not" [YulExpr.lit shiftedMaskNat]
70103
]),
71-
YulStmt.expr (YulExpr.call "sstore" [
104+
YulStmt.expr (YulExpr.call storeBuiltin [
72105
writeSlot,
73106
YulExpr.call "or" [
74107
YulExpr.ident "__compat_slot_cleared",
@@ -90,12 +123,12 @@ def compileMappingPackedSlotWrite (fields : List Field) (field : String)
90123
YulStmt.let_ "__compat_packed" (YulExpr.call "and" [YulExpr.ident "__compat_value", YulExpr.lit maskNat])] ++
91124
slots.map (fun slot =>
92125
YulStmt.block [
93-
YulStmt.let_ "__compat_slot_word" (YulExpr.call "sload" [slotExpr slot]),
126+
YulStmt.let_ "__compat_slot_word" (YulExpr.call loadBuiltin [slotExpr slot]),
94127
YulStmt.let_ "__compat_slot_cleared" (YulExpr.call "and" [
95128
YulExpr.ident "__compat_slot_word",
96129
YulExpr.call "not" [YulExpr.lit shiftedMaskNat]
97130
]),
98-
YulStmt.expr (YulExpr.call "sstore" [
131+
YulStmt.expr (YulExpr.call storeBuiltin [
99132
slotExpr slot,
100133
YulExpr.call "or" [
101134
YulExpr.ident "__compat_slot_cleared",

0 commit comments

Comments
 (0)