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

module Spartan6.Netlist.NormalizeScheduledCombinationalSoundness where

open import Spartan6.Prelude

import Spartan6.Netlist.Candidate as Candidate
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.GenericBuilder as Generic
import Spartan6.Netlist.NormalizeMixedSoundness as MixedSoundness
import Spartan6.Netlist.NormalizeScheduledCombinational as Normalize
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.Raw as Validation

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

-- Acceptance retains both scheduler provenance and the replayed GenericBuilder
-- equations.  MixedSoundness.GenericProcessingTrace contributes canonical
-- ordinary modes plus full specialized CARRY4/OBUFDS evidence for every
-- scheduled occurrence.

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

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

    scheduled :
      Schedule.Scheduled
        (Normalize.initialBuilder inputNets)
        (Raw.rawInstances design)
    scheduleAccepted :
      Schedule.scheduleInstances
        (Normalize.initialBuilder inputNets)
        (Raw.rawInstances design)
      ≡ Diagnostic.accepted scheduled
    schedulingProvenance :
      Schedule.ScheduleTrace
        (Normalize.initialBuilder inputNets)
        (Raw.rawInstances design)
        (Schedule.scheduledInstances scheduled)
        (Schedule.finalBuilder scheduled)
    occurrencePermutation :
      Schedule.RemovalPermutation
        (Raw.rawInstances design)
        (Schedule.scheduledInstances scheduled)

    genericReplay :
      Generic.processInstances
        (Schedule.scheduledInstances scheduled)
        (Normalize.initialBuilder inputNets)
      ≡ Diagnostic.accepted (Schedule.finalBuilder scheduled)
    acceptedModeTrace :
      MixedSoundness.GenericProcessingTrace
        (Schedule.scheduledInstances scheduled)
        (Normalize.initialBuilder inputNets)
        (Schedule.finalBuilder scheduled)

    outputWires :
      List
        (Checked.Wire
          (lengthList inputNets) 
          (Generic.builderLocalCount
            (Schedule.finalBuilder scheduled)))
    outputsCollected :
      TopInterface.collectBuilderOutputWires
        (Raw.rawTopPorts design)
        (Schedule.finalBuilder scheduled)
      ≡ Diagnostic.accepted outputWires

    candidateBuilt :
      candidate
      ≡ Normalize.finishCandidate
          design structural-proof inputNets
          (Schedule.finalBuilder scheduled) outputWires

    candidateInitialIsEmpty :
      Checked.checkedInitial
        (Candidate.candidateNetlist candidate)
      ≡ []
    candidateNextIsEmpty :
      Checked.checkedNext
        (Candidate.candidateNetlist candidate)
      ≡ []

open ScheduledCombinationalBuildWitness public

normaliseScheduledCombinational-witness : ∀ checked candidate
  → Normalize.normaliseScheduledCombinational checked
    ≡ Diagnostic.accepted candidate
  → ScheduledCombinationalBuildWitness
      (fst checked) (snd checked) candidate
normaliseScheduledCombinational-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 Schedule.scheduleInstances
         (Normalize.initialBuilder input-nets)
         (Raw.rawInstances design)
     | inspect
        (Schedule.scheduleInstances
          (Normalize.initialBuilder input-nets))
        (Raw.rawInstances design)
...     | Diagnostic.rejected diagnostics | [ schedule-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
...     | Diagnostic.accepted scheduled | [ schedule-path ]ᵢ
  with TopInterface.collectBuilderOutputWires
         (Raw.rawTopPorts design)
         (Schedule.finalBuilder scheduled)
     | inspect
        (TopInterface.collectBuilderOutputWires (Raw.rawTopPorts design))
        (Schedule.finalBuilder scheduled)
...       | 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
    ; scheduled = scheduled
    ; scheduleAccepted = schedule-path
    ; schedulingProvenance = Schedule.schedulingTrace scheduled
    ; occurrencePermutation = Schedule.scheduled-permutation scheduled
    ; genericReplay = Schedule.scheduled-replays scheduled
    ; acceptedModeTrace =
        MixedSoundness.genericProcessInstances-sound
          (Schedule.scheduledInstances scheduled)
          (Normalize.initialBuilder input-nets)
          (Schedule.finalBuilder scheduled)
          (Schedule.scheduled-replays scheduled)
    ; outputWires = outputs
    ; outputsCollected = outputs-path
    ; candidateBuilt = sym finish-is-candidate
    ; candidateInitialIsEmpty =
        Candidate.candidate-has-no-registers candidate
    ; candidateNextIsEmpty =
        Candidate.candidate-next-is-empty candidate
    }

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

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

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

candidate-local-count-matches-schedule :
  ∀ {design structural-proof candidate}
  → (witness :
      ScheduledCombinationalBuildWitness
        design structural-proof candidate)
  → Candidate.candidateLocalCount candidate
    ≡ Generic.builderLocalCount
        (Schedule.finalBuilder (scheduled witness))
candidate-local-count-matches-schedule witness =
  cong Candidate.candidateLocalCount (candidateBuilt witness)