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

module Spartan6.Netlist.NormalizeRegistersSoundness where

open import Spartan6.Prelude

import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeRegisterSoundness as SingleSoundness
import Spartan6.Netlist.NormalizeRegisters as Normalize
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.RegisterMode as Single
import Spartan6.Netlist.TopInterface as TopInterface
open import Spartan6.Validation.CheckResult
  using (rejected≢accepted; accepted-injective)
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

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

-- A successful descriptor remembers every decision that connects it to the
-- raw instance at the same position.  CanonicalRegisterMode adds the exact
-- FDRE/FDSE scalar-parameter boundary proved by the single-register layer.

record CanonicalDescriptor
  (item : Raw.RawInstance)
  (descriptor : Normalize.RegisterDescriptor)
  : Type₀ where
  field
    canonicalPorts : Single.RegisterPorts
    canonicalPortsParsed :
      Single.parseRegisterPorts (Raw.rawInstancePorts item)
      ≡ just canonicalPorts

    canonicalMode : Single.RegisterMode
    canonicalModeNormalised :
      Single.normaliseRegisterMode item
      ≡ Diagnostic.accepted canonicalMode
    canonicalModeEvidence :
      SingleSoundness.CanonicalRegisterMode item canonicalMode

    canonicalQNet : Raw.NetId
    canonicalQAccepted :
      Single.outputNet item canonicalPorts
      ≡ Diagnostic.accepted canonicalQNet

    canonicalDescriptorBuilt :
      descriptor
      ≡ Normalize.registerDescriptor
          item canonicalPorts canonicalMode canonicalQNet

open CanonicalDescriptor public

normaliseDescriptor-sound : ∀ item descriptor
  → Normalize.normaliseDescriptor item ≡ Diagnostic.accepted descriptor
  → CanonicalDescriptor item descriptor
normaliseDescriptor-sound item descriptor result
  with Single.parseRegisterPorts (Raw.rawInstancePorts item)
     | inspect Single.parseRegisterPorts (Raw.rawInstancePorts item)
