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

module Spartan6.Architecture.ProfileDeclaration where

open import Spartan6.Prelude
open import Spartan6.Evidence

import Spartan6.Architecture.EvidenceRegistry as Registry
import Spartan6.Architecture.ModeCapability as Capability
import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Architecture.Profile as LegacyProfile
import Spartan6.Validation.Parameter as Mode

open import Cubical.Foundations.Path using (inspect; [_]ᵢ)

-- A declaration is policy input.  Its support label alone grants nothing:
-- the exact mode must also carry semantic evidence and the canonical premise.

record DeclaredModeCapability {kind : Architecture.PrimitiveKind}
  (mode : Mode.CoreParameters kind) : Type₀ where
  constructor declaredModeCapability
  field
    declaredSupport : SupportStatus
    declaredSemantics : Maybe (Capability.ModeSemanticEvidence mode)
    declaredPremise : Maybe Capability.ConditionalPremise

open DeclaredModeCapability public

unsupportedModeDeclaration : ∀ {kind}
  → (mode : Mode.CoreParameters kind) → DeclaredModeCapability mode
unsupportedModeDeclaration mode =
  declaredModeCapability unsupportedFeature nothing nothing

canonicalModeDeclaration : ∀ {kind}
  → (mode : Mode.CoreParameters kind) → DeclaredModeCapability mode
canonicalModeDeclaration mode =
  declaredModeCapability
    (Capability.modeSupport mode)
    (just (Capability.semanticEvidenceFor mode))
    (just (Capability.modePremise mode))

-- This compiler is the trust boundary between labels and capabilities.  It
-- accepts only the exact support/premise combinations used by the semantic
-- registry; every other declaration is executable rejection.

compileDeclaredMode : ∀ {kind}
  → {mode : Mode.CoreParameters kind}
  → DeclaredModeCapability mode
  → Maybe (Capability.ExactModeCapability mode)
compileDeclaredMode {kind} {mode} declaration with
  Capability.modeSupport mode | inspect Capability.modeSupport mode
  | Capability.modePremise mode | inspect Capability.modePremise mode
  | declaredSupport declaration | declaredSemantics declaration
  | declaredPremise declaration
... | fullySupported | [ support-path ]ᵢ
    | Capability.noAdditionalPremise | [ premise-path ]ᵢ
    | fullySupported | just semantics | just Capability.noAdditionalPremise =
  just
    (Capability.exactModeCapability
      fullySupported Capability.noAdditionalPremise semantics
      (sym support-path) (sym premise-path)
      (Registry.modeTraceability kind mode) refl
      (Capability.mode-trace-executable mode))
... | conditionallySupported | [ support-path ]ᵢ
    | Capability.nonselectedCarryEntryIsLow | [ premise-path ]ᵢ
    | conditionallySupported | just semantics
    | just Capability.nonselectedCarryEntryIsLow =
  just
    (Capability.exactModeCapability
      conditionallySupported
      Capability.nonselectedCarryEntryIsLow semantics
      (sym support-path) (sym premise-path)
      (Registry.modeTraceability kind mode) refl
      (Capability.mode-trace-executable mode))
... | expected-status | [ support-path ]ᵢ
    | expected-premise | [ premise-path ]ᵢ
    | declared-status | declared-semantics | declared-premise = nothing

capabilityAvailable? : ∀ {kind} {mode : Mode.CoreParameters kind}
  → Maybe (Capability.ExactModeCapability mode) → Bool
capabilityAvailable? nothing = false
capabilityAvailable? (just capability) = true

canonical-mode-is-available : ∀ {kind}
  → (mode : Mode.CoreParameters kind)
  → capabilityAvailable?
      (compileDeclaredMode (canonicalModeDeclaration mode))
    ≡ true
canonical-mode-is-available (Mode.lut1Parameters table) = refl
canonical-mode-is-available (Mode.lut2Parameters table) = refl
canonical-mode-is-available (Mode.lut3Parameters table) = refl
canonical-mode-is-available (Mode.lut4Parameters table) = refl
canonical-mode-is-available (Mode.lut5Parameters table) = refl
canonical-mode-is-available (Mode.lut6Parameters table) = refl
canonical-mode-is-available Mode.muxf7Parameters = refl
canonical-mode-is-available Mode.muxf8Parameters = refl
canonical-mode-is-available Mode.carry4Parameters = refl
canonical-mode-is-available (Mode.fdreParameters initial) = refl
canonical-mode-is-available (Mode.fdseParameters initial) = refl
canonical-mode-is-available Mode.ibufParameters = refl
canonical-mode-is-available Mode.obufParameters = refl
canonical-mode-is-available Mode.obufdsParameters = refl
canonical-mode-is-available Mode.bufgParameters = refl
canonical-mode-is-available Mode.bufgceParameters = refl

