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

module Spartan6.Semantics.Invariant where

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

record Invariant
  {ℓ : Level}
  {inputCount outputCount registerCount : ℕ}
  (design : Design inputCount outputCount registerCount)
  (Property : State design → Type ℓ) : Type ℓ where
  field
    initially : Property (initial design)
    preserved : ∀ event external state
              → Property state
              → Property (step design event external state)

open Invariant public

run-preserves :
  ∀ {ℓ inputCount outputCount registerCount}
    {design : Design inputCount outputCount registerCount}
    {Property : State design → Type ℓ}
  → Invariant design Property
  → (state : State design)
  → (samples : List (Stimulus inputCount))
  → Property state
  → Property (run design state samples)
run-preserves invariant state []ᴸ property = property
run-preserves {design = design} invariant state (sample ∷ᴸ samples) property =
  run-preserves invariant
    (step design (stimulusEvent sample) (stimulusInputs sample) state)
    samples
    (preserved invariant
      (stimulusEvent sample)
      (stimulusInputs sample)
      state
      property)

initial-run-preserves :
  ∀ {ℓ inputCount outputCount registerCount}
    {design : Design inputCount outputCount registerCount}
    {Property : State design → Type ℓ}
  → (invariant : Invariant design Property)
  → (samples : List (Stimulus inputCount))
  → Property (run design (initial design) samples)
initial-run-preserves invariant samples =
  run-preserves invariant _ samples (initially invariant)