Skip to content

typst-agda-spec-2: Migrate the specification prose from LaTeX to Typst - #2785

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

typst-agda-spec-2: Migrate the specification prose from LaTeX to Typst#2785
noonio wants to merge 1 commit into
typst-agda-spec-1from
typst-agda-spec-2

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
  2. typst-agda-spec-3: Add the Agda formalisation of the specification #2786 — Agda formalisation + developer docs + changelog
  3. 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 2/5 — splits #2736.
Base: typst-agda-spec-1 · Next: typst-agda-spec-3.

Replace the LaTeX/TikZ/SVG spec sources with a literate-Typst tree rendered by
Typst. Prose only here — the Agda code blocks and the Agda typecheck stage
are added in PR 3, so this PR reviews as a document migration with no Agda.

  • Prose, notation macros, and native cetz/fletcher diagrams replace the .tex
    sources, TikZ/SVG figures, and the stripped JuliaMono fonts.
  • build.sh renders the .lagda.typ tree with Typst (+ tooltip postprocess);
    the Shakefile/LaTeX toolchain is removed.
  • The @preview diagram packages (cetz, fletcher, oxifmt) are supplied at
    pinned versions from nixpkgs via typst.withPackages
    (TYPST_PACKAGE_CACHE_PATH), so the build stays hermetic without vendoring
    ~15k lines
    into the repo (a deliberate change from Revise spec to be in Typst + Add some agda #2736, which vendored
    spec/typst-packages).

The formalisation appendix is intentionally empty until PR 3.

Verified: nix build .#spec renders the 55-page PDF; 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) 495.39 588.13 🟢 +92.74 (+18.7%)
Sustained TPS (tx/s) 1,049.44 1,284.62 🟢 +235.18 (+22.4%)
Backlog drain time (s) 29.40 24.80 🟢 -4.60 (-15.6%)
Snapshots per second (/s) 0.56 0.67 +0.11 (+19.6%)
Avg txs per snapshot 882.40 882.40 ≈ +0.00 (+0.0%)
Avg. Confirmation Time (s) 24.707 21.101 🟢 -3.606 (-14.6%)
P50 confirmation (s) 25.961 22.014 🟢 -3.947 (-15.2%)
P95 confirmation (s) 29.463 25.017 🟢 -4.447 (-15.1%)
P99 confirmation (s) 29.549 25.110 🟢 -4.439 (-15.0%)
Tx validation time p50 (s) 9.186 10.196 🔴 +1.010 (+11.0%)
Peak node RSS (MB) 419.50 425.40 ≈ +5.90 (+1.4%)
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) 237.13 265.38 🟢 +28.25 (+11.9%)
Backlog drain time (s) 16.80 14.80 🟢 -2.00 (-11.9%)
Snapshots per second (/s) 0.47 0.46 ≈ -0.01 (-2.1%)
Avg txs per snapshot 500.00 571.40 +71.40 (+14.3%)
Avg. Confirmation Time (s) 10.900 9.942 🟢 -0.958 (-8.8%)
P50 confirmation (s) 9.486 11.393 🔴 +1.907 (+20.1%)
P95 confirmation (s) 16.685 14.845 🟢 -1.840 (-11.0%)
P99 confirmation (s) 16.687 14.846 🟢 -1.842 (-11.0%)
Tx validation time p50 (s) 5.270 4.696 🟢 -0.575 (-10.9%)
Peak node RSS (MB) 394.30 379.60 ≈ -14.70 (-3.7%)
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) 99.51 101.92 ≈ +2.41 (+2.4%)
Sustained TPS (tx/s) 99.07 100.12 ≈ +1.05 (+1.1%)
Backlog drain time (s) 0.00 0.00 ≈ +0.00 (n/a%)
Snapshots per second (/s) 67.00 69.44 ≈ +2.44 (+3.6%)
Avg txs per snapshot 1.50 1.50 ≈ +0.00 (+0.0%)
Avg. Confirmation Time (s) 0.030 0.029 ≈ -0.001 (-3.0%)
P50 confirmation (s) 0.029 0.027 🟢 -0.002 (-8.0%)
P95 confirmation (s) 0.040 0.044 🔴 +0.004 (+10.6%)
P99 confirmation (s) 0.048 0.088 🔴 +0.040 (+84.1%)
Tx validation time p50 (s) 0.008 0.006 🟢 -0.002 (-19.0%)
Peak node RSS (MB) 151.40 150.10 ≈ -1.30 (-0.9%)
Invalid txs 0.00 0.00 ≈ +0.00 (n/a%)

@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-07-28 04:48:28.343225101 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 5475 9.32 3.06 0.49
2 5571 9.86 3.23 0.50
3 5668 10.15 3.32 0.51
5 5860 11.36 3.71 0.53
10 6341 14.02 4.57 0.58
50 10182 35.49 11.28 0.97
100 14980 62.13 19.60 1.45
114 16324 69.73 21.98 1.59

