From 935cada482063bdde87ca4f5b1828f11b2618562 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 18:50:11 +0200 Subject: [PATCH 1/5] =?UTF-8?q?#3605:=20removed=5Fby=20gets=20a=20shape=20?= =?UTF-8?q?=E2=80=94=20refusal-receipt-v1,=20with=20a=20closed=20sentinel?= =?UTF-8?q?=20set=20so=20the=20required=20field=20manufactures=20nothing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `removed_by` had 0 occurrences tree-wide, no schema and no validator. Every refusal #3597 writes would have minted an unenforced convention, and a tree full of consistent-looking `removed_by:` lines reads as validated when it is decoration. PHASE 0 — ITS OWN CONTRACT, AND NOT BECAUSE IT IS EASIER TO WRITE Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD. It is in unmerged #3600, and there it is deliberately the RETIRED layout with no shape and no instances. A live validated field on a superseded contract with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree has now used twice — an artifact family is named by its REQUIRED KEYS, never by its filename — a parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a refusal requires a verb, a reason, an exit code and removed_by. They share no required key. A THIRD option was considered and refused, and it is the more attractive one: put removed_by on apr-cli-commands-v1.yaml, where the verb already IS the focus node and the universe is already the trustworthy 111. Refused because the registry is the UNIVERSE and #3597's method is to DIFF the registry against the buckets. If the buckets live in the registry, the denominator and the numerator are the same artifact and the diff is vacuous by construction. The registry says what EXISTS; a refusal says what was TRIED. Keeping them apart is what lets that diff be a real diff. THE FORCED-BINDING TRAP, AND WHY minCount 1 IS SAFE HERE A required field with no escape manufactures false data: `pv validate` requires kani_harnesses so authors fabricate one, and apex#57 had lean_theorem copied verbatim into twelve contracts resolving to nothing, gate green throughout. The escape is a closed sentinel set, so "there is legitimately nothing here" is SAYABLE and still CHECKABLE: v. the release that removes it never refused permanently by design unscheduled a defect with no release chosen tbd, soon, n/a, pending, a bare `0.70`, a patch-level `v0.70.1` and a git sha are all RED. A version rather than a sha because a refusal answers "which release do I need?" and a sha is precise about the tree and silent about the boundary; the sha form is made INVALID rather than discouraged, because a shape that permits two spellings gets both. BOTH ARMS, and the second is the point: 9 cases over 8 fixtures. refusal-ok carries all three declared forms and passes with 3 focus nodes; refusal-undeclared-sentinel plants the PLAUSIBLE `tbd` and must go red. Mutation proved red-capable: widening the pattern to accept tbd fails exactly a_plausible_but_undeclared_sentinel_is_refused and accept_and_refuse_are_distinct_answers, and restoring makes 9/9 green. Fixtures carry the real contract byte for byte, so widening it without them is caught too. No new extractor: entity {type: json, ref} + vocabulary is the existing machinery for "validate this document", and a second reader for one more family is the thing this tree keeps filing against. done_when 6 — the interim re-check list is EMPTY: `removed_by` still has 0 occurrences at HEAD, so no refusal written under the interim needs revisiting. The ledger is seeded with the one refusal already measured (`apr bench` refuses qwen35) so the shape has a real focus node instead of passing vacuously over an empty list. WHICH verbs land there is #3597's bucket, not this row's. Refs #3605, #3597, #3600, #3080 Pmat-Ticket: PMAT-3605 Co-Authored-By: Claude Opus 5 (1M context) --- ...nder-contracts-cli-ont-refusal-receipt.cmd | 1 + contracts/census.json | 11 +- contracts/contracts.nt | 20 ++ contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ contracts/shapes.ttl | 30 +++ .../tests/ont_refusal_receipt.rs | 189 ++++++++++++++++++ evidence/verbs/refusals.json | 12 ++ .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../evidence/verbs/refusals.json | 11 + .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../evidence/verbs/refusals.json | 10 + .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../evidence/verbs/refusals.json | 10 + .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../refusal-ok/evidence/verbs/refusals.json | 23 +++ .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../evidence/verbs/refusals.json | 11 + .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../refusal-sha/evidence/verbs/refusals.json | 11 + .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../evidence/verbs/refusals.json | 11 + .../contracts/refusal-receipt-v1.yaml | 173 ++++++++++++++++ .../evidence/verbs/refusals.json | 11 + 23 files changed, 1913 insertions(+), 5 deletions(-) create mode 100644 ci/explicit-test-commands.d/430-aprender-contracts-cli-ont-refusal-receipt.cmd create mode 100644 contracts/refusal-receipt-v1.yaml create mode 100644 crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs create mode 100644 evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-bare-version/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-bare-version/evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-missing/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-missing/evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-no-exit-code/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-no-exit-code/evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-ok/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-ok/evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-patch-version/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-patch-version/evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-sha/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-sha/evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-terse-reason/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-terse-reason/evidence/verbs/refusals.json create mode 100644 tests/fixtures/ont/refusal-undeclared-sentinel/contracts/refusal-receipt-v1.yaml create mode 100644 tests/fixtures/ont/refusal-undeclared-sentinel/evidence/verbs/refusals.json diff --git a/ci/explicit-test-commands.d/430-aprender-contracts-cli-ont-refusal-receipt.cmd b/ci/explicit-test-commands.d/430-aprender-contracts-cli-ont-refusal-receipt.cmd new file mode 100644 index 0000000000..ab720e9323 --- /dev/null +++ b/ci/explicit-test-commands.d/430-aprender-contracts-cli-ont-refusal-receipt.cmd @@ -0,0 +1 @@ +cargo test -p aprender-contracts-cli --test ont_refusal_receipt diff --git a/contracts/census.json b/contracts/census.json index 3009dd4060..08e83cc72c 100644 --- a/contracts/census.json +++ b/contracts/census.json @@ -1,8 +1,8 @@ { "schema": "ont.paiml.dev/census/v1alpha1", "git_sha": null, - "n_files": 1799, - "n_parsed": 1799, + "n_files": 1800, + "n_parsed": 1800, "n_parse_errors": 0, "parse_errors": [], "quarantined_n": 0, @@ -12,7 +12,7 @@ "kernel": 362, "model-family": 28, "model-family-variant": 1, - "pattern": 86, + "pattern": 87, "pretraining-corpus": 2, "registry": 519, "schema": 766, @@ -22,14 +22,15 @@ }, "by_entity_type": { "gguf": 2, + "json": 1, "pv-contract": 1 }, "by_anchoring": { "unanchored": 1796, "class": 2, - "instance": 1 + "instance": 2 }, - "id_set_sha256": "a547cd5527caeffade2d8260d25421f26506df1c1d8f00f5eb7b9cde12e8107e", + "id_set_sha256": "f05f6dc17ca050bf5bb082afc5af7012f978d64b826d82192f40da5ed064cf3f", "declared_external": [ { "name": "provable-contracts", diff --git a/contracts/contracts.nt b/contracts/contracts.nt index 16022a5f13..7cc63d0876 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -8772,6 +8772,16 @@ "reduce-lr-plateau-v1"^^ . "reduce-lr-plateau-patience-strictly-greater"^^ . "1.0.0"^^ . + . + . + "evidence/verbs/refusals.json"^^ . + "json"^^ . + "contracts/refusal-receipt-v1.yaml"^^ . + "refusal-receipt-v1"^^ . + "pattern"^^ . + "refusal-receipt"^^ . + "active"^^ . + "1.0.0"^^ . . . "contracts/pacha/registry-integrity-v1.yaml"^^ . @@ -9814,6 +9824,16 @@ . "03b74727a860a56338e042c4420bb3f04b2fec5734175f4cb9fa853daf52b7e8"^^ . "0.68.2"^^ . + . + . + "The refusal bucket of the verb-set audit (#3597). Every entry is shaped by contracts/refusal-receipt-v1.yaml: a verb from the 111-verb registry, one reason line, the exit code a caller sees, and the release that removes the refusal or a declared sentinel saying none will. #3597 owns WHICH verbs land here; this file is seeded with the one refusal already measured so the shape has a real focus node rather than passing vacuously over an empty list."^^ . + . + "apr-refusal-ledger/v1"^^ . + . + "8"^^ . + "apr bench refuses qwen35 outright: the subcommand routes through the dense QuantizedGGUFTransformer loader, which does not carry the Gated-DeltaNet hybrid, so the benchmark verb cannot measure the architecture the last release shipped."^^ . + "unscheduled"^^ . + "bench"^^ . . . "doc"^^ . diff --git a/contracts/refusal-receipt-v1.yaml b/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/contracts/shapes.ttl b/contracts/shapes.ttl index 06b73b15c7..6767e2da68 100644 --- a/contracts/shapes.ttl +++ b/contracts/shapes.ttl @@ -112,3 +112,33 @@ ] ; . + a sh:NodeShape ; + sh:targetClass ; + sh:closed true ; + sh:property [ + sh:path ; + sh:minCount 1 ; + sh:maxCount 1 ; + sh:datatype ; + ] ; + sh:property [ + sh:path ; + sh:minCount 1 ; + sh:maxCount 1 ; + sh:datatype ; + sh:minLength 12 ; + ] ; + sh:property [ + sh:path ; + sh:minCount 1 ; + sh:maxCount 1 ; + sh:datatype ; + ] ; + sh:property [ + sh:path ; + sh:minCount 1 ; + sh:maxCount 1 ; + sh:pattern "^(v[0-9]+\\.[0-9]+|never|unscheduled)$" ; + ] ; +. + diff --git a/crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs b/crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs new file mode 100644 index 0000000000..b58eb2d007 --- /dev/null +++ b/crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs @@ -0,0 +1,189 @@ +//! #3605 / PMAT-3605 — `removed_by` under contract, on the CLI. +//! +//! **Both arms, and the second one is the point.** A validator that only ever sees valid input is +//! indistinguishable from `exit 0`, so the table plants a **plausible but undeclared** sentinel +//! (`tbd`) and requires RED. Accepting `v0.70` proves nothing on its own. +//! +//! | fixture | `removed_by` | expected | +//! |---|---|---| +//! | `refusal-ok` | `v0.70`, `never`, `unscheduled` | **Pass** — the declared set, all three forms | +//! | `refusal-undeclared-sentinel` | `tbd` | Fail — the arm that matters | +//! | `refusal-sha` | `ddb5a15eb` | Fail — precise about the tree, silent about the boundary | +//! | `refusal-bare-version` | `0.70` | Fail — a shape that permits two spellings gets both | +//! | `refusal-patch-version` | `v0.70.1` | Fail — a patch is not a release boundary | +//! | `refusal-missing` | *(absent)* | Fail — every refusal answers for its own lifetime | +//! | `refusal-no-exit-code` | — | Fail — a refusal a caller cannot branch on | +//! | `refusal-terse-reason` | — | Fail — `reason: "broken"` names no defect | +//! +//! **Why `minCount 1` is safe here and manufactures nothing.** A required field with no escape +//! produces fabricated data — `pv validate` requires `kani_harnesses`, so authors invent one, and +//! apex#57 had `lean_theorem: Theorems.RowMerged` copied verbatim into twelve contracts, resolving +//! to nothing, gate green throughout. The escape is the closed sentinel set: `never` and +//! `unscheduled` let "there is legitimately nothing here" be SAID and still CHECKED. That is why +//! `refusal-ok` carries all three forms and `refusal-undeclared-sentinel` must be red — the escape +//! has to be open enough to be honest and closed enough to be a gate. + +use std::path::{Path, PathBuf}; +use std::process::Command; + +fn pv_bin() -> PathBuf { + PathBuf::from(env!("CARGO_BIN_EXE_pv")) +} + +fn repo_root() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).join("../..") +} + +fn fixture(name: &str) -> PathBuf { + repo_root().join("tests/fixtures/ont").join(name) +} + +struct Run { + code: i32, + stdout: String, + stderr: String, +} + +impl Run { + fn all(&self) -> String { + format!( + "exit {}\n--- stdout\n{}\n--- stderr\n{}", + self.code, self.stdout, self.stderr + ) + } +} + +fn shapes_on(name: &str) -> Run { + let contracts = fixture(name).join("contracts"); + let out = Command::new(pv_bin()) + .args([ + "lint", + contracts.to_str().expect("utf-8 path"), + "--gate", + "shapes", + "--format", + "json", + ]) + .output() + .expect("failed to spawn pv"); + Run { + code: out.status.code().unwrap_or(-1), + stdout: String::from_utf8_lossy(&out.stdout).into_owned(), + stderr: String::from_utf8_lossy(&out.stderr).into_owned(), + } +} + +/// Every fixture whose `removed_by` is outside the declared set must FAIL, and the report must name +/// the focus node — a red that does not say which entry is a red nobody can act on. +fn assert_refused(name: &str) { + let r = shapes_on(name); + assert_eq!(r.code, 1, "{name} was not refused\n{}", r.all()); + assert!( + r.stdout.contains("refusal-receipt-v1"), + "{name}: the report must name the shape that fired\n{}", + r.all() + ); +} + +#[test] +fn all_three_declared_forms_conform() { + // A release, and BOTH sentinels. If the escape did not work, a refusal with nothing to promise + // would have to invent a release — which is the defect this contract exists to prevent. + let r = shapes_on("refusal-ok"); + assert_eq!(r.code, 0, "{}", r.all()); + let v: serde_json::Value = serde_json::from_str(&r.stdout).expect("json report"); + assert_eq!(v["extra"]["violations"].as_u64(), Some(0), "{}", r.all()); + assert!( + v["extra"]["by_shape"] + .as_array() + .expect("by_shape") + .iter() + .any(|s| s.as_str() == Some("refusal-receipt-v1=3")), + "all three entries must be focus nodes\n{}", + r.all() + ); +} + +#[test] +fn a_plausible_but_undeclared_sentinel_is_refused() { + // THE ARM THAT MATTERS. `tbd` is exactly what someone writes when the field is required and + // they have nothing to say; if it passed, the closed set would be decoration. + assert_refused("refusal-undeclared-sentinel"); +} + +#[test] +fn a_sha_is_refused_because_it_answers_a_different_question() { + assert_refused("refusal-sha"); +} + +#[test] +fn a_shape_that_permits_two_spellings_would_get_both() { + assert_refused("refusal-bare-version"); + assert_refused("refusal-patch-version"); +} + +#[test] +fn a_refusal_that_says_nothing_about_its_lifetime_is_refused() { + assert_refused("refusal-missing"); +} + +#[test] +fn a_refusal_a_caller_cannot_branch_on_or_read_is_refused() { + assert_refused("refusal-no-exit-code"); + assert_refused("refusal-terse-reason"); +} + +#[test] +fn accept_and_refuse_are_distinct_answers() { + // A build that collapses them passes an all-invalid table and an all-valid one alike. + assert_eq!(shapes_on("refusal-ok").code, 0); + assert_eq!(shapes_on("refusal-undeclared-sentinel").code, 1); +} + +#[test] +fn every_fixture_carries_the_real_contract_byte_for_byte() { + // Without this, the shape could be widened in `contracts/` while the case table stayed green — + // the mutation control's blind spot. + let real = std::fs::read(repo_root().join("contracts/refusal-receipt-v1.yaml")) + .expect("the real contract is in the tree"); + for name in [ + "refusal-ok", + "refusal-undeclared-sentinel", + "refusal-sha", + "refusal-bare-version", + "refusal-patch-version", + "refusal-missing", + "refusal-no-exit-code", + "refusal-terse-reason", + ] { + let copy = std::fs::read(fixture(name).join("contracts/refusal-receipt-v1.yaml")) + .unwrap_or_else(|e| panic!("{name} carries the contract: {e}")); + assert_eq!( + copy, real, + "{name}'s copy of refusal-receipt-v1.yaml has drifted from contracts/" + ); + } +} + +#[test] +fn every_refusal_in_the_tree_names_a_verb_the_registry_carries() { + // The join the contract declares: the registry is the universe, and a refusal naming a verb + // `apr --help` does not expose is a dangling reference. Checked here rather than in the shape + // because the implemented subset cannot reach across documents. + let ledger: serde_json::Value = serde_json::from_str( + &std::fs::read_to_string(repo_root().join("evidence/verbs/refusals.json")) + .expect("the ledger is in the tree"), + ) + .expect("the ledger is JSON"); + let registry = std::fs::read_to_string(repo_root().join("contracts/apr-cli-commands-v1.yaml")) + .expect("the registry is in the tree"); + let refusals = ledger["refusals"].as_array().expect("refusals[]"); + assert!(!refusals.is_empty(), "an empty ledger passes vacuously"); + for r in refusals { + let verb = r["verb"].as_str().expect("verb is a string"); + assert!( + registry.contains(&format!("- name: {verb}\n")), + "refusal names verb {verb:?}, which contracts/apr-cli-commands-v1.yaml does not carry" + ); + } +} diff --git a/evidence/verbs/refusals.json b/evidence/verbs/refusals.json new file mode 100644 index 0000000000..08fa293054 --- /dev/null +++ b/evidence/verbs/refusals.json @@ -0,0 +1,12 @@ +{ + "schema": "apr-refusal-ledger/v1", + "note": "The refusal bucket of the verb-set audit (#3597). Every entry is shaped by contracts/refusal-receipt-v1.yaml: a verb from the 111-verb registry, one reason line, the exit code a caller sees, and the release that removes the refusal or a declared sentinel saying none will. #3597 owns WHICH verbs land here; this file is seeded with the one refusal already measured so the shape has a real focus node rather than passing vacuously over an empty list.", + "refusals": [ + { + "verb": "bench", + "reason": "apr bench refuses qwen35 outright: the subcommand routes through the dense QuantizedGGUFTransformer loader, which does not carry the Gated-DeltaNet hybrid, so the benchmark verb cannot measure the architecture the last release shipped.", + "exit_code": 8, + "removed_by": "unscheduled" + } + ] +} diff --git a/tests/fixtures/ont/refusal-bare-version/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-bare-version/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-bare-version/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-bare-version/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-bare-version/evidence/verbs/refusals.json new file mode 100644 index 0000000000..d57a0e751f --- /dev/null +++ b/tests/fixtures/ont/refusal-bare-version/evidence/verbs/refusals.json @@ -0,0 +1,11 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8, + "removed_by": "0.70" + } + ] +} diff --git a/tests/fixtures/ont/refusal-missing/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-missing/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-missing/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-missing/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-missing/evidence/verbs/refusals.json new file mode 100644 index 0000000000..e9cf5dfd25 --- /dev/null +++ b/tests/fixtures/ont/refusal-missing/evidence/verbs/refusals.json @@ -0,0 +1,10 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8 + } + ] +} diff --git a/tests/fixtures/ont/refusal-no-exit-code/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-no-exit-code/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-no-exit-code/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-no-exit-code/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-no-exit-code/evidence/verbs/refusals.json new file mode 100644 index 0000000000..1eccd7d2b7 --- /dev/null +++ b/tests/fixtures/ont/refusal-no-exit-code/evidence/verbs/refusals.json @@ -0,0 +1,10 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "the subcommand routes through the dense loader and cannot measure this", + "removed_by": "never" + } + ] +} diff --git a/tests/fixtures/ont/refusal-ok/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-ok/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-ok/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-ok/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-ok/evidence/verbs/refusals.json new file mode 100644 index 0000000000..c50219c187 --- /dev/null +++ b/tests/fixtures/ont/refusal-ok/evidence/verbs/refusals.json @@ -0,0 +1,23 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8, + "removed_by": "v0.70" + }, + { + "verb": "chat", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8, + "removed_by": "never" + }, + { + "verb": "code", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8, + "removed_by": "unscheduled" + } + ] +} diff --git a/tests/fixtures/ont/refusal-patch-version/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-patch-version/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-patch-version/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-patch-version/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-patch-version/evidence/verbs/refusals.json new file mode 100644 index 0000000000..c0c23a2bd3 --- /dev/null +++ b/tests/fixtures/ont/refusal-patch-version/evidence/verbs/refusals.json @@ -0,0 +1,11 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8, + "removed_by": "v0.70.1" + } + ] +} diff --git a/tests/fixtures/ont/refusal-sha/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-sha/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-sha/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-sha/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-sha/evidence/verbs/refusals.json new file mode 100644 index 0000000000..e13fa08788 --- /dev/null +++ b/tests/fixtures/ont/refusal-sha/evidence/verbs/refusals.json @@ -0,0 +1,11 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8, + "removed_by": "ddb5a15eb" + } + ] +} diff --git a/tests/fixtures/ont/refusal-terse-reason/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-terse-reason/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-terse-reason/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-terse-reason/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-terse-reason/evidence/verbs/refusals.json new file mode 100644 index 0000000000..275f196455 --- /dev/null +++ b/tests/fixtures/ont/refusal-terse-reason/evidence/verbs/refusals.json @@ -0,0 +1,11 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "broken", + "exit_code": 8, + "removed_by": "never" + } + ] +} diff --git a/tests/fixtures/ont/refusal-undeclared-sentinel/contracts/refusal-receipt-v1.yaml b/tests/fixtures/ont/refusal-undeclared-sentinel/contracts/refusal-receipt-v1.yaml new file mode 100644 index 0000000000..f0d98bc34c --- /dev/null +++ b/tests/fixtures/ont/refusal-undeclared-sentinel/contracts/refusal-receipt-v1.yaml @@ -0,0 +1,173 @@ +# ────────────────────────────────────────────── +# refusal-receipt-v1 — a refused verb, under contract (issue #3605, PMAT-3605; blocks #3597) +# +# THE DEFECT THIS CLOSES. `removed_by` had **0 occurrences tree-wide**, no schema and no validator. +# Every refusal #3597 writes would have minted an unenforced convention, and a tree full of +# consistent-looking `removed_by:` lines reads as validated when it is decoration — the +# `pv validate`-accepts-a-key-by-ignoring-it class. +# +# ── PHASE 0: WHY ITS OWN CONTRACT, DECIDED FROM Σ AT HEAD ────────────────────────────────────── +# +# The ruling offered two options — `refusal-receipt-v1`, or a field on `parity-receipt-v1` — and +# warned against defaulting to a new contract because it is easier to write. It is not the easier +# one; it is the one the measurements leave standing. +# +# **Option B is refused on a fact: `parity-receipt-v1` DOES NOT EXIST AT HEAD.** It is in unmerged +# PR #3600, and there it is deliberately the RETIRED logit-parity layout carrying **no shape and no +# instances** — every record was migrated to v2. A live, validated field on a superseded contract +# with zero focus nodes is a field nothing can carry. Independently, by the discriminator this tree +# has now used twice (an artifact family is named by its REQUIRED KEYS, never by its filename): a +# parity receipt requires host, backend, comparator, threshold_source and per-position metrics; a +# refusal requires a verb, a reason, an exit code and `removed_by`. **They share no required key.** +# +# **A third option was considered and refused, and it is the one worth writing down** because it is +# more attractive than B: put `removed_by` on `apr-cli-commands-v1.yaml`, where the verb already is +# the focus node and the universe is already the trustworthy 111 (FALSIFY-CLI-001/002). Refused +# because the registry is the **universe**, and #3597's whole method is to DIFF the registry against +# the V / V2 / refusal buckets. If the buckets live inside the registry, the denominator and the +# numerator are the same artifact and the diff is vacuous by construction — a counter measuring its +# own decoration. The registry says what EXISTS; a refusal says what was TRIED and what happened. +# Keeping them apart is what lets that diff be a real diff. +# +# So: its own contract, joined to the registry by `verb`, so a refusal naming a verb the registry +# does not carry is a dangling reference and red. +# +# ── THE FORCED-BINDING TRAP, AND THE ESCAPE THAT MAKES `minCount 1` SAFE ──────────────────────── +# +# A required field with no escape MANUFACTURES FALSE DATA. Two instances were on the table: +# `pv validate` requires a `kani_harnesses` block, so authors fabricate one; and apex#57, where +# `lean_theorem: Theorems.RowMerged` was copied verbatim into TWELVE contracts, resolved to nothing, +# and the gate stayed green throughout. +# +# The fix copied from apex is a **closed set of declared sentinels**: "there is legitimately nothing +# here" must be SAYABLE and still CHECKABLE. `removed_by` is therefore `minCount 1` — every refusal +# must answer — and the answer may be a release OR one of exactly two sentinels, with everything +# else refused as hard as a dangling value: +# +# v. the release that removes this refusal e.g. v0.70 +# never refused permanently and by design; nothing will remove it +# unscheduled a defect or gap with no release chosen yet +# +# `tbd`, `soon`, `n/a`, `pending`, `0.70` (no `v`), `v0.70.1` (a patch is not a release boundary) +# and a git sha are ALL RED. That is the arm that matters: a validator which only accepts cannot +# tell a real value from an invented one, so the falsifier plants a PLAUSIBLE-but-undeclared +# sentinel and requires red. +# +# WHY A VERSION AND NOT A SHA (`done_when` 2 asks for the choice and the reason). A refusal answers +# a user's question — *"which release do I need?"* — and a sha does not answer it. A sha is precise +# about the tree and silent about the boundary; `v0.70` is the thing a person can wait for, and the +# thing `check_milestone_cut.sh` can count. The sha form is made invalid rather than merely +# discouraged, because a shape that permits two spellings gets both. +# +# KIND: pattern. One JSON document, shaped through the `extract:json` path (ONT-001 §3.7) — no new +# extractor: `entity: {type: json, ref}` + `vocabulary:` is exactly the machinery for "validate this +# document", and a second reader for one more family is the thing this tree keeps filing against. +# ────────────────────────────────────────────── +name: refusal-receipt +version: "1.0.0" +scope: > + What a refused verb must state — the verb, one reason line, the exit code a caller sees, and the + release that removes the refusal or a declared sentinel saying none will. Out of scope: WHICH verbs + are refused (that is #3597's bucket over the 111-verb registry), the V / V2 classification, and + parity receipts, which share none of these required keys. +status: active + +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: PAIML Engineering + description: > + A refusal is a measurement about a verb: what was tried, what the caller sees, and when it ends. + removed_by is required so no refusal is silent about its own lifetime, and answerable with a + closed sentinel so a required field never manufactures a fabricated release. + references: + - 'aprender#3605 (this row), #3597 (the refusal bucket this unblocks), #3080' + - 'contracts/apr-cli-commands-v1.yaml — the 111-verb registry this joins to by `verb`' + - 'apex#57 — lean_theorem copied into twelve contracts, resolving to nothing, gate green: the forced-binding precedent' + - 'tests/fixtures/ont/refusal-{ok,undeclared-sentinel,sha,missing} — the case table, both arms' + +entity: + type: json + ref: evidence/verbs/refusals.json + +vocabulary: + prefix: refusal + root_class: refusal:Ledger + nested: + refusals: refusal:Refusal + +shape: + targetClass: refusal:Refusal + closed: true + properties: + # The join into the registry. A refusal naming a verb `apr --help` does not carry is a dangling + # reference; the registry is the universe and this field is the only thing pointing at it. + - {path: refusal:verb, minCount: 1, maxCount: 1, datatype: xsd:string} + # One line, and it must say something: #3597 records that a refusal whose text names the wrong + # defect is a fail-open, so an empty reason is refused before a wrong one can be written. + - {path: refusal:reason, minCount: 1, maxCount: 1, datatype: xsd:string, minLength: 12} + # What the CALLER sees. A refusal with no distinct exit code is indistinguishable from success + # to anything that is not reading prose. + - {path: refusal:exit_code, minCount: 1, maxCount: 1, datatype: xsd:integer} + # THE FIELD. Required — every refusal answers — with the closed sentinel set as the escape, so + # "nothing will remove this" is sayable without inventing a release. Anything outside the three + # declared forms is as red as a dangling value. + - {path: refusal:removed_by, minCount: 1, maxCount: 1, + pattern: "^(v[0-9]+\\.[0-9]+|never|unscheduled)$"} + +equations: + answerable: + formula: "∀ r ∈ Refusal: removed_by(r) ∈ {v.} ∪ {never, unscheduled}" + domain: "every entry of evidence/verbs/refusals.json" + codomain: "conforms, or a violation naming the focus node and the value" + invariants: + - "a required field with a closed escape cannot be satisfied by inventing a release" + - "a plausible-but-undeclared sentinel (tbd, soon, n/a, pending) is refused, not tolerated" + - "a sha is refused: it is precise about the tree and silent about the boundary a user waits for" + preconditions: + - "the verb names an entry of contracts/apr-cli-commands-v1.yaml" + postconditions: + - "no refusal is silent about its own lifetime" + lean_theorem: none — L4 not declared + +invariants: + - id: RFS-INV-001 + property: every refusal answers for its own lifetime + formal: '|removed_by(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-002 + property: the escape is closed, so the required field cannot manufacture a release + formal: 'removed_by(r) ∉ {v., never, unscheduled} ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-003 + property: a refusal states an exit code a caller can branch on + formal: '|exit_code(r)| = 0 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + - id: RFS-INV-004 + property: a refusal states a reason, so a wrong one is at least visible + formal: 'len(reason(r)) < 12 ⇒ Fail(refusal-receipt-v1, r)' + prose: false + +falsification_tests: + - id: FALSIFY-RFS-001 + rule: both arms of the sentinel set + prediction: > + a refusal carrying `v0.70`, `never` or `unscheduled` conforms; one carrying the PLAUSIBLE but + undeclared `tbd` is refused naming the focus node and the value; so is a git sha, a bare + `0.70`, and a patch-level `v0.70.1` + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a validator that only accepts cannot tell a real value from an invented one + - id: FALSIFY-RFS-002 + rule: the required field, with its escape + prediction: > + a refusal with no `removed_by` at all is refused; adding `never` makes it conform without + naming a release that does not exist + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: the field is required with no escape and starts manufacturing fabricated releases + - id: FALSIFY-RFS-003 + rule: a refusal is legible to a caller + prediction: an entry with no exit_code, or a one-word reason, is refused + test: cargo test -p aprender-contracts-cli --test ont_refusal_receipt + if_fails: a refusal is indistinguishable from success to anything not reading prose diff --git a/tests/fixtures/ont/refusal-undeclared-sentinel/evidence/verbs/refusals.json b/tests/fixtures/ont/refusal-undeclared-sentinel/evidence/verbs/refusals.json new file mode 100644 index 0000000000..1ca401ee7d --- /dev/null +++ b/tests/fixtures/ont/refusal-undeclared-sentinel/evidence/verbs/refusals.json @@ -0,0 +1,11 @@ +{ + "schema": "apr-refusal-ledger/v1", + "refusals": [ + { + "verb": "bench", + "reason": "the subcommand routes through the dense loader and cannot measure this architecture", + "exit_code": 8, + "removed_by": "tbd" + } + ] +} From 51a279ff946fc300cce1a053042ad038c1943785 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 23:37:02 +0200 Subject: [PATCH 2/5] register the new CLI test in scripts/tree_reader_tests.txt MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The registry is derived from the tree and drifts the moment a test that reads the tree is added without listing it. Each of the three new tests failed this guard on its OWN branch — not a shared commit, as first read. Pmat-Ticket: PMAT-3598 Co-Authored-By: Claude Opus 5 (1M context) --- scripts/tree_reader_tests.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/tree_reader_tests.txt b/scripts/tree_reader_tests.txt index e93a263eb2..732e68d042 100644 --- a/scripts/tree_reader_tests.txt +++ b/scripts/tree_reader_tests.txt @@ -72,6 +72,7 @@ aprender-contracts-cli --test ont6_lint_verdict aprender-contracts-cli --test ont6b_kind_default aprender-contracts-cli --test ont_entity_properties aprender-contracts-cli --test ont_extract_json +aprender-contracts-cli --test ont_refusal_receipt aprender-contracts-cli --test pv_surface_gate aprender-contracts-cli --test pvl_zero_contracts aprender-core --lib format::metadata_bounds_contract_falsify From 16d4ae177da6d92784ce4bfb2046fe63faed958a Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 21 Sep 2026 00:43:19 +0200 Subject: [PATCH 3/5] chore(roadmap): mint PMAT-3605 as a work item so the AD-04 quorum can resolve it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `quorum-review.sh` refuses without `pmat work status `, and `pmat work` reads the aggregated roadmap rather than an id counter. This branch carried the trailer while no such work item existed — a GitHub issue number is not a work item until something mints it. The id is DERIVED from the issue: `pmat work add --github-issue` calls that "the path to prefer", because GitHub allocates centrally and `max(id)+1` cannot promise two agents different ids. A fragment rather than a direct roadmap.yaml edit — additive, one file, and it does not make every stacked branch dirty on the same lines. Acceptance hand-entered from the issue's done_when; `pmat work add` derives neither `spec:` nor `acceptance_criteria:` (paiml-mcp-agent-toolkit#1414). Guards: diff_additive, fragment_required, ids_unique, sorted, completion_is_cited all exit 0; `make roadmap-aggregate-check` idempotent. Refs #3605 Pmat-Ticket: PMAT-3605 --- docs/roadmaps/entries/PMAT-3605.yaml | 17 +++++++++++++++++ docs/roadmaps/roadmap.yaml | 17 +++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 docs/roadmaps/entries/PMAT-3605.yaml diff --git a/docs/roadmaps/entries/PMAT-3605.yaml b/docs/roadmaps/entries/PMAT-3605.yaml new file mode 100644 index 0000000000..a23ec665f6 --- /dev/null +++ b/docs/roadmaps/entries/PMAT-3605.yaml @@ -0,0 +1,17 @@ +- id: PMAT-3605 + github_issue: 3605 + item_type: task + title: 'removed_by gets a shape: refusal-receipt-v1 with a closed escape set' + status: in_progress + priority: medium + assigned_to: null + created: 2026-09-21T00:00:00Z + updated: 2026-09-21T00:00:00Z + spec: null + acceptance_criteria: [] + phases: [] + subtasks: [] + estimated_effort: null + labels: + - kind:code + notes: 'ACCEPTANCE (hand-entered from gh#3605 done_when; see paiml-mcp-agent-toolkit#1414). Done when: contracts/refusal-receipt-v1.yaml exists with a shape over removed_by, and the value space is a CLOSED SET rather than free text: pattern ^(v[0-9]+\\.[0-9]+|never|unscheduled)$. The point of the closed set is that legitimately-nothing stays SAYABLE and CHECKABLE — never and unscheduled are honest answers with a shape behind them, instead of a required field manufacturing a fake version. Fixtures cover each arm of the alternation plus a rejecting case. STOP: do not admit free text; do not make the field optional, which would make absence indistinguishable from a deliberate never.' diff --git a/docs/roadmaps/roadmap.yaml b/docs/roadmaps/roadmap.yaml index 3a90bd6297..5ea44e1c1a 100644 --- a/docs/roadmaps/roadmap.yaml +++ b/docs/roadmaps/roadmap.yaml @@ -18848,3 +18848,20 @@ roadmap: labels: - kind:code notes: 'ACCEPTANCE (hand-entered; pmat work add derived neither spec: nor acceptance_criteria: — defect paiml-mcp-agent-toolkit#1414). Spec: docs/specifications/ruling-receipts-under-contract.md (operator ruling 2026-09-20). Done when: contracts/parity-receipt-v1.yaml with its shape on origin/main; extract:parity-receipt implemented; pv lint --gate shapes --path evidence/ in the required check; PR body shows 7 older receipts RED before back-fill and 0 after, plant violation = 1, mutation RED, pc_shape fired; check_parity_receipt.sh folded into the shape or its remainder listed under not_expressible; ONT-4c3 bound with the parity receipt as focus node; verdict rendered on a fleet host once the pv pin lands, else checkout-only: true. Sigma parent bound: json. Back-fill denominator: 7. STOP: subset-insufficient; shared-file-touched without the guard label; any threshold typed into the shape instead of resolved from thresholds.yaml.' +- id: PMAT-3605 + github_issue: 3605 + item_type: task + title: 'removed_by gets a shape: refusal-receipt-v1 with a closed escape set' + status: in_progress + priority: medium + assigned_to: null + created: 2026-09-21T00:00:00Z + updated: 2026-09-21T00:00:00Z + spec: null + acceptance_criteria: [] + phases: [] + subtasks: [] + estimated_effort: null + labels: + - kind:code + notes: 'ACCEPTANCE (hand-entered from gh#3605 done_when; see paiml-mcp-agent-toolkit#1414). Done when: contracts/refusal-receipt-v1.yaml exists with a shape over removed_by, and the value space is a CLOSED SET rather than free text: pattern ^(v[0-9]+\\.[0-9]+|never|unscheduled)$. The point of the closed set is that legitimately-nothing stays SAYABLE and CHECKABLE — never and unscheduled are honest answers with a shape behind them, instead of a required field manufacturing a fake version. Fixtures cover each arm of the alternation plus a rejecting case. STOP: do not admit free text; do not make the field optional, which would make absence indistinguishable from a deliberate never.' From 0cd2c6aee7d38b8024c97b8bf46f9a30addddb7a Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 21 Sep 2026 01:54:46 +0200 Subject: [PATCH 4/5] =?UTF-8?q?fix(tests):=20the=20shape-count=20ratchet?= =?UTF-8?q?=20was=20red=20=E2=80=94=20#3605=20adds=20a=206th=20shape=20(qu?= =?UTF-8?q?orum=20round=201)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `the_tracked_repo_graph_is_fresh` asserts `shapes_n == 5` and names the five. `refusal-receipt-v1` makes six, so this PR shipped a CI red that a quorum lane found and I did not. MEASURED, not guessed: `pv extract contracts --check` on this branch reports `shapes_n: 6, triples: 15620`. The hardcoded count stays hardcoded. A shape added without anyone noticing is exactly what this assertion exists to prevent, so adding one is SUPPOSED to turn it red and make you name the new shape. Noted in the comment that the counter is shared across branches — a sibling PR adding a shape (#3600's parity-receipt-v2) will need it raised again at merge, which is the ratchet working rather than a conflict to route around. Refs #3605 Pmat-Ticket: PMAT-3605 --- .../tests/ont4b_shapes_gate.rs | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/crates/aprender-contracts-cli/tests/ont4b_shapes_gate.rs b/crates/aprender-contracts-cli/tests/ont4b_shapes_gate.rs index 25c6931414..22f750c9b3 100644 --- a/crates/aprender-contracts-cli/tests/ont4b_shapes_gate.rs +++ b/crates/aprender-contracts-cli/tests/ont4b_shapes_gate.rs @@ -216,10 +216,21 @@ fn the_tracked_repo_graph_is_fresh() { assert_eq!(r.code, 0, "{}", show(&r)); let v = json_of(&r); assert!(v["triples"].as_u64().unwrap_or(0) > 5000, "{}", show(&r)); + // MEASURED on this branch: `pv extract contracts --check` reports + // shapes_n=6, triples=15620. The count is deliberately hardcoded rather + // than derived — a shape added without anyone noticing is the thing this + // assertion exists to prevent, so adding one is SUPPOSED to turn it red and + // make you name the new shape here. + // + // It did exactly that for #3605's `refusal-receipt-v1`, and a quorum lane + // caught it rather than I did. Note for whoever merges second: this counter + // is shared across branches, so a sibling PR that also adds a shape + // (#3600's parity-receipt-v2) will need the number raised again at merge — + // that is the ratchet working, not a conflict to route around. assert_eq!( v["shapes_n"], - 5, - "ont-shapes-v1 + ladder-measured + ladder-green (ONT-4c1) + bound-symbols-resolve + lean-statements-grounded (ONT-4b2)\n{}", + 6, + "ont-shapes-v1 + ladder-measured + ladder-green (ONT-4c1) + bound-symbols-resolve + lean-statements-grounded (ONT-4b2) + refusal-receipt-v1 (#3605)\n{}", show(&r) ); } From 644db5cdf7812db3f150081305582015c60e5e45 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 21 Sep 2026 02:02:51 +0200 Subject: [PATCH 5/5] =?UTF-8?q?chore(audits):=20AD-04=20quorum=20receipt?= =?UTF-8?q?=20for=20PMAT-3605=20=E2=80=94=20AGREED=203/3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gemini-3.1-pro-high = PASS, gemini-3.1-pro-low = PASS, gemini-3.6-flash-high = PASS. Author measured as Opus 5 (claude); no lane in the author's family. Lane models set per-invocation via PAIML_IMPLEMENT_CONFIG, never by editing the shared config that other sessions were launching against. This trio was chosen on measured odds after flash-class lanes returned NO-VERDICT intermittently (3.7-flash 3/7, 3.6-flash 1/7, pro-high 0/7 across my earlier runs). All 15 lanes voted in this batch. Refs #3613 Pmat-Ticket: PMAT-3605 --- docs/audits/quorum-PMAT-3605.json | 201 ++++++++++++++++++++++++++++++ 1 file changed, 201 insertions(+) create mode 100644 docs/audits/quorum-PMAT-3605.json diff --git a/docs/audits/quorum-PMAT-3605.json b/docs/audits/quorum-PMAT-3605.json new file mode 100644 index 0000000000..e3ea20aeb4 --- /dev/null +++ b/docs/audits/quorum-PMAT-3605.json @@ -0,0 +1,201 @@ +{ + "ticket": "PMAT-3605", + "base": "origin/main", + "base_resolved": "origin/main", + "base_note": "no origin/origin/main exists; judged against the local ref", + "head": "0cd2c6aee7d38b8024c97b8bf46f9a30addddb7a", + "diff_sha256": "0786058175344b37587bbf439231e7c79b53085bba429a2468ec83c190a15eca", + "width": 3, + "executor": "agy", + "prompt_mode": "file", + "prompt_bytes": 125886, + "author": { + "model": "Opus 5 (1M context)", + "family": "claude", + "source": "measured" + }, + "agreed": true, + "lanes": [ + { + "lane": 1, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "The diff correctly implements PMAT-3605. It creates the refusal-receipt-v1 shape with `removed_by` configured as a mandatory field (minCount: 1) matching the exact closed set pattern `^(v[0-9]+\\.[0-9]+|never|unscheduled)$`. It includes fixtures for each accepted sentinel arm as well as rejecting edge cases (such as 'tbd', sha, and bare versions). Both the ont_refusal_receipt and ont4b_shapes_gate tests pass successfully. There are no violations of the ticket's negative criteria.", + "findings": [ + { + "claim": "The ont_refusal_receipt test suite successfully verifies the requirements, passing 9/9 tests including all arms of the alternation and rejection cases.", + "command": "cargo test -p aprender-contracts-cli --test ont_refusal_receipt", + "file": "crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs", + "grounding": "measured", + "line": 442, + "output": "test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s" + }, + { + "claim": "The ont4b_shapes_gate test suite passes 11/11 tests, successfully verifying the tracked repo graph is fresh and confirming shapes_n equals 6.", + "command": "cargo test -p aprender-contracts-cli --test ont4b_shapes_gate", + "file": "crates/aprender-contracts-cli/tests/ont4b_shapes_gate.rs", + "grounding": "measured", + "line": 228, + "output": "test result: ok. 11 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 13.86s" + }, + { + "claim": "refusal-receipt-v1.yaml defines removed_by as a required property (minCount: 1) and enforces a closed pattern ^(v[0-9]+\\.[0-9]+|never|unscheduled)$, satisfying the ticket criteria.", + "file": "contracts/refusal-receipt-v1.yaml", + "grounding": "cited", + "line": 226 + } + ], + "raw_bytes": 5709, + "err_bytes": 100, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.1-pro-high", + "model_measured": "gemini-3.1-pro-high", + "model_source": "measured", + "family": "gemini" + }, + { + "lane": 2, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "The provided diff correctly implements PMAT-3605. The 'removed_by' field is constrained by a shape in 'refusal-receipt-v1.yaml' using a closed set pattern ('^(v[0-9]+\\\\.[0-9]+|never|unscheduled)$') and is mandatory (minCount: 1). The test fixtures cover the acceptable arms and rejection cases.", + "findings": [ + { + "claim": "The diff implements a contract 'refusal-receipt-v1.yaml' with a shape over 'removed_by' that uses a closed set pattern for its values, ensuring it is required and not free text.", + "file": "contracts/refusal-receipt-v1.yaml", + "grounding": "cited" + } + ], + "raw_bytes": 3256, + "err_bytes": 0, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.1-pro-low", + "model_measured": "gemini-3.1-pro-low", + "model_source": "measured", + "family": "gemini" + }, + { + "lane": 3, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "Diff for ticket PMAT-3605 (#3605) completely and correctly implements 'removed_by gets a shape: refusal-receipt-v1 with a closed escape set'. The new pattern contract `contracts/refusal-receipt-v1.yaml` defines a closed set regex pattern `^(v[0-9]+\\\\.[0-9]+|never|unscheduled)$` with `minCount: 1` on `removed_by`, preventing free text and fabricated releases. Eight fixture test cases in `tests/fixtures/ont/` and `crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs` test both valid sentinels (v0.70, never, unscheduled) and invalid entries (tbd, sha, bare version, patch version, missing field, terse reason). `shapes_n` count in `ont4b_shapes_gate.rs` was updated from 5 to 6, and all tests pass without drift.", + "findings": [ + { + "claim": "The ont_refusal_receipt test suite passes 9/9 tests, verifying both accepted sentinels (v0.70, never, unscheduled) and rejected edge cases (tbd, sha, bare version 0.70, patch version v0.70.1, missing removed_by, no exit_code, terse reason).", + "command": "cargo test -p aprender-contracts-cli --test ont_refusal_receipt", + "file": "crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs", + "grounding": "measured", + "line": 442, + "output": "test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s" + }, + { + "claim": "The ont4b_shapes_gate test suite passes 11/11 tests, confirming the tracked repo graph assertion for shapes_n == 6.", + "command": "cargo test -p aprender-contracts-cli --test ont4b_shapes_gate", + "file": "crates/aprender-contracts-cli/tests/ont4b_shapes_gate.rs", + "grounding": "measured", + "line": 228, + "output": "test result: ok. 11 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 16.42s" + }, + { + "claim": "pv extract contracts --check verifies zero drift across 15620 triples and 6 shapes.", + "command": "cargo run -p aprender-contracts-cli --bin pv -- extract contracts --check", + "file": "contracts/census.json", + "grounding": "measured", + "line": 32, + "output": "{\n \"triples\": 15620,\n \"sha256\": \"54e4a15ab7f6e4415aa7959a51826f731b650a1998e80b635e6850ae8f5df283\",\n \"shapes_n\": 6,\n \"written\": [],\n \"check\": []\n}" + }, + { + "claim": "contracts/refusal-receipt-v1.yaml defines removed_by as a required property (minCount: 1) with a closed pattern pattern: ^(v[0-9]+\\.[0-9]+|never|unscheduled)$.", + "file": "contracts/refusal-receipt-v1.yaml", + "grounding": "cited", + "line": 226 + } + ], + "raw_bytes": 7209, + "err_bytes": 100, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.6-flash-high", + "model_measured": "gemini-3.6-flash-high", + "model_source": "measured", + "family": "gemini" + } + ], + "dissent": [], + "dedup": [ + { + "file": "contracts/census.json", + "line": 32, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "pv extract contracts --check verifies zero drift across 15620 triples and 6 shapes." + ] + }, + { + "file": "contracts/refusal-receipt-v1.yaml", + "line": null, + "lanes_agreeing": [ + 2 + ], + "claims": [ + "The diff implements a contract 'refusal-receipt-v1.yaml' with a shape over 'removed_by' that uses a closed set pattern for its values, ensuring it is required and not free text." + ] + }, + { + "file": "contracts/refusal-receipt-v1.yaml", + "line": 226, + "lanes_agreeing": [ + 1, + 3 + ], + "claims": [ + "contracts/refusal-receipt-v1.yaml defines removed_by as a required property (minCount: 1) with a closed pattern pattern: ^(v[0-9]+\\.[0-9]+|never|unscheduled)$.", + "refusal-receipt-v1.yaml defines removed_by as a required property (minCount: 1) and enforces a closed pattern ^(v[0-9]+\\.[0-9]+|never|unscheduled)$, satisfying the ticket criteria." + ] + }, + { + "file": "crates/aprender-contracts-cli/tests/ont4b_shapes_gate.rs", + "line": 228, + "lanes_agreeing": [ + 1, + 3 + ], + "claims": [ + "The ont4b_shapes_gate test suite passes 11/11 tests, confirming the tracked repo graph assertion for shapes_n == 6.", + "The ont4b_shapes_gate test suite passes 11/11 tests, successfully verifying the tracked repo graph is fresh and confirming shapes_n equals 6." + ] + }, + { + "file": "crates/aprender-contracts-cli/tests/ont_refusal_receipt.rs", + "line": 442, + "lanes_agreeing": [ + 1, + 3 + ], + "claims": [ + "The ont_refusal_receipt test suite passes 9/9 tests, verifying both accepted sentinels (v0.70, never, unscheduled) and rejected edge cases (tbd, sha, bare version 0.70, patch version v0.70.1, missing removed_by, no exit_code, terse reason).", + "The ont_refusal_receipt test suite successfully verifies the requirements, passing 9/9 tests including all arms of the alternation and rejection cases." + ] + } + ], + "uncovered": [], + "coverage_source": "lanes", + "partial": false, + "partial_reasons": [], + "auto_merge": { + "checked": true, + "was_armed": false, + "disarmed": false, + "note": "auto-merge not armed" + }, + "lint": { + "ok": true, + "output": "receipt complete: kind=artifact lanes=3 author=Opus 5 (1M context)/claude" + } +}