source: src/Clight/MemProperties.ma @ 2468

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

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

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