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

module Spartan6.Netlist.ExactAdmission where

open import Spartan6.Prelude

import Spartan6.Import.Artifact as Artifact
import Spartan6.Netlist.AdmissionCore as Legacy
import Spartan6.Netlist.DecodedOperation as Operation
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.ReadySchedule as Schedule
import Spartan6.Validation.Design as Validation

-- One exact-admission schema replaces public pure/mixed route alternatives.
-- The legacy witness is retained only as compatibility evidence until all
-- certified handlers lower directly through the new operation plan.

record ExactAdmission (artifact : Artifact.RawArtifact) : Type₀ where
  constructor exactAdmission
  field
    validatedSource : Validation.ValidatedDesign artifact
    operationPlan : Operation.OperationPlan
    operationPlan-is-source :
      operationPlan ≡ Operation.planValidated validatedSource
    checkedSchedule :
      Schedule.Scheduled
        (Operation.initiallyAvailableNets operationPlan)
        (Operation.combinationalOperations operationPlan)
    legacyCompatibility : Legacy.RestrictedCoreAdmission
    legacySource-is-exact :
      Legacy.admittedRawSource legacyCompatibility
      ≡ Artifact.decodedDesign artifact
    executable : Legacy.ExecutableCore
    executable-is-compatibility :
      executable ≡ Legacy.admittedExecutable legacyCompatibility

open ExactAdmission public

exact-source-digest : ∀ {artifact : Artifact.RawArtifact}
  → ExactAdmission artifact
  → Artifact.artifactDigest (Artifact.envelope artifact)
    ≡ Artifact.artifactDigest (Artifact.envelope artifact)
exact-source-digest admission = refl