From 7543b165f595b5f01fde66362d75838e819b71ac Mon Sep 17 00:00:00 2001
From: Mouzayan Delbourgo <mouzbuilds@gmail.com>
Date: Sun, 8 Nov 2026 17:58:00 -0500
Subject: [PATCH 1/6] feat(mux): replace the core mock with Libp2p.Core

---
 Tests/Mux.lean                                | 24 +++---
 packages/libp2p/mux/Libp2p/Mux/Constants.lean | 11 +--
 packages/libp2p/mux/Libp2p/Mux/Mock/Core.lean | 75 -------------------
 .../mux/Libp2p/Mux/Mock/Core/ProtocolId.lean  | 27 -------
 packages/libp2p/mux/Libp2p/Mux/Test.lean      |  4 +-
 .../libp2p/mux/Libp2p/Mux/Test/Session.lean   |  4 +-
 .../libp2p/mux/Libp2p/Mux/Test/State.lean     |  5 +-
 7 files changed, 23 insertions(+), 127 deletions(-)
 delete mode 100644 packages/libp2p/mux/Libp2p/Mux/Mock/Core.lean
 delete mode 100644 packages/libp2p/mux/Libp2p/Mux/Mock/Core/ProtocolId.lean

diff --git a/Tests/Mux.lean b/Tests/Mux.lean
index 253b3cfc..06fc9186 100644
--- a/Tests/Mux.lean
+++ b/Tests/Mux.lean
@@ -1,6 +1,6 @@
 import Tests.Support
+import Libp2p.Core.Mux
 import Libp2p.Mux
-import Libp2p.Mux.Mock.Core
 import Libp2p.Mux.Test.Wire
 import Libp2p.Mux.Test.State
 import Libp2p.Mux.Test.Session
@@ -11,7 +11,7 @@ import Multiformats
 /-!
 # Mux suite (unit W5.4)
 
-The constant checks, the temporary core seam, the private
+The constant checks, the core seam, the private
 test-wire codec and parser, the pure session transitions, and the
 runtime shell (`packages/libp2p/mux/docs/ARCHITECTURE.md`).
 -/
@@ -412,7 +412,7 @@ end Tests.Mux.Wire
 namespace Tests.Mux.Seam
 
 open Libp2p.Mux
-open Libp2p.Mux.Mock.Core
+open Libp2p.Core
 
 /-- The detail carried by one seam error. -/
 private def detail : Error → String
@@ -446,13 +446,13 @@ example : Muxer := {
       openStream := fun _ => throw (Error.closed "unused")
       accept := pure none
       close := pure ()
-      join := pure (.ok ())
+      join := pure ()
     }
 }
 
-/-- The temporary seam types. -/
+/-- The seam types. -/
 def run (r : Runner) : IO Unit := do
-  r.section "mux core seam" "packages/libp2p/mux/Libp2p/Mux/Mock/Core.lean"
+  r.section "mux core seam" "packages/libp2p/core/Libp2p/Core/Mux.lean"
   r.check "the two roles are distinct"
     (decide (Role.initiator ≠ Role.responder))
   let p := Error.protocol "wire"
@@ -468,7 +468,7 @@ end Tests.Mux.Seam
 
 namespace Tests.Mux.State
 
-open Libp2p.Mux.Mock.Core
+open Libp2p.Core
 open Libp2p.Mux.Test.Wire
 open Libp2p.Mux.Test.State
 
@@ -1639,7 +1639,7 @@ end Tests.Mux.State
 
 namespace Tests.Mux.Session
 
-open Libp2p.Mux.Mock.Core
+open Libp2p.Core
 open Libp2p.Mux.Test.Session
 open Libp2p.Mux.Test.State
 open Libp2p.Mux.Test.Wire
@@ -2830,7 +2830,7 @@ end Tests.Mux.Session
 namespace Tests.Mux.Public
 
 open Libp2p.Mux
-open Libp2p.Mux.Mock.Core
+open Libp2p.Core
 open Libp2p.Mux.Test.Wire
 open Conc
 open Streams
@@ -3044,8 +3044,8 @@ private def runConcurrentOpens (r : Runner) : Async Unit := do
   let pair ← ends 49
   let initiator ← openSession .initiator pair.dialer
   let responder ← openSession .responder pair.peer
-  let initiatorOpen : Chan (Except Mock.Core.Error Stream) ← Chan.new 1
-  let responderOpen : Chan (Except Mock.Core.Error Stream) ← Chan.new 1
+  let initiatorOpen : Chan (Except Libp2p.Core.Error Stream) ← Chan.new 1
+  let responderOpen : Chan (Except Libp2p.Core.Error Stream) ← Chan.new 1
   let workers ← TaskSet.new
   workers.spawn do
     let result ← (initiator.openStream testId).run
@@ -3156,7 +3156,7 @@ private def runMalformed (r : Runner) : Async Unit := do
     r.check "a second public join returns the same protocol error" false
   | .ok sess =>
     let observed : Except IO.Error
-        (Except Mock.Core.Error Unit × Except Mock.Core.Error Unit) ←
+        (Except Libp2p.Core.Error Unit × Except Libp2p.Core.Error Unit) ←
       try
         pair.peer.write ⟨#[0, 0, 0, 0, 1, 0, 0, 0, 0]⟩
         pure (.ok (← sess.join, ← sess.join))
