Traces

We consider traces of the (global) step relation, defined as its reflexive-transitive closure, and use these to prove invariants as state predicates:

open import Prelude.Closures _—→_ public
  using ( begin_; _∎
        ; _↞—_; _⟨_⟩←—_; _⟨_∣_⟩←—_
        ; _—↠_; _—→⟨_⟩_
        ; Reachable; Invariant; StepPreserved; Step⇒Invariant
        ; Trace; TraceProperty; TraceInvariant
        )

StateProperty = GlobalState → Type

Now, we can consider a specific local step occurring within a sequence of global transitions:

record Step : Type where
  constructor _⊢_
  field
    stepArgs : _ × _ × _ × _ × _
    step : let p , e , ls , mm , ls' = stepArgs in
           p ▷ e ⊢ ls —[ mm ]→ ls'

LocalStepProperty = Step → Type

allLocalSteps : (s′ ↞— s) → List Step
allLocalSteps = λ where
  (_ ∎) → []
  (_ ⟨ LocalStep st ⟩←— tr) → (_ ⊢ st) ∷ allLocalSteps tr
  (_ ⟨ _ ⟩←— tr) → allLocalSteps tr

_∋⋯_ : Trace → LocalStepProperty → Type
(_ , _ , _ , tr) ∋⋯ P = Any P (allLocalSteps tr)