Module Simulation

From Coq Require Import Psatz.
From CDF Require Import Sequences.

A generic simulation diagram, to prove semantic equivalence of two programs based on their small-step semantics.

The diagram is parameterized by - the small-step semantics for each of the two programs: type of configurations and transition relation between configurations; - an invariant that connects the configurations of the two programs - a nonnegative measure over source configurations.

Variable C1: Type. (* the type of configurations for the source program *)
Variable step1: C1 -> C1 -> Prop. (* its transition relation *)

Variable C2: Type. (* the type of configurations for the transformed program *)
Variable step2: C2 -> C2 -> Prop. (* its transition relation *)

Variable inv: C1 -> C2 -> Prop. (* the invariant *)

Variable measure: C1 -> nat. (* the measure that prevents infinite stuttering *)

The diagram properly speaking is the following assumption: every source program transition is simulated by zero, one or several transitions of the transformed program, while preserving the invariant and decreasing the measure in the stuttering case.

Hypothesis simulation:
  forall c1 c1', step1 c1 c1' ->
  forall c2, inv c1 c2 ->
  exists c2',
     (plus step2 c2 c2' \/ (star step2 c2 c2' /\ measure c1' < measure c1))
  /\ inv c1' c2'.

We first extend the simulation diagram to finite sequences of source transitions. This is the crucial lemma to show semantic preservation when the source program terminates.

Lemma simulation_star:
  forall c1 c1', star step1 c1 c1' ->
  forall c2, inv c1 c2 ->
  exists c2', star step2 c2 c2' /\ inv c1' c2'.

Proof.

  induction 1; intros.
- (* zero transitions *)
  exists c2; split. apply star_refl. auto.
- (* one or several transitions *)
  destruct (simulation _ _ H _ H1) as (c2' & P & Q).
  destruct (IHstar _ Q) as (c2'' & U & V).
  exists c2''; split.
  eapply star_trans; eauto. destruct P. apply plus_star; auto. destruct H2; auto.
  auto.
Qed.

Now consider a source program that performs infinitely many transitions. We first show that the transformed program can always make progress (perform at least one transition) while preserving the invariant inv. The proof is by induction on N, the greatest number of stuttering steps that the transformed program can make before being forced to take at least one transition.

Lemma simulation_infseq_productive:
  forall N c1 c2,
  measure c1 < N ->
  infseq step1 c1 ->
  inv c1 c2 ->
  exists c1', exists c2',
      plus step2 c2 c2'
   /\ infseq step1 c1'
   /\ inv c1' c2'.

Proof.

  induction N; intros c1 c2 MEAS INF1 INV.
- (* N = 0 *)
  lia.
- (* N > 0 *)
  destruct (infseq_inv INF1) as (c1' & STEP1 & INF1').
  destruct (simulation _ _ STEP1 _ INV) as (c2' & P & INV').
  destruct P as [STEPS2 | [STEPS2 MEAS']].
  + (* one or several *)
    exists c1'; exists c2'; auto.
  + (* zero, one or several transitions *)
    inversion STEPS2; subst; clear STEPS2.
    * (* zero transitions *)
      eapply IHN; eauto. lia.
    * (* one or several transitions *)
      exists c1'; exists c2'; split. eapply plus_left; eauto. auto.
Qed.

As a consequence, the transformed program performs infinitely many transitions if started in a configuration that is related to a diverging configuration of the source program.

Lemma simulation_infseq:
  forall c1 c2,
  infseq step1 c1 ->
  inv c1 c2 ->
  infseq step2 c2.

Proof.

  intros.
  apply infseq_coinduction_principle with
    (X := fun c2 => exists c1, infseq step1 c1 /\ inv c1 c2).
- clear c1 c2 H H0. intros c2 (c1 & INF & INV).
  destruct (simulation_infseq_productive (measure c1 + 1) c1 c2)
  as (c1' & c2' & PLUS2 & INF' & INV').
  lia. auto. auto.
  exists c2'; split. auto. exists c1'; auto.
- exists c1; auto.
Qed.

End SIMULATION_DIAGRAM.