source: src/Clight/memoryInjections.ma @ 2483

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

Memory injections for Clight to Cminor, partially axiomatized.

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