[IvanAnishchuk]

Summary

The host now runs on the merged libp2p/negotiate. It builds its upgrade from the package's public stages. The secured checkpoint sits between the handshake and the muxer stage, where the core seam puts it. Stream selection is a host shell over the pure negotiate core. The Negotiate.Legacy copy from PR #59 is gone, and the unit 1b host legs run. Closes #70.

What changed

libp2p/host:

• Upgrade.lean (new): upgrade runs Negotiate.negotiate for security, the handshake, checkIdentity, the host's checkpoint, Negotiate.negotiate for the muxer, and Muxer.open. One withinDeadline covers the whole upgrade, and settleUpgrade maps its answer. Upgraded and Admission live here.
• StreamSelect.lean (new): negotiateStream runs multistream-select on a muxed Stream over initiatorStart, responderStart, and drive. It hands the bytes after the selection to the handler through Stream.prependBytes (§5.6).
• Swarm.lean drops the Negotiate.Legacy import and calls upgrade. A refusal at allowSecured or setPeer closes and joins the secure connection before the muxer stage, and answers gated.
• The package ARCHITECTURE and PLAN drop the section "The mock", add the two module rows, and describe the composed upgrade and the stream shell.

libp2p/negotiate:

• Negotiate/Legacy.lean and Negotiate/Legacy/ are deleted. Nothing imports them now.

Tests:

• Tests/Host.lean runs the six unit 1b legs in place of the skips: the pipeline in both directions, the host's own answers, the policy doubles, the silent peer, the shutdown stages, and the leftover hand-over.
• The legs run on the test values of root §3.1: the sim transport, Noise.fixedKeyProtocol seeded from each host's identity byte, and a TestClock. The host PLAN named the production Noise.securityProtocol as an option for these legs, and now names the test value only.
• A new check sets a gater that refuses only at the secured checkpoint. It covers the outbound and the inbound refusal, with no session and no failure report.
• The silent-peer and shutdown checks read the raw connection to its end. The host's responder writes its multistream header first, as go's listener does.

Test plan

• lake build --wfail is green (286 jobs).
• lake test passes: 27824 passed, 0 failed, 4 skipped. It passes again with LEAN_NUM_THREADS=1.
• Stress: the test binary passes 8 of 8 runs at 4 workers, each under a 600 s timeout.
• The import-rule lint is green: 188 modules, 0 violations.
• A new codec or framing layer comes with its round-trip theorem or property test, and with a test for its length cap. (n/a: no new codec)
• If this touches wire behavior: the captured vectors still pass, and the description names the spec section the change follows. (n/a: the multistream bytes come from the merged negotiate core)
• If this touches the go interop path: the interop matrix (PLAN W5.9) is green. (The matrix run on the real stack lands with [SEAM] W5.9 interop: connect Interop.Mock.Stack and land the green matrix run inside #60 #73.)

Risk / trust footprint

None added or removed. The new modules hold no theorem, no partial def, and no @[extern]. The negotiation loops use repeat, as Negotiate.negotiate does. The dedup theorems in Dedup.lean are unchanged.

Notes for reviewers

• Negotiate.upgradeWith takes no checkpoint, so the host composes the stages itself. The stage order follows the private Negotiate.upgradeCore. Both module docs say that a change to the order in one needs the same change in the other.
• The ledger rows on [TRACKING] Machine-Checked Devcon Week: the task tree #25 for Host.Mock.Negotiate (PR feat(host): W5.6, the host with dedup, serving, and shutdown #61) and Negotiate/Legacy/ (PR feat(protocols): W6.4, gossipsub v1.1 #59) can be struck when this merges.
• Next: [SEAM] W6.3 req/resp: drop the three mocks after PR #46 #78 (the req/resp Mock.Muxer and Mock.HostStream), then [SEAM] W5.9 interop: connect Interop.Mock.Stack and land the green matrix run inside #60 #73.

LICENSE (LGPL version 3)

• I have read and accepted LICENSE (LGPL version 3), NOTICE and CLA in the root of this project.