From 8f395b3af3b0d0ebdad2953377983abf36bd0300 Mon Sep 17 00:00:00 2001
From: Ivan Anishchuk <ivan@agorism.org>
Date: Sun, 8 Nov 2026 14:11:42 +0530
Subject: [PATCH] refactor(negotiate): run the upgrader over the seam types of
 libp2p/core

W5.2 merged, so the package drops Negotiate.Mock.Core and takes
ProtocolId, Role, Error, SecureConn, SecurityProtocol, MuxSession, and
Muxer from Libp2p.Core.

Two seam rules of the real core change the upgrader. The secure read
delivers the bytes the handshake over-read, so the muxer negotiation
starts with no seed; SecureConn.leftover only records them. The
upgrader owns the SecureConn and must join it. The answered session's
join now waits for the session loop, then for the secure connection.
Every failure after the handshake closes and joins the secure
connection, and a session that opens as the deadline fires is closed
and joined before the call answers.

The suite's plaintext security value delivers its over-read bytes
through its read, as the real seam does, and the pipeline checks join
both sessions.

Closes #53
---
 Tests/Negotiate.lean                          |  12 +-
 Tests/Upgrade.lean                            | 150 ++++++++++--------
 .../libp2p/negotiate/Libp2p/Negotiate.lean    |   6 +-
 .../negotiate/Libp2p/Negotiate/Constants.lean |   7 +-
 .../negotiate/Libp2p/Negotiate/Message.lean   |  22 +--
 .../negotiate/Libp2p/Negotiate/Mock/Core.lean |  87 ----------
 .../negotiate/Libp2p/Negotiate/Step.lean      |  61 +++----
 .../negotiate/Libp2p/Negotiate/Upgrade.lean   | 133 ++++++++++------
 .../libp2p/negotiate/docs/ARCHITECTURE.md     |  16 +-
 9 files changed, 237 insertions(+), 257 deletions(-)
 delete mode 100644 packages/libp2p/negotiate/Libp2p/Negotiate/Mock/Core.lean

diff --git a/Tests/Negotiate.lean b/Tests/Negotiate.lean
index 278caee0..85a731dc 100644
--- a/Tests/Negotiate.lean
+++ b/Tests/Negotiate.lean
@@ -40,13 +40,13 @@ private def writesOf (actions : List Action) : List (List Nat) :=
     | .select .. => none
 
 /-- The selects of an action list, in order. -/
-private def selectsOf (actions : List Action) : List (Mock.Core.ProtocolId × List Nat) :=
+private def selectsOf (actions : List Action) : List (Libp2p.Core.ProtocolId × List Nat) :=
   actions.filterMap fun
     | .select p r => some (p, r)
     | .write _ => none
 
 /-- The responder's initial state. -/
-private def responderState (supported : List Mock.Core.ProtocolId) : State :=
+private def responderState (supported : List Libp2p.Core.ProtocolId) : State :=
   { role := .responder, supported := supported, proposals := [], buffer := [], phase := .headerPending }
 
 /-- The initiator's initial state. -/
@@ -136,7 +136,7 @@ def run (r : Runner) : IO Unit := do
   let protos ← Tests.jStrs "mss-ls.json" reply "protocols"
   let bodyHex ← Tests.jStr "mss-ls.json" reply "bodyHex"
   let bodyBytes ← hexOf bodyHex
-  let ids : List Mock.Core.ProtocolId := protos.map fun s => ⟨s⟩
+  let ids : List Libp2p.Core.ProtocolId := protos.map fun s => ⟨s⟩
   r.check "mss ls body encode" (lsBody ids == bodyBytes)
   r.check "mss ls reply encode"
     (encodeLs ids == Varint.encode (boundedVarint bodyBytes.length) ++ bodyBytes)
@@ -158,8 +158,8 @@ def run (r : Runner) : IO Unit := do
   let (i2rN, r2iN) ← traceHexes "mss-go-trace.json" naTrace
   let lazyTrace ← Tests.jArr "mss-go-trace.json" goj "lazyTrace"
   let (i2rL, r2iL) ← traceHexes "mss-go-trace.json" lazyTrace
-  let kadId : Mock.Core.ProtocolId := ⟨"/ipfs/kad/1.0.0"⟩
-  let nopeId : Mock.Core.ProtocolId := ⟨"/nope/9.9.9"⟩
+  let kadId : Libp2p.Core.ProtocolId := ⟨"/ipfs/kad/1.0.0"⟩
+  let nopeId : Libp2p.Core.ProtocolId := ⟨"/nope/9.9.9"⟩
 
   match replay (responderState [kadId]) (← i2rF.mapM hexOf) with
   | .error _ => r.check "mss go full trace" false
