Changeset 1919
 Timestamp:
 May 7, 2012, 11:12:13 AM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1916 r1919 79 79 let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in 80 80 reachable_program_counter code_memory total_program_size jump_target 81 (*match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with82 [ ADDR11 addr ⇒ λaddr11: True.83 let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in84 let 〈nu, nl〉 ≝ split … 4 4 pc_bu in85 let bit ≝ get_index' … O ? nl in86 let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in87 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in88 let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in89 reachable_program_counter code_memory total_program_size new_program_counter90  _ ⇒ λother: False. ⊥91 ] (subaddressing_modein … addr) *)92 81  LJMP addr ⇒ 93 82 let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in 94 83 reachable_program_counter code_memory total_program_size jump_target 95 (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with96 [ ADDR16 addr ⇒ λaddr16: True.97 reachable_program_counter code_memory total_program_size addr98  _ ⇒ λother: False. ⊥99 ] (subaddressing_modein … addr)*)100 84  SJMP addr ⇒ 101 85 let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in 102 86 reachable_program_counter code_memory total_program_size jump_target 103 (*match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with104 [ RELATIVE addr ⇒ λrelative: True.105 let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in106 reachable_program_counter code_memory total_program_size new_program_counter107  _ ⇒ λother: False. ⊥108 ] (subaddressing_modein … addr)*)109 87  JMP addr ⇒ (* XXX: JMP is used for fptrs and unconstrained *) 110 88 nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ … … 134 112 let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in 135 113 program_counter ? code_memory after = program_counter_after. 136 (* XXX: why defined like this?137 let size ≝ current_instruction_cost code_memory before in138 let pc_before ≝ program_counter … code_memory before in139 let pc_after ≝ program_counter … code_memory after in140 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in141 sum = pc_after.142 *)143 114 144 115 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝ … … 148 119 (Status code_memory) 149 120 (λs,s'. (execute_1 … s) = s') 121 ? 122 ? 150 123 (λs,class. ASM_classify … s = class) 151 124 (current_instruction_is_labelled … cost_labels) 152 (next_instruction_properly_relates_program_counters code_memory). 125 (next_instruction_properly_relates_program_counters code_memory) 126 ?. 127 cases daemon (* XXX: new additions to abstract status record *) 128 qed. 153 129 154 130 let rec trace_any_label_length … … 172 148 ]. 173 149 174 let rec trace_any_label_length' 175 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 176 (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) 177 (final_status: Status code_memory) 178 (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) 179 on the_trace: nat ≝ 180 match the_trace with 181 [ tal_base_not_return the_status _ _ _ _ ⇒ 1 182  tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 1 183  tal_base_return the_status _ _ _ ⇒ 1 184  tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒ 185 let tail_length ≝ trace_any_label_length' … final_trace in 186 S tail_length 187  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 188 let tail_length ≝ trace_any_label_length' … tail_trace in 189 S tail_length 190 ]. 150 definition trace_any_label_length' ≝ 151 λcode_memory: BitVectorTrie Byte 16. 152 λcost_labels: BitVectorTrie costlabel 16. 153 λtrace_ends_flag: trace_ends_with_ret. 154 λstart_status: Status code_memory. 155 λfinal_status: Status code_memory. 156 λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status. 157 as_trace_any_label_length' … the_trace. 191 158 192 159 let rec compute_paid_trace_any_label … … 618 585 @plus_right_monotone whd in ⊢ (???%); <FETCH % 619 586 2: 620 normalize in size_invariant; 621 lapply (le_S_S_to_le … size_invariant) 622 #assm assumption 587 @le_S_S_to_le @size_invariant 623 588 3: 624 589 % … … 1194 1159 inverter nat_jmdiscr for nat. 1195 1160 1196 (* XXX: this is false in the general case. For instance, if n = 0 then the1197 base case requires us prove 1 = 0, as it is the carry bit that holds1198 the result of the addition. *)1199 axiom succ_nat_of_bitvector_half_add_1:1200 ∀n: nat.1201 ∀bv: BitVector n.1202 ∀power_proof: nat_of_bitvector … bv < 2^n  1.1203 S (nat_of_bitvector … bv) = nat_of_bitvector …1204 (\snd (half_add n (bitvector_of_nat … 1) bv)).1205 1206 1161 lemma plus_lt_to_lt: 1207 1162 ∀m, n, o: nat. … … 1245 1200 lapply (injective_S … absurd) absurd #absurd 1246 1201 /2/ 1247 ]1248 qed.1249 1250 lemma generalized_nat_cases:1251 ∀n: nat.1252 n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m).1253 #n1254 cases n1255 [1:1256 @or_introl @or_introl %1257 2:1258 #n' cases n'1259 [1:1260 @or_introl @or_intror %1261 2:1262 #n'' @or_intror %{n''} %1263 ]1264 1202 ] 1265 1203 qed. 
src/ASM/ASMCostsSplit.ma
r1899 r1919 41 41 λ${ident E}.$s ] ] (refl ? $t) }. 42 42 43 lemma succ_nat_of_bitvector_aux_half_add_1: 44 ∀n: nat. 45 ∀bv: BitVector n. 46 ∀buffer: nat. 47 ∀power_proof: nat_of_bitvector … bv < 2^n  1. 48 S (nat_of_bitvector_aux n buffer bv) = 49 nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)). 50 #n #bv elim bv 51 [1: 52 #buffer normalize #absurd 53 cases (lt_to_not_zero … absurd) 54 2: 55 #n' #hd #tl #inductive_hypothesis #buffer 56 cases daemon 57 ] 58 qed. 59 60 lemma succ_nat_of_bitvector_half_add_1: 61 ∀n: nat. 62 ∀bv: BitVector n. 63 ∀power_proof: nat_of_bitvector … bv < 2^n  1. 64 S (nat_of_bitvector … bv) = nat_of_bitvector … 65 (\snd (half_add n (bitvector_of_nat … 1) bv)). 66 #n #bv elim bv 67 [1: 68 normalize #absurd 69 cases (lt_to_not_zero … absurd) 70 2: 71 #n' #hd #tl #inductive_hypothesis 72 cases daemon 73 ] 74 qed. 75 43 76 let rec traverse_code_internal 44 77 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 
src/ASM/CostsProof.ma
r1910 r1919 677 677 cases (block_cost ? ? ? ? ? ?) 678 678 #cost block_cost_assm #block_cost_assm 679 cases (block_cost_assm ? ? ? trace_any_label (refl …)) % 679 cases (block_cost_assm ? ? ? trace_any_label ? (refl …)) 680 try % (* XXX: assumption about length of trace *) cases daemon 680 681 ] 681 682 ]
Note: See TracChangeset
for help on using the changeset viewer.