Liking cljdoc? Tell your friends :D

Phase F + G5 Design: Delete the Owned Tree, Collapse RwLockArc

Status: DESIGN ONLY — no code written. Owner reviews before any implementation. The irreversible steps (G5 arbitrary-V flip; owned-tree deletion; RwLockArc) are individually gated and require explicit owner GO. V7 — incorporates Round-1…Round-6 red-team (12 independent adversarial passes, claims re-verified against live code incl. an executed TLC run). Round 6 (the confirmation round) ruled the DATA-LOSS/code surface fully CONVERGED (every fix re-verified against code; C-1 complete) and found the design surfaces (§2-§4, §6-§8) coherent — but caught that §5 (the RT1-RT6 red-team narratives) had NOT been re-synced across rounds 2-5 and still stated the V2 checkpoint_lock-gating (RT3, refuted by V3), the absolute "never .ok()-swallow" bar (RT2, refined by §2.5), and "no new ordering" (RT6, refuted by R14). V7 re-syncs §5 RT2/RT3/RT6 to the current resolutions + clears the editorial NITs (effort framing, F0 seam naming, §8 file set). The whole doc — including §5 — is now self-consistent. Round-6 fixes SUPERSEDE all prior deltas where they conflict. Verified against live code at the cited file:line (re-opened each during this pass). Baseline as stated: cargo nextest run --features persistent-artrie --no-fail-fast ~2610 passed / 3 skipped; scripts/verify-formal-correspondence.sh exit 0; UNSAFE_INVENTORY.tsv = 99 rows (the load-bearing gate is the set-equality check, not a fixed count).

V2 deltas (Round-1 red-team resolutions)

