source: src/Clight/memoryInjections.ma @ 2468

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

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File size: 82.3 KB
Line 
1include "Clight/Cexec.ma".
2include "Clight/MemProperties.ma". 
3include "Clight/frontend_misc.ma".
4
5(* This file contains some definitions and lemmas related to memory injections.
6   Could be useful for the Clight → Cminor. Needs revision: the definitions are
7   too lax and allow inconsistent embeddings (more precisely, these embeddings do
8   not allow to prove that the semantics for pointer less-than comparisons is
9   conserved). *)
10
11
12(* --------------------------------------------------------------------------- *)   
13(* Aux lemmas that are likely to be found elsewhere. *)
14(* --------------------------------------------------------------------------- *)   
15
16lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
17#a #b #HA
18lapply (Zltb_true_to_Zlt … HA) #HA_prop
19@Zlt_to_Zltb_true /2/
20qed.
21
22lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
23#a @Zlt_to_Zltb_true /2/ qed.
24(*
25definition le_offset : offset → offset → bool.
26  λx,y. Zleb (offv x) (offv y).
27*)
28lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
29
30lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
31
32(* --------------------------------------------------------------------------- *)
33(* Some shorthands for conversion functions from BitVectorZ. *)
34(* --------------------------------------------------------------------------- *)
35
36definition Zoub ≝ Z_of_unsigned_bitvector.
37definition boZ ≝ bitvector_of_Z.
38
39(* Offsets are just bitvectors packed inside some useless and annoying constructor. *)
40definition Zoo ≝ λx. Zoub ? (offv x).
41definition boo ≝ λx. mk_offset (boZ ? x).
42
43(* --------------------------------------------------------------------------- *)   
44(* In the definition of injections below, we maintain a list of blocks that are
45   writeable. We need some lemmas to reason on the fact that a block cannot be
46   both writeable and not writeable, etc. *)
47(* --------------------------------------------------------------------------- *)
48
49(* When equality on A is decidable, [mem A elt l] is too. *)
50lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
51#A #dec #elt #l elim l
52[ 1: normalize %2 /2/
53| 2: #hd #tl #Hind
54     elim (dec elt hd)
55     [ 1: #Heq >Heq %1 /2/
56     | 2: #Hneq cases Hind
57        [ 1: #Hmem %1 /2/
58        | 2: #Hnmem %2 normalize
59              % #H cases H
60              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
61              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
62] ] ]
63qed.
64
65lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
66#a #b @(eq_block_elim … a b) /2/ qed.
67
68lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
69#l #elt1 #elt2 elim l
70[ 1: normalize #Habsurd @(False_ind … Habsurd)
71| 2: #hd #tl #Hind normalize #Hl #Hr
72   cases Hl
73   [ 1: #Heq >Heq
74        @(eq_block_elim … hd elt2)
75        [ 1: #Heq >Heq /2 by not_to_not/
76        | 2: #x @x ]
77   | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
78        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
79        | 2: #Hmem2 @Hind //
80        ]
81   ]
82] qed.
83
84lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
85#b1 #b2 * #Hb
86@(eq_block_elim … b1 b2)
87[ 1: #Habsurd @(False_ind … (Hb Habsurd))
88| 2: // ] qed.
89
90(* --------------------------------------------------------------------------- *)   
91(* Lemmas related to freeing memory and pointer validity. *)
92(* --------------------------------------------------------------------------- *)   
93(*
94lemma nextblock_free_ok : ∀m,b. nextblock m = nextblock (free m b).
95* #contents #next #posnext * #rg #id
96normalize @refl
97qed.
98
99lemma low_bound_free_ok : ∀m,b,ptr.
100   b ≠ (pblock ptr) →
101   Zleb (low_bound (free m b) (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) =
102   Zleb (low_bound m (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))).
103* #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize
104cases prg cases brg normalize nodelta try //
105@(eqZb_elim pid bid)
106[ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))
107| 2,4: #_ #_ @refl
108] qed.
109
110lemma high_bound_free_ok : ∀m,b,ptr.
111   b ≠ (pblock ptr) →
112   Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound (free m b) (pblock ptr)) =
113   Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound m (pblock ptr)).
114* #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize
115cases prg cases brg normalize nodelta try //
116@(eqZb_elim pid bid)
117[ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))
118| 2,4: #_ #_ @refl
119] qed.
120
121lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
122   valid_pointer m ptr = true →
123   pblock ptr ≠ b →
124   valid_pointer (free m b) ptr = true.
125* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
126normalize
127@(eqZb_elim pbid bid)
128[ 1: #Heqid >Heqid cases pbr cases br normalize
129     [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
130     cases (Zltb bid next) normalize nodelta
131     [ 2,4: #Habsurd destruct (Habsurd) ]
132     //
133| 2: #Hneqid cases pbr cases br normalize try // ]
134qed.
135
136lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr.
137   valid_pointer m ptr = true →
138   ¬ mem ? (pblock ptr) blocks →
139   valid_pointer (free_list m blocks) ptr = true.
140#blocks
141elim blocks
142[ 1: #m #ptr normalize #H #_ @H
143| 2: #b #tl #Hind #m #ptr #Hvalid
144     whd in match (mem block (pblock ptr) ?);
145     >free_list_cons * #Hguard
146     @valid_pointer_free_ok
147     [ 2: % #Heq @Hguard %1 @Heq ]
148     @Hind
149     [ 1: @Hvalid
150     | 2: % #Hmem @Hguard %2 @Hmem ]
151] qed. *)
152
153
154lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr.
155   valid_pointer m ptr = true →
156   pblock ptr ≠ b →
157   valid_pointer (free m b) ptr = true.
158* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
159normalize
160@(eqZb_elim pbid bid)
161[ 1: #Heqid >Heqid cases pbr cases br normalize
162     [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
163     cases (Zltb bid next) normalize nodelta
164     [ 2,4: #Habsurd destruct (Habsurd) ]
165     //
166| 2: #Hneqid cases pbr cases br normalize try // ]
167qed.
168
169lemma free_list_cons : ∀m,b,tl. free_list m (b :: tl) = (free (free_list m tl) b).
170#m #b #tl whd in match (free_list ??) in ⊢ (??%%);
171whd in match (free ??); @refl qed.
172
173lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
174   valid_pointer (free m b) ptr = true →
175   pblock ptr ≠ b → (* This hypothesis is necessary to handle the cse of "valid" pointers to empty  *)
176   valid_pointer m ptr = true.
177* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
178@(eqZb_elim pbid bid)
179[ 1: #Heqid >Heqid
180     cases pbr cases br normalize
181     [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
182     cases (Zltb bid next) normalize nodelta
183     [ 2,4: #Habsurd destruct (Habsurd) ]
184     //
185| 2: #Hneqid cases pbr cases br normalize try //
186     >(eqZb_false … Hneqid) normalize nodelta try //
187qed.
188
189lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr.
190   valid_pointer (free_list m blocks) ptr = true →
191   ¬ mem ? (pblock ptr) blocks →
192   valid_pointer m ptr = true.
193#blocks
194elim blocks
195[ 1: #m #ptr normalize #H #_ @H
196| 2: #b #tl #Hind #m #ptr #Hvalid
197     whd in match (mem block (pblock ptr) ?);
198     >free_list_cons in Hvalid; #Hvalid * #Hguard
199     lapply (valid_pointer_free_ok … Hvalid) #H
200     @Hind
201     [ 2: % #Heq @Hguard %2 @Heq
202     | 1: @H % #Heq @Hguard %1 @Heq ]
203] qed.
204
205(* An alternative version without the gard on the equality of blocks. *)
206lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr.
207   valid_pointer (free m b) ptr = true →
208   (pblock ptr) = b ∨ (pblock ptr ≠ b ∧ valid_pointer m ptr = true).
209* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
210@(eq_block_elim … (mk_block br bid) (mk_block pbr pbid))
211[ 1: #Heq #_ %1 @(sym_eq … Heq)
212| 2: cases pbr cases br normalize nodelta
213     [ 1,4: @(eqZb_elim pbid bid)
214         [ 1,3: #Heq >Heq * #H @(False_ind … (H (refl ??)))
215         | 2,4: #Hneq #_ normalize >(eqZb_false … Hneq) normalize nodelta
216                 #H %2 @conj try assumption
217                 % #Habsurd destruct (Habsurd) elim Hneq #Hneq @Hneq try @refl
218         ]
219     | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ]
220] qed.     
221
222(* Well in fact a valid pointer can be valid even after a free. Ah. *)
223(*
224lemma pointer_in_free_list_not_valid : ∀blocks,m,ptr.
225  mem ? (pblock ptr) blocks →
226  valid_pointer (free_list m blocks) ptr = false.
227*)
228(*
229#blocks elim blocks
230[ 1: #m #ptr normalize #Habsurd @(False_ind … Habsurd)
231| 2: #b #tl #Hind #m #ptr
232     whd in match (mem block (pblock ptr) ?);
233     >free_list_cons
234     *
235     [ 1: #Hptr_match whd in match (free ??);
236          whd in match (update_block ????);
237          whd in match (valid_pointer ??);
238          whd in match (low_bound ??);
239          whd in match (high_bound ??);
240          >Hptr_match >eq_block_identity normalize nodelta
241          whd in match (low ?);
242          cut (Zleb OZ (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) = true)
243          [ 1: elim (offv (poff ptr)) //
244               #n' #hd #tl cases hd normalize
245               [ 1: #_ try @refl
246               | 2: #H @H ] ]
247          #H >H
248          cut (Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) OZ = false)
249          [ 1: elim (offv (poff ptr)) normalize
250               #n' #hd #tl cases hd normalize
251               [ 1: normalize #_ try @refl
252               | 2: #H @H ] ]
253  valid_pointer (free_list m blocks) ptr = false.
254*)
255
256
257(* --------------------------------------------------------------------------- *)   
258(* Memory injections *)
259(* --------------------------------------------------------------------------- *)   
260
261(* An embedding is a function from blocks to (blocks × offset). *)
262definition embedding ≝ block → option (block × offset).
263
264definition offset_plus : offset → offset → offset ≝
265  λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)).
266
267lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o.
268* #o
269whd in match (offset_plus ??);
270>addition_n_0 @refl
271qed.
272
273(* Translates a pointer through an embedding. *)
274definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
275λp,E.
276match p with
277[ mk_pointer pblock poff ⇒
278   match E pblock with
279   [ None ⇒ None ?
280   | Some loc ⇒
281    let 〈dest_block,dest_off〉 ≝ loc in
282    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
283    Some ? ptr
284   ]
285].
286
287(* We parameterise the "equivalence" relation on values with an embedding. *)
288(* Front-end values. *)
289inductive value_eq (E : embedding) : val → val → Prop ≝
290| undef_eq :
291  value_eq E Vundef Vundef
292| vint_eq : ∀sz,i.
293  value_eq E (Vint sz i) (Vint sz i)
294| vnull_eq :
295  value_eq E Vnull Vnull
296| vptr_eq : ∀p1,p2.
297  pointer_translation p1 E = Some ? p2 →
298  value_eq E (Vptr p1) (Vptr p2).
299 
300(* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t.
301 * the values are equivalent. *)
302definition load_sim ≝
303λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
304 ∀b1,off1,b2,off2,ty,v1.
305  valid_block m1 b1 →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
306  E b1 = Some ? 〈b2,off2〉 →
307  load_value_of_type ty m1 b1 off1 = Some ? v1 →
308  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
309 
310definition load_sim_ptr ≝
311λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
312 ∀b1,off1,b2,off2,ty,v1.
313  valid_pointer m1 (mk_pointer b1 off1) = true →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
314  pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →
315  load_value_of_type ty m1 b1 off1 = Some ? v1 →
316  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
317 
318(* Adapted from Compcert's Memory *)
319definition non_aliasing : embedding → mem → Prop ≝
320  λE,m.
321  ∀b1,b2,b1',b2',delta1,delta2.
322  b1 ≠ b2 →
323  E b1 = Some ? 〈b1',delta1〉 →
324  E b2 = Some ? 〈b2',delta2〉 →
325  (b1' ≠ b2') ∨
326  high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
327  high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1).
328 
329(* Definition of a memory injection *)
330record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝
331{ (* Load simulation *)
332  mi_inj : load_sim_ptr E m1 m2;
333  (* Invalid blocks are not mapped *)
334  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
335  (* Valid pointers are mapped to valid pointers*)
336  mi_valid_pointers : ∀p,p'.
337                       valid_pointer m1 p = true →
338                       pointer_translation p E = Some ? p' →
339                       valid_pointer m2 p' = true;
340  (* Blocks in the codomain are valid *)
341  (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)
342  (* Regions are preserved *)
343  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
344  (* sub-blocks do not overlap (non-aliasing property) *)
345  mi_nonalias : non_aliasing E m1
346}.
347
348(* ---------------------------------------------------------------------------- *)
349(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
350
351(* A particular inversion. *)
352lemma value_eq_ptr_inversion :
353  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
354#E #p1 #v #Heq inversion Heq
355[ 1: #Habsurd destruct (Habsurd)
356| 2: #sz #i #Habsurd destruct (Habsurd)
357| 3:  #Habsurd destruct (Habsurd)
358| 4: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
359     %{p2} @conj try @refl try assumption
360] qed.
361
362(* A cleaner version of inversion for [value_eq] *)
363lemma value_eq_inversion :
364  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
365  (P Vundef Vundef) →
366  (∀sz,i. P (Vint sz i) (Vint sz i)) →
367  (P Vnull Vnull) →
368  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
369  P v1 v2.
370#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4
371inversion Heq
372[ 1: #Hv1 #Hv2 #_ destruct @H1
373| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
374| 3: #Hv1 #Hv2 #_ destruct @H3
375| 4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed.
376
377(* If we succeed to load something by value from a 〈b,off〉 location,
378   [b] is a valid block. *)
379lemma load_by_value_success_valid_block_aux :
380  ∀ty,m,b,off,v.
381    access_mode ty = By_value (typ_of_type ty) →
382    load_value_of_type ty m b off = Some ? v →
383    Zltb (block_id b) (nextblock m) = true.
384#ty #m * #brg #bid #off #v
385cases ty
386[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
387| #structname #fieldspec | #unionname #fieldspec | #id ]
388whd in match (load_value_of_type ????);
389[ 1,6,7: #_ #Habsurd destruct (Habsurd) ]
390#Hmode
391[ 1,2,5: [ 1: elim sz ]
392     normalize in match (typesize ?);
393     whd in match (loadn ???);
394     whd in match (beloadv ??);
395     cases (Zltb bid (nextblock m)) normalize nodelta
396     try // #Habsurd destruct (Habsurd)
397| *: normalize in Hmode; destruct (Hmode)
398] qed.
399
400(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
401lemma load_by_value_success_valid_ptr_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    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
407    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
408#ty #m * #brg #bid #off #v
409cases ty
410[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
411| #structname #fieldspec | #unionname #fieldspec | #id ]
412whd in match (load_value_of_type ????);
413[ 1,6,7: #_ #Habsurd destruct (Habsurd) ]
414#Hmode
415[ 1,2,5: [ 1: elim sz  ]
416     normalize in match (typesize ?);
417     whd in match (loadn ???);
418     whd in match (beloadv ??);
419     cases (Zltb bid (nextblock m)) normalize nodelta
420     cases (Zleb (low (blocks m (mk_block brg bid)))
421                  (Z_of_unsigned_bitvector offset_size (offv off)))
422     cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid))))
423     normalize nodelta
424     #Heq destruct (Heq)
425     try /3 by conj, refl/
426| *: normalize in Hmode; destruct (Hmode)
427] qed.
428
429lemma load_by_value_success_valid_block :
430  ∀ty,m,b,off,v.
431    access_mode ty = By_value (typ_of_type ty) →
432    load_value_of_type ty m b off = Some ? v →
433    valid_block m b.
434#ty #m #b #off #v #Haccess_mode #Hload
435@Zltb_true_to_Zlt
436elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
437qed.
438
439lemma load_by_value_success_valid_pointer :
440  ∀ty,m,b,off,v.
441    access_mode ty = By_value (typ_of_type ty) →
442    load_value_of_type ty m b off = Some ? v →
443    valid_pointer m (mk_pointer b off).
444#ty #m #b #off #v #Haccess_mode #Hload normalize
445elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
446* #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I
447qed.
448
449(* Making explicit the contents of memory_inj for load_value_of_type.
450 * Equivalent to Lemma 59 of Leroy & Blazy *)
451lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
452    memory_inj E m1 m2 →
453    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
454    load_value_of_type ty m1 b1 off1 = Some ? v1 →
455    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
456#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
457lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
458lapply (refl ? (access_mode ty))
459cases ty
460[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
461| #structname #fieldspec | #unionname #fieldspec | #id ]
462normalize in ⊢ ((???%) → ?); #Hmode #Hyp
463[ 1,6,7: normalize in Hyp; destruct (Hyp)
464| 4,5: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
465lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
466lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
467qed.
468
469(* -------------------------------------- *)
470(* Lemmas pertaining to memory allocation *)
471
472(* A valid block stays valid after an alloc. *)
473lemma alloc_valid_block_conservation :
474  ∀m,m',z1,z2,r,new_block.
475  alloc m z1 z2 r = 〈m', new_block〉 →
476  ∀b. valid_block m b → valid_block m' b.
477#m #m' #z1 #z2 #r * #b' #Hregion_eq
478elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
479#Halloc destruct (Halloc)
480#b whd in match (valid_block ??) in ⊢ (% → %); /2/
481qed.
482
483(* Allocating a new zone produces a valid block. *)
484lemma alloc_valid_new_block :
485  ∀m,m',z1,z2,r,new_block.
486  alloc m z1 z2 r = 〈m', new_block〉 →
487  valid_block m' new_block.
488* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
489whd in match (alloc ????); whd in match (valid_block ??);
490#Halloc destruct (Halloc) /2/
491qed.
492
493(* All data in a valid block is unchanged after an alloc. *)
494lemma alloc_beloadv_conservation :
495  ∀m,m',block,offset,z1,z2,r,new_block.
496    valid_block m block →
497    alloc m z1 z2 r = 〈m', new_block〉 →
498    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
499* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
500whd in Halloc:(??%?); destruct (Halloc)
501whd in match (beloadv ??) in ⊢ (??%%);
502lapply (Zlt_to_Zltb_true … Hvalid) #Hlt
503>Hlt >(zlt_succ … Hlt)
504normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
505cut (eqZb (block_id block) next = false)
506[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq
507>Hneq cases (eq_region ??) normalize nodelta  @refl
508qed.
509
510(* Lift [alloc_beloadv_conservation] to loadn *)
511lemma alloc_loadn_conservation :
512  ∀m,m',z1,z2,r,new_block.
513    alloc m z1 z2 r = 〈m', new_block〉 →
514    ∀n. ∀block,offset.
515    valid_block m block →
516    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
517#m #m' #z1 #z2 #r #new_block #Halloc #n
518elim n try //
519#n' #Hind #block #offset #Hvalid_block
520whd in ⊢ (??%%);
521>(alloc_beloadv_conservation … Hvalid_block Halloc)
522cases (beloadv m' (mk_pointer block offset)) //
523#bev normalize nodelta
524whd in match (shift_pointer ???); >Hind try //
525qed.
526
527(* Memory allocation preserves [memory_inj] *)
528lemma alloc_memory_inj :
529  ∀E:embedding.
530  ∀m1,m2,m2',z1,z2,r,new_block.
531  ∀H:memory_inj E m1 m2.
532  alloc m2 z1 z2 r = 〈m2', new_block〉 →
533  memory_inj E m1 m2'.
534#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
535%
536[ 1:
537  whd
538  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
539  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
540  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
541  lapply (refl ? (access_mode ty))
542  cases ty in Hload_eq;
543  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
544  | #structname #fieldspec | #unionname #fieldspec | #id ]
545  #Hload normalize in ⊢ ((???%) → ?); #Haccess
546  [ 1,6,7: normalize in Hload; destruct (Hload)
547  | 2,3,8: whd in match (load_value_of_type ????);
548     whd in match (load_value_of_type ????);
549     lapply (load_by_value_success_valid_block … Haccess Hload)
550     #Hvalid_block
551     whd in match (load_value_of_type ????) in Hload;
552     <(alloc_loadn_conservation … Halloc … Hvalid_block)
553     @Hload
554  | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
555| 2: @(mi_freeblock … Hmemory_inj)
556| 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
557     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
558     elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
559     whd in match (valid_pointer ??) in ⊢ (% → %);
560     @Zltb_elim_Type0
561     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
562     #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
563     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
564     whd in match (high_bound ??) in ⊢ (% → %);
565     whd in match (update_block ?????);
566     whd in match (eq_block ??);
567     cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
568     #Hbid_neq >Hbid_neq
569     cases (eq_region br' r) normalize #H @H
570| 4: @(mi_region … Hmemory_inj)
571| 5: @(mi_nonalias … Hmemory_inj)
572qed.
573
574(* ---------------------------------------------------------- *)
575(* Lemma 40 of the paper of Leroy & Blazy on the memory model
576 * and related lemmas *)
577
578lemma bestorev_beloadv_conservation :
579  ∀mA,mB,wb,wo,v.
580    bestorev mA (mk_pointer wb wo) v = Some ? mB →
581    ∀rb,ro. eq_block wb rb = false →
582    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
583#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
584whd in ⊢ (??%%);
585elim mB in Hstore; #contentsB #nextblockB #HnextblockB
586normalize in ⊢ (% → ?);
587cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
588[ 2: #Habsurd destruct (Habsurd) ]
589cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo))
590       then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) 
591       else false) normalize nodelta
592[ 2: #Habsurd destruct (Habsurd) ]
593#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
594cases rr cases wr normalize try //
595@(eqZb_elim … rid wid)
596[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
597try //
598qed.
599
600(* lift [bestorev_beloadv_conservation to [loadn] *)
601lemma bestorev_loadn_conservation :
602  ∀mA,mB,n,wb,wo,v.
603    bestorev mA (mk_pointer wb wo) v = Some ? mB →
604    ∀rb,ro. eq_block wb rb = false →
605    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
606#mA #mB #n
607elim n
608[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
609| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
610     whd in ⊢ (??%%);
611     >(bestorev_beloadv_conservation … Hstore … Hneq)
612     >(Hind … Hstore … Hneq) @refl
613] qed.
614
615(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
616lemma bestorev_load_value_of_type_conservation :
617  ∀mA,mB,wb,wo,v.
618    bestorev mA (mk_pointer wb wo) v = Some ? mB →
619    ∀rb,ro. eq_block wb rb = false →
620    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
621#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
622cases ty
623[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
624| #structname #fieldspec | #unionname #fieldspec | #id ]
625//
626[ 1: elim sz ]
627whd in ⊢ (??%%);
628>(bestorev_loadn_conservation … Hstore … Hneq) @refl
629qed.
630
631(* lift [bestorev_load_value_of_type_conservation] to storen *)
632lemma storen_load_value_of_type_conservation :
633  ∀l,mA,mB,wb,wo.
634    storen mA (mk_pointer wb wo) l = Some ? mB →
635    ∀rb,ro. eq_block wb rb = false →
636    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
637#l elim l
638[ 1: #mA #mB #wb #wo normalize #Heq destruct //
639| 2: #hd #tl #Hind #mA #mB #wb #wo #Hstoren
640     cases (some_inversion ????? Hstoren) #mA' * #Hbestorev #Hstoren'
641     whd in match (shift_pointer ???) in Hstoren':(??%?); #rb #ro #Hneq_block #ty
642     lapply (Hind ???? Hstoren' … ro … Hneq_block ty) #Heq1
643     lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2
644     //
645] qed.     
646
647definition typesize' ≝ λty. typesize (typ_of_type ty).
648
649lemma storen_load_value_of_type_conservation_in_block_high :
650  ∀E,mA,mB,mC,wo,l.
651    memory_inj E mA mB →
652    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
653    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
654    high_bound mA b1 + Zoo delta < Zoo wo →
655    ∀ty,off.
656       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
657       low_bound … mA b1 ≤ Zoo off →
658       Zoo off < high_bound … mA b1 →
659       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
660       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
661#E #mA #mB #mC #wo #data #Hinj #blo #Hstoren #b1 #delta #Hembed #Hhigh #ty
662(* need some stuff asserting that if a ptr is valid at the start of a write it's valid at the end. *)
663cases data in Hstoren;
664[ 1: normalize in ⊢ (% → ?); #Heq destruct //
665| 2: #xd #data ]
666#Hstoren
667cases ty
668[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
669| #structname #fieldspec | #unionname #fieldspec | #id ]#off #Hofflt #Hlow_load #Hhigh_load try @refl
670whd in match (load_value_of_type ????) in ⊢ (??%%);
671[ 1: lapply (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hbefore #Hafter
672     lapply Hofflt -Hofflt lapply Hlow_load -Hlow_load lapply Hhigh_load -Hhigh_load
673     lapply off -off whd in match typesize'; normalize nodelta     
674     generalize in match (typesize ?); #n elim n try //
675     #n' #Hind #o #Hhigh_load #Hlow_load #Hlt
676     whd in match (loadn ???) in ⊢ (??%%);
677     whd in match (beloadv ??) in ⊢ (??%%);
678     cases (valid_pointer_to_Prop … Hbefore) * #HltB_store #HlowB_store #HhighB_store
679     cases (valid_pointer_to_Prop … Hafter) * #HltC_store #HlowC_store #HhighC_store
680     >(Zlt_to_Zltb_true … HltB_store) >(Zlt_to_Zltb_true … HltC_store) normalize nodelta
681     cut (Zleb (low (blocks mB blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
682     [ 1: (* Notice that:
683                low mA b1 ≤ o < high mA b1
684             hence, since E b1 = 〈blo, delta〉 with delta >= 0
685                low mB blo ≤ (low mA b1 + delta) ≤ o+delta < (high mA b1 + delta) ≤ high mB blo *)
686          @cthulhu ]
687     #HA >HA >andb_lsimpl_true -HA
688     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mB blo)) = true)
689     [ 1: (* Same argument as above *) @cthulhu ]
690     #HA >HA normalize nodelta -HA
691     cut (Zleb (low (blocks mC blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true)
692     [ 1: (* Notice that storen does not modify the bounds of a block. Related lemma present in [MemProperties].
693             This cut follows from this lemma (which needs some info on the size of the data written, which we
694             have but must make explicit) and from the first cut. *)
695          @cthulhu ]         
696     #HA >HA >andb_lsimpl_true -HA
697     cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mC blo)) = true)
698     [ 1: (* Same argument as above *) @cthulhu ]
699     #HA >HA normalize nodelta -HA
700     normalize in match (bitvector_of_nat ??); whd in match (shift_pointer ???);
701     whd in match (shift_offset ???); >commutative_addition_n >associative_addition_n
702     lapply (Hind (mk_offset (addition_n offset_size (sign_ext 2 ? [[false; true]]) (offv o))) ???)
703     [ 1: (* Provable from Hlt *) @cthulhu
704     | 2: (* Provable from Hlow_load, need to make a "succ" commute from bitvector to Z *) @cthulhu
705     | 3: (* Provable from Hlt, again *) @cthulhu ]
706     cases (loadn mB (mk_pointer blo
707              (mk_offset (addition_n ? (addition_n ?
708                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
709     normalize nodelta                 
710     cases (loadn mC (mk_pointer blo
711              (mk_offset (addition_n ? (addition_n ?
712                 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n')
713     normalize nodelta try //
714     [ 1,2: #l #Habsurd destruct ]
715     #l1 #l2 #Heq
716     cut (contents (blocks mB blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) =
717          contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
718     [ 1: (* Follows from Hhigh, indirectly *) @cthulhu ]
719     #Hcontents_eq >Hcontents_eq whd in match (be_to_fe_value ??) in ⊢ (??%%);
720     cases (contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))))
721     normalize nodelta try //
722     (* Ok this is going to be more painful than what I thought. *)
723     @cthulhu
724| *: @cthulhu
725] qed.
726
727lemma storen_load_value_of_type_conservation_in_block_low :
728  ∀E,mA,mB,mC,wo,l.
729    memory_inj E mA mB →
730    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
731    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
732    Zoo wo < low_bound mA b1 + Zoo delta →
733    ∀ty,off.
734       Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 →
735       low_bound … mA b1 ≤ Zoo off →
736       Zoo off < high_bound … mA b1 →
737       load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) =
738       load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))).
739@cthulhu
740qed.
741
742(* Writing in the "extended" part of a memory preserves the underlying injection. *)
743lemma bestorev_memory_inj_to_load_sim :
744  ∀E,mA,mB,mC.
745  ∀Hext:memory_inj E mA mB.
746  ∀block2. ∀i : offset. ∀ty : type.
747  (∀block1,delta.
748    E block1 = Some ? 〈block2, delta〉 →
749    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
750  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
751  load_sim_ptr E mA mC.
752#E #mA #mB #mC #Hinj #block2 #i #storety
753cases storety
754[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
755| #structname #fieldspec | #unionname #fieldspec | #id ]#Hout #storeval #Hstore whd
756#b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value
757whd in Hstore:(??%?);
758[  1,5,6,7,8: destruct ]
759[ 1:
760lapply (mi_inj … Hinj … Hvalid … Hptr_trans … Hload_value)
761lapply Hload_value -Hload_value
762cases ty
763[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
764| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
765#Hload_value
766(* Prove that the contents of mB where v1 was were untouched. *)
767* #readval' * #Hload_value2 #Hvalue_eq %{readval'} @conj try assumption
768cases (some_inversion ????? Hptr_trans) * #b2' #delta' * #Hembed -Hptr_trans normalize nodelta
769#Heq destruct (Heq)
770@(eq_block_elim  … b2 block2)
771[ 2,4,6,8: #Hblocks_neq <Hload_value2 @sym_eq @(storen_load_value_of_type_conservation … Hstore)
772           @not_eq_block @sym_neq @Hblocks_neq
773| 1,3,5,7: #Heq destruct (Heq) lapply (Hout … Hembed) *
774           [ 1,3,5,7: #Hhigh <Hload_value2 -Hload_value2 @sym_eq
775                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
776                      * * #Hlt #Hlowb_off1 #Hhighb_off1
777                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
778                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
779                      @(storen_load_value_of_type_conservation_in_block_high … Hinj … Hstore … Hembed)
780                      try //
781                      (* remaining stuff provable from Hload_value  *)
782                      @cthulhu
783           | 2,4,6,8: #Hlow <Hload_value2 -Hload_value2 @sym_eq
784                      lapply (load_by_value_success_valid_ptr_aux … Hload_value) //
785                      * * #Hlt #Hlowb_off1 #Hhighb_off1
786                      lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1
787                      lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1
788                      @(storen_load_value_of_type_conservation_in_block_low … Hinj … Hstore … Hembed)
789                      try //
790                      [ 1,3,5,7: (* deductible from Hlow + (sizeof ?) > 0 *) @cthulhu
791                      | 2,4,6,8: (* deductible from Hload_value *) @cthulhu ]
792           ]
793]
794| *: (* exactly the same proof as above  *) @cthulhu ]
795qed.
796
797(* Lift the above result to memory_inj
798 * This is Lemma 40 of Leroy & Blazy *)
799lemma bestorev_memory_inj_to_memory_inj :
800  ∀E,mA,mB,mC.
801  ∀Hext:memory_inj E mA mB.
802  ∀block2. ∀i : offset. ∀ty : type.
803  (∀block1,delta.
804    E block1 = Some ? 〈block2, delta〉 →
805    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
806  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
807  memory_inj E mA mC.
808#E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore %
809lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try //
810cases Hinj #Hsim' #Hnot_valid #Hvalid #Hregion #Hnonalias try assumption
811#p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
812cases ty in Hstore;
813[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
814| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
815whd in ⊢ ((??%?) → ?);
816[ 1,4,5,6,7: #Habsurd destruct ]
817cases (fe_to_be_values ??)
818[ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl
819| *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_
820     @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh
821     @conj try @conj try assumption >Hnext try //
822     cases (Hbounds (pblock p')) #HA #HB
823     whd in match (low_bound ??); whd in match (high_bound ??);
824     >HA >HB try assumption
825] qed.
826
827(* ---------------------------------------------------------- *)
828(* Lemma 41 of the paper of Leroy & Blazy on the memory model
829 * and related lemmas *)
830
831(* The back-end might contain something similar to this lemma. *)
832lemma be_to_fe_value_ptr :
833  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
834#b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
835cases br normalize nodelta >eqZb_z_z normalize nodelta
836cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
837<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
838* //
839qed.
840
841lemma value_eq_to_be_and_back_again :
842  ∀E,ty,v1,v2.
843  value_eq E v1 v2 →
844  ast_typ_consistent_with_value ty v1 →
845  ast_typ_consistent_with_value ty v2 →
846  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)).
847#E #ty #v1 #v2 #Hvalue_eq
848@(value_eq_inversion … Hvalue_eq) try //
849[ 1: cases ty //
850| 2: #sz #i cases ty
851     [ 2: @False_ind
852     | 1: #sz' #sg #H whd in ⊢ (% → ?); #Heq
853          lapply (fe_to_be_to_fe_value … H) #H >H // ]
854| 3: #p1 #p2 #Hembed cases ty
855     [ 1: #sz #sg @False_ind
856     | 2: #_ #_
857          cases p1 in Hembed; #b1 #o1
858          cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H
859          cases (some_inversion ????? H) * #b3 #o3 * #Hembed
860          normalize nodelta #Heq >be_to_fe_value_ptr >be_to_fe_value_ptr
861          destruct %4 whd in match (pointer_translation ??);
862          >Hembed normalize nodelta @refl
863     ]
864] qed.
865
866lemma storen_parallel_memory_exists :
867  ∀E,m1,m2,m1',b1,i,b2,delta,ty,v1,v2.
868  memory_inj E m1 m2 →
869  value_eq E v1 v2 →
870  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
871  E b1 = Some ? 〈b2, delta〉 →
872  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'.
873@cthulhu qed.
874  (*
875#E #m1 #m2 #m1' #b1 #i #b2 #delta #ty #v1 #v2 #Hinj #Hvalue_eq
876@(value_eq_inversion … Hvalue_eq)
877[ 1: #v #Hstoren *)
878     
879
880lemma storen_parallel_aux :
881  ∀E,m1,m2.
882  ∀Hinj:memory_inj E m1 m2.
883  ∀v1,v2. value_eq E v1 v2 →
884  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
885  ∀ty,i,m1'.
886  ast_typ_consistent_with_value ty v1 →
887  ast_typ_consistent_with_value ty v2 → 
888  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
889  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
890        memory_inj E m1' m2'.
891#E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hok1 #Hok2
892#Hstoren lapply (storen_to_valid_pointer_fe_to_be … Hstoren)
893* * * #Hblocks_eq1 #Hnextblock1 #Hvalid_m1 #Hvalid_m1'
894lapply (mi_valid_pointers … Hinj … (mk_pointer b1 i) (mk_pointer b2 (offset_plus i delta)) Hvalid_m1 ?)
895[ 1: whd in ⊢ (??%%); >Hembed @refl ]
896#Hvalid_m2
897cases (valid_pointer_to_Prop … Hvalid_m2) * #Hnextblock2 #Hlow2 #Hhigh2
898@cthulhu
899qed.
900
901lemma foo :
902  ∀E,m1,m2.
903  ∀Hinj:memory_inj E m1 m2.
904  ∀v1,v2. value_eq E v1 v2 →
905  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
906  ∀ty,i,m1'. store_value_of_type ty m1 b1 i v1 = Some ? m1' →
907  ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧
908         memory_inj E m1' m2'.
909#E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hstore
910@cthulhu qed.
911
912(* ------------------------------------------------------------------------- *)
913(* Commutation results of standard unary and binary operations with value_eq. *)
914
915lemma unary_operation_value_eq :
916  ∀E,op,v1,v2,ty.
917   value_eq E v1 v2 →
918   ∀r1.
919   sem_unary_operation op v1 ty = Some ? r1 →
920    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
921#E #op #v1 #v2 #ty #Hvalue_eq #r1
922inversion Hvalue_eq
923[ 1: #v #Hv1 #Hv2 destruct
924     cases op normalize
925     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
926          normalize #Habsurd destruct (Habsurd)
927     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
928          normalize #Habsurd destruct (Habsurd)
929     | 2: #Habsurd destruct (Habsurd) ]
930| 2: #vsz #i #Hv1 #Hv2 #_
931     cases op
932     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
933          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
934          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
935               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
936               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
937               //
938          | *: #Habsurd destruct (Habsurd) ]
939     | 2: whd in match (sem_unary_operation ???);     
940          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
941     | 3: whd in match (sem_unary_operation ???);
942          cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
943          normalize nodelta
944          whd in ⊢ ((??%?) → ?);
945          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
946               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
947          | *: #Habsurd destruct (Habsurd) ] ]
948| 3: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
949     cases op normalize nodelta
950     [ 1: cases ty   [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
951          whd in match (sem_notbool ??);
952          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
953     | 2: normalize #Habsurd destruct (Habsurd)
954     | 3: cases ty    [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
955          whd in match (sem_neg ??);
956          #Heq1 destruct ]
957| 4: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
958     cases op normalize nodelta
959     [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
960          whd in match (sem_notbool ??);         
961          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
962     | 2: normalize #Habsurd destruct (Habsurd)
963     | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
964          whd in match (sem_neg ??);         
965          #Heq1 destruct ]
966]
967qed.
968
969(* value_eq lifts to addition *)
970lemma add_value_eq :
971  ∀E,v1,v2,v1',v2',ty1,ty2.
972   value_eq E v1 v2 →
973   value_eq E v1' v2' →
974   (* memory_inj E m1 m2 →  This injection seems useless TODO *)
975   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
976           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
977#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
978@(value_eq_inversion E … Hvalue_eq1)
979[ 1: | 2: #sz #i | 3: | 4: #p1 #p2 #Hembed ]
980[ 1: whd in match (sem_add ????); normalize nodelta
981     cases (classify_add ty1 ty2) normalize nodelta
982     [ 1: #sz #sg | 2: #n #ty #sz #sg | 3: #n #sz #sg #ty | 4: #ty1' #ty2' ]
983     #Habsurd destruct (Habsurd)
984| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
985     cases (classify_add ty1 ty2) normalize nodelta
986     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
987     [ 2,4: #Habsurd destruct (Habsurd) ]
988     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
989     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
990     [ 1,2,4,5,7: #Habsurd destruct (Habsurd) ]
991     [ 1: @intsize_eq_elim_elim
992          [ 1: #_ #Habsurd destruct (Habsurd)
993          | 2: #Heq destruct (Heq) normalize nodelta
994               #Heq destruct (Heq)
995               /3 by ex_intro, conj, vint_eq/ ]
996     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
997          /3 by ex_intro, conj, vint_eq/
998     | 3: #Heq destruct (Heq)
999          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
1000          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
1001          @vptr_eq whd in match (pointer_translation ??);
1002          cases (E b1') in Hembed;
1003          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1004          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
1005               whd in match (shift_pointer_n ????);
1006               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
1007                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i))
1008               [ 1: whd in match (offset_plus ??);
1009                    whd in match (shift_offset_n ????) in ⊢ (??%%);
1010                    >commutative_addition_n >associative_addition_n
1011                    <(commutative_addition_n … (offv offset) (offv o1')) @refl ]
1012               #Heq >Heq @refl ]
1013     ]
1014(* | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
1015     cases (classify_add ty1 ty2) normalize nodelta
1016     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
1017     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1018     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1019     [ 1: | 2: #sz' #i'| 3: | 4: #p1' #p2' #Hembed' ]
1020     [ 1,3,4,5,7: #Habsurd destruct (Habsurd) ]
1021     #Heq >Heq %{r1} @conj //
1022     /3 by ex_intro, conj, vfloat_eq/ *)
1023| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
1024     cases (classify_add ty1 ty2) normalize nodelta
1025     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
1026     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1027     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1028     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
1029     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1030     @eq_bv_elim
1031     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
1032     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
1033| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
1034     cases (classify_add ty1 ty2) normalize nodelta
1035     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
1036     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1037     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1038     [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ]
1039     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1040     #Heq destruct (Heq)
1041     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
1042     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
1043     elim p1 in Hembed; #b1 #o1 normalize nodelta
1044     cases (E b1)
1045     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1046     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
1047          whd in match (shift_pointer_n ????);
1048          whd in match (shift_offset_n ????) in ⊢ (??%%);
1049          whd in match (offset_plus ??);
1050          whd in match (offset_plus ??);
1051          >commutative_addition_n >(associative_addition_n … offset_size ?)
1052          >(commutative_addition_n ? (offv offset) ?) @refl
1053     ]
1054] qed.
1055
1056lemma subtraction_delta : ∀x,y,delta.
1057  subtraction offset_size
1058    (addition_n offset_size x delta)
1059    (addition_n offset_size y delta) =
1060  subtraction offset_size x y.
1061#x #y #delta whd in match subtraction; normalize nodelta
1062(* Remove all the equal parts on each side of the equation. *)
1063<associative_addition_n
1064>two_complement_negation_plus
1065<(commutative_addition_n … (two_complement_negation ? delta))
1066>(associative_addition_n ? delta) >bitvector_opp_addition_n
1067>(commutative_addition_n ? (zero ?)) >neutral_addition_n
1068@refl
1069qed.
1070
1071(* Offset subtraction is invariant by translation *)
1072lemma sub_offset_translation :
1073 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
1074#n #x #y #delta
1075whd in match (sub_offset ???) in ⊢ (??%%);
1076elim x #x' elim y #y' elim delta #delta'
1077whd in match (offset_plus ??);
1078whd in match (offset_plus ??);
1079>subtraction_delta @refl
1080qed.
1081
1082(* value_eq lifts to subtraction *)
1083lemma sub_value_eq :
1084  ∀E,v1,v2,v1',v2',ty1,ty2.
1085   value_eq E v1 v2 →
1086   value_eq E v1' v2' →
1087   ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
1088           ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1089#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1090@(value_eq_inversion E … Hvalue_eq1)
1091[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
1092[ 1: whd in match (sem_sub ????); normalize nodelta
1093     cases (classify_sub ty1 ty2) normalize nodelta
1094     [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ]
1095     #Habsurd destruct (Habsurd)
1096| 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1097     cases (classify_sub ty1 ty2) normalize nodelta     
1098     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
1099     [ 2,3,4: #Habsurd destruct (Habsurd) ]
1100     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1101     [  | #sz' #i' | | #p1' #p2' #Hembed' ]
1102     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1103     @intsize_eq_elim_elim
1104      [ 1: #_ #Habsurd destruct (Habsurd)
1105      | 2: #Heq destruct (Heq) normalize nodelta
1106           #Heq destruct (Heq)
1107          /3 by ex_intro, conj, vint_eq/           
1108      ]
1109(*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1110     cases (classify_sub ty1 ty2) normalize nodelta
1111     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
1112     [ 1,4: #Habsurd destruct (Habsurd) ]
1113     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1114     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
1115     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
1116     #Heq destruct (Heq)
1117     /3 by ex_intro, conj, vfloat_eq/ *)
1118| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1119     cases (classify_sub ty1 ty2) normalize nodelta
1120     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
1121     [ 1,4: #Habsurd destruct (Habsurd) ]
1122     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1123     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
1124     [ 1,2,4,5,7,8: #Habsurd destruct (Habsurd) ]
1125     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
1126                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
1127     | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
1128| 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1129     cases (classify_sub ty1 ty2) normalize nodelta
1130     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
1131     [ 1,4: #Habsurd destruct (Habsurd) ]
1132     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1133     [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ]
1134     [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ]
1135     #Heq destruct (Heq)
1136     [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
1137          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
1138          elim p1 in Hembed; #b1 #o1 normalize nodelta
1139          cases (E b1)
1140          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1141          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
1142               whd in match (offset_plus ??) in ⊢ (??%%);
1143               whd in match (neg_shift_pointer_n ????) in ⊢ (??%%);
1144               whd in match (neg_shift_offset_n ????) in ⊢ (??%%);
1145               whd in match (subtraction) in ⊢ (??%%); normalize nodelta
1146               generalize in match (short_multiplication ???); #mult
1147               /3 by associative_addition_n, commutative_addition_n, refl/
1148          ]
1149     | 2: lapply Heq @eq_block_elim
1150          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
1151          | 1: #Hpblock1_eq normalize nodelta
1152               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
1153               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
1154               whd in ⊢ ((??%?) → (??%?) → ?);
1155               cases (E b1') normalize nodelta
1156               [ 1: #Habsurd destruct (Habsurd) ]
1157               * #dest_block #dest_off normalize nodelta
1158               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_b_b normalize nodelta
1159               cases (eqb (sizeof tsg) O) normalize nodelta
1160               [ 1: #Habsurd destruct (Habsurd)
1161               | 2: >(sub_offset_translation 32 off1 off1' dest_off)
1162                    cases (division_u 31
1163                            (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
1164                            (repr (sizeof tsg)))
1165                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
1166                    | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
1167                         /3 by ex_intro, conj, vint_eq/ ]
1168    ] ] ]
1169] qed.
1170
1171
1172lemma mul_value_eq :
1173  ∀E,v1,v2,v1',v2',ty1,ty2.
1174   value_eq E v1 v2 →
1175   value_eq E v1' v2' →
1176   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
1177           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1178#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1179@(value_eq_inversion E … Hvalue_eq1)
1180[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
1181[ 1: whd in match (sem_mul ????); normalize nodelta
1182     cases (classify_aop ty1 ty2) normalize nodelta
1183     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1184     #Habsurd destruct (Habsurd)
1185| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
1186     cases (classify_aop ty1 ty2) normalize nodelta
1187     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1188     [ 2: #Habsurd destruct (Habsurd) ]
1189     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1190     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
1191     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1192     @intsize_eq_elim_elim
1193      [ 1: #_ #Habsurd destruct (Habsurd)
1194      | 2: #Heq destruct (Heq) normalize nodelta
1195           #Heq destruct (Heq)
1196          /3 by ex_intro, conj, vint_eq/           
1197      ]
1198| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
1199     cases (classify_aop ty1 ty2) normalize nodelta
1200     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1201     [ 1,2: #Habsurd destruct (Habsurd) ]
1202| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
1203     cases (classify_aop ty1 ty2) normalize nodelta
1204     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1205     #Habsurd destruct (Habsurd)
1206] qed.     
1207
1208lemma div_value_eq :
1209  ∀E,v1,v2,v1',v2',ty1,ty2.
1210   value_eq E v1 v2 →
1211   value_eq E v1' v2' →
1212   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
1213           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1214#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1215@(value_eq_inversion E … Hvalue_eq1)
1216[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
1217[ 1: whd in match (sem_div ????); normalize nodelta
1218     cases (classify_aop ty1 ty2) normalize nodelta
1219     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1220     #Habsurd destruct (Habsurd)
1221| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
1222     cases (classify_aop ty1 ty2) normalize nodelta
1223     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1224     [ 2: #Habsurd destruct (Habsurd) ]
1225     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1226     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
1227     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1228     elim sg normalize nodelta
1229     @intsize_eq_elim_elim
1230     [ 1,3: #_ #Habsurd destruct (Habsurd)
1231     | 2,4: #Heq destruct (Heq) normalize nodelta
1232            @(match (division_s (bitsize_of_intsize sz') i i') with
1233              [ None ⇒ ?
1234              | Some bv' ⇒ ? ])
1235            [ 1: normalize  #Habsurd destruct (Habsurd)
1236            | 2: normalize #Heq destruct (Heq)
1237                 /3 by ex_intro, conj, vint_eq/
1238            | 3,4: elim sz' in i' i; #i' #i
1239                   normalize in match (pred_size_intsize ?);
1240                   generalize in match division_u; #division_u normalize
1241                   @(match (division_u ???) with
1242                    [ None ⇒ ?
1243                    | Some bv ⇒ ?]) normalize nodelta
1244                   #H destruct (H)
1245                  /3 by ex_intro, conj, vint_eq/ ]
1246     ]
1247| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
1248     cases (classify_aop ty1 ty2) normalize nodelta
1249     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1250     [ 1,2: #Habsurd destruct (Habsurd) ]
1251| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
1252     cases (classify_aop ty1 ty2) normalize nodelta
1253     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1254     #Habsurd destruct (Habsurd)
1255] qed.     
1256
1257lemma mod_value_eq :
1258  ∀E,v1,v2,v1',v2',ty1,ty2.
1259   value_eq E v1 v2 →
1260   value_eq E v1' v2' →
1261   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
1262           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1263#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1264@(value_eq_inversion E … Hvalue_eq1)
1265[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
1266[ 1: whd in match (sem_mod ????); normalize nodelta
1267     cases (classify_aop ty1 ty2) normalize nodelta
1268     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1269     #Habsurd destruct (Habsurd)
1270| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
1271     cases (classify_aop ty1 ty2) normalize nodelta
1272     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1273     [ 2: #Habsurd destruct (Habsurd) ]
1274     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1275     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
1276     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1277     elim sg normalize nodelta
1278     @intsize_eq_elim_elim
1279     [ 1,3: #_ #Habsurd destruct (Habsurd)
1280     | 2,4: #Heq destruct (Heq) normalize nodelta
1281            @(match (modulus_s (bitsize_of_intsize sz') i i') with
1282              [ None ⇒ ?
1283              | Some bv' ⇒ ? ])
1284            [ 1: normalize  #Habsurd destruct (Habsurd)
1285            | 2: normalize #Heq destruct (Heq)
1286                 /3 by ex_intro, conj, vint_eq/
1287            | 3,4: elim sz' in i' i; #i' #i
1288                   generalize in match modulus_u; #modulus_u normalize
1289                   @(match (modulus_u ???) with
1290                    [ None ⇒ ?
1291                    | Some bv ⇒ ?]) normalize nodelta
1292                   #H destruct (H)
1293                  /3 by ex_intro, conj, vint_eq/ ]
1294     ]     
1295| *: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
1296     cases (classify_aop ty1 ty2) normalize nodelta #foo #bar #Habsurd destruct (Habsurd)
1297] qed.
1298
1299(* boolean ops *)
1300lemma and_value_eq :
1301  ∀E,v1,v2,v1',v2'.
1302   value_eq E v1 v2 →
1303   value_eq E v1' v2' →
1304   ∀r1. (sem_and v1 v1'=Some val r1→
1305           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
1306#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1307@(value_eq_inversion E … Hvalue_eq1)
1308[ 2: #sz #i
1309     @(value_eq_inversion E … Hvalue_eq2)
1310     [ 2: #sz' #i' whd in match (sem_and ??);
1311          @intsize_eq_elim_elim
1312          [ 1: #_ #Habsurd destruct (Habsurd)
1313          | 2: #Heq destruct (Heq) normalize nodelta
1314               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
1315] ]
1316normalize in match (sem_and ??); #arg1 destruct
1317normalize in match (sem_and ??); #arg2 destruct
1318normalize in match (sem_and ??); #arg3 destruct
1319normalize in match (sem_and ??); #arg4 destruct
1320qed.
1321
1322lemma or_value_eq :
1323  ∀E,v1,v2,v1',v2'.
1324   value_eq E v1 v2 →
1325   value_eq E v1' v2' →
1326   ∀r1. (sem_or v1 v1'=Some val r1→
1327           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
1328#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1329@(value_eq_inversion E … Hvalue_eq1)
1330[ 2: #sz #i
1331     @(value_eq_inversion E … Hvalue_eq2)
1332     [ 2: #sz' #i' whd in match (sem_or ??);
1333          @intsize_eq_elim_elim
1334          [ 1: #_ #Habsurd destruct (Habsurd)
1335          | 2: #Heq destruct (Heq) normalize nodelta
1336               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
1337] ]
1338normalize in match (sem_or ??); #arg1 destruct
1339normalize in match (sem_or ??); #arg2 destruct
1340normalize in match (sem_or ??); #arg3 destruct
1341normalize in match (sem_or ??); #arg4 destruct
1342qed.
1343
1344lemma xor_value_eq :
1345  ∀E,v1,v2,v1',v2'.
1346   value_eq E v1 v2 →
1347   value_eq E v1' v2' →
1348   ∀r1. (sem_xor v1 v1'=Some val r1→
1349           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
1350#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1351@(value_eq_inversion E … Hvalue_eq1)
1352[ 2: #sz #i
1353     @(value_eq_inversion E … Hvalue_eq2)
1354     [ 2: #sz' #i' whd in match (sem_xor ??);
1355          @intsize_eq_elim_elim
1356          [ 1: #_ #Habsurd destruct (Habsurd)
1357          | 2: #Heq destruct (Heq) normalize nodelta
1358               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
1359] ]
1360normalize in match (sem_xor ??); #arg1 destruct
1361normalize in match (sem_xor ??); #arg2 destruct
1362normalize in match (sem_xor ??); #arg3 destruct
1363normalize in match (sem_xor ??); #arg4 destruct
1364qed.
1365
1366lemma shl_value_eq :
1367  ∀E,v1,v2,v1',v2'.
1368   value_eq E v1 v2 →
1369   value_eq E v1' v2' →
1370   ∀r1. (sem_shl v1 v1'=Some val r1→
1371           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
1372#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1373@(value_eq_inversion E … Hvalue_eq1)
1374[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
1375[ 2:
1376     @(value_eq_inversion E … Hvalue_eq2)
1377     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
1378     [ 2: whd in match (sem_shl ??);
1379          cases (lt_u ???) normalize nodelta
1380          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
1381          | 2: #Habsurd destruct (Habsurd)
1382          ]
1383     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
1384| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
1385qed.
1386
1387lemma shr_value_eq :
1388  ∀E,v1,v2,v1',v2',ty,ty'.
1389   value_eq E v1 v2 →
1390   value_eq E v1' v2' →
1391   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
1392           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
1393#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
1394@(value_eq_inversion E … Hvalue_eq1)
1395[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
1396whd in match (sem_shr ????); whd in match (sem_shr ????);
1397[ 1: cases (classify_aop ty ty') normalize nodelta
1398     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1399     #Habsurd destruct (Habsurd)
1400| 2: cases (classify_aop ty ty') normalize nodelta
1401     [ 1: #sz #sg | 2: #ty1' #ty2' ]
1402     [ 2: #Habsurd destruct (Habsurd) ]
1403     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1404     [  | #sz' #i' |  |  #p1' #p2' #Hembed' ]
1405     [ 1,3,4: #Habsurd destruct (Habsurd) ]
1406     elim sg normalize nodelta
1407     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
1408     /3 by ex_intro, conj, refl, vint_eq/
1409| *: cases (classify_aop ty ty') normalize nodelta
1410     #foo #bar
1411     #Habsurd destruct (Habsurd)
1412] qed.     
1413
1414lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
1415* #delta * #x * #y
1416whd in match (offset_plus ??);
1417whd in match (offset_plus ??);
1418whd in match cmp_offset; normalize nodelta
1419whd in match eq_offset; normalize nodelta
1420@(eq_bv_elim … x y)
1421[ 1: #Heq >Heq >eq_bv_true @refl
1422| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
1423     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
1424     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
1425] qed.     
1426
1427lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
1428* #delta * #x * #y
1429whd in match (offset_plus ??);
1430whd in match (offset_plus ??);
1431whd in match cmp_offset; normalize nodelta
1432whd in match eq_offset; normalize nodelta
1433@(eq_bv_elim … x y)
1434[ 1: #Heq >Heq >eq_bv_true @refl
1435| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
1436     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
1437     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
1438] qed.
1439
1440
1441(* /!\ Here is the source of all sadness (op = lt) /!\ *)
1442axiom cmp_offset_translation : ∀op,delta,x,y.
1443   cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
1444
1445(* 5 Nov. 2012 : the rest of the stuff doesn't checks anymore. Not a big deal, it was here
1446 * for historical purposes, and for potential inspiration for Clight to Cminor. I leave the
1447 * code commented for future reference.
1448 *)
1449
1450(*
1451lemma cmp_value_eq :
1452  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
1453   value_eq E v1 v2 →
1454   value_eq E v1' v2' →
1455   memory_inj E m1 m2 →   
1456   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
1457           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
1458#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
1459elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj
1460whd in match (sem_cmp ??????) in ⊢ ((??%?) → %);
1461cases (classify_cmp ty ty') normalize nodelta
1462[ 1: #tsz #tsg
1463     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
1464     [ 1: #v #Habsurd destruct (Habsurd)
1465     | 3: #f #Habsurd destruct (Habsurd)
1466     | 4: #Habsurd destruct (Habsurd)
1467     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
1468     #sz #i
1469     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1470     [ 1: #v #Habsurd destruct (Habsurd)
1471     | 3: #f #Habsurd destruct (Habsurd)
1472     | 4: #Habsurd destruct (Habsurd)
1473     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
1474     #sz' #i' cases tsg normalize nodelta
1475     @intsize_eq_elim_elim
1476     [ 1,3: #Hneq #Habsurd destruct (Habsurd)
1477     | 2,4: #Heq destruct (Heq) normalize nodelta
1478            #Heq destruct (Heq)
1479            [ 1: cases (cmp_int ????) whd in match (of_bool ?);
1480            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
1481              /3 by ex_intro, conj, vint_eq/ ]
1482| 3: #fsz
1483     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
1484     [ 1: #v #Habsurd destruct (Habsurd)
1485     | 2: #sz #i #Habsurd destruct (Habsurd)
1486     | 4: #Habsurd destruct (Habsurd)
1487     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
1488     #f
1489     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1490     [ 1: #v #Habsurd destruct (Habsurd)
1491     | 2: #sz #i #Habsurd destruct (Habsurd)
1492     | 4: #Habsurd destruct (Habsurd)
1493     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
1494     #f'
1495     #Heq destruct (Heq) cases (Fcmp op f f')
1496     /3 by ex_intro, conj, vint_eq/
1497| 4: #ty1 #ty2 #Habsurd destruct (Habsurd)
1498| 2: #optn #typ
1499     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
1500     [ 1: #v #Habsurd destruct (Habsurd)
1501     | 2: #sz #i #Habsurd destruct (Habsurd)
1502     | 3: #f #Habsurd destruct (Habsurd)
1503     | 5: #p1 #p2 #Hembed ]
1504     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1505     [ 1,6: #v #Habsurd destruct (Habsurd)
1506     | 2,7: #sz #i #Habsurd destruct (Habsurd)
1507     | 3,8: #f #Habsurd destruct (Habsurd)
1508     | 5,10: #p1' #p2' #Hembed' ]
1509     [ 2,3: cases op whd in match (sem_cmp_mismatch ?);
1510          #Heq destruct (Heq)
1511          [ 1,3: %{Vfalse} @conj try @refl @vint_eq
1512          | 2,4: %{Vtrue} @conj try @refl @vint_eq ]
1513     | 4: cases op whd in match (sem_cmp_match ?);
1514          #Heq destruct (Heq)
1515          [ 2,4: %{Vfalse} @conj try @refl @vint_eq
1516          | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ]
1517     lapply (mi_valid_pointers … Hinj p1' p2')
1518     lapply (mi_valid_pointers … Hinj p1 p2)         
1519     cases (valid_pointer (mk_mem ???) p1')
1520     [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
1521     cases (valid_pointer (mk_mem ???) p1)
1522     [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
1523     #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
1524     >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
1525     elim p1 in Hembed; #b1 #o1
1526     elim p1' in Hembed'; #b1' #o1'
1527     whd in match (pointer_translation ??);
1528     whd in match (pointer_translation ??);
1529     @(eq_block_elim … b1 b1')
1530     [ 1: #Heq destruct (Heq)
1531          cases (E b1') normalize nodelta
1532          [ 1: #Habsurd destruct (Habsurd) ]
1533          * #eb1' #eo1' normalize nodelta
1534          #Heq1 #Heq2 #Heq3 destruct
1535          >eq_block_b_b normalize nodelta
1536          <cmp_offset_translation
1537          cases (cmp_offset ???) normalize nodelta         
1538          /3 by ex_intro, conj, vint_eq/
1539     | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
1540          cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
1541          * #eb1 #eo1
1542          cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
1543          * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
1544          lapply (H ???? Hneq (refl ??) (refl ??))
1545          #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
1546          elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
1547          /3 by ex_intro, conj, vint_eq/
1548     ]
1549] qed.    *)           
1550
1551(*
1552lemma binary_operation_value_eq :
1553  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
1554   value_eq E v1 v2 →
1555   value_eq E v1' v2' →
1556   memory_inj E m1 m2 →
1557   ∀r1.
1558   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
1559   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
1560#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
1561cases op
1562whd in match (sem_binary_operation ??????);
1563whd in match (sem_binary_operation ??????);
1564[ 1: @add_value_eq try assumption
1565| 2: @sub_value_eq try assumption
1566| 3: @mul_value_eq try assumption
1567| 4: @div_value_eq try assumption
1568| 5: @mod_value_eq try assumption
1569| 6: @and_value_eq try assumption
1570| 7: @or_value_eq try assumption
1571| 8: @xor_value_eq try assumption
1572| 9: @shl_value_eq try assumption
1573| 10: @shr_value_eq try assumption
1574| *: @cmp_value_eq try assumption
1575] qed. *)
1576
1577(*
1578lemma cast_value_eq :
1579 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 →
1580  ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res →
1581  ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'.
1582#E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res
1583@(value_eq_inversion … Hvalue_eq)
1584[ 1: #v normalize #Habsurd destruct (Habsurd)
1585| 2: #vsz #vi whd in match (exec_cast ????);
1586     cases ty
1587     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
1588     normalize nodelta
1589     [ 1,3,7,8,9: #Habsurd destruct (Habsurd)
1590     | 2: @intsize_eq_elim_elim
1591          [ 1: #Hneq #Habsurd destruct (Habsurd)
1592          | 2: #Heq destruct (Heq) normalize nodelta
1593               cases cast_ty
1594               [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
1595               | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
1596               normalize nodelta
1597               [ 1,7,8,9: #Habsurd destruct (Habsurd)
1598               | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
1599               | 3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/
1600               | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
1601                    @eq_bv_elim
1602                    [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta
1603                         whd in match (m_bind ?????);
1604                         #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
1605                    | 2,4,6: #Hneq >eq_intsize_identity normalize nodelta
1606                         whd in match (m_bind ?????);
1607                         #Habsurd destruct (Habsurd) ] ]
1608          ]
1609     | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
1610          @eq_bv_elim
1611          [ 1,3,5: #Heq destruct (Heq) normalize nodelta
1612               whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
1613          | 2,4,6: #Hneq normalize nodelta
1614               whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ]
1615     ]
1616| 3: #f whd in match (exec_cast ????);
1617     cases ty
1618     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
1619     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
1620     normalize nodelta
1621     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
1622     cases cast_ty
1623     [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
1624     | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
1625     normalize nodelta
1626     [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
1627     #Heq destruct (Heq)
1628     [ 1: /3 by ex_intro, conj, vint_eq/
1629     | 2: /3 by ex_intro, conj, vfloat_eq/ ]
1630| 4: whd in match (exec_cast ????);
1631     cases ty
1632     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
1633     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
1634     normalize
1635     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
1636     cases cast_ty normalize nodelta
1637     [ 1,10,19: #Habsurd destruct (Habsurd)
1638     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
1639     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
1640     | 4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
1641     | 5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
1642     | 6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
1643     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
1644     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
1645     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
1646| 5: #p1 #p2 #Hembed whd in match (exec_cast ????);
1647     cases ty
1648     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
1649     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
1650     normalize
1651     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
1652     cases cast_ty normalize nodelta
1653     [ 1,10,19: #Habsurd destruct (Habsurd)
1654     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
1655     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
1656     | 4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption
1657     | 5,14,23: #carrayty #cn #Heq destruct (Heq)
1658                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
1659     | 6,15,24: #ctl #cretty #Heq destruct (Heq)
1660                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
1661     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
1662     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
1663     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
1664qed.
1665
1666lemma bool_of_val_value_eq :
1667 ∀E,v1,v2. value_eq E v1 v2 →
1668   ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b.
1669#E #v1 #v2 #Hvalue_eq #ty #b
1670@(value_eq_inversion … Hvalue_eq) //
1671[ 1: #v #H normalize in H; destruct (H)
1672| 2: #p1 #p2 #Hembed #H @H ] qed.
1673
1674*)
1675(*
1676lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
1677  ∀E:embedding.
1678  ∀Hext:memory_ext E m1 m2.
1679  switch_removal_globals E ? fundef_switch_removal ge ge' →
1680  disjoint_extension en1 m1 en2 m2 ext E Hext →
1681  ext_fresh_for_genv ext ge →
1682  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
1683  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
1684#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
1685@expr_lvalue_ind_combined
1686[ 1: #csz #cty #i #a1
1687     whd in match (exec_expr ????); elim cty
1688     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1689     normalize nodelta
1690     [ 2: cases (eq_intsize csz sz) normalize nodelta
1691          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
1692          | 2: #Habsurd destruct (Habsurd) ]
1693     | 4,5,6: #_ #H destruct (H)
1694     | *: #H destruct (H) ]
1695| 2: #ty #fl #a1
1696     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
1697| 3: *
1698  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
1699  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
1700  #ty whd in ⊢ (% → ?); #Hind try @I
1701  whd in match (Plvalue ???);
1702  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
1703       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
1704       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1705       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
1706           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
1707           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
1708           whd in match (load_value_of_type' ???);
1709           whd in match (load_value_of_type' ???);
1710           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
1711           cases (load_value_of_type ty m1 bl1 o1)
1712           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
1713           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
1714                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
1715                    normalize /4 by ex_intro, conj/
1716  ] ] ]
1717| 4: #v #ty whd * * #b1 #o1 #tr1
1718     whd in match (exec_lvalue' ?????);
1719     whd in match (exec_lvalue' ?????);
1720     lapply (Hdisjoint v)
1721     lapply (Hext_fresh_for_genv v)
1722     cases (mem_assoc_env v ext) #Hglobal
1723     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
1724          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
1725          >(Hglobal (refl ??)) normalize
1726          #Habsurd destruct (Habsurd)
1727     | 2: normalize nodelta
1728          cases (lookup ?? en1 v) normalize nodelta
1729          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
1730               lapply (rg_find_symbol … Hrelated v)
1731               cases (find_symbol ???) normalize
1732               [ 1: #_ #Habsurd destruct (Habsurd)
1733               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
1734                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
1735                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
1736                         %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl
1737                         normalize /2/
1738                ] ]
1739         | 2: #block
1740              cases (lookup ?? en2 v) normalize nodelta
1741              [ 1: #Hfalse @(False_ind … Hfalse)
1742              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
1743                   %{〈b, zero_offset, E0〉} @conj try @refl
1744                   normalize /2/
1745    ] ] ]
1746| 5: #e #ty whd in ⊢ (% → %);
1747     whd in match (exec_lvalue' ?????);
1748     whd in match (exec_lvalue' ?????);
1749     cases (exec_expr ge en1 m1 e)
1750     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
1751          * elim v1 normalize nodelta
1752          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
1753          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
1754          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
1755          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
1756          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
1757               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
1758               #Hvalue_eq normalize
1759               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
1760               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
1761               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
1762               %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl
1763               normalize @conj // ]
1764     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
1765| 6: #ty #e #ty'
1766     #Hsim @(exec_lvalue_expr_elim … Hsim)
1767     cases ty
1768     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1769     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
1770     #tr #H @conj try @refl try assumption
1771| 7: #ty #op #e
1772     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
1773     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
1774     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
1775     [ 1: #_ @I
1776     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
1777           normalize /2/ ]
1778| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
1779     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
1780     cases (exec_expr ge en1 m1 e2) in Hsim2;
1781     [ 2: #error // ]
1782     * #val #trace normalize in ⊢ (% → ?); #Hsim2
1783     elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2
1784     whd in match (m_bind ?????); whd in match (m_bind ?????);
1785     lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext))
1786     cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1)
1787     [ 1: #_ // ]
1788     #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq  #Hvalue_eq_opval
1789     >Hopval_eq normalize destruct /2 by conj/
1790| 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
1791     #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty)
1792     cases (exec_cast m1 v1 (typeof e) cast_ty)
1793     [ 2: #error #_ normalize @I
1794     | 1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????);
1795          * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta
1796          @conj // ]
1797| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
1798     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
1799     lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1))
1800     cases (exec_bool_of_val ? (typeof e1)) #b
1801     [ 2: #_ normalize @I ]
1802     #H lapply (H ? (refl ??)) #Hexec >Hexec normalize
1803     cases b normalize nodelta
1804     [ 1: (* true branch *)
1805          cases (exec_expr ge en1 m1 e2) in Hsim2;
1806          [ 2: #error normalize #_ @I
1807          | 1: * #e2v #e2tr normalize #H elim (H ? (refl ??))
1808               * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize
1809                    destruct @conj try // ]
1810     | 2: (* false branch *)
1811          cases (exec_expr ge en1 m1 e3) in Hsim3;
1812          [ 2: #error normalize #_ @I
1813          | 1: * #e3v #e3tr normalize #H elim (H ? (refl ??))
1814               * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize
1815               destruct @conj // ] ]
1816| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
1817     @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq
1818     lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1))     
1819     cases (exec_bool_of_val v1 (typeof e1))
1820     [ 2,4:  #error #_ normalize @I ]
1821     #b cases b #H lapply (H ? (refl ??)) #Heq >Heq
1822     whd in match (m_bind ?????);
1823     whd in match (m_bind ?????);
1824     [ 2,3: normalize @conj try @refl try @vint_eq ]
1825     cases (exec_expr ge en1 m1 e2) in Hsim2;
1826     [ 2,4: #error #_ normalize @I ]
1827     * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??))
1828     * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta
1829     lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2))
1830     cases (exec_bool_of_val v2 (typeof e2))
1831     [ 2,4: #error #_ normalize @I ]
1832     #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta
1833     destruct @conj try @conj //
1834     cases b2 whd in match (of_bool ?); @vint_eq
1835| 13: #ty #ty' cases ty
1836     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n
1837     | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1838     whd in match (exec_expr ????); whd
1839     * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉}
1840     @conj try @refl @conj //
1841| 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta
1842    whd in match (exec_lvalue' ?????);
1843    whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
1844    whd in match (typeof ?);
1845    cases aggregty in Hsim;
1846    [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
1847    | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
1848    normalize nodelta #Hsim
1849    [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
1850    whd in match (m_bind ?????);
1851    whd in match (m_bind ?????);
1852    whd in match (exec_lvalue ge en1 m1 (Expr ed ?));
1853    cases (exec_lvalue' ge en1 m1 ed ?) in Hsim;
1854    [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
1855    * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??))
1856    * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq
1857    whd in match (exec_lvalue ????); >Hexec normalize nodelta
1858    [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj //
1859         normalize @conj // ]
1860    cases (field_offset i fl')
1861    [ 2: #error normalize #Habsurd destruct (Habsurd) ]
1862    #offset whd in match (m_bind ?????); #Heq destruct (Heq)
1863    whd in match (m_bind ?????);
1864    %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj
1865    destruct // normalize nodelta @conj try @refl @vptr_eq
1866    -H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq
1867    whd in match (pointer_translation ??);     
1868    whd in match (pointer_translation ??);
1869    cases (E b)
1870    [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
1871    * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq)
1872    cut (offset_plus (mk_offset (addition_n offset_size
1873                                      (offv o1)
1874                                      (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 offset)))) o'
1875          = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset)))
1876    [ whd in match (shift_offset ???) in ⊢ (???%);
1877      whd in match (offset_plus ??) in ⊢ (??%%);
1878      /3 by associative_addition_n, commutative_addition_n, refl/ ]
1879    #Heq >Heq @refl
1880| 15: #ty #l #e #Hsim
1881     @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj //
1882| 16: *
1883  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
1884  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
1885  #ty normalize in ⊢ (% → ?);
1886  [ 3,4,13: @False_ind
1887  | *: #_ normalize #a1 #Habsurd destruct (Habsurd) ]
1888] qed. *)
Note: See TracBrowser for help on using the repository browser.