[Wenbobobo]

Summary

Adds unit 3 of libp2p/protocols: gossipsub v1.1 as a total step, with the loop and the application seam that drive it. Unit 3a and the pure half of 3b bring the codec, the signing check, the score function, the caches and the router core. Unit 3b adds the session loop with publish and subscribe, the heartbeat schedule that the trickle regressions pin, and the Go-encoded RPC fixture that pins the wire bytes.

Refs #23. Row 3c of the package PLAN stays open; the two small questions below ask about the gate.

The live interop gate of unit 3c cannot run before the dependency units listed under "The 3c gate" merge, and the package PLAN gives its row 3c the dependencies unit 3b and W5.6. This description records what we measured instead: nine Shadow control cells of the vendored harness, the attribution of every Lean cell to the unit that blocks it, and the adapter contract. The measurements ran on the author's host. The branch carries the adapter's pure half, and its socket half follows the W5 stack. The image is the
Shadow release tarball plus the Go 1.27.3 and Rust 1.99.1 toolchains over Ubuntu 24.04, and it needs
--security-opt seccomp=unconfined --shm-size=8g. The harness runs its own orchestrator and checks,
with one small Makefile override, because the default recipe builds every composition and the
baselines need only the two reference binaries.

uv run run_gate.py --node_count 32 --composition go --scenario subnet-blob-msg --seed 1 \
  --output_dir /runs/go-32-s1
uv run checks/subnet_blob_msg.py /runs/go-32-s1           # reach, the harness check
uv run analyze_message_deliveries.py /runs/go-32-s1       # p50 and duplicate counts

The router models a subset of the v1.1 spec. The omissions and the spec deltas are documented in the module header of Core.lean and in the module header of Node.lean.

What changed

packages/libp2p/protocols:

• Libp2p/Protocols/Constants.lean: the gossipsub protocol ids /meshsub/1.1.0, /meshsub/1.0.0 and /floodsub/1.0.0, and the RPC cap of 1 MiB.
• Libp2p/Protocols/Mock/: the seam stand-ins for the unmerged dependencies, listed under Risk. Mock/Host.lean now also declares HostSeam, the two calls the loop makes, and Switch, an in-memory double of that seam that serves the loop suite. Mock/Core.lean carries the sender peer in StreamHandler, because the router scores, greylists and forwards by it.
• Libp2p/Protocols.lean: imports Constants, the gossipsub modules and Gossipsub/Node.lean.
• Libp2p/Protocols/Gossipsub/Types.lean: topic and message ids, the published message, the fixed-point score unit, the score thresholds, and the time unit.
• Libp2p/Protocols/Gossipsub/Rpc.lean: the RPC message and its control envelope, with the Pb.ProtoMessage instances. Field numbers and cardinalities follow the vendored protobufs in vendor/specs/pubsub.
• Libp2p/Protocols/Gossipsub/Sign.lean: strictSign, strictNoSign, the signature input, and the spec's default message id.
• Libp2p/Protocols/Gossipsub/Score.lean: the P1 to P7 formulas and the decay.
• Libp2p/Protocols/Gossipsub/Cache.lean: the message cache, the seen cache, the backoff table, and the IWANT promise table.
• Libp2p/Protocols/Gossipsub/Core.lean: State, Event, Action, ProtocolError, and the total step. run drives a list of events.
• Libp2p/Protocols/Gossipsub/Node.lean: the loop task over the core, the heartbeat alarm, one writer task and a bounded queue per peer, the /meshsub/1.1.0 inbound handler, the receipt observer, and the application seam.
• packages/libp2p/protocols/docs/PLAN.md: the trickle regressions gain an owner under ## Test milestones (unit 3), with the loop suite's checks beside it.
• packages/libp2p/protocols/tools/go-rpc-fixtures: the generator that writes the Go-encoded RPC fixture, with its go.mod and go.sum. Go tooling is test only (repo CLAUDE.md, "Dependencies").

Tests: Tests/Gossipsub/{Rpc,Sign,Score,Cache,Core}.lean replay fixed transcripts. Tests/Gossipsub/Node.lean runs the loop over the in-memory switch of Mock/Host.lean and a test clock. Tests/Gossipsub/Wire.lean decodes Tests/fixtures/gossipsub-rpc-go.json and checks it. All of them are wired into Tests/Main.lean.

The loop and the seam (unit 3b)

One task owns the router state, and it parks only on the one event channel that stop closes. Every action the loop performs returns without parking, so no peer can hold the loop. The delivery callback of subscribe and the Config.onRpc observer run on the loop task, and the module header requires both to return without parking.

• The loop. It takes one input, either a core event or an alarm wake, steps the core, and asks one Conc.Alarm for the next due time. stop closes the event channel, resets installed streams and joins the tasks. A writer parked inside HostSeam.newStream keeps stop parked until the host ends that call. The alarm task posts the wake. The loop is a repeat with a mutable state, as the yamux session loop is, so a ready park costs no stack.
• Outbound. Each known peer has one writer task and one stream, matching Go and Rust. The loop encodes the frame and offers it to the peer's queue of 32 frames. A full queue drops the frame, just as Go does when a peer's queue fills, and Node.dropped counts the drops, both here and at the pending-send bound. The writer opens the peer's stream, writes in order, and closes the stream when it ends. A failed write retires the entry and closes the queue, so the next send opens a fresh stream; the peer stays in the router, because its inbound stream is still open.
• Inbound. A peer opens one stream for many RPCs. The handler reads every frame of that stream: it collects the length prefix in a small buffer, checks the length against Constants.rpcCap, allocates the body once, and copies each input byte once with a cursor. It posts one event per frame with the opener as its sender, and resets the stream on a bad prefix, an over-cap frame or an end of stream inside a frame. Small reads therefore cost linear time, and the reader keeps constant stack for any number of chunks. It announces its opener first, because the core ignores an RPC from a peer it does not know.
• The application surface. publish builds the message of a topic and a payload and offers it to the queue. subscribe registers a callback that must not park, and unsubscribe drops the callbacks of a topic. peerJoined and peerLeft take the connection events of the host. stop sets a closing flag, closes the channel, closes every writer queue and resets every installed stream, and joins the owned tasks.
• The receipt observer. Config.onRpc sees each inbound RPC, with its sender, before the core step, so a harness can log every received message including a duplicate.

