From ecd2dc430e90a251305f67a8fad8a2620ca96087 Mon Sep 17 00:00:00 2001 From: Thomas Marchand Date: Fri, 12 Jun 2026 22:33:05 +0200 Subject: [PATCH 1/2] Support packed struct member writes --- Compiler/CompilationModelFeatureTest.lean | 44 +++++++++++++ .../Proofs/IRGeneration/DenoteAgreement.lean | 6 ++ .../Proofs/IRGeneration/SourceSemantics.lean | 64 +++++++++++++++++++ PrintAxioms.lean | 3 +- Verity/Core/Model/Denote.lean | 30 +++++++++ 5 files changed, 146 insertions(+), 1 deletion(-) diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean index ef0c0bffb..ed7a213b0 100644 --- a/Compiler/CompilationModelFeatureTest.lean +++ b/Compiler/CompilationModelFeatureTest.lean @@ -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 @@ -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 := diff --git a/Compiler/Proofs/IRGeneration/DenoteAgreement.lean b/Compiler/Proofs/IRGeneration/DenoteAgreement.lean index 0d47431ec..8310ca950 100644 --- a/Compiler/Proofs/IRGeneration/DenoteAgreement.lean +++ b/Compiler/Proofs/IRGeneration/DenoteAgreement.lean @@ -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 = diff --git a/Compiler/Proofs/IRGeneration/SourceSemantics.lean b/Compiler/Proofs/IRGeneration/SourceSemantics.lean index 13ab10572..dcf4f1a0d 100644 --- a/Compiler/Proofs/IRGeneration/SourceSemantics.lean +++ b/Compiler/Proofs/IRGeneration/SourceSemantics.lean @@ -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 := @@ -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 => @@ -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 => @@ -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 => @@ -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 => @@ -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 => @@ -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 => diff --git a/PrintAxioms.lean b/PrintAxioms.lean index d9ed9e5db..4b4a6421e 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -1743,6 +1743,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 @@ -5542,4 +5543,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 5187 theorems/lemmas (3588 public, 1599 private, 0 sorry'd) +-- Total: 5188 theorems/lemmas (3589 public, 1599 private, 0 sorry'd) diff --git a/Verity/Core/Model/Denote.lean b/Verity/Core/Model/Denote.lean index cc445c0a2..bb0058e12 100644 --- a/Verity/Core/Model/Denote.lean +++ b/Verity/Core/Model/Denote.lean @@ -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 @@ -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 => @@ -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 => From 8d91aa948629b2716b0ce472db183f4914ed0e92 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Tue, 16 Jun 2026 09:16:01 +0100 Subject: [PATCH 2/2] chore: auto-refresh derived artifacts --- PrintAxioms.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PrintAxioms.lean b/PrintAxioms.lean index 89a857256..07209d3de 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -5567,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)