source: src/Clight/memoryInjections.ma @ 2572

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

Progress on toCminorCorrectness.

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