Module CountingSem_proof

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Behaviors.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import Errors.
Require Import String.
Require Import DLib.
Require Import Scope.
Require Import Counter.
Require Import CountingSem.

Open Scope error_monad_scope.

Definition check_one_single_func (prog:program) : res function :=
  let ge := Genv.globalenv prog in
  do b_main <- get_opt (Genv.find_symbol ge prog.(prog_main)) "main block not found";
  do main <- get_opt (Genv.find_funct_ptr ge b_main) "main func not found";
    match main with
      | External _ => Error (MSG "main is external"::nil)
      | Internal main =>
        do _ <- ptree_forall_error
          (fun pc ins =>
            match ins with
              | Itailcall _ _ _
              | Icall _ _ _ _ _ => Error (MSG "call after inlining ?"::nil)
              | _ => OK tt
            end)
          (fn_code main);
          OK main
    end.

Section ge.

Variable prog : program.
Definition ge := Genv.globalenv prog.
Variable b_main : block.
Variable b_main_eq : Genv.find_symbol ge prog.(prog_main) = Some b_main.
Variable f: function.
Variable f_eq : Genv.find_funct_ptr ge b_main = Some (Internal f).
Variable m0: mem.
Variable m0_eq: Genv.init_mem prog = Some m0.
Variable stk:block.
Variable m1:mem.
Variable m1_stk_eq: Mem.alloc m0 0 (fn_stacksize f) = (m1, stk).
Notation sp := (Vptr stk Int.zero).
Variable scp: Scope.family f.

Hypothesis no_call:
    forall pc ins,
      (fn_code f)!pc = Some ins ->
      match ins with
        | Itailcall _ _ _
        | Icall _ _ _ _ _ => False
        | _ => True
      end.

Variable annots: PMap.t (list node).

