Changeset 2211 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Jul 18, 2012, 3:57:09 PM (8 years ago)
Author:
boender
Message:
  • finished proof of sigma specification
  • added some stuff to Util, as usual
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2152 r2211  
    1717    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
    1818    (sigma_compact_unsafe program labels policy))
    19     (\fst policy < 2^16)).
     19    (\fst policy 2^16)).
    2020  (Σx:bool × (option ppc_pc_map).
    2121    let 〈no_ch,y〉 ≝ x in
     
    3030       (sigma_jump_equal program old_policy p → no_ch = true))
    3131       (no_ch = true → sigma_pc_equal program old_policy p))
    32        (\fst p < 2^16)
     32       (\fst p 2^16)
    3333    ])
    3434    ≝
     
    9393        (Stub ??)〉〉
    9494    ) in
    95     if geb (\fst final_policy) 2^16 then
     95    if gtb (\fst final_policy) 2^16 then
    9696      〈eqb final_added 0, None ?〉
    9797    else
     
    127127    ]
    128128  | #abs >abs in Hsig; #Hsig
    129     @(absurd ? Hsig) @le_to_not_lt @leb_true_to_le <geb_to_leb @Hge
     129    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
    130130  ]
    131131| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
     
    141141     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
    142142  ]
    143   | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
     143  | @not_lt_to_le @ltb_false_to_not_lt @p1
    144144  ]
    145145|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
     
    153153  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    154154   * commented out for full proofs, but this needs a lot of memory and time *)
    155   [ (* not_jump_default *) cases daemon (*
    156     #i >append_length <commutative_plus #Hi normalize in Hi;
     155  [ (* not_jump_default *) cases daemon
     156    (* #i >append_length <commutative_plus #Hi normalize in Hi;
    157157    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    158158    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     
    160160        [ >(nth_append_first ? i prefix ?? Hi)
    161161          (* USE[pass]: not_jump_default *)
    162           @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)
     162          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)
    163163        | @bitvector_of_nat_abs
    164164          [ @(transitive_lt ??? Hi) ]
     
    199199      ]
    200200    ] *)
    201   | (* 0 ↦ 0 *) cases daemon (*
    202     <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     201  | (* 0 ↦ 0 *) cases daemon
     202    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    203203    [ cases (decidable_eq_nat 0 (|prefix|))
    204204      [ #Heq <Heq >lookup_insert_hit
    205205        (* USE: inc_pc = fst policy *)
    206         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     206        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     207        <Heq
    207208        (* USE[pass]: 0 ↦ 0 *)
    208         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    209         <Heq #ONE #TWO >TWO >ONE @refl
     209        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    210210      | #Hneq >lookup_insert_miss
    211         [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     211        [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    212212        | @bitvector_of_nat_abs
    213213          [3: @Hneq]
     
    216216    | @bitvector_of_nat_abs
    217217      [3: @lt_to_not_eq / by / ]
    218     ]     
     218    ]
    219219    [1,3: / by /
    220220    |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     
    226226    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    227227  ]
    228   | (* jump_increase *) cases daemon (*
    229     #i >append_length >commutative_plus #Hi normalize in Hi;
     228  | (* jump_increase *) cases daemon
     229    (* #i >append_length >commutative_plus #Hi normalize in Hi;
    230230    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    231231    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    232232      [ (* USE[pass]: jump_increase *)
    233         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi))
     233        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
    234234        <(proj2 ?? (pair_destruct ?????? Heq2))
    235235        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     
    322322    ] *)
    323323  ]
    324   | (* sigma_compact_unsafe *) cases daemon (*
    325     #i >append_length <commutative_plus #Hi normalize in Hi;
     324  | (* sigma_compact_unsafe *) cases daemon
     325    (* #i >append_length <commutative_plus #Hi normalize in Hi;
    326326    <(proj2 ?? (pair_destruct ?????? Heq2))
    327327    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     
    332332            [ >lookup_opt_insert_miss
    333333              [ (* USE[pass]: sigma_compact_unsafe *)
    334                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
     334                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    335335                [ @le_S_to_le @Hi ]
    336336                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     
    351351            | >Hi >lookup_opt_insert_hit normalize nodelta
    352352              (* USE[pass]: sigma_compact_unsafe *)
    353               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
     353              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    354354              [ <Hi @le_n
    355355              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     
    357357                | #x cases x -x #x1 #x2
    358358                  (* USE: inc_pc = fst inc_sigma *)
    359                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     359                  lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    360360                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
    361361                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
     
    393393      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
    394394      (* USE: out_of_program_none ← *)
    395       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i ?))
     395      lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?))
    396396      [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r
    397397      | >Hi
    398398        (* USE: inc_pc = fst policy *)
    399         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     399        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    400400        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
    401401        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
    402402        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
    403           [ @H @refl
     403          [ @H %
    404404          | @le_to_not_lt @le_n
    405405          ]
     
    427427    ] *)
    428428  ]
    429   | (* policy_jump_equal → added = 0 *) cases daemon (*
    430     <(proj2 ?? (pair_destruct ?????? Heq2))
     429  | (* policy_jump_equal → added = 0 *) cases daemon
     430    (* <(proj2 ?? (pair_destruct ?????? Heq2))
    431431    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
    432432    (* USE[pass]: policy_jump_equal → added = 0 *)
    433     >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) ?)
     433    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?)
    434434    [ cases instr in Heq1 Heq;
    435435      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
     
    437437        #Heq lapply Holdeq -Holdeq
    438438        (* USE: inc_pc = fst inc_sigma *)
    439         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     439        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    440440        lapply (Heq (|prefix|) ?)
    441441        [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     
    458458          <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq -Holdeq
    459459          (* USE: inc_pc = fst inc_sigma *)
    460           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     460          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    461461          lapply (Heq (|prefix|) ?)
    462462          [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     
    496496    ] *)
    497497  ]
    498   | (* added = 0 → policy_pc_equal *) cases daemon (*
    499     (* USE: added = 0 → policy_pc_equal *)
    500     lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     498  | (* added = 0 → policy_pc_equal *) cases daemon
     499    (* USE[pass]: added = 0 → policy_pc_equal *)
     500    (* lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    501501    <(proj2 ?? (pair_destruct ?????? Heq2))
    502502    <(proj1 ?? (pair_destruct ?????? Heq2))
     
    527527          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
    528528            @sym_eq (* USE: fst p = lookup |prefix| *)
    529              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     529            @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    530530          |2,4,6: @bitvector_of_nat_abs
    531531            [3,6,9: @lt_to_not_eq @le_n
     
    538538      |2,4,6: >Hi >lookup_insert_hit
    539539        (* USE fst p = lookup |prefix| *)
    540         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     540        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    541541        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    542542        (* USE: sigma_compact (from old_sigma) *)
     
    587587             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
    588588             (* USE: fst p = lookup |prefix| *)
    589              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     589             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    590590           |2,4: @bitvector_of_nat_abs
    591591             [3,6: @lt_to_not_eq @le_n
     
    601601           @jump_length_le_max / by I/
    602602         |2,4: #H (* USE: fst p = lookup |prefix| *)
    603            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     603           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    604604           <(Hold ? (|prefix|) (le_n (|prefix|)))
    605605           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
     
    671671              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
    672672              (* USE: fst p = lookup |prefix| *)
    673               @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     673              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    674674            |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    675675              @bitvector_of_nat_abs
     
    686686          >Hi >lookup_insert_hit
    687687          (* USE fst p = lookup |prefix| *)
    688           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     688          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    689689          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    690690          (* USE: sigma_compact (from old_sigma) *)
     
    746746              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
    747747              (* USE: fst p = lookup |prefix| *)
    748               @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     748              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    749749            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    750750              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
     
    797797    ] *)
    798798  ]
    799   | (* out_of_program_none *) cases daemon 
     799  | (* out_of_program_none *) cases daemon
    800800    (* #i #Hi2 >append_length <commutative_plus @conj
    801801    [ (* → *) #Hi normalize in Hi;
     
    969969    ] *)
    970970  ]
    971   | (* sigma_safe *) cases daemon
    972     (* #i >append_length >commutative_plus #Hi normalize in Hi;
     971  | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
    973972    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    974973    [ >nth_append_first [2: @Hi]
     
    978977          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
    979978            [ >lookup_insert_miss
    980               [ lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
    981                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi))
    982                lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma))
    983                 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) in ⊢ (???% → %);
    984                 [ normalize nodelta #_ #abs cases abs
    985                 | #x cases x -x #ipc #ij #EQi normalize nodelta
    986                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
    987                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
    988                   [ normalize nodelta #_ #abs cases abs
    989                   | #x cases x -x #Sipc #Sij #EQSi normalize nodelta #Hcompact
    990                     >(lookup_opt_lookup_hit … EQi 〈0,short_jump〉)
    991                     >(lookup_opt_lookup_hit … EQSi 〈0,short_jump〉) >Hcompact
    992                     normalize nodelta (*cases ij*) normalize nodelta
    993                     lapply (refl ? (nth i ? prefix 〈None ?, Comment []〉))
    994                     cases (nth i ? prefix 〈None ?, Comment []〉) in ⊢ (???% → %);
    995                     #lbl #ins normalize nodelta #Hins #Hind #dest #Hi
    996                     lapply (Hind dest Hi) -Hind #Hind
    997                     elim (decidable_le (lookup_def … labels dest 0) (S (|prefix|)))
    998                     [ #Hle elim (le_to_or_lt_eq … Hle) -Hle #Hle
    999                       [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) -Hle #Hle
    1000                         [ >(le_to_leb_true ?? (le_S_to_le ?? Hle)) in Hind;
    1001                           >(le_to_leb_true ?? (le_S ?? (le_S_to_le ?? Hle)))
    1002                           normalize nodelta >lookup_insert_miss
    1003                           [ >lookup_insert_miss
    1004                             [ #H @H
    1005                             | @bitvector_of_nat_abs
    1006                               [3: @lt_to_not_eq @Hle
    1007                               |1: @(transitive_lt ??? Hle)
    1008                               ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    1009                                >append_length @le_S_S @le_plus_n_r
    1010                             ]
    1011                           | @bitvector_of_nat_abs
    1012                             [3: @lt_to_not_eq @le_S_to_le @le_S_S @Hle
    1013                             |1: @(transitive_lt ??? Hle) @le_S_to_le
    1014                             ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    1015                             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    1016                           ]
    1017                         | >Hle >Hle in Hind; >(le_to_leb_true ?? (le_n (|prefix|)))
    1018                           >(le_to_leb_true ?? (le_S ?? (le_n (|prefix|))))
    1019                           normalize nodelta >lookup_insert_miss
    1020                           [ >lookup_insert_hit
    1021                             >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1022                             #H @H
    1023                           | @bitvector_of_nat_abs
    1024                             [3: @lt_to_not_eq @le_n
    1025                             |1: @le_S_to_le
    1026                             ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    1027                             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    1028                           ]
    1029                         ]
    1030                       | >Hle >Hle in Hind;
    1031                         >(not_le_to_leb_false (S (|prefix|)) (|prefix|))
    1032                         [2: @le_to_not_lt @le_n]
    1033                         >(le_to_leb_true ?? (le_n (S (|prefix|))))
    1034                         normalize nodelta >lookup_insert_hit
    1035                         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    1036                         [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    1037                         | lapply (proj2 ?? (proj1 ?? Hpolicy))
    1038                           lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    1039                           cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    1040                           [ normalize nodelta #_ #_ #abs cases abs
    1041                           | #x cases x -x #opc #oj #EQo
    1042                             lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    1043                             cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    1044                             [ normalize nodelta #_ #_ #abs cases abs
    1045                             | #x cases x -x #Sopc #Soj #EQSo normalize nodelta
    1046                               #Hadded #Hcommon
    1047                               >(lookup_opt_lookup_hit … EQSo 〈0,short_jump〉)
    1048                               >Hcommon >(lookup_opt_lookup_hit … EQo 〈0,short_jump〉) in Holdeq;
    1049                               #Holdeq >(proj1 ?? (pair_destruct ?????? Holdeq))
    1050                               >(commutative_plus old_pc ?) >associative_plus
    1051                               <Hadded
    1052                               <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1053                               >prf >nth_append_second
    1054                               [ <minus_n_n whd in match (nth ????); >p1 cases instr in Heq1;
    1055                                 [2,3,6: #x [3: #y] normalize nodelta #Heq1
    1056                                   <(proj2 ?? (pair_destruct ?????? Heq1))
    1057                                   <(commutative_plus inc_pc)
    1058                                   >(instruction_size_irrelevant ?? oj short_jump)
    1059                                   [1,3,5: #H @H
    1060                                   |2,4,6: @nmk #H @H
    1061                                   ]
    1062                                 |4,5: #x normalize nodelta #Heq1
    1063                                   <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
    1064                                   cases daemon (* axiomatise this *)
    1065                                 |1: #pi cases pi
    1066                                   [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    1067                                     [1,2,3,6,7,24,25: #x #y
    1068                                     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    1069                                     normalize nodelta #Heq1
    1070                                     <(proj2 ?? (pair_destruct ?????? Heq1))
    1071                                     <(commutative_plus inc_pc)
    1072                                     >(instruction_size_irrelevant ?? oj short_jump)
    1073                                     [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    1074                                       #H @H
    1075                                     |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    1076                                       @nmk #H @H
    1077                                     ]
    1078                                   |9,10,11,12,13,14,15,16,17:
    1079                                     #x [3,4,5,8,9: #y] normalize nodelta #Heq1
    1080                                     <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
    1081                                     cases daemon (* axiomatise this *)
    1082                                   ]
    1083                                 ]
    1084                               | @le_n
    1085                               ]
    1086                             ]
    1087                           ]
    1088                         ]
    1089                       ]
    1090                     | #X >(not_le_to_leb_false … X)
    1091                       >(not_le_to_leb_false … (lt_to_not_le … (le_S_to_le … (not_le_to_lt … X)))) in Hind;
    1092                       normalize nodelta <(proj1 ?? (pair_destruct ?????? Heq2))
    1093                       cases instr in Heq1;
    1094                       [2,3,6: #x [3: #y] normalize nodelta #_ #H @H
    1095                       |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
    1096                         cases daemon (* axiomatise this *)
    1097                       |1: #pi cases pi
    1098                         [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    1099                           [1,2,3,6,7,24,25: #x #y
    1100                           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    1101                           normalize nodelta #_ #H @H
    1102                         |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    1103                           normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    1104                           #Hind cases daemon (* axiomatise this *)
    1105                         ]
    1106                       ]
    1107                     ]
    1108                   ]
    1109                 ]
    1110               | @bitvector_of_nat_abs
    1111                 [3: @lt_to_not_eq @Hi
    1112                 |1: @(transitive_lt ??? Hi)
    1113                 ]
    1114                 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    1115                 @le_S_S @le_plus_n_r
    1116               ]
    1117             | >Hi >lookup_insert_hit lapply ((proj2 ?? Hpolicy) i)
    1118             ] XXX to be continued *)
     979              [ >lookup_insert_miss
     980                [ (* USE[pass]: sigma_safe *)
     981                  lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
     982                  cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
     983                  #pc #j normalize nodelta
     984                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
     985                  #Spc #Sj normalize nodelta
     986                  cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
     987                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
     988                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
     989                    [1,4,7: *)
     990                 
    1119991  ]         
    1120992| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
Note: See TracChangeset for help on using the changeset viewer.