diff --git a/packages/libp2p/mux/Libp2p/Mux/Constants.lean b/packages/libp2p/mux/Libp2p/Mux/Constants.lean
index 1287a263..e719a7b9 100644
--- a/packages/libp2p/mux/Libp2p/Mux/Constants.lean
+++ b/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" }
diff --git a/packages/libp2p/mux/Libp2p/Mux/Mock/Core.lean b/packages/libp2p/mux/Libp2p/Mux/Mock/Core.lean
deleted file mode 100644
index f1f67417..00000000
--- a/packages/libp2p/mux/Libp2p/Mux/Mock/Core.lean
+++ /dev/null
@@ -1,75 +0,0 @@
-import Libp2p.Mux.Mock.Core.ProtocolId
-import Conc
-import Streams
-
-/-!
-# Mock: the muxer seam of `libp2p/core`
-
-W5.2 is not merged. This module copies the seam that `Mux.test` must
-compile against (the core pair, public surface; the mux pair, public
-surface). It holds no protocol logic.
-
-`Role` and the four `Error` arms follow the core architecture. The
-`String` on each arm is a provisional rendered payload. `MuxSession.join`
-is a provisional name for the completion the owner joins. Neither
-spelling is a landed `Libp2p.Core` declaration.
-
-`Connection` and `Stream` come from `Streams`. `Async` comes from
-`Conc`. This module does not copy those types. When W5.2 lands, delete
-this module and `Mock/Core/ProtocolId.lean`. The imports move to the
-`Libp2p.Core` modules that own the same names.
--/
-
-set_option autoImplicit false
-
-namespace Libp2p.Mux.Mock.Core
-
-open Conc
-
-/-- The local direction of a connection. The core architecture names
-`initiator` and `responder`, and gives the set no wire code. -/
-inductive Role where
-  | initiator
-  | responder
-  deriving DecidableEq, Repr, Hashable
-
-/-- The coarse seam error. The four arms are the categories in the
-core architecture. `detail` is a provisional `String` rendering of the
-implementation error. -/
-inductive Error where
-  | protocol (detail : String)
-  | authentication (detail : String)
-  | timeout (detail : String)
-  | closed (detail : String)
-  deriving DecidableEq, Repr, Hashable
-
-/-- The session view a `Muxer` returns. `join` is the provisional
-completion the owner waits on after `close`. -/
-structure MuxSession where
-  /-- Open one outbound stream. The argument is a `ProtocolId`. -/
-  openStream :
-    ProtocolId → ExceptT Error Async Streams.Stream
-  /-- The next inbound stream. `none` means the session has closed. -/
-  accept :
-    Async (Option Streams.Stream)
-  /-- Close the session. -/
-  close :
-    IO Unit
-  /-- Wait until the session tasks end. `.ok ()` is an orderly end.
-  `.error` is the protocol result. A fault throws. -/
-  join :
-    Async (Except Error Unit)
-
-/-- A muxer selected by its protocol id. `«open»` is the field `open`:
-`open` is a Lean keyword. -/
-structure Muxer where
-  /-- The id the negotiator compares. -/
-  id : ProtocolId
-  /-- Start a session. The `ByteArray` is the negotiation leftover. -/
-  «open» :
-    Role →
-    Streams.Connection →
-    ByteArray →
-    ExceptT Error Async MuxSession
-
-end Libp2p.Mux.Mock.Core
diff --git a/packages/libp2p/mux/Libp2p/Mux/Mock/Core/ProtocolId.lean b/packages/libp2p/mux/Libp2p/Mux/Mock/Core/ProtocolId.lean
deleted file mode 100644
index 4c29041e..00000000
--- a/packages/libp2p/mux/Libp2p/Mux/Mock/Core/ProtocolId.lean
+++ /dev/null
@@ -1,27 +0,0 @@
-/-!
-# Mock: the `ProtocolId` surface of `libp2p/core`
-
-W5.2 (`libp2p/core`) is not yet merged, so this package builds against
-a temporary copy of the documented `ProtocolId` surface (RULES.md,
-"Working ahead of the tree"; the core pair, public surface). The copy
-is `structure ProtocolId where toString : String`. It derives
-`DecidableEq` and `Hashable` from that surface, and `Repr` from the
-standard identifier classes (ARCHITECTURE §3.2, §3.4).
-
-This module imports nothing. `Constants.lean` imports it alone, so the
-protocol ids stay free of the session seam. The seam lives in
-`Libp2p/Mux/Mock/Core.lean`. When W5.2 lands, delete both mock
-modules. `Constants.lean` then imports `Libp2p.Core`.
--/
-
-set_option autoImplicit false
-
-namespace Libp2p.Mux.Mock.Core
-
-/-- A protocol id: an open wrapped string (ARCHITECTURE §3.4). Peers
-define ids, so the set stays open. -/
-structure ProtocolId where
-  toString : String
-  deriving DecidableEq, Repr, Hashable
-
-end Libp2p.Mux.Mock.Core
diff --git a/packages/libp2p/mux/Libp2p/Mux/Test.lean b/packages/libp2p/mux/Libp2p/Mux/Test.lean
index 69683713..faf9c4ee 100644
--- a/packages/libp2p/mux/Libp2p/Mux/Test.lean
+++ b/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. -/
diff --git a/packages/libp2p/mux/Libp2p/Mux/Test/Session.lean b/packages/libp2p/mux/Libp2p/Mux/Test/Session.lean
index d09bc50a..06c8756c 100644
--- a/packages/libp2p/mux/Libp2p/Mux/Test/Session.lean
+++ b/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
diff --git a/packages/libp2p/mux/Libp2p/Mux/Test/State.lean b/packages/libp2p/mux/Libp2p/Mux/Test/State.lean
index 12327ee9..027e69b4 100644
--- a/packages/libp2p/mux/Libp2p/Mux/Test/State.lean
+++ b/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 -/

From a78e73ccb3efe97f10fd12973bdafc5e6e3c8f60 Mon Sep 17 00:00:00 2001
From: Mouzayan Delbourgo <mouzbuilds@gmail.com>
Date: Sun, 8 Nov 2026 18:21:43 -0500
Subject: [PATCH 2/6] feat(mux): add the yamux Muxer value

---
 packages/libp2p/mux/Libp2p/Mux.lean       |  7 +--
 packages/libp2p/mux/Libp2p/Mux/Yamux.lean | 60 +++++++++++++++++++++++
 2 files changed, 64 insertions(+), 3 deletions(-)
 create mode 100644 packages/libp2p/mux/Libp2p/Mux/Yamux.lean

diff --git a/packages/libp2p/mux/Libp2p/Mux.lean b/packages/libp2p/mux/Libp2p/Mux.lean
index d74c8f08..e3ee104a 100644
--- a/packages/libp2p/mux/Libp2p/Mux.lean
+++ b/packages/libp2p/mux/Libp2p/Mux.lean
@@ -1,4 +1,5 @@
 import Libp2p.Mux.Constants
+import Libp2p.Mux.Yamux
 import Libp2p.Mux.Test
 
 /-!
@@ -6,7 +7,7 @@ import Libp2p.Mux.Test
 
 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.
 -/
diff --git a/packages/libp2p/mux/Libp2p/Mux/Yamux.lean b/packages/libp2p/mux/Libp2p/Mux/Yamux.lean
new file mode 100644
index 00000000..6e829005
--- /dev/null
+++ b/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

From dfe78ed8493bf0814adc6edd1857cfae9018e672 Mon Sep 17 00:00:00 2001
From: Mouzayan Delbourgo <mouzbuilds@gmail.com>
Date: Sun, 8 Nov 2026 18:57:58 -0500
Subject: [PATCH 3/6] test(mux): cover the yamux adapter

---
 Tests/Mux.lean | 249 ++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 247 insertions(+), 2 deletions(-)

diff --git a/Tests/Mux.lean b/Tests/Mux.lean
index 06fc9186..b4c9f6fa 100644
--- a/Tests/Mux.lean
+++ b/Tests/Mux.lean
@@ -4,6 +4,7 @@ import Libp2p.Mux
 import Libp2p.Mux.Test.Wire
 import Libp2p.Mux.Test.State
 import Libp2p.Mux.Test.Session
+import Yamux.Header
 import Conc
 import Streams
 import Multiformats
@@ -12,8 +13,9 @@ import Multiformats
 # Mux suite (unit W5.4)
 
 The constant checks, the core seam, the private
-test-wire codec and parser, the pure session transitions, and the
-runtime shell (`packages/libp2p/mux/docs/ARCHITECTURE.md`).
+test-wire codec and parser, the pure session transitions, the
+runtime shell, and the yamux adapter boundary
+(`packages/libp2p/mux/docs/ARCHITECTURE.md`).
 -/
 
 set_option autoImplicit false
@@ -3744,6 +3746,248 @@ def runLocal (r : Runner) : IO Unit := do
 
 end Tests.Mux.Public
 