Cost of Increment Transaction

Parties Tx size % max Mem % max CPU Min fee ₳
1 2321 20.59 7.33 0.47
2 2452 21.63 8.33 0.49
3 2586 22.64 9.31 0.51
5 2850 24.69 11.30 0.56
10 3501 29.93 16.31 0.66
50 8740 72.31 56.23 1.52
75 12021 97.78 80.85 2.05

Cost of Decrement Transaction

Parties Tx size % max Mem % max CPU Min fee ₳
1 646 18.46 6.68 0.38
2 772 19.42 7.65 0.40
3 904 20.35 8.61 0.42
5 1171 22.30 10.56 0.46
10 1822 27.16 15.44 0.56
50 7063 67.80 54.81 1.40
75 10338 93.17 79.40 1.93

Close transaction costs

Parties Tx size % max Mem % max CPU Min fee ₳
2 800 18.76 12.65 0.43
3 932 19.74 13.63 0.45
10 1849 26.44 20.44 0.59
50 7090 67.47 60.01 1.44
75 10365 93.44 84.83 1.97

Contest transaction costs

Parties Tx size % max Mem % max CPU Min fee ₳
1 701 21.48 14.90 0.46
2 827 22.62 15.93 0.48
3 964 23.81 16.97 0.51
5 1225 26.07 19.02 0.55
10 1880 31.85 24.18 0.66
50 7118 79.67 65.77 1.58
66 9209 98.78 82.40 1.95

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 5644 23.29 42.87 0.90
10 1 57 5678 25.63 45.39 0.93
10 5 285 5814 35.88 55.71 1.10
10 10 568 5983 49.89 68.99 1.31
10 20 1137 6321 82.42 96.97 1.79
10 20 1140 6324 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 570 987 34.91 66.33 0.95
25 1311 1430 68.24 99.40 1.48
30 1309 1428 68.24 99.40 1.48
40 1307 1426 68.24 99.40 1.48
50 1310 1429 68.24 99.40 1.48
100 1307 1426 68.24 99.40 1.48
150 1310 1429 68.24 99.40 1.48
200 1309 1428 68.24 99.40 1.48
200 1309 1428 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 2247 2500 76.59 99.17 1.59
30 2583 2852 76.56 99.27 1.61
40 2478 2742 76.59 99.22 1.61
50 2142 2391 76.56 99.16 1.59
100 2562 2831 76.59 99.27 1.61
150 2310 2567 76.56 99.21 1.60
200 2079 2325 76.59 99.12 1.59
200 2163 2413 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 5527 22.10 44.31 0.89
5 535 5870 35.70 55.83 1.10
10 1230 6460 53.78 70.64 1.38
10 1200 6430 53.90 70.67 1.38

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:52.309071617 UTC

Baseline Scenario

Number of nodes 1
Number of txs 300
Avg. Confirmation Time (ms) 204.3
P99 209.0ms
P95 208.5ms
P50 204.7ms
Tx validation time p50 (ms) 122.7
End-to-end TPS 1399.62 tx/s
Backlog drain time (s) 0.2
Snapshots observed 3
Snapshots per second 14.00 /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) 980.1
P99 1047.2ms
P95 1046.3ms
P50 996.3ms
Tx validation time p50 (ms) 495.7
End-to-end TPS 854.91 tx/s
Backlog drain time (s) 1.0
Snapshots observed 3
Snapshots per second 2.85 /s
Avg txs per snapshot 300.0
Peak node RSS (MB) 147.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-28 05:06:46.739009398 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 1194.49 n/a 24.3 24.8
Nodes=1, Constant, wait for tx valid 30 0.2 182.44 184.17 5.4 6.4
Nodes=1, Growing, fire and forget 30 0.0 955.19 n/a 30.4 31.1
Nodes=1, Growing, wait for tx valid 30 0.2 127.40 125.75 7.8 11.3
Nodes=1, Mixed, fire and forget 30 0.0 977.42 n/a 29.9 30.4
Nodes=1, Mixed, wait for tx valid 30 0.2 132.01 134.08 7.5 11.0
Nodes=2, Constant, fire and forget 60 0.1 874.06 n/a 66.9 67.6
Nodes=2, Constant, wait for tx valid 60 0.5 124.15 124.40 15.9 21.2
Nodes=2, Growing, fire and forget 60 0.1 670.04 n/a 87.3 89.0
Nodes=2, Growing, wait for tx valid 60 0.7 85.69 85.85 23.0 31.3
Nodes=2, Mixed, fire and forget 60 0.1 756.90 n/a 76.8 78.9
Nodes=2, Mixed, wait for tx valid 60 0.7 89.58 87.12 22.1 27.2
Nodes=3, Constant, fire and forget 90 0.1 721.90 n/a 121.8 124.4
Nodes=3, Constant, wait for tx valid 90 0.9 98.53 99.50 30.1 38.9
Nodes=3, Growing, fire and forget 90 0.2 524.28 n/a 166.3 171.3
Nodes=3, Growing, wait for tx valid 90 1.3 68.79 68.60 42.8 54.7
Nodes=3, Mixed, fire and forget 90 0.2 507.81 n/a 172.7 176.9
Nodes=3, Mixed, wait for tx valid 90 1.2 76.29 73.64 38.7 50.2

