source: src/Clight/memoryInjections.ma @ 2500

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

Continuing work on simulation in Clight/Cminor?

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