# Compiler Intrinsics

`verity_intrinsic` is the extension point for consumer-owned opcode or builtin
bindings. It lets a downstream project bind a small EVM primitive that Verity
does not yet model directly, while keeping the trust boundary visible in code,
docs, and build settings.

The motivating example is EIP-7939 `CLZ`. Tamago declares `clz` in its own
tree, compiles calls to `verbatim_1i_1o(hex"1e", x)`, and keeps the CLZ trust
assumption in Tamago instead of adding CLZ-specific semantics to Verity.

## When to use one

Use an intrinsic when all of the following are true:

- the operation is a single low-level EVM opcode or Yul builtin;
- Verity does not yet have first-class semantics for it;
- the consumer can state the Lean semantics clearly;
- the deployment fork where the primitive exists is known;
- the consumer is willing to own and document the temporary trust assumption.

Do not use an intrinsic for multi-step libraries, contract calls, precompile
protocols, or operations whose semantics cannot be stated precisely.

## Declaring an intrinsic

```verity
def clzLowering : Verity.Core.Intrinsics.YulLowering :=
  .verbatim 1 1 "1e"

verity_intrinsic clz (x : Uint256) : Uint256 where
  pure
  yul := verbatim 1 1 (hex "1e")
  min_fork := osaka
  semantics := fun x =>
    Uint256.ofNat (if x.val = 0 then 256 else 255 - Nat.log2 x.val)
  obligation [clz_matches_eip7939 :=
    assumed "EIP-7939 CLZ opcode; chain must support Osaka+ execution semantics"]
```

Lean proofs can use the generated wrapper `clz x`. Verity contract bodies use
the explicit intrinsic form so the compiler sees the lowering descriptor:

```verity
let xClz :=
  intrinsic_osaka "clz" (Verity.Core.Intrinsics.YulLowering.verbatim 1 1 "1e") [x]
```

The three-argument contract form can infer `min_fork` only when the
`verity_intrinsic` declaration is in the same elaboration session. Cross-module
uses should use the explicit fork form:
`intrinsic_cancun`, `intrinsic_prague`, or `intrinsic_osaka`.
`intrinsic_fusaka` is accepted as a compatibility alias for the Ethereum
combined network-upgrade name.

The declaration has five responsibilities:

- `pure` states that the intrinsic has no storage, environment, or external-call
  effects.
- `yul := verbatim N M (hex "...")` states the compiler lowering. The generated
  Yul call is `verbatim_Ni_Mo(hex"...", args...)`.
- `min_fork := ...` records the minimum chain fork where the emitted opcode is
  valid. Verity enforces this fail-closed: builds targeting an older fork error
  unless the caller explicitly passes `--allow-future-fork-intrinsics`.
- `semantics := ...` is the Lean function used by source-level and consumer
  proofs.
- `obligation [...]` names the consumer-owned trust boundary. While the
  obligation is `assumed`, the consumer must document it in its own `AXIOMS.md`
  or equivalent trust-boundary file.

## Fork targeting

The pinned EVMYulLean fork used by Verity declares
`EvmYul.TargetSchedule := "Cancun"` and models Cancun-era opcodes such as
`BLOBHASH`, `BLOBBASEFEE`, `TLOAD`, `TSTORE`, `MCOPY`, and `PUSH0`. For that
reason, Verity's intrinsic fork enum starts at `cancun`.

Supported intrinsic fork labels are:

- `cancun`
- `prague`
- `osaka`
- `fusaka` as an accepted alias for Ethereum's combined Fulu/Osaka network-upgrade name

The compiler default is `--target-fork cancun`. Use `--target-fork prague` or
`--target-fork osaka` for newer deployments. Parity packs set the target from
their `evmVersion` when possible. If a build intentionally emits newer-fork
intrinsics while using an older target, it must pass
`--allow-future-fork-intrinsics`; otherwise compilation fails before Yul is
written.

## Trust model

Intrinsics deliberately keep Verity's project-level axiom count at zero. The
declaration records the consumer-owned obligation next to the generated Lean
semantic wrapper, but it does not create a Verity project axiom. Consumers must
document each assumed obligation in their own axiom or trust-boundary file.

For an assumed intrinsic, reviewers should check:

- the emitted opcode bytes or builtin name match the intended EVM primitive;
- the `semantics` function matches the EIP or target-chain behavior, including
  edge cases such as `clz(0)`;
- the `min_fork` is correct for the deployment target;
- the obligation text names the EIP, fork assumption, and any temporary nature
  of the trust boundary.

This is a consumer trust boundary, not a Verity proof-system axiom. Verity's
own `AXIOMS.md` remains the registry of project-level axioms and should stay at
zero unless Verity itself introduces an axiom.

## What Verity proves

Verity implements the generic intrinsic path needed by consumers such as
Tamago. The production compiler path is opcode-agnostic: consumers declare the
opcode or builtin they want to bind, and Verity validates and lowers that
declaration without adding opcode-specific semantics to its own tree.

The Verity-owned proofs cover:

- fork-order facts and fail-closed `min_fork` checks;
- intrinsic argument scope accounting;
- generic verbatim and builtin lowering shape;
- fail-closed arity rejection;
- source-semantics exclusion for intrinsics until opcode semantics are modeled.

These proofs intentionally stop before opcode semantics. Until EVMYulLean
models CLZ, the statement "opcode `0x1e` computes the declared Lean semantics"
remains the consumer-owned obligation documented next to the
`verity_intrinsic` declaration.

## Audit surface

Consumer builds that use intrinsics should archive the normal compiler
artifacts, the selected `--target-fork`, and the `verity_intrinsic`
declarations they rely on. Until machine-readable intrinsic trust-report rows
exist, reviewers should grep the consumer tree for `verity_intrinsic` and audit
each declaration manually.

For CLZ, the intended lifecycle is:

1. Tamago declares `clz` as an assumed intrinsic and documents
   `clz_matches_eip7939`.
2. Verity emits `verbatim_1i_1o(hex"1e", x)` for Tamago builds targeting
   chains that support Osaka-or-later execution semantics.
3. EVMYulLean adds first-class CLZ semantics.
4. Tamago flips the obligation from assumed to proved, removing the consumer
   trust assumption without changing source call sites.