Changeset 2211 for src/ASM/PolicyStep.ma
 Timestamp:
 Jul 18, 2012, 3:57:09 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2152 r2211 17 17 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd policy) 〈0,short_jump〉))) 18 18 (sigma_compact_unsafe program labels policy)) 19 (\fst policy <2^16)).19 (\fst policy ≤ 2^16)). 20 20 (Σx:bool × (option ppc_pc_map). 21 21 let 〈no_ch,y〉 ≝ x in … … 30 30 (sigma_jump_equal program old_policy p → no_ch = true)) 31 31 (no_ch = true → sigma_pc_equal program old_policy p)) 32 (\fst p <2^16)32 (\fst p ≤ 2^16) 33 33 ]) 34 34 ≝ … … 93 93 (Stub ??)〉〉 94 94 ) in 95 if g eb (\fst final_policy) 2^16 then95 if gtb (\fst final_policy) 2^16 then 96 96 〈eqb final_added 0, None ?〉 97 97 else … … 127 127 ] 128 128  #abs >abs in Hsig; #Hsig 129 @(absurd ? Hsig) @l e_to_not_lt @leb_true_to_le <geb_to_leb@Hge129 @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge 130 130 ] 131 131  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 … … 141 141 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2 142 142 ] 143  @not_l e_to_lt @leb_false_to_not_le <geb_to_leb@p1143  @not_lt_to_le @ltb_false_to_not_lt @p1 144 144 ] 145 145 4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %); … … 153 153 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 154 154 * 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; 157 157 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 158 158 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss … … 160 160 [ >(nth_append_first ? i prefix ?? Hi) 161 161 (* USE[pass]: not_jump_default *) 162 @(proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)162 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi) 163 163  @bitvector_of_nat_abs 164 164 [ @(transitive_lt ??? Hi) ] … … 199 199 ] 200 200 ] *) 201  (* 0 ↦ 0 *) cases daemon (*202 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss201  (* 0 ↦ 0 *) cases daemon 202 (* <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 203 203 [ cases (decidable_eq_nat 0 (prefix)) 204 204 [ #Heq <Heq >lookup_insert_hit 205 205 (* 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 207 208 (* 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))))))))) 210 210  #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))))))))) 212 212  @bitvector_of_nat_abs 213 213 [3: @Hneq] … … 216 216  @bitvector_of_nat_abs 217 217 [3: @lt_to_not_eq / by / ] 218 ] 218 ] 219 219 [1,3: / by / 220 220 2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S … … 226 226 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 227 227 ] 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; 230 230 cases (le_to_or_lt_eq … Hi) Hi; #Hi 231 231 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 232 232 [ (* 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)) 234 234 <(proj2 ?? (pair_destruct ?????? Heq2)) 235 235 @pair_elim #opc #oj #EQ1 >lookup_insert_miss … … 322 322 ] *) 323 323 ] 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; 326 326 <(proj2 ?? (pair_destruct ?????? Heq2)) 327 327 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 332 332 [ >lookup_opt_insert_miss 333 333 [ (* USE[pass]: sigma_compact_unsafe *) 334 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)334 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 335 335 [ @le_S_to_le @Hi ] 336 336 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 351 351  >Hi >lookup_opt_insert_hit normalize nodelta 352 352 (* USE[pass]: sigma_compact_unsafe *) 353 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)353 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 354 354 [ <Hi @le_n 355 355  cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 357 357  #x cases x x #x1 #x2 358 358 (* 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)))))))) 360 360 <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 361 361 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); … … 393 393 >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta 394 394 (* USE: out_of_program_none ← *) 395 lapply (proj2 ?? (proj 1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i ?))395 lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?)) 396 396 [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r 397 397  >Hi 398 398 (* 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)))))))) 400 400 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma)) 401 401 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma) in ⊢ (???% → %); 402 402 [ #Heq #_ #H @⊥ @(absurd (prefix > prefix)) 403 [ @H @refl403 [ @H % 404 404  @le_to_not_lt @le_n 405 405 ] … … 427 427 ] *) 428 428 ] 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)) 431 431 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) 432 432 (* USE[pass]: policy_jump_equal → added = 0 *) 433 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) ?)433 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?) 434 434 [ cases instr in Heq1 Heq; 435 435 [2,3,6: #x [3: #y] normalize nodelta #_ #_ % … … 437 437 #Heq lapply Holdeq Holdeq 438 438 (* 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)))))))) 440 440 lapply (Heq (prefix) ?) 441 441 [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] … … 458 458 <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq Holdeq 459 459 (* 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)))))))) 461 461 lapply (Heq (prefix) ?) 462 462 [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] … … 496 496 ] *) 497 497 ] 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)))) 501 501 <(proj2 ?? (pair_destruct ?????? Heq2)) 502 502 <(proj1 ?? (pair_destruct ?????? Heq2)) … … 527 527 [1,3,5: >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) 528 528 @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)))))))) 530 530 2,4,6: @bitvector_of_nat_abs 531 531 [3,6,9: @lt_to_not_eq @le_n … … 538 538 2,4,6: >Hi >lookup_insert_hit 539 539 (* USE fst p = lookup prefix *) 540 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))540 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 541 541 <(Hold Hadded (prefix) (le_n (prefix))) 542 542 (* USE: sigma_compact (from old_sigma) *) … … 587 587 [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 588 588 (* USE: fst p = lookup prefix *) 589 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))589 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 590 590 2,4: @bitvector_of_nat_abs 591 591 [3,6: @lt_to_not_eq @le_n … … 601 601 @jump_length_le_max / by I/ 602 602 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)))))))) 604 604 <(Hold ? (prefix) (le_n (prefix))) 605 605 [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H … … 671 671 >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) @sym_eq 672 672 (* USE: fst p = lookup prefix *) 673 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))673 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 674 674 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: 675 675 @bitvector_of_nat_abs … … 686 686 >Hi >lookup_insert_hit 687 687 (* USE fst p = lookup prefix *) 688 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))688 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 689 689 <(Hold Hadded (prefix) (le_n (prefix))) 690 690 (* USE: sigma_compact (from old_sigma) *) … … 746 746 [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 747 747 (* USE: fst p = lookup prefix *) 748 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))748 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 749 749 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 750 750 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n … … 797 797 ] *) 798 798 ] 799  (* out_of_program_none *) cases daemon 799  (* out_of_program_none *) cases daemon 800 800 (* #i #Hi2 >append_length <commutative_plus @conj 801 801 [ (* → *) #Hi normalize in Hi; … … 969 969 ] *) 970 970 ] 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; 973 972 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 974 973 [ >nth_append_first [2: @Hi] … … 978 977 [ elim (le_to_or_lt_eq … Hi) Hi #Hi 979 978 [ >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 1119 991 ] 1120 992  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
Note: See TracChangeset
for help on using the changeset viewer.