The module header records the decisions, five of which cite the exact Go or Rust source line they mirror:

1. No signer and no local peer id. Core.validationOk uses strictNoSign, which requires from and seqno absent. The Go and Rust reference implementations configure the same policy (go-libp2p/main.go:35-37, rust-libp2p/src/main.rs:120-131).
2. The loop announces a subscription change. Core.join announces our topics when a peer joins. Nothing announces a subscribe after the join, so the loop sends the one record, before the core step. The Go library announces from its own layer (pubsub.go:1205-1232), outside its router.
3. The heartbeat order is a replayable order. A tick carries the known peers in an order derived from the heartbeat count and each peer's bytes, so a run replays and the order depends on no random source. Go shuffles with rand; the hash keeps the sampling shape and makes the test deterministic.
4. The gossip spread is opt-in. Go queues the heartbeat's IHAVEs and flushes them at once (gossipsub.go:2078-2092). The loop can spread them across the interval, and Config.trickle fixes the spread. Its default spreads nothing, so the default behavior matches Go. The suite pins the spread with an explicit function, because issue [W6.4] gossipsub v1.1 (gate) #23's done list names the trickle regressions and the schedule belongs to the loop.
5. The stream handler carries the peer. The host knows the peer at the call site and drops it at the handler. The router needs the sender, and identify needs the same field for its validate.
6. Subscribe registers before it posts. A delivery that the loop handles between the post and the registration would miss its callback. An earlier iteration of this branch posted first and lost 11 deliveries in 60 trials. This head registers first and takes its own registration back by id when the post is refused, and concurrent callers remove only their own entries.

What the step implements

• The RPC codec for the v1.0 and v1.1 control messages, including the prune peer list.
• strictSign and strictNoSign, and the signature input libp2p-pubsub: followed by the
  re-encoded message with signature and key cleared.
• The score formulas P1, P2, P3, P3b, P4, P5, P6 and P7, and the decay.
• The message cache, the seen cache, the backoff table, and the IWANT promise table.
• The mesh heartbeat: decay, the per-topic plan, the prune of a mesh above dHigh down toward d,
  the graft up toward d from peers at or above score 0 and outside backoff, and the negative
  prune.
• Inbound handling: validate, reject a repeated id, deliver, score the sender, and forward a new
  message to every other peer of mesh[topic].
• Local publish: cache the message, record its id as seen, and forward to the mesh, or to the
  fanout when the router does not subscribe.
• Gossip emission: after the mesh is settled and before the cache shifts, each topic of the mesh
  and the fanout sends its ids to peers of the supplied order that sit in neither set and score at
  or above the gossip threshold, up to dLazy per topic.

What the step does not implement

The step omits these. No flag enables them.

• Floodsub peers. PubsubProto is stored on the peer record and no path reads it, so an
  inbound message goes to the mesh only.
• Peer exchange. ControlPrune.peers decodes and round-trips, but handlePrune ignores it,
  and acceptPXThreshold is never read.
• Opportunistic grafting. opportunisticGraftThreshold is never read.
• Fanout expiry. fanoutTtl is never read, so a fanout entry lives until the router subscribes
  to the topic or the peer leaves.
• The IWANT follow-up penalty. handleIhave records a promise, and nothing calls
  PromiseTable.deliver or PromiseTable.broken, so an expired promise changes no score.
  iwantDeadline is written and never compared.
• P5, P6 and P7 have no producer. No router event writes appScore, ipColocation or
  behaviourPenalty, and PeerData carries no address, so P6 cannot be computed from the state
  the router keeps. The score suite tests the formulas directly.
• The mesh delivery window. meshMessageDeliveriesWindow is stored and never read, so a mesh
  peer counts toward P3 for every accepted message rather than only for a first or near-first
  delivery inside the window.
• Score retention. leave deletes the peer record. The spec keeps the score for RetainScore.
• Direction and score in the mesh cut. planTopic drops the oldest entries. dScore is never
  read and there is no outbound flag, so the spec's D_out quota is absent.
• Adaptive gossip. gossipFactor is stored and never read, so the emission count stays at
  dLazy instead of growing with the number of eligible peers.
• The extended validator. A message is accepted or counted as an invalid delivery. There is no
  Ignore outcome, the policy is not per topic, and validationOk uses strictNoSign.
• IHAVE and IWANT caps, and flood publishing. Neither is present, and publishThreshold is
  stored and never read. The gossip threshold and the graylist threshold are read.
• The unsubscribe backoff. unsubscribe writes pruneBackoff. The spec uses a shorter
  UnsubscribeBackoff, and subscribe does not consult the backoff.

Recorded deltas

• Message.from is bytes. The spec says optional string. The codec reads and writes bytes,
  so a from value that is not valid UTF-8 round-trips here and is rejected by a conforming peer.
  data, seqno, signature and key are bytes in the spec too.
• The signature input clears key and drops unknown fields. The spec signs the marshalled
  bytes with signature removed and with unknown fields kept. This follows the Go implementation
  and clears key as well, and it re-encodes, so an unknown field that arrived on the wire is not
  in the signed bytes. Sign.lean states the key part.
