pv and ontology: verification defects and coverage gaps #5308

Scope

Where pv and the ontology say something is verified or covered when it is not: the SHACL shapes gate (silent passes, dropped contracts, missing constraints), bindings to functions that no longer exist, proof levels claimed without evidence, Kani/schema/#[contract] enforcement gaps, and the ontology extractors, focus nodes and typed entities (ONT-4/5/9) not yet covered.

Why it matters

The shapes gate and the ontology are how contract structure and coverage are enforced. A silent pass ships a malformed contract as valid, and a coverage gap is a question the ontology cannot answer yet.

Done when

Each row below is fixed with a planted-bad-contract test that the gate now rejects, or lands its extractor or entity with a test, or is closed as no longer needed.

Parent epic: #3269.

Rows

• check_pr_ont_delta.sh grades an event-SNAPSHOT body against a LIVE file list, so the documented fix can never be applied without a push #3298 — check_pr_ont_delta.sh grades an event-SNAPSHOT body against a LIVE file list, so the documented fix can never be applied without a push (branch: fix/3298-pr-body-live)
• pv: a shapes gate reports Pass AND armed over ZERO focus nodes — aggregate swallows decline: NoFocus #3610 — pv: a shapes gate reports Pass AND armed over ZERO focus nodes — aggregate swallows decline: NoFocus (branch: PMAT-3610-vacuous-shapes-r)
• pv: implement sh:lessThan / sh:lessThanOrEquals — SHACL Core property-pair constraints #3611 — pv: implement sh:lessThan / sh:lessThanOrEquals — SHACL Core property-pair constraints (branch: PMAT-3611-shacl-lessthan)
• check_ont_ratchet.sh probes a BARE pv (pvbin="$(command -v pv)") — on a fleet-clobbered runner (pv 0.65.2, no census) it reads 'no consumer' and REDs an honest anchored rise; check_apr_bin_pinned.sh is blind to the form #3679 — check_ont_ratchet.sh probes a BARE pv (pvbin="$(command -v pv)") — on a fleet-clobbered runner (pv 0.65.2, no census) it reads 'no consumer' and REDs an honest anchored rise; check_apr_bin_pinned.sh is blind to the form (branch: fix/3679-ont-ratchet-pinned-pv)
• pv lint --gate shapes: the GLOBAL NoFocus decline prints no report — by_shape/declines exist only on the per-shape path (#3610 follow-up) #4100 — pv lint --gate shapes: the GLOBAL NoFocus decline prints no report — by_shape/declines exist only on the per-shape path (pv: a shapes gate reports Pass AND armed over ZERO focus nodes — aggregate swallows decline: NoFocus #3610 follow-up) (branch: 76/4100-nofocus-report)
• pv lint --gate shapes: a contract whose YAML does not parse is dropped silently from a directory run, which still reports Pass #4622 — pv lint --gate shapes: a contract whose YAML does not parse is dropped silently from a directory run, which still reports Pass
• S4: pv writes a W3C sh:ValidationReport (Turtle and JSON) carrying the R-FEEDBACK tuple #4987 — S4: pv writes a W3C sh:ValidationReport (Turtle and JSON) carrying the R-FEEDBACK tuple
• shapes collect_shapes: unparsed YAML → Malformed, exit 3 #5191 — shapes collect_shapes: unparsed YAML → Malformed, exit 3 — done when: the pv lint --gate shapes: a contract whose YAML does not parse is dropped silently from a directory run, which still reports Pass #4622 repro exits non-zero and names broken-v1.yaml, both alone and beside a good contract; a unit test covers both venues; pv lint contracts --gate shapes

Each row was a separate ticket, folded here under the 100-open-ticket cap (TRIAGE-100, 2026-10-14) and closed as not planned. Reopen a row's ticket when its work starts; an open PR for it reopens it.

Agent: aprender-clerk

Merged in (TRIAGE-100, 2026-10-14)

From #4347 — PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of confirming them

• PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of confirming them #4347 — PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of confirming them
• PVL-001 EV-9 — PVL-9: provable-ladder required on main #4083 — PVL-001 EV-9 — PVL-9: provable-ladder required on main (branch: 52/4083-ladder-fanin, a2/4083-ev9-one-owner)
• PVL-001 EV-6c — PVL-6c: Kani assume baseline #4197 — PVL-001 EV-6c — PVL-6c: Kani assume baseline (branch: 0d/4197-ev6c-pt2, a01/070-4197-ev6c)

From #5310 — pv contract verification: Kani labels, schema count fields and #[contract] enforcement

• pv contract verification: Kani labels, schema count fields and #[contract] enforcement #5310 — pv contract verification: Kani labels, schema count fields and #[contract] enforcement
• KaniStrategy has no label for symbolic-f32-array harnesses, the dominant DSP verification technique — 7 of rmedia's 8 real Kani proofs are unrepresentable #2530 — KaniStrategy has no label for symbolic-f32-array harnesses, the dominant DSP verification technique — 7 of rmedia's 8 real Kani proofs are unrepresentable (branch: fix/2530-kani-bounded-array)
• pv schema forces the count constant P7 bans: verification_summary requires total_obligations/tested as hand-maintained integers #2648 — pv schema forces the count constant P7 bans: verification_summary requires total_obligations/tested as hand-maintained integers (branch: PMAT-2648-summary-count-drift)
• PVL-001 EV-2 — PVL-2: proof-status resolves bindings; ghost binding is a reject #4080 — PVL-001 EV-2 — PVL-2: proof-status resolves bindings; ghost binding is a reject (branch: devont/4080-ev2-pub-use-alias)
• PVL-001 EV-12 — PVL-12: release aprender-contracts-cli with PVL-1..11 #4084 — PVL-001 EV-12 — PVL-12: release aprender-contracts-cli with PVL-1..11 (branch: prep/4084-pvl12)
• PVL-001 EV-5a: pin Mathlib, scoped Lean warning gate, orphan allowlist #4122 — PVL-001 EV-5a: pin Mathlib, scoped Lean warning gate, orphan allowlist (branch: 5d/4122-orphans-wire)
• #[contract]: a registry sentinel — "no registry" is silent, "registry has no such contract" is a compile error (#2699 cause 2) #4368 — #[contract]: a registry sentinel — "no registry" is silent, "registry has no such contract" is a compile error (aprender-contracts-macros: #[contract] fails open in four places, and the doc comment claims the opposite #2699 cause 2) (branch: fix/4368-setfit-bindings)
• apr-cli: 65 #[contract] sites with no producer build.rs enforce nothing (#2699 remainder) #4370 — apr-cli: 65 #[contract] sites with no producer build.rs enforce nothing (aprender-contracts-macros: #[contract] fails open in four places, and the doc comment claims the opposite #2699 remainder) (branch: feat/4370-apr-cli-producer)

From #5333 — pv bindings and proof-status: ghost bindings and unearned proof credit

• pv bindings and proof-status: ghost bindings and unearned proof credit #5333 — pv bindings and proof-status: ghost bindings and unearned proof credit
• proof_status Lean scan: 'sorry' in a doc comment, and the domain.file citation form, deny credit to sorry-free theorems #4351 — proof_status Lean scan: 'sorry' in a doc comment, and the domain.file citation form, deny credit to sorry-free theorems (branch: 91/4351-on-r5a)
• 213 restored binding.yaml rows name symbols that do not resolve (bindings-gate ghosts, #4369 follow-up) #4379 — 213 restored binding.yaml rows name symbols that do not resolve (bindings-gate ghosts, Migrate the 12 hand-rolled producer build.rs key builders onto build_helper::env_key (#2699 remainder) #4369 follow-up) (branch: e6/4379-ghost-bindings)
• bindings resolver: bin-only modules and OUT_DIR-generated items are invisible to the ONT-3a walk (5 allowlisted rows) #4420 — bindings resolver: bin-only modules and OUT_DIR-generated items are invisible to the ONT-3a walk (5 allowlisted rows) (branch: e6/4420-resolver-bin-outdir)
• pv extract:code: binding function: Type::method never resolves; bare method names are ambiguous across impls #4521 — pv extract:code: binding function: Type::method never resolves; bare method names are ambiguous across impls
• binding-allowlist: 173 ghost bindings (debt ledger, goal empty) #4530 — binding-allowlist: 173 ghost bindings (debt ledger, goal empty)
• pv proof-status credits L3 for kani_harnesses whose harness fn does not exist, even with --verify-bindings #4531 — pv proof-status credits L3 for kani_harnesses whose harness fn does not exist, even with --verify-bindings
• pv bindings resolver: follow OUT_DIR includes mapped to a checked-in file (arch_requirements fallback) #5008 — pv bindings resolver: follow OUT_DIR includes mapped to a checked-in file (arch_requirements fallback)

From #5291 — DEFECT: pv validate passes a contract with no falsification tests or an empty test_harness (763 contracts have zero tests)

• DEFECT: pv validate passes a contract with no falsification tests or an empty test_harness (763 contracts have zero tests) #5291 — DEFECT: pv validate passes a contract with no falsification tests or an empty test_harness (763 contracts have zero tests)

From #5335 — Ontology coverage: extractors, focus nodes and typed entities (ONT-4/5/9)

• Ontology coverage: extractors, focus nodes and typed entities (ONT-4/5/9) #5335 — Ontology coverage: extractors, focus nodes and typed entities (ONT-4/5/9)
• ONT-001 to 80% in 0.69 (≈7 more rows) with SHACL armed and falsifiable — and the §11 one-row-per-train conflict this creates #3559 — ONT-001 to 80% in 0.69 (≈7 more rows) with SHACL armed and falsifiable — and the §11 one-row-per-train conflict this creates (branch: 0d/3559-ghosts)
• Docs, all 1037 examples and the cookbook: pv-SHACL validated and current for Qwen3.5 (6 of ~1500 artifacts mention it today) #3560 — Docs, all 1037 examples and the cookbook: pv-SHACL validated and current for Qwen3.5 (6 of ~1500 artifacts mention it today) (branch: c1/3560-r5-on-4502)
• binary-debt #1: ledger + DERIVED-universe guard (BINARY_DEBT ≤ 22, LEGACY_NAMES ≤ 13 at 0.70) — a new binary must be classified #4058 — binary-debt Feature Request: Decision Tree & Random Forest for Classification Tasks #1: ledger + DERIVED-universe guard (BINARY_DEBT ≤ 22, LEGACY_NAMES ≤ 13 at 0.70) — a new binary must be classified (branch: feat/4058-binary-debt-ledger)
• ONT-4c4: kernel symbols as focus nodes — extract:kernel over extract:code (ont:KernelSymbol ⊑ ont:Symbol, v4.15) #4069 — ONT-4c4: kernel symbols as focus nodes — extract:kernel over extract:code (ont:KernelSymbol ⊑ ont:Symbol, v4.15) (branch: c1/4069-ont-4c4-fresh)
• ONT-4d: subsumption in Σ; shapes inherit down the hierarchy #4070 — ONT-4d: subsumption in Σ; shapes inherit down the hierarchy (branch: df/4070-ont4d-fixture-sigma)
• ONT-2c: in-house OWL 2 EL writer; TBox check via the oracle, advisory #4071 — ONT-2c: in-house OWL 2 EL writer; TBox check via the oracle, advisory (branch: la-72/4071-tbox-differential-regen)
• ONT-3b: formalization.yaml gains model_of; a statement with no model earns no L4 #4073 — ONT-3b: formalization.yaml gains model_of; a statement with no model earns no L4 (branch: GH-4073-refine-callsite-test)
• ONT-5: pv-sat offline behind a bin boundary; witness checked in the gate; two positive controls #4074 — ONT-5: pv-sat offline behind a bin boundary; witness checked in the gate; two positive controls
• ONT-4e: requires/ensures as first-class; Liskov rule on refines, witness-checked #4075 — ONT-4e: requires/ensures as first-class; Liskov rule on refines, witness-checked
• ONT-9: the ontology has a contract; checker soundness by Kani and planted-solution generation #4078 — ONT-9: the ontology has a contract; checker soundness by Kani and planted-solution generation (branch: PMAT-4078-ont-9)
• ONT-4f: GitHub's own objects — repo, issue, pull-request, milestone — as typed focus nodes (ONT-001 v4.16) #4330 — ONT-4f: GitHub's own objects — repo, issue, pull-request, milestone — as typed focus nodes (ONT-001 v4.16) (branch: PMAT-4330-ont-4f-github-entities)
• ont extract:example ignores [[example]] targets — apr-cookbook read 0 of 1825 examples and passed #4466 — ont extract:example ignores [[example]] targets — apr-cookbook read 0 of 1825 examples and passed (branch: fix/4466-example-targets)
• ONT coverage P0: make contracts stops after pv lint (.ONESHELL exit); extract --check not on PRs; per-entity-type shape coverage ratchet #4475 — ONT coverage P0: make contracts stops after pv lint (.ONESHELL exit); extract --check not on PRs; per-entity-type shape coverage ratchet
• ONT-4g: every binary is an ONT-001 entity (Σ binary + extract:binary + surface_audit.csv ledger) #4476 — ONT-4g: every binary is an ONT-001 entity (Σ binary + extract:binary + surface_audit.csv ledger) (branch: 52/4476-ont4g-arm)
• FND-20260927-sigma-skips-crate-contracts: Σ extract must walk crates/*/contracts (PV-DUP-001 on non-identical stems) #4538 — FND-20260927-sigma-skips-crate-contracts: Σ extract must walk crates/*/contracts (PV-DUP-001 on non-identical stems) (branch: 6b/4538-sigma-crate-contracts)
• simular: serve command for web GET endpoints (post-0.70; 3 ONT-10 S13 rows marked 'unserved: GET') #4553 — simular: serve command for web GET endpoints (post-0.70; 3 ONT-10 S13 rows marked 'unserved: GET') (branch: feat/simular-serve-4553)
• apr code: record the prompt bytes sent and consumed, and exit ≠ 0 when consumed < sent (L22 slice 1) #5190 — apr code: record the prompt bytes sent and consumed, and exit ≠ 0 when consumed < sent (L22 slice 1)
• pv binary extractor: ledger rows naming a non-default feature (unblocks arming the apr surfaces) #5304 — pv binary extractor: ledger rows naming a non-default feature (unblocks arming the apr surfaces)

Open sub-issues moved here from #5335: #3856, #4465.

Folded P0 and operator-worded rows (TRIAGE-100, 2026-10-14)

These tickets were folded here by the cop ruling of 2026-10-14 (sub-rows of this master). Each keeps its priority and its owner. The operator text each carried is quoted below exactly as written; if an owner objects, the ticket is reopened.

• Capability facts as a contract: apr-model-capability-v1 + SHACL + exposure on verb/http/mcp (operator keystone) #3856 — Capability facts as a contract: apr-model-capability-v1 + SHACL + exposure on verb/http/mcp (operator keystone) (P1 owner:aprender-a7)

  Operator, verbatim (2026-09-22): "capability.rs need deep pv SHACL support and exposure on all surfaces verb + transport (http/mcp/cli)".

• README-ONT-001: README as a rendered, SHACL-proven, read-only artifact (under ONT-4c #3847) #4465 — README-ONT-001: README as a rendered, SHACL-proven, read-only artifact (under ONT-4c ONT-4c: the first non-code contracts — README.md, CLAUDE.md, one .apr model file, one CSV — with their extractors #3847) (P1 owner:aprender-a7)

  Operator, verbatim (2026-09-26): "going forward README is a SHACL ontology with schema and toml crerated READ only and provable". The operator accepted proposal v2 on 2026-09-26. v2 folds in the team review (S1 1–5, S2, S3, exit targets).