source: src/Clight/switchRemoval.ma @ 2588

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

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

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