Changeset 2241


Ignore:
Timestamp:
Jul 24, 2012, 11:51:49 AM (7 years ago)
Author:
boender
Message:
  • merged changes by Claudio
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2240 r2241  
    14201420        ]
    14211421      ]
    1422     ]*)
     1422    ] *)
    14231423qed.
    14241424
     
    15901590    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    15911591    [ >nth_append_first [2: @Hi]
    1592       <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     1592      <Heq2b >lookup_insert_miss
    15931593      [ >lookup_insert_miss
    15941594        [ >lookup_insert_miss
    15951595          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
    15961596            [ >lookup_insert_miss
     1597              [ (* USE[pass]: sigma_safe *)
     1598                lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
     1599                cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
     1600                #pc #j normalize nodelta
     1601                cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
     1602                #Spc #Sj normalize nodelta
     1603                cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
     1604                #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj
     1605                lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|))))
     1606                cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %); #H
     1607                [ cases (le_to_or_lt_eq … (leb_true_to_le … H)) -H #H
     1608                  [ >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
     1609                    >lookup_insert_miss
     1610                    [ cases (le_to_or_lt_eq … (le_S_S_to_le … H)) -H #H
     1611                      [ >lookup_insert_miss
     1612                        [ #H2 @H2
     1613                        | @bitvector_of_nat_abs
     1614                          [3: @lt_to_not_eq @H
     1615                          |1: @(transitive_lt ??? H)
     1616                          ]
     1617                          @prefix_ok
     1618                        ]
     1619                      | >H >lookup_insert_hit
     1620                        (* USE: inc_pc = lookup |prefix| *)
     1621                        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1622                        #H2 @H2
     1623                      ]
     1624                    | @bitvector_of_nat_abs
     1625                      [3: @lt_to_not_eq @H
     1626                      |1: @(transitive_lt ??? H)
     1627                      ]
     1628                      @prefix_ok1
     1629                    ]
     1630                  | >H >lookup_insert_hit normalize nodelta
     1631                    >(not_le_to_leb_false … (lt_to_not_le ?? (le_S_S ?? (le_n (|prefix|)))))
     1632                    normalize nodelta
     1633                    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1634                    #H2 >(proj2 ?? (proj1 ?? Hpolicy))
     1635                  ]
     1636                |
     1637                       
     1638                       
     1639                       
     1640                [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
     1641                  [1,4,7: cases (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) #H
     1642                    [1,3,5: >(le_to_leb_true … H) normalize nodelta cases (le_to_or_lt_eq … H) -H #H
     1643                      [1,3,5: >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
     1644                        >lookup_insert_miss
     1645                        [2,4,6: @bitvector_of_nat_abs
     1646                          [3,6,9: @lt_to_not_eq @H
     1647                          |1,4,7: @(transitive_lt ??? H)
     1648                          ]
     1649                          @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
     1650                          @le_S_S >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     1651                        ]
     1652                        cases (le_to_or_lt_eq … H) -H #H
     1653                        [1,3,5: >lookup_insert_miss
     1654                          [1,3,5: #H @H
     1655                          |2,4,6: @bitvector_of_nat_abs
     1656                            [3,6,9: @lt_to_not_eq @(le_S_S_to_le … H)
     1657                            |1,4,7: @(transitive_lt ??? (le_S_S_to_le … H))
     1658                            ]
     1659                            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
     1660                            >append_length @le_S_S @le_plus_n_r
     1661                          ]
     1662                        |2,4,6: >(injective_S … H) >lookup_insert_hit
     1663                          (* USE: blerp *)
     1664                          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1665                          #H @H
     1666                        ]
     1667                      |2,4,6: >H >lookup_insert_hit >(not_le_to_leb_false)
     1668                        [2,4,6: @le_to_not_lt @le_n]
     1669                        normalize nodelta
     1670                        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     1671                        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     1672                         lapply (refl ? (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     1673                          cases (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     1674                          [1,3,5: normalize nodelta #_ #abs cases abs
     1675                          |2,4,6: #x cases x -x #ppc #pj normalize nodelta #PEQ
     1676                            lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     1677                            cases (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     1678                            [1,3,5: normalize nodelta #_ #abs cases abs
     1679                            |2,4,6: #x cases x -x #Sppc #Spj normalize nodelta #SPEQ #Pcompact
     1680                              >(lookup_opt_lookup_hit … SPEQ 〈0,short_jump〉)
     1681                              >(lookup_opt_lookup_hit … PEQ 〈0,short_jump〉) in Holdeq;
     1682                              #H >Pcompact >(proj1 ?? (pair_destruct ?????? H))
     1683                              >commutative_plus >assoc_plus1 <(proj2 ?? (proj1 ?? Hpolicy))
     1684                              <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1685                              >prf >nth_append_second
     1686                              [1,3,5: <minus_n_n whd in match (nth ????); >p1
     1687                                cases daemon (* to be lemmatized *)
     1688                              |2,4,6: @le_n
     1689                              ]
     1690                            ]
     1691                          ]
     1692                        ]
     1693                      |2,4,6: >(not_le_to_leb_false … H)
     1694                        >not_le_to_leb_false
     1695                        [2,4,6: @lt_to_not_le @le_S_to_le @not_le_to_lt @H
     1696                        |1,3,5: normalize nodelta #H @H
     1697                        ]
     1698                      ]
     1699                    |2,5,8: cases daemon (* like previous case *)
     1700                    |3,6,9: cases daemon (* like previous case *)
     1701                    ]
     1702                  |4,5: #x normalize nodelta cases daemon (* blerp *)
     1703                  |1: cases daemon (* blerp *)
     1704                  ]
     1705               
     1706                               
     1707                         
     1708
     1709   (*(\fst  (short_jump_cond (bitvector_of_nat 16 Spc)
     1710              (bitvector_of_nat 16
     1711               (inc_pc
     1712                +instruction_size_jmplen
     1713                 (max_length old_length
     1714                  (select_jump_length labels old_sigma inc_pc_sigma inc_added
     1715                   (|prefix|) xx)) (Jmp xx))))
     1716  =true                   *)
     1717                       
     1718                 
     1719  ]       
    15971720              [ >lookup_insert_miss
    15981721                [ (* USE[pass]: sigma_safe *)
     
    16051728                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
    16061729                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
    1607                     [1,4,7:
    1608 *)
     1730                    [1,4,7: *)
    16091731qed.
    16101732
Note: See TracChangeset for help on using the changeset viewer.