From 7007b4cbdaa5b63592727676108f333c5ae5bd3d Mon Sep 17 00:00:00 2001 From: Thomas Marchand Date: Mon, 28 Sep 2026 22:57:45 +0200 Subject: [PATCH] feat(edsl): symbolic mapChain channel for hashed nested/struct mappings (G2 residual) #2432 stored nested-mapping, word-offset mapping and struct-mapping words in the flat `.slot` channel at the Solidity keccak slot. That made key-vs-key separation depend on `solidityMappingSlot_injective`, and it left mapping-vs-scalar separation (e.g. `requests[user][epoch]` vs slot 206) unprovable. These words now live on dedicated constructor-keyed channels: * `StorageKey.mapChain slot keys offset` (`ContractState.readMapChain` / `writeMapChain`, view `storageMapChain`), used by getMappingN/setMappingN, getMappingWord/setMappingWord, structMemberAt/structMember2At, setStructMemberAt/setStructMember2At and `structMembers` destructuring; * `StorageKey.transientMapChain slot keys` (`readTransientMapChain` / `writeTransientMapChain`, view `transientStorageMapChain`), used by getTransientMappingN/setTransientMappingN. The import harness' `beginTransaction` clears it. Both are plain non-slot keys, so hops namespace them per contract through `StorageKey.scoped`, and `Contract.run` rollback restores them. Lens laws: readMapChain_writeMapChain(_same/_of_ne/_keys_ne/_offset_ne/_slot_ne), independence from `.slot`, addr, map*, transient and arrays, context-field frames, and the hop lemmas (enterHop_/exitHop_readMapChain, readMapChain_exitHop_enterHop_of_frame). The Solidity layout is now an interpretation. `mappingChainSlotLocation` lives in MappingSlot, and Storage/HashedMappingLayout relates the channel to the flat `.slot` channel (`HashedCoherentOn`, preserved by aligned writes under a finite `LayoutNonAlias` certificate). No axiom is involved. The smoke proves key, member, mapping-vs-scalar and hop separation, using only propext / Classical.choice / Quot.sound. Closes #2456 Co-Authored-By: Claude Opus 5.5 --- Compiler/Proofs/MappingSlot.lean | 37 ++ .../Proofs/Storage/HashedMappingLayout.lean | 183 ++++++++ Compiler/Proofs/Storage/MappingCoherence.lean | 10 + .../Storage/MappingCoherentAllKeys.lean | 18 + Compiler/SolidityImport/Transactions.lean | 1 + Compiler/TypedIRCompilerCorrectness.lean | 2 + Contracts/Common.lean | 219 +++++++--- .../OwnedCounter/Proofs/StorageCoherence.lean | 2 + Contracts/Smoke/HashedMappings.lean | 100 ++++- PrintAxioms.lean | 22 +- Verity/Core.lean | 406 +++++++++++++++++- .../PropertyHashedMappingExecSmoke.t.sol | 10 +- artifacts/verification_status.json | 2 +- docs-site/public/llms.txt | 2 +- docs/AXIOMS.md | 12 +- docs/PARETO_MODEL_SUPPORT.md | 83 ++-- docs/TRUST_ASSUMPTIONS.md | 39 +- 17 files changed, 1028 insertions(+), 120 deletions(-) create mode 100644 Compiler/Proofs/Storage/HashedMappingLayout.lean diff --git a/Compiler/Proofs/MappingSlot.lean b/Compiler/Proofs/MappingSlot.lean index 6eda5180e7..4010558937 100644 --- a/Compiler/Proofs/MappingSlot.lean +++ b/Compiler/Proofs/MappingSlot.lean @@ -310,4 +310,41 @@ theorem solidityMappingSlot_add_wordOffset_lt_evmModulus solidityMappingSlot baseSlot key + wordOffset < Compiler.Constants.evmModulus := by exact solidityMappingSlot_add_lt_evmModulus baseSlot key wordOffset h +/-! ### Hashed mapping-chain layout (interpretation of `StorageKey.mapChain`) + +The executable plane keeps nested / struct mapping words under the symbolic +key `Verity.StorageKey.mapChain baseSlot keys wordOffset`. Their Solidity +storage location folds `keccak256(key ‖ acc)` left-to-right over the key path +and adds the word offset modulo `2^256`. None of the facts below use +`solidityMappingSlot_injective`. -/ + +/-- Solidity storage location of word `wordOffset` of the value stored under + the key path `keys` of the mapping rooted at `baseSlot`. -/ +def mappingChainSlotLocation (baseSlot : Nat) (keys : List Nat) (wordOffset : Nat) : Nat := + (keys.foldl solidityMappingSlot baseSlot + wordOffset) % Compiler.Constants.evmModulus + +theorem mappingChainSlotLocation_single (baseSlot key wordOffset : Nat) : + mappingChainSlotLocation baseSlot [key] wordOffset = + mappingSlotLocation baseSlot key wordOffset := rfl + +theorem mappingChainSlotLocation_pair (baseSlot key1 key2 wordOffset : Nat) : + mappingChainSlotLocation baseSlot [key1, key2] wordOffset = + nestedMappingSlotLocation baseSlot key1 key2 wordOffset := rfl + +theorem foldl_solidityMappingSlot_lt_evmModulus (acc : Nat) (keys : List Nat) + (h : acc < Compiler.Constants.evmModulus) : + keys.foldl solidityMappingSlot acc < Compiler.Constants.evmModulus := by + induction keys generalizing acc with + | nil => exact h + | cons key keys ih => exact ih _ (solidityMappingSlot_lt_evmModulus acc key) + +/-- A non-empty key path at word offset `0` is exactly the folded keccak slot. -/ +theorem mappingChainSlotLocation_zero (baseSlot key : Nat) (keys : List Nat) : + mappingChainSlotLocation baseSlot (key :: keys) 0 = + (key :: keys).foldl solidityMappingSlot baseSlot := by + unfold mappingChainSlotLocation + rw [Nat.add_zero] + exact Nat.mod_eq_of_lt + (foldl_solidityMappingSlot_lt_evmModulus _ keys (solidityMappingSlot_lt_evmModulus _ _)) + end Compiler.Proofs diff --git a/Compiler/Proofs/Storage/HashedMappingLayout.lean b/Compiler/Proofs/Storage/HashedMappingLayout.lean new file mode 100644 index 0000000000..b644e500c6 --- /dev/null +++ b/Compiler/Proofs/Storage/HashedMappingLayout.lean @@ -0,0 +1,183 @@ +/- + G2 residual: the Solidity keccak layout of hashed mapping chains as an + *interpretation* of the symbolic executable channel. + + The executable plane stores nested-mapping, word-offset mapping and + struct-mapping words under `StorageKey.mapChain base keys offset` + (transient chains under `StorageKey.transientMapChain base keys`), so + contract proofs separate entries by constructor injectivity alone. The + compiler/model plane addresses the same words in the flat `.slot` + (resp. `.transient`) channel at `mappingChainSlotLocation base keys offset` + = `(fold keccak256(key ‖ acc) + offset) mod 2^256`. + + This file relates the two, in the same shape as the `.map` / `.mapUint` / + `.map2` shadows in `MappingCoherence`: a coherence relation over a finite + set of tracked entries, preserved by aligned writes (symbolic entry + flat + slot) and by every other channel write whose flat slot avoids the tracked + locations. Non-aliasing of the tracked Solidity slots is a hypothesis + (`LayoutNonAlias`, dischargeable from the existing + `StorageSlotNonAliasCertificate`), never an axiom: nothing here uses + `solidityMappingSlot_injective`, and contract-level proofs over the + executable plane never need this file. +-/ + +import Verity.Core +import Compiler.Proofs.MappingSlot + +namespace Compiler.Proofs.Storage.HashedMappingLayout + +open Verity +open Verity.ContractState +open Compiler.Proofs + +/-- A tracked hashed-mapping word: `(baseSlot, keyWords, wordOffset)`. -/ +abbrev Entry := Nat × List Nat × Nat + +/-- The symbolic executable key of an entry. -/ +def Entry.key (e : Entry) : StorageKey := .mapChain e.1 e.2.1 e.2.2 + +/-- The Solidity storage location of an entry (the compiler's slot). -/ +def Entry.location (e : Entry) : Nat := mappingChainSlotLocation e.1 e.2.1 e.2.2 + +/-- The executable word of an entry. -/ +def Entry.read (s : ContractState) (e : Entry) : Uint256 := s.readMapChain e.1 e.2.1 e.2.2 + +theorem Entry.key_injective {e e' : Entry} (h : e.key = e'.key) : e = e' := by + rcases e with ⟨b, ks, o⟩ + rcases e' with ⟨b', ks', o'⟩ + simp only [Entry.key, StorageKey.mapChain.injEq] at h + rcases h with ⟨rfl, rfl, rfl⟩ + rfl + +/-- Executable hashed words agree with the flat `.slot` channel (the channel the + model plane reads) at the Solidity location of every tracked entry. -/ +def HashedCoherentOn (tracked : List Entry) (s : ContractState) : Prop := + ∀ e ∈ tracked, e.read s = s.storage e.location + +/-- Layout certificate: distinct tracked entries have distinct Solidity slots. -/ +def LayoutNonAlias (tracked : List Entry) : Prop := + ∀ e ∈ tracked, ∀ e' ∈ tracked, e ≠ e' → e.location ≠ e'.location + +/-- The existing finite non-alias certificate over the tracked locations is a + layout certificate. -/ +theorem layoutNonAlias_of_certificate {tracked : List Entry} + (cert : StorageSlotNonAliasCertificate (tracked.map Entry.location)) : + LayoutNonAlias tracked := by + intro e he e' he' hne hloc + exact hne (List.inj_on_of_nodup_map cert.distinct he he' hloc) + +theorem defaultState_hashedCoherentOn (tracked : List Entry) : + HashedCoherentOn tracked defaultState := by + intro e _ + rfl + +/-- Aligned write: the symbolic entry plus the compiler's flat slot. -/ +def alignedWrite (s : ContractState) (e : Entry) (v : Uint256) : ContractState := + (s.writeMapChain e.1 e.2.1 e.2.2 v).writeSlot e.location v + +/-- Reading a tracked entry is reading the flat channel at its Solidity slot. -/ +theorem read_eq_storage_location {tracked : List Entry} {s : ContractState} + (hcoh : HashedCoherentOn tracked s) {e : Entry} (he : e ∈ tracked) : + s.readMapChain e.1 e.2.1 e.2.2 = s.storage e.location := + hcoh e he + +/-- The aligned write makes the written entry coherent regardless of the prior world. -/ +theorem alignedWrite_same (s : ContractState) (e : Entry) (v : Uint256) : + e.read (alignedWrite s e v) = (alignedWrite s e v).storage e.location := by + simp [Entry.read, alignedWrite] + +/-- Aligned writes preserve coherence on a layout-certified tracked set. -/ +theorem alignedWrite_preserves {tracked : List Entry} {s : ContractState} + (hcoh : HashedCoherentOn tracked s) (hna : LayoutNonAlias tracked) + {w : Entry} (hw : w ∈ tracked) (v : Uint256) : + HashedCoherentOn tracked (alignedWrite s w v) := by + intro e he + by_cases hew : e = w + · subst hew + exact alignedWrite_same s e v + · have hloc : e.location ≠ w.location := hna e he w hw hew + have hkey : StorageKey.mapChain e.1 e.2.1 e.2.2 ≠ .mapChain w.1 w.2.1 w.2.2 := + fun h => hew (Entry.key_injective h) + have hread : e.read (alignedWrite s w v) = e.read s := by + simp only [Entry.read, alignedWrite, readMapChain_writeSlot] + exact readMapChain_writeMapChain_of_ne s hkey v + have hflat : (alignedWrite s w v).storage e.location = s.storage e.location := by + simp only [alignedWrite] + rw [storage_writeSlot_other _ hloc, storage_writeMapChain] + rw [hread, hflat] + exact hcoh e he + +/-- A scalar write preserves coherence when its slot avoids every tracked + Solidity location. This is where mapping-vs-scalar separation lives for the + *interpretation*; the executable plane needs no such fact + (`ContractState.readMapChain_writeSlot`). -/ +theorem writeSlot_preserves {tracked : List Entry} {s : ContractState} + (hcoh : HashedCoherentOn tracked s) {n : Nat} (havoid : ∀ e ∈ tracked, e.location ≠ n) + (v : Uint256) : HashedCoherentOn tracked (s.writeSlot n v) := by + intro e he + simp only [Entry.read, readMapChain_writeSlot] + rw [storage_writeSlot_other _ (havoid e he)] + exact hcoh e he + +theorem writeTransient_preserves {tracked : List Entry} {s : ContractState} + (hcoh : HashedCoherentOn tracked s) (n : Nat) (v : Uint256) : + HashedCoherentOn tracked (s.writeTransient n v) := by + intro e he + have := hcoh e he + simp only [Entry.read] at this ⊢ + simpa [storage, writeTransient, readMapChain, storageMapChain] using this + +theorem writeTransientMapChain_preserves {tracked : List Entry} {s : ContractState} + (hcoh : HashedCoherentOn tracked s) (n : Nat) (keys : List Nat) (v : Uint256) : + HashedCoherentOn tracked (s.writeTransientMapChain n keys v) := by + intro e he + simp only [Entry.read, readMapChain_writeTransientMapChain, storage_writeTransientMapChain] + exact hcoh e he + +theorem writeAddrSlot_preserves {tracked : List Entry} {s : ContractState} + (hcoh : HashedCoherentOn tracked s) (n : Nat) (v : Address) : + HashedCoherentOn tracked (s.writeAddrSlot n v) := by + intro e he + have := hcoh e he + simp only [Entry.read] at this ⊢ + simpa [storage, writeAddrSlot, readMapChain, storageMapChain] using this + +/-! ### Transient chains + +Transient chains are interpreted in the flat `.transient` channel at the same +folded keccak location (word offset `0`). -/ + +/-- A tracked transient hashed word: `(baseSlot, keyWords)`. -/ +abbrev TEntry := Nat × List Nat + +def TEntry.location (e : TEntry) : Nat := mappingChainSlotLocation e.1 e.2 0 + +def TransientHashedCoherentOn (tracked : List TEntry) (s : ContractState) : Prop := + ∀ e ∈ tracked, s.readTransientMapChain e.1 e.2 = s.transientStorage e.location + +def alignedTransientWrite (s : ContractState) (e : TEntry) (v : Uint256) : ContractState := + (s.writeTransientMapChain e.1 e.2 v).writeTransient e.location v + +theorem alignedTransientWrite_preserves {tracked : List TEntry} {s : ContractState} + (hcoh : TransientHashedCoherentOn tracked s) + (hna : ∀ e ∈ tracked, ∀ e' ∈ tracked, e ≠ e' → e.location ≠ e'.location) + {w : TEntry} (hw : w ∈ tracked) (v : Uint256) : + TransientHashedCoherentOn tracked (alignedTransientWrite s w v) := by + intro e he + rcases e with ⟨b, ks⟩ + rcases w with ⟨b', ks'⟩ + by_cases hew : (b, ks) = (b', ks') + · simp only [Prod.mk.injEq] at hew + rcases hew with ⟨rfl, rfl⟩ + simp [alignedTransientWrite, readTransientMapChain, transientStorageMapChain, + transientStorage, writeTransient] + · have hloc := hna _ he _ hw hew + have hne : ¬ (b = b' ∧ ks = ks') := fun h => hew (by rw [h.1, h.2]) + have := hcoh _ he + have hloc' : mappingChainSlotLocation b ks 0 ≠ mappingChainSlotLocation b' ks' 0 := hloc + simp only [TEntry.location] at this ⊢ + simp [alignedTransientWrite, readTransientMapChain, transientStorageMapChain, + transientStorage, writeTransient, TEntry.location, hloc', hne] at this ⊢ + exact this + +end Compiler.Proofs.Storage.HashedMappingLayout diff --git a/Compiler/Proofs/Storage/MappingCoherence.lean b/Compiler/Proofs/Storage/MappingCoherence.lean index 6e8310e911..6531f240fd 100644 --- a/Compiler/Proofs/Storage/MappingCoherence.lean +++ b/Compiler/Proofs/Storage/MappingCoherence.lean @@ -28,7 +28,9 @@ def storageKeySlot : StorageKey → Option Nat | .mapUint n key => some (solidityMappingSlot n key.val) | .map2 n k1 k2 => some (abstractNestedMappingSlot n (addressToWord k1).val (addressToWord k2).val) + | .mapChain n keys offset => some (mappingChainSlotLocation n keys offset) | .transient _ => none + | .transientMapChain _ _ => none | .contractSlot c n => if c = 0 then some n else none | .scoped _ _ => none @@ -193,6 +195,14 @@ theorem writeMap2_aligned_other (s : ContractState) (slot : Nat) (k1 k2 : Addres theorem storageKeySlot_mapUint (slot : Nat) (key : Uint256) : storageKeySlot (.mapUint slot key) = some (solidityMappingSlot slot key.val) := rfl +/-- `storageKeySlot` on a hashed mapping-chain key is its Solidity location. -/ +theorem storageKeySlot_mapChain (slot : Nat) (keys : List Nat) (offset : Nat) : + storageKeySlot (.mapChain slot keys offset) = + some (mappingChainSlotLocation slot keys offset) := rfl + +theorem storageKeySlot_transientMapChain (slot : Nat) (keys : List Nat) : + storageKeySlot (.transientMapChain slot keys) = none := rfl + theorem storageKeySlot_map2 (slot : Nat) (k1 k2 : Address) : storageKeySlot (.map2 slot k1 k2) = some (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) := diff --git a/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean b/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean index deae41a11b..393ffbaeea 100644 --- a/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean +++ b/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean @@ -92,6 +92,10 @@ def storageKeySlot (fields : List Field) : StorageKey → Option (Channel × Nat | .transient n => some (.transient, n) | .contractSlot c n => some (.contract c, n) | .scoped _ _ => none + -- Hashed mapping chains are related to the flat channel by + -- `Compiler.Proofs.Storage.HashedMappingLayout`, not by this layout table. + | .mapChain _ _ _ => none + | .transientMapChain _ _ => none | .map n key => match fieldMapKindAt fields n with | some (.simple .address) => @@ -242,6 +246,8 @@ theorem mappingCoherentAllKeys_of_globals (fields : List Field) (s : ContractSta | contractSlot c m => obtain ⟨rfl, rfl⟩ := storageKeySlot_contractSlot_eq h; rfl | «scoped» _ _ => simp [storageKeySlot] at h + | mapChain _ _ _ => simp [storageKeySlot] at h + | transientMapChain _ _ => simp [storageKeySlot] at h | map m key => obtain ⟨_, rfl, rfl⟩ := storageKeySlot_map_eq h exact h1 m key @@ -475,6 +481,8 @@ theorem writeMap_aligned_preserves_mappingCoherentAllKeys | transient m => obtain ⟨rfl, rfl⟩ := storageKeySlot_transient_eq h; rfl | contractSlot c m => obtain ⟨rfl, rfl⟩ := storageKeySlot_contractSlot_eq h; rfl | «scoped» _ _ => simp [storageKeySlot] at h + | mapChain _ _ _ => simp [storageKeySlot] at h + | transientMapChain _ _ => simp [storageKeySlot] at h | map m key' => obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map_eq h exact writeMap_aligned_map_case fields s slot key v m key' hkind' hcoh @@ -513,6 +521,8 @@ theorem writeMapUint_aligned_preserves_mappingCoherentAllKeys | transient m => obtain ⟨rfl, rfl⟩ := storageKeySlot_transient_eq h; rfl | contractSlot c m => obtain ⟨rfl, rfl⟩ := storageKeySlot_contractSlot_eq h; rfl | «scoped» _ _ => simp [storageKeySlot] at h + | mapChain _ _ _ => simp [storageKeySlot] at h + | transientMapChain _ _ => simp [storageKeySlot] at h | map m key' => obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map_eq h have hm : m ≠ slot := base_ne_of_kind_ne hkind' hkind (by simp) @@ -550,6 +560,8 @@ theorem writeMap2_aligned_preserves_mappingCoherentAllKeys | transient m => obtain ⟨rfl, rfl⟩ := storageKeySlot_transient_eq h; rfl | contractSlot c m => obtain ⟨rfl, rfl⟩ := storageKeySlot_contractSlot_eq h; rfl | «scoped» _ _ => simp [storageKeySlot] at h + | mapChain _ _ _ => simp [storageKeySlot] at h + | transientMapChain _ _ => simp [storageKeySlot] at h | map m key' => obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map_eq h have hsome' : (fieldMapKindAt fields m).isSome = true := by rw [hkind']; rfl @@ -589,6 +601,8 @@ theorem writeSlot_preserves_mappingCoherentAllKeys | transient m => obtain ⟨rfl, rfl⟩ := storageKeySlot_transient_eq h; rfl | contractSlot c m => obtain ⟨rfl, rfl⟩ := storageKeySlot_contractSlot_eq h; rfl | «scoped» _ _ => simp [storageKeySlot] at h + | mapChain _ _ _ => simp [storageKeySlot] at h + | transientMapChain _ _ => simp [storageKeySlot] at h | map m key' => have hne := havoid _ _ _ h rfl obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map_eq h @@ -621,6 +635,8 @@ theorem writeAddrSlot_preserves_mappingCoherentAllKeys | transient m => obtain ⟨rfl, rfl⟩ := storageKeySlot_transient_eq h; rfl | contractSlot c m => obtain ⟨rfl, rfl⟩ := storageKeySlot_contractSlot_eq h; rfl | «scoped» _ _ => simp [storageKeySlot] at h + | mapChain _ _ _ => simp [storageKeySlot] at h + | transientMapChain _ _ => simp [storageKeySlot] at h | map m key' => obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map_eq h simpa [channelRead, storageMap, storage, writeAddrSlot] using @@ -646,6 +662,8 @@ theorem writeTransient_preserves_mappingCoherentAllKeys | transient m => obtain ⟨rfl, rfl⟩ := storageKeySlot_transient_eq h; rfl | contractSlot c m => obtain ⟨rfl, rfl⟩ := storageKeySlot_contractSlot_eq h; rfl | «scoped» _ _ => simp [storageKeySlot] at h + | mapChain _ _ _ => simp [storageKeySlot] at h + | transientMapChain _ _ => simp [storageKeySlot] at h | map m key' => obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map_eq h simpa [channelRead, storageMap, storage, writeTransient] using diff --git a/Compiler/SolidityImport/Transactions.lean b/Compiler/SolidityImport/Transactions.lean index 5c2bab0b25..f5cd57b1a9 100644 --- a/Compiler/SolidityImport/Transactions.lean +++ b/Compiler/SolidityImport/Transactions.lean @@ -9,6 +9,7 @@ open Denote Verity.Core /-- Transient keys can be parked under another account during external calls. -/ def isTransientKey : Verity.StorageKey → Bool | .transient _ => true + | .transientMapChain _ _ => true | .scoped _ key => isTransientKey key | _ => false diff --git a/Compiler/TypedIRCompilerCorrectness.lean b/Compiler/TypedIRCompilerCorrectness.lean index e8a80cfbea..8d65768fa5 100644 --- a/Compiler/TypedIRCompilerCorrectness.lean +++ b/Compiler/TypedIRCompilerCorrectness.lean @@ -1800,6 +1800,8 @@ theorem compile_letCaller_letStorageAddr_reqEq_letMapping_letStorage_setMapping_ | addr slot => simp | mapUint slot mapKey => simp | map2 slot key1 key2 => simp + | mapChain slot keys offset => simp + | transientMapChain slot keys => simp | «scoped» contract key => simp · simp [evalTStmtsFuel, evalTStmtFuel, evalTExpr, hEq, TVars.set, TVars.get] diff --git a/Contracts/Common.lean b/Contracts/Common.lean index d76bb27864..2d45e22865 100644 --- a/Contracts/Common.lean +++ b/Contracts/Common.lean @@ -1789,12 +1789,13 @@ private def encodePackedWord (current value : Uint256) (offset width : Nat) : Ui let cleared := Verity.Core.Uint256.and current (Verity.Core.Uint256.not shiftedMask) Verity.Core.Uint256.or cleared (Verity.Core.Uint256.shl offset packedValue) +/-- Read struct member word `wordOffset` of `mapping[key]` at `baseSlot` from the + hashed mapping-chain channel (`StorageKey.mapChain baseSlot [key] wordOffset`). -/ def structMemberAt {κ α : Type} [StorageKey κ] [StorageWord α] (baseSlot : Nat) (wordOffset : Nat) (packed : Option (Nat × Nat)) (key : κ) : Contract α := fun state => - let targetSlot := structSlot baseSlot (StorageKey.toWord key) wordOffset - let raw := state.storage targetSlot + let raw := state.readMapChain baseSlot [StorageKey.toWord key] wordOffset let word := match packed with | none => raw | some (offset, width) => decodePackedWord raw offset width @@ -1804,8 +1805,8 @@ def structMember2At {κ₁ κ₂ α : Type} [StorageKey κ₁] [StorageKey κ₂ (baseSlot : Nat) (wordOffset : Nat) (packed : Option (Nat × Nat)) (key1 : κ₁) (key2 : κ₂) : Contract α := fun state => - let targetSlot := structSlot2 baseSlot (StorageKey.toWord key1) (StorageKey.toWord key2) wordOffset - let raw := state.storage targetSlot + let raw := state.readMapChain baseSlot + [StorageKey.toWord key1, StorageKey.toWord key2] wordOffset let word := match packed with | none => raw | some (offset, width) => decodePackedWord raw offset width @@ -1815,32 +1816,50 @@ def setStructMemberAt {κ α : Type} [StorageKey κ] [StorageWord α] (baseSlot : Nat) (wordOffset : Nat) (packed : Option (Nat × Nat)) (key : κ) (value : α) : Contract Unit := fun state => - let targetSlot := structSlot baseSlot (StorageKey.toWord key) wordOffset + let keys := [StorageKey.toWord key] let word := StorageWord.toWord value let stored := match packed with | none => word - | some (offset, width) => encodePackedWord (state.storage targetSlot) word offset width - ContractResult.success () (state.writeSlot targetSlot stored) + | some (offset, width) => + encodePackedWord (state.readMapChain baseSlot keys wordOffset) word offset width + ContractResult.success () (state.writeMapChain baseSlot keys wordOffset stored) def setStructMember2At {κ₁ κ₂ α : Type} [StorageKey κ₁] [StorageKey κ₂] [StorageWord α] (baseSlot : Nat) (wordOffset : Nat) (packed : Option (Nat × Nat)) (key1 : κ₁) (key2 : κ₂) (value : α) : Contract Unit := fun state => - let targetSlot := structSlot2 baseSlot (StorageKey.toWord key1) (StorageKey.toWord key2) wordOffset + let keys := [StorageKey.toWord key1, StorageKey.toWord key2] let word := StorageWord.toWord value let stored := match packed with | none => word - | some (offset, width) => encodePackedWord (state.storage targetSlot) word offset width - ContractResult.success () (state.writeSlot targetSlot stored) + | some (offset, width) => + encodePackedWord (state.readMapChain baseSlot keys wordOffset) word offset width + ContractResult.success () (state.writeMapChain baseSlot keys wordOffset stored) -/-! ### Hashed mapping channel (Solidity keccak slot layout) +/-! ### Hashed mapping channel (symbolic keys; Solidity keccak layout as interpretation) Nested mappings (`getMappingN` / `setMappingN`), word-offset mapping words (`getMappingWord` / `setMappingWord`) and struct mappings (`structMemberAt`, -`structMember2At`) share one executable slot derivation with the compiler's -proof model (`Compiler.Proofs.MappingSlot`): +`structMember2At`, `setStructMemberAt`, `setStructMember2At`, `structMembers` +destructuring) execute on a dedicated symbolic channel of `ContractState`: +the word lives under `StorageKey.mapChain baseSlot keyWords wordOffset` +(`ContractState.readMapChain` / `writeMapChain`), and transient chains under +`StorageKey.transientMapChain baseSlot keyWords` +(`readTransientMapChain` / `writeTransientMapChain`). Key words are the ABI +words of the keys (`MappingKeyWord.word`, `StorageKey.toWord`). Two entries are +independent iff their `(baseSlot, keyWords, wordOffset)` differ, and the channel +never touches the scalar `.slot` channel, so non-aliasing — between keys, +struct members, fields, or a mapping entry and a plain scalar slot — is +constructor injectivity, with no keccak assumption +(`ContractState.readMapChain_writeMapChain`, `readMapChain_writeSlot`, +`storage_writeMapChain`, ...). + +The Solidity slot the compiler emits for each entry is an interpretation, +`Compiler.Proofs.mappingChainSlotLocation` (related to the executable channel in +`Compiler.Proofs.Storage.HashedMappingLayout`), and is kept here for layout +statements (`mappingChainSlot`, `structSlot`, `structSlot2`): * `mapping(k => v)` at base slot `p` stores `v` at `keccak256(k ‖ p)` (`Compiler.Proofs.abstractMappingSlot`, i.e. `solidityMappingSlot`); @@ -1849,18 +1868,18 @@ proof model (`Compiler.Proofs.MappingSlot`): * struct members and `getMappingWord` add their word offset modulo `2^256` (`mappingSlotLocation` / `nestedMappingSlotLocation`). -Values live in the `.slot` channel of `ContractState` (`ContractState.storage`), -which is the channel the model plane reads through `readFieldWord` with -`DenoteOracle.mappingSlot := abstractMappingSlot`. Transient mapping chains use -the `.transient` channel (`getTransientMappingN` / `setTransientMappingN`; the -macro routes `getMappingN` / `setMappingN` on a `transient` field there). +The model plane (`readFieldWord` with `DenoteOracle.mappingSlot := +abstractMappingSlot`) reads the flat `.slot` channel at those locations; the +executable plane agrees with it under the coherence relation of +`HashedMappingLayout`, exactly as the `.map` / `.mapUint` / `.map2` shadows +relate to it in `Compiler.Proofs.Storage.MappingCoherence`. The macro routes +`getMappingN` / `setMappingN` on a `transient` field to +`getTransientMappingN` / `setTransientMappingN`. -This channel is deliberately disjoint from the constructor-keyed -`storageMap` / `storageMapUint` / `storageMap2` channels behind `getMapping`, -`getMappingUint` and `getMapping2`: those keep keys symbolic so lens laws use -constructor injectivity instead of keccak collision-resistance. A field must -be accessed through one family consistently; the macro already fixes the -family per storage type. -/ +This channel is disjoint from the constructor-keyed `storageMap` / +`storageMapUint` / `storageMap2` channels behind `getMapping`, +`getMappingUint` and `getMapping2`. A field must be accessed through one +family consistently; the macro already fixes the family per storage type. -/ @[simp] theorem StorageKey.toWord_address (key : Address) : StorageKey.toWord key = key.toNat := rfl @@ -1886,8 +1905,33 @@ instance : Coe Address MappingKeyWord where instance : Coe Uint256 MappingKeyWord where coe key := ⟨StorageKey.toWord key⟩ -/-- Solidity slot of a nested-mapping value: fold `keccak256(key ‖ slot)` -left-to-right over the key path. The empty path is the base slot itself. -/ +/-- Key words of a hashed-mapping key path (the symbolic `mapChain` key path). -/ +abbrev MappingKeyWord.words (keys : List MappingKeyWord) : List Nat := + keys.map MappingKeyWord.word + +@[simp] theorem MappingKeyWord.words_nil : MappingKeyWord.words [] = [] := rfl +@[simp] theorem MappingKeyWord.words_cons (key : MappingKeyWord) (keys : List MappingKeyWord) : + MappingKeyWord.words (key :: keys) = key.word :: MappingKeyWord.words keys := rfl + +@[simp] theorem MappingKeyWord.word_ofAddress (key : Address) : + (key : MappingKeyWord).word = key.toNat := rfl +@[simp] theorem MappingKeyWord.word_ofUint256 (key : Uint256) : + (key : MappingKeyWord).word = key.val := rfl + +/-- Key words are injective per key type, so key-path inequality reduces to key +inequality (`[↑user, ↑epoch]` vs `[↑user', ↑epoch']`). -/ +@[simp] theorem MappingKeyWord.address_word_eq_iff (a b : Address) : + a.toNat = b.toNat ↔ a = b := + ⟨Verity.Core.Address.toNat_injective a b, fun h => h ▸ rfl⟩ + +@[simp] theorem MappingKeyWord.uint256_word_eq_iff (a b : Uint256) : + a.val = b.val ↔ a = b := + ⟨Verity.Core.Uint256.ext, fun h => h ▸ rfl⟩ + +/-- Layout (interpretation only): Solidity slot of a nested-mapping value, folding +`keccak256(key ‖ slot)` left-to-right over the key path. The empty path is the +base slot itself. The executable plane does not read or write this slot; see +`mappingChainSlot_eq_location`. -/ def mappingChainSlot (baseSlot : Nat) (keys : List MappingKeyWord) : Nat := keys.foldl (fun acc key => Compiler.Proofs.abstractMappingSlot acc key.word) baseSlot @@ -1908,6 +1952,26 @@ theorem mappingChainSlot_pair (baseSlot : Nat) (key1 key2 : MappingKeyWord) : mappingChainSlot baseSlot [key1, key2] = Compiler.Proofs.abstractNestedMappingSlot baseSlot key1.word key2.word := rfl +/-- A non-empty key path's slot is the interpretation of `mapChain baseSlot keys 0`. -/ +theorem mappingChainSlot_eq_location (baseSlot : Nat) (key : MappingKeyWord) + (keys : List MappingKeyWord) : + mappingChainSlot baseSlot (key :: keys) = + Compiler.Proofs.mappingChainSlotLocation baseSlot + (MappingKeyWord.words (key :: keys)) 0 := by + rw [MappingKeyWord.words_cons, Compiler.Proofs.mappingChainSlotLocation_zero] + unfold mappingChainSlot + rw [← List.map_cons, List.foldl_map] + rfl + +/-- Struct-member slots are the interpretation of `mapChain baseSlot [key] wordOffset`. -/ +theorem structSlot_eq_location (baseSlot key wordOffset : Nat) : + structSlot baseSlot key wordOffset = + Compiler.Proofs.mappingChainSlotLocation baseSlot [key] wordOffset := rfl + +theorem structSlot2_eq_location (baseSlot key1 key2 wordOffset : Nat) : + structSlot2 baseSlot key1 key2 wordOffset = + Compiler.Proofs.mappingChainSlotLocation baseSlot [key1, key2] wordOffset := rfl + /-- Struct-member slots are the compiler's `mappingSlotLocation`. -/ theorem structSlot_eq_mappingSlotLocation (baseSlot key wordOffset : Nat) : structSlot baseSlot key wordOffset = @@ -1938,102 +2002,157 @@ theorem structSlot_ne_succ (baseSlot key wordOffset : Nat) : rw [← Nat.add_assoc] exact mod_ne_succ_mod _ _ (by decide) -/-- Read a nested-mapping word at the Solidity slot of `keys` under `slot`. -/ +/-- Read the nested-mapping word under `keys` of `field` (`mapChain field.slot keys 0`). -/ def getMappingN {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) : Contract Uint256 := - fun state => ContractResult.success (state.storage (mappingChainSlot field.slot keys)) state + fun state => + ContractResult.success (state.readMapChain field.slot (MappingKeyWord.words keys) 0) state -/-- Write a nested-mapping word at the Solidity slot of `keys` under `slot`. -/ +/-- Write the nested-mapping word under `keys` of `field` (`mapChain field.slot keys 0`). -/ def setMappingN {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (value : Uint256) : Contract Unit := - fun state => ContractResult.success () (state.writeSlot (mappingChainSlot field.slot keys) value) + fun state => + ContractResult.success () (state.writeMapChain field.slot (MappingKeyWord.words keys) 0 value) /-- `getMappingN` for a `transient` mapping chain (EIP-1153 channel). -/ def getTransientMappingN {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) : Contract Uint256 := fun state => - ContractResult.success (state.transientStorage (mappingChainSlot field.slot keys)) state + ContractResult.success + (state.readTransientMapChain field.slot (MappingKeyWord.words keys)) state /-- `setMappingN` for a `transient` mapping chain (EIP-1153 channel). -/ def setTransientMappingN {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (value : Uint256) : Contract Unit := fun state => - ContractResult.success () (state.writeTransient (mappingChainSlot field.slot keys) value) + ContractResult.success () + (state.writeTransientMapChain field.slot (MappingKeyWord.words keys) value) -/-- Read word `wordOffset` of the value stored under `key` (`keccak256(key ‖ slot) + wordOffset`). -/ +/-- Read word `wordOffset` of the value stored under `key` (`mapChain field.slot [key] wordOffset`; + Solidity slot `keccak256(key ‖ slot) + wordOffset`). -/ def getMappingWord (field : StorageSlot (Uint256 → Uint256)) (key wordOffset : Uint256) : Contract Uint256 := - fun state => ContractResult.success (state.storage (structSlot field.slot key.val wordOffset.val)) state + fun state => + ContractResult.success (state.readMapChain field.slot [key.val] wordOffset.val) state /-- Write word `wordOffset` of the value stored under `key`. -/ def setMappingWord (field : StorageSlot (Uint256 → Uint256)) (key wordOffset value : Uint256) : Contract Unit := fun state => - ContractResult.success () (state.writeSlot (structSlot field.slot key.val wordOffset.val) value) + ContractResult.success () (state.writeMapChain field.slot [key.val] wordOffset.val value) @[simp] theorem getMappingN_run {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (state : ContractState) : (getMappingN field keys).run state = - ContractResult.success (state.storage (mappingChainSlot field.slot keys)) state := rfl + ContractResult.success (state.readMapChain field.slot (MappingKeyWord.words keys) 0) state := + rfl @[simp] theorem setMappingN_run {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (value : Uint256) (state : ContractState) : (setMappingN field keys value).run state = - ContractResult.success () (state.writeSlot (mappingChainSlot field.slot keys) value) := rfl + ContractResult.success () + (state.writeMapChain field.slot (MappingKeyWord.words keys) 0 value) := rfl @[simp] theorem getTransientMappingN_run {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (state : ContractState) : (getTransientMappingN field keys).run state = - ContractResult.success (state.transientStorage (mappingChainSlot field.slot keys)) state := rfl + ContractResult.success + (state.readTransientMapChain field.slot (MappingKeyWord.words keys)) state := rfl @[simp] theorem setTransientMappingN_run {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (value : Uint256) (state : ContractState) : (setTransientMappingN field keys value).run state = - ContractResult.success () (state.writeTransient (mappingChainSlot field.slot keys) value) := rfl + ContractResult.success () + (state.writeTransientMapChain field.slot (MappingKeyWord.words keys) value) := rfl @[simp] theorem getMappingWord_run (field : StorageSlot (Uint256 → Uint256)) (key wordOffset : Uint256) (state : ContractState) : (getMappingWord field key wordOffset).run state = - ContractResult.success (state.storage (structSlot field.slot key.val wordOffset.val)) state := rfl + ContractResult.success (state.readMapChain field.slot [key.val] wordOffset.val) state := rfl @[simp] theorem setMappingWord_run (field : StorageSlot (Uint256 → Uint256)) (key wordOffset value : Uint256) (state : ContractState) : (setMappingWord field key wordOffset value).run state = - ContractResult.success () (state.writeSlot (structSlot field.slot key.val wordOffset.val) value) := + ContractResult.success () (state.writeMapChain field.slot [key.val] wordOffset.val value) := rfl @[simp] theorem structMemberAt_run {κ α : Type} [StorageKey κ] [StorageWord α] (baseSlot wordOffset : Nat) (key : κ) (state : ContractState) : (structMemberAt (α := α) baseSlot wordOffset none key).run state = ContractResult.success - (StorageWord.fromWord (state.storage (structSlot baseSlot (StorageKey.toWord key) wordOffset))) + (StorageWord.fromWord (state.readMapChain baseSlot [StorageKey.toWord key] wordOffset)) state := rfl @[simp] theorem setStructMemberAt_run {κ α : Type} [StorageKey κ] [StorageWord α] (baseSlot wordOffset : Nat) (key : κ) (value : α) (state : ContractState) : (setStructMemberAt baseSlot wordOffset none key value).run state = ContractResult.success () - (state.writeSlot (structSlot baseSlot (StorageKey.toWord key) wordOffset) + (state.writeMapChain baseSlot [StorageKey.toWord key] wordOffset + (StorageWord.toWord value)) := rfl + +@[simp] theorem structMember2At_run {κ₁ κ₂ α : Type} [StorageKey κ₁] [StorageKey κ₂] + [StorageWord α] (baseSlot wordOffset : Nat) (key1 : κ₁) (key2 : κ₂) (state : ContractState) : + (structMember2At (α := α) baseSlot wordOffset none key1 key2).run state = + ContractResult.success + (StorageWord.fromWord (state.readMapChain baseSlot + [StorageKey.toWord key1, StorageKey.toWord key2] wordOffset)) + state := rfl + +@[simp] theorem setStructMember2At_run {κ₁ κ₂ α : Type} [StorageKey κ₁] [StorageKey κ₂] + [StorageWord α] (baseSlot wordOffset : Nat) (key1 : κ₁) (key2 : κ₂) (value : α) + (state : ContractState) : + (setStructMember2At baseSlot wordOffset none key1 key2 value).run state = + ContractResult.success () + (state.writeMapChain baseSlot [StorageKey.toWord key1, StorageKey.toWord key2] wordOffset (StorageWord.toWord value)) := rfl /-- Writing then reading the same key path returns the written word. -/ theorem getMappingN_setMappingN_same {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (value : Uint256) (state : ContractState) : (Verity.bind (setMappingN field keys value) fun _ => getMappingN field keys).run state = - ContractResult.success value (state.writeSlot (mappingChainSlot field.slot keys) value) := by + ContractResult.success value + (state.writeMapChain field.slot (MappingKeyWord.words keys) 0 value) := by simp [Contract.run, Verity.bind, setMappingN, getMappingN] -/-- Transient chains do not touch persistent storage, and vice versa (constructor -injectivity of `StorageKey`, no hash reasoning). -/ +/-- Writing one key path leaves every other key path of any hashed field unchanged + (key-path inequality; no keccak reasoning). -/ +theorem getMappingN_setMappingN_other {α β : Type} (field : StorageSlot α) + (field' : StorageSlot β) (keys keys' : List MappingKeyWord) (value : Uint256) + (state : ContractState) + (h : field'.slot ≠ field.slot ∨ MappingKeyWord.words keys' ≠ MappingKeyWord.words keys) : + (Verity.bind (setMappingN field keys value) fun _ => getMappingN field' keys').run state = + ContractResult.success (state.readMapChain field'.slot (MappingKeyWord.words keys') 0) + (state.writeMapChain field.slot (MappingKeyWord.words keys) 0 value) := by + have hne : Verity.StorageKey.mapChain field'.slot (MappingKeyWord.words keys') 0 ≠ + .mapChain field.slot (MappingKeyWord.words keys) 0 := by + intro hk + simp only [Verity.StorageKey.mapChain.injEq] at hk + rcases h with h | h + · exact h hk.1 + · exact h hk.2.1 + simp only [Contract.run, Verity.bind, setMappingN, getMappingN] + rw [ContractState.readMapChain_writeMapChain_of_ne _ hne] + +/-- Hashed-mapping writes never touch a scalar slot, and scalar writes never touch + a hashed-mapping entry (constructor inequality, no keccak reasoning). -/ +theorem storage_setMappingN {α : Type} (field : StorageSlot α) + (keys : List MappingKeyWord) (value : Uint256) (state : ContractState) (n : Nat) : + (state.writeMapChain field.slot (MappingKeyWord.words keys) 0 value).storage n = + state.storage n := by + simp + +/-- Transient chains do not touch persistent storage or persistent hashed entries, +and vice versa (constructor injectivity of `StorageKey`, no hash reasoning). -/ theorem storage_setTransientMappingN {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (value : Uint256) (state : ContractState) (n : Nat) : - (state.writeTransient (mappingChainSlot field.slot keys) value).storage n = state.storage n := by - simp [ContractState.storage, ContractState.writeTransient] + (state.writeTransientMapChain field.slot (MappingKeyWord.words keys) value).storage n = + state.storage n := by + simp theorem transientStorage_setMappingN {α : Type} (field : StorageSlot α) (keys : List MappingKeyWord) (value : Uint256) (state : ContractState) (n : Nat) : - (state.writeSlot (mappingChainSlot field.slot keys) value).transientStorage n = + (state.writeMapChain field.slot (MappingKeyWord.words keys) 0 value).transientStorage n = state.transientStorage n := by - simp [ContractState.transientStorage, ContractState.writeSlot] + simp end Contracts diff --git a/Contracts/OwnedCounter/Proofs/StorageCoherence.lean b/Contracts/OwnedCounter/Proofs/StorageCoherence.lean index d2a12f46ab..5fcc71555e 100644 --- a/Contracts/OwnedCounter/Proofs/StorageCoherence.lean +++ b/Contracts/OwnedCounter/Proofs/StorageCoherence.lean @@ -115,6 +115,8 @@ theorem storageKeySlot_not_mappingEntry {k : Verity.StorageKey} {ch : Channel} { | «transient» _ => simp [isMappingEntryKey] at hmap | contractSlot _ _ => simp [isMappingEntryKey] at hmap | «scoped» _ _ => simp [isMappingEntryKey] at hmap + | mapChain _ _ _ => simp [isMappingEntryKey] at hmap + | transientMapChain _ _ => simp [isMappingEntryKey] at hmap | map b key => obtain ⟨hkind, _, _⟩ := storageKeySlot_map_eq hk rw [fieldMapKindAt_eq_none] at hkind diff --git a/Contracts/Smoke/HashedMappings.lean b/Contracts/Smoke/HashedMappings.lean index 59309e92c9..fac2b719e2 100644 --- a/Contracts/Smoke/HashedMappings.lean +++ b/Contracts/Smoke/HashedMappings.lean @@ -27,6 +27,7 @@ verity_contract HashedMappingExecSmoke where settledInterest @word 3 ]) := slot 219 transient locks : Bytes32 → Uint256 := slot 1 + withdrawn : Uint256 := slot 206 function setRequest (user : Address, epoch : Uint256, amount : Uint256) : Unit := do setMappingN withdrawsRequestsByEpoch [user, epoch] amount @@ -42,6 +43,9 @@ verity_contract HashedMappingExecSmoke where let current ← getMappingN locks [lockId] return current + function setWithdrawn (amount : Uint256) : Unit := do + setStorage withdrawn amount + function setReceipt (user : Address, principal : Uint256, epoch : Uint256) : Unit := do setStructMember "apr0Users" user "principal" principal setStructMember "apr0Users" user "principalEpoch" epoch @@ -50,7 +54,7 @@ verity_contract HashedMappingExecSmoke where let (principal, epoch) := structMembers "apr0Users" user ["principal", "principalEpoch"] return (principal, epoch) -/-! ## Slot layout agrees with Solidity +/-! ## Slot layout agrees with Solidity (interpretation only) `withdrawsRequestsByEpoch[user][epoch]` at slot 226 lives at `keccak256(epoch ‖ keccak256(user ‖ 226))`; `apr0Users[user].principalEpoch` @@ -66,49 +70,117 @@ theorem receipt_epoch_slot_is_solidity (user : Address) : structSlot HashedMappingExecSmoke.apr0Users.slot user.toNat 1 = (Compiler.Proofs.solidityMappingSlot 219 user.toNat + 1) % Compiler.Constants.evmModulus := rfl -/-! ## The executable plane is no longer opaque -/ +/-- The same slot is the interpretation of the symbolic entry +`mapChain 226 [user, epoch] 0` (`Compiler.Proofs.mappingChainSlotLocation`). -/ +theorem request_location_is_solidity (user : Address) (epoch : Uint256) : + Compiler.Proofs.mappingChainSlotLocation 226 [user.toNat, epoch.val] 0 = + Compiler.Proofs.solidityMappingSlot + (Compiler.Proofs.solidityMappingSlot 226 user.toNat) epoch.val := + Compiler.Proofs.mappingChainSlotLocation_zero _ _ _ + +/-! ## The executable plane: symbolic, separated by construction + +Every lemma below uses only `propext`, `Classical.choice` and `Quot.sound` +(see `PrintAxioms.lean`): no `solidityMappingSlot_injective`. -/ /-- A write through `setRequest` is visible to `requestOf` at the same keys. -/ theorem requestOf_after_setRequest (s : ContractState) (user : Address) (epoch amount : Uint256) : (Verity.bind (HashedMappingExecSmoke.setRequest user epoch amount) fun _ => HashedMappingExecSmoke.requestOf user epoch).run s = ContractResult.success amount - (s.writeSlot (mappingChainSlot 226 [↑user, ↑epoch]) amount) := by + (s.writeMapChain 226 [user.toNat, epoch.val] 0 amount) := by simp [HashedMappingExecSmoke.setRequest, HashedMappingExecSmoke.requestOf, HashedMappingExecSmoke.withdrawsRequestsByEpoch, Contract.run, Bind.bind, Pure.pure, Verity.bind, Verity.pure, setMappingN, getMappingN] -/-- `acquire` writes the transient channel only: persistent storage is untouched. -/ -theorem acquire_leaves_storage (s : ContractState) (lockId : Bytes32) (n : Nat) : +/-- Different keys never alias: key inequality, no keccak injectivity. -/ +theorem requestOf_other_after_setRequest (s : ContractState) (user user' : Address) + (epoch epoch' amount : Uint256) (h : user' ≠ user ∨ epoch' ≠ epoch) : + (Verity.bind (HashedMappingExecSmoke.setRequest user epoch amount) + fun _ => HashedMappingExecSmoke.requestOf user' epoch').run s = + ContractResult.success (s.readMapChain 226 [user'.toNat, epoch'.val] 0) + (s.writeMapChain 226 [user.toNat, epoch.val] 0 amount) := by + have hne : ¬ (user' = user ∧ epoch' = epoch) := by + rintro ⟨rfl, rfl⟩; rcases h with h | h <;> exact h rfl + simp [HashedMappingExecSmoke.setRequest, HashedMappingExecSmoke.requestOf, + HashedMappingExecSmoke.withdrawsRequestsByEpoch, Contract.run, Bind.bind, Pure.pure, + Verity.bind, Verity.pure, setMappingN, getMappingN, hne] + +/-- Mapping-vs-scalar separation: a nested-mapping write leaves the plain scalar +slot 206 (and every other scalar slot) untouched. Unprovable when the entry +lived in `.slot` at its keccak slot. -/ +theorem setRequest_leaves_scalar (s : ContractState) (user : Address) (epoch amount : Uint256) + (n : Nat) : + ((HashedMappingExecSmoke.setRequest user epoch amount).run s).getState.storage n = + s.storage n := by + simp [HashedMappingExecSmoke.setRequest, HashedMappingExecSmoke.withdrawsRequestsByEpoch, + Contract.run, setMappingN, ContractResult.getState] + +/-- ... and a scalar write at slot 206 leaves every hashed entry untouched. -/ +theorem requestOf_after_setWithdrawn (s : ContractState) (user : Address) + (epoch amount : Uint256) : + (Verity.bind (HashedMappingExecSmoke.setWithdrawn amount) + fun _ => HashedMappingExecSmoke.requestOf user epoch).run s = + ContractResult.success (s.readMapChain 226 [user.toNat, epoch.val] 0) + (s.writeSlot 206 amount) := by + simp [HashedMappingExecSmoke.setWithdrawn, HashedMappingExecSmoke.requestOf, + HashedMappingExecSmoke.withdrawsRequestsByEpoch, HashedMappingExecSmoke.withdrawn, + Contract.run, Bind.bind, Pure.pure, Verity.bind, Verity.pure, getMappingN, + Verity.setStorage] + +/-- `acquire` writes the transient channel only: persistent storage and persistent +hashed entries are untouched. -/ +theorem acquire_leaves_storage (s : ContractState) (lockId : Bytes32) (n : Nat) + (base : Nat) (keys : List Nat) (offset : Nat) : ∀ s', (HashedMappingExecSmoke.acquire lockId).run s = ContractResult.success () s' → - s'.storage n = s.storage n := by + s'.storage n = s.storage n ∧ + s'.readMapChain base keys offset = s.readMapChain base keys offset := by intro s' h simp [HashedMappingExecSmoke.acquire, HashedMappingExecSmoke.locks, Contract.run, setTransientMappingN] at h subst h - simp [ContractState.storage, ContractState.writeTransient] + simp /-- `locked` reads back what `acquire` wrote. -/ theorem locked_after_acquire (s : ContractState) (lockId : Bytes32) : (Verity.bind (HashedMappingExecSmoke.acquire lockId) fun _ => HashedMappingExecSmoke.locked lockId).run s = - ContractResult.success 1 (s.writeTransient (mappingChainSlot 1 [↑lockId]) 1) := by + ContractResult.success 1 (s.writeTransientMapChain 1 [lockId.val] 1) := by simp [HashedMappingExecSmoke.acquire, HashedMappingExecSmoke.locked, HashedMappingExecSmoke.locks, Contract.run, Bind.bind, Pure.pure, Verity.bind, Verity.pure, setTransientMappingN, getTransientMappingN] -/-- `structMembers` destructuring reads the hashed struct slots written by `setReceipt`. -/ +/-- `structMembers` destructuring reads the struct words written by `setReceipt`; +adjacent members are distinct entries by word offset. -/ theorem receiptOf_after_setReceipt (s : ContractState) (user : Address) (principal epoch : Uint256) : (Verity.bind (HashedMappingExecSmoke.setReceipt user principal epoch) fun _ => HashedMappingExecSmoke.receiptOf user).run s = ContractResult.success (principal, epoch) - ((s.writeSlot (structSlot 219 user.toNat 0) principal).writeSlot - (structSlot 219 user.toNat 1) epoch) := by - have hne : structSlot 219 user.toNat 0 ≠ structSlot 219 user.toNat 1 := - structSlot_ne_succ 219 user.toNat 0 + ((s.writeMapChain 219 [user.toNat] 0 principal).writeMapChain 219 [user.toNat] 1 epoch) := by simp [HashedMappingExecSmoke.setReceipt, HashedMappingExecSmoke.receiptOf, HashedMappingExecSmoke.structMember, HashedMappingExecSmoke.setStructMember, Contract.run, Bind.bind, Pure.pure, Verity.bind, Verity.pure, structMemberAt, - setStructMemberAt, hne] + setStructMemberAt] + +/-- Struct writes leave the nested mapping and the scalar slot untouched. -/ +theorem setReceipt_leaves_request_and_scalar (s : ContractState) (user user' : Address) + (principal epoch epoch' : Uint256) (n : Nat) : + let s' := ((HashedMappingExecSmoke.setReceipt user principal epoch).run s).getState + s'.readMapChain 226 [user'.toNat, epoch'.val] 0 = s.readMapChain 226 [user'.toNat, epoch'.val] 0 ∧ + s'.storage n = s.storage n := by + simp [HashedMappingExecSmoke.setReceipt, HashedMappingExecSmoke.setStructMember, + Contract.run, Bind.bind, Verity.bind, setStructMemberAt, ContractResult.getState] + +/-- Hop frame: a distinct-address callee running `setRequest` writes its own +namespaced entry; the caller's entries are unchanged after the hop. -/ +theorem hop_setRequest_frame (s : ContractState) (callee user : Address) + (epoch amount : Uint256) (h : s.thisAddress ≠ callee) (keys : List Nat) (offset : Nat) : + (Contract.hopCall callee (HashedMappingExecSmoke.setRequest user epoch amount) s).getState.readMapChain + 226 keys offset = s.readMapChain 226 keys offset := by + rw [Contract.hopCall_of_ne _ _ _ h] + simp only [HashedMappingExecSmoke.setRequest, HashedMappingExecSmoke.withdrawsRequestsByEpoch, + setMappingN, ContractResult.getState] + exact ContractState.readMapChain_exitHop_enterHop_of_frame _ _ _ _ _ _ _ + (ContractState.storageWords_scoped_writeMapChain _ _ _ _ _ _ _) end Contracts.Smoke diff --git a/PrintAxioms.lean b/PrintAxioms.lean index 152da4231d..cc799558ad 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -129,6 +129,7 @@ import Compiler.Proofs.Storage.FieldCoherence import Compiler.Proofs.Storage.FieldEncode import Compiler.Proofs.Storage.FieldPackedCompile import Compiler.Proofs.Storage.FieldStorageKey +import Compiler.Proofs.Storage.HashedMappingLayout import Compiler.Proofs.Storage.MappingCoherence import Compiler.Proofs.Storage.MappingCoherenceOn import Compiler.Proofs.Storage.MappingCoherentAllKeys @@ -5124,6 +5125,10 @@ end Verity.AxiomAudit Compiler.Proofs.abstractNestedMappingSlot_ne Compiler.Proofs.solidityMappingSlot_add_lt_evmModulus Compiler.Proofs.solidityMappingSlot_add_wordOffset_lt_evmModulus + Compiler.Proofs.mappingChainSlotLocation_single + Compiler.Proofs.mappingChainSlotLocation_pair + Compiler.Proofs.foldl_solidityMappingSlot_lt_evmModulus + Compiler.Proofs.mappingChainSlotLocation_zero -- Compiler/Proofs/Storage/FieldCoherence.lean Compiler.Proofs.Storage.FieldCoherence.fieldMapKey_coherent_storageKeySlot @@ -5187,6 +5192,19 @@ end Verity.AxiomAudit Compiler.Proofs.Storage.FieldStorageKey.packedExtract_eq_mod Compiler.Proofs.Storage.FieldStorageKey.fieldPackedExtract_eq_mod + -- Compiler/Proofs/Storage/HashedMappingLayout.lean + Compiler.Proofs.Storage.HashedMappingLayout.Entry.key_injective + Compiler.Proofs.Storage.HashedMappingLayout.layoutNonAlias_of_certificate + Compiler.Proofs.Storage.HashedMappingLayout.defaultState_hashedCoherentOn + Compiler.Proofs.Storage.HashedMappingLayout.read_eq_storage_location + Compiler.Proofs.Storage.HashedMappingLayout.alignedWrite_same + Compiler.Proofs.Storage.HashedMappingLayout.alignedWrite_preserves + Compiler.Proofs.Storage.HashedMappingLayout.writeSlot_preserves + Compiler.Proofs.Storage.HashedMappingLayout.writeTransient_preserves + Compiler.Proofs.Storage.HashedMappingLayout.writeTransientMapChain_preserves + Compiler.Proofs.Storage.HashedMappingLayout.writeAddrSlot_preserves + Compiler.Proofs.Storage.HashedMappingLayout.alignedTransientWrite_preserves + -- Compiler/Proofs/Storage/MappingCoherence.lean Compiler.Proofs.Storage.MappingCoherence.defaultState_mappingCoherent Compiler.Proofs.Storage.MappingCoherence.writeMap_aligned_same @@ -5204,6 +5222,8 @@ end Verity.AxiomAudit Compiler.Proofs.Storage.MappingCoherence.writeMap2_aligned_same Compiler.Proofs.Storage.MappingCoherence.writeMap2_aligned_other Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_mapUint + Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_mapChain + Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_transientMapChain Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_map2 Compiler.Proofs.Storage.MappingCoherence.addressToWord_injective Compiler.Proofs.Storage.MappingCoherence.mappingAddrSlot_ne_of_map_ne @@ -7599,4 +7619,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 7019 theorems/lemmas (5006 public, 2013 private, 0 sorry'd) +-- Total: 7036 theorems/lemmas (5023 public, 2013 private, 0 sorry'd) diff --git a/Verity/Core.lean b/Verity/Core.lean index 3e8670b219..7a071d4d68 100644 --- a/Verity/Core.lean +++ b/Verity/Core.lean @@ -276,8 +276,22 @@ inductive StorageKey where | map (slot : Nat) (key : Address) | mapUint (slot : Nat) (key : Uint256) | map2 (slot : Nat) (key1 key2 : Address) + /-- Hashed mapping-chain word (nested mappings, word-offset mapping values, + struct mappings): word `offset` of the value stored under the key path + `keys` of the mapping rooted at base slot `slot`. Key words are the ABI + words of the keys (`Address.toNat`, `Uint256.val`), outermost first. + Separation between entries is constructor injectivity on + `(slot, keys, offset)`; the Solidity keccak slot + `(fold keccak256(key ‖ acc) + offset) mod 2^256` is only an + interpretation (`Compiler.Proofs.mappingChainSlotLocation`, + `Compiler.Proofs.Storage.HashedMappingLayout`). -/ + | mapChain (slot : Nat) (keys : List Nat) (offset : Nat) + /-- Transient (EIP-1153) hashed mapping-chain word: the value stored under + `keys` of the transient mapping rooted at `slot`. -/ + | transientMapChain (slot : Nat) (keys : List Nat) /-- Parked copy of a non-slot channel key (`addr` / `transient` / `map` / - `mapUint` / `map2`) belonging to contract `contract`. Hops + `mapUint` / `map2` / `mapChain` / `transientMapChain`) belonging to + contract `contract`. Hops (`ContractState.switchSlotWorld`) park the caller's plain non-slot world here and load the callee's, exactly as `contractSlot` does for `.slot`. -/ | scoped (contract : Nat) (key : StorageKey) @@ -288,9 +302,24 @@ namespace StorageKey /-- Plain (unparked) non-slot channel keys: the keys that hops namespace via `scoped`. `slot` is namespaced via `contractSlot` instead. -/ def isPlainNonSlot : StorageKey → Bool - | .addr _ | .transient _ | .map _ _ | .mapUint _ _ | .map2 _ _ _ => true + | .addr _ | .transient _ | .map _ _ | .mapUint _ _ | .map2 _ _ _ + | .mapChain _ _ _ | .transientMapChain _ _ => true | .slot _ | .contractSlot _ _ | .scoped _ _ => false +@[simp] theorem slot_ne_mapChain (n m : Nat) (ks : List Nat) (o : Nat) : + slot n ≠ mapChain m ks o := by intro h; cases h +@[simp] theorem mapChain_ne_slot (m : Nat) (ks : List Nat) (o n : Nat) : + mapChain m ks o ≠ slot n := by intro h; cases h +@[simp] theorem transient_ne_transientMapChain (n m : Nat) (ks : List Nat) : + transient n ≠ transientMapChain m ks := by intro h; cases h +@[simp] theorem transientMapChain_ne_transient (m : Nat) (ks : List Nat) (n : Nat) : + transientMapChain m ks ≠ transient n := by intro h; cases h +@[simp] theorem mapChain_ne_transientMapChain (m : Nat) (ks : List Nat) (o n : Nat) + (ks' : List Nat) : mapChain m ks o ≠ transientMapChain n ks' := by intro h; cases h +@[simp] theorem transientMapChain_ne_mapChain (n : Nat) (ks' : List Nat) (m : Nat) + (ks : List Nat) (o : Nat) : transientMapChain n ks' ≠ mapChain m ks o := by + intro h; cases h + @[simp] theorem slot_ne_scoped (n c : Nat) (k : StorageKey) : slot n ≠ StorageKey.scoped c k := by intro h; cases h @[simp] theorem scoped_ne_slot (c : Nat) (k : StorageKey) (n : Nat) : StorageKey.scoped c k ≠ slot n := by intro h; cases h @[simp] theorem contractSlot_ne_scoped (c n d : Nat) (k : StorageKey) : @@ -476,7 +505,8 @@ def withStorageWords (s : ContractState) (f : StorageKey → Uint256) : Contract /-- Park the current plain storage world under `parkId` and load `loadId`'s parked world into the plain keys. Every word-valued channel is namespaced: `.slot n` is parked under `.contractSlot id n`, and every plain non-slot - key `k` (`addr` / `transient` / `map` / `mapUint` / `map2`) under + key `k` (`addr` / `transient` / `map` / `mapUint` / `map2` / `mapChain` / + `transientMapChain`) under `.scoped id k`. Parked worlds of contracts other than `parkId` are left unchanged. `storageArray` (a separate field) is NOT namespaced and stays global across hops. Swapping the ids restores the plain world. -/ @@ -1024,6 +1054,366 @@ theorem exitHop_enterHop_storageWords_plain (s : ContractState) (caller callee : enterHop_scoped_caller _ _ _ k hk] · simp [exitHop, enterHop, switchSlotWorld] +/-! ### Hashed mapping-chain channel (G2 residual, #2432 follow-up) + +`getMappingN` / `setMappingN`, `getMappingWord` / `setMappingWord` and the +struct-mapping accessors (`structMemberAt`, `structMember2At`, +`setStructMemberAt`, `setStructMember2At`, `structMembers` destructuring) +store their words under `StorageKey.mapChain slot keys offset`; transient +mapping chains under `StorageKey.transientMapChain slot keys`. Two entries are +independent iff their `(slot, keys, offset)` differ — constructor +injectivity, no keccak collision-resistance — and neither channel ever +touches the scalar `.slot` channel. The Solidity keccak layout is an +interpretation (`Compiler.Proofs.Storage.HashedMappingLayout`), not the +executable representation. Both keys are plain non-slot keys, so hops +namespace them per contract via `StorageKey.scoped`, and `Contract.run` +rollback restores them with the rest of `storageWords`. -/ + +/-- View of the hashed mapping-chain channel. -/ +def storageMapChain (s : ContractState) : Nat → List Nat → Nat → Uint256 := + fun slot keys offset => s.storageWords (.mapChain slot keys offset) + +/-- View of the transient hashed mapping-chain channel. -/ +def transientStorageMapChain (s : ContractState) : Nat → List Nat → Uint256 := + fun slot keys => s.storageWords (.transientMapChain slot keys) + +/-- Read word `offset` under key path `keys` of the mapping rooted at `slot`. -/ +def readMapChain (s : ContractState) (slot : Nat) (keys : List Nat) (offset : Nat) : + Uint256 := + s.storageMapChain slot keys offset + +/-- Write word `offset` under key path `keys` of the mapping rooted at `slot`. -/ +def writeMapChain (s : ContractState) (slot : Nat) (keys : List Nat) (offset : Nat) + (value : Uint256) : ContractState := + s.withStorageWords fun key => + if key == .mapChain slot keys offset then value else s.storageWords key + +/-- Read the transient word under key path `keys` of the transient mapping at `slot`. -/ +def readTransientMapChain (s : ContractState) (slot : Nat) (keys : List Nat) : Uint256 := + s.transientStorageMapChain slot keys + +/-- Write the transient word under key path `keys` of the transient mapping at `slot`. -/ +def writeTransientMapChain (s : ContractState) (slot : Nat) (keys : List Nat) + (value : Uint256) : ContractState := + s.withStorageWords fun key => + if key == .transientMapChain slot keys then value else s.storageWords key + +theorem storageMapChain_unfold (s : ContractState) : + s.storageMapChain = fun n keys offset => s.storageWords (.mapChain n keys offset) := rfl +theorem transientStorageMapChain_unfold (s : ContractState) : + s.transientStorageMapChain = fun n keys => s.storageWords (.transientMapChain n keys) := rfl + +theorem storageWords_mapChain (s : ContractState) (slot : Nat) (keys : List Nat) + (offset : Nat) : s.storageWords (.mapChain slot keys offset) = s.readMapChain slot keys offset := + rfl + +theorem storageWords_transientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) : + s.storageWords (.transientMapChain slot keys) = s.readTransientMapChain slot keys := + rfl + +@[simp] theorem storageWords_writeMapChain (s : ContractState) (slot : Nat) (keys : List Nat) + (offset : Nat) (value : Uint256) (key : StorageKey) : + (s.writeMapChain slot keys offset value).storageWords key = + if key = .mapChain slot keys offset then value else s.storageWords key := by + simp [writeMapChain] + +@[simp] theorem storageWords_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) (key : StorageKey) : + (s.writeTransientMapChain slot keys value).storageWords key = + if key = .transientMapChain slot keys then value else s.storageWords key := by + simp [writeTransientMapChain] + +/-! Read-after-write: same entry, and a general form that `simp` discharges +by deciding `slot' = slot ∧ keys' = keys ∧ offset' = offset`. -/ + +@[simp, storage_simps] theorem readMapChain_writeMapChain_same (s : ContractState) + (slot : Nat) (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).readMapChain slot keys offset = value := by + simp [readMapChain, storageMapChain, writeMapChain] + +@[simp, storage_simps] theorem readMapChain_writeMapChain (s : ContractState) + (slot : Nat) (keys : List Nat) (offset : Nat) (value : Uint256) + (slot' : Nat) (keys' : List Nat) (offset' : Nat) : + (s.writeMapChain slot keys offset value).readMapChain slot' keys' offset' = + if slot' = slot ∧ keys' = keys ∧ offset' = offset then value + else s.readMapChain slot' keys' offset' := by + simp [readMapChain, storageMapChain, writeMapChain] + +theorem readMapChain_writeMapChain_of_ne (s : ContractState) + {slot slot' : Nat} {keys keys' : List Nat} {offset offset' : Nat} + (h : StorageKey.mapChain slot' keys' offset' ≠ .mapChain slot keys offset) + (value : Uint256) : + (s.writeMapChain slot keys offset value).readMapChain slot' keys' offset' = + s.readMapChain slot' keys' offset' := by + simp only [readMapChain, storageMapChain, writeMapChain, storageWords_withStorageWords] + simp [h] + +/-- Different key paths never alias (key-path inequality, no hashing). -/ +theorem readMapChain_writeMapChain_keys_ne (s : ContractState) + {slot slot' : Nat} {keys keys' : List Nat} {offset offset' : Nat} + (h : keys' ≠ keys) (value : Uint256) : + (s.writeMapChain slot keys offset value).readMapChain slot' keys' offset' = + s.readMapChain slot' keys' offset' := + readMapChain_writeMapChain_of_ne s (by intro hk; cases hk; exact h rfl) value + +/-- Different word offsets (struct members) never alias. -/ +theorem readMapChain_writeMapChain_offset_ne (s : ContractState) + {slot slot' : Nat} {keys keys' : List Nat} {offset offset' : Nat} + (h : offset' ≠ offset) (value : Uint256) : + (s.writeMapChain slot keys offset value).readMapChain slot' keys' offset' = + s.readMapChain slot' keys' offset' := + readMapChain_writeMapChain_of_ne s (by intro hk; cases hk; exact h rfl) value + +/-- Different base slots (different mapping fields) never alias. -/ +theorem readMapChain_writeMapChain_slot_ne (s : ContractState) + {slot slot' : Nat} {keys keys' : List Nat} {offset offset' : Nat} + (h : slot' ≠ slot) (value : Uint256) : + (s.writeMapChain slot keys offset value).readMapChain slot' keys' offset' = + s.readMapChain slot' keys' offset' := + readMapChain_writeMapChain_of_ne s (by intro hk; cases hk; exact h rfl) value + +@[simp, storage_simps] theorem readTransientMapChain_writeTransientMapChain_same + (s : ContractState) (slot : Nat) (keys : List Nat) (value : Uint256) : + (s.writeTransientMapChain slot keys value).readTransientMapChain slot keys = value := by + simp [readTransientMapChain, transientStorageMapChain, writeTransientMapChain] + +@[simp, storage_simps] theorem readTransientMapChain_writeTransientMapChain + (s : ContractState) (slot : Nat) (keys : List Nat) (value : Uint256) + (slot' : Nat) (keys' : List Nat) : + (s.writeTransientMapChain slot keys value).readTransientMapChain slot' keys' = + if slot' = slot ∧ keys' = keys then value else s.readTransientMapChain slot' keys' := by + simp [readTransientMapChain, transientStorageMapChain, writeTransientMapChain] + +/-! Independence from every other channel. The hashed channel never writes a +scalar `.slot`, and scalar / address / simple-mapping / transient writes never +touch it. Mapping-vs-scalar separation (e.g. `receipts[user][epoch]` vs a plain +slot 206) is therefore constructor inequality, not a keccak fact. -/ + +@[simp, storage_simps] theorem storage_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).storage = s.storage := by + funext n; simp [storage, writeMapChain] + +@[simp, storage_simps] theorem readSlot_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) (n : Nat) : + (s.writeMapChain slot keys offset value).readSlot n = s.readSlot n := by + simp [readSlot, storage, writeMapChain] + +@[simp] theorem storageAddr_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).storageAddr = s.storageAddr := by + funext n; simp [storageAddr, writeMapChain] + +@[simp] theorem transientStorage_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).transientStorage = s.transientStorage := by + funext n; simp [transientStorage, writeMapChain] + +@[simp] theorem storageMap_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).storageMap = s.storageMap := by + funext n k; simp [storageMap, writeMapChain] + +@[simp] theorem storageMapUint_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).storageMapUint = s.storageMapUint := by + funext n k; simp [storageMapUint, writeMapChain] + +@[simp] theorem storageMap2_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).storageMap2 = s.storageMap2 := by + funext n k1 k2; simp [storageMap2, writeMapChain] + +@[simp] theorem transientStorageMapChain_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).transientStorageMapChain = + s.transientStorageMapChain := by + funext n ks; simp [transientStorageMapChain, writeMapChain] + +@[simp] theorem readTransientMapChain_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) (slot' : Nat) (keys' : List Nat) : + (s.writeMapChain slot keys offset value).readTransientMapChain slot' keys' = + s.readTransientMapChain slot' keys' := by + simp [readTransientMapChain, transientStorageMapChain, writeMapChain] + +@[simp] theorem storage_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) : + (s.writeTransientMapChain slot keys value).storage = s.storage := by + funext n; simp [storage, writeTransientMapChain] + +@[simp] theorem readSlot_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) (n : Nat) : + (s.writeTransientMapChain slot keys value).readSlot n = s.readSlot n := by + simp [readSlot, storage, writeTransientMapChain] + +@[simp] theorem transientStorage_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) : + (s.writeTransientMapChain slot keys value).transientStorage = s.transientStorage := by + funext n; simp [transientStorage, writeTransientMapChain] + +@[simp] theorem storageMapChain_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) : + (s.writeTransientMapChain slot keys value).storageMapChain = s.storageMapChain := by + funext n ks o; simp [storageMapChain, writeTransientMapChain] + +@[simp] theorem readMapChain_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) (slot' : Nat) (keys' : List Nat) (offset' : Nat) : + (s.writeTransientMapChain slot keys value).readMapChain slot' keys' offset' = + s.readMapChain slot' keys' offset' := by + simp [readMapChain, storageMapChain, writeTransientMapChain] + +@[simp, storage_simps] theorem readMapChain_writeSlot (s : ContractState) (n : Nat) + (v : Uint256) (slot : Nat) (keys : List Nat) (offset : Nat) : + (s.writeSlot n v).readMapChain slot keys offset = s.readMapChain slot keys offset := by + simp [readMapChain, storageMapChain, writeSlot] + +@[simp] theorem readMapChain_writeAddrSlot (s : ContractState) (n : Nat) + (v : Address) (slot : Nat) (keys : List Nat) (offset : Nat) : + (s.writeAddrSlot n v).readMapChain slot keys offset = s.readMapChain slot keys offset := by + simp [readMapChain, storageMapChain, writeAddrSlot] + +@[simp] theorem readMapChain_writeTransient (s : ContractState) (n : Nat) + (v : Uint256) (slot : Nat) (keys : List Nat) (offset : Nat) : + (s.writeTransient n v).readMapChain slot keys offset = s.readMapChain slot keys offset := by + simp [readMapChain, storageMapChain, writeTransient] + +@[simp] theorem readMapChain_writeMap (s : ContractState) (n : Nat) (k : Address) + (v : Uint256) (slot : Nat) (keys : List Nat) (offset : Nat) : + (s.writeMap n k v).readMapChain slot keys offset = s.readMapChain slot keys offset := by + simp [readMapChain, storageMapChain, writeMap] + +@[simp] theorem readMapChain_writeMapUint (s : ContractState) (n : Nat) (k : Uint256) + (v : Uint256) (slot : Nat) (keys : List Nat) (offset : Nat) : + (s.writeMapUint n k v).readMapChain slot keys offset = s.readMapChain slot keys offset := by + simp [readMapChain, storageMapChain, writeMapUint] + +@[simp] theorem readMapChain_writeMap2 (s : ContractState) (n : Nat) (k1 k2 : Address) + (v : Uint256) (slot : Nat) (keys : List Nat) (offset : Nat) : + (s.writeMap2 n k1 k2 v).readMapChain slot keys offset = s.readMapChain slot keys offset := by + simp [readMapChain, storageMapChain, writeMap2] + +@[simp] theorem readTransientMapChain_writeSlot (s : ContractState) (n : Nat) + (v : Uint256) (slot : Nat) (keys : List Nat) : + (s.writeSlot n v).readTransientMapChain slot keys = s.readTransientMapChain slot keys := by + simp [readTransientMapChain, transientStorageMapChain, writeSlot] + +@[simp] theorem readTransientMapChain_writeTransient (s : ContractState) (n : Nat) + (v : Uint256) (slot : Nat) (keys : List Nat) : + (s.writeTransient n v).readTransientMapChain slot keys = + s.readTransientMapChain slot keys := by + simp [readTransientMapChain, transientStorageMapChain, writeTransient] + +@[simp] theorem storageArray_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) : + (s.writeMapChain slot keys offset value).storageArray = s.storageArray := rfl +@[simp] theorem storageArray_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) : + (s.writeTransientMapChain slot keys value).storageArray = s.storageArray := rfl + +/-! Non-storage fields are untouched by both hashed-chain writes. -/ +section MapChainContext +variable (s : ContractState) (slot : Nat) (keys : List Nat) (offset : Nat) (value : Uint256) +@[simp] theorem sender_writeMapChain : + (s.writeMapChain slot keys offset value).sender = s.sender := rfl +@[simp] theorem thisAddress_writeMapChain : + (s.writeMapChain slot keys offset value).thisAddress = s.thisAddress := rfl +@[simp] theorem txOrigin_writeMapChain : + (s.writeMapChain slot keys offset value).txOrigin = s.txOrigin := rfl +@[simp] theorem msgValue_writeMapChain : + (s.writeMapChain slot keys offset value).msgValue = s.msgValue := rfl +@[simp] theorem selfBalance_writeMapChain : + (s.writeMapChain slot keys offset value).selfBalance = s.selfBalance := rfl +@[simp] theorem blockTimestamp_writeMapChain : + (s.writeMapChain slot keys offset value).blockTimestamp = s.blockTimestamp := rfl +@[simp] theorem blockNumber_writeMapChain : + (s.writeMapChain slot keys offset value).blockNumber = s.blockNumber := rfl +@[simp] theorem chainId_writeMapChain : + (s.writeMapChain slot keys offset value).chainId = s.chainId := rfl +@[simp] theorem knownAddresses_writeMapChain : + (s.writeMapChain slot keys offset value).knownAddresses = s.knownAddresses := rfl +@[simp] theorem events_writeMapChain : + (s.writeMapChain slot keys offset value).events = s.events := rfl +@[simp] theorem calls_writeMapChain : + (s.writeMapChain slot keys offset value).calls = s.calls := rfl +@[simp] theorem returndata_writeMapChain : + (s.writeMapChain slot keys offset value).returndata = s.returndata := rfl +@[simp] theorem sender_writeTransientMapChain : + (s.writeTransientMapChain slot keys value).sender = s.sender := rfl +@[simp] theorem thisAddress_writeTransientMapChain : + (s.writeTransientMapChain slot keys value).thisAddress = s.thisAddress := rfl +@[simp] theorem msgValue_writeTransientMapChain : + (s.writeTransientMapChain slot keys value).msgValue = s.msgValue := rfl +@[simp] theorem events_writeTransientMapChain : + (s.writeTransientMapChain slot keys value).events = s.events := rfl +@[simp] theorem calls_writeTransientMapChain : + (s.writeTransientMapChain slot keys value).calls = s.calls := rfl +@[simp] theorem returndata_writeTransientMapChain : + (s.writeTransientMapChain slot keys value).returndata = s.returndata := rfl +end MapChainContext + +/-! Hop namespacing of the hashed channels: a distinct-address callee sees its +own hashed entries (`.scoped callee`), the caller's are parked under +`.scoped caller`, and hashed writes never touch any parked world. -/ + +theorem enterHop_readMapChain (s : ContractState) (caller callee : Address) (slot : Nat) + (keys : List Nat) (offset : Nat) : + (s.enterHop caller callee).readMapChain slot keys offset = + s.storageWords (.scoped callee.toNat (.mapChain slot keys offset)) := + rfl + +theorem enterHop_readTransientMapChain (s : ContractState) (caller callee : Address) + (slot : Nat) (keys : List Nat) : + (s.enterHop caller callee).readTransientMapChain slot keys = + s.storageWords (.scoped callee.toNat (.transientMapChain slot keys)) := + rfl + +theorem exitHop_readMapChain (snap s' : ContractState) (caller callee : Address) + (slot : Nat) (keys : List Nat) (offset : Nat) : + (snap.exitHop s' caller callee).readMapChain slot keys offset = + s'.storageWords (.scoped caller.toNat (.mapChain slot keys offset)) := + rfl + +theorem exitHop_readTransientMapChain (snap s' : ContractState) (caller callee : Address) + (slot : Nat) (keys : List Nat) : + (snap.exitHop s' caller callee).readTransientMapChain slot keys = + s'.storageWords (.scoped caller.toNat (.transientMapChain slot keys)) := + rfl + +@[simp] theorem storageWords_scoped_writeMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (offset : Nat) (value : Uint256) (c : Nat) (k : StorageKey) : + (s.writeMapChain slot keys offset value).storageWords (.scoped c k) = + s.storageWords (.scoped c k) := by + simp [writeMapChain] + +@[simp] theorem storageWords_scoped_writeTransientMapChain (s : ContractState) (slot : Nat) + (keys : List Nat) (value : Uint256) (c : Nat) (k : StorageKey) : + (s.writeTransientMapChain slot keys value).storageWords (.scoped c k) = + s.storageWords (.scoped c k) := by + simp [writeTransientMapChain] + +/-- Hop frame: if the callee body leaves the caller's parked hashed entry + alone, the caller reads the same hashed entry after the hop. -/ +theorem readMapChain_exitHop_enterHop_of_frame (s s' : ContractState) + (caller callee : Address) (slot : Nat) (keys : List Nat) (offset : Nat) + (hframe : s'.storageWords (.scoped caller.toNat (.mapChain slot keys offset)) = + (s.enterHop caller callee).storageWords (.scoped caller.toNat (.mapChain slot keys offset))) : + (s.exitHop s' caller callee).readMapChain slot keys offset = + s.readMapChain slot keys offset := by + rw [exitHop_readMapChain, hframe, enterHop_scoped_caller _ _ _ _ rfl] + rfl + +/-- The callee's hashed writes land in its own namespace: after entering a hop + and writing an entry, the caller's parked world is unchanged. -/ +theorem writeMapChain_enterHop_frame (s : ContractState) (caller callee : Address) + (slot : Nat) (keys : List Nat) (offset : Nat) (value : Uint256) + (slot' : Nat) (keys' : List Nat) (offset' : Nat) : + (((s.enterHop caller callee).writeMapChain slot keys offset value).storageWords + (.scoped caller.toNat (.mapChain slot' keys' offset'))) = + s.readMapChain slot' keys' offset' := by + rw [storageWords_scoped_writeMapChain, enterHop_scoped_caller _ _ _ _ rfl] + rfl + @[simp] theorem storage_writeMap2 (s : ContractState) (slot : Nat) (key1 key2 : Address) (value : Uint256) : (s.writeMap2 slot key1 key2 value).storage = s.storage := by funext wordSlot @@ -1092,6 +1482,10 @@ def writeArray (s : ContractState) (slot : Nat) (values : List Uint256) : Contra (value : Uint256) : (s.writeSlot slot value).storageArray = s.storageArray := rfl +@[simp] theorem readMapChain_writeArray (s : ContractState) (n : Nat) (vs : List Uint256) + (slot : Nat) (keys : List Nat) (offset : Nat) : + (s.writeArray n vs).readMapChain slot keys offset = s.readMapChain slot keys offset := rfl + /-! ### Bulk lenses (C5) @@ -1465,7 +1859,9 @@ def ofChannels (sender : Address := 0) (thisAddress : Address := 0) (msgValue : Uint256 := 0) - (blockTimestamp : Uint256 := 0) : ContractState := + (blockTimestamp : Uint256 := 0) + (mapChainChannel : Nat → List Nat → Nat → Uint256 := fun _ _ _ => 0) + (transientMapChainChannel : Nat → List Nat → Uint256 := fun _ _ => 0) : ContractState := { storageWords := fun key => match key with | .slot slot => uintChannel slot | .contractSlot _ _ => 0 @@ -1475,6 +1871,8 @@ def ofChannels | .map slot key => mapChannel slot key | .mapUint slot key => mapUintChannel slot key | .map2 slot key1 key2 => map2Channel slot key1 key2 + | .mapChain slot keys offset => mapChainChannel slot keys offset + | .transientMapChain slot keys => transientMapChainChannel slot keys storageArray := arrayChannel sender := sender thisAddress := thisAddress diff --git a/artifacts/macro_property_tests/PropertyHashedMappingExecSmoke.t.sol b/artifacts/macro_property_tests/PropertyHashedMappingExecSmoke.t.sol index 3fcb3ac159..e3a30f6162 100644 --- a/artifacts/macro_property_tests/PropertyHashedMappingExecSmoke.t.sol +++ b/artifacts/macro_property_tests/PropertyHashedMappingExecSmoke.t.sol @@ -49,13 +49,19 @@ contract PropertyHashedMappingExecSmokeTest is YulTestBase { // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem. ret; } - // Property 5: setReceipt has no unexpected revert + // Property 5: setWithdrawn has no unexpected revert + function testAuto_SetWithdrawn_NoUnexpectedRevert() public { + vm.prank(alice); + (bool ok,) = target.call(abi.encodeWithSignature("setWithdrawn(uint256)", uint256(1))); + require(ok, "setWithdrawn reverted unexpectedly"); + } + // Property 6: setReceipt has no unexpected revert function testAuto_SetReceipt_NoUnexpectedRevert() public { vm.prank(alice); (bool ok,) = target.call(abi.encodeWithSignature("setReceipt(address,uint256,uint256)", alice, uint256(1), uint256(1))); require(ok, "setReceipt reverted unexpectedly"); } - // Property 6: TODO decode and assert `receiptOf` result + // Property 7: TODO decode and assert `receiptOf` result function testTODO_ReceiptOf_DecodeAndAssert() public { vm.prank(alice); (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("receiptOf(address)", alice)); diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json index 8ef8e8ed64..015a9839c3 100644 --- a/artifacts/verification_status.json +++ b/artifacts/verification_status.json @@ -1,6 +1,6 @@ { "codebase": { - "core_lines": 2412, + "core_lines": 2810, "example_contracts": 19 }, "proofs": { diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index e2da1c067e..7d7898a3a6 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -31,7 +31,7 @@ Every transition inside the proof envelope is either fully verified or recorded - **Language**: Lean 4.31.0 -- **Core Size**: 2412 lines +- **Core Size**: 2810 lines - **Verified Contracts**: 15 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault) - **Theorems**: 329 across 15 categories, 329 fully proven - **Axioms**: 1 documented Lean axioms (see docs/AXIOMS.md) diff --git a/docs/AXIOMS.md b/docs/AXIOMS.md index d2bc6fb202..f5fe526d3f 100644 --- a/docs/AXIOMS.md +++ b/docs/AXIOMS.md @@ -28,7 +28,10 @@ C5 step 3 (`ContractState.storageWords` over injective `StorageKey`) does not add a keccak-injectivity axiom. Source lens laws use constructor injectivity; Solidity slot derivation remains compiler-side. The G24 hop namespace constructor `StorageKey.scoped` (#2440) likewise adds no axiom: -its hop lemmas are definitional or constructor case splits. +its hop lemmas are definitional or constructor case splits. The hashed +mapping-chain constructors `StorageKey.mapChain` / `transientMapChain` +(G2 residual) likewise add no axiom and make nested / struct mapping +separation a constructor fact. C5 step 4 is complete under `solidityMappingSlot_injective` below — collision-resistance of the 64-byte ABI mapping preimage, **not** @@ -103,6 +106,13 @@ listed-pair certificates remain valid without the axiom. - `DOCUMENTED_AXIOMS` in that script - Kernel Keccak output is already cross-checked against FFI/EVM keccak +**Not used by hashed mapping chains**: nested / word-offset / struct +mappings (`getMappingN`, `getMappingWord`, `structMember*`) execute on the +symbolic `StorageKey.mapChain` channel, so their executable-plane separation is +constructor injectivity. Their Solidity-layout interpretation +(`Compiler/Proofs/Storage/HashedMappingLayout.lean`) takes a finite +`LayoutNonAlias` certificate as a hypothesis instead of this axiom. + **Elimination path**: Replace with a theorem if a restricted-domain injectivity proof becomes available, or keep as an explicit cryptographic assumption diff --git a/docs/PARETO_MODEL_SUPPORT.md b/docs/PARETO_MODEL_SUPPORT.md index aed5ce2a4f..7afe959e41 100644 --- a/docs/PARETO_MODEL_SUPPORT.md +++ b/docs/PARETO_MODEL_SUPPORT.md @@ -228,55 +228,74 @@ the executable plane read `0` from every `getMappingN` and dropped every A mixed key list (`[user, epoch]` with an `Address` and a `Uint256`) did not even typecheck. -**Slot model.** `Contracts.getMappingN` / `setMappingN` / -`getMappingWord` / `setMappingWord` now read and write -`ContractState.storage` at the Solidity slot, sharing the proof model's +**Storage model.** `Contracts.getMappingN` / `setMappingN` / +`getMappingWord` / `setMappingWord` and the struct-mapping accessors read and +write a dedicated symbolic channel of `ContractState`, +`StorageKey.mapChain baseSlot keyWords wordOffset` +(`ContractState.readMapChain` / `writeMapChain`). Separation is constructor +injectivity: different keys, different struct members, different fields, and +a mapping entry vs a plain scalar slot never alias, with no keccak +assumption (G2 residual, follow-up to #2432). The Solidity slot below is the +*interpretation* of each entry, shared with the proof model's `Compiler.Proofs.abstractMappingSlot` (`keccak256(key ‖ slot)`): -| Solidity | Executable slot | -|----------|-----------------| -| `m[k]` at `p` | `keccak256(k ‖ p)` (`mappingChainSlot p [k]`) | -| `m[k₁][k₂]` at `p` | `keccak256(k₂ ‖ keccak256(k₁ ‖ p))` (`mappingChainSlot p [k₁, k₂]`) | -| `m[k].member` at `p`, word `w` | `(keccak256(k ‖ p) + w) mod 2²⁵⁶` (`structSlot p k w`) | -| `m[k₁][k₂].member` | `(keccak256(k₂ ‖ keccak256(k₁ ‖ p)) + w) mod 2²⁵⁶` (`structSlot2`) | - -`mappingChainSlot_single` / `_pair`, `structSlot_eq_mappingSlotLocation` and +| Solidity | Symbolic entry | Solidity slot (interpretation) | +|----------|----------------|--------------------------------| +| `m[k]` at `p` | `mapChain p [k] 0` | `keccak256(k ‖ p)` (`mappingChainSlot p [k]`) | +| `m[k₁][k₂]` at `p` | `mapChain p [k₁, k₂] 0` | `keccak256(k₂ ‖ keccak256(k₁ ‖ p))` | +| `m[k].member` at `p`, word `w` | `mapChain p [k] w` | `(keccak256(k ‖ p) + w) mod 2²⁵⁶` (`structSlot p k w`) | +| `m[k₁][k₂].member` | `mapChain p [k₁, k₂] w` | `(keccak256(k₂ ‖ keccak256(k₁ ‖ p)) + w) mod 2²⁵⁶` (`structSlot2`) | + +All rows are `Compiler.Proofs.mappingChainSlotLocation p keys w` +(`mappingChainSlot_eq_location`, `structSlot_eq_location`, +`structSlot2_eq_location`), and `mappingChainSlot_single` / `_pair`, +`structSlot_eq_mappingSlotLocation` and `structSlot2_eq_nestedMappingSlotLocation` are `rfl` against the compiler's -`MappingSlot` definitions, so the executable plane, the model plane -(`DenoteOracle.mappingSlot`) and the Yul lowering derive the same slot. +`MappingSlot` definitions. `Compiler.Proofs.Storage.HashedMappingLayout` +relates the executable channel to the flat `.slot` channel the model plane +reads (`HashedCoherentOn`, preserved by aligned writes under a finite +`LayoutNonAlias` certificate), without `solidityMappingSlot_injective`. **Keys.** `getMappingN` / `setMappingN` take a `List MappingKeyWord`; `Address`, `Uint256` and `Bytes32` coerce through `StorageKey.toWord`, so `getMappingN withdrawsRequestsByEpoch [user, epoch]` typechecks. **Transient chains.** A `transient` mapping chain routes to -`getTransientMappingN` / `setTransientMappingN` (EIP-1153 channel); the -macro inserts the rewrite, matching `readFieldWord` in the model plane. +`getTransientMappingN` / `setTransientMappingN`, which use +`StorageKey.transientMapChain baseSlot keyWords` (EIP-1153; cleared by the +import harness' `beginTransaction` like `.transient`); the macro inserts the +rewrite, matching `readFieldWord` in the model plane. **`structMembers`.** `let (a, b) := structMembers f k [m₁, m₂]` and `return structMembers f k [..]` lower to one generated `structMember` read per member in the executable plane. The pure expression form elsewhere is still the `default` stub. -**Channels.** This hashed channel is disjoint from the constructor-keyed -`storageMap` / `storageMapUint` / `storageMap2` channels behind -`getMapping` / `getMappingUint` / `getMapping2`. A field is accessed through -exactly one family, chosen by its declared storage type, so no contract -observes both channels for one slot. +**Channels.** The hashed channel is disjoint from the scalar `.slot` +channel and from the constructor-keyed `storageMap` / `storageMapUint` / +`storageMap2` channels behind `getMapping` / `getMappingUint` / +`getMapping2`. A field is accessed through exactly one family, chosen by its +declared storage type, so no contract observes two channels for one slot. +Both hashed keys are plain non-slot keys: distinct-address hops +(`enterHop` / `exitHop`, `hopCall`, `hopCallView`) park and load them per +contract via `StorageKey.scoped`, and revert rollback restores them. **Proofs.** `Contracts/Smoke/HashedMappings.lean` proves, through the -generated functions, that a nested-mapping write is read back at the same -keys, that a struct receipt destructures to the written words, that a -transient lock is read back and leaves persistent storage untouched, and -that the slots are the Solidity slots. Adjacent struct words are distinct -without keccak reasoning (`structSlot_ne_succ`); distinct keys rely on the -existing `solidityMappingSlot_injective` axiom. No new axioms. - -**Alternative considered.** A new `StorageKey.hashed` constructor would keep -keys symbolic but breaks every exhaustive match on `StorageKey` (EVMYulLean -bridges, lens laws) and still needs a keccak-parity story for the compiler. -Reusing the `.slot` channel is what the generated struct-mapping accessors -already did; this feature extends it to chains and words. +generated functions and using only `propext` / `Classical.choice` / +`Quot.sound`, that a nested-mapping write is read back at the same keys, +that other keys are unchanged (key inequality), that nested-mapping writes +leave a plain scalar slot untouched and vice versa, that a struct receipt +destructures to the written words, that a transient lock is read back and +leaves persistent storage untouched, and that a callee's write in a hop does +not reach the caller's entries. Lens laws: `ContractState.readMapChain_writeMapChain(_same)`, +`readMapChain_writeMapChain_keys_ne` / `_offset_ne` / `_slot_ne`, +`readMapChain_writeSlot`, `storage_writeMapChain`, +`readMapChain_exitHop_enterHop_of_frame`. + +**History.** #2432 first stored these words in the `.slot` channel at the +keccak slot. That made key-vs-key separation depend on +`solidityMappingSlot_injective` and mapping-vs-scalar separation unprovable; +the symbolic `mapChain` channel replaces it. ## How to translate an OpenZeppelin-style contract chain diff --git a/docs/TRUST_ASSUMPTIONS.md b/docs/TRUST_ASSUMPTIONS.md index df4d55a08d..08d9de7451 100644 --- a/docs/TRUST_ASSUMPTIONS.md +++ b/docs/TRUST_ASSUMPTIONS.md @@ -229,7 +229,8 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V `Contract.hopCallView`: every word-valued storage channel is namespaced per contract across a distinct-address hop — scalar slots move through `StorageKey.contractSlot`, and address slots, transient slots and all - mappings (`addr` / `transient` / `map` / `mapUint` / `map2`) through + mappings (`addr` / `transient` / `map` / `mapUint` / `map2` / + `mapChain` / `transientMapChain`) through `StorageKey.scoped` (G24, #2440; `ContractState.switchSlotWorld`, `enterHop_readAddrSlot` / `enterHop_readMap` / …, `exitHop_enterHop_storageWords_plain`). A callee never sees or clobbers the @@ -597,21 +598,31 @@ of byte-for-byte EVM ABI layout. Trust boundaries of that plane: call observability must use the monadic primitives. - **`callExternal name(args)` surface** remains an unmodeled no-op at this plane. -- **Hashed mapping accessors are executable, on the `.slot` channel.** +- **Hashed mapping accessors are executable, on a symbolic channel.** `getMappingN`/`setMappingN`, `getMappingWord`/`setMappingWord` and the generated `structMember`/`setStructMember` family read and write - `ContractState.storage` at the Solidity keccak slot - (`Compiler.Proofs.abstractMappingSlot`, folded left over the key path, plus - the member word offset modulo `2^256`); `transient` mapping chains use the - `.transient` channel. `structMembers`/`structMembers2` destructuring lowers - to those reads. This channel is disjoint from the constructor-keyed - `storageMap`/`storageMapUint`/`storageMap2` channels behind - `getMapping`/`getMappingUint`/`getMapping2`; a field is accessed through - exactly one family, fixed by its declared storage type. Distinctness of two - hashed slots with different keys rests on the existing - `solidityMappingSlot_injective` axiom; adjacent struct words are distinct - without it (`Contracts.structSlot_ne_succ`). The pure expression form - `structMembers` outside `let (..) :=` / `return` still yields `default`. + `StorageKey.mapChain baseSlot keyWords wordOffset` + (`ContractState.readMapChain`/`writeMapChain`); `transient` mapping chains + use `StorageKey.transientMapChain baseSlot keyWords` + (`readTransientMapChain`/`writeTransientMapChain`). + `structMembers`/`structMembers2` destructuring lowers to those reads. + Entries with different `(baseSlot, keyWords, wordOffset)` are independent + by constructor injectivity, and the channel is disjoint from the scalar + `.slot` channel and from the `storageMap`/`storageMapUint`/`storageMap2` + channels behind `getMapping`/`getMappingUint`/`getMapping2`, so executable + plane non-aliasing (key vs key, member vs member, mapping entry vs scalar + slot) uses no axiom. The Solidity keccak slot + (`Compiler.Proofs.mappingChainSlotLocation`: keccak folded over the key + path plus the word offset modulo `2^256`) is an interpretation: the + executable channel agrees with the flat `.slot` channel the model plane + reads under `Compiler.Proofs.Storage.HashedMappingLayout.HashedCoherentOn`, + preserved by aligned writes given a finite layout non-alias certificate + (a hypothesis, not `solidityMappingSlot_injective`). A field is accessed + through exactly one family, fixed by its declared storage type. Hops + namespace both hashed keys per contract (`StorageKey.scoped`), and + `Contract.run` rollback restores them with the rest of `storageWords`. The + pure expression form `structMembers` outside `let (..) :=` / `return` still + yields `default`. - **`externalCallBindTo` journals target and value and debits ETH on success.** It is still a stub for the callee return word (`externalCallStubWord`). Real callee state is the model-plane