Changeset 2448 for src/Clight
 Timestamp:
 Nov 9, 2012, 4:38:02 PM (9 years ago)
 Location:
 src/Clight
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/MemProperties.ma
r2441 r2448 4 4 include "Clight/frontend_misc.ma". 5 5 include "common/FrontEndMem.ma". 6 7 (* for store_value_of_type' *) 8 include "Clight/Cexec.ma". 9 6 10 7 11 (*  *) … … 57 61 qed. 58 62 63 lemma 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 72 qed. 73 59 74 (*  *) 60 75 (* "Observational" memory equivalence. Memories use closures to represent contents, … … 187 202 qed. 188 203 204 (* valid pointer implies successful bestorev *) 189 205 lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'. 190 206 #m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) * … … 332 348 (*  *) 333 349 (* loading and storing are inverse operations for integers. (Paolo's work 334 * contain a proof of this fact for pointers 350 * contain a proof of this fact for pointers) *) 335 351 (*  *) 336 352 … … 757 773 758 774 775 lemma mem_bounds_after_store_value_of_type : 776 ∀m,m',ty,b,o,v. 777 store_value_of_type ty m b o v = Some ? m' → 778 (nextblock m' = nextblock m ∧ 779 (∀b.low (blocks m' b) = low (blocks m b) ∧ 780 high (blocks m' b) = high (blocks m b))). 781 #m #m' #ty #b #o #v 782 lapply (fe_to_be_values_bounded (typ_of_type ty) v) 783 cases ty 784 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 785  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] 786 whd in match (typ_of_type ?); #Hbounded 787 whd in match (store_value_of_type ?????); 788 [ 1,5,6,7,8: #Habsurd destruct (Habsurd) 789  *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren) 790 * * * * * #Hnextblock #Hbounds_eq #Hnonempty 791 #Hcontents_upd #Hcontents_inv #Hvalid_ptr 792 >Hnextblock @conj // 793 ] qed. 794 795 lemma mem_bounds_after_store_value_of_type' : 796 ∀m,m',ty,p,v. 797 store_value_of_type' ty m p v = Some ? m' → 798 (nextblock m' = nextblock m ∧ 799 (∀b.low (blocks m' b) = low (blocks m b) ∧ 800 high (blocks m' b) = high (blocks m b))). 801 #m #m' #ty * #b #o #v whd in match (store_value_of_type' ????); 802 @mem_bounds_after_store_value_of_type 803 qed. 804 805 759 806 definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v. 760 807 match ty with … … 779 826  _ ⇒ True 780 827 ]. 781 782 828 783 829 (* We also need the following property. It is not provable unless [v] and [ty] are consistent. *) 
src/Clight/frontend_misc.ma
r2441 r2448 1290 1290 @lset_eq_concrete_cons >nil_append >nil_append 1291 1291 @Hind 1292  1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta1293 >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%));1294 @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl'))1295 [ 1: @Hind1296  2: %21297  3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ]1298 ]1292  1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta 1293 >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%)); 1294 @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl')) 1295 [ 1: @Hind 1296  2: %2 1297  3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ] 1298 ] 1299 1299 ] qed. 1300 1300 … … 1417 1417 qed. 1418 1418 1419 1420 1419 (* Additional lemmas on lsets *) 1420 1421 lemma lset_difference_empty : 1422 ∀A : DeqSet. 1423 ∀s1. lset_difference A s1 [ ] = s1. 1424 #A #s1 elim s1 try // 1425 #hd #tl #Hind >lset_difference_unfold >Hind @refl 1426 qed. 1427 1428 lemma lset_not_mem_difference : 1429 ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3). 1430 #A #s1 #s2 #s3 #Hincl #x #Hmem 1431 lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3 1432 elim s1 in Hincl Hmem; 1433 [ 1: #_ * 1434  2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall * 1435 [ 2: #Hmem_x_tl @Hind assumption 1436  1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ] 1437 ] qed. 1438 1439 lemma lset_mem_inclusion_mem : 1440 ∀A,s1,s2,elt. 1441 mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2. 1442 #A #s1 elim s1 1443 [ 1: #s2 #elt * 1444  2: #hd #tl #Hind #s2 #elt * 1445 [ 1: #Heq destruct * // 1446  2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl; 1447 [ 1: #_ * 1448  2: #hd' #tl' #Hind * #Hmem' #Hall * 1449 [ 1: #Heq destruct @Hmem' 1450  2: #Hmem'' @Hind assumption ] ] ] ] 1451 qed. 1452 1453 lemma lset_remove_inclusion : 1454 ∀A : DeqSet. ∀s,elt. 1455 lset_inclusion A (lset_remove ? s elt) s. 1456 #A #s elim s try // qed. 1457 1458 lemma lset_difference_remove_inclusion : 1459 ∀A : DeqSet. ∀s1,s2,elt. 1460 lset_inclusion A 1461 (lset_difference ? (lset_remove ? s1 elt) s2) 1462 (lset_difference ? s1 s2). 1463 #A #s elim s try // qed. 1464 1465 lemma lset_difference_permute : 1466 ∀A : DeqSet. ∀s1,s2,s3. 1467 lset_difference A s1 (s2 @ s3) = 1468 lset_difference A s1 (s3 @ s2). 1469 #A #s1 #s2 elim s2 try // 1470 #hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute 1471 >Hind elim s3 try // 1472 #hd' #tl' #Hind' >cons_to_append >associative_append 1473 >associative_append >(cons_to_append … hd tl) 1474 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append 1475 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append 1476 <Hind' generalize in match (lset_difference ???); #foo 1477 whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?); 1478 whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%)); 1479 elim foo 1480 [ 1: normalize @refl 1481  2: #hd'' #tl'' #Hind normalize 1482 @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with 1483 [ true ⇒ λH. ? 1484  false ⇒ λH. ? 1485 ] (refl ? (hd''==hd'))) 1486 @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with 1487 [ true ⇒ λH'. ? 1488  false ⇒ λH'. ? 1489 ] (refl ? (hd''==hd))) 1490 normalize nodelta 1491 try @Hind 1492 [ 1: normalize >H normalize nodelta @Hind 1493  2: normalize >H' normalize nodelta @Hind 1494  3: normalize >H >H' normalize nodelta >Hind @refl 1495 ] qed. 1496 1497 1498 1499 lemma lset_disjoint_dec : 1500 ∀A : DeqSet. 1501 ∀s1,elt,s2. 1502 mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1). 1503 #A #s1 #elt #s2 1504 @(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ? 1505 with 1506 [ false ⇒ λHA. ? 1507  true ⇒ λHA. ? ] (refl ? (elt ∈ s1))) 1508 [ 1: lapply (memb_to_mem … HA) #Hmem 1509 %1 @Hmem 1510  2: %2 elim s1 in HA; 1511 [ 1: #_ whd %1 @refl 1512  2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?); 1513 >lset_difference_unfold 1514 >lset_difference_unfold2 1515 lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %); 1516 cases (elt==hd1) normalize nodelta 1517 [ 1: #_ #Habsurd destruct 1518  2: #HA #HB >HB normalize nodelta %1 @refl ] ] ] 1519 qed. 1520 1521 lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2. 1522 mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l. 1523 #A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/ 1524 qed. 1525 1526 lemma lset_inclusion_difference_aux : 1527 ∀A : DeqSet. ∀s1,s2. 1528 lset_inclusion A s1 s2 → 1529 (lset_eq A s2 (s1@lset_difference A s2 s1)). 1530 #A #s1 1531 @(WF_ind ????? (filtered_list_wf A s1)) 1532 * 1533 [ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq 1534  2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl 1535 lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?) 1536 [ 1: whd normalize 1537 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ] 1538 #Hind_wf 1539 elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq 1540 >cons_to_append in ⊢ (???%); >associative_append 1541 >lset_difference_unfold2 1542 >nil_append 1543 >lset_remove_split >lset_remove_split 1544 normalize in match (lset_remove ? [hd1] hd1); 1545 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1546 >nil_append <lset_remove_split >lset_difference_lset_remove_commute 1547 lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?) 1548 [ 1: lapply (lset_inclusion_remove … Hincl hd1) 1549 >Heq @lset_inclusion_eq2 1550 >lset_remove_split >lset_remove_split >lset_remove_split 1551 normalize in match (lset_remove ? [hd1] hd1); 1552 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1553 >nil_append @reflexive_lset_eq ] 1554 #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind 1555 @lset_eq_concrete_to_lset_eq 1556 lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc 1557 @(square_lset_eq_concrete ????? Hindc) Hindc Hind 1558 [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B)) 1559 [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete 1560  1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ] 1561  2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …)) 1562 elim (s2A@s2B) 1563 [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq 1564  2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold 1565 @(match (hd2∈filter A (λx:A.¬x==hd1) tl1) 1566 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ? 1567 with 1568 [ false ⇒ λH. ? 1569  true ⇒ λH. ? 1570 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta 1571 [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter)) 1572 normalize nodelta @Hind 1573  2: @(match (hd2∈tl1) 1574 return λx. ((hd2∈tl1) = x) → ? 1575 with 1576 [ false ⇒ λH'. ? 1577  true ⇒ λH'. ? 1578 ] (refl ? (hd2∈tl1))) normalize nodelta 1579 [ 1: (* We have hd2 = hd1 *) 1580 cut (hd2 = hd1) 1581 [ elim tl1 in H H'; 1582 [ 1: normalize #_ #Habsurd destruct (Habsurd) 1583  2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?); 1584 lapply (eqb_true ? hdtl1 hd1) 1585 cases (hdtl1==hd1) normalize nodelta 1586 [ 1: * #H >(H (refl ??)) #_ 1587 lapply (eqb_true ? hd2 hd1) 1588 cases (hd2==hd1) normalize nodelta * 1589 [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl 1590  2: #_ #_ @Hind ] 1591  2: #_ normalize lapply (eqb_true ? hd2 hdtl1) 1592 cases (hd2 == hdtl1) normalize nodelta * 1593 [ 1: #_ #_ #Habsurd destruct (Habsurd) 1594  2: #_ #_ @Hind ] ] ] ] 1595 #Heq_hd2hd1 destruct (Heq_hd2hd1) 1596 @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind) 1597 #Hind' @(square_lset_eq_concrete … Hind') 1598 [ 2: @lset_refl 1599  1: >cons_to_append >cons_to_append in ⊢ (???%); 1600 @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 1601 [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract 1602  2: >(cons_to_append … hd1 (lset_difference ???)) 1603 @lset_eq_concrete_cons >nil_append >nil_append 1604 @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ] 1605  2: @(match hd2 == hd1 1606 return λx. ((hd2 == hd1) = x) → ? 1607 with 1608 [ true ⇒ λH''. ? 1609  false ⇒ λH''. ? 1610 ] (refl ? (hd2 == hd1))) 1611 [ 1: whd in match (lset_remove ???) in ⊢ (???%); 1612 >H'' normalize nodelta >((proj1 … (eqb_true …)) H'') 1613 @(transitive_lset_eq … Hind) 1614 @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 1615 [ 2: @lset_eq_contract ] 1616 @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons 1617 @switch_lset_eq_concrete 1618  2: whd in match (lset_remove ???) in ⊢ (???%); 1619 >H'' >notb_false normalize nodelta 1620 @lset_eq_concrete_to_lset_eq 1621 lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc 1622 lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' Hindc 1623 @(square_lset_eq_concrete … Hindc') 1624 [ 1: @symmetric_lset_eq_concrete 1625 >cons_to_append >cons_to_append in ⊢ (???%); 1626 >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%); 1627 @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 1628  2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 1629 ] 1630 ] 1631 ] 1632 ] 1633 ] 1634 ] 1635 ] qed. 1636 1637 lemma lset_inclusion_difference : 1638 ∀A : DeqSet. 1639 ∀s1,s2 : lset (carr A). 1640 lset_inclusion ? s1 s2 → 1641 ∃s2'. lset_eq ? s2 (s1 @ s2') ∧ 1642 lset_disjoint ? s1 s2' ∧ 1643 lset_eq ? s2' (lset_difference ? s2 s1). 1644 #A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj 1645 [ 1: @lset_inclusion_difference_aux @Hincl 1646  2: /2 by lset_difference_disjoint/ 1647  3,4: @reflexive_lset_inclusion ] 1648 qed. 
src/Clight/memoryInjections.ma
r2438 r2448 777 777  2: % #Hmem @Hguard %2 @Hmem ] 778 778 ] qed. *) 779 779 780 780 781 lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr. 
src/Clight/switchRemoval.ma
r2441 r2448 10 10 include "basics/lists/list.ma". 11 11 include "basics/lists/listb.ma". 12 13 14 15 12 16 13 (*  … … 779 776 ]. 780 777 781 782 783 778 (*  *) 784 779 (* Memory extensions (limited form on memoryInjection.ma). Note that we state the … … 792 787 record nonempty_block (m : mem) (b : block) : Prop ≝ 793 788 { 794 wb_valid 795 wb_nonempty 789 wb_valid : valid_block m b; 790 wb_nonempty : low (blocks m b) < high (blocks m b) 796 791 }. 797 792 … … 1402 1397 qed. 1403 1398 1404 (* freeing equivalent sets of blocks on memory extensions yields memory extensions *)1405 lemma free_equivalent_sets :1406 ∀m1,m2,writeable,set1,set2.1407 lset_eq ? set1 set2 →1408 sr_memext m1 m2 writeable →1409 sr_memext (free_list m1 set1) (free_list m2 set2) (lset_difference ? writeable set1).1410 #m1 #m2 #writeable #set1 #set2 #Heq #Hext1411 lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq))1412 #Heq1413 lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext'1414 lapply (memory_ext_transitive (free_list m1 set1) (free_list m2 set1) (free_list m2 set2) (filter block_eq (λwb:block_eq.¬wb∈set1) writeable) [ ] ? Hext')1415 [ 2: >append_nil #H @H ]1416 elim set11417 [ 1: whd in match (free_list ??); whd in match (free_list ??);1418 normalize >foldr_identity @Hext1419  2: #hd #tl #Hind >free_list_cons >free_list_cons1420 lapply (free_memory_ext … hd … Hind)1421 cut ((lset_remove block_eq (filter block_eq (λwb:block_eq.¬wb∈tl) writeable) hd) =1422 (filter block_eq (λwb:block_eq.¬wb∈hd::tl) writeable))1423 [ whd in match (lset_remove ???); elim writeable //1424 #hd' #tl' #Hind_cut >filter_cons_unfold >filter_cons_unfold1425 whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block1426 (* elim (eqb_true block_DeqSet hd' hd)*)1427 @(eq_block_elim … hd' hd) normalize nodelta1428 [ 1: #Heq1429 cases (¬hd'∈tl) normalize nodelta1430 [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?);1431 normalize nodelta1432 lapply Hind_cut destruct #H @H1433  2: lapply Hind_cut destruct #H @H ]1434  2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption1435 whd in match (foldr ?????); >eqb_to_eq_block1436 >(neq_block_eq_block_false … Hneq)1437 normalize in match (notb ?); normalize nodelta >Hind_cut @refl1438 ]1439 ]1440 #Heq >Heq #H @H1441 ] qed.1442 1443 (* Remove a writeable block. *)1444 lemma memory_ext_weaken :1445 ∀m1,m2,hd,writeable.1446 sr_memext m1 m2 (hd :: writeable) →1447 sr_memext m1 m2 writeable.1448 #m1 #m2 #hd #writeable *1449 #Hnonempty #Hwriteable_valid #Hnot_writeable %1450 try assumption1451 [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption1452  2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem1453 ] qed.1454 1455 (* Perform a "rewrite" using lset_eq on the writeable blocks *)1456 lemma memory_ext_writeable_eq :1457 ∀m1,m2,wr1,wr2.1458 sr_memext m1 m2 wr1 →1459 lset_eq ? wr1 wr2 →1460 sr_memext m1 m2 wr2.1461 #m1 #m2 #wr1 #wr2 #Hext #Hset_eq %1462 [ 1: @(me_nonempty … Hext)1463  2: #b #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem)1464 @(me_writeable_valid … Hext)1465  3: #b #Hnonempty % #Hmem1466 lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'1467 lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption1468 ] qed.1469 1470 lemma lset_difference_empty :1471 ∀A : DeqSet.1472 ∀s1. lset_difference A s1 [ ] = s1.1473 #A #s1 elim s1 try //1474 #hd #tl #Hind >lset_difference_unfold >Hind @refl1475 qed.1476 1477 lemma lset_not_mem_difference :1478 ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3).1479 #A #s1 #s2 #s3 #Hincl #x #Hmem1480 lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s31481 elim s1 in Hincl Hmem;1482 [ 1: #_ *1483  2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall *1484 [ 2: #Hmem_x_tl @Hind assumption1485  1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ]1486 ] qed.1487 1488 lemma lset_mem_inclusion_mem :1489 ∀A,s1,s2,elt.1490 mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2.1491 #A #s1 elim s11492 [ 1: #s2 #elt *1493  2: #hd #tl #Hind #s2 #elt *1494 [ 1: #Heq destruct * //1495  2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl;1496 [ 1: #_ *1497  2: #hd' #tl' #Hind * #Hmem' #Hall *1498 [ 1: #Heq destruct @Hmem'1499  2: #Hmem'' @Hind assumption ] ] ] ]1500 qed.1501 1502 lemma lset_remove_inclusion :1503 ∀A : DeqSet. ∀s,elt.1504 lset_inclusion A (lset_remove ? s elt) s.1505 #A #s elim s try // qed.1506 1507 lemma lset_difference_remove_inclusion :1508 ∀A : DeqSet. ∀s1,s2,elt.1509 lset_inclusion A1510 (lset_difference ? (lset_remove ? s1 elt) s2)1511 (lset_difference ? s1 s2).1512 #A #s elim s try // qed.1513 1514 lemma lset_difference_permute :1515 ∀A : DeqSet. ∀s1,s2,s3.1516 lset_difference A s1 (s2 @ s3) =1517 lset_difference A s1 (s3 @ s2).1518 #A #s1 #s2 elim s2 try //1519 #hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute1520 >Hind elim s3 try //1521 #hd' #tl' #Hind' >cons_to_append >associative_append1522 >associative_append >(cons_to_append … hd tl)1523 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append1524 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append1525 <Hind' generalize in match (lset_difference ???); #foo1526 whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);1527 whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));1528 elim foo1529 [ 1: normalize @refl1530  2: #hd'' #tl'' #Hind normalize1531 @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with1532 [ true ⇒ λH. ?1533  false ⇒ λH. ?1534 ] (refl ? (hd''==hd')))1535 @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with1536 [ true ⇒ λH'. ?1537  false ⇒ λH'. ?1538 ] (refl ? (hd''==hd)))1539 normalize nodelta1540 try @Hind1541 [ 1: normalize >H normalize nodelta @Hind1542  2: normalize >H' normalize nodelta @Hind1543  3: normalize >H >H' normalize nodelta >Hind @refl1544 ] qed.1545 1546 1399 lemma mem_not_mem_diff_aux : 1547 1400 ∀s1,s2,s3,hd. … … 1586 1439 ] qed. 1587 1440 1588 lemma lset_disjoint_dec : 1589 ∀A : DeqSet. 1590 ∀s1,elt,s2. 1591 mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1). 1592 #A #s1 #elt #s2 1593 @(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ? 1594 with 1595 [ false ⇒ λHA. ? 1596  true ⇒ λHA. ? ] (refl ? (elt ∈ s1))) 1597 [ 1: lapply (memb_to_mem … HA) #Hmem 1598 %1 @Hmem 1599  2: %2 elim s1 in HA; 1600 [ 1: #_ whd %1 @refl 1601  2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?); 1602 >lset_difference_unfold 1603 >lset_difference_unfold2 1604 lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %); 1605 cases (elt==hd1) normalize nodelta 1606 [ 1: #_ #Habsurd destruct 1607  2: #HA #HB >HB normalize nodelta %1 @refl ] ] ] 1608 qed. 1609 1610 lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2. 1611 mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l. 1612 #A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/ 1613 qed. 1614 1615 lemma lset_inclusion_difference_aux : 1616 ∀A : DeqSet. ∀s1,s2. 1617 lset_inclusion A s1 s2 → 1618 (lset_eq A s2 (s1@lset_difference A s2 s1)). 1619 #A #s1 1620 @(WF_ind ????? (filtered_list_wf A s1)) 1621 * 1622 [ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq 1623  2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl 1624 lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?) 1625 [ 1: whd normalize 1626 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ] 1627 #Hind_wf 1628 elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq 1629 >cons_to_append in ⊢ (???%); >associative_append 1630 >lset_difference_unfold2 1631 >nil_append 1632 >lset_remove_split >lset_remove_split 1633 normalize in match (lset_remove ? [hd1] hd1); 1634 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1635 >nil_append <lset_remove_split >lset_difference_lset_remove_commute 1636 lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?) 1637 [ 1: lapply (lset_inclusion_remove … Hincl hd1) 1638 >Heq @lset_inclusion_eq2 1639 >lset_remove_split >lset_remove_split >lset_remove_split 1640 normalize in match (lset_remove ? [hd1] hd1); 1641 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1642 >nil_append @reflexive_lset_eq ] 1643 #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind 1644 @lset_eq_concrete_to_lset_eq 1645 lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc 1646 @(square_lset_eq_concrete ????? Hindc) Hindc Hind 1647 [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B)) 1648 [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete 1649  1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ] 1650  2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …)) 1651 elim (s2A@s2B) 1652 [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq 1653  2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold 1654 @(match (hd2∈filter A (λx:A.¬x==hd1) tl1) 1655 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ? 1656 with 1657 [ false ⇒ λH. ? 1658  true ⇒ λH. ? 1659 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta 1660 [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter)) 1661 normalize nodelta @Hind 1662  2: @(match (hd2∈tl1) 1663 return λx. ((hd2∈tl1) = x) → ? 1664 with 1665 [ false ⇒ λH'. ? 1666  true ⇒ λH'. ? 1667 ] (refl ? (hd2∈tl1))) normalize nodelta 1668 [ 1: (* We have hd2 = hd1 *) 1669 cut (hd2 = hd1) 1670 [ elim tl1 in H H'; 1671 [ 1: normalize #_ #Habsurd destruct (Habsurd) 1672  2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?); 1673 lapply (eqb_true ? hdtl1 hd1) 1674 cases (hdtl1==hd1) normalize nodelta 1675 [ 1: * #H >(H (refl ??)) #_ 1676 lapply (eqb_true ? hd2 hd1) 1677 cases (hd2==hd1) normalize nodelta * 1678 [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl 1679  2: #_ #_ @Hind ] 1680  2: #_ normalize lapply (eqb_true ? hd2 hdtl1) 1681 cases (hd2 == hdtl1) normalize nodelta * 1682 [ 1: #_ #_ #Habsurd destruct (Habsurd) 1683  2: #_ #_ @Hind ] ] ] ] 1684 #Heq_hd2hd1 destruct (Heq_hd2hd1) 1685 @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind) 1686 #Hind' @(square_lset_eq_concrete … Hind') 1687 [ 2: @lset_refl 1688  1: >cons_to_append >cons_to_append in ⊢ (???%); 1689 @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 1690 [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract 1691  2: >(cons_to_append … hd1 (lset_difference ???)) 1692 @lset_eq_concrete_cons >nil_append >nil_append 1693 @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ] 1694  2: @(match hd2 == hd1 1695 return λx. ((hd2 == hd1) = x) → ? 1696 with 1697 [ true ⇒ λH''. ? 1698  false ⇒ λH''. ? 1699 ] (refl ? (hd2 == hd1))) 1700 [ 1: whd in match (lset_remove ???) in ⊢ (???%); 1701 >H'' normalize nodelta >((proj1 … (eqb_true …)) H'') 1702 @(transitive_lset_eq … Hind) 1703 @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 1704 [ 2: @lset_eq_contract ] 1705 @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons 1706 @switch_lset_eq_concrete 1707  2: whd in match (lset_remove ???) in ⊢ (???%); 1708 >H'' >notb_false normalize nodelta 1709 @lset_eq_concrete_to_lset_eq 1710 lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc 1711 lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' Hindc 1712 @(square_lset_eq_concrete … Hindc') 1713 [ 1: @symmetric_lset_eq_concrete 1714 >cons_to_append >cons_to_append in ⊢ (???%); 1715 >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%); 1716 @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 1717  2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 1718 ] 1719 ] 1720 ] 1721 ] 1722 ] 1723 ] 1724 ] qed. 1725 1726 lemma lset_inclusion_difference : 1727 ∀A : DeqSet. 1728 ∀s1,s2 : lset (carr A). 1729 lset_inclusion ? s1 s2 → 1730 ∃s2'. lset_eq ? s2 (s1 @ s2') ∧ 1731 lset_disjoint ? s1 s2' ∧ 1732 lset_eq ? s2' (lset_difference ? s2 s1). 1733 #A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj 1734 [ 1: @lset_inclusion_difference_aux @Hincl 1735  2: /2 by lset_difference_disjoint/ 1736  3,4: @reflexive_lset_inclusion ] 1737 qed. 1738 1739 1441 (* freeing equivalent sets of blocks on memory extensions yields memory extensions *) 1442 lemma free_equivalent_sets : 1443 ∀m1,m2,writeable,set1,set2. 1444 lset_eq ? set1 set2 → 1445 sr_memext m1 m2 writeable → 1446 sr_memext (free_list m1 set1) (free_list m2 set2) (lset_difference ? writeable set1). 1447 #m1 #m2 #writeable #set1 #set2 #Heq #Hext 1448 lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq)) 1449 #Heq 1450 lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext' 1451 lapply (memory_ext_transitive (free_list m1 set1) (free_list m2 set1) (free_list m2 set2) (filter block_eq (λwb:block_eq.¬wb∈set1) writeable) [ ] ? Hext') 1452 [ 2: >append_nil #H @H ] 1453 elim set1 1454 [ 1: whd in match (free_list ??); whd in match (free_list ??); 1455 normalize >foldr_identity @Hext 1456  2: #hd #tl #Hind >free_list_cons >free_list_cons 1457 lapply (free_memory_ext … hd … Hind) 1458 cut ((lset_remove block_eq (filter block_eq (λwb:block_eq.¬wb∈tl) writeable) hd) = 1459 (filter block_eq (λwb:block_eq.¬wb∈hd::tl) writeable)) 1460 [ whd in match (lset_remove ???); elim writeable // 1461 #hd' #tl' #Hind_cut >filter_cons_unfold >filter_cons_unfold 1462 whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block 1463 (* elim (eqb_true block_DeqSet hd' hd)*) 1464 @(eq_block_elim … hd' hd) normalize nodelta 1465 [ 1: #Heq 1466 cases (¬hd'∈tl) normalize nodelta 1467 [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?); 1468 normalize nodelta 1469 lapply Hind_cut destruct #H @H 1470  2: lapply Hind_cut destruct #H @H ] 1471  2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption 1472 whd in match (foldr ?????); >eqb_to_eq_block 1473 >(neq_block_eq_block_false … Hneq) 1474 normalize in match (notb ?); normalize nodelta >Hind_cut @refl 1475 ] 1476 ] 1477 #Heq >Heq #H @H 1478 ] qed. 1479 1480 (* Remove a writeable block. *) 1481 lemma memory_ext_weaken : 1482 ∀m1,m2,hd,writeable. 1483 sr_memext m1 m2 (hd :: writeable) → 1484 sr_memext m1 m2 writeable. 1485 #m1 #m2 #hd #writeable * 1486 #Hnonempty #Hwriteable_valid #Hnot_writeable % 1487 try assumption 1488 [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption 1489  2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem 1490 ] qed. 1491 1492 (* Perform a "rewrite" using lset_eq on the writeable blocks *) 1493 lemma memory_ext_writeable_eq : 1494 ∀m1,m2,wr1,wr2. 1495 sr_memext m1 m2 wr1 → 1496 lset_eq ? wr1 wr2 → 1497 sr_memext m1 m2 wr2. 1498 #m1 #m2 #wr1 #wr2 #Hext #Hset_eq % 1499 [ 1: @(me_nonempty … Hext) 1500  2: #b #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) 1501 @(me_writeable_valid … Hext) 1502  3: #b #Hnonempty % #Hmem 1503 lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' 1504 lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption 1505 ] qed. 1506 1507 1508 1740 1509 lemma memory_eq_to_memory_ext_pre : 1741 1510 ∀m1,m1',m2,writeable. … … 2061 1830 @memext_store_value_of_type @Hext qed. 2062 1831 1832 lemma memext_store_value_of_type_writeable : 1833 ∀m1,m2,writeable. 1834 ∀Hext:sr_memext m1 m2 writeable. 1835 ∀wb. meml ? wb writeable → 1836 ∀ty,off,v,m2'. store_value_of_type ty m2 wb off v = Some ? m2' → 1837 sr_memext m1 m2' writeable. 1838 #m1 #m2 #writeable #Hext #wb #Hmem 1839 #ty #off #v #m2' 1840 cases ty 1841 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 1842  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] 1843 whd in ⊢ ((??%?) → ?); 1844 [ 1,5,6,7,8: #Habsurd destruct ] 1845 lapply Hext lapply m1 lapply m2 lapply m2' lapply off Hext m1 m2 m2' off ty 1846 elim (fe_to_be_values ??) 1847 [ 1,3,5,7: #o #m2' #m2 #m1 #Hext normalize #Heq destruct assumption 1848  *: #hd #tl #Hind #o #m2_end #m2 #m1 #Hext whd in match (storen ???); #Hbestorev 1849 cases (some_inversion ????? Hbestorev) #m2' * #Hbestorev #Hstoren 1850 lapply (bestorev_writeable_memory_ext … Hext … o hd Hmem … Hbestorev) #Hext' 1851 @(Hind … Hstoren) // 1852 ] qed. 1853 2063 1854 (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if 2064 1855 * the variable is not in a local environment, then we search into the global one. … … 2188 1979 (* The new variables are allocated to a size corresponding to their types. *) 2189 1980 ∀sss_new_alloc : 2190 ∀v.meml ? v sss_new_vars →1981 (∀v.meml ? v sss_new_vars → 2191 1982 ∀vb. lookup … sss_env_ext (\fst v) = Some ? vb → 1983 valid_block sss_m_ext vb ∧ 2192 1984 low (blocks sss_m_ext vb) = OZ ∧ 2193 high (blocks sss_m_ext vb) = sizeof (\snd v). 1985 high (blocks sss_m_ext vb) = sizeof (\snd v)). 1986 (* Exit label for the enclosing switch, if any. Use for [break] conversion in switches. *) 1987 ∀sss_enclosing_label : option label. 2194 1988 (* Extension blocks are writeable. *) 2195 1989 ∀sss_ext_write : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable. … … 2270 2064 #ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq} 2271 2065 try assumption 2272 qed. 2066 qed. 2273 2067 2274 2068 lemma exec_lvalue_expr_elim : … … 2613 2407 ] qed. 2614 2408 2615 (*2616 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.2617 related_globals ? fundef_switch_removal ge ge' →2618 ∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).2619 #ge #ge' #en #m #Hrelated #args2620 elim args2621 [ 1: /3/2622  2: #hd #tl #Hind normalize2623 elim (sim_related_globals ge ge' en m Hrelated)2624 #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)2625 cases (exec_expr ge en m hd)2626 [ 2: #error #_ @SimFail /2 by refl, ex_intro/2627  1: * #val_hd #trace_hd normalize nodelta2628 cases Hind2629 [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/2630  1: cases (exec_exprlist ge en m tl)2631 [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/2632  1: * #values #trace #H >(H 〈values, trace〉 (refl ??))2633 normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H22634 cases Hexec_hd2635 [ 2: * #error #Habsurd destruct (Habsurd)2636  1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]2637 ] ] ] ] qed.2638 *)2639 2640 2409 (* The return type of any function is invariant under switch removal *) 2641 2410 lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f. … … 2650 2419 normalize nodelta #u @refl 2651 2420 qed. 2652 2653 (*2654 lemma expr_fresh_lift :2655 ∀e,u,id.2656 fresh_for_expression e u →2657 fresh_for_univ SymbolTag id u →2658 fresh_for_univ SymbolTag (max_of_expr e id) u.2659 #e #u #id2660 normalize in match (fresh_for_expression e u);2661 #H1 #H22662 >max_of_expr_rewrite2663 normalize in match (fresh_for_univ ???);2664 cases (max_of_expr e ?) in H1; #p #H12665 cases id in H2; #p' #H22666 normalize nodelta2667 cases (leb p p') normalize nodelta2668 [ 1: @H2  2: @H1 ]2669 qed. *)2670 2421 2671 2422 lemma while_fresh_lift : ∀e,s,u. … … 2834 2585 #e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed. 2835 2586 2836 (*  2837 What follows is some rather generic stuff on proving that reading where we 2838 just wrote yields what we expect. We have to prove everything at the backend 2839 level, and then lift this to the frontend. This entails having to reason on 2840 invariants bearing on "intervals" of memories, and a lot of annoying stuff 2841 to go back and forth nats, Zs and bitvectors ... *) 2842 2843 2844 2845 2846 (* This axiom looks reasonable to me. But I slept 3 hours last night. *) 2847 axiom bv_incr_to_Z : ∀sz.∀bv:BitVector sz. 2848 Z_of_unsigned_bitvector ? (increment ? bv) = OZ ∨ 2849 Z_of_unsigned_bitvector ? (increment ? bv) = (Zsucc (Z_of_unsigned_bitvector ? bv)). 2850 2851 (* Note the possibility of overflow of bv. But it should be allright in the big picture. *) 2852 lemma offset_succ_to_Z_succ : 2853 ∀bv : BitVector 16. ∀x. Z_of_unsigned_bitvector ? bv < x → Z_of_unsigned_bitvector ? (increment ? bv) ≤ x. 2854 #bv #x 2855 cases (bv_incr_to_Z ? bv) 2856 [ 1: #Heq >Heq lapply (Z_of_unsigned_not_neg bv) * 2857 [ 1: #Heq >Heq elim x // 2858  2: * #p #H >H elim x // ] 2859  2: #H >H elim x 2860 elim (Z_of_unsigned_bitvector 16 bv) try /2/ 2861 ] qed. 2862 2863 (* 2864 lemma Z_not_le_shifted : ∀ofs. 2865 (Z_of_unsigned_bitvector 16 (offv (shift_offset 2 ofs (bitvector_of_nat 2 1))) ≤ Z_of_unsigned_bitvector 16 (offv ofs)) → False. 2866 * #vec *) 2867 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 (* 2882 lemma load_int_value_inversion : 2883 ∀t,m,p,sz,i. load_value_of_type' t m p = Some ? (Vint sz i) → ∃sg. t = Tint sz sg. 2884 #t #m * #b #o #sz #i whd in match (load_value_of_type' ???); 2885 cases t 2886 [ 2: #tsz #tsg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 2887  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] normalize nodelta 2888 whd in match (load_value_of_type ????); 2889 [ 4,5,6,7,9: #Habsurd destruct ] 2890 whd in match (be_to_fe_value ??); 2891 cases (loadn ???) normalize nodelta 2892 [ 1,3,5,7: #Habsurd destruct ] 2893 * 2894 [ 1,3,5,7: #Heq normalize in Heq; destruct ] 2895 #hd #tl 2896 [ 2,3,4: cases hd 2897 [ 1,2,7,8,13,14: whd in match (be_to_fe_value ??); #Heq destruct 2898  4,5,10,11,16,17: #HA #Heq destruct (Heq) cases (eqb ??∧?) in e0; 2899 normalize nodelta #Heq' destruct 2900  6,12,18: #ptr #part #Heq destruct cases (pointer_of_bevals ?) in e0; 2901 #foo normalize #Habsurd destruct 2902  *: #op1 #op2 #part #Heq destruct ] 2903  1: #H destruct cases hd in e0; normalize nodelta 2904 [ 1,2: #Heq destruct 2905  3: #op1 #op2 #part #Habsurd destruct 2906  4: #by whd in match (build_integer_val ??); 2907 cases (build_integer ??) normalize nodelta 2908 [ 1: #Heq destruct 2909  2: #bv #Heq destruct /2 by ex_intro/ ] 2910  5: #p cases (eqb ?? ∧ ?) normalize nodelta #Heq destruct 2911  6: #ptr #part cases (pointer_of_bevals ?) #foo normalize nodelta #Heq destruct ] 2912 ] qed. 2913 2914 lemma opt_to_res_load_int_value_inversion : 2915 ∀t,m,p,sz,i. 2916 (opt_to_res val (msg FailedLoad) (load_value_of_type' t m p) = OK ? (Vint sz i)) 2917 → ∃sg. t = Tint sz sg. 2918 #t #m #p #sz #i whd in match (opt_to_res ???); 2919 lapply (load_int_value_inversion t m p sz i) 2920 cases (load_value_of_type' t m p) 2921 [ 1: #H normalize nodelta #Habsurd destruct 2922  2: #v #H normalize nodelta #Heq destruct lapply (H (refl ??)) * 2923 #sg #Heq >Heq /2 by ex_intro/ 2924 ] qed. 2925 2926 lemma res_inversion : ∀A,B:Type[0]. ∀e:res A. ∀f:A → res B. ∀res:B. 2927 match e with 2928 [ OK x ⇒ f x 2929  Error msg ⇒ Error ? msg ] = OK ? res → 2930 ∃res_e. e = OK ? res_e ∧ OK ? res = f res_e. 2931 #A #B * 2932 [ 2: #err #f #res normalize nodelta #Habsurd destruct 2933  1: #a #f #res normalize nodelta #Heq destruct %{a} @conj try @refl >Heq @refl 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 2947 2948 (* In order to prove the consistency of types wrt values, we need the following lemma. *) 2949 (* 2950 lemma exec_expr_Vint_type_inversion : 2951 ∀ge,env,m,e,sz,i,tr. (exec_expr ge env m e=return 〈Vint sz i,tr〉) → 2952 ∃sg. typeof e = Tint sz sg. 2953 #ge #env #m * #ed #ty 2954 @(expr_ind2 … (λed,ty.∀sz:intsize.∀i:bvint sz.∀tr:trace. 2955 exec_expr ge env m (Expr ed ty)=return 〈Vint sz i,tr〉 → 2956 ∃sg:signedness.typeof (Expr ed ty)=Tint sz sg) … (Expr ed ty)) 2957 [ 1: #e' #ty' #H @H 2958  2: #sz #i #t #sz0 #i0 #tr whd in ⊢ ((??%?) → ?); cases t 2959 [ 2: #tsz #tsg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 2960  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] normalize nodelta 2961 [ 1: @(eq_intsize_elim … sz tsz) normalize nodelta 2962 [ 2: #Hsz_eq destruct (Hsz_eq) normalize #Heq destruct (Heq) 2963 %{tsg} @refl 2964  1: #_ normalize #Habsurd destruct (Habsurd) ] 2965  *: #Habsurd normalize in Habsurd; destruct ] 2966  3: #f #t #sz #i #tr whd in ⊢ ((??%?) → ?); #H normalize in H; destruct (H) 2967  4: #id #t #sz #i #tr whd in ⊢ ((??%?) → ?); 2968 @(match exec_lvalue' ge env m (Evar id) t 2969 return λr. r = exec_lvalue' ge env m (Evar id) t → ? 2970 with 2971 [ OK x ⇒ λHeq. ? 2972  Error msg ⇒ λHeq. ? 2973 ] (refl ? (exec_lvalue' ge env m (Evar id) t))) normalize nodelta 2974 [ 2: normalize #Habsurd destruct ] #Hload 2975 cases (bind_inversion ????? Hload) #loadval * #Heq_loadval #Heq_res 2976 normalize in Heq_res; destruct (Heq_res) 2977 Hload 2978 whd in Heq_loadval:(??%%); lapply Heq_loadval 2979 @(match load_value_of_type' t m (\fst x) 2980 return λr. r = load_value_of_type' t m (\fst x) → ? 2981 with 2982 [ None ⇒ λHeq. ? 2983  Some v' ⇒ λHeq. ? 2984 ] (refl ? (load_value_of_type' t m (\fst x)))) normalize nodelta 2985 [ 1: #Habsurd destruct ] 2986 #Heq_v' destruct (Heq_v') 2987 cases (load_int_value_inversion … (sym_eq ??? Heq)) #sg #Htyp_eq 2988 >Htyp_eq %{sg} @refl 2989  5: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); 2990 whd in match (exec_lvalue' ?????); 2991 @(match exec_expr ge env m e 2992 return λx. x = (exec_expr ge env m e) → ? 2993 with 2994 [ OK res ⇒ λH. ? 2995  Error msg ⇒ λH. ? ] (refl ? (exec_expr ge env m e))) 2996 normalize nodelta 2997 [ 2: #Habsurd destruct ] 2998 cases res in H; #vres #trres #Hexec #H 2999 cases (res_inversion ????? H) H * * #b' #o' #tr' * 3000 cases vres in Hexec; normalize nodelta 3001 [ 1: #_ #Habsurd destruct 3002  2: #sz' #i' #_ #Habsurd destruct 3003  3: #f #_ #Habsurd destruct 3004  4: #_ #Habsurd destruct ] 3005 #p #Heq_exec_expr #Heq destruct (Heq) #Heq 3006 lapply (sym_eq ??? Heq) Heq #Heq 3007 cases (bind_inversion ????? Heq) Heq #x * #Hload_value 3008 #Heq normalize in Heq; destruct (Heq) 3009 @(opt_to_res_load_int_value_inversion … Hload_value) 3010  6: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H 3011 cases (res_inversion ????? H) * * #b #o #tr * #Hexec_lvalue 3012 cases t 3013 [ 2: #tsz #tsg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 3014  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] normalize nodelta 3015 #Habsurd destruct 3016  7: #op #arg #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H 3017 cases (res_inversion ????? H) * #v #tr * #Hexec_expr 3018 #H' lapply (sym_eq ??? H') H' #H' 3019 cases (bind_inversion ????? H') #v' * #Hopt_sem #Hvalues 3020 normalize in Hvalues:(??%%); destruct (Hvalues) H' H 3021 3022 lapp 3023 >Hopt_sem in H'; 3024 destruct (Hvalues) 3025 3026 whd in match (exec_lvalue ????);*) 3027 3028 2587 lemma store_int_success : 2588 ∀b,m,sz,sg,i. valid_block m b → low (blocks m b) = OZ → high (blocks m b) = sizeof (Tint sz sg) → 2589 ∃m'. store_value_of_type (Tint sz sg) m b zero_offset (Vint sz i) = Some ? m'. 2590 #b #m #sz #sg 2591 cases sz 2592 [ 1: #i #Hvalid #Hlow #Hhigh 2593 whd in match (store_value_of_type ?????); 2594 whd in match (fe_to_be_values ??); 2595 normalize nodelta 2596 normalize in match (size_intsize ?); 2597 whd in match (bytes_of_bitvector ??); 2598 lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i 2599 <(vsplit_prod … Heq_i) normalize nodelta 2600 >(BitVector_O … ri) whd in match (storen ???); 2601 lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) 2602 [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true 2603 >unfold_low_bound >unfold_high_bound >Hlow >Hhigh 2604 >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta 2605 @Zlt_to_Zltb_true // ] 2606 * #m' #Hbestorev >Hbestorev %{m'} @refl 2607  2: #i #Hvalid #Hlow #Hhigh 2608 whd in match (store_value_of_type ?????); 2609 whd in match (fe_to_be_values ??); 2610 normalize nodelta 2611 normalize in match (size_intsize ?); 2612 whd in match (bytes_of_bitvector ??); 2613 lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i 2614 <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); 2615 lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) 2616 [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true 2617 >unfold_low_bound >unfold_high_bound >Hlow >Hhigh 2618 >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta 2619 @Zlt_to_Zltb_true // ] 2620 * #m0 #Hbestorev >Hbestorev normalize nodelta 2621 whd in match (bytes_of_bitvector ??); 2622 lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri 2623 <(vsplit_prod … Heq_ri) normalize nodelta 2624 cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ 2625 lapply (valid_pointer_to_bestorev_ok m0 2626 (mk_pointer b (mk_offset 2627 [[false; false; false; false; false; false; false; false; 2628 false; false; false; false; false; false; false; true]])) 2629 (BVByte rli) ?) 2630 [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true 2631 cases (Hblocks0 b) #HA #HB 2632 >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta 2633 @Zlt_to_Zltb_true normalize // ] 2634 * #m1 #Hbestorev1 %{m1} whd in ⊢ (??(???%)?); whd in match (storen ???); 2635 normalize in match (shift_pointer ???); >Hbestorev1 normalize nodelta 2636 @refl 2637  3: #i #Hvalid #Hlow #Hhigh 2638 whd in match (store_value_of_type ?????); 2639 whd in match (fe_to_be_values ??); 2640 normalize nodelta 2641 normalize in match (size_intsize ?); 2642 whd in match (bytes_of_bitvector ??); 2643 lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i 2644 <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); 2645 lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte iA) ?) 2646 [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true 2647 >unfold_low_bound >unfold_high_bound >Hlow >Hhigh 2648 >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta 2649 @Zlt_to_Zltb_true // ] 2650 * #m0 #Hbestorev >Hbestorev normalize nodelta 2651 whd in match (bytes_of_bitvector ??); 2652 lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB 2653 <(vsplit_prod … Heq_iB) normalize nodelta 2654 cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ 2655 lapply (valid_pointer_to_bestorev_ok m0 2656 (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)) 2657 (BVByte iC) ?) 2658 [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true 2659 cases (Hblocks0 b) #HA #HB 2660 >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta 2661 @Zlt_to_Zltb_true normalize // ] 2662 * #m1 #Hbestorev1 whd in ⊢ (??(λ_.??(???%)?)); whd in match (storen ???); 2663 normalize in match (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)); 2664 >Hbestorev1 normalize nodelta 2665 lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD 2666 whd in match (bytes_of_bitvector ??); 2667 <(vsplit_prod … Heq_iD) normalize nodelta 2668 whd in ⊢ (??(λ_.??(???%)?)); 2669 whd in match (storen ???); 2670 cases (mem_bounds_invariant_after_bestorev … Hbestorev1) * * * #Hnext1 #Hblocks1 #_ #_ #_ 2671 lapply (valid_pointer_to_bestorev_ok m1 2672 (shift_pointer 2 (mk_pointer b (mk_offset 2673 [[ false; false; false; false; false; false; false; false; false; false; 2674 false; false; false; false; false; true ]])) 2675 (bitvector_of_nat 2 1)) 2676 (BVByte iE) ?) 2677 [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); 2678 >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) 2679 >andb_lsimpl_true cases (Hblocks1 b) #HA #HB cases (Hblocks0 b) #HC #HD 2680 >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >Hlow >Hhigh normalize nodelta 2681 @Zlt_to_Zltb_true normalize // ] 2682 * #m2 #Hbestorev2 >Hbestorev2 normalize nodelta 2683 whd in match (bytes_of_bitvector ??); 2684 lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF 2685 <(vsplit_prod … Heq_iF) normalize nodelta 2686 >(BitVector_O … iH) whd in ⊢ (??(λ_.??(???%)?)); 2687 whd in match (storen ???); 2688 cases (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * #Hnext2 #Hblocks2 #_ #_ #_ 2689 lapply (valid_pointer_to_bestorev_ok m2 2690 (shift_pointer 2 (shift_pointer 2 (mk_pointer b (mk_offset 2691 [[ false; false; false; false; false; false; false; false; false; false; 2692 false; false; false; false; false; true ]])) 2693 (bitvector_of_nat 2 1)) (bitvector_of_nat 2 1)) 2694 (BVByte iG) ?) 2695 [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); 2696 >Hnext2 >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) 2697 >andb_lsimpl_true cases (Hblocks2 b) #HA #HB cases (Hblocks1 b) #HC #HD cases (Hblocks0 b) #HE #HF 2698 >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >HE >HF >Hlow >Hhigh normalize nodelta 2699 @Zlt_to_Zltb_true normalize // ] 2700 * #m3 #Hbestorev3 >Hbestorev3 normalize nodelta %{m3} @refl 2701 ] qed. 3029 2702 3030 2703 … … 3043 2716 #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars 3044 2717 #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp 3045 #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 2718 #sss_env_hyp #sss_new_alloc #sss_enclosing_label #sss_writeable_hyp #sss_result_rec #sss_result_hyp 2719 #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge 3046 2720 #Hs1_eq #Hs1_eq' 3047 2721 elim (sim_related_globals … ge ge' … … 3160 2834 #Hexec %{0} whd in sss_result_hyp:(??%?); 3161 2835 cases (bindIO_inversion ??????? Hexec) #xl * #Heq_lhs #Hexec_lhs 3162 cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs 3163 cases (bindIO_inversion ??????? Hexec_rhs) # xs * #Heq_store #Hexec_store2836 cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs Hexec_lhs 2837 cases (bindIO_inversion ??????? Hexec_rhs) #m' * #Heq_store #Hexec_store Hexec_rhs 3164 2838 whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj <sss_result_hyp normalize nodelta 3165 2839 >(Hsim … Heq_lhs) whd in match (m_bind ?????); 3166 2840 >(Hsim_expr … Heq_rhs) >bindIO_Value 3167 lapply (memext_store_value_of_type' sss_m sss_m_ext xssss_writeable (typeof lhs) (\fst xl) (\fst xr) sss_mem_hyp ?)2841 lapply (memext_store_value_of_type' sss_m sss_m_ext m' sss_writeable (typeof lhs) (\fst xl) (\fst xr) sss_mem_hyp ?) 3168 2842 [ 1: cases (store_value_of_type' ????) in Heq_store; 3169 2843 [ 1: normalize #Habsurd destruct (Habsurd) 3170 2844  2: #m normalize #Heq destruct (Heq) @refl ] ] 3171 * #m_ext' * #H store_eq #Hnew_ext >Hstore_eqwhd in match (m_bind ?????);2845 * #m_ext' * #Heq_store' #Hnew_ext >Heq_store' whd in match (m_bind ?????); 3172 2846 whd destruct @conj try @refl 3173 2847 %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip sss_lu) } … … 3175 2849 [ 1: @(fresh_for_Sskip … sss_lu_fresh) 3176 2850  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 ] 2851  2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * * #Hvb #Hlow #Hhigh 2852 cut (store_value_of_type' (typeof lhs) sss_m (\fst xl) (\fst xr) = Some ? m') 2853 [ cases (store_value_of_type' (typeof lhs) sss_m (\fst xl) (\fst xr)) in Heq_store; 2854 [ whd in ⊢ ((??%%) → ?); #Habsurd destruct 2855  #m0 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl ] ] 2856 #Hstore lapply (mem_bounds_after_store_value_of_type' … Heq_store') * 2857 #HA #HB cases (HB vb) #Hlow' #Hhigh' @conj try @conj 2858 [ 2: >Hlow' in Hlow; // 2859  3: >Hhigh' in Hhigh; // 2860  1: whd >HA @Hvb ] ] 3182 2861  3: (* Call statement *) 3183 2862 #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp) … … 3365 3044 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 3366 3045  9: (* break *) 3046 (* sss_enclosing_label TODO : switch case *) 3367 3047 #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta 3368 3048 lapply Hexec Hexec … … 3504 3184 cases (simplify_switch_elim (Expr (Evar new) (Tint sz sg)) switchcases' u'') #simplified * #u''' 3505 3185 #Hswitch_eq >Hswitch_eq normalize nodelta 3506 %{ 1} whd whd in ⊢ (??%?);3186 %{2} whd whd in ⊢ (??%?); 3507 3187 (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *) 3508 3188 whd in match (exec_lvalue ????); … … 3516 3196 #Hlookup_new_in_new 3517 3197 #Hlookup_old 3518 lapply (Hlookup_new_in_new new ?)3198 cut (mem_assoc_env new sss_new_vars=true) 3519 3199 [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem; 3520 3200 [ 1: @False_ind … … 3526 3206 cases (identifier_eq ? new hdv) normalize nodelta 3527 3207 [ 1: #_ @refl  2: #_ @Hmem_in_tl ] ] ] ] 3208 #Hnew_in_new_vars 3209 lapply (Hlookup_new_in_new new Hnew_in_new_vars) 3528 3210 * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????); 3529 3211 (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *) … … 3533 3215 normalize in match store_value_of_type'; normalize nodelta 3534 3216 whd in match (typeof ?); 3535 3217 lapply (sss_new_alloc 〈new,Tint sz sg〉 ? res Hlookup) 3218 [ 1: cases sss_incl // ] * * #Hvalid #Hlow #Hhigh 3219 lapply (store_int_success … i … Hvalid Hlow Hhigh) * #m_ext' #Hstore 3220 lapply (store_value_load_value_ok … Hstore) // #Hload_value_correct 3221 >Hstore whd in match (m_bind ?????); whd @conj try // 3222 cut (mem block res sss_writeable) 3223 [ 1: @cthulhu ] 3224 (* lapply (memext_store_value_of_type_writeable … sss_mem_hyp … Hstore) *) 3536 3225 @cthulhu 3537 3226  *: @cthulhu ]
Note: See TracChangeset
for help on using the changeset viewer.