source: src/Clight/MemProperties.ma @ 2448

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

Comitting current state of switch removal.

File size: 38.9 KB
Line 
1(* This file is dedicated to general properties of memory w.r.t. writing and reading to it.
2   It also contains facts about related functions and predicates, such as valid_pointer. *)
3   
4include "Clight/frontend_misc.ma".
5include "common/FrontEndMem.ma".
6
7(* for store_value_of_type' *)
8include "Clight/Cexec.ma".
9
10
11(* --------------------------------------------------------------------------- *)
12(* Stuff on [valid_pointer m p].                                               *)
13(* --------------------------------------------------------------------------- *)
14
15(* [do_if_in_bounds] is used to check consistency when reading and storing stuff. *)
16definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.
17
18lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p.
19#m #p @conj
20[ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);
21     whd in match (do_if_in_bounds); normalize nodelta
22     cases (Zltb (block_id (pblock p)) (nextblock m))
23     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
24     >andb_lsimpl_true normalize nodelta
25     cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
26     [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]
27     >andb_lsimpl_true normalize nodelta
28     #Hlt >Hlt normalize nodelta #A #f /2 by ex_intro/
29| 2: whd in match (valid_pointer ??);
30     whd in match (in_bounds_pointer ??); #H
31     lapply (H bool (λblock,contents,off. true))
32     * #foo whd in match (do_if_in_bounds ????);
33     cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
34     [ 2: #Habsurd destruct (Habsurd) ]
35     >andb_lsimpl_true
36     cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
37     normalize nodelta
38     [ 2: #Habsurd destruct (Habsurd) ]
39     >andb_lsimpl_true
40     elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))     
41     [ 1: #H >H //
42     | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
43] qed.
44
45lemma valid_pointer_to_Prop :
46  ∀m,p. valid_pointer m p = true →
47        (block_id (pblock p)) < (nextblock m) ∧
48        (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧
49        (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)).
50#m #p whd in match (valid_pointer ??);       
51#H
52lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
53lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m))
54cases (Zltb (block_id (pblock p)) (nextblock m)) in H;
55[ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
56cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
57normalize nodelta
58[ 2: #Habsurd destruct ]
59#Hlt1 #Hlt2 #Hle @conj try @conj
60try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1)
61qed.
62
63lemma valid_pointer_of_Prop :
64  ∀m,p. (block_id (pblock p)) < (nextblock m) ∧
65        (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧
66        (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)) →
67        valid_pointer m p = true.
68#m #p * * #Hnextblock #Hlowbound #Hhighbound whd in match (valid_pointer ??);
69>(Zle_to_Zleb_true … Hlowbound)
70>(Zlt_to_Zltb_true … Hhighbound)
71>(Zlt_to_Zltb_true … Hnextblock) @refl
72qed.
73
74(* --------------------------------------------------------------------------- *)
75(* "Observational" memory equivalence. Memories use closures to represent contents,
76   so we have to use that short of asserting functional extensionality to reason
77   on reordering of operations on memories, among others. For our
78   limited purposes, we do not need (at this time of writing, i.e. 22 sept. 2012)
79   to push the observation in the content_map. *)
80(* --------------------------------------------------------------------------- *) 
81definition memory_eq ≝ λm1,m2.
82  nextblock m1 = nextblock m2 ∧
83  ∀b. blocks m1 b = blocks m2 b.
84 
85(* memory_eq is an equivalence relation. *)
86lemma reflexive_memory_eq : reflexive ? memory_eq.
87whd * #contents #nextblock #Hpos normalize @conj try //
88qed.
89
90lemma symmetric_memory_eq : symmetric ? memory_eq.
91whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos'
92normalize * #H1 #H2 @conj >H1 try //
93qed.
94
95lemma transitive_memory_eq : transitive ? memory_eq.
96whd
97* #contents #nextblock #Hpos
98* #contents1 #nextblock1 #Hpos1
99* #contents2 #nextblock2 #Hpos2
100normalize * #H1 #H2 * #H3 #H4 @conj //
101qed.
102
103(* --------------------------------------------------------------------------- *)
104(* Some definitions and results useful for simulation proofs. *)
105(* --------------------------------------------------------------------------- *)
106
107(* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end values are equal. *)
108definition load_sim ≝
109λ(m1 : mem).λ(m2 : mem).
110 ∀ptr,bev.
111  beloadv m1 ptr = Some ? bev →
112  beloadv m2 ptr = Some ? bev.
113   
114(* --------------------------------------------------------------------------- *)
115(* Lift beloadv simulation to the front-end. *)       
116
117(* Lift load_sim to loadn. *)
118lemma load_sim_loadn :
119 ∀m1,m2. load_sim m1 m2 →
120 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.
121#m1 #m2 #Hload_sim #sz
122elim sz
123[ 1: #p #res #H @H
124| 2: #n' #Hind #p #res
125     whd in match (loadn ???);
126     whd in match (loadn m2 ??);
127     lapply (Hload_sim p)
128     cases (beloadv m1 p) normalize nodelta
129     [ 1: #_ #Habsurd destruct (Habsurd) ]
130     #bval #H >(H ? (refl ??)) normalize nodelta
131     lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))
132     cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')
133     normalize nodelta
134     [ 1: #_ #Habsurd destruct (Habsurd) ]
135     #res' #H >(H ? (refl ??)) normalize
136     #H @H
137] qed.
138 
139(* Lift load_sim to front-end values. *)
140lemma load_sim_fe :
141  ∀m1,m2. load_sim m1 m2 →
142  ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →
143            load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.
144#m1 #m2 #Hloadsim #ptr #ty #v
145cases ty
146[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
147| 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
148whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
149[ 1,7,8: #Habsurd destruct (Habsurd)
150| 5,6: #H @H
151| 2,3,4,9:
152  generalize in match (mk_pointer (pblock ptr) (poff ptr));
153  elim (typesize ?)
154  [ 1,3,5,7: #p #H @H
155  | 2,4,6,8: #n' #Hind #p
156      lapply (load_sim_loadn … Hloadsim (S n') p)
157      cases (loadn m1 p (S n')) normalize nodelta
158      [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]     
159      #bv #H >(H ? (refl ??)) #H @H
160  ]
161] qed.
162 
163(* --------------------------------------------------------------------------- *)
164(* Lemmas relating reading and writing operation to memory properties. *)
165
166(* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)
167lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true.
168* #contents #next #nextpos #ptr #res
169whd in match (beloadv ??);
170whd in match (valid_pointer ??);
171cases (Zltb (block_id (pblock ptr)) next)
172normalize nodelta
173[ 2: #Habsurd destruct (Habsurd) ]
174>andb_lsimpl_true
175whd in match (low_bound ??);
176whd in match (high_bound ??);
177cases (Zleb (low (contents (pblock ptr)))
178        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
179[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
180>andb_lsimpl_true
181normalize nodelta #H
182cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
183try // normalize #Habsurd destruct (Habsurd)
184qed.
185
186lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true.
187* #contents #next #nextpos #ptr #v #res
188whd in match (bestorev ???);
189whd in match (valid_pointer ??);
190cases (Zltb (block_id (pblock ptr)) next)
191normalize nodelta
192[ 2: #Habsurd destruct (Habsurd) ]
193>andb_lsimpl_true
194whd in match (low_bound ??);
195whd in match (high_bound ??);
196cases (Zleb (low (contents (pblock ptr)))
197        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
198[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
199>andb_lsimpl_true
200cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))
201normalize nodelta try // #Habsurd destruct (Habsurd)
202qed.
203
204(* valid pointer implies successful bestorev *)
205lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'.
206#m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) *
207#Hnext #Hlow #Hhigh normalize
208>(Zlt_to_Zltb_true … Hnext) normalize nodelta
209>(Zle_to_Zleb_true … Hlow) normalize nodelta
210>(Zlt_to_Zltb_true … Hhigh) normalize nodelta
211/2 by ex_intro/
212qed.
213
214(* --------------------------------------------------------------------------- *)
215(* Some facts on [free] *)
216
217lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
218* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
219@(eqZb_elim … bid1 bid2)
220[ 1: #Heq >Heq cases br1 cases br2 normalize
221     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
222     #_ @refl
223| 2: cases br1 cases br2 normalize #_ #_ @refl ]
224qed.
225
226lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
227* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
228@(eqZb_elim … bid1 bid2)
229[ 1: #Heq >Heq cases br1 cases br2 normalize
230     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
231     #_ @refl
232| 2: cases br1 cases br2 normalize #_ #_ @refl ]
233qed.
234
235lemma beloadv_free_blocks_neq :
236  ∀m,block,pblock,poff,res.
237  beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
238* #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
239normalize
240cases (Zltb pbid next) normalize nodelta
241[ 2: #Habsurd destruct (Habsurd) ]
242cases pbr cases br normalize nodelta
243[ 2,3: #_ % #Habsurd destruct (Habsurd) ]
244@(eqZb_elim pbid bid) normalize nodelta
245#Heq destruct (Heq)
246[ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
247#_ % #H destruct (H) elim Heq #H @H @refl
248qed.
249
250lemma beloadv_free_beloadv :
251  ∀m,block,ptr,res.
252    beloadv (free m block) ptr = Some ? res →
253    beloadv m ptr = Some ? res.
254* #contents #next #nextpos #block * #pblock #poff #res
255#H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq
256lapply H
257whd in match (beloadv ??);
258whd in match (beloadv ??) in ⊢ (? → %);
259whd in match (nextblock (free ??));
260cases (Zltb (block_id pblock) next)
261[ 2: normalize #Habsurd destruct (Habsurd) ]
262normalize nodelta
263<(low_free_eq … Hblocks_neq)
264<(high_free_eq … Hblocks_neq)
265whd in match (free ??);
266whd in match (update_block ?????);
267@(eq_block_elim … pblock block)
268[ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ]
269#_ normalize nodelta
270#H @H
271qed.
272
273lemma beloadv_free_beloadv2 :
274  ∀m,block,ptr,res.
275  pblock ptr ≠ block →
276  beloadv m ptr = Some ? res →
277  beloadv (free m block) ptr = Some ? res.
278* #contents #next #nextpos #block * #pblock #poff #res #Hneq
279whd in match (beloadv ??);
280whd in match (beloadv ??) in ⊢ (? → %);
281whd in match (nextblock (free ??));
282cases (Zltb (block_id pblock) next)
283[ 2: normalize #Habsurd destruct (Habsurd) ]
284normalize nodelta
285<(low_free_eq … Hneq)
286<(high_free_eq … Hneq)
287whd in match (free ??);
288whd in match (update_block ?????);
289@(eq_block_elim … pblock block)
290[ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ]
291#_ normalize nodelta
292#H @H
293qed.
294
295(* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *)
296lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
297#m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
298#H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
299elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
300[ 1: #Hlt >Hlt normalize nodelta
301     @(eq_block_elim … b (pblock p))
302     [ 1: #Heq >Heq whd in match (free ??);
303          whd in match (update_block ?????); >eq_block_b_b
304          normalize nodelta normalize in match (low ?);
305          >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta
306          #Habsurd destruct (Habsurd)
307     | 2: #Hblock_neq whd in match (free ? ?);
308          whd in match (update_block ?????);
309          >(not_eq_block_rev … Hblock_neq) normalize nodelta
310          cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
311          [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
312          >andb_lsimpl_true
313          lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p)))
314                                     (high (blocks m (pblock p))))
315          cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
316          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
317          normalize nodelta #H #_ /2 by ex_intro/
318     ]
319| 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ]
320qed.
321
322(* Cf [in_bounds_free_to_in_bounds] *)
323lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
324#m #b #p #Hvalid
325cases (valid_pointer_def … m p) #HA #HB
326cases (valid_pointer_def … (free m b) p) #HC #HD
327@HB @(in_bounds_free_to_in_bounds … b)
328@HC @Hvalid
329qed.
330
331(* Making explicit the argument above. *)
332lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
333#m #b #p
334whd in match (valid_pointer ??);
335whd in match (free ??);
336whd in match (update_block ????);
337whd in match (low_bound ??);
338whd in match (high_bound ??);
339@(eq_block_elim … b (pblock p))
340[ 1: #Heq <Heq >eq_block_b_b normalize nodelta
341     whd in match (low ?); whd in match (high ?);
342     cases (Zltb ? (nextblock m))
343     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
344     >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd)
345| 2: #Hneq #_ @Hneq ]
346qed.
347
348(* --------------------------------------------------------------------------- *)
349(* loading and storing are inverse operations for integers. (Paolo's work
350 * contain a proof of this fact for pointers)                                  *)
351(* --------------------------------------------------------------------------- *)
352
353lemma fold_left_neq_acc_neq :
354  ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m.
355    acc1 ≠ acc2 →
356    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠
357    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2.
358#m elim m
359[ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
360| 2: #m' #Hind #acc1 #acc2 #y1 #y2
361     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
362     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
363     >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?);
364     cases hd1 cases hd2 normalize nodelta #H
365     [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?)
366          [ 1: % #H' @Hneq destruct (H') @refl ]
367          * #H' @H' @H
368     | 4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?)
369          [ 1: % #H' @Hneq destruct (H') @refl ]
370          * #H' @H' @H
371     | 2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?)
372          [ 1: % #H' destruct ]
373          * #H' @H' try @H
374     | 3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?)
375          [ 1: % #H' destruct ]
376          * #H' @H' try @H ]
377] qed.
378
379lemma fold_left_aux :
380  ∀m. ∀acc. ∀y1,y2:BitVector m.
381    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 =
382    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 →
383    y1 = y2.
384#m elim m
385[ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
386| 2: #m' #Hind #acc #y1 #y2
387     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
388     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
389     >Heq1 >Heq2 whd in ⊢ ((??%%) → ?);
390     cases hd1 cases hd2 normalize nodelta
391     [ 1,4: #H >(Hind … H) @refl
392     | 2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?)
393          [ 1: % #H' destruct ]
394          * #H @(False_ind … (H Habsurd))
395     | 3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?)
396          [ 1: % #H' destruct ]
397          * #H @(False_ind … (H Habsurd)) ]
398] qed.
399
400
401lemma bv_neq_Z_neq_aux :
402  ∀n. ∀bv1,bv2 : BitVector n. ∀f.
403    Z_of_unsigned_bitvector n bv1 ≠
404    pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2).
405#n elim n
406[ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct
407| 2: #n' #Hind #bv1 #bv2 #f
408     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
409     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
410     >Heq1 >Heq2 %
411     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
412     cases hd1 cases hd2 normalize nodelta
413     normalize in ⊢ ((??%%) → ?);
414     [ 1: #Hpos destruct (Hpos)
415          lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?)
416          [ 1: % #H destruct ]
417          * #H @H @e0
418     | 2: #Hpos destruct (Hpos)
419          lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?)
420          [ 1: % #H destruct ]
421          * #H @H @e0
422     | 3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H
423     | 4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H
424     ]
425] qed.
426
427(* Some aux. lemmas (and axioms ...) first *)
428lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n.
429  bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2.
430#n #bv1 #bv2 * #Hneq % #Hneq' @Hneq -Hneq lapply Hneq' -Hneq'
431lapply bv2 lapply bv1 -bv1 -bv2
432elim n
433[ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) //
434| 2: #n' #Hind #bv1 #bv2
435     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
436     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
437     >Heq1 >Heq2
438     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
439     cases hd1 cases hd2 normalize nodelta
440     [ 1: #Heq destruct (Heq) lapply (fold_left_aux … e0) * @refl
441     | 4: #H >(Hind ?? H) @refl
442     | 2: #H lapply (sym_eq ??? H) -H #H
443          cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H))
444     | 3: #H
445          cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ]
446] qed.
447
448definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs).
449
450
451(* We prove the following properties for bestorev :
452  1) storing doesn't modify the nextblock
453  2) it does not modify the extents of the block written to
454  3) since we succeeded in storing, the offset is in the bounds
455  4) reading where we wrote yields the obvious result
456  5) besides the written offset, the memory contains the same stuff
457*)
458lemma mem_bounds_invariant_after_bestorev :
459∀m,m',b,ofs,bev.
460  bestorev m (mk_pointer b ofs) bev = Some ? m' →
461  nextblock m' = nextblock m ∧
462  (∀b.low (blocks m' b) = low (blocks m b) ∧
463      high (blocks m' b) = high (blocks m b)) ∧
464  (low (blocks m b) ≤ (Z_of_offset ofs) ∧
465   (Z_of_offset ofs) < high (blocks m b)) ∧   
466  (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧
467  (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) =
468                 contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))).
469#m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?);
470#H
471cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H
472cases (if_opt_inversion ???? H) #Hlelt -H #H
473cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj
474destruct try @refl
475[ 1:
476  #b' normalize cases b #br #bid cases b' #br' #bid'
477  cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize
478  try /2 by conj, refl/
479| 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H
480| 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H
481| 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize
482     >eqZb_z_z @refl
483| 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta
484     >eqZb_z_z normalize nodelta
485     @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs)))
486     [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2
487            #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?)
488            [ 1,3: % #Heq destruct cases Hneq #H @H @refl ]
489            * #H #Habsurd @(False_ind … (H Habsurd))
490     | 2,4: normalize nodelta #H @refl ]
491] qed.
492
493(* Shifts an offset [i] times. storen uses a similar operation internally. *)
494let rec shiftn (off:offset) (i:nat) on i : offset ≝
495match i with
496[ O ⇒ off
497| S n ⇒
498  shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n
499].
500
501(* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a
502   serious PITA to prove. *)
503axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs.
504
505(* /!\ TODO the following proof is extremely ugly and indirect. I expect it to be
506 *      hugely improvable.
507 * /!\ *)
508
509(* We prove some properties of [storen m ptr data]. Note that [data] is a list of back-end chunks.
510   What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to
511   have is that the contents of this particular zone (ptr to ptr+|data|-1) match exactly [data], and
512   that elsewhere the memory is untouched.
513   Not so simple. Some observations:
514   A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16).
515      On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems
516      when writing at the edge of the range of offsets and wrapping around, but that can be solved
517      resorting to ugliness and trickery.
518   B) The [data] list is unbounded. Taking into account the point A), this means that we can lose
519      data when writing (exactly as when we write in a circular buffer, overwriting previous stuff).
520      The only solution to that is to explicitly bound |data| with something reasonable.
521   Taking these observations into account, we prove the following invariants:
522  1) storing doesn't modify the nextblock (trivial)
523  2) it does not modify the extents of the block written to (trivial)
524  3) all the offsets on which we run while writing are legal (trivial)
525  3) if we index properly, we hit the stored data in the same order as in the list
526  4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere",
527     because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as
528     "not reachable by shiftn from [ofs] to |data|"
529  5) the pointer we write to is valid (trivial)
530*)
531lemma mem_bounds_invariant_after_storen :
532  ∀data,m,m',b,ofs.
533    |data| ≤ 8 → (* 8 is the size of a double. *)
534    storen m (mk_pointer b ofs) data = Some ? m' →
535    (nextblock m' = nextblock m ∧
536    (∀b.low (blocks m' b) = low (blocks m b) ∧
537        high (blocks m' b) = high (blocks m b)) ∧
538    (∀index. index < |data| → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧
539                               Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧
540    (∀index. index < |data| → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧
541    (∀o. (∀i. i < |data| → o ≠ shiftn ofs i) →
542         contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧
543    (|data| > 0 → valid_pointer m (mk_pointer b ofs) = true)).
544#l elim l
545[ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl
546     [ 1: #b0 @conj try @refl
547(*     | 2: #Habsurd @False_ind /2 by le_S_O_absurd/*)
548     | 2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/
549     | 4: #o #Hout @refl
550     | 5: #H @False_ind /2 by le_S_O_absurd/ ]
551| 2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren
552     whd in Hstoren:(??%?);
553     cases (some_inversion ????? Hstoren) #m'' * #Hbestorev -Hstoren #Hstoren
554     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK
555     lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * *
556     #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj
557     [ 1: <HA <HC @refl
558     | 2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try //     
559     | 4: *
560          [ 1: #_ <HJ whd in match (nth 0 ???);
561               lapply (HV ofs ?)
562               [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs)
563                    [ 1: normalize in Hsize_bound;
564                         cut (|tl| < 8) [ /2 by lt_plus_to_minus_r/ ]
565                         #Hlt' lapply (transitive_lt … Hlt Hlt') // ]
566                    * #H @H whd in match (shiftn ??); @Heq
567               | 2: cases ofs #ofs' normalize // ]
568          | 2: #i' #Hlt lapply (HF i' ?)
569               [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) //
570               | 2: #H whd in match (nth_opt ???); >H @refl ] ]
571     | 5: #o #H >HV
572          [ 2: #i #Hlt @(H (S i) ?)
573               normalize normalize in Hlt; /2 by le_S_S/
574          | 1: @HK @(H 0) // ]     
575     | 6: #_ @(bestorev_to_valid_pointer … Hbestorev)
576     | 3: *
577          [ 1: #_ <HJ whd in match (shiftn ??);
578               lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
579               lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
580               whd in match (low_bound ??); whd in match (high_bound ??);
581               cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
582               cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
583               [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb
584               lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) -Hleb #Hleb'
585               normalize @conj try assumption
586          | 2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2
587               lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ]
588               >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2
589          ]
590     ]
591] qed.
592
593lemma storen_beloadv_ok :
594  ∀m,m',b,ofs,hd,tl.
595  |hd::tl| ≤ 8 → (* 8 is the size of a double. *)
596  storen m (mk_pointer b ofs) (hd::tl) = Some ? m' →
597  ∀i. i < |hd::tl| → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl).
598#m #m' #b #ofs #hd #tl #Hle #Hstoren
599lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
600#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
601#i #Hle lapply (Hdata i Hle) #Helt >Helt
602whd in match (beloadv ??); whd in match (nth_opt ???);
603lapply (Hvalid_ptr ?) try //
604whd in ⊢ ((??%?) → ?);
605>Hnext cases (Zltb (block_id b) (nextblock m))
606[ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ]
607>andb_lsimpl_true normalize nodelta
608whd in match (low_bound ??); whd in match (high_bound ??);
609cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H
610lapply (Hvalid_offs i Hle) * #Hzle #Hzlt
611>(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl
612qed.
613
614lemma loadn_beloadv_ok :
615  ∀size,m,b,ofs,result.
616  loadn m (mk_pointer b ofs) size = Some ? result →
617  ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result.
618#size elim size
619[ 1: #m #b #ofs #result #Hloadn *
620     [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
621     | 2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ]
622| 2: #size' #Hind_size #m #b #ofs #result #Hloadn #i
623     elim i
624     [ 1: #_
625          cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
626          cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq
627          destruct (Heq) whd in match (shiftn ofs 0);
628          >Hbeloadv @refl
629    | 2: #i' #Hind #Hlt
630         whd in match (shiftn ofs (S i'));
631         lapply (Hind ?)
632         [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind
633         whd in Hloadn:(??%?);
634         cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
635         cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq -Hloadn'
636         destruct (Heq)
637         @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ]
638         @Hloadn_tl
639    ]
640] qed.
641
642lemma storen_loadn_nonempty :
643  ∀data,m,m',b,ofs.
644  |data| ≤ 8 →
645  storen m (mk_pointer b ofs) data = Some ? m' →
646  ∃result. loadn m' (mk_pointer b ofs) (|data|) = Some ? result ∧ |result|=|data|.
647#data elim data
648[ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ]
649#hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren
650lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
651#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
652cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0
653whd in match (loadn ???);
654lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
655whd in match (beloadv ??);
656whd in match (low_bound ??); whd in match (high_bound ??);
657>Hnext
658cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
659normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh
660cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta
661[ 2: #Habsurd destruct ] >andb_lsimpl_true
662#Hltb >Hltb normalize nodelta
663cases (Hind  … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ]
664#tl' * #Hloadn >Hloadn #Htl' normalize nodelta
665%{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl
666normalize >Htl' @refl
667qed.
668
669(* for leb_elim, shadowed in positive.ma *)
670definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop.
671(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim.
672
673(*include alias "arithmetics/nat.ma".*)
674
675lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. |l| ≤ i → nth_opt A i l = None ?.
676#A #l elim l //
677#hd #tl #H #i elim i
678[ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/
679| 2: #i' #H' #Hle whd in match (nth_opt ???); @H lapply (monotonic_pred … Hle) //
680] qed.
681
682lemma storen_loadn_ok :
683  ∀data.
684  |data| ≤ 8 → (* 8 is the size of a double. *)
685  ∀m,m',b,ofs.
686  storen m (mk_pointer b ofs) data = Some ? m' →
687  loadn m' (mk_pointer b ofs) (|data|) = Some ? data.
688#data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren
689lapply (storen_beloadv_ok m m' …  Hle Hstoren) #Hyp_storen
690cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz
691lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn
692cut (∀i. i < |hd::tl| → nth_opt ? i (hd::tl) = nth_opt ? i result)
693[ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1
694  lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ]
695#Hyp
696cut (result = hd :: tl)
697[ 2: #Heq destruct (Heq) @Hloadn ]
698@nth_eq_to_eq #i @sym_eq
699@(leb_elim' … (S i) (|hd::tl|))
700[ 1: #Hle @(Hyp ? Hle)
701| 2: #Hnle cut (|hd::tl| ≤ i)
702     [ lapply (not_le_to_lt … Hnle) normalize
703       @monotonic_pred ]
704     #Hle'
705     >nth_miss // >nth_miss //
706] qed.
707
708(* In order to prove the lemma on store_value_of_type and load_value_of_type,
709   we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *)
710lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
711* try //
712[ 1: * try //
713| 2: * try //
714] qed.
715
716(* Lifting bound on make_list *)
717lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → |make_list A elt sz| ≤ bound.
718#A #sz elim sz try //
719#sz' #Hind #bound #elt #Hbound normalize
720cases bound in Hbound;
721[ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
722| 2: #bound' #Hbound' lapply (Hind bound' elt ?)
723     [ 1: @(monotonic_pred … Hbound')
724     | 2: /2 by le_S_S/ ]
725] qed.
726
727lemma bytes_of_bitvector_bounded :
728  ∀sz,bv. |bytes_of_bitvector (size_intsize sz) bv| = size_intsize sz.
729* #bv normalize
730[ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 //
731| 2: cases (vsplit ????) normalize nodelta #bv0 #bv1
732     cases (vsplit ????) normalize nodelta #bv2 #bv3 //
733| 3: cases (vsplit ????) normalize nodelta #bv0 #bv1
734     cases (vsplit ????) normalize nodelta #bv2 #bv3
735     cases (vsplit ????) normalize nodelta #bv4 #bv5
736     cases (vsplit ????) normalize nodelta #bv6 #bv7
737     //
738] qed.
739
740lemma map_bounded :
741  ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|.
742  #A #B #l elim l try //
743qed.
744
745lemma fe_to_be_values_bounded :
746  ∀ty,v. |fe_to_be_values ty v| ≤ 8.
747#ty cases ty
748[ 3: #fsz #v whd in match (fe_to_be_values ??);
749     cases v normalize nodelta
750     [ 1: @makelist_bounded @typesize_bounded
751     | 2: * normalize nodelta #bv
752          >map_bounded >bytes_of_bitvector_bounded //
753     | 3: #fl @makelist_bounded @typesize_bounded
754     | 4: //
755     | 5: #ptr // ]
756| 2: #v whd in match (fe_to_be_values ??);
757     cases v normalize nodelta
758     [ 1: @makelist_bounded @typesize_bounded
759     | 2: * normalize nodelta #bv
760          >map_bounded >bytes_of_bitvector_bounded //
761     | 3: #fl @makelist_bounded @typesize_bounded
762     | 4: //
763     | 5: #ptr // ]
764| 1: #sz #sg #v whd in match (fe_to_be_values ??);
765     cases v normalize nodelta
766     [ 1: @makelist_bounded @typesize_bounded
767     | 2: * normalize nodelta #bv
768          >map_bounded >bytes_of_bitvector_bounded //
769     | 3: #fl @makelist_bounded @typesize_bounded
770     | 4: //
771     | 5: #ptr // ]
772] qed.
773
774
775lemma mem_bounds_after_store_value_of_type :
776  ∀m,m',ty,b,o,v.
777  store_value_of_type ty m b o v = Some ? m' →
778  (nextblock m' = nextblock m ∧
779   (∀b.low (blocks m' b) = low (blocks m b) ∧
780       high (blocks m' b) = high (blocks m b))).
781#m #m' #ty #b #o #v
782lapply (fe_to_be_values_bounded (typ_of_type ty) v)
783cases ty
784[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
785| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
786whd in match (typ_of_type ?); #Hbounded
787whd in match (store_value_of_type ?????);
788[ 1,5,6,7,8: #Habsurd destruct (Habsurd)
789| *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren)
790     * * * * * #Hnextblock #Hbounds_eq #Hnonempty
791     #Hcontents_upd #Hcontents_inv #Hvalid_ptr
792     >Hnextblock @conj //
793] qed.
794
795lemma mem_bounds_after_store_value_of_type' :
796  ∀m,m',ty,p,v.
797  store_value_of_type' ty m p v = Some ? m' →
798  (nextblock m' = nextblock m ∧
799   (∀b.low (blocks m' b) = low (blocks m b) ∧
800       high (blocks m' b) = high (blocks m b))).
801#m #m' #ty * #b #o #v whd in match (store_value_of_type' ????);
802@mem_bounds_after_store_value_of_type
803qed.
804
805
806definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v.
807  match ty with
808  [ ASTint sz sg ⇒
809    match v with
810    [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *)
811    | _ ⇒ False ]
812  | ASTptr ⇒
813    match v with
814    [ Vptr p ⇒ True
815    | _ ⇒ False ]
816  | ASTfloat fsz ⇒
817    match v with
818    [ Vfloat _ ⇒ True
819    | _ ⇒ False ]   
820  ].
821
822
823definition type_consistent_with_value : type → val → Prop ≝ λty,v.
824match access_mode ty with
825[ By_value chunk ⇒ ast_typ_consistent_with_value chunk v
826| _ ⇒ True
827].
828
829(* We also need the following property. It is not provable unless [v] and [ty] are consistent. *)
830lemma fe_to_be_values_size :
831  ∀ty,v. ast_typ_consistent_with_value ty v →
832         typesize ty = |fe_to_be_values ty v|.
833*
834[ 1: #sz #sg #v
835     whd in match (fe_to_be_values ??); cases v
836     normalize in ⊢ (% → ?);
837     [ 1,4: @False_ind
838     | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta
839          >map_bounded >bytes_of_bitvector_bounded cases sz' //
840     | 3: #f normalize in ⊢ (% → ?); @False_ind
841     | 5: #p normalize in ⊢ (% → ?); @False_ind ]
842| 2: #v cases v
843     normalize in ⊢ (% → ?);
844     [ 1,4: @False_ind
845     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
846     | 3: #f normalize in ⊢ (% → ?); @False_ind
847     | 5: #p #_ // ]
848| 3: #fsz #v cases v
849     normalize in ⊢ (% → ?);
850     [ 1: @False_ind
851     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
852     | 3: #f #_ cases fsz //
853     | 4: @False_ind
854     | 5: #p normalize in ⊢ (% → ?); @False_ind ]
855] qed.
856
857
858(* Not verified for floats atm. Restricting to integers. *)
859lemma fe_to_be_to_fe_value : ∀sz,sg,v.
860  ast_typ_consistent_with_value (ASTint sz sg) v →
861  (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v).
862#sz #sg #v
863whd in match (fe_to_be_values ??);
864cases v normalize in ⊢ (% → ?);
865[ 1,4: @False_ind
866| 3: #f @False_ind
867| 5: #p @False_ind
868| 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta
869     cases sz' in i'; #i normalize nodelta
870     normalize in i;
871     whd in match (be_to_fe_value ??);
872     normalize in match (size_intsize ?);
873     whd in match (bytes_of_bitvector ??);
874     [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i
875          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
876          whd in match (build_integer_val ??);
877          >(BitVector_O … ri) //
878     | 2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i
879          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
880          whd in match (build_integer_val ??);
881          normalize in match (size_intsize ?);
882          whd in match (bytes_of_bitvector ??);
883          lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri
884          <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri
885          whd in match (build_integer_val ??);
886          >(BitVector_O … rri) //
887     | 3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i
888          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
889          whd in match (build_integer_val ??);
890          normalize in match (size_intsize ?);
891          whd in match (bytes_of_bitvector ??);
892          lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB
893          <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB
894          whd in match (bytes_of_bitvector ??);
895          lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD
896          <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD
897          whd in match (bytes_of_bitvector ??);
898          lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF
899          <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF
900          >(BitVector_O … iH) @refl ]
901] qed.                   
902
903(* It turns out that the following property is not true in general. Floats are converted to
904   BVundef, which are converted back to Vundef. But we care only about ints.  *)
905lemma storev_loadv_ok :
906  ∀sz,sg,m,b,ofs,v,m'.
907    ast_typ_consistent_with_value (ASTint sz sg) v →
908    store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' →
909    load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v.
910#sz #sg #m #b #ofs #v #m' #H
911whd in ⊢ ((??%?) → (??%?)); #Hstoren
912lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren)
913>(fe_to_be_values_size … H) #H >H normalize nodelta
914>fe_to_be_to_fe_value try //
915qed.
916
917(* For the arguments exposed before, we restrict the lemma to ints.
918 *)
919lemma store_value_load_value_ok :
920  ∀sz,sg,m,b,ofs,v,m'.
921    type_consistent_with_value (Tint sz sg) v →
922    store_value_of_type (Tint sz sg) m b ofs v = Some ? m' →
923    load_value_of_type (Tint sz sg) m' b ofs = Some ? v.
924#sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?);
925cases v in H; normalize nodelta
926[ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #vf #_ @False_ind | 4: #_ @False_ind | 5: #vp #_ @False_ind ]
927#Heq >Heq in H; #H
928(* The lack of control on unfolds is extremely annoying. *)
929whd in match (store_value_of_type ?????); #Hstoren
930lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren)
931whd in match (load_value_of_type ????);
932>(fe_to_be_values_size … H) #H' >H' normalize nodelta
933>fe_to_be_to_fe_value try //
934qed.
935 
936
Note: See TracBrowser for help on using the repository browser.