formal-ledger-specifications - 17 commits this week

Home / Input Output / formal-ledger-specifications

Insights Pull Requests

Mar 17, 10-11 AM (0)

Mar 17, 11-12 PM (0)

Mar 17, 12-1 PM (0)

Mar 17, 1-2 PM (0)

Mar 17, 2-3 PM (0)

Mar 17, 3-4 PM (0)

Mar 17, 4-5 PM (0)

Mar 17, 5-6 PM (0)

Mar 17, 6-7 PM (0)

Mar 17, 7-8 PM (1)

Mar 17, 8-9 PM (1)

Mar 17, 9-10 PM (0)

Mar 17, 10-11 PM (0)

Mar 17, 11-12 AM (0)

Mar 18, 12-1 AM (0)

Mar 18, 1-2 AM (0)

Mar 18, 2-3 AM (0)

Mar 18, 3-4 AM (0)

Mar 18, 4-5 AM (0)

Mar 18, 5-6 AM (0)

Mar 18, 6-7 AM (0)

Mar 18, 7-8 AM (0)

Mar 18, 8-9 AM (0)

Mar 18, 9-10 AM (0)

Mar 18, 10-11 AM (0)

Mar 18, 11-12 PM (0)

Mar 18, 12-1 PM (0)

Mar 18, 1-2 PM (0)

Mar 18, 2-3 PM (0)

Mar 18, 3-4 PM (0)

Mar 18, 4-5 PM (0)

Mar 18, 5-6 PM (0)

Mar 18, 6-7 PM (0)

Mar 18, 7-8 PM (0)

Mar 18, 8-9 PM (0)

Mar 18, 9-10 PM (0)

Mar 18, 10-11 PM (0)

Mar 18, 11-12 AM (0)

Mar 19, 12-1 AM (0)

Mar 19, 1-2 AM (0)

Mar 19, 2-3 AM (0)

Mar 19, 3-4 AM (0)

Mar 19, 4-5 AM (0)

Mar 19, 5-6 AM (0)

Mar 19, 6-7 AM (1)

Mar 19, 7-8 AM (0)

Mar 19, 8-9 AM (0)

Mar 19, 9-10 AM (0)

Mar 19, 10-11 AM (0)

Mar 19, 11-12 PM (0)

Mar 19, 12-1 PM (0)

Mar 19, 1-2 PM (1)

Mar 19, 2-3 PM (0)

Mar 19, 3-4 PM (0)

Mar 19, 4-5 PM (0)

Mar 19, 5-6 PM (0)

Mar 19, 6-7 PM (0)

Mar 19, 7-8 PM (0)

Mar 19, 8-9 PM (0)

Mar 19, 9-10 PM (0)

Mar 19, 10-11 PM (0)

Mar 19, 11-12 AM (0)

Mar 20, 12-1 AM (0)

Mar 20, 1-2 AM (0)

Mar 20, 2-3 AM (0)

Mar 20, 3-4 AM (1)

Mar 20, 4-5 AM (1)

Mar 20, 5-6 AM (0)

Mar 20, 6-7 AM (0)

Mar 20, 7-8 AM (0)

Mar 20, 8-9 AM (0)

Mar 20, 9-10 AM (2)

Mar 20, 10-11 AM (1)

Mar 20, 11-12 PM (1)

Mar 20, 12-1 PM (1)

Mar 20, 1-2 PM (0)

Mar 20, 2-3 PM (0)

Mar 20, 3-4 PM (1)

Mar 20, 4-5 PM (1)

Mar 20, 5-6 PM (0)

Mar 20, 6-7 PM (0)

Mar 20, 7-8 PM (0)

Mar 20, 8-9 PM (0)

Mar 20, 9-10 PM (0)

Mar 20, 10-11 PM (0)

Mar 20, 11-12 AM (0)

Mar 21, 12-1 AM (0)

Mar 21, 1-2 AM (0)

Mar 21, 2-3 AM (0)

Mar 21, 3-4 AM (0)

Mar 21, 4-5 AM (0)

Mar 21, 5-6 AM (0)

Mar 21, 6-7 AM (0)

Mar 21, 7-8 AM (0)

Mar 21, 8-9 AM (0)

