Module CsharpminorLogic

Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Utf8.
Require Import AST.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Behaviors.
Require Import Csharpminor.
Require Import Switch.

Lemma eval_expr_det:
  ∀ ge e t m exp,
    ∀ v, eval_expr ge e t m exp v →
    ∀ v', eval_expr ge e t m exp v' →
    v = v'.

Lemma eval_exprlist_det:
  ∀ ge e t m expl,
    ∀ vl, eval_exprlist ge e t m expl vl →
    ∀ vl', eval_exprlist ge e t m expl vl' →
    vl = vl'.

Lemma alloc_variables_det:
  ∀ e1 m1 vars e2 m2 e2' m2',
    alloc_variables e1 m1 vars e2 m2 ->
    alloc_variables e1 m1 vars e2' m2' ->
    e2 = e2' /\ m2 = m2'.

Lemma bool_of_val_det:
  ∀ v b b',
    Val.bool_of_val v b ->
    Val.bool_of_val v b' ->
    b = b'.

Lemma switch_argument_det:
  ∀ b v n n',
    switch_argument b v n ->
    switch_argument b v n' ->
    n = n'.

Ltac determ :=
  repeat match goal with
           | H : eval_expr ?ge ?e ?t ?m ?exp ?v,
             H' : eval_expr ?ge ?e ?t ?m ?exp ?v' |- _ =>
             let EQ := fresh "EQ" in
             assert (EQ:=eval_expr_det _ _ _ _ _ _ H _ H');
               try (subst v'); clear H'
           | H : eval_exprlist ?ge ?e ?t ?m ?expl ?vl,
             H' : eval_exprlist ?ge ?e ?t ?m ?expl ?vl' |- _ =>
             let EQ := fresh "EQ" in
             assert (EQ:=eval_exprlist_det _ _ _ _ _ _ H _ H');
               subst vl'; clear H'
           | H : alloc_variables ?e1 ?m1 ?vars ?e2 ?m2,
             H' : alloc_variables ?e1 ?m1 ?vars ?e2' ?m2' |- _ =>
             let EQ := fresh "EQ" in
             let EQ1 := fresh "EQ1" in
             let EQ2 := fresh "EQ2" in
             assert (EQ:=alloc_variables_det _ _ _ _ _ _ _ H H');
               destruct EQ as [EQ1 EQ2];
               subst e2' m2'; clear H'
           | H : Val.bool_of_val ?v ?b,
             H' : Val.bool_of_val ?v ?b' |- _ =>
             let EQ := fresh "EQ" in
             assert (EQ:=bool_of_val_det _ _ _ H H');
               subst b; clear H'
           | H : switch_argument ?b ?v ?n,
             H' : switch_argument ?b ?v ?n' |- _ =>
             let EQ := fresh "EQ" in
             assert (EQ:=switch_argument_det _ _ _ _ H H');
               subst n; clear H'
           | H : ?A = Some ?x,
             H' : ?B = Some ?x' |- _ =>
             change B with A in H';
             let EQ := fresh "EQ" in
             assert (EQ:x = x') by congruence;
               subst x; clear H'
           | H : Genv.find_symbol _ ?i = Some ?x,
             H' : Genv.find_symbol _ ?i' = Some ?x |- _ =>
             let EQ := fresh "EQ" in
             assert (EQ:=Genv.genv_vars_inj _ _ _ H H'); subst i; clear H'
           | H : Vptr _ _ = Vptr _ _ |- _ => inv H
         end.

Section PROG.

Variable (prog: program).
Let ge := Genv.globalenv prog.

CoInductive hoare_stmt:
  ∀ (env:env)
    (pre_normal:temp_env -> mem -> Prop)
    (pre_label:ident -> temp_env -> mem -> Prop)
    (stmt:stmt)
    (post_normal:temp_env -> mem -> Prop)
    (post_return:val -> mem -> Prop)
    (post_exit:nat -> temp_env -> mem -> Prop)
    (post_goto:ident -> temp_env -> mem -> Prop), Prop :=

| hoare_Sskip:
  ∀ env pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) -> (post_normal le mem:Prop)) ->
    hoare_stmt env
               pre_normal pre_label
               Sskip
               post_normal post_return post_exit post_goto

| hoare_Sset:
  ∀ env id a pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
               ∃ v, eval_expr ge env le mem a v /\
                    post_normal (PTree.set id v le) mem) ->
    hoare_stmt env
               pre_normal pre_label
               (Sset id a)
               post_normal post_return post_exit post_goto

| hoare_Sstore:
  ∀ env chunk addr a pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
               ∃ vaddr v mem',
                 eval_expr ge env le mem addr vaddr /\
                 eval_expr ge env le mem a v /\
                 Mem.storev chunk mem vaddr v = Some mem' /\
                 post_normal le mem') ->
    hoare_stmt env
               pre_normal pre_label
               (Sstore chunk addr a)
               post_normal post_return post_exit post_goto

| hoare_Scall:
  ∀ env optid sig a bl pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
               ∃ vf vargs fd,
                 eval_expr ge env le mem a vf /\
                 eval_exprlist ge env le mem bl vargs /\
                 Genv.find_funct ge vf = Some fd /\
                 funsig fd = sig /\
                 hoare_fun (fun vargs' mem' => vargs = vargs' /\ mem = mem')
                           fd
                           (fun v mem' =>
                              post_normal (Cminor.set_optvar optid v le) mem')) ->
    hoare_stmt env
               pre_normal pre_label
               (Scall optid sig a bl)
               post_normal post_return post_exit post_goto

| hoare_Sbuiltin:
  ∀ env optid ef bl pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
               ∃ vargs ,
                 eval_exprlist ge env le mem bl vargs /\
                 (∃ t v mem', external_call ef ge vargs mem t v mem') /\
                 ∀ t v mem', external_call ef ge vargs mem t v mem' ->
                   (post_normal (Cminor.set_optvar optid v le) mem':Prop)) ->
    hoare_stmt env
               pre_normal pre_label
               (Sbuiltin optid ef bl)
               post_normal post_return post_exit post_goto

| hoare_Sseq:
  ∀ env s1 s2,
  ∀ pre_normal pre_label P
    post_normal post_return post_exit post_goto,
    hoare_stmt env
               pre_normal pre_label
               s1
               P post_return post_exit post_goto ->
    hoare_stmt env
               P pre_label
               s2
               post_normal post_return post_exit post_goto ->
    hoare_stmt env
               pre_normal pre_label
               (Sseq s1 s2)
               post_normal post_return post_exit post_goto

| hoare_Sifthenelse:
  ∀ env a s1 s2,
  ∀ pre_normal1 pre_normal2 pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
               ∃ v b, eval_expr ge env le mem a v /\
                      Val.bool_of_val v b /\
                      if b then pre_normal1 le mem else pre_normal2 le mem) ->
    hoare_stmt env
               pre_normal1 pre_label
               s1
               post_normal post_return post_exit post_goto ->
    hoare_stmt env
               pre_normal2 pre_label
               s2
               post_normal post_return post_exit post_goto ->
    hoare_stmt env
               pre_normal pre_label
               (Sifthenelse a s1 s2)
               post_normal post_return post_exit post_goto

| hoare_Sloop:
  ∀ env s,
  ∀ inv pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) -> (inv le mem:Prop)) ->
    hoare_stmt env
               inv pre_label
               s
               inv post_return post_exit post_goto ->
    hoare_stmt env
               pre_normal pre_label
               (Sloop s)
               post_normal post_return post_exit post_goto

| hoare_Sblock:
  ∀ env s,
  ∀ pre_normal pre_label
    post_normal post_return post_exit post_goto,
    hoare_stmt env
               pre_normal pre_label
               s
               post_normal post_return
               (fun n => match n with
                           | S n => post_exit n
                           | O => post_normal
                         end) post_goto ->
    hoare_stmt env
               pre_normal pre_label
               (Sblock s)
               post_normal post_return post_exit post_goto

| hoare_Sexit:
  ∀ env x,
  ∀ pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) -> (post_exit x le mem:Prop)) ->
    hoare_stmt env
               pre_normal pre_label
               (Sexit x)
               post_normal post_return post_exit post_goto

| hoare_Sswitch:
  ∀ env islong a cases,
  ∀ pre_normal pre_label pre_case pre_default
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
       ∃ v n,
         switch_argument islong v n /\
         eval_expr ge env le mem a v /\
         pre_case n le mem /\
         (select_switch_case n cases = None -> (pre_default le mem:Prop))) ->

    hoare_lbl_stmt env
                   pre_case pre_default (fun _ _ => False) pre_label
                   cases
                   post_normal post_return post_exit post_goto ->

    hoare_stmt env
               pre_normal pre_label
               (Sswitch islong a cases)
               post_normal post_return post_exit post_goto

