Repository navigation
[SEAM] W5.8 cli: connect CliApp.Mock.Stack to the real stack inside #50 #72
Description
Seam connections inside open PR #50 (W5.8 the demo and ping binaries). The PR builds the binaries against one mock, CliApp/Mock/Stack.lean, standing for the whole W5 stack. The mock declares opaque ops with executable failure bodies, and its NEED CHANGES review records which names are false against the current tree (Mock/Stack.lean:220,231, packages/cli/docs/ARCHITECTURE.md:154); the swap must re-check each.
The dependencies behind the stack: #20 W5.7 (PR #45), #11 W5.1 (PR #63 or #44, organiser picks), #15 W5.2 (PR #64), #17 W5.4 (PR #49, draft), #16 W5.3 (PR #67, draft), #19 W5.6 (PR #61). #14 W4.3 merged on 2026-11-06 (PR #62).
Definition of done
CliApp/Mock/Stack.leanis gone; the binaries drive the real packages.- The live loopback demo and the interop gates run for real, per the issue [W5.8] cli: the demo and ping binaries #22 done-list, and the PLAN documents the substitutions no longer needed.
- The ledger rows for PR feat(cli): add the W5.8 demo and ping binaries #50 on issue [TRACKING] Machine-Checked Devcon Week: the task tree #25 land at merge time and get marked done with the swap.
lake build --wfail,lake test,lake test -- +RTS -N1 -RTS, andscripts/lint-imports.shstay green.
Ground rules
- The cli author (PR feat(cli): add the W5.8 demo and ping binaries #50) owes this work; comment
claimto take it if they do not. Work happens on the feat(cli): add the W5.8 demo and ping binaries #50 branch, together with the fixes its NEED CHANGES names (the ownerless stdin reader, the stale prose); the issue closes when the swap lands in the branch. - Target the
hackathon26branch. Prose register everywhere: CLAUDE.md, "Writing Style".
Activity
IvanAnishchuk commentedon Nov 10, 2026
#86 moves the host onto the merged
libp2p/negotiateand deletesNegotiate.Legacy. No existing signature changes. The host adds four names:Libp2p.Host.upgraderuns the upgrade, with the secured checkpoint after the handshake and before the muxer stage.Libp2p.Host.negotiateStreamruns multistream-select on a muxedStream, and hands the bytes after the selection to the handler.UpgradedandAdmissionnow live inLibp2p.Host. No code outside the host named them before.Once #86 merges,
Tests/Host.leanruns real hosts over the sim (unit 1b). A swap of this unit's host mock can build its test hosts the same way.IvanAnishchuk commentedon Nov 10, 2026
#89 moves identify and ping onto the real
libp2p/coreandlibp2p/host, and deletesProtocols/Mock/Core.leanandProtocols/Mock/Host.lean. The swap ofCliApp/Mock/Stack.lean(#50) connects to these shapes:Ping.protocolId,Identify.protocolId, andIdentify.pushIdareLibp2p.Core.ProtocolIdvalues.Ping.pingHandleris aLibp2p.Core.StreamHandler.Identify.respondHandler key addrs protocols agent sprtakes no observed address. Each answer carries theremoteAddrof the stream's connection.Identify.pushHandler h clock timeoutMstakes theLibp2p.Host.Hostwhose peerstore it updates. It checks each push against theremotePeerof the stream's connection.Identify.client s clock timeoutMs expectedandPing.ping s clock payloadkeep their signatures.Tests/Protocols.leanin #89 runs identify and push between two real hosts ofTests/HostPair.lean, the same setup a demo node uses.