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

module Spartan6.Examples.StateDomains where

open import Spartan6.Prelude
open import Spartan6.Hierarchy.Interface
open import Spartan6.Semantics.StateAdapters
open import Spartan6.Semantics.StateComposition
open import Spartan6.Semantics.StateResource

open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty
import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.FlatMachine as Flat
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Hierarchy.ResourcePairFlattening as PairFlattening
import Spartan6.Primitive.SRL16E as SRL16E

data ClockDomain : Type₀ where
  domainA : ClockDomain
  domainB : ClockDomain

sameClockDomain : ClockDomain → ClockDomain → Bit
sameClockDomain domainA domainA = high
sameClockDomain domainA domainB = low
sameClockDomain domainB domainA = low
sameClockDomain domainB domainB = high

sameClockDomain-sound : ∀ source target
  → sameClockDomain source target ≡ high
  → source ≡ target
sameClockDomain-sound domainA domainA result = refl
sameClockDomain-sound domainA domainB result =
  Empty.rec (false≢true result)
sameClockDomain-sound domainB domainA result =
  Empty.rec (false≢true result)
sameClockDomain-sound domainB domainB result = refl

data DomainContract : Type₀ where
  simultaneousSwapContract : DomainContract

noCrossDomainContract : ClockDomain → ClockDomain → Maybe DomainContract
noCrossDomainContract source target = nothing

noCrossDomainPolicy : CrossDomainPolicy ClockDomain DomainContract
noCrossDomainPolicy =
  crossDomainPolicy
    sameClockDomain sameClockDomain-sound noCrossDomainContract

swapContract : ClockDomain → ClockDomain → Maybe DomainContract
swapContract domainA domainB = just simultaneousSwapContract
swapContract domainB domainA = just simultaneousSwapContract
swapContract domainA domainA = nothing
swapContract domainB domainB = nothing

swapPolicy : CrossDomainPolicy ClockDomain DomainContract
swapPolicy =
  crossDomainPolicy sameClockDomain sameClockDomain-sound swapContract

unsupported-cross-domain-is-rejected :
  checkInteraction noCrossDomainPolicy domainA domainB ≡ nothing
unsupported-cross-domain-is-rejected = refl

unsupported-cross-domain-has-no-permission :
  PermissionFor noCrossDomainPolicy domainA domainB → Empty.⊥
unsupported-cross-domain-has-no-permission permission =
  rejected-permission-impossible permission

swap-a-to-b-permission : PermissionFor swapPolicy domainA domainB
swap-a-to-b-permission =
  contractPermission simultaneousSwapContract

swap-b-to-a-permission : PermissionFor swapPolicy domainB domainA
swap-b-to-a-permission =
  contractPermission simultaneousSwapContract

bothDomains : EdgeSet ClockDomain
bothDomains domainA = high
bothDomains domainB = high

onlyDomainA : EdgeSet ClockDomain
onlyDomainA domainA = high
onlyDomainA domainB = low

leftSwapInput : Unit → Bit × Bit → FDREInput
leftSwapInput external before =
  fdreInput (snd before) high low

rightSwapInput : Unit → Bit × Bit → FDREInput
rightSwapInput external before =
  fdreInput (fst before) high low

ownStateInput : Unit -> Bit -> FDREInput
ownStateInput external state = fdreInput state high low

independentPair :
  IndependentResourcePair
    RegisterInitial FDREInput Bit Bit
    RegisterInitial FDREInput Bit Bit
    Unit ClockDomain
independentPair =
  independentResourcePair
    (fdreResource domainA) (fdreResource domainB)
    ownStateInput ownStateInput

independent-domains-require-no-cross-permission :
  stepIndependentPair independentPair bothDomains tt (low , high)
  ≡ (low , high)
independent-domains-require-no-cross-permission = refl

rightFeedsLeftPair :
  RightToLeftResourcePair
    RegisterInitial FDREInput Bit Bit
    RegisterInitial FDREInput Bit Bit
    Unit ClockDomain DomainContract swapPolicy
rightFeedsLeftPair =
  rightToLeftResourcePair
    (fdreResource domainA) (fdreResource domainB)
    leftSwapInput ownStateInput swap-b-to-a-permission

one-direction-needs-one-permission :
  stepRightToLeftPair rightFeedsLeftPair bothDomains tt (low , high)
  ≡ (high , high)
one-direction-needs-one-permission = refl

swapPair :
  CoupledResourcePair
    RegisterInitial FDREInput Bit Bit
    RegisterInitial FDREInput Bit Bit
    Unit ClockDomain DomainContract swapPolicy