| hoare_Sreturn:
  ∀ env a,
  ∀ pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
               ∃ v mem',
                 match a with
                 | None => v = Vundef
                 | Some a => eval_expr ge env le mem a v
                 end /\
                 Mem.free_list mem (blocks_of_env env) = Some mem' /\
                 post_return v mem') ->
    hoare_stmt env
               pre_normal pre_label
               (Sreturn a)
               post_normal post_return post_exit post_goto

| hoare_Slabel:
  ∀ env lbl s,
  ∀ pre_normal pre_label
    post_normal post_return post_exit post_goto,
    hoare_stmt env
               (fun le mem => pre_label lbl le mem \/ pre_normal le mem) pre_label
               s
               post_normal post_return post_exit post_goto ->
    hoare_stmt env
               pre_normal pre_label
               (Slabel lbl s)
               post_normal post_return post_exit post_goto

| hoare_Sgoto:
  ∀ env lbl,
  ∀ pre_normal pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) -> (post_goto lbl le mem:Prop)) ->
    hoare_stmt env
               pre_normal pre_label
               (Sgoto lbl)
               post_normal post_return post_exit post_goto

with hoare_lbl_stmt :
  ∀ (env:env)
    (pre_case:Z -> temp_env -> mem -> Prop)
    (pre_default:temp_env -> mem -> Prop)
    (pre_fallthrough:temp_env -> mem -> Prop)
    (pre_label:ident -> temp_env -> mem -> Prop)
    (lbl_stmt:lbl_stmt)
    (post_normal:temp_env -> mem -> Prop)
    (post_return:val -> mem -> Prop)
    (post_exit:nat -> temp_env -> mem -> Prop)
    (post_goto:ident -> temp_env -> mem -> Prop), Prop :=