• An omitted string comes back as empty. SubOpts.topicid and the control topicId fields
  collapse an absent field to "", so a re-encode emits a field the input omitted.
• P7 has a threshold. The vendored spec describes P7 as the square of the counter, and the
  global parameter table names no threshold. This module carries behaviourPenaltyThreshold, as
  the Go implementation does, and squares the excess over it. A threshold of 0 reproduces the
  spec, and Score.lean states this.
• The default message id is the payload. validationOk uses strictNoSign, which requires
  from and seqno to be absent, so the spec's default id from ++ seqno is empty for every
  accepted message and the seen cache would treat all of them as one. defaults.msgId is the
  payload bytes, which is the content-addressed choice the spec pairs with strictNoSign. The
  consequence, which the spec's own margin note records, is that two messages with the same
  payload collide inside the seen-cache window. Sign.defaultMsgId remains for a caller that
  pairs it with strictSign.
• A graft for an unsubscribed topic is ignored. The v1.0 spec answers with PRUNE. The v1.1
  spam measures say to ignore it, because answering opens a way to flood the router with
  GRAFTs. This step follows v1.1, and core.reject.graft-unknown-topic-ignored pins that
  choice.
• The message cache ages by one and drops at historyLength. An entry written at age 0
  survives historyLength - 1 shifts, and gossipIds lists entries with age < historyGossip.

The loop's deltas from the reference implementations.

• The gossip spread is opt-in. Go flushes the heartbeat's IHAVE gossip at once. This loop can spread it, and its default spreads nothing.
• The message id function is a parameter. Go and Rust derive the harness id from the first eight bytes of the data. Core.defaults pins the payload bytes, which is the content-addressed choice that pairs with strictNoSign. The harness adapter supplies Core.Params.msgId.
• The peer order is a replayable hash. Go and Rust shuffle with a random source, and this loop orders by the heartbeat count and the peer bytes, so a run replays.
• A slow peer stalls its own writer. Go writes from a per-peer goroutine over a bounded queue and drops on a full queue. This loop does the same, and Node.dropped counts the drops.
• A parked host open ends the way the host ends it. If a writer parks inside newStream, stop waits for that call to return; the module header assigns the end of the open to the host session teardown, and the mock switch never parks.

The 3c gate (unit 3c)

Every unit of the row's closure merged on 2026-11-07: #11 identity (#63), #14 yamux (#62), #15 core (#64),
#16 Noise (#69), #17 mux (#49), #18 negotiate (#40), #19 host (#61) and #20 identify/ping (#45), with
#43/#75 ENR and #46 req/resp. hackathon26 stands at fd70eeb, and this branch carries the merged stack.

The adapter's pure half. Libp2p/Protocols/Gossipsub/Interop/ reads the params.json script (the
seven in-scope instructions, with the two v1.2 ones rejected), writes the NDJSON records, resolves the
node number from the nodeN name, formats the harness message id, reads the hosts table, and plans the
run over a virtual clock. Tests/Gossipsub/Interop.lean checks it with 160 checks, registered in the
suite runner, so CI runs them.

The socket half. packages/cli/GossipsubInterop.lean, GossipsubSession.lean and Main.lean build
the gossipsub-interop executable over the real host: TCP, Noise, the yamux adapter, multistream-select,
identify and the gossipsub loop. A small C shim in packages/cli/hostname resolves the nodeN name.

One interop fix. The identify response lists /ipfs/id/1.0.0 and /meshsub/1.1.0 now. Before the
change, go-libp2p-pubsub never opened its outbound pubsub stream to a Lean peer, because it notifies a
peer only when identify lists the pubsub protocol id. In a 32-node seed-1 mixed cell, Go's outbound RPCs
to Lean peers went from 0 to 3851, subscriptions from 0 to 153, GRAFTs from 0 to 44 and publishes from 0
to 991. The mixed cell reached 48 percent before the fix and 100 percent after it. That 0.48 run predates
the cells below.

The 3c gate runs on the merged head. Head 7ac636a89f5e207a2a6785320d4ff661c7f50093 is the nit commit
d1c1ab3 plus the merge of hackathon26 at 6a1f832. The two 3c cells below ran on it. We built the
participant from this head; its SHA-256 is 0e083022d1896af1ecb8145931e278b406288c3c9823f60b390f51865a5a9e2a.
That digest belongs to the executable file. The earlier cc4a74ae is also the executable digest of the
407878c build.

Every run in this section used 32 nodes on topic subnet-blob-msg, in Shadow 3.3.0 and the
gate-shadow:2026-11-06 image, with the vendored harness at /work:

Composition	Seed	Reach	Duplicates per node
Go and Lean	1	1.0	6.25
Rust and Lean	1	1.0	5.39

Reach 1.0 means all 12 checked messages reached every non-publisher node. The check skips the 4 warmup
messages. p50 is the mean of the 12 per-message median dissemination times. Duplicates per node is the
analyzer's average duplicate count per node over the same messages.

An earlier matrix of sixteen runs on head 407878c, with the executable cc4a74ae, gives the seed and repeat
measurements:

Composition	Runs	Reach	p50	Duplicates per node
Go	seeds 1, 2, 3	1.0	94.0 to 125.7 ms	4.15 to 4.58
Lean only	seeds 1, 2, 3, and a repeat at seed 1	1.0	106.7 to 129.3 ms	7.41 to 7.68
Go and Lean	seeds 1, 2, 3, two runs each	1.0	no comparable p50 (1)	6.14 to 6.80 (2)
Rust and Lean	seeds 1, 2, 3	1.0	no comparable p50 (1)	4.29 to 5.36 (2)

1. Go and Rust stamp their records on the 2000-01-01 synthetic epoch; Lean stamps its records on 1970-01-01.
   The analyzer's cross-implementation p50 is therefore unusable.
