{-# OPTIONS --safe --cubical #-}

module Spartan6.Semantics.StateComposition where

open import Spartan6.Prelude
open import Spartan6.Semantics.StateResource

import Cubical.Data.Empty as Empty

-- A policy classifies a directed state-dependent interaction.  The Boolean
-- same-domain test is part of the policy evidence boundary: if it says false,
-- an explicit contract must be present or the interaction is rejected.

record CrossDomainPolicy (Domain Contract : Type₀) : Type₀ where
  constructor crossDomainPolicy
  field
    sameDomainTest       : Domain → Domain → Bit
    sameDomainSound      : ∀ source target
      → sameDomainTest source target ≡ high
      → source ≡ target
    interactionContract : Domain → Domain → Maybe Contract

open CrossDomainPolicy public

data InteractionDecision (Contract : Type₀) : Type₀ where
  localInteraction      : InteractionDecision Contract
  contractedInteraction : Contract → InteractionDecision Contract
  rejectedInteraction   : InteractionDecision Contract

decideInteraction :
  ∀ {Domain Contract}
  → CrossDomainPolicy Domain Contract
  → Domain → Domain → InteractionDecision Contract
decideInteraction policy source target
  with sameDomainTest policy source target
... | true = localInteraction
... | false with interactionContract policy source target
...   | nothing       = rejectedInteraction
...   | just contract = contractedInteraction contract

-- Permission is indexed by the decision and deliberately has no constructor
-- for rejection.

data InteractionPermission {Contract : Type₀}
  : InteractionDecision Contract → Type₀ where
  localPermission : InteractionPermission localInteraction
  contractPermission : ∀ contract
    → InteractionPermission (contractedInteraction contract)

PermissionFor :
  ∀ {Domain Contract}
  → CrossDomainPolicy Domain Contract → Domain → Domain → Type₀
PermissionFor policy source target =
  InteractionPermission (decideInteraction policy source target)

checkDecision : ∀ {Contract} (decision : InteractionDecision Contract)
  → Maybe (InteractionPermission decision)
checkDecision localInteraction = just localPermission
checkDecision (contractedInteraction contract) =
  just (contractPermission contract)
checkDecision rejectedInteraction = nothing

checkInteraction :
  ∀ {Domain Contract}
    (policy : CrossDomainPolicy Domain Contract)
    (source target : Domain)
  → Maybe (PermissionFor policy source target)
checkInteraction policy source target
  with decideInteraction policy source target
... | localInteraction = just localPermission
... | contractedInteraction contract =
  just (contractPermission contract)
... | rejectedInteraction = nothing

rejected-permission-impossible :
  ∀ {Contract}
  → InteractionPermission
      (rejectedInteraction {Contract = Contract})
  → Empty.⊥
rejected-permission-impossible ()

private
  variable
    Initial₁ Input₁ Observation₁ State₁ : Type₀
    Initial₂ Input₂ Observation₂ State₂ : Type₀
    External Domain Contract : Type₀
    policy : CrossDomainPolicy Domain Contract

-- Both input functions may inspect both old states.  Consequently each
-- direction carries a checked interaction permission.  The transition below
-- applies both functions to the same `before` pair.

record CoupledResourcePair
  (Initial₁ Input₁ Observation₁ State₁ : Type₀)
  (Initial₂ Input₂ Observation₂ State₂ : Type₀)
  (External Domain Contract : Type₀)
  (policy : CrossDomainPolicy Domain Contract) : Type₀ where
  constructor coupledResourcePair
  field
    leftResource :
      StateResource Initial₁ Input₁ Observation₁ Domain State₁
    rightResource :
      StateResource Initial₂ Input₂ Observation₂ Domain State₂

    leftInput  : External → State₁ × State₂ → Input₁
    rightInput : External → State₁ × State₂ → Input₂

    right-to-left-permission :
      PermissionFor policy
        (resourceDomain rightResource) (resourceDomain leftResource)
    left-to-right-permission :
      PermissionFor policy
        (resourceDomain leftResource) (resourceDomain rightResource)

open CoupledResourcePair public

decodePairInitial :
  CoupledResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy
  → Initial₁ × Initial₂ → Maybe (State₁ × State₂)
decodePairInitial pair initial
  with decodeInitial (leftResource pair) (fst initial)
... | nothing = nothing
... | just left-state
  with decodeInitial (rightResource pair) (snd initial)
...   | nothing = nothing
...   | just right-state = just (left-state , right-state)

observePair :
  CoupledResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy
  → External → State₁ × State₂ → Observation₁ × Observation₂
observePair pair external before =
  observeResource (leftResource pair)
    (leftInput pair external before) (fst before)
  ,
  observeResource (rightResource pair)
    (rightInput pair external before) (snd before)

stepPair :
  CoupledResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy
  → EdgeSet Domain → External → State₁ × State₂ → State₁ × State₂
stepPair pair edges external before =
  stepResource (leftResource pair) edges
    (leftInput pair external before) (fst before)
  ,
  stepResource (rightResource pair) edges
    (rightInput pair external before) (snd before)

-- This equation is the composition theorem: neither component is fed an
-- intermediate pair containing the other component's new state.

simultaneous-step-components :
  (pair : CoupledResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy)
  → (edges : EdgeSet Domain) (external : External)
  → (before : State₁ × State₂)
  → stepPair pair edges external before
  ≡
    ( stepResource (leftResource pair) edges
        (leftInput pair external before) (fst before)
    , stepResource (rightResource pair) edges
        (rightInput pair external before) (snd before)
    )
simultaneous-step-components pair edges external before = refl

left-step-uses-common-pre-state :
  (pair : CoupledResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy)
  → (edges : EdgeSet Domain) (external : External)
  → (before : State₁ × State₂)
  → fst (stepPair pair edges external before)
  ≡ stepResource (leftResource pair) edges
      (leftInput pair external before) (fst before)
left-step-uses-common-pre-state pair edges external before = refl

right-step-uses-common-pre-state :
  (pair : CoupledResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy)
  → (edges : EdgeSet Domain) (external : External)
  → (before : State₁ × State₂)
  → snd (stepPair pair edges external before)
  ≡ stepResource (rightResource pair) edges
      (rightInput pair external before) (snd before)
right-step-uses-common-pre-state pair edges external before = refl

-- Dependency-shaped composition ------------------------------------------

-- The fully coupled record above remains the compatibility surface.  These
-- additive records avoid demanding permissions for state dependencies that
-- are absent from the input functions' types.

record IndependentResourcePair
  (Initial₁ Input₁ Observation₁ State₁ : Type₀)
  (Initial₂ Input₂ Observation₂ State₂ : Type₀)
  (External Domain : Type₀) : Type₀ where
  constructor independentResourcePair
  field
    independentLeftResource :
      StateResource Initial₁ Input₁ Observation₁ Domain State₁
    independentRightResource :
      StateResource Initial₂ Input₂ Observation₂ Domain State₂
    independentLeftInput : External -> State₁ -> Input₁
    independentRightInput : External -> State₂ -> Input₂

open IndependentResourcePair public

observeIndependentPair :
  IndependentResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain
  -> External -> State₁ × State₂ -> Observation₁ × Observation₂
observeIndependentPair pair external before =
  observeResource (independentLeftResource pair)
    (independentLeftInput pair external (fst before)) (fst before)
  ,
  observeResource (independentRightResource pair)
    (independentRightInput pair external (snd before)) (snd before)

stepIndependentPair :
  IndependentResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain
  -> EdgeSet Domain -> External -> State₁ × State₂ -> State₁ × State₂
stepIndependentPair pair edges external before =
  stepResource (independentLeftResource pair) edges
    (independentLeftInput pair external (fst before)) (fst before)
  ,
  stepResource (independentRightResource pair) edges
    (independentRightInput pair external (snd before)) (snd before)

record RightToLeftResourcePair
  (Initial₁ Input₁ Observation₁ State₁ : Type₀)
  (Initial₂ Input₂ Observation₂ State₂ : Type₀)
  (External Domain Contract : Type₀)
  (policy : CrossDomainPolicy Domain Contract) : Type₀ where
  constructor rightToLeftResourcePair
  field
    rightToLeftLeftResource :
      StateResource Initial₁ Input₁ Observation₁ Domain State₁
    rightToLeftRightResource :
      StateResource Initial₂ Input₂ Observation₂ Domain State₂
    rightToLeftLeftInput : External -> State₁ × State₂ -> Input₁
    rightToLeftRightInput : External -> State₂ -> Input₂
    rightToLeftPermission :
      PermissionFor policy
        (resourceDomain rightToLeftRightResource)
        (resourceDomain rightToLeftLeftResource)

open RightToLeftResourcePair public

observeRightToLeftPair :
  RightToLeftResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy
  -> External -> State₁ × State₂ -> Observation₁ × Observation₂
observeRightToLeftPair pair external before =
  observeResource (rightToLeftLeftResource pair)
    (rightToLeftLeftInput pair external before) (fst before)
  ,
  observeResource (rightToLeftRightResource pair)
    (rightToLeftRightInput pair external (snd before)) (snd before)

stepRightToLeftPair :
  RightToLeftResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy
  -> EdgeSet Domain -> External -> State₁ × State₂ -> State₁ × State₂
stepRightToLeftPair pair edges external before =
  stepResource (rightToLeftLeftResource pair) edges
    (rightToLeftLeftInput pair external before) (fst before)
  ,
  stepResource (rightToLeftRightResource pair) edges
    (rightToLeftRightInput pair external (snd before)) (snd before)

record LeftToRightResourcePair
  (Initial₁ Input₁ Observation₁ State₁ : Type₀)
  (Initial₂ Input₂ Observation₂ State₂ : Type₀)
  (External Domain Contract : Type₀)
  (policy : CrossDomainPolicy Domain Contract) : Type₀ where
  constructor leftToRightResourcePair
  field
    leftToRightLeftResource :
      StateResource Initial₁ Input₁ Observation₁ Domain State₁
    leftToRightRightResource :
      StateResource Initial₂ Input₂ Observation₂ Domain State₂
    leftToRightLeftInput : External -> State₁ -> Input₁
    leftToRightRightInput : External -> State₁ × State₂ -> Input₂
    leftToRightPermission :
      PermissionFor policy
        (resourceDomain leftToRightLeftResource)
        (resourceDomain leftToRightRightResource)

open LeftToRightResourcePair public

observeLeftToRightPair :
  LeftToRightResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy
  -> External -> State₁ × State₂ -> Observation₁ × Observation₂
observeLeftToRightPair pair external before =
  observeResource (leftToRightLeftResource pair)
    (leftToRightLeftInput pair external (fst before)) (fst before)
  ,
  observeResource (leftToRightRightResource pair)
    (leftToRightRightInput pair external before) (snd before)

stepLeftToRightPair :
  LeftToRightResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy
  -> EdgeSet Domain -> External -> State₁ × State₂ -> State₁ × State₂
stepLeftToRightPair pair edges external before =
  stepResource (leftToRightLeftResource pair) edges
    (leftToRightLeftInput pair external (fst before)) (fst before)
  ,
  stepResource (leftToRightRightResource pair) edges
    (leftToRightRightInput pair external before) (snd before)

independent-step-uses-common-pre-state :
  (pair : IndependentResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain)
  -> (edges : EdgeSet Domain) (external : External)
  -> (before : State₁ × State₂)
  -> stepIndependentPair pair edges external before
    ≡
      ( stepResource (independentLeftResource pair) edges
          (independentLeftInput pair external (fst before)) (fst before)
      , stepResource (independentRightResource pair) edges
          (independentRightInput pair external (snd before)) (snd before))
independent-step-uses-common-pre-state pair edges external before = refl

right-to-left-step-uses-common-pre-state :
  (pair : RightToLeftResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy)
  -> (edges : EdgeSet Domain) (external : External)
  -> (before : State₁ × State₂)
  -> fst (stepRightToLeftPair pair edges external before)
    ≡ stepResource (rightToLeftLeftResource pair) edges
        (rightToLeftLeftInput pair external before) (fst before)
right-to-left-step-uses-common-pre-state pair edges external before = refl

left-to-right-step-uses-common-pre-state :
  (pair : LeftToRightResourcePair
    Initial₁ Input₁ Observation₁ State₁
    Initial₂ Input₂ Observation₂ State₂
    External Domain Contract policy)
  -> (edges : EdgeSet Domain) (external : External)
  -> (before : State₁ × State₂)
  -> snd (stepLeftToRightPair pair edges external before)
    ≡ stepResource (leftToRightRightResource pair) edges
        (leftToRightRightInput pair external before) (snd before)
left-to-right-step-uses-common-pre-state pair edges external before = refl