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 016e5b245e..0b10e7672c 100644 --- a/contracts/census.json +++ b/contracts/census.json @@ -1,8 +1,8 @@ { "schema": "ont.paiml.dev/census/v1alpha1", "git_sha": null, - "n_files": 1801, - "n_parsed": 1801, + "n_files": 1802, + "n_parsed": 1802, "n_parse_errors": 0, "parse_errors": [], "quarantined_n": 0, @@ -12,7 +12,7 @@ "kernel": 363, "model-family": 28, "model-family-variant": 1, - "pattern": 87, + "pattern": 88, "pretraining-corpus": 2, "registry": 519, "schema": 766, @@ -22,14 +22,15 @@ }, "by_entity_type": { "gguf": 2, + "json": 1, "pv-contract": 1 }, "by_anchoring": { "unanchored": 1798, "class": 2, - "instance": 1 + "instance": 2 }, - "id_set_sha256": "e624814d2c82e8a53ab24faac0b5281c0dad15618d9f14e970c740c8391cb712", + "id_set_sha256": "8d53c71ff540e3bb91f2d6648ed821be663a8d9315712fec3bcaa2a7e9c9cc10", "declared_external": [ { "name": "provable-contracts", diff --git a/contracts/contracts.nt b/contracts/contracts.nt index dc9a62ac7d..ecf029474e 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -8778,6 +8778,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"^^ . @@ -9825,6 +9835,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/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) ); } 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/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" + } +} 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 618b9a93ca..4855c552e8 100644 --- a/docs/roadmaps/roadmap.yaml +++ b/docs/roadmaps/roadmap.yaml @@ -18973,6 +18973,23 @@ roadmap: labels: - kind:code notes: 'ACCEPTANCE (hand-entered from issue #3587 "What lands"; minted on the PR branch so the AD-04 quorum can run -- pmat work status refuses a missing item). Two halves: the explicit-command runner (#3616, merged) and the nextest [profile.ci] key (#3626). Lands: 1. **--no-fail-fast on the shard.** The cost is runner minutes on an already-red shard; the benefit is that a red run still measures everything else it was going to measure — which is exactly when you most want the data. 2. **The reducer reports ran / skipped / total** in the shard receipt. The skipped count is a **number**, never an absence. 3. **A receipt with skipped > 0 is Unknown, not Fail and not Pass** — it names what was not measured, per doctrine 4. ' +- 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.' - id: PMAT-3627 github_issue: 3627 item_type: task 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/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 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" + } + ] +}