2. A mixed count covers both implementations. Every Rust cell also ran Lean. The Go and Lean cell ran 16 Go and
   16 Lean in seeds 1 and 2, and 19 Go and 13 Lean in seed 3. The Lean-only cell reproduced byte for byte at seed
   1; the Go and Lean cell's count moved by up to about 10 percent between two runs of the same seed.

The harness compares reach only. checks/subnet_blob_msg.py fails below 1.0, and
analyze_message_deliveries.py reports p50 and the average duplicate count without comparing them. We report
the duplicate counts above as information.

Test plan

On this host. The full lake test does not link on Windows, because the crypto C shims need OpenSSL 3.2
or newer headers that the Windows toolchain does not carry. The five gates of .github/workflows/ci.yml
on this head ran in a Linux container with the pinned toolchain and the vendored sources.

• lake build --wfail: "Build completed successfully (281 jobs)", zero warnings.
• lake test: "summary: 27696 passed, 0 failed, 0 todo (known gaps), 10 skipped (needs phase 1+ features)".
• lake test -- +RTS -N1 -RTS: the same summary line.
• scripts/lint-imports.sh: "lint-imports: checked 180 module files, 0 violations".
• scripts/vendor-pull.sh --verify: every vendored tree reports OK.
• The gossipsub loop suite, the interop suite and the req/resp, host and negotiation suites all run inside that summary.
• #print axioms over the public theorems of the gossipsub modules is unchanged by this head: no sorry, no admit, no native_decide, no unsafe, and no module declares an axiom.
• CI runs the same five gates on the pushed head 407878c.

The gossipsub suites add the loop checks (109), the wire checks (104) and the interop checks (160).

Notes for reviewers

Score monotonicity requires non-zero penalty weights. Params.Valid forces the penalty weights
to be non-positive, and defaults sets every weight to 0, so under those parameters the
monotonicity theorems hold because both sides are 0. They become non-trivial only when the caller
configures a non-zero weight, which is what the score suite does. The core suite uses the zero table except for
the one check that configures invalidMessageDeliveriesWeight.

heartbeatMeshBound holds for any score parameters. The mesh bound relies only on the
List.take at dHigh and on the fact that the negative prune only removes peers, so the mesh size
invariant is independent of the score configuration.

The gossip score gate covers every gossip action. mem_gossipActions concludes the threshold
for every action gossipActions builds, because every one of them is an ihave. tickGossipGated
lifts that to the heartbeat by showing that the prune and graft actions fail the ihave test.

rpcGraylistIgnored proves the gate. The graylist premise is the only hypothesis, and the
conclusion is step p s (.rpc sender bytes) = .ok (s, []), so the gate runs before the decode and
the bytes are never consulted.

Deduplication is one step. stepDeliverUnseen says a delivered message was absent from the
seen cache of the pre-state. It does not say that a message is delivered at most once across a run
of run, because the one-step form is what the acceptance loop establishes directly.

Two graft laws are private equations. A graft into an active backoff and a graft into a mesh
that already holds dHigh peers each produce a prune. Both are private theorems,
handleGraft_backoff and handleGraft_overfull, and both have a suite check. Neither is stated
as a property of step.

The backoff exclusion covers the heartbeat only. tickNoBackoffGraft says the heartbeat never
grafts a peer whose backoff is active. subscribe also grafts and filters backoff, and no theorem
covers that path.

An inbound forward never returns to the sender. forwardPubs_excludes_sender says so, and
core.forward.mesh checks a three-peer mesh. publishLocal records the id it forwards, so a later
echo of the same id is neither delivered nor forwarded again, which
core.forward.own-echo-dropped checks on a non-empty mesh.

Risk / trust footprint

No new Lean dependency. The gossipsub modules import Pb, Streams.Framing, Constants and the gossipsub modules themselves. packages/libp2p/protocols/tools/go-rpc-fixtures is a test-only Go tool (repo CLAUDE.md, "Dependencies": Go tooling stays test only and never on a shipped or proof path). Lake does not build it, and the import lint reads only Lean modules.

When this branch started, four dependencies were unmerged, so it declared their interfaces in Libp2p/Protocols/Mock/. Every one of them merged on 2026-11-07, and the branch now deletes the six mocks it owned: this package's core, host and negotiate mocks, the negotiate core mock, the mux core mock and the security core mock. The gossipsub loop, the upgrader, the host, the muxer and identify take Libp2p.Core types, and the inbound handler reads ctx.remotePeer from Libp2p.Core.StreamContext.

Libp2p/Protocols/Mock/ keeps the req/resp mocks that #46 landed with its own package. They move with that package, not with this branch.

#print axioms over the public theorems shows the standard axioms only, apart from the three RPC frame theorems decodeFrame?Encode, decodeFrame?EncodeRpc and decodeFrame?OverCap. Those reduce to Streams.Framing.Frame, which takes Streams.Mock.Varint.decodeEncodeSuffix. That axiom belongs to net/streams, which this pull request does not touch, so removing it belongs to Framing.lean.

LICENSE (LGPL version 3)

• I have read and accepted LICENSE (LGPL version 3), NOTICE and CLA in the root of this project.

[leolara]

Reviewed at 0699717, the head after my nit commit below. I read every changed file, ran the checks on this host, and audited the axioms.

Checks

• lake build --wfail: 189 jobs, zero warnings.
• lake test: 25997 passed, 0 failed, 2 skipped. The skips are pre-existing.
• lake test -- +RTS -N1 -RTS: the same numbers.
• scripts/lint-imports.sh: 107 module files, 0 violations.

Every number matches the body's claims. The suite counts match too: 40 RPC, 19 signing, 33 score, 32 cache, 25 core, 149 new checks.

The core and its proofs

