source: src/Clight/MemProperties.ma @ 2896

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

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

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