+namespace Tests.Mux.YamuxAdapter
+
+open Libp2p.Mux
+open Libp2p.Core
+open Conc
+open Streams hiding Error
+open Streams.Sim
+open Multiformats
+
+/-- A protocol id passed to `openStream`. A Yamux header carries the
+type, the flags, the stream id, and the length. -/
+private def unrelatedId : ProtocolId := { toString := "/leanp2p/adapter-probe/1" }
+
+/-- The payload the initiator writes. -/
+private def toResponder : ByteArray := "from the initiator".toUTF8
+
+/-- The payload the responder writes. -/
+private def toInitiator : ByteArray := "from the responder".toUTF8
+
+private structure Ends where
+  dialer : Connection
+  peer : Connection
+
+/-- Close the listener, then join it. A close fault is dropped, so the
+caller can rethrow the error that happened first. -/
+private def closeListener (l : Listener) : Async Unit := do
+  try
+    l.close
+    l.join
+  catch _ =>
+    pure ()
+
+/-- A connected pair on a fresh sim net. The listener closes once both
+ends exist. It also closes when dial or accept fails, and that failure
+is the one that propagates. -/
+private def ends (n : Nat) : Async Ends := do
+  let net ← Net.new
+  let addr ← match Multiaddr.parse? s!"/ip4/127.0.0.1/tcp/{n}" with
+    | .ok a => pure a
+    | .error _ => throw <| IO.userError s!"test address {n} does not parse"
+  let l ← net.listen addr
+  let dialed : Except IO.Error Connection ← try
+    match ← net.dial l.addr with
+    | some dialer => pure (.ok dialer)
+    | none => pure (.error <| IO.userError "dial failed")
+  catch e =>
+    pure (.error e)
+  match dialed with
+  | .error e =>
+    closeListener l
+    throw e
+  | .ok dialer =>
+    let accepted : Except IO.Error Connection ← try
+      match ← l.accept with
+      | some peer => pure (.ok peer)
+      | none => pure (.error <| IO.userError "accept failed")
+    catch e =>
+      pure (.error e)
+    match accepted with
+    | .error e =>
+      dialer.closeQuietly
+      closeListener l
+      throw e
+    | .ok peer =>
+      let closed : Except IO.Error Unit ← try
+        l.close
+        l.join
+        pure (.ok ())
+      catch e =>
+        pure (.error e)
+      match closed with
+      | .error e =>
+        dialer.closeQuietly
+        peer.closeQuietly
+        throw e
+      | .ok () =>
+        return { dialer, peer }
+
+/-- The next header-sized read, decoded as one Yamux header. -/
+private def nextHeader (c : Connection) : Async (Except String Yamux.Header) := do
+  match ← c.readExactly Yamux.headerSize with
+  | none => return .error "the peer connection ended before a header"
+  | some (frame, _) =>
+    match Yamux.Header.decodeB? frame with
+    | .error e => return .error s!"the next frame is not a Yamux header ({repr e})"
+    | .ok (h, _) => return .ok h
+
+/-- The Yamux stream-open frame for `streamId`: a window update, the
+SYN flag alone, and a zero length. -/
+private def isSynOpen (h : Yamux.Header) (streamId : Nat) : Bool :=
+  h.type == .windowUpdate
+    && h.flags == { Yamux.Flags.none with syn := true }
+    && h.streamId == streamId
+    && h.length == 0
+
+/-- Close `sessions`, then both raw ends. The body error in `fault`
+has priority. Otherwise the first session close or join error is
+reported. Both raw ends are always closed quietly. -/
+private def cleanup (fault : Option IO.Error) (sessions : List MuxSession)
+    (dialer peer : Connection) : Async Unit := do
+  let mut cleanupError : Option IO.Error := none
+  for s in sessions do
+    let closed ← try
+      s.close
+      pure true
+    catch e =>
+      if cleanupError.isNone then
+        cleanupError := some e
+      pure false
+    if closed then
+      try
+        match ← s.join with
+        | .ok () => pure ()
+        | .error e =>
+          if cleanupError.isNone then
+            cleanupError := some (IO.userError s!"yamux adapter join: {e}")
+      catch e =>
+        if cleanupError.isNone then
+          cleanupError := some e
+  dialer.closeQuietly
+  peer.closeQuietly
+  match fault with
+  | some e => throw e
+  | none =>
+    match cleanupError with
+    | some e => throw e
+    | none => pure ()
+
+/-- Read `n` bytes from the stream. A short close or a stream error
+throws. -/
+private def readBytes (s : Stream) (n : Nat) : Async ByteArray := do
+  let mut acc : ByteArray := .empty
+  while acc.size < n do
+    match ← s.read with
+    | .ok (some chunk) => acc := acc ++ chunk
+    | .ok none => throw <| IO.userError "the stream ended before the payload"
+    | .error e => throw <| IO.userError s!"a stream read failed: {repr e}"
+  return acc
+
+/-- The first outbound frame of one isolated session. The raw peer
+reads it. `streamId` is the id that role opens first. -/
+private def runRole (r : Runner) (n : Nat) (role : Role) (streamId : Nat)
+    (title : String) : Async Unit := do
+  let pair ← ends n
+  let mut opened : Option MuxSession := none
+  let outcome : Except IO.Error Unit ← try
+    match ← (yamux.open role pair.dialer .empty).run with
+    | .error e =>
+      r.check s!"{title} ({e})" false
+      pure (.ok ())
+    | .ok sess =>
+      opened := some sess
+      match ← (sess.openStream unrelatedId).run with
+      | .error e =>
+        r.check s!"{title} ({e})" false
+      | .ok _ =>
+        match ← nextHeader pair.peer with
+        | .error detail =>
+          r.check s!"{title} ({detail})" false
+        | .ok h =>
+          -- `unrelatedId` is the argument of this open. The check
+          -- reads the Yamux header fields.
+          r.check title (isSynOpen h streamId)
+      pure (.ok ())
+  catch e =>
+    pure (.error e)
+  let fault := match outcome with
+    | .error e => some e
+    | .ok () => none
+  cleanup fault opened.toList pair.dialer pair.peer
+
+/-- One full-duplex stream through `Mux.yamux`, with payloads in both
+directions, then clean joins. -/
+private def runExchange (r : Runner) : Async Unit := do
+  let pair ← ends 4182
+  let mut dialSess : Option MuxSession := none
+  let mut peerSess : Option MuxSession := none
+  let outcome : Except IO.Error Unit ← try
+    match ← (yamux.open .initiator pair.dialer .empty).run with
+    | .error e =>
+      r.check s!"the initiator session opens ({e})" false
+      pure (.ok ())
+    | .ok dial =>
+      dialSess := some dial
+      match ← (yamux.open .responder pair.peer .empty).run with
+      | .error e =>
+        r.check s!"the responder session opens ({e})" false
+        pure (.ok ())
+      | .ok peer =>
+        peerSess := some peer
+        match ← (dial.openStream unrelatedId).run with
+        | .error e =>
+          r.check s!"the initiator opens a stream ({e})" false
+          pure (.ok ())
+        | .ok outbound =>
+          match ← peer.accept with
+          | none =>
+            r.check "the responder accepts the initiator's stream" false
+            pure (.ok ())
+          | some inbound =>
+            r.check "the responder accepts the initiator's stream" true
+            match ← outbound.write toResponder with
+            | .error e => throw <| IO.userError s!"the initiator write failed: {repr e}"
+            | .ok () => pure ()
+            let got ← readBytes inbound toResponder.size
+            r.check "the initiator's payload arrives unchanged" (got == toResponder)
+            match ← inbound.write toInitiator with
+            | .error e => throw <| IO.userError s!"the responder write failed: {repr e}"
+            | .ok () => pure ()
+            let back ← readBytes outbound toInitiator.size
+            r.check "the responder's payload arrives unchanged" (back == toInitiator)
+            dial.close
+            peer.close
+            match ← dial.join with
+            | .ok () => r.check "the initiator joins cleanly" true
+            | .error e => r.check s!"the initiator joins cleanly ({e})" false
+            match ← peer.join with
+            | .ok () => r.check "the responder joins cleanly" true
+            | .error e => r.check s!"the responder joins cleanly ({e})" false
+            dialSess := none
+            peerSess := none
+            pure (.ok ())
+  catch e =>
+    pure (.error e)
+  let fault := match outcome with
+    | .error e => some e
+    | .ok () => none
+  cleanup fault (dialSess.toList ++ peerSess.toList) pair.dialer pair.peer
+
+private def checks (r : Runner) : Async Unit := do
+  r.check "Mux.yamux.id is Mux.yamuxId" (decide (yamux.id = yamuxId))
+  runRole r 4180 .initiator 1 "an initiator open emits a Yamux SYN for stream 1"
+  runRole r 4181 .responder 2 "a responder open emits a Yamux SYN for stream 2"
+  runExchange r
+
+/-- The yamux adapter boundary over the sim connection. -/
+def run (r : Runner) : IO Unit := do
+  r.section "mux yamux adapter" "packages/libp2p/mux/Libp2p/Mux/Yamux.lean"
+  Async.run (checks r)
+
+end Tests.Mux.YamuxAdapter
+
 namespace Tests
 
 open Libp2p.Mux
