source: src/Clight/switchRemoval.ma @ 2255

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

Had to modify the definition of memory injections to prove that valid_pointer is preserved.

  • Property svn:executable set to *
File size: 177.4 KB
Line 
1include "Clight/Csyntax.ma".
2include "Clight/fresh.ma".
3include "basics/lists/list.ma".
4include "common/Identifiers.ma".
5include "Clight/Cexec.ma".
6include "Clight/CexecInd.ma".
7include "Clight/frontend_misc.ma".
8(*
9include "Clight/maps_obsequiv.ma".
10*)
11
12
13(* -----------------------------------------------------------------------------
14   ----------------------------------------------------------------------------*)
15
16(* -----------------------------------------------------------------------------
17   Documentation
18   ----------------------------------------------------------------------------*)
19
20(* This file implements transformation of switches to linear sequences of
21 * if/then/else. The implementation roughly follows the lines of the prototype.
22 * /!\ We assume that the program is well-typed (the type of the evaluated
23 * expression must match the constants on each branch of the switch). /!\ *)
24
25(* Documentation. Let the follwing be our input switch construct:
26   // --------------------------------- 
27   switch(e) {
28   case v1:
29     stmt1
30   case v2:
31     stmt2
32   .
33   .
34   .
35   default:
36     stmt_default
37   }
38   // --------------------------------- 
39 
40   Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting
41   the switch statement. In the absence of break, the execution falls through each case sequentially.
42 
43   Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos:
44
45   // --------------------------------- 
46   fresh = e;
47   if(fresh == v1) {
48     stmt1';
49     goto lbl_case2;
50   }
51   if(fresh == v2) {
52     lbl_case2:
53     stmt2';
54     goto lbl_case2;
55   }   
56   ...
57   stmt_default';
58   exit_label:
59   // ---------------------------------   
60
61   where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements
62   were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels.
63*)
64
65
66(* -----------------------------------------------------------------------------
67   Definitions allowing to state that the program resulting of the transformation
68   is switch-free.
69   ---------------------------------------------------------------------------- *)
70
71(* Property of a Clight statement of containing no switch. Could be generalized into a kind of
72 * statement_P, if useful elsewhere. *)
73let rec switch_free (st : statement) : Prop ≝
74match st with
75[ Sskip ⇒ True
76| Sassign _ _ ⇒ True
77| Scall _ _ _ ⇒ True
78| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
79| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
80| Swhile e body ⇒ switch_free body
81| Sdowhile e body ⇒ switch_free body
82| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
83| Sbreak ⇒ True
84| Scontinue ⇒ True
85| Sreturn _ ⇒ True
86| Sswitch _ _ ⇒ False
87| Slabel _ body ⇒ switch_free body
88| Sgoto _ ⇒ True
89| Scost _ body ⇒ switch_free body
90].
91
92(* Property of a list of labeled statements of being switch-free *)
93let rec branches_switch_free (sts : labeled_statements) : Prop ≝
94match sts with
95[ LSdefault st =>
96  switch_free st
97| LScase _ _ st tl =>
98  switch_free st ∧ branches_switch_free tl
99].
100
101let rec branches_ind
102  (sts : labeled_statements)
103  (H   : labeled_statements → Prop) 
104  (defcase : ∀st. H (LSdefault st))
105  (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝
106match sts with
107[ LSdefault st ⇒
108  defcase st
109| LScase sz int st tl ⇒
110  indcase sz int st tl (branches_ind tl H defcase indcase)
111].
112
113(* -----------------------------------------------------------------------------
114   Switch-removal code for statements, functions and fundefs.
115   ----------------------------------------------------------------------------*)
116
117(* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
118let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
119match st with
120[ Sbreak ⇒
121  Sgoto lab
122| Ssequence s1 s2 ⇒
123  Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab)
124| Sifthenelse e iftrue iffalse ⇒
125  Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab)
126| Sfor init e update body ⇒
127  Sfor (convert_break_to_goto init lab) e update body
128| Slabel l body ⇒
129  Slabel l (convert_break_to_goto body lab)
130| Scost cost body ⇒
131  Scost cost (convert_break_to_goto body lab)
132| _ ⇒ st
133].
134
135(* Converting breaks preserves switch-freeness. *)
136lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label).
137#s elim s //
138[ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
139| 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
140| 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
141     try @conj try @conj /3/
142| 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/
143| 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/
144] qed.
145
146(* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)
147(*
148let rec produce_cond
149  (e : expr)
150  (switch_cases : stlist)
151  (def_case : ident × sf_statement)
152  (exit : label) on switch_cases : sf_statement × label ≝
153match switch_cases with
154[ nil ⇒
155  match def_case with
156  [ mk_Prod default_label default_statement ⇒
157    〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
158  ]
159| cons switch_case tail ⇒
160  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
161    match case_value with
162    [ mk_DPair sz val ⇒
163       let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
164       (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *)
165       (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed)  in *)
166       let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in
167       let result ≝
168         Sifthenelse test
169          (Slabel case_label
170            (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
171                       (Sgoto sub_label)))
172          (pi1 … sub_statement)
173      in
174      〈«result, ?», case_label〉
175    ]
176].
177[ 1: normalize @convert_break_lift elim default_statement //
178| 2: whd @conj normalize try @conj try //
179  [ 1: @convert_break_lift elim case_statement //
180  | 2: elim sub_statement // ]
181] qed. *)
182
183(* We assume that the expression e is consistely typed w.r.t. the switch branches *)
184(*
185let rec produce_cond2
186  (e : expr)
187  (switch_cases : stlist)
188  (def_case : ident × sf_statement)
189  (exit : label) on switch_cases : sf_statement × label ≝
190match switch_cases with
191[ nil ⇒
192  let 〈default_label, default_statement〉 ≝ def_case in
193  〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
194| cons switch_case tail ⇒
195  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
196  match case_value with
197  [ mk_DPair sz val ⇒
198    let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
199    let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in
200    let case_statement_res ≝
201       Sifthenelse test
202        (Slabel case_label
203          (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
204                     (Sgoto sub_label)))
205        Sskip
206    in
207    〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉
208  ]
209].
210[ 1: normalize @convert_break_lift elim default_statement //
211| 2: whd @conj
212     [ 1: whd @conj try // whd in match (switch_free ?); @conj
213          [ 1: @convert_break_lift elim case_statement //
214          | 2: // ]
215     | 2: elim sub_statement // ]
216] qed. *)
217
218(*  (def_case : ident × sf_statement) *)
219
220let rec produce_cond
221  (e : expr)
222  (switch_cases : labeled_statements)
223  (u : universe SymbolTag)
224  (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝
225match switch_cases with
226[ LSdefault st ⇒ 
227  let 〈lab,u1〉 ≝ fresh ? u in
228  let st' ≝ convert_break_to_goto st exit in
229  〈Slabel lab st', lab, u1〉
230| LScase sz tag st other_cases ⇒
231  let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in
232  let st' ≝ convert_break_to_goto st exit in
233  let 〈lab, u2〉 ≝ fresh ? u1 in
234  let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in
235  let case_statement ≝
236       Sifthenelse test
237        (Slabel lab (Ssequence st' (Sgoto sub_label)))
238        Sskip
239  in
240  〈Ssequence case_statement sub_statements, lab, u2〉
241].
242
243definition simplify_switch ≝
244   λ(e : expr).
245   λ(switch_cases : labeled_statements).
246   λ(uv : universe SymbolTag).
247 let 〈exit_label, uv1〉            ≝ fresh ? uv in
248 let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in
249 〈Ssequence result (Slabel exit_label Sskip), uv2〉.
250
251lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))).
252#l @(labeled_statements_ind … l)
253[ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1
254     normalize in Hsf ⊢ %; @(convert_break_lift … Hsf)
255| 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl
256     #e #lab #u normalize
257     lapply (Hind Hsf_tl e lab u)
258     cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta
259     cases (fresh ??) #lab0 #u2 normalize nodelta
260     normalize try @conj try @conj try @conj try //
261     @(convert_break_lift … Hsf_hd)
262] qed.
263
264lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)).
265#e #l cases l
266[ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta
267     whd @conj whd
268     [ 1: @convert_break_lift assumption
269     | 2: @I ]
270| 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u
271     cases (fresh ? u) #exit_label #uv1 normalize nodelta
272     lapply (produce_cond_switch_free tl Hsftl e exit_label uv1)
273     cases (produce_cond e tl uv1 exit_label)
274     * #cond #lab #u1 #Hsf_cond normalize nodelta
275     cases (fresh ??) #lab0 #u2 normalize nodelta
276     normalize @conj try @conj try @conj try @conj try //
277     @(convert_break_lift ?? Hsf)
278] qed.
279
280(* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in
281   order to circumvent the associativity problems in notations. *)
282record swret (A : Type[0]) : Type[0] ≝ {
283  ret_st  : A;
284  ret_acc : list (ident × type);
285  ret_fvs : list ident;
286  ret_u   : universe SymbolTag
287}.
288
289notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48
290for @{ match ${e} with
291       [ None ⇒ None ?
292       | Some ${fresh ret} ⇒
293          (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'})
294          (ret_st ? ${fresh ret})
295          (ret_acc ? ${fresh ret})
296          (ret_fvs ? ${fresh ret})
297          (ret_u ? ${fresh ret}) ] }.
298
299notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49
300for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4})  }.
301     
302(* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
303   of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another
304   'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables
305   allows it to proceed without failing. This is all in order to ease the proof of simulation. *)
306let rec switch_removal
307  (st : statement)           (* the statement in which we will remove switches *)
308  (fvs : list ident)         (* a finite list of names usable to create variables. *)
309  (u : universe SymbolTag)   (* a fresh /label/ generator *)
310  : option (swret statement) ≝
311match st with
312[ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
313| Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
314| Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉
315| Ssequence s1 s2 ⇒
316  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
317  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
318  ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉
319| Sifthenelse e s1 s2 ⇒
320  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
321  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
322  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
323| Swhile e body ⇒
324  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
325  ret 〈Swhile e body', acc, fvs', u'〉
326| Sdowhile e body ⇒
327  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
328  ret 〈Sdowhile e body', acc, fvs', u'〉
329| Sfor s1 e s2 s3 ⇒
330  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
331  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
332  do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
333  ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
334| Sbreak ⇒
335  ret 〈st, [ ], fvs, u〉
336| Scontinue ⇒
337  ret 〈st, [ ], fvs, u〉
338| Sreturn _ ⇒
339  ret 〈st, [ ], fvs, u〉
340| Sswitch e branches ⇒   
341   do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u;
342   match fvs' with
343   [ nil ⇒ None ?
344   | cons fresh tl ⇒
345     (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *)
346     let ident         ≝ Expr (Evar fresh) (typeof e) in
347     let assign        ≝ Sassign ident e in
348     let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in
349       ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉
350   ]
351| Slabel label body ⇒
352  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
353  ret 〈Slabel label body', acc, fvs', u'〉
354| Sgoto _ ⇒
355  ret 〈st, [ ], fvs, u〉
356| Scost cost body ⇒
357  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
358  ret 〈Scost cost body', acc, fvs', u'〉
359]
360
361and switch_removal_branches
362  (l : labeled_statements)
363  (fvs : list ident)
364  (u : universe SymbolTag)
365(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
366match l with
367[ LSdefault st ⇒
368  do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
369  ret 〈LSdefault st', acc1, fvs', u'〉
370| LScase sz int st tl =>
371  do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u;
372  do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u';
373  ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉
374].
375
376let rec mk_fresh_variables
377  (st : statement)           (* the statement in which we will remove switches *)
378  (u : universe SymbolTag)   (* a fresh /label/ generator *)
379  : (list ident) × (universe SymbolTag) ≝
380match st with
381[ Sskip       ⇒ 〈[ ], u〉
382| Sassign _ _ ⇒ 〈[ ], u〉
383| Scall _ _ _ ⇒ 〈[ ], u〉
384| Ssequence s1 s2 ⇒
385  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
386  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
387  〈fvs @ fvs', u''〉
388| Sifthenelse e s1 s2 ⇒
389  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
390  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
391  〈fvs @ fvs', u''〉
392| Swhile e body ⇒
393  mk_fresh_variables body u
394| Sdowhile e body ⇒
395  mk_fresh_variables body u
396| Sfor s1 e s2 s3 ⇒
397  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
398  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
399  let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
400  〈fvs @ fvs' @fvs'', u'''〉
401| Sbreak ⇒
402  〈[ ], u〉
403| Scontinue ⇒
404  〈[ ], u〉
405| Sreturn _ ⇒
406  〈[ ], u〉
407| Sswitch e branches ⇒   
408   let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *)
409   let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in
410   〈fvs @ [ident], u''〉  (* reversing the order to match a proof invariant *)
411| Slabel label body ⇒
412  mk_fresh_variables body u
413| Sgoto _ ⇒
414  〈[ ], u〉
415| Scost cost body ⇒
416  mk_fresh_variables body u
417]
418
419and mk_fresh_variables_branches
420  (l : labeled_statements)
421  (u : universe SymbolTag)
422(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
423match l with
424[ LSdefault st ⇒
425  mk_fresh_variables st u
426| LScase sz int st tl =>
427  let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in
428  let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in
429  〈fvs @ fvs', u''〉
430].
431
432(* Copied this from Csyntax.ma, lifted from Prop to Type
433   (I needed to eliminate something proved with this towards Type)  *)
434let rec statement_indT
435  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
436  (Ssk:P Sskip)
437  (Sas:∀e1,e2. P (Sassign e1 e2))
438  (Sca:∀eo,e,args. P (Scall eo e args))
439  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
440  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
441  (Swh:∀e,s. P s → P (Swhile e s))
442  (Sdo:∀e,s. P s → P (Sdowhile e s))
443  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
444  (Sbr:P Sbreak)
445  (Sco:P Scontinue)
446  (Sre:∀eo. P (Sreturn eo))
447  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
448  (Sla:∀l,s. P s → P (Slabel l s))
449  (Sgo:∀l. P (Sgoto l))
450  (Scs:∀l,s. P s → P (Scost l s))
451  (LSd:∀s. P s → Q (LSdefault s))
452  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
453  (s:statement) on s : P s ≝
454match s with
455[ Sskip ⇒ Ssk
456| Sassign e1 e2 ⇒ Sas e1 e2
457| Scall eo e args ⇒ Sca eo e args
458| Ssequence s1 s2 ⇒ Ssq s1 s2
459    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
460    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
461| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
462    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
463    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
464| Swhile e s ⇒ Swh e s
465    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
466| Sdowhile e s ⇒ Sdo e s
467    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
468| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
469    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
470    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
471    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
472| Sbreak ⇒ Sbr
473| Scontinue ⇒ Sco
474| Sreturn eo ⇒ Sre eo
475| Sswitch e ls ⇒ Ssw e ls
476    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
477| Slabel l s ⇒ Sla l s
478    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
479| Sgoto l ⇒ Sgo l
480| Scost l s ⇒ Scs l s
481    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
482]
483and labeled_statements_indT
484  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
485  (Ssk:P Sskip)
486  (Sas:∀e1,e2. P (Sassign e1 e2))
487  (Sca:∀eo,e,args. P (Scall eo e args))
488  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
489  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
490  (Swh:∀e,s. P s → P (Swhile e s))
491  (Sdo:∀e,s. P s → P (Sdowhile e s))
492  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
493  (Sbr:P Sbreak)
494  (Sco:P Scontinue)
495  (Sre:∀eo. P (Sreturn eo))
496  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
497  (Sla:∀l,s. P s → P (Slabel l s))
498  (Sgo:∀l. P (Sgoto l))
499  (Scs:∀l,s. P s → P (Scost l s))
500  (LSd:∀s. P s → Q (LSdefault s))
501  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
502  (ls:labeled_statements) on ls : Q ls ≝
503match ls with
504[ LSdefault s ⇒ LSd s
505    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
506| LScase sz i s t ⇒ LSc sz i s t
507    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
508    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
509].
510
511lemma switch_removal_ok :
512  ∀st, u0, u1, post.
513  Σresult.
514  (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post).
515#st
516@(statement_indT ? (λls. ∀u0, u1, post.
517                          Σresult.
518                          (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result)
519                          ∧ (ret_fvs ? result = post)
520                   ) … st)
521[ 1: #u0 #u1 #post normalize
522     %{(mk_swret statement Sskip [] post u1)} % //
523| 2: #e1 #e2 #u0 #u1 #post normalize
524     %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try //
525| 3: #e0 #e #args #u0 #u1 #post normalize
526     %{(mk_swret statement (Scall e0 e args) [] post u1)} % try //
527| 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
528     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
529     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
530     elim (H2 u' (ret_u ? s1') post) #s2' *
531     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
532     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
533     %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2'))
534        (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
535        (ret_u statement s2'))} % try //
536| 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
537     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
538     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
539     elim (H2 u' (ret_u ? s1') post) #s2' *
540     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
541     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
542     %{((mk_swret statement
543         (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
544         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
545         (ret_u statement s2')))} % try //
546| 6: #e #s #H #u0 #u1 #post normalize
547     elim (H u0 u1 post) #s1' * normalize
548     cases (mk_fresh_variables s u0) #fvs #u'
549     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
550     %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
551        (ret_fvs statement s1') (ret_u statement s1'))} % try //
552| 7: #e #s #H #u0 #u1 #post normalize
553     elim (H u0 u1 post) #s1' * normalize
554     cases (mk_fresh_variables s u0) #fvs #u'
555     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
556     %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
557        (ret_fvs statement s1') (ret_u statement s1'))} % try //
558| 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
559     elim (H1 u0 u1
560                (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
561                (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
562                post)) #s1' *
563     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
564     elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 u')))) @
565                                 post)) #s2' *
566     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
567     elim (H3 u'' (ret_u ? s2') post) #s3' *
568     cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta
569     #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs
570     >associative_append >associative_append >Heq1 normalize >Heq1_fvs
571     >Heq2 normalize >Heq2_fvs >Heq3 normalize
572     %{(mk_swret statement
573        (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
574        (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
575        (ret_fvs statement s3') (ret_u statement s3'))} % try //
576| 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
577| 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % //
578| 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % //
579| 12: #e #ls #H #u0 #u1 #post
580      whd in match (mk_fresh_variables ??);
581      whd in match (switch_removal ???);     
582      elim (fresh ? u0) #fresh #u'
583      elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta
584      cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta     
585      >associative_append #Heq #Heq_fvs >Heq normalize nodelta
586      >Heq_fvs normalize nodelta
587      cases (simplify_switch ???) #st' #u''' normalize nodelta
588      %{((mk_swret statement
589          (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st')
590          (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post)
591          (ret_u labeled_statements ls')))} % //
592| 13: #l #s #H #u0 #u1 #post normalize
593      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
594      %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s')
595           post (ret_u statement s'))} % //
596| 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % //
597| 15: #l #s #H #u0 #u1 #post normalize
598      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
599      %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s')
600           post (ret_u statement s'))} % //
601| 16: #s #H #u0 #u1 #post normalize
602      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
603      %{(mk_swret labeled_statements (LSdefault (ret_st statement s'))
604         (ret_acc statement s') post (ret_u statement s'))} % //
605| 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize
606      elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' *
607      cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize
608      elim (H1 u' (ret_u labeled_statements ls') post) #s1' *
609      cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs
610      >associative_append >Heql normalize >Heql_fvs >Heq normalize
611      %{(mk_swret labeled_statements
612          (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls'))
613          (ret_acc labeled_statements ls'@ret_acc statement s1')
614          (ret_fvs statement s1') (ret_u statement s1'))} % //
615] qed.
616
617axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
618
619(* Proof that switch_removal_switch_free does its job. *)
620lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result).
621#st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result →
622                                                 branches_switch_free (ret_st ? ls_result)) … st)
623[ 1: #fvs #u #result normalize #Heq destruct (Heq) //
624| 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) //
625| 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) //
626| 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u)
627     elim (switch_removal s1 fvs u) normalize
628     [ 1: #_ #Habsurd destruct (Habsurd)
629     | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1))
630          elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1))
631          [ 1: normalize #_ #Habsurd destruct (Habsurd)
632          | 2: normalize #res2 #Heq2 #Heq destruct (Heq)
633               normalize @conj
634               [ 1: @Heq1 // | 2: @Heq2 // ]
635     ] ]
636| *:
637  (* TODO the first few cases show that the lemma is routinely proved. TBF later. *)
638  @cthulhu ]
639qed.
640
641(* -----------------------------------------------------------------------------
642   Switch-removal code for programs.
643   ----------------------------------------------------------------------------*) 
644
645(* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to
646 * name clashes for labels. We have no choice but to actually run through the function and to
647 * compute the maximum of labels+identifiers. This way we can generate both fresh variables and
648 * fresh labels using the same univ. While we're at it we also consider record fields.
649 * Cost labels are not considered, though. They already live in a separate universe.
650 *
651 * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes,
652 * but in the end it might be good to move the following functions into fresh.ma.
653 *)
654
655(* Least element in the total order of identifiers. *)
656definition least_identifier ≝ an_identifier SymbolTag one.
657
658(* This is certainly overkill: variables adressed in an expression should be declared in the
659 * enclosing function's prototype. *)
660let rec max_of_expr (e : expr) : ident ≝
661match e with
662[ Expr ed _ ⇒
663  match ed with
664  [ Econst_int _ _ ⇒ least_identifier
665  | Econst_float _ ⇒ least_identifier
666  | Evar id ⇒ id
667  | Ederef e1 ⇒ max_of_expr e1
668  | Eaddrof e1 ⇒ max_of_expr e1
669  | Eunop _ e1 ⇒ max_of_expr e1
670  | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
671  | Ecast _ e1 ⇒ max_of_expr e1
672  | Econdition e1 e2 e3 ⇒ 
673    max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3))
674  | Eandbool e1 e2 ⇒
675    max_id (max_of_expr e1) (max_of_expr e2)
676  | Eorbool e1 e2 ⇒
677    max_id (max_of_expr e1) (max_of_expr e2) 
678  | Esizeof _ ⇒ least_identifier
679  | Efield r f ⇒ max_id f (max_of_expr r)
680  | Ecost _ e1 ⇒ max_of_expr e1
681  ]
682].
683
684(* Reasoning about this promises to be a serious pain. Especially the Scall case. *)
685let rec max_of_statement (s : statement) : ident ≝
686match s with
687[ Sskip ⇒ least_identifier
688| Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
689| Scall r f args ⇒
690  let retmax ≝
691    match r with
692    [ None ⇒ least_identifier
693    | Some e ⇒ max_of_expr e ]
694  in
695  max_id (max_of_expr f)
696         (max_id retmax
697                 (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )
698| Ssequence s1 s2 ⇒
699  max_id (max_of_statement s1) (max_of_statement s2)
700| Sifthenelse e s1 s2 ⇒
701  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
702| Swhile e body ⇒
703  max_id (max_of_expr e) (max_of_statement body)
704| Sdowhile e body ⇒
705  max_id (max_of_expr e) (max_of_statement body)
706| Sfor init test incr body ⇒
707  max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body))
708| Sbreak ⇒ least_identifier
709| Scontinue ⇒ least_identifier
710| Sreturn opt ⇒
711  match opt with
712  [ None ⇒ least_identifier
713  | Some e ⇒ max_of_expr e
714  ]
715| Sswitch e ls ⇒
716  max_id (max_of_expr e) (max_of_ls ls)
717| Slabel lab body ⇒
718  max_id lab (max_of_statement body)
719| Sgoto lab ⇒
720  lab
721| Scost _ body ⇒
722  max_of_statement body
723]
724and max_of_ls (ls : labeled_statements) : ident ≝
725match ls with
726[ LSdefault s ⇒ max_of_statement s
727| LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s)
728].
729
730definition max_id_of_function : function → ident ≝
731λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f).
732
733(* We compute fresh universes on a function-by function basis, since there can't
734 * be cross-functions gotos or stuff like that. *)
735definition function_switch_removal : function → function × (list (ident × type)) ≝
736λf.
737  (λres_record.
738    let new_vars ≝ ret_acc ? res_record in
739    let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in
740    〈result, new_vars〉)
741  (let u ≝ universe_of_max (max_id_of_function f) in
742   let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in
743   match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with
744   [ None ⇒ λHsr. ?
745   | Some res_record ⇒ λ_. res_record
746   ] (refl ? (switch_removal (fn_body f) fvs u'))).   
747lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq
748<Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd)
749qed.
750
751let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝
752match f with
753[ CL_Internal f ⇒
754  CL_Internal (\fst (function_switch_removal f))
755| CL_External _ _ _ ⇒
756  f
757].
758
759let rec program_switch_removal (p : clight_program) : clight_program ≝
760 let prog_funcs ≝ prog_funct ?? p in
761 let sf_funcs   ≝ map ?? (λcl_fundef.
762    let 〈fun_id, fun_def〉 ≝ cl_fundef in
763    〈fun_id, fundef_switch_removal fun_def〉
764  ) prog_funcs in
765 mk_program ??
766  (prog_vars … p)
767  sf_funcs
768  (prog_main … p).
769
770
771(* -----------------------------------------------------------------------------
772   Applying two relations on all substatements and all subexprs (directly under).
773   ---------------------------------------------------------------------------- *)
774
775let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝
776match s1 with
777[ Sskip ⇒ True
778| Sassign e1 e2 ⇒ Q e1 ∧ Q e2
779| Scall r f args ⇒
780  match r with
781  [ None ⇒ Q f ∧ (All … Q args)
782  | Some r ⇒ Q r ∧ Q f ∧ (All … Q args)
783  ]
784| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
785| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
786| Swhile e sub ⇒ Q e ∧ P sub
787| Sdowhile e sub ⇒ Q e ∧ P sub
788| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
789| Sbreak ⇒ True
790| Scontinue ⇒ True
791| Sreturn r ⇒
792  match r with
793  [ None ⇒ True
794  | Some r ⇒ Q r ]
795| Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P)
796| Slabel _ sub ⇒ P sub
797| Sgoto _ ⇒ True
798| Scost _ sub ⇒ P sub
799]
800and substatement_ls ls (P : statement → Prop) : Prop ≝
801match ls with
802[ LSdefault sub ⇒ P sub
803| LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P)
804].
805
806(* -----------------------------------------------------------------------------
807   Freshness conservation results on switch removal.
808   ---------------------------------------------------------------------------- *)
809
810(* Similar stuff in toCminor.ma. *)
811lemma fresh_for_univ_still_fresh :
812   ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'.
813* #p * #i #H1 #v * #p' lapply H1 normalize
814#H1 #H2 destruct (H2) /2/ qed.
815
816lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'.
817#u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh)
818cases (fresh SymbolTag u)
819#fv #u' #H %{fv} %{u'} @conj try // @H //
820qed.
821
822lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)).
823#e #exit #ls @(branches_ind … ls)
824[ 1: #st #u #i #Hfresh normalize
825     lapply (fresh_for_univ_still_fresh … Hfresh)
826     cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize //
827| 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize
828     lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) *
829     #subcond #sublabel #u1 #Hfresh1 normalize
830     lapply (fresh_for_univ_still_fresh … Hfresh1)
831     cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize //
832] qed.
833
834lemma simplify_switch_fresh : ∀u,i,e,ls.
835 fresh_for_univ ? i u →
836 fresh_for_univ ? i (\snd (simplify_switch e ls u)).
837#u #i #e #ls #Hfresh
838normalize
839lapply (fresh_for_univ_still_fresh … Hfresh)
840cases (fresh ? u)
841#exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux
842normalize lapply (produce_cond_fresh e exit_label ls … Haux)
843elim (produce_cond ????) * #stm #label #uv2 normalize nodelta //
844qed.
845
846(*
847lemma switch_removal_fresh : ∀i,s,u.
848    fresh_for_univ ? i u →
849    fresh_for_univ ? i (\snd (switch_removal s u)).
850#i #s @(statement_ind2 ? (λls. ∀u. fresh_for_univ ? i u →
851                                      fresh_for_univ ? i (\snd (switch_removal_branches ls u))) … s)
852try //
853[ 1: #s1' #s2' #Hind1 #Hind2 #u #Hyp
854     whd in match (switch_removal (Ssequence s1' s2') u);
855     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
856     * #irr1 #irr2 #uA #HuA normalize nodelta
857     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
858     * #irr3 #irr4 #uB #HuB normalize nodelta //
859| 2: #e #s1' #s2' #Hind1 #Hind2 #u #Hyp
860     whd in match (switch_removal (Sifthenelse e s1' s2') u);
861     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
862     * #irr1 #irr2 #uA #HuA normalize nodelta
863     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
864     * #irr3 #irr4 #uB #HuB normalize nodelta //
865| 3,4: #e #s' #Hind #u #Hyp
866     whd in match (switch_removal ? u);
867     lapply (Hind u Hyp) elim (switch_removal s' u)
868     * #irr1 #irr2 #uA #HuA normalize nodelta //
869| 5: #s1' #e #s2' #s3' #Hind1 #Hind2 #Hind3 #u #Hyp
870     whd in match (switch_removal (Sfor s1' e s2' s3') u);
871     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
872     * #irr1 #irr2 #uA #HuA normalize nodelta
873     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
874     * #irr3 #irr4 #uB #HuB normalize nodelta
875     lapply (Hind3 uB HuB) elim (switch_removal s3' uB)
876     * #irr5 #irr6 #uC #HuC normalize nodelta //
877| 6: #e #ls #Hind #u #Hyp
878     whd in match (switch_removal (Sswitch e ls) u);
879     lapply (Hind u Hyp)
880     cases (switch_removal_branches ls u)
881     * #irr1 #irr2 #uA #HuA normalize nodelta
882     lapply (fresh_for_univ_still_fresh … HuA)
883     cases (fresh SymbolTag uA) #v #uA' #Haux lapply (Haux v uA' (refl ? 〈v,uA'〉))
884     -Haux #HuA' normalize nodelta
885     lapply (simplify_switch_fresh uA' i (Expr (Evar v) (typeof e)) irr1 HuA')
886     cases (simplify_switch ???) #stm #uB
887     #Haux normalize nodelta //
888| 7,8: #label #body #Hind #u #Hyp
889     whd in match (switch_removal ? u);
890     lapply (Hind u Hyp) elim (switch_removal body u)
891     * #irr1 #irr2 #uA #HuA normalize nodelta //
892| 9: #defcase #Hind #u #Hyp whd in match (switch_removal_branches ??);
893     lapply (Hind u Hyp) elim (switch_removal defcase u)
894     * #irr1 #irr2 #uA #HuA normalize nodelta //
895| 10: #sz #i0 #s0 #tl #Hind1 #Hind2 #u #Hyp normalize
896     lapply (Hind2 u Hyp) elim (switch_removal_branches tl u)
897     * #irr1 #irr2 #uA #HuA normalize nodelta
898     lapply (Hind1 uA HuA) elim (switch_removal s0 uA)
899     * #irr3 #irr4 #uB #HuB //
900] qed.
901
902lemma switch_removal_branches_fresh : ∀i,ls,u.
903    fresh_for_univ ? i u →
904    fresh_for_univ ? i (\snd (switch_removal_branches ls u)).
905#i #ls @(labeled_statements_ind2 (λs. ∀u. fresh_for_univ ? i u →
906                                           fresh_for_univ ? i (\snd (switch_removal s u))) ? … ls)
907try /2 by switch_removal_fresh/
908[ 1: #s #Hind #u #Hfresh normalize lapply (switch_removal_fresh ? s ? Hfresh)
909     cases (switch_removal s u) * //
910| 2: #sz #i #s #tl #Hs #Htl #u #Hfresh normalize
911     lapply (Htl u Hfresh)
912     cases (switch_removal_branches tl u) * normalize nodelta
913     #ls' #fvs #u' #Hfresh'
914     lapply (Hs u' Hfresh')
915     cases (switch_removal s u') * //
916] qed.
917*)
918(* -----------------------------------------------------------------------------
919   Simulation proof and related voodoo.
920   ----------------------------------------------------------------------------*)
921
922definition expr_lvalue_ind_combined ≝
923λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
924conj ??
925 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
926 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
927 
928let rec expr_ind2
929    (P : expr → Prop) (Q : expr_descr → type → Prop)
930    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
931    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
932    (Iconst_float : ∀f, t. Q (Econst_float f) t)
933    (Ivar : ∀id, t. Q (Evar id) t)
934    (Ideref : ∀e, t. P e → Q (Ederef e) t)
935    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
936    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
937    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
938    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t) 
939    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
940    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
941    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
942    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
943    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
944    (Icost : ∀c,e,t. P e → Q (Ecost c e) t)
945    (e : expr) on e : P e ≝
946match e with
947[ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ]
948
949and expr_desc_ind2
950    (P : expr → Prop) (Q : expr_descr → type → Prop)
951    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
952    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
953    (Iconst_float : ∀f, t. Q (Econst_float f) t)
954    (Ivar : ∀id, t. Q (Evar id) t)
955    (Ideref : ∀e, t. P e → Q (Ederef e) t)
956    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
957    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
958    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
959    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t) 
960    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
961    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
962    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
963    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
964    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
965    (Icost : ∀c,e,t. P e → Q (Ecost c e) t)
966    (ed : expr_descr) (t : type) on ed : Q ed t ≝
967match ed with
968[ Econst_int sz i ⇒ Iconst_int sz i t
969| Econst_float f ⇒ Iconst_float f t
970| Evar id ⇒ Ivar id t
971| Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
972| Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
973| Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
974| Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
975| Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
976| Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
977| Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
978| Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
979| Esizeof sizeoft ⇒ Isizeof sizeoft t
980| Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
981| Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e)
982].
983
984
985(* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched
986   by a non-constant number of evaluations in the converted program. More precisely,
987   [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps
988   necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *)
989   
990(* A version of simplify_switch hiding the ugly projs *)
991definition fresh_for_expression ≝
992λe,u. fresh_for_univ SymbolTag (max_of_expr e) u.
993
994definition fresh_for_statement ≝
995λs,u. fresh_for_univ SymbolTag (max_of_statement s) u.
996
997(* needed during mutual induction ... *)
998definition fresh_for_labeled_statements ≝
999λls,u. fresh_for_univ ? (max_of_ls ls) u.
1000   
1001definition fresh_for_function ≝
1002λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.
1003
1004(* misc properties of the max function on positives. *)
1005
1006lemma max_one_neutral : ∀v. max v one = v.
1007* // qed.
1008
1009lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v.
1010* #p whd in ⊢ (??%?); >max_one_neutral // qed.
1011
1012lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1.
1013* #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%);
1014>commutative_max // qed.
1015
1016lemma transitive_le : transitive ? le. // qed.
1017
1018lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
1019#a #b /2/ qed.
1020
1021(* cycle of length 1 *)
1022lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
1023* /2 by absurd/ qed.
1024
1025(* cycle of length 2 *)
1026lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False.
1027#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2))
1028#Heq @(le_S_contradiction_1 a) destruct // qed.
1029
1030(* cycle of length 3 *)
1031lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False.
1032#a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4
1033@(le_S_contradiction_2 … H3 H4)
1034qed.
1035
1036lemma reflexive_leb : ∀a. leb a a = true.
1037#a @(le_to_leb_true a a) // qed.
1038
1039(* This should be somewhere else. *)
1040lemma associative_max : associative ? max.
1041#a #b #c
1042whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
1043lapply (pos_compare_to_Prop a b)
1044cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
1045[ 1: >(le_to_leb_true a b) normalize nodelta /2/
1046     lapply (pos_compare_to_Prop b c)
1047     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1048     [ 1: >(le_to_leb_true b c) normalize nodelta
1049          lapply (pos_compare_to_Prop a c)
1050          cases (pos_compare a c) whd in ⊢ (% → ?); #Hac
1051          [ 1: >(le_to_leb_true a c) /2/
1052          | 2: destruct cases (leb c c) //
1053          | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *)
1054               @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac))           
1055          ]
1056          @le_S_weaken //
1057     | 2: destruct
1058          cases (leb c c) normalize nodelta
1059          >(le_to_leb_true a c) /2/
1060     | 3: >(not_le_to_leb_false b c) normalize nodelta /2/
1061          >(le_to_leb_true a b) /2/
1062     ]
1063| 2: destruct (Hab) >reflexive_leb normalize nodelta
1064     lapply (pos_compare_to_Prop b c)
1065     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1066     [ 1: >(le_to_leb_true b c) normalize nodelta
1067          >(le_to_leb_true b c) normalize nodelta
1068          /2/
1069     | 2: destruct >reflexive_leb normalize nodelta
1070          >reflexive_leb //
1071     | 3: >(not_le_to_leb_false b c) normalize nodelta
1072          >reflexive_leb /2/ ]
1073| 3: >(not_le_to_leb_false a b) normalize nodelta /2/
1074     lapply (pos_compare_to_Prop b c)
1075     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1076     [ 1: >(le_to_leb_true b c) normalize nodelta /2/
1077     | 2: destruct >reflexive_leb normalize nodelta @refl
1078     | 3: >(not_le_to_leb_false b c) normalize nodelta
1079          >(not_le_to_leb_false a b) normalize nodelta
1080          >(not_le_to_leb_false a c) normalize nodelta
1081          lapply (transitive_le … Hbc (le_S_weaken … Hab))
1082          #Hca /2/
1083     ]
1084] qed.   
1085
1086lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3).
1087* #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max //
1088qed.
1089(*
1090lemma max_of_expr_rewrite :
1091  ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id.
1092@(expr_ind2 … (λed,t. ∀id. max_of_expr (Expr ed t) id=max_id (max_of_expr (Expr ed t) (an_identifier SymbolTag one)) id))
1093[ 1: #ed #t // ]
1094[ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
1095| 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
1096#ty
1097[ 3: * #id_p whd in match (max_of_expr ??); cases var_id #var_p normalize nodelta
1098     whd in match (max_id ??) in ⊢ (???%);
1099     >max_one_neutral // ]
1100[ 1,2,11: * * //
1101| 3,4,5,7,13: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); @Hind
1102| 6,9,10: #Hind1 #Hind2 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
1103     >(Hind1 (max_of_expr e2 (an_identifier SymbolTag one)))
1104     >max_id_associative
1105     >Hind1
1106     cases (max_of_expr e1 ?)
1107     #v1 <Hind2 @refl
1108| 8: #Hind1 #Hind2 #Hind3 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
1109     >Hind1 in ⊢ (??%?); >Hind2 in ⊢ (??%?); >Hind3 in ⊢ (??%?);
1110     >Hind1 in ⊢ (???%); >Hind2 in ⊢ (???%);
1111     >max_id_associative >max_id_associative @refl
1112| 12: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
1113      cases field #p normalize nodelta
1114      >Hind cases (max_of_expr e1 ?) #e'
1115      cases id #id'
1116      whd in match (max_id ??); normalize nodelta
1117      whd in match (max_id ??); >associative_max @refl
1118] qed.
1119*)
1120lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u.
1121* #a * #b * #u normalize
1122lapply (pos_compare_to_Prop a b)
1123cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
1124[ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/
1125| 2: destruct >reflexive_leb /2/
1126| 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/
1127] qed.
1128
1129(* Auxilliary commutation lemma used in [substatement_fresh]. *)
1130
1131lemma foldl_max : ∀l,a,b.
1132  foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l =
1133  max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l).
1134#l elim l
1135[ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl
1136| 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%);
1137     <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
1138] qed.
1139
1140(* -----------------------------------------------------------------------------
1141   Stuff on memory and environments extensions.
1142   Let us recap: the memory model of a function is in two layers. An environment
1143   (type [env]) maps identifiers to blocks, and a memory maps blocks
1144   switch_removal introduces new, fresh variables. What is to be noted is that
1145   switch_removal modifies both the contents of the "disjoint" part of memory, but
1146   also where the data is allocated. The first solution considered was to consider
1147   an extensional equivalence relation on values, saying that equivalent pointers
1148   point to equivalent values. This has to be a coinductive relation, in order to
1149   take into account cyclic data structures. Rather than using coinductive types,
1150   we use the compcert solution, using so-called memory embeddings.
1151   ---------------------------------------------------------------------------- *)
1152
1153(* ---------------- *)
1154(* auxillary lemmas *)
1155lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
1156#a #b #HA
1157lapply (Zltb_true_to_Zlt … HA) #HA_prop
1158@Zlt_to_Zltb_true /2/
1159qed.
1160
1161lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
1162#a @Zlt_to_Zltb_true /2/ qed.
1163
1164
1165definition le_offset : offset → offset → bool ≝
1166  λx,y. Zleb (offv x) (offv y).
1167 
1168lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
1169
1170lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
1171
1172(* When equality on A is decidable, [mem A elt l] is too. *)
1173lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
1174#A #dec #elt #l elim l
1175[ 1: normalize %2 /2/
1176| 2: #hd #tl #Hind
1177     elim (dec elt hd)
1178     [ 1: #Heq >Heq %1 /2/
1179     | 2: #Hneq cases Hind
1180        [ 1: #Hmem %1 /2/
1181        | 2: #Hnmem %2 normalize
1182              % #H cases H
1183              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
1184              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
1185] ] ]
1186qed.
1187
1188lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
1189#a #b @(eq_block_elim … a b) /2/ qed.
1190
1191lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
1192#l #elt1 #elt2 elim l
1193[ 1: normalize #Habsurd @(False_ind … Habsurd)
1194| 2: #hd #tl #Hind normalize #Hl #Hr
1195   cases Hl
1196   [ 1: #Heq >Heq
1197        @(eq_block_elim … hd elt2)
1198        [ 1: #Heq >Heq /2 by not_to_not/
1199        | 2: #x @x ]
1200   | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
1201        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
1202        | 2: #Hmem2 @Hind //
1203        ]
1204   ]
1205] qed.
1206
1207lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
1208#b1 #b2 * #Hb
1209@(eq_block_elim … b1 b2)
1210[ 1: #Habsurd @(False_ind … (Hb Habsurd))
1211| 2: // ] qed.
1212
1213(* Type of blocks in a particular region. *)
1214definition block_in : region → Type[0] ≝ λrg. Σb. (block_region b) = rg.
1215
1216(* An embedding is a function from blocks to (blocks+offset). *)
1217definition embedding ≝ block → option (block × offset).
1218
1219definition offset_plus : offset → offset → offset ≝
1220  λo1,o2. mk_offset (offv o1 + offv o2).
1221 
1222lemma offset_plus_O : ∀o. offset_plus o (mk_offset OZ) = o.
1223* #z normalize // qed.
1224
1225(* Translates a pointer through an embedding. *)
1226definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
1227λp,E.
1228match p with
1229[ mk_pointer pblock poff ⇒
1230   match E pblock with
1231   [ None ⇒ None ?
1232   | Some loc ⇒
1233    let 〈dest_block,dest_off〉 ≝ loc in
1234    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
1235    Some ? ptr
1236   ]
1237].
1238
1239(* We parameterise the "equivalence" relation on values with an embedding. *)
1240(* Front-end values. *)
1241inductive value_eq (E : embedding) : val → val → Prop ≝
1242| undef_eq : ∀v.
1243  value_eq E Vundef v
1244| vint_eq : ∀sz,i.
1245  value_eq E (Vint sz i) (Vint sz i)
1246| vfloat_eq : ∀f.
1247  value_eq E (Vfloat f) (Vfloat f)
1248| vnull_eq :
1249  value_eq E Vnull Vnull
1250| vptr_eq : ∀p1,p2.
1251  pointer_translation p1 E = Some ? p2 →
1252  value_eq E (Vptr p1) (Vptr p2).
1253
1254(* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t.
1255 * the values are equivalent. *)
1256definition load_sim ≝
1257λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
1258 ∀b1,off1,b2,off2,ty,v1.
1259  valid_block m1 b1 →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
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
1264definition load_sim_ptr ≝
1265λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
1266 ∀b1,off1,b2,off2,ty,v1.
1267  valid_pointer m1 (mk_pointer b1 off1) = true →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
1268  pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →
1269  load_value_of_type ty m1 b1 off1 = Some ? v1 →
1270  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
1271
1272(* Definition of a memory injection *)
1273record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
1274{ (* Load simulation *)
1275  mi_inj : load_sim_ptr E m1 m2;
1276  (* Invalid blocks are not mapped *)
1277  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
1278  (* Valid pointers are mapped to valid pointers*)
1279  mi_valid_pointers : ∀p,p'.
1280                       valid_pointer m1 p = true →
1281                       pointer_translation p E = Some ? p' →
1282                       valid_pointer m2 p' = true;
1283  (* Blocks in the codomain are valid *)
1284  (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)
1285  (* Regions are preserved *)
1286  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
1287  (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.
1288   * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where
1289   * all variables are allocated in the same block. *)
1290  mi_disjoint : ∀b1,b2,b1',b2',o1',o2'.
1291                b1 ≠ b2 →
1292                E b1 = Some ? 〈b1',o1'〉 →
1293                E b2 = Some ? 〈b2',o2'〉 →
1294                b1' ≠ b2'
1295}.
1296
1297(* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\
1298 * A memory extension is a [memory_inj] with some particular blocks designated as
1299 * being writeable. *)
1300
1301alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
1302
1303record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
1304{ me_inj : memory_inj E m1 m2;
1305  (* A list of blocks where we can write freely *)
1306  me_writeable : list block;
1307  (* These blocks are valid *)
1308  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
1309  (* And pointers to m1 are oblivious to these blocks *)
1310  me_writeable_ok : ∀p,p'.
1311                     valid_pointer m1 p = true →
1312                     pointer_translation p E = Some ? p' →
1313                     ¬ (meml ? (pblock p') me_writeable)
1314}.
1315
1316(* ---------------------------------------------------------------------------- *)
1317(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
1318
1319(* A particular inversion. *)
1320lemma value_eq_ptr_inversion :
1321  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
1322#E #p1 #v #Heq inversion Heq
1323[ 1: #v #Habsurd destruct (Habsurd)
1324| 2: #sz #i #Habsurd destruct (Habsurd)
1325| 3: #f #Habsurd destruct (Habsurd)
1326| 4:  #Habsurd destruct (Habsurd)
1327| 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
1328     %{p2} @conj try @refl try assumption
1329] qed.
1330
1331(* A cleaner version of inversion for [value_eq] *)
1332lemma value_eq_inversion :
1333  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
1334  (∀v. P Vundef v) →
1335  (∀sz,i. P (Vint sz i) (Vint sz i)) →
1336  (∀f. P (Vfloat f) (Vfloat f)) →
1337  (P Vnull Vnull) →
1338  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
1339  P v1 v2.
1340#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
1341inversion Heq
1342[ 1: #v #Hv1 #Hv2 #_ destruct @H1
1343| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
1344| 3: #f #Hv1 #Hv2 #_ destruct @H3
1345| 4: #Hv1 #Hv2 #_ destruct @H4
1346| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
1347 
1348(* If we succeed to load something by value from a 〈b,off〉 location,
1349   [b] is a valid block. *)
1350lemma load_by_value_success_valid_block_aux :
1351  ∀ty,m,b,off,v.
1352    access_mode ty = By_value (typ_of_type ty) →
1353    load_value_of_type ty m b off = Some ? v →
1354    Zltb (block_id b) (nextblock m) = true.
1355#ty #m * #brg #bid #off #v
1356cases ty
1357[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1358| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1359whd in match (load_value_of_type ????);
1360[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
1361#Hmode
1362[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
1363     normalize in match (typesize ?);
1364     whd in match (loadn ???);
1365     whd in match (beloadv ??);
1366     cases (Zltb bid (nextblock m)) normalize nodelta
1367     try // #Habsurd destruct (Habsurd)
1368| *: normalize in Hmode; destruct (Hmode)
1369] qed.
1370
1371(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
1372lemma load_by_value_success_valid_ptr_aux :
1373  ∀ty,m,b,off,v.
1374    access_mode ty = By_value (typ_of_type ty) →
1375    load_value_of_type ty m b off = Some ? v →
1376    Zltb (block_id b) (nextblock m) = true ∧
1377    Zleb (low_bound m b) (offv off) = true ∧
1378    Zltb (offv off) (high_bound m b) = true.
1379#ty #m * #brg #bid #off #v
1380cases ty
1381[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1382| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1383whd in match (load_value_of_type ????);
1384[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
1385#Hmode
1386[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
1387     normalize in match (typesize ?);
1388     whd in match (loadn ???);
1389     whd in match (beloadv ??);
1390     cases (Zltb bid (nextblock m)) normalize nodelta
1391     cases (Zleb (low (blocks m (mk_block brg bid))) (offv off))
1392     cases (Zleb (low (blocks m (mk_block brg bid))) (offv off))
1393     cases (Zltb (offv off) (high (blocks m (mk_block brg bid)))) normalize nodelta
1394     #Heq destruct (Heq)
1395     try /3 by conj, refl/
1396| *: normalize in Hmode; destruct (Hmode)
1397] qed.
1398
1399
1400lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
1401* #rg #id #m normalize
1402elim id /2/ qed.
1403
1404lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
1405* #rg #id #m normalize
1406elim id /2/ qed.
1407
1408lemma load_by_value_success_valid_block :
1409  ∀ty,m,b,off,v.
1410    access_mode ty = By_value (typ_of_type ty) →
1411    load_value_of_type ty m b off = Some ? v →
1412    valid_block m b.
1413#ty #m #b #off #v #Haccess_mode #Hload
1414@valid_block_from_bool
1415elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
1416qed.
1417
1418lemma load_by_value_success_valid_pointer :
1419  ∀ty,m,b,off,v.
1420    access_mode ty = By_value (typ_of_type ty) →
1421    load_value_of_type ty m b off = Some ? v →
1422    valid_pointer m (mk_pointer b off).
1423#ty #m #b #off #v #Haccess_mode #Hload normalize
1424elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
1425* #H1 #H2 #H3 >H1 >H2 normalize nodelta
1426>Zle_to_Zleb_true try //
1427lapply (Zlt_to_Zle … (Zltb_true_to_Zlt … H3)) /2/
1428qed.
1429
1430
1431(* Making explicit the contents of memory_inj for load_value_of_type *)
1432lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
1433    memory_inj E m1 m2 →
1434    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
1435    load_value_of_type ty m1 b1 off1 = Some ? v1 →
1436    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
1437#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
1438lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
1439lapply (refl ? (access_mode ty))
1440cases ty
1441[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1442| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1443normalize in ⊢ ((???%) → ?); #Hmode #Hyp
1444[ 1,7,8: normalize in Hyp; destruct (Hyp)
1445| 5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
1446lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
1447lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
1448qed.     
1449
1450
1451(* -------------------------------------- *)
1452(* Lemmas pertaining to memory allocation *)
1453
1454(* A valid block stays valid after an alloc. *)
1455lemma alloc_valid_block_conservation :
1456  ∀m,m',z1,z2,r,new_block.
1457  alloc m z1 z2 r = 〈m', new_block〉 →
1458  ∀b. valid_block m b → valid_block m' b.
1459#m #m' #z1 #z2 #r * #b' #Hregion_eq
1460elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
1461#Halloc destruct (Halloc)
1462#b whd in match (valid_block ??) in ⊢ (% → %); /2/
1463qed.
1464
1465(* Allocating a new zone produces a valid block. *)
1466lemma alloc_valid_new_block :
1467  ∀m,m',z1,z2,r,new_block.
1468  alloc m z1 z2 r = 〈m', new_block〉 →
1469  valid_block m' new_block.
1470* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
1471whd in match (alloc ????); whd in match (valid_block ??);
1472#Halloc destruct (Halloc) /2/
1473qed.
1474
1475(* All data in a valid block is unchanged after an alloc. *)
1476lemma alloc_beloadv_conservation :
1477  ∀m,m',block,offset,z1,z2,r,new_block.
1478    valid_block m block →
1479    alloc m z1 z2 r = 〈m', new_block〉 →
1480    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
1481* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
1482whd in Halloc:(??%?); destruct (Halloc)
1483whd in match (beloadv ??) in ⊢ (??%%);
1484lapply (valid_block_to_bool … Hvalid) #Hlt
1485>Hlt >(zlt_succ … Hlt)
1486normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
1487cut (eqZb (block_id block) next = false)
1488[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
1489>Hneq cases (eq_region ??) normalize nodelta  @refl
1490qed.
1491
1492(* Lift [alloc_beloadv_conservation] to loadn *)
1493lemma alloc_loadn_conservation :
1494  ∀m,m',z1,z2,r,new_block.
1495    alloc m z1 z2 r = 〈m', new_block〉 →
1496    ∀n. ∀block,offset.
1497    valid_block m block →
1498    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
1499#m #m' #z1 #z2 #r #new_block #Halloc #n
1500elim n try //
1501#n' #Hind #block #offset #Hvalid_block
1502whd in ⊢ (??%%);
1503>(alloc_beloadv_conservation … Hvalid_block Halloc)
1504cases (beloadv m' (mk_pointer block offset)) //
1505#bev normalize nodelta
1506whd in match (shift_pointer ???); >Hind try //
1507qed.
1508
1509(* Memory allocation preserves [memory_inj] *)
1510lemma alloc_memory_inj :
1511  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1512  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1513  memory_inj E m1 m2'.
1514#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
1515%
1516[ 1:
1517  whd
1518  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1519  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
1520  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
1521  lapply (refl ? (access_mode ty))
1522  cases ty in Hload_eq;
1523  [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1524  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1525  #Hload normalize in ⊢ ((???%) → ?); #Haccess
1526  [ 1,7,8: normalize in Hload; destruct (Hload)
1527  | 2,3,4,9: whd in match (load_value_of_type ????);
1528     whd in match (load_value_of_type ????);
1529     lapply (load_by_value_success_valid_block … Haccess Hload)
1530     #Hvalid_block
1531     whd in match (load_value_of_type ????) in Hload;
1532     <(alloc_loadn_conservation … Halloc … Hvalid_block)
1533     @Hload
1534  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
1535| 2: @(mi_freeblock … Hmemory_inj)
1536| 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
1537     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
1538     elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
1539     whd in match (valid_pointer ??) in ⊢ (% → %);
1540     @Zltb_elim_Type0
1541     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
1542     #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
1543     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
1544     whd in match (high_bound ??) in ⊢ (% → %);
1545     whd in match (update_block ?????);
1546     whd in match (eq_block ??);
1547     cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
1548     #Hbid_neq >Hbid_neq
1549     cases (eq_region br' r) normalize #H @H
1550| 4: @(mi_region … Hmemory_inj)
1551| 5: @(mi_disjoint … Hmemory_inj)
1552] qed.
1553
1554(* Memory allocation induces a memory extension. *)
1555lemma alloc_memory_ext :
1556  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1557  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1558  memory_ext E m1 m2'.
1559#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
1560lapply (alloc_memory_inj … Hmemory_inj Halloc)
1561#Hinj' %
1562[ 1: @Hinj'
1563| 2: @[new_block]
1564| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
1565      #Heq destruct (Heq) whd elim m2 in Halloc;
1566      #Hcontents #nextblock #Hnextblock
1567      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1568      /2/
1569| 4: * #b #o * #b' #o' #Hvalid_ptr #Hembed %
1570     normalize in ⊢ (% → ?); * [ 2: #H @H ]
1571     #Heq destruct (Heq)
1572     lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed)
1573     whd in ⊢ (% → ?);
1574     (* contradiction because ¬ (valid_block m2 new_block)  *)
1575     elim m2 in Halloc;
1576     #contents_m2 #nextblock_m2 #Hnextblock_m2
1577     whd in ⊢ ((??%?) → ?);
1578     #Heq_alloc destruct (Heq_alloc)
1579     normalize
1580     lapply (irreflexive_Zlt nextblock_m2)
1581     @Zltb_elim_Type0
1582     [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd)
1583] qed.
1584
1585lemma bestorev_beloadv_conservation :
1586  ∀mA,mB,wb,wo,v.
1587    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1588    ∀rb,ro. eq_block wb rb = false →
1589    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
1590#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
1591whd in ⊢ (??%%);
1592elim mB in Hstore; #contentsB #nextblockB #HnextblockB
1593normalize in ⊢ (% → ?);
1594cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
1595[ 2: #Habsurd destruct (Habsurd) ]
1596cases (if Zleb (low (blocks mA wb)) (offv wo) 
1597       then Zltb (offv wo) (high (blocks mA wb)) 
1598       else false) normalize nodelta
1599[ 2: #Habsurd destruct (Habsurd) ]
1600#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
1601cases rr cases wr normalize try //
1602@(eqZb_elim … rid wid)
1603[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
1604try //
1605qed.
1606
1607(* lift [bestorev_beloadv_conservation to [loadn] *)
1608lemma bestorev_loadn_conservation :
1609  ∀mA,mB,n,wb,wo,v.
1610    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1611    ∀rb,ro. eq_block wb rb = false →
1612    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
1613#mA #mB #n
1614elim n
1615[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
1616| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
1617     whd in ⊢ (??%%);
1618     >(bestorev_beloadv_conservation … Hstore … Hneq)
1619     >(Hind … Hstore … Hneq) @refl
1620] qed.
1621
1622(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
1623lemma bestorev_load_value_of_type_conservation :
1624  ∀mA,mB,wb,wo,v.
1625    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1626    ∀rb,ro. eq_block wb rb = false →
1627    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1628#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
1629cases ty
1630[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1631| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //
1632[ 1: elim sz | 2: elim fsz | 3: | 4: ]
1633whd in ⊢ (??%%);
1634>(bestorev_loadn_conservation … Hstore … Hneq) @refl
1635qed.
1636
1637(* Writing in the "extended" part of a memory preserves the underlying injection *)
1638lemma bestorev_memory_ext_to_load_sim :
1639  ∀E,mA,mB,mC.
1640  ∀Hext:memory_ext E mA mB.
1641  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1642  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1643  load_sim_ptr E mA mC.
1644#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
1645#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1646(* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *)
1647lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2
1648lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
1649cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
1650<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
1651@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
1652qed.
1653
1654(* Writing in the "extended" part of a memory preserves the whole memory injection *)
1655lemma bestorev_memory_ext_to_memory_inj :
1656  ∀E,mA,mB,mC.
1657  ∀Hext:memory_ext E mA mB.
1658  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1659  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1660  memory_inj E mA mC.
1661#E #mA * #contentsB #nextblockB #HnextblockB #mC
1662#Hext #wb #wo #v #Hwb #Hstore
1663%
1664[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
1665elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
1666#Hmem
1667[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint
1668whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
1669normalize in ⊢ (% → ?); #Hlt_wb
1670#p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain
1671normalize in match (valid_pointer ??) in ⊢ (% → %);
1672>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
1673cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
1674normalize nodelta
1675[ 2: #Habsurd destruct (Habsurd) ]
1676#Heq destruct (Heq)
1677cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta
1678[ 2: // ]
1679whd in match (update_block ?????);
1680cut (eq_block (pblock p') wb = false)
1681[ 2: #Heq >Heq normalize nodelta #H @H ]
1682@neq_block_eq_block_false @sym_neq
1683@(mem_not_mem_neq writeable … Hmem)
1684@(Hwriteable_ok … HvalidA Hembed)
1685qed.
1686
1687(* It even preserves memory extensions, with the same writeable blocks.  *)
1688lemma bestorev_memory_ext_to_memory_ext :
1689  ∀E,mA,mB.
1690  ∀Hext:memory_ext E mA mB.
1691  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1692  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
1693  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
1694#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
1695%{(mk_memory_ext …
1696      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
1697      (me_writeable … Hext)
1698      ?
1699      (me_writeable_ok … Hext)
1700 )} try @refl
1701#b #Hmemb
1702lapply (me_writeable_valid … Hext b Hmemb)
1703lapply (me_writeable_valid … Hext wb Hmem)
1704elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
1705lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
1706>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
1707cases (if Zleb (low (contentsB wb)) (offv wo) 
1708       then Zltb (offv wo) (high (contentsB wb)) 
1709       else false)
1710normalize [ 2: #Habsurd destruct (Habsurd) ]
1711#Heq destruct (Heq) @Hb_valid
1712qed.
1713
1714(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
1715lemma storen_memory_ext_to_memory_ext :
1716  ∀E,mA,l,mB,mC.
1717  ∀Hext:memory_ext E mA mB.
1718  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1719  storen mB (mk_pointer wb wo) l = Some ? mC →
1720  memory_ext E mA mC.
1721#E #mA #l elim l
1722[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
1723     @Hext
1724| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
1725     whd in ⊢ ((??%?) → ?);
1726     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
1727     cases (bestorev mB (mk_pointer wb wo) hd)
1728     normalize nodelta
1729     [ 1: #H #Habsurd destruct (Habsurd) ]
1730     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
1731     @(Hind … HextD … Hstore)
1732     <Heq @Hmem
1733] qed.     
1734
1735(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
1736lemma store_value_of_type_memory_ext_to_memory_ext :
1737  ∀E,mA,mB,mC.
1738  ∀Hext:memory_ext E mA mB.
1739  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1740  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
1741  memory_ext E mA mC.
1742#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
1743cases ty
1744[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1745| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1746whd in ⊢ ((??%?) → ?);
1747[ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
1748#Hstore
1749@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
1750qed.
1751
1752(* End of the memory injection-related stuff. *)
1753(* ------------------------------------------ *)
1754
1755(* Lookup functions in list environments (used to type local variables in functions) *)     
1756let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
1757match l with
1758[ nil ⇒ false
1759| cons hd tl ⇒
1760  let 〈id, ty〉 ≝ hd in
1761  match identifier_eq SymbolTag i id with
1762  [ inl Hid_eq ⇒ true
1763  | inr Hid_neq ⇒ mem_assoc_env i tl 
1764  ]
1765].
1766
1767let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝
1768match l with
1769[ nil ⇒ None ?
1770| cons hd tl ⇒
1771  let 〈id, ty〉 ≝ hd in
1772  match identifier_eq SymbolTag i id with
1773  [ inl Hid_eq ⇒ Some ? ty
1774  | inr Hid_neq ⇒ assoc_env i tl 
1775  ]
1776].
1777
1778(* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension
1779   of the environment [e1] s.t. the new binders are in [new], and such that those
1780   new binders are "writeable" in the memory extension [Hext] *)
1781definition disjoint_extension ≝
1782λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem).
1783λ(new : list (ident × type)). λ(E:embedding). λ(Hext: memory_ext E m1 m2).
1784  ∀id. match mem_assoc_env id new with
1785       [ true ⇒
1786           ∃b. lookup ?? e2 id = Some ? b
1787            ∧ meml ? b (me_writeable … Hext)
1788            ∧ lookup ?? e1 id = None ?
1789       | false ⇒
1790         match lookup ?? e1 id with
1791         [ None ⇒ lookup ?? e2 id = None ?
1792         | Some b1 ⇒
1793           match lookup ?? e2 id with
1794           [ None ⇒ False
1795           | Some b2 ⇒
1796             valid_block m1 b1 ∧
1797             value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))
1798           ]
1799         ]
1800       ].
1801
1802(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
1803 * the variable is not in a local environment, then we search into the global one.
1804 * A proper "extension" of a local environment should be such that the extension
1805 * does not collide with a given global env.
1806 * To see the details of why we need that, see [exec_lvalue'], Evar id case.
1807 *)
1808definition ext_fresh_for_genv ≝
1809λ(ext : list (ident × type)). λ(ge : genv).
1810  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.
1811
1812(* Any environment is a "disjoint" extension of itself with nothing. *)
1813(*
1814lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].
1815#e #m #ty #id
1816normalize in match (mem_assoc_env id []); normalize nodelta
1817cases (lookup ?? e id) try //
1818#b normalize nodelta
1819% #ty cases (load_value_of_type ????)
1820[ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj //
1821cases (assoc_env id ty) //
1822qed. *)
1823
1824
1825(* "generic" simulation relation on [res ?] *)
1826definition res_sim ≝
1827  λ(A : Type[0]).
1828  λ(eq : A → A → Prop).
1829  λ(r1, r2 : res A).
1830  ∀a1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2.
1831
1832(* Specialisation of [res_sim] to match [exec_expr] *)
1833definition exec_expr_sim ≝ λE.
1834  res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)).
1835
1836(* Specialisation of [res_sim] to match [exec_lvalue] *)
1837definition exec_lvalue_sim ≝ λE.
1838  res_sim (block × offset × trace)
1839    (λr1,r2.
1840      let 〈b1,o1,tr1〉 ≝ r1 in
1841      let 〈b2,o2,tr2〉 ≝ r2 in
1842      value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2).
1843
1844lemma 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.
1845#ty #m #b #o cases (load_value_of_type ty m b o)
1846[ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed.
1847
1848(*
1849lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'.
1850   env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
1851   〈f',vars〉 = function_switch_removal f →
1852   env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
1853   environment_extension env env' vars.
1854
1855#f #f'
1856cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append
1857cases (fn_params f) cases (fn_vars f)
1858[ 1: #vars >append_nil >append_nil >nil_append elim vars   
1859   [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct //
1860   | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq
1861        whd in ⊢ ((???(???%)) → ?);
1862 #Henv #Hswrem #Henv'
1863#id   
1864*)
1865
1866(*
1867lemma substatement_fresh : ∀s,u.
1868    fresh_for_statement s u →
1869    substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
1870#s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s)
1871try /by I/
1872[ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption
1873| 2: *
1874    [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
1875         #Hfresh_e #Hfresh_args @conj try assumption
1876         normalize nodelta in Hfresh_args;
1877         >max_id_commutative in Hfresh_args; >max_id_one_neutral
1878         #Hfresh_args         
1879    | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
1880         #Hfresh_e #H lapply (fresh_max_split ??? H) *
1881         #Hfresh_ret #Hfresh_args @conj try @conj try assumption ]
1882    elim args in Hfresh_args;
1883    [ 1,3: //
1884    | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???);
1885            >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj
1886            [ 1,3: @Hu
1887            | 2,4: @Hind assumption ] ]
1888| 3: #s1 #s2 #_ #_
1889     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
1890     whd in match (substatement_P ??); /2/
1891| 4: #e #cond #iftrue #iffalse #_
1892     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
1893     #Hexpr #H2 lapply (fresh_max_split … H2) * /2/
1894| 5,6: #e #stm #_
1895     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/
1896| 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) *
1897      #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond
1898      elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/
1899| 8: #ret #H whd elim ret in H; try //     
1900| 9: #expr #ls #Hind #H whd @conj
1901     [ 1: elim (fresh_max_split … H) //
1902     | 2: @Hind elim (fresh_max_split … H) // ]
1903| 10: #l #body #Hind #H whd elim (fresh_max_split … H) //
1904| 11: #sz #i #hd #tl #Hhd #Htl #H whd
1905     elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj //
1906     @Htl //
1907] qed.
1908*)
1909
1910(* Eliminating switches introduces fresh variables. [environment_extension] characterizes
1911 * a local environment extended by some local variables. *)
1912 
1913
1914(* lookup on environment extension *)
1915(*
1916lemma extension_lookup :
1917  ∀map, map', ext, id, result.
1918  environment_extension map map' ext →
1919  lookup ?? map id = Some ? result →
1920  lookup ?? map' id = Some ? result.
1921#map #map' #ext #id #result #Hext lapply (Hext id)
1922cases (mem_assoc_env ??) normalize nodelta
1923[ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd)
1924| 2: #H >H // ] qed.
1925
1926*)
1927
1928(* Extending a map by an empty list of variables yields an observationally equivalent
1929 * environment. *)
1930(*
1931lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'.
1932* #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H
1933[ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
1934     cases (lookup_opt block id map2) normalize
1935     [ 1: >H #H2 >H2 @refl
1936     | 2: #b >H cases v
1937          [ 1: normalize * #H @(False_ind … H)
1938          | 2: #block normalize // ] ]
1939| 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
1940     >H cases v normalize try //
1941     #block cases (lookup_opt ? id map1) normalize try //
1942     * #H @(False_ind … H)
1943] qed. *)
1944
1945(* If two identifier maps are observationally equal, then they contain the same bocks.
1946 * see maps_obsequiv.ma for the details of the proof. *)
1947(*
1948lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'.
1949* #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold
1950>Hfold @refl
1951qed.
1952*)
1953
1954(* Simulation relations. *)
1955inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
1956| swc_stop : ∀fvs.
1957    switch_cont_sim fvs Kstop Kstop
1958| swc_seq : ∀fvs,s,k,k',u,result.
1959    fresh_for_statement s u →
1960    switch_cont_sim fvs k k' →
1961    switch_removal s fvs u = Some ? result →
1962    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
1963| swc_while : ∀fvs,e,s,k,k',u,result.
1964    fresh_for_statement (Swhile e s) u →
1965    switch_cont_sim fvs k k' →
1966    switch_removal s fvs u = Some ? result →
1967    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
1968| swc_dowhile : ∀fvs,e,s,k,k',u,result.
1969    fresh_for_statement (Sdowhile e s) u →
1970    switch_cont_sim fvs k k' →
1971    switch_removal s fvs u = Some ? result →
1972    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
1973| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
1974    fresh_for_statement (Sfor Sskip e s1 s2) u →
1975    switch_cont_sim fvs k k' →
1976    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
1977    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
1978| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1979    fresh_for_statement (Sfor Sskip e s1 s2) u →
1980    switch_cont_sim fvs k k' →
1981    switch_removal s1 fvs u = Some ? result1 →
1982    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
1983    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
1984| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1985    fresh_for_statement (Sfor Sskip e s1 s2) u →
1986    switch_cont_sim fvs k k' →
1987    switch_removal s1 fvs u = Some ? result1 →
1988    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
1989    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
1990| swc_switch : ∀fvs,k,k'.
1991    switch_cont_sim fvs k k' →
1992    switch_cont_sim fvs (Kswitch k) (Kswitch k')
1993| swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
1994    switch_cont_sim fvs k k' →
1995    (* /!\ Update [en] with [fvs'] ... *)
1996    switch_cont_sim
1997      (map … (fst ??) (\snd (function_switch_removal f)))
1998      (Kcall r f en k)
1999      (Kcall r (\fst (function_switch_removal f)) en' k').
2000
2001
2002(*
2003 en' = exec_alloc_variables en m (\snd (function_switch_removal f))
2004 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
2005        variable dans en'.
2006
2007        1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que
2008           dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
2009           de savoir que :
2010           si je lookup une variable générée à partir d'un univers frais dans l'environement en',
2011           alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
2012           et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
2013           et à etre "(function_switch_removal f)-contained".
2014
2015        2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
2016           et l'update n'altèrent pas le comportement du reste du programme.
2017
2018        relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
2019                   depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
2020                   en particulier, si u est frais pour S1 u est frais pour S0.
2021
2022        Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
2023                    "environment_extension en en' (\fst (\fst (switch_removal s u)))"
2024                   
2025 ---------------------------------------------------------------
2026 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
2027   et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
2028   on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
2029   en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
2030*)
2031
2032inductive switch_state_sim : state → state → Prop ≝
2033| sws_state : ∀u,f,s,k,k',m,m',result.
2034    ∀env, env', f', vars.
2035    ∀E:embedding.   
2036    ∀Hext:memory_ext E m m'.
2037    fresh_for_statement s u →
2038    (*
2039    env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
2040    env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
2041    *)
2042    〈f',vars〉 = function_switch_removal f →
2043    disjoint_extension env m env' m' vars E Hext →
2044    switch_removal s (map ?? (fst ??) vars) u = Some ? result →
2045    switch_cont_sim (map ?? (fst ??) vars) k k' →
2046    switch_state_sim
2047      (State f s k env m)
2048      (State f' (ret_st ? result) k' env' m')
2049| sws_callstate : ∀vars, fd,args,k,k',m.
2050    switch_cont_sim vars k k' →
2051    switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m)
2052| sws_returnstate : ∀vars,res,k,k',m.
2053    switch_cont_sim vars k k' →
2054    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
2055| sws_finalstate : ∀r.
2056    switch_state_sim (Finalstate r) (Finalstate r).
2057
2058lemma call_cont_swremoval : ∀fv,k,k'.
2059  switch_cont_sim fv k k' →
2060  switch_cont_sim fv (call_cont k) (call_cont k').
2061#fv #k0 #k0' #K elim K /2/
2062qed.
2063
2064(* [eventually ge P s tr] states that after a finite number of [exec_step], the
2065   property P on states will be verified. *)
2066inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
2067| eventually_base : ∀s,t,s'.
2068    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
2069    P s' →
2070    eventually ge P s t
2071| eventually_step : ∀s,t,s',t',trace.
2072    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
2073    eventually ge P s' t' →
2074    trace = (t ⧺ t') →
2075    eventually ge P s trace.
2076
2077(* [eventually] is not so nice to use directly, we would like to make the mandatory
2078 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
2079   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
2080lemma eventually_now : ∀ge,P,s,t.
2081  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
2082   eventually ge P s t.
2083#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
2084qed.
2085(*   
2086lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
2087                                      ∃t'.eventually ge P s (t ⧺ t').
2088#ge #P #s #t * #s' * #Hexec #HP %{E0} normalize >(append_nil ? t) %1{????? Hexec HP}
2089qed.
2090*)
2091lemma eventually_later : ∀ge,P,s,t.
2092   (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) →
2093    eventually ge P s t.
2094#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
2095try assumption
2096qed.
2097
2098(* lift value_eq to option block *)
2099definition option_block_eq ≝ λE,ob1,ob2.
2100match ob1 with
2101[ None ⇒
2102  match ob2 with
2103  [ None ⇒ True
2104  | Some _ ⇒ False ]
2105| Some b1 ⇒
2106  match ob2 with
2107  [ None ⇒ False
2108  | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))  ]
2109].
2110
2111definition value_eq_opt ≝ λE,ov1,ov2.
2112match ov1 with
2113[ None ⇒
2114  match ov2 with
2115  [ None ⇒ True
2116  | Some _ ⇒ False ]
2117| Some v1 ⇒
2118  match ov2 with
2119  [ None ⇒ False
2120  | Some v2 ⇒
2121    value_eq E v1 v2 ]
2122].
2123
2124record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
2125  rg_find_symbol: ∀s.
2126    option_block_eq E (find_symbol ? ge s) (find_symbol ? ge' s);
2127  rg_find_funct: ∀v,f.
2128    find_funct ? ge v = Some ? f →
2129    find_funct ? ge' v = Some ? (t f);
2130  rg_find_funct_ptr: ∀b,f.
2131    find_funct_ptr ? ge b = Some ? f →
2132    find_funct_ptr ? ge' b = Some ? (t f)
2133}.
2134
2135lemma exec_lvalue_expr_elim :
2136  ∀E,r1,r2,Pok,Qok.
2137  ∀H:exec_lvalue_sim E r1 r2.
2138  (∀bo1,bo2,tr.
2139    let 〈b1,o1〉 ≝ bo1 in
2140    let 〈b2,o2〉 ≝ bo2 in
2141    value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) →
2142    match Pok 〈bo1,tr〉 with
2143    [ Error err ⇒ True
2144    | OK vt1 ⇒
2145      let 〈val1,trace1〉 ≝ vt1 in
2146      match Qok 〈bo2,tr〉 with
2147      [ Error err ⇒ False
2148      | OK vt2 ⇒
2149        let 〈val2,trace2〉 ≝ vt2 in
2150        trace1 = trace2 ∧ value_eq E val1 val2     
2151      ]
2152    ]) →
2153  exec_expr_sim E
2154    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
2155    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
2156#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
2157elim r1
2158[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
2159| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
2160     * #a2 * #Hr2 >Hr2 normalize nodelta
2161     elim a1 * #b1 #o1 #tr1
2162     elim a2 * #b2 #o2 #tr2 normalize nodelta
2163     * #Hvalue_eq #Htrace_eq #H2
2164     destruct (Htrace_eq)
2165     lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq)
2166     cases (Pok 〈b1, o1, tr2〉)
2167     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
2168     | 1: * #v1 #tr1' normalize nodelta #H3 whd
2169          * #v1' #tr1'' #Heq destruct (Heq)
2170          cases (Qok 〈b2,o2,tr2〉) in H3;
2171          [ 2: #error #Hfalse @(False_ind … Hfalse)
2172          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
2173               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
2174] ] ] qed.
2175
2176lemma exec_expr_expr_elim :
2177  ∀E,r1,r2,Pok,Qok.
2178  ∀H:exec_expr_sim E r1 r2.
2179  (∀v1,v2,trace.
2180    value_eq E v1 v2 →
2181    match Pok 〈v1,trace〉 with
2182    [ Error err ⇒ True
2183    | OK vt1 ⇒
2184      let 〈val1,trace1〉 ≝ vt1 in
2185      match Qok 〈v2,trace〉 with
2186      [ Error err ⇒ False
2187      | OK vt2 ⇒
2188        let 〈val2,trace2〉 ≝ vt2 in
2189        trace1 = trace2 ∧ value_eq E val1 val2     
2190      ]
2191    ]) →
2192  exec_expr_sim E
2193    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
2194    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
2195#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
2196elim r1
2197[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
2198| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
2199     * #a2 * #Hr2 >Hr2 normalize nodelta
2200     elim a1 #v1 #tr1
2201     elim a2 #v2 #tr2 normalize nodelta
2202     * #Hvalue_eq #Htrace_eq #H2
2203     destruct (Htrace_eq)
2204     lapply (H2 v1 v2 tr2 Hvalue_eq)
2205     cases (Pok 〈v1, tr2〉)
2206     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
2207     | 1: * #v1 #tr1' normalize nodelta #H3 whd
2208          * #v1' #tr1'' #Heq destruct (Heq)
2209          cases (Qok 〈v2,tr2〉) in H3;
2210          [ 2: #error #Hfalse @(False_ind … Hfalse)
2211          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
2212               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
2213] ] ] qed.
2214
2215(* Commutation results of standard binary operations with value_eq. *)
2216lemma unary_operation_value_eq :
2217  ∀E,op,v1,v2,ty.
2218   value_eq E v1 v2 →
2219   ∀r1.
2220   sem_unary_operation op v1 ty = Some ? r1 →
2221    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
2222#E #op #v1 #v2 #ty #Hvalue_eq #r1
2223inversion Hvalue_eq
2224[ 1: #v #Hv1 #Hv2 #_ destruct
2225     cases op normalize
2226     [ 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 ]
2227          normalize #Habsurd destruct (Habsurd)
2228     | 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 ]
2229          normalize #Habsurd destruct (Habsurd)
2230     | 2: #Habsurd destruct (Habsurd) ]
2231| 2: #vsz #i #Hv1 #Hv2 #_
2232     cases op
2233     [ 1: cases ty
2234          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2235          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
2236          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2237               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
2238               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
2239               //
2240          | *: #Habsurd destruct (Habsurd) ]
2241     | 2: whd in match (sem_unary_operation ???);     
2242          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
2243     | 3: whd in match (sem_unary_operation ???);
2244          cases ty
2245          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2246          normalize nodelta
2247          whd in ⊢ ((??%?) → ?);
2248          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2249               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
2250          | *: #Habsurd destruct (Habsurd) ] ]
2251| 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2252     cases op normalize nodelta
2253     [ 1: cases ty
2254          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2255          whd in match (sem_notbool ??);
2256          #Heq1 destruct
2257          cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
2258     | 2: normalize #Habsurd destruct (Habsurd)
2259     | 3: cases ty
2260          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2261          whd in match (sem_neg ??);
2262          #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
2263| 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2264     cases op normalize nodelta
2265     [ 1: cases ty
2266          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2267          whd in match (sem_notbool ??);
2268          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2269     | 2: normalize #Habsurd destruct (Habsurd)
2270     | 3: cases ty
2271          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2272          whd in match (sem_neg ??);
2273          #Heq1 destruct ]
2274| 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
2275     cases op normalize nodelta
2276     [ 1: cases ty
2277          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2278          whd in match (sem_notbool ??);         
2279          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2280     | 2: normalize #Habsurd destruct (Habsurd)
2281     | 3: cases ty
2282          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2283          whd in match (sem_neg ??);         
2284          #Heq1 destruct ]
2285]
2286qed.
2287
2288
2289(* value_eq lifts to addition *)
2290lemma add_value_eq :
2291  ∀E,v1,v2,v1',v2',ty1,ty2.
2292   value_eq E v1 v2 →
2293   value_eq E v1' v2' →
2294   (* memory_inj E m1 m2 →  This injection seems useless TODO *)
2295   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
2296           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2297#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2298@(value_eq_inversion E … Hvalue_eq1)
2299[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2300[ 1: whd in match (sem_add ????); normalize nodelta
2301     cases (classify_add ty1 ty2) normalize nodelta
2302     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
2303     #Habsurd destruct (Habsurd)
2304| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2305     cases (classify_add ty1 ty2) normalize nodelta     
2306     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2307     [ 2,3,5: #Habsurd destruct (Habsurd) ]
2308     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2309     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2310     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
2311     [ 1: @intsize_eq_elim_elim
2312          [ 1: #_ #Habsurd destruct (Habsurd)
2313          | 2: #Heq destruct (Heq) normalize nodelta
2314               #Heq destruct (Heq)
2315               /3 by ex_intro, conj, vint_eq/ ]
2316     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
2317          /3 by ex_intro, conj, vint_eq/
2318     | 3: #Heq destruct (Heq)
2319          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
2320          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
2321          @vptr_eq whd in match (pointer_translation ??);
2322          cases (E b1') in Hembed;
2323          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2324          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2325               whd in match (shift_pointer_n ????);
2326               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
2327                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i))
2328               [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ]
2329               #Heq >Heq @refl ]
2330     ]
2331| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2332     cases (classify_add ty1 ty2) normalize nodelta     
2333     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2334     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2335     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2336     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2337     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2338     #Heq destruct (Heq)
2339     /3 by ex_intro, conj, vfloat_eq/
2340| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2341     cases (classify_add ty1 ty2) normalize nodelta     
2342     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2343     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2344     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2345     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2346     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2347     @eq_bv_elim
2348     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2349     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2350| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2351     cases (classify_add ty1 ty2) normalize nodelta
2352     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2353     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2354     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2355     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2356     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2357     #Heq destruct (Heq)
2358     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
2359     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2360     elim p1 in Hembed; #b1 #o1 normalize nodelta
2361     cases (E b1)
2362     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2363     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2364          normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
2365          @refl
2366     ]
2367] qed.
2368
2369(* Offset subtraction is invariant by translation *)
2370lemma sub_offset_translation :
2371 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
2372#n #x #y #delta
2373whd in match (sub_offset ???) in ⊢ (??%%);
2374elim x #x' elim y #y' elim delta #delta'
2375normalize in match (offset_plus ??);
2376normalize in match (offset_plus ??);
2377cut ((x' - y') = (x'+delta'-(y'+delta')))
2378[ whd in match (Zminus ??) in ⊢ (??%%);
2379  >(Zopp_Zplus y' delta') <associative_Zplus /2/ ]
2380#Heq >Heq @refl
2381qed.   
2382
2383(* value_eq lifts to addition *)
2384lemma sub_value_eq :
2385  ∀E,v1,v2,v1',v2',ty1,ty2.
2386   value_eq E v1 v2 →
2387   value_eq E v1' v2' →
2388   ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
2389           ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2390#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2391@(value_eq_inversion E … Hvalue_eq1)
2392[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2393[ 1: whd in match (sem_sub ????); normalize nodelta
2394     cases (classify_sub ty1 ty2) normalize nodelta
2395     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
2396     #Habsurd destruct (Habsurd)
2397| 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2398     cases (classify_sub ty1 ty2) normalize nodelta     
2399     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2400     [ 2,3,5: #Habsurd destruct (Habsurd) ]
2401     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2402     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2403     [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ]
2404     @intsize_eq_elim_elim
2405      [ 1: #_ #Habsurd destruct (Habsurd)
2406      | 2: #Heq destruct (Heq) normalize nodelta
2407           #Heq destruct (Heq)
2408          /3 by ex_intro, conj, vint_eq/           
2409      ]
2410| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2411     cases (classify_sub ty1 ty2) normalize nodelta     
2412     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2413     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2414     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2415     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2416     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2417     #Heq destruct (Heq)
2418     /3 by ex_intro, conj, vfloat_eq/
2419| 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2420     cases (classify_sub ty1 ty2) normalize nodelta
2421     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2422     [ 1,2,5: #Habsurd destruct (Habsurd) ]
2423     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2424     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2425     [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ]         
2426     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2427                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2428     | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
2429| 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2430     cases (classify_sub ty1 ty2) normalize nodelta
2431     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2432     [ 1,2,5: #Habsurd destruct (Habsurd) ]
2433     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2434     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2435     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
2436     #Heq destruct (Heq)
2437     [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
2438          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2439          elim p1 in Hembed; #b1 #o1 normalize nodelta
2440          cases (E b1)
2441          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2442          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2443               normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
2444               @refl
2445          ]
2446     | 2: lapply Heq @eq_block_elim
2447          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
2448          | 1: #Hpblock1_eq normalize nodelta
2449               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
2450               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
2451               whd in ⊢ ((??%?) → (??%?) → ?);
2452               cases (E b1') normalize nodelta
2453               [ 1: #Habsurd destruct (Habsurd) ]
2454               * #dest_block #dest_off normalize nodelta
2455               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_identity normalize nodelta
2456               cases (eqb (sizeof tsg) O) normalize nodelta
2457               [ 1: #Habsurd destruct (Habsurd)
2458               | 2: >(sub_offset_translation 32 off1 off1' dest_off)
2459                    cases (division_u 31
2460                            (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
2461                            (repr (sizeof tsg)))
2462                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
2463                    | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
2464                         /3 by ex_intro, conj, vint_eq/ ]
2465    ] ] ]
2466] qed.
2467
2468
2469lemma mul_value_eq :
2470  ∀E,v1,v2,v1',v2',ty1,ty2.
2471   value_eq E v1 v2 →
2472   value_eq E v1' v2' →
2473   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
2474           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2475#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2476@(value_eq_inversion E … Hvalue_eq1)
2477[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2478[ 1: whd in match (sem_mul ????); normalize nodelta
2479     cases (classify_aop ty1 ty2) normalize nodelta
2480     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2481     #Habsurd destruct (Habsurd)
2482| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2483     cases (classify_aop ty1 ty2) normalize nodelta
2484     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2485     [ 2,3: #Habsurd destruct (Habsurd) ]
2486     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2487     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2488     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2489     @intsize_eq_elim_elim
2490      [ 1: #_ #Habsurd destruct (Habsurd)
2491      | 2: #Heq destruct (Heq) normalize nodelta
2492           #Heq destruct (Heq)
2493          /3 by ex_intro, conj, vint_eq/           
2494      ]
2495| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2496     cases (classify_aop ty1 ty2) normalize nodelta
2497     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2498     [ 1,3: #Habsurd destruct (Habsurd) ]
2499     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
2500     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2501     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2502     #Heq destruct (Heq)
2503     /3 by ex_intro, conj, vfloat_eq/
2504| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2505     cases (classify_aop ty1 ty2) normalize nodelta
2506     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2507     #Habsurd destruct (Habsurd)
2508| 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2509     cases (classify_aop ty1 ty2) normalize nodelta
2510     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2511     #Habsurd destruct (Habsurd)
2512] qed.
2513
2514lemma div_value_eq :
2515  ∀E,v1,v2,v1',v2',ty1,ty2.
2516   value_eq E v1 v2 →
2517   value_eq E v1' v2' →
2518   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
2519           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2520#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2521@(value_eq_inversion E … Hvalue_eq1)
2522[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2523[ 1: whd in match (sem_div ????); normalize nodelta
2524     cases (classify_aop ty1 ty2) normalize nodelta
2525     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2526     #Habsurd destruct (Habsurd)
2527| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2528     cases (classify_aop ty1 ty2) normalize nodelta
2529     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2530     [ 2,3: #Habsurd destruct (Habsurd) ]
2531     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2532     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2533     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2534     elim sg normalize nodelta
2535     @intsize_eq_elim_elim
2536     [ 1,3: #_ #Habsurd destruct (Habsurd)
2537     | 2,4: #Heq destruct (Heq) normalize nodelta
2538            @(match (division_s (bitsize_of_intsize sz') i i') with
2539              [ None ⇒ ?
2540              | Some bv' ⇒ ? ])
2541            [ 1: normalize  #Habsurd destruct (Habsurd)
2542            | 2: normalize #Heq destruct (Heq)
2543                 /3 by ex_intro, conj, vint_eq/
2544            | 3,4: elim sz' in i' i; #i' #i
2545                   normalize in match (pred_size_intsize ?);
2546                   generalize in match division_u; #division_u normalize
2547                   @(match (division_u ???) with
2548                    [ None ⇒ ?
2549                    | Some bv ⇒ ?]) normalize nodelta
2550                   #H destruct (H)
2551                  /3 by ex_intro, conj, vint_eq/ ]
2552     ]
2553| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2554     cases (classify_aop ty1 ty2) normalize nodelta
2555     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2556     [ 1,3: #Habsurd destruct (Habsurd) ]
2557     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
2558     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2559     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2560     #Heq destruct (Heq)
2561     /3 by ex_intro, conj, vfloat_eq/
2562| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2563     cases (classify_aop ty1 ty2) normalize nodelta
2564     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2565     #Habsurd destruct (Habsurd)
2566| 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2567     cases (classify_aop ty1 ty2) normalize nodelta
2568     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2569     #Habsurd destruct (Habsurd)
2570] qed.
2571
2572lemma mod_value_eq :
2573  ∀E,v1,v2,v1',v2',ty1,ty2.
2574   value_eq E v1 v2 →
2575   value_eq E v1' v2' →
2576   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
2577           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2578#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2579@(value_eq_inversion E … Hvalue_eq1)
2580[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2581[ 1: whd in match (sem_mod ????); normalize nodelta
2582     cases (classify_aop ty1 ty2) normalize nodelta
2583     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2584     #Habsurd destruct (Habsurd)
2585| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2586     cases (classify_aop ty1 ty2) normalize nodelta
2587     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2588     [ 2,3: #Habsurd destruct (Habsurd) ]
2589     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2590     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2591     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2592     elim sg normalize nodelta
2593     @intsize_eq_elim_elim
2594     [ 1,3: #_ #Habsurd destruct (Habsurd)
2595     | 2,4: #Heq destruct (Heq) normalize nodelta
2596            @(match (modulus_s (bitsize_of_intsize sz') i i') with
2597              [ None ⇒ ?
2598              | Some bv' ⇒ ? ])
2599            [ 1: normalize  #Habsurd destruct (Habsurd)
2600            | 2: normalize #Heq destruct (Heq)
2601                 /3 by ex_intro, conj, vint_eq/
2602            | 3,4: elim sz' in i' i; #i' #i
2603                   generalize in match modulus_u; #modulus_u normalize
2604                   @(match (modulus_u ???) with
2605                    [ None ⇒ ?
2606                    | Some bv ⇒ ?]) normalize nodelta
2607                   #H destruct (H)
2608                  /3 by ex_intro, conj, vint_eq/ ]
2609     ]
2610| 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2611     cases (classify_aop ty1 ty2) normalize nodelta
2612     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2613     #Habsurd destruct (Habsurd)
2614| 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2615     cases (classify_aop ty1 ty2) normalize nodelta
2616     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2617     #Habsurd destruct (Habsurd)
2618| 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2619     cases (classify_aop ty1 ty2) normalize nodelta
2620     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2621     #Habsurd destruct (Habsurd)
2622] qed.
2623
2624(* boolean ops *)
2625lemma and_value_eq :
2626  ∀E,v1,v2,v1',v2'.
2627   value_eq E v1 v2 →
2628   value_eq E v1' v2' →
2629   ∀r1. (sem_and v1 v1'=Some val r1→
2630           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
2631#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2632@(value_eq_inversion E … Hvalue_eq1)
2633[ 2: #sz #i
2634     @(value_eq_inversion E … Hvalue_eq2)
2635     [ 2: #sz' #i' whd in match (sem_and ??);
2636          @intsize_eq_elim_elim
2637          [ 1: #_ #Habsurd destruct (Habsurd)
2638          | 2: #Heq destruct (Heq) normalize nodelta
2639               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2640] ]
2641normalize in match (sem_and ??); #arg1 destruct
2642normalize in match (sem_and ??); #arg2 destruct
2643normalize in match (sem_and ??); #arg3 destruct
2644normalize in match (sem_and ??); #arg4 destruct
2645qed.
2646
2647lemma or_value_eq :
2648  ∀E,v1,v2,v1',v2'.
2649   value_eq E v1 v2 →
2650   value_eq E v1' v2' →
2651   ∀r1. (sem_or v1 v1'=Some val r1→
2652           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
2653#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2654@(value_eq_inversion E … Hvalue_eq1)
2655[ 2: #sz #i
2656     @(value_eq_inversion E … Hvalue_eq2)
2657     [ 2: #sz' #i' whd in match (sem_or ??);
2658          @intsize_eq_elim_elim
2659          [ 1: #_ #Habsurd destruct (Habsurd)
2660          | 2: #Heq destruct (Heq) normalize nodelta
2661               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2662] ]
2663normalize in match (sem_or ??); #arg1 destruct
2664normalize in match (sem_or ??); #arg2 destruct
2665normalize in match (sem_or ??); #arg3 destruct
2666normalize in match (sem_or ??); #arg4 destruct
2667qed.
2668
2669lemma xor_value_eq :
2670  ∀E,v1,v2,v1',v2'.
2671   value_eq E v1 v2 →
2672   value_eq E v1' v2' →
2673   ∀r1. (sem_xor v1 v1'=Some val r1→
2674           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
2675#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2676@(value_eq_inversion E … Hvalue_eq1)
2677[ 2: #sz #i
2678     @(value_eq_inversion E … Hvalue_eq2)
2679     [ 2: #sz' #i' whd in match (sem_xor ??);
2680          @intsize_eq_elim_elim
2681          [ 1: #_ #Habsurd destruct (Habsurd)
2682          | 2: #Heq destruct (Heq) normalize nodelta
2683               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2684] ]
2685normalize in match (sem_xor ??); #arg1 destruct
2686normalize in match (sem_xor ??); #arg2 destruct
2687normalize in match (sem_xor ??); #arg3 destruct
2688normalize in match (sem_xor ??); #arg4 destruct
2689qed.
2690
2691lemma shl_value_eq :
2692  ∀E,v1,v2,v1',v2'.
2693   value_eq E v1 v2 →
2694   value_eq E v1' v2' →
2695   ∀r1. (sem_shl v1 v1'=Some val r1→
2696           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
2697#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2698@(value_eq_inversion E … Hvalue_eq1)
2699[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2700[ 2:
2701     @(value_eq_inversion E … Hvalue_eq2)
2702     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2703     [ 2: whd in match (sem_shl ??);
2704          cases (lt_u ???) normalize nodelta
2705          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
2706          | 2: #Habsurd destruct (Habsurd)
2707          ]
2708     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2709| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2710qed.
2711
2712lemma shr_value_eq :
2713  ∀E,v1,v2,v1',v2',ty,ty'.
2714   value_eq E v1 v2 →
2715   value_eq E v1' v2' →
2716   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
2717           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
2718#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
2719@(value_eq_inversion E … Hvalue_eq1)
2720[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2721whd in match (sem_shr ????); whd in match (sem_shr ????);
2722[ 1: cases (classify_aop ty ty') normalize nodelta
2723     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2724     #Habsurd destruct (Habsurd)
2725| 2: cases (classify_aop ty ty') normalize nodelta
2726     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2727     [ 2,3: #Habsurd destruct (Habsurd) ]
2728     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2729     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2730     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2731     elim sg normalize nodelta
2732     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
2733     /3 by ex_intro, conj, refl, vint_eq/
2734| 3: cases (classify_aop ty ty') normalize nodelta
2735     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2736     #Habsurd destruct (Habsurd)
2737| 4: cases (classify_aop ty ty') normalize nodelta
2738     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2739     #Habsurd destruct (Habsurd)
2740| 5: cases (classify_aop ty ty') normalize nodelta
2741     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2742     #Habsurd destruct (Habsurd)
2743] qed.
2744
2745lemma Zplus_eq_eq : ∀x,y,delta:Z. eqZb x y = eqZb (x + delta) (y + delta).
2746#x #y #delta
2747@eqZb_elim
2748[ 1: #Heq >Heq >eqZb_z_z @refl
2749| 2: * #Hneq cut (x+delta ≠ y + delta)
2750     [ 1: % #H cut (x = y) [ 1: @(injective_Zplus_l delta) @H ] #H' @Hneq @H' ]
2751     #H @sym_eq @eqZb_false @H ] qed.
2752
2753(* offset equality is invariant by translation *)
2754lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
2755#delta #x #y normalize
2756elim delta #zdelta @sym_eq @Zplus_eq_eq qed.
2757
2758lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
2759#delta #x #y normalize
2760elim delta #zdelta @sym_eq <Zplus_eq_eq @refl qed.
2761
2762(* The key problem is that [sem_cmp] is a let-rec defined on [op], but we /don't want/ to
2763   perform a case-analysis on [op]. TODO: try and see if specifying another pseudo-decreasing
2764   argument is ok. This just won't cut it.. *)
2765lemma sem_cmp_value_eq :
2766  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
2767   value_eq E v1 v2 →
2768   value_eq E v1' v2' →
2769   memory_inj E m1 m2 →   
2770   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
2771           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
2772@cthulhu qed.
2773
2774(*           
2775#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
2776elim m1 in Hinj; #contents_map1 #nextblock1 #Hnextblock1 #Hinj
2777cases op whd in match (sem_cmp ??????) in ⊢ (% → ?);
2778cases (classify_cmp ty ty') normalize nodelta
2779[ 1,9,17: #sz #sg
2780  @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
2781  [ 1,6,11: #v #Habsurd destruct (Habsurd)
2782  | 2,7,12: #sz #i @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2783    [ 1,6,11: #v' #Habsurd destruct (Habsurd)
2784    | 2,7,12: #sz' #i'
2785    | 3,8,13: #f #Habsurd destruct (Habsurd)
2786    | 4,9,14: #Habsurd destruct (Habsurd)
2787    | 5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ]
2788
2789  | 3,8,13: #f #Habsurd destruct (Habsurd)   
2790  | 4,9,14: #Habsurd destruct (Habsurd)
2791  | 5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ]
2792| 2,10,18: #n #ty0 | 3,11,19: #fsz | 4,12,20: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
2793[ 1,6,11,16,21,26,31,36,41,46,51,56,61,66,71,76,81,86,91,96: #v #Habsurd destruct (Habsurd)
2794| 2,7,12,17,22,27,32,37,42,47,52,57,62,67,72,77,82,87,92,97: #sz' #i
2795
2796|
2797| 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
2798*)
2799
2800
2801(* The proof of the following lemma begs for factorization. *)
2802(*
2803lemma sem_cmp_value_eq :
2804  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
2805   value_eq E v1 v2 →
2806   value_eq E v1' v2' →
2807   memory_inj E m1 m2 →   
2808   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
2809           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
2810#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
2811cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????);
2812[ 1: (* Equality *)
2813  cases (classify_cmp ty ty') normalize nodelta
2814  [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
2815  @(value_eq_inversion E … Hvalue_eq1)
2816  [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
2817  normalize nodelta
2818  [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ]
2819  @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2820  [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ]
2821  [ 5: elim sg normalize nodelta
2822       @intsize_eq_elim_elim
2823       [ 1,3: #_ #Habsurd destruct (Habsurd)
2824       | 2,4: #Heq destruct (Heq) normalize nodelta
2825              [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq)
2826              | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ]
2827              /3 by ex_intro, conj, vint_eq/ ]
2828  | 10: #Heq destruct (Heq) cases (Fcmp Ceq f f') /3 by ex_intro, conj, vint_eq/
2829  | 15: whd in match (sem_cmp_match ?); #Heq destruct (Heq)
2830        /3 by ex_intro, conj, vint_eq/
2831  | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
2832        /3 by ex_intro, conj, vint_eq/
2833  | 20: lapply (mi_valid_pointers … Hinj p1' p2')
2834        lapply (mi_valid_pointers … Hinj p1 p2)
2835        cases (valid_pointer m1 p1')
2836        [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2837        cases (valid_pointer m1 p1)
2838        [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2839        #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
2840        >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
2841        elim p1 in Hembed; #b1 #o1
2842        elim p1' in Hembed'; #b1' #o1'
2843        whd in match (pointer_translation ??);
2844        whd in match (pointer_translation ??);
2845        @(eq_block_elim … b1 b1')
2846        [ 1: #Heq destruct (Heq)
2847              cases (E b1')
2848              [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
2849              * #eb1' #eo1' normalize nodelta
2850              #Heq1 #Heq2 #Heq3 destruct
2851              >eq_block_identity normalize nodelta
2852              >eq_offset_translation cases (cmp_offset ???)
2853              /3 by ex_intro, conj, vint_eq/
2854        | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
2855             cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2856             * #eb1 #eo1
2857             cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
2858             * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
2859             lapply (H ???? Hneq (refl ??) (refl ??))
2860             #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
2861             #Heq destruct (Heq) whd in match (sem_cmp_mismatch Ceq);
2862             %{Vfalse} @conj try @refl normalize in Heq; destruct (Heq)
2863             @vint_eq ]
2864  | *: #Habsurd destruct (Habsurd) ]
2865| 2: (* Inequality *)
2866  cases (classify_cmp ty ty') normalize nodelta
2867  [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
2868  @(value_eq_inversion E … Hvalue_eq1)
2869  [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
2870  normalize nodelta
2871  [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ]
2872  @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2873  [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ]
2874  [ 5: cases sg normalize nodelta
2875       @intsize_eq_elim_elim
2876       [ 1,3: #_ #Habsurd destruct (Habsurd)
2877       | 2,4: #Heq destruct (Heq) normalize nodelta
2878              [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq)
2879              | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ]
2880              /3 by ex_intro, conj, vint_eq/ ]
2881  | 10: #Heq destruct (Heq) cases (Fcmp Cne f f') /3 by ex_intro, conj, vint_eq/
2882  | 15: whd in match (sem_cmp_match ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
2883  | 16,19: whd in match (sem_cmp_mismatch ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
2884  | 20: lapply (mi_valid_pointers … Hinj p1' p2')
2885        lapply (mi_valid_pointers … Hinj p1 p2)
2886        cases (valid_pointer m1 p1')
2887        [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2888        cases (valid_pointer m1 p1)
2889        [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2890        #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
2891        >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
2892        elim p1 in Hembed; #b1 #o1
2893        elim p1' in Hembed'; #b1' #o1'
2894        whd in match (pointer_translation ??);
2895        whd in match (pointer_translation ??);
2896        @(eq_block_elim … b1 b1')
2897        [ 1: #Heq destruct (Heq)
2898              cases (E b1')
2899              [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
2900              * #eb1' #eo1' normalize nodelta
2901              #Heq1 #Heq2 #Heq3 destruct
2902              >eq_block_identity normalize nodelta
2903              >neq_offset_translation cases (cmp_offset ???)
2904              /3 by ex_intro, conj, vint_eq/
2905        | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
2906             cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2907             * #eb1 #eo1
2908             cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
2909             * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
2910             lapply (H ???? Hneq (refl ??) (refl ??))
2911             #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
2912             #Heq destruct (Heq) whd in match (sem_cmp_mismatch Cne);
2913             %{Vtrue} @conj try @refl normalize in Heq; destruct (Heq)
2914             @vint_eq ]
2915  | *: #Habsurd destruct (Habsurd) ]
2916| 3: (* Less-than *)
2917 
2918| 3: *: @cthulhu ]
2919qed.*)
2920 
2921(* Commutation result for binary operators. *)
2922lemma binary_operation_value_eq :
2923  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
2924   value_eq E v1 v2 →
2925   value_eq E v1' v2' →
2926   memory_inj E m1 m2 →
2927   ∀r1.
2928   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
2929   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
2930#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
2931cases op
2932whd in match (sem_binary_operation ??????);
2933whd in match (sem_binary_operation ??????);
2934@cthulhu
2935qed.
2936
2937 
2938(* Simulation relation on expressions *)
2939lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
2940  ∀E:embedding.
2941  ∀Hext:memory_ext E m1 m2.
2942  switch_removal_globals E ? fundef_switch_removal ge ge' →
2943  disjoint_extension en1 m1 en2 m2 ext E Hext →
2944  ext_fresh_for_genv ext ge →
2945  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
2946  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
2947#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
2948@expr_lvalue_ind_combined
2949[ 1: #csz #cty #i #a1
2950     whd in match (exec_expr ????); elim cty
2951     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2952     normalize nodelta
2953     [ 2: cases (eq_intsize csz sz) normalize nodelta
2954          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
2955          | 2: #Habsurd destruct (Habsurd) ]
2956     | 4,5,6: #_ #H destruct (H)
2957     | *: #H destruct (H) ]
2958| 2: #ty #fl #a1
2959     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
2960| 3: *
2961  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
2962  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
2963  #ty whd in ⊢ (% → ?); #Hind try @I
2964  whd in match (Plvalue ???);
2965  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
2966       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
2967       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2968       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
2969           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
2970           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
2971           whd in match (load_value_of_type' ???);
2972           whd in match (load_value_of_type' ???);
2973           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
2974           cases (load_value_of_type ty m1 bl1 o1)
2975           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2976           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
2977                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
2978                    normalize /4 by ex_intro, conj/
2979  ] ] ]
2980| 4: #v #ty whd * * #b1 #o1 #tr1
2981     whd in match (exec_lvalue' ?????);
2982     whd in match (exec_lvalue' ?????);
2983     lapply (Hdisjoint v)
2984     lapply (Hext_fresh_for_genv v)
2985     cases (mem_assoc_env v ext) #Hglobal
2986     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
2987          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
2988          >(Hglobal (refl ??)) normalize
2989          #Habsurd destruct (Habsurd)
2990     | 2: normalize nodelta
2991          cases (lookup ?? en1 v) normalize nodelta
2992          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
2993               lapply (rg_find_symbol … Hrelated v)
2994               cases (find_symbol ???) normalize
2995               [ 1: #_ #Habsurd destruct (Habsurd)
2996               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
2997                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
2998                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
2999                         %{〈block',mk_offset OZ,[]〉} @conj try @refl
3000                         normalize /2/
3001                ] ]
3002         | 2: #block
3003              cases (lookup ?? en2 v) normalize nodelta
3004              [ 1: #Hfalse @(False_ind … Hfalse)
3005              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
3006                   %{〈b, zero_offset, E0〉} @conj try @refl
3007                   normalize /2/
3008    ] ] ]
3009| 5: #e #ty whd in ⊢ (% → %);
3010     whd in match (exec_lvalue' ?????);
3011     whd in match (exec_lvalue' ?????);
3012     cases (exec_expr ge en1 m1 e)
3013     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
3014          * elim v1 normalize nodelta
3015          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
3016          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
3017          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
3018          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
3019          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
3020               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
3021               #Hvalue_eq normalize
3022               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
3023               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
3024               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
3025               %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
3026               normalize @conj // ]
3027     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
3028| 6: #ty #e #ty'
3029     #Hsim @(exec_lvalue_expr_elim … Hsim)
3030     cases ty
3031     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
3032     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
3033     #tr #H @conj try @refl try assumption
3034| 7: #ty #op #e
3035     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
3036     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
3037     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
3038     [ 1: #_ @I
3039     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
3040           normalize /2/ ]
3041| *: @cthulhu ] qed.
3042
3043(* TODO: Old cases, to be ported to memory injection.
3044| 8: #ty #op #e1 #e2 #Hind1 #Hind2
3045     whd in match (exec_expr ge ???);   
3046     whd in match (exec_expr ge' ???);
3047     @(exec_expr_expr_elim … Hind1)
3048     cases (exec_expr ge en1 m1 e2) in Hind2;
3049     [ 2: #error normalize //
3050     | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 *
3051          #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq'
3052          >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????);
3053
3054
3055| 9: #ty #castty #e #Hind
3056     whd in match (exec_expr ge ???);   
3057     whd in match (exec_expr ge' ???);
3058     cases Hind
3059     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3060     | 1: cases (exec_expr ge en m e)
3061          [ 2: #error #_ @SimFail /2 by ex_intro/
3062          | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
3063          ]
3064     ]
3065| 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3
3066     whd in match (exec_expr ge ???);   
3067     whd in match (exec_expr ge' ???);
3068     cases Hind1
3069     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3070     | 1: cases (exec_expr ge en m e1)
3071          [ 2: #error #_ @SimFail /2 by ex_intro/
3072          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
3073               normalize nodelta
3074               cases (exec_bool_of_val ??)
3075               [ 2: #error @SimFail /2 by ex_intro/
3076               | 1: * whd in match (m_bind ?????); normalize nodelta
3077                    [ 1: cases Hind2
3078                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3079                         | 1: cases (exec_expr ge en m e2)
3080                              [ 2: #error #_  @SimFail /2 by ex_intro/
3081                              | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))                                   
3082                                   @SimOk normalize nodelta #a2
3083                                   whd in match (m_bind ?????); // ]
3084                         ]
3085                    | 2: cases Hind3
3086                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3087                         | 1: cases (exec_expr ge en m e3)
3088                              [ 2: #error #_  @SimFail /2 by ex_intro/
3089                              | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3)))
3090                                   @SimOk normalize nodelta #a3
3091                                   whd in match (m_bind ?????); // ]
3092                         ]
3093     ] ] ] ]                     
3094| 11: #ty #e1 #e2 #Hind1 #Hind2
3095     whd in match (exec_expr ge ???);   
3096     whd in match (exec_expr ge' ???);
3097     cases Hind1
3098     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3099     | 1: cases (exec_expr ge en m e1)
3100          [ 2: #error #_ @SimFail /2 by ex_intro/
3101          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
3102               normalize nodelta
3103               cases (exec_bool_of_val ??)
3104               [ 2: #error @SimFail /2 by ex_intro/
3105               | 1: * whd in match (m_bind ?????);
3106                    [ 2: @SimOk // ]
3107                    cases Hind2
3108                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3109                    | 1: cases (exec_expr ge en m e2)
3110                         [ 2: #error #_  @SimFail /2 by ex_intro/
3111                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
3112                              @SimOk #a2
3113                              whd in match (m_bind ?????); //
3114     ] ] ] ] ]
3115| 12: #ty #e1 #e2 #Hind1 #Hind2
3116     whd in match (exec_expr ge ???);   
3117     whd in match (exec_expr ge' ???);
3118     cases Hind1
3119     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3120     | 1: cases (exec_expr ge en m e1)
3121          [ 2: #error #_ @SimFail /2 by ex_intro/
3122          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
3123               normalize nodelta
3124               cases (exec_bool_of_val ??)
3125               [ 2: #error @SimFail /2 by ex_intro/
3126               | 1: * whd in match (m_bind ?????);
3127                    [ 1: @SimOk // ]
3128                    cases Hind2
3129                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3130                    | 1: cases (exec_expr ge en m e2)
3131                         [ 2: #error #_  @SimFail /2 by ex_intro/
3132                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
3133                              @SimOk #a2
3134                              whd in match (m_bind ?????); //
3135     ] ] ] ] ]
3136| 13: #ty #sizeof_ty
3137     whd in match (exec_expr ge ???);   
3138     whd in match (exec_expr ge' ???);
3139     @SimOk //
3140| 14: #ty #e #ty' #fld #Hind
3141     whd in match (exec_lvalue' ge ????);
3142     whd in match (exec_lvalue' ge' ????);
3143     whd in match (typeof ?);
3144     cases ty' in Hind;
3145     [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
3146     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
3147     normalize nodelta #Hind
3148     try (@SimFail /2 by ex_intro/)
3149     whd in match (exec_lvalue ????);
3150     whd in match (exec_lvalue ????);     
3151     cases Hind
3152     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3153     | 1,3: cases (exec_lvalue' ge en m e ?)
3154         [ 2,4: #error #_ @SimFail /2 by ex_intro/
3155         | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
3156     ] ]
3157| 15: #ty #l #e #Hind
3158     whd in match (exec_expr ge ???);
3159     whd in match (exec_expr ge' ???);
3160     cases Hind
3161     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
3162     | 1: cases (exec_expr ge en m e)
3163        [ 2: #error #_ @SimFail /2 by ex_intro/
3164        | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
3165     ] ]
3166| 16: *
3167  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
3168  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
3169  #ty normalize in ⊢ (% → ?);
3170  [ 1,2: #_ @SimOk #a normalize //
3171  | 3,4,13: #H @(False_ind … H)
3172  | *: #_ @SimFail /2 by ex_intro/
3173  ]
3174] qed. *)
3175
3176(*
3177lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
3178related_globals ? fundef_switch_removal ge ge' →
3179∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
3180#ge #ge' #en #m #Hrelated #args
3181elim args
3182[ 1: /3/
3183| 2: #hd #tl #Hind normalize
3184     elim (sim_related_globals ge ge' en m Hrelated)
3185     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
3186     cases (exec_expr ge en m hd)
3187     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
3188     | 1: * #val_hd #trace_hd normalize nodelta
3189          cases Hind
3190          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
3191          | 1: cases (exec_exprlist ge en m tl)
3192               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
3193               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
3194                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
3195                    cases Hexec_hd
3196                    [ 2: * #error #Habsurd destruct (Habsurd)
3197                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
3198] ] ] ] qed.
3199*)
3200
3201(* The return type of any function is invariant under switch removal *)
3202lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
3203#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
3204qed.
3205
3206(* Similar stuff for fundefs *)
3207lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
3208* // qed.
3209
3210(*
3211lemma expr_fresh_lift :
3212  ∀e,u,id.
3213      fresh_for_expression e u →
3214      fresh_for_univ SymbolTag id u →
3215      fresh_for_univ SymbolTag (max_of_expr e id) u.
3216#e #u #id
3217normalize in match (fresh_for_expression e u);
3218#H1 #H2
3219>max_of_expr_rewrite
3220normalize in match (fresh_for_univ ???);
3221cases (max_of_expr e ?) in H1; #p #H1
3222cases id in H2; #p' #H2
3223normalize nodelta
3224cases (leb p p') normalize nodelta
3225[ 1: @H2 | 2: @H1 ]
3226qed. *)
3227
3228lemma while_fresh_lift : ∀e,s,u.
3229   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
3230#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
3231cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
3232cases (leb e s) try /2/
3233qed.
3234
3235(*
3236lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
3237#e0 #s0 #us0 normalize
3238cases (switch_removal s0 us0) * #body #newvars #u' normalize //
3239qed.*)
3240
3241lemma dowhile_fresh_lift : ∀e,s,u.
3242   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
3243#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
3244cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
3245cases (leb e s) try /2/
3246qed.
3247(*
3248lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
3249#e0 #s0 #us0 normalize
3250cases (switch_removal s0 us0) * #body #newvars #u' normalize //
3251qed.*)
3252
3253lemma for_fresh_lift : ∀cond,step,body,u.
3254  fresh_for_statement step u →
3255  fresh_for_statement body u →
3256  fresh_for_expression cond u →
3257  fresh_for_statement (Sfor Sskip cond step body) u.
3258#cond #step #body #u
3259whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
3260cases (max_of_statement step) #s
3261cases (max_of_statement body) #b
3262cases (max_of_expr cond) #c
3263whd in match (max_of_statement Sskip);
3264>(max_id_commutative least_identifier)
3265>max_id_one_neutral normalize nodelta
3266normalize elim u #u
3267cases (leb s b) cases (leb c b) cases (leb c s) try /2/
3268qed.
3269
3270(*
3271lemma for_commute : ∀e,stm1,stm2,u,uA.
3272   (uA=\snd  (switch_removal stm1 u)) →
3273   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
3274#e #stm1 #stm2 #u #uA #HuA
3275whd in match (sw_rem (Sfor ????) u);
3276whd in match (switch_removal ??);   
3277destruct
3278normalize in match (\snd (switch_removal Sskip u));
3279whd in match (sw_rem stm1 u);
3280cases (switch_removal stm1 u)
3281* #stm1' #fresh_vars #uA normalize nodelta
3282whd in match (sw_rem stm2 uA);
3283cases (switch_removal stm2 uA)
3284* #stm2' #fresh_vars2 #uB normalize nodelta
3285//
3286qed.*)
3287
3288(*
3289lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
3290*
3291[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
3292| 2: #e1 #e2 #u #_
3293     whd in match (sw_rem ??);
3294     whd in match (is_Sskip ?);
3295     try /2 by refl, ex_intro/
3296| 3: #ret #f #args #u
3297     whd in match (sw_rem ??);
3298     whd in match (is_Sskip ?);
3299     try /2 by refl, ex_intro/
3300| 4: #s1 #s2 #u
3301     whd in match (sw_rem ??);
3302     whd in match (switch_removal ??);     
3303     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
3304     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
3305     whd in match (is_Sskip ?);
3306     try /2 by refl, ex_intro/
3307| 5: #e #s1 #s2 #u #_
3308     whd in match (sw_rem ??);
3309     whd in match (switch_removal ??);     
3310     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3311     cases (switch_removal ? ?) * #e #f #h normalize nodelta
3312     whd in match (is_Sskip ?);
3313     try /2 by refl, ex_intro/
3314| 6,7: #e #s #u #_
3315     whd in match (sw_rem ??);
3316     whd in match (switch_removal ??);     
3317     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3318     whd in match (is_Sskip ?);
3319     try /2 by refl, ex_intro/
3320| 8: #s1 #e #s2 #s3 #u #_     
3321     whd in match (sw_rem ??);
3322     whd in match (switch_removal ??);     
3323     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3324     cases (switch_removal ? ?) * #e #f #g normalize nodelta
3325     cases (switch_removal ? ?) * #i #j #k normalize nodelta
3326     whd in match (is_Sskip ?);
3327     try /2 by refl, ex_intro/
3328| 9,10: #u #_     
3329     whd in match (is_Sskip ?);
3330     try /2 by refl, ex_intro/
3331| 11: #e #u #_
3332     whd in match (is_Sskip ?);
3333     try /2 by refl, ex_intro/
3334| 12: #e #ls #u #_
3335     whd in match (sw_rem ??);
3336     whd in match (switch_removal ??);
3337     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
3338     cases (fresh ??) #e #f normalize nodelta
3339     normalize in match (simplify_switch ???);
3340     cases (fresh ? f) #g #h normalize nodelta
3341     cases (produce_cond ????) * #k #l #m normalize nodelta
3342     whd in match (is_Sskip ?);
3343     try /2 by refl, ex_intro/
3344| 13,15: #lab #st #u #_
3345     whd in match (sw_rem ??);
3346     whd in match (switch_removal ??);
3347     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3348     whd in match (is_Sskip ?);
3349     try /2 by refl, ex_intro/
3350| 14: #lab #u     
3351     whd in match (is_Sskip ?);
3352     try /2 by refl, ex_intro/ ]
3353qed.
3354*)
3355
3356(*
3357lemma sw_rem_commute : ∀stm,u.
3358  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
3359#stm #u whd in match (sw_rem stm u); // qed.
3360*)
3361
3362lemma fresh_for_statement_inv :
3363  ∀u,s. fresh_for_statement s u →
3364        match u with
3365        [ mk_universe p ⇒ le (p0 one) p ].
3366* #p #s whd in match (fresh_for_statement ??);
3367cases (max_of_statement s) #s
3368normalize /2/ qed.
3369
3370lemma fresh_for_Sskip :
3371  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
3372#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3373
3374lemma fresh_for_Sbreak :
3375  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
3376#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3377
3378lemma fresh_for_Scontinue :
3379  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
3380#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3381
3382(*
3383lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
3384#s #u elim (switch_removal s u) * #res #fvs #u'
3385%{res} %{fvs} %{u'} //
3386qed.
3387
3388lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
3389#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
3390%{res} %{fvs} %{u'} //
3391qed.
3392*)
3393
3394lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
3395#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
3396#s #lab #u' %{s} %{lab} %{u'} //
3397qed.
3398
3399(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
3400lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
3401* * *
3402[ 1,5,9: #H @(False_ind … (H (refl ??)))
3403| *: #_ normalize @refl ]
3404qed.
3405
3406lemma exec_expr_int : ∀ge,e,m,expr.
3407    (∃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〉)).
3408#ge #e #m #expr cases (exec_expr ge e m expr)
3409[ 2: #error %2 #sz #n #tr % #H destruct (H)
3410| 1: * #val #trace cases val
3411     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
3412     | 3: #fl | 4: | 5: #ptr ]
3413     %2 #sz #n #tr % #H destruct (H)
3414] qed.
3415
3416(*
3417lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
3418  exec_expr ge e m cond = OK ? 〈v,tr〉 →
3419  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
3420  exec_expr ge' e m cond = OK ? 〈v,tr〉.
3421#ge #ge' #e #m #cond #v #tr #H *
3422[ 1: #Hsim >(Hsim ? H) //
3423| 2: * #error >H #Habsurd destruct (Habsurd) ]
3424qed. *)
3425
3426(*
3427lemma switch_simulation :
3428∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
3429 switch_cont_sim k k' →
3430 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
3431 fresh_for_statement (Sswitch cond switchcases) u →
3432 ∃tr'.
3433 (eventually ge'
3434  (λs2':state
3435   .switch_state_sim
3436    (State f
3437     (seq_of_labeled_statement (select_switch condsz condval switchcases))
3438     (Kswitch k) e m) s2')
3439  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
3440  tr').
3441#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
3442whd in match (sw_rem (Sswitch cond switchcases) u);
3443whd in match (switch_removal (Sswitch cond switchcases) u);
3444cases switchcases in Hfresh;
3445[ 1: #default_statement #Hfresh_for_default
3446     whd in match (switch_removal_branches ??);
3447     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
3448     elim (switch_removal_eq default_statement u)
3449     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
3450     normalize nodelta
3451     cut (u' = (\snd (switch_removal default_statement u)))
3452     [ 1: >Hdefault_statement_eq // ] #Heq_u'
3453     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
3454     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
3455     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
3456     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
3457     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
3458     normalize nodelta
3459     whd in match (simplify_switch (Expr ??) ?? uv2);
3460     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
3461     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
3462     -Hfreshness #Heq_uv3
3463     normalize nodelta whd in match (add_starting_lbl_list ????);
3464     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
3465     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
3466     -Hfreshness #Heq_uv4
3467     normalize nodelta
3468     @(eventually_later ge' ?? E0)
3469     whd in match (exec_step ??);
3470     %{(State (function_switch_removal f)
3471          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
3472          (Kseq
3473          (Ssequence
3474            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
3475            (Slabel exit_label Sskip))
3476          k') e m)} @conj try //
3477     @(eventually_later ge' ?? E0)
3478     whd in match (exec_step ??);
3479     
3480@chthulhu | @chthulhu
3481qed. *)
3482
3483
3484
3485(* Main theorem. To be ported and completed to memory injections. TODO *)
3486(*
3487theorem switch_removal_correction : ∀ge, ge'.
3488  related_globals ? fundef_switch_removal ge ge' →
3489  ∀s1, s1', tr, s2.
3490  switch_state_sim s1 s1' →
3491  exec_step ge s1 = Value … 〈tr,s2〉 →
3492  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
3493#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
3494inversion Hsim_state
3495[ 1: (* regular state *)
3496  #u #f #s #k #k' #m #m' #result #en #en' #f' #vars
3497  #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_
3498
3499  lapply (sim_related_globals ge ge' e m Hrelated) *
3500  #Hexpr_related #Hlvalue_related
3501  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
3502  cases s in Hu_fresh Heq_env;
3503 
3504
3505theorem switch_removal_correction : ∀ge, ge'.
3506  related_globals ? fundef_switch_removal ge ge' →
3507  ∀s1, s1', tr, s2.
3508  switch_state_sim s1 s1' →
3509  exec_step ge s1 = Value … 〈tr,s2〉 →
3510  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
3511#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
3512inversion Hsim_state
3513[ 1: (* regular state *)
3514  #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_
3515  lapply (sim_related_globals ge ge' e m Hrelated) *
3516  #Hexpr_related #Hlvalue_related
3517  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
3518  cases s in Hu_fresh Heq_env;
3519  (* Perform the intros for the statements*)
3520  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
3521  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
3522  | 14: #lab | 15: #cost #body ]
3523  #Hu_fresh #Heq_env
3524  [ 1: (* Skip *)
3525    whd in match (sw_rem ??);
3526    inversion Hsim_cont normalize nodelta
3527    [ 1: #Hk #Hk' #_ #Hexec_step
3528         @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify
3529         cases (fn_return f) in Hexec_step;
3530         [ 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
3531         | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
3532         normalize nodelta
3533         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H)
3534                %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try //
3535                normalize in Heq_env; destruct (Heq_env)
3536                %3 //
3537(*                cut (blocks_of_env e = blocks_of_env e')
3538                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
3539                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
3540                #Heq >Heq %3 // *)
3541         | *: #H destruct (H) ]
3542    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3543         whd in match (ret ??) in Heq; destruct (Heq)
3544         @(eventually_now ????) whd in match (exec_step ??);
3545         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
3546         %1 try //   
3547    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3548         @(eventually_now ????) whd in match (exec_step ??);
3549         whd in match (ret ??) in Heq; destruct (Heq)
3550         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
3551         >while_commute %1 try //
3552    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3553         @(eventually_now ????) whd in match (exec_step ??);
3554         lapply (Hexpr_related e0)
3555         cases (exec_expr ge e m e0) in Heq;
3556         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
3557         | 1: * #b #tr whd in match (m_bind ?????); #Heq
3558              *
3559              [ 2: * #error #Habsurd destruct (Habsurd)
3560              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
3561                   whd in match (bindIO ??????);
3562                   cases (exec_bool_of_val b (typeof e0)) in Heq;
3563                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3564                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
3565                        whd in match (bindIO ??????);
3566                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
3567                             @conj // >dowhile_commute %1 try //
3568                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
3569                             @conj // %1{us} try //
3570                             @(fresh_for_Sskip … Hus_fresh)
3571                        ] ] ] ]
3572    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3573         @(eventually_now ????) whd in match (exec_step ??);
3574         whd in match (ret ??) in Heq; destruct
3575         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
3576         @conj try // %1{u} try //
3577    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
3578         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
3579         destruct (Heq)
3580         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
3581         @conj try // %1
3582         [ 2: @swc_for3 //
3583         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
3584    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
3585         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
3586         destruct (Heq)
3587         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
3588         @conj try // <(for_commute ??? u uA) try // %1
3589         [ 2: assumption
3590         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
3591    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
3592         #Heq @(eventually_now ????) whd in match (exec_step ??);
3593         destruct (Heq)
3594         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
3595         %1{u} //
3596    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
3597         @(eventually_now ????) whd in match (exec_step ??);
3598         >fn_return_simplify cases (fn_return f) in Heq;
3599         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
3600         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
3601         normalize nodelta
3602         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
3603              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
3604              @conj try // %3 destruct //
3605         | *: #H destruct (H) ]     
3606     ]
3607  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
3608       whd in match (exec_step ??);
3609       cases lhs in Hu_fresh Heq; #lhs #lhs_type
3610       cases (Hlvalue_related lhs lhs_type)
3611       whd in match (exec_lvalue ge e m (Expr ??));
3612       whd in match (exec_lvalue ge' e m (Expr ??));
3613       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
3614       cases (exec_lvalue' ge e m lhs lhs_type)
3615       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
3616       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
3617            whd in match (m_bind ?????);
3618            cases (Hexpr_related rhs)
3619            [ 2: * #error #Hfail >Hfail #_
3620                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3621            | 1: cases (exec_expr ge e m rhs)
3622                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3623                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
3624                      whd in match (bindIO ??????) in ⊢ (% → % → %);
3625                      cases (opt_to_io io_out io_in ???)
3626                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3627                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3628                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
3629                           %{(State (function_switch_removal f) Sskip k' e mem)}
3630                           whd in match (bindIO ??????); @conj //
3631                           %1{u} try // @(fresh_for_Sskip … Hfresh)
3632       ] ] ] ]
3633   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
3634        whd in match (exec_step ??);
3635        cases (Hexpr_related func) in Heq;
3636        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3637        | 1: cases (exec_expr ge e m func)
3638             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3639             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
3640                  whd in match (m_bind ?????); normalize nodelta
3641                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
3642                  #Hexprlist_sim cases (Hexprlist_sim args)
3643                  [ 2: * #error #Hfail >Hfail
3644                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3645                  | 1: cases (exec_exprlist ge e m args)
3646                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3647                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
3648                            whd in match (bindIO ??????) in ⊢ (% → %);
3649                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
3650                            cases (find_funct clight_fundef ge fval)
3651                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
3652                                 whd in match (bindIO ??????) in ⊢ (% → %);
3653                                 >fundef_type_simplify
3654                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
3655                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3656                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
3657                                      cases retv normalize nodelta
3658                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
3659                                           %{(Callstate (fundef_switch_removal clfd) values
3660                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
3661                                           @conj try // %2 try // @swc_call //
3662                                      | 2: * #retval_ed #retval_type
3663                                           whd in match (exec_lvalue ge ???);
3664                                           whd in match (exec_lvalue ge' ???);                                     
3665                                           elim (Hlvalue_related retval_ed retval_type)
3666                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3667                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
3668                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
3669                                                     destruct (Habsurd)
3670                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
3671                                                     whd in match (m_bind ?????) in ⊢ (% → %);
3672                                                     #Heq destruct (Heq)
3673                                                     %{(Callstate (fundef_switch_removal clfd) values
3674                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
3675                                                               (function_switch_removal f) e k') m)}
3676                                                     @conj try //
3677                                                     %2 @swc_call //
3678                                ] ] ] ]
3679                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
3680                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3681       ] ] ] ] ]
3682   | 4: (* Ssequence *) normalize nodelta
3683        whd in match (ret ??) in ⊢ (% → ?); #Heq
3684        @(eventually_now ????)
3685        %{(State (function_switch_removal f)
3686                 (\fst (\fst (switch_removal stm1 u)))
3687                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
3688        @conj
3689        [ 2: destruct (Heq) %1
3690             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
3691             | 2: @swc_seq try // @switch_removal_fresh
3692                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
3693        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
3694             cases (switch_removal stm1 u)
3695             * #stm1' #fresh_vars #u' normalize nodelta
3696             cases (switch_removal stm2 u')
3697             * #stm2' #fresh_vars2 #u'' normalize nodelta
3698             whd in match (exec_step ??);
3699             destruct (Heq) @refl
3700        ]
3701   | 5: (* If-then-else *) normalize nodelta
3702        whd in match (ret ??) in ⊢ (% → ?); #Heq
3703        @(eventually_now ????) whd in match (sw_rem ??);
3704        whd in match (switch_removal ??);
3705        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
3706        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
3707        whd in match (exec_step ??);
3708        cases (Hexpr_related cond) in Heq;
3709        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3710        | 1: cases (exec_expr ge e m cond)
3711             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3712             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3713                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3714                  cases (exec_bool_of_val condval (typeof cond))
3715                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3716                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
3717                       destruct (Heq_condval) whd in match (bindIO ??????);
3718                       normalize nodelta
3719                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
3720                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
3721                           [ 1: >Hiftrue_eq normalize // ]
3722                           #Hrewrite >Hrewrite %1
3723                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
3724                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
3725                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
3726                           [ 1: >Hiffalse_eq // ]
3727                           #Hrewrite >Hrewrite %1 try //
3728                           cut (uA = (\snd (switch_removal iftrue u)))
3729                           [ 1: >Hiftrue_eq //
3730                           | 2: #Heq_uA >Heq_uA
3731                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
3732                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
3733       ] ] ] ] ]
3734   | 6: (* While loop *) normalize nodelta
3735        whd in match (ret ??) in ⊢ (% → ?); #Heq
3736        @(eventually_now ????) whd in match (sw_rem ??);
3737        whd in match (switch_removal ??);
3738        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
3739        whd in match (exec_step ??);
3740        cases (Hexpr_related cond) in Heq;
3741        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3742        | 1: cases (exec_expr ge e m cond)
3743             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3744             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3745                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3746                  cases (exec_bool_of_val condval (typeof cond))
3747                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3748                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
3749                       destruct (Heq_condval) whd in match (bindIO ??????);
3750                       normalize nodelta
3751                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
3752                            cut (body' = (\fst (\fst (switch_removal body u))))
3753                            [ 1: >Hbody_eq // ]
3754                            #Hrewrite >Hrewrite %1
3755                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
3756                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
3757                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
3758                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
3759        ] ] ] ]
3760   | 7: (* Dowhile loop *) normalize nodelta
3761        whd in match (ret ??) in ⊢ (% → ?); #Heq
3762        @(eventually_now ????) whd in match (sw_rem ??);
3763        whd in match (switch_removal ??);
3764        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
3765        whd in match (exec_step ??);
3766        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
3767        try //
3768        cut (body' = (\fst (\fst (switch_removal body u))))
3769        [ 1: >Hbody_eq // ]
3770        #Hrewrite >Hrewrite %1
3771        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
3772        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
3773   | 8: (* For loop *) normalize nodelta
3774        whd in match (ret ??) in ⊢ (% → ?); #Heq
3775        @(eventually_now ????) whd in match (sw_rem ??);
3776        whd in match (switch_removal ??);
3777        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
3778        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
3779              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
3780              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
3781              whd in match (exec_step ??);
3782              cases (Hexpr_related cond)
3783              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3784              | 1: cases (exec_expr ge e m cond)
3785                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3786                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
3787                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
3788                        cases (exec_bool_of_val condval (typeof cond))
3789                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3790                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
3791                             destruct (Heq_condval)
3792                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
3793                                  try //
3794                                  cut (body' = (\fst (\fst (switch_removal body uA))))
3795                                  [ 1: >Hbody_eq // ]
3796                                  #Hrewrite >Hrewrite
3797                                  cut (uA = (\snd (switch_removal step u)))
3798                                  [ 1: >Hstep_eq // ] #HuA
3799                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
3800                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
3801                                  [ 1: >HuA @switch_removal_fresh assumption
3802                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
3803                                       [ >Hstep_eq // ]
3804                                       #Hstep >Hstep @swc_for2 try assumption
3805                                       @for_fresh_lift try assumption ]
3806                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
3807                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
3808               ] ] ] ]
3809        | 2: #Heq
3810             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
3811             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
3812             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
3813             whd in match (exec_step ??);
3814             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
3815             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
3816             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
3817             whd in match (ret ??); destruct (Heq)
3818             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
3819             @conj try //
3820             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
3821             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
3822             <for_commute [ 2: >Hstep_eq // ]
3823             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
3824             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
3825             @swc_seq try // @for_fresh_lift
3826             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
3827             >HuA_eq @switch_removal_fresh assumption       
3828       ]
3829   | 9: (* break *) normalize nodelta
3830        inversion Hsim_cont
3831        [ 1: #Hk #Hk' #_       
3832        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
3833        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
3834        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3835        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3836        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
3837        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
3838        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
3839        normalize nodelta #H try (destruct (H))
3840        whd in match (ret ??) in H; destruct (H)
3841        @(eventually_now ????)
3842        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
3843        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
3844    | 10: (* Continue *) normalize nodelta
3845        inversion Hsim_cont
3846        [ 1: #Hk #Hk' #_       
3847        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
3848        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
3849        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3850        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
3851        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
3852        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
3853        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
3854        normalize nodelta #H try (destruct (H))
3855        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
3856        destruct (H)
3857        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
3858        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
3859             >while_commute %1{u0} try assumption
3860        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
3861             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3862             | 1: * #condval #trace whd in match (m_bind ?????);
3863                  #Heq *
3864                  [ 2: * #error #Habsurd destruct (Habsurd)
3865                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
3866                       whd in match (bindIO ??????);
3867                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
3868                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3869                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
3870                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)}
3871                                 @conj try // >dowhile_commute %1{u0} assumption
3872                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
3873                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
3874             ] ] ]
3875        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
3876             try // @(fresh_for_Scontinue … Hfor_fresh)
3877        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
3878             @conj try // %1{u0}
3879             elim (substatement_fresh … Hfor_fresh) * * try //
3880             #HSskip #Hcond #Hstep #Hbody
3881             @swc_for3 assumption
3882        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
3883             %1{u} try //
3884        ]
3885    | 11: (* Sreturn *) normalize nodelta #Heq
3886          @(eventually_now ????)
3887          whd in match (exec_step ??) in Heq ⊢ %;
3888          cases retval in Heq; normalize nodelta
3889          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
3890               whd in match (ret ??) in ⊢ (% → %);
3891               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
3892               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
3893               #H destruct (H)
3894               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
3895               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
3896          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
3897               [ 1: #_ #Habsurd destruct (Habsurd)
3898               | 2: #_ elim (Hexpr_related expr)
3899                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3900                    | 1: cases (exec_expr ??? expr)
3901                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3902                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
3903                              #Hrewrite >Hrewrite
3904                              whd in match (m_bind ?????); whd in match (m_bind ?????);
3905                              #Heq destruct (Heq)
3906                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
3907                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
3908         ] ] ] ]
3909    | 12: (* Sswitch. Main proof case. *) normalize nodelta
3910          (* Case analysis on the outcome of the tested expression *)
3911          cases (exec_expr_int ge e m cond)
3912          [ 2: cases (exec_expr ge e m cond)
3913               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
3914               | 1: * #val #trace cases val
3915                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
3916                    whd in match (m_bind ?????);
3917                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
3918                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
3919          ]
3920          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
3921          whd in match (m_bind ?????); #Heq
3922          destruct (Heq)
3923          @eventually_later
3924          whd in match (sw_rem (Sswitch cond switchcases) u);
3925          whd in match (switch_removal (Sswitch cond switchcases) u);
3926          elim (switch_removal_branches_eq switchcases u)
3927          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
3928          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
3929          [ 1: >Hsrb_eq // ] #Huv1_eq
3930          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
3931          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
3932          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
3933          whd in match (simplify_switch ???);
3934          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
3935          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
3936          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)         
3937          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
3938          #Huv4_eq
3939          whd in match (exec_step ??);
3940          %{(State (function_switch_removal f)
3941                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
3942                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
3943          %{E0} @conj try @refl
3944          %{tr} normalize in match (eq ???); @conj try //
3945          (* execute the conditional *)
3946          @eventually_later
3947          (* lift the result of the previous case analysis from [ge] to [ge'] *)
3948          whd in match (exec_step ??);
3949          whd in match (exec_lvalue ????);
3950         
3951          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
3952         
3953  *)
3954 
Note: See TracBrowser for help on using the repository browser.