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

module Spartan6.Validation.LUT1ParameterSoundness where

open import Spartan6.Prelude

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

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

private
  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≢nothing : ∀ {ℓ} {A : Type ℓ} {value : A}
    → just value ≡ nothing
    → Empty.⊥
  just≢nothing path = nothing≢just (sym 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

-- The nibble-level statement exposes the range check without relying on
-- reflection from characters or Strings.  Exactly the low two nibble bits
-- survive, in vendor INIT order; both high padding bits are low.

data CanonicalTwoBitINITNibble
  : Hex.Nibble → Vec Bit  → Type₀ where
  canonicalTwoBitINITNibble : ∀ {b1 b0}
    → CanonicalTwoBitINITNibble
        (low ∷ low ∷ b1 ∷ b0 ∷ [])
        (b0 ∷ b1 ∷ [])

twoBitINITNibble-sound : ∀ nibble table
  → Hex.twoBitINITNibble nibble ≡ just table
  → CanonicalTwoBitINITNibble nibble table
twoBitINITNibble-sound
  (false ∷ false ∷ b1 ∷ b0 ∷ []) table result
  with just-injective result
... | decoded-is-table =
  subst
    (CanonicalTwoBitINITNibble
      (low ∷ low ∷ b1 ∷ b0 ∷ []))
    decoded-is-table
    canonicalTwoBitINITNibble
twoBitINITNibble-sound
  (false ∷ true ∷ b1 ∷ b0 ∷ []) table result =
  Empty.rec (nothing≢just result)
twoBitINITNibble-sound
  (true ∷ b2 ∷ b1 ∷ b0 ∷ []) table result =
  Empty.rec (nothing≢just result)

twoBitINITNibble-complete : ∀ {nibble table}
  → CanonicalTwoBitINITNibble nibble table
  → Hex.twoBitINITNibble nibble ≡ just table
twoBitINITNibble-complete canonicalTwoBitINITNibble = refl

data HighPaddedTwoBitINITNibble : Hex.Nibble → Type₀ where
  secondPaddingBitHigh : ∀ {b1 b0}
    → HighPaddedTwoBitINITNibble
        (low ∷ high ∷ b1 ∷ b0 ∷ [])
  topPaddingBitHigh : ∀ {b2 b1 b0}
    → HighPaddedTwoBitINITNibble
        (high ∷ b2 ∷ b1 ∷ b0 ∷ [])

twoBitINITNibble-rejection-sound : ∀ nibble
  → Hex.twoBitINITNibble nibble ≡ nothing
  → HighPaddedTwoBitINITNibble nibble
twoBitINITNibble-rejection-sound
  (false ∷ false ∷ b1 ∷ b0 ∷ []) result =
  Empty.rec (just≢nothing result)
twoBitINITNibble-rejection-sound
  (false ∷ true ∷ b1 ∷ b0 ∷ []) result =
  secondPaddingBitHigh
twoBitINITNibble-rejection-sound
  (true ∷ b2 ∷ b1 ∷ b0 ∷ []) result =
  topPaddingBitHigh

twoBitINITNibble-rejection-complete : ∀ {nibble}
  → HighPaddedTwoBitINITNibble nibble
  → Hex.twoBitINITNibble nibble ≡ nothing
twoBitINITNibble-rejection-complete secondPaddingBitHigh = refl
twoBitINITNibble-rejection-complete topPaddingBitHigh = refl

-- At the String boundary we retain the safe conversion and hexDigit paths.
-- This proves that successful decode is one recognized character whose
-- decoded nibble satisfies the low-padding condition above.

data CanonicalHexINIT2 : String → Vec Bit  → Type₀ where
  canonicalHexINIT2 : ∀ {text char nibble table}
    → primStringToList text ≡ char ∷ᴸ []ᴸ
    → Hex.hexDigit char ≡ just nibble
    → CanonicalTwoBitINITNibble nibble table
    → CanonicalHexINIT2 text table

decodeHexINIT2-sound : ∀ text table
  → Hex.decodeHexINIT2 text ≡ just table
  → CanonicalHexINIT2 text table
decodeHexINIT2-sound text table result
  with primStringToList text | inspect primStringToList text
... | []ᴸ | [ characters-path ]ᵢ =
  Empty.rec (nothing≢just result)
... | first ∷ᴸ second ∷ᴸ rest | [ characters-path ]ᵢ =
  Empty.rec (nothing≢just result)
... | char ∷ᴸ []ᴸ | [ characters-path ]ᵢ
  with Hex.hexDigit char | inspect Hex.hexDigit char
...   | nothing | [ digit-path ]ᵢ =
  Empty.rec (nothing≢just result)
...   | just nibble | [ digit-path ]ᵢ
  with Hex.twoBitINITNibble nibble
     | inspect Hex.twoBitINITNibble nibble
...     | nothing | [ nibble-path ]ᵢ =
  Empty.rec (nothing≢just result)
...     | just decoded | [ nibble-path ]ᵢ
  with just-injective result
...       | decoded-is-table =
  subst
    (CanonicalHexINIT2 text)
    decoded-is-table
    (canonicalHexINIT2
      characters-path digit-path
      (twoBitINITNibble-sound nibble decoded nibble-path))

decodeSingleHexINIT2-complete : ∀ char nibble table
  → Hex.hexDigit char ≡ just nibble
  → CanonicalTwoBitINITNibble nibble table
  → Hex.decodeTwoBitINITChars (char ∷ᴸ []ᴸ) ≡ just table
decodeSingleHexINIT2-complete char nibble table digit-path canonical-nibble
  with Hex.hexDigit char
... | nothing = Empty.rec (nothing≢just digit-path)
... | just decoded
  with just-injective digit-path
...   | decoded-is-nibble =
  twoBitINITNibble-complete
    (subst
      (λ candidate → CanonicalTwoBitINITNibble candidate table)
      (sym decoded-is-nibble)
      canonical-nibble)

decodeHexINIT2-complete : ∀ {text table}
  → CanonicalHexINIT2 text table
  → Hex.decodeHexINIT2 text ≡ just table
decodeHexINIT2-complete
  (canonicalHexINIT2 {char = char} {nibble = nibble} {table = table}
    characters-path digit-path canonical-nibble) =
  subst
    (λ characters →
      Hex.decodeTwoBitINITChars characters ≡ just table)
    (sym characters-path)
    (decodeSingleHexINIT2-complete
      char nibble table digit-path canonical-nibble)

-- The parameter-list boundary is either omission with the all-low default,
-- or exactly one name/value pair that passes the Boolean INIT-name test and
-- the range-checked two-bit decoder.

data CanonicalLUT1ParameterList
  : List Raw.RawParameter → LUT.TruthTable  → Type₀ where
  canonicalLUT1ParameterDefault :
    CanonicalLUT1ParameterList []ᴸ Parameter.defaultLUT1INIT

  canonicalLUT1ParameterExplicit : ∀ {name text table}
    → primStringEquality name "INIT" ≡ true
    → Hex.decodeHexINIT2 text ≡ just table
    → CanonicalLUT1ParameterList
        (Raw.rawParameter name text ∷ᴸ []ᴸ)
        table

normaliseLUT1ParameterList-sound :
  ∀ subject parameters table
  → Parameter.normaliseLUT1ParameterList subject parameters
    ≡ Diagnostic.accepted table
  → CanonicalLUT1ParameterList parameters table
normaliseLUT1ParameterList-sound subject []ᴸ table result
  with accepted-injective result
... | default-is-table =
  subst
    (CanonicalLUT1ParameterList []ᴸ)
    default-is-table
    canonicalLUT1ParameterDefault
normaliseLUT1ParameterList-sound subject
  (Raw.rawParameter name text ∷ᴸ []ᴸ) 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.decodeHexINIT2 text | inspect Hex.decodeHexINIT2 text
...   | nothing | [ decode-test ]ᵢ =
  Empty.rec (rejected≢accepted result)
...   | just decoded | [ decode-test ]ᵢ
  with accepted-injective result
...     | decoded-is-table =
  subst
    (CanonicalLUT1ParameterList
      (Raw.rawParameter name text ∷ᴸ []ᴸ))
    decoded-is-table
    (canonicalLUT1ParameterExplicit
      {name = name} {text = text} {table = decoded}
      name-test decode-test)
normaliseLUT1ParameterList-sound subject
  (first ∷ᴸ second ∷ᴸ rest) table result =
  Empty.rec (rejected≢accepted result)

normaliseLUT1ParameterList-complete :
  ∀ subject {parameters table}
  → CanonicalLUT1ParameterList parameters table
  → Parameter.normaliseLUT1ParameterList subject parameters
    ≡ Diagnostic.accepted table
normaliseLUT1ParameterList-complete
  subject canonicalLUT1ParameterDefault = refl
normaliseLUT1ParameterList-complete subject
  (canonicalLUT1ParameterExplicit {name} {text} {table}
    name-test decode-test)
  with primStringEquality name "INIT"
... | false = Empty.rec (false≢true name-test)
... | true with Hex.decodeHexINIT2 text
...   | nothing = Empty.rec (nothing≢just decode-test)
...   | just decoded =
  cong Diagnostic.accepted (just-injective decode-test)

canonicalLUT1Explicit-range : ∀ {name text table}
  → CanonicalLUT1ParameterList
      (Raw.rawParameter name text ∷ᴸ []ᴸ) table
  → CanonicalHexINIT2 text table
canonicalLUT1Explicit-range
  (canonicalLUT1ParameterExplicit name-test decode-test) =
  decodeHexINIT2-sound _ _ decode-test

data LUT1AcceptedParameterShape
  : List Raw.RawParameter → Type₀ where
  LUT1DefaultParameterShape : LUT1AcceptedParameterShape []ᴸ
  LUT1SingletonParameterShape : ∀ {parameter}
    → LUT1AcceptedParameterShape (parameter ∷ᴸ []ᴸ)

canonicalLUT1ParameterList-shape : ∀ {parameters table}
  → CanonicalLUT1ParameterList parameters table
  → LUT1AcceptedParameterShape parameters
canonicalLUT1ParameterList-shape canonicalLUT1ParameterDefault =
  LUT1DefaultParameterShape
canonicalLUT1ParameterList-shape
  (canonicalLUT1ParameterExplicit name-test decode-test) =
  LUT1SingletonParameterShape

-- The full normalizer adds the vector/scalar separation: every canonical
-- LUT1 parameter list is admitted only when rawInstanceInitialBit is absent.

data CanonicalLUT1Parameters
  : List Raw.RawParameter → Maybe Bit → LUT.TruthTable  → Type₀ where
  canonicalLUT1Parameters : ∀ {parameters table}
    → CanonicalLUT1ParameterList parameters table
    → CanonicalLUT1Parameters parameters nothing table

normaliseLUT1Parameters-sound :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT1Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → CanonicalLUT1Parameters parameters initial-bit table
normaliseLUT1Parameters-sound
  subject parameters nothing table result
  with Parameter.normaliseLUT1ParameterList subject parameters
     | inspect (Parameter.normaliseLUT1ParameterList subject) parameters
... | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted decoded | [ parameter-path ]ᵢ
  with accepted-injective result
...   | decoded-is-table =
  subst
    (CanonicalLUT1Parameters parameters nothing)
    decoded-is-table
    (canonicalLUT1Parameters
      (normaliseLUT1ParameterList-sound
        subject parameters decoded parameter-path))
normaliseLUT1Parameters-sound
  subject parameters (just bit) table result
  with Parameter.normaliseLUT1ParameterList subject parameters
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted decoded =
  Empty.rec (rejected≢accepted result)

normaliseLUT1Parameters-complete :
  ∀ subject {parameters initial-bit table}
  → CanonicalLUT1Parameters parameters initial-bit table
  → Parameter.normaliseLUT1Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
normaliseLUT1Parameters-complete subject
  (canonicalLUT1Parameters canonicalLUT1ParameterDefault) = refl
normaliseLUT1Parameters-complete subject
  (canonicalLUT1Parameters
    (canonicalLUT1ParameterExplicit {name} {text} {table}
      name-test decode-test))
  with primStringEquality name "INIT"
... | false = Empty.rec (false≢true name-test)
... | true with Hex.decodeHexINIT2 text
...   | nothing = Empty.rec (nothing≢just decode-test)
...   | just decoded =
  cong Diagnostic.accepted (just-injective decode-test)

canonicalLUT1-has-no-scalar-INIT :
  ∀ {parameters initial-bit table}
  → CanonicalLUT1Parameters parameters initial-bit table
  → initial-bit ≡ nothing
canonicalLUT1-has-no-scalar-INIT
  (canonicalLUT1Parameters canonical-parameters) = refl

normaliseLUT1Parameters-accepted-has-no-scalar-INIT :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT1Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → initial-bit ≡ nothing
normaliseLUT1Parameters-accepted-has-no-scalar-INIT
  subject parameters initial-bit table result =
  canonicalLUT1-has-no-scalar-INIT
    (normaliseLUT1Parameters-sound
      subject parameters initial-bit table result)

normaliseLUT1Parameters-accepted-shape :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT1Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → LUT1AcceptedParameterShape parameters
normaliseLUT1Parameters-accepted-shape
  subject parameters initial-bit table result
  with normaliseLUT1Parameters-sound
    subject parameters initial-bit table result
... | canonicalLUT1Parameters canonical-parameters =
  canonicalLUT1ParameterList-shape canonical-parameters

-- Direct boundary corollaries for clients that do not need to construct the
-- canonical predicates themselves.

normaliseLUT1Parameters-default : ∀ subject
  → Parameter.normaliseLUT1Parameters subject []ᴸ nothing
    ≡ Diagnostic.accepted Parameter.defaultLUT1INIT
normaliseLUT1Parameters-default subject = refl

literal-LUT1-INIT-complete : ∀ subject text table
  → Hex.decodeHexINIT2 text ≡ just table
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted table
literal-LUT1-INIT-complete subject text table decode-test =
  normaliseLUT1Parameters-complete subject
    (canonicalLUT1Parameters
      (canonicalLUT1ParameterExplicit
        {name = "INIT"} {text = text} {table = table}
        refl decode-test))

literal-LUT1-INIT-decode-rejected : ∀ subject text
  → Hex.decodeHexINIT2 text ≡ nothing
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.rejected
        (Parameter.malformedFixedINIT
          subject
          "exactly 1 hexadecimal digit in the range 0..3 encoding 2 INIT bits"
          text)
literal-LUT1-INIT-decode-rejected subject text decode-test
  with Hex.decodeHexINIT2 text
... | nothing = refl
... | just table = Empty.rec (just≢nothing decode-test)

literal-LUT1-INIT-zero : ∀ subject
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" "0" ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted (low ∷ low ∷ [])
literal-LUT1-INIT-zero subject =
  literal-LUT1-INIT-complete
    subject "0" (low ∷ low ∷ []) Hex.two-bit-INIT-zero

literal-LUT1-INIT-one : ∀ subject
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" "1" ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted (high ∷ low ∷ [])
literal-LUT1-INIT-one subject =
  literal-LUT1-INIT-complete
    subject "1" (high ∷ low ∷ []) Hex.two-bit-INIT-one

literal-LUT1-INIT-two : ∀ subject
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" "2" ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted (low ∷ high ∷ [])
literal-LUT1-INIT-two subject =
  literal-LUT1-INIT-complete
    subject "2" (low ∷ high ∷ []) Hex.two-bit-INIT-two

literal-LUT1-INIT-three : ∀ subject
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" "3" ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted (high ∷ high ∷ [])
literal-LUT1-INIT-three subject =
  literal-LUT1-INIT-complete
    subject "3" (high ∷ high ∷ []) Hex.two-bit-INIT-three

literal-LUT1-INIT-four-is-high-padding : ∀ subject
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" "4" ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.rejected
        (Parameter.malformedFixedINIT
          subject
          "exactly 1 hexadecimal digit in the range 0..3 encoding 2 INIT bits"
          "4")
literal-LUT1-INIT-four-is-high-padding subject =
  literal-LUT1-INIT-decode-rejected
    subject "4" Hex.two-bit-INIT-rejects-high-padding

literal-LUT1-INIT-F-is-high-padding : ∀ subject
  → Parameter.normaliseLUT1Parameters
      subject
      (Raw.rawParameter "INIT" "F" ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.rejected
        (Parameter.malformedFixedINIT
          subject
          "exactly 1 hexadecimal digit in the range 0..3 encoding 2 INIT bits"
          "F")
literal-LUT1-INIT-F-is-high-padding subject =
  literal-LUT1-INIT-decode-rejected subject "F" refl