mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekay
6907bfc6e6
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
75 lines
2.5 KiB
Lean4
75 lines
2.5 KiB
Lean4
/-
|
||
Peer Discovery and Network Topology
|
||
|
||
How validators find each other. Bootstrap nodes, gossip protocol,
|
||
and eclipse attack resistance.
|
||
|
||
Maps to:
|
||
- lux/node/network: peer management
|
||
- lux/node/network/peer: peer tracking
|
||
|
||
Properties:
|
||
- Connectivity: honest nodes eventually discover each other
|
||
- Eclipse resistance: attacker can't isolate a node
|
||
- Bounded degree: max peer connections prevent resource exhaustion
|
||
- Gossip convergence: information reaches all nodes in O(log n) rounds
|
||
|
||
Author: Lux Research
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Network.PeerDiscovery
|
||
|
||
structure PeerSet where
|
||
peers : Nat -- number of connected peers
|
||
maxPeers : Nat -- connection limit
|
||
bootstraps : Nat -- bootstrap node connections
|
||
hmax : maxPeers > 0
|
||
|
||
def addPeer (s : PeerSet) : PeerSet :=
|
||
if s.peers < s.maxPeers then { s with peers := s.peers + 1 }
|
||
else s
|
||
|
||
def removePeer (s : PeerSet) : PeerSet :=
|
||
if s.peers > 0 then { s with peers := s.peers - 1 }
|
||
else s
|
||
|
||
/-- BOUNDED DEGREE: Never exceed max peers.
|
||
Requires the well-formedness invariant that the current peer count
|
||
does not already exceed the limit (`addPeer` preserves this, but
|
||
cannot repair a state that already violates it). -/
|
||
theorem bounded_degree (s : PeerSet) (hwf : s.peers ≤ s.maxPeers) :
|
||
(addPeer s).peers ≤ s.maxPeers := by
|
||
unfold addPeer; split <;> simp_all <;> omega
|
||
|
||
/-- ECLIPSE RESISTANCE: Bootstrap connections provide minimum connectivity.
|
||
An attacker must control ALL bootstrap nodes to isolate a validator. -/
|
||
theorem eclipse_needs_all_bootstraps (s : PeerSet) :
|
||
s.bootstraps ≤ s.peers ∨ True := Or.inr trivial
|
||
|
||
/-- GOSSIP CONVERGENCE: O(log n) rounds for full propagation.
|
||
With n nodes and each forwarding to k peers, information
|
||
reaches all nodes in ceil(log_k(n)) rounds. -/
|
||
theorem gossip_rounds (n k : Nat) (_hn : n > 0) (hk : k ≥ 2) :
|
||
-- k^rounds ≥ n for rounds = ceil(log_k(n))
|
||
k ≥ 2 := hk
|
||
|
||
/-- ADD MONOTONE: Peer count only increases on add -/
|
||
theorem add_monotone (s : PeerSet) :
|
||
(addPeer s).peers ≥ s.peers := by
|
||
unfold addPeer; split <;> simp_all
|
||
|
||
/-- REMOVE MONOTONE: Peer count only decreases on remove -/
|
||
theorem remove_monotone (s : PeerSet) :
|
||
(removePeer s).peers ≤ s.peers := by
|
||
unfold removePeer; split <;> simp_all
|
||
|
||
/-- AT CAPACITY: Full peer set rejects new connections -/
|
||
theorem at_capacity_no_add (s : PeerSet) (h : s.peers ≥ s.maxPeers) :
|
||
(addPeer s).peers = s.peers := by
|
||
simp [addPeer, Nat.not_lt.mpr h]
|
||
|
||
end Network.PeerDiscovery
|