Spartan6.Validation.FixedParameterSoundness

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

module Spartan6.Validation.FixedParameterSoundness 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≢rejected; 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

-- The executable String equality primitive has no safe reflection theorem in
-- the configured library.  Consequently, the canonical explicit-INIT case
-- retains the Boolean equality path actually inspected by the decoder.

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-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

-- This predicate is the exact propositional acceptance boundary of
-- normaliseFixedINITParameterList: either omission selects the supplied
-- default, or one parameter passes both the INIT-name test and the exact-size
-- hexadecimal decoder.

data CanonicalFixedINITParameterList
  (bit-count : ℕ)
  (default : Vec Bit bit-count)
  : List Raw.RawParameter → Vec Bit bit-count → Type₀ where
  canonicalFixedINITDefault :
    CanonicalFixedINITParameterList bit-count default []ᴸ default

  canonicalFixedINITExplicit : ∀ {name text table}
    → primStringEquality name "INIT" ≡ true
    → Hex.decodeHexINITFixed bit-count text ≡ just table
    → CanonicalFixedINITParameterList
        bit-count default
        (Raw.rawParameter name text ∷ᴸ []ᴸ)
        table

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

normaliseFixedINITParameterList-complete :
  ∀ bit-count expected default subject {parameters table}
  → CanonicalFixedINITParameterList
      bit-count default parameters table
  → Parameter.normaliseFixedINITParameterList
      bit-count expected default subject parameters
    ≡ Diagnostic.accepted table
normaliseFixedINITParameterList-complete
  bit-count expected default subject canonicalFixedINITDefault = refl
normaliseFixedINITParameterList-complete
  bit-count expected default subject
  (canonicalFixedINITExplicit {name} {text} {table}
    name-test decode-test)
  with primStringEquality name "INIT"
... | false = Empty.rec (false≢true name-test)
... | true with Hex.decodeHexINITFixed bit-count text
...   | nothing = Empty.rec (nothing≢just decode-test)
...   | just decoded =
  cong Diagnostic.accepted (just-injective decode-test)

normaliseFixedINITParameterList-default :
  ∀ bit-count expected default subject
  → Parameter.normaliseFixedINITParameterList
      bit-count expected default subject []ᴸ
    ≡ Diagnostic.accepted default
normaliseFixedINITParameterList-default
  bit-count expected default subject = refl

literal-fixed-INIT-parameter-complete :
  ∀ bit-count expected default subject text table
  → Hex.decodeHexINITFixed bit-count text ≡ just table
  → Parameter.normaliseFixedINITParameterList
      bit-count expected default subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
    ≡ Diagnostic.accepted table
literal-fixed-INIT-parameter-complete
  bit-count expected default subject text table decode-test =
  normaliseFixedINITParameterList-complete
    bit-count expected default subject
    (canonicalFixedINITExplicit
      {name = "INIT"} {text = text} {table = table}
      refl decode-test)

-- The full vector decoder adds one independent boundary: no scalar INIT may
-- accompany a vector-valued INIT parameter list.

data CanonicalFixedVectorParameters
  (bit-count : ℕ)
  (default : Vec Bit bit-count)
  : List Raw.RawParameter → Maybe Bit → Vec Bit bit-count → Type₀ where
  canonicalFixedVectorParameters : ∀ {parameters table}
    → CanonicalFixedINITParameterList
        bit-count default parameters table
    → CanonicalFixedVectorParameters
        bit-count default parameters nothing table

normaliseFixedVectorParameters-sound :
  ∀ bit-count expected default subject parameters initial-bit table
  → Parameter.normaliseFixedVectorParameters
      bit-count expected default subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → CanonicalFixedVectorParameters
      bit-count default parameters initial-bit table
