proof: evaluate short mappingChain reads

[Th0rgal]

Summary

• add source semantics for one-key and two-key Expr.mappingChain reads, matching the existing mapping / mapping2 slot bridge behavior
• mirror the new short-chain cases in Verity.Core.Model.Denote
• extend DenoteAgreement so the denotational evaluator remains checked against SourceSemantics

Refs #2081.

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.SourceSemantics
• lean-slot lake build Compiler.Proofs.IRGeneration.DenoteAgreement
• git diff --check
• rg -n "\\bsorry\\b|\\badmit\\b|^\\s*axiom\\b" Compiler/Proofs/IRGeneration/SourceSemantics.lean Verity/Core/Model/Denote.lean Compiler/Proofs/IRGeneration/DenoteAgreement.lean

Remaining blockers

• Arbitrary 3+ key mappingChain reads are still deferred; they need shared list-recursion infrastructure for evaluating arbitrary key lists without restructuring the large evaluator unsafely.
• The coarse unsupported-state/helper surfaces still classify mapping-chain/storage surfaces conservatively; this PR only removes a local semantic gap for the one-key and two-key bridge cases.

---

Note

Low Risk
Proof-layer semantic extensions only; no runtime auth or IO. Remaining gap for 3+ key reads is unchanged and documented.

Overview
Implements one-key and two-key Expr.mappingChain read semantics in SourceSemantics, aligned with existing mapping / mapping2 slot hashing via abstractMappingSlot. The denotation interpreter in Verity.Core.Model.Denote mirrors the same cases (oracle mappingSlot instead of abstractMappingSlot).

DenoteAgreement splits the old catch-all mappingChain arm: empty lists and three-or-more keys stay unsupported (rfl); singleton and pair reads use bindAgree like other keyed expressions. Private evalExpr_mappingChain_singleton / _pair rfl lemmas and PrintAxioms entries track the new proof surface.

Documentation now states that only 0- and 3+-key chain reads remain outside the denotation fragment; 1- and 2-key reads are in scope. Arbitrary longer chains are still explicitly deferred pending list-recursion infrastructure.

^{Reviewed by Cursor Bugbot for commit 692253e. 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, Comment	Jul 3, 2026 12:49pm

[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_6316e9db-9de9-4a1f-82e7-32170dae3339)

[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_b348186f-fc13-40c9-a71b-94fed156c35f)

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

[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_e8f4ce74-8f30-4397-aa0a-8c5d58ffc4d3)