Intermediate Representation

The Covenant compiler uses a Static Single Assignment (SSA) IR between the typechecker and the backend. The IR is the stable interface for compiler plugins, alternative backends, and tooling.

Why SSA?

In SSA form, every variable is assigned exactly once. This simplifies optimizations: dead code elimination becomes “remove definitions with no uses”; common subexpression elimination becomes “find identical definitions and merge them”.

Covenant’s IR extends SSA with:

Privacy domain tags (P, E, A) on every value
Covenant-specific opcodes for FHE, ZK, PQ, and amnesia operations
Effect annotations (reads/writes storage slots, emits events, calls external)

IR Grammar

Program    := Function*
Function   := "fn" Name "(" Param* ")" "->" Type "{" Block "}"
Block      := Instr* Terminator
Instr      := "%" Var "=" Opcode Arg* (":" Type)? ("@" Domain)?
Terminator := "ret" Arg | "br" Label | "br_if" Arg Label Label | "revert" Arg?
Arg        := "%" Var | Const
Const      := IntLit | "true" | "false" | "null" | "0x" HexLit
Domain     := "P" | "E" | "A"

Standard Opcodes

Arithmetic and Logic

Opcode	Description
`Add`	Integer addition
`Sub`	Integer subtraction
`Mul`	Integer multiplication
`Div`	Integer division (reverts on zero)
`Mod`	Modulo
`And`	Bitwise AND
`Or`	Bitwise OR
`Xor`	Bitwise XOR
`Shl`	Shift left
`Shr`	Shift right
`Not`	Bitwise NOT
`Eq`	Equality comparison
`Lt`, `Gt`, `Le`, `Ge`	Ordered comparisons

Memory and Storage

Opcode	Description
`Load`	Read a storage slot
`Store`	Write a storage slot
`MapLoad`	Read a mapping entry
`MapStore`	Write a mapping entry
`Alloc`	Allocate memory (transient)
`MemLoad`	Read from memory
`MemStore`	Write to memory

Control Flow

Opcode	Description
`Phi`	SSA phi node (merge values at join point)
`Select`	Conditional select (ternary)
`Call`	Internal function call
`ExternalCall`	Call to another contract
`StaticCall`	Read-only external call
`Revert`	Revert with error data
`Return`	Return from function

Events and Errors

Opcode	Description
`Emit`	Emit an event
`RevertWith`	Revert with typed error
`Require`	Assert or revert

Covenant-Specific Opcodes

FHE Opcodes (ERC-8227)

Opcode	Signature	Description
`FheEncrypt`	`(uint256, bytes32) -> bytes128`	Encrypt plaintext with public key
`FheDecrypt`	`(bytes128, address[]) -> uint256`	Threshold decrypt
`FheAdd`	`(bytes128, bytes128) -> bytes128`	Homomorphic addition
`FheSub`	`(bytes128, bytes128) -> bytes128`	Homomorphic subtraction
`FheMul`	`(bytes128, bytes128) -> bytes128`	Homomorphic multiplication
`FheCmp`	`(bytes128, bytes128) -> bytes128`	Encrypted comparison
`FheReencrypt`	`(bytes128, bytes32, bytes32) -> bytes128`	Re-encrypt to different key
`FheVerifyCt`	`(bytes128, bytes32) -> bool`	Verify ciphertext is well-formed

All FHE opcodes are tagged @E in the IR. A FheDecrypt result is tagged @P only after an authorization check is verified by the privacy flow analyzer.

ZK Opcodes (ERC-8229)

Opcode	Signature	Description
`ZkVerify`	`(bytes, bytes32[]) -> bool`	Verify a ZK proof against public signals
`ZkProve`	`(bytes32, bytes[]) -> bytes`	Generate a proof (off-chain WASM, returns handle)
`NovaFold`	`(bytes32, bytes) -> bytes`	Accumulate one Nova IVC step
`NovaCompress`	`(bytes) -> bytes`	Compress Nova accumulator to Halo2
`SelectiveDisclose`	`(bytes128, address) -> bytes`	Generate selective disclosure proof

PQ Opcodes (ERC-8231)

Opcode	Signature	Description
`PqVerify`	`(bytes2600, bytes, bytes4627) -> bool`	Verify Dilithium-5 signature
`PqSign`	`(bytes4864, bytes) -> bytes4627`	Sign with Dilithium-5 key (off-chain)
`KyberEncap`	`(bytes1568) -> (bytes1568, bytes32)`	Kyber key encapsulation
`KyberDecap`	`(bytes1568, bytes1568) -> bytes32`	Kyber decapsulation

Amnesia Opcodes (ERC-8228)

Opcode	Signature	Description
`AmnesiaDestroy`	`(bytes32[]) -> ()`	Zero storage slots and generate erasure proof
`AmnesiaPhaseCheck`	`(bytes32) -> uint8`	Read current ceremony phase
`AmnesiaPhaseTransition`	`(bytes32, uint8) -> ()`	Advance ceremony phase (reverts if invalid)
`ShamirVerify`	`(bytes32, bytes32, bytes) -> bool`	Verify a Shamir share commitment
`VdfGenerate`	`(bytes32, uint64) -> bytes`	Generate Wesolowski VDF output (off-chain)
`VdfVerify`	`(bytes32, uint64, bytes) -> bool`	Verify VDF proof

IR Dump

Use covenant inspect ir to dump the IR for any contract:

covenant inspect ir ./src/Token.cvt

Example output for a simple transfer action:

fn transfer(%to: address @P, %amount: uint256 @P) -> () {
entry:
  %caller_bal = MapLoad storage[0] %caller @P
  %to_bal     = MapLoad storage[0] %to     @P
  %ok         = Ge %caller_bal %amount @P
  br_if %ok body revert_block

body:
  %new_caller = Sub %caller_bal %amount @P
  %new_to     = Add %to_bal     %amount @P
  MapStore storage[0] %caller %new_caller
  MapStore storage[0] %to     %new_to
  Emit Transfer(%caller, %to, %amount)
  ret

revert_block:
  RevertWith InsufficientBalance()
}

Optimizer Passes

The 22 optimizer passes operate on this IR. The most impactful:

Constant Folding: Evaluates constant expressions at compile time.

; Before:          ; After:
%a = Add 5 3      %a = 8

FHE Batching: Groups consecutive FHE operations into a single precompile batch call, saving 10,000+ gas:

; Before:
%r1 = FheAdd %a %b
%r2 = FheAdd %r1 %c
%r3 = FheMul %r2 %d

; After (batched into one precompile call):
%r3 = FheBatch [FheAdd %a %b, FheAdd _, %c, FheMul _, %d]

Storage Slot Packing: Adjacent fields of type bool, uint8, uint16, uint32 are packed into a single 32-byte slot.