Spartan6.Netlist.NormalizeRegisterSoundness

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

module Spartan6.Netlist.NormalizeRegisterSoundness where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeRegister as Normalize
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.TopInterface as TopInterface
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

open import Spartan6.Validation.CheckResult
  using (rejected≢accepted; accepted-injective)
open import Spartan6.Validation.ParameterSoundness
  using (ScalarInitial; scalarDefault; scalarExplicit)
open import Cubical.Foundations.Path using (inspect; [_]ᵢ)
import Cubical.Data.Empty as Empty

-- CanonicalRegisterMode states the exact scalar raw parameter boundary that
-- can produce an accepted register mode.  In particular, there are no string
-- parameters, and the optional scalar bit is either preserved or replaced by
-- the primitive's documented default.

data CanonicalRegisterMode
  : Raw.RawInstance → Normalize.RegisterMode → Type₀ where
  canonicalFDRE : ∀ {name ports initial-bit value}
    → ScalarInitial low initial-bit value
    → CanonicalRegisterMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.FDRE)
          ports
          []ᴸ
          initial-bit)
        (Normalize.fdreMode value)

  canonicalFDSE : ∀ {name ports initial-bit value}
    → ScalarInitial high initial-bit value
    → CanonicalRegisterMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.FDSE)
          ports
          []ᴸ
          initial-bit)
        (Normalize.fdseMode value)

normaliseRegisterMode-sound : ∀ item mode
  → Normalize.normaliseRegisterMode item ≡ Diagnostic.accepted mode
  → CanonicalRegisterMode item mode
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDRE) ports []ᴸ nothing)
  mode result
  with accepted-injective result
... | mode-path =
  subst
    (CanonicalRegisterMode
      (Raw.rawInstance name
        (Raw.knownPrimitive Architecture.FDRE) ports []ᴸ nothing))
    mode-path
    (canonicalFDRE scalarDefault)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDRE) ports []ᴸ (just bit))
  mode result
  with accepted-injective result
... | mode-path =
  subst
    (CanonicalRegisterMode
      (Raw.rawInstance name
        (Raw.knownPrimitive Architecture.FDRE) ports []ᴸ (just bit)))
    mode-path
    (canonicalFDRE (scalarExplicit bit))
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDRE)
    ports (parameter ∷ᴸ parameters) nothing)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDRE)
    ports (parameter ∷ᴸ parameters) (just bit))
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDSE) ports []ᴸ nothing)
  mode result
  with accepted-injective result
... | mode-path =
  subst
    (CanonicalRegisterMode
      (Raw.rawInstance name
        (Raw.knownPrimitive Architecture.FDSE) ports []ᴸ nothing))
    mode-path
    (canonicalFDSE scalarDefault)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDSE) ports []ᴸ (just bit))
  mode result
  with accepted-injective result
... | mode-path =
  subst
    (CanonicalRegisterMode
      (Raw.rawInstance name
        (Raw.knownPrimitive Architecture.FDSE) ports []ᴸ (just bit)))
    mode-path
    (canonicalFDSE (scalarExplicit bit))
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDSE)
    ports (parameter ∷ᴸ parameters) nothing)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.FDSE)
    ports (parameter ∷ᴸ parameters) (just bit))
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name (Raw.unknownPrimitive unknown) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.LUT1) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.LUT2) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.LUT3) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.LUT4) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.LUT5) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.LUT6) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.MUXF7) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.MUXF8) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.CARRY4) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.SRL16E) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.RAM64X1S) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.IBUF) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.OBUF) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.OBUFDS) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.OBUFT) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.BUFG) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)
normaliseRegisterMode-sound
  (Raw.rawInstance name
    (Raw.knownPrimitive Architecture.BUFGCE) ports parameters initial-bit)
  mode result =
  Empty.rec (rejected≢accepted result)

