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

module Spartan6.Validation.DefaultStateParameter where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.RAM64X1S as RAM64X1S
import Spartan6.Primitive.SRL16E as SRL16E
open import Spartan6.Validation.CheckResult
  using (rejected≢accepted; accepted-injective)
import Spartan6.Validation.Diagnostic as Diagnostic

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

-- Source-conservative raw parameter decoding for exactly two documented
-- all-zero defaults.  Omission is sufficient to choose these defaults without
-- deciding how an arbitrary hexadecimal INIT maps to shift stages or RAM
-- addresses.  Consequently even an explicitly all-zero INIT string is
-- rejected here: accepting it would establish a raw string-to-state
-- convention that the existing primitive modules deliberately do not claim.

singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton item = item ∷ᴸ []ᴸ

issue : Diagnostic.DiagnosticCode
      → String → String → String → String
      → Diagnostic.Diagnostic
issue code subject expected observed detail =
  Diagnostic.diagnostic
    code Diagnostic.reject subject expected observed detail

explicitStateParameterDiagnostics : String → String
                                  → Diagnostic.Diagnostics
explicitStateParameterDiagnostics subject observed =
  singleton
    (issue Diagnostic.unsupportedMode subject
      "an empty raw parameter list selecting only the documented all-zero default"
      observed
      "Nonempty INIT and unknown parameters are rejected because nondefault raw hexadecimal-to-state ordering is not justified.")

scalarStateBitDiagnostics : String → Diagnostic.Diagnostics
scalarStateBitDiagnostics subject =
  singleton
    (issue Diagnostic.malformedInitialisation subject
      "no scalar rawInstanceInitialBit for vector state"
      "a scalar rawInstanceInitialBit"
      "SRL16E and RAM64X1S state is vector-valued; this isolated default decoder accepts only omitted initialization data.")

requireNoStateParameters : String → List Raw.RawParameter
                         → Diagnostic.CheckResult Unit
requireNoStateParameters subject []ᴸ = Diagnostic.accepted tt
requireNoStateParameters subject
  (Raw.rawParameter name value ∷ᴸ parameters) =
  Diagnostic.rejected (explicitStateParameterDiagnostics subject name)

requireNoScalarStateBit : String → Maybe Bit
                        → Diagnostic.CheckResult Unit
requireNoScalarStateBit subject nothing = Diagnostic.accepted tt
requireNoScalarStateBit subject (just bit) =
  Diagnostic.rejected (scalarStateBitDiagnostics subject)

validateCanonicalDefault : String → List Raw.RawParameter → Maybe Bit
                         → Diagnostic.CheckResult Unit
validateCanonicalDefault subject parameters initial-bit =
  Diagnostic.mapResult fst
    (Diagnostic.appendResult
      (requireNoStateParameters subject parameters)
      (requireNoScalarStateBit subject initial-bit))

-- Only these two primitive indices have constructors.  Each result retains
-- the typed state and a proof that it is exactly the existing source-backed
-- primitive default, not merely an extensionally all-low replacement.

data DecodedDefaultState : Architecture.PrimitiveKind → Type₀ where
  decodedSRL16EDefault :
    (state : SRL16E.SRL16EState)
    → state ≡ SRL16E.defaultInitialState
    → DecodedDefaultState Architecture.SRL16E

  decodedRAM64X1SDefault :
    (state : RAM64X1S.RAM64X1SState)
    → state ≡ RAM64X1S.defaultInitialState
    → DecodedDefaultState Architecture.RAM64X1S

srl16eDefaultResult : DecodedDefaultState Architecture.SRL16E
srl16eDefaultResult =
  decodedSRL16EDefault SRL16E.defaultInitialState refl

ram64x1sDefaultResult : DecodedDefaultState Architecture.RAM64X1S
ram64x1sDefaultResult =
  decodedRAM64X1SDefault RAM64X1S.defaultInitialState refl

decodedSRL16EState : DecodedDefaultState Architecture.SRL16E
                   → SRL16E.SRL16EState
decodedSRL16EState (decodedSRL16EDefault state state-is-default) = state

decodedSRL16EState-is-default :
  (decoded : DecodedDefaultState Architecture.SRL16E)
  → decodedSRL16EState decoded ≡ SRL16E.defaultInitialState
decodedSRL16EState-is-default
  (decodedSRL16EDefault state state-is-default) = state-is-default

decodedRAM64X1SState : DecodedDefaultState Architecture.RAM64X1S
                    → RAM64X1S.RAM64X1SState
decodedRAM64X1SState
  (decodedRAM64X1SDefault state state-is-default) = state

