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

module Spartan6.Validation.ParameterSoundness where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Foundation.Hex as Hex
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.LUT as LUT
open import Spartan6.Validation.CheckResult public
  using (accepted?; rejected≢accepted; accepted-injective)
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter

open import Agda.Builtin.String using (primStringEquality)
open import Cubical.Data.Bool.Properties using (false≢true)
open import Cubical.Foundations.Path using (inspect; [_]ᵢ)
import Cubical.Data.Empty as Empty

just? : ∀ {ℓ} {A : Type ℓ} → Maybe A → Bool
just? nothing = false
just? (just value) = true

nothing≢just : ∀ {ℓ} {A : Type ℓ} {value : A}
  → nothing ≡ just value
  → Empty.⊥
nothing≢just path = false≢true (cong just? path)

just-injective : ∀ {ℓ} {A : Type ℓ} {left right : A}
  → just left ≡ just right
  → left ≡ right
just-injective {left = left} path =
  cong (fromMaybe left) path
  where
  fromMaybe : ∀ {ℓ} {A : Type ℓ} → A → Maybe A → A
  fromMaybe fallback nothing = fallback
  fromMaybe fallback (just value) = value

-- CanonicalLUT6 is the propositional meaning of successful raw LUT6
-- parameter normalization.  The explicit case records exactly the two tests
-- made by the executable decoder: the singleton name test and the fixed-size
-- hexadecimal decode.
--
-- Agda's builtin String module in this checkout provides executable equality
-- but no safe reflection theorem from
--
--   primStringEquality name "INIT" ≡ true
--
-- to a path name ≡ "INIT".  Retaining the Boolean equality witness is
-- therefore the strongest assumption-free statement about a non-literal raw
-- name.  Literal "INIT" specializes this witness to refl below.

data CanonicalLUT6
  : List Raw.RawParameter → Maybe Bit → LUT.LUT6Table → Type₀ where
  canonicalLUT6Default :
    CanonicalLUT6 []ᴸ nothing Parameter.defaultLUT6INIT

  canonicalLUT6Explicit : ∀ {name text table}
    → primStringEquality name "INIT" ≡ true
    → Hex.decodeHexINITFixed  text ≡ just table
    → CanonicalLUT6
        (Raw.rawParameter name text ∷ᴸ []ᴸ)
        nothing
        table

normaliseLUT6Parameters-sound :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT6Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → CanonicalLUT6 parameters initial-bit table
normaliseLUT6Parameters-sound
  subject []ᴸ nothing table result
  with accepted-injective result
... | default-is-table =
  subst
    (CanonicalLUT6 []ᴸ nothing)
    default-is-table
    canonicalLUT6Default
normaliseLUT6Parameters-sound
  subject []ᴸ (just bit) table result =
  Empty.rec (rejected≢accepted result)
normaliseLUT6Parameters-sound
  subject (Raw.rawParameter name text ∷ᴸ []ᴸ) nothing table result
  with primStringEquality name "INIT"
     | inspect (λ candidate → primStringEquality candidate "INIT") name
