[Trust Reduction] Symbolic mapChain channel for hashed nested/struct mappings (G2 residual)

[Th0rgal]

Summary

Closes #2456 (G2 residual; follow-up to #2416 / #2432).

Hashed nested / word-offset / struct mapping words now execute on a dedicated symbolic storage channel, not on .slot at the keccak slot. In the executable plane, separating two entries is a matter of constructor injectivity:

• New StorageKey constructors: mapChain (slot : Nat) (keys : List Nat) (offset : Nat) and transientMapChain (slot : Nat) (keys : List Nat).

• Lenses (Verity/Core.lean): ContractState.readMapChain / writeMapChain / storageMapChain, plus readTransientMapChain / writeTransientMapChain / transientStorageMapChain.

• Routed through the new channel (Contracts/Common.lean): getMappingN / setMappingN, getTransientMappingN / setTransientMappingN, getMappingWord / setMappingWord, structMemberAt / structMember2At / setStructMemberAt / setStructMember2At, and therefore also structMembers destructuring. Packed members still do read-modify-write on the same entry.

• Lens laws:

  • read-after-write: readMapChain_writeMapChain_same, readMapChain_writeMapChain (simp, as an if), and _of_ne / _keys_ne / _offset_ne / _slot_ne;
  • independence: storage_writeMapChain, readSlot_writeMapChain, readMapChain_writeSlot / _writeAddrSlot / _writeMap / _writeMapUint / _writeMap2 / _writeTransient / _writeArray, the transient counterparts, and context-field frames.

• Hops: both keys are plain non-slot keys (isPlainNonSlot), so enterHop / exitHop / hopCall / hopCallView namespace them per contract via StorageKey.scoped. New lemmas: enterHop_readMapChain, exitHop_readMapChain, storageWords_scoped_writeMapChain, readMapChain_exitHop_enterHop_of_frame, writeMapChain_enterHop_frame. Revert rollback covers these keys because they are part of storageWords.

• Transient: Transactions.isTransientKey clears transientMapChain at transaction start.

• Interpretation, no axiom:

  • Compiler.Proofs.mappingChainSlotLocation (fold keccak + offset mod 2^256), _single / _pair / _zero;
  • mappingChainSlot_eq_location, structSlot_eq_location, structSlot2_eq_location;
  • the new Compiler/Proofs/Storage/HashedMappingLayout.lean: HashedCoherentOn relates the channel to the flat .slot channel the model plane reads. It is preserved by aligned writes (alignedWrite_preserves), by scalar writes that avoid the tracked locations (writeSlot_preserves), and by the other channels' writes. It takes a finite LayoutNonAlias certificate (layoutNonAlias_of_certificate from the existing StorageSlotNonAliasCertificate) instead of solidityMappingSlot_injective. Transient chains have the analogue TransientHashedCoherentOn. MappingCoherence.storageKeySlot maps mapChain to its Solidity location.

• Smoke (Contracts/Smoke/HashedMappings.lean) proves the following through the generated functions:

  • key-vs-key separation (requestOf_other_after_setRequest);
  • mapping-vs-scalar separation in both directions (setRequest_leaves_scalar, requestOf_after_setWithdrawn);
  • struct members (receiptOf_after_setReceipt, setReceipt_leaves_request_and_scalar);
  • transient (acquire_leaves_storage, locked_after_acquire);
  • hop frame (hop_setRequest_frame).

  All of them depend only on propext / Classical.choice / Quot.sound.

Migration. Contract-level statements that used s.writeSlot (mappingChainSlot base keys) v, s.storage (structSlot base k w) or s.writeTransient (mappingChainSlot ..) v should now use s.writeMapChain base (MappingKeyWord.words keys) 0 v (with keys written as words: [user.toNat, epoch.val]), s.readMapChain base [k] w, or s.writeTransientMapChain base keys v. Separation lemmas no longer need slot-inequality hypotheses. mappingChainSlot / structSlot / structSlot2 remain as layout (interpretation) definitions.

Note (found while doing this, not fixed here): solidityMappingSlot_injective as stated over all Nat is inconsistent. abiEncodeMappingSlot reduces keys mod 2^256, so solidityMappingSlot 0 0 = solidityMappingSlot 0 (2^256) is provable axiom-free, and the axiom then yields False (repro in #2456). This PR adds no uses of the axiom. Restricting it to < 2^256 inputs should be done separately.

Test Plan

• lake build Verity Contracts Compiler StorageLayoutReport PrintAxioms (2811 jobs) passes.
• make check passes: storage-lens freeze unchanged (new lenses go through withStorageWords), print-axioms / verification-status / macro property-test artifacts regenerated.
• lake env lean PrintAxioms.lean + scripts/check_axioms.py --log passes. The new smoke / layout lemmas use only the three standard axioms.
• Lean warning count for touched files is unchanged vs artifacts/lean_warning_baseline.json.

Related Issues

Closes #2456. Refs #2416, #2432, #2441.

🤖 Generated with Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-28T21:00:31.672453Z	7007b4c	PR opened

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 7007b4cbda

ℹ️ 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".

[chatgpt-codex-connector]

Preserve the flat-slot coherence on mapping writes

Route this write through the coherence bridge (or integrate an equivalent two-state simulation): starting from defaultState, which satisfies HashedCoherentOn [e], setting a nonzero value here updates only .mapChain while storage_writeMapChain leaves the Solidity slot unchanged, so coherence is immediately false. HashedMappingLayout.alignedWrite_preserves only covers alignedWrite, and that operation is not used by this or the other changed mapping setters; consequently the executable contract can return the new value while the Denote/Yul model still reads the old flat-slot value, leaving the new proofs disconnected from compiled behavior.

Useful? React with 👍 / 👎.

[github-actions]

\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```

[Th0rgal]

CI note: the only failing step is Check Solidity slice imports and mutation regressions → HARNESS ERROR: mutation positive control failed: denote-panic-selector. It fails identically on main @ 9d0d56a (run 36374679612, job 108778320002), so it is pre-existing and unrelated to this PR. All Lean builds / checks for this PR pass.

🤖 Generated with Claude Code

[Th0rgal]

CI note: the only failing job (build → "Check Solidity slice imports and mutation regressions", HARNESS ERROR: mutation positive control failed: denote-panic-selector) fails identically on main since 2026-09-26 (e.g. run 36374679612, job 108778320002). It is unrelated to this PR; all other checks pass and the full lake build + make check pass locally.

🤖 Generated with Claude Code

[Th0rgal]

CI note: the only failing step, build › Check Solidity slice imports and mutation regressions (check_solidity_differential.sh --mutations --mutant denote-panic-selector), also fails on main at 9d0d56a (https://github.com/lfglabs-dev/verity/actions/runs/36374679612), i.e. it predates this PR. All other checks pass.

🤖 Generated with Claude Code