Nodes=1, Constant, fire and forget

Number of nodes 1
Number of txs 30
Avg. Confirmation Time (ms) 24.3
P99 24.9ms
P95 24.8ms
P50 24.5ms
Tx validation time p50 (ms) 9.4
End-to-end TPS 1194.49 tx/s
Backlog drain time (s) 0.0
Snapshots observed 2
Snapshots per second 79.63 /s
Avg txs per snapshot 15.0
Peak node RSS (MB) 143.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.4
P99 6.9ms
P95 6.4ms
P50 5.3ms
Tx validation time p50 (ms) 1.9
End-to-end TPS 182.44 tx/s
Sustained TPS 184.17 tx/s
Backlog drain time (s) 0.0
Snapshots observed 30
Snapshots per second 182.44 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 143.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) 30.4
P99 31.2ms
P95 31.1ms
P50 30.7ms
Tx validation time p50 (ms) 11.5
End-to-end TPS 955.19 tx/s
Backlog drain time (s) 0.0
Snapshots observed 2
Snapshots per second 63.68 /s
Avg txs per snapshot 15.0
Peak node RSS (MB) 145.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.8
P99 12.1ms
P95 11.3ms
P50 7.1ms
Tx validation time p50 (ms) 2.1
End-to-end TPS 127.40 tx/s
Sustained TPS 125.75 tx/s
Backlog drain time (s) 0.0
Snapshots observed 30
Snapshots per second 127.40 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 145.7
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) 29.9
P99 30.5ms
P95 30.4ms
P50 30.1ms
Tx validation time p50 (ms) 12.7
End-to-end TPS 977.42 tx/s
Backlog drain time (s) 0.0
Snapshots observed 2
Snapshots per second 65.16 /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) 7.5
P99 11.4ms
P95 11.0ms
P50 7.0ms
Tx validation time p50 (ms) 2.1
End-to-end TPS 132.01 tx/s
Sustained TPS 134.08 tx/s
Backlog drain time (s) 0.0
Snapshots observed 30
Snapshots per second 132.01 /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) 66.9
P99 67.7ms
P95 67.6ms
P50 67.1ms
Tx validation time p50 (ms) 23.1
End-to-end TPS 874.06 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 29.14 /s
Avg txs per snapshot 30.0
Peak node RSS (MB) 144.2
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.9
P99 21.8ms
P95 21.2ms
P50 15.5ms
Tx validation time p50 (ms) 4.9
End-to-end TPS 124.15 tx/s
Sustained TPS 124.40 tx/s
Backlog drain time (s) 0.0
Snapshots observed 60
Snapshots per second 124.15 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 144.4
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) 87.3
P99 89.1ms
P95 89.0ms
P50 87.8ms
Tx validation time p50 (ms) 25.3
End-to-end TPS 670.04 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 22.33 /s
Avg txs per snapshot 30.0
Peak node RSS (MB) 144.8
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.0
P99 32.9ms
P95 31.3ms
P50 23.3ms
Tx validation time p50 (ms) 6.7
End-to-end TPS 85.69 tx/s
Sustained TPS 85.85 tx/s
Backlog drain time (s) 0.0
Snapshots observed 60
Snapshots per second 85.69 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 145.8
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.8
P99 79.0ms
P95 78.9ms
P50 77.3ms
Tx validation time p50 (ms) 28.3
End-to-end TPS 756.90 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 25.23 /s
Avg txs per snapshot 30.0
Peak node RSS (MB) 144.9
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.1
P99 29.8ms
P95 27.2ms
P50 22.3ms
Tx validation time p50 (ms) 6.2
End-to-end TPS 89.58 tx/s
Sustained TPS 87.12 tx/s
Backlog drain time (s) 0.0
Snapshots observed 60
Snapshots per second 89.58 /s
Avg txs per snapshot 1.0
Peak node RSS (MB) 145.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) 121.8
P99 124.5ms
P95 124.4ms
P50 122.8ms
Tx validation time p50 (ms) 55.9
End-to-end TPS 721.90 tx/s
Backlog drain time (s) 0.1
Snapshots observed 2
Snapshots per second 16.04 /s
Avg txs per snapshot 45.0
Peak node RSS (MB) 144.9
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) 30.1
P99 42.2ms
P95 38.9ms
P50 29.4ms
Tx validation time p50 (ms) 8.1
End-to-end TPS 98.53 tx/s
Sustained TPS 99.50 tx/s
Backlog drain time (s) 0.0
Snapshots observed 60
Snapshots per second 65.69 /s
Avg txs per snapshot 1.5
Peak node RSS (MB) 144.6
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) 166.3
P99 171.4ms
P95 171.3ms
P50 166.7ms
Tx validation time p50 (ms) 51.2
End-to-end TPS 524.28 tx/s
Backlog drain time (s) 0.2
Snapshots observed 2
Snapshots per second 11.65 /s
Avg txs per snapshot 45.0
Peak node RSS (MB) 146.6
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) 42.8
P99 66.5ms
P95 54.7ms
P50 42.6ms
Tx validation time p50 (ms) 10.9
End-to-end TPS 68.79 tx/s
Sustained TPS 68.60 tx/s
Backlog drain time (s) 0.0
Snapshots observed 62
Snapshots per second 47.39 /s
Avg txs per snapshot 1.5
Peak node RSS (MB) 147.1
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) 172.7
P99 177.0ms
P95 176.9ms
P50 174.4ms
Tx validation time p50 (ms) 46.8
End-to-end TPS 507.81 tx/s
Backlog drain time (s) 0.2
Snapshots observed 2
Snapshots per second 11.28 /s
Avg txs per snapshot 45.0
Peak node RSS (MB) 145.0
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) 38.7
P99 63.8ms
P95 50.2ms
P50 37.4ms
Tx validation time p50 (ms) 10.0
End-to-end TPS 76.29 tx/s
Sustained TPS 73.64 tx/s
Backlog drain time (s) 0.0
Snapshots observed 62
Snapshots per second 52.55 /s
Avg txs per snapshot 1.5
Peak node RSS (MB) 146.4
Number of Invalid txs 0
Fanout outputs 4

