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

module Spartan6.Netlist.OBUFDSBuilderSoundness where

open import Spartan6.Prelude

import Spartan6.Netlist.BuildOBUFDS as Build
import Spartan6.Netlist.BuilderCore as Generic
import Spartan6.Netlist.Carry4BuilderSoundness as Evaluation
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Expression as Expression
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.CycleSoundness as Cycle

open import Spartan6.Validation.CheckResult
  using (accepted?; rejected≢accepted; accepted-injective)
open import Cubical.Data.Nat using (_≡ᵇ_)
open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty

-- The exact builder produced by the accepted OBUFDS witness: O aliases the
-- incoming wire, while OB is a newly appended invert node.

constructedOBUFDS : ∀ {inputCount registerCount}
  → (current : Generic.Builder inputCount registerCount)
  → Checked.Wire
      inputCount registerCount (Generic.builderLocalCount current)
  → Raw.NetId
  → Raw.NetId
  → Generic.Builder inputCount registerCount
constructedOBUFDS current input positive-net negative-net =
  Generic.extendBuilder
    (Generic.aliasBuilder current positive-net input)
    negative-net
    (Checked.invertNode input)

-- Lifting the aliased input over the appended invert node preserves its
-- compiled expression for arbitrary prior external/state/local structure.

positive-evaluation : ∀ {inputCount registerCount}
  (current : Generic.Builder inputCount registerCount)
  input positive-net negative-net external state
  → Evaluation.evaluateBuilderWire
      (constructedOBUFDS current input positive-net negative-net)
      external state
      (Generic.liftLocalWire input)
    ≡ Evaluation.evaluateBuilderWire current external state input
positive-evaluation
  (Generic.builder local-count nodes bindings)
  input positive-net negative-net external state =
  cong (Expression.eval external state)
    (Evaluation.compile-liftLocalWire
      nodes (Checked.invertNode input) input)

negative-evaluation : ∀ {inputCount registerCount}
  (current : Generic.Builder inputCount registerCount)
  input positive-net negative-net external state
  → Evaluation.evaluateBuilderWire
      (constructedOBUFDS current input positive-net negative-net)
      external state
      (Checked.localWire fzero)
    ≡ not (Evaluation.evaluateBuilderWire current external state input)
negative-evaluation
  (Generic.builder local-count nodes bindings)
  input positive-net negative-net external state = refl

-- Lookup lemmas expose exactly where raw-ID shadowing matters.  A head
-- binding always wins; a provably different head ID is skipped.

lookup-head : ∀ {inputCount registerCount localCount}
  (net-id : Raw.NetId)
  (wire : Checked.Wire inputCount registerCount localCount)
  (bindings : Generic.Bindings inputCount registerCount localCount)
  → Generic.lookupNet net-id
      (Generic.bindNet net-id wire ∷ᴸ bindings)
    ≡ just wire
lookup-head net-id wire bindings =
  subst
    (λ same →
      (if same then just wire else Generic.lookupNet net-id bindings)
      ≡ just wire)
    (sym (Cycle.nat-equality-reflexive net-id))
    refl

lookup-skips-different :
  ∀ {inputCount registerCount localCount}
  (wanted other : Raw.NetId)
  (other-wire : Checked.Wire inputCount registerCount localCount)
  (bindings : Generic.Bindings inputCount registerCount localCount)
  → (wanted ≡ᵇ other) ≡ false
  → Generic.lookupNet wanted
      (Generic.bindNet other other-wire ∷ᴸ bindings)
    ≡ Generic.lookupNet wanted bindings
lookup-skips-different wanted other other-wire bindings different =
  subst
    (λ same →
      (if same
       then just other-wire
       else Generic.lookupNet wanted bindings)
      ≡ Generic.lookupNet wanted bindings)
    (sym different)
    refl

distinct-accepted?-is-not : ∀ positive-net negative-net
  → accepted? (Build.distinctOutputNets positive-net negative-net)
    ≡ not (positive-net ≡ᵇ negative-net)
distinct-accepted?-is-not positive-net negative-net
  with positive-net ≡ᵇ negative-net
... | false = refl
... | true = refl

distinctOutputNets-false : ∀ positive-net negative-net
  → Build.distinctOutputNets positive-net negative-net
    ≡ Diagnostic.accepted tt
  → (positive-net ≡ᵇ negative-net) ≡ false
distinctOutputNets-false positive-net negative-net result
  with positive-net ≡ᵇ negative-net UsingEq
... | false , comparison = comparison
... | true , comparison =
  Empty.rec
    (false≢true
      (sym (cong not comparison)
       ∙ sym (distinct-accepted?-is-not positive-net negative-net)
       ∙ cong accepted? result))

negative-output-bound : ∀ {inputCount registerCount}
  (current : Generic.Builder inputCount registerCount)
  input positive-net negative-net
  → Generic.lookupNet negative-net
      (Generic.builderBindings
        (constructedOBUFDS current input positive-net negative-net))
    ≡ just (Checked.localWire fzero)
negative-output-bound
  (Generic.builder local-count nodes bindings)
  input positive-net negative-net =
  lookup-head negative-net (Checked.localWire fzero)
    (Generic.liftLocalBindings
      (Generic.bindNet positive-net input ∷ᴸ bindings))

positive-output-bound : ∀ {inputCount registerCount}
  (current : Generic.Builder inputCount registerCount)
  input positive-net negative-net
  → Build.distinctOutputNets positive-net negative-net
    ≡ Diagnostic.accepted tt
  → Generic.lookupNet positive-net
      (Generic.builderBindings
        (constructedOBUFDS current input positive-net negative-net))
    ≡ just (Generic.liftLocalWire input)
