refactor(negotiate): run the upgrader over the seam types of libp2p/core

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

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

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

packages/libp2p/negotiate/Libp2p/Negotiate/Message.lean

@@ -283,24 +283,24 @@ 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
 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