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 fields in mapping structs across Denote and SourceSemantics; incorrect slot or bit masking would corrupt adjacent packed data, though behavior mirrors existing single-key packed mapping paths and is covered by agreement proofs and eval smoke.

Overview
Extends packed struct member storage semantics so setStructMember / setStructMember2 can update bitfield members inside mapping-backed structs, not only full-word members. Packed writes use read-modify-write via existing packedWordWrite; invalid PackedBits still revert.

Adds writeAddressKeyedMapping2PackedWordSlots for double-keyed mappings (nested slot resolution + packed update), mirrors it in SourceSemantics, and proves writeAddressKeyedMapping2PackedWordSlots_eq for denote/source agreement. PrintAxioms.lean picks up the new theorem (5197 total, still 0 sorry'd).

Adds PackedStructMemberDenoteSmoke: an ERC-4337-style packed DepositInfo word where updating stake preserves adjacent packed fields in the same storage word.

^{Reviewed by Cursor Bugbot for commit 139787b. 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 13, 2026 12:21am

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