Skip to content

typst-agda-spec-4: Add the hydra-agda package (MAlonzo extraction) and CI gate - #2787

Open
noonio wants to merge 1 commit into
typst-agda-spec-3from
typst-agda-spec-4
Open

typst-agda-spec-4: Add the hydra-agda package (MAlonzo extraction) and CI gate#2787
noonio wants to merge 1 commit into
typst-agda-spec-3from
typst-agda-spec-4

Conversation

@noonio

@noonio noonio commented Jul 23, 2026

Copy link
Copy Markdown
Contributor

🧱 Stack (split of #2736)

  1. typst-agda-spec-1: Forbid simultaneous commit and decommit in the head logic #2784 — protocol fix
  2. typst-agda-spec-2: Migrate the specification prose from LaTeX to Typst #2785 — Typst prose migration
  3. typst-agda-spec-3: Add the Agda formalisation of the specification #2786 — Agda formalisation + developer docs + changelog
    👉 4. typst-agda-spec-4: Add the hydra-agda package (MAlonzo extraction) and CI gate #2787 — hydra-agda package + CI
  4. typst-agda-spec-5: Differentially test the node and validator against the Agda reference #2788 — agreement tests

Merge in order (1→5) into the typst-agda-stacked integration branch, then merge that branch into master as the final step.


Stacked PR 4/5 — splits #2736.
Base: typst-agda-spec-3 · Next: typst-agda-spec-5.

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.
  • 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.

Verified: nix build .#checks.x86_64-linux.hydra-agda-generated passes;
cabal build hydra-agda compiles; treefmt-clean.

🤖 Generated with Claude Code

@github-actions

Copy link
Copy Markdown

Transaction cost differences

No cost or size differences found

@github-actions

github-actions Bot commented Jul 23, 2026

Copy link
Copy Markdown

End-to-end benchmark differences

Comparing this PR (new) against master (old). Numbers come from cloud VMs, so changes under 5% are shown as and are likely run-to-run noise rather than a real regression or improvement. 🟢 = improvement, 🔴 = regression; uncolored rows are neutral measures reported for context.

Sustained load (3 nodes, 3x5000 txs)

Metric master PR Δ
End-to-end TPS (tx/s) 659.53 524.54 🔴 -134.99 (-20.5%)
Sustained TPS (tx/s) 1,250.97 1,016.46 🔴 -234.51 (-18.7%)
Backlog drain time (s) 22.30 27.90 🔴 +5.60 (+25.1%)
Snapshots per second (/s) 0.70 0.59 -0.11 (-15.7%)
Avg txs per snapshot 937.50 882.40 -55.10 (-5.9%)
Avg. Confirmation Time (s) 18.351 23.193 🔴 +4.842 (+26.4%)
P50 confirmation (s) 19.433 24.525 🔴 +5.092 (+26.2%)
P95 confirmation (s) 22.408 28.135 🔴 +5.727 (+25.6%)
P99 confirmation (s) 22.548 28.283 🔴 +5.736 (+25.4%)
Tx validation time p50 (s) 7.556 9.449 🔴 +1.893 (+25.1%)
Peak node RSS (MB) 420.20 428.00 ≈ +7.80 (+1.9%)
Invalid txs 0.00 0.00 ≈ +0.00 (n/a%)

Plateau 1000 UTxO (1 node, 4000 txs)

Metric master PR Δ
End-to-end TPS (tx/s) 272.63 234.95 🔴 -37.68 (-13.8%)
Backlog drain time (s) 14.60 16.90 🔴 +2.30 (+15.8%)
Snapshots per second (/s) 0.55 0.47 -0.08 (-14.5%)
Avg txs per snapshot 500.00 500.00 ≈ +0.00 (+0.0%)
Avg. Confirmation Time (s) 9.133 10.612 🔴 +1.479 (+16.2%)
P50 confirmation (s) 9.980 12.663 🔴 +2.683 (+26.9%)
P95 confirmation (s) 14.614 16.918 🔴 +2.303 (+15.8%)
P99 confirmation (s) 14.615 16.919 🔴 +2.304 (+15.8%)
Tx validation time p50 (s) 5.371 5.464 ≈ +0.092 (+1.7%)
Peak node RSS (MB) 358.30 376.90 +18.60 (+5.2%)
Invalid txs 0.00 0.00 ≈ +0.00 (n/a%)

Round-trip latency (3 nodes, closed-loop, 3x250 txs)

Metric master PR Δ
End-to-end TPS (tx/s) 87.58 103.88 🟢 +16.30 (+18.6%)
Sustained TPS (tx/s) 87.19 103.83 🟢 +16.64 (+19.1%)
Backlog drain time (s) 0.00 0.00 ≈ +0.00 (n/a%)
Snapshots per second (/s) 59.20 69.94 +10.74 (+18.1%)
Avg txs per snapshot 1.50 1.50 ≈ +0.00 (+0.0%)
Avg. Confirmation Time (s) 0.034 0.029 🟢 -0.005 (-15.6%)
P50 confirmation (s) 0.024 0.028 🔴 +0.005 (+19.1%)
P95 confirmation (s) 0.094 0.037 🟢 -0.057 (-60.7%)
P99 confirmation (s) 0.147 0.042 🟢 -0.105 (-71.3%)
Tx validation time p50 (s) 0.006 0.007 🔴 +0.001 (+21.7%)
Peak node RSS (MB) 149.10 149.20 ≈ +0.10 (+0.1%)
Invalid txs 0.00 0.00 ≈ +0.00 (n/a%)

@noonio
noonio force-pushed the typst-agda-spec-3 branch from f16c983 to c998d82 Compare July 23, 2026 12:25
@noonio
noonio force-pushed the typst-agda-spec-4 branch from 6c5f1fb to a9793ff Compare July 23, 2026 12:25
@github-actions

github-actions Bot commented Jul 23, 2026

Copy link
Copy Markdown

Transaction costs

Sizes and execution budgets for Hydra protocol transactions. Note that unlisted parameters are currently using arbitrary values and results are not fully deterministic and comparable to previous runs.

Metadata
Generated at 2026-08-07 16:31:16.1473449 UTC
Max. memory units 14000000
Max. CPU units 10000000000
Max. tx size (kB) 16384

Script summary

Name Hash Size (Bytes)
νHead f2dd4ade71e19c2310a86215aa78aea06463aca2d8b818af8dc1b8a4 12805
μHead 4abb8dedbcd6a6f03f4fe227300e2713d73b7680d47baa898b60d27a* 4971
νDeposit c78e8c9205721eb3ef4410f3db9c6169fa6db497c24641d29c20529c 1615
νCRS 09db7ee6cf7a4b358dd5c8a2f19d2c048336ffc5a01ef35a47ca7072 2736
  • The minting policy hash is only usable for comparison. As the script is parameterized, the actual script is unique per head.

Init transaction costs

Parties Tx size % max Mem % max CPU Min fee ₳
1 5473 9.16 3.00 0.49
2 5569 9.82 3.22 0.50
3 5668 10.37 3.39 0.51
5 5865 11.40 3.72 0.53
10 6341 14.16 4.62 0.58
50 10184 35.31 11.22 0.96
100 14982 62.00 19.56 1.45
114 16326 69.49 21.89 1.59

Cost of Increment Transaction

Parties Tx size % max Mem % max CPU Min fee ₳
1 2321 21.15 7.52 0.48
2 2452 21.63 8.33 0.49
3 2583 22.74 9.35 0.52
5 2850 24.97 11.40 0.56
10 3501 30.21 16.40 0.67
50 8745 72.88 56.40 1.53
75 12017 97.82 80.87 2.05

Cost of Decrement Transaction

Parties Tx size % max Mem % max CPU Min fee ₳
1 643 18.46 6.68 0.38
2 773 19.40 7.64 0.40
3 903 20.37 8.62 0.42
5 1167 22.31 10.57 0.46
10 1821 27.21 15.45 0.56
50 7063 67.47 54.72 1.40
75 10338 93.00 79.36 1.93

Close transaction costs

Parties Tx size % max Mem % max CPU Min fee ₳
1 669 17.76 11.66 0.41
2 800 18.74 12.64 0.43
3 927 19.69 13.61 0.45
10 1849 26.57 20.47 0.59
50 7094 67.85 60.11 1.44
75 10366 93.26 84.78 1.97

Contest transaction costs

Parties Tx size % max Mem % max CPU Min fee ₳
1 697 21.48 14.90 0.46
2 832 22.64 15.93 0.48
3 964 23.75 16.95 0.51
5 1225 26.07 19.02 0.55
10 1881 31.85 24.18 0.66
50 7121 79.93 65.84 1.58
66 9222 99.48 82.59 1.96

FanOut transaction costs

Involves spending head output and burning head tokens. Uses ada-only UTXO for better comparability.
Rows first grow the UTxO set at a fixed 10 parties, then show the largest set that still fits per number of parties (burning more participation tokens leaves less room for outputs).

Parties UTxO UTxO (bytes) Tx size % max Mem % max CPU Min fee ₳
10 0 0 5645 23.29 42.87 0.90
10 1 56 5677 25.63 45.39 0.93
10 5 284 5814 35.88 55.71 1.10
10 10 570 5985 49.89 68.99 1.31
10 20 1138 6323 82.42 96.97 1.79
1 20 1137 6043 76.20 95.00 1.72
5 20 1138 6168 78.96 95.88 1.75
10 20 1138 6322 82.42 96.97 1.79
20 20 1136 6630 89.74 99.26 1.88
50 15 854 7394 94.70 91.88 1.90

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.

Total UTxO Distributed UTxO (bytes) Tx size % max Mem % max CPU Min fee ₳
11 10 570 987 34.91 66.33 0.95
25 23 1310 1429 68.24 99.40 1.48
30 23 1305 1424 68.24 99.40 1.48
40 23 1309 1428 68.24 99.40 1.48
50 23 1307 1426 68.24 99.40 1.48
100 23 1309 1428 68.24 99.40 1.48
150 23 1309 1428 68.24 99.40 1.48
200 23 1310 1429 68.24 99.40 1.48
200 23 1311 1430 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.

Total UTxO Distributed UTxO (bytes) Tx size % max Mem % max CPU Min fee ₳
11 10 1190 1686 42.00 68.90 1.06
25 21 1953 2192 76.59 99.12 1.58
30 21 2079 2324 76.56 99.12 1.59
40 21 2415 2676 76.59 99.22 1.60
50 21 2100 2347 76.56 99.12 1.59
100 21 2268 2523 76.59 99.17 1.60
150 21 2205 2457 76.59 99.17 1.59
200 21 2310 2567 76.59 99.22 1.60
200 21 2331 2589 76.56 99.21 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 119 5539 22.10 44.31 0.89
5 465 5800 35.70 55.82 1.10
10 990 6221 53.78 70.57 1.37
10 1030 6260 53.90 70.62 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-08-07 16:32:12.314896942 UTC

Baseline Scenario

Number of nodes 1
Number of txs 300
Avg. Confirmation Time (ms) 195.5
P99 198.0ms
P95 197.8ms
P50 195.8ms
Tx validation time p50 (ms) 125.7
End-to-end TPS 1485.18 tx/s
Backlog drain time (s) 0.2
Snapshots observed 3
Snapshots per second 14.85 /s
Avg txs per snapshot 100.0
Peak node RSS (MB) 143.6
Number of Invalid txs 0
Fanout outputs 2

Three local nodes

Number of nodes 3
Number of txs 900
Avg. Confirmation Time (ms) 966.3
P99 1024.7ms
P95 1023.8ms
P50 986.5ms
Tx validation time p50 (ms) 468.0
End-to-end TPS 870.58 tx/s
Backlog drain time (s) 1.0
Snapshots observed 3
Snapshots per second 2.90 /s
Avg txs per snapshot 300.0
Peak node RSS (MB) 148.1
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-08-07 16:46:29.745379496 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 855.99 n/a 34.3 34.8
Nodes=1, Constant, wait for tx valid 30 0.2 175.82 175.84 5.6 7.4
Nodes=1, Growing, fire and forget 30 0.0 823.68 n/a 35.4 36.1
Nodes=1, Growing, wait for tx valid 30 0.2 136.28 137.88 7.3 11.8
Nodes=1, Mixed, fire and forget 30 0.0 854.48 n/a 34.3 34.8
Nodes=1, Mixed, wait for tx valid 30 0.2 150.16 148.72 6.6 9.3
Nodes=2, Constant, fire and forget 60 0.1 599.89 n/a 98.2 99.6
Nodes=2, Constant, wait for tx valid 60 0.5 123.50 123.12 16.0 21.6
Nodes=2, Growing, fire and forget 60 0.1 762.51 n/a 76.3 77.7
Nodes=2, Growing, wait for tx valid 60 0.7 82.91 83.73 23.9 30.9
Nodes=2, Mixed, fire and forget 60 0.1 754.92 n/a 77.4 78.4
Nodes=2, Mixed, wait for tx valid 60 0.7 89.22 85.19 22.2 31.4
Nodes=3, Constant, fire and forget 90 0.1 673.10 n/a 127.2 133.2
Nodes=3, Constant, wait for tx valid 90 0.9 99.86 102.22 29.5 37.6
Nodes=3, Growing, fire and forget 90 0.2 574.86 n/a 152.3 155.2
Nodes=3, Growing, wait for tx valid 90 1.4 66.59 68.57 43.1 66.1
Nodes=3, Mixed, fire and forget 90 0.2 573.63 n/a 153.5 155.6
Nodes=3, Mixed, wait for tx valid 90 1.1 78.60 77.00 37.4 48.5

Nodes=1, Constant, fire and forget

Number of nodes 1
Number of txs 30
Avg. Confirmation Time (ms) 34.3
P99 34.8ms
P95 34.8ms
P50 34.5ms
Tx validation time p50 (ms) 12.6
End-to-end TPS 855.99 tx/s
Backlog drain time (s) 0.0
Snapshots observed 2
Snapshots per second 57.07 /s
Avg txs per snapshot 15.0
Peak node RSS (MB) 144.8
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.6
P99 10.7ms
P95 7.4ms
P50 5.2ms
Tx validation time p50 (ms) 1.8
End-to-end TPS 175.82 tx/s
Sustained TPS 175.84 tx/s
Backlog drain time (s) 0.0
Snapshots observed 30
Snapshots per second 175.82 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 144.6
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) 35.4
P99 36.2ms
P95 36.1ms
P50 35.6ms
Tx validation time p50 (ms) 18.3
End-to-end TPS 823.68 tx/s
Backlog drain time (s) 0.0
Snapshots observed 2
Snapshots per second 54.91 /s
Avg txs per snapshot 15.0
Peak node RSS (MB) 144.2
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.3
P99 12.0ms
P95 11.8ms
P50 6.7ms
Tx validation time p50 (ms) 1.8
End-to-end TPS 136.28 tx/s
Sustained TPS 137.88 tx/s
Backlog drain time (s) 0.0
Snapshots observed 30
Snapshots per second 136.28 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 145.5
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 34.9ms
P95 34.8ms
P50 34.5ms
Tx validation time p50 (ms) 22.8
End-to-end TPS 854.48 tx/s
Backlog drain time (s) 0.0
Snapshots observed 2
Snapshots per second 56.97 /s
Avg txs per snapshot 15.0
Peak node RSS (MB) 144.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) 6.6
P99 11.0ms
P95 9.3ms
P50 6.2ms
Tx validation time p50 (ms) 1.8
End-to-end TPS 150.16 tx/s
Sustained TPS 148.72 tx/s
Backlog drain time (s) 0.0
Snapshots observed 30
Snapshots per second 150.16 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 144.1
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) 98.2
P99 99.6ms
P95 99.6ms
P50 98.5ms
Tx validation time p50 (ms) 65.1
End-to-end TPS 599.89 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 20.00 /s
Avg txs per snapshot 30.0
Peak node RSS (MB) 145.0
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) 16.0
P99 23.6ms
P95 21.6ms
P50 15.4ms
Tx validation time p50 (ms) 4.5
End-to-end TPS 123.50 tx/s
Sustained TPS 123.12 tx/s
Backlog drain time (s) 0.0
Snapshots observed 60
Snapshots per second 123.50 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 145.3
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) 76.3
P99 78.1ms
P95 77.7ms
P50 76.8ms
Tx validation time p50 (ms) 23.4
End-to-end TPS 762.51 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 25.42 /s
Avg txs per snapshot 30.0
Peak node RSS (MB) 146.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) 23.9
P99 35.8ms
P95 30.9ms
P50 23.1ms
Tx validation time p50 (ms) 6.2
End-to-end TPS 82.91 tx/s
Sustained TPS 83.73 tx/s
Backlog drain time (s) 0.0
Snapshots observed 60
Snapshots per second 82.91 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 146.3
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) 77.4
P99 78.9ms
P95 78.4ms
P50 77.8ms
Tx validation time p50 (ms) 28.8
End-to-end TPS 754.92 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 25.16 /s
Avg txs per snapshot 30.0
Peak node RSS (MB) 145.0
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) 22.2
P99 34.6ms
P95 31.4ms
P50 21.9ms
Tx validation time p50 (ms) 6.9
End-to-end TPS 89.22 tx/s
Sustained TPS 85.19 tx/s
Backlog drain time (s) 0.0
Snapshots observed 60
Snapshots per second 89.22 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 146.5
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) 127.2
P99 133.3ms
P95 133.2ms
P50 126.0ms
Tx validation time p50 (ms) 42.3
End-to-end TPS 673.10 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 14.96 /s
Avg txs per snapshot 45.0
Peak node RSS (MB) 145.0
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) 29.5
P99 41.0ms
P95 37.6ms
P50 29.3ms
Tx validation time p50 (ms) 8.0
End-to-end TPS 99.86 tx/s
Sustained TPS 102.22 tx/s
Backlog drain time (s) 0.0
Snapshots observed 61
Snapshots per second 67.68 /s
Avg txs per snapshot 1.5
Peak node RSS (MB) 144.3
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) 152.3
P99 155.3ms
P95 155.2ms
P50 154.7ms
Tx validation time p50 (ms) 53.4
End-to-end TPS 574.86 tx/s
Backlog drain time (s) 0.2
Snapshots observed 2
Snapshots per second 12.77 /s
Avg txs per snapshot 45.0
Peak node RSS (MB) 145.5
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) 43.1
P99 73.3ms
P95 66.1ms
P50 42.0ms
Tx validation time p50 (ms) 11.6
End-to-end TPS 66.59 tx/s
Sustained TPS 68.57 tx/s
Backlog drain time (s) 0.1
Snapshots observed 64
Snapshots per second 47.35 /s
Avg txs per snapshot 1.4
Peak node RSS (MB) 147.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) 153.5
P99 155.7ms
P95 155.6ms
P50 154.9ms
Tx validation time p50 (ms) 58.5
End-to-end TPS 573.63 tx/s
Backlog drain time (s) 0.2
Snapshots observed 2
Snapshots per second 12.75 /s
Avg txs per snapshot 45.0
Peak node RSS (MB) 145.4
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) 37.4
P99 52.0ms
P95 48.5ms
P50 37.9ms
Tx validation time p50 (ms) 10.2
End-to-end TPS 78.60 tx/s
Sustained TPS 77.00 tx/s
Backlog drain time (s) 0.0
Snapshots observed 62
Snapshots per second 54.14 /s
Avg txs per snapshot 1.5
Peak node RSS (MB) 146.0
Number of Invalid txs 0
Fanout outputs 4

