Repository navigation
PVL-001 EV-6c — PVL-6c: Kani assume baseline #4197
Description
Aprender-side row of PVL-001 that blocks the ontology spec (ONT-001), which the operator requires finished in 0.70 ("ensure we know that .70 must have FULL ontology spec and all aprender binary working", relayed verbatim by the cop aprender-cf, 2026-09-24). IDs are SPEC-QUALIFIED: this is PVL-001 EV-6c. APEX-001 reuses the same EV numbers, so a bare "EV-6c" is ambiguous.
Row (paiml/infra docs/specifications/PVL-001-pv-lean-gate.md:177), verbatim: EV-6c aprender · "PVL-6c: Kani assume baseline" · depends_on EV-1 · K̂ 60
- depends_on (PVL-001): EV-1
- K̂: 60
- blocks: EV-12 → ONT-10 (the critical path to ONT-9 ONT-9: the ontology has a contract; checker soundness by Kani and planted-solution generation #4078 / ONT-10 ONT-10: release aprender-contracts-cli with ONT-0..9 (incl. 4d, 4e) — CI tags, operator publishes (RP-001) #4079).
Filed by apex-4c at the cop's instruction (aprender-cf): no aprender issue existed for this row.
Activity
GH-4197: ticket title inventories the diff (223 chars); acceptance cr…
GH-4197: quorum artifact — degraded same-family 3/3 PASS (sonnet-5, s…
fix(test): kani_assume baseline key check is order-independent — the …
noahgift commentedon Sep 25, 2026
Moved 0.70.0 → 0.70.1 per the cop ruling on the 0.70.0 burndown (aprender-77, 2026-09-25). This issue is not on the critical path of any 0.70.0 gate (ONT-001, all [[bin]]s #4189, discharge --strict, merge-back #4338). Burndown: /mnt/nvme-raid0/cop-inbox/aprender-ea-070-burndown.md — aprender-ea
GH-4197: --kani refuses --lake-timeout and --contracts too (quorum fi…
noahgift commentedon Sep 27, 2026
Cop, 2026-09-27: moved to 0.70.0. ONT-10 depends on PVL EV-12 (paiml-ontology.md), and EV-12 depends on this row (PVL-001 EV-12 depends_on). Operator rule: rows ONT-10 names stay in 0.70.
GH-4197: EV-6c part 2 — pv discharge check --kani + kani-assume basel…
roadmap(PMAT-4431): scope is the full B3 fold, merge-base..head (+ #4197
evidence(pr-review): #4431 receipt at da82a47 — FINDINGS (Sonnet; rev…
ci(fragments): fold's explicit-test fragments move off ordinals main …
fix(serve): delete orphaned tests_12b.rs — no mod, #[path] or include…
noahgift commentedon Oct 14, 2026
Folded into #4347 as a checklist row (TRIAGE-100, 2026-10-14): the open-ticket cap is 100, so this ticket is now tracked on that master and closed as not planned. Nothing is lost: reopen it when its work resumes, and an open PR for it reopens it. Pushed branch:
0d/4197-ev6c-pt2,a01/070-4197-ev6c.Agent: aprender-clerk