Module rt

graven

Module rt 

Source
Expand description

Support for code generated by the Graven compiler (and the hand-written code in graven-schemas that freezes its pattern). Items marked #[doc(hidden)] are called only by generated code; the rest (ListR, VListR, VStrList, ListW, StreamW) appear in generated signatures.

All unsafe of the generated pattern lives here and in TableRef::str_unchecked: [FromVerified::from_verified], VListR::new and VStrList::new. Generated code has no unsafe blocks of its own beyond calling these fixed-contract functions, each item carrying #[allow(unsafe_code)] and a // SAFETY: comment that cites the invariant below.

§Generated pattern (frozen by hand in graven-schemas)

  • The caller charges the header. [FromTable::verify] never charges its own header (2 + fixed_len). The public inherent method X::verify(&self, ctx) is the “as root” entry point: it charges 2 + fixed_len and calls FromTable::verify; X::verified / X::verified_with only call the inherent X::verify (they do not charge again). A table/union field charges 2 + fixed_len of the target and calls the child’s FromTable::verify (or the child’s inherent verify, which does both); ListR::verify charges the elements and calls FromTable::verify on each one. [string] / [bytes] go through [verify_strs] / [verify_bytes_list]. The totals are those of spec §7.3.
  • A single kind of view. Every table generates XVerified<'a> with explicit accessors (never Deref) and reader(); strings via str_unchecked, tables via YVerified, table lists via VListR, [string] via VStrList, unions via an enum with an Unknown(u16) that is not descended into.
  • Every table can be a root. X::SCHEMA_ID, read, verified, verified_with, from_bytes, XW::root, XW::to_bytes, XW::seal.

§Invariants for the code generator (codegen)

The *Verified views skip UTF-8 validation, relying on the verify() that already ran. That is only sound if the generated code maintains, for every type X:

  1. Same edge, same type. An XVerified is only created (via [FromVerified::from_verified]) over a table that the root’s verify() reached successfully along the same edge (same field of the same parent table, same list element) and with the same reader type X. Being “reachable” is not enough: the same bytes can be pointed to by two edges as tables of different types, and verify only validated the type of the edge it walked.
  2. str_unchecked mirrors str. Every str_unchecked(off) call in a view corresponds to a validating str(off) call, at the same offset, in that type’s verify. Likewise, every VStrList in a view corresponds to a [verify_strs] call over the same list (same offset) in that type’s verify; a VStrList is only sound for lists verified by verify_strs.
  3. Nothing beyond what verify walks. Views never follow edges that verify skips: union tags unknown to the reader, fields beyond the reader’s layout, reserved fields.
  4. VListR<T> with verify’s T. VListR::new is only called with the same T that verify used for that list.
  5. verify is #[inline]. The generated verify functions carry #[inline] (its absence once caused a performance regression in verified reads).
  6. Strings validated by str(). verify MUST validate every string by calling str() (which checks UTF-8), never by charging bytes(off).len() to the budget without validating; otherwise item 2 no longer holds.

Items 2 and 6 also hold for [string]: verify MUST call [verify_strs] (never [verify_bytes_list]) on every list that the view exposes as a VStrList.

The mutation test in graven-schemas/tests/verified.rs (verified_matches_checked_under_mutation) is the acceptance gate: for mutated messages that pass verify, every read through the verified view MUST equal the checked read.

Structs§

ListR
Typed list of tables; an absent list reads as empty.
ListW
Known-count typed list writer.
StreamW
Unknown-count typed list writer.
VListR
Typed list of verified views; an absent list reads as empty. Only obtainable from a verified view, so its elements are verified too.
VStrList
[string] inside a verified message: get skips UTF-8 validation. An absent list reads as empty; a 0 element pointer reads as "" (spec §5.6).