source: src/Clight/switchRemoval.ma @ 2407

Last change on this file since 2407 was 2391, checked in by campbell, 8 years ago

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

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