From 7ce0be9887c9d57094e2bd9f4f6a03a76bdb94b5 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 29 Sep 2026 13:40:36 +0200
Subject: [PATCH 1/7] WIP: range-restrict solidityMappingSlot_injective

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Compiler/Proofs/MappingSlot.lean | 79 +++++++++++++++++++++++++++++---
 1 file changed, 73 insertions(+), 6 deletions(-)

diff --git a/Compiler/Proofs/MappingSlot.lean b/Compiler/Proofs/MappingSlot.lean
index 4010558937..056b35d22a 100644
--- a/Compiler/Proofs/MappingSlot.lean
+++ b/Compiler/Proofs/MappingSlot.lean
@@ -57,21 +57,72 @@ private def solidityMappingSlot_ffi (baseSlot key : Nat) : Nat :=
 def solidityMappingSlot (baseSlot key : Nat) : Nat :=
   EvmYul.fromByteArrayBigEndian (KeccakEngine.keccak256 (abiEncodeMappingSlot baseSlot key))
 
+/-- `EvmYul.UInt256.ofNat` reduces its argument modulo `2^256`. -/
+theorem evmYul_uint256_ofNat_mod (n : Nat) :
+    EvmYul.UInt256.ofNat (n % Compiler.Constants.evmModulus) = EvmYul.UInt256.ofNat n := by
+  unfold EvmYul.UInt256.ofNat
+  simp only [Id.run]
+  congr 1
+  apply Fin.ext
+  simp [Fin.ofNat, EvmYul.UInt256.size]
+
+/-- The ABI encoding only sees base slot and key modulo `2^256`. -/
+theorem abiEncodeMappingSlot_mod (baseSlot key : Nat) :
+    abiEncodeMappingSlot (baseSlot % Compiler.Constants.evmModulus)
+        (key % Compiler.Constants.evmModulus) =
+      abiEncodeMappingSlot baseSlot key := by
+  simp only [abiEncodeMappingSlot, evmYul_uint256_ofNat_mod]
+
+/-- The mapping-slot derivation only sees base slot and key modulo `2^256`.
+    In particular `solidityMappingSlot b k = solidityMappingSlot b (k + 2^256)`,
+    which is why `solidityMappingSlot_injective` must be range-restricted. -/
+theorem solidityMappingSlot_mod (baseSlot key : Nat) :
+    solidityMappingSlot (baseSlot % Compiler.Constants.evmModulus)
+        (key % Compiler.Constants.evmModulus) =
+      solidityMappingSlot baseSlot key := by
+  unfold solidityMappingSlot
+  rw [abiEncodeMappingSlot_mod]
+
 /-- Collision-resistance of Solidity mapping-slot derivation
-    `keccak256(abi.encode(key, baseSlot))`.
+    `keccak256(abi.encode(key, baseSlot))` on in-range (`< 2^256`) base
+    slots and keys, i.e. on the 64-byte ABI words actually hashed.
 
     **Not** injectivity of keccak256 on arbitrary `ByteArray`s (256-bit
-    output, infinite domain). See `docs/AXIOMS.md`. -/
+    output, infinite domain). The range hypotheses are required: the ABI
+    encoding reduces both arguments modulo `2^256` (`solidityMappingSlot_mod`),
+    so an unrestricted statement over `Nat` is refutable
+    (`solidityMappingSlot 0 0 = solidityMappingSlot 0 (2^256)`).
+    See `docs/AXIOMS.md`. -/
 axiom solidityMappingSlot_injective
     (base₁ key₁ base₂ key₂ : Nat) :
+    base₁ < Compiler.Constants.evmModulus →
+    key₁ < Compiler.Constants.evmModulus →
+    base₂ < Compiler.Constants.evmModulus →
+    key₂ < Compiler.Constants.evmModulus →
     solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂ →
     base₁ = base₂ ∧ key₁ = key₂
 
+/-- Unbounded consequence of `solidityMappingSlot_injective`: equal derived
+    slots force equal base slots and keys modulo `2^256`. -/
+theorem solidityMappingSlot_injective_mod (base₁ key₁ base₂ key₂ : Nat)
+    (h : solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂) :
+    base₁ % Compiler.Constants.evmModulus = base₂ % Compiler.Constants.evmModulus ∧
+      key₁ % Compiler.Constants.evmModulus = key₂ % Compiler.Constants.evmModulus := by
+  have hpos : 0 < Compiler.Constants.evmModulus := by decide
+  apply solidityMappingSlot_injective _ _ _ _
+    (Nat.mod_lt _ hpos) (Nat.mod_lt _ hpos) (Nat.mod_lt _ hpos) (Nat.mod_lt _ hpos)
+  rw [solidityMappingSlot_mod, solidityMappingSlot_mod]
+  exact h
+
 theorem solidityMappingSlot_ne {base₁ key₁ base₂ key₂ : Nat}
+    (hb₁ : base₁ < Compiler.Constants.evmModulus)
+    (hk₁ : key₁ < Compiler.Constants.evmModulus)
+    (hb₂ : base₂ < Compiler.Constants.evmModulus)
+    (hk₂ : key₂ < Compiler.Constants.evmModulus)
     (h : base₁ ≠ base₂ ∨ key₁ ≠ key₂) :
     solidityMappingSlot base₁ key₁ ≠ solidityMappingSlot base₂ key₂ := by
   intro heq
-  rcases solidityMappingSlot_injective base₁ key₁ base₂ key₂ heq with ⟨hb, hk⟩
+  rcases solidityMappingSlot_injective base₁ key₁ base₂ key₂ hb₁ hk₁ hb₂ hk₂ heq with ⟨hb, hk⟩
   cases h with
   | inl hbase => exact hbase hb
   | inr hkey => exact hkey hk
@@ -271,25 +322,41 @@ theorem abstractMappingSlot_lt_evmModulus (baseSlot key : Nat) :
 
 theorem abstractNestedMappingSlot_injective
     (base₁ key₁ key₂ base₂ key₁' key₂' : Nat)
+    (hb₁ : base₁ < Compiler.Constants.evmModulus)
+    (hk₁ : key₁ < Compiler.Constants.evmModulus)
+    (hk₂ : key₂ < Compiler.Constants.evmModulus)
+    (hb₂ : base₂ < Compiler.Constants.evmModulus)
+    (hk₁' : key₁' < Compiler.Constants.evmModulus)
+    (hk₂' : key₂' < Compiler.Constants.evmModulus)
     (h : abstractNestedMappingSlot base₁ key₁ key₂ =
       abstractNestedMappingSlot base₂ key₁' key₂') :
     base₁ = base₂ ∧ key₁ = key₁' ∧ key₂ = key₂' := by
   have hinj :=
     solidityMappingSlot_injective
       (solidityMappingSlot base₁ key₁) key₂
