source: src/Clight/switchRemoval.ma @ 2450

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

Minor typo

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