Changeset 2441 for src/Clight/switchRemoval.ma
 Timestamp:
 Nov 7, 2012, 6:02:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2438 r2441 7 7 include "Clight/frontend_misc.ma". 8 8 include "Clight/memoryInjections.ma". 9 include "Clight/MemProperties.ma". 9 10 include "basics/lists/list.ma". 10 11 include "basics/lists/listb.ma". 11 include "Clight/SimplifyCasts.ma". 12 12 13 13 14 … … 778 779 ]. 779 780 780 (*  *) 781 (* "Observational" memory equivalence. Memories use closures to represent contents, 782 so we have to use that short of asserting functional extensionality to reason 783 on reordering of operations on memories, among others. For our 784 limited purposes, we do not need (at this time of writing, i.e. 22 sept. 2012) 785 to push the observation in the content_map. *) 786 (*  *) 787 definition memory_eq ≝ λm1,m2. 788 nextblock m1 = nextblock m2 ∧ 789 ∀b. blocks m1 b = blocks m2 b. 790 791 (* memory_eq is an equivalence relation. *) 792 lemma reflexive_memory_eq : reflexive ? memory_eq. 793 whd * #contents #nextblock #Hpos normalize @conj try // 794 qed. 795 796 lemma symmetric_memory_eq : symmetric ? memory_eq. 797 whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos' 798 normalize * #H1 #H2 @conj >H1 try // 799 qed. 800 801 lemma transitive_memory_eq : transitive ? memory_eq. 802 whd 803 * #contents #nextblock #Hpos 804 * #contents1 #nextblock1 #Hpos1 805 * #contents2 #nextblock2 #Hpos2 806 normalize * #H1 #H2 * #H3 #H4 @conj // 807 qed. 781 808 782 809 783 (*  *) … … 811 785 properties at the backend level. *) 812 786 (*  *) 813 814 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the backend values are equal. *)815 definition load_sim ≝816 λ(m1 : mem).λ(m2 : mem).817 ∀ptr,bev.818 beloadv m1 ptr = Some ? bev →819 beloadv m2 ptr = Some ? bev.820 821 definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.822 823 lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p.824 #m #p @conj825 [ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);826 whd in match (do_if_in_bounds); normalize nodelta827 cases (Zltb (block_id (pblock p)) (nextblock m))828 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]829 >andb_lsimpl_true normalize nodelta830 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))831 [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]832 >andb_lsimpl_true normalize nodelta833 #Hlt >Hlt normalize nodelta #A #f /2 by ex_intro/834  2: whd in match (valid_pointer ??);835 whd in match (in_bounds_pointer ??); #H836 lapply (H bool (λblock,contents,off. true))837 * #foo whd in match (do_if_in_bounds ????);838 cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta839 [ 2: #Habsurd destruct (Habsurd) ]840 >andb_lsimpl_true841 cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))842 normalize nodelta843 [ 2: #Habsurd destruct (Habsurd) ]844 >andb_lsimpl_true845 elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))846 [ 1: #H >H //847  2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]848 ] qed.849 850 lemma valid_pointer_to_Prop :851 ∀m,p. valid_pointer m p = true →852 (block_id (pblock p)) < (nextblock m) ∧853 (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧854 (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)).855 #m #p whd in match (valid_pointer ??);856 #H857 lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))858 lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m))859 cases (Zltb (block_id (pblock p)) (nextblock m)) in H;860 [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true861 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))862 normalize nodelta863 [ 2: #Habsurd destruct ]864 #Hlt1 #Hlt2 #Hle @conj try @conj865 try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1)866 qed.867 787 868 788 (* A writeable_block is a block that is: … … 1284 1204 1285 1205 (*  *) 1286 (* Lift beloadv simulation to the frontend. *)1287 1288 (* Lift load_sim to loadn. *)1289 lemma load_sim_loadn :1290 ∀m1,m2. load_sim m1 m2 →1291 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.1292 #m1 #m2 #Hload_sim #sz1293 elim sz1294 [ 1: #p #res #H @H1295  2: #n' #Hind #p #res1296 whd in match (loadn ???);1297 whd in match (loadn m2 ??);1298 lapply (Hload_sim p)1299 cases (beloadv m1 p) normalize nodelta1300 [ 1: #_ #Habsurd destruct (Habsurd) ]1301 #bval #H >(H ? (refl ??)) normalize nodelta1302 lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))1303 cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')1304 normalize nodelta1305 [ 1: #_ #Habsurd destruct (Habsurd) ]1306 #res' #H >(H ? (refl ??)) normalize1307 #H @H1308 ] qed.1309 1310 (* Lift load_sim to frontend values. *)1311 lemma load_sim_fe :1312 ∀m1,m2. load_sim m1 m2 →1313 ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →1314 load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.1315 #m1 #m2 #Hloadsim #ptr #ty #v1316 cases ty1317 [ 1:  2: #sz #sg  3: #fsz  4: #ptrty  5: #arrayty #arraysz  6: #argsty #retty1318  7: #sid #fields  8: #uid #fields  9: #cptr_id ]1319 whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));1320 [ 1,7,8: #Habsurd destruct (Habsurd)1321  5,6: #H @H1322  2,3,4,9:1323 generalize in match (mk_pointer (pblock ptr) (poff ptr));1324 elim (typesize ?)1325 [ 1,3,5,7: #p #H @H1326  2,4,6,8: #n' #Hind #p1327 lapply (load_sim_loadn … Hloadsim (S n') p)1328 cases (loadn m1 p (S n')) normalize nodelta1329 [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]1330 #bv #H >(H ? (refl ??)) #H @H1331 ]1332 ] qed.1333 1334 (*  *)1335 (* Lemmas relating reading and writing operation to memory properties. *)1336 1337 (* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)1338 lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true.1339 * #contents #next #nextpos #ptr #res1340 whd in match (beloadv ??);1341 whd in match (valid_pointer ??);1342 cases (Zltb (block_id (pblock ptr)) next)1343 normalize nodelta1344 [ 2: #Habsurd destruct (Habsurd) ]1345 >andb_lsimpl_true1346 whd in match (low_bound ??);1347 whd in match (high_bound ??);1348 cases (Zleb (low (contents (pblock ptr)))1349 (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))1350 [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]1351 >andb_lsimpl_true1352 normalize nodelta #H1353 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;1354 try // normalize #Habsurd destruct (Habsurd)1355 qed.1356 1357 lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true.1358 * #contents #next #nextpos #ptr #v #res1359 whd in match (bestorev ???);1360 whd in match (valid_pointer ??);1361 cases (Zltb (block_id (pblock ptr)) next)1362 normalize nodelta1363 [ 2: #Habsurd destruct (Habsurd) ]1364 >andb_lsimpl_true1365 whd in match (low_bound ??);1366 whd in match (high_bound ??);1367 cases (Zleb (low (contents (pblock ptr)))1368 (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))1369 [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]1370 >andb_lsimpl_true1371 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))1372 normalize nodelta try // #Habsurd destruct (Habsurd)1373 qed.1374 1375 (*  *)1376 1206 (* Lemmas relating memory extensions to [free] *) 1377 1378 lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).1379 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize1380 @(eqZb_elim … bid1 bid2)1381 [ 1: #Heq >Heq cases br1 cases br2 normalize1382 [ 1,4: * #H @(False_ind … (H (refl ??))) ]1383 #_ @refl1384  2: cases br1 cases br2 normalize #_ #_ @refl ]1385 qed.1386 1387 lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).1388 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize1389 @(eqZb_elim … bid1 bid2)1390 [ 1: #Heq >Heq cases br1 cases br2 normalize1391 [ 1,4: * #H @(False_ind … (H (refl ??))) ]1392 #_ @refl1393  2: cases br1 cases br2 normalize #_ #_ @refl ]1394 qed.1395 1396 lemma beloadv_free_blocks_neq :1397 ∀m,block,pblock,poff,res.1398 beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.1399 * #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res1400 normalize1401 cases (Zltb pbid next) normalize nodelta1402 [ 2: #Habsurd destruct (Habsurd) ]1403 cases pbr cases br normalize nodelta1404 [ 2,3: #_ % #Habsurd destruct (Habsurd) ]1405 @(eqZb_elim pbid bid) normalize nodelta1406 #Heq destruct (Heq)1407 [ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]1408 #_ % #H destruct (H) elim Heq #H @H @refl1409 qed.1410 1411 lemma beloadv_free_beloadv :1412 ∀m,block,ptr,res.1413 beloadv (free m block) ptr = Some ? res →1414 beloadv m ptr = Some ? res.1415 * #contents #next #nextpos #block * #pblock #poff #res1416 #H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq1417 lapply H1418 whd in match (beloadv ??);1419 whd in match (beloadv ??) in ⊢ (? → %);1420 whd in match (nextblock (free ??));1421 cases (Zltb (block_id pblock) next)1422 [ 2: normalize #Habsurd destruct (Habsurd) ]1423 normalize nodelta1424 <(low_free_eq … Hblocks_neq)1425 <(high_free_eq … Hblocks_neq)1426 whd in match (free ??);1427 whd in match (update_block ?????);1428 @(eq_block_elim … pblock block)1429 [ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ]1430 #_ normalize nodelta1431 #H @H1432 qed.1433 1434 lemma beloadv_free_beloadv2 :1435 ∀m,block,ptr,res.1436 pblock ptr ≠ block →1437 beloadv m ptr = Some ? res →1438 beloadv (free m block) ptr = Some ? res.1439 * #contents #next #nextpos #block * #pblock #poff #res #Hneq1440 whd in match (beloadv ??);1441 whd in match (beloadv ??) in ⊢ (? → %);1442 whd in match (nextblock (free ??));1443 cases (Zltb (block_id pblock) next)1444 [ 2: normalize #Habsurd destruct (Habsurd) ]1445 normalize nodelta1446 <(low_free_eq … Hneq)1447 <(high_free_eq … Hneq)1448 whd in match (free ??);1449 whd in match (update_block ?????);1450 @(eq_block_elim … pblock block)1451 [ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ]1452 #_ normalize nodelta1453 #H @H1454 qed.1455 1207 1456 1208 lemma beloadv_free_simulation : … … 1469 1221 qed. 1470 1222 1471 (* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *)1472 lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.1473 #m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);1474 #H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);1475 elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))1476 [ 1: #Hlt >Hlt normalize nodelta1477 @(eq_block_elim … b (pblock p))1478 [ 1: #Heq >Heq whd in match (free ??);1479 whd in match (update_block ?????); >eq_block_b_b1480 normalize nodelta normalize in match (low ?);1481 >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta1482 #Habsurd destruct (Habsurd)1483  2: #Hblock_neq whd in match (free ? ?);1484 whd in match (update_block ?????);1485 >(not_eq_block_rev … Hblock_neq) normalize nodelta1486 cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))1487 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]1488 >andb_lsimpl_true1489 lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p)))1490 (high (blocks m (pblock p))))1491 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))1492 [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]1493 normalize nodelta #H #_ /2 by ex_intro/1494 ]1495  2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ]1496 qed.1497 1498 (* Cf [in_bounds_free_to_in_bounds] *)1499 lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.1500 #m #b #p #Hvalid1501 cases (valid_pointer_def … m p) #HA #HB1502 cases (valid_pointer_def … (free m b) p) #HC #HD1503 @HB @(in_bounds_free_to_in_bounds … b)1504 @HC @Hvalid1505 qed.1506 1507 (* Making explicit the argument above. *)1508 lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.1509 #m #b #p1510 whd in match (valid_pointer ??);1511 whd in match (free ??);1512 whd in match (update_block ????);1513 whd in match (low_bound ??);1514 whd in match (high_bound ??);1515 @(eq_block_elim … b (pblock p))1516 [ 1: #Heq <Heq >eq_block_b_b normalize nodelta1517 whd in match (low ?); whd in match (high ?);1518 cases (Zltb ? (nextblock m))1519 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]1520 >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd)1521  2: #Hneq #_ @Hneq ]1522 qed.1523 1223 1524 1224 (* Lifting the property of being valid after a free to memory extensions *) … … 2464 2164 (* current function after translation *) 2465 2165 ∀sss_func_tr : function. 2466 (* variables generated during conversion of the function *) 2166 (* variables generated during conversion of the function *) 2467 2167 ∀sss_new_vars : list (ident × type). 2468 (* statement of the transformation *) 2168 (* statement of the transformation *) 2469 2169 ∀sss_func_hyp : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func. 2470 2170 (* memory state before conversion *) … … 2486 2186 (* The extended environment does not interfer with the old one. *) 2487 2187 ∀sss_env_hyp : disjoint_extension sss_env sss_env_ext sss_new_vars. 2188 (* The new variables are allocated to a size corresponding to their types. *) 2189 ∀sss_new_alloc : 2190 ∀v.meml ? v sss_new_vars → 2191 ∀vb. lookup … sss_env_ext (\fst v) = Some ? vb → 2192 low (blocks sss_m_ext vb) = OZ ∧ 2193 high (blocks sss_m_ext vb) = sizeof (\snd v). 2488 2194 (* Extension blocks are writeable. *) 2489 2195 ∀sss_ext_write : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable. … … 3135 2841 to go back and forth nats, Zs and bitvectors ... *) 3136 2842 3137 lemma fold_left_neq_acc_neq : 3138 ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m. 3139 acc1 ≠ acc2 → 3140 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠ 3141 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2. 3142 #m elim m 3143 [ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) // 3144  2: #m' #Hind #acc1 #acc2 #y1 #y2 3145 elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1 3146 elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2 3147 >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?); 3148 cases hd1 cases hd2 normalize nodelta #H 3149 [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?) 3150 [ 1: % #H' @Hneq destruct (H') @refl ] 3151 * #H' @H' @H 3152  4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?) 3153 [ 1: % #H' @Hneq destruct (H') @refl ] 3154 * #H' @H' @H 3155  2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?) 3156 [ 1: % #H' destruct ] 3157 * #H' @H' try @H 3158  3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?) 3159 [ 1: % #H' destruct ] 3160 * #H' @H' try @H ] 3161 ] qed. 3162 3163 lemma fold_left_eq : 3164 ∀m. ∀acc. ∀y1,y2:BitVector m. 3165 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 = 3166 fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 → 3167 y1 = y2. 3168 #m elim m 3169 [ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) // 3170  2: #m' #Hind #acc #y1 #y2 3171 elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1 3172 elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2 3173 >Heq1 >Heq2 whd in ⊢ ((??%%) → ?); 3174 cases hd1 cases hd2 normalize nodelta 3175 [ 1,4: #H >(Hind … H) @refl 3176  2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?) 3177 [ 1: % #H' destruct ] 3178 * #H @(False_ind … (H Habsurd)) 3179  3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?) 3180 [ 1: % #H' destruct ] 3181 * #H @(False_ind … (H Habsurd)) ] 3182 ] qed. 3183 3184 lemma bv_neq_Z_neq_aux : 3185 ∀n. ∀bv1,bv2 : BitVector n. ∀f. 3186 Z_of_unsigned_bitvector n bv1 ≠ 3187 pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2). 3188 #n elim n 3189 [ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct 3190  2: #n' #Hind #bv1 #bv2 #f 3191 elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1 3192 elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2 3193 >Heq1 >Heq2 % 3194 whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?); 3195 cases hd1 cases hd2 normalize nodelta 3196 normalize in ⊢ ((??%%) → ?); 3197 [ 1: #Hpos destruct (Hpos) 3198 lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?) 3199 [ 1: % #H destruct ] 3200 * #H @H @e0 3201  2: #Hpos destruct (Hpos) 3202 lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?) 3203 [ 1: % #H destruct ] 3204 * #H @H @e0 3205  3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H 3206  4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H 3207 ] 3208 ] qed. 3209 3210 lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n. 3211 bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2. 3212 #n #bv1 #bv2 * #Hneq % #Hneq' @Hneq Hneq lapply Hneq' Hneq' 3213 lapply bv2 lapply bv1 bv1 bv2 3214 elim n 3215 [ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) // 3216  2: #n' #Hind #bv1 #bv2 3217 elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1 3218 elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2 3219 >Heq1 >Heq2 3220 whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?); 3221 cases hd1 cases hd2 normalize nodelta 3222 [ 1: #Heq destruct (Heq) lapply (fold_left_eq … e0) * @refl 3223  4: #H >(Hind ?? H) @refl 3224  2: #H lapply (sym_eq ??? H) H #H 3225 cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H)) 3226  3: #H 3227 cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ] 3228 ] qed. 3229 3230 definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs). 2843 2844 3231 2845 3232 2846 (* This axiom looks reasonable to me. But I slept 3 hours last night. *) … … 3252 2866 * #vec *) 3253 2867 3254 (* We prove the following properties for bestorev : 3255 1) storing doesn't modify the nextblock 3256 2) it does not modify the extents of the block written to 3257 3) since we succeeded in storing, the offset is in the bounds 3258 4) reading where we wrote yields the obvious result 3259 5) besides the written offset, the memory contains the same stuff 3260 *) 3261 lemma mem_bounds_invariant_after_bestorev : 3262 ∀m,m',b,ofs,bev. 3263 bestorev m (mk_pointer b ofs) bev = Some ? m' → 3264 nextblock m' = nextblock m ∧ 3265 (∀b.low (blocks m' b) = low (blocks m b) ∧ 3266 high (blocks m' b) = high (blocks m b)) ∧ 3267 (low (blocks m b) ≤ (Z_of_offset ofs) ∧ 3268 (Z_of_offset ofs) < high (blocks m b)) ∧ 3269 (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧ 3270 (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) = 3271 contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))). 3272 #m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?); 3273 #H 3274 cases (if_opt_inversion ???? H) #Hlt H normalize nodelta #H 3275 cases (if_opt_inversion ???? H) #Hlelt H #H 3276 cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj 3277 destruct try @refl 3278 [ 1: 3279 #b' normalize cases b #br #bid cases b' #br' #bid' 3280 cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize 3281 try /2 by conj, refl/ 3282  2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H 3283  3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H 3284  4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize 3285 >eqZb_z_z @refl 3286  5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta 3287 >eqZb_z_z normalize nodelta 3288 @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs))) 3289 [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2 3290 #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?) 3291 [ 1,3: % #Heq destruct cases Hneq #H @H @refl ] 3292 * #H #Habsurd @(False_ind … (H Habsurd)) 3293  2,4: normalize nodelta #H @refl ] 3294 ] qed. 3295 3296 (* Shifts an offset [i] times. storen uses a similar operation internally. *) 3297 let rec shiftn (off:offset) (i:nat) on i : offset ≝ 3298 match i with 3299 [ O ⇒ off 3300  S n ⇒ 3301 shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n 3302 ]. 3303 3304 (* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a 3305 serious PITA to prove. *) 3306 axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs. 3307 3308 (* We prove some properties of [storen m ptr data]. Note that [data] is a list of backend chunks. 3309 What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to 3310 have is that the contents of this particular zone (ptr to ptr+data1) match exactly [data], and 3311 that elsewhere the memory is untouched. 3312 Not so simple. Some observations: 3313 A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16). 3314 On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems 3315 when writing at the edge of the range of offsets and wrapping around, but that can be solved 3316 resorting to ugliness and trickery. 3317 B) The [data] list is unbounded. Taking into account the point A), this means that we can lose 3318 data when writing (exactly as when we write in a circular buffer, overwriting previous stuff). 3319 The only solution to that is to explicitly bound data with something reasonable. 3320 Taking these observations into account, we prove the following invariants: 3321 1) storing doesn't modify the nextblock (trivial) 3322 2) it does not modify the extents of the block written to (trivial) 3323 3) all the offsets on which we run while writing are legal (trivial) 3324 3) if we index properly, we hit the stored data in the same order as in the list 3325 4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere", 3326 because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as 3327 "not reachable by shiftn from [ofs] to data" 3328 5) the pointer we write to is valid (trivial) 3329 *) 3330 lemma mem_bounds_invariant_after_storen : 3331 ∀data,m,m',b,ofs. 3332 data ≤ 8 → (* 8 is the size of a double. *) 3333 storen m (mk_pointer b ofs) data = Some ? m' → 3334 (nextblock m' = nextblock m ∧ 3335 (∀b.low (blocks m' b) = low (blocks m b) ∧ 3336 high (blocks m' b) = high (blocks m b)) ∧ 3337 (∀index. index < data → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧ 3338 Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧ 3339 (∀index. index < data → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧ 3340 (∀o. (∀i. i < data → o ≠ shiftn ofs i) → 3341 contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧ 3342 (data > 0 → valid_pointer m (mk_pointer b ofs) = true)). 3343 #l elim l 3344 [ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl 3345 [ 1: #b0 @conj try @refl 3346 (*  2: #Habsurd @False_ind /2 by le_S_O_absurd/*) 3347  2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/ 3348  4: #o #Hout @refl 3349  5: #H @False_ind /2 by le_S_O_absurd/ ] 3350  2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren 3351 whd in Hstoren:(??%?); 3352 cases (some_inversion ????? Hstoren) #m'' * #Hbestorev Hstoren #Hstoren 3353 lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK 3354 lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * * 3355 #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj 3356 [ 1: <HA <HC @refl 3357  2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try // 3358  4: * 3359 [ 1: #_ <HJ whd in match (nth 0 ???); 3360 lapply (HV ofs ?) 3361 [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs) 3362 [ 1: normalize in Hsize_bound; 3363 cut (tl < 8) [ /2 by lt_plus_to_minus_r/ ] 3364 #Hlt' lapply (transitive_lt … Hlt Hlt') // ] 3365 * #H @H whd in match (shiftn ??); @Heq 3366  2: cases ofs #ofs' normalize // ] 3367  2: #i' #Hlt lapply (HF i' ?) 3368 [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) // 3369  2: #H whd in match (nth_opt ???); >H @refl ] ] 3370  5: #o #H >HV 3371 [ 2: #i #Hlt @(H (S i) ?) 3372 normalize normalize in Hlt; /2 by le_S_S/ 3373  1: @HK @(H 0) // ] 3374  6: #_ @(bestorev_to_valid_pointer … Hbestorev) 3375  3: * 3376 [ 1: #_ <HJ whd in match (shiftn ??); 3377 lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) 3378 lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); 3379 whd in match (low_bound ??); whd in match (high_bound ??); 3380 cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true 3381 cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) 3382 [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb 3383 lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) Hleb #Hleb' 3384 normalize @conj try assumption 3385  2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2 3386 lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ] 3387 >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2 3388 ] 3389 ] 3390 ] qed. 3391 3392 lemma storen_beloadv_ok : 3393 ∀m,m',b,ofs,hd,tl. 3394 hd::tl ≤ 8 → (* 8 is the size of a double. *) 3395 storen m (mk_pointer b ofs) (hd::tl) = Some ? m' → 3396 ∀i. i < hd::tl → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl). 3397 #m #m' #b #ofs #hd #tl #Hle #Hstoren 3398 lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 3399 #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr 3400 #i #Hle lapply (Hdata i Hle) #Helt >Helt 3401 whd in match (beloadv ??); whd in match (nth_opt ???); 3402 lapply (Hvalid_ptr ?) try // 3403 whd in ⊢ ((??%?) → ?); 3404 >Hnext cases (Zltb (block_id b) (nextblock m)) 3405 [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ] 3406 >andb_lsimpl_true normalize nodelta 3407 whd in match (low_bound ??); whd in match (high_bound ??); 3408 cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H 3409 lapply (Hvalid_offs i Hle) * #Hzle #Hzlt 3410 >(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl 3411 qed. 3412 3413 lemma loadn_beloadv_ok : 3414 ∀size,m,b,ofs,result. 3415 loadn m (mk_pointer b ofs) size = Some ? result → 3416 ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result. 3417 #size elim size 3418 [ 1: #m #b #ofs #result #Hloadn * 3419 [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ 3420  2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ] 3421  2: #size' #Hind_size #m #b #ofs #result #Hloadn #i 3422 elim i 3423 [ 1: #_ 3424 cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn' 3425 cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq 3426 destruct (Heq) whd in match (shiftn ofs 0); 3427 >Hbeloadv @refl 3428  2: #i' #Hind #Hlt 3429 whd in match (shiftn ofs (S i')); 3430 lapply (Hind ?) 3431 [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind 3432 whd in Hloadn:(??%?); 3433 cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn' 3434 cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq Hloadn' 3435 destruct (Heq) 3436 @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ] 3437 @Hloadn_tl 3438 ] 3439 ] qed. 3440 3441 lemma storen_loadn_nonempty : 3442 ∀data,m,m',b,ofs. 3443 data ≤ 8 → 3444 storen m (mk_pointer b ofs) data = Some ? m' → 3445 ∃result. loadn m' (mk_pointer b ofs) (data) = Some ? result ∧ result=data. 3446 #data elim data 3447 [ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ] 3448 #hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren 3449 lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 3450 #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr 3451 cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0 3452 whd in match (loadn ???); 3453 lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); 3454 whd in match (beloadv ??); 3455 whd in match (low_bound ??); whd in match (high_bound ??); 3456 >Hnext 3457 cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true 3458 normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh 3459 cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta 3460 [ 2: #Habsurd destruct ] >andb_lsimpl_true 3461 #Hltb >Hltb normalize nodelta 3462 cases (Hind … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ] 3463 #tl' * #Hloadn >Hloadn #Htl' normalize nodelta 3464 %{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl 3465 normalize >Htl' @refl 3466 qed. 3467 3468 let rec double_list_ind 3469 (A : Type[0]) 3470 (P : list A → list A → Prop) 3471 (base_nil : P [ ] [ ]) 3472 (base_l1 : ∀hd1,l1. P (hd1::l1) [ ]) 3473 (base_l2 : ∀hd2,l2. P [ ] (hd2::l2)) 3474 (ind : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2)) 3475 (l1, l2 : list A) on l1 ≝ 3476 match l1 with 3477 [ nil ⇒ 3478 match l2 with 3479 [ nil ⇒ base_nil 3480  cons hd2 tl2 ⇒ base_l2 hd2 tl2 ] 3481  cons hd1 tl1 ⇒ 3482 match l2 with 3483 [ nil ⇒ base_l1 hd1 tl1 3484  cons hd2 tl2 ⇒ 3485 ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2) 3486 ] 3487 ]. 3488 3489 lemma nth_eq_tl : 3490 ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2. 3491 (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) → 3492 (∀i. nth_opt A i l1 = nth_opt A i l2). 3493 #A #l1 #l2 @(double_list_ind … l1 l2) 3494 [ 1: #hd1 #hd2 #_ #i elim i try /2/ 3495  2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct 3496  3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct 3497  4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2 3498 #Hind 3499 @(λi. Hind (S i)) 3500 ] qed. 3501 3502 3503 lemma nth_eq_to_eq : 3504 ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2. 3505 #A #l1 elim l1 3506 [ 1: #l2 #H lapply (H 0) normalize 3507 cases l2 3508 [ 1: // 3509  2: #hd2 #tl2 normalize #Habsurd destruct ] 3510  2: #hd1 #tl1 #Hind * 3511 [ 1: #H lapply (H 0) normalize #Habsurd destruct 3512  2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq) 3513 >(Hind tl2) try @refl @(nth_eq_tl … H) 3514 ] 3515 ] qed. 3516 3517 (* for leb_elim, shadowed in positive.ma *) 3518 definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop. 3519 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim. 3520 3521 include alias "arithmetics/nat.ma". 3522 3523 lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. l ≤ i → nth_opt A i l = None ?. 3524 #A #l elim l // 3525 #hd #tl #H #i elim i 3526 [ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/ 3527  2: #i' #H' #Hle whd in match (nth_opt ???); @H /2 by monotonic_pred/ 3528 ] qed. 3529 3530 lemma storen_loadn_ok : 3531 ∀data. 3532 data ≤ 8 → (* 8 is the size of a double. *) 3533 ∀m,m',b,ofs. 3534 storen m (mk_pointer b ofs) data = Some ? m' → 3535 loadn m' (mk_pointer b ofs) (data) = Some ? data. 3536 #data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren 3537 lapply (storen_beloadv_ok m m' … Hle Hstoren) #Hyp_storen 3538 cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz 3539 lapply (loadn_beloadv_ok (hd::tl) m' b ofs … Hloadn) #Hyp_loadn 3540 cut (∀i. i < hd::tl → nth_opt ? i (hd::tl) = nth_opt ? i result) 3541 [ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1 3542 lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ] 3543 #Hyp 3544 cut (result = hd :: tl) 3545 [ 2: #Heq destruct (Heq) @Hloadn ] 3546 @nth_eq_to_eq #i @sym_eq 3547 @(leb_elim' … (S i) (hd::tl)) 3548 [ 1: #Hle @(Hyp ? Hle) 3549  2: #Hnle cut (hd::tl ≤ i) 3550 [ lapply (not_le_to_lt … Hnle) normalize /2 by monotonic_pred/ ] 3551 #Hle' 3552 >nth_miss // >nth_miss // 3553 ] qed. 3554 3555 (* In order to prove the lemma on store_value_of_type and load_value_of_type, 3556 we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *) 3557 lemma typesize_bounded : ∀ty. typesize ty ≤ 8. 3558 * try // 3559 [ 1: * try // 3560  2: * try // 3561 ] qed. 3562 3563 (* Lifting bound on make_list *) 3564 lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → make_list A elt sz ≤ bound. 3565 #A #sz elim sz try // 3566 #sz' #Hind #bound #elt #Hbound normalize 3567 cases bound in Hbound; 3568 [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ 3569  2: #bound' #Hbound' lapply (Hind bound' elt ?) 3570 [ 1: /2 by monotonic_pred/ 3571  2: /2 by le_S_S/ ] 3572 ] qed. 3573 3574 lemma bytes_of_bitvector_bounded : 3575 ∀sz,bv. bytes_of_bitvector (size_intsize sz) bv = size_intsize sz. 3576 * #bv normalize 3577 [ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 // 3578  2: cases (vsplit ????) normalize nodelta #bv0 #bv1 3579 cases (vsplit ????) normalize nodelta #bv2 #bv3 // 3580  3: cases (vsplit ????) normalize nodelta #bv0 #bv1 3581 cases (vsplit ????) normalize nodelta #bv2 #bv3 3582 cases (vsplit ????) normalize nodelta #bv4 #bv5 3583 cases (vsplit ????) normalize nodelta #bv6 #bv7 3584 // 3585 ] qed. 3586 3587 lemma map_bounded : 3588 ∀A,B:Type[0]. ∀l:list A. ∀f. map A B f l = l. 3589 #A #B #l elim l try // 3590 qed. 3591 3592 lemma fe_to_be_values_bounded : 3593 ∀ty,v. fe_to_be_values ty v ≤ 8. 3594 #ty cases ty 3595 [ 3: #fsz #v whd in match (fe_to_be_values ??); 3596 cases v normalize nodelta 3597 [ 1: @makelist_bounded @typesize_bounded 3598  2: * normalize nodelta #bv 3599 >map_bounded >bytes_of_bitvector_bounded // 3600  3: #fl @makelist_bounded @typesize_bounded 3601  4: // 3602  5: #ptr // ] 3603  2: #v whd in match (fe_to_be_values ??); 3604 cases v normalize nodelta 3605 [ 1: @makelist_bounded @typesize_bounded 3606  2: * normalize nodelta #bv 3607 >map_bounded >bytes_of_bitvector_bounded // 3608  3: #fl @makelist_bounded @typesize_bounded 3609  4: // 3610  5: #ptr // ] 3611  1: #sz #sg #v whd in match (fe_to_be_values ??); 3612 cases v normalize nodelta 3613 [ 1: @makelist_bounded @typesize_bounded 3614  2: * normalize nodelta #bv 3615 >map_bounded >bytes_of_bitvector_bounded // 3616  3: #fl @makelist_bounded @typesize_bounded 3617  4: // 3618  5: #ptr // ] 3619 ] qed. 3620 3621 3622 definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v. 3623 match ty with 3624 [ ASTint sz sg ⇒ 3625 match v with 3626 [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *) 3627  _ ⇒ False ] 3628  ASTptr ⇒ 3629 match v with 3630 [ Vptr p ⇒ True 3631  _ ⇒ False ] 3632  ASTfloat fsz ⇒ 3633 match v with 3634 [ Vfloat _ ⇒ True 3635  _ ⇒ False ] 3636 ]. 3637 3638 3639 definition type_consistent_with_value : type → val → Prop ≝ λty,v. 3640 match access_mode ty with 3641 [ By_value chunk ⇒ ast_typ_consistent_with_value chunk v 3642  _ ⇒ True 3643 ]. 3644 3645 3646 (* We also need the following property. It is not provable unless [v] and [ty] are consistent. *) 3647 lemma fe_to_be_values_size : 3648 ∀ty,v. ast_typ_consistent_with_value ty v → 3649 typesize ty = fe_to_be_values ty v. 3650 * 3651 [ 1: #sz #sg #v 3652 whd in match (fe_to_be_values ??); cases v 3653 normalize in ⊢ (% → ?); 3654 [ 1,4: @False_ind 3655  2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta 3656 >map_bounded >bytes_of_bitvector_bounded cases sz' // 3657  3: #f normalize in ⊢ (% → ?); @False_ind 3658  5: #p normalize in ⊢ (% → ?); @False_ind ] 3659  2: #v cases v 3660 normalize in ⊢ (% → ?); 3661 [ 1,4: @False_ind 3662  2: #sz' #i normalize in ⊢ (% → ?); @False_ind 3663  3: #f normalize in ⊢ (% → ?); @False_ind 3664  5: #p #_ // ] 3665  3: #fsz #v cases v 3666 normalize in ⊢ (% → ?); 3667 [ 1: @False_ind 3668  2: #sz' #i normalize in ⊢ (% → ?); @False_ind 3669  3: #f #_ cases fsz // 3670  4: @False_ind 3671  5: #p normalize in ⊢ (% → ?); @False_ind ] 3672 ] qed. 3673 3674 (* Not verified for floats atm. Restricting to integers. *) 3675 lemma fe_to_be_to_fe_value : ∀sz,sg,v. 3676 ast_typ_consistent_with_value (ASTint sz sg) v → 3677 (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v). 3678 #sz #sg #v 3679 whd in match (fe_to_be_values ??); 3680 cases v normalize in ⊢ (% → ?); 3681 [ 1,4: @False_ind 3682  3: #f @False_ind 3683  5: #p @False_ind 3684  2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta 3685 cases sz' in i'; #i normalize nodelta 3686 normalize in i; 3687 whd in match (be_to_fe_value ??); 3688 normalize in match (size_intsize ?); 3689 whd in match (bytes_of_bitvector ??); 3690 [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i 3691 <(vsplit_prod … Heq_i) normalize nodelta >Heq_i 3692 whd in match (build_integer_val ??); 3693 >(BitVector_O … ri) // 3694  2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i 3695 <(vsplit_prod … Heq_i) normalize nodelta >Heq_i 3696 whd in match (build_integer_val ??); 3697 normalize in match (size_intsize ?); 3698 whd in match (bytes_of_bitvector ??); 3699 lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri 3700 <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri 3701 whd in match (build_integer_val ??); 3702 >(BitVector_O … rri) // 3703  3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i 3704 <(vsplit_prod … Heq_i) normalize nodelta >Heq_i 3705 whd in match (build_integer_val ??); 3706 normalize in match (size_intsize ?); 3707 whd in match (bytes_of_bitvector ??); 3708 lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB 3709 <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB 3710 whd in match (bytes_of_bitvector ??); 3711 lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD 3712 <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD 3713 whd in match (bytes_of_bitvector ??); 3714 lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF 3715 <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF 3716 >(BitVector_O … iH) @refl ] 3717 ] qed. 3718 3719 (* It turns out that the following property is not true in general. Floats are converted to 3720 BVundef, which are converted back to Vundef. But we care only about ints. *) 3721 lemma storev_loadv_ok : 3722 ∀sz,sg,m,b,ofs,v,m'. 3723 ast_typ_consistent_with_value (ASTint sz sg) v → 3724 store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' → 3725 load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v. 3726 #sz #sg #m #b #ofs #v #m' #H 3727 whd in ⊢ ((??%?) → (??%?)); #Hstoren 3728 lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren) 3729 >(fe_to_be_values_size … H) #H >H normalize nodelta 3730 >fe_to_be_to_fe_value try // 3731 qed. 3732 3733 (* For the arguments exposed before, we restrict the lemma to ints. 3734 *) 3735 lemma store_value_load_value_ok : 3736 ∀sz,sg,m,b,ofs,v,m'. 3737 type_consistent_with_value (Tint sz sg) v → 3738 store_value_of_type (Tint sz sg) m b ofs v = Some ? m' → 3739 load_value_of_type (Tint sz sg) m' b ofs = Some ? v. 3740 #sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?); 3741 cases v in H; normalize nodelta 3742 [ 1: #_ @False_ind  2: #vsz #vi #H  3: #vf #_ @False_ind  4: #_ @False_ind  5: #vp #_ @False_ind ] 3743 #Heq >Heq in H; #H 3744 (* The lack of control on unfolds is extremely annoying. *) 3745 whd in match (store_value_of_type ?????); #Hstoren 3746 lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren) 3747 whd in match (load_value_of_type ????); 3748 >(fe_to_be_values_size … H) #H' >H' normalize nodelta 3749 >fe_to_be_to_fe_value try // 3750 qed. 3751 2868 2869 (* 2870 lemma valid_pointer_to_storen_ok : 2871 ∀data,m,p. valid_pointer m p → ∃m'. storen m p data = Some ? m'. 2872 #data elim data try /2 by ex_intro/ 2873 #hd #tl #Hind 2874 #m #p #Hvalid_ptr whd in match (storen ???); 2875 cases (valid_pointer_to_bestorev_ok … hd … Hvalid_ptr) #m' #Hbestorev >Hbestorev 2876 normalize nodelta 2877 lapply (Hind m' (shift_pointer 2 p (bitvector_of_nat 2 1))) 2878 #m #p #data *) 2879 2880 2881 (* 3752 2882 lemma load_int_value_inversion : 3753 2883 ∀t,m,p,sz,i. load_value_of_type' t m p = Some ? (Vint sz i) → ∃sg. t = Tint sz sg. … … 3802 2932 [ 2: #err #f #res normalize nodelta #Habsurd destruct 3803 2933  1: #a #f #res normalize nodelta #Heq destruct %{a} @conj try @refl >Heq @refl 3804 ] qed. 2934 ] qed. *) 2935 2936 (* 2937 lemma valid_pointer_store_succeeds : 2938 ∀sz,sg,m,p,i. 2939 valid_pointer m p → 2940 ∃m'. store_value_of_type (Tint sz sg) m (pblock p) (poff p) (Vint sz i) = Some ? m'. 2941 #sz #sg #m * #b #o #i #Hvalid 2942 whd in match (store_value_of_type' ????); 2943 whd in match (store_value_of_type ?????); 2944 whd in match (storen ???); 2945 *) 2946 3805 2947 3806 2948 (* In order to prove the consistency of types wrt values, we need the following lemma. *) … … 3901 3043 #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars 3902 3044 #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp 3903 #sss_env_hyp #sss_ writeable_hyp #sss_result_rec #sss_result_hyp #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge3045 #sss_env_hyp #sss_new_alloc #sss_writeable_hyp #sss_result_rec #sss_result_hyp #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge 3904 3046 #Hs1_eq #Hs1_eq' 3905 3047 elim (sim_related_globals … ge ge' … … 3973 3115 #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step) 3974 3116 @conj try @refl 3975 %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // 3117 %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // try assumption 3976 3118 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 3977 3119  6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars … … 3992 3134 #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl 3993 3135 %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} 3994 try // 3136 try // try assumption 3995 3137 [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize 3996 3138 cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize … … 4029 3171 * #m_ext' * #Hstore_eq #Hnew_ext >Hstore_eq whd in match (m_bind ?????); 4030 3172 whd destruct @conj try @refl 4031 %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip sss_lu) } try // try assumption 3173 %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip sss_lu) } 3174 try // try assumption 4032 3175 [ 1: @(fresh_for_Sskip … sss_lu_fresh) 4033  2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 3176  3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 3177  2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * #Hlow #Hhigh 3178 lapply (me_nonempty … Hnew_ext) 3179 3180 @cthulhu 3181 ] 4034 3182  3: (* Call statement *) 4035 3183 #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp) … … 4080 3228 cases (switch_removal_elim stm1 sss_lu) #stm1' * #fvs1' * #u' #HeqA >HeqA normalize nodelta 4081 3229 cases (switch_removal_elim stm2 u') #stm2' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta 4082 normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try // 3230 normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} 3231 try // try assumption 4083 3232 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // 4084 3233  2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta … … 4327 3476 #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec Hexec 4328 3477 >sss_result_proj <sss_result_hyp normalize nodelta #Hexec 4329 cases (bindIO_inversion ??????? Hexec) * #condval #condtrace 3478 cases (bindIO_inversion ??????? Hexec) * #condval #condtrace Hexec 4330 3479 cases condval normalize nodelta 4331 3480 [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) … … 4333 3482  4: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 4334 3483  5: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ] 4335 #sz #i * #Hexec_eq #Heq whd in Heq:(??%%); destruct (Heq) 4336 3484 #sz #i * #Hexec_eq #Heq 3485 cut (∃sg. typeof cond = Tint sz sg) whd in Heq:(??%%); destruct (Heq) 3486 [ 1: cases (typeof cond) in Heq; normalize nodelta 3487 [ 1:  2: #sz' #sg'  3: #fsz  4: #ptrty  5: #arrayty #arraysz  6: #argsty #retty 3488  7: #sid #fields  8: #uid #fields  9: #cptr_id ] 3489 [ 2: cases (sz_eq_dec ??) normalize nodelta #H 3490 [ 2: #Habsurd destruct 3491  1: destruct (H) #_ %{sg'} try @refl ] 3492  *: #Habsurd destruct (Habsurd) ] ] 3493 * #sg #Htypeof_cond >Htypeof_cond in Heq; normalize nodelta >sz_eq_identity normalize nodelta 3494 #Heq whd in Heq:(??%%); 3495 cases (bindIO_inversion ??????? Heq) #switchcases_truncated * #Heq1 #Heq2 Heq 3496 whd in Heq1:(??%%); whd in Heq2:(??%%); 3497 cut (select_switch sz i switchcases = Some ? switchcases_truncated) 3498 [ 1: cases (select_switch sz i switchcases) in Heq1; normalize nodelta 3499 [ 1: #Habsurd destruct  2: #ls #Heq destruct (Heq) @refl ] ] 3500 Heq1 #Heq_select_switch destruct (Heq2) 4337 3501 cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq 4338 3502 >Hbranch_eq normalize nodelta 4339 3503 cases (fresh_elim … u') #new * #u'' #Hfresh_eq >Hfresh_eq normalize nodelta 4340 cases (simplify_switch_elim (Expr (Evar new) ( typeof cond)) switchcases' u'') #simplified * #u'''3504 cases (simplify_switch_elim (Expr (Evar new) (Tint sz sg)) switchcases' u'') #simplified * #u''' 4341 3505 #Hswitch_eq >Hswitch_eq normalize nodelta 4342 %{1} whd whd in ⊢ (??%?); 3506 %{1} whd whd in ⊢ (??%?); 4343 3507 (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *) 4344 3508 whd in match (exec_lvalue ????); 4345 3509 (* show that the resulting ident is in the memory extension and that the lookup succeeds *) 4346 Hexec >Hbranch_eq in sss_result_hyp; normalize nodelta 4347 >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta #sss_result_hyp 3510 >Hbranch_eq in sss_result_hyp; normalize nodelta 3511 >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta >Htypeof_cond >Hswitch_eq 3512 normalize nodelta #sss_result_hyp 4348 3513 <sss_result_hyp in sss_incl; whd in match (ret_vars ??); #sss_incl 4349 3514 cases sss_env_hyp * … … 4352 3517 #Hlookup_old 4353 3518 lapply (Hlookup_new_in_new new ?) 4354 3519 [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem; 4355 3520 [ 1: @False_ind 4356 3521  2: * #hdv #hdty #tl #Hind whd in ⊢ (% → (??%?)); * … … 4367 3532 to set up things so that loading from that fresh location will yield exactly the stored value. *) 4368 3533 normalize in match store_value_of_type'; normalize nodelta 3534 whd in match (typeof ?); 3535 4369 3536 @cthulhu 4370 3537  *: @cthulhu ]
Note: See TracChangeset
for help on using the changeset viewer.