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

module Spartan6.Netlist.NormalizeMixedSoundness where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.BuildOBUFDS as OBUFDS
import Spartan6.Netlist.Carry4Builder as Carry4
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.GenericBuilder as Generic
import Spartan6.Netlist.NormalizeCombinationalSoundness as CombinationalSoundness
import Spartan6.Netlist.NormalizeMixed as Normalize
import Spartan6.Netlist.NormalizeRegisters as Registers
import Spartan6.Netlist.NormalizeRegistersSoundness as RegistersSoundness
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.Schedule as Schedule
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.Parameter as Parameter
import Spartan6.Validation.Raw as Validation

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

-- The partition relation preserves source order in both retained sublists.
-- A register branch additionally carries the canonical descriptor proof from
-- NormalizeRegistersSoundness; its nested CanonicalRegisterMode rules out any
-- kind other than FDRE/FDSE.

data CanonicalMixedPartition
  : List Raw.RawInstance → Normalize.InstancePartition → Type₀ where
  canonicalMixedPartitionNil :
    CanonicalMixedPartition
      []ᴸ (Normalize.instancePartition []ᴸ []ᴸ)

  canonicalMixedPartitionRegister :
    ∀ {item items descriptor rest}
    → RegistersSoundness.CanonicalDescriptor item descriptor
    → CanonicalMixedPartition items rest
    → CanonicalMixedPartition
        (item ∷ᴸ items)
        (Normalize.instancePartition
          (descriptor ∷ᴸ Normalize.partitionRegisters rest)
          (Normalize.partitionCombinational rest))

  canonicalMixedPartitionCombinational :
    ∀ {item items rest}
    → CanonicalMixedPartition items rest
    → CanonicalMixedPartition
        (item ∷ᴸ items)
        (Normalize.instancePartition
          (Normalize.partitionRegisters rest)
          (item ∷ᴸ Normalize.partitionCombinational rest))

mutual
  partitionInstances-sound : ∀ items partition
    → Normalize.partitionInstances items
      ≡ Diagnostic.accepted partition
    → CanonicalMixedPartition items partition
  partitionInstances-sound []ᴸ partition result
    with accepted-injective result
  ... | empty-is-partition =
    subst
      (CanonicalMixedPartition []ᴸ)
      empty-is-partition
      canonicalMixedPartitionNil
  partitionInstances-sound (item ∷ᴸ items) partition result
    with Raw.rawInstanceKind item
  ... | Raw.knownPrimitive Architecture.FDRE =
    partitionRegisterItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.FDSE =
    partitionRegisterItem-sound item items partition result
  ... | Raw.unknownPrimitive unknown =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.LUT1 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.LUT2 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.LUT3 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.LUT4 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.LUT5 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.LUT6 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.MUXF7 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.MUXF8 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.CARRY4 =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.SRL16E =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.RAM64X1S =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.IBUF =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.OBUF =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.OBUFDS =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.OBUFT =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.BUFG =
    partitionCombinationalItem-sound item items partition result
  ... | Raw.knownPrimitive Architecture.BUFGCE =
    partitionCombinationalItem-sound item items partition result

  partitionRegisterItem-sound : ∀ item items partition
    → Normalize.partitionRegisterItem item items
      ≡ Diagnostic.accepted partition
    → CanonicalMixedPartition (item ∷ᴸ items) partition
  partitionRegisterItem-sound item items partition result
    with Registers.normaliseDescriptor item
       | inspect Registers.normaliseDescriptor item
  ... | Diagnostic.rejected diagnostics | [ descriptor-path ]ᵢ =
    Empty.rec (rejected≢accepted result)
  ... | Diagnostic.accepted descriptor | [ descriptor-path ]ᵢ
    with Normalize.partitionInstances items
       | inspect Normalize.partitionInstances items
  ...   | Diagnostic.rejected diagnostics | [ rest-path ]ᵢ =
    Empty.rec (rejected≢accepted result)
  ...   | Diagnostic.accepted rest | [ rest-path ]ᵢ
    with accepted-injective result
  ...     | built-is-partition =
    subst
      (CanonicalMixedPartition (item ∷ᴸ items))
      built-is-partition
      (canonicalMixedPartitionRegister
        (RegistersSoundness.normaliseDescriptor-sound
          item descriptor descriptor-path)
        (partitionInstances-sound items rest rest-path))

  partitionCombinationalItem-sound : ∀ item items partition
    → Normalize.prependCombinational item
        (Normalize.partitionInstances items)
      ≡ Diagnostic.accepted partition
    → CanonicalMixedPartition (item ∷ᴸ items) partition
  partitionCombinationalItem-sound item items partition result
    with Normalize.partitionInstances items
       | inspect Normalize.partitionInstances items
  ... | Diagnostic.rejected diagnostics | [ rest-path ]ᵢ =
    Empty.rec (rejected≢accepted result)
  ... | Diagnostic.accepted rest | [ rest-path ]ᵢ
    with accepted-injective result
  ...   | built-is-partition =
    subst
      (CanonicalMixedPartition (item ∷ᴸ items))
      built-is-partition
      (canonicalMixedPartitionCombinational
        (partitionInstances-sound items rest rest-path))