decodedRAM64X1SState-is-default :
  (decoded : DecodedDefaultState Architecture.RAM64X1S)
  → decodedRAM64X1SState decoded ≡ RAM64X1S.defaultInitialState
decodedRAM64X1SState-is-default
  (decodedRAM64X1SDefault state state-is-default) = state-is-default

-- This indexed selector prevents accidental use for another primitive kind.

data DefaultStateMode : Architecture.PrimitiveKind → Type₀ where
  srl16eDefaultMode   : DefaultStateMode Architecture.SRL16E
  ram64x1sDefaultMode : DefaultStateMode Architecture.RAM64X1S

documentedDefaultResult : ∀ {kind}
  → DefaultStateMode kind → DecodedDefaultState kind
documentedDefaultResult srl16eDefaultMode = srl16eDefaultResult
documentedDefaultResult ram64x1sDefaultMode = ram64x1sDefaultResult

normaliseDefaultStateParameters : ∀ {kind}
  → DefaultStateMode kind
  → String → List Raw.RawParameter → Maybe Bit
  → Diagnostic.CheckResult (DecodedDefaultState kind)
normaliseDefaultStateParameters mode subject parameters initial-bit =
  Diagnostic.mapResult
    (λ ignored → documentedDefaultResult mode)
    (validateCanonicalDefault subject parameters initial-bit)

normaliseSRL16EDefaultParameters :
  String → List Raw.RawParameter → Maybe Bit
  → Diagnostic.CheckResult
      (DecodedDefaultState Architecture.SRL16E)
normaliseSRL16EDefaultParameters =
  normaliseDefaultStateParameters srl16eDefaultMode

normaliseRAM64X1SDefaultParameters :
  String → List Raw.RawParameter → Maybe Bit
  → Diagnostic.CheckResult
      (DecodedDefaultState Architecture.RAM64X1S)
normaliseRAM64X1SDefaultParameters =
  normaliseDefaultStateParameters ram64x1sDefaultMode

-- Exact raw canonical form and checker correspondence.

data CanonicalDefaultRaw
  : List Raw.RawParameter → Maybe Bit → Type₀ where
  canonicalDefaultRaw : CanonicalDefaultRaw []ᴸ nothing

validateCanonicalDefault-sound : ∀ subject parameters initial-bit
  → validateCanonicalDefault subject parameters initial-bit
    ≡ Diagnostic.accepted tt
  → CanonicalDefaultRaw parameters initial-bit
validateCanonicalDefault-sound subject []ᴸ nothing result =
  canonicalDefaultRaw
validateCanonicalDefault-sound subject []ᴸ (just bit) result =
  Empty.rec (rejected≢accepted result)
validateCanonicalDefault-sound
  subject (parameter ∷ᴸ parameters) nothing result =
  Empty.rec (rejected≢accepted result)
validateCanonicalDefault-sound
  subject (parameter ∷ᴸ parameters) (just bit) result =
  Empty.rec (rejected≢accepted result)

validateCanonicalDefault-complete : ∀ subject {parameters initial-bit}
  → CanonicalDefaultRaw parameters initial-bit
  → validateCanonicalDefault subject parameters initial-bit
    ≡ Diagnostic.accepted tt
validateCanonicalDefault-complete subject canonicalDefaultRaw = refl

-- Indexed decoder soundness, exact-result preservation, and completeness.

normaliseDefaultStateParameters-sound : ∀ {kind}
  (mode : DefaultStateMode kind) subject parameters initial-bit result
  → normaliseDefaultStateParameters
      mode subject parameters initial-bit
    ≡ Diagnostic.accepted result
  → CanonicalDefaultRaw parameters initial-bit
normaliseDefaultStateParameters-sound
  mode subject parameters initial-bit result accepted-path with
  validateCanonicalDefault subject parameters initial-bit
  | inspect (validateCanonicalDefault subject parameters) initial-bit
... | Diagnostic.rejected diagnostics | [ validation-path ]ᵢ =
  Empty.rec (rejected≢accepted accepted-path)
... | Diagnostic.accepted tt | [ validation-path ]ᵢ =
  validateCanonicalDefault-sound
    subject parameters initial-bit validation-path

normaliseDefaultStateParameters-result-exact : ∀ {kind}
  (mode : DefaultStateMode kind) subject parameters initial-bit result
  → normaliseDefaultStateParameters
      mode subject parameters initial-bit
    ≡ Diagnostic.accepted result
  → result ≡ documentedDefaultResult mode
normaliseDefaultStateParameters-result-exact
  mode subject parameters initial-bit result accepted-path with
  validateCanonicalDefault subject parameters initial-bit
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted accepted-path)
... | Diagnostic.accepted tt =
  sym (accepted-injective accepted-path)

