Skip to content

feat(cli): run the interop harness on the real stack - #88

Open
IvanAnishchuk wants to merge 7 commits into
etheorem:hackathon26from
IvanAnishchuk:seam-interop-stack
Open

feat(cli): run the interop harness on the real stack#88
IvanAnishchuk wants to merge 7 commits into
etheorem:hackathon26from
IvanAnishchuk:seam-interop-stack

Conversation

@IvanAnishchuk

@IvanAnishchuk IvanAnishchuk commented Nov 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

The transport-interop harness now runs on the real stack, and the W5.9 matrix is green against go-libp2p v0.50.0: both dial directions, lean with lean, the silent peer, and the slow reader. This PR deletes Interop/Mock/Stack.lean. Closes #73.

This PR stacks on #86 (the host on the real negotiate), #87 (the req/resp mocks), and #89 (identify and ping on the real core and host). Until those merge, the diff also shows their commits. Review the last commit, feat(cli): ….

What changed

cli/:

  • Interop.lean imports the real packages. startHost builds an Ed25519 identity, Noise.Config.generate for the static key, Mux.yamux, and Libp2p.Host with TCP and Ping.pingHandler. The dialer opens its stream for Ping.protocolId.
  • muxer=mplex still parses, as a name of the test plan. libp2p/mux holds no mplex value (P2, the mux PLAN, unit 2), so the host start refuses it, and the run exits nonzero. The Config.lean doc called mplex "the second Muxer value", which is false on this tip, and now says the above.
  • Interop/Mock/Stack.lean is deleted. The cli ARCHITECTURE replaces "The mock" with "The stack", and drops the module row.

Test plan

  • lake build --wfail interop is green (329 jobs).
  • lake test passes: 27832 passed, 0 failed, 4 skipped. It passes again with LEAN_NUM_THREADS=1.
  • Stress: the test binary passes 8 of 8 runs at 4 workers, each under a 600 s timeout.
  • The import-rule lint is green: 183 modules, 0 violations.
  • A new codec or framing layer comes with its round-trip theorem or property test, and with a test for its length cap. (n/a: no new codec)
  • If this touches wire behavior: the captured vectors still pass, and the description names the spec section the change follows. (n/a: no wire code changes)
  • If this touches the go interop path: the interop matrix (PLAN W5.9) is green. scripts/interop-matrix.sh, binary SHA-256 cc33582966bd36c8c2377ea029e0bbf1784da5deb77b827886e7c593fdcaf039:
Cell Record
go x go (tcp, noise, yamux) {"handshakePlusOneRTTMillis":6.579,"pingRTTMilllis":0.217}
lean x go {"handshakePlusOneRTTMillis":49.061,"pingRTTMilllis":0.973}
go x lean {"handshakePlusOneRTTMillis":138.545,"pingRTTMilllis":0.982}
lean x lean {"handshakePlusOneRTTMillis":52.583,"pingRTTMilllis":2.580}
silent-peer (closed after 30 s, go dialer passed meanwhile) {"handshakePlusOneRTTMillis":136.802,"pingRTTMilllis":0.853}
slow-reader {"stalledAfterBytes":524224,"pingRTTMillis":12.417}

Risk / trust footprint

None added or removed. The deleted mock held eleven opaque declarations and no axiom.

Notes for reviewers

LICENSE (LGPL version 3)

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

@IvanAnishchuk
refactor(host): run the upgrade and stream selection on the real nego…
87a8abb 
…tiate

The host builds its upgrade from the public stages of libp2p/negotiate.
The secured checkpoint sits between the handshake and the muxer stage,
where the core seam puts it. Stream selection is a host shell over the
pure negotiate core. This commit deletes the Negotiate.Legacy copy, and
the unit 1b host legs now run.

Part of etheorem#70.
This was referenced Nov 10, 2026
Closed
Open
@IvanAnishchuk
test(host): run the unit 1b legs on the fixed-key Noise value
da08cf0 
Root ARCHITECTURE §3.1 says every suite above the transport runs on the
test values, and the Noise test value has fixed keys. The host legs used
Noise.securityProtocol, whose ephemeral keys come from Rng.system. Each
suite host now takes Noise.fixedKeyProtocol, seeded from its identity
byte. The host PLAN offered the production value as an option, and now
names the test value only.

Part of etheorem#70.
@IvanAnishchuk
test(protocols): run the req/resp sim checks between two real hosts
c1fa46b 
The sim checks of the req/resp suite now run between two hosts with
Noise and yamux. Tests/HostPair.lean builds the pair. The requester
opens its stream through the host's newStream. This commit deletes
Protocols.Mock.Muxer and Protocols.Mock.HostStream.

An id the peer does not serve now fails the open. Multistream-select
answers na, so the stream never opens for that id.

Part of etheorem#78.
@IvanAnishchuk
docs(protocols): drop the stale negotiate-mock sentence of req/resp
5e5374b 
The req/resp section said the host still upgrades through a mock of
libp2p/negotiate, so the suite ran against a mock of the stream call.
etheorem#86 puts the host on the real negotiate, and this branch runs the suite
between two real hosts, so the sentence goes.

Part of etheorem#78.
@IvanAnishchuk
test(protocols): run the host pair on the fixed-key Noise value and a…
0d4c414 
… test clock

Root ARCHITECTURE §3.1 says every suite above the transport runs on the
test values. Tests/HostPair.lean built its hosts with
Noise.securityProtocol and the system clock. Each host now takes
Noise.fixedKeyProtocol, seeded from its identity byte, and both hosts
run on one TestClock that Pair.close closes.

Part of etheorem#78.
@IvanAnishchuk
refactor(protocols): run identify and ping on the real core and host
3234c20 
Identify and ping now type over the seam types of libp2p/core, and this
commit deletes Protocols.Mock.Core and Protocols.Mock.Host. The push
handler checks the pushed key against the peer of its stream's
connection and stores the addresses through the host's peerstore. The
responder writes the connection's remote address as the observed
address, as go reads both from the connection.

The identify deadline reset now runs in a TaskSet the call owns and
joins. The old reset task had no owner.

GossipsubSession serves the identify handler with no bridge.
ReqResp/Payload.lean imports Streams.Error, which it had reached only
through the core mock.

Part of etheorem#55.
@IvanAnishchuk
feat(cli): run the interop harness on the real stack
013e7f5 
The harness composes the identity, TCP, Noise with a generated static
key, yamux, the host, and ping from the real packages. This commit
deletes Interop/Mock/Stack.lean. scripts/interop-matrix.sh passes every
cell: lean and go in both dial directions, lean with lean, the silent
peer, and the slow reader.

libp2p/mux holds no mplex value (P2), so a run with muxer=mplex exits
nonzero at the host start.

Part of etheorem#73.
@IvanAnishchuk IvanAnishchuk mentioned this pull request Nov 10, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

[SEAM] W5.9 interop: connect Interop.Mock.Stack and land the green matrix run inside #60

1 participant

@IvanAnishchuk