Reuse decoded task prefixes and immutable filesystem page entries
Local command observers now retain their decoded task-volume index and cursor across typed and erased reopening. Filesystem readers borrow decoded entries, and cached leaf mutations retain unchanged immutable entry payloads with their original funding. Object-store quota accounting and persistence inspect changed persistent subtrees instead of scanning unchanged buckets, objects and multipart parts.
The three changes are consolidated here because they sit on the same per-turn path. This PR remains draft: the component proofs pass, but PERF-turn remains a merge blocker.
Guarantee
- Class: H/F. A private shared index and its cursor eliminate prefix replay on observer reopening. A single generation-checked acknowledgement prevents delayed publication from overwriting a newer observation. Private immutable funded entries and borrowed page views retain unchanged payloads; authenticated written-page admission makes them available to the next mutation. Private cached object/upload byte totals and entry counts are settled at transaction/replay boundaries. Persistence derives its delta from immutable map identity rather than a caller-maintained changed-key list.
- Proof: Independently initialized historical observer/layout, owned leaf mutation/wire writer and object delta writer are checked with the shared differential harness. Properties compare complete bytes, exact errors and ordered events; cached page histories cover directory, file-table and attribute formats, splits, retained old-page immutability and release of native funding. Physical Arc-layout and denied-admission tests require reservation before allocation. Exact production count pins and restored replay/deep-clone/full-scan/old-writer controls pass. Omitted cache/aggregate controls fail their identity/recount assertions. Real crate-local-shim Loom models cover acknowledgement versus refresh, entry custody, owned-page handoff and object publication/rollback/cancellation/lock order, including negative controls. Component proofs do not establish the complete-turn guarantee below.
- Entry points: TaskVolume typed/erased reopening, TaskFiles reopening, command-session construction/reopening and local command dispatch; snapshot/head/observe refresh, commit acknowledgement and reset. Filesystem shared and owned mutations, point/batch lookup, directory/attribute pagination, persistent diff, incremental closure, canonical codecs and cache admission/handoff. Object memory transactions, pending put publication, journal validation/inline preparation, delta serialization/relocation and checkpoint/journal replay, including multipart, rollback and durable retries. Provider calls and stream polls remain outside the task index lock; reset releases the fresh-index lock before taking the shared lock.
- Gaps: PERF-turn is open and blocks merge. The complete public command turn still needs an independently initialized old implementation, full output/error/ordered-trace equality, exact work/allocation equality at K=8/24, a restored-work control, a fixture under 10 seconds and paired measurements on all three operating systems. Current page reference-vector copying and canonical encoding still visit the leaf. Source audit also finds global history scans in scheduler capacity/model-claim/completion checks and growing attention-list projection. These gaps must close in this PR before re-review.
Component validation
Every listed focused suite finished under 10 seconds. Build durations are separate from test runtime.
| Gate | Source / result |
|---|---|
| Linux filesystem | c08fa0dc9: 130 passed across 15 focused groups, largest 0.26 s; build 6m42s |
| Linux objects | 2897c9a7d: 32 passed, largest 1.37 s; build 14.43 s |
| Linux real-lock models | Observer 2 passed incl. control, 4.81 s at bb05b1442; entry/owned custody 6 passed at 170fd59e1; objects 3 passed, 0.44 s at d27eb805d; subsequent test-clock code is excluded from Loom |
| Linux Harness callers | Observer 3 passed, 0.01 s; command-file callers 5 passed, 1.62 s at 170fd59e1; authorized file queries 7 passed at bb05b1442 |
| Windows GNU compile | Filesystem + Harness lib/tests passed at c08fa0dc9, 3m06s; objects lib/tests passed at 2897c9a7d, 2.78 s |
| macOS ivar | 2897c9a7d: objects 32 passed, largest 2.00 s; build 1m27s. Filesystem unchanged since a1570b3ca: 130 passed, largest 0.13 s; build 6m52s |
| Native Windows | 2897c9a7d: objects 32 passed, largest 4.21 s; build 14.92 s. Filesystem unchanged since a1570b3ca: 130 passed. First filesystem compiler exited with rustc access violation 0xc0000005 before a test executable; the single filesystem-only retry built in 16m16s and all selected tests passed |
Observer source is unchanged since its qualified measurements. The c08 leaf proof adds a native test module/fault switch excluded from the earlier Loom and ordinary Harness dependency builds. a157 adds the object delta implementation and proofs. macOS used RUSTC_WRAPPER=/opt/homebrew/bin/sccache; its 4.6 GiB target, source copy, archive and driver were removed immediately and verified absent (55 GiB free afterward).
Exact counts and paired measurements
Observer values are old/new. Each side owns a separate provider, journal, decoded index and cursor. Time varies with shared-host load; work, allocation count and bytes are assertions.
| K | Items old/new | Allocations old/new (Linux/Windows) | Bytes old/new (Linux/Windows) | Linux us old/new | Windows us old/new | macOS us old/new |
|---|---|---|---|---|---|---|
| 8 | 43 / 7 | 76 / 30 | 11844 / 4531 | 23.541 / 10.561 | 29.1 / 7.2 | 30.542 / 13.167 |
| 16 | 75 / 7 | 111 / 30 | 18452 / 4531 | 34.032 / 12.261 | 24.1 / 5.9 | 32.708 / 10.042 |
| 24 | 107 / 7 | 144 / 30 | 21540 / 4531 | 50.974 / 11.021 | 31.9 / 5.8 | 44.292 / 9.625 |
macOS historical observer adds one allocation / 64 bytes at each K; candidate counts match all platforms. Linux measurement head bb05b1442; Windows/macOS 2f399c35c.
Shared leaf replacement requires exactly 3 allocations at K=8 and K=24 on all platforms. Restoring unchanged-entry deep clones fails the same pin at 17 versus 3 allocations. This measures the production mutation helper; complete-turn work remains open.
At 2897c9a7d, each platform passes these production object-path pins and controls (cells are allocations / bytes):
| Path | Linux K=8; K=24 | macOS K=8; K=24 | Windows K=8; K=24 |
|---|---|---|---|
| Memory put | 10/620; 10/620 | 10/620; 10/620 | 10/620; 10/620 |
| Unchanged durable delta | 0/0; 0/0 | 0/0; 0/0 | 0/0; 0/0 |
| Durable put incl. journal | 23/3188; 23/3188 | 27/3460; 27/3460 | 23/3188; 23/3188 |
| Same durable put, restored old delta writer | 47/4276; 99/6516 | 51/4548; 103/6788 | 47/4276; 99/6516 |
Memory put visits zero unchanged members at both K values; restored quota scans visit 25/73 and fail the same work pin. The independent frozen writer requires 24/76 allocations and 1088/3328 bytes for an unchanged delta. Durable-put fixtures recover their seed before measurement and reopen afterward to compare complete state and aggregate recounts. The mixed-history property compares full encoded deltas/events against the independent writer and checks replayed full snapshots. Restoring that writer inside a real put is a negative control, not a historical whole-turn baseline.
Paired measurement commands (resolve the test executable from Cargo JSON and run that binary directly for repetitions):
cargo test --locked -p acyclic-harness --lib --features filesystem-local,native-execution,test-support,grpc,model-checking --no-run --message-format=json
"$harness_bin" task_volume::observer_tests:: --nocapture
cargo test --locked -p acyclic-fs --lib --features model-checking --no-run --message-format=json
"$fs_bin" kernel::persistent_btree::shared_leaf::tests:: --nocapture
cargo test --locked -p acyclic-objects --lib --features local --no-run --message-format=json
"$objects_bin" v1::memory::state::tests:: --nocapture
"$objects_bin" v1::memory::persistence::delta::tests:: --nocapture
Whole-turn diagnostic
The uncommitted development probe uses public connect_local/run_headless over real completed command history. Its entire fixture exceeded the 10 s suite bound before reaching K=24. The measured K=8 command used 78,248 current-thread allocations / 23,418,935 bytes and 361.7 ms. Async scheduling changes raw allocation totals between runs, and worker-thread allocations are outside this allocator scope. These are diagnostic numbers, not acceptance proof. A bounded CPU sample had incomplete stack unwinding, so it does not identify a sole dominant caller.
Decisions
- Fold the observer, immutable page entry and object delta work into one PR for the per-turn path.
- Preserve canonical persisted bytes, receipts, quota/error ordering, original allocation custody and independent observer initialization.
- Keep this PR draft until the complete-turn guarantee passes. Development probes and scratch scripts stay out of commits.
Latest counter and fixture audit (2897c9a7d)
Quota totals now subtract removed values before adding replacements through one checked helper, and publish the aggregate fields only after every check succeeds. A 128-case shrinking property compares against wider arithmetic, 64 boundary combinations cover zero/maximum values, and restoring add-first settlement fails the same oracle. Pending put uses the same helper.
The d27 macOS run caught a three-byte difference in the durable-put allocation pin caused by independently sampled timestamp protobuf widths. A test-only scoped clock supplies identical time inputs through the actual timestamp function, verifies the persisted timestamp, and restores on nested scopes and unwind. Exact allocation and byte pins remain unchanged. All 32 focused object tests now pass on Linux/macOS/Windows. The macOS target (935 MiB), source, archive and driver were deleted immediately; absence verified, 55 GiB free.
A second uncommitted public command probe seeds independently cancelled histories and finishes in 3.12 s. K=8/24 used 75,891/78,240 allocations and 22,441,649/23,571,244 bytes. Connection is flat at 31 allocations / 40,080 bytes; the task observer examines 256 items at both K values. Thus completed attention-list growth cannot alone explain the remaining command-execution growth. A bounded CPU profile of the existing binary passed in 3.58 s; raw async allocation totals varied, so these remain diagnostic measurements. PERF-turn remains open; this PR stays draft.
Coordinator retry index at fb3d0f258: replaces repeated canonical-history scans with an admitted compressed byte trie maintained during replay. Linux focused coordinator suites: 40 passed (largest suite 0.06 s); original-native custody and restored-scan control passed. Windows GNU lib/tests passed (5m38s). Whole-turn diagnostic remains non-flat: K=8 75,837 allocations / 22,429,545 bytes; K=24 78,039 / 23,411,685, on the same current-thread diagnostic fixture; this is not an acceptance proof. Remaining: task-admission lookup consolidation and expanded index proofs are committed locally but not yet qualified or pushed; per-OS qualification of the index and whole-turn PERF-turn proof are pending. PR stays draft.
Qualified retry lookup checkpoint (ad6ba8d0c)
Known declaration retries now pass through the coordinator's single indexed lookup under its existing publication gate. The separately maintained unapplied-envelope index advances without replaying scheduler state; malformed-tail fallback refreshes the scheduler before using the historical path, preserving old error order. Trie nodes and copied Unicode keys reserve original custody before allocation. Differential proofs compare complete canonical event bytes, digest, revision and commit identity against an independently initialized retained scan.
Linux native focused coordinator/host checks: 70 passed (largest 2.19 s). Windows: 70 passed (largest 0.11 s). macOS: 72 passed (largest 0.39 s), including fresh-process native source initialization and an omitted-initialization control. Linux real-lock retry publication models: 2 passed including missing-lookup control, 0.06 s. The existing 4 KiB coroutine-frame assertion passes with observe_declaration at 1264 bytes. Windows GNU lib/tests cross-check passed at ad6ba8d0c (5m24s). No limits were enlarged.
The macOS pass exposed cold CoreServices initialization occurring inside bounded native watch setup. Ordinary LocalHarness startup now initializes the native source service before bounded checkout/watch work; original typed errors remain intact. The fresh-process control reproduces the original custody refusal when initialization is omitted. This belongs at the native cold-start qualification tier; warm process tests had hidden the loader state.
Known retry lookup is exactly 61 allocations / 16,231 bytes at both K=8 and K=24; the restored historical scan uses 64/66 allocations and 16,567/17,719 bytes and fails the same pin. Missing lookup is exactly zero allocations/bytes at both sizes. Full paired tuple comparison retains complete canonical event bytes.
The current-thread public command diagnostic still grows: K=8 72,602 allocations / 20,739,916 bytes; K=24 73,925 / 21,442,528 bytes, with allocation-stack sampling enabled (5.11 s for the fixture). Connection remains 31 allocations / 40,080 bytes and task-volume observations remain 256 at both sizes. These are diagnostic numbers, not acceptance proof. PERF-turn remains open and this PR remains draft.
Decoded handoff and borrowed leaf checkpoint (c2e072e7a)
Durable acknowledgement now transfers the staged decoded owner into the durable cache before removing the staged entry, under the actual crate-local index lock. A rejected handoff retains the staged owner for retry. Directory/file-table leaf comparisons borrow cached entries and clone only changed output; the old frontier-limit behavior is retained when intermediate output or internal traversal prevents a direct paired comparison.
Linux: 62 focused filesystem tests pass across eight groups (largest 0.70 s; borrowed-leaf differential group 0.48 s), including independently initialized old collectors, full canonical bytes, exact errors, store traces, mixed leaf/internal layouts and bounded frontier limits. Three actual-lock handoff Loom models pass in 0.01 s, including the omitted-handoff control. Windows GNU filesystem/Harness lib/tests cross-check passes (1m56s). Native build 7m21s; model build 11m08s. macOS borrowed-leaf group: 4 passed in 0.09 s, build 6m48s. Prior handoff-focused macOS/Windows groups remain qualified; Native Windows borrowed-leaf group: 4 passed in 0.09 s, build 15m12s.
One changed shared leaf uses exactly 8 allocations / 3,428 total bytes at both K=8/24, for ordinary and original-native custody. All six allocation fields match. The restored old collector uses 32/82 allocations and 5,570/12,770 bytes and fails the same equality pin. Published decoded-leaf reads use zero physical allocations/bytes at both sizes; omitted handoff restores 22/54 allocations. These pins establish payload reuse, not flat leaf comparison or canonical encoding work.
Paired leaf command (same command on bb2, ivar and native Windows): cargo test --locked -p acyclic-fs --lib --features model-checking kernel::persistent_diff::tests::borrowed:: -- --nocapture. Linux runs through build-slot; Windows through lb; ivar uses sccache and deletes the lane target/source/archive/driver after completion. macOS cleanup was verified absent, with 55 GiB free.
The current-thread full-command diagnostic completes in 4.60 s but remains non-flat: K=8 71,360 allocations / 20,638,983 bytes; K=24 72,410 / 21,235,039 bytes. Connection stays at 31 allocations / 40,080 bytes; task-volume observations stay at 256 items. Allocation sampling and current-thread-only counters make this diagnostic rather than acceptance evidence. PERF-turn remains open and blocks merge; this PR remains draft.
Coordinator: add the filesystem persistent_io/shared_leaf focused proofs, staged decoded-page handoff models and existing parser/corpus qualification to the bb2 merge gate; no GitHub-hosted Rust job is added.
Qualified cache recency checkpoint — 1e2c5d5e6
Pushed signed commits 30f36451f and 1e2c5d5e6. Cache hits now relink stable admitted LRU nodes under the existing cache mutex. They retain eviction ordering without removing/reinserting heap-backed tree keys. Independent old-tree histories compare values, errors, exact order, statistics and provider traces; the missing-touch and historical-allocation controls fail the same predicates. The fixture warms Vec-backed byte sharing before capture on every OS.
For 288 mixed canonical-read, contains and decoded-page hits, all six physical allocation fields are exactly zero at K=8 and K=24 on Linux, macOS and Windows. The independent old-tree control allocates 41 times / 43,952 bytes at K=24 on every OS. K=24 paired old/new capture times: Linux 103.387/65.104 µs; macOS 73.500/64.125 µs; Windows 45.700/35.300 µs. These are single debug captures with exact-count assertions, not statistical latency claims.
Linux: 74 focused filesystem tests passed (largest group 0.68 s), eight real-lock handoff/cache Loom models including controls passed (0.01/0.00 s groups), and filesystem/harness GNU library/test compile proof passed (4m16s). macOS and Windows each passed 55 focused tests (largest groups 0.14/0.26 s). macOS target/source/archive/driver were deleted immediately; all four paths were independently verified absent.
Paired command after the focused build: $fs_binary all_three_hit_entry_points_allocate_zero_at_both_history_sizes --nocapture (the test prints both initialized implementations at both history sizes); mixed recency properties and models are in cache/lru_tests and decoded_model.
The complete-turn scratch diagnostic still grows: K=8 71,019 allocations / 20,319,472 bytes; K=24 72,340 / 20,909,104 bytes. It lacks the independent full-turn baseline and worker-thread allocation coverage. PERF-turn remains open; #985 remains draft. Local internal-routing-entry work is not part of this qualified checkpoint.
Qualified internal routing entries — 5599f747d
Cached internal pages now retain immutable routing-entry owners while rewriting a path. Unchanged routing names are borrowed/shared through the frame; changed summaries acquire their own funding. Written shared internal pages enter the decoded cache only after the authenticated put succeeds. Paired owned/shared frame representations prevent mixing custody modes. No synchronization primitive changed.
At K=8 and K=24, preserving unchanged routing entries has all six physical allocation fields exactly zero with ordinary and original native custody on Linux, macOS and Windows. The independent former owned path allocates K name buffers (512/1,536 bytes), and fails the same zero-allocation predicate. The canonical-history property now generates multi-level layouts as well as single leaves and compares full canonical pages, errors, mutation events, old-page immutability, flush/handoff and final funding release across all three formats.
| Gate | Result | Largest focused group | Build |
|---|---|---|---|
| Linux filesystem | 38 passed | 0.20 s | 8m09s, combined filesystem/harness build |
| Linux existing future bound | 1 passed | 0.02 s | same build |
| Windows native filesystem | 38 passed | 0.25 s | 15m04s |
| macOS filesystem | 38 passed | 0.11 s | 6m51s |
| Windows GNU filesystem/harness library/tests | passed | compile proof | 1m28s |
K=24 old/new unchanged-entry capture times: Linux 8.060/1.540 µs, Windows 36.500/1.000 µs, macOS 6.833/1.875 µs (single debug captures, not latency distributions). Run $fs_binary unchanged_internal_routing_entries_retain_their_owner_without_allocating --nocapture and the restored_owned_children_fail_the_same_zero_allocation_pin control after the focused test build. The existing eight handoff/cache real-lock models from 1e2 are reused because these locks and their code paths are unchanged. macOS target, source, archive and driver were deleted and independently verified absent.
This removes unchanged routing-key cloning, while pointer-vector work and canonical page serialization still depend on page size. The current whole-turn diagnostic remains nonflat: K=8 70,671 allocations / 20,103,255 bytes; K=24 71,337 / 20,581,005 bytes (4.91 s fixture). It still lacks the independent complete-turn baseline and worker-thread counter coverage. PERF-turn remains open; #985 remains draft. Main's capture-oracle failures are being corrected on a separate clean branch from origin/main.
Dependency proof checkpoint
Dependency-proof checkpoint cef721117 (still draft).
Facade mutations no longer take an unconditional rollback snapshot of the entire captured dependency map. A single private installer validates/funds the delta under the proof lock, performs the fallible root handoff, then installs the delta without another fallible step. Both ordinary and original-native paths use it. Genuine shared snapshots retain copy-on-write semantics; retries revalidate the current dependency count and expected state before transferring the root.
The independent old map implementation, generated mixed/duplicate deltas and every admission/custody/finish cut compare complete dependency semantics and claim retirement. At K=8/24 an existing-key upgrade has exactly two charged visits and no new physical allocations; all six allocation fields equal the independently prepared input's destruction. Restoring the former full-map snapshot fails that same predicate. The actual proof-lock Loom models pass, including the split-snapshot lost-observation negative control.
The shipping current-thread facade mutation retains all prior observations and returns exact truncated bytes. Linux and macOS both report identical K=8/24 pairs: 50 total allocations, 19,192 total bytes, 1,476 bytes copied and 31 examined items; all six physical allocation fields match. Eleven focused facade tests pass on both (largest group 0.02 s / 0.01 s). Seventeen kernel/rebase proofs and ten facade regressions passed on native Windows at 199b79506; production code is unchanged, but the corrected public facade pair still needs a native Windows run. macOS used sccache; the lane target, source, archive and driver were deleted and independently verified absent.
The whole-turn diagnostic remains nonflat: K=8 70,686 allocations / 20,070,451 bytes; K=24 71,287 / 20,609,626 bytes. The fixture runs in 3.98 s. The next probe reuses the built binary and targets the growing 36-KiB allocation bin. PERF-turn still blocks readiness, together with the complete-turn independent baseline, full output/error/trace equality, restored-work control and final per-OS measurements. Scratch profiler/scripts are excluded from commits. #1036's separate main-regression fix is in the merge gate.
Paired proof commands: $fs_binary existing_dependency_upgrade_has_exact_constant_work_and_no_allocations --nocapture; $fs_binary original_native_upgrade_has_no_copy_or_allocation_and_rejects_snapshot_control --nocapture; $fs_binary facade::tests::dependency_delta:: --nocapture. Dedicated model build: RUSTFLAGS="$RUSTFLAGS --cfg acyclic_fs_loom --cfg acyclic_loom" cargo test --locked -p acyclic-fs --lib --features model-checking --no-run, then run its binary with facade::proof::model_checking:: (4 passed, <0.01 s).
Windows GNU filesystem/harness library/tests compile proof passed (5m18s). Linux native build 5m11s; dedicated model build 11m25s. Build-slot job 1792351264132-303744 completed rc=0, verdict cache 4e0d7e403e68.
Closure leaf-diff checkpoint (0e1cedd71)
The retained-binary allocation stacks identified the temporary union of unchanged file records in closure proof as the source of the growing 36/72-KiB buffers. The proof caller now cancels equal shared leaf entries on every aligned frontier before staging changed records. Public bounded diffs and merge callers retain their original intermediate-union semantics. A paired leaf stops at the existing change bound and returns truncation to the full-proof fallback; it never attempts another slot beyond that bound.
Linux at this head: 54 focused filesystem tests passed (24 diff, 3 full-proof/cache properties, 23 closure, 3 incremental namespace, 1 facade dependency), largest suite 1.95 s. Harness future bounds passed in 0.03 s. Filesystem and Harness Windows GNU library/tests compile proof passed in 2m30s; native build took 8m16s. Build-slot job 1792353812007-380528 completed rc=0. The earlier 4ff compile was intentionally cancelled after the bounded-pair audit found the issue; its remote rc143 is not a test failure. Native Windows and macOS qualification have both passed; complete platform results follow below.
Exact K=8/24 allocation pairs, including all six physical fields: candidate 11 allocations / 4,614 total bytes at both sizes; restored old collector 13 / 8,070 versus 15 / 21,894, and fails the same pin. Copied bytes also match (ordinary 0, original-native 576); entry visits still grow 11 to 27. The independently initialized old collector compares complete changed records, canonical bytes, exact errors and store traces in shrinking histories. A separate generated bounded-prefix property compares against its complete old diff; removing the production bound fails with DiffAllocationFailed. Paired commands: $fs_binary proof_diff_retains_only_changed_records_across_leaf_frontiers --nocapture; $fs_binary restored_union_collector_fails_the_same_proof_allocation_pin --nocapture; $fs_binary bounded_proof_leaf_matches_the_complete_old_diff_prefix --nocapture; $fs_binary removed_pair_bound_breaks_the_same_complete_diff_prefix_property --nocapture.
Guarantee: class H, redundant retention of unchanged records, is removed for aligned shared leaf pairs at the closure diff choke point. Both ordinary and original-native proof entry points use it; public diff/merge entry points retain the old path and its existing properties. No synchronization paths changed, so the previously posted actual-lock models are reused. This is a draft component checkpoint: remaining gaps include leaf entry scans, cold/unaligned frontiers and the whole-turn differential proof. The whole-turn diagnostic is still nonflat (K=8 70,573 allocations / 19,471,862 bytes; K=24 71,220 / 19,751,652; fixture 4.25 s). Neither size has any 36/72-KiB allocation now. PERF-turn remains open; this PR is not ready for review. Scratch scripts and profile probes remain outside the commits.
Platform completion for signed head 0e1cedd71: Linux, macOS and native Windows each passed all 54 focused filesystem tests, including the bounded-prefix and restored-union controls. Largest suite: Linux 1.95 s, macOS 0.84 s, Windows 0.63 s. Builds: Linux native 8m16s / Windows GNU proof 2m30s, macOS 14m58s, Windows native 15m55s. All OSes report the same K=8/24 six-field allocation pair (11 allocations / 4,614 bytes) and copied-byte pin; native public-facade dependency pairs also match (50 allocations / 19,192 bytes / 1,476 copied / 31 visits). macOS used sccache, then removed its 4.1-GiB target, source, tar and driver; a separate SSH check verified all four absent (34 GiB free).
The retained Linux binary was hash-verified and rerun without compilation: the 36/72-KiB allocations are absent; two 18-KiB samples at K=24 still come from the unmatched-frontier union collector. Diagnostics ran in 4.12 s and 6.63 s. This is the next component to remove. Entry scans and the full-turn independent baseline/counter/trace proof still block readiness. #985 remains draft.