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

module Spartan6.Netlist.NormalizeCombinationalSoundness where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeCombinational as Normalize
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.LUT as LUT
open import Spartan6.Validation.CheckResult
  using (rejected≢accepted; accepted-injective)
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
import Spartan6.Validation.Raw as Validation

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

-- The exact raw/structural boundary stored by a candidate.

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

normaliseCombinational-preserves-boundary :
  ∀ checked candidate
  → Normalize.normaliseCombinational checked
    ≡ Diagnostic.accepted candidate
  → candidateBoundary candidate ≡ checked
normaliseCombinational-preserves-boundary
  (design , structural-proof) candidate result
  with Normalize.checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted tt
  with Normalize.collectInputNets (Raw.rawTopPorts design)
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted input-net-ids
  with Normalize.processInstances
    (Raw.rawInstances design) (Normalize.initialBuilder input-net-ids)
...   | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted current
  with Normalize.collectOutputWires
    (Raw.rawTopPorts design) (Normalize.builderBindings current)
...     | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
...     | Diagnostic.accepted outputs =
  sym (cong candidateBoundary (accepted-injective result))

normaliseCombinational-preserves-source :
  ∀ checked candidate
  → Normalize.normaliseCombinational checked
    ≡ Diagnostic.accepted candidate
  → Normalize.candidateSource candidate ≡ fst checked
normaliseCombinational-preserves-source checked candidate result =
  cong fst
    (normaliseCombinational-preserves-boundary checked candidate result)

-- Zero registers are intrinsic in candidateNetlist's CheckedNetlist index.
-- These two field equalities expose the type-level fact to clients that only
-- inspect the netlist record.

candidate-next-is-empty : (candidate : Normalize.CheckedCombinationalCandidate)
  → Checked.checkedNext (Normalize.candidateNetlist candidate) ≡ []
candidate-next-is-empty = Normalize.candidate-next-is-empty

record ZeroRegisterInvariant
  (candidate : Normalize.CheckedCombinationalCandidate) : Type₀ where
  constructor zeroRegisterInvariant
  field
    initial-is-empty :
      Checked.checkedInitial (Normalize.candidateNetlist candidate) ≡ []
    next-is-empty :
      Checked.checkedNext (Normalize.candidateNetlist candidate) ≡ []

open ZeroRegisterInvariant public

candidate-has-zero-registers :
  (candidate : Normalize.CheckedCombinationalCandidate)
  → ZeroRegisterInvariant candidate
candidate-has-zero-registers candidate =
  zeroRegisterInvariant
    (Normalize.candidate-has-no-registers candidate)
    (candidate-next-is-empty candidate)

normaliseCombinational-has-zero-registers :
  ∀ checked candidate
  → Normalize.normaliseCombinational checked
    ≡ Diagnostic.accepted candidate
  → ZeroRegisterInvariant candidate
normaliseCombinational-has-zero-registers checked candidate result =
  candidate-has-zero-registers candidate

-- AcceptedInstanceMode records both the closed raw kind and the exact
-- successful parameter-normalization boundary used by processInstance.

