source: src/Clight/switchRemoval.ma @ 2438

Last change on this file since 2438 was 2438, checked in by garnier, 8 years ago

Sync of the w.i.p. for switch removal.

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