feat(storage): thread mapping coherence through contract execution (#2330) - #2381
Merged
Conversation
…on (#2330) The all-keys shadow-vs-flat coherence invariant was only known to be preserved by individual write helpers. This carries it across whole entrypoint execution and instantiates it for a real contract. - `MappingCoherentExec`: layout-agnostic `PreservesCoherence`, closed under `>>=`/`pure`, `Contract.run` (both branches), the read-only primitives and the flat/address write primitives. - `OwnedCounter/Proofs/StorageCoherence`: discharges both layout certificates outright (the layout declares no mapping), proves every entrypoint preserves coherence, and concludes `coherent_of_genesis` — any call sequence from `defaultState` lands in a coherent state, no hypotheses.
The 15 new OwnedCounter storage-coherence theorems are Lean-model metatheory about the shadow/flat storage representation; they have no on-chain observable, so they are proof-only exclusions rather than differential-test targets. Regenerated the verification artifact and the doc figures that derive from it.
setMapping is shadow-only, so a mapping write falsifies MappingCoherentAllKeys under current semantics; the aligned preservation law on main describes the post-flip shape. Note that at both the framework and the contract instantiation, so the next reader does not re-derive it.
Member
Author
|
@codex review |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_2657eaa6-8cbb-45b2-9575-712e78f39881) |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 0/3 paquet(s) reviewés sémantiquement. 6 finding(s) (1 high / 1 medium / 4 low); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Compiler/Proofs/Storage/MappingCoherentExec.lean — timeout (spawnSync ocr ETIMEDOUT)
- Contracts/OwnedCounter/Proofs/StorageCoherence.lean — timeout (spawnSync ocr ETIMEDOUT)
- PrintAxioms.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 3 Lean file(s), 493 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 6/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 6 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 7 supported / 8 total; Lean 3, trust docs 0, workflow/scripts 3, contracts 0, docs 1
- Changed lines: 493 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 6; files 3; tokens 0; tool calls 0; warnings 1; duration 2461s
- Largest changed files: Contracts/OwnedCounter/Proofs/StorageCoherence.lean (+239/-0), Compiler/Proofs/Storage/MappingCoherentExec.lean (+164/-0), PrintAxioms.lean (+33/-1), test/property_exclusions.json (+15/-0), test/property_manifest.json (+15/-0)
Packet coverage
- Packet review: enabled; selected 6/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 6 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: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
- Covered packets:
- Compiler/Proofs/Storage/MappingCoherentExec.lean:1 score 102 [lenses: verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Does
MappingCoherentAllKeys(and hencePreservesCoherenceat L50) compare against an independently defined shadow semantics, or are both sides of the correspondence computed by the compiler's own read/write helpers — i.e., is the invariant near-tautological with respect to producer code? - Contracts/OwnedCounter/Proofs/StorageCoherence.lean:1 score 86 [lenses: verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Is
Call.step/runderived from (or proved equal to) the actual compiled contract semantics, or is it a fresh re-implementation controlled by this PR — and aremappingBasesNotDerived/derivedMappingSlotsAvoiddischarged from the producer's own layout definition rather than an independent layout certificate, making the end-to-end theorem self-referential? - PrintAxioms.lean:26 score 42 [lenses: provenance, environment-determinism, proof-soundness] — changed imports; ask: Confirm the import (pkt-3) and golden-list entries (pkt-5) jointly cover every public declaration added by StorageCoherence.lean, and identify what — if anything — fails the build when a proof module is added without both a matching import and complete list entries.
- PrintAxioms.lean:119 score 42 [lenses: provenance, environment-determinism, proof-soundness] — changed imports; ask: What mechanism enforces that every Compiler/Proofs/**/.lean and Contracts//Proofs/*.lean module is imported into PrintAxioms.lean — is there a CI completeness check, or could a future proof file (e.g., one leaning on keccak axioms) pass CI while never entering the audited set?
- PrintAxioms.lean:506 score 12 [lenses: provenance, verification-independence, environment-determinism, proof-soundness] — hotspot path/churn; ask: Does the check compare verityPrintAxioms output against this list in both directions (unexpected extra declarations and missing expected ones both fail), and are ALL new public theorems of StorageCoherence.lean (constructor/increment/decrement/transferOwnership/getCount/getOwner/Call.step/run/coherent_of_genesis plus the layout certificates) present in the audited set rather than a cherry-picked subset?
- PrintAxioms.lean:4905 score 12 [lenses: provenance, verification-independence, environment-determinism, proof-soundness] — hotspot path/churn; ask: Is this name list mechanically generated from the build or bidirectionally reconciled by CI (failing on both missing expected entries AND unmatched/extra declarations), or only hand-diffed — and does each of the 13 appended names correspond to a real declaration from MappingCoherentExec.lean whose axioms were actually printed and checked?
- Compiler/Proofs/Storage/MappingCoherentExec.lean:1 score 102 [lenses: verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Does
Pilot mode: advisory only. Codex Review remains the merge gate.
| representation flip makes `setMapping` aligned, this file can thread coherence | ||
| only through mapping-free entrypoints. -/ | ||
|
|
||
| end Compiler.Proofs.Storage.MappingCoherentExec |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| theorem coherent_of_genesis (calls : List Call) : Coherent (run calls defaultState) := | ||
| run_preservesCoherence calls (defaultState_mappingCoherentAllKeys ownedCounterFields) | ||
|
|
||
| end Contracts.OwnedCounter.Proofs.StorageCoherence |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| import Contracts.OwnedCounter.Proofs.Basic | ||
| import Contracts.OwnedCounter.Proofs.Correctness | ||
| import Contracts.OwnedCounter.Proofs.Isolation | ||
| import Contracts.OwnedCounter.Proofs.StorageCoherence |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| import Compiler.Proofs.Storage.MappingCoherence | ||
| import Compiler.Proofs.Storage.MappingCoherenceOn | ||
| import Compiler.Proofs.Storage.MappingCoherentAllKeys | ||
| import Compiler.Proofs.Storage.MappingCoherentExec |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| Contracts.OwnedCounter.Proofs.StorageCoherence.Call.step_preservesCoherence | ||
| Contracts.OwnedCounter.Proofs.StorageCoherence.run_preservesCoherence | ||
| Contracts.OwnedCounter.Proofs.StorageCoherence.coherent_of_genesis | ||
|
|
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_require | ||
| Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_setStorage | ||
| Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_setStorageAddr | ||
|
|
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
…erent-contract-level Reconciles C5 step 4 contract-level mapping coherence with main's #2085 slice 3 (bytes as a supported external parameter type, #2382). Only conflict was the generated tally line in PrintAxioms.lean; resolved by regenerating the file with scripts/generate_print_axioms.py so the theorem list is the union of both sides (6654 total, 4759 public, 1895 private, 0 sorry'd). No proof or gate was weakened.
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_51aca3e6-cd7e-4a02-a821-06dae0bbd380) |
Member
Author
|
@codex review |
|
To use Codex here, create a Codex account and connect to github. |
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 0/3 paquet(s) reviewés sémantiquement. 6 finding(s) (1 high / 1 medium / 4 low); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Compiler/Proofs/Storage/MappingCoherentExec.lean — timeout (spawnSync ocr ETIMEDOUT)
- Contracts/OwnedCounter/Proofs/StorageCoherence.lean — timeout (spawnSync ocr ETIMEDOUT)
- PrintAxioms.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 3 Lean file(s), 493 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 6/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 6 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 7 supported / 8 total; Lean 3, trust docs 0, workflow/scripts 3, contracts 0, docs 1
- Changed lines: 493 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 6; files 3; tokens 0; tool calls 0; warnings 1; duration 2464s
- Largest changed files: Contracts/OwnedCounter/Proofs/StorageCoherence.lean (+239/-0), Compiler/Proofs/Storage/MappingCoherentExec.lean (+164/-0), PrintAxioms.lean (+33/-1), test/property_exclusions.json (+15/-0), test/property_manifest.json (+15/-0)
Packet coverage
- Packet review: enabled; selected 6/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 6 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: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
- Covered packets:
- Compiler/Proofs/Storage/MappingCoherentExec.lean:1 score 102 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Cross-check the 13 declarations in this file against the names appended in PrintAxioms.lean (pkt-5/pkt-6): is any theorem missing from the manifest such that PreservesCoherence-based claims could be cited while their axiom dependencies remain unaudited?
- Contracts/OwnedCounter/Proofs/StorageCoherence.lean:1 score 86 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Which concrete axioms do mappingBasesNotDerived, derivedMappingSlotsAvoid, and run_preservesCoherence ultimately depend on, and does PrintAxioms output for every listed theorem in this file show only the accepted in-tree axiom set (no keccak assumption, propext-class surprises, or sorry) — i.e., is the claimed 'no hypotheses left open' actually pinned by the audited manifest?
- PrintAxioms.lean:26 score 42 [lenses: provenance, verification-independence, environment-determinism, proof-soundness] — changed imports; ask: Confirm every new theorem in StorageCoherence.lean is transitively reachable from this import AND appears in the hardcoded name list (pkt-5); is either reachability or list membership mechanically enforced anywhere in the repo?
- PrintAxioms.lean:121 score 42 [lenses: provenance, verification-independence, environment-determinism, proof-soundness] — changed imports; ask: Is PrintAxioms coverage driven solely by this manually maintained import list (no glob/auto-discovery over Compiler/Proofs/**), and is there any check that every new Compiler/Proofs/Storage/*.lean file gets imported and its theorems enumerated?
- PrintAxioms.lean:508 score 12 [lenses: provenance, verification-independence, environment-determinism, proof-soundness] — hotspot path/churn; ask: Does the enumeration added here cover EVERY public theorem introduced by Contracts/OwnedCounter/Proofs/StorageCoherence.lean (all *_preservesCoherence, Call.step_preservesCoherence, run_preservesCoherence, coherent_of_genesis, mappingBasesNotDerived, derivedMappingSlotsAvoid, etc.), and is there any mechanism that fails when a reachable theorem is missing from this manifest?
- PrintAxioms.lean:4960 score 12 [lenses: provenance, verification-independence, environment-determinism, proof-soundness] — hotspot path/churn; ask: Are all 13 declarations from Compiler/Proofs/Storage/MappingCoherentExec.lean (PreservesCoherence, preservesCoherence_bind/run/getStorage/getMapping/setStorage*/msgSender/require, etc.) present in this list, and what enforces list-to-artifact equality (e.g., a completeness check against the environment's declared constants) rather than hand-curated membership?
Pilot mode: advisory only. Codex Review remains the merge gate.
| representation flip makes `setMapping` aligned, this file can thread coherence | ||
| only through mapping-free entrypoints. -/ | ||
|
|
||
| end Compiler.Proofs.Storage.MappingCoherentExec |
Contributor
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.
Findings (3 lenses):
- Data & artifact provenance: Introduces the PreservesCoherence framework and 13 public theorems that downstream trust claims now cite; these are exactly the artifacts the hardcoded PrintAxioms manifest must pin, and the diff alone cannot show whether every declaration was added to the audited enumeration or only a curated subset.
- Ask the reviewer: Cross-check the 13 declarations in this file against the names appended in PrintAxioms.lean (pkt-5/pkt-6): is any theorem missing from the manifest such that PreservesCoherence-based claims could be cited while their axiom dependencies remain unaudited?
- Verification independence: The compositional framework advertised as closing the gap to 'contract-level' verification threads each primitive's preservation through the storage layer's own MappingCoherentAllKeys write-preservation lemmas; if the preservesCoherence_* proofs merely apply those producer results instead of re-deriving from the primitives' operational semantics, the end-to-end theorem only confirms self-consistency with the code being verified — a replay, not an independent check.
- Ask the reviewer: For each preservesCoherence_* lemma (especially setStorage/setStorageAddr at L136/L144 and getMapping at L115), does the proof re-derive coherence from the primitive's semantics, or does it
exact/apply the same MappingCoherentAllKeys lemmas produced by the storage layer under verification — and would a correlated mis-statement of the invariant or the per-write lemma be inherited silently?
- Ask the reviewer: For each preservesCoherence_* lemma (especially setStorage/setStorageAddr at L136/L144 and getMapping at L115), does the proof re-derive coherence from the primitive's semantics, or does it
- Lean proof soundness: Introduces the entire contract-level soundness framework (
PreservesCoherence, bind/pure/stateless/primitive lemmas) in one new file. The definition at L50 is the load-bearing predicate: if it only constrains the success branch ofContractResult, quantifies over an unsatisfiable pre-state class, or delegates the primitive cases (setStorage/setStorageAddr/require) to broad automation (simp/decidecollapsing to trivial), every downstream contract-level coherence theorem becomes vacuously tr- Ask the reviewer: Does
PreservesCoherence fields c(L50) quantify over allContractResultbranches including revert, and is the revert case ofpreservesCoherence_bind(L74) actually discharged rather than assumed? Do the primitive lemmas (L107-L144) avoidsorry/native_decide/axiomand avoid folding in hypotheses that make the predicate vacuous, and doespreservesCoherence_run(L93) match the real execution semantics?
Why flagged: public declaration/signature changed, changed imports; 164 changed line(s) near Compiler/Proofs/Storage/MappingCoherentExec.lean:1. Signals: public declaration/signature changed, changed imports.
Added-line sample:
- Ask the reviewer: Does
- L1:
/- - L2:
C5 step 4 (contract-level slice): threading ′MappingCoherentAllKeys′ - L3:
through ′Contract′ execution. - L4:
(empty) - L5:
′MappingCoherentAllKeys′ is preserved by the individual write helpers
| theorem coherent_of_genesis (calls : List Call) : Coherent (run calls defaultState) := | ||
| run_preservesCoherence calls (defaultState_mappingCoherentAllKeys ownedCounterFields) | ||
|
|
||
| end Contracts.OwnedCounter.Proofs.StorageCoherence |
Contributor
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.
Findings (3 lenses):
- Data & artifact provenance: New 239-line proof artifact whose trust story leans on an in-tree axiom set ('The in-tree axiom set gives collision resistance') while claiming the layout certificates are discharged 'from the layout itself, not from any keccak assumption'. The actual axiom dependencies of these theorems are only as traceable as the PrintAxioms manifest makes them; any theorem left off that manifest would let untracked axioms silently back the end-to-end coherence claim.
- Ask the reviewer: Which concrete axioms do mappingBasesNotDerived, derivedMappingSlotsAvoid, and run_preservesCoherence ultimately depend on, and does PrintAxioms output for every listed theorem in this file show only the accepted in-tree axiom set (no keccak assumption, propext-class surprises, or sorry) — i.e., is the claimed 'no hypotheses left open' actually pinned by the audited manifest?
- Verification independence: Headline claim of 'end-to-end ... no hypotheses left open' shadow-vs-flat coherence, yet the two layout certificates feed the very write laws imported from the producer storage layer, and the file itself notes reliance on an in-tree axiom set (L40) for collision resistance — a circular discharge of the certificates or axiom-carried dependence would make the claimed independent verification a replay of producer assumptions.
- Ask the reviewer: Are mappingBasesNotDerived (L132) and derivedMappingSlotsAvoid (L140) discharged by fresh computation over ownedCounterFields, or by appealing to lemmas/axioms from the same storage module whose write laws consume them (circular discharge)? Enumerate exactly which in-tree axioms coherent_of_genesis (L236) transitively rests on, and confirm it does not depend on the producer's own writeMap_aligned_* preservation lemmas as its only justification.
- Lean proof soundness: 239 new lines claiming end-to-end OwnedCounter coherence 'with no hypotheses left open', yet the file defines its own
Call/Call.step/runmodel (L192-L228) that may be a weaker proxy for the real entrypoints — a classic silent theorem weakening. The layout certificatesmappingBasesNotDerived(L132) andderivedMappingSlotsAvoid(L140) are the exact places a keccak/collision-resistance assumption or opaquedecidecould be smuggled in, and the in-file note 'The in-tree axiom set gives co- Ask the reviewer: Are
mappingBasesNotDerivedandderivedMappingSlotsAvoidproven purely fromownedCounterFieldswithout keccak/collision axioms,native_decide, or trusted layout certificates; is theCall/Call.step/runinductive model definitionally tied to the actualincrement/decrement/transferOwnershipentrypoints (not a weakened shadow); and doescoherent_of_genesis(L236) hold of the real genesis state rather than a convenientdefaultState?
Why flagged: public declaration/signature changed, changed imports; 239 changed line(s) near Contracts/OwnedCounter/Proofs/StorageCoherence.lean:1. Signals: public declaration/signature changed, changed imports.
Added-line sample:
- Ask the reviewer: Are
- L1:
/- - L2:
C5 step 4 (contract-level slice): ′OwnedCounter′ end-to-end shadow-vs-flat - L3:
storage coherence. - L4:
(empty) - L5:
′MappingCoherentAllKeys′ (see ′Compiler/Proofs/Storage/MappingCoherentAllKeys.lean′)
| import Contracts.OwnedCounter.Proofs.Basic | ||
| import Contracts.OwnedCounter.Proofs.Correctness | ||
| import Contracts.OwnedCounter.Proofs.Isolation | ||
| import Contracts.OwnedCounter.Proofs.StorageCoherence |
Contributor
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Findings (4 lenses):
- Data & artifact provenance: Mirror of pkt-4 on the contract side: Contracts.OwnedCounter.Proofs.StorageCoherence is only pulled into axiom auditing through this added import. The import manifest is manually scoped, so an unimported or later-swapped contract proof artifact escapes verification silently.
- Ask the reviewer: Confirm every new theorem in StorageCoherence.lean is transitively reachable from this import AND appears in the hardcoded name list (pkt-5); is either reachability or list membership mechanically enforced anywhere in the repo?
- Verification independence: Mirror of pkt-4 for the contract proof file: the import gates whether the independent axiom audit ever loads StorageCoherence; a traversal gap here means the headline end-to-end theorem is never checked for sorry/axiom dependence.
- Ask the reviewer: Does importing Contracts.OwnedCounter.Proofs.StorageCoherence put every new theorem into the audited environment (via transitive collection), or is audit coverage determined solely by the pkt-5 list — and is there any other axioms-check entry point (e.g., a separate expected-axiom file) that must be updated in lockstep?
- Environment determinism: Adds Contracts.OwnedCounter.Proofs.StorageCoherence to the same audit harness import set. The end-to-end soundness claim for OwnedCounter now depends on this file being swept for axioms; because audit scope is configured by manually synchronized in-repo lists rather than computed from the build, environments with drifted lists can verify a different theorem set than the one the committed verification_status. artifact describes.
- Ask the reviewer: Is there any CI mechanism that fails when the PrintAxioms import set or name lists drift from what the current toolchain/build actually produces, or is the audit scope only as complete as the last manual edit — i.e., can two environments disagree on whether StorageCoherence theorems were axiom-audited?
- Lean proof soundness: Wires the new contract-level proof file into the axiom-reporting tool. This import line is the only mechanism by which any axiom consumed by
Contracts.OwnedCounter.Proofs.StorageCoherencebecomes visible to audit; if the tool silently skips unimported or misspelled entries, an introduced axiom would go unreported.- Ask the reviewer: After this import is added, does
verityPrintAxiomsactually enumerate the axioms of the new StorageCoherence theorems, and does the tool error on unexpected axioms (e.g.,sorryAx) instead of only printing names that happen to be listed?
Why flagged: changed imports; 1 changed line(s) near PrintAxioms.lean:26. Signals: changed imports.
Added-line sample:
- Ask the reviewer: After this import is added, does
- L26:
import Contracts.OwnedCounter.Proofs.StorageCoherence
| import Compiler.Proofs.Storage.MappingCoherence | ||
| import Compiler.Proofs.Storage.MappingCoherenceOn | ||
| import Compiler.Proofs.Storage.MappingCoherentAllKeys | ||
| import Compiler.Proofs.Storage.MappingCoherentExec |
Contributor
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Findings (4 lenses):
- Data & artifact provenance: Hand-maintained import wiring that brings MappingCoherentExec into PrintAxioms' collection scope. The tool only audits artifacts reachable via its imports, so this line effectively scopes the verification claim: a future proof file added without a matching import here would silently fall outside the audit with no checksum or manifest failure.
- Ask the reviewer: Is PrintAxioms coverage driven solely by this manually maintained import list (no glob/auto-discovery over Compiler/Proofs/**), and is there any check that every new Compiler/Proofs/Storage/*.lean file gets imported and its theorems enumerated?
- Verification independence: This one-line import into the PrintAxioms audit tool is the sole mechanism placing MappingCoherentExec constants into the audited environment; if audit scope depends on hand-edited name lists instead of full traversal of imported files, unlisted constants escape the independent axiom/sorry check — a partial-view verification.
- Ask the reviewer: Does importing Compiler.Proofs.Storage.MappingCoherentExec guarantee the audit enumerates all of its declarations (including PreservesCoherence itself and every intermediate lemma), or only those also added to the name lists — and can any constant in the file evade axiom/sorry detection?
- Environment determinism: Adds Compiler.Proofs.Storage.MappingCoherentExec to the axiom-audit harness's import set. What the verification environment actually checks is defined by this in-repo import list plus manually maintained hardcoded name lists (see hunks near L508+ and L4960+), not by anything derived from the build itself; if sweep membership is list-driven rather than import-driven, the new contract-execution coherence theorems can silently escape axiom auditing in any checkout/CI run whose lists are stale, chan
- Ask the reviewer: Does verityPrintAxioms enumerate theorems from the import closure or only from the hardcoded name lists? Confirm whether adding this import alone guarantees the MappingCoherentExec theorems are audited in every environment, or whether a stale list / regenerated artifacts/verification_status. (possibly under an unpinned Lean toolchain) can report a verified verdict that differs between environments.
- Lean proof soundness: Adds the new compositional framework
MappingCoherentExecto the axiom-audit imports. Same trust-boundary concern as pkt-3: thePreservesCoherenceframework and its primitive lemmas must appear in the axiom report, or any hidden assumption in the bind/pure/stateless layer would be invisible to the audit pipeline.- Ask the reviewer: Does importing
Compiler.Proofs.Storage.MappingCoherentExeccause every public lemma in pkt-1 (especiallypreservesCoherence_bindand the setStorage lemmas) to be axiom-checked, and is there a CI gate that fails if the printed axiom set deviates from the expected in-tree axiom set?
Why flagged: changed imports; 1 changed line(s) near PrintAxioms.lean:121. Signals: changed imports.
Added-line sample:
- Ask the reviewer: Does importing
- L121:
import Compiler.Proofs.Storage.MappingCoherentExec
| Contracts.OwnedCounter.Proofs.StorageCoherence.Call.step_preservesCoherence | ||
| Contracts.OwnedCounter.Proofs.StorageCoherence.run_preservesCoherence | ||
| Contracts.OwnedCounter.Proofs.StorageCoherence.coherent_of_genesis | ||
|
|
Contributor
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Findings (4 lenses):
- Data & artifact provenance: Appends new OwnedCounter StorageCoherence theorem names to a hardcoded enumeration in PrintAxioms.lean (~L508) that functions as the manifest of proof terms whose axioms get audited. The manifest appears purely additive: nothing fails if a theorem from the newly added proof files is omitted, so a producer can silently add or swap proof artifacts outside the audited set, and there is no visible completeness enforcement tying the list to the actual declarations.
- Ask the reviewer: Does the enumeration added here cover EVERY public theorem introduced by Contracts/OwnedCounter/Proofs/StorageCoherence.lean (all *_preservesCoherence, Call.step_preservesCoherence, run_preservesCoherence, coherent_of_genesis, mappingBasesNotDerived, derivedMappingSlotsAvoid, etc.), and is there any mechanism that fails when a reachable theorem is missing from this manifest?
- Verification independence: The PrintAxioms audit's hand-maintained coverage/expected list is co-edited in the same PR as the proofs it audits — the verifier's expectations are producer-controlled, so completeness of this list determines whether the independent axiom/sorry audit actually inspects the new StorageCoherence theorems or passes on a partial view.
- Ask the reviewer: Confirm every new StorageCoherence theorem (constructor/increment/decrement/transferOwnership/getCount/getOwner_preservesCoherence, Call.step_preservesCoherence, run_preservesCoherence, coherent_of_genesis) is listed here with no omissions or misspellings, and that the check fails on unlisted/unknown constants rather than silently skipping them.
- Environment determinism: Hand-appends OwnedCounter theorem names to a hardcoded audit list. This list is effectively a configuration file embedded in the harness that determines which theorems the verification step covers; manual maintenance means coverage is environment/commit-dependent (a stale or partially updated list narrows what is verified with no error), and adjacent test/property_exclusions. can further narrow scope invisibly.
- Ask the reviewer: How is this Contracts/OwnedCounter list generated and kept in sync with the compiled environment — is it diffed against the actual import closure anywhere, and can a stale list plus test/property_exclusions. entries cause the audit to pass while the new StorageCoherence theorems are never actually checked?
- Lean proof soundness: Adds a new OwnedCounter section to what appears to be the declaration allowlist inside the axiom-audit tool. If this list is advisory rather than enforced, a new theorem with a
sorry/axiomcould be omitted by typo or deliberately excluded, hiding unsoundness; if enforced, the additions themselves define what gets audited.- Ask the reviewer: Is this declaration list exhaustive over the new
StorageCoherence.leantheorems, and does the tool fail (rather than silently skip) when a listed name is missing, misnamed, or when an unlisted declaration in the same module carries an axiom?
Why flagged: hotspot path/churn; 17 changed line(s) near PrintAxioms.lean:508. Signals: hotspot path/churn.
Added-line sample:
- Ask the reviewer: Is this declaration list exhaustive over the new
- L508:
-- Contracts/OwnedCounter/Proofs/StorageCoherence.lean - L509:
Contracts.OwnedCounter.Proofs.StorageCoherence.findResolvedFieldAtStorageSlot_go_mem - L510:
Contracts.OwnedCounter.Proofs.StorageCoherence.findResolvedFieldAtSlot_mem - L511:
Contracts.OwnedCounter.Proofs.StorageCoherence.fieldMapKindAt_eq_none - L512:
Contracts.OwnedCounter.Proofs.StorageCoherence.storageKeySlot_not_mappingEntry
| Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_require | ||
| Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_setStorage | ||
| Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_setStorageAddr | ||
|
|
Contributor
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Findings (4 lenses):
- Data & artifact provenance: Extends the second hardcoded manifest in PrintAxioms.lean (~L4960) with MappingCoherentExec-related compiler proof names. Same scoping hazard as pkt-5: the list gates which compiler proof terms get axiom-printed, so subset coverage or later silent additions/omissions go undetected and the 'axioms checked' trust claim can overstate what is actually pinned.
- Ask the reviewer: Are all 13 declarations from Compiler/Proofs/Storage/MappingCoherentExec.lean (PreservesCoherence, preservesCoherence_bind/run/getStorage/getMapping/setStorage*/msgSender/require, etc.) present in this list, and what enforces list-to-artifact equality (e.g., a completeness check against the environment's declared constants) rather than hand-curated membership?
- Verification independence: Same producer-co-edited list for the MappingCoherent* lemmas underpinning the new framework; if entries are incomplete or the expected-axiom allowlist was widened in this PR, the independent audit can pass without re-deriving the axiom dependencies of the constants the new contract-level proofs rely on.
- Ask the reviewer: Do these entries cover all lemmas MappingCoherentExec transitively uses (writeMap/writeMapUint/writeMap2_aligned_, writeSlot/writeAddrSlot/writeTransient preservation, readMap_eq_encodeStorageAt_of_coherent), and does the audit recompute the dependency closure from the environment rather than trusting this hand-edited list — i.e., was the expected-axiom allowlist itself unchanged in this PR?
- Environment determinism: Hand-appends Compiler.Proofs.Storage theorem names to a second hardcoded audit list. Same determinism exposure as pkt-5: the set of theorems whose axiom usage is asserted is fixed by manual edits, so what is 'verified' varies with list state rather than being reproducibly derived from the build; regeneration of artifacts/verification_status. from this list makes the recorded verdict sensitive to list/toolchain state at generation time.
- Ask the reviewer: Does this Compiler.Proofs.Storage list feed verification_status. or any gate, and is its regeneration pinned to an exact Lean/toolchain version so output is deterministic across environments — or can different environments regenerate divergent 'verified' artifacts from the same commit?
- Lean proof soundness: Extends the compiler-side declaration list adjacent to the
MappingCoherentGlobalentries, presumably registering the newMappingCoherentExectheorems. Completeness of this registration determines whether the pkt-1 framework is actually covered by the axiom audit — a gap here would let an unsound shortcut in the new file evade the only axiom-detection mechanism.- Ask the reviewer: Do the added entries cover every public declaration from
MappingCoherentExec.lean(includingPreservesCoherenceauxiliary lemmas), and is the list mechanically derived from the module or hand-maintained (hand-maintenance being the silent-exclusion risk)?
Why flagged: hotspot path/churn; 13 changed line(s) near PrintAxioms.lean:4960. Signals: hotspot path/churn.
Added-line sample:
- Ask the reviewer: Do the added entries cover every public declaration from
- L4960:
-- Compiler/Proofs/Storage/MappingCoherentExec.lean - L4961:
Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_of_stateless - L4962:
Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_pure - L4963:
Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_bind - L4964:
Compiler.Proofs.Storage.MappingCoherentExec.preservesCoherence_run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the contract-level slice of #2330 (C5 storage flip, étape 4).
What this changes
MappingCoherentAllKeys— the global shadow-vs-flat storage invariant landedin #2380 — was only known to be preserved by individual write helpers. That is
a statement about single state updates; it said nothing about running a whole
entrypoint, and no contract had discharged the two layout certificates.
Two new files close that distance.
Compiler/Proofs/Storage/MappingCoherentExec.lean(layout-agnostic, 165 lines)PreservesCoherence fields csays the actioncmaps coherent pre-states tocoherent post-states, and it is made compositional:
preservesCoherence_bind— closure underdosequencing, covering therevert branch as well as the success branch;
preservesCoherence_run— transfer toContract.run, whose revert branchrestores the (coherent) pre-call snapshot, so the guarantee is unconditional
on success or revert;
preservesCoherence_of_stateless— every read-only primitive in one step;preservesCoherence_setStorage/_setStorageAddr— the write primitives,reduced to the write-helper laws. Only
setStoragecarries a side condition(
DerivedMappingSlotsAvoid); address writes land on a differentStorageKeyconstructor and need none.
PreservesCoherenceis deliberately stated on the raw actionc srather thanContract.run c s, so that it composes acrossbind.Contracts/OwnedCounter/Proofs/StorageCoherence.lean(contract instantiation)ownedCounterFieldsmirrors the declaredstorageblock;mappingBasesNotDerivedandderivedMappingSlotsAvoiddischarge bothlayout certificates outright — from the layout itself, not from any keccak
assumption. They reduce to
fieldMapKindAt_eq_none, which needs the newmembership lemma
findResolvedFieldAtSlot_mem(slot resolution only everreturns a declared field);
Call/Call.step/rungive the external surface, andcoherent_of_genesisruns an arbitrary sequence of entrypoints fromdefaultStateand concludes coherence of the final state, with nohypotheses.
#print axioms Contracts.OwnedCounter.Proofs.StorageCoherence.coherent_of_genesisgives
[propext, Classical.choice, Quot.sound]— nosolidityMappingSlot_injective,no new axioms, zero
sorry.Scope: why a mapping-free contract
Worth being explicit, since it bounds what this closes. Two things block a
mapping-bearing layout, in order of severity, and both are documented in-tree
next to the code:
setMappingis shadow-only —ContractState.writeMapupdates
storageWords (.map b k)and never the flat slotsolidityMappingSlot b k. A mapping write therefore falsifiesMappingCoherentAllKeystoday. The preservation law on main,writeMap_aligned_preserves_mappingCoherentAllKeys, is stated for thealigned write
(s.writeMap ..).writeSlot (solidityMappingSlot ..) v— thepost-flip shape that no EDSL primitive emits yet. So the missing
preservesCoherence_setMappingis not hard, it is false under currentsemantics, and this is a step-3 dependency rather than a proof gap.
MappingBasesNotDerivedneedssolidityMappingSlot _ _ ≠ bat each declared mapping base slot. The treehas collision resistance (
solidityMappingSlot_injective) and an upperbound (
solidityMappingSlot_lt_evmModulus); neither implies the derivedimage misses the small declared-slot region. A mapping-bearing contract
would carry the certificates as explicit hypotheses.
The execution-threading framework is layout-agnostic and gets reused verbatim
once aligned writes land. Dynamic arrays are untouched (documented-unsupported;
storageKeySlotreturnsnoneat dynamic-array roots).Bookkeeping
The 15 new
OwnedCountertheorems are Lean-model metatheory about the storagerepresentation with no on-chain observable, so they are registered as
proof-only exclusions rather than differential-test targets. That moves the
headline coverage figure 81% → 78% (255/329) purely by growing the denominator;
covered count is unchanged. Manifest, exclusions, verification artifact and the
derived doc figures are regenerated by their own scripts.
Receipts
lake buildlake build PrintAxiomsmake checkAll checks passed.scripts/check_storage_lens_freeze.pyscripts/generate_print_axioms.py --checkscripts/generate_trust_surface_report.py --check@[implemented_by]=1, unchangedsorryaddedTest plan
lake buildclean from a warm cachelake build PrintAxiomsclean; axiom audit shows the three standard Lean axioms onlymake checkgreen end to endnative_decide/implemented_bydelta)Note
Low Risk
Lean proof-only additions with no runtime, auth, or compiler behavior changes; bookkeeping lowers reported property-test coverage without reducing covered tests.
Overview
Adds contract-level preservation for the
MappingCoherentAllKeysshadow-vs-flat storage invariant, which previously held only for single write helpers.MappingCoherentExec.leanintroducesPreservesCoherenceand compositional lemmas (bind,Contract.run, stateless reads,setStoragewithDerivedMappingSlotsAvoid,setStorageAddr). It documents whysetMappinghas no preservation lemma under current shadow-only semantics.OwnedCounter/Proofs/StorageCoherence.leaninstantiates the layout (owner/count), proves both layout certificates without keccak hypotheses (mapping-free), shows every entrypoint preserves coherence, and closes withcoherent_of_genesis: arbitrary call sequences fromdefaultStatestay coherent.Registers 15 new OwnedCounter theorems in
PrintAxiomsand marks them proof-only in property manifests (coverage 81%→78% from denominator growth). Updates verification artifacts and docs counts (314→329 theorems).Reviewed by Cursor Bugbot for commit 3250143. Bugbot is set up for automated code reviews on this repo. Configure here.