[IvanAnishchuk]

Summary

PR #61 merged with two own mocks. This PR drops the first, Host.Mock.Core, now that W5.2 merged in #64. The second, Host.Mock.Negotiate, cannot go yet: the merged negotiate package types its upgrader over its own core mock (issue #53), so the host cannot hand it real seam values. Part of #70.

What changed

libp2p/host:

• Error, Registry, Dedup, Policy, and Swarm import Libp2p.Core (or the one submodule they need) in place of the mock. The real types match the mock field for field; Role and Error add a Hashable instance, which the host does not use.
• Mock/Core.lean is deleted.
• Mock/Negotiate.lean names the real core types. Its module doc says why it stays, and that the swap is a retype: the merged upgrader takes no admit checkpoint and exports no negotiateStream.
• The package ARCHITECTURE section "The mock" and the module row describe the one mock left. The PLAN says the unit 1b code builds over the real core and identity.

Tests:

• Tests/Host.lean opens Libp2p.Core. Its module doc and the skip reason of the unit 1b legs name the swaps they wait on: [SEAM] W5.5 negotiate: drop the stale varint and streams mocks inside #40 #53, [SEAM] W5.3 security/noise: drop the core mock after PR #69 #76 (PR refactor(security): take the seam types from libp2p/core #79), [SEAM] W5.4 mux: drop the core mock and land Mux.yamux after PR #49 #77, and the rest of [SEAM] W5.6 host: the mock connections of #61 #70.

Test plan

• lake build --wfail is green.
• lake test passes: 27169 passed, 0 failed, 10 skipped. It passes again with LEAN_NUM_THREADS=1.
• Stress: the test binary passes 10 of 10 runs at 4 workers, each under a 300 s timeout.
• The import-rule lint is green: 162 modules, 0 violations.

Risk / trust footprint

None added or removed. #print axioms over the package theorems:

Libp2p.Host.raceLoserAgree  [propext, Classical.choice, Quot.sound]
Libp2p.Host.dedupEmpty      [propext, Classical.choice, Quot.sound]
Libp2p.Host.dedupDead       [propext, Classical.choice, Quot.sound]
Libp2p.Host.dedupKeepTable  [propext, Classical.choice, Quot.sound]

Notes for reviewers

• The Host.Mock.Core row for PR feat(host): W5.6, the host with dedup, serving, and shutdown #61 on [TRACKING] Machine-Checked Devcon Week: the task tree #25 can be struck when this merges. The Host.Mock.Negotiate row stays open.
• The order of the remaining work: [SEAM] W5.5 negotiate: drop the stale varint and streams mocks inside #40 #53 retypes negotiate over the real core, then this package swaps its negotiate mock, then the unit 1b legs run with the Noise value of refactor(security): take the seam types from libp2p/core #79 and the Mux.yamux value of [SEAM] W5.4 mux: drop the core mock and land Mux.yamux after PR #49 #77.

LICENSE (LGPL version 3)

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

[leolara]

Review at head 34da9b1 (was a11b24c7), rebased onto the tip 244b2d1.

The rebase

The tip carried #79, #82, #84, and #83 since the branch was cut. The
rebase was clean: #82 touched only packages/libp2p/negotiate, and the
host diff between the old and new heads is empty, so the reviewed
content reappears byte for byte.

The core swap

Mock/Core.lean is gone, and no importer remains. A grep over the tree
finds only Libp2p.Protocols.Mock.Core, the protocols package's own
mock, which follows its seam issue. Seven modules and the suite now
take the real types (Dedup.lean:2, Error.lean:3, Policy.lean:1,
Registry.lean:3, Swarm.lean:5, Mock/Negotiate.lean:4,
Tests/Host.lean:32).

I compared the real core with the deleted mock field for field:
ProtocolId, Error, Role, SecureConn, SecurityProtocol,
MuxSession, Muxer, StreamContext, StreamHandler, and the six
policy shapes match. The real Role and Error add a Hashable
instance, as the body says, and the host uses neither. The error arms
map cleanly: Error.toCore sends closed to .closed and the other
two arms to .protocol (Mock/Negotiate.lean:52), and the swarm and
policy modules compile against the real Core.Error with no behavior
drift. The unit 1a checks pass with the same counts as at #61.

Mock/Negotiate.lean stays, and it is retyped over the real core. Its
module doc states why it stays (Mock/Negotiate.lean:9) and that the
swap is a retype (:16), the shape issue #70 fixes for its second row.

The nit I fixed

The #82 rebase staled four prose spots: they named #53, #76, and #77
as pending, and all three closed on 9 November. One commit (34da9b1)
brings them to the current tree:

• Mock/Negotiate.lean:9 states the stay as the host swap of [SEAM] W5.6 host: the mock connections of #61 #70, and
  :22 cites the core ARCHITECTURE for the policy shapes, where the
  text cited the deleted core mock.
• Swarm.lean:72 names [SEAM] W5.6 host: the mock connections of #61 #70 as the reason the mock stays.
• The package ARCHITECTURE keeps "The mock" truthful
  (docs/ARCHITECTURE.md:27, :303), and the unit 1b paragraph drops
  the closed [SEAM] W5.3 security/noise: drop the core mock after PR #69 #76 and [SEAM] W5.4 mux: drop the core mock and land Mux.yamux after PR #49 #77 as pending (:314).
• Tests/Host.lean:22 and the skip reason at :303 name only the
  remaining blocker, the host swap of [SEAM] W5.6 host: the mock connections of #61 #70.

The overage

Overage on record: the core-mock window closed at 19:22 UTC on
7 November, and the swap opened at 06:35 UTC on 8 November, about
11 hours late.

Gates

• lake build --wfail: green, 252 jobs, no warnings.
• lake test: 27189 passed, 0 failed, 10 skipped.
• lake test -- +RTS -N1 -RTS: the same counts.
• scripts/lint-imports.sh: 159 modules, 0 violations.

#print axioms over raceLoserAgree, dedupEmpty, dedupDead,
dedupKeepTable, and the four policy seam values
(Policy.permissiveGater, denyingGater, unlimited, keepOrder)
shows propext, Classical.choice, Quot.sound only. No sorryAx,
no mock axiom.

Merge order

The PR merges now. The second part of #70, the negotiate retype of the
host, follows it and closes the issue. The Host.Mock.Core row for
PR #61 on #25 can be struck at merge.

APPROVE