Module PLF_SPEC_op

Require Import List.
Import ListNotations.
Require Import Relations.

Require Import util.
Require Import specification.
Require Import plf.
Require Import PLFO.
Require Import PL.
Require Import PLO.

Require Import PLF_PLFO.
Require Import PLFO_PL.
Require Import PL_PLO.
Require Import PLO_SPEC.
Require PLF_SPEC.

Final correctness theorem, with explicit trace filtering


The final correctness result can be alternatively stated using an operational characterization of the subtrace relation. Given the trace emitted by the PLF machine, the corresponding subtrace emitted by the SPEC machine can be explicitly built with the filter function: ∀ t. PLF.sem t -> SPEC.sem (filter t).

Defining the filter function


Filtering portions of trace from failing checkpointing
Fixpoint split_at_chkpt_events (t: PLF.trace) : list (bool * PL.trace) :=
  match t with
  | [] => []
  | PLF.ChkptS::t => (true, []) :: (split_at_chkpt_events t)
  | PLF.ChkptF::t => (false, []) :: (split_at_chkpt_events t)
  | e::t =>
    match split_at_chkpt_events t with
    | [] => [(false, match e with
                     | PLF.LogS => [PL.LogS]
                     | PLF.LogF => [PL.LogF]
                     | PLF.Op op => [PL.Op op]
                     | _ => []
                     end)]
    | (b,x)::m => (b, match e with
                      | PLF.LogS => PL.LogS::x
                      | PLF.LogF => PL.LogF::x
                      | PLF.Op op => (PL.Op op)::x
                      | _ => []
                      end)::m
    end
  end.