Hypothesis valid_annotation1:
    forall pc id,
      In pc (annots # id) ->
      match (fn_code f)!pc with
        | Some (Ibuiltin (EF_annot id' _) _ _ _)
        | Some (Ibuiltin (EF_annot_val id' _) _ _ _) => id = id'
        | _ => False
      end.

Hypothesis valid_annotation2:
    forall pc ins,
      (fn_code f)!pc = Some ins ->
      match ins with
        | Ibuiltin (EF_annot id _) _ _ _
        | Ibuiltin (EF_annot_val id _) _ _ _ => In pc (annots # id)
        | _ => True
      end.

Open Scope nat_scope.

Fixpoint count_annot (id0:ident) (t:trace) : nat :=
  match t with
      | nil => 0
      | (Event_annot id _)::q =>
        if peq id id0
        then S (count_annot id0 q)
        else count_annot id0 q
      | _::q => count_annot id0 q
  end.

Fixpoint sum (f:node->nat) (l:list node) : nat :=
  match l with
      | nil => 0
      | x::q => (f x) + (sum f q)
  end.

Variable id0:ident.

Lemma count_annot_app : forall t1 t2,
  count_annot id0 (t1++t2) = count_annot id0 t1 + count_annot id0 t2.

Lemma sum_incr: forall cs pc l,
   sum (fun n : node => cs # n) l <=
   sum (fun n : node => (cs # pc <- (cs # pc + 1)) # n) l.

Lemma sum_incr_not_In: forall cs pc l,
   ~ In pc l ->
   sum (fun n : node => (cs # pc <- (cs # pc + 1)) # n) l =
   sum (fun n : node => cs # n) l.

Lemma sum_incr_In: forall cs pc l,
   In pc l ->
   S (sum (fun n : node => cs # n) l) <=
    sum (fun n : node => (cs # pc <- (cs # pc + 1)) # n) l.

Inductive match_states (tr:trace) : RTL.state -> cstate -> Prop :=
| match_states_st: forall pc rs m cs rcs,
  count_annot id0 tr <= sum (fun n => cs # n) (annots # id0) ->
  match_states
   tr (RTL.State nil f sp pc rs m) (CST (State pc rs m) cs rcs)
| match_states_ret: forall pc rs m cs rcs r mr or,
  count_annot id0 tr <= sum (fun n => cs # n) (annots # id0) ->
  (fn_code f) ! pc = Some (Ireturn or) ->
  match_states
   tr (RTL.Returnstate nil r mr) (CST (State pc rs m) cs rcs)
.

Lemma forward_simulation: forall tr s1 t s2,
  RTL.step ge s1 t s2 ->
  forall s1' (MS: match_states tr s1 s1'),
    (exists s2', cstep ge f scp sp s1' s2' /\ match_states (app tr t) s2 s2')
    \/ match_states (app tr t) s2 s1'.

Lemma match_initial_states: forall st0 t st1,
   initial_state prog st0 ->
   RTL.step ge st0 t st1 ->
   exists rs, exists m,
     match_states t st1 (init_st f rs m).

Definition L := semantics prog.

Definition star := (star (Smallstep.step L) (globalenv L)).

Lemma reach_match_states: forall s1 tr2 s2,
  star s1 tr2 s2 ->
  forall tr1 s1' rs m,
    match_states tr1 s1 s1' ->
    Reach ge f scp sp rs m s1' ->
    exists s2',
      match_states (app tr1 tr2) s2 s2' /\
      Reach ge f scp sp rs m s2'.

Lemma rtl_terminates_counter: forall t r,
  program_behaves L (Behaviors.Terminates t r) ->
  exists rs, exists m, exists s,
    Reaches_final ge f scp sp rs m /\
    Reach ge f scp sp rs m s /\
    count_annot id0 t <= sum (fun n => (get_cs s) # n) (annots # id0).

Variable bound : node -> option Z.
Variable correct_bound :
  forall rs m, Reaches_final ge f scp sp rs m ->
  forall s, Reach ge f scp sp rs m s ->
  forall n, (fn_code f)!n <> None ->
  forall b, bound n = Some b ->
    ((Z_of_nat (get_cs s) # n) <= b)%Z.

Fixpoint bound_from_list (l:list node) : option Z :=
  match l with
    | nil => Some 0%Z
    | n::q =>
      match bound_from_list q with
        | None => None
        | Some b =>
          match bound n with
              | None => None
              | Some bn => Some (bn+b)%Z
          end
      end
  end.

Lemma bound_from_list_correct: forall f l b,
  (forall n b, In n l -> bound n = Some b -> (Z_of_nat (f n) <= b)%Z) ->
  bound_from_list l = Some b ->
  (Z_of_nat (sum f l) <= b)%Z.

Lemma rtl_terminates_bound: forall t r b,
  program_behaves L (Behaviors.Terminates t r) ->
  bound_from_list (annots # id0) = Some b ->
  (Z_of_nat (count_annot id0 t) <= b)%Z.

End ge.

Section get_annots.
Variable f: function.

Definition annots : PMap.t (list node) :=
  PTree.fold
    (fun m pc ins =>
       match ins with
        | Ibuiltin (EF_annot id _) _ _ _
        | Ibuiltin (EF_annot_val id _) _ _ _ =>
          PMap.set id (pc::PMap.get id m) m
        | _ => m
       end)
    (fn_code f) (PMap.init nil).

Lemma valid_annotation1:
    forall pc id,
      In pc (annots # id) ->
      match (fn_code f)!pc with
        | Some (Ibuiltin (EF_annot id' _) _ _ _)
        | Some (Ibuiltin (EF_annot_val id' _) _ _ _) => id = id'
        | _ => False
      end.

Lemma valid_annotation2:
    forall pc ins,
      (fn_code f)!pc = Some ins ->
      match ins with
        | Ibuiltin (EF_annot id _) _ _ _
        | Ibuiltin (EF_annot_val id _) _ _ _ => In pc (annots # id)
        | _ => True
      end.

End get_annots.