Prototype verity_intrinsic support for CLZ

[Th0rgal]

Summary

Prototype verity_intrinsic support for CLZ-shaped opcode intrinsics without adding Verity-side Lean axioms.

This draft includes:

• Verity.Core.Intrinsics descriptor types
• verity_intrinsic command syntax/elaboration for the focused CLZ case
• Expr.intrinsic and Yul lowering to verbatim_1i_1o(hex"1e", arg)
• linker allowance for verbatim_* calls
• smoke coverage via Contracts.Smoke.IntrinsicClzSmoke
• docs describing the prototype trust posture

Verification

• lake build Contracts.Smoke
• downstream Tamago source check: lake build Tamago.Utils.FixedPointMathLib against this branch
• downstream manual codegen confirmed verbatim_1i_1o(hex"1e", x) in generated Yul

Known gaps before ready for review

• Parser is prototype semicolon syntax, not the intended multiline syntax.
• Only CLZ-shaped one-arg lowering is implemented; declarations are not fully data-driven yet.
• min_fork hard-error enforcement is not implemented yet.
• Intrinsic entries are not yet integrated into --trust-report.
• Consumer semantics are represented as an obligation marker, not a verified EVMYulLean bridge.

Downstream benchmark note

Using the Tamago th0rgal/showcase-root-gas-benchmark branch with a local Verity path override and manually patched generated deployer bytecode from direct Verity Yul + solc output:

Operation	Baseline net	CLZ intrinsic net	Delta
sqrt	1292	1209	-83
cbrt	1411	1334	-77

tama build --contract FixedPointMathLib --no-forge is still blocked by downstream proof updates in Tamago.Proof.Utils.FixedPointMathLibProof.

---

Note

Medium Risk
New trust boundaries and compiler emission paths for arbitrary opcodes, mitigated by fail-closed fork enforcement and exclusion from the proven end-to-end fragment until opcode semantics exist; machine-readable trust-report integration is still outstanding.

Overview
Introduces consumer-owned intrinsics: verity_intrinsic declarations, Verity.Core.Intrinsics descriptors (HardFork, YulLowering, obligations), and Expr.intrinsic in the compilation model with lowering to verbatim_Ni_Mo(hex"...", args) or named Yul builtins. Contract syntax adds intrinsic / intrinsic_{cancun,prague,fusaka,osaka}; the macro registers declarations and translates call sites into IR.

Compiler/runtime behavior: expression compile validates arity and single output; Yul AST/pretty-print emit opcode hex via YulExpr.verbatimHex; the linker treats verbatim_* like builtins. YulEmitOptions.targetFork (default Cancun) plus --target-fork / tama.toml [yul] evm_version drive a fail-closed min_fork gate at compile time, with --allow-future-fork-intrinsics as an explicit override. Compile-driver tests cover rejection and acceptance paths.

Proofs & safety posture: new IntrinsicProofs covers fork ordering, scope accounting, lowering shape, and arity errors; SupportedSpec and source semantics treat intrinsics as unsupported so the end-to-end proven fragment does not silently widen. Audit/trust docs (INTRINSICS.md, AXIOMS.md, AUDIT.md, TRUST_ASSUMPTIONS.md) document consumer obligations at zero Verity axioms; trust_report.intrinsics remains follow-up. Smoke adds IntrinsicClzSmoke (EIP-7939 CLZ example) and a generated Foundry property stub.

^{Reviewed by Cursor Bugbot for commit fd2ef9a. 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 26, 2026 4:23pm

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

[cursor]

Redundant inputArity/outputArity shadow their useful ? variants

Low Severity

YulLowering.inputArity and outputArity return none for .builtin lowerings, while the nearly identically named inputArity? and outputArity? actually resolve builtin arity via yulBuiltinArity?. The non-? variants appear unused and risk silent none results if a future caller picks the wrong one for a builtin-backed intrinsic. Having two pairs of functions with Option Nat return types and confusingly similar names invites mistakes.

Additional Locations (1)

• Verity/Core/Intrinsics.lean#L133-L140

 

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

[cursor]

TOML parser strips comments before handling quoted values

Low Severity

parseTomlStringValue? splits on # before extracting quoted content, so a TOML value like evm_version = "value#tag" would be incorrectly truncated at the #. While unlikely for evm_version values today, this is a latent parsing bug that violates TOML spec and could cause silent mis-parsing if fork names or conventions ever include special characters.

 

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