feat: bytecode immutables (#1992)

[Th0rgal]

Summary

Implements issue #1992 — Solidity-style bytecode immutables.

• Adds Expr.immutable, Stmt.setImmutable, ImmutableSpec, and CompilationModel.immutables.
• Macro immutables stay out of storage fields; constructor initializers lower to setImmutable.
• Yul lowering emits loadimmutable(...) reads and deploy-side setimmutable(dataoffset("runtime"), ...).
• Layout / reporting / validation / trust / usage surfaces all account for immutables.
• Removes the INITIAL_CHAIN_ID slot-1024 hack.

Proofs

• Immutable semantics added to source/denote states; denote/source agreement proved for immutable reads and setImmutable.
• setImmutable wired through supported statement fragments, generic induction boundaries, end-to-end base cases, and generated transition summaries.

Test plan

• lake build Verity Contracts Compiler PrintAxioms → "Build completed successfully."
• scripts/refresh_verification_artifacts.sh → "[refresh] PASS"
• python3 scripts/check_proof_length.py → passed (no proof > 50 lines)
• make check → "All checks passed."
• zero sorry, zero axioms

---

Note

Medium Risk
Large compiler and proof surface change affecting generated contract bytecode; mitigated by strict validation and extensive tests, but incorrect lowering would affect all contracts using immutables.

Overview
Replaces the prior approach of hiding immutables in synthetic storage fields with Solidity-style bytecode immutables on CompilationModel.immutables.

The IR gains Expr.immutable and Stmt.setImmutable. Lowering emits loadimmutable for reads and deploy-side setimmutable(dataoffset("runtime"), …) for writes; setImmutable is rejected outside constructor/deploy (memory vs calldata dynamic source). Compile-time checks add duplicate immutable names, constructor-only initialization (every declared immutable must appear as Stmt.setImmutable in the constructor), and scoped name validation for reads/writes in functions vs constructor.

Layout reporting now includes an immutables array (bytecodeImmutable kind, zero storage footprint). Macro smoke tests and compile-driver tests were updated to expect the new surface instead of __immutable_* storage slots.

Formal semantics and proofs thread an immutable : String → Uint256 through runtime/denote state, prove denote/source agreement for immutable reads and setImmutable, and extend supported fragments, scope discipline, transition summaries, and end-to-end proof cases accordingly.

^{Reviewed by Cursor Bugbot for commit 1a19449. 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 10:49am

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

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 343b051. Configure here.}