source: src/Clight/switchRemoval.ma @ 2298

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

WIP: converting switch removal from Z to bitvectors. Does not compile, contains axioms.

  • Property svn:executable set to *
File size: 190.4 KB
Line 
1include "Clight/Csyntax.ma".
2include "Clight/fresh.ma".
3include "basics/lists/list.ma".
4include "common/Identifiers.ma".
5include "Clight/Cexec.ma".
6include "Clight/CexecInd.ma".
7include "Clight/frontend_misc.ma".
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
2330axiom associative_add_with_carries :
2331  ∀n,a,b,c,carry1,carry2.
2332 ((let 〈res,flags〉 ≝
2333          add_with_carries n a
2334          (let 〈res,flags〉 ≝add_with_carries n b c carry1 in res) carry2 in 
2335   res)
2336  =(let 〈res,flags〉 ≝
2337           add_with_carries n
2338           (let 〈res,flags〉 ≝add_with_carries n a b carry1 in res) c carry2 in 
2339    res)). 
2340(*
2341    (\fst (add_with_carries n a (\fst (add_with_carries n b c carry1)) carry2)) =
2342    (\fst (add_with_carries n (\fst (add_with_carries n a b carry1)) c carry2)).
2343
2344#n elim n
2345[ 1: #a #b #c #carry1 #carry2
2346     lapply (BitVector_O … a)
2347     lapply (BitVector_O … b)
2348     lapply (BitVector_O … c)
2349     #Ha #Hb #Hc
2350     destruct //
2351| 2: #n' #Hind #a #b #c #carry1 #carry2
2352     lapply (BitVector_Sn … a)
2353     lapply (BitVector_Sn … b)
2354     lapply (BitVector_Sn … c)
2355     * #chd * #ctl #Heqc
2356     * #bhd * #btl #Heqb
2357     * #ahd * #atl #Heqa
2358     lapply (Hind atl btl ctl carry2 carry1) #Hind
2359     lapply (BitVector_Sn … (\fst  (add_with_carries (S n') b c carry1)))
2360     lapply (BitVector_Sn … (\fst  (add_with_carries (S n') a b carry1)))
2361     * #ab1 * #abtl1 #Heq_ab
2362     * #bc1 * #bctl1 #Heq_bc
2363     >Heq_ab >Heq_bc destruct
2364     whd in match (add_with_carries) in ⊢ (??%%);
2365     normalize nodelta
2366     whd in match (add_with_carries) in Heq_bc Heq_ab;
2367     normalize nodelta in Heq_bc Heq_ab;
2368     <Heq_ab <Heq_bc
2369     >fold_right2_i_unfold
2370     >fold_right2_i_unfold
2371     lapply Hind;
2372     whd in match (add_with_carries ????) in ⊢ ((??%%) → ?);
2373     normalize in match (add_with_carries ????) in ⊢ ((??%%) → ?);
2374     normalize
2375     #Hind >Hind
2376     normalize nodelta
2377     
2378     normalize in Hind;
2379*) 
2380   
2381lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a.
2382#n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries
2383@refl
2384qed.
2385
2386lemma 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.
2387#n #a #b #c whd in match (addition_n ???) in ⊢ (??%%);
2388whd in match (addition_n n b c);
2389whd in match (addition_n n a b);
2390<(associative_add_with_carries … n a b c false false)
2391@refl
2392qed.
2393
2394(* value_eq lifts to addition *)
2395lemma add_value_eq :
2396  ∀E,v1,v2,v1',v2',ty1,ty2.
2397   value_eq E v1 v2 →
2398   value_eq E v1' v2' →
2399   (* memory_inj E m1 m2 →  This injection seems useless TODO *)
2400   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
2401           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2402#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2403@(value_eq_inversion E … Hvalue_eq1)
2404[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2405[ 1: whd in match (sem_add ????); normalize nodelta
2406     cases (classify_add ty1 ty2) normalize nodelta
2407     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
2408     #Habsurd destruct (Habsurd)
2409| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2410     cases (classify_add ty1 ty2) normalize nodelta     
2411     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2412     [ 2,3,5: #Habsurd destruct (Habsurd) ]
2413     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2414     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2415     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
2416     [ 1: @intsize_eq_elim_elim
2417          [ 1: #_ #Habsurd destruct (Habsurd)
2418          | 2: #Heq destruct (Heq) normalize nodelta
2419               #Heq destruct (Heq)
2420               /3 by ex_intro, conj, vint_eq/ ]
2421     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
2422          /3 by ex_intro, conj, vint_eq/
2423     | 3: #Heq destruct (Heq)
2424          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
2425          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
2426          @vptr_eq whd in match (pointer_translation ??);
2427          cases (E b1') in Hembed;
2428          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2429          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2430               whd in match (shift_pointer_n ????);
2431               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
2432                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i))
2433               [ 1: whd in match (offset_plus ??);
2434                    whd in match (shift_offset_n ????) in ⊢ (??%%);
2435                    >commutative_addition_n >associative_addition_n
2436                    <(commutative_addition_n … (offv offset) (offv o1')) @refl ]
2437               #Heq >Heq @refl ]
2438     ]
2439| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2440     cases (classify_add ty1 ty2) normalize nodelta     
2441     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2442     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2443     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2444     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2445     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2446     #Heq destruct (Heq)
2447     /3 by ex_intro, conj, vfloat_eq/
2448| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2449     cases (classify_add ty1 ty2) normalize nodelta     
2450     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2451     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2452     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2453     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2454     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2455     @eq_bv_elim
2456     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2457     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2458| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2459     cases (classify_add ty1 ty2) normalize nodelta
2460     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2461     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2462     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2463     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2464     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2465     #Heq destruct (Heq)
2466     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
2467     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2468     elim p1 in Hembed; #b1 #o1 normalize nodelta
2469     cases (E b1)
2470     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2471     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2472          whd in match (shift_pointer_n ????);
2473          whd in match (shift_offset_n ????) in ⊢ (??%%);
2474          whd in match (offset_plus ??);
2475          whd in match (offset_plus ??);
2476          >commutative_addition_n >(associative_addition_n … offset_size ?)
2477          >(commutative_addition_n ? (offv offset) ?) @refl
2478     ]
2479] qed.
2480
2481lemma fold_right2_O : ∀A,B,C,f,init,vec1,vec2.
2482  fold_right2_i A B C f init 0 vec1 vec2 = init.
2483#A #B #C #f #init #vec1 #vec2
2484>(Vector_O … vec1) 
2485>(Vector_O … vec2)
2486normalize @refl
2487qed.
2488
2489lemma map_unfold : ∀A,B:Type[0].∀n,f,hd.∀tl:Vector A n.
2490  map A B (S n) f (hd ::: tl) = (f hd) ::: (map A B n f tl).
2491#A #B #n #f #hd #tl normalize @refl qed.
2492
2493lemma replicate_unfold : ∀A,sz,elt.
2494  replicate A (S sz) elt = elt ::: (replicate A sz elt).
2495// qed.
2496
2497axiom subtraction_delta : ∀x,y,delta.
2498  subtraction offset_size
2499    (addition_n offset_size x delta)
2500    (addition_n offset_size y delta) =
2501  subtraction offset_size x y.
2502(*
2503elim offset_size
2504[ 1: #x #y #delta
2505     >(BitVector_O … x)
2506     >(BitVector_O … y)
2507     >(BitVector_O … delta)
2508     //
2509     
2510| 2: #sz elim sz (* I would like to do this elim much later, but it fails. *)
2511    [ 1: #Hind #x #y #delta
2512         lapply (BitVector_Sn … x)
2513         lapply (BitVector_Sn … y)
2514         lapply (BitVector_Sn … delta)
2515         * #delta_hd * #delta_tl #Heq_delta
2516         * #y_hd * #y_tl #Heq_y
2517         * #x_hd * #x_tl #Heq_x
2518         destruct
2519         whd in match (addition_n ? (x_hd:::x_tl) ?);
2520         whd in match (addition_n ? (y_hd:::y_tl) ?);
2521         >add_with_carries_unfold
2522         >add_with_carries_unfold
2523         >fold_right2_i_unfold
2524         >fold_right2_i_unfold
2525         <add_with_carries_unfold
2526         <add_with_carries_unfold
2527         cases (add_with_carries 0 x_tl delta_tl false);
2528         #x_delta_res #x_delta_flags normalize nodelta
2529         cases (add_with_carries 0 y_tl delta_tl false)
2530         #y_delta_res #y_delta_flags normalize nodelta
2531         >(BitVector_O … x_delta_flags)
2532         >(BitVector_O … y_delta_flags)
2533         >(BitVector_O … x_delta_res)
2534         >(BitVector_O … y_delta_res)
2535         normalize nodelta
2536         whd in match (xorb ? false) in ⊢ (??(??%%)?); normalize nodelta
2537         whd in match (subtraction ???) in ⊢ (??%%);
2538         >add_with_carries_unfold
2539         whd in match (two_complement_negation ??);
2540         whd in match (negation_bv ??);
2541         whd in match (zero ?);
2542         >add_with_carries_unfold
2543         >fold_right2_i_unfold >fold_right2_O
2544         normalize nodelta
2545         >fold_right2_i_unfold >fold_right2_O
2546         normalize nodelta
2547         cases x_hd cases y_hd cases delta_hd normalize try @refl
2548    | 2: #sz' #HindA #HindB #x #y #delta
2549         lapply (BitVector_Sn … x)
2550         lapply (BitVector_Sn … y)
2551         lapply (BitVector_Sn … delta)
2552         * #delta_hd * #delta_tl #Heq_delta
2553         * #y_hd * #y_tl #Heq_y
2554         * #x_hd * #x_tl #Heq_x
2555         lapply (HindB x_tl y_tl delta_tl)
2556         destruct
2557         whd in match (addition_n ???) in ⊢ ((??(??%%)?) → ?); #Hind0
2558         whd in match (addition_n ? (x_hd:::x_tl) ?);
2559         whd in match (addition_n ? (y_hd:::y_tl) ?);
2560         >add_with_carries_unfold
2561         >add_with_carries_unfold
2562         >fold_right2_i_unfold
2563         >fold_right2_i_unfold
2564         <add_with_carries_unfold
2565         <add_with_carries_unfold
2566         cases (add_with_carries (S sz') x_tl delta_tl false) in Hind0;
2567         #x_delta_res #x_delta_flags normalize nodelta
2568         cases (add_with_carries (S sz') y_tl delta_tl false)
2569         #y_delta_res #y_delta_flags normalize nodelta
2570         elim (BitVector_Sn … x_delta_flags) #hd_x_delta * #tl_x_delta #Heq_xdelta >Heq_xdelta
2571         elim (BitVector_Sn … y_delta_flags) #hd_y_delta * #tl_y_delta #Heq_ydelta >Heq_ydelta
2572         #Heq_ind
2573         normalize nodelta
2574         cases hd_x_delta cases hd_y_delta normalize nodelta
2575         whd in match (subtraction ???) in ⊢ (??%%);
2576         whd in match (two_complement_negation ??) in ⊢ (??%%);
2577         whd in match (negation_bv ??) in ⊢ (??%%);
2578         whd in match (zero (S (S sz')));
2579         >add_with_carries_unfold in match (\fst (add_with_carries ????)) in ⊢ (??%?);
2580         >add_with_carries_unfold in match (\fst (add_with_carries ????)) in ⊢ (???%);
2581         lapply (add_with_carries_unfold
2582                       (S (S sz'))
2583                       ((¬y_hd):::map bool bool (S sz') notb y_tl)
2584                       (false:::replicate bool (S sz') false)
2585                       true) #Heq >Heq
2586         >fold_right2_i_unfold >fold_right2_i_unfold
2587         >add_with_carries_unfold in ⊢ (???(match (???%?) with [ _ ⇒ ? ] ));
2588
2589*)
2590
2591(* Offset subtraction is invariant by translation *)
2592lemma sub_offset_translation :
2593 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
2594#n #x #y #delta
2595whd in match (sub_offset ???) in ⊢ (??%%);
2596elim x #x' elim y #y' elim delta #delta'
2597whd in match (offset_plus ??);
2598whd in match (offset_plus ??);
2599>subtraction_delta @refl
2600qed.
2601
2602(* value_eq lifts to addition *)
2603lemma sub_value_eq :
2604  ∀E,v1,v2,v1',v2',ty1,ty2.
2605   value_eq E v1 v2 →
2606   value_eq E v1' v2' →
2607   ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
2608           ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2609#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2610@(value_eq_inversion E … Hvalue_eq1)
2611[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2612[ 1: whd in match (sem_sub ????); normalize nodelta
2613     cases (classify_sub ty1 ty2) normalize nodelta
2614     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
2615     #Habsurd destruct (Habsurd)
2616| 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2617     cases (classify_sub ty1 ty2) normalize nodelta     
2618     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2619     [ 2,3,5: #Habsurd destruct (Habsurd) ]
2620     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2621     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2622     [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ]
2623     @intsize_eq_elim_elim
2624      [ 1: #_ #Habsurd destruct (Habsurd)
2625      | 2: #Heq destruct (Heq) normalize nodelta
2626           #Heq destruct (Heq)
2627          /3 by ex_intro, conj, vint_eq/           
2628      ]
2629| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2630     cases (classify_sub ty1 ty2) normalize nodelta     
2631     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2632     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2633     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2634     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2635     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2636     #Heq destruct (Heq)
2637     /3 by ex_intro, conj, vfloat_eq/
2638| 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2639     cases (classify_sub ty1 ty2) normalize nodelta
2640     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2641     [ 1,2,5: #Habsurd destruct (Habsurd) ]
2642     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2643     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2644     [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ]         
2645     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2646                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2647     | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
2648| 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2649     cases (classify_sub ty1 ty2) normalize nodelta
2650     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
2651     [ 1,2,5: #Habsurd destruct (Habsurd) ]
2652     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2653     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
2654     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
2655     #Heq destruct (Heq)
2656     [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
2657          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2658          elim p1 in Hembed; #b1 #o1 normalize nodelta
2659          cases (E b1)
2660          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2661          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2662               whd in match (offset_plus ??) in ⊢ (??%%);
2663               whd in match (neg_shift_pointer_n ????) in ⊢ (??%%);
2664               whd in match (neg_shift_offset_n ????) in ⊢ (??%%);
2665               whd in match (subtraction) in ⊢ (??%%); normalize nodelta
2666               generalize in match (short_multiplication ???); #mult
2667               /3 by associative_addition_n, commutative_addition_n, refl/
2668          ]
2669     | 2: lapply Heq @eq_block_elim
2670          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
2671          | 1: #Hpblock1_eq normalize nodelta
2672               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
2673               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
2674               whd in ⊢ ((??%?) → (??%?) → ?);
2675               cases (E b1') normalize nodelta
2676               [ 1: #Habsurd destruct (Habsurd) ]
2677               * #dest_block #dest_off normalize nodelta
2678               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_identity normalize nodelta
2679               cases (eqb (sizeof tsg) O) normalize nodelta
2680               [ 1: #Habsurd destruct (Habsurd)
2681               | 2: >(sub_offset_translation 32 off1 off1' dest_off)
2682                    cases (division_u 31
2683                            (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
2684                            (repr (sizeof tsg)))
2685                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
2686                    | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
2687                         /3 by ex_intro, conj, vint_eq/ ]
2688    ] ] ]
2689] qed.
2690
2691
2692lemma mul_value_eq :
2693  ∀E,v1,v2,v1',v2',ty1,ty2.
2694   value_eq E v1 v2 →
2695   value_eq E v1' v2' →
2696   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
2697           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2698#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2699@(value_eq_inversion E … Hvalue_eq1)
2700[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2701[ 1: whd in match (sem_mul ????); normalize nodelta
2702     cases (classify_aop ty1 ty2) normalize nodelta
2703     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2704     #Habsurd destruct (Habsurd)
2705| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2706     cases (classify_aop ty1 ty2) normalize nodelta
2707     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2708     [ 2,3: #Habsurd destruct (Habsurd) ]
2709     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2710     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2711     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2712     @intsize_eq_elim_elim
2713      [ 1: #_ #Habsurd destruct (Habsurd)
2714      | 2: #Heq destruct (Heq) normalize nodelta
2715           #Heq destruct (Heq)
2716          /3 by ex_intro, conj, vint_eq/           
2717      ]
2718| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2719     cases (classify_aop ty1 ty2) normalize nodelta
2720     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2721     [ 1,3: #Habsurd destruct (Habsurd) ]
2722     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
2723     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2724     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2725     #Heq destruct (Heq)
2726     /3 by ex_intro, conj, vfloat_eq/
2727| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2728     cases (classify_aop ty1 ty2) normalize nodelta
2729     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2730     #Habsurd destruct (Habsurd)
2731| 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2732     cases (classify_aop ty1 ty2) normalize nodelta
2733     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2734     #Habsurd destruct (Habsurd)
2735] qed.
2736
2737lemma div_value_eq :
2738  ∀E,v1,v2,v1',v2',ty1,ty2.
2739   value_eq E v1 v2 →
2740   value_eq E v1' v2' →
2741   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
2742           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2743#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2744@(value_eq_inversion E … Hvalue_eq1)
2745[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2746[ 1: whd in match (sem_div ????); normalize nodelta
2747     cases (classify_aop ty1 ty2) normalize nodelta
2748     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2749     #Habsurd destruct (Habsurd)
2750| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2751     cases (classify_aop ty1 ty2) normalize nodelta
2752     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2753     [ 2,3: #Habsurd destruct (Habsurd) ]
2754     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2755     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2756     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2757     elim sg normalize nodelta
2758     @intsize_eq_elim_elim
2759     [ 1,3: #_ #Habsurd destruct (Habsurd)
2760     | 2,4: #Heq destruct (Heq) normalize nodelta
2761            @(match (division_s (bitsize_of_intsize sz') i i') with
2762              [ None ⇒ ?
2763              | Some bv' ⇒ ? ])
2764            [ 1: normalize  #Habsurd destruct (Habsurd)
2765            | 2: normalize #Heq destruct (Heq)
2766                 /3 by ex_intro, conj, vint_eq/
2767            | 3,4: elim sz' in i' i; #i' #i
2768                   normalize in match (pred_size_intsize ?);
2769                   generalize in match division_u; #division_u normalize
2770                   @(match (division_u ???) with
2771                    [ None ⇒ ?
2772                    | Some bv ⇒ ?]) normalize nodelta
2773                   #H destruct (H)
2774                  /3 by ex_intro, conj, vint_eq/ ]
2775     ]
2776| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2777     cases (classify_aop ty1 ty2) normalize nodelta
2778     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2779     [ 1,3: #Habsurd destruct (Habsurd) ]
2780     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
2781     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2782     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2783     #Heq destruct (Heq)
2784     /3 by ex_intro, conj, vfloat_eq/
2785| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2786     cases (classify_aop ty1 ty2) normalize nodelta
2787     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2788     #Habsurd destruct (Habsurd)
2789| 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2790     cases (classify_aop ty1 ty2) normalize nodelta
2791     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2792     #Habsurd destruct (Habsurd)
2793] qed.
2794
2795lemma mod_value_eq :
2796  ∀E,v1,v2,v1',v2',ty1,ty2.
2797   value_eq E v1 v2 →
2798   value_eq E v1' v2' →
2799   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
2800           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2801#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2802@(value_eq_inversion E … Hvalue_eq1)
2803[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2804[ 1: whd in match (sem_mod ????); normalize nodelta
2805     cases (classify_aop ty1 ty2) normalize nodelta
2806     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2807     #Habsurd destruct (Habsurd)
2808| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2809     cases (classify_aop ty1 ty2) normalize nodelta
2810     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2811     [ 2,3: #Habsurd destruct (Habsurd) ]
2812     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2813     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2814     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2815     elim sg normalize nodelta
2816     @intsize_eq_elim_elim
2817     [ 1,3: #_ #Habsurd destruct (Habsurd)
2818     | 2,4: #Heq destruct (Heq) normalize nodelta
2819            @(match (modulus_s (bitsize_of_intsize sz') i i') with
2820              [ None ⇒ ?
2821              | Some bv' ⇒ ? ])
2822            [ 1: normalize  #Habsurd destruct (Habsurd)
2823            | 2: normalize #Heq destruct (Heq)
2824                 /3 by ex_intro, conj, vint_eq/
2825            | 3,4: elim sz' in i' i; #i' #i
2826                   generalize in match modulus_u; #modulus_u normalize
2827                   @(match (modulus_u ???) with
2828                    [ None ⇒ ?
2829                    | Some bv ⇒ ?]) normalize nodelta
2830                   #H destruct (H)
2831                  /3 by ex_intro, conj, vint_eq/ ]
2832     ]
2833| 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2834     cases (classify_aop ty1 ty2) normalize nodelta
2835     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2836     #Habsurd destruct (Habsurd)
2837| 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2838     cases (classify_aop ty1 ty2) normalize nodelta
2839     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2840     #Habsurd destruct (Habsurd)
2841| 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2842     cases (classify_aop ty1 ty2) normalize nodelta
2843     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
2844     #Habsurd destruct (Habsurd)
2845] qed.
2846
2847(* boolean ops *)
2848lemma and_value_eq :
2849  ∀E,v1,v2,v1',v2'.
2850   value_eq E v1 v2 →
2851   value_eq E v1' v2' →
2852   ∀r1. (sem_and v1 v1'=Some val r1→
2853           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
2854#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2855@(value_eq_inversion E … Hvalue_eq1)
2856[ 2: #sz #i
2857     @(value_eq_inversion E … Hvalue_eq2)
2858     [ 2: #sz' #i' whd in match (sem_and ??);
2859          @intsize_eq_elim_elim
2860          [ 1: #_ #Habsurd destruct (Habsurd)
2861          | 2: #Heq destruct (Heq) normalize nodelta
2862               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2863] ]
2864normalize in match (sem_and ??); #arg1 destruct
2865normalize in match (sem_and ??); #arg2 destruct
2866normalize in match (sem_and ??); #arg3 destruct
2867normalize in match (sem_and ??); #arg4 destruct
2868qed.
2869
2870lemma or_value_eq :
2871  ∀E,v1,v2,v1',v2'.
2872   value_eq E v1 v2 →
2873   value_eq E v1' v2' →
2874   ∀r1. (sem_or v1 v1'=Some val r1→
2875           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
2876#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2877@(value_eq_inversion E … Hvalue_eq1)
2878[ 2: #sz #i
2879     @(value_eq_inversion E … Hvalue_eq2)
2880     [ 2: #sz' #i' whd in match (sem_or ??);
2881          @intsize_eq_elim_elim
2882          [ 1: #_ #Habsurd destruct (Habsurd)
2883          | 2: #Heq destruct (Heq) normalize nodelta
2884               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2885] ]
2886normalize in match (sem_or ??); #arg1 destruct
2887normalize in match (sem_or ??); #arg2 destruct
2888normalize in match (sem_or ??); #arg3 destruct
2889normalize in match (sem_or ??); #arg4 destruct
2890qed.
2891
2892lemma xor_value_eq :
2893  ∀E,v1,v2,v1',v2'.
2894   value_eq E v1 v2 →
2895   value_eq E v1' v2' →
2896   ∀r1. (sem_xor v1 v1'=Some val r1→
2897           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
2898#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2899@(value_eq_inversion E … Hvalue_eq1)
2900[ 2: #sz #i
2901     @(value_eq_inversion E … Hvalue_eq2)
2902     [ 2: #sz' #i' whd in match (sem_xor ??);
2903          @intsize_eq_elim_elim
2904          [ 1: #_ #Habsurd destruct (Habsurd)
2905          | 2: #Heq destruct (Heq) normalize nodelta
2906               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2907] ]
2908normalize in match (sem_xor ??); #arg1 destruct
2909normalize in match (sem_xor ??); #arg2 destruct
2910normalize in match (sem_xor ??); #arg3 destruct
2911normalize in match (sem_xor ??); #arg4 destruct
2912qed.
2913
2914lemma shl_value_eq :
2915  ∀E,v1,v2,v1',v2'.
2916   value_eq E v1 v2 →
2917   value_eq E v1' v2' →
2918   ∀r1. (sem_shl v1 v1'=Some val r1→
2919           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
2920#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2921@(value_eq_inversion E … Hvalue_eq1)
2922[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2923[ 2:
2924     @(value_eq_inversion E … Hvalue_eq2)
2925     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2926     [ 2: whd in match (sem_shl ??);
2927          cases (lt_u ???) normalize nodelta
2928          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
2929          | 2: #Habsurd destruct (Habsurd)
2930          ]
2931     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2932| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2933qed.
2934
2935lemma shr_value_eq :
2936  ∀E,v1,v2,v1',v2',ty,ty'.
2937   value_eq E v1 v2 →
2938   value_eq E v1' v2' →
2939   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
2940           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
2941#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
2942@(value_eq_inversion E … Hvalue_eq1)
2943[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
2944whd in match (sem_shr ????); whd in match (sem_shr ????);
2945[ 1: cases (classify_aop ty ty') normalize nodelta
2946     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2947     #Habsurd destruct (Habsurd)
2948| 2: cases (classify_aop ty ty') normalize nodelta
2949     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2950     [ 2,3: #Habsurd destruct (Habsurd) ]
2951     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2952     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
2953     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2954     elim sg normalize nodelta
2955     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
2956     /3 by ex_intro, conj, refl, vint_eq/
2957| 3: cases (classify_aop ty ty') normalize nodelta
2958     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2959     #Habsurd destruct (Habsurd)
2960| 4: cases (classify_aop ty ty') normalize nodelta
2961     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2962     #Habsurd destruct (Habsurd)
2963| 5: cases (classify_aop ty ty') normalize nodelta
2964     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
2965     #Habsurd destruct (Habsurd)
2966] qed.
2967
2968lemma monotonic_Zlt_Zsucc: monotonic Z Zlt Zsucc.
2969whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle)
2970/3 by monotonic_Zle_Zplus_r, Zle_to_Zlt/ qed.
2971
2972lemma monotonic_Zlt_Zpred: monotonic Z Zlt Zpred.
2973whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle)
2974/3 by monotonic_Zle_Zpred, Zle_to_Zlt/ qed.
2975
2976lemma antimonotonic_Zle_Zsucc: ∀x,y. Zsucc x ≤ Zsucc y → x ≤ y.
2977#x #y #H lapply (monotonic_Zle_Zpred … H) >Zpred_Zsucc >Zpred_Zsucc #H @H
2978qed.
2979
2980(*
2981lemma antimonotonic_Zle_Zpred: ∀x,y. Zpred x ≤ Zpred y → x ≤ y.
2982#x #y #H lapply (monotonic_Zle_Zsucc … H) >Zsucc_Zpred >Zsucc_Zpred #H @H
2983qed. *)
2984
2985lemma antimonotonic_Zlt_Zsucc: ∀x,y. Zsucc x < Zsucc y → x < y.
2986#x #y #Hlt lapply (Zle_to_Zlt … (antimonotonic_Zle_Zsucc … (Zlt_to_Zle … Hlt)))
2987>Zpred_Zsucc #H @H
2988qed.
2989
2990lemma antimonotonic_Zlt_Zpred: ∀x,y. Zpred x < Zpred y → x < y.
2991#x #y #Hlt lapply (monotonic_Zlt_Zsucc … Hlt) >Zsucc_Zpred >Zsucc_Zpred #H @H
2992qed.
2993
2994lemma not_Zlt_to_Zltb_false : ∀n,m. n ≮ m → Zltb n m = false.
2995#n #m #Hnlt
2996@Zltb_elim_Type0
2997[ 1: elim Hnlt #H0 #H1 @(False_ind … (H0 H1))
2998| 2: #_ @refl ] qed.
2999
3000lemma Zplus_eq_eq : ∀x,y,delta:Z. eqZb x y = eqZb (x + delta) (y + delta).
3001#x #y #delta
3002@eqZb_elim
3003[ 1: #Heq >Heq >eqZb_z_z @refl
3004| 2: * #Hneq cut (x+delta ≠ y + delta)
3005     [ 1: % #H cut (x = y) [ 1: @(injective_Zplus_l delta) @H ] #H' @Hneq @H' ]
3006     #H @sym_eq @eqZb_false @H ] qed.
3007     
3008lemma Zltb_Zsucc : ∀x,y. Zltb x y = Zltb (Zsucc x) (Zsucc y).
3009#x #y
3010@(Zltb_elim_Type0 … x y)
3011[ 1: #Hlt @sym_eq lapply (monotonic_Zlt_Zsucc … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt')
3012| 2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc
3013      lapply (antimonotonic_Zlt_Zsucc … Hltsucc) #Hlt
3014      @(absurd … Hlt Hnlt)
3015] qed.
3016
3017lemma Zltb_Zpred : ∀x,y. Zltb x y = Zltb (Zpred x) (Zpred y).
3018#x #y
3019@(Zltb_elim_Type0 … x y)
3020[ 1: #Hlt @sym_eq
3021lapply (monotonic_Zlt_Zpred … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt')
3022| 2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc
3023      lapply (antimonotonic_Zlt_Zpred … Hltsucc) #Hlt
3024      @(absurd … Hlt Hnlt)
3025] qed.           
3026
3027lemma Zplus_pos_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (pos delta)) (y + (pos delta)).
3028#x #y #delta @(pos_elim … delta)
3029[ 1: >(sym_Zplus x) >(sym_Zplus y) <Zsucc_Zplus_pos_O <Zsucc_Zplus_pos_O
3030     >Zltb_Zsucc @refl
3031| 2: #n #Hind >Hind >Zltb_Zsucc
3032     >(sym_Zplus x) >(sym_Zplus y)
3033     <Zplus_Zsucc <Zplus_Zsucc
3034     >(sym_Zplus ? x) >(sym_Zplus ? y)
3035     normalize in match (Zsucc ?); @refl
3036] qed.
3037
3038lemma Zplus_neg_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (neg delta)) (y + (neg delta)).
3039#x #y #delta @(pos_elim … delta)
3040[ 1: >(sym_Zplus x) >(sym_Zplus y) <Zpred_Zplus_neg_O <Zpred_Zplus_neg_O
3041     >Zltb_Zpred @refl
3042| 2: #n #Hind >Hind >Zltb_Zpred
3043     >(sym_Zplus x) >(sym_Zplus y)
3044     <Zplus_Zpred <Zplus_Zpred
3045     >(sym_Zplus ? x) >(sym_Zplus ? y)
3046     normalize in match (Zpred ?); @refl
3047] qed.
3048
3049(* I would not be surprised for a simpler proof that mine to exist. *)
3050lemma Zplus_lt_lt : ∀x,y,delta:Z. Zltb x y = Zltb (x + delta) (y + delta).
3051#x #y #delta
3052cases delta
3053[ 1: >Zplus_z_OZ >Zplus_z_OZ @refl
3054| 2: #p @Zplus_pos_lt_lt
3055| 3: #p @Zplus_neg_lt_lt
3056] qed.
3057
3058(* offset equality is invariant by translation *)
3059lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
3060#delta #x #y normalize
3061elim delta #zdelta @sym_eq @Zplus_eq_eq qed.
3062
3063lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
3064#delta #x #y normalize
3065elim delta #zdelta @sym_eq <Zplus_eq_eq @refl qed.
3066
3067lemma cmp_offset_translation : ∀op,delta,x,y.
3068   cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
3069* #delta #x #y normalize
3070elim delta #zdelta
3071[ 1: @Zplus_eq_eq
3072| 2: <Zplus_eq_eq @refl
3073| 3: @Zplus_lt_lt
3074| 4: <Zplus_lt_lt @refl
3075| 5: @Zplus_lt_lt
3076| 6: <Zplus_lt_lt @refl
3077qed.
3078
3079lemma cmp_value_eq :
3080  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
3081   value_eq E v1 v2 →
3082   value_eq E v1' v2' →
3083   memory_inj E m1 m2 →   
3084   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
3085           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
3086#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
3087elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj
3088whd in match (sem_cmp ??????) in ⊢ ((??%?) → %);
3089cases (classify_cmp ty ty') normalize nodelta
3090[ 1: #tsz #tsg
3091     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
3092     [ 1: #v #Habsurd destruct (Habsurd)
3093     | 3: #f #Habsurd destruct (Habsurd)
3094     | 4: #Habsurd destruct (Habsurd)
3095     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
3096     #sz #i
3097     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
3098     [ 1: #v #Habsurd destruct (Habsurd)
3099     | 3: #f #Habsurd destruct (Habsurd)
3100     | 4: #Habsurd destruct (Habsurd)
3101     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
3102     #sz' #i' cases tsg normalize nodelta
3103     @intsize_eq_elim_elim
3104     [ 1,3: #Hneq #Habsurd destruct (Habsurd)
3105     | 2,4: #Heq destruct (Heq) normalize nodelta
3106            #Heq destruct (Heq)     
3107            [ 1: cases (cmp_int ????) whd in match (of_bool ?);
3108            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
3109              /3 by ex_intro, conj, vint_eq/ ]
3110| 3: #fsz
3111     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
3112     [ 1: #v #Habsurd destruct (Habsurd)
3113     | 2: #sz #i #Habsurd destruct (Habsurd)
3114     | 4: #Habsurd destruct (Habsurd)
3115     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
3116     #f
3117     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
3118     [ 1: #v #Habsurd destruct (Habsurd)
3119     | 2: #sz #i #Habsurd destruct (Habsurd)
3120     | 4: #Habsurd destruct (Habsurd)
3121     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
3122     #f'
3123     #Heq destruct (Heq) cases (Fcmp op f f')
3124     /3 by ex_intro, conj, vint_eq/
3125| 4: #ty1 #ty2 #Habsurd destruct (Habsurd)
3126| 2: #optn #typ             
3127     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
3128     [ 1: #v #Habsurd destruct (Habsurd)
3129     | 2: #sz #i #Habsurd destruct (Habsurd)
3130     | 3: #f #Habsurd destruct (Habsurd)
3131     | 5: #p1 #p2 #Hembed ]
3132     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
3133     [ 1,6: #v #Habsurd destruct (Habsurd)
3134     | 2,7: #sz #i #Habsurd destruct (Habsurd)
3135     | 3,8: #f #Habsurd destruct (Habsurd)
3136     | 5,10: #p1' #p2' #Hembed' ]
3137     [ 2,3: cases op whd in match (sem_cmp_mismatch ?);
3138          #Heq destruct (Heq)
3139          [ 1,3: %{Vfalse} @conj try @refl @vint_eq
3140          | 2,4: %{Vtrue} @conj try @refl @vint_eq ]
3141     | 4: cases op whd in match (sem_cmp_match ?);
3142          #Heq destruct (Heq)
3143          [ 2,4: %{Vfalse} @conj try @refl @vint_eq
3144          | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ]
3145     lapply (mi_valid_pointers … Hinj p1' p2')
3146     lapply (mi_valid_pointers … Hinj p1 p2)         
3147     cases (valid_pointer (mk_mem ???) p1')
3148     [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
3149     cases (valid_pointer (mk_mem ???) p1)
3150     [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
3151     #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
3152     >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
3153     elim p1 in Hembed; #b1 #o1
3154     elim p1' in Hembed'; #b1' #o1'
3155     whd in match (pointer_translation ??);
3156     whd in match (pointer_translation ??);
3157     @(eq_block_elim … b1 b1')
3158     [ 1: #Heq destruct (Heq)
3159          cases (E b1') normalize nodelta
3160          [ 1: #Habsurd destruct (Habsurd) ]
3161          * #eb1' #eo1' normalize nodelta
3162          #Heq1 #Heq2 #Heq3 destruct
3163          >eq_block_identity normalize nodelta
3164          <cmp_offset_translation
3165          cases (cmp_offset ???) normalize nodelta         
3166          /3 by ex_intro, conj, vint_eq/
3167     | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
3168          cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
3169          * #eb1 #eo1
3170          cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
3171          * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
3172          lapply (H ???? Hneq (refl ??) (refl ??))
3173          #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
3174          elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
3175          /3 by ex_intro, conj, vint_eq/
3176     ]
3177] qed.               
3178 
3179(* Commutation result for binary operators. *)
3180lemma binary_operation_value_eq :
3181  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
3182   value_eq E v1 v2 →
3183   value_eq E v1' v2' →
3184   memory_inj E m1 m2 →
3185   ∀r1.
3186   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
3187   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
3188#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
3189cases op
3190whd in match (sem_binary_operation ??????);
3191whd in match (sem_binary_operation ??????);
3192[ 1: @add_value_eq try assumption
3193| 2: @sub_value_eq try assumption
3194| 3: @mul_value_eq try assumption
3195| 4: @div_value_eq try assumption
3196| 5: @mod_value_eq try assumption
3197| 6: @and_value_eq try assumption
3198| 7: @or_value_eq try assumption
3199| 8: @xor_value_eq try assumption
3200| 9: @shl_value_eq try assumption
3201| 10: @shr_value_eq try assumption
3202| *: @cmp_value_eq try assumption
3203] qed.
3204
3205lemma cast_value_eq :
3206 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 →
3207  ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res →
3208  ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'.
3209#E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res
3210@(value_eq_inversion … Hvalue_eq)
3211[ 1: #v normalize #Habsurd destruct (Habsurd)
3212| 2: #vsz #vi whd in match (exec_cast ????);
3213     cases ty
3214     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
3215     normalize nodelta
3216     [ 1,3,7,8,9: #Habsurd destruct (Habsurd)
3217     | 2: @intsize_eq_elim_elim
3218          [ 1: #Hneq #Habsurd destruct (Habsurd)
3219          | 2: #Heq destruct (Heq) normalize nodelta
3220               cases cast_ty
3221               [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
3222               | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
3223               normalize nodelta
3224               [ 1,7,8,9: #Habsurd destruct (Habsurd)
3225               | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
3226               | 3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/
3227               | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
3228                    @eq_bv_elim
3229                    [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta
3230                         whd in match (m_bind ?????);
3231                         #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
3232                    | 2,4,6: #Hneq >eq_intsize_identity normalize nodelta
3233                         whd in match (m_bind ?????);
3234                         #Habsurd destruct (Habsurd) ] ]
3235          ]
3236     | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
3237          @eq_bv_elim
3238          [ 1,3,5: #Heq destruct (Heq) normalize nodelta
3239               whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
3240          | 2,4,6: #Hneq normalize nodelta
3241               whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ]
3242     ]
3243| 3: #f whd in match (exec_cast ????);
3244     cases ty
3245     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
3246     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
3247     normalize nodelta
3248     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
3249     cases cast_ty
3250     [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
3251     | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
3252     normalize nodelta
3253     [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
3254     #Heq destruct (Heq)
3255     [ 1: /3 by ex_intro, conj, vint_eq/
3256     | 2: /3 by ex_intro, conj, vfloat_eq/ ]
3257| 4: whd in match (exec_cast ????);
3258     cases ty
3259     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
3260     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
3261     normalize
3262     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
3263     cases cast_ty normalize nodelta
3264     [ 1,10,19: #Habsurd destruct (Habsurd)
3265     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
3266     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
3267     | 4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
3268     | 5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
3269     | 6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
3270     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
3271     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
3272     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
3273| 5: #p1 #p2 #Hembed whd in match (exec_cast ????);
3274     cases ty
3275     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
3276     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
3277     normalize
3278     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
3279     cases cast_ty normalize nodelta
3280     [ 1,10,19: #Habsurd destruct (Habsurd)
3281     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
3282     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
3283     | 4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption
3284     | 5,14,23: #carrayty #cn #Heq destruct (Heq)
3285                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
3286     | 6,15,24: #ctl #cretty #Heq destruct (Heq)
3287                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
3288     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
3289     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
3290     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
3291qed.
3292
3293lemma bool_of_val_value_eq :
3294 ∀E,v1,v2. value_eq E v1 v2 →
3295   ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b.
3296#E #v1 #v2 #Hvalue_eq #ty #b
3297@(value_eq_inversion … Hvalue_eq) //
3298[ 1: #v #H normalize in H; destruct (H)
3299| 2: #p1 #p2 #Hembed #H @H ] qed.
3300 
3301(* Simulation relation on expressions *)
3302lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
3303  ∀E:embedding.
3304  ∀Hext:memory_ext E m1 m2.
3305  switch_removal_globals E ? fundef_switch_removal ge ge' →
3306  disjoint_extension en1 m1 en2 m2 ext E Hext →
3307  ext_fresh_for_genv ext ge →
3308  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
3309  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
3310#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
3311@expr_lvalue_ind_combined
3312[ 1: #csz #cty #i #a1
3313     whd in match (exec_expr ????); elim cty
3314     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
3315     normalize nodelta
3316     [ 2: cases (eq_intsize csz sz) normalize nodelta
3317          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
3318          | 2: #Habsurd destruct (Habsurd) ]
3319     | 4,5,6: #_ #H destruct (H)
3320     | *: #H destruct (H) ]
3321| 2: #ty #fl #a1
3322     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
3323| 3: *
3324  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
3325  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
3326  #ty whd in ⊢ (% → ?); #Hind try @I
3327  whd in match (Plvalue ???);
3328  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
3329       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
3330       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
3331       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
3332           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
3333           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
3334           whd in match (load_value_of_type' ???);
3335           whd in match (load_value_of_type' ???);
3336           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
3337           cases (load_value_of_type ty m1 bl1 o1)
3338           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3339           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
3340                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
3341                    normalize /4 by ex_intro, conj/
3342  ] ] ]
3343| 4: #v #ty whd * * #b1 #o1 #tr1
3344     whd in match (exec_lvalue' ?????);
3345     whd in match (exec_lvalue' ?????);
3346     lapply (Hdisjoint v)
3347     lapply (Hext_fresh_for_genv v)
3348     cases (mem_assoc_env v ext) #Hglobal
3349     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
3350          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
3351          >(Hglobal (refl ??)) normalize
3352          #Habsurd destruct (Habsurd)
3353     | 2: normalize nodelta
3354          cases (lookup ?? en1 v) normalize nodelta
3355          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
3356               lapply (rg_find_symbol … Hrelated v)
3357               cases (find_symbol ???) normalize
3358               [ 1: #_ #Habsurd destruct (Habsurd)
3359               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
3360                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
3361                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
3362                         %{〈block',mk_offset OZ,[]〉} @conj try @refl
3363                         normalize /2/
3364                ] ]
3365         | 2: #block
3366              cases (lookup ?? en2 v) normalize nodelta
3367              [ 1: #Hfalse @(False_ind … Hfalse)
3368              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
3369                   %{〈b, zero_offset, E0〉} @conj try @refl
3370                   normalize /2/
3371    ] ] ]
3372| 5: #e #ty whd in ⊢ (% → %);
3373     whd in match (exec_lvalue' ?????);
3374     whd in match (exec_lvalue' ?????);
3375     cases (exec_expr ge en1 m1 e)
3376     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
3377          * elim v1 normalize nodelta
3378          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
3379          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
3380          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
3381          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
3382          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
3383               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
3384               #Hvalue_eq normalize
3385               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
3386               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
3387               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
3388               %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
3389               normalize @conj // ]
3390     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
3391| 6: #ty #e #ty'
3392     #Hsim @(exec_lvalue_expr_elim … Hsim)
3393     cases ty
3394     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
3395     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
3396     #tr #H @conj try @refl try assumption
3397| 7: #ty #op #e
3398     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
3399     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
3400     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
3401     [ 1: #_ @I
3402     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
3403           normalize /2/ ]
3404| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
3405     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
3406     cases (exec_expr ge en1 m1 e2) in Hsim2;
3407     [ 2: #error // ]
3408     * #val #trace normalize in ⊢ (% → ?); #Hsim2
3409     elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2
3410     whd in match (m_bind ?????); whd in match (m_bind ?????);
3411     lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext))
3412     cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1)
3413     [ 1: #_ // ]
3414     #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq  #Hvalue_eq_opval
3415     >Hopval_eq normalize destruct /2 by conj/
3416| 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
3417     #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty)
3418     cases (exec_cast m1 v1 (typeof e) cast_ty)
3419     [ 2: #error #_ normalize @I
3420     | 1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????);
3421          * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta
3422          @conj // ]
3423| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
3424     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
3425     lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1))
3426     cases (exec_bool_of_val ? (typeof e1)) #b
3427     [ 2: #_ normalize @I ]
3428     #H lapply (H ? (refl ??)) #Hexec >Hexec normalize
3429     cases b normalize nodelta
3430     [ 1: (* true branch *)
3431          cases (exec_expr ge en1 m1 e2) in Hsim2;
3432          [ 2: #error normalize #_ @I
3433          | 1: * #e2v #e2tr normalize #H elim (H ? (refl ??))
3434               * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize
3435                    destruct @conj try // ]
3436     | 2: (* false branch *)
3437          cases (exec_expr ge en1 m1 e3) in Hsim3;
3438          [ 2: #error normalize #_ @I
3439          | 1: * #e3v #e3tr normalize #H elim (H ? (refl ??))
3440               * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize
3441               destruct @conj // ] ]
3442| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
3443     @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq
3444     lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1))     
3445     cases (exec_bool_of_val v1 (typeof e1))
3446     [ 2,4:  #error #_ normalize @I ]
3447     #b cases b #H lapply (H ? (refl ??)) #Heq >Heq
3448     whd in match (m_bind ?????);
3449     whd in match (m_bind ?????);
3450     [ 2,3: normalize @conj try @refl try @vint_eq ]
3451     cases (exec_expr ge en1 m1 e2) in Hsim2;
3452     [ 2,4: #error #_ normalize @I ]
3453     * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??))
3454     * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta
3455     lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2))
3456     cases (exec_bool_of_val v2 (typeof e2))
3457     [ 2,4: #error #_ normalize @I ]
3458     #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta
3459     destruct @conj try @conj //
3460     cases b2 whd in match (of_bool ?); @vint_eq
3461| 13: #ty #ty' cases ty
3462     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n
3463     | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
3464     whd in match (exec_expr ????); whd
3465     * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉}
3466     @conj try @refl @conj //
3467| 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta
3468    whd in match (exec_lvalue' ?????);
3469    whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
3470    whd in match (typeof ?);
3471    cases aggregty in Hsim;
3472    [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
3473    | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
3474    normalize nodelta #Hsim
3475    [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
3476    whd in match (m_bind ?????);
3477    whd in match (m_bind ?????);
3478    whd in match (exec_lvalue ge en1 m1 (Expr ed ?));
3479    cases (exec_lvalue' ge en1 m1 ed ?) in Hsim;
3480    [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
3481    * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??))
3482    * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq
3483    whd in match (exec_lvalue ????); >Hexec normalize nodelta
3484    [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj //
3485         normalize @conj // ]
3486    cases (field_offset i fl')
3487    [ 2: #error normalize #Habsurd destruct (Habsurd) ]
3488    #offset whd in match (m_bind ?????); #Heq destruct (Heq)
3489    whd in match (m_bind ?????);
3490    %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj
3491    destruct // normalize nodelta @conj try @refl @vptr_eq
3492    -H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq
3493    whd in match (pointer_translation ??);     
3494    whd in match (pointer_translation ??);
3495    cases (E b)
3496    [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
3497    * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq)
3498    cut (offset_plus (mk_offset (offv o1+Z_of_signed_bitvector (bitsize_of_intsize I32) (repr I32 offset))) o'
3499          = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset)))
3500    [ normalize >associative_Zplus >(sym_Zplus ? (offv o')) in ⊢ (??%?); <associative_Zplus @refl ]
3501    #Heq >Heq @refl
3502| 15: #ty #l #e #Hsim
3503     @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj //
3504| 16: *
3505  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
3506  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
3507  #ty normalize in ⊢ (% → ?);
3508  [ 3,4,13: @False_ind
3509  | *: #_ normalize #a1 #Habsurd destruct (Habsurd) ]
3510] qed.   
3511
3512
3513(*
3514lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
3515related_globals ? fundef_switch_removal ge ge' →
3516∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
3517#ge #ge' #en #m #Hrelated #args
3518elim args
3519[ 1: /3/
3520| 2: #hd #tl #Hind normalize
3521     elim (sim_related_globals ge ge' en m Hrelated)
3522     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
3523     cases (exec_expr ge en m hd)
3524     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
3525     | 1: * #val_hd #trace_hd normalize nodelta
3526          cases Hind
3527          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
3528          | 1: cases (exec_exprlist ge en m tl)
3529               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
3530               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
3531                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
3532                    cases Hexec_hd
3533                    [ 2: * #error #Habsurd destruct (Habsurd)
3534                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
3535] ] ] ] qed.
3536*)
3537
3538(* The return type of any function is invariant under switch removal *)
3539lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
3540#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
3541qed.
3542
3543(* Similar stuff for fundefs *)
3544lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
3545* // qed.
3546
3547(*
3548lemma expr_fresh_lift :
3549  ∀e,u,id.
3550      fresh_for_expression e u →
3551      fresh_for_univ SymbolTag id u →
3552      fresh_for_univ SymbolTag (max_of_expr e id) u.
3553#e #u #id
3554normalize in match (fresh_for_expression e u);
3555#H1 #H2
3556>max_of_expr_rewrite
3557normalize in match (fresh_for_univ ???);
3558cases (max_of_expr e ?) in H1; #p #H1
3559cases id in H2; #p' #H2
3560normalize nodelta
3561cases (leb p p') normalize nodelta
3562[ 1: @H2 | 2: @H1 ]
3563qed. *)
3564
3565lemma while_fresh_lift : ∀e,s,u.
3566   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
3567#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
3568cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
3569cases (leb e s) try /2/
3570qed.
3571
3572(*
3573lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
3574#e0 #s0 #us0 normalize
3575cases (switch_removal s0 us0) * #body #newvars #u' normalize //
3576qed.*)
3577
3578lemma dowhile_fresh_lift : ∀e,s,u.
3579   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
3580#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
3581cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
3582cases (leb e s) try /2/
3583qed.
3584(*
3585lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
3586#e0 #s0 #us0 normalize
3587cases (switch_removal s0 us0) * #body #newvars #u' normalize //
3588qed.*)
3589
3590lemma for_fresh_lift : ∀cond,step,body,u.
3591  fresh_for_statement step u →
3592  fresh_for_statement body u →
3593  fresh_for_expression cond u →
3594  fresh_for_statement (Sfor Sskip cond step body) u.
3595#cond #step #body #u
3596whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
3597cases (max_of_statement step) #s
3598cases (max_of_statement body) #b
3599cases (max_of_expr cond) #c
3600whd in match (max_of_statement Sskip);
3601>(max_id_commutative least_identifier)
3602>max_id_one_neutral normalize nodelta
3603normalize elim u #u
3604cases (leb s b) cases (leb c b) cases (leb c s) try /2/
3605qed.
3606
3607(*
3608lemma for_commute : ∀e,stm1,stm2,u,uA.
3609   (uA=\snd  (switch_removal stm1 u)) →
3610   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
3611#e #stm1 #stm2 #u #uA #HuA
3612whd in match (sw_rem (Sfor ????) u);
3613whd in match (switch_removal ??);   
3614destruct
3615normalize in match (\snd (switch_removal Sskip u));
3616whd in match (sw_rem stm1 u);
3617cases (switch_removal stm1 u)
3618* #stm1' #fresh_vars #uA normalize nodelta
3619whd in match (sw_rem stm2 uA);
3620cases (switch_removal stm2 uA)
3621* #stm2' #fresh_vars2 #uB normalize nodelta
3622//
3623qed.*)
3624
3625(*
3626lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
3627*
3628[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
3629| 2: #e1 #e2 #u #_
3630     whd in match (sw_rem ??);
3631     whd in match (is_Sskip ?);
3632     try /2 by refl, ex_intro/
3633| 3: #ret #f #args #u
3634     whd in match (sw_rem ??);
3635     whd in match (is_Sskip ?);
3636     try /2 by refl, ex_intro/
3637| 4: #s1 #s2 #u
3638     whd in match (sw_rem ??);
3639     whd in match (switch_removal ??);     
3640     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
3641     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
3642     whd in match (is_Sskip ?);
3643     try /2 by refl, ex_intro/
3644| 5: #e #s1 #s2 #u #_
3645     whd in match (sw_rem ??);
3646     whd in match (switch_removal ??);     
3647     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3648     cases (switch_removal ? ?) * #e #f #h normalize nodelta
3649     whd in match (is_Sskip ?);
3650     try /2 by refl, ex_intro/
3651| 6,7: #e #s #u #_
3652     whd in match (sw_rem ??);
3653     whd in match (switch_removal ??);     
3654     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3655     whd in match (is_Sskip ?);
3656     try /2 by refl, ex_intro/
3657| 8: #s1 #e #s2 #s3 #u #_     
3658     whd in match (sw_rem ??);
3659     whd in match (switch_removal ??);     
3660     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3661     cases (switch_removal ? ?) * #e #f #g normalize nodelta
3662     cases (switch_removal ? ?) * #i #j #k normalize nodelta
3663     whd in match (is_Sskip ?);
3664     try /2 by refl, ex_intro/
3665| 9,10: #u #_     
3666     whd in match (is_Sskip ?);
3667     try /2 by refl, ex_intro/
3668| 11: #e #u #_
3669     whd in match (is_Sskip ?);
3670     try /2 by refl, ex_intro/
3671| 12: #e #ls #u #_
3672     whd in match (sw_rem ??);
3673     whd in match (switch_removal ??);
3674     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
3675     cases (fresh ??) #e #f normalize nodelta
3676     normalize in match (simplify_switch ???);
3677     cases (fresh ? f) #g #h normalize nodelta
3678     cases (produce_cond ????) * #k #l #m normalize nodelta
3679     whd in match (is_Sskip ?);
3680     try /2 by refl, ex_intro/
3681| 13,15: #lab #st #u #_
3682     whd in match (sw_rem ??);
3683     whd in match (switch_removal ??);
3684     cases (switch_removal ? ?) * #a #b #c normalize nodelta
3685     whd in match (is_Sskip ?);
3686     try /2 by refl, ex_intro/
3687| 14: #lab #u     
3688     whd in match (is_Sskip ?);
3689     try /2 by refl, ex_intro/ ]
3690qed.
3691*)
3692
3693(*
3694lemma sw_rem_commute : ∀stm,u.
3695  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
3696#stm #u whd in match (sw_rem stm u); // qed.
3697*)
3698
3699lemma fresh_for_statement_inv :
3700  ∀u,s. fresh_for_statement s u →
3701        match u with
3702        [ mk_universe p ⇒ le (p0 one) p ].
3703* #p #s whd in match (fresh_for_statement ??);
3704cases (max_of_statement s) #s
3705normalize /2/ qed.
3706
3707lemma fresh_for_Sskip :
3708  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
3709#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3710
3711lemma fresh_for_Sbreak :
3712  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
3713#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3714
3715lemma fresh_for_Scontinue :
3716  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
3717#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
3718
3719(*
3720lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
3721#s #u elim (switch_removal s u) * #res #fvs #u'
3722%{res} %{fvs} %{u'} //
3723qed.
3724
3725lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
3726#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
3727%{res} %{fvs} %{u'} //
3728qed.
3729*)
3730
3731lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
3732#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
3733#s #lab #u' %{s} %{lab} %{u'} //
3734qed.
3735
3736(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
3737lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
3738* * *
3739[ 1,5,9: #H @(False_ind … (H (refl ??)))
3740| *: #_ normalize @refl ]
3741qed.
3742
3743lemma exec_expr_int : ∀ge,e,m,expr.
3744    (∃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〉)).
3745#ge #e #m #expr cases (exec_expr ge e m expr)
3746[ 2: #error %2 #sz #n #tr % #H destruct (H)
3747| 1: * #val #trace cases val
3748     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
3749     | 3: #fl | 4: | 5: #ptr ]
3750     %2 #sz #n #tr % #H destruct (H)
3751] qed.
3752
3753(*
3754lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
3755  exec_expr ge e m cond = OK ? 〈v,tr〉 →
3756  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
3757  exec_expr ge' e m cond = OK ? 〈v,tr〉.
3758#ge #ge' #e #m #cond #v #tr #H *
3759[ 1: #Hsim >(Hsim ? H) //
3760| 2: * #error >H #Habsurd destruct (Habsurd) ]
3761qed. *)
3762
3763(*
3764lemma switch_simulation :
3765∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
3766 switch_cont_sim k k' →
3767 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
3768 fresh_for_statement (Sswitch cond switchcases) u →
3769 ∃tr'.
3770 (eventually ge'
3771  (λs2':state
3772   .switch_state_sim
3773    (State f
3774     (seq_of_labeled_statement (select_switch condsz condval switchcases))
3775     (Kswitch k) e m) s2')
3776  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
3777  tr').
3778#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
3779whd in match (sw_rem (Sswitch cond switchcases) u);
3780whd in match (switch_removal (Sswitch cond switchcases) u);
3781cases switchcases in Hfresh;
3782[ 1: #default_statement #Hfresh_for_default
3783     whd in match (switch_removal_branches ??);
3784     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
3785     elim (switch_removal_eq default_statement u)
3786     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
3787     normalize nodelta
3788     cut (u' = (\snd (switch_removal default_statement u)))
3789     [ 1: >Hdefault_statement_eq // ] #Heq_u'
3790     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
3791     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
3792     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
3793     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
3794     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
3795     normalize nodelta
3796     whd in match (simplify_switch (Expr ??) ?? uv2);
3797     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
3798     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
3799     -Hfreshness #Heq_uv3
3800     normalize nodelta whd in match (add_starting_lbl_list ????);
3801     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
3802     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
3803     -Hfreshness #Heq_uv4
3804     normalize nodelta
3805     @(eventually_later ge' ?? E0)
3806     whd in match (exec_step ??);
3807     %{(State (function_switch_removal f)
3808          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
3809          (Kseq
3810          (Ssequence
3811            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
3812            (Slabel exit_label Sskip))
3813          k') e m)} @conj try //
3814     @(eventually_later ge' ?? E0)
3815     whd in match (exec_step ??);
3816     
3817@chthulhu | @chthulhu
3818qed. *)
3819
3820
3821
3822(* Main theorem. To be ported and completed to memory injections. TODO *)
3823(*
3824theorem switch_removal_correction : ∀ge, ge'.
3825  related_globals ? fundef_switch_removal ge ge' →
3826  ∀s1, s1', tr, s2.
3827  switch_state_sim s1 s1' →
3828  exec_step ge s1 = Value … 〈tr,s2〉 →
3829  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
3830#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
3831inversion Hsim_state
3832[ 1: (* regular state *)
3833  #u #f #s #k #k' #m #m' #result #en #en' #f' #vars
3834  #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_
3835
3836  lapply (sim_related_globals ge ge' e m Hrelated) *
3837  #Hexpr_related #Hlvalue_related
3838  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
3839  cases s in Hu_fresh Heq_env;
3840 
3841
3842theorem switch_removal_correction : ∀ge, ge'.
3843  related_globals ? fundef_switch_removal ge ge' →
3844  ∀s1, s1', tr, s2.
3845  switch_state_sim s1 s1' →
3846  exec_step ge s1 = Value … 〈tr,s2〉 →
3847  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
3848#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
3849inversion Hsim_state
3850[ 1: (* regular state *)
3851  #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_
3852  lapply (sim_related_globals ge ge' e m Hrelated) *
3853  #Hexpr_related #Hlvalue_related
3854  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
3855  cases s in Hu_fresh Heq_env;
3856  (* Perform the intros for the statements*)
3857  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
3858  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
3859  | 14: #lab | 15: #cost #body ]
3860  #Hu_fresh #Heq_env
3861  [ 1: (* Skip *)
3862    whd in match (sw_rem ??);
3863    inversion Hsim_cont normalize nodelta
3864    [ 1: #Hk #Hk' #_ #Hexec_step
3865         @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify
3866         cases (fn_return f) in Hexec_step;
3867         [ 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
3868         | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
3869         normalize nodelta
3870         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H)
3871                %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try //
3872                normalize in Heq_env; destruct (Heq_env)
3873                %3 //
3874(*                cut (blocks_of_env e = blocks_of_env e')
3875                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
3876                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
3877                #Heq >Heq %3 // *)
3878         | *: #H destruct (H) ]
3879    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3880         whd in match (ret ??) in Heq; destruct (Heq)
3881         @(eventually_now ????) whd in match (exec_step ??);
3882         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
3883         %1 try //   
3884    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3885         @(eventually_now ????) whd in match (exec_step ??);
3886         whd in match (ret ??) in Heq; destruct (Heq)
3887         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
3888         >while_commute %1 try //
3889    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3890         @(eventually_now ????) whd in match (exec_step ??);
3891         lapply (Hexpr_related e0)
3892         cases (exec_expr ge e m e0) in Heq;
3893         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
3894         | 1: * #b #tr whd in match (m_bind ?????); #Heq
3895              *
3896              [ 2: * #error #Habsurd destruct (Habsurd)
3897              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
3898                   whd in match (bindIO ??????);
3899                   cases (exec_bool_of_val b (typeof e0)) in Heq;
3900                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3901                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
3902                        whd in match (bindIO ??????);
3903                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
3904                             @conj // >dowhile_commute %1 try //
3905                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
3906                             @conj // %1{us} try //
3907                             @(fresh_for_Sskip … Hus_fresh)
3908                        ] ] ] ]
3909    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
3910         @(eventually_now ????) whd in match (exec_step ??);
3911         whd in match (ret ??) in Heq; destruct
3912         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
3913         @conj try // %1{u} try //
3914    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
3915         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
3916         destruct (Heq)
3917         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
3918         @conj try // %1
3919         [ 2: @swc_for3 //
3920         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
3921    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
3922         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
3923         destruct (Heq)
3924         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
3925         @conj try // <(for_commute ??? u uA) try // %1
3926         [ 2: assumption
3927         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
3928    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
3929         #Heq @(eventually_now ????) whd in match (exec_step ??);
3930         destruct (Heq)
3931         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
3932         %1{u} //
3933    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
3934         @(eventually_now ????) whd in match (exec_step ??);
3935         >fn_return_simplify cases (fn_return f) in Heq;
3936         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
3937         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
3938         normalize nodelta
3939         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
3940              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
3941              @conj try // %3 destruct //
3942         | *: #H destruct (H) ]     
3943     ]
3944  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
3945       whd in match (exec_step ??);
3946       cases lhs in Hu_fresh Heq; #lhs #lhs_type
3947       cases (Hlvalue_related lhs lhs_type)
3948       whd in match (exec_lvalue ge e m (Expr ??));
3949       whd in match (exec_lvalue ge' e m (Expr ??));
3950       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
3951       cases (exec_lvalue' ge e m lhs lhs_type)
3952       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
3953       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
3954            whd in match (m_bind ?????);
3955            cases (Hexpr_related rhs)
3956            [ 2: * #error #Hfail >Hfail #_
3957                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3958            | 1: cases (exec_expr ge e m rhs)
3959                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3960                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
3961                      whd in match (bindIO ??????) in ⊢ (% → % → %);
3962                      cases (opt_to_io io_out io_in ???)
3963                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
3964                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3965                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
3966                           %{(State (function_switch_removal f) Sskip k' e mem)}
3967                           whd in match (bindIO ??????); @conj //
3968                           %1{u} try // @(fresh_for_Sskip … Hfresh)
3969       ] ] ] ]
3970   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
3971        whd in match (exec_step ??);
3972        cases (Hexpr_related func) in Heq;
3973        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
3974        | 1: cases (exec_expr ge e m func)
3975             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
3976             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
3977                  whd in match (m_bind ?????); normalize nodelta
3978                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
3979                  #Hexprlist_sim cases (Hexprlist_sim args)
3980                  [ 2: * #error #Hfail >Hfail
3981                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3982                  | 1: cases (exec_exprlist ge e m args)
3983                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
3984                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
3985                            whd in match (bindIO ??????) in ⊢ (% → %);
3986                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
3987                            cases (find_funct clight_fundef ge fval)
3988                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
3989                                 whd in match (bindIO ??????) in ⊢ (% → %);
3990                                 >fundef_type_simplify
3991                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
3992                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3993                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
3994                                      cases retv normalize nodelta
3995                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
3996                                           %{(Callstate (fundef_switch_removal clfd) values
3997                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
3998                                           @conj try // %2 try // @swc_call //
3999                                      | 2: * #retval_ed #retval_type
4000                                           whd in match (exec_lvalue ge ???);
4001                                           whd in match (exec_lvalue ge' ???);                                     
4002                                           elim (Hlvalue_related retval_ed retval_type)
4003                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
4004                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
4005                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
4006                                                     destruct (Habsurd)
4007                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
4008                                                     whd in match (m_bind ?????) in ⊢ (% → %);
4009                                                     #Heq destruct (Heq)
4010                                                     %{(Callstate (fundef_switch_removal clfd) values
4011                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
4012                                                               (function_switch_removal f) e k') m)}
4013                                                     @conj try //
4014                                                     %2 @swc_call //
4015                                ] ] ] ]
4016                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
4017                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
4018       ] ] ] ] ]
4019   | 4: (* Ssequence *) normalize nodelta
4020        whd in match (ret ??) in ⊢ (% → ?); #Heq
4021        @(eventually_now ????)
4022        %{(State (function_switch_removal f)
4023                 (\fst (\fst (switch_removal stm1 u)))
4024                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
4025        @conj
4026        [ 2: destruct (Heq) %1
4027             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
4028             | 2: @swc_seq try // @switch_removal_fresh
4029                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
4030        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
4031             cases (switch_removal stm1 u)
4032             * #stm1' #fresh_vars #u' normalize nodelta
4033             cases (switch_removal stm2 u')
4034             * #stm2' #fresh_vars2 #u'' normalize nodelta
4035             whd in match (exec_step ??);
4036             destruct (Heq) @refl
4037        ]
4038   | 5: (* If-then-else *) normalize nodelta
4039        whd in match (ret ??) in ⊢ (% → ?); #Heq
4040        @(eventually_now ????) whd in match (sw_rem ??);
4041        whd in match (switch_removal ??);
4042        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
4043        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
4044        whd in match (exec_step ??);
4045        cases (Hexpr_related cond) in Heq;
4046        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
4047        | 1: cases (exec_expr ge e m cond)
4048             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
4049             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
4050                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
4051                  cases (exec_bool_of_val condval (typeof cond))
4052                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
4053                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
4054                       destruct (Heq_condval) whd in match (bindIO ??????);
4055                       normalize nodelta
4056                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
4057                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
4058                           [ 1: >Hiftrue_eq normalize // ]
4059                           #Hrewrite >Hrewrite %1
4060                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
4061                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
4062                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
4063                           [ 1: >Hiffalse_eq // ]
4064                           #Hrewrite >Hrewrite %1 try //
4065                           cut (uA = (\snd (switch_removal iftrue u)))
4066                           [ 1: >Hiftrue_eq //
4067                           | 2: #Heq_uA >Heq_uA
4068                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
4069                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
4070       ] ] ] ] ]
4071   | 6: (* While loop *) normalize nodelta
4072        whd in match (ret ??) in ⊢ (% → ?); #Heq
4073        @(eventually_now ????) whd in match (sw_rem ??);
4074        whd in match (switch_removal ??);
4075        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
4076        whd in match (exec_step ??);
4077        cases (Hexpr_related cond) in Heq;
4078        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
4079        | 1: cases (exec_expr ge e m cond)
4080             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
4081             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
4082                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
4083                  cases (exec_bool_of_val condval (typeof cond))
4084                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
4085                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
4086                       destruct (Heq_condval) whd in match (bindIO ??????);
4087                       normalize nodelta
4088                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
4089                            cut (body' = (\fst (\fst (switch_removal body u))))
4090                            [ 1: >Hbody_eq // ]
4091                            #Hrewrite >Hrewrite %1
4092                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
4093                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
4094                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
4095                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
4096        ] ] ] ]
4097   | 7: (* Dowhile loop *) normalize nodelta
4098        whd in match (ret ??) in ⊢ (% → ?); #Heq
4099        @(eventually_now ????) whd in match (sw_rem ??);
4100        whd in match (switch_removal ??);
4101        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
4102        whd in match (exec_step ??);
4103        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
4104        try //
4105        cut (body' = (\fst (\fst (switch_removal body u))))
4106        [ 1: >Hbody_eq // ]
4107        #Hrewrite >Hrewrite %1
4108        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
4109        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
4110   | 8: (* For loop *) normalize nodelta
4111        whd in match (ret ??) in ⊢ (% → ?); #Heq
4112        @(eventually_now ????) whd in match (sw_rem ??);
4113        whd in match (switch_removal ??);
4114        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
4115        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
4116              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
4117              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
4118              whd in match (exec_step ??);
4119              cases (Hexpr_related cond)
4120              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
4121              | 1: cases (exec_expr ge e m cond)
4122                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
4123                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
4124                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
4125                        cases (exec_bool_of_val condval (typeof cond))
4126                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
4127                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
4128                             destruct (Heq_condval)
4129                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
4130                                  try //
4131                                  cut (body' = (\fst (\fst (switch_removal body uA))))
4132                                  [ 1: >Hbody_eq // ]
4133                                  #Hrewrite >Hrewrite
4134                                  cut (uA = (\snd (switch_removal step u)))
4135                                  [ 1: >Hstep_eq // ] #HuA
4136                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
4137                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
4138                                  [ 1: >HuA @switch_removal_fresh assumption
4139                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
4140                                       [ >Hstep_eq // ]
4141                                       #Hstep >Hstep @swc_for2 try assumption
4142                                       @for_fresh_lift try assumption ]
4143                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
4144                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
4145               ] ] ] ]
4146        | 2: #Heq
4147             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
4148             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
4149             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
4150             whd in match (exec_step ??);
4151             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
4152             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
4153             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
4154             whd in match (ret ??); destruct (Heq)
4155             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
4156             @conj try //
4157             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
4158             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
4159             <for_commute [ 2: >Hstep_eq // ]
4160             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
4161             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
4162             @swc_seq try // @for_fresh_lift
4163             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
4164             >HuA_eq @switch_removal_fresh assumption       
4165       ]
4166   | 9: (* break *) normalize nodelta
4167        inversion Hsim_cont
4168        [ 1: #Hk #Hk' #_       
4169        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
4170        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
4171        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
4172        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
4173        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
4174        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
4175        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
4176        normalize nodelta #H try (destruct (H))
4177        whd in match (ret ??) in H; destruct (H)
4178        @(eventually_now ????)
4179        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
4180        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
4181    | 10: (* Continue *) normalize nodelta
4182        inversion Hsim_cont
4183        [ 1: #Hk #Hk' #_       
4184        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
4185        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
4186        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
4187        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
4188        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
4189        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
4190        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
4191        normalize nodelta #H try (destruct (H))
4192        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
4193        destruct (H)
4194        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
4195        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
4196             >while_commute %1{u0} try assumption
4197        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
4198             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
4199             | 1: * #condval #trace whd in match (m_bind ?????);
4200                  #Heq *
4201                  [ 2: * #error #Habsurd destruct (Habsurd)
4202                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
4203                       whd in match (bindIO ??????);
4204                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
4205                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
4206                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
4207                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)}
4208                                 @conj try // >dowhile_commute %1{u0} assumption
4209                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
4210                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
4211             ] ] ]
4212        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
4213             try // @(fresh_for_Scontinue … Hfor_fresh)
4214        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
4215             @conj try // %1{u0}
4216             elim (substatement_fresh … Hfor_fresh) * * try //
4217             #HSskip #Hcond #Hstep #Hbody
4218             @swc_for3 assumption
4219        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
4220             %1{u} try //
4221        ]
4222    | 11: (* Sreturn *) normalize nodelta #Heq
4223          @(eventually_now ????)
4224          whd in match (exec_step ??) in Heq ⊢ %;
4225          cases retval in Heq; normalize nodelta
4226          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
4227               whd in match (ret ??) in ⊢ (% → %);
4228               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
4229               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
4230               #H destruct (H)
4231               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
4232               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
4233          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
4234               [ 1: #_ #Habsurd destruct (Habsurd)
4235               | 2: #_ elim (Hexpr_related expr)
4236                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
4237                    | 1: cases (exec_expr ??? expr)
4238                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
4239                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
4240                              #Hrewrite >Hrewrite
4241                              whd in match (m_bind ?????); whd in match (m_bind ?????);
4242                              #Heq destruct (Heq)
4243                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
4244                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
4245         ] ] ] ]
4246    | 12: (* Sswitch. Main proof case. *) normalize nodelta
4247          (* Case analysis on the outcome of the tested expression *)
4248          cases (exec_expr_int ge e m cond)
4249          [ 2: cases (exec_expr ge e m cond)
4250               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
4251               | 1: * #val #trace cases val
4252                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
4253                    whd in match (m_bind ?????);
4254                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
4255                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
4256          ]
4257          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
4258          whd in match (m_bind ?????); #Heq
4259          destruct (Heq)
4260          @eventually_later
4261          whd in match (sw_rem (Sswitch cond switchcases) u);
4262          whd in match (switch_removal (Sswitch cond switchcases) u);
4263          elim (switch_removal_branches_eq switchcases u)
4264          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
4265          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
4266          [ 1: >Hsrb_eq // ] #Huv1_eq
4267          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
4268          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
4269          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
4270          whd in match (simplify_switch ???);
4271          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
4272          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
4273          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)         
4274          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
4275          #Huv4_eq
4276          whd in match (exec_step ??);
4277          %{(State (function_switch_removal f)
4278                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
4279                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
4280          %{E0} @conj try @refl
4281          %{tr} normalize in match (eq ???); @conj try //
4282          (* execute the conditional *)
4283          @eventually_later
4284          (* lift the result of the previous case analysis from [ge] to [ge'] *)
4285          whd in match (exec_step ??);
4286          whd in match (exec_lvalue ????);
4287         
4288          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
4289         
4290  *)
4291 
Note: See TracBrowser for help on using the repository browser.