Skip to content

Bitfield-packed struct storage writes in mappings (#1976) #2011

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Th0rgal wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Bitfield-packed struct storage writes in mappings (#1976) #2011

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
ecd2dc4
Support packed struct member writes
Th0rgal Jun 12, 2026
139787b
Merge remote-tracking branch 'origin/main' into task/1976-packed-arrays
Th0rgal Jun 13, 2026
2b3223e
Merge remote-tracking branch 'origin/main' into wt-2011-fix
Th0rgal Jun 16, 2026
8d91aa9
chore: auto-refresh derived artifacts
github-actions[bot] Jun 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 44 additions & 0 deletions Compiler/CompilationModelFeatureTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ import Contracts.ProxyUpgradeabilityMacroSmoke
import Contracts.Smoke
import Contracts.StringArrayErrorSmoke
import Contracts.StringArrayEventSmoke
import Verity.Core.Model.Denote
import Verity.Macro.Translate

-- The `unnecessarySeqFocus` linter recurses through every tactic block in the
Expand Down Expand Up @@ -5196,6 +5197,49 @@ example : routerStructMembersDestructuringKeepsMemberTypes = true := by native_d

end MacroSolidityTypeFidelitySmoke

namespace PackedStructMemberDenoteSmoke

private def oracle : Denote.DenoteOracle :=
{ mappingSlot := fun base key => base * 1000 + key
keccakMemorySlice := fun _ _ _ => 0 }

private def fields : List Field :=
[{ name := "deposits",
ty := FieldType.mappingStruct MappingKeyType.address
[{ name := "deposit", wordOffset := 0, packed := none },
{ name := "staked", ty := .bool, wordOffset := 1,
packed := some { offset := 0, width := 1 } },
{ name := "stake", wordOffset := 1,
packed := some { offset := 1, width := 112 } },
{ name := "unstakeDelaySec", ty := .uint256, wordOffset := 1,
packed := some { offset := 113, width := 32 } },
{ name := "withdrawTime", wordOffset := 1,
packed := some { offset := 145, width := 48 } }],
«slot» := some 1 }]

private def key : Nat := 7
private def packedSlot : Nat := oracle.mappingSlot 1 key + 1
private def oldWord : Nat := 1 + 5 * 2 ^ 1 + 9 * 2 ^ 113
private def expectedWord : Nat := 1 + 7 * 2 ^ 1 + 9 * 2 ^ 113

private def preservesAdjacentPackedFields : Bool :=
let world : Verity.ContractState :=
{ Verity.defaultState with
«storage» := fun s => if s == packedSlot then oldWord else 0 }
let state : Denote.DenoteState := { world := world, bindings := [] }
match Denote.execStmt oracle fields state
(Stmt.setStructMember "deposits" (.literal key) "stake" (.literal 7)) with
| .continue next =>
(next.world.storage packedSlot).val == expectedWord
| _ => false

#eval! do
expectTrue
"packed mapping struct writes preserve adjacent fields in the same word"
preservesAdjacentPackedFields

end PackedStructMemberDenoteSmoke

set_option maxRecDepth 4096 in
#eval! do
let compiled :=
Expand Down
6 changes: 6 additions & 0 deletions Compiler/Proofs/IRGeneration/DenoteAgreement.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -291,6 +291,12 @@ theorem writeAddressKeyedMapping2Slots_eq
Denote.writeAddressKeyedMapping2WordSlots sourceOracle w slots k1 k2 off v =
SourceSemantics.writeAddressKeyedMapping2WordSlots w slots k1 k2 off v := rfl

@[simp] theorem writeAddressKeyedMapping2PackedWordSlots_eq
(w : Verity.ContractState) (slots : List Nat) (k1 k2 off : Nat)
(p : PackedBits) (v : Nat) :
Denote.writeAddressKeyedMapping2PackedWordSlots sourceOracle w slots k1 k2 off p v =
SourceSemantics.writeAddressKeyedMapping2PackedWordSlots w slots k1 k2 off p v := rfl

@[simp] theorem writeAddressKeyedMappingChainSlots_eq
(w : Verity.ContractState) (slots keys : List Nat) (v : Nat) :
Denote.writeAddressKeyedMappingChainSlots sourceOracle w slots keys v =
Expand Down
64 changes: 64 additions & 0 deletions Compiler/Proofs/IRGeneration/SourceSemantics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -472,6 +472,22 @@ def writeAddressKeyedMappingPackedWordSlots
else
world.storage slot }

def writeAddressKeyedMapping2PackedWordSlots
(world : Verity.ContractState) (slots : List Nat) (key1 key2 wordOffset : Nat)
(packed : PackedBits) (value : Nat) :
Verity.ContractState :=
let targets :=
slots.map (fun slot =>
wordNormalize
(Compiler.Proofs.abstractMappingSlot
(Compiler.Proofs.abstractMappingSlot slot key1) key2 + wordOffset))
{ world with
storage := fun slot =>
if targets.contains slot then
packedWordWrite (world.storage slot).val value packed
else
world.storage slot }

def writeUintKeyedMappingSlots
(world : Verity.ContractState) (slots : List Nat) (key value : Nat) :
Verity.ContractState :=
Expand Down Expand Up @@ -1950,6 +1966,14 @@ mutual
{ state with
world := writeAddressKeyedMappingWordSlots
state.world slots resolvedKey wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMappingPackedWordSlots
state.world slots resolvedKey wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _ => .revert
| state, .setMapping2 fieldName key1 key2 value =>
Expand Down Expand Up @@ -1998,6 +2022,14 @@ mutual
{ state with
world := writeAddressKeyedMapping2WordSlots
state.world slots resolvedKey1 resolvedKey2 wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMapping2PackedWordSlots
state.world slots resolvedKey1 resolvedKey2 wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _, _ => .revert
| state, .setMappingUint fieldName key value =>
Expand Down Expand Up @@ -2194,6 +2226,14 @@ mutual
{ state with
world := writeAddressKeyedMappingWordSlots
state.world slots resolvedKey wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMappingPackedWordSlots
state.world slots resolvedKey wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _ => .revert
| state, .setMapping2 fieldName key1 key2 value =>
Expand Down Expand Up @@ -2242,6 +2282,14 @@ mutual
{ state with
world := writeAddressKeyedMapping2WordSlots
state.world slots resolvedKey1 resolvedKey2 wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMapping2PackedWordSlots
state.world slots resolvedKey1 resolvedKey2 wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _, _ => .revert
| state, .setMappingUint fieldName key value =>
Expand Down Expand Up @@ -3231,6 +3279,14 @@ mutual
{ state with
world := writeAddressKeyedMappingWordSlots
state.world slots resolvedKey wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMappingPackedWordSlots
state.world slots resolvedKey wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _ => .revert
| .setMapping2 fieldName key1 key2 value =>
Expand Down Expand Up @@ -3279,6 +3335,14 @@ mutual
{ state with
world := writeAddressKeyedMapping2WordSlots
state.world slots resolvedKey1 resolvedKey2 wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMapping2PackedWordSlots
state.world slots resolvedKey1 resolvedKey2 wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _, _ => .revert
| .setMappingUint fieldName key value =>
Expand Down
3 changes: 2 additions & 1 deletion PrintAxioms.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1761,6 +1761,7 @@ end Verity.AxiomAudit
Compiler.Proofs.IRGeneration.DenoteAgreement.writeAddressKeyedMappingWordSlots_eq
Compiler.Proofs.IRGeneration.DenoteAgreement.writeAddressKeyedMappingPackedWordSlots_eq
Compiler.Proofs.IRGeneration.DenoteAgreement.writeAddressKeyedMapping2WordSlots_eq
Compiler.Proofs.IRGeneration.DenoteAgreement.writeAddressKeyedMapping2PackedWordSlots_eq
Compiler.Proofs.IRGeneration.DenoteAgreement.writeAddressKeyedMappingChainSlots_eq
Compiler.Proofs.IRGeneration.DenoteAgreement.writeStorageArray_eq
Compiler.Proofs.IRGeneration.DenoteAgreement.packedBitsValid_eq
Expand Down Expand Up @@ -5566,4 +5567,4 @@ end Verity.AxiomAudit
Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
]

-- Total: 5202 theorems/lemmas (3596 public, 1606 private, 0 sorry'd)
-- Total: 5209 theorems/lemmas (3603 public, 1606 private, 0 sorry'd)
30 changes: 30 additions & 0 deletions Verity/Core/Model/Denote.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -410,6 +410,20 @@ def writeAddressKeyedMapping2WordSlots (oracle : DenoteOracle)
storage := fun slot =>
if targets.contains slot then word else world.storage slot }

def writeAddressKeyedMapping2PackedWordSlots (oracle : DenoteOracle)
(world : Verity.ContractState) (slots : List Nat) (key1 key2 wordOffset : Nat)
(packed : PackedBits) (value : Nat) :
Verity.ContractState :=
let targets := slots.map (fun slot =>
wordNormalize
(oracle.mappingSlot (oracle.mappingSlot slot key1) key2 + wordOffset))
{ world with
storage := fun slot =>
if targets.contains slot then
packedWordWrite (world.storage slot).val value packed
else
world.storage slot }

def storageArraySetAt :
List Verity.Core.Uint256 → Nat → Verity.Core.Uint256 → Option (List Verity.Core.Uint256)
| [], _, _ => none
Expand Down Expand Up @@ -833,6 +847,14 @@ mutual
{ state with
world := writeAddressKeyedMappingWordSlots oracle
state.world slots resolvedKey wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMappingPackedWordSlots oracle
state.world slots resolvedKey wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _ => .revert
| state, .setMapping2 fieldName key1 key2 value =>
Expand Down Expand Up @@ -881,6 +903,14 @@ mutual
{ state with
world := writeAddressKeyedMapping2WordSlots oracle
state.world slots resolvedKey1 resolvedKey2 wordOffset resolved }
| some { wordOffset := wordOffset, packed := some packed, .. } =>
if packedBitsValid packed then
.continue
{ state with
world := writeAddressKeyedMapping2PackedWordSlots oracle
state.world slots resolvedKey1 resolvedKey2 wordOffset packed resolved }
else
.revert
| _ => .revert
| _, _, _, _, _ => .revert
| state, .setMappingUint fieldName key value =>
Expand Down