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

module Spartan6.Semantics.Equivalence where

open import Spartan6.Prelude
open import Spartan6.Semantics.Design

record BehaviorallyEquivalent
  {inputCount outputCount registerCount : ℕ}
  (left right : Design inputCount outputCount registerCount) : Type₀ where
  field
    initialAgreement : initial left ≡ initial right
    outputAgreement  : ∀ external state
                     → observe left external state ≡ observe right external state
    stepAgreement    : ∀ event external state
                     → step left event external state ≡ step right event external state

open BehaviorallyEquivalent public

reflexive : ∀ {inputCount outputCount registerCount}
              (design : Design inputCount outputCount registerCount)
          → BehaviorallyEquivalent design design
initialAgreement (reflexive design) = refl
outputAgreement (reflexive design) external state = refl
stepAgreement (reflexive design) event external state = refl

symmetric : ∀ {inputCount outputCount registerCount}
              {left right : Design inputCount outputCount registerCount}
          → BehaviorallyEquivalent left right
          → BehaviorallyEquivalent right left
initialAgreement (symmetric equivalence) =
  sym (initialAgreement equivalence)
outputAgreement (symmetric equivalence) external state =
  sym (outputAgreement equivalence external state)
stepAgreement (symmetric equivalence) event external state =
  sym (stepAgreement equivalence event external state)

transitive : ∀ {inputCount outputCount registerCount}
               {left middle right : Design inputCount outputCount registerCount}
           → BehaviorallyEquivalent left middle
           → BehaviorallyEquivalent middle right
           → BehaviorallyEquivalent left right
initialAgreement (transitive first second) =
  initialAgreement first ∙ initialAgreement second
outputAgreement (transitive first second) external state =
  outputAgreement first external state ∙ outputAgreement second external state
stepAgreement (transitive first second) event external state =
  stepAgreement first event external state
  ∙ stepAgreement second event external state

run-agreement :
  ∀ {inputCount outputCount registerCount}
    {left right : Design inputCount outputCount registerCount}
  → (equivalence : BehaviorallyEquivalent left right)
  → (state : Vec Bit registerCount)
  → (stimuli : List (Stimulus inputCount))
  → run left state stimuli ≡ run right state stimuli
run-agreement equivalence state []ᴸ = refl
run-agreement {left = left} {right = right}
              equivalence state (sample ∷ᴸ samples) =
  cong (λ next → run left next samples)
       (stepAgreement equivalence
         (stimulusEvent sample) (stimulusInputs sample) state)
  ∙ run-agreement equivalence
      (step right (stimulusEvent sample) (stimulusInputs sample) state)
      samples

initial-run-agreement :
  ∀ {inputCount outputCount registerCount}
    {left right : Design inputCount outputCount registerCount}
  → (equivalence : BehaviorallyEquivalent left right)
  → (stimuli : List (Stimulus inputCount))
  → run left (initial left) stimuli ≡ run right (initial right) stimuli
initial-run-agreement {left = left} equivalence stimuli =
  cong (λ state → run left state stimuli) (initialAgreement equivalence)
  ∙ run-agreement equivalence _ stimuli