source: src/Clight/switchRemoval.ma @ 2302

Last change on this file since 2302 was 2302, checked in by garnier, 7 years ago

Finally proved associativity of addition on bitvectors. Rejoice.

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