source: src/Clight/memoryInjections.ma @ 2598

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

Tentative, partial draft for the definition of Clight-Cminor simulation for statements. Commented out for now.
Also, some stuff on memory injections, and some more aliases on abstract.ma.

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