Repository navigation
pv contract verification: Kani labels, schema count fields and #[contract] enforcement #5310
Closed as not planned
Description
Scope
pv contract verification gaps: Kani harness labels, schema count fields, and #[contract] enforcement that is missing.
Why it matters
These are places where a contract claims verification that the tooling does not actually perform.
Done when
Each row below is fixed, with pv validate or pv lint failing on the planted bad case.
Parent epic: #2870.
Rows
-
KaniStrategyhas no label for symbolic-f32-array harnesses, the dominant DSP verification technique — 7 of rmedia's 8 real Kani proofs are unrepresentable #2530 —KaniStrategyhas 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)
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
Activity
[-]MASTER S2: folded sub-tickets[/-][+]pv contract verification: Kani labels, schema count fields and #[contract] enforcement[/+]noahgift commentedon Oct 14, 2026
#5310 row evidence, measured on
main@8c3b19c8c1(aprender-wprodmodels). Evidence only; no state changed.#4122 (EV-5a): every done-when item holds on main; no code work is left.
theorem … := by sorryanddef plantUnused5310 (x : Nat) : Nat := 0inProvableContracts/Defs/Rand.lean../build.shgave rc 1:FAIL warning in our tree: …Rand.lean:27: declaration uses sorry,…:29: unused variable x,RED lake build rc=0, 2 warning(s). The control and the after-revert run were both rc 0 (0 warning(s) in ProvableContracts/).mathlib-warning-is-ignoredfixture lands itswant.build.sh --self-testPASSes, and every mutant is killed.ProvableContracts/PlantOrphan5310.leangave rc 1 (RED modules=162 in-cone=107 orphans=55 allowlisted=54). The control gave rc 0 (orphans=54 allowlisted=54).check-orphans.sh --self-testPASSes.1d042d3e1e93904b24c4fe209c75d2adbb22ee24inlakefile.leanand the manifest. The clean-cache build is in the EV-5a evidence comment on PVL-001 EV-5a: pin Mathlib, scoped Lean warning gate, orphan allowlist #4122.haveinside a tactic block. It produced no warning, so the build stayed green. Lean does not analyse tactic blocks for unused variables by default (linter.unusedVariables.analyzeTactics). A plant for this gate must be a warning Lean actually emits.Other rows:
KaniStrategyhas no label for symbolic-f32-array harnesses, the dominant DSP verification technique — 7 of rmedia's 8 real Kani proofs are unrepresentable #2530, pv schema forces the count constant P7 bans: verification_summary requires total_obligations/tested as hand-maintained integers #2648, #[contract]: a registry sentinel — "no registry" is silent, "registry has no such contract" is a compile error (#2699 cause 2) #4368 and PVL-001 EV-2 — PVL-2: proof-status resolves bindings; ghost binding is a reject #4080 are done on main. Each planted case is RED and its control is GREEN.#[contract]producer) is on a branch waiting for a merge slot.noahgift commentedon Oct 14, 2026
Merged into #5308 (TRIAGE-100, 2026-10-14): same theme, so this master's scope and every checklist row now live on #5308, and this ticket is closed as not planned. Reopen it if the theme splits again.
Agent: aprender-clerk