Mar 21, 9-10 AM (0)

Mar 21, 10-11 AM (0)

Mar 21, 11-12 PM (0)

Mar 21, 12-1 PM (0)

Mar 21, 1-2 PM (0)

Mar 21, 2-3 PM (0)

Mar 21, 3-4 PM (0)

Mar 21, 4-5 PM (0)

Mar 21, 5-6 PM (0)

Mar 21, 6-7 PM (0)

Mar 21, 7-8 PM (0)

Mar 21, 8-9 PM (0)

Mar 21, 9-10 PM (0)

Mar 21, 10-11 PM (0)

Mar 21, 11-12 AM (0)

Mar 22, 12-1 AM (0)

Mar 22, 1-2 AM (0)

Mar 22, 2-3 AM (0)

Mar 22, 3-4 AM (0)

Mar 22, 4-5 AM (0)

Mar 22, 5-6 AM (0)

Mar 22, 6-7 AM (0)

Mar 22, 7-8 AM (0)

Mar 22, 8-9 AM (0)

Mar 22, 9-10 AM (0)

Mar 22, 10-11 AM (0)

Mar 22, 11-12 PM (0)

Mar 22, 12-1 PM (0)

Mar 22, 1-2 PM (0)

Mar 22, 2-3 PM (0)

Mar 22, 3-4 PM (0)

Mar 22, 4-5 PM (0)

Mar 22, 5-6 PM (0)

Mar 22, 6-7 PM (0)

Mar 22, 7-8 PM (0)

Mar 22, 8-9 PM (0)

Mar 22, 9-10 PM (0)

Mar 22, 10-11 PM (0)

Mar 22, 11-12 AM (0)

Mar 23, 12-1 AM (0)

Mar 23, 1-2 AM (0)

Mar 23, 2-3 AM (0)

Mar 23, 3-4 AM (0)

Mar 23, 4-5 AM (0)

Mar 23, 5-6 AM (0)

Mar 23, 6-7 AM (0)

Mar 23, 7-8 AM (0)

Mar 23, 8-9 AM (0)

Mar 23, 9-10 AM (0)

Mar 23, 10-11 AM (0)

Mar 23, 11-12 PM (0)

Mar 23, 12-1 PM (0)

Mar 23, 1-2 PM (0)

Mar 23, 2-3 PM (0)

Mar 23, 3-4 PM (1)

Mar 23, 4-5 PM (1)

Mar 23, 5-6 PM (0)

Mar 23, 6-7 PM (0)

Mar 23, 7-8 PM (0)

Mar 23, 8-9 PM (0)

Mar 23, 9-10 PM (0)

Mar 23, 10-11 PM (2)

Mar 23, 11-12 AM (0)

Mar 24, 12-1 AM (0)

Mar 24, 1-2 AM (0)

Mar 24, 2-3 AM (0)

Mar 24, 3-4 AM (0)

Mar 24, 4-5 AM (0)

Mar 24, 5-6 AM (0)

Mar 24, 6-7 AM (0)

Mar 24, 7-8 AM (0)

Mar 24, 8-9 AM (0)

Mar 24, 9-10 AM (0)

Mar 24, 10-11 AM (0)

17 commits this week Mar 17, 2026 - Mar 24, 2026

williamdemeo · Mon, 23 Mar 26 23:43:56 +0000 · formal-ledger-specifications

[Dijkstra] CIP-159-02: Extend TxBody

Closes #1114 by adding the two new transaction body fields required by [CIP-159](https://github.com/cardano-foundation/CIPs/tree/master/CIP-0159) (Account Address Enhancement) to the Dijkstra-era `TxBody` record, along with type class accessors and batch-wide aggregation helpers.

2f5677f0 · 1114-cip-159-02-extend-txbody · 1/45 ++ 0 --

williamdemeo · Mon, 23 Mar 26 23:43:56 +0000 · formal-ledger-specifications

update CHANGELOG

60b87cf6 · 1114-cip-159-02-extend-txbody · 1/1 ++ 0 --

github-actions[bot] · Mon, 23 Mar 26 17:55:30 +0000 · formal-ledger-specifications

Artifacts generated from 1620bfc1978732c1341a5ee193204aeeaa47acf0

