Cairn · module

Cairn.Abi

lean/Cairn/Abi.lean

The runtime's Boundary, filled in: v1 event decoding, Frame.ofLaid, v1 frame encoding. An app's ABI file passes Cairn.Frame.boundary to Runtime.stepBytes and Runtime.frameBytes (docs/runtime.md).

Imports Cairn.Frame.Build, Cairn.Frame.Events, Cairn.Runtime.Abi, Cairn.Text.Host

Order

Definitions 1

def

Cairn.Frame.boundary

lean/Cairn/Abi.lean:19

boundary : Runtime.Boundary

A batch that does not decode is dropped whole: the host's encoder is checked against Lean's decoder by the corpus test, so a bad batch means a host bug, and running half of it would be worse than running none.

Theorems 1

theorem

Cairn.satU32_eq_host_sat

provedlean/Cairn/Abi.lean:26

satU32_eq_host_sat (n : Nat) : Wire.satU32 n = (Text.Host.sat n).toNat

The frame encoder clamps font fields exactly as the text host does, so the font painted is the font measured.