source: src/Clight/MemProperties.ma @ 2441

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

Moved general stuff on memories from switchRemoval to MemProperties?, e.g. on loading, storing and free, as an
attempt to reduce the typechecking time of switchRemoval.ma.
Moved some other generic stuff on vectors from SimplifyCasts? to frontend_misc.

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