| hoare_LSnil:
  ∀ env pre_case pre_default pre_fallthrough pre_label
    post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_default le mem:Prop) -> (post_normal le mem:Prop)) ->
    (∀ le mem, (pre_fallthrough le mem:Prop) -> (post_normal le mem:Prop)) ->
    hoare_lbl_stmt env
                   pre_case pre_default pre_fallthrough pre_label
                   LSnil
                   post_normal post_return post_exit post_goto

| hoare_LScons:
  ∀ lbl s ls env pre_case pre_default pre_fallthrough pre_label
    P post_normal post_return post_exit post_goto,

    hoare_stmt env
               (fun le mem =>
                  match lbl with
                  | None => pre_default le mem
                  | Some n => pre_case n le mem
                  end \/ pre_fallthrough le mem) pre_label
               s
               P post_return post_exit post_goto ->

    hoare_lbl_stmt env
                   pre_case
                   (match lbl with
                    | None => fun _ _ => False
                    | Some _ => pre_default
                   end)
                   P pre_label
                   ls
                   post_normal post_return post_exit post_goto ->

    hoare_lbl_stmt env
                   pre_case pre_default pre_fallthrough pre_label
                   (LScons lbl s ls)
                   post_normal post_return post_exit post_goto

with hoare_fun :
       ∀ (pre:list val -> mem -> Prop)
         (f:fundef)
         (post:val -> mem -> Prop), Prop :=

| hoare_Internal:
  ∀ f pre post,
    (∀ vargs mem, (pre vargs mem:Prop) ->
     list_norepet (map fst f.(fn_vars)) /\
     list_norepet f.(fn_params) /\
     list_disjoint f.(fn_params) f.(fn_temps) /\
     ∃ mem1 env le,
       alloc_variables empty_env mem f.(fn_vars) env mem1 /\
       bind_parameters f.(fn_params) vargs
                       (create_undef_temps f.(fn_temps)) = Some le /\
       ∃ inv,
         (∀ lbl le mem, (inv lbl le mem:Prop) -> ∀ k, find_label lbl (fn_body f) k <> None) /\
         hoare_stmt env
                    (fun le' mem' => le' = le /\ mem' = mem1) inv
                    (fn_body f)
                    (fun le mem =>
                       ∃ mem',
                         Mem.free_list mem (blocks_of_env env) = Some mem' /\
                         post Vundef mem') post
                    (fun _ _ _ => False) inv) ->
    hoare_fun pre
              (Internal f)
              post
