[IvanAnishchuk]

Summary

PR #40 merged with Negotiate.Mock.Core, a copy of the W5.2 surface. W5.2 merged in #64, so the negotiate package takes its seam types from libp2p/core and the mock goes. Two rules of the real seam change the upgrader, and this PR applies them: the muxer negotiation reads the handshake's over-read bytes through the secure read, and the upgrader joins the SecureConn it owns. Closes #53.

What changed

libp2p/negotiate:

• Constants.lean, Message.lean, and Step.lean name Core.ProtocolId and Core.Role from libp2p/core.
• Upgrade.lean imports Libp2p.Core and takes the real SecurityProtocol, SecureConn, Muxer, and MuxSession:
  • The muxer negotiation runs over sc.toConnection with an empty seed. The real SecureConn delivers the bytes its handshake over-read through read, and the core pair says no stage above read takes SecureConn.leftover ("The leftover hand-over"). For Noise those bytes are ciphertext.
  • The upgrader owns the SecureConn (core contract 4). The frozen answer stays (MuxSession × PeerId); the answered session's join waits for the session loop, then for the secure connection (ownSecure). The secure connection is joined even when the session's join throws.
  • Every failure after the handshake (identity check, muxer negotiation, muxer lookup, Muxer.open) closes the secure connection and joins it (discardSecure).
  • A session that opens as the deadline fires: releaseLate closes it and gives its join to a task set that upgradeWith joins before it answers.
• Mock/Core.lean is deleted. The root module doc and Constants.lean lose their mock sentences.
• The package ARCHITECTURE: contract 5 says how the handshake's bytes reach the muxer negotiation, and the upgrade bullet states the ownership of the secure connection.

Tests:

• Tests/Upgrade.lean: the two plaintext security values build their SecureConn through secureOf, whose read delivers the over-read bytes first, as the real seam does. The test muxer's openStream takes the id. The full and split pipeline checks join both sessions and check that the joins answer .ok (two new checks).
• Tests/Negotiate.lean names Libp2p.Core.ProtocolId.

Test plan

• lake build --wfail is green, with no warning.
• lake test passes: 27171 passed, 0 failed, 10 skipped. It passes again with LEAN_NUM_THREADS=1.
• Stress at 4 workers: 3 of about 132 plain runs hung, from the yamux test race that test(yamux): wait for the pong deadline before the clock moves #83 fixes (see the note below); 190 runs with LEANP2P_TRACE passed.
• The import-rule lint is green: 162 modules, 0 violations.

Risk / trust footprint

None added or removed. #print axioms over the 44 package theorems and upgrade shows propext, Classical.choice, and Quot.sound at most.

Notes for reviewers

