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

module Spartan6.Architecture.ModeCapability where

open import Spartan6.Prelude
open import Spartan6.Evidence

import Spartan6.Architecture.EvidenceRegistry as Registry
import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.PrimitiveHandler as Handler
import Spartan6.Validation.Parameter as Mode

-- A Boolean-valued relation is an independent, executable specification of
-- permitted initial states, observations, and transitions.  It is deliberately
-- separate from the expression-backed handlers used by the current exact
-- modes: a future profile may admit a relational contract without pretending
-- that it has a deterministic lowering.

record DecidableModeRelation
  (inputCount outputCount stateCount : ℕ) : Type₀ where
  constructor decidableModeRelation
  field
    initialAllowed : Vec Bit stateCount → Bool
    observationAllowed :
      Vec Bit inputCount → Vec Bit stateCount
      → Vec Bit outputCount → Bool
    transitionAllowed :
      Vec Bit inputCount → Vec Bit stateCount
      → Vec Bit stateCount → Bool

open DecidableModeRelation public

modeInputBits : ∀ {kind}
  → Mode.CoreParameters kind → ℕ
modeInputBits (Mode.lut1Parameters table) = 1
modeInputBits (Mode.lut2Parameters table) = 2
modeInputBits (Mode.lut3Parameters table) = 3
modeInputBits (Mode.lut4Parameters table) = 4
modeInputBits (Mode.lut5Parameters table) = 5
modeInputBits (Mode.lut6Parameters table) = 6
modeInputBits Mode.muxf7Parameters = 3
modeInputBits Mode.muxf8Parameters = 3
modeInputBits Mode.carry4Parameters = 9
modeInputBits (Mode.fdreParameters initial) = 3
modeInputBits (Mode.fdseParameters initial) = 3
modeInputBits Mode.ibufParameters = 1
modeInputBits Mode.obufParameters = 1
modeInputBits Mode.obufdsParameters = 1
modeInputBits Mode.bufgParameters = 1
modeInputBits Mode.bufgceParameters = 2

modeOutputBits : ∀ {kind}
  → Mode.CoreParameters kind → ℕ
modeOutputBits (Mode.lut1Parameters table) = 1
modeOutputBits (Mode.lut2Parameters table) = 1
modeOutputBits (Mode.lut3Parameters table) = 1
modeOutputBits (Mode.lut4Parameters table) = 1
modeOutputBits (Mode.lut5Parameters table) = 1
modeOutputBits (Mode.lut6Parameters table) = 1
modeOutputBits Mode.muxf7Parameters = 1
modeOutputBits Mode.muxf8Parameters = 1
modeOutputBits Mode.carry4Parameters = 8
modeOutputBits (Mode.fdreParameters initial) = 1
modeOutputBits (Mode.fdseParameters initial) = 1
modeOutputBits Mode.ibufParameters = 1
modeOutputBits Mode.obufParameters = 1
modeOutputBits Mode.obufdsParameters = 2
modeOutputBits Mode.bufgParameters = 1
modeOutputBits Mode.bufgceParameters = 1

modeStateBits : ∀ {kind}
  → Mode.CoreParameters kind → ℕ
modeStateBits (Mode.lut1Parameters table) = 0
modeStateBits (Mode.lut2Parameters table) = 0
modeStateBits (Mode.lut3Parameters table) = 0
modeStateBits (Mode.lut4Parameters table) = 0
modeStateBits (Mode.lut5Parameters table) = 0
modeStateBits (Mode.lut6Parameters table) = 0
modeStateBits Mode.muxf7Parameters = 0
modeStateBits Mode.muxf8Parameters = 0
modeStateBits Mode.carry4Parameters = 0
modeStateBits (Mode.fdreParameters initial) = 1
modeStateBits (Mode.fdseParameters initial) = 1
modeStateBits Mode.ibufParameters = 0
modeStateBits Mode.obufParameters = 0
modeStateBits Mode.obufdsParameters = 0
modeStateBits Mode.bufgParameters = 0
modeStateBits Mode.bufgceParameters = 0

-- Executable evidence is indexed by the exact decoded mode and exact bit
-- shape.  A combinational witness must additionally prove that the mode has
-- no semantic state.  Relational evidence uses the same exact dimensions.