... | nothing | [ ports-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | just ports | [ ports-path ]ᵢ
  with Single.normaliseRegisterMode item
     | inspect Single.normaliseRegisterMode item
...   | Diagnostic.rejected diagnostics | [ mode-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted mode | [ mode-path ]ᵢ
  with Single.outputNet item ports
     | inspect (Single.outputNet item) ports
...     | Diagnostic.rejected diagnostics | [ output-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...     | Diagnostic.accepted q-net | [ output-path ]ᵢ
  with accepted-injective result
...       | built-is-descriptor =
  record
    { canonicalPorts = ports
    ; canonicalPortsParsed = ports-path
    ; canonicalMode = mode
    ; canonicalModeNormalised = mode-path
    ; canonicalModeEvidence =
        SingleSoundness.normaliseRegisterMode-sound item mode mode-path
    ; canonicalQNet = q-net
    ; canonicalQAccepted = output-path
    ; canonicalDescriptorBuilt = sym built-is-descriptor
    }

-- Pointwise correspondence preserves order as well as membership: every
-- accepted descriptor was produced from exactly the raw instance occupying
-- the same list position.

data CanonicalDescriptorList
  : List Raw.RawInstance → List Normalize.RegisterDescriptor → Type₀ where
  canonicalDescriptorsNil : CanonicalDescriptorList []ᴸ []ᴸ
  canonicalDescriptorsCons : ∀ {item items descriptor descriptors}
    → CanonicalDescriptor item descriptor
    → CanonicalDescriptorList items descriptors
    → CanonicalDescriptorList
        (item ∷ᴸ items) (descriptor ∷ᴸ descriptors)

normaliseDescriptors-sound : ∀ items descriptors
  → Normalize.normaliseDescriptors items
    ≡ Diagnostic.accepted descriptors
  → CanonicalDescriptorList items descriptors
normaliseDescriptors-sound []ᴸ descriptors result
  with accepted-injective result
... | empty-is-descriptors =
  subst
    (CanonicalDescriptorList []ᴸ)
    empty-is-descriptors
    canonicalDescriptorsNil
normaliseDescriptors-sound (item ∷ᴸ items) descriptors result
  with Normalize.normaliseDescriptor item
     | inspect Normalize.normaliseDescriptor item
... | Diagnostic.rejected diagnostics | [ descriptor-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted descriptor | [ descriptor-path ]ᵢ
  with Normalize.normaliseDescriptors items
     | inspect Normalize.normaliseDescriptors items
...   | Diagnostic.rejected diagnostics | [ descriptors-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted rest | [ descriptors-path ]ᵢ
  with accepted-injective result
...     | built-is-descriptors =
  subst
    (CanonicalDescriptorList (item ∷ᴸ items))
    built-is-descriptors
    (canonicalDescriptorsCons
      (normaliseDescriptor-sound item descriptor descriptor-path)
      (normaliseDescriptors-sound items rest descriptors-path))

data NonemptyList {A : Type₀} : List A → Type₀ where
  listIsNonempty : ∀ {item items} → NonemptyList (item ∷ᴸ items)

-- This predicate mirrors buildNext constructor-for-constructor.  Each step
-- adds exactly the enable/data mux and the control/forced-value mux, then
-- records the latter as the next-state wire for that register.

data TwoMuxNext {inputCount registerCount : ℕ}
  : ∀ {count}
  → (resolved :
      Vec (Normalize.ResolvedRegister inputCount registerCount) count)
  → Normalize.BuiltNext inputCount registerCount count
  → Type₀ where
  noRegisterMuxes :
    TwoMuxNext [] (Normalize.builtNext  Checked.noNodes [])

  addRegisterMuxes :
    ∀ {count local-count}
      {nodes : Checked.Nodes inputCount registerCount local-count}
      {next-wires :
        Vec
          (Checked.Wire inputCount registerCount local-count)
          count}
      {resolveds :
        Vec (Normalize.ResolvedRegister inputCount registerCount) count}
      (resolved : Normalize.ResolvedRegister inputCount registerCount)
    → TwoMuxNext
        resolveds
        (Normalize.builtNext local-count nodes next-wires)
    → TwoMuxNext
        (resolved ∷ resolveds)
        (Normalize.builtNext
          (suc (suc local-count))
          ((nodes Checked.▻
            Checked.muxNode
              (Normalize.weakenBase (Normalize.resolvedEnable resolved))
              (Normalize.weakenBase (Normalize.resolvedCurrent resolved))
              (Normalize.weakenBase (Normalize.resolvedData resolved)))
           Checked.▻
            Checked.muxNode
              (Normalize.weakenBase (Normalize.resolvedControl resolved))
              (Checked.localWire fzero)
              (Checked.literalWire
                (Single.modeForcedValue
                  (Normalize.resolvedMode resolved))))
          (Checked.localWire fzero
           ∷ Normalize.liftNextTwice next-wires))

buildNext-two-muxes :
  ∀ {inputCount registerCount count}
    (resolveds :
      Vec (Normalize.ResolvedRegister inputCount registerCount) count)
  → TwoMuxNext resolveds (Normalize.buildNext resolveds)
buildNext-two-muxes [] = noRegisterMuxes
buildNext-two-muxes (resolved ∷ resolveds)
  with Normalize.buildNext resolveds
     | buildNext-two-muxes resolveds
... | Normalize.builtNext local-count nodes next-wires | rest-shape =
  addRegisterMuxes resolved rest-shape

twice : ℕ → ℕ
twice zero = zero
twice (suc count) = suc (suc (twice count))

buildNext-local-count :
  ∀ {inputCount registerCount count}
    (resolveds :
      Vec (Normalize.ResolvedRegister inputCount registerCount) count)
  → Normalize.builtLocalCount (Normalize.buildNext resolveds)
    ≡ twice count
buildNext-local-count [] = refl
buildNext-local-count (resolved ∷ resolveds)
  with Normalize.buildNext resolveds
     | buildNext-local-count resolveds
... | Normalize.builtNext local-count nodes next-wires | rest-count =
  cong (λ count → suc (suc count)) rest-count

record RegistersBuildWitness
  (design : Raw.RawDesign)
  (structural-proof : Validation.StructurallyValid design)
  (candidate : Normalize.CheckedRegistersCandidate)
  : Type₀ where
  field
    targetValidated :
      TopInterface.checkDevelopmentTarget design
      ≡ Diagnostic.accepted tt

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

    descriptors : List Normalize.RegisterDescriptor
    descriptorsNormalised :
      Normalize.normaliseDescriptors (Raw.rawInstances design)
      ≡ Diagnostic.accepted descriptors
    descriptorCanonicity :
      CanonicalDescriptorList (Raw.rawInstances design) descriptors
    descriptorsNonempty : NonemptyList descriptors

    clockIndex : Fin (lengthList inputNets)
    commonClockAccepted :
      Normalize.commonClock inputNets descriptors
      ≡ Diagnostic.accepted clockIndex

    resolvedRegisters :
      Vec
        (Normalize.ResolvedRegister
          (lengthList inputNets) (lengthList descriptors))
        (lengthList descriptors)
    descriptorsResolved :
      Normalize.resolveDescriptors inputNets descriptors descriptors
      ≡ Diagnostic.accepted resolvedRegisters

    outputWires :
      List
        (Checked.Wire
          (lengthList inputNets) (lengthList descriptors) )
    outputsCollected :
      Normalize.collectOutputs
        inputNets descriptors (Raw.rawTopPorts design)
      ≡ Diagnostic.accepted outputWires

    nextBuilderShape :
      TwoMuxNext resolvedRegisters
        (Normalize.buildNext resolvedRegisters)

    candidateBuilt :
      candidate
      ≡ Normalize.finishCandidate
          design structural-proof inputNets descriptors clockIndex
          resolvedRegisters (Normalize.buildNext resolvedRegisters)
          outputWires

open RegistersBuildWitness public

normaliseResolved-witness :
  ∀ design structural-proof input-nets descriptors clock-index candidate
  → TopInterface.checkDevelopmentTarget design
    ≡ Diagnostic.accepted tt
  → TopInterface.collectInputNets (Raw.rawTopPorts design)
    ≡ Diagnostic.accepted input-nets
  → Normalize.normaliseDescriptors (Raw.rawInstances design)
    ≡ Diagnostic.accepted descriptors
  → CanonicalDescriptorList (Raw.rawInstances design) descriptors
  → NonemptyList descriptors
  → Normalize.commonClock input-nets descriptors
    ≡ Diagnostic.accepted clock-index
  → Normalize.normaliseResolved
      design structural-proof input-nets descriptors clock-index
    ≡ Diagnostic.accepted candidate
  → RegistersBuildWitness design structural-proof candidate
normaliseResolved-witness
  design structural-proof input-nets descriptors clock-index candidate
  target-path inputs-path descriptors-path canonical-descriptors
  nonempty-descriptors clock-path result
  with Normalize.resolveDescriptors input-nets descriptors descriptors
     | inspect
         (Normalize.resolveDescriptors input-nets descriptors)
         descriptors
... | Diagnostic.rejected diagnostics | [ resolved-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted resolved | [ resolved-path ]ᵢ
  with Normalize.collectOutputs
         input-nets descriptors (Raw.rawTopPorts design)
     | inspect
         (Normalize.collectOutputs input-nets descriptors)
         (Raw.rawTopPorts design)
...   | Diagnostic.rejected diagnostics | [ outputs-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | Diagnostic.accepted outputs | [ outputs-path ]ᵢ
  with accepted-injective result
...     | built-is-candidate =
  record
    { targetValidated = target-path
    ; inputNets = input-nets
    ; inputNetsCollected = inputs-path
    ; descriptors = descriptors
    ; descriptorsNormalised = descriptors-path
    ; descriptorCanonicity = canonical-descriptors
    ; descriptorsNonempty = nonempty-descriptors
    ; clockIndex = clock-index
    ; commonClockAccepted = clock-path
    ; resolvedRegisters = resolved
    ; descriptorsResolved = resolved-path
    ; outputWires = outputs
    ; outputsCollected = outputs-path
    ; nextBuilderShape = buildNext-two-muxes resolved
    ; candidateBuilt = sym built-is-candidate
    }

normaliseWithDescriptors-witness :
  ∀ design structural-proof input-nets descriptors candidate
  → TopInterface.checkDevelopmentTarget design
    ≡ Diagnostic.accepted tt
  → TopInterface.collectInputNets (Raw.rawTopPorts design)
    ≡ Diagnostic.accepted input-nets
  → Normalize.normaliseDescriptors (Raw.rawInstances design)
    ≡ Diagnostic.accepted descriptors
  → CanonicalDescriptorList (Raw.rawInstances design) descriptors
  → Normalize.normaliseWithDescriptors
      design structural-proof input-nets descriptors
    ≡ Diagnostic.accepted candidate
  → RegistersBuildWitness design structural-proof candidate
normaliseWithDescriptors-witness
  design structural-proof input-nets []ᴸ candidate
  target-path inputs-path descriptors-path canonical-descriptors result =
  Empty.rec (rejected≢accepted result)
normaliseWithDescriptors-witness
  design structural-proof input-nets (descriptor ∷ᴸ descriptors) candidate
  target-path inputs-path descriptors-path canonical-descriptors result
  with Normalize.commonClock input-nets (descriptor ∷ᴸ descriptors)
     | inspect
         (Normalize.commonClock input-nets)
         (descriptor ∷ᴸ descriptors)
... | Diagnostic.rejected diagnostics | [ clock-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted clock-index | [ clock-path ]ᵢ =
  normaliseResolved-witness
    design structural-proof input-nets (descriptor ∷ᴸ descriptors)
    clock-index candidate
    target-path inputs-path descriptors-path canonical-descriptors
    listIsNonempty clock-path result

normaliseRegisters-witness : ∀ checked candidate
  → Normalize.normaliseRegisters checked
    ≡ Diagnostic.accepted candidate
  → RegistersBuildWitness (fst checked) (snd checked) candidate
normaliseRegisters-witness (design , structural-proof) candidate result
  with TopInterface.checkDevelopmentTarget design
     | inspect TopInterface.checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics | [ target-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted tt | [ target-path ]ᵢ
  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.normaliseDescriptors (Raw.rawInstances design)
     | inspect Normalize.normaliseDescriptors (Raw.rawInstances design)
...     | Diagnostic.rejected diagnostics | [ descriptors-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...     | Diagnostic.accepted descriptors | [ descriptors-path ]ᵢ =
  normaliseWithDescriptors-witness
    design structural-proof input-nets descriptors candidate
    target-path inputs-path descriptors-path
    (normaliseDescriptors-sound
      (Raw.rawInstances design) descriptors descriptors-path)
    result

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

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

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

InputClock : Type₀
InputClock = Σ ℕ Fin

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

candidate-clock-matches-common :
  ∀ {design structural-proof candidate}
  → (witness : RegistersBuildWitness design structural-proof candidate)
  → candidateInputClock candidate
    ≡ (lengthList (inputNets witness) , clockIndex witness)
candidate-clock-matches-common witness =
  cong candidateInputClock (candidateBuilt witness)

candidate-register-count-matches-descriptors :
  ∀ {design structural-proof candidate}
  → (witness : RegistersBuildWitness design structural-proof candidate)
  → Normalize.candidateRegisterCount candidate
    ≡ lengthList (descriptors witness)
candidate-register-count-matches-descriptors witness =
  cong Normalize.candidateRegisterCount (candidateBuilt witness)

candidate-has-two-locals-per-register :
  ∀ {design structural-proof candidate}
  → (witness : RegistersBuildWitness design structural-proof candidate)
  → Normalize.candidateLocalCount candidate
    ≡ twice (lengthList (descriptors witness))
candidate-has-two-locals-per-register witness =
  cong Normalize.candidateLocalCount (candidateBuilt witness)
  ∙ buildNext-local-count (resolvedRegisters witness)

canonicalDescriptorList-length : ∀ {items descriptors}
  → CanonicalDescriptorList items descriptors
  → lengthList items ≡ lengthList descriptors
canonicalDescriptorList-length canonicalDescriptorsNil = refl
canonicalDescriptorList-length
  (canonicalDescriptorsCons descriptor rest) =
  cong suc (canonicalDescriptorList-length rest)

candidate-register-count-matches-source :
  ∀ {design structural-proof candidate}
  → (witness : RegistersBuildWitness design structural-proof candidate)
  → Normalize.candidateRegisterCount candidate
    ≡ lengthList (Raw.rawInstances design)
candidate-register-count-matches-source witness =
  candidate-register-count-matches-descriptors witness
  ∙ sym (canonicalDescriptorList-length (descriptorCanonicity witness))