[IvanAnishchuk]

Summary

PR #46 merged with three own mocks. This PR moves req/resp off the first one, Protocols.Mock.Core, now that W5.2 merged in #64. It retypes the other two, the muxer and host-stream test values, onto the real core seams. Neither can go yet: the W5.4 muxer values still type over Mux.Mock.Core (issue #77), and the host still upgrades through its negotiate mock (#70, PR #80). Part of #78.

What changed

libp2p/protocols:

• ReqResp/Payload.lean: Error.openFailed carries a Libp2p.Core.Error, and Method.id is a Libp2p.Core.ProtocolId.
• ReqResp/Limiter.lean keys its table by Libp2p.Core.ProtocolId.
• ReqResp/Exchange.lean: OpenStream, mapError, and handler name Libp2p.Core. Inside ReqResp a bare Core is the reader core, so the seam types keep the full prefix, and a comment says so.
• Constants.lean: reqRespId answers a Libp2p.Core.ProtocolId. The identify and ping ids stay on the mock for [SEAM] W5.7 identify/ping: the mock connections of #45 #55.
• StreamError.lean (new) holds mapStreamError over the real Core.Error. Protocols.Mock.Core keeps its copy for identify and ping; [SEAM] W5.7 identify/ping: the mock connections of #45 #55 deletes it with the module.
• Mock/Muxer.lean drops its copies of Role, MuxSession, and Muxer, and muxer is a value of the real seam. openStream takes the protocol id and leaves it unread, as yamux does, and join replaces done.
• Mock/HostStream.lean takes ProtocolId, StreamContext, StreamHandler, and MuxSession from libp2p/core.
• The package ARCHITECTURE splits the mock row, adds the StreamError row, and says what each remaining mock waits on. The sentence that the host lists no outbound call is gone: the host names newStream.

Tests:

• Tests/ReqResp.lean imports Mock.Muxer directly, since Mock.HostStream no longer imports it.

Test plan

• lake build --wfail is green (257 jobs).
• lake test passes: 27169 passed, 0 failed, 10 skipped. It passes again with LEAN_NUM_THREADS=1.
• Stress: the test binary passes 10 of 10 runs at 4 workers, each under a 300 s timeout.
• The import-rule lint is green: 164 modules, 0 violations.

Risk / trust footprint

None added or removed. #print axioms over the req/resp theorems shows propext, Classical.choice, and Quot.sound at most:

Crc32c.crc32cNil                    [propext]
Crc32c.tableSize                    [propext, Quot.sound]
SnappyFrame.Kind.ofCode?_toCode     [propext, Quot.sound]
SnappyFrame.Kind.toCodeLt           [propext, Quot.sound]
SnappyFrame.Kind.toCodeOfCode?      [propext]
SnappyFrame.leOfLength              [propext, Quot.sound]
SnappyFrame.decodeEncodeAppend      [propext, Quot.sound]
Table.countSet                      [propext]
Table.takeBounded                   [propext, Quot.sound]
Table.takeTrue                      [propext]
Core.endedRefusesBytes              [propext, Quot.sound]
Core.eofBetweenChunks               [propext, Quot.sound]
Core.eofInsidePayload               [propext, Quot.sound]
Result.ofCode?_toCode               [propext, Quot.sound]
Result.ofCode?IsSome                [propext, Classical.choice, Quot.sound]
lengthGroupsEncode                  [propext, Quot.sound]
decodeLengthEncode                  [propext, Quot.sound]

Notes for reviewers

• The Protocols.Mock.Core row for PR feat(protocols): W6.3, the req/resp framework over the snappy framing format #46 on [TRACKING] Machine-Checked Devcon Week: the task tree #25 is done for req/resp. The module stays for the PR feat(protocols): W5.7, identify and ping #45 row ([SEAM] W5.7 identify/ping: the mock connections of #45 #55).
• Two copies of the stream error map live side by side until [SEAM] W5.7 identify/ping: the mock connections of #45 #55 lands. The swap there deletes the mock copy, and identify and ping import StreamError.

LICENSE (LGPL version 3)

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

[leolara]

