From 3cf3c635546b7ae051205565a07f96ecc971cb11 Mon Sep 17 00:00:00 2001
From: Ivan Anishchuk <ivan@agorism.org>
Date: Sun, 8 Nov 2026 12:04:44 +0530
Subject: [PATCH 1/2] refactor(host): take the seam types from libp2p/core

W5.2 merged, so the host drops Host.Mock.Core. Error, Registry, Dedup,
Policy, and Swarm import Libp2p.Core, and the real types match the
mock field for field.

Host.Mock.Negotiate stays. The merged negotiate package types its
upgrader over its own core mock, so the host cannot pass it real seam
values until issue #53 lands. The mock now names the real core types.
The docs and the skipped host legs name what the swap waits on.

Part of #70
---
 Tests/Host.lean                               |  10 +-
 packages/libp2p/host/Libp2p/Host/Dedup.lean   |   4 +-
 packages/libp2p/host/Libp2p/Host/Error.lean   |   8 +-
 .../libp2p/host/Libp2p/Host/Mock/Core.lean    | 176 ------------------
 .../host/Libp2p/Host/Mock/Negotiate.lean      |  25 ++-
 packages/libp2p/host/Libp2p/Host/Policy.lean  |   4 +-
 .../libp2p/host/Libp2p/Host/Registry.lean     |   4 +-
 packages/libp2p/host/Libp2p/Host/Swarm.lean   |   9 +-
 packages/libp2p/host/docs/ARCHITECTURE.md     |  29 +--
 packages/libp2p/host/docs/PLAN.md             |   6 +-
 10 files changed, 51 insertions(+), 224 deletions(-)
 delete mode 100644 packages/libp2p/host/Libp2p/Host/Mock/Core.lean

diff --git a/Tests/Host.lean b/Tests/Host.lean
index 0bb1e43e..46547faf 100644
--- a/Tests/Host.lean
+++ b/Tests/Host.lean
@@ -19,15 +19,17 @@ here, since the rule never reads it.
 Unit 1b runs hosts over the sim transport, with the real
 `Noise.securityProtocol` and `Mux.yamux` values (PRINCIPLES 1.4). Every
 host derives its peer id through `libp2p/identity`, and the upgrade runs
-through `libp2p/negotiate`, so the legs wait for W5.3, W5.4, and W5.5
-to merge. Until then the suite names each leg as a skip.
+through `libp2p/negotiate`. Those packages merged over mocks of
+`libp2p/core`, so the legs wait for their seam swaps: issues #53
+(negotiate), #76 (Noise), #77 (`Mux.yamux`), and the negotiate swap of
+the host, issue #70. Until then the suite names each leg as a skip.
 -/
 
 set_option autoImplicit false
 
 namespace Tests
 
-open Conc Multiformats Libp2p.Identity Libp2p.Host.Mock.Core Libp2p.Host
+open Conc Multiformats Libp2p.Identity Libp2p.Core Libp2p.Host
 
 /-! ## Helpers -/
 
@@ -298,6 +300,6 @@ def Host.run (r : Runner) : IO Unit := do
   (peerstoreChecks r).run
   errorChecks r
   for leg in swarmLegs do
-    r.skip s!"host: {leg}" "needs W5.3, W5.4, and W5.5 merged"
+    r.skip s!"host: {leg}" "needs the seam swaps of issues #53, #76, #77, and #70"
 
 end Tests
diff --git a/packages/libp2p/host/Libp2p/Host/Dedup.lean b/packages/libp2p/host/Libp2p/Host/Dedup.lean
index 6a88bce4..57e86bd8 100644
--- a/packages/libp2p/host/Libp2p/Host/Dedup.lean
+++ b/packages/libp2p/host/Libp2p/Host/Dedup.lean
@@ -1,5 +1,5 @@
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 import Libp2p.Host.Constants
 import Libp2p.Host.Registry
 
@@ -46,7 +46,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
-open Libp2p.Identity Libp2p.Host.Mock.Core
+open Libp2p.Identity Libp2p.Core
 
 /-- The order of two peer ids by their binary form, byte by byte
 (module doc, "The order on peer ids"). -/