positive-output-bound
  (Generic.builder local-count nodes bindings)
  input positive-net negative-net distinct =
  lookup-skips-different
    positive-net negative-net (Checked.localWire fzero)
    (Generic.liftLocalBindings
      (Generic.bindNet positive-net input ∷ᴸ bindings))
    (distinctOutputNets-false positive-net negative-net distinct)
  ∙ lookup-head positive-net (Generic.liftLocalWire input)
      (Generic.liftLocalBindings bindings)

-- This record is the reusable local correspondence boundary.  It says which
-- checked wires the two raw IDs retrieve and how those wires evaluate.

record OBUFDSBuilderCorrespondence
  {inputCount registerCount : ℕ}
  (current : Generic.Builder inputCount registerCount)
  (input : Checked.Wire
    inputCount registerCount (Generic.builderLocalCount current))
  (positive-net negative-net : Raw.NetId)
  (result : Generic.Builder inputCount registerCount)
  (external : Vec Bit inputCount)
  (state : Vec Bit registerCount)
  : Type₀ where
  field
    positiveWire : Checked.Wire
      inputCount registerCount (Generic.builderLocalCount result)
    negativeWire : Checked.Wire
      inputCount registerCount (Generic.builderLocalCount result)

    positiveBinding :
      Generic.lookupNet positive-net (Generic.builderBindings result)
      ≡ just positiveWire
    negativeBinding :
      Generic.lookupNet negative-net (Generic.builderBindings result)
      ≡ just negativeWire

    positiveValue :
      Evaluation.evaluateBuilderWire result external state positiveWire
      ≡ Evaluation.evaluateBuilderWire current external state input
    negativeValue :
      Evaluation.evaluateBuilderWire result external state negativeWire
      ≡ not (Evaluation.evaluateBuilderWire current external state input)

open OBUFDSBuilderCorrespondence public

constructedOBUFDS-correspondence :
  ∀ {inputCount registerCount}
  (current : Generic.Builder inputCount registerCount)
  input positive-net negative-net external state
  → Build.distinctOutputNets positive-net negative-net
    ≡ Diagnostic.accepted tt
  → OBUFDSBuilderCorrespondence
      current input positive-net negative-net
      (constructedOBUFDS current input positive-net negative-net)
      external state
constructedOBUFDS-correspondence
  (Generic.builder local-count nodes bindings)
  input positive-net negative-net external state distinct =
  record
    { positiveWire = Generic.liftLocalWire input
    ; negativeWire = Checked.localWire fzero
    ; positiveBinding =
        positive-output-bound
          (Generic.builder local-count nodes bindings)
          input positive-net negative-net distinct
    ; negativeBinding =
        negative-output-bound
          (Generic.builder local-count nodes bindings)
          input positive-net negative-net
    ; positiveValue =
        positive-evaluation
          (Generic.builder local-count nodes bindings)
          input positive-net negative-net external state
    ; negativeValue =
        negative-evaluation
          (Generic.builder local-count nodes bindings)
          input positive-net negative-net external state
    }

-- Every accepted build result already contains the one shadowing premise
-- needed locally: O and OB have distinct raw IDs.  No freshness premise
-- against older bindings is needed because both new bindings precede them.

build-result-correspondence :
  ∀ {inputCount registerCount item current}
  (built : Build.OBUFDSBuildResult
    {inputCount = inputCount} {registerCount = registerCount}
    item current)
  (external : Vec Bit inputCount)
  (state : Vec Bit registerCount)
  → OBUFDSBuilderCorrespondence
      current
      (Build.resolvedInput built)
      (Build.positiveOutputNet built)
      (Build.negativeOutputNet built)
      (Build.resultBuilder built)
      external state
build-result-correspondence built external state =
  subst
    (λ result →
      OBUFDSBuilderCorrespondence
        _ _ _ _ result external state)
    (sym (Build.resultBuilderBuilt built))
    (constructedOBUFDS-correspondence
      _ _ _ _ external state (Build.outputNetsDistinct built))

-- Bare processOBUFDS acceptance can be replayed to the specialized build
-- witness and the same correspondence, so projection does not lose semantic
-- provenance.

record ProcessedOBUFDSCorrespondence
  {inputCount registerCount : ℕ}
  (item : Raw.RawInstance)
  (current next : Generic.Builder inputCount registerCount)
  (external : Vec Bit inputCount)
  (state : Vec Bit registerCount)
  : Type₀ where
  field
    buildEvidence : Build.OBUFDSBuildResult item current
    nextIsResult : next ≡ Build.resultBuilder buildEvidence
    processedCorrespondence :
      OBUFDSBuilderCorrespondence
        current
        (Build.resolvedInput buildEvidence)
        (Build.positiveOutputNet buildEvidence)
        (Build.negativeOutputNet buildEvidence)
        next external state

open ProcessedOBUFDSCorrespondence public

processOBUFDS-correspondence :
  ∀ {inputCount registerCount}
  (item : Raw.RawInstance)
  (current next : Generic.Builder inputCount registerCount)
  (external : Vec Bit inputCount)
  (state : Vec Bit registerCount)
  → Build.processOBUFDS item current ≡ Diagnostic.accepted next
  → ProcessedOBUFDSCorrespondence
      item current next external state
processOBUFDS-correspondence
  item current next external state result
  with Build.buildOBUFDS item current
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted built
  with accepted-injective result
...   | built-is-next =
  record
    { buildEvidence = built
    ; nextIsResult = sym built-is-next
    ; processedCorrespondence =
        subst
          (λ result-builder →
            OBUFDSBuilderCorrespondence
              current
              (Build.resolvedInput built)
              (Build.positiveOutputNet built)
              (Build.negativeOutputNet built)
              result-builder external state)
          built-is-next
          (build-result-correspondence built external state)
    }