Repository navigation
P-0.1: one proof ladder (upstream numbering: L4 Kani, L5 Lean; PVI-D-1) in proof_status.rs and the three docs; ladder_consistency test (FALSIFY-PVI-001) #2916
Description
DAG row P-0.1 — docs/specifications/pp-066-dag.yaml (epic #2873; spec: #2870 phase 0/1 text (improve-provable-contracts.md not in tree); PP-066 §5 Track P).
Track: P · lane: 0.66 · host: intel (CI runner) for P-0.6, else any · owner: spec-owner · expiry: 2026-10-03 · quorum: teamwork
Blockers (rows): DEC-D-11
Linked issues: —
A — acceptance (exit 0 = done):
cargo test -p aprender-contracts --lib ladder_consistency
Contract: contracts/pv-p-0-1-v1.yaml
Mutation → RED: change one doc ladder -> RED
Filed by the PP-066 driver STEP 5; status tracked in the DAG (status: complete after the receipt docs/audits/impl-<ticket>-receipt.md).
Activity
noahgift commentedon Sep 23, 2026
triage 2026-09-23 (aprender-dd, standing triage owner): milestoned to 0.70.0, theme Fast Train (CI, gates, pv, release tooling, hygiene); it moved out of
backlog(the 2026-09-17 overflow bucket, not a release).noahgift commentedon Sep 25, 2026
Parked by APR-EPIC-001: over S2 budget (rank 33/38). Reopen = pull. Applied by aprender-d1 under a 3-lane quorum receipt (handoff/balance-quorum-rev4.json).