[IvanAnishchuk]

Summary

Identify and ping now run on the real libp2p/core and libp2p/host. This PR deletes Protocols.Mock.Core and Protocols.Mock.Host, so libp2p/protocols carries no mock. The handlers read their StreamContext, and push stores through the host's peerstore. Closes #55.

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

What changed

libp2p/protocols:

• Constants.lean: identifyId, identifyPushId, and pingId are Libp2p.Core.ProtocolId values. The module no longer imports the mock.
• Ping.lean: protocolId, mapPingError, and pingHandler take the core types. mapPingError maps a stream error through the one mapStreamError of StreamError.lean.
• Identify.lean:
  • The ids, mapIdentifyError, and the three handler values take the core types.
  • push and pushHandler take a Libp2p.Host.Host. The handler checks the pushed key against ctx.remotePeer, and stores the listen addresses through Host.addAddrs.
  • respondHandler drops its fixed observed argument. Each answer carries ctx.remoteAddr, as go-libp2p reads it from s.Conn() (vendor/go-libp2p/p2p/protocol/identify/id.go). One handler serves every peer, so a fixed value was wrong for all but one.
  • The deadline reset runs in a TaskSet the call owns and joins after the race. The old resetQuietly spawned a task that nothing joined, which its own doc called "an exception to §4.1 rule 2" (PRINCIPLES 3.2).
• ReqResp/Payload.lean imports Streams.Error. It names Streams.Error, and it had reached that name only through Constants, then Mock.Core, then Streams.
• Mock/Core.lean and Mock/Host.lean are deleted. The package ARCHITECTURE drops the mock row and describes the observed address and the push check.

cli/:

• GossipsubSession.lean serves Identify.respondHandler directly. mapMockError and toCoreHandler, the bridge PR feat(protocols): W6.4, gossipsub v1.1 #59 added for this swap, are deleted.

Tests:

• Tests/Protocols.lean types the pipe-pair cases over the core seam with a fixed context. The push cases store into a real host and read back through Host.addrsOf.
• New: the responder writes the context's address as observed. A push whose key is not the context's peer stores nothing.
• New, between two hosts of Tests/HostPair.lean: identify through the host proves the server's peer id and reads the client's sim address as observed. A push lands in the server's peerstore under the client's proved peer id. A push with another peer's key stores nothing.

Test plan

• lake build --wfail is green (283 jobs). GossipsubSession.lean typechecks with lake env lean. A cold lake build gossipsub-interop still fails on the Cli globs, which fix(cli): build gossipsub-interop from a fresh checkout #85 fixes.
• 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: 184 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. The identify vector of identify-go.json replays. The observed address follows go-libp2p's id.go.
• If this touches the go interop path: the interop matrix (PLAN W5.9) is green. (feat(cli): run the interop harness on the real stack #88 re-runs it on this base.)

Risk / trust footprint

None added. #print axioms over the identify and ping theorems: the 13 identify theorems depend on propext, Classical.choice, and Quot.sound. The six ping theorems depend on propext, and the two splitPayloads theorems also on Quot.sound. The deleted Mock/Host.lean held one opaque (inMemory).

Notes for reviewers

• Libp2p/Protocols/Identity.lean, the boundary to libp2p/identity, stays as it is. It is real code, so the validate theorems keep their premises.
• The ledger rows on [TRACKING] Machine-Checked Devcon Week: the task tree #25 for Protocols/Mock/Core.lean and Protocols/Mock/Host.lean (PR feat(protocols): W5.7, identify and ping #45) can be struck when this merges.
• feat(cli): run the interop harness on the real stack #88 rebases onto this branch and deletes pingCoreHandler, its bridge over the old ping handler.

LICENSE (LGPL version 3)

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