EPIC v0.1.619 — Ledgers the tools can read, proofs that can block

Epic 1 of 5 in xpile's tagged-release plan, drafted 2026-09-23 by xpile's standing owner session (xpile-74) from the operator's request relayed verbatim by the cop (aprender-cf): "ensure all of these have next five epics planned out as they will be continuously worked on". Pattern copied from paiml/apex#130–#134: one milestone per tag, one epic per milestone. Grill pending (Claude Code lanes, Sonnet 5 — author is Opus 5.5).

v0.1.619 — "Ledgers the tools can read, proofs that can block"

Theme: every signal xpile publishes about itself must be readable by the fleet's tools and able to stop a merge. Today pmat work cannot parse the roadmap (#2123) and the three proof jobs are advisory (#2119).

row	done_when	depends on
#2123 — roadmap `priority` P0/P1/absent breaks `pmat work`	`pmat work status PMAT-1516` exits 0; `roadmap_ledger_parses.rs` gains an arm asserting every `priority ∈ {low,medium,high,critical}`, shown RED by re-inserting one `P1`	mapping P0→critical, P1→high, absent→medium (as proposed on the issue)
#2119 — kani / lake-build / lean-models advisory; pv unpinned; Lean↔contract pairing	`gate` `needs:` the three proof jobs (or they join the required set); `cargo install aprender-contracts-cli --version <pin> --locked`; a pairing gate names every unpaired `.lean` file. RED arm: a deliberately broken theorem fails `gate`	branch-protection edit is owner-gated → cop
CRUX-0 — author `crates/xpile/tests/released_binary_crux.rs` (the CRUX gate below)	runs green against the installed 0.1.618 binary; both positive controls RED	—
0.1.619 deferrals — PMAT-1390 (attested/unattested semantics), PMAT-1392 (WAT `bool`/`CUInt` ambiguity documented), PMAT-1393 (READMEs outside `current_md_carries_no_bare_derived_counts`), PMAT-1353 (unsigned FFI call-site retype)	each closed with its own falsifier, or re-deferred on this epic with a reason	—
#2138 — Python → C `unsigned int` workspace fails E0308 (the PMAT-1353 deferral)	`--verify` on hybrid_unsigned MATCHes CPython without `--repair`; PR #2140	—
#2139 — `--verify` skips `float` / `unsigned long` as non-ABI-mappable at exit 0 while the workspace fails E0308	float bridged via ctypes `c_float` semantics; unsigned long reported, not skipped; red arm per type	#2138
#2145 — a Python bool into a C `int` boundary fails E0308 (currently the repair loop's convergence witness)	builds and matches without `--repair`, and the repair witness is re-pointed or its domain recorded	#2138
Honesty-hunt lead (a) — `book_published_command_witness.rs` module-doc claims "nothing in this repo had ever executed a command it publishes"; `cli_docs_drift.rs` may falsify it	sentence verified against `cli_docs_drift.rs` and corrected, or kept with the measurement recorded	—
Ledger hygiene — PMAT-465 (reprioritise v0.2.0) superseded by this plan; PMAT-956 marked planned but memory records the arc done	each row closed or re-statused with the sha that proves it	—
Repo hygiene — `delete_branch_on_merge` on; merged/closed-head branches pruned (shas recorded)	`gh repo view --json deleteBranchOnMerge` = true; branch list diff recorded here	cop approves the delete list

Release gates (every release in this plan)

gate	command	positive control (must go RED)
CRUX — known answer on the RELEASED binary	`XPILE_BIN=$(mktemp -d)/bin/xpile` after `cargo install xpile --version <X> --locked --root <that dir>`, then `cargo test -p xpile --test released_binary_crux -- --ignored`: transpile the pinned known-answer corpus (`examples/{factorial,gcd,word_count}.py` → `--target rust` → `rustc` → run) and compare stdout byte-for-byte against BOTH `python3` and a pinned answer table; `xpile --version` must equal `<X>`	`XPILE_CRUX_SELF_TEST=flip` flips one pinned answer and must go RED; `XPILE_BIN` pointed at a stub printing the previous version must go RED
dogfood	the `dogfood` skill: fresh `cargo install` from crates.io into a scratch root, then every command published in `README.md` / `book/src` / crate READMEs runs against the installed binary (not `target/`)	the runner's planted stub (wrong version, one missing subcommand) must go RED
release procedure	`docs/RELEASE.md` §2a tripwires exit 0; §5 steps 1-9 recorded on this epic	—

A row is DONE only when its merged sha is an ancestor of origin/main. done_when is the row's own falsifier — a test that was run RED against the unfixed tree before going green (the honesty-hunt rule: green→red arm is the deliverable).

Progress (xpile-74, 2026-09-23):

