typst-agda-spec-3: Add the Agda formalisation of the specification - #2786
typst-agda-spec-3: Add the Agda formalisation of the specification#2786noonio wants to merge 2 commits into
Conversation
Transaction cost differencesNo cost or size differences found |
82c7343 to
5e520d5
Compare
f16c983 to
c998d82
Compare
End-to-end benchmark differencesComparing this PR ( Sustained load (3 nodes, 3x5000 txs)
Plateau 1000 UTxO (1 node, 4000 txs)
Round-trip latency (3 nodes, closed-loop, 3x250 txs)
|
Transaction costsSizes and execution budgets for Hydra protocol transactions. Note that unlisted parameters are currently using
Script summary
|
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 5475 | 9.33 | 3.06 | 0.49 |
| 2 | 5571 | 10.02 | 3.29 | 0.50 |
| 3 | 5667 | 10.15 | 3.32 | 0.51 |
| 5 | 5860 | 11.16 | 3.64 | 0.52 |
| 10 | 6340 | 14.06 | 4.58 | 0.58 |
| 50 | 10180 | 35.59 | 11.33 | 0.97 |
| 100 | 14982 | 61.99 | 19.57 | 1.45 |
| 114 | 16326 | 69.36 | 21.87 | 1.59 |
Cost of Increment Transaction
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 2321 | 21.24 | 7.55 | 0.48 |
| 2 | 2452 | 22.19 | 8.52 | 0.50 |
| 3 | 2583 | 23.30 | 9.54 | 0.52 |
| 5 | 2846 | 25.22 | 11.48 | 0.56 |
| 10 | 3501 | 29.65 | 16.21 | 0.66 |
| 50 | 8741 | 71.41 | 55.94 | 1.52 |
| 75 | 12015 | 96.99 | 80.60 | 2.04 |
Cost of Decrement Transaction
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 642 | 18.46 | 6.68 | 0.38 |
| 2 | 777 | 19.43 | 7.65 | 0.40 |
| 3 | 904 | 20.37 | 8.62 | 0.42 |
| 5 | 1167 | 22.31 | 10.57 | 0.46 |
| 10 | 1825 | 27.16 | 15.44 | 0.56 |
| 50 | 7063 | 67.90 | 54.84 | 1.40 |
| 75 | 10337 | 93.55 | 79.51 | 1.93 |
Close transaction costs
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 666 | 17.78 | 11.67 | 0.41 |
| 2 | 800 | 18.76 | 12.65 | 0.43 |
| 3 | 931 | 19.69 | 13.61 | 0.45 |
| 10 | 1849 | 26.62 | 20.49 | 0.59 |
| 50 | 7086 | 67.30 | 59.96 | 1.44 |
| 75 | 10362 | 93.98 | 84.98 | 1.98 |
Contest transaction costs
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 700 | 21.50 | 14.91 | 0.46 |
| 2 | 832 | 22.64 | 15.93 | 0.48 |
| 3 | 959 | 23.79 | 16.96 | 0.51 |
| 5 | 1226 | 26.09 | 19.02 | 0.55 |
| 10 | 1881 | 31.79 | 24.16 | 0.66 |
| 50 | 7121 | 80.27 | 65.94 | 1.59 |
| 67 | 9348 | 99.93 | 83.43 | 1.97 |
FanOut transaction costs
Involves spending head output and burning head tokens. Uses ada-only UTXO for better comparability.
| Parties | UTxO | UTxO (bytes) | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|---|---|
| 10 | 0 | 0 | 5645 | 23.29 | 42.87 | 0.90 |
| 10 | 1 | 57 | 5678 | 25.63 | 45.39 | 0.93 |
| 10 | 5 | 283 | 5812 | 35.88 | 55.71 | 1.10 |
| 10 | 10 | 567 | 5982 | 49.89 | 68.99 | 1.31 |
| 10 | 20 | 1138 | 6322 | 82.42 | 96.97 | 1.79 |
| 10 | 20 | 1138 | 6322 | 82.42 | 96.97 | 1.79 |
PartialFanOut transaction costs
Largest chunk of ada-only outputs that can be distributed in one partial fanout step, computed dynamically. The last row is the maximum total UTxO count where at least one output can still be distributed.
| Distributed | UTxO (bytes) | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|---|
| 11 | 567 | 984 | 34.91 | 66.33 | 0.95 |
| 25 | 1310 | 1425 | 68.24 | 99.40 | 1.48 |
| 30 | 1311 | 1430 | 68.24 | 99.40 | 1.48 |
| 40 | 1308 | 1427 | 68.24 | 99.40 | 1.48 |
| 50 | 1312 | 1431 | 68.24 | 99.40 | 1.48 |
| 100 | 1307 | 1426 | 68.24 | 99.40 | 1.48 |
| 150 | 1308 | 1423 | 68.24 | 99.40 | 1.48 |
| 200 | 1311 | 1430 | 68.24 | 99.40 | 1.48 |
| 200 | 1307 | 1426 | 68.24 | 99.40 | 1.48 |
PartialFanOut transaction costs (with native tokens)
Largest chunk of native-token outputs that can be distributed in one partial fanout step, computed dynamically. The last row is the maximum total UTxO count where at least one output can still be distributed.
| Distributed | UTxO (bytes) | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|---|
| 11 | 1080 | 1565 | 42.00 | 68.86 | 1.05 |
| 25 | 2037 | 2276 | 76.59 | 99.12 | 1.58 |
| 30 | 2142 | 2390 | 76.59 | 99.17 | 1.59 |
| 40 | 2436 | 2698 | 76.56 | 99.22 | 1.60 |
| 50 | 2331 | 2589 | 76.59 | 99.22 | 1.60 |
| 100 | 2415 | 2677 | 76.56 | 99.22 | 1.60 |
| 150 | 2184 | 2431 | 76.59 | 99.17 | 1.59 |
| 200 | 2163 | 2413 | 76.56 | 99.16 | 1.59 |
| 200 | 2247 | 2501 | 76.59 | 99.17 | 1.59 |
FinalPartialFanOut transaction costs (with native tokens)
Terminal partial fanout step (FanoutProgress → Final) with outputs carrying a native token. Burns all head tokens and proves accumulator exhaustion via BLS proof.
| Distributed | UTxO (bytes) | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|---|
| 1 | 108 | 5528 | 22.10 | 44.31 | 0.89 |
| 5 | 485 | 5820 | 35.70 | 55.82 | 1.10 |
| 10 | 1020 | 6250 | 53.90 | 70.62 | 1.37 |
| 10 | 1060 | 6290 | 53.78 | 70.59 | 1.37 |
End-to-end benchmark results
This page is intended to collect the latest end-to-end benchmark results produced by Hydra's continuous integration (CI) system from the latest master code.
Please note that these results are approximate as they are currently produced from limited cloud VMs and not controlled hardware. Rather than focusing on the absolute results, the emphasis should be on relative results, such as how the timings for a scenario evolve as the code changes.
Generated at 2026-07-28 05:01:44.775227373 UTC
Baseline Scenario
| Number of nodes | 1 |
|---|---|
| Number of txs | 300 |
| Avg. Confirmation Time (ms) | 188.6 |
| P99 | 193.2ms |
| P95 | 192.7ms |
| P50 | 188.7ms |
| Tx validation time p50 (ms) | 120.7 |
| End-to-end TPS | 1508.87 tx/s |
| Backlog drain time (s) | 0.2 |
| Snapshots observed | 3 |
| Snapshots per second | 15.09 /s |
| Avg txs per snapshot | 100.0 |
| Peak node RSS (MB) | 144.6 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Three local nodes
| Number of nodes | 3 |
|---|---|
| Number of txs | 900 |
| Avg. Confirmation Time (ms) | 979.6 |
| P99 | 1039.0ms |
| P95 | 1037.8ms |
| P50 | 1009.2ms |
| Tx validation time p50 (ms) | 470.7 |
| End-to-end TPS | 858.77 tx/s |
| Backlog drain time (s) | 1.0 |
| Snapshots observed | 3 |
| Snapshots per second | 2.86 /s |
| Avg txs per snapshot | 300.0 |
| Peak node RSS (MB) | 147.3 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
Scenario benchmark results
This page collects results from the scenario matrix: every combination of cluster size, UTxO shape, and incremental-ops mode is exercised by CI from the latest master code and reported below.
Numbers are approximate. They come from cloud VMs rather than controlled hardware, so the useful signal is the relative change between cells and between commits, not the absolute throughput.
Generated at 2026-07-28 05:01:51.317068085 UTC
Summary across cells
TPS columns are rates (transactions per second); Wall clock (s) is the measured elapsed time from the first tx submission to the last confirmation. Times are rounded to one decimal.
| Scenario | Txs | Wall clock (s) | End-to-end TPS (tx/s) | Sustained TPS (tx/s) | Avg conf (ms) | P95 conf (ms) |
|---|---|---|---|---|---|---|
| Nodes=1, Constant, fire and forget | 30 | 0.0 | 1063.89 | n/a | 27.5 | 27.9 |
| Nodes=1, Constant, wait for tx valid | 30 | 0.2 | 173.80 | 171.53 | 5.7 | 6.9 |
| Nodes=1, Growing, fire and forget | 30 | 0.0 | 849.79 | n/a | 34.4 | 35.0 |
| Nodes=1, Growing, wait for tx valid | 30 | 0.2 | 132.35 | 130.36 | 7.5 | 11.3 |
| Nodes=1, Mixed, fire and forget | 30 | 0.0 | 851.00 | n/a | 34.3 | 35.0 |
| Nodes=1, Mixed, wait for tx valid | 30 | 0.2 | 136.77 | 131.37 | 7.2 | 10.3 |
| Nodes=2, Constant, fire and forget | 60 | 0.1 | 871.50 | n/a | 67.5 | 68.3 |
| Nodes=2, Constant, wait for tx valid | 60 | 0.5 | 124.94 | 127.78 | 15.7 | 20.1 |
| Nodes=2, Growing, fire and forget | 60 | 0.1 | 712.29 | n/a | 82.0 | 83.7 |
| Nodes=2, Growing, wait for tx valid | 60 | 0.7 | 81.41 | 80.41 | 24.3 | 30.9 |
| Nodes=2, Mixed, fire and forget | 60 | 0.1 | 757.32 | n/a | 76.9 | 78.2 |
| Nodes=2, Mixed, wait for tx valid | 60 | 0.7 | 82.49 | 78.08 | 24.0 | 31.5 |
| Nodes=3, Constant, fire and forget | 90 | 0.1 | 614.42 | n/a | 140.9 | 145.2 |
| Nodes=3, Constant, wait for tx valid | 90 | 1.0 | 89.44 | 90.09 | 33.0 | 43.7 |
| Nodes=3, Growing, fire and forget | 90 | 0.2 | 479.57 | n/a | 181.7 | 185.2 |
| Nodes=3, Growing, wait for tx valid | 90 | 1.5 | 61.01 | 61.80 | 48.0 | 64.2 |
| Nodes=3, Mixed, fire and forget | 90 | 0.2 | 538.22 | n/a | 162.5 | 166.9 |
| Nodes=3, Mixed, wait for tx valid | 90 | 1.2 | 74.99 | 71.94 | 39.2 | 52.3 |
Nodes=1, Constant, fire and forget
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 27.5 |
| P99 | 27.9ms |
| P95 | 27.9ms |
| P50 | 27.6ms |
| Tx validation time p50 (ms) | 14.4 |
| End-to-end TPS | 1063.89 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 2 |
| Snapshots per second | 70.93 /s |
| Avg txs per snapshot | 15.0 |
| Peak node RSS (MB) | 144.9 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=1, Constant, wait for tx valid
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 5.7 |
| P99 | 11.2ms |
| P95 | 6.9ms |
| P50 | 5.3ms |
| Tx validation time p50 (ms) | 1.8 |
| End-to-end TPS | 173.80 tx/s |
| Sustained TPS | 171.53 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 30 |
| Snapshots per second | 173.80 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 142.9 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=1, Growing, fire and forget
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 34.4 |
| P99 | 35.0ms |
| P95 | 35.0ms |
| P50 | 34.7ms |
| Tx validation time p50 (ms) | 13.8 |
| End-to-end TPS | 849.79 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 2 |
| Snapshots per second | 56.65 /s |
| Avg txs per snapshot | 15.0 |
| Peak node RSS (MB) | 143.3 |
| Number of Invalid txs | 0 |
| Fanout outputs | 31 |
Nodes=1, Growing, wait for tx valid
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 7.5 |
| P99 | 13.3ms |
| P95 | 11.3ms |
| P50 | 6.8ms |
| Tx validation time p50 (ms) | 2.0 |
| End-to-end TPS | 132.35 tx/s |
| Sustained TPS | 130.36 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 30 |
| Snapshots per second | 132.35 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 143.6 |
| Number of Invalid txs | 0 |
| Fanout outputs | 31 |
Nodes=1, Mixed, fire and forget
Each client first grows its UTxO set (1-in to 2-out) for half of its tx budget, then contracts it back (2-in to 1-out) for the remainder.
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 34.3 |
| P99 | 35.0ms |
| P95 | 35.0ms |
| P50 | 34.6ms |
| Tx validation time p50 (ms) | 14.0 |
| End-to-end TPS | 851.00 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 2 |
| Snapshots per second | 56.73 /s |
| Avg txs per snapshot | 15.0 |
| Peak node RSS (MB) | 145.0 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=1, Mixed, wait for tx valid
Each client first grows its UTxO set (1-in to 2-out) for half of its tx budget, then contracts it back (2-in to 1-out) for the remainder.
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 7.2 |
| P99 | 11.5ms |
| P95 | 10.3ms |
| P50 | 6.9ms |
| Tx validation time p50 (ms) | 2.1 |
| End-to-end TPS | 136.77 tx/s |
| Sustained TPS | 131.37 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 30 |
| Snapshots per second | 136.77 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 144.3 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=2, Constant, fire and forget
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 67.5 |
| P99 | 68.4ms |
| P95 | 68.3ms |
| P50 | 67.8ms |
| Tx validation time p50 (ms) | 29.6 |
| End-to-end TPS | 871.50 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 29.05 /s |
| Avg txs per snapshot | 30.0 |
| Peak node RSS (MB) | 144.9 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=2, Constant, wait for tx valid
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 15.7 |
| P99 | 24.6ms |
| P95 | 20.1ms |
| P50 | 15.1ms |
| Tx validation time p50 (ms) | 4.8 |
| End-to-end TPS | 124.94 tx/s |
| Sustained TPS | 127.78 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 60 |
| Snapshots per second | 124.94 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 144.1 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=2, Growing, fire and forget
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 82.0 |
| P99 | 83.7ms |
| P95 | 83.7ms |
| P50 | 82.6ms |
| Tx validation time p50 (ms) | 28.4 |
| End-to-end TPS | 712.29 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 23.74 /s |
| Avg txs per snapshot | 30.0 |
| Peak node RSS (MB) | 144.1 |
| Number of Invalid txs | 0 |
| Fanout outputs | 62 |
Nodes=2, Growing, wait for tx valid
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 24.3 |
| P99 | 34.1ms |
| P95 | 30.9ms |
| P50 | 24.5ms |
| Tx validation time p50 (ms) | 7.8 |
| End-to-end TPS | 81.41 tx/s |
| Sustained TPS | 80.41 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 60 |
| Snapshots per second | 81.41 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 146.9 |
| Number of Invalid txs | 0 |
| Fanout outputs | 62 |
Nodes=2, Mixed, fire and forget
Each client first grows its UTxO set (1-in to 2-out) for half of its tx budget, then contracts it back (2-in to 1-out) for the remainder.
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 76.9 |
| P99 | 78.3ms |
| P95 | 78.2ms |
| P50 | 77.4ms |
| Tx validation time p50 (ms) | 36.7 |
| End-to-end TPS | 757.32 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 25.24 /s |
| Avg txs per snapshot | 30.0 |
| Peak node RSS (MB) | 145.2 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=2, Mixed, wait for tx valid
Each client first grows its UTxO set (1-in to 2-out) for half of its tx budget, then contracts it back (2-in to 1-out) for the remainder.
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 24.0 |
| P99 | 34.2ms |
| P95 | 31.5ms |
| P50 | 23.7ms |
| Tx validation time p50 (ms) | 7.3 |
| End-to-end TPS | 82.49 tx/s |
| Sustained TPS | 78.08 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 60 |
| Snapshots per second | 82.49 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 146.7 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=3, Constant, fire and forget
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 140.9 |
| P99 | 145.3ms |
| P95 | 145.2ms |
| P50 | 142.0ms |
| Tx validation time p50 (ms) | 46.5 |
| End-to-end TPS | 614.42 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 13.65 /s |
| Avg txs per snapshot | 45.0 |
| Peak node RSS (MB) | 146.4 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
Nodes=3, Constant, wait for tx valid
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 33.0 |
| P99 | 47.1ms |
| P95 | 43.7ms |
| P50 | 32.7ms |
| Tx validation time p50 (ms) | 9.2 |
| End-to-end TPS | 89.44 tx/s |
| Sustained TPS | 90.09 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 61 |
| Snapshots per second | 60.62 /s |
| Avg txs per snapshot | 1.5 |
| Peak node RSS (MB) | 144.4 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
Nodes=3, Growing, fire and forget
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 181.7 |
| P99 | 185.5ms |
| P95 | 185.2ms |
| P50 | 183.3ms |
| Tx validation time p50 (ms) | 67.2 |
| End-to-end TPS | 479.57 tx/s |
| Backlog drain time (s) | 0.2 |
| Snapshots observed | 2 |
| Snapshots per second | 10.66 /s |
| Avg txs per snapshot | 45.0 |
| Peak node RSS (MB) | 145.4 |
| Number of Invalid txs | 0 |
| Fanout outputs | 0 |
Nodes=3, Growing, wait for tx valid
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 48.0 |
| P99 | 65.8ms |
| P95 | 64.2ms |
| P50 | 48.9ms |
| Tx validation time p50 (ms) | 12.2 |
| End-to-end TPS | 61.01 tx/s |
| Sustained TPS | 61.80 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 62 |
| Snapshots per second | 42.03 /s |
| Avg txs per snapshot | 1.5 |
| Peak node RSS (MB) | 146.4 |
| Number of Invalid txs | 0 |
| Fanout outputs | 0 |
Nodes=3, Mixed, fire and forget
Each client first grows its UTxO set (1-in to 2-out) for half of its tx budget, then contracts it back (2-in to 1-out) for the remainder.
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 162.5 |
| P99 | 167.0ms |
| P95 | 166.9ms |
| P50 | 164.2ms |
| Tx validation time p50 (ms) | 55.8 |
| End-to-end TPS | 538.22 tx/s |
| Backlog drain time (s) | 0.2 |
| Snapshots observed | 2 |
| Snapshots per second | 11.96 /s |
| Avg txs per snapshot | 45.0 |
| Peak node RSS (MB) | 144.3 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
Nodes=3, Mixed, wait for tx valid
Each client first grows its UTxO set (1-in to 2-out) for half of its tx budget, then contracts it back (2-in to 1-out) for the remainder.
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 39.2 |
| P99 | 56.1ms |
| P95 | 52.3ms |
| P50 | 39.0ms |
| Tx validation time p50 (ms) | 11.0 |
| End-to-end TPS | 74.99 tx/s |
| Sustained TPS | 71.94 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 62 |
| Snapshots per second | 51.66 /s |
| Avg txs per snapshot | 1.5 |
| Peak node RSS (MB) | 147.1 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
5e520d5 to
611c1f0
Compare
c998d82 to
9b8c98b
Compare
611c1f0 to
f1d7b41
Compare
9b8c98b to
0e92b08
Compare
f1d7b41 to
ca4bf10
Compare
0e92b08 to
675ab4a
Compare
ca4bf10 to
856748e
Compare
675ab4a to
8d384ed
Compare
Populate the literate sources with their Agda content and machine-check them as part of the spec build: - Re-add the Agda code blocks to the .lagda.typ tree (datum/redeemer types, transition relations, validity bundles, coverage/safety and security theorems and proofs), which now render in the formalisation appendix. - Add the standalone reference modules (Prelude, Reference, ReferenceBridge, OffChainReference, RefReflection). - build.sh now typechecks the tree with Agda before rendering, and runs the Agda<->Typst reference lint (check-refs.sh) and the trust-ledger drift check (check-trust-ledger.sh). - Wire the Agda toolchain (spec-agda) into the spec build and dev shell. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- Add the developer docs page for the Agda formalisation and update the specification docs page and sidebar. - Changelog entry for the spec migration and agreement layer. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
856748e to
4389a7e
Compare
8d384ed to
2c2ec36
Compare
🧱 Stack (split of #2736)
👉 3. typst-agda-spec-3: Add the Agda formalisation of the specification #2786 — Agda formalisation + developer docs + changelog
Merge in order (1→5) into the
typst-agda-stackedintegration branch, then merge that branch intomasteras the final step.Stacked PR 3/5 — splits #2736.
Base:
typst-agda-spec-2· Next:typst-agda-spec-4.Also includes the developer docs page for the Agda formalisation (
docs/dev/agda.md), the specification docs + sidebar updates, and the spec-migration changelog entry (absorbed from the former docs PR #2789).Populate the literate sources with their Agda content and machine-check them as
part of the spec build. This PR is the formalisation half of the migration:
it re-inserts exactly the Agda code blocks that PR 2 held back, so the two PRs
together reproduce the full literate tree.
.lagda.typtree (datum/redeemer types,transition relations, validity bundles, coverage/safety and security theorems
and proofs); they now render in the formalisation appendix.
Prelude,Reference,ReferenceBridge,OffChainReference,RefReflection).build.shnow typechecks the tree with Agda before rendering and runs theAgda↔Typst reference lint (
check-refs.sh) and the trust-ledger drift check(
check-trust-ledger.sh); the Agda toolchain is wired into the build and devshell.
Verified:
nix build .#specruns the full Agda typecheck + lints and renders the61-page PDF; treefmt-clean.
🤖 Generated with Claude Code