automatic signing mode
Apr 14, 6-7 PM (22)
Apr 14, 7-8 PM (14)
Apr 14, 8-9 PM (10)
Apr 14, 9-10 PM (11)
Apr 14, 10-11 PM (24)
Apr 14, 11-12 AM (24)
Apr 15, 12-1 AM (3)
Apr 15, 1-2 AM (9)
Apr 15, 2-3 AM (8)
Apr 15, 3-4 AM (1)
Apr 15, 4-5 AM (1)
Apr 15, 5-6 AM (32)
Apr 15, 6-7 AM (7)
Apr 15, 7-8 AM (25)
Apr 15, 8-9 AM (49)
Apr 15, 9-10 AM (40)
Apr 15, 10-11 AM (127)
Apr 15, 11-12 PM (53)
Apr 15, 12-1 PM (60)
Apr 15, 1-2 PM (43)
Apr 15, 2-3 PM (45)
Apr 15, 3-4 PM (29)
Apr 15, 4-5 PM (44)
Apr 15, 5-6 PM (21)
Apr 15, 6-7 PM (33)
Apr 15, 7-8 PM (15)
Apr 15, 8-9 PM (17)
Apr 15, 9-10 PM (5)
Apr 15, 10-11 PM (20)
Apr 15, 11-12 AM (16)
Apr 16, 12-1 AM (12)
Apr 16, 1-2 AM (6)
Apr 16, 2-3 AM (7)
Apr 16, 3-4 AM (3)
Apr 16, 4-5 AM (4)
Apr 16, 5-6 AM (8)
Apr 16, 6-7 AM (33)
Apr 16, 7-8 AM (32)
Apr 16, 8-9 AM (31)
Apr 16, 9-10 AM (27)
Apr 16, 10-11 AM (50)
Apr 16, 11-12 PM (56)
Apr 16, 12-1 PM (58)
Apr 16, 1-2 PM (30)
Apr 16, 2-3 PM (40)
Apr 16, 3-4 PM (46)
Apr 16, 4-5 PM (47)
Apr 16, 5-6 PM (56)
Apr 16, 6-7 PM (17)
Apr 16, 7-8 PM (68)
Apr 16, 8-9 PM (38)
Apr 16, 9-10 PM (11)
Apr 16, 10-11 PM (23)
Apr 16, 11-12 AM (23)
Apr 17, 12-1 AM (12)
Apr 17, 1-2 AM (8)
Apr 17, 2-3 AM (3)
Apr 17, 3-4 AM (4)
Apr 17, 4-5 AM (3)
Apr 17, 5-6 AM (9)
Apr 17, 6-7 AM (26)
Apr 17, 7-8 AM (96)
Apr 17, 8-9 AM (70)
Apr 17, 9-10 AM (53)
Apr 17, 10-11 AM (41)
Apr 17, 11-12 PM (58)
Apr 17, 12-1 PM (64)
Apr 17, 1-2 PM (39)
Apr 17, 2-3 PM (46)
Apr 17, 3-4 PM (36)
Apr 17, 4-5 PM (13)
Apr 17, 5-6 PM (10)
Apr 17, 6-7 PM (25)
Apr 17, 7-8 PM (22)
Apr 17, 8-9 PM (3)
Apr 17, 9-10 PM (16)
Apr 17, 10-11 PM (24)
Apr 17, 11-12 AM (16)
Apr 18, 12-1 AM (2)
Apr 18, 1-2 AM (2)
Apr 18, 2-3 AM (6)
Apr 18, 3-4 AM (1)
Apr 18, 4-5 AM (2)
Apr 18, 5-6 AM (2)
Apr 18, 6-7 AM (1)
Apr 18, 7-8 AM (2)
Apr 18, 8-9 AM (4)
Apr 18, 9-10 AM (4)
Apr 18, 10-11 AM (1)
Apr 18, 11-12 PM (6)
Apr 18, 12-1 PM (7)
Apr 18, 1-2 PM (8)
Apr 18, 2-3 PM (9)
Apr 18, 3-4 PM (0)
Apr 18, 4-5 PM (2)
Apr 18, 5-6 PM (6)
Apr 18, 6-7 PM (2)
Apr 18, 7-8 PM (2)
Apr 18, 8-9 PM (4)
Apr 18, 9-10 PM (9)
Apr 18, 10-11 PM (21)
Apr 18, 11-12 AM (23)
Apr 19, 12-1 AM (1)
Apr 19, 1-2 AM (4)
Apr 19, 2-3 AM (1)
Apr 19, 3-4 AM (0)
Apr 19, 4-5 AM (0)
Apr 19, 5-6 AM (2)
Apr 19, 6-7 AM (0)
Apr 19, 7-8 AM (2)
Apr 19, 8-9 AM (1)
Apr 19, 9-10 AM (1)
Apr 19, 10-11 AM (4)
Apr 19, 11-12 PM (7)
Apr 19, 12-1 PM (6)
Apr 19, 1-2 PM (8)
Apr 19, 2-3 PM (22)
Apr 19, 3-4 PM (7)
Apr 19, 4-5 PM (4)
Apr 19, 5-6 PM (3)
Apr 19, 6-7 PM (8)
Apr 19, 7-8 PM (3)
Apr 19, 8-9 PM (8)
Apr 19, 9-10 PM (6)
Apr 19, 10-11 PM (25)
Apr 19, 11-12 AM (23)
Apr 20, 12-1 AM (4)
Apr 20, 1-2 AM (5)
Apr 20, 2-3 AM (2)
Apr 20, 3-4 AM (7)
Apr 20, 4-5 AM (1)
Apr 20, 5-6 AM (6)
Apr 20, 6-7 AM (11)
Apr 20, 7-8 AM (29)
Apr 20, 8-9 AM (42)
Apr 20, 9-10 AM (37)
Apr 20, 10-11 AM (95)
Apr 20, 11-12 PM (42)
Apr 20, 12-1 PM (39)
Apr 20, 1-2 PM (53)
Apr 20, 2-3 PM (68)
Apr 20, 3-4 PM (47)
Apr 20, 4-5 PM (40)
Apr 20, 5-6 PM (31)
Apr 20, 6-7 PM (24)
Apr 20, 7-8 PM (10)
Apr 20, 8-9 PM (7)
Apr 20, 9-10 PM (16)
Apr 20, 10-11 PM (28)
Apr 20, 11-12 AM (18)
Apr 21, 12-1 AM (24)
Apr 21, 1-2 AM (5)
Apr 21, 2-3 AM (13)
Apr 21, 3-4 AM (4)
Apr 21, 4-5 AM (3)
Apr 21, 5-6 AM (8)
Apr 21, 6-7 AM (15)
Apr 21, 7-8 AM (44)
Apr 21, 8-9 AM (119)
Apr 21, 9-10 AM (36)
Apr 21, 10-11 AM (35)
Apr 21, 11-12 PM (98)
Apr 21, 12-1 PM (57)
Apr 21, 1-2 PM (71)
Apr 21, 2-3 PM (60)
Apr 21, 3-4 PM (31)
Apr 21, 4-5 PM (27)
Apr 21, 5-6 PM (25)
Apr 21, 6-7 PM (29)
3,847 commits this week
Apr 14, 2026
-
Apr 21, 2026
cardano: preserve managed kupo authenticated host
Snapshot of Frisby's SQLite latency investigation during 2026 March
cardano: tighten managed provider diagnostics
fix(ledger): wire into the response for past (closed) eras so their EraEnd reflects confirmed boundaries rather than the raw epoch-end slot
Signed-off-by: Chris Guiney <[email protected]>
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`), apply batch-wide direct deposits to the final CertState via `applyDirectDeposits` and `allDirectDeposits`. `Ledger.lagda.md`: + Update `LEDGER-V` output: compute `certStateFinal` by applying `allDirectDeposits` to `certState₂`, use `certStateFinal` in the output `LedgerState` and in `rmOrphanDRepVotes`; + `LEDGER-I` unchanged (invalid batches don't apply deposits); + Document direct deposit application ordering and phantom asset prevention rationale. `Ledger/Properties/Computational.lagda.md`: + Update `computeProof` valid branch to compute `certStateFinal` and use it in the output `LedgerState`.
CIP-159-11: Initial PoV property module skeletons (#1123)
Add preservation-of-value property modules for the Dijkstra era, adapted from the Conway PoV proof structure for CIP-159 (partial withdrawals and direct deposits). New modules: - Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov, PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics) - Certs.Properties.PoV: CERTS-pov top-level theorem - Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls - Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement with proof sketch for direct deposit cancellation Design notes: - PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction) instead of Conway's constMap/res-decomp/sumConstZero chain - LEDGER-pov identifies the applyDirectDeposits cancellation as the main new proof obligation vs Conway - applyWithdrawals-pov is structured as three layers: single-step (applyOne-pov), fold induction (foldl-applyOne-pov), top-level Status: Skeleton with holes; does not yet fully typecheck.
CIP-159-11: LEDGER-pov structure with LEDGER-I proved (#1123)
State and partially prove the Dijkstra LEDGER preservation-of-value theorem with the corrected HasCoin-LedgerState that includes deposits. - LEDGER-I (invalid case): Fully proved via utxow-pov-invalid. - LEDGER-V (valid case): Equational chain with holes, to be filled. The HasCoin-LedgerState total is: getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState) Key insight: SUBLEDGERS-pov cannot be proved independently because individual SUBUTXO rules have no balance premise — only the batch-level consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof must reason about the entire step at once.
`indexedSumᵛ'-∪` and `sumConstZero` have proofs!
There were unresolved proof obligations from Conway.
[Dijkstra] CIP-159-08: Phantom asset attack prevention (#1120)
Add batch-wide withdrawal bound check to prevent phantom asset attacks when nested transactions combine deposits and withdrawals. `Transaction.lagda.md`: + Define allWithdrawals batch aggregation helper (mirrors allDirectDeposits) `Utxo.lagda.md`: + Define NoPhantomWithdrawals predicate using allWithdrawals + Add NoPhantomWithdrawals premise to UTXO rule + Document phantom asset attack and spend-side safety analogy `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (21+h → 22+h)
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)
CIP-159 changes the transaction balancing rules and introduces Phase-1 balance interval validation. This commit updates the UTxO transition system accordingly. `Utxo.lagda.md`: + Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for pre-batch account balance lookups; + Add HasAccountBalances type class and instances; + Update producedTx to include direct deposit amounts on the produced side of the preservation-of-value equation; + Add direct deposit registration premise to UTXO and SUBUTXO (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`); + Add balance interval validation premise to UTXO and SUBUTXO (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using pre-batch account balances). `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (19+h → 21+h) `Ledger.lagda.md`: + Add accountBalances field to SubLedgerEnv; + Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, LEDGER-I using RewardsOf certState₀ (pre-batch balances).
CIP-159-11: applyWithdrawals-pov and new library lemmas (#1123)
Add the applyWithdrawals preservation-of-value proof machinery and prove several lemmas that were previously assumed as module parameters in Conway. New proofs in Ledger.Prelude (previously Conway module parameters): - indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ - sumConstZero: getCoin (constMap X 0) ≡ 0 - getCoin-cong: indexedSum' proj₂ respects set equality - res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ)) - getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡: singleton map getCoin lemmas - indexedSumL-proj₂-zero: sum of zero-valued entries is zero - setToList-∈: opaque bridge from list membership to set membership New module Certs.Properties.ApplyWithdrawalsPoV: - applyOne-pov: single withdrawal step decreases getCoin by amt - foldl-applyOne-pov: fold induction with Unique invariant - applyWithdrawals-pov: top-level lemma for PRE-CERT-pov - ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves domain membership for other credentials Remaining assumptions (deferred to agda-sets library): - ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys - sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ' - setToList-Unique: credential uniqueness of withdrawal list - ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming
CIP-159-11: LEDGER-pov fully structured, all holes filled (#1123)
Complete the LEDGER preservation-of-value proof structure for Dijkstra. - LEDGER-I: Fully proved via utxow-pov-invalid. - LEDGER-V: Complete equational chain with no holes or unresolved metas. Decomposes into: - step-i: combined CERTS accounting (sub + top level) - arithmetic-1, arithmetic-2: ℕ rearrangements - step-iii-iv: batch UTxO + deposit accounting (assumption) - step-ii: applyDirectDeposits cancellation (assumption) New sub-lemma proved: - SUBLEDGERS-certs-pov: induction on ReflexiveTransitiveClosure showing rewardsBalance decreases by exactly the sum of sub-withdrawal amounts. Dispatches SUBLEDGER-I (impossible when isTopLevelValid ≡ true) and SUBLEDGER-V (uses sub-level CERTS-pov with NetworkId extracted from SUBUTXOW → SUBUTXO premises). Remaining assumptions (module parameters): - batch-utxo-accounting: consumedBatch ≡ producedBatch coin projection combined with mechanical UTxO tracking and deposit accounting - applyDirectDeposits-rewardsBalance: gc-hom (∪⁺ distributes getCoin) - utxow-pov-invalid: collateral collection preserves getCoin utxoSt - ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`), apply batch-wide direct deposits to the final CertState via `applyDirectDeposits` and `allDirectDeposits`. `Ledger.lagda.md`: + Update `LEDGER-V` output: compute `certStateFinal` by applying `allDirectDeposits` to `certState₂`, use `certStateFinal` in the output `LedgerState` and in `rmOrphanDRepVotes`; + `LEDGER-I` unchanged (invalid batches don't apply deposits); + Document direct deposit application ordering and phantom asset prevention rationale. `Ledger/Properties/Computational.lagda.md`: + Update `computeProof` valid branch to compute `certStateFinal` and use it in the output `LedgerState`.
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)
CIP-159 changes the transaction balancing rules and introduces Phase-1 balance interval validation. This commit updates the UTxO transition system accordingly. `Utxo.lagda.md`: + Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for pre-batch account balance lookups; + Add HasAccountBalances type class and instances; + Update producedTx to include direct deposit amounts on the produced side of the preservation-of-value equation; + Add direct deposit registration premise to UTXO and SUBUTXO (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`); + Add balance interval validation premise to UTXO and SUBUTXO (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using pre-batch account balances). `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (19+h → 21+h) `Ledger.lagda.md`: + Add accountBalances field to SubLedgerEnv; + Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, LEDGER-I using RewardsOf certState₀ (pre-batch balances).
[Dijkstra] CIP-159-08: Phantom asset attack prevention (#1120)
Add batch-wide withdrawal bound check to prevent phantom asset attacks when nested transactions combine deposits and withdrawals. `Transaction.lagda.md`: + Define allWithdrawals batch aggregation helper (mirrors allDirectDeposits) `Utxo.lagda.md`: + Define NoPhantomWithdrawals predicate using allWithdrawals + Add NoPhantomWithdrawals premise to UTXO rule + Document phantom asset attack and spend-side safety analogy `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (21+h → 22+h)
[Dijkstra] CIP-159-08: Phantom asset attack prevention (#1120)
Add batch-wide withdrawal bound check to prevent phantom asset attacks when nested transactions combine deposits and withdrawals. `Transaction.lagda.md`: + Define allWithdrawals batch aggregation helper (mirrors allDirectDeposits) `Utxo.lagda.md`: + Define NoPhantomWithdrawals predicate using allWithdrawals + Add NoPhantomWithdrawals premise to UTXO rule + Document phantom asset attack and spend-side safety analogy `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (21+h → 22+h)
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)
CIP-159 changes the transaction balancing rules and introduces Phase-1 balance interval validation. This commit updates the UTxO transition system accordingly. `Utxo.lagda.md`: + Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for pre-batch account balance lookups; + Add HasAccountBalances type class and instances; + Update producedTx to include direct deposit amounts on the produced side of the preservation-of-value equation; + Add direct deposit registration premise to UTXO and SUBUTXO (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`); + Add balance interval validation premise to UTXO and SUBUTXO (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using pre-batch account balances). `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (19+h → 21+h) `Ledger.lagda.md`: + Add accountBalances field to SubLedgerEnv; + Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, LEDGER-I using RewardsOf certState₀ (pre-batch balances).
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`), apply batch-wide direct deposits to the final CertState via `applyDirectDeposits` and `allDirectDeposits`. `Ledger.lagda.md`: + Update `LEDGER-V` output: compute `certStateFinal` by applying `allDirectDeposits` to `certState₂`, use `certStateFinal` in the output `LedgerState` and in `rmOrphanDRepVotes`; + `LEDGER-I` unchanged (invalid batches don't apply deposits); + Document direct deposit application ordering and phantom asset prevention rationale. `Ledger/Properties/Computational.lagda.md`: + Update `computeProof` valid branch to compute `certStateFinal` and use it in the output `LedgerState`.
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)
CIP-159 changes the transaction balancing rules and introduces Phase-1 balance interval validation. This commit updates the UTxO transition system accordingly. `Utxo.lagda.md`: + Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for pre-batch account balance lookups; + Add HasAccountBalances type class and instances; + Update producedTx to include direct deposit amounts on the produced side of the preservation-of-value equation; + Add direct deposit registration premise to UTXO and SUBUTXO (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`); + Add balance interval validation premise to UTXO and SUBUTXO (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using pre-batch account balances). `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (19+h → 21+h) `Ledger.lagda.md`: + Add accountBalances field to SubLedgerEnv; + Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, LEDGER-I using RewardsOf certState₀ (pre-batch balances).
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)
CIP-159 changes the transaction balancing rules and introduces Phase-1 balance interval validation. This commit updates the UTxO transition system accordingly. `Utxo.lagda.md`: + Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for pre-batch account balance lookups; + Add HasAccountBalances type class and instances; + Update producedTx to include direct deposit amounts on the produced side of the preservation-of-value equation; + Add direct deposit registration premise to UTXO and SUBUTXO (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`); + Add balance interval validation premise to UTXO and SUBUTXO (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using pre-batch account balances). `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (19+h → 21+h) `Ledger.lagda.md`: + Add accountBalances field to SubLedgerEnv; + Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, LEDGER-I using RewardsOf certState₀ (pre-batch balances).
Rename choosePeerTx size-check bindings to match review
Align the parameter and pattern-match names with @nfrisby's suggested snippet: 'targetBytesSize' -> 'targetTxBytesSize', '_k' -> '_ebHash', '_offset' -> '_txOffset', 'sz' -> 'txBytesSize'. Pure rename; no behavioral change. Addresses @nfrisby's review comment (the C1 rename suggestion and the exact snippet at https://github.com/IntersectMBO/ouroboros-consensus/pull/1996#discussion_r3118984718).
caribic: update injective token swap demo
cardano: make provider failures explicit
cardano: harden preprod gateway runtime paths