canonical-register-kind : ∀ {item mode}
  → CanonicalRegisterMode item mode
  → (Raw.rawInstanceKind item ≡ Raw.knownPrimitive Architecture.FDRE)
    ⊎ (Raw.rawInstanceKind item ≡ Raw.knownPrimitive Architecture.FDSE)
canonical-register-kind (canonicalFDRE initial) = inl refl
canonical-register-kind (canonicalFDSE initial) = inr refl

-- A witness records every successful decision that contributes to the final
-- build.  It is intentionally stronger than merely restating acceptance.

record RegisterBuildWitness
  (design : Raw.RawDesign)
  (structural-proof : Validation.StructurallyValid design)
  (candidate : Normalize.CheckedRegisterCandidate)
  : Type₀ where
  field
    registerItem : Raw.RawInstance
    exactlyOneInstance :
      Raw.rawInstances design ≡ registerItem ∷ᴸ []ᴸ

    registerPorts : Normalize.RegisterPorts
    portsParsed :
      Normalize.parseRegisterPorts (Raw.rawInstancePorts registerItem)
      ≡ just registerPorts

    registerMode : Normalize.RegisterMode
    modeNormalised :
      Normalize.normaliseRegisterMode registerItem
      ≡ Diagnostic.accepted registerMode
    canonicalMode : CanonicalRegisterMode registerItem registerMode

    inputNets : List Raw.NetId
    inputNetsCollected :
      TopInterface.collectInputNets (Raw.rawTopPorts design)
      ≡ Diagnostic.accepted inputNets

    outputNet : Raw.NetId
    outputNetAccepted :
      Normalize.outputNet registerItem registerPorts
      ≡ Diagnostic.accepted outputNet

    clockIndex : Fin (lengthList inputNets)
    clockAccepted :
      Normalize.clockInput inputNets (Normalize.registerC registerPorts)
      ≡ Diagnostic.accepted clockIndex

    dataWire : Checked.Wire (lengthList inputNets) 1 0
    dataAccepted :
      Normalize.resolveBasePort
        inputNets outputNet "register.D" (Normalize.registerD registerPorts)
      ≡ Diagnostic.accepted dataWire

    enableWire : Checked.Wire (lengthList inputNets) 1 0
    enableAccepted :
      Normalize.resolveBasePort
        inputNets outputNet "register.CE" (Normalize.registerCE registerPorts)
      ≡ Diagnostic.accepted enableWire

    controlWire : Checked.Wire (lengthList inputNets) 1 0
    controlAccepted :
      Normalize.resolveBasePort
        inputNets outputNet "register.control"
        (Normalize.registerControl registerPorts)
      ≡ Diagnostic.accepted controlWire

    outputWires : List (Checked.Wire (lengthList inputNets) 1 0)
    outputsAccepted :
      Normalize.collectTopOutputs
        inputNets outputNet (Raw.rawTopPorts design)
      ≡ Diagnostic.accepted outputWires

    candidateBuilt :
      candidate
      ≡ Normalize.buildCandidate
          design structural-proof registerItem registerPorts registerMode
          inputNets outputNet clockIndex
          dataWire enableWire controlWire outputWires

open RegisterBuildWitness public

normaliseParsedRegister-witness :
  ∀ design structural-proof item ports mode candidate
  → Raw.rawInstances design ≡ item ∷ᴸ []ᴸ
  → Normalize.parseRegisterPorts (Raw.rawInstancePorts item) ≡ just ports
  → Normalize.normaliseRegisterMode item ≡ Diagnostic.accepted mode
  → CanonicalRegisterMode item mode
  → Normalize.normaliseParsedRegister
      design structural-proof item ports mode
    ≡ Diagnostic.accepted candidate
  → RegisterBuildWitness design structural-proof candidate
normaliseParsedRegister-witness
  design structural-proof item ports mode candidate
  one-instance ports-path mode-path canonical-mode result
  with TopInterface.collectInputNets (Raw.rawTopPorts design)
     | inspect TopInterface.collectInputNets (Raw.rawTopPorts design)