data AcceptedInstanceMode : Raw.RawInstance → Type₀ where
  acceptedLUT1 :
    ∀ {name ports raw-parameters initial-bit table}
    → Parameter.normaliseCoreParameters
        Architecture.LUT1 name raw-parameters initial-bit
      ≡ Diagnostic.accepted (Parameter.lut1Parameters table)
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.LUT1)
          ports raw-parameters initial-bit)

  acceptedLUT2 :
    ∀ {name ports raw-parameters initial-bit table}
    → Parameter.normaliseCoreParameters
        Architecture.LUT2 name raw-parameters initial-bit
      ≡ Diagnostic.accepted (Parameter.lut2Parameters table)
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.LUT2)
          ports raw-parameters initial-bit)

  acceptedLUT3 :
    ∀ {name ports raw-parameters initial-bit table}
    → Parameter.normaliseCoreParameters
        Architecture.LUT3 name raw-parameters initial-bit
      ≡ Diagnostic.accepted (Parameter.lut3Parameters table)
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.LUT3)
          ports raw-parameters initial-bit)

  acceptedLUT4 :
    ∀ {name ports raw-parameters initial-bit table}
    → Parameter.normaliseCoreParameters
        Architecture.LUT4 name raw-parameters initial-bit
      ≡ Diagnostic.accepted (Parameter.lut4Parameters table)
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.LUT4)
          ports raw-parameters initial-bit)

  acceptedLUT5 :
    ∀ {name ports raw-parameters initial-bit table}
    → Parameter.normaliseCoreParameters
        Architecture.LUT5 name raw-parameters initial-bit
      ≡ Diagnostic.accepted (Parameter.lut5Parameters table)
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.LUT5)
          ports raw-parameters initial-bit)

  acceptedLUT6 :
    ∀ {name ports raw-parameters initial-bit table}
    → Parameter.normaliseCoreParameters
        Architecture.LUT6 name raw-parameters initial-bit
      ≡ Diagnostic.accepted (Parameter.lut6Parameters table)
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.LUT6)
          ports raw-parameters initial-bit)

  acceptedMUXF7 :
    ∀ {name ports raw-parameters initial-bit}
    → Parameter.normaliseCoreParameters
        Architecture.MUXF7 name raw-parameters initial-bit
      ≡ Diagnostic.accepted Parameter.muxf7Parameters
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.MUXF7)
          ports raw-parameters initial-bit)

  acceptedMUXF8 :
    ∀ {name ports raw-parameters initial-bit}
    → Parameter.normaliseCoreParameters
        Architecture.MUXF8 name raw-parameters initial-bit
      ≡ Diagnostic.accepted Parameter.muxf8Parameters
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.MUXF8)
          ports raw-parameters initial-bit)

  acceptedIBUF :
    ∀ {name ports raw-parameters initial-bit}
    → Parameter.normaliseCoreParameters
        Architecture.IBUF name raw-parameters initial-bit
      ≡ Diagnostic.accepted Parameter.ibufParameters
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.IBUF)
          ports raw-parameters initial-bit)

  acceptedOBUF :
    ∀ {name ports raw-parameters initial-bit}
    → Parameter.normaliseCoreParameters
        Architecture.OBUF name raw-parameters initial-bit
      ≡ Diagnostic.accepted Parameter.obufParameters
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.OBUF)
          ports raw-parameters initial-bit)

  acceptedBUFG :
    ∀ {name ports raw-parameters initial-bit}
    → Parameter.normaliseCoreParameters
        Architecture.BUFG name raw-parameters initial-bit
      ≡ Diagnostic.accepted Parameter.bufgParameters
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.BUFG)
          ports raw-parameters initial-bit)

  acceptedBUFGCE :
    ∀ {name ports raw-parameters initial-bit}
    → Parameter.normaliseCoreParameters
        Architecture.BUFGCE name raw-parameters initial-bit
      ≡ Diagnostic.accepted Parameter.bufgceParameters
    → AcceptedInstanceMode
        (Raw.rawInstance
          name
          (Raw.knownPrimitive Architecture.BUFGCE)
          ports raw-parameters initial-bit)

processInstance-mode-sound :
  ∀ item {inputCount}
    (current next : Normalize.Builder inputCount)
  → Normalize.processInstance item current ≡ Diagnostic.accepted next
  → AcceptedInstanceMode item
processInstance-mode-sound
  (Raw.rawInstance name (Raw.unknownPrimitive unknown)
    ports raw-parameters initial-bit)
  current next result =
  Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.LUT1)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.LUT1 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.LUT1 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted (Parameter.lut1Parameters table)
      | [ parameter-path ]ᵢ =
  acceptedLUT1 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.LUT2)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.LUT2 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.LUT2 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted (Parameter.lut2Parameters table)
      | [ parameter-path ]ᵢ =
  acceptedLUT2 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.LUT3)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.LUT3 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.LUT3 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted (Parameter.lut3Parameters table)
      | [ parameter-path ]ᵢ =
  acceptedLUT3 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.LUT4)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.LUT4 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.LUT4 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted (Parameter.lut4Parameters table)
      | [ parameter-path ]ᵢ =
  acceptedLUT4 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.LUT5)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.LUT5 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.LUT5 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted (Parameter.lut5Parameters table)
      | [ parameter-path ]ᵢ =
  acceptedLUT5 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.LUT6)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.LUT6 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.LUT6 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted (Parameter.lut6Parameters table)
      | [ parameter-path ]ᵢ =
  acceptedLUT6 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.MUXF7)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.MUXF7 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.MUXF7 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted Parameter.muxf7Parameters
      | [ parameter-path ]ᵢ =
  acceptedMUXF7 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.MUXF8)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.MUXF8 name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.MUXF8 name raw-parameters)
        initial-bit
