Add typed unsafe Yul fragments to CompilationModel

[Th0rgal]

Summary

• adds a typed UnsafeYulFragment / RawYul escape hatch to CompilationModel.Stmt via Stmt.unsafeYul
• removes the dedicated Stmt.rawRevert path; one-off low-level instructions now live behind reusable UnsafeYulFragment helpers such as UnsafeYulFragment.rawRevert
• gives each fragment structured proof/audit metadata: UnsafeYulContracts, local obligations, LowLevelMechanic enum tags, ControlFlowSummary, and declared scope effects
• validates declared scope effects against the embedded Yul AST so fragments cannot silently under-report local binds, assignments, or storage writes
• centralizes lowering through unsafeYulToEVMYul, the single bridge from typed raw-Yul fragments to the backend EVMYul AST
• proves exact pass-through with unsafeYulToEVMYul_eq and compileStmt_unsafeYul
• moves trust/usage collectors toward generic StmtMetadata, Stmt.fold, and Stmt.foldList, reducing constructor-by-constructor duplication
• adds a YulImporter path for imported Solidity/Yul AST blocks to become explicit Stmt.unsafeYul fragments with generated metadata

Why

The SPHINCS- verifier models need to mirror Solidity handwritten assembly closely, including exact empty reverts and manually constructed Error(string) revert data. Adding a first-class Verity statement for every Yul instruction would grow the trusted surface and duplicate backend AST concepts. The cleaner boundary is a typed raw-Yul fragment: the model author supplies the Yul AST, and Verity requires the proof obligations, trust tags, termination/control-flow summary, and scope effects needed by validation and reports.

Architecture

• Verity Stmt remains separate from backend EVMYul YulStmt. The wrapper is intentional: backend Yul does not carry source-level proof obligations, trust metadata, or validation policy.
• Stmt.unsafeYul fragment embeds backend Yul AST statements, not raw Yul strings.
• Common stable primitives such as mstore, calldatacopy, and other semantically modeled operations remain first-class when they have proof/audit value.
• One-off low-level instructions should be helper constructors returning UnsafeYulFragments, not new Stmt constructors.
• The lowering proof is intentionally small: compileStmt_unsafeYul shows the compiler emits exactly fragment.stmts. The larger proof boundary is semantic: each fragment’s UnsafeYulContract and local obligations must be discharged by the model proof.

Verification

• lake build
• lake build Compiler.CompileDriverTest
• lake build Compiler.CompilationModel.Compile

---

Note

Medium Risk
Touches compiler lowering, validation, CEI, and trust-report surfaces for low-level/assembly code; semantic correctness still depends on discharging fragment obligations rather than full interpreter modeling.

Overview
This PR adds a typed raw-Yul escape hatch via Stmt.unsafeYul and UnsafeYulFragment, replacing ad-hoc paths like dedicated Stmt.rawRevert with helpers such as UnsafeYulFragment.rawRevert. Fragments carry EVMYul AST, local obligations, LowLevelMechanic tags, scope effects, control-flow/termination summaries, and optional UnsafeYulContract refinements; lowering is centralized in unsafeYulToEVMYul with a proved compileStmt_unsafeYul pass-through.

Validation and scope now require non-empty obligations, check declared scope effects against the embedded Yul AST (binds, assigns, storage writes), and integrate fragments into view/pure, CEI, untrackable writes, and scope validation. YulImporter turns imported Solidity/Yul blocks into Stmt.unsafeYul with derived metadata.

Trust reporting drops large per-constructor statement walks in favor of Stmt.fold / StmtMetadata, surfaces unsafeYulContracts in JSON, treats rawRevert as a denied mechanic, and merges fragment local obligations from function/constructor bodies. ControlFlowSummary drives “all paths return/revert” checks. Docs and tests cover the new boundary.

^{Reviewed by Cursor Bugbot for commit 0e50381. 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 30, 2026 8:23am

[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 0e50381. Configure here.}

[cursor]

Undeclared call mechanics bypass CEI

High Severity

validateUnsafeYulDeclaredScopeEffects cross-checks binds, assigns, and storage writes against the embedded Yul AST, but LowLevelMechanic tags are not. CEI and external-call detection for Stmt.unsafeYul rely only on fragment.mechanics, so a fragment whose Yul contains call/staticcall/delegatecall but omits those mechanics can skip interaction tracking and later persistent writes without a CEI error.

Additional Locations (2)

• Compiler/CompilationModel/Validation.lean#L40-L51
• Compiler/CompilationModel/Validation.lean#L883-L887

 

^{Reviewed by Cursor Bugbot for commit 0e50381. Configure here.}

[cursor]

Yul funcDef pollutes Verity scope

Medium Severity

yulStmtScopeEffects treats a nested Yul function definition name as a bindNames entry like a let. Scope validation then requires that name in declared effects and adds it to the enclosing Verity local scope, even though the name is an internal Yul callable, not a Verity local binding.

Additional Locations (1)

• Compiler/CompilationModel/ScopeValidation.lean#L568-L580

 

^{Reviewed by Cursor Bugbot for commit 0e50381. Configure here.}