Round 1 CONFIRMED the core: the G5 substrate (node/format/recovery/checkpoint) is genuinely V-generic (§2.1); build_value_path_recursive is mechanically genericizable + compile-clean (load_overlay_node_from_disk is already in the <V,S> block); the lock-collapse keystone (§3.5) holds (overlay arm is self.read(); only the dormant owned arm holds the write lock); and the formal claim is proven by EXECUTION — TLC on LockFreeDurableCheckpoint.cfg (USE_WATERMARK=TRUE) = no error / 2810 states, the _Unsafe.cfg exhibits the NoLostWriteUnderLockFreeCommit losing trace. RT5 (arbitrary-V eviction read) is RESOLVED to a non-issueevict_node_at_path walks the OWNED tree only (char mod.rs:~2103, byte shared_trait_impl.rs:~343), empty under the flip, so overlay finals are never freed in production for ANY V; the non-faulting read is exact. Four material gaps fixed below:

  • G-NH1 (data-loss): get_or_insert falls through to the dead owned tree for arbitrary V post-flip (its unranked WAL record is dropped under the Overlay regime) → genericize it to the overlay value seam, NEVER fall through (§2.2, §2.6, §2.7).
  • G-NH2 (silent regression): compare_and_swap is rejected under route_overlay(); for arbitrary V it would break at the eligibility flip (F2), not at owned-deletion. DECISION: supply a generic overlay value-CAS (§2.7) so no working feature regresses.
  • PF-1 (decomposition self-contradiction): RT3 proves Slice 2 (lock collapse) cannot land before Slice 3 (owned deletion) UNLESS the owned root is interior-mutable. ~~RESOLUTION: adopt the narrow owned-path lock — the existing checkpoint_lock gates owned mutations when !route_overlay()~~ [SUPERSEDED by V3/V5 PF-1: checkpoint_lock does NOT exist + a Mutex can't mutate the non-IM root; the real fix is owned_root: RwLock<TrieRoot<V>> + the whole-struct 8-field audit, §3.5] — genuinely decoupling F4 from F7 and restoring the Slices-1+2 value (§1.3, §3.5, §4).
  • RT5 forward-constraint + C4 scoping: record the "no production overlay eviction" invariant as a tested precondition + a Phase-E/F forward constraint (§2.4); the C4 assert fix is char-ONLY (byte already routes through the correct !route_overlay() trait assert) + debug-only (§3.5).

V3 deltas (Round-2 red-team resolutions — SUPERSEDE the V2 entries where noted)

Round 2 verified the V2 substrate/eviction/formal fixes hold, but found the V2 §2.7/PF-1 fixes themselves under-specified or wrong. Six corrections:

  • G-NH2 CORRECTED — the value-CAS uses BINCODE-BYTE comparison, NOT V: PartialEq. Round 2 proved DictionaryValue has NO PartialEq and the existing public compare_and_swap compares by serializing both values and comparing bytes (c_bytes == e_bytes, char atomic_ops.rs:~237). The generic overlay value-CAS must do the same (needs only Serialize, already a supertrait). Its recheck-failure-after-WAL exit MUST: not rank + mark_committed_burned(lsn) (liveness — else the watermark stalls). (§2.7 rewritten.)
  • G-NH1 CORRECTED — get_or_insert needs insert_cas_with_value_durable to be INSERT-ONCE. Round 2 found the naive "present? read : insert" is non-linearizable (the durable insert overwrites on CAS-retry + the readback can disagree with the stored value). FIX: make insert_cas_with_value_durable re-check presence INSIDE the CAS loop (return Ok(false) + the existing value on a concurrent insert), so all racers converge on one value and get_or_insert reads-its-write. (§2.7.)
  • G-NH4 (NEW, data-loss) — byte insert_batch drops arbitrary-V values. byte insert_batch_entry_overlay (mutation_api.rs:~354) falls back to membership-only insert_cas_durable for non-{i64,u64} V (char is safe — it delegates to the single-op). Genericize insert_batch_entry_overlay over V (route to the generic value path), in F0. (§2.7.)
  • G-NH5 (NEW, F2-timing) — merge/document-tx regress at F2, not F7. merge_from/merge_replace/merge_from_batched + begin_document/commit_document reject under route_overlay() (same class as CAS) — they break the instant eligibility flips (F2), for arbitrary V that used the owned path. Re-classify them as F2 carve-outs (reject-or-rework at the flip, like CAS): F2 must EITHER rework them to overlay OR explicitly document "arbitrary-V merge/doc-tx require kill_switch_to_owned()" and carve them out of "lock-free for all V". (§2.7, §6 R6→split.) (increment/fetch_add likewise — a one-line F2 carve-out; legitimately counter-only.)
  • PF-1 CORRECTED (SUPERSEDES the V2 PF-1) — the owned root becomes interior-mutable; checkpoint_lock is ADDED, not "existing". Round 2 proved (a) checkpoint_lock does NOT exist in src/ (it's ADDED in F3), and (b) a Mutex<()> CANNOT enable &self owned mutation — the owned root: TrieRoot<V> has no interior mutability and the mutators assign self.root + take &mut. CORRECT design: under Arc<T>, wrap the owned root field in RwLock<TrieRoot<V>> (NOT a bare Mutex<()>) — this (i) provides safe interior mutability for the &self-converted owned mutators (NO new unsafe), (ii) ~~PRESERVES the downgrade semantics~~ [SUPERSEDED by V4/NF-2: the downgrade is DELETED, not preserved — owned-arm readers become lock-free &self], (iii) confines the lock to the dormant owned path (overlay path stays lock-free). Add a SEPARATE checkpoint_lock: Mutex<()> to serialize concurrent CHECKPOINTS (distinct concern). ~~Re-cost PF-1 from "mechanical/S" to "structural/M"~~ [SUPERSEDED by V4/NF-1: whole-struct field audit, re-cost M+]. (§3.5 rewritten.)
  • RT6 CORRECTED — the eviction callback takes the OWNED-ROOT lock, not checkpoint_lock. Because eviction mutates the owned tree, post-PF-1 it takes the new owned_root RwLock (not checkpoint_lock), and the existing drop-before-join discipline (disable_eviction drops the guard before shutdown().join(), shared_trait_impl.rs:~286) is re-established for the owned_root lock — so no new join-while-holding-lock deadlock. (§3.5, §6 RT6.)

V4 deltas (Round-3 red-team resolutions — SUPERSEDE the V2/V3 entries where noted)

Round 3 (two independent passes, every claim re-verified against live code) confirmed the V3 substrate but found the V3 §2.2 and §3.5 fixes THEMSELVES incomplete — TWO new data-loss-class holes plus seven correctness/scoping clean-ups:

  • G5-NEW-4 (NEW, DATA-LOSS — the V3 §2.2 fix was wrong) — the DURABLE empty-term value publish must be RANKED. §2.2 said route key_bytes.is_empty() through overlay_publish_root_value "exactly as the counter path does." VERIFIED WRONG: overlay_publish_root_value (flip.rs:663) uses the UNRANKED publish_root_cas (flip.rs:574 docstring: "no WAL, no commit rank"), so a durable empty-term Insert LSN would be left UNRANKED → dropped by reconcile_lww_with_regime on Overlay-regime reopen → insert_with_value("",v)/upsert("",v) lost across restart (the C2c footgun the empty-string effort already fixed for counters). The existing u64 insert_cas_with_value_durable (lockfree_cas.rs:1765) does NOT special-case "" — build_value_path_recursive(&root,&[],0,value) at depth 0 INSIDE the ranked commit_seq CAS loop (:1834:1854commit_rank_and_mark :1862) handles "" correctly (comment :1787-1789). FIX: value_publish_inner must NOT special-case the empty term — let build_value_path_recursive at depth 0 handle it inside the ranked loop, exactly as u64 does. The unranked overlay_publish_root_value is correct ONLY for the no-WAL reestablish-value fold (§2.3), where there is no LSN to rank. (§2.2 rewritten.)
  • NF-1 (NEW, BLOCKER — the V3 PF-1 was under-scoped) — the interior-mutability audit must cover ALL &mut self-written fields, not just root. Under Arc<T> (no outer RwLock), EVERY method reachable on the shared handle must be &self; each one writing a non-interior-mutable field fails to compile. V3 PF-1 enumerated only root. VERIFIED at least THREE more need it: eviction_coordinator (char mod.rs:451/byte dict_impl.rs:297, written by enable_eviction :1822 + the ALREADY-&self disable_eviction :1832 via self.write().…take()), overlay_write_mode (char :391/byte :353, written by the pub kill_switch_to_owned(&mut self) flip.rs:416), and byte dirty_prefixes (:306, written by owned mutators live under Option-B WAL-replay). FIX: re-scope PF-1 to a FULL field audit (rootRwLock<TrieRoot<V>>; eviction_coordinatorMutex<Option<…>>; overlay_write_modeAtomicU8-backed or RwLock; dirty_prefixesMutex/RwLock; enumerate the rest), each safe (no new unsafe). Re-cost PF-1 above structural/M to a whole-struct interior-mutability pass. (§3.5 rewritten.)
  • NF-3 (NEW, DATA-LOSS reasoning + likely pre-existing live bug) — checkpoint_lock is LOAD-BEARING, not "redundant-but-harmless." §3.5/F3 said the new checkpoint_lock is redundant pre-collapse because "the RwLock write guard serializes checkpoints incidentally." VERIFIED FALSE for the overlay arm: char's overlay-arm checkpoint returns holding only self.read() (mod.rs:1344-1352), so two concurrent checkpoint() calls do NOT exclude each other → they race capture_snapshot_immutable + publish_immutable_snapshot_retaining_wal (block-0 descriptor + arena alloc). Reachable in production TODAY for eligible V ({(),u64} char) since the create-flip is wired (NF-5). FIX: (a) treat checkpoint_lock as a load-bearing concurrent-checkpoint fix (NOT redundant), add it with a real two-checkpoint + reopen test (the loom Model can't see the descriptor race); (b) it is MANDATORY at F4 for byte (byte serializes checkpoints via the outer self.write() today — shared_trait_impl.rs:134 — and loses that at the collapse); (c) flag the char overlay-arm concurrent-checkpoint race as a PRE-EXISTING bug to surface to the owner (the checkpoint_lock closes it regardless of Phase F). (§3.5, §6 R-NF3, §7.)
  • NF-2 (the V3 "preserves downgrade" justification is incoherent) — the downgrade is DELETED, not preserved. V3 delta 5(ii) claimed wrapping the owned-root field in RwLock<TrieRoot> "PRESERVES the downgrade semantics (mod.rs:1357/1384)." VERIFIED: the live downgrade (mod.rs:1384) is on the guard from self.write() (:1362) = the OUTER trie RwLock that Phase F DELETES; the inner owned-root RwLock is a different lock, and the readers the current downgrade admits (contains/get_value via self.read()) become LOCK-FREE post-collapse. So the downgrade is obsoleted, not preserved. FIX: replace the justification — post-collapse the owned checkpoint takes owned_root.read() for capture; owned-arm readers are lock-free &self; there is no downgrade. (§3.5.) (Cite correction: only :1384 is a downgrade site; :1357 is not.)
  • G5-NEW-2 (the V3 §2.7 NH1 fix omits the WAL burn) — liveness. The insert-once recheck moves presence-detection AFTER the WAL append, so a racer that loses to a concurrent insert has ALREADY appended its Insert LSN and must BURN it (mark_committed_burned(lsn)), else the unranked-unburned LSN stalls the contiguous committed watermark (committed_watermark.rs:84-90) → checkpoint reclaim halts. FIX: the in-loop recheck uses the existing publish_root_cas_rankedRootPublishOutcome::AlreadyInStatemark_committed_burned(lsn) idiom (lockfree_cas.rs:436-440); §2.7 must cite it. (§2.7.)
  • G5-NEW-3 (the V3 NH5 carve-out list is incomplete) — add the parallel-merge ops. merge_from_parallel (byte parallel_merge.rs:80/char :34) + merge_from_batched_parallel (char :~131) are pub, arbitrary-V, route_overlay()-rejecting — same F2-regression class as merge_from. Add them to the F2 carve-out list (§2.7 NH5, §6 R13).
  • G5-NEW-5 (doc-internal contradiction) — §4 F0 still says V: PartialEq. §4 F0 (the CAS line) carries a stale "V: PartialEq bound on the method" that directly contradicts the V3 §2.7/R11 correction (no PartialEq; bincode-byte compare; Serialize-only). FIX: reconcile §4 F0 to bincode-byte comparison. (§4.)
  • G5-NEW-6 (the RT2 "never swallow" obligation is not currently honored) — acknowledge it. The owned-replay apply path G5 reuses under Option B (mutation_core.rs Insert/Upsert/CAS arms; byte :615/:621; byte reestablish overlay_write_mode.rs:375 deserialize::<V>(...).ok()) warn-drops a bincode-deserialize failure rather than propagating. Valid values are unaffected, but the doc over-claims its own bar. FIX: §2.5/RT2 must acknowledge the current warn-drop and DECIDE corrupt-record policy (warn-drop vs hard-fail recovery) explicitly. (§2.5.)
  • NF-4 / NF-6 / NF-7 (scoping/honesty) — enumerate the ctor + &mut self.root sites broken by wrapping root (NF-4: mmap_ctor.rs:44/431/676 + twins, dirty_tracking.rs:57, mod.rs:2102); quantify the in-repo .read()/.write() blast radius in R8 (NF-6: $\ge$15 test/bench/example files + the liblevenshtein sibling per the cross-repo gate); tighten the §3.5 claim-1 wording "the ONLY write across I/O" to "the only write that REQUIRES exclusion-across-I/O for correctness" (NF-7: mutations also hold the lock across I/O but route to lock-free CAS internally). Stale-comment sweep (NF-5): "INERT pre-flip / not-yet-wired" comments (overlay/checkpoint.rs:125, persistence_api.rs:286, char mod.rs:1339) predate the wired create-flip — the flip IS live for eligible V; re-audit any route_overlay()==false-in-production reasoning.

V5 deltas (Round-4 red-team resolutions — SUPERSEDE the V4 entries where noted)

Round 4: G5 surface CONVERGED (every data-loss fix confirmed correct against code); Phase-F surface NOT CONVERGED — the V4 NF-1 audit was STILL incomplete + a deadlock-adjacent lock-ordering gap. Resolutions:

  • NF-1 COMPLETED (the V4 4-field list was inconsistent + incomplete) — the audit now covers ALL &mut self-written fields with an explicit policy. Round 4 enumerated every field and found the V4 table wrapped overlay_write_mode (written by the inherent &mut self kill_switch_to_owned) while OMITTING four sister fields written by the IDENTICAL category of inherent &mut self lifecycle method: char durability_policy (mod.rs:447, set_durability_policy wal_helpers.rs:47), checkpoint_manager (:444, enable_epoch_checkpointing epoch_checkpointing.rs:62), memory_monitor (:436, enable_memory_monitor observability.rs:199), group_commit (:431, enable_group_commit observability.rs:124); byte durability_policy (dict_impl.rs:289, persistence_api.rs:131). VERIFIED none are reachable on the shared handle today (the collapse compiles iff they STAY &mut self), so the omission is silent. FIX: §3.5 PF-1 now carries the COMPLETE field table + states the two-tier policy explicitly — Tier-1 "pre-share configure" methods stay &mut self (absent from the Arc<T> API, NO wrap); Tier-2 "runtime shared-handle" methods are &self (fields wrapped). The background-subsystem family (eviction/memory_monitor/checkpoint_manager/group_commit) is treated UNIFORMLY (eviction is ALREADY &self via EvictableARTrie, so the consistent choice makes the family Mutex<Option<Arc<…>>>+&self runtime toggles). (§3.5 rewritten; §6 R3.)
  • NF-? eviction lock hierarchy (NEW, MED / deadlock-adjacent — the V4 RT6 "no new ordering" was too glib). Post-collapse the eviction Mutex (EC) gains two new in-edges: the eviction callback reads it under the owned-root lock (OR→EC, mod.rs:~1738) and the eviction-on checkpoint publisher reads it under checkpoint_lock (CK→EC, persist.rs:~735). The CK↔OR↔EC cycle is averted TODAY only by the existing drop-before-join discipline. FIX: §3.5 documents the hard lock hierarchy CK > OR > EC with EC a LEAF (never held across CK/OR/or a worker join) + a loom/stress gate (checkpoint‖disable_eviction‖writer). (§3.5, §6 R14.)
  • R-1/R-2 (G5 MED — the insert-once mechanism citation was empty-term-only). The V4 §2.7 NH1 cited the empty-term publish_root_cas_rankedAlreadyInState idiom for insert-once, but that publisher inspects only the ROOT — a NON-empty leaf already-present needs the value-path AlreadyExists arm (the membership pattern: char LockfreeInsertResult::AlreadyExists lockfree_cas.rs:~514, byte DurableBuildError::AlreadyExists :~883). AND the single value_publish_inner seam must distinguish INSERT-ONCE (abort-on-present) from UPSERT (always-write). FIX: §2.2/§2.6 split the seam (insert vs upsert discriminator); §2.7 NH1/§4 F0 cite the membership AlreadyExists pattern for the non-empty case, reserving the empty-term publish_root_cas_ranked for "" only. (Mechanism gap, not data-loss — the goal + the liveness burn were already correct.)
  • R-3a/R-3b/R-4 (G5 NIT/LOW — carve-out completeness + honesty). Add merge_from_batched_grouped (char merge_api.rs:183) to the §2.7/R13 carve-out enumeration; add compact (byte compaction_impl.rs:110, rejects under route_overlay() :129) to the §2.7 F2 carve-out (it's an F2 regression for arbitrary V, same class as merge — V4 filed it only under R6/§3.2); note increment/fetch_add was NEVER a working arbitrary-V feature (owned increment itself fails for non-numeric V — char atomic_ops.rs:71/91), so carving it loses nothing (favorable). (§2.7.)
  • F3 reversibility honesty (LOW). §4 F3 "Reversible: trivial" is incomplete: checkpoint_lock closes the NF-3 live data-loss race, so reverting it REOPENS a data-loss bug. FIX: §4 F3 qualified to "mechanically reversible, but forward-only — reverting reopens the NF-3 race." (§4.)
  • R15 (NEW, MED — checkpoint_lock scope). checkpoint_lock serializes checkpoint↔checkpoint but NOT checkpoint↔compact (compaction renames the file via a different mechanism, compaction_impl.rs:~322, not gated by checkpoint_lock). In production compact rejects under route_overlay() (unreachable), but under a kill-switched-owned trie it's reachable. FIX: gate compact under checkpoint_lock too, OR document owned-mode compaction-vs-checkpoint as single-threaded-by-convention under kill-switch. (§3.2, §6 R15.)

V6 deltas (Round-5 red-team resolutions)

Round 5 ruled BOTH surfaces CONVERGED (the Phase-F field audit was independently re-derived from scratch and confirmed COMPLETE — first clean round for it; the lock graph proven ACYCLIC) — modulo ONE MED doc-propagation defect + minor editorial. Resolutions (no new data-loss in the design itself; these tighten the SPEC so an implementer can't build the hole):

  • C-1 (MED — the R-G5NEW4 fix wasn't propagated to §2.7). The V4 empty-term ranked-publish fix landed in §2.2 + §4 F0 but NOT in §2.7's two OTHER durable value-routed ops: the §2.7 get_or_insert and compare_and_swap paragraphs still named the UNRANKED overlay_publish_root_value for "" — which §4 F0 explicitly forbids. For CAS this is the exposed case (line 191 was its only "" instruction → an implementer following §2.7 verbatim would build the unranked-"" data-loss into CAS: Upsert LSN unranked → dropped on Overlay reopen → CAS returned Ok(true) but value lost). FIX: both §2.7 "" references rewritten to the RANKED mechanism (build_value_path_recursive depth-0 for get_or_insert; publish_root_cas_ranked baking as_final().with_value for CAS), reserving overlay_publish_root_value for the no-WAL reestablish fold (§2.3) only. (§2.7.)
  • C-2 (NIT) — §2.6 seam table reconciled to the R-2 split (two seams: value_insert_publish_inner insert-once vs value_upsert_publish_inner always-write).
  • F1 (NIT) — lockfree_root/lockfree_cache rationale corrected from "already interior-mutable" to "Tier-1 pre-share-only" (the Option wrapper is whole-&mut self-assigned by enable_lockfree; the contents are IM but the wrapper isn't — the exact category-error of rounds 2-4, now stated precisely + a forward strong_count==1 guard added). (§3.5.)
  • F2 (NIT) — the ambiguous Tier-1 "candidates" sentence replaced with the firm decision (overlay-installers Tier-1; the subsystem family + durability_policy + kill-switch Tier-2). (§3.5.)
  • F5 (NIT) — clarified the owned-arm checkpoint holds BOTH CK and OR (CK because it is a checkpoint; OR for owned-root capture exclusion); "NOT checkpoint_lock" was scoped to which lock provides the exclusion. (§3.5/§4 F4.)
  • F6 (NIT) — vocab scoped OUT explicitly: SharedVocabARTrie is a distinct struct, a separate follow-on, not covered by this field audit (the vocab overlay shares the NODE, not the trie struct). (§3.5.)

1. SCOPE / EFFORT — read this first (the honest assessment)

1.1 The plan you handed me was wrong in exactly one load-bearing way, and the code proves it

The old plan (carefully-review-…md, Phase F line 218) says Phase F is "mechanical once E is proven." That is false, and the reason is concrete and verifiable: the owned dual-representation tree (TrieRoot/ChildNode) is still the SOLE representation for four production-reachable regimes, each of which I verified against live code:

#Owned-tree dependencyVerified at
1Arbitrary V never flips; uses owned exclusivelyoverlay_write_mode.rs:466-468 (byte overlay_eligible_v = {(), i64}); char twin overlay_write_mode.rs:119-121 ({(), u64}). flip_to_overlay is a no-op for ineligible V (flip.rs:377-380).
2Every reopen loads the on-disk image into owned, then republishes owned→overlay + clear_ownedmmap_ctor.rs:431/:676 (load_root_from_diskinner.root = root), then :483-487 (flip_to_overlay() + reestablish_overlay_dispatch()). No load_root_immutable exists (grep: zero hits).
3Kill-switch (kill_switch_to_owned) — restart-time fallback to ownedflip.rs:416-421; production-pub on byte (overlay_write_mode.rs:738).
4Compaction rejects under route_overlay(); owned-mode onlycompaction_impl.rs:129-136 (byte).

So "delete the owned tree" is blocked on first routing arbitrary V through the overlay — the deferred G5 flip — and then on replacing the reopen-into-owned reconstruction. Until both land, deleting the owned tree silently breaks (1)–(4).

1.2 This is a large, multi-week re-architecture. Say so.

This couples two efforts, each individually the size of a shipped milestone:

  • G5 (route arbitrary V through the overlay): generic durable value-write + a third reestablish fold + the arbitrary-V read route + eligibility flip. Effort: L ($\approx$ 1–2 weeks incl. proofs). The good news the code confirms (below) shrinks this materially.
  • Phase F (delete owned + RwLockArc): reopen-into-overlay loader, compaction rework, kill-switch removal, dead-code deletion across byte+char+vocab, the lock collapse. Effort: XL ($\approx$ 2–4 weeks; the deletion blast radius is ~thousands of LOC — byte transitions.rs alone is 1157 LOC + mutation_core.rs 623 LOC, with char twins).

Total realistic envelope: 4–6 weeks of careful, reversible, per-phase-green work, with three separately-gated irreversible flips at the end.

1.3 The scoped-subset recommendation (the high-value, low-risk slice)

The single most valuable piece is decoupleable from the riskiest piece. Two observations from the code drive this:

  1. The RwLockArc collapse does NOT require deleting the owned tree. The lock is collapsible the moment no path needs &mut self write-exclusion across I/O. Today exactly ONE path does: the owned arm of the non-blocking checkpoint (mod.rs:1362-1386 char — self.write() → capture → downgrade). The overlay arm (mod.rs:1343-1352) is already lock-free (self.read() + lock-free capture_snapshot_immutable). So if every live write target is the overlay, the write lock has no remaining writer to exclude — even with the owned tree still present as a dormant reopen-staging buffer.

  2. G5 is what makes every live write target the overlay (it flips arbitrary V too).

This yields a decomposition the owner should weigh:

  • Slice 1 (G5 only): arbitrary V routes through the overlay. Owned tree stays (as the reopen-staging buffer + compaction backend). Delivers: lock-free writes/reads for ALL V. Irreversible (one gated flip). This alone removes the write lock's last writer.
  • Slice 2 (the lock collapse): Arc<RwLock<…>>Arc<…> + a dedicated checkpoint Mutex. Delivers: the max-parallelism win (no reader/writer ever serializes on the trie lock). Irreversible (type change). Depends on Slice 1; DECOUPLED from Slice 3 via the owned-root interior-mutability audit (§3.5/PF-1 — owned_root: RwLock<TrieRoot<V>> + the whole-struct 8-field wrap; the V1 claim that Slice 2 needed Slice 3 was a real hole, resolved).
  • Slice 3 (owned-tree deletion): reopen-into-overlay loader + compaction rework + delete ~thousands of dead LOC. Delivers: code-size/maintenance win, NOT a runtime-parallelism win (the owned tree is already off the hot path post-Slice-1+2). Irreversible. Highest effort, lowest marginal runtime value.

My recommendation: Slices 1+2 deliver ~90% of the value (lock-free everything + the lock collapse) at a MINORITY of the effort (G5=L + the now-M+ whole-struct lock collapse vs Slice 3 = "the bulk"; the original "~40%" estimate predates PF-1's re-cost from mechanical/S to whole-struct M+, so read it as "a minority", not a precise fraction) — and Round-1's RT3 hole (that Slice 2 was secretly gated on Slice 3) is resolved by the owned-root interior-mutability audit (§3.5/PF-1 — owned_root RwLock + whole-struct field wrap), so this framing is now SOUND, not aspirational. Slice 3 is a genuinely-optional correctness-neutral cleanup that can be staged indefinitely behind a #[cfg]/dead-code allowance. The owner should explicitly decide whether Slice 3's code-hygiene payoff justifies its blast radius now, or whether to ship 1+2 and leave the owned tree as a documented, dormant reopen-staging buffer. I phase all three below but mark Slice 3 as owner-optional.

This mirrors the prior empty-string effort's discipline: ship the coupled-but-bounded change, leave the sprawling cleanup as a follow-on.


2. G5 DESIGN — route arbitrary V through the overlay

2.1 What is already done (the code shrinks G5 dramatically — verified)

The task's framing is correct and the code confirms it: the NODE already holds arbitrary V, the on-disk format already stores bincode(V), recovery is already V-agnostic, and the checkpoint capture is already V-agnostic. Specifically:

  • Node: OverlayNode<K, V> carries value: Option<V> immutably; with_value(v: V), as_final(), get_value() -> Option<V> are all generic (g4-unify-overlay-node.md §2.3; node mutators verified generic via the empty-string doc's keystone §8 field-by-field check).
  • On-disk: serialize_char_node_to_disk bincodes node.value: Option<V> into [value_len:u32][bincode(V)] (persist.rs:1052-1071) — zero format change for any V.
  • Checkpoint capture: capture_snapshot_immutable reads Option<V> off the node directly (persist.rs:362-364: "the converter reads the value off the node — the former map_value: Fn(u64)->V bridge is gone"). Already V-generic.
  • Recovery: recovered_operations_from_record treats WalRecord::Insert{value: Option<Vec<u8>>} / Upsert{value: Vec<u8>} as opaque bytes (recovery.rs:355-375). The bincode round-trips through DictionaryValue: Serialize + DeserializeOwned (the existing bound). Already V-agnostic.

What is NOT done (the actual G5 surface): the durable write path and the read route and the reestablish fold are counter-specific via the CounterValue seam (u64/i64). These are the three things G5 must generalize.

2.2 G5-A — the generic durable value-write path

The problem (verified): insert_cas_with_value_durable (char lockfree_cas.rs:1765) and upsert_cas_durable (:1881) take value: u64, serialize it (:1810), and bake it via build_value_path_recursive(&root, &chars, 0, value) whose signature is value: u64 (:1986-1992). Byte's build_value_path_recursive is value: i64 (lockfree_cas.rs:1189-1192). These are the u64/i64 monomorph specializations.

The design — a value-write seam distinct from the counter seam. The counter path (increment) does RMW arithmetic (old + delta, overflow-bounded) and is inherently {i64,u64}-specific — it stays. Arbitrary V has no increment; it only has set-the-value (insert-with-value / upsert), which is a plain path-copy of a leaf carrying V. So the clean split is:

  1. Generalize build_value_path_recursive over V. Its body is pure structure (path-copy + with_value(value)), and with_value is already generic. Change the signature from value: u64/i64 to value: V and the node type from PersistentCharNode<u64> to PersistentCharNode<V> (= OverlayNode<CharKey, V>). This is mechanical — the only u64-ness is the parameter type. Rename to build_value_path_recursive staying, but lifted into the generic impl<V: DictionaryValue, S> block (today it sits in the <u64,S> block).

    • Why correct: the recursion only calls find_child/with_child/as_final/with_value, all <K,V>-generic on the unified node. No arithmetic, no u64 semantics. The empty-string keystone (empty-string-value-support.md §8) already proved with_value preserves orthogonal fields for any V.
  2. Add a generic durable value-write to the shared DurableOverlayWrite trait (Template-Method, DRY) — insert_cas_with_value_durable_default(&self, key_bytes: &[u8], value: V) -> Result<bool> and upsert_cas_durable_default(...). The skeleton is identical to the existing increment template (durable_write.rs:220-275), step-for-step:

    • gate (durable_policy_gate, noun "write") → enable-check → present-hoist (faulting-with-fallback, the existing valued-insert hoist at char :1796-1806) → step 1: append_durable_wal(WalRecord::Insert{term, value: Some(bincode(value))})step 2: publish via a new seam value_publish_inner(key_bytes, value) -> Result<(bool, u64)> (the path-copy CAS loop, returning insert-happened + winning generation) → step 3: commit_rank_and_mark(lsn, key_bytes, generation).
    • Empty term "" — NO special-casing; it MUST stay inside the RANKED loop (Round-3 G5-NEW-4 correction, DATA-LOSS). The V3 text here said "route key_bytes.is_empty() to overlay_publish_root_value(value) … exactly as the counter path does." That is wrong and data-loss-critical: overlay_publish_root_value (flip.rs:663) wraps the UNRANKED publish_root_cas (flip.rs:574 docstring "no WAL, no commit rank"), so a durable empty-term Insert LSN would be left UNRANKED → dropped by reconcile_lww_with_regime on Overlay-regime reopen → insert_with_value("",v) lost across restart (the C2c footgun). The existing u64 insert_cas_with_value_durable (lockfree_cas.rs:1765) proves the correct shape: it does NOT special-case "" — build_value_path_recursive(&root, &[], 0, value) at depth 0 is the empty-term root publish, run INSIDE the ranked commit_seq CAS loop (:1834compare_exchange :1854commit_rank_and_mark :1862), which produces a real generation (comment :1787-1789). So value_publish_inner carries NO is_empty() branch: build_value_path_recursive(&root, &units, 0, value) at units == [] IS the ranked empty-term publish. (The unranked overlay_publish_root_value is correct ONLY for the no-WAL reestablish-value fold §2.3, where there is no LSN to rank.)
    • Why DRY: the gate/append/rank/mark control flow lives ONCE in the trait (the data-loss-critical Order-A ordering); only value_publish_inner is a per-variant seam (it names the concrete OverlayNode<K,V> via build_value_path_recursive). This is the value-write seam, parallel to but separate from increment_publish_inner (the counter seam, which stays {i64,u64}).
    • INSERT-once vs UPSERT distinction (Round-4 R-2): insert_with_value (insert-once: abort-on-present, the entry().or_insert contract) and upsert (always-write, last-writer-wins) need DIFFERENT publish behavior, so the seam takes a discriminator — either value_publish_inner(key_bytes, value, insert_once: bool) or two seams (value_insert_publish_inner / value_upsert_publish_inner). The INSERT-ONCE variant carries the AlreadyExists detection (§2.7 NH1 / R-1: return already-present when the leaf is final, so the caller burns the LSN + returns the existing value); the UPSERT variant always overwrites (no recheck, like today's upsert_cas_durable char lockfree_cas.rs:1905). The V4 single-always-overwrite seam was correct for upsert but silently broke insert-once — do NOT share one always-overwrite seam.
    • Bincode placement: serialize $V \to Vec<u8>$ once, BEFORE append_durable_wal (matching :1810); the WAL record is V-agnostic bytes thereafter.
  3. Wire byte/char insert_with_value/upsert to route arbitrary V. Today insert_with_value (byte mutation_api.rs:56-71) uses route_insert_with_value_bytes (lockfree_value_route.rs:68-78) which downcasts to the <i64,S> monomorph and returns None for non-i64 V (→ owned). After G5-A, the route helper is no longer needed for the value path: insert_with_value calls the generic insert_cas_with_value_durable_default::<V> directly under route_overlay() (no Any downcast — V is the trie's own type param). The Any downcast survives ONLY for the counter/increment seam.

Effort: M. Mostly genericizing one recursive fn + lifting two durable wrappers into a shared template. The Any dispatch shrinks (value path drops it).

2.3 G5-B — the third reestablish fold (generic value)

The problem (verified): reestablish_overlay_dispatch (char lockfree_cas.rs:328-345) has exactly two arms — u64 → counter fold, () → membership fold, ineligible → no-op (Ok(()) at :344). Arbitrary V currently hits the no-op (correct today, because arbitrary V never flips). Under G5 it must republish (term, V) pairs.

The design — add a generic value fold to LockFreeOverlay alongside the existing reestablish_overlay_membership (flip.rs:437) and reestablish_overlay_counter (flip.rs:473):

fn reestablish_overlay_value(&mut self) -> Result<()>   // the third fold

Its body is a near-clone of reestablish_overlay_counter (flip.rs:473-502) with two changes:

  • the empty-term partition publishes via overlay_publish_root_value(v) (already generic — flip.rs:663) — identical to the counter fold's empty arm (flip.rs:480-484), since that arm is already V-generic.
  • the per-unit chunk publishes via a new generic seam overlay_publish_value(units, v: V) (the no-WAL path-copy value insert), instead of overlay_publish_counter(units, cv). This seam wraps build_value_path_recursive::<V> (no-WAL) — the generic twin of the existing overlay_publish_counter (overlay_write_mode.rs:524-552).
  • it reads owned pairs via the existing owned_units_with_values_under seam (flip.rs:165-168) — already returns (Vec<K::Unit>, V) generically (byte impl overlay_write_mode.rs:499-502 is V-generic). No new owned reader needed.

Then extend the dispatch (lockfree_cas.rs:328) with a third arm: after the u64/() checks, for any other (eligible) V, call reestablish_overlay_value(). Because the dispatch is the single chokepoint hit by ALL reopen paths (mmap_ctor.rs:487,709,1086,1331; io_uring_ctor.rs:285), one edit covers every reopen.

  • Why the clear-owned-LAST discipline survives (D1): reestablish_overlay_value reuses the SAME owned_* un-routed readers and the SAME clear_owned()-LAST control flow as the proven counter fold (flip.rs:498-501). The D1 grep gate (flip.rs:24-34) already scans owned_* bodies; the new fold adds no owned_* seam. The data-loss-critical invariant is inherited, not re-derived.

Effort: S–M (one fold $\approx$ 30 LOC + one publisher seam + one dispatch arm).

2.4 G5-C — the arbitrary-V read route

The problem (verified): overlay_route_get_value (flip.rs:531-546) dispatches V == CounterValue (:534) and V == () (:538), returning None for arbitrary V (:545). None means "caller reads owned" — correct today, broken once arbitrary V lives in the overlay.

The design — add the direct-V arm. The overlay node stores Option<V> directly, so the arbitrary-V read is the simplest of the three: navigate to the leaf and return get_value(). Add a fall-through arm to overlay_route_get_value:

// after the CounterValue and () arms:
// arbitrary V: the node stores Option<V> directly — read it.
let node = self.overlay_navigate(units);            // flip.rs:278, in-mem only, non-faulting
return Some(node.and_then(|n| if n.is_final() { n.get_value() } else { None }));
  • Why correct: overlay_navigate walks in-memory children only (flip.rs:278-286, the non-faulting rule §"NON-FAULTING read engine"); a final node's get_value() is the stored Option<V>. For a present-but-valueless final (a V trie always sets a value on insert_with_value, so this is only the membership () corner which the () arm already handles), returns None — consistent with owned semantics.
  • Why Some(...) not None: returning Some(maybe_v) tells the caller "the overlay handled it" (the term is absent or present-with-value), so the caller does NOT fall through to the empty owned tree. Returning None (today) would wrongly fall through. This is the load-bearing one-line behavior change — it MUST flip in lockstep with eligibility (§2.5) and the write route (§2.2), exactly as the empty-string H5 read/write coupling (empty-string-value-support.md §3 H5).
  • Reader fault-in caveat — RESOLVED to a non-issue (Round-1 RT5, verified): the non-faulting walk is exact because overlay finals are NEVER freed in production, for ANY V. Production eviction enters via enable_eviction → the callback → evict_node_at_path, which walks the OWNED tree only (char mod.rs:~2103 match self.root { Node => .., Empty => return false }; byte shared_trait_impl.rs:~343 find_parent_mut over owned ChildNode) — it never touches lockfree_root/OverlayNode. Under route_overlay() the owned tree is cleared (clear_owned after reestablish), so evict_node_at_path is a structural no-op (documented verbatim at persist.rs:~2351-2369). This walk is over the OWNED tree generically, so arbitrary V inherits the identical non-eviction property as {(),counter} → the resident-finals read is exact. Two obligations: (a) ADD a test asserting overlay finals survive a force_eviction for an arbitrary-V flipped trie (pins the invariant); (b) forward constraint — any future Phase-E/F work that "wires the overlay into the eviction walk" (the persist.rs:2360 TODO) REINTRODUCES this read-vs-eviction hazard and must re-establish faulting-or-resident exactness before doing so. (The flip.rs:36-44 "#[cfg(bench-internals)] test-only" comment is imprecise: the eviction registry population runs in production, but the node reclamation no-ops on the empty owned tree — the operative invariant "overlay finals never freed in production" holds.)

2.5 G5-D — eligibility flip + recovery

  • Eligibility: overlay_eligible_v() (overlay_write_mode.rs:466-468 byte / :119-121 char) currently returns true only for {(), counter}. Change to return true for all V: DictionaryValue once G5-A/B/C exist. This is the single irreversible line that activates arbitrary-V overlay routing (every gate keys on it: flip_to_overlay flip.rs:378, the create-flip mmap_ctor.rs:90, the reopen flip mmap_ctor.rs:484). Gate it behind a feature flag + kill-switch (§4).
  • Recovery reconcile_lww: verified V-agnosticrecovered_operations_from_record (recovery.rs:353-375) carries value as Option<Vec<u8>> opaque bytes; the apply step bincode-deserializes to V via the existing DictionaryValue bound. No change needed. The only obligation is a test proving arbitrary-V WAL records round-trip through reconcile_lww (the reconcile_lww_with_regime Overlay-rank path drops unranked records — arbitrary-V durable writes are RANKED via commit_rank_and_mark in §2.2, so they survive; add a negative-control test that an unranked arbitrary-V record is dropped, mirroring the counter discipline durable_write.rs:196-204).
  • Corrupt-record policy (Round-3 G5-NEW-6) — make the deserialize-failure decision explicit. The owned-replay apply path G5 reuses under Option B (mutation_core.rs Insert/Upsert/CAS arms; byte :615/:621; byte reestablish overlay_write_mode.rs:375 deserialize::<V>(value_bytes).ok()) currently log::warn!-drops a bincode-deserialize FAILURE (a genuinely-corrupt record), NOT propagates it. Well-formed arbitrary-V values are unaffected (they deserialize fine — no valid-value loss), so this is not a G5 data-loss hole, but the doc must not over-claim "never .ok()-swallow." DECISION (record it): a corrupt arbitrary-V record stays warn-drop (matches the existing membership/counter discipline + avoids one bad record bricking recovery); upgrading to hard-fail-recovery is a separate cross-cutting change out of G5 scope. State this in the GAP_LEDGER so the RT2 obligation is honestly scoped, not silently violated.

2.6 G5 summary — the seam split (the DRY answer)

OperationSeamDomainNew in G5?
membership insertoverlay_publish_membership / insert_cas_durable()no
value insert (insert-once)value_insert_publish_inner (NEW; aborts-on-present via AlreadyExists, R-1/R-2) + shared templatearbitrary Vyes
value upsert (always-write)value_upsert_publish_inner (NEW; always overwrites) + shared templatearbitrary Vyes
increment (RMW)increment_publish_inner (counter seam){i64,u64}no (unchanged)
reestablish membershipreestablish_overlay_membership()no
reestablish valuereestablish_overlay_value (NEW fold)arbitrary Vyes
reestablish counterreestablish_overlay_counter{i64,u64}no
readoverlay_route_get_value (+ NEW arbitrary-V arm)allarm added

The value seam and the counter seam are cleanly disjoint: value = set (path-copy + with_value), counter = RMW (read + arithmetic + with_value). No code is shared between them beyond build_value_path_recursive (now generic) and the Order-A skeleton (already shared).

2.7 G5-E — the OTHER value-routed operations: get_or_insert + compare_and_swap (Round-1 NH1/NH2)

Round 1 found two value-routed operations the original §2 missed; BOTH mis-behave the instant overlay_eligible_v() flips for arbitrary V, so they are part of G5's surface (not Phase F):

get_or_insert (NH1 — data-loss/split-brain). Today get_or_insert(_bytes) routes via route_get_or_insert* (char lockfree_value_route.rs:~70, byte :~107) which downcasts to the {i64,u64} monomorph and returns None for arbitrary V → the caller runs its OWNED body (WAL Insert + owned-tree write). Under the G5 flip (route_overlay() true, owned tree empty) that owned write is invisible to the overlay read/checkpoint AND its WAL record is UNRANKED → dropped by reconcile_lww_with_regime under the Overlay regime → silent value loss. FIX: genericize get_or_insert to the overlay — present (overlay read) ? return it : insert via the new generic insert_cas_with_value_durable_default::<V> then return. It MUST route to the overlay for eligible V and NEVER fall through to owned. (Empty term "": the RANKED depth-0 build_value_path_recursive publish inside the durable seam handles it — §2.2/G5-NEW-4 — NOT the unranked overlay_publish_root_value, which would drop the LSN on reopen.) Land it in F0. Insert-once requirement (Round-2 correction): the naive "present? read : insert" is NON-linearizable — insert_cas_with_value_durable overwrites on CAS-retry, and the post-insert readback can disagree with the stored value (two concurrent get_or_insert(K,d1)/(K,d2) on an absent K can each return their OWN default while the stored value is the other's). FIX: make insert_cas_with_value_durable re-check presence INSIDE the CAS loop (on a concurrent insert that won, return Ok(false) + the now-present value rather than re-baking the value), so all racers converge on ONE inserted value and get_or_insert reads-its-own-write (the entry().or_insert contract). This insert-once fix is part of F0 (it also tightens plain insert_with_value's insert-vs-overwrite semantics). Burn the WAL record on the concurrent-insert branch (Round-3 G5-NEW-2, liveness): moving the presence detection from BEFORE the append (today lockfree_cas.rs:1796-1806) to INSIDE the loop (after the append at :1813) means a racer that loses to a concurrent insert has ALREADY appended its Insert LSN; returning Ok(false) without burning it leaves an unranked-unburned LSN that STALLS the contiguous committed watermark (committed_watermark.rs:84-90) → checkpoint reclaim halts. The branch's BURN uses mark_committed_burned(lsn) (durable_write.rs:202). Mechanism correction (Round-4 R-1): the empty-term publish_root_cas_rankedRootPublishOutcome::AlreadyInState idiom (lockfree_cas.rs:436-440) inspects only the ROOT, so it is the "" sub-case ONLY. For a NON-empty leaf, the already-present detection is the MEMBERSHIP pattern — LockfreeInsertResult::AlreadyExists (char lockfree_cas.rs:~514) / DurableBuildError::AlreadyExists (byte :~883): the value-path publish (the insert-once variant of value_publish_inner, §2.2) must return an already-present signal when the leaf is final, on which the caller burns + returns Ok(false) + the existing value. (The current build_value_path_recursive ALWAYS overwrites and has no such arm — that arm is the actual F0 code change.) No data divergence (the unranked record is dropped on reopen), but the burn is mandatory for liveness.

compare_and_swap (NH2 — silent regression). Today CAS is REJECTED under route_overlay() (char atomic_ops.rs:~209, byte :~248) — the overlay has no value-level CAS. Arbitrary-V tries never hit that reject today (they're owned). The instant eligibility flips (F2), every arbitrary-V compare_and_swap returns InvalidOperation — a working owned feature breaks. DECISION: supply a generic overlay value-CAS (no feature regression). Design — a generic compare_and_swap_cas_durable_default(&self, key_bytes, expected: Option<V>, new: V) -> Result<bool> in DurableOverlayWrite, Order-A:

  • read the current leaf value (overlay navigate, non-faulting); compare to expected; on mismatch return Ok(false) with NO WAL (a failed CAS is a no-op — burns no LSN, punches no watermark hole);
  • on match: append WAL Upsert{term, value: bincode(new)}, then a path-copy + root-CAS loop that re-checks expected against the freshly-loaded root each iteration (so a concurrent change between the initial read and the publish correctly fails the CAS), commit_rank_and_mark;
  • Comparison = BINCODE BYTES, not PartialEq (Round-2 correction): DictionaryValue has NO PartialEq, and the existing public compare_and_swap compares by serializing both values and comparing bytes (c_bytes == e_bytes, char atomic_ops.rs:~237, byte :~280). The generic overlay value-CAS does the SAME — bincode expected + the loaded leaf value, compare bytes — needing only Serialize (already a supertrait). NO PartialEq bound anywhere.
  • Recheck-failure-after-WAL exit (Round-2 — data-loss/liveness): the WAL Upsert is appended before the CAS loop; if the per-iteration recheck finds expected no longer matches (a concurrent change), the CAS returns Ok(false) and MUST (i) NOT rank it (the unranked record is dropped on Overlay-regime reopen, so no CAS-returns-false-but-recovery-applies divergence) AND (ii) mark_committed_burned(lsn) (liveness — else the burned LSN stalls the contiguous watermark + checkpoint reclaim).
  • empty term "": the leaf IS the root, so read-compare-then-publish via the RANKED root-CAS (publish_root_cas_ranked baking as_final().with_value(new), returning a generation for commit_rank_and_mark) — NOT the unranked overlay_publish_root_value (Round-5 C-1: it would leave the CAS's Upsert LSN unranked → dropped on Overlay reopen → CAS returned Ok(true) but the value lost across restart, the same G5-NEW-4 data-loss class). overlay_publish_root_value is reserved for the no-WAL reestablish fold (§2.3) only.

If supplying the overlay value-CAS is deferred, the documented FALLBACK is: keep the reject, but F2 must EXPLICITLY carve CAS out of "lock-free for all V" and document that arbitrary-V CAS requires kill_switch_to_owned(). The design RECOMMENDS supplying it (effort M — one value-seam method mirroring upsert + the compare).

NH3 (framing fix): post-G5 the Any value-downcast survives ONLY for increment (counter, legit); it is REMOVED for insert_with_value/upsert/get_or_insert/compare_and_swap (all genericized to the trie's own V). Three value routes drop the downcast, not two.

G-NH4 / G-NH5 (Round-2 — the eligibility-flip surface is WIDER than CAS+get_or_insert). Two more operation classes mis-behave at F2 for arbitrary V; both must be handled at the flip, not deferred to F7:

  • G-NH4 (data-loss) — byte insert_batch/insert_batch_bytes (+ sorted/grouped) DROP values. byte insert_batch_entry_overlay (mutation_api.rs:~354) falls back to membership-only insert_cas_durable for non-{i64,u64} V (char is safe — it delegates to the single-op insert_with_value, so it inherits F0). FIX: genericize insert_batch_entry_overlay over V to route each valued entry through the generic value path (F0).
  • G-NH5 (F2-timing regression) — merge_from/merge_replace/merge_from_batched + merge_from_parallel/merge_from_batched_parallel + begin_document/commit_document. All reject under route_overlay() (the same class as CAS); the instant eligibility flips (F2), they return InvalidOperation for any arbitrary V that used the owned path. The parallel-merge variants (byte parallel_merge.rs:80/char :34 merge_from_parallel; char :~131 merge_from_batched_parallel) are pub, arbitrary-V, feature-gated (parallel-merge) — Round 3 (G5-NEW-3) added them. Round 4 additions: merge_from_batched_grouped (char merge_api.rs:183merge_from_batched_with_options reject :221) — R-3a; and compact (byte compaction_impl.rs:110, V-generic, rejects under route_overlay() :129) — R-3b: compact WORKED for arbitrary V in owned mode, so it is an F2 regression of the SAME class as merge (V4 filed it only under §3.2/R6 — the same mis-classification V3 fixed for merge). F2 must EITHER rework these to overlay OR document "arbitrary-V merge/doc-tx/compact require kill_switch_to_owned()" and carve them out of "lock-free for all V". increment/fetch_add is NOT a regression (R-4, favorable): it was NEVER a working arbitrary-V feature — the owned increment body itself fails for non-numeric V (deserialize-as-i64, char atomic_ops.rs:71/91; comment :51 "Arbitrary V never reaches here"), so carving it loses nothing (a true one-line carve-out, not a feature loss). V1/V2 mis-filed all these under Slice-3/F7; they are F2-flip regressions and belong in the F2 gate's carve-out list. (NOT in this list: merge_lockfree_to_persistent/merge_lockfree_values_to_persistent — those are overlay→owned cache drains, a different class, correctly not arbitrary-V owned features.)

3. PHASE F DESIGN — delete owned + RwLockArc

3.1 F-A — reopen must load directly into the overlay (the prerequisite for deletion)

The problem (verified): every reopen does load-into-owned → reestablishclear_owned (mmap_ctor.rs:431/676 then :483-487). To delete the owned tree, the on-disk image must reconstruct the OverlayNode root without the owned TrieRoot intermediary. No such loader exists (grep load_root_immutable: zero hits).

Two options — assessed (the task asks for both):

  • Option A — load_root_immutable (load straight into the overlay). Write a new loader that reads the arena image into OverlayNode<K,V> directly (mirroring the existing owned load_root_from_disk/disk_load.rs arena walk, but emitting OverlayNode nodes + Child::OnDisk(SwizzledPtr) for unfaulted children). Then reestablish + clear_owned are deleted (no owned tree to clear). Pro: the clean end state; no owned reconstruction at all. Con: a NEW arena→overlay parser is real work + a NEW forward/back-compat surface (the loader must read every existing on-disk format the owned loader reads, incl. buckets, Bucket→ART, on-disk children). The empty-string feature's H1 load path (disk_load.rs 3-edit thread) shows how fiddly the arena loader is.

  • Option B — keep load→owned→reestablish, delete owned ONLY after. Reuse the proven owned loader as a transient reopen-staging buffer, then republish to the overlay and drop the staging buffer immediately. Pro: zero new parser; the proven load path is untouched; back-compat is inherited verbatim. Con: the owned TrieRoot/ChildNode types + their load/serialize/iter paths cannot be deleted (they ARE the staging buffer) — so "delete the owned tree" becomes "delete the owned mutation/read paths but keep the owned load+iter paths."

Recommendation: Option B for Slices 1+2, Option A only if Slice 3 (full deletion) is greenlit. Option B is what makes Slices 1+2 shippable without the parser rewrite: the owned tree stays as a dormant load-staging buffer (it's already exactly that post-flip), and we delete only the genuinely-dead owned write paths (insert_impl/mutation_core.rs owned mutators, ~623 LOC byte) while keeping the owned loader + iter (used by reestablish + compaction). Option A is the "true zero owned tree" end state and is the bulk of Slice 3's effort + risk (a new data-loss-critical parser). Surface this fork to the owner explicitly — Option A is weeks of parser + back-compat work for a code-hygiene payoff, not a runtime win.

3.2 F-B — compaction rework

The problem (verified): compact() rejects under route_overlay() (compaction_impl.rs:129-136) because it rebuilds from the owned tree (empty under the flip) + atomically renames the file (clobbering the durable overlay/WAL). Once arbitrary V flips (G5), compact() is unreachable in production (every trie is overlay-routed) unless kill-switched to owned.

The design — two sub-options:

  • B1 (minimal, recommended for Slices 1+2): leave the reject in place. compact() is only reachable after an explicit kill_switch_to_owned() (which is staying as the owned-mode escape hatch — see §3.3). The reject already documents this (:131-134: "use OverlayWriteMode::OwnedTree"). Zero new code; correct. R15 (Round-4, checkpoint_lock scope): compact() mutates the durable image via a DIFFERENT mechanism than checkpoint (file rename, compaction_impl.rs:~322), NOT gated by checkpoint_lock — so a kill-switched-owned compact() racing an owned-mode checkpoint() is unguarded. In production (overlay-routed) compact is unreachable (the reject), so no race; but the design must EITHER also gate compact under checkpoint_lock OR document owned-mode compaction-vs-checkpoint as single-threaded-by-convention under the degraded kill-switch fallback (checkpoint_lock does NOT cover it — do not over-claim "serializes ALL checkpoints").
  • B2 (overlay-snapshot compaction, Slice 3): rework compact() to build the fresh file from capture_overlay_snapshot() (the watermark-bounded overlay image) instead of compaction_snapshot (owned). This is the "E1-iter-B follow-on" the reject comment already anticipates (:127-128). It must record checkpoint_lsn = committed watermark and retain the WAL post-rename (the overlay durability discipline), NOT the owned next_lsn reclaim. Effort: M; data-loss-critical (a compaction that mis-bounds the WAL reclaim is #41 reborn at file-rewrite scale). Defer to Slice 3.

Recommendation: B1 for now (kill-switch-gated compaction is honest and safe); B2 only if owned-mode compaction must remain a production feature after deletion — which the owner should decide, because if compaction is overlay-only then owned-mode is no longer needed for ANY feature, simplifying §3.3.

3.3 F-C — the kill-switch: what safety it provides, and whether to remove it

What it provides (verified): kill_switch_to_owned (flip.rs:416-421) reverts route_overlay() to false so writes/reads/checkpoint take the owned arm, and on a fresh WAL restamps the Owned regime. It is the documented one-release production fallback if the overlay flip misbehaves, AND it is how owned-only features (doc-tx, trie-merge, compaction, CAS) force the regime they require (overlay_write_mode.rs:728-740).

The tension: "delete the owned tree" and "keep the kill-switch to the owned tree" are contradictory. If the owned tree is deleted (Slice 3 / Option A), the kill-switch has nothing to switch to.

The design decision (staged):

  • Slices 1+2 (owned tree retained as staging buffer): KEEP the kill-switch. It still works (the owned tree still exists). This preserves the production fallback through the risky G5 flip + the lock collapse. This is a key reversibility lever — if arbitrary-V overlay routing regresses in production, kill-switch reverts that trie to the proven owned path (and the owned load+iter+mutation paths are still present in Slices 1+2 under Option B).
  • Slice 3 (owned tree deleted / Option A): REMOVE the kill-switch as part of deletion. Its replacement safety: (a) the create-flip + reopen-flip are by then formally proven + soaked for $\ge$1 release; (b) the durability guarantee no longer depends on an owned fallback (it depends on the WAL + watermark, which are representation-independent); (c) owned-only features (doc-tx/merge/compaction) must EITHER be reworked to overlay (B2-style) OR be explicitly dropped. Removing the kill-switch is the point of no return — it must be the LAST irreversible step, behind explicit owner GO, AFTER the flip has soaked. Do NOT remove it in the same change that flips eligibility.

Recommendation: keep the kill-switch through 1+2; treat its removal as the final gate of Slice 3, separately from everything else.

3.4 F-D — delete the owned tree + dead paths

Scope (Option B, Slices 1+2): delete only the genuinely-dead owned mutation paths once no live writer hits them:

  • byte mutation_core.rs owned mutators (insert_impl_core/owned upsert/owned increment), ~623 LOC — but verify each is not called by the reopen-staging WAL replay (insert_impl_no_walinsert_impl_core IS the replay path per empty-string-value-support.md H7). The owned mutators are NOT fully dead under Option B — WAL replay into the staging buffer uses them. So under Option B, almost nothing owned is deletable (load, iter, AND replay-mutate are all live). This is the honest cost of Option B: it keeps the lock collapse + lock-free writes but defers code deletion.
  • Therefore real owned-tree deletion requires Option A (load-into-overlay) so the staging buffer + its replay-mutators + its loaders all go. That is Slice 3's bulk.

Scope (Option A, Slice 3): delete TrieRoot/ChildNode (byte transitions.rs 1157 LOC, char twin), the owned insert_impl/mutation_core, the owned serializer paths superseded by capture_overlay_snapshot, the owned capture_owned_snapshot arm + publish_owned_and_reclaim seam (overlay_checkpoint.rs:103-109; checkpoint.rs:103,109), the owned arm of checkpoint_route_split (checkpoint.rs:136-149), and the owned arm of the non-blocking checkpoint (mod.rs:1354-1386). Each deletion is compiler-driven (remove the seam method → the trait default's owned arm won't compile → remove the arm).

im already dropped — verified. Cargo.toml has NO im dependency (grep: "NO im dependency"). The old plan's "drop im after Phase F" is already satisfied (Phase A dropped it per the old plan's Phase-A box). Nothing remains — note this and move on.

3.5 F-E — SharedCharARTrie/SharedARTrie Arc<RwLock<…>>Arc<…> (the lock collapse)

The current state (verified):

  • SharedCharARTrie<V,S> = Arc<RwLock<PersistentARTrieChar<V,S>>> (mod.rs:349-350); byte SharedARTrie<V> = Arc<RwLock<PersistentARTrie<V>>> (mod.rs:369). Scope (Round-5 F6): this collapse targets SharedCharARTrie/SharedARTrie ONLY. SharedVocabARTrie = Arc<RwLock<PersistentVocabARTrie>> (persistent_vocab_artrie/dict_impl.rs:220) is a DISTINCT struct (its own RwLock, own fields) and is OUT OF SCOPE — a separate follow-on, NOT covered by this field audit. (Note: the vocab overlay shares PersistentCharNode/OverlayNode, but the vocab trie struct is untouched here.)
  • The ARTrie trait impls take self.read()/self.write() throughout (shared_trait_impl.rs; char mod.rs 1297-1439). Most are reads; the writes are: insert/upsert/increment/remove/merge/checkpoint/enable_eviction.
  • The only write that REQUIRES exclusion-across-I/O for correctness is the owned-arm checkpoint (char mod.rs:1362-1386: self.write()capture_snapshotdowngrade → publish). The mutation writes (insert etc.) DO hold self.write() across their internal WAL-append+fsync I/O (NF-7), but they route through the overlay (lock-free CAS) under route_overlay() and only take self.write() to satisfy the &mut self signature — the exclusion is vestigial, not needed once they're lock-free CAS internally. char/byte asymmetry (Round-3 claim-1): char's overlay-arm checkpoint uses self.read() (mod.rs:1344-1352) — so char checkpoints are NOT mutually excluded today (NF-3); byte's checkpoint() trait impl holds the OUTER self.write() across the ENTIRE inherent checkpoint incl. the overlay arm (shared_trait_impl.rs:134), so byte DOES serialize checkpoints today (and loses that at F4 → checkpoint_lock mandatory, §3.5 PF-1 item 3).

Why the collapse is safe once every live write target is the overlay (G5 done):

  • Mutations are lock-free CAS on the overlay root (insert_cas_durable et al.) — they need &self, not &mut self exclusion. The &mut self on the inherent methods is a vestige; under Arc<…> they become &self (the overlay root is AtomicNodePtr, interior-mutable).
  • The checkpoint's owned arm (the only true write-exclusion user) is gone (Slice 3) or dormant/kill-switch-only (Slices 1+2). The overlay-arm checkpoint is already &self + lock-free.

The design — Arc<PersistentARTrieChar<V,S>> + a dedicated checkpoint Mutex:

  1. SharedCharARTrie<V,S> = Arc<PersistentARTrieChar<V,S>> (drop the RwLock). Same for byte.
  2. Mutation methods take &self (the inherent insert/upsert/increment/remove change &mut self&self; their bodies already route to &self lock-free CAS under the flip). The ARTrie trait impl drops every self.read()/self.write() — it calls the inherent &self method directly on the Arc deref.
  3. A small dedicated checkpoint_lock: Mutex<()> field on the trie. checkpoint() takes let _g = self.checkpoint_lock.lock(); ONLY to serialize concurrent checkpoints (two checkpoints racing the same arena allocator / descriptor / WAL-rotate would corrupt). Writers and readers never touch this mutex — they proceed fully lock-free. The checkpoint body is the overlay-arm capture (capture_snapshot_immutable / capture_overlay_snapshot) + publish-retaining, all &self.
    • Why a Mutex not the old RwLock: the old RwLock excluded writers (the L1 gate). The new Mutex excludes only other checkpoints — writers proceed. This is the whole point of the collapse (max parallelism over reads AND writes).

The data-loss-critical correctness (the heart of the red-team, §5): the old design's "no lost write" rested on the write lock excluding writers during owned capture. The new design's "no lost write" rests on the checkpoint_lsn = committed watermark discipline (overlay_checkpoint.rs:215-261; char persist.rs capture-ordering) — which is already how the overlay arm works, and which already assumes no write-exclusion. Specifically:

  • The overlay capture reads watermark Acquire BEFORE the atomic root load (overlay_checkpoint.rs:226,234), establishing $snapshot \subseteq committed-prefix(watermark)$. Writers committing concurrently are either $\le$ watermark (in the snapshot) or > watermark (retained in WAL, replayed). No write lock is needed for this — it's the Order-A Acquire/Release chain.
  • The capture asserts watermark ≤ synced_frontier (overlay_checkpoint.rs:255-261) — the executable #41 guard.
  • So the collapse does not weaken durability: it deletes a lock the durability proof never relied on. The overlay arm already runs lock-free; the collapse just removes the now-vestigial RwLock wrapper and the dead owned arm. This is the cleanest possible version of the change.

The C2 assert (char-ONLY, debug-only — Round-1 C4). char's owned arm debug_assert!(guard.lockfree_root.is_none()) (mod.rs:1368) would FALSELY fire on a kill-switched-with-overlay-installed trie (kill_switch_to_owned sets route_overlay() false but does NOT clear lockfree_root). Fix: change it to !route_overlay() to match the trait's RES-4 assert (checkpoint.rs:142-146, whose comment already names this bug). Byte needs NO assert fix — byte's non-blocking checkpoint delegates to the inherent checkpoint()checkpoint_route_split → the correct !route_overlay() trait assert (persistence_api.rs:~296). Severity bounded: it's a debug_assert! (a false test/debug panic, not production data-loss).

PF-1 — the owned root becomes interior-mutable; this decouples Slice 2 from Slice 3 (Round-1 RT3 + Round-2 correction). Round 1 proved the V1 phasing wrong: making mutations &self for the Arc collapse strips the OWNED path's &mut self exclusion → a kill-switched-owned mutation racing the owned checkpoint tears the snapshot, which would force F4 to wait for F7 and collapse the Slices-1+2 value. Round 2 then proved the V2 "narrow Mutex<()> + mechanical conversion" resolution itself WRONG: checkpoint_lock does NOT exist today (it is ADDED), and a Mutex<()> CANNOT enable &self owned mutation — the owned root: TrieRoot<V> (dict_impl.rs:~269) / CharTrieRoot<V> has no interior mutability, and the owned mutators ASSIGN self.root + take &mut under a &mut self exclusivity contract. CORRECTED design (the real PF-1):

NF-1 (BLOCKER) — the field audit is WHOLE-STRUCT + governed by an explicit two-tier policy (V5-completed). Under Arc<T> (no outer RwLock), EVERY method reachable on the shared handle must be &self; each one writing a non-interior-mutable field fails to compile. V3 wrapped only root; V4 added three more but was INCONSISTENT — it wrapped overlay_write_mode (an inherent-&mut self-written field) yet omitted four sister fields written by the IDENTICAL category of method. Round 4 enumerated every field. The policy that resolves it (decide per method, apply consistently):

  • Tier-1 — "pre-share configuration" (stays &mut self; NOT in the Arc<T> shared API; NO wrap). Construction-time knobs set on the owned trie BEFORE Arc-wrapping. The DECISION (made below, not left open): the overlay-installers enable_lockfree/flip_to_overlay/reestablish_* are Tier-1 (called only in ctors/reopen pre-share — VERIFIED on NO Shared* trait), so the whole-Option fields they set (lockfree_root/lockfree_cache) need NO wrap. Forward guard: add a debug_assert!(Arc::strong_count == 1) (or keep them off every Shared* trait) so a future edit that calls them at runtime fails loudly rather than silently needing lockfree_root wrapped (this is the Round-2/3/4 category-error — a &mut self write mis-filed as safe — guarded against).
  • Tier-2 — "runtime shared-handle op" (&self; field wrapped). Anything that must work on a live shared trie.

The consistency rule (the V4 inconsistency, fixed): the background-subsystem ENABLE/DISABLE family must be treated UNIFORMLY — enable_eviction/disable_eviction are ALREADY &self (the EvictableARTrie trait on SharedCharARTrie), so eviction_coordinator is unavoidably Tier-2; the consistent choice puts the whole family (memory_monitor, checkpoint_manager, group_commit) in Tier-2 too, so the shared trie has a uniform runtime subsystem-toggle API. kill_switch_to_owned is Tier-2 by design (runtime fallback). durability_policy is read on the write path → Tier-2 (cheap atomic).

Complete field table (char mod.rs:366-493, byte dict_impl.rs:267-379):

FieldDecl (char / byte)WriterTier / Treatment
rootmod.rs:368 / dict_impl.rs:269owned mutators (kill-switch + Option-B WAL-replay), &self-reachable via insert/upsert/removeT2 → RwLock<TrieRoot<V>>
eviction_coordinatormod.rs:451 / dict_impl.rs:297enable_eviction/disable_eviction — ALREADY &self (mod.rs:1822/1832, byte shared_trait_impl.rs:276/286)T2 → Mutex<Option<Arc<…>>> (LEAF lock — see hierarchy)
overlay_write_modemod.rs:391 / dict_impl.rs:353kill_switch_to_owned(&mut self) (flip.rs:416) — runtime fallback; read on the hot route_overlay() path (flip.rs:215)T2 → AtomicU8-backed cell (cheap hot-path read)
dirty_prefixes (byte)— / dict_impl.rs:306owned mutators via record_dirty_path (dirty_tracking.rs:41/97)T2 → Mutex/RwLock (or fold into the owned-state lock)
durability_policymod.rs:447 / dict_impl.rs:289set_durability_policy(&mut self) (wal_helpers.rs:47 / persistence_api.rs:131)T2 (read on write path) → atomic/RwLock [V4 MISSED — NF-1 round-4]
checkpoint_managermod.rs:444 / —enable/disable_epoch_checkpointing(&mut self) (epoch_checkpointing.rs:62/102)T2 (family) → Mutex<Option<Arc<…>>> [V4 MISSED]
memory_monitormod.rs:436 / —enable/disable_memory_monitor(&mut self) (observability.rs:199/223)T2 (family) → Mutex<Option<Arc<…>>> [V4 MISSED]
group_commit (cfg)mod.rs:431 / —enable/disable_group_commit(&mut self) (observability.rs:124/148)T2 (family) → Mutex<Option<Arc<…>>> [V4 MISSED]

Already interior-mutable (NO wrap, verified): the atomics len/dirty/next_lsn/structural_generation/cas_retries/commit_seq/version, the all-atomic retry_stats/cache_stats, prefetcher(Mutex+atomics), committed_watermark(AtomicU64+Mutex), commit_seq_by_data_lsn(Mutex), the Arc/Arc<RwLock> handles (epoch_manager/buffer_manager/arena_manager/wal_writer/retire_list), byte persisted_disk_locations(RwLock). Tier-1 / construction-only (NO wrap, but their writers are &mut self whole-Option/whole-value assignments — kept pre-share, NOT "already IM"; Round-5 F1): wal_config/file_path (no post-open writer), and the overlay-installer fields lockfree_root(Option<AtomicNodePtr>)/lockfree_cache(Option<DashMap>) — set only by enable_lockfree/reopen pre-share (the AtomicNodePtr/DashMap contents are IM, but the Option wrapper is whole-assigned, so the no-wrap rationale is "Tier-1 pre-share", not "already IM").

F3 obligation: grep EVERY &mut self inherent/trait method on BOTH tries and assign each to Tier-1 (document "pre-share only") or Tier-2 (wrap its fields above). The table must be exhaustive — an omitted Tier-2 field is a compile error or an unsafe.

  1. rootRwLock<TrieRoot<V>> (NOT a bare Mutex<()>): SAFE interior mutability so the &self-converted owned mutators can owned_root.write() (NO new unsafe; the Mutex<()>/UnsafeCell routes would add unsafe + an UNSAFE_INVENTORY.tsv reconciliation, which this avoids), confined to the DORMANT owned path. NF-4 (ctor sites): wrapping root breaks every direct self.root =/&mut self.root site — at minimum mmap_ctor.rs:44 (newEmpty), :431/:676 (reopen inner.root = root) + io_uring_ctor.rs twins, dirty_tracking.rs:57 (propagate_dirty_to_root), mod.rs:2102 (eviction's owned descent), mutation_core.rs:91/131/353. These run SINGLE-THREADED at open BEFORE the Arc is shared (correctness-safe — the unsynchronized .write() at open is sound), but they are real mechanical surface PF-1 must enumerate (not "mechanical/S").
  2. NF-2 CORRECTION — the downgrade is DELETED, not "preserved." V3 claimed RwLock<TrieRoot> "PRESERVES the downgrade semantics (mod.rs:1357/1384)." VERIFIED WRONG: the live downgrade (mod.rs:1384 — the ONLY downgrade site; :1357 is not one) operates on the guard from self.write() (:1362) = the OUTER trie RwLock that Phase F DELETES. The readers it admits (contains/get_value via self.read()) become LOCK-FREE &self post-collapse. So the property is OBSOLETED, not preserved: post-collapse the owned checkpoint simply takes owned_root.read() for capture, and owned-arm readers run lock-free regardless — there is no guard to downgrade. (Do NOT attempt to "preserve the downgrade" on owned_root — there is no shared reader on that lock to admit.)
  3. checkpoint_lock: Mutex<()> (NF-3 CORRECTION — LOAD-BEARING, not "redundant"). Add a NEW checkpoint_lock: Mutex<()> (F3) to serialize concurrent CHECKPOINTS. V3's "the RwLock write guard did this incidentally" is FALSE for the overlay arm: char's overlay-arm checkpoint returns holding only self.read() (mod.rs:1344-1352), so two concurrent checkpoint() calls do NOT exclude each other today — they race capture_snapshot_immutable + publish_immutable_snapshot_retaining_wal (block-0 descriptor + arena alloc). This is reachable in production NOW for eligible V (the create-flip is wired via apply_create_flip mmap_ctor.rs:89, despite the stale "INERT pre-flip" comments at mod.rs:1339/overlay/checkpoint.rs:125/persistence_api.rs:286 — NF-5; sweep those when touching the area), so checkpoint_lock is (a) a LOAD-BEARING fix for a likely PRE-EXISTING concurrent-checkpoint race on the char overlay arm (surface to owner; the lock closes it regardless of Phase F), and (b) MANDATORY at F4 for byte (byte serializes checkpoints via the outer self.write() today — shared_trait_impl.rs:134 — and loses that at the collapse). Gate it with a real two-checkpoint + reopen test (the loom Model abstracts the descriptor, so loom validates LSN accounting but NOT the descriptor race — the only protection is checkpoint_lock).
  4. Eviction (RT6) + the LOCK HIERARCHY (Round-4 — the V4 "no new ordering" was too glib). The eviction reclaim callback mutates the owned tree → takes the owned_root lock (OR); the existing drop-before-join discipline (disable_eviction drops the guard before shutdown().join(), char mod.rs:1827-1837 / byte shared_trait_impl.rs:~286) is re-established for OR. Round 4 found the V4 claim "different locks $\Rightarrow$ no new ordering" wrong: the eviction-coordinator Mutex (EC) gains two new in-edges — the callback reads EC under OR (OR→EC, mod.rs:~1738) and the eviction-on checkpoint publisher reads EC under checkpoint_lock (CK→EC, persist.rs:~735). With the owned checkpoint's CK→OR, that is a CK/OR/EC graph; it is acyclic ONLY under a documented discipline. Adopt the hard hierarchy CK > OR > EC (acquire in that order; EC is a LEAF — never held across an acquisition of CK or OR, and never across a worker join). The current drop-before-join already honors it; promote it from incidental to a stated, tested invariant (a loom/stress gate: checkpoint(+eviction) ‖ disable_eviction ‖ a writer).

Result: overlay writers/readers take NOTHING (lock-free CAS — Slice 2's max-parallelism payoff, delivered NOW); the dormant owned path serializes on owned_root (OR); concurrent checkpoints serialize on checkpoint_lock (CK); the eviction coordinator on EC (leaf). Lock order CK > OR > EC, EC leaf. It DECOUPLES F4 from F7: Slice 2 lands independently, so the §1.3 "Slices 1+2 $\approx$ 90% value" framing is SOUND. Re-cost: PF-1 is a whole-struct interior-mutability pass (M→M+), not "mechanical/S" — wrap the COMPLETE field set above (8 fields, Tier-2) + thread the locks through the (now &self) owned mutators/readers/checkpoint/eviction/subsystem-toggles + the ctor/&mut self.root sites (NF-4) + document the Tier-1/Tier-2 split per method. No new unsafe.


4. PER-PHASE PLAN — edit intent, why-correct, verification, reversibility/gate

Ordering principle: reversible/low-risk first; the three irreversible flips LAST, each individually gated. Every phase: cargo nextest run --features persistent-artrie --no-fail-fast green ($\ge$ baseline 2610/3/0) + verify-formal-correspondence.sh exit 0 + 0-new-unsafe. Disk tests use target/test-tmp (real disk), never tmpfs.

Slice 1 — G5 (route arbitrary V through the overlay)

F0 — generic value-write path + the two extra value routes (REVERSIBLE; inert).

  • Edits: lift build_value_path_recursive to impl<V: DictionaryValue,S> with value: V (char lockfree_cas.rs:1986; byte :1189); add to DurableOverlayWrite (durable_write.rs, mirroring the increment template :220-275): the value-publish seam — SPLIT into value_insert_publish_inner (insert-once: abort-on-present via AlreadyExists) + value_upsert_publish_inner (always-write), per §2.2/§2.6/R-2, or one seam with an insert_once: bool discriminator (both variants: NO is_empty() branch — build_value_path_recursive(&root,&units,0,value) at units==[] IS the ranked empty-term publish, §2.2/G5-NEW-4; do NOT route "" through the unranked overlay_publish_root_value) + insert_cas_with_value_durable_default (insert-once: re-check presence INSIDE the CAS loop; on a concurrent-insert win return Ok(false)+now-present value AND mark_committed_burned(lsn) — §2.7 NH1/G5-NEW-2) + upsert_cas_durable_default + get_or_insert generic (§2.7 NH1) + compare_and_swap_cas_durable_default (§2.7 NH2 — the overlay value-CAS; comparison = BINCODE BYTES, Serialize-only, NO V: PartialEq bound (G5-NEW-5: DictionaryValue has none); failed-recheck-after-WAL exit = no-rank + mark_committed_burned(lsn)) + genericize byte insert_batch_entry_overlay over V (NH4/G5-NEW-4 — it drops arbitrary-V values today, mutation_api.rs:~354; char already delegates to the single-op); char/byte impl the new seams; rewire get_or_insert/compare_and_swap to the generic overlay path under route_overlay() (NEVER fall through to owned for eligible V — that is the NH1 data-loss + NH2 regression fix).
  • Why correct: the new methods are unreachable until eligibility flips (F-flip below); the generic path is byte-equivalent to the proven u64/i64 path (same recursion, same Order-A skeleton). The u64/i64 durable wrappers (:1765/:1881) become thin callers of the generic default (DRY).
  • Verify: a #[cfg(test)] test that insert_cas_with_value_durable_default::<String> on a flipped-in-test <String> trie writes+reads (drive via a test-only flip_to_overlay override, like the M2a tests). Full suite green (the existing u64/i64 paths now go through the generic default — the counter+value correspondence suites are the oracle).
  • Reversible: delete the new methods; the wrappers revert to inline.
  • Gate: none (inert, additive).

F1 — third reestablish fold + read-route arm (REVERSIBLE; inert for ineligible V).

  • Edits: add reestablish_overlay_value + overlay_publish_value seam to LockFreeOverlay (flip.rs, mirroring reestablish_overlay_counter :473-502); add the third dispatch arm (lockfree_cas.rs:328); add the arbitrary-V arm to overlay_route_get_value (flip.rs:545).
  • Why correct: the dispatch arm + read arm are only reached for eligible arbitrary V (still false until the flip). The fold reuses the proven D1 owned_* readers + clear-owned-LAST.
  • Verify: #[cfg(test)] reopen round-trip for a test-flipped <String> trie (write→checkpoint→reopen→get_value and write→reopen-WAL-replay→get_value), mirroring m2a_reestablish_counter_round_trip. D1 grep gate still green (no new owned_* seam).
  • Reversible: delete the fold + arms.
  • Gate: none (inert).

F2 — IRREVERSIBLE: flip overlay_eligible_v() for all V (GATED, owner GO #1).

  • STATUS (DONE): both gates are landed. overlay_eligible_v() returns true for all V unconditionally, and the second, smaller gate (the default-on flip) has been applied: the overlay-arbitrary-v Cargo feature has been removed — arbitrary-V overlay routing is now the production default whenever persistent-artrie is enabled. The kill-switch remains the per-trie runtime fallback. The historical (pre-removal) plan is preserved below.
  • Edits (historical): overlay_eligible_v() returns true for all V (byte overlay_write_mode.rs:466; char :119). Originally landed behind a Cargo feature overlay-arbitrary-v (default OFF initially) so it lands dark; the create-flip/reopen-flip activate only with the feature. The kill-switch remains the per-trie runtime fallback.
  • Why correct: F0/F1 supply the write/read/reestablish for arbitrary V; recovery is already V-agnostic (§2.5). The flip only activates code proven inert-correct in F0/F1.
  • Verify: the FULL arbitrary-V matrix (insert-with-value/upsert/reopen-both-paths/concurrent-writers/recovery-ranked + unranked-drop negative control) for a representative non-counter V (e.g. String, a struct). A multi-writer + checkpointer soak on <String> (real disk). The arbitrary-V reader-eviction question (§2.4) RESOLVED (confirm no overlay eviction for arbitrary V, or accept last-checkpoint-consistent reads + test it).
  • Reversible: feature-flag OFF + per-trie kill-switch. After a soak release, flip the feature default ON (a second, smaller gate).
  • Gate: owner GO #1 (the arbitrary-V flip). This is one of the three irreversible flips.

Slice 2 — the lock collapse

F3 — fix the C2 assert + add checkpoint_lock (REVERSIBLE; the checkpoint_lock is a LOAD-BEARING fix, NF-3).

  • Edits: change the non-blocking owned-arm assert (mod.rs:1368) from lockfree_root.is_none() to !route_overlay() (matching checkpoint.rs:142); add checkpoint_lock: Mutex<()> field to both tries; ALL checkpoint entry points take it.
  • Why correct / NOT redundant (NF-3 correction): the assert fix removes a latent false-fire under kill-switch-with-overlay (§3.5). The mutex is NOT "redundant-but-harmless" — char's overlay-arm checkpoint holds only self.read() (mod.rs:1344), so two concurrent checkpoint() calls already race the block-0 descriptor + arena alloc TODAY (a likely pre-existing bug for eligible V; surface to owner). The mutex CLOSES that race at F3 (before the collapse), and is MANDATORY at F4 for byte (byte's outer self.write() serializes checkpoints today — shared_trait_impl.rs:134 — and loses it at the collapse). So F3 is a real concurrency fix, not a no-op.
  • Verify: a kill-switch-then-checkpoint test (assert no longer false-fires) PLUS a two-concurrent-checkpoints + reopen test on an eligible-V flipped char trie (must lose no term — this is the NF-3 descriptor-race gate; the loom Model abstracts the descriptor so it cannot substitute). Full suite green.
  • Reversible: mechanically reversible (delete the field), but FORWARD-ONLY in practicecheckpoint_lock closes the NF-3 concurrent-checkpoint data-loss race, so reverting it REOPENS a data-loss bug (Round-4). Treat as a forward fix, not a freely-revertible one.
  • Gate: none (the assert fix + the lock are both safe-to-land; the lock is a strict improvement).

F4 — IRREVERSIBLE: Arc<RwLock<…>>Arc<…> (GATED, owner GO #2).

  • Edits: SharedCharARTrie/SharedARTrie drop RwLock (mod.rs:349, :369); mutation inherent methods &mut self&self; the ARTrie/EvictableARTrie trait impls drop every read()/write() and call inherent &self methods on the Arc; wrap the COMPLETE Tier-2 field set (§3.5 PF-1 table) for interior mutability. Lock order CK > OR > EC: checkpoint() takes checkpoint_lock (CK); the owned-arm checkpoint + owned (kill-switched) mutators take owned_root (OR); the eviction coordinator is EC (leaf). The owned-arm checkpoint (mod.rs:1354-1386, kill-switched-owned only) holds BOTH CK (it IS a checkpoint → serializes against other checkpoints) and OR (to exclude a concurrent owned mutator from tearing the owned snapshot — CK alone does not do that), in CK > OR order; the "NOT checkpoint_lock" phrasing (§3.5/R3/RT6) means OR is what provides the owned-root exclusion, not that CK is absent. No new unsafe.
  • Why correct: §3.5 — every live write target is the overlay (lock-free CAS, &self); the durability proof rests on the watermark, not the lock. The mutex serializes concurrent checkpoints. Readers + writers never block.
  • Verify: a high-concurrency soak (N writers + M readers + a checkpointer, real disk) showing no reader/writer ever blocks on the trie (only checkpoints serialize); every committed key survives reopen (the #41 witness). Send/Sync still auto-derive (the trie has no new raw pointers; AtomicNodePtr is Send/Sync). The loom no-lost-write + checkpoint-concurrent-with-writer tests (persistent_lockfree_durable_loom.rs) re-run — they already model lock-free writers + concurrent checkpoint, so they cover the collapse.
  • Reversible: NOT reversible (public type signature change Arc<RwLock<T>>Arc<T> is a breaking API change + the &mut&self ripple). Mitigation: land behind a major-version bump; keep a deprecated Arc<RwLock<>>-shaped shim type for one release if downstream needs it.
  • Gate: owner GO #2 (the lock collapse — API/Send-Sync surface).

Slice 3 — owned-tree deletion (OWNER-OPTIONAL; highest effort, lowest runtime value)

F5 — load_root_immutable (Option A loader) (REVERSIBLE; alongside).

  • Edits: new arena→OverlayNode loader alongside load_root_from_disk; gated by a config flag (load-into-overlay vs load-into-owned). Both run; correspondence test: identical terms/values both loaders.
  • Verify: a both-loaders correspondence proptest (every on-disk format — bucket, ART, Bucket→ART, on-disk children, empty-term root value); back-compat (old files read identically).
  • Reversible: flag selects the old loader.
  • Gate: none (alongside).

F6 — compaction B2 (overlay-snapshot compaction) (REVERSIBLE) — IF compaction must survive owned deletion.

  • Per §3.2 B2. Data-loss-critical (watermark-bounded WAL retain post-rename). Or skip + keep B1's kill-switch-gated owned compaction (then owned compaction dies with the kill-switch in F7).
  • Gate: none (alongside) until wired.

F7 — IRREVERSIBLE: delete owned tree + kill-switch (GATED, owner GO #3 — the FINAL step).

  • Edits: switch reopen to load_root_immutable; delete reestablish+clear_owned (no owned tree); delete TrieRoot/ChildNode + owned mutators/serializers/readers; delete the owned checkpoint arm + its seams; delete kill_switch_to_owned + OverlayWriteMode::OwnedTree; delete the owned-only feature paths (or confirm reworked to overlay).
  • Why correct: nothing live reaches owned after F5 (reopen) + F6 (compaction) + F2 (all V flipped). Compiler-driven deletion (remove a seam → its caller won't compile → delete the caller).
  • Verify: full suite green after each deletion sub-step; the formal gate; 0-new-unsafe (deletion only REMOVES code). A final reopen + recovery + concurrent soak with the owned tree GONE.
  • Reversible: NO. This is the point of no return (no owned fallback exists after).
  • Gate: owner GO #3 (delete the owned tree + kill-switch). MUST be after F2/F4 have soaked $\ge$1 release.

5. RED TEAM — attacking my own design

RT1 (data-loss, the headline) — does the RwLockArc collapse open a lost-write window the write lock was closing? Attack: the old owned-arm checkpoint excluded writers via self.write() (mod.rs:1362). Remove the lock → a writer commits concurrently with capture → its WAL record is appended-before-capture but committed-after → archived out of recovery's reach while not in the snapshot (#41). Defense (verified): the collapse only removes the lock from the overlay arm, which never held the write lock (mod.rs:1344 is self.read()). The owned arm (the lock holder) is dead (Slice 3) or kill-switch-only (Slices 1+2, where there is no concurrent overlay writer because route is owned). The overlay arm's safety is the watermark capture-ordering (overlay_checkpoint.rs:226-261), which is lock-free by construction and TLC-proven with NO writer-exclusion (LockFreeDurableCheckpoint.tla: CaptureCheckpoint at :132 checks only ckptPhase = "Idle", not writer-idle; NoLostWriteUnderLockFreeCommit at :200 holds under USE_WATERMARK=TRUE). The lock the collapse removes is one the no-lost-write proof never used. This is the strongest defense — the formal model is already more permissive than today's code. Residual: the synced_frontier ≤ watermark assert (overlay_checkpoint.rs:255) must hold under the collapse — it does (it reads the same atomics). Keep it as the runtime tripwire.

RT2 (data-loss) — arbitrary-V recovery drops values. Attack: a durable arbitrary-V Insert{value: Some(bincode(V))} is dropped on reopen (unranked, or bincode fails). Defense: §2.5 — the generic durable write RANKS via commit_rank_and_mark (§2.2 step 3), so reconcile_lww_with_regime's Overlay-rank path retains it (recovery.rs:290). Bincode round-trips through DictionaryValue: DeserializeOwned. Negative control required: an unranked arbitrary-V record IS dropped (test it — mirrors the counter discipline). Bincode-failure handling (refined by §2.5/G5-NEW-6, R2 — two distinct cases): (i) NEW G5 durable-write/serialize paths PROPAGATE bincode errors, never .ok()-swallow (the empty-string H7 rule) — a swallowed serialize on the write path is silent loss; (ii) the PRE-EXISTING owned-replay/reestablish apply sites that G5 reuses (mutation_core.rs Insert/Upsert/CAS arms; byte overlay_write_mode.rs:375 deserialize::<V>(...).ok()) currently WARN-DROP a genuinely-CORRUPT record, and that stays by DECISION (matches the membership/counter discipline; avoids one bad record bricking recovery). VALID arbitrary-V values are never swallowed on either path. Record the decision in the GAP_LEDGER so RT2's bar is honestly scoped, not over-claimed.

RT3 (lock-ordering / liveness) — the kill-switch-owned checkpoint under Arc (no write lock). Attack: after F4, an owned-mode checkpoint (kill-switched trie) has no write lock; a concurrent &self owned mutation (the owned mutators are now &self) races the owned capture → torn owned snapshot. Defense — REAL HOLE, RESOLVED (PF-1, §3.5; the V2 mechanism below was REFUTED in V3 — current resolution stated): the owned tree is &mut self-mutated today; making mutations &self for the lock collapse strips the owned path's exclusion too. ~~V2 (REFUTED): gate the &self-converted owned mutators on the existing checkpoint_lock — "mechanical."~~ Round 2/3 proved this WRONG on two counts: (a) checkpoint_lock does NOT exist today (it is ADDED in F3), and (b) a Mutex<()> CANNOT give &self mutation of the non-interior-mutable owned root (dict_impl.rs:269/mod.rs:368). CURRENT RESOLUTION (V3-V5, §3.5 PF-1 + R3): wrap the owned root in RwLock<TrieRoot<V>> (the owned_root/OR lock — safe interior mutability, NO new unsafe) as part of the complete 8-field whole-struct interior-mutability audit (root, eviction_coordinator, overlay_write_mode, dirty_prefixes, durability_policy, checkpoint_manager, memory_monitor, group_commit), under a Tier-1(&mut self pre-share)/Tier-2(&self runtime) policy; the owned-arm checkpoint captures under owned_root.read() (the downgrade is DELETED — owned-arm readers become lock-free, NF-2); a SEPARATE new checkpoint_lock: Mutex<()> serializes concurrent checkpoints (R-NF3, load-bearing); lock order CK > OR > EC. The overlay path (every live production write post-G5) takes nothing (lock-free CAS). This DECOUPLES F4 from F7: Slice 2 lands independently with full overlay parallelism, while the dormant owned/kill-switch path serializes on OR (no torn owned snapshot). Re-cost: whole-struct M+ (not "mechanical"). The V1 conclusion ("collapse only when owned is GONE / defer F4 to F7") was over-conservative; the interior-mutability audit restores the Slices-1+2 value for a local, correctness-preserving change.

RT4 (correctness) — what breaks when owned is deleted (Slice 3)? Attack: doc-tx, trie-to-trie merge, CAS, compaction — all owned-mode features (overlay_write_mode.rs:733-735 lists them) — break with no owned tree. Defense: each must be reworked to overlay OR explicitly dropped BEFORE F7. Verify the live caller set of each (find_callers_by_signature / change_impact_analysis) — if a feature has external callers, it can't be silently dropped. This is a scoping gate, not a code gate: the owner must decide per-feature (rework vs drop) before F7. I flag it as a blocker on F7, not a design detail.

RT5 (data-loss) — the arbitrary-V non-faulting read returns stale/absent under eviction. Attack: §2.4 — the overlay read is non-faulting (resident-finals); an evicted arbitrary-V leaf reads as absent → false "not found" → caller overwrites → lost value. Defense — RESOLVED to a non-issue in V2 (§2.4, Round-1 verified): overlay finals are NEVER freed in production for ANY Vevict_node_at_path walks the OWNED tree only (char mod.rs:~2103, byte shared_trait_impl.rs:~343), which is empty under the flip, so eviction is a structural no-op (persist.rs:~2351-2369). The walk is over the owned tree generically, so arbitrary V inherits the proven non-eviction property and the resident-finals read is exact. Pin with a test (overlay finals survive force_eviction on an arbitrary-V flipped trie) + a forward constraint: any future overlay-eviction wiring (persist.rs:2360 TODO) reintroduces this hazard.

RT6 (liveness/DEADLOCK) — the eviction coordinator lock vs checkpoint/owned-root. Attack: the eviction coordinator takes self.write() today (shared_trait_impl.rs:286); under Arc it becomes a wrapped field (EC, Mutex<Option<Arc>>) — a new lock-ordering surface. Defense — UPDATED (Round-4 R14; the V2 "no new ordering" was WRONG): there ARE two new edges — the eviction reclaim callback reads EC under the owned-root lock (OR→EC, mod.rs:~1738) and the eviction-on checkpoint publisher reads EC under checkpoint_lock (CK→EC, persist.rs:~735; the publisher publish_overlay_snapshot_retaining_with_eviction runs inside the CK-held checkpoint). Combined with the owned checkpoint's CK→OR, that is a CK/OR/EC graph. RESOLUTION (§3.5 PF-1 item 4, R14): adopt the hard hierarchy CK > OR > EC with EC a LEAF — never held across an acquisition of CK/OR or across a worker join. The existing drop-before-join discipline (disable_eviction drops the guard before shutdown().join(), shared_trait_impl.rs:~286, since the worker callback takes the trie) ALREADY honors it; promote it from incidental to a stated, tested invariant (a loom/stress gate checkpoint(+eviction) ‖ disable_eviction ‖ writer). A cycle would deadlock the production trie (costs money).


6. RISK TABLE (data-loss rows flagged 🔴)

#ChangeRiskSevGuard
R1 🔴F4 RwLockArc (checkpoint vs writer)lost write if watermark ordering is wrong without the lockDATA-LOSSwatermark capture-order assert (overlay_checkpoint.rs:255); LockFreeDurableCheckpoint.tla (already no-writer-exclusion); concurrent soak + reopen #41 witness
R2 🔴F2 arbitrary-V flip — recoveryunranked value dropped on reopenDATA-LOSSRANK via commit_rank_and_mark; unranked-drop negative control. (Corrupt-record bincode failures stay warn-drop by decision — §2.5/G5-NEW-6; VALID values are never swallowed)
R3 🔴F4 — kill-switched-owned mutation under Arctorn owned snapshot (owned loses &mut exclusion)DATA-LOSSRESOLVED (PF-1, §3.5 — Round-4 completed): COMPLETE 8-field interior-mutability audit w/ a Tier-1(&mut self pre-share)/Tier-2(&self runtime) policy: rootRwLock, eviction_coordinator/checkpoint_manager/memory_monitor/group_commitMutex<Option<Arc>> (uniform subsystem family), overlay_write_mode/durability_policy→atomic, dirty_prefixesMutex (NF-1; the V4 table missed the last four); downgrade DELETED (NF-2). NO new unsafe. Decouples F4 from F7. Re-cost whole-struct M+
R-NF3 🔴F3/F4 — concurrent checkpoints under Arc (and ALREADY on char overlay arm)torn block-0 descriptor + arena alloc → lost terms on reopenDATA-LOSSRESOLVED (PF-1 item 3, §3.5): checkpoint_lock: Mutex<()> serializes checkpoint↔checkpoint (NOT checkpoint↔compact — R15) — LOAD-BEARING (char overlay-arm holds only self.read() today, NF-3), added at F3 (closes the likely pre-existing race), mandatory at F4 for byte. Two-concurrent-checkpoint + reopen test (loom can't see the descriptor)
R-G5NEW4 🔴F0/F2 — durable empty-term "" value writeunranked Insert LSN → dropped on Overlay reopen → insert_with_value("",v) lostDATA-LOSSRESOLVED (§2.2): value_publish_inner has NO is_empty() branch — build_value_path_recursive(&root,&[],0,value) at depth 0 IS the RANKED empty-term publish (as u64 lockfree_cas.rs:1765 does); the unranked overlay_publish_root_value is ONLY for the no-WAL reestablish fold. Empty-term arbitrary-V reopen test
R4 🔴F2 read route arm — non-faulting under evictionfalse-absent arbitrary-V read → overwrite → lossDATA-LOSSRESOLVED (§2.4): evict_node_at_path walks owned-only (empty under flip) → overlay finals never freed; read exact. Pin w/ a force-eviction-survives test + forward constraint
R10 🔴F0/F2 — get_or_insert falls through to dead owned (NH1)silent value loss (unranked WAL record dropped) post-flipDATA-LOSS§2.7: genericize to overlay value seam, NEVER fall through; arbitrary-V get_or_insert reopen test
R11 🟠F2 — compare_and_swap rejected for arbitrary V (NH2)working owned feature regresses to InvalidOperation at the flipHigh§2.7: supply generic overlay value-CAS via BINCODE-BYTE compare (not PartialEq) + the no-rank/mark_committed_burned recheck exit; OR carve+document CAS-needs-kill-switch
R12 🔴F0/F2 — byte insert_batch drops arbitrary-V values (NH4)silent value loss (membership-only fallback)DATA-LOSS§2.7: genericize byte insert_batch_entry_overlay over V (char already delegates to the single-op)
R13 🟠F2 — merge/document-tx regress at F2 not F7 (NH5)InvalidOperation for arbitrary-V that used the owned pathHigh§2.7: F2 carve-out — rework to overlay OR document kill_switch_to_owned()-required + carve out of "lock-free for all V"
R5 🔴F7 reopen-into-overlay (load_root_immutable)new parser mis-reads a format → silent corruption on reopenDATA-LOSSF5 both-loaders correspondence proptest (every format + back-compat) BEFORE F7
R6 🟠F7 delete owned-only featurescompaction + the reopen-staging machinery break at F7 (doc-tx/merge/CAS break EARLIER at F2 — R11/R13)HighRT4: per-feature rework-or-drop decision (scoping gate on F7)
R7 🟠F2 eligibility flip is irreversiblea broken arbitrary-V overlay in prodHighCargo feature (dark land) + per-trie kill-switch + soak before default-on
R8 🟠F4 API break (Arc<RwLock>Arc)downstream compile breakageHighmajor-version bump + deprecated shim one release. Blast radius (NF-6): IN-REPO $\ge$15 test/bench/example files call .read()/.write() on shared handles (e.g. tests/persistent_shared_concurrency_correspondence.rs, tests/persistent_nonblocking_checkpoint_correspondence.rs, benches/lockfree_flip_benchmark.rs, examples/exp_checkpoint_throughput.rs) — they are part of the F4 changeset, not just downstream. kill_switch_to_owned callers use the BARE inner trie (survive). Check the liblevenshtein sibling per the cross-repo gate before F4
R9 🟡F6 overlay-snapshot compaction WAL reclaim#41 at file-rewrite scaleMedwatermark-bounded retain + post-rename retain test
R14 🟠F4 — eviction Mutex (EC) lock-orderingCK/OR/EC cycle → production trie DEADLOCK (costs money)DEADLOCKRESOLVED (PF-1 item 4, §3.5 — Round-4): hard hierarchy CK > OR > EC, EC a LEAF (never held across CK/OR/a worker join); existing drop-before-join honors it → promote to a stated+tested invariant (checkpoint‖disable_eviction‖writer loom/stress gate). The V4 "no new ordering" was wrong (2 new edges OR→EC, CK→EC)
R15 🟠F4 — checkpoint↔compact under kill-switchtorn descriptor (compact renames the file, not gated by checkpoint_lock)High (kill-switch-only)§3.2: gate compact under checkpoint_lock too, OR document owned-mode compaction-vs-checkpoint as single-threaded-by-convention under the degraded fallback. Unreachable in production (overlay rejects compact)

The single most dangerous change: R1 (the RwLockArc checkpoint collapse). It is the one change that, if wrong, silently loses an acknowledged write in production (which costs money). Its guard is unusually strong and already in place: the durability proof was re-derived under no-writer-exclusion in LockFreeDurableCheckpoint.tla (the CaptureCheckpoint transition has no writer-idle precondition — verified :132-139), the watermark capture-ordering + synced_frontier assert is the executable refinement (overlay_checkpoint.rs:226-261), and the loom suite already models lock-free-writers-concurrent-with-checkpoint. The collapse removes a lock the proof never used — so the danger is not "does the new design work" (the proof says yes) but "did I correctly identify what the overlay arm held" — which Round 3 SHARPENED: char's overlay-arm checkpoint holds only self.read() (mod.rs:1344), which means it never excluded concurrent CHECKPOINTS either (NF-3 / R-NF3) — so the collapse is preceded by adding the load-bearing checkpoint_lock to serialize checkpoints (a fix the read-guard never provided), and the residual write-vs-checkpoint durability is the watermark discipline, not any lock. The residual owned-arm danger is R3 (the owned arm losing &mut exclusion under Arc), RESOLVED by the COMPLETE 8-field interior-mutability audit (V5/NF-1: rootRwLock; the subsystem family eviction_coordinator/checkpoint_manager/memory_monitor/group_commitMutex<Option<Arc>>; overlay_write_mode/durability_policy→atomic; dirty_prefixesMutex) under a Tier-1/Tier-2 &mut self-vs-&self policy, with the downgrade DELETED (NF-2) and the lock hierarchy CK > OR > EC (EC leaf) preventing the eviction deadlock (R14), no new unsafe. So F4 lands independently of F7, at a re-costed whole-struct M+ (not the original mechanical/S).


7. FORMAL-VERIFICATION PLAN

The decisive finding: the RwLockArc checkpoint change needs NO new TLA spec — the existing LockFreeDurableCheckpoint.tla already subsumes it. Verified:

  • The spec models "writers commit with Order A ... with NO lock excluding the checkpoint" (docstring :5-9).
  • CaptureCheckpoint (:132) fires on ckptPhase = "Idle" alone — writers run throughout (:131 comment: "NO writer-exclusion: writers continue throughout").
  • NoLostWriteUnderLockFreeCommit (:200), DurablePrefix (:188), ImmutableSnapshotIsClosed (:191), CaptureEqualsPublishFrontier (:195), RecoveredNeverInventsState (:204) all proven under USE_WATERMARK=TRUE; the _Unsafe.cfg (appended-frontier) exhibits the losing trace.

So the spec is already the proof for the post-collapse code. The collapse makes the code match the model (today the code is stricter than the model — it holds a lock the model doesn't). Obligation: state this explicitly in the design doc + GAP_LEDGER (the collapse closes the code-vs-model gap, it doesn't open one). Re-run TLC on both .cfgs as a regression gate at F4 (no spec edit).

What DOES need formal/loom attention:

  1. G5 arbitrary-V value-write (F2): the value path is path-copy-then-root-CAS — structurally identical to the membership/value insert the overlay model already abstracts (LockFreeOverlayDurableReplay.tla treats terms as an opaque present set, every transition "published by the root CAS" — empty-string-value-support.md §5.2). Arbitrary V is "just another member of present carrying an opaque value" — no new spec, but a loom gate (write-V ‖ write-V' same key ‖ read) proving the root-CAS arbitration (last-writer-wins) holds, mirroring the empty-string loom gate (persistent_lockfree_overlay_loom.rs). The same-key value-race (first-committer vs last-writer) semantics gap (arbitrary-v-overlay-genericization.md R1) must be pinned by a BTreeMap<String,V>-oracle proptest. Empty-term arbitrary-V (G5-NEW-4): add a loom/reopen gate that durable insert_with_value("", v) survives reopen (it must use the RANKED depth-0 publish, NOT the unranked overlay_publish_root_value — the negative control is the unranked variant losing "" on reopen, mirroring the empty-string C2c gate).
  2. F4 collapse: loom checkpoint-concurrent-with-writer already exists (persistent_lockfree_durable_loom.rs) and models the exact scenario; re-run it post-collapse (it should pass unchanged — it never modeled a lock). Two concurrent checkpoints (NF-3 correction): this concurrency is NOT new to the collapse — char's overlay-arm checkpoint already takes only self.read() (mod.rs:1344), so it is reachable TODAY for eligible V; the checkpoint_lock closes it. CRUCIAL: the loom Model abstracts away the block-0 descriptor + arena allocator, so a two-checkpoint loom schedule validates LSN/watermark accounting but CANNOT see the real descriptor/arena race — the descriptor-level protection is solely checkpoint_lock, gated by a real-disk two-concurrent-checkpoints + reopen-loses-nothing test (not loom). Add both: the loom schedule (accounting) AND the real-disk test (descriptor). Lock-hierarchy gate (R14): add a loom/stress schedule checkpoint(+eviction) ‖ disable_eviction ‖ writer exercising the CK > OR > EC order + the EC-leaf/drop-before-join invariant — a cycle would deadlock the production trie.
  3. F7 owned deletion: no formal change (deletion removes paths the specs don't model); the correspondence suites (persistent_nonblocking_checkpoint_correspondence.rs, etc.) are the oracle.

Memory-efficient policy: TLC under systemd-run -p MemoryMax=…, tiny CONSTANTS (2 writers / contiguous LSNs / USE_WATERMARK both polarities); loom $\le$3 threads / 2 keys; disk tests on target/test-tmp.


8. CRITICAL FILES (the load-bearing set for implementation)

  • /home/dylon/Workspace/f1r3fly.io/libdictenstein/src/persistent_artrie_core/overlay/flip.rsLockFreeOverlay trait: add reestablish_overlay_value fold + overlay_publish_value seam + the arbitrary-V arm of overlay_route_get_value (:531); reuse publish_root_* (:655-666). The D1 contract (:24-44) governs the new fold.
  • /home/dylon/Workspace/f1r3fly.io/libdictenstein/src/persistent_artrie_core/overlay/durable_write.rsDurableOverlayWrite trait: add the generic insert_cas_with_value_durable_default/upsert_cas_durable_default + the SPLIT value-publish seams (value_insert_publish_inner insert-once / value_upsert_publish_inner always-write, §2.6/R-2) + generic get_or_insert/compare_and_swap_cas_durable_default (mirror the increment template :220-275). The Order-A ordering (:17-43) is sacred.
  • /home/dylon/Workspace/f1r3fly.io/libdictenstein/src/persistent_artrie_char/lockfree_cas.rs — genericize build_value_path_recursive (:1986) over V; the u64 durable wrappers (:1765,:1881) become callers of the shared default; the reestablish_overlay_dispatch third arm (:328-345). (Byte twin: src/persistent_artrie/lockfree_cas.rs:1189.)
  • /home/dylon/Workspace/f1r3fly.io/libdictenstein/src/persistent_artrie_char/overlay_write_mode.rs (and byte twin src/persistent_artrie/overlay_write_mode.rs:466) — the overlay_eligible_v() flip (the single irreversible eligibility line, :119/:466).
  • /home/dylon/Workspace/f1r3fly.io/libdictenstein/src/persistent_artrie_char/mod.rsSharedCharARTrie type (:349-350); the non-blocking checkpoint route-split + the C2 assert fix (:1332-1387, the lockfree_root.is_none()!route_overlay() fix at :1368); the RwLockArc collapse + checkpoint_lock. (Byte: src/persistent_artrie/mod.rs:369 + src/persistent_artrie/shared_trait_impl.rs:134.)
  • /home/dylon/Workspace/f1r3fly.io/libdictenstein/src/persistent_artrie_char/mmap_ctor.rs — the reopen-into-owned path (:431,:676,:483-487) that F5/F7 replace with load_root_immutable; the create-flip gate (:90); the ctor self.root = sites broken by the RwLock<TrieRoot> wrap (:44,:431,:676; NF-4).
  • The PF-1 whole-struct field-audit files (F3/F4 interior-mutability pass, §3.5; the re-costed M+ centerpiece of Slice 2) — the Tier-2 field writers that become &self: char observability.rs (enable/disable_memory_monitor :199/:223, enable/disable_group_commit :124/:148), epoch_checkpointing.rs (enable/disable_epoch_checkpointing :62/:102), wal_helpers.rs (set_durability_policy :47), dirty_tracking.rs (byte :41/:97), mutation_core.rs (owned mutators &mut self.root char :91/:131, byte :353); plus the eviction lifecycle (enable/disable_eviction, char mod.rs:1822/1832, byte shared_trait_impl.rs:276/286) for the EC leaf lock + drop-before-join.

Supporting (verification): formal-verification/tla+/LockFreeDurableCheckpoint.tla (already no-writer-exclusion — the proof for the collapse); tests/persistent_lockfree_durable_loom.rs (re-run for F4 + add two-checkpoint schedule); src/persistent_artrie_core/recovery.rs:353-375 (verified V-agnostic — no change); src/persistent_artrie/compaction_impl.rs:129-136 (the route-overlay reject — B1 keep / B2 rework).

Can you improve this documentation?Edit on GitHub

cljdoc builds & hosts documentation for Clojure/Script libraries

Keyboard shortcuts
Ctrl+kJump to recent docs
Move to previous article
Move to next article
Ctrl+/Jump to the search field
× close