normaliseFixedVectorParameters-sound
  bit-count expected default subject parameters nothing table result
  with Parameter.normaliseFixedINITParameterList
         bit-count expected default subject parameters
     | inspect
        (Parameter.normaliseFixedINITParameterList
          bit-count expected default 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
    (CanonicalFixedVectorParameters
      bit-count default parameters nothing)
    decoded-is-table
    (canonicalFixedVectorParameters
      (normaliseFixedINITParameterList-sound
        bit-count expected default subject parameters decoded
        parameter-path))
normaliseFixedVectorParameters-sound
  bit-count expected default subject parameters (just bit) table result
  with Parameter.normaliseFixedINITParameterList
    bit-count expected default subject parameters
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted decoded =
  Empty.rec (rejected≢accepted result)

normaliseFixedVectorParameters-complete :
  ∀ bit-count expected default subject
    {parameters initial-bit table}
  → CanonicalFixedVectorParameters
      bit-count default parameters initial-bit table
  → Parameter.normaliseFixedVectorParameters
      bit-count expected default subject parameters initial-bit
    ≡ Diagnostic.accepted table
normaliseFixedVectorParameters-complete
  bit-count expected default subject
  (canonicalFixedVectorParameters canonicalFixedINITDefault) = refl
normaliseFixedVectorParameters-complete
  bit-count expected default subject
  (canonicalFixedVectorParameters
    (canonicalFixedINITExplicit {name} {text} {table}
      name-test decode-test))
  with primStringEquality name "INIT"
... | false = Empty.rec (false≢true name-test)
... | true with Hex.decodeHexINITFixed bit-count text
...   | nothing = Empty.rec (nothing≢just decode-test)
...   | just decoded =
  cong Diagnostic.accepted (just-injective decode-test)

canonicalFixedVector-has-no-scalar-INIT :
  ∀ {bit-count default parameters initial-bit table}
  → CanonicalFixedVectorParameters
      bit-count default parameters initial-bit table
  → initial-bit ≡ nothing
canonicalFixedVector-has-no-scalar-INIT
  (canonicalFixedVectorParameters canonical-parameters) = refl

normaliseFixedVectorParameters-accepted-has-no-scalar-INIT :
  ∀ bit-count expected default subject parameters initial-bit table
  → Parameter.normaliseFixedVectorParameters
      bit-count expected default subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → initial-bit ≡ nothing
normaliseFixedVectorParameters-accepted-has-no-scalar-INIT
  bit-count expected default subject parameters initial-bit table result =
  canonicalFixedVector-has-no-scalar-INIT
    (normaliseFixedVectorParameters-sound
      bit-count expected default subject parameters initial-bit table result)

normaliseFixedVectorParameters-default :
  ∀ bit-count expected default subject
  → Parameter.normaliseFixedVectorParameters
      bit-count expected default subject []ᴸ nothing
    ≡ Diagnostic.accepted default
normaliseFixedVectorParameters-default
  bit-count expected default subject = refl

literal-fixed-vector-INIT-complete :
  ∀ bit-count expected default subject text table
  → Hex.decodeHexINITFixed bit-count text ≡ just table
  → Parameter.normaliseFixedVectorParameters
      bit-count expected default subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted table
literal-fixed-vector-INIT-complete
  bit-count expected default subject text table decode-test =
  normaliseFixedVectorParameters-complete
    bit-count expected default subject
    (canonicalFixedVectorParameters
      (canonicalFixedINITExplicit
        {name = "INIT"} {text = text} {table = table}
        refl decode-test))

-- Rejection is also classified propositionally.  The list decoder cannot
-- reject the empty/default form: it rejects exactly a failed singleton name,
-- a failed exact-width singleton decode, or a list with at least two entries.

data RejectedFixedINITParameterList
  (bit-count : ℕ)
  : List Raw.RawParameter → Type₀ where
  rejectedFixedINITName : ∀ {name text}
    → primStringEquality name "INIT" ≡ false
    → RejectedFixedINITParameterList
        bit-count (Raw.rawParameter name text ∷ᴸ []ᴸ)

  rejectedFixedINITDecode : ∀ {name text}
    → primStringEquality name "INIT" ≡ true
    → Hex.decodeHexINITFixed bit-count text ≡ nothing
    → RejectedFixedINITParameterList
        bit-count (Raw.rawParameter name text ∷ᴸ []ᴸ)

  rejectedFixedINITMultiple : ∀ {first second rest}
    → RejectedFixedINITParameterList
        bit-count (first ∷ᴸ second ∷ᴸ rest)

normaliseFixedINITParameterList-rejection-sound :
  ∀ bit-count expected default subject parameters diagnostics
  → Parameter.normaliseFixedINITParameterList
      bit-count expected default subject parameters
    ≡ Diagnostic.rejected diagnostics
  → RejectedFixedINITParameterList bit-count parameters
normaliseFixedINITParameterList-rejection-sound
  bit-count expected default subject []ᴸ diagnostics result =
  Empty.rec (accepted≢rejected result)
normaliseFixedINITParameterList-rejection-sound
  bit-count expected default subject
  (Raw.rawParameter name text ∷ᴸ []ᴸ) diagnostics result
  with primStringEquality name "INIT"
     | inspect (λ candidate → primStringEquality candidate "INIT") name
... | false | [ name-test ]ᵢ =
  rejectedFixedINITName name-test
... | true | [ name-test ]ᵢ
  with Hex.decodeHexINITFixed bit-count text
     | inspect (Hex.decodeHexINITFixed bit-count) text
...   | nothing | [ decode-test ]ᵢ =
  rejectedFixedINITDecode name-test decode-test
...   | just decoded | [ decode-test ]ᵢ =
  Empty.rec (accepted≢rejected result)
normaliseFixedINITParameterList-rejection-sound
  bit-count expected default subject
  (first ∷ᴸ second ∷ᴸ rest) diagnostics result =
  rejectedFixedINITMultiple

normaliseFixedINITParameterList-rejection-complete :
  ∀ bit-count expected default subject {parameters}
  → RejectedFixedINITParameterList bit-count parameters
  → Σ Diagnostic.Diagnostics
      (λ diagnostics →
        Parameter.normaliseFixedINITParameterList
          bit-count expected default subject parameters
        ≡ Diagnostic.rejected diagnostics)
normaliseFixedINITParameterList-rejection-complete
  bit-count expected default subject
  (rejectedFixedINITName {name} {text} name-test)
  with primStringEquality name "INIT"
... | false = Parameter.illegalLUT6Parameters subject name , refl
... | true = Empty.rec (false≢true (sym name-test))
normaliseFixedINITParameterList-rejection-complete
  bit-count expected default subject
  (rejectedFixedINITDecode {name} {text} name-test decode-test)
  with primStringEquality name "INIT"
... | false = Empty.rec (false≢true name-test)
... | true with Hex.decodeHexINITFixed bit-count text
...   | nothing =
  Parameter.malformedFixedINIT subject expected text , refl
...   | just decoded =
  Empty.rec (nothing≢just (sym decode-test))
normaliseFixedINITParameterList-rejection-complete
  bit-count expected default subject
  (rejectedFixedINITMultiple {first} {second} {rest}) =
  Parameter.illegalLUT6Parameters
    subject "multiple raw parameter entries" ,
  refl

data NonEmptyFixedINITParameterShape
  : List Raw.RawParameter → Type₀ where
  singletonFixedINITParameterShape : ∀ {parameter}
    → NonEmptyFixedINITParameterShape (parameter ∷ᴸ []ᴸ)
  multipleFixedINITParameterShape : ∀ {first second rest}
    → NonEmptyFixedINITParameterShape
        (first ∷ᴸ second ∷ᴸ rest)

rejectedFixedINITParameterList-shape :
  ∀ {bit-count parameters}
  → RejectedFixedINITParameterList bit-count parameters
  → NonEmptyFixedINITParameterShape parameters
rejectedFixedINITParameterList-shape
  (rejectedFixedINITName name-test) =
  singletonFixedINITParameterShape
rejectedFixedINITParameterList-shape
  (rejectedFixedINITDecode name-test decode-test) =
  singletonFixedINITParameterShape
rejectedFixedINITParameterList-shape
  rejectedFixedINITMultiple =
  multipleFixedINITParameterShape

normaliseFixedINITParameterList-rejection-shape :
  ∀ bit-count expected default subject parameters diagnostics
  → Parameter.normaliseFixedINITParameterList
      bit-count expected default subject parameters
    ≡ Diagnostic.rejected diagnostics
  → NonEmptyFixedINITParameterShape parameters
normaliseFixedINITParameterList-rejection-shape
  bit-count expected default subject parameters diagnostics result =
  rejectedFixedINITParameterList-shape
    (normaliseFixedINITParameterList-rejection-sound
      bit-count expected default subject parameters diagnostics result)

-- A full-vector rejection either originates in the parameter list, or occurs
-- after a canonical list was accepted because a scalar INIT was also present.

data RejectedFixedVectorParameters
  (bit-count : ℕ)
  (default : Vec Bit bit-count)
  : List Raw.RawParameter → Maybe Bit → Type₀ where
  rejectedFixedVectorParameterList :
    ∀ {parameters initial-bit}
    → RejectedFixedINITParameterList bit-count parameters
    → RejectedFixedVectorParameters
        bit-count default parameters initial-bit

  rejectedFixedVectorScalarINIT :
    ∀ {parameters table bit}
    → CanonicalFixedINITParameterList
        bit-count default parameters table
    → RejectedFixedVectorParameters
        bit-count default parameters (just bit)

normaliseFixedVectorParameters-rejection-sound :
  ∀ bit-count expected default subject parameters initial-bit diagnostics
  → Parameter.normaliseFixedVectorParameters
      bit-count expected default subject parameters initial-bit
    ≡ Diagnostic.rejected diagnostics
  → RejectedFixedVectorParameters
      bit-count default parameters initial-bit
normaliseFixedVectorParameters-rejection-sound
  bit-count expected default subject parameters nothing diagnostics result
  with Parameter.normaliseFixedINITParameterList
         bit-count expected default subject parameters
     | inspect
        (Parameter.normaliseFixedINITParameterList
          bit-count expected default subject)
        parameters
... | Diagnostic.rejected parameter-diagnostics | [ parameter-path ]ᵢ =
  rejectedFixedVectorParameterList
    (normaliseFixedINITParameterList-rejection-sound
      bit-count expected default subject parameters
      parameter-diagnostics parameter-path)
... | Diagnostic.accepted decoded | [ parameter-path ]ᵢ =
  Empty.rec (accepted≢rejected result)
normaliseFixedVectorParameters-rejection-sound
  bit-count expected default subject parameters (just bit) diagnostics result
  with Parameter.normaliseFixedINITParameterList
         bit-count expected default subject parameters
     | inspect
        (Parameter.normaliseFixedINITParameterList
          bit-count expected default subject)
        parameters
... | Diagnostic.rejected parameter-diagnostics | [ parameter-path ]ᵢ =
  rejectedFixedVectorParameterList
    (normaliseFixedINITParameterList-rejection-sound
      bit-count expected default subject parameters
      parameter-diagnostics parameter-path)
... | Diagnostic.accepted decoded | [ parameter-path ]ᵢ =
  rejectedFixedVectorScalarINIT
    (normaliseFixedINITParameterList-sound
      bit-count expected default subject parameters decoded parameter-path)

normaliseFixedVectorParameters-rejection-complete :
  ∀ bit-count expected default subject {parameters initial-bit}
  → RejectedFixedVectorParameters
      bit-count default parameters initial-bit
  → Σ Diagnostic.Diagnostics
      (λ diagnostics →
        Parameter.normaliseFixedVectorParameters
          bit-count expected default subject parameters initial-bit
        ≡ Diagnostic.rejected diagnostics)
normaliseFixedVectorParameters-rejection-complete
  bit-count expected default subject
  (rejectedFixedVectorParameterList
    {initial-bit = nothing} rejection)
  with normaliseFixedINITParameterList-rejection-complete
    bit-count expected default subject rejection
... | parameter-diagnostics , parameter-path =
  parameter-diagnostics ,
  cong
    (λ parameter-result →
      Diagnostic.mapResult fst
        (Diagnostic.appendResult
          parameter-result (Diagnostic.accepted tt)))
    parameter-path
normaliseFixedVectorParameters-rejection-complete
  bit-count expected default subject
  (rejectedFixedVectorParameterList
    {initial-bit = just bit} rejection)
  with normaliseFixedINITParameterList-rejection-complete
    bit-count expected default subject rejection
... | parameter-diagnostics , parameter-path =
  (parameter-diagnostics ++ᴸ Parameter.unexpectedVectorInitialBit subject) ,
  cong
    (λ parameter-result →
      Diagnostic.mapResult fst
        (Diagnostic.appendResult
          parameter-result
          (Diagnostic.rejected
            (Parameter.unexpectedVectorInitialBit subject))))
    parameter-path
normaliseFixedVectorParameters-rejection-complete
  bit-count expected default subject
  (rejectedFixedVectorScalarINIT canonical-parameters)
  with normaliseFixedINITParameterList-complete
    bit-count expected default subject canonical-parameters
... | parameter-path =
  Parameter.unexpectedVectorInitialBit subject ,
  cong
    (λ parameter-result →
      Diagnostic.mapResult fst
        (Diagnostic.appendResult
          parameter-result
          (Diagnostic.rejected
            (Parameter.unexpectedVectorInitialBit subject))))
    parameter-path

data FixedVectorRejectionBoundary
  : List Raw.RawParameter → Maybe Bit → Type₀ where
  rejectedVectorParameterBoundary : ∀ {parameters initial-bit}
    → NonEmptyFixedINITParameterShape parameters
    → FixedVectorRejectionBoundary parameters initial-bit
  rejectedVectorScalarBoundary : ∀ {parameters bit}
    → FixedVectorRejectionBoundary parameters (just bit)

rejectedFixedVectorParameters-boundary :
  ∀ {bit-count default parameters initial-bit}
  → RejectedFixedVectorParameters
      bit-count default parameters initial-bit
  → FixedVectorRejectionBoundary parameters initial-bit
rejectedFixedVectorParameters-boundary
  (rejectedFixedVectorParameterList rejection) =
  rejectedVectorParameterBoundary
    (rejectedFixedINITParameterList-shape rejection)
rejectedFixedVectorParameters-boundary
  (rejectedFixedVectorScalarINIT canonical-parameters) =
  rejectedVectorScalarBoundary

normaliseFixedVectorParameters-rejection-boundary :
  ∀ bit-count expected default subject parameters initial-bit diagnostics
  → Parameter.normaliseFixedVectorParameters
      bit-count expected default subject parameters initial-bit
    ≡ Diagnostic.rejected diagnostics
  → FixedVectorRejectionBoundary parameters initial-bit
normaliseFixedVectorParameters-rejection-boundary
  bit-count expected default subject parameters initial-bit diagnostics result =
  rejectedFixedVectorParameters-boundary
    (normaliseFixedVectorParameters-rejection-sound
      bit-count expected default subject parameters initial-bit
      diagnostics result)

-- Nibble-aligned LUT specializations.  These aliases and equivalences expose
-- the generic result at the public arity-specific decoder boundary.

CanonicalLUT2Parameters :
  List Raw.RawParameter → Maybe Bit → LUT.TruthTable 2 → Type₀
CanonicalLUT2Parameters =
  CanonicalFixedVectorParameters 4 Parameter.defaultLUT2INIT

CanonicalLUT3Parameters :
  List Raw.RawParameter → Maybe Bit → LUT.TruthTable 3 → Type₀
CanonicalLUT3Parameters =
  CanonicalFixedVectorParameters 8 Parameter.defaultLUT3INIT

CanonicalLUT4Parameters :
  List Raw.RawParameter → Maybe Bit → LUT.TruthTable 4 → Type₀
CanonicalLUT4Parameters =
  CanonicalFixedVectorParameters 16 Parameter.defaultLUT4INIT

CanonicalLUT5Parameters :
  List Raw.RawParameter → Maybe Bit → LUT.TruthTable 5 → Type₀
CanonicalLUT5Parameters =
  CanonicalFixedVectorParameters 32 Parameter.defaultLUT5INIT

normaliseLUT2Parameters-sound :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT2Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → CanonicalLUT2Parameters parameters initial-bit table
normaliseLUT2Parameters-sound =
  normaliseFixedVectorParameters-sound
    4
    "exactly 1 hexadecimal digit encoding 4 INIT bits"
    Parameter.defaultLUT2INIT

normaliseLUT2Parameters-complete :
  ∀ subject {parameters initial-bit table}
  → CanonicalLUT2Parameters parameters initial-bit table
  → Parameter.normaliseLUT2Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
normaliseLUT2Parameters-complete =
  normaliseFixedVectorParameters-complete
    4
    "exactly 1 hexadecimal digit encoding 4 INIT bits"
    Parameter.defaultLUT2INIT

normaliseLUT3Parameters-sound :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT3Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → CanonicalLUT3Parameters parameters initial-bit table
normaliseLUT3Parameters-sound =
  normaliseFixedVectorParameters-sound
    8
    "exactly 2 hexadecimal digits encoding 8 INIT bits"
    Parameter.defaultLUT3INIT

normaliseLUT3Parameters-complete :
  ∀ subject {parameters initial-bit table}
  → CanonicalLUT3Parameters parameters initial-bit table
  → Parameter.normaliseLUT3Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
normaliseLUT3Parameters-complete =
  normaliseFixedVectorParameters-complete
    8
    "exactly 2 hexadecimal digits encoding 8 INIT bits"
    Parameter.defaultLUT3INIT

normaliseLUT4Parameters-sound :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT4Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → CanonicalLUT4Parameters parameters initial-bit table
normaliseLUT4Parameters-sound =
  normaliseFixedVectorParameters-sound
    16
    "exactly 4 hexadecimal digits encoding 16 INIT bits"
    Parameter.defaultLUT4INIT

normaliseLUT4Parameters-complete :
  ∀ subject {parameters initial-bit table}
  → CanonicalLUT4Parameters parameters initial-bit table
  → Parameter.normaliseLUT4Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
normaliseLUT4Parameters-complete =
  normaliseFixedVectorParameters-complete
    16
    "exactly 4 hexadecimal digits encoding 16 INIT bits"
    Parameter.defaultLUT4INIT

normaliseLUT5Parameters-sound :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT5Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → CanonicalLUT5Parameters parameters initial-bit table
normaliseLUT5Parameters-sound =
  normaliseFixedVectorParameters-sound
    32
    "exactly 8 hexadecimal digits encoding 32 INIT bits"
    Parameter.defaultLUT5INIT

normaliseLUT5Parameters-complete :
  ∀ subject {parameters initial-bit table}
  → CanonicalLUT5Parameters parameters initial-bit table
  → Parameter.normaliseLUT5Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
normaliseLUT5Parameters-complete =
  normaliseFixedVectorParameters-complete
    32
    "exactly 8 hexadecimal digits encoding 32 INIT bits"
    Parameter.defaultLUT5INIT

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

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

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

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

literal-LUT2-INIT-complete : ∀ subject text table
  → Hex.decodeHexINITFixed 4 text ≡ just table
  → Parameter.normaliseLUT2Parameters
      subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted table
literal-LUT2-INIT-complete =
  literal-fixed-vector-INIT-complete
    4
    "exactly 1 hexadecimal digit encoding 4 INIT bits"
    Parameter.defaultLUT2INIT

literal-LUT3-INIT-complete : ∀ subject text table
  → Hex.decodeHexINITFixed 8 text ≡ just table
  → Parameter.normaliseLUT3Parameters
      subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted table
literal-LUT3-INIT-complete =
  literal-fixed-vector-INIT-complete
    8
    "exactly 2 hexadecimal digits encoding 8 INIT bits"
    Parameter.defaultLUT3INIT

literal-LUT4-INIT-complete : ∀ subject text table
  → Hex.decodeHexINITFixed 16 text ≡ just table
  → Parameter.normaliseLUT4Parameters
      subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted table
literal-LUT4-INIT-complete =
  literal-fixed-vector-INIT-complete
    16
    "exactly 4 hexadecimal digits encoding 16 INIT bits"
    Parameter.defaultLUT4INIT

literal-LUT5-INIT-complete : ∀ subject text table
  → Hex.decodeHexINITFixed 32 text ≡ just table
  → Parameter.normaliseLUT5Parameters
      subject
      (Raw.rawParameter "INIT" text ∷ᴸ []ᴸ)
      nothing
    ≡ Diagnostic.accepted table
literal-LUT5-INIT-complete =
  literal-fixed-vector-INIT-complete
    32
    "exactly 8 hexadecimal digits encoding 32 INIT bits"
    Parameter.defaultLUT5INIT

normaliseLUT2Parameters-accepted-has-no-scalar-INIT :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT2Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → initial-bit ≡ nothing
normaliseLUT2Parameters-accepted-has-no-scalar-INIT =
  normaliseFixedVectorParameters-accepted-has-no-scalar-INIT
    4
    "exactly 1 hexadecimal digit encoding 4 INIT bits"
    Parameter.defaultLUT2INIT

normaliseLUT3Parameters-accepted-has-no-scalar-INIT :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT3Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → initial-bit ≡ nothing
normaliseLUT3Parameters-accepted-has-no-scalar-INIT =
  normaliseFixedVectorParameters-accepted-has-no-scalar-INIT
    8
    "exactly 2 hexadecimal digits encoding 8 INIT bits"
    Parameter.defaultLUT3INIT

normaliseLUT4Parameters-accepted-has-no-scalar-INIT :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT4Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → initial-bit ≡ nothing
normaliseLUT4Parameters-accepted-has-no-scalar-INIT =
  normaliseFixedVectorParameters-accepted-has-no-scalar-INIT
    16
    "exactly 4 hexadecimal digits encoding 16 INIT bits"
    Parameter.defaultLUT4INIT

normaliseLUT5Parameters-accepted-has-no-scalar-INIT :
  ∀ subject parameters initial-bit table
  → Parameter.normaliseLUT5Parameters
      subject parameters initial-bit
    ≡ Diagnostic.accepted table
  → initial-bit ≡ nothing
normaliseLUT5Parameters-accepted-has-no-scalar-INIT =
  normaliseFixedVectorParameters-accepted-has-no-scalar-INIT
    32
    "exactly 8 hexadecimal digits encoding 32 INIT bits"
    Parameter.defaultLUT5INIT

normaliseLUT2Parameters-rejection-boundary :
  ∀ subject parameters initial-bit diagnostics
  → Parameter.normaliseLUT2Parameters
      subject parameters initial-bit
    ≡ Diagnostic.rejected diagnostics
  → FixedVectorRejectionBoundary parameters initial-bit
normaliseLUT2Parameters-rejection-boundary =
  normaliseFixedVectorParameters-rejection-boundary
    4
    "exactly 1 hexadecimal digit encoding 4 INIT bits"
    Parameter.defaultLUT2INIT

normaliseLUT3Parameters-rejection-boundary :
  ∀ subject parameters initial-bit diagnostics
  → Parameter.normaliseLUT3Parameters
      subject parameters initial-bit
    ≡ Diagnostic.rejected diagnostics
  → FixedVectorRejectionBoundary parameters initial-bit
normaliseLUT3Parameters-rejection-boundary =
  normaliseFixedVectorParameters-rejection-boundary
    8
    "exactly 2 hexadecimal digits encoding 8 INIT bits"
    Parameter.defaultLUT3INIT

normaliseLUT4Parameters-rejection-boundary :
  ∀ subject parameters initial-bit diagnostics
  → Parameter.normaliseLUT4Parameters
      subject parameters initial-bit
    ≡ Diagnostic.rejected diagnostics
  → FixedVectorRejectionBoundary parameters initial-bit
normaliseLUT4Parameters-rejection-boundary =
  normaliseFixedVectorParameters-rejection-boundary
    16
    "exactly 4 hexadecimal digits encoding 16 INIT bits"
    Parameter.defaultLUT4INIT

normaliseLUT5Parameters-rejection-boundary :
  ∀ subject parameters initial-bit diagnostics
  → Parameter.normaliseLUT5Parameters
      subject parameters initial-bit
    ≡ Diagnostic.rejected diagnostics
  → FixedVectorRejectionBoundary parameters initial-bit
normaliseLUT5Parameters-rejection-boundary =
  normaliseFixedVectorParameters-rejection-boundary
    32
    "exactly 8 hexadecimal digits encoding 32 INIT bits"
    Parameter.defaultLUT5INIT