swapPair =
  coupledResourcePair
    (fdreResource domainA)
    (fdreResource domainB)
    leftSwapInput
    rightSwapInput
    swap-b-to-a-permission
    swap-a-to-b-permission

-- Both domains load from the one common pre-state.  A sequential update would
-- instead feed the new left value to the right register and produce high/high.

two-domain-simultaneous-update :
  stepPair swapPair bothDomains tt (low , high) ≡ (high , low)
two-domain-simultaneous-update = refl

one-domain-edge-holds-the-other :
  stepPair swapPair onlyDomainA tt (low , high) ≡ (high , high)
one-domain-edge-holds-the-other = refl

pair-default-initialization :
  decodePairInitial swapPair (nothing , nothing)
  ≡ just (low , low)
pair-default-initialization = refl

swap-step-is-the-composed-simultaneous-step :
  stepPair swapPair bothDomains tt (low , high)
  ≡
    ( stepResource (leftResource swapPair) bothDomains
        (leftInput swapPair tt (low , high)) low
    , stepResource (rightResource swapPair) bothDomains
        (rightInput swapPair tt (low , high)) high
    )
swap-step-is-the-composed-simultaneous-step =
  simultaneous-step-components
    swapPair bothDomains tt (low , high)

-- The same pair now reaches a flat bit-state machine through two independent
-- certified resource lowerings.  The flat transition splits the one common
-- pre-state, computes both next states, and only then appends the results.

leftStatePort rightStatePort : StablePort
leftStatePort = stablePort 0 "left-state" 1
rightStatePort = stablePort 1 "right-state" 1

pairOutput : Interface
pairOutput =
  signalInterface leftStatePort ∥ᵢ signalInterface rightStatePort

swapBoundary : PairFlattening.PairBoundary
  emptyInterface pairOutput Unit Bit Bit
swapBoundary = PairFlattening.pairBoundary
  (λ input -> tt)
  (λ observations ->
    (fst observations ∷ []) , (snd observations ∷ []))

swapInitialization : PairFlattening.PairInitialization swapPair
swapInitialization = PairFlattening.pairInitialization
  (nothing , nothing) (low , low) refl

swapIdentity : Provenance.ComponentIdentity
swapIdentity = Provenance.componentIdentity 80 "two-domain-swap"

swapOrigin : Provenance.SourceOrigin
swapOrigin =
  Provenance.sourceOrigin nothing nothing []ᴸ "constructed.two-domain-swap"

swapHierarchy : Component.Component
  emptyInterface pairOutput (EdgeSet ClockDomain) (Bit × Bit)
swapHierarchy =
  PairFlattening.pairComponent
    swapIdentity swapOrigin swapPair swapBoundary swapInitialization

swapFlattening : Flat.CertifiedMachineFlattening swapHierarchy
swapFlattening =
  PairFlattening.pairFlattens 1 1
    swapIdentity swapOrigin swapPair swapBoundary swapInitialization
    (fdreBitLowering domainA) (fdreBitLowering domainB)

flat-pair-default-initialization :
  Flat.flatInitial (Flat.flatTarget swapFlattening)
  ≡ low ∷ low ∷ []
flat-pair-default-initialization = refl

flat-two-domain-simultaneous-update :
  Flat.flatStep (Flat.flatTarget swapFlattening)
    bothDomains tt (low ∷ high ∷ [])
  ≡ high ∷ low ∷ []
flat-two-domain-simultaneous-update = refl

swap-flattening-preserves-the-two-domain-step :
  Flat.StateRelation swapFlattening
    (stepPair swapPair bothDomains tt (low , high))
    (Flat.flatStep (Flat.flatTarget swapFlattening)
      bothDomains tt (low ∷ high ∷ []))
swap-flattening-preserves-the-two-domain-step =
  Flat.transitionPreserved swapFlattening
    bothDomains tt (low , high) (low ∷ high ∷ [])
    (refl , refl)

-- SRL16E is adapted as typed standalone semantics only.  This reduction
-- checks that an owned edge uses the existing enabled-shift definition.

srl16e-owned-edge-loads-first-stage :
  SRL16E.readSRL16E
    (stepResource (srl16eResource domainA) bothDomains
      (srl16eInput SRL16E.address0000 high high)
      SRL16E.defaultInitialState)
    SRL16E.address0000
  ≡ high
srl16e-owned-edge-loads-first-stage = refl

srl16e-foreign-edge-holds :
  stepResource (srl16eResource domainB) onlyDomainA
    (srl16eInput SRL16E.address0000 high high)
    SRL16E.defaultInitialState
  ≡ SRL16E.defaultInitialState
srl16e-foreign-edge-holds = refl