Invariants / DC-LEDGER-VALUE-01

DC-LEDGER-VALUE-01

DC true enforced

Ade's authoritative UTxO OUTPUT asset quantity preserves the full non-negative Cardano Word64 domain (0 ..= 2^64-1) via the OutputAssetQuantity(u64) newtype. BOTH MultiAsset definitions (the codec-layer ade_types::mary::value::MultiAsset and the ledger-layer ade_ledger::value::MultiAsset) hold BTreeMap<Hash28, BTreeMap<AssetName, OutputAssetQuantity>>; ade_ledger REUSES the ade_types newtype (it does not define its own). A negative output quantity is UNREPRESENTABLE by type. Output arithmetic is CHECKED: multi_asset_add uses checked_add (overflow -> a structured LedgerError), multi_asset_sub/value_sub use checked_sub and an output underflow (subtrahend qty > minuend qty) is the structured authoritative LedgerError::AssetUnderflow { policy, name } -- it NEVER wraps and NEVER produces or deletes a negative entry. The canonical output encoding is a CBOR unsigned integer (u64) on every authoritative encode path (the snapshot write_multi_asset and the fingerprint write_multi_asset), so a quantity > i64::MAX round-trips faithfully, and -- the BYTE-IDENTITY guarantee -- a representable quantity (<= i64::MAX) encodes to the SAME bytes as the prior signed form (a non-negative CBOR int and a u64 <= i64::MAX are both a CBOR major-0 uint). The snapshot decoder reads the output quantity via a dedicated non-negative reader (read_output_quantity); a negative CBOR integer in an output position is a structured terminal StructuralReason::NegativeAssetQuantity, never coerced. Mint/burn is the DISTINCT signed MintBurnQuantity(i64) (DORMANT until S-13 mint decoding): it is never used as a MultiAsset map value type and therefore cannot enter an output bundle. This widens the authoritative value model so the faithful u64 quantities the Stage-2 MemPack decoder already produces (DC-MITHRIL-05) can be promoted into UTxOState and persisted without loss -- the downstream release-blocker DC-MITHRIL-05 named is exactly this slice's subject. SCOPE: OUTPUT domain only; mint decoding + signed conservation remain future work (S-13).

Source: docs/clusters/LEDGER-VALUE-CORRECTNESS/SLICE-1-output-asset-quantity-u64.md; the DC-MITHRIL-05 downstream release-blocker (Ade's i64 MultiAsset model could not safely validate real Cardano outputs with quantities > i64::MAX); user directive 2026-06-23 (the authoritative value model is widened to the non-negative Word64 domain via a distinct OutputAssetQuantity(u64) newtype -- NOT a universal i128, NOT a u64->checked-i64->reject adapter, NOT a truncating cast; checked output arithmetic with a structured underflow error; the canonical prune_zeros normalization stays; mint/burn stays the distinct signed MintBurnQuantity(i64) and cannot enter outputs; representable values stay byte-identical so existing replay/snapshot/codec tests are unchanged)
Introduced in: LEDGER-VALUE-CORRECTNESS-S1

Enforcement trace

Code

Tests 8

multi_asset_word64_add_sub_round_trips_above_i64_max
multi_asset_sub_underflow_returns_asset_underflow
multi_asset_add_overflow_returns_error
negative_output_quantity_is_unrepresentable
utxo_state_word64_multi_asset_quantity_round_trips
utxo_state_negative_output_quantity_is_rejected
representable_quantity_encodes_byte_identical_golden
stage2_mempack_word64_output_survives_snapshot_recovery

CI 1

ci_check_value_quantity_domain.sh

Cross-references

Attack rationale

A real Cardano UTxO output can hold up to 2^64-1 of a token (i64::MAX is the common max-supply mint; some exceed it). With the value model storing i64, three losses were possible at the authority boundary. (1) Silent truncation/wrap: promoting a decoded snapshot output with a quantity > i64::MAX into an i64 store would wrap to a negative or a different magnitude -- a different ledger than the network's, undermining replay and conservation. Closed by the u64 storage type (a quantity > i64::MAX is representable and round-trips byte-exactly). (2) Underflow wrap on subtraction: the prior unchecked *current -= qty on i64 could wrap on an adversarial/corrupt input; on u64 a naive -= would wrap to a huge value. Closed by checked_sub -> the structured AssetUnderflow (fail-closed, never a fabricated huge balance, never a negative). (3) Signed-mint contamination: a signed mint/burn delta entering an output bundle could encode a negative output quantity. Closed by type -- MultiAsset holds only OutputAssetQuantity; the signed domain is the distinct dormant MintBurnQuantity that is never a map value. The snapshot decoder additionally rejects a negative CBOR integer in an output position (NegativeAssetQuantity terminal) rather than coercing it. BYTE-IDENTITY is the safety hinge: because a representable value encodes identically, the change is provably behaviour-invariant for the entire existing corpus (replay/snapshot/codec tests unchanged) while extending the representable domain.

Evidence notes

Introduced as ONE mergeable slice LEDGER-VALUE-CORRECTNESS S1 (2026-06-23). The blast radius was narrower than the worst-case estimate: the codec (ade_codec mary/alonzo/babbage/conway tx.rs) keeps the multi-asset bundle OPAQUE (Option<Vec>), and the seed importer (ade_runtime seed_import/importer.rs) already builds intermediate maps as u64 and writes CBOR uints -- neither touches the typed MultiAsset, so neither changed. The typed-quantity sites were ade_types::mary::value, ade_ledger::value, the snapshot utxo_state codec, and the fingerprint writer (plus test fixtures). The MINT field stays opaque/undecoded (parse_mint_field still returns an empty bundle; the mary.rs value_add(consumed_ma, minted) stays a no-op). The fingerprint write_multi_asset moved from write_i64_cbor to write_uint_canonical(qty.0) -- byte-identical for non-negative values, so the v2 UTxO fingerprint is unchanged for the live corpus (all live MultiAssets are empty today). The snapshot signed helpers write_int_i64/read_int_i64 were removed from the OUTPUT path (mint is opaque). check_non_negative's asset-sign loop became type-dead and was removed; its only caller (mary.rs:65) kept the min-UTxO check. cargo test -p ade_types -p ade_ledger green; ade_codec + ade_runtime + ade_testkit (replay) green; ci_check_value_quantity_domain.sh PASS (negative-controlled: it fails on a stray BTreeMap<AssetName, i64> and on an unchecked *current -= qty). NOT a claim of mint/burn decoding or signed cross-epoch conservation (S-13).