Skip to content

Host interface

The boundary between the specification and its execution environment. Sail owns all protocol semantics; the host owns only containers and raw byte storage, exposed to the specification as bodyless axioms — val declarations with stated contracts and no definitions. Proof targets treat the axioms as uninterpreted functions constrained by their contracts; the executable build binds them to an implementation.

Data crosses the boundary in two forms. Scalar values pass directly through axiom arguments and results. Bulk bytes never cross at all: they stay in host-owned regions — the stateless input buffer, frame memories, the output buffer, the scratch and absolute-memory arenas — and the specification manipulates them through nominal region slices naming an offset and length. The slice type itself identifies stateless input, memory, code, log data, output, or scratch; there is no runtime source tag. The accelerator interface (the eth-act zkvm-standards surface) is the third piece: cryptographic operations the execution environment proves natively, reached through the same axiom discipline.

Non-normative

These pages document the model's host interface — internal contracts of the executable specification, not protocol rules. The protocol semantics built on top of these axioms live in the state kernel and the normative sections.