module ControlFlowInvariants where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

-- ============================================================
-- Abstract types for the ICP state machine architecture
-- ============================================================

postulate
  Label : Set    -- node identifiers in the ^ICP DAG
  State : Set    -- contents of ^ICP globals (memory/environment)

-- ============================================================
-- Control transfer primitives — structural duals
-- ============================================================

-- GOTO  : push mechanics — L1 dictates the future by pushing to L2
-- COME-FROM : pull mechanics — L2 dictates the past by pulling from L1
data Transfer : Set where
  GOTO      : Label → Transfer
  COME-FROM : Label → Transfer

-- A Program maps every Label to its outgoing Transfer
Prog = Label → Transfer

-- ============================================================
-- Operational semantics — the execution step relation
-- ============================================================

data Step (P : Prog) : Label × State → Label × State → Set where

  -- PUSH INVARIANT: L1 actively pushes execution to L2.
  -- State is passed through unchanged.
  step-goto : ∀ {l₁ l₂ s}
    → P l₁ ≡ GOTO l₂
    ------------------------------
    → Step P (l₁ , s) (l₂ , s)

  -- PULL INVARIANT: L2 actively pulls execution from L1.
  -- State is passed through unchanged.
  step-come-from : ∀ {l₁ l₂ s}
    → P l₂ ≡ COME-FROM l₁
    ------------------------------
    → Step P (l₁ , s) (l₂ , s)

-- ============================================================
-- INVARIANT 1: Strict State Preservation
--
-- Pure control-flow graph traversal guarantees the domain (State)
-- is unmutated across the topological shift.
-- This justifies the MUMPS PUSH/PULL routines passing STATE by value
-- and the ASP layer not touching ^ICP("NODE",...) data during traversal.
-- ============================================================

state-invariant : ∀ {P l₁ l₂ s₁ s₂}
  → Step P (l₁ , s₁) (l₂ , s₂)
  → s₁ ≡ s₂
state-invariant (step-goto _)       = refl
state-invariant (step-come-from _)  = refl

-- ============================================================
-- INVARIANT 2: Control-Flow Duality
--
-- A GOTO edge is structurally isomorphic to a COME-FROM edge.
-- is-dual P₁ P₂ captures the bidirectional adjacency requirement
-- enforced by the ASP integrity constraints:
--   :- goto(L1,L2,Guard), not come_from(L2,L1,Guard).
--   :- come_from(L2,L1,Guard), not goto(L1,L2,Guard).
-- ============================================================

is-dual : Prog → Prog → Set
is-dual P₁ P₂ =
  ∀ l₁ l₂
  → (P₁ l₁ ≡ GOTO l₂      → P₂ l₂ ≡ COME-FROM l₁)
  × (P₂ l₂ ≡ COME-FROM l₁ → P₁ l₁ ≡ GOTO l₂)

-- If P₁ has a GOTO step from (l₁,s) to (l₂,s),
-- then the dual program P₂ achieves the identical topological move
-- via COME-FROM — the same (Label × State) transition, different mechanics.
duality-invariant : ∀ {P₁ P₂ l₁ l₂ s}
  → is-dual P₁ P₂
  → P₁ l₁ ≡ GOTO l₂
  → Step P₂ (l₁ , s) (l₂ , s)
duality-invariant dual p₁-goto =
  step-come-from (proj₁ (dual _ _) p₁-goto)

-- Symmetric: a COME-FROM step in P₂ corresponds to a GOTO step in P₁.
duality-invariant-sym : ∀ {P₁ P₂ l₁ l₂ s}
  → is-dual P₁ P₂
  → P₂ l₂ ≡ COME-FROM l₁
  → Step P₁ (l₁ , s) (l₂ , s)
duality-invariant-sym dual p₂-come-from =
  step-goto (proj₂ (dual _ _) p₂-come-from)

-- ============================================================
-- INVARIANT 3: Conditional Duality (Guard-tripartite edges)
--
-- When transitions are guarded, both GOTO and COME-FROM must
-- agree on the same guard. This is enforced by the ASP layer:
--   :- goto(L1,L2,Guard), not come_from(L2,L1,Guard).
-- Formalised here as a stronger is-dual over guarded programs.
-- ============================================================

postulate
  Guard : Set   -- guard conditions (evaluated against State)

-- A guarded transfer carries a condition
data GuardedTransfer : Set where
  GOTO-IF      : Label → Guard → GuardedTransfer
  COME-FROM-IF : Label → Guard → GuardedTransfer

GuardedProg = Label → GuardedTransfer

-- Guarded step: transition fires only when guard matches
data GuardedStep (P : GuardedProg) (holds : Guard → State → Set)
    : Label × State → Label × State → Set where

  step-goto-guard : ∀ {l₁ l₂ g s}
    → P l₁ ≡ GOTO-IF l₂ g
    → holds g s
    → GuardedStep P holds (l₁ , s) (l₂ , s)

  step-come-from-guard : ∀ {l₁ l₂ g s}
    → P l₂ ≡ COME-FROM-IF l₁ g
    → holds g s
    → GuardedStep P holds (l₁ , s) (l₂ , s)

-- Guarded duality: both programs must use the same guard on the same edge.
is-guarded-dual : GuardedProg → GuardedProg → Set
is-guarded-dual P₁ P₂ =
  ∀ l₁ l₂ g
  → (P₁ l₁ ≡ GOTO-IF l₂ g      → P₂ l₂ ≡ COME-FROM-IF l₁ g)
  × (P₂ l₂ ≡ COME-FROM-IF l₁ g → P₁ l₁ ≡ GOTO-IF l₂ g)

-- Conditional duality invariant:
-- If P₁ fires a guarded GOTO under guard g at state s,
-- the dual P₂ fires the identical move via COME-FROM-IF with the same guard.
conditional-duality-invariant : ∀ {P₁ P₂ holds l₁ l₂ g s}
  → is-guarded-dual P₁ P₂
  → P₁ l₁ ≡ GOTO-IF l₂ g
  → holds g s
  → GuardedStep P₂ holds (l₁ , s) (l₂ , s)
conditional-duality-invariant dual p₁-goto-g hgs =
  step-come-from-guard (proj₁ (dual _ _ _) p₁-goto-g) hgs

-- Determinism corollary (mirrors ASP constraint):
-- A state machine is deterministic iff at most one outgoing guarded edge holds.
is-deterministic : GuardedProg → (Guard → State → Set) → Set
is-deterministic P holds =
  ∀ l₁ l₂ l₃ g₁ g₂ s
  → P l₁ ≡ GOTO-IF l₂ g₁
  → P l₁ ≡ GOTO-IF l₃ g₂
  → holds g₁ s
  → holds g₂ s
  → l₂ ≡ l₃