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

module Tutorials.Project08.Main where

open import Spartan6.API.StateResources
open import Spartan6.API.Profiles

open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty

-- Two domain names are semantic identifiers, not Boolean clock wires.  One
-- system event is a simultaneous membership function over these names.

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

sameDomain : ClockDomain -> ClockDomain -> Bit
sameDomain domainA domainA = high
sameDomain domainA domainB = low
sameDomain domainB domainA = low
sameDomain domainB domainB = high

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

data SwapContract : Type₀ where
  simultaneousSwap : SwapContract

noContracts : ClockDomain -> ClockDomain -> Maybe SwapContract
noContracts source target = nothing

noCrossDomainPolicy :
  Composition.CrossDomainPolicy ClockDomain SwapContract
noCrossDomainPolicy =
  Composition.crossDomainPolicy sameDomain sameDomain-sound noContracts

swapContracts : ClockDomain -> ClockDomain -> Maybe SwapContract
swapContracts domainA domainB = just simultaneousSwap
swapContracts domainB domainA = just simultaneousSwap
swapContracts domainA domainA = nothing
swapContracts domainB domainB = nothing

swapPolicy : Composition.CrossDomainPolicy ClockDomain SwapContract
swapPolicy =
  Composition.crossDomainPolicy
    sameDomain sameDomain-sound swapContracts

swap-a-to-b : Composition.PermissionFor swapPolicy domainA domainB
swap-a-to-b = Composition.contractPermission simultaneousSwap

swap-b-to-a : Composition.PermissionFor swapPolicy domainB domainA
swap-b-to-a = Composition.contractPermission simultaneousSwap

leftInput : Unit -> Bit × Bit -> Adapters.FDREInput
leftInput external before =
  Adapters.fdreInput (snd before) high low

rightInput : Unit -> Bit × Bit -> Adapters.FDREInput
rightInput external before =
  Adapters.fdreInput (fst before) high low

swapPair : Composition.CoupledResourcePair
  Adapters.RegisterInitial Adapters.FDREInput Bit Bit
  Adapters.RegisterInitial Adapters.FDREInput Bit Bit
  Unit ClockDomain SwapContract swapPolicy
swapPair = Composition.coupledResourcePair
  (Adapters.fdreResource domainA)
  (Adapters.fdreResource domainB)
  leftInput rightInput swap-b-to-a swap-a-to-b

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

onlyDomainB : Resource.EdgeSet ClockDomain
onlyDomainB domainA = low
onlyDomainB domainB = high

both-domain-update-is-simultaneous :
  Composition.stepPair swapPair bothDomains tt (low , high)
  ≡ (high , low)
both-domain-update-is-simultaneous = refl

one-domain-update-holds-the-other-register :
  Composition.stepPair swapPair onlyDomainB tt (low , high)
  ≡ (low , low)
one-domain-update-holds-the-other-register = refl

uncontracted-cross-domain-link-is-rejected :
  Composition.checkInteraction noCrossDomainPolicy domainA domainB
  ≡ nothing
uncontracted-cross-domain-link-is-rejected = refl

-- Profiles are executable policy checkers, not labels.  These deliberately
-- contradictory declarations are defined here instead of borrowing a
-- theorem from a production example.

fullySupportedWithoutSemantics :
  Profile.DeclaredModeCapability Mode.ibufParameters
fullySupportedWithoutSemantics =
  Profile.declaredModeCapability Evidence.fullySupported nothing
    (just Capability.noAdditionalPremise)

fully-supported-without-semantics-stays-closed :
  Profile.compileDeclaredMode fullySupportedWithoutSemantics ≡ nothing
fully-supported-without-semantics-stays-closed = refl

conditionalCarryWithoutPremise :
  Profile.DeclaredModeCapability Mode.carry4Parameters
conditionalCarryWithoutPremise =
  Profile.declaredModeCapability Evidence.conditionallySupported
    (just (Capability.semanticEvidenceFor Mode.carry4Parameters))
    nothing

conditional-mode-without-premise-stays-closed :
  Profile.compileDeclaredMode conditionalCarryWithoutPremise ≡ nothing
conditional-mode-without-premise-stays-closed = refl

ibufIdentityRelation : Capability.DecidableModeRelation   
ibufIdentityRelation = Capability.decidableModeRelation
  (λ { [] -> true })
  (λ { (input ∷ []) [] (output ∷ []) -> not (input ⊕ output) })
  (λ { input [] [] -> true })

relationalIBUFDeclaration :
  Profile.DeclaredModeCapability Mode.ibufParameters
relationalIBUFDeclaration =
  Profile.declaredModeCapability Evidence.fullySupported
    (just (Capability.relationalContract ibufIdentityRelation))
    (just Capability.noAdditionalPremise)

relational-mode-with-evidence-is-available :
  Profile.capabilityAvailable?
    (Profile.compileDeclaredMode relationalIBUFDeclaration)
  ≡ true
relational-mode-with-evidence-is-available = refl

tutorialClosedProfile : Profile.EnforceableProfile
tutorialClosedProfile =
  Profile.closedProfile "tutorial-closed-profile" nothing  false true

closed-profile-builder-grants-no-mode-by-default :
  Profile.capabilityFor tutorialClosedProfile _ Mode.ibufParameters
  ≡ nothing
closed-profile-builder-grants-no-mode-by-default = refl

development-profile-is-still-closed :
  Profile.capabilityFor Profile.developmentProfile
    _ Mode.ibufParameters
  ≡ nothing
development-profile-is-still-closed =
  Profile.development-mode-is-closed _ Mode.ibufParameters

no-device-or-silicon-claim-is-created :
  LegacyProfile.selectedDeviceProfile ≡ nothing
no-device-or-silicon-claim-is-created =
  Profile.development-selects-no-device