typst-agda-spec-6: Document the Agda formalisation and record the changelog entry - #2789
typst-agda-spec-6: Document the Agda formalisation and record the changelog entry#2789noonio wants to merge 3 commits into
Conversation
Package the decidable core of the Agda formalisation as Haskell so the node/tx test suites can differentially test against it: - hydra-agda: the committed MAlonzo extraction of Reference.agda / OffChainReference.agda plus the hand-written Hydra.Agda.* wrappers, with regenerate.sh to refresh it. - checks.hydra-agda-generated regenerates the extraction hermetically and fails on drift, so a semantic edit to the reference modules cannot leave the committed oracle stale. - Exclude hydra-agda/generated from treefmt (machine-generated) and add the CI job that builds the spec and the extraction check. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add the agreement layer that checks the real implementations against the MAlonzo-extracted Agda reference (hydra-agda): - hydra-tx HeadValidatorAgreement: the real Plutus head validator vs the extracted on-chain reference across every transaction family (accept and reject, including KZG membership). - hydra-node OffChainAgreementSpec/OffChainLeaderSpec: the real head-logic handlers (ack collection, contest eligibility, round-robin leader) vs the extracted off-chain reference. Wires hydra-agda (and mtl) into the two test suites. 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>
Transaction cost differencesNo cost or size differences found |
dae600f to
8b4fa54
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 | 5352 | 8.66 | 2.84 | 0.48 |
| 2 | 5448 | 9.53 | 3.13 | 0.49 |
| 3 | 5543 | 9.65 | 3.15 | 0.49 |
| 5 | 5737 | 10.93 | 3.58 | 0.52 |
| 10 | 6217 | 13.57 | 4.42 | 0.57 |
| 50 | 10060 | 35.07 | 11.17 | 0.96 |
| 100 | 14859 | 61.41 | 19.37 | 1.44 |
| 115 | 16298 | 70.30 | 22.19 | 1.60 |
Cost of Increment Transaction
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 2310 | 19.10 | 6.87 | 0.46 |
| 2 | 2442 | 19.55 | 7.68 | 0.47 |
| 3 | 2574 | 20.46 | 8.63 | 0.49 |
| 5 | 2837 | 22.84 | 10.73 | 0.54 |
| 10 | 3491 | 27.12 | 15.42 | 0.63 |
| 50 | 8732 | 66.76 | 54.49 | 1.47 |
| 75 | 12008 | 91.77 | 79.00 | 1.99 |
Cost of Decrement Transaction
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 633 | 16.44 | 6.04 | 0.35 |
| 2 | 763 | 17.34 | 7.00 | 0.37 |
| 3 | 895 | 18.28 | 7.96 | 0.39 |
| 5 | 1157 | 20.03 | 9.86 | 0.43 |
| 10 | 1813 | 24.62 | 14.65 | 0.53 |
| 50 | 7054 | 62.84 | 53.31 | 1.35 |
| 75 | 10328 | 88.14 | 77.86 | 1.88 |
Close transaction costs
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 656 | 15.60 | 10.45 | 0.38 |
| 2 | 791 | 16.53 | 11.42 | 0.40 |
| 3 | 918 | 17.48 | 12.39 | 0.42 |
| 10 | 1841 | 24.01 | 19.14 | 0.56 |
| 50 | 7085 | 62.47 | 57.96 | 1.38 |
| 75 | 10361 | 86.86 | 82.32 | 1.90 |
Contest transaction costs
| Parties | Tx size | % max Mem | % max CPU | Min fee ₳ |
|---|---|---|---|---|
| 1 | 691 | 18.91 | 13.56 | 0.43 |
| 2 | 823 | 20.02 | 14.58 | 0.45 |
| 3 | 954 | 21.08 | 15.59 | 0.47 |
| 5 | 1217 | 23.33 | 17.63 | 0.52 |
| 10 | 1868 | 28.71 | 22.67 | 0.63 |
| 50 | 7116 | 75.02 | 63.80 | 1.53 |
| 71 | 9860 | 98.20 | 85.08 | 1.99 |
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 | 5530 | 23.24 | 42.86 | 0.89 |
| 10 | 1 | 57 | 5563 | 25.58 | 45.37 | 0.93 |
| 10 | 5 | 284 | 5699 | 35.83 | 55.69 | 1.09 |
| 10 | 10 | 570 | 5869 | 49.84 | 68.98 | 1.31 |
| 10 | 20 | 1138 | 6207 | 82.37 | 96.95 | 1.79 |
| 10 | 20 | 1140 | 6209 | 82.37 | 96.96 | 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 | 570 | 987 | 34.86 | 66.32 | 0.95 |
| 25 | 1305 | 1424 | 68.19 | 99.38 | 1.48 |
| 30 | 1307 | 1422 | 68.19 | 99.38 | 1.48 |
| 40 | 1310 | 1429 | 68.19 | 99.38 | 1.48 |
| 50 | 1310 | 1425 | 68.19 | 99.38 | 1.48 |
| 100 | 1308 | 1427 | 68.19 | 99.38 | 1.48 |
| 150 | 1308 | 1427 | 68.19 | 99.38 | 1.48 |
| 200 | 1311 | 1430 | 68.19 | 99.38 | 1.48 |
| 200 | 1311 | 1430 | 68.19 | 99.38 | 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 | 1000 | 1477 | 41.93 | 68.81 | 1.05 |
| 25 | 2478 | 2742 | 76.54 | 99.21 | 1.60 |
| 30 | 2436 | 2694 | 76.54 | 99.21 | 1.60 |
| 40 | 2142 | 2390 | 76.52 | 99.14 | 1.59 |
| 50 | 2268 | 2519 | 76.54 | 99.16 | 1.59 |
| 100 | 2478 | 2743 | 76.52 | 99.20 | 1.60 |
| 150 | 2520 | 2787 | 76.54 | 99.25 | 1.61 |
| 200 | 2415 | 2677 | 76.52 | 99.20 | 1.60 |
| 200 | 2331 | 2589 | 76.54 | 99.20 | 1.60 |
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 | 100 | 5404 | 21.97 | 44.27 | 0.88 |
| 5 | 590 | 5811 | 35.70 | 55.84 | 1.10 |
| 10 | 1160 | 6276 | 53.90 | 70.65 | 1.37 |
| 10 | 1180 | 6296 | 53.90 | 70.65 | 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-23 11:45:09.621563737 UTC
Baseline Scenario
| Number of nodes | 1 |
|---|---|
| Number of txs | 300 |
| Avg. Confirmation Time (ms) | 416.5 |
| P99 | 425.8ms |
| P95 | 425.7ms |
| P50 | 418.1ms |
| Tx validation time p50 (ms) | 264.4 |
| End-to-end TPS | 699.37 tx/s |
| Backlog drain time (s) | 0.4 |
| Snapshots observed | 4 |
| Snapshots per second | 9.32 /s |
| Avg txs per snapshot | 75.0 |
| Peak node RSS (MB) | 128.8 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Three local nodes
| Number of nodes | 3 |
|---|---|
| Number of txs | 900 |
| Avg. Confirmation Time (ms) | 2527.1 |
| P99 | 2842.8ms |
| P95 | 2841.9ms |
| P50 | 2553.8ms |
| Tx validation time p50 (ms) | 1363.0 |
| End-to-end TPS | 315.64 tx/s |
| Sustained TPS | 1105.43 tx/s |
| Backlog drain time (s) | 2.8 |
| Snapshots observed | 10 |
| Snapshots per second | 3.51 /s |
| Avg txs per snapshot | 90.0 |
| Peak node RSS (MB) | 160.4 |
| 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-23 12:12:54.220561893 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, incremental ops off, fire and forget | 30 | 0.1 | 520.78 | n/a | 56.9 | 57.3 |
| Nodes=1, Constant, incremental ops off, wait for tx valid | 30 | 0.2 | 169.80 | 179.35 | 5.8 | 7.6 |
| Nodes=1, Growing, incremental ops off, fire and forget | 30 | 0.1 | 446.74 | n/a | 65.8 | 66.9 |
| Nodes=1, Growing, incremental ops off, wait for tx valid | 30 | 0.3 | 115.32 | 116.51 | 8.6 | 11.2 |
| Nodes=1, Mixed, incremental ops off, fire and forget | 30 | 0.1 | 448.98 | n/a | 65.7 | 66.5 |
| Nodes=1, Mixed, incremental ops off, wait for tx valid | 30 | 0.2 | 131.10 | 124.06 | 7.6 | 11.3 |
| Nodes=2, Constant, incremental ops off, fire and forget | 60 | 0.1 | 423.22 | n/a | 139.7 | 141.4 |
| Nodes=2, Constant, incremental ops off, wait for tx valid | 60 | 0.5 | 113.38 | 111.67 | 17.5 | 21.7 |
| Nodes=2, Growing, incremental ops off, fire and forget | 60 | 0.2 | 313.40 | n/a | 188.6 | 190.0 |
| Nodes=2, Growing, incremental ops off, wait for tx valid | 60 | 0.9 | 66.43 | 66.72 | 29.7 | 41.7 |
| Nodes=2, Mixed, incremental ops off, fire and forget | 60 | 0.1 | 407.05 | n/a | 145.4 | 147.1 |
| Nodes=2, Mixed, incremental ops off, wait for tx valid | 60 | 0.7 | 87.24 | 83.08 | 22.8 | 30.4 |
| Nodes=3, Constant, incremental ops off, fire and forget | 90 | 0.3 | 359.04 | n/a | 245.5 | 249.6 |
| Nodes=3, Constant, incremental ops off, wait for tx valid | 90 | 0.9 | 101.89 | 101.76 | 29.2 | 37.2 |
| Nodes=3, Growing, incremental ops off, fire and forget | 90 | 0.3 | 273.77 | n/a | 324.4 | 326.3 |
| Nodes=3, Growing, incremental ops off, wait for tx valid | 90 | 1.8 | 50.56 | 52.14 | 55.6 | 88.6 |
| Nodes=3, Mixed, incremental ops off, fire and forget | 90 | 0.3 | 326.78 | n/a | 272.0 | 274.8 |
| Nodes=3, Mixed, incremental ops off, wait for tx valid | 90 | 1.3 | 69.93 | 66.01 | 42.6 | 55.8 |
Nodes=1, Constant, incremental ops off, fire and forget
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 56.9 |
| P99 | 57.4ms |
| P95 | 57.3ms |
| P50 | 57.0ms |
| Tx validation time p50 (ms) | 25.8 |
| End-to-end TPS | 520.78 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 34.72 /s |
| Avg txs per snapshot | 15.0 |
| Peak node RSS (MB) | 157.2 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=1, Constant, incremental ops off, wait for tx valid
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 5.8 |
| P99 | 12.7ms |
| P95 | 7.6ms |
| P50 | 5.3ms |
| Tx validation time p50 (ms) | 1.8 |
| End-to-end TPS | 169.80 tx/s |
| Sustained TPS | 179.35 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 30 |
| Snapshots per second | 169.80 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 159.7 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=1, Growing, incremental ops off, fire and forget
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 65.8 |
| P99 | 66.9ms |
| P95 | 66.9ms |
| P50 | 66.3ms |
| Tx validation time p50 (ms) | 25.2 |
| End-to-end TPS | 446.74 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 29.78 /s |
| Avg txs per snapshot | 15.0 |
| Peak node RSS (MB) | 154.2 |
| Number of Invalid txs | 0 |
| Fanout outputs | 31 |
Nodes=1, Growing, incremental ops off, wait for tx valid
| Number of nodes | 1 |
|---|---|
| Number of txs | 30 |
| Avg. Confirmation Time (ms) | 8.6 |
| P99 | 16.0ms |
| P95 | 11.2ms |
| P50 | 8.4ms |
| Tx validation time p50 (ms) | 2.0 |
| End-to-end TPS | 115.32 tx/s |
| Sustained TPS | 116.51 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 30 |
| Snapshots per second | 115.32 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 158.4 |
| Number of Invalid txs | 0 |
| Fanout outputs | 31 |
Nodes=1, Mixed, incremental ops off, 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) | 65.7 |
| P99 | 66.6ms |
| P95 | 66.5ms |
| P50 | 66.0ms |
| Tx validation time p50 (ms) | 25.7 |
| End-to-end TPS | 448.98 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 29.93 /s |
| Avg txs per snapshot | 15.0 |
| Peak node RSS (MB) | 158.9 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=1, Mixed, incremental ops off, 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.6 |
| P99 | 15.1ms |
| P95 | 11.3ms |
| P50 | 6.8ms |
| Tx validation time p50 (ms) | 1.9 |
| End-to-end TPS | 131.10 tx/s |
| Sustained TPS | 124.06 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 30 |
| Snapshots per second | 131.10 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 160.7 |
| Number of Invalid txs | 0 |
| Fanout outputs | 2 |
Nodes=2, Constant, incremental ops off, fire and forget
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 139.7 |
| P99 | 141.5ms |
| P95 | 141.4ms |
| P50 | 140.0ms |
| Tx validation time p50 (ms) | 63.6 |
| End-to-end TPS | 423.22 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 14.11 /s |
| Avg txs per snapshot | 30.0 |
| Peak node RSS (MB) | 153.0 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=2, Constant, incremental ops off, wait for tx valid
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 17.5 |
| P99 | 33.3ms |
| P95 | 21.7ms |
| P50 | 16.9ms |
| Tx validation time p50 (ms) | 5.7 |
| End-to-end TPS | 113.38 tx/s |
| Sustained TPS | 111.67 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 60 |
| Snapshots per second | 113.38 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 159.1 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=2, Growing, incremental ops off, fire and forget
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 188.6 |
| P99 | 190.7ms |
| P95 | 190.0ms |
| P50 | 189.4ms |
| Tx validation time p50 (ms) | 68.5 |
| End-to-end TPS | 313.40 tx/s |
| Backlog drain time (s) | 0.2 |
| Snapshots observed | 2 |
| Snapshots per second | 10.45 /s |
| Avg txs per snapshot | 30.0 |
| Peak node RSS (MB) | 156.5 |
| Number of Invalid txs | 0 |
| Fanout outputs | 62 |
Nodes=2, Growing, incremental ops off, wait for tx valid
| Number of nodes | 2 |
|---|---|
| Number of txs | 60 |
| Avg. Confirmation Time (ms) | 29.7 |
| P99 | 44.5ms |
| P95 | 41.7ms |
| P50 | 29.7ms |
| Tx validation time p50 (ms) | 7.4 |
| End-to-end TPS | 66.43 tx/s |
| Sustained TPS | 66.72 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 60 |
| Snapshots per second | 66.43 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 155.3 |
| Number of Invalid txs | 0 |
| Fanout outputs | 62 |
Nodes=2, Mixed, incremental ops off, 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) | 145.4 |
| P99 | 147.1ms |
| P95 | 147.1ms |
| P50 | 145.8ms |
| Tx validation time p50 (ms) | 68.5 |
| End-to-end TPS | 407.05 tx/s |
| Backlog drain time (s) | 0.1 |
| Snapshots observed | 2 |
| Snapshots per second | 13.57 /s |
| Avg txs per snapshot | 30.0 |
| Peak node RSS (MB) | 153.2 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=2, Mixed, incremental ops off, 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) | 22.8 |
| P99 | 33.9ms |
| P95 | 30.4ms |
| P50 | 23.3ms |
| Tx validation time p50 (ms) | 7.4 |
| End-to-end TPS | 87.24 tx/s |
| Sustained TPS | 83.08 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 60 |
| Snapshots per second | 87.24 /s |
| Avg txs per snapshot | 1.0 |
| Peak node RSS (MB) | 157.9 |
| Number of Invalid txs | 0 |
| Fanout outputs | 3 |
Nodes=3, Constant, incremental ops off, fire and forget
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 245.5 |
| P99 | 249.7ms |
| P95 | 249.6ms |
| P50 | 246.6ms |
| Tx validation time p50 (ms) | 100.8 |
| End-to-end TPS | 359.04 tx/s |
| Backlog drain time (s) | 0.2 |
| Snapshots observed | 2 |
| Snapshots per second | 7.98 /s |
| Avg txs per snapshot | 45.0 |
| Peak node RSS (MB) | 153.1 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
Nodes=3, Constant, incremental ops off, wait for tx valid
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 29.2 |
| P99 | 42.1ms |
| P95 | 37.2ms |
| P50 | 28.5ms |
| Tx validation time p50 (ms) | 8.3 |
| End-to-end TPS | 101.89 tx/s |
| Sustained TPS | 101.76 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 60 |
| Snapshots per second | 67.93 /s |
| Avg txs per snapshot | 1.5 |
| Peak node RSS (MB) | 157.1 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
Nodes=3, Growing, incremental ops off, fire and forget
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 324.4 |
| P99 | 326.4ms |
| P95 | 326.3ms |
| P50 | 325.4ms |
| Tx validation time p50 (ms) | 107.6 |
| End-to-end TPS | 273.77 tx/s |
| Backlog drain time (s) | 0.3 |
| Snapshots observed | 2 |
| Snapshots per second | 6.08 /s |
| Avg txs per snapshot | 45.0 |
| Peak node RSS (MB) | 157.8 |
| Number of Invalid txs | 0 |
| Fanout outputs | 0 |
Nodes=3, Growing, incremental ops off, wait for tx valid
| Number of nodes | 3 |
|---|---|
| Number of txs | 90 |
| Avg. Confirmation Time (ms) | 55.6 |
| P99 | 103.0ms |
| P95 | 88.6ms |
| P50 | 53.6ms |
| Tx validation time p50 (ms) | 16.4 |
| End-to-end TPS | 50.56 tx/s |
| Sustained TPS | 52.14 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 63 |
| Snapshots per second | 35.40 /s |
| Avg txs per snapshot | 1.4 |
| Peak node RSS (MB) | 159.8 |
| Number of Invalid txs | 0 |
| Fanout outputs | 0 |
Nodes=3, Mixed, incremental ops off, 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) | 272.0 |
| P99 | 275.1ms |
| P95 | 274.8ms |
| P50 | 273.0ms |
| Tx validation time p50 (ms) | 105.2 |
| End-to-end TPS | 326.78 tx/s |
| Backlog drain time (s) | 0.3 |
| Snapshots observed | 2 |
| Snapshots per second | 7.26 /s |
| Avg txs per snapshot | 45.0 |
| Peak node RSS (MB) | 157.2 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
Nodes=3, Mixed, incremental ops off, 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) | 42.6 |
| P99 | 60.3ms |
| P95 | 55.8ms |
| P50 | 44.1ms |
| Tx validation time p50 (ms) | 12.0 |
| End-to-end TPS | 69.93 tx/s |
| Sustained TPS | 66.01 tx/s |
| Backlog drain time (s) | 0.0 |
| Snapshots observed | 61 |
| Snapshots per second | 47.40 /s |
| Avg txs per snapshot | 1.5 |
| Peak node RSS (MB) | 158.9 |
| Number of Invalid txs | 0 |
| Fanout outputs | 4 |
🧱 Stack (split of #2736)
👉 6. typst-agda-spec-6: Document the Agda formalisation and record the changelog entry #2789 — docs + changelog
Merge in order (1→6); each PR targets the previous branch.
Stacked PR 6/6 — splits #2736.
Base:
typst-agda-spec-5.specification docs page and sidebar.
Once this stack is reviewed/merged it supersedes #2736 (which can then be
closed). The tip of this stack equals #2736's branch except that the vendored
spec/typst-packages(~15k lines) is replaced by thetypst.withPackagesapproach (PR 2).
🤖 Generated with Claude Code