@@ -206,7 +206,7 @@ def run (r : Runner) : IO Unit := do
       r.check "mss step responder unknown id writes na and stays negotiating"
         (s'.phase = .negotiating ∧ actions == [.write (encodeMsg (Reply.toMsg .na))])
 
-  let sup : List Mock.Core.ProtocolId := [⟨"/ipfs/kad/1.0.0"⟩, ⟨"/ipfs/id/1.0.0"⟩]
+  let sup : List Libp2p.Core.ProtocolId := [⟨"/ipfs/kad/1.0.0"⟩, ⟨"/ipfs/id/1.0.0"⟩]
   let sSup : State := { role := .responder, supported := sup, proposals := [], buffer := [], phase := .negotiating }
   match step sSup (.bytes (encodeText "ls")) with
   | .error _ => r.check "mss step responder ls writes ls reply and stays negotiating" false
diff --git a/Tests/Upgrade.lean b/Tests/Upgrade.lean
index 0754181f..145b6b33 100644
--- a/Tests/Upgrade.lean
+++ b/Tests/Upgrade.lean
@@ -17,8 +17,8 @@ The test milestones of the negotiate package plan, unit 1b. The full
 pipeline runs both directions over an in-process pipe pair, and the
 byte-split runs use the in-memory sim transport of `Streams.Sim`. The
 fixed-key plaintext security value and the minimal muxer value replace
-the Noise and yamux milestones (#16 merged, #17 open; the matrix check
-names the live gate). The deadline check
+the Noise and yamux milestones, so the suite runs no crypto and no
+session loop (the matrix check names the live gate). The deadline check
 advances the test `Clock` of `base/conc`, so the suite waits on no wall
 clock.
 
@@ -102,15 +102,33 @@ private def dialerId : Libp2p.Identity.PeerId := peerOf 1
 /-- The fixed peer id of the listening side. -/
 private def listenerId : Libp2p.Identity.PeerId := peerOf 2
 
+/-- The secure connection of a test handshake: `conn`, whose `read`
+delivers `front` before any connection byte, as the core seam asks of a
+`SecureConn` (the core pair, "The leftover hand-over"). `leftover`
+records the same bytes. The plaintext handshake starts no task, so the
+join answers at once. -/
+private def secureOf (conn : Streams.Connection) (front : ByteArray)
+    (localPeer remotePeer : Libp2p.Identity.PeerId) : BaseIO Libp2p.Core.SecureConn := do
+  let pending ← Conc.OnceRef.new front
+  return {
+    conn with
+    read := do
+      -- Hand out the front once; every later read goes to the connection.
+      let b ← (pending.updateGet fun b => (b, ByteArray.empty) : BaseIO ByteArray)
+      if b.isEmpty then conn.read else return some b
+    localPeer, remotePeer
+    leftover := front
+    join := pure () }
+
 /-- The fixed-key plaintext test security value. It replaces the Noise
-milestone (#16, merged; the real value joins when the core mock drops).
-The handshake writes its marker, reads the
+milestone, since the suite needs a handshake with no crypto in the
+loop. The handshake writes its marker, reads the
 peer's marker from the seed first and then from the connection, and
 hands the unconsumed bytes to the next stage. `overread` adds one read
 whose chunk joins the leftover, so a check can force the hand-over.
 `seedRef` records the seed the negotiation handed over. -/
 private def secValue (overread : Bool) (seedRef : Conc.OnceRef (Option ByteArray)) :
-    Mock.Core.SecurityProtocol where
+    Libp2p.Core.SecurityProtocol where
   id := ⟨"/test/plain/1.0.0"⟩
   handshake := fun role conn seed => do
     seedRef.set (some seed)
@@ -133,25 +151,23 @@ private def secValue (overread : Bool) (seedRef : Conc.OnceRef (Option ByteArray
         | none => throw (.closed "test handshake over-read found the connection closed")
         | some chunk => pure chunk
       else pure ByteArray.empty
-    return { conn := conn,
-             localPeer := if role = .initiator then dialerId else listenerId,
-             remotePeer := if role = .initiator then listenerId else dialerId,
-             leftover := rest ++ over,
-             close := Streams.Connection.closeQuietly conn }
+    secureOf conn (rest ++ over)
+      (if role = .initiator then dialerId else listenerId)
+      (if role = .initiator then listenerId else dialerId)
 
 /-- The test muxer value. It replaces the yamux milestone (#17,
 unmerged). `open` records its leftover argument, the opened id, and a
 ran flag in shared cells, and returns a no-op session. -/
-private def muxValue (id : Mock.Core.ProtocolId) (ranRef : Conc.OnceRef Bool)
+private def muxValue (id : Libp2p.Core.ProtocolId) (ranRef : Conc.OnceRef Bool)
     (leftRef : Conc.OnceRef (Option ByteArray))
-    (openRef : Conc.OnceRef (Option Mock.Core.ProtocolId)) : Mock.Core.Muxer where
+    (openRef : Conc.OnceRef (Option Libp2p.Core.ProtocolId)) : Libp2p.Core.Muxer where
   id := id
   «open» := fun _ _ leftover => do
     ranRef.set true
     leftRef.set (some leftover)
     openRef.set (some id)
-    return { openStream := (throw (.protocol "the test session opens no stream") :
-                ExceptT Mock.Core.Error Conc.Async Streams.Stream),
+    return { openStream := fun _ => (throw (.protocol "the test session opens no stream") :
+                ExceptT Libp2p.Core.Error Conc.Async Streams.Stream),
              accept := pure none,
              close := pure (),
              join := pure () }
@@ -196,7 +212,7 @@ private def recordWrites (conn : Streams.Connection) (ref : Conc.OnceRef (List B
 
 /-- The answer of one upgrade run. -/
 private abbrev UpAnswer :=
-  Option (Except Mock.Core.Error (Mock.Core.MuxSession × Libp2p.Identity.PeerId))
+  Option (Except Libp2p.Core.Error (Libp2p.Core.MuxSession × Libp2p.Identity.PeerId))
 
 /-! ## The pipeline checks -/
 
@@ -205,15 +221,15 @@ assertion. The test security value carries no advertisement
 field, so the wire exchange alone selects the muxer. -/
 private def checkFullPipeline (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let dSeed : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lSeed : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let dRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
-  let dOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
-  let lOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let dOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
+  let lOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let lAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let tasks ← Conc.TaskSet.new
@@ -230,8 +246,9 @@ private def checkFullPipeline (r : Runner) : Async Unit := do
   | some (.ok (ds, dp)), some (.ok (ls, lp)) => do
       ds.close
       ls.close
-      ds.join
-      ls.join
+      let dj ← ds.join.run
+      let lj ← ls.join.run
+      r.check "upgrade sessions join cleanly" (dj matches .ok () && lj matches .ok ())
       r.check "upgrade full pipeline dial and listen"
         (dp == listenerId && lp == dialerId)
       r.check "upgrade muxer selected on the wire"
@@ -251,7 +268,7 @@ responder's negotiation over-reads the marker and hands it to the
 handshake. -/
 private def checkNegotiationLeftover (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let count : Conc.OnceRef Nat ← Conc.OnceRef.new 0
   let dSeed : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lSeed : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
@@ -259,8 +276,8 @@ private def checkNegotiationLeftover (r : Runner) : Async Unit := do
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
-  let dOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
-  let lOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let dOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
+  let lOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let lAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let tasks ← Conc.TaskSet.new
@@ -283,17 +300,18 @@ private def checkNegotiationLeftover (r : Runner) : Async Unit := do
   (← sideConn iside).close
   (← sideConn rside).close
 
-/-- The handshake over-reads the muxer header chunk, and the muxer
-stage still selects from the `SecureConn` leftover. -/
+/-- The handshake over-reads the muxer header chunk. The secure `read`
+delivers it first, so the muxer stage still selects, and `Muxer.open`
+gets no bytes. -/
 private def checkHandshakeLeftover (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let dRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
-  let dOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
-  let lOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let dOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
+  let lOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let lAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let tasks ← Conc.TaskSet.new
@@ -321,15 +339,15 @@ private def checkHandshakeLeftover (r : Runner) : Async Unit := do
 `Muxer.open` as its `ByteArray` argument. -/
 private def checkMuxOpenLeftover (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let extra := Bytes.ofNatList [9, 9, 9]
   let count : Conc.OnceRef Nat ← Conc.OnceRef.new 0
   let dRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
-  let dOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
-  let lOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let dOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
+  let lOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let lAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let tasks ← Conc.TaskSet.new
@@ -356,14 +374,14 @@ private def checkMuxOpenLeftover (r : Runner) : Async Unit := do
 supports only the second, and the chosen session is the second id. -/
 private def checkNaRetry (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxA : Mock.Core.ProtocolId := ⟨"/test/mux/a"⟩
-  let muxB : Mock.Core.ProtocolId := ⟨"/test/mux/b"⟩
+  let muxA : Libp2p.Core.ProtocolId := ⟨"/test/mux/a"⟩
+  let muxB : Libp2p.Core.ProtocolId := ⟨"/test/mux/b"⟩
   let aRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
-  let aOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let aOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let bRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
-  let bOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let bOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
-  let lOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let lOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let lWrites : Conc.OnceRef (List ByteArray) ← Conc.OnceRef.new []
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let lAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
@@ -400,7 +418,7 @@ parked negotiation with `closed`. -/
 private def checkIdentityMismatch (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
   let wrongId : Libp2p.Identity.PeerId := peerOf 3
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let dRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
@@ -432,7 +450,7 @@ connection, and the parked read ends on its own. -/
 private def checkDeadline (r : Runner) : Async Unit := do
   let tc ← Conc.TestClock.new
   let (sc, farPipe) ← silentPeer
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let answer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let tasks ← Conc.TaskSet.new
   tasks.spawn do
@@ -475,7 +493,7 @@ private def checkEmptySecurity (r : Runner) : Async Unit := do
 propose fails, and the teardown close reaches the responder. -/
 private def checkEmptyMuxer (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxB : Mock.Core.ProtocolId := ⟨"/test/mux/b"⟩
+  let muxB : Libp2p.Core.ProtocolId := ⟨"/test/mux/b"⟩
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let lAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
@@ -508,7 +526,7 @@ private def checkEmptyMuxer (r : Runner) : Async Unit := do
 private def checkEof (r : Runner) : Async Unit := do
   let tc ← Conc.TestClock.new
   let (iside, rside) ← newPair
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let answer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let tasks ← Conc.TaskSet.new
   tasks.spawn do
@@ -528,8 +546,8 @@ private def checkEof (r : Runner) : Async Unit := do
 list and the `negotiationFailed` maps to `protocol`. -/
 private def checkExhausted (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxA : Mock.Core.ProtocolId := ⟨"/test/mux/a"⟩
-  let muxB : Mock.Core.ProtocolId := ⟨"/test/mux/b"⟩
+  let muxA : Libp2p.Core.ProtocolId := ⟨"/test/mux/a"⟩
+  let muxB : Libp2p.Core.ProtocolId := ⟨"/test/mux/b"⟩
   let dRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
@@ -564,7 +582,7 @@ private def checkExhausted (r : Runner) : Async Unit := do
 teardown close reaches the peer. -/
 private def checkHostile (r : Runner) : Async Unit := do
   let (iside, rside) ← newPair
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let garbage := Bytes.ofNatList (List.replicate 9 255)
   let count : Conc.OnceRef Nat ← Conc.OnceRef.new 0
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
@@ -616,7 +634,7 @@ private def traceHexes (file : String) (trace : List Json) : IO (List String ×
 writes equal the recorded `r2i` bytes, byte for byte. -/
 private def checkGoTraces (r : Runner) : Async Unit := do
   let goj ← Tests.loadJson "mss-go-trace.json"
-  let kadId : Mock.Core.ProtocolId := ⟨"/ipfs/kad/1.0.0"⟩
+  let kadId : Libp2p.Core.ProtocolId := ⟨"/ipfs/kad/1.0.0"⟩
   let fullTrace ← Tests.jArr "mss-go-trace.json" goj "fullTrace"
   let (i2rF, r2iF) ← traceHexes "mss-go-trace.json" fullTrace
   let rs : State := { role := .responder, supported := [kadId], proposals := [],
@@ -653,7 +671,7 @@ private def checkGoTraces (r : Runner) : Async Unit := do
 /-! ## The send-side cap -/
 
 /-- A protocol id whose frame is over the 1 KiB cap. -/
-private def overCapId : Mock.Core.ProtocolId :=
+private def overCapId : Libp2p.Core.ProtocolId :=
   ⟨String.ofList (List.replicate 1100 'a')⟩
 
 /-- A configured id that would produce an over-cap frame is refused before
@@ -668,14 +686,14 @@ private def checkSendCap (r : Runner) : Async Unit := do
      | .error .negotiationFailed => true
      | _ => false)
   r.check "negotiate send cap admits a normal id"
-    (match initiatorStart [Mock.Core.ProtocolId.mk "/ipfs/kad/1.0.0"] with
+    (match initiatorStart [Libp2p.Core.ProtocolId.mk "/ipfs/kad/1.0.0"] with
      | .ok _ => true
      | _ => false)
 
 /-- The responder writes its header before it reads anything, so a dialer
 that also waits does not stall. -/
 private def checkResponderFirst (r : Runner) : Async Unit := do
-  match responderStart [Mock.Core.ProtocolId.mk "/ipfs/kad/1.0.0"] with
+  match responderStart [Libp2p.Core.ProtocolId.mk "/ipfs/kad/1.0.0"] with
   | .ok (s, ws) =>
       r.check "negotiate responder sends its header first"
         (ws == [encodeMsg header] && s.phase = .negotiating)
@@ -722,11 +740,10 @@ private def readExactly (conn : Streams.Connection) (seed : ByteArray) (n : Nat)
 
 /-- The fixed-key test handshake, chunk-agnostic: it reads its marker
 with `readExactly`, so it accepts whatever chunks the transport chose.
-It replaces the Noise milestone (#16, merged; the real value joins
-when the core mock drops) as `secValue` does, and
+It replaces the Noise milestone as `secValue` does, and
 it exists so the pipeline can run over the splitting sim. -/
 private def secValueExact (seedRef : Conc.OnceRef (Option ByteArray)) :
-    Mock.Core.SecurityProtocol where
+    Libp2p.Core.SecurityProtocol where
   id := ⟨"/test/plain/1.0.0"⟩
   handshake := fun role conn seed => do
     seedRef.set (some seed)
@@ -739,29 +756,27 @@ private def secValueExact (seedRef : Conc.OnceRef (Option ByteArray)) :
     match ← readExactly conn seed 4 with
     | none => throw (.closed "test handshake read ended before the marker")
     | some four =>
-      return { conn := conn,
-               localPeer := if role = .initiator then dialerId else listenerId,
-               remotePeer := if role = .initiator then listenerId else dialerId,
-               leftover := Bytes.ofNatList (four.drop 4),
-               close := Streams.Connection.closeQuietly conn }
+      secureOf conn (Bytes.ofNatList (four.drop 4))
+        (if role = .initiator then dialerId else listenerId)
+        (if role = .initiator then listenerId else dialerId)
 
 /-- The multistream exchange of both roles over a splitting sim, for a
 supported id and for the `na` retry. Each run also asserts that the
 responder's reader saw one byte per chunk, which shows the sim split the
 writes. -/
 private def checkSplitNegotiate (r : Runner) : Async Unit := do
-  let kadId : Mock.Core.ProtocolId := ⟨"/ipfs/kad/1.0.0"⟩
-  let idId : Mock.Core.ProtocolId := ⟨"/ipfs/id/1.0.0"⟩
-  let runOne (name : String) (iIds rIds : List Mock.Core.ProtocolId)
-      (expect : Mock.Core.ProtocolId) : Async Unit := do
+  let kadId : Libp2p.Core.ProtocolId := ⟨"/ipfs/kad/1.0.0"⟩
+  let idId : Libp2p.Core.ProtocolId := ⟨"/ipfs/id/1.0.0"⟩
+  let runOne (name : String) (iIds rIds : List Libp2p.Core.ProtocolId)
+      (expect : Libp2p.Core.ProtocolId) : Async Unit := do
     let (ic, rc) ← simPair true
     let sizes : Conc.OnceRef (List Nat) ← Conc.OnceRef.new []
     let split := recordReadSizes rc sizes
     let iReader := Streams.BufReader.new ic
     let rReader := Streams.BufReader.new split
-    let iAnswer : Conc.OnceRef (Option (Except Mock.Core.Error StageResult)) ←
+    let iAnswer : Conc.OnceRef (Option (Except Libp2p.Core.Error StageResult)) ←
       Conc.OnceRef.new none
-    let rAnswer : Conc.OnceRef (Option (Except Mock.Core.Error StageResult)) ←
+    let rAnswer : Conc.OnceRef (Option (Except Libp2p.Core.Error StageResult)) ←
       Conc.OnceRef.new none
     let tasks ← Conc.TaskSet.new
     tasks.spawn do
@@ -789,15 +804,15 @@ and the open. This is the two-party run that the definition of done of
 #18 requires. -/
 private def checkSplitPipeline (r : Runner) : Async Unit := do
   let (ic, rc) ← simPair true
-  let muxId : Mock.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
+  let muxId : Libp2p.Core.ProtocolId := ⟨"/test/mux/1.0.0"⟩
   let dSeed : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lSeed : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let dRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let lRan : Conc.OnceRef Bool ← Conc.OnceRef.new false
   let dLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
   let lLeft : Conc.OnceRef (Option ByteArray) ← Conc.OnceRef.new none
-  let dOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
-  let lOpen : Conc.OnceRef (Option Mock.Core.ProtocolId) ← Conc.OnceRef.new none
+  let dOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
+  let lOpen : Conc.OnceRef (Option Libp2p.Core.ProtocolId) ← Conc.OnceRef.new none
   let dAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let lAnswer : Conc.OnceRef UpAnswer ← Conc.OnceRef.new none
   let tasks ← Conc.TaskSet.new
@@ -814,8 +829,9 @@ private def checkSplitPipeline (r : Runner) : Async Unit := do
   | some (.ok (ds, dp)), some (.ok (ls, lp)) => do
       ds.close
       ls.close
-      ds.join
-      ls.join
+      let dj ← ds.join.run
+      let lj ← ls.join.run
+      r.check "split sim upgrade sessions join cleanly" (dj matches .ok () && lj matches .ok ())
       r.check "split sim upgrade pipeline, dial and listen"
         (dp == listenerId && lp == dialerId)
       r.check "split sim upgrade selects the muxer on the wire"
@@ -852,6 +868,6 @@ def run (r : Runner) : IO Unit := do
     checkSplitPipeline r
   Conc.Async.run all
   r.skip "upgrade noise yamux matrix over tcp"
-    "needs the core swap, which frees the merged Noise value, and the muxer value of #17 (the W5.9 live gate)"
+    "needs the Noise value on the real core (#76) and the yamux muxer value (#77) (the W5.9 live gate)"
 
 end Tests.Upgrade
diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate.lean b/packages/libp2p/negotiate/Libp2p/Negotiate.lean
index 25f5d964..8fc6fa2d 100644
--- a/packages/libp2p/negotiate/Libp2p/Negotiate.lean
+++ b/packages/libp2p/negotiate/Libp2p/Negotiate.lean
@@ -7,7 +7,7 @@ import Libp2p.Negotiate.Upgrade
 # Libp2p.Negotiate
 
 The negotiate subpackage: multistream-select 1.0.0 and the upgrader
-(ARCHITECTURE §4.9). One import line per public submodule. The root
-names no Mock module directly. Its submodules still expose `Mock.Core`
-until W5.2 lands. The identity field types name `Libp2p.Identity`.
+(ARCHITECTURE §4.9). One import line per public submodule. The seam
+types come from `Libp2p.Core`, and the identity field types name
+`Libp2p.Identity`.
 -/
diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Constants.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Constants.lean
index e1659d4e..0d5eaf40 100644
--- a/packages/libp2p/negotiate/Libp2p/Negotiate/Constants.lean
+++ b/packages/libp2p/negotiate/Libp2p/Negotiate/Constants.lean
@@ -1,11 +1,10 @@
-import Libp2p.Negotiate.Mock.Core
+import Libp2p.Core.ProtocolId
 
 /-!
 # The constants of the negotiation
 
 One home per fact (root §3.8). The multistream protocol id and the
-1 KiB message cap live only here. At W5.2 integration the `Mock.Core`
-import swaps to `Libp2p.Core`, and the literal stays.
+1 KiB message cap live only here.
 -/
 
 set_option autoImplicit false
@@ -14,7 +13,7 @@ namespace Libp2p.Negotiate
 
 /-- The multistream 1.0.0 protocol id. The only protocol id literal of
 the package (root §3.4). -/
-def protocolId : Mock.Core.ProtocolId := ⟨"/multistream/1.0.0"⟩
+def protocolId : Core.ProtocolId := ⟨"/multistream/1.0.0"⟩
 
 /-- The 1 KiB multistream cap (root §5.1, contract 1 of the package
 docs). -/
diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Message.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Message.lean
index e70f841d..ce8f45d5 100644
--- a/packages/libp2p/negotiate/Libp2p/Negotiate/Message.lean
+++ b/packages/libp2p/negotiate/Libp2p/Negotiate/Message.lean
@@ -283,16 +283,16 @@ theorem encodeMsgLength (m : Msg) :
 
 /-- One `ls` entry is an ordinary message frame: the entry's text is
 the protocol id, and the frame carries the id plus its newline. -/
-def lsEntries (ids : List Mock.Core.ProtocolId) : List Nat :=
+def lsEntries (ids : List Core.ProtocolId) : List Nat :=
   (ids.map (fun p => encodeText p.toString)).flatten
 
 /-- The body of an `ls` reply: one entry frame per id, then the final
 newline byte that ends the list. -/
-def lsBody (ids : List Mock.Core.ProtocolId) : List Nat := lsEntries ids ++ [10]
+def lsBody (ids : List Core.ProtocolId) : List Nat := lsEntries ids ++ [10]
 
 /-- The full `ls` reply: the body wrapped in one uvarint length
 prefix, exactly like a message. -/
-def encodeLs (ids : List Mock.Core.ProtocolId) : List Nat :=
+def encodeLs (ids : List Core.ProtocolId) : List Nat :=
   Varint.encode (boundedVarint (lsBody ids).length) ++ lsBody ids
 
 /-- Walk the entries of one complete `ls` body. The fuel counts
@@ -300,7 +300,7 @@ entries; the caller passes the body's byte length, which is at least
 the entry count because every entry carries its newline. `[10]` alone
 is the terminator, not a leading byte: a leading `0x0A` can be a
 legitimate one-byte prefix for a nine-byte id. -/
-def decodeEntries : Nat → List Nat → Except DecodeError (List Mock.Core.ProtocolId)
+def decodeEntries : Nat → List Nat → Except DecodeError (List Core.ProtocolId)
   | 0, _ => .error .malformed
   | fuel + 1, bs =>
     if bs = [10] then .ok []
@@ -313,7 +313,7 @@ same split and cap as a message. An entry that ends mid-body is
 malformed, because only the outer prefix and length can be completed
 by more bytes. -/
 def decodeLs? (bs : List Nat) :
-    Except DecodeError (List Mock.Core.ProtocolId × List Nat) :=
+    Except DecodeError (List Core.ProtocolId × List Nat) :=
   match splitFrame bs with
   | .error e => .error e
   | .ok (body, rest) => (decodeEntries body.length body).map (·, rest)
@@ -324,7 +324,7 @@ theorem encodeTextLength (s : String) : (payloadOf s).length ≤ (encodeText s).
 
 /-- The entries of an encoded list read back in order, under fuel and
 cap bounds. -/
-theorem decodeEntriesLs (ids : List Mock.Core.ProtocolId) (fuel : Nat)
+theorem decodeEntriesLs (ids : List Core.ProtocolId) (fuel : Nat)
     (hf : ids.length < fuel) (hb : (lsEntries ids).length ≤ maxMsg) :
     decodeEntries fuel (lsEntries ids ++ [10]) = .ok ids := by
   induction ids generalizing fuel with
@@ -354,13 +354,13 @@ theorem decodeEntriesLs (ids : List Mock.Core.ProtocolId) (fuel : Nat)
         simp [lsEntries]
       simp only [decodeEntries, hne, ite_false]
       rw [hsplit, decodeMsgSuffix ⟨p.toString, hfit⟩ (lsEntries ps ++ [10])]
-      change (Except.map (fun x => (⟨p.toString⟩ : Mock.Core.ProtocolId) :: x)
+      change (Except.map (fun x => (⟨p.toString⟩ : Core.ProtocolId) :: x)
         (decodeEntries f (lsEntries ps ++ [10])) = .ok (p :: ps))
       rw [ih f (by simp at hf; omega) (by omega)]
       rfl
 
 /-- The byte length of the entries is at least the id count. -/
-theorem lsEntriesLength (ids : List Mock.Core.ProtocolId) :
+theorem lsEntriesLength (ids : List Core.ProtocolId) :
     ids.length ≤ (lsEntries ids).length := by
   induction ids with
   | nil => simp [lsEntries]
@@ -371,7 +371,7 @@ theorem lsEntriesLength (ids : List Mock.Core.ProtocolId) :
 
 /-- The `ls` reply round trip. The length prefix alone delimits the
 entries, so no cleanliness hypothesis is needed. -/
-theorem decodeLsEncodeLs (ids : List Mock.Core.ProtocolId)
+theorem decodeLsEncodeLs (ids : List Core.ProtocolId)
     (hbody : (lsBody ids).length ≤ maxMsg) :
     decodeLs? (encodeLs ids) = .ok (ids, []) := by
   have hlim : (lsBody ids).length < Varint.limit := by
@@ -414,7 +414,7 @@ theorem splitFrameInv {bs body rest : List Nat} (h : splitFrame bs = .ok (body,
     exact hbs.symm
 
 /-- Entries that read back are exactly the encoding of the list. -/
-theorem decodeEntriesInv (f : Nat) (bs : List Nat) (ids : List Mock.Core.ProtocolId)
+theorem decodeEntriesInv (f : Nat) (bs : List Nat) (ids : List Core.ProtocolId)
     (h : decodeEntries f bs = .ok ids) : lsEntries ids ++ [10] = bs := by
   induction f generalizing bs ids with
   | zero => simp [decodeEntries] at h
@@ -441,7 +441,7 @@ theorem decodeEntriesInv (f : Nat) (bs : List Nat) (ids : List Mock.Core.Protoco
 
 /-- The all-input inverse of the `ls` reply: every accepted input is
 the encoding of the decoded list. -/
-theorem decodeLsInv {bs : List Nat} {ids : List Mock.Core.ProtocolId} {rest : List Nat}
+theorem decodeLsInv {bs : List Nat} {ids : List Core.ProtocolId} {rest : List Nat}
     (h : decodeLs? bs = .ok (ids, rest)) : encodeLs ids ++ rest = bs := by
   unfold decodeLs? at h
   split at h
diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Mock/Core.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Mock/Core.lean
deleted file mode 100644
index f18ddd1f..00000000
--- a/packages/libp2p/negotiate/Libp2p/Negotiate/Mock/Core.lean
+++ /dev/null
@@ -1,87 +0,0 @@
-import Std
-import Conc
-import Streams.Conn
-import Streams.Stream
-import Libp2p.Identity
-
-/-!
-# Core mocks for units 1a and 1b
-
-`ProtocolId` and `Role` live in `libp2p/core` (W5.2, not merged yet).
-Unit 1b adds `Error`, `SecurityProtocol`, `SecureConn`, `Muxer`, and
-`MuxSession`. This module follows the core ARCHITECTURE "Public
-surface", so the negotiate core and the upgrader compile against the
-frozen shapes. It differs in three places: `Repr` is derived,
-`MuxSession.close` is `BaseIO Unit`, and `SecureConn` has no completion
-to join. The import swaps to `Libp2p.Core` when W5.2 lands. `Repr`
-joins the derived classes per root §3.2, so `State`, `Event`, and
-`Action` can derive `Repr` per root §3.3.
-
-`SecurityProtocol` and `Muxer` mention the streams `Connection`, and
-`SecureConn` mentions the identity `PeerId`, so this module imports
-`Streams.Conn`, `Streams.Stream`, and `Libp2p.Identity`. The identity
-package landed as W5.1, so the field types name the real one.
--/
-
-set_option autoImplicit false
-
-namespace Libp2p.Negotiate.Mock.Core
-
-/-- A wrapped-string protocol id. Peers define ids, so the set stays
-open. Code compares `ProtocolId` values only (root §3.4). -/
-structure ProtocolId where
-  toString : String
-  deriving DecidableEq, Hashable, Repr
-
-/-- The role of one side of a negotiation (root §4.9). No spec gives
-roles a wire code, so it has no `toCode`/`ofCode?` pair. -/
-inductive Role where
-  | initiator
-  | responder
-  deriving DecidableEq, Repr, Hashable
-
-/-- The coarse error of root §4.9. Each arm carries the error of the
-implementation, in its rendered form. The upgrader and the host act on
-this one type (root §3.5). -/
-inductive Error where
-  | protocol (s : String)
-  | authentication (s : String)
-  | timeout (s : String)
-  | closed (s : String)
-  deriving DecidableEq, Repr
-
-/-- The post-handshake connection. It holds the underlying
-`Connection` because `Muxer.open` takes a `Connection` (core
-ARCHITECTURE, "Public surface"). The `leftover` is every byte the
-handshake read past its end; it seeds the reader of the next stage. -/
-structure SecureConn where
-  conn : Streams.Connection
-  localPeer : Libp2p.Identity.PeerId
-  remotePeer : Libp2p.Identity.PeerId
-  leftover : ByteArray
-  close : BaseIO Unit
-
-/-- The security seam. `handshake` consumes the `ByteArray` the
-negotiation over-read before it reads the connection (root §4.7). -/
-structure SecurityProtocol where
-  id : ProtocolId
-  handshake : Role → Streams.Connection → ByteArray →
-    ExceptT Error Conc.Async SecureConn
-
-/-- The uniform session view of core ARCHITECTURE, "Public surface".
-The upgrader returns the opened session and never calls its fields. -/
-structure MuxSession where
-  openStream : ExceptT Error Conc.Async Streams.Stream
-  accept : Conc.Async (Option Streams.Stream)
-  close : BaseIO Unit
-  join : Conc.Async Unit
-
-/-- The muxer seam. The field is the frozen `open` of the core docs;
-`open` is a Lean keyword, so the field is declared escaped and called
-`mux.«open»`. -/
-structure Muxer where
-  id : ProtocolId
-  «open» : Role → Streams.Connection → ByteArray →
-    ExceptT Error Conc.Async MuxSession
-
-end Libp2p.Negotiate.Mock.Core
diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Step.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Step.lean
index 687eaeb0..53c4b588 100644
--- a/packages/libp2p/negotiate/Libp2p/Negotiate/Step.lean
+++ b/packages/libp2p/negotiate/Libp2p/Negotiate/Step.lean
@@ -1,5 +1,6 @@
 import Libp2p.Negotiate.Message
-import Libp2p.Negotiate.Mock.Core
+import Libp2p.Core.ProtocolId
+import Libp2p.Core.Role
 import Bytes
 
 /-!
@@ -37,9 +38,9 @@ inductive Phase where
 ordered list. `proposals` is the initiator's remaining list, in order.
 `buffer` holds the bytes no frame has consumed yet. -/
 structure State where
-  role : Mock.Core.Role
-  supported : List Mock.Core.ProtocolId
-  proposals : List Mock.Core.ProtocolId
+  role : Core.Role
+  supported : List Core.ProtocolId
+  proposals : List Core.ProtocolId
   buffer : List Nat
   phase : Phase
   deriving Repr, DecidableEq
@@ -48,14 +49,14 @@ structure State where
 is the local dialer's input. -/
 inductive Event where
   | bytes (bs : List Nat)
-  | propose (p : Mock.Core.ProtocolId)
+  | propose (p : Core.ProtocolId)
   deriving Repr, DecidableEq
 
 /-- One output of the core. A write carries framed bytes. A select
 ends the negotiation with the chosen id and the leftover bytes. -/
 inductive Action where
   | write (bs : List Nat)
-  | select (proto : Mock.Core.ProtocolId) (leftover : List Nat)
+  | select (proto : Core.ProtocolId) (leftover : List Nat)
   deriving Repr, DecidableEq
 
 /-- The replies the responder sends, the closed set of §3.4. -/
@@ -108,11 +109,11 @@ inductive Error where
 
 /-- The pure negotiation core of the spike: the first of `ours` that
 `theirs` also supports. -/
-def choose (ours theirs : List Mock.Core.ProtocolId) : Option Mock.Core.ProtocolId :=
+def choose (ours theirs : List Core.ProtocolId) : Option Core.ProtocolId :=
   List.find? theirs.contains ours
 
 /-- A chosen id is in our list and supported by theirs. -/
-theorem chooseSpec {ours theirs : List Mock.Core.ProtocolId} {p : Mock.Core.ProtocolId}
+theorem chooseSpec {ours theirs : List Core.ProtocolId} {p : Core.ProtocolId}
     (h : choose ours theirs = some p) : p ∈ ours ∧ theirs.contains p = true := by
   unfold choose at h
   exact ⟨List.mem_of_find?_eq_some h, List.find?_some h⟩
@@ -124,11 +125,11 @@ theorems about the chosen id reason over this classification. -/
 private inductive Answer where
   | echo
   | listIds
-  | pick (p : Mock.Core.ProtocolId)
+  | pick (p : Core.ProtocolId)
   | refuse
   | advance
-  | retry (q : Mock.Core.ProtocolId) (ps : List Mock.Core.ProtocolId)
-  | accept (p : Mock.Core.ProtocolId)
+  | retry (q : Core.ProtocolId) (ps : List Core.ProtocolId)
+  | accept (p : Core.ProtocolId)
   | fail
 
 /-- Classify a decoded text for a state. -/
@@ -140,7 +141,7 @@ private def classify (s : State) (text : String) : Answer :=
       | some .ls => .listIds
       | _ =>
         if text = protocolId.toString then .advance
-        else if (⟨text⟩ : Mock.Core.ProtocolId) ∈ s.supported then .pick ⟨text⟩
+        else if (⟨text⟩ : Core.ProtocolId) ∈ s.supported then .pick ⟨text⟩
         else .refuse
   | .initiator, .negotiating => if text = protocolId.toString then .advance else .fail
   | .initiator, .awaitingAnswer =>
@@ -175,7 +176,7 @@ records the id and writes the coalesced header plus the first proposal frame.
 Any other proposal event leaves the state unchanged: `initiatorStart` seeds
 the ordered list before the first frame moves, and the `na` retry walks that
 list from `classify`. -/
-private def propose (s : State) (p : Mock.Core.ProtocolId) : Except Error (State × List Action) :=
+private def propose (s : State) (p : Core.ProtocolId) : Except Error (State × List Action) :=
   if s.role = .initiator then
     if s.phase = .headerPending then
       if s.proposals = [] then
@@ -201,7 +202,7 @@ def step (s : State) : Event → Except Error (State × List Action)
 
 /-- A step that selects came from the pick or accept answer. -/
 private theorem actSelect {s : State} {rest : List Nat} {v : Answer} {s' : State}
-    {acts : List Action} {p : Mock.Core.ProtocolId} {r : List Nat}
+    {acts : List Action} {p : Core.ProtocolId} {r : List Nat}
     (h : act s rest v = .ok (s', acts)) (hm : Action.select p r ∈ acts) :
     v = .pick p ∨ v = .accept p := by
   cases v <;> simp only [act] at h
@@ -211,35 +212,35 @@ private theorem actSelect {s : State} {rest : List Nat} {v : Answer} {s' : State
          <;> (try simp_all))
 
 /-- A pick comes from the responder's supported list. -/
-private theorem classifyPick {s : State} {t : String} {p : Mock.Core.ProtocolId}
+private theorem classifyPick {s : State} {t : String} {p : Core.ProtocolId}
     (h : classify s t = .pick p) : p ∈ s.supported := by
   unfold classify at h
   repeat' split at h
   all_goals simp_all
 
 /-- An accept comes from the head of the initiator's proposals. -/
-private theorem classifyAcceptInitiator {s : State} {t : String} {p : Mock.Core.ProtocolId}
+private theorem classifyAcceptInitiator {s : State} {t : String} {p : Core.ProtocolId}
     (h : classify s t = .accept p) : p ∈ s.proposals := by
   unfold classify at h
   repeat' split at h
   all_goals simp_all
 
 /-- An accept carries the accepted text. -/
-private theorem classifyAcceptText {s : State} {t : String} {p : Mock.Core.ProtocolId}
+private theorem classifyAcceptText {s : State} {t : String} {p : Core.ProtocolId}
     (h : classify s t = .accept p) : p.toString = t := by
   unfold classify at h
   repeat' split at h
   all_goals simp_all
 
 /-- A responder never accepts. -/
-private theorem classifyAcceptResponder {s : State} {t : String} {p : Mock.Core.ProtocolId}
+private theorem classifyAcceptResponder {s : State} {t : String} {p : Core.ProtocolId}
     (hr : s.role = .responder) (h : classify s t = .accept p) : False := by
   unfold classify at h
   repeat' split at h
   all_goals simp_all
 
 /-- An initiator never picks. -/
-private theorem classifyPickInitiator {s : State} {t : String} {p : Mock.Core.ProtocolId}
+private theorem classifyPickInitiator {s : State} {t : String} {p : Core.ProtocolId}
     (hr : s.role = .initiator) (h : classify s t = .pick p) : False := by
   unfold classify at h
   repeat' split at h
@@ -277,7 +278,7 @@ private theorem classifyListIds {s : State} {t : String}
 /-- An unknown id in the negotiation draws the refuse answer. -/
 private theorem classifyRefuse {s : State} {t : String}
     (hrole : s.role = .responder) (hphase : s.phase = .negotiating)
-    (hnot : (⟨t⟩ : Mock.Core.ProtocolId) ∉ s.supported)
+    (hnot : (⟨t⟩ : Core.ProtocolId) ∉ s.supported)
     (hheader : t ≠ protocolId.toString) (hreply : Reply.ofText? t = none) :
     classify s t = .refuse := by
   unfold classify
@@ -286,8 +287,8 @@ private theorem classifyRefuse {s : State} {t : String}
   rw [ite_eq_right hheader, ite_eq_right hnot]
 
 /-- A retry pops one proposal: the new list is the tail of the old. -/
-private theorem classifyRetryTail {s : State} {t : String} {q : Mock.Core.ProtocolId}
-    {ps : List Mock.Core.ProtocolId} (h : classify s t = .retry q ps) :
+private theorem classifyRetryTail {s : State} {t : String} {q : Core.ProtocolId}
+    {ps : List Core.ProtocolId} (h : classify s t = .retry q ps) :
     s.proposals.tail = ps := by
   unfold classify at h
   repeat' split at h
@@ -341,8 +342,8 @@ private theorem actRefuse {s : State} {rest : List Nat} {s' : State} {actions :
   simp
 
 /-- The retry answer replaces the proposals with the remaining list. -/
-private theorem actRetryWrites {s : State} {rest : List Nat} {q : Mock.Core.ProtocolId}
-    {ps : List Mock.Core.ProtocolId} {s' : State} {actions : List Action}
+private theorem actRetryWrites {s : State} {rest : List Nat} {q : Core.ProtocolId}
+    {ps : List Core.ProtocolId} {s' : State} {actions : List Action}
     (h : act s rest (.retry q ps) = .ok (s', actions)) : s'.proposals = ps := by
   unfold act at h
   simp only [Except.ok.injEq, Prod.mk.injEq] at h
@@ -353,7 +354,7 @@ private theorem actRetryWrites {s : State} {rest : List Nat} {q : Mock.Core.Prot
 
 /-- A responder selects only from its supported list (contract 2). -/
 theorem stepSelectResponderMem {s : State} {bs : List Nat} {s' : State}
-    {actions : List Action} {p : Mock.Core.ProtocolId} {rest : List Nat}
+    {actions : List Action} {p : Core.ProtocolId} {rest : List Nat}
     (hrole : s.role = .responder)
     (hstep : step s (.bytes bs) = .ok (s', actions))
     (hmem : Action.select p rest ∈ actions) : p ∈ s.supported := by
@@ -369,7 +370,7 @@ theorem stepSelectResponderMem {s : State} {bs : List Nat} {s' : State}
 
 /-- An initiator selects only from its own proposal list. -/
 theorem stepSelectInitiatorMem {s : State} {bs : List Nat} {s' : State}
-    {actions : List Action} {p : Mock.Core.ProtocolId} {rest : List Nat}
+    {actions : List Action} {p : Core.ProtocolId} {rest : List Nat}
     (hrole : s.role = .initiator)
     (hstep : step s (.bytes bs) = .ok (s', actions))
     (hmem : Action.select p rest ∈ actions) : p ∈ s.proposals := by
@@ -387,7 +388,7 @@ theorem stepSelectInitiatorMem {s : State} {bs : List Nat} {s' : State}
 head: the new list is the old tail, so it is strictly shorter
 (contract 2, the `na` retry). -/
 theorem stepInitiatorNaProgress {s : State} {bs : List Nat} {s' : State}
-    {actions : List Action} {p : Mock.Core.ProtocolId} {ps : List Mock.Core.ProtocolId}
+    {actions : List Action} {p : Core.ProtocolId} {ps : List Core.ProtocolId}
     {w : List Nat}
     (hrole : s.role = .initiator) (hprop : s.proposals = p :: ps)
     (hstep : step s (.bytes bs) = .ok (s', actions))
@@ -442,7 +443,7 @@ theorem stepResponderLsStays {s : State} {bs : List Nat} {s' : State}
 /-- An unknown id draws the `na` frame and stays in the negotiation
 (contract 2). -/
 theorem stepResponderUnknownStays {s : State} {bs : List Nat} {s' : State}
-    {actions : List Action} {m : Msg} {rest : List Nat} {id : Mock.Core.ProtocolId}
+    {actions : List Action} {m : Msg} {rest : List Nat} {id : Core.ProtocolId}
     (hrole : s.role = .responder) (hphase : s.phase = .negotiating)
     (hdec : decodeMsg? (s.buffer ++ bs) = .ok (m, rest))
     (htext : m.text = id.toString) (hnot : id ∉ s.supported)
@@ -450,7 +451,7 @@ theorem stepResponderUnknownStays {s : State} {bs : List Nat} {s' : State}
     (hreply : Reply.ofMsg? m = none)
     (hstep : step s (.bytes bs) = .ok (s', actions)) :
     actions = [.write (encodeMsg (Reply.toMsg .na))] ∧ s'.phase = .negotiating ∧ s'.buffer = rest := by
-  have hnot' : (⟨m.text⟩ : Mock.Core.ProtocolId) ∉ s.supported := by
+  have hnot' : (⟨m.text⟩ : Core.ProtocolId) ∉ s.supported := by
     intro hm
     apply hnot
     simpa [htext] using hm
@@ -469,7 +470,7 @@ theorem stepResponderUnknownStays {s : State} {bs : List Nat} {s' : State}
 /-- Conservation: the bytes the accepting initiator consumed, plus the
 leftover, equal the bytes fed in (contract 5). -/
 theorem stepSelectConservation {s : State} {bs : List Nat} {s' : State}
-    {p : Mock.Core.ProtocolId} {rest r : List Nat} {m : Msg}
+    {p : Core.ProtocolId} {rest r : List Nat} {m : Msg}
     (hrole : s.role = .initiator)
     (hdec : decodeMsg? (s.buffer ++ bs) = .ok (m, r))
     (hstep : step s (.bytes bs) = .ok (s', [Action.select p rest])) :
diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Upgrade.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Upgrade.lean
index 1f8c34c2..355b3a84 100644
--- a/packages/libp2p/negotiate/Libp2p/Negotiate/Upgrade.lean
+++ b/packages/libp2p/negotiate/Libp2p/Negotiate/Upgrade.lean
@@ -1,6 +1,6 @@
 import Libp2p.Negotiate.Step
 import Libp2p.Negotiate.Message
-import Libp2p.Negotiate.Mock.Core
+import Libp2p.Core
 import Libp2p.Identity
 import Streams.Conn
 import Streams.BufReader
@@ -33,8 +33,19 @@ wait, so the loop keeps the package's `repeat` form, the form of
 
 The three stages thread the leftover bytes by contract 5 of the
 package docs: the negotiation leftover seeds the handshake, the
-`SecureConn` leftover seeds the muxer negotiation, and the muxer
-negotiation leftover reaches `Muxer.open`.
+`SecureConn` delivers its own leftover through its `read`, so the
+muxer negotiation starts with no bytes, and the muxer negotiation
+leftover reaches `Muxer.open`.
+
+## The secure connection has an owner
+
+The handshake answers a `SecureConn`, whose transport runs tasks, and
+the upgrader is the owner that closes it and joins it (the core pair,
+contract 4; PRINCIPLES 3.2). The frozen answer is the `MuxSession`, so
+the upgrader hands the join on inside it: the session's `join` waits
+for the session loop, then for the secure connection. Every failure
+after the handshake closes the secure connection and joins it before
+the upgrader answers.
 -/
 
 set_option autoImplicit false
@@ -58,7 +69,7 @@ open Bytes (DecodeError)
   complete frame. The caller calls `drive` again with `leftover`; it
   must not read. -/
 inductive DriveResult where
-  | selected (p : Mock.Core.ProtocolId) (consumed leftover : List Nat)
+  | selected (p : Core.ProtocolId) (consumed leftover : List Nat)
       (writes : List (List Nat))
   | waiting (s : State) (consumed leftover : List Nat) (writes : List (List Nat))
   | running (s : State) (consumed leftover : List Nat) (writes : List (List Nat))
@@ -87,7 +98,7 @@ def writesOf (actions : List Action) : List (List Nat) :=
     | .select .. => none
 
 /-- The protocol an action list selects, if it selects one. -/
-def selectOf : List Action → Option Mock.Core.ProtocolId
+def selectOf : List Action → Option Core.ProtocolId
   | [] => none
   | .write _ :: rest => selectOf rest
   | .select p _ :: _ => some p
@@ -125,7 +136,7 @@ The write holds the header and the first proposal back-to-back, the
 lazy dialer's wire shape (contract 4 of the package docs). The state
 carries the whole ordered list, so the core's `na` retry walks it.
 An empty ordered list is a protocol error before any byte moves. -/
-def initiatorStart (ids : List Mock.Core.ProtocolId) :
+def initiatorStart (ids : List Core.ProtocolId) :
     Except Error (State × List (List Nat)) :=
   match ids with
   | [] => .error .negotiationFailed
@@ -140,7 +151,7 @@ def initiatorStart (ids : List Mock.Core.ProtocolId) :
 at once. The spec lets either side send first, and the responder that waits
 for the dialer's header stalls a dialer that also waits. The state starts in
 `negotiating` because the header is already on the wire. -/
-def responderStart (ids : List Mock.Core.ProtocolId) :
+def responderStart (ids : List Core.ProtocolId) :
     Except Error (State × List (List Nat)) :=
   if ids.any (fun q => !fitsText q.toString) then .error .negotiationFailed
   else if maxMsg < (lsBody ids).length then .error .negotiationFailed
@@ -159,7 +170,7 @@ def renderDecodeError : Bytes.DecodeError → String
 
 /-- Contract 8's one mapping point: every negotiation error becomes
 the `protocol` arm, with the detail rendered. -/
-def mapNegotiateError : Error → Mock.Core.Error
+def mapNegotiateError : Error → Core.Error
   | .decode e => .protocol ("multistream decode: " ++ renderDecodeError e)
   | .negotiationFailed => .protocol "multistream negotiation failed"
 
@@ -168,7 +179,7 @@ peer. The dial path compares the derived id against the expectation
 and answers `authentication` on a difference, before any muxer byte
 moves (negotiate ARCHITECTURE, "Decisions"). -/
 def checkIdentity (expected : Option Libp2p.Identity.PeerId)
-    (remote : Libp2p.Identity.PeerId) : Except Mock.Core.Error Unit :=
+    (remote : Libp2p.Identity.PeerId) : Except Core.Error Unit :=
   match expected with
   | none => .ok ()
   | some e =>
@@ -179,7 +190,7 @@ def checkIdentity (expected : Option Libp2p.Identity.PeerId)
 `.error .deadlineExpired`; the `.closed` arm is required by the match
 and is unreachable from `withinDeadline`. -/
 def settleUpgrade {α : Type} :
-    Except Conc.Error (Except Mock.Core.Error α) → Except Mock.Core.Error α
+    Except Conc.Error (Except Core.Error α) → Except Core.Error α
   | .ok (.ok a) => .ok a
   | .ok (.error e) => .error e
   | .error .deadlineExpired => .error (.timeout "upgrade deadline expired")
@@ -189,7 +200,7 @@ def settleUpgrade {α : Type} :
 the stage over-read. `ByteArray` carries no `Repr` in Lean 4.34, so
 the structure derives none; the suite compares the fields it needs. -/
 structure StageResult where
-  proto : Mock.Core.ProtocolId
+  proto : Core.ProtocolId
   leftover : ByteArray
 
 /-! ## The driver theorems -/
@@ -244,7 +255,7 @@ theorem driveConservation {fuel : Nat} {s : State} {input : List Nat} {r : Drive
 /-- The selected arm: the bytes in equal the frames consumed plus
 the leftover handed to the next stage (contract 5). -/
 theorem driveSelectedConservation {fuel : Nat} {s : State} {input : List Nat}
-    {p : Mock.Core.ProtocolId} {consumed leftover : List Nat}
+    {p : Core.ProtocolId} {consumed leftover : List Nat}
     {writes : List (List Nat)}
     (h : drive fuel s input = .ok (.selected p consumed leftover writes)) :
     input = consumed ++ leftover := by
@@ -335,7 +346,7 @@ theorem handoverCompose {ε α β : Type}
 the first drive's leftover, the bytes fed in equal the bytes both
 drives consumed plus the final leftover. -/
 theorem driveTwostage {fuel₁ fuel₂ : Nat} {s₁ s₂ : State}
-    {input₁ input₂ : List Nat} {p₁ p₂ : Mock.Core.ProtocolId}
+    {input₁ input₂ : List Nat} {p₁ p₂ : Core.ProtocolId}
     {c₁ c₂ l₁ l₂ : List Nat} {w₁ w₂ : List (List Nat)}
     (h₁ : drive fuel₁ s₁ input₁ = .ok (.selected p₁ c₁ l₁ w₁))
     (h₂ : drive fuel₂ s₂ (l₁ ++ input₂) = .ok (.selected p₂ c₂ l₂ w₂)) :
@@ -347,7 +358,7 @@ theorem driveTwostage {fuel₁ fuel₂ : Nat} {s₁ s₂ : State}
 
 /-- The shell's manual first write equals the core's propose step for
 a singleton list. The theorem does not cover a longer list. -/
-theorem initiatorStartPropose {p : Mock.Core.ProtocolId}
+theorem initiatorStartPropose {p : Core.ProtocolId}
     (hfits : fitsText p.toString = true) :
     initiatorStart [p] =
       (step { role := .initiator, supported := [], proposals := [], buffer := [],
@@ -391,7 +402,7 @@ theorem checkIdentityNone {r : Libp2p.Identity.PeerId} :
 /-- The deadline wiring of contract 6: the race's expiry is the
 `timeout` arm, and the seam errors pass through untouched. The
 `.closed` arm is required by the match over `Conc.Error`. -/
-theorem settleUpgradeSpec {α : Type} {e : Mock.Core.Error} {a : α} :
+theorem settleUpgradeSpec {α : Type} {e : Core.Error} {a : α} :
     settleUpgrade (α := α) (.error .deadlineExpired) =
       .error (.timeout "upgrade deadline expired") ∧
     settleUpgrade (α := α) (.error .closed) =
@@ -406,7 +417,7 @@ theorem settleUpgradeSpec {α : Type} {e : Mock.Core.Error} {a : α} :
 `closed` arm. `Connection.write` throws `IO.Error`, which is outside
 this shell's `Core.Error` channel. -/
 private def writeFrame (conn : Streams.Connection) (b : ByteArray) :
-    ExceptT Mock.Core.Error Conc.Async Unit := do
+    ExceptT Core.Error Conc.Async Unit := do
   let ok ← (try
     conn.write b
     pure true
@@ -416,7 +427,7 @@ private def writeFrame (conn : Streams.Connection) (b : ByteArray) :
 /-- Write each frame payload through the connection, in order. A
 failed write is the `closed` arm: the connection is gone. -/
 private def sendWrites (conn : Streams.Connection) (ws : List (List Nat)) :
-    ExceptT Mock.Core.Error Conc.Async Unit := do
+    ExceptT Core.Error Conc.Async Unit := do
   for w in ws do
     writeFrame conn (Bytes.ofNatList w)
 
@@ -429,7 +440,7 @@ long as the peer stays silent, so no measure bounds the loop (root
 marker, like `Conc.TaskSet.joinAll`. -/
 private def negotiateLoop (reader : Streams.BufReader)
     (conn : Streams.Connection) (s : State) (input : List Nat) :
-    ExceptT Mock.Core.Error Conc.Async StageResult := do
+    ExceptT Core.Error Conc.Async StageResult := do
   let mut s := s
   let mut input := input
   let mut reader := reader
@@ -461,10 +472,10 @@ initiator writes the coalesced header plus first proposal, and the
 responder writes its header. The seed is the leftover of the previous
 stage. The end of the stream mid-negotiation is `Core.Error.closed`; a
 `Negotiate.Error` maps once through `mapNegotiateError`. -/
-def negotiate (role : Mock.Core.Role) (reader : Streams.BufReader)
+def negotiate (role : Core.Role) (reader : Streams.BufReader)
     (conn : Streams.Connection) (seed : ByteArray)
-    (ids : List Mock.Core.ProtocolId) :
-    ExceptT Mock.Core.Error Conc.Async StageResult := do
+    (ids : List Core.ProtocolId) :
+    ExceptT Core.Error Conc.Async StageResult := do
   match role with
   | .initiator =>
     match initiatorStart ids with
@@ -479,13 +490,34 @@ def negotiate (role : Mock.Core.Role) (reader : Streams.BufReader)
         sendWrites conn first
         negotiateLoop reader conn s (Bytes.toNatList seed)
 
+/-- Close a secure connection and wait for its tasks. The answer of its
+join is dropped: the caller already holds the failure it reports. -/
+private def discardSecure (sc : Core.SecureConn) : Conc.Async Unit := do
+  sc.toConnection.closeQuietly
+  discard sc.join.run
+
+/-- The session the upgrader answers: `s`, with a `join` that also
+waits for the secure connection under it. The secure connection is
+joined even when the session's join throws a fault, so none of its
+tasks outlives the join (PRINCIPLES 3.2); the first failure wins. -/
+private def ownSecure (s : Core.MuxSession) (sc : Core.SecureConn) : Core.MuxSession :=
+  { s with
+    join := ExceptT.mk do
+      let a : Except IO.Error (Except Core.Error Unit) ←
+        try pure (.ok (← s.join.run)) catch e => pure (.error e)
+      let b ← sc.join.run
+      match a with
+      | .error e => throw e
+      | .ok a => return a.bind fun () => b }
+
 /-- The pipeline: negotiate the security protocol, run the handshake,
 check the identity, negotiate the muxer, open the session. Each lookup
-is total; a miss after a selection is `protocol`. -/
-private def upgradeCore (role : Mock.Core.Role) (conn : Streams.Connection)
+is total; a miss after a selection is `protocol`. A failure after the
+handshake closes and joins the secure connection. -/
+private def upgradeCore (role : Core.Role) (conn : Streams.Connection)
     (leftover : ByteArray) (expected : Option Libp2p.Identity.PeerId)
-    (secs : List Mock.Core.SecurityProtocol) (muxers : List Mock.Core.Muxer) :
-    Conc.Async (Except Mock.Core.Error (Mock.Core.MuxSession × Libp2p.Identity.PeerId)) := do
+    (secs : List Core.SecurityProtocol) (muxers : List Core.Muxer) :
+    Conc.Async (Except Core.Error (Core.MuxSession × Libp2p.Identity.PeerId)) := do
   let reader := Streams.BufReader.new conn
   match ← negotiate role reader conn leftover (secs.map (·.id)) with
   | .error e => return .error e
@@ -497,18 +529,24 @@ private def upgradeCore (role : Mock.Core.Role) (conn : Streams.Connection)
       | .error e => return .error e
       | .ok sc =>
         match checkIdentity expected sc.remotePeer with
-        | .error e => return .error e
+        | .error e => discardSecure sc; return .error e
         | .ok () =>
-          let muxReader := Streams.BufReader.new sc.conn
-          match ← negotiate role muxReader sc.conn sc.leftover (muxers.map (·.id)) with
-          | .error e => return .error e
+          -- The secure `read` delivers the handshake's leftover, so the
+          -- muxer negotiation starts with no bytes (the core pair, "The
+          -- leftover hand-over").
+          let secure := sc.toConnection
+          let muxReader := Streams.BufReader.new secure
+          match ← negotiate role muxReader secure .empty (muxers.map (·.id)) with
+          | .error e => discardSecure sc; return .error e
           | .ok stage2 =>
             match muxers.find? (fun m => decide (m.id = stage2.proto)) with
-            | none => return .error (.protocol "selected muxer is not configured")
+            | none =>
+              discardSecure sc
+              return .error (.protocol "selected muxer is not configured")
             | some mux =>
-              match ← mux.«open» role sc.conn stage2.leftover with
-              | .error e => return .error e
-              | .ok session => return .ok (session, sc.remotePeer)
+              match ← mux.«open» role secure stage2.leftover with
+              | .error e => discardSecure sc; return .error e
+              | .ok session => return .ok (ownSecure session sc, sc.remotePeer)
 
 /-- Whether the deadline boundary already closed the connection.
 `withinDeadline` returns an error value only on expiry, after the hook
@@ -517,12 +555,15 @@ private def boundaryClosed {α : Type} : Except Conc.Error α → Bool
   | .error _ => true
   | .ok _ => false
 
-/-- Close a session that finished after the timer won. No caller
-receives that session. -/
-private def releaseLate (r : Except Mock.Core.Error
-    (Mock.Core.MuxSession × Libp2p.Identity.PeerId)) : BaseIO Unit :=
+/-- Close a session that finished after the timer won, and give its
+join to `late`, the task set `upgradeWith` joins. No caller receives
+that session. -/
+private def releaseLate (late : Conc.TaskSet) (r : Except Core.Error
+    (Core.MuxSession × Libp2p.Identity.PeerId)) : BaseIO Unit :=
   match r with
-  | .ok pair => pair.1.close
+  | .ok pair => do
+    discard pair.1.close.toBaseIO
+    late.spawn (discard pair.1.join.run)
   | .error _ => pure ()
 
 /-- The upgrade under one `Conc.withinDeadline`. The expiry closes
@@ -530,15 +571,17 @@ the connection once at the boundary (root §3.5), and the race's
 `deadlineExpired` maps to the `timeout` arm through `settleUpgrade`.
 The clock is a seam, so the deadline test can advance it. -/
 
-def upgradeWith (clock : Conc.Clock) (role : Mock.Core.Role)
+def upgradeWith (clock : Conc.Clock) (role : Core.Role)
     (conn : Streams.Connection) (leftover : ByteArray)
     (expected : Option Libp2p.Identity.PeerId)
-    (secs : List Mock.Core.SecurityProtocol) (muxers : List Mock.Core.Muxer) :
-    ExceptT Mock.Core.Error Conc.Async (Mock.Core.MuxSession × Libp2p.Identity.PeerId) := do
+    (secs : List Core.SecurityProtocol) (muxers : List Core.Muxer) :
+    ExceptT Core.Error Conc.Async (Core.MuxSession × Libp2p.Identity.PeerId) := do
+  let late ← Conc.TaskSet.new
   let answer ← Conc.withinDeadline clock Streams.unauthDeadlineMs
     (Streams.Connection.closeQuietly conn)
     (upgradeCore role conn leftover expected secs muxers)
-    releaseLate
+    (releaseLate late)
+  late.joinAll
   match settleUpgrade answer with
   | .ok pair => return pair
   | .error e => do
@@ -552,10 +595,10 @@ def upgradeWith (clock : Conc.Clock) (role : Mock.Core.Role)
 /-- The frozen entry of the package docs. The clock is fixed to the
 system clock here and stays a seam in `upgradeWith` for the deadline
 test. -/
-def upgrade (role : Mock.Core.Role) (conn : Streams.Connection)
+def upgrade (role : Core.Role) (conn : Streams.Connection)
     (leftover : ByteArray) (expected : Option Libp2p.Identity.PeerId)
-    (secs : List Mock.Core.SecurityProtocol) (muxers : List Mock.Core.Muxer) :
-    ExceptT Mock.Core.Error Conc.Async (Mock.Core.MuxSession × Libp2p.Identity.PeerId) :=
+    (secs : List Core.SecurityProtocol) (muxers : List Core.Muxer) :
+    ExceptT Core.Error Conc.Async (Core.MuxSession × Libp2p.Identity.PeerId) :=
   upgradeWith Conc.Clock.system role conn leftover expected secs muxers
 
 end Libp2p.Negotiate
diff --git a/packages/libp2p/negotiate/docs/ARCHITECTURE.md b/packages/libp2p/negotiate/docs/ARCHITECTURE.md
index 9a0bb013..729b2ebb 100644
--- a/packages/libp2p/negotiate/docs/ARCHITECTURE.md
+++ b/packages/libp2p/negotiate/docs/ARCHITECTURE.md
@@ -65,7 +65,11 @@ and `Streams.Stream`.
   when an accept path peeked before it handed the connection over, or
   when the transport delivers bytes together with the connection. The
   output is the pair of the `MuxSession` and the verified remote
-  `PeerId`. Errors surface as `Core.Error` (§3.5).
+  `PeerId`. Errors surface as `Core.Error` (§3.5). The upgrader owns
+  the `SecureConn` of the handshake (the core pair, contract 4): the
+  answered session's `join` waits for the session loop, then for the
+  secure connection, and every failure after the handshake closes the
+  secure connection and joins it before the upgrader answers.
 
 ## The muxer-selection decision
 
@@ -108,9 +112,13 @@ connection-level selection.
    Go's upgrade traces and §4.9's "lazy dialer" bullet both name the
    lazy write, and the target moves it into the upgrade.
 5. **Leftover hand-over between all three stages** (§4.7, §5.6). The
-   negotiation leftover seeds the handshake; the `SecureConn` leftover
-   seeds the muxer negotiation; the bytes that stage over-reads enter
-   `Muxer.open` and become the first `Event` of the session loop (§4.7).
+   negotiation leftover seeds the handshake; the bytes the handshake
+   over-read reach the muxer negotiation through the secure `read`,
+   which delivers them before any connection byte, so that negotiation
+   starts with no seed (the core pair, "The leftover hand-over": no
+   stage above `read` takes `SecureConn.leftover`); the bytes the muxer
+   negotiation over-reads enter `Muxer.open` and become the first
+   `Event` of the session loop (§4.7).
    Each stage owns one reader, and no two stages share a `BufReader`
    (§5.6).
 6. **The 30 s deadline covers the whole unauthenticated upgrade**