source: src/Clight/switchRemoval.ma @ 2234

Last change on this file since 2234 was 2234, checked in by garnier, 8 years ago

Progress on proving semantics preservation under memory injections.

  • Property svn:executable set to *
File size: 169.0 KB
Line 
1include "Clight/Csyntax.ma".
2include "Clight/fresh.ma".
3include "basics/lists/list.ma".
4include "common/Identifiers.ma".
5include "Clight/Cexec.ma".
6include "Clight/CexecInd.ma".
7include "Clight/frontend_misc.ma".
8(*
9include "Clight/maps_obsequiv.ma".
10*)
11
12
13(* -----------------------------------------------------------------------------
14   ----------------------------------------------------------------------------*)
15
16(* -----------------------------------------------------------------------------
17   Documentation
18   ----------------------------------------------------------------------------*)
19
20(* This file implements transformation of switches to linear sequences of
21 * if/then/else. The implementation roughly follows the lines of the prototype.
22 * /!\ We assume that the program is well-typed (the type of the evaluated
23 * expression must match the constants on each branch of the switch). /!\ *)
24
25(* Documentation. Let the follwing be our input switch construct:
26   // --------------------------------- 
27   switch(e) {
28   case v1:
29     stmt1
30   case v2:
31     stmt2
32   .
33   .
34   .
35   default:
36     stmt_default
37   }
38   // --------------------------------- 
39 
40   Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting
41   the switch statement. In the absence of break, the execution falls through each case sequentially.
42 
43   Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos:
44
45   // --------------------------------- 
46   fresh = e;
47   if(fresh == v1) {
48     stmt1';
49     goto lbl_case2;
50   }
51   if(fresh == v2) {
52     lbl_case2:
53     stmt2';
54     goto lbl_case2;
55   }   
56   ...
57   stmt_default';
58   exit_label:
59   // ---------------------------------   
60
61   where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements
62   were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels.
63*)
64
65
66(* -----------------------------------------------------------------------------
67   Definitions allowing to state that the program resulting of the transformation
68   is switch-free.
69   ---------------------------------------------------------------------------- *)
70
71(* Property of a Clight statement of containing no switch. Could be generalized into a kind of
72 * statement_P, if useful elsewhere. *)
73let rec switch_free (st : statement) : Prop ≝
74match st with
75[ Sskip ⇒ True
76| Sassign _ _ ⇒ True
77| Scall _ _ _ ⇒ True
78| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
79| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
80| Swhile e body ⇒ switch_free body
81| Sdowhile e body ⇒ switch_free body
82| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
83| Sbreak ⇒ True
84| Scontinue ⇒ True
85| Sreturn _ ⇒ True
86| Sswitch _ _ ⇒ False
87| Slabel _ body ⇒ switch_free body
88| Sgoto _ ⇒ True
89| Scost _ body ⇒ switch_free body
90].
91
92(* Property of a list of labeled statements of being switch-free *)
93let rec branches_switch_free (sts : labeled_statements) : Prop ≝
94match sts with
95[ LSdefault st =>
96  switch_free st
97| LScase _ _ st tl =>
98  switch_free st ∧ branches_switch_free tl
99].
100
101let rec branches_ind
102  (sts : labeled_statements)
103  (H   : labeled_statements → Prop) 
104  (defcase : ∀st. H (LSdefault st))
105  (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝
106match sts with
107[ LSdefault st ⇒
108  defcase st
109| LScase sz int st tl ⇒
110  indcase sz int st tl (branches_ind tl H defcase indcase)
111].
112
113(* -----------------------------------------------------------------------------
114   Switch-removal code for statements, functions and fundefs.
115   ----------------------------------------------------------------------------*)
116
117(* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
118let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
119match st with
120[ Sbreak ⇒
121  Sgoto lab
122| Ssequence s1 s2 ⇒
123  Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab)
124| Sifthenelse e iftrue iffalse ⇒
125  Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab)
126| Sfor init e update body ⇒
127  Sfor (convert_break_to_goto init lab) e update body
128| Slabel l body ⇒
129  Slabel l (convert_break_to_goto body lab)
130| Scost cost body ⇒
131  Scost cost (convert_break_to_goto body lab)
132| _ ⇒ st
133].
134
135(* Converting breaks preserves switch-freeness. *)
136lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label).
137#s elim s //
138[ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
139| 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
140| 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
141     try @conj try @conj /3/
142| 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/
143| 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/
144] qed.
145
146(* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)
147(*
148let rec produce_cond
149  (e : expr)
150  (switch_cases : stlist)
151  (def_case : ident × sf_statement)
152  (exit : label) on switch_cases : sf_statement × label ≝
153match switch_cases with
154[ nil ⇒
155  match def_case with
156  [ mk_Prod default_label default_statement ⇒
157    〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
158  ]
159| cons switch_case tail ⇒
160  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
161    match case_value with
162    [ mk_DPair sz val ⇒
163       let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
164       (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *)
165       (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed)  in *)
166       let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in
167       let result ≝
168         Sifthenelse test
169          (Slabel case_label
170            (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
171                       (Sgoto sub_label)))
172          (pi1 … sub_statement)
173      in
174      〈«result, ?», case_label〉
175    ]
176].
177[ 1: normalize @convert_break_lift elim default_statement //
178| 2: whd @conj normalize try @conj try //
179  [ 1: @convert_break_lift elim case_statement //
180  | 2: elim sub_statement // ]
181] qed. *)
182
183(* We assume that the expression e is consistely typed w.r.t. the switch branches *)
184(*
185let rec produce_cond2
186  (e : expr)
187  (switch_cases : stlist)
188  (def_case : ident × sf_statement)
189  (exit : label) on switch_cases : sf_statement × label ≝
190match switch_cases with
191[ nil ⇒
192  let 〈default_label, default_statement〉 ≝ def_case in
193  〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
194| cons switch_case tail ⇒
195  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
196  match case_value with
197  [ mk_DPair sz val ⇒
198    let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
199    let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in
200    let case_statement_res ≝
201       Sifthenelse test
202        (Slabel case_label
203          (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
204                     (Sgoto sub_label)))
205        Sskip
206    in
207    〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉
208  ]
209].
210[ 1: normalize @convert_break_lift elim default_statement //
211| 2: whd @conj
212     [ 1: whd @conj try // whd in match (switch_free ?); @conj
213          [ 1: @convert_break_lift elim case_statement //
214          | 2: // ]
215     | 2: elim sub_statement // ]
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).
247 let 〈exit_label, uv1〉            ≝ fresh ? uv in
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'〉
350   ]
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]
360
361and switch_removal_branches
362  (l : labeled_statements)
363  (fvs : list ident)
364  (u : universe SymbolTag)
365(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
366match l with
367[ LSdefault st ⇒
368  do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
369  ret 〈LSdefault st', acc1, fvs', u'〉
370| LScase sz int st tl =>
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''〉
374].
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'))} % //
615] qed.
616
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.
640
641(* -----------------------------------------------------------------------------
642   Switch-removal code for programs.
643   ----------------------------------------------------------------------------*) 
644
645(* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to
646 * name clashes for labels. We have no choice but to actually run through the function and to
647 * compute the maximum of labels+identifiers. This way we can generate both fresh variables and
648 * fresh labels using the same univ. While we're at it we also consider record fields.
649 * Cost labels are not considered, though. They already live in a separate universe.
650 *
651 * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes,
652 * but in the end it might be good to move the following functions into fresh.ma.
653 *)
654
655(* Least element in the total order of identifiers. *)
656definition least_identifier ≝ an_identifier SymbolTag one.
657
658(* This is certainly overkill: variables adressed in an expression should be declared in the
659 * enclosing function's prototype. *)
660let rec max_of_expr (e : expr) : ident ≝
661match e with
662[ Expr ed _ ⇒
663  match ed with
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))
674  | Eandbool e1 e2 ⇒
675    max_id (max_of_expr e1) (max_of_expr e2)
676  | Eorbool e1 e2 ⇒
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
681  ]
682].
683
684(* Reasoning about this promises to be a serious pain. Especially the Scall case. *)
685let rec max_of_statement (s : statement) : ident ≝
686match s with
687[ Sskip ⇒ least_identifier
688| Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
689| Scall r f args ⇒
690  let retmax ≝
691    match r with
692    [ None ⇒ least_identifier
693    | Some e ⇒ max_of_expr e ]
694  in
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)
700| Sifthenelse e s1 s2 ⇒
701  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
702| Swhile e body ⇒
703  max_id (max_of_expr e) (max_of_statement body)
704| Sdowhile e body ⇒
705  max_id (max_of_expr e) (max_of_statement body)
706| Sfor init test incr body ⇒
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
710| Sreturn opt ⇒
711  match opt with
712  [ None ⇒ least_identifier
713  | Some e ⇒ max_of_expr e
714  ]
715| Sswitch e ls ⇒
716  max_id (max_of_expr e) (max_of_ls ls)
717| Slabel lab body ⇒
718  max_id lab (max_of_statement body)
719| Sgoto lab ⇒
720  lab
721| Scost _ body ⇒
722  max_of_statement body
723]
724and max_of_ls (ls : labeled_statements) : ident ≝
725match ls with
726[ LSdefault s ⇒ max_of_statement s
727| LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s)
728].
729
730definition max_id_of_function : function → ident ≝
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].
758
759let rec program_switch_removal (p : clight_program) : clight_program ≝
760 let prog_funcs ≝ prog_funct ?? p 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
765 mk_program ??
766  (prog_vars … p)
767  sf_funcs
768  (prog_main … p).
769
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*)
918(* -----------------------------------------------------------------------------
919   Simulation proof and related voodoo.
920   ----------------------------------------------------------------------------*)
921
922definition expr_lvalue_ind_combined ≝
923λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
924conj ??
925 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
926 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
927 
928let rec expr_ind2
929    (P : expr → Prop) (Q : expr_descr → type → Prop)
930    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
931    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
932    (Iconst_float : ∀f, t. Q (Econst_float f) t)
933    (Ivar : ∀id, t. Q (Evar id) t)
934    (Ideref : ∀e, t. P e → Q (Ederef e) t)
935    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
936    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
937    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
938    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t) 
939    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
940    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
941    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
942    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
943    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
944    (Icost : ∀c,e,t. P e → Q (Ecost c e) t)
945    (e : expr) on e : P e ≝
946match e with
947[ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ]
948
949and expr_desc_ind2
950    (P : expr → Prop) (Q : expr_descr → type → Prop)
951    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
952    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
953    (Iconst_float : ∀f, t. Q (Econst_float f) t)
954    (Ivar : ∀id, t. Q (Evar id) t)
955    (Ideref : ∀e, t. P e → Q (Ederef e) t)
956    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
957    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
958    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
959    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t) 
960    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
961    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
962    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
963    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
964    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
965    (Icost : ∀c,e,t. P e → Q (Ecost c e) t)
966    (ed : expr_descr) (t : type) on ed : Q ed t ≝
967match ed with
968[ Econst_int sz i ⇒ Iconst_int sz i t
969| Econst_float f ⇒ Iconst_float f t
970| Evar id ⇒ Ivar id t
971| Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
972| Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
973| Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
974| Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
975| Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
976| Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
977| Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
978| Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
979| Esizeof sizeoft ⇒ Isizeof sizeoft t
980| Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
981| Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e)
982].
983
984
985(* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched
986   by a non-constant number of evaluations in the converted program. More precisely,
987   [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps
988   necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *)
989   
990(* A version of simplify_switch hiding the ugly projs *)
991definition fresh_for_expression ≝
992λe,u. fresh_for_univ SymbolTag (max_of_expr e) u.
993
994definition fresh_for_statement ≝
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   
1001definition fresh_for_function ≝
1002λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.
1003
1004(* misc properties of the max function on positives. *)
1005
1006lemma max_one_neutral : ∀v. max v one = v.
1007* // qed.
1008
1009lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v.
1010* #p whd in ⊢ (??%?); >max_one_neutral // qed.
1011
1012lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1.
1013* #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%);
1014>commutative_max // qed.
1015
1016lemma transitive_le : transitive ? le. // qed.
1017
1018lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
1019#a #b /2/ qed.
1020
1021(* cycle of length 1 *)
1022lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
1023* /2 by absurd/ qed.
1024
1025(* cycle of length 2 *)
1026lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False.
1027#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2))
1028#Heq @(le_S_contradiction_1 a) destruct // qed.
1029
1030(* cycle of length 3 *)
1031lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False.
1032#a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4
1033@(le_S_contradiction_2 … H3 H4)
1034qed.
1035
1036lemma reflexive_leb : ∀a. leb a a = true.
1037#a @(le_to_leb_true a a) // qed.
1038
1039(* This should be somewhere else. *)
1040lemma associative_max : associative ? max.
1041#a #b #c
1042whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
1043lapply (pos_compare_to_Prop a b)
1044cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
1045[ 1: >(le_to_leb_true a b) normalize nodelta /2/
1046     lapply (pos_compare_to_Prop b c)
1047     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1048     [ 1: >(le_to_leb_true b c) normalize nodelta
1049          lapply (pos_compare_to_Prop a c)
1050          cases (pos_compare a c) whd in ⊢ (% → ?); #Hac
1051          [ 1: >(le_to_leb_true a c) /2/
1052          | 2: destruct cases (leb c c) //
1053          | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *)
1054               @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac))           
1055          ]
1056          @le_S_weaken //
1057     | 2: destruct
1058          cases (leb c c) normalize nodelta
1059          >(le_to_leb_true a c) /2/
1060     | 3: >(not_le_to_leb_false b c) normalize nodelta /2/
1061          >(le_to_leb_true a b) /2/
1062     ]
1063| 2: destruct (Hab) >reflexive_leb normalize nodelta
1064     lapply (pos_compare_to_Prop b c)
1065     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1066     [ 1: >(le_to_leb_true b c) normalize nodelta
1067          >(le_to_leb_true b c) normalize nodelta
1068          /2/
1069     | 2: destruct >reflexive_leb normalize nodelta
1070          >reflexive_leb //
1071     | 3: >(not_le_to_leb_false b c) normalize nodelta
1072          >reflexive_leb /2/ ]
1073| 3: >(not_le_to_leb_false a b) normalize nodelta /2/
1074     lapply (pos_compare_to_Prop b c)
1075     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1076     [ 1: >(le_to_leb_true b c) normalize nodelta /2/
1077     | 2: destruct >reflexive_leb normalize nodelta @refl
1078     | 3: >(not_le_to_leb_false b c) normalize nodelta
1079          >(not_le_to_leb_false a b) normalize nodelta
1080          >(not_le_to_leb_false a c) normalize nodelta
1081          lapply (transitive_le … Hbc (le_S_weaken … Hab))
1082          #Hca /2/
1083     ]
1084] qed.   
1085
1086lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3).
1087* #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max //
1088qed.
1089(*
1090lemma max_of_expr_rewrite :
1091  ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id.
1092@(expr_ind2 … (λed,t. ∀id. max_of_expr (Expr ed t) id=max_id (max_of_expr (Expr ed t) (an_identifier SymbolTag one)) id))
1093[ 1: #ed #t // ]
1094[ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
1095| 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
1096#ty
1097[ 3: * #id_p whd in match (max_of_expr ??); cases var_id #var_p normalize nodelta
1098     whd in match (max_id ??) in ⊢ (???%);
1099     >max_one_neutral // ]
1100[ 1,2,11: * * //
1101| 3,4,5,7,13: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); @Hind
1102| 6,9,10: #Hind1 #Hind2 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
1103     >(Hind1 (max_of_expr e2 (an_identifier SymbolTag one)))
1104     >max_id_associative
1105     >Hind1
1106     cases (max_of_expr e1 ?)
1107     #v1 <Hind2 @refl
1108| 8: #Hind1 #Hind2 #Hind3 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
1109     >Hind1 in ⊢ (??%?); >Hind2 in ⊢ (??%?); >Hind3 in ⊢ (??%?);
1110     >Hind1 in ⊢ (???%); >Hind2 in ⊢ (???%);
1111     >max_id_associative >max_id_associative @refl
1112| 12: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
1113      cases field #p normalize nodelta
1114      >Hind cases (max_of_expr e1 ?) #e'
1115      cases id #id'
1116      whd in match (max_id ??); normalize nodelta
1117      whd in match (max_id ??); >associative_max @refl
1118] qed.
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(* A cleaner version of inversion for [value_eq] *)
1315lemma value_eq_inversion :
1316  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
1317  (∀v. P Vundef v) →
1318  (∀sz,i. P (Vint sz i) (Vint sz i)) →
1319  (∀f. P (Vfloat f) (Vfloat f)) →
1320  (P Vnull Vnull) →
1321  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
1322  P v1 v2.
1323#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
1324inversion Heq
1325[ 1: #v #Hv1 #Hv2 #_ destruct @H1
1326| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
1327| 3: #f #Hv1 #Hv2 #_ destruct @H3
1328| 4: #Hv1 #Hv2 #_ destruct @H4
1329| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
1330 
1331(* If we succeed to load something by value from a 〈b,off〉 location,
1332   [b] is a valid block. *)
1333lemma load_by_value_success_valid_block_aux :
1334  ∀ty,m,b,off,v.
1335    access_mode ty = By_value (typ_of_type ty) →
1336    load_value_of_type ty m b off = Some ? v →
1337    Zltb (block_id b) (nextblock m) = true.
1338#ty #m * #brg #bid #off #v
1339cases ty
1340[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1341| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1342whd in match (load_value_of_type ????);
1343[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
1344#Hmode
1345[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
1346     normalize in match (typesize ?);
1347     whd in match (loadn ???);
1348     whd in match (beloadv ??);
1349     cases (Zltb bid (nextblock m)) normalize nodelta
1350     try // #Habsurd destruct (Habsurd)
1351| *: normalize in Hmode; destruct (Hmode)
1352] qed.
1353
1354(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
1355lemma load_by_value_success_valid_ptr_aux :
1356  ∀ty,m,b,off,v.
1357    access_mode ty = By_value (typ_of_type ty) →
1358    load_value_of_type ty m b off = Some ? v →
1359    Zltb (block_id b) (nextblock m) = true ∧
1360    Zleb (low_bound m b) (offv off) = true ∧
1361    Zltb (offv off) (high_bound m b) = true.
1362#ty #m * #brg #bid #off #v
1363cases ty
1364[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1365| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1366whd in match (load_value_of_type ????);
1367[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
1368#Hmode
1369[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
1370     normalize in match (typesize ?);
1371     whd in match (loadn ???);
1372     whd in match (beloadv ??);
1373     cases (Zltb bid (nextblock m)) normalize nodelta
1374     cases (Zleb (low (blocks m (mk_block brg bid))) (offv off))
1375     cases (Zleb (low (blocks m (mk_block brg bid))) (offv off))
1376     cases (Zltb (offv off) (high (blocks m (mk_block brg bid)))) normalize nodelta
1377     #Heq destruct (Heq)
1378     try /3 by conj, refl/
1379| *: normalize in Hmode; destruct (Hmode)
1380] qed.
1381
1382
1383lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
1384* #rg #id #m normalize
1385elim id /2/ qed.
1386
1387lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
1388* #rg #id #m normalize
1389elim id /2/ qed.
1390
1391lemma load_by_value_success_valid_block :
1392  ∀ty,m,b,off,v.
1393    access_mode ty = By_value (typ_of_type ty) →
1394    load_value_of_type ty m b off = Some ? v →
1395    valid_block m b.
1396#ty #m #b #off #v #Haccess_mode #Hload
1397@valid_block_from_bool
1398elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
1399qed.
1400
1401lemma load_by_value_success_valid_pointer :
1402  ∀ty,m,b,off,v.
1403    access_mode ty = By_value (typ_of_type ty) →
1404    load_value_of_type ty m b off = Some ? v →
1405    valid_pointer m (mk_pointer b off).
1406#ty #m #b #off #v #Haccess_mode #Hload normalize
1407elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
1408* #H1 #H2 #H3 >H1 >H2 normalize nodelta
1409>Zle_to_Zleb_true try //
1410lapply (Zlt_to_Zle … (Zltb_true_to_Zlt … H3)) /2/
1411qed.
1412
1413
1414(* Making explicit the contents of memory_inj for load_value_of_type *)
1415lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
1416    memory_inj E m1 m2 →
1417    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
1418    load_value_of_type ty m1 b1 off1 = Some ? v1 →
1419    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
1420#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
1421lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
1422     normalize in Hembed;
1423     lapply (mi_inj … Hinj b1 off1)
1424     cases (E b1) in Hembed;
1425     [ 1: normalize #Habsurd destruct (Habsurd)
1426     | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ]
1427     lapply (refl ? (access_mode ty))
1428     cases ty
1429     [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1430     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1431     normalize in ⊢ ((???%) → ?); #Hmode #Hyp
1432     [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd)
1433     | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ]
1434     #Hload_success
1435     lapply (load_by_value_success_valid_block … Hmode … Hload_success)
1436     #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success)
1437qed.
1438
1439
1440(* -------------------------------------- *)
1441(* Lemmas pertaining to memory allocation *)
1442
1443(* A valid block stays valid after an alloc. *)
1444lemma alloc_valid_block_conservation :
1445  ∀m,m',z1,z2,r,new_block.
1446  alloc m z1 z2 r = 〈m', new_block〉 →
1447  ∀b. valid_block m b → valid_block m' b.
1448#m #m' #z1 #z2 #r * #b' #Hregion_eq
1449elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
1450#Halloc destruct (Halloc)
1451#b whd in match (valid_block ??) in ⊢ (% → %); /2/
1452qed.
1453
1454(* Allocating a new zone produces a valid block. *)
1455lemma alloc_valid_new_block :
1456  ∀m,m',z1,z2,r,new_block.
1457  alloc m z1 z2 r = 〈m', new_block〉 →
1458  valid_block m' new_block.
1459* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
1460whd in match (alloc ????); whd in match (valid_block ??);
1461#Halloc destruct (Halloc) /2/
1462qed.
1463
1464(* All data in a valid block is unchanged after an alloc. *)
1465lemma alloc_beloadv_conservation :
1466  ∀m,m',block,offset,z1,z2,r,new_block.
1467    valid_block m block →
1468    alloc m z1 z2 r = 〈m', new_block〉 →
1469    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
1470* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
1471whd in Halloc:(??%?); destruct (Halloc)
1472whd in match (beloadv ??) in ⊢ (??%%);
1473lapply (valid_block_to_bool … Hvalid) #Hlt
1474>Hlt >(zlt_succ … Hlt)
1475normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
1476cut (eqZb (block_id block) next = false)
1477[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
1478>Hneq cases (eq_region ??) normalize nodelta  @refl
1479qed.
1480
1481(* Lift [alloc_beloadv_conservation] to loadn *)
1482lemma alloc_loadn_conservation :
1483  ∀m,m',z1,z2,r,new_block.
1484    alloc m z1 z2 r = 〈m', new_block〉 →
1485    ∀n. ∀block,offset.
1486    valid_block m block →
1487    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
1488#m #m' #z1 #z2 #r #new_block #Halloc #n
1489elim n try //
1490#n' #Hind #block #offset #Hvalid_block
1491whd in ⊢ (??%%);
1492>(alloc_beloadv_conservation … Hvalid_block Halloc)
1493cases (beloadv m' (mk_pointer block offset)) //
1494#bev normalize nodelta
1495whd in match (shift_pointer ???); >Hind try //
1496qed.
1497
1498(* Memory allocation preserves [memory_inj] *)
1499lemma alloc_memory_inj :
1500  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1501  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1502  memory_inj E m1 m2'.
1503#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
1504%
1505[ 1:
1506  whd
1507  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1508  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
1509  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
1510  lapply (refl ? (access_mode ty))
1511  cases ty in Hload_eq;
1512  [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1513  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1514  #Hload normalize in ⊢ ((???%) → ?); #Haccess
1515  [ 1,7,8: normalize in Hload; destruct (Hload)
1516  | 2,3,4,9: whd in match (load_value_of_type ????);
1517     whd in match (load_value_of_type ????);
1518     lapply (load_by_value_success_valid_block … Haccess Hload)
1519     #Hvalid_block
1520     whd in match (load_value_of_type ????) in Hload;
1521     <(alloc_loadn_conservation … Halloc … Hvalid_block)
1522     @Hload
1523  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
1524| 2: @(mi_freeblock … Hmemory_inj)
1525| 3: #b #b' #o' #HE
1526     lapply (mi_incl … Hmemory_inj … HE)
1527     elim m2 in Halloc; #contents #nextblock #Hnextblock
1528     whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1529     whd in match (valid_block ??) in ⊢ (% → %); /2/
1530| 4: @(mi_region … Hmemory_inj)
1531| 5: @(mi_disjoint … Hmemory_inj)
1532] qed.
1533
1534(* Memory allocation induces a memory extension. *)
1535lemma alloc_memory_ext :
1536  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1537  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1538  memory_ext E m1 m2'.
1539#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
1540lapply (alloc_memory_inj … Hmemory_inj Halloc)
1541#Hinj' %
1542[ 1: @Hinj'
1543| 2: @[new_block]
1544| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
1545      #Heq destruct (Heq) whd elim m2 in Halloc;
1546      #Hcontents #nextblock #Hnextblock
1547      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1548      /2/
1549| 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload %
1550     normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ]
1551     #Heq destruct (Heq)
1552     lapply (mi_incl … Hmemory_inj … Hload)
1553     whd in ⊢ (% → ?); #Habsurd
1554     (* contradiction car ¬ (valid_block m2 new_block)  *)
1555     elim m2 in Halloc Habsurd;
1556     #contents_m2 #nextblock_m2 #Hnextblock_m2
1557     whd in ⊢ ((??%?) → ?);
1558     #Heq_alloc destruct (Heq_alloc)
1559     lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd)
1560] qed.
1561
1562lemma bestorev_beloadv_conservation :
1563  ∀mA,mB,wb,wo,v.
1564    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1565    ∀rb,ro. eq_block wb rb = false →
1566    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
1567#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
1568whd in ⊢ (??%%);
1569elim mB in Hstore; #contentsB #nextblockB #HnextblockB
1570normalize in ⊢ (% → ?);
1571cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
1572[ 2: #Habsurd destruct (Habsurd) ]
1573cases (if Zleb (low (blocks mA wb)) (offv wo) 
1574       then Zltb (offv wo) (high (blocks mA wb)) 
1575       else false) normalize nodelta
1576[ 2: #Habsurd destruct (Habsurd) ]
1577#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
1578cases rr cases wr normalize try //
1579@(eqZb_elim … rid wid)
1580[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
1581try //
1582qed.
1583
1584(* lift [bestorev_beloadv_conservation to [loadn] *)
1585lemma bestorev_loadn_conservation :
1586  ∀mA,mB,n,wb,wo,v.
1587    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1588    ∀rb,ro. eq_block wb rb = false →
1589    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
1590#mA #mB #n
1591elim n
1592[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
1593| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
1594     whd in ⊢ (??%%);
1595     >(bestorev_beloadv_conservation … Hstore … Hneq)
1596     >(Hind … Hstore … Hneq) @refl
1597] qed.
1598
1599(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
1600lemma bestorev_load_value_of_type_conservation :
1601  ∀mA,mB,wb,wo,v.
1602    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1603    ∀rb,ro. eq_block wb rb = false →
1604    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1605#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
1606cases ty
1607[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1608| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //
1609[ 1: elim sz | 2: elim fsz | 3: | 4: ]
1610whd in ⊢ (??%%);
1611>(bestorev_loadn_conservation … Hstore … Hneq) @refl
1612qed.
1613
1614(* Writing in the "extended" part of a memory preserves the underlying injection *)
1615lemma bestorev_memory_ext_to_load_sim :
1616  ∀E,mA,mB,mC.
1617  ∀Hext:memory_ext E mA mB.
1618  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1619  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1620  load_sim E mA mC.
1621#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
1622#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1623(* Show that (wb ≠ b2) *)
1624lapply (me_writeable_ok … Hext … Hvalid Hembed) #Hb2
1625lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
1626cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
1627<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
1628@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
1629qed.
1630
1631(* Writing in the "extended" part of a memory preserves the whole memory injection *)
1632lemma bestorev_memory_ext_to_memory_inj :
1633  ∀E,mA,mB,mC.
1634  ∀Hext:memory_ext E mA mB.
1635  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1636  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1637  memory_inj E mA mC.
1638#E #mA * #contentsB #nextblockB #HnextblockB #mC
1639#Hext #wb #wo #v #Hwb #Hstore
1640%
1641[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
1642elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
1643#Hmem
1644[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj
1645whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
1646normalize in ⊢ (% → ?); #Hlt_wb
1647>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
1648cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
1649normalize nodelta
1650[ 2: #Habsurd destruct (Habsurd) ]
1651#Heq destruct (Heq)
1652#b #b' #o' #Hembed @(Hcodomain … Hembed)
1653qed.
1654
1655(* It even preserves memory extensions, with the same writeable blocks.  *)
1656lemma bestorev_memory_ext_to_memory_ext :
1657  ∀E,mA,mB.
1658  ∀Hext:memory_ext E mA mB.
1659  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1660  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
1661  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
1662#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
1663%{(mk_memory_ext …
1664      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
1665      (me_writeable … Hext)
1666      ?
1667      (me_writeable_ok … Hext)
1668 )} try @refl
1669#b #Hmemb
1670lapply (me_writeable_valid … Hext b Hmemb)
1671lapply (me_writeable_valid … Hext wb Hmem)
1672elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
1673lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
1674>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
1675cases (if Zleb (low (contentsB wb)) (offv wo) 
1676       then Zltb (offv wo) (high (contentsB wb)) 
1677       else false)
1678normalize [ 2: #Habsurd destruct (Habsurd) ]
1679#Heq destruct (Heq) @Hb_valid
1680qed.
1681
1682(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
1683lemma storen_memory_ext_to_memory_ext :
1684  ∀E,mA,l,mB,mC.
1685  ∀Hext:memory_ext E mA mB.
1686  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1687  storen mB (mk_pointer wb wo) l = Some ? mC →
1688  memory_ext E mA mC.
1689#E #mA #l elim l
1690[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
1691     @Hext
1692| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
1693     whd in ⊢ ((??%?) → ?);
1694     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
1695     cases (bestorev mB (mk_pointer wb wo) hd)
1696     normalize nodelta
1697     [ 1: #H #Habsurd destruct (Habsurd) ]
1698     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
1699     @(Hind … HextD … Hstore)
1700     <Heq @Hmem
1701] qed.     
1702
1703(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
1704lemma store_value_of_type_memory_ext_to_memory_ext :
1705  ∀E,mA,mB,mC.
1706  ∀Hext:memory_ext E mA mB.
1707  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1708  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
1709  memory_ext E mA mC.
1710#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
1711cases ty
1712[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1713| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1714whd in ⊢ ((??%?) → ?);
1715[ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
1716#Hstore
1717@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
1718qed.
1719
1720(* End of the memory injection-related stuff. *)
1721(* ------------------------------------------ *)
1722
1723(* Lookup functions in list environments (used to type local variables in functions) *)     
1724let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
1725match l with
1726[ nil ⇒ false
1727| cons hd tl ⇒
1728  let 〈id, ty〉 ≝ hd in
1729  match identifier_eq SymbolTag i id with
1730  [ inl Hid_eq ⇒ true
1731  | inr Hid_neq ⇒ mem_assoc_env i tl 
1732  ]
1733].
1734
1735let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝
1736match l with
1737[ nil ⇒ None ?
1738| cons hd tl ⇒
1739  let 〈id, ty〉 ≝ hd in
1740  match identifier_eq SymbolTag i id with
1741  [ inl Hid_eq ⇒ Some ? ty
1742  | inr Hid_neq ⇒ assoc_env i tl 
1743  ]
1744].
1745
1746(* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension
1747   of the environment [e1] s.t. the new binders are in [new], and such that those
1748   new binders are "writeable" in the memory extension [Hext] *)
1749definition disjoint_extension ≝
1750λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem).
1751λ(new : list (ident × type)). λ(E:embedding). λ(Hext: memory_ext E m1 m2).
1752  ∀id. match mem_assoc_env id new with
1753       [ true ⇒
1754           ∃b. lookup ?? e2 id = Some ? b
1755            ∧ meml ? b (me_writeable … Hext)
1756            ∧ lookup ?? e1 id = None ?
1757       | false ⇒
1758         match lookup ?? e1 id with
1759         [ None ⇒ lookup ?? e2 id = None ?
1760         | Some b1 ⇒
1761           match lookup ?? e2 id with
1762           [ None ⇒ False
1763           | Some b2 ⇒
1764             valid_block m1 b1 ∧
1765             value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))
1766           ]
1767         ]
1768       ].
1769
1770(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
1771 * the variable is not in a local environment, then we search into the global one.
1772 * A proper "extension" of a local environment should be such that the extension
1773 * does not collide with a given global env.
1774 * To see the details of why we need that, see [exec_lvalue'], Evar id case.
1775 *)
1776definition ext_fresh_for_genv ≝
1777λ(ext : list (ident × type)). λ(ge : genv).
1778  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.
1779
1780(* Any environment is a "disjoint" extension of itself with nothing. *)
1781(*
1782lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].
1783#e #m #ty #id
1784normalize in match (mem_assoc_env id []); normalize nodelta
1785cases (lookup ?? e id) try //
1786#b normalize nodelta
1787% #ty cases (load_value_of_type ????)
1788[ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj //
1789cases (assoc_env id ty) //
1790qed. *)
1791
1792
1793(* "generic" simulation relation on [res ?] *)
1794definition res_sim ≝
1795  λ(A : Type[0]).
1796  λ(eq : A → A → Prop).
1797  λ(r1, r2 : res A).
1798  ∀a1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2.
1799
1800(* Specialisation of [res_sim] to match [exec_expr] *)
1801definition exec_expr_sim ≝ λE.
1802  res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)).
1803
1804(* Specialisation of [res_sim] to match [exec_lvalue] *)
1805definition exec_lvalue_sim ≝ λE.
1806  res_sim (block × offset × trace)
1807    (λr1,r2.
1808      let 〈b1,o1,tr1〉 ≝ r1 in
1809      let 〈b2,o2,tr2〉 ≝ r2 in
1810      value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2).
1811
1812lemma 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.
1813#ty #m #b #o cases (load_value_of_type ty m b o)
1814[ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed.
1815
1816(*
1817lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'.
1818   env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
1819   〈f',vars〉 = function_switch_removal f →
1820   env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
1821   environment_extension env env' vars.
1822
1823#f #f'
1824cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append
1825cases (fn_params f) cases (fn_vars f)
1826[ 1: #vars >append_nil >append_nil >nil_append elim vars   
1827   [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct //
1828   | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq
1829        whd in ⊢ ((???(???%)) → ?);
1830 #Henv #Hswrem #Henv'
1831#id   
1832*)
1833
1834(*
1835lemma substatement_fresh : ∀s,u.
1836    fresh_for_statement s u →
1837    substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
1838#s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s)
1839try /by I/
1840[ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption
1841| 2: *
1842    [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
1843         #Hfresh_e #Hfresh_args @conj try assumption
1844         normalize nodelta in Hfresh_args;
1845         >max_id_commutative in Hfresh_args; >max_id_one_neutral
1846         #Hfresh_args         
1847    | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
1848         #Hfresh_e #H lapply (fresh_max_split ??? H) *
1849         #Hfresh_ret #Hfresh_args @conj try @conj try assumption ]
1850    elim args in Hfresh_args;
1851    [ 1,3: //
1852    | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???);
1853            >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj
1854            [ 1,3: @Hu
1855            | 2,4: @Hind assumption ] ]
1856| 3: #s1 #s2 #_ #_
1857     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
1858     whd in match (substatement_P ??); /2/
1859| 4: #e #cond #iftrue #iffalse #_
1860     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
1861     #Hexpr #H2 lapply (fresh_max_split … H2) * /2/
1862| 5,6: #e #stm #_
1863     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/
1864| 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) *
1865      #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond
1866      elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/
1867| 8: #ret #H whd elim ret in H; try //     
1868| 9: #expr #ls #Hind #H whd @conj
1869     [ 1: elim (fresh_max_split … H) //
1870     | 2: @Hind elim (fresh_max_split … H) // ]
1871| 10: #l #body #Hind #H whd elim (fresh_max_split … H) //
1872| 11: #sz #i #hd #tl #Hhd #Htl #H whd
1873     elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj //
1874     @Htl //
1875] qed.
1876*)
1877
1878(* Eliminating switches introduces fresh variables. [environment_extension] characterizes
1879 * a local environment extended by some local variables. *)
1880 
1881
1882(* lookup on environment extension *)
1883(*
1884lemma extension_lookup :
1885  ∀map, map', ext, id, result.
1886  environment_extension map map' ext →
1887  lookup ?? map id = Some ? result →
1888  lookup ?? map' id = Some ? result.
1889#map #map' #ext #id #result #Hext lapply (Hext id)
1890cases (mem_assoc_env ??) normalize nodelta
1891[ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd)
1892| 2: #H >H // ] qed.
1893
1894*)
1895
1896(* Extending a map by an empty list of variables yields an observationally equivalent
1897 * environment. *)
1898(*
1899lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'.
1900* #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H
1901[ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
1902     cases (lookup_opt block id map2) normalize
1903     [ 1: >H #H2 >H2 @refl
1904     | 2: #b >H cases v
1905          [ 1: normalize * #H @(False_ind … H)
1906          | 2: #block normalize // ] ]
1907| 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
1908     >H cases v normalize try //
1909     #block cases (lookup_opt ? id map1) normalize try //
1910     * #H @(False_ind … H)
1911] qed. *)
1912
1913(* If two identifier maps are observationally equal, then they contain the same bocks.
1914 * see maps_obsequiv.ma for the details of the proof. *)
1915(*
1916lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'.
1917* #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold
1918>Hfold @refl
1919qed.
1920*)
1921
1922(* Simulation relations. *)
1923inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
1924| swc_stop : ∀fvs.
1925    switch_cont_sim fvs Kstop Kstop
1926| swc_seq : ∀fvs,s,k,k',u,result.
1927    fresh_for_statement s u →
1928    switch_cont_sim fvs k k' →
1929    switch_removal s fvs u = Some ? result →
1930    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
1931| swc_while : ∀fvs,e,s,k,k',u,result.
1932    fresh_for_statement (Swhile e s) u →
1933    switch_cont_sim fvs k k' →
1934    switch_removal s fvs u = Some ? result →
1935    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
1936| swc_dowhile : ∀fvs,e,s,k,k',u,result.
1937    fresh_for_statement (Sdowhile e s) u →
1938    switch_cont_sim fvs k k' →
1939    switch_removal s fvs u = Some ? result →
1940    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
1941| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
1942    fresh_for_statement (Sfor Sskip e s1 s2) u →
1943    switch_cont_sim fvs k k' →
1944    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
1945    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
1946| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1947    fresh_for_statement (Sfor Sskip e s1 s2) u →
1948    switch_cont_sim fvs k k' →
1949    switch_removal s1 fvs u = Some ? result1 →
1950    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
1951    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
1952| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1953    fresh_for_statement (Sfor Sskip e s1 s2) u →
1954    switch_cont_sim fvs k k' →
1955    switch_removal s1 fvs u = Some ? result1 →
1956    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
1957    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
1958| swc_switch : ∀fvs,k,k'.
1959    switch_cont_sim fvs k k' →
1960    switch_cont_sim fvs (Kswitch k) (Kswitch k')
1961| swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
1962    switch_cont_sim fvs k k' →
1963    (* /!\ Update [en] with [fvs'] ... *)
1964    switch_cont_sim
1965      (map … (fst ??) (\snd (function_switch_removal f)))
1966      (Kcall r f en k)
1967      (Kcall r (\fst (function_switch_removal f)) en' k').
1968
1969
1970(*
1971 en' = exec_alloc_variables en m (\snd (function_switch_removal f))
1972 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
1973        variable dans en'.
1974
1975        1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que
1976           dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
1977           de savoir que :
1978           si je lookup une variable générée à partir d'un univers frais dans l'environement en',
1979           alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
1980           et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
1981           et à etre "(function_switch_removal f)-contained".
1982
1983        2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
1984           et l'update n'altèrent pas le comportement du reste du programme.
1985
1986        relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
1987                   depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
1988                   en particulier, si u est frais pour S1 u est frais pour S0.
1989
1990        Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
1991                    "environment_extension en en' (\fst (\fst (switch_removal s u)))"
1992                   
1993 ---------------------------------------------------------------
1994 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
1995   et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
1996   on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
1997   en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
1998*)
1999
2000inductive switch_state_sim : state → state → Prop ≝
2001| sws_state : ∀u,f,s,k,k',m,m',result.
2002    ∀env, env', f', vars.
2003    ∀E:embedding.   
2004    ∀Hext:memory_ext E m m'.
2005    fresh_for_statement s u →
2006    (*
2007    env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
2008    env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
2009    *)
2010    〈f',vars〉 = function_switch_removal f →
2011    disjoint_extension env m env' m' vars E Hext →
2012    switch_removal s (map ?? (fst ??) vars) u = Some ? result →
2013    switch_cont_sim (map ?? (fst ??) vars) k k' →
2014    switch_state_sim
2015      (State f s k env m)
2016      (State f' (ret_st ? result) k' env' m')
2017| sws_callstate : ∀vars, fd,args,k,k',m.
2018    switch_cont_sim vars k k' →
2019    switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m)
2020| sws_returnstate : ∀vars,res,k,k',m.
2021    switch_cont_sim vars k k' →
2022    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
2023| sws_finalstate : ∀r.
2024    switch_state_sim (Finalstate r) (Finalstate r).
2025
2026lemma call_cont_swremoval : ∀fv,k,k'.
2027  switch_cont_sim fv k k' →
2028  switch_cont_sim fv (call_cont k) (call_cont k').
2029#fv #k0 #k0' #K elim K /2/
2030qed.
2031
2032(* [eventually ge P s tr] states that after a finite number of [exec_step], the
2033   property P on states will be verified. *)
2034inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
2035| eventually_base : ∀s,t,s'.
2036    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
2037    P s' →
2038    eventually ge P s t
2039| eventually_step : ∀s,t,s',t',trace.
2040    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
2041    eventually ge P s' t' →
2042    trace = (t ⧺ t') →
2043    eventually ge P s trace.
2044
2045(* [eventually] is not so nice to use directly, we would like to make the mandatory
2046 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
2047   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
2048lemma eventually_now : ∀ge,P,s,t.
2049  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
2050   eventually ge P s t.
2051#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
2052qed.
2053(*   
2054lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
2055                                      ∃t'.eventually ge P s (t ⧺ t').
2056#ge #P #s #t * #s' * #Hexec #HP %{E0} normalize >(append_nil ? t) %1{????? Hexec HP}
2057qed.
2058*)
2059lemma eventually_later : ∀ge,P,s,t.
2060   (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) →
2061    eventually ge P s t.
2062#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
2063try assumption
2064qed.
2065
2066(* lift value_eq to option block *)
2067definition option_block_eq ≝ λE,ob1,ob2.
2068match ob1 with
2069[ None ⇒
2070  match ob2 with
2071  [ None ⇒ True
2072  | Some _ ⇒ False ]
2073| Some b1 ⇒
2074  match ob2 with
2075  [ None ⇒ False
2076  | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))  ]
2077].
2078
2079definition value_eq_opt ≝ λE,ov1,ov2.
2080match ov1 with
2081[ None ⇒
2082  match ov2 with
2083  [ None ⇒ True
2084  | Some _ ⇒ False ]
2085| Some v1 ⇒
2086  match ov2 with
2087  [ None ⇒ False
2088  | Some v2 ⇒
2089    value_eq E v1 v2 ]
2090].
2091
2092record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
2093  rg_find_symbol: ∀s.
2094    option_block_eq E (find_symbol ? ge s) (find_symbol ? ge' s);
2095  rg_find_funct: ∀v,f.
2096    find_funct ? ge v = Some ? f →
2097    find_funct ? ge' v = Some ? (t f);
2098  rg_find_funct_ptr: ∀b,f.
2099    find_funct_ptr ? ge b = Some ? f →
2100    find_funct_ptr ? ge' b = Some ? (t f)
2101}.
2102
2103lemma exec_lvalue_expr_elim :
2104  ∀E,r1,r2,Pok,Qok.
2105  ∀H:exec_lvalue_sim E r1 r2.
2106  (∀bo1,bo2,tr.
2107    let 〈b1,o1〉 ≝ bo1 in
2108    let 〈b2,o2〉 ≝ bo2 in
2109    value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) →
2110    match Pok 〈bo1,tr〉 with
2111    [ Error err ⇒ True
2112    | OK vt1 ⇒
2113      let 〈val1,trace1〉 ≝ vt1 in
2114      match Qok 〈bo2,tr〉 with
2115      [ Error err ⇒ False
2116      | OK vt2 ⇒
2117        let 〈val2,trace2〉 ≝ vt2 in
2118        trace1 = trace2 ∧ value_eq E val1 val2     
2119      ]
2120    ]) →
2121  exec_expr_sim E
2122    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
2123    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
2124#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
2125elim r1
2126[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
2127| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
2128     * #a2 * #Hr2 >Hr2 normalize nodelta
2129     elim a1 * #b1 #o1 #tr1
2130     elim a2 * #b2 #o2 #tr2 normalize nodelta
2131     * #Hvalue_eq #Htrace_eq #H2
2132     destruct (Htrace_eq)
2133     lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq)
2134     cases (Pok 〈b1, o1, tr2〉)
2135     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
2136     | 1: * #v1 #tr1' normalize nodelta #H3 whd
2137          * #v1' #tr1'' #Heq destruct (Heq)
2138          cases (Qok 〈b2,o2,tr2〉) in H3;
2139          [ 2: #error #Hfalse @(False_ind … Hfalse)
2140          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
2141               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
2142] ] ] qed.
2143
2144lemma exec_expr_expr_elim :
2145  ∀E,r1,r2,Pok,Qok.
2146  ∀H:exec_expr_sim E r1 r2.
2147  (∀v1,v2,trace.
2148    value_eq E v1 v2 →
2149    match Pok 〈v1,trace〉 with
2150    [ Error err ⇒ True
2151    | OK vt1 ⇒
2152      let 〈val1,trace1〉 ≝ vt1 in
2153      match Qok 〈v2,trace〉 with
2154      [ Error err ⇒ False
2155      | OK vt2 ⇒
2156        let 〈val2,trace2〉 ≝ vt2 in
2157        trace1 = trace2 ∧ value_eq E val1 val2     
2158      ]
2159    ]) →
2160  exec_expr_sim E
2161    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
2162    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
2163#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
2164elim r1
2165[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
2166| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
2167     * #a2 * #Hr2 >Hr2 normalize nodelta
2168     elim a1 #v1 #tr1
2169     elim a2 #v2 #tr2 normalize nodelta
2170     * #Hvalue_eq #Htrace_eq #H2
2171     destruct (Htrace_eq)
2172     lapply (H2 v1 v2 tr2 Hvalue_eq)
2173     cases (Pok 〈v1, tr2〉)
2174     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
2175     | 1: * #v1 #tr1' normalize nodelta #H3 whd
2176          * #v1' #tr1'' #Heq destruct (Heq)
2177          cases (Qok 〈v2,tr2〉) in H3;
2178          [ 2: #error #Hfalse @(False_ind … Hfalse)
2179          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
2180               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
2181] ] ] qed.
2182
2183(* Commutation results of standard binary operations with value_eq. *)
2184lemma unary_operation_value_eq :
2185  ∀E,op,v1,v2,ty.
2186   value_eq E v1 v2 →
2187   ∀r1.
2188   sem_unary_operation op v1 ty = Some ? r1 →
2189    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
2190#E #op #v1 #v2 #ty #Hvalue_eq #r1
2191inversion Hvalue_eq
2192[ 1: #v #Hv1 #Hv2 #_ destruct
2193     cases op normalize
2194     [ 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 ]
2195          normalize #Habsurd destruct (Habsurd)
2196     | 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 ]
2197          normalize #Habsurd destruct (Habsurd)
2198     | 2: #Habsurd destruct (Habsurd) ]
2199| 2: #vsz #i #Hv1 #Hv2 #_
2200     cases op
2201     [ 1: cases ty
2202          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2203          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
2204          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2205               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
2206               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
2207               //
2208          | *: #Habsurd destruct (Habsurd) ]
2209     | 2: whd in match (sem_unary_operation ???);     
2210          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
2211     | 3: whd in match (sem_unary_operation ???);
2212          cases ty
2213          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2214          normalize nodelta
2215          whd in ⊢ ((??%?) → ?);
2216          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2217               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
2218          | *: #Habsurd destruct (Habsurd) ] ]
2219| 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2220     cases op normalize nodelta
2221     [ 1: cases ty
2222          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2223          whd in match (sem_notbool ??);
2224          #Heq1 destruct
2225          cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
2226     | 2: normalize #Habsurd destruct (Habsurd)
2227     | 3: cases ty
2228          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2229          whd in match (sem_neg ??);
2230          #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
2231| 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2232     cases op normalize nodelta
2233     [ 1: cases ty
2234          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2235          whd in match (sem_notbool ??);
2236          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2237     | 2: normalize #Habsurd destruct (Habsurd)
2238     | 3: cases ty
2239          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2240          whd in match (sem_neg ??);
2241          #Heq1 destruct ]
2242| 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
2243     cases op normalize nodelta
2244     [ 1: cases ty
2245          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2246          whd in match (sem_notbool ??);         
2247          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2248     | 2: normalize #Habsurd destruct (Habsurd)
2249     | 3: cases ty
2250          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2251          whd in match (sem_neg ??);         
2252          #Heq1 destruct ]
2253]
2254qed.
2255
2256
2257(* value_eq lifts to addition *)
2258lemma add_value_eq :
2259  ∀E,v1,v2,v1',v2',ty1,ty2.
2260   value_eq E v1 v2 →
2261   value_eq E v1' v2' →
2262   (* memory_inj E m1 m2 →  This injection seems useless TODO *)
2263   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
2264           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2265#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2266@(value_eq_inversion E … Hvalue_eq1)
2267[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2268[ 1: whd in match (sem_add ????); normalize nodelta
2269     cases (classify_add ty1 ty2) normalize nodelta
2270     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
2271     #Habsurd destruct (Habsurd)
2272| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2273     cases (classify_add ty1 ty2) normalize nodelta     
2274     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2275     [ 2,3,5: #Habsurd destruct (Habsurd) ]
2276     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2277     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2278     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
2279     [ 1: @intsize_eq_elim_elim
2280          [ 1: #_ #Habsurd destruct (Habsurd)
2281          | 2: #Heq destruct (Heq) normalize nodelta
2282               #Heq destruct (Heq)
2283               /3 by ex_intro, conj, vint_eq/ ]
2284     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
2285          /3 by ex_intro, conj, vint_eq/
2286     | 3: #Heq destruct (Heq)
2287          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
2288          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
2289          @vptr_eq whd in match (pointer_translation ??);
2290          cases (E b1') in Hembed;
2291          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2292          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2293               whd in match (shift_pointer_n ????);
2294               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
2295                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i))
2296               [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ]
2297               #Heq >Heq @refl ]
2298     ]
2299| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2300     cases (classify_add ty1 ty2) normalize nodelta     
2301     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2302     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2303     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2304     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2305     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2306     #Heq destruct (Heq)
2307     /3 by ex_intro, conj, vfloat_eq/
2308| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2309     cases (classify_add ty1 ty2) normalize nodelta     
2310     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2311     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2312     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2313     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2314     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2315     @eq_bv_elim
2316     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2317     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2318| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2319     cases (classify_add ty1 ty2) normalize nodelta
2320     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2321     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2322     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2323     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2324     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2325     #Heq destruct (Heq)
2326     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
2327     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2328     elim p1 in Hembed; #b1 #o1 normalize nodelta
2329     cases (E b1)
2330     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2331     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2332          normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
2333          @refl
2334     ]
2335] qed.
2336
2337(* Offset subtraction is invariant by translation *)
2338lemma sub_offset_translation :
2339 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
2340#n #x #y #delta
2341whd in match (sub_offset ???) in ⊢ (??%%);
2342elim x #x' elim y #y' elim delta #delta'
2343normalize in match (offset_plus ??);
2344normalize in match (offset_plus ??);
2345cut ((x' - y') = (x'+delta'-(y'+delta')))
2346[ whd in match (Zminus ??) in ⊢ (??%%);
2347  >(Zopp_Zplus y' delta') <associative_Zplus /2/ ]
2348#Heq >Heq @refl
2349qed.   
2350
2351(* value_eq lifts to addition *)
2352lemma sub_value_eq :
2353  ∀E,v1,v2,v1',v2',ty1,ty2.
2354   value_eq E v1 v2 →
2355   value_eq E v1' v2' →
2356   ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
2357           ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2358#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2359@(value_eq_inversion E … Hvalue_eq1)
2360[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2361[ 1: whd in match (sem_sub ????); normalize nodelta
2362     cases (classify_sub ty1 ty2) normalize nodelta
2363     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
2364     #Habsurd destruct (Habsurd)
2365| 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2366     cases (classify_sub ty1 ty2) normalize nodelta     
2367     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2368     [ 2,3,5: #Habsurd destruct (Habsurd) ]
2369     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2370     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2371     [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ]
2372     @intsize_eq_elim_elim
2373      [ 1: #_ #Habsurd destruct (Habsurd)
2374      | 2: #Heq destruct (Heq) normalize nodelta
2375           #Heq destruct (Heq)
2376          /3 by ex_intro, conj, vint_eq/           
2377      ]
2378| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2379     cases (classify_sub ty1 ty2) normalize nodelta     
2380     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2381     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2382     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2383     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2384     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2385     #Heq destruct (Heq)
2386     /3 by ex_intro, conj, vfloat_eq/
2387| 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2388     cases (classify_sub ty1 ty2) normalize nodelta
2389     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2390     [ 1,2,5: #Habsurd destruct (Habsurd) ]
2391     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2392     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2393     [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ]         
2394     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2395                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2396     | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
2397| 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2398     cases (classify_sub ty1 ty2) normalize nodelta
2399     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2400     [ 1,2,5: #Habsurd destruct (Habsurd) ]
2401     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2402     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2403     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
2404     #Heq destruct (Heq)
2405     [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
2406          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2407          elim p1 in Hembed; #b1 #o1 normalize nodelta
2408          cases (E b1)
2409          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2410          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2411               normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
2412               @refl
2413          ]
2414     | 2: lapply Heq @eq_block_elim
2415          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
2416          | 1: #Hpblock1_eq normalize nodelta
2417               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
2418               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
2419               whd in ⊢ ((??%?) → (??%?) → ?);
2420               cases (E b1') normalize nodelta
2421               [ 1: #Habsurd destruct (Habsurd) ]
2422               * #dest_block #dest_off normalize nodelta
2423               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_identity normalize nodelta
2424               cases (eqb (sizeof tsg) O) normalize nodelta
2425               [ 1: #Habsurd destruct (Habsurd)
2426               | 2: >(sub_offset_translation 32 off1 off1' dest_off)
2427                    cases (division_u 31
2428                            (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
2429                            (repr (sizeof tsg)))
2430                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
2431                    | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
2432                         /3 by ex_intro, conj, vint_eq/ ]
2433    ] ] ]
2434] qed.
2435
2436
2437lemma mul_value_eq :
2438  ∀E,v1,v2,v1',v2',ty1,ty2.
2439   value_eq E v1 v2 →
2440   value_eq E v1' v2' →
2441   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
2442           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2443#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2444@(value_eq_inversion E … Hvalue_eq1)
2445[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2446[ 1: whd in match (sem_mul ????); normalize nodelta
2447     cases (classify_aop ty1 ty2) normalize nodelta
2448     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2449     #Habsurd destruct (Habsurd)
2450| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2451     cases (classify_aop ty1 ty2) normalize nodelta
2452     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2453     [ 2,3: #Habsurd destruct (Habsurd) ]
2454     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2455     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2456     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2457     @intsize_eq_elim_elim
2458      [ 1: #_ #Habsurd destruct (Habsurd)
2459      | 2: #Heq destruct (Heq) normalize nodelta
2460           #Heq destruct (Heq)
2461          /3 by ex_intro, conj, vint_eq/           
2462      ]
2463| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2464     cases (classify_aop ty1 ty2) normalize nodelta
2465     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2466     [ 1,3: #Habsurd destruct (Habsurd) ]
2467     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
2468     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2469     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2470     #Heq destruct (Heq)
2471     /3 by ex_intro, conj, vfloat_eq/
2472| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2473     cases (classify_aop ty1 ty2) normalize nodelta
2474     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2475     #Habsurd destruct (Habsurd)
2476| 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2477     cases (classify_aop ty1 ty2) normalize nodelta
2478     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2479     #Habsurd destruct (Habsurd)
2480] qed.
2481
2482lemma div_value_eq :
2483  ∀E,v1,v2,v1',v2',ty1,ty2.
2484   value_eq E v1 v2 →
2485   value_eq E v1' v2' →
2486   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
2487           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2488#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2489@(value_eq_inversion E … Hvalue_eq1)
2490[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2491[ 1: whd in match (sem_div ????); normalize nodelta
2492     cases (classify_aop ty1 ty2) normalize nodelta
2493     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2494     #Habsurd destruct (Habsurd)
2495| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2496     cases (classify_aop ty1 ty2) normalize nodelta
2497     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2498     [ 2,3: #Habsurd destruct (Habsurd) ]
2499     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2500     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2501     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2502     elim sg normalize nodelta
2503     @intsize_eq_elim_elim
2504     [ 1,3: #_ #Habsurd destruct (Habsurd)
2505     | 2,4: #Heq destruct (Heq) normalize nodelta
2506            @(match (division_s (bitsize_of_intsize sz') i i') with
2507              [ None ⇒ ?
2508              | Some bv' ⇒ ? ])
2509            [ 1: normalize  #Habsurd destruct (Habsurd)
2510            | 2: normalize #Heq destruct (Heq)
2511                 /3 by ex_intro, conj, vint_eq/
2512            | 3,4: elim sz' in i' i; #i' #i
2513                   normalize in match (pred_size_intsize ?);
2514                   generalize in match division_u; #division_u normalize
2515                   @(match (division_u ???) with
2516                    [ None ⇒ ?
2517                    | Some bv ⇒ ?]) normalize nodelta
2518                   #H destruct (H)
2519                  /3 by ex_intro, conj, vint_eq/ ]
2520     ]
2521| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2522     cases (classify_aop ty1 ty2) normalize nodelta
2523     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2524     [ 1,3: #Habsurd destruct (Habsurd) ]
2525     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
2526     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2527     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2528     #Heq destruct (Heq)
2529     /3 by ex_intro, conj, vfloat_eq/
2530| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2531     cases (classify_aop ty1 ty2) normalize nodelta
2532     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2533     #Habsurd destruct (Habsurd)
2534| 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2535     cases (classify_aop ty1 ty2) normalize nodelta
2536     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2537     #Habsurd destruct (Habsurd)
2538] qed.
2539
2540lemma mod_value_eq :
2541  ∀E,v1,v2,v1',v2',ty1,ty2.
2542   value_eq E v1 v2 →
2543   value_eq E v1' v2' →
2544   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
2545           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2546#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2547@(value_eq_inversion E … Hvalue_eq1)
2548[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2549[ 1: whd in match (sem_mod ????); normalize nodelta
2550     cases (classify_aop ty1 ty2) normalize nodelta
2551     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2552     #Habsurd destruct (Habsurd)
2553| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2554     cases (classify_aop ty1 ty2) normalize nodelta
2555     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2556     [ 2,3: #Habsurd destruct (Habsurd) ]
2557     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2558     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2559     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2560     elim sg normalize nodelta
2561     @intsize_eq_elim_elim
2562     [ 1,3: #_ #Habsurd destruct (Habsurd)
2563     | 2,4: #Heq destruct (Heq) normalize nodelta
2564            @(match (modulus_s (bitsize_of_intsize sz') i i') with
2565              [ None ⇒ ?
2566              | Some bv' ⇒ ? ])
2567            [ 1: normalize  #Habsurd destruct (Habsurd)
2568            | 2: normalize #Heq destruct (Heq)
2569                 /3 by ex_intro, conj, vint_eq/
2570            | 3,4: elim sz' in i' i; #i' #i
2571                   generalize in match modulus_u; #modulus_u normalize
2572                   @(match (modulus_u ???) with
2573                    [ None ⇒ ?
2574                    | Some bv ⇒ ?]) normalize nodelta
2575                   #H destruct (H)
2576                  /3 by ex_intro, conj, vint_eq/ ]
2577     ]
2578| 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2579     cases (classify_aop ty1 ty2) normalize nodelta
2580     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2581     #Habsurd destruct (Habsurd)
2582| 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2583     cases (classify_aop ty1 ty2) normalize nodelta
2584     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2585     #Habsurd destruct (Habsurd)
2586| 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2587     cases (classify_aop ty1 ty2) normalize nodelta
2588     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2589     #Habsurd destruct (Habsurd)
2590] qed.
2591
2592(* boolean ops *)
2593lemma and_value_eq :
2594  ∀E,v1,v2,v1',v2'.
2595   value_eq E v1 v2 →
2596   value_eq E v1' v2' →
2597   ∀r1. (sem_and v1 v1'=Some val r1→
2598           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
2599#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2600@(value_eq_inversion E … Hvalue_eq1)
2601[ 2: #sz #i
2602     @(value_eq_inversion E … Hvalue_eq2)
2603     [ 2: #sz' #i' whd in match (sem_and ??);
2604          @intsize_eq_elim_elim
2605          [ 1: #_ #Habsurd destruct (Habsurd)
2606          | 2: #Heq destruct (Heq) normalize nodelta
2607               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2608] ]
2609normalize in match (sem_and ??); #arg1 destruct
2610normalize in match (sem_and ??); #arg2 destruct
2611normalize in match (sem_and ??); #arg3 destruct
2612normalize in match (sem_and ??); #arg4 destruct
2613qed.
2614
2615lemma or_value_eq :
2616  ∀E,v1,v2,v1',v2'.
2617   value_eq E v1 v2 →
2618   value_eq E v1' v2' →
2619   ∀r1. (sem_or v1 v1'=Some val r1→
2620           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
2621#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2622@(value_eq_inversion E … Hvalue_eq1)
2623[ 2: #sz #i
2624     @(value_eq_inversion E … Hvalue_eq2)
2625     [ 2: #sz' #i' whd in match (sem_or ??);
2626          @intsize_eq_elim_elim
2627          [ 1: #_ #Habsurd destruct (Habsurd)
2628          | 2: #Heq destruct (Heq) normalize nodelta
2629               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2630] ]
2631normalize in match (sem_or ??); #arg1 destruct
2632normalize in match (sem_or ??); #arg2 destruct
2633normalize in match (sem_or ??); #arg3 destruct
2634normalize in match (sem_or ??); #arg4 destruct
2635qed.
2636
2637lemma xor_value_eq :
2638  ∀E,v1,v2,v1',v2'.
2639   value_eq E v1 v2 →
2640   value_eq E v1' v2' →
2641   ∀r1. (sem_xor v1 v1'=Some val r1→
2642           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
2643#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2644@(value_eq_inversion E … Hvalue_eq1)
2645[ 2: #sz #i
2646     @(value_eq_inversion E … Hvalue_eq2)
2647     [ 2: #sz' #i' whd in match (sem_xor ??);
2648          @intsize_eq_elim_elim
2649          [ 1: #_ #Habsurd destruct (Habsurd)
2650          | 2: #Heq destruct (Heq) normalize nodelta
2651               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2652] ]
2653normalize in match (sem_xor ??); #arg1 destruct
2654normalize in match (sem_xor ??); #arg2 destruct
2655normalize in match (sem_xor ??); #arg3 destruct
2656normalize in match (sem_xor ??); #arg4 destruct
2657qed.
2658
2659lemma shl_value_eq :
2660  ∀E,v1,v2,v1',v2'.
2661   value_eq E v1 v2 →
2662   value_eq E v1' v2' →
2663   ∀r1. (sem_shl v1 v1'=Some val r1→
2664           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
2665#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2666@(value_eq_inversion E … Hvalue_eq1)
2667[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2668[ 2:
2669     @(value_eq_inversion E … Hvalue_eq2)
2670     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2671     [ 2: whd in match (sem_shl ??);
2672          cases (lt_u ???) normalize nodelta
2673          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
2674          | 2: #Habsurd destruct (Habsurd)
2675          ]
2676     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2677| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2678qed.
2679
2680lemma shr_value_eq :
2681  ∀E,v1,v2,v1',v2',ty,ty'.
2682   value_eq E v1 v2 →
2683   value_eq E v1' v2' →
2684   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
2685           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
2686#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
2687@(value_eq_inversion E … Hvalue_eq1)
2688[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2689whd in match (sem_shr ????); whd in match (sem_shr ????);
2690[ 1: cases (classify_aop ty ty') normalize nodelta
2691     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2692     #Habsurd destruct (Habsurd)
2693| 2: cases (classify_aop ty ty') normalize nodelta
2694     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2695     [ 2,3: #Habsurd destruct (Habsurd) ]
2696     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2697     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2698     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2699     elim sg normalize nodelta
2700     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
2701     /3 by ex_intro, conj, refl, vint_eq/
2702| 3: cases (classify_aop ty ty') normalize nodelta
2703     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2704     #Habsurd destruct (Habsurd)
2705| 4: cases (classify_aop ty ty') normalize nodelta
2706     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2707     #Habsurd destruct (Habsurd)
2708| 5: cases (classify_aop ty ty') normalize nodelta
2709     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2710     #Habsurd destruct (Habsurd)
2711] qed.
2712
2713(* We want to prove that, but we can't since valid_pointers can in fact be one off outside the block,
2714   and [memory_inj] handles only stuff that is loadable (i.e. inside a block). TODO *)
2715lemma pointer_eq_valid :
2716∀E,m,m',p,p'.
2717 memory_inj E m m' →
2718 pointer_translation p E = Some ? p' →
2719 valid_pointer m p →
2720 valid_pointer m' p'.
2721@cthulhu qed.
2722
2723
2724lemma sem_cmp_value_eq :
2725  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
2726   value_eq E v1 v2 →
2727   value_eq E v1' v2' →
2728   memory_inj E m1 m2 →   
2729   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
2730           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
2731#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
2732cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????);
2733[ 1:
2734  cases (classify_cmp ty ty') normalize nodelta
2735  [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
2736  @(value_eq_inversion E … Hvalue_eq1)
2737  [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
2738  normalize nodelta
2739  [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ]
2740  @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2741  [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ]
2742  [ 5: elim sg normalize nodelta
2743       @intsize_eq_elim_elim
2744       [ 1,3: #_ #Habsurd destruct (Habsurd)
2745       | 2,4: #Heq destruct (Heq) normalize nodelta
2746              [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq)
2747              | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ]
2748              /3 by ex_intro, conj, vint_eq/ ]
2749  | 10: #Heq destruct (Heq) cases (Fcmp Ceq f f') /3 by ex_intro, conj, vint_eq/
2750  | 15: whd in match (sem_cmp_match ?); #Heq destruct (Heq)
2751        /3 by ex_intro, conj, vint_eq/
2752  | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
2753        /3 by ex_intro, conj, vint_eq/
2754  | 20: @cthulhu (* relies on [pointer_eq_valid] TODO *)   
2755  | *: #Habsurd destruct (Habsurd) ]
2756| *: @cthulhu ]
2757qed.
2758 
2759(* Commutation result for binary operators. *)
2760lemma binary_operation_value_eq :
2761  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
2762   value_eq E v1 v2 →
2763   value_eq E v1' v2' →
2764   memory_inj E m1 m2 →
2765   ∀r1.
2766   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
2767   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
2768#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
2769cases op
2770whd in match (sem_binary_operation ??????);
2771whd in match (sem_binary_operation ??????);
2772@cthulhu
2773qed.
2774
2775 
2776(* Simulation relation on expressions *)
2777lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
2778  ∀E:embedding.
2779  ∀Hext:memory_ext E m1 m2.
2780  switch_removal_globals E ? fundef_switch_removal ge ge' →
2781  disjoint_extension en1 m1 en2 m2 ext E Hext →
2782  ext_fresh_for_genv ext ge →
2783  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
2784  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
2785#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
2786@expr_lvalue_ind_combined
2787[ 1: #csz #cty #i #a1
2788     whd in match (exec_expr ????); elim cty
2789     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2790     normalize nodelta
2791     [ 2: cases (eq_intsize csz sz) normalize nodelta
2792          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
2793          | 2: #Habsurd destruct (Habsurd) ]
2794     | 4,5,6: #_ #H destruct (H)
2795     | *: #H destruct (H) ]
2796| 2: #ty #fl #a1
2797     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
2798| 3: *
2799  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
2800  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
2801  #ty whd in ⊢ (% → ?); #Hind try @I
2802  whd in match (Plvalue ???);
2803  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
2804       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
2805       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2806       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
2807           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
2808           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
2809           whd in match (load_value_of_type' ???);
2810           whd in match (load_value_of_type' ???);
2811           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
2812           cases (load_value_of_type ty m1 bl1 o1)
2813           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2814           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
2815                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
2816                    normalize /4 by ex_intro, conj/
2817  ] ] ]
2818| 4: #v #ty whd * * #b1 #o1 #tr1
2819     whd in match (exec_lvalue' ?????);
2820     whd in match (exec_lvalue' ?????);
2821     lapply (Hdisjoint v)
2822     lapply (Hext_fresh_for_genv v)
2823     cases (mem_assoc_env v ext) #Hglobal
2824     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
2825          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
2826          >(Hglobal (refl ??)) normalize
2827          #Habsurd destruct (Habsurd)
2828     | 2: normalize nodelta
2829          cases (lookup ?? en1 v) normalize nodelta
2830          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
2831               lapply (rg_find_symbol … Hrelated v)
2832               cases (find_symbol ???) normalize
2833               [ 1: #_ #Habsurd destruct (Habsurd)
2834               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
2835                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
2836                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
2837                         %{〈block',mk_offset OZ,[]〉} @conj try @refl
2838                         normalize /2/
2839                ] ]
2840         | 2: #block
2841              cases (lookup ?? en2 v) normalize nodelta
2842              [ 1: #Hfalse @(False_ind … Hfalse)
2843              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
2844                   %{〈b, zero_offset, E0〉} @conj try @refl
2845                   normalize /2/
2846    ] ] ]
2847| 5: #e #ty whd in ⊢ (% → %);
2848     whd in match (exec_lvalue' ?????);
2849     whd in match (exec_lvalue' ?????);
2850     cases (exec_expr ge en1 m1 e)
2851     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
2852          * elim v1 normalize nodelta
2853          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
2854          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
2855          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
2856          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
2857          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
2858               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
2859               #Hvalue_eq normalize
2860               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2861               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
2862               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
2863               %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
2864               normalize @conj // ]
2865     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
2866| 6: #ty #e #ty'
2867     #Hsim @(exec_lvalue_expr_elim … Hsim)
2868     cases ty
2869     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2870     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
2871     #tr #H @conj try @refl try assumption
2872| 7: #ty #op #e
2873     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
2874     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
2875     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
2876     [ 1: #_ @I
2877     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
2878           normalize /2/ ]
2879| *: @cthulhu ] qed.
2880
2881(* TODO: Old cases, to be ported to memory injection.
2882| 8: #ty #op #e1 #e2 #Hind1 #Hind2
2883     whd in match (exec_expr ge ???);   
2884     whd in match (exec_expr ge' ???);
2885     @(exec_expr_expr_elim … Hind1)
2886     cases (exec_expr ge en1 m1 e2) in Hind2;
2887     [ 2: #error normalize //
2888     | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 *
2889          #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq'
2890          >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????);
2891
2892
2893| 9: #ty #castty #e #Hind
2894     whd in match (exec_expr ge ???);   
2895     whd in match (exec_expr ge' ???);
2896     cases Hind
2897     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2898     | 1: cases (exec_expr ge en m e)
2899          [ 2: #error #_ @SimFail /2 by ex_intro/
2900          | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
2901          ]
2902     ]
2903| 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3
2904     whd in match (exec_expr ge ???);   
2905     whd in match (exec_expr ge' ???);
2906     cases Hind1
2907     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2908     | 1: cases (exec_expr ge en m e1)
2909          [ 2: #error #_ @SimFail /2 by ex_intro/
2910          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
2911               normalize nodelta
2912               cases (exec_bool_of_val ??)
2913               [ 2: #error @SimFail /2 by ex_intro/
2914               | 1: * whd in match (m_bind ?????); normalize nodelta
2915                    [ 1: cases Hind2
2916                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2917                         | 1: cases (exec_expr ge en m e2)
2918                              [ 2: #error #_  @SimFail /2 by ex_intro/
2919                              | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))                                   
2920                                   @SimOk normalize nodelta #a2
2921                                   whd in match (m_bind ?????); // ]
2922                         ]
2923                    | 2: cases Hind3
2924                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2925                         | 1: cases (exec_expr ge en m e3)
2926                              [ 2: #error #_  @SimFail /2 by ex_intro/
2927                              | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3)))
2928                                   @SimOk normalize nodelta #a3
2929                                   whd in match (m_bind ?????); // ]
2930                         ]
2931     ] ] ] ]                     
2932| 11: #ty #e1 #e2 #Hind1 #Hind2
2933     whd in match (exec_expr ge ???);   
2934     whd in match (exec_expr ge' ???);
2935     cases Hind1
2936     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2937     | 1: cases (exec_expr ge en m e1)
2938          [ 2: #error #_ @SimFail /2 by ex_intro/
2939          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
2940               normalize nodelta
2941               cases (exec_bool_of_val ??)
2942               [ 2: #error @SimFail /2 by ex_intro/
2943               | 1: * whd in match (m_bind ?????);
2944                    [ 2: @SimOk // ]
2945                    cases Hind2
2946                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2947                    | 1: cases (exec_expr ge en m e2)
2948                         [ 2: #error #_  @SimFail /2 by ex_intro/
2949                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
2950                              @SimOk #a2
2951                              whd in match (m_bind ?????); //
2952     ] ] ] ] ]
2953| 12: #ty #e1 #e2 #Hind1 #Hind2
2954     whd in match (exec_expr ge ???);   
2955     whd in match (exec_expr ge' ???);
2956     cases Hind1
2957     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2958     | 1: cases (exec_expr ge en m e1)
2959          [ 2: #error #_ @SimFail /2 by ex_intro/
2960          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
2961               normalize nodelta
2962               cases (exec_bool_of_val ??)
2963               [ 2: #error @SimFail /2 by ex_intro/
2964               | 1: * whd in match (m_bind ?????);
2965                    [ 1: @SimOk // ]
2966                    cases Hind2
2967                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2968                    | 1: cases (exec_expr ge en m e2)
2969                         [ 2: #error #_  @SimFail /2 by ex_intro/
2970                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
2971                              @SimOk #a2
2972                              whd in match (m_bind ?????); //
2973     ] ] ] ] ]
2974| 13: #ty #sizeof_ty
2975     whd in match (exec_expr ge ???);   
2976     whd in match (exec_expr ge' ???);
2977     @SimOk //
2978| 14: #ty #e #ty' #fld #Hind
2979     whd in match (exec_lvalue' ge ????);
2980     whd in match (exec_lvalue' ge' ????);
2981     whd in match (typeof ?);
2982     cases ty' in Hind;
2983     [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
2984     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
2985     normalize nodelta #Hind
2986     try (@SimFail /2 by ex_intro/)
2987     whd in match (exec_lvalue ????);
2988     whd in match (exec_lvalue ????);     
2989     cases Hind
2990     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2991     | 1,3: cases (exec_lvalue' ge en m e ?)
2992         [ 2,4: #error #_ @SimFail /2 by ex_intro/
2993         | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
2994     ] ]
2995| 15: #ty #l #e #Hind
2996     whd in match (exec_expr ge ???);
2997     whd in match (exec_expr ge' ???);
2998     cases Hind
2999     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3000     | 1: cases (exec_expr ge en m e)
3001        [ 2: #error #_ @SimFail /2 by ex_intro/
3002        | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
3003     ] ]
3004| 16: *
3005  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
3006  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
3007  #ty normalize in ⊢ (% → ?);
3008  [ 1,2: #_ @SimOk #a normalize //
3009  | 3,4,13: #H @(False_ind … H)
3010  | *: #_ @SimFail /2 by ex_intro/
3011  ]
3012] qed. *)
3013
3014(*
3015lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
3016related_globals ? fundef_switch_removal ge ge' →
3017∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
3018#ge #ge' #en #m #Hrelated #args
3019elim args
3020[ 1: /3/
3021| 2: #hd #tl #Hind normalize
3022     elim (sim_related_globals ge ge' en m Hrelated)
3023     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
3024     cases (exec_expr ge en m hd)
3025     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
3026     | 1: * #val_hd #trace_hd normalize nodelta
3027          cases Hind
3028          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
3029          | 1: cases (exec_exprlist ge en m tl)
3030               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
3031               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
3032                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
3033                    cases Hexec_hd
3034                    [ 2: * #error #Habsurd destruct (Habsurd)
3035                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
3036] ] ] ] qed.
3037*)
3038
3039(* The return type of any function is invariant under switch removal *)
3040lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
3041#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
3042qed.
3043
3044(* Similar stuff for fundefs *)
3045lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
3046* // qed.
3047
3048(*
3049lemma expr_fresh_lift :
3050  ∀e,u,id.
3051      fresh_for_expression e u →
3052      fresh_for_univ SymbolTag id u →
3053      fresh_for_univ SymbolTag (max_of_expr e id) u.
3054#e #u #id
3055normalize in match (fresh_for_expression e u);
3056#H1 #H2
3057>max_of_expr_rewrite
3058normalize in match (fresh_for_univ ???);
3059cases (max_of_expr e ?) in H1; #p #H1
3060cases id in H2; #p' #H2
3061normalize nodelta
3062cases (leb p p') normalize nodelta
3063[ 1: @H2 | 2: @H1 ]
3064qed. *)
3065
3066lemma while_fresh_lift : ∀e,s,u.
3067   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
3068#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
3069cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
3070cases (leb e s) try /2/
3071qed.
3072
3073(*
3074lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
3075#e0 #s0 #us0 normalize
3076cases (switch_removal s0 us0) * #body #newvars #u' normalize //
3077qed.*)
3078
3079lemma dowhile_fresh_lift : ∀e,s,u.
3080   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
3081#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
3082cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
3083cases (leb e s) try /2/
3084qed.
3085(*
3086lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
3087#e0 #s0 #us0 normalize
3088cases (switch_removal s0 us0) * #body #newvars #u' normalize //
3089qed.*)
3090
3091lemma for_fresh_lift : ∀cond,step,body,u.
3092  fresh_for_statement step u →
3093  fresh_for_statement body u →
3094  fresh_for_expression cond u →
3095  fresh_for_statement (Sfor Sskip cond step body) u.
3096#cond #step #body #u
3097whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
3098cases (max_of_statement step) #s
3099cases (max_of_statement body) #b
3100cases (max_of_expr cond) #c
3101whd in match (max_of_statement Sskip);
3102>(max_id_commutative least_identifier)
3103>max_id_one_neutral normalize nodelta
3104normalize elim u #u
3105cases (leb s b) cases (leb c b) cases (leb c s) try /2/
3106qed.
3107
3108(*
3109lemma for_commute : ∀e,stm1,stm2,u,uA.
3110   (uA=\snd  (switch_removal stm1 u)) →
3111   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
3112#e #stm1 #stm2 #u #uA #HuA
3113whd in match (sw_rem (Sfor ????) u);
3114whd in match (switch_removal ??);   
3115destruct
3116normalize in match (\snd (switch_removal Sskip u));
3117whd in match (sw_rem stm1 u);
3118cases (switch_removal stm1 u)
3119* #stm1' #fresh_vars #uA normalize nodelta
3120whd in match (sw_rem stm2 uA);
3121cases (switch_removal stm2 uA)
3122* #stm2' #fresh_vars2 #uB normalize nodelta
3123//
3124qed.*)
3125
3126(*
3127lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
3128*
3129[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
3130| 2: #e1 #e2 #u #_
3131     whd in match (sw_rem ??);
3132     whd in match (is_Sskip ?);
3133     try /2 by refl, ex_intro/
3134| 3: #ret #f #args #u
3135     whd in match (sw_rem ??);
3136     whd in match (is_Sskip ?);
3137     try /2 by refl, ex_intro/
3138| 4: #s1 #s2 #u
3139     whd in match (sw_rem ??);
3140     whd in match (switch_removal ??);     
3141     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
3142     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
3143     whd in match (is_Sskip ?);
3144     try /2 by refl, ex_intro/
3145| 5: #e #s1 #s2 #u #_
3146     whd in match (sw_rem ??);
3147     whd in match (switch_removal ??);     
3148     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3149     cases (switch_removal ? ?) * #e #f #h normalize nodelta
3150     whd in match (is_Sskip ?);
3151     try /2 by refl, ex_intro/
3152| 6,7: #e #s #u #_
3153     whd in match (sw_rem ??);
3154     whd in match (switch_removal ??);     
3155     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3156     whd in match (is_Sskip ?);
3157     try /2 by refl, ex_intro/
3158| 8: #s1 #e #s2 #s3 #u #_     
3159     whd in match (sw_rem ??);
3160     whd in match (switch_removal ??);     
3161     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3162     cases (switch_removal ? ?) * #e #f #g normalize nodelta
3163     cases (switch_removal ? ?) * #i #j #k normalize nodelta
3164     whd in match (is_Sskip ?);
3165     try /2 by refl, ex_intro/
3166| 9,10: #u #_     
3167     whd in match (is_Sskip ?);
3168     try /2 by refl, ex_intro/
3169| 11: #e #u #_
3170     whd in match (is_Sskip ?);
3171     try /2 by refl, ex_intro/
3172| 12: #e #ls #u #_
3173     whd in match (sw_rem ??);
3174     whd in match (switch_removal ??);
3175     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
3176     cases (fresh ??) #e #f normalize nodelta
3177     normalize in match (simplify_switch ???);
3178     cases (fresh ? f) #g #h normalize nodelta
3179     cases (produce_cond ????) * #k #l #m normalize nodelta
3180     whd in match (is_Sskip ?);
3181     try /2 by refl, ex_intro/
3182| 13,15: #lab #st #u #_
3183     whd in match (sw_rem ??);
3184     whd in match (switch_removal ??);
3185     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3186     whd in match (is_Sskip ?);
3187     try /2 by refl, ex_intro/
3188| 14: #lab #u     
3189     whd in match (is_Sskip ?);
3190     try /2 by refl, ex_intro/ ]
3191qed.
3192*)
3193
3194(*
3195lemma sw_rem_commute : ∀stm,u.
3196  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
3197#stm #u whd in match (sw_rem stm u); // qed.
3198*)
3199
3200lemma fresh_for_statement_inv :
3201  ∀u,s. fresh_for_statement s u →
3202        match u with
3203        [ mk_universe p ⇒ le (p0 one) p ].
3204* #p #s whd in match (fresh_for_statement ??);
3205cases (max_of_statement s) #s
3206normalize /2/ qed.
3207
3208lemma fresh_for_Sskip :
3209  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
3210#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3211
3212lemma fresh_for_Sbreak :
3213  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
3214#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3215
3216lemma fresh_for_Scontinue :
3217  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
3218#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3219
3220(*
3221lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
3222#s #u elim (switch_removal s u) * #res #fvs #u'
3223%{res} %{fvs} %{u'} //
3224qed.
3225
3226lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
3227#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
3228%{res} %{fvs} %{u'} //
3229qed.
3230*)
3231
3232lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
3233#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
3234#s #lab #u' %{s} %{lab} %{u'} //
3235qed.
3236
3237(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
3238lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
3239* * *
3240[ 1,5,9: #H @(False_ind … (H (refl ??)))
3241| *: #_ normalize @refl ]
3242qed.
3243
3244lemma exec_expr_int : ∀ge,e,m,expr.
3245    (∃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〉)).
3246#ge #e #m #expr cases (exec_expr ge e m expr)
3247[ 2: #error %2 #sz #n #tr % #H destruct (H)
3248| 1: * #val #trace cases val
3249     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
3250     | 3: #fl | 4: | 5: #ptr ]
3251     %2 #sz #n #tr % #H destruct (H)
3252] qed.
3253
3254(*
3255lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
3256  exec_expr ge e m cond = OK ? 〈v,tr〉 →
3257  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
3258  exec_expr ge' e m cond = OK ? 〈v,tr〉.
3259#ge #ge' #e #m #cond #v #tr #H *
3260[ 1: #Hsim >(Hsim ? H) //
3261| 2: * #error >H #Habsurd destruct (Habsurd) ]
3262qed. *)
3263
3264(*
3265lemma switch_simulation :
3266∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
3267 switch_cont_sim k k' →
3268 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
3269 fresh_for_statement (Sswitch cond switchcases) u →
3270 ∃tr'.
3271 (eventually ge'
3272  (λs2':state
3273   .switch_state_sim
3274    (State f
3275     (seq_of_labeled_statement (select_switch condsz condval switchcases))
3276     (Kswitch k) e m) s2')
3277  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
3278  tr').
3279#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
3280whd in match (sw_rem (Sswitch cond switchcases) u);
3281whd in match (switch_removal (Sswitch cond switchcases) u);
3282cases switchcases in Hfresh;
3283[ 1: #default_statement #Hfresh_for_default
3284     whd in match (switch_removal_branches ??);
3285     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
3286     elim (switch_removal_eq default_statement u)
3287     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
3288     normalize nodelta
3289     cut (u' = (\snd (switch_removal default_statement u)))
3290     [ 1: >Hdefault_statement_eq // ] #Heq_u'
3291     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
3292     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
3293     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
3294     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
3295     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
3296     normalize nodelta
3297     whd in match (simplify_switch (Expr ??) ?? uv2);
3298     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
3299     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
3300     -Hfreshness #Heq_uv3
3301     normalize nodelta whd in match (add_starting_lbl_list ????);
3302     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
3303     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
3304     -Hfreshness #Heq_uv4
3305     normalize nodelta
3306     @(eventually_later ge' ?? E0)
3307     whd in match (exec_step ??);
3308     %{(State (function_switch_removal f)
3309          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
3310          (Kseq
3311          (Ssequence
3312            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
3313            (Slabel exit_label Sskip))
3314          k') e m)} @conj try //
3315     @(eventually_later ge' ?? E0)
3316     whd in match (exec_step ??);
3317     
3318@chthulhu | @chthulhu
3319qed. *)
3320
3321
3322
3323(* Main theorem. To be ported and completed to memory injections. TODO *)
3324(*
3325theorem switch_removal_correction : ∀ge, ge'.
3326  related_globals ? fundef_switch_removal ge ge' →
3327  ∀s1, s1', tr, s2.
3328  switch_state_sim s1 s1' →
3329  exec_step ge s1 = Value … 〈tr,s2〉 →
3330  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
3331#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
3332inversion Hsim_state
3333[ 1: (* regular state *)
3334  #u #f #s #k #k' #m #m' #result #en #en' #f' #vars
3335  #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_
3336
3337  lapply (sim_related_globals ge ge' e m Hrelated) *
3338  #Hexpr_related #Hlvalue_related
3339  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
3340  cases s in Hu_fresh Heq_env;
3341 
3342
3343theorem switch_removal_correction : ∀ge, ge'.
3344  related_globals ? fundef_switch_removal ge ge' →
3345  ∀s1, s1', tr, s2.
3346  switch_state_sim s1 s1' →
3347  exec_step ge s1 = Value … 〈tr,s2〉 →
3348  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
3349#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
3350inversion Hsim_state
3351[ 1: (* regular state *)
3352  #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_
3353  lapply (sim_related_globals ge ge' e m Hrelated) *
3354  #Hexpr_related #Hlvalue_related
3355  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
3356  cases s in Hu_fresh Heq_env;
3357  (* Perform the intros for the statements*)
3358  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
3359  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
3360  | 14: #lab | 15: #cost #body ]
3361  #Hu_fresh #Heq_env
3362  [ 1: (* Skip *)
3363    whd in match (sw_rem ??);
3364    inversion Hsim_cont normalize nodelta
3365    [ 1: #Hk #Hk' #_ #Hexec_step
3366         @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify
3367         cases (fn_return f) in Hexec_step;
3368         [ 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
3369         | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
3370         normalize nodelta
3371         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H)
3372                %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try //
3373                normalize in Heq_env; destruct (Heq_env)
3374                %3 //
3375(*                cut (blocks_of_env e = blocks_of_env e')
3376                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
3377                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
3378                #Heq >Heq %3 // *)
3379         | *: #H destruct (H) ]
3380    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3381         whd in match (ret ??) in Heq; destruct (Heq)
3382         @(eventually_now ????) whd in match (exec_step ??);
3383         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
3384         %1 try //   
3385    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3386         @(eventually_now ????) whd in match (exec_step ??);
3387         whd in match (ret ??) in Heq; destruct (Heq)
3388         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
3389         >while_commute %1 try //
3390    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3391         @(eventually_now ????) whd in match (exec_step ??);
3392         lapply (Hexpr_related e0)
3393         cases (exec_expr ge e m e0) in Heq;
3394         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
3395         | 1: * #b #tr whd in match (m_bind ?????); #Heq
3396              *
3397              [ 2: * #error #Habsurd destruct (Habsurd)
3398              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
3399                   whd in match (bindIO ??????);
3400                   cases (exec_bool_of_val b (typeof e0)) in Heq;
3401                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3402                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
3403                        whd in match (bindIO ??????);
3404                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
3405                             @conj // >dowhile_commute %1 try //
3406                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
3407                             @conj // %1{us} try //
3408                             @(fresh_for_Sskip … Hus_fresh)
3409                        ] ] ] ]
3410    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3411         @(eventually_now ????) whd in match (exec_step ??);
3412         whd in match (ret ??) in Heq; destruct
3413         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
3414         @conj try // %1{u} try //
3415    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
3416         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
3417         destruct (Heq)
3418         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
3419         @conj try // %1
3420         [ 2: @swc_for3 //
3421         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
3422    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
3423         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
3424         destruct (Heq)
3425         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
3426         @conj try // <(for_commute ??? u uA) try // %1
3427         [ 2: assumption
3428         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
3429    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
3430         #Heq @(eventually_now ????) whd in match (exec_step ??);
3431         destruct (Heq)
3432         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
3433         %1{u} //
3434    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
3435         @(eventually_now ????) whd in match (exec_step ??);
3436         >fn_return_simplify cases (fn_return f) in Heq;
3437         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
3438         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
3439         normalize nodelta
3440         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
3441              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
3442              @conj try // %3 destruct //
3443         | *: #H destruct (H) ]     
3444     ]
3445  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
3446       whd in match (exec_step ??);
3447       cases lhs in Hu_fresh Heq; #lhs #lhs_type
3448       cases (Hlvalue_related lhs lhs_type)
3449       whd in match (exec_lvalue ge e m (Expr ??));
3450       whd in match (exec_lvalue ge' e m (Expr ??));
3451       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
3452       cases (exec_lvalue' ge e m lhs lhs_type)
3453       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
3454       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
3455            whd in match (m_bind ?????);
3456            cases (Hexpr_related rhs)
3457            [ 2: * #error #Hfail >Hfail #_
3458                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3459            | 1: cases (exec_expr ge e m rhs)
3460                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3461                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
3462                      whd in match (bindIO ??????) in ⊢ (% → % → %);
3463                      cases (opt_to_io io_out io_in ???)
3464                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3465                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3466                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
3467                           %{(State (function_switch_removal f) Sskip k' e mem)}
3468                           whd in match (bindIO ??????); @conj //
3469                           %1{u} try // @(fresh_for_Sskip … Hfresh)
3470       ] ] ] ]
3471   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
3472        whd in match (exec_step ??);
3473        cases (Hexpr_related func) in Heq;
3474        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3475        | 1: cases (exec_expr ge e m func)
3476             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3477             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
3478                  whd in match (m_bind ?????); normalize nodelta
3479                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
3480                  #Hexprlist_sim cases (Hexprlist_sim args)
3481                  [ 2: * #error #Hfail >Hfail
3482                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3483                  | 1: cases (exec_exprlist ge e m args)
3484                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3485                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
3486                            whd in match (bindIO ??????) in ⊢ (% → %);
3487                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
3488                            cases (find_funct clight_fundef ge fval)
3489                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
3490                                 whd in match (bindIO ??????) in ⊢ (% → %);
3491                                 >fundef_type_simplify
3492                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
3493                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3494                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
3495                                      cases retv normalize nodelta
3496                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
3497                                           %{(Callstate (fundef_switch_removal clfd) values
3498                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
3499                                           @conj try // %2 try // @swc_call //
3500                                      | 2: * #retval_ed #retval_type
3501                                           whd in match (exec_lvalue ge ???);
3502                                           whd in match (exec_lvalue ge' ???);                                     
3503                                           elim (Hlvalue_related retval_ed retval_type)
3504                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3505                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
3506                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
3507                                                     destruct (Habsurd)
3508                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
3509                                                     whd in match (m_bind ?????) in ⊢ (% → %);
3510                                                     #Heq destruct (Heq)
3511                                                     %{(Callstate (fundef_switch_removal clfd) values
3512                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
3513                                                               (function_switch_removal f) e k') m)}
3514                                                     @conj try //
3515                                                     %2 @swc_call //
3516                                ] ] ] ]
3517                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
3518                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3519       ] ] ] ] ]
3520   | 4: (* Ssequence *) normalize nodelta
3521        whd in match (ret ??) in ⊢ (% → ?); #Heq
3522        @(eventually_now ????)
3523        %{(State (function_switch_removal f)
3524                 (\fst (\fst (switch_removal stm1 u)))
3525                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
3526        @conj
3527        [ 2: destruct (Heq) %1
3528             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
3529             | 2: @swc_seq try // @switch_removal_fresh
3530                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
3531        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
3532             cases (switch_removal stm1 u)
3533             * #stm1' #fresh_vars #u' normalize nodelta
3534             cases (switch_removal stm2 u')
3535             * #stm2' #fresh_vars2 #u'' normalize nodelta
3536             whd in match (exec_step ??);
3537             destruct (Heq) @refl
3538        ]
3539   | 5: (* If-then-else *) normalize nodelta
3540        whd in match (ret ??) in ⊢ (% → ?); #Heq
3541        @(eventually_now ????) whd in match (sw_rem ??);
3542        whd in match (switch_removal ??);
3543        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
3544        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
3545        whd in match (exec_step ??);
3546        cases (Hexpr_related cond) in Heq;
3547        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3548        | 1: cases (exec_expr ge e m cond)
3549             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3550             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3551                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3552                  cases (exec_bool_of_val condval (typeof cond))
3553                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3554                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
3555                       destruct (Heq_condval) whd in match (bindIO ??????);
3556                       normalize nodelta
3557                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
3558                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
3559                           [ 1: >Hiftrue_eq normalize // ]
3560                           #Hrewrite >Hrewrite %1
3561                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
3562                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
3563                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
3564                           [ 1: >Hiffalse_eq // ]
3565                           #Hrewrite >Hrewrite %1 try //
3566                           cut (uA = (\snd (switch_removal iftrue u)))
3567                           [ 1: >Hiftrue_eq //
3568                           | 2: #Heq_uA >Heq_uA
3569                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
3570                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
3571       ] ] ] ] ]
3572   | 6: (* While loop *) normalize nodelta
3573        whd in match (ret ??) in ⊢ (% → ?); #Heq
3574        @(eventually_now ????) whd in match (sw_rem ??);
3575        whd in match (switch_removal ??);
3576        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
3577        whd in match (exec_step ??);
3578        cases (Hexpr_related cond) in Heq;
3579        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3580        | 1: cases (exec_expr ge e m cond)
3581             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3582             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3583                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3584                  cases (exec_bool_of_val condval (typeof cond))
3585                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3586                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
3587                       destruct (Heq_condval) whd in match (bindIO ??????);
3588                       normalize nodelta
3589                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
3590                            cut (body' = (\fst (\fst (switch_removal body u))))
3591                            [ 1: >Hbody_eq // ]
3592                            #Hrewrite >Hrewrite %1
3593                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
3594                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
3595                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
3596                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
3597        ] ] ] ]
3598   | 7: (* Dowhile loop *) normalize nodelta
3599        whd in match (ret ??) in ⊢ (% → ?); #Heq
3600        @(eventually_now ????) whd in match (sw_rem ??);
3601        whd in match (switch_removal ??);
3602        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
3603        whd in match (exec_step ??);
3604        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
3605        try //
3606        cut (body' = (\fst (\fst (switch_removal body u))))
3607        [ 1: >Hbody_eq // ]
3608        #Hrewrite >Hrewrite %1
3609        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
3610        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
3611   | 8: (* For loop *) normalize nodelta
3612        whd in match (ret ??) in ⊢ (% → ?); #Heq
3613        @(eventually_now ????) whd in match (sw_rem ??);
3614        whd in match (switch_removal ??);
3615        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
3616        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
3617              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
3618              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
3619              whd in match (exec_step ??);
3620              cases (Hexpr_related cond)
3621              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3622              | 1: cases (exec_expr ge e m cond)
3623                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3624                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3625                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3626                        cases (exec_bool_of_val condval (typeof cond))
3627                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3628                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
3629                             destruct (Heq_condval)
3630                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
3631                                  try //
3632                                  cut (body' = (\fst (\fst (switch_removal body uA))))
3633                                  [ 1: >Hbody_eq // ]
3634                                  #Hrewrite >Hrewrite
3635                                  cut (uA = (\snd (switch_removal step u)))
3636                                  [ 1: >Hstep_eq // ] #HuA
3637                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
3638                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
3639                                  [ 1: >HuA @switch_removal_fresh assumption
3640                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
3641                                       [ >Hstep_eq // ]
3642                                       #Hstep >Hstep @swc_for2 try assumption
3643                                       @for_fresh_lift try assumption ]
3644                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
3645                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
3646               ] ] ] ]
3647        | 2: #Heq
3648             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
3649             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
3650             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
3651             whd in match (exec_step ??);
3652             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
3653             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
3654             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
3655             whd in match (ret ??); destruct (Heq)
3656             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
3657             @conj try //
3658             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
3659             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
3660             <for_commute [ 2: >Hstep_eq // ]
3661             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
3662             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
3663             @swc_seq try // @for_fresh_lift
3664             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
3665             >HuA_eq @switch_removal_fresh assumption       
3666       ]
3667   | 9: (* break *) normalize nodelta
3668        inversion Hsim_cont
3669        [ 1: #Hk #Hk' #_       
3670        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
3671        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
3672        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3673        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3674        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
3675        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
3676        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
3677        normalize nodelta #H try (destruct (H))
3678        whd in match (ret ??) in H; destruct (H)
3679        @(eventually_now ????)
3680        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
3681        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
3682    | 10: (* Continue *) normalize nodelta
3683        inversion Hsim_cont
3684        [ 1: #Hk #Hk' #_       
3685        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
3686        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
3687        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3688        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3689        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
3690        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
3691        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
3692        normalize nodelta #H try (destruct (H))
3693        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
3694        destruct (H)
3695        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
3696        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
3697             >while_commute %1{u0} try assumption
3698        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
3699             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3700             | 1: * #condval #trace whd in match (m_bind ?????);
3701                  #Heq *
3702                  [ 2: * #error #Habsurd destruct (Habsurd)
3703                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
3704                       whd in match (bindIO ??????);
3705                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
3706                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3707                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
3708                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)}
3709                                 @conj try // >dowhile_commute %1{u0} assumption
3710                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
3711                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
3712             ] ] ]
3713        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
3714             try // @(fresh_for_Scontinue … Hfor_fresh)
3715        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
3716             @conj try // %1{u0}
3717             elim (substatement_fresh … Hfor_fresh) * * try //
3718             #HSskip #Hcond #Hstep #Hbody
3719             @swc_for3 assumption
3720        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
3721             %1{u} try //
3722        ]
3723    | 11: (* Sreturn *) normalize nodelta #Heq
3724          @(eventually_now ????)
3725          whd in match (exec_step ??) in Heq ⊢ %;
3726          cases retval in Heq; normalize nodelta
3727          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
3728               whd in match (ret ??) in ⊢ (% → %);
3729               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
3730               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
3731               #H destruct (H)
3732               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
3733               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
3734          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
3735               [ 1: #_ #Habsurd destruct (Habsurd)
3736               | 2: #_ elim (Hexpr_related expr)
3737                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3738                    | 1: cases (exec_expr ??? expr)
3739                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3740                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
3741                              #Hrewrite >Hrewrite
3742                              whd in match (m_bind ?????); whd in match (m_bind ?????);
3743                              #Heq destruct (Heq)
3744                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
3745                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
3746         ] ] ] ]
3747    | 12: (* Sswitch. Main proof case. *) normalize nodelta
3748          (* Case analysis on the outcome of the tested expression *)
3749          cases (exec_expr_int ge e m cond)
3750          [ 2: cases (exec_expr ge e m cond)
3751               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
3752               | 1: * #val #trace cases val
3753                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
3754                    whd in match (m_bind ?????);
3755                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
3756                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
3757          ]
3758          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
3759          whd in match (m_bind ?????); #Heq
3760          destruct (Heq)
3761          @eventually_later
3762          whd in match (sw_rem (Sswitch cond switchcases) u);
3763          whd in match (switch_removal (Sswitch cond switchcases) u);
3764          elim (switch_removal_branches_eq switchcases u)
3765          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
3766          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
3767          [ 1: >Hsrb_eq // ] #Huv1_eq
3768          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
3769          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
3770          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
3771          whd in match (simplify_switch ???);
3772          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
3773          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
3774          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)         
3775          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
3776          #Huv4_eq
3777          whd in match (exec_step ??);
3778          %{(State (function_switch_removal f)
3779                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
3780                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
3781          %{E0} @conj try @refl
3782          %{tr} normalize in match (eq ???); @conj try //
3783          (* execute the conditional *)
3784          @eventually_later
3785          (* lift the result of the previous case analysis from [ge] to [ge'] *)
3786          whd in match (exec_step ??);
3787          whd in match (exec_lvalue ????);
3788         
3789          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
3790         
3791  *)
3792 
Note: See TracBrowser for help on using the repository browser.