feat(mux): integrate the core and yamux seams

packages/libp2p/mux/Libp2p/Mux.lean

@@ -1,12 +1,13 @@
 import Libp2p.Mux.Constants
+import Libp2p.Mux.Yamux
 import Libp2p.Mux.Test
 
 /-!
 # Libp2p.Mux
 
 The mux subpackage: the `Muxer` values over the muxer sessions
 (ARCHITECTURE §4.9). This root imports each public submodule.
-`Constants.lean` holds the ids. `Test.lean` holds `Mux.test`.
-`Mux.yamux` and `Mux.mplex` are later values. The package docs live
-under `docs/` beside this file.
+`Constants.lean` holds the ids. `Yamux.lean` holds `Mux.yamux`.
+`Test.lean` holds `Mux.test`. `Mux.mplex` is a later value. The
+package docs live under `docs/` beside this file.
 -/

packages/libp2p/mux/Libp2p/Mux/Constants.lean

@@ -1,4 +1,4 @@
-import Libp2p.Mux.Mock.Core.ProtocolId
+import Libp2p.Core.ProtocolId
 
 /-!
 # The constants of `libp2p/mux`
@@ -7,18 +7,15 @@ Each fact has one home (ARCHITECTURE §3.8). This module holds the
 three protocol ids and the mplex length cap. The production
 definitions of the ids live only here (§3.4).
 
-`ProtocolId` is the temporary copy in
-`Libp2p.Mux.Mock.Core.ProtocolId`. This module imports that file
-alone, so the constants do not import the session seam. W5.2 has not
-merged. When W5.2 lands, this import becomes `Libp2p.Core`. The four
-public names stay.
+`ProtocolId` comes from `Libp2p.Core.ProtocolId`. This module imports
+that file alone, so the constants do not import the session seam.
 -/
 
 set_option autoImplicit false
 
 namespace Libp2p.Mux
 
-open Mock.Core
+open Libp2p.Core
 
 /-- The yamux protocol id. Peers negotiate `/yamux/1.0.0` on the wire. -/
 def yamuxId : ProtocolId := { toString := "/yamux/1.0.0" }

packages/libp2p/mux/Libp2p/Mux/Test.lean

@@ -1,5 +1,5 @@
+import Libp2p.Core.Mux
 import Libp2p.Mux.Constants
-import Libp2p.Mux.Mock.Core
 import Libp2p.Mux.Test.Session
 
 /-!
@@ -15,7 +15,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Mux
 
-open Mock.Core
+open Libp2p.Core
 
 /-- The independent test muxer. `id` is `testId`. `open` starts the
 private session. The leftover bytes are the reader's first input. -/

packages/libp2p/mux/Libp2p/Mux/Test/Session.lean

@@ -1,4 +1,4 @@
-import Libp2p.Mux.Mock.Core
+import Libp2p.Core.Mux
 import Libp2p.Mux.Test.State
 import Libp2p.Mux.Test.Wire
 import Conc
@@ -28,7 +28,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Mux.Test.Session
 
-open Libp2p.Mux.Mock.Core
+open Libp2p.Core
 open Libp2p.Mux.Test.State
 open Libp2p.Mux.Test.Wire
 open Conc hiding Error

packages/libp2p/mux/Libp2p/Mux/Test/State.lean

@@ -1,5 +1,6 @@
+import Libp2p.Core.Error
+import Libp2p.Core.Role
 import Libp2p.Mux.Test.Wire
-import Libp2p.Mux.Mock.Core
 import Streams
 
 /-!
@@ -39,7 +40,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Mux.Test.State
 
-open Libp2p.Mux.Mock.Core
+open Libp2p.Core
 open Libp2p.Mux.Test.Wire
 
 /-! ## Caps and ids -/

packages/libp2p/mux/Libp2p/Mux/Yamux.lean

@@ -0,0 +1,60 @@
+import Libp2p.Core.Mux
+import Libp2p.Mux.Constants
+import Yamux.Session
+
+/-!
+# The yamux muxer
+
+`Mux.yamux` is the thin libp2p value over the landed session of
+`net/yamux`. It moves the role, the connection, and the negotiation
+leftover into `Session.new`. It maps errors returned by `openStream`
+and `join` into `Core.Error` at this boundary. The frames, the window,
+and the tasks stay in `net/yamux`.
+-/
+
+set_option autoImplicit false
+
+namespace Libp2p.Mux
+
+open Libp2p.Core
+
+/-- The Yamux side of a core role. The initiator is the client. It
+opens odd ids from 1. The responder is the server. It opens even ids
+from 2. -/
+private def yamuxRole : Role → Yamux.Role
+  | .initiator => .client
+  | .responder => .server
+
+/-- A Yamux protocol failure at the seam. Every arm ends the session,
+so the seam reports the protocol arm. The detail is the derived
+`Repr`. -/
+private def mapProtocolError (e : Yamux.ProtocolError) : Error :=
+  .protocol s!"yamux: {repr e}"
+
+/-- A refusal from `Session.openStream`. `closed` and `reset` use the
+closed arm, because this call has produced no stream. `timeout` uses
+the timeout arm. A later read or write on the returned stream keeps
+`Streams.Error`. -/
+private def mapOpenError (e : Streams.Error) : Error :=
+  let detail := s!"yamux: {repr e}"
+  match e with
+  | .closed => .closed detail
+  | .reset => .closed detail
+  | .timeout => .timeout detail
+
+/-- The production yamux muxer. `id` is `yamuxId`. `open` starts the
+landed session. The adapter maps its returned open and join errors
+into `Core.Error`. -/
+def yamux : Muxer where
+  id := yamuxId
+  «open» := fun role connection leftover => ExceptT.mk do
+    let session ← Yamux.Session.new (yamuxRole role) connection leftover
+    return .ok {
+      openStream := fun _ =>
+        ExceptT.mk ((Except.mapError mapOpenError) <$> session.openStream)
+      accept := session.acceptStream
+      close := session.close
+      join := ExceptT.mk ((Except.mapError mapProtocolError) <$> session.join)
+    }
+
+end Libp2p.Mux