Changeset 2227


Ignore:
Timestamp:
Jul 20, 2012, 8:28:57 PM (7 years ago)
Author:
garnier
Message:
  • New version of the switch removal algorithm, described at the top of the file.
  • Memory injections (in a slightly weaker form than in Compcert, sufficient for this file) and related lemmas
  • Ongoing: proof of semantics preservation for expression evaluation under memory injections. Progressively

port old proofs to the new setting.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2076 r2227  
    1 include "Clight/Csyntax.ma".
     1 include "Clight/Csyntax.ma".
    22include "Clight/fresh.ma".
    33include "basics/lists/list.ma".
     
    55include "Clight/Cexec.ma".
    66include "Clight/CexecInd.ma".
     7include "Clight/frontend_misc.ma".
     8(*
     9include "Clight/maps_obsequiv.ma".
     10*)
     11
    712
    813(* -----------------------------------------------------------------------------
     
    6166(* -----------------------------------------------------------------------------
    6267   Definitions allowing to state that the program resulting of the transformation
    63    is switch-free. The actual proof is done using Russell.
    64    ----------------------------------------------------------------------------*)
     68   is switch-free.
     69   ---------------------------------------------------------------------------- *)
    6570
    6671(* Property of a Clight statement of containing no switch. Could be generalized into a kind of
     
    8590].
    8691
    87 definition sf_statement ≝ Σs:statement. switch_free s.
    88 
    89 definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement).
    90 
    9192(* Property of a list of labeled statements of being switch-free *)
    9293let rec branches_switch_free (sts : labeled_statements) : Prop ≝
    9394match sts with
    94 [ LSdefault st => 
     95[ LSdefault st =>
    9596  switch_free st
    9697| LScase _ _ st tl =>
     
    9899].
    99100
    100 let rec branch_switch_free_ind
     101let rec branches_ind
    101102  (sts : labeled_statements)
    102103  (H   : labeled_statements → Prop) 
     
    107108  defcase st
    108109| LScase sz int st tl ⇒
    109   indcase sz int st tl (branch_switch_free_ind tl H defcase indcase)
     110  indcase sz int st tl (branches_ind tl H defcase indcase)
    110111].
    111 
    112112
    113113(* -----------------------------------------------------------------------------
    114114   Switch-removal code for statements, functions and fundefs.
    115115   ----------------------------------------------------------------------------*)
    116 
    117 (* Given a list of switch cases, prefixes each case by a fresh goto label. It is
    118    assumed as an hypothesis that each sub-statement is already switch-free
    119    (argument [H]). The whole function returns a list of labelled switch-free switch
    120    cases, along the particular label of the default statement and its associated
    121    statement. A fresh label generator [uv] is threaded through the function.  *)
    122 let rec add_starting_lbl_list
    123   (l : labeled_statements) 
    124   (H : branches_switch_free l)
    125   (uv : universe SymbolTag)
    126   (acc : stlist) : stlist × (label × sf_statement) × (universe SymbolTag) ≝
    127 match l return λl'. l = l' → stlist × (label × sf_statement) × (universe SymbolTag) with
    128 [ LSdefault st ⇒ λEq.
    129   let 〈default_lab, uv'〉 ≝ fresh ? uv in
    130   〈rev ? acc, 〈default_lab, «st, ?»〉, uv'〉
    131 | LScase sz tag st other_cases ⇒ λEq.
    132   let 〈lab, uv'〉 ≝ fresh ? uv in
    133   let acc' ≝ 〈lab, (mk_DPair ?? sz tag), «st, ?»〉 :: acc in
    134   add_starting_lbl_list other_cases ? uv' acc'
    135 ] (refl ? l).
    136 [ 1: destruct whd in H; //
    137 | 2: letin H1 ≝ H >Eq in H1;
    138   #H' normalize in H'; elim H' //
    139 | 3: >Eq in H; normalize * //
    140 ] qed.
    141116
    142117(* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
     
    170145
    171146(* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)
     147(*
    172148let rec produce_cond
    173149  (e : expr)
     
    203179  [ 1: @convert_break_lift elim case_statement //
    204180  | 2: elim sub_statement // ]
    205 ] qed.
     181] qed. *)
    206182
    207183(* We assume that the expression e is consistely typed w.r.t. the switch branches *)
     184(*
    208185let rec produce_cond2
    209186  (e : expr)
     
    237214          | 2: // ]
    238215     | 2: elim sub_statement // ]
    239 ] qed.     
    240 
    241 (* takes an expression, a list of switch-free cases and a freshgen and returns a
    242  * switch-free equivalent, along an updated freshgen and a new local variable
    243  * (for storing the value of the expr). *)
    244 definition simplify_switch :
    245   expr → ∀l:labeled_statements. branches_switch_free l → (universe SymbolTag) → sf_statement × (universe SymbolTag) ≝
    246 λe.λswitch_cases.λH.λuv.
     216] qed. *)
     217
     218(*  (def_case : ident × sf_statement) *)
     219
     220let rec produce_cond
     221  (e : expr)
     222  (switch_cases : labeled_statements)
     223  (u : universe SymbolTag)
     224  (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝
     225match switch_cases with
     226[ LSdefault st ⇒ 
     227  let 〈lab,u1〉 ≝ fresh ? u in
     228  let st' ≝ convert_break_to_goto st exit in
     229  〈Slabel lab st', lab, u1〉
     230| LScase sz tag st other_cases ⇒
     231  let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in
     232  let st' ≝ convert_break_to_goto st exit in
     233  let 〈lab, u2〉 ≝ fresh ? u1 in
     234  let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in
     235  let case_statement ≝
     236       Sifthenelse test
     237        (Slabel lab (Ssequence st' (Sgoto sub_label)))
     238        Sskip
     239  in
     240  〈Ssequence case_statement sub_statements, lab, u2〉
     241].
     242
     243definition simplify_switch ≝
     244   λ(e : expr).
     245   λ(switch_cases : labeled_statements).
     246   λ(uv : universe SymbolTag).
    247247 let 〈exit_label, uv1〉            ≝ fresh ? uv in
    248  let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in
    249  let 〈result, useless_label〉      ≝ produce_cond2 e switch_cases defcase exit_label in
    250  〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉.
    251 [ 1:  normalize try @conj try @conj try // elim result //
    252 | 2: @H ]
    253 qed.
    254 
    255 (* recursively convert a statement into a switch-free one. *)
    256 let rec switch_removal
    257   (st : statement)
    258   (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
    259 match st return λs.s = st → ? with
    260 [ Sskip       ⇒ λEq. 〈«st,?», [ ], uv〉
    261 | Sassign _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
    262 | Scall _ _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
    263 | Ssequence s1 s2 ⇒ λEq.
    264   let 〈s1', vars1, uv'〉  ≝ switch_removal s1 uv in
    265   let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in
    266   〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉
    267 | Sifthenelse e s1 s2 ⇒ λEq.
    268   let 〈s1', vars1, uv'〉  ≝ switch_removal s1 uv in
    269   let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in
    270   〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉
    271 | Swhile e body ⇒ λEq.
    272   let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    273   〈«Swhile e (pi1 … body'),?», vars', uv'〉
    274 | Sdowhile e body ⇒ λEq.
    275   let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    276   〈«Sdowhile e (pi1 … body'),?», vars', uv'〉
    277 | Sfor s1 e s2 s3 ⇒ λEq.
    278   let 〈s1', vars1, uv'〉   ≝ switch_removal s1 uv in
    279   let 〈s2', vars2, uv''〉  ≝ switch_removal s2 uv' in
    280   let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 uv'' in
    281   〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars1 @ vars2 @ vars3, uv'''〉
    282 | Sbreak ⇒ λEq.
    283   〈«st,?», [ ], uv〉
    284 | Scontinue ⇒ λEq.
    285   〈«st,?», [ ], uv〉
    286 | Sreturn _ ⇒ λEq.
    287   〈«st,?», [ ], uv〉
    288 | Sswitch e branches ⇒ λEq.
    289    let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches uv in
    290    match sf_branches with
    291    [ mk_Sig branches' H ⇒
    292      let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in
    293      let ident             ≝ Expr (Evar switch_tmp) (typeof e) in
    294      let assign            ≝ Sassign ident e in     
    295      let 〈result, uv3〉     ≝ simplify_switch ident branches' H uv2 in
    296      〈«Ssequence assign (pi1 … result), ?», (〈switch_tmp, typeof e〉 :: vars'), uv3〉
     248 let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in
     249 〈Ssequence result (Slabel exit_label Sskip), uv2〉.
     250
     251lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))).
     252#l @(labeled_statements_ind … l)
     253[ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1
     254     normalize in Hsf ⊢ %; @(convert_break_lift … Hsf)
     255| 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl
     256     #e #lab #u normalize
     257     lapply (Hind Hsf_tl e lab u)
     258     cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta
     259     cases (fresh ??) #lab0 #u2 normalize nodelta
     260     normalize try @conj try @conj try @conj try //
     261     @(convert_break_lift … Hsf_hd)
     262] qed.
     263
     264lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)).
     265#e #l cases l
     266[ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta
     267     whd @conj whd
     268     [ 1: @convert_break_lift assumption
     269     | 2: @I ]
     270| 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u
     271     cases (fresh ? u) #exit_label #uv1 normalize nodelta
     272     lapply (produce_cond_switch_free tl Hsftl e exit_label uv1)
     273     cases (produce_cond e tl uv1 exit_label)
     274     * #cond #lab #u1 #Hsf_cond normalize nodelta
     275     cases (fresh ??) #lab0 #u2 normalize nodelta
     276     normalize @conj try @conj try @conj try @conj try //
     277     @(convert_break_lift ?? Hsf)
     278] qed.
     279
     280(* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in
     281   order to circumvent the associativity problems in notations. *)
     282record swret (A : Type[0]) : Type[0] ≝ {
     283  ret_st  : A;
     284  ret_acc : list (ident × type);
     285  ret_fvs : list ident;
     286  ret_u   : universe SymbolTag
     287}.
     288
     289notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48
     290for @{ match ${e} with
     291       [ None ⇒ None ?
     292       | Some ${fresh ret} ⇒
     293          (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'})
     294          (ret_st ? ${fresh ret})
     295          (ret_acc ? ${fresh ret})
     296          (ret_fvs ? ${fresh ret})
     297          (ret_u ? ${fresh ret}) ] }.
     298
     299notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49
     300for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4})  }.
     301     
     302(* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
     303   of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another
     304   'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables
     305   allows it to proceed without failing. This is all in order to ease the proof of simulation. *)
     306let rec switch_removal
     307  (st : statement)           (* the statement in which we will remove switches *)
     308  (fvs : list ident)         (* a finite list of names usable to create variables. *)
     309  (u : universe SymbolTag)   (* a fresh /label/ generator *)
     310  : option (swret statement) ≝
     311match st with
     312[ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
     313| Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
     314| Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉
     315| Ssequence s1 s2 ⇒
     316  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
     317  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
     318  ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉
     319| Sifthenelse e s1 s2 ⇒
     320  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
     321  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
     322  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
     323| Swhile e body ⇒
     324  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     325  ret 〈Swhile e body', acc, fvs', u'〉
     326| Sdowhile e body ⇒
     327  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     328  ret 〈Sdowhile e body', acc, fvs', u'〉
     329| Sfor s1 e s2 s3 ⇒
     330  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
     331  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
     332  do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
     333  ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
     334| Sbreak ⇒
     335  ret 〈st, [ ], fvs, u〉
     336| Scontinue ⇒
     337  ret 〈st, [ ], fvs, u〉
     338| Sreturn _ ⇒
     339  ret 〈st, [ ], fvs, u〉
     340| Sswitch e branches ⇒   
     341   do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u;
     342   match fvs' with
     343   [ nil ⇒ None ?
     344   | cons fresh tl ⇒
     345     (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *)
     346     let ident         ≝ Expr (Evar fresh) (typeof e) in
     347     let assign        ≝ Sassign ident e in
     348     let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in
     349       ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉
    297350   ]
    298 | Slabel label body ⇒ λEq.
    299   let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    300   〈«Slabel label (pi1 … body'), ?», vars', uv'〉
    301 | Sgoto _ ⇒ λEq.
    302   〈«st, ?», [ ], uv
    303 | Scost cost body ⇒ λEq.
    304   let 〈body', vars', uv'〉 ≝ switch_removal body uv in
    305   〈«Scost cost (pi1 … body'),?», vars', uv'〉
    306 ] (refl ? st)
     351| Slabel label body ⇒
     352  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     353  ret 〈Slabel label body', acc, fvs', u'〉
     354| Sgoto _ ⇒
     355  ret 〈st, [ ], fvs, u
     356| Scost cost body ⇒
     357  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     358  ret 〈Scost cost body', acc, fvs', u'〉
     359]
    307360
    308361and switch_removal_branches
    309362  (l : labeled_statements)
    310   (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝
     363  (fvs : list ident)
     364  (u : universe SymbolTag)
     365(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
    311366match l with
    312367[ LSdefault st ⇒
    313   let 〈st, vars',  uv'〉 ≝ switch_removal st uv in
    314   〈«LSdefault (pi1 … st), ?», vars', uv'〉
     368  do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
     369  ret 〈LSdefault st', acc1, fvs', u'〉
    315370| LScase sz int st tl =>
    316   let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl uv in
    317   let 〈st', vars'', uv''〉     ≝ switch_removal st uv' in
    318   〈«LScase sz int st' (pi1 … tl_result), ?», vars' @ vars'', uv''〉
     371  do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u;
     372  do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u';
     373  ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉
    319374].
    320 try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try //
    321 [ 1: #st1 #H1 #st2 #H2 #st3 #H3 @conj //
    322 | 2: elim result //
    323 | 3: elim st //
    324 | 4: elim st' //
    325 | 5: elim tl_result //
     375
     376let rec mk_fresh_variables
     377  (st : statement)           (* the statement in which we will remove switches *)
     378  (u : universe SymbolTag)   (* a fresh /label/ generator *)
     379  : (list ident) × (universe SymbolTag) ≝
     380match st with
     381[ Sskip       ⇒ 〈[ ], u〉
     382| Sassign _ _ ⇒ 〈[ ], u〉
     383| Scall _ _ _ ⇒ 〈[ ], u〉
     384| Ssequence s1 s2 ⇒
     385  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
     386  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
     387  〈fvs @ fvs', u''〉
     388| Sifthenelse e s1 s2 ⇒
     389  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
     390  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
     391  〈fvs @ fvs', u''〉
     392| Swhile e body ⇒
     393  mk_fresh_variables body u
     394| Sdowhile e body ⇒
     395  mk_fresh_variables body u
     396| Sfor s1 e s2 s3 ⇒
     397  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
     398  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
     399  let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
     400  〈fvs @ fvs' @fvs'', u'''〉
     401| Sbreak ⇒
     402  〈[ ], u〉
     403| Scontinue ⇒
     404  〈[ ], u〉
     405| Sreturn _ ⇒
     406  〈[ ], u〉
     407| Sswitch e branches ⇒   
     408   let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *)
     409   let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in
     410   〈fvs @ [ident], u''〉  (* reversing the order to match a proof invariant *)
     411| Slabel label body ⇒
     412  mk_fresh_variables body u
     413| Sgoto _ ⇒
     414  〈[ ], u〉
     415| Scost cost body ⇒
     416  mk_fresh_variables body u
     417]
     418
     419and mk_fresh_variables_branches
     420  (l : labeled_statements)
     421  (u : universe SymbolTag)
     422(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
     423match l with
     424[ LSdefault st ⇒
     425  mk_fresh_variables st u
     426| LScase sz int st tl =>
     427  let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in
     428  let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in
     429  〈fvs @ fvs', u''〉
     430].
     431
     432(* Copied this from Csyntax.ma, lifted from Prop to Type
     433   (I needed to eliminate something proved with this towards Type)  *)
     434let rec statement_indT
     435  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
     436  (Ssk:P Sskip)
     437  (Sas:∀e1,e2. P (Sassign e1 e2))
     438  (Sca:∀eo,e,args. P (Scall eo e args))
     439  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
     440  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
     441  (Swh:∀e,s. P s → P (Swhile e s))
     442  (Sdo:∀e,s. P s → P (Sdowhile e s))
     443  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     444  (Sbr:P Sbreak)
     445  (Sco:P Scontinue)
     446  (Sre:∀eo. P (Sreturn eo))
     447  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
     448  (Sla:∀l,s. P s → P (Slabel l s))
     449  (Sgo:∀l. P (Sgoto l))
     450  (Scs:∀l,s. P s → P (Scost l s))
     451  (LSd:∀s. P s → Q (LSdefault s))
     452  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
     453  (s:statement) on s : P s ≝
     454match s with
     455[ Sskip ⇒ Ssk
     456| Sassign e1 e2 ⇒ Sas e1 e2
     457| Scall eo e args ⇒ Sca eo e args
     458| Ssequence s1 s2 ⇒ Ssq s1 s2
     459    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     460    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
     461| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
     462    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     463    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
     464| Swhile e s ⇒ Swh e s
     465    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     466| Sdowhile e s ⇒ Sdo e s
     467    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     468| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
     469    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     470    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
     471    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
     472| Sbreak ⇒ Sbr
     473| Scontinue ⇒ Sco
     474| Sreturn eo ⇒ Sre eo
     475| Sswitch e ls ⇒ Ssw e ls
     476    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
     477| Slabel l s ⇒ Sla l s
     478    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     479| Sgoto l ⇒ Sgo l
     480| Scost l s ⇒ Scs l s
     481    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     482]
     483and labeled_statements_indT
     484  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
     485  (Ssk:P Sskip)
     486  (Sas:∀e1,e2. P (Sassign e1 e2))
     487  (Sca:∀eo,e,args. P (Scall eo e args))
     488  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
     489  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
     490  (Swh:∀e,s. P s → P (Swhile e s))
     491  (Sdo:∀e,s. P s → P (Sdowhile e s))
     492  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     493  (Sbr:P Sbreak)
     494  (Sco:P Scontinue)
     495  (Sre:∀eo. P (Sreturn eo))
     496  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
     497  (Sla:∀l,s. P s → P (Slabel l s))
     498  (Sgo:∀l. P (Sgoto l))
     499  (Scs:∀l,s. P s → P (Scost l s))
     500  (LSd:∀s. P s → Q (LSdefault s))
     501  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
     502  (ls:labeled_statements) on ls : Q ls ≝
     503match ls with
     504[ LSdefault s ⇒ LSd s
     505    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     506| LScase sz i s t ⇒ LSc sz i s t
     507    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     508    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
     509].
     510
     511lemma switch_removal_ok :
     512  ∀st, u0, u1, post.
     513  Σresult.
     514  (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post).
     515#st
     516@(statement_indT ? (λls. ∀u0, u1, post.
     517                          Σresult.
     518                          (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result)
     519                          ∧ (ret_fvs ? result = post)
     520                   ) … st)
     521[ 1: #u0 #u1 #post normalize
     522     %{(mk_swret statement Sskip [] post u1)} % //
     523| 2: #e1 #e2 #u0 #u1 #post normalize
     524     %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try //
     525| 3: #e0 #e #args #u0 #u1 #post normalize
     526     %{(mk_swret statement (Scall e0 e args) [] post u1)} % try //
     527| 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
     528     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
     529     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
     530     elim (H2 u' (ret_u ? s1') post) #s2' *
     531     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
     532     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
     533     %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2'))
     534        (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
     535        (ret_u statement s2'))} % try //
     536| 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
     537     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
     538     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
     539     elim (H2 u' (ret_u ? s1') post) #s2' *
     540     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
     541     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
     542     %{((mk_swret statement
     543         (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
     544         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
     545         (ret_u statement s2')))} % try //
     546| 6: #e #s #H #u0 #u1 #post normalize
     547     elim (H u0 u1 post) #s1' * normalize
     548     cases (mk_fresh_variables s u0) #fvs #u'
     549     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
     550     %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
     551        (ret_fvs statement s1') (ret_u statement s1'))} % try //
     552| 7: #e #s #H #u0 #u1 #post normalize
     553     elim (H u0 u1 post) #s1' * normalize
     554     cases (mk_fresh_variables s u0) #fvs #u'
     555     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
     556     %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
     557        (ret_fvs statement s1') (ret_u statement s1'))} % try //
     558| 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
     559     elim (H1 u0 u1
     560                (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
     561                (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
     562                post)) #s1' *
     563     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
     564     elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 u')))) @
     565                                 post)) #s2' *
     566     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
     567     elim (H3 u'' (ret_u ? s2') post) #s3' *
     568     cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta
     569     #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs
     570     >associative_append >associative_append >Heq1 normalize >Heq1_fvs
     571     >Heq2 normalize >Heq2_fvs >Heq3 normalize
     572     %{(mk_swret statement
     573        (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
     574        (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
     575        (ret_fvs statement s3') (ret_u statement s3'))} % try //
     576| 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
     577| 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % //
     578| 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % //
     579| 12: #e #ls #H #u0 #u1 #post
     580      whd in match (mk_fresh_variables ??);
     581      whd in match (switch_removal ???);     
     582      elim (fresh ? u0) #fresh #u'
     583      elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta
     584      cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta     
     585      >associative_append #Heq #Heq_fvs >Heq normalize nodelta
     586      >Heq_fvs normalize nodelta
     587      cases (simplify_switch ???) #st' #u''' normalize nodelta
     588      %{((mk_swret statement
     589          (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st')
     590          (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post)
     591          (ret_u labeled_statements ls')))} % //
     592| 13: #l #s #H #u0 #u1 #post normalize
     593      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
     594      %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s')
     595           post (ret_u statement s'))} % //
     596| 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % //
     597| 15: #l #s #H #u0 #u1 #post normalize
     598      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
     599      %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s')
     600           post (ret_u statement s'))} % //
     601| 16: #s #H #u0 #u1 #post normalize
     602      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
     603      %{(mk_swret labeled_statements (LSdefault (ret_st statement s'))
     604         (ret_acc statement s') post (ret_u statement s'))} % //
     605| 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize
     606      elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' *
     607      cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize
     608      elim (H1 u' (ret_u labeled_statements ls') post) #s1' *
     609      cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs
     610      >associative_append >Heql normalize >Heql_fvs >Heq normalize
     611      %{(mk_swret labeled_statements
     612          (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls'))
     613          (ret_acc labeled_statements ls'@ret_acc statement s1')
     614          (ret_fvs statement s1') (ret_u statement s1'))} % //
    326615] qed.
    327616
    328 definition function_switch_removal : function → universe SymbolTag → function × (universe SymbolTag) ≝
    329 λf,u.
    330   let 〈body, new_vars, u'〉 ≝ switch_removal (fn_body f) u in
    331   let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (pi1 … body) in
    332   〈f, u'〉.
    333 
    334 let rec fundef_switch_removal (f : clight_fundef) (u : universe SymbolTag) : clight_fundef × (universe SymbolTag) ≝
    335 match f with
    336 [ CL_Internal f ⇒
    337   let 〈f',u'〉 ≝ function_switch_removal f u in
    338   〈CL_Internal f', u'〉
    339 | CL_External _ _ _ ⇒
    340   〈f, u〉
    341 ].
    342 
     617axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
     618
     619(* Proof that switch_removal_switch_free does its job. *)
     620lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result).
     621#st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result →
     622                                                 branches_switch_free (ret_st ? ls_result)) … st)
     623[ 1: #fvs #u #result normalize #Heq destruct (Heq) //
     624| 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) //
     625| 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) //
     626| 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u)
     627     elim (switch_removal s1 fvs u) normalize
     628     [ 1: #_ #Habsurd destruct (Habsurd)
     629     | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1))
     630          elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1))
     631          [ 1: normalize #_ #Habsurd destruct (Habsurd)
     632          | 2: normalize #res2 #Heq2 #Heq destruct (Heq)
     633               normalize @conj
     634               [ 1: @Heq1 // | 2: @Heq2 // ]
     635     ] ]
     636| *:
     637  (* TODO the first few cases show that the lemma is routinely proved. TBF later. *)
     638  @cthulhu ]
     639qed.
    343640
    344641(* -----------------------------------------------------------------------------
     
    356653 *)
    357654
     655(* Least element in the total order of identifiers. *)
     656definition least_identifier ≝ an_identifier SymbolTag one.
     657
    358658(* This is certainly overkill: variables adressed in an expression should be declared in the
    359  * enclosing function's prototype. *)
    360 let rec max_of_expr (e : expr) (current : ident) : ident ≝
     659 * enclosing function's prototype. *) 
     660let rec max_of_expr (e : expr) : ident ≝
    361661match e with
    362662[ Expr ed _ ⇒
    363663  match ed with
    364   [ Econst_int _ _ ⇒ current
    365   | Econst_float _ ⇒ current
    366   | Evar id ⇒ max_id id current
    367   | Ederef e1 ⇒ max_of_expr e1 current
    368   | Eaddrof e1 ⇒ max_of_expr e1 current
    369   | Eunop _ e1 ⇒ max_of_expr e1 current
    370   | Ebinop _ e1 e2 ⇒ max_of_expr e1 (max_of_expr e2 current)
    371   | Ecast _ e1 ⇒ max_of_expr e1 current
    372   | Econdition e1 e2 e3 ⇒
    373     max_of_expr e1 (max_of_expr e2 (max_of_expr e3 current))
     664  [ Econst_int _ _ ⇒ least_identifier
     665  | Econst_float _ ⇒ least_identifier
     666  | Evar id ⇒ id
     667  | Ederef e1 ⇒ max_of_expr e1
     668  | Eaddrof e1 ⇒ max_of_expr e1
     669  | Eunop _ e1 ⇒ max_of_expr e1
     670  | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
     671  | Ecast _ e1 ⇒ max_of_expr e1
     672  | Econdition e1 e2 e3 ⇒ 
     673    max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3))
    374674  | Eandbool e1 e2 ⇒
    375     max_of_expr e1 (max_of_expr e2 current)
     675    max_id (max_of_expr e1) (max_of_expr e2)
    376676  | Eorbool e1 e2 ⇒
    377     max_of_expr e1 (max_of_expr e2 current)
    378   | Esizeof _ ⇒ current
    379   | Efield r f ⇒ max_id f (max_of_expr r current)
    380   | Ecost _ e1 ⇒ max_of_expr e1 current
     677    max_id (max_of_expr e1) (max_of_expr e2) 
     678  | Esizeof _ ⇒ least_identifier
     679  | Efield r f ⇒ max_id f (max_of_expr r)
     680  | Ecost _ e1 ⇒ max_of_expr e1
    381681  ]
    382682].
    383683
    384 (* Reeasoning about this promises to be a serious pain. Especially the Scall case. *)
    385 let rec max_of_statement (s : statement) (current : ident) : ident ≝
     684(* Reasoning about this promises to be a serious pain. Especially the Scall case. *)
     685let rec max_of_statement (s : statement) : ident ≝
    386686match s with
    387 [ Sskip ⇒ current
    388 | Sassign e1 e2 ⇒ max_of_expr e2 (max_of_expr e1 current)
    389 | Scall ret f args ⇒
     687[ Sskip ⇒ least_identifier
     688| Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
     689| Scall r f args ⇒
    390690  let retmax ≝
    391     match ret with
    392     [ None ⇒ current
    393     | Some e ⇒ max_of_expr e current ]
     691    match r with
     692    [ None ⇒ least_identifier
     693    | Some e ⇒ max_of_expr e ]
    394694  in
    395   foldl ?? (λacc,elt. max_of_expr elt acc) (max_of_expr f retmax) args
    396 | Ssequence s1 s2 ⇒
    397   max_of_statement s1 (max_of_statement s2 current)
     695  max_id (max_of_expr f)
     696         (max_id retmax
     697                 (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )
     698| Ssequence s1 s2 ⇒
     699  max_id (max_of_statement s1) (max_of_statement s2)
    398700| Sifthenelse e s1 s2 ⇒
    399   max_of_expr e (max_of_statement s1 (max_of_statement s2 current))
     701  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
    400702| Swhile e body ⇒
    401   max_of_expr e (max_of_statement body current)
     703  max_id (max_of_expr e) (max_of_statement body)
    402704| Sdowhile e body ⇒
    403   max_of_expr e (max_of_statement body current)
     705  max_id (max_of_expr e) (max_of_statement body)
    404706| Sfor init test incr body ⇒
    405   max_of_statement init (max_of_expr test (max_of_statement incr (max_of_statement body current)))
    406 | Sbreak ⇒ current
    407 | Scontinue ⇒ current
     707  max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body))
     708| Sbreak ⇒ least_identifier
     709| Scontinue ⇒ least_identifier
    408710| Sreturn opt ⇒
    409711  match opt with
    410   [ None ⇒ current
    411   | Some e ⇒ max_of_expr e current
     712  [ None ⇒ least_identifier
     713  | Some e ⇒ max_of_expr e
    412714  ]
    413715| Sswitch e ls ⇒
    414   max_of_expr e (max_of_ls ls current)
     716  max_id (max_of_expr e) (max_of_ls ls)
    415717| Slabel lab body ⇒
    416   max_id lab (max_of_statement body current)
     718  max_id lab (max_of_statement body)
    417719| Sgoto lab ⇒
    418   max_id lab current
     720  lab
    419721| Scost _ body ⇒
    420   max_of_statement body current 
     722  max_of_statement body
    421723]
    422 and max_of_ls (ls : labeled_statements) (current : ident) : ident ≝
     724and max_of_ls (ls : labeled_statements) : ident ≝
    423725match ls with
    424 [ LSdefault s ⇒ max_of_statement s current
    425 | LScase _ _ s ls' ⇒ max_of_ls ls' (max_of_statement s current)
     726[ LSdefault s ⇒ max_of_statement s
     727| LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s)
    426728].
    427729
    428730definition max_id_of_function : function → ident ≝
    429 λf. max_of_statement (fn_body f) (max_id_of_fn f).
    430 
    431 definition max_id_of_fundef_deep : clight_fundef → ident ≝
    432 λf. match f with
    433   [ CL_Internal f ⇒ max_id_of_function f
    434   | CL_External id _ _ ⇒ id
    435   ].
    436 
    437 let rec max_id_of_functs_deep (funcs : list (ident × clight_fundef)) (current : ident) : ident ≝
    438 let func_max ≝
    439   foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef_deep (\snd idf))) id) (an_identifier ? one) funcs
    440 in max_id func_max current.
    441 
    442 definition max_id_of_program_deep : clight_program → ident ≝
    443 λp.
    444   max_id
    445     (max_id_of_functs_deep (prog_funct ?? p) (prog_main ?? p))
    446     (max_id_of_globvars (prog_vars ?? p)).
    447        
    448 (* The previous functions compute an (over?)-approximation of the identifiers and labels.
    449    The following function builds a "good" universe for a complete clight program. *)
    450 definition universe_for_program_deep : clight_program → universe SymbolTag ≝
    451 λp. universe_of_max (max_id_of_program_deep p).
    452 
     731λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f).
     732
     733(* We compute fresh universes on a function-by function basis, since there can't
     734 * be cross-functions gotos or stuff like that. *)
     735definition function_switch_removal : function → function × (list (ident × type)) ≝
     736λf.
     737  (λres_record.
     738    let new_vars ≝ ret_acc ? res_record in
     739    let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in
     740    〈result, new_vars〉)
     741  (let u ≝ universe_of_max (max_id_of_function f) in
     742   let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in
     743   match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with
     744   [ None ⇒ λHsr. ?
     745   | Some res_record ⇒ λ_. res_record
     746   ] (refl ? (switch_removal (fn_body f) fvs u'))).   
     747lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq
     748<Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd)
     749qed.
     750
     751let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝
     752match f with
     753[ CL_Internal f ⇒
     754  CL_Internal (\fst (function_switch_removal f))
     755| CL_External _ _ _ ⇒
     756  f
     757].
    453758
    454759let rec program_switch_removal (p : clight_program) : clight_program ≝
    455  let uv         ≝ universe_for_program_deep p in
    456760 let prog_funcs ≝ prog_funct ?? p in
    457  let 〈sf_funcs, final_uv〉 ≝
    458   foldr ?? (λcl_fundef.λacc.
    459     let 〈fundefs, uv1〉    ≝ acc in   
    460     let 〈fun_id, fun_def〉 ≝ cl_fundef in
    461     let 〈new_fun_def,uv2〉 ≝ fundef_switch_removal fun_def uv1 in
    462     〈〈fun_id, new_fun_def〉 :: fundefs, uv2〉
    463    ) 〈[ ], uv〉 prog_funcs
    464  in
     761 let sf_funcs   ≝ map ?? (λcl_fundef.
     762    let 〈fun_id, fun_def〉 ≝ cl_fundef in
     763    〈fun_id, fundef_switch_removal fun_def〉
     764  ) prog_funcs in
    465765 mk_program ??
    466766  (prog_vars … p)
     
    468768  (prog_main … p).
    469769
     770
     771(* -----------------------------------------------------------------------------
     772   Applying two relations on all substatements and all subexprs (directly under).
     773   ---------------------------------------------------------------------------- *)
     774
     775let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝
     776match s1 with
     777[ Sskip ⇒ True
     778| Sassign e1 e2 ⇒ Q e1 ∧ Q e2
     779| Scall r f args ⇒
     780  match r with
     781  [ None ⇒ Q f ∧ (All … Q args)
     782  | Some r ⇒ Q r ∧ Q f ∧ (All … Q args)
     783  ]
     784| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
     785| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
     786| Swhile e sub ⇒ Q e ∧ P sub
     787| Sdowhile e sub ⇒ Q e ∧ P sub
     788| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
     789| Sbreak ⇒ True
     790| Scontinue ⇒ True
     791| Sreturn r ⇒
     792  match r with
     793  [ None ⇒ True
     794  | Some r ⇒ Q r ]
     795| Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P)
     796| Slabel _ sub ⇒ P sub
     797| Sgoto _ ⇒ True
     798| Scost _ sub ⇒ P sub
     799]
     800and substatement_ls ls (P : statement → Prop) : Prop ≝
     801match ls with
     802[ LSdefault sub ⇒ P sub
     803| LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P)
     804].
     805
     806(* -----------------------------------------------------------------------------
     807   Freshness conservation results on switch removal.
     808   ---------------------------------------------------------------------------- *)
     809
     810(* Similar stuff in toCminor.ma. *)
     811lemma fresh_for_univ_still_fresh :
     812   ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'.
     813* #p * #i #H1 #v * #p' lapply H1 normalize
     814#H1 #H2 destruct (H2) /2/ qed.
     815
     816lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'.
     817#u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh)
     818cases (fresh SymbolTag u)
     819#fv #u' #H %{fv} %{u'} @conj try // @H //
     820qed.
     821
     822lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)).
     823#e #exit #ls @(branches_ind … ls)
     824[ 1: #st #u #i #Hfresh normalize
     825     lapply (fresh_for_univ_still_fresh … Hfresh)
     826     cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize //
     827| 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize
     828     lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) *
     829     #subcond #sublabel #u1 #Hfresh1 normalize
     830     lapply (fresh_for_univ_still_fresh … Hfresh1)
     831     cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize //
     832] qed.
     833
     834lemma simplify_switch_fresh : ∀u,i,e,ls.
     835 fresh_for_univ ? i u →
     836 fresh_for_univ ? i (\snd (simplify_switch e ls u)).
     837#u #i #e #ls #Hfresh
     838normalize
     839lapply (fresh_for_univ_still_fresh … Hfresh)
     840cases (fresh ? u)
     841#exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux
     842normalize lapply (produce_cond_fresh e exit_label ls … Haux)
     843elim (produce_cond ????) * #stm #label #uv2 normalize nodelta //
     844qed.
     845
     846(*
     847lemma switch_removal_fresh : ∀i,s,u.
     848    fresh_for_univ ? i u →
     849    fresh_for_univ ? i (\snd (switch_removal s u)).
     850#i #s @(statement_ind2 ? (λls. ∀u. fresh_for_univ ? i u →
     851                                      fresh_for_univ ? i (\snd (switch_removal_branches ls u))) … s)
     852try //
     853[ 1: #s1' #s2' #Hind1 #Hind2 #u #Hyp
     854     whd in match (switch_removal (Ssequence s1' s2') u);
     855     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
     856     * #irr1 #irr2 #uA #HuA normalize nodelta
     857     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
     858     * #irr3 #irr4 #uB #HuB normalize nodelta //
     859| 2: #e #s1' #s2' #Hind1 #Hind2 #u #Hyp
     860     whd in match (switch_removal (Sifthenelse e s1' s2') u);
     861     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
     862     * #irr1 #irr2 #uA #HuA normalize nodelta
     863     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
     864     * #irr3 #irr4 #uB #HuB normalize nodelta //
     865| 3,4: #e #s' #Hind #u #Hyp
     866     whd in match (switch_removal ? u);
     867     lapply (Hind u Hyp) elim (switch_removal s' u)
     868     * #irr1 #irr2 #uA #HuA normalize nodelta //
     869| 5: #s1' #e #s2' #s3' #Hind1 #Hind2 #Hind3 #u #Hyp
     870     whd in match (switch_removal (Sfor s1' e s2' s3') u);
     871     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
     872     * #irr1 #irr2 #uA #HuA normalize nodelta
     873     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
     874     * #irr3 #irr4 #uB #HuB normalize nodelta
     875     lapply (Hind3 uB HuB) elim (switch_removal s3' uB)
     876     * #irr5 #irr6 #uC #HuC normalize nodelta //
     877| 6: #e #ls #Hind #u #Hyp
     878     whd in match (switch_removal (Sswitch e ls) u);
     879     lapply (Hind u Hyp)
     880     cases (switch_removal_branches ls u)
     881     * #irr1 #irr2 #uA #HuA normalize nodelta
     882     lapply (fresh_for_univ_still_fresh … HuA)
     883     cases (fresh SymbolTag uA) #v #uA' #Haux lapply (Haux v uA' (refl ? 〈v,uA'〉))
     884     -Haux #HuA' normalize nodelta
     885     lapply (simplify_switch_fresh uA' i (Expr (Evar v) (typeof e)) irr1 HuA')
     886     cases (simplify_switch ???) #stm #uB
     887     #Haux normalize nodelta //
     888| 7,8: #label #body #Hind #u #Hyp
     889     whd in match (switch_removal ? u);
     890     lapply (Hind u Hyp) elim (switch_removal body u)
     891     * #irr1 #irr2 #uA #HuA normalize nodelta //
     892| 9: #defcase #Hind #u #Hyp whd in match (switch_removal_branches ??);
     893     lapply (Hind u Hyp) elim (switch_removal defcase u)
     894     * #irr1 #irr2 #uA #HuA normalize nodelta //
     895| 10: #sz #i0 #s0 #tl #Hind1 #Hind2 #u #Hyp normalize
     896     lapply (Hind2 u Hyp) elim (switch_removal_branches tl u)
     897     * #irr1 #irr2 #uA #HuA normalize nodelta
     898     lapply (Hind1 uA HuA) elim (switch_removal s0 uA)
     899     * #irr3 #irr4 #uB #HuB //
     900] qed.
     901
     902lemma switch_removal_branches_fresh : ∀i,ls,u.
     903    fresh_for_univ ? i u →
     904    fresh_for_univ ? i (\snd (switch_removal_branches ls u)).
     905#i #ls @(labeled_statements_ind2 (λs. ∀u. fresh_for_univ ? i u →
     906                                           fresh_for_univ ? i (\snd (switch_removal s u))) ? … ls)
     907try /2 by switch_removal_fresh/
     908[ 1: #s #Hind #u #Hfresh normalize lapply (switch_removal_fresh ? s ? Hfresh)
     909     cases (switch_removal s u) * //
     910| 2: #sz #i #s #tl #Hs #Htl #u #Hfresh normalize
     911     lapply (Htl u Hfresh)
     912     cases (switch_removal_branches tl u) * normalize nodelta
     913     #ls' #fvs #u' #Hfresh'
     914     lapply (Hs u' Hfresh')
     915     cases (switch_removal s u') * //
     916] qed.
     917*)
    470918(* -----------------------------------------------------------------------------
    471919   Simulation proof and related voodoo.
    472920   ----------------------------------------------------------------------------*)
    473 
    474 (* Copied from SimplifyCasts.ma. Might be good to create a new file for shared stuff. *)
    475 inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
    476 | SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
    477 | SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.
    478921
    479922definition expr_lvalue_ind_combined ≝
     
    539982].
    540983
     984
    541985(* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched
    542986   by a non-constant number of evaluations in the converted program. More precisely,
     
    544988   necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *)
    545989   
    546 (* A version of simplify_switch hiding the ugly proj *)
    547 definition sw_rem : statement → (universe SymbolTag) → statement ≝
    548 λs,u.
    549   \fst (\fst (switch_removal s u)).
    550 
     990(* A version of simplify_switch hiding the ugly projs *)
    551991definition fresh_for_expression ≝
    552 λe,u. fresh_for_univ SymbolTag (max_of_expr e (an_identifier ? one)) u. 
    553  
     992λe,u. fresh_for_univ SymbolTag (max_of_expr e) u.
     993
    554994definition fresh_for_statement ≝
    555 λs,u. fresh_for_univ SymbolTag (max_of_statement s (an_identifier ? one)) u.
    556 
     995λs,u. fresh_for_univ SymbolTag (max_of_statement s) u.
     996
     997(* needed during mutual induction ... *)
     998definition fresh_for_labeled_statements ≝
     999λls,u. fresh_for_univ ? (max_of_ls ls) u.
     1000   
    5571001definition fresh_for_function ≝
    5581002λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.
    5591003
    560 let rec fresh_for_continuation (k : cont) (u : universe SymbolTag) : Prop ≝
    561 match k with
    562 [ Kstop ⇒ True
    563 | Kseq s k0 ⇒ (fresh_for_statement s u) ∧ (fresh_for_continuation k0 u)
    564 | Kwhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u)
    565 | Kdowhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u)
    566 | Kfor2 e s1 s2 k0 ⇒
    567   (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧
    568   (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u)
    569 | Kfor3 e s1 s2 k0 ⇒
    570   (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧
    571   (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u)
    572 | Kswitch k0 ⇒ fresh_for_continuation k0 u
    573 | Kcall _ f e k ⇒ (fresh_for_function f u) ∧ (fresh_for_continuation k u)
    574 ].
    575 
    576 inductive switch_cont_sim : cont → cont → Prop ≝
    577 | swc_stop :
    578     switch_cont_sim Kstop Kstop
    579 | swc_seq : ∀s,k,k',u.
    580     fresh_for_statement s u →
    581     switch_cont_sim k k' →
    582     switch_cont_sim (Kseq s k) (Kseq (sw_rem s u) k')
    583 | swc_while : ∀e,s,k,k',u.
    584     fresh_for_expression e u →
    585     fresh_for_statement s u →
    586     switch_cont_sim k k' →
    587     switch_cont_sim (Kwhile e s k) (Kwhile e (sw_rem s u) k')
    588 | swc_dowhile : ∀e,s,k,k',u.
    589     fresh_for_expression e u →
    590     fresh_for_statement s u →
    591     switch_cont_sim k k' →
    592     switch_cont_sim (Kdowhile e s k) (Kdowhile e (sw_rem s u) k')
    593 | swc_for1 : ∀e,s1,s2,k,k',u1,u2.
    594     fresh_for_statement s1 u1 →
    595     fresh_for_statement s2 u2 →
    596     switch_cont_sim k k' →
    597     switch_cont_sim (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip e (sw_rem s1 u1) (sw_rem s2 u2)) k')
    598 | swc_for2 : ∀e,s1,s2,k,k',u1,u2.
    599     fresh_for_statement s1 u1 →
    600     fresh_for_statement s2 u2 →
    601     switch_cont_sim k k' →
    602     switch_cont_sim (Kfor2 e s1 s2 k) (Kfor2 e (sw_rem s1 u1) (sw_rem s2 u2) k')
    603 | swc_for3 : ∀e,s1,s2,k,k',u1,u2.
    604     fresh_for_statement s1 u1 →
    605     fresh_for_statement s2 u2 →
    606     switch_cont_sim k k' →
    607     switch_cont_sim (Kfor3 e s1 s2 k) (Kfor3 e (sw_rem s1 u1) (sw_rem s2 u2) k')
    608 | swc_switch : ∀k,k'.
    609     switch_cont_sim k k' →
    610     switch_cont_sim (Kswitch k) (Kswitch k')
    611 | swc_call : ∀r,f,en,k,k',u.
    612     fresh_for_function f u →
    613     switch_cont_sim k k' →
    614     switch_cont_sim (Kcall r f en k) (Kcall r (\fst (function_switch_removal f u)) en k').
    615 
    616 
    617 inductive switch_state_sim : state → state → Prop ≝
    618 | sws_state : ∀uf,us,uk,f,s,k,k',e,m.
    619     fresh_for_function f uf →
    620     fresh_for_statement s us →
    621     fresh_for_continuation k' uk →
    622     switch_cont_sim k k' →
    623     switch_state_sim (State f s k e m) (State (\fst (function_switch_removal f uf)) (sw_rem s us) k' e m)
    624 (* Extra matching states that we can reach that don't quite correspond to the
    625    labelling function *)
    626 (*   
    627 | sws_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
    628     switch_state_sim (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    629 | sws_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
    630     switch_state_sim (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    631 | sws_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
    632     switch_state_sim (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    633 *)
    634 (* and the rest *)
    635 | sws_callstate : ∀ufd,fd,args,k,k',m.
    636     switch_cont_sim k k' →
    637     switch_state_sim (Callstate fd args k m) (Callstate (\fst (fundef_switch_removal fd ufd)) args k' m)
    638 | sws_returnstate : ∀res,k,k',m.
    639     switch_cont_sim k k' →
    640     switch_state_sim (Returnstate res k m) (Returnstate res k' m)
    641 | sws_finalstate : ∀r.
    642     switch_state_sim (Finalstate r) (Finalstate r)
    643 .
    644 
    645 inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
    646 | eventually_base : ∀s,t,s'.
    647     exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    648     P s' →
    649     eventually ge P s t
    650 | eventually_step : ∀s,t,s',t'.
    651     exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    652     eventually ge P s' t' →
    653     eventually ge P s (t ⧺ t').
    654    
    655 (* [eventually] is not so nice to use directly, we would like to make the mandatory
    656  * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
    657    to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
    658 lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
    659                                       eventually ge P s t.
    660 #ge #P #s #t * #s' * #Hexec #HP %1{? Hexec HP}
    661 qed.
    662 
    663 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    664   rg_find_symbol: ∀s.
    665     find_symbol ? ge s = find_symbol ? ge' s;
    666   rg_find_funct: ∀v,f.
    667     find_funct ? ge v = Some ? f →
    668     find_funct ? ge' v = Some ? (t f);
    669   rg_find_funct_ptr: ∀b,f.
    670     find_funct_ptr ? ge b = Some ? f →
    671     find_funct_ptr ? ge' b = Some ? (t f)
    672 }.
    673 
    674 (* TODO ... fundef_switch_removal wants a universe which is fresh-for-its argument. *)
    675 (*
    676 lemma sim_related_globals : ∀ge,ge',en,m,u. related_globals ? fundef_switch_removal ge ge' →
    677   (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
    678   (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
    679 *) 
    680 
    681 (* The return type of any function is invariant under switch removal *)
    682 lemma fn_return_simplify : ∀f,u. fn_return (\fst (function_switch_removal f u)) = fn_return f.
    683 #f #u elim f #ret #args #vars #body normalize elim (switch_removal body u)
    684 * * #body' #Hswitch_free #new_vars #u' normalize //
    685 qed.
    686 
    687 lemma while_commute : ∀e0, s0, us0. Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0).
    688 #e0 #s0 #us0 normalize
    689 cases (switch_removal s0 us0) * * #body #Hswfree #newvars #u' normalize //
    690 qed.
     1004(* misc properties of the max function on positives. *)
    6911005
    6921006lemma max_one_neutral : ∀v. max v one = v.
     
    7231037#a @(le_to_leb_true a a) // qed.
    7241038
    725 (*
    726 lemma le_S_contradiction : ∀a,b. le (succ a) b → le (succ b) a → False.
    727 #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) #Heq
    728 destruct inversion H2
    729 [ 2: #m #H1 #H2 #H3
    730 elim b; normalize in match (succ ?);
    731 [ 1: #H destruct (H)
    732 | 2: #p #H
    733 *)
    7341039(* This should be somewhere else. *)
    7351040lemma associative_max : associative ? max.
     
    7771082          #Hca /2/
    7781083     ]
    779 ] qed.      
     1084] qed.   
    7801085
    7811086lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3).
    7821087* #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max //
    7831088qed.
    784 
     1089(*
    7851090lemma max_of_expr_rewrite :
    7861091  ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id.
     
    8121117      whd in match (max_id ??); >associative_max @refl
    8131118] qed.
    814 
     1119*)
     1120lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u.
     1121* #a * #b * #u normalize
     1122lapply (pos_compare_to_Prop a b)
     1123cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
     1124[ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/
     1125| 2: destruct >reflexive_leb /2/
     1126| 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/
     1127] qed.
     1128
     1129(* Auxilliary commutation lemma used in [substatement_fresh]. *)
     1130
     1131lemma foldl_max : ∀l,a,b.
     1132  foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l =
     1133  max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l).
     1134#l elim l
     1135[ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl
     1136| 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%);
     1137     <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
     1138] qed.
     1139
     1140(* -----------------------------------------------------------------------------
     1141   Stuff on memory and environments extensions.
     1142   Let us recap: the memory model of a function is in two layers. An environment
     1143   (type [env]) maps identifiers to blocks, and a memory maps blocks
     1144   switch_removal introduces new, fresh variables. What is to be noted is that
     1145   switch_removal modifies both the contents of the "disjoint" part of memory, but
     1146   also where the data is allocated. The first solution considered was to consider
     1147   an extensional equivalence relation on values, saying that equivalent pointers
     1148   point to equivalent values. This has to be a coinductive relation, in order to
     1149   take into account cyclic data structures. Rather than using coinductive types,
     1150   we use the compcert solution, using so-called memory embeddings.
     1151   ---------------------------------------------------------------------------- *)
     1152
     1153(* ---------------- *)
     1154(* auxillary lemmas *)
     1155lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
     1156#a #b #HA
     1157lapply (Zltb_true_to_Zlt … HA) #HA_prop
     1158@Zlt_to_Zltb_true /2/
     1159qed.
     1160
     1161lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
     1162#a @Zlt_to_Zltb_true /2/ qed.
     1163
     1164
     1165definition le_offset : offset → offset → bool ≝
     1166  λx,y. Zleb (offv x) (offv y).
     1167 
     1168lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
     1169
     1170lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
     1171
     1172(* When equality on A is decidable, [mem A elt l] is too. *)
     1173lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
     1174#A #dec #elt #l elim l
     1175[ 1: normalize %2 /2/
     1176| 2: #hd #tl #Hind
     1177     elim (dec elt hd)
     1178     [ 1: #Heq >Heq %1 /2/
     1179     | 2: #Hneq cases Hind
     1180        [ 1: #Hmem %1 /2/
     1181        | 2: #Hnmem %2 normalize
     1182              % #H cases H
     1183              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
     1184              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
     1185] ] ]
     1186qed.
     1187
     1188lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
     1189#a #b @(eq_block_elim … a b) /2/ qed.
     1190
     1191lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
     1192#l #elt1 #elt2 elim l
     1193[ 1: normalize #Habsurd @(False_ind … Habsurd)
     1194| 2: #hd #tl #Hind normalize #Hl #Hr
     1195   cases Hl
     1196   [ 1: #Heq >Heq
     1197        @(eq_block_elim … hd elt2)
     1198        [ 1: #Heq >Heq /2 by not_to_not/
     1199        | 2: #x @x ]
     1200   | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
     1201        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
     1202        | 2: #Hmem2 @Hind //
     1203        ]
     1204   ]
     1205] qed.
     1206
     1207lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
     1208#b1 #b2 * #Hb
     1209@(eq_block_elim … b1 b2)
     1210[ 1: #Habsurd @(False_ind … (Hb Habsurd))
     1211| 2: // ] qed.
     1212
     1213(* Type of blocks in a particular region. *)
     1214definition block_in : region → Type[0] ≝ λrg. Σb. (block_region b) = rg.
     1215
     1216(* An embedding is a function from blocks to (blocks+offset). *)
     1217definition embedding ≝ block → option (block × offset).
     1218
     1219definition offset_plus : offset → offset → offset ≝
     1220  λo1,o2. mk_offset (offv o1 + offv o2).
     1221 
     1222lemma offset_plus_O : ∀o. offset_plus o (mk_offset OZ) = o.
     1223* #z normalize // qed.
     1224
     1225(* Translates a pointer through an embedding. *)
     1226definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
     1227λp,E.
     1228match p with
     1229[ mk_pointer pblock poff ⇒
     1230   match E pblock with
     1231   [ None ⇒ None ?
     1232   | Some loc ⇒
     1233    let 〈dest_block,dest_off〉 ≝ loc in
     1234    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
     1235    Some ? ptr
     1236   ]
     1237].
     1238
     1239(* We parameterise the "equivalence" relation on values with an embedding. *)
     1240(* Front-end values. *)
     1241inductive value_eq (E : embedding) : val → val → Prop ≝
     1242| undef_eq : ∀v.
     1243  value_eq E Vundef v
     1244| vint_eq : ∀sz,i.
     1245  value_eq E (Vint sz i) (Vint sz i)
     1246| vfloat_eq : ∀f.
     1247  value_eq E (Vfloat f) (Vfloat f)
     1248| vnull_eq :
     1249  value_eq E Vnull Vnull
     1250| vptr_eq : ∀p1,p2.
     1251  pointer_translation p1 E = Some ? p2 →
     1252  value_eq E (Vptr p1) (Vptr p2).
     1253 
     1254(* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t.
     1255 * the values are equivalent. *)
     1256definition load_sim ≝
     1257λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
     1258 ∀b1,off1,b2,off2,ty,v1.
     1259  valid_block m1 b1 →
     1260  E b1 = Some ? 〈b2,off2〉 →
     1261  load_value_of_type ty m1 b1 off1 = Some ? v1 →
     1262  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
     1263
     1264(* Definition of a memory injection *)
     1265record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
     1266{ (* Load simulation *)
     1267  mi_inj : load_sim E m1 m2;
     1268  (* Invalid blocks are not mapped *)
     1269  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
     1270  (* Blocks in the codomain are valid *)
     1271  mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
     1272  (* Regions are preserved *)
     1273  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
     1274  (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.
     1275   * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where
     1276   * all variables are allocated in the same block. *)
     1277  mi_disjoint : ∀b1,b2,b1',b2',o1',o2'.
     1278                b1 ≠ b2 →
     1279                E b1 = Some ? 〈b1',o1'〉 →
     1280                E b2 = Some ? 〈b2',o2'〉 →
     1281                b1' ≠ b2'
     1282}.
     1283
     1284(* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\
     1285 * A memory extension is a [memory_inj] with some particular blocks designated *)
     1286
     1287alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
     1288
     1289record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
     1290{ me_inj : memory_inj E m1 m2;
     1291  me_writeable : list block;
     1292  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
     1293  me_writeable_ok : ∀b,b',o'.
     1294                    valid_block m1 b →
     1295                    E b = Some ? 〈b',o'〉 →
     1296                    ¬ (meml ? b' me_writeable)
     1297}.
     1298
     1299(* ---------------------------------------------------------------------------- *)
     1300(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
     1301
     1302(* A particular inversion. *)
     1303lemma value_eq_ptr_inversion :
     1304  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
     1305#E #p1 #v #Heq inversion Heq
     1306[ 1: #v #Habsurd destruct (Habsurd)
     1307| 2: #sz #i #Habsurd destruct (Habsurd)
     1308| 3: #f #Habsurd destruct (Habsurd)
     1309| 4:  #Habsurd destruct (Habsurd)
     1310| 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
     1311     %{p2} @conj try @refl try assumption
     1312] qed.
     1313 
     1314(* If we succeed to load something by value from a 〈b,off〉 location,
     1315   [b] is a valid block. *)
     1316lemma load_by_value_success_valid_block_aux :
     1317  ∀ty,m,b,off,v.
     1318    access_mode ty = By_value (typ_of_type ty) →
     1319    load_value_of_type ty m b off = Some ? v →
     1320    Zltb (block_id b) (nextblock m) = true. (* → valid_block m b *)
     1321#ty #m * #brg #bid #off #v whd in match (valid_block ??);
     1322cases ty
     1323[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1324| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1325whd in match (load_value_of_type ????);
     1326[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
     1327#Hmode
     1328[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
     1329     normalize in match (typesize ?);
     1330     whd in match (loadn ???);
     1331     whd in match (beloadv ??);
     1332     cases (Zltb bid (nextblock m)) normalize nodelta
     1333     try // #Habsurd destruct (Habsurd)
     1334| *: normalize in Hmode; destruct (Hmode)
     1335] qed.
     1336
     1337
     1338lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
     1339* #rg #id #m normalize
     1340elim id /2/ qed.
     1341
     1342lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
     1343* #rg #id #m normalize
     1344elim id /2/ qed.
     1345
     1346lemma load_by_value_success_valid_block :
     1347  ∀ty,m,b,off,v.
     1348    access_mode ty = By_value (typ_of_type ty) →
     1349    load_value_of_type ty m b off = Some ? v →
     1350    valid_block m b.
     1351#ty #m #b #off #v #Haccess_mode #Hload
     1352@valid_block_from_bool
     1353@(load_by_value_success_valid_block_aux ty m b off v Haccess_mode Hload)
     1354qed.
     1355
     1356(* Making explicit the contents of memory_inj for load_value_of_type *)
     1357lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
     1358    memory_inj E m1 m2 →
     1359    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
     1360    load_value_of_type ty m1 b1 off1 = Some ? v1 →
     1361    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
     1362#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
     1363lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
     1364     normalize in Hembed;
     1365     lapply (mi_inj … Hinj b1 off1)
     1366     cases (E b1) in Hembed;
     1367     [ 1: normalize #Habsurd destruct (Habsurd)
     1368     | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ]
     1369     lapply (refl ? (access_mode ty))
     1370     cases ty
     1371     [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1372     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1373     normalize in ⊢ ((???%) → ?); #Hmode #Hyp
     1374     [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd)
     1375     | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ]
     1376     #Hload_success
     1377     lapply (load_by_value_success_valid_block … Hmode … Hload_success)
     1378     #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success)
     1379qed.
     1380
     1381
     1382(* -------------------------------------- *)
     1383(* Lemmas pertaining to memory allocation *)
     1384
     1385(* A valid block stays valid after an alloc. *)
     1386lemma alloc_valid_block_conservation :
     1387  ∀m,m',z1,z2,r,new_block.
     1388  alloc m z1 z2 r = 〈m', new_block〉 →
     1389  ∀b. valid_block m b → valid_block m' b.
     1390#m #m' #z1 #z2 #r * #b' #Hregion_eq
     1391elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
     1392#Halloc destruct (Halloc)
     1393#b whd in match (valid_block ??) in ⊢ (% → %); /2/
     1394qed.
     1395
     1396(* Allocating a new zone produces a valid block. *)
     1397lemma alloc_valid_new_block :
     1398  ∀m,m',z1,z2,r,new_block.
     1399  alloc m z1 z2 r = 〈m', new_block〉 →
     1400  valid_block m' new_block.
     1401* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
     1402whd in match (alloc ????); whd in match (valid_block ??);
     1403#Halloc destruct (Halloc) /2/
     1404qed.
     1405
     1406(* All data in a valid block is unchanged after an alloc. *)
     1407lemma alloc_beloadv_conservation :
     1408  ∀m,m',block,offset,z1,z2,r,new_block.
     1409    valid_block m block →
     1410    alloc m z1 z2 r = 〈m', new_block〉 →
     1411    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
     1412* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
     1413whd in Halloc:(??%?); destruct (Halloc)
     1414whd in match (beloadv ??) in ⊢ (??%%);
     1415lapply (valid_block_to_bool … Hvalid) #Hlt
     1416>Hlt >(zlt_succ … Hlt)
     1417normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
     1418cut (eqZb (block_id block) next = false)
     1419[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
     1420>Hneq cases (eq_region ??) normalize nodelta  @refl
     1421qed.
     1422
     1423(* Lift [alloc_beloadv_conservation] to loadn *)
     1424lemma alloc_loadn_conservation :
     1425  ∀m,m',z1,z2,r,new_block.
     1426    alloc m z1 z2 r = 〈m', new_block〉 →
     1427    ∀n. ∀block,offset.
     1428    valid_block m block →
     1429    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
     1430#m #m' #z1 #z2 #r #new_block #Halloc #n
     1431elim n try //
     1432#n' #Hind #block #offset #Hvalid_block
     1433whd in ⊢ (??%%);
     1434>(alloc_beloadv_conservation … Hvalid_block Halloc)
     1435cases (beloadv m' (mk_pointer block offset)) //
     1436#bev normalize nodelta
     1437whd in match (shift_pointer ???); >Hind try //
     1438qed.
     1439
     1440(* Memory allocation preserves [memory_inj] *)
     1441lemma alloc_memory_inj :
     1442  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
     1443  alloc m2 z1 z2 r = 〈m2', new_block〉 →
     1444  memory_inj E m1 m2'.
     1445#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
     1446%
     1447[ 1:
     1448  whd
     1449  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
     1450  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
     1451  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
     1452  lapply (refl ? (access_mode ty))
     1453  cases ty in Hload_eq;
     1454  [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1455  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1456  #Hload normalize in ⊢ ((???%) → ?); #Haccess
     1457  [ 1,7,8: normalize in Hload; destruct (Hload)
     1458  | 2,3,4,9: whd in match (load_value_of_type ????);
     1459     whd in match (load_value_of_type ????);
     1460     lapply (load_by_value_success_valid_block … Haccess Hload)
     1461     #Hvalid_block
     1462     whd in match (load_value_of_type ????) in Hload;
     1463     <(alloc_loadn_conservation … Halloc … Hvalid_block)
     1464     @Hload
     1465  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
     1466| 2: @(mi_freeblock … Hmemory_inj)
     1467| 3: #b #b' #o' #HE
     1468     lapply (mi_incl … Hmemory_inj … HE)
     1469     elim m2 in Halloc; #contents #nextblock #Hnextblock
     1470     whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1471     whd in match (valid_block ??) in ⊢ (% → %); /2/
     1472| 4: @(mi_region … Hmemory_inj)
     1473| 5: @(mi_disjoint … Hmemory_inj)
     1474] qed.
     1475
     1476(* Memory allocation induces a memory extension. *)
     1477lemma alloc_memory_ext :
     1478  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
     1479  alloc m2 z1 z2 r = 〈m2', new_block〉 →
     1480  memory_ext E m1 m2'.
     1481#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
     1482lapply (alloc_memory_inj … Hmemory_inj Halloc)
     1483#Hinj' %
     1484[ 1: @Hinj'
     1485| 2: @[new_block]
     1486| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
     1487      #Heq destruct (Heq) whd elim m2 in Halloc;
     1488      #Hcontents #nextblock #Hnextblock
     1489      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1490      /2/
     1491| 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload %
     1492     normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ]
     1493     #Heq destruct (Heq)
     1494     lapply (mi_incl … Hmemory_inj … Hload)
     1495     whd in ⊢ (% → ?); #Habsurd
     1496     (* contradiction car ¬ (valid_block m2 new_block)  *)
     1497     elim m2 in Halloc Habsurd;
     1498     #contents_m2 #nextblock_m2 #Hnextblock_m2
     1499     whd in ⊢ ((??%?) → ?);
     1500     #Heq_alloc destruct (Heq_alloc)
     1501     lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd)
     1502] qed.
     1503
     1504lemma bestorev_beloadv_conservation :
     1505  ∀mA,mB,wb,wo,v.
     1506    bestorev mA (mk_pointer wb wo) v = Some ? mB →
     1507    ∀rb,ro. eq_block wb rb = false →
     1508    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
     1509#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
     1510whd in ⊢ (??%%);
     1511elim mB in Hstore; #contentsB #nextblockB #HnextblockB
     1512normalize in ⊢ (% → ?);
     1513cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
     1514[ 2: #Habsurd destruct (Habsurd) ]
     1515cases (if Zleb (low (blocks mA wb)) (offv wo) 
     1516       then Zltb (offv wo) (high (blocks mA wb)) 
     1517       else false) normalize nodelta
     1518[ 2: #Habsurd destruct (Habsurd) ]
     1519#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
     1520cases rr cases wr normalize try //
     1521@(eqZb_elim … rid wid)
     1522[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
     1523try //
     1524qed.
     1525
     1526(* lift [bestorev_beloadv_conservation to [loadn] *)
     1527lemma bestorev_loadn_conservation :
     1528  ∀mA,mB,n,wb,wo,v.
     1529    bestorev mA (mk_pointer wb wo) v = Some ? mB →
     1530    ∀rb,ro. eq_block wb rb = false →
     1531    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
     1532#mA #mB #n
     1533elim n
     1534[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
     1535| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
     1536     whd in ⊢ (??%%);
     1537     >(bestorev_beloadv_conservation … Hstore … Hneq)
     1538     >(Hind … Hstore … Hneq) @refl
     1539] qed.
     1540
     1541(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
     1542lemma bestorev_load_value_of_type_conservation :
     1543  ∀mA,mB,wb,wo,v.
     1544    bestorev mA (mk_pointer wb wo) v = Some ? mB →
     1545    ∀rb,ro. eq_block wb rb = false →
     1546    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
     1547#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
     1548cases ty
     1549[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1550| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //
     1551[ 1: elim sz | 2: elim fsz | 3: | 4: ]
     1552whd in ⊢ (??%%);
     1553>(bestorev_loadn_conservation … Hstore … Hneq) @refl
     1554qed.
     1555
     1556(* Writing in the "extended" part of a memory preserves the underlying injection *)
     1557lemma bestorev_memory_ext_to_load_sim :
     1558  ∀E,mA,mB,mC.
     1559  ∀Hext:memory_ext E mA mB.
     1560  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
     1561  bestorev mB (mk_pointer wb wo) v = Some ? mC →
     1562  load_sim E mA mC.
     1563#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
     1564#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
     1565(* Show that (wb ≠ b2) *)
     1566lapply (me_writeable_ok … Hext … Hvalid Hembed) #Hb2
     1567lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
     1568cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
     1569<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
     1570@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
     1571qed.
     1572
     1573(* Writing in the "extended" part of a memory preserves the whole memory injection *)
     1574lemma bestorev_memory_ext_to_memory_inj :
     1575  ∀E,mA,mB,mC.
     1576  ∀Hext:memory_ext E mA mB.
     1577  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
     1578  bestorev mB (mk_pointer wb wo) v = Some ? mC →
     1579  memory_inj E mA mC.
     1580#E #mA * #contentsB #nextblockB #HnextblockB #mC
     1581#Hext #wb #wo #v #Hwb #Hstore
     1582%
     1583[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
     1584elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
     1585#Hmem
     1586[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj
     1587whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
     1588normalize in ⊢ (% → ?); #Hlt_wb
     1589>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
     1590cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
     1591normalize nodelta
     1592[ 2: #Habsurd destruct (Habsurd) ]
     1593#Heq destruct (Heq)
     1594#b #b' #o' #Hembed @(Hcodomain … Hembed)
     1595qed.
     1596
     1597(* It even preserves memory extensions, with the same writeable blocks.  *)
     1598lemma bestorev_memory_ext_to_memory_ext :
     1599  ∀E,mA,mB.
     1600  ∀Hext:memory_ext E mA mB.
     1601  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
     1602  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
     1603  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
     1604#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
     1605%{(mk_memory_ext …
     1606      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
     1607      (me_writeable … Hext)
     1608      ?
     1609      (me_writeable_ok … Hext)
     1610 )} try @refl
     1611#b #Hmemb
     1612lapply (me_writeable_valid … Hext b Hmemb)
     1613lapply (me_writeable_valid … Hext wb Hmem)
     1614elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
     1615lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
     1616>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
     1617cases (if Zleb (low (contentsB wb)) (offv wo) 
     1618       then Zltb (offv wo) (high (contentsB wb)) 
     1619       else false)
     1620normalize [ 2: #Habsurd destruct (Habsurd) ]
     1621#Heq destruct (Heq) @Hb_valid
     1622qed.
     1623
     1624(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
     1625lemma storen_memory_ext_to_memory_ext :
     1626  ∀E,mA,l,mB,mC.
     1627  ∀Hext:memory_ext E mA mB.
     1628  ∀wb,wo. meml ? wb (me_writeable … Hext) →
     1629  storen mB (mk_pointer wb wo) l = Some ? mC →
     1630  memory_ext E mA mC.
     1631#E #mA #l elim l
     1632[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
     1633     @Hext
     1634| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
     1635     whd in ⊢ ((??%?) → ?);
     1636     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
     1637     cases (bestorev mB (mk_pointer wb wo) hd)
     1638     normalize nodelta
     1639     [ 1: #H #Habsurd destruct (Habsurd) ]
     1640     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
     1641     @(Hind … HextD … Hstore)
     1642     <Heq @Hmem
     1643] qed.     
     1644
     1645(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
     1646lemma store_value_of_type_memory_ext_to_memory_ext :
     1647  ∀E,mA,mB,mC.
     1648  ∀Hext:memory_ext E mA mB.
     1649  ∀wb,wo. meml ? wb (me_writeable … Hext) →
     1650  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
     1651  memory_ext E mA mC.
     1652#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
     1653cases ty
     1654[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1655| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1656whd in ⊢ ((??%?) → ?);
     1657[ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
     1658#Hstore
     1659@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
     1660qed.
     1661
     1662(* End of the memory injection-related stuff. *)
     1663(* ------------------------------------------ *)
     1664
     1665(* Lookup functions in list environments (used to type local variables in functions) *)     
     1666let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
     1667match l with
     1668[ nil ⇒ false
     1669| cons hd tl ⇒
     1670  let 〈id, ty〉 ≝ hd in
     1671  match identifier_eq SymbolTag i id with
     1672  [ inl Hid_eq ⇒ true
     1673  | inr Hid_neq ⇒ mem_assoc_env i tl 
     1674  ]
     1675].
     1676
     1677let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝
     1678match l with
     1679[ nil ⇒ None ?
     1680| cons hd tl ⇒
     1681  let 〈id, ty〉 ≝ hd in
     1682  match identifier_eq SymbolTag i id with
     1683  [ inl Hid_eq ⇒ Some ? ty
     1684  | inr Hid_neq ⇒ assoc_env i tl 
     1685  ]
     1686].
     1687
     1688(* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension
     1689   of the environment [e1] s.t. the new binders are in [new], and such that those
     1690   new binders are "writeable" in the memory extension [Hext] *)
     1691definition disjoint_extension ≝
     1692λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem).
     1693λ(new : list (ident × type)). λ(E:embedding). λ(Hext: memory_ext E m1 m2).
     1694  ∀id. match mem_assoc_env id new with
     1695       [ true ⇒
     1696           ∃b. lookup ?? e2 id = Some ? b
     1697            ∧ meml ? b (me_writeable … Hext)
     1698            ∧ lookup ?? e1 id = None ?
     1699       | false ⇒
     1700         match lookup ?? e1 id with
     1701         [ None ⇒ lookup ?? e2 id = None ?
     1702         | Some b1 ⇒
     1703           match lookup ?? e2 id with
     1704           [ None ⇒ False
     1705           | Some b2 ⇒
     1706             valid_block m1 b1 ∧
     1707             value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))
     1708           ]
     1709         ]
     1710       ].
     1711
     1712(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
     1713 * the variable is not in a local environment, then we search into the global one.
     1714 * A proper "extension" of a local environment should be such that the extension
     1715 * does not collide with a given global env.
     1716 * To see the details of why we need that, see [exec_lvalue'], Evar id case.
     1717 *)
     1718definition ext_fresh_for_genv ≝
     1719λ(ext : list (ident × type)). λ(ge : genv).
     1720  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.
     1721
     1722(* Any environment is a "disjoint" extension of itself with nothing. *)
     1723(*
     1724lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].
     1725#e #m #ty #id
     1726normalize in match (mem_assoc_env id []); normalize nodelta
     1727cases (lookup ?? e id) try //
     1728#b normalize nodelta
     1729% #ty cases (load_value_of_type ????)
     1730[ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj //
     1731cases (assoc_env id ty) //
     1732qed. *)
     1733
     1734
     1735(* "generic" simulation relation on [res ?] *)
     1736definition res_sim ≝
     1737  λ(A : Type[0]).
     1738  λ(eq : A → A → Prop).
     1739  λ(r1, r2 : res A).
     1740  ∀a1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2.
     1741
     1742(* Specialisation of [res_sim] to match [exec_expr] *)
     1743definition exec_expr_sim ≝ λE.
     1744  res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)).
     1745
     1746(* Specialisation of [res_sim] to match [exec_lvalue] *)
     1747definition exec_lvalue_sim ≝ λE.
     1748  res_sim (block × offset × trace)
     1749    (λr1,r2.
     1750      let 〈b1,o1,tr1〉 ≝ r1 in
     1751      let 〈b2,o2,tr2〉 ≝ r2 in
     1752      value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2).
     1753
     1754lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r.
     1755#ty #m #b #o cases (load_value_of_type ty m b o)
     1756[ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed.
     1757
     1758(*
     1759lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'.
     1760   env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
     1761   〈f',vars〉 = function_switch_removal f →
     1762   env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
     1763   environment_extension env env' vars.
     1764
     1765#f #f'
     1766cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append
     1767cases (fn_params f) cases (fn_vars f)
     1768[ 1: #vars >append_nil >append_nil >nil_append elim vars   
     1769   [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct //
     1770   | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq
     1771        whd in ⊢ ((???(???%)) → ?);
     1772 #Henv #Hswrem #Henv'
     1773#id   
     1774*)
     1775
     1776(*
     1777lemma substatement_fresh : ∀s,u.
     1778    fresh_for_statement s u →
     1779    substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
     1780#s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s)
     1781try /by I/
     1782[ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption
     1783| 2: *
     1784    [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
     1785         #Hfresh_e #Hfresh_args @conj try assumption
     1786         normalize nodelta in Hfresh_args;
     1787         >max_id_commutative in Hfresh_args; >max_id_one_neutral
     1788         #Hfresh_args         
     1789    | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
     1790         #Hfresh_e #H lapply (fresh_max_split ??? H) *
     1791         #Hfresh_ret #Hfresh_args @conj try @conj try assumption ]
     1792    elim args in Hfresh_args;
     1793    [ 1,3: //
     1794    | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???);
     1795            >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj
     1796            [ 1,3: @Hu
     1797            | 2,4: @Hind assumption ] ]
     1798| 3: #s1 #s2 #_ #_
     1799     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
     1800     whd in match (substatement_P ??); /2/
     1801| 4: #e #cond #iftrue #iffalse #_
     1802     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
     1803     #Hexpr #H2 lapply (fresh_max_split … H2) * /2/
     1804| 5,6: #e #stm #_
     1805     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/
     1806| 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) *
     1807      #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond
     1808      elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/
     1809| 8: #ret #H whd elim ret in H; try //     
     1810| 9: #expr #ls #Hind #H whd @conj
     1811     [ 1: elim (fresh_max_split … H) //
     1812     | 2: @Hind elim (fresh_max_split … H) // ]
     1813| 10: #l #body #Hind #H whd elim (fresh_max_split … H) //
     1814| 11: #sz #i #hd #tl #Hhd #Htl #H whd
     1815     elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj //
     1816     @Htl //
     1817] qed.
     1818*)
     1819
     1820(* Eliminating switches introduces fresh variables. [environment_extension] characterizes
     1821 * a local environment extended by some local variables. *)
     1822 
     1823
     1824(* lookup on environment extension *)
     1825(*
     1826lemma extension_lookup :
     1827  ∀map, map', ext, id, result.
     1828  environment_extension map map' ext →
     1829  lookup ?? map id = Some ? result →
     1830  lookup ?? map' id = Some ? result.
     1831#map #map' #ext #id #result #Hext lapply (Hext id)
     1832cases (mem_assoc_env ??) normalize nodelta
     1833[ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd)
     1834| 2: #H >H // ] qed.
     1835
     1836*)
     1837
     1838(* Extending a map by an empty list of variables yields an observationally equivalent
     1839 * environment. *)
     1840(*
     1841lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'.
     1842* #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H
     1843[ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
     1844     cases (lookup_opt block id map2) normalize
     1845     [ 1: >H #H2 >H2 @refl
     1846     | 2: #b >H cases v
     1847          [ 1: normalize * #H @(False_ind … H)
     1848          | 2: #block normalize // ] ]
     1849| 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
     1850     >H cases v normalize try //
     1851     #block cases (lookup_opt ? id map1) normalize try //
     1852     * #H @(False_ind … H)
     1853] qed. *)
     1854
     1855(* If two identifier maps are observationally equal, then they contain the same bocks.
     1856 * see maps_obsequiv.ma for the details of the proof. *)
     1857(*
     1858lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'.
     1859* #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold
     1860>Hfold @refl
     1861qed.
     1862*)
     1863
     1864(* Simulation relations. *)
     1865inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
     1866| swc_stop : ∀fvs.
     1867    switch_cont_sim fvs Kstop Kstop
     1868| swc_seq : ∀fvs,s,k,k',u,result.
     1869    fresh_for_statement s u →
     1870    switch_cont_sim fvs k k' →
     1871    switch_removal s fvs u = Some ? result →
     1872    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
     1873| swc_while : ∀fvs,e,s,k,k',u,result.
     1874    fresh_for_statement (Swhile e s) u →
     1875    switch_cont_sim fvs k k' →
     1876    switch_removal s fvs u = Some ? result →
     1877    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
     1878| swc_dowhile : ∀fvs,e,s,k,k',u,result.
     1879    fresh_for_statement (Sdowhile e s) u →
     1880    switch_cont_sim fvs k k' →
     1881    switch_removal s fvs u = Some ? result →
     1882    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
     1883| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
     1884    fresh_for_statement (Sfor Sskip e s1 s2) u →
     1885    switch_cont_sim fvs k k' →
     1886    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
     1887    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
     1888| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
     1889    fresh_for_statement (Sfor Sskip e s1 s2) u →
     1890    switch_cont_sim fvs k k' →
     1891    switch_removal s1 fvs u = Some ? result1 →
     1892    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
     1893    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
     1894| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
     1895    fresh_for_statement (Sfor Sskip e s1 s2) u →
     1896    switch_cont_sim fvs k k' →
     1897    switch_removal s1 fvs u = Some ? result1 →
     1898    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
     1899    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
     1900| swc_switch : ∀fvs,k,k'.
     1901    switch_cont_sim fvs k k' →
     1902    switch_cont_sim fvs (Kswitch k) (Kswitch k')
     1903| swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
     1904    switch_cont_sim fvs k k' →
     1905    (* /!\ Update [en] with [fvs'] ... *)
     1906    switch_cont_sim
     1907      (map … (fst ??) (\snd (function_switch_removal f)))
     1908      (Kcall r f en k)
     1909      (Kcall r (\fst (function_switch_removal f)) en' k').
     1910
     1911
     1912(*
     1913 en' = exec_alloc_variables en m (\snd (function_switch_removal f))
     1914 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
     1915        variable dans en'.
     1916
     1917        1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que
     1918           dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
     1919           de savoir que :
     1920           si je lookup une variable générée à partir d'un univers frais dans l'environement en',
     1921           alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
     1922           et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
     1923           et à etre "(function_switch_removal f)-contained".
     1924
     1925        2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
     1926           et l'update n'altèrent pas le comportement du reste du programme.
     1927
     1928        relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
     1929                   depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
     1930                   en particulier, si u est frais pour S1 u est frais pour S0.
     1931
     1932        Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
     1933                    "environment_extension en en' (\fst (\fst (switch_removal s u)))"
     1934                   
     1935 ---------------------------------------------------------------
     1936 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
     1937   et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
     1938   on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
     1939   en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
     1940*)
     1941
     1942inductive switch_state_sim : state → state → Prop ≝
     1943| sws_state : ∀u,f,s,k,k',m,m',result.
     1944    ∀env, env', f', vars.
     1945    ∀E:embedding.   
     1946    ∀Hext:memory_ext E m m'.
     1947    fresh_for_statement s u →
     1948    (*
     1949    env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
     1950    env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
     1951    *)
     1952    〈f',vars〉 = function_switch_removal f →
     1953    disjoint_extension env m env' m' vars E Hext →
     1954    switch_removal s (map ?? (fst ??) vars) u = Some ? result →
     1955    switch_cont_sim (map ?? (fst ??) vars) k k' →
     1956    switch_state_sim
     1957      (State f s k env m)
     1958      (State f' (ret_st ? result) k' env' m')
     1959| sws_callstate : ∀vars, fd,args,k,k',m.
     1960    switch_cont_sim vars k k' →
     1961    switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m)
     1962| sws_returnstate : ∀vars,res,k,k',m.
     1963    switch_cont_sim vars k k' →
     1964    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
     1965| sws_finalstate : ∀r.
     1966    switch_state_sim (Finalstate r) (Finalstate r).
     1967
     1968lemma call_cont_swremoval : ∀fv,k,k'.
     1969  switch_cont_sim fv k k' →
     1970  switch_cont_sim fv (call_cont k) (call_cont k').
     1971#fv #k0 #k0' #K elim K /2/
     1972qed.
     1973
     1974(* [eventually ge P s tr] states that after a finite number of [exec_step], the
     1975   property P on states will be verified. *)
     1976inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
     1977| eventually_base : ∀s,t,s'.
     1978    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
     1979    P s' →
     1980    eventually ge P s t
     1981| eventually_step : ∀s,t,s',t',trace.
     1982    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
     1983    eventually ge P s' t' →
     1984    trace = (t ⧺ t') →
     1985    eventually ge P s trace.
     1986
     1987(* [eventually] is not so nice to use directly, we would like to make the mandatory
     1988 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
     1989   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
     1990lemma eventually_now : ∀ge,P,s,t.
     1991  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
     1992   eventually ge P s t.
     1993#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
     1994qed.
     1995(*   
     1996lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
     1997                                      ∃t'.eventually ge P s (t ⧺ t').
     1998#ge #P #s #t * #s' * #Hexec #HP %{E0} normalize >(append_nil ? t) %1{????? Hexec HP}
     1999qed.
     2000*)
     2001lemma eventually_later : ∀ge,P,s,t.
     2002   (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) →
     2003    eventually ge P s t.
     2004#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
     2005try assumption
     2006qed.
     2007
     2008(* lift value_eq to option block *)
     2009definition option_block_eq ≝ λE,ob1,ob2.
     2010match ob1 with
     2011[ None ⇒
     2012  match ob2 with
     2013  [ None ⇒ True
     2014  | Some _ ⇒ False ]
     2015| Some b1 ⇒
     2016  match ob2 with
     2017  [ None ⇒ False
     2018  | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))  ]
     2019].
     2020
     2021definition value_eq_opt ≝ λE,ov1,ov2.
     2022match ov1 with
     2023[ None ⇒
     2024  match ov2 with
     2025  [ None ⇒ True
     2026  | Some _ ⇒ False ]
     2027| Some v1 ⇒
     2028  match ov2 with
     2029  [ None ⇒ False
     2030  | Some v2 ⇒
     2031    value_eq E v1 v2 ]
     2032].
     2033
     2034record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
     2035  rg_find_symbol: ∀s.
     2036    option_block_eq E (find_symbol ? ge s) (find_symbol ? ge' s);
     2037  rg_find_funct: ∀v,f.
     2038    find_funct ? ge v = Some ? f →
     2039    find_funct ? ge' v = Some ? (t f);
     2040  rg_find_funct_ptr: ∀b,f.
     2041    find_funct_ptr ? ge b = Some ? f →
     2042    find_funct_ptr ? ge' b = Some ? (t f)
     2043}.
     2044
     2045lemma exec_lvalue_expr_elim :
     2046  ∀E,r1,r2,Pok,Qok.
     2047  ∀H:exec_lvalue_sim E r1 r2.
     2048  (∀bo1,bo2,tr.
     2049    let 〈b1,o1〉 ≝ bo1 in
     2050    let 〈b2,o2〉 ≝ bo2 in
     2051    value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) →
     2052    match Pok 〈bo1,tr〉 with
     2053    [ Error err ⇒ True
     2054    | OK vt1 ⇒
     2055      let 〈val1,trace1〉 ≝ vt1 in
     2056      match Qok 〈bo2,tr〉 with
     2057      [ Error err ⇒ False
     2058      | OK vt2 ⇒
     2059        let 〈val2,trace2〉 ≝ vt2 in
     2060        trace1 = trace2 ∧ value_eq E val1 val2     
     2061      ]
     2062    ]) →
     2063  exec_expr_sim E
     2064    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
     2065    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
     2066#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
     2067elim r1
     2068[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
     2069| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
     2070     * #a2 * #Hr2 >Hr2 normalize nodelta
     2071     elim a1 * #b1 #o1 #tr1
     2072     elim a2 * #b2 #o2 #tr2 normalize nodelta
     2073     * #Hvalue_eq #Htrace_eq #H2
     2074     destruct (Htrace_eq)
     2075     lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq)
     2076     cases (Pok 〈b1, o1, tr2〉)
     2077     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
     2078     | 1: * #v1 #tr1' normalize nodelta #H3 whd
     2079          * #v1' #tr1'' #Heq destruct (Heq)
     2080          cases (Qok 〈b2,o2,tr2〉) in H3;
     2081          [ 2: #error #Hfalse @(False_ind … Hfalse)
     2082          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
     2083               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
     2084] ] ] qed.
     2085
     2086lemma exec_expr_expr_elim :
     2087  ∀E,r1,r2,Pok,Qok.
     2088  ∀H:exec_expr_sim E r1 r2.
     2089  (∀v1,v2,trace.
     2090    value_eq E v1 v2 →
     2091    match Pok 〈v1,trace〉 with
     2092    [ Error err ⇒ True
     2093    | OK vt1 ⇒
     2094      let 〈val1,trace1〉 ≝ vt1 in
     2095      match Qok 〈v2,trace〉 with
     2096      [ Error err ⇒ False
     2097      | OK vt2 ⇒
     2098        let 〈val2,trace2〉 ≝ vt2 in
     2099        trace1 = trace2 ∧ value_eq E val1 val2     
     2100      ]
     2101    ]) →
     2102  exec_expr_sim E
     2103    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
     2104    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
     2105#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
     2106elim r1
     2107[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
     2108| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
     2109     * #a2 * #Hr2 >Hr2 normalize nodelta
     2110     elim a1 #v1 #tr1
     2111     elim a2 #v2 #tr2 normalize nodelta
     2112     * #Hvalue_eq #Htrace_eq #H2
     2113     destruct (Htrace_eq)
     2114     lapply (H2 v1 v2 tr2 Hvalue_eq)
     2115     cases (Pok 〈v1, tr2〉)
     2116     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
     2117     | 1: * #v1 #tr1' normalize nodelta #H3 whd
     2118          * #v1' #tr1'' #Heq destruct (Heq)
     2119          cases (Qok 〈v2,tr2〉) in H3;
     2120          [ 2: #error #Hfalse @(False_ind … Hfalse)
     2121          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
     2122               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
     2123] ] ] qed.
     2124
     2125(* Commutation results of standard binary operations with value_eq. *)
     2126lemma unary_operation_value_eq :
     2127  ∀E,op,v1,v2,ty.
     2128   value_eq E v1 v2 →
     2129   ∀r1.
     2130   sem_unary_operation op v1 ty = Some ? r1 →
     2131    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
     2132#E #op #v1 #v2 #ty #Hvalue_eq #r1
     2133inversion Hvalue_eq
     2134[ 1: #v #Hv1 #Hv2 #_ destruct
     2135     cases op normalize
     2136     [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2137          normalize #Habsurd destruct (Habsurd)
     2138     | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2139          normalize #Habsurd destruct (Habsurd)
     2140     | 2: #Habsurd destruct (Habsurd) ]
     2141| 2: #vsz #i #Hv1 #Hv2 #_
     2142     cases op
     2143     [ 1: cases ty
     2144          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2145          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
     2146          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
     2147               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
     2148               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
     2149               //
     2150          | *: #Habsurd destruct (Habsurd) ]
     2151     | 2: whd in match (sem_unary_operation ???);     
     2152          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
     2153     | 3: whd in match (sem_unary_operation ???);
     2154          cases ty
     2155          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2156          normalize nodelta
     2157          whd in ⊢ ((??%?) → ?);
     2158          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
     2159               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
     2160          | *: #Habsurd destruct (Habsurd) ] ]
     2161| 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
     2162     cases op normalize nodelta
     2163     [ 1: cases ty
     2164          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2165          whd in match (sem_notbool ??);
     2166          #Heq1 destruct
     2167          cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
     2168     | 2: normalize #Habsurd destruct (Habsurd)
     2169     | 3: cases ty
     2170          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2171          whd in match (sem_neg ??);
     2172          #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
     2173| 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
     2174     cases op normalize nodelta
     2175     [ 1: cases ty
     2176          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2177          whd in match (sem_notbool ??);
     2178          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
     2179     | 2: normalize #Habsurd destruct (Habsurd)
     2180     | 3: cases ty
     2181          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2182          whd in match (sem_neg ??);
     2183          #Heq1 destruct ]
     2184| 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
     2185     cases op normalize nodelta
     2186     [ 1: cases ty
     2187          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2188          whd in match (sem_notbool ??);         
     2189          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
     2190     | 2: normalize #Habsurd destruct (Habsurd)
     2191     | 3: cases ty
     2192          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2193          whd in match (sem_neg ??);         
     2194          #Heq1 destruct ]
     2195]
     2196qed.
     2197
     2198(* A cleaner version of inversion for [value_eq] *)
     2199lemma value_eq_inversion :
     2200  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
     2201  (∀v. P Vundef v) →
     2202  (∀sz,i. P (Vint sz i) (Vint sz i)) →
     2203  (∀f. P (Vfloat f) (Vfloat f)) →
     2204  (P Vnull Vnull) →
     2205  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
     2206  P v1 v2.
     2207#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
     2208inversion Heq
     2209[ 1: #v #Hv1 #Hv2 #_ destruct @H1
     2210| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
     2211| 3: #f #Hv1 #Hv2 #_ destruct @H3
     2212| 4: #Hv1 #Hv2 #_ destruct @H4
     2213| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
     2214
     2215(* value_eq lifts to addition *)
     2216lemma add_value_eq :
     2217  ∀E,v1,v2,v1',v2',ty1,ty2,m1,m2.
     2218   value_eq E v1 v2 →
     2219   value_eq E v1' v2' →
     2220   memory_inj E m1 m2 → (* This injection seems useless TODO *)
     2221   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
     2222           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
     2223#E #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
     2224@(value_eq_inversion E … Hvalue_eq1)
     2225[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     2226[ 1: whd in match (sem_add ????); normalize nodelta
     2227     cases (classify_add ty1 ty2) normalize nodelta
     2228     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
     2229     #Habsurd destruct (Habsurd)
     2230| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     2231     cases (classify_add ty1 ty2) normalize nodelta     
     2232     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2233     [ 2,3,5: #Habsurd destruct (Habsurd) ]
     2234     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2235     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
     2236     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
     2237     [ 1: @intsize_eq_elim_elim
     2238          [ 1: #_ #Habsurd destruct (Habsurd)
     2239          | 2: #Heq destruct (Heq) normalize nodelta
     2240               #Heq destruct (Heq)
     2241               /3 by ex_intro, conj, vint_eq/ ]
     2242     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
     2243          /3 by ex_intro, conj, vint_eq/
     2244     | 3: #Heq destruct (Heq)
     2245          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
     2246          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
     2247          @vptr_eq whd in match (pointer_translation ??);
     2248          cases (E b1') in Hembed;
     2249          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
     2250          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     2251               whd in match (shift_pointer_n ????);
     2252               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
     2253                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i))
     2254               [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ]
     2255               #Heq >Heq @refl ]
     2256     ]
     2257| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     2258     cases (classify_add ty1 ty2) normalize nodelta     
     2259     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2260     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2261     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2262     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2263     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     2264     #Heq destruct (Heq)
     2265     /3 by ex_intro, conj, vfloat_eq/
     2266| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     2267     cases (classify_add ty1 ty2) normalize nodelta     
     2268     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2269     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     2270     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2271     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2272     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2273     @eq_bv_elim
     2274     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
     2275     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
     2276| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     2277     cases (classify_add ty1 ty2) normalize nodelta
     2278     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2279     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     2280     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2281     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2282     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2283     #Heq destruct (Heq)
     2284     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
     2285     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
     2286     elim p1 in Hembed; #b1 #o1 normalize nodelta
     2287     cases (E b1)
     2288     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
     2289     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     2290          normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
     2291          @refl
     2292     ]
     2293] qed.
     2294         
     2295(* TODO all other 10 binary operations. Then wrap this in [binary_operation_value_eq] *)
     2296
     2297
     2298(* Commutation result for binary operators. *)
     2299lemma binary_operation_value_eq :
     2300  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
     2301   value_eq E v1 v2 →
     2302   value_eq E v1' v2' →
     2303   memory_inj E m1 m2 →
     2304   ∀r1.
     2305   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
     2306   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
     2307#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
     2308cases op
     2309whd in match (sem_binary_operation ??????);
     2310whd in match (sem_binary_operation ??????);
     2311@cthulhu
     2312qed.
     2313
     2314 
     2315(* Simulation relation on expressions *)
     2316lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
     2317  ∀E:embedding.
     2318  ∀Hext:memory_ext E m1 m2.
     2319  switch_removal_globals E ? fundef_switch_removal ge ge' →
     2320  disjoint_extension en1 m1 en2 m2 ext E Hext →
     2321  ext_fresh_for_genv ext ge →
     2322  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
     2323  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
     2324#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
     2325@expr_lvalue_ind_combined
     2326[ 1: #csz #cty #i #a1
     2327     whd in match (exec_expr ????); elim cty
     2328     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2329     normalize nodelta
     2330     [ 2: cases (eq_intsize csz sz) normalize nodelta
     2331          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
     2332          | 2: #Habsurd destruct (Habsurd) ]
     2333     | 4,5,6: #_ #H destruct (H)
     2334     | *: #H destruct (H) ]
     2335| 2: #ty #fl #a1
     2336     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
     2337| 3: *
     2338  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
     2339  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2340  #ty whd in ⊢ (% → ?); #Hind try @I
     2341  whd in match (Plvalue ???);
     2342  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
     2343       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
     2344       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
     2345       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
     2346           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
     2347           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
     2348           whd in match (load_value_of_type' ???);
     2349           whd in match (load_value_of_type' ???);
     2350           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
     2351           cases (load_value_of_type ty m1 bl1 o1)
     2352           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2353           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
     2354                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
     2355                    normalize /4 by ex_intro, conj/
     2356  ] ] ]
     2357| 4: #v #ty whd * * #b1 #o1 #tr1
     2358     whd in match (exec_lvalue' ?????);
     2359     whd in match (exec_lvalue' ?????);
     2360     lapply (Hdisjoint v)
     2361     lapply (Hext_fresh_for_genv v)
     2362     cases (mem_assoc_env v ext) #Hglobal
     2363     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
     2364          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
     2365          >(Hglobal (refl ??)) normalize
     2366          #Habsurd destruct (Habsurd)
     2367     | 2: normalize nodelta
     2368          cases (lookup ?? en1 v) normalize nodelta
     2369          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
     2370               lapply (rg_find_symbol … Hrelated v)
     2371               cases (find_symbol ???) normalize
     2372               [ 1: #_ #Habsurd destruct (Habsurd)
     2373               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
     2374                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
     2375                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
     2376                         %{〈block',mk_offset OZ,[]〉} @conj try @refl
     2377                         normalize /2/
     2378                ] ]
     2379         | 2: #block
     2380              cases (lookup ?? en2 v) normalize nodelta
     2381              [ 1: #Hfalse @(False_ind … Hfalse)
     2382              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
     2383                   %{〈b, zero_offset, E0〉} @conj try @refl
     2384                   normalize /2/
     2385    ] ] ]
     2386| 5: #e #ty whd in ⊢ (% → %);
     2387     whd in match (exec_lvalue' ?????);
     2388     whd in match (exec_lvalue' ?????);
     2389     cases (exec_expr ge en1 m1 e)
     2390     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
     2391          * elim v1 normalize nodelta
     2392          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
     2393          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
     2394          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
     2395          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
     2396          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
     2397               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
     2398               #Hvalue_eq normalize
     2399               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
     2400               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
     2401               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
     2402               %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
     2403               normalize @conj // ]
     2404     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
     2405| 6: #ty #e #ty'
     2406     #Hsim @(exec_lvalue_expr_elim … Hsim)
     2407     cases ty
     2408     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2409     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
     2410     #tr #H @conj try @refl try assumption
     2411| 7: #ty #op #e
     2412     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
     2413     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
     2414     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
     2415     [ 1: #_ @I
     2416     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
     2417           normalize /2/ ]
     2418| *: @cthulhu ] qed.
     2419
     2420(* TODO: Old cases, to be ported to memory injection.
     2421| 8: #ty #op #e1 #e2 #Hind1 #Hind2
     2422     whd in match (exec_expr ge ???);   
     2423     whd in match (exec_expr ge' ???);
     2424     @(exec_expr_expr_elim … Hind1)
     2425     cases (exec_expr ge en1 m1 e2) in Hind2;
     2426     [ 2: #error normalize //
     2427     | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 *
     2428          #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq'
     2429          >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????);
     2430
     2431
     2432| 9: #ty #castty #e #Hind
     2433     whd in match (exec_expr ge ???);   
     2434     whd in match (exec_expr ge' ???);
     2435     cases Hind
     2436     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2437     | 1: cases (exec_expr ge en m e)
     2438          [ 2: #error #_ @SimFail /2 by ex_intro/
     2439          | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
     2440          ]
     2441     ]
     2442| 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3
     2443     whd in match (exec_expr ge ???);   
     2444     whd in match (exec_expr ge' ???);
     2445     cases Hind1
     2446     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2447     | 1: cases (exec_expr ge en m e1)
     2448          [ 2: #error #_ @SimFail /2 by ex_intro/
     2449          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
     2450               normalize nodelta
     2451               cases (exec_bool_of_val ??)
     2452               [ 2: #error @SimFail /2 by ex_intro/
     2453               | 1: * whd in match (m_bind ?????); normalize nodelta
     2454                    [ 1: cases Hind2
     2455                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2456                         | 1: cases (exec_expr ge en m e2)
     2457                              [ 2: #error #_  @SimFail /2 by ex_intro/
     2458                              | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))                                   
     2459                                   @SimOk normalize nodelta #a2
     2460                                   whd in match (m_bind ?????); // ]
     2461                         ]
     2462                    | 2: cases Hind3
     2463                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2464                         | 1: cases (exec_expr ge en m e3)
     2465                              [ 2: #error #_  @SimFail /2 by ex_intro/
     2466                              | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3)))
     2467                                   @SimOk normalize nodelta #a3
     2468                                   whd in match (m_bind ?????); // ]
     2469                         ]
     2470     ] ] ] ]                     
     2471| 11: #ty #e1 #e2 #Hind1 #Hind2
     2472     whd in match (exec_expr ge ???);   
     2473     whd in match (exec_expr ge' ???);
     2474     cases Hind1
     2475     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2476     | 1: cases (exec_expr ge en m e1)
     2477          [ 2: #error #_ @SimFail /2 by ex_intro/
     2478          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
     2479               normalize nodelta
     2480               cases (exec_bool_of_val ??)
     2481               [ 2: #error @SimFail /2 by ex_intro/
     2482               | 1: * whd in match (m_bind ?????);
     2483                    [ 2: @SimOk // ]
     2484                    cases Hind2
     2485                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2486                    | 1: cases (exec_expr ge en m e2)
     2487                         [ 2: #error #_  @SimFail /2 by ex_intro/
     2488                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
     2489                              @SimOk #a2
     2490                              whd in match (m_bind ?????); //
     2491     ] ] ] ] ]
     2492| 12: #ty #e1 #e2 #Hind1 #Hind2
     2493     whd in match (exec_expr ge ???);   
     2494     whd in match (exec_expr ge' ???);
     2495     cases Hind1
     2496     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2497     | 1: cases (exec_expr ge en m e1)
     2498          [ 2: #error #_ @SimFail /2 by ex_intro/
     2499          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
     2500               normalize nodelta
     2501               cases (exec_bool_of_val ??)
     2502               [ 2: #error @SimFail /2 by ex_intro/
     2503               | 1: * whd in match (m_bind ?????);
     2504                    [ 1: @SimOk // ]
     2505                    cases Hind2
     2506                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2507                    | 1: cases (exec_expr ge en m e2)
     2508                         [ 2: #error #_  @SimFail /2 by ex_intro/
     2509                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
     2510                              @SimOk #a2
     2511                              whd in match (m_bind ?????); //
     2512     ] ] ] ] ]
     2513| 13: #ty #sizeof_ty
     2514     whd in match (exec_expr ge ???);   
     2515     whd in match (exec_expr ge' ???);
     2516     @SimOk //
     2517| 14: #ty #e #ty' #fld #Hind
     2518     whd in match (exec_lvalue' ge ????);
     2519     whd in match (exec_lvalue' ge' ????);
     2520     whd in match (typeof ?);
     2521     cases ty' in Hind;
     2522     [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
     2523     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
     2524     normalize nodelta #Hind
     2525     try (@SimFail /2 by ex_intro/)
     2526     whd in match (exec_lvalue ????);
     2527     whd in match (exec_lvalue ????);     
     2528     cases Hind
     2529     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2530     | 1,3: cases (exec_lvalue' ge en m e ?)
     2531         [ 2,4: #error #_ @SimFail /2 by ex_intro/
     2532         | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
     2533     ] ]
     2534| 15: #ty #l #e #Hind
     2535     whd in match (exec_expr ge ???);
     2536     whd in match (exec_expr ge' ???);
     2537     cases Hind
     2538     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2539     | 1: cases (exec_expr ge en m e)
     2540        [ 2: #error #_ @SimFail /2 by ex_intro/
     2541        | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
     2542     ] ]
     2543| 16: *
     2544  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
     2545  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2546  #ty normalize in ⊢ (% → ?);
     2547  [ 1,2: #_ @SimOk #a normalize //
     2548  | 3,4,13: #H @(False_ind … H)
     2549  | *: #_ @SimFail /2 by ex_intro/
     2550  ]
     2551] qed. *)
     2552
     2553(*
     2554lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
     2555related_globals ? fundef_switch_removal ge ge' →
     2556∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
     2557#ge #ge' #en #m #Hrelated #args
     2558elim args
     2559[ 1: /3/
     2560| 2: #hd #tl #Hind normalize
     2561     elim (sim_related_globals ge ge' en m Hrelated)
     2562     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
     2563     cases (exec_expr ge en m hd)
     2564     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
     2565     | 1: * #val_hd #trace_hd normalize nodelta
     2566          cases Hind
     2567          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
     2568          | 1: cases (exec_exprlist ge en m tl)
     2569               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
     2570               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
     2571                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
     2572                    cases Hexec_hd
     2573                    [ 2: * #error #Habsurd destruct (Habsurd)
     2574                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
     2575] ] ] ] qed.
     2576*)
     2577
     2578(* The return type of any function is invariant under switch removal *)
     2579lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
     2580#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
     2581qed.
     2582
     2583(* Similar stuff for fundefs *)
     2584lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
     2585* // qed.
     2586
     2587(*
    8152588lemma expr_fresh_lift :
    8162589  ∀e,u,id.
     
    8282601cases (leb p p') normalize nodelta
    8292602[ 1: @H2 | 2: @H1 ]
    830 qed.
    831 
     2603qed. *)
    8322604
    8332605lemma while_fresh_lift : ∀e,s,u.
    8342606   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
    835 #e #s #u normalize #Hfresh_expr
    836 elim (max_of_statement s (an_identifier SymbolTag one)) #p
    837 #Hfresh_p
    838 @expr_fresh_lift
    839 [ 2: //
    840 | 1: @Hfresh_expr ]
    841 qed.
    842 
    843 (*   
    844 theorem switch_removal_correction : ∀ge, ge', u.
    845   related_globals ? (λclfd.\fst (fundef_switch_removal clfd u)) ge ge' →
    846   ∀s1, s1', tr, s2.
     2607#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
     2608cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
     2609cases (leb e s) try /2/
     2610qed.
     2611
     2612(*
     2613lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
     2614#e0 #s0 #us0 normalize
     2615cases (switch_removal s0 us0) * #body #newvars #u' normalize //
     2616qed.*)
     2617
     2618lemma dowhile_fresh_lift : ∀e,s,u.
     2619   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
     2620#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
     2621cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
     2622cases (leb e s) try /2/
     2623qed.
     2624(*
     2625lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
     2626#e0 #s0 #us0 normalize
     2627cases (switch_removal s0 us0) * #body #newvars #u' normalize //
     2628qed.*)
     2629
     2630lemma for_fresh_lift : ∀cond,step,body,u.
     2631  fresh_for_statement step u →
     2632  fresh_for_statement body u →
     2633  fresh_for_expression cond u →
     2634  fresh_for_statement (Sfor Sskip cond step body) u.
     2635#cond #step #body #u
     2636whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
     2637cases (max_of_statement step) #s
     2638cases (max_of_statement body) #b
     2639cases (max_of_expr cond) #c
     2640whd in match (max_of_statement Sskip);
     2641>(max_id_commutative least_identifier)
     2642>max_id_one_neutral normalize nodelta
     2643normalize elim u #u
     2644cases (leb s b) cases (leb c b) cases (leb c s) try /2/
     2645qed.
     2646
     2647(*
     2648lemma for_commute : ∀e,stm1,stm2,u,uA.
     2649   (uA=\snd  (switch_removal stm1 u)) →
     2650   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
     2651#e #stm1 #stm2 #u #uA #HuA
     2652whd in match (sw_rem (Sfor ????) u);
     2653whd in match (switch_removal ??);   
     2654destruct
     2655normalize in match (\snd (switch_removal Sskip u));
     2656whd in match (sw_rem stm1 u);
     2657cases (switch_removal stm1 u)
     2658* #stm1' #fresh_vars #uA normalize nodelta
     2659whd in match (sw_rem stm2 uA);
     2660cases (switch_removal stm2 uA)
     2661* #stm2' #fresh_vars2 #uB normalize nodelta
     2662//
     2663qed.*)
     2664
     2665(*
     2666lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
     2667*
     2668[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
     2669| 2: #e1 #e2 #u #_
     2670     whd in match (sw_rem ??);
     2671     whd in match (is_Sskip ?);
     2672     try /2 by refl, ex_intro/
     2673| 3: #ret #f #args #u
     2674     whd in match (sw_rem ??);
     2675     whd in match (is_Sskip ?);
     2676     try /2 by refl, ex_intro/
     2677| 4: #s1 #s2 #u
     2678     whd in match (sw_rem ??);
     2679     whd in match (switch_removal ??);     
     2680     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
     2681     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
     2682     whd in match (is_Sskip ?);
     2683     try /2 by refl, ex_intro/
     2684| 5: #e #s1 #s2 #u #_
     2685     whd in match (sw_rem ??);
     2686     whd in match (switch_removal ??);     
     2687     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     2688     cases (switch_removal ? ?) * #e #f #h normalize nodelta
     2689     whd in match (is_Sskip ?);
     2690     try /2 by refl, ex_intro/
     2691| 6,7: #e #s #u #_
     2692     whd in match (sw_rem ??);
     2693     whd in match (switch_removal ??);     
     2694     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     2695     whd in match (is_Sskip ?);
     2696     try /2 by refl, ex_intro/
     2697| 8: #s1 #e #s2 #s3 #u #_     
     2698     whd in match (sw_rem ??);
     2699     whd in match (switch_removal ??);     
     2700     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     2701     cases (switch_removal ? ?) * #e #f #g normalize nodelta
     2702     cases (switch_removal ? ?) * #i #j #k normalize nodelta
     2703     whd in match (is_Sskip ?);
     2704     try /2 by refl, ex_intro/
     2705| 9,10: #u #_     
     2706     whd in match (is_Sskip ?);
     2707     try /2 by refl, ex_intro/
     2708| 11: #e #u #_
     2709     whd in match (is_Sskip ?);
     2710     try /2 by refl, ex_intro/
     2711| 12: #e #ls #u #_
     2712     whd in match (sw_rem ??);
     2713     whd in match (switch_removal ??);
     2714     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
     2715     cases (fresh ??) #e #f normalize nodelta
     2716     normalize in match (simplify_switch ???);
     2717     cases (fresh ? f) #g #h normalize nodelta
     2718     cases (produce_cond ????) * #k #l #m normalize nodelta
     2719     whd in match (is_Sskip ?);
     2720     try /2 by refl, ex_intro/
     2721| 13,15: #lab #st #u #_
     2722     whd in match (sw_rem ??);
     2723     whd in match (switch_removal ??);
     2724     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     2725     whd in match (is_Sskip ?);
     2726     try /2 by refl, ex_intro/
     2727| 14: #lab #u     
     2728     whd in match (is_Sskip ?);
     2729     try /2 by refl, ex_intro/ ]
     2730qed.
     2731*)
     2732
     2733(*
     2734lemma sw_rem_commute : ∀stm,u.
     2735  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
     2736#stm #u whd in match (sw_rem stm u); // qed.
     2737*)
     2738
     2739lemma fresh_for_statement_inv :
     2740  ∀u,s. fresh_for_statement s u →
     2741        match u with
     2742        [ mk_universe p ⇒ le (p0 one) p ].
     2743* #p #s whd in match (fresh_for_statement ??);
     2744cases (max_of_statement s) #s
     2745normalize /2/ qed.
     2746
     2747lemma fresh_for_Sskip :
     2748  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
     2749#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
     2750
     2751lemma fresh_for_Sbreak :
     2752  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
     2753#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
     2754
     2755lemma fresh_for_Scontinue :
     2756  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
     2757#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
     2758
     2759(*
     2760lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
     2761#s #u elim (switch_removal s u) * #res #fvs #u'
     2762%{res} %{fvs} %{u'} //
     2763qed.
     2764
     2765lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
     2766#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
     2767%{res} %{fvs} %{u'} //
     2768qed.
     2769*)
     2770
     2771lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
     2772#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
     2773#s #lab #u' %{s} %{lab} %{u'} //
     2774qed.
     2775
     2776(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
     2777lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
     2778* * *
     2779[ 1,5,9: #H @(False_ind … (H (refl ??)))
     2780| *: #_ normalize @refl ]
     2781qed.
     2782
     2783lemma exec_expr_int : ∀ge,e,m,expr.
     2784    (∃sz,n,tr. exec_expr ge e m expr = (OK ? 〈Vint sz n, tr〉)) ∨ (∀sz,n,tr. exec_expr ge e m expr ≠ (OK ? 〈Vint sz n, tr〉)).
     2785#ge #e #m #expr cases (exec_expr ge e m expr)
     2786[ 2: #error %2 #sz #n #tr % #H destruct (H)
     2787| 1: * #val #trace cases val
     2788     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
     2789     | 3: #fl | 4: | 5: #ptr ]
     2790     %2 #sz #n #tr % #H destruct (H)
     2791] qed.
     2792
     2793(*
     2794lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
     2795  exec_expr ge e m cond = OK ? 〈v,tr〉 →
     2796  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
     2797  exec_expr ge' e m cond = OK ? 〈v,tr〉.
     2798#ge #ge' #e #m #cond #v #tr #H *
     2799[ 1: #Hsim >(Hsim ? H) //
     2800| 2: * #error >H #Habsurd destruct (Habsurd) ]
     2801qed. *)
     2802
     2803(*
     2804lemma switch_simulation :
     2805∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
     2806 switch_cont_sim k k' →
     2807 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
     2808 fresh_for_statement (Sswitch cond switchcases) u →
     2809 ∃tr'.
     2810 (eventually ge'
     2811  (λs2':state
     2812   .switch_state_sim
     2813    (State f
     2814     (seq_of_labeled_statement (select_switch condsz condval switchcases))
     2815     (Kswitch k) e m) s2')
     2816  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
     2817  tr').
     2818#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
     2819whd in match (sw_rem (Sswitch cond switchcases) u);
     2820whd in match (switch_removal (Sswitch cond switchcases) u);
     2821cases switchcases in Hfresh;
     2822[ 1: #default_statement #Hfresh_for_default
     2823     whd in match (switch_removal_branches ??);
     2824     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
     2825     elim (switch_removal_eq default_statement u)
     2826     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
     2827     normalize nodelta
     2828     cut (u' = (\snd (switch_removal default_statement u)))
     2829     [ 1: >Hdefault_statement_eq // ] #Heq_u'
     2830     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
     2831     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
     2832     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
     2833     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
     2834     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
     2835     normalize nodelta
     2836     whd in match (simplify_switch (Expr ??) ?? uv2);
     2837     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
     2838     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
     2839     -Hfreshness #Heq_uv3
     2840     normalize nodelta whd in match (add_starting_lbl_list ????);
     2841     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
     2842     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
     2843     -Hfreshness #Heq_uv4
     2844     normalize nodelta
     2845     @(eventually_later ge' ?? E0)
     2846     whd in match (exec_step ??);
     2847     %{(State (function_switch_removal f)
     2848          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
     2849          (Kseq
     2850          (Ssequence
     2851            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
     2852            (Slabel exit_label Sskip))
     2853          k') e m)} @conj try //
     2854     @(eventually_later ge' ?? E0)
     2855     whd in match (exec_step ??);
     2856     
     2857@chthulhu | @chthulhu
     2858qed. *)
     2859
     2860
     2861
     2862(* Main theorem. To be ported and completed to memory injections. TODO *)
     2863(*
     2864theorem switch_removal_correction : ∀ge, ge'.
     2865  related_globals ? fundef_switch_removal ge ge' →
     2866  ∀s1, s1', tr, s2.
    8472867  switch_state_sim s1 s1' →
    8482868  exec_step ge s1 = Value … 〈tr,s2〉 →
    8492869  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
    850 #ge #ge' #u #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
     2870#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
    8512871inversion Hsim_state
    8522872[ 1: (* regular state *)
    853   #uf #us #uk #f #s #k #k' #e #m #Huf_fresh #Hus_fresh #Huk_fresh #Hsim_cont #Hs1_eq #Hs1_eq' #_
     2873  #u #f #s #k #k' #m #m' #result #en #en' #f' #vars
     2874  #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_
     2875
     2876  lapply (sim_related_globals ge ge' e m Hrelated) *
     2877  #Hexpr_related #Hlvalue_related
    8542878  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
    855   cases s in Hus_fresh;
     2879  cases s in Hu_fresh Heq_env;
     2880 
     2881
     2882theorem switch_removal_correction : ∀ge, ge'.
     2883  related_globals ? fundef_switch_removal ge ge' →
     2884  ∀s1, s1', tr, s2.
     2885  switch_state_sim s1 s1' →
     2886  exec_step ge s1 = Value … 〈tr,s2〉 →
     2887  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
     2888#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
     2889inversion Hsim_state
     2890[ 1: (* regular state *)
     2891  #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_
     2892  lapply (sim_related_globals ge ge' e m Hrelated) *
     2893  #Hexpr_related #Hlvalue_related
     2894  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
     2895  cases s in Hu_fresh Heq_env;
    8562896  (* Perform the intros for the statements*)
    857   [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
     2897  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
    8582898  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
    8592899  | 14: #lab | 15: #cost #body ]
    860   #Hus_fresh
     2900  #Hu_fresh #Heq_env
    8612901  [ 1: (* Skip *)
    8622902    whd in match (sw_rem ??);
    8632903    inversion Hsim_cont normalize nodelta
    8642904    [ 1: #Hk #Hk' #_ #Hexec_step
    865          @(eventually_base … (Returnstate Vundef Kstop (free_list m (blocks_of_env e))))
    866          [ 1: whd in match (exec_step ??); >fn_return_simplify ]
     2905         @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify
    8672906         cases (fn_return f) in Hexec_step;
    8682907         [ 1,10: | 2,11: #sz #sg | 3,12: #fsz | 4,13: #rg #ptr_ty | 5,14: #rg #array_ty #array_sz | 6,15: #domain #codomain
    8692908         | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
    8702909         normalize nodelta
    871          [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) // %3 destruct //
     2910         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H)
     2911                %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try //
     2912                normalize in Heq_env; destruct (Heq_env)
     2913                %3 //
     2914(*                cut (blocks_of_env e = blocks_of_env e')
     2915                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
     2916                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
     2917                #Heq >Heq %3 // *)
    8722918         | *: #H destruct (H) ]
    873     | 2: #s0 #k0 #k0' #us0 #Hus0_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
     2919    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
    8742920         whd in match (ret ??) in Heq; destruct (Heq)
    8752921         @(eventually_now ????) whd in match (exec_step ??);
    876          %{(State (\fst  (function_switch_removal f uf)) (sw_rem s0 us0) k0' e m)} @conj try //
    877          %1{uf us0 uk} //
    878          >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); >Hk'
    879          whd in ⊢ (% → ?); * #_ //
    880     | 3: #e0 #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq
     2922         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
     2923         %1 try //   
     2924    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
    8812925         @(eventually_now ????) whd in match (exec_step ??);
    8822926         whd in match (ret ??) in Heq; destruct (Heq)
    883          %{(State (\fst  (function_switch_removal f uf)) (Swhile e0 (sw_rem s0 us0)) k0' e m)} @conj try //
    884          >while_commute %1{uf us0 uk} //
    885          [ 1: @while_fresh_lift assumption
    886          | 2: >Hk' in Huk_fresh; whd in ⊢ (% → ?); * #_ // ]
    887     | 4: #eO #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq
     2927         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
     2928         >while_commute %1 try //
     2929    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
    8882930         @(eventually_now ????) whd in match (exec_step ??);
    889  
    890          
    891          
    892          [ 1: @uk
    893          | 2: >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); * * // ]
    894                  
    895          whd
    896          normalize
    897          
    898          cut (Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0))
    899          [ 1: whd in match (sw_rem (Swhile ??) ?);
    900               whd in match (switch_removal ??);
    901          whd in match (exec_step ??);
    902 
    903 (* foireux pour le (Expr (Econst_int sz n) ?) *)
    904 lemma convert :
    905 ∀uv.
    906   ∀sz,n,sl.
    907     seq_of_labeled_statements (select_switch sz n sl)
    908     ~~~u
    909     let 〈exit_label, uv1〉            ≝ fresh ? uv in   
    910     let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list sl ? uv1 [ ] in   
    911     Ssequence (pi1 … (produce_cond2 (Expr (Econst_int sz n)) sl defcase exit_label)) (Slabel exit_label Sskip)
    912    
    913 
    914 lemma convert :
    915 ∀f,cond,ls,k,ge,e,m.
    916   ∀t.
    917     ∀sz,n. exec_step ge (State f (Sswitch cond ls) k e m) = Value ??? 〈t,State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m〉 →
    918     ∀uf,us.
    919      fresh_for_function f uf →
    920      fresh_for_statement (Sswitch cond ls) us →   
    921     ∃s',k'.
    922      (exec_plus ge
    923         E0 (State (\fst (function_switch_removal f uf)) (sw_rem (Sswitch cond ls) us) k' e m)
    924         t s')
    925      ∧ switch_cont_sim k k'
    926      ∧ switch_state_sim
    927         (State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m)
    928         s'.
    929 #f #cond #ls #k #ge #e #m #t #sz #n #Hexec #uf #us #Huf #Hus
    930 whd in match (sw_rem ??);
    931 whd in match (switch_removal ??);
    932 check eq_ind
    933 
    934 
    935 
    936 whd in Hexec:(??%?); cases (exec_expr ge e m cond) in Hexec;
    937 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) ]
    938 * #cond_val #cond_trace
    939 whd in match (bindIO ??????);
    940 cases cond_val
    941 [ 1: | 2: #sz' #n' | 3: #fl | 4: #rg | 5: #ptr ]
    942 [ 1,3,4,5: #Habsurd normalize in Habsurd; destruct (Habsurd) ]
    943 normalize nodelta #Heq whd in match (ret ??) in Heq;
    944 
    945 
    946    
    947    
    948       ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    949       match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
    950                     | _ ⇒ Wrong ??? (msg TypeMismatch) ]   
    951 
    952 theorem step_with_labels : ∀ge,ge'.
    953   related_globals ? label_fundef ge ge' →
    954   state_with_labels s1 s1' →
    955   exec_expr ge en m e = OK ? 〈Vint sz v, tr〉 →
    956   (seq_of_labeled_statement (select_switch sz n sl) ~ simplify_switch
    957   (exec_step ge st (Sswitch e ls)
     2931         lapply (Hexpr_related e0)
     2932         cases (exec_expr ge e m e0) in Heq;
     2933         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
     2934         | 1: * #b #tr whd in match (m_bind ?????); #Heq
     2935              *
     2936              [ 2: * #error #Habsurd destruct (Habsurd)
     2937              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
     2938                   whd in match (bindIO ??????);
     2939                   cases (exec_bool_of_val b (typeof e0)) in Heq;
     2940                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     2941                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
     2942                        whd in match (bindIO ??????);
     2943                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
     2944                             @conj // >dowhile_commute %1 try //
     2945                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
     2946                             @conj // %1{us} try //
     2947                             @(fresh_for_Sskip … Hus_fresh)
     2948                        ] ] ] ]
     2949    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
     2950         @(eventually_now ????) whd in match (exec_step ??);
     2951         whd in match (ret ??) in Heq; destruct
     2952         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
     2953         @conj try // %1{u} try //
     2954    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
     2955         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
     2956         destruct (Heq)
     2957         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
     2958         @conj try // %1
     2959         [ 2: @swc_for3 //
     2960         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
     2961    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
     2962         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
     2963         destruct (Heq)
     2964         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
     2965         @conj try // <(for_commute ??? u uA) try // %1
     2966         [ 2: assumption
     2967         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
     2968    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
     2969         #Heq @(eventually_now ????) whd in match (exec_step ??);
     2970         destruct (Heq)
     2971         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
     2972         %1{u} //
     2973    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
     2974         @(eventually_now ????) whd in match (exec_step ??);
     2975         >fn_return_simplify cases (fn_return f) in Heq;
     2976         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
     2977         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
     2978         normalize nodelta
     2979         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
     2980              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
     2981              @conj try // %3 destruct //
     2982         | *: #H destruct (H) ]     
     2983     ]
     2984  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
     2985       whd in match (exec_step ??);
     2986       cases lhs in Hu_fresh Heq; #lhs #lhs_type
     2987       cases (Hlvalue_related lhs lhs_type)
     2988       whd in match (exec_lvalue ge e m (Expr ??));
     2989       whd in match (exec_lvalue ge' e m (Expr ??));
     2990       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
     2991       cases (exec_lvalue' ge e m lhs lhs_type)
     2992       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
     2993       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
     2994            whd in match (m_bind ?????);
     2995            cases (Hexpr_related rhs)
     2996            [ 2: * #error #Hfail >Hfail #_
     2997                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     2998            | 1: cases (exec_expr ge e m rhs)
     2999                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
     3000                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
     3001                      whd in match (bindIO ??????) in ⊢ (% → % → %);
     3002                      cases (opt_to_io io_out io_in ???)
     3003                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
     3004                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     3005                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
     3006                           %{(State (function_switch_removal f) Sskip k' e mem)}
     3007                           whd in match (bindIO ??????); @conj //
     3008                           %1{u} try // @(fresh_for_Sskip … Hfresh)
     3009       ] ] ] ]
     3010   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
     3011        whd in match (exec_step ??);
     3012        cases (Hexpr_related func) in Heq;
     3013        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     3014        | 1: cases (exec_expr ge e m func)
     3015             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     3016             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
     3017                  whd in match (m_bind ?????); normalize nodelta
     3018                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
     3019                  #Hexprlist_sim cases (Hexprlist_sim args)
     3020                  [ 2: * #error #Hfail >Hfail
     3021                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     3022                  | 1: cases (exec_exprlist ge e m args)
     3023                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     3024                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
     3025                            whd in match (bindIO ??????) in ⊢ (% → %);
     3026                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
     3027                            cases (find_funct clight_fundef ge fval)
     3028                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
     3029                                 whd in match (bindIO ??????) in ⊢ (% → %);
     3030                                 >fundef_type_simplify
     3031                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
     3032                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3033                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
     3034                                      cases retv normalize nodelta
     3035                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
     3036                                           %{(Callstate (fundef_switch_removal clfd) values
     3037                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
     3038                                           @conj try // %2 try // @swc_call //
     3039                                      | 2: * #retval_ed #retval_type
     3040                                           whd in match (exec_lvalue ge ???);
     3041                                           whd in match (exec_lvalue ge' ???);                                     
     3042                                           elim (Hlvalue_related retval_ed retval_type)
     3043                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     3044                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
     3045                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
     3046                                                     destruct (Habsurd)
     3047                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
     3048                                                     whd in match (m_bind ?????) in ⊢ (% → %);
     3049                                                     #Heq destruct (Heq)
     3050                                                     %{(Callstate (fundef_switch_removal clfd) values
     3051                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
     3052                                                               (function_switch_removal f) e k') m)}
     3053                                                     @conj try //
     3054                                                     %2 @swc_call //
     3055                                ] ] ] ]
     3056                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
     3057                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     3058       ] ] ] ] ]
     3059   | 4: (* Ssequence *) normalize nodelta
     3060        whd in match (ret ??) in ⊢ (% → ?); #Heq
     3061        @(eventually_now ????)
     3062        %{(State (function_switch_removal f)
     3063                 (\fst (\fst (switch_removal stm1 u)))
     3064                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
     3065        @conj
     3066        [ 2: destruct (Heq) %1
     3067             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
     3068             | 2: @swc_seq try // @switch_removal_fresh
     3069                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
     3070        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
     3071             cases (switch_removal stm1 u)
     3072             * #stm1' #fresh_vars #u' normalize nodelta
     3073             cases (switch_removal stm2 u')
     3074             * #stm2' #fresh_vars2 #u'' normalize nodelta
     3075             whd in match (exec_step ??);
     3076             destruct (Heq) @refl
     3077        ]
     3078   | 5: (* If-then-else *) normalize nodelta
     3079        whd in match (ret ??) in ⊢ (% → ?); #Heq
     3080        @(eventually_now ????) whd in match (sw_rem ??);
     3081        whd in match (switch_removal ??);
     3082        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
     3083        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
     3084        whd in match (exec_step ??);
     3085        cases (Hexpr_related cond) in Heq;
     3086        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     3087        | 1: cases (exec_expr ge e m cond)
     3088             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     3089             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
     3090                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
     3091                  cases (exec_bool_of_val condval (typeof cond))
     3092                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3093                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
     3094                       destruct (Heq_condval) whd in match (bindIO ??????);
     3095                       normalize nodelta
     3096                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
     3097                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
     3098                           [ 1: >Hiftrue_eq normalize // ]
     3099                           #Hrewrite >Hrewrite %1
     3100                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
     3101                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
     3102                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
     3103                           [ 1: >Hiffalse_eq // ]
     3104                           #Hrewrite >Hrewrite %1 try //
     3105                           cut (uA = (\snd (switch_removal iftrue u)))
     3106                           [ 1: >Hiftrue_eq //
     3107                           | 2: #Heq_uA >Heq_uA
     3108                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
     3109                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
     3110       ] ] ] ] ]
     3111   | 6: (* While loop *) normalize nodelta
     3112        whd in match (ret ??) in ⊢ (% → ?); #Heq
     3113        @(eventually_now ????) whd in match (sw_rem ??);
     3114        whd in match (switch_removal ??);
     3115        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
     3116        whd in match (exec_step ??);
     3117        cases (Hexpr_related cond) in Heq;
     3118        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     3119        | 1: cases (exec_expr ge e m cond)
     3120             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     3121             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
     3122                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
     3123                  cases (exec_bool_of_val condval (typeof cond))
     3124                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3125                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
     3126                       destruct (Heq_condval) whd in match (bindIO ??????);
     3127                       normalize nodelta
     3128                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
     3129                            cut (body' = (\fst (\fst (switch_removal body u))))
     3130                            [ 1: >Hbody_eq // ]
     3131                            #Hrewrite >Hrewrite %1
     3132                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
     3133                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
     3134                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
     3135                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
     3136        ] ] ] ]
     3137   | 7: (* Dowhile loop *) normalize nodelta
     3138        whd in match (ret ??) in ⊢ (% → ?); #Heq
     3139        @(eventually_now ????) whd in match (sw_rem ??);
     3140        whd in match (switch_removal ??);
     3141        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
     3142        whd in match (exec_step ??);
     3143        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
     3144        try //
     3145        cut (body' = (\fst (\fst (switch_removal body u))))
     3146        [ 1: >Hbody_eq // ]
     3147        #Hrewrite >Hrewrite %1
     3148        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
     3149        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
     3150   | 8: (* For loop *) normalize nodelta
     3151        whd in match (ret ??) in ⊢ (% → ?); #Heq
     3152        @(eventually_now ????) whd in match (sw_rem ??);
     3153        whd in match (switch_removal ??);
     3154        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
     3155        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
     3156              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
     3157              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
     3158              whd in match (exec_step ??);
     3159              cases (Hexpr_related cond)
     3160              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     3161              | 1: cases (exec_expr ge e m cond)
     3162                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     3163                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
     3164                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
     3165                        cases (exec_bool_of_val condval (typeof cond))
     3166                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3167                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
     3168                             destruct (Heq_condval)
     3169                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
     3170                                  try //
     3171                                  cut (body' = (\fst (\fst (switch_removal body uA))))
     3172                                  [ 1: >Hbody_eq // ]
     3173                                  #Hrewrite >Hrewrite
     3174                                  cut (uA = (\snd (switch_removal step u)))
     3175                                  [ 1: >Hstep_eq // ] #HuA
     3176                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
     3177                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
     3178                                  [ 1: >HuA @switch_removal_fresh assumption
     3179                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
     3180                                       [ >Hstep_eq // ]
     3181                                       #Hstep >Hstep @swc_for2 try assumption
     3182                                       @for_fresh_lift try assumption ]
     3183                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
     3184                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
     3185               ] ] ] ]
     3186        | 2: #Heq
     3187             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
     3188             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
     3189             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
     3190             whd in match (exec_step ??);
     3191             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
     3192             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
     3193             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
     3194             whd in match (ret ??); destruct (Heq)
     3195             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
     3196             @conj try //
     3197             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
     3198             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
     3199             <for_commute [ 2: >Hstep_eq // ]
     3200             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
     3201             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
     3202             @swc_seq try // @for_fresh_lift
     3203             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
     3204             >HuA_eq @switch_removal_fresh assumption       
     3205       ]
     3206   | 9: (* break *) normalize nodelta
     3207        inversion Hsim_cont
     3208        [ 1: #Hk #Hk' #_       
     3209        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
     3210        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
     3211        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
     3212        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
     3213        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
     3214        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
     3215        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
     3216        normalize nodelta #H try (destruct (H))
     3217        whd in match (ret ??) in H; destruct (H)
     3218        @(eventually_now ????)
     3219        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
     3220        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
     3221    | 10: (* Continue *) normalize nodelta
     3222        inversion Hsim_cont
     3223        [ 1: #Hk #Hk' #_       
     3224        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
     3225        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
     3226        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
     3227        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
     3228        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
     3229        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
     3230        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
     3231        normalize nodelta #H try (destruct (H))
     3232        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
     3233        destruct (H)
     3234        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
     3235        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
     3236             >while_commute %1{u0} try assumption
     3237        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
     3238             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3239             | 1: * #condval #trace whd in match (m_bind ?????);
     3240                  #Heq *
     3241                  [ 2: * #error #Habsurd destruct (Habsurd)
     3242                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
     3243                       whd in match (bindIO ??????);
     3244                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
     3245                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3246                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
     3247                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)}
     3248                                 @conj try // >dowhile_commute %1{u0} assumption
     3249                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
     3250                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
     3251             ] ] ]
     3252        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
     3253             try // @(fresh_for_Scontinue … Hfor_fresh)
     3254        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
     3255             @conj try // %1{u0}
     3256             elim (substatement_fresh … Hfor_fresh) * * try //
     3257             #HSskip #Hcond #Hstep #Hbody
     3258             @swc_for3 assumption
     3259        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
     3260             %1{u} try //
     3261        ]
     3262    | 11: (* Sreturn *) normalize nodelta #Heq
     3263          @(eventually_now ????)
     3264          whd in match (exec_step ??) in Heq ⊢ %;
     3265          cases retval in Heq; normalize nodelta
     3266          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
     3267               whd in match (ret ??) in ⊢ (% → %);
     3268               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
     3269               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     3270               #H destruct (H)
     3271               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
     3272               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
     3273          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
     3274               [ 1: #_ #Habsurd destruct (Habsurd)
     3275               | 2: #_ elim (Hexpr_related expr)
     3276                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     3277                    | 1: cases (exec_expr ??? expr)
     3278                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     3279                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
     3280                              #Hrewrite >Hrewrite
     3281                              whd in match (m_bind ?????); whd in match (m_bind ?????);
     3282                              #Heq destruct (Heq)
     3283                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
     3284                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
     3285         ] ] ] ]
     3286    | 12: (* Sswitch. Main proof case. *) normalize nodelta
     3287          (* Case analysis on the outcome of the tested expression *)
     3288          cases (exec_expr_int ge e m cond)
     3289          [ 2: cases (exec_expr ge e m cond)
     3290               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
     3291               | 1: * #val #trace cases val
     3292                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
     3293                    whd in match (m_bind ?????);
     3294                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
     3295                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
     3296          ]
     3297          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
     3298          whd in match (m_bind ?????); #Heq
     3299          destruct (Heq)
     3300          @eventually_later
     3301          whd in match (sw_rem (Sswitch cond switchcases) u);
     3302          whd in match (switch_removal (Sswitch cond switchcases) u);
     3303          elim (switch_removal_branches_eq switchcases u)
     3304          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
     3305          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
     3306          [ 1: >Hsrb_eq // ] #Huv1_eq
     3307          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
     3308          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
     3309          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
     3310          whd in match (simplify_switch ???);
     3311          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
     3312          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
     3313          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)         
     3314          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
     3315          #Huv4_eq
     3316          whd in match (exec_step ??);
     3317          %{(State (function_switch_removal f)
     3318                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
     3319                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
     3320          %{E0} @conj try @refl
     3321          %{tr} normalize in match (eq ???); @conj try //
     3322          (* execute the conditional *)
     3323          @eventually_later
     3324          (* lift the result of the previous case analysis from [ge] to [ge'] *)
     3325          whd in match (exec_step ??);
     3326          whd in match (exec_lvalue ????);
     3327         
     3328          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
     3329         
     3330  *)
    9583331 
    959  
    960    ∃tr',s2'. plus ge' s1' tr' s2' ∧
    961              trace_with_extra_labels tr tr' ∧
    962              state_with_labels s2 s2').
    963 
    964 
    965 *)
    966 
Note: See TracChangeset for help on using the changeset viewer.