@@ -3767,5 +4011,6 @@ def Mux.run (r : Runner) : IO Unit := do
   Mux.State.run r
   Mux.Session.run r
   Mux.Public.run r
+  Mux.YamuxAdapter.run r
 
 end Tests

From a384d82409c8f292a4f02b3dfe18fdc2fc545915 Mon Sep 17 00:00:00 2001
From: Mouzayan Delbourgo <mouzbuilds@gmail.com>
Date: Sun, 8 Nov 2026 19:15:21 -0500
Subject: [PATCH 4/6] test(mux): cover yamux adapter errors

---
 Tests/Mux.lean | 199 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 199 insertions(+)

diff --git a/Tests/Mux.lean b/Tests/Mux.lean
index b4c9f6fa..e2b8ae54 100644
--- a/Tests/Mux.lean
+++ b/Tests/Mux.lean
@@ -5,6 +5,7 @@ import Libp2p.Mux.Test.Wire
 import Libp2p.Mux.Test.State
 import Libp2p.Mux.Test.Session
 import Yamux.Header
+import Yamux.Core
 import Conc
 import Streams
 import Multiformats
@@ -3975,17 +3976,215 @@ private def runExchange (r : Runner) : Async Unit := do
     | .ok () => none
   cleanup fault (dialSess.toList ++ peerSess.toList) pair.dialer pair.peer
 
+/-- The payload carried in the leftover. -/
+private def leftoverPayload : ByteArray := "from the leftover".toUTF8
+
+/-- The peer's stream open and its payload. The responder sees stream 1.
+The peer connection writes none of these bytes. -/
+private def leftoverBytes : ByteArray :=
+  let openHeader := Yamux.Header.make .windowUpdate
+    { Yamux.Flags.none with syn := true } 1 0
+  let dataHeader := Yamux.Header.make .data
+    { Yamux.Flags.none with fin := true } 1 leftoverPayload.size
+  Yamux.Header.encodeB openHeader ++ Yamux.Header.encodeB dataHeader ++ leftoverPayload
+
+/-- A 12-byte header whose version is 1. The codec accepts version 0. -/
+private def malformedHeader : ByteArray :=
+  ⟨#[1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]⟩
+
+/-- The text of the connection fault the read gate throws. -/
+private def readFault : IO.Error :=
+  IO.userError "yamux adapter: the connection read failed"
+
+/-- What one public `join` did. A throw keeps its rendered text. -/
+private inductive ObservedJoin where
+  | returned (result : Except Libp2p.Core.Error Unit)
+  | threw (text : String)
+
+/-- Run `join`. A returned `Core.Error` stays returned. A thrown
+`IO.Error` stays thrown, and this call renders it. -/
+private def observeJoin (s : MuxSession) : Async ObservedJoin := do
+  try
+    return .returned (← (s.join).run)
+  catch e =>
+    return .threw (toString e)
+
+/-- The responder takes a remote open from the leftover `ByteArray`. -/
+private def runLeftover (r : Runner) : Async Unit := do
+  let pair ← ends 4190
+  let mut opened : Option MuxSession := none
+  let outcome : Except IO.Error Unit ← try
+    match ← (yamux.open .responder pair.dialer leftoverBytes).run with
+    | .error e =>
+      r.check s!"the leftover stream is accepted ({e})" false
+      pure (.ok ())
+    | .ok sess =>
+      opened := some sess
+      match ← sess.accept with
+      | none =>
+        r.check "the leftover stream is accepted" false
+        pure (.ok ())
+      | some inbound =>
+        r.check "the leftover stream is accepted" true
+        let got ← readBytes inbound leftoverPayload.size
+        r.check "the leftover payload arrives unchanged" (got == leftoverPayload)
+        sess.close
+        match ← observeJoin sess with
+        | .returned (.ok ()) =>
+          r.check "the leftover session joins cleanly" true
+        | .returned (.error e) =>
+          r.check s!"the leftover session joins cleanly ({e})" false
+        | .threw text =>
+          r.check s!"the leftover session joins cleanly (thrown {text})" false
+        opened := none
+        pure (.ok ())
+  catch e =>
+    pure (.error e)
+  let fault := match outcome with
+    | .error e => some e
+    | .ok () => none
+  cleanup fault opened.toList pair.dialer pair.peer
+
+/-- One malformed header becomes the yamux protocol error, twice. -/
+private def runProtocol (r : Runner) : Async Unit := do
+  let pair ← ends 4191
+  let mut opened : Option MuxSession := none
+  let outcome : Except IO.Error Unit ← try
+    match ← (yamux.open .initiator pair.dialer .empty).run with
+    | .error e =>
+      r.check s!"a malformed header joins as the yamux protocol error ({e})" false
+      pure (.ok ())
+    | .ok sess =>
+      opened := some sess
+      pair.peer.write malformedHeader
+      let detail := s!"yamux: {repr Yamux.ProtocolError.malformedHeader}"
+      match ← observeJoin sess with
+      | .threw text =>
+        r.check s!"a malformed header joins as the yamux protocol error (thrown {text})" false
+      | .returned (.ok ()) =>
+        r.check "a malformed header joins as the yamux protocol error (join returned ok)" false
+      | .returned (.error e) =>
+        r.check "a malformed header joins as the yamux protocol error"
+          (e == .protocol detail)
+        match ← observeJoin sess with
+        | .threw text =>
+          r.check s!"a second join returns the same protocol error (thrown {text})" false
+        | .returned (.ok ()) =>
+          r.check "a second join returns the same protocol error (join returned ok)" false
+        | .returned (.error e2) =>
+          r.check "a second join returns the same protocol error" (e2 == e)
+      opened := none
+      pure (.ok ())
+  catch e =>
+    pure (.error e)
+  let fault := match outcome with
+    | .error e => some e
+    | .ok () => none
+  cleanup fault opened.toList pair.dialer pair.peer
+
+/-- After a clean close, `openStream` returns the yamux closed error. -/
+private def runOpenAfterClose (r : Runner) : Async Unit := do
+  let pair ← ends 4192
+  let mut opened : Option MuxSession := none
+  let outcome : Except IO.Error Unit ← try
+    match ← (yamux.open .initiator pair.dialer .empty).run with
+    | .error e =>
+      r.check s!"a closed session joins cleanly ({e})" false
+      pure (.ok ())
+    | .ok sess =>
+      opened := some sess
+      sess.close
+      match ← observeJoin sess with
+      | .threw text =>
+        r.check s!"a closed session joins cleanly (thrown {text})" false
+      | .returned (.error e) =>
+        r.check s!"a closed session joins cleanly ({e})" false
+      | .returned (.ok ()) =>
+        r.check "a closed session joins cleanly" true
+        let detail := s!"yamux: {repr Streams.Error.closed}"
+        match ← (sess.openStream unrelatedId).run with
+        | .error (.closed d) =>
+          r.check "an open after close returns the yamux closed error" (d == detail)
+        | .error e =>
+          r.check s!"an open after close returns the yamux closed error ({e})" false
+        | .ok _ =>
+          r.check "an open after close returns the yamux closed error (a stream opened)" false
+      opened := none
+      pure (.ok ())
+  catch e =>
+    pure (.error e)
+  let fault := match outcome with
+    | .error e => some e
+    | .ok () => none
+  cleanup fault opened.toList pair.dialer pair.peer
+
+/-- A gated read throws, and both joins throw that same fault. -/
+private def runReadFault (r : Runner) : Async Unit := do
+  let pair ← ends 4193
+  let gate ← Chan.new 1
+  let dialer : Connection := { pair.dialer with
+    read := do
+      discard <| gate.recv
+      throw readFault }
+  let mut opened : Option MuxSession := none
+  let outcome : Except IO.Error Unit ← try
+    match ← (yamux.open .initiator dialer .empty).run with
+    | .error e =>
+      r.check s!"a connection read fault escapes the first join ({e})" false
+      pure (.ok ())
+    | .ok sess =>
+      opened := some sess
+      -- `open` has returned. The read is still parked on `gate`.
+      match ← gate.send () with
+      | .error _ => throw <| IO.userError "the read gate did not release"
+      | .ok () => pure ()
+      let want := toString readFault
+      match ← observeJoin sess with
+      | .returned result =>
+        r.check s!"a connection read fault escapes the first join (returned {repr result})" false
+      | .threw text =>
+        r.check "a connection read fault escapes the first join" (text == want)
+        match ← observeJoin sess with
+        | .returned result =>
+          r.check s!"a second join throws the same connection fault (returned {repr result})" false
+        | .threw text2 =>
+          r.check "a second join throws the same connection fault" (text2 == want)
+      opened := none
+      pure (.ok ())
+  catch e =>
+    pure (.error e)
+  let fault := match outcome with
+    | .error e => some e
+    | .ok () => none
+  cleanup fault opened.toList dialer pair.peer
+
 private def checks (r : Runner) : Async Unit := do
   r.check "Mux.yamux.id is Mux.yamuxId" (decide (yamux.id = yamuxId))
   runRole r 4180 .initiator 1 "an initiator open emits a Yamux SYN for stream 1"
   runRole r 4181 .responder 2 "a responder open emits a Yamux SYN for stream 2"
   runExchange r
