diff --git a/Tests/Host.lean b/Tests/Host.lean index 7d444cc3..662dd862 100644 --- a/Tests/Host.lean +++ b/Tests/Host.lean @@ -3,6 +3,11 @@ import Tests.Support import Conc import Streams import Multiformats +import Libp2p.Identity +import Libp2p.Core +import Libp2p.Security +import Libp2p.Mux +import Libp2p.Negotiate import Libp2p.Host /-! @@ -16,13 +21,11 @@ pure update functions, by value or under an `OnceRef`, with no connection in the loop. The session handle of a table entry is a `Nat` 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`. 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. +Unit 1b: hosts over the test values of root §3.1 (PRINCIPLES 1.4): the +sim transport, the fixed-key test value `Noise.fixedKeyProtocol`, and +a test clock that drives the upgrade deadline, so no check waits on the +wall clock. The muxer is `Mux.yamux`. Each host hands its failures to a +channel that the check reads. -/ set_option autoImplicit false @@ -278,18 +281,360 @@ private def errorChecks (r : Runner) : IO Unit := do for (e, line) in arms do r.check s!"Host.Error renders {line}" (toString e == line) -/-! ## Unit 1b -/ - -/-- The unit 1b legs of the plan. Each one needs a host, and a host -derives its peer id through `libp2p/identity` and upgrades through -`libp2p/negotiate` (module doc). -/ -private def swarmLegs : List String := - ["the upgrade pipeline in both directions, with the identity check", - "the host's own answers: dial to self, no address, no transport, unknown protocol, failing handler, after close", - "the policy doubles: a denying gater refuses a dial and an inbound connection", - "the silent peer at the deadline, and close reaching a parked upgrade", - "the shutdown stages of §5.5 in order", - "the leftover hand-over on a served stream"] +/-! ## Unit 1b: hosts over the sim -/ + +section Swarm + +open Streams Libp2p.Security +open Libp2p.Host (Host Config Failure Stage) + +/-- `n` bytes of the value `v`. -/ +private def fill (n : Nat) (v : UInt8) : ByteArray := ⟨Array.replicate n v⟩ + +/-- A Noise configuration from an Ed25519 identity byte. The static key +byte follows from it. -/ +private def cfgOf (idByte : UInt8) : Async Noise.Config := do + let .ok identity := PrivKey.ofData? .ed25519 (fill 32 idByte) + | throw <| IO.userError "test identity does not build" + let some static := Noise.Bytes32.ofByteArray? (fill 32 (idByte + 100)) + | throw <| IO.userError "test static key is not 32 bytes" + return { identity, static } + +/-- The fixed-key Noise value of the identity byte `idByte`: its +ephemeral keys come from an `Rng` seeded with 32 copies of +`idByte + 50` (root §3.1). -/ +private def noiseOf (idByte : UInt8) : Async SecurityProtocol := + return Noise.fixedKeyProtocol (← cfgOf idByte) (fill 32 (idByte + 50)) + +/-- The echo protocol of the suite. The `/test/` prefix keeps it apart +from every real id. -/ +private def echoId : ProtocolId := ⟨"/test/echo"⟩ + +/-- A protocol whose handler fails at once. -/ +private def failId : ProtocolId := ⟨"/test/fail"⟩ + +/-- An id no host serves. -/ +private def unknownId : ProtocolId := ⟨"/test/unknown"⟩ + +/-- Read until the end of the stream, or a reset. -/ +private def readAll (s : Stream) : Async ByteArray := do + let mut acc := ByteArray.empty + repeat + match ← s.read with + | .ok (some b) => acc := acc ++ b + | _ => break + return acc + +/-- The echo handler: read to the end, write it back, close. -/ +private def echoHandler : StreamHandler where + id := echoId + handle _ s := do + let got ← readAll s + discard <| s.write got + s.close + +/-- The id of the handler that records its context. -/ +private def ctxId : ProtocolId := ⟨"/test/ctx"⟩ + +/-- The failing handler. -/ +private def failHandler : StreamHandler where + id := failId + handle _ _ := throw (.protocol "the test handler fails") + +/-- A host of the suite on `net`, its peer id, and the channel its +failures arrive on. -/ +private def mkHost (net : Sim.Net) (idByte : UInt8) (tc : TestClock) + (gater : ConnectionGater := Policy.permissiveGater) : + Async (Host × Chan Failure) := do + let cfg ← cfgOf idByte + let failures : Chan Failure ← Chan.new 16 + let config : Config := { + identity := cfg.identity + transports := [net.transport] + security := [← noiseOf idByte] + muxers := [Libp2p.Mux.yamux] + handlers := [echoHandler, failHandler] + gater + clock := tc.clock + onFailure := fun f => discard (failures.trySend f) } + match ← (Host.new config : BaseIO _) with + | .ok h => return (h, failures) + | .error _ => throw <| IO.userError "test host does not build" + +/-- The address with `/p2p/` after it. -/ +private def withPeer (a : Multiaddr) (p : PeerId) : Async Multiaddr := do + match a.encapsulate (← ma s!"/p2p/{p}") with + | .ok full => return full + | .error _ => throw <| IO.userError "the /p2p address does not build" + +/-- Start a listener, or fail the run. -/ +private def listenOn (h : Host) (text : String) : Async Multiaddr := do + match ← h.startListening (← ma text) with + | .ok a => return a + | .error e => throw <| IO.userError s!"listen failed: {e}" + +/-- One echo round trip from `h` to `peer`: the stream negotiates +`echoId`, the bytes come back, and the stream ends. -/ +private def echoOnce (h : Host) (peer : PeerId) (payload : String) : Async Bool := do + match ← h.newStream peer [echoId] with + | .error _ => return false + | .ok (id, s) => + discard <| s.write payload.toUTF8 + s.close + return id == echoId && (← readAll s) == payload.toUTF8 + +/-- The pipeline in both directions: a dial with `/p2p`, an echo each +way, a redial that reuses the session, and an identity mismatch. -/ +private def pipelineChecks (r : Runner) : Async Unit := do + let net ← Sim.Net.new + let tc ← TestClock.new + let (a, _) ← mkHost net 1 tc + let (b, _) ← mkHost net 2 tc + let addrA ← listenOn a "/memory/101" + let addrB ← listenOn b "/memory/102" + -- B dials A by its address and peer id. + match ← b.dial (← withPeer addrA a.localPeer) with + | .ok p => r.check "host: a dial proves the listener's peer id" (p == a.localPeer) + | .error e => r.check s!"host: a dial succeeds ({e})" false + r.check "host: the dialer serves the session" (← (b.connected a.localPeer : BaseIO Bool)) + r.check "host: the dialer's stream echoes" (← echoOnce b a.localPeer "ping") + -- The listener committed the session too, and it opens streams back. + r.check "host: the listener's stream echoes" (← echoOnce a b.localPeer "pong") + -- A served stream gets the session's context: the proved peer, and + -- the connection's remote address. B dialed, so B's connection names + -- `addrA` as its remote end. A's connection names the sim port of + -- B's dial. + let seenA : Chan StreamContext ← Chan.new 1 + let seenB : Chan StreamContext ← Chan.new 1 + let recorder (seen : Chan StreamContext) : StreamHandler := + { id := ctxId, handle := fun ctx s => do discard <| seen.send ctx; s.close } + a.setHandler (recorder seenA) + b.setHandler (recorder seenB) + discard <| b.newStream a.localPeer [ctxId] + discard <| a.newStream b.localPeer [ctxId] + match ← seenA.recv, ← seenB.recv with + | some ca, some cb => + r.check "host: the handler context names the proved peer" + (ca.remotePeer == b.localPeer && cb.remotePeer == a.localPeer) + r.check "host: the dialer's handler context names the listener's address" + (cb.remoteAddr == addrA && ca.remoteAddr != addrA) + | _, _ => r.check "host: both handlers saw a context" false + -- A redial reuses the live session, and the peerstore grows nothing. + match ← b.dial (← withPeer addrA a.localPeer) with + | .ok p => r.check "host: a redial reuses the session" (p == a.localPeer) + | .error e => r.check s!"host: a redial succeeds ({e})" false + r.check "host: the dial stored the address once" + ((← (b.addrsOf a.localPeer : BaseIO (List Multiaddr))) == [addrA]) + -- A dial that expects another peer fails at the identity check. + let (c, _) ← mkHost net 3 tc + match ← c.dial addrB (peer := some a.localPeer) with + | .error (.upgrade (.authentication _)) => + r.check "host: an identity mismatch fails with authentication" true + | _ => r.check "host: an identity mismatch fails with authentication" false + r.check "host: the mismatched dial leaves no session" !(← (c.connected b.localPeer : BaseIO Bool)) + c.close + b.close + a.close + tc.close + +/-- The host's own answers: a dial to itself, a peer with no address, +an address with no transport part, an unknown protocol, a failing +handler, and the calls after `close`. -/ +private def answerChecks (r : Runner) : Async Unit := do + let net ← Sim.Net.new + let tc ← TestClock.new + let (a, failsA) ← mkHost net 4 tc + let (b, _) ← mkHost net 5 tc + let addrA ← listenOn a "/memory/111" + r.check "host: a dial to our own id fails" + ((← b.dial addrA (peer := some b.localPeer)) matches .error .dialSelf) + r.check "host: a peer with no address fails" + ((← b.dialPeer a.localPeer) matches .error (.noAddresses _)) + r.check "host: a /p2p address alone has no transport" + ((← b.dial (← ma s!"/p2p/{a.localPeer}")) matches .error (.noTransport _)) + -- `dialPeer` walks the peerstore. + b.addAddrs a.localPeer [addrA] + r.check "host: dialPeer dials the peerstore address" + ((← b.dialPeer a.localPeer) matches .ok _) + -- The host answers `na` to an unknown protocol, and the session stays. + r.check "host: an unknown protocol fails the stream" + ((← b.newStream a.localPeer [unknownId]) matches .error (.stream _)) + r.check "host: the session stays after an unknown protocol" + (← echoOnce b a.localPeer "still here") + -- A handler set on a running host serves the next stream. + (a.setHandler { echoHandler with id := unknownId } : BaseIO Unit) + r.check "host: a handler set at runtime serves the next stream" + ((← b.newStream a.localPeer [unknownId]) matches .ok _) + -- A failing handler resets the stream and reaches A's owner. The + -- session stays. A sends its reset right after its negotiation reply, + -- and a reset may drop the bytes in flight (`Streams.Error.reset`). + -- So B sees the reset in its first read. Or the reset comes before B + -- reads the reply, and B's negotiation ends with `closed`. + let resetSeen ← match ← b.newStream a.localPeer [failId] with + | .error (.stream (.closed _)) => pure true + | .error _ => pure false + | .ok (_, s) => pure ((← s.read) matches .error .reset) + r.check "host: a handler failure resets the stream" resetSeen + match ← failsA.recv with + | some f => + r.check "host: a handler failure reaches the owner" + (f.peer == some b.localPeer && f.protocol == some failId && + f.error matches .stream (.protocol _)) + | none => r.check "host: a handler failure reaches the owner" false + r.check "host: the session stays after a handler failure" + (← echoOnce b a.localPeer "and here") + b.close + a.close + r.check "host: a dial after close fails with closing" + ((← b.dial addrA) matches .error .closing) + r.check "host: a listen after close fails with closing" + ((← a.startListening (← ma "/memory/112")) matches .error .closing) + tc.close + +/-- A gater that passes the dial and the accept, and refuses every +proved peer: only the secured checkpoint answers no. -/ +private def securedOnlyGater : ConnectionGater := + { Policy.permissiveGater with allowSecured := fun _ _ _ _ => pure false } + +/-- The policy doubles. A denying gater refuses a dial and an accepted +connection. The permissive gater passes both, in the other checks. A +gater that refuses at the secured checkpoint refuses after the +handshake, and the scope and the secure connection close with it. -/ +private def policyChecks (r : Runner) : Async Unit := do + let net ← Sim.Net.new + let tc ← TestClock.new + let (open_, _) ← mkHost net 6 tc + let (shut, failsShut) ← mkHost net 7 tc (gater := Policy.denyingGater) + let addrOpen ← listenOn open_ "/memory/121" + let addrShut ← listenOn shut "/memory/122" + r.check "host: a denying gater refuses a dial" + ((← shut.dial addrOpen) matches .error (.gated .dial)) + -- The refused inbound connection closes before any byte moves. The + -- dialer meets the close as the end of its read (`closed`), or as a + -- failed write, which is a fault (`Connection.write`, §3.5). The + -- order of its write and the close decides which. + let refused ← try + pure ((← open_.dial addrShut) matches .error (.upgrade (.closed _))) + catch _ => pure true + r.check "host: a denying gater refuses an inbound connection" refused + r.check "host: the refusal is no failure" (← (failsShut.tryRecv : BaseIO _)).isNone + r.check "host: the refused inbound peer has no session" + !(← (shut.connected open_.localPeer : BaseIO Bool)) + -- The secured checkpoint: the dial and the handshake pass, and the + -- checkpoint refuses the proved peer before the muxer stage. + let (picky, failsPicky) ← mkHost net 13 tc (gater := securedOnlyGater) + r.check "host: the secured checkpoint refuses an outbound peer" + ((← picky.dial addrOpen) matches .error (.gated .secured)) + r.check "host: the outbound secured refusal leaves no session" + !(← (picky.connected open_.localPeer : BaseIO Bool)) + let addrPicky ← listenOn picky "/memory/123" + -- The dialer's handshake completes, then its muxer stage meets the + -- close. A failed write is a fault (§3.5), as above. + let refusedIn ← try + pure ((← open_.dial addrPicky) matches .error (.upgrade _)) + catch _ => pure true + r.check "host: the secured checkpoint refuses an inbound peer" refusedIn + r.check "host: the secured refusal is no failure" (← (failsPicky.tryRecv : BaseIO _)).isNone + r.check "host: the inbound secured refusal leaves no session" + !(← (picky.connected open_.localPeer : BaseIO Bool)) + picky.close + open_.close + shut.close + tc.close + +/-- True when `raw` reaches its end within eight reads. The host's +responder writes its multistream header before it reads, as go's +listener does (`Negotiate.negotiate`). So a raw peer can read that +header before the end. A peer that sends past the bound counts as no +end. -/ +private def endsSoon (raw : Connection) : Async Bool := do + for _ in [0:8] do + if (← raw.read).isNone then return true + return false + +/-- The silent peer, at host level (PRINCIPLES 5.4): a raw connection +that sends nothing parks the inbound upgrade. The deadline fails it, +and the failure reaches the owner. In a second run, `close` reaches +the parked upgrade through the pending list, and every join returns. -/ +private def silentPeerChecks (r : Runner) : Async Unit := do + let net ← Sim.Net.new + let tc ← TestClock.new + let (a, failsA) ← mkHost net 8 tc + let addrA ← listenOn a "/memory/131" + let some raw ← net.transport.dial addrA | throw <| IO.userError "raw dial failed" + -- The upgrade arms its deadline before its first read parks. + discard tc.nextTimer + tc.advance Streams.unauthDeadlineMs + match ← failsA.recv with + | some f => + r.check "host: a silent peer fails at the deadline" + (f.peer.isNone && f.error matches .upgrade (.timeout _)) + | none => r.check "host: a silent peer fails at the deadline" false + r.check "host: the deadline closed the silent connection" (← endsSoon raw) + -- A second silent peer, and `close` before the deadline. + let some raw ← net.transport.dial addrA | throw <| IO.userError "raw dial failed" + discard tc.nextTimer + a.close + r.check "host: close reaches a parked upgrade, and returns" (← endsSoon raw) + tc.close + +/-- The shutdown order (§5.5): the stages run in sequence, and every +join returns, with a listener whose accept parks, a live session, and +a pending connection. -/ +private def shutdownChecks (r : Runner) : Async Unit := do + let net ← Sim.Net.new + let tc ← TestClock.new + let (a, _) ← mkHost net 9 tc + let (b, _) ← mkHost net 10 tc + let addrA ← listenOn a "/memory/141" + discard <| listenOn a "/memory/142" + discard <| b.dial addrA + let some raw ← net.transport.dial addrA | throw <| IO.userError "raw dial failed" + let stages : OnceRef (List Stage) ← OnceRef.new [] + a.close (onStage := fun s => stages.update (· ++ [s])) + r.check "host: the shutdown runs the stages of §5.5 in order" + ((← (stages.get : BaseIO (List Stage))) == + [.flag, .listeners, .pending, .sessions, .sessionLoops, .hostTasks]) + r.check "host: the shutdown closed the pending connection" (← endsSoon raw) + r.check "host: a closed listener refuses a dial" + ((← b.dial addrA (peer := none)) matches .error _) + -- A second close finds nothing left, and returns. + a.close + b.close + tc.close + +/-- The leftover hand-over on a served stream (§4.7, §5.6). A peer +writes its stream header, its proposal, and data in one write. The +handler gets the data in its first read. The peer runs the plain +upgrader of `libp2p/negotiate`, so the host's listen path meets a peer +that is no host. -/ +private def handOverChecks (r : Runner) : Async Unit := do + let net ← Sim.Net.new + let tc ← TestClock.new + let (a, _) ← mkHost net 11 tc + let addrA ← listenOn a "/memory/151" + let noise ← noiseOf 12 + let some conn ← net.transport.dial addrA | throw <| IO.userError "dial failed" + match ← (Libp2p.Negotiate.upgradeWith tc.clock .initiator conn .empty (some a.localPeer) + [noise] [Libp2p.Mux.yamux]).run with + | .error e => r.check s!"host: a plain upgrader reaches the host ({e})" false + | .ok (session, _) => + match ← (session.openStream echoId).run with + | .error e => r.check s!"host: the stream opens ({e})" false + | .ok s => + let msg (t : String) : ByteArray := Bytes.ofNatList (Libp2p.Negotiate.encodeText t) + discard <| s.write (msg "/multistream/1.0.0" ++ msg "/test/echo" ++ "coalesced".toUTF8) + s.close + -- The echo handler answers the header and the id, then the bytes. + let back ← readAll s + r.check "host: the bytes behind the proposal reach the handler" + (back == msg "/multistream/1.0.0" ++ msg "/test/echo" ++ "coalesced".toUTF8) + discard session.close.toBaseIO + discard session.join.run + a.close + tc.close + +end Swarm def Host.run (r : Runner) : IO Unit := do r.section "host" "(packages/libp2p/host/docs/PLAN.md, test milestones, units 1a and 1b)" @@ -299,7 +644,10 @@ def Host.run (r : Runner) : IO Unit := do (handlerChecks r).run (peerstoreChecks r).run errorChecks r - for leg in swarmLegs do - r.skip s!"host: {leg}" "needs the negotiate swap of the host, issue #70" + for (label, act) in [("pipeline", pipelineChecks r), ("answers", answerChecks r), + ("policy", policyChecks r), ("silent peer", silentPeerChecks r), + ("shutdown", shutdownChecks r), ("hand-over", handOverChecks r)] do + try act.run + catch e => r.check s!"host {label}: runs ({e})" false end Tests \ No newline at end of file diff --git a/Tests/HostPair.lean b/Tests/HostPair.lean new file mode 100644 index 00000000..17770df2 --- /dev/null +++ b/Tests/HostPair.lean @@ -0,0 +1,83 @@ +import Conc +import Streams +import Libp2p.Identity +import Libp2p.Security +import Libp2p.Mux +import Libp2p.Host +import Multiformats.Multiaddr + +/-! +# Two hosts over the sim + +The protocol suites run their handlers between two real hosts, on the +test values of root §3.1 (PRINCIPLES 1.4): the in-memory sim transport, +the fixed-key Noise value with Ed25519 identities from one byte each, +and a test clock. The muxer is yamux. The server listens on +`/memory/4100`, and the client holds a session to it. +-/ + +set_option autoImplicit false + +namespace Tests.HostPair + +open Conc (Async Clock OnceRef TestClock) +open Libp2p.Host (Host Failure) + +/-- A host on `net` and `clock`: the fixed-key Noise value with an +Ed25519 identity from one byte, yamux, and the sim transport. The +ephemeral keys come from an `Rng` seeded with 32 copies of +`idByte + 50`. Its failures go to `failures`. -/ +def mkHost (net : Streams.Sim.Net) (clock : Clock) (idByte : UInt8) + (failures : OnceRef (List Failure)) : Async Host := do + let .ok identity := Libp2p.Identity.PrivKey.ofData? .ed25519 ⟨Array.replicate 32 idByte⟩ + | throw (IO.userError "test identity does not build") + let some static := Libp2p.Security.Noise.Bytes32.ofByteArray? ⟨Array.replicate 32 (idByte + 100)⟩ + | throw (IO.userError "test static key is not 32 bytes") + let noise := Libp2p.Security.Noise.fixedKeyProtocol { identity, static } + ⟨Array.replicate 32 (idByte + 50)⟩ + match ← (Host.new { + identity + transports := [net.transport] + security := [noise] + muxers := [Libp2p.Mux.yamux] + clock + onFailure := fun f => failures.update (f :: ·) } : BaseIO _) with + | .ok h => return h + | .error _ => throw (IO.userError "test host does not build") + +/-- Two hosts over a new sim net: the server listens, and the client +holds a session to it. -/ +structure Pair where + client : Host + server : Host + /-- The peer id the client proved for the server. -/ + serverPeer : Libp2p.Identity.PeerId + /-- The address the server listens on. -/ + serverAddr : Multiformats.Multiaddr + /-- The failures of the server's owned tasks, newest first. -/ + failures : OnceRef (List Failure) + /-- The test clock both hosts run on. `Pair.close` closes it. -/ + clock : TestClock + +/-- The pair. With `split`, the sim delivers each byte as its own read. -/ +def hostPair (split : Bool := false) : Async Pair := do + let net ← Streams.Sim.Net.new split + let tc ← TestClock.new + let failures ← OnceRef.new [] + let client ← mkHost net tc.clock 1 (← OnceRef.new []) + let server ← mkHost net tc.clock 2 failures + let addr ← match Multiformats.Multiaddr.parse? "/memory/4100" with + | .ok a => pure a + | .error _ => throw (IO.userError "test address") + let .ok bound ← server.startListening addr | throw (IO.userError "listen failed") + let .ok serverPeer ← client.dial bound | throw (IO.userError "dial failed") + return { client, server, serverPeer, serverAddr := bound, failures, clock := tc } + +/-- Close both hosts, then the clock. Each close joins its own tasks +(§5.5). -/ +def Pair.close (p : Pair) : Async Unit := do + p.client.close + p.server.close + p.clock.close + +end Tests.HostPair diff --git a/Tests/Protocols.lean b/Tests/Protocols.lean index e11434c8..fa05fa56 100644 --- a/Tests/Protocols.lean +++ b/Tests/Protocols.lean @@ -1,4 +1,5 @@ import Tests.Support +import Tests.HostPair import Proto import Bytes import Varint @@ -6,10 +7,11 @@ import Conc import Streams.Error import Streams.Framing import Streams.Stream +import Multiformats.Multiaddr +import Libp2p.Core +import Libp2p.Host import Libp2p.Protocols import Libp2p.Protocols.Identity -import Libp2p.Protocols.Mock.Core -import Libp2p.Protocols.Mock.Host /-! # Identify and ping suite @@ -18,16 +20,17 @@ Mirrors `vendor/specs/ping/ping.md` (32-byte echo, protocol id `/ipfs/ping/1.0.0`) and the captured go-libp2p Identify protobuf (`identify-go.json`). The suite replays the vector and drives the pure `Identify.validate` and `Ping.checkEcho` checks. The real key -fixtures and the host stand-in run here, and the address checks run the -real Multiformats decoder, so every validate outcome appears in a -check. +fixtures run here, and the address checks run the real Multiformats +decoder, so every validate outcome appears in a check. The exchange cases cover the identify client against the responder -handler, the push handler against the in-memory peerstore double, the -client deadline on the test clock, and the ping echo, with the -initiator on end `a` and the handler on end `b`. The exchanges run over -a private pair of `Conc.Pipe` values, wired as two `Streams.Stream` -ends. +handler, the push handler against a real host's peerstore, the client +deadline on the test clock, and the ping echo, with the initiator on +end `a` and the handler on end `b`. Those exchanges run over a private +pair of `Conc.Pipe` values, wired as two `Streams.Stream` ends, with a +fixed `StreamContext`. Identify and push then run once more between two +real hosts (`Tests.HostPair`), so each handler reads the context of a +real connection and serves through the host's registry. -/ set_option autoImplicit false @@ -36,6 +39,7 @@ namespace Tests.Protocols open Libp2p.Protocols open Libp2p.Identity +open Tests.HostPair (hostPair) /-- A real Ed25519 public key for the suite. A 32-byte key needs no native call, and the key round trips through the wire form. -/ @@ -47,12 +51,35 @@ private def testPeer (tag : UInt8) : PeerId := PeerId.inline (ByteArray.mk #[tag]) (by simp [ByteArray.size, Libp2p.Identity.maxInlineKeyBytes]) -/-- A placeholder served-stream context. The identify and ping -handlers read no context field, so the empty address never reaches a -check. -/ -private def testContext : Libp2p.Protocols.Mock.Core.StreamContext := - { remotePeer := testPeer 0, - remoteAddr := ⟨{ frames := [], valid := by decide }⟩ } +/-- A multiaddr from its text form. -/ +private def ma (s : String) : IO Multiformats.Multiaddr := + match Multiformats.Multiaddr.parse? s with + | .ok a => return a + | .error _ => throw (IO.userError s!"test address {s} does not parse") + +/-- The context of a pipe-pair exchange: the peer `p`, and a memory +address. The pipe pair has no connection under it. -/ +private def ctxOf (p : PeerId) : IO Libp2p.Core.StreamContext := + return { remotePeer := p, remoteAddr := ← ma "/memory/9" } + +/-- The binary form of `/ip4/127.0.0.1/tcp/35371`, the vector's listen +address, and its parsed form. -/ +private def vectorAddr : List Nat := [4, 127, 0, 0, 1, 6, 138, 43] +private def vectorMultiaddr : IO Multiformats.Multiaddr := ma "/ip4/127.0.0.1/tcp/35371" + +/-- A host that serves no connection, over a new sim net and `clock`: +the peerstore of the push checks. -/ +private def storeHost (clock : Conc.Clock) : Conc.Async Libp2p.Host.Host := do + Tests.HostPair.mkHost (← Streams.Sim.Net.new) clock 3 (← Conc.OnceRef.new []) + +/-- The Ed25519 public key of 32 copies of `v`, the key a host of +`Tests.HostPair` derives from the seed `v` (client 1, server 2). -/ +private def hostKey (v : UInt8) : IO PubKey := do + let .ok k := PrivKey.ofData? .ed25519 ⟨Array.replicate 32 v⟩ + | throw (IO.userError s!"test key {v} does not build") + match k.toPublic with + | .ok pk => return pk + | .error _ => throw (IO.userError s!"test key {v} has no public half") /-- The model decode over the byte list. -/ private def decodeModel (bs : List Nat) : Except Pb.Error (Identify × List Nat) := @@ -119,34 +146,35 @@ private def isOkNone {ε α : Type} (x : Except ε (Option α)) : Bool := | _ => false /-- True when the handler answer is a protocol error. -/ -private def isProtocolError (x : Except Libp2p.Protocols.Mock.Core.Error Unit) : Bool := +private def isProtocolError (x : Except Libp2p.Core.Error Unit) : Bool := match x with | .error (.protocol _) => true | _ => false -/-- Run the handler on `s`, and fail the task when the handler -answers an error. -/ -private def runHandler (h : Libp2p.Protocols.Mock.Core.StreamHandler) +/-- Run the handler on `s` with the context `ctx`, and fail the task +when the handler answers an error. -/ +private def runHandler (h : Libp2p.Core.StreamHandler) (ctx : Libp2p.Core.StreamContext) (s : Streams.Stream) : Conc.Async Unit := do - let res : Except Libp2p.Protocols.Mock.Core.Error Unit ← h.handle testContext s + let res : Except Libp2p.Core.Error Unit ← h.handle ctx s match res with | .error e => throw (IO.userError s!"the handler answered {repr e}") | .ok () => pure () /-- The exchange cases, on the test clock and the private pair. -/ private def asyncChecks (r : Runner) : Conc.Async Unit := do - -- identify: the responder round trip + -- identify: the responder round trip; the observed address is the + -- context's remote address do let pair ← mkPair let tc ← Conc.TestClock.new let key := testKey 1 let pid : PeerId := peerIdOfPubKey key - let addr := [4, 127, 0, 0, 1, 6, 138, 43] + let ctx ← ctxOf (testPeer 0) let agent := "leanp2p" let protocols := ["/ipfs/id/1.0.0"] let ts ← Conc.TaskSet.new ts.spawn do - runHandler (Identify.respondHandler key [addr] protocols none agent none) pair.b + runHandler (Identify.respondHandler key [vectorAddr] protocols agent none) ctx pair.b let res ← Identify.client pair.a tc.clock 1000 (some pid) ts.joinAll r.check "identify e2e responder round trip accepted" @@ -154,6 +182,10 @@ private def asyncChecks (r : Runner) : Conc.Async Unit := do | .ok (some (m, got)) => decide (got = pid) && m.agentVersion == some agent && m.protocols == protocols | _ => false) + r.check "identify e2e responder writes the context's address as observed" + (match res with + | .ok (some (m, _)) => m.observedAddr == some ctx.remoteAddr.toBytes + | _ => false) tc.close -- identify: the same pair runs the exchange twice, roles swapped @@ -162,92 +194,125 @@ private def asyncChecks (r : Runner) : Conc.Async Unit := do let tc ← Conc.TestClock.new let key := testKey 3 let pid : PeerId := peerIdOfPubKey key + let ctx ← ctxOf (testPeer 0) let agent := "leanp2p" let ts ← Conc.TaskSet.new ts.spawn do - runHandler (Identify.respondHandler key [] [] none agent none) pair.b + runHandler (Identify.respondHandler key [] [] agent none) ctx pair.b let first ← Identify.client pair.a tc.clock 1000 (some pid) ts.joinAll ts.spawn do - runHandler (Identify.respondHandler key [] [] none agent none) pair.a + runHandler (Identify.respondHandler key [] [] agent none) ctx pair.a let second ← Identify.client pair.b tc.clock 1000 (some pid) ts.joinAll r.check "identify e2e round trip both directions" (isOkSome first && isOkSome second) tc.close - -- identify: the push handler updates the peerstore + -- identify: the push handler updates the host's peerstore, under the + -- context's peer do let pair ← mkPair let tc ← Conc.TestClock.new - let store ← Mock.Host.inMemory + let store ← storeHost tc.clock let key := testKey 1 let pid : PeerId := peerIdOfPubKey key - let addr := [4, 127, 0, 0, 1, 6, 138, 43] - let msg := Identify.respond key [addr] [] none "" none + let ctx ← ctxOf pid + let want ← vectorMultiaddr + let msg := Identify.respond key [vectorAddr] [] none "" none match Streams.Framing.encodeB? .uvarint Constants.identifyCap (Pb.encodeMessageB msg) with | none => r.check "identify e2e push updates the peerstore and reads back" false | some frame => let ts ← Conc.TaskSet.new ts.spawn do - runHandler (Identify.pushHandler store pid tc.clock 1000) pair.b + runHandler (Identify.pushHandler store tc.clock 1000) ctx pair.b discard <| pair.a.write frame ts.joinAll - let stored ← store.addrsOf pid + let stored ← (store.addrsOf pid : BaseIO (List Multiformats.Multiaddr)) r.check "identify e2e push updates the peerstore and reads back" - (stored == [addr]) + (stored == [want]) + store.close tc.close -- identify: a second push of the same addresses grows nothing do let pair ← mkPair let tc ← Conc.TestClock.new - let store ← Mock.Host.inMemory + let store ← storeHost tc.clock let key := testKey 1 let pid : PeerId := peerIdOfPubKey key - let addr := [4, 127, 0, 0, 1, 6, 138, 43] - let msg := Identify.respond key [addr] [] none "" none + let ctx ← ctxOf pid + let want ← vectorMultiaddr + let msg := Identify.respond key [vectorAddr] [] none "" none match Streams.Framing.encodeB? .uvarint Constants.identifyCap (Pb.encodeMessageB msg) with | none => r.check "identify e2e push redial adds no duplicate address" false | some frame => let ts ← Conc.TaskSet.new ts.spawn do - runHandler (Identify.pushHandler store pid tc.clock 1000) pair.b + runHandler (Identify.pushHandler store tc.clock 1000) ctx pair.b discard <| pair.a.write frame ts.joinAll let ts2 ← Conc.TaskSet.new ts2.spawn do - runHandler (Identify.pushHandler store pid tc.clock 1000) pair.b + runHandler (Identify.pushHandler store tc.clock 1000) ctx pair.b discard <| pair.a.write frame ts2.joinAll - let stored ← store.addrsOf pid + let stored ← (store.addrsOf pid : BaseIO (List Multiformats.Multiaddr)) r.check "identify e2e push redial adds no duplicate address" - (stored == [addr]) + (stored == [want]) + store.close tc.close -- identify: the push sender announces the record and the receiver stores it do let pair ← mkPair let tc ← Conc.TestClock.new - let store ← Mock.Host.inMemory + let store ← storeHost tc.clock let key := testKey 7 let pid : PeerId := peerIdOfPubKey key - let addr := [4, 127, 0, 0, 1, 6, 138, 43] + let ctx ← ctxOf pid + let want ← vectorMultiaddr let ts ← Conc.TaskSet.new ts.spawn do - runHandler (Identify.pushHandler store pid tc.clock 1000) pair.b - let sent ← Identify.pushTo key [addr] [] none "" none + runHandler (Identify.pushHandler store tc.clock 1000) ctx pair.b + let sent ← Identify.pushTo key [vectorAddr] [] none "" none { pair.a with close := pair.ab.close } ts.joinAll let ended ← pair.b.read - let stored ← store.addrsOf pid + let stored ← (store.addrsOf pid : BaseIO (List Multiformats.Multiaddr)) r.check "identify e2e push sender announces the record" ((match sent with | Except.ok _ => true - | Except.error _ => false) && stored == [addr]) + | Except.error _ => false) && stored == [want]) r.check "identify e2e push sender half-closes the stream" (isOkNone ended) + store.close + tc.close + + -- identify: a push whose key is not the context's peer fails, and + -- the peerstore stores nothing for either peer + do + let pair ← mkPair + let tc ← Conc.TestClock.new + let store ← storeHost tc.clock + let key := testKey 7 + let pid : PeerId := peerIdOfPubKey key + let other := testPeer 8 + let ctx ← ctxOf other + let msg := Identify.respond key [vectorAddr] [] none "" none + match Streams.Framing.encodeB? .uvarint Constants.identifyCap + (Pb.encodeMessageB msg) with + | none => r.check "identify e2e push with another peer's key stores nothing" false + | some frame => + discard <| pair.a.write frame + let res : Except Libp2p.Core.Error Unit ← + (Identify.pushHandler store tc.clock 1000).handle ctx pair.b + let forKey ← (store.addrsOf pid : BaseIO (List Multiformats.Multiaddr)) + let forCtx ← (store.addrsOf other : BaseIO (List Multiformats.Multiaddr)) + r.check "identify e2e push with another peer's key stores nothing" + (isProtocolError res && forKey.isEmpty && forCtx.isEmpty) + store.close tc.close -- identify: the client rejects an over-cap frame before the body @@ -304,9 +369,10 @@ private def asyncChecks (r : Runner) : Conc.Async Unit := do let pair ← mkPair let tc ← Conc.TestClock.new let payload := Bytes.ofNatList (List.replicate 32 7) + let ctx ← ctxOf (testPeer 0) let ts ← Conc.TaskSet.new ts.spawn do - runHandler Ping.pingHandler pair.b + runHandler Ping.pingHandler ctx pair.b let res ← Ping.ping pair.a tc.clock payload pair.ab.close ts.joinAll @@ -393,9 +459,10 @@ private def asyncChecks (r : Runner) : Conc.Async Unit := do let tc ← Conc.TestClock.new let payload := List.replicate 32 7 let half := List.replicate 16 7 + let ctx ← ctxOf (testPeer 0) let ts ← Conc.TaskSet.new ts.spawn do - runHandler Ping.pingHandler pair.b + runHandler Ping.pingHandler ctx pair.b discard <| pair.a.write (Bytes.ofNatList half) discard <| pair.a.write (Bytes.ofNatList half) let echo ← pair.a.read @@ -411,11 +478,12 @@ private def asyncChecks (r : Runner) : Conc.Async Unit := do do let pair ← mkPair let tc ← Conc.TestClock.new - let answer : Conc.OnceRef (Option (Except Libp2p.Protocols.Mock.Core.Error Unit)) ← + let ctx ← ctxOf (testPeer 0) + let answer : Conc.OnceRef (Option (Except Libp2p.Core.Error Unit)) ← Conc.OnceRef.new none let ts ← Conc.TaskSet.new ts.spawn do - answer.set (some (← Ping.pingHandler.handle testContext pair.b)) + answer.set (some (← Ping.pingHandler.handle ctx pair.b)) discard <| pair.a.write (Bytes.ofNatList (List.replicate 20 7)) pair.ab.close ts.joinAll @@ -433,6 +501,82 @@ private def asyncChecks (r : Runner) : Conc.Async Unit := do (failsWith (Ping.Error.wrongSize 31) res) tc.close +/-! ## Identify and push between two hosts -/ + +/-- `h` with the handler `sh` registered under its id, wrapped so that +the end of each served stream sends on `done`. -/ +private def setSignalling (h : Libp2p.Host.Host) (sh : Libp2p.Core.StreamHandler) + (done : Conc.Chan Unit) : BaseIO Unit := + h.setHandler { sh with handle := fun ctx s => ExceptT.mk do + let res ← (sh.handle ctx s).run + discard (done.trySend () : BaseIO Bool) + return res } + +/-- The handlers over real connections: the context comes from the +host, and the handlers serve through its registry. -/ +private def hostChecks (r : Runner) : Conc.Async Unit := do + let clientPeer ← match PeerId.ofPubKey (← hostKey 1) with + | .ok p => pure p + | .error _ => throw (IO.userError "the client key derives no peer id") + let serverKey ← hostKey 2 + + -- The client identifies the server through the host. The answer + -- proves the server's peer id. The observed address is the one the + -- server's connection reports for the client. + do + let p ← hostPair + p.server.setHandler + (Identify.respondHandler serverKey [p.serverAddr.toBytes] ["/ipfs/id/1.0.0"] "leanp2p") + match ← p.client.newStream p.serverPeer [Identify.protocolId] with + | .error e => r.check s!"host identify: the stream opens ({e})" false + | .ok (_, s) => + match ← Identify.client s p.clock.clock 5000 (some p.serverPeer) with + | .ok (some (m, got)) => + r.check "host identify: the answer proves the server's peer id" (got == p.serverPeer) + r.check "host identify: the listen address reads back" + (m.listenAddrs == [p.serverAddr.toBytes]) + r.check "host identify: the observed address is the client's sim address" + (m.observedAddr.any fun o => Identify.validAddress o && o != p.serverAddr.toBytes) + | _ => r.check "host identify: the client accepts the answer" false + p.close + + -- A push from the client lands in the server's peerstore, under the + -- peer id that the connection proved. + do + let p ← hostPair + let done : Conc.Chan Unit ← Conc.Chan.new 1 + setSignalling p.server (Identify.pushHandler p.server p.clock.clock 5000) done + let pushed ← ma "/ip4/10.0.0.1/tcp/4001" + match ← p.client.newStream p.serverPeer [Identify.pushId] with + | .error e => r.check s!"host push: the stream opens ({e})" false + | .ok (_, s) => + let sent ← Identify.pushTo (← hostKey 1) [pushed.toBytes] [] none "leanp2p" none s + discard done.recv + let stored ← (p.server.addrsOf clientPeer : BaseIO (List Multiformats.Multiaddr)) + r.check "host push: the sender writes the record" (sent matches .ok ()) + r.check "host push: the server stores the address under the client's peer id" + (stored.contains pushed) + p.close + + -- A push that carries another peer's key fails, and the peerstore + -- holds nothing for either peer. + do + let p ← hostPair + let done : Conc.Chan Unit ← Conc.Chan.new 1 + setSignalling p.server (Identify.pushHandler p.server p.clock.clock 5000) done + let pushed ← ma "/ip4/10.0.0.9/tcp/4001" + let spoofKey := testKey 9 + match ← p.client.newStream p.serverPeer [Identify.pushId] with + | .error e => r.check s!"host push spoof: the stream opens ({e})" false + | .ok (_, s) => + discard <| Identify.pushTo spoofKey [pushed.toBytes] [] none "leanp2p" none s + discard done.recv + let forClient ← (p.server.addrsOf clientPeer : BaseIO (List Multiformats.Multiaddr)) + let forSpoof ← (p.server.addrsOf (peerIdOfPubKey spoofKey) : BaseIO (List Multiformats.Multiaddr)) + r.check "host push spoof: a push with another peer's key stores nothing" + (!forClient.contains pushed && forSpoof.isEmpty) + p.close + def run (r : Runner) : IO Unit := do r.section "protocols" "libp2p/specs identify/README.md + ping/ping.md + captured go Identify protobuf" @@ -569,5 +713,6 @@ def run (r : Runner) : IO Unit := do (failsWith .mismatch (Ping.checkEcho sent altered)) Conc.Async.run (asyncChecks r) + Conc.Async.run (hostChecks r) end Tests.Protocols diff --git a/Tests/ReqResp.lean b/Tests/ReqResp.lean index 1970345a..b386b9a0 100644 --- a/Tests/ReqResp.lean +++ b/Tests/ReqResp.lean @@ -1,7 +1,7 @@ import Tests.Support +import Tests.HostPair import Libp2p.Protocols.ReqResp.Exchange -import Libp2p.Protocols.Mock.Muxer -import Libp2p.Protocols.Mock.HostStream +import Libp2p.Host import Multiformats.Multiaddr /-! @@ -18,8 +18,8 @@ encoder shape writes through go's snappy. The sections follow the layers: the checksum, the chunk codec, the length prefix, the reader core as transcripts with no clock and no task, the writer, the concurrency limit, the exchange over a stream -pair with the test clock, and the exchange over the sim transport -through the mock muxer and the host stream mock. +pair with the test clock, and the exchange between two hosts over the +sim transport, with the fixed-key Noise value and yamux. -/ set_option autoImplicit false @@ -607,35 +607,17 @@ def limiterChecks (r : Runner) : IO Unit := do /-! ## Over the sim transport -/ -open Libp2p.Protocols.Mock.Muxer (muxer) -open Libp2p.Protocols.Mock.HostStream (Host) - -/-- The peer id of a fixed Ed25519 seed of 32 copies of `v`. -/ -private def seedPeer (v : UInt8) : Async Libp2p.Identity.PeerId := do - let seed : ByteArray := ⟨Array.replicate 32 v⟩ - match (do Libp2p.Identity.PeerId.ofPubKey (← (← Libp2p.Identity.PrivKey.ofData? .ed25519 seed).toPublic) - : Except Libp2p.Identity.Error Libp2p.Identity.PeerId) with - | .ok p => return p - | .error _ => throw (IO.userError "test: the fixed seed derives no peer id") - -/-- A connected pair of hosts over a new sim net and the mock muxer. -Each end's handler context names the other end's peer and its own -connection's remote address. -/ -def hostPair (split : Bool := false) : Async (Host × Host) := do - let net ← Streams.Sim.Net.new split - let addr ← match Multiformats.Multiaddr.parse? "/ip4/127.0.0.1/tcp/4100" with - | .ok a => pure a - | .error _ => throw (IO.userError "test address") - let l ← net.transport.listen addr - let some c ← net.transport.dial l.addr | throw (IO.userError "dial failed") - let some s ← l.accept | throw (IO.userError "accept failed") - l.close - let .ok cs ← (muxer.«open» .initiator c ByteArray.empty).run | throw (IO.userError "open failed") - let .ok ss ← (muxer.«open» .responder s ByteArray.empty).run | throw (IO.userError "open failed") - let client ← seedPeer 1 - let server ← seedPeer 2 - return (← Host.new cs { remotePeer := server, remoteAddr := c.remoteAddr }, - ← Host.new ss { remotePeer := client, remoteAddr := s.remoteAddr }) +open Tests.HostPair (Pair hostPair) + +/-- The host's stream call for the server, as the `OpenStream` of +`requestPeer`. A host failure that wraps a seam error reaches the +requester as that error. The host renders its own refusals into +`protocol`. -/ +def openStreamOf (p : Pair) : OpenStream := fun ids => do + match ← p.client.newStream p.serverPeer ids with + | .ok x => return .ok x + | .error (.stream e) | .error (.upgrade e) | .error (.session e) => return .error e + | .error e => return .error (.protocol (toString e)) def simChecks (r : Runner) : Async Unit := do r.section "over the sim" "phase0 Req/Resp interaction; ARCHITECTURE §5.4; PRINCIPLES 1.4" @@ -644,83 +626,69 @@ def simChecks (r : Runner) : Async Unit := do let answer : List Chunk := [⟨.success, digest, noise 1 70000⟩, ⟨.success, digest, noise 2 5⟩] for split in [false, true] do let tc ← TestClock.new - let (client, server) ← hostPair split - server.setHandler (handler m tc.clock 1000 fun _ => return answer) - server.serve + let p ← hostPair split + p.server.setHandler (handler m tc.clock 1000 fun _ => return answer) let limiter ← Limiter.new let got : OnceRef (List Chunk) ← OnceRef.new [] - let res ← requestPeer client.newStream limiter m tc.clock 1000 (some (noise 3 200)) + let res ← requestPeer (openStreamOf p) limiter m tc.clock 1000 (some (noise 3 200)) fun c => got.update (· ++ [c]) r.check s!"sim (split {split}): a request through the host gets its chunks" (succeedsWith () res && (← got.get).map (·.payload) == answer.map (·.payload)) - r.check s!"sim (split {split}): the handler saw no failure" ((← server.failures.get).isEmpty) + r.check s!"sim (split {split}): the handler saw no failure" ((← p.failures.get).isEmpty) r.check s!"sim (split {split}): the limiter slot came back" ((← limiter.take m.id) && (← limiter.take m.id)) - client.close - server.close - client.join - server.join + p.close tc.close - -- An id the peer does not serve: the stream is reset. + -- An id the peer does not serve: multistream-select answers `na`, so + -- the stream never opens for it. do let tc ← TestClock.new - let (client, server) ← hostPair - server.serve - let res ← requestPeer client.newStream (← Limiter.new) m tc.clock 1000 (some (noise 3 4)) + let p ← hostPair + let res ← requestPeer (openStreamOf p) (← Limiter.new) m tc.clock 1000 (some (noise 3 4)) fun _ => pure () - r.check "sim: an id with no handler fails the request with a reset" - (failsWith (.stream .reset) res) - client.close - server.close - client.join - server.join + r.check "sim: an id with no handler fails the open" + (match res with | .error (.openFailed _) => true | _ => false) + p.close tc.close -- A silent peer over the sim: the deadline resets the stream, and the -- connection stays for the next exchange. do let tc ← TestClock.new - let (client, server) ← hostPair + let p ← hostPair -- The handler takes one read and ends with no answer and no close. - server.setHandler ⟨m.id, fun _ s => ExceptT.mk do + p.server.setHandler ⟨m.id, fun _ s => ExceptT.mk do discard <| s.read return .ok ()⟩ - server.serve let owner ← TaskSet.new let res : OnceRef (Option (Except Error Unit)) ← OnceRef.new none owner.spawn do - res.set (some (← requestPeer client.newStream (← Limiter.new) m tc.clock 300 (some (noise 3 4)) + res.set (some (← requestPeer (openStreamOf p) (← Limiter.new) m tc.clock 300 (some (noise 3 4)) fun _ => pure ())) r.check "sim: a silent peer, the deadline arms" (← tc.nextTimer) tc.advance 300 owner.joinAll r.check "sim: a silent peer fails the request at its deadline" ((← res.get).any (failsWith .timeout)) tc.close - client.close - server.close - client.join - server.join + p.close -- The connection closes under a parked read: the request ends. do let tc ← TestClock.new - let (client, server) ← hostPair + let p ← hostPair let parked : Chan Unit ← Chan.new 1 - server.setHandler ⟨m.id, fun _ _ => ExceptT.mk do + p.server.setHandler ⟨m.id, fun _ _ => ExceptT.mk do discard <| parked.send () return .ok ()⟩ - server.serve let owner ← TaskSet.new let res : OnceRef (Option (Except Error Unit)) ← OnceRef.new none owner.spawn do - res.set (some (← requestPeer client.newStream (← Limiter.new) m tc.clock 60000 (some (noise 3 4)) + res.set (some (← requestPeer (openStreamOf p) (← Limiter.new) m tc.clock 60000 (some (noise 3 4)) fun _ => pure ())) -- The handler ran, so the request is past its write and parks on the read. discard <| parked.recv - client.close + p.client.close owner.joinAll r.check "sim: a connection closed under a parked read ends the request" ((← res.get).any fun e => match e with | .error _ => true | .ok _ => false) - server.close - client.join - server.join + p.server.close tc.close def run (r : Runner) : IO Unit := do diff --git a/packages/cli/GossipsubSession.lean b/packages/cli/GossipsubSession.lean index 5300c618..9f9d6c89 100644 --- a/packages/cli/GossipsubSession.lean +++ b/packages/cli/GossipsubSession.lean @@ -19,22 +19,6 @@ open Conc Streams Multiformats Libp2p.Core Libp2p.Identity Libp2p.Host open Libp2p.Protocols Libp2p.Protocols.Constants open Libp2p.Protocols.Gossipsub Libp2p.Protocols.Gossipsub.Node -/-- Map the protocols package's mock-seam error onto the core error. The identify package still -types over the mock seam (issue #55), so the participant converts at the host boundary. -/ -def mapMockError : Libp2p.Protocols.Mock.Core.Error → Libp2p.Core.Error - | .protocol s => .protocol s - | .authentication s => .authentication s - | .timeout s => .timeout s - | .closed s => .closed s - -/-- Adapt a handler of the protocols package's mock seam onto the real core handler seam. -/ -def toCoreHandler (h : Libp2p.Protocols.Mock.Core.StreamHandler) : Libp2p.Core.StreamHandler where - id := ⟨h.id.toString⟩ - handle := fun ctx stream => ExceptT.mk do - match ← (h.handle ⟨ctx.remotePeer, ctx.remoteAddr⟩ stream).run with - | .ok () => return .ok () - | .error e => return .error (mapMockError e) - /-- Use the production yamux session through the core muxer seam. -/ def yamuxMuxer : Libp2p.Core.Muxer := Libp2p.Mux.yamux @@ -70,7 +54,7 @@ def start (identity : PrivKey) (nodeConfig : Node.Config := {}) : IO (Except Str transports := [Streams.Tcp.transport] security := [Libp2p.Security.Noise.securityProtocol noise] muxers := [yamuxMuxer] - handlers := [toCoreHandler (Identify.respondHandler pubkey [] servedProtocols none "leanp2p")] } + handlers := [Identify.respondHandler pubkey [] servedProtocols "leanp2p"] } let hostResult ← BaseIO.toIO (Libp2p.Host.Host.new config) let host ← match hostResult with | .error e => return .error (reprStr e) diff --git a/packages/cli/Interop.lean b/packages/cli/Interop.lean index df91e16d..6a13167d 100644 --- a/packages/cli/Interop.lean +++ b/packages/cli/Interop.lean @@ -2,8 +2,11 @@ import Crypto import Streams import Interop.Config import Interop.Redis -import Interop.Mock.Stack import Libp2p.Identity +import Libp2p.Security +import Libp2p.Mux +import Libp2p.Host +import Libp2p.Protocols.Ping /-! # The transport-interop harness @@ -15,7 +18,9 @@ test-plan peer is the model on the other side of the wire (`vendor/go-libp2p/test-plans/cmd/ping/main.go`). Both sides read the configuration, connect to Redis, and start a host -with the TCP transport, Noise, and the configured muxer. +with the TCP transport, Noise, and yamux. `libp2p/mux` holds no mplex +value (P2, the mux PLAN, unit 2), so a run with `muxer=mplex` exits +nonzero at the host start. * **The listener** listens, publishes its address with the `/p2p/` suffix through `RPUSH`, and sleeps for the test timeout. The runner @@ -50,8 +55,9 @@ namespace Interop open Conc (Async) open Interop.Config (Config) -open Interop.Mock open Libp2p.Identity (PeerId PrivKey) +open Libp2p.Host (Host) +open Libp2p.Protocols (Ping.protocolId Ping.payloadSize Ping.ping Ping.pingHandler) /-- The interval between two `PING`s while Redis starts, in milliseconds. The go peer waits the same 100 ms (line 84 of its `main.go`). -/ @@ -83,8 +89,9 @@ partial def connectRedis (cfg : Config) (deadlineMs : Nat) : Run Redis.Client := if deadlineMs ≤ (← IO.monoMsNow) then throw s!"redis at {cfg.redisAddr.describe}: no answer within {cfg.timeoutSec} s" let sleep ← Conc.Park.sleep redisRetryMs () - -- Park: the sleep ends it; nothing else waits on this task. The - -- ascription keeps `select` in `Async` (see `dial` for the unfolding). + -- Park: the sleep ends it; nothing else waits on this task. `Run` + -- unfolds to `Async (Except String _)`, so the ascription keeps + -- `select` in `Async`. (Conc.select #[sleep] : Async Unit) connectRedis cfg deadlineMs @@ -96,19 +103,22 @@ def generateKey : Run PrivKey := do let seed ← orFail "identity seed" (fun e => reprStr e) (← Crypto.ed25519Generate.run) orFail "identity key" (fun e => reprStr e) (PrivKey.ofData? .ed25519 seed.bytes) -/-- The host of one run: TCP, Noise, and the configured muxer, with the -ping handler (root §3.1: the ordered lists are assembled here). -/ +/-- The host of one run: TCP, Noise with a static key from the system +generator, yamux, and the ping handler (root §3.1: the ordered lists +are assembled here). -/ def startHost (cfg : Config) : Run Host := do + let muxer ← match cfg.muxer with + | .yamux => pure Libp2p.Mux.yamux + | .mplex => throw "muxer mplex: libp2p/mux holds no mplex value (P2, the mux PLAN, unit 2)" let key ← generateKey - let muxer := match cfg.muxer with - | .yamux => yamux - | .mplex => mplex - orFail "host" (fun e => reprStr e) (← Host.new { - key + let noise ← orFail "noise static key" (fun e => reprStr e) + (← (Libp2p.Security.Noise.Config.generate key).run) + orFail "host" (fun e => reprStr e) (← (Host.new { + identity := key transports := [Streams.Tcp.transport] - securities := [noise key] + security := [Libp2p.Security.Noise.securityProtocol noise] muxers := [muxer] - handlers := [Ping.handler] }) + handlers := [Ping.pingHandler] } : BaseIO _)) /-- The address the listener publishes: the bound address, with the Redis connection's local IP in place of `0.0.0.0`, and the `/p2p/` @@ -126,8 +136,8 @@ def publishedAddr (bound redisLocal : Multiformats.Multiaddr) (peer : PeerId) : /-- The listener: publish the address, then sleep for the timeout. -/ def listen (cfg : Config) (redis : Redis.Client) (h : Host) : Run Unit := do - let bound ← orFail "listen" (fun e => reprStr e) (← h.startListening cfg.listenAddr) - let addr ← orFail "address" id (publishedAddr bound redis.conn.localAddr h.id) + let bound ← orFail "listen" toString (← h.startListening cfg.listenAddr) + let addr ← orFail "address" id (publishedAddr bound redis.conn.localAddr h.localPeer) IO.eprintln s!"listening on {addr}" discard <| orFail "redis RPUSH" (fun e => reprStr e) (← redis.rpush Config.listenerAddrKey addr) @@ -148,20 +158,19 @@ def dial (cfg : Config) (redis : Redis.Client) (h : Host) : Run Unit := do (Multiformats.Multiaddr.parse? text) IO.eprintln s!"dialing {text}" let start ← IO.monoNanosNow - let peer ← orFail "dial" (fun e => reprStr e) (← h.dial addr) - let (_, stream) ← orFail "ping stream" (fun e => reprStr e) + let peer ← orFail "dial" toString (← h.dial addr) + let (_, stream) ← orFail "ping stream" toString (← h.newStream peer [Ping.protocolId]) let payload ← orFail "ping payload" (fun e => reprStr e) (← (Crypto.randomBytes Ping.payloadSize).run) let pingStart ← IO.monoNanosNow - -- `Run` unfolds to `Async (Except String _)`, the type of `Ping.ping`, - -- so an unannotated `←` would run the call as a `Run` step and throw - -- its error here, before the reset below. The annotation makes Lean - -- lift the `Async` call and bind the `Except` as data. - let answer : Except String (Option Nat) ← (Ping.ping stream Conc.Clock.system payload : Async _) + -- The annotation binds the ping's `Except` as data, so its failure + -- waits until after the reset below. `orFail` then reports it. + let answer : Except Libp2p.Protocols.Ping.Error (Option Nat) ← + (Ping.ping stream Conc.Clock.system payload : Async _) let done ← IO.monoNanosNow stream.reset - discard <| orFail "ping" id answer + discard <| orFail "ping" (fun e => reprStr e) answer IO.println (Config.timingJson ((done - start) / 1000) ((done - pingStart) / 1000)) /-- One harness run. The host closes on every path (cli ARCHITECTURE, diff --git a/packages/cli/Interop/Config.lean b/packages/cli/Interop/Config.lean index a0308fbc..fe879aa5 100644 --- a/packages/cli/Interop/Config.lean +++ b/packages/cli/Interop/Config.lean @@ -17,11 +17,12 @@ the runner compares the keys literally. ## What the harness supports -The gate runs `tcp + /noise + yamux` (root PLAN W5.9). The harness also -reads `mplex`, the second `Muxer` value (root §4.9). Any other -transport, security, or muxer name is a configuration error, and the -binary exits nonzero (the test plan: "On error, the dialer should -return a non-zero exit code"). +The gate runs `tcp + /noise + yamux` (root PLAN W5.9). The parse also +reads `mplex`, the second muxer of root §4.9. `libp2p/mux` holds no +mplex value yet (P2, the mux PLAN, unit 2), so the host start refuses +it. Any other transport, security, or muxer name is a configuration +error. On every refusal the binary exits nonzero (the test plan: "On +error, the dialer should return a non-zero exit code"). `ip` and `redis_addr` take literal IPv4 addresses. The TCP transport dials and listens on `/ip4` and `/ip6` only (the streams ARCHITECTURE, diff --git a/packages/cli/Interop/Mock/Stack.lean b/packages/cli/Interop/Mock/Stack.lean deleted file mode 100644 index ed6b318a..00000000 --- a/packages/cli/Interop/Mock/Stack.lean +++ /dev/null @@ -1,160 +0,0 @@ -import Conc -import Streams -import Libp2p.Identity - -/-! -# Mock: the unmerged stack under the harness - -The harness composes a host from `libp2p/identity` (W5.1), -`libp2p/core` (W5.2), `libp2p/security` (W5.3), `libp2p/mux` (W5.4), -`libp2p/host` (W5.6), and `libp2p/protocols` (W5.7). W5.1 has merged, -so the keys and the peer id come from `Libp2p.Identity`. The others -have not, so the harness builds against mocks of their frozen surfaces -(RULES.md, "Working ahead of the tree"). The mock imports nothing from -those packages. It states no axiom. - -The forms: - -* A type is a copy of the frozen shape, reduced to the fields the - harness touches. The sources: the root ARCHITECTURE §3.1 and §4.9, - and the public surface sections of the host, security, mux, and - protocols ARCHITECTURE files. -* An operation is `opaque`, and its body fails with the name of the - missing package. No body fakes a connection, a handshake, or an - identity, so the harness cannot pass a live run against this mock. - -`Host.newStream` follows go-libp2p's `host.NewStream` -(`vendor/go-libp2p/core/host/host.go`, lines 61 to 65): a peer and the -protocol ids in preference order, answered with the stream and the id -it selected. The -host ARCHITECTURE, "Public surface", names no outbound stream call, and -this unit adds the line there. - -At integration, the harness imports the real packages, and the module -goes. --/ - -set_option autoImplicit false - -namespace Interop.Mock - -open Libp2p.Identity - -/-! ## `libp2p/core` -/ - -/-- A protocol id, wrapped (root §3.4). -/ -structure ProtocolId where - /-- The id text. -/ - toString : String - deriving DecidableEq, Repr - -/-- The coarse error every seam returns (root §4.9). -/ -inductive CoreError where - | protocol (detail : String) - | authentication (detail : String) - | timeout (detail : String) - | closed (detail : String) - deriving Repr - -/-- A security protocol value: its id, and its handshake (root §4.9). -/ -structure SecurityProtocol where - /-- The negotiated id. -/ - id : ProtocolId - -/-- A muxer value: its id, and its session entry (root §4.9). -/ -structure Muxer where - /-- The negotiated id. -/ - id : ProtocolId - -/-- A stream handler: its id, and its serve function (root §3.1). -/ -structure StreamHandler where - /-- The negotiated id. -/ - id : ProtocolId - -/-! ## `libp2p/security` and `libp2p/mux` -/ - -/-- `Noise.securityProtocol`, for the identity `key`. -/ -opaque noise (_key : PrivKey) : SecurityProtocol := - ⟨⟨"/noise"⟩⟩ - -/-- `Mux.yamux`. -/ -opaque yamux : Muxer := ⟨⟨"/yamux/1.0.0"⟩⟩ - -/-- `Mux.mplex`. -/ -opaque mplex : Muxer := ⟨⟨"/mplex/6.7.0"⟩⟩ - -/-! ## `libp2p/protocols` -/ - -namespace Ping - -/-- `Ping.protocolId`. -/ -opaque protocolId : ProtocolId := ⟨"/ipfs/ping/1.0.0"⟩ - -/-- The payload size of one ping. -/ -def payloadSize : Nat := 32 - -/-- The ping handler, which echoes each payload. -/ -opaque handler : StreamHandler := ⟨⟨"/ipfs/ping/1.0.0"⟩⟩ - -/-- One ping: send the payload, await the echo, check it, and answer -the round trip in milliseconds (the shape of W5.7's `Ping.ping`). -/ -opaque ping (_s : Streams.Stream) (_clock : Conc.Clock) (_payload : ByteArray) : - Conc.Async (Except String (Option Nat)) := - return .error "libp2p/protocols (W5.7) is not integrated" - -end Ping - -/-! ## `libp2p/host` -/ - -/-- `Host.Error`, with the arms of the host ARCHITECTURE. -/ -inductive HostError where - | upgrade (reason : CoreError) - | gated - | noAddresses (peer : PeerId) - | closing - deriving Repr - -/-- The configuration of `Host.new`: the ordered seam lists and the -identity (root §3.1; the host ARCHITECTURE, "Public surface"). -/ -structure HostConfig where - /-- The identity key. -/ - key : PrivKey - /-- The transports, in preference order. -/ - transports : List Streams.Transport - /-- The security protocols, in preference order. -/ - securities : List SecurityProtocol - /-- The muxers, in preference order. -/ - muxers : List Muxer - /-- The initial handler set. -/ - handlers : List StreamHandler - -/-- A running host. -/ -structure Host where - /-- The local peer id. -/ - id : PeerId - -/-- Start a host. -/ -opaque Host.new (_config : HostConfig) : Conc.Async (Except HostError Host) := - return .error (.upgrade (.closed "libp2p/host (W5.6) is not integrated")) - -/-- Listen on an address. The answer is the bound address. -/ -opaque Host.startListening (_h : Host) (_addr : Multiformats.Multiaddr) : - Conc.Async (Except HostError Multiformats.Multiaddr) := - return .error .closing - -/-- Dial an address. A trailing `/p2p/` supplies the expected peer. -The answer is the peer the handshake proved. -/ -opaque Host.dial (_h : Host) (_addr : Multiformats.Multiaddr) : - Conc.Async (Except HostError PeerId) := - return .error .closing - -/-- Open a stream to a peer, and negotiate one of the ids. -/ -opaque Host.newStream (_h : Host) (_peer : PeerId) (_protocols : List ProtocolId) : - Conc.Async (Except HostError (ProtocolId × Streams.Stream)) := - return .error .closing - -/-- Run the shutdown sequence of root §5.5. -/ -opaque Host.close (_h : Host) : Conc.Async Unit := - return () - -end Interop.Mock diff --git a/packages/cli/docs/ARCHITECTURE.md b/packages/cli/docs/ARCHITECTURE.md index adfa23d2..912a72ca 100644 --- a/packages/cli/docs/ARCHITECTURE.md +++ b/packages/cli/docs/ARCHITECTURE.md @@ -22,7 +22,6 @@ row 18). | `Interop/Config.lean` | the test plan's environment variables, read into a `Config`, and the timing record | | `Interop/Resp.lean` | RESP2, pure: the reply header parse with its caps, and the command encoding | | `Interop/Redis.lean` | the harness coordination client, private to the `interop` executable: `PING`, `RPUSH`, and `BLPOP` over one connection; the spike's `LeanP2P/Interop/Redis.lean` mapped here | -| `Interop/Mock/Stack.lean` | the mock of the unmerged stack under the harness (RULES.md, "Working ahead of the tree"), until W5.2 to W5.7 merge | The package is executables only, with no library root (see Decisions). The W0.1 scaffold gives every leaf a nominal `lean_lib`; @@ -62,7 +61,9 @@ three CLI contracts. environment variables, in the shape of the libp2p transport-interop test plan: `transport` (`tcp`), `muxer` (`yamux` or `mplex`), `security` (`noise`), `is_dialer`, `ip`, `redis_addr`, - and `test_timeout_seconds`. The listener publishes its dialable + and `test_timeout_seconds`. `libp2p/mux` holds no mplex value yet + (P2, the mux PLAN, unit 2), so a run with `muxer=mplex` exits + nonzero at the host start. The listener publishes its dialable multiaddr with the `/p2p/` suffix through Redis, and the dialer fetches it, dials, pings once, and prints the timing JSON with the test plan's keys verbatim, `handshakePlusOneRTTMillis` and @@ -150,19 +151,12 @@ three CLI contracts. (root §2: "shows, as running code, how to compose the stack"). A reader who wants to compose the stack reads `Main.lean`. -## The mock +## The stack -W5.2, W5.3, W5.4, W5.6, and W5.7 are open, so the harness builds -against `Interop/Mock/Stack.lean`, a mock of their frozen surfaces -(RULES.md, "Working ahead of the tree"). A type is a copy of the frozen -shape, reduced to the fields the harness touches. An operation is -`opaque`, and its body fails with the name of the missing package: no -body fakes a connection or a handshake. The mock states no axiom. -W5.1 has merged, so the identity key and the peer id come from the -real `Libp2p.Identity`, and the harness generates its key through it. -Until the integration, a live run stops at the first host call, and -the gate cannot pass. At the integration, `Interop.lean` imports the -real packages, and the module goes. +The harness composes the real packages: an Ed25519 identity from +`Libp2p.Identity`, the TCP transport, `Noise.securityProtocol` with a +static key from `Noise.Config.generate`, `Mux.yamux`, `Libp2p.Host`, +and ping's handler and initiator from `Libp2p.Protocols.Ping`. ## What the package must not depend on diff --git a/packages/libp2p/host/Libp2p/Host.lean b/packages/libp2p/host/Libp2p/Host.lean index 569462a0..c15d17fd 100644 --- a/packages/libp2p/host/Libp2p/Host.lean +++ b/packages/libp2p/host/Libp2p/Host.lean @@ -5,6 +5,8 @@ import Libp2p.Host.Dedup import Libp2p.Host.Peerstore import Libp2p.Host.Policy import Libp2p.Host.Gate +import Libp2p.Host.Upgrade +import Libp2p.Host.StreamSelect import Libp2p.Host.Swarm import Libp2p.Host.Shutdown diff --git a/packages/libp2p/host/Libp2p/Host/StreamSelect.lean b/packages/libp2p/host/Libp2p/Host/StreamSelect.lean new file mode 100644 index 00000000..b2ad5524 --- /dev/null +++ b/packages/libp2p/host/Libp2p/Host/StreamSelect.lean @@ -0,0 +1,82 @@ +import Streams +import Bytes +import Libp2p.Core +import Libp2p.Negotiate + +/-! +# Protocol selection on a muxed stream + +Every stream the muxer opens starts with its own multistream-select +1.0.0 exchange (the connection spec, "Opening new streams over a +multiplexed connection"): the initiator proposes the protocol ids in +order, and the responder answers with the first one in its handler +table. This module runs that exchange on a `Streams.Stream`. + +The negotiate package drives the same pure core over a +`Streams.Connection` (`Negotiate.negotiate`), for the security and muxer +stages of the upgrade. A muxed stream is a different seam: it reads and +writes through `Except` answers, and it carries a read-back buffer for +the leftover. The host owns this shell, and it reuses the core +unchanged: `initiatorStart`, `responderStart`, `drive`, and +`mapNegotiateError` all come from `Libp2p.Negotiate`. + +The bytes that follow the selection on the same read belong to the +protocol. `Stream.prependBytes` hands them on to the handler +(ARCHITECTURE §5.6). + +The read parks for as long as the peer stays silent, so no measure +bounds the loop (root §3.3). The `repeat` form keeps the definition free +of a `partial` marker, as in `Negotiate.negotiate`. +-/ + +set_option autoImplicit false + +namespace Libp2p.Host + +open Libp2p.Negotiate (initiatorStart responderStart drive mapNegotiateError) + +/-- Write each frame payload of the core to the stream, in order. A +failed write is the `closed` arm: the stream is gone. -/ +private def sendWrites (stream : Streams.Stream) (ws : List (List Nat)) : + ExceptT Libp2p.Core.Error Conc.Async Unit := do + for w in ws do + if let .error e ← stream.write (Bytes.ofNatList w) then + throw (.closed s!"stream negotiation write failed: {repr e}") + +/-- Negotiate a protocol on a muxed stream. The answer is the selected +id and the stream with the bytes after the selection put back in front +of its reads. -/ +def negotiateStream (role : Libp2p.Core.Role) (stream : Streams.Stream) + (ids : List Libp2p.Core.ProtocolId) : + ExceptT Libp2p.Core.Error Conc.Async (Libp2p.Core.ProtocolId × Streams.Stream) := do + let start := match role with + | .initiator => initiatorStart ids + | .responder => responderStart ids + let (initial, first) ← match start with + | .error e => throw (mapNegotiateError e) + | .ok pair => pure pair + sendWrites stream first + let mut state := initial + let mut input : List Nat := [] + repeat + match drive 1 state input with + | .error e => throw (mapNegotiateError e) + | .ok (.selected p _ rest writes) => + sendWrites stream writes + return (p, ← Streams.Stream.prependBytes stream (Bytes.ofNatList rest)) + | .ok (.running s _ rest writes) => + sendWrites stream writes + state := s + input := rest + | .ok (.waiting s _ rest writes) => + sendWrites stream writes + state := s + match ← stream.read with + | .error e => throw (.closed s!"stream negotiation read failed: {repr e}") + | .ok none => throw (.closed "stream ended during negotiation") + | .ok (some bytes) => input := rest ++ Bytes.toNatList bytes + -- Every arm above returns or loops, so the `repeat` never falls + -- through. The tail gives the `do` block its result type. + throw (.closed "stream negotiation ended without a selection") + +end Libp2p.Host diff --git a/packages/libp2p/host/Libp2p/Host/Swarm.lean b/packages/libp2p/host/Libp2p/Host/Swarm.lean index 9711349e..a5045240 100644 --- a/packages/libp2p/host/Libp2p/Host/Swarm.lean +++ b/packages/libp2p/host/Libp2p/Host/Swarm.lean @@ -3,8 +3,9 @@ import Conc import Streams import Libp2p.Identity import Libp2p.Core -import Libp2p.Negotiate.Legacy import Libp2p.Host.Error +import Libp2p.Host.StreamSelect +import Libp2p.Host.Upgrade import Libp2p.Host.Registry import Libp2p.Host.Dedup import Libp2p.Host.Peerstore @@ -36,7 +37,7 @@ ARCHITECTURE, "Refinements fixed at implementation (unit 1b)"): `allowDial` before a dial, `allowInbound` after an accept, the resource manager's `openConnection` before the upgrade, and `allowSecured` and `ConnectionScope.setPeer` inside the upgrade, after -the handshake and before the muxer stage (`Negotiate.upgradeWith`). A +the handshake and before the muxer stage (`Libp2p.Host.upgrade`). A refusal is `Error.gated` with the checkpoint. ## Ownership @@ -69,7 +70,7 @@ set_option autoImplicit false namespace Libp2p.Host -open Conc Streams Multiformats Libp2p.Identity Libp2p.Core Libp2p.Negotiate.Legacy +open Conc Streams Multiformats Libp2p.Identity Libp2p.Core /-- A failure of a task that no caller awaits: an inbound upgrade, a session that ended badly, an inbound stream. -/ @@ -242,9 +243,9 @@ private def admit (h : Host) (role : Role) (scope : ConnectionScope) (conn : Con /-! ## The upgrade -/ /-- Run the upgrade of `conn` as a pending connection: registered for -the shutdown (§5.5), under the deadline of the upgrader, with the -checkpoint. Every failure releases `scope`; the upgrader has already -closed the connection. -/ +the shutdown (§5.5), under the deadline of the upgrade, with the +checkpoint. Every failure releases `scope`. On a failure, the upgrade +already closed the connection. -/ private def upgradeConn (h : Host) (role : Role) (conn : Connection) (expected : Option PeerId) (scope : ConnectionScope) : Async (Except Error Upgraded) := do let key ← (h.draw : BaseIO Nat) @@ -257,7 +258,7 @@ private def upgradeConn (h : Host) (role : Role) (conn : Connection) (expected : conn.closeQuietly let unregister : BaseIO Unit := h.pending.update (·.map (·.erase key)) let r ← try - (upgradeAdmit h.config.clock role conn .empty expected (h.admit role scope conn) + (upgrade h.config.clock role conn expected (h.admit role scope conn) h.config.security h.config.muxers).run catch e => unregister diff --git a/packages/libp2p/host/Libp2p/Host/Upgrade.lean b/packages/libp2p/host/Libp2p/Host/Upgrade.lean new file mode 100644 index 00000000..31b74316 --- /dev/null +++ b/packages/libp2p/host/Libp2p/Host/Upgrade.lean @@ -0,0 +1,144 @@ +import Conc +import Streams +import Libp2p.Identity +import Libp2p.Core +import Libp2p.Negotiate +import Libp2p.Host.Error + +/-! +# The host's upgrade + +The upgrade of one connection, with the peer checkpoints in the place +the core seam fixes: `ConnectionGater.allowSecured` runs after the +handshake and before the muxer stage (`Libp2p/Core/Policy.lean`), as +go-libp2p's upgrader calls `InterceptSecured` +(`vendor/go-libp2p/p2p/net/upgrader/upgrader.go`, line 176). + +`Negotiate.upgradeWith` runs the same stages with no checkpoint. The +host composes the stages from the public functions of +`libp2p/negotiate` instead: `negotiate` for the security and the muxer +stages, `checkIdentity`, and `settleUpgrade`. The stage order follows +`Negotiate.upgradeCore`. A change to the order in one module needs the +same change in the other. + +The whole upgrade runs under one `Conc.withinDeadline` of +`Streams.unauthDeadlineMs` (root §5, invariant 4). A refusal at a +checkpoint is an answer, and no failure: the caller maps it to +`Host.Error.gated`. +-/ + +set_option autoImplicit false + +namespace Libp2p.Host + +open Conc Streams Libp2p.Identity Libp2p.Core + +/-- An upgraded connection: the muxer session and the peer the +handshake proved. The session's `join` also waits for the secure +connection under it, so `Upgraded.join` is the join of both. -/ +structure Upgraded where + /-- The muxer session. -/ + session : MuxSession + /-- The peer the handshake proved. -/ + remotePeer : PeerId + +/-- Wait for the session and the secure connection under it. -/ +def Upgraded.join (u : Upgraded) : ExceptT Core.Error Async Unit := + u.session.join + +/-- The answer of an upgrade that ran to its end: a session, or the +checkpoint that refused the proved peer. -/ +inductive Admission where + | upgraded (u : Upgraded) + | refused (at_ : Checkpoint) + +/-- Close a secure connection and wait for its tasks. The function +drops the answer of the join, because the caller already holds the +answer it reports. -/ +private def discardSecure (sc : SecureConn) : Async Unit := do + sc.toConnection.closeQuietly + discard sc.join.run + +/-- The session `s`, with a `join` that also waits for the secure +connection under it. The join waits for the secure connection 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 : MuxSession) (sc : SecureConn) : 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 stages: negotiate the security protocol, run the handshake, +check the identity, ask `admit` about the proved peer, negotiate the +muxer, open the session. A failure or a refusal after the handshake +closes and joins the secure connection. -/ +private def stages (role : Role) (conn : Connection) (expected : Option PeerId) + (admit : PeerId → BaseIO (Option Checkpoint)) + (secs : List SecurityProtocol) (muxers : List Muxer) : + Async (Except Core.Error Admission) := do + match ← (Negotiate.negotiate role (BufReader.new conn) conn .empty (secs.map (·.id))).run with + | .error e => return .error e + | .ok stage => + let some sec := secs.find? (fun s => decide (s.id = stage.proto)) + | return .error (.protocol "selected security protocol is not configured") + match ← (sec.handshake role conn stage.leftover).run with + | .error e => return .error e + | .ok sc => + if let .error e := Negotiate.checkIdentity expected sc.remotePeer then + discardSecure sc + return .error e + -- The checkpoint: the handshake proved the peer, and no muxer + -- byte moves before this point. + if let some c ← admit sc.remotePeer then + discardSecure sc + return .ok (.refused c) + -- The secure `read` delivers the handshake's leftover, so the + -- muxer stage starts with no bytes. + let secure := sc.toConnection + match ← (Negotiate.negotiate role (BufReader.new secure) secure .empty + (muxers.map (·.id))).run with + | .error e => discardSecure sc; return .error e + | .ok stage2 => + let some mux := muxers.find? (fun m => decide (m.id = stage2.proto)) + | discardSecure sc + return .error (.protocol "selected muxer is not configured") + match ← (mux.«open» role secure stage2.leftover).run with + | .error e => discardSecure sc; return .error e + | .ok session => + return .ok (.upgraded { session := ownSecure session sc, remotePeer := sc.remotePeer }) + +/-- Close a session that finished after the timer won, and give its +join to `late`, the task set `upgrade` joins. No caller receives that +session. -/ +private def releaseLate (late : TaskSet) : Except Core.Error Admission → BaseIO Unit + | .ok (.upgraded u) => do + discard u.session.close.toBaseIO + late.spawn (discard u.join.run) + | _ => pure () + +/-- The upgrade of `conn` under the deadline, on `clock`. The expiry +closes the connection once, at the boundary. `Negotiate.settleUpgrade` +maps the expiry to the `timeout` arm. On a failure inside the stages, +this function closes the connection. -/ +def upgrade (clock : Clock) (role : Role) (conn : Connection) (expected : Option PeerId) + (admit : PeerId → BaseIO (Option Checkpoint)) + (secs : List SecurityProtocol) (muxers : List Muxer) : + ExceptT Core.Error Async Admission := do + let late ← TaskSet.new + let answer ← withinDeadline clock Streams.unauthDeadlineMs conn.closeQuietly + (stages role conn expected admit secs muxers) (releaseLate late) + late.joinAll + match Negotiate.settleUpgrade answer with + | .ok a => return a + | .error e => + -- An error from the boundary means the expiry hook closed the + -- connection. A failure inside the work leaves it open. + if answer matches .ok _ then conn.closeQuietly + throw e + +end Libp2p.Host diff --git a/packages/libp2p/host/docs/ARCHITECTURE.md b/packages/libp2p/host/docs/ARCHITECTURE.md index 10b82a98..a9eb11eb 100644 --- a/packages/libp2p/host/docs/ARCHITECTURE.md +++ b/packages/libp2p/host/docs/ARCHITECTURE.md @@ -24,7 +24,8 @@ 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 host swap of issue #70 (see "The mock") | +| `Libp2p/Host/Upgrade.lean` | `upgrade` and `Upgraded`: the stages of `libp2p/negotiate`, with the peer checkpoint between the handshake and the muxer stage, under one deadline | +| `Libp2p/Host/StreamSelect.lean` | `negotiateStream`, multistream-select on a muxed stream, a shell over the pure core of `libp2p/negotiate` | All declarations live in the `Libp2p.Host` namespace, and the root module re-exports the public submodules. @@ -237,9 +238,16 @@ fixes them as follows. `allowInbound`, then `openConnection`, after an accept (`vendor/go-libp2p/p2p/net/upgrader/listener.go`, lines 183 and 193); and `allowSecured`, then `ConnectionScope.setPeer`, inside the - upgrade, through `Negotiate.upgradeWith` - (`vendor/go-libp2p/p2p/net/upgrader/upgrader.go`, line 176). A - refusal is `gated` with the checkpoint, and the scope is released. + upgrade, after the handshake and before the muxer stage + (`vendor/go-libp2p/p2p/net/upgrader/upgrader.go`, line 176, and the + core seam `ConnectionGater.allowSecured`). A refusal is `gated` with + the checkpoint, and the host releases the scope. +- **The host composes the upgrade.** `Negotiate.upgradeWith` takes no + checkpoint. `Libp2p/Host/Upgrade.lean` runs the stages from the + public functions of `libp2p/negotiate`: `negotiate`, `checkIdentity`, + and `settleUpgrade`. The stages keep the order of the upgrader, and + the checkpoint sits between the handshake and the muxer stage. One + `withinDeadline` bounds the whole upgrade, as in `upgradeWith`. The policy shapes are this unit's refinement of the core seams (the core ARCHITECTURE, "The policy shapes"). - **The answers of the dial path.** `dial` and `dialPeer` answer the @@ -265,9 +273,13 @@ fixes them as follows. - **Stream serving.** The serve task of a session accepts the peer's streams, and each stream runs in a task that the serve task owns and joins when the session ends. The stream negotiates against the - handler ids through `Negotiate.negotiateStream`, which puts the - bytes it read past the selecting message at the front of the stream - (§4.7). A failed negotiation, an id whose handler left the table, + handler ids through `negotiateStream`, which puts the bytes it read + past the selecting message at the front of the stream (§4.7). The + upgrader's `Negotiate.negotiate` runs over a `Connection`, and a + muxed stream is a `Stream`, so the host holds this shell + (`Libp2p/Host/StreamSelect.lean`). It drives the same pure core: + `initiatorStart`, `responderStart`, and `drive`. A failed + negotiation, an id whose handler left the table, and a handler failure reset the stream; the session stays. go-libp2p resets a stream whose negotiation fails in the same place (`vendor/go-libp2p/p2p/host/basic/basic_host.go`, line 347). A @@ -298,29 +310,13 @@ 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 mock - -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, 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 - Inside libp2p, the chain puts everything below the host at its disposal (§2, §7 row 10). The host imports `identity` for the id and key types, `core` for the seam types, and `negotiate` for the - upgrader and the stream-negotiation responder its paths call. The + stages `upgrade` composes and the pure core that `negotiateStream` + drives. The security and mux implementations arrive inside the configuration lists (§3.1), so a host module that names a concrete seam value is a review failure. Test modules import diff --git a/packages/libp2p/host/docs/PLAN.md b/packages/libp2p/host/docs/PLAN.md index c058f57c..17adc85c 100644 --- a/packages/libp2p/host/docs/PLAN.md +++ b/packages/libp2p/host/docs/PLAN.md @@ -24,15 +24,14 @@ 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. 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 -calls from `libp2p/negotiate` beside `upgrade`: the post-handshake -checkpoint (`upgradeWith`) and the stream negotiation -(`negotiateStream`). The negotiate pair records both. +Units 0 and 1a are done. Unit 1b's code builds over `libp2p/core`, +`libp2p/identity`, and `libp2p/negotiate`. The suite is +`Tests/Host.lean`. The dedup rule also carries theorems in +`Libp2p/Host/Dedup.lean`. The host composes the upgrade from the +public stages of `libp2p/negotiate`, with the peer checkpoint after +the handshake (`Libp2p/Host/Upgrade.lean`). The stream negotiation is +the host's own shell, `negotiateStream`, over the pure core of +`libp2p/negotiate` (the package ARCHITECTURE, "Stream serving"). ## Consumers @@ -80,8 +79,8 @@ checkpoint (`upgradeWith`) and the stream negotiation ## Test milestones (unit 1b) - The upgrade pipeline over the sim, in both directions: dial and - listen through the real `Noise.securityProtocol` value, or the - fixed-key test value, and `Mux.yamux` (PRINCIPLES 1.4). An + listen through the fixed-key test value `Noise.fixedKeyProtocol` and + `Mux.yamux`, on a test clock (root §3.1, PRINCIPLES 1.4). An identity-check mismatch fails with the `Host.Error` arm that wraps `Core.Error.authentication` (§4.9; the negotiate pair). - The silent-peer regression at host level (PRINCIPLES 5.4): a raw diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy.lean deleted file mode 100644 index bc5f4610..00000000 --- a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Libp2p.Negotiate.Legacy.Constants -import Libp2p.Negotiate.Legacy.Message -import Libp2p.Negotiate.Legacy.Step -import Libp2p.Negotiate.Legacy.Upgrade - -/-! -# The legacy negotiate surface - -The host of this branch still runs the pre-seam negotiate API: `upgradeWith` with the -checkpoint hook and `negotiateStream` per muxed stream. The reviewed tip carries the seam -versions of the negotiate package (issue #70 tracks the host swap), so this module keeps the -legacy entry points beside them, under their own namespace. Host files import this module -instead of `Libp2p.Negotiate`. --/ diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Constants.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Constants.lean deleted file mode 100644 index 13e04526..00000000 --- a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Constants.lean +++ /dev/null @@ -1,22 +0,0 @@ -import Libp2p.Core - -/-! -# 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. --/ - -set_option autoImplicit false - -namespace Libp2p.Negotiate.Legacy - -/-- The multistream 1.0.0 protocol id. The only protocol id literal of -the package (root §3.4). -/ -def protocolId : Libp2p.Core.ProtocolId := ⟨"/multistream/1.0.0"⟩ - -/-- The 1 KiB multistream cap (root §5.1, contract 1 of the package -docs). -/ -def maxMsg : Nat := 1024 - -end Libp2p.Negotiate.Legacy \ No newline at end of file diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Message.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Message.lean deleted file mode 100644 index bb2d68c7..00000000 --- a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Message.lean +++ /dev/null @@ -1,461 +0,0 @@ -import Libp2p.Negotiate.Legacy.Constants -import Varint -import Bytes - -/-! -# The multistream message - -`Msg` is one multistream message: a uvarint length prefix, then the -UTF-8 bytes of the text plus a trailing newline. The length counts the -newline (ARCHITECTURE §3.2, package docs "Public surface"). - -The decoder splits one frame at the index the prefix computes, then -runs the computed inverse of the payload map: it reads the body as -UTF-8, re-encodes it, and compares. `Bytes.toString?` rejects bad -UTF-8. The comparison rejects a missing trailing newline and a model -value at or above 256. So the `encodeDecode` proof needs no UTF-8 -reasoning. - -The 1 KiB cap is checked in `splitFrame`, before any payload -inspection (contract 1). The `ls` reply framing walks its entries as -ordinary `Msg` frames on a fuel counter, so the entry reader reuses -the proved frame decoder. --/ - -set_option autoImplicit false - -namespace Libp2p.Negotiate.Legacy - -open Bytes (DecodeError) - -/-! ## The payload map and its inverse -/ - -/-- The model bytes of a text, newline included. The one total map -between texts and payloads. -/ -def payloadOf (s : String) : List Nat := - Bytes.toNatList (Bytes.ofString (s ++ "\n")) - -/-- A total `UVarint` constructor for a length. `initiatorStart` and -`responderStart` keep the upgrade's lengths at or under `maxMsg`; the -modulo keeps the constructor total for any input. -/ -def boundedVarint (n : Nat) : Varint.UVarint := - ⟨n % Varint.limit, Nat.mod_lt _ (by decide)⟩ - -/-- The total text encoder: a uvarint length prefix, then the payload. -/ -def encodeText (s : String) : List Nat := - Varint.encode (boundedVarint (payloadOf s).length) ++ payloadOf s - -/-- A multistream message. `text` excludes the trailing newline. -`fits` is the proof-carrying cap fact of root §3.7: the message fits -the 1 KiB cap, so the encoder writes the exact length. -/ -structure Msg where - text : String - fits : (Bytes.ofString (text ++ "\n")).size ≤ maxMsg - deriving Repr, DecidableEq - -/-- The model payload length equals the byte size of the text with its -newline. -/ -theorem payloadOfLength (s : String) : - (payloadOf s).length = (Bytes.ofString (s ++ "\n")).size := by - simp only [payloadOf, Bytes.toNatList, List.length_map, Array.length_toList] - rfl - -/-- The payload of a text is its UTF-8 bytes plus the newline byte. -/ -theorem payloadOfEq (s : String) : - payloadOf s = Bytes.toNatList (Bytes.ofString s) ++ [10] := by - simp [payloadOf, Bytes.toNatList, Bytes.ofString, String.toByteArray_append] - exact ⟨10, by decide, rfl⟩ - -/-- Every payload ends in a newline, so it is never empty. -/ -theorem payloadOfNe (s : String) : payloadOf s ≠ [] := by - rw [payloadOfEq]; simp - -/-- The checked constructor. The tests build messages through it. -/ -def Msg.ofText? (s : String) : Option Msg := - if h : (Bytes.ofString (s ++ "\n")).size ≤ maxMsg then some ⟨s, h⟩ else none - -/-- A text whose frame fits the 1 KiB cap. `initiatorStart` and -`responderStart` call this before any write, so a configured id that -would produce an over-cap frame is a protocol error rather than a frame -the decoder refuses (root §5.1). -/ -def fitsText (s : String) : Bool := - decide ((Bytes.ofString (s ++ "\n")).size ≤ maxMsg) - -/-- The frame the codec writes for a message. -/ -def encodeMsg (m : Msg) : List Nat := encodeText m.text - -/-- The multistream header message. The literal lives in `Constants`. -/ -def header : Msg := ⟨protocolId.toString, by decide⟩ - -/-! ## The frame split -/ - -/-- Split one frame at the index the length prefix computes. The cap -is checked first, before any payload inspection (contract 1). A zero -declared length is malformed. A payload cut short is truncated, so -the caller keeps waiting. -/ -def splitFrame (bs : List Nat) : Except DecodeError (List Nat × List Nat) := - match Varint.decode? bs with - | .error e => .error e - | .ok (v, rest) => - if maxMsg < v.val then .error .malformed - else if v.val = 0 then .error .malformed - else if rest.length < v.val then .error .truncated - else .ok (rest.take v.val, rest.drop v.val) - -/-- The computed inverse of `payloadOf`, checked by re-encoding. -/ -def textOf? (payload : List Nat) : Option String := - match Bytes.toString? (Bytes.ofNatList payload.dropLast) with - | none => none - | some t => if payloadOf t = payload then some t else none - -/-- A text read back from a payload re-encodes to that payload. -/ -theorem textOf?Spec {payload : List Nat} {t : String} (h : textOf? payload = some t) : - payloadOf t = payload := by - unfold textOf? at h - split at h - · simp at h - · split at h - · simp_all - · simp at h - -/-- The inverse reads its own image back. -/ -theorem textOf?PayloadOf (s : String) : textOf? (payloadOf s) = some s := by - unfold textOf? - have hd : (payloadOf s).dropLast = Bytes.toNatList (Bytes.ofString s) := by - rw [payloadOfEq]; simp - rw [hd, Bytes.ofNatListToNatList, Bytes.toString?OfString] - simp - -/-- A payload whose last byte is not the newline reads back as no -text. -/ -theorem textOf?None {payload : List Nat} (hlast : payload.getLast? ≠ some 10) : - textOf? payload = none := by - unfold textOf? - cases hto : Bytes.toString? (Bytes.ofNatList payload.dropLast) with - | none => rfl - | some t => - by_cases heq : payloadOf t = payload - · have hpl : (payloadOf t).getLast? = some 10 := by rw [payloadOfEq]; simp - rw [heq] at hpl - exact (hlast hpl).elim - · simp [heq] - -/-- Decode one message and the bytes left after it. -/ -def decodeMsg? (bs : List Nat) : Except DecodeError (Msg × List Nat) := - match splitFrame bs with - | .error e => .error e - | .ok (payload, rest) => - match textOf? payload with - | none => .error .malformed - | some t => - if hf : (Bytes.ofString (t ++ "\n")).size ≤ maxMsg then .ok (⟨t, hf⟩, rest) - else .error .malformed - -/-! ## The frame lemmas -/ - -/-- One shared lemma: a framed payload splits back into that payload -and the remainder. -/ -theorem splitFrameEncode (s : String) (h : (payloadOf s).length ≤ maxMsg) (rest : List Nat) : - splitFrame (encodeText s ++ rest) = .ok (payloadOf s, rest) := by - have hlim : (payloadOf s).length < Varint.limit := by - unfold Varint.limit Varint.maxBytes maxMsg at *; omega - have hb : (boundedVarint (payloadOf s).length).val = (payloadOf s).length := by - simp [boundedVarint, Nat.mod_eq_of_lt hlim] - have hpos : 0 < (payloadOf s).length := List.length_pos_iff.mpr (payloadOfNe s) - unfold splitFrame encodeText - rw [List.append_assoc, Varint.decodeEncodeSuffix] - simp only [hb] - have h1 : ¬ maxMsg < (payloadOf s).length := by omega - have h2 : ¬ (payloadOf s).length = 0 := by omega - simp [h1, h2] - -/-- The suffix round trip: a message decodes back from its frame plus -any remainder. The lazy dialer's coalesced read needs this form. The -frame is `encodeText m.text`, definitionally `encodeMsg m`. -/ -theorem decodeMsgSuffix (m : Msg) (rest : List Nat) : - decodeMsg? (encodeText m.text ++ rest) = .ok (m, rest) := by - have h : (payloadOf m.text).length ≤ maxMsg := by rw [payloadOfLength]; exact m.fits - unfold decodeMsg? - rw [splitFrameEncode m.text h] - simp [textOf?PayloadOf, m.fits] - -/-- The inverse direction: every accepted input is the encoding of -the decoded value. No UTF-8 reasoning; `textOf?` already re-encoded. -/ -theorem decodeMsgEncodeDecode (bs : List Nat) (m : Msg) (rest : List Nat) - (h : decodeMsg? bs = .ok (m, rest)) : encodeMsg m ++ rest = bs := by - show encodeText m.text ++ rest = bs - unfold decodeMsg? splitFrame at h - split at h - · simp at h - · rename_i payload rest0 hsplit - split at hsplit - · simp at hsplit - · rename_i v r0 hdec - have hbs := Varint.encodeDecode hdec - split at hsplit - · simp at hsplit - split at hsplit - · simp at hsplit - split at hsplit - · simp at hsplit - rename_i hcap _ hlen - simp only [Except.ok.injEq, Prod.mk.injEq] at hsplit - obtain ⟨rfl, rfl⟩ := hsplit - split at h - · simp at h - · rename_i t ht - have hp := textOf?Spec ht - split at h - · simp only [Except.ok.injEq, Prod.mk.injEq] at h - obtain ⟨rfl, rfl⟩ := h - have hl : (payloadOf t).length = v.val := by - rw [hp]; simp; omega - have hv : boundedVarint (payloadOf t).length = v := by - cases v; simp_all [boundedVarint, Nat.mod_eq_of_lt] - rw [encodeText, hv, hp, List.append_assoc, List.take_append_drop] - exact hbs.symm - · simp at h - -/-- The codec writes the frame and reads one message back. -/ -instance : Bytes.Codec Msg where - encode := encodeMsg - decode? := decodeMsg? - -theorem decodeMsgEncode (m : Msg) : decodeMsg? (encodeMsg m) = .ok (m, []) := by - simpa [encodeMsg] using decodeMsgSuffix m [] - -/-- The round-trip law that §3.2 requires. -/ -instance : Bytes.LawfulCodec Msg where - decodeEncode := decodeMsgEncode - encodeDecode := by - intro bs a rest h - exact decodeMsgEncodeDecode bs a rest h - -/-- The cap fires before the payload is read, for every payload that -follows the prefix (contract 1). -/ -theorem decodeMsgCap {v : Varint.UVarint} {payload : List Nat} - (h : maxMsg < v.val) : - decodeMsg? (Varint.encode v ++ payload) = .error .malformed := by - simp [decodeMsg?, splitFrame, Varint.decodeEncodeSuffix, h] - -/-- A payload cut short is incomplete: more bytes may complete it. -/ -theorem decodeMsgTruncated {v : Varint.UVarint} {payload : List Nat} - (hv0 : 0 < v.val) (hcap : v.val ≤ maxMsg) (hshort : payload.length < v.val) : - decodeMsg? (Varint.encode v ++ payload) = .error .truncated := by - unfold decodeMsg? splitFrame - rw [Varint.decodeEncodeSuffix] - have h1 : ¬ maxMsg < v.val := by omega - have h2 : ¬ v.val = 0 := by omega - simp only [h1, h2, hshort, ite_true, ite_false] - -/-- A zero declared length is malformed. -/ -theorem decodeMsgZeroLength {v : Varint.UVarint} {payload : List Nat} - (h : v.val = 0) : - decodeMsg? (Varint.encode v ++ payload) = .error .malformed := by - simp [decodeMsg?, splitFrame, Varint.decodeEncodeSuffix, h, maxMsg] - -/-- A body whose last byte is not the newline is malformed. -/ -theorem decodeMsgNoNewline {v : Varint.UVarint} {payload : List Nat} - (hv0 : 0 < v.val) (hcap : v.val ≤ maxMsg) (hlen : payload.length = v.val) - (hlast : payload.getLast? ≠ some 10) : - decodeMsg? (Varint.encode v ++ payload) = .error .malformed := by - have hnone : textOf? (List.take v.val payload) = none := by - rw [← hlen, List.take_length] - exact textOf?None hlast - unfold decodeMsg? splitFrame - rw [Varint.decodeEncodeSuffix] - have h1 : ¬ maxMsg < v.val := by omega - have h2 : ¬ v.val = 0 := by omega - have h3 : ¬ payload.length < v.val := by omega - simp only [h1, h2, h3, ite_false] - rw [hnone] - -/-- The framing budget: a message frame spans its payload plus at -most nine prefix bytes. -/ -theorem encodeMsgLength (m : Msg) : - (encodeMsg m).length ≤ maxMsg + Varint.maxBytes := by - have h1 := Varint.lengthEncodeLe (boundedVarint (payloadOf m.text).length) - have h2 : (payloadOf m.text).length ≤ maxMsg := by rw [payloadOfLength]; exact m.fits - simp only [encodeMsg, encodeText, List.length_append] - omega - -/-! ## The `ls` reply framing -/ - -/-- 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 Libp2p.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 Libp2p.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 Libp2p.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 Libp2p.Core.ProtocolId) - | 0, _ => .error .malformed - | fuel + 1, bs => - if bs = [10] then .ok [] - else match decodeMsg? bs with - | .error _ => .error .malformed - | .ok (m, rest) => (decodeEntries fuel rest).map (⟨m.text⟩ :: ·) - -/-- Decode one `ls` reply frame. The outer prefix goes through the -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 Libp2p.Core.ProtocolId × List Nat) := - match splitFrame bs with - | .error e => .error e - | .ok (body, rest) => (decodeEntries body.length body).map (·, rest) - -/-- An entry frame is at least as long as its payload. -/ -theorem encodeTextLength (s : String) : (payloadOf s).length ≤ (encodeText s).length := by - simp [encodeText] - -/-- The entries of an encoded list read back in order, under fuel and -cap bounds. -/ -theorem decodeEntriesLs (ids : List Libp2p.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 - | nil => - cases fuel with - | zero => simp at hf - | succ f => simp [decodeEntries, lsEntries] - | cons p ps ih => - cases fuel with - | zero => simp at hf - | succ f => - have hlen : (lsEntries (p :: ps)).length = - (encodeText p.toString).length + (lsEntries ps).length := by - simp [lsEntries] - have hfit : (Bytes.ofString (p.toString ++ "\n")).size ≤ maxMsg := by - rw [← payloadOfLength]; have := encodeTextLength p.toString; omega - have hne : lsEntries (p :: ps) ++ [10] ≠ [10] := by - intro h - have hl := congrArg List.length h - rw [List.length_append, hlen] at hl - have h0 := List.length_pos_iff.mpr (payloadOfNe p.toString) - have h1 := encodeTextLength p.toString - simp only [List.length_singleton] at hl - omega - have hsplit : lsEntries (p :: ps) ++ [10] = - encodeText (Msg.text ⟨p.toString, hfit⟩) ++ (lsEntries ps ++ [10]) := by - simp [lsEntries] - simp only [decodeEntries, hne, ite_false] - rw [hsplit, decodeMsgSuffix ⟨p.toString, hfit⟩ (lsEntries ps ++ [10])] - change (Except.map (fun x => (⟨p.toString⟩ : Libp2p.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 Libp2p.Core.ProtocolId) : - ids.length ≤ (lsEntries ids).length := by - induction ids with - | nil => simp [lsEntries] - | cons p ps ih => - have h0 := List.length_pos_iff.mpr (payloadOfNe p.toString) - have := encodeTextLength p.toString - simp [lsEntries] at ih ⊢; omega - -/-- The `ls` reply round trip. The length prefix alone delimits the -entries, so no cleanliness hypothesis is needed. -/ -theorem decodeLsEncodeLs (ids : List Libp2p.Core.ProtocolId) - (hbody : (lsBody ids).length ≤ maxMsg) : - decodeLs? (encodeLs ids) = .ok (ids, []) := by - have hlim : (lsBody ids).length < Varint.limit := by - unfold Varint.limit Varint.maxBytes maxMsg at *; omega - have hb : (boundedVarint (lsBody ids).length).val = (lsBody ids).length := by - simp [boundedVarint, Nat.mod_eq_of_lt hlim] - have hl := lsEntriesLength ids - unfold decodeLs? encodeLs splitFrame - rw [← List.append_nil (lsBody ids), Varint.decodeEncodeSuffix] - simp only [hb, List.append_nil] - have h1 : ¬ maxMsg < (lsBody ids).length := by omega - have h2 : ¬ (lsBody ids).length = 0 := by simp [lsBody] - simp only [h1, h2, ite_false, Nat.lt_irrefl, List.take_length, List.drop_length] - have hb2 : (lsEntries ids).length ≤ maxMsg := by simp [lsBody] at hbody; omega - rw [lsBody, decodeEntriesLs ids _ (by simp; omega) hb2] - rfl - -/-- A frame that splits back is exactly the prefix plus body plus -remainder. -/ -theorem splitFrameInv {bs body rest : List Nat} (h : splitFrame bs = .ok (body, rest)) : - Varint.encode (boundedVarint body.length) ++ body ++ rest = bs := by - unfold splitFrame at h - split at h - · simp at h - · rename_i v r0 hdec - have hbs := Varint.encodeDecode hdec - split at h - · simp at h - split at h - · simp at h - split at h - · simp at h - rename_i hcap _ hlen - simp only [Except.ok.injEq, Prod.mk.injEq] at h - obtain ⟨rfl, rfl⟩ := h - have hl : (r0.take v.val).length = v.val := by simp; omega - have hv : boundedVarint (r0.take v.val).length = v := by - cases v; simp_all [boundedVarint, Nat.mod_eq_of_lt] - rw [hv, List.append_assoc, List.take_append_drop] - exact hbs.symm - -/-- Entries that read back are exactly the encoding of the list. -/ -theorem decodeEntriesInv (f : Nat) (bs : List Nat) (ids : List Libp2p.Core.ProtocolId) - (h : decodeEntries f bs = .ok ids) : lsEntries ids ++ [10] = bs := by - induction f generalizing bs ids with - | zero => simp [decodeEntries] at h - | succ f ih => - unfold decodeEntries at h - split at h - · rename_i hb - simp only [Except.ok.injEq] at h - subst h - simp [lsEntries, hb] - · split at h - · simp at h - · rename_i m rest hm - cases hr : decodeEntries f rest with - | error e => simp [hr, Except.map] at h - | ok ids' => - simp [hr, Except.map] at h - subst h - have h1 := decodeMsgEncodeDecode bs m rest hm - have h2 := ih rest ids' hr - simp only [lsEntries, List.map_cons, List.flatten_cons, List.append_assoc] at h2 ⊢ - rw [h2] - exact h1 - -/-- 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 Libp2p.Core.ProtocolId} {rest : List Nat} - (h : decodeLs? bs = .ok (ids, rest)) : encodeLs ids ++ rest = bs := by - unfold decodeLs? at h - split at h - · simp at h - · rename_i body r hs - cases he : decodeEntries body.length body with - | error e => simp [he, Except.map] at h - | ok ids' => - simp [he, Except.map] at h - obtain ⟨rfl, rfl⟩ := h - have hb := decodeEntriesInv _ _ _ he - have hs' := splitFrameInv hs - unfold encodeLs lsBody - rw [hb] - exact hs' - -end Libp2p.Negotiate.Legacy \ No newline at end of file diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Step.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Step.lean deleted file mode 100644 index 8fedc1b1..00000000 --- a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Step.lean +++ /dev/null @@ -1,509 +0,0 @@ -import Libp2p.Negotiate.Legacy.Message -import Libp2p.Core -import Bytes - -/-! -# The pure negotiation core - -`State`, `Event`, `Action`, and `step` are the pure state machine of -multistream-select (root §3.3). One `Event.bytes` feeds raw bytes, and -the core decodes exactly one frame per call, so the -malformed-versus-incomplete call stays in the core (§3.1). A decoded -frame goes through a private `classify` step that names the answer, -then a private `act` step that performs it. The theorems about the -chosen id reason over `classify`; the theorems about writes and phase -reason over `act`. - -The step returns `Except Error (State × List Action)`, the root §3.3 -shape. `Action` has no error constructor (package docs, "Decisions"): -the `Except` channel carries the failure (root §3.5). --/ - -set_option autoImplicit false - -namespace Libp2p.Negotiate.Legacy - -open Bytes (DecodeError) - -/-- The phase of one negotiation. -/ -inductive Phase where - | headerPending - | negotiating - | awaitingAnswer - | selected - deriving Repr, DecidableEq - -/-- The core state. `role` is the side. `supported` is the responder's -ordered list. `proposals` is the initiator's remaining list, in order. -`buffer` holds the bytes no frame has consumed yet. -/ -structure State where - role : Libp2p.Core.Role - supported : List Libp2p.Core.ProtocolId - proposals : List Libp2p.Core.ProtocolId - buffer : List Nat - phase : Phase - deriving Repr, DecidableEq - -/-- One input to the core. Raw bytes arrive as one event; a proposal -is the local dialer's input. -/ -inductive Event where - | bytes (bs : List Nat) - | propose (p : Libp2p.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 : Libp2p.Core.ProtocolId) (leftover : List Nat) - deriving Repr, DecidableEq - -/-- The replies the responder sends, the closed set of §3.4. -/ -inductive Reply where - | na - | ls - deriving DecidableEq, Repr, Hashable - -/-- The wire text of a reply. -/ -def Reply.text : Reply → String - | .na => "na" - | .ls => "ls" - -/-- The table the inverse searches. -/ -def Reply.all : List Reply := [.na, .ls] - -/-- The computed inverse of `Reply.text`: a text names a reply when it -equals the reply's text. -/ -def Reply.ofText? (s : String) : Option Reply := Reply.all.find? (fun r => r.text = s) - -/-- The table conformance: the inverse reads exactly the reply whose -text it is given. -/ -theorem Reply.ofText?EqSome {s : String} {r : Reply} : - Reply.ofText? s = some r ↔ r.text = s := by - constructor - · intro h - have := List.find?_some h - simpa using this - · intro h - subst h - have hmem : r ∈ Reply.all := by cases r <;> simp [Reply.all] - unfold Reply.ofText? - cases r <;> simp [Reply.all, Reply.text] - -/-- The reply as a message. The text is the message text. -/ -def Reply.toMsg : Reply → Msg - | .na => ⟨"na", by decide⟩ - | .ls => ⟨"ls", by decide⟩ - -/-- The message form of the reply recognition. -/ -def Reply.ofMsg? (m : Msg) : Option Reply := Reply.ofText? m.text - -/-- Why a negotiation failed. `decode` carries a frame the decoder -rejects. `negotiationFailed` covers a bad exchange, an exhausted -proposal list, and an invalid local list at start. -/ -inductive Error where - | decode (e : DecodeError) - | negotiationFailed - deriving Repr, DecidableEq, Hashable - -/-- The pure negotiation core of the spike: the first of `ours` that -`theirs` also supports. -/ -def choose (ours theirs : List Libp2p.Core.ProtocolId) : Option Libp2p.Core.ProtocolId := - List.find? theirs.contains ours - -/-- A chosen id is in our list and supported by theirs. -/ -theorem chooseSpec {ours theirs : List Libp2p.Core.ProtocolId} {p : Libp2p.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⟩ - -/-! ## The answers -/ - -/-- What a decoded text means for this state. Byte-free, so the -theorems about the chosen id reason over this classification. -/ -private inductive Answer where - | echo - | listIds - | pick (p : Libp2p.Core.ProtocolId) - | refuse - | advance - | retry (q : Libp2p.Core.ProtocolId) (ps : List Libp2p.Core.ProtocolId) - | accept (p : Libp2p.Core.ProtocolId) - | fail - -/-- Classify a decoded text for a state. -/ -private def classify (s : State) (text : String) : Answer := - match s.role, s.phase with - | .responder, .headerPending => if text = protocolId.toString then .echo else .fail - | .responder, .negotiating => - match Reply.ofText? text with - | some .ls => .listIds - | _ => - if text = protocolId.toString then .advance - else if (⟨text⟩ : Libp2p.Core.ProtocolId) ∈ s.supported then .pick ⟨text⟩ - else .refuse - | .initiator, .negotiating => if text = protocolId.toString then .advance else .fail - | .initiator, .awaitingAnswer => - match s.proposals with - | [] => .fail - | p :: ps => - if Reply.ofText? text = some .na then - match ps with - | [] => .fail - | q :: qs => .retry q (q :: qs) - else if text = p.toString then .accept p else .fail - | _, _ => .fail - -/-- Perform an answer. It decodes nothing, so its theorems need no -decoder facts. -/ -private def act (s : State) (rest : List Nat) : Answer → Except Error (State × List Action) - | .echo => .ok ({ s with buffer := rest, phase := .negotiating }, [.write (encodeText protocolId.toString)]) - | .listIds => .ok ({ s with buffer := rest }, [.write (encodeLs s.supported)]) - | .pick p => .ok ({ s with buffer := [], phase := .selected }, - [.write (encodeText p.toString), .select p rest]) - | .refuse => .ok ({ s with buffer := rest }, [.write (encodeMsg (Reply.toMsg .na))]) - | .advance => - match s.role with - | .initiator => .ok ({ s with buffer := rest, phase := .awaitingAnswer }, []) - | .responder => .ok ({ s with buffer := rest }, []) - | .retry q ps => .ok ({ s with buffer := rest, proposals := ps }, [.write (encodeText q.toString)]) - | .accept p => .ok ({ s with buffer := [], phase := .selected }, [.select p rest]) - | .fail => .error .negotiationFailed - -/-- A proposal event. An initiator in the header phase with an empty list -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 : Libp2p.Core.ProtocolId) : Except Error (State × List Action) := - if s.role = .initiator then - if s.phase = .headerPending then - if s.proposals = [] then - .ok ({ s with proposals := [p], phase := .negotiating }, - [.write (encodeMsg header ++ encodeText p.toString)]) - else .ok (s, []) - else .ok (s, []) - else .ok (s, []) - -/-- One transition of the core. A `bytes` event appends to the buffer -and decodes one frame. `truncated` keeps the buffer and waits; -`malformed` is a protocol error; a decoded frame goes through -`classify` and `act`. -/ -def step (s : State) : Event → Except Error (State × List Action) - | .propose p => propose s p - | .bytes bs => - match decodeMsg? (s.buffer ++ bs) with - | .error .truncated => .ok ({ s with buffer := s.buffer ++ bs }, []) - | .error .malformed => .error (.decode .malformed) - | .ok (m, rest) => act s rest (classify s m.text) - -/-! ## The answer lemmas -/ - -/-- 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 : Libp2p.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 - <;> ((try split at h) - <;> (try simp only [Except.ok.injEq, Prod.mk.injEq] at h) - <;> (try obtain ⟨-, rfl⟩ := h) - <;> (try simp_all)) - -/-- A pick comes from the responder's supported list. -/ -private theorem classifyPick {s : State} {t : String} {p : Libp2p.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 : Libp2p.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 : Libp2p.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 : Libp2p.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 : Libp2p.Core.ProtocolId} - (hr : s.role = .initiator) (h : classify s t = .pick p) : False := by - unfold classify at h - repeat' split at h - all_goals simp_all - -/-- An initiator never sees the echo answer. -/ -private theorem classifyEchoInitiator {s : State} {t : String} - (hr : s.role = .initiator) (h : classify s t = .echo) : False := by - unfold classify at h - repeat' split at h - all_goals simp_all - -/-- An initiator never sees the list answer. -/ -private theorem classifyListIdsInitiator {s : State} {t : String} - (hr : s.role = .initiator) (h : classify s t = .listIds) : False := by - unfold classify at h - repeat' split at h - all_goals simp_all - -/-- An initiator never sees the refuse answer. -/ -private theorem classifyRefuseInitiator {s : State} {t : String} - (hr : s.role = .initiator) (h : classify s t = .refuse) : False := by - unfold classify at h - repeat' split at h - all_goals simp_all - -/-- The `ls` text in the negotiation draws the list answer. -/ -private theorem classifyListIds {s : State} {t : String} - (hrole : s.role = .responder) (hphase : s.phase = .negotiating) - (hls : Reply.ofText? t = some .ls) : classify s t = .listIds := by - unfold classify - rw [hrole, hphase] - rw [hls] - -/-- 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⟩ : Libp2p.Core.ProtocolId) ∉ s.supported) - (hheader : t ≠ protocolId.toString) (hreply : Reply.ofText? t = none) : - classify s t = .refuse := by - unfold classify - rw [hrole, hphase] - simp only [hreply] - 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 : Libp2p.Core.ProtocolId} - {ps : List Libp2p.Core.ProtocolId} (h : classify s t = .retry q ps) : - s.proposals.tail = ps := by - unfold classify at h - repeat' split at h - all_goals (cases h <;> simp_all [List.tail_cons]) - -/-- A write came from one of the five writing answers. -/ -private theorem actWriteAnswer {s : State} {rest : List Nat} {v : Answer} {s' : State} - {actions : List Action} {w : List Nat} - (h : act s rest v = .ok (s', actions)) (hw : Action.write w ∈ actions) : - v = .echo ∨ v = .listIds ∨ (∃ p, v = .pick p) ∨ v = .refuse ∨ - (∃ q ps, v = .retry q ps) := by - cases v with - | echo => exact Or.inl rfl - | listIds => exact Or.inr (Or.inl rfl) - | pick p => exact Or.inr (Or.inr (Or.inl ⟨p, rfl⟩)) - | refuse => exact Or.inr (Or.inr (Or.inr (Or.inl rfl))) - | retry q ps => exact Or.inr (Or.inr (Or.inr (Or.inr ⟨q, ps, rfl⟩))) - | advance => - simp only [act] at h - split at h <;> simp only [Except.ok.injEq, Prod.mk.injEq] at h - all_goals (obtain ⟨-, rfl⟩ := h; simp at hw) - | accept p => - simp only [act] at h - simp only [Except.ok.injEq, Prod.mk.injEq] at h - obtain ⟨-, rfl⟩ := h - simp at hw - | fail => - simp only [act] at h - cases h - -/-- The list answer writes the `ls` reply and stays in the phase. -/ -private theorem actListIds {s : State} {rest : List Nat} {s' : State} {actions : List Action} - (h : act s rest .listIds = .ok (s', actions)) : - actions = [.write (encodeLs s.supported)] ∧ s'.phase = s.phase ∧ s'.buffer = rest := by - unfold act at h - simp only [Except.ok.injEq, Prod.mk.injEq] at h - obtain ⟨hstate, hact⟩ := h - subst hact - rw [← hstate] - simp - -/-- The refuse answer writes the `na` frame and stays in the phase. -/ -private theorem actRefuse {s : State} {rest : List Nat} {s' : State} {actions : List Action} - (h : act s rest .refuse = .ok (s', actions)) : - actions = [.write (encodeMsg (Reply.toMsg .na))] ∧ s'.phase = s.phase ∧ s'.buffer = rest := by - unfold act at h - simp only [Except.ok.injEq, Prod.mk.injEq] at h - obtain ⟨hstate, hact⟩ := h - subst hact - rw [← hstate] - simp - -/-- The retry answer replaces the proposals with the remaining list. -/ -private theorem actRetryWrites {s : State} {rest : List Nat} {q : Libp2p.Core.ProtocolId} - {ps : List Libp2p.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 - obtain ⟨hstate, _⟩ := h - rw [← hstate] - -/-! ## The step theorems -/ - -/-- A responder selects only from its supported list (contract 2). -/ -theorem stepSelectResponderMem {s : State} {bs : List Nat} {s' : State} - {actions : List Action} {p : Libp2p.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 - simp only [step] at hstep - split at hstep - · simp only [Except.ok.injEq, Prod.mk.injEq] at hstep - obtain ⟨-, rfl⟩ := hstep - simp at hmem - · simp at hstep - · rcases actSelect hstep hmem with hv | hv - · exact classifyPick hv - · exact (classifyAcceptResponder hrole hv).elim - -/-- An initiator selects only from its own proposal list. -/ -theorem stepSelectInitiatorMem {s : State} {bs : List Nat} {s' : State} - {actions : List Action} {p : Libp2p.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 - simp only [step] at hstep - split at hstep - · simp only [Except.ok.injEq, Prod.mk.injEq] at hstep - obtain ⟨-, rfl⟩ := hstep - simp at hmem - · simp at hstep - · rcases actSelect hstep hmem with hv | hv - · exact (classifyPickInitiator hrole hv).elim - · exact classifyAcceptInitiator hv - -/-- A step that writes advances the initiator's proposal list by one -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 : Libp2p.Core.ProtocolId} {ps : List Libp2p.Core.ProtocolId} - {w : List Nat} - (hrole : s.role = .initiator) (hprop : s.proposals = p :: ps) - (hstep : step s (.bytes bs) = .ok (s', actions)) - (hwrite : Action.write w ∈ actions) : - s'.proposals = ps ∧ s'.proposals.length < s.proposals.length := by - simp only [step] at hstep - split at hstep - · simp only [Except.ok.injEq, Prod.mk.injEq] at hstep - obtain ⟨-, rfl⟩ := hstep - simp at hwrite - · simp at hstep - · rcases actWriteAnswer hstep hwrite with hc | hc | hc | hc | hc - · exact (classifyEchoInitiator hrole hc).elim - · exact (classifyListIdsInitiator hrole hc).elim - · rcases hc with ⟨p', hc⟩ - exact (classifyPickInitiator hrole hc).elim - · exact (classifyRefuseInitiator hrole hc).elim - · rcases hc with ⟨q, ps', hc⟩ - rw [hc] at hstep - have hnew : s'.proposals = ps' := actRetryWrites hstep - have htail : s.proposals.tail = ps' := classifyRetryTail hc - have hps : ps' = ps := by - rw [← htail, hprop] - rfl - constructor - · rw [hnew, hps] - · rw [hnew, hps, hprop] - simp only [List.length_cons] - omega - -/-- The `ls` answer writes the reply and stays in the negotiation -(contract 3). -/ -theorem stepResponderLsStays {s : State} {bs : List Nat} {s' : State} - {actions : List Action} {m : Msg} {rest : List Nat} - (hrole : s.role = .responder) (hphase : s.phase = .negotiating) - (hdec : decodeMsg? (s.buffer ++ bs) = .ok (m, rest)) - (hls : Reply.ofMsg? m = some .ls) - (hstep : step s (.bytes bs) = .ok (s', actions)) : - actions = [.write (encodeLs s.supported)] ∧ s'.phase = .negotiating ∧ s'.buffer = rest := by - simp only [step, hdec] at hstep - have hc := classifyListIds hrole hphase hls - rw [hc] at hstep - have ha := actListIds hstep - rcases ha with ⟨hacts, hphase', hbuf⟩ - constructor - · exact hacts - constructor - · rw [hphase'] - exact hphase - · exact hbuf - -/-- 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 : Libp2p.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) - (hheader : m.text ≠ protocolId.toString) - (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⟩ : Libp2p.Core.ProtocolId) ∉ s.supported := by - intro hm - apply hnot - simpa [htext] using hm - simp only [step, hdec] at hstep - have hc := classifyRefuse hrole hphase hnot' hheader hreply - rw [hc] at hstep - have ha := actRefuse hstep - rcases ha with ⟨hacts, hphase', hbuf⟩ - constructor - · exact hacts - constructor - · rw [hphase'] - exact hphase - · exact hbuf - -/-- 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 : Libp2p.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])) : - s.buffer ++ bs = encodeText p.toString ++ rest := by - simp only [step, hdec] at hstep - have hmem : Action.select p rest ∈ [Action.select p rest] := by simp - have hv := actSelect hstep hmem - rcases hv with hc | hc - · exact (classifyPickInitiator hrole hc).elim - · have hpt : p.toString = m.text := classifyAcceptText hc - rw [hc] at hstep - have hr : r = rest := by - unfold act at hstep - simp only [Except.ok.injEq, Prod.mk.injEq] at hstep - obtain ⟨-, hact⟩ := hstep - injection hact with hsel hnil - injection hsel with hp hrest - have hlaw : encodeText m.text ++ r = s.buffer ++ bs := - decodeMsgEncodeDecode (s.buffer ++ bs) m r hdec - rw [← hlaw] - rw [← hpt] - rw [hr] - -/-- A truncated buffer waits: no actions, no error, the phase holds, -and the buffer keeps the bytes (§3.1). -/ -theorem stepTruncatedWaits {s : State} {bs : List Nat} {s' : State} {actions : List Action} - (hdec : decodeMsg? (s.buffer ++ bs) = .error .truncated) - (hstep : step s (.bytes bs) = .ok (s', actions)) : - actions = [] ∧ s'.phase = s.phase ∧ s'.buffer = s.buffer ++ bs := by - simp only [step, hdec] at hstep - simp only [Except.ok.injEq, Prod.mk.injEq] at hstep - obtain ⟨hstate, hact⟩ := hstep - subst hact - rw [← hstate] - simp - -end Libp2p.Negotiate.Legacy \ No newline at end of file diff --git a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Upgrade.lean b/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Upgrade.lean deleted file mode 100644 index 3587d597..00000000 --- a/packages/libp2p/negotiate/Libp2p/Negotiate/Legacy/Upgrade.lean +++ /dev/null @@ -1,639 +0,0 @@ -import Libp2p.Negotiate.Legacy.Step -import Libp2p.Negotiate.Legacy.Message -import Libp2p.Core -import Libp2p.Identity -import Streams.Conn -import Streams.BufReader -import Streams.Constants -import Conc -import Bytes - -/-! -# The upgrader - -`Upgrade` walks a raw `Connection` through security negotiation, the -security handshake, the identity check, and muxer negotiation into a -`MuxSession` (root §4.9, negotiate ARCHITECTURE, "Public surface"). The -pure part is `drive`: one fuel-bounded run over a byte cursor that -feeds the 1a core one `Event.bytes` call per complete frame. The IO -part is `negotiate`, one negotiation stage, and `upgradeWith`, the -three-stage pipeline under one `Conc.withinDeadline`. - -The driver owns the byte cursor. It never reads `s.buffer`; it resets -the buffer before every `step` call, and every unconsumed byte stays -in the `input` argument. The `leftover` field of the result is -authoritative. The shell passes the driver's own states and leftovers -back unchanged. - -The negotiation loop parks on the connection read until a selection, -an error, a close, or the deadline (root §3.3). No measure bounds that -wait, so the loop keeps the package's `repeat` form, the form of -`Conc.TaskSet.joinAll`, and stays outside the proved core. The pure -`drive` is total, and its theorems carry no IO obligation. - -The three stages thread the leftover bytes by contract 5 of the -package docs: the negotiation leftover seeds the handshake, the -secure connection delivers the handshake leftover through its reader, -and the muxer negotiation leftover reaches `Muxer.open`. --/ - -set_option autoImplicit false - -namespace Libp2p.Negotiate.Legacy - -open Bytes (DecodeError) - -/-! ## The driver -/ - -/-- The answer of one driver run. - -* `selected p consumed leftover writes`: a `step` selected `p`. - `consumed` is the concatenation of the encoded frames the run - consumed, the selected frame included. `leftover` is the byte suffix - after it. `writes` are the `Action.write` payloads, in order. -* `waiting s consumed leftover writes`: `decodeMsg?` reported - `truncated` on `leftover`. The caller reads more bytes and appends - them; it must not call `drive` again without new bytes. -* `running s consumed leftover writes`: the fuel ran out after a - complete frame. The caller calls `drive` again with `leftover`; it - must not read. -/ -inductive DriveResult where - | selected (p : Libp2p.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)) - deriving Repr, DecidableEq - -namespace DriveResult - -/-- The frames the run consumed, as their encoded bytes. -/ -@[simp] def consumed : DriveResult → List Nat - | .selected _ c _ _ => c - | .waiting _ c _ _ => c - | .running _ c _ _ => c - -/-- The bytes the run did not consume. -/ -@[simp] def leftover : DriveResult → List Nat - | .selected _ _ l _ => l - | .waiting _ _ l _ => l - | .running _ _ l _ => l - -end DriveResult - -/-- The `Action.write` payloads of an action list, in order. -/ -def writesOf (actions : List Action) : List (List Nat) := - actions.filterMap fun - | .write bs => some bs - | .select .. => none - -/-- The protocol an action list selects, if it selects one. -/ -def selectOf : List Action → Option Libp2p.Core.ProtocolId - | [] => none - | .write _ :: rest => selectOf rest - | .select p _ :: _ => some p - -/-- One fuel unit consumes at most one complete frame. The -accumulators keep the consumed bytes and the writes of the run. -/ -private def driveAux : Nat → State → List Nat → List Nat → List (List Nat) → - Except Error DriveResult - | 0, s, input, consumed, writes => .ok (.running s consumed input writes) - | fuel + 1, s, input, consumed, writes => - match decodeMsg? input with - | .error .truncated => .ok (.waiting s consumed input writes) - | .error .malformed => .error (.decode .malformed) - | .ok (m, rest) => - match step { s with buffer := [] } (.bytes input) with - | .error e => .error e - | .ok (s', actions) => - match selectOf actions with - | some p => - .ok (.selected p (consumed ++ encodeMsg m) rest - (writes ++ writesOf actions)) - | none => - driveAux fuel s' rest (consumed ++ encodeMsg m) - (writes ++ writesOf actions) - -/-- Drive the pure core over a byte cursor. `s.buffer` is -unused: pass every unconsumed byte in `input`, and read the -`leftover` field of the result as authoritative. One fuel unit -consumes at most one frame. -/ -def drive (fuel : Nat) (s : State) (input : List Nat) : Except Error DriveResult := - driveAux fuel s input [] [] - -/-- The initiator's post-propose state and its one coalesced write. -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 Libp2p.Core.ProtocolId) : - Except Error (State × List (List Nat)) := - match ids with - | [] => .error .negotiationFailed - | p :: _ => - if ids.any (fun q => !fitsText q.toString) then .error .negotiationFailed - else - .ok ({ role := .initiator, supported := [], proposals := ids, buffer := [], - phase := .negotiating }, - [encodeMsg header ++ encodeText p.toString]) - -/-- The responder's start: validate the offered list, then send the header -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 Libp2p.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 - else - .ok ({ role := .responder, supported := ids, proposals := [], buffer := [], - phase := .negotiating }, - [encodeMsg header]) - -/-! ## The error mappings -/ - -/-- The rendered form of a decode error. `Bytes.DecodeError` carries no -`ToString` instance, so the mapping renders it here. -/ -def renderDecodeError : Bytes.DecodeError → String - | .truncated => "truncated" - | .malformed => "malformed" - -/-- Contract 8's one mapping point: every negotiation error becomes -the `protocol` arm, with the detail rendered. -/ -def mapNegotiateError : Error → Libp2p.Core.Error - | .decode e => .protocol ("multistream decode: " ++ renderDecodeError e) - | .negotiationFailed => .protocol "multistream negotiation failed" - -/-- The identity gate. `none` is the listen path, which accepts any -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 Libp2p.Core.Error Unit := - match expected with - | none => .ok () - | some e => - if e = remote then .ok () - else .error (.authentication "remote peer id differs from the expected peer id") - -/-- The race answer flattened. `Conc.withinDeadline` constructs -`.error .deadlineExpired`; the `.closed` arm is required by the match -and is unreachable from `withinDeadline`. -/ -def settleUpgrade {α : Type} : - Except Conc.Error (Except Libp2p.Core.Error α) → Except Libp2p.Core.Error α - | .ok (.ok a) => .ok a - | .ok (.error e) => .error e - | .error .deadlineExpired => .error (.timeout "upgrade deadline expired") - | .error .closed => .error (.closed "upgrade deadline select closed") - -/-- The answer of one negotiation stage: the selected id and the bytes -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 : Libp2p.Core.ProtocolId - leftover : ByteArray - -/-! ## The driver theorems -/ - -/-- The accumulator invariant behind the conservation law: the bytes -fed in equal the bytes consumed plus the final leftover, for every -arm of the result. The proof inducts on the fuel; -`decodeMsgEncodeDecode` reassociates each consumed frame. -/ -private theorem driveAux_conservation (fuel : Nat) : - ∀ (s : State) (input consumed : List Nat) (writes : List (List Nat)) - (r : DriveResult), - driveAux fuel s input consumed writes = .ok r → - consumed ++ input = r.consumed ++ r.leftover := by - induction fuel with - | zero => - intro s input consumed writes r h - simp only [driveAux, Except.ok.injEq] at h - subst h - simp - | succ fuel ih => - intro s input consumed writes r h - simp only [driveAux] at h - split at h - · simp only [Except.ok.injEq] at h - subst h - simp - · simp at h - · rename_i m rest hdec - split at h - · rename_i e - simp at h - · rename_i s' actions hstep - split at h - · rename_i p - simp only [Except.ok.injEq] at h - subst h - have hbs := decodeMsgEncodeDecode input m rest hdec - rw [← hbs] - simp [List.append_assoc] - · have hrec := ih s' rest (consumed ++ encodeMsg m) - (writes ++ writesOf actions) r h - have hbs := decodeMsgEncodeDecode input m rest hdec - rw [← hbs, ← List.append_assoc] - exact hrec - -/-- Every byte fed to the driver is consumed or left over. -/ -theorem driveConservation {fuel : Nat} {s : State} {input : List Nat} {r : DriveResult} - (h : drive fuel s input = .ok r) : input = r.consumed ++ r.leftover := by - have h' := driveAux_conservation fuel s input [] [] r h - simpa using h' - -/-- 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 : Libp2p.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 - simpa using driveConservation h - -/-- The truncated arm: every byte the run saw sits in the -consumed frames or in the waiting buffer, so the shell loses no byte -when it reads the next chunk. -/ -theorem driveWaitingConservation {fuel : Nat} {s s' : State} {input : List Nat} - {consumed leftover : List Nat} {writes : List (List Nat)} - (h : drive fuel s input = .ok (.waiting s' consumed leftover writes)) : - input = consumed ++ leftover := by - simpa using driveConservation h - -/-- The accumulator prefix invariant: a run appends the frames it -consumes to the accumulator it received. -/ -private theorem driveAux_consumed_prefix (fuel : Nat) : - ∀ (s : State) (input consumed : List Nat) (writes : List (List Nat)) - (r : DriveResult), - driveAux fuel s input consumed writes = .ok r → - ∃ tail : List Nat, r.consumed = consumed ++ tail := by - induction fuel with - | zero => - intro s input consumed writes r h - simp only [driveAux, Except.ok.injEq] at h - subst h - exact ⟨[], by simp⟩ - | succ fuel ih => - intro s input consumed writes r h - simp only [driveAux] at h - split at h - · simp only [Except.ok.injEq] at h - subst h - exact ⟨[], by simp⟩ - · simp at h - · rename_i m rest hdec - split at h - · rename_i e - simp at h - · rename_i s' actions hstep - split at h - · rename_i p - simp only [Except.ok.injEq] at h - subst h - exact ⟨encodeMsg m, rfl⟩ - · obtain ⟨tail, htail⟩ := - ih s' rest (consumed ++ encodeMsg m) (writes ++ writesOf actions) r h - exact ⟨encodeMsg m ++ tail, by rw [htail, List.append_assoc]⟩ - -/-- A frame the shell writes through `encodeMsg` decodes and appears -at the head of the consumed bytes. -/ -theorem driveConsumedHead {fuel : Nat} {s : State} {m : Msg} {rest : List Nat} - {r : DriveResult} - (h : drive (fuel + 1) s (encodeMsg m ++ rest) = .ok r) : - ∃ tail : List Nat, r.consumed = encodeMsg m ++ tail := by - have h' : driveAux (fuel + 1) s (encodeMsg m ++ rest) [] [] = .ok r := h - simp only [driveAux, encodeMsg, decodeMsgSuffix] at h' - split at h' - · rename_i e - simp at h' - · rename_i s' actions hstep - split at h' - · rename_i p - simp only [Except.ok.injEq] at h' - subst h' - exact ⟨[], by simp [encodeMsg]⟩ - · obtain ⟨tail, htail⟩ := - driveAux_consumed_prefix fuel s' rest ([] ++ encodeMsg m) (writesOf actions) r h' - exact ⟨tail, by simpa [encodeMsg, List.append_assoc] using htail⟩ - -/-- Two stages compose: bytes in equal the consumed bytes of both -stages plus the final leftover. The reusable form of the leftover -hand-over (contract 5). -/ -theorem handoverCompose {ε α β : Type} - {f : List Nat → Except ε (α × List Nat)} - {g : List Nat → Except ε (β × List Nat)} - {c₁ : α → List Nat} {c₂ : β → List Nat} - {bs₁ bs₂ l₁ l₂ : List Nat} {a₁ : α} {a₂ : β} - (law₁ : ∀ x a r, f x = .ok (a, r) → x = c₁ a ++ r) - (law₂ : ∀ x a r, g x = .ok (a, r) → x = c₂ a ++ r) - (h₁ : f bs₁ = .ok (a₁, l₁)) - (h₂ : g (l₁ ++ bs₂) = .ok (a₂, l₂)) : - bs₁ ++ bs₂ = c₁ a₁ ++ c₂ a₂ ++ l₂ := by - rw [law₁ bs₁ a₁ l₁ h₁, List.append_assoc, law₂ (l₁ ++ bs₂) a₂ l₂ h₂] - simp only [List.append_assoc] - -/-- The pure form of one hand-over: when a second drive starts from -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₂ : Libp2p.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₂)) : - input₁ ++ input₂ = c₁ ++ c₂ ++ l₂ := by - have h1 := driveSelectedConservation h₁ - have h2 := driveSelectedConservation h₂ - rw [h1, List.append_assoc, h2] - simp only [List.append_assoc] - -/-- 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 : Libp2p.Core.ProtocolId} - (hfits : fitsText p.toString = true) : - initiatorStart [p] = - (step { role := .initiator, supported := [], proposals := [], buffer := [], - phase := .headerPending } (.propose p)).map - (fun sa => (sa.1, writesOf sa.2)) := by - have hany : ([p].any (fun q => !fitsText q.toString)) = false := by - simp [List.any, hfits] - simp only [initiatorStart, hany] - rfl - -/-- An empty ordered list is a protocol error before any byte is -written. -/ -theorem initiatorStartNil : initiatorStart [] = .error .negotiationFailed := rfl - -/-- The one mapping point of contract 8: every `Negotiate.Error` -becomes the `protocol` arm, with the detail rendered. -/ -theorem mapNegotiateErrorSpec {e : Bytes.DecodeError} : - mapNegotiateError (.decode e) = - .protocol ("multistream decode: " ++ renderDecodeError e) ∧ - mapNegotiateError .negotiationFailed = - .protocol "multistream negotiation failed" := by - simp [mapNegotiateError] - -/-- A differing derived id is authentication, before any muxer -byte moves. -/ -theorem checkIdentityReject {expected remote : Libp2p.Identity.PeerId} - (h : expected ≠ remote) : - checkIdentity (some expected) remote = - .error (.authentication "remote peer id differs from the expected peer id") := by - simp [checkIdentity, h] - -/-- The dial to the expected peer passes. -/ -theorem checkIdentityAccept {e : Libp2p.Identity.PeerId} : - checkIdentity (some e) e = .ok () := by - simp [checkIdentity] - -/-- The listen path accepts any peer. -/ -theorem checkIdentityNone {r : Libp2p.Identity.PeerId} : - checkIdentity none r = .ok () := rfl - -/-- 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 : Libp2p.Core.Error} {a : α} : - settleUpgrade (α := α) (.error .deadlineExpired) = - .error (.timeout "upgrade deadline expired") ∧ - settleUpgrade (α := α) (.error .closed) = - .error (.closed "upgrade deadline select closed") ∧ - settleUpgrade (α := α) (.ok (.error e)) = .error e ∧ - settleUpgrade (.ok (.ok a)) = .ok a := by - simp [settleUpgrade] - -/-! ## The IO shell -/ - -/-- Write one frame, and turn a fault of the connection into the -`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 Libp2p.Core.Error Conc.Async Unit := do - let ok ← (try - conn.write b - pure true - catch _ => pure false : Conc.Async Bool) - if ok then pure () else throw (.closed "connection write failed during the upgrade") - -/-- 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 Libp2p.Core.Error Conc.Async Unit := do - for w in ws do - writeFrame conn (Bytes.ofNatList w) - -/-- The negotiation loop. It parks on `reader.read` only when `drive` -reports `waiting`; a `running` answer costs no read, because the driver -has not yet tried to decode `leftover`. `reader.read` returns the next -reader, and the loop keeps it for the next read. The read parks for as -long as the peer stays silent, so no measure bounds the loop (root -§3.3). The `repeat` form keeps the definition free of a `partial` -marker, like `Conc.TaskSet.joinAll`. -/ -private def negotiateLoop (reader : Streams.BufReader) - (conn : Streams.Connection) (s : State) (input : List Nat) : - ExceptT Libp2p.Core.Error Conc.Async StageResult := do - let mut s := s - let mut input := input - let mut reader := reader - repeat - match drive 1 s input with - | .error e => throw (mapNegotiateError e) - | .ok (.selected p _ leftover writes) => do - sendWrites conn writes - return { proto := p, leftover := Bytes.ofNatList leftover } - | .ok (.waiting s' _ leftover writes) => do - sendWrites conn writes - match ← reader.read with - | none => throw (.closed "multistream negotiation ended before a selection") - | some (chunk, reader') => - s := s' - input := leftover ++ Bytes.toNatList chunk - reader := reader' - | .ok (.running s' _ leftover writes) => do - sendWrites conn writes - s := s' - input := leftover - -- Every arm above returns or loops, so the `repeat` never falls - -- through. The tail gives the `do` block its result type without an - -- `Inhabited`. - throw (.closed "the negotiation loop ended without an answer") - -/-- One negotiation stage. Both roles write before the loop: the -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 : Libp2p.Core.Role) (reader : Streams.BufReader) - (conn : Streams.Connection) (seed : ByteArray) - (ids : List Libp2p.Core.ProtocolId) : - ExceptT Libp2p.Core.Error Conc.Async StageResult := do - match role with - | .initiator => - match initiatorStart ids with - | .error e => throw (mapNegotiateError e) - | .ok (s, first) => do - sendWrites conn first - negotiateLoop reader conn s (Bytes.toNatList seed) - | .responder => - match responderStart ids with - | .error e => throw (mapNegotiateError e) - | .ok (s, first) => do - sendWrites conn first - negotiateLoop reader conn s (Bytes.toNatList seed) - -/-- An upgraded session and its secure connection completion. -/ -structure Upgraded where - session : Libp2p.Core.MuxSession - remotePeer : Libp2p.Identity.PeerId - join : ExceptT Libp2p.Core.Error Conc.Async Unit - -/-- The result of the post-handshake admission checkpoint. -/ -inductive UpgradeResult (ρ : Type) where - | upgraded (value : Upgraded) - | refused (reason : ρ) - -private def upgradeCore {ρ : Type} (role : Libp2p.Core.Role) (conn : Streams.Connection) - (leftover : ByteArray) (expected : Option Libp2p.Identity.PeerId) - (admit : Libp2p.Identity.PeerId → BaseIO (Option ρ)) - (secs : List Libp2p.Core.SecurityProtocol) (muxers : List Libp2p.Core.Muxer) : - Conc.Async (Except Libp2p.Core.Error (UpgradeResult ρ)) := do - let reader := Streams.BufReader.new conn - match ← negotiate role reader conn leftover (secs.map (·.id)) with - | .error e => return .error e - | .ok stage => - match secs.find? (fun s => decide (s.id = stage.proto)) with - | none => return .error (.protocol "selected security protocol is not configured") - | some sec => - match ← sec.handshake role conn stage.leftover with - | .error e => return .error e - | .ok sc => - match checkIdentity expected sc.remotePeer with - | .error e => - sc.toConnection.closeQuietly - discard sc.join.run - return .error e - | .ok () => - if let some reason ← (admit sc.remotePeer : BaseIO (Option ρ)) then - sc.toConnection.closeQuietly - discard sc.join.run - return .ok (.refused reason) - let muxReader := Streams.BufReader.new sc.toConnection - match ← negotiate role muxReader sc.toConnection ByteArray.empty (muxers.map (·.id)) with - | .error e => - sc.toConnection.closeQuietly - discard sc.join.run - return .error e - | .ok stage2 => - match muxers.find? (fun m => decide (m.id = stage2.proto)) with - | none => - sc.toConnection.closeQuietly - discard sc.join.run - return .error (.protocol "selected muxer is not configured") - | some mux => - match ← mux.«open» role sc.toConnection stage2.leftover with - | .error e => - sc.toConnection.closeQuietly - discard sc.join.run - return .error e - | .ok session => - let join : ExceptT Libp2p.Core.Error Conc.Async Unit := ExceptT.mk do - let muxResult ← session.join.run - let secureResult ← sc.join.run - return match muxResult, secureResult with - | .error e, _ => .error e - | _, .error e => .error e - | .ok (), .ok () => .ok () - return .ok (.upgraded { session, remotePeer := sc.remotePeer, join }) - -/-- Whether the deadline boundary already closed the connection. -`withinDeadline` returns an error value only on expiry, after the hook -ran. -/ -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 {ρ : Type} (r : Except Libp2p.Core.Error (UpgradeResult ρ)) : BaseIO Unit := - match r with - | .ok (.upgraded value) => discard value.session.close.toBaseIO - | _ => pure () - -/-- The upgrade under one `Conc.withinDeadline`. The expiry closes -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 upgradeAdmit {ρ : Type} (clock : Conc.Clock) (role : Libp2p.Core.Role) - (conn : Streams.Connection) (leftover : ByteArray) - (expected : Option Libp2p.Identity.PeerId) - (admit : Libp2p.Identity.PeerId → BaseIO (Option ρ)) - (secs : List Libp2p.Core.SecurityProtocol) (muxers : List Libp2p.Core.Muxer) : - ExceptT Libp2p.Core.Error Conc.Async (UpgradeResult ρ) := do - let answer ← Conc.withinDeadline clock Streams.unauthDeadlineMs - (Streams.Connection.closeQuietly conn) - (upgradeCore role conn leftover expected admit secs muxers) - releaseLate - match settleUpgrade answer with - | .ok pair => return pair - | .error e => do - -- An error from the boundary means the expiry hook closed the - -- connection. A failure inside the work leaves it open. - if boundaryClosed answer then throw e - else do - Streams.Connection.closeQuietly conn - throw e - -/-- Upgrade with a clock and admit every authenticated peer. -/ -def upgradeWith (clock : Conc.Clock) (role : Libp2p.Core.Role) - (conn : Streams.Connection) (leftover : ByteArray) - (expected : Option Libp2p.Identity.PeerId) - (secs : List Libp2p.Core.SecurityProtocol) (muxers : List Libp2p.Core.Muxer) : - ExceptT Libp2p.Core.Error Conc.Async (Libp2p.Core.MuxSession × Libp2p.Identity.PeerId) := do - match ← upgradeAdmit clock role conn leftover expected (fun _ => pure (none : Option Empty)) secs muxers with - | .upgraded value => return (value.session, value.remotePeer) - | .refused reason => nomatch reason - -/-- 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 : Libp2p.Core.Role) (conn : Streams.Connection) - (leftover : ByteArray) (expected : Option Libp2p.Identity.PeerId) - (secs : List Libp2p.Core.SecurityProtocol) (muxers : List Libp2p.Core.Muxer) : - ExceptT Libp2p.Core.Error Conc.Async (Libp2p.Core.MuxSession × Libp2p.Identity.PeerId) := - upgradeWith Conc.Clock.system role conn leftover expected secs muxers - -/-- Negotiate a protocol on a muxed stream and retain any extra bytes. -/ -def negotiateStream (role : Libp2p.Core.Role) (stream : Streams.Stream) - (ids : List Libp2p.Core.ProtocolId) : - ExceptT Libp2p.Core.Error Conc.Async (Libp2p.Core.ProtocolId × Streams.Stream) := do - let (initial, writes) ← match role with - | .initiator => (initiatorStart ids).mapError mapNegotiateError - | .responder => (responderStart ids).mapError mapNegotiateError - let mut state := initial - let mut input : List Nat := [] - for bytes in writes do - if let .error e ← stream.write (Bytes.ofNatList bytes) then - throw (.closed s!"stream negotiation write failed: {repr e}") - repeat - match drive 1 state input with - | .error e => throw (mapNegotiateError e) - | .ok result => - let (next, rest, writes, selected) := match result with - | .selected p _ rest writes => (state, rest, writes, some p) - | .waiting s _ rest writes => (s, rest, writes, none) - | .running s _ rest writes => (s, rest, writes, none) - for bytes in writes do - if let .error e ← stream.write (Bytes.ofNatList bytes) then - throw (.closed s!"stream negotiation write failed: {repr e}") - if let some p := selected then - let s ← Streams.Stream.prependBytes stream (Bytes.ofNatList rest) - return (p, s) - state := next - input := rest - if result matches .waiting .. then - match ← stream.read with - | .error e => throw (.closed s!"stream negotiation read failed: {repr e}") - | .ok none => throw (.closed "stream ended during negotiation") - | .ok (some bytes) => input := input ++ Bytes.toNatList bytes - throw (.closed "stream negotiation ended without a selection") - -end Libp2p.Negotiate.Legacy \ No newline at end of file diff --git a/packages/libp2p/protocols/Libp2p/Protocols/Constants.lean b/packages/libp2p/protocols/Libp2p/Protocols/Constants.lean index 877b11f8..92069cdc 100644 --- a/packages/libp2p/protocols/Libp2p/Protocols/Constants.lean +++ b/packages/libp2p/protocols/Libp2p/Protocols/Constants.lean @@ -1,5 +1,4 @@ import Libp2p.Core.ProtocolId -import Libp2p.Protocols.Mock.Core /-! # Protocol constants @@ -41,13 +40,13 @@ def floodsubId : Libp2p.Core.ProtocolId := ⟨"/floodsub/1.0.0"⟩ def rpcCap : Nat := 1048576 /-- The identify protocol id, `/ipfs/id/1.0.0`. -/ -def identifyId : Mock.Core.ProtocolId := ⟨"/ipfs/id/1.0.0"⟩ +def identifyId : Libp2p.Core.ProtocolId := ⟨"/ipfs/id/1.0.0"⟩ /-- The identify push protocol id, `/ipfs/id/push/1.0.0`. -/ -def identifyPushId : Mock.Core.ProtocolId := ⟨"/ipfs/id/push/1.0.0"⟩ +def identifyPushId : Libp2p.Core.ProtocolId := ⟨"/ipfs/id/push/1.0.0"⟩ /-- The ping protocol id, `/ipfs/ping/1.0.0`. -/ -def pingId : Mock.Core.ProtocolId := ⟨"/ipfs/ping/1.0.0"⟩ +def pingId : Libp2p.Core.ProtocolId := ⟨"/ipfs/ping/1.0.0"⟩ /-- The identify message cap, inherited from the spike: 65536 bytes. -/ def identifyCap : Nat := 65536 @@ -58,8 +57,6 @@ def pingSize : Nat := 32 /-- The protocol version the responder writes, the spike's constant. -/ def identifyProtocolVersion : String := "/ipfs/1.0.0" --- Req/resp takes its ids from `libp2p/core`. The identify and ping ids --- above stay on the mock until their swap (issue #55). open Libp2p.Core (ProtocolId) /-! ## Req/resp: the protocol id -/ diff --git a/packages/libp2p/protocols/Libp2p/Protocols/Identify.lean b/packages/libp2p/protocols/Libp2p/Protocols/Identify.lean index 30548756..1c488412 100644 --- a/packages/libp2p/protocols/Libp2p/Protocols/Identify.lean +++ b/packages/libp2p/protocols/Libp2p/Protocols/Identify.lean @@ -6,8 +6,10 @@ import Streams.Framing import Streams.Stream import Multiformats.Multiaddr.Binary import Libp2p.Protocols.Identity -import Libp2p.Protocols.Mock.Host +import Libp2p.Core +import Libp2p.Host import Libp2p.Protocols.Constants +import Libp2p.Protocols.StreamError /-! # Identify @@ -29,19 +31,25 @@ UTF-8 entries are dropped, as the Proto accessors already do. The strings read back through `Bytes.toString?`. +The handlers read the connection from their `StreamContext`. The push +handler checks the pushed key against `remotePeer`, and it stores the +addresses under that peer in the host's peerstore. The responder writes +`remoteAddr` as the observed address. go-libp2p reads both from +`s.Conn()` (`vendor/go-libp2p/p2p/protocol/identify/id.go`). + The private read loop `readFrameFrom` is a `partial def`: a silent peer never ends the loop, and the deadline of `client` or `push` ends -it. `client` and `push` read one frame per stream and drop the bytes -after it. Go merges chunked identify messages; this client reads one. -The read rejects a zero-length frame, the spike's rule. +it. On expiry, the reset runs in a `TaskSet` that the call owns and +joins after the race (PRINCIPLES 3.2). `client` and `push` read one +frame per stream and drop the bytes after it. Go merges chunked +identify messages; this client reads one. The read rejects a +zero-length frame, the spike's rule. -/ set_option autoImplicit false namespace Libp2p.Protocols -open Mock - /-- One identify response. The field numbers are the ones of the go-libp2p v0.50.0 identify protobuf. -/ structure Identify where @@ -56,12 +64,11 @@ structure Identify where namespace Identify - /-- The identify protocol id. -/ -def protocolId : Mock.Core.ProtocolId := Constants.identifyId +def protocolId : Libp2p.Core.ProtocolId := Constants.identifyId /-- The identify push protocol id. -/ -def pushId : Mock.Core.ProtocolId := Constants.identifyPushId +def pushId : Libp2p.Core.ProtocolId := Constants.identifyPushId /-- The wire view: one entry per present singular field and per element of a repeated field, in the ascending order 1, 2, 3, 4, 5, 6, @@ -459,64 +466,70 @@ private partial def readFrameFrom (s : Streams.Stream) (buf : List Nat) : else return .error (.badMessage (.framing .truncated)) | .ok (some chunk) => readFrameFrom s (buf ++ Bytes.toNatList chunk) -/-- One frame from the stream, over the private loop. -/ -private def readFrame (s : Streams.Stream) : - Conc.Async (Except Error (Option (List Nat))) := - readFrameFrom s [] - -/-- `withinDeadline` needs a `BaseIO` expiry. The stream's `close` is -the write half-close, so it does not wake a parked `read`. `reset` stops -both directions, so it wakes the read. The body starts the reset with -`asTask`, as `Conc.Wrap.spawn` does. Nothing joins this task and the -code ignores its result, an exception to §4.1 rule 2. -/ -private def resetQuietly (s : Streams.Stream) : BaseIO Unit := - discard (s.reset.asTask.toBaseIO) +/-- One frame from the stream under the deadline. `withinDeadline` +takes a `BaseIO` expiry, and `Stream.reset` is `Async`, so the expiry +spawns the reset into a `TaskSet` that this call owns. The call joins +it after the race (the module doc). The stream's `close` is the write +half-close and does not wake a parked `read`. `reset` stops both +directions, so it ends the parked read. -/ +private def readFrame (s : Streams.Stream) (clock : Conc.Clock) (timeoutMs : Nat) : + Conc.Async (Except Error (Option (List Nat))) := do + let owner ← Conc.TaskSet.new + let r ← Conc.withinDeadline clock timeoutMs (owner.spawn s.reset) (readFrameFrom s []) + owner.joinAll + match r with + | .error .deadlineExpired => return .error .timeout + | .error .closed => return .error (.stream .closed) + | .ok a => return a /-- Read one response under the cap and the deadline, then validate it. `.ok none` means that the stream ended before any byte arrived. -/ def client (s : Streams.Stream) (clock : Conc.Clock) (timeoutMs : Nat) (expected : Option Libp2p.Identity.PeerId) : Conc.Async (Except Error (Option (Identify × Libp2p.Identity.PeerId))) := do - match ← Conc.withinDeadline clock timeoutMs (resetQuietly s) (readFrame s) with - | .error .deadlineExpired => return .error .timeout - | .error .closed => return .error (.stream .closed) - | .ok (.error e) => return .error e - | .ok (.ok none) => return .ok none - | .ok (.ok (some payload)) => return (some <$> validate payload expected) + match ← readFrame s clock timeoutMs with + | .error e => return .error e + | .ok none => return .ok none + | .ok (some payload) => return (some <$> validate payload expected) /-- The one map from this protocol's error into the coarse core error. `pushHandler` and `writeRecord` call it at the seam. -/ -def mapIdentifyError : Error → Mock.Core.Error - | .stream e => Mock.Core.mapStreamError e +def mapIdentifyError : Error → Libp2p.Core.Error + | .stream e => mapStreamError e | .timeout => .timeout "identify: the deadline expired" | .emptyFrame => .protocol "identify: a zero-length frame" | e => .protocol (toString (repr e)) -/-- Handle one pushed message: validate it, then update the peerstore. -An empty read leaves the peerstore unchanged. This is a delta from go, -whose `consumeMessage` runs on the empty message and clears the peer's +/-- The listen addresses of a validated message as multiaddrs. +`validate` already decoded each one, so `filterMap` drops none. -/ +private def listenMultiaddrs (m : Identify) : List Multiformats.Multiaddr := + m.listenAddrs.filterMap fun a => (Multiformats.Multiaddr.ofBytes? a).toOption + +/-- Handle one pushed message from `peer`: validate it against `peer`, +then add its listen addresses to the host's peerstore. An empty read +leaves the peerstore unchanged. This is a delta from go, whose +`consumeMessage` runs on the empty message and clears the peer's protocols. -/ -def push (store : Mock.Host.Peerstore) (expected : Libp2p.Identity.PeerId) +def push (h : Libp2p.Host.Host) (peer : Libp2p.Identity.PeerId) (clock : Conc.Clock) (timeoutMs : Nat) (s : Streams.Stream) : Conc.Async (Except Error Unit) := do - match ← Conc.withinDeadline clock timeoutMs (resetQuietly s) (readFrame s) with - | .error .deadlineExpired => return .error .timeout - | .error .closed => return .error (.stream .closed) - | .ok (.error e) => return .error e - | .ok (.ok none) => return .ok () - | .ok (.ok (some payload)) => - match validate payload (some expected) with + match ← readFrame s clock timeoutMs with + | .error e => return .error e + | .ok none => return .ok () + | .ok (some payload) => + match validate payload (some peer) with | .error e => return .error e | .ok (m, pid) => - store.addAddrs pid m.listenAddrs + h.addAddrs pid (listenMultiaddrs m) return .ok () -/-- The push handler value. -/ -def pushHandler (store : Mock.Host.Peerstore) (expected : Libp2p.Identity.PeerId) - (clock : Conc.Clock) (timeoutMs : Nat) : Mock.Core.StreamHandler := +/-- The push handler value. Each stream checks the push against the +peer of its own connection, from the `StreamContext`. -/ +def pushHandler (h : Libp2p.Host.Host) (clock : Conc.Clock) (timeoutMs : Nat) : + Libp2p.Core.StreamHandler := { id := pushId, - handle := fun _ctx s => ExceptT.mk ((Except.mapError mapIdentifyError) <$> - push store expected clock timeoutMs s) } + handle := fun ctx s => ExceptT.mk ((Except.mapError mapIdentifyError) <$> + push h ctx.remotePeer clock timeoutMs s) } /-- Write one length-delimited message and half-close. The responder and the push sender share this body: both announce the same @@ -524,7 +537,7 @@ record, and only the protocol id of the stream differs. -/ private def writeRecord (key : Libp2p.Identity.PubKey) (addrs : List (List Nat)) (protocols : List String) (observed : Option (List Nat)) (agent : String) (spr : Option (List Nat)) (s : Streams.Stream) : - Conc.Async (Except Mock.Core.Error Unit) := do + Conc.Async (Except Libp2p.Core.Error Unit) := do match respond? key addrs protocols observed agent spr with | .error e => return .error (mapIdentifyError e) | .ok msg => @@ -533,7 +546,7 @@ private def writeRecord (key : Libp2p.Identity.PubKey) (addrs : List (List Nat)) | none => return .error (.protocol "the identify record exceeds the cap") | some frame => match ← s.write frame with - | .error e => return .error (Mock.Core.mapStreamError e) + | .error e => return .error (mapStreamError e) | .ok () => discard s.close return .ok () @@ -543,7 +556,7 @@ half-close. -/ def respondTo (key : Libp2p.Identity.PubKey) (addrs : List (List Nat)) (protocols : List String) (observed : Option (List Nat)) (agent : String) (spr : Option (List Nat) := none) (s : Streams.Stream) : - Conc.Async (Except Mock.Core.Error Unit) := + Conc.Async (Except Libp2p.Core.Error Unit) := writeRecord key addrs protocols observed agent spr s /-- The push sender: announce this peer's record on the stream that the @@ -552,31 +565,32 @@ host opened under `pushId`, then half-close. The host calls the sender after the local address set or the local protocol set changes. Go's identify service skips a push when the snapshot did not change, merges pending pushes into one round, and -skips a connection that already carries the current record (the -spike's `vendor/go-libp2p/p2p/protocol/identify/id.go`, the `loop` and +skips a connection that already carries the current record +(`vendor/go-libp2p/p2p/protocol/identify/id.go`, the `loop` and `sendPushes` functions). This package sends one record per call and starts no timer. -/ def pushTo (key : Libp2p.Identity.PubKey) (addrs : List (List Nat)) (protocols : List String) (observed : Option (List Nat)) (agent : String) (spr : Option (List Nat) := none) (s : Streams.Stream) : - Conc.Async (Except Mock.Core.Error Unit) := + Conc.Async (Except Libp2p.Core.Error Unit) := writeRecord key addrs protocols observed agent spr s -/-- The responder handler value. -/ +/-- The responder handler value. The observed address of each answer +is the remote address of the stream's connection, from the +`StreamContext`. -/ def respondHandler (key : Libp2p.Identity.PubKey) (addrs : List (List Nat)) - (protocols : List String) (observed : Option (List Nat)) (agent : String) - (spr : Option (List Nat) := none) : Mock.Core.StreamHandler := + (protocols : List String) (agent : String) + (spr : Option (List Nat) := none) : Libp2p.Core.StreamHandler := { id := protocolId, - handle := fun _ctx s => respondTo key addrs protocols observed agent spr s } + handle := fun ctx s => ExceptT.mk <| + respondTo key addrs protocols (some ctx.remoteAddr.toBytes) agent spr s } /-! ## The client-core theorems `clientCoreFrame` pins the frame that `clientCore` validates. `clientCoreOverCap` pins the cap check before the body. `clientCoreEmptyFrame` pins the zero-length rule. Each consumes a law of -`Streams.Framing`, and the laws rest on no mock axiom: the base -replaced the streams mocks with the real encoders. None takes a result -of this package's mocks as a premise. -/ +`Streams.Framing`. -/ /-- The frame step reads a whole frame back from its encoding, with any rest after it. -/ diff --git a/packages/libp2p/protocols/Libp2p/Protocols/Mock/Core.lean b/packages/libp2p/protocols/Libp2p/Protocols/Mock/Core.lean deleted file mode 100644 index 0cd8b65c..00000000 --- a/packages/libp2p/protocols/Libp2p/Protocols/Mock/Core.lean +++ /dev/null @@ -1,53 +0,0 @@ -import Std -import Conc -import Streams -import Libp2p.Identity - -/-! -# Core seam mock - -`Libp2p.Core` (issue #15, PR #64) is not merged. This mock declares -the frozen seam shapes from `packages/libp2p/core/docs/ARCHITECTURE.md`: -`ProtocolId`, the coarse `Error`, `StreamContext`, and `StreamHandler`. -The real core package replaces this module at integration. --/ - -set_option autoImplicit false - -namespace Libp2p.Protocols.Mock.Core - -/-- A peer-defined protocol id, an open set of strings. The code -compares `ProtocolId` values only. -/ -structure ProtocolId where - toString : String - deriving DecidableEq, Hashable - -/-- The coarse error of the core seam, with the rendered inner error. -/ -inductive Error where - | protocol (rendered : String) - | authentication (rendered : String) - | timeout (rendered : String) - | closed (rendered : String) - deriving DecidableEq, BEq, Repr - -/-- What the host knows about the connection under a served stream: -the proved peer id and the peer's transport address. -/ -structure StreamContext where - remotePeer : Libp2p.Identity.PeerId - remoteAddr : Multiformats.Multiaddr - -/-- The handler seam: the id it registers under, and the callback a -served stream reaches. -/ -structure StreamHandler where - id : ProtocolId - handle : StreamContext → Streams.Stream → ExceptT Error Conc.Async Unit - -/-- One map from a stream error to the coarse error, shared by every -handler of this package. `closed` stays closed, `reset` is a protocol -fault, and `timeout` stays timeout. -/ -def mapStreamError : Streams.Error → Error - | .closed => .closed "the stream closed" - | .reset => .protocol "the peer reset the stream" - | .timeout => .timeout "the stream deadline expired" - -end Libp2p.Protocols.Mock.Core diff --git a/packages/libp2p/protocols/Libp2p/Protocols/Mock/Host.lean b/packages/libp2p/protocols/Libp2p/Protocols/Mock/Host.lean deleted file mode 100644 index 42ab3615..00000000 --- a/packages/libp2p/protocols/Libp2p/Protocols/Mock/Host.lean +++ /dev/null @@ -1,47 +0,0 @@ -import Std -import Conc -import Libp2p.Identity - -/-! -# Host peerstore mock - -`Libp2p.Host` (issue #19) is not merged. This mock declares the -peerstore surface that the identify push handler updates, from -`packages/libp2p/host/docs/ARCHITECTURE.md`: `addAddrs`, deduplicated -at add, and `addrsOf`. The host doc freezes the names and the dedup -rule, and it leaves the signatures open. This mock fixes minimal -signatures. The real host package replaces this module at integration. --/ - -set_option autoImplicit false - -namespace Libp2p.Protocols.Mock.Host - -open Libp2p.Identity - -/-- The peerstore seam the push handler updates: addresses by peer, -deduplicated at add. -/ -structure Peerstore where - /-- Store the addresses of one peer, deduplicated at add. -/ - addAddrs : PeerId → List (List Nat) → IO Unit - /-- The stored addresses of one peer. -/ - addrsOf : PeerId → IO (List (List Nat)) - -/-- The executable in-memory double. Each call makes a fresh table: -bind the action once, and pass the resulting value to both the handler -and `addrsOf`. A second add of the same addresses grows nothing. The -table changes through `OnceRef.update`, one atomic step per add -(ARCHITECTURE §4.1, rule 3). -/ -opaque inMemory : IO Peerstore := do - let table ← Conc.OnceRef.new ([] : List (PeerId × List (List Nat))) - let addAddrs : PeerId → List (List Nat) → IO Unit := fun p addrs => - table.update fun cur => - let old := (cur.find? (fun e => decide (e.1 = p))).map (·.2) |>.getD [] - let merged := (old ++ addrs).eraseDups - (p, merged) :: cur.filter (fun e => !(decide (e.1 = p))) - let addrsOf : PeerId → IO (List (List Nat)) := fun p => do - let cur ← table.get - return (cur.find? (fun e => decide (e.1 = p))).map (·.2) |>.getD [] - return { addAddrs, addrsOf } - -end Libp2p.Protocols.Mock.Host diff --git a/packages/libp2p/protocols/Libp2p/Protocols/Mock/HostStream.lean b/packages/libp2p/protocols/Libp2p/Protocols/Mock/HostStream.lean deleted file mode 100644 index dc68a998..00000000 --- a/packages/libp2p/protocols/Libp2p/Protocols/Mock/HostStream.lean +++ /dev/null @@ -1,144 +0,0 @@ -import Conc -import Streams -import Libp2p.Core.Handler -import Libp2p.Core.Mux -import Libp2p.Protocols.StreamError - -/-! -# Host stream mock - -`Libp2p.Host` (W5.6) merged, but it still runs its upgrade through a -mock of `libp2p/negotiate` (issue #70), so no host opens a session yet. -The protocols docs have the req/resp client open its stream through -the host, with `newStream`, and serve through `setHandler` over the -registry of §3.10; go-libp2p's outbound call is `NewStream` -(`vendor/go-libp2p/p2p/host/basic/basic_host.go`, line 441). This -mock fixes minimal signatures for both sides over one muxer session of -the real `MuxSession` seam (RULES.md, "Working ahead of the tree"). - -## What it leaves out - -* Dialing: the mock holds one session, so `newStream` needs no peer. -* Negotiation (W5.5): the opener writes the first id it asks for, with a - one-byte length (an id of at most 255 bytes), and the listener looks - the id up in its registry. An id it does not serve resets the stream. - The bytes the listener read past the id go in front of the stream - with `Stream.prependBytes` (§4.7), as the negotiation hands them on. -* Failure reporting: a handler's failure goes to `failures`, the place - the host's `onFailure` will take. - -## Tasks and parks - -`serve` accepts in a loop and runs each stream in a task of a set it -owns, then joins the set when the session ends. The accept parks on the -session, which `close` ends. `close` closes the session, and `join` -waits for the serve loop and the session loop. - -## Integration - -Delete this module. Use the host's `newStream` for the peer, bound to -the peer id, in place of `Host.newStream`, and the host's `setHandler` -in place of `Host.setHandler`. --/ - -set_option autoImplicit false - -namespace Libp2p.Protocols.Mock.HostStream - -open Conc Streams -open Libp2p.Core (ProtocolId StreamContext StreamHandler MuxSession) - -/-- One end of a peer connection, with its handler registry. -/ -structure Host where - /-- The mock session to the peer. -/ - session : MuxSession - /-- The context every served stream of the session gets: the peer and - its address, which the real host takes from the upgrade. -/ - ctx : StreamContext - /-- The registry, by protocol id; changed only through `update`. -/ - handlers : OnceRef (List StreamHandler) - /-- The handler failures, newest first. -/ - failures : OnceRef (List Libp2p.Core.Error) - /-- The tasks of the served streams and the serve loop. -/ - owner : TaskSet - -/-- A host over a session to the peer that `ctx` names. -/ -def Host.new (session : MuxSession) (ctx : StreamContext) : BaseIO Host := do - return ⟨session, ctx, ← OnceRef.new [], ← OnceRef.new [], ← TaskSet.new⟩ - -/-- Store one handler under its id; a second store replaces the first. -/ -def Host.setHandler (h : Host) (sh : StreamHandler) : BaseIO Unit := - h.handlers.update fun hs => sh :: hs.filter (·.id != sh.id) - -/-- The header the opener writes: the id with a one-byte length. -/ -def idHeader (id : ProtocolId) : Option ByteArray := - let b := id.toString.toUTF8 - if b.size < 256 then some (ByteArray.mk #[b.size.toUInt8] ++ b) else none - -/-- Open a stream to the peer for the first id of `protocols`. -/ -def Host.newStream (h : Host) (protocols : List ProtocolId) : - Async (Except Libp2p.Core.Error (ProtocolId × Stream)) := do - let some id := protocols.head? | return .error (.protocol "newStream: no protocol id") - let some header := idHeader id | return .error (.protocol "newStream: an id over 255 bytes") - match ← (h.session.openStream id).run with - | .error e => return .error e - | .ok s => - match ← s.write header with - | .error e => s.reset; return .error (mapStreamError e) - | .ok () => return .ok (id, s) - -/-- Read the id header from `s`: the id and the bytes after it. `none` -when the stream ends or fails first. The read parks on the stream, which -the session close or a reset wakes; the loop is `partial` for the same -reason as every stream read loop. -/ -partial def readHeader (s : Stream) (buf : ByteArray) : Async (Option (String × ByteArray)) := do - if h : 0 < buf.size then - let len := (buf.get 0 h).toNat - if 1 + len ≤ buf.size then - return (String.fromUTF8? (buf.extract 1 (1 + len))).map fun id => - (id, buf.extract (1 + len) buf.size) - match ← s.read with - | .ok (some b) => readHeader s (buf ++ b) - | _ => return none - -/-- Serve one inbound stream through the registry. -/ -def serveStream (h : Host) (s : Stream) : Async Unit := do - let some (id, rest) ← readHeader s ByteArray.empty | s.reset - let hs ← (h.handlers.get : BaseIO _) - match hs.find? (·.id.toString == id) with - | none => s.reset - | some sh => - let s ← s.prependBytes rest - match ← (sh.handle h.ctx s).run with - | .ok () => pure () - | .error e => - h.failures.update (e :: ·) - s.reset - -/-- The serve loop: accept until the session ends, one task per stream. -`partial`: the peer may open streams forever; the session close ends the -accept with `none`. -/ -partial def serveLoop (h : Host) (streams : TaskSet) : Async Unit := do - -- Park: a new stream of the peer wakes it, and so does the close. - match ← h.session.accept with - | none => streams.joinAll - | some s => - streams.spawn (serveStream h s) - serveLoop h streams - -/-- Start serving inbound streams. -/ -def Host.serve (h : Host) : BaseIO Unit := do - let streams ← TaskSet.new - h.owner.spawn (serveLoop h streams) - -/-- Close the session. -/ -def Host.close (h : Host) : IO Unit := h.session.close - -/-- Wait for the serve loop, its streams, and the session loop. The -session of `Mock.Muxer.muxer` always joins with `.ok`, so the answer -goes unread. -/ -def Host.join (h : Host) : Async Unit := do - h.owner.joinAll - discard h.session.join.run - -end Libp2p.Protocols.Mock.HostStream diff --git a/packages/libp2p/protocols/Libp2p/Protocols/Mock/Muxer.lean b/packages/libp2p/protocols/Libp2p/Protocols/Mock/Muxer.lean deleted file mode 100644 index a451b431..00000000 --- a/packages/libp2p/protocols/Libp2p/Protocols/Mock/Muxer.lean +++ /dev/null @@ -1,222 +0,0 @@ -import Std.Data.HashMap -import Conc -import Streams -import Libp2p.Core.Mux - -/-! -# Muxer mock - -The muxer values of `libp2p/mux` took the real core seams while this -branch ran (PR #84, issue #77 closed), so the swap of this mock is due -now (issue #78). Until it lands, this module stands in with one value, -`muxer`, of the real `Muxer` seam of `libp2p/core`. It runs over any -`Connection`, so the req/resp suite runs over the sim transport -(PRINCIPLES 1.4; RULES.md, "Working ahead of the tree"). - -## The wire of the mock - -One frame shape, and nothing else: - -``` - -``` - -The kind is data (0), close (1), or reset (2). The 2-byte length caps a -frame at 65535 bytes, and the reader takes no more (§5.1). The dialer -numbers its streams odd and the listener even, so the two sides never -pick one id. The first frame of a new id from the peer opens the -stream, and `accept` hands it out. A close ends the peer's read -direction only (§5.3). A reset fails both sides, also after a close. -The end of the session fails every open stream with `.closed`. - -The mock enforces no flow control: the inboxes are unbounded, and the -yamux window of W5.4 is what bounds them in production. - -## Tasks and parks - -One reader task per session, in a `TaskSet` the session owns; `join` -joins it. The reader parks on `Connection.read`, which `close` wakes. -Writers take a one-token channel around each frame write, so two -streams never interleave the bytes of their frames; the token's park -wakes when the writer before it sends the token back. - -## Integration - -Delete this module, and use `Mux.test` or `Mux.yamux` where the suite -takes `muxer`. The suite needs no other change: it uses the seam fields -only. --/ - -set_option autoImplicit false - -namespace Libp2p.Protocols.Mock.Muxer - -open Conc Streams -open Libp2p.Core (Role MuxSession Muxer) - -/-! ## Frames -/ - -/-- The header of a frame: id, kind, length. -/ -def headerLen : Nat := 7 - -/-- The largest payload of one frame. -/ -def maxPayload : Nat := 2 ^ 16 - 1 - -/-- One frame on the wire. -/ -def frameB (sid kind : Nat) (payload : ByteArray) : ByteArray := - ByteArray.mk #[(sid / 2 ^ 24).toUInt8, (sid / 2 ^ 16).toUInt8, (sid / 2 ^ 8).toUInt8, - sid.toUInt8, kind.toUInt8, (payload.size / 256).toUInt8, payload.size.toUInt8] ++ payload - -/-- The frames of one write: the bytes in pieces of at most `maxPayload`. -/ -def dataFramesB (sid : Nat) (bytes : ByteArray) : ByteArray := Id.run do - let mut out := ByteArray.empty - let pieces := (bytes.size + maxPayload - 1) / maxPayload - for i in [0:pieces] do - out := out ++ frameB sid 0 (bytes.extract (i * maxPayload) (i * maxPayload + maxPayload)) - return out - -/-- One frame at the front of `b`: the id, the kind, the payload, and the -bytes it took; `none` while the frame is not whole. -/ -def readFrame? (b : ByteArray) : Option (Nat × Nat × ByteArray × Nat) := - if b.size < headerLen then none - else - let byte (i : Nat) : Nat := (b.get! i).toNat - let sid := ((byte 0 * 256 + byte 1) * 256 + byte 2) * 256 + byte 3 - let len := byte 5 * 256 + byte 6 - if b.size < headerLen + len then none - else some (sid, byte 4, b.extract headerLen (headerLen + len), headerLen + len) - -/-! ## The session -/ - -/-- The parts of one stream that the reader reaches. -/ -structure Entry where - /-- The chunks the reader delivers. -/ - inbox : Chan (Except Streams.Error ByteArray) - /-- Set by a reset, so a read after the close of the inbox fails. -/ - rst : OnceRef (Option Streams.Error) - -/-- What the streams and the reader of one session share. -/ -structure Shared where - conn : Connection - /-- The streams by id. Changed only through `update` and `updateGet`. -/ - streams : OnceRef (Std.HashMap Nat Entry) - /-- The next id this side opens. -/ - next : OnceRef Nat - /-- The streams the peer opened, for `accept`. -/ - incoming : Chan Stream - /-- The write token: one frame write at a time. -/ - token : Chan Unit - -/-- Write one frame run under the token. A failed write answers `false`. -/ -def Shared.send (sh : Shared) (bytes : ByteArray) : Async Bool := do - -- Park: the writer before this one sends the token back; a session - -- close closes the token channel and wakes this with `none`. - let some () ← sh.token.recv | return false - let ok ← try sh.conn.write bytes; pure true catch _ => pure false - discard <| sh.token.trySend () - return ok - -/-- A fresh entry. -/ -def newEntry : BaseIO Entry := do - return ⟨← Chan.newUnbounded, ← OnceRef.new none⟩ - -/-- The stream of id `sid` over the session. -/ -def mkStream (sh : Shared) (sid : Nat) (e : Entry) : BaseIO Stream := do - let completions ← Completions.new - Stream.ofPort { - inbox := e.inbox - endedBy := e.rst.get - completions - postWrite := fun tag bytes => do - let ok ← sh.send (dataFramesB sid bytes) - completions.resolve tag (if ok then .ok () else .error .closed) - return .ok () - postConsumed := fun _ => return .ok () - postClose := do - discard <| sh.send (frameB sid 1 ByteArray.empty) - return .ok () - postReset := do - e.rst.set (some .reset) - discard <| e.inbox.trySend (.error .reset) - e.inbox.close - sh.streams.update (·.erase sid) - discard <| sh.send (frameB sid 2 ByteArray.empty) - return .ok () } - -/-- Route one frame from the peer. A new id of the peer's parity opens a -stream; a frame for any other unknown id is dropped. -/ -def route (sh : Shared) (peerParity : Nat) (sid kind : Nat) (payload : ByteArray) : Async Unit := do - let entry? ← (sh.streams.get : BaseIO _) - let e ← match entry?.get? sid with - | some e => pure (some e) - | none => - if sid % 2 = peerParity ∧ kind ≠ 2 then - let e ← newEntry - sh.streams.update (·.insert sid e) - discard <| sh.incoming.trySend (← mkStream sh sid e) - pure (some e) - else pure none - let some e := e | return - match kind with - | 0 => discard <| e.inbox.trySend (.ok payload) - | 1 => e.inbox.close - | _ => - e.rst.set (some .reset) - discard <| e.inbox.trySend (.error .reset) - e.inbox.close - sh.streams.update (·.erase sid) - -/-- The reader loop. `partial`: a peer may send frames forever; the -session's close ends the connection read with `none`, which ends the -loop. At the end every inbox and `incoming` close, so each parked read -and accept wakes. -/ -partial def readLoop (sh : Shared) (peerParity : Nat) (buf : ByteArray) : Async Unit := do - match readFrame? buf with - | some (sid, kind, payload, k) => - route sh peerParity sid kind payload - readLoop sh peerParity (buf.extract k buf.size) - | none => - -- Park: the peer's bytes wake it, and so does `close` of the connection. - match ← sh.conn.read with - | some b => readLoop sh peerParity (buf ++ b) - | none => - -- The session ended under the open streams, so a read after this - -- answers `.closed`, the failure §5.2 keeps apart from an end. - for (_, e) in (← (sh.streams.get : BaseIO _)).toList do - e.rst.update fun r => r <|> some .closed - e.inbox.close - sh.incoming.close - sh.token.close - -/-- Run a mock session over `conn`. -/ -def openSession (role : Role) (conn : Connection) (leftover : ByteArray) : - ExceptT Libp2p.Core.Error Async MuxSession := do - let token : Chan Unit ← Chan.new 1 - discard <| token.trySend () - let sh : Shared := { - conn - streams := ← OnceRef.new {} - next := ← OnceRef.new (if role = .initiator then 1 else 2) - incoming := ← Chan.newUnbounded - token } - let owner ← TaskSet.new - let peerParity := if role = .initiator then 0 else 1 - owner.spawn (readLoop sh peerParity leftover) - return { - -- The mock wire carries no protocol label, so the id goes unread, - -- as yamux drops it (the core `MuxSession.openStream` doc). - openStream := fun _ => do - let sid ← (sh.next.updateGet fun n => (n, n + 2) : BaseIO Nat) - let e ← newEntry - sh.streams.update (·.insert sid e) - mkStream sh sid e - accept := sh.incoming.recv - close := sh.conn.close - -- The reader loop has no failure of its own, so the join answers - -- `.ok` once the loop ends. - join := ExceptT.lift owner.joinAll } - -/-- The mock muxer value. -/ -def muxer : Muxer := ⟨⟨"/leanp2p-mock-mux/1.0.0"⟩, openSession⟩ - -end Libp2p.Protocols.Mock.Muxer diff --git a/packages/libp2p/protocols/Libp2p/Protocols/Ping.lean b/packages/libp2p/protocols/Libp2p/Protocols/Ping.lean index 5d3e7350..aa91923b 100644 --- a/packages/libp2p/protocols/Libp2p/Protocols/Ping.lean +++ b/packages/libp2p/protocols/Libp2p/Protocols/Ping.lean @@ -2,8 +2,9 @@ import Bytes import Conc import Streams.Error import Streams.Stream -import Libp2p.Protocols.Mock.Core +import Libp2p.Core import Libp2p.Protocols.Constants +import Libp2p.Protocols.StreamError /-! # Ping @@ -27,7 +28,7 @@ set_option autoImplicit false namespace Libp2p.Protocols.Ping /-- The ping protocol id. -/ -def protocolId : Mock.Core.ProtocolId := Constants.pingId +def protocolId : Libp2p.Core.ProtocolId := Constants.pingId /-- The ping payload size of the spec. -/ def payloadSize : Nat := Constants.pingSize @@ -138,12 +139,12 @@ def handleCore (s : Streams.Stream) : Conc.Async (Except Error Unit) := /-- One map from this protocol's error into the coarse core error, used once, at the seam value. -/ -def mapPingError : Error → Mock.Core.Error - | .stream e => Mock.Core.mapStreamError e +def mapPingError : Error → Libp2p.Core.Error + | .stream e => mapStreamError e | e => .protocol (toString (repr e)) /-- The ping handler value. -/ -def pingHandler : Mock.Core.StreamHandler := +def pingHandler : Libp2p.Core.StreamHandler := { id := protocolId, handle := fun _ctx s => ExceptT.mk ((Except.mapError mapPingError) <$> handleCore s) } diff --git a/packages/libp2p/protocols/Libp2p/Protocols/ReqResp/Payload.lean b/packages/libp2p/protocols/Libp2p/Protocols/ReqResp/Payload.lean index 33184090..d395ed1d 100644 --- a/packages/libp2p/protocols/Libp2p/Protocols/ReqResp/Payload.lean +++ b/packages/libp2p/protocols/Libp2p/Protocols/ReqResp/Payload.lean @@ -1,5 +1,6 @@ import Varint import Snappy +import Streams.Error import Libp2p.Core.Error import Libp2p.Core.ProtocolId import Libp2p.Protocols.ReqResp.Crc32c diff --git a/packages/libp2p/protocols/Libp2p/Protocols/StreamError.lean b/packages/libp2p/protocols/Libp2p/Protocols/StreamError.lean index 088a6d41..eae1d34c 100644 --- a/packages/libp2p/protocols/Libp2p/Protocols/StreamError.lean +++ b/packages/libp2p/protocols/Libp2p/Protocols/StreamError.lean @@ -8,9 +8,7 @@ A handler of this package reads and writes one negotiated `Stream`, and a failed read or write answers a `Streams.Error`. The handler seam of `libp2p/core` fails with the coarse `Core.Error` (ARCHITECTURE §3.5), so each handler maps the stream error once, through this function. - -Identify and ping still type over `Libp2p.Protocols.Mock.Core`, which -keeps its own copy of this map until their swap (issue #55). +Identify, ping, and req/resp share it. -/ set_option autoImplicit false diff --git a/packages/libp2p/protocols/docs/ARCHITECTURE.md b/packages/libp2p/protocols/docs/ARCHITECTURE.md index 6cd65031..d34e6cb7 100644 --- a/packages/libp2p/protocols/docs/ARCHITECTURE.md +++ b/packages/libp2p/protocols/docs/ARCHITECTURE.md @@ -27,8 +27,6 @@ group is §7, row 10). The spike has no req/resp or gossipsub code. | `Libp2p/Protocols/ReqResp/Limiter.lean` | `MAX_CONCURRENT_REQUESTS`: the pure table rule with its bound theorem, and the per-peer `Limiter` over `OnceRef` | | `Libp2p/Protocols/ReqResp/Exchange.lean` | the shell over the core: the requester `request` and `requestPeer`, the responder `serve`, the handler value the registry stores, and the deadlines | | `Libp2p/Protocols/StreamError.lean` | `mapStreamError`, the one map from a stream error into `Core.Error` that the req/resp handler uses | -| `Libp2p/Protocols/Mock/Core.lean` | the mock of W5.2 that identify and ping still type over, until their swap (issue #55) | -| `Libp2p/Protocols/Mock/{Muxer,HostStream}.lean` | the test values that stand in for a muxer value of W5.4 and the host of W5.6, over the real core seams; the muxer swap is due (`libp2p/mux` took the real core in PR #84, issue #77 closed, the swap owes on issue #78), and the host swap waits for the host's negotiate swap (issue #70) | | `Libp2p/Protocols/Gossipsub/Rpc.lean` | the RPC message with its `ProtoMessage` instance (§3.2) | | `Libp2p/Protocols/Gossipsub/Core.lean` | `State`, `Event`, `Action`, `ProtocolError`, and the total `step` that holds mesh, scoring, and heartbeat (§3.3) | | `Libp2p/Protocols/Gossipsub/Node.lean` | the loop task over the core, and the publish and subscribe surface at the seam level | @@ -64,17 +62,20 @@ package; §4.9 names no echo, so no module line covers it. one frame and caps at 64 KiB. The two handler values serve inbound streams and register under their ids. The responder builds the message from the host's identity, - addresses, protocol list, observed address, and agent version, as the - spike's `respond` does. `Identify.pushTo` announces the same record + addresses, protocol list, and agent version, as the spike's `respond` + does. The observed address is the `remoteAddr` of the stream's + `StreamContext`, as go-libp2p reads it from `s.Conn()` + (`vendor/go-libp2p/p2p/protocol/identify/id.go`). The push handler + checks the pushed key against the context's `remotePeer`. `Identify.pushTo` announces the same record on the stream that the host opened under `pushId`, and then half-closes. The host calls the sender after the local address set or the local protocol set changes. Go's identify service skips a push when the snapshot did not change, merges pending pushes into one round, and skips a connection that already carries the current record - (the spike's `vendor/go-libp2p/p2p/protocol/identify/id.go`, the - `loop` and `sendPushes` functions). This package sends one record per + (`vendor/go-libp2p/p2p/protocol/identify/id.go`, the `loop` and + `sendPushes` functions). This package sends one record per call and starts no timer. A received push updates the peerstore - through the host. The push stores the addresses. The + through the host (`Host.addAddrs`). The push stores the addresses. The peerstore surface of the host doc holds addresses only, so a push's protocols list has no store yet. Go's push handler stores both. A push frame must carry the public key. The spec says to ignore missing @@ -96,9 +97,7 @@ package; §4.9 names no echo, so no module line covers it. stream to the peer and negotiating the id is the host's job (W5.6), as go-libp2p's `NewStream` does it (`vendor/go-libp2p/p2p/host/basic/basic_host.go`, line 441). The host - names it `newStream`. The host still upgrades through a mock of - `libp2p/negotiate` (issue #70), so the suite runs against a mock of - the call. `requestPeer` takes the call as an argument, with a slot + names it `newStream`. `requestPeer` takes the call as an argument, with a slot of the peer's `Limiter`, and runs `request` on the stream the call returns. `request` needs no host type: it writes the request, half-closes, and hands each response chunk to a callback @@ -264,16 +263,13 @@ Both spike programs call `Ping.ping`. forbids the request and a wait would park on another request's deadline. The slot goes back on every path. The responder's side of the rule, "MAY penalise", is scoring, and stays with the client. -- **The suite runs over the sim through two mocks.** The mock muxer is - one value of the `Muxer` seam of `libp2p/core` over a sim - `Connection`, and the host stream mock fixes minimal signatures for - the outbound stream call (go-libp2p's `NewStream`, - `vendor/go-libp2p/p2p/host/basic/basic_host.go`, line 441) and for - `setHandler`. Both type over the real core. `libp2p/mux` landed its - values over the real core (PR #84, issue #77 closed), so the muxer - swap is due (issue #78). The host swap waits for the host's - negotiate swap (issue #70). The suite then runs over yamux and the - host. +- **The suite runs between two hosts over the sim.** `Tests/HostPair.lean` + builds two real hosts on the test values of root §3.1: the sim + transport, the fixed-key Noise value, and a test clock, with yamux. The + requester opens its stream through the host's `newStream` (go-libp2p's + `NewStream`, `vendor/go-libp2p/p2p/host/basic/basic_host.go`, line + 441). The responder registers through `setHandler`. A host failure + that wraps a seam error reaches `requestPeer` as that error. ## What the package must not depend on diff --git a/packages/libp2p/protocols/docs/PLAN.md b/packages/libp2p/protocols/docs/PLAN.md index 38dfa427..bd5e383c 100644 --- a/packages/libp2p/protocols/docs/PLAN.md +++ b/packages/libp2p/protocols/docs/PLAN.md @@ -94,11 +94,15 @@ in the codec group wrapping upstream `google/snappy`. - The concurrency limit: two requests with one id take a slot each, a third is refused, another id has its own slots, and a request gives its slot back when it ends (the bound of `Table.take` is a theorem). -- Over the sim transport, through the mock muxer and the host stream - mock (PRINCIPLES 1.4): a request through the host gets its chunks, - with whole and with split writes; an id the peer does not serve - resets the stream; a silent peer fails the request at its deadline; - a connection closed under a parked read ends the request. +- Between two hosts over the sim transport, with the fixed-key Noise + value and yamux + (PRINCIPLES 1.4): + - a request through the host gets its chunks, with whole and with + split writes; + - an id the peer does not serve fails the open, since + multistream-select answers `na`; + - a silent peer fails the request at its deadline; + - a connection closed under a parked read ends the request. - The error/EOF distinction: a framing failure returns the protocol error, and a clean stream end returns `finished`, through different channels (§5.2). An end inside a chunk is an early EOF.