source: src/Clight/memoryInjections.ma @ 2600

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

Memory injections are now only defined relatively to block ids, not regions. Used to prove some more unfinished lemmas.

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