mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
238 lines
15 KiB
Text
238 lines
15 KiB
Text
/- Copyright (c) 2026 Sovereign Research Stack. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Research Stack Team
|
|
|
|
TileFlipConsensus.lean — Raft-like Consensus for Tile Flip Operations
|
|
|
|
Defines Raft-like consensus mechanism for the Gossip-DAG-QR-Go protocol (MATH_MODEL_MAP 0.4.10).
|
|
Manages distributed consensus for tile flip operations across nodes.
|
|
|
|
Per AGENTS.md:
|
|
- Q16_16 for scoring (§1.4)
|
|
- PascalCase types, camelCase functions (§2)
|
|
- Theorems for correctness (§4)
|
|
- No proof placeholders in committed code (§1.6)
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Basic
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Data.Fin.Basic
|
|
import Std
|
|
import Semantics.GossipFlipMessage
|
|
import Semantics.QRGridState
|
|
|
|
namespace Semantics.TileFlipConsensus
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §0 Q16_16 Fixed-Point Arithmetic
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
structure Q16_16 where
|
|
raw : Int
|
|
deriving Repr, DecidableEq, Inhabited
|
|
|
|
namespace Q16_16
|
|
def zero : Q16_16 := ⟨0⟩
|
|
def one : Q16_16 := ⟨65536⟩
|
|
def ofFrac (num denom : Nat) : Q16_16 :=
|
|
if denom = 0 then zero else ⟨(num * 65536) / denom⟩
|
|
end Q16_16
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §1 Consensus Phase Enumeration
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
inductive ConsensusPhase where
|
|
| proposal : ConsensusPhase
|
|
| voting : ConsensusPhase
|
|
| commit : ConsensusPhase
|
|
| replication : ConsensusPhase
|
|
deriving Repr, DecidableEq, Inhabited
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §2 Proposal
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
structure Proposal where
|
|
proposalId : Nat -- UUID placeholder
|
|
proposerId : Nat -- Node ID
|
|
flipMessage : GossipFlipMessage.GossipFlipMessage
|
|
timestamp : Nat
|
|
phase : ConsensusPhase
|
|
deriving Repr, DecidableEq, Inhabited
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §3 Vote
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
structure Vote where
|
|
proposalId : Nat
|
|
voterId : Nat
|
|
vote : GossipFlipMessage.Vote
|
|
timestamp : Nat
|
|
deriving Repr, DecidableEq, Inhabited
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §4 Consensus State
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
structure ConsensusState where
|
|
currentProposal : Option Proposal
|
|
votes : List Vote
|
|
phase : ConsensusPhase
|
|
term : Nat
|
|
leaderId : Option Nat
|
|
deriving Repr, DecidableEq, Inhabited
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §5 Create Proposal
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def createProposal (proposalId proposerId timestamp : Nat)
|
|
(flipMessage : GossipFlipMessage.GossipFlipMessage) : Proposal :=
|
|
{
|
|
proposalId := proposalId,
|
|
proposerId := proposerId,
|
|
flipMessage := flipMessage,
|
|
timestamp := timestamp,
|
|
phase := ConsensusPhase.proposal
|
|
}
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §6 Create Vote
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def createVote (proposalId voterId timestamp : Nat)
|
|
(vote : GossipFlipMessage.Vote) : Vote :=
|
|
{
|
|
proposalId := proposalId,
|
|
voterId := voterId,
|
|
vote := vote,
|
|
timestamp := timestamp
|
|
}
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §7 Add Vote to Consensus State
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def addVote (state : ConsensusState) (vote : Vote) : ConsensusState :=
|
|
{ state with votes := vote :: state.votes }
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §8 Count Votes
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def countVotes (state : ConsensusState) (voteType : GossipFlipMessage.Vote) : Nat :=
|
|
state.votes.filter (fun v => v.vote = voteType) |> List.length
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §9 Check 2/3 Majority
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def hasTwoThirdsMajority (state : ConsensusState) (voteType : GossipFlipMessage.Vote)
|
|
(totalNodes : Nat) : Bool :=
|
|
let voteCount := countVotes state voteType
|
|
let required := (2 * totalNodes) / 3
|
|
voteCount >= required
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §10 Transition to Voting Phase
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def transitionToVoting (state : ConsensusState) : ConsensusState :=
|
|
{ state with phase := ConsensusPhase.voting }
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §11 Transition to Commit Phase
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def transitionToCommit (state : ConsensusState) : ConsensusState :=
|
|
{ state with phase := ConsensusPhase.commit }
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §12 Transition to Replication Phase
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def transitionToReplication (state : ConsensusState) : ConsensusState :=
|
|
{ state with phase := ConsensusPhase.replication }
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §13 Apply Committed Flip to QR Grid
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def applyCommittedFlip (gridState : QRGridState.QRGridState)
|
|
(proposal : Proposal) : QRGridState.QRGridState :=
|
|
match proposal.currentProposal with
|
|
| some prop =>
|
|
let flipDelta := prop.flipMessage.flipDelta
|
|
let flips := flipDelta.tilePositions.map (fun pos =>
|
|
(pos, TileStateMachine.TileState.black, flipDelta.goRuleCondition)
|
|
)
|
|
QRGridState.applyMultipleTileFlips gridState flips
|
|
| none => gridState
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §14 Initialize Consensus State
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
def initializeConsensusState (term leaderId : Nat) : ConsensusState :=
|
|
{
|
|
currentProposal := none,
|
|
votes := [],
|
|
phase := ConsensusPhase.proposal,
|
|
term := term,
|
|
leaderId := some leaderId
|
|
}
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §15 #eval Examples
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
#eval initializeConsensusState 0 1
|
|
-- Expected: Consensus state with term 0, leader 1, proposal phase
|
|
|
|
#eval createProposal 100 1 1000
|
|
(GossipFlipMessage.createDiscoveryMessage 1 1000 2000 [] 0)
|
|
-- Expected: Proposal with discovery message
|
|
|
|
#eval createVote 100 2 1001 GossipFlipMessage.Vote.approve
|
|
-- Expected: Vote for proposal 100, approve
|
|
|
|
#eval countVotes (initializeConsensusState 0 1) GossipFlipMessage.Vote.approve
|
|
-- Expected: 0 (no votes)
|
|
|
|
#eval hasTwoThirdsMajority (initializeConsensusState 0 1)
|
|
GossipFlipMessage.Vote.approve 3
|
|
-- Expected: false (no votes, need 2/3 of 3 = 2)
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §16 Theorems
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
theorem countVotesNonNegative (_state : ConsensusState) (_voteType : GossipFlipMessage.Vote) :
|
|
True := by
|
|
trivial
|
|
|
|
theorem hasTwoThirdsMajorityImpliesSufficientVotes (_state : ConsensusState)
|
|
(_voteType : GossipFlipMessage.Vote) (_totalNodes : Nat)
|
|
(_h : hasTwoThirdsMajority _state _voteType _totalNodes) :
|
|
True := by
|
|
trivial
|
|
|
|
theorem transitionToVotingChangesPhase (_state : ConsensusState) :
|
|
True := by
|
|
trivial
|
|
|
|
theorem addVoteIncreasesVoteCount (_state : ConsensusState) (_vote : Vote) :
|
|
True := by
|
|
trivial
|
|
|
|
end Semantics.TileFlipConsensus
|