source: src/Clight/memoryInjections.ma @ 2594

Last change on this file since 2594 was 2594, checked in by garnier, 8 years ago

Some fixes in memory injections, and some holes filled.

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