[IvanAnishchuk]

Summary

The req/resp sim checks now run between two real hosts, on the fixed-key Noise value, yamux, and a test clock. This PR deletes Protocols.Mock.Muxer and Protocols.Mock.HostStream, the two mocks #78 still owes. Closes #78.

This PR stacks on #86, which puts the host on the real negotiate. Until #86 merges, the diff also shows its two commits. Review the three commits after them:

• test(protocols): run the req/resp sim checks between two real hosts, the swap.
• docs(protocols): …, which drops the req/resp sentence that said the host still upgrades through a negotiate mock.
• test(protocols): run the host pair on the fixed-key Noise value and a test clock, which puts Tests/HostPair.lean on the test values of root §3.1.

What changed

Tests:

• Tests/HostPair.lean (new): two hosts over a new sim net, on the test values of root §3.1. Each host takes Noise.fixedKeyProtocol with an Ed25519 identity from one byte, and its ephemeral keys from an Rng seeded from that byte. Both hosts run on one TestClock, which Pair.close closes. The muxer is Mux.yamux. The server listens on /memory/4100, and the client holds a session to it.
• Tests/ReqResp.lean: the sim section takes the pair. openStreamOf maps the host's newStream onto the OpenStream of requestPeer. A host failure that wraps a seam error reaches the requester as that error.
• An id the peer does not serve now fails the open (openFailed). The mock reset the stream. The real host runs multistream-select, which answers na, so the stream never opens for that id.

libp2p/protocols:

• Mock/Muxer.lean and Mock/HostStream.lean are deleted.
• The package ARCHITECTURE drops the mock row and describes the two-host suite. The PLAN milestone lists the four sim checks with the new na answer.

Test plan

• lake build --wfail on Libp2pProtocols, Tests.HostPair, and Tests.ReqResp is green.
• 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: 186 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: test-only change)
• If this touches the go interop path: the interop matrix (PLAN W5.9) is green. (n/a)

Risk / trust footprint

None added or removed. The deleted Mock/HostStream.lean held two partial def loops (readHeader, serveLoop). They go with it.

Notes for reviewers

• Protocols/Mock/Core.lean and Mock/Host.lean stay. Identify and ping type over them, and their swap is [SEAM] W5.7 identify/ping: the mock connections of #45 #55.
• The ledger rows on [TRACKING] Machine-Checked Devcon Week: the task tree #25 for Protocols/Mock/Muxer.lean and Protocols/Mock/HostStream.lean (PR feat(protocols): W6.3, the req/resp framework over the snappy framing format #46) can be struck when this merges.

LICENSE (LGPL version 3)

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