Changeset 1609 for src/ASM/Assembly.ma
- Timestamp:
- Dec 14, 2011, 2:44:42 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r1607 r1609 5 5 include alias "basics/logic.ma". 6 6 include alias "arithmetics/nat.ma". 7 include "utilities/extralib.ma". 7 8 8 9 definition assembly_preinstruction ≝ … … 462 463 463 464 464 (* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)465 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.465 (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *) 466 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16. 466 467 467 468 definition expand_relative_jump_internal: … … 667 668 let 〈pc,labels〉 ≝ acc in 668 669 let 〈label,instr〉 ≝ x in 669 670 671 672 673 674 let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉)in675 670 let new_labels ≝ 671 match label with 672 [ None ⇒ labels 673 | Some l ⇒ add … labels l 〈|prefix|, pc〉 674 ] in 675 let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in 676 〈add_instruction_size pc jmp_len instr, new_labels〉 676 677 ) 〈0, empty_map …〉 in 677 678 final_labels. … … 705 706 qed. 706 707 707 definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝708 definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝ 708 709 λlabels.λpc.λlbl. 709 710 let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in 710 711 if leb pc addr (* forward jump *) 711 712 then if leb (addr - pc) 126 712 then short_jump713 else long_jump713 then 〈addr, short_jump〉 714 else 〈addr, long_jump〉 714 715 else if leb (pc - addr) 129 715 then short_jump716 else long_jump.717 718 definition select_call_length: label_map → ℕ → Identifier → jump_length ≝716 then 〈addr, short_jump〉 717 else 〈addr, long_jump〉. 718 719 definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝ 719 720 λlabels.λpc_nat.λlbl. 720 721 let pc ≝ bitvector_of_nat 16 pc_nat in 721 let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in 722 let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in 723 let addr ≝ bitvector_of_nat 16 addr_nat in 722 724 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in 723 725 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 724 726 if eq_bv ? fst_5_addr fst_5_pc 725 then medium_jump726 else long_jump.727 then 〈addr_nat, medium_jump〉 728 else 〈addr_nat, long_jump〉. 727 729 728 definition select_jump_length: label_map → ℕ → Identifier → jump_length ≝730 definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝ 729 731 λlabels.λpc.λlbl. 730 732 let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in 731 733 if leb pc addr 732 734 then if leb (addr - pc) 126 733 then short_jump735 then 〈addr, short_jump〉 734 736 else select_call_length labels pc lbl 735 737 else if leb (pc - addr) 129 736 then short_jump738 then 〈addr, short_jump〉 737 739 else select_call_length labels pc lbl. 738 740 739 741 definition jump_expansion_step_instruction: label_map → ℕ → 740 preinstruction Identifier → option jump_length≝742 preinstruction Identifier → option (ℕ × jump_length) ≝ 741 743 λlabels.λpc.λi. 742 744 match i with … … 800 802 ∀i:ℕ.i < |prefix| → 801 803 (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ 802 ∃p, j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).804 ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉). 803 805 804 806 (* these should be moved to BitVector at some point *) … … 826 828 jump_in_policy prefix p). 827 829 ∀i:ℕ.i < |prefix| → 828 ¬is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔829 lookup_opt … (bitvector_of_nat 16 i) policy = None ?.830 iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉)) 831 (lookup_opt … (bitvector_of_nat 16 i) policy = None ?). 830 832 #prefix #policy #i #Hi @conj 831 833 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy)) 832 834 cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?); 833 835 [ #H @H 834 | #x cases x #y #z#H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))835 @(ex_intro … y (ex_intro … z H))836 | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi)) 837 @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H))) 836 838 ] 837 839 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj) 838 #H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)840 #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs) 839 841 ] 840 842 qed. 841 843 842 844 definition jump_expansion_start: 843 845 ∀program:(Σl:list labelled_instruction.|l| < 2^16). … … 846 848 jump_in_policy program policy ∧ 847 849 ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) → 848 lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0, short_jump〉 ≝850 lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝ 849 851 λprogram. 850 852 foldl_strong (option Identifier × pseudo_instruction) … … 853 855 jump_in_policy prefix policy ∧ 854 856 ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 855 lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0, short_jump〉)857 lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉) 856 858 program 857 859 (λprefix.λx.λtl.λprf.λpolicy. … … 859 861 match instr with 860 862 [ Instruction i ⇒ match i with 861 [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy862 | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy863 | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy864 | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy865 | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy866 | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy867 | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy868 | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy869 | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy863 [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 864 | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 865 | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 866 | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 867 | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 868 | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 869 | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 870 | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 871 | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 870 872 | _ ⇒ (pi1 … policy) 871 873 ] 872 | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy873 | Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0, short_jump〉 policy874 | _ ⇒ (pi1 …policy)874 | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 875 | Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy 876 | _ ⇒ (pi1 ?? policy) 875 877 ] 876 878 ) (Stub ? ?). … … 901 903 >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H 902 904 ] 903 #H elim H; -H; #t1 #H elim H; -H #t2 #H 905 #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H 904 906 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H; 905 907 [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,57,59,61: … … 950 952 >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n // 951 953 ] 952 @(ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))954 @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))) 953 955 ] 954 956 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) … … 980 982 λprogram.λop.λp. 981 983 (∀i:ℕ.i < |program| → 982 jmpleq 983 (\snd (bvt_lookup … (bitvector_of_nat ? i) op 〈0,short_jump〉)) 984 (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))). 985 984 let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in 985 let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in 986 jmpleq oj j). 987 988 definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝ 989 (*λlabels.*)λpolicy. 990 bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in 991 match jmp_len with 992 [ short_jump ⇒ if leb pc_nat addr_nat 993 then le (addr_nat - pc_nat) 126 994 else le (pc_nat - addr_nat) 129 995 | medium_jump ⇒ 996 let addr ≝ bitvector_of_nat 16 addr_nat in 997 let pc ≝ bitvector_of_nat 16 pc_nat in 998 let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in 999 let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in 1000 eq_bv 5 fst_5_addr fst_5_pc = true 1001 | long_jump ⇒ True 1002 ] 1003 ). 1004 986 1005 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16). 1006 ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) → 1007 ∀l.occurs_exactly_once l program → 1008 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 1009 ∃a.lookup … lm l = Some ? 〈i,a〉). 987 1010 ∀old_policy:(Σpolicy. 988 1011 (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ … … 993 1016 policy_increase program old_policy policy) 994 1017 ≝ 995 λprogram.λold_policy. 996 let labels ≝ create_label_map program old_policy in 1018 λprogram.λlabels.λold_policy. 997 1019 let 〈final_pc, final_policy〉 ≝ 998 1020 foldl_strong (option Identifier × pseudo_instruction) … … 1015 1037 ] in 1016 1038 let 〈new_pc, new_policy〉 ≝ 1017 let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, short_jump〉 in1039 let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in 1018 1040 match add_instr with 1019 1041 [ None ⇒ (* i.e. it's not a jump *) 1020 1042 〈add_instruction_size pc long_jump instr, policy〉 1021 | Some ai ⇒1043 | Some z ⇒ let 〈addr,ai〉 ≝ z in 1022 1044 let new_length ≝ max_length old_length ai in 1023 〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉1045 〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉 1024 1046 ] in 1025 1047 〈new_pc, new_policy〉 … … 1029 1051 [ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr 1030 1052 [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 1031 | #z normalize nodelta >lookup_opt_insert_miss1053 | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss 1032 1054 [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 1033 1055 | >eq_bv_sym @bitvector_of_nat_abs … … 1044 1066 cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y 1045 1067 [ @(proj1 ?? Hacc Hj) 1046 | #z elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #Hn 1047 % [ @h | % [ @n | <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs 1068 | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj 1069 @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???); 1070 >lookup_opt_insert_miss [ @Hj | @bitvector_of_nat_abs ] 1048 1071 [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) 1049 1072 |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) … … 1051 1074 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1052 1075 @le_S_S @le_plus_n_r 1053 ] ]1054 1076 ] 1055 1077 | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc 1056 #H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)1078 #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?) 1057 1079 normalize nodelta #x #y [2: #z] 1058 #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?))1059 [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs1080 #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) 1081 [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs 1060 1082 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 1061 1083 |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) … … 1070 1092 [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta 1071 1093 [3,5,11: #H @⊥ @H (* instr is not a jump *) 1072 |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)1094 |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?) 1073 1095 #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) 1074 1096 [1,3,5: #H destruct (H)] 1075 1097 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1076 1098 @le_S_S @le_plus_n_r 1077 |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) # h #n1099 |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j 1078 1100 whd in match (snd ???); @(ex_intro ?? pc) 1079 [ @(ex_intro ?? (max_length n (select_jump_length (create_label_map program old_policy) pc id))) 1080 | @(ex_intro ?? (max_length n (select_call_length (create_label_map program old_policy) pc id))) 1081 ] @lookup_opt_insert_hit 1101 [ @(ex_intro ?? (\fst (select_jump_length labels pc id))) 1102 @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id)))) 1103 cases (select_jump_length labels pc id) 1104 | @(ex_intro ?? (\fst (select_call_length labels pc id))) 1105 @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id)))) 1106 cases (select_call_length labels pc id) 1107 ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit 1082 1108 |8,10: #_ // 1083 1109 |1,2: cases pi … … 1085 1111 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H 1086 1112 |1,2,3,6,7,33,34: #x #y #H @⊥ @H 1087 |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #h #n 1088 whd in match (snd ???); 1089 @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?)) 1113 |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j 1114 whd in match (snd ???); @(ex_intro ?? pc) 1115 @(ex_intro ?? (\fst (select_reljump_length labels pc id))) 1116 @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id)))) 1117 normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta 1090 1118 @lookup_opt_insert_hit 1091 |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #h #n 1092 whd in match (snd ???); 1093 @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?)) 1119 |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j 1120 whd in match (snd ???); @(ex_intro ?? pc) 1121 @(ex_intro ?? (\fst (select_reljump_length labels pc id))) 1122 @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id)))) 1123 normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta 1094 1124 @lookup_opt_insert_hit 1095 |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)1096 # x #ynormalize nodelta1125 |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?) 1126 #z cases z -z #x #y #z normalize nodelta 1097 1127 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) 1098 1128 [1,3,5: #H destruct (H)] … … 1100 1130 @le_S_S @le_plus_n_r 1101 1131 |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x 1102 #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)1103 # x #ynormalize nodelta1132 #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?) 1133 #z cases z -z #x #y #z normalize nodelta 1104 1134 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) 1105 1135 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)] 1106 1136 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1107 1137 @le_S_S @le_plus_n_r 1108 |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n 1109 cases (lookup ??? old_policy ?) # x #ynormalize nodelta1138 |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j 1139 cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta 1110 1140 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) 1111 1141 [1,3,5,7,9,11,13: #H destruct (H)] … … 1121 1151 [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi; 1122 1152 cases (le_to_or_lt_eq … Hi) -Hi; #Hi 1123 [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0, short_jump〉)1153 [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉) 1124 1154 #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 1125 1155 | normalize nodelta >(injective_S … Hi) … … 1127 1157 [ >lookup_opt_lookup_miss 1128 1158 [ // 1129 | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0, short_jump〉)1159 | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉) 1130 1160 #x #y normalize nodelta 1131 1161 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) … … 1156 1186 ] 1157 1187 ] 1158 | #x #Ha #i >append_length >commutative_plus #Hi normalize in Hi;1188 | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi; 1159 1189 cases (le_to_or_lt_eq … Hi) -Hi; #Hi 1160 [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0, short_jump〉)1161 #y #z normalize nodelta normalize nodelta >lookup_insert_miss1190 [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉) 1191 #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss 1162 1192 [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 1163 1193 | @bitvector_of_nat_abs … … 1169 1199 ] 1170 1200 | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?) 1171 [ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)1201 [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H) 1172 1202 normalize nodelta >lookup_insert_hit @jmpleq_max_length 1173 1203 | >prf >p1 >nth_append_second … … 1191 1221 | @conj [ @conj 1192 1222 [ #i #Hi // 1193 | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 1194 normalize in H 2; destruct (H2) ]1223 | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3 1224 normalize in H3; destruct (H3) ] 1195 1225 ] 1196 1226 | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ] … … 1205 1235 match n with 1206 1236 [ O ⇒ jump_expansion_start program 1207 | S m ⇒ jump_expansion_step program (jump_expansion_internal program m) 1237 | S m ⇒ let old_policy ≝ jump_expansion_internal program m in 1238 jump_expansion_step program (create_label_map program old_policy) old_policy 1208 1239 ]. 1209 1240 [ @(proj1 ?? (pi2 ?? (jump_expansion_start program))) 1210 | @(proj1 ?? (pi2 ?? (jump_expansion_step program ( jump_expansion_internal program m))))1241 | @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy))) 1211 1242 ] 1212 1243 qed. … … 1215 1246 λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy. 1216 1247 ∀n:ℕ.n < |program| → 1217 (\snd (bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,short_jump〉)) = 1218 (\snd (bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,short_jump〉)). 1248 let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in 1249 let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in 1250 j1 = j2. 1219 1251 1220 1252 lemma pe_refl: 1221 1253 ∀program.reflexive ? (policy_equal program). 1222 #program whd #x whd #n #Hn @refl 1254 #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) 1255 #y cases y -y #y #z normalize nodelta @refl 1223 1256 qed. 1224 1257 … … 1226 1259 ∀program.symmetric ? (policy_equal program). 1227 1260 #program whd #x #y #Hxy whd #n #Hn 1228 >(Hxy n Hn) @refl 1261 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) 1262 #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) 1263 #z cases z -z #y1 #y2 #y3 normalize nodelta // 1229 1264 qed. 1230 1265 1231 1266 lemma pe_trans: 1232 1267 ∀program.transitive ? (policy_equal program). 1233 #program whd #x #y #z #Hxy #Hyz whd #n #Hn 1234 >(Hxy n Hn) @(Hyz n Hn) 1268 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?); 1269 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn 1270 lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz 1271 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3 1272 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3 1273 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3 1274 normalize nodelta // 1235 1275 qed. 1236 1276 … … 1240 1280 ∧jump_in_policy program policy. 1241 1281 policy_equal program p1 p2 → 1242 policy_equal program (jump_expansion_step program p1) (jump_expansion_step program p2). 1282 policy_equal program (jump_expansion_step program (create_label_map program p1) p1) 1283 (jump_expansion_step program (create_label_map program p2) p2). 1243 1284 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H 1244 1285 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1)) … … 1248 1289 [ >lookup_opt_lookup_miss 1249 1290 [ @refl 1250 | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p2)) n Hn))1251 [ @(proj1 ?? (pi2 … (jump_expansion_step program p2)))1291 | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn)) 1292 [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2))) 1252 1293 | @Hnotjmp 1253 1294 ] 1254 1295 ] 1255 | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p1)) n Hn))1256 [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1)))1296 | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn)) 1297 [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1))) 1257 1298 | @Hnotjmp 1258 1299 ] 1259 1300 ] 1260 | #x #Hl cases daemon 1301 | #x #Hl cases daemon (* XXX *) 1261 1302 ] 1262 1303 qed. … … 1287 1328 qed. 1288 1329 1289 include "utilities/extralib.ma".1290 1291 1330 lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16). 1292 1331 ∀policy:(Σp:jump_expansion_policy. 1293 1332 (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1294 1333 jump_in_policy program p). 1295 ¬policy_equal program policy (jump_expansion_step program policy) →1334 ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) → 1296 1335 ∃n:ℕ.n < (|program|) ∧ jmple 1297 (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0, short_jump〉))1298 (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).1336 (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉)) 1337 (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)). 1299 1338 #program #policy #Hp 1300 1339 cases (dec_bounded_exists (λn.jmple 1301 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0, short_jump〉))1302 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (|program|))1340 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉)) 1341 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|)) 1303 1342 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi 1304 | #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) n Hn) 1305 [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | @Hj ] 1306 | #H @H 1343 | #abs @⊥ @(absurd ?? Hp) #n #Hn 1344 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn) 1345 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉)) 1346 cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %); 1347 #z cases z -z #x1 #x2 #x3 #Hx 1348 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)) 1349 cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %); 1350 #z cases z -z #y1 #y2 #y3 #Hy 1351 normalize nodelta #Hj cases Hj 1352 [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ] 1353 | // 1307 1354 ] 1308 1355 | #n @dec_jmple … … 1312 1359 lemma stupid: 1313 1360 ∀program,n. 1314 pi1 … (jump_expansion_step program ( jump_expansion_internal program n)) =1361 pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) = 1315 1362 pi1 … (jump_expansion_internal program (S n)). 1316 1363 // … … 1321 1368 match program with 1322 1369 [ nil ⇒ acc 1323 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0, short_jump〉)) with1370 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with 1324 1371 [ long_jump ⇒ measure_int t policy (acc + 2) 1325 1372 | medium_jump ⇒ measure_int t policy (acc + 1) … … 1328 1375 ]. 1329 1376 1330 definition measure ≝1331 λprogram.λpolicy.measure_int program policy 0. 1377 (* definition measure ≝ 1378 λprogram.λpolicy.measure_int program policy 0. *) 1332 1379 1333 1380 lemma measure_plus: ∀program.∀policy.∀x,d:ℕ. … … 1338 1385 [ // 1339 1386 | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1340 cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0, short_jump〉))1387 cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) 1341 1388 [ normalize nodelta @Hd 1342 1389 |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus … … 1351 1398 (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1352 1399 jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ. 1353 measure_int l policy acc ≤ measure_int l (jump_expansion_step program policy) acc.1400 measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc. 1354 1401 #program #policy #l elim l -l; 1355 1402 [ #Hp #acc normalize @le_n 1356 1403 | #h #t #Hind #Hp #acc 1357 cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?) 1358 [ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?); 1359 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) 1360 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉)) 1404 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp) 1405 whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?); 1406 cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3 1407 cases (bvt_lookup … (bitvector_of_nat ? (|t|)) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3 1408 normalize nodelta #Hj cases Hj 1409 [ cases x3 cases y3 1361 1410 [1,4,5,7,8,9: #H @⊥ @H 1362 1411 |2,3,6: #_ normalize nodelta 1363 [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program policy) acc))1364 |3: @(transitive_le ? (measure_int t (jump_expansion_step program policy) (acc+1)))1412 [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc)) 1413 |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1))) 1365 1414 ] 1366 1415 [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn … … 1368 1417 ] 1369 1418 ] 1370 | #Heq whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?); 1371 >Heq cases (\snd (lookup … (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉)) 1372 [ normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 1373 | normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 1374 | normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 1375 ] 1376 | @Hp 1419 | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 1377 1420 ] 1378 1421 ] … … 1384 1427 [ normalize @le_n 1385 1428 | #h #t #Hind whd in match (measure_int ???); 1386 cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0, short_jump〉))1429 cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) 1387 1430 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1388 1431 |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) … … 1409 1452 lemma measure_full: ∀program.∀policy. 1410 1453 measure_int program policy 0 = 2*|program| → ∀i.i<|program| → 1411 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0, short_jump〉)) = long_jump.1454 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump. 1412 1455 #program #policy elim program 1413 1456 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1414 1457 | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|) 1415 1458 [ whd in match (measure_int ???) in Hm; 1416 cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0, short_jump〉)) in Hm;1459 cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm; 1417 1460 normalize nodelta 1418 1461 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ … … 1426 1469 [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) 1427 1470 | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1428 cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0, short_jump〉)) in Hm;1471 cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm; 1429 1472 normalize nodelta 1430 1473 [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|))) … … 1442 1485 (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1443 1486 jump_in_policy program p. 1444 measure_int program policy 0 = measure_int program (jump_expansion_step program policy) 0 →1445 policy_equal program policy (jump_expansion_step program policy).1487 measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 → 1488 policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy). 1446 1489 #program #policy lapply (le_n (|program|)) @(list_ind ? 1447 (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program policy)) 0 →1448 policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program policy)))1490 (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 → 1491 policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy))) 1449 1492 ?? program) 1450 1493 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O … … 1452 1495 [ #Hi @Hind 1453 1496 [ @(transitive_le … Hp) // 1454 | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ?? )?) in Hm;1455 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)1497 | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm; 1498 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?) 1456 1499 [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ] 1457 | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm; 1458 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉)); 1459 normalize nodelta 1500 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm; 1501 #x cases x -x #x1 #x2 #x3 1502 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉); 1503 #y cases y -y #y1 #y2 #y3 1504 normalize nodelta cases x3 cases y3 normalize nodelta 1460 1505 [1: #H #_ @H 1461 1506 |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt … … 1475 1520 ] 1476 1521 | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1477 whd in match (measure_int ?(jump_expansion_step ?? )?) in Hm;1478 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)1522 whd in match (measure_int ?(jump_expansion_step ???)?) in Hm; 1523 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?) 1479 1524 [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ] 1480 | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm; 1481 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉)); 1482 normalize nodelta 1525 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm; 1526 #x cases x -x #x1 #x2 #x3 1527 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉); 1528 #y cases y -y #y1 #y2 #y3 1529 normalize nodelta cases x3 cases y3 normalize nodelta 1483 1530 [1,5,9: #_ #_ // 1484 1531 |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ] … … 1501 1548 | #h #t #Hind #Hp whd in match (measure_int ???); 1502 1549 cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj 1503 [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0, short_jump〉)1550 [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉) 1504 1551 [ normalize nodelta @Hind @le_S_to_le ] 1505 1552 @Hp 1506 | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0, short_jump〉)1553 | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉) 1507 1554 [ normalize nodelta @Hind @le_S_to_le ] 1508 1555 @Hp … … 1513 1560 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16). 1514 1561 Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p. 1515 #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))1562 #program @(mk_Sig … (jump_expansion_internal program (2*|program|))) 1516 1563 @(ex_intro … (2*|program|)) #k #Hk 1517 1564 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k) … … 1534 1581 [ lapply (measure_full program (jump_expansion_internal program (2*|program|))) 1535 1582 #Hfull #i #Hi 1536 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program (2*|program|)))) i Hi) 1537 >(Hfull ? i Hi) 1538 [ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*|program|))) 〈0,short_jump〉)) 1539 [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ] 1540 | #_ // 1541 ] 1542 | -i @le_to_le_to_eq 1583 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*|program|))) (jump_expansion_internal program (2*|program|)))) i Hi) 1584 lapply (Hfull ? i Hi) 1585 [ -i @le_to_le_to_eq 1543 1586 [ @measure_le 1544 1587 | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %); … … 1556 1599 ] 1557 1600 ] 1601 | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉) 1602 #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull 1603 >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉) 1604 #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 1605 [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ] 1606 | #_ // 1607 ] 1558 1608 ] 1559 1609 | @le_S_to_le @Hk 1560 1610 ] 1561 | #n @dec_bounded_forall #m @dec_eq_jump_length 1611 | #n @dec_bounded_forall #m 1612 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉) 1613 #x cases x -x #x1 #x2 #x3 1614 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉) 1615 #y cases y -y #y1 #y2 #y3 normalize nodelta 1616 @dec_eq_jump_length 1562 1617 ] 1563 1618 qed. … … 1754 1809 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix 1755 1810 (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?); 1756 @pair_elim '#ppc #pc_map #EQ3 normalize nodelta1757 @pair_elim '#pc #map #EQ4 normalize nodelta1758 @pair_elim '#l' #i' #EQ5 normalize nodelta1811 @pair_elim #ppc #pc_map #EQ3 normalize nodelta 1812 @pair_elim #pc #map #EQ4 normalize nodelta 1813 @pair_elim #l' #i' #EQ5 normalize nodelta 1759 1814 cases (construct_costs_safe ??????) normalize 1760 1815 [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
Note: See TracChangeset
for help on using the changeset viewer.