Skip to main content

Module verifier

Module verifier 

Source
Expand description

Host-walk bounds verifier for the binary handshake buffer.

Modelled on the FlatBuffers verifier / rkyv bytecheck discipline: before the host dereferences any in-buffer offset it first proves the offset (and the length / payload it introduces) lands inside the buffer — and, for the return-side single-region invariant, inside the one region the value is supposed to be self-contained in. A walk that would step outside the region returns a precise VerifyError rather than reading garbage or panicking.

This is a read-only structural pass: it never decodes payload semantics (no utf-8 validation, no integer interpretation). Its sole job is to certify that a subsequent crate::buffer::BufferReader walk over the same bytes can dereference every pointer it will follow without an out-of-bounds access. The reader already performs the same bounds checks inline (and returns its own BufferError); the verifier exists so a host can run one cheap up-front pass — and so the single-region invariant (every reachable offset is confined to [region_start, region_end)) can be asserted independently of the reader, which only checks against the whole-buffer end.

§Single-region invariant (the load-bearing wall)

The compiled-backend ABI lays the arena out as [const_data | in_buf | out_buf | scratch]. A #main return value is required to be self-contained inside one region: a value built in out_buf (const-pool literals, copied records) references only out_buf; a value returned by identity from a parameter references only in_buf. The verifier takes the region bounds explicitly and rejects any offset that escapes them, so a cross-region pointer (the one shape the return marshaller must keep behind a loud capability) is caught as VerifyError::OutOfRegion instead of being silently dereferenced.

§Multi-region walk (F0 cross-region safety net)

The S5 cross-region return shape (-> Dict { servers: List<Cfg> }) builds the object head in out_buf while the parameter-sourced field data still lives in in_buf — a single value graph that legitimately spans two regions. The single-region wall would (correctly, for S1–S6) reject it. MultiRegion + verify_value_at_multi / verify_record_multi are the multi-region-aware sibling pass: they walk over the whole arena in absolute coordinates, and at every pointer they (1) read the slot value as an arena-absolute offset (the convention F1 codegen will emit — see the plan’s “F0 design decision” note: a single global arena-relative pointer convention), (2) classify which region that absolute offset lands in, and (3) bounds-check the introduced span against that one region. A pointer that lands in no region, or whose span runs off the region it starts in, is a loud VerifyError — never a wild read. The object positive-bytes_written return path runs this pass before any decode, closing the red-line “cross-region pointer into an object slot is not verified” gap.

F0 does not release any capability. The multi-region pass is the safety net + the facilities that let F1 release the first cross-region shape behind a verified gate; the cross-region object/struct lowering stays capped until then.

Structs§

MultiRegion
A set of arena regions in absolute arena coordinates, the multi-region sibling of Region. Where a Region confines an entire value graph to one window, a MultiRegion lets the graph span regions: every followed pointer is an arena-absolute offset that must land fully inside one of these regions (contains_span picks the region whose window the span starts in and requires the whole span to fit it). A span that starts in no region, or starts in one region but runs past its end, is rejected — there is no “fell through to the next region” silent over-read.
Region
A half-open byte window [start, end) inside the arena that a value is required to be self-contained in. start <= end is enforced by Region::new; every offset the verifier follows must satisfy start <= off and the introduced span must end at or before end.

Enums§

RegionTag
The four arena regions a cross-region return value may reach, in the fixed ABI layout order [const_data | in_buf | out_buf | scratch]. Used only to label which region a multi-region span landed in for diagnostics; the verifier itself treats them uniformly.
VerifyError
Why a verifier walk rejected a buffer. Every variant names the field (and where useful the offending offset / span) so a host can surface a precise diagnostic. The verifier returns these instead of reading out of bounds or panicking.

Functions§

verify_record
Verify that every offset reachable from a record laid out by layout / fields — anchored at record_base — stays inside region for the byte slice bytes.
verify_record_multi
Multi-region sibling of verify_record: verify a record laid out at the arena-absolute offset record_base, where every pointer slot holds an arena-absolute offset and the graph may legitimately span the const / in / out / scratch regions described by multi.
verify_value_at
Verify a bare value reachable from a direct pointer offset, rather than from a record’s fixed-area slot. This is the entry point the in-place region-walk return ABI calls: the machine code reports the arena-absolute offset of a value’s root (e.g. a List<List<scalar>> header) and the host rebases it to a region-relative offset, then asks the verifier to certify the whole reachable graph stays inside region before any decode.
verify_value_at_multi
Multi-region sibling of verify_value_at: certify a bare value whose root pointer (and every pointer reachable from it) is an arena-absolute offset and whose graph may span regions. bytes is the whole arena slice; root is the arena-absolute offset of the value’s root header. Any escape (a span fitting no region, or running off the region it starts in) is a loud VerifyError — the decode must not run.