Reviewed at f0d269e, one nit commit over the rebased unit. The branch sat 17 commits behind the tip (fd70eeb to 22c0679), so I rebased onto origin/hackathon26. The rebase is clean: no conflicts, the unit commit re-lands one to one, and no merged commit appears twice. Overage note, one line: the core-mock window closed 19:22 UTC 7 November and the swap commit is dated 8 November 06:43 UTC, about 11 hours past it.

The muxer-mock finding applies. The branch started while issue #77 was open, and it retypes Mock/Muxer.lean over the real core seams as an intermediate state. PR #84 landed the mux seam swap while this branch ran, so the intermediate state is already obsolete: Mux.yamux and Mux.test now exist as Libp2p.Core.Muxer values (packages/libp2p/mux/Libp2p/Mux/Yamux.lean:47, Test.lean:25), and the mock can simply be deleted. The suite takes muxer in one place, hostPair (Tests/ReqResp.lean:633-634), and uses the seam fields only. The swap is issue #78's muxer row, whose window closed 00:18 UTC 8 November, so it is overdue. I left the swap to you; it is the owed work, and a review nit commit should not rewire the suite's transport.

The stale prose is fixed in f0d269e. Four sites said issue #77 was still open. The module docstring of Mock/Muxer.lean now states the truth: the mux values took the real core in PR #84, and the swap of this mock is due on issue #78. The integration note drops the met condition. The package docs say the same at the mock row (packages/libp2p/protocols/docs/ARCHITECTURE.md:31) and at the suite bullet (:271-275). The retype stays acceptable as an intermediate state only because the docs now say so honestly. The body's sentence on #77 predates #84, so I read it as stale timing, not a false claim.

The core-mock swap itself is done and honest. Req/resp takes no type from Protocols.Mock.Core. ReqResp/Payload.lean names Libp2p.Core.Error and Libp2p.Core.ProtocolId (:107, :209), ReqResp/Limiter.lean keys its table by the real id (:27), and reqRespId answers the real ProtocolId (Constants.lean:66). The identify and ping ids stay on the mock with the comment that names issue #55 (Constants.lean:48-49), and their importers are Ping.lean:5, Constants.lean:2, and Tests/Protocols.lean:11. The prefix discipline the body claims holds: the comment at ReqResp/Exchange.lean:64-65 says once that a bare Core inside ReqResp is the reader core, OpenStream and mapError and handler carry the full prefix (:136, :208, :215), and Payload.lean uses no bare Core.

The new StreamError.lean is the one home. mapStreamError maps the real Streams.Error into the real Core.Error (:23-27), with set_option autoImplicit false (:16), the module doc, and the note that the mock keeps its copy until issue #55. The arms match the mock's copy field for field. Exchange.lean imports it and drops the mock import (:4). The root re-exports the module (Protocols.lean:2).

The two retyped mocks state their waits. Mock/Muxer.lean drops its copies of Role, MuxSession, and Muxer, takes them from Libp2p.Core (:55), reads the id and leaves it unread (:208), and joins instead of done (:217). Mock/HostStream.lean takes ProtocolId, StreamContext, StreamHandler, and MuxSession from libp2p/core (:49), and its docstring names what it waits for: the host's negotiate mock, issue #70 (:10-11). That claim stays true at this tip; the host package still carries Host/Mock/, and issue #70 is open. No new sorry, axiom, native_decide, or partial def enters the diff; the four partial defs of the package are the pre-existing read loops with their reasons.

Gates at f0d269e.

• lake build --wfail: pass, 253 jobs.
• lake test: 27189 passed, 0 failed, 10 skipped.
• lake test -- +RTS -N1 -RTS: 27189 passed, 0 failed.
• scripts/lint-imports.sh: 160 module files, 0 violations.

Axiom audit. #print axioms on Core.step, request, requestPeer, serve, handler, and all 17 package theorems, plus Libp2p.Protocols.mapStreamError: propext, Classical.choice, and Quot.sound at most, and mapStreamError depends on none. No sorryAx, no mock axiom. The result matches the body's table.

What remains of the three mocks. Mock/Core.lean stays for identify and ping until issue #55. Mock/HostStream.lean stays until the host's negotiate retype, the second part of issue #70. Mock/Muxer.lean owes its deletion on issue #78 now, and the integration note tells you the shape: take Mux.test or Mux.yamux in hostPair, no other change.

I pushed f0d269e to your fork with your branch as the lease.

APPROVE