b719449d · master-artifacts · 300/365,033 ++ 157,365 --

carlostome · Mon, 23 Mar 26 16:19:27 +0000 · formal-ledger-specifications

Refactor HSLedger

23afdc63 · master · 34/716 ++ 330 --

github-actions[bot] · Fri, 20 Mar 26 17:56:24 +0000 · formal-ledger-specifications

Artifacts generated from f7b29bf9749024ec39b928792ac36e8cc4ea443f

4fe44aa5 · carlos/dijkstra-conformance-artifacts · 44/3,237 ++ 3,216 --

carlostome · Fri, 20 Mar 26 16:56:37 +0000 · formal-ledger-specifications

Flatten HSLedger hierarchy

64ed2ba2 · carlos/dijkstra-conformance · 28/172 ++ 173 --

github-actions[bot] · Fri, 20 Mar 26 13:48:58 +0000 · formal-ledger-specifications

Artifacts generated from 4e8e7571f1dfe4ca1c2d6ce4f7db3e1f22a131c8

f2dc39f4 · master-artifacts · 44/3,247 ++ 3,219 --

carlostome · Fri, 20 Mar 26 12:49:19 +0000 · formal-ledger-specifications

Fix alignment

4e8e7571 · master · 1/3 ++ 2 --

carlostome · Fri, 20 Mar 26 11:18:20 +0000 · formal-ledger-specifications

Fix mkdocs

c6c1f757 · carlos/dijkstra-conformance · 3/15 ++ 4 --

carlostome · Fri, 20 Mar 26 10:58:08 +0000 · formal-ledger-specifications

Add missing preconditions to SUBUTXOW

b7be9fdd · carlos/subutxow · 4/45 ++ 8 --

github-actions[bot] · Fri, 20 Mar 26 10:47:31 +0000 · formal-ledger-specifications

Artifacts generated from 3343095f0e4305975db81437ceefb3f5a33bd79e

ae4d4d8e · carlos/subutxow-artifacts · 51/17,338 ++ 2,585 --

williamdemeo · Fri, 20 Mar 26 05:40:33 +0000 · formal-ledger-specifications

suggestions from review of #1124

8543938d · 1114-cip-159-02-extend-txbody · 1/28 ++ 26 --

williamdemeo · Fri, 20 Mar 26 04:51:46 +0000 · formal-ledger-specifications

update CHANGELOG

9d490e27 · 1114-cip-159-02-extend-txbody · 1/1 ++ 0 --

carlostome · Thu, 19 Mar 26 14:15:54 +0000 · formal-ledger-specifications

Refactor HSLedger

a0c1244d · carlos/dijkstra-conformance · 34/716 ++ 330 --

carlostome · Thu, 19 Mar 26 07:46:13 +0000 · formal-ledger-specifications

Refactor HSLedger

321f0611 · carlos/dijkstra-conformance · 32/708 ++ 322 --

williamdemeo · Tue, 17 Mar 26 21:16:35 +0000 · formal-ledger-specifications

remove irrelevant implementation notes

b724a420 · 1115-cip-159-03-extend-dstate · 1/3 ++ 23 --

williamdemeo · Tue, 17 Mar 26 20:41:57 +0000 · formal-ledger-specifications

Refactor BalanceInterval as richer type

- `BalanceInterval` is now a three-constructor `data` type instead of a type alias
- `open import Tactic.Derive.DecEq` added to the preamble
- `DecEq-BalanceInterval` derived via `unquoteDecl`
- `inBalanceInterval` constructors renamed: `both` → `inBoth`, `lower` → `inLower`, `upper` → `inUpper` (to avoid name clashes with the `BalanceInterval` constructors)
- `Dec-inBalanceInterval` now matches on `both lo hi`, `lower lo`, `upper hi` directly — cleaner, with no impossible `(nothing, nothing)` case

**One thing to watch for**.  The `inBalanceInterval` constructor names changed (`both` → `inBoth`, etc.), so if any downstream code in the #1114 or #1115 branches pattern-matches on these, it will need updating.

ff9c627f · 1113-cip-159-01-core-types · 1/26 ++ 55 --

Showing 17 of 17 recent commits. Check out Input Output on GitHub to see more.