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§
- Multi
Region - A set of arena regions in absolute arena coordinates, the
multi-region sibling of
Region. Where aRegionconfines an entire value graph to one window, aMultiRegionlets the graph span regions: every followed pointer is an arena-absolute offset that must land fully inside one of these regions (contains_spanpicks 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 <= endis enforced byRegion::new; every offset the verifier follows must satisfystart <= offand the introduced span must end at or beforeend.
Enums§
- Region
Tag - 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. - Verify
Error - 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 atrecord_base— stays insideregionfor the byte slicebytes. - verify_
record_ multi - Multi-region sibling of
verify_record: verify a record laid out at the arena-absolute offsetrecord_base, where every pointer slot holds an arena-absolute offset and the graph may legitimately span theconst/in/out/scratchregions described bymulti. - 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 insideregionbefore 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.bytesis the whole arena slice;rootis 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 loudVerifyError— the decode must not run.