source: src/Clight/memoryInjections.ma @ 2608

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

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

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