Fixpoint x_filter_chkpt (t: list (bool * PL.trace)) : PL.trace :=
  match t with
  | [] => []
  | (true, t')::t => t'++ x_filter_chkpt t
  | (false,_ )::t => x_filter_chkpt t
  end.

Definition filter_chkpt (t: PLF.trace) : PL.trace :=
  x_filter_chkpt (split_at_chkpt_events t).

Filtering portions of PL.trace from aborted power-continuous sections.
Fixpoint split_at_log_events (t: PL.trace) : list (bool * SPEC.trace) :=
  match t with
  | [] => []
  | PL.LogS::t => (true, []) :: (split_at_log_events t)
  | PL.LogF::t => (false, []) :: (split_at_log_events t)
  | PL.Op op::t =>
    match split_at_log_events t with
    | [] => [(false, [op])]
    | (b,x)::m => (b, op::x)::m
    end
  end.

Fixpoint x_filter_log (t: list (bool * SPEC.trace)) : SPEC.trace :=
  match t with
  | [] => []
  | (true, t')::t => t' ++ x_filter_log t
  | (false,_ )::t => x_filter_log t
  end.

Definition filter_log (t: PL.trace) : SPEC.trace :=
  x_filter_log (split_at_log_events t).

The final filter function
Definition filter (t: PLF.trace) : SPEC.trace :=
  filter_log (filter_chkpt t).


Properties of the filter_chkpt function.


Properties of the auxiliary split_at_chkpt_events function.

Lemma split_at_chkpt_events_ops_nil : forall top,
    forall b pt,
      In (b,pt) (split_at_chkpt_events (map PLFevent top)) ->
      b = false.
Proof.
  induction top; intros.
  - inv H.
  - destruct a; simpl in *.
    + destruct split_at_chkpt_events.
      * inv H; try congruence.
        inv H0.
      * destruct p. inv H.
        -- inv H0. eapply IHtop; eauto with datatypes.
        -- eapply IHtop; eauto with datatypes.
    + destruct split_at_chkpt_events.
      * inv H; try congruence.
        inv H0.
      * destruct p. inv H.
        -- inv H0. eapply IHtop; eauto with datatypes.
        -- eapply IHtop; eauto with datatypes.
    + destruct split_at_chkpt_events.
      * inv H; try congruence.
        inv H0.
      * destruct p. inv H.
        -- inv H0. eapply IHtop; eauto with datatypes.
        -- eapply IHtop; eauto with datatypes.
Qed.

Lemma split_at_chkpt_events_split_F : forall top tend,
    split_at_chkpt_events (map PLFevent top ++ PLF.ChkptF :: tend) =
    (false, top)::split_at_chkpt_events tend.
Proof.
  induction top; intros.
  - simpl. auto.
  - destruct a; simpl.
    + case_eq (split_at_chkpt_events (map PLFevent top ++ PLF.ChkptF :: tend)); intros.
      * rewrite IHtop in H; eauto.
        congruence.
      * rewrite IHtop in H; eauto.
        inv H. auto.
    + case_eq (split_at_chkpt_events (map PLFevent top ++ PLF.ChkptF :: tend)); intros.
      * rewrite IHtop in H; eauto.
        congruence.
      * rewrite IHtop in H; eauto.
        inv H. auto.
    + case_eq (split_at_chkpt_events (map PLFevent top ++ PLF.ChkptF :: tend)); intros.
      * rewrite IHtop in H; eauto.
        congruence.
      * rewrite IHtop in H; eauto.
        inv H. auto.
Qed.

Lemma split_at_chkpt_events_split_S : forall top tend,
    split_at_chkpt_events (map PLFevent top ++ PLF.ChkptS :: tend) =
    (true, top)::split_at_chkpt_events tend.
Proof.
  induction top; intros.
  - simpl. auto.
  - destruct a; simpl.
    + case_eq (split_at_chkpt_events (map PLFevent top ++ PLF.ChkptS :: tend)); intros.
      * rewrite IHtop in H; eauto.
        congruence.
      * rewrite IHtop in H; eauto.
        inv H. auto.
    + case_eq (split_at_chkpt_events (map PLFevent top ++ PLF.ChkptS :: tend)); intros.
      * rewrite IHtop in H; eauto.
        congruence.
      * rewrite IHtop in H; eauto.
        inv H. auto.
    + case_eq (split_at_chkpt_events (map PLFevent top ++ PLF.ChkptS :: tend)); intros.
      * rewrite IHtop in H; eauto.
        congruence.
      * rewrite IHtop in H; eauto.
        inv H. auto.
Qed.

Lemma x_filter_chkpt_false : forall l,
    (forall b x, In (b,x) l -> b = false) ->
    x_filter_chkpt l = [].
Proof.
  induction l ; intros.
  - auto.
  - simpl. destruct a.
    rewrite (H b t); eauto with datatypes.
Qed.

Lemmas characterizing the filtering action of filter_chkpt

Lemma filter_chkpt_ops_nil: forall top,
    filter_chkpt (map PLFevent top) = [].
Proof.
  unfold filter_chkpt.
  intros.
  eapply x_filter_chkpt_false; eauto.
  eapply split_at_chkpt_events_ops_nil; eauto.
Qed.

Lemma filter_chkpt_false : forall top tend,
    filter_chkpt (map PLFevent top ++ PLF.ChkptF :: tend) =
    filter_chkpt tend.
Proof.
  unfold filter_chkpt. intros.
  rewrite split_at_chkpt_events_split_F.
  simpl; auto.
Qed.

Lemma filter_chkpt_true : forall top tend,
    filter_chkpt (map PLFevent top ++ PLF.ChkptS :: tend) =
    top ++ filter_chkpt tend.
Proof.
  unfold filter_chkpt. intros.
  rewrite split_at_chkpt_events_split_S.
  simpl; auto.
Qed.

Alternative induction principle to reason about PLF traces.
Inductive PLFtrace : PLF.trace -> Prop :=
| plftrace_op : forall op,
    PLFtrace (map PLFevent op)
| plftrace_chkptS : forall op tend,
    PLFtrace tend ->
    PLFtrace ((map PLFevent op)++ PLF.ChkptS::tend)
| plftrace_chkptF : forall op tend,
    PLFtrace tend ->
    PLFtrace ((map PLFevent op)++ PLF.ChkptF::tend).

Lemma PLFtrace_ind' : forall t, PLFtrace t.
Proof.
  induction t ; intros.
  - eapply (plftrace_op []).
  - destruct a.
    + eapply (plftrace_chkptS [] t); auto.
    + eapply (plftrace_chkptF [] t); auto.
    + inv IHt.
      * eapply (plftrace_op (LogS::op)); auto.
      * eapply (plftrace_chkptS (LogS::op)); auto.
      * eapply (plftrace_chkptF (LogS::op)); auto.
    + inv IHt.
      * eapply (plftrace_op (LogF::op)); auto.
      * eapply (plftrace_chkptS (LogF::op)); auto.
      * eapply (plftrace_chkptF (LogF::op)); auto.
    + inv IHt.
      * eapply (plftrace_op (Op o::op)); auto.
      * eapply (plftrace_chkptS (Op o::op)); auto.
      * eapply (plftrace_chkptF (Op o::op)); auto.
Qed.

The filter_chkpt is correct for the subtrace_chk relation
Lemma filter_chkpt_correct: forall t,
    exists b, subtrace_chk b t (filter_chkpt t).
Proof.
  intros.
  generalize (PLFtrace_ind' t).
  induction 1 ; intros.
  - exists false.
    unfold filter_chkpt.
    erewrite x_filter_chkpt_false; eauto.
    + apply subtrace_chkpt_ops.
    + apply split_at_chkpt_events_ops_nil ; eauto.
  - destruct IHPLFtrace as [b Hsub].
    rewrite filter_chkpt_true.
    exists true.
    eapply subtrace_chk_alt_subtrace_chk; eauto.
    eapply subtrace_chk_subtrace_chk_alt in Hsub; eauto.
    econstructor; eauto. econstructor; eauto.
  - destruct IHPLFtrace as [b Hsub].
    rewrite filter_chkpt_false.
    exists false.
    eapply subtrace_chk_alt_subtrace_chk; eauto.
    eapply subtrace_chk_subtrace_chk_alt in Hsub; eauto.
    econstructor; eauto. econstructor; eauto.
Qed.

The subtrace_chk co-domain is populated with traces filtered with filter_chkpt.
Lemma filter_chkpt_complete : forall t b t',
    subtrace_chk b t t' ->
    t' = filter_chkpt t.
Proof.
  intros.
  edestruct (filter_chkpt_correct t) as [bt Hsubt].
  eapply subtrace_chk_unique; eauto.
Qed.
    

Properties of the filter_log function.


Properties of the auxiliary split_at_log_events function.

Lemma split_at_log_events_ops_nil : forall top,
    forall b pt,
      In (b,pt) (split_at_log_events (map Op top)) ->
      b = false.
Proof.
  induction top; intros.
  - inv H.
  - simpl in *.
    destruct split_at_log_events.
    + inv H; inv H0. auto.
    + destruct p. inv H.
        -- inv H0. eapply IHtop; eauto with datatypes.
        -- eapply IHtop; eauto with datatypes.
Qed.

Lemma split_at_log_events_split_F : forall top tend,
    split_at_log_events (map Op top ++ LogF :: tend) =
    (false, top)::split_at_log_events tend.
Proof.
  induction top; intros.
  - simpl. auto.
  - simpl.
    case_eq (split_at_log_events (map Op top ++ LogF :: tend)); intros.
    * rewrite IHtop in H; eauto.
      congruence.
    * rewrite IHtop in H; eauto.
      inv H. auto.
Qed.

Lemma split_at_log_events_split_S : forall top tend,
    split_at_log_events (map Op top ++ LogS :: tend) =
    (true, top)::split_at_log_events tend.
Proof.
  induction top; intros.
  - simpl. auto.
  - simpl.
    case_eq (split_at_log_events (map Op top ++ LogS :: tend)); intros.
    * rewrite IHtop in H; eauto.
      congruence.
    * rewrite IHtop in H; eauto.
      inv H. auto.
Qed.

Lemma x_filter_log_false : forall l,
    (forall b x, In (b,x) l -> b = false) ->
    x_filter_log l = [].
Proof.
  induction l ; intros.
  - auto.
  - simpl. destruct a.
    rewrite (H b t); eauto with datatypes.
Qed.

Lemmas characterizing the filtering action of filter_log.

Lemma filter_log_ops_nil: forall top,
    filter_log (map Op top) = [].
Proof.
  unfold filter_log.
  intros.
  eapply x_filter_log_false; eauto.
  eapply split_at_log_events_ops_nil; eauto.
Qed.

Lemma filter_log_false : forall top tend,
    filter_log (map Op top ++ LogF :: tend) =
    filter_log tend.
Proof.
  unfold filter_log. intros.
  rewrite split_at_log_events_split_F.
  simpl; auto.
Qed.

Lemma filter_log_true : forall top tend,
    filter_log (map Op top ++ LogS :: tend) =
    top ++ filter_log tend.
Proof.
  unfold filter_log. intros.
  rewrite split_at_log_events_split_S.
  simpl; auto.
Qed.


Alternative induction principle to reason about PL traces.
Inductive PLtrace : PL.trace -> Prop :=
| pltrace_op : forall op,
    PLtrace (map PL.Op op)
| pltrace_LogS : forall op tend,
    PLtrace tend ->
    PLtrace ((map PL.Op op)++ LogS::tend)
| pltrace_LogF : forall op tend,
    PLtrace tend ->
    PLtrace ((map PL.Op op)++ LogF::tend).

Lemma PLtrace_ind' : forall t, PLtrace t.
Proof.
  induction t ; intros.
  - eapply (pltrace_op []).
  - destruct a.
    + eapply (pltrace_LogS [] t); auto.
    + eapply (pltrace_LogF [] t); auto.
    + inv IHt.
      * eapply (pltrace_op (o::op)); auto.
      * eapply (pltrace_LogS (o::op)); auto.
      * eapply (pltrace_LogF (o::op)); auto.
Qed.

The filter_log is correct for the subtrace_log relation
Lemma filter_log_correct: forall t,
    exists b, subtrace_log b t (filter_log t).
Proof.
  intros.
  generalize (PLtrace_ind' t).
  induction 1 ; intros.
  - exists false.
    unfold filter_log.
    erewrite x_filter_log_false; eauto.
    + apply subtrace_log_ops.
    + apply split_at_log_events_ops_nil ; eauto.
  - destruct IHPLtrace as [b Hsub].
    rewrite filter_log_true.
    exists true.
    eapply subtrace_log_alt_subtrace_log; eauto.
    eapply subtrace_log_subtrace_log_alt in Hsub; eauto.
    econstructor; eauto. econstructor; eauto.
  - destruct IHPLtrace as [b Hsub].
    rewrite filter_log_false.
    exists false.
    eapply subtrace_log_alt_subtrace_log; eauto.
    eapply subtrace_log_subtrace_log_alt in Hsub; eauto.
    econstructor; eauto. econstructor; eauto.
Qed.

The subtrace_log co-domain is populated with traces filtered with filter_log.
Lemma filter_log_complete : forall t b t',
    subtrace_log b t t' ->
    t' = filter_log t.
Proof.
  intros.
  edestruct (filter_log_correct t) as [bt Hsubt].
  eapply subtrace_log_unique; eauto.
Qed.

filter functionally characterizes the subtrace relation


filter is a correct implementation of subtrace
Lemma filter_correct: forall t,
    PLF_SPEC.subtrace t (filter t).
Proof.
  intros.
  unfold filter.
  exists (filter_chkpt t).
  edestruct (filter_chkpt_correct t) as [bc Hsubc].
  edestruct (filter_log_correct (filter_chkpt t)) as [bl Hsubl].
  eauto.
Qed.
  
filter is a complete implementation of subtrace
Lemma filter_complete: forall t t',
    PLF_SPEC.subtrace t t' ->
    t' = filter t.
Proof.
  intros.
  assert (Hcor:= filter_correct t).
  eapply PLF_SPEC.subtrace_unicity; eauto.
Qed.
                                     

Final correctness result, with explicit trace filtering

Theorem correctness_final: forall t,
    PLF.sem t ->
    SPEC.sem (filter t).
Proof.
  intros.
  eapply PLF_SPEC.correctness_final in H; eauto.
  destruct H as [t' [Hsem Hsub]].
  eapply filter_complete in Hsub.
  congruence.
Qed.