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**