normaliseDefaultStateParameters-complete : ∀ {kind}
  (mode : DefaultStateMode kind) subject {parameters initial-bit}
  → CanonicalDefaultRaw parameters initial-bit
  → normaliseDefaultStateParameters
      mode subject parameters initial-bit
    ≡ Diagnostic.accepted (documentedDefaultResult mode)
normaliseDefaultStateParameters-complete
  mode subject canonicalDefaultRaw = refl

srl16e-default-sound : ∀ subject parameters initial-bit result
  → normaliseSRL16EDefaultParameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted result
  → CanonicalDefaultRaw parameters initial-bit
srl16e-default-sound =
  normaliseDefaultStateParameters-sound srl16eDefaultMode

srl16e-default-complete : ∀ subject {parameters initial-bit}
  → CanonicalDefaultRaw parameters initial-bit
  → normaliseSRL16EDefaultParameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted srl16eDefaultResult
srl16e-default-complete =
  normaliseDefaultStateParameters-complete srl16eDefaultMode

ram64x1s-default-sound : ∀ subject parameters initial-bit result
  → normaliseRAM64X1SDefaultParameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted result
  → CanonicalDefaultRaw parameters initial-bit
ram64x1s-default-sound =
  normaliseDefaultStateParameters-sound ram64x1sDefaultMode

ram64x1s-default-complete : ∀ subject {parameters initial-bit}
  → CanonicalDefaultRaw parameters initial-bit
  → normaliseRAM64X1SDefaultParameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted ram64x1sDefaultResult
ram64x1s-default-complete =
  normaliseDefaultStateParameters-complete ram64x1sDefaultMode

-- Positive reductions expose the existing typed defaults.

srl16e-omitted-INIT-selects-default :
  normaliseSRL16EDefaultParameters "u_srl" []ᴸ nothing
  ≡ Diagnostic.accepted srl16eDefaultResult
srl16e-omitted-INIT-selects-default = refl

srl16e-decoded-state-is-existing-default :
  decodedSRL16EState srl16eDefaultResult
  ≡ SRL16E.defaultInitialState
srl16e-decoded-state-is-existing-default = refl

ram64x1s-omitted-INIT-selects-default :
  normaliseRAM64X1SDefaultParameters "u_ram" []ᴸ nothing
  ≡ Diagnostic.accepted ram64x1sDefaultResult
ram64x1s-omitted-INIT-selects-default = refl

ram64x1s-decoded-state-is-existing-default :
  decodedRAM64X1SState ram64x1sDefaultResult
  ≡ RAM64X1S.defaultInitialState
ram64x1s-decoded-state-is-existing-default = refl

-- Rejection reductions: explicit zero text remains raw text and is not
-- equated with either typed default; unknown names and scalar bits also fail.

srl16e-explicit-zero-INIT-is-rejected :
  normaliseSRL16EDefaultParameters
    "u_srl" (Raw.rawParameter "INIT" "0000" ∷ᴸ []ᴸ) nothing
  ≡ Diagnostic.rejected
      (explicitStateParameterDiagnostics "u_srl" "INIT")
srl16e-explicit-zero-INIT-is-rejected = refl

ram64x1s-explicit-zero-INIT-is-rejected :
  normaliseRAM64X1SDefaultParameters
    "u_ram"
    (Raw.rawParameter "INIT" "0000000000000000" ∷ᴸ []ᴸ)
    nothing
  ≡ Diagnostic.rejected
      (explicitStateParameterDiagnostics "u_ram" "INIT")
ram64x1s-explicit-zero-INIT-is-rejected = refl

unknown-state-parameter-is-rejected :
  normaliseRAM64X1SDefaultParameters
    "u_ram" (Raw.rawParameter "UNKNOWN" "1" ∷ᴸ []ᴸ) nothing
  ≡ Diagnostic.rejected
      (explicitStateParameterDiagnostics "u_ram" "UNKNOWN")
unknown-state-parameter-is-rejected = refl

scalar-initial-bit-is-rejected :
  normaliseSRL16EDefaultParameters "u_srl" []ᴸ (just low)
  ≡ Diagnostic.rejected (scalarStateBitDiagnostics "u_srl")
scalar-initial-bit-is-rejected = refl

parameter-and-scalar-bit-report-both-boundaries :
  normaliseRAM64X1SDefaultParameters
    "u_ram" (Raw.rawParameter "INIT" "0" ∷ᴸ []ᴸ) (just high)
  ≡ Diagnostic.rejected
      (explicitStateParameterDiagnostics "u_ram" "INIT"
       ++ᴸ scalarStateBitDiagnostics "u_ram")
parameter-and-scalar-bit-report-both-boundaries = refl