pmat work cannot read this roadmap: 67 rows carry priority P0/P1 (and 2 carry none), so every pmat work status/quorum-review call fails #2123 ✅ merged (fix(roadmap,gate): pmat work could not parse the ledger — 67 P0/P1 priorities (Refs #2123) #2129)
PVL-F3: lake-build, lean-models, kani are ADVISORY; aprender-contracts-cli install unpinned; 28/42 Lean files unpaired #2119: pins and the Lean pairing gate merged (fix(ci,gate): pin every cargo install in CI — pv, cargo-deny, kani-verifier (Refs #2119) #2130); making the proof jobs block is waiting on the owner (escalated)
CRUX-0 (CRUX-0: known-answer gate on the RELEASED xpile binary (released_binary_crux.rs) #2131): PR test(release,gate): known answer on the RELEASED binary (Refs #2131) #2132 has an agreed quorum and is waiting on CI
Repo hygiene ✅: delete_branch_on_merge is on, 494 remote branches are pruned (shas in the gist; 4 evidence/ tags), and both open issues are in this milestone

New row, found while working honesty lead (a): the book_published_command_witness.rs headline overclaims (verified false: cli_docs_drift.rs already ran xpile info). The one-sentence fix is ready, but the pre-commit complexity gate refuses any commit to that file, because published_commands sits at cyclomatic 27 and cognitive 83 (thresholds 20/30), and advertised_subcommands (41) and precondition_claims (42) are also over. That debt makes the gate file uneditable. Row: split those three functions below the thresholds with no change in behaviour (the gate's own red arms must stay red), then land the headline fix.

Paused 2026-09-23 on the operator's order (via the cop) until 02:00 CEST. State at pause:

test(release,gate): known answer on the RELEASED binary (Refs #2131) #2132 (CRUX-0): agreed quorum; CI workspace-test was still pending. On resume: confirm green, then merge.
refactor(test): book_published_command_witness below the complexity gate + headline correction (Refs #2133) #2134 (book_published_command_witness.rs cannot be committed to: three functions exceed the pre-commit complexity gate #2133 complexity refactor + honesty lead (a)): quorum lane 1 PASS at 6aa5035 after one applied finding. Lanes 2–3 not yet run.
PVL-F3: lake-build, lean-models, kani are ADVISORY; aprender-contracts-cli install unpinned; 28/42 Lean files unpaired #2119: blocking policy waiting on the owner.
Next rows: the 0.1.619 deferrals (PMAT-1390/1392/1393/1353); ledger hygiene (mark PMAT-2123 done, PMAT-465/956).

chore(roadmap): register the v0.1.619 epic as PMAT-2124 (Refs #2124)

chore(roadmap): receipts for PMAT-956 (done) and PMAT-465 (superseded…

docs(audit): quorum-PMAT-2124 — round 2 3/3 PASS (agy gemini x3) afte…

chore(roadmap): ledger hygiene; repair main's red release_story_deriv…

refactor(test): book_published_command_witness below the complexity g…

0.1.619 deferrals: resolved (xpile-74, 2026-09-24).

PMAT-1353 (unsigned FFI call site): fixed in fix(hybrid,ffi): Python → C unsigned int builds and matches CPython (Refs PMAT-2138) #2140 (PMAT-2138). Probing it found the float/unsigned long false green, filed as hybrid --verify skips float and unsigned long boundaries as 'non-ABI-mappable' and exits 0, while --emit-workspace emits code that fails E0308 #2139.
PMAT-1393 (READMEs outside the bare-count gate): covered, closed. Measured: root README.md has 0 bare derived counts. contracts/README.md's only counts are a dated snapshot (@ 2026-07-27, 34592ceb) that names its derive command and still equals live xpile quorum (26/9/0 of 35). Later claims_drift.rs gates (the census check and docs_claim_no_total_quorum_while_any_contract_is_partial) cover both READMEs.
PMAT-1390 (attested = mentioned anywhere): re-measured, kept deferred with a reason. xpile attestations --json shows 0 of 35 contracts attested only through the preamble (preamble_mentions is reported per contract), so changing the semantics still has no live effect, and the report already discloses it when non-zero. Revisit when a contract's attestation first depends on the preamble.
PMAT-1392 (WAT i32 → bool vs CUInt): moved to EPIC v0.1.622 — Aliasing, and WASM both ways #2127 (v0.1.622, WASM lift, PMAT-952). It's an emit-image ambiguity with no correct inverse unless out-of-band type information is available, which is exactly the lift design's problem. It's value-preserving today and documented in the crate docs.

test(release,gate): known answer on the RELEASED binary, not the tree…

Progress (xpile-74, 2026-09-24 ~09:30 CEST). Merged: #2135 (ledger hygiene; repaired a red main), #2137 (PMAT-2136), #2134 (PMAT-2133 plus honesty lead (a)), #2143 (PMAT-2141, main.rs committable again), #2132 (CRUX-0 gate, closes #2131). Waiting on CI: #2144 (PMAT-2142), #2140 (PMAT-2138, the PMAT-1353 deferral).
Still open in this milestone: #2119's blocking half (owner decision), #2139 (float / unsigned-long false green, next after #2140) and #2145 (bool into int; this is also the repair witness).
Quorum practice changed today per the operator: 2 agy lanes + 1 claude-haiku lane per round, with Claude fallback when agy is quota-out. Two lanes caught false claims in my own PR text this morning (#2140, #2143); both were corrected before merge.

Backlog rule applied (operator, 2026-09-24). backlog milestone created. Unmilestoned open issues: 0 before, 0 after. #2138, #2139 and #2145 were in v0.1.619 without being listed in this epic; all three came out of its '0.1.619 deferrals' row, so they're now listed here as rows rather than moved. Backlog count: 0. Standing rule: any new unmilestoned issue goes to backlog the same day.

docs(release): plan v0.1.619 (core) and v0.1.620 (look-ahead) as one …

merge main into the C1 ledger-reconcile branch: keep the row-5 Done n…

chore(roadmap): reconcile the ten merged epic #2124/#2125 rows to don…

Navigation Menu

Repository navigation

EPIC v0.1.619 — Ledgers the tools can read, proofs that can block #2124

v0.1.619 — "Ledgers the tools can read, proofs that can block"

Release gates (every release in this plan)

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

EPIC v0.1.619 — Ledgers the tools can read, proofs that can block #2124

Description

v0.1.619 — "Ledgers the tools can read, proofs that can block"

Release gates (every release in this plan)

Activity

noahgift commented on Sep 23, 2026

noahgift commented on Sep 23, 2026

noahgift commented on Sep 24, 2026

noahgift commented on Sep 24, 2026

noahgift commented on Sep 24, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions