Changeset 1648
 Timestamp:
 Jan 18, 2012, 11:01:14 AM (8 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1646 r1648 118 118 qed. 119 119 120 axiom is_in_subvector_is_in_supervector: 120 lemma is_in_singleton_to_is_a: 121 ∀tag. 122 ∀element. 123 is_in … [[tag]] element → is_a tag element. 124 #tag #element 125 normalize in ⊢ (% → ?); 126 cases (is_a tag element) 127 [1: 128 normalize nodelta #irrelevant 129 @I 130 2: 131 normalize nodelta #absurd 132 cases absurd 133 ] 134 qed. 135 136 lemma is_a_decidable: 137 ∀hd. 138 ∀element. 139 is_a hd element = true ∨ is_a hd element = false. 140 #hd #element // 141 qed. 142 143 lemma mem_decidable: 144 ∀n: nat. 145 ∀v: Vector addressing_mode_tag n. 146 ∀element: addressing_mode_tag. 147 mem … eq_a n v element = true ∨ 148 mem … eq_a … v element = false. 149 #n #v #element // 150 qed. 151 152 (* 153 lemma is_in_cons_hd_tl_to_is_in_tl: 154 ∀n: nat. 155 ∀the_vect: Vector addressing_mode_tag n. 156 ∀h: addressing_mode_tag. 157 ∀element: addressing_mode. 158 is_in (S n) (h:::the_vect) element → 159 is_in n the_vect element. *) 160 161 lemma is_in_subvector_is_in_supervector: 121 162 ∀m, n: nat. 122 163 ∀subvector: Vector addressing_mode_tag m. 164 ∀supervector: Vector addressing_mode_tag n. 123 165 ∀element: addressing_mode. 124 ∀supervector: Vector addressing_mode_tag n.125 166 subvector_with … eq_a subvector supervector → 126 167 is_in m subvector element → is_in n supervector element. 168 (* 169 #m #n #subvector #supervector #element 170 elim subvector 171 [1: 172 #subvector_with_proof #is_in_proof 173 cases is_in_proof 174 2: 175 #n #hd #tl #inductive_hypothesis 176 cases supervector 177 [1: 178 #subvector_with_proof #is_in_proof 179 cases subvector_with_proof 180 2: 181 #n' #hd' #tl' #subvector_with_proof #is_in_proof 182 whd in match (is_in … (hd':::tl') element); 183 cases (is_a_decidable hd' element) 184 [1: 185 #is_a_true >is_a_true normalize nodelta 186 @I 187 2: 188 #is_a_false >is_a_false normalize nodelta 189 @inductive_hypothesis' 190 [2: 191 assumption 192 1: 193 ] 194 ] 195 ] 196 ] 197 qed. 198 3: 199 #n #hd #tl #inductive_hypothesis 200 #subvector_with_proof #is_in_proof 201 @inductive_hypothesis 202 [1: 203 assumption 204 4: 205 ] 206 qed. 207 208 209 210 [1: 211 #n #supervector #subvector_proof #is_in_proof 212 cases is_in_proof 213 2: 214 #m' #hd #tl #inductive_hypothesis #n' #supervector 215 #subvector_proof #is_in_proof 216 generalize in match is_in_proof; 217 cases(is_a_decidable hd element) 218 whd in match (is_in … (hd:::tl) element); 219 [1: 220 #is_a_true >is_a_true normalize nodelta 221 #irrelevant 222 2: 223 #is_a_false >is_a_false normalize nodelta 224 #assm 225 @inductive_hypothesis 226 [1: 227 generalize in match subvector_proof; 228 whd in match (subvector_with … eq_a (hd:::tl) supervector); 229 cases(mem_decidable n' supervector hd) 230 [1: 231 #mem_true >mem_true normalize nodelta 232 #assm assumption 233 2: 234 #mem_false >mem_false #absurd 235 cases absurd 236 ] 237 2: 238 assumption 239 ] 240 ] 241 242 243 244 245 generalize in match subvector_proof; 246 whd in match (subvector_with … eq_a (hd:::tl) supervector); 247 cases(mem_decidable n' supervector hd) 248 [1: 249 #mem_true >mem_true normalize nodelta 250 #subvector_with_proof 251 @inductive_hypothesis 252 [1: 253 assumption 254 2: 255 generalize in match is_in_proof; 256 whd in match (is_in (S m') (hd:::tl) element); 257 cases(is_a_decidable hd element) 258 [1: 259 #is_a_true >is_a_true normalize nodelta 260 #irrelevant 261 whd whd in match (is_in … tl element); 262 2: 263 #is_a_false >is_a_false normalize nodelta 264 #assm assumption 265 ] 266 ] 267 2: 268 #mem_false >mem_false normalize nodelta 269 #absurd cases absurd 270 ] 271 1: 272 normalize nodelta #subvector_with_assm 273 cases(is_a_decidable hd element) 274 [1: 275 #is_a_hd 276 generalize in match subvector_proof; 277 whd in match (subvector_with … eq_a (hd:::tl) supervector); 278 2: 279 #not_is_a_hd 280 ] 281 ] 282 ] *) 283 cases daemon 284 qed. 127 285 128 286 let rec member_addressing_mode_tag … … 538 696 λgood_program_witness: good_program code_memory program_size. 539 697 traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness. 540 698 541 699 definition compute_costs ≝ 542 700 λprogram: list Byte. 543 701 λcost_labels: BitVectorTrie costlabel 16. 544 λhas_main: bool. 545 λreachable_program_counter_witness: 546 ∀lbl: costlabel. 547 ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → 548 reachable_program_counter (load_code_memory program) (program + 1) program_counter. 702 λreachable_program_witness. 549 703 λgood_program_witness: good_program (load_code_memory program) (program + 1). 550 704 let program_size ≝ program + 1 in 551 705 let code_memory ≝ load_code_memory program in 552 traverse_code code_memory cost_labels program_size reachable_program_ counter_witness ?.706 traverse_code code_memory cost_labels program_size reachable_program_witness ?. 553 707 @good_program_witness 554 708 qed. 
src/ASM/CostsProof.ma
r1620 r1648 6 6 include alias "arithmetics/nat.ma". 7 7 include alias "basics/logic.ma". 8 9 definition current_instruction0 ≝ 10 λcode_memory: BitVectorTrie Byte 16. 11 λprogram_counter: Word. 12 \fst (\fst (fetch … code_memory program_counter)). 13 14 definition current_instruction ≝ 15 λs: Status. 16 current_instruction0 (code_memory … s) (program_counter … s). 17 18 definition ASM_classify0: instruction → status_class ≝ 19 λi: instruction. 20 match i with 21 [ RealInstruction pre ⇒ 22 match pre with 23 [ RET ⇒ cl_return 24  JZ _ ⇒ cl_jump 25  JNZ _ ⇒ cl_jump 26  JC _ ⇒ cl_jump 27  JNC _ ⇒ cl_jump 28  JB _ _ ⇒ cl_jump 29  JNB _ _ ⇒ cl_jump 30  JBC _ _ ⇒ cl_jump 31  CJNE _ _ ⇒ cl_jump 32  DJNZ _ _ ⇒ cl_jump 33  _ ⇒ cl_other 34 ] 35  ACALL _ ⇒ cl_call 36  LCALL _ ⇒ cl_call 37  JMP _ ⇒ cl_call 38  AJMP _ ⇒ cl_jump 39  LJMP _ ⇒ cl_jump 40  SJMP _ ⇒ cl_jump 41  _ ⇒ cl_other 42 ]. 43 44 definition ASM_classify: Status → status_class ≝ 45 λs: Status. 46 ASM_classify0 (current_instruction s). 8 47 9 48 let rec compute_max_trace_label_label_cost 
src/utilities/monad.ma
r1647 r1648 126 126 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f). 127 127 128 (* 128 129 check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H) 130 *) 129 131 130 132 record MonadProps : Type[1] ≝
Note: See TracChangeset
for help on using the changeset viewer.