diff --git a/packages/libp2p/host/Libp2p/Host/Error.lean b/packages/libp2p/host/Libp2p/Host/Error.lean
index 854042d6..8eb88b5d 100644
--- a/packages/libp2p/host/Libp2p/Host/Error.lean
+++ b/packages/libp2p/host/Libp2p/Host/Error.lean
@@ -1,6 +1,6 @@
 import Multiformats
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core.Error
 
 /-!
 # `Host.Error`
@@ -20,9 +20,9 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
--- The mock of the unmerged core (RULES.md, "Working ahead of the
--- tree"); `Core.Error` resolves through `Libp2p.Host.Mock`.
-open Multiformats Libp2p.Host.Mock Libp2p.Identity
+-- `Core.Error` resolves to `Libp2p.Core.Error` through the parent
+-- namespace `Libp2p`.
+open Multiformats Libp2p.Identity
 
 /-- The policy checkpoint that refused a connection (§3.4: a closed
 set). The gater answers at the first three (`Core.ConnectionGater`),
diff --git a/packages/libp2p/host/Libp2p/Host/Mock/Core.lean b/packages/libp2p/host/Libp2p/Host/Mock/Core.lean
deleted file mode 100644
index 6678d411..00000000
--- a/packages/libp2p/host/Libp2p/Host/Mock/Core.lean
+++ /dev/null
@@ -1,176 +0,0 @@
-import Conc
-import Streams
-import Libp2p.Identity
-
-/-!
-# Mock: the surface of `libp2p/core` that the host uses
-
-W5.2 (`libp2p/core`) has not merged, so the host builds against a mock
-of its frozen surface (RULES.md, "Working ahead of the tree"). The
-types are copies: the seam shapes of the core ARCHITECTURE, "Public
-surface", with `MuxSession.openStream` carrying a `ProtocolId` (the mux
-ARCHITECTURE, "Public surface"). The mock imports nothing from the real
-package, and it states no axiom.
-
-## The policy shapes
-
-The core ARCHITECTURE fixes the three policy hooks and no signatures:
-"the decision inputs beyond these are the seam's to refine as the host
-lands (W5.6)". This unit fixes them, and the core ARCHITECTURE records
-them. The peer of an inbound connection is unknown until the handshake
-ends, so the gater and the resource manager each take a second decision
-there, with the proved peer, as go-libp2p does:
-`ConnectionGater.InterceptSecured` (`vendor/go-libp2p/core/connmgr/gater.go`)
-and `ResourceScope.SetPeer` (`vendor/go-libp2p/core/network/rcmgr.go`).
-The ranker answers a dial schedule, an address and a delay each, the
-shape of go-libp2p's `AddrDelay` and `DialRanker`
-(`vendor/go-libp2p/core/network/network.go`, lines 212 and 218).
-
-A policy answer runs in `BaseIO`: it has no fault channel, so a policy
-throw cannot lose a dial.
-
-At the integration, the host imports `Libp2p.Core`, and the module goes.
--/
-
-set_option autoImplicit false
-
-namespace Libp2p.Host.Mock.Core
-
-open Conc Streams Multiformats Libp2p.Identity
-
-/-- A protocol id, wrapped (§3.4). -/
-structure ProtocolId where
-  /-- The id text. -/
-  toString : String
-  deriving DecidableEq, Hashable, Ord, Repr
-
-instance : ToString ProtocolId := ⟨ProtocolId.toString⟩
-
-/-- The coarse error every seam returns (§4.9). Each arm carries the
-rendered error of the implementation. -/
-inductive Error where
-  | protocol (detail : String)
-  | authentication (detail : String)
-  | timeout (detail : String)
-  | closed (detail : String)
-  deriving DecidableEq, Repr
-
-/-- The log line of the error: the kind, then the rendered detail. -/
-def Error.render : Error → String
-  | .protocol d => s!"protocol error: {d}"
-  | .authentication d => s!"authentication failure: {d}"
-  | .timeout d => s!"timeout: {d}"
-  | .closed d => s!"closed: {d}"
-
-instance : ToString Error := ⟨Error.render⟩
-
-/-- Our side of a connection (§4.9). -/
-inductive Role where
-  | initiator
-  | responder
-  deriving DecidableEq, Repr
-
-/-- The connection after the handshake: the secure connection, the two
-peer ids, the bytes the handshake read past its end, and the
-completion of its tasks. -/
-structure SecureConn extends Connection where
-  /-- Our peer id. -/
-  localPeer : PeerId
-  /-- The peer id the handshake proved. -/
-  remotePeer : PeerId
-  /-- The bytes the handshake read past its end (§4.7). -/
-  leftover : ByteArray
-  /-- Wait until the secure connection's tasks end. -/
-  join : ExceptT Error Async Unit
-
-/-- The security seam. -/
-structure SecurityProtocol where
-  /-- The negotiated id. -/
-  id : ProtocolId
-  /-- Run the handshake over a connection, with the negotiation's
-  leftover. -/
-  handshake : Role → Connection → ByteArray → ExceptT Error Async SecureConn
-
-/-- A muxer session. -/
-structure MuxSession where
-  /-- Open a stream, labeled with its protocol id. -/
-  openStream : ProtocolId → ExceptT Error Async Stream
-  /-- The next stream the peer opened; `none` once the session ends. -/
-  accept : Async (Option Stream)
-  /-- End the session. -/
-  close : IO Unit
-  /-- Wait until the session loop ends. -/
-  join : ExceptT Error Async Unit
-
-/-- The muxer seam. -/
-structure Muxer where
-  /-- The negotiated id. -/
-  id : ProtocolId
-  /-- Open a session over a secure connection, with the negotiation's
-  leftover. -/
-  «open» : Role → Connection → ByteArray → ExceptT Error Async MuxSession
-
-/-- What the host knows about the connection under a served stream. -/
-structure StreamContext where
-  /-- The peer id the security handshake proved. -/
-  remotePeer : PeerId
-  /-- The peer's transport address, as the connection reports it. -/
-  remoteAddr : Multiaddr
-
-/-- The callback a served stream reaches. -/
-structure StreamHandler where
-  /-- The id the handler serves. -/
-  id : ProtocolId
-  /-- Serve one stream of the connection that `StreamContext`
-  describes. -/
-  handle : StreamContext → Stream → ExceptT Error Async Unit
-
-/-! ## The policy hooks (module doc, "The policy shapes") -/
-
-/-- The connection gater. `true` allows. -/
-structure ConnectionGater where
-  /-- Before an outbound dial, by the expected peer and the address. -/
-  allowDial : Option PeerId → Multiaddr → BaseIO Bool
-  /-- After an accept, before any byte moves, by the two addresses. -/
-  allowInbound : (localAddr remoteAddr : Multiaddr) → BaseIO Bool
-  /-- After the handshake, before the muxer stage, by the proved peer. -/
-  allowSecured : Role → PeerId → (localAddr remoteAddr : Multiaddr) → BaseIO Bool
-
-/-- An admitted share of a limit. A second `release` does nothing. -/
-structure Reservation where
-  /-- Return the share. -/
-  release : BaseIO Unit
-
-/-- The resource scope of one admitted connection. -/
-structure ConnectionScope where
-  /-- Name the proved peer; `false` when the connection does not fit
-  that peer's limits. -/
-  setPeer : PeerId → BaseIO Bool
-  /-- Admit one more stream; `none` when it does not fit. -/
-  reserveStream : BaseIO (Option Reservation)
-  /-- Admit this many more buffered bytes; `none` when they do not fit. -/
-  reserveMemory : Nat → BaseIO (Option Reservation)
-  /-- Return the connection's share and every share it still holds. -/
-  release : BaseIO Unit
-
-/-- The resource manager. -/
-structure ResourceManager where
-  /-- Admit a new connection, by its direction, the expected peer, and
-  the remote address; `none` when it does not fit. -/
-  openConnection : Role → Option PeerId → Multiaddr → BaseIO (Option ConnectionScope)
-
-/-- One address of a dial schedule, with its delay from the start of
-the dial, in milliseconds. -/
-structure AddrDelay where
-  /-- The address to dial. -/
-  addr : Multiaddr
-  /-- The wait before this dial. -/
-  delayMs : Nat
-  deriving DecidableEq, Repr
-
-/-- The address ranker: the dial schedule of a peer's addresses. -/
-structure AddressRanker where
-  /-- The schedule, in dial order. -/
-  rank : List Multiaddr → List AddrDelay
-
-end Libp2p.Host.Mock.Core
diff --git a/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean b/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
index a399021b..2597e5d6 100644
--- a/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
+++ b/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
@@ -1,20 +1,22 @@
 import Conc
 import Streams
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 
 /-!
 # Mock: the surface of `libp2p/negotiate` that the host uses
 
