source: src/Clight/memoryInjections.ma @ 2578

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

Progress on CL to CM, fixed some stuff in memory injections.

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