+  runLeftover r
+  runProtocol r
+  runOpenAfterClose r
+  runReadFault r
+
+/-- The leftover and the public error boundary. -/
+private def boundary (r : Runner) : Async Unit := do
+  runLeftover r
+  runProtocol r
+  runOpenAfterClose r
+  runReadFault r
 
 /-- The yamux adapter boundary over the sim connection. -/
 def run (r : Runner) : IO Unit := do
   r.section "mux yamux adapter" "packages/libp2p/mux/Libp2p/Mux/Yamux.lean"
   Async.run (checks r)
 
+/-- The leftover and the public error boundary, for a focused run. -/
+def runBoundary (r : Runner) : IO Unit := do
+  r.section "mux yamux adapter errors" "packages/libp2p/mux/Libp2p/Mux/Yamux.lean"
+  Async.run (boundary r)
+
 end Tests.Mux.YamuxAdapter
 
 namespace Tests

From 6ecb901baa509b5848a10a54f9e5471879f04b0c Mon Sep 17 00:00:00 2001
From: Mouzayan Delbourgo <mouzbuilds@gmail.com>
Date: Sun, 8 Nov 2026 19:36:12 -0500
Subject: [PATCH 5/6] docs(mux): record core and yamux integration

---
 packages/libp2p/mux/docs/ARCHITECTURE.md | 158 +++++++++++------------
 packages/libp2p/mux/docs/PLAN.md         | 126 +++++++-----------
 2 files changed, 124 insertions(+), 160 deletions(-)

diff --git a/packages/libp2p/mux/docs/ARCHITECTURE.md b/packages/libp2p/mux/docs/ARCHITECTURE.md
index 44ab9513..36f82da2 100644
--- a/packages/libp2p/mux/docs/ARCHITECTURE.md
+++ b/packages/libp2p/mux/docs/ARCHITECTURE.md
@@ -17,53 +17,81 @@ same node code ran under both muxers in-process and over loopback TCP
 
 | Module | Holds, and why |
 |---|---|
