diff --git a/ci/explicit-test-commands.d/450-aprender-contracts-cli-shapes-vacuity.cmd b/ci/explicit-test-commands.d/450-aprender-contracts-cli-shapes-vacuity.cmd new file mode 100644 index 0000000000..75beb0e63c --- /dev/null +++ b/ci/explicit-test-commands.d/450-aprender-contracts-cli-shapes-vacuity.cmd @@ -0,0 +1 @@ +cargo test -p aprender-contracts-cli --test shapes_vacuity diff --git a/crates/aprender-contracts-cli/tests/shapes_vacuity.rs b/crates/aprender-contracts-cli/tests/shapes_vacuity.rs new file mode 100644 index 0000000000..c96ed9b246 --- /dev/null +++ b/crates/aprender-contracts-cli/tests/shapes_vacuity.rs @@ -0,0 +1,305 @@ +//! #3610 — an armed shape that graded ZERO focus nodes must not be counted as clean. +//! +//! **The defect, measured on pv 0.68.2.** `NoFocus` asked the question GLOBALLY — +//! `report.focus_nodes_n == 0` — which is only ever true for a lone contract. In a **directory** +//! one empty shape is invisible: the other shapes carry the total above zero, the empty one +//! contributes no violations, and the aggregate reports **`Pass` while listing it in +//! `armed_shapes`**. A `type: jsonl` contract whose rows violate its own `sh:pattern` passed exactly +//! that way, and `armed_shapes` is the tool's claim about what it measured. +//! +//! `by_shape` had carried `=0` all along. **Nothing read it** — the same *computed but +//! unexposed* shape as #3597, this time inside the gate itself. +//! +//! **BOTH VENUES, because the lone-contract case already declined correctly and a fix proved only +//! there proves nothing.** The directory case is the one that lied. +//! +//! | fixture | shape reach | armed? | expected | +//! |---|---|---|---| +//! | `shapes-one-empty` | `empty-shape=0`, `tool-status=1` | yes | **exit 2**, decline naming `empty-shape` | +//! | `shapes-one-empty-unarmed` | same | no | **Pass**, `declines: ["empty-shape"]` | +//! | `shapes-one-empty-and-violating` | `empty-shape=0`, `tool-status=1` (violating) | yes | **exit 1**, Fail, `declines: ["empty-shape"]` | +//! | `json-ok` | `tool-status=1` | yes | Pass, `declines: []` | +//! | `shapes-all-empty` | `empty-shape=0` (the only shape) | yes | **exit 2** via the global path, no report yet (#4100) | +//! +//! The second row is what keeps the fix from being "refuse whenever anything is empty": an UNARMED +//! shape at zero did not affect the verdict, so it is **reported** rather than refused — and it is +//! reported, not swallowed, which is the half the original defect got wrong. + +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("../..") +} + +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 extra(&self) -> serde_json::Value { + serde_json::from_str::(&self.stdout) + .map(|v| v["extra"].clone()) + .unwrap_or(serde_json::Value::Null) + } +} + +fn shapes_on(fixture: &str) -> Run { + let contracts = repo_root() + .join("tests/fixtures/ont") + .join(fixture) + .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(), + } +} + +#[test] +fn an_armed_shape_that_graded_nothing_refuses_in_a_directory() { + // THE CASE THAT LIED. Before #3610 this was `Pass` with `empty-shape` in `armed_shapes`. + let r = shapes_on("shapes-one-empty"); + assert_eq!( + r.code, + 2, + "a vacuous armed shape must DECLINE, not pass and not fail\n{}", + r.all() + ); + // THE REFUSAL IS THE EXIT CODE; THE REPORT IS THE EVIDENCE. Downstream consumers (infra's SLK + // gate) capture stdout and parse it REGARDLESS of exit code, because pv already exits non-zero + // on Fail. A refusal that printed only a bare `decline:` line would read to them as "no + // by_shape" and score UNMEASURED — indistinguishable, from their side, from a broken pv. + let extra = r.extra(); + assert!( + !extra.is_null(), + "stdout must still parse as JSON on the exit-2 path\n{}", + r.all() + ); + assert_eq!( + serde_json::from_str::(&r.stdout).expect("json")["verdict"].as_str(), + Some("Unknown(NoFocus)"), + "the report must carry the declining verdict\n{}", + r.all() + ); + assert!( + extra["by_shape"] + .as_array() + .expect("by_shape") + .iter() + .any(|s| s.as_str() == Some("empty-shape=0")), + "by_shape must NAME the zero-focus shape on the exit-2 path — it is the evidence\n{}", + r.all() + ); + assert_eq!( + extra["declines"][0].as_str(), + Some("empty-shape"), + "the refusal must name the shape in declines\n{}", + r.all() + ); + assert!( + !extra["armed_shapes"] + .as_array() + .expect("armed_shapes") + .iter() + .any(|s| s.as_str() == Some("empty-shape")), + "a shape that graded nothing has no place in armed_shapes\n{}", + r.all() + ); + assert!( + !extra["not_armed_shapes"] + .as_array() + .expect("not_armed_shapes") + .iter() + .any(|s| s.as_str() == Some("empty-shape")), + "nor in not_armed_shapes: filing a vacuity as a policy choice is how it hid\n{}", + r.all() + ); +} + +#[test] +fn an_unarmed_shape_that_graded_nothing_is_reported_not_refused() { + // The other direction, and the reason this is not "refuse whenever anything is empty". + let r = shapes_on("shapes-one-empty-unarmed"); + assert_eq!( + r.code, + 0, + "an UNARMED empty shape must not refuse\n{}", + r.all() + ); + let extra = r.extra(); + assert_eq!( + extra["declines"].as_array().map(|a| a.len()), + Some(1), + "the empty shape must be REPORTED in declines, not swallowed\n{}", + r.all() + ); + assert_eq!( + extra["declines"][0].as_str(), + Some("empty-shape"), + "{}", + r.all() + ); + assert!( + !extra["armed_shapes"] + .as_array() + .expect("armed_shapes") + .iter() + .any(|s| s.as_str() == Some("empty-shape")), + "a shape that graded nothing has no place in armed_shapes\n{}", + r.all() + ); + // THE HALF THIS TEST WAS MISSING. The criterion is "neither list", and only + // the armed sibling above checked both — so an UNARMED vacuity could sit in + // `not_armed_shapes`, filed as a deliberate policy choice, which is exactly + // how the original defect hid. It did: the partition filtered on + // `vacuous_armed`, and two quorum lanes found it independently while this + // test stayed green. + assert!( + !extra["not_armed_shapes"] + .as_array() + .expect("not_armed_shapes") + .iter() + .any(|s| s.as_str() == Some("empty-shape")), + "an UNARMED shape that graded nothing must not be filed under \ + not_armed_shapes either — `declines` is the only list it belongs in\n{}", + r.all() + ); +} + +/// A REAL VIOLATION OUTRANKS A VACUITY — found by all three lanes of the #3622 re-review. +/// +/// `vacuous_armed` and `passed` are computed over DISJOINT shapes: one armed shape can grade +/// nothing while another armed shape grades a node and finds it broken. The first cut checked +/// vacuity first, so this corpus reported `Unknown(NoFocus)` / exit 2 — and a consumer that reads +/// exit 2 as "unmeasured" never saw a Fail the gate had actually measured. The decline is still +/// REPORTED in `declines`; it just may not hide the verdict. +#[test] +fn a_real_violation_is_a_fail_even_beside_a_vacuous_armed_shape() { + let r = shapes_on("shapes-one-empty-and-violating"); + assert_eq!( + r.code, + 1, + "a measured violation must FAIL, not decline, when another armed shape graded nothing\n{}", + r.all() + ); + assert_eq!( + serde_json::from_str::(&r.stdout).expect("json")["verdict"].as_str(), + Some("Fail"), + "{}", + r.all() + ); + assert_eq!( + r.extra()["declines"][0].as_str(), + Some("empty-shape"), + "the vacuous shape must still be NAMED in declines on the Fail path\n{}", + r.all() + ); +} + +#[test] +fn a_corpus_whose_shapes_all_graded_something_still_passes_with_an_empty_declines() { + // The control for the control: without this, a build that declined EVERYTHING would pass the + // two cases above. + let r = shapes_on("json-ok"); + assert_eq!(r.code, 0, "{}", r.all()); + assert_eq!( + r.extra()["declines"].as_array().map(Vec::len), + Some(0), + "nothing graded zero here, so declines must be empty\n{}", + r.all() + ); +} + +/// THE GLOBAL VENUE — every shape at zero, so `report.focus_nodes_n == 0` and `decline()` returns +/// `ShapesOutcome::NoFocus` before the result path runs. It declined before #3610 and must still. +/// +/// **Corrected by the #3622 re-review (all three lanes).** These two tests first ran +/// `json-missing-ref`, which exits **3** on an unreadable `entity.ref` (`ont_extract_json.rs:128`) +/// before `decline()` is consulted, so `code != 0` and "no report" both held for the wrong reason +/// and neither test ever reached the path it named. `shapes-all-empty` reaches it: exit 2. +#[test] +fn a_corpus_whose_every_shape_graded_nothing_declines_through_the_global_path() { + let r = shapes_on("shapes-all-empty"); + assert_eq!( + r.code, + 2, + "every shape at zero must DECLINE (exit 2), not pass, fail, or error out\n{}", + r.all() + ); + assert!( + r.stderr.contains("NoFocus"), + "the decline must be the NoFocus one, not some other refusal\n{}", + r.all() + ); +} + +/// THE ASYMMETRY, ASSERTED RATHER THAN LEFT UNSAID. The global path renders through +/// `skipped_gate(...)` with no `extra`, so it declines with **no `by_shape` and no `declines`**, +/// while the per-shape path (the one #3610 fixed) declines *with* the full report. The consumer that +/// motivated the report requirement (infra's SLK gate) parses stdout whatever the exit code, so on +/// this path it gets nothing. **Filed as #4100**, not fixed here: it needs the NoFocus outcome to +/// carry the report, a change to the outcome path rather than to the verdict. +#[test] +fn the_global_nofocus_decline_prints_no_report_and_that_is_recorded() { + let r = shapes_on("shapes-all-empty"); + assert_eq!(r.code, 2, "{}", r.all()); + assert!( + r.extra().is_null(), + "if this venue has GAINED a report, #4100 is fixed — replace this test with an assertion of \ + the report and add `shapes-all-empty` to the_three_answers_remain_distinct's loop\n{}", + r.all() + ); +} + +#[test] +fn the_three_answers_remain_distinct() { + // pass / fail / decline must not collapse: a build that returned one code for everything + // would satisfy any single assertion above. + let pass = shapes_on("json-ok").code; + let fail = shapes_on("json-violation").code; + let decline = shapes_on("shapes-one-empty").code; + assert_eq!( + (pass, fail, decline), + (0, 1, 2), + "pass / fail / decline must differ" + ); + // Every one of the three must also PRINT its report — a consumer that captures stdout and + // parses it regardless of exit code must get a document in all three cases, not two. + for fixture in ["json-ok", "json-violation", "shapes-one-empty"] { + let r = shapes_on(fixture); + assert!( + !r.extra().is_null(), + "{fixture} did not emit a parseable report\n{}", + r.all() + ); + assert!( + r.extra()["by_shape"].is_array(), + "{fixture}: extra.by_shape must be present whatever the exit code\n{}", + r.all() + ); + } +} diff --git a/crates/aprender-contracts/src/lint/mod.rs b/crates/aprender-contracts/src/lint/mod.rs index 47f2950b46..5f69bf48fe 100644 --- a/crates/aprender-contracts/src/lint/mod.rs +++ b/crates/aprender-contracts/src/lint/mod.rs @@ -144,6 +144,23 @@ pub enum GateDetail { /// it and none can `match` it. That is what makes it extensible where `GateDetail` is /// not, and it is `#[non_exhaustive]` from birth so the *next* post-0.3.1 gate does /// not have to repeat this exercise. +// `Shapes` is 304 bytes against a 88-byte second-largest, and adding `declines` to it is what +// crossed the threshold — `origin/main` at 237fbc32f lints clean, this branch does not, so the +// finding is this PR's and not inherited. +// +// ALLOWED RATHER THAN BOXED, deliberately. `large_enum_variant` is a cost heuristic about copying +// and stack size: a `GateExtra` is built ONCE PER GATE RUN, moved a handful of times, and then +// serialised. There is no hot path here for 216 bytes to matter on, so the lint is measuring a cost +// this type does not pay. +// +// The alternatives are worse. Boxing one field (clippy suggests `pc_extract`) reclaims 16 bytes and +// does not clear the ratio, so it would be churn that silences nothing. Boxing the whole payload — +// `Shapes(Box)` — turns a struct variant into a newtype variant, which CHANGES THE +// SERDE REPRESENTATION of a `#[serde(tag = "type")]` enum that downstream consumers parse; the SLK +// gate reads this JSON. Breaking a wire format to satisfy a stack-size heuristic is the wrong trade. +// +// If `GateExtra` ever ends up in a loop or a large collection, this allow is the thing to revisit. +#[allow(clippy::large_enum_variant)] #[derive(Debug, Clone, Serialize)] #[serde(tag = "type")] #[non_exhaustive] @@ -221,6 +238,27 @@ pub enum GateExtra { armed_shapes: Vec, /// Shapes computed and reported but not armed — their violations are in `unarmed_violations`. not_armed_shapes: Vec, + /// #3610: shapes that graded ZERO focus nodes, named — the reach the gate did not have. + /// + /// A separate list from `not_armed_shapes` on purpose. "Not armed by policy" and "armed and + /// measured nothing" are different facts, and folding the second into the first would file a + /// vacuity as a deliberate choice — which is how the defect hid in the first place. + /// + /// **This carries EVERY shape that graded zero, armed or unarmed**, and it is the only list + /// any of them appears in: a vacuity is in neither `armed_shapes` (the tool's claim about + /// what it MEASURED) nor `not_armed_shapes` (a policy choice it never made). + /// + /// The two differ in what they do to the verdict, not in whether they are listed here. An + /// ARMED vacuity drives the verdict to `Unknown(NoFocus)` and the run declines — unless an + /// armed shape that DID grade something found a violation, in which case the verdict is + /// `Fail` (a measured violation outranks a vacuity, #3622). An UNARMED one leaves the + /// verdict alone, because it never fed it. Both are named, because a reader + /// needs to know the gate looked at nothing for them either way. + /// + /// An earlier draft of this comment said an armed vacuity "does not reach here at all", + /// which was false — nothing returns early at the verdict, and both kinds reach this field. + /// A quorum lane caught the sentence; the code beside it had the matching bug. + declines: Vec, /// Violations from unarmed shapes (named in the findings as warnings; never in the meet). unarmed_violations: usize, /// Focus nodes each extractor produced: `pv-contract`, `gguf`, `apr-model`. diff --git a/crates/aprender-contracts/src/lint/shapes_gate.rs b/crates/aprender-contracts/src/lint/shapes_gate.rs index e813127d18..f66b77c296 100644 --- a/crates/aprender-contracts/src/lint/shapes_gate.rs +++ b/crates/aprender-contracts/src/lint/shapes_gate.rs @@ -153,6 +153,40 @@ pub fn run_shapes_gate(contract_dir: &Path) -> ShapesOutcome { .any(|p| p.resolves.as_deref() == Some("receipt")) }); + // #3610: the per-shape reach, computed BEFORE any verdict. `by_shape` has carried this number + // all along and nothing ever read it for the one question it answers: did this shape grade + // anything at all? + let focus_of: Vec<(String, usize)> = shapes + .iter() + .map(|s| { + ( + s.id.clone(), + shapes::instances_closed(&graph, &s.target_class).len(), + ) + }) + .collect(); + // TWO sets, because they answer two different questions and conflating them + // was the defect a quorum lane caught here (#3610 round 1, found independently + // by two lanes). + // + // `vacuous_armed` decides the VERDICT: only an ARMED shape that graded nothing + // can refuse, because an unarmed one never fed the verdict in the first place. + // + // `vacuous_any` decides the LISTS. The criterion is that a vacuous shape appears + // in NEITHER `armed_shapes` NOR `not_armed_shapes` — and filtering the partition + // by `vacuous_armed` left every UNARMED vacuity sitting in `not_armed_shapes`, + // filed as a policy choice, which is precisely how the original defect hid. + let vacuous_any: Vec = focus_of + .iter() + .filter(|(_, n)| *n == 0) + .map(|(id, _)| id.clone()) + .collect(); + let vacuous_armed: Vec = vacuous_any + .iter() + .filter(|id| arming.is_armed(id)) + .cloned() + .collect(); + let (mut report, plant_violations) = validate_with_plant(&graph, &shapes, &arming); // A torn JSONL line is the INPUT's fault and is carried as a warning on the entity's root shape — the // gate already rules that warnings alone are `Unknown{Warn}`, never a pass and never a silent drop. @@ -199,24 +233,39 @@ pub fn run_shapes_gate(contract_dir: &Path) -> ShapesOutcome { &extraction.apr_model, ); let passed = counted.violations == 0; + // #3610: an armed shape that graded nothing cannot contribute to a verdict, and a verdict that + // counts it as clean is a Pass over an unasked question. + // + // THE REFUSAL IS THE EXIT CODE; THE REPORT IS THE EVIDENCE. This declines through the ordinary + // result path rather than short-circuiting, so stdout still carries the full JSON — `verdict`, + // `by_shape` naming the zero-focus shape, `declines` — and `meet_exit` turns Unknown into + // exit 2. Downstream consumers (infra's SLK gate) capture stdout and parse it REGARDLESS of the + // exit code, because pv already exits non-zero on Fail; a refusal that printed only a bare + // `decline:` line would read to them as "no by_shape" and score UNMEASURED — the same defect as + // a gate swallowing a decline, seen from the other side. + // + // A MEASURED violation outranks a vacuity (#3622 re-review, all three lanes): `passed` and + // `vacuous_armed` range over DISJOINT shapes, so checking vacuity first turned a real Fail from + // one shape into exit 2 because a DIFFERENT shape graded nothing. The vacuity stays in + // `declines`; it may not hide the verdict. let verdict = if !passed { Verdict::Fail + } else if !vacuous_armed.is_empty() { + Verdict::Unknown(Reason::NoFocus) } else if counted.warnings > 0 { Verdict::Unknown(Reason::Warn) } else { Verdict::Pass }; - let mut by_shape: Vec = shapes - .iter() - .map(|s| { - let n = shapes::instances_closed(&graph, &s.target_class).len(); - format!("{}={}", s.id, n) - }) - .collect(); + let mut by_shape: Vec = focus_of.iter().map(|(id, n)| format!("{id}={n}")).collect(); by_shape.sort(); + // A shape that graded nothing appears in NEITHER list: `armed_shapes` is the tool's claim about + // what it MEASURED, and `not_armed_shapes` means "not armed by policy". Filing a vacuity as a + // policy choice is how this defect hid, so it is named in `declines` only. let (armed_names, not_armed): (Vec, Vec) = shapes .iter() .map(|s| s.id.clone()) + .filter(|id| !vacuous_any.contains(id)) .partition(|id| arming.is_armed(id)); let by_entity_type: BTreeMap = [ ( @@ -265,6 +314,13 @@ pub fn run_shapes_gate(contract_dir: &Path) -> ShapesOutcome { triples: graph.len(), armed_shapes: armed_names, not_armed_shapes: not_armed, + // Every shape that graded NOTHING, armed or not — this is the ONLY list a + // vacuity appears in. An armed vacuity also drove the verdict to + // `Unknown(NoFocus)` above (nothing returns early there; the verdict is set + // and the run continues, so both armed and unarmed vacuities reach here). + // A field that can only ever be empty is decoration, which is the defect one + // layer up from this one. + declines: vacuous_any.clone(), unarmed_violations: counted.unarmed_violations, by_entity_type, pc_extract, diff --git a/docs/audits/quorum-PMAT-3610.json b/docs/audits/quorum-PMAT-3610.json new file mode 100644 index 0000000000..083372aaad --- /dev/null +++ b/docs/audits/quorum-PMAT-3610.json @@ -0,0 +1,272 @@ +{ + "ticket": "PMAT-3610", + "base": "origin/main", + "base_resolved": "origin/main", + "base_note": "no origin/origin/main exists; judged against the local ref", + "head": "3aab786b1b0cbf689449faac68b534e4df4d2f0e", + "diff_sha256": "4302e9fa569c04f0974d30c1cf15d23384378d5754c66f99db39b611f2ac9e6e", + "width": 3, + "executor": "agy", + "prompt_mode": "inline", + "prompt_bytes": 67893, + "author": { + "model": "Opus 5 (1M context)", + "family": "claude", + "source": "measured" + }, + "agreed": true, + "lanes": [ + { + "lane": 1, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "The diff correctly implements per-shape vacuity checking as requested in PMAT-3610. Vacuity is evaluated for each shape individually before making verdict decisions. Armed shapes with zero focus nodes correctly trigger an `Unknown(NoFocus)` decline (exit 2), while unarmed vacuous shapes are reported without refusing the gate. Vacuous shapes are explicitly filtered out from both the `armed_shapes` and `not_armed_shapes` arrays to prevent them from being hidden as policy choices. All changes are thoroughly tested in both the directory and lone-contract venues, with assertions confirming exit codes remain distinct and JSON outputs parse correctly.", + "findings": [ + { + "claim": "Vacuity is computed per-shape before verdicts.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 156 + }, + { + "claim": "An ARMED shape with zero focus nodes declines with Unknown(NoFocus).", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 245 + }, + { + "claim": "Vacuous shapes are explicitly removed from both armed_shapes and not_armed_shapes.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 260 + }, + { + "claim": "Both armed and unarmed vacuous shapes are correctly reported in declines[] array.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 318 + }, + { + "claim": "pass/fail/decline remain distinct (0/1/2) and emit parseable reports.", + "file": "crates/aprender-contracts-cli/tests/shapes_vacuity.rs", + "grounding": "cited", + "line": 184 + } + ], + "raw_bytes": 5254, + "err_bytes": 0, + "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 diff correctly computes vacuity per-shape before formulating a verdict. Armed vacuous shapes decline the run (`Unknown(NoFocus)`) and unarmed vacuous shapes simply report via `declines[]` without declining the build. Both cases properly omit the vacuous shapes from `armed_shapes` and `not_armed_shapes`, addressing the defect. Additionally, robust integration tests are included that verify both the directory and lone-contract venues, ensuring exit codes 0/1/2 are strictly preserved along with valid JSON output. No gates are weakened and all PMAT-3610 requirements are met.", + "findings": [ + { + "claim": "Vacuity is computed per-shape before any verdict is formed.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 156 + }, + { + "claim": "An ARMED shape at zero declines with Unknown(NoFocus) (which maps to exit 2) and is explicitly named in `declines`.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 245 + }, + { + "claim": "An UNARMED shape at zero is reported in `declines[]` without refusing the build.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 318 + }, + { + "claim": "Vacuous shapes are explicitly removed from both `armed_shapes` and `not_armed_shapes` via a filter prior to partitioning.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 260 + }, + { + "claim": "The added tests verify that pass, fail, and decline answers remain distinct (exit codes 0, 1, 2) and all three cases emit parseable reports.", + "file": "crates/aprender-contracts-cli/tests/shapes_vacuity.rs", + "grounding": "cited", + "line": 184 + } + ], + "raw_bytes": 5458, + "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": "Review PASS (Lane 3 of 3): The diff fully satisfies ticket PMAT-3610 without violating any constraints or weakening gates. Per-shape vacuity is computed before forming verdicts, armed vacuous shapes in directory evaluations decline with exit code 2 while retaining stdout JSON reports and `declines[]` listings, unarmed vacuous shapes are reported in `declines[]` without refusing (exit code 0), and vacuous shapes are correctly excluded from `armed_shapes` and `not_armed_shapes`. Integration tests and fixtures verify both directory and lone-contract venues.", + "findings": [ + { + "claim": "Per-shape focus node counts (`focus_of`) and vacuous sets (`vacuous_any`, `vacuous_armed`) are evaluated before forming any gate verdict.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 159 + }, + { + "claim": "An armed shape grading zero focus nodes sets the verdict to `Unknown(NoFocus)` (exit code 2) while continuing stdout JSON report generation.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 246 + }, + { + "claim": "Vacuous shapes (armed or unarmed) are filtered out of both `armed_shapes` and `not_armed_shapes` partitions, appearing exclusively in `declines`.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 260 + }, + { + "claim": "Unarmed vacuous shapes do not trigger a refusal verdict but are reported in `declines[]` without swallowing the finding.", + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "grounding": "cited", + "line": 318 + }, + { + "claim": "Integration tests in `shapes_vacuity.rs` cover directory and lone-contract venues, verifying 0/1/2 exit code distinction and JSON report emission.", + "file": "crates/aprender-contracts-cli/tests/shapes_vacuity.rs", + "grounding": "cited", + "line": 79 + } + ], + "raw_bytes": 5895, + "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": "crates/aprender-contracts-cli/tests/shapes_vacuity.rs", + "line": 79, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "Integration tests in `shapes_vacuity.rs` cover directory and lone-contract venues, verifying 0/1/2 exit code distinction and JSON report emission." + ] + }, + { + "file": "crates/aprender-contracts-cli/tests/shapes_vacuity.rs", + "line": 184, + "lanes_agreeing": [ + 1, + 2 + ], + "claims": [ + "The added tests verify that pass, fail, and decline answers remain distinct (exit codes 0, 1, 2) and all three cases emit parseable reports.", + "pass/fail/decline remain distinct (0/1/2) and emit parseable reports." + ] + }, + { + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "line": 156, + "lanes_agreeing": [ + 1, + 2 + ], + "claims": [ + "Vacuity is computed per-shape before any verdict is formed.", + "Vacuity is computed per-shape before verdicts." + ] + }, + { + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "line": 159, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "Per-shape focus node counts (`focus_of`) and vacuous sets (`vacuous_any`, `vacuous_armed`) are evaluated before forming any gate verdict." + ] + }, + { + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "line": 245, + "lanes_agreeing": [ + 1, + 2 + ], + "claims": [ + "An ARMED shape at zero declines with Unknown(NoFocus) (which maps to exit 2) and is explicitly named in `declines`.", + "An ARMED shape with zero focus nodes declines with Unknown(NoFocus)." + ] + }, + { + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "line": 246, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "An armed shape grading zero focus nodes sets the verdict to `Unknown(NoFocus)` (exit code 2) while continuing stdout JSON report generation." + ] + }, + { + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "line": 260, + "lanes_agreeing": [ + 1, + 2, + 3 + ], + "claims": [ + "Vacuous shapes (armed or unarmed) are filtered out of both `armed_shapes` and `not_armed_shapes` partitions, appearing exclusively in `declines`.", + "Vacuous shapes are explicitly removed from both `armed_shapes` and `not_armed_shapes` via a filter prior to partitioning.", + "Vacuous shapes are explicitly removed from both armed_shapes and not_armed_shapes." + ] + }, + { + "file": "crates/aprender-contracts/src/lint/shapes_gate.rs", + "line": 318, + "lanes_agreeing": [ + 1, + 2, + 3 + ], + "claims": [ + "An UNARMED shape at zero is reported in `declines[]` without refusing the build.", + "Both armed and unarmed vacuous shapes are correctly reported in declines[] array.", + "Unarmed vacuous shapes do not trigger a refusal verdict but are reported in `declines[]` without swallowing the finding." + ] + } + ], + "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-3610.yaml b/docs/roadmaps/entries/PMAT-3610.yaml new file mode 100644 index 0000000000..2e2c20eedc --- /dev/null +++ b/docs/roadmaps/entries/PMAT-3610.yaml @@ -0,0 +1,17 @@ +- id: PMAT-3610 + github_issue: 3610 + item_type: task + title: 'shapes gate reported Pass over ZERO focus nodes: per-shape vacuity, not a global total' + 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#3610 done_when; see paiml-mcp-agent-toolkit#1414). The defect: NoFocus asked the question GLOBALLY (report.focus_nodes_n == 0), which is only ever true for a lone contract. In a DIRECTORY one empty shape is invisible — the others carry the total above zero, the empty one contributes no violations, and the aggregate reports Pass WHILE LISTING IT IN armed_shapes, which is the tool s claim about what it measured. Done when: vacuity is computed per-shape before any verdict is formed; an ARMED shape at zero declines (exit 2, Unknown(NoFocus), named in declines[]); an UNARMED shape at zero is REPORTED in declines[] and does not refuse; a vacuous shape appears in NEITHER armed_shapes NOR not_armed_shapes, because filing a vacuity as a policy choice is how it hid. BOTH VENUES: the lone-contract case already declined correctly, so a fix proved only there proves nothing. pass/fail/decline must stay distinct (0/1/2) and all three must still emit a parseable report with by_shape, since downstream captures stdout regardless of exit code. STOP: do not refuse whenever anything is empty — that breaks the unarmed direction. PRECEDENCE (#3622 re-review, cop ruling B, 2026-09-23): a measured violation outranks a vacuity — an armed zero-focus shape beside a violating armed shape is Fail/exit 1, with the vacuity still named in declines[]. The global NoFocus path (every shape at zero) declines with exit 2 but prints no report yet: #4100.' diff --git a/docs/roadmaps/roadmap.yaml b/docs/roadmaps/roadmap.yaml index 618b9a93ca..c620b2e62e 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-3610 + github_issue: 3610 + item_type: task + title: 'shapes gate reported Pass over ZERO focus nodes: per-shape vacuity, not a global total' + 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#3610 done_when; see paiml-mcp-agent-toolkit#1414). The defect: NoFocus asked the question GLOBALLY (report.focus_nodes_n == 0), which is only ever true for a lone contract. In a DIRECTORY one empty shape is invisible — the others carry the total above zero, the empty one contributes no violations, and the aggregate reports Pass WHILE LISTING IT IN armed_shapes, which is the tool s claim about what it measured. Done when: vacuity is computed per-shape before any verdict is formed; an ARMED shape at zero declines (exit 2, Unknown(NoFocus), named in declines[]); an UNARMED shape at zero is REPORTED in declines[] and does not refuse; a vacuous shape appears in NEITHER armed_shapes NOR not_armed_shapes, because filing a vacuity as a policy choice is how it hid. BOTH VENUES: the lone-contract case already declined correctly, so a fix proved only there proves nothing. pass/fail/decline must stay distinct (0/1/2) and all three must still emit a parseable report with by_shape, since downstream captures stdout regardless of exit code. STOP: do not refuse whenever anything is empty — that breaks the unarmed direction. PRECEDENCE (#3622 re-review, cop ruling B, 2026-09-23): a measured violation outranks a vacuity — an armed zero-focus shape beside a violating armed shape is Fail/exit 1, with the vacuity still named in declines[]. The global NoFocus path (every shape at zero) declines with exit 2 but prints no report yet: #4100.' - id: PMAT-3627 github_issue: 3627 item_type: task diff --git a/evidence/pv/3610/MEASUREMENT.md b/evidence/pv/3610/MEASUREMENT.md new file mode 100644 index 0000000000..6cea294817 --- /dev/null +++ b/evidence/pv/3610/MEASUREMENT.md @@ -0,0 +1,102 @@ +# #3610 — a shapes gate that reported Pass over zero focus nodes + +## The defect, reproduced before anything was changed + +`crates/aprender-contracts/src/lint/shapes_gate.rs`: + +```rust +if report.focus_nodes_n == 0 { + return Some(ShapesOutcome::NoFocus { shapes_n }); +} +``` + +The question is asked **globally**, so it is only ever true for a lone contract. In a **directory**, +the other shapes carry the total above zero and an empty shape is invisible. + +Fixture `tests/fixtures/ont/shapes-one-empty` — one shape with a focus node, one whose target class +nothing instantiates — on `origin/main`: + +``` +verdict: Pass violations: 0 focus_nodes_n: 1 +by_shape: ['empty-shape=0', 'tool-status=1'] +armed_shapes: ['empty-shape', 'tool-status'] <- the claim +not_armed_shapes: [] +``` + +**`armed_shapes` is the tool's claim about what it measured, and it named a shape that graded +nothing.** `by_shape` had carried `empty-shape=0` all along and nothing read it — the same *computed +but unexposed* class as #3597, one layer down, inside the gate itself. + +## After + +| case | verdict | exit | `declines` | +|---|---|---|---| +| **armed** shape at zero, in a directory | decline `NoFocus` | **2** | `["empty-shape"]`, in the stdout report | +| **armed** shape at zero **beside a violating armed shape** (`shapes-one-empty-and-violating`) | **`Fail`** | **1** | `["empty-shape"]` | +| **unarmed** shape at zero | `Pass` | 0 | `["empty-shape"]` — reported, not swallowed | +| every shape graded something (`json-ok`) | `Pass` | 0 | `[]` | +| EVERY shape at zero (`shapes-all-empty`: the global path) | decline `NoFocus` | **2** | **no report** — #4100 | + +**A measured violation outranks a vacuity** (#3622 re-review). `passed` and the armed vacuity range +over DISJOINT shapes. The first cut checked vacuity first, so a real `Fail` from one shape came out as +exit 2 because a *different* shape graded nothing. `Fail` is the bottom of the verdict lattice, so it +absorbs. The vacuity is still named in `declines`. + +The shape is named in the stdout report's `declines`. stderr carries only `decline: NoFocus`. An +earlier draft of this file quoted a stderr block naming the shape; that message was removed in the +"refusal carries its evidence" rework (69d7b7992), and the draft was not updated. + +## The refusal carries its evidence: full JSON, then exit 2 + +`slk-session-gate.sh` and the SLK bridge's self-test **capture stdout and parse it regardless of the +exit code** — pv already exits non-zero on `Fail`, so capture-then-parse is their normal path. A +refusal that printed only a bare `decline:` line would read to them as *no `by_shape`* and score +**UNMEASURED** — indistinguishable, from their side, from a broken pv. **So the fix would have turned +their gate grey on the same day it turned ours red.** + +The refusal therefore declines through the **ordinary result path** rather than short-circuiting: + +``` +$ pv lint tests/fixtures/ont/shapes-one-empty/contracts --gate shapes --format json ; echo $? +{ … "verdict": "Unknown(NoFocus)", "extra": { + "by_shape": ["empty-shape=0", "tool-status=1"], + "declines": ["empty-shape"], + "armed_shapes": ["tool-status"], + "not_armed_shapes": [] } } +decline: NoFocus # stderr +2 +``` + +**The refusal is the exit code; the report is the evidence.** A refusal that suppresses its own +evidence is the same defect as a gate that swallows a decline, seen from the other side. + +Note `not_armed_shapes: []` — the vacuous shape is in **neither** list. `armed_shapes` is the claim +about what was measured and `not_armed_shapes` means *not armed by policy*; filing a vacuity as a +policy choice is how the defect hid in the first place. + +## Why the unarmed row exists + +Without it the fix would be *"refuse whenever anything is empty"*, which is a different tool. An +unarmed shape at zero did not affect the verdict, so it is **reported** rather than refused — and +**reported rather than swallowed**, which is the half the original defect got wrong. `declines` +carries those names; a field that could only ever be empty would be decoration, which is the defect +one layer up from this one. + +## Both venues, and the mutation + +The global venue (every shape at zero) already declined, so a fix proved only there proves nothing. +The committed table covers both, and RED-turns on the defect: disabling the new per-shape check fails +`an_armed_shape_that_graded_nothing_refuses_in_a_directory` and `the_three_answers_remain_distinct`. +Checking vacuity before `!passed` again fails `a_real_violation_is_a_fail_even_beside_a_vacuous_armed_shape`, +measured at f663d39e4 (exit 2, `Unknown(NoFocus)`). + +**Correction (#3622 re-review).** The "lone-contract" tests first ran `json-missing-ref`. That fixture +exits **3** on an unreadable `entity.ref` (`ont_extract_json.rs:128`) before `decline()` is ever +consulted, so those tests held for the wrong reason. They now run `shapes-all-empty`, which exits 2 +through the real global `NoFocus` path. Its missing report is recorded, not hidden (#4100). + +## The real corpus is unaffected + +`pv lint contracts --gate {sigma,relations,shapes}` on aprender: **Pass, 0 violations**, every armed +shape with focus nodes (`ladder-measured=8`, `ladder-green=7`, `ont-shapes-v1=1734`), `declines: []`. +The fix refuses the vacuous case and nothing else. diff --git a/scripts/tree_reader_tests.txt b/scripts/tree_reader_tests.txt index e93a263eb2..1990798081 100644 --- a/scripts/tree_reader_tests.txt +++ b/scripts/tree_reader_tests.txt @@ -74,6 +74,7 @@ aprender-contracts-cli --test ont_entity_properties aprender-contracts-cli --test ont_extract_json aprender-contracts-cli --test pv_surface_gate aprender-contracts-cli --test pvl_zero_contracts +aprender-contracts-cli --test shapes_vacuity aprender-core --lib format::metadata_bounds_contract_falsify aprender-core --lib format::model_family_loader aprender-core --lib format::ship_001 diff --git a/tests/fixtures/ont/shapes-all-empty/contracts/empty-shape.yaml b/tests/fixtures/ont/shapes-all-empty/contracts/empty-shape.yaml new file mode 100644 index 0000000000..9d0837f06e --- /dev/null +++ b/tests/fixtures/ont/shapes-all-empty/contracts/empty-shape.yaml @@ -0,0 +1,16 @@ +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: fixture + description: "#3610 fixture — the ONLY shape, and nothing instantiates its target class: the global NoFocus path" +name: empty-shape +version: "1.0.0" +scope: fixture +status: active +shape: + targetClass: ghost:Nothing + closed: true + properties: + - {path: ghost:must_exist, minCount: 1, maxCount: 1, datatype: xsd:string} diff --git a/tests/fixtures/ont/shapes-all-empty/contracts/ontology.yaml b/tests/fixtures/ont/shapes-all-empty/contracts/ontology.yaml new file mode 100644 index 0000000000..cee5fd4d6b --- /dev/null +++ b/tests/fixtures/ont/shapes-all-empty/contracts/ontology.yaml @@ -0,0 +1,163 @@ +# Σ — the ontology's own declaration (ONT-001 v4.4 §4.1, row ONT-2b, PMAT-3471). +# +# WHAT THIS FILE IS. Everything the corpus is allowed to say: the concepts, the roles a `relations:` block may use, +# the symbols a `formal:` expression may carry, the worlds, the agents, the entity types and the extractors that read +# them, and the keys the ontology deliberately cannot express. `pv lint --gate sigma` reads it; nothing else may. +# +# EVERY KEY NAMES ITS READER. `readers:` below claims each populated key, and a key no reader claims is exit 3 — +# ONT-1's lesson, in the file that would otherwise repeat it: an anchor nothing reads is decoration. +# +# THE SYMBOL VOCABULARY IS MEASURED, NOT INVENTED. It was taken from the 2330 `formal:` expressions in 489 contract +# files at f30c67de3: `∀` 275, `∧` 134, `∈` 116, `→` 72, `⟹` 63, `≥` 52, `≤` 42, `ε` 34, `≠` 27, `⇒` 24, `¬` 21, +# and the function names `len`, `shape`, `isFinite`, `modifies`, `preserves` that the kernel contracts actually use. +# Most of those 2330 expressions are PROSE, not notation — the ten most frequent identifiers in them are `for`, `x`, +# `all`, `in`, `i`, `and`, `t`, `forall`, `s`, `p`. That debt is counted in `lint-baseline.json.formal_prose` and +# shrinks; it is not declared away here by adding English words to `symbols`. +schema: ont-sigma-v1 + +concepts: + Entity: {doc: "anything the ontology can name"} + Contract: {doc: "a pv contract file under contracts/"} + Kernel: {doc: "a contract whose kind is kernel: it carries equations and proof obligations"} + Code: {doc: "a Rust item — a function, type or module — in this workspace"} + Test: {doc: "a test function a contract cites as its falsifier"} + Proof: {doc: "a Kani harness or Lean theorem discharging an obligation"} + Doc: {doc: "a prose document under contract (README.md, CLAUDE.md)"} + Model: {doc: "an .apr model file"} + Dataset: {doc: "a CSV or corpus file"} + +roles: + binds: + {domain: Contract, range: Code, symmetric: false, acyclic: false, doc: "the contract governs this code"} + falsified_by: + {domain: Contract, range: Test, symmetric: false, acyclic: false, doc: "the test that would refute the contract"} + proved_by: + {domain: Contract, range: Proof, symmetric: false, acyclic: false, doc: "the harness or theorem discharging it"} + refines: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "a stricter contract over the same subject"} + depends_on: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract assumes that one"} + documents: + {domain: Doc, range: Code, symmetric: false, acyclic: false, doc: "the prose that describes this code"} + supersedes: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract replaces that one; a chain, never a loop (ONT-4)"} + contradicts: + {domain: Contract, range: Contract, symmetric: true, acyclic: false, doc: "the two cannot both hold; declared once, read both ways (ONT-4)"} + +# Operators and functions a `formal:` expression may carry. A bare variable (x, i, out_i, θ) is not a symbol and is +# not checked — see the plan's ruling 2 for what symbol-level deliberately does NOT check. +symbols: + - {name: "∀", kind: operator, doc: "for all"} + - {name: "∃", kind: operator, doc: "there exists"} + - {name: "∧", kind: operator, doc: "and"} + - {name: "∨", kind: operator, doc: "or"} + - {name: "¬", kind: operator, doc: "not"} + - {name: "⇒", kind: operator, doc: "implies"} + - {name: "⟹", kind: operator, doc: "implies (long)"} + - {name: "→", kind: operator, doc: "maps to"} + - {name: "≡", kind: operator, doc: "identical to"} + - {name: "≈", kind: operator, doc: "approximately equal"} + - {name: "≠", kind: operator, doc: "not equal"} + - {name: "≥", kind: operator, doc: "greater or equal"} + - {name: "≤", kind: operator, doc: "less or equal"} + - {name: "∈", kind: operator, doc: "member of"} + - {name: "∉", kind: operator, doc: "not a member of"} + - {name: "⊆", kind: operator, doc: "subset of"} + - {name: "∪", kind: operator, doc: "union"} + - {name: "∩", kind: operator, doc: "intersection"} + - {name: "∅", kind: constant, doc: "the empty set"} + - {name: "·", kind: operator, doc: "product"} + - {name: "×", kind: operator, doc: "cartesian product or multiplication"} + - {name: "‖", kind: operator, doc: "norm delimiter"} + - {name: "Σ", kind: operator, doc: "sum"} + - {name: "ε", kind: constant, doc: "the tolerance a contract declares"} + - {name: len, kind: function, doc: "length of a sequence"} + - {name: shape, kind: function, doc: "tensor shape"} + - {name: isFinite, kind: predicate, doc: "neither NaN nor infinite"} + - {name: isNaN, kind: predicate, doc: "is NaN"} + - {name: modifies, kind: predicate, doc: "frame condition: what the kernel writes"} + - {name: preserves, kind: predicate, doc: "frame condition: what the kernel leaves alone"} + - {name: max, kind: function, doc: "maximum"} + - {name: min, kind: function, doc: "minimum"} + - {name: abs, kind: function, doc: "absolute value"} + - {name: exp, kind: function, doc: "exponential"} + - {name: log, kind: function, doc: "logarithm"} + - {name: sqrt, kind: function, doc: "square root"} + - {name: sum, kind: function, doc: "sum of a sequence"} + - {name: mod, kind: operator, doc: "modulo"} + # Measured from the corpus after the first pass: 79 expressions in 51 files carried an operator Σ did not yet + # declare. Every one below is real notation and is declared; the two glyphs deliberately left OUT are `—` and `§`, + # which are prose punctuation — the entries carrying those say `prose: true` instead. + - {name: "²", kind: operator, doc: "squared"} + - {name: "¹", kind: operator, doc: "to the first power"} + - {name: "₁", kind: operator, doc: "subscript one"} + - {name: "₂", kind: operator, doc: "subscript two"} + - {name: "√", kind: function, doc: "square root"} + - {name: "∞", kind: constant, doc: "infinity"} + - {name: "⊥", kind: constant, doc: "bottom — undefined or unreachable"} + - {name: "∘", kind: operator, doc: "function composition"} + - {name: "∋", kind: operator, doc: "contains"} + - {name: "∌", kind: operator, doc: "does not contain"} + - {name: "⊇", kind: operator, doc: "superset of"} + - {name: "⊄", kind: operator, doc: "not a subset of"} + - {name: "−", kind: operator, doc: "minus (U+2212)"} + - {name: "↔", kind: operator, doc: "if and only if"} + - {name: "⟺", kind: operator, doc: "if and only if (long)"} + - {name: "≺", kind: operator, doc: "precedes"} + - {name: "±", kind: operator, doc: "plus or minus"} + - {name: "⟨", kind: operator, doc: "inner-product open"} + - {name: "⟩", kind: operator, doc: "inner-product close"} + - {name: "∇", kind: operator, doc: "gradient"} + - {name: "∂", kind: operator, doc: "partial derivative"} + - {name: "⌈", kind: operator, doc: "ceiling open"} + - {name: "⌉", kind: operator, doc: "ceiling close"} + - {name: "′", kind: operator, doc: "prime"} + - {name: "̄", kind: operator, doc: "combining macron — the mean of a variable"} + - {name: "₀", kind: operator, doc: "subscript zero"} + - {name: "⋃", kind: operator, doc: "n-ary union"} + - {name: "←", kind: operator, doc: "assignment"} + +worlds: + committed: {doc: "the tree as committed — the world every contract is read in unless it says otherwise"} + +agents: + - pv + - pmat + - human + +# Each entry names the extractor that reads it. `implemented: false` is the honest state until ONT-4b/4c build them; +# an entry naming NO extractor, or one extractors[] does not declare, is exit 3. +entity_types: + - {name: pv-contract, extractor: pv_contract, implemented: false} + - {name: code, extractor: code, implemented: false} + - {name: lean, extractor: lean, implemented: false} + - {name: readme, extractor: readme, implemented: false} + - {name: llm-context, extractor: llm_context, implemented: false} + - {name: apr-model, extractor: apr_model, implemented: false} + - {name: csv, extractor: csv, implemented: false} + +extractors: + - {name: pv_contract, reader: ontology/extract/pv_contract.rs, implemented: false} + - {name: code, reader: ontology/extract/code.rs, implemented: false} + - {name: lean, reader: ontology/extract/lean.rs, implemented: false} + - {name: readme, reader: ontology/extract/readme.rs, implemented: false} + - {name: llm_context, reader: ontology/extract/llm_context.rs, implemented: false} + - {name: apr_model, reader: ontology/extract/apr_model.rs, implemented: false} + - {name: csv, reader: ontology/extract/csv.rs, implemented: false} + +# What this ontology does NOT express, said out loud so nobody encodes it by accident. Each names the reader that +# would have to change first. +not_expressible: + - {key: taste, reader: ontology/sigma.rs} + - {key: urgency, reader: ontology/sigma.rs} + - {key: authorship_intent, reader: ontology/sigma.rs} + +readers: + concepts: ontology/sigma.rs + roles: lint/sigma_gate.rs, lint/relations_gate.rs + symbols: lint/sigma_symbols.rs + worlds: ontology/sigma.rs + agents: ontology/sigma.rs + entity_types: lint/sigma_gate.rs + extractors: ontology/sigma.rs + not_expressible: ontology/sigma.rs diff --git a/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/empty-shape.yaml b/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/empty-shape.yaml new file mode 100644 index 0000000000..a199254c2b --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/empty-shape.yaml @@ -0,0 +1,16 @@ +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: fixture + description: "#3610 fixture — a shape whose target class NOTHING instantiates, beside one whose focus node VIOLATES it" +name: empty-shape +version: "1.0.0" +scope: fixture +status: active +shape: + targetClass: ghost:Nothing + closed: true + properties: + - {path: ghost:must_exist, minCount: 1, maxCount: 1, datatype: xsd:string} diff --git a/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/ontology.yaml b/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/ontology.yaml new file mode 100644 index 0000000000..cee5fd4d6b --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/ontology.yaml @@ -0,0 +1,163 @@ +# Σ — the ontology's own declaration (ONT-001 v4.4 §4.1, row ONT-2b, PMAT-3471). +# +# WHAT THIS FILE IS. Everything the corpus is allowed to say: the concepts, the roles a `relations:` block may use, +# the symbols a `formal:` expression may carry, the worlds, the agents, the entity types and the extractors that read +# them, and the keys the ontology deliberately cannot express. `pv lint --gate sigma` reads it; nothing else may. +# +# EVERY KEY NAMES ITS READER. `readers:` below claims each populated key, and a key no reader claims is exit 3 — +# ONT-1's lesson, in the file that would otherwise repeat it: an anchor nothing reads is decoration. +# +# THE SYMBOL VOCABULARY IS MEASURED, NOT INVENTED. It was taken from the 2330 `formal:` expressions in 489 contract +# files at f30c67de3: `∀` 275, `∧` 134, `∈` 116, `→` 72, `⟹` 63, `≥` 52, `≤` 42, `ε` 34, `≠` 27, `⇒` 24, `¬` 21, +# and the function names `len`, `shape`, `isFinite`, `modifies`, `preserves` that the kernel contracts actually use. +# Most of those 2330 expressions are PROSE, not notation — the ten most frequent identifiers in them are `for`, `x`, +# `all`, `in`, `i`, `and`, `t`, `forall`, `s`, `p`. That debt is counted in `lint-baseline.json.formal_prose` and +# shrinks; it is not declared away here by adding English words to `symbols`. +schema: ont-sigma-v1 + +concepts: + Entity: {doc: "anything the ontology can name"} + Contract: {doc: "a pv contract file under contracts/"} + Kernel: {doc: "a contract whose kind is kernel: it carries equations and proof obligations"} + Code: {doc: "a Rust item — a function, type or module — in this workspace"} + Test: {doc: "a test function a contract cites as its falsifier"} + Proof: {doc: "a Kani harness or Lean theorem discharging an obligation"} + Doc: {doc: "a prose document under contract (README.md, CLAUDE.md)"} + Model: {doc: "an .apr model file"} + Dataset: {doc: "a CSV or corpus file"} + +roles: + binds: + {domain: Contract, range: Code, symmetric: false, acyclic: false, doc: "the contract governs this code"} + falsified_by: + {domain: Contract, range: Test, symmetric: false, acyclic: false, doc: "the test that would refute the contract"} + proved_by: + {domain: Contract, range: Proof, symmetric: false, acyclic: false, doc: "the harness or theorem discharging it"} + refines: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "a stricter contract over the same subject"} + depends_on: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract assumes that one"} + documents: + {domain: Doc, range: Code, symmetric: false, acyclic: false, doc: "the prose that describes this code"} + supersedes: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract replaces that one; a chain, never a loop (ONT-4)"} + contradicts: + {domain: Contract, range: Contract, symmetric: true, acyclic: false, doc: "the two cannot both hold; declared once, read both ways (ONT-4)"} + +# Operators and functions a `formal:` expression may carry. A bare variable (x, i, out_i, θ) is not a symbol and is +# not checked — see the plan's ruling 2 for what symbol-level deliberately does NOT check. +symbols: + - {name: "∀", kind: operator, doc: "for all"} + - {name: "∃", kind: operator, doc: "there exists"} + - {name: "∧", kind: operator, doc: "and"} + - {name: "∨", kind: operator, doc: "or"} + - {name: "¬", kind: operator, doc: "not"} + - {name: "⇒", kind: operator, doc: "implies"} + - {name: "⟹", kind: operator, doc: "implies (long)"} + - {name: "→", kind: operator, doc: "maps to"} + - {name: "≡", kind: operator, doc: "identical to"} + - {name: "≈", kind: operator, doc: "approximately equal"} + - {name: "≠", kind: operator, doc: "not equal"} + - {name: "≥", kind: operator, doc: "greater or equal"} + - {name: "≤", kind: operator, doc: "less or equal"} + - {name: "∈", kind: operator, doc: "member of"} + - {name: "∉", kind: operator, doc: "not a member of"} + - {name: "⊆", kind: operator, doc: "subset of"} + - {name: "∪", kind: operator, doc: "union"} + - {name: "∩", kind: operator, doc: "intersection"} + - {name: "∅", kind: constant, doc: "the empty set"} + - {name: "·", kind: operator, doc: "product"} + - {name: "×", kind: operator, doc: "cartesian product or multiplication"} + - {name: "‖", kind: operator, doc: "norm delimiter"} + - {name: "Σ", kind: operator, doc: "sum"} + - {name: "ε", kind: constant, doc: "the tolerance a contract declares"} + - {name: len, kind: function, doc: "length of a sequence"} + - {name: shape, kind: function, doc: "tensor shape"} + - {name: isFinite, kind: predicate, doc: "neither NaN nor infinite"} + - {name: isNaN, kind: predicate, doc: "is NaN"} + - {name: modifies, kind: predicate, doc: "frame condition: what the kernel writes"} + - {name: preserves, kind: predicate, doc: "frame condition: what the kernel leaves alone"} + - {name: max, kind: function, doc: "maximum"} + - {name: min, kind: function, doc: "minimum"} + - {name: abs, kind: function, doc: "absolute value"} + - {name: exp, kind: function, doc: "exponential"} + - {name: log, kind: function, doc: "logarithm"} + - {name: sqrt, kind: function, doc: "square root"} + - {name: sum, kind: function, doc: "sum of a sequence"} + - {name: mod, kind: operator, doc: "modulo"} + # Measured from the corpus after the first pass: 79 expressions in 51 files carried an operator Σ did not yet + # declare. Every one below is real notation and is declared; the two glyphs deliberately left OUT are `—` and `§`, + # which are prose punctuation — the entries carrying those say `prose: true` instead. + - {name: "²", kind: operator, doc: "squared"} + - {name: "¹", kind: operator, doc: "to the first power"} + - {name: "₁", kind: operator, doc: "subscript one"} + - {name: "₂", kind: operator, doc: "subscript two"} + - {name: "√", kind: function, doc: "square root"} + - {name: "∞", kind: constant, doc: "infinity"} + - {name: "⊥", kind: constant, doc: "bottom — undefined or unreachable"} + - {name: "∘", kind: operator, doc: "function composition"} + - {name: "∋", kind: operator, doc: "contains"} + - {name: "∌", kind: operator, doc: "does not contain"} + - {name: "⊇", kind: operator, doc: "superset of"} + - {name: "⊄", kind: operator, doc: "not a subset of"} + - {name: "−", kind: operator, doc: "minus (U+2212)"} + - {name: "↔", kind: operator, doc: "if and only if"} + - {name: "⟺", kind: operator, doc: "if and only if (long)"} + - {name: "≺", kind: operator, doc: "precedes"} + - {name: "±", kind: operator, doc: "plus or minus"} + - {name: "⟨", kind: operator, doc: "inner-product open"} + - {name: "⟩", kind: operator, doc: "inner-product close"} + - {name: "∇", kind: operator, doc: "gradient"} + - {name: "∂", kind: operator, doc: "partial derivative"} + - {name: "⌈", kind: operator, doc: "ceiling open"} + - {name: "⌉", kind: operator, doc: "ceiling close"} + - {name: "′", kind: operator, doc: "prime"} + - {name: "̄", kind: operator, doc: "combining macron — the mean of a variable"} + - {name: "₀", kind: operator, doc: "subscript zero"} + - {name: "⋃", kind: operator, doc: "n-ary union"} + - {name: "←", kind: operator, doc: "assignment"} + +worlds: + committed: {doc: "the tree as committed — the world every contract is read in unless it says otherwise"} + +agents: + - pv + - pmat + - human + +# Each entry names the extractor that reads it. `implemented: false` is the honest state until ONT-4b/4c build them; +# an entry naming NO extractor, or one extractors[] does not declare, is exit 3. +entity_types: + - {name: pv-contract, extractor: pv_contract, implemented: false} + - {name: code, extractor: code, implemented: false} + - {name: lean, extractor: lean, implemented: false} + - {name: readme, extractor: readme, implemented: false} + - {name: llm-context, extractor: llm_context, implemented: false} + - {name: apr-model, extractor: apr_model, implemented: false} + - {name: csv, extractor: csv, implemented: false} + +extractors: + - {name: pv_contract, reader: ontology/extract/pv_contract.rs, implemented: false} + - {name: code, reader: ontology/extract/code.rs, implemented: false} + - {name: lean, reader: ontology/extract/lean.rs, implemented: false} + - {name: readme, reader: ontology/extract/readme.rs, implemented: false} + - {name: llm_context, reader: ontology/extract/llm_context.rs, implemented: false} + - {name: apr_model, reader: ontology/extract/apr_model.rs, implemented: false} + - {name: csv, reader: ontology/extract/csv.rs, implemented: false} + +# What this ontology does NOT express, said out loud so nobody encodes it by accident. Each names the reader that +# would have to change first. +not_expressible: + - {key: taste, reader: ontology/sigma.rs} + - {key: urgency, reader: ontology/sigma.rs} + - {key: authorship_intent, reader: ontology/sigma.rs} + +readers: + concepts: ontology/sigma.rs + roles: lint/sigma_gate.rs, lint/relations_gate.rs + symbols: lint/sigma_symbols.rs + worlds: ontology/sigma.rs + agents: ontology/sigma.rs + entity_types: lint/sigma_gate.rs + extractors: ontology/sigma.rs + not_expressible: ontology/sigma.rs diff --git a/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/tool-status.yaml b/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/tool-status.yaml new file mode 100644 index 0000000000..8025269b50 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-and-violating/contracts/tool-status.yaml @@ -0,0 +1,33 @@ +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-19' + last_modified: '2026-09-19' + author: fixture + description: fixture — a tool's --json output as a shaped entity (extract:json) +name: tool-status +version: "1.0.0" +scope: fixture +status: active +entity: + type: json + ref: data/status.json +vocabulary: + prefix: tool + root_class: tool:Status + nested: + push: tool:Push + findings: tool:Finding +shape: + targetClass: tool:Status + closed: true + properties: + - {path: tool:schema, minCount: 1, maxCount: 1, in: ["tool/status-v1"]} + - {path: tool:ok, minCount: 1, maxCount: 1, datatype: xsd:boolean} + - {path: tool:push, minCount: 1, maxCount: 1, node: {closed: true, properties: [ + {path: tool:state, minCount: 1, maxCount: 1, in: [ok, failing, never]}, + {path: tool:attempts, minCount: 1, maxCount: 1, datatype: xsd:integer}]}} + - {path: tool:findings, node: {closed: true, properties: [ + {path: tool:sensor, minCount: 1, maxCount: 1, datatype: xsd:string}, + {path: tool:open, minCount: 1, maxCount: 1, datatype: xsd:integer}]}} + diff --git a/tests/fixtures/ont/shapes-one-empty-and-violating/data/status.json b/tests/fixtures/ont/shapes-one-empty-and-violating/data/status.json new file mode 100644 index 0000000000..ac3de35238 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-and-violating/data/status.json @@ -0,0 +1 @@ +{"schema":"tool/status-v1","ok":true,"surprise":"undeclared","push":{"state":"broken","attempts":0},"findings":[]} diff --git a/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/empty-shape.yaml b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/empty-shape.yaml new file mode 100644 index 0000000000..5ca7a7ad61 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/empty-shape.yaml @@ -0,0 +1,16 @@ +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: fixture + description: "#3610 fixture — a shape whose target class NOTHING instantiates, beside one that has focus nodes" +name: empty-shape +version: "1.0.0" +scope: fixture +status: active +shape: + targetClass: ghost:Nothing + closed: true + properties: + - {path: ghost:must_exist, minCount: 1, maxCount: 1, datatype: xsd:string} diff --git a/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/lint-baseline.json b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/lint-baseline.json new file mode 100644 index 0000000000..e31a67ecf8 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/lint-baseline.json @@ -0,0 +1,3 @@ +{ + "armed_shapes": ["tool-status"] +} diff --git a/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/ontology.yaml b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/ontology.yaml new file mode 100644 index 0000000000..cee5fd4d6b --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/ontology.yaml @@ -0,0 +1,163 @@ +# Σ — the ontology's own declaration (ONT-001 v4.4 §4.1, row ONT-2b, PMAT-3471). +# +# WHAT THIS FILE IS. Everything the corpus is allowed to say: the concepts, the roles a `relations:` block may use, +# the symbols a `formal:` expression may carry, the worlds, the agents, the entity types and the extractors that read +# them, and the keys the ontology deliberately cannot express. `pv lint --gate sigma` reads it; nothing else may. +# +# EVERY KEY NAMES ITS READER. `readers:` below claims each populated key, and a key no reader claims is exit 3 — +# ONT-1's lesson, in the file that would otherwise repeat it: an anchor nothing reads is decoration. +# +# THE SYMBOL VOCABULARY IS MEASURED, NOT INVENTED. It was taken from the 2330 `formal:` expressions in 489 contract +# files at f30c67de3: `∀` 275, `∧` 134, `∈` 116, `→` 72, `⟹` 63, `≥` 52, `≤` 42, `ε` 34, `≠` 27, `⇒` 24, `¬` 21, +# and the function names `len`, `shape`, `isFinite`, `modifies`, `preserves` that the kernel contracts actually use. +# Most of those 2330 expressions are PROSE, not notation — the ten most frequent identifiers in them are `for`, `x`, +# `all`, `in`, `i`, `and`, `t`, `forall`, `s`, `p`. That debt is counted in `lint-baseline.json.formal_prose` and +# shrinks; it is not declared away here by adding English words to `symbols`. +schema: ont-sigma-v1 + +concepts: + Entity: {doc: "anything the ontology can name"} + Contract: {doc: "a pv contract file under contracts/"} + Kernel: {doc: "a contract whose kind is kernel: it carries equations and proof obligations"} + Code: {doc: "a Rust item — a function, type or module — in this workspace"} + Test: {doc: "a test function a contract cites as its falsifier"} + Proof: {doc: "a Kani harness or Lean theorem discharging an obligation"} + Doc: {doc: "a prose document under contract (README.md, CLAUDE.md)"} + Model: {doc: "an .apr model file"} + Dataset: {doc: "a CSV or corpus file"} + +roles: + binds: + {domain: Contract, range: Code, symmetric: false, acyclic: false, doc: "the contract governs this code"} + falsified_by: + {domain: Contract, range: Test, symmetric: false, acyclic: false, doc: "the test that would refute the contract"} + proved_by: + {domain: Contract, range: Proof, symmetric: false, acyclic: false, doc: "the harness or theorem discharging it"} + refines: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "a stricter contract over the same subject"} + depends_on: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract assumes that one"} + documents: + {domain: Doc, range: Code, symmetric: false, acyclic: false, doc: "the prose that describes this code"} + supersedes: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract replaces that one; a chain, never a loop (ONT-4)"} + contradicts: + {domain: Contract, range: Contract, symmetric: true, acyclic: false, doc: "the two cannot both hold; declared once, read both ways (ONT-4)"} + +# Operators and functions a `formal:` expression may carry. A bare variable (x, i, out_i, θ) is not a symbol and is +# not checked — see the plan's ruling 2 for what symbol-level deliberately does NOT check. +symbols: + - {name: "∀", kind: operator, doc: "for all"} + - {name: "∃", kind: operator, doc: "there exists"} + - {name: "∧", kind: operator, doc: "and"} + - {name: "∨", kind: operator, doc: "or"} + - {name: "¬", kind: operator, doc: "not"} + - {name: "⇒", kind: operator, doc: "implies"} + - {name: "⟹", kind: operator, doc: "implies (long)"} + - {name: "→", kind: operator, doc: "maps to"} + - {name: "≡", kind: operator, doc: "identical to"} + - {name: "≈", kind: operator, doc: "approximately equal"} + - {name: "≠", kind: operator, doc: "not equal"} + - {name: "≥", kind: operator, doc: "greater or equal"} + - {name: "≤", kind: operator, doc: "less or equal"} + - {name: "∈", kind: operator, doc: "member of"} + - {name: "∉", kind: operator, doc: "not a member of"} + - {name: "⊆", kind: operator, doc: "subset of"} + - {name: "∪", kind: operator, doc: "union"} + - {name: "∩", kind: operator, doc: "intersection"} + - {name: "∅", kind: constant, doc: "the empty set"} + - {name: "·", kind: operator, doc: "product"} + - {name: "×", kind: operator, doc: "cartesian product or multiplication"} + - {name: "‖", kind: operator, doc: "norm delimiter"} + - {name: "Σ", kind: operator, doc: "sum"} + - {name: "ε", kind: constant, doc: "the tolerance a contract declares"} + - {name: len, kind: function, doc: "length of a sequence"} + - {name: shape, kind: function, doc: "tensor shape"} + - {name: isFinite, kind: predicate, doc: "neither NaN nor infinite"} + - {name: isNaN, kind: predicate, doc: "is NaN"} + - {name: modifies, kind: predicate, doc: "frame condition: what the kernel writes"} + - {name: preserves, kind: predicate, doc: "frame condition: what the kernel leaves alone"} + - {name: max, kind: function, doc: "maximum"} + - {name: min, kind: function, doc: "minimum"} + - {name: abs, kind: function, doc: "absolute value"} + - {name: exp, kind: function, doc: "exponential"} + - {name: log, kind: function, doc: "logarithm"} + - {name: sqrt, kind: function, doc: "square root"} + - {name: sum, kind: function, doc: "sum of a sequence"} + - {name: mod, kind: operator, doc: "modulo"} + # Measured from the corpus after the first pass: 79 expressions in 51 files carried an operator Σ did not yet + # declare. Every one below is real notation and is declared; the two glyphs deliberately left OUT are `—` and `§`, + # which are prose punctuation — the entries carrying those say `prose: true` instead. + - {name: "²", kind: operator, doc: "squared"} + - {name: "¹", kind: operator, doc: "to the first power"} + - {name: "₁", kind: operator, doc: "subscript one"} + - {name: "₂", kind: operator, doc: "subscript two"} + - {name: "√", kind: function, doc: "square root"} + - {name: "∞", kind: constant, doc: "infinity"} + - {name: "⊥", kind: constant, doc: "bottom — undefined or unreachable"} + - {name: "∘", kind: operator, doc: "function composition"} + - {name: "∋", kind: operator, doc: "contains"} + - {name: "∌", kind: operator, doc: "does not contain"} + - {name: "⊇", kind: operator, doc: "superset of"} + - {name: "⊄", kind: operator, doc: "not a subset of"} + - {name: "−", kind: operator, doc: "minus (U+2212)"} + - {name: "↔", kind: operator, doc: "if and only if"} + - {name: "⟺", kind: operator, doc: "if and only if (long)"} + - {name: "≺", kind: operator, doc: "precedes"} + - {name: "±", kind: operator, doc: "plus or minus"} + - {name: "⟨", kind: operator, doc: "inner-product open"} + - {name: "⟩", kind: operator, doc: "inner-product close"} + - {name: "∇", kind: operator, doc: "gradient"} + - {name: "∂", kind: operator, doc: "partial derivative"} + - {name: "⌈", kind: operator, doc: "ceiling open"} + - {name: "⌉", kind: operator, doc: "ceiling close"} + - {name: "′", kind: operator, doc: "prime"} + - {name: "̄", kind: operator, doc: "combining macron — the mean of a variable"} + - {name: "₀", kind: operator, doc: "subscript zero"} + - {name: "⋃", kind: operator, doc: "n-ary union"} + - {name: "←", kind: operator, doc: "assignment"} + +worlds: + committed: {doc: "the tree as committed — the world every contract is read in unless it says otherwise"} + +agents: + - pv + - pmat + - human + +# Each entry names the extractor that reads it. `implemented: false` is the honest state until ONT-4b/4c build them; +# an entry naming NO extractor, or one extractors[] does not declare, is exit 3. +entity_types: + - {name: pv-contract, extractor: pv_contract, implemented: false} + - {name: code, extractor: code, implemented: false} + - {name: lean, extractor: lean, implemented: false} + - {name: readme, extractor: readme, implemented: false} + - {name: llm-context, extractor: llm_context, implemented: false} + - {name: apr-model, extractor: apr_model, implemented: false} + - {name: csv, extractor: csv, implemented: false} + +extractors: + - {name: pv_contract, reader: ontology/extract/pv_contract.rs, implemented: false} + - {name: code, reader: ontology/extract/code.rs, implemented: false} + - {name: lean, reader: ontology/extract/lean.rs, implemented: false} + - {name: readme, reader: ontology/extract/readme.rs, implemented: false} + - {name: llm_context, reader: ontology/extract/llm_context.rs, implemented: false} + - {name: apr_model, reader: ontology/extract/apr_model.rs, implemented: false} + - {name: csv, reader: ontology/extract/csv.rs, implemented: false} + +# What this ontology does NOT express, said out loud so nobody encodes it by accident. Each names the reader that +# would have to change first. +not_expressible: + - {key: taste, reader: ontology/sigma.rs} + - {key: urgency, reader: ontology/sigma.rs} + - {key: authorship_intent, reader: ontology/sigma.rs} + +readers: + concepts: ontology/sigma.rs + roles: lint/sigma_gate.rs, lint/relations_gate.rs + symbols: lint/sigma_symbols.rs + worlds: ontology/sigma.rs + agents: ontology/sigma.rs + entity_types: lint/sigma_gate.rs + extractors: ontology/sigma.rs + not_expressible: ontology/sigma.rs diff --git a/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/tool-status.yaml b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/tool-status.yaml new file mode 100644 index 0000000000..8025269b50 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-unarmed/contracts/tool-status.yaml @@ -0,0 +1,33 @@ +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-19' + last_modified: '2026-09-19' + author: fixture + description: fixture — a tool's --json output as a shaped entity (extract:json) +name: tool-status +version: "1.0.0" +scope: fixture +status: active +entity: + type: json + ref: data/status.json +vocabulary: + prefix: tool + root_class: tool:Status + nested: + push: tool:Push + findings: tool:Finding +shape: + targetClass: tool:Status + closed: true + properties: + - {path: tool:schema, minCount: 1, maxCount: 1, in: ["tool/status-v1"]} + - {path: tool:ok, minCount: 1, maxCount: 1, datatype: xsd:boolean} + - {path: tool:push, minCount: 1, maxCount: 1, node: {closed: true, properties: [ + {path: tool:state, minCount: 1, maxCount: 1, in: [ok, failing, never]}, + {path: tool:attempts, minCount: 1, maxCount: 1, datatype: xsd:integer}]}} + - {path: tool:findings, node: {closed: true, properties: [ + {path: tool:sensor, minCount: 1, maxCount: 1, datatype: xsd:string}, + {path: tool:open, minCount: 1, maxCount: 1, datatype: xsd:integer}]}} + diff --git a/tests/fixtures/ont/shapes-one-empty-unarmed/data/status.json b/tests/fixtures/ont/shapes-one-empty-unarmed/data/status.json new file mode 100644 index 0000000000..3ca2851700 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty-unarmed/data/status.json @@ -0,0 +1 @@ +{"schema":"tool/status-v1","ok":true,"push":{"state":"ok","attempts":0},"findings":[{"sensor":"s-self","open":1},{"sensor":"s-drift","open":0}]} diff --git a/tests/fixtures/ont/shapes-one-empty/contracts/empty-shape.yaml b/tests/fixtures/ont/shapes-one-empty/contracts/empty-shape.yaml new file mode 100644 index 0000000000..5ca7a7ad61 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty/contracts/empty-shape.yaml @@ -0,0 +1,16 @@ +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-20' + last_modified: '2026-09-20' + author: fixture + description: "#3610 fixture — a shape whose target class NOTHING instantiates, beside one that has focus nodes" +name: empty-shape +version: "1.0.0" +scope: fixture +status: active +shape: + targetClass: ghost:Nothing + closed: true + properties: + - {path: ghost:must_exist, minCount: 1, maxCount: 1, datatype: xsd:string} diff --git a/tests/fixtures/ont/shapes-one-empty/contracts/ontology.yaml b/tests/fixtures/ont/shapes-one-empty/contracts/ontology.yaml new file mode 100644 index 0000000000..cee5fd4d6b --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty/contracts/ontology.yaml @@ -0,0 +1,163 @@ +# Σ — the ontology's own declaration (ONT-001 v4.4 §4.1, row ONT-2b, PMAT-3471). +# +# WHAT THIS FILE IS. Everything the corpus is allowed to say: the concepts, the roles a `relations:` block may use, +# the symbols a `formal:` expression may carry, the worlds, the agents, the entity types and the extractors that read +# them, and the keys the ontology deliberately cannot express. `pv lint --gate sigma` reads it; nothing else may. +# +# EVERY KEY NAMES ITS READER. `readers:` below claims each populated key, and a key no reader claims is exit 3 — +# ONT-1's lesson, in the file that would otherwise repeat it: an anchor nothing reads is decoration. +# +# THE SYMBOL VOCABULARY IS MEASURED, NOT INVENTED. It was taken from the 2330 `formal:` expressions in 489 contract +# files at f30c67de3: `∀` 275, `∧` 134, `∈` 116, `→` 72, `⟹` 63, `≥` 52, `≤` 42, `ε` 34, `≠` 27, `⇒` 24, `¬` 21, +# and the function names `len`, `shape`, `isFinite`, `modifies`, `preserves` that the kernel contracts actually use. +# Most of those 2330 expressions are PROSE, not notation — the ten most frequent identifiers in them are `for`, `x`, +# `all`, `in`, `i`, `and`, `t`, `forall`, `s`, `p`. That debt is counted in `lint-baseline.json.formal_prose` and +# shrinks; it is not declared away here by adding English words to `symbols`. +schema: ont-sigma-v1 + +concepts: + Entity: {doc: "anything the ontology can name"} + Contract: {doc: "a pv contract file under contracts/"} + Kernel: {doc: "a contract whose kind is kernel: it carries equations and proof obligations"} + Code: {doc: "a Rust item — a function, type or module — in this workspace"} + Test: {doc: "a test function a contract cites as its falsifier"} + Proof: {doc: "a Kani harness or Lean theorem discharging an obligation"} + Doc: {doc: "a prose document under contract (README.md, CLAUDE.md)"} + Model: {doc: "an .apr model file"} + Dataset: {doc: "a CSV or corpus file"} + +roles: + binds: + {domain: Contract, range: Code, symmetric: false, acyclic: false, doc: "the contract governs this code"} + falsified_by: + {domain: Contract, range: Test, symmetric: false, acyclic: false, doc: "the test that would refute the contract"} + proved_by: + {domain: Contract, range: Proof, symmetric: false, acyclic: false, doc: "the harness or theorem discharging it"} + refines: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "a stricter contract over the same subject"} + depends_on: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract assumes that one"} + documents: + {domain: Doc, range: Code, symmetric: false, acyclic: false, doc: "the prose that describes this code"} + supersedes: + {domain: Contract, range: Contract, symmetric: false, acyclic: true, doc: "this contract replaces that one; a chain, never a loop (ONT-4)"} + contradicts: + {domain: Contract, range: Contract, symmetric: true, acyclic: false, doc: "the two cannot both hold; declared once, read both ways (ONT-4)"} + +# Operators and functions a `formal:` expression may carry. A bare variable (x, i, out_i, θ) is not a symbol and is +# not checked — see the plan's ruling 2 for what symbol-level deliberately does NOT check. +symbols: + - {name: "∀", kind: operator, doc: "for all"} + - {name: "∃", kind: operator, doc: "there exists"} + - {name: "∧", kind: operator, doc: "and"} + - {name: "∨", kind: operator, doc: "or"} + - {name: "¬", kind: operator, doc: "not"} + - {name: "⇒", kind: operator, doc: "implies"} + - {name: "⟹", kind: operator, doc: "implies (long)"} + - {name: "→", kind: operator, doc: "maps to"} + - {name: "≡", kind: operator, doc: "identical to"} + - {name: "≈", kind: operator, doc: "approximately equal"} + - {name: "≠", kind: operator, doc: "not equal"} + - {name: "≥", kind: operator, doc: "greater or equal"} + - {name: "≤", kind: operator, doc: "less or equal"} + - {name: "∈", kind: operator, doc: "member of"} + - {name: "∉", kind: operator, doc: "not a member of"} + - {name: "⊆", kind: operator, doc: "subset of"} + - {name: "∪", kind: operator, doc: "union"} + - {name: "∩", kind: operator, doc: "intersection"} + - {name: "∅", kind: constant, doc: "the empty set"} + - {name: "·", kind: operator, doc: "product"} + - {name: "×", kind: operator, doc: "cartesian product or multiplication"} + - {name: "‖", kind: operator, doc: "norm delimiter"} + - {name: "Σ", kind: operator, doc: "sum"} + - {name: "ε", kind: constant, doc: "the tolerance a contract declares"} + - {name: len, kind: function, doc: "length of a sequence"} + - {name: shape, kind: function, doc: "tensor shape"} + - {name: isFinite, kind: predicate, doc: "neither NaN nor infinite"} + - {name: isNaN, kind: predicate, doc: "is NaN"} + - {name: modifies, kind: predicate, doc: "frame condition: what the kernel writes"} + - {name: preserves, kind: predicate, doc: "frame condition: what the kernel leaves alone"} + - {name: max, kind: function, doc: "maximum"} + - {name: min, kind: function, doc: "minimum"} + - {name: abs, kind: function, doc: "absolute value"} + - {name: exp, kind: function, doc: "exponential"} + - {name: log, kind: function, doc: "logarithm"} + - {name: sqrt, kind: function, doc: "square root"} + - {name: sum, kind: function, doc: "sum of a sequence"} + - {name: mod, kind: operator, doc: "modulo"} + # Measured from the corpus after the first pass: 79 expressions in 51 files carried an operator Σ did not yet + # declare. Every one below is real notation and is declared; the two glyphs deliberately left OUT are `—` and `§`, + # which are prose punctuation — the entries carrying those say `prose: true` instead. + - {name: "²", kind: operator, doc: "squared"} + - {name: "¹", kind: operator, doc: "to the first power"} + - {name: "₁", kind: operator, doc: "subscript one"} + - {name: "₂", kind: operator, doc: "subscript two"} + - {name: "√", kind: function, doc: "square root"} + - {name: "∞", kind: constant, doc: "infinity"} + - {name: "⊥", kind: constant, doc: "bottom — undefined or unreachable"} + - {name: "∘", kind: operator, doc: "function composition"} + - {name: "∋", kind: operator, doc: "contains"} + - {name: "∌", kind: operator, doc: "does not contain"} + - {name: "⊇", kind: operator, doc: "superset of"} + - {name: "⊄", kind: operator, doc: "not a subset of"} + - {name: "−", kind: operator, doc: "minus (U+2212)"} + - {name: "↔", kind: operator, doc: "if and only if"} + - {name: "⟺", kind: operator, doc: "if and only if (long)"} + - {name: "≺", kind: operator, doc: "precedes"} + - {name: "±", kind: operator, doc: "plus or minus"} + - {name: "⟨", kind: operator, doc: "inner-product open"} + - {name: "⟩", kind: operator, doc: "inner-product close"} + - {name: "∇", kind: operator, doc: "gradient"} + - {name: "∂", kind: operator, doc: "partial derivative"} + - {name: "⌈", kind: operator, doc: "ceiling open"} + - {name: "⌉", kind: operator, doc: "ceiling close"} + - {name: "′", kind: operator, doc: "prime"} + - {name: "̄", kind: operator, doc: "combining macron — the mean of a variable"} + - {name: "₀", kind: operator, doc: "subscript zero"} + - {name: "⋃", kind: operator, doc: "n-ary union"} + - {name: "←", kind: operator, doc: "assignment"} + +worlds: + committed: {doc: "the tree as committed — the world every contract is read in unless it says otherwise"} + +agents: + - pv + - pmat + - human + +# Each entry names the extractor that reads it. `implemented: false` is the honest state until ONT-4b/4c build them; +# an entry naming NO extractor, or one extractors[] does not declare, is exit 3. +entity_types: + - {name: pv-contract, extractor: pv_contract, implemented: false} + - {name: code, extractor: code, implemented: false} + - {name: lean, extractor: lean, implemented: false} + - {name: readme, extractor: readme, implemented: false} + - {name: llm-context, extractor: llm_context, implemented: false} + - {name: apr-model, extractor: apr_model, implemented: false} + - {name: csv, extractor: csv, implemented: false} + +extractors: + - {name: pv_contract, reader: ontology/extract/pv_contract.rs, implemented: false} + - {name: code, reader: ontology/extract/code.rs, implemented: false} + - {name: lean, reader: ontology/extract/lean.rs, implemented: false} + - {name: readme, reader: ontology/extract/readme.rs, implemented: false} + - {name: llm_context, reader: ontology/extract/llm_context.rs, implemented: false} + - {name: apr_model, reader: ontology/extract/apr_model.rs, implemented: false} + - {name: csv, reader: ontology/extract/csv.rs, implemented: false} + +# What this ontology does NOT express, said out loud so nobody encodes it by accident. Each names the reader that +# would have to change first. +not_expressible: + - {key: taste, reader: ontology/sigma.rs} + - {key: urgency, reader: ontology/sigma.rs} + - {key: authorship_intent, reader: ontology/sigma.rs} + +readers: + concepts: ontology/sigma.rs + roles: lint/sigma_gate.rs, lint/relations_gate.rs + symbols: lint/sigma_symbols.rs + worlds: ontology/sigma.rs + agents: ontology/sigma.rs + entity_types: lint/sigma_gate.rs + extractors: ontology/sigma.rs + not_expressible: ontology/sigma.rs diff --git a/tests/fixtures/ont/shapes-one-empty/contracts/tool-status.yaml b/tests/fixtures/ont/shapes-one-empty/contracts/tool-status.yaml new file mode 100644 index 0000000000..8025269b50 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty/contracts/tool-status.yaml @@ -0,0 +1,33 @@ +metadata: + version: "1.0.0" + kind: pattern + created: '2026-09-19' + last_modified: '2026-09-19' + author: fixture + description: fixture — a tool's --json output as a shaped entity (extract:json) +name: tool-status +version: "1.0.0" +scope: fixture +status: active +entity: + type: json + ref: data/status.json +vocabulary: + prefix: tool + root_class: tool:Status + nested: + push: tool:Push + findings: tool:Finding +shape: + targetClass: tool:Status + closed: true + properties: + - {path: tool:schema, minCount: 1, maxCount: 1, in: ["tool/status-v1"]} + - {path: tool:ok, minCount: 1, maxCount: 1, datatype: xsd:boolean} + - {path: tool:push, minCount: 1, maxCount: 1, node: {closed: true, properties: [ + {path: tool:state, minCount: 1, maxCount: 1, in: [ok, failing, never]}, + {path: tool:attempts, minCount: 1, maxCount: 1, datatype: xsd:integer}]}} + - {path: tool:findings, node: {closed: true, properties: [ + {path: tool:sensor, minCount: 1, maxCount: 1, datatype: xsd:string}, + {path: tool:open, minCount: 1, maxCount: 1, datatype: xsd:integer}]}} + diff --git a/tests/fixtures/ont/shapes-one-empty/data/status.json b/tests/fixtures/ont/shapes-one-empty/data/status.json new file mode 100644 index 0000000000..3ca2851700 --- /dev/null +++ b/tests/fixtures/ont/shapes-one-empty/data/status.json @@ -0,0 +1 @@ +{"schema":"tool/status-v1","ok":true,"push":{"state":"ok","attempts":0},"findings":[{"sensor":"s-self","open":1},{"sensor":"s-drift","open":0}]}