Skip to content

Commit 9b8c98b

Browse files
noonioclaude
noonio
and
claude
committed
Document the Agda formalisation and record the changelog entry
- 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>
1 parent 0707f95 commit 9b8c98b

4 files changed

Lines changed: 149 additions & 1 deletion

File tree

‎CHANGELOG.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,20 @@ compile-time coupling to a single version's scripts [#2740](https://github.com/c
2626
the funds to the prefilled own address, and an invalid amount sent the full
2727
UTxO value).
2828

29+
- The formal specification (`spec/`) was migrated from LaTeX to literate Agda +
30+
Typst: the same sources are type-checked by Agda (definitions, validity
31+
bundles and security proofs are machine-checked, including consistency,
32+
soundness/completeness and the on-chain safety invariants) and rendered to
33+
the PDF by Typst. A decidable core is extracted to Haskell via MAlonzo (the
34+
new `hydra-agda` package) and differentially tested against the real Plutus
35+
validator (`hydra-tx` `HeadValidatorAgreement`) and the real head logic
36+
handlers (`hydra-node` `OffChainAgreementSpec`/`OffChainLeaderSpec`). CI
37+
gates the spec build (`checks.spec`, including reference/diagram and
38+
trust-ledger drift checks) and the extraction freshness
39+
(`checks.hydra-agda-generated`). The spec models the current protocol,
40+
including the commit/decommit output-set hashes bound into the snapshot
41+
multisignature and the canonical CRS datum binding of the fanout paths.
42+
2943
- The head logic now enforces the specification's "no commit and decommit in
3044
flight at once" discipline on the message level: a `ReqSn` carrying both a
3145
deposit and a decommit is rejected (`ReqSnDepositAndDecommit`), and a

