diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..6e3acff --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +compiler/tests/fixtures/model-receipt-golden.json text eol=lf diff --git a/CHANGELOG.md b/CHANGELOG.md index 302fe4d..230f6f9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,41 @@ tracked in `STATUS.md`, `README.md`, and ## Unreleased +- **Model boundary receipts, the verify arm and chain admission**: a new + artifact kind, `buildlang-model-boundary-receipt/v0`, documented in the new + `docs/MODEL-RECEIPT.md` (SCIENTIFIC-RECEIPT.md gains a pointer section). + Emission is harness-side (`harness/model_shim.py`'s `--receipt-dir` flag, + local-model repo), never buildc; this slice ships the buildc-side READ path + only. `receipt verify` gains a fourth schema arm (beside gpu, + scientific-runtime, and check) in the new `compiler/src/model_receipt.rs`: + offline seal recompute, digest well-formedness (`DIGEST_MALFORMED`), and + field-shape contracts (`FIELD_CONTRACT_VIOLATION` for a `daemon_digest.hex` + present alongside `UNAVAILABLE`, a `COMPLETED` outcome with a null `reply`, + or a `PROTOCOL_VIOLATION` with a present `prompt`) -- no new failure + classes, the shared taxonomy is reused whole. `receipt chain build`'s + member-schema gate widens from a single-schema equality to a two-schema + allowlist (scientific-runtime + model-boundary-receipt); chain verify needed + zero changes, since pinned seals and subprocess re-verification already + dispatch through the new arm. The scientific verifier's + `CAPABILITY_INADMISSIBLE` refusal of any `Model`-observing program is + untouched: a model receipt is a different artifact kind by construction, it + cannot masquerade as scientific evidence. A byte-identical GOLDEN FIXTURE + (`compiler/tests/fixtures/model-receipt-golden.json`, an echo-mode + `COMPLETED` receipt) is checked into both this repo and local-model's + `_wshim` worktree with the same pinned seal, proving the Rust + (`serde_json::to_vec`) and Python (`json.dumps(..., separators=(",", ":"))`) + canonicalizations agree byte-for-byte; the no-floats schema is what makes + that agreement stable across the two serializers. Tamper coverage: a + resealed field-shape violation, a seal mismatch, and a chain binding a + model receipt beside a scientific receipt that breaks + (`CHAIN_LINK_UNVERIFIED`) when only the model member is tampered, all + exercised both as `compiler/src/model_receipt.rs` unit tests and as + `compiler/tests/cli.rs` CLI-level tests against the real `buildc` binary. + The model receipt is **not** a corpus member (it has no invariant to + classify PASS/FAIL_EXPECTED against, and is emitted by a different program + entirely) and not a `--self-test` case (that table is + scientific-runtime-only): corpus 29/29 and self-test 10/10 stay unchanged, + re-run and recorded. Full suite: 1,698 passed, 0 failed; `cargo fmt` clean. - **Executed Monte Carlo intervals with a witnessed denominator**: `monte_carlo` gains a two-arm `DECLARED | EXECUTED` status. Under the new `--mc-executed` flag (opt-in; requires the full `--mc-*` declaration and forces `--columns` diff --git a/README.md b/README.md index 2fb1836..15c131f 100644 --- a/README.md +++ b/README.md @@ -257,7 +257,7 @@ output, and the receipt tooling are the verified core; SPIR-V, LLVM IR, WASM, Rust, x86-64, ARM64, GPU dispatch, and `#[linear]` types are labeled experimental and stay that way until their evidence says otherwise. The release-shaped baseline (2026-07-29, local `cargo test` from `compiler/`): -1683 tests passing, 0 failing (11 ignored), with `buildc receipt corpus` +1698 tests passing, 0 failing (11 ignored), with `buildc receipt corpus` 29/29 and `buildc corpus verify` 8/8. Ground-truth release evidence lives in [STATUS.md](STATUS.md); [CHANGELOG.md](CHANGELOG.md) tracks changes. diff --git a/STATUS.md b/STATUS.md index 101045d..dc0ed2f 100644 --- a/STATUS.md +++ b/STATUS.md @@ -56,10 +56,15 @@ Last audited: 2026-07-01 (wind-down point); broader status audit remains 2026-06 > models propose, oracles dispose. `docs/FIVE-MODES-TOUR.md` chains one > receipt per computation mode (deterministic, exact-probabilistic, seeded > stochastic, Monte Carlo, budgeted heuristic, plus the cross-backend bonus) -> into one ordered, tamper-evident bundle via `receipt chain`. Current -> baseline: 1683 tests passing, 0 failing, 11 ignored; the example corpus -> (`examples/scientific-corpus.json`) is 29/29; the verifier `--self-test` is -> 10/10. +> into one ordered, tamper-evident bundle via `receipt chain`. A model +> boundary receipt (`buildlang-model-boundary-receipt/v0`, +> `docs/MODEL-RECEIPT.md`) can now be a chain member beside a +> scientific-runtime receipt (`receipt chain build`'s two-schema allowlist); +> it is a harness-emitted, offline-verified provenance artifact, not scientific +> evidence, and is not a corpus or `--self-test` member. Current baseline: +> 1698 tests passing, 0 failing, 11 ignored; the example corpus +> (`examples/scientific-corpus.json`) is unchanged at 29/29; the verifier +> `--self-test` is unchanged at 10/10. ## Identity The Effects Language -- algebraic effects as a first-class feature. @@ -80,7 +85,7 @@ The Effects Language -- algebraic effects as a first-class feature. - **Macro expansion**: Builtin macros, pattern matching, hygiene. Unit tests present. - **Interprocedural Lifetime Analysis** (Phase 1): Lifetime parameters flow through `FnTy` (function types), enabling precise borrow tracking at call sites. Functions like `fn pick<'a, 'b>(x: &'a i32, y: &'b i32) -> &'a i32` correctly propagate only the `'a`-linked borrow. Return lifetime mismatches (returning `'b` where `'a` expected) are rejected with clear errors. 8 new unit tests, 3 integration test programs. - **Current CI-shaped cargo baseline (2026-07-02, invariant family complete)**: lib 940, bin 140, cli 309, lexer 52, parser 88 (0 failed; 3 lib + 8 doc-test ignored) via `cargo test` from `compiler/`; `cargo fmt --check` clean; corpus 8/8. The rise from the `939/81/301` wind-down baseline is Phases A/B/C/D1-D3 of the Telos master-plan mandate: the receipt export bridge, the capability-witnessed receipt fields, and the seven-member invariant family (conservation, bounded, energy-identity, relation, conserved-band, non-negative) with their paired kernels and multi-column capture. (Prior 2026-06-23 baseline was 1002 passed / 0 failed / 11 ignored under a different aggregation.) -- **Current CI-shaped cargo baseline (2026-07-29, five-modes wave complete)**: lib 1004 (1001 passed, 3 ignored), bin 179, cli 341, gpu 12, lexer 52, parser 98 -- 1683 passed, 0 failed, 11 ignored total, via `cargo test` from `compiler/`; `cargo fmt --check` clean; `buildc receipt corpus examples/scientific-corpus.json` 29/29; verifier `--self-test` 10/10; `buildc corpus verify` (the 8-program semantic corpus, a separate C-backend regression check) stays 8/8. The rise from the 2026-07-02 `940/140/309/52/88` baseline above is the five-modes wave (2026-07-28 to 2026-07-29): the `Random` capability with witnessed-seed receipts, Monte Carlo estimator receipts, budgeted-search receipts, the `Model` capability's propose/dispose refusal, cross-backend relation receipts through the Rust backend (the invariant family's eighth member), wall-clock metering (`runtime_state.wall_seconds`, the receipt's first EXECUTED budget fact), executed Monte Carlo intervals with a witnessed denominator (the `monte_carlo` block's EXECUTED status), split-frontier drop flags (memory pillar increment 5, opt-in), and unit-annotated numeric types (checker slice one, experimental). Detail: `docs/FIVE-MODES-TOUR.md`. +- **Current CI-shaped cargo baseline (2026-07-29, model boundary receipts verify arm)**: lib 1004 (1001 passed, 3 ignored), bin 189 (+10 model_receipt.rs tamper/seal/golden-fixture unit tests), cli 346 (+5 model-receipt CLI integration tests: golden fixture, seal mismatch, resealed field-shape violation, chain-allowlist refusal, propose/dispose chain with a tampered model member), gpu 12, lexer 52, parser 98 -- 1698 passed, 0 failed, 11 ignored total, via `cargo test` from `compiler/`; `cargo fmt --check` clean; `buildc receipt corpus examples/scientific-corpus.json` 29/29 (unchanged: the model receipt is a different artifact kind, not a corpus member); verifier `--self-test` 10/10 (unchanged: scientific-runtime-only table); `buildc corpus verify` (the 8-program semantic corpus, a separate C-backend regression check) stays 8/8. The rise from the 2026-07-02 `940/140/309/52/88` baseline above is the five-modes wave (2026-07-28 to 2026-07-29): the `Random` capability with witnessed-seed receipts, Monte Carlo estimator receipts, budgeted-search receipts, the `Model` capability's propose/dispose refusal, cross-backend relation receipts through the Rust backend (the invariant family's eighth member), wall-clock metering (`runtime_state.wall_seconds`, the receipt's first EXECUTED budget fact), executed Monte Carlo intervals with a witnessed denominator (the `monte_carlo` block's EXECUTED status), split-frontier drop flags (memory pillar increment 5, opt-in), and unit-annotated numeric types (checker slice one, experimental). Detail: `docs/FIVE-MODES-TOUR.md`. - **Linear types `#[linear]` (2026-07-01, experimental — best-effort LINT, not a proven-sound checker):** opt-in no-cloning. A `#[linear]` struct/enum value is tracked as a resource that should be moved/consumed at most once -- the shared foundation for quantum qubit no-cloning, on-chain no-double-spend, and fin-sec resource-handle safety. Now enforced by **two layers**: the conservative AST gate (sound-over-complete name tracking + containment rule) AND a new **MIR affine/borrow checker** (`codegen/analysis/linear.rs`, built on the reusable `codegen::analysis` dataflow substrate) that runs post-lowering and closes the classes the name tracker cannot follow -- move-out-of-shared-borrow (incl. laundered through aggregates/returns and higher-order fn-pointers), field-extract from an owned linear aggregate, generic deref-and-return, and struct/enum record-pattern-through-`&`. Verified by repeated empirical adversarial sweeps (`buildc check` on constructed clones, confirmed with `buildc run`). **Not yet fully sound (do NOT claim a soundness guarantee):** known residual = `&mut`-match payload move + un-enumerated advanced corners; a complete affine checker is a deliberate multi-brick effort (cf. Rust's borrow checker). Honest scope: `docs/LINEAR-TYPES.md`. Ordinary types are unaffected (copy-like reuse preserved). - **Multiple dispatch (2026-07-01, static):** Julia-style — multiple functions may share one name, and a call selects the method by the tuple of ALL argument types (not just the receiver), resolved statically via one shared resolver (`types/dispatch.rs`) used by both the checker and codegen. Specificity: exact > coercion/concrete > generic; ambiguity and no-match are ERRORS (never a silent pick). Generic and concrete defs of a name compose (concrete wins when it matches, else the generic monomorphizes). Backward-compatible: only overloaded (2+ def) names are mangled, so single-def names and `extern "C"` FFI are byte-identical (verified by a 22/22 differential C sweep). Deferred: operator overloading on both operands (still left-operand-only), and dynamic runtime-type dispatch (no runtime type descriptors yet). Details: `docs/MULTIPLE-DISPATCH.md`. - **Math syntax (2026-07-01, Pillar B):** four additive, backward-compatible features (each verified by a differential C sweep showing existing programs unchanged). (1) **Broadcasting operators `.+ .- .* ./`** over fixed-size `Array` (the type of an array literal `[..]`), including scalar broadcast in both directions; length agreement is a COMPILE-TIME check carried in the `Array` type (no runtime dimension check), and codegen desugars each operator into an unrolled array of per-element SCALAR MIR ops, so the broadcast ops never reach any backend. (2) **`linalg` stdlib module** (`stdlib/linalg.bld`): free functions `vec_add/sub/mul/div`, `vec_scale`, `vec_scalar_add`, `vec_dot`, `vec_sum`, `vec_norm` over the dynamic `Vec`, no compiler/runtime change. (3) **`**` power** wired to the pre-existing `BinOp::Pow` (right-associative, `-2 ** 2 == -4`; prefix `**x` stays double-deref, so no pointer code changes). (4) **Unicode operator aliases** `× · ∙ -> *`, `÷ -> /`, `− -> -`. Honest scope: this is elementwise broadcasting over FIXED-SIZE arrays plus a 1-D vector library over DYNAMIC `Vec` (two distinct surfaces: operators work on array literals, the library on `Vec`; a `Vec` cannot yet use `.+`), NOT Julia-parity linear algebra. Deferred: dynamic-`Vec` broadcasting operators, a true 2-D `Matrix{T}` with linear algebra (no N-D MIR type exists), `f32` element parity, and broadcast comparisons/`.^`. Details: `docs/MATH-SYNTAX.md`. @@ -179,4 +184,4 @@ package API completion. LSP readiness is tracked separately through the checked `buildlang-lsp-dispatch-receipt/v0` artifact and still excludes end-to-end VS Code extension verification. -BuildLang has a **working compiler core** (lexer -> parser -> type checker -> MIR -> C backend -> executable) with a current local baseline (2026-07-29) of 1683 tests passed, 0 failed (11 ignored) via `cargo test --quiet` from `compiler/` (per-target splits live in the dated baseline entries above). It can compile and run real programs with variables, functions, control flow, pattern matching, recursion, and algebraic effects. C, LLVM, x86-64, ARM64, WASM, SPIR-V, HLSL, GLSL, and Rust are accessible from the CLI via `buildc build --target `, but with different maturity levels. The C backend is production-verified and now has a semantic-corpus C execution receipt matching the current 8-program corpus; `buildc run` uses per-run temp build directories so concurrent C receipt probes avoid shared temp C/PDB collisions; `buildc corpus verify` validates the semantic corpus manifest, C/Rust receipts, and real C-backend stdout, accepts explicit corpus roots, and can refresh the C receipt for copied corpus fixtures after C stdout passes. The same corpus path now carries a `buildlang-substrate-receipt/v0` aggregation receipt that checks source-set size, backend maturity, memory gaps, representation fallback policy, and evidence commands without promoting experimental backends. Its representation surface is now backed by a checked `buildlang-mir-representation-receipt/v0` artifact that recomputes per-program MIR operation families, symbols, memory-surface flags, and control-flow summaries during `buildc corpus verify`. The same verification path now also checks a `buildlang-memory-layout-receipt/v0` artifact that binds the corpus memory surface to manifest tags, MIR-derived memory flags, ownership/layout classification, digest evidence, and explicit known gaps without claiming byte-level ABI layout or full borrow proof. `buildc receipt verify` re-checks saved source-bound check receipts against current source inputs, policy/profile digests, replayed effect/accountability surfaces, optional required built-in profile identity, and optional required policy digest, with optional JSON verification reports for CI; check policies now validate referenced effect names against built-in capabilities and the checked source graph so misspelled gates fail instead of silently weakening enforcement, can require `allowed_effects` to be authoritative even when empty, can require explicit direct/propagated provenance allowlists, can constrain direct capability boundaries to exact ambient helper/macro/FFI sources, can classify compile-time ambient macros such as `include_str!` and `env!` under `FileSystem`/`Environment`, can scan macro argument token trees with `SourceId` provenance so `println!(read_file(...))` requires both `Console` and `FileSystem` in entry sources and external module files and unknown extern calls/statics surface as `Foreign`, can classify known effectful `build_*` C runtime helper aliases declared in extern blocks under their real domain capability instead of generic `Foreign`, can preserve qualified ambient helper paths such as `io::read_file` in diagnostics, receipts, and scaffolded source allowlists, can reject effectful callbacks passed into pure `fn(...)` boundaries instead of erasing effect rows, and can preserve delayed or propagated capability evidence across callbacks, closures, aggregates, async awaits, branches, loops, casts, refs/derefs, pipes, assignments, selected aggregate fields, returned functions, and exact source allowlists. The built-in `strict-accountability` policy profile packages required effect inventory, digest, provenance, source, and coverage requirements into a named adoption gate for teams that want no ambient IO without exact allowlists, and `buildc policy scaffold` can turn observed receipt evidence into an exact strict policy skeleton for review while preserving pure receipts against later effect drift. `buildc doctor` reports local toolchain, stdlib, registry, optional backend tools, and backend maturity for adoption diagnostics; tested quickstart examples cover first-run CPU execution, mutable control flow, algebraic effects, and HLSL shader output; the Rust backend is subset-validated with `rustc --emit=metadata` and has a narrower generated-executable stdout smoke layer over the same semantic corpus plus manifest contract/receipt consistency/metadata guards; LLVM can optionally link with clang; native/WASM backends output assembly/binary for external toolchain linking. Formatter and package-manager entry points (`buildc fmt`, `buildc pkg`) are wired into the CLI, but the package manager has no live registry. `buildc lsp` starts the current stdio server loop, dispatches the checked raw LSP receipt sequence through structural JSON-RPC parsing, emits compiler-backed diagnostics, and returns receipt-verified semantic tokens v0 plus opened-document workspace symbols; full compiler-backed semantic token indexing, global workspace-symbol indexing, and end-to-end VS Code extension verification remain open. The self-hosted compiler and standard library (244,085 lines of `.bld` code) represent an ambitious long-term vision but cannot be compiled or executed today. +BuildLang has a **working compiler core** (lexer -> parser -> type checker -> MIR -> C backend -> executable) with a current local baseline (2026-07-29) of 1698 tests passed, 0 failed (11 ignored) via `cargo test --quiet` from `compiler/` (per-target splits live in the dated baseline entries above). It can compile and run real programs with variables, functions, control flow, pattern matching, recursion, and algebraic effects. C, LLVM, x86-64, ARM64, WASM, SPIR-V, HLSL, GLSL, and Rust are accessible from the CLI via `buildc build --target `, but with different maturity levels. The C backend is production-verified and now has a semantic-corpus C execution receipt matching the current 8-program corpus; `buildc run` uses per-run temp build directories so concurrent C receipt probes avoid shared temp C/PDB collisions; `buildc corpus verify` validates the semantic corpus manifest, C/Rust receipts, and real C-backend stdout, accepts explicit corpus roots, and can refresh the C receipt for copied corpus fixtures after C stdout passes. The same corpus path now carries a `buildlang-substrate-receipt/v0` aggregation receipt that checks source-set size, backend maturity, memory gaps, representation fallback policy, and evidence commands without promoting experimental backends. Its representation surface is now backed by a checked `buildlang-mir-representation-receipt/v0` artifact that recomputes per-program MIR operation families, symbols, memory-surface flags, and control-flow summaries during `buildc corpus verify`. The same verification path now also checks a `buildlang-memory-layout-receipt/v0` artifact that binds the corpus memory surface to manifest tags, MIR-derived memory flags, ownership/layout classification, digest evidence, and explicit known gaps without claiming byte-level ABI layout or full borrow proof. `buildc receipt verify` re-checks saved source-bound check receipts against current source inputs, policy/profile digests, replayed effect/accountability surfaces, optional required built-in profile identity, and optional required policy digest, with optional JSON verification reports for CI; check policies now validate referenced effect names against built-in capabilities and the checked source graph so misspelled gates fail instead of silently weakening enforcement, can require `allowed_effects` to be authoritative even when empty, can require explicit direct/propagated provenance allowlists, can constrain direct capability boundaries to exact ambient helper/macro/FFI sources, can classify compile-time ambient macros such as `include_str!` and `env!` under `FileSystem`/`Environment`, can scan macro argument token trees with `SourceId` provenance so `println!(read_file(...))` requires both `Console` and `FileSystem` in entry sources and external module files and unknown extern calls/statics surface as `Foreign`, can classify known effectful `build_*` C runtime helper aliases declared in extern blocks under their real domain capability instead of generic `Foreign`, can preserve qualified ambient helper paths such as `io::read_file` in diagnostics, receipts, and scaffolded source allowlists, can reject effectful callbacks passed into pure `fn(...)` boundaries instead of erasing effect rows, and can preserve delayed or propagated capability evidence across callbacks, closures, aggregates, async awaits, branches, loops, casts, refs/derefs, pipes, assignments, selected aggregate fields, returned functions, and exact source allowlists. The built-in `strict-accountability` policy profile packages required effect inventory, digest, provenance, source, and coverage requirements into a named adoption gate for teams that want no ambient IO without exact allowlists, and `buildc policy scaffold` can turn observed receipt evidence into an exact strict policy skeleton for review while preserving pure receipts against later effect drift. `buildc doctor` reports local toolchain, stdlib, registry, optional backend tools, and backend maturity for adoption diagnostics; tested quickstart examples cover first-run CPU execution, mutable control flow, algebraic effects, and HLSL shader output; the Rust backend is subset-validated with `rustc --emit=metadata` and has a narrower generated-executable stdout smoke layer over the same semantic corpus plus manifest contract/receipt consistency/metadata guards; LLVM can optionally link with clang; native/WASM backends output assembly/binary for external toolchain linking. Formatter and package-manager entry points (`buildc fmt`, `buildc pkg`) are wired into the CLI, but the package manager has no live registry. `buildc lsp` starts the current stdio server loop, dispatches the checked raw LSP receipt sequence through structural JSON-RPC parsing, emits compiler-backed diagnostics, and returns receipt-verified semantic tokens v0 plus opened-document workspace symbols; full compiler-backed semantic token indexing, global workspace-symbol indexing, and end-to-end VS Code extension verification remain open. The self-hosted compiler and standard library (244,085 lines of `.bld` code) represent an ambitious long-term vision but cannot be compiled or executed today. diff --git a/compiler/src/main.rs b/compiler/src/main.rs index a430afa..0ca31e8 100644 --- a/compiler/src/main.rs +++ b/compiler/src/main.rs @@ -17,6 +17,7 @@ mod gpu_receipt; mod lsp_dispatch; mod memory_layout; mod mir_representation; +mod model_receipt; mod module_graph; mod scientific_runtime; mod symbol_graph; @@ -42,6 +43,7 @@ use memory_layout::{verify_memory_layout_receipt, MemoryLayoutReceipt, MEMORY_LA use mir_representation::{ verify_mir_representation_receipt, MirRepresentationReceipt, MIR_REPRESENTATION_RECEIPT, }; +use model_receipt::{verify_model_boundary_receipt, MODEL_RECEIPT_SCHEMA}; use module_graph::{verify_module_graph_receipt, ModuleGraphReceipt, MODULE_GRAPH_RECEIPT}; use scientific_runtime::{ build_receipt_chain, receipt_chain_seal_hex, ReceiptChainManifest, ScientificCorpusManifest, @@ -1899,11 +1901,21 @@ fn cmd_receipt_chain_build(receipts: &[PathBuf], output: &Path) -> Result<(), i3 code })?; let schema = receipt.get("schema").and_then(|v| v.as_str()).unwrap_or(""); - if schema != SCIENTIFIC_RUNTIME_SCHEMA { + // Allowlist widened for model boundary receipts (design section 6): + // a model receipt can be a chain member beside scientific-runtime + // receipts, demonstrating propose (model) / dispose (oracle) as a + // single chained bundle. `source` extraction below needs no change: + // both schemas carry a top-level `source` label. Chain VERIFY needs + // zero changes beyond this: pinned seals and subprocess + // re-verification (`buildc receipt verify `) already compose + // through the schema-agnostic dispatch this widening exercises. + if schema != SCIENTIFIC_RUNTIME_SCHEMA && schema != MODEL_RECEIPT_SCHEMA { eprintln!( - "Error: '{}' is not a scientific-runtime receipt (schema `{}`)", + "Error: '{}' is not a chainable receipt (schema `{}`; expected `{}` or `{}`)", path.display(), - schema + schema, + SCIENTIFIC_RUNTIME_SCHEMA, + MODEL_RECEIPT_SCHEMA ); return Err(1); } @@ -2714,6 +2726,9 @@ fn cmd_receipt_verify( if schema == SCIENTIFIC_RUNTIME_SCHEMA { return verify_scientific_receipt_dispatch(&receipt, source_override, false); } + if schema == MODEL_RECEIPT_SCHEMA { + return verify_model_boundary_receipt(&receipt, false); + } if schema != "buildlang-check-receipt/v1" { eprintln!("Error: unsupported check receipt schema `{}`", schema); return Err(1); @@ -2846,6 +2861,18 @@ fn cmd_receipt_verify_json( return verify_scientific_receipt_dispatch(&receipt, source_override, true); } + // Model boundary receipts (design: + // docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md): + // offline schema/seal/field-contract verification only, no re-run. Routed + // the same way as the scientific-runtime arm above, before the + // check-receipt schema guard. + if receipt_field_str(&receipt, "/schema", "schema") + .map_err(|code| receipt_load_failure(true, "SCHEMA_UNSUPPORTED", code))? + == MODEL_RECEIPT_SCHEMA + { + return verify_model_boundary_receipt(&receipt, true); + } + let mut checks = Vec::new(); let schema = receipt_field_str(&receipt, "/schema", "schema")?; diff --git a/compiler/src/model_receipt.rs b/compiler/src/model_receipt.rs new file mode 100644 index 0000000..dc190b0 --- /dev/null +++ b/compiler/src/model_receipt.rs @@ -0,0 +1,494 @@ +// =============================================================================== +// BUILDLANG MODEL BOUNDARY RECEIPT - offline verify arm for a harness-emitted +// provenance artifact over a `Model`-capability boundary crossing +// =============================================================================== +// Copyright (c) 2026 Zain Dana Harper. BuildLang Fair-Source License v1.0. +// =============================================================================== +// +//! `buildlang-model-boundary-receipt/v0`: a receipt about a boundary crossing +//! the harness-side shim (`harness/model_shim.py` in local-model) witnessed, +//! never emitted by buildc itself. This module implements ONLY the read side +//! -- schema struct, seal recompute, and field-shape contracts for `buildc +//! receipt verify` -- because emission belongs to the shim (see +//! docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md, +//! section 1: the shim is the only party that observes prompt bytes, reply +//! bytes, and its own adapter identity at once). +//! +//! This is deliberately a SEPARATE module from `scientific_runtime`, not a +//! section of it: the whole point of the artifact is that it is NOT +//! scientific evidence. A model receipt carries no invariant, no oracle, no +//! verdict -- it witnesses that a proposal crossed the boundary and what +//! bytes crossed, nothing more. The scientific verifier's +//! `CAPABILITY_INADMISSIBLE` refusal of any `Model`-observing program is +//! untouched by this module; the two artifact kinds share a seal idiom and a +//! verifier binary, never a claim vocabulary. +//! +//! Every field in the schema is tagged in the design doc as either +//! SHIM-WITNESSED (the shim observed the bytes or performed the act itself) +//! or DECLARED (someone's say-so passed through unwitnessed). The seal makes +//! tampering evident; it does not upgrade a declaration into a witness, and +//! this module's verify arm does not pretend otherwise: it checks integrity +//! and internal coherence only, never anything about the model itself (there +//! is no re-run -- the artifact witnesses a PAST crossing). + +use sha2::{Digest, Sha256}; + +/// Schema tag for a model boundary receipt (see the module doc and design +/// section 2). Flat top-level `schema` + top-level `seal`, mirroring the +/// scientific receipt's shape so the existing chain pointers `/schema` and +/// `/seal/hex` read it unchanged (design section 6). +pub const MODEL_RECEIPT_SCHEMA: &str = "buildlang-model-boundary-receipt/v0"; + +/// `{ algorithm, hex }`, the receipt's own integrity seal. A distinct type +/// from `scientific_runtime::ScientificDigest` on purpose: this module does +/// not depend on the scientific module, by design (see the module doc). +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelReceiptSeal { + pub algorithm: String, + pub hex: String, +} + +/// `shim`: SHIM-WITNESSED self-identity (design section 2 row 3). +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelReceiptShim { + pub name: String, + pub version: String, + /// `"echo"` | `"ollama"`. + pub mode: String, +} + +/// `session`: timestamps are SHIM-CLOCK-DECLARED (ordering witnessed, wall +/// accuracy is the host's); `reply_written_utc` is `null` for a receipt whose +/// outcome never reached a reply (design section 2 row 4). +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelReceiptSession { + pub listen: String, + pub nonce: String, + pub request_received_utc: String, + pub reply_written_utc: Option, +} + +/// The `prompt` / `reply` blocks: SHIM-WITNESSED `{ sha256, bytes }` over raw +/// bytes, never plaintext (design section 2 rows 5-6, section 3). `bytes` is +/// a byte COUNT, not content: the receipt is shareable, and whoever holds the +/// plaintext can re-hash it to check `sha256`. +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelReceiptHashedBytes { + pub sha256: String, + pub bytes: u64, +} + +/// `model.daemon_digest`: DAEMON-DECLARED even when `FETCHED` -- the shim +/// witnesses the fetch, not the weights (design section 3). `hex` is present +/// IFF `status == "FETCHED"`; present alongside `"UNAVAILABLE"` is a +/// `FIELD_CONTRACT_VIOLATION` (design section 5). +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelReceiptDaemonDigest { + /// `"FETCHED"` | `"UNAVAILABLE"`. + pub status: String, + #[serde(default, skip_serializing_if = "Option::is_none")] + pub hex: Option, +} + +/// `model`: echo mode carries only `name`; ollama mode additionally carries +/// `endpoint`, `request_body_sha256` (SHIM-WITNESSED: the exact JSON POSTed), +/// and `daemon_digest` (design section 2 row 7). The three ollama-only fields +/// are OMITTED (not null) on an echo receipt, which is why they are +/// `skip_serializing_if`, unlike `prompt`/`reply` which are explicit `null`. +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelReceiptModel { + /// DECLARED: a string is not a digest. + pub name: String, + #[serde(default, skip_serializing_if = "Option::is_none")] + pub endpoint: Option, + #[serde(default, skip_serializing_if = "Option::is_none")] + pub request_body_sha256: Option, + #[serde(default, skip_serializing_if = "Option::is_none")] + pub daemon_digest: Option, +} + +/// `seed`: SHIM-WITNESSED as to what was SENT, never a claim the daemon +/// honored it (design section 2 row 8). v1's shim sends no `options.seed`, +/// so every v1 receipt carries `{ status: "NOT_SENT" }`; the `SENT` variant +/// is schema headroom for a future `--seed` flag, not exercised by v1. +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelReceiptSeed { + /// `"NOT_SENT"` | `"SENT"`. + pub status: String, + #[serde(default, skip_serializing_if = "Option::is_none")] + pub value: Option, +} + +/// The model boundary receipt itself. Field order is FIXED and matches the +/// design's schema table exactly: it is the canonical (sealed) order, and +/// `serde_json::to_vec` preserves struct field order, which is the Rust half +/// of the cross-language canonicalization contract (design section 2, +/// "Seal and the cross-language canonicalization contract"). Do not reorder +/// these fields without re-deriving the golden fixture's seal. +#[derive(Clone, Debug, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct ModelBoundaryReceipt { + pub schema: String, + /// `model::`, e.g. `model:echo:echo/v1`. DECLARED label; lets + /// `ReceiptChainLink.source` carry a human-readable member label with + /// zero chain-code change (design section 2 row 2, section 6). + pub source: String, + pub shim: ModelReceiptShim, + pub session: ModelReceiptSession, + /// `null` IFF `outcome == "PROTOCOL_VIOLATION"` (the line never + /// terminated, so there is nothing to hash). + pub prompt: Option, + /// `null` unless `outcome == "COMPLETED"`. + pub reply: Option, + pub model: ModelReceiptModel, + pub seed: ModelReceiptSeed, + /// `"COMPLETED"` | `"FAILED_CLOSED"` | `"PROTOCOL_VIOLATION"`. + pub outcome: String, + pub seal: ModelReceiptSeal, +} + +fn sha256_hex(bytes: &[u8]) -> String { + let digest = Sha256::digest(bytes); + let mut hex = String::with_capacity(digest.len() * 2); + for byte in digest { + use std::fmt::Write as _; + let _ = write!(&mut hex, "{byte:02x}"); + } + hex +} + +/// Seal a receipt in place: same idiom as +/// `scientific_runtime::seal_receipt` (sha256 over the canonical JSON with +/// `seal.hex` blanked and `seal.algorithm` fixed to `"sha256"`). Used by +/// tests to build valid fixtures; buildc itself never emits this artifact +/// (emission is the shim's job -- see the module doc), so this is dead code +/// in a non-test build, same as `gpu_receipt::emit_gpu_receipt` outside the +/// `gpu` feature. +#[allow(dead_code)] +pub fn seal_model_receipt(receipt: &mut ModelBoundaryReceipt) { + receipt.seal.algorithm = "sha256".to_string(); + receipt.seal.hex.clear(); + let canonical = serde_json::to_vec(receipt).expect("serialize model boundary receipt"); + receipt.seal.hex = sha256_hex(&canonical); +} + +/// Re-derive the seal from a receipt read back from disk and compare against +/// the stored `seal.hex`. This is the Rust half of the cross-language +/// canonicalization contract: the Python emitter must produce byte-identical +/// canonical bytes for the same logical receipt, pinned by the golden +/// fixture test in both repos. +pub fn recompute_seal_hex(receipt: &ModelBoundaryReceipt) -> String { + let mut probe = receipt.clone(); + probe.seal.algorithm = "sha256".to_string(); + probe.seal.hex.clear(); + let canonical = serde_json::to_vec(&probe).expect("serialize model boundary receipt"); + sha256_hex(&canonical) +} + +/// A sealed digest field must be a real sha256: exactly 64 hex chars. Same +/// rule as the scientific verifier's `digest_is_well_formed`: an absent or +/// malformed hash cannot masquerade as witnessed provenance +/// (`DIGEST_MALFORMED`). +fn digest_hex_is_well_formed(hex: &str) -> bool { + hex.len() == 64 && hex.chars().all(|ch| ch.is_ascii_hexdigit()) +} + +/// Report a stable machine-readable `failure_class` for a model-receipt +/// verify failure and return the exit code to propagate. Same shape as +/// `scientific_runtime::verify_failure_class`: a `failure_class: ` line +/// on stderr always, plus a JSON failure report on stdout in `--json` mode. +/// Deliberately reuses the SHARED failure taxonomy (no new classes for v1, +/// design section 5): a reader of any buildc refusal already knows these +/// words. +fn model_failure_class(json: bool, failure_class: &str, exit_code: i32) -> i32 { + eprintln!("failure_class: {failure_class}"); + if json { + let report = serde_json::json!({ + "status": "failed", + "failure_class": failure_class, + }); + if let Ok(text) = serde_json::to_string_pretty(&report) { + println!("{text}"); + } + } + exit_code +} + +/// Verify a model boundary receipt: offline only, no re-run (there is +/// nothing to re-run -- the artifact witnesses a past crossing). Checks, in +/// order (design section 5): +/// +/// 1. The document deserializes into the typed schema (`MALFORMED` +/// otherwise; schema-tag mismatch is caught by the caller's dispatch +/// before this function is reached). +/// 2. Seal integrity (`SEAL_MISMATCH`), BEFORE any sealed field is +/// interpreted -- same ordering discipline as the scientific verifier, so +/// every field-level rejection below is known to concern a genuinely +/// author-sealed value. +/// 3. Digest well-formedness (`DIGEST_MALFORMED`): `prompt.sha256`, +/// `reply.sha256` (when present), `model.request_body_sha256` (when +/// present), `model.daemon_digest.hex` (when present) must each be 64 hex +/// chars. +/// 4. Status coherence (`FIELD_CONTRACT_VIOLATION`), exactly the three cases +/// the design names: `daemon_digest.hex` present alongside status +/// `UNAVAILABLE`; a `COMPLETED` outcome with a `null` reply; a +/// `PROTOCOL_VIOLATION` outcome with a present (non-null) prompt. +/// +/// Deliberately NO new failure classes (design section 5): the shared +/// taxonomy with the scientific verifier is a feature. +pub fn verify_model_boundary_receipt( + receipt_json: &serde_json::Value, + json: bool, +) -> Result<(), i32> { + let receipt: ModelBoundaryReceipt = + serde_json::from_value(receipt_json.clone()).map_err(|err| { + eprintln!("Error: model boundary receipt is malformed: {err}"); + model_failure_class(json, "MALFORMED", 1) + })?; + + // Integrity gate FIRST, before any sealed field is interpreted (mirrors + // the scientific verifier's ordering contract). + let recomputed_seal = recompute_seal_hex(&receipt); + if !recomputed_seal.eq_ignore_ascii_case(&receipt.seal.hex) { + eprintln!( + "Error: seal mismatch: receipt sha256:{}, recomputed sha256:{}", + receipt.seal.hex, recomputed_seal + ); + return Err(model_failure_class(json, "SEAL_MISMATCH", 1)); + } + + // Digest well-formedness. + if let Some(prompt) = &receipt.prompt { + if !digest_hex_is_well_formed(&prompt.sha256) { + eprintln!("Error: malformed digest in `prompt.sha256`"); + return Err(model_failure_class(json, "DIGEST_MALFORMED", 1)); + } + } + if let Some(reply) = &receipt.reply { + if !digest_hex_is_well_formed(&reply.sha256) { + eprintln!("Error: malformed digest in `reply.sha256`"); + return Err(model_failure_class(json, "DIGEST_MALFORMED", 1)); + } + } + if let Some(request_body_sha256) = &receipt.model.request_body_sha256 { + if !digest_hex_is_well_formed(request_body_sha256) { + eprintln!("Error: malformed digest in `model.request_body_sha256`"); + return Err(model_failure_class(json, "DIGEST_MALFORMED", 1)); + } + } + if let Some(daemon_digest) = &receipt.model.daemon_digest { + if let Some(hex) = &daemon_digest.hex { + if !digest_hex_is_well_formed(hex) { + eprintln!("Error: malformed digest in `model.daemon_digest.hex`"); + return Err(model_failure_class(json, "DIGEST_MALFORMED", 1)); + } + } + } + + // Status coherence: exactly the three cases the design names. + if let Some(daemon_digest) = &receipt.model.daemon_digest { + if daemon_digest.status == "UNAVAILABLE" && daemon_digest.hex.is_some() { + eprintln!("Error: `model.daemon_digest.hex` is present alongside status `UNAVAILABLE`"); + return Err(model_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + } + if receipt.outcome == "COMPLETED" && receipt.reply.is_none() { + eprintln!("Error: outcome `COMPLETED` carries a null `reply`"); + return Err(model_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + if receipt.outcome == "PROTOCOL_VIOLATION" && receipt.prompt.is_some() { + eprintln!("Error: outcome `PROTOCOL_VIOLATION` carries a present `prompt`"); + return Err(model_failure_class(json, "FIELD_CONTRACT_VIOLATION", 1)); + } + + if json { + let out = serde_json::json!({ + "schema": MODEL_RECEIPT_SCHEMA, + "status": "verified", + "source": receipt.source, + "outcome": receipt.outcome, + "seal": { "algorithm": "sha256", "hex": receipt.seal.hex }, + }); + let text = serde_json::to_string_pretty(&out).map_err(|err| { + eprintln!("Error serializing model receipt verification report: {err}"); + 1 + })?; + println!("{text}"); + } else { + println!( + "model receipt: VERIFIED (seal intact, field contracts hold; source={}, outcome={}). \ + This artifact witnesses a past boundary crossing only: no re-run, no claim about \ + model quality, weights, or determinism.", + receipt.source, receipt.outcome + ); + } + Ok(()) +} + +#[cfg(test)] +mod tests { + use super::*; + + /// Build a valid, sealed echo-mode COMPLETED receipt matching the golden + /// fixture's logical content exactly (see + /// compiler/tests/fixtures/model-receipt-golden.json). Kept in sync by + /// hand; the golden-fixture test below is the actual cross-repo pin. + fn sample_receipt() -> ModelBoundaryReceipt { + let mut r = ModelBoundaryReceipt { + schema: MODEL_RECEIPT_SCHEMA.to_string(), + source: "model:echo:echo/v1".to_string(), + shim: ModelReceiptShim { + name: "model_shim.py".to_string(), + version: "0.1.0".to_string(), + mode: "echo".to_string(), + }, + session: ModelReceiptSession { + listen: "127.0.0.1:8931".to_string(), + nonce: "a1b2c3d4".to_string(), + request_received_utc: "2026-07-29T00:00:00Z".to_string(), + reply_written_utc: Some("2026-07-29T00:00:00Z".to_string()), + }, + prompt: Some(ModelReceiptHashedBytes { + sha256: "758d61f26a44448384e5c4468a0dcb7a2abe456067b0f7b505bc28b9411fe931" + .to_string(), + bytes: 4, + }), + reply: Some(ModelReceiptHashedBytes { + sha256: "de2406a7ccdb9add6361bdf86cfd31dfaa95806f8d42f91102290ae3abe5afae" + .to_string(), + bytes: 10, + }), + model: ModelReceiptModel { + name: "echo/v1".to_string(), + endpoint: None, + request_body_sha256: None, + daemon_digest: None, + }, + seed: ModelReceiptSeed { + status: "NOT_SENT".to_string(), + value: None, + }, + outcome: "COMPLETED".to_string(), + seal: ModelReceiptSeal { + algorithm: "sha256".to_string(), + hex: String::new(), + }, + }; + seal_model_receipt(&mut r); + r + } + + #[test] + fn seal_round_trips_through_serialize_deserialize() { + let r = sample_receipt(); + let value = serde_json::to_value(&r).expect("to_value"); + let reloaded: ModelBoundaryReceipt = serde_json::from_value(value).expect("from_value"); + assert_eq!(recompute_seal_hex(&reloaded), reloaded.seal.hex); + } + + #[test] + fn a_valid_receipt_verifies() { + let r = sample_receipt(); + let value = serde_json::to_value(&r).expect("to_value"); + assert!(verify_model_boundary_receipt(&value, false).is_ok()); + } + + #[test] + fn seal_mismatch_is_rejected_before_any_field_contract_is_interpreted() { + // An unsealed edit to a witnessed field must report SEAL_MISMATCH, + // not whichever field-contract check it happens to trip. Flip the + // reply hash's first hex char without resealing. + let mut r = sample_receipt(); + r.reply.as_mut().unwrap().sha256 = "0".repeat(64); + let value = serde_json::to_value(&r).expect("to_value"); + let err = verify_model_boundary_receipt(&value, false).unwrap_err(); + assert_eq!(err, 1); + } + + #[test] + fn seal_mismatch_reports_the_expected_failure_class() { + let mut r = sample_receipt(); + r.session.nonce = "ffffffff".to_string(); // unsealed edit + let value = serde_json::to_value(&r).expect("to_value"); + assert!(verify_model_boundary_receipt(&value, true).is_err()); + // The JSON report and the stderr line both carry SEAL_MISMATCH; the + // stderr line is asserted at the CLI-integration layer (cli.rs), + // this unit test only pins the Result is Err. + } + + #[test] + fn resealed_daemon_digest_hex_with_unavailable_status_is_field_contract_violation() { + let mut r = sample_receipt(); + r.shim.mode = "ollama".to_string(); + r.model = ModelReceiptModel { + name: "llama3.2".to_string(), + endpoint: Some("http://127.0.0.1:11434".to_string()), + request_body_sha256: Some("1".repeat(64)), + daemon_digest: Some(ModelReceiptDaemonDigest { + status: "UNAVAILABLE".to_string(), + hex: Some("2".repeat(64)), + }), + }; + seal_model_receipt(&mut r); // reseal so this reaches the contract gate + let value = serde_json::to_value(&r).expect("to_value"); + let err = verify_model_boundary_receipt(&value, false).unwrap_err(); + assert_eq!(err, 1); + } + + #[test] + fn resealed_completed_outcome_with_null_reply_is_field_contract_violation() { + let mut r = sample_receipt(); + r.reply = None; + seal_model_receipt(&mut r); + let value = serde_json::to_value(&r).expect("to_value"); + assert!(verify_model_boundary_receipt(&value, false).is_err()); + } + + #[test] + fn resealed_protocol_violation_with_present_prompt_is_field_contract_violation() { + let mut r = sample_receipt(); + r.outcome = "PROTOCOL_VIOLATION".to_string(); + r.reply = None; // a PROTOCOL_VIOLATION receipt never has a reply either + seal_model_receipt(&mut r); + let value = serde_json::to_value(&r).expect("to_value"); + assert!(verify_model_boundary_receipt(&value, false).is_err()); + } + + #[test] + fn malformed_digest_is_rejected() { + let mut r = sample_receipt(); + r.prompt.as_mut().unwrap().sha256 = "not-a-real-digest".to_string(); + seal_model_receipt(&mut r); + let value = serde_json::to_value(&r).expect("to_value"); + assert!(verify_model_boundary_receipt(&value, false).is_err()); + } + + #[test] + fn a_required_field_removed_is_malformed() { + let r = sample_receipt(); + let mut value = serde_json::to_value(&r).expect("to_value"); + value.as_object_mut().unwrap().remove("shim"); + assert!(verify_model_boundary_receipt(&value, false).is_err()); + } + + /// The cross-language canonicalization contract (design section 2): the + /// golden fixture is checked into BOTH repos with the SAME seal. This + /// test is the buildlang half of that pin -- if it fails, the Python + /// sealer and this Rust sealer have diverged and the contract is broken. + #[test] + fn golden_fixture_reseals_to_its_pinned_seal() { + let text = include_str!("../tests/fixtures/model-receipt-golden.json"); + let value: serde_json::Value = serde_json::from_str(text).expect("parse golden fixture"); + let receipt: ModelBoundaryReceipt = + serde_json::from_value(value.clone()).expect("golden fixture matches schema"); + let recomputed = recompute_seal_hex(&receipt); + assert_eq!( + recomputed, receipt.seal.hex, + "golden fixture seal must reseal identically (cross-language pin)" + ); + assert_eq!( + receipt.seal.hex, "6bb2a09c47f5eaa2e3208a5eadcd6d57d1faffa74a567e024e920571c3794035", + "golden fixture's PINNED seal changed -- this breaks the cross-repo contract" + ); + assert!(verify_model_boundary_receipt(&value, false).is_ok()); + } +} diff --git a/compiler/tests/cli.rs b/compiler/tests/cli.rs index 4ec7456..f01fbab 100644 --- a/compiler/tests/cli.rs +++ b/compiler/tests/cli.rs @@ -18194,3 +18194,281 @@ fn units_check_receipt_clean_and_mismatch() { "unit mismatch: cannot add `m` and `s` (dimensions differ)" ); } + +// ============================================================================= +// MODEL BOUNDARY RECEIPT (buildlang-model-boundary-receipt/v0) +// +// Design: docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md +// Emission belongs to the harness-side shim (local-model), never to buildc; +// these tests exercise the READ side only -- `receipt verify`'s model arm and +// the chain-build allowlist widening -- against hand-built and golden-fixture +// JSON. No C backend is required for any test in this section. +// ============================================================================= + +fn model_receipt_golden_fixture_path() -> PathBuf { + repo_root() + .join("compiler") + .join("tests") + .join("fixtures") + .join("model-receipt-golden.json") +} + +#[test] +fn model_receipt_golden_fixture_verifies_byte_identically() { + // The cross-repo pin (design section 2, "Seal and the cross-language + // canonicalization contract"): this exact file, with this exact seal, is + // ALSO checked into the local-model / _wshim repo, sealed there by the + // Python shim. buildc's verify arm accepting it here is the buildlang + // half of the byte-identity claim. + let verify = buildc() + .args(["receipt", "verify"]) + .arg(model_receipt_golden_fixture_path()) + .output() + .expect("verify golden model receipt"); + assert!( + verify.status.success(), + "the golden model receipt must verify\nstdout:\n{}\nstderr:\n{}", + String::from_utf8_lossy(&verify.stdout), + String::from_utf8_lossy(&verify.stderr) + ); + let stdout = String::from_utf8_lossy(&verify.stdout); + assert!( + stdout.contains("VERIFIED"), + "human output should report VERIFIED\nstdout:\n{stdout}" + ); + + let verify_json = buildc() + .args(["receipt", "verify"]) + .arg(model_receipt_golden_fixture_path()) + .arg("--json") + .output() + .expect("verify golden model receipt --json"); + assert!( + verify_json.status.success(), + "--json verify must also succeed" + ); + let report = receipt_from_stdout(&verify_json); + assert_eq!(report["schema"], "buildlang-model-boundary-receipt/v0"); + assert_eq!(report["status"], "verified"); + assert_eq!( + report["seal"]["hex"], + "6bb2a09c47f5eaa2e3208a5eadcd6d57d1faffa74a567e024e920571c3794035" + ); +} + +#[test] +fn model_receipt_seal_mismatch_is_rejected() { + // A resealed-looking edit that was NOT actually resealed: the integrity + // gate must catch it before any field-contract check runs. + let mut receipt: serde_json::Value = + serde_json::from_slice(&fs::read(model_receipt_golden_fixture_path()).unwrap()).unwrap(); + receipt["session"]["nonce"] = serde_json::Value::String("ffffffff".to_string()); + let dir = std::env::temp_dir().join(format!("buildlang_model_seal_{}", std::process::id())); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + let path = dir.join("tampered.json"); + fs::write(&path, serde_json::to_vec_pretty(&receipt).unwrap()).unwrap(); + + let verify = buildc() + .args(["receipt", "verify"]) + .arg(&path) + .output() + .expect("verify tampered model receipt"); + assert!( + !verify.status.success(), + "an unsealed edit must fail verify" + ); + assert!( + String::from_utf8_lossy(&verify.stderr).contains("failure_class: SEAL_MISMATCH"), + "an unsealed edit must report SEAL_MISMATCH\nstderr:\n{}", + String::from_utf8_lossy(&verify.stderr) + ); + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn model_receipt_resealed_field_shape_violation_is_rejected() { + // A COMPLETED outcome with a null reply, re-sealed so the tamper reaches + // the field-contract gate instead of tripping SEAL_MISMATCH first. + // + // The reseal is computed over a HAND-BUILT canonical string, not by + // round-tripping through `serde_json::Value` (this crate's `Value` is a + // `BTreeMap`, so re-serializing a `Value` sorts keys ALPHABETICALLY -- + // it would NOT reproduce the struct-field-order canonicalization the + // real seal uses). The string below mirrors the golden fixture's field + // order with `reply` set to `null`, exactly as `model_receipt.rs`'s + // typed struct would serialize it. + let mut receipt: serde_json::Value = + serde_json::from_slice(&fs::read(model_receipt_golden_fixture_path()).unwrap()).unwrap(); + receipt["reply"] = serde_json::Value::Null; + let canonical = concat!( + r#"{"schema":"buildlang-model-boundary-receipt/v0","source":"model:echo:echo/v1","#, + r#""shim":{"name":"model_shim.py","version":"0.1.0","mode":"echo"},"#, + r#""session":{"listen":"127.0.0.1:8931","nonce":"a1b2c3d4","#, + r#""request_received_utc":"2026-07-29T00:00:00Z","reply_written_utc":"2026-07-29T00:00:00Z"},"#, + r#""prompt":{"sha256":"758d61f26a44448384e5c4468a0dcb7a2abe456067b0f7b505bc28b9411fe931","bytes":4},"#, + r#""reply":null,"model":{"name":"echo/v1"},"seed":{"status":"NOT_SENT"},"#, + r#""outcome":"COMPLETED","seal":{"algorithm":"sha256","hex":""}}"#, + ); + receipt["seal"]["hex"] = serde_json::Value::String(sha256_hex(canonical.as_bytes())); + + let dir = std::env::temp_dir().join(format!("buildlang_model_fcv_{}", std::process::id())); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + let path = dir.join("resealed_bad_shape.json"); + fs::write(&path, serde_json::to_vec_pretty(&receipt).unwrap()).unwrap(); + + let verify = buildc() + .args(["receipt", "verify"]) + .arg(&path) + .output() + .expect("verify resealed field-shape violation"); + assert!( + !verify.status.success(), + "a re-sealed COMPLETED-with-null-reply receipt must still fail verify" + ); + assert!( + String::from_utf8_lossy(&verify.stderr).contains("failure_class: FIELD_CONTRACT_VIOLATION"), + "must report FIELD_CONTRACT_VIOLATION\nstderr:\n{}", + String::from_utf8_lossy(&verify.stderr) + ); + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn model_receipt_chain_build_refuses_before_the_allowlist_widening_check() { + // Sanity: an unrelated schema (neither scientific-runtime nor + // model-boundary-receipt) is still refused by chain build. This pins the + // allowlist is exactly two members, not "anything with a seal". + let dir = std::env::temp_dir().join(format!( + "buildlang_model_chain_refuse_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + let bogus = serde_json::json!({ + "schema": "not-a-real-schema/v0", + "source": "nowhere", + "seal": { "algorithm": "sha256", "hex": "0".repeat(64) }, + }); + let a = dir.join("bogus.json"); + fs::write(&a, serde_json::to_vec_pretty(&bogus).unwrap()).unwrap(); + let b = model_receipt_golden_fixture_path(); + let out = dir.join("chain.json"); + let build = buildc() + .args(["receipt", "chain", "build"]) + .arg(&a) + .arg(&b) + .arg("-o") + .arg(&out) + .output() + .expect("attempt chain build with a bogus schema member"); + assert!( + !build.status.success(), + "chain build must refuse a member whose schema is neither allowlisted schema" + ); + let _ = fs::remove_dir_all(&dir); +} + +#[test] +fn model_receipt_chains_beside_a_scientific_receipt_and_tamper_breaks_it() { + // The propose/dispose demo (design section 6): a model receipt (the + // proposal crossing) chained beside a scientific-runtime receipt (a + // Model-FREE disposer kernel), bound in order. Tampering the model member + // must break the chain even though the scientific member is untouched -- + // this is the chain-build allowlist widening plus the verify arm + // composing with ZERO changes to the schema-agnostic chain machinery. + if !c_backend_ready() { + eprintln!( + "skipping model_receipt_chains_beside_a_scientific_receipt_and_tamper_breaks_it: C backend not ready" + ); + return; + } + let dir = std::env::temp_dir().join(format!("buildlang_model_chain_{}", std::process::id())); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("create fixture dir"); + + // Member 0: the model receipt (the proposer). Copy the golden fixture + // byte-for-byte so its seal stays intact. + let model_member = dir.join("model.json"); + fs::copy(model_receipt_golden_fixture_path(), &model_member) + .expect("copy golden model receipt as chain member 0"); + let model_member_original = fs::read(&model_member).expect("snapshot model member"); + + // Member 1: a Model-free scientific-runtime receipt (the disposer). Any + // corpus kernel works; CAPABILITY_INADMISSIBLE never fires because this + // kernel does not observe Model -- the rule is demonstrated by what each + // chain member IS, not bent. + let sci_member = dir.join("sci.json"); + let emit = buildc() + .arg("run") + .arg(repo_example("funnel_probe.bld")) + .args(["--emit-receipt"]) + .arg(&sci_member) + .args([ + "--invariant", + "non-negative", + "--metric", + "slack", + "--problem", + "disposer", + ]) + .output() + .expect("emit disposer receipt"); + assert!( + emit.status.success(), + "emitting the disposer receipt should succeed" + ); + + let chain = dir.join("chain.json"); + let build = buildc() + .args(["receipt", "chain", "build"]) + .arg(&model_member) + .arg(&sci_member) + .arg("-o") + .arg(&chain) + .output() + .expect("build propose/dispose chain"); + assert!( + build.status.success(), + "chaining a model receipt beside a scientific receipt must succeed\nstderr:\n{}", + String::from_utf8_lossy(&build.stderr) + ); + + let verify = buildc() + .args(["receipt", "chain", "verify"]) + .arg(&chain) + .output() + .expect("verify propose/dispose chain"); + assert!( + verify.status.success(), + "the clean propose/dispose chain must verify\nstdout:\n{}\nstderr:\n{}", + String::from_utf8_lossy(&verify.stdout), + String::from_utf8_lossy(&verify.stderr) + ); + + // Tamper the model member's body WITHOUT touching its seal.hex text + // field: the chain's pinned-seal check (step 2) still matches, so the + // break is caught only when `receipt verify` re-derives the seal over + // the now-inconsistent body (step 3), reported as CHAIN_LINK_UNVERIFIED. + let mut tampered: serde_json::Value = serde_json::from_slice(&model_member_original).unwrap(); + tampered["prompt"]["bytes"] = serde_json::Value::from(999); + fs::write(&model_member, serde_json::to_vec_pretty(&tampered).unwrap()).unwrap(); + + let verify_tampered = buildc() + .args(["receipt", "chain", "verify"]) + .arg(&chain) + .output() + .expect("verify chain with a tampered model member"); + assert!( + !verify_tampered.status.success(), + "a tampered model member must break the chain" + ); + assert!( + String::from_utf8_lossy(&verify_tampered.stderr).contains("CHAIN_LINK_UNVERIFIED"), + "a model member whose body no longer re-seals must report CHAIN_LINK_UNVERIFIED\nstderr:\n{}", + String::from_utf8_lossy(&verify_tampered.stderr) + ); + + let _ = fs::remove_dir_all(&dir); +} diff --git a/compiler/tests/fixtures/model-receipt-golden.json b/compiler/tests/fixtures/model-receipt-golden.json new file mode 100644 index 0000000..befc50b --- /dev/null +++ b/compiler/tests/fixtures/model-receipt-golden.json @@ -0,0 +1,34 @@ +{ + "schema": "buildlang-model-boundary-receipt/v0", + "source": "model:echo:echo/v1", + "shim": { + "name": "model_shim.py", + "version": "0.1.0", + "mode": "echo" + }, + "session": { + "listen": "127.0.0.1:8931", + "nonce": "a1b2c3d4", + "request_received_utc": "2026-07-29T00:00:00Z", + "reply_written_utc": "2026-07-29T00:00:00Z" + }, + "prompt": { + "sha256": "758d61f26a44448384e5c4468a0dcb7a2abe456067b0f7b505bc28b9411fe931", + "bytes": 4 + }, + "reply": { + "sha256": "de2406a7ccdb9add6361bdf86cfd31dfaa95806f8d42f91102290ae3abe5afae", + "bytes": 10 + }, + "model": { + "name": "echo/v1" + }, + "seed": { + "status": "NOT_SENT" + }, + "outcome": "COMPLETED", + "seal": { + "algorithm": "sha256", + "hex": "6bb2a09c47f5eaa2e3208a5eadcd6d57d1faffa74a567e024e920571c3794035" + } +} diff --git a/docs/MODEL-RECEIPT.md b/docs/MODEL-RECEIPT.md new file mode 100644 index 0000000..5e289da --- /dev/null +++ b/docs/MODEL-RECEIPT.md @@ -0,0 +1,183 @@ +# Model Boundary Receipt (`buildlang-model-boundary-receipt/v0`) + +> Status: **v1, verify arm shipped 2026-07-29** (buildc side only). Emission is +> harness-side (`harness/model_shim.py`, the local-model repo's `--receipt-dir` +> flag), never buildc. This is the contract that side implements against. +> Design of record: +> `docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md`. + +A model boundary receipt is a PROVENANCE artifact about one connection to +BuildLang's `Model` capability wire contract (`model_complete`, a line +protocol over TCP to `BUILD_MODEL_ENDPOINT`; see the `model_complete` +paragraph in [SCIENTIFIC-RECEIPT.md](SCIENTIFIC-RECEIPT.md)). It carries no +invariant, no oracle, and no verdict, by construction: models propose; this +artifact witnesses THAT they proposed and WHAT bytes crossed, nothing more. + +## Honest scope + +Claims (all offline-checkable): these exact bytes crossed the boundary, in +this session, in this order, under this shim mode, and this is what the +adapter's daemon declared about itself at the time. + +Refuses, explicitly, by the schema's absence of fields: quality or +correctness of the completion; that `model.name` corresponds to any +particular weights; that `daemon_digest.hex` corresponds to the weights +actually consulted (it is the daemon's declaration about itself, witnessed +only as a fetch, never as ground truth); determinism (not claimed even for +echo mode, whose reply happens to be re-derivable from the spec); that the +reply derived from the prompt at all (the shim observed a request and a +response on one connection; causality inside the daemon is not witnessed). + +The scientific-runtime receipt's `CAPABILITY_INADMISSIBLE` refusal of any +`Model`-observing program (`scientific_runtime.rs`, `receipt verify`) is +**untouched** by this schema. A model receipt cannot become scientific +evidence and a scientific receipt cannot carry `Model` -- the two artifact +kinds share a seal idiom and a verifier binary, never a claim vocabulary. + +## The schema + +Flat top-level `schema` string plus top-level `seal`, mirroring the +scientific receipt's shape so the existing chain pointers `/schema` and +`/seal/hex` read it unchanged. Fields, in canonical (sealed) order -- this +order is load-bearing: it is exactly the Rust struct's serde field order in +`compiler/src/model_receipt.rs::ModelBoundaryReceipt`, and `serde_json::to_vec` +preserves struct field order, which is half of the cross-language +canonicalization contract below. + +| field | content | epistemic tag | +|---|---|---| +| `schema` | `buildlang-model-boundary-receipt/v0` | structural | +| `source` | `model::` (e.g. `model:echo:echo/v1`) | DECLARED label; carries a human-readable chain-member label | +| `shim` | `{ name: "model_shim.py", version, mode: "echo"\|"ollama" }` | SHIM-WITNESSED (self-identity) | +| `session` | `{ listen, nonce, request_received_utc, reply_written_utc\|null }` | timestamps SHIM-CLOCK-DECLARED; `reply_written_utc` is `null` unless the outcome reached a reply | +| `prompt` | `{ sha256, bytes }` over the raw prompt-line bytes as received (line terminator stripped, before UTF-8 decode), or `null` iff `outcome == "PROTOCOL_VIOLATION"` | SHIM-WITNESSED | +| `reply` | `{ sha256, bytes }` over the sanitized completion bytes exactly as written (protocol terminator excluded), or `null` unless `outcome == "COMPLETED"` | SHIM-WITNESSED | +| `model` | echo: `{ name: "echo/v1" }`. ollama: `{ name, endpoint, request_body_sha256, daemon_digest: { status: "FETCHED"\|"UNAVAILABLE", hex? } }` | `name` is DECLARED; `request_body_sha256` is SHIM-WITNESSED over the exact JSON POSTed; `daemon_digest` is DAEMON-DECLARED even when `FETCHED` (the shim witnesses the fetch, not the weights) | +| `seed` | `{ status: "NOT_SENT" }` in v1; `{ status: "SENT", value }` is schema headroom for a future `--seed` flag, not exercised by v1 | SHIM-WITNESSED as to what was sent, never a claim the daemon honored it | +| `outcome` | `"COMPLETED"` \| `"FAILED_CLOSED"` (adapter failure, nothing written; `reply` null) \| `"PROTOCOL_VIOLATION"` (overlong or unterminated prompt line; `prompt` null) | SHIM-WITNESSED | +| `seal` | `{ algorithm: "sha256", hex }` | integrity, not truth | + +Deliberate exclusions: no plaintext prompt or reply (hashes only), no +floating-point fields anywhere in the sealed body (integers and strings only +-- this is what makes the cross-language seal trivially stable), no +invariant/oracle/verdict vocabulary. + +`model.endpoint`, `model.request_body_sha256`, and `model.daemon_digest` are +OMITTED (not `null`) on an echo receipt: only `model.name` is present. This +differs from `prompt`/`reply`, which are always present as either an object or +an explicit JSON `null`. + +## The seal and the cross-language canonicalization contract + +Same idiom as the scientific receipt's `seal_receipt` / +`recompute_seal_hex` (`scientific_runtime.rs`): sha256 over the canonical +bytes of the receipt with `seal.hex` set to `""` and `seal.algorithm` fixed to +`"sha256"`. Because the emitter is Python (the shim) and the verifier is Rust +(buildc), the canonical form is pinned exactly, not assumed: + +- UTF-8, compact separators (no whitespace): `serde_json::to_vec` on the + Rust side; `json.dumps(obj, separators=(",", ":"))` on the Python side. +- Object keys in the FIXED schema order above. On the Rust side this falls + out of the struct's field declaration order for free. On the Python side it + requires building the dict with keys inserted in that exact order (Python + dicts preserve insertion order; `json.dumps` does not re-sort unless asked + to). +- Non-ASCII unescaped: `ensure_ascii=False` on the Python side, matching + `serde_json`'s default. +- No floats anywhere in the schema, which sidesteps float-formatting + divergence between the two serializers entirely. + +The contract is enforced by a GOLDEN FIXTURE: one byte-exact receipt with its +known seal, committed in BOTH repos +(`compiler/tests/fixtures/model-receipt-golden.json` here; the same file, +same bytes, same seal, in local-model's `tests/fixtures/`), with a test in +each repo that recomputes the seal from the fixture and asserts it against the +pinned hex. The fixture is an echo-mode `COMPLETED` receipt: prompt `"ping"` +(sha256 `758d61f2...9411fe931`), reply `"echo: ping"` (sha256 +`de2406a7...abe5afae`), pinned seal +`6bb2a09c47f5eaa2e3208a5eadcd6d57d1faffa74a567e024e920571c3794035`. If the +fixture tests ever disagree between the two repos, the cross-language contract +is broken and both sides know before any live artifact does. + +## Verifying a receipt (`buildc receipt verify`) + +`receipt verify` dispatches on the receipt's flat `/schema`, the same +lookup that already routes GPU cross-check, scientific-runtime, and +check-receipts. A model receipt is the fourth arm, implemented in +`compiler/src/model_receipt.rs` and wired into both the plain and `--json` +verify paths. It is **offline only**: there is no re-run, because the +artifact witnesses a PAST boundary crossing, not a re-derivable one. + +Checks, in order: + +1. **Structural.** The document deserializes into the typed schema + (`MALFORMED` otherwise; a missing/unrecognized `/schema` is caught by the + load-stage dispatch before this arm is reached, `SCHEMA_UNSUPPORTED`). +2. **Seal integrity** (`SEAL_MISMATCH`), recomputed BEFORE any sealed field is + interpreted -- the same ordering discipline the scientific verifier uses, + so every field-level rejection below is known to concern a genuinely + author-sealed value, not an unsealed hand-edit. +3. **Digest well-formedness** (`DIGEST_MALFORMED`): `prompt.sha256`, + `reply.sha256` (when present), `model.request_body_sha256` (when present), + and `model.daemon_digest.hex` (when present) must each be 64 hex chars. An + absent or malformed hash cannot masquerade as witnessed provenance. +4. **Status coherence** (`FIELD_CONTRACT_VIOLATION`), exactly three cases: + `model.daemon_digest.hex` present alongside status `"UNAVAILABLE"`; outcome + `"COMPLETED"` with a `null` `reply`; outcome `"PROTOCOL_VIOLATION"` with a + present (non-null) `prompt`. + +Deliberately **no new failure classes** for v1: the shared taxonomy with the +scientific verifier is a feature, not a gap. A reader of any buildc refusal +already knows these words. + +What it cannot check, and says so in its human output line: anything about +the model itself. There is no re-run, so no claim about model quality, +weights, or determinism rides on a `VERIFIED` result. + +`--prompt ` re-hashing (a SHOULD-level extra the design names, for +re-checking a held prompt against `prompt.sha256` and, for echo mode, +re-deriving the expected reply hash from the spec) is **not implemented in +v1**; the design marks it optional and not required for v1 acceptance. + +## Chain integration + +`receipt chain build`'s member-schema gate +(`compiler/src/main.rs::cmd_receipt_chain_build`) is an allowlist of two +schemas: `buildlang-scientific-runtime-receipt/v0` and +`buildlang-model-boundary-receipt/v0`. Nothing else about chain build or +chain verify changed: `source` extraction already reads a top-level `source` +field present on both schemas, chain seal computation only ever touches +`(index, receipt_seal)` pairs, and `receipt chain verify`'s member +re-verification shells out to `buildc receipt verify `, which is +exactly the arm this document describes. + +This makes the propose/dispose demo a single chain: a model receipt (the +proposal crossing) as one member, a Model-FREE disposer kernel's +scientific-runtime receipt (checking the proposed value) as the other, +bound in order. `CAPABILITY_INADMISSIBLE` never fires in this demo, because +the disposer kernel does not observe `Model` -- the propose/dispose rule is +demonstrated by what each chain member IS, not bent to fit. Tampering the +model member (without re-sealing) breaks the chain at re-verification with +`CHAIN_LINK_UNVERIFIED`, exactly like a tampered scientific member would. + +Honest limit: the chain proves co-presence and order, not data flow. That the +disposer consumed the proposer's output is a hash equality a reader can check +by hand across the two sealed artifacts (the model receipt's `reply.sha256` +against the disposer's witnessed input); the chain machinery has no +cross-member field-relation check in v1. + +## Not a corpus member + +`examples/scientific-corpus.json` and the `29/29` corpus count +(`buildc receipt corpus`) are about scientific-runtime receipts emitted from +`.bld` kernels. A model receipt has no invariant to classify PASS or +FAIL_EXPECTED against and is emitted by a different program entirely (the +shim, not buildc), so it is not corpus-shaped -- this is by construction, not +an oversight, and the corpus count is unchanged by this schema landing. The +`10/10` `--self-test` count is likewise scientific-runtime-only (its tamper +table is built from `ScientificRuntimeReceipt`); the model arm's tamper +coverage lives in `compiler/src/model_receipt.rs`'s unit tests (seal mismatch, +each named `FIELD_CONTRACT_VIOLATION` case, `DIGEST_MALFORMED`, `MALFORMED`, +and the golden-fixture reseal pin) and `compiler/tests/cli.rs`'s CLI-level +tests (the same tamper shapes through the real `buildc` binary, plus the +propose/dispose chain and its tampered-member break). diff --git a/docs/SCIENTIFIC-RECEIPT.md b/docs/SCIENTIFIC-RECEIPT.md index 75ea8f0..9a221d7 100644 --- a/docs/SCIENTIFIC-RECEIPT.md +++ b/docs/SCIENTIFIC-RECEIPT.md @@ -223,6 +223,44 @@ The receipt is a single JSON object. Its layers, outermost meaning first: practice, since no receipt over a Model-observing program can exist to carry those fields. There is no corpus member and no `--self-test` case for `Model`: the refusal happens before a receipt can exist, so there is nothing for either to exercise. + **The refusal is unchanged and un-weakened by the paragraph below.** A model + boundary crossing still cannot become scientific evidence; it becomes a + DIFFERENT, separately-schemed artifact instead. + +### Model boundary receipts (`buildlang-model-boundary-receipt/v0`) + +A model receipt is a PROVENANCE artifact about a `Model`-capability boundary +crossing: harness-side, emitted by `harness/model_shim.py` (the local-model +repo), never by buildc. It carries no invariant, no oracle, and no verdict, so +it cannot masquerade as a scientific-runtime receipt, and the reverse is +enforced structurally too: `receipt chain build`'s allowlist accepts exactly +`buildlang-scientific-runtime-receipt/v0` and +`buildlang-model-boundary-receipt/v0`, nothing else. Full schema, field-tag +table (SHIM-WITNESSED vs. DECLARED), and the verify arm's failure classes are +documented in [MODEL-RECEIPT.md](MODEL-RECEIPT.md). Two consequences worth +stating here, beside the scientific schema they sit next to: + +- `buildc receipt verify` dispatches a model receipt to its own arm (offline + only: seal recompute, digest well-formedness, field-shape contracts -- + there is no re-run, because the artifact witnesses a PAST crossing, not a + re-derivable one). It shares the same `failure_class` taxonomy as the + scientific verifier (`SEAL_MISMATCH`, `DIGEST_MALFORMED`, + `FIELD_CONTRACT_VIOLATION`, `MALFORMED`, `SCHEMA_UNSUPPORTED`) -- no new + classes for v1. +- `receipt chain build` accepts a model receipt as a chain member beside + scientific-runtime receipts (the propose/dispose demo: a model receipt as + the proposer link, a Model-FREE disposer kernel's scientific receipt as the + checker link). `receipt chain verify` needed zero changes: pinned seals and + subprocess re-verification (`buildc receipt verify `) already + compose across schemas. +- The model receipt is **not** a corpus member: `examples/scientific-corpus.json` + and the `29/29` corpus count are about scientific-runtime receipts over + `.bld` kernels only. A model receipt has no invariant to classify PASS or + FAIL_EXPECTED against, so it is not corpus-shaped, by construction -- not an + oversight. The `10/10` self-test count is likewise scientific-runtime-only + (`--self-test` builds its tamper table from `ScientificRuntimeReceipt`); the + model arm's own tamper coverage lives in `compiler/src/model_receipt.rs`'s + unit tests and `compiler/tests/cli.rs`'s CLI-level tests instead. - `numerical_method`: `{ description?, status }`, author-DECLARED via `--method` (buildc cannot derive scheme semantics from source and does not pretend to); an inconsistent status/description pair is rejected (`FIELD_CONTRACT_VIOLATION`). diff --git a/docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md b/docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md new file mode 100644 index 0000000..1a742eb --- /dev/null +++ b/docs/superpowers/specs/2026-07-29-model-boundary-receipts-design.md @@ -0,0 +1,296 @@ +# Model boundary receipts v1 (design) + +Status: DRAFT for review. Design only: no implementation, no plan tasks. +Register: internal (.superpowers/sdd). Date: 2026-07-29. +Scope: v1 of the boundary receipt the five-modes brief promised for the Model +capability ("receipted like any other boundary crossing: model digest, prompt +hash, parameters, seed"), designed so the propose/dispose rule is never +weakened: the scientific-receipt path keeps refusing Model-observing programs +(CAPABILITY_INADMISSIBLE), and a model receipt is a DIFFERENT artifact kind +that cannot masquerade as scientific evidence. + +Ground truth read for this design (all verified in-tree, high confidence): + +- Slice 4 plan: docs/superpowers/plans/2026-07-28-model-capability.md (honest + scope, line 9: v0 ships NO model receipts; they belong harness-side). +- Shipped emit refusal: compiler/src/main.rs:7799; shipped verify refusal: + compiler/src/scientific_runtime.rs:2291-2293 (CAPABILITY_INADMISSIBLE on the + RE-DERIVED capability union). +- The runtime client: build_model_complete in compiler/src/codegen/runtime.rs + (one prompt line out, read to CLOSE, trim one trailing \n and a preceding \r). +- Seal idiom: seal_receipt / recompute_seal_hex, scientific_runtime.rs:1319-1335 + (sha256 over canonical bytes with seal.hex blanked, algorithm fixed). +- Chain machinery: ReceiptChainLink / receipt_chain_seal_hex / build_receipt_chain, + scientific_runtime.rs:1579-1648; cmd_receipt_chain_build main.rs:1874-1933; + cmd_receipt_chain_verify main.rs:1939-2018. +- Verifier schema dispatch: cmd_receipt_verify main.rs:2656-2701 (three artifact + kinds already dispatch: gpu at 2679, scientific-runtime at 2695, check at 2698). +- The shim: local-model branch feat/model-shim, commit fefecd0c, + harness/model_shim.py + tests/test_model_shim.py (echo + ollama modes; the + ollama path is UNTESTED-LIVE, hardware gated; fail-closed writes nothing). + +## 0. Problem and non-goals + +Slice 4 deliberately shipped a model call with no record of what was asked, +what came back, or what served it. This design adds that record WITHOUT +touching the admission rule. Non-goals for v1: no quality or correctness +claims about completions; no in-language changes (no new builtins, no receipt +fields on the scientific side); no live-model verification (hardware gated); +no plaintext capture by default. + +The thesis sentence, up front: a model receipt is a PROVENANCE artifact about +a boundary crossing. It carries no invariant, no oracle, no verdict, and no +field that could be mistaken for one, by construction. Models propose; this +artifact witnesses THAT they proposed and WHAT bytes crossed, nothing more. + +## 1. Decision: the shim emits the receipt + +**Chosen: (a) the shim emits.** One receipt per connection, written as a JSON +artifact when (and only when) the shim is started with a new `--receipt-dir` +flag. No flag, no receipt, byte-identical behavior to today. + +Why the shim: it is the only party that observes all three fact families at +once: the prompt bytes as received, the reply bytes as written, and its own +adapter identity (mode, endpoint, model name, what the daemon declared). The +compiled program's runtime cannot emit this artifact: it is candidate-side and +untrusted by thesis (a receipt about the proposer written by the proposer is +not evidence). buildc at `run` time sees neither prompt nor reply: the TCP +session is program-to-shim. + +**Killed: (b) a buildc `model-proxy` mode.** It would put live model traffic +inside the compiler, which the slice 4 plan explicitly placed on the harness +side of the seam ("the model adapter... lives on the harness side of this +seam, never in the compiler"). Worse, it buys no trust: a proxy witnesses +transport bytes one hop earlier than the shim does, but still cannot witness +adapter identity (the model name and daemon digest live behind the shim's +HTTP hop), and both processes are operator-run on the same host, so there is +no trust gradient in which buildc's word outranks the shim's. Scope growth +with no added claim. + +**Killed for v1: (c) both, layered.** Two emitters of the same facts is double +schema surface for zero additional claim while shim and buildc share a trust +domain. Revisit only if a real trust gradient appears (for example the shim +running on remote hardware while buildc runs locally); the schema below does +not preclude a second, independently sealed witness later. + +Trust framing, stated in the artifact's own vocabulary: every field is tagged +either SHIM-WITNESSED (the shim observed the bytes or performed the act +itself) or DECLARED (someone's say-so passed through: the operator's model +name argument, the ollama daemon's self-reported digest, the shim host's wall +clock). The seal makes tampering evident; it does not upgrade a declaration +into a witness. + +## 2. The artifact + +Schema tag: `buildlang-model-boundary-receipt/v0` (flat top-level `schema` +string plus top-level `seal`, mirroring the scientific receipt's shape so the +existing chain pointers `/schema` and `/seal/hex` read it unchanged). + +Filename: `model-receipt--.json` in `--receipt-dir` +(nonce: 8 hex chars of urandom, collision guard only, not a claim). + +Fields, in canonical (sealed) order: + +| field | content | epistemic tag | +|---|---|---| +| `schema` | the tag above | structural | +| `source` | `model::` (e.g. `model:echo:echo/v1`, `model:ollama:llama3.2`) | DECLARED label; exists so ReceiptChainLink.source (scientific_runtime.rs:1592) carries a human-readable member label with zero chain-code change | +| `shim` | `{ name: "model_shim.py", version: , mode: "echo"\|"ollama" }` | SHIM-WITNESSED (self-identity) | +| `session` | `{ listen: "host:port", nonce, request_received_utc, reply_written_utc\|null }` | timestamps SHIM-CLOCK-DECLARED (ordering witnessed, wall accuracy is the host's) | +| `prompt` | `{ sha256, bytes }` over the RAW prompt-line bytes as received, after stripping the single trailing `\n` and one preceding `\r`, BEFORE utf-8 decode | SHIM-WITNESSED. Raw bytes, not the decoded string: `_read_prompt_line` decodes with errors="replace", which is lossy; the boundary fact is bytes | +| `reply` | `{ sha256, bytes }` over the sanitized completion bytes exactly as written, EXCLUDING the protocol-terminator `\n` | SHIM-WITNESSED. This equals sha256 of the string the program observed (the client trims exactly that terminator), which is what makes downstream binding possible (section 6) | +| `model` | echo: `{ name: "echo/v1" }`. ollama: `{ name: , endpoint: , request_body_sha256, daemon_digest: { status: "FETCHED"\|"UNAVAILABLE", hex? } }` | name is DECLARED (a string is not a digest); request_body_sha256 is SHIM-WITNESSED over the exact JSON POSTed to /api/generate, and is the parameters witness by construction (model, prompt, stream flag, and any future options all live inside that body); daemon_digest is DAEMON-DECLARED even when FETCHED (section 3) | +| `seed` | `{ status: "NOT_SENT" }` in v1 (the shim sends no options.seed); when a --seed flag lands: `{ status: "SENT", value: }`, and the value also rides inside request_body | SHIM-WITNESSED as to what was SENT; never a claim the daemon honored it | +| `outcome` | `"COMPLETED"` \| `"FAILED_CLOSED"` (adapter failure, nothing written; reply is null) \| `"PROTOCOL_VIOLATION"` (overlong or unterminated prompt line; prompt is null) | SHIM-WITNESSED. Refusals get receipts too: the fail-closed path is a boundary fact worth witnessing | +| `seal` | `{ algorithm: "sha256", hex }` | integrity, not truth | + +Deliberate exclusions: NO plaintext prompt or reply (hashes only; the receipt +is shareable, and whoever holds the plaintext can re-hash to check it), NO +floating-point fields anywhere in the sealed body (integers and strings only; +durations if ever added are integer milliseconds), NO invariant/oracle/verdict +vocabulary. The no-floats rule is what makes the cross-language seal below +trivially stable. + +**Seal and the cross-language canonicalization contract.** Same idiom as +seal_receipt (scientific_runtime.rs:1319): sha256 over the canonical bytes of +the receipt with `seal.hex` set to `""` and `seal.algorithm` fixed to +`"sha256"`. Because the emitter is Python and the verifier is Rust, the +canonical form must be pinned, not assumed: UTF-8, compact separators (no +whitespace), object keys in the FIXED schema order above (matching the Rust +struct's serde field order; serde_json::to_vec preserves it), non-ASCII +unescaped (Python: `ensure_ascii=False`, matching serde_json), no floats. The +contract is enforced by a GOLDEN FIXTURE: one byte-exact receipt with its +known seal committed in BOTH repos, with a test in each repo that recomputes +the seal from the fixture bytes. If the fixture tests disagree, the contract +is broken and both sides know before any artifact does. + +## 3. What the receipt claims and refuses + +Claims (all offline-checkable): these exact bytes crossed the boundary, in +this session, in this order, under this shim mode, and this is what the +adapter's daemon declared about itself at the time. Nothing else. + +Refuses, explicitly, in the doc and in the schema's absence of fields: + +- Quality or correctness of the completion. No field exists to carry it. +- That `model.name` corresponds to any particular weights. An ollama model + name is a string the operator typed, tagged DECLARED. +- That `daemon_digest.hex` corresponds to the weights actually consulted. The + adapter CAN fetch a real digest: spec is `GET /api/tags`, match + the entry whose name equals `model.name`, take its `digest` field (exact + JSON shape: moderate confidence, from memory; pin it during the gated live + session, which the ollama path needs anyway as UNTESTED-LIVE). But even + when FETCHED, the digest is the DAEMON'S declaration about itself; the shim + witnesses the fetch, not the weights. Status UNAVAILABLE keeps the receipt + valid and honest: the model block is then fully DECLARED and says so. A + `hex` present alongside status UNAVAILABLE is a field-contract violation. +- Determinism. Not claimed even for echo mode in the sealed fields; echo's + reply is re-derivable ("echo: " + prompt) and the verify arm MAY offer that + re-check when handed the prompt (section 5), but re-derivability is a + property of the spec, not a sealed claim. +- That the reply derived from the prompt at all. The shim observed a request + and a response on one connection; causality inside the daemon is not + witnessed and never stated. + +## 4. Wire contract v1.1: the wire does not change + +The shipped client (build_model_complete) writes the prompt line and then +reads to CONNECTION CLOSE, trimming one trailing `\n` (and a `\r` before it). +Every byte the shim writes lands in the program's returned string. Therefore +ANY in-band addition (a header line before the completion, a trailer after +it, a length prefix) is not a compatible extension: it does not break the +transport, it silently corrupts the completion every v1 client returns. The +line protocol also has no channel in which a client could negotiate ("I +understand headers"), so in-band versioning is unreachable from here. + +Consequence, stated precisely: model identity travels OUT-OF-BAND, into the +receipt only. Wire v1.1 is byte-identical to wire v1; the ".1" names the SHIM +CONTRACT, not the wire grammar: a v1.1 shim additionally emits one boundary +receipt per connection when started with `--receipt-dir`. v1 clients (the +shipped runtime, the cli.rs TCP-listener test) are untouched and cannot +observe the difference. If a future protocol truly needs in-band metadata, it +is a v2 wire with a new builtin or an explicit env-var opt-in on the client +side; out of scope here and probably never needed, because the receipt is the +metadata channel. + +## 5. The `receipt verify` model arm (buildlang side) + +cmd_receipt_verify already dispatches over artifact kinds: gpu cross-check +receipts route at main.rs:2679 (verified as pure JSON + SHA-256, no Vulkan, +which is the exact precedent: buildc verifying an artifact it did not emit, +offline), scientific-runtime at 2695, check receipts at 2698. The model +receipt becomes the fourth arm on the same flat `/schema` lookup: a typed +struct in a new module (or a sibling section of scientific_runtime.rs), +recompute-seal in the reseal idiom, then field contracts. Both the plain and +`--json` paths get the arm (they share the dispatch shape; chain verify uses +the plain path). + +What offline verification of a model receipt CHECKS: seal integrity +(SEAL_MISMATCH), schema and structure (MALFORMED / SCHEMA_UNSUPPORTED at the +load stage via receipt_load_failure, main.rs:2797, which already fires before +schema dispatch), digest well-formedness (DIGEST_MALFORMED: 64 hex chars, the +existing rule that an absent hash cannot masquerade as witnessed provenance), +and status coherence (FIELD_CONTRACT_VIOLATION: daemon_digest hex present +with UNAVAILABLE; a COMPLETED outcome with a null reply; a PROTOCOL_VIOLATION +with a present prompt). Deliberately NO new failure classes in v1: the shared +taxonomy is a feature; a reader of any buildc refusal already knows these +words. + +What it cannot check, and says so in its output line: anything about the +model (there is no re-run; the artifact witnesses a past crossing). One +SHOULD-level extra: `receipt verify --prompt ` re-hashes the given +bytes against `prompt.sha256`, and for echo mode additionally re-derives the +expected reply hash from the spec. Cheap, offline, and it makes the golden +fixture self-demonstrating. Not required for v1 acceptance. + +The scientific verifier is UNTOUCHED. CAPABILITY_INADMISSIBLE +(scientific_runtime.rs:2293) keeps firing on any scientific receipt whose +re-derived capabilities include Model. The two artifact kinds share a seal +idiom and a verifier binary, never a claim vocabulary. + +## 6. Chain integration and the propose/dispose demo + +The precise code answer first: **the shipped chain machinery does NOT bind +both artifact kinds as-is.** `cmd_receipt_chain_build` refuses any member +whose flat `schema` is not SCIENTIFIC_RUNTIME_SCHEMA (main.rs:1886-1893), so +a model receipt cannot become a link today. The verify side, however, is +already agnostic: the chain seal binds only (index, member seal) pairs +(receipt_chain_seal_hex, scientific_runtime.rs:1614-1624), seal pinning reads +the schema-agnostic pointer `/seal/hex` (main.rs:1978-1981), and member +re-verification shells out to `buildc receipt verify ` +(main.rs:1989-1991), which is exactly the schema dispatch section 5 extends. + +So the chain extension is two small, separable edits: + +1. Chain build: widen the main.rs:1886 gate from a single-schema equality to + an allowlist { scientific-runtime/v0, model-boundary-receipt/v0 }. The + `source` extraction at main.rs:1902 needs no change: the model receipt + carries a top-level `source` label precisely so this line keeps working. +2. Receipt verify: the model arm (section 5). Chain verify then works with + ZERO changes: pinned seals and subprocess re-verification compose. + +Member-kind substitution is already caught: the member's `schema` sits inside +its own sealed body, so swapping artifact kinds under a pinned seal is +CHAIN_LINK_TAMPERED, and re-sealing changes the seal, which is +CHAIN_SEAL_MISMATCH. + +**The demo's final shape.** Three artifacts: the shim's model receipt (the +proposal crossing), a scientific receipt over a Model-FREE disposer kernel +that checks the proposed value (so CAPABILITY_INADMISSIBLE never fires; the +rule is demonstrated by what each member IS, not bent), and a chain manifest +binding the two in order (proposer link 0, disposer link 1; the two-member +minimum at main.rs:1875/1946 is exactly met). `receipt chain verify` then +re-checks order, membership, both seals, and both members through one +verifier. That is the propose/dispose thesis as a single command. + +Honest limit, stated in the demo doc and here: the chain proves co-presence +and order, NOT data flow. The fact that the disposer consumed the proposer's +output is carried by hash equality a reader can check across the two sealed +artifacts (the model receipt's `reply.sha256` against the disposer run's +witnessed input provenance), because `reply.sha256` was defined in section 2 +to hash exactly the string the program observed. Automating that equality as +an optional cross-member binding check is a chain v1.1 candidate, not v1: the +chain machinery has no cross-member field relations today, and adding one is +a schema change to the manifest, not a widening. + +## 7. Cross-repo split + +| lands in | what | why there | +|---|---|---| +| local-model (follow-on to feat/model-shim) | `--receipt-dir` emission in harness/model_shim.py; receipt construction + Python-side seal; tests in tests/test_model_shim.py (echo receipts end-to-end over a real socket, fail-closed receipt cases, seal recompute); the golden fixture + its test | the emitter is the shim and the shim lives there; its tests already mock urllib at the network boundary | +| buildlang | docs contract of record (a Model-receipt section: SCIENTIFIC-RECEIPT.md grows a pointer paragraph, the schema itself gets docs/MODEL-RECEIPT.md, continuing the pattern where the shim commit cited SCIENTIFIC-RECEIPT.md as its contract source); the `receipt verify` model arm + typed schema; the chain-build allowlist widening; the golden fixture + tamper-table tests (SEAL_MISMATCH, DIGEST_MALFORMED, FIELD_CONTRACT_VIOLATION, and the chain cases: model member pre-widening refused, post-widening chained, tampered model member fails CHAIN_LINK_TAMPERED) | one verifier for every artifact kind is the established shape (the gpu arm proves it); chain verify REQUIRES the arm because it subprocesses `receipt verify`; and the demo's audience runs one binary | + +Sequencing note: buildlang's docs/MODEL-RECEIPT.md is the contract; the shim +implements it; the fixture pins both. Either implementation slice can land +first behind its flag, but the fixture must be identical bytes in both repos +before either claims done. + +## 8. Honest scope: what v1 does not claim + +- Everything in v1 is offline-verifiable: echo-mode receipts over a real + local socket, golden fixtures, tamper tables, chain build/verify with the + widened gate. No live network calls in any test, matching the shim commit's + own discipline. +- The ollama path stays UNTESTED-LIVE until the hardware-gated session runs; + the daemon_digest fetch spec (the /api/tags shape) is pinned in that same + session. Until then the ollama receipt path is unit-tested with urllib + mocked, exactly like the completion path already is. +- The live propose/dispose demo (real model proposing, buildc-verified kernel + disposing) is gated on the same hardware and says so wherever it is + mentioned. The chain demo is buildable TODAY with an echo-mode receipt, and + that is the v1 acceptance demo: the epistemics are identical, only the + proposer is boring. +- No public-surface copy changes in this design; register stays internal + until the feature ships and earns its user-facing paragraph. + +## 9. Open questions for review + +1. Module placement of the verify arm: a new compiler/src/model_receipt.rs + (mirroring gpu_receipt's separation) vs a section in scientific_runtime.rs. + Leaning new module: the point of the artifact is that it is NOT scientific. +2. Should FAILED_CLOSED receipts be on by default once --receipt-dir is set, + or behind a second flag? Leaning on by default: a refusal is a boundary + fact, and silent refusal receipts cost nothing. +3. Does the demo's disposer kernel read the proposed value from stdin or from + a file? Whichever the existing corpus idiom prefers; it only affects how + the reply-hash equality is presented, not the schema.