lfglabs-dev · Th0rgal · Aug 17, 2026 · Aug 17, 2026
@@ -363,7 +363,10 @@ sibling entrypoint.
   listed-vs-written slot inequality. A lone `writeTransient` preserves
   the same lists by constructor injectivity (`StorageKey.transient`
   vs persistent `.slot` / `.map` / `.mapUint` / `.map2`); no slot
-  inequality. Global (all-keys) preservation remains open.
+  inequality. Global aligned `writeMap`+`writeSlot` preservation of
+  `MappingCoherent` uses `solidityMappingSlot_injective`. Lone
+  `writeSlot` all-keys remains open. C5 step 4 is not axiom-free
+  complete.
   `FieldEncode` derives `findResolvedFieldAtSlot` from
   `findFieldWithResolvedSlot` plus no write-slot conflict, persistent,
   and unpacked, then identifies that slot with `encodeStorageAt`.

@@ -13,24 +13,17 @@ Axioms are exceptional. When an axiom exists, it must have:
 
 ## Current Axioms
 
-**None.** Verity has zero project-level Lean axioms.
-
-- Active axioms: 0
-
-The last remaining axiom (`solidityMappingSlot_lt_evmModulus`) was eliminated
-by replacing the opaque FFI-based keccak256 call with the kernel-computable
-Keccak engine (`Compiler/Keccak/Sponge.lean`), which exposes the 32-byte
-output-length guarantee to Lean's proof system.
+- Active axioms: 1
 
 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.
 
-C5 step 4's mapping-coherence, field-list, and finite-set slices
-likewise add no axiom: other-pair and finite-list preservation
-(address / uint / map2, including cross-channel lists) is
-hypothesized by an explicit derived-slot inequality, not by keccak
-injectivity. `FieldStorageKey` is a
+C5 step 4's finite-set slices still use explicit derived-slot
+inequalities. Global aligned-write `MappingCoherent` preservation
+depends on `solidityMappingSlot_injective` below — collision-resistance
+of the 64-byte ABI mapping preimage, **not** injectivity of keccak256
+on arbitrary byte strings. `FieldStorageKey` is a
 constructor match on `FieldType` / `isTransient`; struct-member
 slots add `wordOffset` via `mappingSlotLocation`. Compatibility
 `aliasSlots` are extra compiler slots, not extra source keys.
@@ -54,6 +47,40 @@ FunctionSpec call denotation (`DenoteFunctionCalls`), ETH-valued
 is an explicit `AdversaryModel` / `calleeStep` parameter, not an
 assumed transition.
 
+### 1. `solidityMappingSlot_injective`
+
+**Location**: `Compiler/Proofs/MappingSlot.lean:65`
+
+**Statement**:
+```lean
+axiom solidityMappingSlot_injective
+    (base₁ key₁ base₂ key₂ : Nat) :
+    solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂ →
+    base₁ = base₂ ∧ key₁ = key₂
+```
+
+**Justification**:
+`solidityMappingSlot base key` is `keccak256(abi.encode(key, base))` —
+a 64-byte ABI preimage. Distinct `(base, key)` pairs colliding would
+alias two Solidity mapping entries onto one EVM word. Solidity's
+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).
+
+**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.
+
+**CI validation**:
+- `scripts/check_axioms.py` location + count check
+- `DOCUMENTED_AXIOMS` in that script
+- Kernel Keccak output is already cross-checked against FFI/EVM keccak
+
+**Elimination path**:
+Replace with a theorem if a restricted-domain injectivity proof
+becomes available, or keep as an explicit cryptographic assumption
+and stop calling C5 step 4 axiom-free.
+
 ## Eliminated Axioms
 
 ### 1. `solidityMappingSlot_lt_evmModulus` (eliminated)
@@ -357,7 +384,7 @@ proof exists.
 
 ## Trust Summary
 
-- Active project-level axioms: 0
+- Active project-level axioms: 1
 - Production blockers from project-level axioms: 0
 - Consumer intrinsic obligations: owned and documented by consumer packages
 - Enforcement: `scripts/check_axioms.py` ensures this file tracks exact source locations.

@@ -13,7 +13,7 @@ Mapping slot abstraction used by proof interpreters.
 
 The active backend is keccak-faithful (`solidityMappingSlot`).
 
