source: src/Clight/memoryInjections.ma @ 2822

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

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

File size: 131.7 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
762(* All data in a valid block is unchanged after an alloc. *)
763lemma alloc_beloadv_conservation :
764  ∀m,m',block,offset,z1,z2,(*r,*)new_block.
765    valid_block m block →
766    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
767    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
768* #contents #next #Hcorrect #m' #block #offset #z1 #z2 (* #r*) #new_block #Hvalid #Halloc
769whd in Halloc:(??%?); destruct (Halloc)
770whd in match (beloadv ??) in ⊢ (??%%);
771lapply (Zlt_to_Zltb_true … Hvalid) #Hlt
772>Hlt >(zlt_succ … Hlt)
773normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
774cut (eqZb (block_id block) next = false)
775[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq
776>Hneq @refl
777qed.
778
779(* Lift [alloc_beloadv_conservation] to loadn *)
780lemma alloc_loadn_conservation :
781  ∀m,m',z1,z2,(*r,*)new_block.
782    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
783    ∀n. ∀block,offset.
784    valid_block m block →
785    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
786#m #m' #z1 #z2 (*#r*) #new_block #Halloc #n
787elim n try //
788#n' #Hind #block #offset #Hvalid_block
789whd in ⊢ (??%%);
790>(alloc_beloadv_conservation … Hvalid_block Halloc)
791cases (beloadv m' (mk_pointer block offset)) //
792#bev normalize nodelta
793whd in match (shift_pointer ???); >Hind try //
794qed.
795
796lemma alloc_load_value_of_type_conservation :
797  ∀m,m',z1,z2(*,r*),new_block.
798    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
799    ∀block,offset.
800    valid_block m block →
801    ∀ty. load_value_of_type ty m block offset =
802         load_value_of_type ty m' block offset.
803#m #m' #z1 #z2 (*#r*) #new_block #Halloc #block #offset #Hvalid         
804#ty cases ty
805[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
806| #structname #fieldspec | #unionname #fieldspec | #id ]
807try //
808whd in match (load_value_of_type ????) in ⊢ (??%%);
809>(alloc_loadn_conservation … Halloc … Hvalid) @refl
810qed.
811
812(* Memory allocation in m2 preserves [memory_inj].
813 * This is lemma 66 from Leroy&Blazy. *)
814lemma alloc_memory_inj_m2 :
815  ∀E:embedding.
816  ∀m1,m2,m2',z1,z2(*,r*),new_block.
817  ∀H:memory_inj E m1 m2.
818  alloc m2 z1 z2 (*r*) = 〈m2', new_block〉 →
819  block_implementable_bv m2' new_block →
820  memory_inj E m1 m2'.
821#E #m1 #m2 #m2' #z1 #z2 (*#r*) * #new_block (* #Hregion *) #Hmemory_inj #Halloc #Himpl
822%
823[ whd
824  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
825  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
826  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
827  lapply (refl ? (access_mode ty))
828  cases ty in Hload_eq;
829  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
830  | #structname #fieldspec | #unionname #fieldspec | #id ]
831  #Hload normalize in ⊢ ((???%) → ?); #Haccess
832  [ 1,6,7: normalize in Hload; destruct (Hload)
833  | 2,3,8:
834     lapply (load_by_value_success_valid_block … Haccess Hload)
835     #Hvalid_block
836      <(alloc_load_value_of_type_conservation … Halloc … Hvalid_block)
837     assumption
838  | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
839| @(mi_freeblock … Hmemory_inj)
840| #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
841     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
842     elim p' * (*#br'*) #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
843     whd in match (valid_pointer ??) in ⊢ (% → %);
844     @Zltb_elim_Type0
845     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
846     #Hbid' cut (Zltb bid' (Zsucc new_block) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
847     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
848     whd in match (high_bound ??) in ⊢ (% → %);
849     whd in match (update_block ?????);
850     whd in match (eq_block ??);
851     cut (eqZb bid' new_block = false) [ 1: @eqZb_false /2 by not_to_not/ ]
852     #Hbid_neq >Hbid_neq #H @H
853(*     cases (eq_region br' r) normalize #H @H*)
854| #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H
855  @(alloc_valid_block_conservation … Halloc … H)
856| @(mi_region … Hmemory_inj)
857| @(mi_nonalias … Hmemory_inj)
858| #b lapply (mi_nowrap … Hmemory_inj b)
859   whd in ⊢ (% → %);
860   lapply (mi_nodangling … Hmemory_inj b)
861   cases (E b) normalize nodelta try //
862   * #B #OFF normalize nodelta #Hguard
863   * * #H1 #H2 #Hinbounds @conj try @conj try assumption
864   @(eq_block_elim … (mk_block new_block) B)
865   [ #H <H assumption
866   | #H cases m2 in Halloc H2; #contents #nextblock #notnull
867       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) *
868       >unfold_low_bound >unfold_high_bound #HA #HB
869       @conj
870       >unfold_low_bound >unfold_high_bound
871       whd in match (update_block ?????);
872       >(not_eq_block … (sym_neq ??? H)) normalize nodelta
873       try assumption ]
874] qed.
875
876(* Allocating in m1 such that the resulting block has no image in m2 preserves
877   the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as
878   in Blazy & Leroy. Notice that we must consider blocks with different regions but
879   same id as equal. *)
880lemma alloc_memory_inj_m1 :
881  ∀E:embedding.
882  ∀m1,m2,m1',z1,z2,(*r,*)new_block.
883  ∀H:memory_inj E m1 m2.
884  alloc m1 z1 z2 (*r*) = 〈m1', new_block〉 →
885  memory_inj (λx. if eq_block new_block x then None ? else E x) m1' m2 ∧
886  embedding_compatible E (λx. if eq_block new_block x then None ? else E x).
887#E #m1 #m2 #m1' #z1 #z2 (* #r*) #new_block (* #Hregion_eq *) #Hinj #Halloc
888cut (E new_block = None ?)
889[ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?);
890  #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
891#Hempty
892cut (embedding_compatible E
893     (λx.
894       if eq_block new_block x
895       then None (block×offset)
896       else E x))
897[ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 @Hempty ]
898#Hembedding_compatible @conj try assumption
899%
900[ whd #b1 #off1 #b2 #off2 #ty #v1
901  @(eq_block_elim … b1 new_block)
902  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta
903    #Habsurd destruct ]
904  #Hneq #Hvalid
905  whd in ⊢ ((??%?) → ?);
906  @(eq_block_elim … new_block b1)
907  normalize nodelta
908  [ #Heq #Habsurd destruct (Habsurd) ]
909  #Hneq_id
910  #Hembed #Hload
911  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) (sym_neq ??? Hneq_id) Hvalid)
912  #Hvalid'
913  cut (valid_block m1 b1)
914  [ cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block #_ #_ @Hvalid_block ]
915  #Hvalid_block
916  lapply (alloc_load_value_of_type_conservation … Halloc … off1 … Hvalid_block ty)
917  #Heq <Heq in Hload; #Hload
918  lapply (mi_inj … Hinj … Hvalid' … Hembed … Hload) * #v2 * #Hload2 #Hveq2
919  %{v2} @conj try assumption
920  @(embedding_compatibility_value_eq … Hveq2) assumption
921| #b #Hnot_valid @(eq_block_elim … new_block b)
922  normalize nodelta
923  [ #Heq @refl
924  | #Hneq @(mi_freeblock … Hinj) % #Hvalid cases Hnot_valid #H @H
925    @(alloc_valid_block_conservation … Halloc) assumption ]
926| #p #p' lapply (mi_valid_pointers … Hinj p p')
927  cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1'
928  whd in ⊢ ((??%%) → ?); 
929  @(eq_block_elim … new_block b) normalize nodelta
930  [ #Heq #Habsurd destruct ]
931  #Hneq #Hembed
932  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b o) (sym_neq ??? Hneq) Hvalid1')
933  #Hvalid1
934  @(Hvalidptr Hvalid1 Hembed)
935| #b #b' #o' @(eq_block_elim … new_block b)
936  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
937  normalize nodelta #Henq
938  @(mi_nodangling … Hinj)
939| #b #b' #o' @(eq_block_elim … new_block b)
940  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
941  #Hneq @(mi_region … Hinj)
942| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
943  @(eq_block_elim … new_block b1)
944  normalize nodelta
945  [ #Heq #Habsurd destruct (Habsurd) ]
946  #Hneq1 #Hembed1
947  @(eq_block_elim … new_block b2)
948  normalize nodelta
949  [ #Heq #Habsurd destruct (Habsurd) ]
950  #Hneq2 #Hembed2
951  @(eq_block_elim … b1' b2') normalize nodelta try //
952  #Heq
953  lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq
954  >eq_block_b_b normalize nodelta
955  cases m1 in Halloc; #contents #next #Hnext
956  >unfold_high_bound >unfold_low_bound
957  >unfold_high_bound >unfold_low_bound
958  >unfold_high_bound >unfold_low_bound
959  >unfold_high_bound >unfold_low_bound
960  whd in ⊢ ((??%%) → ?); destruct (Heq) #Heq destruct (Heq)
961  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq1))
962  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq2))
963  #Heq_block_2
964  #Heq_block_1
965  * [ * [ * | ] | ]
966  whd in match (update_block ?????);
967  >Heq_block_1 normalize nodelta
968  whd in match (update_block ?????);
969  >Heq_block_2 normalize nodelta
970  #H
971  try /4 by or_introl, or_intror, conj/
972  [ %1 %2 whd whd in H;
973    >unfold_high_bound
974    whd in match (update_block ?????);
975    >unfold_low_bound
976    whd in match (update_block ?????);
977    >Heq_block_1 normalize nodelta @H
978  | %2 whd whd in H;
979    >unfold_high_bound
980    whd in match (update_block ?????);
981    >unfold_low_bound
982    whd in match (update_block ?????);
983    >Heq_block_1 >Heq_block_2 @H
984  ]
985| #b whd @(eq_block_elim … new_block b) normalize nodelta try //
986  #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
987  cases (E b) normalize nodelta try //
988  * #bb #oo normalize nodelta
989  * * * #HA #HB * #HC #HD #HE @conj try @conj
990  try @conj
991  lapply HE -HE
992  lapply HD -HD
993  lapply HC -HC
994  lapply HB -HB
995  lapply HA -HA
996  >unfold_low_bound >unfold_low_bound [ >unfold_low_bound ]
997  >unfold_high_bound >unfold_high_bound [ 2,5: >unfold_high_bound ]
998 cases m1 in Halloc; #cont #next #Hnext
999 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try //
1000 whd in match (update_block ?????);
1001 cut (eq_block b (mk_block next) = false)
1002 [ 1,3,5: @neq_block_eq_block_false @(sym_neq … Hneq)
1003 | 2,4,6: #Heq_block >Heq_block // ]
1004] qed.
1005
1006(* loading by-value from a freshly allocated block yields either an undef value or
1007 * None. *)
1008lemma load_by_value_after_alloc_undef :
1009  ∀m,m',z1,z2,b.
1010    alloc m z1 z2 = 〈m', b〉 →
1011    ∀ty. access_mode ty = By_value (typ_of_type ty) →
1012    ∀off. load_value_of_type ty m' b off = Some ? Vundef ∨
1013          load_value_of_type ty m' b off = None ?.
1014#m #m' #z1 #z2 (* * #br  #bid *) #b
1015cases m #contents #nextblock #Hnext
1016whd in ⊢ ((??%?) → ?);
1017#Heq destruct (Heq)
1018#ty cases ty   
1019[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1020| #structname #fieldspec | #unionname #fieldspec | #id ]
1021whd in ⊢ ((??%?) → ?);
1022#Heq destruct (Heq)
1023#off
1024whd in match (load_value_of_type ????);
1025(* We can't generalize over the typesize, sadly. We thus perform three identical inductions.
1026 * Another solution would be to provide an ad-hoc lemma, but the goal is too ugly for that. *)
1027[ lapply off -off
1028  generalize in match (typesize ?); #tsz
1029| lapply off -off
1030  generalize in match (typesize ?); #tsz
1031| lapply off -off
1032  generalize in match (typesize ?); #tsz
1033]
1034elim tsz 
1035[ 1,3,5: #off whd in match (loadn ???); normalize nodelta %1 @refl
1036| *: #tsz' #Hind #off
1037    whd in match (loadn ???);
1038    whd in match (beloadv ??);
1039    cases (Zltb ??) normalize nodelta try /1 by or_intror/
1040    cases (Zleb ??) normalize nodelta try /1 by or_intror/
1041    >andb_lsimpl_true
1042    cases (Zltb ??); normalize nodelta try /1 by or_intror/
1043    whd in match (update_block ?????);
1044    >eq_block_b_b normalize nodelta
1045    cases (Hind (shift_offset 2 off (bitvector_of_nat 2 1)))
1046    cases (loadn ???) normalize nodelta try //
1047    #bevals #Heq %1 whd in match (be_to_fe_value ??);
1048    try @refl ]
1049qed.
1050
1051
1052(* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order
1053 * to prove the equivalent of lemma 68 of L&B, we need to provide an additional
1054 * property of the target memory: the /target/ portion of memory we are going to map a block
1055 * to must only contains BVundef (whereas in CompCert, the fact that the source block
1056 * contains BVundefs is enough to proceed).
1057 *
1058 * The following definition expresses the fact that a portion of memory [z1; z2] contains only
1059 * BVundefs.
1060 * Note that the bounds are /inclusive/. We do not check for their validity. *)
1061definition undef_memory_zone : mem → block → Z → Z → Prop ≝
1062  λm,b,z1,z2.
1063    ∀i. z1 ≤ i → i ≤ z2 → contents (blocks m b) i = BVundef.
1064
1065(* Explictly stating the properties of alloc. *)
1066lemma alloc_properties :
1067  ∀m,m',z1,z2(*,r*),b.
1068   alloc m z1 z2 (* r *) = 〈m',b〉 →
1069   low_bound m' b = z1 ∧
1070   high_bound m' b = z2 ∧
1071   undef_memory_zone m' b z1 z2.
1072#m #m'  #z1 #z2 * (* #br *) #bid
1073cases m #contents #next #Hnext
1074whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1075>unfold_low_bound >unfold_high_bound
1076@conj try @conj
1077/2 by refl, pair_destruct_2/
1078whd
1079#i #H1 #H2 whd in match (update_block ?????);
1080>eq_block_b_b normalize nodelta @refl
1081qed.
1082
1083
1084(* Embed a fresh block inside an unmapped portion of the target block.
1085 * This is the equivalent of lemma 68 of Leroy&Blazy.
1086 * Compared to L&B, an additional "undef_memory_zone" proof object must be provided.
1087 * We also constrain the memory bounds of the new block to be bitvector-implementable,
1088 * otherwise we can't prove that addition commutes with conversions between Z and
1089 * bitvectors.
1090 *)
1091lemma alloc_memory_inj_m1_to_m2 :
1092  ∀E:embedding.
1093  ∀m1,m2,m1':mem.
1094  ∀z1,z2:Z.
1095  ∀target,new_block.
1096  ∀delta:offset.
1097  valid_block m2 target →
1098  block_implementable_bv m1' new_block →
1099  block_implementable_bv m2 target →
1100  block_region new_block = block_region target →
1101  (high_bound m1' new_block) + (Zoo delta) < Z_two_power_nat 16 →
1102  alloc m1 z1 z2 = 〈m1', new_block〉 →
1103  low_bound m2 target ≤ z1 + Zoo delta →
1104  z2 + Zoo delta ≤ high_bound m2 target →
1105  undef_memory_zone m2 target (z1 + Zoo delta) (z2 + Zoo delta) →
1106  (∀b,delta'. b ≠ new_block →
1107              E b = Some ? 〈target, delta'〉 →
1108              high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
1109              z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →
1110  memory_inj E m1 m2 →
1111  memory_inj (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x) m1' m2.
1112#E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #target (* * * #newr *) #new_block (* * *) #delta
1113#Hvalid #Himpl1 #Himpl2 #Hregion #Hno_overflow #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj
1114cut (E new_block = (None ?))
1115[ @(mi_freeblock ??? Hinj new_block) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj
1116  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
1117#Hnew_not_mapped
1118cut (embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x))
1119[ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 assumption ]
1120#Hembedding_compatible
1121%
1122[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload
1123  @(eq_block_elim … new_block b1)
1124  [ 2: (* we do not load from the newly allocated block *)
1125     #Hneq
1126     (* prove that we can equivalently load from the memory before alloc *)
1127     cases (some_inversion ????? Hembed) * #target' #delta'
1128     >(neq_block_eq_block_false … Hneq) normalize nodelta
1129     * #Hembed #Heq destruct (Heq)
1130     cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh
1131     lapply (alloc_valid_block_conservation2 … Halloc … (sym_neq ??? Hneq) Hvalid_block')
1132     #Hvalid_block
1133     lapply (alloc_load_value_of_type_conservation … Halloc b1 off1 … Hvalid_block ty)
1134     #Heq_load <Heq_load in Hload; #Hload
1135     lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … (sym_neq ??? Hneq) Hvalid')     
1136     #Hvalid_ptr
1137     lapply (mi_inj … Hinj b1 off1 b2 (offset_plus off1 delta') … Hvalid_ptr … Hload)
1138     [ whd in ⊢ (??%?); >Hembed @refl ]
1139     (* conclude *)
1140     * #v2 * #Hload2 #Hvalue_eq %{v2} @conj
1141     [ @Hload2
1142     | @(embedding_compatibility_value_eq … Hvalue_eq) @Hembedding_compatible ]
1143  | 1: (* we allegedly performed a load from a block with the same id as
1144        * the newly allocated block (which by def. of alloc contains only BVundefs) *)
1145     #Heq destruct (Heq)
1146     whd in Hembed:(??%?); >eq_block_b_b in Hembed; normalize nodelta
1147     #Heq_ptr
1148     (* cull out all boring cases *)
1149     lapply Hload -Hload cases ty
1150     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1151     | #structname #fieldspec | #unionname #fieldspec | #id ]
1152     [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
1153     | 4,5: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq_ptr Heq)
1154            %{(Vptr (mk_pointer b2 (offset_plus off1 delta)))}
1155            @conj
1156            [ 1,3: @refl
1157            | *: %4 whd in ⊢ (??%?); >eq_block_b_b @refl ] ]
1158     (* Now: load-by-value cases. Outcome is either None or Undef. *)
1159     lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 Halloc)
1160     #Hload_eq
1161     [ lapply (Hload_eq (Tint sz sg) (refl ??) off1)
1162     | lapply (Hload_eq (Tpointer ptr_ty) (refl ??) off1)
1163     | lapply (Hload_eq (Tcomp_ptr id) (refl ??) off1) ]
1164     *
1165     (* None case: absurd *)
1166     [ 2,4,6: #Hload >Hload #Habsurd destruct (Habsurd) ]
1167     #Hload >Hload #Heq destruct (Heq) %{Vundef}
1168     @conj try // destruct (Heq_ptr)
1169     (* prove the validity of this pointer  in order tu unfold load *)
1170     cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true)
1171     [ 1,3,5: @valid_pointer_of_Prop @conj try @conj
1172        [ 1,4,7: assumption
1173        | 2,5,8: >unfold_low_bound
1174           lapply (alloc_properties … Halloc) * *
1175           >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef
1176           lapply (valid_pointer_to_Prop … Hvalid') * *
1177           #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh'
1178           #Hle_low #Hlt_high destruct
1179           cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta)
1180           [ 1,3,5: >Z_addition_bv_commute try @refl
1181                    @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l
1182                    @Hlt_high
1183           ]
1184           #Hsum_split
1185           cut (low (blocks m1' b1) + Zoo delta ≤ Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta)))
1186           [ 1,3,5: >Hsum_split @monotonic_Zle_Zplus_l assumption ]
1187           @(transitive_Zle … Hlow)
1188       | 3,6,9: >unfold_high_bound
1189           lapply (alloc_properties … Halloc) * *
1190           >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef
1191           lapply (valid_pointer_to_Prop … Hvalid') * *
1192           #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh'
1193           #Hle_low #Hlt_high destruct
1194           cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta)
1195           [ 1,3,5: >Z_addition_bv_commute try @refl
1196                    @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l
1197                    @Hlt_high
1198           ]
1199           #Hsum_split
1200           cut (Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta)) < high (blocks m1' b1) + Zoo delta)
1201           [ 1,3,5: >Hsum_split @monotonic_Zlt_Zplus_l assumption ]
1202           #Hlt_aux @(Zlt_to_Zle_to_Zlt … Hlt_aux Hhigh)
1203       ]
1204    ]
1205    -Hno_interference
1206    #Hvalid_ptr2
1207    (* reformulate the goals in an induction friendly way *)       
1208    [ cut (∃bvals. loadn m2
1209                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
1210                       (typesize (typ_of_type (Tint sz sg))) = Some ? bvals ∧
1211                   (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef)))
1212      [ 2: * #bvals * #Hloadn * #Heq destruct (Heq)
1213           whd in match (load_value_of_type ????);
1214           >Hloadn normalize nodelta try @refl
1215           cases bvals in Heq; try //
1216           #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?);
1217           #Heq destruct (Heq) try @refl ]
1218    | cut (∃bvals. loadn m2
1219                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
1220                       (typesize (typ_of_type (Tpointer ptr_ty))) = 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 (Tcomp_ptr id))) = 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    ]
1239    cases (valid_pointer_to_Prop … Hvalid') -Hvalid' * #HA #HB #HC
1240    cases (valid_pointer_to_Prop … Hvalid_ptr2) -Hvalid_ptr2 * #HD
1241    whd in match (offset_plus ??); #HE #HF
1242    cases Himpl1 cases Himpl2 -Himpl1 -Himpl2
1243    >unfold_low_bound >unfold_low_bound >unfold_high_bound >unfold_high_bound
1244    * #HG #HH * #HI #HJ * #HK #HL * #HM #HN
1245    lapply (alloc_properties … Halloc) * * #HO #HP #Hsrc_undef destruct (HO HP)
1246    cases (some_inversion ????? Hload)
1247    #bevals *
1248    #Hloadn #_ lapply Hloadn -Hloadn
1249    whd in match (typesize ?);
1250    [ generalize in match (S (pred_size_intsize sz));
1251    | generalize in match (S (S O));
1252    | generalize in match (S (S O)); ]
1253    #typesize
1254    lapply HE lapply HF lapply HB lapply HC
1255    -HE -HF -HB -HC
1256    lapply bevals
1257    lapply off1
1258    elim typesize
1259    [ 1,3,5:
1260      #off #bevals #HC #HB #HF #HE #_ %{[ ]} @conj try @refl
1261      %1 @refl
1262    | *:
1263      #n #Hind #off #bevals #HC #HB #HF #HE #Hloadn
1264      cases (some_inversion ????? Hloadn) -Hloadn
1265      #bval1 * #Hbeloadv_eq #Hloadn
1266      cases (some_inversion ????? Hloadn) -Hloadn
1267      whd in match (shift_pointer ???);
1268      whd in match (shift_offset ???);
1269      #bevals1 * #Hloadn #Hbevals'
1270      whd in match (loadn ???);
1271      whd in match (beloadv ??);
1272      >(Zlt_to_Zltb_true … HD) normalize nodelta
1273      >(Zle_to_Zleb_true … HE)
1274      >(Zlt_to_Zltb_true … HF) normalize nodelta
1275      lapply (Hundef_zone (Z_of_unsigned_bitvector ? (addition_n offset_size (offv off) (offv delta))) ??)
1276      [ 1,4,7: >Z_addition_bv_commute
1277          [ 2,4,6: @(transitive_Zlt … Hno_overflow)
1278                   @(monotonic_Zlt_Zplus_l) assumption
1279          | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ]
1280          | 2,5,8: >Z_addition_bv_commute
1281             [ 2,4,6: @(transitive_Zlt … Hno_overflow)
1282                      @(monotonic_Zlt_Zplus_l) assumption
1283             | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ]
1284      ]
1285      #Hcontents_undef
1286      cases n in Hind Hloadn;
1287      [ 1,3,5: #_ normalize in match (loadn ???); normalize nodelta #Heq destruct
1288               >Hcontents_undef %{[BVundef]} @conj try @refl %2 @refl ]
1289      #n' #Hind #Hloadn
1290      lapply Hloadn #Hloadn'
1291      cases (some_inversion ????? Hloadn') -Hloadn'
1292      #bval * whd in match (beloadv ??);
1293      >(Zlt_to_Zltb_true … HA) normalize nodelta #Hbeloadv
1294      cases (if_opt_inversion ???? Hbeloadv) -Hbeloadv #Hbounds
1295      cases (andb_inversion … Hbounds) -Hbounds #Hle1 #Hlt1 #Hcontents1 #_
1296      lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ????)
1297      (* lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ???? Hloadn) *)
1298      [ 1,6,11:
1299        @(transitive_Zle ??? HE)
1300        <associative_addition_n
1301        >(commutative_addition_n ? (sign_ext ???) (offv delta))
1302        >associative_addition_n
1303        >(Z_addition_bv_commute ?? (sign_ext ???))
1304        [ 2,4,6: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???));
1305                 >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O
1306                 @(Zle_to_Zlt_to_Zlt … HJ) @Zlt_to_Zle @HF
1307        | 1,3,5: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???));
1308                 >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O @Zsucc_le
1309        ]
1310      | 2,7,12:
1311        @(Zlt_to_Zle_to_Zlt ??? ? Hhigh)
1312        >Z_addition_bv_commute
1313        [ 2,4,6: @(transitive_Zlt … Hno_overflow)
1314                 @(monotonic_Zlt_Zplus_l) @(Zltb_true_to_Zlt … Hlt1)
1315        | 1,3,5: @monotonic_Zlt_Zplus_l @(Zltb_true_to_Zlt … Hlt1) ]
1316      | 3,8,13:
1317        @(Zleb_true_to_Zle … Hle1)
1318      | 4,9,14:
1319        @(Zltb_true_to_Zlt … Hlt1)
1320      ]
1321      -Hind #Hind lapply (Hind Hloadn)
1322      * #bevals2 * #Hloadn2 #Hbe_to_fe
1323      whd in match (shift_pointer ???);
1324      whd in match (shift_offset ???);
1325      cases Hbe_to_fe
1326      [ 1,3,5: #Heq destruct (Heq)
1327        %{(contents (blocks m2 b2)
1328             (Z_of_unsigned_bitvector offset_size
1329              (addition_n offset_size (offv off) (offv delta)))
1330               ::[ ])}
1331        <associative_addition_n
1332        >(commutative_addition_n ? (offv delta))
1333        >associative_addition_n
1334        >Hloadn2 normalize nodelta @conj try @refl %2
1335        >Hcontents_undef @refl
1336      | *: #Hhd_empty
1337        %{(contents (blocks m2 b2)
1338             (Z_of_unsigned_bitvector offset_size
1339              (addition_n offset_size (offv off) (offv delta)))
1340               :: bevals2)}
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      ]
1347    ]
1348  ]
1349| #b lapply (alloc_valid_new_block … Halloc) @(eq_block_elim … new_block b)
1350  [ #Heq destruct #Ha #Hb @False_ind @(absurd … Ha Hb)
1351  | #Hneq #Hvalid_new #Hnot_valid normalize nodelta
1352    cut (¬valid_block m1 b)
1353    [ cases m1 in Halloc; #cont #next #Hnext
1354      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1355      % #H cases Hnot_valid #H' @H'
1356      whd whd in H; /2 by transitive_Zlt/ ]
1357    @ (mi_freeblock … Hinj) ]
1358| * #blo #off #p' #Hvalid1
1359  @(eq_block_elim … new_block blo)
1360  [ #Heq whd in match (pointer_translation ??);
1361    destruct (Heq) >eq_block_b_b normalize nodelta
1362    lapply (alloc_properties … Halloc) * *
1363    #Hlow_eq #Hhigh_eq #Hundef destruct
1364    cases (valid_pointer_to_Prop … Hvalid1) *
1365    #Hvalid_block1 #Hlow1 #Hhigh1
1366    #Heq destruct (Heq) @valid_pointer_of_Prop
1367    @conj try @conj   
1368    [ @Hvalid
1369    | @(transitive_Zle … Hlow)
1370      >Z_addition_bv_commute
1371      [ @monotonic_Zle_Zplus_l assumption
1372      | @(transitive_Zlt … Hno_overflow)
1373        @monotonic_Zlt_Zplus_l assumption
1374      ]
1375    | @(Zlt_to_Zle_to_Zlt … Hhigh)
1376      >Z_addition_bv_commute
1377      [ @monotonic_Zlt_Zplus_l assumption
1378      | @(transitive_Zlt … Hno_overflow)
1379        @monotonic_Zlt_Zplus_l assumption
1380      ]
1381    ]
1382  | #Hblocks_neq whd in match (pointer_translation ??);
1383    >(neq_block_eq_block_false … Hblocks_neq) normalize nodelta
1384    #Htranslate
1385    lapply (mi_valid_pointers ??? Hinj (mk_pointer blo off) p' ?)
1386    [ @(alloc_valid_pointer_conservation … Halloc … Hvalid1) @sym_neq assumption ]
1387    #H @H
1388    assumption
1389  ]
1390| #b #b' #o'
1391  @(eq_block_elim … new_block b)
1392  [ #Heq destruct (Heq) normalize nodelta
1393    #Heq destruct (Heq) @Hvalid
1394  | #Hneq normalize nodelta
1395    #Hembed
1396    @(mi_nodangling ??? Hinj … Hembed)
1397  ]
1398| #b #b' #o'
1399  @(eq_block_elim … new_block b)
1400  [ #Heq normalize nodelta #Heq' destruct (Heq Heq')
1401    @Hregion
1402  | #Hneq normalize nodelta #Hembed
1403    @(mi_region … Hinj … Hembed)
1404  ]
1405| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
1406  cases (alloc_properties … Halloc) * #Hlow1 #Hhigh1 #Hundef
1407  @(eq_block_elim … new_block b1)
1408  normalize nodelta
1409  [ #Heq #Heq' destruct
1410    >(neq_block_eq_block_false … Hneq) normalize nodelta
1411    #Hembed
1412(*    lapply (alloc_bounds_conservation … Halloc) …  *)
1413    @(eq_block_elim … b1' b2') normalize nodelta
1414    [ #Heq destruct (Heq)
1415      lapply (Hno_interference b2 ? (sym_neq ??? Hneq) Hembed) *
1416      cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq)) #HA #HB
1417      [ #H %1 %1 %2
1418        >HB @H
1419      | #H %1 %1 %1 >HA @H ]
1420    | #Hneq @I ]
1421  | #Hneq' #Hembed
1422    @(eq_block_elim … new_block b2) normalize nodelta
1423    [ #Heq #Heq' destruct
1424      @(eq_block_elim … b1' b2') normalize nodelta
1425      [ #Heq destruct (Heq)
1426        lapply (Hno_interference b1 ? Hneq Hembed) *
1427        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq')) #HA #HB
1428        [ #H %1 %1 %1
1429          >HB @H
1430        | #H %1 %1 %2 >HA @H ]
1431      | #Hneq @I ]
1432    | #Hneq'' #Hembed'
1433      @(eq_block_elim … b1' b2') normalize nodelta
1434      [ #Heq'' destruct (Heq'')
1435        lapply (mi_nonalias … Hinj … Hneq … Hembed Hembed')
1436        >eq_block_b_b normalize nodelta
1437        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq''))
1438        #HA #HB
1439        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq'))
1440        #HC #HD
1441        * [ * [ * | ] | ]
1442        [ #Hle %1 %1 %1 >HD >HA @Hle
1443        | #Hle %1 %1 %2 >HB >HC @Hle
1444        | #Hempty %1 %2 whd in Hempty ⊢ %; >HD >HC
1445          @Hempty
1446        | #Hempty %2 whd in Hempty ⊢ %; >HB >HA @Hempty
1447        ]
1448      | #_ @I
1449      ]
1450    ]
1451  ]
1452| #b whd
1453  @(eq_block_elim … new_block b)
1454  normalize nodelta
1455  #Hneq destruct (Hneq)
1456  [ @conj try @conj try assumption
1457  | lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
1458    cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq))
1459    #HA #HB
1460    cases (E b) normalize nodelta try //
1461    * #blo #off normalize nodelta * * #HA' #HB' #HC'
1462    @conj try @conj whd in HA'; whd in HB';
1463    whd in match (block_implementable_bv ??);
1464    [ 1,2: >HA >HB assumption
1465    | *: >HB assumption ]
1466  ]
1467] qed.   
1468
1469(* -------------------------------------- *)
1470(* Lemmas pertaining to [free] *)
1471
1472(* Lemma 46 by Leroy&Blazy *)
1473lemma free_load_sim_ptr_m1 :
1474  ∀E:embedding.
1475  ∀m1,m2,m1'.
1476  load_sim_ptr E m1 m2 →
1477  ∀b. free m1 b = m1' →
1478      load_sim_ptr E m1' m2.     
1479#E #m1 #m2 #m1' #Hinj #b #Hfree
1480whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
1481cases ty
1482[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1483| #structname #fieldspec | #unionname #fieldspec | #id ]
1484[ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1485             normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl
1486             %4 @Htrans ]
1487#Hload <Hfree in Hload; #Hload lapply (load_value_of_type_free_load_value_of_type … Hload)
1488#Hload' @(Hinj … Hload') //
1489<Hfree in Hvalid; @valid_free_to_valid
1490qed.
1491
1492(* lemma 47 of L&B *)
1493
1494lemma free_loadn_sim_ptr_m2 :
1495  ∀sz,m,b,b',o,res.
1496   b ≠ b' →
1497   loadn m (mk_pointer b' o) sz = Some ? res →
1498   loadn (free m b) (mk_pointer b' o) sz = Some ? res.
1499#sz
1500elim sz
1501[ normalize //
1502| #sz' #Hind #m #b #b' #o #res #Hneq whd in ⊢ ((??%?) → (??%?));
1503  #H cases (some_inversion ????? H) -H #beres *
1504  #Hbeloadv #Hloadn
1505  lapply (beloadv_free_beloadv2 m b ??? Hbeloadv)
1506  [ @sym_neq @Hneq ]
1507  #Hbeloadv' >Hbeloadv' normalize nodelta
1508  cases (some_inversion ????? Hloadn) -Hloadn #bevals * #Hloadn
1509  #Heq destruct (Heq)
1510  >(Hind … Hneq Hloadn) normalize nodelta @refl
1511] qed. 
1512
1513lemma free_load_sim_ptr_m2 :
1514  ∀E:embedding.
1515  ∀m1,m2,m2'.
1516  load_sim_ptr E m1 m2 →
1517  ∀b. free m2 b = m2' →
1518      (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
1519      load_sim_ptr E m1 m2'.     
1520#E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped
1521whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
1522cases ty
1523[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1524| #structname #fieldspec | #unionname #fieldspec | #id ]
1525[ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1526             normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl
1527             %4 @Htrans ]
1528lapply Htrans -Htrans lapply Hsim -Hsim lapply Hfree -Hfree
1529cases m2 #contents2 #next2 #Hnext2
1530whd in ⊢ ((??%?) → ?); #Hm2' destruct
1531#Hsim #Htrans
1532cases (some_inversion ????? Htrans) * #b2' #off2' * #Hembed normalize nodelta
1533#Heq destruct (Heq) #Hload
1534lapply (Hsim … Hvalid … Htrans … Hload)
1535* #v2' * #Hload_before_free #Hvalue_eq
1536@(eq_block_elim … b2 b)
1537[ 1,3,5: #Heq destruct
1538         lapply (Hunmapped b1 off2' Hembed) *
1539         [ 1,3,5: #Hnot_valid lapply (valid_pointer_to_Prop … Hvalid)
1540                  -Hvalid whd in match (valid_block ??) in Hnot_valid;
1541                  * * #Hvalid #_ #_ @False_ind
1542                  cases Hnot_valid #H @H @Hvalid
1543         | *: whd in ⊢ (% → ?); #Hempty
1544              lapply (valid_pointer_to_Prop … Hvalid)
1545              -Hvalid * * #_ #Hlow #Hhigh
1546              cut ((low_bound m1 b1 < high_bound m1 b1))
1547              [ 1,3,5: /2 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle_to_Zlt/ ]
1548              #Hnonempty @False_ind -Hlow -Hhigh
1549              lapply (Zlt_to_Zle_to_Zlt … Hnonempty Hempty)
1550              #H cases (irreflexive_Zlt (low_bound m1 b1)) #H' @H' @H ]
1551| *: #Hneq %{v2'} @conj try assumption
1552     whd in match (load_value_of_type ????) in Hload_before_free:(??%?) ⊢ (??%?);
1553     cases (some_inversion ????? Hload_before_free) -Hload_before_free
1554     #bevals * #Hloadn #Heq
1555     >(free_loadn_sim_ptr_m2 … Hloadn) normalize nodelta
1556     try assumption @sym_neq @Hneq
1557] qed.     
1558
1559lemma free_block_is_empty :
1560  ∀m,m',b,b'.
1561  block_region b = block_region b' →
1562  block_is_empty m b →
1563  free m b' = m' →
1564  block_is_empty m' b.
1565* #contents #nextblock #Hpos
1566#m' #b #b' #Hregions_eq
1567#HA #HB normalize in HB; <HB whd
1568normalize >Hregions_eq cases (block_region b') normalize nodelta
1569@(eqZb_elim … (block_id b) (block_id b'))
1570[ 1,3: #Heq normalize nodelta //
1571| 2,4: #Hneq normalize nodelta @HA ]
1572qed.
1573
1574lemma high_bound_freed_block :
1575  ∀m,b. high_bound (free m b) b = OZ.
1576#m #b normalize
1577cases (block_region b) normalize
1578>eqZb_z_z normalize @refl
1579qed.
1580
1581lemma low_bound_freed_block :
1582  ∀m,b. low_bound (free m b) b = (pos one).
1583#m #b normalize
1584cases (block_region b) normalize
1585>eqZb_z_z normalize @refl
1586qed.
1587
1588(* Lemma 49 in Leroy&Blazy *)
1589lemma free_non_aliasing_m1 :
1590  ∀E:embedding.
1591  ∀m1,m2,m1'.
1592  memory_inj E m1 m2 →
1593  ∀b. free m1 b = m1' →
1594      non_aliasing E m1'.
1595(* The proof proceeds by a first case analysis to see wether b lives in the
1596   same world as the non-aliasing blocks (if not : trivial), in this case
1597   we proceed to a second case analysis on the non-aliasing hypothesis in
1598   memory_inj. *)
1599#E #m1 #m2 #m1' #Hinj #b #Hfree
1600whd
1601#b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
1602#Hembed1 #Hembed2
1603@(eq_block_elim … b1' b2') normalize nodelta
1604[ 2: try // ]
1605#Hblocks_eq
1606lapply Hembed2 -Hembed2
1607lapply Hembed1 -Hembed1
1608lapply Hblocks_eq -Hblocks_eq
1609(*cases b1' #r1' #bid1'
1610  cases b2' #r2' #bid2' *)
1611#Heq destruct (Heq)
1612generalize in match b2';
1613#target #Hembed1 #Hembed2
1614lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2)
1615>eq_block_b_b normalize nodelta
1616normalize nodelta <Hfree
1617@(eq_block_elim … b1 b)
1618[ #Heq destruct (Heq) #Hcase
1619  %1 %2 whd
1620  >high_bound_freed_block >low_bound_freed_block
1621  //
1622| #Hneq1 @(eq_block_elim … b2 b)
1623  [ #Heq destruct (Heq) #Hcase
1624    %2 whd
1625    >high_bound_freed_block >low_bound_freed_block
1626    // ] ]
1627#Hneq2
1628>unfold_high_bound >unfold_high_bound >unfold_high_bound >unfold_high_bound
1629>unfold_low_bound >unfold_low_bound >unfold_low_bound >unfold_low_bound
1630<(high_free_eq … Hneq1) <(high_free_eq … Hneq2)
1631<(low_free_eq … Hneq1) <(low_free_eq … Hneq2)
1632*
1633[ 2: #H %2 whd >unfold_high_bound >unfold_low_bound
1634     <(low_free_eq … Hneq2) <(high_free_eq … Hneq2) @H ]
1635*
1636[ 2: #H %1%2 whd >unfold_high_bound >unfold_low_bound
1637     <(low_free_eq … Hneq1) <(high_free_eq … Hneq1) @H ]
1638* #H
1639[ %1 %1 %1 @H
1640| %1 %1 %2 @H ]
1641qed.
1642
1643(* Extending lemma 46 and 49 to memory injections *)
1644lemma free_memory_inj_m1 :
1645  ∀E:embedding.
1646  ∀m1,m2,m1'.
1647  memory_inj E m1 m2 →
1648  ∀b. free m1 b = m1' →
1649      memory_inj E m1' m2.
1650#E #m1 #m2 #m1' #Hinj #b #Hfree
1651cases Hinj
1652#Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable
1653% try assumption
1654[ @(free_load_sim_ptr_m1 … Hload_sim … Hfree)
1655| #bb #Hnot_valid lapply (Hfreeblock bb) #HA @HA % #HB
1656  cases Hnot_valid #HC @HC <Hfree @HB
1657| #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation)
1658  <Hfree in Hvalid_m1'; @valid_free_to_valid
1659| @(free_non_aliasing_m1 … Hinj … Hfree)
1660| #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?);
1661  cases (E bb) normalize nodelta try //
1662  * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj
1663  try //
1664  @(eq_block_elim … b bb)
1665  [ 2,4:
1666      #Hneq destruct (Hfree)
1667      whd in match (free ??);
1668      whd >unfold_low_bound >unfold_high_bound
1669      whd in match (update_block ?????); >(not_eq_block … (sym_neq ??? Hneq))
1670      try @conj normalize nodelta cases HA try //
1671  | 1,3:
1672      #H destruct whd in match (free ??);
1673      whd [ >unfold_low_bound ] >unfold_high_bound
1674      whd in match (update_block ?????); >eq_block_b_b
1675      normalize nodelta try @conj try // % try //
1676  ]
1677] qed.
1678
1679(* Lifting lemma 47 to memory injs - note that we require a much stronger condition
1680 * on the freed block : no block of m1 can map to it. Not even an invalid block or
1681 * an empty one.
1682 * XXX this lemma is not given in Leroy&Blazy, and unless future developments requires
1683 * it I will comment it out. XXX *)
1684lemma free_memory_inj_m2 :
1685  ∀E:embedding.
1686  ∀m1,m2,m2'.
1687  memory_inj E m1 m2 →
1688  ∀b. free m2 b = m2' →
1689      (∀b1,delta. E b1 = Some ? 〈b, delta〉 →
1690      (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 
1691      memory_inj E m1 m2'.
1692#E #m1 #m2 #m2' #Hinj #b #Hfree #b_not_mapped
1693% cases Hinj try //
1694#Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl
1695[ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed
1696  @(b_not_mapped … b1 delta Hembed)
1697| @Hfreeblock
1698| * #bp #op #p' #Hp_valid #Hptr_trans
1699  @(eq_block_elim … (pblock p') b)
1700  [ #Heq lapply (Hvalid … Hp_valid Hptr_trans) #Hp_valid' destruct (Heq)
1701    cases (some_inversion ????? Hptr_trans)
1702    * #bp' #op' * #Hembed normalize nodelta #Heq destruct (Heq)
1703    cases (b_not_mapped … Hembed)
1704    [ #Hnot_valid lapply (Hfreeblock … Hnot_valid) >Hembed #Habsurd destruct (Habsurd)
1705    | #Hempty @False_ind lapply (valid_pointer_to_Prop … Hp_valid) * * #_
1706      whd in Hempty; #Hle #Hlt
1707      lapply (Zlt_to_Zle_to_Zlt … Hlt Hempty) #Hlt2
1708      lapply (Zlt_to_Zle_to_Zlt … Hlt2 Hle) #Hlt3
1709      @(absurd … Hlt3 (irreflexive_Zlt ?)) ]
1710  | #Hneq lapply (Hvalid … Hp_valid Hptr_trans) <Hfree #HA
1711    @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … HA) -HA * *
1712    #HA #HB #HC @conj try @conj try assumption
1713    [ >unfold_low_bound <(low_free_eq m2 ?? Hneq) @HB
1714    | >unfold_high_bound <(high_free_eq m2 ?? Hneq) @HC ]
1715  ]
1716| #bb #b' #o' #Hembed
1717  lapply (Hnodangling … Hembed) <Hfree //
1718| @Hregion
1719| #bb lapply (Himpl bb)
1720  whd in ⊢ (% → %); cases (E bb) normalize nodelta try //
1721  * #BLO #OFF normalize nodelta * * destruct (Hfree)
1722  #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption
1723  cases Hbb try // #Hlow_bb #Hhigh_bb
1724  [ >unfold_low_bound
1725  | *: >unfold_high_bound ]
1726  whd in match (update_block ?????);
1727  @(eq_block_elim … BLO b)
1728  #H [ 1,3,5: destruct (H) normalize nodelta try //
1729               @conj try //
1730     | *: normalize nodelta cases HBLO try // ]
1731] qed.
1732
1733
1734(* Lemma 64 of L&B on [freelist] *)
1735lemma freelist_memory_inj_m1_m2 :
1736  ∀E:embedding.
1737  ∀m1,m2,m1',m2'.
1738  memory_inj E m1 m2 →
1739  ∀blocklist,b2.
1740  (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
1741  free m2 b2 = m2' →
1742  free_list m1 blocklist = m1' →
1743  memory_inj E m1' m2'.
1744#E #m1 #m2 #m1' #m2' #Hinj #blocklist #b2 #Hnot_mapped #Hfree2 #Hfree_list
1745cut (memory_inj E m1' m2)
1746[ <Hfree_list -Hfree_list
1747  -Hnot_mapped
1748  lapply Hinj -Hinj
1749  lapply m1 -m1
1750  elim blocklist
1751  [ #m1 #Hinj @Hinj
1752  | #hd #tl #Hind #m1 #Hinj
1753    @(free_memory_inj_m1 ? (free_list m1 tl) ? (free (free_list m1 tl) hd) ? hd)
1754    try @refl @(Hind … Hinj)
1755  ]
1756]
1757#Hinj'
1758@(free_memory_inj_m2 … Hinj' … Hfree2)
1759#b1 #delta #Hembed %2
1760lapply (Hnot_mapped … Hembed)
1761lapply Hfree_list -Hfree_list
1762generalize in match m1';
1763generalize in match m1;
1764elim blocklist
1765[ #m1 #m1' whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @False_ind
1766| #hd #tl #Hind #m1 #m1' #Hfree_list *
1767  [ #Heq destruct whd
1768    whd in match (free_list ??);
1769    >unfold_high_bound >unfold_low_bound
1770    whd in match (update_block ?????); >eq_block_b_b
1771    normalize nodelta @I
1772  | >free_list_cons in Hfree_list; #Hfree_list #H
1773    <Hfree_list whd cases m1 #contents2 #n2 #Hn2
1774    >unfold_high_bound >unfold_low_bound
1775    whd in match (update_block ?????);
1776    @(eq_block_elim … b1 hd)
1777    [ #Heq normalize nodelta @I
1778    | #Hneq normalize nodelta @(Hind … (mk_mem contents2 n2 Hn2) … (refl ??) … H)
1779    ]
1780  ]
1781] qed.
1782
1783(* ---------------------------------------------------------- *)
1784(* Lemma 40 of the paper of Leroy & Blazy on the memory model
1785 * and store-related lemmas *)
1786
1787lemma bestorev_beloadv_conservation :
1788  ∀mA,mB,wb,wo,v.
1789    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1790    ∀rb,ro. eq_block wb rb = false →
1791    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
1792#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
1793whd in ⊢ (??%%);
1794elim mB in Hstore; #contentsB #nextblockB #HnextblockB
1795normalize in ⊢ (% → ?);
1796cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
1797[ 2: #Habsurd destruct (Habsurd) ]
1798cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo))
1799       then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) 
1800       else false) normalize nodelta
1801[ 2: #Habsurd destruct (Habsurd) ]
1802#Heq destruct (Heq)
1803cases (Zltb (block_id rb) (nextblock mA)) normalize nodelta try //
1804cut (eqZb (block_id rb) (block_id wb) = false)
1805[ >eqZb_symmetric @Hblock_neq ]
1806#Heqzb >Heqzb normalize nodelta @refl
1807qed.
1808
1809(* lift [bestorev_beloadv_conservation to [loadn] *)
1810lemma bestorev_loadn_conservation :
1811  ∀mA,mB,n,wb,wo,v.
1812    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1813    ∀rb,ro. eq_block wb rb = false →
1814    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
1815#mA #mB #n
1816elim n
1817[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
1818| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
1819     whd in ⊢ (??%%);
1820     >(bestorev_beloadv_conservation … Hstore … Hneq)
1821     >(Hind … Hstore … Hneq) @refl
1822] qed.
1823
1824(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
1825lemma bestorev_load_value_of_type_conservation :
1826  ∀mA,mB,wb,wo,v.
1827    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1828    ∀rb,ro. eq_block wb rb = false →
1829    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1830#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
1831cases ty
1832[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1833| #structname #fieldspec | #unionname #fieldspec | #id ]
1834//
1835[ 1: elim sz ]
1836whd in ⊢ (??%%);
1837>(bestorev_loadn_conservation … Hstore … Hneq) @refl
1838qed.
1839
1840(* lift [bestorev_load_value_of_type_conservation] to storen *)
1841lemma storen_load_value_of_type_conservation :
1842  ∀l,mA,mB,wb,wo.
1843    storen mA (mk_pointer wb wo) l = Some ? mB →
1844    ∀rb,ro. eq_block wb rb = false →
1845    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1846#l elim l
1847[ 1: #mA #mB #wb #wo normalize #Heq destruct //
1848| 2: #hd #tl #Hind #mA #mB #wb #wo #Hstoren
1849     cases (some_inversion ????? Hstoren) #mA' * #Hbestorev #Hstoren'
1850     whd in match (shift_pointer ???) in Hstoren':(??%?); #rb #ro #Hneq_block #ty
1851     lapply (Hind ???? Hstoren' … ro … Hneq_block ty) #Heq1
1852     lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2
1853     //
1854] qed.
1855
1856lemma store_value_of_type_load_value_of_type_conservation :
1857  ∀ty,mA,mB,wb,wo,v.
1858    store_value_of_type ty mA wb wo v = Some ? mB →
1859    ∀rb,ro. eq_block wb rb = false →
1860    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1861#ty #mA #mB #wb #wo #v #Hstore #rb #ro #Heq_block
1862cases ty in Hstore;
1863[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1864| #structname #fieldspec | #unionname #fieldspec | #id ]
1865[ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct ]
1866whd in ⊢ ((??%?) → ?); #Hstoren
1867@(storen_load_value_of_type_conservation … Hstoren … Heq_block)
1868qed.
1869
1870definition typesize' ≝ λty. typesize (typ_of_type ty).
1871
1872lemma storen_load_value_of_type_conservation_in_block_high :
1873  ∀E,mA,mB,mC,wo,l.
1874    memory_inj E mA mB →
1875    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
1876    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
1877    high_bound mA b1 + Zoo delta < Zoo wo →
1878    ∀ty,off.
1879       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
1880       low_bound … mA b1 ≤ Zoo off →
1881       Zoo off < high_bound … mA b1 →
1882       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
1883       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
1884#E #mA #mB #mC #wo #data #Hinj #blo #Hstoren #b1 #delta #Hembed #Hhigh #ty
1885(* need some stuff asserting that if a ptr is valid at the start of a write it's valid at the end. *)
1886cases data in Hstoren;
1887[ 1: normalize in ⊢ (% → ?); #Heq destruct //
1888| 2: #xd #data ]
1889#Hstoren
1890cases ty
1891[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1892| #structname #fieldspec | #unionname #fieldspec | #id ]#off #Hofflt #Hlow_load #Hhigh_load try @refl
1893whd in match (load_value_of_type ????) in ⊢ (??%%);
1894[ 1: lapply (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hbefore #Hafter
1895     lapply Hofflt -Hofflt lapply Hlow_load -Hlow_load lapply Hhigh_load -Hhigh_load
1896     lapply off -off whd in match typesize'; normalize nodelta     
1897     generalize in match (typesize ?); #n elim n try //
1898     #n' #Hind #o #Hhigh_load #Hlow_load #Hlt
1899     whd in match (loadn ???) in ⊢ (??%%);
1900     whd in match (beloadv ??) in ⊢ (??%%);
1901     cases (valid_pointer_to_Prop … Hbefore) * #HltB_store #HlowB_store #HhighB_store
1902     cases (valid_pointer_to_Prop … Hafter) * #HltC_store #HlowC_store #HhighC_store
1903     >(Zlt_to_Zltb_true … HltB_store) >(Zlt_to_Zltb_true … HltC_store) normalize nodelta
1904     cut (Zleb (low (blocks mB blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
1905     [ 1: (* Notice that:
1906                low mA b1 ≤ o < high mA b1
1907             hence, since E b1 = 〈blo, delta〉 with delta >= 0
1908                low mB blo ≤ (low mA b1 + delta) ≤ o+delta < (high mA b1 + delta) ≤ high mB blo *)
1909          @cthulhu ]
1910     #HA >HA >andb_lsimpl_true -HA
1911     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mB blo)) = true)
1912     [ 1: (* Same argument as above *) @cthulhu ]
1913     #HA >HA normalize nodelta -HA
1914     cut (Zleb (low (blocks mC blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
1915     [ 1: (* Notice that storen does not modify the bounds of a block. Related lemma present in [MemProperties].
1916             This cut follows from this lemma (which needs some info on the size of the data written, which we
1917             have but must make explicit) and from the first cut. *)
1918          @cthulhu ]         
1919     #HA >HA >andb_lsimpl_true -HA
1920     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mC blo)) = true)
1921     [ 1: (* Same argument as above *) @cthulhu ]
1922     #HA >HA normalize nodelta -HA
1923     normalize in match (bitvector_of_nat ??); whd in match (shift_pointer ???);
1924     whd in match (shift_offset ???); >commutative_addition_n >associative_addition_n
1925     lapply (Hind (mk_offset (addition_n offset_size (sign_ext 2 ? [[false; true]]) (offv o))) ???)
1926     [ 1: (* Provable from Hlt *) @cthulhu
1927     | 2: (* Provable from Hlow_load, need to make a "succ" commute from bitvector to Z *) @cthulhu
1928     | 3: (* Provable from Hlt, again *) @cthulhu ]
1929     cases (loadn mB (mk_pointer blo
1930              (mk_offset (addition_n ? (addition_n ?
1931                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
1932     normalize nodelta                 
1933     cases (loadn mC (mk_pointer blo
1934              (mk_offset (addition_n ? (addition_n ?
1935                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
1936     normalize nodelta try //
1937     [ 1,2: #l #Habsurd destruct ]
1938     #l1 #l2 #Heq
1939     cut (contents (blocks mB blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) =
1940          contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
1941     [ 1: (* Follows from Hhigh, indirectly *) @cthulhu ]
1942     #Hcontents_eq >Hcontents_eq whd in match (be_to_fe_value ??) in ⊢ (??%%);
1943     cases (contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
1944     normalize nodelta try //
1945     (* Ok this is going to be more painful than what I thought. *)
1946     @cthulhu
1947| *: @cthulhu
1948] qed.
1949
1950lemma storen_load_value_of_type_conservation_in_block_low :
1951  ∀E,mA,mB,mC,wo,l.
1952    memory_inj E mA mB →
1953    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
1954    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
1955    Zoo wo < low_bound mA b1 + Zoo delta →
1956    ∀ty,off.
1957       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
1958       low_bound … mA b1 ≤ Zoo off →
1959       Zoo off < high_bound … mA b1 →
1960       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
1961       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
1962@cthulhu
1963qed.
1964
1965(* Writing in the "extended" part of a memory preserves the underlying injection. *)
1966lemma bestorev_memory_inj_to_load_sim :
1967  ∀E,mA,mB,mC.
1968  ∀Hext:memory_inj E mA mB.
1969  ∀block2. ∀i : offset. ∀ty : type.
1970  (∀block1,delta.
1971    E block1 = Some ? 〈block2, delta〉 →
1972    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
1973  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
1974  load_sim_ptr E mA mC.
1975#E #mA #mB #mC #Hinj #block2 #i #storety
1976cases storety
1977[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1978| #structname #fieldspec | #unionname #fieldspec | #id ] #Hout #storeval #Hstore whd
1979#b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value
1980whd in Hstore:(??%?);
1981[  1,5,6,7,8: destruct ]
1982[ 1:
1983lapply (mi_inj … Hinj … Hvalid … Hptr_trans … Hload_value)
1984lapply Hload_value -Hload_value
1985cases ty
1986[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
1987| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
1988#Hload_value
1989(* Prove that the contents of mB where v1 was were untouched. *)
1990* #readval' * #Hload_value2 #Hvalue_eq %{readval'} @conj try assumption
1991cases (some_inversion ????? Hptr_trans) * #b2' #delta' * #Hembed -Hptr_trans normalize nodelta
1992#Heq destruct (Heq)
1993@(eq_block_elim  … b2 block2)
1994[ 2,4,6,8: #Hblocks_neq <Hload_value2 @sym_eq @(storen_load_value_of_type_conservation … Hstore)
1995           @not_eq_block @sym_neq @Hblocks_neq
1996| 1,3,5,7: #Heq destruct (Heq) lapply (Hout … Hembed) *
1997           [ 1,3,5,7: #Hhigh <Hload_value2 -Hload_value2 @sym_eq
1998                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
1999                      * * #Hlt #Hlowb_off1 #Hhighb_off1
2000                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
2001                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
2002                      @(storen_load_value_of_type_conservation_in_block_high … Hinj … Hstore … Hembed)
2003                      try //
2004                      (* remaining stuff provable from Hload_value  *)
2005                      @cthulhu
2006           | 2,4,6,8: #Hlow <Hload_value2 -Hload_value2 @sym_eq
2007                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
2008                      * * #Hlt #Hlowb_off1 #Hhighb_off1
2009                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
2010                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
2011                      @(storen_load_value_of_type_conservation_in_block_low … Hinj … Hstore … Hembed)
2012                      try //
2013                      [ 1,3,5,7: (* deductible from Hlow + (sizeof ?) > 0 *) @cthulhu
2014                      | 2,4,6,8: (* deductible from Hload_value *) @cthulhu ]
2015           ]
2016]
2017| *: (* exactly the same proof as above  *) @cthulhu ]
2018qed.
2019
2020(* Lift the above result to memory_inj
2021 * This is Lemma 40 of Leroy & Blazy *)
2022lemma store_value_of_type_memory_inj_to_memory_inj :
2023  ∀E,mA,mB,mC.
2024  ∀Hext:memory_inj E mA mB.
2025  ∀block2. ∀i : offset. ∀ty : type.
2026  (∀block1,delta.
2027    E block1 = Some ? 〈block2, delta〉 →
2028    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
2029  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
2030  memory_inj E mA mC.
2031#E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore %
2032lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try //
2033cases Hinj #Hsim' #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption
2034[
2035  #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
2036  cases ty in Hstore;
2037  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2038  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2039  whd in ⊢ ((??%?) → ?);
2040  [ 1,4,5,6,7: #Habsurd destruct ]
2041  cases (fe_to_be_values ??)
2042  [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl
2043  | *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_
2044       @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh
2045       @conj try @conj try assumption >Hnext try //
2046       cases (Hbounds (pblock p')) #HA #HB
2047       whd in match (low_bound ??); whd in match (high_bound ??);
2048       >HA >HB try assumption
2049  ]
2050| lapply (mem_bounds_after_store_value_of_type … Hstore)
2051  * #Hnext_eq #Hb
2052  #b #b' #o' cases (Hb b') #Hlow_eq #Hhigh_eq #Hembed
2053  lapply (mi_nodangling … Hinj … Hembed)
2054  whd in match (valid_block ??) in ⊢ (% → %);
2055  >(Hnext_eq) try //
2056| #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %);
2057  cases (E b) try //
2058  * #BLO #OFF normalize nodelta * *
2059  #Hb #HBLO #Hbound try @conj try @conj try assumption
2060  lapply (mem_bounds_after_store_value_of_type … Hstore) *
2061  #_ #Hbounds
2062  cases (Hbounds BLO) #Hlow #Hhigh whd %
2063  [ >unfold_low_bound | >unfold_high_bound ]
2064  >Hlow >Hhigh cases HBLO try //
2065] qed.
2066
2067
2068(* ---------------------------------------------------------- *)
2069(* Lemma 41 of the paper of Leroy & Blazy on the memory model
2070 * and related lemmas *)
2071
2072(* The back-end might contain something similar to this lemma. *)
2073lemma be_to_fe_value_ptr :
2074  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
2075#b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid normalize nodelta
2076(*cases br normalize nodelta *) >eqZb_z_z normalize nodelta
2077cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
2078<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
2079* //
2080qed.
2081
2082lemma fe_to_be_values_length :
2083  ∀E,v1,v2,ty.
2084  value_eq E v1 v2 → |fe_to_be_values ty v1| = |fe_to_be_values ty v2|.
2085#E #v1 #v2 #ty #Hvalue_eq
2086@(value_eq_inversion … Hvalue_eq) //
2087qed.
2088
2089lemma value_eq_to_be_and_back_again :
2090  ∀E,ty,v1,v2.
2091  value_eq E v1 v2 →
2092  ast_typ_consistent_with_value ty v1 →
2093  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)).
2094#E #ty #v1 #v2 #Hvalue_eq
2095@(value_eq_inversion … Hvalue_eq) try //
2096[ 1: cases ty //
2097| 2: #sz #i cases ty
2098     [ 2: @False_ind
2099     | 1: #sz' #sg #H lapply H whd in ⊢ (% → ?); #Heq
2100          lapply (fe_to_be_to_fe_value_int … H) #H >H // ]
2101| 3: #p1 #p2 #Hembed cases ty
2102     [ 1: #sz #sg @False_ind
2103     | 2: #_
2104          cases p1 in Hembed; #b1 #o1
2105          cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H
2106          cases (some_inversion ????? H) * #b3 #o3 * #Hembed
2107          normalize nodelta #Heq >be_to_fe_value_ptr >be_to_fe_value_ptr
2108          destruct %4 whd in match (pointer_translation ??);
2109          >Hembed normalize nodelta @refl
2110     ]
2111] qed.
2112
2113(* ------------------------------------------------------------ *)
2114(* Lemma ?? of the paper of Leroy & Blazy on the memory model ? *)
2115
2116lemma storen_parallel_memory_exists :
2117  ∀E,m1,m2.
2118  memory_inj E m1 m2 →
2119  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
2120  ∀v1,v2. value_eq E v1 v2 →
2121  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
2122  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'.
2123(*        ∧ loadn m2' (mk_pointer b2 (offset_plus i delta)) (|fe_to_be_values ty v2|) = Some ? (fe_to_be_values ty v2).*)
2124#E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty
2125lapply (mi_valid_pointers … Hinj)
2126generalize in match m2;
2127generalize in match m1;
2128generalize in match i;
2129lapply (fe_to_be_values_length … ty Hvalue_eq)
2130generalize in match (fe_to_be_values ty v2);
2131generalize in match (fe_to_be_values ty v1);
2132#l1 elim l1
2133[ 1: #l2 #Hl2
2134     cut (l2 = [])
2135     [ cases l2 in Hl2; // #hd' #tl' normalize #Habsurd destruct ]
2136     #Hl2_empty >Hl2_empty #o #m1 #m2 #_ normalize /2 by ex_intro/
2137| 2: #hd1 #tl1 #Hind #l2 #Hlength
2138     cut (∃hd2,tl2.l2 = hd2::tl2 ∧ |tl1| = |tl2|)
2139     [ cases l2 in Hlength;
2140       [ normalize #Habsurd destruct
2141       | #hd2 #tl2 normalize #H %{hd2} %{tl2} @conj try @refl destruct (H) assumption ] ]
2142     * #hd2 * #tl2 * #Heq2 destruct (Heq2) #Hlen_tl
2143     #o #m1 #m2 #Hvalid_embed #Hstoren
2144     cases (some_inversion ????? Hstoren) #m1_tmp * #Hbestorev #Hstoren_tl
2145     lapply (Hvalid_embed (mk_pointer b1 o) (mk_pointer b2 (offset_plus o delta)) ??)
2146     [ 1: whd in match (pointer_translation ??);
2147          >Hembed normalize nodelta @refl
2148     | 2: @(bestorev_to_valid_pointer … Hbestorev) ]
2149     #Hvalid_ptr_m2
2150     whd in match (storen ???);
2151     lapply (valid_pointer_to_bestorev_ok m2 (mk_pointer b2 (offset_plus o delta)) hd2 Hvalid_ptr_m2)
2152     * #m2_tmp #Hbestorev2 >Hbestorev2 normalize nodelta
2153     whd in match (shift_pointer ???) in Hstoren_tl ⊢ %;
2154     whd in match (shift_offset ???) in Hstoren_tl ⊢ %;
2155     (*     normalize in match (sign_ext ???) in Hstoren_tl ⊢ %;*)
2156     cut (mk_offset (addition_n ? (offv (offset_plus o delta)) (sign_ext 2 offset_size (bitvector_of_nat 2 1))) =
2157          offset_plus (offset_plus o (mk_offset (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) delta)
2158     [ cases o #o' normalize nodelta whd in match (offset_plus ??) in ⊢ (??%%);
2159       whd in match (offset_plus ??) in ⊢ (???(?%));
2160      /2 by associative_addition_n, commutative_addition_n, refl/ ]
2161     #Heq_cleanup >Heq_cleanup >Heq_cleanup in Hind; #Hind @(Hind … Hstoren_tl)
2162     try assumption
2163     #p #p' #Hvalid_in_m1_tmp #Hp_embed @valid_pointer_of_Prop
2164     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * *
2165     #Hnextblock_eq #Hbounds_eq #Hoffset_in_bounds #Hcontents_at_eq #Hcontents_else_eq
2166     lapply (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * *
2167     #Hnextblock_eq2 #Hbounds_eq2 #Hoffset_in_bounds2 #Hcontents_at_eq2 #Hcontents_else_eq2
2168     cut (valid_pointer m1 p = true)
2169     [ @valid_pointer_of_Prop
2170       cases (valid_pointer_to_Prop … Hvalid_in_m1_tmp)
2171       >Hnextblock_eq cases (Hbounds_eq (pblock p)) #Hlow' #Hhigh'
2172       whd in match (low_bound ??); whd in match (high_bound ??);
2173       >Hlow' >Hhigh' * /3 by conj/ ]
2174     #Hvalid_in_m1
2175     lapply (Hvalid_embed p p' Hvalid_in_m1 Hp_embed) #Hvalid_in_m2     
2176     cases (valid_pointer_to_Prop … Hvalid_in_m2) * #Hnextblock2' #Hlow2' #Hhigh2'
2177     @conj try @conj
2178     >Hnextblock_eq2 try assumption
2179     cases (Hbounds_eq2 … (pblock p')) #Hlow2'' #Hhigh2''
2180     whd in match (low_bound ??);
2181     whd in match (high_bound ??);
2182      >Hlow2'' >Hhigh2'' assumption
2183] qed.     
2184
2185lemma storen_parallel_memory_exists_and_preserves_loads :
2186  ∀E,m1,m2.
2187  memory_inj E m1 m2 →
2188  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
2189  ∀v1,v2. value_eq E v1 v2 →
2190  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
2191  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
2192        loadn m2' (mk_pointer b2 (offset_plus i delta)) (|fe_to_be_values ty v2|) = Some ? (fe_to_be_values ty v2).
2193#E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty #Hstoren
2194cases (storen_parallel_memory_exists … Hinj … Hembed … Hvalue_eq i m1' ty Hstoren)
2195#m2' #Hstoren' %{m2'} @conj try assumption
2196@(storen_loadn_ok … Hstoren')
2197//
2198qed.
2199
2200(* If E ⊢ m1 ↦ m2
2201   *and* if E b1 = 〈b2,delta〉,
2202   *and* if we write /A PROPER VALUE/ at 〈b1,i〉 successfuly,
2203   *then* we can write /something value_eq-compatible/ in m2 at 〈b2,i+delta〉 successfuly yielding m2'
2204          *and* preserve the injection : E ⊢ m1' ↦ m2'         
2205   N.B.: this result cannot be given at the back-end level : we could overwrite a pointer
2206         and break the value_eq correspondence between the memories. *)       
2207axiom storen_parallel_aux :
2208  ∀E,m1,m2.
2209  ∀Hinj:memory_inj E m1 m2.
2210  ∀v1,v2. value_eq E v1 v2 →
2211  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
2212  ∀ty,i,m1'.
2213  (* ast_typ_consistent_with_value ty v1 → *)
2214  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
2215  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
2216        memory_inj E m1' m2'.
2217(* This lemma is not provable as in CompCert. In the following chunk of text, I'll try to
2218 * explain why, and how we might still be able to prove it given enough time.
2219   I'll be refering to a paper by Leroy & Blazy in the J.A.R.
2220   In CompCert, when storing some data of size S in some location 〈block, offset〉,
2221   what happens is that
2222   1) the memory is extended with a map from 〈block,offset〉 to the actual data
2223   2) the memory inteval from 〈block,offset+1〉 to 〈block,offset+S-1〉 is invalidated,
2224      meaning that every load in this interval will fail.
2225   This behaviour is documented at page 9 in the aforementioned paper.
2226   The memory model of Cerco is in a sense much more realistic. When storing a front-end
2227   value fv, the story is the following :
2228   1) the value fv is marshalled into a list of back-end values (byte-sized) which correspond
2229      to the actual size of the data in-memory. 2) This list is then stored as-is at the
2230      location 〈block, offset〉.
2231     
2232   Now on to the lemma we want to prove. The difficult part is to prove [load_sim E m1' m2'],
2233   i.e. we want to prove that ∀c1,off1,c2,off2,delta. s.t. E c1 = 〈c2, off2〉
2234     load_value_of_type m1' c1 off1 = ⌊vA⌋ →
2235     load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋ ∧
2236     value_eq E vA vB,
2237   where m1' and m2' are the result of storing some values v1 and v2 in resp. m1 and m2
2238   at some resp. locations 〈b1,i〉 and (pointer_translation E b1 i) (cf statement).
2239
2240   In CompCert, the proof of this statement goes by case analysis on 〈c1,off1〉.
2241   Case 1: 〈b1,i〉 = 〈c1,off1〉 → we read the freshly stored data.
2242   Case 2: b1 = c1 but [i; i+|v1|] and [c1, c1+|vA|] describe /disjoint/ areas of the
2243           same block. In this case, we can use the lemma store_value_load_disjoint
2244           on the hypothesis (load_value_of_type m1' c1 off1 = ⌊vA⌋)
2245           yielding (load_value_of_type m1' c1 off1 = load_value_of_type m1 c1 off1)
2246           allowing us to use the load_sim hypothesis on (m1, m2) to obtain
2247           (load_value_of_type m2 c2 (off1+off2) = ⌊vB⌋)
2248           which we can lift back to
2249           (load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋)
2250           using the disjointness hypothesis contained in the original memory injection [Hinj].
2251   case 4: b1 ≠ c1, nothing difficult
2252   case 3: the intervals  [i; i+|v1|] and [c1, c1+|vA|] /overalap/ !
2253           in CompCert, the prof follows simply from the fact that the load
2254           (load_value_of_type m1' c1 off1) will fail because of invalidated memory,
2255           yielding a contradiction. We have no such possibility in Cerco.
2256   
2257   I see a possible, convoluted way out of this problem. In the case of an overlap, we
2258   need to proceed to an inversion on load_value_of_type m1' c1 off1 = ⌊vA⌋ and to
2259   actually look at the data beeing written. If we succeeded in proceeding to this load,
2260   this means that the back-end values stored are "consistent".
2261   Besides, we need to proceed to a case analysis on what we stored beforehand.
2262   A) If we stored an integer
2263    . of size 8: this means that the overlap actually includes all of the freshly stored
2264      area. This area contains one [BVByte]. If we succeeded in performing an overlapping load,
2265      we either overlapped from the beginning, from the end or from both ends of the stored
2266      area. In all cases, since this area contains a BVByte, all other offsets MUST contain
2267      BVBytes, otherwise we would have a contradiction ... (cumbersome to show but possible)
2268      Hence, we can splice the load in 2 or 3 sub-loads :
2269       . re-use the Case 2 above (disjoint areas) for the parts of the load that are before
2270         and after the stored area
2271       . re-use the Case 1 above for the stored area
2272      and show the whole successful load
2273    . of size 16,32: we have more freedom but only a finite number of overlap possibilities
2274      in each case. We can enumerate them and proceed along the same lines as in the 8 bit
2275      case.
2276   B) If we stored a pointer (of size 2 bytes, necessarily)
2277    . the bytes of a pointer are stored in order and (/!\ important /!\) are /numbered/.
2278    This means that any successful overlapping load has managed to read a pointer in
2279    the wrong order, which yields a contradiction.
2280   C) If we stored a Vnull, roughly the same reasoning as in the pointer case
2281   D) If we stored a Vundef ... This gets hairy. We must reason on the way fe_to_be_values
2282      and be_to_fe_value works. What we want is to show that the load
2283      [load_value_of_a type m1' c1 off1] yields a Vundef. This can happen in several ways.
2284      . If we try to load something of integer type, we will have a Vundef because
2285        we can show that some of the back-end values are BVundef (cf [build_integer])
2286      . If we try to load a pointer, it will also fail for the same reason.
2287  I'll admit that I'm not too sure about the last case. Also, my reasoning on pointers might
2288  fail if we have "longer that 2 bytes" pointers.
2289 
2290  This was a high-level and sketchy proof, and in the interests of time I decide to axiomatize
2291  it.
2292*)
2293
2294(* This is lemma 60 from Leroy&Blazy *)
2295lemma store_value_of_type_parallel :
2296  ∀E,m1,m2.
2297  ∀Hinj:memory_inj E m1 m2.
2298  ∀v1,v2. value_eq E v1 v2 →
2299  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
2300  ∀ty,i,m1'.
2301  (* type_consistent_with_value ty v1 → *)
2302  store_value_of_type ty m1 b1 i v1 = Some ? m1' →
2303  ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧
2304        memory_inj E m1' m2'.
2305#E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1'
2306cases ty
2307[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2308| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2309whd in ⊢ ((??%?) → ?);
2310[ 1,4,5,6,7: #Habsurd destruct ]
2311whd in match (store_value_of_type ?????);
2312@(storen_parallel_aux … Hinj … Hembed) //
2313qed.
2314
2315lemma store_value_of_type_load_sim :
2316  ∀E,m1,m2,m1'.
2317  ∀Hinj:memory_inj E m1 m2.
2318  ∀ty,b,i,v.
2319  E b = None ? →
2320  store_value_of_type ty m1 b i v = Some ? m1' →
2321  load_sim_ptr E m1' m2.
2322#E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore
2323cases Hinj #Hsim #Hfreeblock #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl
2324cases ty in Hstore;
2325[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2326| #structname #fieldspec | #unionname #fieldspec | #id ]
2327[ 1,4,5,6,7: #Heq normalize in Heq; destruct ]
2328#Hstore whd
2329#b1 #off1 #b2 #off2 #ty' #v1 #Hvalid #Hembed' #Hload
2330lapply (store_value_of_type_load_value_of_type_conservation … Hstore b1 off1 ? ty')
2331[ 1,3,5: @(eq_block_elim … b b1) try // #Heq >Heq in Hembed;
2332         #Hembed whd in Hembed':(??%?); >Hembed in Hembed'; #H normalize in H;
2333         destruct ]
2334#Heq <Heq in Hload; #Hload
2335(* Three times the same proof, but computing the indices for the subcases is a PITA *)
2336[ 1:
2337  cases ty' in Hload;
2338  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2339  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2340  [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????);
2341               #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))}
2342               @conj try @refl %4 assumption ]
2343  #Hload @(Hsim … Hembed' … Hload)
2344  @(load_by_value_success_valid_pointer … Hload) //
2345| 2:
2346  cases ty' in Hload;
2347  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2348  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2349  [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????);
2350               #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))}
2351               @conj try @refl %4 assumption ]
2352  #Hload @(Hsim … Hembed' … Hload)
2353  @(load_by_value_success_valid_pointer … Hload) //
2354| 3:
2355  cases ty' in Hload;
2356  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
2357  | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2358  [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????);
2359               #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))}
2360               @conj try @refl %4 assumption ]
2361  #Hload @(Hsim … Hembed' … Hload)
2362  @(load_by_value_success_valid_pointer … Hload) //
2363] qed.
2364
2365lemma store_value_of_type_memory_inj :
2366  ∀E,m1,m2,m1'.
2367  ∀Hinj:memory_inj E m1 m2.
2368  ∀ty,b,i,v.
2369  E b = None ? →
2370  store_value_of_type ty m1 b i v = Some ? m1' →
2371  memory_inj E m1' m2.
2372#E #m1 #m2 #m1' #Hinj #ty #b #i #v1 #Hnot_mapped #Hstore
2373%
2374[ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore)
2375| *: lapply (mem_bounds_after_store_value_of_type … Hstore)
2376     * #H1 #H2
2377    [ #b * #Hnot_valid @(mi_freeblock ??? Hinj)
2378      % #H @Hnot_valid whd in H:% ⊢ %; >H1 @H
2379    | #p #p' #Hvalid @(mi_valid_pointers ??? Hinj)
2380      @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
2381      >H1 cases (H2 (pblock p)) #HA #HB
2382      >unfold_high_bound >unfold_low_bound
2383      >unfold_high_bound >unfold_low_bound
2384      >HA >HB //
2385    | @(mi_nodangling … Hinj)
2386    | @(mi_region … Hinj)
2387    | whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq #Hembed1 #Hembed2
2388      whd in match (block_is_empty ??);
2389      whd in match (block_is_empty m1' b2);
2390      >unfold_high_bound >unfold_low_bound
2391      >unfold_high_bound >unfold_low_bound
2392      cases (H2 b1) #HA #HB
2393      cases (H2 b2) #HC #HD
2394      >HA >HB >HC >HD
2395      @(mi_nonalias ??? Hinj) assumption
2396    | #bb whd
2397      lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?);
2398      cases (E bb) normalize nodelta try // * #bb' #off
2399      normalize nodelta
2400      whd in match (block_implementable_bv ??);     
2401      whd in match (block_implementable_bv m2 bb');
2402      whd in match (block_implementable_bv m1' bb);
2403      >unfold_high_bound >unfold_low_bound
2404      >unfold_high_bound >unfold_low_bound
2405      >unfold_high_bound
2406      cases (H2 bb) #HA #HB
2407      >HA >HB //
2408    ]
2409] qed.
2410
2411(* ------------------------------------------------------------------------- *)
2412(* Commutation results of standard unary and binary operations with value_eq. *)
2413
2414lemma unary_operation_value_eq :
2415  ∀E,op,v1,v2,ty.
2416   value_eq E v1 v2 →
2417   ∀r1.
2418   sem_unary_operation op v1 ty = Some ? r1 →
2419    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
2420#E #op #v1 #v2 #ty #Hvalue_eq #r1
2421inversion Hvalue_eq
2422[ 1: #v #Hv1 #Hv2 destruct
2423     cases op normalize
2424     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2425          normalize #Habsurd destruct (Habsurd)
2426     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2427          normalize #Habsurd destruct (Habsurd)
2428     | 2: #Habsurd destruct (Habsurd) ]
2429| 2: #vsz #i #Hv1 #Hv2 #_
2430     cases op
2431     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2432          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
2433          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2434               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
2435               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
2436               //
2437          | *: #Habsurd destruct (Habsurd) ]
2438     | 2: whd in match (sem_unary_operation ???);     
2439          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
2440     | 3: whd in match (sem_unary_operation ???);
2441          cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2442          normalize nodelta
2443          whd in ⊢ ((??%?) → ?);
2444          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
2445               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
2446          | *: #Habsurd destruct (Habsurd) ] ]
2447| 3: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
2448     cases op normalize nodelta
2449     [ 1: cases ty   [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2450          whd in match (sem_notbool ??);
2451          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2452     | 2: normalize #Habsurd destruct (Habsurd)
2453     | 3: cases ty    [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2454          whd in match (sem_neg ??);
2455          #Heq1 destruct ]
2456| 4: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
2457     cases op normalize nodelta
2458     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2459          whd in match (sem_notbool ??);         
2460          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
2461     | 2: normalize #Habsurd destruct (Habsurd)
2462     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
2463          whd in match (sem_neg ??);         
2464          #Heq1 destruct ]
2465]
2466qed.
2467
2468(* value_eq lifts to addition *)
2469lemma add_value_eq :
2470  ∀E,v1,v2,v1',v2',ty1,ty2.
2471   value_eq E v1 v2 →
2472   value_eq E v1' v2' →
2473   (* memory_inj E m1 m2 →  This injection seems useless TODO *)
2474   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
2475           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2476#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2477@(value_eq_inversion E … Hvalue_eq1)
2478[ 1: | 2: #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2479[ 1: whd in match (sem_add ????); normalize nodelta
2480     cases (classify_add ty1 ty2) normalize nodelta
2481     [ 1: #sz #sg | 2: #n #ty #sz #sg | 3: #n #sz #sg #ty | 4: #ty1' #ty2' ]
2482     #Habsurd destruct (Habsurd)
2483| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2484     cases (classify_add ty1 ty2) normalize nodelta
2485     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2486     [ 2,4: #Habsurd destruct (Habsurd) ]
2487     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2488     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
2489     [ 1,2,4,5,7: #Habsurd destruct (Habsurd) ]
2490     [ 1: @intsize_eq_elim_elim
2491          [ 1: #_ #Habsurd destruct (Habsurd)
2492          | 2: #Heq destruct (Heq) normalize nodelta
2493               #Heq destruct (Heq)
2494               /3 by ex_intro, conj, vint_eq/ ]
2495     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
2496          /3 by ex_intro, conj, vint_eq/
2497     | 3: #Heq destruct (Heq)
2498          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
2499          @(ex_intro … (conj … (refl …) ?))
2500          @vptr_eq whd in match (pointer_translation ??);
2501          cases (E b1') in Hembed;
2502          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2503          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2504               whd in match (shift_pointer_n ????);
2505               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) tsg i) offset =
2506                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) tsg i))
2507               [ 1: whd in match (offset_plus ??);
2508                    whd in match (shift_offset_n ????) in ⊢ (??%%);
2509                    >commutative_addition_n >associative_addition_n
2510                    <(commutative_addition_n … (offv offset) (offv o1')) @refl ]
2511               #Heq >Heq @refl ]
2512     ]
2513(* | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2514     cases (classify_add ty1 ty2) normalize nodelta
2515     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2516     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2517     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2518     [ 1: | 2: #sz' #i'| 3: | 4: #p1' #p2' #Hembed' ]
2519     [ 1,3,4,5,7: #Habsurd destruct (Habsurd) ]
2520     #Heq >Heq %{r1} @conj //
2521     /3 by ex_intro, conj, vfloat_eq/ *)
2522| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2523     cases (classify_add ty1 ty2) normalize nodelta
2524     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2525     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2526     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2527     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
2528     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2529     @eq_bv_elim
2530     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2531     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2532| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
2533     cases (classify_add ty1 ty2) normalize nodelta
2534     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2535     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2536     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2537     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
2538     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
2539     #Heq destruct (Heq)
2540     @(ex_intro … (conj … (refl …) ?))
2541     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2542     elim p1 in Hembed; #b1 #o1 normalize nodelta
2543     cases (E b1)
2544     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2545     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2546          whd in match (shift_pointer_n ????);
2547          whd in match (shift_offset_n ????) in ⊢ (??%%);
2548          whd in match (offset_plus ??);
2549          whd in match (offset_plus ??);
2550          >commutative_addition_n >(associative_addition_n … offset_size ?)
2551          >(commutative_addition_n ? (offv offset) ?) @refl
2552     ]
2553] qed.
2554
2555lemma subtraction_delta : ∀x,y,delta.
2556  subtraction offset_size
2557    (addition_n offset_size x delta)
2558    (addition_n offset_size y delta) =
2559  subtraction offset_size x y.
2560#x #y #delta whd in match subtraction; normalize nodelta
2561(* Remove all the equal parts on each side of the equation. *)
2562<associative_addition_n
2563>two_complement_negation_plus
2564<(commutative_addition_n … (two_complement_negation ? delta))
2565>(associative_addition_n ? delta) >bitvector_opp_addition_n
2566>(commutative_addition_n ? (zero ?)) >neutral_addition_n
2567@refl
2568qed.
2569
2570(* Offset subtraction is invariant by translation *)
2571lemma sub_offset_translation :
2572 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
2573#n #x #y #delta
2574whd in match (sub_offset ???) in ⊢ (??%%);
2575elim x #x' elim y #y' elim delta #delta'
2576whd in match (offset_plus ??);
2577whd in match (offset_plus ??);
2578>subtraction_delta @refl
2579qed.
2580
2581(* value_eq lifts to subtraction *)
2582lemma sub_value_eq :
2583  ∀E,v1,v2,v1',v2',ty1,ty2,target.
2584   value_eq E v1 v2 →
2585   value_eq E v1' v2' →
2586   ∀r1. (sem_sub v1 ty1 v1' ty2 target=Some val r1→
2587           ∃r2:val.sem_sub v2 ty1 v2' ty2 target=Some val r2∧value_eq E r1 r2).
2588#E #v1 #v2 #v1' #v2' #ty1 #ty2 #target #Hvalue_eq1 #Hvalue_eq2 #r1
2589@(value_eq_inversion E … Hvalue_eq1)
2590[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2591[ 1: whd in match (sem_sub ?????); normalize nodelta
2592     cases (classify_sub ty1 ty2) normalize nodelta
2593     [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ]
2594     #Habsurd destruct (Habsurd)
2595| 2: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
2596     cases (classify_sub ty1 ty2) normalize nodelta     
2597     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2598     [ 2,3,4: #Habsurd destruct (Habsurd) ]
2599     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2600     [  | #sz' #i' | | #p1' #p2' #Hembed' ]
2601     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2602     @intsize_eq_elim_elim
2603      [ 1: #_ #Habsurd destruct (Habsurd)
2604      | 2: #Heq destruct (Heq) normalize nodelta
2605           #Heq destruct (Heq)
2606          /3 by ex_intro, conj, vint_eq/
2607      ]
2608(*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
2609     cases (classify_sub ty1 ty2) normalize nodelta
2610     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2611     [ 1,4: #Habsurd destruct (Habsurd) ]
2612     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2613     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2614     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
2615     #Heq destruct (Heq)
2616     /3 by ex_intro, conj, vfloat_eq/ *)
2617| 3: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
2618     cases (classify_sub ty1 ty2) normalize nodelta
2619     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2620     [ 1,4: #Habsurd destruct (Habsurd) ]
2621     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2622     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
2623     [ 1,2,4,5,7,8: #Habsurd destruct (Habsurd) ]
2624     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
2625                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2626     | 2: cases target
2627          [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2628          | #structname #fieldspec | #unionname #fieldspec | #id ]
2629          normalize nodelta
2630          #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
2631| 4: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
2632     cases (classify_sub ty1 ty2) normalize nodelta
2633     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
2634     [ 1,4: #Habsurd destruct (Habsurd) ]
2635     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2636     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
2637     [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ]
2638     #Heq destruct (Heq)
2639     [ 1: @(ex_intro … (conj … (refl …) ?))
2640          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
2641          elim p1 in Hembed; #b1 #o1 normalize nodelta
2642          cases (E b1)
2643          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2644          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
2645               whd in match (offset_plus ??) in ⊢ (??%%);
2646               whd in match (neg_shift_pointer_n ?????) in ⊢ (??%%);
2647               whd in match (neg_shift_offset_n ?????) in ⊢ (??%%);
2648               whd in match (subtraction) in ⊢ (??%%); normalize nodelta
2649               generalize in match (short_multiplication ???); #mult
2650               /3 by associative_addition_n, commutative_addition_n, refl/
2651          ]
2652     | 2: lapply Heq @eq_block_elim
2653          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
2654          | 1: #Hpblock1_eq normalize nodelta
2655               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
2656               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
2657               whd in ⊢ ((??%?) → (??%?) → ?);
2658               cases (E b1') normalize nodelta
2659               [ 1: #Habsurd destruct (Habsurd) ]
2660               * #dest_block #dest_off normalize nodelta
2661               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_b_b normalize nodelta
2662               cases (eqb (sizeof tsg) O) normalize nodelta
2663               [ 1: #Habsurd destruct (Habsurd)
2664               | 2: cases target
2665                    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2666                    | #structname #fieldspec | #unionname #fieldspec | #id ]
2667                    normalize nodelta
2668                    #Heq destruct (Heq)
2669                    <(sub_offset_translation 32 off1 off1' dest_off)
2670                    cases (division_u ?
2671                            (sub_offset ? off1 off1')
2672                            (repr (sizeof tsg))) in Heq;
2673                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
2674                    | 2: #r1' cases sg normalize nodelta #Heq2 destruct (Heq2)
2675                         /3 by ex_intro, conj, vint_eq/ ]
2676    ] ] ]
2677] qed.
2678
2679lemma mul_value_eq :
2680  ∀E,v1,v2,v1',v2',ty1,ty2.
2681   value_eq E v1 v2 →
2682   value_eq E v1' v2' →
2683   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
2684           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2685#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2686@(value_eq_inversion E … Hvalue_eq1)
2687[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2688[ 1: whd in match (sem_mul ????); normalize nodelta
2689     cases (classify_aop ty1 ty2) normalize nodelta
2690     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2691     #Habsurd destruct (Habsurd)
2692| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2693     cases (classify_aop ty1 ty2) normalize nodelta
2694     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2695     [ 2: #Habsurd destruct (Habsurd) ]
2696     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2697     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2698     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2699     @intsize_eq_elim_elim
2700      [ 1: #_ #Habsurd destruct (Habsurd)
2701      | 2: #Heq destruct (Heq) normalize nodelta
2702           #Heq destruct (Heq)
2703          /3 by ex_intro, conj, vint_eq/           
2704      ]
2705| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2706     cases (classify_aop ty1 ty2) normalize nodelta
2707     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2708     [ 1,2: #Habsurd destruct (Habsurd) ]
2709| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
2710     cases (classify_aop ty1 ty2) normalize nodelta
2711     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2712     #Habsurd destruct (Habsurd)
2713] qed.     
2714
2715lemma div_value_eq :
2716  ∀E,v1,v2,v1',v2',ty1,ty2.
2717   value_eq E v1 v2 →
2718   value_eq E v1' v2' →
2719   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
2720           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2721#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2722@(value_eq_inversion E … Hvalue_eq1)
2723[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2724[ 1: whd in match (sem_div ????); normalize nodelta
2725     cases (classify_aop ty1 ty2) normalize nodelta
2726     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2727     #Habsurd destruct (Habsurd)
2728| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2729     cases (classify_aop ty1 ty2) normalize nodelta
2730     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2731     [ 2: #Habsurd destruct (Habsurd) ]
2732     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2733     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2734     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2735     elim sg normalize nodelta
2736     @intsize_eq_elim_elim
2737     [ 1,3: #_ #Habsurd destruct (Habsurd)
2738     | 2,4: #Heq destruct (Heq) normalize nodelta
2739            @(match (division_s (bitsize_of_intsize sz') i i') with
2740              [ None ⇒ ?
2741              | Some bv' ⇒ ? ])
2742            [ 1: normalize  #Habsurd destruct (Habsurd)
2743            | 2: normalize #Heq destruct (Heq)
2744                 /3 by ex_intro, conj, vint_eq/
2745            | 3,4: elim sz' in i' i; #i' #i
2746                   normalize in match (pred_size_intsize ?);
2747                   generalize in match division_u; #division_u normalize
2748                   @(match (division_u ???) with
2749                    [ None ⇒ ?
2750                    | Some bv ⇒ ?]) normalize nodelta
2751                   #H destruct (H)
2752                  /3 by ex_intro, conj, vint_eq/ ]
2753     ]
2754| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2755     cases (classify_aop ty1 ty2) normalize nodelta
2756     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2757     [ 1,2: #Habsurd destruct (Habsurd) ]
2758| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
2759     cases (classify_aop ty1 ty2) normalize nodelta
2760     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2761     #Habsurd destruct (Habsurd)
2762] qed.     
2763
2764lemma mod_value_eq :
2765  ∀E,v1,v2,v1',v2',ty1,ty2.
2766   value_eq E v1 v2 →
2767   value_eq E v1' v2' →
2768   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
2769           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
2770#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
2771@(value_eq_inversion E … Hvalue_eq1)
2772[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2773[ 1: whd in match (sem_mod ????); normalize nodelta
2774     cases (classify_aop ty1 ty2) normalize nodelta
2775     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2776     #Habsurd destruct (Habsurd)
2777| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2778     cases (classify_aop ty1 ty2) normalize nodelta
2779     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2780     [ 2: #Habsurd destruct (Habsurd) ]
2781     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2782     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2783     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2784     elim sg normalize nodelta
2785     @intsize_eq_elim_elim
2786     [ 1,3: #_ #Habsurd destruct (Habsurd)
2787     | 2,4: #Heq destruct (Heq) normalize nodelta
2788            @(match (modulus_s (bitsize_of_intsize sz') i i') with
2789              [ None ⇒ ?
2790              | Some bv' ⇒ ? ])
2791            [ 1: normalize  #Habsurd destruct (Habsurd)
2792            | 2: normalize #Heq destruct (Heq)
2793                 /3 by ex_intro, conj, vint_eq/
2794            | 3,4: elim sz' in i' i; #i' #i
2795                   generalize in match modulus_u; #modulus_u normalize
2796                   @(match (modulus_u ???) with
2797                    [ None ⇒ ?
2798                    | Some bv ⇒ ?]) normalize nodelta
2799                   #H destruct (H)
2800                  /3 by ex_intro, conj, vint_eq/ ]
2801     ]     
2802| *: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
2803     cases (classify_aop ty1 ty2) normalize nodelta #foo #bar #Habsurd destruct (Habsurd)
2804] qed.
2805
2806(* boolean ops *)
2807lemma and_value_eq :
2808  ∀E,v1,v2,v1',v2'.
2809   value_eq E v1 v2 →
2810   value_eq E v1' v2' →
2811   ∀r1. (sem_and v1 v1'=Some val r1→
2812           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
2813#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2814@(value_eq_inversion E … Hvalue_eq1)
2815[ 2: #sz #i
2816     @(value_eq_inversion E … Hvalue_eq2)
2817     [ 2: #sz' #i' whd in match (sem_and ??);
2818          @intsize_eq_elim_elim
2819          [ 1: #_ #Habsurd destruct (Habsurd)
2820          | 2: #Heq destruct (Heq) normalize nodelta
2821               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2822] ]
2823normalize in match (sem_and ??); #arg1 destruct
2824normalize in match (sem_and ??); #arg2 destruct
2825normalize in match (sem_and ??); #arg3 destruct
2826normalize in match (sem_and ??); #arg4 destruct
2827qed.
2828
2829lemma or_value_eq :
2830  ∀E,v1,v2,v1',v2'.
2831   value_eq E v1 v2 →
2832   value_eq E v1' v2' →
2833   ∀r1. (sem_or v1 v1'=Some val r1→
2834           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
2835#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2836@(value_eq_inversion E … Hvalue_eq1)
2837[ 2: #sz #i
2838     @(value_eq_inversion E … Hvalue_eq2)
2839     [ 2: #sz' #i' whd in match (sem_or ??);
2840          @intsize_eq_elim_elim
2841          [ 1: #_ #Habsurd destruct (Habsurd)
2842          | 2: #Heq destruct (Heq) normalize nodelta
2843               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2844] ]
2845normalize in match (sem_or ??); #arg1 destruct
2846normalize in match (sem_or ??); #arg2 destruct
2847normalize in match (sem_or ??); #arg3 destruct
2848normalize in match (sem_or ??); #arg4 destruct
2849qed.
2850
2851lemma xor_value_eq :
2852  ∀E,v1,v2,v1',v2'.
2853   value_eq E v1 v2 →
2854   value_eq E v1' v2' →
2855   ∀r1. (sem_xor v1 v1'=Some val r1→
2856           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
2857#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2858@(value_eq_inversion E … Hvalue_eq1)
2859[ 2: #sz #i
2860     @(value_eq_inversion E … Hvalue_eq2)
2861     [ 2: #sz' #i' whd in match (sem_xor ??);
2862          @intsize_eq_elim_elim
2863          [ 1: #_ #Habsurd destruct (Habsurd)
2864          | 2: #Heq destruct (Heq) normalize nodelta
2865               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
2866] ]
2867normalize in match (sem_xor ??); #arg1 destruct
2868normalize in match (sem_xor ??); #arg2 destruct
2869normalize in match (sem_xor ??); #arg3 destruct
2870normalize in match (sem_xor ??); #arg4 destruct
2871qed.
2872
2873lemma shl_value_eq :
2874  ∀E,v1,v2,v1',v2'.
2875   value_eq E v1 v2 →
2876   value_eq E v1' v2' →
2877   ∀r1. (sem_shl v1 v1'=Some val r1→
2878           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
2879#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
2880@(value_eq_inversion E … Hvalue_eq1)
2881[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2882[ 2:
2883     @(value_eq_inversion E … Hvalue_eq2)
2884     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2885     [ 2: whd in match (sem_shl ??);
2886          cases (lt_u ???) normalize nodelta
2887          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
2888          | 2: #Habsurd destruct (Habsurd)
2889          ]
2890     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2891| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
2892qed.
2893
2894lemma shr_value_eq :
2895  ∀E,v1,v2,v1',v2',ty,ty'.
2896   value_eq E v1 v2 →
2897   value_eq E v1' v2' →
2898   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
2899           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
2900#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
2901@(value_eq_inversion E … Hvalue_eq1)
2902[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
2903whd in match (sem_shr ????); whd in match (sem_shr ????);
2904[ 1: cases (classify_aop ty ty') normalize nodelta
2905     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2906     #Habsurd destruct (Habsurd)
2907| 2: cases (classify_aop ty ty') normalize nodelta
2908     [ 1: #sz #sg | 2: #ty1' #ty2' ]
2909     [ 2: #Habsurd destruct (Habsurd) ]
2910     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2911     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
2912     [ 1,3,4: #Habsurd destruct (Habsurd) ]
2913     elim sg normalize nodelta
2914     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
2915     /3 by ex_intro, conj, refl, vint_eq/
2916| *: cases (classify_aop ty ty') normalize nodelta
2917     #foo #bar
2918     #Habsurd destruct (Habsurd)
2919] qed.     
2920
2921lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
2922* #delta * #x * #y
2923whd in match (offset_plus ??);
2924whd in match (offset_plus ??);
2925whd in match cmp_offset; normalize nodelta
2926whd in match eq_offset; normalize nodelta
2927@(eq_bv_elim … x y)
2928[ 1: #Heq >Heq >eq_bv_true @refl
2929| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
2930     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
2931     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
2932] qed.     
2933
2934lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
2935* #delta * #x * #y
2936whd in match (offset_plus ??);
2937whd in match (offset_plus ??);
2938whd in match cmp_offset; normalize nodelta
2939whd in match eq_offset; normalize nodelta
2940@(eq_bv_elim … x y)
2941[ 1: #Heq >Heq >eq_bv_true @refl
2942| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
2943     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
2944     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
2945] qed.
2946
2947(* Note that x and y are bounded below and above, similarly for the shifted offsets.
2948   This is enough to prove that there is no "wrap-around-the-end" problem,
2949   /provided we know that the block bounds are implementable by 2^16 bitvectors/.
2950   We axiomatize it for now. *)
2951axiom cmp_offset_translation :
2952  ∀op,delta,x,y.
2953  (Zoo x) + (Zoo delta) < Z_two_power_nat 16 →
2954  (Zoo y) + (Zoo delta) < Z_two_power_nat 16 →
2955  cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
2956
2957lemma valid_pointer_of_implementable_block_is_implementable :
2958  ∀m,b.
2959    block_implementable_bv m b →
2960    ∀o. valid_pointer m (mk_pointer b o) = true →
2961        Zoo o < Z_two_power_nat 16.
2962#m #b whd in ⊢ (% → ?); * #Hlow #Hhigh
2963* #o #Hvalid cases (valid_pointer_to_Prop … Hvalid) * #_
2964#Hlow' #Hhigh'
2965cases Hlow -Hlow #Hlow0 #Hlow16
2966cases Hhigh -Hhigh #Hhigh0 #Hhigh16
2967whd in match (Zoo ?);
2968@(transitive_Zlt … Hhigh' Hhigh16)
2969qed.
2970
2971lemma cmp_value_eq :
2972  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
2973   value_eq E v1 v2 →
2974   value_eq E v1' v2' →
2975   memory_inj E m1 m2 →
2976   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1 →
2977           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
2978#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
2979elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj
2980whd in match (sem_cmp ??????) in ⊢ ((??%?) → %);
2981cases (classify_cmp ty ty') normalize nodelta
2982[ 1: #tsz #tsg
2983     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
2984     [ 1: #Habsurd destruct (Habsurd)
2985     | 3: #Habsurd destruct (Habsurd)
2986     | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
2987     #sz #i
2988     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2989     [ 1: #Habsurd destruct (Habsurd)
2990     | 3: #Habsurd destruct (Habsurd)
2991     | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
2992     #sz' #i' cases tsg normalize nodelta
2993     @intsize_eq_elim_elim
2994     [ 1,3: #Hneq #Habsurd destruct (Habsurd)
2995     | 2,4: #Heq destruct (Heq) normalize nodelta
2996            #Heq destruct (Heq)
2997            [ 1: cases (cmp_int ????) whd in match (of_bool ?);
2998            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
2999              /3 by ex_intro, conj, vint_eq/ ]
3000| 3: #ty1 #ty2 #Habsurd destruct (Habsurd)
3001| 2: lapply Hinj -Hinj
3002     generalize in match (mk_mem contmap1 ??); #m1
3003     generalize in match (mk_mem contmap2 ??); #m2
3004     #Hinj #optn #typ
3005     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
3006     [ 1: #Habsurd destruct (Habsurd)
3007     | 2: #sz #i #Habsurd destruct (Habsurd)
3008     | 4: #p1 #p2 #Hembed ]
3009     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
3010     [ 1,5: #Habsurd destruct (Habsurd)
3011     | 2,6: #sz #i #Habsurd destruct (Habsurd)
3012     | 4,8: #q1 #q2 #Hembed' ]
3013     [ 2,3: cases op whd in match (sem_cmp_mismatch ?);
3014          #Heq destruct (Heq)
3015          [ 1,3: %{Vfalse} @conj try @refl @vint_eq
3016          | 2,4: %{Vtrue} @conj try @refl @vint_eq ]
3017     | 4: cases op whd in match (sem_cmp_match ?);
3018          #Heq destruct (Heq)
3019          [ 2,4: %{Vfalse} @conj try @refl @vint_eq
3020          | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ]
3021     #Hvalid
3022     lapply (if_opt_inversion ???? Hvalid) -Hvalid * #Hconj
3023     lapply (andb_inversion … Hconj) -Hconj * #Hvalid #Hvalid'
3024     lapply (mi_valid_pointers … Hinj q1 q2 Hvalid' Hembed') #Hvalid2' >Hvalid2'
3025     lapply (mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) #Hvalid2 >Hvalid2
3026     normalize nodelta
3027(*   >(mi_valid_pointers … Hinj p1' p2' Hvalid' Hembed')
3028     >(mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) normalize nodelta *)
3029     elim p1 in Hvalid Hembed; #bp1 #op1
3030     elim q1 in Hvalid' Hembed'; #bq1 #oq1
3031     #Hvalid' #Htmp #Hvalid lapply Htmp -Htmp
3032     whd in match (pointer_translation ??);
3033     whd in match (pointer_translation ??);
3034     @(eq_block_elim … bp1 bq1)
3035     [ 1: #Heq destruct (Heq) normalize nodelta
3036          lapply (mi_nowrap … Hinj bq1)
3037          whd in ⊢ (% → ?);
3038          cases (E bq1) normalize nodelta
3039          [ #_ #Habsurd destruct ]
3040          * #BLO #OFF normalize nodelta * *         
3041          #Hbq1_implementable #HBLO_implementable #Hno_wrap
3042          #Heq1 #Heq2 #Heq3 destruct
3043          >eq_block_b_b normalize nodelta
3044          lapply (cmp_offset_translation op OFF op1 oq1 ??)
3045          [ @(Zlt_sum_weaken … Hno_wrap)
3046            cases (valid_pointer_to_Prop … Hvalid') * #_ #_ try //
3047          | @(Zlt_sum_weaken … Hno_wrap)
3048            cases (valid_pointer_to_Prop … Hvalid) * #_ #_ try // ]
3049          #Heq <Heq
3050          cases (cmp_offset op op1 oq1)
3051          normalize nodelta
3052          try /3 by ex_intro, conj, refl, vint_eq/
3053     | 2: #Hneq lapply (mi_nonalias … Hinj bp1 bq1)
3054          normalize nodelta
3055          lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?);
3056          lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?);
3057          lapply (mi_region … Hinj bq1)
3058          lapply (mi_region … Hinj bp1)
3059          cases (E bq1) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
3060          * #BLOq #DELTAq normalize nodelta
3061          cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
3062          * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
3063          lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2
3064          #Hregion2 #Hregion1
3065          cases op
3066          whd in ⊢ ((??%?) → ?); #H' destruct (H')
3067          whd in match (sem_cmp_mismatch ?);
3068          lapply (H ???? Hneq (refl ??) (refl ??)) -H
3069          cases (block_decidable_eq BLOp BLOq) normalize nodelta
3070          #H
3071          [ 2: #_ >(not_eq_block … H) normalize nodelta %{Vfalse} @conj try @refl %2
3072          | 4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ]
3073          destruct (H) generalize in match BLOq in Hnowrap1 Hnowrap2 Hvalid2 Hvalid2' ⊢ %;
3074          #target_block * * #Himplq1 #Himpltarget #Hnowrap_q1
3075          * * #Himplp1 #_ #Hnowrap_p1 #Hvalid2 #Hvalid2'
3076          lapply (valid_pointer_to_Prop … Hvalid)
3077          lapply (valid_pointer_to_Prop … Hvalid')
3078          * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
3079          >eq_block_b_b normalize nodelta
3080          *
3081          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
3082                 cases (valid_pointer_to_Prop … Hvalid') * #_ #Hle #Hlt
3083                 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt'
3084                 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl
3085                 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ]
3086          *
3087          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
3088                 cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt
3089                 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt'
3090                 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl
3091                 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ]
3092          *
3093          #Hdisjoint
3094          whd in match (cmp_offset); normalize nodelta
3095          whd in match (eq_offset); normalize nodelta
3096          whd in match (offset_plus ??);
3097          whd in match (offset_plus ??);
3098          lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2)
3099          lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2')
3100          #Himpl1 #Himpl2
3101          [ 1,3:
3102              (* We show the non-equality of the rhs by exhibiting disjointness of blocks. This is made
3103               * painful by invariants on non-overflowing offsets. We exhibit [a]+[b] < [c]+[d], then
3104               * cut [a+b]<[c+d] (using a subcut for needed consistency hypotheses) and conclude easily
3105               * [a+b] ≠ [c+d]. *)
3106              cut ((Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp))
3107                   < (Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq)))
3108              [ 1,3:
3109                @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bp1 + Zoo DELTAp) ?)
3110                [ 1,3: @Zlt_translate assumption
3111                | 2,4: @(transitive_Zle ? (low_bound m1 bq1+Zoo DELTAq) ?) try assumption
3112                       @monotonic_Zle_Zplus_l try assumption ]
3113              ]
3114              #Hlt_stepA
3115              cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp))
3116                   < Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq)))
3117              [ 1,3:
3118                >Z_addition_bv_commute
3119                [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ]
3120                >Z_addition_bv_commute
3121                [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ]
3122                try assumption ] -Hlt_stepA
3123           | 2,4:
3124              cut ((Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq))
3125                   < (Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp)))
3126              [ 1,3:
3127                @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bq1 + Zoo DELTAq) ?)
3128                [ 1,3: @Zlt_translate assumption
3129                | 2,4: @(transitive_Zle ? (low_bound m1 bp1+Zoo DELTAp) ?) try assumption
3130                       @monotonic_Zle_Zplus_l try assumption ]
3131              ]
3132              #Hlt_stepA
3133              cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq))
3134                   < Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp)))
3135              [ 1,3:
3136                >Z_addition_bv_commute
3137                [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ]
3138                >Z_addition_bv_commute
3139                [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ]
3140                try assumption ] -Hlt_stepA
3141            ]
3142            generalize in match (addition_n ? (offv op1) ?); #lhs
3143            generalize in match (addition_n ? (offv oq1) ?); #rhs
3144            #Hlt_stepB lapply (Zlt_to_Zneq … Hlt_stepB)
3145            @(eq_bv_elim … lhs rhs)
3146            [ 1,3,5,7: #Heq destruct * #H @(False_ind … (H (refl ??)))
3147            | 2,4,6,8: #Hneq #_ /3 by ex_intro, conj, vint_eq/ ]
3148    ]
3149] qed.
3150   
Note: See TracBrowser for help on using the repository browser.