From 2b82867d2bb6a8d2d9f5a20eaeb15db899c47078 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 5 Aug 2026 12:45:48 +0000 Subject: [PATCH] ogar-loco: proof-carrying vocabularies, the 3-ref min_shape fix, and the permanent floor External review of #239 surfaced the panic edge: Program traversal indexed call.values[slot] with slot driven by v.body_refs(), so an unvalidated vocabulary claiming more than three references panicked. Conformance would have rejected that vocabulary, but nothing forced conformance to have run before traversal. - conformance::validate(v) -> CheckedVocabulary: the proof-carrying wrapper, constructible only through validation. references_are_resolvable and branches_of now require it, turning the test-time convention into a type. The wrapper delegates ALL Vocabulary methods (composed included -- conformance validated the composed answers, so re-deriving from the hooks could answer differently than what was validated). - Fixing the edge surfaced a second defect: the default min_shape mapped everything >=2 refs to Triples, wrongly rejecting a LEGAL three-reference domain function (three refs fit Quads exactly). Fixed in the trait default and in shared_core, pinned two-sided: the three-ref vocabulary conforms and defaults to Quads; the hostile 200-ref vocabulary is refused by validate even with a Quads override (no shape holds more than three value bytes). - DOMAIN_FLOOR declared PERMANENT stored-byte ABI: 0x00..=0x8F universal forever, 0x90..=0xFF vocabulary-local forever. Moving the floor would silently reinterpret persisted programs, so it is documented as permanent and pinned by a const assert whose message names why the 'fix' would be wrong. Gates: fmt, clippy -D warnings, tests (38 loco + 7 blockly), rustdoc -D warnings -- all green. --- crates/ogar-loco/src/lib.rs | 26 +++++- crates/ogar-loco/src/program.rs | 44 +++++++-- crates/ogar-loco/src/vocabulary.rs | 144 ++++++++++++++++++++++++++++- docs/BLOCK-EDITOR-PLAN.md | 24 +++++ 4 files changed, 223 insertions(+), 15 deletions(-) diff --git a/crates/ogar-loco/src/lib.rs b/crates/ogar-loco/src/lib.rs index f5f61da..b165f9e 100644 --- a/crates/ogar-loco/src/lib.rs +++ b/crates/ogar-loco/src/lib.rs @@ -128,6 +128,7 @@ pub use node::FunctionNode; pub use pool::{Constant, ConstantPool, PoolError}; pub use program::{Program, branches_of}; pub use vocabulary::Vocabulary; +pub use vocabulary::conformance::CheckedVocabulary; // ── The function-body budget ──────────────────────────────────────────────── @@ -241,13 +242,32 @@ const _: () = assert!(LaneShape::Quads.calls_per_function() == 90); /// one-compare test for "this op is vocabulary-specific", which a renderer, /// validator, or compiler can branch on without a table lookup. /// +/// # This boundary is PERMANENT, not today's allocation +/// +/// `0x00..=0x8F` is the universal ABI **forever**; `0x90..=0xFF` is +/// vocabulary-local **forever**. Stored programs encode the boundary +/// implicitly in every function byte they carry: moving the floor would +/// silently reinterpret persisted bytes — a shared-core opcode becoming +/// vocabulary-local (or the reverse) under a reader that never changed the +/// data. That is the same layout-reclaim hazard the substrate's +/// reserve-don't-reclaim rule exists to forbid. Unallocated shared-core +/// slots (`0x0F..0x1F` gaps, `0x86..0x8F`, …) stay reserved for the CORE to +/// mint; unallocated domain slots stay reserved for each vocabulary. Neither +/// side ever annexes the other's range. +/// /// In the first vocabulary (`ogar-blockly`) the domain range hosts the /// Scratch-style *device families* (motion, looks, sound, …) and the constant -/// is re-exported there under its historical name `DEVICE_FAMILY_FLOOR`. The -/// range above the floor is **reserved, not allocated** — entries mint when a -/// vocabulary needs them. Reserve, don't reclaim. +/// is re-exported there under its historical name `DEVICE_FAMILY_FLOOR`. pub const DOMAIN_FLOOR: u8 = 0x90; +// The permanence pin: changing the floor MUST fail compilation here, and the +// failure message must say why the "fix" is wrong. +const _: () = assert!( + DOMAIN_FLOOR == 0x90, + "DOMAIN_FLOOR is stored-byte ABI: moving it reinterprets every persisted \ + program; mint inside the existing ranges instead" +); + /// An index into the **function codebook** — one byte that names any callable /// thing in scope. /// diff --git a/crates/ogar-loco/src/program.rs b/crates/ogar-loco/src/program.rs index 7212641..63f21f3 100644 --- a/crates/ogar-loco/src/program.rs +++ b/crates/ogar-loco/src/program.rs @@ -41,7 +41,8 @@ //! the substrate's, per vocabulary. A `Program` carries bodies and the caller //! supplies keys — the same boundary [`crate::node`] draws. -use crate::{Call, FunctionBody, Vocabulary}; +use crate::vocabulary::conformance::CheckedVocabulary; +use crate::{Call, FunctionBody, MAX_VALUES_PER_CALL, Vocabulary}; /// One script's functions. Index `0` is the entry. #[derive(Debug, Clone, PartialEq, Eq)] @@ -81,12 +82,25 @@ impl Program { /// The vocabulary is a parameter because *which value bytes are /// references* is a per-function fact ([`Vocabulary::body_refs`]) — the /// same bytes under a different vocabulary could be plain immediates. + /// It must arrive as a [`CheckedVocabulary`] because this walk indexes a + /// call's fixed three value bytes by `body_refs`: an unvalidated + /// vocabulary claiming more references than a call can carry would drive + /// that indexing out of bounds. Validation bounds it (`body_refs ≤ 3` + /// everywhere), so holding the wrapper IS the proof — see + /// [`crate::vocabulary::conformance::validate`]. #[must_use] - pub fn references_are_resolvable(&self, v: &V) -> bool { + pub fn references_are_resolvable(&self, v: &CheckedVocabulary) -> bool { for body in &self.functions { for call in body.calls() { - let n = v.body_refs(call.function); - for slot in 0..usize::from(n) { + let n = usize::from(v.body_refs(call.function)); + // Guaranteed by validation; asserted so a hypothetical + // non-deterministic vocabulary fails loudly in debug builds + // instead of panicking on the index below. + debug_assert!( + n <= MAX_VALUES_PER_CALL, + "validated body_refs exceeds a call" + ); + for slot in 0..n { let idx = usize::from(call.values[slot]); if idx == 0 || idx >= self.functions.len() { return false; @@ -103,12 +117,22 @@ impl Program { /// /// Useful to a consumer walking a program: it says *which* bytes are function /// indices without re-deriving [`Vocabulary::body_refs`] call by call. +/// Requires a [`CheckedVocabulary`] for the same reason as +/// [`Program::references_are_resolvable`]: the slice below is bounded by the +/// validated `body_refs ≤ 3` guarantee. #[must_use] -pub fn branches_of(v: &V, body: &FunctionBody) -> Vec<(usize, Call, Vec)> { +pub fn branches_of( + v: &CheckedVocabulary, + body: &FunctionBody, +) -> Vec<(usize, Call, Vec)> { body.calls() .enumerate() .filter_map(|(i, c)| { let n = usize::from(v.body_refs(c.function)); + debug_assert!( + n <= MAX_VALUES_PER_CALL, + "validated body_refs exceeds a call" + ); (n > 0).then(|| (i, c, c.values[..n].to_vec())) }) .collect() @@ -160,7 +184,7 @@ mod tests { #[test] fn every_reference_resolves_and_none_points_at_the_entry() { - let v = EmptyVocab; + let v = crate::vocabulary::conformance::validate(EmptyVocab).unwrap(); let prog = repeat_ten(); assert!(prog.references_are_resolvable(&v)); assert_eq!(prog.len(), 2); @@ -217,14 +241,16 @@ mod tests { ], }; // Under the empty vocabulary 0x90's value byte is a plain immediate. - assert!(prog.references_are_resolvable(&EmptyVocab)); + let empty = crate::vocabulary::conformance::validate(EmptyVocab).unwrap(); + assert!(prog.references_are_resolvable(&empty)); // Under a vocabulary where 0x90 branches, 7 is a dangling reference. - assert!(!prog.references_are_resolvable(&BranchyDomain)); + let branchy = crate::vocabulary::conformance::validate(BranchyDomain).unwrap(); + assert!(!prog.references_are_resolvable(&branchy)); } #[test] fn branches_of_reports_which_bytes_are_function_indices() { - let v = EmptyVocab; + let v = crate::vocabulary::conformance::validate(EmptyVocab).unwrap(); let prog = repeat_ten(); let b = branches_of(&v, prog.entry()); assert_eq!(b.len(), 1, "one branching call in the entry"); diff --git a/crates/ogar-loco/src/vocabulary.rs b/crates/ogar-loco/src/vocabulary.rs index b8d36ed..8df52d5 100644 --- a/crates/ogar-loco/src/vocabulary.rs +++ b/crates/ogar-loco/src/vocabulary.rs @@ -158,12 +158,15 @@ pub mod shared_core { /// `Pairs` — a one-byte immediate would truncate the else arm into /// nothing, and the program would run its then-branch and silently skip /// the else. A cast refuses rather than narrowing; this is what it - /// consults. + /// consults. (No shared-core function carries three references today; + /// the `Quads` arm exists so the mapping is total by construction + /// rather than by the current table's accident.) #[must_use] pub fn min_shape(f: FnIndex) -> LaneShape { match body_refs(f) { 0 | 1 => LaneShape::Pairs, - _ => LaneShape::Triples, + 2 => LaneShape::Triples, + _ => LaneShape::Quads, } } } @@ -213,10 +216,18 @@ pub trait Vocabulary { } /// The narrowest shape that can hold `f`'s body references. + /// + /// Three references are LEGAL (they fit `Quads` exactly), so the default + /// maps them there rather than to `Triples` — an earlier draft's + /// `_ => Triples` would have made [`conformance::check`] wrongly reject a + /// conforming three-reference domain function. Four or more references + /// fit no shape; the default still answers `Quads` and the conformance + /// shape check is what refuses them. fn min_shape(&self, f: FnIndex) -> LaneShape { match self.body_refs(f) { 0 | 1 => LaneShape::Pairs, - _ => LaneShape::Triples, + 2 => LaneShape::Triples, + _ => LaneShape::Quads, } } } @@ -262,6 +273,78 @@ pub mod conformance { impl core::error::Error for ConformanceError {} + /// A vocabulary that has PASSED [`check`] — the proof-carrying form. + /// + /// Program traversal ([`Program::references_are_resolvable`], + /// [`branches_of`]) requires this wrapper rather than a bare + /// [`Vocabulary`], because those walks index a call's fixed three value + /// bytes by `body_refs` — under an unvalidated vocabulary claiming more + /// than three references that indexing would panic. The wrapper turns + /// "every consumer remembers to run the conformance test" into a type: + /// it cannot be constructed except through [`validate`], so holding one + /// IS the proof that `body_refs ≤ 3` everywhere (the shape check bounds + /// it: no [`LaneShape`](crate::LaneShape) holds more than three value + /// bytes). + /// + /// It implements [`Vocabulary`] by delegation, so it composes anywhere a + /// vocabulary is accepted. + /// + /// [`Program::references_are_resolvable`]: crate::Program::references_are_resolvable + /// [`branches_of`]: crate::branches_of + #[derive(Debug, Clone, Copy, PartialEq, Eq)] + pub struct CheckedVocabulary(V); + + impl CheckedVocabulary { + /// Borrow the validated vocabulary. + pub fn inner(&self) -> &V { + &self.0 + } + + /// Unwrap, discarding the proof. + pub fn into_inner(self) -> V { + self.0 + } + } + + impl Vocabulary for CheckedVocabulary { + fn domain_stack_arity(&self, f: FnIndex) -> Option { + self.0.domain_stack_arity(f) + } + fn domain_body_refs(&self, f: FnIndex) -> u8 { + self.0.domain_body_refs(f) + } + // The composed methods delegate too — conformance validated the + // COMPOSED answers, so the wrapper must forward them rather than + // re-derive from the hooks (a vocabulary with overridden composed + // methods would otherwise answer differently through the wrapper + // than it was validated as). + fn stack_arity(&self, f: FnIndex) -> Option { + self.0.stack_arity(f) + } + fn body_refs(&self, f: FnIndex) -> u8 { + self.0.body_refs(f) + } + fn branches(&self, f: FnIndex) -> bool { + self.0.branches(f) + } + fn min_shape(&self, f: FnIndex) -> crate::LaneShape { + self.0.min_shape(f) + } + } + + /// Validate a vocabulary and, on success, return the proof-carrying + /// wrapper program traversal requires. + /// + /// # Errors + /// + /// The first [`ConformanceError`] found, naming the byte and the defect + /// — same gate as [`check`], which remains available for test-time + /// assertion without taking ownership. + pub fn validate(v: V) -> Result, ConformanceError> { + check(&v)?; + Ok(CheckedVocabulary(v)) + } + /// Check a vocabulary against the sharing discipline, over the full /// 256-byte codebook. /// @@ -473,6 +556,61 @@ mod tests { ); } + #[test] + fn three_body_references_are_legal_and_default_to_quads() { + // The default min_shape must map 3 refs to Quads (they fit exactly). + // An earlier draft mapped everything >=2 to Triples, which would have + // wrongly rejected this conforming vocabulary — surfaced while + // hardening the >3 panic edge, pinned here so it cannot regress. + struct TripleRefVocab; + impl Vocabulary for TripleRefVocab { + fn domain_stack_arity(&self, f: FnIndex) -> Option { + (f.0 == 0x90).then_some(0) + } + fn domain_body_refs(&self, f: FnIndex) -> u8 { + if f.0 == 0x90 { 3 } else { 0 } + } + } + assert_eq!( + TripleRefVocab.min_shape(FnIndex(0x90)), + LaneShape::Quads, + "three refs fit Quads exactly" + ); + assert_eq!(check(&TripleRefVocab), Ok(())); + } + + #[test] + fn validate_refuses_a_vocabulary_whose_refs_exceed_a_calls_capacity() { + // The panic edge the proof-carrying wrapper closes: body_refs beyond + // MAX_VALUES_PER_CALL would drive `call.values[slot]` out of bounds + // in program traversal. No LaneShape holds more than three value + // bytes, so even a min_shape override answering Quads cannot make + // 200 references conform — validate must refuse, and traversal is + // unreachable without the wrapper it refused to construct. + struct HostileVocab; + impl Vocabulary for HostileVocab { + fn domain_stack_arity(&self, _f: FnIndex) -> Option { + Some(0) + } + fn domain_body_refs(&self, f: FnIndex) -> u8 { + if f.0 == 0x90 { 200 } else { 0 } + } + fn min_shape(&self, _f: FnIndex) -> LaneShape { + LaneShape::Quads + } + } + assert_eq!( + conformance::validate(HostileVocab).err(), + Some(ConformanceError::ShapeTooNarrowForRefs { f: FnIndex(0x90) }) + ); + // Silence twin: validate hands back the proof for conforming + // vocabularies, and the wrapper answers exactly as the inner one. + let checked = conformance::validate(EmptyVocab).expect("EmptyVocab conforms"); + assert_eq!(checked.stack_arity(FnIndex::ADD), Some(2)); + assert_eq!(checked.body_refs(FnIndex::IF_ELSE), 2); + assert_eq!(checked.inner().body_refs(FnIndex::IF_ELSE), 2); + } + #[test] fn conformance_fires_on_a_shape_too_narrow_for_the_refs() { // IF_ELSE under a Pairs-only min_shape would truncate its else arm. diff --git a/docs/BLOCK-EDITOR-PLAN.md b/docs/BLOCK-EDITOR-PLAN.md index ad4fefe..8c3fb46 100644 --- a/docs/BLOCK-EDITOR-PLAN.md +++ b/docs/BLOCK-EDITOR-PLAN.md @@ -555,3 +555,27 @@ Gates: fmt / clippy `-D warnings` / tests (36 loco + 7 blockly) / rustdoc direction call. 5. All mints stay operator-gated: M1–M3 above, plus the template/flow concept domains. + +### W6 hardening — proof-carrying vocabularies + the permanent floor (post-#239 review) + +External review of #239 (operator's design-discussion loop) surfaced a real +panic edge, and fixing it surfaced a second defect the review had not seen: + +1. **The `>3 body_refs` panic edge — closed by type.** Program traversal + indexed `call.values[slot]` with `slot` driven by `v.body_refs()`; an + unvalidated vocabulary claiming more than three references panicked. + `conformance::validate(v) → CheckedVocabulary` is now the only way to + construct the wrapper `Program::references_are_resolvable` and + `branches_of` accept — holding it IS the proof `body_refs ≤ 3` everywhere + (the shape check bounds it; no `LaneShape` holds more than three value + bytes). "Socially and mechanically enforced" became type-enforced. +2. **The default `min_shape` wrongly rejected THREE references.** The trait + default mapped everything ≥2 to `Triples`, so a legal three-reference + domain function (fits `Quads` exactly) failed conformance unless the + vocabulary overrode `min_shape`. Fixed (`2 → Triples`, `3+ → Quads`) and + pinned two-sided: `three_body_references_are_legal_and_default_to_quads` + plus the hostile 200-ref vocabulary that `validate` must refuse. +3. **`DOMAIN_FLOOR` is declared PERMANENT stored-byte ABI.** `0x00..=0x8F` + universal forever, `0x90..=0xFF` vocabulary-local forever — moving the + floor would reinterpret persisted programs. Documented on the constant + and pinned by a `const` assert whose message says why the "fix" is wrong.