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

module Spartan6.Fixtures.YosysArtifacts where

open import Spartan6.Prelude

import FF.Json as JSON
import Spartan6.Generated.YosysToggleEnable as Generated
import Spartan6.Generated.YosysIdentityUnknown as UnknownGenerated
import Spartan6.Import.Artifact as Artifact
import Spartan6.Import.YosysCorpus as Corpus
import Spartan6.Validation.Design as Validation
import Spartan6.Validation.LocatedDiagnostic as Located

-- Pinned corpus fixtures are reusable validation inputs, not examples whose
-- theorem names happen to be consumed as an API.  Their envelopes retain the
-- exact generated bytes' digest and decoder equality.

toggleJsonDocument : JSON.JsonValue
toggleJsonDocument = Generated.jsonDocument

toggleAdapterSourceSHA256 : String
toggleAdapterSourceSHA256 = Generated.adapterSourceSHA256

toggleEnvelope : Artifact.ArtifactEnvelope
toggleEnvelope = Artifact.artifactEnvelope
  Artifact.sha256
  toggleAdapterSourceSHA256
  "yosys-json-to-agda" "1"
  "Yosys JSON" "0.62"
  Generated.adapterRequestedTop Generated.adapterRequestedTop
  []ᴸ []ᴸ false false
  "tools/yosys_json_to_agda.py"

toggleArtifact : Artifact.RawArtifact
toggleArtifact = Artifact.rawArtifact
  toggleEnvelope toggleJsonDocument Corpus.toggleRawDesign
  Corpus.toggleDecoderEquality

toggle-digest-is-exact :
  Artifact.artifactDigest (Artifact.envelope toggleArtifact)
  ≡ toggleAdapterSourceSHA256
toggle-digest-is-exact = refl

toggle-validation-succeeds :
  Located.isValid (Validation.validateArtifact toggleArtifact) ≡ true
toggle-validation-succeeds = refl

toggleValidated : Validation.ValidatedDesign toggleArtifact
toggleValidated = Located.extractValid
  (Validation.validateArtifact toggleArtifact)
  toggle-validation-succeeds

unknownEnvelope : Artifact.ArtifactEnvelope
unknownEnvelope = Artifact.artifactEnvelope
  Artifact.sha256
  UnknownGenerated.adapterSourceSHA256
  "yosys-json-to-agda" "1"
  "Yosys JSON" "0.62"
  UnknownGenerated.adapterRequestedTop UnknownGenerated.adapterRequestedTop
  []ᴸ []ᴸ false false
  "tools/yosys_json_to_agda.py"

unknownArtifact : Artifact.RawArtifact
unknownArtifact = Artifact.rawArtifact
  unknownEnvelope UnknownGenerated.jsonDocument Corpus.unknownRawDesign
  Corpus.unknownDecoderEquality

unknown-mode-is-permanent-validation-failure :
  Located.isValid (Validation.validateArtifact unknownArtifact) ≡ false
unknown-mode-is-permanent-validation-failure = refl