source: src/Clight/memoryInjections.ma @ 3178

Last change on this file since 3178 was 3178, checked in by campbell, 6 years ago

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

File size: 132.5 KB
Line 
1(*include "Clight/Cexec.ma".*)
2include "Clight/MemProperties.ma". 
3(*include "Clight/frontend_misc.ma".*)
4
5(* This file contains some definitions and lemmas related to memory injections.
6 * The whole development is quite similar to the one described in the article by
7 * Leroy & Blazy in J.A.R., except that in Cerco, we describe data down to the byte
8 * level (similar to the memory model of CompCert v2 but not to the aforementioned
9 * paper).
10 * *)
11
12(* --------------------------------------------------------------------------- *)   
13(* Aux lemmas that are likely to be found elsewhere. *)
14(* --------------------------------------------------------------------------- *)   
15
16lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
17#a #b #HA
18lapply (Zltb_true_to_Zlt … HA) #HA_prop
19@Zlt_to_Zltb_true /2/
20qed.
21
22lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
23#a @Zlt_to_Zltb_true /2/ qed.
24(*
25definition le_offset : offset → offset → bool.
26  λx,y. Zleb (offv x) (offv y).
27*)
28lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
29
30lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
31
32lemma eqZb_symmetric : ∀x,y:Z. eqZb x y = eqZb y x.
33#x #y @(eqZb_elim … x y)
34[ * >eqZb_z_z @refl
35| #Hneq >(eqZb_false … (sym_neq ??? Hneq)) @refl ]
36qed.
37
38(* TODO: move in frontend_misc. This axiom states that for small bitvectors, bitvector addition
39 * commutes with conversion to Z, i.e. there is no overflow. *)
40axiom Z_addition_bv_commute :
41  ∀n. ∀v1,v2:BitVector n.
42        (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2) < Z_two_power_nat n →
43        Z_of_unsigned_bitvector ? (addition_n ? v1 v2) =
44        (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2).
45
46(* TODO: move in frontend_misc *)
47lemma Zlt_to_Zneq : ∀x,y:Z. x < y → x ≠ y.
48#x #y /3 by absurd, nmk/
49qed.
50
51lemma Zlt_translate : ∀x,y,delta:Z. x < y → x + delta < y + delta.
52#x #y #delta /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle/
53qed.
54
55lemma Zlt_weaken : ∀x,y,delta:Z. delta ≥ 0 → x < y → x < y + delta.
56#x #y #delta cases delta try // #p
57[ 2: #Habsurd @(False_ind … Habsurd) ]
58/3 by Zlt_to_Zle_to_Zlt, Zplus_le_pos/
59qed.
60
61lemma Zlt_sum_weaken : ∀a,a',b,c:Z. a+b < c → a' < a → a'+b < c.
62#a #a' #b #c /3 by transitive_Zlt, Zlt_translate/ qed.
63
64
65(* TODO: move to Z.ma *)
66lemma monotonic_Zlt_Zsucc : monotonic Z Zlt Zsucc.
67#x #y cases x cases y /2/
68[ #n /3 by Zle_to_Zlt_to_Zlt, monotonic_Zle_Zplus_r/ ]
69#n #m @(pos_cases … n) @(pos_cases … m) //
70[ #n /3 by I, Zle_to_Zlt, monotonic_Zle_Zplus_r/
71| #m #n /3 by I, Zle_to_Zlt, monotonic_Zle_Zplus_r/
72| /2 by Zlt_translate/
73| /3 by Zle_to_Zlt, monotonic_Zle_Zplus_r/
74| #n' /3 by Zle_to_Zlt_to_Zlt, lt_to_Zlt_neg_neg, Zlt_to_Zle/
75| #n' #m' /3 by lt_plus_to_lt_r, lt_to_Zlt_neg_neg/ ]
76qed.
77
78lemma monotonic_Zlt_Zpred : monotonic Z Zlt Zpred.
79#x #y cases x cases y /2/
80[ #n /3 by Zle_to_Zlt, monotonic_Zle_Zpred/
81| #m #n @(pos_cases … n) @(pos_cases … m)
82  [ /3 by monotonic_Zlt_Zsucc/
83  | /3 by refl, true_to_andb_true, Zltb_true_to_Zlt/
84  | #n' cases n' normalize
85    [ #H inversion H [ #H' destruct | #m' #_ #_ #Habsurd  @(absurd … Habsurd (not_eq_one_succ m')) ]
86    | #p /3 by le_to_lt_to_lt, le_S_contradiction_1/
87    | #p /3 by le_to_lt_to_lt, le_S_contradiction_1/ ]
88  | #m' #n' /3 by lt_plus_to_lt_r, lt_to_Zlt_pos_pos/ ]
89| #m #n /3 by Zplus_le_pos, Zle_to_Zlt/
90] qed. 
91
92lemma monotonic_Zlt_Zplus_l: ∀n.monotonic Z Zlt (λm.m + n).
93#n cases n // #n' #a #b #H
94[ @(pos_elim … n')
95  [ >sym_Zplus >(sym_Zplus b) <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) @monotonic_Zlt_Zsucc @H
96  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //
97      >(Zplus_Zsucc …) >(Zplus_Zsucc …) //
98      cases a in H; cases b /2/
99      #p #H /3 by Zlt_to_Zle_to_Zlt, monotonic_Zle_Zsucc, monotonic_Zlt_Zsucc/
100  ]
101| @(pos_elim … n')
102  [ >sym_Zplus >(sym_Zplus b)  <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
103  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //
104    /3 by Zle_to_Zlt_to_Zlt, monotonic_Zlt_Zpred/
105  ]
106] qed.
107
108
109lemma Zlt_to_Zle' : ∀x,y:Z. x < y → x ≤ y.
110#x #y /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/
111qed.
112
113       
114
115(* --------------------------------------------------------------------------- *)
116(* Some shorthands for conversion functions from BitVectorZ. *)
117(* --------------------------------------------------------------------------- *)
118
119(* Offsets are just bitvectors packed inside some annoying constructor. *)
120definition Zoo ≝ λx. Z_of_unsigned_bitvector ? (offv x).
121definition boo ≝ λx. mk_offset (bitvector_of_Z ? x).
122
123(* --------------------------------------------------------------------------- *)   
124(* In the definition of injections below, we maintain a list of blocks that are
125   writeable. We need some lemmas to reason on the fact that a block cannot be
126   both writeable and not writeable, etc. *)
127(* --------------------------------------------------------------------------- *)
128
129(* When equality on A is decidable, [mem A elt l] is too. *)
130lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
131#A #dec #elt #l elim l
132[ 1: normalize %2 /2/
133| 2: #hd #tl #Hind
134     elim (dec elt hd)
135     [ 1: #Heq >Heq %1 /2/
136     | 2: #Hneq cases Hind
137        [ 1: #Hmem %1 /2/
138        | 2: #Hnmem %2 normalize
139              % #H cases H
140              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
141              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
142] ] ]
143qed.
144
145
146lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
147* #a * #b
148cases (decidable_eq_Z … a b)
149[ * %1 @refl
150| #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed.
151
152lemma block_decidable_eq : ∀a,b:block. (a = b) + (a ≠ b).
153* #a * #b
154cases (decidable_eq_Z_Type … a b)
155[ * %1 @refl
156| #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed.
157
158lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
159#l #elt1 #elt2 elim l
160[ 1: normalize #Habsurd @(False_ind … Habsurd)
161| 2: #hd #tl #Hind normalize #Hl #Hr
162   cases Hl
163   [ 1: #Heq >Heq
164        @(eq_block_elim … hd elt2)
165        [ 1: #Heq >Heq /2 by not_to_not/
166        | 2: #x @x ]
167   | 2: #Hmem1 cases (mem_dec ? block_eq_dec ? tl)
168        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
169        | 2: #Hmem2 @Hind //
170        ]
171   ]
172] qed.
173
174lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
175#b1 #b2 * #Hb
176@(eq_block_elim … b1 b2)
177[ 1: #Habsurd @(False_ind … (Hb Habsurd))
178| 2: // ] qed.
179
180(* --------------------------------------------------------------------------- *)   
181(* Lemmas related to freeing memory and pointer validity. *)
182(* --------------------------------------------------------------------------- *)   
183
184lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr.
185   valid_pointer m ptr = true →
186   pblock ptr ≠ b →
187   valid_pointer (free m b) ptr = true.
188* (* #br *) #bid * #contents #next #posnext * * (* #pbr *) #pbid #poff
189normalize
190@(eqZb_elim pbid bid)
191[ 1: #Heqid >Heqid (* cases pbr cases br normalize *)
192     cases (Zltb bid next) normalize nodelta
193     [ 2: #Habsurd destruct (Habsurd) ]
194     #_ #H @False_ind @(absurd … (refl ??) H)
195| 2: #Hneqid (* cases pbr cases br normalize *) try // ]
196qed.
197
198lemma free_list_cons : ∀m,b,tl. free_list m (b :: tl) = (free (free_list m tl) b).
199#m #b #tl whd in match (free_list ??) in ⊢ (??%%);
200whd in match (free ??); @refl qed.
201
202(*
203lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
204   valid_pointer (free m b) ptr = true →
205   pblock ptr ≠ b → (* This hypothesis is necessary to handle the cse of "valid" pointers to empty  *)
206   valid_pointer m ptr = true.
207* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
208@(eqZb_elim pbid bid)
209[ 1: #Heqid >Heqid
210     cases pbr cases br normalize
211     [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
212     cases (Zltb bid next) normalize nodelta
213     [ 2,4: #Habsurd destruct (Habsurd) ]
214     //
215| 2: #Hneqid cases pbr cases br normalize try //
216     >(eqZb_false … Hneqid) normalize nodelta try //
217qed.
218
219lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr.
220   valid_pointer (free_list m blocks) ptr = true →
221   ¬ mem ? (pblock ptr) blocks →
222   valid_pointer m ptr = true.
223#blocks
224elim blocks
225[ 1: #m #ptr normalize #H #_ @H
226| 2: #b #tl #Hind #m #ptr #Hvalid
227     whd in match (mem block (pblock ptr) ?);
228     >free_list_cons in Hvalid; #Hvalid * #Hguard
229     lapply (valid_pointer_free_ok … Hvalid) #H
230     @Hind
231     [ 2: % #Heq @Hguard %2 @Heq
232     | 1: @H % #Heq @Hguard %1 @Heq ]
233] qed. *)
234
235(* An alternative version without the gard on the equality of blocks. *)
236(*
237lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr.
238   valid_pointer (free m b) ptr = true →
239   (pblock ptr) = b ∨ (pblock ptr ≠ b ∧ valid_pointer m ptr = true).
240* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
241@(eq_block_elim … (mk_block br bid) (mk_block pbr pbid))
242[ 1: #Heq #_ %1 @(sym_eq … Heq)
243| 2: cases pbr cases br normalize nodelta
244     [ 1,4: @(eqZb_elim pbid bid)
245         [ 1,3: #Heq >Heq * #H @(False_ind … (H (refl ??)))
246         | 2,4: #Hneq #_ normalize >(eqZb_false … Hneq) normalize nodelta
247                 #H %2 @conj try assumption
248                 % #Habsurd destruct (Habsurd) elim Hneq #Hneq @Hneq try @refl
249         ]
250     | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ]
251] qed. *)
252
253(* Well in fact a valid pointer can be valid even after a free. Ah. *)
254(*
255lemma pointer_in_free_list_not_valid : ∀blocks,m,ptr.
256  mem ? (pblock ptr) blocks →
257  valid_pointer (free_list m blocks) ptr = false.
258*)
259(*
260#blocks elim blocks
261[ 1: #m #ptr normalize #Habsurd @(False_ind … Habsurd)
262| 2: #b #tl #Hind #m #ptr
263     whd in match (mem block (pblock ptr) ?);
264     >free_list_cons
265     *
266     [ 1: #Hptr_match whd in match (free ??);
267          whd in match (update_block ????);
268          whd in match (valid_pointer ??);
269          whd in match (low_bound ??);
270          whd in match (high_bound ??);
271          >Hptr_match >eq_block_identity normalize nodelta
272          whd in match (low ?);
273          cut (Zleb OZ (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) = true)
274          [ 1: elim (offv (poff ptr)) //
275               #n' #hd #tl cases hd normalize
276               [ 1: #_ try @refl
277               | 2: #H @H ] ]
278          #H >H
279          cut (Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) OZ = false)
280          [ 1: elim (offv (poff ptr)) normalize
281               #n' #hd #tl cases hd normalize
282               [ 1: normalize #_ try @refl
283               | 2: #H @H ] ]
284  valid_pointer (free_list m blocks) ptr = false.
285*)
286
287
288(* --------------------------------------------------------------------------- *)   
289(* Memory injections *)
290(* --------------------------------------------------------------------------- *)   
291
292(* An embedding is a function from block ids to (blocks × offset). *)
293definition embedding ≝ block → option (block × offset).
294
295definition offset_plus : offset → offset → offset ≝
296  λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)).
297
298lemma offset_plus_0 : ∀o. offset_plus (mk_offset (zero ?)) o = o.
299* #o
300whd in match (offset_plus ??);
301>commutative_addition_n
302>addition_n_0 @refl
303qed.
304
305(* Translates a pointer through an embedding. *)
306definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
307λp,E.
308match p with
309[ mk_pointer pblock poff ⇒
310   match E pblock with
311   [ None ⇒ None ?
312   | Some loc ⇒
313    let 〈dest_block,dest_off〉 ≝ loc in
314    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
315    Some ? ptr
316   ]
317].
318
319(* Definition of embedding compatibility. *)
320definition embedding_compatible : embedding → embedding → Prop ≝
321λE,E'.
322  ∀b:block. E b = None ? ∨
323            E b = E' b.
324
325(* We parameterise the "equivalence" relation on values with an embedding. *)
326(* Front-end values. *)
327inductive value_eq (E : embedding) : val → val → Prop ≝
328| undef_eq :
329  value_eq E Vundef Vundef
330| vint_eq : ∀sz,i.
331  value_eq E (Vint sz i) (Vint sz i)
332| vnull_eq :
333  value_eq E Vnull Vnull
334| vptr_eq : ∀p1,p2.
335  pointer_translation p1 E = Some ? p2 →
336  value_eq E (Vptr p1) (Vptr p2).
337 
338(* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t.
339 * the values are equivalent. *)
340definition load_sim ≝
341λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
342 ∀b1,off1,b2,off2,ty,v1.
343  valid_block m1 b1 →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
344  E b1 = Some ? 〈b2,off2〉 →
345  load_value_of_type ty m1 b1 off1 = Some ? v1 →
346  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
347 
348definition load_sim_ptr ≝
349λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
350 ∀b1,off1,b2,off2,ty,v1.
351  valid_pointer m1 (mk_pointer b1 off1) = true →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
352  pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →
353  load_value_of_type ty m1 b1 off1 = Some ? v1 →
354  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
355
356definition block_is_empty : mem → block → Prop ≝
357λm,b.
358  high_bound m b ≤ low_bound m b.
359 
360(* Definition of a 16 bit bitvector-implementable Z *)
361definition z_implementable_bv : Z → Prop ≝
362  λz:Z.
363    0 ≤ z ∧ z < Z_two_power_nat 16.
364
365(* Characterizing implementable blocks *)
366definition block_implementable_bv ≝
367  λm:mem.λb:block.
368   z_implementable_bv (low_bound m b) ∧
369   z_implementable_bv (high_bound m b).  (* FIXME this is slightly restrictive. We could allow the high bound to be 2^16.*)
370
371(* Characterizing blocks compatible with an embedding. This condition ensures
372 * that we do not stray out of memory. *)
373(*
374definition block_ok_with_embedding ≝ λE:embedding.λb,m.
375  ∀b',delta.
376    E b = Some ? 〈b', delta〉 →
377    (high_bound m b) + (Zoo delta) < Z_two_power_nat 16. *)
378
379(* We have to prove that the blocks we allocate are compatible with a given embedding.
380   This amounts to proving that the embedding cannot shift the new block outside the 2^16 bound.
381   Notice that the following def. only constraints block mapped through the embedding.
382*)
383definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝
384λE.λb.λm,m'.
385  match E b with
386  [ None ⇒ True
387  | Some loc ⇒
388    let 〈b', delta〉 ≝ loc in
389    block_implementable_bv m b ∧
390    block_implementable_bv m' b' ∧
391    (high_bound m b) + (Zoo delta) < Z_two_power_nat 16
392  ].
393
394(* Adapted from Compcert's Memory *)
395definition non_aliasing : embedding → mem → Prop ≝
396  λE,m.
397  ∀b1,b2,b1',b2',delta1,delta2.
398  b1 ≠ b2 → (* note that two blocks can be different only becuase of this region *)
399  E b1 = Some ? 〈b1',delta1〉 →
400  E b2 = Some ? 〈b2',delta2〉 →
401  (if eq_block b1' b2' then
402    (* block_is_empty m b1' ∨ *)
403    high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
404    high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) ∨
405    block_is_empty m b1 ∨
406    block_is_empty m b2
407   else
408    True).
409
410
411(* Adapted from Compcert's "Memory" *)
412
413(* Definition of a memory injection *)
414record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝
415{ (* Load simulation *)
416  mi_inj : load_sim_ptr E m1 m2;
417  (* Invalid blocks are not mapped *)
418  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
419  (* Valid pointers are mapped to valid pointers *)
420  mi_valid_pointers : ∀p,p'.
421                       valid_pointer m1 p = true →
422                       pointer_translation p E = Some ? p' →
423                       valid_pointer m2 p' = true;
424  (* Blocks in the codomain are valid *)
425  mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
426  (* Regions are preserved *)
427  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
428  (* sub-blocks do not overlap (non-aliasing property) *)
429  mi_nonalias : non_aliasing E m1;
430  (* mapped blocks are bitvector-implementable *)
431  (*  mi_implementable :
432    ∀b,b',o'.
433      E b = Some ? 〈b',o'〉 →
434      block_implementable_bv m1 b ∧
435      block_implementable_bv m2 b'; *)
436  (* The offset produced by the embedding shifts data within the 2^16 bound ...
437   * We need this to rule out the following case: consider a huge block taking up
438   * all the space [0; 2^16[. We can come up with an embedding that keeps the same block
439   * but which shifts the data by some value, effectively rotating all the data around the
440   * 2^16 offset limit. Valid pointers stay valid, the block is implementable ... But we
441   * obviously can't prove that the semantics of pointer comparisons is preserved. *)
442  mi_nowrap :
443    ∀b. block_in_bounds_if_mapped E b m1 m2
444}.
445
446(* ---------------------------------------------------------------------------- *)
447(* Setting up an empty injection *)
448(* ---------------------------------------------------------------------------- *)
449
450definition empty_injection : memory_inj (λx. None ?) empty empty.
451%
452[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload
453  normalize in Hptr_trans; destruct
454| #b #H @refl
455| * #b #o #p' #_ normalize #Habsurd destruct
456| #b #b' #off #Habsurd destruct
457| #b #b' #o' #Habsurd destruct
458| whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct
459| #b whd @I
460] qed.
461
462(* ---------------------------------------------------------------------------- *)
463(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
464(* ---------------------------------------------------------------------------- *)
465
466
467
468(**** Lemmas on value_eq. *)
469
470(* particulars inversions. *)
471lemma value_eq_ptr_inversion :
472  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
473#E #p1 #v #Heq inversion Heq
474[ 1: #Habsurd destruct (Habsurd)
475| 2: #sz #i #Habsurd destruct (Habsurd)
476| 3:  #Habsurd destruct (Habsurd)
477| 4: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
478     %{p2} @conj try @refl try assumption
479] qed.
480
481lemma value_eq_int_inversion :
482  ∀E,sz,i,v. value_eq E (Vint sz i) v → v = (Vint sz i).
483#E #sz #i #v #Heq inversion Heq
484[ 1: #Habsurd destruct (Habsurd)
485| 2: #sz #i #Heq #Heq' #_ @refl
486| 3: #Habsurd destruct (Habsurd)
487| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
488qed.
489
490lemma value_eq_int_inversion' :
491  ∀E,sz,i,v. value_eq E v (Vint sz i) → v = (Vint sz i).
492#E #sz #i #v #Heq inversion Heq
493[ 1: #_ #Habsurd destruct (Habsurd)
494| 2: #sz #i #Heq #Heq' #_ @refl
495| 3: #_ #Habsurd destruct (Habsurd)
496| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
497qed.
498
499lemma value_eq_null_inversion :
500  ∀E,v. value_eq E Vnull v → v = Vnull.
501#E #v #Heq inversion Heq //
502#p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd)
503#Habsurd' destruct
504qed.
505
506lemma value_eq_null_inversion' :
507  ∀E,v. value_eq E v Vnull → v = Vnull.
508#E #v #Heq inversion Heq //
509#p1 #p2 #Htranslate #_ #Habsurd lapply (jmeq_to_eq ??? Habsurd)
510#Habsurd' destruct
511qed.
512
513(* A cleaner version of inversion for [value_eq] *)
514lemma value_eq_inversion :
515  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
516  (P Vundef Vundef) →
517  (∀sz,i. P (Vint sz i) (Vint sz i)) →
518  (P Vnull Vnull) →
519  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
520  P v1 v2.
521#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4
522inversion Heq
523[ 1: #Hv1 #Hv2 #_ destruct @H1
524| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
525| 3: #Hv1 #Hv2 #_ destruct @H3
526| 4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed.
527
528(* Avoids the use of cut in toCminorCorrectness *)
529lemma value_eq_triangle_diagram :
530  ∀E,v1,v2,v3.
531  value_eq E v1 v2 → v2 = v3 → value_eq E v1 v3.
532#H1 #H2 #H3 #H4 #H5 #H6 destruct //
533qed. 
534
535(* embedding compatibility preserves value equivalence *)
536(* This is lemma 65 of Leroy&Blazy. *)
537lemma embedding_compatibility_value_eq :
538  ∀E,E'. embedding_compatible E E' → ∀v1,v2. value_eq E v1 v2 → value_eq E' v1 v2.
539#E #E' #Hcompat #v1 #v2 #Hvalue_eq
540@(value_eq_inversion … Hvalue_eq) try //
541#p1 #p2 whd in match (pointer_translation ??); cases p1 #b1 #o1 normalize nodelta
542cases (Hcompat b1)
543[ #Hnone >Hnone normalize nodelta #Habsurd destruct
544| #Heq >Heq #Hres %4 @Hres ]
545qed.
546
547
548
549
550(**** Lemmas on pointer validity wrt loads. *)
551
552(* If we succeed to load something by value from a 〈b,off〉 location,
553   [b] is a valid block. *)
554(*   
555lemma load_by_value_success_valid_block_aux :
556  ∀ty,m,b,off,v.
557    access_mode ty = By_value (typ_of_type ty) →
558    load_value_of_type ty m b off = Some ? v →
559    Zltb (block_id b) (nextblock m) = true.
560#ty #m * #brg #bid #off #v
561cases ty
562[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
563| #structname #fieldspec | #unionname #fieldspec | #id ]
564whd in match (load_value_of_type ????);
565[ 1,6,7: #_ #Habsurd destruct (Habsurd) ]
566#Hmode
567[ 1,2,5: [ 1: elim sz ]
568     normalize in match (typesize ?);
569     whd in match (loadn ???);
570     whd in match (beloadv ??);
571     cases (Zltb bid (nextblock m)) normalize nodelta
572     try // #Habsurd destruct (Habsurd)
573| *: normalize in Hmode; destruct (Hmode)
574] qed. *)
575
576(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
577lemma load_by_value_success_valid_ptr_aux :
578  ∀ty,m,b,off,v.
579    access_mode ty = By_value (typ_of_type ty) →
580    load_value_of_type ty m b off = Some ? v →
581    Zltb (block_id b) (nextblock m) = true ∧
582    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
583    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
584#ty #m * (* #brg *) #bid #off #v
585cases ty
586[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
587| #structname #fieldspec | #unionname #fieldspec | #id ]
588whd in match (load_value_of_type ????);
589[ 1,6,7: #_ #Habsurd destruct (Habsurd) ]
590#Hmode
591[ 1,2,5: [ 1: elim sz  ]
592     normalize in match (typesize ?);
593     whd in match (loadn ???);
594     whd in match (beloadv ??);
595     cases (Zltb bid (nextblock m)) normalize nodelta
596     cases (Zleb (low (blocks m (mk_block (*brg*) bid)))
597                  (Z_of_unsigned_bitvector offset_size (offv off)))
598     cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block (*brg*) bid))))
599     normalize nodelta
600     #Heq destruct (Heq)
601     try /3 by conj, refl/
602| *: normalize in Hmode; destruct (Hmode)
603] qed.
604
605lemma load_by_value_success_valid_block :
606  ∀ty,m,b,off,v.
607    access_mode ty = By_value (typ_of_type ty) →
608    load_value_of_type ty m b off = Some ? v →
609    valid_block m b.
610#ty #m #b #off #v #Haccess_mode #Hload
611@Zltb_true_to_Zlt
612elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
613qed.
614
615lemma load_by_value_success_valid_pointer :
616  ∀ty,m,b,off,v.
617    access_mode ty = By_value (typ_of_type ty) →
618    load_value_of_type ty m b off = Some ? v →
619    valid_pointer m (mk_pointer b off) = true.
620#ty #m #b #off #v #Haccess_mode #Hload normalize
621elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
622* #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @refl
623qed.
624
625
626
627(**** Lemmas related to memory injections. *)
628
629(* Making explicit the contents of memory_inj for load_value_of_type.
630 * Equivalent to Lemma 59 of Leroy & Blazy *)
631lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
632    memory_inj E m1 m2 →
633    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
634    load_value_of_type ty m1 b1 off1 = Some ? v1 →
635    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
636#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
637lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
638lapply (refl ? (access_mode ty))
639cases ty
640[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
641| #structname #fieldspec | #unionname #fieldspec | #id ]
642normalize in ⊢ ((???%) → ?); #Hmode #Hyp
643[ 1,6,7: normalize in Hyp; destruct (Hyp)
644| 4,5: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
645lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
646lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
647qed.
648
649
650(* Lemmas pertaining to memory allocation *)
651
652(*
653lemma alloc_valid_block_not_eq :
654  ∀m,m',z1,z2,(*r,*)new_block.
655  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
656  ∀b. valid_block m b → b ≠ new_block.
657* #c #n #Hn #m' #z1 #z2 #new
658whd in ⊢ ((??%?) → ?); #Heq destruct
659#b whd in ⊢ (% → ?); cases b #bid
660#Hlt % #Heq destruct (Heq)
661@(absurd … Hlt (irreflexive_Zlt n))
662qed. 
663*)
664(* A valid block stays valid after an alloc. *)
665lemma alloc_valid_block_conservation :
666  ∀m,m',z1,z2,(*r,*)new_block.
667  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
668  ∀b. valid_block m b → valid_block m' b.
669#m #m' #z1 #z2 (* #r*) * #b' (* #Hregion_eq *)
670elim m #contents #nextblock #Hcorrect whd in match (alloc ???(*?*));
671#Halloc destruct (Halloc)
672#b whd in match (valid_block ??) in ⊢ (% → %); /2/
673qed.
674
675lemma Zle_split :
676  ∀a,b:Z. a ≤ b → a ≠ b → a <  b.
677#a #b elim a elim b try /2/
678#p1 #p2 #Hle #Hneq whd
679@not_eq_to_le_to_lt
680try // % #Heq destruct cases Hneq #H @H @refl
681qed.
682
683(* A valid block /after/ an alloc was valid before if it is different
684 * from the newly allocated one. *)
685lemma alloc_valid_block_conservation2 :
686  ∀m,m',z1,z2,new_block.
687  alloc m z1 z2 =〈m',new_block〉 →
688  ∀b. b ≠ new_block →
689      valid_block m' b →
690      valid_block m b.
691#m #m' #z1 #z2 #new_block
692cases m #cont #next #Hnext
693whd in ⊢ ((??%%) → ?);
694#Heq destruct (Heq) #b #Hneq #Hvalid
695whd in Hvalid ⊢ %;
696cases b in Hneq Hvalid; #bid * #H #Hlt
697cut (bid ≠ next)
698[ % #Heq destruct @H @refl ]
699#Hneq
700@(Zle_split … Hneq)
701/3 by monotonic_Zle_Zpred, Zlt_to_Zle/
702qed.
703
704lemma alloc_bounds_conservation :
705  ∀m,m',z1,z2,new_block.
706  alloc m z1 z2 =〈m',new_block〉 →
707  ∀b. b ≠ new_block →
708      low_bound m' b = low_bound m b ∧
709      high_bound m' b = high_bound m b.
710#m #m' #z1 #z2 #new #Halloc #b
711#Hneq cases m in Halloc; #c #n #Hn
712whd in ⊢ ((??%?) → ?); #Heq destruct
713@conj
714[ >unfold_low_bound whd in match (update_block ?????);
715  >(neq_block_eq_block_false … Hneq) @refl
716| >unfold_high_bound whd in match (update_block ?????);
717  >(neq_block_eq_block_false … Hneq) @refl
718] qed.
719
720(* A valid pointer stays valid after an alloc *)
721
722lemma alloc_valid_pointer_conservation :
723  ∀m,m',z1,z2,(*r,*)new_block.
724  alloc m z1 z2 (*r*) = 〈m',new_block〉 →
725  ∀p. (pblock p) ≠ new_block →
726      valid_pointer m' p = true →
727      valid_pointer m p = true.
728#m #m' #z1 #z2 (*#r*) #new_block
729cases m #cont #next #Hnext
730whd in ⊢ ((??%%) → ?);
731#Heq destruct (Heq) * #b #o #Hneq #Hvalid
732@valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
733-Hvalid
734* * #Hblock_id
735>unfold_low_bound >unfold_high_bound
736>unfold_low_bound >unfold_high_bound
737whd in match (update_block ?????);
738whd in match (update_block ?????);
739cut (b ≠ (mk_block (*r*) next))
740[ @(eq_block_elim … b (mk_block (*r*) next)) #H destruct try //
741  @False_ind
742  @(absurd … (refl ??) Hneq) ] #Hneqb
743>(not_eq_block … Hneqb) normalize nodelta
744#HA #HB % [ % ] try assumption
745cases b in Hneqb Hneq Hblock_id; (* #r'*) #id * #Hnext_not_id #Hneq
746#Hlt cut (id ≤ next)
747[ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ]
748#Hle @Zle_split try @Hle % #Heq destruct
749@(absurd … (refl ??) Hneq)
750qed.
751
752(* Allocating a new zone produces a valid block. *)
753lemma alloc_valid_new_block :
754  ∀m,m',z1,z2(*,r*),new_block.
755  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
756  valid_block m' new_block.
757* #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *)
758whd in match (alloc ???(*?*)); whd in match (valid_block ??);
759#Halloc destruct (Halloc) /2/
760qed.
761
762lemma new_block_invalid_before_alloc :
763  ∀m,m',z1,z2,new_block.
764  alloc m z1 z2 = 〈m', new_block〉 →
765  ¬valid_block m new_block.
766* #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *)
767whd in match (alloc ???(*?*)); whd in match (valid_block ??);
768#Halloc destruct (Halloc) /2/
769qed.
770
771
772(* All data in a valid block is unchanged after an alloc. *)
773lemma alloc_beloadv_conservation :
774  ∀m,m',block,offset,z1,z2,(*r,*)new_block.
775    valid_block m block →
776    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
777    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
778* #contents #next #Hcorrect #m' #block #offset #z1 #z2 (* #r*) #new_block #Hvalid #Halloc
779whd in Halloc:(??%?); destruct (Halloc)
780whd in match (beloadv ??) in ⊢ (??%%);
781lapply (Zlt_to_Zltb_true … Hvalid) #Hlt
782>Hlt >(zlt_succ … Hlt)
783normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
784cut (eqZb (block_id block) next = false)
785[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq
786>Hneq @refl
787qed.
788
789(* Lift [alloc_beloadv_conservation] to loadn *)
790lemma alloc_loadn_conservation :
791  ∀m,m',z1,z2,(*r,*)new_block.
792    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
793    ∀n. ∀block,offset.
794    valid_block m block →
795    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
796#m #m' #z1 #z2 (*#r*) #new_block #Halloc #n
797elim n try //
798#n' #Hind #block #offset #Hvalid_block
799whd in ⊢ (??%%);
800>(alloc_beloadv_conservation … Hvalid_block Halloc)
801cases (beloadv m' (mk_pointer block offset)) //
802#bev normalize nodelta
803whd in match (shift_pointer ???); >Hind try //
804qed.
805
806lemma alloc_load_value_of_type_conservation :
807  ∀m,m',z1,z2(*,r*),new_block.
808    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
809    ∀block,offset.
810    valid_block m block →
811    ∀ty. load_value_of_type ty m block offset =
812         load_value_of_type ty m' block offset.
813#m #m' #z1 #z2 (*#r*) #new_block #Halloc #block #offset #Hvalid         
814#ty cases ty
815[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
816| #structname #fieldspec | #unionname #fieldspec | #id ]
817try //
818whd in match (load_value_of_type ????) in ⊢ (??%%);
819>(alloc_loadn_conservation … Halloc … Hvalid) @refl
820qed.
821
822(* Memory allocation in m2 preserves [memory_inj].
823 * This is lemma 66 from Leroy&Blazy. *)
824lemma alloc_memory_inj_m2 :
825  ∀E:embedding.
826  ∀m1,m2,m2',z1,z2(*,r*),new_block.
827  ∀H:memory_inj E m1 m2.
828  alloc m2 z1 z2 (*r*) = 〈m2', new_block〉 →
829  block_implementable_bv m2' new_block →
830  memory_inj E m1 m2'.
831#E #m1 #m2 #m2' #z1 #z2 (*#r*) * #new_block (* #Hregion *) #Hmemory_inj #Halloc #Himpl
832%
833[ whd
834  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
835  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
836  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
837  lapply (refl ? (access_mode ty))
838  cases ty in Hload_eq;
839  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
840  | #structname #fieldspec | #unionname #fieldspec | #id ]
841  #Hload normalize in ⊢ ((???%) → ?); #Haccess
842  [ 1,6,7: normalize in Hload; destruct (Hload)
843  | 2,3,8:
844     lapply (load_by_value_success_valid_block … Haccess Hload)
845     #Hvalid_block
846      <(alloc_load_value_of_type_conservation … Halloc … Hvalid_block)
847     assumption
848  | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
849| @(mi_freeblock … Hmemory_inj)
850| #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
851     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
852     elim p' * (*#br'*) #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
853     whd in match (valid_pointer ??) in ⊢ (% → %);
854     @Zltb_elim_Type0
855     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
856     #Hbid' cut (Zltb bid' (Zsucc new_block) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
857     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
858     whd in match (high_bound ??) in ⊢ (% → %);
859     whd in match (update_block ?????);
860     whd in match (eq_block ??);
861     cut (eqZb bid' new_block = false) [ 1: @eqZb_false /2 by not_to_not/ ]
862     #Hbid_neq >Hbid_neq #H @H
863(*     cases (eq_region br' r) normalize #H @H*)
864| #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H
865  @(alloc_valid_block_conservation … Halloc … H)
866| @(mi_region … Hmemory_inj)
867| @(mi_nonalias … Hmemory_inj)
868| #b lapply (mi_nowrap … Hmemory_inj b)
869   whd in ⊢ (% → %);
870   lapply (mi_nodangling … Hmemory_inj b)
871   cases (E b) normalize nodelta try //
872   * #B #OFF normalize nodelta #Hguard
873   * * #H1 #H2 #Hinbounds @conj try @conj try assumption
874   @(eq_block_elim … (mk_block new_block) B)
875   [ #H <H assumption
876   | #H cases m2 in Halloc H2; #contents #nextblock #notnull
877       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) *
878       >unfold_low_bound >unfold_high_bound #HA #HB
879       @conj
880       >unfold_low_bound >unfold_high_bound
881       whd in match (update_block ?????);
882       >(not_eq_block … (sym_neq ??? H)) normalize nodelta
883       try assumption ]
884] qed.
885
886(* Allocating in m1 such that the resulting block has no image in m2 preserves
887   the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as
888   in Blazy & Leroy. Notice that we must consider blocks with different regions but
889   same id as equal. *)
890lemma alloc_memory_inj_m1 :
891  ∀E:embedding.
892  ∀m1,m2,m1',z1,z2,(*r,*)new_block.
893  ∀H:memory_inj E m1 m2.
894  alloc m1 z1 z2 (*r*) = 〈m1', new_block〉 →
895  memory_inj (λx. if eq_block new_block x then None ? else E x) m1' m2 ∧
896  embedding_compatible E (λx. if eq_block new_block x then None ? else E x).
897#E #m1 #m2 #m1' #z1 #z2 (* #r*) #new_block (* #Hregion_eq *) #Hinj #Halloc
898cut (E new_block = None ?)
899[ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?);
900  #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
901#Hempty
902cut (embedding_compatible E
903     (λx.
904       if eq_block new_block x
905       then None (block×offset)
906       else E x))
907[ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 @Hempty ]
908#Hembedding_compatible @conj try assumption
909%
910[ whd #b1 #off1 #b2 #off2 #ty #v1
911  @(eq_block_elim … b1 new_block)
912  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta
913    #Habsurd destruct ]
914  #Hneq #Hvalid
915  whd in ⊢ ((??%?) → ?);
916  @(eq_block_elim … new_block b1)
917  normalize nodelta
918  [ #Heq #Habsurd destruct (Habsurd) ]
919  #Hneq_id
920  #Hembed #Hload
921  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) (sym_neq ??? Hneq_id) Hvalid)
922  #Hvalid'
923  cut (valid_block m1 b1)
924  [ cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block #_ #_ @Hvalid_block ]
925  #Hvalid_block
926  lapply (alloc_load_value_of_type_conservation … Halloc … off1 … Hvalid_block ty)
927  #Heq <Heq in Hload; #Hload
928  lapply (mi_inj … Hinj … Hvalid' … Hembed … Hload) * #v2 * #Hload2 #Hveq2
929  %{v2} @conj try assumption
930  @(embedding_compatibility_value_eq … Hveq2) assumption
931| #b #Hnot_valid @(eq_block_elim … new_block b)
932  normalize nodelta
933  [ #Heq @refl
934  | #Hneq @(mi_freeblock … Hinj) % #Hvalid cases Hnot_valid #H @H
935    @(alloc_valid_block_conservation … Halloc) assumption ]
936| #p #p' lapply (mi_valid_pointers … Hinj p p')
937  cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1'
938  whd in ⊢ ((??%%) → ?); 
939  @(eq_block_elim … new_block b) normalize nodelta
940  [ #Heq #Habsurd destruct ]
941  #Hneq #Hembed
942  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b o) (sym_neq ??? Hneq) Hvalid1')
943  #Hvalid1
944  @(Hvalidptr Hvalid1 Hembed)
945| #b #b' #o' @(eq_block_elim … new_block b)
946  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
947  normalize nodelta #Henq
948  @(mi_nodangling … Hinj)
949| #b #b' #o' @(eq_block_elim … new_block b)
950  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
951  #Hneq @(mi_region … Hinj)
952| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
953  @(eq_block_elim … new_block b1)
954  normalize nodelta
955  [ #Heq #Habsurd destruct (Habsurd) ]
956  #Hneq1 #Hembed1
957  @(eq_block_elim … new_block b2)
958  normalize nodelta
959  [ #Heq #Habsurd destruct (Habsurd) ]
960  #Hneq2 #Hembed2
961  @(eq_block_elim … b1' b2') normalize nodelta try //
962  #Heq
963  lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq
964  >eq_block_b_b normalize nodelta
965  cases m1 in Halloc; #contents #next #Hnext
966  >unfold_high_bound >unfold_low_bound
967  >unfold_high_bound >unfold_low_bound
968  >unfold_high_bound >unfold_low_bound
969  >unfold_high_bound >unfold_low_bound
970  whd in ⊢ ((??%%) → ?); destruct (Heq) #Heq destruct (Heq)
971  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq1))
972  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq2))
973  #Heq_block_2
974  #Heq_block_1
975  * [ * [ * | ] | ]
976  whd in match (update_block ?????);
977  >Heq_block_1 normalize nodelta
978  whd in match (update_block ?????);
979  >Heq_block_2 normalize nodelta
980  #H
981  try /4 by or_introl, or_intror, conj/
982  [ %1 %2 whd whd in H;
983    >unfold_high_bound
984    whd in match (update_block ?????);
985    >unfold_low_bound
986    whd in match (update_block ?????);
987    >Heq_block_1 normalize nodelta @H
988  | %2 whd whd in H;
989    >unfold_high_bound
990    whd in match (update_block ?????);
991    >unfold_low_bound
992    whd in match (update_block ?????);
993    >Heq_block_1 >Heq_block_2 @H
994  ]
995| #b whd @(eq_block_elim … new_block b) normalize nodelta try //
996  #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
997  cases (E b) normalize nodelta try //
998  * #bb #oo normalize nodelta
999  * * * #HA #HB * #HC #HD #HE @conj try @conj
1000  try @conj
1001  lapply HE -HE
1002  lapply HD -HD
1003  lapply HC -HC
1004  lapply HB -HB
1005  lapply HA -HA
1006  >unfold_low_bound >unfold_low_bound [ >unfold_low_bound ]
1007  >unfold_high_bound >unfold_high_bound [ 2,5: >unfold_high_bound ]
1008 cases m1 in Halloc; #cont #next #Hnext
1009 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try //
1010 whd in match (update_block ?????);
1011 cut (eq_block b (mk_block next) = false)
1012 [ 1,3,5: @neq_block_eq_block_false @(sym_neq … Hneq)
1013 | 2,4,6: #Heq_block >Heq_block // ]
1014] qed.
1015
1016(* loading by-value from a freshly allocated block yields either an undef value or
1017 * None. *)
1018lemma load_by_value_after_alloc_undef :
1019  ∀m,m',z1,z2,b.
1020    alloc m z1 z2 = 〈m', b〉 →
1021    ∀ty. access_mode ty = By_value (typ_of_type ty) →
1022    ∀off. load_value_of_type ty m' b off = Some ? Vundef ∨
1023          load_value_of_type ty m' b off = None ?.
1024#m #m' #z1 #z2 (* * #br  #bid *) #b
1025cases m #contents #nextblock #Hnext
1026whd in ⊢ ((??%?) → ?);
1027#Heq destruct (Heq)
1028#ty cases ty   
1029[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1030| #structname #fieldspec | #unionname #fieldspec | #id ]
1031whd in ⊢ ((??%?) → ?);
1032#Heq destruct (Heq)
1033#off
1034whd in match (load_value_of_type ????);
1035(* We can't generalize over the typesize, sadly. We thus perform three identical inductions.
1036 * Another solution would be to provide an ad-hoc lemma, but the goal is too ugly for that. *)
1037[ lapply off -off
1038  generalize in match (typesize ?); #tsz
1039| lapply off -off
1040  generalize in match (typesize ?); #tsz
1041| lapply off -off
1042  generalize in match (typesize ?); #tsz
1043]
1044elim tsz 
1045[ 1,3,5: #off whd in match (loadn ???); normalize nodelta %1 @refl
1046| *: #tsz' #Hind #off
1047    whd in match (loadn ???);
1048    whd in match (beloadv ??);
1049    cases (Zltb ??) normalize nodelta try /1 by or_intror/
1050    cases (Zleb ??) normalize nodelta try /1 by or_intror/
1051    >andb_lsimpl_true
1052    cases (Zltb ??); normalize nodelta try /1 by or_intror/
1053    whd in match (update_block ?????);
1054    >eq_block_b_b normalize nodelta
1055    cases (Hind (shift_offset 2 off (bitvector_of_nat 2 1)))
1056    cases (loadn ???) normalize nodelta try //
1057    #bevals #Heq %1 whd in match (be_to_fe_value ??);
1058    try @refl ]
1059qed.
1060
1061
1062(* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order
1063 * to prove the equivalent of lemma 68 of L&B, we need to provide an additional
1064 * property of the target memory: the /target/ portion of memory we are going to map a block
1065 * to must only contains BVundef (whereas in CompCert, the fact that the source block
1066 * contains BVundefs is enough to proceed).
1067 *
1068 * The following definition expresses the fact that a portion of memory [z1; z2] contains only
1069 * BVundefs.
1070 * Note that the bounds are /inclusive/. We do not check for their validity. *)
1071definition undef_memory_zone : mem → block → Z → Z → Prop ≝
1072  λm,b,z1,z2.
1073    ∀i. z1 ≤ i → i ≤ z2 → contents (blocks m b) i = BVundef.
1074
1075(* Explictly stating the properties of alloc. *)
1076lemma alloc_properties :
1077  ∀m,m',z1,z2(*,r*),b.
1078   alloc m z1 z2 (* r *) = 〈m',b〉 →
1079   low_bound m' b = z1 ∧
1080   high_bound m' b = z2 ∧
1081   undef_memory_zone m' b z1 z2.
1082#m #m'  #z1 #z2 * (* #br *) #bid
1083cases m #contents #next #Hnext
1084whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1085>unfold_low_bound >unfold_high_bound
1086@conj try @conj
1087/2 by refl, pair_destruct_2/
1088whd
1089#i #H1 #H2 whd in match (update_block ?????);
1090>eq_block_b_b normalize nodelta @refl
1091qed.
1092
1093
1094(* Embed a fresh block inside an unmapped portion of the target block.
1095 * This is the equivalent of lemma 68 of Leroy&Blazy.
1096 * Compared to L&B, an additional "undef_memory_zone" proof object must be provided.
1097 * We also constrain the memory bounds of the new block to be bitvector-implementable,
1098 * otherwise we can't prove that addition commutes with conversions between Z and
1099 * bitvectors.
1100 *)
1101lemma alloc_memory_inj_m1_to_m2 :
1102  ∀E:embedding.
1103  ∀m1,m2,m1':mem.
1104  ∀z1,z2:Z.
1105  ∀target,new_block.
1106  ∀delta:offset.
1107  valid_block m2 target →
1108  block_implementable_bv m1' new_block →
1109  block_implementable_bv m2 target →
1110  block_region new_block = block_region target →
1111  (high_bound m1' new_block) + (Zoo delta) < Z_two_power_nat 16 →
1112  alloc m1 z1 z2 = 〈m1', new_block〉 →
1113  low_bound m2 target ≤ z1 + Zoo delta →
1114  z2 + Zoo delta ≤ high_bound m2 target →
1115  undef_memory_zone m2 target (z1 + Zoo delta) (z2 + Zoo delta) →
1116  (∀b,delta'. b ≠ new_block →
1117              E b = Some ? 〈target, delta'〉 →
1118              high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
1119              z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →
1120  memory_inj E m1 m2 →
1121  memory_inj (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x) m1' m2.
1122#E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #target (* * * #newr *) #new_block (* * *) #delta
1123#Hvalid #Himpl1 #Himpl2 #Hregion #Hno_overflow #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj
1124cut (E new_block = (None ?))
1125[ @(mi_freeblock ??? Hinj new_block) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj
1126  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
1127#Hnew_not_mapped
1128cut (embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x))
1129[ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 assumption ]
1130#Hembedding_compatible
1131%
1132[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload
1133  @(eq_block_elim … new_block b1)
1134  [ 2: (* we do not load from the newly allocated block *)
1135     #Hneq
1136     (* prove that we can equivalently load from the memory before alloc *)
1137     cases (some_inversion ????? Hembed) * #target' #delta'
1138     >(neq_block_eq_block_false … Hneq) normalize nodelta
1139     * #Hembed #Heq destruct (Heq)
1140     cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh
1141     lapply (alloc_valid_block_conservation2 … Halloc … (sym_neq ??? Hneq) Hvalid_block')
1142     #Hvalid_block
1143     lapply (alloc_load_value_of_type_conservation … Halloc b1 off1 … Hvalid_block ty)
1144     #Heq_load <Heq_load in Hload; #Hload
1145     lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … (sym_neq ??? Hneq) Hvalid')     
1146     #Hvalid_ptr
1147     lapply (mi_inj … Hinj b1 off1 b2 (offset_plus off1 delta') … Hvalid_ptr … Hload)
1148     [ whd in ⊢ (??%?); >Hembed @refl ]
1149     (* conclude *)
1150     * #v2 * #Hload2 #Hvalue_eq %{v2} @conj
1151     [ @Hload2
1152     | @(embedding_compatibility_value_eq … Hvalue_eq) @Hembedding_compatible ]
1153  | 1: (* we allegedly performed a load from a block with the same id as
1154        * the newly allocated block (which by def. of alloc contains only BVundefs) *)
1155     #Heq destruct (Heq)
1156     whd in Hembed:(??%?); >eq_block_b_b in Hembed; normalize nodelta
1157     #Heq_ptr
1158     (* cull out all boring cases *)
1159     lapply Hload -Hload cases ty
1160     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1161     | #structname #fieldspec | #unionname #fieldspec | #id ]
1162     [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
1163     | 4,5: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq_ptr Heq)
1164            %{(Vptr (mk_pointer b2 (offset_plus off1 delta)))}
1165            @conj
1166            [ 1,3: @refl
1167            | *: %4 whd in ⊢ (??%?); >eq_block_b_b @refl ] ]
1168     (* Now: load-by-value cases. Outcome is either None or Undef. *)
1169     lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 Halloc)
1170     #Hload_eq
1171     [ lapply (Hload_eq (Tint sz sg) (refl ??) off1)
1172     | lapply (Hload_eq (Tpointer ptr_ty) (refl ??) off1)
1173     | lapply (Hload_eq (Tcomp_ptr id) (refl ??) off1) ]
1174     *
1175     (* None case: absurd *)
1176     [ 2,4,6: #Hload >Hload #Habsurd destruct (Habsurd) ]
1177     #Hload >Hload #Heq destruct (Heq) %{Vundef}
1178     @conj try // destruct (Heq_ptr)
1179     (* prove the validity of this pointer  in order tu unfold load *)
1180     cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true)
1181     [ 1,3,5: @valid_pointer_of_Prop @conj try @conj
1182        [ 1,4,7: assumption
1183        | 2,5,8: >unfold_low_bound
1184           lapply (alloc_properties … Halloc) * *
1185           >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef
1186           lapply (valid_pointer_to_Prop … Hvalid') * *
1187           #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh'
1188           #Hle_low #Hlt_high destruct
1189           cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta)
1190           [ 1,3,5: >Z_addition_bv_commute try @refl
1191                    @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l
1192                    @Hlt_high
1193           ]
1194           #Hsum_split
1195           cut (low (blocks m1' b1) + Zoo delta ≤ Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta)))
1196           [ 1,3,5: >Hsum_split @monotonic_Zle_Zplus_l assumption ]
1197           @(transitive_Zle … Hlow)
1198       | 3,6,9: >unfold_high_bound
1199           lapply (alloc_properties … Halloc) * *
1200           >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef
1201           lapply (valid_pointer_to_Prop … Hvalid') * *
1202           #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh'
1203           #Hle_low #Hlt_high destruct
1204           cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta)
1205           [ 1,3,5: >Z_addition_bv_commute try @refl
1206                    @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l
1207                    @Hlt_high
1208           ]
1209           #Hsum_split
1210           cut (Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta)) < high (blocks m1' b1) + Zoo delta)
1211           [ 1,3,5: >Hsum_split @monotonic_Zlt_Zplus_l assumption ]
1212           #Hlt_aux @(Zlt_to_Zle_to_Zlt … Hlt_aux Hhigh)
1213       ]
1214    ]
1215    -Hno_interference
1216    #Hvalid_ptr2
1217    (* reformulate the goals in an induction friendly way *)       
1218    [ cut (∃bvals. loadn m2
1219                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
1220                       (typesize (typ_of_type (Tint sz sg))) = Some ? bvals ∧
1221                   (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef)))
1222      [ 2: * #bvals * #Hloadn * #Heq destruct (Heq)
1223           whd in match (load_value_of_type ????);
1224           >Hloadn normalize nodelta try @refl
1225           cases bvals in Heq; try //
1226           #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?);
1227           #Heq destruct (Heq) try @refl ]
1228    | cut (∃bvals. loadn m2
1229                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
1230                       (typesize (typ_of_type (Tpointer ptr_ty))) = Some ? bvals ∧
1231                   (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef)))
1232      [ 2: * #bvals * #Hloadn * #Heq destruct (Heq)
1233           whd in match (load_value_of_type ????);
1234           >Hloadn normalize nodelta try @refl
1235           cases bvals in Heq; try //
1236           #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?);
1237           #Heq destruct (Heq) try @refl ]
1238    | cut (∃bvals. loadn m2
1239                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
1240                       (typesize (typ_of_type (Tcomp_ptr id))) = Some ? bvals ∧
1241                   (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef)))
1242      [ 2: * #bvals * #Hloadn * #Heq destruct (Heq)
1243           whd in match (load_value_of_type ????);
1244           >Hloadn normalize nodelta try @refl
1245           cases bvals in Heq; try //
1246           #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?);
1247           #Heq destruct (Heq) try @refl ]
1248    ]
1249    cases (valid_pointer_to_Prop … Hvalid') -Hvalid' * #HA #HB #HC
1250    cases (valid_pointer_to_Prop … Hvalid_ptr2) -Hvalid_ptr2 * #HD
1251    whd in match (offset_plus ??); #HE #HF
1252    cases Himpl1 cases Himpl2 -Himpl1 -Himpl2
1253    >unfold_low_bound >unfold_low_bound >unfold_high_bound >unfold_high_bound
1254    * #HG #HH * #HI #HJ * #HK #HL * #HM #HN
1255    lapply (alloc_properties … Halloc) * * #HO #HP #Hsrc_undef destruct (HO HP)
1256    cases (some_inversion ????? Hload)
1257    #bevals *
1258    #Hloadn #_ lapply Hloadn -Hloadn
1259    whd in match (typesize ?);
1260    [ generalize in match (S (pred_size_intsize sz));
1261    | generalize in match (S (S O));
1262    | generalize in match (S (S O)); ]
1263    #typesize
1264    lapply HE lapply HF lapply HB lapply HC
1265    -HE -HF -HB -HC
1266    lapply bevals
1267    lapply off1
1268    elim typesize
1269    [ 1,3,5:
1270      #off #bevals #HC #HB #HF #HE #_ %{[ ]} @conj try @refl
1271      %1 @refl
1272    | *:
1273      #n #Hind #off #bevals #HC #HB #HF #HE #Hloadn
1274      cases (some_inversion ????? Hloadn) -Hloadn
1275      #bval1 * #Hbeloadv_eq #Hloadn
1276      cases (some_inversion ????? Hloadn) -Hloadn
1277      whd in match (shift_pointer ???);
1278      whd in match (shift_offset ???);
1279      #bevals1 * #Hloadn #Hbevals'
1280      whd in match (loadn ???);
1281      whd in match (beloadv ??);
1282      >(Zlt_to_Zltb_true … HD) normalize nodelta
1283      >(Zle_to_Zleb_true … HE)
1284      >(Zlt_to_Zltb_true … HF) normalize nodelta
1285      lapply (Hundef_zone (Z_of_unsigned_bitvector ? (addition_n offset_size (offv off) (offv delta))) ??)
1286      [ 1,4,7: >Z_addition_bv_commute
1287          [ 2,4,6: @(transitive_Zlt … Hno_overflow)
1288                   @(monotonic_Zlt_Zplus_l) assumption
1289          | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ]
1290          | 2,5,8: >Z_addition_bv_commute
1291             [ 2,4,6: @(transitive_Zlt … Hno_overflow)
1292                      @(monotonic_Zlt_Zplus_l) assumption
1293             | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ]
1294      ]
1295      #Hcontents_undef
1296      cases n in Hind Hloadn;
1297      [ 1,3,5: #_ normalize in match (loadn ???); normalize nodelta #Heq destruct
1298               >Hcontents_undef %{[BVundef]} @conj try @refl %2 @refl ]
1299      #n' #Hind #Hloadn
1300      lapply Hloadn #Hloadn'
1301      cases (some_inversion ????? Hloadn') -Hloadn'
1302      #bval * whd in match (beloadv ??);
1303      >(Zlt_to_Zltb_true … HA) normalize nodelta #Hbeloadv
1304      cases (if_opt_inversion ???? Hbeloadv) -Hbeloadv #Hbounds
1305      cases (andb_inversion … Hbounds) -Hbounds #Hle1 #Hlt1 #Hcontents1 #_
1306      lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ????)
1307      (* lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ???? Hloadn) *)
1308      [ 1,6,11:
1309        @(transitive_Zle ??? HE)
1310        <associative_addition_n
1311        >(commutative_addition_n ? (sign_ext ???) (offv delta))
1312        >associative_addition_n
1313        >(Z_addition_bv_commute ?? (sign_ext ???))
1314        [ 2,4,6: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???));
1315                 >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O
1316                 @(Zle_to_Zlt_to_Zlt … HJ) @Zlt_to_Zle @HF
1317        | 1,3,5: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???));
1318                 >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O @Zsucc_le
1319        ]
1320      | 2,7,12:
1321        @(Zlt_to_Zle_to_Zlt ??? ? Hhigh)
1322        >Z_addition_bv_commute
1323        [ 2,4,6: @(transitive_Zlt … Hno_overflow)
1324                 @(monotonic_Zlt_Zplus_l) @(Zltb_true_to_Zlt … Hlt1)
1325        | 1,3,5: @monotonic_Zlt_Zplus_l @(Zltb_true_to_Zlt … Hlt1) ]
1326      | 3,8,13:
1327        @(Zleb_true_to_Zle … Hle1)
1328      | 4,9,14:
1329        @(Zltb_true_to_Zlt … Hlt1)
1330      ]
1331      -Hind #Hind lapply (Hind Hloadn)
1332      * #bevals2 * #Hloadn2 #Hbe_to_fe
1333      whd in match (shift_pointer ???);
1334      whd in match (shift_offset ???);
1335      cases Hbe_to_fe
1336      [ 1,3,5: #Heq destruct (Heq)
1337        %{(contents (blocks m2 b2)
1338             (Z_of_unsigned_bitvector offset_size
1339              (addition_n offset_size (offv off) (offv delta)))
1340               ::[ ])}
1341        <associative_addition_n
1342        >(commutative_addition_n ? (offv delta))
1343        >associative_addition_n
1344        >Hloadn2 normalize nodelta @conj try @refl %2
1345        >Hcontents_undef @refl
1346      | *: #Hhd_empty
1347        %{(contents (blocks m2 b2)
1348             (Z_of_unsigned_bitvector offset_size
1349              (addition_n offset_size (offv off) (offv delta)))
1350               :: bevals2)}
1351        <associative_addition_n
1352        >(commutative_addition_n ? (offv delta))
1353        >associative_addition_n
1354        >Hloadn2 normalize nodelta @conj try @refl %2
1355        >Hcontents_undef @refl
1356      ]
1357    ]
1358  ]
1359| #b lapply (alloc_valid_new_block … Halloc) @(eq_block_elim … new_block b)
1360  [ #Heq destruct #Ha #Hb @False_ind @(absurd … Ha Hb)
1361  | #Hneq #Hvalid_new #Hnot_valid normalize nodelta
1362    cut (¬valid_block m1 b)
1363    [ cases m1 in Halloc; #cont #next #Hnext
1364      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1365      % #H cases Hnot_valid #H' @H'
1366      whd whd in H; /2 by transitive_Zlt/ ]
1367    @ (mi_freeblock … Hinj) ]
1368| * #blo #off #p' #Hvalid1
1369  @(eq_block_elim … new_block blo)
1370  [ #Heq whd in match (pointer_translation ??);
1371    destruct (Heq) >eq_block_b_b normalize nodelta
1372    lapply (alloc_properties … Halloc) * *
1373    #Hlow_eq #Hhigh_eq #Hundef destruct
1374    cases (valid_pointer_to_Prop … Hvalid1) *
1375    #Hvalid_block1 #Hlow1 #Hhigh1
1376    #Heq destruct (Heq) @valid_pointer_of_Prop
1377    @conj try @conj   
1378    [ @Hvalid
1379    | @(transitive_Zle … Hlow)
1380      >Z_addition_bv_commute
1381      [ @monotonic_Zle_Zplus_l assumption
1382      | @(transitive_Zlt … Hno_overflow)
1383        @monotonic_Zlt_Zplus_l assumption
1384      ]
1385    | @(Zlt_to_Zle_to_Zlt … Hhigh)
1386      >Z_addition_bv_commute
1387      [ @monotonic_Zlt_Zplus_l assumption
1388      | @(transitive_Zlt … Hno_overflow)
1389        @monotonic_Zlt_Zplus_l assumption
1390      ]
1391    ]
1392  | #Hblocks_neq whd in match (pointer_translation ??);
1393    >(neq_block_eq_block_false … Hblocks_neq) normalize nodelta
1394    #Htranslate
1395    lapply (mi_valid_pointers ??? Hinj (mk_pointer blo off) p' ?)
1396    [ @(alloc_valid_pointer_conservation … Halloc … Hvalid1) @sym_neq assumption ]
1397    #H @H
1398    assumption
1399  ]
1400| #b #b' #o'
1401  @(eq_block_elim … new_block b)
1402  [ #Heq destruct (Heq) normalize nodelta
1403    #Heq destruct (Heq) @Hvalid
1404  | #Hneq normalize nodelta
1405    #Hembed
1406    @(mi_nodangling ??? Hinj … Hembed)
1407  ]
1408| #b #b' #o'
1409  @(eq_block_elim … new_block b)
1410  [ #Heq normalize nodelta #Heq' destruct (Heq Heq')
1411    @Hregion
1412  | #Hneq normalize nodelta #Hembed
1413    @(mi_region … Hinj … Hembed)
1414  ]
1415| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
1416  cases (alloc_properties … Halloc) * #Hlow1 #Hhigh1 #Hundef
1417  @(eq_block_elim … new_block b1)
1418  normalize nodelta
1419  [ #Heq #Heq' destruct
1420    >(neq_block_eq_block_false … Hneq) normalize nodelta
1421    #Hembed
1422(*    lapply (alloc_bounds_conservation … Halloc) …  *)
1423    @(eq_block_elim … b1' b2') normalize nodelta
1424    [ #Heq destruct (Heq)
1425      lapply (Hno_interference b2 ? (sym_neq ??? Hneq) Hembed) *
1426      cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq)) #HA #HB
1427      [ #H %1 %1 %2
1428        >HB @H
1429      | #H %1 %1 %1 >HA @H ]
1430    | #Hneq @I ]
1431  | #Hneq' #Hembed
1432    @(eq_block_elim … new_block b2) normalize nodelta
1433    [ #Heq #Heq' destruct
1434      @(eq_block_elim … b1' b2') normalize nodelta
1435      [ #Heq destruct (Heq)
1436        lapply (Hno_interference b1 ? Hneq Hembed) *
1437        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq')) #HA #HB
1438        [ #H %1 %1 %1
1439          >HB @H
1440        | #H %1 %1 %2 >HA @H ]
1441      | #Hneq @I ]
1442    | #Hneq'' #Hembed'
1443      @(eq_block_elim … b1' b2') normalize nodelta
1444      [ #Heq'' destruct (Heq'')
1445        lapply (mi_nonalias … Hinj … Hneq … Hembed Hembed')
1446        >eq_block_b_b normalize nodelta
1447        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq''))
1448        #HA #HB
1449        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq'))
1450        #HC #HD
1451        * [ * [ * | ] | ]
1452        [ #Hle %1 %1 %1 >HD >HA @Hle
1453        | #Hle %1 %1 %2 >HB >HC @Hle
1454        | #Hempty %1 %2 whd in Hempty ⊢ %; >HD >HC
1455          @Hempty
1456        | #Hempty %2 whd in Hempty ⊢ %; >HB >HA @Hempty
1457        ]
1458      | #_ @I
1459      ]
1460    ]
1461  ]
1462| #b whd
1463  @(eq_block_elim … new_block b)
1464  normalize nodelta
1465  #Hneq destruct (Hneq)
1466  [ @conj try @conj try assumption
1467  | lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
1468    cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq))
1469    #HA #HB
1470    cases (E b) normalize nodelta try //
1471    * #blo #off normalize nodelta * * #HA' #HB' #HC'
1472    @conj try @conj whd in HA'; whd in HB';
1473    whd in match (block_implementable_bv ??);
1474    [ 1,2: >HA >HB assumption
1475    | *: >HB assumption ]
1476  ]
1477] qed.   
1478
1479(* And show the compatibility of the new injection. *)
1480
1481lemma alloc_memory_inj_m1_to_m2_compat :
1482  ∀E:embedding.
1483  ∀m1,m2,m1':mem.
1484  ∀z1,z2:Z.
1485  ∀target,new_block.
1486  ∀delta:offset.
1487  alloc m1 z1 z2 = 〈m1', new_block〉 →
1488  memory_inj E m1 m2 →
1489  embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x).
1490#E #m1 #m2 #m1' #z1 #z2 #target #new_block #delta #ALLOC #MI
1491whd
1492#b @eq_block_elim
1493[ #E destruct %1 @(mi_freeblock … MI) /2/
1494| #_ %2 %
1495] qed.
1496
1497
1498(* -------------------------------------- *)
1499(* Lemmas pertaining to [free] *)
1500
1501(* Lemma 46 by Leroy&Blazy *)
1502lemma free_load_sim_ptr_m1 :
1503  ∀E:embedding.
1504  ∀m1,m2,m1'.
1505  load_sim_ptr E m1 m2 →
1506  ∀b. free m1 b = m1' →
1507      load_sim_ptr E m1' m2.     
1508#E #m1 #m2 #m1' #Hinj #b #Hfree
1509whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
1510cases ty
1511[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1512| #structname #fieldspec | #unionname #fieldspec | #id ]
1513[ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1514             normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl
1515             %4 @Htrans ]
1516#Hload <Hfree in Hload; #Hload lapply (load_value_of_type_free_load_value_of_type … Hload)
1517#Hload' @(Hinj … Hload') //
1518<Hfree in Hvalid; @valid_free_to_valid
1519qed.
1520
1521(* lemma 47 of L&B *)
1522
1523lemma free_loadn_sim_ptr_m2 :
1524  ∀sz,m,b,b',o,res.
1525   b ≠ b' →
1526   loadn m (mk_pointer b' o) sz = Some ? res →
1527   loadn (free m b) (mk_pointer b' o) sz = Some ? res.
1528#sz
1529elim sz
1530[ normalize //
1531| #sz' #Hind #m #b #b' #o #res #Hneq whd in ⊢ ((??%?) → (??%?));
1532  #H cases (some_inversion ????? H) -H #beres *
1533  #Hbeloadv #Hloadn
1534  lapply (beloadv_free_beloadv2 m b ??? Hbeloadv)
1535  [ @sym_neq @Hneq ]
1536  #Hbeloadv' >Hbeloadv' normalize nodelta
1537  cases (some_inversion ????? Hloadn) -Hloadn #bevals * #Hloadn
1538  #Heq destruct (Heq)
1539  >(Hind … Hneq Hloadn) normalize nodelta @refl
1540] qed. 
1541
1542lemma free_load_sim_ptr_m2 :
1543  ∀E:embedding.
1544  ∀m1,m2,m2'.
1545  load_sim_ptr E m1 m2 →
1546  ∀b. free m2 b = m2' →
1547      (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
1548      load_sim_ptr E m1 m2'.     
1549#E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped
1550whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
1551cases ty
1552[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1553| #structname #fieldspec | #unionname #fieldspec | #id ]
1554[ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1555             normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl
1556             %4 @Htrans ]
1557lapply Htrans -Htrans lapply Hsim -Hsim lapply Hfree -Hfree
1558cases m2 #contents2 #next2 #Hnext2
1559whd in ⊢ ((??%?) → ?); #Hm2' destruct
1560#Hsim #Htrans
1561cases (some_inversion ????? Htrans) * #b2' #off2' * #Hembed normalize nodelta
1562#Heq destruct (Heq) #Hload
1563lapply (Hsim … Hvalid … Htrans … Hload)
1564* #v2' * #Hload_before_free #Hvalue_eq
1565@(eq_block_elim … b2 b)
1566[ 1,3,5: #Heq destruct
1567         lapply (Hunmapped b1 off2' Hembed) *
1568         [ 1,3,5: #Hnot_valid lapply (valid_pointer_to_Prop … Hvalid)
1569                  -Hvalid whd in match (valid_block ??) in Hnot_valid;
1570                  * * #Hvalid #_ #_ @False_ind
1571                  cases Hnot_valid #H @H @Hvalid
1572         | *: whd in ⊢ (% → ?); #Hempty
1573              lapply (valid_pointer_to_Prop … Hvalid)
1574              -Hvalid * * #_ #Hlow #Hhigh
1575              cut ((low_bound m1 b1 < high_bound m1 b1))
1576              [ 1,3,5: /2 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle_to_Zlt/ ]
1577              #Hnonempty @False_ind -Hlow -Hhigh
1578              lapply (Zlt_to_Zle_to_Zlt … Hnonempty Hempty)
1579              #H cases (irreflexive_Zlt (low_bound m1 b1)) #H' @H' @H ]
1580| *: #Hneq %{v2'} @conj try assumption
1581     whd in match (load_value_of_type ????) in Hload_before_free:(??%?) ⊢ (??%?);
1582     cases (some_inversion ????? Hload_before_free) -Hload_before_free
1583     #bevals * #Hloadn #Heq
1584     >(free_loadn_sim_ptr_m2 … Hloadn) normalize nodelta
1585     try assumption @sym_neq @Hneq
1586] qed.     
1587
1588lemma free_block_is_empty :
1589  ∀m,m',b,b'.
1590  block_region b = block_region b' →
1591  block_is_empty m b →
1592  free m b' = m' →
1593  block_is_empty m' b.
1594* #contents #nextblock #Hpos
1595#m' #b #b' #Hregions_eq
1596#HA #HB normalize in HB; <HB whd
1597normalize >Hregions_eq cases (block_region b') normalize nodelta
1598@(eqZb_elim … (block_id b) (block_id b'))
1599[ 1,3: #Heq normalize nodelta //
1600| 2,4: #Hneq normalize nodelta @HA ]
1601qed.
1602
1603lemma high_bound_freed_block :
1604  ∀m,b. high_bound (free m b) b = OZ.
1605#m #b normalize
1606cases (block_region b) normalize
1607>eqZb_z_z normalize @refl
1608qed.
1609
1610lemma low_bound_freed_block :
1611  ∀m,b. low_bound (free m b) b = (pos one).
1612#m #b normalize
1613cases (block_region b) normalize
1614>eqZb_z_z normalize @refl
1615qed.
1616
1617(* Lemma 49 in Leroy&Blazy *)
1618lemma free_non_aliasing_m1 :
1619  ∀E:embedding.
1620  ∀m1,m2,m1'.
1621  memory_inj E m1 m2 →
1622  ∀b. free m1 b = m1' →
1623      non_aliasing E m1'.
1624(* The proof proceeds by a first case analysis to see wether b lives in the
1625   same world as the non-aliasing blocks (if not : trivial), in this case
1626   we proceed to a second case analysis on the non-aliasing hypothesis in
1627   memory_inj. *)
1628#E #m1 #m2 #m1' #Hinj #b #Hfree
1629whd
1630#b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
1631#Hembed1 #Hembed2
1632@(eq_block_elim … b1' b2') normalize nodelta
1633[ 2: try // ]
1634#Hblocks_eq
1635lapply Hembed2 -Hembed2
1636lapply Hembed1 -Hembed1
1637lapply Hblocks_eq -Hblocks_eq
1638(*cases b1' #r1' #bid1'
1639  cases b2' #r2' #bid2' *)
1640#Heq destruct (Heq)
1641generalize in match b2';
1642#target #Hembed1 #Hembed2
1643lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2)
1644>eq_block_b_b normalize nodelta
1645normalize nodelta <Hfree
1646@(eq_block_elim … b1 b)
1647[ #Heq destruct (Heq) #Hcase
1648  %1 %2 whd
1649  >high_bound_freed_block >low_bound_freed_block
1650  //
1651| #Hneq1 @(eq_block_elim … b2 b)
1652  [ #Heq destruct (Heq) #Hcase
1653    %2 whd
1654    >high_bound_freed_block >low_bound_freed_block
1655    // ] ]
1656#Hneq2
1657>unfold_high_bound >unfold_high_bound >unfold_high_bound >unfold_high_bound
1658>unfold_low_bound >unfold_low_bound >unfold_low_bound >unfold_low_bound
1659<(high_free_eq … Hneq1) <(high_free_eq … Hneq2)
1660<(low_free_eq … Hneq1) <(low_free_eq … Hneq2)
1661*
1662[ 2: #H %2 whd >unfold_high_bound >unfold_low_bound
1663     <(low_free_eq … Hneq2) <(high_free_eq … Hneq2) @H ]
1664*
1665[ 2: #H %1%2 whd >unfold_high_bound >unfold_low_bound
1666     <(low_free_eq … Hneq1) <(high_free_eq … Hneq1) @H ]
1667* #H
1668[ %1 %1 %1 @H
1669| %1 %1 %2 @H ]
1670qed.
1671
1672(* Extending lemma 46 and 49 to memory injections *)
1673lemma free_memory_inj_m1 :
1674  ∀E:embedding.
1675  ∀m1,m2,m1'.
1676  memory_inj E m1 m2 →
1677  ∀b. free m1 b = m1' →
1678      memory_inj E m1' m2.
1679#E #m1 #m2 #m1' #Hinj #b #Hfree
1680cases Hinj
1681#Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable
1682% try assumption
1683[ @(free_load_sim_ptr_m1 … Hload_sim … Hfree)
1684| #bb #Hnot_valid lapply (Hfreeblock bb) #HA @HA % #HB
1685  cases Hnot_valid #HC @HC <Hfree @HB
1686| #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation)
1687  <Hfree in Hvalid_m1'; @valid_free_to_valid
1688| @(free_non_aliasing_m1 … Hinj … Hfree)
1689| #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?);
1690  cases (E bb) normalize nodelta try //
1691  * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj
1692  try //
1693  @(eq_block_elim … b bb)
1694  [ 2,4:
1695      #Hneq destruct (Hfree)
1696      whd in match (free ??);
1697      whd >unfold_low_bound >unfold_high_bound
1698      whd in match (update_block ?????); >(not_eq_block … (sym_neq ??? Hneq))
1699      try @conj normalize nodelta cases HA try //
1700  | 1,3:
1701      #H destruct whd in match (free ??);
1702      whd [ >unfold_low_bound ] >unfold_high_bound
1703      whd in match (update_block ?????); >eq_block_b_b
1704      normalize nodelta try @conj try // % try //
1705  ]
1706] qed.
1707
1708(* Lifting lemma 47 to memory injs - note that we require a much stronger condition
1709 * on the freed block : no block of m1 can map to it. Not even an invalid block or
1710 * an empty one.
1711 * XXX this lemma is not given in Leroy&Blazy, and unless future developments requires
1712 * it I will comment it out. XXX *)
1713lemma free_memory_inj_m2 :
1714  ∀E:embedding.
1715  ∀m1,m2,m2'.
1716  memory_inj E m1 m2 →
1717  ∀b. free m2 b = m2' →
1718      (∀b1,delta. E b1 = Some ? 〈b, delta〉 →
1719      (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 
1720      memory_inj E m1 m2'.
1721#E #m1 #m2 #m2' #Hinj #b #Hfree #b_not_mapped
1722% cases Hinj try //
1723#Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl
1724[ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed
1725  @(b_not_mapped … b1 delta Hembed)
1726| @Hfreeblock
1727| * #bp #op #p' #Hp_valid #Hptr_trans
1728  @(eq_block_elim … (pblock p') b)
1729  [ #Heq lapply (Hvalid … Hp_valid Hptr_trans) #Hp_valid' destruct (Heq)
1730    cases (some_inversion ????? Hptr_trans)
1731    * #bp' #op' * #Hembed normalize nodelta #Heq destruct (Heq)
1732    cases (b_not_mapped … Hembed)
1733    [ #Hnot_valid lapply (Hfreeblock … Hnot_valid) >Hembed #Habsurd destruct (Habsurd)
1734    | #Hempty @False_ind lapply (valid_pointer_to_Prop … Hp_valid) * * #_
1735      whd in Hempty; #Hle #Hlt
1736      lapply (Zlt_to_Zle_to_Zlt … Hlt Hempty) #Hlt2
1737      lapply (Zlt_to_Zle_to_Zlt … Hlt2 Hle) #Hlt3
1738      @(absurd … Hlt3 (irreflexive_Zlt ?)) ]
1739  | #Hneq lapply (Hvalid … Hp_valid Hptr_trans) <Hfree #HA
1740    @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … HA) -HA * *
1741    #HA #HB #HC @conj try @conj try assumption
1742    [ >unfold_low_bound <(low_free_eq m2 ?? Hneq) @HB
1743    | >unfold_high_bound <(high_free_eq m2 ?? Hneq) @HC ]
1744  ]
1745| #bb #b' #o' #Hembed
1746  lapply (Hnodangling … Hembed) <Hfree //
1747| @Hregion
1748| #bb lapply (Himpl bb)
1749  whd in ⊢ (% → %); cases (E bb) normalize nodelta try //
1750  * #BLO #OFF normalize nodelta * * destruct (Hfree)
1751  #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption
1752  cases Hbb try // #Hlow_bb #Hhigh_bb
1753  [ >unfold_low_bound
1754  | *: >unfold_high_bound ]
1755  whd in match (update_block ?????);
1756  @(eq_block_elim … BLO b)
1757  #H [ 1,3,5: destruct (H) normalize nodelta try //
1758               @conj try //
1759     | *: normalize nodelta cases HBLO try // ]
1760] qed.
1761
1762
1763(* Lemma 64 of L&B on [freelist] *)
1764lemma freelist_memory_inj_m1_m2 :
1765  ∀E:embedding.
1766  ∀m1,m2,m1',m2'.
1767  memory_inj E m1 m2 →
1768  ∀blocklist,b2.
1769  (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
1770  free m2 b2 = m2' →
1771  free_list m1 blocklist = m1' →
1772  memory_inj E m1' m2'.
1773#E #m1 #m2 #m1' #m2' #Hinj #blocklist #b2 #Hnot_mapped #Hfree2 #Hfree_list
1774cut (memory_inj E m1' m2)
1775[ <Hfree_list -Hfree_list
1776  -Hnot_mapped
1777  lapply Hinj -Hinj
1778  lapply m1 -m1
1779  elim blocklist
1780  [ #m1 #Hinj @Hinj
1781  | #hd #tl #Hind #m1 #Hinj
1782    @(free_memory_inj_m1 ? (free_list m1 tl) ? (free (free_list m1 tl) hd) ? hd)
1783    try @refl @(Hind … Hinj)
1784  ]
1785]
1786#Hinj'
1787@(free_memory_inj_m2 … Hinj' … Hfree2)
1788#b1 #delta #Hembed %2
1789lapply (Hnot_mapped … Hembed)
1790lapply Hfree_list -Hfree_list
1791generalize in match m1';
1792generalize in match m1;
1793elim blocklist
1794[ #m1 #m1' whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @False_ind
1795| #hd #tl #Hind #m1 #m1' #Hfree_list *
1796  [ #Heq destruct whd
1797    whd in match (free_list ??);
1798    >unfold_high_bound >unfold_low_bound
1799    whd in match (update_block ?????); >eq_block_b_b
1800    normalize nodelta @I
1801  | >free_list_cons in Hfree_list; #Hfree_list #H
1802    <Hfree_list whd cases m1 #contents2 #n2 #Hn2
1803    >unfold_high_bound >unfold_low_bound
1804    whd in match (update_block ?????);
1805    @(eq_block_elim … b1 hd)
1806    [ #Heq normalize nodelta @I
1807    | #Hneq normalize nodelta @(Hind … (mk_mem contents2 n2 Hn2) … (refl ??) … H)
1808    ]
1809  ]
1810] qed.
1811
1812(* ---------------------------------------------------------- *)
1813(* Lemma 40 of the paper of Leroy & Blazy on the memory model
1814 * and store-related lemmas *)
1815
1816lemma bestorev_beloadv_conservation :
1817  ∀mA,mB,wb,wo,v.
1818    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1819    ∀rb,ro. eq_block wb rb = false →
1820    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
1821#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
1822whd in ⊢ (??%%);
1823elim mB in Hstore; #contentsB #nextblockB #HnextblockB
1824normalize in ⊢ (% → ?);
1825cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
1826[ 2: #Habsurd destruct (Habsurd) ]
1827cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo))
1828       then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) 
1829       else false) normalize nodelta
1830[ 2: #Habsurd destruct (Habsurd) ]
1831#Heq destruct (Heq)
1832cases (Zltb (block_id rb) (nextblock mA)) normalize nodelta try //
1833cut (eqZb (block_id rb) (block_id wb) = false)
1834[ >eqZb_symmetric @Hblock_neq ]
1835#Heqzb >Heqzb normalize nodelta @refl
1836qed.
1837
1838(* lift [bestorev_beloadv_conservation to [loadn] *)
1839lemma bestorev_loadn_conservation :
1840  ∀mA,mB,n,wb,wo,v.
1841    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1842    ∀rb,ro. eq_block wb rb = false →
1843    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
1844#mA #mB #n
1845elim n
1846[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
1847| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
1848     whd in ⊢ (??%%);
1849     >(bestorev_beloadv_conservation … Hstore … Hneq)
1850     >(Hind … Hstore … Hneq) @refl
1851] qed.
1852
1853(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
1854lemma bestorev_load_value_of_type_conservation :
1855  ∀mA,mB,wb,wo,v.
1856    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1857    ∀rb,ro. eq_block wb rb = false →
1858    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1859#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
1860cases ty
1861[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1862| #structname #fieldspec | #unionname #fieldspec | #id ]
1863//
1864[ 1: elim sz ]
1865whd in ⊢ (??%%);
1866>(bestorev_loadn_conservation … Hstore … Hneq) @refl
1867qed.
1868
1869(* lift [bestorev_load_value_of_type_conservation] to storen *)
1870lemma storen_load_value_of_type_conservation :
1871  ∀l,mA,mB,wb,wo.
1872    storen mA (mk_pointer wb wo) l = Some ? mB →
1873    ∀rb,ro. eq_block wb rb = false →
1874    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1875#l elim l
1876[ 1: #mA #mB #wb #wo normalize #Heq destruct //
1877| 2: #hd #tl #Hind #mA #mB #wb #wo #Hstoren
1878     cases (some_inversion ????? Hstoren) #mA' * #Hbestorev #Hstoren'
1879     whd in match (shift_pointer ???) in Hstoren':(??%?); #rb #ro #Hneq_block #ty
1880     lapply (Hind ???? Hstoren' … ro … Hneq_block ty) #Heq1
1881     lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2
1882     //
1883] qed.
1884
1885lemma store_value_of_type_load_value_of_type_conservation :
1886  ∀ty,mA,mB,wb,wo,v.
1887    store_value_of_type ty mA wb wo v = Some ? mB →
1888    ∀rb,ro. eq_block wb rb = false →
1889    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1890#ty #mA #mB #wb #wo #v #Hstore #rb #ro #Heq_block
1891cases ty in Hstore;
1892[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1893| #structname #fieldspec | #unionname #fieldspec | #id ]
1894[ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct ]
1895whd in ⊢ ((??%?) → ?); #Hstoren
1896@(storen_load_value_of_type_conservation … Hstoren … Heq_block)
1897qed.
1898
1899definition typesize' ≝ λty. typesize (typ_of_type ty).
1900
1901lemma storen_load_value_of_type_conservation_in_block_high :
1902  ∀E,mA,mB,mC,wo,l.
1903    memory_inj E mA mB →
1904    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
1905    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
1906    high_bound mA b1 + Zoo delta < Zoo wo →
1907    ∀ty,off.
1908       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
1909       low_bound … mA b1 ≤ Zoo off →
1910       Zoo off < high_bound … mA b1 →
1911       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
1912       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
1913#E #mA #mB #mC #wo #data #Hinj #blo #Hstoren #b1 #delta #Hembed #Hhigh #ty
1914(* need some stuff asserting that if a ptr is valid at the start of a write it's valid at the end. *)
1915cases data in Hstoren;
1916[ 1: normalize in ⊢ (% → ?); #Heq destruct //
1917| 2: #xd #data ]
1918#Hstoren
1919cases ty
1920[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1921| #structname #fieldspec | #unionname #fieldspec | #id ]#off #Hofflt #Hlow_load #Hhigh_load try @refl
1922whd in match (load_value_of_type ????) in ⊢ (??%%);
1923[ 1: lapply (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hbefore #Hafter
1924     lapply Hofflt -Hofflt lapply Hlow_load -Hlow_load lapply Hhigh_load -Hhigh_load
1925     lapply off -off whd in match typesize'; normalize nodelta     
1926     generalize in match (typesize ?); #n elim n try //
1927     #n' #Hind #o #Hhigh_load #Hlow_load #Hlt
1928     whd in match (loadn ???) in ⊢ (??%%);
1929     whd in match (beloadv ??) in ⊢ (??%%);
1930     cases (valid_pointer_to_Prop … Hbefore) * #HltB_store #HlowB_store #HhighB_store
1931     cases (valid_pointer_to_Prop … Hafter) * #HltC_store #HlowC_store #HhighC_store
1932     >(Zlt_to_Zltb_true … HltB_store) >(Zlt_to_Zltb_true … HltC_store) normalize nodelta
1933     cut (Zleb (low (blocks mB blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
1934     [ 1: (* Notice that:
1935                low mA b1 ≤ o < high mA b1
1936             hence, since E b1 = 〈blo, delta〉 with delta >= 0
1937                low mB blo ≤ (low mA b1 + delta) ≤ o+delta < (high mA b1 + delta) ≤ high mB blo *)
1938          @cthulhu ]
1939     #HA >HA >andb_lsimpl_true -HA
1940     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mB blo)) = true)
1941     [ 1: (* Same argument as above *) @cthulhu ]
1942     #HA >HA normalize nodelta -HA
1943     cut (Zleb (low (blocks mC blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
1944     [ 1: (* Notice that storen does not modify the bounds of a block. Related lemma present in [MemProperties].
1945             This cut follows from this lemma (which needs some info on the size of the data written, which we
1946             have but must make explicit) and from the first cut. *)
1947          @cthulhu ]         
1948     #HA >HA >andb_lsimpl_true -HA
1949     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mC blo)) = true)
1950     [ 1: (* Same argument as above *) @cthulhu ]
1951     #HA >HA normalize nodelta -HA
1952     normalize in match (bitvector_of_nat ??); whd in match (shift_pointer ???);
1953     whd in match (shift_offset ???); >commutative_addition_n >associative_addition_n
1954     lapply (Hind (mk_offset (addition_n offset_size (sign_ext 2 ? [[false; true]]) (offv o))) ???)
1955     [ 1: (* Provable from Hlt *) @cthulhu
1956     | 2: (* Provable from Hlow_load, need to make a "succ" commute from bitvector to Z *) @cthulhu
1957     | 3: (* Provable from Hlt, again *) @cthulhu ]
1958     cases (loadn mB (mk_pointer blo
1959              (mk_offset (addition_n ? (addition_n ?
1960                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
1961     normalize nodelta                 
1962     cases (loadn mC (mk_pointer blo
1963              (mk_offset (addition_n ? (addition_n ?
1964                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
1965     normalize nodelta try //
1966     [ 1,2: #l #Habsurd destruct ]
1967     #l1 #l2 #Heq
1968     cut (contents (blocks mB blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) =
1969          contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
1970     [ 1: (* Follows from Hhigh, indirectly *) @cthulhu ]
1971     #Hcontents_eq >Hcontents_eq whd in match (be_to_fe_value ??) in ⊢ (??%%);
1972     cases (contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
1973     normalize nodelta try //
1974     (* Ok this is going to be more painful than what I thought. *)
1975     @cthulhu
1976| *: @cthulhu
1977] qed.
1978
1979lemma storen_load_value_of_type_conservation_in_block_low :
1980  ∀E,mA,mB,mC,wo,l.
1981    memory_inj E mA mB →
1982    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
1983    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
1984    Zoo wo < low_bound mA b1 + Zoo delta →
1985    ∀ty,off.
1986       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
1987       low_bound … mA b1 ≤ Zoo off →
1988       Zoo off < high_bound … mA b1 →
1989       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
1990       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
1991@cthulhu
1992qed.
1993
1994(* Writing in the "extended" part of a memory preserves the underlying injection. *)
1995lemma bestorev_memory_inj_to_load_sim :
1996  ∀E,mA,mB,mC.
1997  ∀Hext:memory_inj E mA mB.
1998  ∀block2. ∀i : offset. ∀ty : type.
1999  (∀block1,delta.
2000    E block1 = Some ? 〈block2, delta〉 →
2001    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
2002  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
2003  load_sim_ptr E mA mC.
2004#E #mA #mB #mC #Hinj #block2 #i #storety
2005cases storety
2006[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2007| #structname #fieldspec | #unionname #fieldspec | #id ] #Hout #storeval #Hstore whd
2008#b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value
2009whd in Hstore:(??%?);
2010[  1,5,6,7,8: destruct ]
2011[ 1:
2012lapply (mi_inj … Hinj … Hvalid … Hptr_trans … Hload_value)
2013lapply Hload_value -Hload_value
2014cases ty
2015[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2016| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2017#Hload_value
2018(* Prove that the contents of mB where v1 was were untouched. *)
2019* #readval' * #Hload_value2 #Hvalue_eq %{readval'} @conj try assumption
2020cases (some_inversion ????? Hptr_trans) * #b2' #delta' * #Hembed -Hptr_trans normalize nodelta
2021#Heq destruct (Heq)
2022@(eq_block_elim  … b2 block2)
2023[ 2,4,6,8: #Hblocks_neq <Hload_value2 @sym_eq @(storen_load_value_of_type_conservation … Hstore)
2024           @not_eq_block @sym_neq @Hblocks_neq
2025| 1,3,5,7: #Heq destruct (Heq) lapply (Hout … Hembed) *
2026           [ 1,3,5,7: #Hhigh <Hload_value2 -Hload_value2 @sym_eq
2027                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
2028                      * * #Hlt #Hlowb_off1 #Hhighb_off1
2029                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
2030                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
2031                      @(storen_load_value_of_type_conservation_in_block_high … Hinj … Hstore … Hembed)
2032                      try //
2033                      (* remaining stuff provable from Hload_value  *)
2034                      @cthulhu
2035           | 2,4,6,8: #Hlow <Hload_value2 -Hload_value2 @sym_eq
2036                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
2037                      * * #Hlt #Hlowb_off1 #Hhighb_off1
2038                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
2039                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
2040                      @(storen_load_value_of_type_conservation_in_block_low … Hinj … Hstore … Hembed)
2041                      try //
2042                      [ 1,3,5,7: (* deductible from Hlow + (sizeof ?) > 0 *) @cthulhu
2043                      | 2,4,6,8: (* deductible from Hload_value *) @cthulhu ]
2044           ]
2045]
2046| *: (* exactly the same proof as above  *) @cthulhu ]
2047qed.
2048
2049(* Lift the above result to memory_inj
2050 * This is Lemma 40 of Leroy & Blazy *)
2051lemma store_value_of_type_memory_inj_to_memory_inj :
2052  ∀E,mA,mB,mC.
2053  ∀Hext:memory_inj E mA mB.
2054  ∀block2. ∀i : offset. ∀ty : type.
2055  (∀block1,delta.
2056    E block1 = Some ? 〈block2, delta〉 →
2057    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
2058  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
2059  memory_inj E mA mC.
2060#E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore %
2061lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try //
2062cases Hinj #Hsim' #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption
2063[
2064  #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
2065  cases ty in Hstore;
2066  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2067  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2068  whd in ⊢ ((??%?) → ?);
2069  [ 1,4,5,6,7: #Habsurd destruct ]
2070  cases (fe_to_be_values ??)
2071  [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl
2072  | *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_
2073       @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh
2074       @conj try @conj try assumption >Hnext try //
2075       cases (Hbounds (pblock p')) #HA #HB
2076       whd in match (low_bound ??); whd in match (high_bound ??);
2077       >HA >HB try assumption
2078  ]
2079| lapply (mem_bounds_after_store_value_of_type … Hstore)
2080  * #Hnext_eq #Hb
2081  #b #b' #o' cases (Hb b') #Hlow_eq #Hhigh_eq #Hembed
2082  lapply (mi_nodangling … Hinj … Hembed)
2083  whd in match (valid_block ??) in ⊢ (% → %);
2084  >(Hnext_eq) try //
2085| #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %);
2086  cases (E b) try //
2087  * #BLO #OFF normalize nodelta * *
2088  #Hb #HBLO #Hbound try @conj try @conj try assumption
2089  lapply (mem_bounds_after_store_value_of_type … Hstore) *
2090  #_ #Hbounds
2091  cases (Hbounds BLO) #Hlow #Hhigh whd %
2092  [ >unfold_low_bound | >unfold_high_bound ]
2093  >Hlow >Hhigh cases HBLO try //
2094] qed.
2095
2096
2097(* ---------------------------------------------------------- *)
2098(* Lemma 41 of the paper of Leroy & Blazy on the memory model
2099 * and related lemmas *)
2100
2101(* The back-end might contain something similar to this lemma. *)
2102lemma be_to_fe_value_ptr :
2103  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
2104#b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid normalize nodelta
2105(*cases br normalize nodelta *) >eqZb_z_z normalize nodelta
2106cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
2107<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
2108* //
2109qed.
2110
2111lemma fe_to_be_values_length :
2112  ∀E,v1,v2,ty.
2113  value_eq E v1 v2 → |fe_to_be_values ty v1| = |fe_to_be_values ty v2|.
2114#E #v1 #v2 #ty #Hvalue_eq
2115@(value_eq_inversion … Hvalue_eq) //
2116qed.
2117
2118lemma value_eq_to_be_and_back_again :
2119  ∀E,ty,v1,v2.
2120  value_eq E v1 v2 →
2121  ast_typ_consistent_with_value ty v1 →
2122  value_eq E (be_to_fe_value ty (fe_to_be_values ty v1 )) (be_to_fe_value ty (fe_to_be_values ty v2)).
2123#E #ty #v1 #v2 #Hvalue_eq
2124@(value_eq_inversion … Hvalue_eq) try //
2125[ 1: cases ty //
2126| 2: #sz #i cases ty
2127     [ 2: @False_ind
2128     | 1: #sz' #sg #H lapply H whd in ⊢ (% → ?); #Heq
2129          lapply (fe_to_be_to_fe_value_int … H) #H >H // ]
2130| 3: #p1 #p2 #Hembed cases ty
2131     [ 1: #sz #sg @False_ind
2132     | 2: #_
2133          cases p1 in Hembed; #b1 #o1
2134          cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H
2135          cases (some_inversion ????? H) * #b3 #o3 * #Hembed
2136          normalize nodelta #Heq >be_to_fe_value_ptr >be_to_fe_value_ptr
2137          destruct %4 whd in match (pointer_translation ??);
2138          >Hembed normalize nodelta @refl
2139     ]
2140] qed.
2141
2142(* ------------------------------------------------------------ *)
2143(* Lemma ?? of the paper of Leroy & Blazy on the memory model ? *)
2144
2145lemma storen_parallel_memory_exists :
2146  ∀E,m1,m2.
2147  memory_inj E m1 m2 →
2148  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
2149  ∀v1,v2. value_eq E v1 v2 →
2150  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
2151  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'.
2152(*        ∧ loadn m2' (mk_pointer b2 (offset_plus i delta)) (|fe_to_be_values ty v2|) = Some ? (fe_to_be_values ty v2).*)
2153#E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty
2154lapply (mi_valid_pointers … Hinj)
2155generalize in match m2;
2156generalize in match m1;
2157generalize in match i;
2158lapply (fe_to_be_values_length … ty Hvalue_eq)
2159generalize in match (fe_to_be_values ty v2);
2160generalize in match (fe_to_be_values ty v1);
2161#l1 elim l1
2162[ 1: #l2 #Hl2
2163     cut (l2 = [])
2164     [ cases l2 in Hl2; // #hd' #tl' normalize #Habsurd destruct ]
2165     #Hl2_empty >Hl2_empty #o #m1 #m2 #_ normalize /2 by ex_intro/
2166| 2: #hd1 #tl1 #Hind #l2 #Hlength
2167     cut (∃hd2,tl2.l2 = hd2::tl2 ∧ |tl1| = |tl2|)
2168     [ cases l2 in Hlength;
2169       [ normalize #Habsurd destruct
2170       | #hd2 #tl2 normalize #H %{hd2} %{tl2} @conj try @refl destruct (H) assumption ] ]
2171     * #hd2 * #tl2 * #Heq2 destruct (Heq2) #Hlen_tl
2172     #o #m1 #m2 #Hvalid_embed #Hstoren
2173     cases (some_inversion ????? Hstoren) #m1_tmp * #Hbestorev #Hstoren_tl
2174     lapply (Hvalid_embed (mk_pointer b1 o) (mk_pointer b2 (offset_plus o delta)) ??)
2175     [ 1: whd in match (pointer_translation ??);
2176          >Hembed normalize nodelta @refl
2177     | 2: @(bestorev_to_valid_pointer … Hbestorev) ]
2178     #Hvalid_ptr_m2
2179     whd in match (storen ???);
2180     lapply (valid_pointer_to_bestorev_ok m2 (mk_pointer b2 (offset_plus o delta)) hd2 Hvalid_ptr_m2)
2181     * #m2_tmp #Hbestorev2 >Hbestorev2 normalize nodelta
2182     whd in match (shift_pointer ???) in Hstoren_tl ⊢ %;
2183     whd in match (shift_offset ???) in Hstoren_tl ⊢ %;
2184     (*     normalize in match (sign_ext ???) in Hstoren_tl ⊢ %;*)
2185     cut (mk_offset (addition_n ? (offv (offset_plus o delta)) (sign_ext 2 offset_size (bitvector_of_nat 2 1))) =
2186          offset_plus (offset_plus o (mk_offset (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) delta)
2187     [ cases o #o' normalize nodelta whd in match (offset_plus ??) in ⊢ (??%%);
2188       whd in match (offset_plus ??) in ⊢ (???(?%));
2189      /2 by associative_addition_n, commutative_addition_n, refl/ ]
2190     #Heq_cleanup >Heq_cleanup >Heq_cleanup in Hind; #Hind @(Hind … Hstoren_tl)
2191     try assumption
2192     #p #p' #Hvalid_in_m1_tmp #Hp_embed @valid_pointer_of_Prop
2193     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * *
2194     #Hnextblock_eq #Hbounds_eq #Hoffset_in_bounds #Hcontents_at_eq #Hcontents_else_eq
2195     lapply (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * *
2196     #Hnextblock_eq2 #Hbounds_eq2 #Hoffset_in_bounds2 #Hcontents_at_eq2 #Hcontents_else_eq2
2197     cut (valid_pointer m1 p = true)
2198     [ @valid_pointer_of_Prop
2199       cases (valid_pointer_to_Prop … Hvalid_in_m1_tmp)
2200       >Hnextblock_eq cases (Hbounds_eq (pblock p)) #Hlow' #Hhigh'
2201       whd in match (low_bound ??); whd in match (high_bound ??);
2202       >Hlow' >Hhigh' * /3 by conj/ ]
2203     #Hvalid_in_m1
2204     lapply (Hvalid_embed p p' Hvalid_in_m1 Hp_embed) #Hvalid_in_m2     
2205     cases (valid_pointer_to_Prop … Hvalid_in_m2) * #Hnextblock2' #Hlow2' #Hhigh2'
2206     @conj try @conj
2207     >Hnextblock_eq2 try assumption
2208     cases (Hbounds_eq2 … (pblock p')) #Hlow2'' #Hhigh2''
2209     whd in match (low_bound ??);
2210     whd in match (high_bound ??);
2211      >Hlow2'' >Hhigh2'' assumption
2212] qed.     
2213
2214lemma storen_parallel_memory_exists_and_preserves_loads :
2215  ∀E,m1,m2.
2216  memory_inj E m1 m2 →
2217  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
2218  ∀v1,v2. value_eq E v1 v2 →
2219  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
2220  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
2221        loadn m2' (mk_pointer b2 (offset_plus i delta)) (|fe_to_be_values ty v2|) = Some ? (fe_to_be_values ty v2).
2222#E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty #Hstoren
2223cases (storen_parallel_memory_exists … Hinj … Hembed … Hvalue_eq i m1' ty Hstoren)
2224#m2' #Hstoren' %{m2'} @conj try assumption
2225@(storen_loadn_ok … Hstoren')
2226//
2227qed.
2228
2229(* If E ⊢ m1 ↦ m2
2230   *and* if E b1 = 〈b2,delta〉,
2231   *and* if we write /A PROPER VALUE/ at 〈b1,i〉 successfuly,
2232   *then* we can write /something value_eq-compatible/ in m2 at 〈b2,i+delta〉 successfuly yielding m2'
2233          *and* preserve the injection : E ⊢ m1' ↦ m2'         
2234   N.B.: this result cannot be given at the back-end level : we could overwrite a pointer
2235         and break the value_eq correspondence between the memories. *)       
2236axiom storen_parallel_aux :
2237  ∀E,m1,m2.
2238  ∀Hinj:memory_inj E m1 m2.
2239  ∀v1,v2. value_eq E v1 v2 →
2240  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
2241  ∀ty,i,m1'.
2242  (* ast_typ_consistent_with_value ty v1 → *)
2243  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
2244  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
2245        memory_inj E m1' m2'.
2246(* This lemma is not provable as in CompCert. In the following chunk of text, I'll try to
2247 * explain why, and how we might still be able to prove it given enough time.
2248   I'll be refering to a paper by Leroy & Blazy in the J.A.R.
2249   In CompCert, when storing some data of size S in some location 〈block, offset〉,
2250   what happens is that
2251   1) the memory is extended with a map from 〈block,offset〉 to the actual data
2252   2) the memory inteval from 〈block,offset+1〉 to 〈block,offset+S-1〉 is invalidated,
2253      meaning that every load in this interval will fail.
2254   This behaviour is documented at page 9 in the aforementioned paper.
2255   The memory model of Cerco is in a sense much more realistic. When storing a front-end
2256   value fv, the story is the following :
2257   1) the value fv is marshalled into a list of back-end values (byte-sized) which correspond
2258      to the actual size of the data in-memory. 2) This list is then stored as-is at the
2259      location 〈block, offset〉.
2260     
2261   Now on to the lemma we want to prove. The difficult part is to prove [load_sim E m1' m2'],
2262   i.e. we want to prove that ∀c1,off1,c2,off2,delta. s.t. E c1 = 〈c2, off2〉
2263     load_value_of_type m1' c1 off1 = ⌊vA⌋ →
2264     load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋ ∧
2265     value_eq E vA vB,
2266   where m1' and m2' are the result of storing some values v1 and v2 in resp. m1 and m2
2267   at some resp. locations 〈b1,i〉 and (pointer_translation E b1 i) (cf statement).
2268
2269   In CompCert, the proof of this statement goes by case analysis on 〈c1,off1〉.
2270   Case 1: 〈b1,i〉 = 〈c1,off1〉 → we read the freshly stored data.
2271   Case 2: b1 = c1 but [i; i+|v1|] and [c1, c1+|vA|] describe /disjoint/ areas of the
2272           same block. In this case, we can use the lemma store_value_load_disjoint
2273           on the hypothesis (load_value_of_type m1' c1 off1 = ⌊vA⌋)
2274           yielding (load_value_of_type m1' c1 off1 = load_value_of_type m1 c1 off1)
2275           allowing us to use the load_sim hypothesis on (m1, m2) to obtain
2276           (load_value_of_type m2 c2 (off1+off2) = ⌊vB⌋)
2277           which we can lift back to
2278           (load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋)
2279           using the disjointness hypothesis contained in the original memory injection [Hinj].
2280   case 4: b1 ≠ c1, nothing difficult
2281   case 3: the intervals  [i; i+|v1|] and [c1, c1+|vA|] /overalap/ !
2282           in CompCert, the prof follows simply from the fact that the load
2283           (load_value_of_type m1' c1 off1) will fail because of invalidated memory,
2284           yielding a contradiction. We have no such possibility in Cerco.
2285   
2286   I see a possible, convoluted way out of this problem. In the case of an overlap, we
2287   need to proceed to an inversion on load_value_of_type m1' c1 off1 = ⌊vA⌋ and to
2288   actually look at the data beeing written. If we succeeded in proceeding to this load,
2289   this means that the back-end values stored are "consistent".
2290   Besides, we need to proceed to a case analysis on what we stored beforehand.
2291   A) If we stored an integer
2292    . of size 8: this means that the overlap actually includes all of the freshly stored
2293      area. This area contains one [BVByte]. If we succeeded in performing an overlapping load,
2294      we either overlapped from the beginning, from the end or from both ends of the stored
2295      area. In all cases, since this area contains a BVByte, all other offsets MUST contain
2296      BVBytes, otherwise we would have a contradiction ... (cumbersome to show but possible)
2297      Hence, we can splice the load in 2 or 3 sub-loads :
2298       . re-use the Case 2 above (disjoint areas) for the parts of the load that are before
2299         and after the stored area
2300       . re-use the Case 1 above for the stored area
2301      and show the whole successful load
2302    . of size 16,32: we have more freedom but only a finite number of overlap possibilities
2303      in each case. We can enumerate them and proceed along the same lines as in the 8 bit
2304      case.
2305   B) If we stored a pointer (of size 2 bytes, necessarily)
2306    . the bytes of a pointer are stored in order and (/!\ important /!\) are /numbered/.
2307    This means that any successful overlapping load has managed to read a pointer in
2308    the wrong order, which yields a contradiction.
2309   C) If we stored a Vnull, roughly the same reasoning as in the pointer case
2310   D) If we stored a Vundef ... This gets hairy. We must reason on the way fe_to_be_values
2311      and be_to_fe_value works. What we want is to show that the load
2312      [load_value_of_a type m1' c1 off1] yields a Vundef. This can happen in several ways.
2313      . If we try to load something of integer type, we will have a Vundef because
2314        we can show that some of the back-end values are BVundef (cf [build_integer])
2315      . If we try to load a pointer, it will also fail for the same reason.
2316  I'll admit that I'm not too sure about the last case. Also, my reasoning on pointers might
2317  fail if we have "longer that 2 bytes" pointers.
2318 
2319  This was a high-level and sketchy proof, and in the interests of time I decide to axiomatize
2320  it.
2321*)
2322
2323(* This is lemma 60 from Leroy&Blazy *)
2324lemma store_value_of_type_parallel :
2325  ∀E,m1,m2.
2326  ∀Hinj:memory_inj E m1 m2.
2327  ∀v1,v2. value_eq E v1 v2 →
2328  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
2329  ∀ty,i,m1'.
2330  (* type_consistent_with_value ty v1 → *)
2331  store_value_of_type ty m1 b1 i v1 = Some ? m1' →
2332  ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧
2333        memory_inj E m1' m2'.
2334#E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1'
2335cases ty
2336[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2337| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2338whd in ⊢ ((??%?) → ?);
2339[ 1,4,5,6,7: #Habsurd destruct ]
2340whd in match (store_value_of_type ?????);
2341@(storen_parallel_aux … Hinj … Hembed) //
2342qed.
2343
2344lemma store_value_of_type_load_sim :
2345  ∀E,m1,m2,m1'.
2346  ∀Hinj:memory_inj E m1 m2.
2347  ∀ty,b,i,v.
2348  E b = None ? →
2349  store_value_of_type ty m1 b i v = Some ? m1' →
2350  load_sim_ptr E m1' m2.
2351#E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore
2352cases Hinj #Hsim #Hfreeblock #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl
2353cases ty in Hstore;
2354[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2355| #structname #fieldspec | #unionname #fieldspec | #id ]
2356[ 1,4,5,6,7: #Heq normalize in Heq; destruct ]
2357#Hstore whd
2358#b1 #off1 #b2 #off2 #ty' #v1 #Hvalid #Hembed' #Hload
2359lapply (store_value_of_type_load_value_of_type_conservation … Hstore b1 off1 ? ty')
2360[ 1,3,5: @(eq_block_elim … b b1) try // #Heq >Heq in Hembed;
2361         #Hembed whd in Hembed':(??%?); >Hembed in Hembed'; #H normalize in H;
2362         destruct ]
2363#Heq <Heq in Hload; #Hload
2364(* Three times the same proof, but computing the indices for the subcases is a PITA *)
2365[ 1:
2366  cases ty' in Hload;
2367  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2368  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2369  [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????);
2370               #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))}
2371               @conj try @refl %4 assumption ]
2372  #Hload @(Hsim … Hembed' … Hload)
2373  @(load_by_value_success_valid_pointer … Hload) //
2374| 2:
2375  cases ty' in Hload;
2376  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2377  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2378  [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????);
2379               #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))}
2380               @conj try @refl %4 assumption ]
2381  #Hload @(Hsim … Hembed' … Hload)
2382  @(load_by_value_success_valid_pointer … Hload) //
2383| 3:
2384  cases ty' in Hload;
2385  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2386  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2387  [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????);
2388               #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))}
2389               @conj try @refl %4 assumption ]
2390  #Hload @(Hsim … Hembed' … Hload)
2391  @(load_by_value_success_valid_pointer … Hload) //
2392] qed.
2393
2394lemma store_value_of_type_memory_inj :
2395  ∀E,m1,m2,m1'.
2396  ∀Hinj:memory_inj E m1 m2.
2397  ∀ty,b,i,v.
2398  E b = None ? →
2399  store_value_of_type ty m1 b i v = Some ? m1' →
2400  memory_inj E m1' m2.
2401#E #m1 #m2 #m1' #Hinj #ty #b #i #v1 #Hnot_mapped #Hstore
2402%
2403[ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore)
2404| *: lapply (mem_bounds_after_store_value_of_type … Hstore)
2405     * #H1 #H2
2406    [ #b * #Hnot_valid @(mi_freeblock ??? Hinj)
2407      % #H @Hnot_valid whd in H:% ⊢ %; >H1 @H
2408    | #p #p' #Hvalid @(mi_valid_pointers ??? Hinj)
2409      @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
2410      >H1 cases (H2 (pblock p)) #HA #HB
2411      >unfold_high_bound >unfold_low_bound
2412      >unfold_high_bound >unfold_low_bound
2413      >HA >HB //
2414    | @(mi_nodangling … Hinj)
2415    | @(mi_region … Hinj)
2416    | whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq #Hembed1 #Hembed2
2417      whd in match (block_is_empty ??);
2418      whd in match (block_is_empty m1' b2);
2419      >unfold_high_bound >unfold_low_bound
2420      >unfold_high_bound >unfold_low_bound
2421      cases (H2 b1) #HA #HB
2422      cases (H2 b2) #HC #HD
2423      >HA >HB >HC >HD
2424      @(mi_nonalias ??? Hinj) assumption
2425    | #bb whd
2426      lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?);
2427      cases (E bb) normalize nodelta try // * #bb' #off
2428      normalize nodelta
2429      whd in match (block_implementable_bv ??);     
2430      whd in match (block_implementable_bv m2 bb');
2431      whd in match (block_implementable_bv m1' bb);
2432      >unfold_high_bound >unfold_low_bound
2433      >unfold_high_bound >unfold_low_bound
2434      >unfold_high_bound
2435      cases (H2 bb) #HA #HB
2436      >HA >HB //
2437    ]
2438] qed.
2439
2440(* ------------------------------------------------------------------------- *)
2441(* Commutation results of standard unary and binary operations with value_eq. *)
2442
2443lemma unary_operation_value_eq :
2444  ∀E,op,v1,v2,ty.
2445   value_eq E v1 v2 →
2446   ∀r1.
2447   sem_unary_operation op v1 ty = Some ? r1 →
2448    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
2449#E #op #v1 #v2 #ty #Hvalue_eq #r1
2450inversion Hvalue_eq
2451[ 1: #v #Hv1 #Hv2 destruct
2452     cases op normalize
2453     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2454          normalize #Habsurd destruct (Habsurd)
2455     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2456          normalize #Habsurd destruct (Habsurd)
2457     | 2: #Habsurd destruct (Habsurd) ]
2458| 2: #vsz #i #Hv1 #Hv2 #_
2459     cases op
2460     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2461          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
2462          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2463               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
2464               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
2465               //
2466          | *: #Habsurd destruct (Habsurd) ]
2467     | 2: whd in match (sem_unary_operation ???);     
2468          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
2469     | 3: whd in match (sem_unary_operation ???);
2470          cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2471          normalize nodelta
2472          whd in ⊢ ((??%?) → ?);
2473          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2474               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
2475          | *: #Habsurd destruct (Habsurd) ] ]
2476| 3: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2477     cases op normalize nodelta
2478     [ 1: cases ty   [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2479          whd in match (sem_notbool ??);
2480          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2481     | 2: normalize #Habsurd destruct (Habsurd)
2482     | 3: cases ty    [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2483          whd in match (sem_neg ??);
2484          #Heq1 destruct ]
2485| 4: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
2486     cases op normalize nodelta
2487     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2488          whd in match (sem_notbool ??);         
2489          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2490     | 2: normalize #Habsurd destruct (Habsurd)
2491     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2492          whd in match (sem_neg ??);         
2493          #Heq1 destruct ]
2494]
2495qed.
2496
2497(* value_eq lifts to addition *)
2498lemma add_value_eq :
2499  ∀E,v1,v2,v1',v2',ty1,ty2.
2500   value_eq E v1 v2 →
2501   value_eq E v1' v2' →
2502   (* memory_inj E m1 m2 →  This injection seems useless TODO *)
2503   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
2504           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2505#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2506@(value_eq_inversion E … Hvalue_eq1)
2507[ 1: | 2: #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2508[ 1: whd in match (sem_add ????); normalize nodelta
2509     cases (classify_add ty1 ty2) normalize nodelta
2510     [ 1: #sz #sg | 2: #n #ty #sz #sg | 3: #n #sz #sg #ty | 4: #ty1' #ty2' ]
2511     #Habsurd destruct (Habsurd)
2512| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2513     cases (classify_add ty1 ty2) normalize nodelta
2514     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2515     [ 2,4: #Habsurd destruct (Habsurd) ]
2516     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2517     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
2518     [ 1,2,4,5,7: #Habsurd destruct (Habsurd) ]
2519     [ 1: @intsize_eq_elim_elim
2520          [ 1: #_ #Habsurd destruct (Habsurd)
2521          | 2: #Heq destruct (Heq) normalize nodelta
2522               #Heq destruct (Heq)
2523               /3 by ex_intro, conj, vint_eq/ ]
2524     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
2525          /3 by ex_intro, conj, vint_eq/
2526     | 3: #Heq destruct (Heq)
2527          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
2528          @(ex_intro … (conj … (refl …) ?))
2529          @vptr_eq whd in match (pointer_translation ??);
2530          cases (E b1') in Hembed;
2531          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2532          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2533               whd in match (shift_pointer_n ????);
2534               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) tsg i) offset =
2535                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) tsg i))
2536               [ 1: whd in match (offset_plus ??);
2537                    whd in match (shift_offset_n ????) in ⊢ (??%%);
2538                    >commutative_addition_n >associative_addition_n
2539                    <(commutative_addition_n … (offv offset) (offv o1')) @refl ]
2540               #Heq >Heq @refl ]
2541     ]
2542(* | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2543     cases (classify_add ty1 ty2) normalize nodelta
2544     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2545     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2546     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2547     [ 1: | 2: #sz' #i'| 3: | 4: #p1' #p2' #Hembed' ]
2548     [ 1,3,4,5,7: #Habsurd destruct (Habsurd) ]
2549     #Heq >Heq %{r1} @conj //
2550     /3 by ex_intro, conj, vfloat_eq/ *)
2551| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2552     cases (classify_add ty1 ty2) normalize nodelta
2553     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2554     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2555     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2556     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
2557     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2558     @eq_bv_elim
2559     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2560     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2561| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2562     cases (classify_add ty1 ty2) normalize nodelta
2563     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2564     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2565     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2566     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
2567     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2568     #Heq destruct (Heq)
2569     @(ex_intro … (conj … (refl …) ?))
2570     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2571     elim p1 in Hembed; #b1 #o1 normalize nodelta
2572     cases (E b1)
2573     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2574     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2575          whd in match (shift_pointer_n ????);
2576          whd in match (shift_offset_n ????) in ⊢ (??%%);
2577          whd in match (offset_plus ??);
2578          whd in match (offset_plus ??);
2579          >commutative_addition_n >(associative_addition_n … offset_size ?)
2580          >(commutative_addition_n ? (offv offset) ?) @refl
2581     ]
2582] qed.
2583
2584lemma subtraction_delta : ∀x,y,delta.
2585  subtraction offset_size
2586    (addition_n offset_size x delta)
2587    (addition_n offset_size y delta) =
2588  subtraction offset_size x y.
2589#x #y #delta whd in match subtraction; normalize nodelta
2590(* Remove all the equal parts on each side of the equation. *)
2591<associative_addition_n
2592>two_complement_negation_plus
2593<(commutative_addition_n … (two_complement_negation ? delta))
2594>(associative_addition_n ? delta) >bitvector_opp_addition_n
2595>(commutative_addition_n ? (zero ?)) >neutral_addition_n
2596@refl
2597qed.
2598
2599(* Offset subtraction is invariant by translation *)
2600lemma sub_offset_translation :
2601 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
2602#n #x #y #delta
2603whd in match (sub_offset ???) in ⊢ (??%%);
2604elim x #x' elim y #y' elim delta #delta'
2605whd in match (offset_plus ??);
2606whd in match (offset_plus ??);
2607>subtraction_delta @refl
2608qed.
2609
2610(* value_eq lifts to subtraction *)
2611lemma sub_value_eq :
2612  ∀E,v1,v2,v1',v2',ty1,ty2,target.
2613   value_eq E v1 v2 →
2614   value_eq E v1' v2' →
2615   ∀r1. (sem_sub v1 ty1 v1' ty2 target=Some val r1→
2616           ∃r2:val.sem_sub v2 ty1 v2' ty2 target=Some val r2∧value_eq E r1 r2).
2617#E #v1 #v2 #v1' #v2' #ty1 #ty2 #target #Hvalue_eq1 #Hvalue_eq2 #r1
2618@(value_eq_inversion E … Hvalue_eq1)
2619[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2620[ 1: whd in match (sem_sub ?????); normalize nodelta
2621     cases (classify_sub ty1 ty2) normalize nodelta
2622     [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ]
2623     #Habsurd destruct (Habsurd)
2624| 2: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
2625     cases (classify_sub ty1 ty2) normalize nodelta     
2626     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2627     [ 2,3,4: #Habsurd destruct (Habsurd) ]
2628     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2629     [  | #sz' #i' | | #p1' #p2' #Hembed' ]
2630     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2631     @intsize_eq_elim_elim
2632      [ 1: #_ #Habsurd destruct (Habsurd)
2633      | 2: #Heq destruct (Heq) normalize nodelta
2634           #Heq destruct (Heq)
2635          /3 by ex_intro, conj, vint_eq/
2636      ]
2637(*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2638     cases (classify_sub ty1 ty2) normalize nodelta
2639     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2640     [ 1,4: #Habsurd destruct (Habsurd) ]
2641     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2642     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2643     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2644     #Heq destruct (Heq)
2645     /3 by ex_intro, conj, vfloat_eq/ *)
2646| 3: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
2647     cases (classify_sub ty1 ty2) normalize nodelta
2648     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2649     [ 1,4: #Habsurd destruct (Habsurd) ]
2650     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2651     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
2652     [ 1,2,4,5,7,8: #Habsurd destruct (Habsurd) ]
2653     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2654                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2655     | 2: cases target
2656          [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2657          | #structname #fieldspec | #unionname #fieldspec | #id ]
2658          normalize nodelta
2659          #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
2660| 4: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
2661     cases (classify_sub ty1 ty2) normalize nodelta
2662     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2663     [ 1,4: #Habsurd destruct (Habsurd) ]
2664     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2665     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
2666     [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ]
2667     #Heq destruct (Heq)
2668     [ 1: @(ex_intro … (conj … (refl …) ?))
2669          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2670          elim p1 in Hembed; #b1 #o1 normalize nodelta
2671          cases (E b1)
2672          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2673          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2674               whd in match (offset_plus ??) in ⊢ (??%%);
2675               whd in match (neg_shift_pointer_n ?????) in ⊢ (??%%);
2676               whd in match (neg_shift_offset_n ?????) in ⊢ (??%%);
2677               whd in match (subtraction) in ⊢ (??%%); normalize nodelta
2678               generalize in match (short_multiplication ???); #mult
2679               /3 by associative_addition_n, commutative_addition_n, refl/
2680          ]
2681     | 2: lapply Heq @eq_block_elim
2682          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
2683          | 1: #Hpblock1_eq normalize nodelta
2684               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
2685               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
2686               whd in ⊢ ((??%?) → (??%?) → ?);
2687               cases (E b1') normalize nodelta
2688               [ 1: #Habsurd destruct (Habsurd) ]
2689               * #dest_block #dest_off normalize nodelta
2690               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_b_b normalize nodelta
2691               cases (eqb (sizeof tsg) O) normalize nodelta
2692               [ 1: #Habsurd destruct (Habsurd)
2693               | 2: cases target
2694                    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2695                    | #structname #fieldspec | #unionname #fieldspec | #id ]
2696                    normalize nodelta
2697                    #Heq destruct (Heq)
2698                    <(sub_offset_translation 32 off1 off1' dest_off)
2699                    cases (division_u ?
2700                            (sub_offset ? off1 off1')
2701                            (repr (sizeof tsg))) in Heq;
2702                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
2703                    | 2: #r1' cases sg normalize nodelta #Heq2 destruct (Heq2)
2704                         /3 by ex_intro, conj, vint_eq/ ]
2705    ] ] ]
2706] qed.
2707
2708lemma mul_value_eq :
2709  ∀E,v1,v2,v1',v2',ty1,ty2.
2710   value_eq E v1 v2 →
2711   value_eq E v1' v2' →
2712   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
2713           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2714#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2715@(value_eq_inversion E … Hvalue_eq1)
2716[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2717[ 1: whd in match (sem_mul ????); normalize nodelta
2718     cases (classify_aop ty1 ty2) normalize nodelta
2719     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2720     #Habsurd destruct (Habsurd)
2721| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2722     cases (classify_aop ty1 ty2) normalize nodelta
2723     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2724     [ 2: #Habsurd destruct (Habsurd) ]
2725     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2726     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2727     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2728     @intsize_eq_elim_elim
2729      [ 1: #_ #Habsurd destruct (Habsurd)
2730      | 2: #Heq destruct (Heq) normalize nodelta
2731           #Heq destruct (Heq)
2732          /3 by ex_intro, conj, vint_eq/           
2733      ]
2734| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2735     cases (classify_aop ty1 ty2) normalize nodelta
2736     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2737     [ 1,2: #Habsurd destruct (Habsurd) ]
2738| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2739     cases (classify_aop ty1 ty2) normalize nodelta
2740     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2741     #Habsurd destruct (Habsurd)
2742] qed.     
2743
2744lemma div_value_eq :
2745  ∀E,v1,v2,v1',v2',ty1,ty2.
2746   value_eq E v1 v2 →
2747   value_eq E v1' v2' →
2748   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
2749           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2750#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2751@(value_eq_inversion E … Hvalue_eq1)
2752[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2753[ 1: whd in match (sem_div ????); normalize nodelta
2754     cases (classify_aop ty1 ty2) normalize nodelta
2755     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2756     #Habsurd destruct (Habsurd)
2757| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2758     cases (classify_aop ty1 ty2) normalize nodelta
2759     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2760     [ 2: #Habsurd destruct (Habsurd) ]
2761     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2762     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2763     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2764     elim sg normalize nodelta
2765     @intsize_eq_elim_elim
2766     [ 1,3: #_ #Habsurd destruct (Habsurd)
2767     | 2,4: #Heq destruct (Heq) normalize nodelta
2768            @(match (division_s (bitsize_of_intsize sz') i i') with
2769              [ None ⇒ ?
2770              | Some bv' ⇒ ? ])
2771            [ 1: normalize  #Habsurd destruct (Habsurd)
2772            | 2: normalize #Heq destruct (Heq)
2773                 /3 by ex_intro, conj, vint_eq/
2774            | 3,4: elim sz' in i' i; #i' #i
2775                   normalize in match (pred_size_intsize ?);
2776                   generalize in match division_u; #division_u normalize
2777                   @(match (division_u ???) with
2778                    [ None ⇒ ?
2779                    | Some bv ⇒ ?]) normalize nodelta
2780                   #H destruct (H)
2781                  /3 by ex_intro, conj, vint_eq/ ]
2782     ]
2783| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2784     cases (classify_aop ty1 ty2) normalize nodelta
2785     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2786     [ 1,2: #Habsurd destruct (Habsurd) ]
2787| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2788     cases (classify_aop ty1 ty2) normalize nodelta
2789     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2790     #Habsurd destruct (Habsurd)
2791] qed.     
2792
2793lemma mod_value_eq :
2794  ∀E,v1,v2,v1',v2',ty1,ty2.
2795   value_eq E v1 v2 →
2796   value_eq E v1' v2' →
2797   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
2798           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2799#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2800@(value_eq_inversion E … Hvalue_eq1)
2801[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2802[ 1: whd in match (sem_mod ????); normalize nodelta
2803     cases (classify_aop ty1 ty2) normalize nodelta
2804     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2805     #Habsurd destruct (Habsurd)
2806| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2807     cases (classify_aop ty1 ty2) normalize nodelta
2808     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2809     [ 2: #Habsurd destruct (Habsurd) ]
2810     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2811     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2812     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2813     elim sg normalize nodelta
2814     @intsize_eq_elim_elim
2815     [ 1,3: #_ #Habsurd destruct (Habsurd)
2816     | 2,4: #Heq destruct (Heq) normalize nodelta
2817            @(match (modulus_s (bitsize_of_intsize sz') i i') with
2818              [ None ⇒ ?
2819              | Some bv' ⇒ ? ])
2820            [ 1: normalize  #Habsurd destruct (Habsurd)
2821            | 2: normalize #Heq destruct (Heq)
2822                 /3 by ex_intro, conj, vint_eq/
2823            | 3,4: elim sz' in i' i; #i' #i
2824                   generalize in match modulus_u; #modulus_u normalize
2825                   @(match (modulus_u ???) with
2826                    [ None ⇒ ?
2827                    | Some bv ⇒ ?]) normalize nodelta
2828                   #H destruct (H)
2829                  /3 by ex_intro, conj, vint_eq/ ]
2830     ]     
2831| *: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2832     cases (classify_aop ty1 ty2) normalize nodelta #foo #bar #Habsurd destruct (Habsurd)
2833] qed.
2834
2835(* boolean ops *)
2836lemma and_value_eq :
2837  ∀E,v1,v2,v1',v2'.
2838   value_eq E v1 v2 →
2839   value_eq E v1' v2' →
2840   ∀r1. (sem_and v1 v1'=Some val r1→
2841           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
2842#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2843@(value_eq_inversion E … Hvalue_eq1)
2844[ 2: #sz #i
2845     @(value_eq_inversion E … Hvalue_eq2)
2846     [ 2: #sz' #i' whd in match (sem_and ??);
2847          @intsize_eq_elim_elim
2848          [ 1: #_ #Habsurd destruct (Habsurd)
2849          | 2: #Heq destruct (Heq) normalize nodelta
2850               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2851] ]
2852normalize in match (sem_and ??); #arg1 destruct
2853normalize in match (sem_and ??); #arg2 destruct
2854normalize in match (sem_and ??); #arg3 destruct
2855normalize in match (sem_and ??); #arg4 destruct
2856qed.
2857
2858lemma or_value_eq :
2859  ∀E,v1,v2,v1',v2'.
2860   value_eq E v1 v2 →
2861   value_eq E v1' v2' →
2862   ∀r1. (sem_or v1 v1'=Some val r1→
2863           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
2864#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2865@(value_eq_inversion E … Hvalue_eq1)
2866[ 2: #sz #i
2867     @(value_eq_inversion E … Hvalue_eq2)
2868     [ 2: #sz' #i' whd in match (sem_or ??);
2869          @intsize_eq_elim_elim
2870          [ 1: #_ #Habsurd destruct (Habsurd)
2871          | 2: #Heq destruct (Heq) normalize nodelta
2872               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2873] ]
2874normalize in match (sem_or ??); #arg1 destruct
2875normalize in match (sem_or ??); #arg2 destruct
2876normalize in match (sem_or ??); #arg3 destruct
2877normalize in match (sem_or ??); #arg4 destruct
2878qed.
2879
2880lemma xor_value_eq :
2881  ∀E,v1,v2,v1',v2'.
2882   value_eq E v1 v2 →
2883   value_eq E v1' v2' →
2884   ∀r1. (sem_xor v1 v1'=Some val r1→
2885           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
2886#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2887@(value_eq_inversion E … Hvalue_eq1)
2888[ 2: #sz #i
2889     @(value_eq_inversion E … Hvalue_eq2)
2890     [ 2: #sz' #i' whd in match (sem_xor ??);
2891          @intsize_eq_elim_elim
2892          [ 1: #_ #Habsurd destruct (Habsurd)
2893          | 2: #Heq destruct (Heq) normalize nodelta
2894               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2895] ]
2896normalize in match (sem_xor ??); #arg1 destruct
2897normalize in match (sem_xor ??); #arg2 destruct
2898normalize in match (sem_xor ??); #arg3 destruct
2899normalize in match (sem_xor ??); #arg4 destruct
2900qed.
2901
2902lemma shl_value_eq :
2903  ∀E,v1,v2,v1',v2'.
2904   value_eq E v1 v2 →
2905   value_eq E v1' v2' →
2906   ∀r1. (sem_shl v1 v1'=Some val r1→
2907           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
2908#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2909@(value_eq_inversion E … Hvalue_eq1)
2910[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2911[ 2:
2912     @(value_eq_inversion E … Hvalue_eq2)
2913     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2914     [ 2: whd in match (sem_shl ??);
2915          cases (lt_u ???) normalize nodelta
2916          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
2917          | 2: #Habsurd destruct (Habsurd)
2918          ]
2919     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2920| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2921qed.
2922
2923lemma shr_value_eq :
2924  ∀E,v1,v2,v1',v2',ty,ty'.
2925   value_eq E v1 v2 →
2926   value_eq E v1' v2' →
2927   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
2928           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
2929#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
2930@(value_eq_inversion E … Hvalue_eq1)
2931[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2932whd in match (sem_shr ????); whd in match (sem_shr ????);
2933[ 1: cases (classify_aop ty ty') normalize nodelta
2934     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2935     #Habsurd destruct (Habsurd)
2936| 2: cases (classify_aop ty ty') normalize nodelta
2937     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2938     [ 2: #Habsurd destruct (Habsurd) ]
2939     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2940     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2941     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2942     elim sg normalize nodelta
2943     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
2944     /3 by ex_intro, conj, refl, vint_eq/
2945| *: cases (classify_aop ty ty') normalize nodelta
2946     #foo #bar
2947     #Habsurd destruct (Habsurd)
2948] qed.     
2949
2950lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
2951* #delta * #x * #y
2952whd in match (offset_plus ??);
2953whd in match (offset_plus ??);
2954whd in match cmp_offset; normalize nodelta
2955whd in match eq_offset; normalize nodelta
2956@(eq_bv_elim … x y)
2957[ 1: #Heq >Heq >eq_bv_true @refl
2958| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
2959     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
2960     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
2961] qed.     
2962
2963lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
2964* #delta * #x * #y
2965whd in match (offset_plus ??);
2966whd in match (offset_plus ??);
2967whd in match cmp_offset; normalize nodelta
2968whd in match eq_offset; normalize nodelta
2969@(eq_bv_elim … x y)
2970[ 1: #Heq >Heq >eq_bv_true @refl
2971| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
2972     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
2973     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
2974] qed.
2975
2976(* Note that x and y are bounded below and above, similarly for the shifted offsets.
2977   This is enough to prove that there is no "wrap-around-the-end" problem,
2978   /provided we know that the block bounds are implementable by 2^16 bitvectors/.
2979   We axiomatize it for now. *)
2980axiom cmp_offset_translation :
2981  ∀op,delta,x,y.
2982  (Zoo x) + (Zoo delta) < Z_two_power_nat 16 →
2983  (Zoo y) + (Zoo delta) < Z_two_power_nat 16 →
2984  cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
2985
2986lemma valid_pointer_of_implementable_block_is_implementable :
2987  ∀m,b.
2988    block_implementable_bv m b →
2989    ∀o. valid_pointer m (mk_pointer b o) = true →
2990        Zoo o < Z_two_power_nat 16.
2991#m #b whd in ⊢ (% → ?); * #Hlow #Hhigh
2992* #o #Hvalid cases (valid_pointer_to_Prop … Hvalid) * #_
2993#Hlow' #Hhigh'
2994cases Hlow -Hlow #Hlow0 #Hlow16
2995cases Hhigh -Hhigh #Hhigh0 #Hhigh16
2996whd in match (Zoo ?);
2997@(transitive_Zlt … Hhigh' Hhigh16)
2998qed.
2999
3000lemma cmp_value_eq :
3001  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
3002   value_eq E v1 v2 →
3003   value_eq E v1' v2' →
3004   memory_inj E m1 m2 →
3005   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1 →
3006           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
3007#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
3008elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj
3009whd in match (sem_cmp ??????) in ⊢ ((??%?) → %);
3010cases (classify_cmp ty ty') normalize nodelta
3011[ 1: #tsz #tsg
3012     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
3013     [ 1: #Habsurd destruct (Habsurd)
3014     | 3: #Habsurd destruct (Habsurd)
3015     | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
3016     #sz #i
3017     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
3018     [ 1: #Habsurd destruct (Habsurd)
3019     | 3: #Habsurd destruct (Habsurd)
3020     | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
3021     #sz' #i' cases tsg normalize nodelta
3022     @intsize_eq_elim_elim
3023     [ 1,3: #Hneq #Habsurd destruct (Habsurd)
3024     | 2,4: #Heq destruct (Heq) normalize nodelta
3025            #Heq destruct (Heq)
3026            [ 1: cases (cmp_int ????) whd in match (of_bool ?);
3027            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
3028              /3 by ex_intro, conj, vint_eq/ ]
3029| 3: #ty1 #ty2 #Habsurd destruct (Habsurd)
3030| 2: lapply Hinj -Hinj
3031     generalize in match (mk_mem contmap1 ??); #m1
3032     generalize in match (mk_mem contmap2 ??); #m2
3033     #Hinj #optn #typ
3034     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
3035     [ 1: #Habsurd destruct (Habsurd)
3036     | 2: #sz #i #Habsurd destruct (Habsurd)
3037     | 4: #p1 #p2 #Hembed ]
3038     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
3039     [ 1,5: #Habsurd destruct (Habsurd)
3040     | 2,6: #sz #i #Habsurd destruct (Habsurd)
3041     | 4,8: #q1 #q2 #Hembed' ]
3042     [ 2,3: cases op whd in match (sem_cmp_mismatch ?);
3043          #Heq destruct (Heq)
3044          [ 1,3: %{Vfalse} @conj try @refl @vint_eq
3045          | 2,4: %{Vtrue} @conj try @refl @vint_eq ]
3046     | 4: cases op whd in match (sem_cmp_match ?);
3047          #Heq destruct (Heq)
3048          [ 2,4: %{Vfalse} @conj try @refl @vint_eq
3049          | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ]
3050     #Hvalid
3051     lapply (if_opt_inversion ???? Hvalid) -Hvalid * #Hconj
3052     lapply (andb_inversion … Hconj) -Hconj * #Hvalid #Hvalid'
3053     lapply (mi_valid_pointers … Hinj q1 q2 Hvalid' Hembed') #Hvalid2' >Hvalid2'
3054     lapply (mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) #Hvalid2 >Hvalid2
3055     normalize nodelta
3056(*   >(mi_valid_pointers … Hinj p1' p2' Hvalid' Hembed')
3057     >(mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) normalize nodelta *)
3058     elim p1 in Hvalid Hembed; #bp1 #op1
3059     elim q1 in Hvalid' Hembed'; #bq1 #oq1
3060     #Hvalid' #Htmp #Hvalid lapply Htmp -Htmp
3061     whd in match (pointer_translation ??);
3062     whd in match (pointer_translation ??);
3063     @(eq_block_elim … bp1 bq1)
3064     [ 1: #Heq destruct (Heq) normalize nodelta
3065          lapply (mi_nowrap … Hinj bq1)
3066          whd in ⊢ (% → ?);
3067          cases (E bq1) normalize nodelta
3068          [ #_ #Habsurd destruct ]
3069          * #BLO #OFF normalize nodelta * *         
3070          #Hbq1_implementable #HBLO_implementable #Hno_wrap
3071          #Heq1 #Heq2 #Heq3 destruct
3072          >eq_block_b_b normalize nodelta
3073          lapply (cmp_offset_translation op OFF op1 oq1 ??)
3074          [ @(Zlt_sum_weaken … Hno_wrap)
3075            cases (valid_pointer_to_Prop … Hvalid') * #_ #_ try //
3076          | @(Zlt_sum_weaken … Hno_wrap)
3077            cases (valid_pointer_to_Prop … Hvalid) * #_ #_ try // ]
3078          #Heq <Heq
3079          cases (cmp_offset op op1 oq1)
3080          normalize nodelta
3081          try /3 by ex_intro, conj, refl, vint_eq/
3082     | 2: #Hneq lapply (mi_nonalias … Hinj bp1 bq1)
3083          normalize nodelta
3084          lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?);
3085          lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?);
3086          lapply (mi_region … Hinj bq1)
3087          lapply (mi_region … Hinj bp1)
3088          cases (E bq1) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
3089          * #BLOq #DELTAq normalize nodelta
3090          cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
3091          * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
3092          lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2
3093          #Hregion2 #Hregion1
3094          cases op
3095          whd in ⊢ ((??%?) → ?); #H' destruct (H')
3096          whd in match (sem_cmp_mismatch ?);
3097          lapply (H ???? Hneq (refl ??) (refl ??)) -H
3098          cases (block_decidable_eq BLOp BLOq) normalize nodelta
3099          #H
3100          [ 2: #_ >(not_eq_block … H) normalize nodelta %{Vfalse} @conj try @refl %2
3101          | 4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ]
3102          destruct (H) generalize in match BLOq in Hnowrap1 Hnowrap2 Hvalid2 Hvalid2' ⊢ %;
3103          #target_block * * #Himplq1 #Himpltarget #Hnowrap_q1
3104          * * #Himplp1 #_ #Hnowrap_p1 #Hvalid2 #Hvalid2'
3105          lapply (valid_pointer_to_Prop … Hvalid)
3106          lapply (valid_pointer_to_Prop … Hvalid')
3107          * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
3108          >eq_block_b_b normalize nodelta
3109          *
3110          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
3111                 cases (valid_pointer_to_Prop … Hvalid') * #_ #Hle #Hlt
3112                 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt'
3113                 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl
3114                 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ]
3115          *
3116          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
3117                 cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt
3118                 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt'
3119                 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl
3120                 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ]
3121          *
3122          #Hdisjoint
3123          whd in match (cmp_offset); normalize nodelta
3124          whd in match (eq_offset); normalize nodelta
3125          whd in match (offset_plus ??);
3126          whd in match (offset_plus ??);
3127          lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2)
3128          lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2')
3129          #Himpl1 #Himpl2
3130          [ 1,3:
3131              (* We show the non-equality of the rhs by exhibiting disjointness of blocks. This is made
3132               * painful by invariants on non-overflowing offsets. We exhibit [a]+[b] < [c]+[d], then
3133               * cut [a+b]<[c+d] (using a subcut for needed consistency hypotheses) and conclude easily
3134               * [a+b] ≠ [c+d]. *)
3135              cut ((Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp))
3136                   < (Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq)))
3137              [ 1,3:
3138                @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bp1 + Zoo DELTAp) ?)
3139                [ 1,3: @Zlt_translate assumption
3140                | 2,4: @(transitive_Zle ? (low_bound m1 bq1+Zoo DELTAq) ?) try assumption
3141                       @monotonic_Zle_Zplus_l try assumption ]
3142              ]
3143              #Hlt_stepA
3144              cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp))
3145                   < Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq)))
3146              [ 1,3:
3147                >Z_addition_bv_commute
3148                [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ]
3149                >Z_addition_bv_commute
3150                [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ]
3151                try assumption ] -Hlt_stepA
3152           | 2,4:
3153              cut ((Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq))
3154                   < (Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp)))
3155              [ 1,3:
3156                @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bq1 + Zoo DELTAq) ?)
3157                [ 1,3: @Zlt_translate assumption
3158                | 2,4: @(transitive_Zle ? (low_bound m1 bp1+Zoo DELTAp) ?) try assumption
3159                       @monotonic_Zle_Zplus_l try assumption ]
3160              ]
3161              #Hlt_stepA
3162              cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq))
3163                   < Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp)))
3164              [ 1,3:
3165                >Z_addition_bv_commute
3166                [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ]
3167                >Z_addition_bv_commute
3168                [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ]
3169                try assumption ] -Hlt_stepA
3170            ]
3171            generalize in match (addition_n ? (offv op1) ?); #lhs
3172            generalize in match (addition_n ? (offv oq1) ?); #rhs
3173            #Hlt_stepB lapply (Zlt_to_Zneq … Hlt_stepB)
3174            @(eq_bv_elim … lhs rhs)
3175            [ 1,3,5,7: #Heq destruct * #H @(False_ind … (H (refl ??)))
3176            | 2,4,6,8: #Hneq #_ /3 by ex_intro, conj, vint_eq/ ]
3177    ]
3178] qed.
3179   
Note: See TracBrowser for help on using the repository browser.