source: src/Clight/memoryInjections.ma @ 2588

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

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

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