-- Ordinary generic modes reuse the established parameter boundary.  CARRY4
-- and OBUFDS retain their specialized evidence because their admitted modes
-- include structural and provenance conditions beyond CoreParameters.

data GenericAcceptedInstanceMode {inputCount registerCount : ℕ}
  (item : Raw.RawInstance)
  (current : Generic.Builder inputCount registerCount)
  : Type₀ where
  genericAcceptedStandard :
    CombinationalSoundness.AcceptedInstanceMode item
    → GenericAcceptedInstanceMode item current

  genericAcceptedCARRY4 :
    (built : Carry4.Carry4Build item current)
    → Carry4.processCARRY4 item current
      ≡ Diagnostic.accepted built
    → GenericAcceptedInstanceMode item current

  genericAcceptedOBUFDS :
    OBUFDS.AcceptedOBUFDSMode item
    → GenericAcceptedInstanceMode item current

genericProcessInstance-mode-sound :
  ∀ item {inputCount registerCount}
    (current next : Generic.Builder inputCount registerCount)
  → Generic.processInstance item current ≡ Diagnostic.accepted next
  → GenericAcceptedInstanceMode item current
genericProcessInstance-mode-sound
  (Raw.rawInstance name (Raw.unknownPrimitive unknown)
    ports raw-parameters initial-bit)
  current next result =
  Empty.rec (rejected≢accepted result)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedLUT1 parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedLUT2 parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedLUT3 parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedLUT4 parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedLUT5 parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedLUT6 parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedMUXF7 parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedMUXF8 parameter-path)
genericProcessInstance-mode-sound
  item@(Raw.rawInstance name (Raw.knownPrimitive Architecture.CARRY4)
    ports raw-parameters initial-bit)
  current next result
  with Carry4.processCARRY4 item current
     | inspect (Carry4.processCARRY4 item) current
... | Diagnostic.rejected diagnostics | [ carry-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted built | [ carry-path ]ᵢ =
  genericAcceptedCARRY4 built carry-path
genericProcessInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.FDRE)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
genericProcessInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.FDSE)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
genericProcessInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.SRL16E)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
genericProcessInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.RAM64X1S)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedIBUF parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedOBUF parameter-path)
genericProcessInstance-mode-sound
  item@(Raw.rawInstance name (Raw.knownPrimitive Architecture.OBUFDS)
    ports raw-parameters initial-bit)
  current next result =
  genericAcceptedOBUFDS
    (OBUFDS.processOBUFDS-mode-sound item current next result)
genericProcessInstance-mode-sound
  (Raw.rawInstance name (Raw.knownPrimitive Architecture.OBUFT)
    ports raw-parameters initial-bit)
  current next result = Empty.rec (rejected≢accepted result)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedBUFG parameter-path)
genericProcessInstance-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 ]ᵢ =
  genericAcceptedStandard
    (CombinationalSoundness.acceptedBUFGCE parameter-path)

data GenericProcessingTrace {inputCount registerCount : ℕ}
  : List Raw.RawInstance
  → Generic.Builder inputCount registerCount
  → Generic.Builder inputCount registerCount
  → Type₀ where
  genericProcessingDone : ∀ {current}
    → GenericProcessingTrace []ᴸ current current

  genericProcessingStep : ∀ {item items current next final}
    → Generic.processInstance item current
      ≡ Diagnostic.accepted next
    → GenericAcceptedInstanceMode item current
    → GenericProcessingTrace items next final
    → GenericProcessingTrace (item ∷ᴸ items) current final

genericProcessInstances-sound :
  ∀ {inputCount registerCount} items
    (current final : Generic.Builder inputCount registerCount)
  → Generic.processInstances items current
    ≡ Diagnostic.accepted final
  → GenericProcessingTrace items current final
genericProcessInstances-sound []ᴸ current final result
  with accepted-injective result