The shape follows ARCHITECTURE §3.3. State, Event, and Action are plain data, and the total step at Core.lean:825 reads no clock and makes no random choice. Time arrives as Event.tick with a peer order, so a test replays a run with no task and no network.

Bounded inputs hold. Constants.rpcCap is 1 MiB (Constants.lean:25), and the frame decoder checks the cap before it takes the body (Rpc.lean:885). decodeFrame?OverCap proves the over-cap prefix fails before any body byte is read. The core sees message bytes only through the frame step, so the cap gates every path in this PR.

This PR adds no task, no channel, and no shared cell, so the §4.1 and §5 contracts have no surface to check here. §5.6 does not apply either: the PR runs no negotiation and hands no stream. Stringly-typed surfaces stay wrapped: topic names sit in TopicId, and the three protocol ids are named constants at Constants.lean:15.

I ran #print axioms over 41 public theorems across the five modules. Every theorem reduces to the standard axioms, propext, Classical.choice, and Quot.sound. Exactly three theorems also name Streams.Mock.Varint.decodeEncodeSuffix: decodeFrame?Encode, decodeFrame?OverCap, and decodeFrame?EncodeRpc. That axiom belongs to net/streams and to PR #32's ledger row on issue #25. This PR adds no axiom, and no sorryAx appears anywhere. The body's claim holds.

The router theorems say what a reviewer wants them to say. heartbeatMeshBound (Core.lean:1031) caps every mesh at dHigh after a tick. rpcGraylistIgnored (Core.lean:1059) proves the gate returns the pre-state and consults no bytes. tickGossipGated (Core.lean:1639) gates every gossip action by the threshold. stepDeliverUnseen (Core.lean:1866) ties each delivery to an empty seen-cache lookup. The module headers teach the spec sections, and the deltas are recorded where they appear, the key clearing at Sign.lean:28 and the ignored graft at Core.lean:58 with its test pin.

Mocks

The mocks comply with RULES.md. Mock/ lives inside the package, declares opaque surfaces, imports nothing from a real package, and adds no axiom. Sign.lean takes the crypto primitives as a Prims record (Sign.lean:120), so no proof depends on a stand-in body. The four files match PR #45's set, one comment line apart, as the body says. Mock.Host and Mock.Multiaddr are unused here and exist to keep the shared set unbroken.

The swap obligations at merge time: add the ledger rows on issue #25 for Mock.Identity and Mock.Core, drop the two unused mocks without connections, and replace the used ones when #11 and #15 land. The 12-hour window of RULES.md runs from the last dependency merge. The Streams.Mock.Varint exposure is already covered by PR #32's row.

Merge order

Issue #23 needs #19, #20, and #1. #1 is merged. #19 has no PR. #20 is PR #45, open, with a conflict against hackathon26. This PR therefore stays open until both land, per RULES.md.

This PR does not stack on #45. It sits on dd36de0, the current base tip, and carries its own copy of the shared Mock/ files.

The known overlap is real. Both branches add Libp2p/Protocols/Constants.lean and edit Libp2p/Protocols.lean. The two Constants.lean bodies are disjoint, identify and ping on #45, gossipsub here, so the second PR to land rebases and unions them. No other file overlaps.

Scope honesty

The PR carries the pure half of the issue's list: the RPC codec with the v1.0 and v1.1 control messages, the mesh with GRAFT, PRUNE, and backoff, the heartbeat as a tick, the IHAVE and IWANT handling, the seen-cache dedup, the score function P1 through P7 with decay, the signing decision, and the spec defaults at Core.lean:860. The omissions are listed at Core.lean:33 through Core.lean:62 and match the body's list.

The PR covers part of issue #23. The loop task and the publish and subscribe seam, unit 3b's remainder at Node.lean, and the go and rust interop gate, unit 3c, remain. The package docs/PLAN.md carries both as units 3b and 3c, and the module map lists Node.lean. That satisfies the repo's rule that a deferral lives in the governing docs. The tests land in Tests/Main.lean, and no lakefile.toml change was needed, because the lib root already pulls the submodules.

One item has no owner anywhere: the issue's done list names the trickle regressions, and trickle appears in no package document and no unit row. Record the choice, either a unit row in the package docs/PLAN.md or a line on issue #25, so the word keeps an owner. With Closes #23 in the body, the merge closes the issue, so the remaining units need their tracking in place at merge time.

Nits fixed

One commit, 0699717, pushed to this branch:

• Score.lean:88: the TopicParams docstring said the window feeds the core's delivery accounting. The core stores the window and never reads it, as Core.lean:46 records. The docstring now says the same.
• Rpc.lean:861: removed a doubled blank line.
• Core.lean:1607: added the missing blank line before tickPruneNegative.

The issue

The PR does not implement all of issue #23. It implements the router core, the codecs, the score function, the caches, and the signing check that the package plan schedules for units 3a and 3b's pure half, with proofs. The gate and the live loop follow in their own units. The work present is complete, checked, and honest about its bounds.

APPROVE

[leolara]

The organiser revises the verdict: NEED CHANGES.

One pull request completes one issue. This PR closes #23 and carries units 3a and 3b's pure half, while the loop and seam of 3b and the interop gate of 3c wait in the package PLAN. The issue's done-list also names the trickle regressions, and no unit owns them today.

The remaining work lands in this PR before merge:

1. The session loop and the seam of 3b (Node.lean), driven by the pure core this PR already carries.
2. The 3c interop gate, per the issue and the package PLAN.
3. An owner for the trickle regressions, in the package PLAN's test milestones.

The code this PR carries reviewed clean (frame caps, axioms, mocks), and that judgment stands. The verdict changes because the issue is not done.

[Wenbobobo]

Head moved to 407878c, rebased on hackathon26 at fd70eeb. The dependency stack merged, so this branch takes it whole.

