Repository navigation
Open
Labels
Description
Seam connections for merged PR #61 (W5.6 the host). PR #61 merged at 40e1fe9 with two own mocks carried, per the organiser ruling of 7 November: an approved PR with a mock of a merged dependency merges, and the swaps land through this issue. The identity mock row of the old table is done: #63 merged on 6 November and the host names the real identity.
| Mock | Real dependency | The connections to make | Window |
|---|---|---|---|
Host.Mock.Core |
#15 W5.2 (merged, PR #64) |
done: PR #80 merged at 22c0679, the mock is gone, the axioms audit is clean | - |
Host.Mock.Negotiate |
#18 W5.5 (merged, PR #40) |
a retype, not a delete: the merged negotiate takes no admit checkpoint and answers the plain pair, and it exports no negotiateStream. The host gates with its own Policy gater before Negotiate.upgrade, and the stream-serving path needs real multistream over the muxed stream on the host side |
00:32 UTC 2026-11-08 (lapsed; the retype is owed now) |
Negotiate/Legacy/ |
the same retype | PR #59 landed this parallel pre-retype upgrader so the host could run before the retype (the tip's host exits at startup against the real upgrader). The retype deletes the subtree and the Negotiate.Legacy imports in Host/Swarm.lean |
with the retype |
The old assumptions row said "upgradeWith carries the post-handshake admit checkpoint that PR #40 must grow". PR #40 grew no such parameter; the assumption is void, and the retype above replaces it.
Definition of done
hackathon26carries noHost/Mock/module.#print axiomsover the package theorems showspropext,Classical.choice, andQuot.soundonly.- The ledger rows for PR feat(host): W5.6, the host with dedup, serving, and shutdown #61 on issue [TRACKING] Machine-Checked Devcon Week: the task tree #25 get struck when the swaps land.
lake build --wfail,lake test,lake test -- +RTS -N1 -RTS, andscripts/lint-imports.shstay green.
Ground rules
- The host author (PR feat(host): W5.6, the host with dedup, serving, and shutdown #61) owes this work; comment
claimto take it if they do not. - Work lands as a follow-up pull request against
hackathon26from the author's fork. This issue closes when the tip is clean of the mocks. - Target the
hackathon26branch. Prose register everywhere: CLAUDE.md, "Writing Style".
Activity
refactor(host): take the keys and the peer id from libp2p/identity
refactor(host): take the keys and the peer id from libp2p/identity
refactor(host): take the seam types from libp2p/core
refactor(protocols): run req/resp over the seam types of libp2p/core
test(host): run the unit 1b legs on the fixed-key Noise value