... | current-is-final =
  subst
    (GenericProcessingTrace []ᴸ current)
    current-is-final
    genericProcessingDone
genericProcessInstances-sound (item ∷ᴸ items) current final result
  with Generic.processInstance item current
     | inspect (Generic.processInstance item) current
... | Diagnostic.rejected diagnostics | [ step-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted next | [ step-path ]ᵢ =
  genericProcessingStep
    step-path
    (genericProcessInstance-mode-sound item current next step-path)
    (genericProcessInstances-sound items next final result)

-- The register builder recurses over the descriptor tail and then finishes
-- the head.  This trace records that exact order and every successful
-- finishRegisterNodes boundary.

data RegisterBuildTrace {inputCount registerCount : ℕ}
  : (descriptors : List Registers.RegisterDescriptor)
  → Generic.Builder inputCount registerCount
  → Normalize.BuiltRegisters
      inputCount registerCount (lengthList descriptors)
  → Type₀ where
  registerBuildDone : ∀ {current}
    → RegisterBuildTrace
        []ᴸ current (Normalize.builtRegisters current [])

  registerBuildStep :
    ∀ {descriptor descriptors current rest built}
    → RegisterBuildTrace descriptors current rest
    → Normalize.finishRegisterNodes descriptor rest
      ≡ Diagnostic.accepted built
    → RegisterBuildTrace
        (descriptor ∷ᴸ descriptors) current built

buildRegisterNodes-sound :
  ∀ {inputCount registerCount} descriptors
    (current : Generic.Builder inputCount registerCount)
    (built : Normalize.BuiltRegisters
      inputCount registerCount (lengthList descriptors))
  → Normalize.buildRegisterNodes descriptors current
    ≡ Diagnostic.accepted built
  → RegisterBuildTrace descriptors current built
buildRegisterNodes-sound []ᴸ current built result
  with accepted-injective result
... | empty-is-built =
  subst
    (RegisterBuildTrace []ᴸ current)
    empty-is-built
    registerBuildDone
buildRegisterNodes-sound
  (descriptor ∷ᴸ descriptors) current built result
  with Normalize.buildRegisterNodes descriptors current
     | inspect (Normalize.buildRegisterNodes descriptors) current
... | Diagnostic.rejected diagnostics | [ rest-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted rest | [ rest-path ]ᵢ =
  registerBuildStep
    (buildRegisterNodes-sound descriptors current rest rest-path)
    result

commonClock-nonempty : ∀ input-nets registers clock-index
  → Registers.commonClock input-nets registers
    ≡ Diagnostic.accepted clock-index
  → RegistersSoundness.NonemptyList registers
commonClock-nonempty input-nets []ᴸ clock-index result =
  Empty.rec (rejected≢accepted result)
commonClock-nonempty
  input-nets (descriptor ∷ᴸ descriptors) clock-index result =
  RegistersSoundness.listIsNonempty

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

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

    partition : Normalize.InstancePartition
    instancesPartitioned :
      Normalize.partitionInstances (Raw.rawInstances design)
      ≡ Diagnostic.accepted partition
    partitionCanonicity :
      CanonicalMixedPartition (Raw.rawInstances design) partition

    partitionRegistersNonempty :
      RegistersSoundness.NonemptyList
        (Normalize.partitionRegisters partition)

    clockIndex : Fin (lengthList inputNets)
    commonClockAccepted :
      Registers.commonClock
        inputNets (Normalize.partitionRegisters partition)
      ≡ Diagnostic.accepted clockIndex

    scheduledCombinational :
      Schedule.Scheduled
        (Normalize.mixedInitialBuilder
          inputNets (Normalize.partitionRegisters partition))
        (Normalize.partitionCombinational partition)
    combinationalScheduled :
      Schedule.scheduleInstances
        (Normalize.mixedInitialBuilder
          inputNets (Normalize.partitionRegisters partition))
        (Normalize.partitionCombinational partition)
      ≡ Diagnostic.accepted scheduledCombinational
    schedulingProvenance :
      Schedule.ScheduleTrace
        (Normalize.mixedInitialBuilder
          inputNets (Normalize.partitionRegisters partition))
        (Normalize.partitionCombinational partition)
        (Schedule.scheduledInstances scheduledCombinational)
        (Schedule.finalBuilder scheduledCombinational)
    combinationalPermutation :
      Schedule.RemovalPermutation
        (Normalize.partitionCombinational partition)
        (Schedule.scheduledInstances scheduledCombinational)

    combinationalBuilder :
      Generic.Builder
        (lengthList inputNets)
        (lengthList (Normalize.partitionRegisters partition))
    combinationalBuilderIsScheduledFinal :
      combinationalBuilder
      ≡ Schedule.finalBuilder scheduledCombinational
    combinationalBuilt :
      Generic.processInstances
        (Schedule.scheduledInstances scheduledCombinational)
        (Normalize.mixedInitialBuilder
          inputNets (Normalize.partitionRegisters partition))
      ≡ Diagnostic.accepted combinationalBuilder
    combinationalBuildTrace :
      GenericProcessingTrace
        (Schedule.scheduledInstances scheduledCombinational)
        (Normalize.mixedInitialBuilder
          inputNets (Normalize.partitionRegisters partition))
        combinationalBuilder

    builtRegisters :
      Normalize.BuiltRegisters
        (lengthList inputNets)
        (lengthList (Normalize.partitionRegisters partition))
        (lengthList (Normalize.partitionRegisters partition))
    registersBuilt :
      Normalize.buildRegisterNodes
        (Normalize.partitionRegisters partition)
        combinationalBuilder
      ≡ Diagnostic.accepted builtRegisters
    registerBuildTrace :
      RegisterBuildTrace
        (Normalize.partitionRegisters partition)
        combinationalBuilder builtRegisters

    outputWires :
      List
        (Checked.Wire
          (lengthList inputNets)
          (lengthList (Normalize.partitionRegisters partition))
          (Generic.builderLocalCount
            (Normalize.builtBuilder builtRegisters)))
    outputsCollected :
      Normalize.collectOutputWires
        (Raw.rawTopPorts design)
        (Normalize.builtBuilder builtRegisters)
      ≡ Diagnostic.accepted outputWires

    candidateBuilt :
      candidate
      ≡ Normalize.finishCandidate
          design structural-proof inputNets
          (Normalize.partitionRegisters partition)
          clockIndex builtRegisters outputWires

open MixedBuildWitness public

normaliseMixed-witness : ∀ checked candidate
  → Normalize.normaliseMixed checked ≡ Diagnostic.accepted candidate
  → MixedBuildWitness (fst checked) (snd checked) candidate
normaliseMixed-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.partitionInstances (Raw.rawInstances design)
     | inspect Normalize.partitionInstances (Raw.rawInstances design)
...     | Diagnostic.rejected diagnostics | [ partition-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...     | Diagnostic.accepted partition | [ partition-path ]ᵢ
  with Registers.commonClock
         input-nets (Normalize.partitionRegisters partition)
     | inspect
        (Registers.commonClock input-nets)
        (Normalize.partitionRegisters partition)
...       | Diagnostic.rejected diagnostics | [ clock-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...       | Diagnostic.accepted clock-index | [ clock-path ]ᵢ
  with Schedule.scheduleInstances
         (Normalize.mixedInitialBuilder
           input-nets (Normalize.partitionRegisters partition))
         (Normalize.partitionCombinational partition)
     | inspect
        (Schedule.scheduleInstances
          (Normalize.mixedInitialBuilder
            input-nets (Normalize.partitionRegisters partition)))
        (Normalize.partitionCombinational partition)
...         | Diagnostic.rejected diagnostics
            | [ schedule-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...         | Diagnostic.accepted scheduled
            | [ schedule-path ]ᵢ
  with Normalize.buildRegisterNodes
         (Normalize.partitionRegisters partition)
         (Schedule.finalBuilder scheduled)
     | inspect
        (Normalize.buildRegisterNodes
          (Normalize.partitionRegisters partition))
        (Schedule.finalBuilder scheduled)
...           | Diagnostic.rejected diagnostics | [ registers-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...           | Diagnostic.accepted built | [ registers-path ]ᵢ
  with Normalize.collectOutputWires
         (Raw.rawTopPorts design) (Normalize.builtBuilder built)
     | inspect
        (Normalize.collectOutputWires (Raw.rawTopPorts design))
        (Normalize.builtBuilder built)
...             | Diagnostic.rejected diagnostics | [ outputs-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...             | Diagnostic.accepted outputs | [ outputs-path ]ᵢ
  with accepted-injective result
...               | finish-is-candidate =
  record
    { targetValidated = target-path
    ; inputNets = input-nets
    ; inputNetsCollected = inputs-path
    ; partition = partition
    ; instancesPartitioned = partition-path
    ; partitionCanonicity =
        partitionInstances-sound
          (Raw.rawInstances design) partition partition-path
    ; partitionRegistersNonempty =
        commonClock-nonempty
          input-nets (Normalize.partitionRegisters partition)
          clock-index clock-path
    ; clockIndex = clock-index
    ; commonClockAccepted = clock-path
    ; scheduledCombinational = scheduled
    ; combinationalScheduled = schedule-path
    ; schedulingProvenance = Schedule.schedulingTrace scheduled
    ; combinationalPermutation = Schedule.scheduled-permutation scheduled
    ; combinationalBuilder = Schedule.finalBuilder scheduled
    ; combinationalBuilderIsScheduledFinal = refl
    ; combinationalBuilt = Schedule.scheduled-replays scheduled
    ; combinationalBuildTrace =
        genericProcessInstances-sound
          (Schedule.scheduledInstances scheduled)
          (Normalize.mixedInitialBuilder
            input-nets (Normalize.partitionRegisters partition))
          (Schedule.finalBuilder scheduled)
          (Schedule.scheduled-replays scheduled)
    ; builtRegisters = built
    ; registersBuilt = registers-path
    ; registerBuildTrace =
        buildRegisterNodes-sound
          (Normalize.partitionRegisters partition)
          (Schedule.finalBuilder scheduled) built registers-path
    ; outputWires = outputs
    ; outputsCollected = outputs-path
    ; candidateBuilt = sym finish-is-candidate
    }

-- Candidate projections below are consequences of the exact finishCandidate
-- equality, so they preserve dependent fields rather than merely comparing
-- raw source names.

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

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

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

candidate-input-count-matches-inputs :
  ∀ {design structural-proof candidate}
  → (witness : MixedBuildWitness design structural-proof candidate)
  → Normalize.candidateInputCount candidate
    ≡ lengthList (inputNets witness)
candidate-input-count-matches-inputs witness =
  cong Normalize.candidateInputCount (candidateBuilt witness)

candidate-output-count-matches-outputs :
  ∀ {design structural-proof candidate}
  → (witness : MixedBuildWitness design structural-proof candidate)
  → Normalize.candidateOutputCount candidate
    ≡ lengthList (outputWires witness)
candidate-output-count-matches-outputs witness =
  cong Normalize.candidateOutputCount (candidateBuilt witness)

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

candidate-local-count-matches-register-build :
  ∀ {design structural-proof candidate}
  → (witness : MixedBuildWitness design structural-proof candidate)
  → Normalize.candidateLocalCount candidate
    ≡ Generic.builderLocalCount
        (Normalize.builtBuilder (builtRegisters witness))
candidate-local-count-matches-register-build witness =
  cong Normalize.candidateLocalCount (candidateBuilt witness)

InputClock : Type₀
InputClock = Σ ℕ Fin

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

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

InitialStateShape : Type₀
InitialStateShape = Σ ℕ (λ register-count → Vec Bit register-count)

candidateInitialState :
  Normalize.CheckedMixedCandidate → InitialStateShape
candidateInitialState candidate =
  Normalize.candidateRegisterCount candidate
  , Checked.checkedInitial (Normalize.candidateNetlist candidate)

candidate-initial-state-matches-partition :
  ∀ {design structural-proof candidate}
  → (witness : MixedBuildWitness design structural-proof candidate)
  → candidateInitialState candidate
    ≡
      ( lengthList
          (Normalize.partitionRegisters (partition witness))
      , Normalize.initialValues
          (Normalize.partitionRegisters (partition witness))
      )
candidate-initial-state-matches-partition witness =
  cong candidateInitialState (candidateBuilt witness)

NextStateShape : Type₀
NextStateShape =
  Σ ℕ (λ input-count →
    Σ ℕ (λ register-count →
      Σ ℕ (λ local-count →
        Vec
          (Checked.Wire input-count register-count local-count)
          register-count)))

candidateNextState :
  Normalize.CheckedMixedCandidate → NextStateShape
candidateNextState candidate =
  Normalize.candidateInputCount candidate
  , (Normalize.candidateRegisterCount candidate
    , (Normalize.candidateLocalCount candidate
      , Checked.checkedNext (Normalize.candidateNetlist candidate)))

candidate-next-state-matches-register-build :
  ∀ {design structural-proof candidate}
  → (witness : MixedBuildWitness design structural-proof candidate)
  → candidateNextState candidate
    ≡
      ( lengthList (inputNets witness)
      , ( lengthList
            (Normalize.partitionRegisters (partition witness))
        , ( Generic.builderLocalCount
              (Normalize.builtBuilder (builtRegisters witness))
          , Normalize.builtNext (builtRegisters witness)
          )
        )
      )
candidate-next-state-matches-register-build witness =
  cong candidateNextState (candidateBuilt witness)