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

module Spartan6.Netlist.AdmissionMixed where

open import Spartan6.Prelude

import Spartan6.Architecture.Profile as Profile
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeMixed as Normalize
import Spartan6.Netlist.NormalizeMixedSoundness as Soundness
import Spartan6.Netlist.Raw as Raw
import Spartan6.Semantics.Design as Semantics
import Spartan6.Semantics.Execution as Execution
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

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

-- A successful mixed translation is narrower than ArchitectureProfile:
-- acceptance depends on exact primitive modes and parameters, retained source
-- occurrence provenance through certified combinational scheduling, one
-- common top-level input clock, and resolvable connectivity.  Marking whole
-- primitive kinds fullySupported
-- would lose those restrictions and would incorrectly open developmentProfile.
--
-- Soundness.MixedBuildWitness records the actual accepting path.  In
-- particular, partitionCanonicity retains canonical FDRE/FDSE modes,
-- combinationalBuildTrace retains every accepted combinational mode, and
-- candidateBuilt relates the produced checked netlist to this exact raw
-- source.  None of these fields is a device, package, timing, placement,
-- synthesis-correctness, or silicon-conformance claim.

-- This scope has deliberately only a candidate-level constructor.  Device or
-- silicon conformance requires a separate future result carrying a selected
-- DeviceProfile, applicable errata, and external correspondence evidence.

data AdmissionScope : Type₀ where
  restrictedTranslationCandidate : AdmissionScope

-- RestrictedMixedProfile is an indexed profile predicate rather than a new
-- ArchitectureProfile.  Its evidence is exact-mode and exact-design evidence;
-- it cannot be mistaken for kind-wide developmentProfile admission.

record RestrictedMixedProfile (design : Raw.RawDesign) : Type₀ where
  constructor restrictedMixedProfile
  field
    admittedStructuralProof : Validation.StructurallyValid design
    admittedCandidate       : Normalize.CheckedMixedCandidate
    translationAccepted     :
      Normalize.normaliseMixed (design , admittedStructuralProof)
      ≡ Diagnostic.accepted admittedCandidate
    translationWitness      :
      Soundness.MixedBuildWitness
        design admittedStructuralProof admittedCandidate
    admissionScope          : AdmissionScope

open RestrictedMixedProfile public

RestrictedMixedAdmission : Type₀
RestrictedMixedAdmission = Σ Raw.RawDesign RestrictedMixedProfile

-- This is the only constructor path exposed by the wrapper: rejected
-- translation remains rejected with its original diagnostics; successful
-- translation returns the raw source together with all retained evidence.

admitRestrictedMixed : Validation.StructurallyChecked
                     → Diagnostic.CheckResult RestrictedMixedAdmission
admitRestrictedMixed checked with Normalize.normaliseMixed checked
                                | inspect Normalize.normaliseMixed checked
... | Diagnostic.rejected diagnostics | [ result-path ]ᵢ =
  Diagnostic.rejected diagnostics
... | Diagnostic.accepted candidate | [ result-path ]ᵢ =
  Diagnostic.accepted
    (fst checked
    , restrictedMixedProfile
        (snd checked)
        candidate
        result-path
        (Soundness.normaliseMixed-witness checked candidate result-path)
        restrictedTranslationCandidate)

-- The explicit candidate profile does not alter the coarse architecture
-- profile or turn partial primitive support into full raw admission.

development-profile-remains-closed : ∀ kind
  → Profile.profileAdmits? Profile.developmentProfile kind ≡ false
development-profile-remains-closed =
  Profile.development-profile-is-closed

admitted-candidate-preserves-source :
  ∀ {design} (membership : RestrictedMixedProfile design)
  → Normalize.candidateSource (admittedCandidate membership) ≡ design
admitted-candidate-preserves-source membership =
  Soundness.candidate-source-preserved (translationWitness membership)

admitted-candidate-scope :
  ∀ {design} (membership : RestrictedMixedProfile design)
  → admissionScope membership ≡ restrictedTranslationCandidate
admitted-candidate-scope membership with admissionScope membership
... | restrictedTranslationCandidate = refl

-- Successful restricted admission exposes an ordinary executable Design.
-- Its indices are retained from the checked candidate, so clients cannot
-- accidentally supply an input, observation, or state vector of the wrong
-- width.

admittedSemantics :
  ∀ {design}
  → (membership : RestrictedMixedProfile design)
  → Semantics.Design
      (Normalize.candidateInputCount
        (admittedCandidate membership))
      (Normalize.candidateOutputCount
        (admittedCandidate membership))
      (Normalize.candidateRegisterCount
        (admittedCandidate membership))
admittedSemantics membership =
  Checked.compileNetlist
    (Normalize.candidateNetlist (admittedCandidate membership))

admitted-observation-deterministic :
  ∀ {design}
  → (membership : RestrictedMixedProfile design)
  → {external : Semantics.Inputs (admittedSemantics membership)}
  → {state : Semantics.State (admittedSemantics membership)}
  → {left right :
      Semantics.Observation (admittedSemantics membership)}
  → Semantics.ObservationOf
      (admittedSemantics membership) external state left
  → Semantics.ObservationOf
      (admittedSemantics membership) external state right
  → left ≡ right
admitted-observation-deterministic
  membership {external} {state} {left} {right} left-path right-path =
  Semantics.observation-deterministic
    {design = admittedSemantics membership}
    {external = external}
    {state = state}
    {left = left}
    {right = right}
    left-path right-path

admitted-transition-deterministic :
  ∀ {design}
  → (membership : RestrictedMixedProfile design)
  → {event : Semantics.Event}
  → {external : Semantics.Inputs (admittedSemantics membership)}
  → {before : Semantics.State (admittedSemantics membership)}
  → {left right : Semantics.State (admittedSemantics membership)}
  → Semantics.Transition
      (admittedSemantics membership) event external before left
  → Semantics.Transition
      (admittedSemantics membership) event external before right
  → left ≡ right
admitted-transition-deterministic
  membership {event} {external} {before} {left} {right}
  left-path right-path =
  Semantics.transition-deterministic
    {design = admittedSemantics membership}
    {event = event}
    {external = external}
    {before = before}
    {left = left}
    {right = right}
    left-path right-path

admitted-execution-complete :
  ∀ {design}
  → (membership : RestrictedMixedProfile design)
  → {state final : Semantics.State (admittedSemantics membership)}
  → {samples :
      List
        (Semantics.Stimulus
          (Normalize.candidateInputCount
            (admittedCandidate membership)))}
  → Execution.Executes
      (admittedSemantics membership) state samples final
  → Semantics.run (admittedSemantics membership) state samples ≡ final
admitted-execution-complete
  membership {state} {final} {samples} execution =
  Execution.execution-complete
    {design = admittedSemantics membership}
    {state = state}
    {final = final}
    {samples = samples}
    execution

admitted-execution-final-unique :
  ∀ {design}
  → (membership : RestrictedMixedProfile design)
  → {state left right :
      Semantics.State (admittedSemantics membership)}
  → {samples :
      List
        (Semantics.Stimulus
          (Normalize.candidateInputCount
            (admittedCandidate membership)))}
  → Execution.Executes
      (admittedSemantics membership) state samples left
  → Execution.Executes
      (admittedSemantics membership) state samples right
  → left ≡ right
admitted-execution-final-unique
  membership {state} {left} {right} {samples}
  left-execution right-execution =
  Execution.execution-final-unique
    {design = admittedSemantics membership}
    {state = state}
    {left = left}
    {right = right}
    {samples = samples}
    left-execution right-execution