-W5.5 (`libp2p/negotiate`) has not merged, so the host builds against a
-mock (RULES.md, "Working ahead of the tree"). The mock imports nothing
-from the real package, and it states no axiom. Both entries fail with
-the name of the package: no body negotiates, runs a handshake, or opens
-a session.
+W5.5 (`libp2p/negotiate`) merged over its own mock of `libp2p/core`,
+so its seam types are not the ones of `Libp2p.Core` that the host
+takes. The host keeps this mock until the negotiate package takes the
+real core (issue #53); the swap is issue #70 (RULES.md, "Working ahead
+of the tree"). The mock imports nothing from the negotiate package,
+and it states no axiom. Both entries fail with the name of the
+package: no body negotiates, runs a handshake, or opens a session.
 
-The negotiate ARCHITECTURE freezes `Negotiate.upgrade`. The host needs
-two calls beside it, and the negotiate ARCHITECTURE gains both in this
-unit:
+The host needs two calls beside `Negotiate.upgrade`. The merged
+package has neither, so the swap retypes the host's use of them
+(issue #70):
 
 * `upgradeWith`, the upgrade with a checkpoint after the handshake and
   before the muxer stage. The host's gater and resource manager decide
@@ -26,16 +28,13 @@ unit:
   serves each inbound stream through it, and `newStream` negotiates
   each outbound one. The bytes it reads past the selecting message go
   to the stream's front (§4.7, `Stream.prependBytes`).
-
-At the integration, the host imports `Libp2p.Negotiate`, and the module
-goes.
 -/
 
 set_option autoImplicit false
 
 namespace Libp2p.Host.Mock.Negotiate
 
-open Conc Streams Libp2p.Identity Libp2p.Host.Mock.Core
+open Conc Streams Libp2p.Identity Libp2p.Core
 
 /-- How a stream negotiation failed. The host reads two arms: the end of
 the stream before a selection, an orderly end, and the empty proposal
diff --git a/packages/libp2p/host/Libp2p/Host/Policy.lean b/packages/libp2p/host/Libp2p/Host/Policy.lean
index 16665b84..b2a0e513 100644
--- a/packages/libp2p/host/Libp2p/Host/Policy.lean
+++ b/packages/libp2p/host/Libp2p/Host/Policy.lean
@@ -1,4 +1,4 @@
-import Libp2p.Host.Mock.Core
+import Libp2p.Core.Policy
 
 /-!
 # The policy values
@@ -17,7 +17,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Host.Policy
 
-open Libp2p.Host.Mock.Core
+open Libp2p.Core
 
 /-- The default gater: it allows every dial, every inbound connection,
 and every proved peer. -/
diff --git a/packages/libp2p/host/Libp2p/Host/Registry.lean b/packages/libp2p/host/Libp2p/Host/Registry.lean
index 5954fdb3..935cf7dc 100644
--- a/packages/libp2p/host/Libp2p/Host/Registry.lean
+++ b/packages/libp2p/host/Libp2p/Host/Registry.lean
@@ -1,6 +1,6 @@
 import Std.Data.HashMap
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 
 /-!
 # The session and handler registries
@@ -44,7 +44,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
-open Libp2p.Identity Libp2p.Host.Mock.Core
+open Libp2p.Identity Libp2p.Core
 
 /-! ## The session table -/
 
diff --git a/packages/libp2p/host/Libp2p/Host/Swarm.lean b/packages/libp2p/host/Libp2p/Host/Swarm.lean
index 2294d866..e22f2e98 100644
--- a/packages/libp2p/host/Libp2p/Host/Swarm.lean
+++ b/packages/libp2p/host/Libp2p/Host/Swarm.lean
@@ -2,7 +2,7 @@ import Std.Data.HashMap
 import Conc
 import Streams
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 import Libp2p.Host.Mock.Negotiate
 import Libp2p.Host.Error
 import Libp2p.Host.Registry
@@ -69,10 +69,11 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
--- The mocks of the unmerged packages (RULES.md, "Working ahead of the
--- tree"); `Negotiate.Error` resolves through `Libp2p.Host.Mock`.
+-- The negotiate mock stays until `libp2p/negotiate` takes the real core
+-- seams (issue #53); `Negotiate.Error` resolves through
+-- `Libp2p.Host.Mock`.
 open Conc Streams Multiformats Libp2p.Host.Mock Libp2p.Identity
-  Libp2p.Host.Mock.Core Libp2p.Host.Mock.Negotiate
+  Libp2p.Core Libp2p.Host.Mock.Negotiate
 
 /-- A failure of a task that no caller awaits: an inbound upgrade, a
 session that ended badly, an inbound stream. -/
diff --git a/packages/libp2p/host/docs/ARCHITECTURE.md b/packages/libp2p/host/docs/ARCHITECTURE.md
index 93db8fb6..6b93d302 100644
--- a/packages/libp2p/host/docs/ARCHITECTURE.md
+++ b/packages/libp2p/host/docs/ARCHITECTURE.md
@@ -24,7 +24,7 @@ libp2p group is §7, row 10).
 | `Libp2p/Host/Swarm.lean` | `Config`, the `Host` state, `dial`, `dialPeer`, `startListening`, `newStream`, the accept loop, the upgrade pipeline, and stream serving |
 | `Libp2p/Host/Shutdown.lean` | `Host.close`, the §5.5 sequence |
 | `Libp2p/Host/Policy.lean` | the permissive default gater, and the permissive and denying test doubles the core pair assigned here; the default resource manager (admits everything) and the default ranker (keeps the order, no delay) |
-| `Libp2p/Host/Mock/{Core,Negotiate}.lean` | the mocks of W5.2 and W5.5 until they merge (see "The mocks") |
+| `Libp2p/Host/Mock/Negotiate.lean` | the mock of the W5.5 surface the host calls, until the negotiate package takes the real core (see "The mock") |
 
 All declarations live in the `Libp2p.Host` namespace, and the root
 module re-exports the public submodules.
@@ -298,22 +298,23 @@ fixes them as follows.
   1b milestone. A fault of a joined task does not stop the sequence,
   and `close` throws the first fault at the end.
 
-## The mocks
+## The mock
 
-W5.2 (`libp2p/core`) and W5.5 (`libp2p/negotiate`) have not merged,
-so the package builds against mocks of their frozen surfaces (RULES.md,
-"Working ahead of the tree"), under `Libp2p/Host/Mock/`. A type is a
-copy of the frozen shape; an operation is `opaque`, and its body fails
-with the name of the missing package. No body negotiates or opens a
-session, and the mocks state no axiom. The host modules open
-`Libp2p.Host.Mock`, so `Core.Error` and `Negotiate.upgradeWith` resolve
-as they will against the real packages, and the integration swaps the
-imports and drops the `open`. The keys and the peer id come from the
-merged `libp2p/identity`.
+The seam types come from `libp2p/core`. W5.5 (`libp2p/negotiate`)
+merged over its own mock of `libp2p/core`, so its upgrader takes seam
+values of another type than the host holds. The host keeps a mock of
+the negotiate surface, `Libp2p/Host/Mock/Negotiate.lean`, until the
+negotiate package takes the real core (issue #53). Its operations are
+`opaque`, and each body fails with the name of the package; it states
+no axiom. Swarm opens `Libp2p.Host.Mock`, so `Negotiate.upgradeWith`
+resolves as it will against the real package. The swap (issue #70)
+is a retype: the merged upgrader takes no `admit` checkpoint and
+exports no `negotiateStream`.
 
 Every upgrade runs through the negotiate mock and fails there, and the
-legs also need the Noise and yamux values (W5.3, W5.4), so the unit 1b
-milestones run at the integration. Unit 1a runs in full.
+legs also need the Noise and yamux values on the real core (issues
+#76 and #77), so the unit 1b milestones run after those swaps. Unit
+1a runs in full.
 
 ## What the package must not depend on
 
diff --git a/packages/libp2p/host/docs/PLAN.md b/packages/libp2p/host/docs/PLAN.md
index 647da5dd..c058f57c 100644
--- a/packages/libp2p/host/docs/PLAN.md
+++ b/packages/libp2p/host/docs/PLAN.md
@@ -24,9 +24,9 @@ so unit 1a lands while the upgrader finishes. W5.2 sits outside the
 root row and reaches this unit through the root chain, which finishes
 it before W5.5.
 
-Units 0 and 1a are done, and unit 1b's code builds against the mocks
-of W5.2 and W5.5 (the package ARCHITECTURE, "The mocks"), with the
-merged `libp2p/identity`. The suite is `Tests/Host.lean`; the dedup
+Units 0 and 1a are done. Unit 1b's code builds over `libp2p/core`
+and `libp2p/identity`, and against a mock of W5.5 (the package
+ARCHITECTURE, "The mock"). The suite is `Tests/Host.lean`; the dedup
 rule also carries theorems in `Libp2p/Host/Dedup.lean`. A host
 upgrades through `libp2p/negotiate`, so the unit 1b milestones run at
 the integration, and the suite names each one as a skip until then. Unit 1b needs two

From 34da9b10bce8a0da3da71b2931a950e29009cdfb Mon Sep 17 00:00:00 2001
From: Leo Lara <leo@leolara.me>
Date: Mon, 9 Nov 2026 10:05:26 +0700
Subject: [PATCH 2/2] docs(host): state the negotiate mock stay after #82
 landed the retype

---
 Tests/Host.lean                               | 10 +++----
 .../host/Libp2p/Host/Mock/Negotiate.lean      | 16 +++++-----
 packages/libp2p/host/Libp2p/Host/Swarm.lean   |  5 ++--
 packages/libp2p/host/docs/ARCHITECTURE.md     | 29 +++++++++----------
 4 files changed, 29 insertions(+), 31 deletions(-)

diff --git a/Tests/Host.lean b/Tests/Host.lean
index 46547faf..afc1051b 100644
--- a/Tests/Host.lean
+++ b/Tests/Host.lean
@@ -19,10 +19,10 @@ here, since the rule never reads it.
 Unit 1b runs hosts over the sim transport, with the real
 `Noise.securityProtocol` and `Mux.yamux` values (PRINCIPLES 1.4). Every
 host derives its peer id through `libp2p/identity`, and the upgrade runs
-through `libp2p/negotiate`. Those packages merged over mocks of
-`libp2p/core`, so the legs wait for their seam swaps: issues #53
-(negotiate), #76 (Noise), #77 (`Mux.yamux`), and the negotiate swap of
-the host, issue #70. Until then the suite names each leg as a skip.
+through `libp2p/negotiate`. The real packages have landed (#53, #76,
+#77), and the upgrade still runs through the negotiate mock of the
+host, whose entries fail. The legs wait for the host swap of issue
+#70. Until then the suite names each leg as a skip.
 -/
 
 set_option autoImplicit false
@@ -300,6 +300,6 @@ def Host.run (r : Runner) : IO Unit := do
   (peerstoreChecks r).run
   errorChecks r
   for leg in swarmLegs do
-    r.skip s!"host: {leg}" "needs the seam swaps of issues #53, #76, #77, and #70"
+    r.skip s!"host: {leg}" "needs the negotiate swap of the host, issue #70"
 
 end Tests
diff --git a/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean b/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
index 2597e5d6..b5d1bf2b 100644
--- a/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
+++ b/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
@@ -6,13 +6,12 @@ import Libp2p.Core
 /-!
 # Mock: the surface of `libp2p/negotiate` that the host uses
 
-W5.5 (`libp2p/negotiate`) merged over its own mock of `libp2p/core`,
-so its seam types are not the ones of `Libp2p.Core` that the host
-takes. The host keeps this mock until the negotiate package takes the
-real core (issue #53); the swap is issue #70 (RULES.md, "Working ahead
-of the tree"). The mock imports nothing from the negotiate package,
-and it states no axiom. Both entries fail with the name of the
-package: no body negotiates, runs a handshake, or opens a session.
+The merged `libp2p/negotiate` takes the seam types of `Libp2p.Core`
+(issue #53), so this mock carries those types too. The mock stays
+until the host swap of issue #70 lands (RULES.md, "Working ahead of
+the tree"). It imports nothing from the negotiate package, and it
+states no axiom. Both entries fail with the name of the package: no
+body negotiates, runs a handshake, or opens a session.
 
 The host needs two calls beside `Negotiate.upgrade`. The merged
 package has neither, so the swap retypes the host's use of them
@@ -20,7 +19,8 @@ package has neither, so the swap retypes the host's use of them
 
 * `upgradeWith`, the upgrade with a checkpoint after the handshake and
   before the muxer stage. The host's gater and resource manager decide
-  there, by the proved peer (the core mock, "The policy shapes"); go's
+  there, by the proved peer (the core ARCHITECTURE, "The policy
+  shapes"); go's
   upgrader calls `InterceptSecured` at the same place
   (`vendor/go-libp2p/p2p/net/upgrader/upgrader.go`, line 176). A refusal is a
   value, `UpgradeResult.refused`, and no `Core.Error` arm (§3.5).
diff --git a/packages/libp2p/host/Libp2p/Host/Swarm.lean b/packages/libp2p/host/Libp2p/Host/Swarm.lean
index e22f2e98..54ffc2ea 100644
--- a/packages/libp2p/host/Libp2p/Host/Swarm.lean
+++ b/packages/libp2p/host/Libp2p/Host/Swarm.lean
@@ -69,9 +69,8 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
--- The negotiate mock stays until `libp2p/negotiate` takes the real core
--- seams (issue #53); `Negotiate.Error` resolves through
--- `Libp2p.Host.Mock`.
+-- The negotiate mock stays until the host swap of issue #70;
+-- `Negotiate.Error` resolves through `Libp2p.Host.Mock`.
 open Conc Streams Multiformats Libp2p.Host.Mock Libp2p.Identity
   Libp2p.Core Libp2p.Host.Mock.Negotiate
 
diff --git a/packages/libp2p/host/docs/ARCHITECTURE.md b/packages/libp2p/host/docs/ARCHITECTURE.md
index 6b93d302..10b82a98 100644
--- a/packages/libp2p/host/docs/ARCHITECTURE.md
+++ b/packages/libp2p/host/docs/ARCHITECTURE.md
@@ -24,7 +24,7 @@ libp2p group is §7, row 10).
 | `Libp2p/Host/Swarm.lean` | `Config`, the `Host` state, `dial`, `dialPeer`, `startListening`, `newStream`, the accept loop, the upgrade pipeline, and stream serving |
 | `Libp2p/Host/Shutdown.lean` | `Host.close`, the §5.5 sequence |
 | `Libp2p/Host/Policy.lean` | the permissive default gater, and the permissive and denying test doubles the core pair assigned here; the default resource manager (admits everything) and the default ranker (keeps the order, no delay) |
-| `Libp2p/Host/Mock/Negotiate.lean` | the mock of the W5.5 surface the host calls, until the negotiate package takes the real core (see "The mock") |
+| `Libp2p/Host/Mock/Negotiate.lean` | the mock of the W5.5 surface the host calls, until the host swap of issue #70 (see "The mock") |
 
 All declarations live in the `Libp2p.Host` namespace, and the root
 module re-exports the public submodules.
@@ -300,21 +300,20 @@ fixes them as follows.
 
 ## The mock
 
-The seam types come from `libp2p/core`. W5.5 (`libp2p/negotiate`)
-merged over its own mock of `libp2p/core`, so its upgrader takes seam
-values of another type than the host holds. The host keeps a mock of
-the negotiate surface, `Libp2p/Host/Mock/Negotiate.lean`, until the
-negotiate package takes the real core (issue #53). Its operations are
-`opaque`, and each body fails with the name of the package; it states
-no axiom. Swarm opens `Libp2p.Host.Mock`, so `Negotiate.upgradeWith`
-resolves as it will against the real package. The swap (issue #70)
-is a retype: the merged upgrader takes no `admit` checkpoint and
-exports no `negotiateStream`.
+The seam types come from `libp2p/core`. `libp2p/negotiate` takes the
+real core too (issue #53), so its upgrader takes the values the host
+holds. The host keeps a mock of the negotiate surface,
+`Libp2p/Host/Mock/Negotiate.lean`, until the host swap of issue #70.
+Its operations are `opaque`, and each body fails with the name of the
+package; it states no axiom. Swarm opens `Libp2p.Host.Mock`, so
+`Negotiate.upgradeWith` resolves as it will against the real package.
+The swap (issue #70) is a retype: the merged upgrader takes no `admit`
+checkpoint and exports no `negotiateStream`.
 
-Every upgrade runs through the negotiate mock and fails there, and the
-legs also need the Noise and yamux values on the real core (issues
-#76 and #77), so the unit 1b milestones run after those swaps. Unit
-1a runs in full.
+Every upgrade runs through the negotiate mock and fails there, so the
+unit 1b milestones run after the host swap of issue #70. The Noise and
+yamux values are on the real core (issues #76 and #77). Unit 1a runs
+in full.
 
 ## What the package must not depend on