source: src/Clight/switchRemoval.ma @ 2734

Last change on this file since 2734 was 2734, checked in by mckinna, 7 years ago

yet another puzzling automation failure, in the repaired case:
"" now fails, while "assumption" succeeds?!

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