• Every mock of a merged dependency is gone: core, the host core and negotiate mocks, the negotiate core mock, the mux core mock and the security core mock. Gossipsub, the upgrader, the host, the muxer and identify speak Libp2p.Core; the inbound handler reads ctx.remotePeer. The one remaining mock, Protocols.Mock for req/resp, belongs to feat(protocols): W6.3, the req/resp framework over the snappy framing format #46 and moves with that package.
• The interop adapter's pure half runs in CI: 160 checks in Tests/Gossipsub/Interop.lean.
• The socket half and the participant are on the branch. packages/cli/{GossipsubInterop,GossipsubSession,Main}.lean build gossipsub-interop over TCP, Noise, yamux, multistream-select, identify and the gossipsub loop, and a C shim resolves the nodeN name.
• One interop fix: the identify response now lists /ipfs/id/1.0.0 and /meshsub/1.1.0. Go's pubsub opens its outbound stream to a peer only after identify lists the pubsub id, so without this line Go sent nothing to a Lean peer. In the 32-node seed-1 mixed cell, Go's outbound RPCs to Lean peers went from 0 to 3851 and the mixed reach went from 48 percent to 100 percent.

Rehearsal on the merged stack, 32 nodes, subnet-blob-msg, seed 1, Shadow: Go control reach 1.0 at 101.4 ms, Lean only reach 1.0 at 111.2 ms, Go and Lean mixed reach 1.0. They are a rehearsal, not the formal gate.

Gates at this head: build 281 jobs; lake test 27696 passed, 0 failed, 10 skipped, the same under -N1; lint 180 modules, 0 violations; vendor provenance OK after the rebase.

[Wenbobobo]

Head 407878c is green on every check and MERGEABLE on fd70eeb. The branch carries the merged stack, the gossipsub loop, the interop adapter and the participant; its six mocks are deleted, and the req/resp mocks stay with #46.

Sixteen runs cover four compositions on the head binary cc4a74ae, 32 nodes, subnet-blob-msg, Shadow v3.3.0 (gate-shadow:2026-11-06). The table is in the description. Two facts frame the tolerance question, and the table's ranges do not show them.

• Duplicates per node: Lean is 63.5 to 85.1 percent above Go in the same seed (7.68 against 4.15 in seed 1, 7.41 against 4.53 in seed 2, 7.49 against 4.58 in seed 3).
• p50: the ranges overlap, and the gap moves with the seed. Lean is 12.7 ms slower in seed 1 and 0.08 ms faster in seed 3.

Four limits apply. No cell ran Rust alone. A mixed cell has no comparable p50, because Go and Rust stamp records on the 2000-01-01 synthetic epoch and Lean on 1970-01-01. A mixed duplicate count covers both implementations, and the Go and Lean split is 16 and 16 in seeds 1 and 2 and 19 and 13 in seed 3. The Lean-only cell reproduced at seed 1: two runs gave the same analysis file. The Go and Lean cell did not match exactly at any seed: two runs per seed gave 6.385 and 6.258, 6.617 and 6.669, 6.802 and 6.143 duplicates per node, so its run-to-run spread reaches about 10 percent and any duplicate tolerance has to allow for that.

The identify fix came before these runs. The Go and Lean seed-1 run of 2026-11-07 had failed the reach check at 0.48; the post-fix Go and Lean seed-1 runs reach 1.0.

The 6 November review kept unit 3c in this PR behind #19 and #20. Both merged on 7 November, so these runs used the merged base.

The harness checks reach only. We would treat 100 percent reach of the 12 checked messages as the pass condition for 3c, and report p50 and duplicates as information. If 3c needs a tolerance on duplicates or on p50, tell us the number and we will run against it. Is that what you intend?

[leolara]

Delta re-review at d1c1ab3 (407878c plus one nit commit). The delta since 76e5136 carries the interop adapter suite (14efcad), the six seam swaps that removed this branch's dependency mocks, the merges that pull the W5 stack in, the socket participant of the cli package (dba4dfc and the five fixes after it), the subscription announce after joins (3aca73c), the gated wire trace (fb49070), and the identify advertisement fix (9dd17ff). I read the delta, ran the four gates, and audited the axioms.

What the delta delivers of the unit 3c gate

The adapter: delivered. Libp2p/Protocols/Gossipsub/Interop/ parses the harness params.json (Script.lean), resolves the Shadow hosts file (Hosts.lean), formats the harness message id (MessageId.lean), writes the NDJSON records (Record.lean), plans the run over a virtual clock (Schedule.lean), and resolves nodeN identities (Address.lean). Tests/Gossipsub/Interop.lean pins all of it to the captured 32-node fixture, 140 checks by r.check count, and Tests/Main.lean runs the suite in CI.

The harness cells over the real stack: delivered. packages/cli/GossipsubSession.lean:42 assembles the real host: TCP, Noise, the yamux Muxer value, multistream-select, and identify with servedProtocols (GossipsubSession.lean:38). packages/cli/Main.lean:73 wires the script driver to that host with dial retries and the bounded record writer. The gossipsub path carries no mocks. The loop suite's switch moved to Tests/Gossipsub/Switch.lean over the real Libp2p.Core handler seam. The root lakefile.toml builds the gossipsub-interop executable.

The green matrix run: recorded, with a broken evidence chain. The body records reach 1.0 for Go only, Lean only, Go and Lean over three seeds with a repeat, and Rust and Lean over three seeds. The numbers are detailed and the pre-fix 0.48 cell is honest. Two facts stop the run from closing the row. First, the body names the run binary's commit as cc4a74ae, built from "this head". That commit exists nowhere: not on this branch, not on the fork, not on upstream, and not on any ref GitHub serves. The runs cannot be tied to any state of this repository. Second, the body itself calls the cells a rehearsal that does not close unit 3c.