@noonio
noonio force-pushed the typst-agda-spec-3 branch from c998d82 to 9b8c98b Compare July 23, 2026 17:56
@noonio
noonio force-pushed the typst-agda-spec-4 branch from a9793ff to c786336 Compare July 23, 2026 17:56
@noonio
noonio force-pushed the typst-agda-spec-3 branch from 9b8c98b to 0e92b08 Compare July 24, 2026 13:41
@noonio
noonio force-pushed the typst-agda-spec-4 branch from c786336 to 2ffa5de Compare July 24, 2026 13:41
@noonio
noonio force-pushed the typst-agda-spec-3 branch from 0e92b08 to 675ab4a Compare July 27, 2026 07:12
@noonio
noonio force-pushed the typst-agda-spec-4 branch from 2ffa5de to f016acd Compare July 27, 2026 07:12
@noonio
noonio force-pushed the typst-agda-spec-3 branch from 675ab4a to 8d384ed Compare July 27, 2026 07:38
@noonio
noonio force-pushed the typst-agda-spec-4 branch from f016acd to 7803a7d Compare July 27, 2026 07:38
@noonio
noonio force-pushed the typst-agda-spec-3 branch from 8d384ed to 2c2ec36 Compare July 28, 2026 04:41
@noonio
noonio force-pushed the typst-agda-spec-4 branch from 7803a7d to 8b5575a Compare July 28, 2026 04:41
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>
@noonio
noonio force-pushed the typst-agda-spec-3 branch from 2c2ec36 to c9ca2cc Compare August 7, 2026 15:56
@noonio
noonio force-pushed the typst-agda-spec-4 branch from 8b5575a to 9caa9e8 Compare August 7, 2026 15:56
@noonio noonio added this to the Maintenance and DevX milestone Aug 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants