Graven

zidl v1: tests and robustness (Plan 3 of 3)

Historical document. Written when the project was called zidl (later Graven). It is the plan that added the remaining conformance vectors, fuzzing, the generated evolution matrix and Miri. Names changed afterwards; the current description of the test suite is in Testing, and the normative text is the format specification.

For agentic workers: REQUIRED SUB-SKILL: Use superpowers:executing-plans (recommended: the user asked for lean execution) or superpowers:subagent-driven-development. Steps use checkbox (- [ ]) syntax for tracking.

Goal: Close part E of the hardening design with four deliverables:

The small pending items that are worth it also go in.

Architecture: Everything is tests or tooling around what already exists. The wire format, the public API and the generated code do not change, with two exceptions:

Fuzz and Miri live in scripts (scripts/fuzz.sh, scripts/miri.sh) and are not part of cargo test --workspace.

Tech Stack:

Spec: design/2026-11-12-zidl-v1-hardening-design.md (part E) and docs/spec/zidl-format-v1.md (§10.3 lists the rules without a vector). Records:

Global Constraints

Review Focus

  1. Verified × checked divergence. If verified() accepts a message, every accessor of the verified view returns exactly the same value as the checked accessor (read()). This holds also for required fields in a nested table, in a union variant and in a table list. → Task 2, the differential target over conformance::Root and edge::Edge.
  2. A new vector that the generated code reads differently from the interpreter. The gate in tests/generated.rs must iterate over all vectors, including those of new tables, not only those of Root. → Task 1, conformance_vectors_generated with an updated minimum count.
  3. Evolution through the envelope. v1, v2 and v3 have the same namespace and the same table name, so the SCHEMA_ID is equal: from_bytes of one version accepts an envelope of another, and the result follows the matrix. → Task 3, envelope_cross_versions.
  4. Input that crashes the compiler. A schema mutated from a valid one (a valid prefix, deep nesting) never makes parse/check/generate panic. → Task 2, the schema target.
  5. Miri too slow. This is solved by reducing cases (PROPTEST_CASES, sizes), never by skipping the tests that exercise unsafe (the Verified views, VListR, VStrList and str_unchecked). → Task 4.

Decisions in this plan (by the assistant)

Task 1: Vectors for the rules of §10.3

Files:

Interfaces:

New tables (append at the end of conformance.zidl):

struct Flags { on: bool, c: Color }
struct Empty {}

// Vectors of §10.3 that Root cannot reach without changing its meaning.
table Extra {
  flags  @0: Flags?;
  bools  @1: [bool]?;
  colors @2: [Color]?;
  names  @3: [string]?;
  blobs  @4: [bytes]?;
  pick   @5: Choice;        // required union
  leaves @6: [Leaf]?;
  e      @7: Empty?;        // zero-size slot
  @8: reserved u64;
  tail   @9: string?;       // a pointer after the reserved field
}

// Reads `[Leaf]` with an elem_fixed_len different from the reader's layout.
table Holder { items @0: [Leaf]; }

New vectors (name → message → expected result). Each error case has one defect over a valid base, like the existing ones:

vector message expect
bool_struct_and_lists flags = {on: 02, c: 1}, bools = [00, 01, 07], colors = [0, 2, 9], pick = Leaf value: on = true, bools = [false, true, true], colors = [Red, Blue, Unknown(9)]
strlist_null_elem names = ["a", <ptr 0>, "c"], blobs = [<ptr 0>] value: names = ["a", "", "c"], blobs = [[]]
union_tag_null_ptr_optional Root with choice tag 1 and pointer 0 value: choice absent
union_tag_null_ptr_required Extra with pick tag 1 and pointer 0 error Missing
union_unknown_tag_bad_ptr Root with choice tag 9 and a pointer beyond the buffer error: the variant that the interpreter and the generated code give today (spec §6.2: BadOffset or OutOfBounds); record the chosen one in the README
reserved_slot_partial Extra with fixed_len cutting slot @8 in half value: the fields before @8; tail absent
ptr_slot_partial Extra with fixed_len cutting the pointer slot of tail in half error Truncated
table_list_elem_wider Holder with a [Leaf] whose elem_fixed_len = layout + 8 extra bytes value: the Leafs read, extras ignored
table_list_elem_narrower Holder with elem_fixed_len covering only n value: Leaf with s and next absent
table_list_elem_zero Holder with elem_fixed_len = 0 and 2 elements value: 2 Leafs with n absent; if the field is required in the reader ⇒ Missing (use the result the interpreter and the generated code agree on and record it)
zero_size_slot_at_end Extra with e present and fixed_len ending exactly at the offset of e (o == fixed_len) value: e present (the bit decides, §4.2)
env_concat two Root envelopes concatenated value: the first one (bytes after the CRC are not an error, §8.6)
env_payload_len_short an envelope with payload_len one less, CRC recomputed over the new size whatever §8.4 gives (expected: a value or a truncated-message error; record it)
env_payload_len_long an envelope with payload_len larger than the buffer error Incomplete

Task 2: Fuzzing with cargo-fuzz

Files:

Interfaces:

Targets:

target input property
read bytes X::read of each root (bank::Transaction, game::Frame, iot::Telemetry, stream::Chunk, conformance::Root, Extra, edge::Edge) plus every accessor, descending into tables, lists and unions, never panics
verify bytes X::verified of the same roots never panics; if it accepts, it walks every accessor of the Verified view
envelope bytes decode and envelopes(..) never panic; the iterator stops at the first error; decode(encode(p)) returns p
differential bytes for conformance::Root, Extra and edge::Edge: if verified(b) is Ok, a snapshot function that reads every field through the verified view equals the same snapshot through the checked accessors of read(b) (which must give Ok)
schema an arbitrary String and mutations of a valid schema parse → check → lock_from_ir → generate never panic

Details of the schema target:

Task 3: The bank v1/v2/v3 evolution matrix

Files:

Interfaces:

The matrix. Each cell is checked through both paths, read + accessors and verified + accessors:

writer \ reader v1 v2 v3
v1 (every field, note = "n") equal from_shard = Some, fee = None same as v2
v2 (from_shard = Some(3), fee = Some(-5)) ok, note = None equal ok, to_shard not exposed
v2 (from_shard omitted) Missing { field: "from_shard" } ok, from_shard = None ok
v3 (to_shard omitted, since it is reserved) Missing { field: "to_shard" } Missing { field: "to_shard" } ok

Task 4: Miri

Files:

Task 5: Small pending items

Files: each item names its own file.

Task 6: Wrap-up