-| `Libp2p/Mux.lean` | the root module. It imports `Constants.lean` and `Test.lean`. The `Test.lean` import loads the session implementation under `Libp2p.Mux.Test` |
-| `Libp2p/Mux/Constants.lean` | `Mux.yamuxId` (`/yamux/1.0.0`), `Mux.mplexId` (`/mplex/6.7.0`), `Mux.testId` (`/leanp2p/test-mux/1.0.0`), and `Mux.mplexMessageCap` (1 MiB); the named ids of §3.4 and the cap of §5.1, one home per fact (§3.8) |
-| `Libp2p/Mux/Yamux.lean` | `Mux.yamux`, the yamux value over the session of `net/yamux`; the `Role` conversion below. Planned |
-| `Libp2p/Mux/Mplex.lean` | the mplex message codec and `Mux.mplex` (P2, §8); the spike reference is `Conn/Mplex.lean` (§10 row 15, §7 row 10). Planned |
-| `Libp2p/Mux/Test.lean` | `Mux.test : Muxer`. Present. `open` calls `Session.start` and lifts the session onto the seam |
-| `Libp2p/Mux/Test/Wire.lean` | the header, frame, and incremental parser. Present. An unsupported implementation detail under `Libp2p.Mux.Test.Wire`. Tests import it directly |
-| `Libp2p/Mux/Test/State.lean` | the pure owner-loop state and its transitions. Present. An unsupported implementation detail under `Libp2p.Mux.Test.State`. A transition returns actions for the runtime shell |
-| `Libp2p/Mux/Test/Session.lean` | the runtime shell, `TestHooks`, and `startWithHooks`. Present. Unsupported implementation and testing details under `Libp2p.Mux.Test.Session`. One reader and one owner loop |
-| `Libp2p/Mux/Mock/Core/ProtocolId.lean` | the temporary `ProtocolId`. Present. `Constants.lean` imports only this module, so the constants stay free of `Conc` and `Streams` |
-| `Libp2p/Mux/Mock/Core.lean` | the temporary `Role`, `Error`, `Muxer`, and `MuxSession` that let W5.4 compile before W5.2. Present. `Test.lean` imports it, so the root loads the seam with `Mux.test` |
-
-The supported names in `Libp2p.Mux` are `Mux.test`, `Mux.testId`,
-and the other constants, together with the `Muxer` and `MuxSession`
-fields. The frame, the parser, the state, and the session shell live
-under `Libp2p.Mux.Test.*`. `Libp2p.Mux` defines no alias for them.
-
-`Libp2p/Mux.lean`, `Libp2p/Mux/Constants.lean`,
-`Libp2p/Mux/Mock/Core/ProtocolId.lean`, `Libp2p/Mux/Mock/Core.lean`,
-`Libp2p/Mux/Test/Wire.lean`, `Libp2p/Mux/Test/State.lean`,
-`Libp2p/Mux/Test/Session.lean`, and `Libp2p/Mux/Test.lean` are in
-the tree. `Yamux.lean` and `Mplex.lean` are the remaining modules
-of this package.
+| `Libp2p/Mux.lean` | the root module. It imports `Constants.lean`, `Yamux.lean`, and `Test.lean` |
+| `Libp2p/Mux/Constants.lean` | `Mux.yamuxId` (`/yamux/1.0.0`), `Mux.mplexId` (`/mplex/6.7.0`), `Mux.testId` (`/leanp2p/test-mux/1.0.0`), and `Mux.mplexMessageCap` (1 MiB). The ids are `Libp2p.Core.ProtocolId` values. One home per fact (§3.4, §3.8) |
+| `Libp2p/Mux/Yamux.lean` | public `Mux.yamux`, the yamux `Muxer` over `Yamux.Session`. The adapter described below |
+| `Libp2p/Mux/Mplex.lean` | the mplex message codec and `Mux.mplex` (P2, §8). Not in the tree. The spike reference is `Conn/Mplex.lean` (§10 row 15, §7 row 10) |
+| `Libp2p/Mux/Test.lean` | public `Mux.test : Muxer`. `open` calls `Session.start` and returns that session on the seam |
+| `Libp2p/Mux/Test/Wire.lean` | the header, frame, and incremental parser. An unsupported implementation detail under `Libp2p.Mux.Test.Wire`. Tests import it directly |
+| `Libp2p/Mux/Test/State.lean` | the pure owner-loop state and its transitions. An unsupported implementation detail under `Libp2p.Mux.Test.State`. A transition returns actions for the runtime shell |
+| `Libp2p/Mux/Test/Session.lean` | the runtime shell, `TestHooks`, and `startWithHooks`. Unsupported implementation and testing details under `Libp2p.Mux.Test.Session`. One reader and one owner loop |
+
+`Libp2p.Core` owns `ProtocolId`, `Core.Error`, `Role`, `Muxer`, and
+`MuxSession`. This package builds values of those seam types.
 
 ## Public surface
 
-- `Mux.yamux : Muxer` carries `id := Mux.yamuxId` and the core seam's
-  `open : Role → Connection → ByteArray → ExceptT Core.Error Async
-  MuxSession` (§4.9; the core pair, public surface). `Yamux.lean`
-  converts `Role` as the decision below records, and the session entry
-  of `net/yamux` then applies that package's parity. The `ByteArray`
-  argument is the negotiation leftover. `open` hands it to the session
-  entry as data, and the session loop turns it into the first `Event`
-  (§4.7).
-- The error mapping happens once, in `Yamux.lean`: the value lifts the
-  session failure into `Core.Error` with one `Except.mapError` (§3.5).
-  The upgrader and the host match on `Core.Error` alone.
-- `Mux.test : Muxer` carries `id := Mux.testId`. `open` calls
+The supported names in `Libp2p.Mux` are the mux values and constants:
+`Mux.yamux`, `Mux.yamuxId`, `Mux.test`, `Mux.testId`, `Mux.mplexId`,
+and `Mux.mplexMessageCap`. Callers use the `Muxer` and `MuxSession`
+operations owned by `Libp2p.Core`: `open`, `openStream`, `accept`,
+`close`, and `join`.
+
+`Libp2p/Mux.lean` imports `Test.lean`. The frame, the parser, the
+state, the session shell, `TestHooks`, and `startWithHooks` then
+load under `Libp2p.Mux.Test.*`. Those declarations stay unsupported.
+`Libp2p.Mux` defines no alias for them.
+
+- `Mux.yamux : Muxer` has `id = Mux.yamuxId`. The yamux value below
+  records how `open` builds the session.
+- `Mux.test : Muxer` has `id = Mux.testId`. `open` calls
   `Test.Session.start` with the role, the connection, and the
-  leftover bytes. `ExceptT.lift` returns that session on the seam.
-  The lift adds no error arm. `openStream` still takes a
-  `ProtocolId`. The private frame does not carry it.
-- `Mux.mplex : Muxer` is the P2 surface: `id := Mux.mplexId`, the pure
+  leftover bytes, and returns that session on the seam. The lift
+  adds no error arm. `openStream` takes a `ProtocolId`. The private
+  frame has no field for it.
+- `Mux.mplex : Muxer` is the P2 surface: `id := Mux.mplexId`, the
   message codec, and a session that keys streams by
-  `(id, initiator)`. The declared message length is capped at
+  `(id, initiator)`. A declared message length is capped at
   `Mux.mplexMessageCap` (§5.1).
-- `MuxSession.openStream` carries a `ProtocolId`; the decisions below
-  record it (the core pair, public surface).
+
+### The yamux value
+
+`open` forwards the `Connection` and the negotiation leftover to
+`Yamux.Session.new`. The session loop takes that leftover as its
+first input (§4.7).
+
+`Core.Role.initiator` selects the Yamux client. That side opens
+stream id `1` first, then the later odd ids. `Core.Role.responder`
+selects the Yamux server. That side opens stream id `2` first, then
+the later even ids. Yamux reserves stream id `0` for session frames.
+An inbound SYN opens a stream when its id has the remote parity.
+
+`openStream` receives a `ProtocolId` and discards it. The Yamux
+stream-open frame has no protocol-id field.
+
+Two returned errors cross this boundary, and each is mapped once.
+`openStream` maps a returned `Streams.Error` through the private
+`mapOpenError`. `closed` and `reset` become `Core.Error.closed`,
+because the call produced no stream. `timeout` becomes
+`Core.Error.timeout`. `join` maps a returned `Yamux.ProtocolError`
+through the private `mapProtocolError` to `Core.Error.protocol`.
+Each detail is `s!"yamux: {repr e}"`. A later read or write on a
+returned stream keeps `Streams.Error`.
+
+A thrown connection `IO.Error` propagates to the caller.
+`mapOpenError` and `mapProtocolError` are private.
+
+Frames, windows, flow control, keepalive, and the session tasks stay
+in `net/yamux`. That package imports no libp2p module.
+
+## Core boundary
+
+`Constants.lean` uses the `ProtocolId` from `Libp2p.Core`. The muxer
+values fill the landed `Muxer` and `MuxSession` seam. Core owns
+`Core.Error` and the public lifecycle. This package owns the
+conversion of returned errors and the construction of the values.
+`net/yamux` stays independent of every libp2p module. The private
+test protocol is a repository muxer on that same seam.
 
 ## Test session
 
@@ -76,27 +104,6 @@ interoperable libp2p protocol. `Mux.test` is not an alias over Yamux.
 Its id is `Mux.testId`, and
 `Mux.testId.toString = "/leanp2p/test-mux/1.0.0"`.
 
