source: src/Clight/MemProperties.ma @ 2562

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

Memory injections for Clight to Cminor, partially axiomatized.

File size: 47.8 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.
108 * This is allright for switch removal but false for Clight to Cminor *)
109definition load_sim ≝
110λ(m1 : mem).λ(m2 : mem).
111 ∀ptr,bev.
112  beloadv m1 ptr = Some ? bev →
113  beloadv m2 ptr = Some ? bev.
114   
115(* --------------------------------------------------------------------------- *)
116(* Lift beloadv simulation to the front-end. *)       
117
118(* Lift load_sim to loadn. *)
119lemma load_sim_loadn :
120 ∀m1,m2. load_sim m1 m2 →
121 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.
122#m1 #m2 #Hload_sim #sz
123elim sz
124[ 1: #p #res #H @H
125| 2: #n' #Hind #p #res
126     whd in match (loadn ???);
127     whd in match (loadn m2 ??);
128     lapply (Hload_sim p)
129     cases (beloadv m1 p) normalize nodelta
130     [ 1: #_ #Habsurd destruct (Habsurd) ]
131     #bval #H >(H ? (refl ??)) normalize nodelta
132     lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))
133     cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')
134     normalize nodelta
135     [ 1: #_ #Habsurd destruct (Habsurd) ]
136     #res' #H >(H ? (refl ??)) normalize
137     #H @H
138] qed.
139 
140(* Lift load_sim to front-end values. *)
141lemma load_sim_fe :
142  ∀m1,m2. load_sim m1 m2 →
143  ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →
144            load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.
145#m1 #m2 #Hloadsim #ptr #ty #v
146cases ty
147[ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty
148| 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ]
149whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
150[ 1,6,7: #Habsurd destruct (Habsurd)
151| 4,5: #H @H
152| 2,3,8:
153  generalize in match (mk_pointer (pblock ptr) (poff ptr));
154  elim (typesize ?)
155  [ 1,3,5: #p #H @H
156  | *: #n' #Hind #p
157      lapply (load_sim_loadn … Hloadsim (S n') p)
158      cases (loadn m1 p (S n')) normalize nodelta
159      [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]     
160      #bv #H >(H ? (refl ??)) #H @H
161  ]
162] qed.
163 
164(* --------------------------------------------------------------------------- *)
165(* Lemmas relating reading and writing operation to memory properties. *)
166
167(* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)
168lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true.
169* #contents #next #nextpos #ptr #res
170whd in match (beloadv ??);
171whd in match (valid_pointer ??);
172cases (Zltb (block_id (pblock ptr)) next)
173normalize nodelta
174[ 2: #Habsurd destruct (Habsurd) ]
175>andb_lsimpl_true
176whd in match (low_bound ??);
177whd in match (high_bound ??);
178cases (Zleb (low (contents (pblock ptr)))
179        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
180[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
181>andb_lsimpl_true
182normalize nodelta #H
183cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
184try // normalize #Habsurd destruct (Habsurd)
185qed.
186
187lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true.
188* #contents #next #nextpos #ptr #v #res
189whd in match (bestorev ???);
190whd in match (valid_pointer ??);
191cases (Zltb (block_id (pblock ptr)) next)
192normalize nodelta
193[ 2: #Habsurd destruct (Habsurd) ]
194>andb_lsimpl_true
195whd in match (low_bound ??);
196whd in match (high_bound ??);
197cases (Zleb (low (contents (pblock ptr)))
198        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
199[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
200>andb_lsimpl_true
201cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))
202normalize nodelta try // #Habsurd destruct (Habsurd)
203qed.
204
205lemma bestorev_to_valid_pointer_after : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer res ptr = true.
206* #contents #next #nextpos #ptr #v #res
207whd in match (bestorev ???);
208whd in match (valid_pointer ??); #Hvalid
209cases (if_opt_inversion ???? Hvalid) #Hnextblock normalize nodelta -Hvalid #Hvalid
210cases (if_opt_inversion ???? Hvalid) #Hin_bounds #Heq destruct (Heq) normalize
211>Hnextblock normalize nodelta cases (block_region (pblock ptr)) normalize nodelta
212>eqZb_z_z normalize nodelta @Hin_bounds
213qed.
214
215(* valid pointer implies successful bestorev *)
216lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'.
217#m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) *
218#Hnext #Hlow #Hhigh normalize
219>(Zlt_to_Zltb_true … Hnext) normalize nodelta
220>(Zle_to_Zleb_true … Hlow) normalize nodelta
221>(Zlt_to_Zltb_true … Hhigh) normalize nodelta
222/2 by ex_intro/
223qed.
224
225(* --------------------------------------------------------------------------- *)
226(* Some facts on [free] *)
227
228lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
229* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
230@(eqZb_elim … bid1 bid2)
231[ 1: #Heq >Heq cases br1 cases br2 normalize
232     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
233     #_ @refl
234| 2: cases br1 cases br2 normalize #_ #_ @refl ]
235qed.
236
237lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
238* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
239@(eqZb_elim … bid1 bid2)
240[ 1: #Heq >Heq cases br1 cases br2 normalize
241     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
242     #_ @refl
243| 2: cases br1 cases br2 normalize #_ #_ @refl ]
244qed.
245
246lemma beloadv_free_blocks_neq :
247  ∀m,block,pblock,poff,res.
248  beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
249* #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
250normalize
251cases (Zltb pbid next) normalize nodelta
252[ 2: #Habsurd destruct (Habsurd) ]
253cases pbr cases br normalize nodelta
254[ 2,3: #_ % #Habsurd destruct (Habsurd) ]
255@(eqZb_elim pbid bid) normalize nodelta
256#Heq destruct (Heq)
257[ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
258#_ % #H destruct (H) elim Heq #H @H @refl
259qed.
260
261lemma beloadv_free_beloadv :
262  ∀m,block,ptr,res.
263    beloadv (free m block) ptr = Some ? res →
264    beloadv m ptr = Some ? res.
265* #contents #next #nextpos #block * #pblock #poff #res
266#H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq
267lapply H
268whd in match (beloadv ??);
269whd in match (beloadv ??) in ⊢ (? → %);
270whd in match (nextblock (free ??));
271cases (Zltb (block_id pblock) next)
272[ 2: normalize #Habsurd destruct (Habsurd) ]
273normalize nodelta
274<(low_free_eq … Hblocks_neq)
275<(high_free_eq … Hblocks_neq)
276whd in match (free ??);
277whd in match (update_block ?????);
278@(eq_block_elim … pblock block)
279[ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ]
280#_ normalize nodelta
281#H @H
282qed.
283
284lemma loadn_free_loadn :
285  ∀n,m,block,ptr,res.
286    loadn (free m block) ptr n = Some ? res →
287    loadn m ptr n = Some ? res.
288#n elim n
289[ 1: normalize //
290| 2: #n' #Hind #m #block #ptr #res #Hloadn
291     whd in Hloadn:(??%?);
292     cases (some_inversion ????? Hloadn) -Hloadn
293     #be * #Hbeloadv #Hloadn
294     cases (some_inversion ????? Hloadn) -Hloadn
295     #res' * #Hloadn #Heq destruct (Heq)
296     whd in match (loadn ???);
297     >(beloadv_free_beloadv … Hbeloadv) normalize nodelta
298     >(Hind … Hloadn) normalize nodelta @refl
299] qed.     
300
301lemma load_value_of_type_free_load_value_of_type :
302  ∀ty,m,block,b,o,res.
303    load_value_of_type ty (free m block) b o = Some ? res →
304    load_value_of_type ty m b o = Some ? res.
305#ty
306cases ty
307[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
308| #structname #fieldspec | #unionname #fieldspec | #id ]
309#m #block #b #o #res
310whd in ⊢ ((??%?) → (??%?)); // #H
311cases (some_inversion ????? H) #be * #Hloadn #Heq
312>(loadn_free_loadn … Hloadn)
313normalize nodelta assumption
314qed.
315
316lemma beloadv_free_beloadv2 :
317  ∀m,block,ptr,res.
318  pblock ptr ≠ block →
319  beloadv m ptr = Some ? res →
320  beloadv (free m block) ptr = Some ? res.
321* #contents #next #nextpos #block * #pblock #poff #res #Hneq
322whd in match (beloadv ??);
323whd in match (beloadv ??) in ⊢ (? → %);
324whd in match (nextblock (free ??));
325cases (Zltb (block_id pblock) next)
326[ 2: normalize #Habsurd destruct (Habsurd) ]
327normalize nodelta
328<(low_free_eq … Hneq)
329<(high_free_eq … Hneq)
330whd in match (free ??);
331whd in match (update_block ?????);
332@(eq_block_elim … pblock block)
333[ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ]
334#_ normalize nodelta
335#H @H
336qed.
337
338(* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *)
339lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
340#m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
341#H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
342elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
343[ 1: #Hlt >Hlt normalize nodelta
344     @(eq_block_elim … b (pblock p))
345     [ 1: #Heq >Heq whd in match (free ??);
346          whd in match (update_block ?????); >eq_block_b_b
347          normalize nodelta normalize in match (low ?);
348          >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta
349          #Habsurd destruct (Habsurd)
350     | 2: #Hblock_neq whd in match (free ? ?);
351          whd in match (update_block ?????);
352          >(not_eq_block_rev … Hblock_neq) normalize nodelta
353          cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
354          [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
355          >andb_lsimpl_true
356          lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p)))
357                                     (high (blocks m (pblock p))))
358          cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
359          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
360          normalize nodelta #H #_ /2 by ex_intro/
361     ]
362| 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ]
363qed.
364
365(* Cf [in_bounds_free_to_in_bounds] *)
366lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
367#m #b #p #Hvalid
368cases (valid_pointer_def … m p) #HA #HB
369cases (valid_pointer_def … (free m b) p) #HC #HD
370@HB @(in_bounds_free_to_in_bounds … b)
371@HC @Hvalid
372qed.
373
374(* Making explicit the argument above. *)
375lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
376#m #b #p
377whd in match (valid_pointer ??);
378whd in match (free ??);
379whd in match (update_block ????);
380whd in match (low_bound ??);
381whd in match (high_bound ??);
382@(eq_block_elim … b (pblock p))
383[ 1: #Heq <Heq >eq_block_b_b normalize nodelta
384     whd in match (low ?); whd in match (high ?);
385     cases (Zltb ? (nextblock m))
386     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
387     >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd)
388| 2: #Hneq #_ @Hneq ]
389qed.
390
391(* --------------------------------------------------------------------------- *)
392(* loading and storing are inverse operations for integers. (Paolo's work
393 * contain a proof of this fact for pointers)                                  *)
394(* --------------------------------------------------------------------------- *)
395
396lemma fold_left_neq_acc_neq :
397  ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m.
398    acc1 ≠ acc2 →
399    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠
400    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2.
401#m elim m
402[ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
403| 2: #m' #Hind #acc1 #acc2 #y1 #y2
404     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
405     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
406     >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?);
407     cases hd1 cases hd2 normalize nodelta #H
408     [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?)
409          [ 1: % #H' @Hneq destruct (H') @refl ]
410          * #H' @H' @H
411     | 4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?)
412          [ 1: % #H' @Hneq destruct (H') @refl ]
413          * #H' @H' @H
414     | 2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?)
415          [ 1: % #H' destruct ]
416          * #H' @H' try @H
417     | 3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?)
418          [ 1: % #H' destruct ]
419          * #H' @H' try @H ]
420] qed.
421
422lemma fold_left_aux :
423  ∀m. ∀acc. ∀y1,y2:BitVector m.
424    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 =
425    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 →
426    y1 = y2.
427#m elim m
428[ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
429| 2: #m' #Hind #acc #y1 #y2
430     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
431     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
432     >Heq1 >Heq2 whd in ⊢ ((??%%) → ?);
433     cases hd1 cases hd2 normalize nodelta
434     [ 1,4: #H >(Hind … H) @refl
435     | 2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?)
436          [ 1: % #H' destruct ]
437          * #H @(False_ind … (H Habsurd))
438     | 3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?)
439          [ 1: % #H' destruct ]
440          * #H @(False_ind … (H Habsurd)) ]
441] qed.
442
443
444lemma bv_neq_Z_neq_aux :
445  ∀n. ∀bv1,bv2 : BitVector n. ∀f.
446    Z_of_unsigned_bitvector n bv1 ≠
447    pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2).
448#n elim n
449[ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct
450| 2: #n' #Hind #bv1 #bv2 #f
451     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
452     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
453     >Heq1 >Heq2 %
454     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
455     cases hd1 cases hd2 normalize nodelta
456     normalize in ⊢ ((??%%) → ?);
457     [ 1: #Hpos destruct (Hpos)
458          lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?)
459          [ 1: % #H destruct ]
460          * #H @H @e0
461     | 2: #Hpos destruct (Hpos)
462          lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?)
463          [ 1: % #H destruct ]
464          * #H @H @e0
465     | 3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H
466     | 4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H
467     ]
468] qed.
469
470(* Some aux. lemmas (and axioms ...) first *)
471lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n.
472  bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2.
473#n #bv1 #bv2 * #Hneq % #Hneq' @Hneq -Hneq lapply Hneq' -Hneq'
474lapply bv2 lapply bv1 -bv1 -bv2
475elim n
476[ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) //
477| 2: #n' #Hind #bv1 #bv2
478     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
479     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
480     >Heq1 >Heq2
481     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
482     cases hd1 cases hd2 normalize nodelta
483     [ 1: #Heq destruct (Heq) lapply (fold_left_aux … e0) * @refl
484     | 4: #H >(Hind ?? H) @refl
485     | 2: #H lapply (sym_eq ??? H) -H #H
486          cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H))
487     | 3: #H
488          cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ]
489] qed.
490
491definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs).
492
493
494(* We prove the following properties for bestorev :
495  1) storing doesn't modify the nextblock
496  2) it does not modify the extents of the block written to
497  3) since we succeeded in storing, the offset is in the bounds
498  4) reading where we wrote yields the obvious result
499  5) besides the written offset, the memory contains the same stuff
500*)
501lemma mem_bounds_invariant_after_bestorev :
502∀m,m',b,ofs,bev.
503  bestorev m (mk_pointer b ofs) bev = Some ? m' →
504  nextblock m' = nextblock m ∧
505  (∀b.low (blocks m' b) = low (blocks m b) ∧
506      high (blocks m' b) = high (blocks m b)) ∧
507  (low (blocks m b) ≤ (Z_of_offset ofs) ∧
508   (Z_of_offset ofs) < high (blocks m b)) ∧   
509  (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧
510  (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) =
511                 contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))).
512#m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?);
513#H
514cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H
515cases (if_opt_inversion ???? H) #Hlelt -H #H
516cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj
517destruct try @refl
518[ 1:
519  #b' normalize cases b #br #bid cases b' #br' #bid'
520  cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize
521  try /2 by conj, refl/
522| 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H
523| 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H
524| 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize
525     >eqZb_z_z @refl
526| 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta
527     >eqZb_z_z normalize nodelta
528     @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs)))
529     [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2
530            #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?)
531            [ 1,3: % #Heq destruct cases Hneq #H @H @refl ]
532            * #H #Habsurd @(False_ind … (H Habsurd))
533     | 2,4: normalize nodelta #H @refl ]
534] qed.
535
536(* Shifts an offset [i] times. storen uses a similar operation internally. *)
537let rec shiftn (off:offset) (i:nat) on i : offset ≝
538match i with
539[ O ⇒ off
540| S n ⇒
541  shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n
542].
543
544(* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a
545   serious PITA to prove. *)
546axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs.
547
548(* Some stuff bunding the size of what we can write in memory *)
549
550(* for leb_elim, shadowed in positive.ma *)
551definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop.
552(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim.
553
554(*include alias "arithmetics/nat.ma".*)
555
556lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. |l| ≤ i → nth_opt A i l = None ?.
557#A #l elim l //
558#hd #tl #H #i elim i
559[ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/
560| 2: #i' #H' #Hle whd in match (nth_opt ???); @H lapply (monotonic_pred … Hle) //
561] qed.
562
563(* In order to prove the lemma on store_value_of_type and load_value_of_type,
564   we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *)
565lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
566* try // * try // qed.
567
568(* Lifting bound on make_list *)
569lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → |make_list A elt sz| ≤ bound.
570#A #sz elim sz try //
571#sz' #Hind #bound #elt #Hbound normalize
572cases bound in Hbound;
573[ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
574| 2: #bound' #Hbound' lapply (Hind bound' elt ?)
575     [ 1: @(monotonic_pred … Hbound')
576     | 2: /2 by le_S_S/ ]
577] qed.
578
579lemma bytes_of_bitvector_bounded :
580  ∀sz,bv. |bytes_of_bitvector (size_intsize sz) bv| = size_intsize sz.
581* #bv normalize
582[ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 //
583| 2: cases (vsplit ????) normalize nodelta #bv0 #bv1
584     cases (vsplit ????) normalize nodelta #bv2 #bv3 //
585| 3: cases (vsplit ????) normalize nodelta #bv0 #bv1
586     cases (vsplit ????) normalize nodelta #bv2 #bv3
587     cases (vsplit ????) normalize nodelta #bv4 #bv5
588     cases (vsplit ????) normalize nodelta #bv6 #bv7
589     //
590] qed.
591
592lemma map_bounded :
593  ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|.
594  #A #B #l elim l try //
595qed.
596
597
598lemma fe_to_be_values_bounded :
599  ∀ty,v. |fe_to_be_values ty v| ≤ 8.
600#ty cases ty
601[ 1: #sz #sg ]
602#v whd in match (fe_to_be_values ??);
603     cases v normalize nodelta
604     [ 1,5: @makelist_bounded @typesize_bounded
605     | 2,6: * normalize nodelta #bv
606          >map_bounded >bytes_of_bitvector_bounded //
607     | 3,7: //
608     | 4,8: #ptr // ]
609qed.     
610
611lemma fe_to_be_values_nonempty : ∀typ,v. ∃hd,tl. fe_to_be_values typ v = hd :: tl.
612*
613[ 2:  * /3 by ex_intro/ * #i
614      [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize
615           lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq
616           <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/
617      | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize
618           lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq
619           <(vsplit_prod … Heq) normalize nodelta
620           lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq'
621            /3 by ex_intro/
622      | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize
623           lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq
624           <(vsplit_prod … Heq) normalize nodelta
625           lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq'
626           <(vsplit_prod … Heq') normalize nodelta
627           lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq''
628           <(vsplit_prod … Heq'') normalize nodelta
629           lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq'''
630            /3 by ex_intro/ ]
631| 1: #sz #sg * /3 by ex_intro/ * #i
632      [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize
633           lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq
634           <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/
635      | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize
636           lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq
637           <(vsplit_prod … Heq) normalize nodelta
638           lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq'
639            /3 by ex_intro/
640      | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize
641           lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq
642           <(vsplit_prod … Heq) normalize nodelta
643           lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq'
644           <(vsplit_prod … Heq') normalize nodelta
645           lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq''
646           <(vsplit_prod … Heq'') normalize nodelta
647           lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq'''
648            /3 by ex_intro/ ]
649] qed.       
650
651
652(* /!\ TODO the following proof is extremely ugly and indirect. I expect it to be
653 *      hugely improvable.
654 * /!\ *)
655
656(* We prove some properties of [storen m ptr data]. Note that [data] is a list of back-end chunks.
657   What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to
658   have is that the contents of this particular zone (ptr to ptr+|data|-1) match exactly [data], and
659   that elsewhere the memory is untouched.
660   Not so simple. Some observations:
661   A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16).
662      On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems
663      when writing at the edge of the range of offsets and wrapping around, but that can be solved
664      resorting to ugliness and trickery.
665   B) The [data] list is unbounded. Taking into account the point A), this means that we can lose
666      data when writing (exactly as when we write in a circular buffer, overwriting previous stuff).
667      The only solution to that is to explicitly bound |data| with something reasonable.
668   Taking these observations into account, we prove the following invariants:
669  1) storing doesn't modify the nextblock (trivial)
670  2) it does not modify the extents of the block written to (trivial)
671  3) all the offsets on which we run while writing are legal (trivial)
672  3) if we index properly, we hit the stored data in the same order as in the list
673  4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere",
674     because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as
675     "not reachable by shiftn from [ofs] to |data|"
676  5) the pointer we write to is valid (trivial)
677*)
678lemma mem_bounds_invariant_after_storen :
679  ∀data,m,m',b,ofs.
680    |data| ≤ 8 → (* 8 is the size of a double. *)
681    storen m (mk_pointer b ofs) data = Some ? m' →
682    (nextblock m' = nextblock m ∧
683    (∀b.low (blocks m' b) = low (blocks m b) ∧
684        high (blocks m' b) = high (blocks m b)) ∧
685    (∀index. index < |data| → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧
686                               Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧
687    (∀index. index < |data| → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧
688    (∀o. (∀i. i < |data| → o ≠ shiftn ofs i) →
689         contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧
690    (|data| > 0 → valid_pointer m (mk_pointer b ofs) = true)).
691#l elim l
692[ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl
693     [ 1: #b0 @conj try @refl
694(*     | 2: #Habsurd @False_ind /2 by le_S_O_absurd/*)
695     | 2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/
696     | 4: #o #Hout @refl
697     | 5: #H @False_ind /2 by le_S_O_absurd/ ]
698| 2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren
699     whd in Hstoren:(??%?);
700     cases (some_inversion ????? Hstoren) #m'' * #Hbestorev -Hstoren #Hstoren
701     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK
702     lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * *
703     #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj
704     [ 1: <HA <HC @refl
705     | 2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try //     
706     | 4: *
707          [ 1: #_ <HJ whd in match (nth 0 ???);
708               lapply (HV ofs ?)
709               [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs)
710                    [ 1: normalize in Hsize_bound;
711                         cut (|tl| < 8) [ /2 by lt_plus_to_minus_r/ ]
712                         #Hlt' lapply (transitive_lt … Hlt Hlt') // ]
713                    * #H @H whd in match (shiftn ??); @Heq
714               | 2: cases ofs #ofs' normalize // ]
715          | 2: #i' #Hlt lapply (HF i' ?)
716               [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) //
717               | 2: #H whd in match (nth_opt ???); >H @refl ] ]
718     | 5: #o #H >HV
719          [ 2: #i #Hlt @(H (S i) ?)
720               normalize normalize in Hlt; /2 by le_S_S/
721          | 1: @HK @(H 0) // ]     
722     | 6: #_ @(bestorev_to_valid_pointer … Hbestorev)
723     | 3: *
724          [ 1: #_ <HJ whd in match (shiftn ??);
725               lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
726               lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
727               whd in match (low_bound ??); whd in match (high_bound ??);
728               cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
729               cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
730               [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb
731               lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) -Hleb #Hleb'
732               normalize @conj try assumption
733          | 2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2
734               lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ]
735               >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2
736          ]
737     ]
738] qed.
739
740(* Adapting the lemma above to (fe_to_be_values ty v) *)
741lemma mem_bounds_invariant_after_storen_bis :
742  ∀ty,v,m,m',b,ofs.
743    storen m (mk_pointer b ofs) (fe_to_be_values ty v) = Some ? m' →
744    (nextblock m' = nextblock m ∧
745    (∀b.low (blocks m' b) = low (blocks m b) ∧
746        high (blocks m' b) = high (blocks m b)) ∧
747    (∀index. index < |fe_to_be_values ty v| →
748             low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧
749             Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧
750    (∀index. index < |(fe_to_be_values ty v)| →
751             nth_opt ? index (fe_to_be_values ty v) = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧
752    (∀o. (∀i. i < |fe_to_be_values ty v| → o ≠ shiftn ofs i) →
753         contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧
754    (valid_pointer m (mk_pointer b ofs) = true)).
755#ty #v #m #m' #b #ofs #Hstoren   
756lapply (mem_bounds_invariant_after_storen … Hstoren)
757[ @fe_to_be_values_bounded ]
758* * * * * #H1 #H2 #H3 #H4 #H5 #H6 @conj try @conj try @conj try @conj try @conj
759try assumption @H6
760cases (fe_to_be_values_nonempty ty v) #hd * #tl #H >H //
761qed.
762
763(* extension of [bestorev_to_valid_pointer] to storen *)
764lemma storen_to_valid_pointer :
765  ∀data,xd,m,ptr,m'. storen m ptr (xd::data) = Some ? m' →
766    (∀b.low (blocks m' b) = low (blocks m b) ∧
767         high (blocks m' b) = high (blocks m b)) ∧
768    nextblock m' = nextblock m ∧         
769    valid_pointer m ptr = true ∧
770    valid_pointer m' ptr = true.
771#data elim data
772[ 1: #xd #m #ptr #res #Hstoren whd in Hstoren:(??%?);
773     cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren'
774     normalize in Hstoren'; destruct (Hstoren')
775     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF
776     lapply (bestorev_to_valid_pointer … Hbestorev) #Hvalid_ptr @conj try @conj try @conj try assumption
777     @(bestorev_to_valid_pointer_after … Hbestorev)
778| 2: #hd #tl #Hind #xd #m #ptr #res whd in match (storen ???); #Hstoren
779     cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren' -Hstoren
780     whd in match (shift_pointer ???) in Hstoren';
781     lapply (bestorev_to_valid_pointer … Hbestorev) #H @conj try @conj try @conj try //
782     lapply (Hind … Hstoren') * * * #Hbounds #Hnext #Hvalid1 #Hvalid2
783     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF
784     [ 1: #b @conj cases (Hbounds b) #HG #HH cases (HB b) #HI #HJ try //
785     | 2: >Hnext >HA @refl ]
786     @valid_pointer_of_Prop @conj try @conj try @conj
787     cases (Hbounds (pblock ptr)) #HG #HH cases (HB (pblock ptr)) #HI #HJ
788     [ 2: cases HC #Hlow #_ whd in match (low_bound ??);
789           whd in match (Z_of_offset ?) in Hlow;
790           >HG >HI @Hlow
791     | 3: cases HC #_ #Hhigh whd in match (high_bound ??); >HH >HJ @Hhigh ]
792     lapply (valid_pointer_to_Prop … Hvalid2) * * #Hnext #Hlow #Hhigh //
793] qed.
794
795     
796
797lemma storen_to_valid_pointer_fe_to_be :
798  ∀typ,v,m,ptr,m'. storen m ptr (fe_to_be_values typ v) = Some ? m' →
799    (∀b.low (blocks m' b) = low (blocks m b) ∧
800         high (blocks m' b) = high (blocks m b)) ∧
801    nextblock m' = nextblock m ∧         
802    valid_pointer m ptr = true ∧
803    valid_pointer m' ptr = true.
804#typ #v cases (fe_to_be_values_nonempty … typ v) #hd * #tl #Heq >Heq
805@storen_to_valid_pointer
806qed.
807
808lemma storen_beloadv_ok :
809  ∀m,m',b,ofs,hd,tl.
810  |hd::tl| ≤ 8 → (* 8 is the size of a double. *)
811  storen m (mk_pointer b ofs) (hd::tl) = Some ? m' →
812  ∀i. i < |hd::tl| → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl).
813#m #m' #b #ofs #hd #tl #Hle #Hstoren
814lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
815#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
816#i #Hle lapply (Hdata i Hle) #Helt >Helt
817whd in match (beloadv ??); whd in match (nth_opt ???);
818lapply (Hvalid_ptr ?) try //
819whd in ⊢ ((??%?) → ?);
820>Hnext cases (Zltb (block_id b) (nextblock m))
821[ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ]
822>andb_lsimpl_true normalize nodelta
823whd in match (low_bound ??); whd in match (high_bound ??);
824cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H
825lapply (Hvalid_offs i Hle) * #Hzle #Hzlt
826>(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl
827qed.
828
829lemma storen_loadn_nonempty :
830  ∀data,m,m',b,ofs.
831  |data| ≤ 8 →
832  storen m (mk_pointer b ofs) data = Some ? m' →
833  ∃result. loadn m' (mk_pointer b ofs) (|data|) = Some ? result ∧ |result|=|data|.
834#data elim data
835[ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ]
836#hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren
837lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
838#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
839cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0
840whd in match (loadn ???);
841lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
842whd in match (beloadv ??);
843whd in match (low_bound ??); whd in match (high_bound ??);
844>Hnext
845cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
846normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh
847cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta
848[ 2: #Habsurd destruct ] >andb_lsimpl_true
849#Hltb >Hltb normalize nodelta
850cases (Hind  … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ]
851#tl' * #Hloadn >Hloadn #Htl' normalize nodelta
852%{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl
853normalize >Htl' @refl
854qed.
855
856
857lemma loadn_beloadv_ok :
858  ∀size,m,b,ofs,result.
859  loadn m (mk_pointer b ofs) size = Some ? result →
860  ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result.
861#size elim size
862[ 1: #m #b #ofs #result #Hloadn *
863     [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
864     | 2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ]
865| 2: #size' #Hind_size #m #b #ofs #result #Hloadn #i
866     elim i
867     [ 1: #_
868          cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
869          cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq
870          destruct (Heq) whd in match (shiftn ofs 0);
871          >Hbeloadv @refl
872    | 2: #i' #Hind #Hlt
873         whd in match (shiftn ofs (S i'));
874         lapply (Hind ?)
875         [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind
876         whd in Hloadn:(??%?);
877         cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
878         cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq -Hloadn'
879         destruct (Heq)
880         @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ]
881         @Hloadn_tl
882    ]
883] qed.
884
885
886
887lemma storen_loadn_ok :
888  ∀data.
889  |data| ≤ 8 → (* 8 is the size of a double. *)
890  ∀m,m',b,ofs.
891  storen m (mk_pointer b ofs) data = Some ? m' →
892  loadn m' (mk_pointer b ofs) (|data|) = Some ? data.
893#data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren
894lapply (storen_beloadv_ok m m' …  Hle Hstoren) #Hyp_storen
895cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz
896lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn
897cut (∀i. i < |hd::tl| → nth_opt ? i (hd::tl) = nth_opt ? i result)
898[ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1
899  lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ]
900#Hyp
901cut (result = hd :: tl)
902[ 2: #Heq destruct (Heq) @Hloadn ]
903@nth_eq_to_eq #i @sym_eq
904@(leb_elim' … (S i) (|hd::tl|))
905[ 1: #Hle @(Hyp ? Hle)
906| 2: #Hnle cut (|hd::tl| ≤ i)
907     [ lapply (not_le_to_lt … Hnle) normalize
908       @monotonic_pred ]
909     #Hle'
910     >nth_miss // >nth_miss //
911] qed.
912 
913
914lemma mem_bounds_after_store_value_of_type :
915  ∀m,m',ty,b,o,v.
916  store_value_of_type ty m b o v = Some ? m' →
917  (nextblock m' = nextblock m ∧
918   (∀b.low (blocks m' b) = low (blocks m b) ∧
919       high (blocks m' b) = high (blocks m b))).
920#m #m' #ty #b #o #v
921lapply (fe_to_be_values_bounded (typ_of_type ty) v)
922cases ty
923[ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty
924| 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ]
925whd in match (typ_of_type ?); #Hbounded
926whd in match (store_value_of_type ?????);
927[ 1,4,5,6,7: #Habsurd destruct (Habsurd)
928| *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren)
929     * * * * * #Hnextblock #Hbounds_eq #Hnonempty
930     #Hcontents_upd #Hcontents_inv #Hvalid_ptr
931     >Hnextblock @conj //
932] qed.
933
934lemma mem_bounds_after_store_value_of_type' :
935  ∀m,m',ty,p,v.
936  store_value_of_type' ty m p v = Some ? m' →
937  (nextblock m' = nextblock m ∧
938   (∀b.low (blocks m' b) = low (blocks m b) ∧
939       high (blocks m' b) = high (blocks m b))).
940#m #m' #ty * #b #o #v whd in match (store_value_of_type' ????);
941@mem_bounds_after_store_value_of_type
942qed.
943
944
945definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v.
946  match ty with
947  [ ASTint sz sg ⇒
948    match v with
949    [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *)
950    | _ ⇒ False ]
951  | ASTptr ⇒
952    match v with
953    [ Vptr p ⇒ True
954    | _ ⇒ False ]
955  ].
956
957
958definition type_consistent_with_value : type → val → Prop ≝ λty,v.
959match access_mode ty with
960[ By_value chunk ⇒ ast_typ_consistent_with_value chunk v
961| _ ⇒ True
962].
963
964(* We also need the following property. It is not provable unless [v] and [ty] are consistent. *)
965lemma fe_to_be_values_size :
966  ∀ty,v. ast_typ_consistent_with_value ty v →
967         typesize ty = |fe_to_be_values ty v|.
968*
969[ 1: #sz #sg #v
970     whd in match (fe_to_be_values ??); cases v
971     normalize in ⊢ (% → ?);
972     [ 1,3: @False_ind
973     | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta
974          >map_bounded >bytes_of_bitvector_bounded cases sz' //
975     | 4: #p normalize in ⊢ (% → ?); @False_ind ]
976| 2: #v cases v
977     normalize in ⊢ (% → ?);
978     [ 1,3: @False_ind
979     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
980     | 4: #p #_ // ]
981] qed.
982
983(* Not verified for floats atm. Restricting to integers. *)
984lemma fe_to_be_to_fe_value_int : ∀sz,sg,v.
985  ast_typ_consistent_with_value (ASTint sz sg) v →
986  (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v).
987#sz #sg #v
988whd in match (fe_to_be_values ??);
989cases v normalize in ⊢ (% → ?);
990[ 1,3: @False_ind
991| 4: #p @False_ind
992| 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta
993     cases sz' in i'; #i normalize nodelta
994     normalize in i;
995     whd in match (be_to_fe_value ??);
996     normalize in match (size_intsize ?);
997     whd in match (bytes_of_bitvector ??);
998     [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i
999          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
1000          whd in match (build_integer_val ??);
1001          >(BitVector_O … ri) //
1002     | 2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i
1003          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
1004          whd in match (build_integer_val ??);
1005          normalize in match (size_intsize ?);
1006          whd in match (bytes_of_bitvector ??);
1007          lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri
1008          <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri
1009          whd in match (build_integer_val ??);
1010          >(BitVector_O … rri) //
1011     | 3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i
1012          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
1013          whd in match (build_integer_val ??);
1014          normalize in match (size_intsize ?);
1015          whd in match (bytes_of_bitvector ??);
1016          lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB
1017          <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB
1018          whd in match (bytes_of_bitvector ??);
1019          lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD
1020          <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD
1021          whd in match (bytes_of_bitvector ??);
1022          lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF
1023          <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF
1024          >(BitVector_O … iH) @refl ]
1025] qed.
1026
1027lemma fe_to_be_to_fe_value_ptr :
1028  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
1029#b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
1030cases br normalize nodelta >eqZb_z_z normalize nodelta
1031cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
1032<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
1033* //
1034qed.
1035
1036(* It turns out that the following property is not true in general. Floats are converted to
1037   BVundef, which are converted back to Vundef. But we care only about ints.  *)
1038lemma storev_loadv_int_compatible :
1039  ∀sz,sg,m,b,ofs,v,m'.
1040    ast_typ_consistent_with_value (ASTint sz sg) v →
1041    store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' →
1042    load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v.
1043#sz #sg #m #b #ofs #v #m' #H
1044whd in ⊢ ((??%?) → (??%?)); #Hstoren
1045lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren)
1046>(fe_to_be_values_size … H) #H >H normalize nodelta
1047>fe_to_be_to_fe_value_int try //
1048qed.
1049
1050(* For the arguments exposed before, we restrict the lemma to ints. *)
1051lemma store_value_load_value_int_compatible :
1052  ∀sz,sg,m,b,ofs,v,m'.
1053    type_consistent_with_value (Tint sz sg) v →
1054    store_value_of_type (Tint sz sg) m b ofs v = Some ? m' →
1055    load_value_of_type (Tint sz sg) m' b ofs = Some ? v.
1056#sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?);
1057cases v in H; normalize nodelta
1058[ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #_ @False_ind | 4: #vp #_ @False_ind ]
1059#Heq >Heq in H; #H
1060(* The lack of control on unfolds is extremely annoying. *)
1061whd in match (store_value_of_type ?????); #Hstoren
1062lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren)
1063whd in match (load_value_of_type ????);
1064>(fe_to_be_values_size … H) #H' >H' normalize nodelta
1065>fe_to_be_to_fe_value_int try //
1066qed.
1067
1068lemma store_value_load_value_compatible :
1069  ∀ty,m,b,ofs,v,m'.
1070    type_consistent_with_value ty v →
1071    store_value_of_type ty m b ofs v = Some ? m' →
1072    load_value_of_type ty m' b ofs = Some ? v.
1073#ty #m #b #ofs #v #m' #H lapply H cases ty
1074[ | #sz #sg | #ty' | #ty' #n | #tl #ty' | #id #fl | #id #fl | #id ]
1075[ 1,4,5,6,7: normalize in ⊢ (? → % → ?); #_ #Habsurd destruct
1076| 2: @store_value_load_value_int_compatible
1077| 3: #Hconsistent whd in match (store_value_of_type ?????);
1078     whd in match (load_value_of_type ????); #Hstoren
1079     lapply (storen_loadn_ok … Hstoren)
1080     [ @fe_to_be_values_bounded ]
1081     #Hloadn >(fe_to_be_values_size … Hconsistent)
1082     >Hloadn normalize nodelta
1083     cases v in Hconsistent;
1084     [ @False_ind | #sz' #i' @False_ind | 3: @False_ind ]
1085     * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl
1086| 8: #Hconsistent whd in match (store_value_of_type ?????);
1087     whd in match (load_value_of_type ????); #Hstoren
1088     lapply (storen_loadn_ok … Hstoren)
1089     [ @fe_to_be_values_bounded ]
1090     #Hloadn >(fe_to_be_values_size … Hconsistent)
1091     >Hloadn normalize nodelta
1092     cases v in Hconsistent;
1093     [ @False_ind | #sz' #i' @False_ind | 3: @False_ind ]
1094     * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl
1095] qed.
1096
1097(* storing something somewhere and loading at a disjoint loc yields the
1098   same result as before the store. *)
1099lemma store_value_load_disjoint :
1100  ∀ty1,ty2,m,b1,ofs1,b2,ofs2,v,m'.
1101    ty1 ≠ ty2 →
1102    type_consistent_with_value ty1 v →
1103    store_value_of_type ty1 m b1 ofs1 v = Some ? m' →
1104    (b1 ≠ b2
1105     ∨ ((Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1))) ≤ (Z_of_offset ofs2))
1106     ∨ ((Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2))) ≤ (Z_of_offset ofs1))) →
1107    load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2.
1108#ty1 #ty2 #m #b1 #ofs1 #b2 #ofs2 #v #m'
1109@cthulhu (*  Provable using the invariants provided by storen (see prev. lemma) *)
1110qed.
1111
1112(* Can we say anything about what we load in the overlap case ?  *)
1113(*
1114lemma store_value_load_overlap :
1115  ∀ty1,ty2,m,b,ofs1,ofs2,v,m'.
1116    ty1 ≠ ty2 →
1117    type_consistent_with_value ty1 v →
1118    store_value_of_type ty1 m b1 ofs1 v = Some ? m' →
1119    (Z_of_offset ofs2 < (Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1)))
1120     ∨ Z_of_offset ofs1 < (Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2)))) →
1121    load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2.
1122*)
Note: See TracBrowser for help on using the repository browser.