Context Navigation

memoryInjections.ma @ 2486

Last change on this file since 2486 was 2483, checked in by garnier, 8 years ago
Memory injections for Clight to Cminor, partially axiomatized.
File size: 101.1 KB

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

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format