AdeAtlas
Invariants / DC-MITHRIL-05

DC-MITHRIL-05

DC true enforced

Faithful Word64 multi-asset quantity on the snapshot-import path. The native V2 LedgerDB tables MemPack TxOut decode keeps every multi-asset quantity as a full u64 (Word64) -- NEVER truncated, saturated, or cast to i64. A persisted/imported snapshot quantity is never lost: a real Cardano output can hold up to 2^64-1 of a token (i64::MAX is the common max-supply mint; some exceed it), so the decoder's TxOutValue holds BTreeMap<PolicyId, BTreeMap<AssetName, u64>> and the whole-tables canonical commitment serializes each quantity big-endian as u64. The surrounding decode is fail-closed

  • faithful: the compact (non-CBOR) TxOut value is decoded via the grounded MemPack layout (the 6-way constructor tag; CompactAddr / Addr28Extra base-address reconstruction with the explicit BE->LE hash double-flip and the payment/stake hash byte-order asymmetry; CompactValue ada-only + multi-asset rep; datum/script with the ORIGINAL inline-datum / script wire bytes PRESERVED, never a re-encode where Cardano hashes the wire bytes); endianness is explicit (no host-endianness contract); CONSUME-EXACTLY is enforced at every nesting boundary; every unknown tag / address form / script language / over-long VarLen is a structured TERMINAL error (no opaque keep-bytes); the tables decode is era-bound to Conway taken from the SAME snapshot's state (the Stage-1 NES), never the tables file or a CLI flag; and the whole-tables commitment is a deterministic blake2b chain over the canonically (ascending-TxIn) sorted UTxO (a non-sorted map is terminal). DERIVED: Cardano multi-asset quantities are Word64-compatible in this decode path. RELEASE BLOCKER (separate, downstream): Ade's i64 MultiAsset model cannot yet safely validate every real Cardano UTxO containing quantities > i64::MAX -- full ledger validation of such outputs is gated until the value-model quantity is widened (this is NOT cleanup). Validated: 300000 real preprod TxOuts decode faithfully (all 6 tags, consume-exactly); a cardano-cli query utxo oracle cross-check matched 10/10 (6 tag-2 Addr28Extra base addresses + coins) -- closing PO#1; the i64::MAX / i64::MAX+1 / u64::MAX quantities round-trip exactly.

Source

docs/clusters/EPOCH-CONSENSUS-VIEW/SLICE-MITHRIL-VERIFIED-ANCHOR-IMPORT.md; user directive 2026-06-23 (Stage 2 = the V2 LedgerDB tables + MemPack TxOut COMPATIBILITY decoder, NOT a CBOR reader; faithful u64 quantity with the i64 ceiling logged as a separate BLOCKING downstream validation obligation, never widen MultiAsset inside the snapshot-decoder slice -- different authority surface; preserve original script/inline-datum bytes where Cardano hash/identity rules require wire bytes; the meaningful oracle comparison is real TxIn -> native decode -> full TxOut vs cardano-cli query utxo; whole-tables proof = a deterministic commitment over sorted TxIn -> canonical TxOut, not just a count)

Introduced in
EPOCH-CONTINUITY-ACTIVATION-ECA-2-3-4

Enforcement trace

Code

Tests 9

  • multiasset_quantities_preserved_exactly_as_u64_no_i64_cast
  • coin_varlen_overflow_is_terminal
  • addr28_base_address_reconstruction_round_trip
  • staking_credential_tag_is_fail_closed
  • compact_value_ada_only_and_multiasset
  • txout_dispatch_tag0_tag5_and_fail_closed
  • tables_commitment_deterministic_era_bound_and_sorted
  • varlen_big_endian_7bit_matches_real_coin
  • decode_real_preprod_tables_commitment

CI 1

Cross-references

DC-MITHRIL-04

Attack rationale