| hoare_External:
  ∀ ef pre post,
    (∀ vargs mem, (pre vargs mem:Prop) ->
                  (∃ t v mem', external_call ef ge vargs mem t v mem') /\
                  ∀ t v mem', external_call ef ge vargs mem t v mem' ->
                              (post v mem':Prop)) ->
    hoare_fun pre
              (External ef)
              post.

Lemma hoare_stmt_pre_impl:
  ∀ env
    pre_normal pre_label post_normal post_return post_exit post_goto
    pre_normal' pre_label',
    (∀ le mem, (pre_normal' le mem:Prop) -> (pre_normal le mem:Prop)) ->
    (∀ lbl le mem, (pre_label' lbl le mem:Prop) -> (pre_label lbl le mem:Prop)) ->
  ∀ stmt,
    hoare_stmt env pre_normal pre_label stmt post_normal post_return post_exit post_goto ->
    hoare_stmt env pre_normal' pre_label' stmt post_normal post_return post_exit post_goto

with hoare_lbl_stmt_pre_impl:
  ∀ env
    pre_case pre_default pre_fallthrough pre_label post_normal post_return post_exit post_goto
    pre_case' pre_default' pre_fallthrough' pre_label',
    (∀ i le mem, (pre_case' i le mem:Prop) -> (pre_case i le mem:Prop)) ->
    (∀ le mem, (pre_default' le mem:Prop) -> (pre_default le mem:Prop)) ->
    (∀ le mem, (pre_fallthrough' le mem:Prop) -> (pre_fallthrough le mem:Prop)) ->
    (∀ lbl le mem, (pre_label' lbl le mem:Prop) -> (pre_label lbl le mem:Prop)) ->
  ∀ stmt,
    hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label stmt post_normal post_return post_exit post_goto ->
    hoare_lbl_stmt env pre_case' pre_default' pre_fallthrough' pre_label' stmt post_normal post_return post_exit post_goto

with hoare_fun_pre_impl:
  ∀ pre pre' post,
    (∀ args mem, (pre' args mem:Prop) -> (pre args mem:Prop)) ->
  ∀ f,
    hoare_fun pre f post ->
    hoare_fun pre' f post.

Lemma hoare_stmt_post_impl:
  ∀ env
    pre_normal pre_label post_normal post_return post_exit post_goto
    post_normal' post_return' post_exit' post_goto',
    (∀ le mem, (post_normal le mem:Prop) -> (post_normal' le mem:Prop)) ->
    (∀ v mem, (post_return v mem:Prop) -> (post_return' v mem:Prop)) ->
    (∀ x le mem, (post_exit x le mem:Prop) -> (post_exit' x le mem:Prop)) ->
    (∀ lbl le mem, (post_goto lbl le mem:Prop) -> (post_goto' lbl le mem:Prop)) ->
  ∀ stmt,
    hoare_stmt env pre_normal pre_label stmt post_normal post_return post_exit post_goto ->
    hoare_stmt env pre_normal pre_label stmt post_normal' post_return' post_exit' post_goto'

with hoare_lbl_stmt_post_impl:
  ∀ env
    pre_case pre_default pre_fallthrough pre_label post_normal post_return post_exit post_goto
    post_normal' post_return' post_exit' post_goto',
    (∀ le mem, (post_normal le mem:Prop) -> (post_normal' le mem:Prop)) ->
    (∀ v mem, (post_return v mem:Prop) -> (post_return' v mem:Prop)) ->
    (∀ x le mem, (post_exit x le mem:Prop) -> (post_exit' x le mem:Prop)) ->
    (∀ lbl le mem, (post_goto lbl le mem:Prop) -> (post_goto' lbl le mem:Prop)) ->
  ∀ stmt,
    hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label stmt post_normal post_return post_exit post_goto ->
    hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label stmt post_normal' post_return' post_exit' post_goto'

with hoare_fun_post_impl:
  ∀ pre post post',
    (∀ val mem, (post val mem:Prop) -> (post' val mem:Prop)) ->
  ∀ f,
    hoare_fun pre f post ->
    hoare_fun pre f post'.

Lemma hoare_stmt_wp_aux:
  ∀ stmt env pre_normal pre_label post_normal post_return post_exit post_goto,
    (∀ le mem, (pre_normal le mem:Prop) ->
       ∃ P, P le mem /\
            hoare_stmt env P (fun _ _ _ => False) stmt
                       post_normal post_return post_exit post_goto) ->
    (∀ lbl le mem, (pre_label lbl le mem:Prop) ->
       ∃ P, P lbl le mem /\
            hoare_stmt env (fun _ _ => False) P stmt
                       post_normal post_return post_exit post_goto) ->
    hoare_stmt env pre_normal pre_label
               stmt post_normal post_return post_exit post_goto
with hoare_lbl_stmt_wp_aux:
  ∀ lbl_stmt env pre_case pre_default pre_fallthrough pre_label
    post_normal post_return post_exit post_goto,
    (∀ n le mem, (pre_case n le mem:Prop) ->
       ∃ P, P n le mem /\
            hoare_lbl_stmt env P (fun _ _ => False) (fun _ _ => False) (fun _ _ _ => False)
                           lbl_stmt
                           post_normal post_return post_exit post_goto) ->
    (∀ le mem, (pre_default le mem:Prop) ->
       ∃ P, P le mem /\
            hoare_lbl_stmt env (fun _ _ _ => False) P (fun _ _ => False) (fun _ _ _ => False)
                           lbl_stmt
                           post_normal post_return post_exit post_goto) ->
    (∀ le mem, (pre_fallthrough le mem:Prop) ->
       ∃ P, P le mem /\
            hoare_lbl_stmt env (fun _ _ _ => False) (fun _ _ => False) P (fun _ _ _ => False)
                           lbl_stmt
                           post_normal post_return post_exit post_goto) ->
    (∀ lbl le mem, (pre_label lbl le mem:Prop) ->
       ∃ P, P lbl le mem /\
            hoare_lbl_stmt env (fun _ _ _ => False) (fun _ _ => False) (fun _ _ => False) P
                           lbl_stmt
                           post_normal post_return post_exit post_goto) ->
    hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label
                   lbl_stmt post_normal post_return post_exit post_goto.

Lemma hoare_stmt_wp:
  ∀ stmt env post_normal post_return post_exit post_goto,
    hoare_stmt env
               (fun le mem =>
                  ∃ P, P le mem /\
                       hoare_stmt env P (fun _ _ _ => False) stmt
                                  post_normal post_return post_exit post_goto)
               (fun lbl le mem =>
                  ∃ P, P lbl le mem /\
                       hoare_stmt env (fun _ _ => False) P stmt
                                  post_normal post_return post_exit post_goto)
               stmt post_normal post_return post_exit post_goto.

Lemma hoare_fun_wp:
  ∀ f post,
    hoare_fun (fun args mem => ∃ P, P args mem /\ hoare_fun P f post) f post.

Lemma hoare_stmt_pre_exists:
  ∀ T stmt env pre_normal pre_label post_normal post_return post_exit post_goto,
    (∀ x:T, hoare_stmt env (pre_normal x) (pre_label x)
                       stmt post_normal post_return post_exit post_goto) ->
    hoare_stmt env (fun le mem => ∃ x, pre_normal x le mem)
               (fun lbl le mem => ∃ x, pre_label x lbl le mem)
               stmt post_normal post_return post_exit post_goto.

Lemma hoare_stmt_pre_or:
  ∀ stmt env pre_normal1 pre_normal2 pre_label1 pre_label2
    post_normal post_return post_exit post_goto,
    hoare_stmt env pre_normal1 pre_label1
               stmt post_normal post_return post_exit post_goto ->
    hoare_stmt env pre_normal2 pre_label2
               stmt post_normal post_return post_exit post_goto ->
    hoare_stmt env (fun le mem => pre_normal1 le mem \/ pre_normal2 le mem)
               (fun lbl le mem => pre_label1 lbl le mem \/ pre_label2 lbl le mem)
               stmt post_normal post_return post_exit post_goto.

Lemma hoare_fun_pre_exists:
  ∀ T f pre post,
    (∀ x:T, hoare_fun (pre x) f post) ->
    hoare_fun (fun vargs mem => ∃ x, pre x vargs mem) f post.

Lemma hoare_fun_pre_or:
  ∀ f pre1 pre2 post,
    hoare_fun pre1 f post ->
    hoare_fun pre2 f post ->
    hoare_fun (fun vargs mem => pre1 vargs mem \/ pre2 vargs mem) f post.

Lemma hoare_stmt_sp_aux:
  ∀ stmt env pre_normal pre_label post_normal0 post_return0 post_exit0 post_goto0,
    hoare_stmt env pre_normal pre_label stmt post_normal0 post_return0 post_exit0 post_goto0 ->
  ∀ post_normal post_return post_exit post_goto,
    (∀ le mem, (∀ P, hoare_stmt env pre_normal pre_label stmt
                               P (fun _ _ => True)
                               (fun _ _ _ => True) (fun _ _ _ => True) ->
                     P le mem) ->
               (post_normal le mem:Prop)) ->
    (∀ v mem, (∀ P, hoare_stmt env pre_normal pre_label stmt
                               (fun _ _ => True) P
                               (fun _ _ _ => True) (fun _ _ _ => True) ->
                     P v mem) ->
               (post_return v mem:Prop)) ->
    (∀ x le mem, (∀ P, hoare_stmt env pre_normal pre_label stmt
                                 (fun _ _ => True) (fun _ _ => True)
                                 P (fun _ _ _ => True) ->
                       P x le mem) ->
                 (post_exit x le mem:Prop)) ->
    (∀ lbl le mem, (∀ P, hoare_stmt env pre_normal pre_label stmt
                                    (fun _ _ => True) (fun _ _ => True)
                                    (fun _ _ _ => True) P ->
                         P lbl le mem) ->
                   (post_goto lbl le mem:Prop)) ->
    hoare_stmt env pre_normal pre_label stmt
               post_normal post_return post_exit post_goto

with hoare_lbl_stmt_sp_aux:
 ∀ lbl_stmt env pre_case pre_default pre_fallthrough pre_label
   post_normal0 post_return0 post_exit0 post_goto0,
   hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label lbl_stmt
                  post_normal0 post_return0 post_exit0 post_goto0 ->
 ∀ post_normal post_return post_exit post_goto,
   (∀ le mem, (∀ P, hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label lbl_stmt
                                   P (fun _ _ => True)
                                   (fun _ _ _ => True) (fun _ _ _ => True) ->
                    P le mem) ->
              (post_normal le mem:Prop)) ->
   (∀ v mem, (∀ P, hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label lbl_stmt
                                   (fun _ _ => True) P
                                   (fun _ _ _ => True) (fun _ _ _ => True) ->
                    P v mem) ->
              (post_return v mem:Prop)) ->
   (∀ x le mem, (∀ P, hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label lbl_stmt
                                     (fun _ _ => True) (fun _ _ => True)
                                     P (fun _ _ _ => True) ->
                      P x le mem) ->
                (post_exit x le mem:Prop)) ->
   (∀ lbl le mem, (∀ P, hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label lbl_stmt
                                       (fun _ _ => True) (fun _ _ => True)
                                       (fun _ _ _ => True) P ->
                        P lbl le mem) ->
                  (post_goto lbl le mem:Prop)) ->
   hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label lbl_stmt
                  post_normal post_return post_exit post_goto

with hoare_fun_sp_aux:
  ∀ f pre post0, hoare_fun pre f post0 ->
  ∀ post,
    (∀ v mem, (∀ P, hoare_fun pre f P -> P v mem) ->
              (post v mem:Prop)) ->
    hoare_fun pre f post.

Lemma hoare_stmt_sp:
  ∀ stmt env pre_normal pre_label post_normal post_return post_exit post_goto,
    hoare_stmt env pre_normal pre_label stmt post_normal post_return post_exit post_goto ->
    hoare_stmt env pre_normal pre_label stmt
               (fun le mem =>
                  ∀ P, hoare_stmt env pre_normal pre_label stmt
                                  P (fun _ _ => True)
                                  (fun _ _ _ => True) (fun _ _ _ => True) ->
                       P le mem)
               (fun v mem =>
                  ∀ P, hoare_stmt env pre_normal pre_label stmt
                                  (fun _ _ => True) P
                                  (fun _ _ _ => True) (fun _ _ _ => True) ->
                       P v mem)
               (fun x le mem =>
                  ∀ P, hoare_stmt env pre_normal pre_label stmt
                                  (fun _ _ => True) (fun _ _ => True)
                                  P (fun _ _ _ => True) ->
                       P x le mem)
               (fun lbl le mem =>
                  ∀ P, hoare_stmt env pre_normal pre_label stmt
                                  (fun _ _ => True) (fun _ _ => True)
                                  (fun _ _ _ => True) P ->
                       P lbl le mem).

Lemma hoare_fun_sp:
  ∀ f pre post, hoare_fun pre f post ->
    hoare_fun pre f (fun v mem => ∀ P, hoare_fun pre f P -> P v mem).

Lemma hoare_stmt_post_forall:
  ∀ T stmt env pre_normal pre_label post_normal post_return post_exit post_goto,
    inhabited T ->
    (∀ x:T, hoare_stmt env pre_normal pre_label
                       stmt (post_normal x) (post_return x) (post_exit x) (post_goto x)) ->
    hoare_stmt env pre_normal pre_label stmt
               (fun le mem => ∀ x, post_normal x le mem)
               (fun v mem => ∀ x, post_return x v mem)
               (fun xx le mem => ∀ x, post_exit x xx le mem)
               (fun lbl le mem => ∀ x, post_goto x lbl le mem).

Lemma hoare_stmt_post_and:
  ∀ stmt env pre_normal pre_label
    post_normal1 post_normal2 post_return1 post_return2 post_exit1 post_exit2 post_goto1 post_goto2,
    hoare_stmt env pre_normal pre_label
               stmt post_normal1 post_return1 post_exit1 post_goto1 ->
    hoare_stmt env pre_normal pre_label
               stmt post_normal2 post_return2 post_exit2 post_goto2 ->
    hoare_stmt env pre_normal pre_label stmt
               (fun le mem => post_normal1 le mem /\ post_normal2 le mem)
               (fun v mem => post_return1 v mem /\ post_return2 v mem)
               (fun x le mem => post_exit1 x le mem /\ post_exit2 x le mem)
               (fun lbl le mem => post_goto1 lbl le mem /\ post_goto2 lbl le mem).

Lemma hoare_fun_post_forall:
  ∀ T f pre post,
    inhabited T ->
    (∀ x:T, hoare_fun pre f (post x)) ->
    hoare_fun pre f (fun mem v => ∀ x, post x mem v).

Lemma hoare_fun_post_and:
  ∀ f pre post1 post2,
    hoare_fun pre f post1 ->
    hoare_fun pre f post2 ->
    hoare_fun pre f (fun mem v => post1 mem v /\ post2 mem v).

Definition safe k s :=
  ∀ tr s' k',
    starN step ge k' s tr s' ->
    Nostep (semantics prog) s' ->
    (∀ r, ¬final_state s' r) ->
    (k <= k')%nat.

Lemma safe_step:
  ∀ s k s' t,
    step ge s t s' ->
    (∀ s' t, step ge s t s' -> safe k s') ->
    safe (S k) s.

Ltac safe_step :=
  lazymatch goal with
    | |- safe (S ?k) ?st =>
      eapply safe_step; [now (econstructor; eauto) | ];
      let s' := fresh "s'" in
      let tr := fresh "tr" in
      let Hs' := fresh "Hs'" in
      intros s' tr Hs'; inv Hs'; try contradiction; [];
      determ
    | |- safe ?k ?st =>
      destruct k; [repeat intro; apply le_0_n|safe_step]
  end.

Lemma safe_le:
  ∀ s k k', safe k s -> (k' <= k)%nat -> safe k' s.

Hint Resolve safe_le.
Local Hint Extern 1 (_ <= _)%nat => omega.
Local Hint Extern 1 (_ < _)%nat => omega.

Definition hoare_stmt_sem
           (fuel:nat)
           (env:env)
           (pre_normal:temp_env -> mem -> Prop)
           (pre_label:ident -> temp_env -> mem -> Prop)
           (stmt:stmt)
           (post_normal:temp_env -> mem -> Prop)
           (post_return:val -> mem -> Prop)
           (post_exit:nat -> temp_env -> mem -> Prop)
           (post_goto:ident -> temp_env -> mem -> Prop) : Prop :=
  ∀ f k,
    (∀ le' mem', post_normal le' mem' ->
                 safe fuel (State f Sskip k env le' mem')) ->

    (∀ mem' v, post_return v mem' ->
               safe fuel (Returnstate v (call_cont k) mem')) ->

    (∀ le' mem' x, post_exit x le' mem' ->
                   safe fuel (State f (Sexit x) k env le' mem')) ->

    (∀ le' mem' k' lbl, post_goto lbl le' mem' ->
                        call_cont k = call_cont k' ->
                        safe fuel (State f (Sgoto lbl) k' env le' mem')) ->

    (∀ le mem, pre_normal le mem -> safe fuel (State f stmt k env le mem)) /\
    (∀ le mem lbl s' k', find_label lbl stmt k = Some (s', k') ->
                         pre_label lbl le mem ->
                         safe fuel (State f s' k' env le mem)).

Definition hoare_fun_sem
           (fuel:nat)
           (pre:list val -> mem -> Prop)
           (f:fundef)
           (post:val -> mem -> Prop) :=
  ∀ k, is_call_cont k ->

    (∀ mem' v, post v mem' ->
               safe fuel (Returnstate v k mem')) ->

    ∀ args mem,
      pre args mem -> safe fuel (Callstate f args k mem).

Definition hoare_lbl_stmt_sem (fuel:nat)
           (env:env)
           (pre_case:Z -> temp_env -> mem -> Prop)
           (pre_default:temp_env -> mem -> Prop)
           (pre_fallthrough:temp_env -> mem -> Prop)
           (pre_label:ident -> temp_env -> mem -> Prop)
           (lbl_stmt:lbl_stmt)
           (post_normal:temp_env -> mem -> Prop)
           (post_return:val -> mem -> Prop)
           (post_exit:nat -> temp_env -> mem -> Prop)
           (post_goto:ident -> temp_env -> mem -> Prop)
           : Prop :=
  ∀ f k,
    (∀ le' mem', post_normal le' mem' ->
                 safe fuel (State f Sskip k env le' mem')) ->

    (∀ mem' v, post_return v mem' ->
               safe fuel (Returnstate v (call_cont k) mem')) ->

    (∀ le' mem' x, post_exit x le' mem' ->
                   safe fuel (State f (Sexit x) k env le' mem')) ->

    (∀ le' mem' k' lbl, post_goto lbl le' mem' ->
                        call_cont k = call_cont k' ->
                        safe fuel (State f (Sgoto lbl) k' env le' mem')) ->

    (∀ le mem n lbl_stmt', pre_case n le mem ->
       select_switch_case n lbl_stmt = Some lbl_stmt' ->
       safe fuel (State f (seq_of_lbl_stmt lbl_stmt') k env le mem)) /\
    (∀ le mem, pre_default le mem ->
       safe fuel (State f (seq_of_lbl_stmt (select_switch_default lbl_stmt)) k env le mem)) /\
    (∀ le mem, pre_fallthrough le mem ->
       safe fuel (State f (seq_of_lbl_stmt lbl_stmt) k env le mem)) /\
    (∀ le mem lbl s' k', find_label_ls lbl lbl_stmt k = Some (s', k') ->
                  pre_label lbl le mem ->
                  safe fuel (State f s' k' env le mem)).

Scheme stmt_ind_2 := Induction for stmt Sort Prop
  with lbl_stmt_ind_2 := Induction for lbl_stmt Sort Prop.
Combined Scheme stmt_lbl_stmt_ind from stmt_ind_2, lbl_stmt_ind_2.

Lemma hoare_correct_aux:
  ∀ fuel,
    (∀ env,
        (∀ stmt pre_normal pre_label post_normal post_return post_exit post_goto,
          hoare_stmt env pre_normal pre_label stmt
                     post_normal post_return post_exit post_goto ->
          hoare_stmt_sem fuel env pre_normal pre_label stmt
                         post_normal post_return post_exit post_goto) /\
        (∀ lbl_stmt pre_case pre_default pre_fallthrough pre_label
           post_normal post_return post_exit post_goto,
            hoare_lbl_stmt env pre_case pre_default pre_fallthrough pre_label
                           lbl_stmt
                           post_normal post_return post_exit post_goto ->
            hoare_lbl_stmt_sem fuel env pre_case pre_default pre_fallthrough pre_label
                               lbl_stmt
                               post_normal post_return post_exit post_goto)) /\
    (∀ pre f post,
       hoare_fun pre f post ->
       hoare_fun_sem fuel pre f post).

Lemma hoare_stmt_correct:
  ∀ env stmt pre_normal pre_label post_normal post_return post_exit post_goto,
    hoare_stmt env pre_normal pre_label stmt
               post_normal post_return post_exit post_goto ->
    ∀ fuel, hoare_stmt_sem fuel env pre_normal pre_label stmt
                           post_normal post_return post_exit post_goto.

Lemma hoare_fun_correct:
  ∀ pre f post,
    hoare_fun pre f post ->
    ∀ fuel, hoare_fun_sem fuel pre f post.

Lemma hoare_prog:
  ∀ f b mem,
    Genv.find_symbol ge (prog_main prog) = Some b ->
    Genv.find_funct_ptr ge b = Some f ->
    funsig f = signature_main ->
    Genv.init_mem prog = Some mem ->
    hoare_fun (fun vargs mem' => vargs = nil /\ mem' = mem)
              f
              (fun v mem => ∃ r, v = Vint r) ->
    ∀ tr, program_behaves (semantics prog) (Goes_wrong tr) ->
          False.


Lemma hoare_loop_pre_unroll:
  ∀ env s,
  ∀ pre_normal pre_label P
    post_normal post_return post_exit post_goto,
    hoare_stmt env
               pre_normal pre_label
               s
               P post_return post_exit post_goto ->
    hoare_stmt env
               P (fun _ _ _ => False)
               (Sloop s)
               post_normal post_return post_exit post_goto ->
    hoare_stmt env
               pre_normal pre_label
               (Sloop s)
               post_normal post_return post_exit post_goto.

Definition loop_unstable_invariant
           env inv pre_normal pre_label s post_return post_exit post_goto :=
  ∃ inv',
    (∀ le mem, (inv' le mem:Prop) -> (inv le mem:Prop)) /\
    (∀ le mem, (pre_normal le mem:Prop) -> (inv' le mem:Prop)) /\
    hoare_stmt env inv' pre_label s inv' post_return post_exit post_goto.

Lemma hoare_Sloop_unstable:
  ∀ env s inv pre_normal pre_label post_normal post_return post_exit post_goto,
    loop_unstable_invariant env
                            inv pre_normal pre_label
                            s
                            post_return post_exit post_goto ->
    hoare_stmt env
               pre_normal pre_label
               (Sloop s)
               post_normal post_return post_exit post_goto.

Lemma loop_unstable_invariant_seq:
  ∀ env s inv inv' pre_normal pre_label
    post_return post_exit post_goto post_return' post_exit' post_goto',
    loop_unstable_invariant env
                            inv pre_normal pre_label
                            s
                            post_return post_exit post_goto ->
    hoare_stmt env
               inv pre_label
               s
               inv' post_return' post_exit' post_goto' ->
    (∀ le mem, pre_normal le mem -> inv' le mem) ->
    loop_unstable_invariant env
                            inv' pre_normal pre_label
                            s
                            post_return' post_exit' post_goto'.

End PROG.