data ModeSemanticEvidence {kind : Architecture.PrimitiveKind}
  (mode : Mode.CoreParameters kind) : Type₀ where
  executableCombinational :
    Handler.CertifiedHandler
      (modeInputBits mode) (modeOutputBits mode)
    → modeStateBits mode ≡ 0
    → ModeSemanticEvidence mode
  executableState :
    Handler.CertifiedStateHandler
      (modeInputBits mode) (modeOutputBits mode) (modeStateBits mode)
    → ModeSemanticEvidence mode
  relationalContract :
    DecidableModeRelation
      (modeInputBits mode) (modeOutputBits mode) (modeStateBits mode)
    → ModeSemanticEvidence mode

-- Conditions name semantic obligations; they are not evidence that a raw
-- occurrence satisfies them.  The latter is source-indexed and belongs to
-- validation.  In particular, CARRY4 keeps the existing exact restriction
-- that the non-selected entry input is literally low.

data ConditionalPremise : Type₀ where
  noAdditionalPremise : ConditionalPremise
  nonselectedCarryEntryIsLow : ConditionalPremise

modePremise : ∀ {kind}
  → Mode.CoreParameters kind → ConditionalPremise
modePremise (Mode.lut1Parameters table) = noAdditionalPremise
modePremise (Mode.lut2Parameters table) = noAdditionalPremise
modePremise (Mode.lut3Parameters table) = noAdditionalPremise
modePremise (Mode.lut4Parameters table) = noAdditionalPremise
modePremise (Mode.lut5Parameters table) = noAdditionalPremise
modePremise (Mode.lut6Parameters table) = noAdditionalPremise
modePremise Mode.muxf7Parameters = noAdditionalPremise
modePremise Mode.muxf8Parameters = noAdditionalPremise
modePremise Mode.carry4Parameters = nonselectedCarryEntryIsLow
modePremise (Mode.fdreParameters initial) = noAdditionalPremise
modePremise (Mode.fdseParameters initial) = noAdditionalPremise
modePremise Mode.ibufParameters = noAdditionalPremise
modePremise Mode.obufParameters = noAdditionalPremise
modePremise Mode.obufdsParameters = noAdditionalPremise
modePremise Mode.bufgParameters = noAdditionalPremise
modePremise Mode.bufgceParameters = noAdditionalPremise

modeSupport : ∀ {kind}
  → Mode.CoreParameters kind → SupportStatus
modeSupport (Mode.lut1Parameters table) = fullySupported
modeSupport (Mode.lut2Parameters table) = fullySupported
modeSupport (Mode.lut3Parameters table) = fullySupported
modeSupport (Mode.lut4Parameters table) = fullySupported
modeSupport (Mode.lut5Parameters table) = fullySupported
modeSupport (Mode.lut6Parameters table) = fullySupported
modeSupport Mode.muxf7Parameters = fullySupported
modeSupport Mode.muxf8Parameters = fullySupported
modeSupport Mode.carry4Parameters = conditionallySupported
modeSupport (Mode.fdreParameters initial) = fullySupported
modeSupport (Mode.fdseParameters initial) = fullySupported
modeSupport Mode.ibufParameters = fullySupported
modeSupport Mode.obufParameters = fullySupported
modeSupport Mode.obufdsParameters = fullySupported
modeSupport Mode.bufgParameters = fullySupported
modeSupport Mode.bufgceParameters = fullySupported

semanticEvidenceFor : ∀ {kind}
  → (mode : Mode.CoreParameters kind) → ModeSemanticEvidence mode
semanticEvidenceFor (Mode.lut1Parameters table) =
  executableCombinational (Handler.lutHandler table) refl
semanticEvidenceFor (Mode.lut2Parameters table) =
  executableCombinational (Handler.lutHandler table) refl
semanticEvidenceFor (Mode.lut3Parameters table) =
  executableCombinational (Handler.lutHandler table) refl
semanticEvidenceFor (Mode.lut4Parameters table) =
  executableCombinational (Handler.lutHandler table) refl
semanticEvidenceFor (Mode.lut5Parameters table) =
  executableCombinational (Handler.lutHandler table) refl
