/- 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

GossipFlipMessage.lean — Gossip Message Format for QR Tile Flipping

Defines the gossip message format for the Gossip-DAG-QR-Go protocol (MATH_MODEL_MAP 0.4.10).
Gossip messages trigger tile flips in the QR grid, encoding DAG state changes.

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

namespace Semantics.GossipFlipMessage

-- ═══════════════════════════════════════════════════════════════════════════
-- §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  Gossip Message Type Enumeration
-- ═══════════════════════════════════════════════════════════════════════════

inductive GossipMessageType where
  | discovery : GossipMessageType
  | heartbeat : GossipMessageType
  | credentialSync : GossipMessageType
  | replicate : GossipMessageType
  | credentialRotationProposal : GossipMessageType
  deriving Repr, DecidableEq, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §2  Tile Position
-- ═══════════════════════════════════════════════════════════════════════════

structure TilePosition where
  row : Nat
  col : Nat
  deriving Repr, DecidableEq, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §3  Flip Type Enumeration
-- ═══════════════════════════════════════════════════════════════════════════

inductive FlipType where
  | single : FlipType
  | group : FlipType
  | pattern : FlipType
  deriving Repr, DecidableEq, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §4  Go Rule Condition Enumeration
-- ═══════════════════════════════════════════════════════════════════════════

inductive GoRuleCondition where
  | liberty : GoRuleCondition
  | capture : GoRuleCondition
  | ko : GoRuleCondition
  | none : GoRuleCondition
  deriving Repr, DecidableEq, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §5  Flip Delta
-- ═══════════════════════════════════════════════════════════════════════════

structure FlipDelta where
  tilePositions : List TilePosition
  flipType : FlipType
  goRuleCondition : GoRuleCondition
  deriving Repr, DecidableEq, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §6  Gossip Flip Message
-- ═══════════════════════════════════════════════════════════════════════════

structure GossipFlipMessage where
  messageType : GossipMessageType
  nodeId : Nat  -- UUID placeholder
  timestamp : Nat  -- Unix timestamp placeholder
  signature : Nat  -- Ed25519 signature placeholder
  flipDelta : FlipDelta
  qrShapeHash : Nat  -- SHA256 placeholder
  dagVersion : Nat
  deriving Repr, DecidableEq, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §7  Consensus Vote Message
-- ═══════════════════════════════════════════════════════════════════════════

inductive Vote where
  | approve : Vote
  | reject : Vote
  | abstain : Vote
  deriving Repr, DecidableEq, Inhabited

structure ConsensusVoteMessage where
  messageType : Nat  -- consensus_vote placeholder
  nodeId : Nat  -- UUID placeholder
  proposalId : Nat  -- UUID placeholder
  vote : Vote
  timestamp : Nat  -- Unix timestamp placeholder
  signature : Nat  -- Ed25519 signature placeholder
  deriving Repr, DecidableEq, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §8  Message Creation Helpers
-- ═══════════════════════════════════════════════════════════════════════════

def createDiscoveryMessage (nodeId timestamp signature : Nat)
    (tilePositions : List TilePosition) (dagVersion : Nat) : GossipFlipMessage :=
  {
    messageType := GossipMessageType.discovery,
    nodeId := nodeId,
    timestamp := timestamp,
    signature := signature,
    flipDelta := {
      tilePositions := tilePositions,
      flipType := FlipType.single,
      goRuleCondition := GoRuleCondition.liberty
    },
    qrShapeHash := 0,  -- Placeholder
    dagVersion := dagVersion
  }

def createHeartbeatMessage (nodeId timestamp signature : Nat)
    (dagVersion : Nat) : GossipFlipMessage :=
  {
    messageType := GossipMessageType.heartbeat,
    nodeId := nodeId,
    timestamp := timestamp,
    signature := signature,
    flipDelta := {
      tilePositions := [],
      flipType := FlipType.single,
      goRuleCondition := GoRuleCondition.none
    },
    qrShapeHash := 0,  -- Placeholder
    dagVersion := dagVersion
  }