-      (solidityMappingSlot base₂ key₁') key₂' (by
+      (solidityMappingSlot base₂ key₁') key₂'
+      (solidityMappingSlot_lt_evmModulus _ _) hk₂
+      (solidityMappingSlot_lt_evmModulus _ _) hk₂' (by
         simpa [abstractNestedMappingSlot, abstractMappingSlot] using h)
   rcases hinj with ⟨hinner, hkey2⟩
-  rcases solidityMappingSlot_injective base₁ key₁ base₂ key₁' hinner with ⟨hbase, hkey1⟩
+  rcases solidityMappingSlot_injective base₁ key₁ base₂ key₁' hb₁ hk₁ hb₂ hk₁' hinner
+    with ⟨hbase, hkey1⟩
   exact ⟨hbase, hkey1, hkey2⟩
 
 theorem abstractNestedMappingSlot_ne
     {base₁ key₁ key₂ base₂ key₁' key₂' : Nat}
+    (hb₁ : base₁ < Compiler.Constants.evmModulus)
+    (hk₁ : key₁ < Compiler.Constants.evmModulus)
+    (hk₂ : key₂ < Compiler.Constants.evmModulus)
+    (hb₂ : base₂ < Compiler.Constants.evmModulus)
+    (hk₁' : key₁' < Compiler.Constants.evmModulus)
+    (hk₂' : key₂' < Compiler.Constants.evmModulus)
     (h : base₁ ≠ base₂ ∨ key₁ ≠ key₁' ∨ key₂ ≠ key₂') :
     abstractNestedMappingSlot base₁ key₁ key₂ ≠
       abstractNestedMappingSlot base₂ key₁' key₂' := by
   intro heq
-  rcases abstractNestedMappingSlot_injective base₁ key₁ key₂ base₂ key₁' key₂' heq
+  rcases abstractNestedMappingSlot_injective base₁ key₁ key₂ base₂ key₁' key₂'
+      hb₁ hk₁ hk₂ hb₂ hk₁' hk₂' heq
     with ⟨hb, hk1, hk2⟩
   rcases h with h | h | h
   · exact h hb

From b3087ea163726c7f4cef7b453619d5aadebc5a76 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 29 Sep 2026 13:46:48 +0200
Subject: [PATCH 2/7] WIP: propagate range hypotheses to storage coherence
 callers

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Compiler/Proofs/Storage/FieldCoherence.lean   |   9 +-
 Compiler/Proofs/Storage/FieldEncode.lean      |   9 +-
 Compiler/Proofs/Storage/MappingCoherence.lean | 116 ++++++++++--------
 .../Proofs/Storage/MappingCoherenceOn.lean    |  35 ++++--
 4 files changed, 103 insertions(+), 66 deletions(-)

diff --git a/Compiler/Proofs/Storage/FieldCoherence.lean b/Compiler/Proofs/Storage/FieldCoherence.lean
index 42f6532798..b61454f920 100644
--- a/Compiler/Proofs/Storage/FieldCoherence.lean
+++ b/Compiler/Proofs/Storage/FieldCoherence.lean
@@ -21,35 +21,38 @@ open Compiler.Proofs
 theorem fieldMapKey_coherent_storageKeySlot
     {s : ContractState} {f : Field} {slot : Nat} {key : Address}
     (hcoh : MappingCoherent s)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (htr : f.isTransient = false)
     (hty : f.ty = .mappingTyped (.simple .address)) :
     (fieldMapKey f slot key).bind (fun sk =>
       (storageKeySlot sk).map (fun n => s.storage n)) =
       some (s.storageMap slot key) := by
   simp [fieldMapKey, htr, hty, storageKeySlot]
-  exact (hcoh slot key).symm
+  exact (hcoh slot key hslot).symm
 
 theorem fieldMapUintKey_coherent_storageKeySlot
     {s : ContractState} {f : Field} {slot : Nat} {key : Uint256}
     (hcoh : MappingCoherentUint s)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (htr : f.isTransient = false)
     (hty : f.ty = .mappingTyped (.simple .uint256)) :
     (fieldMapUintKey f slot key).bind (fun sk =>
       (storageKeySlot sk).map (fun n => s.storage n)) =
       some (s.storageMapUint slot key) := by
   simp [fieldMapUintKey, htr, hty, storageKeySlot]
-  exact (hcoh slot key).symm
+  exact (hcoh slot key hslot).symm
 
 theorem fieldMap2Key_coherent_storageKeySlot
     {s : ContractState} {f : Field} {slot : Nat} {k1 k2 : Address}
     (hcoh : MappingCoherentMap2 s)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (htr : f.isTransient = false)
     (hty : f.ty = .mappingTyped (.nested .address .address)) :
     (fieldMap2Key f slot k1 k2).bind (fun sk =>
       (storageKeySlot sk).map (fun n => s.storage n)) =
       some (s.storageMap2 slot k1 k2) := by
   simp [fieldMap2Key, htr, hty, storageKeySlot]
-  exact (hcoh slot k1 k2).symm
+  exact (hcoh slot k1 k2 hslot).symm
 
 theorem fieldMapKey_coherentOn_storageKeySlot
     {s : ContractState} {f : Field} {slot : Nat} {key : Address}
diff --git a/Compiler/Proofs/Storage/FieldEncode.lean b/Compiler/Proofs/Storage/FieldEncode.lean
index 6eaba1bc6b..ca7562409b 100644
--- a/Compiler/Proofs/Storage/FieldEncode.lean
+++ b/Compiler/Proofs/Storage/FieldEncode.lean
@@ -98,6 +98,7 @@ theorem encodeStorageAt_of_unresolved
 theorem encodeStorageAt_fieldMapKey
     {fields : List Field} {s : ContractState} {slot : Nat} {key : Address}
     (hcoh : MappingCoherent s)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (hresolved :
       findResolvedFieldAtSlot fields
         (solidityMappingSlot slot (addressToWord key).val) = none)
@@ -106,22 +107,24 @@ theorem encodeStorageAt_fieldMapKey
         (solidityMappingSlot slot (addressToWord key).val) = none) :
     encodeStorageAt fields s (solidityMappingSlot slot (addressToWord key).val) =
       (s.storageMap slot key).val := by
-  rw [encodeStorageAt_of_unresolved hresolved hdyn, hcoh slot key]
+  rw [encodeStorageAt_of_unresolved hresolved hdyn, hcoh slot key hslot]
 
 theorem encodeStorageAt_fieldMapUintKey
     {fields : List Field} {s : ContractState} {slot : Nat} {key : Uint256}
     (hcoh : MappingCoherentUint s)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (hresolved :
       findResolvedFieldAtSlot fields (solidityMappingSlot slot key.val) = none)
     (hdyn :
       findDynamicArrayElementAtSlot fields s (solidityMappingSlot slot key.val) = none) :
     encodeStorageAt fields s (solidityMappingSlot slot key.val) =
       (s.storageMapUint slot key).val := by
-  rw [encodeStorageAt_of_unresolved hresolved hdyn, hcoh slot key]
+  rw [encodeStorageAt_of_unresolved hresolved hdyn, hcoh slot key hslot]
 
 theorem encodeStorageAt_fieldMap2Key
     {fields : List Field} {s : ContractState} {slot : Nat} {k1 k2 : Address}
     (hcoh : MappingCoherentMap2 s)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (hresolved :
       findResolvedFieldAtSlot fields
         (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) = none)
@@ -131,7 +134,7 @@ theorem encodeStorageAt_fieldMap2Key
     encodeStorageAt fields s
         (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) =
       (s.storageMap2 slot k1 k2).val := by
-  rw [encodeStorageAt_of_unresolved hresolved hdyn, hcoh slot k1 k2]
+  rw [encodeStorageAt_of_unresolved hresolved hdyn, hcoh slot k1 k2 hslot]
 
 theorem encodeStorageAt_fieldMapKey_on
     {fields : List Field} {s : ContractState} {slot : Nat} {key : Address}
diff --git a/Compiler/Proofs/Storage/MappingCoherence.lean b/Compiler/Proofs/Storage/MappingCoherence.lean
index 6531f240fd..bc01514e62 100644
--- a/Compiler/Proofs/Storage/MappingCoherence.lean
+++ b/Compiler/Proofs/Storage/MappingCoherence.lean
@@ -35,14 +35,17 @@ def storageKeySlot : StorageKey → Option Nat
   | .scoped _ _ => none
 
 /-- Address-keyed mapping shadow agrees with the flat channel at the
-    derived Solidity slot. -/
+    derived Solidity slot, for every in-range (`< 2^256`) base slot.
+    Out-of-range base slots alias in-range ones under the ABI encoding
+    (`solidityMappingSlot_mod`), so they cannot be kept coherent
+    independently. -/
 def MappingCoherent (s : ContractState) : Prop :=
-  ∀ (slot : Nat) (key : Address),
+  ∀ (slot : Nat) (key : Address), slot < Compiler.Constants.evmModulus →
     s.storageMap slot key =
       s.storage (solidityMappingSlot slot (addressToWord key).val)
 
 theorem defaultState_mappingCoherent : MappingCoherent defaultState := by
-  intro slot key
+  intro slot key _
   simp [storageMap, storage, defaultState]
 
 /-- The aligned write — shadow map plus the derived flat slot — makes the
@@ -107,11 +110,11 @@ theorem storageKeySlot_transient (n : Nat) : storageKeySlot (.transient n) = non
 
 /-- Uint-keyed mapping shadow agrees with the flat channel at the derived slot. -/
 def MappingCoherentUint (s : ContractState) : Prop :=
-  ∀ (slot : Nat) (key : Uint256),
+  ∀ (slot : Nat) (key : Uint256), slot < Compiler.Constants.evmModulus →
     s.storageMapUint slot key = s.storage (solidityMappingSlot slot key.val)
 
 theorem defaultState_mappingCoherentUint : MappingCoherentUint defaultState := by
-  intro slot key
+  intro slot key _
   simp [storageMapUint, storage, defaultState]
 
 theorem writeMapUint_aligned_same (s : ContractState) (slot : Nat) (key v : Uint256) :
@@ -144,12 +147,12 @@ theorem writeMapUint_aligned_other (s : ContractState) (slot : Nat) (key v : Uin
 
 /-- Double-address mapping shadow agrees with the nested derived slot. -/
 def MappingCoherentMap2 (s : ContractState) : Prop :=
-  ∀ (slot : Nat) (k1 k2 : Address),
+  ∀ (slot : Nat) (k1 k2 : Address), slot < Compiler.Constants.evmModulus →
     s.storageMap2 slot k1 k2 =
       s.storage (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val)
 
 theorem defaultState_mappingCoherentMap2 : MappingCoherentMap2 defaultState := by
-  intro slot k1 k2
+  intro slot k1 k2 _
   simp [storageMap2, storage, defaultState]
 
 theorem writeMap2_aligned_same (s : ContractState) (slot : Nat) (k1 k2 : Address)
@@ -222,32 +225,46 @@ theorem addressToWord_injective {a b : Address}
   rw [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at hval
   simpa [Core.Address.toNat] using hval
 
+theorem addressToWord_val_lt (a : Address) :
+    (addressToWord a).val < Compiler.Constants.evmModulus :=
+  (addressToWord a).isLt
+
 theorem mappingAddrSlot_ne_of_map_ne {slot slot' : Nat} {key key' : Address}
+    (hs' : slot' < Compiler.Constants.evmModulus)
+    (hs : slot < Compiler.Constants.evmModulus)
     (h : StorageKey.map slot' key' ≠ StorageKey.map slot key) :
     solidityMappingSlot slot' (addressToWord key').val ≠
       solidityMappingSlot slot (addressToWord key).val := by
   intro heq
   rcases solidityMappingSlot_injective slot' (addressToWord key').val
-      slot (addressToWord key).val heq with ⟨hs, hk⟩
+      slot (addressToWord key).val hs' (addressToWord_val_lt key') hs
+      (addressToWord_val_lt key) heq with ⟨hs, hk⟩
   apply h
   rw [hs, addressToWord_injective (Core.Uint256.ext hk)]
 
 theorem mappingUintSlot_ne_of_mapUint_ne {slot slot' : Nat} {key key' : Uint256}
+    (hs' : slot' < Compiler.Constants.evmModulus)
+    (hs : slot < Compiler.Constants.evmModulus)
     (h : StorageKey.mapUint slot' key' ≠ StorageKey.mapUint slot key) :
     solidityMappingSlot slot' key'.val ≠ solidityMappingSlot slot key.val := by
   intro heq
