Module LocalBounds

Computation and correctness proof of local 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 UtilTacs.
Require Import UtilLemmas.
Require Import HeaderBounds.
Require Import ValueAnalysis.
Require Import LightLive.

Local Open Scope nat_scope.

Definition itv_length (itv : interval) :=
  (itv_max itv - itv_min itv + 1)%Z.

Definition prod_doms_aux f z0 (n : node) (xs : list reg) : res Z :=
  fold_left (fun rprod0 x =>
    do prod0 <- rprod0;
      do itv <- value f n x;
          let res := ((itv_length itv) * prod0)%Z in
            OK res
  ) xs (OK z0).

Definition prod_doms (f:function) : node -> list reg -> res Z := prod_doms_aux f 1.


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 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).

  Inductive may_update_mem : node -> Prop :=
  | MUM_builtin: forall pc ef args dst s,
    (fn_code f) !pc = Some (Ibuiltin ef args dst s) ->
    (forall id ty, ef <> EF_annot id ty) ->
    (forall id ty, ef <> EF_annot_val id ty) ->
    may_update_mem pc
  | MUM_store: forall pc chk adr args src s,
    (fn_code f) !pc = Some (Istore chk adr args src s) ->
    may_update_mem pc
  | MUM_call: forall pc sig r args dst s,
    (fn_code f) !pc = Some (Icall sig r args dst s) ->
    may_update_mem pc
  | MUM_tailcall: forall pc sig r args,
    (fn_code f) !pc = Some (Itailcall sig r args) ->
    may_update_mem pc.

  Inductive contains_misc_builtins : node -> Prop :=
  | HS: forall pc ef args dst s,
    (fn_code f) ! pc = Some (Ibuiltin ef args dst s) ->
    (forall sz al, ef <> EF_memcpy sz al) ->
    (forall id ty, ef <> EF_annot id ty) ->
    (forall id ty, ef <> EF_annot_val id ty) ->
    contains_misc_builtins pc.

  Hint Constructors use: use_hints.



  Inductive DTrace : list cstate -> Prop :=
  | DT_init : forall s, DTrace (s::nil)
  | DT_cons : forall s s' tr, DTrace (s :: tr) -> step' s s' -> DTrace (s' :: s :: tr).


     Lemma DTrace_app_left: forall tr1 s tr2,
       DTrace (s::tr1++tr2) -> DTrace (s::tr1).
