fix(trust): range-restrict solidityMappingSlot_injective (unrestricted form is inconsistent) - #2460
Conversation
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…UMPTIONS / VERIFICATION_STATUS Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c62b601a26
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| base₁ < Compiler.Constants.evmModulus → | ||
| key₁ < Compiler.Constants.evmModulus → | ||
| base₂ < Compiler.Constants.evmModulus → | ||
| key₂ < Compiler.Constants.evmModulus → | ||
| solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂ → |
There was a problem hiding this comment.
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 👍 / 👎.
…nRange Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 0/4 paquet(s) reviewés sémantiquement. 5 finding(s) (3 high / 2 medium); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Compiler/Proofs/Storage/MappingCoherentAllKeys.lean — timeout (spawnSync ocr ETIMEDOUT)
- docs/AXIOMS.md — timeout (spawnSync ocr ETIMEDOUT)
- docs/TRUST_ASSUMPTIONS.md — timeout (spawnSync ocr ETIMEDOUT)
- docs/VERIFICATION_STATUS.md — timeout (spawnSync ocr ETIMEDOUT)
📝 1 groupe(s) de paquets au-delà du budget n'ont eu que le triage scout.
Large Lean diff routed to bounded packet review: 8 Lean file(s), 428 changed supported line(s). Multi-lens scout (1/4 lens(es): proof-soundness) surfaced 5/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 5 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v11)
- Changed files: 14 supported / 15 total; Lean 8, trust docs 2, workflow/scripts 3, contracts 0, docs 1
- Changed lines: 428 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 5; tokens 0; tool calls 0; warnings 1; duration 3265s
- Largest changed files: Compiler/Proofs/Storage/MappingCoherence.lean (+68/-48), Compiler/Proofs/Storage/MappingCoherentAllKeys.lean (+63/-31), Compiler/Proofs/MappingSlot.lean (+73/-6), Compiler/Proofs/Storage/MappingCoherenceOn.lean (+23/-12), docs/AXIOMS.md (+29/-3)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness (3 lens(es) failed; union of the rest used); rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 5 scout-ranked packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.
- Strong packet-review blocker: Selected packets require semantic review; see packet review outcomes for actual coverage.
- Covered packets:
- Compiler/Proofs/Storage/MappingCoherentAllKeys.lean:372 score 177 [lenses: proof-soundness] — theorem statement changed/possibly weakened, theorem/public statement changed, public declaration/signature changed; ask: Were the newly added
evmModulusbound hypotheses onnested_ne_simple(and sibling theorems in this file) strictly necessary after the range-axiom elimination, and can every existing call site still discharge them — i.e., is any theorem now vacuous, unprovable at call sites, or its conclusion (full cross-channel key separation) weaker than before? - docs/AXIOMS.md:67 score 172 [lenses: proof-soundness] — introduced/changed axiom, trust-boundary docs drift, public declaration/signature changed; ask: Does the new combined certificate documented here correspond to a Lean definition that genuinely discharges the range obligation, or does it just re-import the eliminated range axiom as a per-theorem hypothesis — and does
#print axiomson every touched theorem confirm the documented 'no new axiom' claim? - docs/TRUST_ASSUMPTIONS.md:184 score 137 [lenses: proof-soundness] — introduced/changed axiom, trust-boundary docs drift; ask: Can the reviewer confirm — via the (also-modified) PrintAxioms tooling, not the docs — that the axiom count is genuinely 1 and that no new
axiom,sorry,admit, ornative_decideaccompanied the range-axiom elimination described in this line? - docs/VERIFICATION_STATUS.md:212 score 75 [lenses: proof-soundness] — introduced/changed axiom; ask: Does the newly excluded OwnedCounter property (exclusion #20) correspond to a theorem whose statement was weakened or whose proof was dropped/deferred as a consequence of the mapping-coherence hypothesis restructuring in this PR?
- Compiler/Proofs/Storage/MappingCoherence.lean:228 score 68 [lenses: proof-soundness] — public declaration/signature changed; ask: Do the rewritten write-preservation and slot-separation theorems here still conclude unconditional disjointness, or are conclusions now conditioned on
evmModulusbounds that the preservation lemmas never establish — and does any proof in this window usesimp/broad automation to paper over the now-missing range reasoning?
- Compiler/Proofs/Storage/MappingCoherentAllKeys.lean:372 score 177 [lenses: proof-soundness] — theorem statement changed/possibly weakened, theorem/public statement changed, public declaration/signature changed; ask: Were the newly added
Pilot mode: advisory only. Codex Review remains the merge gate.
| 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 |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [high]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: Core proof-soundness hotspot: nested_ne_simple gains three new caller-supplied bounds (hb/hk2/hc : < evmModulus) on top of the existing MappingBasesNotDerived certificate, matching a file-wide pattern where facts formerly discharged by the eliminated mapping-slot range axiom are pushed into theorem hypotheses. Three statement-change signals (score 177) indicate multiple conclusions in this window were re-scoped; the added hypotheses may be over-strong, unprovable at call sites, or may leav
Ask the reviewer: Were the newly added evmModulus bound hypotheses on nested_ne_simple (and sibling theorems in this file) strictly necessary after the range-axiom elimination, and can every existing call site still discharge them — i.e., is any theorem now vacuous, unprovable at call sites, or its conclusion (full cross-channel key separation) weaker than before?
Why flagged: theorem statement changed/possibly weakened, theorem/public statement changed, public declaration/signature changed; 66 changed line(s) near Compiler/Proofs/Storage/MappingCoherentAllKeys.lean:372. Signals: theorem statement changed/possibly weakened, theorem/public statement changed, public declaration/signature changed.
Added-line sample:
- L372:
(hkind : (fieldMapKindAt fields b).isSome = true) - L373:
(hb : b < Compiler.Constants.evmModulus) (hk2 : k2 < Compiler.Constants.evmModulus) - L374:
(hc : c < Compiler.Constants.evmModulus) : - L378:
exact (hbases b hkind m a) - L379:
(solidityMappingSlot_injective _ _ _ _
| `writeMap*` preservation theorems take `slot < 2^256`, and the all-keys | ||
| layer takes a `MappingBasesInRange` layout certificate (discharged per | ||
| contract, like `MappingBasesNotDerived`). | ||
|
|
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [high]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: The axiom ledger is being rewritten in the same PR: AXIOMS.md claims the range axiom is eliminated and replaced by layout certificates (MappingBasesNotDerived, DerivedMappingSlotsAvoid, plus a truncated new combined 'Map...' certificate). If those certificates merely re-encode the eliminated axiom as proof hypotheses (per pkt-1/pkt-5), the 'adds no axiom' claims are trust-boundary drift masking weakened theorems; the doc must be reconciled against actual #print axioms output, especially si
Ask the reviewer: Does the new combined certificate documented here correspond to a Lean definition that genuinely discharges the range obligation, or does it just re-import the eliminated range axiom as a per-theorem hypothesis — and does #print axioms on every touched theorem confirm the documented 'no new axiom' claim?
Why flagged: introduced/changed axiom, trust-boundary docs drift, public declaration/signature changed; 29 changed line(s) near docs/AXIOMS.md:67. Signals: introduced/changed axiom, trust-boundary docs drift, public declaration/signature changed.
Added-line sample:
- L67:
certificate (together with ′MappingBasesInRange′, the < 2^256 range of - L68:
the declared mapping bases required by the bounded axiom) and a lone ′writeSlot′ takes ′DerivedMappingSlotsAvoid′; - L84:
**Location**: ′Compiler/Proofs/MappingSlot.lean:96′ - L90:
base₁ < Compiler.Constants.evmModulus → - L91:
key₁ < Compiler.Constants.evmModulus →
| ### 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. |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [high]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: Trust doc now asserts exactly one remaining axiom (solidityMappingSlot_injective) and that the range axiom was 'eliminated via the kern...' (truncated). This is the headline trust claim for the whole PR; if the elimination was achieved by weakening theorem statements rather than proving the range facts, the claimed axiom reduction is illusory and downstream consumers will rely on an inaccurate trust boundary.
Ask the reviewer: Can the reviewer confirm — via the (also-modified) PrintAxioms tooling, not the docs — that the axiom count is genuinely 1 and that no new axiom, sorry, admit, or native_decide accompanied the range-axiom elimination described in this line?
Why flagged: introduced/changed axiom, trust-boundary docs drift; 2 changed line(s) near docs/TRUST_ASSUMPTIONS.md:184. Signals: introduced/changed axiom, trust-boundary docs drift.
Added-line sample:
- L184:
- **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
| 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. |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [medium]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: Lower-priority but suspicious correlation: OwnedCounter coverage drops 70%→69% with one additional 'proof-only' exclusion (19→20) in the same PR that restructures storage-coherence theorem statements and touches Contracts/OwnedCounter/Proofs/StorageCoherence.lean (+6). A newly excluded obligation added while proofs churn may hide a theorem that no longer holds under the new hypotheses.
Ask the reviewer: Does the newly excluded OwnedCounter property (exclusion #20) correspond to a theorem whose statement was weakened or whose proof was dropped/deferred as a consequence of the mapping-coherence hypothesis restructuring in this PR?
Why flagged: introduced/changed axiom; 12 changed line(s) near docs/VERIFICATION_STATUS.md:212. Signals: introduced/changed axiom.
Added-line sample:
- L212:
| OwnedCounter | 69% (44/64) | 20 proof-only | - L220:
**Status**: 77% coverage (255/330), 75 remaining exclusions all proof-only - L222:
- **Total Properties**: 330 - L224:
- **Excluded**: 75 (all proof-only) - L226:
**Proof-Only Properties (75 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
| (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 |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [medium]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: Same hypothesis-stuffing pattern in the primary mapping-coherence file: mappingAddrSlot_ne_of_map_ne gains (hs' : slot' < evmModulus) and 99 changed lines across 4 hunks rewrite the write-preservation lemmas (writeMap*_aligned_other) whose file outline signatures also changed. If slot-range facts now live only in caller-side hypotheses, the preservation proofs may silently rely on bounds that the write lemmas themselves never verify, hollowing out the disjointness guarantees.
Ask the reviewer: Do the rewritten write-preservation and slot-separation theorems here still conclude unconditional disjointness, or are conclusions now conditioned on evmModulus bounds that the preservation lemmas never establish — and does any proof in this window use simp/broad automation to paper over the now-missing range reasoning?
Why flagged: public declaration/signature changed; 99 changed line(s) near Compiler/Proofs/Storage/MappingCoherence.lean:228. Signals: public declaration/signature changed.
Added-line sample:
- L228:
theorem addressToWord_val_lt (a : Address) : - L229:
(addressToWord a).val < Compiler.Constants.evmModulus := - L230:
(addressToWord a).isLt - L231:
(empty) - L233:
(hs' : slot' < Compiler.Constants.evmModulus)
1 participant
Problem
solidityMappingSlot_injectivewas quantified over allNatbase slots and keys. ButabiEncodeMappingSlotencodes both throughEvmYul.UInt256.ofNat, which reduces modulo 2^256. SosolidityMappingSlot 0 0 = solidityMappingSlot 0 (2^256), and the axiom gives0 = 2^256, i.e.False.Fix
solidityMappingSlot_mod(proved): the derivation only sees its arguments modulo 2^256.base₁ key₁ base₂ key₂ < evmModulus. This is collision resistance on the 64-byte ABI words that are actually hashed.solidityMappingSlot_injective_mod: an unbounded consequence stated modulo 2^256.Uint256/Addressvalues and from the < 2^256 range of derived slots:solidityMappingSlot_ne, nested slots,FieldCoherence,FieldEncode,MappingCoherence,MappingCoherenceOn,MappingCoherentAllKeys, OwnedCounter. The OwnedCounter certificate gains a range fact.docs/AXIOMS.mdstates the bounded form and the reason.PrintAxioms.leanis regenerated (--checkOK).No new axiom,
sorryornative_decide. Found while reviewing #2459.🤖 Generated with Claude Code