The branch and the current tip

The head does not contain the current tip 6a1f832. A test merge of the tip into the branch conflicts in 24 files: the branch carries its own parallel versions of the seam swaps that #79, #80, #81, #82, and #84 landed reviewed on hackathon26, and the two versions differ in Security/Noise.lean, Negotiate/Upgrade.lean, Host/Swarm.lean, Mux/Yamux.lean, the tests, and the docs. The recorded runs exercised the branch's parallel stack, and the merge replaces parts of it, so no run recorded today covers the state the merge produces.

Mock state

The gossipsub, identify, ping, negotiate, security, mux, and host paths on this branch take the real seam types. What remains under Libp2p/Protocols/Mock/ (Core, Host, HostStream, Muxer) serves the req/resp chain and Constants.reqRespId that #46 landed, and the same files and uses sit on the tip. That is base-carried debt under issue #71's ledger, and it does not block this gate.

Checks

• lake build --wfail: 281 jobs, zero warnings.
• lake test: 27696 passed, 0 failed, 10 skipped. The skips are pre-existing.
• lake test -- +RTS -N1 -RTS: the same summary.
• scripts/lint-imports.sh: 180 module files, 0 violations.

The axiom audit

I ran #print axioms over 24 sampled public names of the adapter and the participant: the parser, the parameter mapping, the hosts parser, the record encoder, the schedule plan, the message id, the payload builder, the identity derivation, the script runner, and the trace formatter. Every name reduces to propext, Classical.choice, and Quot.sound, or to no axiom at all. No sorryAx appears. The delta adds no axiom, no sorry, and no partial def. The new modules set autoImplicit false and carry doc comments on their public definitions.

Nits fixed

One commit, d1c1ab3, pushed to the fork with the lease:

• packages/cli/GossipsubInterop.lean:6: the module header said host wiring stays provisional. Cli.Main wires the real host today. The header now says where the driver gets its host.
• packages/libp2p/protocols/docs/PLAN.md:133: the plan said the loop suite runs over the switch of Mock/Host.lean. It runs over Tests/Gossipsub/Switch.lean. The plan now names it.

Two optional cleanups for the author: GossipsubSession.listen has no caller, and provisionalBeforeRpc, provisionalOnRpc, and DelayTable.wait wait for a Node.Config field that does not exist. Keep them with their docstrings or drop them.

What remains for the gate

1. One base merge of the current tip 6a1f832, with the seam conflicts resolved on the tip's reviewed versions, so the branch carries the stack that hackathon26 stands on. Re-run the four gates after it.
2. The matrix run on a binary built from that merged head: one Go and Lean cell, one Rust and Lean cell, one seed each suffices if reach stays 1.0. Record the runs in the body with the full 40-hex SHA of the head, and drop the "rehearsal" hedge once the run carries that SHA.

The adapter and the cells are approved work. The run record is the one open item, and the merged stack is its precondition.

NEED CHANGES

[Wenbobobo]

Head 7ac636a89f5e207a2a6785320d4ff661c7f50093: your nit commit d1c1ab3 plus the merge of 6a1f832. Both review items are addressed below.

Merge. The merge resolved 24 conflicts to the tip's reviewed files. Two temporary pieces remain.

