WalOp::OrDelta frame + codec + store-seeded recovery fold — the READER [SPEC-349b, 2/3] - #128
Merged
Conversation
- 7 frames encoded by the tree BEFORE WalOp::OrDelta exists: Store frames carrying RecordValue::Lww (with and without expiration_time / entry timestamp), RecordValue::OrMap (with and without tombstones), RecordValue::OrTombstones, a bare-Value legacy payload, plus a Remove - generated via a throwaway test that asserted decode_all -> Complete on the bytes before writing them; the generator is deliberately not part of the diff - provenance matters: these bytes must predate the variant so SPEC-349b AC10(ii-a)'s byte-identity assertion is not self-referential
…answer
- WalOp::OrDelta { delta: OrDelta } at the pinned on-disk shape: exactly one
field, no expiration_time (a delta mutates an existing slot rather than
establishing one, so TTL stays with the Store frames), no r#type field —
serde owns the discriminant and the wire key is camelCase 'orDelta'
- subsumes_on_coalesce() answers false: a per-op delta carries information a
successor cannot re-derive, so retired sequences ride the carry-forward
route instead of resolving early. Match stays exhaustive, no catch-all at
any level. Mutation-proven: flipping the arm to true turns the new inline
predicate test RED
- replay_entry gains a minimal placeholder arm that refuses rather than
silently dropping the mutation; the store-seeded fold lands with the
recovery wiring
- soak_harness bench: compiler-forced classification arm (an OR delta frame
is an OR-side frame). Outside the spec's file ledger but a one-line
zero-cascade arm the exhaustive match forces; surfaced to the orchestrator
Refs SPEC-349b R2.1, R3, AC7(a)
… shape format.rs carries no production change — encode/decode_all are agnostic to the WalOp variant (serde owns the discriminant inside the payload), so the new frame inherits the CRC32C + length-bound + exhaustive-FrameDecodeResult envelope by construction. - FRAME_VERSION doc: replaces the still-open 'explicit-signal choice' clause with the recorded NO-BUMP decision and why a bump breaks one-step compatibility in BOTH directions (UnknownVersion is fail-closed on either side of the bump), plus the CORRECTED two-case cross-binary guarantee. The inherited unqualified 'always fails closed' claim was false: verified against decode_all and decode_segment_or_refuse, a mid-segment frame is Corruption (refuse to start) but an active-segment TRAILING frame is TruncatedTail, which recovery tolerates — and WalWriter's open path then durably truncates the segment, so the mutation is silently dropped, not skipped - FRAME_VERSION == 1 asserted by a test - codec round-trip test for the new variant - golden fixture or_delta_frame_v1.msgpack, asserted byte-equal by an encode test and decode-equal by a decode test; wire key 'orDelta', single field 'delta', no expirationTime and no entry timestamp - legacy corpus test: decode_all -> Complete AND every decoded entry re-encodes byte-identically. Mutation-proven: swapping to_vec_named for to_vec turns it RED, so the encoder-drift class it guards is real Refs SPEC-349b R2, AC6, AC9, AC10(i)/(ii-a)
…very fold - One line, zero cascade: a visibility keyword on an existing item, so no signature, body, lifetime or borrow change and every call site compiles unchanged (the named Max-5 exemption recorded in SPEC-349b's Delta). - The WAL delta fold must normalize its base through the SAME live normalizer the OR write path uses; a second hand-written shape upgrade would be silent delta loss (apply_or_delta is a no-op on a non-OrMap value).
… replay
Replaces the placeholder OrDelta replay arm with the real, store-seeded fold.
- impl OrDeltaFold for WalRecovery: the fold owns no algebra of its own. It
normalizes the base through the live crdt::normalize_to_or_map and applies
through the live crdt::apply_or_delta, in that order (TG-OR-003). Omitting the
normalize would make the apply a silent no-op on a legacy OrTombstones or
cross-kind base — a lost mutation with no error at all.
- WalRecovery::replay_entry's OrDelta arm is per-frame: inner_store.load ->
fold(ONE delta) -> inner_store.add. The durable store is the accumulator, so
no key's deltas are collected out of the replay stream and folded as a window.
- OrDeltaFold::fold now takes a single `delta: &OrDelta` (SPEC-349b R1.5(a),
preferred shape): the withdrawn window-fold becomes unrepresentable rather
than merely discouraged. The receiver is dropped because replay_entry is an
associated fn (reached as WalRecovery::replay_entry(...), the mechanism
R1.5 pins) and holds no WalRecovery value; WalRecovery remains the one
implementor. apply_or_delta's by-value signature is untouched: the fold clones
each delta, on the cold boot path, by design.
- base = None folds onto an empty OrMap: a legitimate first write, never an
error, byte-identical to the init value the live OR closures use.
- Expiration 0 ("no expiry"): load returns no TTL, add requires one, a delta
frame carries none, and the live OR path writes ExpiryPolicy::NONE — so the
fold introduces no TTL drift.
- WalOp::Store OR frames: the code contract now states the ABSOLUTE SET rule
(R4.2/R4.3) at the arm — applied in sequence position, replacing the
accumulated value, never unioned. What licenses it is that a Store OR frame is
a COMPLETE post-state snapshot of one key (live set AND tombstone set); a
partial or live-only OR snapshot would make absolute set unsafe, and a naive
union resurrects tags the snapshot tombstoned. Ordering/window preconditions
are cited as inherited (TG-WB-001 / TG-WAL-003 / TG-WAL-011), not re-derived.
- replay_entry's OR doc bullet is scoped to snapshot framing, which its
monotonicity argument actually covers; delta-frame re-replay idempotency rests
on the idempotent set ops of the live apply instead.
- Inline tests (constructed only inside mod tests, no emitter): first-write,
accumulate-in-store with remove-wins and prune, legacy OrTombstones base, and
snapshot-then-delta absolute set. Mutation-proven: deleting the
normalize_to_or_map call turns the legacy-base test RED with the delta
swallowed and the OrTombstones blob left intact.
The OR contracts in wal/mod.rs are load-bearing: `WalRecovery::run`'s idempotency paragraph is the text the contiguous-success frontier cites to justify keeping post-failure successes and re-replaying the window next boot. A contract that under-describes a frame kind is a false invariant in code. - `include_str!` this file's own source, truncated at the inline `mod tests` so a test's own literal cannot satisfy the assertion it is arguing for - normalize away comment markers, indentation and line wrapping before searching: a bare single-line grep is NOT equivalent, and four of the phrases assert vacuously without it (measured raw=0 / normalized=1 for "checkpoint-window deltas in WAL sequence order", "for OR via snapshot monotonicity", "before any real delta framing lands", "NOT wired to this in Wave 1") - require `WalOp::OrDelta` + `apply_or_delta` of `run`'s doc AND the frontier loop's inline comment, per region rather than per file - require the `TestNonSubsuming` doc to state the role no other variant fills Lands RED on purpose: all three assertions fail against the contracts as they stand, which is what makes the instrument a proof rather than a formality. The rewrites that turn it GREEN follow. Refs SPEC-349b AC8, TG-OR-003.
The steady-state OR path emits pure per-op deltas, and the truncation signal a
WAL checkpoint traditionally carries ("everything before me is truncatable") is
already owned by the applied watermark. A checkpoint cadence would be a second,
weaker, contradictory truncation signal for no benefit, and its K=1 fallback
framing described a recovery mode — "drop to full snapshots on any fold
anomaly" — that the store-seeded replay does not have and must not grow.
- delete `OrDeltaCheckpointPolicy`, `full_snapshot_only()`, `should_checkpoint()`
- delete their two inline tests, which only pinned the deleted arithmetic
The scaffolding was types-only and unwired, so nothing references it anywhere
in the workspace and the emitter loses no capability it was relying on.
Refs SPEC-349b R4.1, AC8 contracts 2-4.
Turns the assertion instrument GREEN. Each contract below was either factually false in the tree or carried prose provenance, which CLAUDE.md forbids exactly as much as a bare spec marker. `OrDeltaFold` (trait + `fold`): the base was defined as the WAL-window checkpoint value — the withdrawn, silent-add-loss model. A snapshot frame read as the base the fold starts FROM discards its content whenever the coalesced store write had not landed, losing every add it carried. The base is the durable store, always; the whole un-applied window replays in sequence order; no frame is a skip hint. Also drops the `deltas` window language the single-delta signature no longer matches. `WalRecovery::run` doc + the frontier loop's inline repetition: OR re-application was justified by snapshot monotonicity alone. There are now two OR frame kinds with different arguments — `WalOp::Store` snapshots by monotonicity (unchanged in substance, merely scoped to that kind), and `WalOp::OrDelta` by set-algebra fold idempotency through `crdt::apply_or_delta` over the whole window from the durable-store base. Monotonicity is not the delta argument. This is the contract the contiguous-success frontier cites, so leaving it under-describing the new kind would have shipped a false invariant in code created by this change. `OrDelta` main doc: keeps the enum-over-`Option`-bag rationale, drops the "models the spec's candidate shape" framing. `OrDelta` version discipline: no longer open, and no longer claims an unqualified fail-closed guarantee. Carries the two-case truth already recorded in `FRAME_VERSION` — mid-segment corruption refuses to start, but a trailing frame on the active segment is tolerated as a truncated tail and durably truncated away, so the mutation is silently dropped. `WalOp::TestNonSubsuming`: its "before any real delta framing lands" justification is spent. Restated to the two roles that survive — the only `WalOp` with no replay semantics, and a non-subsuming op the mixed coalesce case can use without binding to `OrDelta`'s answer. Refs SPEC-349b R2/R3.1/R4.1, AC8 contracts 1 and 5-7, TG-OR-003, TG-OR-004.
…ality oracle - LogModel tracks max_live_millis per key (max on each Live ack, cleared on remove) as a field SEPARATE from the latest-arrival `acked` map O1/O2 use - the value_equality oracle flags a recovered timestamp strictly older than that maximum, so a clobber landing in [latest_arrival, max_live) is no longer invisible on a key whose writes are non-monotone in arrival order - delete the now-false soundness-domain caveat at evaluate_o1 (the monotone-history limitation this change removes); the value-coupling constraint the lww() note cross-references stays and is unchanged - unit-test that a remove clears the reference so a re-created key is compared against its own timestamps only
…reference
- key 0 written 20 -> 30 -> 10 in arrival order, first frame stranded by an
unhealthy flush, blind in-order replay then a stale re-replay of the oldest
frame leaves durable 20 — the true LWW winner (30) is lost
- caught as AckedValueMismatch { expected 30, recovered 20 }: recovered 20 is
NOT strictly older than the latest arrival (10), so the previous reference
point reported nothing over this same run
- the two reference points are compared directly over one modelled history in
driver.rs, so the miss is asserted in-tree and not only by construction
- fixed-path arm proves the max reference does not manufacture a violation out
of out-of-timestamp-order writes
…criminates - add DefectMode::ReReplayOldestFrameGateOn: the stale re-replay seam WITHOUT disabling the RecordValue::Lww merge gate, selected by an independent match in Driver::recover instead of the two seams being set together - strengthen the fixed-path arm of the replay-clobber case with a run under that mode, asserted GREEN: the gate DEFEATS an out-of-order stale frame, rather than the previous arm's trivial "no re-replay happened at all" - the two existing replay-clobber modes keep setting both seams and behave exactly as before
…seam - add OrMutation / OrSlot plus the OrDelta- and OrStore-shaped WorkOp variants and the OR-shaped ModelValue the extension seam reserved - inject every synthetic OrDelta frame through the OBSERVED append path (ensure_wal_seeded -> assign_wal_sequence -> wal_append -> promote / rollback), asserting exactly one observed (partition, sequence) before binding it, so the model's sequence space stays the store's - leave the injected sequence un-applied on purpose: it owns no queued entry, so nothing flushes it and the watermark cannot pass it — the acked, un-applied window state recovery has to reconstruct - track the model's expected slot per key and compare OR keys by semantic view in O1; report a divergence as an acked write recovery did not reproduce - expose the run's final durable values and the tombstone-bytes total the real boot-time reconciliation recomputes, scoped to an isolated gauge
- recovery equivalence across an incarnation loss over all three fold-base shapes: a durable OrMap, an absent record, and a legacy OrTombstones blob — the last two are what make a missing normalize observable - assert the SPEC-345 gauge through the real reconcile walk, never a second copy of its accounting - mixed snapshot/delta windows: a snapshot above the watermark is applied then folded onto (never a skip hint), a snapshot-only legacy window replays, a snapshot replaces rather than unions, and a cross-kind base normalizes with its post-state recorded literally (an Lww base is discarded exactly as a live OR_ADD onto an Lww slot discards it) - prune is an idempotent tombstone-set subtraction, silent on absent tags - structurally verify the injection rides the observed seam only: no raw WAL append anywhere in the harness, and the seam's steps in order
…cases Five cases on the existing crash/recovery harness, all in cases.rs: - stranded base + re-fold idempotency: a real mark_applied + segment GC runs BETWEEN a key's earlier ops and its later un-applied deltas, so the durable store is the ONLY carrier of the base tags; a second arm crashes inside the flushed-but-unmarked window; a third re-folds the oldest un-applied delta onto a store that already reflects it. Mutation-proven in both directions (a fold seeded from an empty OR-Map, and an apply that lost its tombstone dedup, each turn it RED). - OR merge-idempotency in BOTH frame shapes (snapshot, Add delta, Remove delta): the re-replay run and the single-replay run are indistinguishable on the semantic set AND on the tombstone-bytes gauge. - the coalesce ROUTE for a delta survivor, asserted by calling WriteBehindDataStore::coalesce_wal_sequences with the variant's own subsumes answer: nothing is early-resolved and the retired sequences are carried forward. Flipping the predicate turns both halves RED. - the no-emitter proof: each WAL source truncated at its inline test module must hold zero CONSTRUCTION sites (patterns are classified out, since production code destructures the variant in two arms), plus a by-file belt over src/ and a package-wide by-construction belt. The classifier is guarded against silently finding nothing. - a legacy Store/Remove-only WAL replays unchanged, extending the snapshot-only case with LWW and Remove frames. Harness cases: 28 -> 33. write_behind.rs, wal/mod.rs and crdt.rs are unedited; the mutation probes were transient and are reverted.
Both belts are assertions made OVER a filesystem walk, so a walk that returned nothing would satisfy them silently. The walk must now reach the WAL module it truncates a prefix from, and the package walk must reach strictly further than the src/ one — which is what its coverage of the bench binaries rests on.
The OR delta-fold differential recovery proof now exists, so the catalog row names it and the baseline moves in the same change — the gate is an exact-match ratchet in BOTH directions, so either half alone turns CI red. Verified: with the baseline left at 4 the gate fails 'NAKED count dropped to 3 but NAKED_BASELINE still says 4'; at 3 it exits 0 reporting '3 NAKED (baseline 3)'. - INVARIANTS.md TG-OR-003: Scope narrowed to the wired recovery-read side (no emitter yet, frames synthesised at the codec level); Enforcing test names the 13-case tg_or_003_* family and both mutation proofs; Status open -> enforced - scripts/check-invariants.sh: NAKED_BASELINE 4 -> 3 - drop three added SPEC-345 markers from doc comments in favour of the TG-OR-004 invariant ID, per the code-comments convention Refs SPEC-349b R5, AC11, AC15
- The set-union clause licensing the replay merge-gate bypass read as if replay itself unions tags+tombstones; taken that way it invites the tombstone-resurrecting merge the fold exists to avoid. - States the split in place: cross-node CRDT convergence is set-union, replay is an absolute-set replace.
- Count the IMPORT form of the delta variant (a bare `OrDelta { .. }`
behind `use ..::WalOp::OrDelta;`), which no qualified-path search can
see; gated on the file actually importing the variant so the variant's
own field declaration is not read as a construction.
- Excise the inline test module's BODY instead of truncating at its
header: Rust permits items after `mod tests`, and the two codec files
are belt-exempt, so an emitter below them was seen by nothing.
- Strip nested block comments, string literals, and char literals before
scanning, and skip an unbalanced brace instead of aborting the scan.
- Run AC16's negative assertions over a whitespace-free view of the code
so a wrapped `self.wal\n .append(` cannot slip past the needle.
- Guard the new arms against vacuity: the classifier must report the
import form, must not report a declaration, and must report zero over
comment/string/unbalanced text.
- count constructions behind `use ..::WalOp::OrDelta as X;` — the shape that carries the variant's name nowhere near the site that builds it, and the one a review plant proved slipped past the detector GREEN - skip enum BODIES so the codec's own variant declaration stops counting as a construction against a file that imports the variant - state the instrument's threat model where the classifier lives: it catches an ACCIDENTAL emitter; an adversarial one is review's job, and the frame's wire shape is guaranteed by the byte fixture + cross-binary criteria, not by a grep - non-vacuity samples for the rename, self-rename and declaration arms
… own them - the APPLIED watermark's prefix-completeness is TG-WAL-005, the wal_seq-space tracker; TG-WB-001 is the entry-space FLUSHED watermark and its own row calls itself independent of that tracker, so it never carried this property - cite append-time monotonicity in the seq space it actually holds in (TG-WAL-010, per-partition wal_seq), so the four preconditions the replace rests on are each discharged by a row rather than three of four - catalog the fourth as TG-WAL-012: a Store OR frame is a COMPLETE post-state snapshot. It is the load-bearing one and was the only uncatalogued one; its backing is the payload type, recorded with the two-kinds-of-backing notation TG-WAL-009 premise (b) established - 18 -> 19 entries, NAKED unchanged at 3
Recovery normalizes a legacy blob into OrMap, so by the time final_values is read the shape that discriminated the arm is gone — every post-state these cases assert is reachable from any base. A regression making or_legacy_tombstones write an OrMap silently deleted the coverage while leaving them green. - capture the durable value each key holds when the FIRST recovery begins, before replay normalizes it, and name the shape via recovery_base_kind - AC1 pins the three R1.3 bases (OrMap / absent / legacy OrTombstones), AC3(d) pins OrTombstones + cross-kind Lww, AC3(c) pins the live OrMap base without which union and replace are indistinguishable - mutation-verified: writing or_legacy_tombstones as an OrMap reddens exactly AC1 (`[OrMap, absent, OrMap]`) and AC3(d) (`[OrMap, Lww]`); the other 11 cases, which name no base shape, stay green
…h the live one The mirror sat on the arm whose whole job is to reproduce the PRODUCTION write path, where a hand-written copy is the one thing it must not be: a fork that keeps agreeing with the path under test while both drift from the real algebra. normalize_to_or_map is pub(crate) now, so the copy costs nothing to retire. read_state stays a deliberate reimplementation — it reproduces the OLD get-build-put behaviour, which is what the differential compares against.
…body The rename/self-rename samples pushed the test over clippy::too_many_lines. Extracting the guards keeps the belts legible as three belts and leaves the instrument's own discrimination named rather than silenced with an allow. No coverage moves: assert_classifier_discriminates runs first, before any belt reads a zero from the classifier.
… wire bytes
The anti-drift device has two ends — the codec and the differential — and only
the codec end was bound to the checked-in fixture. The harness built its
injected frames from in-memory values, so the envelope around a delta (which
WalOp variant carries it, whether an entry timestamp rides along, what any of
it encodes to) was pinned by nothing: a wire-level drift would leave the proof
green while diverging from the artifact a future emitter has to match.
- Factor the injection's WalEntry construction into `or_delta_frame`, so the
harness has ONE definition of that envelope rather than an inline literal.
- Load the golden fixture in cases.rs at its pinned relative path and run the
golden bytes back through that same constructor: decode, rebuild, re-encode,
require byte equality.
Load-bearing, not decorative — both drift classes demonstrated RED:
* envelope drift (`timestamp: None` -> `Some(..)` in the constructor the
injection seam itself calls) -> struct assertion fails;
* wire drift (`#[serde(rename = "d")]` on the variant's field) -> the golden
bytes stop decoding.
Both mutations reverted; 1746 lib tests pass (was 1745), clippy and fmt clean.
- WalWriter carries allow_or_delta, false in its one production constructor and settable only through a #[cfg(test)] seam, so a release build has no path to the permitted state at all - Wal::append fail-stops at tier P before encoding when a delta frame arrives: nothing may write one until the emitter lands, so its arrival is a programming bug whatever shape of code produced it - the harness opens the guard for exactly the append it injects and closes it again, leaving every other op in the run under the refusal - tier P's doc widened from the sealed-segment instance to the class it now covers - also lands the fold's structural delegation test, which the review found claimed-but-absent; it shares wal/mod.rs with the guard above
…ygiene - the classifier now resolves `use ..::WalOp as X;` and counts `X::OrDelta`, closing the fourth evasion shape; the sample keeping the arm alive lands beside the variant-rename one - its threat model now says what actually holds the no-emitter property: the append boundary's tier-P refusal, which reads the frame rather than the source and so is blind to no emitter shape - the scan stays for early warning — it names the file at review time — but a zero from it is a hygiene result, not the proof - corrects the AC5 doc claim that pointed at a structural assertion which did not exist, now that one does
…emitter - the row said 13 cases and listed 13; the tree carries 14 (the golden-shape case added at the previous review round was never added to the row) - the ac9 entry now records that the text scan is advisory and that the append boundary's tier-P refusal is what holds the property
Cross-vendor review found the grant was a per-writer mode held across the injected append's .await, so it was open to every concurrent appender on that writer for the duration — the exact window a real emitter could ride through. - append now CONSUMES the permit via compare-exchange, so one grant admits one frame; a racing second delta fail-stops whichever loses - the seam stores with Release and reads with Acquire, replacing Relaxed, which gave no cross-thread visibility guarantee either way - the driver asserts its permit was consumed, the same exactly-one discipline it already applies to the append observer - the AC5 structural test asserts its sliced region is non-trivial: the absence half would pass vacuously on a collapsed slice
…ays clean The gate-on arm's assertions all expect a GREEN run, and a seam degraded back to a no-op produces a GREEN run too — so the arm that exists to observe an already-applied frame being folded a second time could hollow out silently. WalRecovery now counts the frames the seam actually re-replays and the driver carries the run total out, so the three arms that rest on it assert it is non-zero. Degrading the mode to a no-op now reddens exactly those three.
Deploying topgun with
|
| Latest commit: |
376e14c
|
| Status: | ✅ Deploy successful! |
| Preview URL: | https://df5edfce.topgun-f45.pages.dev |
| Branch Preview URL: | https://feat-sf-349b-or-delta-reader.topgun-f45.pages.dev |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Part 2/3 of the OR delta-framing split (reader-first). The recovery READER lands before any emitter exists — the wire format is unchanged by construction at this merge point (the variant exists; nothing emits it; a structural append-boundary guard fail-stops any pre-349c emitter).
OrDeltaframes onto the durable inner-store base, normalizing through the livenormalize_to_or_mapand delegating every mutation to the single liveapply_or_deltaseam (single algebra — no second OR implementation; TG-OR-003 flipped NAKED → enforced, 14-case differential family on the cross-incarnation harness, no model fork).WalWriter.allow_or_deltais false in every production constructor; appending a delta frame without the#[cfg(test)]-only flag fail-stops at tier (P) — closing the source-scan arms race (4 evasion shapes found by reviews are all caught at the one door every emitter must pass). The text classifier is demoted to advisory hygiene with an honest threat model. 349c's emitter becomes a one-flag-site handoff under its compat ACs.or_delta_frame_v1.msgpackat both load sites) — serde-drift reddens the differential family.TruncatedTailrollback caveat is recorded as an explicit 349c decision input.Test evidence
4 audits + 4 reviews (v1–v3 adversarial: planted emitters, mutation proofs, fixture anchoring; v4 APPROVED 0/0). Gates: build ✓ · lib 1749/0/1 ✓ · clippy
-D warnings✓ · fmt ✓ ·pnpm test:ts30/0 ✓ · invariants 19/3==baseline ✓. Re-replay seam non-vacuity mutation-proven (degrade → exactly 3 named arms redden).