record ProfileDeclaration : Type₀ where
  constructor profileDeclaration
  field
    declaredProfileName : String
    declaredTarget : Maybe String
    declaredMaximumClockDomains : ℕ
    declaredAllowsBidirectional : Bool
    declaredRequiresOfficialEvidence : Bool
    declaredModes : (kind : Architecture.PrimitiveKind)
      → (mode : Mode.CoreParameters kind)
      → DeclaredModeCapability mode

open ProfileDeclaration public

-- EnforceableProfile deliberately has only the declaration as stored data.
-- Its capability lookup is defined by compileDeclaredMode, so constructing the
-- wrapper cannot substitute a more permissive decision procedure.

record EnforceableProfile : Type₀ where
  constructor enforceableProfile
  field
    sourceDeclaration : ProfileDeclaration

open EnforceableProfile public

compileProfile : ProfileDeclaration → EnforceableProfile
compileProfile = enforceableProfile

closedProfileDeclaration :
  String -> Maybe String -> ℕ -> Bool -> Bool -> ProfileDeclaration
closedProfileDeclaration name target maximum-domains
  allows-bidirectional requires-official-evidence =
  profileDeclaration name target maximum-domains
    allows-bidirectional requires-official-evidence
    (λ kind mode -> unsupportedModeDeclaration mode)

closedProfile :
  String -> Maybe String -> ℕ -> Bool -> Bool -> EnforceableProfile
closedProfile name target maximum-domains
  allows-bidirectional requires-official-evidence =
  compileProfile
    (closedProfileDeclaration name target maximum-domains
      allows-bidirectional requires-official-evidence)

capabilityFor : (profile : EnforceableProfile)
  → (kind : Architecture.PrimitiveKind)
  → (mode : Mode.CoreParameters kind)
  → Maybe (Capability.ExactModeCapability mode)
capabilityFor profile kind mode =
  compileDeclaredMode
    (declaredModes (sourceDeclaration profile) kind mode)

profileName : EnforceableProfile → String
profileName profile = declaredProfileName (sourceDeclaration profile)

profileTarget : EnforceableProfile → Maybe String
profileTarget profile = declaredTarget (sourceDeclaration profile)

maximumClockDomains : EnforceableProfile → ℕ
maximumClockDomains profile =
  declaredMaximumClockDomains (sourceDeclaration profile)

allowsBidirectional : EnforceableProfile → Bool
allowsBidirectional profile =
  declaredAllowsBidirectional (sourceDeclaration profile)

requiresOfficialEvidence : EnforceableProfile → Bool
requiresOfficialEvidence profile =
  declaredRequiresOfficialEvidence (sourceDeclaration profile)

developmentDeclaration : ProfileDeclaration
developmentDeclaration = closedProfileDeclaration
  "spartan6-level1-development"
  (just "spartan6-level1-development")
   false true

developmentProfile : EnforceableProfile
developmentProfile = compileProfile developmentDeclaration

development-mode-is-closed : ∀ kind
  → (mode : Mode.CoreParameters kind)
  → capabilityFor developmentProfile kind mode ≡ nothing
development-mode-is-closed kind (Mode.lut1Parameters table) = refl
development-mode-is-closed kind (Mode.lut2Parameters table) = refl
development-mode-is-closed kind (Mode.lut3Parameters table) = refl
development-mode-is-closed kind (Mode.lut4Parameters table) = refl
development-mode-is-closed kind (Mode.lut5Parameters table) = refl
development-mode-is-closed kind (Mode.lut6Parameters table) = refl
development-mode-is-closed kind Mode.muxf7Parameters = refl
development-mode-is-closed kind Mode.muxf8Parameters = refl
development-mode-is-closed kind Mode.carry4Parameters = refl
development-mode-is-closed kind (Mode.fdreParameters initial) = refl
development-mode-is-closed kind (Mode.fdseParameters initial) = refl
development-mode-is-closed kind Mode.ibufParameters = refl
development-mode-is-closed kind Mode.obufParameters = refl
development-mode-is-closed kind Mode.obufdsParameters = refl
development-mode-is-closed kind Mode.bufgParameters = refl
development-mode-is-closed kind Mode.bufgceParameters = refl

development-selects-no-device :
  LegacyProfile.selectedDeviceProfile ≡ nothing
development-selects-no-device = refl