def createCredentialSyncMessage (nodeId timestamp signature : Nat)
    (tilePositions : List TilePosition) (dagVersion : Nat) : GossipFlipMessage :=
  {
    messageType := GossipMessageType.credentialSync,
    nodeId := nodeId,
    timestamp := timestamp,
    signature := signature,
    flipDelta := {
      tilePositions := tilePositions,
      flipType := FlipType.group,
      goRuleCondition := GoRuleCondition.liberty
    },
    qrShapeHash := 0,  -- Placeholder
    dagVersion := dagVersion
  }

def createReplicateMessage (nodeId timestamp signature : Nat)
    (tilePositions : List TilePosition) (dagVersion : Nat) : GossipFlipMessage :=
  {
    messageType := GossipMessageType.replicate,
    nodeId := nodeId,
    timestamp := timestamp,
    signature := signature,
    flipDelta := {
      tilePositions := tilePositions,
      flipType := FlipType.pattern,
      goRuleCondition := GoRuleCondition.none
    },
    qrShapeHash := 0,  -- Placeholder
    dagVersion := dagVersion
  }

def createCredentialRotationProposalMessage (nodeId timestamp signature : Nat)
    (tilePositions : List TilePosition) (dagVersion : Nat) : GossipFlipMessage :=
  {
    messageType := GossipMessageType.credentialRotationProposal,
    nodeId := nodeId,
    timestamp := timestamp,
    signature := signature,
    flipDelta := {
      tilePositions := tilePositions,
      flipType := FlipType.pattern,
      goRuleCondition := GoRuleCondition.ko
    },
    qrShapeHash := 0,  -- Placeholder
    dagVersion := dagVersion
  }

def createConsensusVoteMessage (nodeId proposalId timestamp signature : Nat)
    (vote : Vote) : ConsensusVoteMessage :=
  {
    messageType := 0,  -- consensus_vote placeholder
    nodeId := nodeId,
    proposalId := proposalId,
    vote := vote,
    timestamp := timestamp,
    signature := signature
  }

-- ═══════════════════════════════════════════════════════════════════════════
-- §9  #eval Examples
-- ═══════════════════════════════════════════════════════════════════════════

#eval createDiscoveryMessage 1 1000 2000 [] 0
-- Expected: GossipFlipMessage with discovery type, empty tile positions

#eval createHeartbeatMessage 1 1000 2000 0
-- Expected: GossipFlipMessage with heartbeat type, empty tile positions

#eval createCredentialSyncMessage 1 1000 2000 [{row := 0, col := 0}] 0
-- Expected: GossipFlipMessage with credentialSync type, one tile position

#eval createReplicateMessage 1 1000 2000 [{row := 0, col := 0}] 0
-- Expected: GossipFlipMessage with replicate type, one tile position

#eval createCredentialRotationProposalMessage 1 1000 2000 [{row := 0, col := 0}] 0
-- Expected: GossipFlipMessage with credentialRotationProposal type, one tile position

#eval createConsensusVoteMessage 1 100 2000 2000 Vote.approve
-- Expected: ConsensusVoteMessage with approve vote

-- ═══════════════════════════════════════════════════════════════════════════
-- §10  Theorems
-- ═══════════════════════════════════════════════════════════════════════════

theorem discoveryMessageHasDiscoveryType (msg : GossipFlipMessage)
    (h : msg.messageType = GossipMessageType.discovery) :
    msg.messageType = GossipMessageType.discovery := by
  -- Proof: By assumption
  assumption

/-- Invariant: heartbeat messages carry empty tile positions.
  This holds for messages created via `createHeartbeatMessage` but must be enforced
  as a protocol constraint for all heartbeat messages. -/
structure HeartbeatInvariantHypothesis where
  noFlipDelta (msg : GossipFlipMessage) (h : msg.messageType = GossipMessageType.heartbeat) :
    msg.flipDelta.tilePositions = []

/-- Theorem: consensus vote messages have enum values (trivial by Vote type). -/
theorem consensusVoteMessageHasVoteField (msg : ConsensusVoteMessage) :
    msg.vote = Vote.approve ∨ msg.vote = Vote.reject ∨ msg.vote = Vote.abstain := by
  cases msg.vote <;> simp

end Semantics.GossipFlipMessage