source: src/Clight/memoryInjections.ma @ 2562

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

Proof of expression translation correctness "mostly" done for CL to CM. Some inconsistencies found in bit width for constants
regarding boolean operators need to be fixed (either by modifying CL semantics of by making CM code generation inefficient).
An inconsistency between clight and cminor expression evaluation was found for cost labels (placed before and after trace) - not
fixed yet, for fear of breaking proofs. One or two small lemmas missing, and most importantly, binary operators not done yet.

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