refactor(host): take the seam types from libp2p/core

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`. 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
 
 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 negotiate swap of the host, issue #70"
 
 end Tests

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"). -/

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`),

packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean

@@ -1,41 +1,40 @@
 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.
+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 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
-  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).
 * `negotiateStream`, multistream-select over one muxed stream. The host
   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

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. -/

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

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,10 @@ 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 the host swap of issue #70;
+-- `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. -/

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 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.
@@ -298,22 +298,22 @@ 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`. `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 (W5.3, W5.4), so the unit 1b
-milestones run at the integration. 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