Module GlobalBounds_proof

Computation and correctness proof of global 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.
Require Import HeaderBounds.
Require Import LocalBounds.
Require Import GlobalBounds.

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 elements := (Scope.elements 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 Trace_split: forall n tr,
  Trace' tr ->
  exists tr0, exists trl, tr = flatten trl ++ tr0 /\
    (forall s', In s' tr0 -> s'%pc <> n) /\
    forall tr', In tr' trl ->
      exists sn, exists tr'', tr' = tr'' ++ sn :: nil /\ sn%pc = n /\
        (forall s', In s' tr'' -> s'%pc <> n).
Proof.
  induction tr; intros.
  > inv H.
  > inv H.
    set (s:=init_st f rs0 m0).
    destruct (peq s%pc n).
    > exists nil; exists ((s::nil)::nil); split; auto.
      split; intuition.
      simpl in H; intuition.
      econstructor; exists nil; split; eauto.
    > exists (s::nil); exists nil; split; auto.
      simpl; intuition.
      congruence.
  > edestruct IHtr as (tr & trl & S1 & S2 & S3); eauto.
    destruct (peq n a%pc).
    > exists tr; exists ((a::nil)::trl); intuition.
      > simpl; congruence.
      > simpl in H0; destruct H0; eauto.
        econstructor; exists nil; eauto.
    > destruct trl.
      > simpl in *.
        exists (a::s::tr0); exists nil; simpl in *; intuition.
        > simpl; congruence.
        > eelim S2; eauto.
          subst; auto.
        > eelim S2; eauto.
          subst; auto.
      > exists tr; exists ((a::l)::trl); split.
        > rewrite S1; auto.
        > intuition.
          simpl in H0; destruct H0; eauto.
          destruct (S3 l) as (sn & tr'' & T1 & T2 & T3); auto.
          subst; econstructor; exists (a::tr''); split; eauto.
          simpl; eauto.
          split; auto.
          simpl; destruct 1; eauto.
          subst; auto.
  Qed.

Open Scope nat_scope.

Lemma nil_not_eq_app_cons: forall A (x:A) l l',
  nil <> l ++ x :: l'.
Proof.
  red; intros.
  assert (length (l++x::l') = 0).
    rewrite <- H; auto.
  generalize H0.
  rewrite app_length.
  simpl; intros.
  omega.
Qed.

Section parent.
  Variable n : node.
  Variable n_f_In: f_In n f.
  Variable not_root: header (scope n) <> root.
  Let is_header (n:node) := n = header (scope n).
  Variable n_is_header: is_header n.
  Let p := header (parent (scope n)).

  Hypothesis parent_not_in_scope: ~ p ∈ (scope n).

  Variable M: nat.

  Hypothesis rcs_c_bound_by_M:
    forall s tr, Trace' (s::tr) -> s %rcs # n <= M.
  Hypothesis rcs_c_bound_by_M':
    forall s tr, Trace' (s::tr) -> s %rcs # n = M -> s%pc <> n.
  Hypothesis M_strict_pos: M>0.

  Lemma rcs_max_prefix'_out:
    forall tr s,
      Trace' (s :: tr) ->
        ~ s%pc ∈ (scope n) ->
        s%rcs # n = 0.
Proof.
    induction tr; intros.
    > inv H.
      unfold init_st; simpl.
      apply init_counters_zero; auto.
    > inv H.
      exploit step_rcs; eauto; intros R; rewrite R; clear R.
      destruct (List.In_dec peq n (exited_scopes fsc a%pc s%pc)).
      > rewrite inc_r_counter_in; auto.
      > rewrite inc_r_counter_out; auto.
        destruct (In_dec a%pc (scope n)).
        > destruct n0.
          apply In_exited_scope_intro; auto.
        > rewrite inc_counter_old; auto.
          intro; destruct n1.
          rewrite <- H; apply Scope.in_scope; congruence.
  Qed.

  Lemma succ_not_in_last_exited_scope: forall n0 n n',
    n ∈ (scope n0) ->
    n' ∈ (scope n0) ->
    ~ In n0 (exited_scope' n n').
Proof.
    unfold exited_scopes; intros.
    rewrite in_flat_map.
    intros (sc & S1 & S2).
    destruct In_dec; simpl in S2; try (intuition; fail).
    destruct In_dec; simpl in S2; try (intuition; fail).
    destruct n2.
    eapply Scope.scope_least; eauto.
  Qed.

Hint Resolve step_succ_node Scope.in_scope Scope.scope_in_elements.

  Lemma in_scope_after_header: forall (tr1:list cstate) (a sp:cstate) tr2,
    ~ sp%pc ∈ (scope n) ->
    Trace' (a :: tr1 ++ sp :: tr2) ->
    a %pc ∈ (scope n) ->
    exists s', In s' (a::tr1) /\ s'%pc = n.
Proof.
    induction tr1; simpl; intros.
    > inv H0.
      assert (a%pc = header (scope n)).
      > apply enter_in_scope_at_header_only1 with sp0%pc; eauto.
      exists a; split; auto; congruence.
    > inv H0.
      destruct (In_dec a%pc (scope n)).
      > exploit IHtr1; eauto; intros (s' & S1 & S2).
        simpl in S1; intuition eauto.
      > assert (a0%pc = header (scope n)).
        > apply enter_in_scope_at_header_only1 with a%pc; eauto.
        exists a0; split; auto; congruence.
  Qed.

  Lemma In_tr: forall (s:cstate) tr,
    In s tr -> exists tr1, exists tr2, tr = tr1 ++ s :: tr2.
Proof.
    induction tr; simpl; intuition.
    subst; exists nil; simpl; eauto.
    destruct H as (tr1 & tr2 & T); exists (a::tr1); subst; simpl; eauto.
  Qed.

  Lemma diff_cs_and_M: forall (sp:cstate) (tr2: list cstate),
    sp%pc = p -> forall tr1 s,
    Trace' (s::tr1++sp::tr2) ->
    (forall s', In s' tr1 -> s'%pc <> p) ->
      (s %cs # n = sp %cs # n /\ (forall s', In s' tr1 -> s'%pc <> n) /\ s %rcs #n = 0)
      \/
      (s %cs # n = s %rcs #n + sp %cs # n /\ s%pc ∈ (scope n))
      \/
      (exists k, s %cs # n = k + sp %cs # n /\ k <= M /\
        exists sn, In sn tr1 /\ sn%pc =n /\ ~ s%pc ∈ (scope n)).
Proof.
    induction tr1; simpl; intros.
    > left; intuition.
      > inv H0.
        exploit step_cs; eauto; intros HS; rewrite HS; clear HS.
        unfold inc_counter; rewrite PMap.gsspec; destruct peq.
        > eelim parent_not_in_scope.
          rewrite <- H.
          subst; apply Scope.in_scope; eauto.
        > reflexivity.
      > inv H0.
        exploit step_rcs; eauto; intros HS; rewrite HS; clear HS.
        unfold inc_r_counter.
        assert (O:forall x y, x <= y -> y = 0 -> x = 0) by (intros; omega).
        eapply O.
        eapply reset_counters_le.
        unfold inc_counter; rewrite PMap.gsspec; destruct peq.
        > eelim parent_not_in_scope.
          rewrite <- H; subst.
          apply Scope.in_scope; eauto.
        > eapply rcs_max_prefix'_out; eauto.
          rewrite H; auto.
    > inv H0.
      exploit IHtr1; eauto; intros IHtr; clear IHtr1.
      exploit step_cs; eauto; intros HS; rewrite HS; clear HS.
      unfold inc_counter; rewrite PMap.gsspec; destruct peq.
      > right.
        destruct IHtr as [IH | [IH | IH]].
        > destruct IH as (IH1 & IH2 & IH3).
          subst; rewrite IH1.
          destruct (In_dec (s%pc) (scope a%pc)).
          > left; split; auto.
            replace (s%rcs#(a%pc)) with 1; try omega.
            exploit step_rcs; eauto; intros HS; rewrite HS; clear HS.
            unfold inc_r_counter.
            rewrite reset_counters_inv_out.
            > rewrite inc_counter_new; auto; omega.
            > apply succ_not_in_last_exited_scope; auto.
          > right; exists 1; split; try omega.
            split; try omega.
            exists a; auto.
        > destruct IH as (IH1 & IH2).
          subst; rewrite IH1.
          destruct (In_dec (s%pc) (scope a%pc)).
          > left; split; auto.
            replace (s%rcs#(a%pc)) with (a%rcs#(a%pc)+1); try omega.
            exploit step_rcs; eauto; intros HS; rewrite HS; clear HS.
            unfold inc_r_counter.
            rewrite reset_counters_inv_out.
            > rewrite inc_counter_new; auto; omega.
            > apply succ_not_in_last_exited_scope; auto.
          > assert ((a %rcs) # (a %pc) <= M) by eauto with datatypes.
            assert (((a %rcs) # (a %pc) < M)\/((a %rcs) # (a %pc) = M)) by omega.
            destruct H2.
            > right; exists (a%rcs#(a%pc)+1); split; try omega.
              split; try omega.
              eauto.
            > elim rcs_c_bound_by_M' with (1:=H4) (s:=a); auto.
        > destruct IH as (k & IH1 & IH2 & sn & IH3 & IH4 & IH5).
          elim IH5; try congruence.
          rewrite <- e; apply Scope.in_scope; eauto.
      > destruct IHtr as [IH | [IH | IH]].
        > destruct IH as (IH1 & IH2 & IH3).
          subst; rewrite IH1.
          left; split; auto.
          split.
          > destruct 1; auto; congruence.
          > exploit step_rcs; eauto; intros HS; rewrite HS; clear HS.
            unfold inc_r_counter.
            assert (O:forall x y, x <= y -> y = 0 -> x = 0) by (intros; omega).
            eapply O.
            eapply reset_counters_le.
            rewrite inc_counter_old; auto.
        > destruct IH as (IH1 & IH2).
          subst; rewrite IH1.
          destruct (In_dec (s%pc) (scope n)).
          > right; left; split; auto.
            replace (s%rcs#n) with (a%rcs#n); try omega.
            exploit step_rcs; eauto; intros HS; rewrite HS; clear HS.
            unfold inc_r_counter.
            rewrite reset_counters_inv_out.
            > rewrite inc_counter_old; auto.
            > apply succ_not_in_last_exited_scope; auto.
          > assert (exists sn, In sn tr1 /\ sn%pc=n).
              elim in_scope_after_header with (2:=H4); eauto.
              simpl; destruct 1.
              destruct H0; subst; eauto; intuition.
              rewrite H; auto.
            destruct H0 as (sn & S1 & S2).
            > right; right; exists (a%rcs#n); split; try omega.
              split; try omega.
              > exploit rcs_c_bound_by_M; eauto.
              > eauto.
        > destruct IH as (k & IH1 & IH2 & sn & IH3 & IH4 & IH5).
          right; right.
          exists k; split; auto.
          split; try omega.
          exists sn; split; auto.
          split; auto.
          intro.
          assert (s%pc = header (scope n)).
          > apply enter_in_scope_at_header_only1 with a%pc; eauto.
          elim In_tr with (1:=IH3); intros tr1' (tr2' & T); subst.
          assert (Trace' (nil ++ s :: (a::tr1') ++ sn :: (tr2' ++ sp0 :: tr2))).
          > rewrite app_ass in H4; simpl in *; econstructor; eauto.
          exploit Trace_split_rev_path; eauto.
          simpl; rewrite map_app; simpl.
          unfold get_pc'; intros.
          assert (sn%pc = s%pc) by congruence.
          rewrite H7 in *.
          edestruct Scope.cycle_at_header with (3:=H5); eauto.
          congruence.
          simpl in H8; destruct H8.
          > eelim H1; eauto.
          > rewrite in_app in H8; destruct H8; eauto.
            > rewrite in_map_iff in H8.
              destruct H8 as (st & S1 & S2).
              elim (H1 st); eauto with datatypes.
            > simpl in H8; intuition.
              elim (H1 sn); eauto with datatypes.
              congruence.
  Qed.

  Lemma diff_cs_and_M_final: forall (sp:cstate) tr2,
    sp%pc = p -> forall tr1 s,
    Trace' (s::tr1++sp::tr2) ->
    (forall s', In s' tr1 -> s'%pc <> p) ->
      exists k, s %cs # n = k + sp %cs # n /\ k <= M.
Proof.
    intros; exploit diff_cs_and_M; eauto.
    destruct 1 as [I | [I | I]].
    > destruct I as (I1 & I2).
      exists O; split; omega.
    > destruct I as (I1 & I2).
      econstructor; split; eauto.
      exploit rcs_c_bound_by_M; eauto.
    > destruct I as (k & I1 & I2 & sn & I3 & I4 & I5).
      exists k; omega.
  Qed.

Lemma Trace_sc_zero: forall n tr s,
  Trace' (s::tr) ->
  (forall s', In s' tr -> s'%pc <> n) ->
  s%cs # n = 0.
Proof.
  induction tr; simpl; intros.
  > inv H.
    unfold init_st; simpl.
    rewrite init_counters_zero; auto.
  > inv H.
    exploit step_cs; eauto; intros R; rewrite R.
    rewrite inc_counter_old; auto.
Qed.

Lemma Trace_sc_same: forall s0 tr2 n tr1 s,
  Trace' (s::tr1++s0::tr2) ->
  (forall s', In s' tr1 -> s'%pc <> n) ->
  forall s', In s' tr1 -> s%cs # n = s'%cs # n.
Proof.
  induction tr1; simpl; intros.
  > intuition.
  > inv H.
    exploit step_cs; eauto; intros R; rewrite R.
    destruct H1.
    > subst.
      rewrite inc_counter_old; auto.
    > rewrite inc_counter_old; auto.
Qed.

Lemma header_dominates: forall n tr0 s,
  f_In n f ->
  Trace' (s::tr0) ->
  s%pc ∈ (scope n) ->
  header (scope n) = root \/
  exists s0, In s0 (s::tr0) /\ header (scope n) = s0%pc.
Proof.
  induction tr0; simpl; intuition.
   > inv H0.
     unfold init_st in *; simpl in *.
     exploit Scope.in_scope_root; eauto.
   > inv H0.
     destruct (In_dec a%pc (scope n0)).
     > exploit IHtr0; eauto.
       destruct 1; eauto.
       destruct H0 as (s0 & S1 & S2); eauto.
     > right; exists s; split; auto.
       symmetry.
       apply enter_in_scope_at_header_only1 with a%pc; eauto.
Qed.

Lemma header_dominates2: forall n tr0 s s1,
  f_In n f ->
  Trace' (s1::tr0) -> In s tr0 ->
  s%pc ∈ (scope n) ->
  header (scope n) = root \/
  exists s0, In s0 (tr0) /\ header (scope n) = s0%pc.
Proof.
  induction tr0; simpl; intuition.
   > inv H0.
     exploit header_dominates; eauto.
   > inv H0.
     exploit IHtr0; eauto.
     destruct 1; eauto.
     destruct H0 as (s0 & S1 & S2); eauto.
Qed.

Lemma parent_dominates_aux: forall n tr0 s,
  f_In n f ->
  Trace' (s::tr0) ->
  s%pc ∈ (scope n) ->
  header (scope n) = root \/
  exists s0, In s0 tr0 /\ parent (scope n) = scope s0%pc /\ f_In s0%pc f.
Proof.
  induction tr0; simpl; intuition.
   > inv H0.
     unfold init_st in *; simpl in *.
     exploit Scope.in_scope_root; eauto.
   > inv H0.
     destruct (In_dec a%pc (scope n0)).
     > exploit IHtr0; eauto.
       destruct 1; eauto.
       destruct H0 as (s0 & S1 & S2); eauto.
     > right; exists a; split; auto.
     assert (s%pc = header (scope n0)).
       eapply enter_in_scope_at_header_only1; eauto.
     elim Scope.enter_in_scope_at_header_only with f fsc a%pc s%pc; eauto.
     > intros.
       assert (scope n0 = scope s%pc).
         rewrite H0.
         rewrite Scope.scope_header; auto.
       split; try congruence.
       eapply step_f_In; eauto.
     > rewrite H0; rewrite Scope.scope_header ; auto.
Qed.

Lemma init_st_in_Trace: forall tr,
  Trace' tr -> exists s0, In s0 tr /\ s0%pc = root.
Proof.
  induction tr; intros.
  > inv H.
  > inv H.
    > econstructor; simpl; split; eauto.
    > destruct IHtr as (s1 & S1 & S2); auto.
      econstructor; split.
      right; eauto.
      auto.
Qed.

Lemma parent_dominates: forall tr0 s,
  Trace' (s::tr0) ->
  (forall s', In s' tr0 -> s'%pc <> p) ->
  (forall s', In s' tr0 -> ~ s'%pc ∈ (scope n)).
Proof.
  induction tr0; simpl; intuition.
  > subst.
    inv H.
    exploit parent_dominates_aux; eauto.
    destruct 1; auto.
    destruct H as (s0 & S1 & S2 & S3).
    exploit (header_dominates2 s0%pc); eauto.
    destruct 1.
    > assert (p=root) by (unfold p in *; congruence).
      elim init_st_in_Trace with (1:=H4); intros ss0 (SS1 & SS2).
      elim H0 with ss0; auto.
      congruence.
    > destruct H as (s1 & S5 & S4).
      elim H0 with s1; eauto.
      unfold p in *; congruence.
  > inv H; exploit IHtr0; eauto.
Qed.

Lemma global_bound_almost: forall tr0 trl s,
  Trace' (s::flatten trl ++ tr0) ->
  (forall s', In s' tr0 -> s'%pc <> p) ->
  (forall tr', In tr' trl ->
      exists sn, exists tr'', tr' = tr'' ++ sn :: nil /\ sn%pc = p /\
        (forall s', In s' tr'' -> s'%pc <> p)) ->
      s%cs # n <= (length trl) * M.
Proof.
  induction trl; simpl; intros.
  > assert (forall s', In s' tr0 -> s'%pc <>n).
      red; intros.
      eelim parent_dominates with (1:=H); eauto.
      rewrite H3; auto.
    erewrite Trace_sc_zero; eauto.
  > edestruct (H1 a) as (sn & tr'' & T1 & T2 & T3); eauto.
    subst a.
    assert (Trace' (sn::flatten trl ++ tr0)).
      generalize H.
      repeat (rewrite app_ass; simpl); intros.
      apply Trace_app with (s::tr''); auto.
    exploit IHtrl; eauto; intros IH; clear IHtrl H2.
    rewrite (app_ass tr'') in H.
    simpl in H.
    rewrite app_ass in H.
    simpl in H.
    edestruct diff_cs_and_M_final as (k & K1 & K2); eauto.
    omega.
Qed.

Lemma app_cons_case: forall A (l:list A),
  l = nil \/ exists x, exists q, l = q ++ x :: nil.
Proof.
  induction l; simpl; auto.
  right; destruct IHl.
  > subst l; econstructor; exists nil; simpl; eauto.
  > destruct H as (x & q & H1).
    exists x; exists (a::q); simpl; congruence.
Qed.

Lemma cs_parent_length: forall tr0 trl s,
  Trace' (s::flatten trl ++ tr0) ->
  (forall s', In s' tr0 -> s'%pc <> p) ->
  (forall tr', In tr' trl ->
      exists sn, exists tr'', tr' = tr'' ++ sn :: nil /\ sn%pc = p /\
        (forall s', In s' tr'' -> s'%pc <> p)) ->
      s%cs # p = length trl.
Proof.
  induction trl; simpl; intros.
  > erewrite Trace_sc_zero; eauto.
  > edestruct (H1 a) as (sn & tr'' & T1 & T2 & T3); eauto.
    subst a.
    assert (Trace' (sn::flatten trl ++ tr0)).
    > generalize H.
      repeat (rewrite app_ass; simpl); intros.
      apply Trace_app with (s::tr''); auto.
    exploit IHtrl; eauto; intros IH; clear IHtrl H2.
    rewrite (app_ass tr'') in H.
    simpl in H.
    rewrite app_ass in H.
    simpl in H.
    destruct (app_cons_case _ tr'') as [Ha |(x & q & Ha)].
    > subst tr''.
      inv H.
      rewrite <- T2.
      exploit step_cs; eauto; intros R; rewrite R; clear R.
      rewrite inc_counter_new; auto.
      rewrite T2; omega.
    > subst tr''.
      exploit Trace_sc_same; eauto with datatypes.
      intros HH.
      assert (Trace' (x :: sn::flatten trl ++ tr0)).
      > generalize H.
        repeat (rewrite app_ass; simpl); intros.
        apply Trace_app with (s::q); auto.
      assert (step' sn x).
      > inv H2; auto.
      rewrite HH.
      exploit step_cs; eauto; intros R; rewrite R; clear R.
      rewrite T2.
      rewrite inc_counter_new; auto.
      omega.
Qed.

Lemma 3 in the paper: global_bound. It relates local and global bounds for a given scope header.

Lemma global_bound: (* Lemma 3 *)
  forall tr s,
  Trace' (s::tr) ->
  s%cs # n <= s %cs # p * M.
Proof.
  intros.
  inv H.
  > unfold init_st; simpl.
    repeat rewrite init_counters_zero; omega.
  > exploit (Trace_split p); eauto.
    intros (tr & trl & T1 & T2 & T3).
    assert (Trace' (s :: s0 :: tr0)) by (econstructor; eauto).
    rewrite T1 in *.
    exploit cs_parent_length; eauto; intros HL.
    exploit global_bound_almost; eauto.
    rewrite <- HL; auto.
Qed.

End parent.

End FUNCTION.

Require Import String.
Require Import Maps.
Require Import RTLWfFunction.
Require Import Sliceproof.
Require Import SliceCFG.
Require Import SliceGen.
Require Import WCETSlice.
Open Scope Z_scope.

Section BOUND_CORRECT.
Variable f: function.
Variable fsc: Scope.family f.
Variable exit_n : node.
Variable reg_vint : reg.
Hypothesis WFF: check_wf f = OK (exit_n, reg_vint).

Lemma fold_bound_rec_error: forall A B g l e,
    @fold_left (res B) A
          (fun eacc sc' => do acc <- eacc; g sc' acc)
          l
          (Error e) = Error e.
Proof.
  induction l; simpl; intros; auto.
Qed.

Lemma bound_rec_acc: forall fuel sc bmap bmap',
  bound_rec f fsc exit_n reg_vint fuel sc bmap = OK bmap' ->
  forall n b, bmap!n = Some b -> bmap'!n = Some b.
Proof.
  induction fuel; simpl; try congruence.
  intros sc bmap bmap'.
  case_eq (ptree_mem (Scope.header fsc sc) bmap); intros Hb Heq; try congruence.
  destruct peq.
  intros.
  assert (forall l bmap bmap',
    fold_left
          (fun eacc sc' => do acc <- eacc; bound_rec f fsc exit_n reg_vint fuel sc' acc)
          l
          (OK bmap) = OK bmap' ->
          forall n b, bmap!n = Some b -> bmap'!n = Some b).
    induction l; simpl; intros.
    > inv H0. auto.
    > case_eq (bound_rec f fsc exit_n reg_vint fuel a bmap0); intros.
      > rewrite H2 in H0.
        apply (IHl _ _ H0).
        eapply IHfuel; eauto.
      > revert H0.
        rewrite H2.
        rewrite (fold_bound_rec_error _ _ (bound_rec f fsc exit_n reg_vint fuel)); congruence.
  generalize (H0 _ _ _ Heq); clear H0 Heq; intros Heq.
  apply Heq.
  rewrite PTree.gsspec; destruct peq; eauto.
  revert Hb; unfold ptree_mem.
  rewrite <- e0; rewrite H; congruence.
  monadInv Heq.
  destruct x as (tf & tfsc & FOK).
  assert (forall l bmap bmap',
    fold_left
          (fun eacc sc' => do acc <- eacc; bound_rec f fsc exit_n reg_vint fuel sc' acc)
          l
          (OK bmap) = OK bmap' ->
          forall n b, bmap!n = Some b -> bmap'!n = Some b).
    induction l; simpl; intros.
    > inv H. auto.
    > case_eq (bound_rec f fsc exit_n reg_vint fuel a bmap0); intros.
      > rewrite H1 in H.
        apply (IHl _ _ H).
        eapply IHfuel; eauto.
      > revert H.
        rewrite H1.
        rewrite (fold_bound_rec_error _ _ (bound_rec f fsc exit_n reg_vint fuel)); congruence.
  case_eq (local_bound tf tfsc (Scope.header fsc sc)); [intros lbound Hl|intros er Hl];
    rewrite Hl in EQ0.
  monadInv EQ0.
  revert EQ1.
  case_eq (bmap ! (Scope.header fsc (Scope.parent fsc sc))); simpl; intros; try congruence.
  inv EQ1.
  generalize (H _ _ _ EQ2); clear H EQ2; intros EQ2.
  apply EQ2.
  rewrite PTree.gsspec; destruct peq; eauto.
  revert Hb; unfold ptree_mem.
  rewrite <- e; rewrite H1; congruence.

  inv EQ0; auto.
Qed.

Definition correct_bound (n:node) (b:Z) : Prop :=
  (forall ge sp tr rs m s, f_In n f ->
    Reaches_final ge f fsc sp rs m ->
    Trace ge f fsc sp rs m (s::tr) -> (Z_of_nat (get_cs s) # n) <= b) /\ b > 0.

Theorem local_bound_pos : forall f (fsc:Scope.family f) n bound,
  local_bound f fsc n = OK bound -> bound > 0.
Proof.
  unfold local_bound; intros.
  destruct positive_eq_dec.
  > inv H; omega.
  > monadInv H.
   destruct check_may_not_update_mem; destruct check_all_only_special_builtins; simpl in EQ0; try congruence.
    generalize prod_doms_pos; unfold prod_doms_aux; intros T.
    apply T with (1:=EQ0).
    omega.
Qed.

Lemma cs_root: forall ge sp rs m s,
    Reach ge f fsc sp rs m s ->
    Z_of_nat ((get_cs s) # (f.(fn_entrypoint))) <= 1.
Proof.
  induction 1.
  > simpl; rewrite init_counters_zero; simpl; omega.
  > exploit step_cs; eauto; intros R; rewrite R; clear R.
    replace 1 with (Z_of_nat 1%nat) in *; auto.
    apply inj_le.
    rewrite <- inj_le_iff in IHReach.
    inv H.
    > simpl.
      rewrite inc_counter_new; auto.
      rewrite init_counters_zero; simpl; omega.
    > rewrite inc_counter_old; auto.
      intro; elim Scope.root_no_pred with f (get_pc s0); auto.
      rewrite <- H.
      eapply step_succ_node; eauto.
Qed.

Lemma bound_rec_correct: forall fuel sc bmap bmap',
  bound_rec f fsc exit_n reg_vint fuel sc bmap = OK bmap' ->
  In sc (Scope.elements fsc) ->
  (forall n b, bmap!n = Some b -> correct_bound n b) ->
  (forall n b, bmap'!n = Some b -> correct_bound n b).
Proof.
  induction fuel; simpl; try congruence.
  intros sc bmap bmap'.
  case_eq (ptree_mem (Scope.header fsc sc) bmap); intros Hb Heq; try congruence.
  assert (forall l bmap bmap',
    (forall sc', In sc' l -> In sc' (Scope.elements fsc)) ->
    (True) ->
    fold_left
          (fun eacc sc' => do acc <- eacc; bound_rec f fsc exit_n reg_vint fuel sc' acc)
          l
          (OK bmap) = OK bmap' ->
    (forall n b, bmap!n = Some b -> correct_bound n b) ->
    (forall n b, bmap'!n = Some b -> correct_bound n b)).
    induction l; simpl; intros.
    > inv H1; eauto.
    > case_eq (bound_rec f fsc exit_n reg_vint fuel a bmap0); intros; rewrite H4 in H1.
      > eapply IHl; eauto.
        eapply IHfuel with (sc:=a); eauto.
      > revert H1.
        rewrite (fold_bound_rec_error _ _ (bound_rec f fsc exit_n reg_vint fuel)); congruence.
  destruct peq.
  > intros; apply H with (3:=Heq); eauto.
    > intros; eapply Scope.sons_in_element; eauto.
    > intros n1 b0.
      rewrite PTree.gsspec; destruct peq; intros; eauto.
      inv H3.
      split; intros; try omega.
      exploit in_Trace_Reach; eauto; intros.
      rewrite e; eapply cs_root; eauto.
  > monadInv Heq.
    destruct x as (tf & tfsc & of & FOK & Hok); clear EQ.
    case_eq (local_bound tf tfsc (Scope.header fsc sc)); [intros lbound Hlb|intros er Hlb];
      rewrite Hlb in EQ0.
    monadInv EQ0.
    revert EQ1.
    case_eq (bmap ! (Scope.header fsc (Scope.parent fsc sc))); simpl; intros; try congruence.
    rename z into p_bound.
    rewrite H0 in EQ.
    inv EQ.
    rename x into p_bound.
    apply H with (3:=EQ1); eauto.
    > intros; eapply Scope.sons_in_element; eauto.
    > intros n1 b0.
      rewrite PTree.gsspec; destruct peq; intros; eauto.
      inv H4.
      assert (HBp:p_bound > 0).
        destruct (H2 _ _ H0); omega.
      assert (HBl:lbound > 0).
        exploit local_bound_pos; eauto; omega.
      split.
      > intros ge sp tr rs m s Hf Ht.
        exploit local_bound_pos; eauto; intros.
        rewrite <- (nat_of_Z_eq lbound) in H4; try omega.
        replace 0 with (Z_of_nat 0%nat) in H4; auto.
        rewrite <- inj_gt_iff in H4.
        exploit in_Trace_Reach; eauto; intros R.
        assert
          (Htf:forall s : cstate,
            Reach ge tf (SliceCFG.transf_family FOK) sp rs m s ->
            ((get_rcs s) # (Scope.header fsc sc) <= nat_of_Z lbound)%nat /\
            ((get_rcs s) # (Scope.header fsc sc) = nat_of_Z lbound ->
              get_pc s <> Scope.header fsc sc)).
        intros ss HR.
        eelim (local_bound_correct tf (SliceCFG.transf_family FOK) ge sp rs m (Scope.header (SliceCFG.transf_family FOK) sc)); eauto.
        > intros B1 B2.
          rewrite <- (nat_of_Z_eq lbound) in B2.
          rewrite <- (nat_of_Z_eq lbound) in B1.
          rewrite <- inj_le_iff in *; auto.
          > omega.
          > omega.
          > eapply transf_f_In'; eauto.
          > erewrite transf_entry; eauto.
            rewrite Scope.scope_header; auto.
            intro; destruct n.
            symmetry.
            eapply Scope.in_scope_root; eauto.
            eapply slicing_preserves_termination; eauto.
            intros; eapply local_bound_no_builtin; eauto.
            erewrite transf_entry; eauto.
        assert (HSlice:=program_slicing_is_sound_stronger_version
                ge sp f rs m fsc tf _ _ WFF _ _ FOK (nat_of_Z lbound) Htf); clear Htf. exploit global_bound; eauto.
        > rewrite Scope.scope_header; auto.
        > rewrite Scope.scope_header; auto.
        > rewrite Scope.scope_header; auto.
          intro; destruct n.
          exploit Scope.parent_strict_subset; eauto.
        > intros.
          exploit in_Trace_Reach; eauto; intros.
          eelim HSlice; eauto; clear HSlice.
        > intros.
          exploit in_Trace_Reach; eauto; intros.
          eelim HSlice; eauto; clear HSlice.
          > intros B.
            assert (p_bound >= 0).
              destruct (H2 _ _ H0); omega.
            rewrite <- (nat_of_Z_eq p_bound H6) in *.
            assert (lbound >= 0).
              exploit local_bound_pos; eauto; omega.
            rewrite <- (nat_of_Z_eq lbound H7) in *.
            rewrite <- inj_mult.
            rewrite mult_comm.
            apply inj_le.
            apply le_trans with (1:=B).
            rewrite nat_of_Z_eq; auto.
            apply mult_le_compat_r; auto.
          > rewrite Scope.scope_header; auto.
            rewrite inj_le_iff.
            destruct (H2 _ _ H0).
            eapply H8; eauto.
            apply Scope.header_f_In; eauto.
            apply Scope.parent_in_element; auto.

        > auto with zarith.

  rewrite H0 in EQ; inv EQ.
  inv EQ0; auto.
Qed.

End BOUND_CORRECT.

Theorem 1 in the paper: bound_correct. It states the correctness of the method with respect to the instrumented RTL semantics.

Theorem bound_correct: (* Theorem 1 *)
  forall f bmap,
  bound f = OK bmap ->
  exists fsc,
  forall ge sp rs m, Reaches_final ge f fsc sp rs m ->
    forall s, Reach ge f fsc sp rs m s ->
      forall n, f_In n f ->
        forall b, bmap n = Some b ->
          (Z_of_nat (get_cs s) # n) <= b.
Proof.
  unfold bound; intros.
  case_eq (Scope.build_family f); [intros fsc' Hf|intros Hf]; rewrite Hf in H;
    try congruence.
  monadInv H.
  exists fsc'; intros.
  exploit bound_rec_correct; eauto.
  > apply Scope.scope_in_elements.
  > intros n0 b0; rewrite PTree.gempty; congruence.
  > destruct 1.
    exploit Reach_ex_Trace; eauto.
    intros (tr & T).
    assert (Z_of_nat (get_cs s) # (Scope.header fsc' (Scope.scope fsc' n)) <= b).
      eapply H3; eauto.
      apply Scope.header_f_In.
      apply Scope.scope_in_elements.
    apply Zle_trans with (2:=H5).
    apply inj_le.
    eapply trace_respects_header_cs; eauto.
Qed.

Generated by coq2html