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

module Tutorials.Project04.Main where

open import Spartan6.API.Netlist

inputA inputB : Fin 2
inputA = fzero
inputB = fsuc fzero

-- One XOR node feeds two outputs.  A tree representation could duplicate the
-- XOR expression; the DAG gives it one local entry and lets both outputs refer
-- to that entry.

sharedXorNodes : Checked.Nodes 2 0 1
sharedXorNodes =
  Checked.noNodes Checked.▻
    Checked.xorNode
      (Checked.externalWire inputA)
      (Checked.externalWire inputB)

sharedFanout : Checked.CheckedNetlist 2 2 0 1
sharedFanout =
  Checked.checkedNetlist
    []
    sharedXorNodes
    (Checked.localWire fzero ∷ Checked.localWire fzero ∷ [])
    []

sampleInputs : Vec Bit 2
sampleInputs = high ∷ low ∷ []

the-shared-node-has-one-value :
  Direct.evaluateNodes sharedXorNodes sampleInputs [] ≡ high ∷ []
the-shared-node-has-one-value = refl

both-outputs-use-that-one-value :
  Direct.directOutputs sharedFanout sampleInputs [] ≡ high ∷ high ∷ []
both-outputs-use-that-one-value = refl

-- Expression compilation is retained as an independent specification route.
-- This theorem is stronger than checking one sample: the library proof works
-- for every checked netlist and input/state vector.

direct-evaluation-agrees-with-expression-compilation :
  Direct.directOutputs sharedFanout sampleInputs []
  ≡ Semantics.observe
      (Checked.compileNetlist sharedFanout) sampleInputs []
direct-evaluation-agrees-with-expression-compilation =
  Direct.directOutputs-compile sharedFanout sampleInputs []

stableFanout : Stable.StableNetlist 2 2 0 1
stableFanout = Stable.convertNetlist sharedFanout

append-stable-evaluation-retains-the-result :
  Stable.stableDirectOutputs stableFanout sampleInputs []
  ≡ high ∷ high ∷ []
append-stable-evaluation-retains-the-result = refl

-- During construction, natural ordinals remain stable as nodes are appended.
-- Extending the builder adds a new binding but does not rewrite the old one.

emptyBuilder : Builder.StableBuilder 2 0
emptyBuilder = Builder.emptyBuilder 2 0

withXor : Builder.StableBuilder 2 0
withXor =
  Builder.extendBuilder emptyBuilder 40
    (Stable.stableXor
      (Stable.stableExternal inputA)
      (Stable.stableExternal inputB))

withInversion : Builder.StableBuilder 2 0
withInversion =
  Builder.extendBuilder withXor 41
    (Stable.stableInvert (Stable.stableLocal fzero))

old-binding-keeps-ordinal-zero :
  Builder.builderBindings withInversion
  ≡ Builder.bindStable 41 (Builder.localReference 1)
    ∷ᴸ Builder.bindStable 40 (Builder.localReference 0)
    ∷ᴸ []ᴸ
old-binding-keeps-ordinal-zero = refl