‎docs/docs/dev/agda.md‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
# Formal specification in Agda
2+
3+
The Hydra Head protocol specification is written in *literate Agda* rendered by
4+
[Typst](https://typst.app): every definition, validity condition and security
5+
proof shown in the [specification PDF](./specification.md) comes from source
6+
files that Agda type-checks on every build. On top of that, a decidable core of
7+
the spec is extracted to Haskell and *differentially tested* against the real
8+
Plutus validators and the real `hydra-node` head logic. This page is an
9+
orientation: what is proved, what is tested, what is assumed, and where the
10+
machinery lives.
11+
12+
## Why literate Agda + Typst
13+
14+
A specification that lives next to the code but is only prose will drift. Here
15+
the prose, the math and the machine-checked definitions come from one set of
16+
sources ([`spec/src/Hydra/Protocol/`](https://github.com/cardano-scaling/hydra/tree/master/spec/src/Hydra/Protocol)):
17+
`agda Main.lagda.typ` type-checks the whole document and Typst renders the same
18+
files to the PDF. Two kinds of code fences exist: rendered ones (collected into
19+
the PDF's Agda appendix) and typecheck-only ones (imports, proof plumbing). See
20+
[`spec/README.md`](https://github.com/cardano-scaling/hydra/tree/master/spec)
21+
for the authoring details.
22+
23+
## Module map
24+
25+
Three groups of modules, one build:
26+
27+
| Group | Modules | Role |
28+
| --- | --- | --- |
29+
| Rendered (the document) | `Introduction`, `Overview`, `Preliminaries`, `Setup`, `OnChain`, `OnChainCoverage`, `OffChain`, `Security`, `SecurityProofs` | Prose + the machine-checked definitions, validity bundles, invariants and §7 proofs |
30+
| Typecheck-only | `Prelude`, `ReferenceBridge`, `RefReflection` | The abstract trust base and the bridge proofs; verified on every build, never rendered |
31+
| Extractable | `Reference`, `OffChainReference` | Decidable checkers, self-contained over `Agda.Builtin` types so the extracted Haskell stays small |
32+
33+
## The trust story
34+
35+
Three tiers, from strongest to weakest guarantee:
36+
37+
1. **Proved.** The §7 security results (consistency, soundness, completeness,
38+
the reachability invariant, no-settlement-without-unanimity) and the
39+
on-chain coverage/safety theorems (non-stuckness, value conservation,
40+
bounded contest window) are closed Agda proofs over the abstract model.
41+
Multisignature unforgeability is *derived* from per-signature EUF-CMA plus
42+
the aggregation scheme's decomposition, not assumed monolithically.
43+
44+
2. **Assumed.** The model bottoms out in an enumerated trust base: ledger and
45+
crypto primitives (hashing, the multisignature verifier, the `Value`
46+
algebra), the accumulator laws (the KZG construction itself is not
47+
modelled), a small set of on-chain "search" postulates over the opaque
48+
value/key models, and the honest-behaviour premises of the security model.
49+
The PDF appendix section **"What the formalisation assumes"** inventories
50+
all of it — the reading rule is: `postulate` means assumption, everything
51+
else is proved.
52+
53+
3. **Differentially tested.** Where the abstract model meets the real code,
54+
the bridge's trusted base is *fixed and machine-enforced*: exactly 6
55+
injected const-true mocks (crypto/accumulator conjuncts the tests cover
56+
against the real primitives instead) and 7 encoding/faithfulness
57+
postulates, enumerated in
58+
[`spec/check-trust-ledger.sh`](https://github.com/cardano-scaling/hydra/blob/master/spec/check-trust-ledger.sh).
59+
That script fails the spec build if a mock or postulate is added or removed
60+
without updating the ledger — the trusted base cannot grow silently.
61+
62+
The bridge direction is *completeness*: `ReferenceBridge.agda` proves that a
63+
spec-valid transaction makes the extracted checker accept, so a
64+
reference-reject implies a spec-reject. Joined with the agreement tests'
65+
`reference === validator`, a spec-valid transaction is accepted by the real
66+
validator and vice versa — modulo the documented mocks, each of which the
67+
tests exercise with real crypto (Ed25519 signatures, BLS/KZG pairings) in both
68+
accept and reject directions.
69+
70+
## The extraction pipeline
71+
72+
`Reference.agda` and `OffChainReference.agda` are compiled by Agda's MAlonzo
73+
backend into
74+
[`hydra-agda/generated/`](https://github.com/cardano-scaling/hydra/tree/master/hydra-agda),
75+
which is committed. Hand-written shims (`Hydra.Agda.Reference`,
76+
`Hydra.Agda.OffChainReference`) pin the mangled MAlonzo names to stable,
77+
documented Haskell names — a stale pin is a loud compile error. Regeneration
78+
is manual (`hydra-agda/regenerate.sh`); freshness is CI-enforced: the
79+
`hydra-agda-generated` flake check re-extracts hermetically and fails on any
80+
diff against the committed tree.
81+
82+
## The agreement tests
83+
84+
Two layers bind the extracted spec to the real implementation:
85+
86+
- **On-chain** —
87+
[`Hydra.Tx.Contract.HeadValidatorAgreement`](https://github.com/cardano-scaling/hydra/blob/master/hydra-tx/test/Hydra/Tx/Contract/HeadValidatorAgreement.hs)
88+
(hydra-tx) runs the *real* `Head.headValidator` (and the compiled
89+
`deposit.ak` as UPLC) and the extracted reference on the same directly
90+
constructed inputs — no transactions, no mutation corpus — and asserts
91+
`reference === validator` across every transaction family, in both the
92+
accept and reject directions. The crypto the reference mocks is exercised
93+
for real: valid and invalid Ed25519 snapshot signatures (including the
94+
commit/decommit output-set hashes bound into the signed message), BLS/KZG
95+
membership proofs against the canonical CRS, and the canonical-CRS datum
96+
binding (`InvalidCRSDatum`).
97+
- **Off-chain** —
98+
[`Hydra.OffChainAgreementSpec`](https://github.com/cardano-scaling/hydra/blob/master/hydra-node/test/Hydra/OffChainAgreementSpec.hs)
99+
and `Hydra.OffChainLeaderSpec` (hydra-node) bind the extracted §6 handler
100+
decisions (snapshot-signing eligibility, decommit recording, deposit status,
101+
ack counting, contest eligibility, leader election) against the real
102+
`HeadLogic.update` outcomes.
103+
104+
## How do I ...
105+
106+
| Task | What to do |
107+
| --- | --- |
108+
| Build the PDF | `nix build .#spec`, or `./build.sh` inside `nix develop` (output: `spec/_build/hydra-spec.pdf`) |
109+
| Type-check only | `agda src/Hydra/Protocol/Main.lagda.typ` in `spec/` |
110+
| Change a validator condition | Update the section + `*Valid` bundle in `OnChain.lagda.typ`, mirror in `Reference.agda`, prove in `ReferenceBridge.agda`, `regenerate.sh`, extend the shim + `HeadValidatorAgreement` — see the checklist in [`spec/README.md`](https://github.com/cardano-scaling/hydra/tree/master/spec) |
111+
| Change a head-logic handler | Update the §6 arm (+ figure) in `OffChain.lagda.typ`, mirror in `OffChainReference.agda`, bind in the hydra-node agreement tests |
112+
| Change the datum shape | `HeadDatum` in `OnChain.lagda.typ` + `state-fields` in `diagrams.typ`; `check-refs.sh` catches constructor drift |
113+
| Add a mock/postulate to the bridge | The build fails until `check-trust-ledger.sh`'s ledger is updated — that is the point |
114+
115+
CI gates: `checks.spec` (Agda typecheck, reference/diagram lints, trust-ledger
116+
drift check, PDF render) and `checks.hydra-agda-generated` (extraction
117+
freshness). The agreement tests run in the ordinary package test suites.
118+
119+
## Pointers
120+
121+
- The PDF appendix: *"Reading the Agda (for Haskell programmers)"* (a
122+
Haskell-to-Agda glossary) and *"What the formalisation assumes"* (the full
123+
trust-base inventory).
124+
- [`spec/README.md`](https://github.com/cardano-scaling/hydra/tree/master/spec)
125+
— building, authoring, and the keep-in-sync checklist.
126+
- [`spec/check-trust-ledger.sh`](https://github.com/cardano-scaling/hydra/blob/master/spec/check-trust-ledger.sh)
127+
— the enumerated bridge trust ledger.
128+
- The three agreement test modules named above, whose headers document the
129+
per-conjunct coverage.

‎docs/docs/dev/specification.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# Specification
22

3-
The specification is written in Agda and LaTeX and lives in the [`spec/`](https://github.com/cardano-scaling/hydra/tree/master/spec) directory of this repository. You can view the rendered version below or download it for fullscreen viewing [here](/hydra-spec.pdf).
3+
The specification is written in literate Agda and Typst (the same sources are type-checked by Agda and rendered to PDF by Typst) and lives in the [`spec/`](https://github.com/cardano-scaling/hydra/tree/master/spec) directory of this repository. You can view the rendered version below or download it for fullscreen viewing [here](/hydra-spec.pdf). See [Agda formalisation](./agda.md) for how the specification is machine-checked and kept in sync with the implementation.
44

55
import HydraSpecUrl from '@site/static/hydra-spec.pdf';
66

‎docs/sidebars.js‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,11 @@ module.exports = {
7676
id: "dev/specification",
7777
label: "Specification",
7878
},
79+
{
80+
type: "doc",
81+
id: "dev/agda",
82+
label: "Agda formalisation",
83+
},
7984
"dev/protocol",
8085
"dev/commit",
8186
"dev/rollbacks/index",

0 commit comments

Comments
 (0)