-- CarryQuantum.QuantumSpec
-- Agda dependent-type specification.
-- Illegal FSM transitions are unrepresentable at the type level.
-- Compile: agda QuantumSpec.agda

module QuantumSpec where

open import Data.Nat using (ℕ; _<_; suc; zero; _+_)
open import Data.Bool using (Bool; true; false)
open import Data.Product using (_×_; _,_; ∃)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Empty using (⊥; ⊥-elim)

-- ============================================================
-- FSM States
-- ============================================================

data FSMState : Set where
  Init      : FSMState
  Prepare   : FSMState
  Entangle  : FSMState
  Compute   : FSMState
  Measure   : FSMState
  Verify    : FSMState
  Commit    : FSMState
  Halted    : FSMState
  CycleLimit : FSMState

-- ============================================================
-- Allowed Transition — encoded as a type index.
-- A value of type `Transition s s'` is a proof that the edge exists.
-- An illegal (s, s') pair has no constructor → it is unrepresentable.
-- ============================================================

data Transition : FSMState → FSMState → Set where
  T-Init-Prepare   : Transition Init      Prepare
  T-Prep-Entangle  : Transition Prepare   Entangle
  T-Ent-Compute    : Transition Entangle  Compute
  T-Comp-Measure   : Transition Compute   Measure
  T-Meas-Verify    : Transition Measure   Verify
  T-Veri-Commit    : Transition Verify    Commit
  T-Comm-Prepare   : Transition Commit    Prepare    -- loop back
  T-Comm-Commit    : Transition Commit    Commit     -- terminal commit
  T-Any-Halted     : ∀ {s} → Transition s Halted    -- emergency halt

-- ============================================================
-- Terminal states
-- ============================================================

data Terminal : FSMState → Set where
  T-Halted    : Terminal Halted
  T-Cycle     : Terminal CycleLimit

-- INV-5 by construction:
-- There is no constructor of type `Transition Halted s'` for s' ≠ Halted.
-- Proof: inspect every constructor — T-Any-Halted is the only one where
-- Halted appears, and it appears on the RIGHT. So Halted as a source
-- produces no constructors at all (except via T-Any-Halted arriving at Halted).
-- The type Transition Halted (non-Halted) is uninhabited.

-- We can prove this:
halted-absorbing : ∀ {s'} → Transition Halted s' → s' ≡ Halted
halted-absorbing T-Any-Halted = refl
-- No other constructor has Halted as its first argument → proof is total.

cyclelimit-absorbing : ∀ {s'} → Transition CycleLimit s' → s' ≡ Halted
cyclelimit-absorbing T-Any-Halted = refl

-- ============================================================
-- FSM record with cycle budget
-- ============================================================

record FSM : Set where
  field
    state    : FSMState
    cycle    : ℕ
    maxCycle : ℕ
    bounded  : cycle < suc maxCycle   -- cycle ≤ maxCycle

-- ============================================================
-- Step function — INV-4 guaranteed by type signature.
-- `step` only accepts a `Transition (fsm .state) s'` witness.
-- If you cannot construct that witness, you cannot call step.
-- ============================================================

data StepResult : Set where
  Ok    : FSM → StepResult
  Err   : StepResult

step : (fsm : FSM) → (s' : FSMState) → Transition (FSM.state fsm) s' → StepResult
step fsm s' t with FSM.cycle fsm < FSM.maxCycle
... | false = Ok (record fsm { state = CycleLimit })
... | true  = Ok (record fsm
                    { state   = s'
                    ; cycle   = suc (FSM.cycle fsm)
                    ; bounded = {!!}    -- obligation: suc cycle ≤ suc maxCycle
                    })

-- step never returns Err for allowed transitions — that is the type guarantee.
-- For terminal states the caller cannot construct a Transition witness at all,
-- so they cannot call step. No runtime check needed.

-- ============================================================
-- Normalisation
-- ============================================================

postulate
  Amp    : Set
  normSq : Amp → ℕ    -- simplified; use rationals or reals in full version

-- A statevector of dimension 2^n
StateVec : ℕ → Set
StateVec n = (i : ℕ) → Amp    -- domain is Fin(2^n) in a full version

postulate
  sumNormSq : ∀ {n} → StateVec n → ℕ

-- DEF-1: Normalised
Normalised : ∀ {n} → StateVec n → Set
Normalised {n} ψ = sumNormSq ψ ≡ 1

-- DEF-2: Unitary (norm-preserving)
IsUnitary : ∀ {n} → (StateVec n → StateVec n) → Set
IsUnitary {n} U = ∀ ψ → Normalised ψ → Normalised (U ψ)

-- INV-1: Unitary gates preserve normalisation — direct from the definition
inv1 : ∀ {n} (ψ : StateVec n) (U : StateVec n → StateVec n)
     → IsUnitary U → Normalised ψ → Normalised (U ψ)
inv1 ψ U hU hN = hU ψ hN

-- ============================================================
-- Agent ownership
-- ============================================================

postulate
  QubitSet    : Set
  ∅           : QubitSet
  _∩_         : QubitSet → QubitSet → QubitSet
  emptyInter  : ∀ (a b : QubitSet) → Set   -- a ∩ b ≡ ∅

-- DEF-7: Disjoint ownership
OwnershipDisjoint : QubitSet → QubitSet → Set
OwnershipDisjoint a b = emptyInter a b

-- INV-7: If ownership is disjoint, agent A's qubits are not in agent B's set
postulate
  inv7 : ∀ (a b : QubitSet) → OwnershipDisjoint a b
       → ∀ q → q ∈ a → q ∉ b    -- ∈/∉ defined over QubitSet
  where
    postulate
      _∈_ : ℕ → QubitSet → Set
      _∉_ : ℕ → QubitSet → Set