Invariant Explorer

All 467 registry rules. Search by ID or statement, filter by family / tier / status, isolate drift or enforcement gaps, and export the filtered set. Each row links to its full source → code → tests → CI trace.

Families T True — constitution-level always-true properties DC Derived — invariants derived from the true set CN Classification / constraint — classification-table & attack-surface rules RO Release obligation — release-time discipline OP Operational — deployment / operational practice

Family is the rule's origin/kind — distinct from its tier (true / derived / release / operational). Most align, but CN rules span all tiers.

family
tier
status
467 of 467 rules
IDTierStatusStatementTestsCIFlags
CN-ADMIT-01releaseenforcedSingle admission-mode entry authority: exactly one pub fn in ade_node::admission::runner::run_admission enters the admission tokio runner. No second entry point…31
CN-ADMIT-02releaseenforcedSingle seed-to-snapshot bridge authority: exactly one pub fn in ade_node::admission::seed_to_snapshot converts the imported (UTxOState, ledger_fingerprint, seed…41
CN-ANCHOR-01releaseenforcedSingle BootstrapAnchor mint authority: exactly one pub fn in ade_runtime::bootstrap_anchor::mint produces a BootstrapAnchor with all 6 fields populated (network…51
CN-BUILD-01truedeclaredNo build profile, feature flag, cfg, or optimization mode may alter authoritative semantics or persisted bytes00
gap
CN-BUILD-02truedeclaredAll semantic variability must be explicit runtime protocol data, not hidden compile-time choice00
gap
CN-BUILD-03truedeclaredExactly one semantic interpretation may exist for a given protocol version and bootstrap anchor00
gap
CN-BUILD-04deriveddeclaredOperator configuration may tune transport, logging, and telemetry, but may not silently weaken ledger, consensus, or persistence semantics00
gap
CN-CINPUT-01constraintenforcedThe seed-epoch consensus inputs (epoch, active-slots coefficient, total active stake, and the per-pool active-stake + registered VRF keyhash distribution) persi…30
gap
CN-CINPUT-02constraintenforcedThe SeedEpochConsensusInputs sidecar MUST be populated ONLY through the single shared ade_runtime::seed_epoch_lineage::persist_seed_epoch_consensus_inputs autho…41
CN-CINPUT-03constraintenforcedConsume-side anti-laundering fence: on the node-lifecycle forge path the leadership view MUST be projected from the recovered SeedEpochConsensusInputs surface (…21
CN-CONS-01trueenforcedChain selection must be deterministic for the same candidate chains and protocol observables62
CN-CONS-02deriveddeclaredSupported rollout skew must not allow a single adversarial input to induce persistent honest-node consensus divergence22
CN-CONS-03derivedenforcedAfter temporary partition, honest nodes must converge using only protocol-defined observables and declared emergency procedures31
CN-CONS-04derivedenforcedHeader validation must bind exactly to the accepted body and consensus context131
CN-CONS-05truedeclaredAuthoritative consensus decisions must not depend on wall-clock time, arrival-order races, scheduler interleavings, or OS behavior52
CN-CONS-06releaseenforcedCross-impl acceptance: blocks forged by Ade are accepted by cardano-node when delivered via N2N block-fetch / chain-sync. Evidence is operator-action: a sustain…31
CN-CONS-07releaseenforcedSelf-acceptance bridge + serve provenance. A forged block is NOT eligible for RED broadcast unless Ade's own header validator (PHASE4-N-B path) and body validat…154
CN-CONS-08releaseenforcedReceive-side single admission authority: every block that lands in ChainDb via the receive path passed block_validity with BlockValidityVerdict::Valid. No bypas…62
CN-CONS-IN-01releaseenforcedSingle LiveConsensusInputs importer authority: exactly one pub fn ade_runtime::consensus_inputs::importer::import_live_consensus_inputs converts a cardano-cli J…52
CN-CRYPTO-01truedeclaredVerification belongs to the authoritative core; signing belongs outside it00
gap
CN-CRYPTO-02truepartialAll consensus-relevant hashes must be domain-separated and unambiguous30
gap
CN-CRYPTO-03truedeclaredAll collections with consensus meaning must be ordered deterministically before hashing or comparison00
gap
CN-CRYPTO-04truedeclaredVerification failure must fail once and deterministically; no implicit parser or serialization fallback is allowed00
gap
CN-EPOCH-01derivedpartialStake, rewards, parameter changes, and governance effects may activate only at protocol-defined epoch boundaries70
gap
CN-EPOCH-02truedeclaredAt each slot or epoch point there is exactly one authoritative committee and governance interpretation00
gap
CN-EPOCH-03deriveddeclaredStake snapshots and reward computations must be derivable solely from canonical chain state00
gap
CN-EPOCH-04truedeclaredFuture decisions may not leak into present validation, and later states may not retroactively reinterpret prior checkpoints00
gap
CN-FOLLOW-01trueenforcedProducer / follow authority separation. (a) DETERMINISTIC SELECTION: the same candidate set yields the same selected canonical durable tip (the AO / select_best…81
CN-FORGE-01derivedenforcedThe producer-mode forge handler is a closed transition from CoordinatorEvent::RequestForge { slot, kes_period, ledger_snapshot_ref, chain_tip } to exactly one o…82
CN-FORGE-02derivedenforcedLeader-check splits across the RED/BLUE color boundary: RED produces a VRF proof/output for the slot using the operator's VRF signing key; BLUE verifies the pro…101
CN-FORGE-03derivedenforcedProducer/validator codec symmetry: forge_block emits the era-tagged [era, block] envelope (era = Conway discriminant 7) via the single canonical ade_codec::enco…41
CN-FORGE-04derivedenforcedProducer-side Praos VRF construction must match the Conway/Praos validator authority: the leader VRF proof alpha, the leader-schedule evidence, the LeaderSchedu…51
CN-GENESIS-01derivedenforcedThe Shelley genesis closed-contract parser accepts a real cardano-cli `shelley-genesis.json` and produces a canonical `GenesisAnchor`. Required fields (networkM…62
CN-KES-HEADER-01derivedenforcedThe KES signature in a forged block's header is over the canonical unsigned-header CBOR pre-image — the CBOR encoding of ShelleyHeaderBody (the first element of…31
CN-LEDGER-01truedeclaredapply_block must be a pure deterministic function of prior state and canonical block input00
gap
CN-LEDGER-02truedeclaredSame genesis/bootstrap + same block sequence must yield byte-identical authoritative state00
gap
CN-LEDGER-03deriveddeclaredValidity decisions for transactions and blocks must match the Cardano reference oracle for the same era/protocol version00
gap
CN-LEDGER-04deriveddeclaredAny two supported production versions that may coexist must return the same validity verdict for every consensus-relevant input00
gap
CN-LEDGER-05truedeclaredEach feature must have one semantic processing result; no alternate path may disagree on whether work was already applied, failed, or remains valid00
gap
CN-LEDGER-06truedeclaredFailure-state residue must be deterministic and consensus-neutral00
gap
CN-LEDGER-07truedeclaredUTxO and asset conservation must hold for every accepted transition, except where protocol rules explicitly authorize mint, burn, rewards, or treasury effects10
gap
CN-LEDGER-08truedeclaredNo input or equivalent spend authority may be consumed more than once in an accepted canonical chain00
gap
CN-LEDGER-09derivedpartialWitnesses must bind exactly to the intended body, certificates, withdrawals, governance actions, and scripts for the era61
CN-LEDGER-10deriveddeclaredConway governance and certificate transitions must occur only through explicit legal state transitions00
gap
CN-MEM-01derivedpartialUntrusted inbound work must be admitted through deterministic bounded policies before consuming scarce authoritative resources81
CN-MEM-02operationaldeclaredMempool pressure and peer churn must not starve block validation, chain selection, or persistence00
gap
CN-MEM-03deriveddeclaredUnder overload, work shedding must follow deterministic policy, not timing-dependent collapse00
gap
CN-MEM-04deriveddeclaredMempool acceptance rules must never contradict block and ledger acceptance rules for the same authoritative semantics00
gap
CN-META-01truedeclaredEvery claimed invariant must have at least one mechanical enforcement point00
gap
CN-META-02truedeclaredEvery consensus-relevant failure mode must have a deterministic structured error shape00
gap
CN-META-03truedeclaredEvery equivalence claim must be reproducible from named fixtures, oracle versions, and replay inputs00
gap
CN-MITHRIL-01constraintenforcedA Mithril-sourced seed may bootstrap only after a verified binding: the Mithril manifest's attested {network_magic, genesis_hash, certified_point, certificate_h…52
CN-NET-01operationaldeclaredA block producer must not accept arbitrary public peer connectivity; it may connect only through trusted relay topology00
gap
CN-NET-02operationaldeclaredRelay paths must be geographically and topologically diverse enough that isolating one path does not prevent timely propagation00
gap
CN-NET-03operationaldeclaredNo single peer, ASN, region, or operator cluster may dominate the node's authoritative view00
gap
CN-NET-04deriveddeclaredPeer selection and promotion policies must not allow one adversary-controlled set to deterministically starve honest views00
gap
CN-NODE-01releaseenforcedSingle bootstrap authority: exactly one pub fn in ade_runtime::bootstrap returns the initial (LedgerState, PraosChainDepState, ChainDb tip) at node startup. Col…53
CN-NODE-02constraint_networkenforced`--mode node` is the single live-run lifecycle owner. The relay run loop may advance authoritative state ONLY by invoking existing closed seams (bootstrap_initi…52
CN-NODE-03constraint_networkenforcedOperator-key ingress + forge-on flip for --mode node. Ingress constructs an operator-material-backed ForgeActivation STRICTLY through RED-parse -> BLUE-structur…113
CN-NODE-04operationalenforced--mode node emits a CLOSED, allow-listed diagnostic event vocabulary for feed/forge scheduling: feed_unavailable{reason} with a closed reason enum, forge_tick_c…21
CN-OPCERT-01derivedenforcedThe opcert envelope parser accepts a real cardano-cli `node.opcert` text envelope (closed type check `NodeOperationalCertificate` + CBOR array(2) shape locked b…51
CN-OPERATOR-EVIDENCE-01releaseenforcedEvery PHASE4-N-S-C operator-pass evidence manifest (docs/clusters/PHASE4-N-S-C/CE-N-S-LIVE_YYYYMMDD-<short_commit>.toml) carries the closed schema: schema_versi…02
gap
CN-OPS-01operationaldeclaredAfter any partition, authoritative post-incident reconciliation must be derived solely from the recovered canonical chain00
gap
CN-OPS-02operationaldeclaredEmergency recovery procedures must have explicit admissibility criteria, deterministic inputs and outputs, and defined authority thresholds00
gap
CN-OPS-03operationaldeclaredIncident evidence must be sufficient to reconstruct the canonical decision path without relying on nondeterministic logs or local operator memory00
gap
CN-OUTBOUND-RELAY-01derivedenforcedOutboundCommand is the sole channel between produce_mode and MuxPump's outbound encoder. The closed enum carries typed ChainSyncServerMsg / BlockFetchServerMsg …21
CN-PEER-OUTBOUND-MAP-01derivedenforcedPer-peer outbound senders are owned by an Arc<RwLock<BTreeMap<PeerId, mpsc::Sender<OutboundCommand>>>>. Listener (run_per_peer_session) inserts on PeerConnected…10
gap
CN-PLUTUS-01derivedenforcedSame script + same redeemers/datum/context + same cost model must produce identical result and budget accounting22
CN-PLUTUS-02deriveddeclaredBudget exhaustion and script failure must have a single deterministic failure shape71
CN-PLUTUS-03deriveddeclaredScript context must be canonically and completely derived from transaction plus ledger state00
gap
CN-PLUTUS-04trueenforcedNo host-environment property may influence script results11
CN-PREIMAGE-FIXTURE-01derivedenforcedFor every block in ade_testkit::validity::corpus::ConwayValidityCorpus, Ade's unsigned_header_pre_image(...) (with inputs derived from decode_block(block_bytes)…10
gap
CN-PROD-01derivedenforcedProducer-mode listener completes the N2N handshake (CN-SESS-02) on every accepted inbound connection before any mini-protocol traffic is exchanged. Pre-handshak…11
CN-PROD-02derivedenforcedProducer slot loop never signs a block whose KES period has rotated past current_period. Slot → KES period is a pure function of (slot, genesis_kes_anchor, slot…162
CN-PROD-03derivedenforcedproduce_mode's forge base state is derived from bootstrap_initial_state (cold-start, fed the operator-seeded ledger from --json-seed + --consensus-inputs) plus …21
CN-PROD-04derivedenforcedEvery CoordinatorEffect::BroadcastBlock reconstructs the AcceptedBlock from artifact.bytes through the BLUE self_accept authority against the pre-forge base, th…30
gap
CN-PROTO-01deriveddeclaredEach miniprotocol must be an explicit deterministic state machine with legal typed transitions only00
gap
CN-PROTO-02deriveddeclaredFor the same peer transcript, authoritative state and outbound transcript must be identical00
gap
CN-PROTO-03deriveddeclaredAgency must be enforced strictly; impossible messages must fail deterministically00
gap
CN-PROTO-04truedeclaredSocket fragmentation, multiplexing, arrival order, and timeout behavior must not leak nondeterminism into authoritative logic00
gap
CN-PROTO-05truedeclaredUntrusted network inputs must not allocate unbounded authoritative resources before deterministic validation00
gap
CN-PROTO-06derivedenforcedThe producer-side session orchestrator can only construct outgoing mini-protocol messages tagged with Server agency. Client-originated messages from the server-…71
CN-PROTO-07derivedenforcedReceive-side agency closure: the receive bridge consumes only peer-originated ForkChoiceSignal and BatchDeliveryEvent values valid for the client-role N2N recei…31
CN-PUMP-01releaseenforcedSingle admission wire-pump entry per peer: exactly one pub async fn ade_runtime::admission::wire_pump::run_admission_wire_pump drives the per-peer pump that pro…51
CN-REHEARSAL-FIDELITY-01releaseenforcedPrivate-testnet accepted-block bounty dry-run fidelity (two coupled clauses; if either fails the rehearsal becomes misleading). (1) PATH FIDELITY: the C1 privat…103
CN-REL-01releasedeclaredA release is not mainnet-eligible unless mixed-version topologies against supported predecessors show consensus equivalence on malformed and boundary-case input…00
gap
CN-REL-02releasedeclaredNo single implementation bug should exceed the protocol's intended safety or liveness fault threshold at ecosystem level00
gap
CN-REL-03releasedeclaredCross-implementation accept/reject agreement on authoritative corpora is release-blocking00
gap
CN-SEED-01releaseenforcedSingle JSON seed-importer authority: exactly one pub fn in ade_runtime::seed_import::import_cardano_cli_json_utxo converts a cardano-cli `query utxo --whole-utx…192
CN-SESS-01releaseenforcedSingle mux frame authority: ade_network::mux::frame::{encode_frame, decode_frame} is the SOLE pub fn pair encoding/decoding `MuxFrame` to/from bytes in the work…11
CN-SESS-02releaseenforcedSingle handshake authority: ade_network::handshake::n2n_transition is the SOLE pub fn driving the N2N handshake state machine. ade_network::handshake::n2c_trans…21
CN-SESS-03releaseenforcedSingle session step authority: ade_network::session::core::step is the SOLE pub fn reducing (SessionState, ByteChunkIn) -> (SessionState, Vec<SessionEffect>). N…31
CN-SESS-04releaseenforcedSession reducer per-mini-protocol payload reassembly: the GREEN session reducer maintains one accumulating Vec<u8> buffer per AcceptedMiniProtocol variant insid…61
CN-SESS-05derivedenforcedOutbound mini-protocol payloads larger than MAX_PAYLOAD are segmented into ordered mux frames, each no larger than MAX_PAYLOAD, preserving mini-protocol id, mod…71
CN-SNAPSHOT-01deriveddeclaredA forged block becomes visible to peers only AFTER ServedChainHandle::push_atomic succeeds. The push_atomic call covers the full served_chain_admit call inside …30
gap
CN-SNAPSHOT-02derivedenforcedA RequestRange covering a slot range that is not entirely present in ServedChainSnapshot MUST return NoBlocks per the Cardano block-fetch protocol's failure sem…60
gap
CN-STORE-01truedeclaredNo authoritative storage initialization may occur before bootstrap or anchor verification succeeds00
gap
CN-STORE-02truepartialWAL entries, checkpoints, and recovered artifacts must be bound to exactly one anchor or bootstrap lineage30
gap
CN-STORE-03trueenforcedCrash recovery must produce the same authoritative state as clean replay over the accepted canonical inputs41
CN-STORE-04trueenforcedCheckpoints must be atomic: fully committed and valid, or absent41
CN-STORE-05trueenforcedFinalized provenance must be append-only, auditable, and replay-derivable31
CN-STORE-06deriveddeclaredOn-disk bytes must re-enter through the same canonical validation and decode chokepoints as network inputs00
gap
CN-STORE-07releaseenforcedSingle materialize authority for rolled-back state: the function that materializes (LedgerState, PraosChainDepState) at a target point uses ONLY one SnapshotSto…51
CN-STORE-08releaseenforcedSingle encoder authority: encode_ledger_state + decode_ledger_state + encode_chain_dep + decode_chain_dep + encode_snapshot + decode_snapshot are the SOLE pub f…01
gap
CN-TEST-01releasedeclaredConsensus-relevant inputs must be fuzzed differentially across all supported versions and decode or validation paths; any verdict mismatch is release-blocking00
gap
CN-TEST-02releasedeclaredEvery malformed or discrepant input that ever triggered a fork, preview mismatch, or parser disagreement becomes a permanent regression corpus entry00
gap
CN-TEST-03releasedeclaredPreviously failed, duplicate, or boundary-case inputs must remain verdict-stable under resubmission and replay00
gap
CN-WAL-01releaseenforcedSingle WAL append authority: WalStore::append is the SOLE mutation method on any WalStore impl. No truncate/rewrite/replace method exists on the trait or any im…31
CN-WIRE-01truedeclaredHash-critical original bytes must be preserved and used on all hash/signature-critical paths00
gap
CN-WIRE-02truedeclaredInternal replay/state surfaces must use exactly one canonical project encoding00
gap
CN-WIRE-03deriveddeclaredConsensus-critical deserialization must be equivalent across all supported versions and active code paths00
gap
CN-WIRE-04truedeclaredMalformed consensus-relevant inputs must be rejected deterministically before any authoritative state transition00
gap
CN-WIRE-05deriveddeclaredNo legacy or compatibility parser may accept bytes that the canonical parser rejects00
gap
CN-WIRE-06deriveddeclaredEvery network/storage ingress path must pass through named era-aware decode chokepoints00
gap
CN-WIRE-07derivedenforcedEach protocol-visible message must decode into one closed, versioned message type451
CN-WIRE-08derivedenforcedN2N tag-24 CBOR-in-CBOR payload envelopes are constructed and stripped through ONE shared BLUE byte authority in ade_codec (wrap_tag24/unwrap_tag24). Protocol-s…241
CN-WIRE-09derivedenforcedThe Shelley-and-later header_body `prev_hash` field is the closed wire grammar `$hash32 / null` (cardano-ledger PrevHash = GenesisHash | BlockHash). Ade represe…201
CN-WIRE-10derivedenforcedAde's serve-side N2N handshake RESPONDER must encode versionData / MsgAcceptVersion / query-reply in the closed Cardano NodeToNode wire grammar a real cardano-n…41
CN-WIRE-11derivedenforcedAde's serve-side ChainSync server must be wire-compatible with a real cardano-node follower's MsgFindIntersect, in two halves, served from the SINGLE ServedChai…71
CN-WIRE-12derivedenforcedAde's FEED/receive-side BlockFetch path MUST remove the protocol tag-24 wrapper using the SINGLE ade_codec unwrap authority (decompose_blockfetch_block = ade_co…41
DC-ADMIT-01derivedenforcedClosed AgreementVerdict sum (GREEN evidence, not authority): exactly four variants — Agreed{our_hash,peer_hash}, Lagging{our_slot,peer_slot}, Diverged{our_hash,…81
DC-ADMIT-02derivedenforcedVerdict emitted exactly once per admit-attempt: every successful admit path produces exactly one agreement_verdict JSONL event. Never twice for the same block_h…21
DC-ADMIT-03derivedenforcedDiverged + InputNotFound are authority-fatal at the binary boundary. Distinct exit codes: EXIT_LIVE_AGREEMENT_DIVERGED=30, EXIT_LIVE_INPUT_NOT_FOUND=31. Mirrors…31
DC-ADMIT-04derivedenforcedClosed AdmissionLogEvent vocabulary (8 variants: admission_started, snapshot_imported, bootstrap_complete, block_received, block_admitted, agreement_verdict, ad…92
DC-ADMIT-05derivedenforcedPer-admit WAL append: every successful admit appends exactly one WalEntry::AdmitBlock to the configured WalStore. The entry's prior_fp chains to the previous en…22
DC-ADMIT-06derivedenforcedVerdict reducer is pure: verdict::derive(admit_outcome, peer_tip) is a pure function over closed input enums → closed output enum. No I/O, no clock, no state. T…11
DC-ADMIT-07trueenforcedAdmit-replay-equivalence (true-tier): for every successful WalEntry::AdmitBlock transition, replay from the prior checkpoint plus WAL produces (a) the same post…41
DC-ADMIT-08derivedenforcedLagging is evidence-state only: AgreementVerdict::Lagging means the local admitted chain is a prefix of the comparison target (peer's announced chain) up to the…21
DC-ADMIT-09derivedenforcedAdmission code paths do not add partial reference-script support, permissive ref-script skipping, or any seed-import fallback. N-M-A's fail-fast on JsonSeedErro…01
gap
DC-ADMIT-10derivedenforcedEvery admission JSONL block-event carries consensus_inputs_fingerprint. BlockAdmitted, AgreementVerdict, BootstrapComplete, and AdmissionStarted events emit the…32
DC-ADMIT-11derivedenforcedCross-epoch silent use forbidden. If a peer sends a block whose slot is outside [epoch_start_slot, epoch_end_slot], the runner MUST emit AdmissionHalted { reaso…11
DC-ADMIT-12derivedenforcedUndecodable peer bytes are Diverged (or PeerSentUndecodableBytes); never InputNotFound; never silent clean exit. C strengthens N-M-B's ProcessedBlock::Undecodab…11
DC-ANCHOR-01derivedenforcedBootstrapAnchor canonical CBOR round-trip: encode + decode preserves all 6 fields byte-identically. SCHEMA_VERSION = 1 in the encoded bytes; unknown version on …71
DC-CBOR-01deriveddeclaredCardano CBOR decode/encode round-trips to identical bytes for all era types00
gap
DC-CBOR-02deriveddeclaredOriginal wire bytes preserved for hash computation on hash-critical paths (see Byte Authority Model)00
gap
DC-CINPUT-01derivedenforcedWARM-START VERIFICATION CAPABILITY (authority surface — NOT production restart). The seed-epoch consensus-input import is a canonical, replay-reconstructable WA…181
DC-CINPUT-02aderivedenforcedPROJECTION EQUIVALENCE. The recovered SeedEpochConsensusInputs projects deterministically to the leadership-consumed PoolDistrView (the full LedgerView surface:…40
gap
DC-CINPUT-02bderivedenforcedPRODUCER CONSUMPTION (closes CE-A-4b). The node-lifecycle forge base is built from the recovered selected tip + the recovered SeedEpochConsensusInputs: forge_on…32
DC-CINPUT-03derivedenforcedThe producer Praos VRF leader/header input is `praos_vrf_input(slot, eta0)` = `blake2b256(slot_be8 ‖ eta0_32)` (= cardano `mkInputVRF`), where eta0 is the Carda…31
DC-CINPUT-04derivedenforcedThe receive/feed-path header-validation consensus view -- the LedgerView passed to block_validity -> validate_and_apply_header for Step 5 (VRF-keyhash binding) …11
DC-CINPUT-05trueenforcedVenue epoch geometry is DURABLE REPLAY AUTHORITY. A recovered store MUST replay using the epoch geometry (epoch_start_slot + epoch_length_slots) persisted with …50
gap
DC-CINPUT-06trueenforcedThe durable consensus PROFILE includes genesis_hash + protocol_params_hash, persisted canonically in the v4 SeedEpochConsensusInputs sidecar and recovered IDENT…51
DC-CINPUT-07truedeclaredConway deposit-parameter bootstrap authority. The Conway-only deposit params (drep_deposit / gov_action_deposit / drep_activity) are DECODED from the certified …131
DC-COMPAT-01derivedenforcedCardano compatibility is proven ONLY on observable surfaces — per-block accept/reject verdict, selected tip hash, block hashes, cardano-cli query-utxo result, p…11
DC-CONS-03derivedenforcedPraos chain selection ordering: block number first, then Praos TiebreakerView (slot, issuer, op-cert issue number, VRF output). Density-based ordering is reserv…154
DC-CONS-04derivedenforcedPraos chain-dep state (evolving/candidate/epoch/previous_epoch/lab/last_epoch_block nonces, op-cert counters, last_slot) is owned by N-B consensus, not by the l…491
DC-CONS-05derivedenforcedAuthoritative rollback must never exceed the security parameter k measured in blocks (mainnet k = 2160). Rollback requests deeper than k return ExceededRollback…112
DC-CONS-06derivedenforcedrollback(state, depth) produces state byte-identical to truncated replay from the nearest checkpoint. Rollback that would cross the immutable tip (≥ k deep) ret…71
DC-CONS-07derivedenforcedBLUE consensus must consume the HFC schedule only as a typed EraSchedule value anchored to BootstrapAnchorHash. Genesis text parsing happens in RED; BLUE never …121
DC-CONS-08derivedenforcedslot_to_time(EraSchedule, SystemStart, SlotNo) is a pure function; no BLUE consensus path may consult the wall clock to derive a slot or UTC instant for an auth…81
DC-CONS-09derivedenforcedConsensus-derived queries for slots beyond the ledger-view safe zone return OutsideForecastRange, never guessed values. The bound is derived from era history + …51
DC-CONS-10derivedenforcedA header's op-cert issue counter must be >= the highest observed counter for the same (pool, kes_period). Regression yields HeaderInvalid with a typed OpCertCou…161
DC-CONS-11derivedenforcedOpCert kes_period field equals the KES period at the forged slot under an operator-supplied anchor. period_at_slot(slot, anchor) = (slot - anchor) / slots_per_k…61
DC-CONS-12derivedenforcedOpCert serial counter is strictly monotonically increasing per (cold-key, node). BLUE rejects regression or repetition at the RED->BLUE boundary: opcert_validat…31
DC-CONS-13derivedenforcedForge is pure given a canonical ProducerTick. forge_block has no wall-clock, no rand, no HashMap iteration, no I/O, no locale, and no ambient state. All inputs …32
DC-CONS-14derivedenforcedForge byte-equality across replays. For two replays of an identical canonical ProducerTick stream over the same initial LedgerState, forge_block produces a byte…12
DC-CONS-15derivedenforcedForge is invoked only when leader-check passes. forge_block is a forbidden transition for ticks where is_leader(state, vrf_output, sigma, asc) == false at tick.…21
DC-CONS-16derivedenforcedForged header.body_hash MUST equal blake2b_256(forged_body_wire_bytes), where forged_body_wire_bytes are produced by the single Cardano-compatible canonical blo…103
DC-CONS-17derivedenforcedBlock bytes delivered via producer-side block-fetch Block{bytes} are byte-identical to AcceptedBlock.as_bytes() for the AcceptedBlock that cleared self_accept. …52
DC-CONS-18derivedenforcedHeader bytes announced via chain-sync RollForward{header,tip} are the header sub-segment of the AcceptedBlock whose body bytes are subsequently servable via blo…53
DC-CONS-19derivedenforcedReceive-side header-body sourcing coherence: when BlockDelivered {block_bytes} arrives at the receive bridge, the decoded header bytes of block_bytes equal the …31
DC-CONS-20derivedenforcedChainDb-ledger-chain_dep lockstep: a successful receive-side admission updates ChainDb, LedgerState, and PraosChainDepState as one structural transition. A succ…83
DC-CONS-21derivedenforcedSnapshot encode/decode round-trip equivalence: for any reachable (LedgerState, PraosChainDepState), decode(encode(state)) yields a state whose ade_ledger::finge…51
DC-CONS-22derivedenforcedReplay-forward correctness: given state_at_slot_S and the ordered block sequence blocks(S+1..=T) from ChainDb, the replay-forward driver yields a state whose fi…41
DC-CONS-23derivedenforcedOwn-forged stale-tip race safety by extend-only durable admit. An own-forged candidate is admitted to the durable tip ONLY if it EXTENDS the current durable tip…11
DC-CONS-24derivedenforcedForged parent hash byte-equals the peer-visible selected tip. The forged successor's prev_hash byte-equals the followed peer tip hash AND its block_no == follow…11
DC-CONS-IN-01derivedenforcedClosed importer error sum: Io | Json | BadField | MissingField | BadHashHex | BadEpochWindow | BadPoolDistribution | EraNotSupported. No Option field receives a…121
DC-CONS-IN-02derivedenforcedCanonical fingerprint: LiveConsensusInputsCanonical.fingerprint is Blake2b-256 over a canonical CBOR encoding of every field in declared order. Same JSON bytes …51
DC-CONSENSUS-01derivedenforcedChain selection is deterministic and matches Haskell node behavior263
DC-CONSENSUS-02derivedpartialLeadership verification is pure160
gap
DC-CORE-01derivedenforcedBLUE authoritative crates are sync-only: no async fn, .await, tokio::, async_std::, Future, futures::, task spawning, async channels, or timers. Async runtime c…51
DC-CRYPTO-01derivedenforcedCrypto verification is pure and matches Haskell node on all test vectors191
DC-CRYPTO-02derivedenforcedAll signing operations confined to shell01
gap
DC-CRYPTO-03derivedenforcedVRF signing transcript equivalence and verification symmetry. For canonical inputs (slot, epoch_nonce, vrf_signing_key, vrf_role) the RED signer produces a VrfP…21
DC-CRYPTO-04derivedenforcedKES signing transcript equivalence and verification symmetry. For canonical inputs (kes_secret, period, msg) the RED signer produces a KesSignature byte-identic…52
DC-CRYPTO-05derivedenforcedKES evolution discipline: evolve(k_i) -> k_{i+1} is one-way. The evolved key signs period i+1 and MUST NOT sign for period i. RED kes_sign is forbidden when the…42
DC-CRYPTO-06derivedenforcedAde-native KES envelope is the sole accepted hot-signing-key envelope format. Closed grammar `ade.kes.seed.v1`: load-bearing fields {`format`, `role`, `crypto`,…161
DC-CRYPTO-07derivedenforcedcardano-cli's `KesSigningKey_ed25519_kes_2^6` envelope (the upstream `Sum6KES` expanded-tree serialization, 608 bytes for a fresh key) is loadable via the Ade-o…62
DC-CRYPTO-08derivedenforcedAde-owned Sum6KES algorithm is Haskell-equivalent. `ade_crypto::kes_sum::Sum6Kes` is byte-identical to Haskell `cardano-base`'s `Sum6KES Ed25519DSIGN`: `derive_…182
DC-CRYPTO-09derivedenforcedSum6KES expanded signing-key serde and period inference. `raw_serialize_signing_key_kes` / `raw_deserialize_signing_key_kes` are byte-identical to Haskell's `ra…151
DC-CRYPTO-10derivedenforcedThe RED signing shell must evolve the operator KES signing key to the requested KES period before signing, using the existing deterministic Sum6KES update primi…51
DC-DIFF-01derivedpartialDifferential harness must localize first divergence point between Ade and reference oracle20
gap
DC-EPOCH-01derivedpartialConway governance timing: proposals accumulate during epoch, ratification and enactment are atomic at epoch boundary, pulsing distributes DRep stake computation…71
DC-EPOCH-02derivedenforcedHard fork transitions triggered at deterministic slot/epoch boundaries; era translation functions mandatory; forecast horizon extends to era boundary91
DC-EPOCH-03derivedenforcedSingle-epoch forge containment on the --mode node spine: in this forge path, a forge is valid only within the single recovered seed epoch. A candidate forge slo…61
DC-EPOCH-04derivedenforcedFor a target epoch, AT MOST ONE canonically bound EpochConsensusView may activate (S3f-4a substrate). A distinct WalEntry::EpochConsensusViewActivated (append-o…31
DC-EPOCH-05derivedenforcedEpoch N+1 validation and leadership may NOT observe epoch-N seed inputs (S3f-4b). The active epoch view is a ONE-WAY ActiveEpochView transition: `Seed` (the rec…31
DC-EPOCH-06derivedenforcedActivation is durable-before-visible and replay-identical (S3f-4c). The activation WAL record (EpochConsensusViewActivated) is written and made durable BEFORE t…51
DC-EPOCH-07derivedenforcedA missing / stale / conflicting / mismatched candidate view causes TERMINAL fail-closed behaviour, NEVER fallback consensus (S3f-4b). The activation predicate (…31
DC-EPOCH-08derivedenforcedThe activation SOURCE WINDOW is named-role-typed, durable-lineage-pinned, and complete/ordered/bounded (S3f-4d-1). The window that produces an activation candid…81
DC-EPOCH-09derivedenforcedThe activation candidate is derived ONLY from a validated source window, bound to the TARGET-epoch context (S3f-4d-2). derive_candidate drives the reduced check…11
DC-EPOCH-10derivedenforcedThe boundary activation orchestration is ONE atomic, ordered, durable-before-visible path (S3f-4d-3a). activate_at_boundary sequences, in order: validate the du…51
DC-EPOCH-11deriveddeclaredThe live reduced-UTxO checkpoint (S3f-4d-mat) -- the authoritative reduced-stake state Ade maintains on the selected-chain admission path so it derives its OWN …11
DC-EPOCH-12derivedenforcedThe promoted-epoch PoolDistrView is derived EXCLUSIVELY from the sealed EpochConsensusView + the bound-commitment- checked consensus profile (ECA-0b). EpochCons…21
DC-EPOCH-13derivedenforcedNo semantic activation gate: no build- or runtime-level switch decides WHETHER the epoch-view activation occurs. There is no EVIEW_ACTIVATION_ARMED const, no `a…11
DC-EPOCH-14trueenforcedAtomic epoch-authority transition + recovery. The node holds exactly ONE owned ActiveEpochAuthority -- the SOLE leadership + header-validation view source -- an…111
DC-EPOCH-15trueenforcedForecast horizon <=> durable N+1 authority promotion. The relay loop's EraSchedule forecast horizon extends past an epoch boundary N->N+1 IF AND ONLY IF the Act…31
DC-EPOCH-16trueenforcedRolling Praos chain-dep nonce evolution on the live follow path. Each validated followed header drives ONE indivisible BLUE nonce transition over {slot, prev_bl…121
drift
DC-EPOCH-17deriveddeclaredReplay-derived per-boundary leadership authority on the live follow path. The activation seam (prepare_authority_for_candidate_slot) ADVANCES the promoted epoch…00
gap
DC-EPOCH-18derivedenforcedWindow-end bootstrap reward update for the seed+2 leadership authority. The first post-bootstrap replay-derived authority (seed+2, DC-EPOCH-17) is the per-pool …41
DC-EPOCH-19deriveddeclaredSelf-sustaining live ledger epoch evolution. After every durable selected-chain block, the node holds enough durable, replayable state to derive EVERY future ep…21
DC-EPOCH-20deriveddeclaredAtomic-or-rematerialized selected-block admission -- no RESUMED split authority. For every selected block admitted to the durable chain, four derived authoritie…21
DC-EPOCH-21deriveddeclaredThe accumulator's epoch-boundary transition reproduces the canonical cardano NEWEPOCH result. POOLREAP is a SINGLE transition in the cardano order (Shelley Pool…21
DC-EPOCH-22deriveddeclaredBOUNDARY-ALIGNED-MARK-CAPTURE. The live epoch-boundary stake mark is captured ONLY from the durable reduced checkpoint materialized at the EXACT selected-chain …111
DC-EPOCH-23derivedenforcedBootstrap reward-update fee-buffer authority (CE-3d). The one-shot bootstrap reward update applied at the seed->seed+1 boundary carries the certified snapshot R…101
DC-EPOCH-24derivedenforcedSnapshot pool-set inclusion = cardano's ssActiveStake NonZero membership (CE-3d). The per-epoch stake snapshot (mark/set/go) INCLUDES a registered+delegated sta…51
DC-EPOCH-25deriveddeclaredSelf-contained frozen leadership authority (S4-pre). Cardano's leadership PoolDistr (nesPd) -- the per-pool (active_stake, vrf_keyhash) that decides the leader …163
DC-EPOCH-26derivedenforcedSettled rewind target. The epoch accumulator is NEVER rewound to a point within k of the durable tip: every rewind target is beyond the reach of an admissible r…21
DC-EPOCH-27derivedenforcedLineage-bound rewind. A settled rewind target whose header hash no longer resolves canonically at its slot -- a point the chain has ABANDONED -- is REFUSED, and…11
DC-EPOCH-28derivedenforcedLeadership coherence across a rewind. A rewind restores CURRENT_LEADERSHIP_BY_EPOCH to exactly the epochs valid at the rewind point, so no sealed leadership obj…21
DC-EPOCH-29derivedenforcedUncertified after rewind. A rewind clears LAST_ADVANCED_POINT and drops the pending boundary-mark binding, so the store is UNCERTIFIED until a canonical re-fold…21
DC-EPOCH-30derivedenforcedBounded post-rollback refold. Post-rollback re-derivation is bounded by ~2k and is INDEPENDENT OF NODE UPTIME. The settled rewind point is never more than 2k be…21
DC-EPOCH-31derivedenforcedRewind replay equivalence. Refolding from the settled rewind point yields state byte-identical to folding straight through from the bootstrap baseline over the …11
DC-EPOCH-32derivedenforcedBoundary seal reads a POSITIONED checkpoint. The boundary mark and the reduced-checkpoint commitment sealed into a frozen-leadership object are captured with th…31
DC-EPOCH-33derivedenforcedRefold re-seal identity. Re-deriving an epoch boundary the node has already crossed re-seals a frozen-leadership object byte-identical to the one the original c…11
DC-EPOCH-34trueenforcedSettled-triple integrity. The settled rewind triple (accumulator blob + settled point + settled leadership) is bound by a domain-separated, length-prefixed fing…31
DC-EPOCH-35derivedenforcedA bounded settled rewind survives the recovery pass that follows a durable rollback. After the ChainDb rollback COMMITS -- never before -- the settled point is …71
DC-EPOCH-36derivedenforcedAfter the epoch-boundary decision for a block at `slot`, the ledger's epoch MUST equal the venue era schedule's epoch for that slot. A disagreement in EITHER di…41
DC-EPOCH-37releaseenforcedAuthoritative epoch semantics must be proven PER VENUE, not inferred from a mainnet-shaped corpus. Every venue in the closed node-side registry (`native_firstru…41
DC-EPOCH-38derivedenforcedThe Praos candidate-freeze / nonce surface must be proven across SEED-POSITION x VENUE, not once per venue. `eta0(N+1)` is committed from the candidate nonce, w…101
DC-EPOCH-39derivedenforcedA stall's CAUSE is typed, and only a real epoch transition may enter boundary machinery. Advancing the durable accumulator over one block yields exactly one of:…41
DC-EPOCH-40derivedpartialLeadership sigma denominator authority (SLICE LV-1). The leader-check sigma denominator is the SNAPSHOT's total active stake -- cardano's `pdTotalActiveStake` -…42
DC-EVIDENCE-01derivedenforcedOperator-pass live evidence: the C5 live operator pass against the local docker cardano-node-preprod peer produces a JSONL transcript containing AT LEAST: - 1…21
DC-EVIDENCE-02derivedenforcedAdversarial false-accept rejection across 4 mandatory mutation classes: 1. Body byte flip preserving envelope shape 2. Header body-hash mismatch 3. KES / …11
DC-EVIDENCE-03derivedenforced_scaffoldingConvergence-through-reorg transcript shape (CE-AI-6; PHASE4-N-AJ). The participant convergence pass produces ONE JSONL transcript with AT LEAST: - a strict sl…01
gap
DC-EVIDENCE-04derivedenforcedClosed fork-choice convergence evidence (PHASE4-N-AO S9; promotes the live SELECT proof from stderr diagnostics to registry-grade evidence). The live multi-cand…41
DC-EVIDENCE-05derivedenforcedReplayable post-switch branch-continuity verdict (PHASE4-N-AO S10). After a ForkChoiceWin adoption at tip X, a GREEN pure reducer derive_post_switch_continuity(…111
DC-EVIEW-01derivedenforcedTransient epoch-view replay storage is GREEN / non-authoritative substrate. A bounded, disk-backed, TRANSIENT redb store (TransientEpochViewStore) may be materi…153
DC-EVIEW-02derivedenforcedTyped, era-gated stake-reference classification. Given canonical address bytes and a TYPED era / protocol-version context BOUND to the block being processed (Ca…181
DC-EVIEW-03derivedenforcedEra-parameterized pointer decoding + pre-Conway resolution, matching cardano-ledger EXACTLY (the wire authority -- CIP-19 is silent on canonicality, so the card…201
DC-EVIEW-04derivedenforcedThe durable reduced-UTxO checkpoint -- the "minimal native state" (S3b Option B). A disk-backed redb store of TxIn -> (Coin, ReducedStakeRef), built from Ade's …121
DC-EVIEW-04bderivedenforcedThe windowed advance (S3b-2): advance the durable reduced-UTxO checkpoint (DC-EVIEW-04) per epoch boundary by replaying the epoch's admitted blocks, as the redu…71
DC-EVIEW-05derivedenforcedPer-pool stake aggregation (S3c, the linchpin). aggregate_pool_stake computes the next-epoch per-pool active stake from the single ledger authority's own projec…82
drift
DC-EVIEW-06derivedenforcedSnapshot formation + the k-immutability stability gate (S3d). form_mark_snapshot converts the S3c per-pool aggregate (StakeByPool) into the MARK StakeSnapshot's…51
DC-EVIEW-07derivedenforcedThe bound, immutable EpochConsensusView (S3e). EpochConsensusView::bind emits the compact next-epoch consensus view from the finalized snapshot (S3d), BOUND to …62
DC-EVIEW-08deriveddeclaredActivation -- the live-path consumption of Ade's self-derived next-epoch view. MECHANISM (IMPLEMENTED + AUTOMATIC): the boundary activation is wired into the re…11
drift
DC-EVIEW-09derivedenforcedThe manifest-bound bootstrap cert-state import (S3f-2 prerequisite). The seed (SeedEpochConsensusInputs, the compact per-POOL active epoch consensus view) and t…71
DC-EVIEW-10derivedenforcedThe window driver (S3f-2): advance the reduced UTxO checkpoint + the cert/delegation state forward over a window of ordered blocks, then aggregate per-pool stak…21
DC-EVIEW-11derivedenforcedThe deterministic, fail-closed epoch-rebind seam (S3f-3), strengthening DC-EPOCH-03. DC-EPOCH-03 fails the forge closed past the seed-epoch boundary (the recove…91
DC-EVIEW-12derivedenforcedThe leadership-complete, self-contained EpochConsensusView (ECA-0b). The candidate view is the production authority for cross-epoch leadership: every INCLUDED p…41
DC-EVIEW-13derivedenforcedCardano-faithful pool lifecycle in the reduced window (ECA-0a). The cert-state pool lifecycle matches cardano-ledger (Pool.hs/PoolReap.hs/Epoch.hs/SnapShots.hs …71
DC-FOLLOW-FORGE-01derivedenforcedParticipant forge-decision mechanics. The keyed Participant venue uses an initial-catch-up -> extend forge mode mirroring the single-producer two-state mode: pa…101
DC-FORGE-01derivedenforcedGiven the same canonical input set (slot, eta0, vrf_vk, vrf_proof_or_output, LeaderScheduleAnswer), verify_and_evaluate_leader produces a byte-identical LeaderC…30
gap
DC-GENESIS-01derivedenforcedGiven the same canonical Shelley genesis JSON bytes + the same operator-supplied kes_anchor_slot, parse_shelley_genesis produces a byte-identical GenesisAnchor …10
gap
DC-GENESIS-SRC-01derivedenforcedA controlled genesis enters initial state ONLY through the single closed bootstrap_initial_state authority (genesis_initial); the genesis->initial-state transfo…41
DC-GOV-01deriveddeclaredGOVERNANCE-DEPOSIT-EXPIRY-REFUND (negative proof). Ade refunds a removed governance proposal's deposit to its recorded return address ONLY when it can PROVE, fr…51
DC-INGRESS-01deriveddeclaredBlock/tx/protocol message decoding enters core through named chokepoints; no raw-byte bypass without CI-whitelisted justification01
gap
DC-INGRESS-02deriveddeclaredStorage rehydration enters core through the same canonical decode chokepoints as network ingress00
gap
DC-KES-HEADER-01derivedenforcedunsigned_header_pre_image(slot, block_no, prev_hash, vrf_data, opcert, kes_period, hot_vkey, body_hash, body_size, protocol_version) is a pure BLUE function. Sa…10
gap
DC-LEDGER-01derivedenforcedapply_block(state, block) is pure and deterministic31
DC-LEDGER-02derivedpartialSame genesis + same blocks = byte-identical ledger state52
DC-LEDGER-03derivedpartialTx/block validity agrees with Haskell node on all tested inputs93
DC-LEDGER-04derivedpartialEpoch boundary computations (stake snapshots, rewards) match Haskell40
gap
DC-LEDGER-05derivedpartialWitness binding is era-specific: Byron TxWitness, Shelley+ WitsVKey/Scripts/BootstrapWitnesses, Alonzo+ Redeemers/Datums, Conway governance witnesses91
DC-LEDGER-06deriveddeclaredScript context (ScriptContext/TxInfo) derived from tx + ledger state + network-wide constants (EpochInfo, SystemStart); no host-environment data00
gap
DC-LEDGER-07deriveddeclaredCoexisting supported versions must return same validity verdict for consensus-relevant inputs00
gap
DC-LEDGER-08derivedenforcedConway cert-state accumulation is a closed, total, era-versioned transition: for each block at track_utxo, certificates decode through the era-correct closed gr…161
DC-LEDGER-09derivedenforcedConway governance-certificate accumulation is a closed, total, era-versioned transition into ConwayGovState: every governance-affecting Conway cert that B4 owne…171
DC-LEDGER-10derivedenforcedCredential identity is faithful end-to-end: a stake/committee/DRep credential is a closed sum over {KeyHash, ScriptHash} of a 28-byte hash, never a tag-erased H…201
DC-LEDGER-11derivedenforcedproposal_procedures MUST NOT remain an opaque byte field in the authoritative Conway tx-body shape. ConwayTxBody.proposal_procedures is Option<Vec<ProposalProce…211
DC-LEDGER-12derivedenforcedEvery tx in a forged block is admissible via ade_ledger::mempool::admit against the base ledger state, in the snapshot's canonical accumulating order. No tx in …41
DC-LEDGER-13derivedenforcedMAINNET Shelley constants (SHELLEY_START_SLOT / SHELLEY_START_EPOCH / SHELLEY_EPOCH_LENGTH) may enter a computation ONLY through the explicitly-named `mainnet_s…41
DC-LEDGER-PARAMS-01trueenforcedImported protocol parameters are preserved era-faithfully and are NEVER semantically remapped across eras. The shared `ProtocolParameters` carries the minimum-U…71
DC-LEDGER-PHASE2-01derivedenforcedOne authoritative UTxO effect per transaction, gated by phase-2 validity. The UTxO effect of a transaction is derived in exactly ONE place from the canonical bl…41
DC-LEDGER-PHASE2-02derivedenforcedThe accumulator consumes a RESOLVED SCALAR; it does not own a UTxO. The ADA a phase-2-invalid transaction consumes is collAdaBalance = sum(value(collateral inpu…61
DC-LEDGER-PHASE2-03derivedenforcedA phase-2-invalid transaction contributes its consumed collateral and NOTHING else. For a tx in the block's invalid_transactions set the accumulator applies exa…51
DC-LEDGER-PHASE2-04derivedenforcedThe UTxO authority RETAINS what it destroys on another reader's behalf. A collateral value is authoritative only within [create(x), B), where B is the block who…101
DC-LEDGER-VALUE-01trueenforcedAde's authoritative UTxO OUTPUT asset quantity preserves the full non-negative Cardano Word64 domain (0 ..= 2^64-1) via the `OutputAssetQuantity(u64)` newtype. …81
DC-LIVEMEM-01derivedenforcedLive-feed bounded memory (operational-hardening; NOT BLUE consensus law). Peer-driven memory on the live --mode node feed is bounded BEFORE authoritative decode…41
DC-MEM-01derivedenforcedMempool acceptance rules must not contradict block/ledger acceptance rules71
DC-MEM-02derivedenforcedOverload shedding follows deterministic policy, not timing-dependent collapse21
DC-MEM-03derivedenforcedTx ingress reduces to a closed IngressEvent before BLUE mempool admission; the source variant is evidence/policy/replay metadata only and MUST NOT change the va…81
DC-MEM-04derivedenforcedReplaying the same ordered ingress trace against the same base ledger state produces a byte-identical sequence of (MempoolState, AdmitOutcome) pairs.81
DC-MEM-05deriveddeclaredThe UTxO/ledger state fingerprint and post-state are independent of the UTxO storage backend: an in-memory UTxO and an on-disk UTxO produce byte-identical repla…00
gap
DC-MEM-06derivedpartialThe UTxO/ledger state fingerprint is computed by the canonical CBOR encoder over canonically-encoded (fixed-width big-endian) keys, NEVER from a storage backend…52
DC-MEM-07derivedpartialThe in-memory portion of the UTxO (read cache + last-k changelog) is bounded by fixed, closed, non-configurable constants; memory pressure cannot grow it unboun…41
DC-MEM-08deriveddeclaredA compact UTxO/TxOut representation (canonical CBOR slice as the single source of truth + lazily-decoded views) preserves canonical bytes and ledger semantics: …00
gap
DC-MEM-09derivedenforcedThe authoritative UTxO lookup interface returns OWNED values (Option<TxOut>), never a borrow into storage. This is the precondition for a swappable UTxO backend…11
DC-MEM-10derivedenforcedThe v2 UTxO fingerprint component is a NAMED commutative set commitment (Ristretto255 ECMH) binding (TxIn, TxOut) over the canonical encodings, domain-separated…121
DC-MEM-11derivedenforcedThe network forward-sync / forge per-block admit MUST derive the WAL post_fp from the CACHED UTxO-component fingerprint (ForwardSyncState.utxo_fp_cache -> finge…41
DC-MITHRIL-01derivedenforcedverify_mithril_binding is a pure deterministic BLUE predicate over its inputs (the manifest report + the anchor) — no I/O, no clock, no HashMap, no float, no St…31
DC-MITHRIL-02derivedenforcedFor Mithril bootstrap, the BootstrapAnchor seed_point MUST be derived from the operator-provided independent seed-point extraction inputs, not from the Mithril …31
DC-MITHRIL-03trueenforcedThe native Mithril AUTHORITY TRANSITION assembles the COMPLETE authoritative seed (LedgerState + PraosChainDepState + a NATIVE LiveConsensusInputsCanonical) fro…91
DC-MITHRIL-04derivedenforcedNative V2 LedgerDB `state` decode is faithful, fail-closed, and non-emitting. The cardano-node V2 (utxohd-mem, tablesCodecVersion 1) LedgerDB `state` CBOR is de…91
DC-MITHRIL-05trueenforcedFaithful Word64 multi-asset quantity on the snapshot-import path. The native V2 LedgerDB `tables` MemPack TxOut decode keeps every multi-asset quantity as a ful…91
DC-MITHRIL-06trueenforcedThe Stage-2 `tables` (MemPack-decoded TxOuts) materialize into Ade's authoritative `UTxOState` with hash-critical bytes PRESERVED and full Word64 quantities car…111
DC-MITHRIL-07trueenforcedThe live `--mode node` FirstRun arm INVOKES the native Mithril bootstrap path (DC-MITHRIL-03 / S1b) from live snapshot files -- it routes the verified Mithril m…121
drift
DC-MITHRIL-08derivedenforcedThe native Mithril FirstRun is BOUNDARY-COMPLETE: when the decoded cert-state carries delegations (the EVIEW package), native_first_run_bootstrap builds the liv…11
DC-NET-01deriveddeclaredPeer selection uses three-tier management (cold/warm/hot) with bounded admission, per-peer resource limits, and eviction policies00
gap
DC-NODE-01derivedenforcedPer-peer session isolation: one peer session's failure (decode error, validity reject, rollback-too-deep, protocol violation) halts only that peer's session. Th…51
DC-NODE-02derivedenforcedPersistent-writer cadence fidelity: the orchestrator's persistent-snapshot writer calls PersistentSnapshotCache::capture only on the schedule emitted by the N-I…51
DC-NODE-03derivedenforcedClock-injection seam + replay equivalence: the orchestrator depends on a Clock trait yielding now() and tick_stream(). No SystemTime::now() or tokio::time::Inst…52
DC-NODE-04derivedenforcedAuthority-fatal halt + shutdown-resume identity: authoritative errors (chain_write failure on a committed rollback, SnapshotDecodeError::UnknownVersion or Finge…41
DC-NODE-05derivedenforcedForge-slot discipline on the --mode node relay run-loop. A forge is attempted at most once per SlotNo and never for a slot <= the last forged slot (no past or d…103
DC-NODE-06derivedenforcedSelf-accept -> serve handoff on the --mode node relay spine (sibling serve task, shape B). Only a BLUE self-accepted forged artifact may enter the sibling serve…133
DC-NODE-07derivedenforcedNode-spine live serve-to-peer. --mode node serves real peers ONLY from the G-B self-accepted ServedChainView (the read side of the single ServedChainHandle fed …42
DC-NODE-08derivedenforced--mode node MAY forge the genesis-successor (FIRST) block from the recovered authoritative base when ChainDb::tip() AND the recovered tip (recovered.tip) are BO…91
DC-NODE-09derivedenforcedOnce --mode node has spawned a --listen serve task (run_node_serve_task) over a ServedChainView, the end of the upstream feed (the relay loop returning -- e.g. …41
DC-NODE-10derivedenforcedAfter the feed validation/admission advances the node spine (a block ingested -> state.receive evolved), the next forge MUST derive the successor header positio…21
DC-NODE-11derivedenforcedOnce --mode node has self-accepted and SERVED a genesis-successor block at block_no 0, it MUST NOT add/replace the served view (ServedChainView) with another bl…21
DC-NODE-12derivedenforcedOwn-forged durable admit chokepoint. A self-accepted forged block may become part of the durable chain ONLY by being submitted to the same durable admit chokepo…32
DC-NODE-13derivedenforcedServed view is a durable-chain projection. The ChainView served to followers (ChainSync header advertisement + BlockFetch body) is a deterministic PROJECTION of…31
DC-NODE-14derivedenforcedEvery claimed forge parent must be servable or peer-intersectable in the durable served lineage. A --mode node forge may only build on a parent a Haskell peer c…42
DC-NODE-15derivedenforcedForge admissibility requires the durable servable tip to equal the followed peer tip. A --mode node forge is admissible ONLY when durable_servable_tip == follow…31
DC-NODE-16derivedenforcedReceive idempotency: a peer-delivered block already durably present byte-identically in the ChainDb (same slot, same hash) is an idempotent no-op at the durable…31
DC-NODE-17deriveddeclaredfollowed_peer_tip advances ONLY from a real observed peer ChainSync advertisement of the peer's selected tip, INCLUDING the self-adoption echo case where the ad…00
gap
DC-NODE-18derivedenforcedSuccessor extension after an explicit adoption certificate (single-producer, single successor). After initial peer catch-up against a real peer tip (DC-NODE-15)…51
DC-NODE-19deriveddeclaredSingle-producer forge-loop continuation after follow-link EOF. In an explicitly declared single-producer venue (VenueRole::SingleProducer) that has ALREADY ente…00
gap
DC-NODE-20derivedenforcedLocal selected durable chain forge-base authority (rung-1 single-producer). In a declared rung-1 single-producer venue, after Ade self-admits a valid forged blo…42
DC-NODE-21derivedenforcedAdoption certificate is rung-1 evidence-only, never forge authority. The file-based operator adoption certificate is a rung-1 RED EVIDENCE-ONLY shim. It MAY pro…32
DC-NODE-22derivedenforcedSingle-producer warm-start re-entry derives forge mode from the recovered local durable spine. In a declared rung-1 single-producer venue, if warm-start recover…21
DC-NODE-23derivedenforcedShared receive-side fork-choice detector (rung-2). A peer-origin candidate that is NOT already known as part of Ade's admitted durable spine / own-served lineag…61
DC-NODE-24derivedenforcedVenue-split fork-choice resolver (rung-2). The DC-NODE-23 detector's non-spine consequent is gated by venue and TOTAL over the closed venue set: VenueRole::Sing…41
DC-NODE-25derivedenforcedLive fork-choice durable application authority (rung-2). A ChainSelected / RolledBack outcome from the chain_selector orchestrator is applied to the durable sto…52
DC-NODE-26derivedenforcedDecision / durable reconciliation (rung-2). After any applied receive decision, the chain_selector orchestrator's selector.current_tip EQUALS the durable ChainD…21
DC-NODE-27derivedenforcedRollback+reselection replay-equivalence (rung-2). The ordered live receive-event sequence (RollForward headers, RollBackward points, body deliveries) replayed a…42
DC-NODE-28derivedenforcedNo forge across unresolved re-selection (rung-2). Once a peer-origin candidate is classified NeedsForkChoice (DC-NODE-23) in a Participant venue, forging is DIS…52
DC-NODE-29derivedenforcedLive rollback target canonical binding (rung-2; AI-S6 H-1 remediation). For a peer RollBackward(point) on the live Participant path, the rollback target MUST be…51
DC-NODE-30derivedenforcedParticipant-path convergence evidence emission (PHASE4-N-AJ). The live `--mode node --participant-venue` rollback-follow path emits the existing closed Agreemen…73
DC-NODE-31derivedenforcedRecovered-anchor live-follow start authority (PHASE4-N-AK). After recovery from a non-Origin bootstrap anchor, the recovered store PERSISTS the bootstrap anchor…110
gap
DC-NODE-32derivedenforcedRecovered-anchor rollback boundary on the single-producer live-follow path (PHASE4-N-AK AK-S2). After recovery to a bare bootstrap anchor, the single-producer f…70
gap
DC-NODE-33derivedenforcedParticipant-path recovered-anchor rollback boundary (PHASE4-N-AL) -- the participant MIRROR of DC-NODE-32. On the participant live-follow path (run_participant_…50
gap
DC-NODE-34derivedenforcedPeer-identity restoration (PHASE4-N-AO, SELECT foundation). The live receive path preserves the origin peer identity end-to-end: AdmissionPeerEvent (peer: Strin…21
DC-NODE-35derivedenforcedBLUE-safe candidate construction (PHASE4-N-AO). A CandidateFragment fed to the BLUE fork-choice authority select_best_chain (DC-CONS-03) MUST be derived ONLY fr…51
DC-NODE-36derivedenforcedLive single-selector dispatch (PHASE4-N-AO). The live participant NeedsForkChoice arm (today fail-closed in run_participant_sync, node_lifecycle.rs) routes the …41
DC-NODE-37derivedenforcedFork-switch never-abandon (PHASE4-N-AO, SELECT primary invariant; the H-1 class at fork-choice scale). When select_best_chain picks a winner that forks BELOW Ad…71
DC-NODE-38derivedenforcedLive multi-block fork-anchor discovery (PHASE4-N-AO S7; the live-geometry gap CE-AO-6 surfaced). A live competing branch is eligible for SELECT only when Ade wa…81
DC-NODE-39derivedenforcedPost-ForkChoiceWin forward-follow continuity (PHASE4-N-AO S11). After a ForkChoiceWin adoption at tip X, Ade must continue receiving and admitting the winning p…71
DC-NODE-40derivedenforcedRolled-back branch evidence retention for the LCA walk (PHASE4-N-AO S13). Rolled-back blocks MAY be retained only as walk-visible EVIDENCE for future competing-…61
DC-NODE-41derivedenforcedMissing-bridge range re-fetch for winner-descendant recovery (PHASE4-N-AO S14). When a post-ForkChoiceWin WINNING peer (the peer Ade just adopted from) presents…61
DC-NODE-42derivedenforcedLIVE-FORGE-HARDENING S1 within-epoch forge-path rollback guard (INV-FH-4). On the --mode node forge / live-follow path (run_node_sync), a peer RollBackward whos…10
DC-NODE-43deriveddeclaredGap-free resume of a reconnected live feed. A reconnected per-peer session resumes chain-sync from the last block actually DELIVERED downstream, never from the …00
DC-NODE-44releaseenforcedA warm-start replay divergence (T-REC-05) must be SELF-DESCRIBING: the typed fault carries a `ReplayDivergenceReport` alongside the two fingerprints, naming the…61
DC-NODE-45derivedenforcedONE bootstrap-bound wall-clock -> absolute-slot authority on the authoritative --mode node producer path. (a) SOLE AUTHORITY: the forge derives its slot ONLY th…201
DC-NODE-46derivedenforcedEvery ADMITTED ForgeTick yields either a structured refusal or a leader-schedule decision. No admitted tick may disappear, and none may report a reason that is …61
DC-NODE-47derivedpartialFollowed-peer-tip possession evidence (SLICE B12). The forge-admissibility signal (FollowedPeerTipSignal) reports the STRONGEST available evidence that the foll…72
DC-OPCERT-01derivedenforcedGiven the same canonical envelope bytes, parse_opcert_envelope produces a byte-identical DecodedOpCertEnvelope across runs. Replay-equivalence anchor for the op…10
gap
DC-OUTBOUND-FIFO-01derivedenforcedThe per-peer outbound channel preserves FIFO order: OutboundCommands enqueued for PeerId(p) in order O₁..Oₙ arrive at the peer's TCP socket in the same order (m…00
gap
DC-PLUTUS-01deriveddeclaredUPLC evaluation is deterministic: same script + args + cost model = identical result00
gap
DC-PLUTUS-02deriveddeclaredBudget exhaustion produces deterministic structured error00
gap
DC-PROD-01derivedenforcedProducer-mode evidence log emits a closed `ProducerLogEvent` vocabulary: handshake_ok, slot_tick, leader_elected, block_forged, block_served, peer_chain_tip_obs…50
gap
DC-PROD-02derivedenforcedCoordinator slot-tick + forge-result stream replay-equivalence. For a fixed initial CoordinatorState, fixed canonical slot-tick sequence, fixed ledger state, fi…10
gap
DC-PROD-03derivedenforcedProducer chain-forward continuity + replay. The GREEN ChainEvolution linear typestate threads each forge's post-state (post-ledger, post-chain_dep, new tip) int…80
gap
DC-PROTO-01derivedenforcedProtocol state machines have deterministic transitions901
DC-PROTO-02derivedenforcedTranscript-equivalent miniprotocol behavior with Haskell node481
DC-PROTO-03derivedenforcedFull N2N mini-protocol surface: Handshake, ChainSync, BlockFetch, TxSubmission2, KeepAlive, PeerSharing61
DC-PROTO-04derivedenforcedFull N2C mini-protocol surface: Handshake, LocalChainSync, LocalTxSubmission, LocalStateQuery, LocalTxMonitor421
DC-PROTO-05deriveddeclaredVersion negotiation is closed: enumerated N2N/N2C versions, explicit handshake, deterministic refusal on mismatch211
DC-PROTO-06derivedenforcedBLUE mini-protocol transitions are pure functions of (canonical prior state, canonical input message, selected protocol version, deterministic configuration); n…901
DC-PROTO-07derivedenforcedGiven canonical inputs (negotiated_version, peer_message_sequence, broadcast_arrival_sequence, session_event_sequence), the producer-side chain-sync / block-fet…43
DC-PROTO-08derivedenforcedOnce chain-sync enters a state where the server holds agency, the pure per-session reducer must return exactly one of: a legal RollForward, a legal RollBackward…121
DC-PROTO-09derivedenforcedReceive-side transcript determinism: given canonical inputs (initial_ledger, initial_chain_dep, initial_chaindb, event_sequence), the bridge reducer's output st…22
DC-PROTO-10derivedenforcedChain-sync server FindIntersect cursor: after the producer chain-sync server answers IntersectFound(point), its read cursor (last_announced) IS that point -- th…10
gap
DC-PROTO-11derivedenforcedTxSubmission2 codec accepts + byte-identically preserves cardano-node's REAL wire form for the txid/tx messages: each txId is era-tagged [eraIndex, hash32] (the…91
DC-PUMP-01derivedenforcedWire pump emits AdmissionPeerEvent::{Block, TipUpdate, Disconnected} only. It MUST NOT synthesize AgreementVerdict values or any validity claim. The verdict rem…32
DC-PUMP-02derivedenforcedA CLOSED authority event is emitted on every chain-sync reply carrying a Tip: TipUpdate for IntersectFound / IntersectNotFound / RollForward; the DISTINCT Admis…31
DC-PUMP-03derivedenforcedWire-pump keep-alive client (PHASE4-N-AM). The admission wire pump (run_admission_wire_pump -- the SOLE per-peer pump, CN-PUMP-01) runs the N2N keep-alive CLIEN…31
DC-PUMP-04derivedenforcedMulti-peer wire-pump fairness (PHASE4-N-AO S8; the gap the S7 live retry surfaced). When multiple peers are connected to the participant receive path, no connec…31
DC-PUMP-05derivedenforcedCooperative keep-alive liveness under downstream backpressure. No stall of the downstream consumer -- of ANY duration or cause (block application, epoch-boundar…11
DC-PUMP-06derivedenforcedOrdered pump progression under backpressure. The sequence of AdmissionPeerEvents delivered to events_out is identical to the unstalled pump for the same peer in…11
DC-PUMP-07derivedenforcedBounded deferral, fail closed. Peer frames held while the pump waits for downstream capacity are bounded by the fixed, closed, non-configurable MAX_DEFERRED_PEE…11
DC-PUMP-08derivedenforcedReconnect policy is transport-only and TOTAL. should_reconnect_after is the single named authority classifying the wire pump's closed outcome sum: TRANSPORT los…11
DC-PUMP-09derivedenforcedNo bootstrap spin. Reconnect applies ONLY to a session that was established and then lost. An unparseable --peer, or a FIRST dial that fails, keeps the pre-slic…21
DC-PUMP-10derivedenforcedDeterministic, bounded reconnect backoff. Re-dial pacing follows a fixed const escalating schedule (RECONNECT_BACKOFF_SECS) that is monotone non-decreasing and …11
DC-QUERY-01deriveddeclaredN2C queries are era-aware, typed, and version-gated: each NodeToClientVersion gates which queries are available00
gap
DC-REF-01derivedpartialEvery claimed equivalence check must identify its reference source, extraction method, and reproducibility path101
DC-SEED-01derivedenforcedCanonical UtxoFingerprint determinism: the imported UTxOState uses BTreeMap<TxIn, TxOut> iteration order; UtxoFingerprint is Blake2b-256 over canonical CBOR map…62
DC-SERVEMEM-01derivedenforcedPeer-driven serve range work is bounded. The --mode node serve path must not materialize an unbounded chain range, perform per-block full-index scans, or read m…121
DC-SESS-01derivedenforcedHandshake-before-traffic: no mini-protocol frame reaches the orchestrator inbox until the handshake state machine has emitted Accepted. Type-state: a `MuxSessio…21
DC-SESS-02derivedenforcedClosed mini-protocol id registry: the dispatch table over `MiniProtocolId` is a closed `match` on a closed `AcceptedMiniProtocol` enum. Unknown ids return `Sess…41
DC-SESS-03derivedenforcedPer-mini-protocol ordering + session replay equivalence: replaying the same byte chunks through `session::core::step` yields byte-identical outbound frames and …31
DC-SESS-04derivedenforcedBackpressure discipline: every per-peer + per-mini-protocol channel is bounded; queue overflow is fail-fast `TransportError::BackpressureExceeded` rather than s…21
DC-SESS-05derivedenforcedWire-layer clock injection: the session reducer + dispatch table contain no SystemTime / Instant::now / tokio::time reads. Keep-alive is driven by the PHASE4-N-…31
DC-SESS-06derivedenforcedReplay equivalence under fragmented inbound streams: two reducer runs over the same byte-chunk sequence (including inputs where single CBOR items span multiple …31
DC-SNAPSHOT-01derivedenforcedServedChainHandle::push_atomic is deterministic in its argument order: the same sequence of push_atomic(a₀), push_atomic(a₁), ..., push_atomic(aₙ) produces a by…30
gap
DC-STORE-01derivedenforcedRecovery from power-loss produces replay-equivalent state41
DC-STORE-02derivedenforcedAppend-only provenance for finalized data31
DC-STORE-03derivedenforcedAtomic snapshots (fully written or absent)41
DC-STORE-04deriveddeclaredChainDB structure: ImmutableDB (append-only, blocks immutable when k-deep), VolatileDB (recent blocks within k), LedgerDB (snapshots + forward replay)00
gap
DC-STORE-05derivedenforcedRecovery is snapshot + forward replay (not full genesis replay): load most recent valid snapshot, replay forward from ImmutableDB tip41
DC-STORE-06deriveddeclaredVolatileDB uses ValidateAll after unclean shutdown; NoValidation acceptable during clean operation as optimization00
gap
DC-STORE-07derivedenforcedSnapshot cadence determinism: the decision to take a snapshot at slot S is a pure function of (slot, block_no, cadence_params, last_snapshot). Same canonical in…71
DC-STORE-08derivedenforcedSnapshot encoder canonicality: encode_snapshot(s) is byte-identical across runs. Encoder uses BTreeMap iteration only; no HashMap, no wall-clock, no floats, no …91
DC-STORE-09derivedenforcedSnapshot bytes carry a closed u32 version tag (initial == 1) and the source state's blake2b-256 fingerprint. Decoder reads the version tag first and rejects unk…31
DC-STORE-10trueenforcedReplay equivalence requires the persisted authority store and the binary to agree on the MEANING of the bytes, not merely on their layout. Every durable authori…101
DC-STORE-11derivedenforcedThe semantics marker is PER-ARTIFACT, and every authority artifact must agree with the binary independently. `chain.db` (with the WAL written in lockstep beside…41
DC-STORE-12releaseenforcedThe semantics version may not be left to memory. The declared semantics-bearing surface (`ci/store-semantics-surface.lock`) is content-hashed, and any drift fai…01
DC-SYNC-01derivedenforcedDuring network forward-sync, a block's preserved wire bytes and its WAL entry MUST be durable before the chain tip advances to it, and admission is chokepoint-o…72
DC-SYNC-02derivedenforcedContinuous relay sync: every loop iteration preserves durable-before-advance (DC-SYNC-01) and advances the tip ONLY through run_node_sync -> pump_block. Verdict…42
DC-TXV-01derivedenforcedtx_validity is a pure function of (LedgerState, tx_cbor). No wall-clock, arrival order, HashMap/HashSet iteration, float, or ambient state may influence a trans…11
DC-TXV-02derivedenforcedA transaction is Valid iff both phase-1 (structural + UTxO rules + witnesses) and phase-2 (Plutus, when scripts are present) accept it. No path may produce a Va…21
DC-TXV-03derivedenforcedAde's Valid/Invalid verdict for a transaction equals the reference cardano-node verdict, including the reason class where the reference exposes it. Established …171
DC-TXV-04derivedenforcedA Valid transaction yields an applied LedgerState' (the mempool's accumulating view); an Invalid transaction leaves the input state unchanged plus a structured …31
DC-TXV-05derivedenforcedFor each era, required_signers(state, tx_body) is a closed, explicit, era-versioned function over every signer source (resolved input payment credentials, expli…131
DC-TXV-06derivedenforcedFor each era, the certificate-deposit classification map(state, cert) is a closed, total, era-versioned function: every certificate variant resolves to exactly …101
DC-TXV-07derivedenforcedAll deposit/refund amounts used by Conway transaction value-conservation accounting must be sourced from canonical ledger protocol parameters or explicit certif…41
DC-VAL-01derivedenforcedA block's validity verdict is a pure function of (LedgerState, PraosChainDepState, EraSchedule, LedgerView, block_cbor). No wall-clock, arrival order, HashMap/H…81
DC-VAL-02derivedenforcedA block is Valid iff both the consensus header authority (validate_and_apply_header) and the ledger body authority (apply_block_with_verdicts) accept it. No pat…21
DC-VAL-03derivedenforcedThe header is validated before the body; body validation never runs on a header-invalid block. The first failing authority determines the reason (fail-fast orde…11
DC-VAL-04derivedenforcedAde's Valid/Invalid verdict for a block equals the reference cardano-node verdict, including the reason class where the reference exposes it. Established over b…61
DC-VAL-05derivedenforcedA Valid block yields evolved (LedgerState', PraosChainDepState'); an Invalid block yields the unchanged input states plus a structured reason. No partial or in-…21
DC-VAL-06derivedenforcedEvery crypto-input, field-size, and structural check on the authority path rejects (produces Invalid) on wrong size or shape and never silently skips. The patte…201
DC-VIEW-01derivedenforcedLiveLedgerView determinism + epoch-window guard. The view is constructed deterministically from LiveConsensusInputsCanonical. Two guards on every LedgerView qu…51
DC-WAL-01derivedenforcedWAL is append-only by type: the WalStore trait carries no method named truncate / rewrite / replace / delete / clear. CI grep enforces across the workspace (no …01
gap
DC-WAL-02derivedenforcedWAL fingerprint-chain integrity: every WalEntry::AdmitBlock has prior_fp == previous entry's post_fp (or anchor's initial_ledger_fingerprint for the first entry…61
DC-WAL-03derivedenforcedAnchor + WAL replay-equivalence: replaying (BootstrapAnchor + WAL entries 1..N) against (initial_ledger from import + per-entry block bytes) produces a final le…50
gap
DC-WAL-04derivedenforcedForged-block WAL chain integrity. A forged AdmitBlock WAL entry's prior_fp MUST equal the current durable post_fp (the BootstrapAnchor's initial_ledger_fingerpr…31
DC-WAL-05derivedenforcedReceived/followed-block durable-admit is BYTES-FIRST. The live admission runner (run_admission) MUST persist an admitted block's preserved ORIGINAL bytes to the…21
OP-MEM-01operationalpartialMempool pressure and peer churn must not starve block validation, chain selection, or persistence (scheduling priority)01
gap
OP-MEM-02operationalenforcedAde's owned resident memory (Private_Dirty/RssAnon) under a representative venue stays clearly below the reference Haskell cardano-node's on the same chain, WIT…22
OP-NET-01operationaldeclaredBlock producer connects only through trusted relay topology; no direct public peer connectivity00
gap
OP-NET-02operationaldeclaredRelay paths geographically and topologically diverse; isolating one path does not prevent timely propagation00
gap
OP-NET-03operationaldeclaredNo single peer, ASN, region, or operator cluster dominates the node's authoritative view00
gap
OP-OPS-01operationaldeclaredPost-incident reconciliation derived solely from recovered canonical chain00
gap
OP-OPS-02operationaldeclaredEmergency recovery procedures have explicit admissibility criteria, deterministic inputs/outputs, and authority thresholds00
gap
OP-OPS-03operationaldeclaredIncident evidence sufficient to reconstruct canonical decision path without relying on nondeterministic logs00
gap
OP-OPS-04operationalenforcedOperator-supplied keys. Ade supports both KES key flows: (a) Ade-native `ade_node --mode key_gen_kes --out-file PATH` emitting an `ade.kes.seed.v1` envelope loa…283
OP-OPS-05operationalenforcedSlot-deadline forging SLA. Forge + self-accept + N2N hand-off must complete within the slot's deadline (1s on mainnet, smaller on testnets). Operational, not co…11
RO-CLOSE-01releaseenforcedUnmasked close-gate discipline. Any slice that changes canonical bytes, encoded forms, decoder inputs, or golden fixtures MUST run an UNMASKED full close gate (…00
gap
RO-GENESIS-REPLAY-01releasedeclaredAde independently replays the chain from byron genesis through the bootstrap point P, producing the same UTxOState the oracle seed provides. Closes the "Ade has…01
gap
RO-LIVE-01releasepartialA Haskell cardano-node peer issuing RequestRange covering an Ade-forged block receives, via the producer-side block-fetch server, bytes that pass that peer's fu…71
RO-LIVE-02releasepartialA cardano-node peer's RollForward + BlockDelivered stream, consumed by the receive bridge, produces a ChainDb tip equal to the peer's announced tip at every ste…51
RO-LIVE-03releasedeclaredLive tip-following pass: operator runs `ade_node --peer ADDR` against a private cardano-node peer, captures a 30-minute JSONL log of (peer_tip, ade_tip, agreeme…00
gap
RO-LIVE-04releaseenforcedLive wire-smoke pass: operator runs `ade_node --mode wire_only --peer ADDR --network NAME` against a private cardano-node peer. The binary opens TCP, completes …112
RO-LIVE-05releaseenforcedLive admission-agreement pass: operator runs `ade_node` against a private cardano-node peer with admission enabled (bootstrap loads a real initial ledger state …41
RO-LIVE-06releaseenforcedBA-02 peer-acceptance evidence closure (SCHEMA + CORRELATION MECHANICS ONLY). The BA-02 evidence surface is a closed, versioned manifest (Ba02Manifest) plus a p…202
RO-MITHRIL-IMPORT-01releaseenforcedAde imports a Mithril-authenticated snapshot as an alternative to the cardano-cli JSON seed. Provides cryptographic provenance for the seed artifact (over and a…43
RO-REL-01releasedeclaredRelease not mainnet-eligible without mixed-version topology consensus equivalence on adversarial inputs00
gap
RO-REL-02releasedeclaredCross-implementation accept/reject agreement on authoritative corpora is release-blocking00
gap
RO-REL-03releasedeclaredNo single implementation bug should exceed the protocol's intended safety or liveness fault threshold at ecosystem level00
gap
RO-SYNC-EVIDENCE-01releasepartialA committed snapshot->tip sync-evidence manifest carries the closed schema (oracle versions, chain point, fixture refs, sha256, diff/acceptance result) and its …11
RO-TEST-01releasedeclaredConsensus-relevant inputs fuzzed differentially across all supported versions; any verdict mismatch is release-blocking00
gap
RO-TEST-02releasedeclaredEvery fork/mismatch/parser disagreement that ever occurred becomes a permanent regression corpus entry00
gap
RO-TEST-03releasedeclaredFailed, duplicate, and boundary-case inputs remain verdict-stable under resubmission and replay00
gap
T-BOUND-01truedeclaredShell may observe nondeterminism but must convert to deterministic inputs before entering core00
gap
T-BOUND-02trueenforcedAuthoritative crates never depend on shell crates01
gap
T-BUILD-01trueenforcedNo semantic build variability in authoritative code01
gap
T-BUILD-02truedeclaredOne semantic interpretation per protocol version and input set00
gap
T-CAUSAL-01truedeclaredFuture decisions may not leak into present validation; no retroactive reinterpretation of prior checkpoints00
gap
T-CI-01truepartialEvery true invariant has mechanical CI enforcement. No waivers.01
gap
T-COLL-01truedeclaredDeterministic iteration order for all semantically meaningful collections00
gap
T-CONS-01trueenforcedChain selection depends only on canonical observables; same candidates -> same tip62
T-CONS-02truedeclaredAuthoritative consensus decisions must not depend on wall-clock, arrival-order, scheduler, or OS behavior00
gap
T-CONSERV-01trueenforcedUTxO and asset conservation must hold for every accepted transition, except where protocol rules explicitly authorize mint, burn, rewards, or treasury effects41
T-CORE-01trueenforcedAuthoritative logic is pure, side-effect-free, and replayable22
T-CORE-02trueenforcedNo wall-clock, unseeded randomness, floats, or nondeterministic collections in authoritative paths52
T-CORE-03truedeclaredExplicit state transitions: consume old state, produce new state00
gap
T-CORE-04truedeclaredIllegal states unrepresentable via types where practical00
gap
T-DET-01trueenforcedSame canonical inputs -> same authoritative bytes (per Byte Authority Model)213
T-ENC-01truepartialAll persisted/hashed/transmitted data uses canonical encoding31
T-ENC-02truedeclaredNon-canonical bytes rejected deterministically00
gap
T-ENC-03trueenforcedRound-trip identity: encode(decode(bytes)) == bytes for valid encodings191
T-EPOCH-01truepartialExactly one authoritative committee and governance interpretation per epoch100
gap
T-ERR-01truepartialErrors in authoritative paths are structured, comparable, canonical30
gap
T-ERR-02truedeclaredSafety violations fail-fast deterministically00
gap
T-INGRESS-01truedeclaredAll authoritative external bytes enter the core through named canonical decode/validation chokepoints; unchecked bypasses forbidden except for explicitly whitel…01
gap
T-KEY-01truedeclaredSigning and private key operations confined to shell; verification in core00
gap
T-NOSPEND-01trueenforcedNo input or equivalent spend authority may be consumed more than once in an accepted canonical chain31
T-PLATFORM-01truedeclaredNo host-environment property (locale, timezone, architecture, platform) may influence authoritative computation results00
gap
T-REC-01trueenforcedRecovery is replay-equivalent: restart produces byte-identical state to clean run92
T-REC-02trueenforcedAll authoritative state derivable by replay from inputs21
T-REC-03trueenforcedLoop-as-replay: the same recovered/bootstrapped state + the same ordered canonical block feed (NodeBlockSource) + the same deterministic loop inputs + the same …11
T-REC-04trueenforcedThe WarmStart-recovered forge `chain_dep.epoch_nonce` (eta0) MUST come from the imported/recovered consensus input, never from a snapshot placeholder and never …51
T-REC-05trueenforcedReplay/recovery equivalence including forged admits. Same BootstrapAnchor + same WAL (including forged AdmitBlock entries) -> byte-identical recovered durable t…60
gap
T-REC-06trueenforcedRollback-materialization replay-equivalence (PHASE4-N-AN). A block that validates during live admit (against the eta0-overlaid chain_dep, T-REC-04) MUST NOT fai…21
T-RESOURCE-01truedeclaredUntrusted inputs must not allocate unbounded authoritative resources before deterministic validation00
gap
T-TRANSPORT-01truedeclaredTransport nondeterminism (socket fragmentation, mux ordering, timeouts) must not leak into authoritative logic00
gap