feat(proofs): axiomatize mapping-slot collision-resistance

[Th0rgal]

Summary

• add solidityMappingSlot_injective: keccak256(abi.encode(key, base)) does not collide on distinct (base, key) pairs
• not injectivity of keccak256 on arbitrary byte strings (256-bit output)
• prove writeMap_aligned_preserves_mappingCoherent (global aligned address-map write)
• register the axiom in AXIOMS.md, check_axioms.py, and Layer-2 docsync (Layer 2 stays 0 axioms)
• C5 step 4 is not axiom-free complete; lone writeSlot all-keys remains open

Test Plan

• lake build Compiler.Proofs.Storage.MappingCoherence
• make check

Related

C5 step 4 increment. Issue 2330 stays open.

---

Note

Medium Risk
Adds a cryptographic collision-resistance axiom used by global mapping-coherence preservation; a collision on the ABI mapping preimage family would falsify that theorem, though finite certificate paths remain axiom-free.

Overview
Reintroduces a single documented project axiom, solidityMappingSlot_injective, for collision-resistance of keccak256(abi.encode(key, base)) on distinct (base, key) pairs — not injectivity of keccak on arbitrary byte strings. The mapping-slot range property stays a proved theorem via the kernel Keccak engine.

On top of that axiom, the PR adds solidityMappingSlot_ne, nested abstractNestedMappingSlot_injective / _ne, and mapping-coherence lemmas (addressToWord_injective, distinct StorageKey.map* ⇒ distinct derived slots). It proves global preservation of address-keyed MappingCoherent under aligned writeMap + writeSlot (writeMap_aligned_preserves_mappingCoherent). Finite-list / certificate-based preservation in MappingCoherenceOn is unchanged and still does not need the axiom.

Trust and CI: AXIOMS.md, AUDIT.md, TRUST_ASSUMPTIONS.md, docs/ROADMAP.md, verification_status.json, llms.txt, and scripts/check_axioms.py / docsync.py now record 1 active axiom (Layer 2 compilation proofs remain 0 axioms). PrintAxioms registers the new theorems.

Docs explicitly state C5 step 4 is not axiom-free complete; lone writeSlot all-keys MappingCoherent preservation stays open.

^{Reviewed by Cursor Bugbot for commit 7ff15db. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview	Aug 17, 2026 8:29am

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, add credits to your account and enable them for code reviews in your settings.

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot 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_8e964919-ab6d-4f44-9705-d922eea63cc4)

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