Bitfield-packed struct storage writes in mappings (#1976)

[Th0rgal]

Summary

• Adds packed setStructMember / setStructMember2 write semantics for bitfield-packed structs stored in mappings, with a nested packed mapping-struct helper for read-modify-write slot updates.
• Proves the denote/source agreement theorem writeAddressKeyedMapping2PackedWordSlots_eq and regenerates PrintAxioms.lean (zero new axioms, 0 sorry'd).
• Adds an ERC-4337-style regression: packed DepositInfo word update preserving adjacent fields (Compiler/CompilationModelFeatureTest.lean).

Closes #1976.

Test plan

• lake build Verity Contracts Compiler PrintAxioms → "Build completed successfully."
• make check → "All checks passed."
• Proof length check passed (no proof >50 lines)
• CI green

---

Note

Medium Risk
Changes contract storage semantics for packed struct writes in mappings across Denote and SourceSemantics; incorrect bit masking or slot resolution would affect verified behavior, though changes mirror existing single-key packed paths and include agreement proofs.

Overview
Extends Denote and SourceSemantics so setStructMember / setStructMember2 can update bitfield-packed fields inside structs stored in mappings, not only full-word members. Packed writes use read-modify-write via packedWordWrite and revert when packedBitsValid fails.

Adds writeAddressKeyedMapping2PackedWordSlots for double-nested mapping keys (mirroring the existing single-key packed helper), wires it through all relevant execStmt paths, and proves writeAddressKeyedMapping2PackedWordSlots_eq in DenoteAgreement (registered in PrintAxioms.lean).

Adds a PackedStructMemberDenoteSmoke #eval regression: updating one packed field in a mapping struct word leaves adjacent packed fields unchanged (ERC-4337-style DepositInfo layout).

^{Reviewed by Cursor Bugbot for commit fa4aef2. 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	Jun 17, 2026 7:14am

[github-actions]

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

[Th0rgal]

bugbot run

[cursor]

✅ Bugbot reviewed your changes and found no new issues!

Comment @cursor review or bugbot run to trigger another review on this PR

^{Reviewed by Cursor Bugbot for commit 8d91aa9. Configure here.}