Changeset 2448


Ignore:
Timestamp:
Nov 9, 2012, 4:38:02 PM (7 years ago)
Author:
garnier
Message:

Comitting current state of switch removal.

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/MemProperties.ma

    r2441 r2448  
    44include "Clight/frontend_misc.ma".
    55include "common/FrontEndMem.ma".
     6
     7(* for store_value_of_type' *)
     8include "Clight/Cexec.ma".
     9
    610
    711(* --------------------------------------------------------------------------- *)
     
    5761qed.
    5862
     63lemma valid_pointer_of_Prop :
     64  ∀m,p. (block_id (pblock p)) < (nextblock m) ∧
     65        (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧
     66        (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)) →
     67        valid_pointer m p = true.
     68#m #p * * #Hnextblock #Hlowbound #Hhighbound whd in match (valid_pointer ??);
     69>(Zle_to_Zleb_true … Hlowbound)
     70>(Zlt_to_Zltb_true … Hhighbound)
     71>(Zlt_to_Zltb_true … Hnextblock) @refl
     72qed.
     73
    5974(* --------------------------------------------------------------------------- *)
    6075(* "Observational" memory equivalence. Memories use closures to represent contents,
     
    187202qed.
    188203
     204(* valid pointer implies successful bestorev *)
    189205lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'.
    190206#m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) *
     
    332348(* --------------------------------------------------------------------------- *)
    333349(* 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)                                  *)
    335351(* --------------------------------------------------------------------------- *)
    336352
     
    757773
    758774
     775lemma 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
     782lapply (fe_to_be_values_bounded (typ_of_type ty) v)
     783cases 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 ]
     786whd in match (typ_of_type ?); #Hbounded
     787whd 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
     795lemma 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
     803qed.
     804
     805
    759806definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v.
    760807  match ty with
     
    779826| _ ⇒ True
    780827].
    781 
    782828
    783829(* We also need the following property. It is not provable unless [v] and [ty] are consistent. *)
  • src/Clight/frontend_misc.ma

    r2441 r2448  
    12901290          @lset_eq_concrete_cons >nil_append >nil_append
    12911291          @Hind
    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     ]
     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     ]
    12991299] qed.
    13001300
     
    14171417qed.
    14181418
    1419 
    1420 
     1419(* Additional lemmas on lsets *)
     1420
     1421lemma 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
     1426qed.
     1427
     1428lemma 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
     1431lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
     1432elim 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
     1439lemma 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 ] ] ] ]
     1451qed.
     1452
     1453lemma 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
     1458lemma 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
     1465lemma 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
     1477whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);
     1478whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));
     1479elim 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
     1499lemma 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 ] ] ]
     1519qed.
     1520
     1521lemma 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/
     1524qed.
     1525
     1526lemma 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                                                       
     1637lemma 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 ]
     1648qed.
  • src/Clight/memoryInjections.ma

    r2438 r2448  
    777777     | 2: % #Hmem @Hguard %2 @Hmem ]
    778778] qed. *)
     779
    779780
    780781lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr.
  • src/Clight/switchRemoval.ma

    r2441 r2448  
    1010include "basics/lists/list.ma".
    1111include "basics/lists/listb.ma".
    12 
    13 
    14 
    1512
    1613(* -----------------------------------------------------------------------------
     
    779776].
    780777
    781 
    782 
    783778(* --------------------------------------------------------------------------- *)
    784779(* Memory extensions (limited form on memoryInjection.ma). Note that we state the
     
    792787record nonempty_block (m : mem) (b : block) : Prop ≝
    793788{
    794   wb_valid      : valid_block m b;
    795   wb_nonempty   : low (blocks m b) < high (blocks m b)
     789  wb_valid    : valid_block m b;
     790  wb_nonempty : low (blocks m b) < high (blocks m b)
    796791}.
    797792
     
    14021397qed.
    14031398
    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 #Hext
    1411 lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq))
    1412 #Heq
    1413 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 set1
    1417 [ 1: whd in match (free_list ??); whd in match (free_list ??);
    1418      normalize >foldr_identity @Hext
    1419 | 2: #hd #tl #Hind >free_list_cons >free_list_cons
    1420      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_unfold
    1425         whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block
    1426         (* elim (eqb_true block_DeqSet hd' hd)*)
    1427         @(eq_block_elim … hd' hd) normalize nodelta
    1428         [ 1: #Heq
    1429              cases (¬hd'∈tl) normalize nodelta
    1430              [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?);
    1431                   normalize nodelta
    1432                   lapply Hind_cut destruct #H @H
    1433              | 2: lapply Hind_cut destruct #H @H ]
    1434         | 2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption
    1435              whd in match (foldr ?????); >eqb_to_eq_block
    1436              >(neq_block_eq_block_false … Hneq)
    1437              normalize in match (notb ?); normalize nodelta >Hind_cut @refl
    1438         ]
    1439     ]
    1440     #Heq >Heq #H @H
    1441 ] 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 assumption
    1451 [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption
    1452 | 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem
    1453 ] 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 % #Hmem
    1466      lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'
    1467      lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption
    1468 ] 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 @refl
    1475 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 #Hmem
    1480 lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
    1481 elim s1 in Hincl Hmem;
    1482 [ 1: #_ *
    1483 | 2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall *
    1484      [ 2: #Hmem_x_tl @Hind assumption
    1485      | 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 s1
    1492 [ 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 A
    1510       (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_commute
    1520 >Hind elim s3 try //
    1521 #hd' #tl' #Hind' >cons_to_append >associative_append
    1522 >associative_append >(cons_to_append … hd tl)
    1523 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
    1524 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
    1525 <Hind' generalize in match (lset_difference ???); #foo
    1526 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 foo
    1529 [ 1: normalize @refl
    1530 | 2: #hd'' #tl'' #Hind normalize
    1531       @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with
    1532         [ true ⇒ λH. ?
    1533         | false ⇒ λH. ?
    1534         ] (refl ? (hd''==hd')))
    1535       @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with
    1536         [ true ⇒ λH'. ?
    1537         | false ⇒ λH'. ?
    1538         ] (refl ? (hd''==hd)))
    1539       normalize nodelta
    1540       try @Hind
    1541 [ 1: normalize >H normalize nodelta @Hind
    1542 | 2: normalize >H' normalize nodelta @Hind
    1543 | 3: normalize >H >H' normalize nodelta >Hind @refl
    1544 ] qed.
    1545 
    15461399lemma mem_not_mem_diff_aux :
    15471400  ∀s1,s2,s3,hd.
     
    15861439] qed.
    15871440
    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 *)
     1442lemma 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
     1448lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq))
     1449#Heq
     1450lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext'
     1451lapply (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 ]
     1453elim 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. *)
     1481lemma 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 %
     1487try 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 *)
     1493lemma 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         
    17401509lemma memory_eq_to_memory_ext_pre :
    17411510  ∀m1,m1',m2,writeable.
     
    20611830@memext_store_value_of_type @Hext qed.
    20621831
     1832lemma 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'
     1840cases 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 ]
     1843whd in ⊢ ((??%?) → ?);
     1844[ 1,5,6,7,8: #Habsurd destruct ]
     1845lapply Hext lapply m1 lapply m2 lapply m2' lapply off -Hext -m1 -m2 -m2' -off -ty
     1846elim (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
    20631854(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
    20641855 * the variable is not in a local environment, then we search into the global one.
     
    21881979 (* The new variables are allocated to a size corresponding to their types. *)
    21891980 ∀sss_new_alloc  :
    2190     ∀v.meml ? v sss_new_vars →
     1981    (∀v.meml ? v sss_new_vars →
    21911982      ∀vb. lookup … sss_env_ext (\fst v) = Some ? vb →
     1983           valid_block sss_m_ext vb ∧
    21921984           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.
    21941988 (* Extension blocks are writeable. *)
    21951989 ∀sss_ext_write  : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable.
     
    22702064#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
    22712065try assumption
    2272 qed.   
     2066qed.
    22732067
    22742068lemma exec_lvalue_expr_elim :
     
    26132407] qed.
    26142408
    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 #args
    2620 elim args
    2621 [ 1: /3/
    2622 | 2: #hd #tl #Hind normalize
    2623      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 nodelta
    2628           cases Hind
    2629           [ 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 #H2
    2634                     cases Hexec_hd
    2635                     [ 2: * #error #Habsurd destruct (Habsurd)
    2636                     | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
    2637 ] ] ] ] qed.
    2638 *)
    2639 
    26402409(* The return type of any function is invariant under switch removal *)
    26412410lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
     
    26502419normalize nodelta #u @refl
    26512420qed.
    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 #id
    2660 normalize in match (fresh_for_expression e u);
    2661 #H1 #H2
    2662 >max_of_expr_rewrite
    2663 normalize in match (fresh_for_univ ???);
    2664 cases (max_of_expr e ?) in H1; #p #H1
    2665 cases id in H2; #p' #H2
    2666 normalize nodelta
    2667 cases (leb p p') normalize nodelta
    2668 [ 1: @H2 | 2: @H1 ]
    2669 qed. *)
    26702421
    26712422lemma while_fresh_lift : ∀e,s,u.
     
    28342585#e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed.
    28352586
    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 back-end
    2839    level, and then lift this to the front-end. 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 
     2587lemma 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
     2591cases 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.           
    30292702
    30302703
     
    30432716  #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
    30442717  #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
    30462720  #Hs1_eq #Hs1_eq'
    30472721  elim (sim_related_globals … ge ge'
     
    31602834       #Hexec %{0} whd in sss_result_hyp:(??%?);
    31612835       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_store
     2836       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
    31642838       whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj <sss_result_hyp normalize nodelta
    31652839       >(Hsim … Heq_lhs) whd in match (m_bind ?????);
    31662840       >(Hsim_expr … Heq_rhs) >bindIO_Value
    3167        lapply (memext_store_value_of_type' sss_m sss_m_ext xs sss_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 ?)
    31682842       [ 1: cases (store_value_of_type' ????) in Heq_store;
    31692843            [ 1: normalize #Habsurd destruct (Habsurd)
    31702844            | 2: #m normalize #Heq destruct (Heq) @refl ] ]
    3171        * #m_ext' * #Hstore_eq #Hnew_ext >Hstore_eq whd in match (m_bind ?????);
     2845       * #m_ext' * #Heq_store' #Hnew_ext >Heq_store' whd in match (m_bind ?????);
    31722846       whd destruct @conj try @refl
    31732847       %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip  sss_lu) }
     
    31752849       [ 1: @(fresh_for_Sskip … sss_lu_fresh)
    31762850       | 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 ] ]
    31822861  | 3: (* Call statement *)
    31832862       #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp)
     
    33653044        #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
    33663045  | 9: (* break *)
     3046       (* sss_enclosing_label TODO : switch case *)
    33673047       #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta
    33683048       lapply Hexec -Hexec
     
    35043184        cases (simplify_switch_elim (Expr (Evar new) (Tint sz sg)) switchcases' u'') #simplified * #u'''
    35053185        #Hswitch_eq >Hswitch_eq normalize nodelta
    3506         %{1} whd whd in ⊢ (??%?);
     3186        %{2} whd whd in ⊢ (??%?);
    35073187        (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *)
    35083188        whd in match (exec_lvalue ????);
     
    35163196        #Hlookup_new_in_new
    35173197        #Hlookup_old
    3518         lapply (Hlookup_new_in_new new ?)
     3198        cut (mem_assoc_env new sss_new_vars=true)
    35193199        [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem;
    35203200             [ 1: @False_ind
     
    35263206                  cases (identifier_eq ? new hdv) normalize nodelta
    35273207                  [ 1: #_ @refl | 2: #_ @Hmem_in_tl ] ] ] ]
     3208       #Hnew_in_new_vars
     3209       lapply (Hlookup_new_in_new new Hnew_in_new_vars)                 
    35283210       * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????);
    35293211       (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *)
     
    35333215       normalize in match store_value_of_type'; normalize nodelta
    35343216       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) *)       
    35363225       @cthulhu               
    35373226   | *: @cthulhu ]
Note: See TracChangeset for help on using the changeset viewer.