semanticEvidenceFor (Mode.lut6Parameters table) =
  executableCombinational (Handler.lutHandler table) refl
semanticEvidenceFor Mode.muxf7Parameters =
  executableCombinational Handler.muxF7Handler refl
semanticEvidenceFor Mode.muxf8Parameters =
  executableCombinational Handler.muxF7Handler refl
semanticEvidenceFor Mode.carry4Parameters =
  executableCombinational Handler.carry4Handler refl
semanticEvidenceFor (Mode.fdreParameters initial) =
  executableState (Handler.fdreHandler initial)
semanticEvidenceFor (Mode.fdseParameters initial) =
  executableState (Handler.fdseHandler initial)
semanticEvidenceFor Mode.ibufParameters =
  executableCombinational Handler.identityHandler refl
semanticEvidenceFor Mode.obufParameters =
  executableCombinational Handler.identityHandler refl
semanticEvidenceFor Mode.obufdsParameters =
  executableCombinational Handler.obufdsHandler refl
semanticEvidenceFor Mode.bufgParameters =
  executableCombinational Handler.identityHandler refl
semanticEvidenceFor Mode.bufgceParameters =
  executableCombinational Handler.bufgceHandler refl

mode-trace-executable : ∀ {kind}
  → (mode : Mode.CoreParameters kind)
  → traceExecutable? (Registry.modeTraceability kind mode) ≡ true
mode-trace-executable (Mode.lut1Parameters table) = refl
mode-trace-executable (Mode.lut2Parameters table) = refl
mode-trace-executable (Mode.lut3Parameters table) = refl
mode-trace-executable (Mode.lut4Parameters table) = refl
mode-trace-executable (Mode.lut5Parameters table) = refl
mode-trace-executable (Mode.lut6Parameters table) = refl
mode-trace-executable Mode.muxf7Parameters = refl
mode-trace-executable Mode.muxf8Parameters = refl
mode-trace-executable Mode.carry4Parameters = refl
mode-trace-executable (Mode.fdreParameters initial) = refl
mode-trace-executable (Mode.fdseParameters initial) = refl
mode-trace-executable Mode.ibufParameters = refl
mode-trace-executable Mode.obufParameters = refl
mode-trace-executable Mode.obufdsParameters = refl
mode-trace-executable Mode.bufgParameters = refl
mode-trace-executable Mode.bufgceParameters = refl

mode-trace-official : ∀ {kind}
  → (mode : Mode.CoreParameters kind)
  → traceOfficial? (Registry.modeTraceability kind mode) ≡ true
mode-trace-official (Mode.lut1Parameters table) = refl
mode-trace-official (Mode.lut2Parameters table) = refl
mode-trace-official (Mode.lut3Parameters table) = refl
mode-trace-official (Mode.lut4Parameters table) = refl
mode-trace-official (Mode.lut5Parameters table) = refl
mode-trace-official (Mode.lut6Parameters table) = refl
mode-trace-official Mode.muxf7Parameters = refl
mode-trace-official Mode.muxf8Parameters = refl
mode-trace-official Mode.carry4Parameters = refl
mode-trace-official (Mode.fdreParameters initial) = refl
mode-trace-official (Mode.fdseParameters initial) = refl
mode-trace-official Mode.ibufParameters = refl
mode-trace-official Mode.obufParameters = refl
mode-trace-official Mode.obufdsParameters = refl
mode-trace-official Mode.bufgParameters = refl
mode-trace-official Mode.bufgceParameters = refl

record ExactModeCapability {kind : Architecture.PrimitiveKind}
  (mode : Mode.CoreParameters kind) : Type₀ where
  constructor exactModeCapability
  field
    admittedSupport : SupportStatus
    conditionalPremise : ConditionalPremise
    semanticEvidence : ModeSemanticEvidence mode
    support-is-exact : admittedSupport ≡ modeSupport mode
    premise-is-exact : conditionalPremise ≡ modePremise mode
    traceability : RuleTraceability
    traceability-is-canonical :
      traceability ≡ Registry.modeTraceability kind mode
    traceability-is-executable : traceExecutable? traceability ≡ true

open ExactModeCapability public