-### Boundary
-
-The supported surface is `Mux.test`, `Mux.testId`, and the `Muxer`
-and `MuxSession` fields. `Libp2p/Mux.lean` imports `Test.lean`.
-That import loads the frame, the parser, the state, the session
-shell, `TestHooks`, and `startWithHooks` under `Libp2p.Mux.Test.*`.
-Those declarations are unsupported implementation and testing
-details. `Libp2p.Mux` defines no alias for them.
-
-Temporary W5.2 types live only under `Libp2p/Mux/Mock/`.
-`Mock/Core/ProtocolId.lean` holds `ProtocolId`, and `Constants.lean`
-imports that module alone. `Mock/Core.lean` holds `Role`, `Error`,
-`Muxer`, and `MuxSession`, so this package can compile before W5.2.
-The four error arms are the categories in the core architecture.
-Each arm carries a `String` as a provisional rendered payload.
-`MuxSession.join` is the provisional name of the completion the owner
-joins. W5.2 has not landed these declarations. When it lands, delete
-both mock modules. The imports then move to the `Libp2p.Core` modules
-that own the same names. The private test protocol is not part of
-the mock.
-
 ### Owner-loop state
 
 `Test/State.lean` is the pure state the owner loop steps. It holds
@@ -536,8 +543,9 @@ leaves the session open.
    `ProtocolId` values.
 2. **A seam value holds no protocol decisions** (§3.1). `Mux.yamux`
    moves the role, the connection, and the leftover into the session
-   entry of `net/yamux`, and maps the error back. The frames are that
-   package's business.
+   of `net/yamux`, and maps the returned open and join errors at this
+   boundary. A thrown connection `IO.Error` propagates. The frames
+   are that package's business.
 3. **Lifecycle is part of the seam** (§3.1, §4.1). The `MuxSession`
    each value returns exposes `close : IO Unit` and the session
    completion, and the owner closes and then joins.
@@ -554,12 +562,12 @@ leaves the session open.
    names no stream, and the session keys every stream by
    `(id, initiator)`. The flag bit routes each inbound message to the
    key it names. The spike validated the rule against the go-mplex
-   spec, in-process, and the suite keeps the validation.
+   spec and in-process. The unit 2 suite will keep that validation.
 6. **The 1 MiB cap is checked before allocation** (§5.1,
    PRINCIPLES 2.3). `Mux.mplexMessageCap` names that 1 MiB limit.
    `Constants.lean` owns it, beside the ids. A declared length over
-   the cap is a protocol error, and it tears the session down.
-   `Mux.mplex` rejects that length before allocation.
+   the cap is a protocol error, and it tears the session down. The
+   P2 value `Mux.mplex` will reject that length before allocation.
 
 ## Decisions
 
@@ -569,18 +577,10 @@ leaves the session open.
   at the seam (§9, delta 10). A new muxer lands as a new value, with
   no edit to the upgrader (PRINCIPLES 1.3).
 - **`Libp2p/Mux/Yamux.lean` converts `Role`, and the Yamux session
