Skip to content

fix(trust): range-restrict solidityMappingSlot_injective (unrestricted form is inconsistent) #2460

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
Th0rgal merged 7 commits into from
Sep 29, 2026
Merged

fix(trust): range-restrict solidityMappingSlot_injective (unrestricted form is inconsistent) #2460

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
7ce0be9
WIP: range-restrict solidityMappingSlot_injective
Th0rgal Sep 29, 2026
b3087ea
WIP: propagate range hypotheses to storage coherence callers
Th0rgal Sep 29, 2026
60ffaed
WIP: range hypotheses through MappingCoherentAllKeys
Th0rgal Sep 29, 2026
c60c7b2
WIP: OwnedCounter range certificate, regenerate PrintAxioms
Th0rgal Sep 29, 2026
c62b601
WIP: document range-restricted mapping-slot axiom
Th0rgal Sep 29, 2026
313317b
docs: range restriction and MappingBasesInRange in AXIOMS / TRUST_ASS…
Th0rgal Sep 29, 2026
53f8ac3
chore: property manifest, exclusions and doc counts for mappingBasesI…
Th0rgal Sep 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
79 changes: 73 additions & 6 deletions Compiler/Proofs/MappingSlot.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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₂ →
Comment on lines +98 to 102

@chatgpt-codex-connector chatgpt-codex-connector Bot Sep 29, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Replace the still-inconsistent injectivity axiom

Even with these bounds, the axiom remains mathematically inconsistent: its domain contains 2^256 × 2^256 = 2^512 (base, key) pairs, while solidityMappingSlot_lt_evmModulus proves that every result lies in a set of only 2^256 slots. The finite pigeonhole principle therefore guarantees two distinct bounded pairs with equal outputs, contradicting this axiom and allowing False to be derived. To restore soundness, collision assumptions must be limited to the finite pairs actually used (for example via explicit non-alias certificates), rather than universally quantifying over every bounded pair.

Useful? React with 👍 / 👎.

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
Expand Down Expand Up @@ -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
Expand Down
9 changes: 6 additions & 3 deletions Compiler/Proofs/Storage/FieldCoherence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
9 changes: 6 additions & 3 deletions Compiler/Proofs/Storage/FieldEncode.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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}
Expand Down
Loading
Loading