[Mouzayan]

Summary

Mux.yamux now fills the landed Libp2p.Core muxer seam over the net/yamux session.

• Removed the temporary Libp2p/Mux/Mock/ modules. The constants, Mux.test, and Mux.yamux now use Libp2p.Core.
• Mapped the initiator to the Yamux client and the responder to the Yamux server.
• Forwarded the connection and negotiation leftovers to Yamux.Session.new. Mux.yamux intentionally drops the per-stream ProtocolId, because a Yamux SYN has no protocol-ID field.
• Mapped returned open and join errors to Core.Error at the adapter boundary. Connection IO.Errors remain thrown.
• Added public adapter tests for protocol identity, role and stream-ID mapping, full-duplex exchange, leftover delivery, returned errors, repeated joins, and connection faults.
• Kept the ownership boundary narrow: framing, flow control, keepalive, and session tasks remain in net/yamux; Mux.test remains the independent repository test muxer.

Mplex remains deferred P2 work and is not added by this pull request.

Closes #77
Closes #17

Validation

• lake build Libp2pMux
• lake build tests
• lake build --wfail
• scripts/lint-imports.sh
• Linux build-and-test
• Linux snappy-native-hardening

Local macOS testing retains one pre-existing Streams/TCP failure: the teardown aborted the stuck write: the peer meets a reset. The affected code is unchanged from hackathon26; Linux CI passes both test modes.

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 c5d63d3, rebased onto hackathon26 at 147afc4 (the merges of #79 and #82). The rebase applied clean, no conflicts. I read the adapter, the seam it fills, the session it adapts, the package docs, and the test suite. I ran the full gates on Linux.

Window. The core-mock window closed 2026-11-07 19:22 UTC (12 hours after the #64 merge at 07:21 UTC). The swap landed with this PR, whose first commit is dated 2026-11-08 22:58 UTC, 27.6 hours over the window. The swap is complete, so the late landing goes on record as a note.

The mock is gone. Libp2p/Mux/Mock/ is deleted, and a grep over packages/, Tests/, and lakefile.toml finds no Mock reference. Constants.lean imports Libp2p.Core.ProtocolId and imports it alone, so the constants stay free of the session seam (packages/libp2p/mux/Libp2p/Mux/Constants.lean:1). Test.lean, Test/Session.lean, and Test/State.lean import the Libp2p.Core modules that own the same names. The swap is the delete-and-move the seam issue asked for.

The adapter. Mux.yamux is a thin value over Yamux.Session.new (packages/libp2p/mux/Libp2p/Mux/Yamux.lean:48).

• §5.1. The adapter reads no length-prefixed data. It forwards the negotiation leftover to the session, and the session posts it as the first event into its bounded queue (packages/net/yamux/Yamux/Session.lean:87-89). Frame reads stay capped at 256 KiB in net/yamux, reviewed at feat(yamux): W4.3, the stream muxer #62. The forwarding bypasses no cap.
• §4.1. The adapter spawns no task and owns none. Session.new spawns its loop, writer, reader, and ticker into one TaskSet (packages/net/yamux/Yamux/Session.lean:90-96). Teardown closes the event queue and the room channel, which wakes every parked accept, open, and write (Session.lean:125-127). No cancellation anywhere in the path.
• §5.6. The leftover reaches the session as data, and the loop takes it as its first event (packages/libp2p/mux/Libp2p/Mux/Yamux.lean:50-51). No stage shares a reader.
• The ProtocolId drop. openStream discards the argument (Yamux.lean:53). The drop is recorded twice: the seam field docstring (packages/libp2p/core/Libp2p/Core/Mux.lean:36-38) and the package docs, "The yamux value" (packages/libp2p/mux/docs/ARCHITECTURE.md). Recorded per the refactor(protocols): run req/resp over the seam types of libp2p/core #81 precedent, so the unread argument is acceptable.
• Role mapping. yamuxRole maps initiator to the client and responder to the server (Yamux.lean:24-26); the session applies the parity. The tests read the SYN off the raw peer connection: stream 1 for the initiator, stream 2 for the responder (Tests/Mux.lean:3839, 3891).
• Error mapping. mapOpenError covers the three arms of Streams.Error (packages/net/streams/Streams/Error.lean:15-25): closed and reset become Core.Error.closed, timeout becomes Core.Error.timeout (Yamux.lean:38-43). mapProtocolError becomes Core.Error.protocol (Yamux.lean:31-32). Both maps are private and applied once at this boundary, as owned contract 6 asks. A thrown connection IO.Error passes under both maps and reaches the caller thrown, and the test pins that (Tests/Mux.lean:4122).

The tests. The body's list is covered: identity (yamux.id = yamuxId, Tests/Mux.lean:4162), role and stream-id mapping from the wire, a full-duplex exchange with payloads in both directions and clean joins (Tests/Mux.lean:3923), leftover delivery, where a remote SYN, FIN, and payload ride in the leftover ByteArray and the responder accepts the stream (Tests/Mux.lean:3984, 4013), error mapping with the exact detail strings (Tests/Mux.lean:4049), an open after a clean close (Tests/Mux.lean:4086), repeated joins, a second join returns the same protocol error and a second join after a fault throws the same fault (Tests/Mux.lean:4049, 4122), and connection faults. The session-level framing, flow-control, and hostile-frame coverage stays in the net/yamux suite, which keeps the ownership boundary the body records.

Gates. lake build --wfail passes, 253 jobs. lake test reports 27188 passed, 0 failed, 10 skipped. lake test -- +RTS -N1 -RTS reports the same. scripts/lint-imports.sh reports 160 module files, 0 violations.

Axioms. #print axioms on Mux.yamux, Mux.test, Test.Wire.Header.instLawfulCodec, Test.Wire.Frame.instLawfulCodec, Header.decode?_append, Frame.decode?_append, and Frame.decode?_overCap reports propext, Classical.choice, and Quot.sound only. No sorryAx, no mock axiom. A grep over the package and Tests/Mux.lean finds no sorry, axiom, native_decide, unsafe, or partial def.

One nit, fixed. Tests.Mux.YamuxAdapter.runBoundary had no caller, and no suite-selection mechanism exists that could call it. One commit carries the deletion: c5d63d3, "test(mux): drop the uncalled focused-run entry".

The body's macOS note covers a pre-existing Streams/TCP failure in the author's local environment; the affected code is unchanged from hackathon26, and the Linux gates pass both test modes.

APPROVE