source: src/Clight/memoryInjections.ma @ 2569

Last change on this file since 2569 was 2569, checked in by campbell, 7 years ago

Fix Clight semantics for ptr + char. (Compiler works anyway.)

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