-  applies parity.** The core pair folded the spike's client and server
-  entries into one `open` field (the core pair, decisions). The
-  adapter then maps the role. `Core.Role.initiator` selects the Yamux
-  client side, which opens odd ids, starting at `1` and advancing by
-  two. `Core.Role.responder` selects the Yamux server side, which
-  opens even ids, starting at `2` and advancing by two. Yamux reserves
-  stream id `0` for session messages. An inbound SYN creates a stream
-  when its id has the remote parity. A SYN whose id has the local
-  parity creates no stream state. `Libp2p/Mux/Yamux.lean` translates
-  `Core.Role` to the side selector that the final W4.3 public API
-  exports. `net/yamux` keeps its own client and server sides and
-  imports no libp2p module.
+  applies parity.** The seam has one `open` field. The adapter maps
+  the role as "The yamux value" records. `net/yamux` keeps its client
+  and server sides and imports no libp2p module. A SYN whose id has
+  the local parity creates no stream state.
 - **`MuxSession.openStream` takes a `ProtocolId`.** The spike's
   `MuxHandle.openStream` took the name, mplex put it in its NewStream
   frame, and the other muxers ignored it (§10 row 12; the core pair,
diff --git a/packages/libp2p/mux/docs/PLAN.md b/packages/libp2p/mux/docs/PLAN.md
index 2502c22b..3ed15015 100644
--- a/packages/libp2p/mux/docs/PLAN.md
+++ b/packages/libp2p/mux/docs/PLAN.md
@@ -12,16 +12,15 @@ the suite passes under `+RTS -N1`, and the import lint is green.
 | Unit | Root deps | Deliverable | Done when |
 |---|---|---|---|
 | 0 | none | this documentation pair, the first work unit of the package (ARCHITECTURE §2) | written, and consistent with the root docs |
-| 1 | W4.3, W5.2 | the yamux `Muxer` value over the W4.3 session: `Mux.yamux` with the `Role` conversion, the constants module, the `Except.mapError` into `Core.Error`, and the independent `Mux.test` session, with its private frame codec and incremental parser. The temporary W5.2 seam mock stays isolated under `Libp2p/Mux/Mock/` and is replaced by `Libp2p.Core` when that package lands | the root W5.4 row holds, and the unit 1 milestones below pass |
+| 1 | W4.3, W5.2 | the P0 delivery: integration with the landed Core seam, `Mux.yamux` over the Yamux session, the independent `Mux.test` session, and the constants and adapter tests | the root W5.4 row and the unit 1 milestones below are satisfied |
 | 2 | W2.1, W5.2, unit 1 | the mplex value (P2, §8): the message codec, `Mux.mplex`, the go-compatible `(id, initiator)` identity, the half-close rules, and the 1 MiB cap | the mplex half of the root W5.4 deliverable holds, and the unit 2 milestones below pass |
 
-Unit 2's deps are the package's own call. The root graph lets mplex
-follow W5.4 at any time, and the mplex core needs the seam (W5.2) and
-no yamux session. Unit 1 comes first because it lays the constants
-module, including `Mux.mplexMessageCap`. Unit 2 checks a declared
-length against that cap.
+Unit 2 depends on W2.1, on the seam from W5.2, and on the constants
+from unit 1, including `Mux.mplexMessageCap`. The root graph lets
+mplex follow W5.4 at any time. Unit 2 checks a declared length
+against that cap.
 
-Unit 0 is done.
+Units 0 and 1 are complete. Unit 2 remains P2.
 
 ## Consumers
 
@@ -38,77 +37,42 @@ Unit 0 is done.
 
 ## Test milestones (unit 1)
 
-- `Mux.yamux` type-checks against the frozen seam of W5.2 with the
-  session of W4.3, with no edit to `core` (the core pair, plan).
-- `open` over a sim `Connection`, in both roles, returns a working
-  `MuxSession`: the test opens a stream, echoes a payload, and closes
-  (PRINCIPLES 1.4).
-- The leftover `ByteArray` reaches the session as its first `Event`:
-  the "negotiation" over-reads one byte, and the byte arrives at the
-  stream layer (§4.7).
-- The id constant carries the wire string:
-  `Mux.yamuxId.toString = "/yamux/1.0.0"`, as a `#guard` the build
-  checks (§3.4).
-- The error path maps once: a hostile frame tears the session down,
-  and the completion reports `Core.Error.protocol` through the single
-  `Except.mapError` (§3.5).
-- The private frame codec and the incremental parser (the
-  architecture, private frame; parser and codec).
-- `Mux.test` is independent of Yamux. The build checks
-  `Mux.test.id = Mux.testId` and
-  `Mux.testId.toString = "/leanp2p/test-mux/1.0.0"` (the architecture,
-  an independent test muxer).
-- The temporary W5.2 seam mock stays isolated, and the package
-  replaces it with `Libp2p.Core` when W5.2 lands (the architecture,
-  boundary).
-- Pure state-transition tests, then deterministic two-ended sim tests
-  (PRINCIPLES 1.4). A demo registry dials itself over the sim pair and
-  serves one handler through the test session (§3.1).
-- Simultaneous opens in both roles, and several concurrent streams
-  (the architecture, stream ids).
-- Ordered writes, multi-frame writes, and an empty write (the
-  architecture, scheduling and writes).
-- Half-close and reset (the architecture, scheduling and writes;
-  stream lifetime).
-- Both directions close, the id leaves the live table, and a read
-  still drains buffered bytes to EOF (the architecture, stream
-  lifetime).
-- A reset retires the id at once (the architecture, stream lifetime).
-- Reset ordering on one stream: queue bytes, reset, read those bytes,
-  then `.error .reset` once, then `.ok none`. New writes fail, and
-  the id is already retired (the architecture, stream lifetime).
-- Data after a received fin, and a duplicate fin, are ignored on a
-  live stream (the architecture, stream lifetime).
-- A remote open refused for capacity consumes that expected id, and
-  the next remote id is accepted (the architecture, stream ids).
-- A local open that waits takes no id (the architecture, stream ids).
-- A blocked read, write, open, and `accept` each wake on shutdown
-  (the architecture, ownership; terminal causes).
-- A writer waiting outside admission wakes on half-close and on
-  shutdown, and completes with the closed stream result (the
-  architecture, scheduling and writes).
-- Malformed header and body cases. Partial input followed by more
-  bytes. Partial input followed by connection end (the architecture,
-  parser and codec).
-- Id parity, strict sequencing, the final valid ids, and exhaustion
-  (the architecture, stream ids).
-- Accept and inbox backpressure (the architecture, accept and
-  backpressure).
-- Owner-close, connection-end, fault, and protocol terminal races
-  (the architecture, terminal causes).
-- Fairness under a large write and under dense inbound frames (the
-  architecture, scheduling and writes).
-- Buffered frames and a multi-frame write make progress while no new
-  event is queued (the architecture, scheduling and writes).
-- Resource checks separate the copied-byte subtotal from retained
-  caller arrays, the `Connection.read` array, and parked callers (the
-  architecture, resources).
-- `Mux.yamux` maps `initiator` to the Yamux client and `responder` to
-  the Yamux server (the architecture, the `Role` decision).
-- The Yamux wire parity cases belong to the `net/yamux` suite (the
-  yamux pair, plan).
-- The ordinary suite and the `+RTS -N1` suite both pass (§6,
-  PRINCIPLES 5.3).
+**Constants.** The suite checks `Mux.yamuxId.toString = "/yamux/1.0.0"`,
+`Mux.mplexId.toString = "/mplex/6.7.0"`,
+`Mux.testId.toString = "/leanp2p/test-mux/1.0.0"`, the pairwise
+distinctness of the three ids, and `Mux.mplexMessageCap = 1 MiB`. It
+checks `Mux.test.id = Mux.testId`.
+
+**Yamux adapter.** The suite checks `Mux.yamux.id = Mux.yamuxId`. An
+initiator open passes an unrelated `ProtocolId` and emits a
+window-update SYN of length 0 for stream id `1`, the Yamux client
+id. A responder open emits that frame for stream id `2`, the Yamux
+server id. The header carries the type, the flags, the stream id,
+and the length. One full-duplex stream through public `Mux.yamux`
+carries a payload in each direction, and both sessions join cleanly.
+A nonempty leftover on the public responder open accepts the remote
+stream and delivers its payload. One malformed header makes `join`
+return `Core.Error.protocol` with detail
+`s!"yamux: {repr Yamux.ProtocolError.malformedHeader}"`. A second
+`join` returns that same error. After a clean close, `openStream`
+returns `Core.Error.closed` with detail
+`s!"yamux: {repr Streams.Error.closed}"`. A thrown connection
+`IO.Error` leaves the first `join` and the second `join` as that
+same thrown error.
+
+**Yamux session.** Framing, flow control, reset, half-close, hostile
+frames, and keepalive stay in the `net/yamux` suite.
+
+**Test muxer.** `Mux.test` is independent of Yamux. The suite covers
+its lifecycle and hostile input: the private frame codec, the
+incremental parser, the pure state transitions, and deterministic
+two-ended sim tests. Those tests cover stream ids, simultaneous
+opens, ordered and empty writes, half-close, reset, stream lifetime,
+accept and inbox backpressure, terminal races, fairness, and the
+copied-byte accounting.
+
+**Runtime.** CI runs both the ordinary and `+RTS -N1` suites; both
+are required acceptance gates (§6, PRINCIPLES 5.3).
 
 ## Test milestones (unit 2)
 
@@ -141,9 +105,9 @@ Unit 0 is done.
 branch holds no mplex or yamux file; no muxer wire transcript was
 captured. The yamux session carries its own suite in `net/yamux`: the
 fixed header bytes, the hostile frames, and the flow-control cases
-(the yamux pair, plan). This package pins the seam adaptation: the sim
-exchanges of unit 1 through `Mux.yamux` and the test value, and the
-identity and half-close cases of unit 2 through `Mux.mplex`. The live
+(the yamux pair, plan). This package pins the unit 1 seam
+adaptation through `Mux.yamux` and `Mux.test`. Unit 2 will pin the
+mplex identity and half-close cases through `Mux.mplex`. The live
 gate is the go-libp2p interop matrix at W5.9 over `tcp + /noise +
 yamux` (root PLAN W5.9); the spike proved that path once, and W5.9
 re-runs it against this implementation. The same-node-code-under-both

From c5d63d33fa5809112ee0458cd28c4808dbc5d29f Mon Sep 17 00:00:00 2001
From: Leo Lara <leo@leolara.me>
Date: Mon, 9 Nov 2026 09:28:54 +0700
Subject: [PATCH 6/6] test(mux): drop the uncalled focused-run entry

Nothing calls runBoundary, and no suite-selection mechanism exists.
The checks of the focused entry already run in the suite entry.
---
 Tests/Mux.lean | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/Tests/Mux.lean b/Tests/Mux.lean
index e2b8ae54..e871fde0 100644
--- a/Tests/Mux.lean
+++ b/Tests/Mux.lean
@@ -4168,23 +4168,11 @@ private def checks (r : Runner) : Async Unit := do
   runOpenAfterClose r
   runReadFault r
 
-/-- The leftover and the public error boundary. -/
-private def boundary (r : Runner) : Async Unit := do
-  runLeftover r
-  runProtocol r
-  runOpenAfterClose r
-  runReadFault r
-
 /-- The yamux adapter boundary over the sim connection. -/
 def run (r : Runner) : IO Unit := do
   r.section "mux yamux adapter" "packages/libp2p/mux/Libp2p/Mux/Yamux.lean"
   Async.run (checks r)
 
-/-- The leftover and the public error boundary, for a focused run. -/
-def runBoundary (r : Runner) : IO Unit := do
-  r.section "mux yamux adapter errors" "packages/libp2p/mux/Libp2p/Mux/Yamux.lean"
-  Async.run (boundary r)
-
 end Tests.Mux.YamuxAdapter
 
 namespace Tests