Repository navigation
Logbook September 2026
Week of Monday 7th — The repository starts from nothing and ends the week with a proved model, a naming registry running on a real ledger and a packaged release. A Lean model of the registry came first, the simulator and documentation followed from it, and the on-chain validators were then written and tied to pinned script identities. The week's last stretch measured coverage of the Lean theorems and made folding permissionless, so the next step is checking the deployed code against the model.
The project opens with an admitted Lean model of the registry and a playable simulation of it (#3). The same day the 41 admitted statements of the model were proved (#13), so the model started as a proved object rather than a sketch. The design is presented through user stories and diagrams, with a gate that fails when a speech companion drifts from its page, and a comparison with MPFS separates what can be reused from what is new. The first release, 0.1.0, is cut.
The naming validators are authored, and an unenforced rule (LC04) is found and fixed while doing it (#55). The datum codec is implemented against the contract's own bytes, the compiled script identities are pinned and enforced, and the applied identities are tied to the pinned unapplied ones. The canonical initialization is executed on a real ledger, and the validators are observed refusing forged and tampered transactions. The naming lifecycle (maintenance, recovery, retirement, consumer binding) is modelled, and a single command narrates the whole journey, verifying absence, liveness and a false claim. The imported MPFS trees are adapted to their new locations and their builds reproduced. Releases 0.2.0 and 0.3.0 follow.
Maintenance, cancellation, recovery with the committed next key, and retirement by controller or by registration quorum into completion-only custody are all executed on a real ledger, as are the seven wrong canonical initializations. The Haskell serialization and transaction-construction boundary is executed too. A new gate measures how much of the Lean theorem set is covered and refuses to let it regress (#83), the repository constitution establishes Lean as the authority, and the canonical registry identity is authenticated together with the rival it cannot refuse. The on-chain work is packaged as a retrievable release.
Folding becomes permissionless and retraction insert-only (#85). Conformance rows for generic consumers are executed, the Lean/acceptance page becomes readable, teardown is made failure-safe, and instruments are added to locate where the Fork proof diverges.
The connected journey of claiming a name, recovering it and retiring it permanently is released (#90) on top of a real representative fold. Most of the day goes into conformance evidence: complete receipts, held observations bound to a candidate, and a reviewed coverage baseline of 196 obligations.
Week of Monday 14th — The registry gets its own identity and a persistent deployment on a public network. Onboarding for outside integrators, a deployment manifest with a verifier and the first preprod run are the practical result; most remaining work was bug fixing found by running against a real node, and writing the record of what was built in a hurry. Next the model is reshaped around a single registry mode.
The registry is renamed, since MPFS is a different product (#100), and the vendored MPF patch is replaced by upstream v2.1.0. A persistent deployment is added with a manifest, a verifier and a deploy command (#106), along with an external-node mode, a joiner wallet and an onboarding runbook. Representative names are derived from spelling, public naming lifecycles are funded from live protocol parameters, and release archives replay without a git checkout. Several releases (0.4.1 to 0.6.0) ship in the day.
The preprod deployment is recorded with its verifier output and journeys (#144). Running against the live network surfaced a set of fixes: pending requests are classified by phase before resuming, confirmation polling is bounded by the validity window, deploy window parameters are corrected, and the shape of naming record assets is preserved. Retroactive records are written for the earlier fast-moving changes.
The day is spent on the plan for a Lean model in registry mode and the on-chain cage that will replace the consumer script, with the mandate recompiled into two slices and the failing proof for the first slice written.
The registry model in registry mode lands, with naming as its first instance (#161). The CI rename checks are extended to Lean and HTML inputs.
The on-chain cage in registry mode replaces the consumer script, and naming's policies follow (#164). Journey and end-to-end rows are bound to real registry edges, and retirement request completion is split in the model (#176).
The insertActive conformance row is executed on the open registry (#185) and the control for renaming the registry is repaired on main.
The request now carries an edge tag and no tip, and the old operation encoding is removed (#189); both codecs were folded side by side first so the change could be shown to preserve behavior. The updateTerminal transaction row is modelled (#186).
Week of Monday 21st — The conformance suite becomes the product's public evidence: each test reads as a Lean theorem, clause and example, and one generic driver and one generic live interpreter run every scenario against the model. The week also found and closed gaps in what tests could miss, and ends with deposit handling made explicit for every exit.
Conformance tests are restructured to read as a Lean theorem, a clause and an example (#204), and the constitution now states that the suite is the product's public evidence (#216). One boot-and-fold driver replaces the per-harness copies, the Aiken behavior suites are strengthened and reorganized, the insert-absent custody transaction is bound in Lean, and registration and retirement stories run against Lean on a real devnet (#217). Release 0.8.0 is prepared.
A single generic Lean model driver runs the conformance scenarios (#226), and every declared registration observation is compared with Lean (#227). Absent custody datums are corrected to be refund-only.
One generic live interpreter over the model's seven edges is delivered (#234). Devnet submissions and reads are confirmed through the chain-sync UTxO indexer, which speeds the suites up considerably. The fold's required signers are compared with the submitted transaction, a Terminal read is booked without an approval, and deleting a key now removes it from the model's registry. An active registration can be retired with a transaction the node accepts.
The model states every exit's obligations and proves where deposits go (#259). Code follows: the deposit of every non-delivering fold is returned and settled once per payee (#284), and a retracted request returns everything it holds to its owner (#285). A live fold now declares what it measures and says why the node refused it. The conformance runner is split into modules by responsibility, and dated demo plays and a model asciicast for the first registry demo are written.
Conformance compares every exit's payments with the model (#286). The model states which pending requests their owner can retract and when, and the chain is compared against it (#289). Off-chain and end-to-end tests now fail on missing execution or wrong effects instead of passing silently (#219).
A retraction outside its window is refused by name instead of crashing (#292). Builder, blueprint and node responsibilities are separated without behavior change.
Registry fold responsibilities, wire types and codecs, and the deployment manifest, mirror and attachment code are each moved to their own owners (#294, #295, #296).
Week of Monday 28th — A structural clean-up week: command entry points are made small, every source falls under lint and format policy, and Aiken documentation is published. In parallel a new kind of datum, the protected open datum, goes from model to validator to a lifecycle run through the ordinary command line. The first preprod demonstration of one registry and one key follows.
Every source is inventoried with its lint and format policy, and the checks are enforced across all repository code, including the house Fourmolu configuration for Haskell (#311, #307). Validator helpers are extracted, the Aiken reference is published and the documentation aligned, and the protected open-datum application is modelled (#312).
The protected open-datum validator and envelope codec are added (#316). Submission and confirmation waits are bounded, outputs are described only when they exist with their datum forms observed, and a chosen boot seed is preserved during script publication.
Open-datum bookings, updates and protected releases are built (#317), and the whole protected lifecycle runs through the ordinary command line (#319). A test shows that the fold budget regression check can fail in CI.