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

module Spartan6.Semantics.Execution where

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

-- Relational presentation of the executable finite-step semantics.  It is
-- indexed by the exact pre-state, stimulus list, and post-state.

data Executes
  {inputCount outputCount registerCount : ℕ}
  (design : Design inputCount outputCount registerCount)
  : Vec Bit registerCount
  → List (Stimulus inputCount)
  → Vec Bit registerCount
  → Type₀ where

  executionDone : ∀ {state}
                → Executes design state []ᴸ state

  executionStep : ∀ {state final samples}
                → (sample : Stimulus inputCount)
                → Executes design
                    (step design
                          (stimulusEvent sample)
                          (stimulusInputs sample)
                          state)
                    samples
                    final
                → Executes design state (sample ∷ᴸ samples) final

run-executes :
  ∀ {inputCount outputCount registerCount}
    (design : Design inputCount outputCount registerCount)
    (state : Vec Bit registerCount)
    (samples : List (Stimulus inputCount))
  → Executes design state samples (run design state samples)
run-executes design state []ᴸ = executionDone
run-executes design state (sample ∷ᴸ samples) =
  executionStep sample
    (run-executes design
      (step design
            (stimulusEvent sample)
            (stimulusInputs sample)
            state)
      samples)

execution-complete :
  ∀ {inputCount outputCount registerCount}
    {design : Design inputCount outputCount registerCount}
    {state final : Vec Bit registerCount}
    {samples : List (Stimulus inputCount)}
  → Executes design state samples final
  → run design state samples ≡ final
execution-complete executionDone = refl
execution-complete (executionStep sample execution) =
  execution-complete execution

execution-final-unique :
  ∀ {inputCount outputCount registerCount}
    {design : Design inputCount outputCount registerCount}
    {state left right : Vec Bit registerCount}
    {samples : List (Stimulus inputCount)}
  → Executes design state samples left
  → Executes design state samples right
  → left ≡ right
execution-final-unique left-execution right-execution =
  sym (execution-complete left-execution)
  ∙ execution-complete right-execution