... | Diagnostic.rejected diagnostics | [ inputs-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted input-nets | [ inputs-path ]ᵢ
  with Normalize.outputNet item ports
     | inspect (Normalize.outputNet item) ports
...   | Diagnostic.rejected diagnostics | [ output-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted q-net | [ output-path ]ᵢ
  with Normalize.clockInput input-nets (Normalize.registerC ports)
     | inspect (Normalize.clockInput input-nets) (Normalize.registerC ports)
...     | Diagnostic.rejected diagnostics | [ clock-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...     | Diagnostic.accepted clock-index | [ clock-path ]ᵢ
  with Normalize.resolveBasePort
         input-nets q-net "register.D" (Normalize.registerD ports)
     | inspect
         (Normalize.resolveBasePort input-nets q-net "register.D")
         (Normalize.registerD ports)
...       | Diagnostic.rejected diagnostics | [ data-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...       | Diagnostic.accepted data-wire | [ data-path ]ᵢ
  with Normalize.resolveBasePort
         input-nets q-net "register.CE" (Normalize.registerCE ports)
     | inspect
         (Normalize.resolveBasePort input-nets q-net "register.CE")
         (Normalize.registerCE ports)
...         | Diagnostic.rejected diagnostics | [ enable-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...         | Diagnostic.accepted enable-wire | [ enable-path ]ᵢ
  with Normalize.resolveBasePort
         input-nets q-net "register.control"
         (Normalize.registerControl ports)
     | inspect
         (Normalize.resolveBasePort input-nets q-net "register.control")
         (Normalize.registerControl ports)
...           | Diagnostic.rejected diagnostics | [ control-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...           | Diagnostic.accepted control-wire | [ control-path ]ᵢ
  with Normalize.collectTopOutputs
         input-nets q-net (Raw.rawTopPorts design)
     | inspect
         (Normalize.collectTopOutputs input-nets q-net)
         (Raw.rawTopPorts design)
...             | Diagnostic.rejected diagnostics | [ outputs-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...             | Diagnostic.accepted outputs | [ outputs-path ]ᵢ
  with accepted-injective result
...               | build-is-candidate =
  record
    { registerItem = item
    ; exactlyOneInstance = one-instance
    ; registerPorts = ports
    ; portsParsed = ports-path
    ; registerMode = mode
    ; modeNormalised = mode-path
    ; canonicalMode = canonical-mode
    ; inputNets = input-nets
    ; inputNetsCollected = inputs-path
    ; outputNet = q-net
    ; outputNetAccepted = output-path
    ; clockIndex = clock-index
    ; clockAccepted = clock-path
    ; dataWire = data-wire
    ; dataAccepted = data-path
    ; enableWire = enable-wire
    ; enableAccepted = enable-path
    ; controlWire = control-wire
    ; controlAccepted = control-path
    ; outputWires = outputs
    ; outputsAccepted = outputs-path
    ; candidateBuilt = sym build-is-candidate
    }

normaliseRegisterItem-witness :
  ∀ design structural-proof item candidate
  → Raw.rawInstances design ≡ item ∷ᴸ []ᴸ
  → Normalize.normaliseRegisterItem design structural-proof item
    ≡ Diagnostic.accepted candidate
  → RegisterBuildWitness design structural-proof candidate
normaliseRegisterItem-witness
  design structural-proof item candidate one-instance result
  with Normalize.parseRegisterPorts (Raw.rawInstancePorts item)
     | inspect Normalize.parseRegisterPorts (Raw.rawInstancePorts item)
... | nothing | [ ports-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | just ports | [ ports-path ]ᵢ
  with Normalize.normaliseRegisterMode item
     | inspect Normalize.normaliseRegisterMode item
...   | Diagnostic.rejected diagnostics | [ mode-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted mode | [ mode-path ]ᵢ =
  normaliseParsedRegister-witness
    design structural-proof item ports mode candidate
    one-instance ports-path mode-path
    (normaliseRegisterMode-sound item mode mode-path)
    result

normaliseSingleRegister-witness :
  ∀ checked candidate
  → Normalize.normaliseSingleRegister checked
    ≡ Diagnostic.accepted candidate
  → RegisterBuildWitness (fst checked) (snd checked) candidate
normaliseSingleRegister-witness
  (Raw.rawDesign target top-ports (item ∷ᴸ []ᴸ) , structural-proof)
  candidate result
  with TopInterface.checkDevelopmentTarget
         (Raw.rawDesign target top-ports (item ∷ᴸ []ᴸ))
     | inspect TopInterface.checkDevelopmentTarget
         (Raw.rawDesign target top-ports (item ∷ᴸ []ᴸ))
... | Diagnostic.rejected diagnostics | [ target-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted tt | [ target-path ]ᵢ =
  normaliseRegisterItem-witness
    (Raw.rawDesign target top-ports (item ∷ᴸ []ᴸ))
    structural-proof item candidate refl result
normaliseSingleRegister-witness
  (Raw.rawDesign target top-ports []ᴸ , structural-proof)
  candidate result =
  Empty.rec (rejected≢accepted result)
normaliseSingleRegister-witness
  (Raw.rawDesign target top-ports (first ∷ᴸ second ∷ᴸ rest) ,
   structural-proof)
  candidate result =
  Empty.rec (rejected≢accepted result)

candidateBoundary : Normalize.CheckedRegisterCandidate
                  → Validation.StructurallyChecked
candidateBoundary candidate =
  Normalize.candidateSource candidate
  , Normalize.candidateStructuralProof candidate

candidate-boundary-preserved :
  ∀ {design structural-proof candidate}
  → (witness : RegisterBuildWitness design structural-proof candidate)
  → candidateBoundary candidate ≡ (design , structural-proof)
candidate-boundary-preserved witness =
  cong candidateBoundary (candidateBuilt witness)

candidate-source-preserved :
  ∀ {design structural-proof candidate}
  → RegisterBuildWitness design structural-proof candidate
  → Normalize.candidateSource candidate ≡ design
candidate-source-preserved witness =
  cong Normalize.candidateSource (candidateBuilt witness)

accepted-canonical-register :
  ∀ {design structural-proof candidate}
  → (witness : RegisterBuildWitness design structural-proof candidate)
  → Σ Raw.RawInstance λ item
    → (Raw.rawInstances design ≡ item ∷ᴸ []ᴸ)
    × Σ Normalize.RegisterMode λ mode
      → CanonicalRegisterMode item mode
accepted-canonical-register witness =
  registerItem witness
  , exactlyOneInstance witness
  , registerMode witness
  , canonicalMode witness

-- The indices in these packages make the one-state-bit and two-local-node
-- claims explicit without erasing their dependent input count.

InputClock : Type₀
InputClock = Σ ℕ Fin

NodesOfOneRegister : Type₀
NodesOfOneRegister = Σ ℕ λ input-count → Checked.Nodes input-count 1 2

NextOfOneRegister : Type₀
NextOfOneRegister =
  Σ ℕ λ input-count
    → Vec (Checked.Wire input-count 1 2) 1

candidateInputClock : Normalize.CheckedRegisterCandidate → InputClock
candidateInputClock candidate =
  Normalize.candidateInputCount candidate
  , Normalize.candidateClockInput candidate

candidateNodes : Normalize.CheckedRegisterCandidate → NodesOfOneRegister
candidateNodes candidate =
  Normalize.candidateInputCount candidate
  , Checked.checkedNodes (Normalize.candidateNetlist candidate)

candidateNext : Normalize.CheckedRegisterCandidate → NextOfOneRegister
candidateNext candidate =
  Normalize.candidateInputCount candidate
  , Checked.checkedNext (Normalize.candidateNetlist candidate)

candidate-initial-is-mode :
  ∀ {design structural-proof candidate}
  → (witness : RegisterBuildWitness design structural-proof candidate)
  → Checked.checkedInitial (Normalize.candidateNetlist candidate)
    ≡ Normalize.modeInitial (registerMode witness) ∷ []
candidate-initial-is-mode witness =
  cong
    (λ candidate →
      Checked.checkedInitial (Normalize.candidateNetlist candidate))
    (candidateBuilt witness)

candidate-has-two-register-nodes :
  ∀ {design structural-proof candidate}
  → (witness : RegisterBuildWitness design structural-proof candidate)
  → candidateNodes candidate
    ≡ (lengthList (inputNets witness)
       , Normalize.registerNodes
           (registerMode witness)
           (dataWire witness)
           (enableWire witness)
           (controlWire witness))
candidate-has-two-register-nodes witness =
  cong candidateNodes (candidateBuilt witness)

candidate-has-one-local-next :
  ∀ {design structural-proof candidate}
  → (witness : RegisterBuildWitness design structural-proof candidate)
  → candidateNext candidate
    ≡ (lengthList (inputNets witness)
       , Checked.localWire fzero ∷ [])
candidate-has-one-local-next witness =
  cong candidateNext (candidateBuilt witness)

candidate-records-clock-index :
  ∀ {design structural-proof candidate}
  → (witness : RegisterBuildWitness design structural-proof candidate)
  → candidateInputClock candidate
    ≡ (lengthList (inputNets witness) , clockIndex witness)
candidate-records-clock-index witness =
  cong candidateInputClock (candidateBuilt witness)

record RecordedTopLevelClock
  (design : Raw.RawDesign)
  (candidate : Normalize.CheckedRegisterCandidate)
  : Type₀ where
  field
    clockRegisterItem : Raw.RawInstance
    clockOnlyInstance :
      Raw.rawInstances design ≡ clockRegisterItem ∷ᴸ []ᴸ
    clockRegisterPorts : Normalize.RegisterPorts
    clockPortsParsed :
      Normalize.parseRegisterPorts
        (Raw.rawInstancePorts clockRegisterItem)
      ≡ just clockRegisterPorts
    collectedInputNets : List Raw.NetId
    collectedInputsAccepted :
      TopInterface.collectInputNets (Raw.rawTopPorts design)
      ≡ Diagnostic.accepted collectedInputNets
    recordedClockIndex : Fin (lengthList collectedInputNets)
    rawClockAccepted :
      Normalize.clockInput
        collectedInputNets (Normalize.registerC clockRegisterPorts)
      ≡ Diagnostic.accepted recordedClockIndex
    checkedClockRecorded :
      candidateInputClock candidate
      ≡ (lengthList collectedInputNets , recordedClockIndex)

open RecordedTopLevelClock public

accepted-records-top-level-clock :
  ∀ {design structural-proof candidate}
  → (witness : RegisterBuildWitness design structural-proof candidate)
  → RecordedTopLevelClock design candidate
accepted-records-top-level-clock witness =
  record
    { clockRegisterItem = registerItem witness
    ; clockOnlyInstance = exactlyOneInstance witness
    ; clockRegisterPorts = registerPorts witness
    ; clockPortsParsed = portsParsed witness
    ; collectedInputNets = inputNets witness
    ; collectedInputsAccepted = inputNetsCollected witness
    ; recordedClockIndex = clockIndex witness
    ; rawClockAccepted = clockAccepted witness
    ; checkedClockRecorded = candidate-records-clock-index witness
    }

-- The raw clock net identifier and top-port name are not fields of
-- CheckedRegisterCandidate; only the validated Fin index is retained.  The
-- existential normalization trace above is therefore the strongest direct
-- correspondence available without changing the existing candidate API.