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

module Spartan6.Import.YosysCorpus where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Generated.YosysIdentityUnknown as UnknownArtifact
import Spartan6.Generated.YosysToggleEnable as ToggleArtifact
import Spartan6.Generated.YosysToggleUninitialised as UninitialisedArtifact
import Spartan6.Import.Json as Import
import Spartan6.Import.Yosys as Yosys
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic

-- The explicit terms below are the small, reusable side of each certificate.
-- Each successful generated JsonValue is related to its term by exactly one
-- decoder equality in this module.  Downstream semantic proofs consume these
-- terms directly and never repeat normalization of the full JSON syntax tree.

toggleRawDesign : Raw.RawDesign
toggleRawDesign =
  Raw.rawDesign nothing
    ( Raw.rawTopPort "clock" Raw.inputPort 1
        (Raw.net 2 ∷ᴸ []ᴸ)
    ∷ᴸ Raw.rawTopPort "reset" Raw.inputPort 1
        (Raw.net 3 ∷ᴸ []ᴸ)
    ∷ᴸ Raw.rawTopPort "toggle_enable" Raw.inputPort 1
        (Raw.net 4 ∷ᴸ []ᴸ)
    ∷ᴸ Raw.rawTopPort "q" Raw.outputPort 1
        (Raw.net 5 ∷ᴸ []ᴸ)
    ∷ᴸ []ᴸ )
    ( Raw.rawInstance
        "$abc$1414$auto$blifparse.cc:557:parse_blif$1415"
        (Raw.knownPrimitive Architecture.LUT2)
        ( Raw.rawPort "I0" Raw.inputPort 1 (Raw.net 5 ∷ᴸ []ᴸ)
        ∷ᴸ Raw.rawPort "I1" Raw.inputPort 1 (Raw.net 4 ∷ᴸ []ᴸ)
        ∷ᴸ Raw.rawPort "O" Raw.outputPort 1 (Raw.net 6 ∷ᴸ []ᴸ)
        ∷ᴸ []ᴸ )
        (Raw.rawParameter "INIT" "6" ∷ᴸ []ᴸ)
        nothing
    ∷ᴸ Raw.rawInstance
        "$auto$ff.cc:337:slice$1334"
        (Raw.knownPrimitive Architecture.FDRE)
        ( Raw.rawPort "D" Raw.inputPort 1 (Raw.net 6 ∷ᴸ []ᴸ)
        ∷ᴸ Raw.rawPort "C" Raw.inputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
        ∷ᴸ Raw.rawPort "CE" Raw.inputPort 1
            (Raw.constant high ∷ᴸ []ᴸ)
        ∷ᴸ Raw.rawPort "R" Raw.inputPort 1 (Raw.net 3 ∷ᴸ []ᴸ)
        ∷ᴸ Raw.rawPort "Q" Raw.outputPort 1 (Raw.net 5 ∷ᴸ []ᴸ)
        ∷ᴸ []ᴸ )
        []ᴸ
        (just low)
    ∷ᴸ []ᴸ )

toggleDecoderEquality :
  Yosys.decodeSelectedModule
    ToggleArtifact.adapterRequestedTop ToggleArtifact.jsonDocument
  ≡ Diagnostic.accepted toggleRawDesign
toggleDecoderEquality = refl

toggleAcceptance :
  Yosys.SelectedModuleAccepted
    ToggleArtifact.adapterRequestedTop ToggleArtifact.jsonDocument
toggleAcceptance =
  Import.acceptedResult toggleRawDesign toggleDecoderEquality

toggleExtractionEquality :
  Yosys.extractSelectedModule
    ToggleArtifact.adapterRequestedTop ToggleArtifact.jsonDocument
    toggleAcceptance
  ≡ toggleRawDesign
toggleExtractionEquality = refl

unknownRawDesign : Raw.RawDesign
unknownRawDesign =
  Raw.rawDesign nothing
    ( Raw.rawTopPort "input_bit" Raw.inputPort 1
        (Raw.net 2 ∷ᴸ []ᴸ)
    ∷ᴸ Raw.rawTopPort "output_bit" Raw.outputPort 1
        (Raw.net 3 ∷ᴸ []ᴸ)
    ∷ᴸ []ᴸ )
    ( Raw.rawInstance
        "$abc$1406$auto$blifparse.cc:557:parse_blif$1407"
        (Raw.unknownPrimitive "INV")
        ( Raw.rawPort "I" Raw.inputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
        ∷ᴸ Raw.rawPort "O" Raw.outputPort 1 (Raw.net 3 ∷ᴸ []ᴸ)
        ∷ᴸ []ᴸ )
        []ᴸ
        nothing
    ∷ᴸ []ᴸ )

unknownDecoderEquality :
  Yosys.decodeSelectedModule
    UnknownArtifact.adapterRequestedTop UnknownArtifact.jsonDocument
  ≡ Diagnostic.accepted unknownRawDesign
unknownDecoderEquality = refl

unknownAcceptance :
  Yosys.SelectedModuleAccepted
    UnknownArtifact.adapterRequestedTop UnknownArtifact.jsonDocument
unknownAcceptance =
  Import.acceptedResult unknownRawDesign unknownDecoderEquality

unknownExtractionEquality :
  Yosys.extractSelectedModule
    UnknownArtifact.adapterRequestedTop UnknownArtifact.jsonDocument
    unknownAcceptance
  ≡ unknownRawDesign
unknownExtractionEquality = refl

-- The uninitialized corpus also contains INV.  INV selects the unknown branch,
-- but INIT=x rejects the complete module before any partial RawDesign exists
-- for the structural checker to diagnose.

uninitialisedINVIsUnknown : Yosys.supportedKind "INV" ≡ nothing
uninitialisedINVIsUnknown = refl

uninitialisedINITPath : Import.JsonPath
uninitialisedINITPath =
  Import.fieldAt
    (Import.fieldAt
      (Import.fieldAt
        (Import.fieldAt
          (Import.fieldAt
            (Import.fieldAt Import.root "modules")
            UninitialisedArtifact.adapterRequestedTop)
          "cells")
        "$auto$ff.cc:337:slice$1333")
      "parameters")
    "INIT"

uninitialisedDecoderRejection :
  Yosys.decodeSelectedModule
    UninitialisedArtifact.adapterRequestedTop
    UninitialisedArtifact.jsonDocument
  ≡ Diagnostic.rejected
      (Yosys.parameterProblem
        Diagnostic.malformedInitialisation
        uninitialisedINITPath
        "defined scalar bit 0 or 1"
        "x"
        "Register INIT does not admit x, z, wider strings, or alternate spellings.")
uninitialisedDecoderRejection = refl