source: src/Clight/switchRemoval.ma @ 2441

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

Moved general stuff on memories from switchRemoval to MemProperties?, e.g. on loading, storing and free, as an
attempt to reduce the typechecking time of switchRemoval.ma.
Moved some other generic stuff on vectors from SimplifyCasts? to frontend_misc.

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