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

module Tutorials.Project05.Main where

open import Spartan6.API.Validation

-- Imported data is not executable merely because it parsed as JSON.  The
-- envelope retains the exact source identity, and RawArtifact additionally
-- proves which safe decoder produced the raw design.

the-complete-json-tree-is-retained :
  Artifact.jsonValue Fixtures.toggleArtifact ≡ Fixtures.toggleJsonDocument
the-complete-json-tree-is-retained = refl

the-adapter-identity-is-retained :
  Artifact.adapterName (Artifact.envelope Fixtures.toggleArtifact)
  ≡ "yosys-json-to-agda"
the-adapter-identity-is-retained = refl

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

-- Validation first decodes exact primitive modes and ports, then establishes
-- connectivity.  Only the successful branch can yield ValidatedDesign.

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

validatedToggle : Validation.ValidatedDesign Fixtures.toggleArtifact
validatedToggle =
  Located.extractValid
    (Validation.validateArtifact Fixtures.toggleArtifact)
    toggle-validation-is-successful

decoded-stage-is-retained : Decoded.DecodedDesign Fixtures.toggleArtifact
decoded-stage-is-retained = Validation.decoded validatedToggle

-- Dense net numbers are deterministic bookkeeping, not invented source
-- identities.  The certificate retains their correspondence to raw IDs.

dense-net-map-is-canonical :
  Validation.denseNetCorrespondence validatedToggle
  ≡ Provenance.enumerateDenseFrom 
      (Validation.denseRawNets
        (Artifact.decodedDesign Fixtures.toggleArtifact))
dense-net-map-is-canonical =
  Validation.denseNetCorrespondence-is-canonical validatedToggle

-- The same pipeline rejects an unknown primitive.  Located rejections are
-- nonempty by construction; the legacy projection remains available for old
-- callers without making the malformed input executable.

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

legacy-view-also-rejects-the-unknown-mode :
  Result.accepted?
    (Validation.validateArtifactLegacy Fixtures.unknownArtifact)
  ≡ false
legacy-view-also-rejects-the-unknown-mode = refl