Changeset 853 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 27, 2011, 1:58:21 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r852 r853 2 2 include "ASM/Interpret.ma". 3 3 4 (* 4 5 axiom append_cons_commute: 5 6 ∀A: Type[0]. … … 7 8 ∀h: A. 8 9 l @ h::r = l @ [h] @ r. 9 10 *) 10 11 (* 11 12 axiom append_associative: … … 16 17 17 18 let rec foldl_strong_internal 18 (A: Type[0]) (P: list A → Prop) (l: list A)19 (A: Type[0]) (P: list A → Type[0]) (l: list A) 19 20 (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd])) 20 21 (prefix: list A) (suffix: list A) (acc: P prefix) on suffix: … … 35 36 definition foldl_strong ≝ 36 37 λA: Type[0]. 37 λP: list A → Prop.38 λP: list A → Type[0]. 38 39 λl: list A. 39 40 λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). 40 λsuffix: list A.41 41 λacc: P [ ]. 42 foldl_strong_internal A P l H [ ] suffix acc. 43 44 definition bit_elim: ∀P: bool → bool. bool ≝ 45 λP. 46 P true ∧ P false. 47 48 definition bitvector_elim: ∀P: ∀n. BitVector n → bool. ∀n: nat. bool ≝ 49 λP. 50 λn. 51 P n. 52 53 54 55 (* > append_cons_commute 56 @ 42 foldl_strong_internal A P l H [ ] l acc (refl …). 57 43 58 44 (* RUSSEL **) 59 45 60 axiom addr11_elim:61 ∀P: Word11 → Prop.62 (∀b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11: bool.63 P [[ b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11]])→64 ∀w: Word11. P w.65 66 (* using modified version of matita with hacked ng_refiner/nCicMetaSubst.ml *)67 lemma test:68 ∀i: instruction.69 ∃pc.70 let assembled ≝ assembly1 i in71 let code_memory ≝ load_code_memory assembled in72 let fetched ≝ fetch code_memory pc in73 let 〈instr_pc, ticks〉 ≝ fetched in74 \fst instr_pc = i.75 # INSTR76 %77 [ @ (zero 16)78  cases INSTR79 [ #ADDR11 cases ADDR11 #ADDRX cases ADDRX80 [18: #A #P81 @ (addr11_elim … A)82 ***********83 [ normalize84 cases B185 normalize; whd;86 87 88 whd89 normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])90 letin xxx ≝ (subaddressing_modeel O [[addr11]] ADDR11)91 normalize in xxx;92 normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])93 ]94 ].95 46 96 47 include "basics/jmeq.ma". 48 49 notation > "hvbox(a break ≃ b)" 50 non associative with precedence 45 51 for @{ 'jmeq ? $a ? $b }. 52 53 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)" 54 non associative with precedence 45 55 for @{ 'jmeq $t $a $u $b }. 56 57 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y). 97 58 98 59 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p. … … 167 128 qed. 168 129 169 (*170 130 definition build_maps' ≝ 171 131 λpseudo_program. 172 132 let 〈preamble,instr_list〉 ≝ pseudo_program in 173 133 let result ≝ 174 foldl 175 ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))) 134 foldl_strong 176 135 (option Identifier × pseudo_instruction) 177 (λt,i. 136 (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 137 let pre' ≝ 〈preamble,pre〉 in 138 let 〈labels,pc_costs〉 ≝ res in 139 let 〈ignore,costs〉 ≝ pc_costs in 140 ∀pc. (nat_of_bitvector … pc) < length … pre → 141 lookup ?? pc labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre pc))) 142 instr_list 143 (λprefix,i,tl,prf,t. 178 144 let 〈labels, pc_costs〉 ≝ t in 179 145 let 〈program_counter, costs〉 ≝ pc_costs in … … 193 159  Some construct ⇒ 〈labels, construct〉 194 160 ] 195 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list161 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 196 162 in 197 163 let 〈labels, pc_costs〉 ≝ result in 198 164 let 〈pc, costs〉 ≝ pc_costs in 199 165 〈labels, costs〉. 200 166 [ 167  168  whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ] 169 qed. 170 171 (* 201 172 (* 202 173 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" … … 289 260 ∀A:Type[0].∀l,l1,l2:list A. 290 261 is_prefix … l l1 → is_prefix … l (l1@l2). 291 292 record Propify (A:Type[0]) : Prop ≝ { in_propify: A }. 262 axiom prefix_reflexive: ∀A,l. is_prefix A l l. 263 axiom nil_prefix: ∀A,l. is_prefix A [ ] l. 264 265 record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }. 293 266 294 267 definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝ … … 339 312 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]). 340 313 314 axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop. 315 axiom pprefix_of_append: 316 ∀A:Type[0].∀l,l1,l2. 317 is_pprefix A l l1 → is_pprefix A l (l1@l2). 318 axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l. 319 axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l. 320 321 322 axiom foldll': 323 ∀A:Type[0].∀l: list A. 324 ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0]. 325 (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') → 326 B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l). 327 #A #l #B 328 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH 329 330 331 #H #acc 332 @foldll 333 [ 334  335 ] 336 337 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]). 338 339 340 (* 341 record subset (A:Type[0]) (P: A → Prop): Type[0] ≝ 342 { subset_wit:> A; 343 subset_proof: P subset_wit 344 }. 345 *) 346 341 347 definition build_maps' ≝ 342 348 λpseudo_program. 343 349 let 〈preamble,instr_list〉 ≝ pseudo_program in 344 350 let result ≝ 345 foldl 346 (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 347 ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧ 348 tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t))) 349 (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 350 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 351 is_prefix ? instr_list_prefix' instr_list → 352 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?) 353 (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 354 ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧ 355 tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)). 356 λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 357 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 358 is_prefix ? instr_list_prefix' instr_list → 359 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? . 351 foldll 352 (option Identifier × pseudo_instruction) 353 (λprefix. 354 Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 355 match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?]) 356 (λprefix,t,i. 360 357 let 〈labels, pc_costs〉 ≝ t in 361 358 let 〈program_counter, costs〉 ≝ pc_costs in … … 375 372  Some construct ⇒ 〈labels, construct〉 376 373 ] 377 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)374 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list 378 375 in 379 376 let 〈labels, pc_costs〉 ≝ result in 380 377 let 〈pc, costs〉 ≝ pc_costs in 381 378 〈labels, costs〉. 379 [ 380  @⊥ 381  normalize % // 382 ] 383 qed. 382 384 383 385 definition build_maps' ≝
Note: See TracChangeset
for help on using the changeset viewer.