Module HeaderBounds

Correctness proof of header bounds.

Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.

Require Import Coqlib.
Require Import Integers.
Require Import Errors.
Require Import AST.
Require Import RTL.
Require Import Maps.
Require Import Registers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Op.

Require Import RTLPaths.
Require Import CountingSem.
Require Import Scope.
Require Import Counter.
Require Import DLib.
Require Import UtilBase.

Local Open Scope nat_scope.

Hint Immediate in_eq.
Hint Immediate in_cons.

Section FUNCTION.

  Variable f : function.
  Variable fsc : Scope.family f.
  Variable sp : val.
  Variable ge : genv.
  Variable rs0: regset.
  Variable m0 : mem.

  Notation root := f.(fn_entrypoint).
  Notation header := (Scope.header fsc).
  Notation scope := (Scope.scope fsc).
  Notation parent := (Scope.parent fsc).
  Notation inc_r_counter' := (inc_r_counter f fsc).
  Notation inc_r'_counter' := (inc_r'_counter f fsc).
  Notation exited_scope' := (exited_scopes fsc).

  Notation pcs := (map get_pc).

  Notation "a %pc" := (get_pc a) (at level 1).
  Notation "a %rs" := (get_rs a) (at level 1).
  Notation "a %m" := (get_mem a) (at level 1).
  Notation "a %cs" := (get_cs a) (at level 1).
  Notation "a %rcs" := (get_rcs a) (at level 1).

  Notation step' := (cstep ge f fsc sp).
  Notation Reach' := (Reach ge f fsc sp rs0 m0).
  Notation Trace' := (Trace ge f fsc sp rs0 m0).

  Lemma step_cs:
  forall s s'
    (STEP: step' s s'),
    s' %cs = inc_counter (s %pc) (s %cs).

Proof.

    intros.
    inv STEP; auto.
  Qed.

  Lemma step_rcs:
    forall s s'
      (STEP: step' s s'),
      s' %rcs = inc_r_counter' s %pc s' %pc s %rcs.

Proof.

    intros.
    inv STEP; auto.
  Qed.

  Lemma inc_counter_new : forall n n' cs,
    n=n' ->
    (inc_counter n cs) # n' = (cs # n') + 1.

Proof.

    unfold inc_counter; intros.
    subst; rewrite PMap.gss; auto.
  Qed.

  Lemma inc_counter_old : forall n n' cs,
    n<>n' ->
    (inc_counter n cs) # n' = (cs # n').

Proof.

    unfold inc_counter; intros.
    subst; rewrite PMap.gso; auto.
  Qed.

  Lemma reset_counters_inv_in:
    forall n l rcs,
      In n l ->
      (reset_counters l rcs) # n = 0.

Proof.

    unfold reset_counters; induction l; intuition.
    destruct (peq n a); subst; simpl.
    > rewrite PMap.gss; auto.
    > rewrite PMap.gso; auto.
      apply IHl.
      simpl in H; intuition.
  Qed.

  Lemma reset_counters_inv_out:
    forall n l rcs,
      ~ In n l ->
      (reset_counters l rcs) # n = rcs#n.

Proof.

    unfold reset_counters; induction l; intuition.
    destruct (peq n a); subst; simpl.
    > elim H; simpl; auto.
    > rewrite PMap.gso; auto.
  Qed.

  Lemma reset_counters_le:
    forall n l cs,
      (reset_counters l cs) # n <= cs # n.

Proof.

    intros.
    destruct (List.In_dec peq n l).
    rewrite reset_counters_inv_in; auto; omega.
    rewrite reset_counters_inv_out; auto; omega.
  Qed.

  Lemma inc_r_counter_in:
    forall n pc pc' rcs,
      In n (exited_scope' pc pc') ->
      (inc_r_counter' pc pc' rcs) # n = 0.

Proof.

    unfold inc_r_counter; intros.
    apply reset_counters_inv_in; auto.
  Qed.

  Lemma inc_r_counter_out:
    forall n pc pc' rcs,
      ~ In n (exited_scope' pc pc') ->
      (inc_r_counter' pc pc' rcs) # n = (inc_counter pc rcs) # n.

Proof.

    unfold inc_r_counter; intros.
    apply reset_counters_inv_out; auto.
  Qed.

  Lemma inc_r_counter_le:
    forall n pc pc' rcs,
      (inc_r_counter' pc pc' rcs) # n <= (inc_counter pc rcs) # n.

Proof.

    unfold inc_r_counter; intros.
    apply reset_counters_le; auto.
  Qed.

  Lemma In_exited_scope_intro: forall n pc pc',
    f_In n f ->
    pc ∈ (scope n) ->
    ~ pc' ∈ (scope n) ->
    In n (exited_scope' pc pc').

Proof.

    unfold exited_scopes; intros.
    rewrite in_flat_map.
    exists (scope n); split; auto.
    apply Scope.scope_in_elements.
    destruct Scope.In_dec; simpl; intuition.
    destruct Scope.In_dec; simpl; intuition.
  Qed.

Lemma step0_succ_node: forall s t a,
step ge f sp s t a -> succ_node f s%pc a %pc.

Proof.

  intros.
  inv H; econstructor; split; eauto; simpl; eauto.
  destruct b; eauto.
  eapply list_nth_z_in; eauto.
Qed.

Lemma step_succ_node: forall s a,
step' s a -> succ_node f s%pc a %pc.

Proof.

  intros.
  inv H; simpl in *.
  eapply step0_succ_node; eauto.
Qed.

  Lemma rcs_max_prefix'_out:
    forall tr s,
      Trace' (s :: tr) ->
      forall n,
         f_In n f ->
        ~ s%pc ∈ (scope n) ->
        s%rcs # n = 0.

Proof.

    induction tr; intros.
    inv H; simpl.
    apply init_counters_zero.
    inv H.
    exploit step_rcs; eauto; intros RCS.
    rewrite RCS.
    destruct (List.In_dec peq n (exited_scope' a%pc s%pc)).
    > rewrite inc_r_counter_in; auto.
    > rewrite inc_r_counter_out; auto.
      unfold inc_counter; rewrite PMap.gsspec; destruct peq.
      > elim n0; apply In_exited_scope_intro; auto.
        subst.
        apply Scope.in_scope; auto.
      > apply IHtr; auto.
        intro; elim n0.
        apply In_exited_scope_intro; auto.
  Qed.

Hint Resolve Scope.scope_in_elements.

Lemma in_last_exited_scope: forall n0 n n',
  In n0 (exited_scope' n n') ->
  exists sc,
    In sc (Scope.elements fsc) /\ n0 ∈ sc /\ n ∈ sc /\ ~ n' ∈ sc.

Proof.

  unfold exited_scopes; intros.
  rewrite in_flat_map in H.
  destruct H as (nn & N1 & N2).
  destruct Scope.In_dec; simpl in *.
  destruct Scope.In_dec; simpl in *.
  elim N2.
  econstructor; repeat split; eauto.
  elim N2.
Qed.

  Lemma rcs_header_strict_pos_in_scope:
      forall n tr s
      (In: f_In n f)
      (TR: Trace' (s :: tr)),
      s%pc ∈ (scope n) ->
      s%pc = header (scope n) \/ s%rcs # (header (scope n)) > 0.

Proof.

    induction tr; intros.
    > inv TR.
      unfold init_st in *; simpl in *.
      left.
      apply Scope.in_scope_root; auto.
    > inv TR.
      destruct (Scope.In_dec a%pc (scope n)).
      edestruct IHtr; eauto.
      > right.
        exploit step_rcs; eauto; intros Hr; rewrite Hr; clear Hr.
        rewrite inc_r_counter_out.
        > rewrite <-H0; rewrite inc_counter_new; auto; omega.
        > intro; edestruct in_last_exited_scope as [scp (S & S1 & S2 & S3)]; eauto.
          rewrite H0 in *.
          elim S3.
          apply in_scope_get_scope_trans with f fsc n; auto.
          apply in_scope_header_in_scope with f fsc; auto.
      > right.
        exploit step_rcs; eauto; intros Hr; rewrite Hr; clear Hr.
        rewrite inc_r_counter_out.
        > unfold inc_counter; rewrite PMap.gsspec; destruct peq; auto; omega.
        > intro; edestruct in_last_exited_scope as [scp (S & S1 & S2 & S3)]; eauto.
          elim S3.
          apply in_scope_get_scope_trans with f fsc n; auto.
          apply in_scope_header_in_scope with f fsc; auto.
      > exploit enter_in_scope_at_header_only1; eauto.
        apply step_succ_node; auto.
  Qed.

  Lemma cs_header_strict_pos_in_scope:
      forall n tr s
      (TR: Trace' (s :: tr)),
      s%pc ∈ (scope n) ->
      s%pc = header (scope n) \/ s%cs # (header (scope n)) > 0.

Proof.

Definition get_pc' (cs:cstate) : node := cs%pc.

  Lemma Trace_app:
    forall tr' tr s
      (TR: Trace' (tr' ++ s :: tr)),
      Trace' (s :: tr).

Proof.

    induction tr'; intuition.
    inv TR.
    symmetry in H1.
    apply app_eq_nil in H1. destruct H1; congruence.
    apply IHtr'. rewrite <- H0.
    auto.
  Qed.

Lemma step_f_In: forall s a,
step' s a -> UtilBase.f_In s%pc f.

Proof.

  intros.
  exploit step_succ_node; eauto.
  intros (x & X1 & X2).
  unfold UtilBase.f_In.
  congruence.
Qed.

Lemma Trace_split_rev_path: forall tr,
       Trace' tr ->
       forall (tr1 tr2 tr3: list cstate) (s1 s2:cstate),
       tr = tr3 ++ s2 :: tr2 ++ s1 :: tr1 ->
       rev_path f s2 %pc (map get_pc' (tr2 ++ s1 :: nil)) s1 %pc.

Proof.

    induction tr; intros; simpl.
    apply app_cons_not_nil in H0; intuition.
    inv H; simpl.
    destruct tr3; inv H0.
    apply app_cons_not_nil in H2; intuition.
    apply app_cons_not_nil in H2; intuition.
    unfold get_pc'.
    destruct tr3; destruct tr2; inv H0; simpl.
    econstructor; auto.
    econstructor.
    eapply step_f_In; eauto.
    apply step_succ_node; auto.
    econstructor; eauto.
    apply IHtr with tr1 nil; auto.
    apply step_succ_node; auto.
    rewrite H2 in *.
    exploit Trace_app; eauto; intros HT.
    inv HT.
    econstructor; eauto.
    econstructor.
    eapply step_f_In; eauto.
    apply step_succ_node; auto.
    econstructor; eauto.
    apply IHtr with tr1 (tr3++s2::nil); auto.
    rewrite H2; rewrite app_ass; auto.
    apply step_succ_node; auto.
    rewrite H2 in *.
    exploit Trace_app; eauto; intros HT.
    inv HT; auto.
  Qed.

  Hint Resolve succ_node_f_In step_succ_node.

  Lemma bound_rcs_aux:
      forall n (Hf:f_In n f), n <> header (scope n) ->
    forall tr s
      (TR: Trace' (s :: tr)),
        s%rcs # n < s%rcs # (header (scope n))
        \/
        s%rcs # n =0
        \/
        (s%rcs # n = s%rcs # (header (scope n)) /\
          exists tr1, exists s0, exists tr2,
            tr = tr1++s0::tr2 /\
            s0%pc = n /\
            (forall s', In s' tr1 -> ~ s'%pc = header (scope n))).

Proof.

    generalize Trace_split_rev_path; intros Tsrp.
    induction tr; intros.
    > inv TR.
      unfold init_st; simpl.
      rewrite init_counters_zero; auto.
    > inv TR.
      simpl in *.
      exploit step_rcs; eauto; intros HR; rewrite HR; clear HR.
      assert(
        (inc_r_counter' a %pc s %pc a %rcs) # n <= (inc_counter a%pc a%rcs) # n).
        unfold inc_r_counter.
        apply reset_counters_le.
      unfold inc_counter in H0.
      assert (O:forall x y:nat, x<=y -> x<y \/ x=y) by (intros; omega).
      assert (O1:forall x y:nat, x<y -> x+1<y \/ x+1=y) by (intros; omega).
      > unfold inc_r_counter.
        destruct (List.In_dec peq n (exited_scope' a %pc s %pc)).
        > rewrite reset_counters_inv_in; auto.
        > rewrite reset_counters_inv_out; auto.
          rewrite reset_counters_inv_out; auto.
          rewrite PMap.gsspec in H0; destruct peq.
          > subst; rewrite inc_counter_new; auto.
            rewrite inc_counter_old; auto.
            destruct (IHtr _ H2) as [IH | [IH | (IH1 & (tr1 & s0 & tr2 & IH2 & IH3 & IH4))]].
            > destruct (O1 _ _ IH); auto.
              right; right; split; auto.
              exists nil; econstructor; econstructor; split; simpl; eauto.
            > elim rcs_header_strict_pos_in_scope with a%pc tr a; auto.
              > intuition.
              > intros Hh.
                elim O1 with 0 ((a %rcs) # (header (scope a %pc))); try omega.
                > left; omega.
                > right; right; split; try omega.
                  exists nil; econstructor; econstructor; split; simpl; eauto.
                  eauto.
              > eauto.
                subst.
                assert (HR:=Tsrp _ H2 tr2 tr1 nil s0 a (refl_equal _)).
                rewrite IH3 in *.
                exploit Scope.cycle_at_not_header; eauto.
                intro.
                assert (length (map get_pc' (tr1++s0::nil)) = 0).
                  rewrite H1; auto.
                rewrite map_length in H3.
                rewrite app_length in H3.
                simpl in H3; omega.
                intros Hm.
                rewrite in_map_iff in Hm.
                destruct Hm as (ss & S1 & S2).
                rewrite in_app_iff in S2.
                destruct S2; unfold get_pc' in *.
                > eelim IH4; eauto.
                > simpl in H1; intuition try congruence.
      > rewrite inc_counter_old; auto.
        destruct (IHtr _ H2) as [IH | [IH | (IH1 & (tr1 & s0 & tr2 & IH2 & IH3 & IH4))]].
        > left; unfold inc_counter.
          rewrite PMap.gsspec; destruct peq; auto.
          > rewrite e in IH.
            apply lt_trans with (1:=IH).
            generalize ((a %rcs) # (a %pc) ).
            intros; omega.
            auto with arith.
        > unfold inc_counter.
          rewrite PMap.gsspec; destruct peq; auto.
          > left; rewrite IH1.
            rewrite e.
            generalize ((a %rcs) # (a %pc) ).
            intros; omega.
          > right; right; split; auto.
            exists (a::tr1); exists s0; exists tr2; split.
            > simpl; congruence.
            > split; auto.
            simpl; destruct 1; auto.
            subst; auto.
       > intro; eelim n0; clear n0.
         unfold exited_scopes in *; rewrite in_flat_map in *.
         destruct H1 as (sc & S1 & S2).
         destruct Scope.In_dec; try (elim S2; fail).
         destruct Scope.In_dec; try (elim S2; fail).
         simpl in *.
         exists sc; repeat split; auto.
         destruct Scope.In_dec; try (intuition; fail).
         destruct Scope.In_dec; try (intuition; fail).
         simpl.
         eapply in_scope_header_in_scope; eauto.
  Qed.

  Lemma trace_respects_header_rcs:
    forall tr s
      (TR: Trace' (s :: tr)),
      forall n,
        f_In n f ->
        s %rcs # n <= s %rcs # (header (scope n)).

Proof.

    intros.
    destruct (peq n (header (scope n))).
    > rewrite <- e; auto.
    > edestruct bound_rcs_aux as [T | [T | T]]; eauto; try omega.
  Qed.

  Lemma bound_cs_aux:
      forall n (Hf:f_In n f), n <> header (scope n) ->
    forall tr s
      (TR: Trace' (s :: tr)),
        s%cs # n < s%cs # (header (scope n))
        \/
        s%cs # n =0
        \/
        (s%cs # n = s%cs # (header (scope n)) /\
          exists tr1, exists s0, exists tr2,
            tr = tr1++s0::tr2 /\
            s0%pc = n /\
            (forall s', In s' tr1 -> ~ s'%pc = header (scope n))).

Proof.

    generalize Trace_split_rev_path; intros Tsrp.
    induction tr; intros.
    > inv TR.
      unfold init_st; simpl.
      rewrite init_counters_zero; auto.
    > inv TR.
      simpl in *.
      exploit step_cs; eauto; intros HR; rewrite HR; clear HR.
      assert (O:forall x y:nat, x<=y -> x<y \/ x=y) by (intros; omega).
      assert (O1:forall x y:nat, x<y -> x+1<y \/ x+1=y) by (intros; omega).
      destruct (peq n a%pc).
      > subst; rewrite inc_counter_new; auto.
        rewrite inc_counter_old; auto.
        destruct (IHtr _ H2) as [IH | [IH | (IH1 & (tr1 & s0 & tr2 & IH2 & IH3 & IH4))]].
        > destruct (O1 _ _ IH); auto.
          right; right; split; auto.
          exists nil; econstructor; econstructor; split; simpl; eauto.
        > elim cs_header_strict_pos_in_scope with a%pc tr a; auto.
          > intuition.
          > intros Hh.
            elim O1 with 0 ((a %cs) # (header (scope a %pc))); try omega.
            > left; omega.
            > right; right; split; try omega.
              exists nil; econstructor; econstructor; split; simpl; eauto.
        > subst.
           assert (HR:=Tsrp _ H2 tr2 tr1 nil s0 a (refl_equal _)).
           rewrite IH3 in *.
           exploit Scope.cycle_at_not_header; eauto.
           > intro.
             assert (length (map get_pc' (tr1++s0::nil)) = 0).
               rewrite H0; auto.
             rewrite map_length in H1.
             rewrite app_length in H1.
             simpl in H1; omega.
           > intros Hm.
             rewrite in_map_iff in Hm.
             destruct Hm as (ss & S1 & S2).
             rewrite in_app_iff in S2.
             destruct S2; unfold get_pc' in *.
             > eelim IH4; eauto.
             > simpl in H0; intuition try congruence.
      > rewrite inc_counter_old; auto.
        destruct (IHtr _ H2) as [IH | [IH | (IH1 & (tr1 & s0 & tr2 & IH2 & IH3 & IH4))]].
        > left; unfold inc_counter.
          rewrite PMap.gsspec; destruct peq.
          > rewrite e in IH.
            apply lt_trans with (1:=IH).
            generalize ((a %cs) # (a %pc) ).
            intros; omega.
            auto with arith.
        > unfold inc_counter.
          rewrite PMap.gsspec; destruct peq; auto.
      > unfold inc_counter.
        rewrite PMap.gsspec; destruct peq.
        > left.
          rewrite e in *.
          rewrite IH1.
          generalize (a%cs # (a%pc)); intros; omega.
        > right; right; split; auto.
          exists (a::tr1); exists s0; exists tr2; split; auto.
          > rewrite IH2; auto.
          > split; auto.
            simpl; destruct 1; eauto.
            subst; auto.
  Qed.

Lemma 2 in the paper: trace_respects_header_cs. It establishes the relation between the counters of the scope header and those of other vertices in the same scope.

  Lemma trace_respects_header_cs: (* Lemma 2 *)
    forall tr s
      (TR: Trace' (s :: tr)),
      forall n,
        f_In n f ->
        s %cs # n <= s %cs # (header (scope n)).

Proof.

    intros.
    destruct (peq n (header (scope n))).
    > rewrite <- e; auto.
    > edestruct bound_cs_aux as [T | [T | T]]; eauto; try omega.
  Qed.

End FUNCTION.