Library OracleLanguages.ReductionTrace

Basic definitions about reduction traces.
We introduce reduction traces for any deterministic programming language coinductively. Reachability and convergence are defined on top of this notion.

Require Import ProgrammingLanguage.
Require Import Common.

While we will often abusively refer to potentially infinite non-empty lists of configurations as traces, actual reduction traces are characterized by the following trace predicate:

CoInductive trace (L : language) :
  configuration L coplist (configuration L) Prop :=

| TFinal : genv state,
    step L genv state = None
    trace L (genv, state) (CSingle _ (genv, state))
| TStep : genv state S' tr,
    step L genv state = Some S'
    trace L (genv, S') tr
    trace L (genv, state) (CCons _ (genv, state) tr).

We also provide a variant trace' of the trace predicate that hides the precise configuration the trace starts from:

Definition trace' (L : language) (l : coplist (configuration L)) : Prop :=
  trace L (first l) l.

Lemma trace_first {L : language}:
   (c : configuration L) l, trace L c l first l = c.

Lemma trace_trace':
   L l, trace' L l ( c, trace L c l).

Converging and crashing traces are characterized by inductive predicates:

Inductive nsteps_converging_trace {L : language}
  : nat coplist (configuration L) Prop :=
| FinallyConverges:
   c result,
  state_final L (snd c) = Some result
  nsteps_converging_trace 0 (CSingle _ c)
| CConsConverges : c tr n,
  nsteps_converging_trace n tr
  nsteps_converging_trace (S n) (CCons _ c tr).

Inductive nsteps_crashing_trace {L : language}
  : nat coplist (configuration L) Prop :=
| FinallyCrashes:
  step L (fst c) (snd c) = None
  state_final L (snd c) = None
  nsteps_crashing_trace 0 (CSingle _ c)
| CConsCrashes : c tr n,
  nsteps_crashing_trace n tr
  nsteps_crashing_trace (S n) (CCons _ c tr).

CoFixpoint traceFrom {L : language} (c : configuration L) : coplist (configuration L) :=
  match step L (fst c) (snd c) with
  | None
    CSingle _ c
  | Some state'
    CCons _ c (traceFrom (fst c, state'))

Lemma traceFrom_trace:
   L (c : configuration L),
    trace L c (traceFrom c).

Definition program_trace (L : language) (p : prog L) :=
  traceFrom (initial_configuration p).

Lemma nsteps_skipn:
   L tr n genv S S',
    trace L (genv, S) tr
    opt_state_eq (nsteps genv n S) (Some S')
     tr' S'',
      skipn n tr = Some tr'
       trace L (genv, S'') tr'
       state_eq L S'' S'.

CoInductive included_subtrace {L : language}
  : coplist (configuration L) coplist (configuration L) Prop :=
| SameFirst:
     tr₁ tr₂,
    configuration_eq (first tr₁) (first tr₂)
    ( tr₁',
        next tr₁ = Some tr₁'
         tr₂', next tr₂ = Some tr₂' included_subtrace tr₁' tr₂')
    included_subtrace tr₁ tr₂
| Stutter:
     tr₁ tr₁' tr₂,
      configuration_eq (first tr₁) (first tr₂)
      next tr₁ = Some tr₁'
      included_subtrace tr₁' tr₂
      included_subtrace tr₁ tr₂
| IgnoreFirstSN:
     n tr₁ tr₂ tr₂',
      skipn (S n) tr₂ = Some tr₂'
      included_subtrace tr₁ tr₂'
      included_subtrace tr₁ tr₂.