source: src/Clight/switchRemoval.ma @ 3367

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

Switch removal and labelling combined.

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