AdeAtlas
Invariants / DC-EVIEW-04

DC-EVIEW-04

DC derived enforced

The durable reduced-UTxO checkpoint -- the "minimal native state" (S3b Option B). A disk-backed redb store of TxIn -> (Coin, ReducedStakeRef), built from Ade's bootstrap UTxO, that S3b-2 advances per epoch boundary and S3c aggregates. It is the SINGLE ledger authority's OWN reduced-UTxO projection -- a GREEN durable CACHE of a BLUE-derivable projection (a pure function of admitted blocks, reconstructible by replay if lost/corrupt) -- NOT a permanent parallel StakeView, NOT a second stake computation, and NEVER on the live follow/forge path (the live producer stays track_utxo=false; the checkpoint is built/advanced lazily off the per-block path). The reduced record drops datums/scripts/multi-asset, keeping (Coin, ReducedStakeRef); ReducedStakeRef is the Conway-specialized Base(StakeCredential) | NonContributing (option b) -- Ade only snapshots at Conway, where pointer stake is retired and only base credentials contribute, so reduce_txout reuses classify_output_stake_ref(addr, Conway): Base(cred) -> Base, everything else (pointer/enterprise/Byron/reward/ malformed) -> NonContributing (the era gate is thus trivially satisfied; it is applied generally at S3c). CRASH-SAFE: build_from clears any prior partial build, writes all entries (durable redb commits), then writes the completeness marker LAST in a separate commit -- a crash before the marker leaves an INCOMPLETE checkpoint (is_complete()==false) that is rebuilt, never mistaken for complete. REPLAY-EQUIVALENT: the fingerprint is a hash chain over the canonical records (encode_reduced_record) in TxIn key order -- two builds from the same reduced UTxO yield a byte-identical checkpoint + fingerprint (DC-WAL-03 lineage). DURABLE across reopen.

Source

docs/clusters/EPOCH-CONSENSUS-VIEW/SLICE-3b-1-reduced-utxo-checkpoint.md; docs/clusters/EPOCH-CONSENSUS-VIEW/SLICE-3b-replay-window-materialization.md

Introduced in
EPOCH-CONSENSUS-VIEW-S3b-1

Enforcement trace

Code

Tests 12

  • base_output_reduces_to_base_credential
  • enterprise_and_byron_are_non_contributing
  • pointer_output_is_non_contributing_at_conway
  • reduced_stake_ref_round_trips_canonically
  • decode_fails_closed_on_bad_tag_or_truncation
  • record_encoding_is_deterministic_and_canonical
  • build_then_query_and_complete
  • durable_across_reopen
  • replay_equivalent_two_builds_byte_identical
  • fingerprint_changes_with_content
  • crash_mid_build_is_incomplete_then_rebuilds
  • fresh_store_is_incomplete

CI 1

Cross-references

DC-EVIEW-01DC-EVIEW-02DC-EVIEW-03OP-MEM-02

Strengthened in

EPOCH-CONTINUITY-ACTIVATION-ECA-5

Attack rationale

The checkpoint must not (a) be mistaken for complete when a crash truncated the build -- the completeness marker is written LAST in a separate durable commit, so any partial build (entries without the marker) reads is_complete()==false and is rebuilt (never a wrong stake snapshot from a partial UTxO); (b) drift from the chain -- it is a pure function of admitted blocks (reconstructible by replay), a durable cache not an independent authority, so two builds are byte-identical and a lost/corrupt checkpoint is rebuilt; (c) become a second stake authority -- it is the ledger transition's own reduced UTxO, consumed by the single boundary authority (S3c), not a parallel computation; (d) leak onto the live path -- the live producer stays track_utxo=false, the checkpoint is built/advanced lazily off the per-block path and is referenced by no follow/forge/recovery call site; or (e) bake the era gate into the stored record -- the Conway-specialized Base|NonContributing is correct for every Conway snapshot (Ade's only case), and the general era gate stays at S3c. The crash-safety reuses the same redb Immediate-durability backend DC-EVIEW-01 proved under its 1000-kill harness.

Evidence notes

Introduced at EPOCH-CONSENSUS-VIEW S3b-1 (2026-06-20), the first half of S3b (Option B, user-chosen over replay-from-bootstrap), scoped + implemented ALONE. The grounding crux: materialize_rolled_back_state seeds a window from a checkpoint, but Ade's live path keeps NO UTxO (every live checkpoint track_utxo=false), so the window needs a full-UTxO start that does not exist live -> Option B persists a compact reduced UTxO the window advances. ReducedStakeRef = option (b) Conway-specialized (user). Reuses: the redb anchor backend (DC-EVIEW-01) used DURABLY; Slice-2 classify; the bootstrap UTxO import (admission/bootstrap.rs:165, tapped before drop(utxo):298 -- the live BOOTSTRAP WIRING is a later step / S3b-2, NOT in S3b-1, keeping it self-contained + no live-path change). 12 hermetic tests (6 ade_ledger reduction: base->Base, enterprise/Byron/pointer->NonContributing, canonical round-trip, fail-closed decode, deterministic record; 6 ade_runtime store: build/query/complete, durable-across-reopen, replay-equivalent-two-builds, fingerprint-changes+rebuild-discards-prior, crash-mid-build-incomplete-then-rebuilds, fresh-store-incomplete). cargo test -p ade_ledger + -p ade_runtime green. NO advance (S3b-2), NO aggregation (S3c), NO snapshot/emission (S3d/e), NO live wiring, NO track_utxo=true on live, NO leader/header use. Next: S3b-2 advances this checkpoint per boundary (reduced ledger apply + cert/pool/reward + PointerMap population) and wires the bootstrap reduction.