Proof.
       induction tr1; simpl; try constructor.
       inv H; eauto.
       inv H; auto.
     Qed.

  Hint Constructors Live.


  Section STATE_COND_EQ.

    Variable loop : Scope.t.

    Definition state_cond_eq (s s' : cstate) : Prop :=
      s%pc ∈ loop /\
      s%pc = s'%pc /\
      s%m = s'%m /\
      let (rs, rs') := (get_rs s, get_rs s') in
        forall v pc', pc' ∈ loop -> use f pc' v -> Live f s%pc v -> rs # v = rs' # v.

    Lemma regmap_ext:
      forall {A : Type} (rs rs' : Regmap.t A) regs,
        (forall r, In r regs -> rs # r = rs' # r) ->
        rs ## regs = rs' ## regs.
Proof.
      induction regs; intros; intuition; simpl.
      rewrite H; auto.
      rewrite IHregs; auto.
    Qed.

    Lemma state_cond_eq_step:
      forall (st1 st2 st1':cstate)
        (STEQ: state_cond_eq st1 st2)
        (IN': st1'%pc ∈ loop)
        (STEP: step' st1 st1')
        (HR: ~ may_update_mem st1%pc),
        exists st2', step' st2 st2' /\ state_cond_eq st1' st2'.
Proof.
      unfold state_cond_eq.
      intros.
      destruct STEQ as (IN & EQ & MEM & FORALL).
      destruct st2; simpl.
      inv STEP; simpl.
      destruct get_st; simpl in *.
      inv H; simpl in *.
      Case "Inop".
        econstructor; split; [econstructor;eauto;econstructor 1;eauto|simpl; intuition eauto].
      Case "Iop".
        econstructor; split; [econstructor;eauto;econstructor 2;eauto|simpl; intuition].
        replace (rs##args) with (rs1##args); eauto.
        eapply regmap_ext; eauto with use_hints.
        repeat rewrite Regmap.gsspec; destruct peq; eauto.
      Case "Iload".
        econstructor; split; [econstructor;eauto;econstructor 3;eauto|simpl; intuition].
        replace (rs##args) with (rs1##args); eauto.
        eapply regmap_ext; eauto with use_hints.
        repeat rewrite Regmap.gsspec; destruct peq; eauto.
      Case "Istore".
        destruct HR; econstructor 2; eauto.
      Case "Ibuiltin".
        econstructor; split; [econstructor;eauto;econstructor 5;eauto|simpl; intuition].
        destruct ef;
          try solve [destruct HR; econstructor 1; intros; eauto; intro CONTRA; inversion CONTRA].
        replace (rs##args) with (rs1##args); eauto.
        eapply regmap_ext; eauto with use_hints.
        replace (rs##args) with (rs1##args); eauto.
        eapply regmap_ext; eauto with use_hints.
        destruct ef;
          try solve [destruct HR; econstructor 1; intros; eauto; intro CONTRA; inversion CONTRA];
        repeat rewrite Regmap.gsspec; destruct peq; eauto.
      Case "Icond".
        econstructor; split; [econstructor;eauto;econstructor 6;eauto|simpl; intuition].
        replace (rs##args) with (rs1##args); eauto.
        eapply regmap_ext; eauto with use_hints.
        destruct b; eauto.
      Case "Ijumptable".
        econstructor; split; [econstructor; eauto; econstructor 7; eauto|simpl; intuition].
        rewrite <- (FORALL arg pc0); eauto with use_hints.
        apply list_nth_z_in in H2.
        eapply FORALL; eauto.
    Qed.

    Lemma state_cond_eq_path:
      forall tr1 st1 st2 st1',
        state_cond_eq st1 st2 ->
        st1%pc ∈ loop ->
        DTrace (st1'::tr1++st1::nil) ->
        (forall st, In st (st1'::tr1) -> st%pc ∈ loop) ->
        (forall pc, pc ∈ loop -> ~ may_update_mem pc) ->
        exists tr2, exists st2',
          DTrace (st2'::tr2++st2::nil) /\
          (forall st, In st (st2'::tr2) -> st%pc ∈ loop)
          /\ state_cond_eq st1' st2'.
Proof.
      induction tr1; intros.
      exists nil; inv H1.
      assert (st1'%pc ∈ loop) by eauto with datatypes.
      edestruct state_cond_eq_step as (st2' & S1 & S2); eauto.
      exists st2'; simpl; split.
      econstructor; eauto.
      econstructor.
      split; auto.
      destruct S2 as (IN & EQ & MEM & FORALL).
      destruct 1; intuition; congruence.
      inv H1.
      edestruct IHtr1 as (tr2 & st2' & S1 & S2 & S3); eauto.
      assert (st1'%pc ∈ loop) by eauto with datatypes.
      edestruct state_cond_eq_step as (st2'' & S1' & S2'); eauto.
      exists (st2'::tr2); exists st2''; split.
      econstructor; eauto.
      split; auto.
      simpl; destruct 1; auto.
      destruct S2' as (IN & EQ & MEM & FORALL).
      congruence.
    Qed.

    CoInductive State_diverge_DTrace: cstate -> Prop :=
    | State_diverge_DTrace_intro: forall s1 tr s2,
      DTrace (s2::tr++s1::nil) ->
      State_diverge_DTrace s2 ->
      State_diverge_DTrace s1.

    Lemma DTrace_app_elim2: forall tr1 s tr2,
      DTrace (s::tr1++tr2) -> DTrace (s::tr1).
Proof.
      induction tr1; simpl.
      constructor.
      intros.
      inv H; econstructor; eauto.
    Qed.

    Lemma Trace_terminates_no_state_cond_eq_aux:
      forall s tr tr' s'
        (TR: DTrace (s :: tr ++ s' :: tr'))
        (IN_LOOP: forall st, In st (s :: tr ++ s' :: nil) -> st%pc ∈ loop)
        (NO_UPD: forall pc, pc ∈ loop -> ~ may_update_mem pc)
        (SE: state_cond_eq s' s),
        State_diverge_DTrace s.
Proof.
      cofix COINDHYP; intros.
      destruct (state_cond_eq_path tr s' s s) as (tr2 & st2' & S1 & S2 & S3); auto.
      eauto with datatypes.
      unfold state_cond_eq in *; auto.
      apply DTrace_app_elim2 with tr'.
      rewrite app_ass; simpl; auto.
      simpl; intros; intuition eauto with datatypes.
      subst; eauto with datatypes.
      constructor 1 with tr2 st2'; auto.
      apply COINDHYP with tr2 nil s; auto.
      simpl; destruct 1; auto.
      subst; apply S2; eauto with datatypes.
      rewrite in_app in H.
      destruct H; auto.
      simpl in H; intuition.
      subst; eauto with datatypes.
    Qed.

    Lemma nil_or_last: forall A (l:list A),
      l = nil \/ exists x, exists q, l = q++(x::nil).
Proof.
      induction l; auto.
      right.
      destruct IHl as [IH|(x & q & IH)].
      subst; exists a; exists nil; auto.
      subst; exists x; exists (a::q); auto.
    Qed.

    Lemma In_exists_app: forall A x (l:list A),
      In x l -> exists l1, exists l2, l = l1++(x::l2).
Proof.
      induction l; simpl; intuition.
      subst; exists nil; simpl; eauto.
      destruct H as (l1 & l2 & H).
      exists (a::l1); exists l2.
      simpl; congruence.
    Qed.
  
    Lemma Dtrace_last_step: forall q x y,
      DTrace (q ++ x :: y :: nil) ->
      step' y x.
Proof.
      induction q; simpl; intros.
      inv H; auto.
      inv H.
      assert (length (@nil cstate) = length (q++x::y::nil)) by congruence.
      generalize H.
      simpl; rewrite app_length; simpl; intros.
      apply False_ind; omega.
      rewrite H1 in H2; eauto.
    Qed.

    Lemma Dtrace_remove_last: forall q x y,
      DTrace (q ++ x :: y :: nil) ->
      DTrace (q ++ x :: nil).
Proof.
      induction q; simpl; intros.
      constructor.
      destruct q; simpl; constructor.
      constructor.
      inv H; auto.
      simpl in *; inv H; auto.
      apply IHq with y; auto.
      inv H; auto.
    Qed.

    Notation State_diverge := (State_diverge ge f fsc sp).

    Lemma State_diverge_DTrace_State_diverge: forall s,
      State_diverge_DTrace s -> State_diverge s.
Proof.
      cofix COINDHYP; intros.
      inv H.
      destruct (nil_or_last _ tr) as [N|(x & q & N)]; subst; simpl in *.
      inv H0.
      constructor 1 with s2; auto.
      rewrite app_ass in H0; simpl in H0.
      constructor 1 with x.
      apply Dtrace_last_step with (s2::q); auto.
      apply COINDHYP.
      constructor 1 with q s2; auto.
      generalize (Dtrace_remove_last (s2::q) x s); simpl; auto.
    Qed.

   Lemma State_diverge_State_diverge_DTrace: forall s,
      State_diverge s -> State_diverge_DTrace s.
Proof.
      cofix COINDHYP; intros.
      inv H.
      constructor 1 with nil s2; auto.
      simpl; constructor; auto.
      constructor.
    Qed.


    Lemma last_diverge: forall tr s s0,
      DTrace (tr++s0::nil) ->
      In s (tr++s0::nil) ->
      State_diverge s ->
      State_diverge s0 .
Proof.
      induction tr; simpl; intros.
      > intuition.
        congruence.
      > destruct H0; subst.
        > apply State_diverge_DTrace_State_diverge.
          constructor 1 with tr s; auto.
          apply State_diverge_State_diverge_DTrace; auto.
        > inv H.
          > generalize (app_length tr (s0::nil)); rewrite <- H4; simpl.
            intros; apply False_ind; omega.
          > rewrite H3 in *; eauto.
    Qed.

    Lemma Trace_terminates_no_state_cond_eq:
      forall s tr s',
        DTrace (s :: tr) -> In s' tr ->
        (forall st, In st (s::tr) -> st%pc ∈ loop) ->
        (forall pc, pc ∈ loop -> ~ may_update_mem pc) ->
        (state_cond_eq s' s) ->
        State_diverge s.
Proof.
      intros.
      apply State_diverge_DTrace_State_diverge.
      eelim In_exists_app; eauto; intros tr1 (tr2 & TR).
      subst.
      eapply Trace_terminates_no_state_cond_eq_aux; eauto.
      intros; apply H1.
      replace (s :: tr1 ++ s' :: tr2) with ((s :: tr1 ++ s'::nil) ++ tr2).
      eauto with datatypes.
      simpl; rewrite app_ass; auto.
    Qed.

  End STATE_COND_EQ.

  Section bound_rcs.

    Variable n: node.
    Variable loop: Scope.t.
    Variable vars: list reg.
    Variable n_f_In: f_In n f.
    Variable n_in_loop: n ∈ loop.
    Variable scope_n_loop: scope n = loop.
    Variable vars_enough :
      forall v pc1 pc2,
        pc1 ∈ loop ->
        pc2 ∈ loop -> use f pc1 v -> def f pc2 v -> Live f n v -> In v vars.
    Variable no_mem_update:
      forall pc, pc ∈ loop -> ~ may_update_mem pc.

    Lemma same_mem: forall tr s s',
        DTrace (s::tr) -> In s' tr ->
        (forall st, In st (s::tr) -> st%pc ∈ loop) ->
        s%m = s'%m.
Proof.
      induction tr; simpl; try (intuition; fail).
      intros.
      inv H.
      assert (s%m = a%m).
      > exploit (H1 a); auto; intros HI.
        inv H6; simpl in *.
        inv H; auto. eelim no_mem_update; eauto.
        > econstructor 2; eauto.
          destruct ef;
          try (eelim no_mem_update; eauto; econstructor 1; eauto; discriminate);
          inv H3; auto.
      destruct H0; subst; auto.
      rewrite H; auto.
    Qed.

    Definition val_to_Z (v : val) : Z :=
      match v with
        | Vint i => Int.signed i
        | _ => 0%Z
      end.

    Definition var_elem (rs:regset) : list (reg*Z) :=
      map (fun x => (x,val_to_Z rs#x)) vars.

    Definition proj_hist (tr:list cstate) : list (list (reg*Z)) :=
      map (fun (s:cstate) => var_elem s%rs)
        (filter (fun (s:cstate) => peq n s%pc) tr).

    Lemma var_elem_eq: forall rs rs',
      var_elem rs = var_elem rs' ->
      (forall v, In v vars -> exists i, rs#v = Vint i) ->
      (forall v, In v vars -> exists i, rs'#v = Vint i) ->
      forall v, In v vars -> rs#v = rs'#v.
Proof.
      unfold var_elem; clear vars_enough.
      induction vars; simpl.
      > intuition.
      > intros.
        inv H.
        destruct H2.
        > subst.
          destruct (H0 v); auto; clear H0.
          destruct (H1 v); auto; clear H1.
          rewrite H0 in *; rewrite H in *; inv H4.
          destruct x; destruct x0.
          f_equal.
          apply Int.mkint_eq; auto.
          unfold Int.signed in H2; simpl in *.
          destruct zlt; destruct zlt; omega.
        > apply IHl; auto with datatypes.
    Qed.
 
    Lemma step_def: forall s s' v,
      step' s s' ->
      (s %rs) # v = (s' %rs) # v \/ def f s%pc v.
Proof.
      intros.
      inv H.
      inv H0; simpl; auto;
        rewrite Regmap.gsspec; destruct peq; auto;
          subst; right.
        > econstructor 1; eauto.
        > econstructor 2; eauto.
        > econstructor 4; eauto.
    Qed.

    Lemma Dtrace_no_def: forall v tr s,
      DTrace (s::tr) ->
      (forall st, In st tr -> st%pc ∈ loop) ->
      ~ (exists pc' : node, pc' ∈ loop /\ def f pc' v) ->
      forall s', In s' tr ->
        (s' %rs) # v = (s %rs) # v.
Proof.
      induction tr; intuition.
      simpl in H2; intuition.
      > subst; inv H.
        eelim step_def; eauto; intro.
        eelim H1; eauto; congruence.
      > inv H.
        replace (s%rs#v) with (a%rs#v).
        > eapply IHtr; eauto.
        > eelim step_def; eauto; intro.
          eelim H1; eauto; congruence.
    Qed.
    
    Lemma dup_state_cond_eq: forall s tr,
      DTrace (s::tr) ->
      s%pc = n ->
      (forall st, In st (s::tr) -> st%pc = n ->
        forall v, In v vars -> exists i, (st%rs)#v = Vint i) ->
      (forall st, In st tr -> st%pc ∈ loop) ->
      In (var_elem s%rs) (proj_hist tr) ->
      exists s',
        In s' tr /\ state_cond_eq loop s' s.
Proof.
      clear scope_n_loop.
      unfold proj_hist; intros.
      rewrite in_map_iff in H3; destruct H3 as [s' [S1 S2]].
      rewrite filter_In in S2; destruct S2 as (S2 & S3).
      destruct peq; try (intuition; fail); subst; clear S3.
      exists s'; split; auto.
      repeat split; auto.
      > symmetry; eapply same_mem; eauto.
        intros st Hs; simpl in Hs; destruct Hs; auto.
        congruence.
      > rewrite <- e; intros.
        destruct (classic (exists pc', pc' ∈ loop /\ def f pc' v))
          as [(pc'' & D1 & D2)| D].
        > eapply var_elem_eq; eauto.
        > eapply Dtrace_no_def; eauto.
    Qed.

    Lemma DTrace_NoDup_proj_hist: forall tr,
      DTrace tr ->
      (forall st, In st tr -> ~ State_diverge ge f fsc sp st) ->
      (forall st, In st tr -> st%pc = n ->
        forall v, In v vars -> exists i, (st%rs)#v = Vint i) ->
      (forall st, In st tr -> st%pc ∈ loop) ->
      NoDup (proj_hist tr).
Proof.
      clear scope_n_loop.
      induction tr; simpl; intros.
      > constructor.
      > inv H.
        > unfold proj_hist; simpl; destruct peq; simpl;
          repeat constructor; simpl; intuition.
        > exploit IHtr; auto; clear IHtr; intros IH.
          assert (DTrace (a :: s :: tr0)) by (constructor; auto).
          generalize dependent (s::tr0); intros.
          unfold proj_hist; simpl; destruct peq; simpl; auto.
          constructor; auto.
          intro I.
          subst.
          eelim dup_state_cond_eq; eauto.
          > intros s' (S1 & S2).
            elim (H0 a); auto.
            eapply Trace_terminates_no_state_cond_eq; eauto.
          > rewrite e; simpl; auto.
          > unfold proj_hist; rewrite e; auto.
    Qed.


    Lemma rcs_bounded_by_length_proj_hist_aux: forall tr s s0,
      DTrace (s::tr++s0::nil) ->
      (forall st, In st (tr++s0::nil) -> st%pc ∈ loop) ->
      s%pc ∈ (scope n) ->
      s%rcs # n = length (proj_hist (tr++s0::nil)) + s0%rcs#n.
Proof.
      induction tr; simpl; intros.
      > inv H.
        exploit step_rcs; eauto; intros S1.
        rewrite S1.
        rewrite inc_r_counter_out.
        > unfold proj_hist; simpl; destruct peq; simpl.
          > subst; rewrite inc_counter_new; auto.
            omega.
          > rewrite inc_counter_old; auto; omega.
        > intro He; elim in_last_exited_scope with (1:=He).
          intros sc (SS1 & S2 & S3 & S4).
          elim S4.
          eapply in_scope_get_scope_trans; eauto.
      > inv H.
        exploit step_rcs; eauto; intros S1.
        exploit IHtr; eauto; intros IH; clear IHtr.
        rewrite S1.
        rewrite inc_r_counter_out.
        > unfold proj_hist; simpl; destruct peq; simpl.
          > subst; rewrite inc_counter_new; auto.
            rewrite <- e in *.
            unfold proj_hist in *.
            omega.
          > rewrite inc_counter_old; auto; omega.
        > intro He; elim in_last_exited_scope with (1:=He).
          intros sc (SS1 & S2 & S3 & S4).
          elim S4.
          eapply in_scope_get_scope_trans; eauto.
    Qed.

    Lemma not_in_scope_rcs_zero: forall s s',
      step' s s' ->
      (~ s%pc ∈ loop -> s%rcs #n = 0) ->
      (~ s'%pc ∈ loop -> s'%rcs #n = 0).
Proof.
      intros.
      exploit step_rcs; eauto; intros S1; rewrite S1.
      unfold inc_r_counter.
      destruct (In_dec s%pc loop).
      > rewrite reset_counters_inv_in; auto.
        apply in_exited_trans; eauto; rewrite scope_n_loop; auto.
      > assert (forall x:nat, x<= s%rcs#n -> x = 0).
        > intros x; rewrite H0; auto; omega.
        apply H2.
        eapply le_trans.
        eapply reset_counters_le.
        rewrite inc_counter_old; auto.
        intro; eelim n0; try congruence.
        rewrite H3; auto.
    Qed.

    Lemma not_in_scope_rcs_zero_DTrace: forall tr s s',
      DTrace (tr++s::nil) ->
      (~ s%pc ∈ loop -> s%rcs #n = 0) ->
      In s' (tr++s::nil) -> (~ s'%pc ∈ loop -> s'%rcs #n = 0).
Proof.
      clear scope_n_loop.
      induction tr; simpl; intros.
      > intuition.
        subst; auto.
      > inv H.
        > generalize (app_length tr (s::nil)); rewrite <- H5; simpl.
          intros; apply False_ind; omega.
        > destruct H1.
          > subst.
            apply (not_in_scope_rcs_zero s0 s'); eauto.
            intros; apply IHtr with s; auto; try congruence.
            rewrite <- H4; auto with datatypes.
          > apply IHtr with s; auto; congruence.
    Qed.

    Lemma DTrace_init_rcs_exists: forall s0 tr s,
      DTrace (s::tr++s0::nil) ->
      (forall st, In st (s::tr++s0::nil) -> ~ st%pc ∈ loop -> st%rcs #n = 0) ->
      ~ s0%pc ∈ loop ->
      s%pc ∈ loop ->
      exists tr1, exists s', exists tr2,
        s::tr++s0::nil = tr1 ++ s' :: tr2 /\
        s'%rcs # n = 0 /\ s'%pc ∈ loop /\
        (forall s', In s' tr1 -> s'%pc ∈ loop).
Proof.
      induction tr; simpl; intros.
      > exists nil; exists s; exists (s0::nil); repeat split; auto.
        > inv H.
          exploit step_rcs; eauto; intros S1; rewrite S1.
          unfold inc_r_counter.
          assert (forall x:nat, x<= s0%rcs#n -> x = 0).
          > intros x; rewrite H0; auto; omega.
          apply H.
          eapply le_trans.
          > eapply reset_counters_le.
          > rewrite inc_counter_old; auto.
            intro; eelim H1; congruence.
        > simpl; intuition.
      > inv H.
        destruct (In_dec a%pc (scope n)).
        > edestruct IHtr as (tr1 & s' & tr2 & T1 & T2 & T3 & T4); eauto.
          exists (s::tr1); exists s'; exists tr2; intuition.
          > rewrite T1; simpl; auto.
          > simpl in H; destruct H; auto.
            congruence.
        > exists nil; exists s; simpl; econstructor; intuition.
          exploit step_rcs; eauto; intros S1; rewrite S1.
          unfold inc_r_counter.
          assert (forall x:nat, x<= a%rcs#n -> x = 0).
          > intros x; rewrite H0; auto; omega.
          apply H.
          eapply le_trans.
          > eapply reset_counters_le.
          > rewrite inc_counter_old; auto.
            intro; eelim n0.
            rewrite H3; auto.
     Qed.

    Lemma rcs_bounded_by_length_proj_hist: forall tr s s0,
      DTrace (s::tr++s0::nil) ->
      (forall st, In st (s::tr++s0::nil) -> ~ st%pc ∈ loop -> st%rcs #n = 0) ->
      ~ s0%pc ∈ loop ->
      s%pc ∈ loop ->
      exists tr', exists tr'',
        tr++s0::nil = tr' ++ tr'' /\
        s%rcs # n = length (proj_hist tr') /\
        (forall s', In s' tr' -> s'%pc ∈ loop).
Proof.
      intros.
      destruct (In_dec s%pc loop).
      > edestruct DTrace_init_rcs_exists as (tr1 & s' & tr2 & T1 & T2 & T3 & T4); eauto.
        destruct tr1; inversion T1.
        > exists nil; exists (tr++s0::nil); intuition.
        > exists (tr1++s'::nil); exists tr2; repeat split.
          > rewrite app_ass; simpl; auto.
          > exploit (rcs_bounded_by_length_proj_hist_aux tr1 c s'); eauto.
            > rewrite T1 in H.
              eapply DTrace_app_left; rewrite app_ass; simpl; eauto.
            > intros.
              rewrite in_app in H3; destruct H3; auto.
              simpl in H3; intuition; congruence.
            > congruence.
            > omega.
          > intros.
            rewrite in_app in H3.
            destruct H3; auto with datatypes.
            simpl in H3; intuition.
            congruence.
      > exists nil; exists (tr++s0::nil); split; auto.
        rewrite H0; intuition.
    Qed.

  End bound_rcs.

  Section SEQ.

    Fixpoint seq_aux {A : Type} (a : A) (count : nat) (start : Z) : list (A * Z) :=
      match count with
        | O => (a, start) :: nil
        | S n => (a, start) :: seq_aux a n (start + 1)
      end.

    Lemma in_seq_aux:
      forall {A : Type} (a : A) c s n,
        (s <= n <= (Z_of_nat c) + s)%Z ->
        In (a, n) (seq_aux a c s).
Proof.
      induction c; intros.
      simpls.
      assert (s = n) by lia2.
      subst; auto.
      destruct (Z_eq_dec s n); subst.
      simpl; auto.
      gen (IHc (s + 1)%Z n).
      destruct H.
      simpl.
      right. apply H0.
      split; lia2.
    Qed.

    Lemma in_seq_aux_inv:
      forall {A : Type} (a : A) c s n,
        In (a, n) (seq_aux a c s) ->
        (s <= n <= (Z_of_nat c) + s)%Z.
Proof.
      induction c; intros.
      destruct H; trim; simpl. inv H; lia2.
      destruct H; subst; try lia2.
      inv H; lia2.
      apply IHc in H. lia2.
    Qed.

    Lemma seq_aux_length:
      forall {A : Type} (a : A) c s,
        length (seq_aux a c s) = c + 1.
Proof.
      induction c; intros; trim.
      simpls.
      f_equal.
      rewrite IHc; refl.
    Qed.
    
    Definition seq {A : Type} (a : A) (itv : interval) : list (A * Z) :=
      let low := itv_min itv in
        let hi := itv_max itv in
          let diff := (hi - low)%Z in
            seq_aux a (nat_of_Z diff) low.

    
    Lemma itv_length_ge_zero:
      forall o,
        (itv_length o >= 0)%Z.
Proof.
      intros.
      destruct o; simpl.
      unfold itv_length; simpl.
      omega.
    Qed.

Require Import ValueAnalysis_proof.

    Lemma in_seq:
      forall (A : Type) (a : A) itv n,
        In_interval n itv ->
        In (a, n) (seq a itv).
Proof.
      intros.
      unfold seq. apply in_seq_aux. rewrite nat_of_Z_max.
      inv H. lia2.
    Qed.
    
    Lemma seq_length:
      forall (A : Type) (a : A) itv,
        length (seq a itv) = nat_of_Z (itv_length itv).
Proof.
      intros. unfold seq. rewrite seq_aux_length.
      unfold itv_length.
      assert (itv_max itv >= itv_min itv)%Z.
      apply itv_wf.
      rewrite nat_of_Z_plus; auto; lia2.
    Qed.


Definition seq_dom (pc : node) (v : reg) : list (reg * Z) :=
  match value f pc v with
    | Error _ => nil
    | OK itv => seq v itv
  end.

Lemma seq_dom_length:
  forall pc v,
    length (seq_dom pc v) = match value f pc v with
                              | Error _ => 0
                              | OK oitv => nat_of_Z (itv_length oitv)
                            end.
Proof.
  intros.
  unfold seq_dom.
  optDecGN DOM; trim.
  rewrite seq_length; auto.
Qed.

Section SEQ_LIST.
  Variable A : Type.
  Hypothesis Adec : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}.
  
  Fixpoint seq_list (vals : list A) (ll : list (list A)) : list (list A) :=
    match vals with
      | nil => nil
      | v :: r =>
        List.map (fun vals => v :: vals) ll ++ (seq_list r ll)
    end.

Fixpoint seq_lists (vals : list (list A)) : list (list A) :=
  match vals with
    | nil => nil :: nil
    | lv :: lr =>
      let ll := seq_lists lr in
        seq_list lv ll
  end.


Lemma In_seq_list: forall q ll l a,
  In a l ->
  In q ll ->
  In (a :: q) (seq_list l ll).
Proof.
  induction l; simpl; intuition.
  subst; simpl.
  rewrite in_app; left.
  apply in_map; auto.
Qed.

Inductive In_pointwise : list A -> list (list A) -> Prop :=
| In_pointwise_nil: In_pointwise nil nil
| In_pointwise_cons: forall a q l ll
  (IP1: In a l)
  (IP2: In_pointwise q ll),
  In_pointwise (a::q) (l::ll).

Lemma In_pointwise_In_seq_lists: forall l ll,
  In_pointwise l ll ->
  In l (seq_lists ll).
Proof.
  induction 1; simpl.
  > left; constructor.
  > eapply In_seq_list; eauto.
Qed.

Lemma In_pointwise_map: forall B f1 f2 l,
  (forall x:B, In x l -> In (f1 x) (f2 x)) ->
  In_pointwise (map f1 l) (map f2 l).
Proof.
  induction l; simpl; constructor; auto.
Qed.

Lemma length_seq_list:
  forall vals ll,
    length (seq_list vals ll) = length ll * length vals.
Proof.
  induction vals; auto; intros; simpl.
  rewrite app_length.
  rewrite map_length.
  rewrite IHvals.
  lia2.
Qed.

Lemma fold_left_mult_comm:
  forall {A : Type} (f : A -> nat) l v1 v2,
    (fold_left (fun a0 a => f a * a0) l v1) * v2 =
    fold_left (fun a0 a => f a * a0) l (v1 * v2).
Proof.
  induction l; intros; trim.
  simpl.
  rewrite IHl; auto.
  f_equal.
  lia2.
Qed.

Lemma length_seq_lists:
  forall vals,
    length (seq_lists vals) = List.fold_left (fun l0 l => length l * l0) vals 1.
Proof.
  induction vals; auto.
  simpl.
  rewrite length_seq_list.
  rewrite IHvals.
  rewrite mult_1_r.
  rewrite fold_left_mult_comm. f_equal. lia2.
Qed.


End SEQ_LIST.

Implicit Arguments seq_list [[A]].
Implicit Arguments seq_lists [[A]].
Implicit Arguments In_pointwise [[A]].
Implicit Arguments length_seq_list [[A]].
Implicit Arguments length_seq_lists [[A]].


Definition seq_vars (pc : node) (vars : list reg) : list (list (positive * Z)) :=
  let vars_vals := List.map (fun v => seq_dom pc v) vars in seq_lists vars_vals.

Lemma In_seq_vars: forall pc vars vals (tr:list cstate),
  (forall s, In s tr ->
    s%pc = pc ->
    forall x, In x vars ->
      exists itv, value f s %pc x = OK itv /\ In_interval (val_to_Z s%rs#x) itv) ->
  In vals (proj_hist pc vars tr) -> In vals (seq_vars pc vars).
Proof.
  unfold seq_vars; intros pc vars vals tr HH H.
  apply In_pointwise_In_seq_lists.
  unfold proj_hist in H.
  rewrite in_map_iff in H.
  destruct H as (s & S1 & S2).
  rewrite filter_In in S2; destruct S2 as (S2 & S3).
  destruct peq; intuition; subst; clear S3.
  unfold var_elem.
  apply In_pointwise_map.
  intros x Hx.
  unfold seq_dom.
  edestruct HH as (itv & HI1 & HI2); eauto.
  rewrite HI1.
  apply in_seq; auto.
Qed.

Lemma length_seq_vars:
  forall pc vars z z0,
    prod_doms_aux f z0 pc vars = OK z ->
    (Z_of_nat (length (seq_vars pc vars)) * z0 = z)%Z.
Proof.
  induction vars; simpl; intros z; unfold prod_doms.
  > intros.
    inv H; auto.
    destruct z; auto.
  > unfold seq_vars.
    unfold prod_doms_aux; simpl.
    case_eq (value f pc a); simpl; unfold prod_doms_aux in *; intros.
    > generalize (IHvars _ _ H0); clear IHvars H0; intros.
      rewrite length_seq_list.
      unfold seq_vars in *.
      generalize (seq_dom_length pc a); rewrite H; intros T; rewrite T.
      rewrite inj_mult.
      rewrite nat_of_Z_eq.
      simpl in *.
      rewrite <- Zmult_assoc; auto.
      apply itv_length_ge_zero.
    > rewrite fold_error in H0; trim.
  Qed.

Lemma prod_doms_value_itv: forall pc vars z z0,
  prod_doms_aux f z0 pc vars = OK z ->
  forall x,
    In x vars -> exists itv, value f pc x = OK itv.
Proof.
  induction vars; simpl; intros z; unfold prod_doms_aux.
  > intuition.
  > intros; simpl in *.
    case_eq (value f pc a); simpl; intros.
    > rewrite H1 in *; simpl in *.
      > destruct H0; subst; eauto.
    > rewrite H1 in H; simpl in H.
      rewrite fold_error in H; trim.
Qed.

Lemma prod_doms_pos:
  forall pc vars z z0,
    prod_doms_aux f z0 pc vars = OK z ->
    (z0 > 0 -> z > 0)%Z.
Proof.
  induction vars; simpl; intros z; unfold prod_doms.
  > intros.
    inv H; auto.
  > unfold prod_doms_aux; simpl.
    case_eq (value f pc a); simpl; unfold prod_doms_aux in *; intros.
      > generalize (IHvars _ _ H0); clear IHvars H0; intros.
        apply H0.
        generalize (itv_wf i); intros.
        unfold itv_length in *.
        auto with zarith.
      > rewrite fold_error in H0; trim.
  Qed.

End SEQ.

Section Trace.

  Lemma Trace_DTrace: forall tr,
    Trace' tr ->
    exists tr',
      tr = tr'++(init_st f rs0 m0)::nil /\ DTrace tr.
Proof.
    induction 1.
    > exists nil; repeat (econstructor; eauto).
    > destruct IHTrace as (tr' & T1 & T2).
      exists (s'::tr'); split.
      > rewrite T1; simpl; eauto.
      > constructor; auto.
  Qed.

End Trace.

Section check_may_not_update_mem.

Definition check_may_not_update_mem (loop:list node) : bool :=
  forallb
  (fun pc =>
    match (fn_code f)! pc with
      | None => false
      |Some ins =>
        match ins with
          | Ibuiltin ef _ _ _ =>
            match ef with
              | EF_annot _ _
              | EF_annot_val _ _ => true
              | _ => false
            end
          | Istore _ _ _ _ _
          | Icall _ _ _ _ _
          | Itailcall _ _ _ => false
          | _ => true
        end
    end)
  loop.

Lemma check_may_not_update_mem_correct : forall loop,
  check_may_not_update_mem loop = true ->
  forall pc, In pc loop -> ~ may_update_mem pc.
Proof.
  unfold check_may_not_update_mem; intros.
  rewrite forallb_forall in H.
  intro M; inv M; exploit H; eauto.
  rewrite H1; destruct ef; congruence.
  rewrite H1; congruence.
  rewrite H1; congruence.
  rewrite H1; congruence.
Qed.

Definition check_all_only_special_builtins : bool :=
  ptree_forall (fn_code f)
  (fun pc ins =>
        match ins with
          | Ibuiltin ef _ _ _ => match ef with
                                   | EF_annot _ _
                                   | EF_annot_val _ _
                                   | EF_memcpy _ _ => true
                                   | _ => false
                                 end
          | _ => true
        end).

Lemma check_all_only_special_builtins_correct :
  check_all_only_special_builtins = true ->
  forall pc, ~ contains_misc_builtins pc.
Proof.
  unfold check_all_only_special_builtins; intros.
  rewrite ptree_forall_correct in H.
  intro M; inv M; exploit H; eauto; simpl.
  destruct ef; try congruence.
Qed.

Definition check_all_may_update_mem : bool :=
  ptree_forall (fn_code f)
  (fun pc ins =>
        match ins with
          | Ibuiltin ef _ _ _ =>
            match ef with
                | EF_annot _ _
                | EF_annot_val _ _ => true
                | _ => false
            end
          | Istore _ _ _ _ _
          | Icall _ _ _ _ _
          | Itailcall _ _ _ => false
          | _ => true
        end).

Lemma check_all_may_update_mem_correct :
  check_all_may_update_mem = true ->
  forall pc, ~ may_update_mem pc.
Proof.
  unfold check_all_may_update_mem; intros.
  rewrite ptree_forall_correct in H.
  intro M; inv M; exploit H; eauto; simpl; try destruct ef; congruence.
Qed.

End check_may_not_update_mem.

Section Live.


Definition build_live (f:function) : res (node -> Regset.t) :=
  match analyze f with
    | None => Error (MSG ("build live failed") :: nil)
    | Some livemap => OK (fun n => (Lin f n (Lout livemap)))
  end.

Lemma build_live_correct: forall live,
  build_live f = OK live ->
  forall n v,
    Live f n v -> Regset.In v (live n).
Proof.
  unfold build_live; intros live.
  case_eq (analyze f); try congruence.
  intros m Hlive T.
  inv T.
  eapply build_live_correct; eauto.
Qed.

End Live.

Section build_use_def_var.

  Definition build_def (n : node) (rset:Regset.t) : Regset.t :=
  match PTree.get n f.(fn_code) with
    | None => rset
    | Some i => match i with
                  | Inop s => rset
                  | Iop op args res s => Regset.add res rset
                  | Iload chunk addr args dst s => Regset.add dst rset
                  | Istore chunk addr args src s => rset
                  | Icall sig ros args res s => Regset.add res rset
                  | Itailcall sig ros args => rset
                  | Ibuiltin ef args res s => Regset.add res rset
                  | Icond cond args ifso ifnot => rset
                  | Ijumptable arg tbl => rset
                  | Ireturn optarg => rset
                end
  end.

  Lemma build_def_prop1: forall pc v rset,
    def f pc v -> Regset.In v (build_def pc rset).
Proof.
    unfold build_def; intros.
    inv H; rewrite H0;
    apply Regset.add_1; auto.
  Qed.

  Lemma build_def_prop2: forall pc v rset,
    Regset.In v rset -> Regset.In v (build_def pc rset).
Proof.
    unfold build_def; intros.
    destruct ((fn_code f)!pc); auto.
    destruct i; auto;
    apply Regset.add_2; auto.
  Qed.

  Definition build_all_def (l:list node) : Regset.t :=
    List.fold_right build_def Regset.empty l.

  Lemma build_all_def_correct: forall pc v l,
    In pc l -> def f pc v -> Regset.In v (build_all_def l).
Proof.
    unfold build_all_def; induction l; simpl; intros.
    > intuition.
    > destruct H.
      > apply build_def_prop1; subst; auto.
      > apply build_def_prop2; auto.
  Qed.

  Definition regs_to_vars (rs : list reg) (rset:Regset.t) : Regset.t :=
    List.fold_right (fun r rs0 => Regset.add r rs0) rset rs.

  Lemma regs_to_vars_prop1: forall args rset v,
    In v args ->
    Regset.In v (regs_to_vars args rset).
Proof.
    unfold regs_to_vars; induction args; simpl; intuition.
    > subst; apply Regset.add_1; auto.
    > apply Regset.add_2; auto.
  Qed.

  Lemma regs_to_vars_prop2: forall args rset v,
    Regset.In v rset ->
    Regset.In v (regs_to_vars args rset).
Proof.
    unfold regs_to_vars; induction args; simpl; intuition.
    > apply Regset.add_2; auto.
  Qed.

  Definition ros_to_var (ros : reg + ident) (rset:Regset.t) : Regset.t :=
    match ros with
      | inl r => Regset.add r rset
      | inr id => rset
    end.

  Definition optreg_to_var (o : option reg) (rset:Regset.t) : Regset.t :=
    match o with
      | None => rset
      | Some arg => Regset.add arg rset
    end.

  Definition build_use (n : node) (rset:Regset.t) : Regset.t :=
    match PTree.get n f.(fn_code) with
      | None => rset
      | Some i =>
        match i with
          | Inop s => rset
          | Iop op args _ s => regs_to_vars args rset
          | Iload chunk addr args dst s => regs_to_vars args rset
          | Istore chunk addr args src s => regs_to_vars (src :: args) rset
          | Icall _ ros args _ s => ros_to_var ros (regs_to_vars args rset)
          | Itailcall _ ros args => ros_to_var ros (regs_to_vars args rset)
          | Ibuiltin ef args _ s => regs_to_vars args rset
          | Icond cond args ifso ifnot => regs_to_vars args rset
          | Ijumptable arg tbl => Regset.add arg rset
          | Ireturn optarg => optreg_to_var optarg rset
        end
    end.

  Lemma build_use_prop1: forall pc v rset,
    use f pc v -> Regset.In v (build_use pc rset).
Proof.
    unfold build_use; intros.
    inv H; rewrite H0;
    try (apply Regset.add_1; auto; fail);
    try (apply regs_to_vars_prop1; auto; fail).
    simpl in *; destruct H1; subst.
    apply Regset.add_1; auto.
    apply Regset.add_2.
    apply regs_to_vars_prop1; auto.
    simpl in *; destruct H1; subst.
    apply Regset.add_1; auto.
    apply Regset.add_2.
    apply regs_to_vars_prop1; auto.
  Qed.

  Lemma build_use_prop2: forall pc v rset,
    Regset.In v rset -> Regset.In v (build_use pc rset).
Proof.
    unfold build_use; intros.
    destruct ((fn_code f)!pc); auto.
    destruct i; auto;
    try (apply Regset.add_2; auto; fail);
    try (apply regs_to_vars_prop2; auto; fail).
    destruct s0; simpl;
    try (apply Regset.add_2; auto);
    try (apply regs_to_vars_prop2; auto; fail).
    destruct s0; simpl;
    try (apply Regset.add_2; auto);
    try (apply regs_to_vars_prop2; auto; fail).
    destruct o; simpl; auto;
    try (apply Regset.add_2; auto).
  Qed.

  Definition build_all_use (l:list node) : Regset.t :=
    List.fold_right build_use Regset.empty l.

  Lemma build_all_use_correct: forall pc v l,
    In pc l -> use f pc v -> Regset.In v (build_all_use l).
Proof.
    unfold build_all_use; induction l; simpl; intros.
    > intuition.
    > destruct H.
      > apply build_use_prop1; subst; auto.
      > apply build_use_prop2; auto.
  Qed.

  Lemma In_InA: forall (x:reg) l,
    SetoidList.InA (fun x0 y => x0 = y) x l ->
    In x l.
Proof.
    induction l; simpl; intuition.
    inv H.
    inv H; auto.
  Qed.

  Definition build_all_use_and_def (n:node) (l:list node) : res (list reg) :=
    do live <- build_live f;
      let s1 := Regset.inter (build_all_use l) (build_all_def l) in
      let s2 := Regset.inter s1 (live n) in
      OK (Regset.elements s2).

  Lemma build_all_use_and_def_correct : forall l n s,
    build_all_use_and_def n l = OK s ->
    forall v pc1 pc2,
      In pc1 l -> In pc2 l -> use f pc1 v -> def f pc2 v -> Live f n v ->
      In v s.
Proof.
    unfold build_all_use_and_def; intros.
    monadInv H.
    apply In_InA.
    apply Regset.elements_1.
    apply Regset.inter_3.
    > apply Regset.inter_3.
      > eapply build_all_use_correct with (pc:=pc1); eauto.
      > eapply build_all_def_correct with (pc:=pc2); eauto.
    > eapply build_live_correct; eauto.
  Qed.

End build_use_def_var.

Lemma root_not_in_loop: forall h,
  f_In h f ->
  header (scope h) <> root ->
  ~ root ∈ (scope h).
Proof.
  red; intros.
  exploit Scope.in_scope_root; eauto.
  eapply Scope.scope_in_elements.
Qed.

Section main_theorem.
  Variable h: node.
  Variable vars: list reg.

  Let loop := scope h.

  Hypothesis h_in_f: f_In h f.

  Hypothesis root_not_in_loop: ~ root ∈ loop.

  Hypothesis no_infinite_loop: Terminates ge f fsc sp rs0 m0.

  Hypothesis vars_enough :
    forall v pc1 pc2,
      pc1 ∈ loop ->
      pc2 ∈ loop -> use f pc1 v -> def f pc2 v -> Live f h v -> In v vars.

  Hypothesis no_mem_update:
    forall pc, pc ∈ loop -> ~ may_update_mem pc.

  Variable bound:Z.
  Hypothesis prod_doms_res: prod_doms f h vars = OK bound.

  Lemma prod_doms_res_pos: (bound > 0)%Z.
Proof.
    unfold prod_doms in *.
    exploit prod_doms_pos; eauto.
    omega.
  Qed.

  Theorem rcs_bounded_by_prod_doms:
    forall tr s,
      Trace' (s:: tr) ->
      (Z_of_nat (s%rcs # h) <= bound)%Z.
Proof.
    intros tr s HT.
    edestruct Trace_DTrace as (tr1 & M0 & M1); eauto.
    rewrite M0 in M1.
    destruct tr1.
    > inv M0.
      unfold init_st; simpl.
      generalize (prod_doms_res_pos); intros.
      rewrite init_counters_zero; simpl; omega.
    > assert (HB:Z_of_nat (length (seq_vars h vars)) = bound).
        unfold prod_doms in *.
        exploit length_seq_vars; eauto with zarith.
      rewrite <- HB.
      apply inj_le; clear HB.
      inv M0; simpl in *.
      destruct (In_dec c%pc (scope h)) as [IS|IS].
      exploit rcs_bounded_by_length_proj_hist; eauto.
      > intros; eapply not_in_scope_rcs_zero_DTrace with (tr:=c::tr1); eauto.
        unfold init_st; simpl.
        rewrite init_counters_zero; simpl; omega.
      > intros (tr2 & tr3 & T1 & T2 & T3).
        rewrite T2.
        destruct tr2; try (simpl; omega).
        apply pigeonhole_NoDup.
        > decide equality.
          decide equality.
          > apply Z_eq_dec.
          > apply peq.
        > intros; eapply In_seq_vars; eauto.
          intros.
          unfold prod_doms in *.
          exploit prod_doms_value_itv; eauto.
          intros (itv & HI).
          exists itv; split.
          > congruence.
          > assert (HR:Reach' s).
              rewrite T1 in HT.
              eapply in_Trace_Reach; eauto with datatypes.
            exploit variable_domains_are_safe; eauto.
            > rewrite H1; eauto.
            > intros (i & Hi1 & Hi2).
              rewrite Hi1; simpl; auto.
        > eapply DTrace_NoDup_proj_hist; eauto.
          > rewrite T1 in M1.
            exploit DTrace_app_left; eauto.
            intros.
            inv H; auto.
          > red; intros.
            elim no_infinite_loop.
            assert (In st ((c :: tr1) ++ init_st f rs0 m0 :: nil)).
              simpl; rewrite T1.
              eauto with datatypes.
            clear H; eapply last_diverge; eauto.
            simpl; auto.
          > intros.
            unfold prod_doms in *.
            exploit prod_doms_value_itv; eauto.
            intros (itv & HI).
            assert (HR:Reach' st).
              rewrite T1 in HT.
              eapply in_Trace_Reach; eauto with datatypes.
            exploit variable_domains_are_safe; eauto.
            > rewrite H0; eauto.
            > intros (i & Hi1 & Hi2).
              rewrite Hi1; simpl; eauto.
   > exploit rcs_max_prefix'_out; eauto; omega.
  Qed.

  Theorem rcs_bounded_by_prod_doms':
    forall tr s,
      Trace' (s:: tr) ->
      (Z_of_nat (s%rcs # h) = bound)%Z ->
      s%pc<>h.
Proof.
    intros tr s HT HB Hh.
    edestruct Trace_DTrace as (tr1 & M0 & M1); eauto.
    rewrite M0 in M1.
    destruct tr1.
    > inversion M0.
      elim root_not_in_loop.
      unfold loop in *; subst.
      simpl.
      auto.
    > unfold prod_doms in *.
      assert (HB':Z_of_nat (length (seq_vars h vars)) = bound).
        by exploit length_seq_vars; eauto with zarith.
      simpl in M1; inversion M0; clear M0.
      subst c tr.
      exploit rcs_bounded_by_length_proj_hist; eauto.
      > intros; eapply not_in_scope_rcs_zero_DTrace with (tr:=s::tr1); eauto.
        unfold init_st; simpl.
        rewrite init_counters_zero; simpl; omega.
      > rewrite Hh; auto.
      > intros (tr2 & tr3 & T1 & T2 & T3).
        assert (length (proj_hist h vars (s::tr2)) <= length (seq_vars h vars)).
          apply pigeonhole_NoDup.
          > decide equality.
            decide equality.
            > apply Z_eq_dec.
            > apply peq.
          > intros; eapply In_seq_vars; eauto.
            intros.
            exploit prod_doms_value_itv; eauto.
            intros (itv & HI).
            exists itv; split.
            > congruence.
            > assert (HR:Reach' s0).
                rewrite T1 in HT.
                eapply in_Trace_Reach; eauto with datatypes.
                simpl in H0; destruct H0; simpl; auto with datatypes.
              rewrite <- H1 in *.
              exploit variable_domains_are_safe; eauto.
              intros (i & Hi1 & Hi2).
              rewrite Hi1; simpl; auto.
        > eapply DTrace_NoDup_proj_hist; eauto.
          > rewrite T1 in M1.
            exploit DTrace_app_left; eauto.
          > red; intros.
            elim no_infinite_loop.
            assert (In st ((s :: tr1) ++ init_st f rs0 m0 :: nil)).
              simpl; rewrite T1.
              simpl in H; destruct H; auto with datatypes.
            clear H; eapply last_diverge; eauto.
            simpl; auto.
          > intros.
            exploit prod_doms_value_itv; eauto.
            intros (itv & HI).
            assert (HR:Reach' st).
              rewrite T1 in HT.
              eapply in_Trace_Reach; eauto with datatypes.
              simpl in H; destruct H; auto with datatypes.
              left; auto.
            rewrite <- H0 in *.
            exploit variable_domains_are_safe; eauto.
            intros (i & Hi1 & Hi2); eauto.
          > simpl; destruct 1; auto.
            subst s.
            rewrite Hh; auto.
        replace (length (proj_hist h vars (s :: tr2))) with ((s %rcs) # h +1) in H.
        generalize (inj_le _ _ H).
        rewrite inj_plus.
        omega.
        rewrite T2.
        unfold proj_hist; simpl.
        rewrite map_length.
        rewrite map_length.
        destruct peq; intuition.
        simpl.
        omega.
  Qed.

End main_theorem.

End FUNCTION.

Open Scope Z_scope.

Lemma rcs_root: forall ge f fsc sp rs m s,
    Reach ge f fsc sp rs m s ->
    Z_of_nat ((get_rcs s) # (f.(fn_entrypoint))) <= 1.
Proof.
  induction 1.
  > simpl; rewrite init_counters_zero; simpl; omega.
  > exploit step_rcs; 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.
    eapply le_trans; [eapply inc_r_counter_le|idtac].
    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.

Definition local_bound (f : function) (fsc:Scope.family f) (n : node) : res Z :=
  if positive_eq_dec n f.(fn_entrypoint) then OK 1
    else
      let value_f := value f in
      let scope_n := Scope.scope fsc n in
      let nodes_n := Scope.nodes scope_n in
      do vars <- build_all_use_and_def f n nodes_n;
        if check_may_not_update_mem f nodes_n && check_all_only_special_builtins f then
          fold_left (fun rprod0 x =>
            do prod0 <- rprod0;
              do itv <- value_f n x;
                let res := (itv_length itv) * prod0 in
                  OK res
          ) vars (OK 1)
          else Error (MSG ("local_bound failed: memory updates in function") :: nil)
.

Lemma local_bound_not_may_update_mem : forall f (fsc:Scope.family f) n bound,
  local_bound f fsc n = OK bound ->
  n <> f.(fn_entrypoint) ->
  (forall pc, pc ∈ (Scope.scope fsc n) -> ~ may_update_mem f pc).
Proof.
  unfold local_bound; intros.
  destruct positive_eq_dec; intuition.
  monadInv H.
  case_eq (check_may_not_update_mem f (Scope.nodes (Scope.scope fsc n))); intros.
  > exploit check_may_not_update_mem_correct; eauto.
  > rewrite H in EQ0.
  simpl in EQ0.
  congruence.
Qed.

Lemma local_bound_no_builtin : forall f (fsc:Scope.family f) n bound,
  local_bound f fsc n = OK bound ->
  n <> f.(fn_entrypoint) ->
  forall pc, ~ contains_misc_builtins f pc.
Proof.
  unfold local_bound; intros.
  destruct positive_eq_dec; intuition.
  monadInv H.
  case_eq (check_may_not_update_mem f (Scope.nodes (Scope.scope fsc n))); intros;
  case_eq (check_all_only_special_builtins f); intros; rewrite H in EQ0; simpl in EQ0; try inv EQ0.
  > exploit check_all_only_special_builtins_correct; eauto.
  > rewrite H2 in H4.
  congruence.
Qed.

Lemma 4 in the paper: local_bound_correct. It states that local_bound produces safe over-approximations for local counters.

Theorem local_bound_correct: (* Lemma 4 *)
  forall f (fsc:Scope.family f) ge sp rs m n bound,
  local_bound f fsc n = OK bound ->
  f_In n f ->
  ~ f.(fn_entrypoint) ∈ (Scope.scope fsc n) ->
  Terminates ge f fsc sp rs m ->
  forall s,
    Reach ge f fsc sp rs m s ->
    Z_of_nat ((get_rcs s) # n) <= bound /\
    (Z_of_nat ((get_rcs s) # n) = bound -> (get_pc s) <>n).
Proof.
  intros f fsc ge sp rs m n bound H Hn H0 Hh s H1.
  destruct Reach_ex_Trace with (1:=H1) as (tr & T).
  unfold local_bound in H.
  destruct positive_eq_dec.
  > split.
    > inv H; eapply rcs_root; eauto.
    > intros; inv H.
      inv T.
      > simpl in H4.
        rewrite init_counters_zero in H4.
        inv H4.
      > intro; elim Scope.root_no_pred with f (get_pc s0); auto.
        rewrite <- H; eapply step_succ_node; eauto.
  > monadInv H.
    rename EQ0 into H.
    case_eq (check_may_not_update_mem f (Scope.nodes (Scope.scope fsc n))); intros Hc;
    case_eq (check_all_only_special_builtins f); intros Hb;
    rewrite Hc in H; rewrite Hb in H; simpl in H; try (inv H; fail).
    rename x into vars.
    split.
    > apply (rcs_bounded_by_prod_doms f fsc sp ge rs m n vars) with (tr:=tr); auto.
      > apply build_all_use_and_def_correct; auto.
      > intros; eapply check_may_not_update_mem_correct; eauto.
    > intros.
      apply (rcs_bounded_by_prod_doms' f fsc sp ge rs m n vars) with bound tr; auto.
      > apply build_all_use_and_def_correct; auto.
      > intros; eapply check_may_not_update_mem_correct; eauto.
Qed.


Generated by coq2html