source: src/Clight/switchRemoval.ma @ 2227

Last change on this file since 2227 was 2227, checked in by garnier, 7 years ago
  • New version of the switch removal algorithm, described at the top of the file.
  • Memory injections (in a slightly weaker form than in Compcert, sufficient for this file) and related lemmas
  • Ongoing: proof of semantics preservation for expression evaluation under memory injections. Progressively

port old proofs to the new setting.

  • Property svn:executable set to *
File size: 148.9 KB
Line 
1 include "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(* If we succeed to load something by value from a 〈b,off〉 location,
1315   [b] is a valid block. *)
1316lemma load_by_value_success_valid_block_aux :
1317  ∀ty,m,b,off,v.
1318    access_mode ty = By_value (typ_of_type ty) →
1319    load_value_of_type ty m b off = Some ? v →
1320    Zltb (block_id b) (nextblock m) = true. (* → valid_block m b *)
1321#ty #m * #brg #bid #off #v whd in match (valid_block ??);
1322cases ty
1323[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1324| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1325whd in match (load_value_of_type ????);
1326[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
1327#Hmode
1328[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
1329     normalize in match (typesize ?);
1330     whd in match (loadn ???);
1331     whd in match (beloadv ??);
1332     cases (Zltb bid (nextblock m)) normalize nodelta
1333     try // #Habsurd destruct (Habsurd)
1334| *: normalize in Hmode; destruct (Hmode)
1335] qed.
1336
1337
1338lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
1339* #rg #id #m normalize
1340elim id /2/ qed.
1341
1342lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
1343* #rg #id #m normalize
1344elim id /2/ qed.
1345
1346lemma load_by_value_success_valid_block :
1347  ∀ty,m,b,off,v.
1348    access_mode ty = By_value (typ_of_type ty) →
1349    load_value_of_type ty m b off = Some ? v →
1350    valid_block m b.
1351#ty #m #b #off #v #Haccess_mode #Hload
1352@valid_block_from_bool
1353@(load_by_value_success_valid_block_aux ty m b off v Haccess_mode Hload)
1354qed.
1355
1356(* Making explicit the contents of memory_inj for load_value_of_type *)
1357lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
1358    memory_inj E m1 m2 →
1359    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
1360    load_value_of_type ty m1 b1 off1 = Some ? v1 →
1361    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
1362#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
1363lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
1364     normalize in Hembed;
1365     lapply (mi_inj … Hinj b1 off1)
1366     cases (E b1) in Hembed;
1367     [ 1: normalize #Habsurd destruct (Habsurd)
1368     | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ]
1369     lapply (refl ? (access_mode ty))
1370     cases ty
1371     [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1372     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1373     normalize in ⊢ ((???%) → ?); #Hmode #Hyp
1374     [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd)
1375     | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ]
1376     #Hload_success
1377     lapply (load_by_value_success_valid_block … Hmode … Hload_success)
1378     #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success)
1379qed.
1380
1381
1382(* -------------------------------------- *)
1383(* Lemmas pertaining to memory allocation *)
1384
1385(* A valid block stays valid after an alloc. *)
1386lemma alloc_valid_block_conservation :
1387  ∀m,m',z1,z2,r,new_block.
1388  alloc m z1 z2 r = 〈m', new_block〉 →
1389  ∀b. valid_block m b → valid_block m' b.
1390#m #m' #z1 #z2 #r * #b' #Hregion_eq
1391elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
1392#Halloc destruct (Halloc)
1393#b whd in match (valid_block ??) in ⊢ (% → %); /2/
1394qed.
1395
1396(* Allocating a new zone produces a valid block. *)
1397lemma alloc_valid_new_block :
1398  ∀m,m',z1,z2,r,new_block.
1399  alloc m z1 z2 r = 〈m', new_block〉 →
1400  valid_block m' new_block.
1401* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
1402whd in match (alloc ????); whd in match (valid_block ??);
1403#Halloc destruct (Halloc) /2/
1404qed.
1405
1406(* All data in a valid block is unchanged after an alloc. *)
1407lemma alloc_beloadv_conservation :
1408  ∀m,m',block,offset,z1,z2,r,new_block.
1409    valid_block m block →
1410    alloc m z1 z2 r = 〈m', new_block〉 →
1411    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
1412* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
1413whd in Halloc:(??%?); destruct (Halloc)
1414whd in match (beloadv ??) in ⊢ (??%%);
1415lapply (valid_block_to_bool … Hvalid) #Hlt
1416>Hlt >(zlt_succ … Hlt)
1417normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
1418cut (eqZb (block_id block) next = false)
1419[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
1420>Hneq cases (eq_region ??) normalize nodelta  @refl
1421qed.
1422
1423(* Lift [alloc_beloadv_conservation] to loadn *)
1424lemma alloc_loadn_conservation :
1425  ∀m,m',z1,z2,r,new_block.
1426    alloc m z1 z2 r = 〈m', new_block〉 →
1427    ∀n. ∀block,offset.
1428    valid_block m block →
1429    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
1430#m #m' #z1 #z2 #r #new_block #Halloc #n
1431elim n try //
1432#n' #Hind #block #offset #Hvalid_block
1433whd in ⊢ (??%%);
1434>(alloc_beloadv_conservation … Hvalid_block Halloc)
1435cases (beloadv m' (mk_pointer block offset)) //
1436#bev normalize nodelta
1437whd in match (shift_pointer ???); >Hind try //
1438qed.
1439
1440(* Memory allocation preserves [memory_inj] *)
1441lemma alloc_memory_inj :
1442  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1443  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1444  memory_inj E m1 m2'.
1445#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
1446%
1447[ 1:
1448  whd
1449  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1450  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
1451  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
1452  lapply (refl ? (access_mode ty))
1453  cases ty in Hload_eq;
1454  [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1455  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1456  #Hload normalize in ⊢ ((???%) → ?); #Haccess
1457  [ 1,7,8: normalize in Hload; destruct (Hload)
1458  | 2,3,4,9: whd in match (load_value_of_type ????);
1459     whd in match (load_value_of_type ????);
1460     lapply (load_by_value_success_valid_block … Haccess Hload)
1461     #Hvalid_block
1462     whd in match (load_value_of_type ????) in Hload;
1463     <(alloc_loadn_conservation … Halloc … Hvalid_block)
1464     @Hload
1465  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
1466| 2: @(mi_freeblock … Hmemory_inj)
1467| 3: #b #b' #o' #HE
1468     lapply (mi_incl … Hmemory_inj … HE)
1469     elim m2 in Halloc; #contents #nextblock #Hnextblock
1470     whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1471     whd in match (valid_block ??) in ⊢ (% → %); /2/
1472| 4: @(mi_region … Hmemory_inj)
1473| 5: @(mi_disjoint … Hmemory_inj)
1474] qed.
1475
1476(* Memory allocation induces a memory extension. *)
1477lemma alloc_memory_ext :
1478  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1479  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1480  memory_ext E m1 m2'.
1481#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
1482lapply (alloc_memory_inj … Hmemory_inj Halloc)
1483#Hinj' %
1484[ 1: @Hinj'
1485| 2: @[new_block]
1486| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
1487      #Heq destruct (Heq) whd elim m2 in Halloc;
1488      #Hcontents #nextblock #Hnextblock
1489      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1490      /2/
1491| 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload %
1492     normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ]
1493     #Heq destruct (Heq)
1494     lapply (mi_incl … Hmemory_inj … Hload)
1495     whd in ⊢ (% → ?); #Habsurd
1496     (* contradiction car ¬ (valid_block m2 new_block)  *)
1497     elim m2 in Halloc Habsurd;
1498     #contents_m2 #nextblock_m2 #Hnextblock_m2
1499     whd in ⊢ ((??%?) → ?);
1500     #Heq_alloc destruct (Heq_alloc)
1501     lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd)
1502] qed.
1503
1504lemma bestorev_beloadv_conservation :
1505  ∀mA,mB,wb,wo,v.
1506    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1507    ∀rb,ro. eq_block wb rb = false →
1508    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
1509#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
1510whd in ⊢ (??%%);
1511elim mB in Hstore; #contentsB #nextblockB #HnextblockB
1512normalize in ⊢ (% → ?);
1513cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
1514[ 2: #Habsurd destruct (Habsurd) ]
1515cases (if Zleb (low (blocks mA wb)) (offv wo) 
1516       then Zltb (offv wo) (high (blocks mA wb)) 
1517       else false) normalize nodelta
1518[ 2: #Habsurd destruct (Habsurd) ]
1519#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
1520cases rr cases wr normalize try //
1521@(eqZb_elim … rid wid)
1522[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
1523try //
1524qed.
1525
1526(* lift [bestorev_beloadv_conservation to [loadn] *)
1527lemma bestorev_loadn_conservation :
1528  ∀mA,mB,n,wb,wo,v.
1529    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1530    ∀rb,ro. eq_block wb rb = false →
1531    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
1532#mA #mB #n
1533elim n
1534[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
1535| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
1536     whd in ⊢ (??%%);
1537     >(bestorev_beloadv_conservation … Hstore … Hneq)
1538     >(Hind … Hstore … Hneq) @refl
1539] qed.
1540
1541(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
1542lemma bestorev_load_value_of_type_conservation :
1543  ∀mA,mB,wb,wo,v.
1544    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1545    ∀rb,ro. eq_block wb rb = false →
1546    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1547#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
1548cases ty
1549[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1550| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //
1551[ 1: elim sz | 2: elim fsz | 3: | 4: ]
1552whd in ⊢ (??%%);
1553>(bestorev_loadn_conservation … Hstore … Hneq) @refl
1554qed.
1555
1556(* Writing in the "extended" part of a memory preserves the underlying injection *)
1557lemma bestorev_memory_ext_to_load_sim :
1558  ∀E,mA,mB,mC.
1559  ∀Hext:memory_ext E mA mB.
1560  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1561  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1562  load_sim E mA mC.
1563#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
1564#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1565(* Show that (wb ≠ b2) *)
1566lapply (me_writeable_ok … Hext … Hvalid Hembed) #Hb2
1567lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
1568cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
1569<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
1570@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
1571qed.
1572
1573(* Writing in the "extended" part of a memory preserves the whole memory injection *)
1574lemma bestorev_memory_ext_to_memory_inj :
1575  ∀E,mA,mB,mC.
1576  ∀Hext:memory_ext E mA mB.
1577  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1578  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1579  memory_inj E mA mC.
1580#E #mA * #contentsB #nextblockB #HnextblockB #mC
1581#Hext #wb #wo #v #Hwb #Hstore
1582%
1583[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
1584elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
1585#Hmem
1586[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj
1587whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
1588normalize in ⊢ (% → ?); #Hlt_wb
1589>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
1590cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
1591normalize nodelta
1592[ 2: #Habsurd destruct (Habsurd) ]
1593#Heq destruct (Heq)
1594#b #b' #o' #Hembed @(Hcodomain … Hembed)
1595qed.
1596
1597(* It even preserves memory extensions, with the same writeable blocks.  *)
1598lemma bestorev_memory_ext_to_memory_ext :
1599  ∀E,mA,mB.
1600  ∀Hext:memory_ext E mA mB.
1601  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1602  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
1603  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
1604#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
1605%{(mk_memory_ext …
1606      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
1607      (me_writeable … Hext)
1608      ?
1609      (me_writeable_ok … Hext)
1610 )} try @refl
1611#b #Hmemb
1612lapply (me_writeable_valid … Hext b Hmemb)
1613lapply (me_writeable_valid … Hext wb Hmem)
1614elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
1615lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
1616>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
1617cases (if Zleb (low (contentsB wb)) (offv wo) 
1618       then Zltb (offv wo) (high (contentsB wb)) 
1619       else false)
1620normalize [ 2: #Habsurd destruct (Habsurd) ]
1621#Heq destruct (Heq) @Hb_valid
1622qed.
1623
1624(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
1625lemma storen_memory_ext_to_memory_ext :
1626  ∀E,mA,l,mB,mC.
1627  ∀Hext:memory_ext E mA mB.
1628  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1629  storen mB (mk_pointer wb wo) l = Some ? mC →
1630  memory_ext E mA mC.
1631#E #mA #l elim l
1632[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
1633     @Hext
1634| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
1635     whd in ⊢ ((??%?) → ?);
1636     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
1637     cases (bestorev mB (mk_pointer wb wo) hd)
1638     normalize nodelta
1639     [ 1: #H #Habsurd destruct (Habsurd) ]
1640     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
1641     @(Hind … HextD … Hstore)
1642     <Heq @Hmem
1643] qed.     
1644
1645(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
1646lemma store_value_of_type_memory_ext_to_memory_ext :
1647  ∀E,mA,mB,mC.
1648  ∀Hext:memory_ext E mA mB.
1649  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1650  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
1651  memory_ext E mA mC.
1652#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
1653cases ty
1654[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1655| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1656whd in ⊢ ((??%?) → ?);
1657[ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
1658#Hstore
1659@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
1660qed.
1661
1662(* End of the memory injection-related stuff. *)
1663(* ------------------------------------------ *)
1664
1665(* Lookup functions in list environments (used to type local variables in functions) *)     
1666let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
1667match l with
1668[ nil ⇒ false
1669| cons hd tl ⇒
1670  let 〈id, ty〉 ≝ hd in
1671  match identifier_eq SymbolTag i id with
1672  [ inl Hid_eq ⇒ true
1673  | inr Hid_neq ⇒ mem_assoc_env i tl 
1674  ]
1675].
1676
1677let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝
1678match l with
1679[ nil ⇒ None ?
1680| cons hd tl ⇒
1681  let 〈id, ty〉 ≝ hd in
1682  match identifier_eq SymbolTag i id with
1683  [ inl Hid_eq ⇒ Some ? ty
1684  | inr Hid_neq ⇒ assoc_env i tl 
1685  ]
1686].
1687
1688(* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension
1689   of the environment [e1] s.t. the new binders are in [new], and such that those
1690   new binders are "writeable" in the memory extension [Hext] *)
1691definition disjoint_extension ≝
1692λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem).
1693λ(new : list (ident × type)). λ(E:embedding). λ(Hext: memory_ext E m1 m2).
1694  ∀id. match mem_assoc_env id new with
1695       [ true ⇒
1696           ∃b. lookup ?? e2 id = Some ? b
1697            ∧ meml ? b (me_writeable … Hext)
1698            ∧ lookup ?? e1 id = None ?
1699       | false ⇒
1700         match lookup ?? e1 id with
1701         [ None ⇒ lookup ?? e2 id = None ?
1702         | Some b1 ⇒
1703           match lookup ?? e2 id with
1704           [ None ⇒ False
1705           | Some b2 ⇒
1706             valid_block m1 b1 ∧
1707             value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))
1708           ]
1709         ]
1710       ].
1711
1712(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
1713 * the variable is not in a local environment, then we search into the global one.
1714 * A proper "extension" of a local environment should be such that the extension
1715 * does not collide with a given global env.
1716 * To see the details of why we need that, see [exec_lvalue'], Evar id case.
1717 *)
1718definition ext_fresh_for_genv ≝
1719λ(ext : list (ident × type)). λ(ge : genv).
1720  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.
1721
1722(* Any environment is a "disjoint" extension of itself with nothing. *)
1723(*
1724lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].
1725#e #m #ty #id
1726normalize in match (mem_assoc_env id []); normalize nodelta
1727cases (lookup ?? e id) try //
1728#b normalize nodelta
1729% #ty cases (load_value_of_type ????)
1730[ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj //
1731cases (assoc_env id ty) //
1732qed. *)
1733
1734
1735(* "generic" simulation relation on [res ?] *)
1736definition res_sim ≝
1737  λ(A : Type[0]).
1738  λ(eq : A → A → Prop).
1739  λ(r1, r2 : res A).
1740  ∀a1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2.
1741
1742(* Specialisation of [res_sim] to match [exec_expr] *)
1743definition exec_expr_sim ≝ λE.
1744  res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)).
1745
1746(* Specialisation of [res_sim] to match [exec_lvalue] *)
1747definition exec_lvalue_sim ≝ λE.
1748  res_sim (block × offset × trace)
1749    (λr1,r2.
1750      let 〈b1,o1,tr1〉 ≝ r1 in
1751      let 〈b2,o2,tr2〉 ≝ r2 in
1752      value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2).
1753
1754lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r.
1755#ty #m #b #o cases (load_value_of_type ty m b o)
1756[ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed.
1757
1758(*
1759lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'.
1760   env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
1761   〈f',vars〉 = function_switch_removal f →
1762   env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
1763   environment_extension env env' vars.
1764
1765#f #f'
1766cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append
1767cases (fn_params f) cases (fn_vars f)
1768[ 1: #vars >append_nil >append_nil >nil_append elim vars   
1769   [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct //
1770   | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq
1771        whd in ⊢ ((???(???%)) → ?);
1772 #Henv #Hswrem #Henv'
1773#id   
1774*)
1775
1776(*
1777lemma substatement_fresh : ∀s,u.
1778    fresh_for_statement s u →
1779    substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
1780#s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s)
1781try /by I/
1782[ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption
1783| 2: *
1784    [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
1785         #Hfresh_e #Hfresh_args @conj try assumption
1786         normalize nodelta in Hfresh_args;
1787         >max_id_commutative in Hfresh_args; >max_id_one_neutral
1788         #Hfresh_args         
1789    | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
1790         #Hfresh_e #H lapply (fresh_max_split ??? H) *
1791         #Hfresh_ret #Hfresh_args @conj try @conj try assumption ]
1792    elim args in Hfresh_args;
1793    [ 1,3: //
1794    | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???);
1795            >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj
1796            [ 1,3: @Hu
1797            | 2,4: @Hind assumption ] ]
1798| 3: #s1 #s2 #_ #_
1799     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
1800     whd in match (substatement_P ??); /2/
1801| 4: #e #cond #iftrue #iffalse #_
1802     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
1803     #Hexpr #H2 lapply (fresh_max_split … H2) * /2/
1804| 5,6: #e #stm #_
1805     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/
1806| 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) *
1807      #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond
1808      elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/
1809| 8: #ret #H whd elim ret in H; try //     
1810| 9: #expr #ls #Hind #H whd @conj
1811     [ 1: elim (fresh_max_split … H) //
1812     | 2: @Hind elim (fresh_max_split … H) // ]
1813| 10: #l #body #Hind #H whd elim (fresh_max_split … H) //
1814| 11: #sz #i #hd #tl #Hhd #Htl #H whd
1815     elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj //
1816     @Htl //
1817] qed.
1818*)
1819
1820(* Eliminating switches introduces fresh variables. [environment_extension] characterizes
1821 * a local environment extended by some local variables. *)
1822 
1823
1824(* lookup on environment extension *)
1825(*
1826lemma extension_lookup :
1827  ∀map, map', ext, id, result.
1828  environment_extension map map' ext →
1829  lookup ?? map id = Some ? result →
1830  lookup ?? map' id = Some ? result.
1831#map #map' #ext #id #result #Hext lapply (Hext id)
1832cases (mem_assoc_env ??) normalize nodelta
1833[ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd)
1834| 2: #H >H // ] qed.
1835
1836*)
1837
1838(* Extending a map by an empty list of variables yields an observationally equivalent
1839 * environment. *)
1840(*
1841lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'.
1842* #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H
1843[ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
1844     cases (lookup_opt block id map2) normalize
1845     [ 1: >H #H2 >H2 @refl
1846     | 2: #b >H cases v
1847          [ 1: normalize * #H @(False_ind … H)
1848          | 2: #block normalize // ] ]
1849| 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
1850     >H cases v normalize try //
1851     #block cases (lookup_opt ? id map1) normalize try //
1852     * #H @(False_ind … H)
1853] qed. *)
1854
1855(* If two identifier maps are observationally equal, then they contain the same bocks.
1856 * see maps_obsequiv.ma for the details of the proof. *)
1857(*
1858lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'.
1859* #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold
1860>Hfold @refl
1861qed.
1862*)
1863
1864(* Simulation relations. *)
1865inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
1866| swc_stop : ∀fvs.
1867    switch_cont_sim fvs Kstop Kstop
1868| swc_seq : ∀fvs,s,k,k',u,result.
1869    fresh_for_statement s u →
1870    switch_cont_sim fvs k k' →
1871    switch_removal s fvs u = Some ? result →
1872    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
1873| swc_while : ∀fvs,e,s,k,k',u,result.
1874    fresh_for_statement (Swhile e s) u →
1875    switch_cont_sim fvs k k' →
1876    switch_removal s fvs u = Some ? result →
1877    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
1878| swc_dowhile : ∀fvs,e,s,k,k',u,result.
1879    fresh_for_statement (Sdowhile e s) u →
1880    switch_cont_sim fvs k k' →
1881    switch_removal s fvs u = Some ? result →
1882    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
1883| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
1884    fresh_for_statement (Sfor Sskip e s1 s2) u →
1885    switch_cont_sim fvs k k' →
1886    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
1887    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
1888| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1889    fresh_for_statement (Sfor Sskip e s1 s2) u →
1890    switch_cont_sim fvs k k' →
1891    switch_removal s1 fvs u = Some ? result1 →
1892    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
1893    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
1894| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1895    fresh_for_statement (Sfor Sskip e s1 s2) u →
1896    switch_cont_sim fvs k k' →
1897    switch_removal s1 fvs u = Some ? result1 →
1898    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
1899    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
1900| swc_switch : ∀fvs,k,k'.
1901    switch_cont_sim fvs k k' →
1902    switch_cont_sim fvs (Kswitch k) (Kswitch k')
1903| swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
1904    switch_cont_sim fvs k k' →
1905    (* /!\ Update [en] with [fvs'] ... *)
1906    switch_cont_sim
1907      (map … (fst ??) (\snd (function_switch_removal f)))
1908      (Kcall r f en k)
1909      (Kcall r (\fst (function_switch_removal f)) en' k').
1910
1911
1912(*
1913 en' = exec_alloc_variables en m (\snd (function_switch_removal f))
1914 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
1915        variable dans en'.
1916
1917        1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que
1918           dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
1919           de savoir que :
1920           si je lookup une variable générée à partir d'un univers frais dans l'environement en',
1921           alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
1922           et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
1923           et à etre "(function_switch_removal f)-contained".
1924
1925        2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
1926           et l'update n'altèrent pas le comportement du reste du programme.
1927
1928        relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
1929                   depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
1930                   en particulier, si u est frais pour S1 u est frais pour S0.
1931
1932        Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
1933                    "environment_extension en en' (\fst (\fst (switch_removal s u)))"
1934                   
1935 ---------------------------------------------------------------
1936 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
1937   et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
1938   on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
1939   en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
1940*)
1941
1942inductive switch_state_sim : state → state → Prop ≝
1943| sws_state : ∀u,f,s,k,k',m,m',result.
1944    ∀env, env', f', vars.
1945    ∀E:embedding.   
1946    ∀Hext:memory_ext E m m'.
1947    fresh_for_statement s u →
1948    (*
1949    env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
1950    env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
1951    *)
1952    〈f',vars〉 = function_switch_removal f →
1953    disjoint_extension env m env' m' vars E Hext →
1954    switch_removal s (map ?? (fst ??) vars) u = Some ? result →
1955    switch_cont_sim (map ?? (fst ??) vars) k k' →
1956    switch_state_sim
1957      (State f s k env m)
1958      (State f' (ret_st ? result) k' env' m')
1959| sws_callstate : ∀vars, fd,args,k,k',m.
1960    switch_cont_sim vars k k' →
1961    switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m)
1962| sws_returnstate : ∀vars,res,k,k',m.
1963    switch_cont_sim vars k k' →
1964    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
1965| sws_finalstate : ∀r.
1966    switch_state_sim (Finalstate r) (Finalstate r).
1967
1968lemma call_cont_swremoval : ∀fv,k,k'.
1969  switch_cont_sim fv k k' →
1970  switch_cont_sim fv (call_cont k) (call_cont k').
1971#fv #k0 #k0' #K elim K /2/
1972qed.
1973
1974(* [eventually ge P s tr] states that after a finite number of [exec_step], the
1975   property P on states will be verified. *)
1976inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
1977| eventually_base : ∀s,t,s'.
1978    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
1979    P s' →
1980    eventually ge P s t
1981| eventually_step : ∀s,t,s',t',trace.
1982    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
1983    eventually ge P s' t' →
1984    trace = (t ⧺ t') →
1985    eventually ge P s trace.
1986
1987(* [eventually] is not so nice to use directly, we would like to make the mandatory
1988 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
1989   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
1990lemma eventually_now : ∀ge,P,s,t.
1991  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
1992   eventually ge P s t.
1993#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
1994qed.
1995(*   
1996lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
1997                                      ∃t'.eventually ge P s (t ⧺ t').
1998#ge #P #s #t * #s' * #Hexec #HP %{E0} normalize >(append_nil ? t) %1{????? Hexec HP}
1999qed.
2000*)
2001lemma eventually_later : ∀ge,P,s,t.
2002   (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) →
2003    eventually ge P s t.
2004#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
2005try assumption
2006qed.
2007
2008(* lift value_eq to option block *)
2009definition option_block_eq ≝ λE,ob1,ob2.
2010match ob1 with
2011[ None ⇒
2012  match ob2 with
2013  [ None ⇒ True
2014  | Some _ ⇒ False ]
2015| Some b1 ⇒
2016  match ob2 with
2017  [ None ⇒ False
2018  | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))  ]
2019].
2020
2021definition value_eq_opt ≝ λE,ov1,ov2.
2022match ov1 with
2023[ None ⇒
2024  match ov2 with
2025  [ None ⇒ True
2026  | Some _ ⇒ False ]
2027| Some v1 ⇒
2028  match ov2 with
2029  [ None ⇒ False
2030  | Some v2 ⇒
2031    value_eq E v1 v2 ]
2032].
2033
2034record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
2035  rg_find_symbol: ∀s.
2036    option_block_eq E (find_symbol ? ge s) (find_symbol ? ge' s);
2037  rg_find_funct: ∀v,f.
2038    find_funct ? ge v = Some ? f →
2039    find_funct ? ge' v = Some ? (t f);
2040  rg_find_funct_ptr: ∀b,f.
2041    find_funct_ptr ? ge b = Some ? f →
2042    find_funct_ptr ? ge' b = Some ? (t f)
2043}.
2044
2045lemma exec_lvalue_expr_elim :
2046  ∀E,r1,r2,Pok,Qok.
2047  ∀H:exec_lvalue_sim E r1 r2.
2048  (∀bo1,bo2,tr.
2049    let 〈b1,o1〉 ≝ bo1 in
2050    let 〈b2,o2〉 ≝ bo2 in
2051    value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) →
2052    match Pok 〈bo1,tr〉 with
2053    [ Error err ⇒ True
2054    | OK vt1 ⇒
2055      let 〈val1,trace1〉 ≝ vt1 in
2056      match Qok 〈bo2,tr〉 with
2057      [ Error err ⇒ False
2058      | OK vt2 ⇒
2059        let 〈val2,trace2〉 ≝ vt2 in
2060        trace1 = trace2 ∧ value_eq E val1 val2     
2061      ]
2062    ]) →
2063  exec_expr_sim E
2064    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
2065    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
2066#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
2067elim r1
2068[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
2069| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
2070     * #a2 * #Hr2 >Hr2 normalize nodelta
2071     elim a1 * #b1 #o1 #tr1
2072     elim a2 * #b2 #o2 #tr2 normalize nodelta
2073     * #Hvalue_eq #Htrace_eq #H2
2074     destruct (Htrace_eq)
2075     lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq)
2076     cases (Pok 〈b1, o1, tr2〉)
2077     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
2078     | 1: * #v1 #tr1' normalize nodelta #H3 whd
2079          * #v1' #tr1'' #Heq destruct (Heq)
2080          cases (Qok 〈b2,o2,tr2〉) in H3;
2081          [ 2: #error #Hfalse @(False_ind … Hfalse)
2082          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
2083               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
2084] ] ] qed.
2085
2086lemma exec_expr_expr_elim :
2087  ∀E,r1,r2,Pok,Qok.
2088  ∀H:exec_expr_sim E r1 r2.
2089  (∀v1,v2,trace.
2090    value_eq E v1 v2 →
2091    match Pok 〈v1,trace〉 with
2092    [ Error err ⇒ True
2093    | OK vt1 ⇒
2094      let 〈val1,trace1〉 ≝ vt1 in
2095      match Qok 〈v2,trace〉 with
2096      [ Error err ⇒ False
2097      | OK vt2 ⇒
2098        let 〈val2,trace2〉 ≝ vt2 in
2099        trace1 = trace2 ∧ value_eq E val1 val2     
2100      ]
2101    ]) →
2102  exec_expr_sim E
2103    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
2104    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
2105#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
2106elim r1
2107[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
2108| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
2109     * #a2 * #Hr2 >Hr2 normalize nodelta
2110     elim a1 #v1 #tr1
2111     elim a2 #v2 #tr2 normalize nodelta
2112     * #Hvalue_eq #Htrace_eq #H2
2113     destruct (Htrace_eq)
2114     lapply (H2 v1 v2 tr2 Hvalue_eq)
2115     cases (Pok 〈v1, tr2〉)
2116     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
2117     | 1: * #v1 #tr1' normalize nodelta #H3 whd
2118          * #v1' #tr1'' #Heq destruct (Heq)
2119          cases (Qok 〈v2,tr2〉) in H3;
2120          [ 2: #error #Hfalse @(False_ind … Hfalse)
2121          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
2122               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
2123] ] ] qed.
2124
2125(* Commutation results of standard binary operations with value_eq. *)
2126lemma unary_operation_value_eq :
2127  ∀E,op,v1,v2,ty.
2128   value_eq E v1 v2 →
2129   ∀r1.
2130   sem_unary_operation op v1 ty = Some ? r1 →
2131    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
2132#E #op #v1 #v2 #ty #Hvalue_eq #r1
2133inversion Hvalue_eq
2134[ 1: #v #Hv1 #Hv2 #_ destruct
2135     cases op normalize
2136     [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2137          normalize #Habsurd destruct (Habsurd)
2138     | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2139          normalize #Habsurd destruct (Habsurd)
2140     | 2: #Habsurd destruct (Habsurd) ]
2141| 2: #vsz #i #Hv1 #Hv2 #_
2142     cases op
2143     [ 1: cases ty
2144          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2145          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
2146          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2147               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
2148               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
2149               //
2150          | *: #Habsurd destruct (Habsurd) ]
2151     | 2: whd in match (sem_unary_operation ???);     
2152          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
2153     | 3: whd in match (sem_unary_operation ???);
2154          cases ty
2155          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2156          normalize nodelta
2157          whd in ⊢ ((??%?) → ?);
2158          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2159               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
2160          | *: #Habsurd destruct (Habsurd) ] ]
2161| 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2162     cases op normalize nodelta
2163     [ 1: cases ty
2164          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2165          whd in match (sem_notbool ??);
2166          #Heq1 destruct
2167          cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
2168     | 2: normalize #Habsurd destruct (Habsurd)
2169     | 3: cases ty
2170          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2171          whd in match (sem_neg ??);
2172          #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
2173| 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2174     cases op normalize nodelta
2175     [ 1: cases ty
2176          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2177          whd in match (sem_notbool ??);
2178          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2179     | 2: normalize #Habsurd destruct (Habsurd)
2180     | 3: cases ty
2181          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2182          whd in match (sem_neg ??);
2183          #Heq1 destruct ]
2184| 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
2185     cases op normalize nodelta
2186     [ 1: cases ty
2187          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2188          whd in match (sem_notbool ??);         
2189          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2190     | 2: normalize #Habsurd destruct (Habsurd)
2191     | 3: cases ty
2192          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2193          whd in match (sem_neg ??);         
2194          #Heq1 destruct ]
2195]
2196qed.
2197
2198(* A cleaner version of inversion for [value_eq] *)
2199lemma value_eq_inversion :
2200  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
2201  (∀v. P Vundef v) →
2202  (∀sz,i. P (Vint sz i) (Vint sz i)) →
2203  (∀f. P (Vfloat f) (Vfloat f)) →
2204  (P Vnull Vnull) →
2205  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
2206  P v1 v2.
2207#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
2208inversion Heq
2209[ 1: #v #Hv1 #Hv2 #_ destruct @H1
2210| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
2211| 3: #f #Hv1 #Hv2 #_ destruct @H3
2212| 4: #Hv1 #Hv2 #_ destruct @H4
2213| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
2214
2215(* value_eq lifts to addition *)
2216lemma add_value_eq :
2217  ∀E,v1,v2,v1',v2',ty1,ty2,m1,m2.
2218   value_eq E v1 v2 →
2219   value_eq E v1' v2' →
2220   memory_inj E m1 m2 → (* This injection seems useless TODO *)
2221   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
2222           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2223#E #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
2224@(value_eq_inversion E … Hvalue_eq1)
2225[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2226[ 1: whd in match (sem_add ????); normalize nodelta
2227     cases (classify_add ty1 ty2) normalize nodelta
2228     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
2229     #Habsurd destruct (Habsurd)
2230| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2231     cases (classify_add ty1 ty2) normalize nodelta     
2232     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2233     [ 2,3,5: #Habsurd destruct (Habsurd) ]
2234     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2235     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2236     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
2237     [ 1: @intsize_eq_elim_elim
2238          [ 1: #_ #Habsurd destruct (Habsurd)
2239          | 2: #Heq destruct (Heq) normalize nodelta
2240               #Heq destruct (Heq)
2241               /3 by ex_intro, conj, vint_eq/ ]
2242     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
2243          /3 by ex_intro, conj, vint_eq/
2244     | 3: #Heq destruct (Heq)
2245          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
2246          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
2247          @vptr_eq whd in match (pointer_translation ??);
2248          cases (E b1') in Hembed;
2249          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2250          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2251               whd in match (shift_pointer_n ????);
2252               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
2253                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i))
2254               [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ]
2255               #Heq >Heq @refl ]
2256     ]
2257| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2258     cases (classify_add ty1 ty2) normalize nodelta     
2259     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2260     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2261     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2262     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2263     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2264     #Heq destruct (Heq)
2265     /3 by ex_intro, conj, vfloat_eq/
2266| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2267     cases (classify_add ty1 ty2) normalize nodelta     
2268     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2269     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2270     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2271     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2272     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2273     @eq_bv_elim
2274     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2275     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2276| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2277     cases (classify_add ty1 ty2) normalize nodelta
2278     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2279     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2280     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2281     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2282     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2283     #Heq destruct (Heq)
2284     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
2285     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2286     elim p1 in Hembed; #b1 #o1 normalize nodelta
2287     cases (E b1)
2288     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2289     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2290          normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
2291          @refl
2292     ]
2293] qed.
2294         
2295(* TODO all other 10 binary operations. Then wrap this in [binary_operation_value_eq] *)
2296
2297
2298(* Commutation result for binary operators. *)
2299lemma binary_operation_value_eq :
2300  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
2301   value_eq E v1 v2 →
2302   value_eq E v1' v2' →
2303   memory_inj E m1 m2 →
2304   ∀r1.
2305   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
2306   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
2307#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
2308cases op
2309whd in match (sem_binary_operation ??????);
2310whd in match (sem_binary_operation ??????);
2311@cthulhu
2312qed.
2313
2314 
2315(* Simulation relation on expressions *)
2316lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
2317  ∀E:embedding.
2318  ∀Hext:memory_ext E m1 m2.
2319  switch_removal_globals E ? fundef_switch_removal ge ge' →
2320  disjoint_extension en1 m1 en2 m2 ext E Hext →
2321  ext_fresh_for_genv ext ge →
2322  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
2323  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
2324#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
2325@expr_lvalue_ind_combined
2326[ 1: #csz #cty #i #a1
2327     whd in match (exec_expr ????); elim cty
2328     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2329     normalize nodelta
2330     [ 2: cases (eq_intsize csz sz) normalize nodelta
2331          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
2332          | 2: #Habsurd destruct (Habsurd) ]
2333     | 4,5,6: #_ #H destruct (H)
2334     | *: #H destruct (H) ]
2335| 2: #ty #fl #a1
2336     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
2337| 3: *
2338  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
2339  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
2340  #ty whd in ⊢ (% → ?); #Hind try @I
2341  whd in match (Plvalue ???);
2342  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
2343       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
2344       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2345       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
2346           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
2347           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
2348           whd in match (load_value_of_type' ???);
2349           whd in match (load_value_of_type' ???);
2350           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
2351           cases (load_value_of_type ty m1 bl1 o1)
2352           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2353           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
2354                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
2355                    normalize /4 by ex_intro, conj/
2356  ] ] ]
2357| 4: #v #ty whd * * #b1 #o1 #tr1
2358     whd in match (exec_lvalue' ?????);
2359     whd in match (exec_lvalue' ?????);
2360     lapply (Hdisjoint v)
2361     lapply (Hext_fresh_for_genv v)
2362     cases (mem_assoc_env v ext) #Hglobal
2363     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
2364          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
2365          >(Hglobal (refl ??)) normalize
2366          #Habsurd destruct (Habsurd)
2367     | 2: normalize nodelta
2368          cases (lookup ?? en1 v) normalize nodelta
2369          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
2370               lapply (rg_find_symbol … Hrelated v)
2371               cases (find_symbol ???) normalize
2372               [ 1: #_ #Habsurd destruct (Habsurd)
2373               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
2374                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
2375                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
2376                         %{〈block',mk_offset OZ,[]〉} @conj try @refl
2377                         normalize /2/
2378                ] ]
2379         | 2: #block
2380              cases (lookup ?? en2 v) normalize nodelta
2381              [ 1: #Hfalse @(False_ind … Hfalse)
2382              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
2383                   %{〈b, zero_offset, E0〉} @conj try @refl
2384                   normalize /2/
2385    ] ] ]
2386| 5: #e #ty whd in ⊢ (% → %);
2387     whd in match (exec_lvalue' ?????);
2388     whd in match (exec_lvalue' ?????);
2389     cases (exec_expr ge en1 m1 e)
2390     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
2391          * elim v1 normalize nodelta
2392          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
2393          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
2394          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
2395          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
2396          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
2397               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
2398               #Hvalue_eq normalize
2399               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2400               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
2401               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
2402               %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
2403               normalize @conj // ]
2404     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
2405| 6: #ty #e #ty'
2406     #Hsim @(exec_lvalue_expr_elim … Hsim)
2407     cases ty
2408     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2409     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
2410     #tr #H @conj try @refl try assumption
2411| 7: #ty #op #e
2412     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
2413     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
2414     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
2415     [ 1: #_ @I
2416     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
2417           normalize /2/ ]
2418| *: @cthulhu ] qed.
2419
2420(* TODO: Old cases, to be ported to memory injection.
2421| 8: #ty #op #e1 #e2 #Hind1 #Hind2
2422     whd in match (exec_expr ge ???);   
2423     whd in match (exec_expr ge' ???);
2424     @(exec_expr_expr_elim … Hind1)
2425     cases (exec_expr ge en1 m1 e2) in Hind2;
2426     [ 2: #error normalize //
2427     | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 *
2428          #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq'
2429          >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????);
2430
2431
2432| 9: #ty #castty #e #Hind
2433     whd in match (exec_expr ge ???);   
2434     whd in match (exec_expr ge' ???);
2435     cases Hind
2436     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2437     | 1: cases (exec_expr ge en m e)
2438          [ 2: #error #_ @SimFail /2 by ex_intro/
2439          | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
2440          ]
2441     ]
2442| 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3
2443     whd in match (exec_expr ge ???);   
2444     whd in match (exec_expr ge' ???);
2445     cases Hind1
2446     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2447     | 1: cases (exec_expr ge en m e1)
2448          [ 2: #error #_ @SimFail /2 by ex_intro/
2449          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
2450               normalize nodelta
2451               cases (exec_bool_of_val ??)
2452               [ 2: #error @SimFail /2 by ex_intro/
2453               | 1: * whd in match (m_bind ?????); normalize nodelta
2454                    [ 1: cases Hind2
2455                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2456                         | 1: cases (exec_expr ge en m e2)
2457                              [ 2: #error #_  @SimFail /2 by ex_intro/
2458                              | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))                                   
2459                                   @SimOk normalize nodelta #a2
2460                                   whd in match (m_bind ?????); // ]
2461                         ]
2462                    | 2: cases Hind3
2463                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2464                         | 1: cases (exec_expr ge en m e3)
2465                              [ 2: #error #_  @SimFail /2 by ex_intro/
2466                              | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3)))
2467                                   @SimOk normalize nodelta #a3
2468                                   whd in match (m_bind ?????); // ]
2469                         ]
2470     ] ] ] ]                     
2471| 11: #ty #e1 #e2 #Hind1 #Hind2
2472     whd in match (exec_expr ge ???);   
2473     whd in match (exec_expr ge' ???);
2474     cases Hind1
2475     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2476     | 1: cases (exec_expr ge en m e1)
2477          [ 2: #error #_ @SimFail /2 by ex_intro/
2478          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
2479               normalize nodelta
2480               cases (exec_bool_of_val ??)
2481               [ 2: #error @SimFail /2 by ex_intro/
2482               | 1: * whd in match (m_bind ?????);
2483                    [ 2: @SimOk // ]
2484                    cases Hind2
2485                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2486                    | 1: cases (exec_expr ge en m e2)
2487                         [ 2: #error #_  @SimFail /2 by ex_intro/
2488                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
2489                              @SimOk #a2
2490                              whd in match (m_bind ?????); //
2491     ] ] ] ] ]
2492| 12: #ty #e1 #e2 #Hind1 #Hind2
2493     whd in match (exec_expr ge ???);   
2494     whd in match (exec_expr ge' ???);
2495     cases Hind1
2496     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2497     | 1: cases (exec_expr ge en m e1)
2498          [ 2: #error #_ @SimFail /2 by ex_intro/
2499          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
2500               normalize nodelta
2501               cases (exec_bool_of_val ??)
2502               [ 2: #error @SimFail /2 by ex_intro/
2503               | 1: * whd in match (m_bind ?????);
2504                    [ 1: @SimOk // ]
2505                    cases Hind2
2506                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2507                    | 1: cases (exec_expr ge en m e2)
2508                         [ 2: #error #_  @SimFail /2 by ex_intro/
2509                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
2510                              @SimOk #a2
2511                              whd in match (m_bind ?????); //
2512     ] ] ] ] ]
2513| 13: #ty #sizeof_ty
2514     whd in match (exec_expr ge ???);   
2515     whd in match (exec_expr ge' ???);
2516     @SimOk //
2517| 14: #ty #e #ty' #fld #Hind
2518     whd in match (exec_lvalue' ge ????);
2519     whd in match (exec_lvalue' ge' ????);
2520     whd in match (typeof ?);
2521     cases ty' in Hind;
2522     [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
2523     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
2524     normalize nodelta #Hind
2525     try (@SimFail /2 by ex_intro/)
2526     whd in match (exec_lvalue ????);
2527     whd in match (exec_lvalue ????);     
2528     cases Hind
2529     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2530     | 1,3: cases (exec_lvalue' ge en m e ?)
2531         [ 2,4: #error #_ @SimFail /2 by ex_intro/
2532         | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
2533     ] ]
2534| 15: #ty #l #e #Hind
2535     whd in match (exec_expr ge ???);
2536     whd in match (exec_expr ge' ???);
2537     cases Hind
2538     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2539     | 1: cases (exec_expr ge en m e)
2540        [ 2: #error #_ @SimFail /2 by ex_intro/
2541        | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
2542     ] ]
2543| 16: *
2544  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
2545  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
2546  #ty normalize in ⊢ (% → ?);
2547  [ 1,2: #_ @SimOk #a normalize //
2548  | 3,4,13: #H @(False_ind … H)
2549  | *: #_ @SimFail /2 by ex_intro/
2550  ]
2551] qed. *)
2552
2553(*
2554lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
2555related_globals ? fundef_switch_removal ge ge' →
2556∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
2557#ge #ge' #en #m #Hrelated #args
2558elim args
2559[ 1: /3/
2560| 2: #hd #tl #Hind normalize
2561     elim (sim_related_globals ge ge' en m Hrelated)
2562     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
2563     cases (exec_expr ge en m hd)
2564     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
2565     | 1: * #val_hd #trace_hd normalize nodelta
2566          cases Hind
2567          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
2568          | 1: cases (exec_exprlist ge en m tl)
2569               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
2570               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
2571                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
2572                    cases Hexec_hd
2573                    [ 2: * #error #Habsurd destruct (Habsurd)
2574                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
2575] ] ] ] qed.
2576*)
2577
2578(* The return type of any function is invariant under switch removal *)
2579lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
2580#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
2581qed.
2582
2583(* Similar stuff for fundefs *)
2584lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
2585* // qed.
2586
2587(*
2588lemma expr_fresh_lift :
2589  ∀e,u,id.
2590      fresh_for_expression e u →
2591      fresh_for_univ SymbolTag id u →
2592      fresh_for_univ SymbolTag (max_of_expr e id) u.
2593#e #u #id
2594normalize in match (fresh_for_expression e u);
2595#H1 #H2
2596>max_of_expr_rewrite
2597normalize in match (fresh_for_univ ???);
2598cases (max_of_expr e ?) in H1; #p #H1
2599cases id in H2; #p' #H2
2600normalize nodelta
2601cases (leb p p') normalize nodelta
2602[ 1: @H2 | 2: @H1 ]
2603qed. *)
2604
2605lemma while_fresh_lift : ∀e,s,u.
2606   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
2607#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
2608cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
2609cases (leb e s) try /2/
2610qed.
2611
2612(*
2613lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
2614#e0 #s0 #us0 normalize
2615cases (switch_removal s0 us0) * #body #newvars #u' normalize //
2616qed.*)
2617
2618lemma dowhile_fresh_lift : ∀e,s,u.
2619   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
2620#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
2621cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
2622cases (leb e s) try /2/
2623qed.
2624(*
2625lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
2626#e0 #s0 #us0 normalize
2627cases (switch_removal s0 us0) * #body #newvars #u' normalize //
2628qed.*)
2629
2630lemma for_fresh_lift : ∀cond,step,body,u.
2631  fresh_for_statement step u →
2632  fresh_for_statement body u →
2633  fresh_for_expression cond u →
2634  fresh_for_statement (Sfor Sskip cond step body) u.
2635#cond #step #body #u
2636whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
2637cases (max_of_statement step) #s
2638cases (max_of_statement body) #b
2639cases (max_of_expr cond) #c
2640whd in match (max_of_statement Sskip);
2641>(max_id_commutative least_identifier)
2642>max_id_one_neutral normalize nodelta
2643normalize elim u #u
2644cases (leb s b) cases (leb c b) cases (leb c s) try /2/
2645qed.
2646
2647(*
2648lemma for_commute : ∀e,stm1,stm2,u,uA.
2649   (uA=\snd  (switch_removal stm1 u)) →
2650   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
2651#e #stm1 #stm2 #u #uA #HuA
2652whd in match (sw_rem (Sfor ????) u);
2653whd in match (switch_removal ??);   
2654destruct
2655normalize in match (\snd (switch_removal Sskip u));
2656whd in match (sw_rem stm1 u);
2657cases (switch_removal stm1 u)
2658* #stm1' #fresh_vars #uA normalize nodelta
2659whd in match (sw_rem stm2 uA);
2660cases (switch_removal stm2 uA)
2661* #stm2' #fresh_vars2 #uB normalize nodelta
2662//
2663qed.*)
2664
2665(*
2666lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
2667*
2668[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
2669| 2: #e1 #e2 #u #_
2670     whd in match (sw_rem ??);
2671     whd in match (is_Sskip ?);
2672     try /2 by refl, ex_intro/
2673| 3: #ret #f #args #u
2674     whd in match (sw_rem ??);
2675     whd in match (is_Sskip ?);
2676     try /2 by refl, ex_intro/
2677| 4: #s1 #s2 #u
2678     whd in match (sw_rem ??);
2679     whd in match (switch_removal ??);     
2680     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
2681     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
2682     whd in match (is_Sskip ?);
2683     try /2 by refl, ex_intro/
2684| 5: #e #s1 #s2 #u #_
2685     whd in match (sw_rem ??);
2686     whd in match (switch_removal ??);     
2687     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2688     cases (switch_removal ? ?) * #e #f #h normalize nodelta
2689     whd in match (is_Sskip ?);
2690     try /2 by refl, ex_intro/
2691| 6,7: #e #s #u #_
2692     whd in match (sw_rem ??);
2693     whd in match (switch_removal ??);     
2694     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2695     whd in match (is_Sskip ?);
2696     try /2 by refl, ex_intro/
2697| 8: #s1 #e #s2 #s3 #u #_     
2698     whd in match (sw_rem ??);
2699     whd in match (switch_removal ??);     
2700     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2701     cases (switch_removal ? ?) * #e #f #g normalize nodelta
2702     cases (switch_removal ? ?) * #i #j #k normalize nodelta
2703     whd in match (is_Sskip ?);
2704     try /2 by refl, ex_intro/
2705| 9,10: #u #_     
2706     whd in match (is_Sskip ?);
2707     try /2 by refl, ex_intro/
2708| 11: #e #u #_
2709     whd in match (is_Sskip ?);
2710     try /2 by refl, ex_intro/
2711| 12: #e #ls #u #_
2712     whd in match (sw_rem ??);
2713     whd in match (switch_removal ??);
2714     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
2715     cases (fresh ??) #e #f normalize nodelta
2716     normalize in match (simplify_switch ???);
2717     cases (fresh ? f) #g #h normalize nodelta
2718     cases (produce_cond ????) * #k #l #m normalize nodelta
2719     whd in match (is_Sskip ?);
2720     try /2 by refl, ex_intro/
2721| 13,15: #lab #st #u #_
2722     whd in match (sw_rem ??);
2723     whd in match (switch_removal ??);
2724     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2725     whd in match (is_Sskip ?);
2726     try /2 by refl, ex_intro/
2727| 14: #lab #u     
2728     whd in match (is_Sskip ?);
2729     try /2 by refl, ex_intro/ ]
2730qed.
2731*)
2732
2733(*
2734lemma sw_rem_commute : ∀stm,u.
2735  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
2736#stm #u whd in match (sw_rem stm u); // qed.
2737*)
2738
2739lemma fresh_for_statement_inv :
2740  ∀u,s. fresh_for_statement s u →
2741        match u with
2742        [ mk_universe p ⇒ le (p0 one) p ].
2743* #p #s whd in match (fresh_for_statement ??);
2744cases (max_of_statement s) #s
2745normalize /2/ qed.
2746
2747lemma fresh_for_Sskip :
2748  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
2749#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
2750
2751lemma fresh_for_Sbreak :
2752  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
2753#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
2754
2755lemma fresh_for_Scontinue :
2756  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
2757#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
2758
2759(*
2760lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
2761#s #u elim (switch_removal s u) * #res #fvs #u'
2762%{res} %{fvs} %{u'} //
2763qed.
2764
2765lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
2766#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
2767%{res} %{fvs} %{u'} //
2768qed.
2769*)
2770
2771lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
2772#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
2773#s #lab #u' %{s} %{lab} %{u'} //
2774qed.
2775
2776(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
2777lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
2778* * *
2779[ 1,5,9: #H @(False_ind … (H (refl ??)))
2780| *: #_ normalize @refl ]
2781qed.
2782
2783lemma exec_expr_int : ∀ge,e,m,expr.
2784    (∃sz,n,tr. exec_expr ge e m expr = (OK ? 〈Vint sz n, tr〉)) ∨ (∀sz,n,tr. exec_expr ge e m expr ≠ (OK ? 〈Vint sz n, tr〉)).
2785#ge #e #m #expr cases (exec_expr ge e m expr)
2786[ 2: #error %2 #sz #n #tr % #H destruct (H)
2787| 1: * #val #trace cases val
2788     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
2789     | 3: #fl | 4: | 5: #ptr ]
2790     %2 #sz #n #tr % #H destruct (H)
2791] qed.
2792
2793(*
2794lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
2795  exec_expr ge e m cond = OK ? 〈v,tr〉 →
2796  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
2797  exec_expr ge' e m cond = OK ? 〈v,tr〉.
2798#ge #ge' #e #m #cond #v #tr #H *
2799[ 1: #Hsim >(Hsim ? H) //
2800| 2: * #error >H #Habsurd destruct (Habsurd) ]
2801qed. *)
2802
2803(*
2804lemma switch_simulation :
2805∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
2806 switch_cont_sim k k' →
2807 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
2808 fresh_for_statement (Sswitch cond switchcases) u →
2809 ∃tr'.
2810 (eventually ge'
2811  (λs2':state
2812   .switch_state_sim
2813    (State f
2814     (seq_of_labeled_statement (select_switch condsz condval switchcases))
2815     (Kswitch k) e m) s2')
2816  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
2817  tr').
2818#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
2819whd in match (sw_rem (Sswitch cond switchcases) u);
2820whd in match (switch_removal (Sswitch cond switchcases) u);
2821cases switchcases in Hfresh;
2822[ 1: #default_statement #Hfresh_for_default
2823     whd in match (switch_removal_branches ??);
2824     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
2825     elim (switch_removal_eq default_statement u)
2826     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
2827     normalize nodelta
2828     cut (u' = (\snd (switch_removal default_statement u)))
2829     [ 1: >Hdefault_statement_eq // ] #Heq_u'
2830     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
2831     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
2832     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
2833     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
2834     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
2835     normalize nodelta
2836     whd in match (simplify_switch (Expr ??) ?? uv2);
2837     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
2838     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
2839     -Hfreshness #Heq_uv3
2840     normalize nodelta whd in match (add_starting_lbl_list ????);
2841     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
2842     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
2843     -Hfreshness #Heq_uv4
2844     normalize nodelta
2845     @(eventually_later ge' ?? E0)
2846     whd in match (exec_step ??);
2847     %{(State (function_switch_removal f)
2848          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
2849          (Kseq
2850          (Ssequence
2851            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
2852            (Slabel exit_label Sskip))
2853          k') e m)} @conj try //
2854     @(eventually_later ge' ?? E0)
2855     whd in match (exec_step ??);
2856     
2857@chthulhu | @chthulhu
2858qed. *)
2859
2860
2861
2862(* Main theorem. To be ported and completed to memory injections. TODO *)
2863(*
2864theorem switch_removal_correction : ∀ge, ge'.
2865  related_globals ? fundef_switch_removal ge ge' →
2866  ∀s1, s1', tr, s2.
2867  switch_state_sim s1 s1' →
2868  exec_step ge s1 = Value … 〈tr,s2〉 →
2869  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
2870#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
2871inversion Hsim_state
2872[ 1: (* regular state *)
2873  #u #f #s #k #k' #m #m' #result #en #en' #f' #vars
2874  #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_
2875
2876  lapply (sim_related_globals ge ge' e m Hrelated) *
2877  #Hexpr_related #Hlvalue_related
2878  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
2879  cases s in Hu_fresh Heq_env;
2880 
2881
2882theorem switch_removal_correction : ∀ge, ge'.
2883  related_globals ? fundef_switch_removal ge ge' →
2884  ∀s1, s1', tr, s2.
2885  switch_state_sim s1 s1' →
2886  exec_step ge s1 = Value … 〈tr,s2〉 →
2887  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
2888#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
2889inversion Hsim_state
2890[ 1: (* regular state *)
2891  #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_
2892  lapply (sim_related_globals ge ge' e m Hrelated) *
2893  #Hexpr_related #Hlvalue_related
2894  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
2895  cases s in Hu_fresh Heq_env;
2896  (* Perform the intros for the statements*)
2897  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
2898  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
2899  | 14: #lab | 15: #cost #body ]
2900  #Hu_fresh #Heq_env
2901  [ 1: (* Skip *)
2902    whd in match (sw_rem ??);
2903    inversion Hsim_cont normalize nodelta
2904    [ 1: #Hk #Hk' #_ #Hexec_step
2905         @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify
2906         cases (fn_return f) in Hexec_step;
2907         [ 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
2908         | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
2909         normalize nodelta
2910         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H)
2911                %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try //
2912                normalize in Heq_env; destruct (Heq_env)
2913                %3 //
2914(*                cut (blocks_of_env e = blocks_of_env e')
2915                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
2916                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
2917                #Heq >Heq %3 // *)
2918         | *: #H destruct (H) ]
2919    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2920         whd in match (ret ??) in Heq; destruct (Heq)
2921         @(eventually_now ????) whd in match (exec_step ??);
2922         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
2923         %1 try //   
2924    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2925         @(eventually_now ????) whd in match (exec_step ??);
2926         whd in match (ret ??) in Heq; destruct (Heq)
2927         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
2928         >while_commute %1 try //
2929    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2930         @(eventually_now ????) whd in match (exec_step ??);
2931         lapply (Hexpr_related e0)
2932         cases (exec_expr ge e m e0) in Heq;
2933         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2934         | 1: * #b #tr whd in match (m_bind ?????); #Heq
2935              *
2936              [ 2: * #error #Habsurd destruct (Habsurd)
2937              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
2938                   whd in match (bindIO ??????);
2939                   cases (exec_bool_of_val b (typeof e0)) in Heq;
2940                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2941                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
2942                        whd in match (bindIO ??????);
2943                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
2944                             @conj // >dowhile_commute %1 try //
2945                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
2946                             @conj // %1{us} try //
2947                             @(fresh_for_Sskip … Hus_fresh)
2948                        ] ] ] ]
2949    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2950         @(eventually_now ????) whd in match (exec_step ??);
2951         whd in match (ret ??) in Heq; destruct
2952         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
2953         @conj try // %1{u} try //
2954    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
2955         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
2956         destruct (Heq)
2957         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
2958         @conj try // %1
2959         [ 2: @swc_for3 //
2960         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
2961    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
2962         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
2963         destruct (Heq)
2964         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
2965         @conj try // <(for_commute ??? u uA) try // %1
2966         [ 2: assumption
2967         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
2968    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
2969         #Heq @(eventually_now ????) whd in match (exec_step ??);
2970         destruct (Heq)
2971         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
2972         %1{u} //
2973    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
2974         @(eventually_now ????) whd in match (exec_step ??);
2975         >fn_return_simplify cases (fn_return f) in Heq;
2976         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
2977         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
2978         normalize nodelta
2979         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
2980              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
2981              @conj try // %3 destruct //
2982         | *: #H destruct (H) ]     
2983     ]
2984  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
2985       whd in match (exec_step ??);
2986       cases lhs in Hu_fresh Heq; #lhs #lhs_type
2987       cases (Hlvalue_related lhs lhs_type)
2988       whd in match (exec_lvalue ge e m (Expr ??));
2989       whd in match (exec_lvalue ge' e m (Expr ??));
2990       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
2991       cases (exec_lvalue' ge e m lhs lhs_type)
2992       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
2993       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
2994            whd in match (m_bind ?????);
2995            cases (Hexpr_related rhs)
2996            [ 2: * #error #Hfail >Hfail #_
2997                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2998            | 1: cases (exec_expr ge e m rhs)
2999                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3000                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
3001                      whd in match (bindIO ??????) in ⊢ (% → % → %);
3002                      cases (opt_to_io io_out io_in ???)
3003                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3004                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3005                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
3006                           %{(State (function_switch_removal f) Sskip k' e mem)}
3007                           whd in match (bindIO ??????); @conj //
3008                           %1{u} try // @(fresh_for_Sskip … Hfresh)
3009       ] ] ] ]
3010   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
3011        whd in match (exec_step ??);
3012        cases (Hexpr_related func) in Heq;
3013        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3014        | 1: cases (exec_expr ge e m func)
3015             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3016             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
3017                  whd in match (m_bind ?????); normalize nodelta
3018                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
3019                  #Hexprlist_sim cases (Hexprlist_sim args)
3020                  [ 2: * #error #Hfail >Hfail
3021                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3022                  | 1: cases (exec_exprlist ge e m args)
3023                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3024                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
3025                            whd in match (bindIO ??????) in ⊢ (% → %);
3026                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
3027                            cases (find_funct clight_fundef ge fval)
3028                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
3029                                 whd in match (bindIO ??????) in ⊢ (% → %);
3030                                 >fundef_type_simplify
3031                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
3032                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3033                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
3034                                      cases retv normalize nodelta
3035                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
3036                                           %{(Callstate (fundef_switch_removal clfd) values
3037                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
3038                                           @conj try // %2 try // @swc_call //
3039                                      | 2: * #retval_ed #retval_type
3040                                           whd in match (exec_lvalue ge ???);
3041                                           whd in match (exec_lvalue ge' ???);                                     
3042                                           elim (Hlvalue_related retval_ed retval_type)
3043                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3044                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
3045                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
3046                                                     destruct (Habsurd)
3047                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
3048                                                     whd in match (m_bind ?????) in ⊢ (% → %);
3049                                                     #Heq destruct (Heq)
3050                                                     %{(Callstate (fundef_switch_removal clfd) values
3051                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
3052                                                               (function_switch_removal f) e k') m)}
3053                                                     @conj try //
3054                                                     %2 @swc_call //
3055                                ] ] ] ]
3056                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
3057                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3058       ] ] ] ] ]
3059   | 4: (* Ssequence *) normalize nodelta
3060        whd in match (ret ??) in ⊢ (% → ?); #Heq
3061        @(eventually_now ????)
3062        %{(State (function_switch_removal f)
3063                 (\fst (\fst (switch_removal stm1 u)))
3064                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
3065        @conj
3066        [ 2: destruct (Heq) %1
3067             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
3068             | 2: @swc_seq try // @switch_removal_fresh
3069                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
3070        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
3071             cases (switch_removal stm1 u)
3072             * #stm1' #fresh_vars #u' normalize nodelta
3073             cases (switch_removal stm2 u')
3074             * #stm2' #fresh_vars2 #u'' normalize nodelta
3075             whd in match (exec_step ??);
3076             destruct (Heq) @refl
3077        ]
3078   | 5: (* If-then-else *) normalize nodelta
3079        whd in match (ret ??) in ⊢ (% → ?); #Heq
3080        @(eventually_now ????) whd in match (sw_rem ??);
3081        whd in match (switch_removal ??);
3082        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
3083        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
3084        whd in match (exec_step ??);
3085        cases (Hexpr_related cond) in Heq;
3086        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3087        | 1: cases (exec_expr ge e m cond)
3088             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3089             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3090                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3091                  cases (exec_bool_of_val condval (typeof cond))
3092                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3093                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
3094                       destruct (Heq_condval) whd in match (bindIO ??????);
3095                       normalize nodelta
3096                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
3097                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
3098                           [ 1: >Hiftrue_eq normalize // ]
3099                           #Hrewrite >Hrewrite %1
3100                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
3101                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
3102                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
3103                           [ 1: >Hiffalse_eq // ]
3104                           #Hrewrite >Hrewrite %1 try //
3105                           cut (uA = (\snd (switch_removal iftrue u)))
3106                           [ 1: >Hiftrue_eq //
3107                           | 2: #Heq_uA >Heq_uA
3108                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
3109                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
3110       ] ] ] ] ]
3111   | 6: (* While loop *) normalize nodelta
3112        whd in match (ret ??) in ⊢ (% → ?); #Heq
3113        @(eventually_now ????) whd in match (sw_rem ??);
3114        whd in match (switch_removal ??);
3115        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
3116        whd in match (exec_step ??);
3117        cases (Hexpr_related cond) in Heq;
3118        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3119        | 1: cases (exec_expr ge e m cond)
3120             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3121             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3122                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3123                  cases (exec_bool_of_val condval (typeof cond))
3124                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3125                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
3126                       destruct (Heq_condval) whd in match (bindIO ??????);
3127                       normalize nodelta
3128                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
3129                            cut (body' = (\fst (\fst (switch_removal body u))))
3130                            [ 1: >Hbody_eq // ]
3131                            #Hrewrite >Hrewrite %1
3132                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
3133                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
3134                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
3135                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
3136        ] ] ] ]
3137   | 7: (* Dowhile loop *) normalize nodelta
3138        whd in match (ret ??) in ⊢ (% → ?); #Heq
3139        @(eventually_now ????) whd in match (sw_rem ??);
3140        whd in match (switch_removal ??);
3141        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
3142        whd in match (exec_step ??);
3143        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
3144        try //
3145        cut (body' = (\fst (\fst (switch_removal body u))))
3146        [ 1: >Hbody_eq // ]
3147        #Hrewrite >Hrewrite %1
3148        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
3149        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
3150   | 8: (* For loop *) normalize nodelta
3151        whd in match (ret ??) in ⊢ (% → ?); #Heq
3152        @(eventually_now ????) whd in match (sw_rem ??);
3153        whd in match (switch_removal ??);
3154        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
3155        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
3156              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
3157              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
3158              whd in match (exec_step ??);
3159              cases (Hexpr_related cond)
3160              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3161              | 1: cases (exec_expr ge e m cond)
3162                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3163                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3164                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3165                        cases (exec_bool_of_val condval (typeof cond))
3166                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3167                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
3168                             destruct (Heq_condval)
3169                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
3170                                  try //
3171                                  cut (body' = (\fst (\fst (switch_removal body uA))))
3172                                  [ 1: >Hbody_eq // ]
3173                                  #Hrewrite >Hrewrite
3174                                  cut (uA = (\snd (switch_removal step u)))
3175                                  [ 1: >Hstep_eq // ] #HuA
3176                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
3177                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
3178                                  [ 1: >HuA @switch_removal_fresh assumption
3179                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
3180                                       [ >Hstep_eq // ]
3181                                       #Hstep >Hstep @swc_for2 try assumption
3182                                       @for_fresh_lift try assumption ]
3183                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
3184                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
3185               ] ] ] ]
3186        | 2: #Heq
3187             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
3188             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
3189             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
3190             whd in match (exec_step ??);
3191             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
3192             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
3193             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
3194             whd in match (ret ??); destruct (Heq)
3195             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
3196             @conj try //
3197             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
3198             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
3199             <for_commute [ 2: >Hstep_eq // ]
3200             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
3201             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
3202             @swc_seq try // @for_fresh_lift
3203             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
3204             >HuA_eq @switch_removal_fresh assumption       
3205       ]
3206   | 9: (* break *) normalize nodelta
3207        inversion Hsim_cont
3208        [ 1: #Hk #Hk' #_       
3209        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
3210        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
3211        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3212        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3213        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
3214        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
3215        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
3216        normalize nodelta #H try (destruct (H))
3217        whd in match (ret ??) in H; destruct (H)
3218        @(eventually_now ????)
3219        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
3220        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
3221    | 10: (* Continue *) normalize nodelta
3222        inversion Hsim_cont
3223        [ 1: #Hk #Hk' #_       
3224        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
3225        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
3226        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3227        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3228        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
3229        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
3230        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
3231        normalize nodelta #H try (destruct (H))
3232        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
3233        destruct (H)
3234        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
3235        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
3236             >while_commute %1{u0} try assumption
3237        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
3238             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3239             | 1: * #condval #trace whd in match (m_bind ?????);
3240                  #Heq *
3241                  [ 2: * #error #Habsurd destruct (Habsurd)
3242                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
3243                       whd in match (bindIO ??????);
3244                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
3245                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3246                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
3247                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)}
3248                                 @conj try // >dowhile_commute %1{u0} assumption
3249                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
3250                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
3251             ] ] ]
3252        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
3253             try // @(fresh_for_Scontinue … Hfor_fresh)
3254        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
3255             @conj try // %1{u0}
3256             elim (substatement_fresh … Hfor_fresh) * * try //
3257             #HSskip #Hcond #Hstep #Hbody
3258             @swc_for3 assumption
3259        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
3260             %1{u} try //
3261        ]
3262    | 11: (* Sreturn *) normalize nodelta #Heq
3263          @(eventually_now ????)
3264          whd in match (exec_step ??) in Heq ⊢ %;
3265          cases retval in Heq; normalize nodelta
3266          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
3267               whd in match (ret ??) in ⊢ (% → %);
3268               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
3269               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
3270               #H destruct (H)
3271               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
3272               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
3273          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
3274               [ 1: #_ #Habsurd destruct (Habsurd)
3275               | 2: #_ elim (Hexpr_related expr)
3276                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3277                    | 1: cases (exec_expr ??? expr)
3278                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3279                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
3280                              #Hrewrite >Hrewrite
3281                              whd in match (m_bind ?????); whd in match (m_bind ?????);
3282                              #Heq destruct (Heq)
3283                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
3284                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
3285         ] ] ] ]
3286    | 12: (* Sswitch. Main proof case. *) normalize nodelta
3287          (* Case analysis on the outcome of the tested expression *)
3288          cases (exec_expr_int ge e m cond)
3289          [ 2: cases (exec_expr ge e m cond)
3290               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
3291               | 1: * #val #trace cases val
3292                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
3293                    whd in match (m_bind ?????);
3294                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
3295                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
3296          ]
3297          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
3298          whd in match (m_bind ?????); #Heq
3299          destruct (Heq)
3300          @eventually_later
3301          whd in match (sw_rem (Sswitch cond switchcases) u);
3302          whd in match (switch_removal (Sswitch cond switchcases) u);
3303          elim (switch_removal_branches_eq switchcases u)
3304          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
3305          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
3306          [ 1: >Hsrb_eq // ] #Huv1_eq
3307          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
3308          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
3309          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
3310          whd in match (simplify_switch ???);
3311          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
3312          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
3313          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)         
3314          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
3315          #Huv4_eq
3316          whd in match (exec_step ??);
3317          %{(State (function_switch_removal f)
3318                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
3319                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
3320          %{E0} @conj try @refl
3321          %{tr} normalize in match (eq ???); @conj try //
3322          (* execute the conditional *)
3323          @eventually_later
3324          (* lift the result of the previous case analysis from [ge] to [ge'] *)
3325          whd in match (exec_step ??);
3326          whd in match (exec_lvalue ????);
3327         
3328          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
3329         
3330  *)
3331 
Note: See TracBrowser for help on using the repository browser.