...   | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted Parameter.muxf8Parameters
      | [ parameter-path ]ᵢ =
  acceptedMUXF8 parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.CARRY4)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.FDRE)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.FDSE)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.SRL16E)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.RAM64X1S)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.IBUF)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.IBUF name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.IBUF name raw-parameters)
        initial-bit
... | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted Parameter.ibufParameters
    | [ parameter-path ]ᵢ =
  acceptedIBUF parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.OBUF)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.OBUF name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.OBUF name raw-parameters)
        initial-bit
... | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted Parameter.obufParameters
    | [ parameter-path ]ᵢ =
  acceptedOBUF parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.OBUFDS)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.OBUFT)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.BUFG)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.BUFG name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.BUFG name raw-parameters)
        initial-bit
... | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted Parameter.bufgParameters
    | [ parameter-path ]ᵢ =
  acceptedBUFG parameter-path
processInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.BUFGCE)
    ports raw-parameters initial-bit)
  current next result
  with Parameter.normaliseCoreParameters
    Architecture.BUFGCE name raw-parameters initial-bit
     | inspect
        (Parameter.normaliseCoreParameters
          Architecture.BUFGCE name raw-parameters)
        initial-bit
... | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted Parameter.bufgceParameters
    | [ parameter-path ]ᵢ =
  acceptedBUFGCE parameter-path

-- A list-level characterization used by the top-level normalizer theorem.

data AllAcceptedInstanceModes : List Raw.RawInstance → Type₀ where
  noAcceptedInstances : AllAcceptedInstanceModes []ᴸ
  acceptedInstanceAndRest : ∀ {item items}
    → AcceptedInstanceMode item
    → AllAcceptedInstanceModes items
    → AllAcceptedInstanceModes (item ∷ᴸ items)

processInstances-modes-sound :
  ∀ {inputCount} items
    (current final : Normalize.Builder inputCount)
  → Normalize.processInstances items current ≡ Diagnostic.accepted final
  → AllAcceptedInstanceModes items
processInstances-modes-sound []ᴸ current final result =
  noAcceptedInstances
processInstances-modes-sound (item ∷ᴸ items) current final result
  with Normalize.processInstance item current
     | inspect (Normalize.processInstance item) current
... | Diagnostic.rejected diagnostics | [ step-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted next | [ step-path ]ᵢ =
  acceptedInstanceAndRest
    (processInstance-mode-sound item current next step-path)
    (processInstances-modes-sound items next final result)

normaliseCombinational-modes-sound :
  ∀ checked candidate
  → Normalize.normaliseCombinational checked
    ≡ Diagnostic.accepted candidate
  → AllAcceptedInstanceModes (Raw.rawInstances (fst checked))
normaliseCombinational-modes-sound
  (design , structural-proof) candidate result
  with Normalize.checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted tt
  with Normalize.collectInputNets (Raw.rawTopPorts design)
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted input-net-ids
  with Normalize.processInstances
         (Raw.rawInstances design)
         (Normalize.initialBuilder input-net-ids)
     | inspect
        (Normalize.processInstances (Raw.rawInstances design))
        (Normalize.initialBuilder input-net-ids)
...   | Diagnostic.rejected diagnostics | [ process-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted current | [ process-path ]ᵢ
  with Normalize.collectOutputWires
    (Raw.rawTopPorts design) (Normalize.builderBindings current)
...     | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
...     | Diagnostic.accepted outputs =
  processInstances-modes-sound
    (Raw.rawInstances design)
    (Normalize.initialBuilder input-net-ids)
    current
    process-path