The boundary is the highest-risk consensus moment: an N+1 block's leader is decided by the N+1 stake distribution, so any path that lets an N (seed) view decide leadership or validate an N+1 header at an N+1 slot forges/admits against the WRONG distribution. Three failure classes are closed mechanically. (1) Split-authority: if header validation and the forge read DIFFERENT view sources, they can diverge at the swap (one promoted, one stale) -- closed by the ONE holder both resolve fresh (criteria a/e; cross_consumer_identity test). (2) Stale-epoch routing: even with one holder, a wrong boundary predicate / slot->epoch map could use the N view for an N+1 slot -- closed by the slot-aware mode-aware guard (criterion c), which is TERMINAL for a continuity-capable producer whose boundary should have activated (a missed promotion is a routing bug, not a skip) while a seed-only limited producer past its supported epoch merely no-forges (the mode is a CANONICAL recovered contract, not an ambient flag that two builds could set differently). (3) Recovery forgery: a restart could republish a promoted view that was never legitimately derived if it trusted a parsed WAL record -- closed by recover_at_boundary, which RE-DERIVES the candidate from the durable window replay and promotes ONLY if it reproduces the record's entire identity (the tamper test flips view_canonical_hash -> terminal). The guard does NOT fall back to the seed view in any wrong-epoch case (no silent degradation to a stale-but-available distribution). Header validation stays gated-fail-closed (the epoch-gated holder rejects an N+1 block under a seed view before acceptance), so the wrong-epoch admit is already closed; the structured AuthorityEpochMismatch classification there is deferred diagnostic refinement, not missing enforcement.

Evidence notes

Introduced as ONE mergeable slice EPOCH-CONTINUITY-ACTIVATION ECA-2/3/4 (2026-06-22). Built on DC-EPOCH-06 (durable-before-visible recovery primitives: recover_active_view / activation_record_matches / resolve_activation_record, reused verbatim) + DC-EPOCH-12 (to_pool_distr_view projection) + DC-EPOCH-13 (no semantic gate) + DC-CINPUT-06 (the v4 sidecar consensus-profile hashes the recovery re-derivation reads from the store, never CLI). Phases (internal checkpoints, NOT separate commits): 1 validation onto the one holder (byte-identical); 2 deterministic EviewActivationInputs from durable state; 3a project+promote the one holder; 3b forge reads authority.pool_distr_view() (byte-identical seed path); 3c the mode-aware guard at the forge + header gated-fail-closed; 4 recover_at_boundary (warm-start verified recovery). ade_node lib 373 green. The EpochAuthorityMode (SeedOnly{supported_epoch} | ContinuityRequired{source_binding, activation_profile_commitment, target_epoch_policy}) is built at relay setup from the EVIEW package presence (eview_activation Some => ContinuityRequired with the consensus_profile_commitment + SetSnapshotLag{2}; None => SeedOnly) and recovered identically on warm-start. CLOSE CLAIM (binding): 'ECA-2/3/4 implements a deterministic, crash-recoverable authority transition in hermetic tests. It does not prove unattended public Preview continuity until ECA-5 crosses a real boundary.' ECA-5 (the live 1335->1336 boundary, no manual arming/restart/import) is the separate release proof; make NO continuous-operation claim until a real boundary crosses without intervention AND Model A cert-state is tested across >= 2 boundaries/recovery cycles. NETWORK IDENTITY: network_magic is currently sourced from the CLI (not the v4 sidecar); the recovery is fail-closed on a wrong magic -- recover_at_boundary_wrong_cli_network_magic_is_terminal_no_partial_recovery proves a disagreeing CLI magic re-derives a candidate that cannot reproduce the durable record -> a structured terminal EpochViewPostPromotionMismatch, no partial recovery, no fallback, no altered authority. Persisting network_magic in the seed sidecar (so warm-start derives network identity SOLELY from durable state; the CLI is checked for operator-mismatch only, never used as authority) is the separate follow-on slice NETWORK-IDENTITY-DURABILITY, deferred to after ECA-5 (user 2026-06-22: do not widen the v4 durable-schema work nor blur the epoch-authority-transition proof by folding it in).