@noonio
noonio force-pushed the typst-agda-spec-1 branch from 4b3951d to 6f9eb07 Compare July 23, 2026 12:25
@noonio
noonio force-pushed the typst-agda-spec-2 branch from 82c7343 to 5e520d5 Compare July 23, 2026 12:25
@noonio
noonio force-pushed the typst-agda-spec-1 branch from 6f9eb07 to 90ab7a0 Compare July 23, 2026 17:55
@noonio
noonio force-pushed the typst-agda-spec-2 branch from 5e520d5 to 611c1f0 Compare July 23, 2026 17:55
@noonio
noonio force-pushed the typst-agda-spec-1 branch from 90ab7a0 to 6011c61 Compare July 24, 2026 13:41
@noonio
noonio force-pushed the typst-agda-spec-2 branch from 611c1f0 to f1d7b41 Compare July 24, 2026 13:41
@noonio
noonio force-pushed the typst-agda-spec-1 branch from 6011c61 to a791faf Compare July 27, 2026 07:12
@noonio
noonio force-pushed the typst-agda-spec-2 branch from f1d7b41 to ca4bf10 Compare July 27, 2026 07:12
@noonio
noonio force-pushed the typst-agda-spec-1 branch from a791faf to f669cfd Compare July 27, 2026 07:38
@noonio
noonio force-pushed the typst-agda-spec-2 branch from ca4bf10 to 856748e Compare July 27, 2026 07:38
Replace the LaTeX/TikZ/SVG spec sources with a literate-Typst tree
rendered by Typst:

- Prose, notation macros, and native cetz/fletcher diagrams replace the
  .tex sources, TikZ/SVG figures, and the stripped JuliaMono fonts.
- build.sh renders the .lagda.typ tree with Typst (+ the notation-tooltip
  postprocess); the Shakefile/LaTeX toolchain is removed.
- The @Preview diagram packages (cetz, fletcher, oxifmt) are supplied at
  pinned versions from nixpkgs via `typst.withPackages`
  (TYPST_PACKAGE_CACHE_PATH), keeping the build hermetic without vendoring
  them into the repo.
- Dev shell and `just spec` use the same wrapped typst.

The literate sources carry only prose here; the Agda code blocks, the
standalone reference modules, and the Agda typecheck/lint stage are added
in the following change, so the formalisation appendix is empty for now.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@noonio
noonio force-pushed the typst-agda-spec-1 branch from f669cfd to eb19491 Compare July 28, 2026 04:41
@noonio
noonio force-pushed the typst-agda-spec-2 branch from 856748e to 4389a7e Compare July 28, 2026 04:41
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.

1 participant