... | false | [ name-test ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | true | [ name-test ]ᵢ
  with Hex.decodeHexINITFixed  text
     | inspect (Hex.decodeHexINITFixed ) text
...   | nothing | [ decode-test ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | just decoded | [ decode-test ]ᵢ
  with accepted-injective result
...     | decoded-is-table =
  subst
    (CanonicalLUT6
      (Raw.rawParameter name text ∷ᴸ []ᴸ)
      nothing)
    decoded-is-table
    (canonicalLUT6Explicit {name = name} {text = text} {table = decoded}
      name-test
      decode-test)
normaliseLUT6Parameters-sound
  subject (Raw.rawParameter name text ∷ᴸ []ᴸ) (just bit) table result
  with primStringEquality name "INIT"
... | false = Empty.rec (rejected≢accepted result)
... | true with Hex.decodeHexINITFixed  text
...   | nothing = Empty.rec (rejected≢accepted result)
...   | just decoded = Empty.rec (rejected≢accepted result)
normaliseLUT6Parameters-sound
  subject (first ∷ᴸ second ∷ᴸ rest) nothing table result =
  Empty.rec (rejected≢accepted result)
normaliseLUT6Parameters-sound
  subject (first ∷ᴸ second ∷ᴸ rest) (just bit) table result =
  Empty.rec (rejected≢accepted result)

normaliseLUT6Parameters-complete :
  ∀ subject {parameters initial-bit table}
  → CanonicalLUT6 parameters initial-bit table
  → Parameter.normaliseLUT6Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
normaliseLUT6Parameters-complete
  subject canonicalLUT6Default = refl
normaliseLUT6Parameters-complete
  subject (canonicalLUT6Explicit {name} {text} {table}
            name-test decode-test)
  with primStringEquality name "INIT"
... | false = Empty.rec (false≢true name-test)
... | true with Hex.decodeHexINITFixed  text
...   | nothing = Empty.rec (nothing≢just decode-test)
...   | just decoded =
  cong Diagnostic.accepted (just-injective decode-test)

-- Useful specializations of the exact characterization.

accepted-LUT6-has-no-scalar-INIT :
  ∀ {parameters initial-bit table}
  → CanonicalLUT6 parameters initial-bit table
  → initial-bit ≡ nothing
accepted-LUT6-has-no-scalar-INIT canonicalLUT6Default = refl
accepted-LUT6-has-no-scalar-INIT
  (canonicalLUT6Explicit name-test decode-test) = refl

literal-LUT6-INIT-complete : ∀ subject text table
  → Hex.decodeHexINITFixed  text ≡ just table
  → Parameter.normaliseLUT6Parameters
      subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted table
literal-LUT6-INIT-complete subject text table decode-test =
  normaliseLUT6Parameters-complete subject
    (canonicalLUT6Explicit
      {name = "INIT"} {text = text} {table = table}
      refl decode-test)

-- ScalarInitial describes both register decoders: omission selects the
-- primitive's documented default, while an explicit raw bit is preserved.

data ScalarInitial (default : Bit) : Maybe Bit → Bit → Type₀ where
  scalarDefault : ScalarInitial default nothing default
  scalarExplicit : ∀ bit → ScalarInitial default (just bit) bit

normaliseFDREInitialBit-sound : ∀ initial-bit value
  → Parameter.normaliseFDREInitialBit initial-bit
    ≡ Diagnostic.accepted value
  → ScalarInitial low initial-bit value
normaliseFDREInitialBit-sound nothing value result
  with accepted-injective result
... | default-is-value =
  subst (ScalarInitial low nothing) default-is-value scalarDefault
normaliseFDREInitialBit-sound (just bit) value result
  with accepted-injective result
... | bit-is-value =
  subst (ScalarInitial low (just bit)) bit-is-value (scalarExplicit bit)

normaliseFDREInitialBit-complete : ∀ {initial-bit value}
  → ScalarInitial low initial-bit value
  → Parameter.normaliseFDREInitialBit initial-bit
    ≡ Diagnostic.accepted value
normaliseFDREInitialBit-complete scalarDefault = refl
normaliseFDREInitialBit-complete (scalarExplicit bit) = refl

normaliseFDSEInitialBit-sound : ∀ initial-bit value
  → Parameter.normaliseFDSEInitialBit initial-bit
    ≡ Diagnostic.accepted value
  → ScalarInitial high initial-bit value
normaliseFDSEInitialBit-sound nothing value result
  with accepted-injective result
... | default-is-value =
  subst (ScalarInitial high nothing) default-is-value scalarDefault
normaliseFDSEInitialBit-sound (just bit) value result
  with accepted-injective result
... | bit-is-value =
  subst (ScalarInitial high (just bit)) bit-is-value (scalarExplicit bit)

normaliseFDSEInitialBit-complete : ∀ {initial-bit value}
  → ScalarInitial high initial-bit value
  → Parameter.normaliseFDSEInitialBit initial-bit
    ≡ Diagnostic.accepted value
normaliseFDSEInitialBit-complete scalarDefault = refl
normaliseFDSEInitialBit-complete (scalarExplicit bit) = refl

-- CanonicalScalarParameters adds the raw-shape obligation shared by FDRE and
-- FDSE: successful admission has no string parameters at all.

data CanonicalScalarParameters (default : Bit)
  : List Raw.RawParameter → Maybe Bit → Bit → Type₀ where
  canonicalScalarParameters : ∀ {initial-bit value}
    → ScalarInitial default initial-bit value
    → CanonicalScalarParameters default []ᴸ initial-bit value

CanonicalFDREParameters :
  List Raw.RawParameter → Maybe Bit → Bit → Type₀
CanonicalFDREParameters = CanonicalScalarParameters low

CanonicalFDSEParameters :
  List Raw.RawParameter → Maybe Bit → Bit → Type₀
CanonicalFDSEParameters = CanonicalScalarParameters high

normaliseFDREParameters-sound :
  ∀ subject parameters initial-bit value
  → Parameter.normaliseFDREParameters subject parameters initial-bit
    ≡ Diagnostic.accepted value
  → CanonicalFDREParameters parameters initial-bit value
normaliseFDREParameters-sound subject []ᴸ nothing value result
  with accepted-injective result
... | default-is-value =
  subst
    (CanonicalFDREParameters []ᴸ nothing)
    default-is-value
    (canonicalScalarParameters scalarDefault)
normaliseFDREParameters-sound subject []ᴸ (just bit) value result
  with accepted-injective result
... | bit-is-value =
  subst
    (CanonicalFDREParameters []ᴸ (just bit))
    bit-is-value
    (canonicalScalarParameters (scalarExplicit bit))
normaliseFDREParameters-sound
  subject (parameter ∷ᴸ parameters) nothing value result =
  Empty.rec (rejected≢accepted result)
normaliseFDREParameters-sound
  subject (parameter ∷ᴸ parameters) (just bit) value result =
  Empty.rec (rejected≢accepted result)

normaliseFDREParameters-complete :
  ∀ subject {parameters initial-bit value}
  → CanonicalFDREParameters parameters initial-bit value
  → Parameter.normaliseFDREParameters subject parameters initial-bit
    ≡ Diagnostic.accepted value
normaliseFDREParameters-complete
  subject (canonicalScalarParameters scalarDefault) = refl
normaliseFDREParameters-complete
  subject (canonicalScalarParameters (scalarExplicit bit)) = refl

-- FDSE's full raw decoder is exposed through normaliseCoreParameters.  The
-- accepted value is wrapped by fdseParameters, but its raw-shape theorem is
-- otherwise identical to FDRE's.

fdseParameterValue : Parameter.CoreParameters Architecture.FDSE → Bit
fdseParameterValue (Parameter.fdseParameters bit) = bit

fdseParameters-injective : ∀ {left right}
  → Parameter.fdseParameters left ≡ Parameter.fdseParameters right
  → left ≡ right
fdseParameters-injective path = cong fdseParameterValue path

normaliseFDSEParameters-sound :
  ∀ subject parameters initial-bit value
  → Parameter.normaliseCoreParameters
      Architecture.FDSE subject parameters initial-bit
    ≡ Diagnostic.accepted (Parameter.fdseParameters value)
  → CanonicalFDSEParameters parameters initial-bit value
normaliseFDSEParameters-sound subject []ᴸ nothing value result
  with accepted-injective result
... | wrapped-path =
  subst
    (CanonicalFDSEParameters []ᴸ nothing)
    (fdseParameters-injective wrapped-path)
    (canonicalScalarParameters scalarDefault)
normaliseFDSEParameters-sound subject []ᴸ (just bit) value result
  with accepted-injective result
... | wrapped-path =
  subst
    (CanonicalFDSEParameters []ᴸ (just bit))
    (fdseParameters-injective wrapped-path)
    (canonicalScalarParameters (scalarExplicit bit))
normaliseFDSEParameters-sound
  subject (parameter ∷ᴸ parameters) nothing value result =
  Empty.rec (rejected≢accepted result)
normaliseFDSEParameters-sound
  subject (parameter ∷ᴸ parameters) (just bit) value result =
  Empty.rec (rejected≢accepted result)

normaliseFDSEParameters-complete :
  ∀ subject {parameters initial-bit value}
  → CanonicalFDSEParameters parameters initial-bit value
  → Parameter.normaliseCoreParameters
      Architecture.FDSE subject parameters initial-bit
    ≡ Diagnostic.accepted (Parameter.fdseParameters value)
normaliseFDSEParameters-complete
  subject (canonicalScalarParameters scalarDefault) = refl
normaliseFDSEParameters-complete
  subject (canonicalScalarParameters (scalarExplicit bit)) = refl

-- Reduction checks for the propositional interfaces themselves.

explicit-FDRE-high-is-canonical :
  CanonicalFDREParameters []ᴸ (just high) high
explicit-FDRE-high-is-canonical =
  canonicalScalarParameters (scalarExplicit high)

default-FDSE-high-is-canonical :
  CanonicalFDSEParameters []ᴸ nothing high
default-FDSE-high-is-canonical =
  canonicalScalarParameters scalarDefault

literal-zero-LUT6-is-canonical :
  CanonicalLUT6
    (Raw.rawParameter "INIT" "0000000000000000" ∷ᴸ []ᴸ)
    nothing
    Parameter.defaultLUT6INIT
literal-zero-LUT6-is-canonical =
  canonicalLUT6Explicit
    {name = "INIT"}
    {text = "0000000000000000"}
    {table = Parameter.defaultLUT6INIT}
    refl refl