Add target-fork conditional compilation

[Th0rgal]

Summary

Adds target-fork-aware conditional compilation for explicit intrinsic fallback paths.

The core design is a new pure expression form:

fork_if_at_least osaka then nativeExpr else fallbackExpr

Both branches are typechecked and validated, but the compile driver specializes the compilation model using --target-fork before intrinsic fork checks and Yul emission. This keeps intrinsic declarations strict: an Osaka intrinsic still hard-errors below Osaka unless it is in an unselected branch with an explicit fallback.

Architecture

• adds Expr.forkIfAtLeast required thenExpr elseExpr
• adds EDSL syntax and macro translation for fork_if_at_least
• specializes constructor/function bodies in compileSpecsWithOptions before ensureIntrinsicForksAllowed
• preserves fail-closed direct Yul lowering by rejecting unresolved forkIfAtLeast in compileExpr
• threads the new expression through validation, usage analysis, logical purity, ECM axiom collection, and IR proof bound-name analysis
• documents the pattern in the intrinsics reference

This intentionally avoids automatic intrinsic fallback metadata. The fallback remains visible in source, the intrinsic min_fork remains meaningful, and consumers own the equivalence obligation between branches.

Verification

• lake build Compiler.CompileDriverTest
• lake build Compiler.MainTest Compiler.CompileDriverTest Compiler.Proofs.IRGeneration.IntrinsicProofs Contracts.Smoke
• npm run build in docs-site
• make check

---

Note

Medium Risk
Changes compile-time fork specialization and intrinsic gating across the full compiler pipeline; incorrect branch selection or missed analysis cases could emit wrong Yul or weaken fork checks, though driver tests and explicit compileExpr rejection mitigate direct misuse.

Overview
Introduces Expr.forkIfAtLeast and EDSL fork_if_at_least, so authors can pair a newer-fork intrinsic with an emulated fallback while both branches stay typechecked.

compileSpecsWithOptions now runs specializeForkSpec on specs using --target-fork before intrinsic fork checks and Yul emission: the unselected branch is erased, so only the chosen path is subject to min_fork rules. Direct compileExpr still errors on unresolved forkIfAtLeast to keep Yul lowering fail-closed.

The new constructor is wired through validation, usage analysis, logical purity, ECM collection, macro translation, docs, compile-driver smoke tests (Cancun vs Osaka Yul), and IR proof surfaces (source semantics returns none until specialized; proof predicates treat it like other branching forms or as unsupported where appropriate). Default Lean elaboration of fork_if_at_least still reduces to the then branch unless consumers override.

^{Reviewed by Cursor Bugbot for commit 67df694. 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	May 27, 2026 11:13am

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