-  rcases solidityMappingSlot_injective slot' key'.val slot key.val heq with ⟨hs, hk⟩
+  rcases solidityMappingSlot_injective slot' key'.val slot key.val hs' key'.isLt hs key.isLt heq
+    with ⟨hs, hk⟩
   apply h
   rw [hs, Core.Uint256.ext hk]
 
 theorem mappingMap2Slot_ne_of_map2_ne
     {slot slot' : Nat} {k1 k1' k2 k2' : Address}
+    (hs' : slot' < Compiler.Constants.evmModulus)
+    (hs : slot < Compiler.Constants.evmModulus)
     (h : StorageKey.map2 slot' k1' k2' ≠ StorageKey.map2 slot k1 k2) :
     abstractNestedMappingSlot slot' (addressToWord k1').val (addressToWord k2').val ≠
       abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val := by
   intro heq
   rcases abstractNestedMappingSlot_injective slot' (addressToWord k1').val
-      (addressToWord k2').val slot (addressToWord k1).val (addressToWord k2).val heq
+      (addressToWord k2').val slot (addressToWord k1).val (addressToWord k2).val
+      hs' (addressToWord_val_lt k1') (addressToWord_val_lt k2') hs
+      (addressToWord_val_lt k1) (addressToWord_val_lt k2) heq
     with ⟨hs, hk1, hk2⟩
   apply h
   rw [hs, addressToWord_injective (Core.Uint256.ext hk1),
@@ -258,52 +275,55 @@ theorem mappingMap2Slot_ne_of_map2_ne
     Not injectivity of keccak on all ByteArrays. -/
 theorem writeMap_aligned_preserves_mappingCoherent
     (s : ContractState) (slot : Nat) (key : Address) (v : Uint256)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherent s) :
     MappingCoherent
       ((s.writeMap slot key v).writeSlot
         (solidityMappingSlot slot (addressToWord key).val) v) := by
-  intro slot' key'
+  intro slot' key' hslot'
   by_cases hs : slot' = slot
   · by_cases hk : key' = key
     · simp [hs, hk]
     · have hkey : StorageKey.map slot' key' ≠ StorageKey.map slot key := by
         intro heq; injection heq with _ hk'; exact hk hk'
-      exact writeMap_aligned_other s slot key v slot' key' (hcoh slot' key')
-        hkey (mappingAddrSlot_ne_of_map_ne hkey)
+      exact writeMap_aligned_other s slot key v slot' key' (hcoh slot' key' hslot')
+        hkey (mappingAddrSlot_ne_of_map_ne hslot' hslot hkey)
   · have hkey : StorageKey.map slot' key' ≠ StorageKey.map slot key := by
       intro heq; injection heq with hs' _; exact hs hs'
-    exact writeMap_aligned_other s slot key v slot' key' (hcoh slot' key')
-      hkey (mappingAddrSlot_ne_of_map_ne hkey)
+    exact writeMap_aligned_other s slot key v slot' key' (hcoh slot' key' hslot')
+      hkey (mappingAddrSlot_ne_of_map_ne hslot' hslot hkey)
 
 theorem writeMapUint_aligned_preserves_mappingCoherentUint
     (s : ContractState) (slot : Nat) (key v : Uint256)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherentUint s) :
     MappingCoherentUint
       ((s.writeMapUint slot key v).writeSlot
         (solidityMappingSlot slot key.val) v) := by
-  intro slot' key'
+  intro slot' key' hslot'
   by_cases hs : slot' = slot
   · by_cases hk : (key' : Nat) = (key : Nat)
     · have hk' : key' = key := Core.Uint256.ext hk
       simpa [hs, hk'] using writeMapUint_aligned_same s slot key v
     · have hkey : StorageKey.mapUint slot' key' ≠ StorageKey.mapUint slot key := by
         intro heq; injection heq with _ hk'; exact hk (congrArg (fun w : Uint256 => (w : Nat)) hk')
-      exact writeMapUint_aligned_other s slot key v slot' key' (hcoh slot' key')
-        hkey (mappingUintSlot_ne_of_mapUint_ne hkey)
+      exact writeMapUint_aligned_other s slot key v slot' key' (hcoh slot' key' hslot')
+        hkey (mappingUintSlot_ne_of_mapUint_ne hslot' hslot hkey)
   · have hkey : StorageKey.mapUint slot' key' ≠ StorageKey.mapUint slot key := by
       intro heq; injection heq with hs' _; exact hs hs'
-    exact writeMapUint_aligned_other s slot key v slot' key' (hcoh slot' key')
-      hkey (mappingUintSlot_ne_of_mapUint_ne hkey)
+    exact writeMapUint_aligned_other s slot key v slot' key' (hcoh slot' key' hslot')
+      hkey (mappingUintSlot_ne_of_mapUint_ne hslot' hslot hkey)
 
 set_option maxHeartbeats 800000 in
 theorem writeMap2_aligned_preserves_mappingCoherentMap2
     (s : ContractState) (slot : Nat) (k1 k2 : Address) (v : Uint256)
+    (hslot : slot < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherentMap2 s) :
     MappingCoherentMap2
       ((s.writeMap2 slot k1 k2 v).writeSlot
         (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val)
         v) := by
-  intro slot' k1' k2'
+  intro slot' k1' k2' hslot'
   by_cases hs : slot' = slot
   · by_cases h1 : k1' = k1
     · by_cases h2 : k2' = k2
@@ -311,15 +331,15 @@ theorem writeMap2_aligned_preserves_mappingCoherentMap2
       · have hkey : StorageKey.map2 slot' k1' k2' ≠ StorageKey.map2 slot k1 k2 := by
           intro heq; injection heq with _ _ hk2; exact h2 hk2
         exact writeMap2_aligned_other s slot k1 k2 v slot' k1' k2'
-          (hcoh slot' k1' k2') hkey (mappingMap2Slot_ne_of_map2_ne hkey)
+          (hcoh slot' k1' k2' hslot') hkey (mappingMap2Slot_ne_of_map2_ne hslot' hslot hkey)
     · have hkey : StorageKey.map2 slot' k1' k2' ≠ StorageKey.map2 slot k1 k2 := by
         intro heq; injection heq with _ hk1 _; exact h1 hk1
       exact writeMap2_aligned_other s slot k1 k2 v slot' k1' k2'
-        (hcoh slot' k1' k2') hkey (mappingMap2Slot_ne_of_map2_ne hkey)
+        (hcoh slot' k1' k2' hslot') hkey (mappingMap2Slot_ne_of_map2_ne hslot' hslot hkey)
   · have hkey : StorageKey.map2 slot' k1' k2' ≠ StorageKey.map2 slot k1 k2 := by
       intro heq; injection heq with hs' _ _; exact hs hs'
     exact writeMap2_aligned_other s slot k1 k2 v slot' k1' k2'
-      (hcoh slot' k1' k2') hkey (mappingMap2Slot_ne_of_map2_ne hkey)
+      (hcoh slot' k1' k2' hslot') hkey (mappingMap2Slot_ne_of_map2_ne hslot' hslot hkey)
 
 /-- Transient writes never touch persistent `.slot` / `.map*`. Constructor
     injectivity; no keccak hypothesis. -/
@@ -327,7 +347,7 @@ theorem writeTransient_preserves_mappingCoherent
     (s : ContractState) (n : Nat) (v : Uint256)
     (hcoh : MappingCoherent s) :
     MappingCoherent (s.writeTransient n v) := by
-  intro slot key
+  intro slot key hslot
   have hmap : (s.writeTransient n v).storageMap slot key = s.storageMap slot key := by
     simp [storageMap, writeTransient]
   have hflat :
@@ -335,13 +355,13 @@ theorem writeTransient_preserves_mappingCoherent
         (solidityMappingSlot slot (addressToWord key).val) =
         s.storage (solidityMappingSlot slot (addressToWord key).val) := by
     simp [storage, writeTransient]
-  exact (hmap.trans (hcoh slot key)).trans hflat.symm
+  exact (hmap.trans (hcoh slot key hslot)).trans hflat.symm
 
 theorem writeTransient_preserves_mappingCoherentUint
     (s : ContractState) (n : Nat) (v : Uint256)
     (hcoh : MappingCoherentUint s) :
     MappingCoherentUint (s.writeTransient n v) := by
-  intro slot key
+  intro slot key hslot
   have hmap :
       (s.writeTransient n v).storageMapUint slot key = s.storageMapUint slot key := by
     simp [storageMapUint, writeTransient]
@@ -349,13 +369,13 @@ theorem writeTransient_preserves_mappingCoherentUint
       (s.writeTransient n v).storage (solidityMappingSlot slot key.val) =
         s.storage (solidityMappingSlot slot key.val) := by
     simp [storage, writeTransient]
-  exact (hmap.trans (hcoh slot key)).trans hflat.symm
+  exact (hmap.trans (hcoh slot key hslot)).trans hflat.symm
 
 theorem writeTransient_preserves_mappingCoherentMap2
     (s : ContractState) (n : Nat) (v : Uint256)
     (hcoh : MappingCoherentMap2 s) :
     MappingCoherentMap2 (s.writeTransient n v) := by
-  intro slot k1 k2
+  intro slot k1 k2 hslot
   have hmap :
       (s.writeTransient n v).storageMap2 slot k1 k2 = s.storageMap2 slot k1 k2 := by
     simp [storageMap2, writeTransient]
@@ -365,7 +385,7 @@ theorem writeTransient_preserves_mappingCoherentMap2
         s.storage
           (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) := by
     simp [storage, writeTransient]
-  exact (hmap.trans (hcoh slot k1 k2)).trans hflat.symm
+  exact (hmap.trans (hcoh slot k1 k2 hslot)).trans hflat.symm
 
 /-- Address-slot writes never touch persistent `.slot` / `.map*`.
     Constructor injectivity of `StorageKey.addr`; no image-avoidance
@@ -374,7 +394,7 @@ theorem writeAddrSlot_preserves_mappingCoherent
     (s : ContractState) (n : Nat) (v : Address)
     (hcoh : MappingCoherent s) :
     MappingCoherent (s.writeAddrSlot n v) := by
-  intro slot key
+  intro slot key hslot
   have hmap : (s.writeAddrSlot n v).storageMap slot key = s.storageMap slot key := by
     simp [storageMap, writeAddrSlot]
   have hflat :
@@ -382,13 +402,13 @@ theorem writeAddrSlot_preserves_mappingCoherent
         (solidityMappingSlot slot (addressToWord key).val) =
         s.storage (solidityMappingSlot slot (addressToWord key).val) := by
     simp [storage, writeAddrSlot]
-  exact (hmap.trans (hcoh slot key)).trans hflat.symm
+  exact (hmap.trans (hcoh slot key hslot)).trans hflat.symm
 
 theorem writeAddrSlot_preserves_mappingCoherentUint
     (s : ContractState) (n : Nat) (v : Address)
     (hcoh : MappingCoherentUint s) :
     MappingCoherentUint (s.writeAddrSlot n v) := by
-  intro slot key
+  intro slot key hslot
   have hmap :
       (s.writeAddrSlot n v).storageMapUint slot key = s.storageMapUint slot key := by
     simp [storageMapUint, writeAddrSlot]
@@ -396,13 +416,13 @@ theorem writeAddrSlot_preserves_mappingCoherentUint
       (s.writeAddrSlot n v).storage (solidityMappingSlot slot key.val) =
         s.storage (solidityMappingSlot slot key.val) := by
     simp [storage, writeAddrSlot]
-  exact (hmap.trans (hcoh slot key)).trans hflat.symm
+  exact (hmap.trans (hcoh slot key hslot)).trans hflat.symm
 
 theorem writeAddrSlot_preserves_mappingCoherentMap2
     (s : ContractState) (n : Nat) (v : Address)
     (hcoh : MappingCoherentMap2 s) :
     MappingCoherentMap2 (s.writeAddrSlot n v) := by
-  intro slot k1 k2
+  intro slot k1 k2 hslot
   have hmap :
       (s.writeAddrSlot n v).storageMap2 slot k1 k2 = s.storageMap2 slot k1 k2 := by
     simp [storageMap2, writeAddrSlot]
@@ -412,7 +432,7 @@ theorem writeAddrSlot_preserves_mappingCoherentMap2
         s.storage
           (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) := by
     simp [storage, writeAddrSlot]
-  exact (hmap.trans (hcoh slot k1 k2)).trans hflat.symm
+  exact (hmap.trans (hcoh slot k1 k2 hslot)).trans hflat.symm
 
 /-- Array-channel writes never touch `storageWords`. Field independence;
     no image-avoidance and not keccak injectivity. -/
@@ -420,7 +440,7 @@ theorem writeArray_preserves_mappingCoherent
     (s : ContractState) (n : Nat) (vs : List Uint256)
     (hcoh : MappingCoherent s) :
     MappingCoherent (s.writeArray n vs) := by
-  intro slot key
+  intro slot key hslot
   have hmap : (s.writeArray n vs).storageMap slot key = s.storageMap slot key := by
     simp [storageMap, writeArray]
   have hflat :
@@ -428,13 +448,13 @@ theorem writeArray_preserves_mappingCoherent
         (solidityMappingSlot slot (addressToWord key).val) =
         s.storage (solidityMappingSlot slot (addressToWord key).val) := by
     simp [storage, writeArray]
-  exact (hmap.trans (hcoh slot key)).trans hflat.symm
+  exact (hmap.trans (hcoh slot key hslot)).trans hflat.symm
 
 theorem writeArray_preserves_mappingCoherentUint
     (s : ContractState) (n : Nat) (vs : List Uint256)
     (hcoh : MappingCoherentUint s) :
     MappingCoherentUint (s.writeArray n vs) := by
-  intro slot key
+  intro slot key hslot
   have hmap :
       (s.writeArray n vs).storageMapUint slot key = s.storageMapUint slot key := by
     simp [storageMapUint, writeArray]
@@ -442,13 +462,13 @@ theorem writeArray_preserves_mappingCoherentUint
       (s.writeArray n vs).storage (solidityMappingSlot slot key.val) =
         s.storage (solidityMappingSlot slot key.val) := by
     simp [storage, writeArray]
-  exact (hmap.trans (hcoh slot key)).trans hflat.symm
+  exact (hmap.trans (hcoh slot key hslot)).trans hflat.symm
 
 theorem writeArray_preserves_mappingCoherentMap2
     (s : ContractState) (n : Nat) (vs : List Uint256)
     (hcoh : MappingCoherentMap2 s) :
     MappingCoherentMap2 (s.writeArray n vs) := by
-  intro slot k1 k2
+  intro slot k1 k2 hslot
   have hmap :
       (s.writeArray n vs).storageMap2 slot k1 k2 = s.storageMap2 slot k1 k2 := by
     simp [storageMap2, writeArray]
@@ -458,7 +478,7 @@ theorem writeArray_preserves_mappingCoherentMap2
         s.storage
           (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) := by
     simp [storage, writeArray]
-  exact (hmap.trans (hcoh slot k1 k2)).trans hflat.symm
+  exact (hmap.trans (hcoh slot k1 k2 hslot)).trans hflat.symm
 
 /-- A lone `writeSlot` preserves global address-map coherence when the
     written word is not any address-mapping derived slot. The `∀` is that
@@ -469,7 +489,7 @@ theorem writeSlot_preserves_mappingCoherent
     (hna : ∀ mapSlot mapKey,
       solidityMappingSlot mapSlot (addressToWord mapKey).val ≠ n) :
     MappingCoherent (s.writeSlot n v) := by
-  intro mapSlot mapKey
+  intro mapSlot mapKey hmapSlot
   have hmap : (s.writeSlot n v).storageMap mapSlot mapKey = s.storageMap mapSlot mapKey := by
     rw [storageMap_writeSlot]
   have hflat :
@@ -477,14 +497,14 @@ theorem writeSlot_preserves_mappingCoherent
         (solidityMappingSlot mapSlot (addressToWord mapKey).val) =
         s.storage (solidityMappingSlot mapSlot (addressToWord mapKey).val) :=
     storage_writeSlot_other (s := s) (hna mapSlot mapKey) v
-  exact (hmap.trans (hcoh mapSlot mapKey)).trans hflat.symm
+  exact (hmap.trans (hcoh mapSlot mapKey hmapSlot)).trans hflat.symm
 
 theorem writeSlot_preserves_mappingCoherentUint
     (s : ContractState) (n : Nat) (v : Uint256)
     (hcoh : MappingCoherentUint s)
     (hna : ∀ mapSlot mapKey, solidityMappingSlot mapSlot (mapKey : Nat) ≠ n) :
     MappingCoherentUint (s.writeSlot n v) := by
-  intro mapSlot mapKey
+  intro mapSlot mapKey hmapSlot
   have hmap :
       (s.writeSlot n v).storageMapUint mapSlot mapKey = s.storageMapUint mapSlot mapKey := by
     rw [storageMapUint_writeSlot]
@@ -492,7 +512,7 @@ theorem writeSlot_preserves_mappingCoherentUint
       (s.writeSlot n v).storage (solidityMappingSlot mapSlot (mapKey : Nat)) =
         s.storage (solidityMappingSlot mapSlot (mapKey : Nat)) :=
     storage_writeSlot_other (s := s) (hna mapSlot mapKey) v
-  exact (hmap.trans (hcoh mapSlot mapKey)).trans hflat.symm
+  exact (hmap.trans (hcoh mapSlot mapKey hmapSlot)).trans hflat.symm
 
 theorem writeSlot_preserves_mappingCoherentMap2
     (s : ContractState) (n : Nat) (v : Uint256)
@@ -500,7 +520,7 @@ theorem writeSlot_preserves_mappingCoherentMap2
     (hna : ∀ mapSlot mk1 mk2,
       abstractNestedMappingSlot mapSlot (addressToWord mk1).val (addressToWord mk2).val ≠ n) :
     MappingCoherentMap2 (s.writeSlot n v) := by
-  intro mapSlot mk1 mk2
+  intro mapSlot mk1 mk2 hmapSlot
   have hmap :
       (s.writeSlot n v).storageMap2 mapSlot mk1 mk2 = s.storageMap2 mapSlot mk1 mk2 := by
     rw [storageMap2_writeSlot]
@@ -510,6 +530,6 @@ theorem writeSlot_preserves_mappingCoherentMap2
         s.storage
           (abstractNestedMappingSlot mapSlot (addressToWord mk1).val (addressToWord mk2).val) :=
     storage_writeSlot_other (s := s) (hna mapSlot mk1 mk2) v
-  exact (hmap.trans (hcoh mapSlot mk1 mk2)).trans hflat.symm
+  exact (hmap.trans (hcoh mapSlot mk1 mk2 hmapSlot)).trans hflat.symm
 
 end Compiler.Proofs.Storage.MappingCoherence
diff --git a/Compiler/Proofs/Storage/MappingCoherenceOn.lean b/Compiler/Proofs/Storage/MappingCoherenceOn.lean
index a50fae0f4d..0d48b5b03c 100644
--- a/Compiler/Proofs/Storage/MappingCoherenceOn.lean
+++ b/Compiler/Proofs/Storage/MappingCoherenceOn.lean
@@ -49,13 +49,14 @@ def DerivedAddrSlotsDistinct (pairs : List (Nat × Address)) : Prop :=
 
 theorem mappingCoherentOn_of_mappingCoherent
     (s : ContractState) (pairs : List (Nat × Address))
+    (hrange : ∀ p ∈ pairs, p.1 < Compiler.Constants.evmModulus)
     (h : MappingCoherent s) : MappingCoherentOn s pairs := by
   intro p hp
-  exact h p.1 p.2
+  exact h p.1 p.2 (hrange p hp)
 
 theorem defaultState_mappingCoherentOn (pairs : List (Nat × Address)) :
     MappingCoherentOn defaultState pairs :=
-  mappingCoherentOn_of_mappingCoherent _ _ defaultState_mappingCoherent
+  fun _ _ => by simp [MappingCoherentAt, mappingAddrSlot, storageMap, storage, defaultState]
 
 theorem writeMap_aligned_preserves_at_same
     (s : ContractState) (slot : Nat) (key : Address) (v : Uint256) :
@@ -117,13 +118,15 @@ def DerivedUintSlotsDistinct (pairs : List (Nat × Uint256)) : Prop :=
 
 theorem mappingCoherentUintOn_of_mappingCoherentUint
     (s : ContractState) (pairs : List (Nat × Uint256))
+    (hrange : ∀ p ∈ pairs, p.1 < Compiler.Constants.evmModulus)
     (h : MappingCoherentUint s) : MappingCoherentUintOn s pairs := by
   intro p hp
-  exact h p.1 p.2
+  exact h p.1 p.2 (hrange p hp)
 
 theorem defaultState_mappingCoherentUintOn (pairs : List (Nat × Uint256)) :
     MappingCoherentUintOn defaultState pairs :=
-  mappingCoherentUintOn_of_mappingCoherentUint _ _ defaultState_mappingCoherentUint
+  fun _ _ => by
+    simp [MappingCoherentUintAt, mappingUintSlot, storageMapUint, storage, defaultState]
 
 theorem writeMapUint_aligned_preserves_at_same
     (s : ContractState) (slot : Nat) (key v : Uint256) :
@@ -185,13 +188,15 @@ def DerivedMap2SlotsDistinct (pairs : List (Nat × Address × Address)) : Prop :
 
 theorem mappingCoherentMap2On_of_mappingCoherentMap2
     (s : ContractState) (pairs : List (Nat × Address × Address))
+    (hrange : ∀ p ∈ pairs, p.1 < Compiler.Constants.evmModulus)
     (h : MappingCoherentMap2 s) : MappingCoherentMap2On s pairs := by
   intro p hp
-  exact h p.1 p.2.1 p.2.2
+  exact h p.1 p.2.1 p.2.2 (hrange p hp)
 
 theorem defaultState_mappingCoherentMap2On (pairs : List (Nat × Address × Address)) :
     MappingCoherentMap2On defaultState pairs :=
-  mappingCoherentMap2On_of_mappingCoherentMap2 _ _ defaultState_mappingCoherentMap2
+  fun _ _ => by
+    simp [MappingCoherentMap2At, mappingMap2Slot, storageMap2, storage, defaultState]
 
 theorem writeMap2_aligned_preserves_at_same
     (s : ContractState) (slot : Nat) (k1 k2 : Address) (v : Uint256) :
@@ -556,31 +561,37 @@ theorem writeArray_preserves_mappingCoherentMap2On
 theorem writeMap_aligned_preserves_on_of_mappingCoherent
     (s : ContractState) (pairs : List (Nat × Address))
     (slot : Nat) (key : Address) (v : Uint256)
+    (hslot : slot < Compiler.Constants.evmModulus)
+    (hrange : ∀ p ∈ pairs, p.1 < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherent s) :
     MappingCoherentOn
       ((s.writeMap slot key v).writeSlot (mappingAddrSlot slot key) v)
       pairs :=
-  mappingCoherentOn_of_mappingCoherent _ _
-    (writeMap_aligned_preserves_mappingCoherent s slot key v hcoh)
+  mappingCoherentOn_of_mappingCoherent _ _ hrange
+    (writeMap_aligned_preserves_mappingCoherent s slot key v hslot hcoh)
 
 theorem writeMapUint_aligned_preserves_uintOn_of_mappingCoherentUint
     (s : ContractState) (pairs : List (Nat × Uint256))
     (slot : Nat) (key v : Uint256)
+    (hslot : slot < Compiler.Constants.evmModulus)
+    (hrange : ∀ p ∈ pairs, p.1 < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherentUint s) :
     MappingCoherentUintOn
       ((s.writeMapUint slot key v).writeSlot (mappingUintSlot slot key) v)
       pairs :=
-  mappingCoherentUintOn_of_mappingCoherentUint _ _
-    (writeMapUint_aligned_preserves_mappingCoherentUint s slot key v hcoh)
+  mappingCoherentUintOn_of_mappingCoherentUint _ _ hrange
+    (writeMapUint_aligned_preserves_mappingCoherentUint s slot key v hslot hcoh)
 
 theorem writeMap2_aligned_preserves_map2On_of_mappingCoherentMap2
     (s : ContractState) (pairs : List (Nat × Address × Address))
     (slot : Nat) (k1 k2 : Address) (v : Uint256)
+    (hslot : slot < Compiler.Constants.evmModulus)
+    (hrange : ∀ p ∈ pairs, p.1 < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherentMap2 s) :
     MappingCoherentMap2On
       ((s.writeMap2 slot k1 k2 v).writeSlot (mappingMap2Slot slot k1 k2) v)
       pairs :=
-  mappingCoherentMap2On_of_mappingCoherentMap2 _ _
-    (writeMap2_aligned_preserves_mappingCoherentMap2 s slot k1 k2 v hcoh)
+  mappingCoherentMap2On_of_mappingCoherentMap2 _ _ hrange
+    (writeMap2_aligned_preserves_mappingCoherentMap2 s slot k1 k2 v hslot hcoh)
 
 end Compiler.Proofs.Storage.MappingCoherenceOn

From 60ffaed1a7a9f7a0b01436eaf2d676e09bb39420 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 29 Sep 2026 13:48:36 +0200
Subject: [PATCH 3/7] WIP: range hypotheses through MappingCoherentAllKeys

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../Storage/MappingCoherentAllKeys.lean       | 90 ++++++++++++-------
 1 file changed, 60 insertions(+), 30 deletions(-)

diff --git a/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean b/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean
index 393ffbaeea..8fd7e93b7a 100644
--- a/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean
+++ b/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean
@@ -133,6 +133,14 @@ def MappingCoherentAllKeys (fields : List Field) (s : ContractState) : Prop :=
 def MappingBasesNotDerived (fields : List Field) : Prop :=
   ∀ n : Nat, (fieldMapKindAt fields n).isSome → ∀ b k : Nat, solidityMappingSlot b k ≠ n
 
+/-- Layout certificate: every declared mapping base slot is an in-range EVM
+    storage key (`< 2^256`). Needed because `solidityMappingSlot_injective`
+    only separates in-range base slots: the ABI encoding reduces base slots
+    modulo `2^256` (`solidityMappingSlot_mod`). Not an axiom; discharged per
+    contract. -/
+def MappingBasesInRange (fields : List Field) : Prop :=
+  ∀ n : Nat, (fieldMapKindAt fields n).isSome → n < Compiler.Constants.evmModulus
+
 /-- `n` is not the flat image of any layout-derived mapping entry. -/
 def DerivedMappingSlotsAvoid (fields : List Field) (n : Nat) : Prop :=
   ∀ (k : StorageKey) (ch : Channel) (m : Nat),
@@ -233,6 +241,7 @@ theorem storageKeySlot_map2_of_kind {fields : List Field} {m : Nat} (k1 k2 : Add
 /-- The all-keys invariant follows from the three per-channel globals for
     **any** field layout: the non-mapping channels are definitional. -/
 theorem mappingCoherentAllKeys_of_globals (fields : List Field) (s : ContractState)
+    (hrange : MappingBasesInRange fields)
     (h1 : MappingCoherent s) (h2 : MappingCoherentUint s) (h3 : MappingCoherentMap2 s) :
     MappingCoherentAllKeys fields s := by
   intro k ch n h
@@ -249,14 +258,14 @@ theorem mappingCoherentAllKeys_of_globals (fields : List Field) (s : ContractSta
   | mapChain _ _ _ => simp [storageKeySlot] at h
   | transientMapChain _ _ => simp [storageKeySlot] at h
   | map m key =>
-      obtain ⟨_, rfl, rfl⟩ := storageKeySlot_map_eq h
-      exact h1 m key
+      obtain ⟨hk, rfl, rfl⟩ := storageKeySlot_map_eq h
+      exact h1 m key (hrange m (by rw [hk]; rfl))
   | mapUint m key =>
-      obtain ⟨_, rfl, rfl⟩ := storageKeySlot_mapUint_eq h
-      exact h2 m key
+      obtain ⟨hk, rfl, rfl⟩ := storageKeySlot_mapUint_eq h
+      exact h2 m key (hrange m (by rw [hk]; rfl))
   | map2 m k1 k2 =>
-      obtain ⟨_, rfl, rfl⟩ := storageKeySlot_map2_eq h
-      exact h3 m k1 k2
+      obtain ⟨hk, rfl, rfl⟩ := storageKeySlot_map2_eq h
+      exact h3 m k1 k2 (hrange m (by rw [hk]; rfl))
 
 /-- Instantiation at a declared address-keyed mapping. -/
 theorem mappingCoherentAllKeys_map {fields : List Field} {s : ContractState} {m : Nat}
@@ -279,10 +288,9 @@ theorem mappingCoherentAllKeys_map2 {fields : List Field} {s : ContractState} {m
   h (.map2 m k1 k2) _ _ (storageKeySlot_map2_of_kind k1 k2 hkind)
 
 theorem defaultState_mappingCoherentAllKeys (fields : List Field) :
-    MappingCoherentAllKeys fields defaultState :=
-  mappingCoherentAllKeys_of_globals fields defaultState
-    defaultState_mappingCoherent defaultState_mappingCoherentUint
-    defaultState_mappingCoherentMap2
+    MappingCoherentAllKeys fields defaultState := by
+  intro _ ch _ _
+  cases ch <;> rfl
 
 /-! ### Off-key write laws at the `storageWords` level
 
@@ -361,15 +369,20 @@ base slot is not itself keccak-derived (`MappingBasesNotDerived`). -/
 
 theorem nested_ne_simple {fields : List Field} {m b : Nat} {a k2 c : Nat}
     (hbases : MappingBasesNotDerived fields)
-    (hkind : (fieldMapKindAt fields b).isSome = true) :
+    (hkind : (fieldMapKindAt fields b).isSome = true)
+    (hb : b < Compiler.Constants.evmModulus) (hk2 : k2 < Compiler.Constants.evmModulus) (hc : c < Compiler.Constants.evmModulus) :
     abstractNestedMappingSlot m a k2 ≠ solidityMappingSlot b c := by
   intro heq
   simp only [abstractNestedMappingSlot, abstractMappingSlot] at heq
-  exact (hbases b hkind m a) (solidityMappingSlot_injective _ _ _ _ heq).1
+  exact (hbases b hkind m a)
+    (solidityMappingSlot_injective _ _ _ _
+      (solidityMappingSlot_lt_evmModulus m a) hk2 hb hc heq).1
 
-theorem simple_ne_of_base_ne {m b : Nat} {a c : Nat} (hb : m ≠ b) :
+theorem simple_ne_of_base_ne {m b : Nat} {a c : Nat}
+    (hm : m < Compiler.Constants.evmModulus) (ha : a < Compiler.Constants.evmModulus) (hb' : b < Compiler.Constants.evmModulus) (hc : c < Compiler.Constants.evmModulus)
+    (hb : m ≠ b) :
     solidityMappingSlot m a ≠ solidityMappingSlot b c := fun heq =>
-  hb (solidityMappingSlot_injective _ _ _ _ heq).1
+  hb (solidityMappingSlot_injective _ _ _ _ hm ha hb' hc heq).1
 
 /-! ### Preservation by the in-tree write helpers -/
 
@@ -379,6 +392,7 @@ theorem simple_ne_of_base_ne {m b : Nat} {a c : Nat} (hb : m ≠ b) :
 theorem writeMap_aligned_map_case (fields : List Field) (s : ContractState)
     (slot : Nat) (key : Address) (v : Uint256) (m : Nat) (key' : Address)
     (hkind' : fieldMapKindAt fields m = some (.simple .address))
+    (hslot : slot < Compiler.Constants.evmModulus) (hmlt : m < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherentAllKeys fields s) :
     ((s.writeMap slot key v).writeSlot
       (solidityMappingSlot slot (addressToWord key).val) v).storageMap m key' =
@@ -394,17 +408,18 @@ theorem writeMap_aligned_map_case (fields : List Field) (s : ContractState)
         intro heq; injection heq with _ hk'; exact hk hk'
       exact writeMap_aligned_other s m key v m key'
         (mappingCoherentAllKeys_map hcoh hkind' key') hne
-        (mappingAddrSlot_ne_of_map_ne hne)
+        (mappingAddrSlot_ne_of_map_ne hmlt hslot hne)
   · have hne : StorageKey.map m key' ≠ StorageKey.map slot key := by
       intro heq; injection heq with hm' _; exact hm hm'
     exact writeMap_aligned_other s slot key v m key'
       (mappingCoherentAllKeys_map hcoh hkind' key') hne
-      (mappingAddrSlot_ne_of_map_ne hne)
+      (mappingAddrSlot_ne_of_map_ne hmlt hslot hne)
 
 /-- The diagonal case of aligned `writeMapUint`. -/
 theorem writeMapUint_aligned_mapUint_case (fields : List Field) (s : ContractState)
     (slot : Nat) (key v : Uint256) (m : Nat) (key' : Uint256)
     (hkind' : fieldMapKindAt fields m = some (.simple .uint256))
+    (hslot : slot < Compiler.Constants.evmModulus) (hmlt : m < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherentAllKeys fields s) :
     ((s.writeMapUint slot key v).writeSlot
       (solidityMappingSlot slot key.val) v).storageMapUint m key' =
@@ -420,17 +435,18 @@ theorem writeMapUint_aligned_mapUint_case (fields : List Field) (s : ContractSta
         intro heq; injection heq with _ hk'; exact hk hk'
       exact writeMapUint_aligned_other s m key v m key'
         (mappingCoherentAllKeys_mapUint hcoh hkind' key') hne
-        (mappingUintSlot_ne_of_mapUint_ne hne)
+        (mappingUintSlot_ne_of_mapUint_ne hmlt hslot hne)
   · have hne : StorageKey.mapUint m key' ≠ StorageKey.mapUint slot key := by
       intro heq; injection heq with hm' _; exact hm hm'
     exact writeMapUint_aligned_other s slot key v m key'
       (mappingCoherentAllKeys_mapUint hcoh hkind' key') hne
-      (mappingUintSlot_ne_of_mapUint_ne hne)
+      (mappingUintSlot_ne_of_mapUint_ne hmlt hslot hne)
 
 /-- The diagonal case of aligned `writeMap2`. -/
 theorem writeMap2_aligned_map2_case (fields : List Field) (s : ContractState)
     (slot : Nat) (k1 k2 : Address) (v : Uint256) (m : Nat) (j1 j2 : Address)
     (hkind' : fieldMapKindAt fields m = some (.nested .address .address))
+    (hslot : slot < Compiler.Constants.evmModulus) (hmlt : m < Compiler.Constants.evmModulus)
     (hcoh : MappingCoherentAllKeys fields s) :
     ((s.writeMap2 slot k1 k2 v).writeSlot
       (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val)
@@ -449,17 +465,17 @@ theorem writeMap2_aligned_map2_case (fields : List Field) (s : ContractState)
           intro heq; injection heq with _ _ hj2; exact h2 hj2
         exact writeMap2_aligned_other s m k1 k2 v m j1 j2
           (mappingCoherentAllKeys_map2 hcoh hkind' j1 j2) hne
-          (mappingMap2Slot_ne_of_map2_ne hne)
+          (mappingMap2Slot_ne_of_map2_ne hmlt hslot hne)
     · have hne : StorageKey.map2 m j1 j2 ≠ StorageKey.map2 m k1 k2 := by
         intro heq; injection heq with _ hj1 _; exact h1 hj1
       exact writeMap2_aligned_other s m k1 k2 v m j1 j2
         (mappingCoherentAllKeys_map2 hcoh hkind' j1 j2) hne
-        (mappingMap2Slot_ne_of_map2_ne hne)
+        (mappingMap2Slot_ne_of_map2_ne hmlt hslot hne)
   · have hne : StorageKey.map2 m j1 j2 ≠ StorageKey.map2 slot k1 k2 := by
       intro heq; injection heq with hm' _ _; exact hm hm'
     exact writeMap2_aligned_other s slot k1 k2 v m j1 j2
       (mappingCoherentAllKeys_map2 hcoh hkind' j1 j2) hne
-      (mappingMap2Slot_ne_of_map2_ne hne)
+      (mappingMap2Slot_ne_of_map2_ne hmlt hslot hne)
 
 /-- Aligned `writeMap` + `writeSlot` preserves the global all-keys invariant.
     Cross-channel separation comes from the declared layout plus
@@ -469,11 +485,13 @@ theorem writeMap_aligned_preserves_mappingCoherentAllKeys
     (fields : List Field) (s : ContractState) (slot : Nat) (key : Address) (v : Uint256)
     (hkind : fieldMapKindAt fields slot = some (.simple .address))
     (hbases : MappingBasesNotDerived fields)
+    (hrange : MappingBasesInRange fields)
     (hcoh : MappingCoherentAllKeys fields s) :
     MappingCoherentAllKeys fields
       ((s.writeMap slot key v).writeSlot
         (solidityMappingSlot slot (addressToWord key).val) v) := by
   have hsome : (fieldMapKindAt fields slot).isSome = true := by rw [hkind]; rfl
+  have hslotlt := hrange slot hsome
   intro k ch n h
   cases k with
   | slot m => obtain ⟨rfl, rfl⟩ := storageKeySlot_slot_eq h; rfl
@@ -485,12 +503,14 @@ theorem writeMap_aligned_preserves_mappingCoherentAllKeys
   | 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
+      exact writeMap_aligned_map_case fields s slot key v m key' hkind' hslotlt
+        (hrange m (by rw [hkind']; rfl)) hcoh
   | mapUint m key' =>
       obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_mapUint_eq h
       have hm : m ≠ slot := base_ne_of_kind_ne hkind' hkind (by simp)
       have hslot : solidityMappingSlot m key'.val ≠
-          solidityMappingSlot slot (addressToWord key).val := simple_ne_of_base_ne hm
+          solidityMappingSlot slot (addressToWord key).val := simple_ne_of_base_ne
+            (hrange m (by rw [hkind']; rfl)) (Core.Uint256.isLt _) hslotlt (Core.Uint256.isLt _) hm
       have hcoh' := mappingCoherentAllKeys_mapUint hcoh hkind' key'
       simp only [channelRead_persistent, writeSlot_mapUint, writeMap_mapUint,
         writeSlot_slot_of_ne _ _ _ hslot, writeMap_slot]
@@ -500,7 +520,7 @@ theorem writeMap_aligned_preserves_mappingCoherentAllKeys
       have hslot :
           abstractNestedMappingSlot m (addressToWord k1).val (addressToWord k2).val ≠
             solidityMappingSlot slot (addressToWord key).val :=
-        nested_ne_simple hbases hsome
+        nested_ne_simple hbases hsome hslotlt (Core.Uint256.isLt _) (Core.Uint256.isLt _)
       have hcoh' := mappingCoherentAllKeys_map2 hcoh hkind' k1 k2
       simp only [channelRead_persistent, writeSlot_map2, writeMap_map2,
         writeSlot_slot_of_ne _ _ _ hslot, writeMap_slot]
@@ -510,10 +530,12 @@ theorem writeMapUint_aligned_preserves_mappingCoherentAllKeys
     (fields : List Field) (s : ContractState) (slot : Nat) (key v : Uint256)
     (hkind : fieldMapKindAt fields slot = some (.simple .uint256))
     (hbases : MappingBasesNotDerived fields)
+    (hrange : MappingBasesInRange fields)
     (hcoh : MappingCoherentAllKeys fields s) :
     MappingCoherentAllKeys fields
       ((s.writeMapUint slot key v).writeSlot (solidityMappingSlot slot key.val) v) := by
   have hsome : (fieldMapKindAt fields slot).isSome = true := by rw [hkind]; rfl
+  have hslotlt := hrange slot hsome
   intro k ch n h
   cases k with
   | slot m => obtain ⟨rfl, rfl⟩ := storageKeySlot_slot_eq h; rfl
@@ -527,19 +549,22 @@ theorem writeMapUint_aligned_preserves_mappingCoherentAllKeys
       obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map_eq h
       have hm : m ≠ slot := base_ne_of_kind_ne hkind' hkind (by simp)
       have hslot : solidityMappingSlot m (addressToWord key').val ≠
-          solidityMappingSlot slot key.val := simple_ne_of_base_ne hm
+          solidityMappingSlot slot key.val := simple_ne_of_base_ne
+            (hrange m (by rw [hkind']; rfl)) (Core.Uint256.isLt _) hslotlt (Core.Uint256.isLt _) hm
       have hcoh' := mappingCoherentAllKeys_map hcoh hkind' key'
       simp only [channelRead_persistent, writeSlot_map, writeMapUint_map,
         writeSlot_slot_of_ne _ _ _ hslot, writeMapUint_slot]
       exact hcoh'
   | mapUint m key' =>
       obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_mapUint_eq h
-      exact writeMapUint_aligned_mapUint_case fields s slot key v m key' hkind' hcoh
+      exact writeMapUint_aligned_mapUint_case fields s slot key v m key' hkind' hslotlt
+        (hrange m (by rw [hkind']; rfl)) hcoh
   | map2 m k1 k2 =>
       obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map2_eq h
       have hslot :
           abstractNestedMappingSlot m (addressToWord k1).val (addressToWord k2).val ≠
-            solidityMappingSlot slot key.val := nested_ne_simple hbases hsome
+            solidityMappingSlot slot key.val :=
+              nested_ne_simple hbases hsome hslotlt (Core.Uint256.isLt _) (Core.Uint256.isLt _)
       have hcoh' := mappingCoherentAllKeys_map2 hcoh hkind' k1 k2
       simp only [channelRead_persistent, writeSlot_map2, writeMapUint_map2,
         writeSlot_slot_of_ne _ _ _ hslot, writeMapUint_slot]
@@ -548,7 +573,9 @@ theorem writeMapUint_aligned_preserves_mappingCoherentAllKeys
 set_option maxHeartbeats 1600000 in
 theorem writeMap2_aligned_preserves_mappingCoherentAllKeys
     (fields : List Field) (s : ContractState) (slot : Nat) (k1 k2 : Address) (v : Uint256)
+    (hslotlt : slot < Compiler.Constants.evmModulus)
     (hbases : MappingBasesNotDerived fields)
+    (hrange : MappingBasesInRange fields)
     (hcoh : MappingCoherentAllKeys fields s) :
     MappingCoherentAllKeys fields
       ((s.writeMap2 slot k1 k2 v).writeSlot
@@ -567,7 +594,8 @@ theorem writeMap2_aligned_preserves_mappingCoherentAllKeys
       have hsome' : (fieldMapKindAt fields m).isSome = true := by rw [hkind']; rfl
       have hslot : solidityMappingSlot m (addressToWord key').val ≠
           abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val :=
-        fun heq => nested_ne_simple hbases hsome' heq.symm
+        fun heq => nested_ne_simple hbases hsome'
+          (hrange m hsome') (Core.Uint256.isLt _) (Core.Uint256.isLt _) heq.symm
       have hcoh' := mappingCoherentAllKeys_map hcoh hkind' key'
       simp only [channelRead_persistent, writeSlot_map, writeMap2_map,
         writeSlot_slot_of_ne _ _ _ hslot, writeMap2_slot]
@@ -577,14 +605,16 @@ theorem writeMap2_aligned_preserves_mappingCoherentAllKeys
       have hsome' : (fieldMapKindAt fields m).isSome = true := by rw [hkind']; rfl
       have hslot : solidityMappingSlot m key'.val ≠
           abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val :=
-        fun heq => nested_ne_simple hbases hsome' heq.symm
+        fun heq => nested_ne_simple hbases hsome'
+          (hrange m hsome') (Core.Uint256.isLt _) (Core.Uint256.isLt _) heq.symm
       have hcoh' := mappingCoherentAllKeys_mapUint hcoh hkind' key'
       simp only [channelRead_persistent, writeSlot_mapUint, writeMap2_mapUint,
         writeSlot_slot_of_ne _ _ _ hslot, writeMap2_slot]
       exact hcoh'
   | map2 m j1 j2 =>
       obtain ⟨hkind', rfl, rfl⟩ := storageKeySlot_map2_eq h
-      exact writeMap2_aligned_map2_case fields s slot k1 k2 v m j1 j2 hkind' hcoh
+      exact writeMap2_aligned_map2_case fields s slot k1 k2 v m j1 j2 hkind' hslotlt
+        (hrange m (by rw [hkind']; rfl)) hcoh
 
 /-- A lone flat `writeSlot` keeps the global invariant when the written word is
     not the image of any layout-derived mapping entry. Same image-avoidance

From c60c7b2fc3a727fb1dcf836d163fe3f05ea9d31d Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 29 Sep 2026 13:54:44 +0200
Subject: [PATCH 4/7] WIP: OwnedCounter range certificate, regenerate
 PrintAxioms

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Compiler/Proofs/Storage/MappingCoherentAllKeys.lean | 6 ++++--
 Contracts/OwnedCounter/Proofs/StorageCoherence.lean | 6 ++++++
 PrintAxioms.lean                                    | 8 +++++++-
 3 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean b/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean
index 8fd7e93b7a..067934e954 100644
--- a/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean
+++ b/Compiler/Proofs/Storage/MappingCoherentAllKeys.lean
@@ -370,7 +370,8 @@ base slot is not itself keccak-derived (`MappingBasesNotDerived`). -/
 theorem nested_ne_simple {fields : List Field} {m b : Nat} {a k2 c : Nat}
     (hbases : MappingBasesNotDerived fields)
     (hkind : (fieldMapKindAt fields b).isSome = true)
-    (hb : b < Compiler.Constants.evmModulus) (hk2 : k2 < Compiler.Constants.evmModulus) (hc : c < Compiler.Constants.evmModulus) :
+    (hb : b < Compiler.Constants.evmModulus) (hk2 : k2 < Compiler.Constants.evmModulus)
+    (hc : c < Compiler.Constants.evmModulus) :
     abstractNestedMappingSlot m a k2 ≠ solidityMappingSlot b c := by
   intro heq
   simp only [abstractNestedMappingSlot, abstractMappingSlot] at heq
@@ -379,7 +380,8 @@ theorem nested_ne_simple {fields : List Field} {m b : Nat} {a k2 c : Nat}
       (solidityMappingSlot_lt_evmModulus m a) hk2 hb hc heq).1
 
 theorem simple_ne_of_base_ne {m b : Nat} {a c : Nat}
-    (hm : m < Compiler.Constants.evmModulus) (ha : a < Compiler.Constants.evmModulus) (hb' : b < Compiler.Constants.evmModulus) (hc : c < Compiler.Constants.evmModulus)
+    (hm : m < Compiler.Constants.evmModulus) (ha : a < Compiler.Constants.evmModulus)
+    (hb' : b < Compiler.Constants.evmModulus) (hc : c < Compiler.Constants.evmModulus)
     (hb : m ≠ b) :
     solidityMappingSlot m a ≠ solidityMappingSlot b c := fun heq =>
   hb (solidityMappingSlot_injective _ _ _ _ hm ha hb' hc heq).1
diff --git a/Contracts/OwnedCounter/Proofs/StorageCoherence.lean b/Contracts/OwnedCounter/Proofs/StorageCoherence.lean
index 5fcc71555e..bfa076471b 100644
--- a/Contracts/OwnedCounter/Proofs/StorageCoherence.lean
+++ b/Contracts/OwnedCounter/Proofs/StorageCoherence.lean
@@ -137,6 +137,12 @@ theorem mappingBasesNotDerived : MappingBasesNotDerived ownedCounterFields := by
   rw [fieldMapKindAt_eq_none] at hn
   exact absurd hn (by simp)
 
+/-- Declared mapping base slots are in range — vacuous here as well. -/
+theorem mappingBasesInRange : MappingBasesInRange ownedCounterFields := by
+  intro n hn
+  rw [fieldMapKindAt_eq_none] at hn
+  exact absurd hn (by simp)
+
 /-- **Certificate 2.** No flat slot is the image of a derived mapping entry.
     Holds at *every* slot, so no `OwnedCounter` word write needs a side
     condition. -/
diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 28d1c42832..2ab04db45b 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -545,6 +545,7 @@ end Verity.AxiomAudit
   Contracts.OwnedCounter.Proofs.StorageCoherence.fieldMapKindAt_eq_none
   Contracts.OwnedCounter.Proofs.StorageCoherence.storageKeySlot_not_mappingEntry
   Contracts.OwnedCounter.Proofs.StorageCoherence.mappingBasesNotDerived
+  Contracts.OwnedCounter.Proofs.StorageCoherence.mappingBasesInRange
   Contracts.OwnedCounter.Proofs.StorageCoherence.derivedMappingSlotsAvoid
   Contracts.OwnedCounter.Proofs.StorageCoherence.constructor_preservesCoherence
   Contracts.OwnedCounter.Proofs.StorageCoherence.increment_preservesCoherence
@@ -5114,6 +5115,10 @@ end Verity.AxiomAudit
   Compiler.Proofs.LoopSimulation.forEach_sum_over_array
 
   -- Compiler/Proofs/MappingSlot.lean
+  Compiler.Proofs.evmYul_uint256_ofNat_mod
+  Compiler.Proofs.abiEncodeMappingSlot_mod
+  Compiler.Proofs.solidityMappingSlot_mod
+  Compiler.Proofs.solidityMappingSlot_injective_mod
   Compiler.Proofs.solidityMappingSlot_ne
   Compiler.Proofs.abstractMappingSlot_eq_solidity
   Compiler.Proofs.abstractMappingTag_eq_zero
@@ -5238,6 +5243,7 @@ end Verity.AxiomAudit
   Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_transientMapChain
   Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_map2
   Compiler.Proofs.Storage.MappingCoherence.addressToWord_injective
+  Compiler.Proofs.Storage.MappingCoherence.addressToWord_val_lt
   Compiler.Proofs.Storage.MappingCoherence.mappingAddrSlot_ne_of_map_ne
   Compiler.Proofs.Storage.MappingCoherence.mappingUintSlot_ne_of_mapUint_ne
   Compiler.Proofs.Storage.MappingCoherence.mappingMap2Slot_ne_of_map2_ne
@@ -7631,4 +7637,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 7045 theorems/lemmas (5032 public, 2013 private, 0 sorry'd)
+-- Total: 7051 theorems/lemmas (5038 public, 2013 private, 0 sorry'd)

From c62b601a26c8a2f0e5ad4000f1fcbea72221fc3c Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 29 Sep 2026 13:55:47 +0200
Subject: [PATCH 5/7] WIP: document range-restricted mapping-slot axiom

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 docs/AXIOMS.md            | 29 +++++++++++++++++++++++++++--
 docs/TRUST_ASSUMPTIONS.md |  2 +-
 2 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/docs/AXIOMS.md b/docs/AXIOMS.md
index f5fe526d3f..a40e2880af 100644
--- a/docs/AXIOMS.md
+++ b/docs/AXIOMS.md
@@ -34,7 +34,8 @@ mapping-chain constructors `StorageKey.mapChain` / `transientMapChain`
 separation a constructor fact.
 
 C5 step 4 is complete under `solidityMappingSlot_injective` below —
-collision-resistance of the 64-byte ABI mapping preimage, **not**
+collision-resistance of the 64-byte ABI mapping preimage (range-restricted
+to base slots and keys `< 2^256`), **not**
 injectivity of keccak256 on arbitrary byte strings. Finite-set
 slices remain valid without the axiom. Global aligned `writeMap*`
 preservation uses the axiom; lone `writeSlot` still takes an
@@ -79,12 +80,16 @@ assumed transition.
 
 ### 1. `solidityMappingSlot_injective`
 
-**Location**: `Compiler/Proofs/MappingSlot.lean:65`
+**Location**: `Compiler/Proofs/MappingSlot.lean:96`
 
 **Statement**:
 ```lean
 axiom solidityMappingSlot_injective
     (base₁ key₁ base₂ key₂ : Nat) :
+    base₁ < Compiler.Constants.evmModulus →
+    key₁ < Compiler.Constants.evmModulus →
+    base₂ < Compiler.Constants.evmModulus →
+    key₂ < Compiler.Constants.evmModulus →
     solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂ →
     base₁ = base₂ ∧ key₁ = key₂
 ```
@@ -97,6 +102,26 @@ layout makes the same collision-resistance assumption. This is **not**
 a claim that keccak256 is injective on all `ByteArray`s (256-bit
 output, infinite domain).
 
+**Why the range hypotheses (`< 2^256`) are required**: the ABI encoding
+`abiEncodeMappingSlot` passes both arguments through
+`EvmYul.UInt256.ofNat`, i.e. reduces them modulo `2^256`
+(proved as `solidityMappingSlot_mod`). An unrestricted statement over
+all `Nat` is therefore refutable: `solidityMappingSlot 0 (2^256) =
+solidityMappingSlot 0 0` holds by computation, and the old unbounded
+axiom yielded `2^256 = 0`, i.e. `False`. With the bounds, distinct
+`(base, key)` pairs give distinct 64-byte preimages, so the axiom is
+exactly collision-resistance on the hashed words. The bound-free
+consequence `solidityMappingSlot_injective_mod` gives equality modulo
+`2^256`.
+
+Consequences for callers: keys come from `Uint256.val` / `addressToWord`
+and are in range by construction; nested inner slots are keccak outputs
+(`solidityMappingSlot_lt_evmModulus`). Base slots are raw `Nat`s, so
+`MappingCoherent*` quantify only over base slots `< 2^256`, the aligned
+`writeMap*` preservation theorems take `slot < 2^256`, and the all-keys
+layer takes a `MappingBasesInRange` layout certificate (discharged per
+contract, like `MappingBasesNotDerived`).
+
 **Risk**: Medium. A keccak collision on this preimage family would
 make the global `MappingCoherent` preservation theorem false. Finite
 listed-pair certificates remain valid without the axiom.
diff --git a/docs/TRUST_ASSUMPTIONS.md b/docs/TRUST_ASSUMPTIONS.md
index 954f9a753f..cd80070edc 100644
--- a/docs/TRUST_ASSUMPTIONS.md
+++ b/docs/TRUST_ASSUMPTIONS.md
@@ -181,7 +181,7 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V
 
 ### 2. Lean Axioms
 - **Role**: Bridge remaining proof obligations not yet fully discharged.
-- **Status**: 1 documented axiom in [AXIOMS.md](AXIOMS.md): `solidityMappingSlot_injective` (collision-resistance of `keccak256(abi.encode(key, base))`, not keccak injectivity on all inputs). The mapping-slot *range* axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, the Layer 2 generic body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge remains an explicit theorem hypothesis rather than a Lean axiom.
+- **Status**: 1 documented axiom in [AXIOMS.md](AXIOMS.md): `solidityMappingSlot_injective` (collision-resistance of `keccak256(abi.encode(key, base))` for in-range base slots and keys `< 2^256`, not keccak injectivity on all inputs; the range hypotheses are required because the ABI encoding reduces its arguments modulo `2^256`, so the former unbounded statement was inconsistent). The mapping-slot *range* axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, the Layer 2 generic body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge remains an explicit theorem hypothesis rather than a Lean axiom.
 - **Mitigation**: CI axiom reporting and location checks enforce explicit tracking.
 
 ### 3. Keccak-based Selector Computation

From 313317b0cc631b6128e0004cd02a2cbf84112a8a Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 29 Sep 2026 14:32:21 +0200
Subject: [PATCH 6/7] docs: range restriction and MappingBasesInRange in AXIOMS
 / TRUST_ASSUMPTIONS / VERIFICATION_STATUS

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 docs/AXIOMS.md              | 3 ++-
 docs/TRUST_ASSUMPTIONS.md   | 6 ++++--
 docs/VERIFICATION_STATUS.md | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/docs/AXIOMS.md b/docs/AXIOMS.md
index a40e2880af..a7fc688c29 100644
--- a/docs/AXIOMS.md
+++ b/docs/AXIOMS.md
@@ -64,7 +64,8 @@ separation is the declared layout (`fieldMapKindAt` is a function of
 the base slot, so distinct mapping shapes force distinct base slots)
 plus the same `solidityMappingSlot_injective`. The simple-vs-nested
 cross case takes an explicit `MappingBasesNotDerived` layout
-certificate and a lone `writeSlot` takes `DerivedMappingSlotsAvoid`;
+certificate (together with `MappingBasesInRange`, the < 2^256 range of
+the declared mapping bases required by the bounded axiom) and a lone `writeSlot` takes `DerivedMappingSlotsAvoid`;
 both are hypotheses of the existing image-avoidance shape, discharged
 per contract. Dynamic-array element slots are **not** covered: the
 source and Yul derivations diverge and the collapse returns `none` at
diff --git a/docs/TRUST_ASSUMPTIONS.md b/docs/TRUST_ASSUMPTIONS.md
index cd80070edc..2c27026af8 100644
--- a/docs/TRUST_ASSUMPTIONS.md
+++ b/docs/TRUST_ASSUMPTIONS.md
@@ -537,8 +537,10 @@ Aligned `writeMap` / `writeMapUint` / `writeMap2` + `writeSlot`,
 takes the same image-avoidance `∀` (`DerivedMappingSlotsAvoid`). The
 simple-vs-nested cross case additionally takes an explicit per-contract
 layout certificate `MappingBasesNotDerived` (a declared mapping base
-slot is not itself keccak-derived) — a hypothesis discharged per
-contract, not an axiom. Under that invariant the lens read equals the
+slot is not itself keccak-derived) and `MappingBasesInRange` (declared
+mapping base slots are below 2^256, as the bounded
+`solidityMappingSlot_injective` requires) — hypotheses discharged per
+contract, not axioms. Under that invariant the lens read equals the
 flat `encodeStorageAt` read at the derived slot
 (`readMap_eq_encodeStorageAt_of_coherent` and the `mapUint` / `map2`
 variants), reusing the same non-occupation hypotheses `FieldEncode`
diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md
index 251e06814a..2db3920bea 100644
--- a/docs/VERIFICATION_STATUS.md
+++ b/docs/VERIFICATION_STATUS.md
@@ -228,7 +228,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 0 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules.
 5266 theorems/lemmas (3645 public, 1621 private) verified by `lake build PrintAxioms`.
 
-1 documented Lean axiom remains: `solidityMappingSlot_injective` (mapping-slot ABI preimage collision-resistance). The former mapping-slot *range* axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, the Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom. Layer 2 itself still has 0 axioms.
+1 documented Lean axiom remains: `solidityMappingSlot_injective` (mapping-slot ABI preimage collision-resistance, restricted to base slots and keys below 2^256; the unrestricted form over `Nat` was refutable because the ABI encoding reduces modulo 2^256). The former mapping-slot *range* axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, the Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom. Layer 2 itself still has 0 axioms.
 
 ## Differential Testing
 

From 53f8ac34e64228815eb2607b3913595e8caeaaa1 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 29 Sep 2026 14:59:13 +0200
Subject: [PATCH 7/7] chore: property manifest, exclusions and doc counts for
 mappingBasesInRange

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 artifacts/verification_status.json | 12 ++++++------
 docs-site/public/llms.txt          |  4 ++--
 docs/VERIFICATION_STATUS.md        | 16 ++++++++--------
 test/property_exclusions.json      |  1 +
 test/property_manifest.json        |  1 +
 5 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index 0032bfd165..2b67547992 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -16,10 +16,10 @@
   },
   "theorems": {
     "categories": 15,
-    "coverage_percent": 78,
+    "coverage_percent": 77,
     "covered": 255,
-    "excluded": 74,
-    "non_stdlib_total": 329,
+    "excluded": 75,
+    "non_stdlib_total": 330,
     "per_contract": {
       "Counter": 31,
       "ERC20": 22,
@@ -28,7 +28,7 @@
       "LocalObligationMacroSmoke": 4,
       "Ownable": 6,
       "Owned": 23,
-      "OwnedCounter": 63,
+      "OwnedCounter": 64,
       "OwnedCounterComposed": 6,
       "ReentrancyExample": 5,
       "ReentrancyRelyGuarantee": 10,
@@ -37,9 +37,9 @@
       "SimpleToken": 61,
       "Vault": 9
     },
-    "proven": 329,
+    "proven": 330,
     "stdlib": 0,
-    "total": 329
+    "total": 330
   },
   "toolchain": {
     "lean": "leanprover/lean4:v4.31.0",
diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt
index 7d7898a3a6..de8d699186 100644
--- a/docs-site/public/llms.txt
+++ b/docs-site/public/llms.txt
@@ -31,9 +31,9 @@ Every transition inside the proof envelope is either fully verified or recorded
 
 <!-- BEGIN GENERATED QUICK FACTS -->
 - **Language**: Lean 4.31.0
-- **Core Size**: 2810 lines
+- **Core Size**: 2813 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
+- **Theorems**: 330 across 15 categories, 330 fully proven
 - **Axioms**: 1 documented Lean axioms (see docs/AXIOMS.md)
 - **Tests**: 524 Foundry tests, 239 property tests
 - **Build**: `lake build` verifies all proofs
diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md
index 2db3920bea..13b1b6d734 100644
--- a/docs/VERIFICATION_STATUS.md
+++ b/docs/VERIFICATION_STATUS.md
@@ -31,7 +31,7 @@ EVM Bytecode
 | SafeCounter | 25 | Complete | `Contracts/SafeCounter/Proofs/` |
 | Owned | 23 | Complete | `Contracts/Owned/Proofs/` |
 | Ownable | 6 | Complete | `Contracts/Ownable/Proofs/` |
-| OwnedCounter | 63 | Complete | `Contracts/OwnedCounter/Proofs/` |
+| OwnedCounter | 64 | Complete | `Contracts/OwnedCounter/Proofs/` |
 | OwnedCounterComposed | 6 | Complete | `Contracts/OwnedCounterComposed/Proofs/` |
 | Ledger | 33 | Complete | `Contracts/Ledger/Proofs/` |
 | LocalObligationMacroSmoke | 4 | Baseline | `Contracts/LocalObligationMacroSmoke/Proofs/` |
@@ -42,9 +42,9 @@ EVM Bytecode
 | ReentrancyExample | 5 | Complete | `Contracts/ReentrancyExample/Contract.lean` |
 | ReentrancyRelyGuarantee | 10 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` |
 | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` |
-| **Total** | **329** | **✅ 100%** | — |
+| **Total** | **330** | **✅ 100%** | — |
 
-> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (329 total properties).
+> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (330 total properties).
 
 Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary. Higher-order internal helpers (function-pointer parameters, [#1747](https://github.com/lfglabs-dev/verity/issues/1747)) are eliminated by a compile-time monomorphization pre-pass that runs before any lowering, so the `CompilationModel` only ever contains first-order helpers: these calls are covered by the existing first-order proof path and introduce no new boundary trust.
 
@@ -209,7 +209,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 | Ledger | 100% (33/33) | 0 |
 | LocalObligationMacroSmoke | 100% (4/4) | 0 |
 | SimpleStorage | 95% (19/20) | 1 proof-only |
-| OwnedCounter | 70% (44/63) | 19 proof-only |
+| OwnedCounter | 69% (44/64) | 20 proof-only |
 | Owned | 87% (20/23) | 3 proof-only |
 | Ownable | 0% (0/6) | 6 proof-only |
 | OwnedCounterComposed | 0% (0/6) | 6 proof-only |
@@ -217,13 +217,13 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 | Counter | 74% (23/31) | 8 proof-only |
 | Stdlib | 0% (0/0) | 0 proof-only |
 
-**Status**: 78% coverage (255/329), 74 remaining exclusions all proof-only
+**Status**: 77% coverage (255/330), 75 remaining exclusions all proof-only
 
-- **Total Properties**: 329
+- **Total Properties**: 330
 - **Covered**: 255
-- **Excluded**: 74 (all proof-only)
+- **Excluded**: 75 (all proof-only)
 
-**Proof-Only Properties (74 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
+**Proof-Only Properties (75 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
 
 0 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules.
 5266 theorems/lemmas (3645 public, 1621 private) verified by `lake build PrintAxioms`.
diff --git a/test/property_exclusions.json b/test/property_exclusions.json
index b02ea2d277..2866bbb69c 100644
--- a/test/property_exclusions.json
+++ b/test/property_exclusions.json
@@ -45,6 +45,7 @@
   "increment_preservesCoherence",
   "increment_unfold",
   "isOwner_correct",
+  "mappingBasesInRange",
   "mappingBasesNotDerived",
   "run_preservesCoherence",
   "storageKeySlot_not_mappingEntry",
diff --git a/test/property_manifest.json b/test/property_manifest.json
index b43566798a..7b5d1f7685 100644
--- a/test/property_manifest.json
+++ b/test/property_manifest.json
@@ -191,6 +191,7 @@
     "increment_survives_transfer",
     "increment_unfold",
     "isOwner_correct",
+    "mappingBasesInRange",
     "mappingBasesNotDerived",
     "run_preservesCoherence",
     "storageKeySlot_not_mappingEntry",