source: src/Clight/switchRemoval.ma @ 2353

Last change on this file since 2353 was 2353, checked in by campbell, 7 years ago

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

  • Property svn:executable set to *
File size: 125.9 KB
Line 
1include "Clight/Csyntax.ma".
2include "Clight/fresh.ma".
3include "basics/lists/list.ma".
4include "basics/lists/listb.ma".
5include "common/Identifiers.ma".
6include "utilities/extralib.ma".
7include "Clight/Cexec.ma".
8include "Clight/CexecInd.ma".
9include "Clight/frontend_misc.ma".
10include "Clight/memoryInjections.ma".
11
12(* -----------------------------------------------------------------------------
13   ----------------------------------------------------------------------------*)
14
15(* -----------------------------------------------------------------------------
16   Documentation
17   ----------------------------------------------------------------------------*)
18
19(* This file implements transformation of switches to linear sequences of
20 * if/then/else. The implementation roughly follows the lines of the prototype.
21 * /!\ We assume that the program is well-typed (the type of the evaluated
22 * expression must match the constants on each branch of the switch). /!\ *)
23
24(* Documentation. Let the follwing be our input switch construct:
25   // --------------------------------- 
26   switch(e) {
27   case v1:
28     stmt1
29   case v2:
30     stmt2
31   .
32   .
33   .
34   default:
35     stmt_default
36   }
37   // --------------------------------- 
38 
39   Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting
40   the switch statement. In the absence of break, the execution falls through each case sequentially.
41 
42   Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos:
43
44   // --------------------------------- 
45   fresh = e;
46   if(fresh == v1) {
47     stmt1';
48     goto lbl_case2;
49   }
50   if(fresh == v2) {
51     lbl_case2:
52     stmt2';
53     goto lbl_case2;
54   }   
55   ...
56   stmt_default';
57   exit_label:
58   // ---------------------------------   
59
60   where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements
61   were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels.
62*)
63
64
65(* -----------------------------------------------------------------------------
66   Definitions allowing to state that the program resulting of the transformation
67   is switch-free.
68   ---------------------------------------------------------------------------- *)
69
70(* Property of a Clight statement of containing no switch. Could be generalized into a kind of
71 * statement_P, if useful elsewhere. *)
72let rec switch_free (st : statement) : Prop ≝
73match st with
74[ Sskip ⇒ True
75| Sassign _ _ ⇒ True
76| Scall _ _ _ ⇒ True
77| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
78| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
79| Swhile e body _ ⇒ switch_free body
80| Sdowhile e body ⇒ switch_free body
81| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
82| Sbreak ⇒ True
83| Scontinue ⇒ True
84| Sreturn _ ⇒ True
85| Sswitch _ _ ⇒ False
86| Slabel _ body ⇒ switch_free body
87| Sgoto _ ⇒ True
88| Scost _ body ⇒ switch_free body
89].
90
91(* Property of a list of labeled statements of being switch-free *)
92let rec branches_switch_free (sts : labeled_statements) : Prop ≝
93match sts with
94[ LSdefault st =>
95  switch_free st
96| LScase _ _ st tl =>
97  switch_free st ∧ branches_switch_free tl
98].
99
100let rec branches_ind
101  (sts : labeled_statements)
102  (H   : labeled_statements → Prop) 
103  (defcase : ∀st. H (LSdefault st))
104  (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝
105match sts with
106[ LSdefault st ⇒
107  defcase st
108| LScase sz int st tl ⇒
109  indcase sz int st tl (branches_ind tl H defcase indcase)
110].
111
112(* -----------------------------------------------------------------------------
113   Switch-removal code for statements, functions and fundefs.
114   ----------------------------------------------------------------------------*)
115
116(* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
117let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
118match st with
119[ Sbreak ⇒
120  Sgoto lab
121| Ssequence s1 s2 ⇒
122  Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab)
123| Sifthenelse e iftrue iffalse ⇒
124  Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab)
125| Sfor init e update body ⇒
126  Sfor (convert_break_to_goto init lab) e update body
127| Slabel l body ⇒
128  Slabel l (convert_break_to_goto body lab)
129| Scost cost body ⇒
130  Scost cost (convert_break_to_goto body lab)
131| _ ⇒ st
132].
133
134(* Converting breaks preserves switch-freeness. *)
135lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label).
136#s elim s //
137[ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
138| 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
139| 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
140     try @conj try @conj /3/
141| 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/
142| 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/
143] qed.
144
145(*  (def_case : ident × sf_statement) *)
146
147let rec produce_cond
148  (e : expr)
149  (switch_cases : labeled_statements)
150  (u : universe SymbolTag)
151  (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝
152match switch_cases with
153[ LSdefault st ⇒ 
154  let 〈lab,u1〉 ≝ fresh ? u in
155  let st' ≝ convert_break_to_goto st exit in
156  〈Slabel lab st', lab, u1〉
157| LScase sz tag st other_cases ⇒
158  let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in
159  let st' ≝ convert_break_to_goto st exit in
160  let 〈lab, u2〉 ≝ fresh ? u1 in
161  let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in
162  let case_statement ≝
163       Sifthenelse test
164        (Slabel lab (Ssequence st' (Sgoto sub_label)))
165        Sskip
166  in
167  〈Ssequence case_statement sub_statements, lab, u2〉
168].
169
170definition simplify_switch ≝
171   λ(e : expr).
172   λ(switch_cases : labeled_statements).
173   λ(uv : universe SymbolTag).
174 let 〈exit_label, uv1〉            ≝ fresh ? uv in
175 let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in
176 〈Ssequence result (Slabel exit_label Sskip), uv2〉.
177
178lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))).
179#l @(labeled_statements_ind … l)
180[ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1
181     normalize in Hsf ⊢ %; @(convert_break_lift … Hsf)
182| 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl
183     #e #lab #u normalize
184     lapply (Hind Hsf_tl e lab u)
185     cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta
186     cases (fresh ??) #lab0 #u2 normalize nodelta
187     normalize try @conj try @conj try @conj try //
188     @(convert_break_lift … Hsf_hd)
189] qed.
190
191lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)).
192#e #l cases l
193[ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta
194     whd @conj whd
195     [ 1: @convert_break_lift assumption
196     | 2: @I ]
197| 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u
198     cases (fresh ? u) #exit_label #uv1 normalize nodelta
199     lapply (produce_cond_switch_free tl Hsftl e exit_label uv1)
200     cases (produce_cond e tl uv1 exit_label)
201     * #cond #lab #u1 #Hsf_cond normalize nodelta
202     cases (fresh ??) #lab0 #u2 normalize nodelta
203     normalize @conj try @conj try @conj try @conj try //
204     @(convert_break_lift ?? Hsf)
205] qed.
206
207(* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in
208   order to circumvent the associativity problems in notations. *)
209record swret (A : Type[0]) : Type[0] ≝ {
210  ret_st  : A;
211  ret_acc : list (ident × type);
212  ret_fvs : list ident;
213  ret_u   : universe SymbolTag
214}.
215
216notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48
217for @{ match ${e} with
218       [ None ⇒ None ?
219       | Some ${fresh ret} ⇒
220          (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'})
221          (ret_st ? ${fresh ret})
222          (ret_acc ? ${fresh ret})
223          (ret_fvs ? ${fresh ret})
224          (ret_u ? ${fresh ret}) ] }.
225
226notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49
227for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4})  }.
228     
229(* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
230   of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another
231   'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables
232   allows it to proceed without failing. This is all in order to ease the proof of simulation. *)
233let rec switch_removal
234  (st : statement)           (* the statement in which we will remove switches *)
235  (fvs : list ident)         (* a finite list of names usable to create variables. *)
236  (u : universe SymbolTag)   (* a fresh /label/ generator *)
237  : option (swret statement) ≝
238match st with
239[ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
240| Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
241| Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉
242| Ssequence s1 s2 ⇒
243  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
244  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
245  ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉
246| Sifthenelse e s1 s2 ⇒
247  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
248  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
249  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
250| Swhile e body cl ⇒
251  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
252  ret 〈Swhile e body' cl, acc, fvs', u'〉
253| Sdowhile e body ⇒
254  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
255  ret 〈Sdowhile e body', acc, fvs', u'〉
256| Sfor s1 e s2 s3 ⇒
257  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
258  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
259  do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
260  ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
261| Sbreak ⇒
262  ret 〈st, [ ], fvs, u〉
263| Scontinue ⇒
264  ret 〈st, [ ], fvs, u〉
265| Sreturn _ ⇒
266  ret 〈st, [ ], fvs, u〉
267| Sswitch e branches ⇒   
268   do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u;
269   match fvs' with
270   [ nil ⇒ None ?
271   | cons fresh tl ⇒
272     (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *)
273     let ident         ≝ Expr (Evar fresh) (typeof e) in
274     let assign        ≝ Sassign ident e in
275     let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in
276       ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉
277   ]
278| Slabel label body ⇒
279  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
280  ret 〈Slabel label body', acc, fvs', u'〉
281| Sgoto _ ⇒
282  ret 〈st, [ ], fvs, u〉
283| Scost cost body ⇒
284  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
285  ret 〈Scost cost body', acc, fvs', u'〉
286]
287
288and switch_removal_branches
289  (l : labeled_statements)
290  (fvs : list ident)
291  (u : universe SymbolTag)
292(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
293match l with
294[ LSdefault st ⇒
295  do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
296  ret 〈LSdefault st', acc1, fvs', u'〉
297| LScase sz int st tl =>
298  do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u;
299  do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u';
300  ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉
301].
302
303let rec mk_fresh_variables
304  (st : statement)           (* the statement in which we will remove switches *)
305  (u : universe SymbolTag)   (* a fresh /label/ generator *)
306  : (list ident) × (universe SymbolTag) ≝
307match st with
308[ Sskip       ⇒ 〈[ ], u〉
309| Sassign _ _ ⇒ 〈[ ], u〉
310| Scall _ _ _ ⇒ 〈[ ], u〉
311| Ssequence s1 s2 ⇒
312  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
313  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
314  〈fvs @ fvs', u''〉
315| Sifthenelse e s1 s2 ⇒
316  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
317  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
318  〈fvs @ fvs', u''〉
319| Swhile e body cl ⇒
320  mk_fresh_variables body u
321| Sdowhile e body ⇒
322  mk_fresh_variables body u
323| Sfor s1 e s2 s3 ⇒
324  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
325  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
326  let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
327  〈fvs @ fvs' @fvs'', u'''〉
328| Sbreak ⇒
329  〈[ ], u〉
330| Scontinue ⇒
331  〈[ ], u〉
332| Sreturn _ ⇒
333  〈[ ], u〉
334| Sswitch e branches ⇒   
335   let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *)
336   let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in
337   〈fvs @ [ident], u''〉  (* reversing the order to match a proof invariant *)
338| Slabel label body ⇒
339  mk_fresh_variables body u
340| Sgoto _ ⇒
341  〈[ ], u〉
342| Scost cost body ⇒
343  mk_fresh_variables body u
344]
345
346and mk_fresh_variables_branches
347  (l : labeled_statements)
348  (u : universe SymbolTag)
349(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
350match l with
351[ LSdefault st ⇒
352  mk_fresh_variables st u
353| LScase sz int st tl =>
354  let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in
355  let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in
356  〈fvs @ fvs', u''〉
357].
358
359(* Copied this from Csyntax.ma, lifted from Prop to Type
360   (I needed to eliminate something proved with this towards Type)  *)
361let rec statement_indT
362  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
363  (Ssk:P Sskip)
364  (Sas:∀e1,e2. P (Sassign e1 e2))
365  (Sca:∀eo,e,args. P (Scall eo e args))
366  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
367  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
368  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
369  (Sdo:∀e,s. P s → P (Sdowhile e s))
370  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
371  (Sbr:P Sbreak)
372  (Sco:P Scontinue)
373  (Sre:∀eo. P (Sreturn eo))
374  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
375  (Sla:∀l,s. P s → P (Slabel l s))
376  (Sgo:∀l. P (Sgoto l))
377  (Scs:∀l,s. P s → P (Scost l s))
378  (LSd:∀s. P s → Q (LSdefault s))
379  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
380  (s:statement) on s : P s ≝
381match s with
382[ Sskip ⇒ Ssk
383| Sassign e1 e2 ⇒ Sas e1 e2
384| Scall eo e args ⇒ Sca eo e args
385| Ssequence s1 s2 ⇒ Ssq s1 s2
386    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
387    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
388| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
389    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
390    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
391| Swhile e s cl ⇒ Swh e s cl
392    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
393| Sdowhile e s ⇒ Sdo e s
394    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
395| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
396    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
397    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
398    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
399| Sbreak ⇒ Sbr
400| Scontinue ⇒ Sco
401| Sreturn eo ⇒ Sre eo
402| Sswitch e ls ⇒ Ssw e ls
403    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
404| Slabel l s ⇒ Sla l s
405    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
406| Sgoto l ⇒ Sgo l
407| Scost l s ⇒ Scs l s
408    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
409]
410and labeled_statements_indT
411  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
412  (Ssk:P Sskip)
413  (Sas:∀e1,e2. P (Sassign e1 e2))
414  (Sca:∀eo,e,args. P (Scall eo e args))
415  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
416  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
417  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
418  (Sdo:∀e,s. P s → P (Sdowhile e s))
419  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
420  (Sbr:P Sbreak)
421  (Sco:P Scontinue)
422  (Sre:∀eo. P (Sreturn eo))
423  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
424  (Sla:∀l,s. P s → P (Slabel l s))
425  (Sgo:∀l. P (Sgoto l))
426  (Scs:∀l,s. P s → P (Scost l s))
427  (LSd:∀s. P s → Q (LSdefault s))
428  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
429  (ls:labeled_statements) on ls : Q ls ≝
430match ls with
431[ LSdefault s ⇒ LSd s
432    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
433| LScase sz i s t ⇒ LSc sz i s t
434    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
435    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
436].
437
438lemma switch_removal_ok :
439  ∀st, u0, u1, post.
440  Σresult.
441  (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post).
442#st
443@(statement_indT ? (λls. ∀u0, u1, post.
444                          Σresult.
445                          (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result)
446                          ∧ (ret_fvs ? result = post)
447                   ) … st)
448[ 1: #u0 #u1 #post normalize
449     %{(mk_swret statement Sskip [] post u1)} % //
450| 2: #e1 #e2 #u0 #u1 #post normalize
451     %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try //
452| 3: #e0 #e #args #u0 #u1 #post normalize
453     %{(mk_swret statement (Scall e0 e args) [] post u1)} % try //
454| 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
455     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
456     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
457     elim (H2 u' (ret_u ? s1') post) #s2' *
458     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
459     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
460     %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2'))
461        (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
462        (ret_u statement s2'))} % try //
463| 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
464     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *     
465     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
466     elim (H2 u' (ret_u ? s1') post) #s2' *
467     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
468     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
469     %{((mk_swret statement
470         (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
471         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
472         (ret_u statement s2')))} % try //
473| 6: #e #s #cl #H #u0 #u1 #post normalize
474     elim (H u0 u1 post) #s1' * normalize
475     cases (mk_fresh_variables s u0) #fvs #u'
476     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
477     %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
478        (ret_fvs statement s1') (ret_u statement s1'))} % try //
479| 7: #e #s #H #u0 #u1 #post normalize
480     elim (H u0 u1 post) #s1' * normalize
481     cases (mk_fresh_variables s u0) #fvs #u'
482     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
483     %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
484        (ret_fvs statement s1') (ret_u statement s1'))} % try //
485| 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
486     elim (H1 u0 u1
487                (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
488                (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
489                post)) #s1' *
490     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
491     elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 u')))) @
492                                 post)) #s2' *
493     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
494     elim (H3 u'' (ret_u ? s2') post) #s3' *
495     cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta
496     #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs
497     >associative_append >associative_append >Heq1 normalize >Heq1_fvs
498     >Heq2 normalize >Heq2_fvs >Heq3 normalize
499     %{(mk_swret statement
500        (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
501        (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
502        (ret_fvs statement s3') (ret_u statement s3'))} % try //
503| 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
504| 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % //
505| 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % //
506| 12: #e #ls #H #u0 #u1 #post
507      whd in match (mk_fresh_variables ??);
508      whd in match (switch_removal ???);     
509      elim (fresh ? u0) #fresh #u'
510      elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta
511      cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta     
512      >associative_append #Heq #Heq_fvs >Heq normalize nodelta
513      >Heq_fvs normalize nodelta
514      cases (simplify_switch ???) #st' #u''' normalize nodelta
515      %{((mk_swret statement
516          (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st')
517          (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post)
518          (ret_u labeled_statements ls')))} % //
519| 13: #l #s #H #u0 #u1 #post normalize
520      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
521      %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s')
522           post (ret_u statement s'))} % //
523| 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % //
524| 15: #l #s #H #u0 #u1 #post normalize
525      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
526      %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s')
527           post (ret_u statement s'))} % //
528| 16: #s #H #u0 #u1 #post normalize
529      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
530      %{(mk_swret labeled_statements (LSdefault (ret_st statement s'))
531         (ret_acc statement s') post (ret_u statement s'))} % //
532| 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize
533      elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' *
534      cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize
535      elim (H1 u' (ret_u labeled_statements ls') post) #s1' *
536      cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs
537      >associative_append >Heql normalize >Heql_fvs >Heq normalize
538      %{(mk_swret labeled_statements
539          (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls'))
540          (ret_acc labeled_statements ls'@ret_acc statement s1')
541          (ret_fvs statement s1') (ret_u statement s1'))} % //
542] qed.
543
544axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
545
546(* Proof that switch_removal_switch_free does its job. *)
547lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result).
548#st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result →
549                                                 branches_switch_free (ret_st ? ls_result)) … st)
550[ 1: #fvs #u #result normalize #Heq destruct (Heq) //
551| 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) //
552| 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) //
553| 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u)
554     elim (switch_removal s1 fvs u) normalize
555     [ 1: #_ #Habsurd destruct (Habsurd)
556     | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1))
557          elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1))
558          [ 1: normalize #_ #Habsurd destruct (Habsurd)
559          | 2: normalize #res2 #Heq2 #Heq destruct (Heq)
560               normalize @conj
561               [ 1: @Heq1 // | 2: @Heq2 // ]
562     ] ]
563| *:
564  (* TODO the first few cases show that the lemma is routinely proved. TBF later. *)
565  @cthulhu ]
566qed.
567
568(* -----------------------------------------------------------------------------
569   Switch-removal code for programs.
570   ----------------------------------------------------------------------------*) 
571
572(* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to
573 * name clashes for labels. We have no choice but to actually run through the function and to
574 * compute the maximum of labels+identifiers. This way we can generate both fresh variables and
575 * fresh labels using the same univ. While we're at it we also consider record fields.
576 * Cost labels are not considered, though. They already live in a separate universe.
577 *
578 * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes,
579 * but in the end it might be good to move the following functions into fresh.ma.
580 *)
581
582(* Least element in the total order of identifiers. *)
583definition least_identifier ≝ an_identifier SymbolTag one.
584
585(* This is certainly overkill: variables adressed in an expression should be declared in the
586 * enclosing function's prototype. *)
587let rec max_of_expr (e : expr) : ident ≝
588match e with
589[ Expr ed _ ⇒
590  match ed with
591  [ Econst_int _ _ ⇒ least_identifier
592  | Econst_float _ ⇒ least_identifier
593  | Evar id ⇒ id
594  | Ederef e1 ⇒ max_of_expr e1
595  | Eaddrof e1 ⇒ max_of_expr e1
596  | Eunop _ e1 ⇒ max_of_expr e1
597  | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
598  | Ecast _ e1 ⇒ max_of_expr e1
599  | Econdition e1 e2 e3 ⇒ 
600    max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3))
601  | Eandbool e1 e2 ⇒
602    max_id (max_of_expr e1) (max_of_expr e2)
603  | Eorbool e1 e2 ⇒
604    max_id (max_of_expr e1) (max_of_expr e2) 
605  | Esizeof _ ⇒ least_identifier
606  | Efield r f ⇒ max_id f (max_of_expr r)
607  | Ecost _ e1 ⇒ max_of_expr e1
608  ]
609].
610
611(* Reasoning about this promises to be a serious pain. Especially the Scall case. *)
612let rec max_of_statement (s : statement) : ident ≝
613match s with
614[ Sskip ⇒ least_identifier
615| Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
616| Scall r f args ⇒
617  let retmax ≝
618    match r with
619    [ None ⇒ least_identifier
620    | Some e ⇒ max_of_expr e ]
621  in
622  max_id (max_of_expr f)
623         (max_id retmax
624                 (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )
625| Ssequence s1 s2 ⇒
626  max_id (max_of_statement s1) (max_of_statement s2)
627| Sifthenelse e s1 s2 ⇒
628  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
629| Swhile e body _ ⇒
630  max_id (max_of_expr e) (max_of_statement body)
631| Sdowhile e body ⇒
632  max_id (max_of_expr e) (max_of_statement body)
633| Sfor init test incr body ⇒
634  max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body))
635| Sbreak ⇒ least_identifier
636| Scontinue ⇒ least_identifier
637| Sreturn opt ⇒
638  match opt with
639  [ None ⇒ least_identifier
640  | Some e ⇒ max_of_expr e
641  ]
642| Sswitch e ls ⇒
643  max_id (max_of_expr e) (max_of_ls ls)
644| Slabel lab body ⇒
645  max_id lab (max_of_statement body)
646| Sgoto lab ⇒
647  lab
648| Scost _ body ⇒
649  max_of_statement body
650]
651and max_of_ls (ls : labeled_statements) : ident ≝
652match ls with
653[ LSdefault s ⇒ max_of_statement s
654| LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s)
655].
656
657definition max_id_of_function : function → ident ≝
658λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f).
659
660(* We compute fresh universes on a function-by function basis, since there can't
661 * be cross-functions gotos or stuff like that. *)
662definition function_switch_removal : function → function × (list (ident × type)) ≝
663λf.
664  (λres_record.
665    let new_vars ≝ ret_acc ? res_record in
666    let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in
667    〈result, new_vars〉)
668  (let u ≝ universe_of_max (max_id_of_function f) in
669   let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in
670   match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with
671   [ None ⇒ λHsr. ?
672   | Some res_record ⇒ λ_. res_record
673   ] (refl ? (switch_removal (fn_body f) fvs u'))).   
674lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq
675<Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd)
676qed.
677
678let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝
679match f with
680[ CL_Internal f ⇒
681  CL_Internal (\fst (function_switch_removal f))
682| CL_External _ _ _ ⇒
683  f
684].
685
686let rec program_switch_removal (p : clight_program) : clight_program ≝
687 let prog_funcs ≝ prog_funct ?? p in
688 let sf_funcs   ≝ map ?? (λcl_fundef.
689    let 〈fun_id, fun_def〉 ≝ cl_fundef in
690    〈fun_id, fundef_switch_removal fun_def〉
691  ) prog_funcs in
692 mk_program ??
693  (prog_vars … p)
694  sf_funcs
695  (prog_main … p).
696
697
698(* -----------------------------------------------------------------------------
699   Applying two relations on all substatements and all subexprs (directly under).
700   ---------------------------------------------------------------------------- *)
701
702let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝
703match s1 with
704[ Sskip ⇒ True
705| Sassign e1 e2 ⇒ Q e1 ∧ Q e2
706| Scall r f args ⇒
707  match r with
708  [ None ⇒ Q f ∧ (All … Q args)
709  | Some r ⇒ Q r ∧ Q f ∧ (All … Q args)
710  ]
711| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
712| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
713| Swhile e sub _ ⇒ Q e ∧ P sub
714| Sdowhile e sub ⇒ Q e ∧ P sub
715| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
716| Sbreak ⇒ True
717| Scontinue ⇒ True
718| Sreturn r ⇒
719  match r with
720  [ None ⇒ True
721  | Some r ⇒ Q r ]
722| Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P)
723| Slabel _ sub ⇒ P sub
724| Sgoto _ ⇒ True
725| Scost _ sub ⇒ P sub
726]
727and substatement_ls ls (P : statement → Prop) : Prop ≝
728match ls with
729[ LSdefault sub ⇒ P sub
730| LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P)
731].
732
733(* -----------------------------------------------------------------------------
734   Freshness conservation results on switch removal.
735   ---------------------------------------------------------------------------- *)
736
737(* Similar stuff in toCminor.ma. *)
738lemma fresh_for_univ_still_fresh :
739   ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'.
740* #p * #i #H1 #v * #p' lapply H1 normalize
741#H1 #H2 destruct (H2) /2/ qed.
742
743lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'.
744#u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh)
745cases (fresh SymbolTag u)
746#fv #u' #H %{fv} %{u'} @conj try // @H //
747qed.
748
749lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)).
750#e #exit #ls @(branches_ind … ls)
751[ 1: #st #u #i #Hfresh normalize
752     lapply (fresh_for_univ_still_fresh … Hfresh)
753     cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize //
754| 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize
755     lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) *
756     #subcond #sublabel #u1 #Hfresh1 normalize
757     lapply (fresh_for_univ_still_fresh … Hfresh1)
758     cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize //
759] qed.
760
761lemma simplify_switch_fresh : ∀u,i,e,ls.
762 fresh_for_univ ? i u →
763 fresh_for_univ ? i (\snd (simplify_switch e ls u)).
764#u #i #e #ls #Hfresh
765normalize
766lapply (fresh_for_univ_still_fresh … Hfresh)
767cases (fresh ? u)
768#exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux
769normalize lapply (produce_cond_fresh e exit_label ls … Haux)
770elim (produce_cond ????) * #stm #label #uv2 normalize nodelta //
771qed.
772
773(* -----------------------------------------------------------------------------
774   Simulation proof and related voodoo.
775   ----------------------------------------------------------------------------*)
776
777definition expr_lvalue_ind_combined ≝
778λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
779conj ??
780 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
781 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
782 
783let rec expr_ind2
784    (P : expr → Prop) (Q : expr_descr → type → Prop)
785    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
786    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
787    (Iconst_float : ∀f, t. Q (Econst_float f) t)
788    (Ivar : ∀id, t. Q (Evar id) t)
789    (Ideref : ∀e, t. P e → Q (Ederef e) t)
790    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
791    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
792    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
793    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t) 
794    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
795    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
796    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
797    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
798    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
799    (Icost : ∀c,e,t. P e → Q (Ecost c e) t)
800    (e : expr) on e : P e ≝
801match e with
802[ 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) ]
803
804and expr_desc_ind2
805    (P : expr → Prop) (Q : expr_descr → type → Prop)
806    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
807    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
808    (Iconst_float : ∀f, t. Q (Econst_float f) t)
809    (Ivar : ∀id, t. Q (Evar id) t)
810    (Ideref : ∀e, t. P e → Q (Ederef e) t)
811    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
812    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
813    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
814    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t) 
815    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
816    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
817    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
818    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
819    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
820    (Icost : ∀c,e,t. P e → Q (Ecost c e) t)
821    (ed : expr_descr) (t : type) on ed : Q ed t ≝
822match ed with
823[ Econst_int sz i ⇒ Iconst_int sz i t
824| Econst_float f ⇒ Iconst_float f t
825| Evar id ⇒ Ivar id t
826| 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)
827| 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)
828| 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)
829| 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)
830| 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)
831| 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)
832| 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)
833| 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)
834| Esizeof sizeoft ⇒ Isizeof sizeoft t
835| 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)
836| 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)
837].
838
839(* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched
840   by a non-constant number of evaluations in the converted program. More precisely,
841   [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps
842   necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *)
843   
844(* A version of simplify_switch hiding the ugly projs *)
845definition fresh_for_expression ≝
846  λe,u. fresh_for_univ SymbolTag (max_of_expr e) u.
847
848definition fresh_for_statement ≝
849  λs,u. fresh_for_univ SymbolTag (max_of_statement s) u.
850
851(* needed during mutual induction ... *)
852definition fresh_for_labeled_statements ≝
853  λls,u. fresh_for_univ ? (max_of_ls ls) u.
854   
855definition fresh_for_function ≝
856  λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.
857
858(* misc properties of the max function on positives. *)
859
860lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v.
861* #p whd in ⊢ (??%?); >max_one_neutral // qed.
862
863lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1.
864* #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%);
865>commutative_max // qed.
866
867lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3).
868* #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max //
869qed.
870
871lemma 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.
872* #a * #b * #u normalize
873lapply (pos_compare_to_Prop a b)
874cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
875[ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/
876| 2: destruct >reflexive_leb /2/
877| 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/
878] qed.
879
880(* Auxilliary commutation lemma used in [substatement_fresh]. *)
881
882lemma foldl_max : ∀l,a,b.
883  foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l =
884  max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l).
885#l elim l
886[ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl
887| 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%);
888     <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
889] qed.
890
891(* Lookup functions in list environments (used to type local variables in functions) *)     
892let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
893match l with
894[ nil ⇒ false
895| cons hd tl ⇒
896  let 〈id, ty〉 ≝ hd in
897  match identifier_eq SymbolTag i id with
898  [ inl Hid_eq ⇒ true
899  | inr Hid_neq ⇒ mem_assoc_env i tl 
900  ]
901].
902
903let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝
904match l with
905[ nil ⇒ None ?
906| cons hd tl ⇒
907  let 〈id, ty〉 ≝ hd in
908  match identifier_eq SymbolTag i id with
909  [ inl Hid_eq ⇒ Some ? ty
910  | inr Hid_neq ⇒ assoc_env i tl 
911  ]
912].
913
914(* --------------------------------------------------------------------------- *)
915(* Memory extensions (limited form on memoryInjection.ma). Note that we state the
916   properties at the back-end level. *)
917(* --------------------------------------------------------------------------- *) 
918
919(*
920definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_blockb ?.
921* #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2)
922[ 1: #Heq >Heq cases r1 cases r2 normalize
923     >eqZb_reflexive normalize @conj #H destruct (H)
924     try @refl
925| 2: #Hneq cases r1 cases r2 normalize
926     >(eqZb_false … Hneq) normalize @conj
927     #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))
928] qed. *)
929
930(* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end values are equal. *)
931definition load_sim ≝
932λ(m1 : mem).λ(m2 : mem).
933 ∀ptr,bev.
934  beloadv m1 ptr = Some ? bev →
935  beloadv m2 ptr = Some ? bev.
936
937(* The [valid_pointer] property is too weak to be preserved by [free]. We use the following guard. *)
938(* definition freed_pointer ≝ λ(m : mem).λ(p : pointer).
939  low_bound m (pblock p) = OZ ∧
940  high_bound m (pblock p) = OZ. *)
941 
942(* definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. *)
943
944definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.
945
946definition outbound_pointer ≝ λm,p.
947   Zltb (block_id (pblock p)) (nextblock m) = true ∧
948   Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧
949   high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)).
950
951lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p.
952#m #p @conj
953[ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);
954     whd in match (outbound_pointer ??);
955     whd in match (do_if_in_bounds); normalize nodelta
956     cases (Zltb (block_id (pblock p)) (nextblock m))
957     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]     
958     >andb_lsimpl_true normalize nodelta
959     cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
960     [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]
961     >andb_lsimpl_true normalize nodelta
962     lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
963     elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
964     [ 1: #H >H #_ normalize nodelta #_ %1 #A #f /2 by ex_intro/
965     | 2: * #_ #H1 #_ #H2 >(Zleb_true_to_Zleb_true_to_eq … H1 H2) %2 @conj try @conj @refl ]
966| 2: whd in match (valid_pointer ??); *
967     [ 1: whd in match (in_bounds_pointer ??); #H
968          lapply (H bool (λblock,contents,off. true))
969          * #foo whd in match (do_if_in_bounds ????);
970          cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
971          [ 2: #Habsurd destruct (Habsurd) ]
972          >andb_lsimpl_true
973          cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
974          normalize nodelta
975          [ 2: #Habsurd destruct (Habsurd) ]
976          >andb_lsimpl_true
977          elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
978          [ 1: #H >(Zltb_to_Zleb_true … H) #_ @refl
979          | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
980     | 2: whd in match (outbound_pointer ??); * * #Hlt #Hleb >Hlt >Hleb
981          #Hhigh >Hhigh >andb_lsimpl_true
982          lapply (reflexive_Zle … (Z_of_unsigned_bitvector offset_size (offv (poff p))))
983          #Hle >(Zle_to_Zleb_true … Hle) @refl
984     ]
985] qed.
986
987(*
988lemma freed_pointer_dec : ∀m,p. freed_pointer m p ∨ (¬freed_pointer m p).
989#m #p
990whd in match (freed_pointer ??);
991cases (low_bound m (pblock p))
992[ 2,3: #low %2 % * #H destruct (H) ]
993cases (high_bound m (pblock p))
994[ 1: %1 @conj @refl | 2,3: #low %2 % * #_ #H destruct (H) ]
995qed. *)
996
997(* In the limited setting of switch removal, a memory extension is a list of fresh blocks
998 * to which we can write. *)
999record sr_memext (m1 : mem) (m2 : mem) : Type[0] ≝
1000{ me_inj : load_sim m1 m2;
1001  (* A list of blocks where we can write freely *)
1002  me_writeable : list block;   
1003  (* These blocks are valid *)
1004  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b; 
1005  (* And pointers to m1 are oblivious to these blocks *)
1006  me_writeable_ok : ∀p.valid_pointer m1 p = true →
1007                     ¬ (meml ? (pblock p) me_writeable);
1008  (* Valid pointers are still valid in m2. One could think that this is superfluous as
1009     being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer
1010     to be one off the end of a block bound. The internal check in beloadv does not.
1011     valid_pointer should be understood as "pointer making sense" rather than "pointer from
1012     which you can load stuff". [mi_valid_pointers] is used for instance when proving the
1013     semantics preservation for equality testing (where we check that the pointers we
1014     compare are valid before being equal).
1015  *)
1016  me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *)
1017                       valid_pointer m1 p = true →
1018                       valid_pointer m2 p = true
1019}.
1020 
1021(* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension
1022   of the environment [e1] s.t. the new binders are in [new], and such that those
1023   new binders are "writeable" in the memory extension [Hext] *)
1024definition disjoint_extension ≝
1025λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem).
1026λ(new : list (ident × type)). λ(Hext: sr_memext m1 m2).
1027  ∀id. match mem_assoc_env id new with
1028       [ true ⇒
1029           ∃b. lookup ?? e2 id = Some ? b
1030            ∧ meml ? b (me_writeable … Hext)
1031            ∧ lookup ?? e1 id = None ?
1032       | false ⇒ lookup ?? e1 id = lookup ?? e2 id
1033       ].
1034       
1035(* Lift load_sim to loadn. *)
1036lemma load_sim_loadn :
1037 ∀m1,m2. load_sim m1 m2 →
1038 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.
1039#m1 #m2 #Hload_sim #sz
1040elim sz
1041[ 1: #p #res #H @H
1042| 2: #n' #Hind #p #res
1043     whd in match (loadn ???);
1044     whd in match (loadn m2 ??);
1045     lapply (Hload_sim p)
1046     cases (beloadv m1 p) normalize nodelta
1047     [ 1: #_ #Habsurd destruct (Habsurd) ]
1048     #bval #H >(H ? (refl ??)) normalize nodelta
1049     lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))
1050     cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')
1051     normalize nodelta
1052     [ 1: #_ #Habsurd destruct (Habsurd) ]
1053     #res' #H >(H ? (refl ??)) normalize
1054     #H @H
1055] qed.
1056 
1057(* Lift load_sim to front-end values. *)
1058lemma load_sim_fe :
1059  ∀m1,m2. load_sim m1 m2 →
1060  ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →
1061            load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.
1062#m1 #m2 #Hloadsim #ptr #ty #v
1063cases ty
1064[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
1065| 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
1066whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
1067[ 1,7,8: #Habsurd destruct (Habsurd)
1068| 5,6: #H @H
1069| 2,3,4,9:
1070  generalize in match (mk_pointer (pblock ptr) (poff ptr));
1071  elim (typesize ?)
1072  [ 1,3,5,7: #p #H @H
1073  | 2,4,6,8: #n' #Hind #p
1074      lapply (load_sim_loadn … Hloadsim (S n') p)
1075      cases (loadn m1 p (S n')) normalize nodelta
1076      [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]     
1077      #bv #H >(H ? (refl ??)) #H @H
1078  ]
1079] qed.
1080
1081(* Lemmas relating memory extensions to [free] *)
1082
1083(* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)
1084lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true.
1085* #contents #next #nextpos #ptr #res
1086whd in match (beloadv ??);
1087whd in match (valid_pointer ??);
1088cases (Zltb (block_id (pblock ptr)) next)
1089normalize nodelta
1090[ 2: #Habsurd destruct (Habsurd) ]
1091>andb_lsimpl_true
1092whd in match (low_bound ??);
1093whd in match (high_bound ??);
1094cases (Zleb (low (contents (pblock ptr)))
1095        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
1096[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
1097>andb_lsimpl_true
1098normalize nodelta #H
1099@Zltb_to_Zleb_true
1100cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
1101try // normalize #Habsurd destruct (Habsurd) qed.
1102
1103lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
1104* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
1105@(eqZb_elim … bid1 bid2)
1106[ 1: #Heq >Heq cases br1 cases br2 normalize
1107     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
1108     #_ @refl
1109| 2: cases br1 cases br2 normalize #_ #_ @refl ]
1110qed.
1111
1112lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
1113* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
1114@(eqZb_elim … bid1 bid2)
1115[ 1: #Heq >Heq cases br1 cases br2 normalize
1116     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
1117     #_ @refl
1118| 2: cases br1 cases br2 normalize #_ #_ @refl ]
1119qed.
1120
1121lemma beloadv_free_blocks_neq :
1122  ∀m,block,pblock,poff,res.
1123  beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
1124* #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
1125normalize
1126cases (Zltb pbid next) normalize nodelta
1127[ 2: #Habsurd destruct (Habsurd) ]
1128cases pbr cases br normalize nodelta
1129[ 2,3: #_ % #Habsurd destruct (Habsurd) ]
1130@(eqZb_elim pbid bid) normalize nodelta
1131#Heq destruct (Heq)
1132[ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
1133#_ % #H destruct (H) elim Heq #H @H @refl
1134qed.
1135
1136(*
1137lemma be_to_fe_value_inj : ∀bv1,bv2.
1138    be_to_fe_value (ASTint I8 Unsigned) [bv1]
1139  = be_to_fe_value (ASTint I8 Unsigned) [bv2] → bv1 = bv2.
1140#bv1 #bv2
1141whd in match (be_to_fe_value ??);
1142whd in match (be_to_fe_value ??);
1143cases bv1 normalize nodelta
1144[ 1: cases bv2 normalize nodelta
1145     [ 1: #H @refl | 2:
1146try //
1147[ cases bv2 *)
1148
1149lemma beloadv_free_beloadv :
1150  ∀m,block,ptr,res.
1151    beloadv (free m block) ptr = Some ? res →
1152    beloadv m ptr = Some ? res.
1153* #contents #next #nextpos #block * #pblock #poff #res
1154#H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq
1155lapply H
1156whd in match (beloadv ??);
1157whd in match (beloadv ??) in ⊢ (? → %);
1158whd in match (nextblock (free ??));
1159cases (Zltb (block_id pblock) next)
1160[ 2: normalize #Habsurd destruct (Habsurd) ]
1161normalize nodelta
1162<(low_free_eq … Hblocks_neq)
1163<(high_free_eq … Hblocks_neq)
1164whd in match (free ??);
1165whd in match (update_block ?????);
1166@(eq_block_elim … pblock block)
1167[ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ]
1168#_ normalize nodelta
1169#H @H
1170qed.
1171
1172lemma beloadv_free_beloadv2 :
1173  ∀m,block,ptr,res.
1174  pblock ptr ≠ block →
1175  beloadv m ptr = Some ? res →
1176  beloadv (free m block) ptr = Some ? res.
1177* #contents #next #nextpos #block * #pblock #poff #res #Hneq
1178whd in match (beloadv ??);
1179whd in match (beloadv ??) in ⊢ (? → %);
1180whd in match (nextblock (free ??));
1181cases (Zltb (block_id pblock) next)
1182[ 2: normalize #Habsurd destruct (Habsurd) ]
1183normalize nodelta
1184<(low_free_eq … Hneq)
1185<(high_free_eq … Hneq)
1186whd in match (free ??);
1187whd in match (update_block ?????);
1188@(eq_block_elim … pblock block)
1189[ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ]
1190#_ normalize nodelta
1191#H @H
1192qed.
1193
1194lemma beloadv_free_simulation :
1195  ∀m1,m2,block,ptr,res.
1196  ∀mem_hyp : sr_memext m1 m2. 
1197  beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res.
1198* #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2
1199* #br #bid * * #pr #pid #poff #res *
1200#Hload_sim #Hme_writeable #Hme_writeable_valid #Hptr_not_mem #Hvalid_conserv
1201#Hload
1202lapply (beloadv_free_beloadv … Hload) #Hload_before_free
1203lapply (beloadv_free_blocks_neq … Hload) #Hblocks_neq
1204@beloadv_free_beloadv2
1205[ 1: @Hblocks_neq ]
1206@Hload_sim assumption
1207qed.
1208
1209lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
1210#m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
1211#H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
1212elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
1213[ 1: #Hlt >Hlt normalize nodelta
1214     @(eq_block_elim … b (pblock p))
1215     [ 1: #Heq >Heq whd in match (free ??);
1216          whd in match (update_block ?????); >eq_block_b_b
1217          normalize nodelta normalize in match (low ?);
1218          >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta
1219          #Habsurd destruct (Habsurd)
1220     | 2: #Hblock_neq whd in match (free ? ?);
1221          whd in match (update_block ?????);
1222          >(not_eq_block_rev … Hblock_neq) normalize nodelta
1223          cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
1224          [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
1225          >andb_lsimpl_true
1226          lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p)))
1227                                     (high (blocks m (pblock p))))
1228          cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
1229          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
1230          normalize nodelta #H #_ /2 by ex_intro/
1231     ]
1232| 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ]
1233qed.
1234
1235lemma outbound_free_to_outbound : ∀m,b,p. outbound_pointer (free m b) p → outbound_pointer m p.
1236#m #b #p whd in match (free ??);
1237whd in match (outbound_pointer ??) in ⊢ (% → %);
1238whd in match (update_block ????);
1239whd in match (low_bound ??); whd in match (high_bound ??);
1240@(eq_block_elim … (pblock p) b) normalize nodelta
1241[ 1: #Heq >Heq cases (Zltb ? (nextblock m))
1242     [ 2: * * #Habsurd destruct (Habsurd) ]
1243     * * #_ whd in match (low ?); whd in match (high ?);
1244     #H1 #H2 <H2 in H1; normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1245| 2: #Hneq #H @H ]
1246qed.
1247
1248lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
1249#m #b #p #Hvalid
1250lapply (valid_pointer_def … m p) * #_ #Hdef @Hdef
1251elim (valid_pointer_def … (free m b) p) #H #_
1252elim (H Hvalid)
1253[ 1: #Hin %1 @in_bounds_free_to_in_bounds assumption
1254| 2: #Hout %2 @outbound_free_to_outbound assumption ]
1255qed.
1256
1257lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
1258#m #b #p
1259whd in match (valid_pointer ??);
1260whd in match (free ??);
1261whd in match (update_block ????);
1262whd in match (low_bound ??);
1263whd in match (high_bound ??);
1264@(eq_block_elim … b (pblock p))
1265[ 1: #Heq >Heq >eq_block_b_b normalize nodelta
1266     whd in match (low ?); whd in match (high ?);
1267     cases (Zltb ? (nextblock m))
1268     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
1269     >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd)
1270| 2: #Hneq #_ @Hneq ]
1271qed.
1272
1273lemma valid_pointer_free : ∀m1,m2. sr_memext m1 m2 → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true.
1274#m1 #m2 #Hext #p #b #Hvalid
1275lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free
1276lapply (me_valid_pointers … Hext … Hvalid_before_free)
1277lapply (valid_after_free … Hvalid) #Hneq
1278whd in match (free ??);
1279whd in match (update_block ????);
1280whd in match (valid_pointer ??) in ⊢ (% → %);
1281whd in match (low_bound ??) in ⊢ (% → %);
1282whd in match (high_bound ??) in ⊢ (% → %);
1283>(not_eq_block_rev … Hneq) normalize nodelta #H @H
1284qed.
1285
1286(* Performing a [free] preserves memory extensions. *)
1287lemma free_memory_ext :
1288  ∀m1,m2,bl.
1289   sr_memext m1 m2 →
1290   sr_memext (free m1 bl) (free m2 bl).
1291#m1 #m2 #bl #Hext
1292%
1293[ 1: @(λptr,bev. beloadv_free_simulation m1 m2 bl ptr bev Hext)
1294| 2: @(filter ? (λwb. notb (eq_block wb bl)) (me_writeable … Hext))
1295| 3: #b #Hmem
1296     cut (mem block b (me_writeable m1 m2 Hext))
1297     [ elim (me_writeable m1 m2 Hext) in Hmem;
1298       [ 1: #H @H
1299       | 2: #h #tl #Hind whd in match (filter ???);
1300            @(eq_block_elim … h bl) normalize in match (notb ?); normalize nodelta
1301            [ 1: #Heq #H whd in match (meml ???); destruct %2 @Hind @H
1302            | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
1303                 [ 1: #H %1 @H
1304                 | 2: #H %2 @Hind @H ] ] ] ]
1305    #Hmem2 lapply (me_writeable_valid … Hmem2)
1306    elim m2 #contents #nextblock #pos elim b #br #bid
1307    normalize #H @H
1308| 4: #p #Hvalid elim (valid_pointer_free_ok_alt … Hvalid)
1309     [ 1: #Heq >Heq elim (me_writeable m1 m2 Hext)
1310        [ 1: normalize % //
1311        | 2: #hd #tl #Hind
1312             whd in match (filter ???);
1313             @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
1314             [ 1: #Heq @Hind
1315             | 2: #Hneq whd in match (meml ???); % *
1316                  [ 1: #Heq elim Hneq #H @H @(sym_eq … Heq)
1317                  | 2: #H elim Hind #Hind @Hind @H ] ] ]
1318    | 2: * #_ #Hvalid lapply (me_writeable_ok … Hext … Hvalid)
1319        * #Hyp % #Htarget @Hyp
1320        elim (me_writeable m1 m2 Hext) in Htarget;
1321        [ 1: normalize //
1322        | 2: #hd #tl #Hind
1323             whd in match (filter ???);
1324             @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
1325             [ 1: #Heq whd in match (meml ???) in ⊢ (? → %);
1326                  #H %2 @Hind @H
1327             | 2: #Hneq whd in match (meml ???);
1328                  whd in match (meml ???) in ⊢ (? → %); *
1329                  [ 1: #H %1 @H
1330                  | 2: #H %2@Hind @H ] ] ] ]
1331| 5: #p @valid_pointer_free @Hext
1332] qed.
1333
1334
1335lemma free_list_memory_ext :
1336  ∀l,m1,m2.
1337   sr_memext m1 m2 →
1338   sr_memext (free_list m1 l) (free_list m2 l).
1339#l elim l
1340[ 1: #m1 #m2 #H @H
1341| 2: #hd #tl #Hind #m1 #m2 #H >free_list_cons >free_list_cons
1342     @free_memory_ext @Hind @H
1343] qed.
1344
1345(* Extend the previous lemma to [free_list] *)
1346lemma beloadv_free_list_memory_ext :
1347  ∀m1,m2,blocks,ptr,res.
1348  ∀mem_hyp : sr_memext m1 m2. 
1349  beloadv (free_list m1 blocks) ptr = Some ? res → beloadv (free_list m2 blocks) ptr = Some ? res.
1350#m1 #m2 #blocks #mtr #res #Hext #Hload
1351lapply (free_list_memory_ext blocks … Hext) #Hext_list
1352lapply (me_inj … Hext_list) #H @H @Hload
1353qed.
1354
1355
1356(* Prove that memory extensions are preserved by free.*)
1357(*
1358lemma memext_free_conservation :
1359  ∀m1,m2 : mem.
1360  ∀mem_hyp : sr_memext m1 m2.
1361  ∀env,env_ext.
1362  ∀new_vars.
1363  ∀env_hyp : disjoint_extension env m1 env_ext m2 new_vars mem_hyp.
1364   (sr_memext (free_list m1 (blocks_of_env env))
1365     (free_list m2 (blocks_of_env env_ext))).
1366#m1 #m2 * #Hloadsim #Hwriteable #Hwritevalid #Holdnotwriteable #Hvalidok #env #env_ext #new_vars
1367whd in ⊢ (% → ?); #Hdisjoint *)
1368
1369
1370(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
1371 * the variable is not in a local environment, then we search into the global one.
1372 * A proper "extension" of a local environment should be such that the extension
1373 * does not collide with a given global env.
1374 * To see the details of why we need that, see [exec_lvalue'], Evar id case.
1375 *)
1376definition ext_fresh_for_genv ≝
1377λ(ext : list (ident × type)). λ(ge : genv).
1378  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.
1379
1380(* Any environment is a "disjoint" extension of itself with nothing. *)
1381(*
1382lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].
1383#e #m #ty #id
1384normalize in match (mem_assoc_env id []); normalize nodelta
1385cases (lookup ?? e id) try //
1386#b normalize nodelta
1387% #ty cases (load_value_of_type ????)
1388[ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj //
1389cases (assoc_env id ty) //
1390qed. *)
1391
1392(* "generic" simulation relation on [res ?] *)
1393definition res_sim ≝
1394  λ(A : Type[0]).
1395  λ(r1, r2 : res A).
1396  ∀a. r1 = OK ? a → r2 = OK ? a.
1397
1398(* Specialisation of [res_sim] to match [exec_expr] *)
1399definition exec_expr_sim ≝ res_sim (val × trace).
1400
1401(* Specialisation of [res_sim] to match [exec_lvalue] *)
1402definition exec_lvalue_sim ≝ res_sim (block × offset × trace).
1403
1404lemma 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.
1405#ty #m #b #o cases (load_value_of_type ty m b o)
1406[ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed.
1407
1408(* Simulation relations. *)
1409inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
1410| swc_stop : ∀fvs.
1411    switch_cont_sim fvs Kstop Kstop
1412| swc_seq : ∀fvs,s,k,k',u,result.
1413    fresh_for_statement s u →
1414    switch_cont_sim fvs k k' →
1415    switch_removal s fvs u = Some ? result →
1416    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
1417| swc_while : ∀fvs,e,s,cl,k,k',u,result.
1418    fresh_for_statement (Swhile e s cl) u →
1419    switch_cont_sim fvs k k' →
1420    switch_removal s fvs u = Some ? result →
1421    switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k')
1422| swc_dowhile : ∀fvs,e,s,k,k',u,result.
1423    fresh_for_statement (Sdowhile e s) u →
1424    switch_cont_sim fvs k k' →
1425    switch_removal s fvs u = Some ? result →
1426    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
1427| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
1428    fresh_for_statement (Sfor Sskip e s1 s2) u →
1429    switch_cont_sim fvs k k' →
1430    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
1431    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
1432| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1433    fresh_for_statement (Sfor Sskip e s1 s2) u →
1434    switch_cont_sim fvs k k' →
1435    switch_removal s1 fvs u = Some ? result1 →
1436    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
1437    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
1438| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
1439    fresh_for_statement (Sfor Sskip e s1 s2) u →
1440    switch_cont_sim fvs k k' →
1441    switch_removal s1 fvs u = Some ? result1 →
1442    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
1443    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
1444| swc_switch : ∀fvs,k,k'.
1445    switch_cont_sim fvs k k' →
1446    switch_cont_sim fvs (Kswitch k) (Kswitch k')
1447| swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
1448    switch_cont_sim fvs k k' →
1449    (* /!\ Update [en] with [fvs'] ... *)
1450    switch_cont_sim
1451      (map … (fst ??) (\snd (function_switch_removal f)))
1452      (Kcall r f en k)
1453      (Kcall r (\fst (function_switch_removal f)) en' k').
1454
1455(*
1456 en' = exec_alloc_variables en m (\snd (function_switch_removal f))
1457 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
1458        variable dans en'.
1459
1460        1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que
1461           dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
1462           de savoir que :
1463           si je lookup une variable générée à partir d'un univers frais dans l'environement en',
1464           alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
1465           et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
1466           et à etre "(function_switch_removal f)-contained".
1467
1468        2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
1469           et l'update n'altèrent pas le comportement du reste du programme.
1470
1471        relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
1472                   depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
1473                   en particulier, si u est frais pour S1 u est frais pour S0.
1474
1475        Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
1476                    "environment_extension en en' (\fst (\fst (switch_removal s u)))"
1477                   
1478 ---------------------------------------------------------------
1479 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
1480   et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
1481   on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
1482   en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
1483*)
1484
1485(*  env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
1486    env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →  *)
1487record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
1488  rg_find_symbol: ∀s.
1489    find_symbol ? ge s = find_symbol ? ge' s;
1490  rg_find_funct: ∀v,f.
1491    find_funct ? ge v = Some ? f →
1492    find_funct ? ge' v = Some ? (t f);
1493  rg_find_funct_ptr: ∀b,f.
1494    find_funct_ptr ? ge b = Some ? f →
1495    find_funct_ptr ? ge' b = Some ? (t f)
1496}.
1497
1498(* This record aims to shorten the definition of the simulation relation on states more readeable. *)
1499inductive switch_state_sim (ge : genv) : state → state → Prop ≝
1500| sws_state :
1501 (* current statement *)
1502 ∀sss_statement  : statement.
1503 (* statement after transformation *)
1504 ∀sss_result     : swret statement.
1505 (* label universe *)
1506 ∀sss_lu         : universe SymbolTag.
1507 (* [sss_lu] must be fresh *)
1508 ∀sss_lu_fresh   : fresh_for_statement sss_statement sss_lu.
1509 (* current function *)
1510 ∀sss_func       : function.
1511 (* current function after translation *)
1512 ∀sss_func_tr    : function.
1513 (* variables generated during conversion of the function *)
1514 ∀sss_new_vars   : list (ident × type).
1515 (* statement of the transformation *) 
1516 ∀sss_func_hyp   : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func.
1517 (* memory state before conversion *)
1518 ∀sss_m          : mem.
1519 (* memory state after conversion *)
1520 ∀sss_m_ext      : mem.
1521 (* environment before conversion *)
1522 ∀sss_env        : env.
1523 (* environment after conversion *)
1524 ∀sss_env_ext    : env.
1525 (* continuation before conversion *)
1526 ∀sss_k          : cont.
1527 (* continuation after conversion *)
1528 ∀sss_k_ext      : cont.
1529 (* memory "injection" *)
1530 ∀sss_mem_hyp    : sr_memext sss_m sss_m_ext.
1531 (* The extended environment does not interfer with the old one. *)
1532 ∀sss_env_hyp    : disjoint_extension sss_env sss_m sss_env_ext sss_m_ext sss_new_vars sss_mem_hyp.
1533 (* conversion of the current statement, using the variables produced during the conversion of the current function *)
1534 ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result.
1535 (* simulation between the continuations before and after conversion. *)
1536 ∀sss_k_hyp      : switch_cont_sim (map ?? (fst ??) sss_new_vars) sss_k sss_k_ext. 
1537 ext_fresh_for_genv sss_new_vars ge →
1538    switch_state_sim
1539      ge
1540      (State sss_func sss_statement sss_k sss_env sss_m)
1541      (State sss_func_tr (ret_st … sss_result) sss_k_ext sss_env_ext sss_m_ext)
1542| sws_callstate : ∀vars, fd,args,k,k',m.
1543    switch_cont_sim vars k k' →
1544    switch_state_sim ge (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m)
1545| sws_returnstate :
1546 ∀ssr_vars.
1547 ∀ssr_result.
1548 ∀ssr_k       : cont.
1549 ∀ssr_k_ext   : cont.
1550 ∀ssr_m       : mem.
1551 ∀ssr_m_ext   : mem.
1552 ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext.
1553    switch_cont_sim ssr_vars ssr_k ssr_k_ext →
1554    switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext)
1555| sws_finalstate : ∀r.
1556    switch_state_sim ge (Finalstate r) (Finalstate r).
1557
1558lemma call_cont_swremoval : ∀fv,k,k'.
1559  switch_cont_sim fv k k' →
1560  switch_cont_sim fv (call_cont k) (call_cont k').
1561#fv #k0 #k0' #K elim K /2/
1562qed.
1563
1564(* [eventually ge P s tr] states that after a finite number of [exec_step], the
1565   property P on states will be verified. *)
1566inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
1567| eventually_base : ∀s,t,s'.
1568    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
1569    P s' →
1570    eventually ge P s t
1571| eventually_step : ∀s,t,s',t',trace.
1572    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
1573    eventually ge P s' t' →
1574    trace = (t ⧺ t') →
1575    eventually ge P s trace.
1576
1577(* [eventually] is not so nice to use directly, we would like to make the mandatory
1578 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
1579   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
1580lemma eventually_now : ∀ge,P,s,t.
1581  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') →
1582   eventually ge P s t.
1583#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
1584qed.
1585
1586lemma eventually_later : ∀ge,P,s,t.
1587   (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) →
1588    eventually ge P s t.
1589#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
1590try assumption
1591qed.
1592
1593lemma exec_lvalue_expr_elim :
1594  ∀r1,r2,Pok,Qok.
1595  exec_lvalue_sim r1 r2 →
1596  (∀val,trace.
1597    match Pok 〈val,trace〉 with
1598    [ Error err ⇒ True
1599    | OK pvt ⇒
1600      let 〈pval,ptrace〉 ≝ pvt in
1601      match Qok 〈val,trace〉 with
1602      [ Error err ⇒ False
1603      | OK qvt ⇒
1604        let 〈qval,qtrace〉 ≝ qvt in
1605        ptrace = qtrace ∧ pval = qval
1606      ]
1607    ]) → 
1608  exec_expr_sim
1609    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
1610    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
1611#r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
1612elim r1
1613[ 2:  #error #_ #_ normalize #a #Habsurd destruct (Habsurd)
1614| 1: normalize nodelta #a #H lapply (H a (refl ??))
1615     #Hr2 >Hr2 normalize #H #a' elim a * #b #o #tr
1616     lapply (H 〈b, o〉 tr) #H1 #H2 >H2 in H1;
1617     normalize nodelta elim a' in H2; #pval #ptrace #Hpok
1618     normalize nodelta cases (Qok 〈b,o,tr〉)
1619     [ 2: #error normalize #Habsurd @(False_ind … Habsurd)
1620     | 1: * #qval #qtrace normalize nodelta * #Htrace #Hval
1621          destruct @refl
1622] ] qed.
1623
1624
1625lemma exec_expr_expr_elim :
1626  ∀r1,r2,Pok,Qok.
1627  exec_expr_sim r1 r2 →
1628  (∀val,trace.
1629    match Pok 〈val,trace〉 with
1630    [ Error err ⇒ True
1631    | OK pvt ⇒
1632      let 〈pval,ptrace〉 ≝ pvt in
1633      match Qok 〈val,trace〉 with
1634      [ Error err ⇒ False
1635      | OK qvt ⇒
1636        let 〈qval,qtrace〉 ≝ qvt in
1637        ptrace = qtrace ∧ pval = qval
1638      ]
1639    ]) →
1640  exec_expr_sim
1641    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
1642    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
1643#r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
1644elim r1
1645[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
1646| 1: normalize nodelta #a #H lapply (H a (refl ??))
1647     #Hr2 >Hr2 normalize nodelta #H
1648     elim a in Hr2; #val #trace
1649     lapply (H … val trace)
1650     cases (Pok 〈val, trace〉)
1651     [ 2: #error normalize #_ #_ #a' #Habsurd destruct (Habsurd)
1652     | 1: * #pval #ptrace normalize nodelta
1653          cases (Qok 〈val,trace〉)
1654          [ 2: #error normalize #Hfalse @(False_ind … Hfalse)
1655          | 1: * #qval #qtrace normalize nodelta * #Htrace_eq #Hval_eq
1656               #Hr2_eq destruct #a #H @H
1657] ] ] qed.
1658
1659
1660lemma load_value_of_type_inj : ∀m1,m2,b,off,ty.
1661    sr_memext m1 m2 → ∀v.
1662    load_value_of_type ty m1 b off = Some ? v →
1663    load_value_of_type ty m2 b off = Some ? v.
1664#m1 #m2 #b #off #ty #Hinj #v
1665@(load_sim_fe … (me_inj … Hinj) (mk_pointer b off))
1666qed.
1667
1668(* Conservation of the smenantics of binary operators *)
1669lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2.
1670  ∀Hext:sr_memext m1 m2. ∀res.
1671  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res →
1672  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res.
1673#op #v1 #v2 #e1 #e2 #m1 #m2 #Hmemext #res cases op
1674whd in match (sem_binary_operation ??????);
1675try //
1676whd in match (sem_binary_operation ??????);
1677elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1
1678elim m2 #contents2 #nextblocks2 #Hnextpos2
1679* #Hptrsim #writeable #Hvalid #Hdisjoint #Hvalid_cons
1680whd in match (sem_cmp ??????);
1681whd in match (sem_cmp ??????);
1682[ 1: cases (classify_cmp (typeof e1) (typeof e2))
1683     normalize nodelta
1684     [ 1: #sz #sg try //
1685     | 2: #opt #ty
1686          cases v1 normalize nodelta
1687          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
1688          [ 1,2,3: #Habsurd destruct (Habsurd)
1689          | 4: #H @H ]
1690          cases v2 normalize nodelta
1691          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
1692          [ 1,2,3: #Habsurd destruct (Habsurd)
1693          | 4: #H @H ]
1694          lapply (Hvalid_cons ptr)
1695          elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
1696          [ 2: #Hnot_freed #Hvalid lapply (Hvalid … Hnot_freed)
1697               cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
1698               [ 2: >andb_lsimpl_false normalize nodelta #_ #Habsurd destruct (Habsurd) ]
1699               #Hvalid >(Hvalid (refl ??))
1700               lapply (Hvalid_cons ptr')
1701               elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1702               [ 2: #Hnot_freed' #Hvalid' lapply (Hvalid' … Hnot_freed')
1703                    cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1704                    [ 2: >andb_lsimpl_true #_ normalize nodelta #Habsurd destruct (Habsurd) ]
1705                    #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres
1706               | 1: normalize in ⊢ (% → ?); * #Hlow' #Hhigh' #_
1707                    >andb_lsimpl_true >andb_lsimpl_true
1708                    whd in match (valid_pointer ??);
1709                    whd in match (low_bound ??);
1710                    whd in match (high_bound ??);
1711                    >Hlow' >Hhigh' >Zleb_unsigned_OZ >andb_comm >andb_lsimpl_true
1712                    whd in match (valid_pointer ??);
1713               
1714               cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1715               [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1716               #H' >(H' (refl ??)) #Hok @Hok
1717          | 1:
1718          ]
1719     | 3: #fsz #H @H
1720     | 4: #ty1 #ty2 #H @H ]
1721| 2: cases (classify_cmp (typeof e1) (typeof e2))
1722     normalize nodelta
1723     [ 1: #sz #sg try //
1724     | 2: #opt #ty
1725          cases v1 normalize nodelta
1726          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
1727          [ 1,2,3: #Habsurd destruct (Habsurd)
1728          | 4: #H @H ]
1729          cases v2 normalize nodelta
1730          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
1731          [ 1,2,3: #Habsurd destruct (Habsurd)
1732          | 4: #H @H ]
1733          lapply (Hvalid_cons ptr)
1734          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
1735          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1736          #H >(H (refl ??))
1737          lapply (Hvalid_cons ptr')
1738          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1739          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1740          #H' >(H' (refl ??)) #Hok @Hok
1741     | 3: #fsz #H @H
1742     | 4: #ty1 #ty2 #H @H ]
1743| 3: cases (classify_cmp (typeof e1) (typeof e2))
1744     normalize nodelta
1745     [ 1: #sz #sg try //
1746     | 2: #opt #ty
1747          cases v1 normalize nodelta
1748          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
1749          [ 1,2,3: #Habsurd destruct (Habsurd)
1750          | 4: #H @H ]
1751          cases v2 normalize nodelta
1752          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
1753          [ 1,2,3: #Habsurd destruct (Habsurd)
1754          | 4: #H @H ]
1755          lapply (Hvalid_cons ptr)
1756          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
1757          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1758          #H >(H (refl ??))
1759          lapply (Hvalid_cons ptr')
1760          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1761          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1762          #H' >(H' (refl ??)) #Hok @Hok
1763     | 3: #fsz #H @H
1764     | 4: #ty1 #ty2 #H @H ]
1765| 4: cases (classify_cmp (typeof e1) (typeof e2))
1766     normalize nodelta
1767     [ 1: #sz #sg #H @H         
1768     | 2: #opt #ty
1769          cases v1 normalize nodelta
1770          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
1771          [ 1,2,3: #Habsurd destruct (Habsurd)
1772          | 4: #H @H ]
1773          cases v2 normalize nodelta
1774          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
1775          [ 1,2,3: #Habsurd destruct (Habsurd)
1776          | 4: #H @H ]
1777          lapply (Hvalid_cons ptr)
1778          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
1779          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1780          #H >(H (refl ??))
1781          lapply (Hvalid_cons ptr')
1782          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1783          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1784          #H' >(H' (refl ??)) #Hok @Hok
1785     | 3: #fsz #H @H
1786     | 4: #ty1 #ty2 #H @H ]
1787| 5: cases (classify_cmp (typeof e1) (typeof e2))
1788     normalize nodelta
1789     [ 1: #sz #sg #H @H         
1790     | 2: #opt #ty
1791          cases v1 normalize nodelta
1792          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
1793          [ 1,2,3: #Habsurd destruct (Habsurd)
1794          | 4: #H @H ]
1795          cases v2 normalize nodelta
1796          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
1797          [ 1,2,3: #Habsurd destruct (Habsurd)
1798          | 4: #H @H ]
1799          lapply (Hvalid_cons ptr)
1800          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
1801          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1802          #H >(H (refl ??))
1803          lapply (Hvalid_cons ptr')
1804          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1805          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1806          #H' >(H' (refl ??)) #Hok @Hok
1807     | 3: #fsz #H @H
1808     | 4: #ty1 #ty2 #H @H ]
1809| 6: cases (classify_cmp (typeof e1) (typeof e2))
1810     normalize nodelta
1811     [ 1: #sz #sg #H @H         
1812     | 2: #opt #ty
1813          cases v1 normalize nodelta
1814          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
1815          [ 1,2,3: #Habsurd destruct (Habsurd)
1816          | 4: #H @H ]
1817          cases v2 normalize nodelta
1818          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
1819          [ 1,2,3: #Habsurd destruct (Habsurd)
1820          | 4: #H @H ]
1821          lapply (Hvalid_cons ptr)
1822          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
1823          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1824          #H >(H (refl ??))
1825          lapply (Hvalid_cons ptr')
1826          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
1827          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
1828          #H' >(H' (refl ??)) #Hok @Hok
1829     | 3: #fsz #H @H
1830     | 4: #ty1 #ty2 #H @H ]
1831] qed.
1832
1833
1834(* Simulation relation on expressions *)
1835lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
1836  ∀Hext:sr_memext m1 m2.
1837  switch_removal_globals ? fundef_switch_removal ge ge' →
1838  disjoint_extension en1 m1 en2 m2 ext Hext →
1839  ext_fresh_for_genv ext ge →
1840  (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
1841  (∀ed, ty. exec_lvalue_sim (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
1842#ge #ge' #en1 #m1 #en2 #m2 #ext #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
1843@expr_lvalue_ind_combined
1844[ 1: #csz #cty #i #a1
1845     whd in match (exec_expr ????); elim cty
1846     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1847     normalize nodelta
1848     [ 2: cases (eq_intsize csz sz) normalize nodelta
1849          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
1850          | 2: #Habsurd destruct (Habsurd) ]
1851     | 4,5,6: #_ #H destruct (H)
1852     | *: #H destruct (H) ]
1853| 2: #ty #fl #a1
1854     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
1855| 3: *
1856  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
1857  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
1858  #ty whd in ⊢ (% → ?); #Hind try @I
1859  whd in match (Plvalue ???);
1860  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
1861       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
1862       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1863       | 1,3,5: normalize nodelta #b1 #H lapply (H b1 (refl ??)) #Heq >Heq       
1864           normalize nodelta
1865           elim b1 * #bl1 #o1 #tr1 (* elim b2 * #bl2 #o2 #tr2 *)
1866           whd in match (load_value_of_type' ???);
1867           whd in match (load_value_of_type' ???);
1868           lapply (load_value_of_type_inj m1 m2 bl1 o1 ty Hext)
1869           cases (load_value_of_type ty m1 bl1 o1)
1870           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
1871           | 2,4,6: #v #H normalize in ⊢ (% → ?); #Heq destruct (Heq)
1872                    >(H v (refl ??)) @refl
1873  ] ] ]
1874| 4: #v #ty whd * * #b #o #tr
1875     whd in match (exec_lvalue' ?????);
1876     whd in match (exec_lvalue' ?????);
1877     lapply (Hdisjoint v)
1878     lapply (Hext_fresh_for_genv v)
1879     cases (mem_assoc_env v ext) #Hglobal
1880     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
1881          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
1882          >(Hglobal (refl ??)) normalize
1883          #Habsurd destruct (Habsurd)
1884     | 2: normalize nodelta
1885          cases (lookup ?? en1 v) normalize nodelta
1886          [ 1: #Hlookup2 <Hlookup2 normalize nodelta
1887               lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym
1888               #H @H
1889          | 2: #block
1890              cases (lookup ?? en2 v) normalize nodelta
1891              [ 1: #Habsurd destruct (Habsurd)
1892              | 2: #b #Heq destruct (Heq) #H @H ]
1893          ]
1894    ]
1895| 5: #e #ty whd in ⊢ (% → %);
1896     whd in match (exec_lvalue' ?????);
1897     whd in match (exec_lvalue' ?????);
1898     cases (exec_expr ge en1 m1 e)
1899     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H
1900     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
1901| 6: #ty #e #ty'
1902     #Hsim @(exec_lvalue_expr_elim … Hsim)
1903     cases ty
1904     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1905     * #b #o normalize nodelta try /2 by I/
1906     #tr @conj try @refl
1907| 7: #ty #op #e
1908     #Hsim @(exec_expr_expr_elim … Hsim) #v #trace
1909     cases (sem_unary_operation op v (typeof e)) normalize nodelta
1910     try @I
1911     #v @conj @refl
1912| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
1913     @(exec_expr_expr_elim … Hsim1) #v #trace
1914     cases (exec_expr ge en1 m1 e2) in Hsim2;
1915     [ 2: #error // ]
1916     * #pval #ptrace normalize in ⊢ (% → ?); #Hsim2
1917     whd in match (m_bind ?????);
1918     >(Hsim2 ? (refl ??))
1919     whd in match (m_bind ?????);
1920     lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 Hext)
1921     cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1)
1922     [ 1: #_ // ] #val #H >(H val (refl ??))
1923     normalize destruct @conj @refl
1924| 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
1925     #v #tr
1926     cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty)
1927     [ @refl ]
1928     #Heq >Heq     
1929     cases (exec_cast m2 v (typeof e) cast_ty)
1930     [ 2: //
1931     | 1: #v normalize @conj @refl ]
1932| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
1933     @(exec_expr_expr_elim … Hsim1) #v #tr
1934     cases (exec_bool_of_val ? (typeof e1)) #b
1935     [ 2: normalize @I ]
1936     cases b normalize nodelta
1937     whd in match (m_bind ?????);
1938     whd in match (m_bind ?????);
1939     normalize nodelta
1940     [ 1: (* true branch *)
1941          cases (exec_expr ge en1 m1 e2) in Hsim2;
1942          [ 2: #error normalize #_ @I
1943          | 1: * #e2v #e2tr normalize #H >(H ? (refl ??)) normalize nodelta
1944               @conj @refl ]
1945     | 2: (* false branch *)
1946          cases (exec_expr ge en1 m1 e3) in Hsim3;
1947          [ 2: #error normalize #_ @I
1948          | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta
1949               @conj @refl ] ]
1950| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
1951     @(exec_expr_expr_elim … Hsim1) #v #tr
1952     cases (exec_bool_of_val v (typeof e1))
1953     [ 2,4: #error normalize @I ]
1954     *
1955     whd in match (m_bind ?????);
1956     whd in match (m_bind ?????);
1957     [ 2,3: normalize @conj try @refl ]
1958     cases (exec_expr ge en1 m1 e2) in Hsim2;
1959     [ 2,4: #error #_ normalize @I ]
1960     * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta >(H2 ? (refl ??))
1961     normalize nodelta
1962     cases (exec_bool_of_val v2 (typeof e2))
1963     [ 2,4: #error normalize @I ]
1964     * normalize @conj @refl
1965| 13: #ty #ty' cases ty
1966     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n
1967     | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1968     whd in match (exec_expr ????); whd #a #H @H
1969| 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr
1970    whd in match (exec_lvalue' ?????);
1971    whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
1972    whd in match (typeof ?);
1973    cases aggregty in Hsim;
1974    [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
1975    | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
1976    normalize nodelta #Hsim
1977    [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
1978    whd in match (m_bind ?????);
1979    whd in match (m_bind ?????);
1980    whd in match (exec_lvalue ge en1 m1 (Expr ed ?));
1981    cases (exec_lvalue' ge en1 m1 ed ?) in Hsim;
1982    [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
1983    * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H
1984    whd in match (exec_lvalue ge' en2 m2 (Expr ed ?));   
1985     >(H ? (refl ??)) normalize nodelta #H @H
1986| 15: #ty #l #e #Hsim
1987     @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj //
1988| 16: *
1989  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
1990  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
1991  #ty normalize in ⊢ (% → ?);
1992  [ 3,4,13: @False_ind
1993  | *: #_ normalize #a1 #Habsurd @Habsurd ]
1994] qed.
1995
1996
1997
1998(*
1999lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
2000related_globals ? fundef_switch_removal ge ge' →
2001∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
2002#ge #ge' #en #m #Hrelated #args
2003elim args
2004[ 1: /3/
2005| 2: #hd #tl #Hind normalize
2006     elim (sim_related_globals ge ge' en m Hrelated)
2007     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
2008     cases (exec_expr ge en m hd)
2009     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
2010     | 1: * #val_hd #trace_hd normalize nodelta
2011          cases Hind
2012          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
2013          | 1: cases (exec_exprlist ge en m tl)
2014               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
2015               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
2016                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
2017                    cases Hexec_hd
2018                    [ 2: * #error #Habsurd destruct (Habsurd)
2019                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
2020] ] ] ] qed.
2021*)
2022
2023(* The return type of any function is invariant under switch removal *)
2024lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
2025#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
2026qed.
2027
2028(* Similar stuff for fundefs *)
2029lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
2030* // qed.
2031
2032(*
2033lemma expr_fresh_lift :
2034  ∀e,u,id.
2035      fresh_for_expression e u →
2036      fresh_for_univ SymbolTag id u →
2037      fresh_for_univ SymbolTag (max_of_expr e id) u.
2038#e #u #id
2039normalize in match (fresh_for_expression e u);
2040#H1 #H2
2041>max_of_expr_rewrite
2042normalize in match (fresh_for_univ ???);
2043cases (max_of_expr e ?) in H1; #p #H1
2044cases id in H2; #p' #H2
2045normalize nodelta
2046cases (leb p p') normalize nodelta
2047[ 1: @H2 | 2: @H1 ]
2048qed. *)
2049
2050lemma while_fresh_lift : ∀e,s,cl,u.
2051   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u.
2052#e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???));
2053cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
2054cases (leb e s) try /2/
2055qed.
2056
2057(*
2058lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
2059#e0 #s0 #us0 normalize
2060cases (switch_removal s0 us0) * #body #newvars #u' normalize //
2061qed.*)
2062
2063lemma dowhile_fresh_lift : ∀e,s,u.
2064   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
2065#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
2066cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
2067cases (leb e s) try /2/
2068qed.
2069(*
2070lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
2071#e0 #s0 #us0 normalize
2072cases (switch_removal s0 us0) * #body #newvars #u' normalize //
2073qed.*)
2074
2075lemma for_fresh_lift : ∀cond,step,body,u.
2076  fresh_for_statement step u →
2077  fresh_for_statement body u →
2078  fresh_for_expression cond u →
2079  fresh_for_statement (Sfor Sskip cond step body) u.
2080#cond #step #body #u
2081whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
2082cases (max_of_statement step) #s
2083cases (max_of_statement body) #b
2084cases (max_of_expr cond) #c
2085whd in match (max_of_statement Sskip);
2086>(max_id_commutative least_identifier)
2087>max_id_one_neutral normalize nodelta
2088normalize elim u #u
2089cases (leb s b) cases (leb c b) cases (leb c s) try /2/
2090qed.
2091
2092(*
2093lemma for_commute : ∀e,stm1,stm2,u,uA.
2094   (uA=\snd  (switch_removal stm1 u)) →
2095   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
2096#e #stm1 #stm2 #u #uA #HuA
2097whd in match (sw_rem (Sfor ????) u);
2098whd in match (switch_removal ??);   
2099destruct
2100normalize in match (\snd (switch_removal Sskip u));
2101whd in match (sw_rem stm1 u);
2102cases (switch_removal stm1 u)
2103* #stm1' #fresh_vars #uA normalize nodelta
2104whd in match (sw_rem stm2 uA);
2105cases (switch_removal stm2 uA)
2106* #stm2' #fresh_vars2 #uB normalize nodelta
2107//
2108qed.*)
2109
2110(*
2111lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
2112*
2113[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
2114| 2: #e1 #e2 #u #_
2115     whd in match (sw_rem ??);
2116     whd in match (is_Sskip ?);
2117     try /2 by refl, ex_intro/
2118| 3: #ret #f #args #u
2119     whd in match (sw_rem ??);
2120     whd in match (is_Sskip ?);
2121     try /2 by refl, ex_intro/
2122| 4: #s1 #s2 #u
2123     whd in match (sw_rem ??);
2124     whd in match (switch_removal ??);     
2125     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
2126     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
2127     whd in match (is_Sskip ?);
2128     try /2 by refl, ex_intro/
2129| 5: #e #s1 #s2 #u #_
2130     whd in match (sw_rem ??);
2131     whd in match (switch_removal ??);     
2132     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2133     cases (switch_removal ? ?) * #e #f #h normalize nodelta
2134     whd in match (is_Sskip ?);
2135     try /2 by refl, ex_intro/
2136| 6,7: #e #s #u #_
2137     whd in match (sw_rem ??);
2138     whd in match (switch_removal ??);     
2139     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2140     whd in match (is_Sskip ?);
2141     try /2 by refl, ex_intro/
2142| 8: #s1 #e #s2 #s3 #u #_     
2143     whd in match (sw_rem ??);
2144     whd in match (switch_removal ??);     
2145     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2146     cases (switch_removal ? ?) * #e #f #g normalize nodelta
2147     cases (switch_removal ? ?) * #i #j #k normalize nodelta
2148     whd in match (is_Sskip ?);
2149     try /2 by refl, ex_intro/
2150| 9,10: #u #_     
2151     whd in match (is_Sskip ?);
2152     try /2 by refl, ex_intro/
2153| 11: #e #u #_
2154     whd in match (is_Sskip ?);
2155     try /2 by refl, ex_intro/
2156| 12: #e #ls #u #_
2157     whd in match (sw_rem ??);
2158     whd in match (switch_removal ??);
2159     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
2160     cases (fresh ??) #e #f normalize nodelta
2161     normalize in match (simplify_switch ???);
2162     cases (fresh ? f) #g #h normalize nodelta
2163     cases (produce_cond ????) * #k #l #m normalize nodelta
2164     whd in match (is_Sskip ?);
2165     try /2 by refl, ex_intro/
2166| 13,15: #lab #st #u #_
2167     whd in match (sw_rem ??);
2168     whd in match (switch_removal ??);
2169     cases (switch_removal ? ?) * #a #b #c normalize nodelta
2170     whd in match (is_Sskip ?);
2171     try /2 by refl, ex_intro/
2172| 14: #lab #u     
2173     whd in match (is_Sskip ?);
2174     try /2 by refl, ex_intro/ ]
2175qed.
2176*)
2177
2178(*
2179lemma sw_rem_commute : ∀stm,u.
2180  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
2181#stm #u whd in match (sw_rem stm u); // qed.
2182*)
2183
2184lemma fresh_for_statement_inv :
2185  ∀u,s. fresh_for_statement s u →
2186        match u with
2187        [ mk_universe p ⇒ le (p0 one) p ].
2188* #p #s whd in match (fresh_for_statement ??);
2189cases (max_of_statement s) #s
2190normalize /2/ qed.
2191
2192lemma fresh_for_Sskip :
2193  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
2194#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
2195
2196lemma fresh_for_Sbreak :
2197  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
2198#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
2199
2200lemma fresh_for_Scontinue :
2201  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
2202#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
2203
2204(*
2205lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
2206#s #u elim (switch_removal s u) * #res #fvs #u'
2207%{res} %{fvs} %{u'} //
2208qed.
2209
2210lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
2211#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
2212%{res} %{fvs} %{u'} //
2213qed.
2214*)
2215
2216lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
2217#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
2218#s #lab #u' %{s} %{lab} %{u'} //
2219qed.
2220
2221(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
2222lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
2223* * *
2224[ 1,5,9: #H @(False_ind … (H (refl ??)))
2225| *: #_ normalize @refl ]
2226qed.
2227
2228lemma exec_expr_int : ∀ge,e,m,expr.
2229    (∃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〉)).
2230#ge #e #m #expr cases (exec_expr ge e m expr)
2231[ 2: #error %2 #sz #n #tr % #H destruct (H)
2232| 1: * #val #trace cases val
2233     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
2234     | 3: #fl | 4: | 5: #ptr ]
2235     %2 #sz #n #tr % #H destruct (H)
2236] qed.
2237
2238lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.
2239
2240lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c.
2241#A #B #a #b * #a' #b' #H destruct @refl
2242qed.
2243
2244lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c.
2245#A #B #a #b * #a' #b' #H destruct @refl
2246qed.
2247
2248(* Main theorem. To be ported and completed to memory injections. TODO *)
2249theorem switch_removal_correction :
2250  ∀ge,ge',s1, s1', tr, s2.
2251  switch_removal_globals ? fundef_switch_removal ge ge' →
2252  switch_state_sim ge s1 s1' →
2253  exec_step ge s1 = Value … 〈tr,s2〉 →
2254  eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr.
2255#ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state
2256inversion Hsim_state
2257[ 1: (* regular state *)
2258  #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
2259  #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_mem_hyp
2260  #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge
2261  elim (sim_related_globals … ge ge'
2262             sss_env sss_m sss_env_ext sss_m_ext sss_new_vars
2263             sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge)
2264  #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_
2265  cases sss_statement in sss_lu_fresh sss_result_hyp;
2266  (* Perform the intros for the statements *)
2267  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
2268  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
2269  | 14: #lab | 15: #cost #body ]
2270  #sss_lu_fresh #sss_result_hyp
2271  [ 1: (* Skip *)
2272    whd in match (switch_removal ???) in sss_result_hyp;
2273    <(some_inj ??? sss_result_hyp)
2274    inversion sss_k_hyp normalize nodelta
2275    [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step
2276         @(eventually_now ????) whd in match (exec_step ??);
2277         >(prod_eq_lproj ????? sss_func_hyp)
2278         >fn_return_simplify
2279         whd in match (exec_step ??) in Hexec_step;
2280         cases (fn_return sss_func) in Hexec_step;
2281         [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
2282         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
2283         normalize nodelta
2284         whd in ⊢ ((??%?) → ?);
2285         [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))}
2286              @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)} try //
2287                %{(Returnstate Vundef Kstop (free1_list sss_m_ext (blocks_of_env sss_env_ext)))} @conj try //
2288                normalize in Heq_env; destruct (Heq_env)
2289                %3 //
2290(*                cut (blocks_of_env e = blocks_of_env e')
2291                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
2292                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
2293                #Heq >Heq %3 // *)
2294         | *: #H destruct (H) ]
2295    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2296         whd in match (ret ??) in Heq; destruct (Heq)
2297         @(eventually_now ????) whd in match (exec_step ??);
2298         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
2299         %1 try //   
2300    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2301         @(eventually_now ????) whd in match (exec_step ??);
2302         whd in match (ret ??) in Heq; destruct (Heq)
2303         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
2304         >while_commute %1 try //
2305    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2306         @(eventually_now ????) whd in match (exec_step ??);
2307         lapply (Hexpr_related e0)
2308         cases (exec_expr ge e m e0) in Heq;
2309         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2310         | 1: * #b #tr whd in match (m_bind ?????); #Heq
2311              *
2312              [ 2: * #error #Habsurd destruct (Habsurd)
2313              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
2314                   whd in match (bindIO ??????);
2315                   cases (exec_bool_of_val b (typeof e0)) in Heq;
2316                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2317                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
2318                        whd in match (bindIO ??????);
2319                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
2320                             @conj // >dowhile_commute %1 try //
2321                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
2322                             @conj // %1{us} try //
2323                             @(fresh_for_Sskip … Hus_fresh)
2324                        ] ] ] ]
2325    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
2326         @(eventually_now ????) whd in match (exec_step ??);
2327         whd in match (ret ??) in Heq; destruct
2328         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
2329         @conj try // %1{u} try //
2330    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
2331         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
2332         destruct (Heq)
2333         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
2334         @conj try // %1
2335         [ 2: @swc_for3 //
2336         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
2337    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
2338         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
2339         destruct (Heq)
2340         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
2341         @conj try // <(for_commute ??? u uA) try // %1
2342         [ 2: assumption
2343         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
2344    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
2345         #Heq @(eventually_now ????) whd in match (exec_step ??);
2346         destruct (Heq)
2347         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
2348         %1{u} //
2349    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
2350         @(eventually_now ????) whd in match (exec_step ??);
2351         >fn_return_simplify cases (fn_return f) in Heq;
2352         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
2353         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
2354         normalize nodelta
2355         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
2356              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
2357              @conj try // %3 destruct //
2358         | *: #H destruct (H) ]     
2359     ]
2360  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
2361       whd in match (exec_step ??);
2362       cases lhs in Hu_fresh Heq; #lhs #lhs_type
2363       cases (Hlvalue_related lhs lhs_type)
2364       whd in match (exec_lvalue ge e m (Expr ??));
2365       whd in match (exec_lvalue ge' e m (Expr ??));
2366       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
2367       cases (exec_lvalue' ge e m lhs lhs_type)
2368       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
2369       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
2370            whd in match (m_bind ?????);
2371            cases (Hexpr_related rhs)
2372            [ 2: * #error #Hfail >Hfail #_
2373                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2374            | 1: cases (exec_expr ge e m rhs)
2375                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
2376                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
2377                      whd in match (bindIO ??????) in ⊢ (% → % → %);
2378                      cases (opt_to_io io_out io_in ???)
2379                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
2380                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2381                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
2382                           %{(State (function_switch_removal f) Sskip k' e mem)}
2383                           whd in match (bindIO ??????); @conj //
2384                           %1{u} try // @(fresh_for_Sskip … Hfresh)
2385       ] ] ] ]
2386   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
2387        whd in match (exec_step ??);
2388        cases (Hexpr_related func) in Heq;
2389        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2390        | 1: cases (exec_expr ge e m func)
2391             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2392             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
2393                  whd in match (m_bind ?????); normalize nodelta
2394                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
2395                  #Hexprlist_sim cases (Hexprlist_sim args)
2396                  [ 2: * #error #Hfail >Hfail
2397                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2398                  | 1: cases (exec_exprlist ge e m args)
2399                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2400                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
2401                            whd in match (bindIO ??????) in ⊢ (% → %);
2402                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
2403                            cases (find_funct clight_fundef ge fval)
2404                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
2405                                 whd in match (bindIO ??????) in ⊢ (% → %);
2406                                 >fundef_type_simplify
2407                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
2408                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2409                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
2410                                      cases retv normalize nodelta
2411                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
2412                                           %{(Callstate (fundef_switch_removal clfd) values
2413                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
2414                                           @conj try // %2 try // @swc_call //
2415                                      | 2: * #retval_ed #retval_type
2416                                           whd in match (exec_lvalue ge ???);
2417                                           whd in match (exec_lvalue ge' ???);                                     
2418                                           elim (Hlvalue_related retval_ed retval_type)
2419                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2420                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
2421                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
2422                                                     destruct (Habsurd)
2423                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
2424                                                     whd in match (m_bind ?????) in ⊢ (% → %);
2425                                                     #Heq destruct (Heq)
2426                                                     %{(Callstate (fundef_switch_removal clfd) values
2427                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
2428                                                               (function_switch_removal f) e k') m)}
2429                                                     @conj try //
2430                                                     %2 @swc_call //
2431                                ] ] ] ]
2432                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
2433                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2434       ] ] ] ] ]
2435   | 4: (* Ssequence *) normalize nodelta
2436        whd in match (ret ??) in ⊢ (% → ?); #Heq
2437        @(eventually_now ????)
2438        %{(State (function_switch_removal f)
2439                 (\fst (\fst (switch_removal stm1 u)))
2440                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
2441        @conj
2442        [ 2: destruct (Heq) %1
2443             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
2444             | 2: @swc_seq try // @switch_removal_fresh
2445                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
2446        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
2447             cases (switch_removal stm1 u)
2448             * #stm1' #fresh_vars #u' normalize nodelta
2449             cases (switch_removal stm2 u')
2450             * #stm2' #fresh_vars2 #u'' normalize nodelta
2451             whd in match (exec_step ??);
2452             destruct (Heq) @refl
2453        ]
2454   | 5: (* If-then-else *) normalize nodelta
2455        whd in match (ret ??) in ⊢ (% → ?); #Heq
2456        @(eventually_now ????) whd in match (sw_rem ??);
2457        whd in match (switch_removal ??);
2458        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
2459        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
2460        whd in match (exec_step ??);
2461        cases (Hexpr_related cond) in Heq;
2462        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2463        | 1: cases (exec_expr ge e m cond)
2464             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2465             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
2466                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
2467                  cases (exec_bool_of_val condval (typeof cond))
2468                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2469                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
2470                       destruct (Heq_condval) whd in match (bindIO ??????);
2471                       normalize nodelta
2472                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
2473                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
2474                           [ 1: >Hiftrue_eq normalize // ]
2475                           #Hrewrite >Hrewrite %1
2476                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
2477                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
2478                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
2479                           [ 1: >Hiffalse_eq // ]
2480                           #Hrewrite >Hrewrite %1 try //
2481                           cut (uA = (\snd (switch_removal iftrue u)))
2482                           [ 1: >Hiftrue_eq //
2483                           | 2: #Heq_uA >Heq_uA
2484                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
2485                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
2486       ] ] ] ] ]
2487   | 6: (* While loop *) normalize nodelta
2488        whd in match (ret ??) in ⊢ (% → ?); #Heq
2489        @(eventually_now ????) whd in match (sw_rem ??);
2490        whd in match (switch_removal ??);
2491        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
2492        whd in match (exec_step ??);
2493        cases (Hexpr_related cond) in Heq;
2494        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2495        | 1: cases (exec_expr ge e m cond)
2496             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2497             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
2498                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
2499                  cases (exec_bool_of_val condval (typeof cond))
2500                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2501                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
2502                       destruct (Heq_condval) whd in match (bindIO ??????);
2503                       normalize nodelta
2504                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
2505                            cut (body' = (\fst (\fst (switch_removal body u))))
2506                            [ 1: >Hbody_eq // ]
2507                            #Hrewrite >Hrewrite %1
2508                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
2509                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
2510                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
2511                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
2512        ] ] ] ]
2513   | 7: (* Dowhile loop *) normalize nodelta
2514        whd in match (ret ??) in ⊢ (% → ?); #Heq
2515        @(eventually_now ????) whd in match (sw_rem ??);
2516        whd in match (switch_removal ??);
2517        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
2518        whd in match (exec_step ??);
2519        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
2520        try //
2521        cut (body' = (\fst (\fst (switch_removal body u))))
2522        [ 1: >Hbody_eq // ]
2523        #Hrewrite >Hrewrite %1
2524        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
2525        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
2526   | 8: (* For loop *) normalize nodelta
2527        whd in match (ret ??) in ⊢ (% → ?); #Heq
2528        @(eventually_now ????) whd in match (sw_rem ??);
2529        whd in match (switch_removal ??);
2530        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
2531        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
2532              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
2533              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
2534              whd in match (exec_step ??);
2535              cases (Hexpr_related cond)
2536              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2537              | 1: cases (exec_expr ge e m cond)
2538                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2539                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
2540                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
2541                        cases (exec_bool_of_val condval (typeof cond))
2542                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2543                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
2544                             destruct (Heq_condval)
2545                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
2546                                  try //
2547                                  cut (body' = (\fst (\fst (switch_removal body uA))))
2548                                  [ 1: >Hbody_eq // ]
2549                                  #Hrewrite >Hrewrite
2550                                  cut (uA = (\snd (switch_removal step u)))
2551                                  [ 1: >Hstep_eq // ] #HuA
2552                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
2553                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
2554                                  [ 1: >HuA @switch_removal_fresh assumption
2555                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
2556                                       [ >Hstep_eq // ]
2557                                       #Hstep >Hstep @swc_for2 try assumption
2558                                       @for_fresh_lift try assumption ]
2559                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
2560                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
2561               ] ] ] ]
2562        | 2: #Heq
2563             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
2564             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
2565             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
2566             whd in match (exec_step ??);
2567             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
2568             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
2569             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
2570             whd in match (ret ??); destruct (Heq)
2571             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
2572             @conj try //
2573             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
2574             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
2575             <for_commute [ 2: >Hstep_eq // ]
2576             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
2577             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
2578             @swc_seq try // @for_fresh_lift
2579             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
2580             >HuA_eq @switch_removal_fresh assumption       
2581       ]
2582   | 9: (* break *) normalize nodelta
2583        inversion Hsim_cont
2584        [ 1: #Hk #Hk' #_       
2585        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
2586        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
2587        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
2588        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
2589        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
2590        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
2591        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
2592        normalize nodelta #H try (destruct (H))
2593        whd in match (ret ??) in H; destruct (H)
2594        @(eventually_now ????)
2595        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
2596        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
2597    | 10: (* Continue *) normalize nodelta
2598        inversion Hsim_cont
2599        [ 1: #Hk #Hk' #_       
2600        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
2601        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
2602        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
2603        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
2604        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
2605        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
2606        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
2607        normalize nodelta #H try (destruct (H))
2608        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
2609        destruct (H)
2610        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
2611        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
2612             >while_commute %1{u0} try assumption
2613        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
2614             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2615             | 1: * #condval #trace whd in match (m_bind ?????);
2616                  #Heq *
2617                  [ 2: * #error #Habsurd destruct (Habsurd)
2618                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
2619                       whd in match (bindIO ??????);
2620                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
2621                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2622                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
2623                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)}
2624                                 @conj try // >dowhile_commute %1{u0} assumption
2625                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
2626                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
2627             ] ] ]
2628        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
2629             try // @(fresh_for_Scontinue … Hfor_fresh)
2630        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
2631             @conj try // %1{u0}
2632             elim (substatement_fresh … Hfor_fresh) * * try //
2633             #HSskip #Hcond #Hstep #Hbody
2634             @swc_for3 assumption
2635        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
2636             %1{u} try //
2637        ]
2638    | 11: (* Sreturn *) normalize nodelta #Heq
2639          @(eventually_now ????)
2640          whd in match (exec_step ??) in Heq ⊢ %;
2641          cases retval in Heq; normalize nodelta
2642          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
2643               whd in match (ret ??) in ⊢ (% → %);
2644               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
2645               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
2646               #H destruct (H)
2647               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
2648               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
2649          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
2650               [ 1: #_ #Habsurd destruct (Habsurd)
2651               | 2: #_ elim (Hexpr_related expr)
2652                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2653                    | 1: cases (exec_expr ??? expr)
2654                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2655                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
2656                              #Hrewrite >Hrewrite
2657                              whd in match (m_bind ?????); whd in match (m_bind ?????);
2658                              #Heq destruct (Heq)
2659                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
2660                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
2661         ] ] ] ]
2662    | 12: (* Sswitch. Main proof case. *) normalize nodelta
2663          (* Case analysis on the outcome of the tested expression *)
2664          cases (exec_expr_int ge e m cond)
2665          [ 2: cases (exec_expr ge e m cond)
2666               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
2667               | 1: * #val #trace cases val
2668                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
2669                    whd in match (m_bind ?????);
2670                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
2671                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
2672          ]
2673          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
2674          whd in match (m_bind ?????); #Heq
2675          destruct (Heq)
2676          @eventually_later
2677          whd in match (sw_rem (Sswitch cond switchcases) u);
2678          whd in match (switch_removal (Sswitch cond switchcases) u);
2679          elim (switch_removal_branches_eq switchcases u)
2680          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
2681          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
2682          [ 1: >Hsrb_eq // ] #Huv1_eq
2683          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
2684          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
2685          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
2686          whd in match (simplify_switch ???);
2687          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
2688          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
2689          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)         
2690          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
2691          #Huv4_eq
2692          whd in match (exec_step ??);
2693          %{(State (function_switch_removal f)
2694                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
2695                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
2696          %{E0} @conj try @refl
2697          %{tr} normalize in match (eq ???); @conj try //
2698          (* execute the conditional *)
2699          @eventually_later
2700          (* lift the result of the previous case analysis from [ge] to [ge'] *)
2701          whd in match (exec_step ??);
2702          whd in match (exec_lvalue ????);
2703         
2704          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
2705         
2706  *)
2707
2708(*
2709lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
2710  exec_expr ge e m cond = OK ? 〈v,tr〉 →
2711  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
2712  exec_expr ge' e m cond = OK ? 〈v,tr〉.
2713#ge #ge' #e #m #cond #v #tr #H *
2714[ 1: #Hsim >(Hsim ? H) //
2715| 2: * #error >H #Habsurd destruct (Habsurd) ]
2716qed. *)
2717
2718(*
2719lemma switch_simulation :
2720∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
2721 switch_cont_sim k k' →
2722 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
2723 fresh_for_statement (Sswitch cond switchcases) u →
2724 ∃tr'.
2725 (eventually ge'
2726  (λs2':state
2727   .switch_state_sim
2728    (State f
2729     (seq_of_labeled_statement (select_switch condsz condval switchcases))
2730     (Kswitch k) e m) s2')
2731  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
2732  tr').
2733#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
2734whd in match (sw_rem (Sswitch cond switchcases) u);
2735whd in match (switch_removal (Sswitch cond switchcases) u);
2736cases switchcases in Hfresh;
2737[ 1: #default_statement #Hfresh_for_default
2738     whd in match (switch_removal_branches ??);
2739     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
2740     elim (switch_removal_eq default_statement u)
2741     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
2742     normalize nodelta
2743     cut (u' = (\snd (switch_removal default_statement u)))
2744     [ 1: >Hdefault_statement_eq // ] #Heq_u'
2745     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
2746     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
2747     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
2748     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
2749     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
2750     normalize nodelta
2751     whd in match (simplify_switch (Expr ??) ?? uv2);
2752     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
2753     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
2754     -Hfreshness #Heq_uv3
2755     normalize nodelta whd in match (add_starting_lbl_list ????);
2756     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
2757     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
2758     -Hfreshness #Heq_uv4
2759     normalize nodelta
2760     @(eventually_later ge' ?? E0)
2761     whd in match (exec_step ??);
2762     %{(State (function_switch_removal f)
2763          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
2764          (Kseq
2765          (Ssequence
2766            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
2767            (Slabel exit_label Sskip))
2768          k') e m)} @conj try //
2769     @(eventually_later ge' ?? E0)
2770     whd in match (exec_step ??);
2771     
2772@chthulhu | @chthulhu
2773qed. *)
2774
2775
2776
2777 
Note: See TracBrowser for help on using the repository browser.