• The first is the host. Its upgrade runs through Host.Mock.Negotiate, whose body throws for issue [SEAM] W5.6 host: the mock connections of #61 #70. The first build from the merge failed: the participant binary exited at startup. The host files (Swarm, Policy, Error) stay at this branch's pre-merge versions. They run the real upgrader. The host imports the pre-seam entry points as Libp2p.Negotiate.Legacy, kept beside the reviewed package. Host/Mock/Negotiate.lean is gone. This is temporary; we remove it when [SEAM] W5.6 host: the mock connections of #61 #70 lands.
• Identify and ping still come from the tip and type over the mock seam (issue [SEAM] W5.7 identify/ping: the mock connections of #45 #55). The participant converts the handler it installs with one adapter, toCoreHandler. This adapter is temporary; it goes when [SEAM] W5.7 identify/ping: the mock connections of #45 #55 lands.

Gates at the head. The build is clean. lake test 27715 passed, 0 failed, 10 skipped; the same under -N1. Import lint 185 modules, 0 violations. Vendor provenance OK.

The two cells ran on a binary built from this head; its SHA-256 is 0e083022…. That digest belongs to the executable file. The earlier cc4a74ae is the executable digest of the 407878c build.

Composition	Seed	Reach	Duplicates per node
Go and Lean	1	1.0	6.25
Rust and Lean	1	1.0	5.39

Each cell used 32 nodes on subnet-blob-msg, in Shadow 3.3.0 and the gate-shadow:2026-11-06 image, with 12 checked messages. The cells took 131 s and 114 s. The description carries the full head SHA and these two cells as the 3c gate runs; the earlier matrix of sixteen runs keeps its own head label.

A mixed cell has no comparable p50. Go and Rust stamp their records on the 2000-01-01 synthetic epoch; Lean stamps its records on 1970-01-01. We report the duplicate counts as information, since the harness compares reach only.

[leolara]

Delta re-review at b3c76b3 (7ac636a8 plus one nit commit). The delta since d1c1ab3 is one commit: the merge of tip 6a1f832, which the last round demanded. I diffed the five seam packages against the tip, ran the four gates, audited the axioms, and checked the run record.

The merge

7ac636a8 merges exactly 6a1f832; it is an ancestor of the head. The resolution takes the tip's reviewed versions for the security package, the negotiate package (Message, Step, Upgrade, Constants, the root), Mux/Yamux.lean with its tests and constants, Tests/Upgrade.lean, Tests/Mux.lean, StreamError.lean, and the four package doc sets. The diffs against the tip in the five packages reduce to one deliberate exception and to trivia:

• The host keeps this branch's upgrader. Host/Swarm.lean, Policy.lean, and Error.lean stay at the pre-merge versions, and the branch's negotiate survives as Libp2p.Negotiate.Legacy (five files, 1645 lines). I compared the Legacy blobs against d1c1ab3: the content is byte-equal to this branch's reviewed negotiate, modulo the namespace rename. The author discloses the reason in the comment and the body: the tip's Host.Mock.Negotiate throws pending issue [SEAM] W5.6 host: the mock connections of #61 #70, and a build resolved fully on the tip exits at participant startup. The tip's own Tests/Host.lean skips its swarm legs for the same reason, so the tip's host cannot run a real upgrade today. The gate needs a working upgrader, the exception is disclosed, the code is reviewed branch code, and the removal rides on [SEAM] W5.6 host: the mock connections of #61 #70. I accept this as the resolution of that seam, and I record it: the host negotiate seam stays branch-side until [SEAM] W5.6 host: the mock connections of #61 #70 lands.
• Host/Dedup.lean and Registry.lean differed from the tip by a trailing newline each, Mux.lean carried a duplicate import Libp2p.Mux.Yamux, and ReqResp/Limiter.lean and Payload.lean carried an unused import Libp2p.Protocols.Mock.Core. My nit commit cleans all five.

The tip moved after the push: hackathon26 gained PR #60 (W5.9, the transport-interop harness) as 571fa6a at 08:24 UTC, against a head pushed near 06:57 UTC. The demand named 6a1f832, and the branch carries it. The next sync pulls #60.

Mock state

The gossipsub modules import no mock. GossipsubSession.lean converts the mock-typed identify and ping handlers through one adapter, toCoreHandler; the body discloses it and ties it to issue #55. The four Protocols/Mock files (Core, Host, HostStream, Muxer) match the tip's set exactly. Host/Mock/Negotiate.lean is gone from the branch; the tip still carries it, which follows from the host exception above. The tip's new cli/Interop/Mock/Stack.lean comes with #60 and lands with the next sync.

The run record

The body now names head 7ac636a89f5e207a2a6785320d4ff661c7f50093 in full and calls the two cells the 3c gate runs; the "rehearsal" hedge is gone. The cells: Go and Lean, seed 1, reach 1.0; Rust and Lean, seed 1, reach 1.0; 32 nodes on subnet-blob-msg. That satisfies the plan's W6.4 gate row as the last round scoped it. The SHA chain checks out: the head SHA resolves on the fork and on this PR. The body also records the executable's SHA-256 file digest and relabels the old cc4a74ae as the digest of the 407878c build, which explains why it resolved to no ref. A file digest is not reproducible on a foreign host, because Lean binaries embed build paths; my rebuild's digest differs, and I take the head SHA as the verifiable link, which is what the demand asked for.

Checks

I ran the gates at 7ac636a8 and again at b3c76b3 after the nit commit. The numbers below are the second run.

• lake build --wfail: 286 jobs, zero warnings.
• lake test: 27715 passed, 0 failed, 10 skipped. The skips are pre-existing.
• lake test -- +RTS -N1 -RTS: the same summary.
• scripts/lint-imports.sh: 185 module files, 0 violations.

Every number matches the author's claims in the comment and the body.

The axiom audit

I ran #print axioms over 31 public names: 15 of the adapter suite (parseScript, toCoreParams, parseHosts, recordLine, plan, messageIdString, paddedPayload, peerSeed, prepareScript, receivedMessageLine, parseGossipSubParams, instructionForNode, msgIdFn, waitComplete, validWindow) and 16 of the participant (runScript, publishPayload, identityForNode, paramsPath, rpcTraceSummary, receivedRecord, traceInbound, traceOutbound, formatObservationTime, DelayTable.batchDelay, ReceiptObserver.onRpc, toCoreHandler, yamuxMuxer, GossipsubSession.start, Cli.load, Cli.run). Every name reduces to propext, Classical.choice, and Quot.sound, or to no axiom. No sorryAx appears, and the merge adds no axiom.

Nits fixed

One commit, b3c76b3, pushed to the fork with the lease:

• Mux.lean: dropped the duplicate import Libp2p.Mux.Yamux.
• ReqResp/Limiter.lean and Payload.lean: dropped the unused import Libp2p.Protocols.Mock.Core.
• Host/Dedup.lean and Host/Registry.lean: took the tip's bytes; the only delta was a trailing newline.

Tests/Host.lean, Tests/Negotiate.lean, Tests/Noise.lean, and Tests/Interop/Noise.lean still differ from the tip by a trailing newline each, and Swarm.lean, Policy.lean, and Error.lean keep the branch's frozen form until #70. I leave both to the next sync.

What remains

Nothing of the three demands. The merge landed on the reviewed seam versions with one disclosed exception tied to issue #70. The gates are green on the merged head. The run evidence carries a verifiable head SHA and both cells at reach 1.0. The host exception and the identify adapter leave with #70 and #55.

APPROVE

[leolara]

Merge-loop note. The verdict demanded one tip merge on the reviewed seam versions; the author's push brought tip 6a1f832, and this merge adds the new tip 571fa6a (#60, the only move since). One conflict, the Cli library in lakefile.toml, resolved as the union: the four roots of both sides with the interop executable kept. Gates on the new head b320e07: lake build --wfail (289 jobs), lake test (27786 passed, 0 failed, the 10 named skips), the same under +RTS -N1 -RTS, and scripts/lint-imports.sh (191 modules, 0 violations). The APPROVE stands; the recorded interop runs predate this tip merge by one harness merge with no gossipsub change, and the cells re-run at matrix time per the plan.