-## Axiom elimination (zero-axiom target)
+## Range axiom eliminated; slot collision-resistance is axiomatic
 
 The mapping-slot definition now uses the kernel-computable `KeccakEngine.keccak256`
 so that the output-length bound is structurally provable. The FFI version (`ffi.KEC`)
@@ -57,6 +57,25 @@ private def solidityMappingSlot_ffi (baseSlot key : Nat) : Nat :=
 def solidityMappingSlot (baseSlot key : Nat) : Nat :=
   EvmYul.fromByteArrayBigEndian (KeccakEngine.keccak256 (abiEncodeMappingSlot baseSlot key))
 
+/-- Collision-resistance of Solidity mapping-slot derivation
+    `keccak256(abi.encode(key, baseSlot))`.
+
+    **Not** injectivity of keccak256 on arbitrary `ByteArray`s (256-bit
+    output, infinite domain). See `AXIOMS.md`. -/
+axiom solidityMappingSlot_injective
+    (base₁ key₁ base₂ key₂ : Nat) :
+    solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂ →
+    base₁ = base₂ ∧ key₁ = key₂
+
+theorem solidityMappingSlot_ne {base₁ key₁ base₂ key₂ : Nat}
+    (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⟩
+  cases h with
+  | inl hbase => exact hbase hb
+  | inr hkey => exact hkey hk
+
 /-- Active proof-model mapping slot encoding backend. -/
 def abstractMappingSlot (baseSlot key : Nat) : Nat := solidityMappingSlot baseSlot key
 
@@ -250,6 +269,33 @@ theorem abstractMappingSlot_lt_evmModulus (baseSlot key : Nat) :
     abstractMappingSlot baseSlot key < Compiler.Constants.evmModulus :=
   solidityMappingSlot_lt_evmModulus baseSlot key
 
+theorem abstractNestedMappingSlot_injective
+    (base₁ key₁ key₂ base₂ key₁' key₂' : Nat)
+    (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
+        simpa [abstractNestedMappingSlot, abstractMappingSlot] using h)
+  rcases hinj with ⟨hinner, hkey2⟩
+  rcases solidityMappingSlot_injective base₁ key₁ base₂ key₁' hinner with ⟨hbase, hkey1⟩
+  exact ⟨hbase, hkey1, hkey2⟩
+
+theorem abstractNestedMappingSlot_ne
+    {base₁ key₁ key₂ base₂ key₁' key₂' : Nat}
+    (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
+    with ⟨hb, hk1, hk2⟩
+  rcases h with h | h | h
+  · exact h hb
+  · exact h hk1
+  · exact h hk2
+
 theorem solidityMappingSlot_add_lt_evmModulus (baseSlot key wordOffset : Nat)
     (h : wordOffset < Compiler.Constants.evmModulus - solidityMappingSlot baseSlot key) :
     solidityMappingSlot baseSlot key + wordOffset < Compiler.Constants.evmModulus := by

@@ -4,8 +4,8 @@
 
   Source `StorageKey` constructors stay injective. Keccak layout lives only
   here, on the compiler side. Global preservation of `MappingCoherent` is
-  not claimed: that needs finite non-alias certificates, because keccak
-  injectivity is not assumed.
+  not claimed without `solidityMappingSlot_injective`. That axiom is
+  ABI mapping-preimage collision-resistance, not keccak-on-all-bytes.
 -/
 
 import Verity.Core
@@ -194,4 +194,71 @@ theorem storageKeySlot_map2 (slot : Nat) (k1 k2 : Address) :
       some (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) :=
   rfl
 
+theorem addressToWord_injective {a b : Address}
+    (h : addressToWord a = addressToWord b) : a = b := by
+  apply Core.Address.ext
+  have hval :
+      a.toNat % Core.Uint256.modulus = b.toNat % Core.Uint256.modulus := by
+    simpa [addressToWord, Core.Uint256.val_ofNat] using
+      congrArg Core.Uint256.val h
+  have ha : a.toNat < Core.Uint256.modulus :=
+    Nat.lt_trans a.isLt (by decide : Core.ADDRESS_MODULUS < Core.Uint256.modulus)
+  have hb : b.toNat < Core.Uint256.modulus :=
+    Nat.lt_trans b.isLt (by decide : Core.ADDRESS_MODULUS < Core.Uint256.modulus)
+  rw [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at hval
+  simpa [Core.Address.toNat] using hval
+
+theorem mappingAddrSlot_ne_of_map_ne {slot slot' : Nat} {key key' : Address}
+    (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⟩
+  apply h
+  rw [hs, addressToWord_injective (Core.Uint256.ext hk)]
+
+theorem mappingUintSlot_ne_of_mapUint_ne {slot slot' : Nat} {key key' : Uint256}
+    (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⟩
+  apply h
+  rw [hs, Core.Uint256.ext hk]
+
+theorem mappingMap2Slot_ne_of_map2_ne
+    {slot slot' : Nat} {k1 k1' k2 k2' : Address}
+    (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
+    with ⟨hs, hk1, hk2⟩
+  apply h
+  rw [hs, addressToWord_injective (Core.Uint256.ext hk1),
+    addressToWord_injective (Core.Uint256.ext hk2)]
+
+/-- Global aligned-write preservation. Other-pair slot inequality comes
+    from `solidityMappingSlot_injective`, not from a listed certificate.
+    Not injectivity of keccak on all ByteArrays. -/
+theorem writeMap_aligned_preserves_mappingCoherent
+    (s : ContractState) (slot : Nat) (key : Address) (v : Uint256)
+    (hcoh : MappingCoherent s) :
+    MappingCoherent
+      ((s.writeMap slot key v).writeSlot
+        (solidityMappingSlot slot (addressToWord key).val) v) := by
+  intro slot' key'
+  by_cases hs : slot' = slot
+  · by_cases hk : key' = key
+    · simpa [hs, hk] using writeMap_aligned_same s slot key v
+    · 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)
+  · 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)
+
 end Compiler.Proofs.Storage.MappingCoherence
@@ -12,8 +12,9 @@
   constructor injectivity (`StorageKey.transient` vs persistent
   `.slot` / `.map` / `.mapUint` / `.map2`). No slot inequality.
 
-  This is not global preservation. A certificate for every pair would
-  be keccak injectivity on an unbounded preimage set.
+  Global `MappingCoherent` aligned-write preservation lives in
+  `MappingCoherence.writeMap_aligned_preserves_mappingCoherent` and
+  depends on `solidityMappingSlot_injective`. This file stays finite-set.
 -/
 
 import Compiler.Proofs.Storage.MappingCoherence

@@ -4637,6 +4637,7 @@ end Verity.AxiomAudit
   Compiler.Proofs.LoopSimulation.forEach_sum_over_array
 
   -- Compiler/Proofs/MappingSlot.lean
+  Compiler.Proofs.solidityMappingSlot_ne
   Compiler.Proofs.abstractMappingSlot_eq_solidity
   Compiler.Proofs.abstractMappingTag_eq_zero
   Compiler.Proofs.abstractDecodeMappingSlot_eq_none
@@ -4655,6 +4656,8 @@ end Verity.AxiomAudit
   Compiler.Proofs.solidityMappingSlot_lt_evmModulus
   Compiler.Proofs.mappingSlotLocation_zero
   Compiler.Proofs.abstractMappingSlot_lt_evmModulus
+  Compiler.Proofs.abstractNestedMappingSlot_injective
+  Compiler.Proofs.abstractNestedMappingSlot_ne
   Compiler.Proofs.solidityMappingSlot_add_lt_evmModulus
   Compiler.Proofs.solidityMappingSlot_add_wordOffset_lt_evmModulus
 
@@ -4738,6 +4741,11 @@ end Verity.AxiomAudit
   Compiler.Proofs.Storage.MappingCoherence.writeMap2_aligned_other
   Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_mapUint
   Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_map2
+  Compiler.Proofs.Storage.MappingCoherence.addressToWord_injective
+  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
+  Compiler.Proofs.Storage.MappingCoherence.writeMap_aligned_preserves_mappingCoherent
 
   -- Compiler/Proofs/Storage/MappingCoherenceOn.lean
   Compiler.Proofs.Storage.MappingCoherenceOn.mappingCoherentOn_of_mappingCoherent
@@ -6966,4 +6974,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 6458 theorems/lemmas (4588 public, 1870 private, 0 sorry'd)
+-- Total: 6466 theorems/lemmas (4596 public, 1870 private, 0 sorry'd)
@@ -16,7 +16,7 @@ Yul
 EVM Bytecode
 ```
 
-The repository currently has 0 `sorry` placeholders across the `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules that participate in the verified compiler stack. Layer 2 (Source → IR) and Layer 3 (IR → Yul) proof scripts are fully discharged, and it now has 0 documented Lean axioms. See [AXIOMS.md](AXIOMS.md) for details. Audit evidence and generated trust-boundary artifacts are indexed in [AUDIT.md](AUDIT.md).
+The repository currently has 0 `sorry` placeholders across the `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules that participate in the verified compiler stack. Layer 2 (Source → IR) and Layer 3 (IR → Yul) proof scripts are fully discharged, and it now has 1 documented Lean axiom (`solidityMappingSlot_injective`). See [AXIOMS.md](AXIOMS.md) for details. Audit evidence and generated trust-boundary artifacts are indexed in [AUDIT.md](AUDIT.md).
 
 ## What's Verified
 
@@ -38,7 +38,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**: 0 documented axioms in [AXIOMS.md](AXIOMS.md). 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))`, 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.
 - **Mitigation**: CI axiom reporting and location checks enforce explicit tracking.
 
 ### 3. Keccak-based Selector Computation
@@ -224,8 +224,11 @@ stays coherent under an aligned write when the list carries an
 explicit pairwise derived-slot certificate (`MappingCoherentOn` /
 `MappingCoherentUintOn` / `MappingCoherentMap2On`); that is not a
 global (all-keys) claim. Cross-channel preservation of another
-list likewise takes an explicit derived-slot inequality. Keccak
-injectivity is **not** assumed.
+list likewise takes an explicit derived-slot inequality. Global
+aligned `writeMap`+`writeSlot` preservation of `MappingCoherent`
+uses `solidityMappingSlot_injective` (64-byte ABI preimage
+collision-resistance). Keccak injectivity on arbitrary byte
+strings is **not** assumed.
 `storageArray` and `knownAddresses` are still separate fields.
 
 ### External-Call Journal (`ContractState.calls`)

@@ -4,7 +4,7 @@
     "example_contracts": 18
   },
   "proofs": {
-    "axioms": 0,
+    "axioms": 1,
     "sorry": 0
   },
   "schema_version": 1,

@@ -25,7 +25,7 @@ EDSL  -->  CompilationModel  -->  IR  -->  Yul  -->  EVM bytecode
 
 Every transition inside the proof envelope is either fully verified or recorded as an explicit assumption in the per-build trust report. The Yul-to-bytecode step is delegated to `solc --strict-assembly`.
 
-**Layer 2**: Generic whole-contract theorem for the supported fragment. 0 axioms. 0 documented Lean axioms remain (AXIOMS.md). Internal helper calls exist at the source level, and helper-summary proof reuse is available in source-semantics lemmas, but that reuse is not yet fully consumed through the generic body/IR theorem path. ECMs, typed interface calls, external calls, and low-level call/returndata mechanics are trust-reported or compiler-supported rather than fully proof-modeled. Constructors, fallback/receive, events/logs, typed errors, proxy/delegatecall, local obligations, and richer storage-layout features remain outside the generic proof fragment or partial. `forEach` proof support is partial: zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops are proved; positive non-empty loop bodies and nonliteral bounds are not yet proved.
+**Layer 2**: Generic whole-contract theorem for the supported fragment. 0 axioms. 1 documented Lean axiom remains project-wide (`solidityMappingSlot_injective`; Layer 2 still 0). Internal helper calls exist at the source level, and helper-summary proof reuse is available in source-semantics lemmas, but that reuse is not yet fully consumed through the generic body/IR theorem path. ECMs, typed interface calls, external calls, and low-level call/returndata mechanics are trust-reported or compiler-supported rather than fully proof-modeled. Constructors, fallback/receive, events/logs, typed errors, proxy/delegatecall, local obligations, and richer storage-layout features remain outside the generic proof fragment or partial. `forEach` proof support is partial: zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops are proved; positive non-empty loop bodies and nonliteral bounds are not yet proved.
 
 ## Quick facts
 
@@ -34,7 +34,7 @@ Every transition inside the proof envelope is either fully verified or recorded
 - **Core Size**: 1098 lines
 - **Verified Contracts**: 15 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault)
 - **Theorems**: 314 across 15 categories, 314 fully proven
-- **Axioms**: 0 documented Lean axioms (see AXIOMS.md)
+- **Axioms**: 1 documented Lean axiom (`solidityMappingSlot_injective`; see AXIOMS.md)
 - **Tests**: 528 Foundry tests, 239 property tests
 - **Build**: `lake build` verifies all proofs
 - **Repository**: https://github.com/lfglabs-dev/verity