• An intermittent hang in the test binary, found while testing this PR and unrelated to it. About 1 run in 45 parked forever at 4 workers. The cause is the keepalive check of the yamux suite, which advanced the test clock before the pong timer was armed. It hangs on hackathon26 as well. The fix is test(yamux): wait for the pong deadline before the clock moves #83.
• The ledger row for PR feat(negotiate): W5.5, multistream-select and the upgrader #40 on [TRACKING] Machine-Checked Devcon Week: the task tree #25 can be struck when this merges.
• This unblocks the negotiate swap of the host ([SEAM] W5.6 host: the mock connections of #61 #70, after PR refactor(host): take the seam types from libp2p/core #80): the host can then hand the real Noise and muxer values to Negotiate.upgrade.

LICENSE (LGPL version 3)

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

[leolara]

Re-review of the seam swap at 8f395b3.

The base moved; the rebase was clean. The tip gained PR #79 (the security seam swap) after the push, so I rebased the branch onto hackathon26 at 8a34d57. No conflict. The rebased head is 8f395b3; the negotiate package content is byte-identical to the pushed head apart from the parent.

The overage, on record. The core mock window closed at 19:21:56 UTC on 7 Nov (PR #64 merged at 07:21:56 UTC). The swap commit landed at 08:41:42 UTC on 8 Nov, about 13 hours late. The swap is complete, so per the organiser ruling this stays an approval, with the overage recorded here.

Issue #53 is done. Negotiate/Mock/Core.lean is deleted. A repo-wide grep finds zero Negotiate.Mock references in code and prose. Constants.lean, Message.lean, and Step.lean name Core.ProtocolId and Core.Role; Upgrade.lean imports Libp2p.Core. The remaining core mocks in host, mux, and protocols belong to #80, #77, and #81, outside this issue's scope. The skip reason names #76 and #77 correctly; #76 is closed by #79 and #77 is open with PR #84 in flight.

Semantic change 1: the muxer negotiation reads the over-read bytes through read. upgradeCore negotiates over sc.toConnection with an .empty seed (Upgrade.lean:537-539), which follows the core pair's rule: SecureConn.read delivers the handshake's leftover decrypted, before any connection byte, and no stage above read takes the field. The tests pin both sides of the rule. secureOf (Tests/Upgrade.lean:105-122) builds the SecureConn the seam way: one read hands out the front, then every read goes to the connection, and leftover records the same bytes. checkHandshakeLeftover over-reads the muxer header in the handshake and asserts Muxer.open receives ByteArray.empty (Tests/Upgrade.lean:330-334). checkMuxOpenLeftover still pins the third boundary: the bytes the muxer negotiation itself over-reads reach Muxer.open as data.

Semantic change 2: the upgrader owns the SecureConn. I verified every path by hand.

• The four post-handshake failures (identity check, muxer negotiation, muxer lookup, Muxer.open) each call discardSecure before the answer (Upgrade.lean:532, 540, 544, 548). discardSecure (Upgrade.lean:495-497) closes the secure connection, then awaits its join. checkIdentityMismatch pins the close side: the dialer answers authentication, neither muxer runs, and the responder's parked negotiation ends with .closed (Tests/Upgrade.lean:439-444).
• The answered session carries the join: ownSecure (Upgrade.lean:503-511) runs the session join with the fault caught, then runs sc.join unconditionally, and the first failure wins. Both pipeline checks now run the joins and assert .ok (Tests/Upgrade.lean:249-251, 832-834).
• The deadline race: releaseLate (Upgrade.lean:561-567) closes the late session and hands its wrapped join to the late task set. upgradeWith joins the set before it settles the answer, on the success path and the failure path (Upgrade.lean:584). No caller can receive a session whose tasks are unowned.
• No path cancels a task, no path reads-then-writes a bare ref, and every spawn sits in a joined set. The boundary close and the session close are both idempotent, so the race cannot double-close.

One observation, for the record: releaseLate's .ok arm has no deterministic test. The boundary hook closes the connection at expiry, so a session that answers .ok after the timer won sits in a genuine race window, and the suite cannot force it through the Clock seam alone. PR #40 carried the same gap, and this PR only widens that arm with the join hand-off. The construction is the right one; the coverage is an accepted limit.

Strictness. No sorry, no partial def, no native_decide, no unsafe, no @[extern], no declared axiom in the package or the two suites. set_option autoImplicit false sits in all four package modules.

Axiom audit. I ran #print axioms over 43 public theorems and the three seam values (Negotiate.upgrade, Negotiate.upgradeWith, Negotiate.negotiate). Every report lists propext, Classical.choice, and Quot.sound only. No sorryAx, no mock axiom. This matches the body.

Gates at 8f395b3, exact output.

• lake build --wfail: Build completed successfully (254 jobs), no warning.
• lake test: 27171 passed, 0 failed, 10 skipped.
• lake test -- +RTS -N1 -RTS: the same summary.
• scripts/lint-imports.sh: 161 module files, 0 violations.

The body says 162 modules for the lint. That number belongs to the pre-rebase base; PR #79 dropped a module, and the rebased head measures 161.

The body's note about the intermittent hang matches #83, which is unrelated to this PR and open.

Ledger. The row for PR #40 on issue #25 can be struck when this merges, as the body asks. Issue #53 closes with this head.

APPROVE