 Timestamp:
 May 27, 2011, 12:40:19 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r850 r851 2 2 include "ASM/Interpret.ma". 3 3 4 axiom append_cons_commute: 5 ∀A: Type[0]. 6 ∀l, r: list A. 7 ∀h: A. 8 l @ h::r = l @ [h] @ r. 9 10 (* 11 axiom append_associative: 12 ∀A: Type[0]. 13 ∀l, c, r: list A. 14 (l @ c) @ r = l 15 *) 16 17 let rec foldl_strong 18 (A: Type[0]) (P: list A → Prop) (l: list A) 19 (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd])) 20 (prefix: list A) (suffix: list A) (acc: P prefix) on suffix: 21 l = prefix @ suffix → P(prefix @ suffix) ≝ 22 match suffix return λl'. l = prefix @ l' → P (prefix @ l') with 23 [ nil ⇒ λprf. ? 24  cons hd tl ⇒ λprf. ? 25 ]. 26 [ > (append_nil ?) 27 @ acc 28  applyS (foldl_strong A P l H (prefix @ [hd]) tl ? ?) 29 [ @ (H prefix hd tl prf acc) 30  applyS prf 31 ] 32 ] 33 qed. 34 35 (* > append_cons_commute 36 @ 37 4 38 (* RUSSEL **) 39 40 axiom addr11_elim: 41 ∀P: Word11 → Prop. 42 (∀b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11: bool. 43 P [[ b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11]])→ 44 ∀w: Word11. P w. 45 46 (* using modified version of matita with hacked ng_refiner/nCicMetaSubst.ml *) 47 lemma test: 48 ∀i: instruction. 49 ∃pc. 50 let assembled ≝ assembly1 i in 51 let code_memory ≝ load_code_memory assembled in 52 let fetched ≝ fetch code_memory pc in 53 let 〈instr_pc, ticks〉 ≝ fetched in 54 \fst instr_pc = i. 55 # INSTR 56 % 57 [ @ (zero 16) 58  cases INSTR 59 [ #ADDR11 cases ADDR11 #ADDRX cases ADDRX 60 [18: #A #P 61 @ (addr11_elim … A) 62 *********** 63 [ normalize 64 cases B1 65 normalize; whd; 66 67 68 whd 69 normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ]) 70 letin xxx ≝ (subaddressing_modeel O [[addr11]] ADDR11) 71 normalize in xxx; 72 normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ]) 73 ] 74 ]. 5 75 6 76 include "basics/jmeq.ma". … … 552 622 ]. 553 623 554 lemma test: 555 ∀i: instruction. 556 ∃pc. 557 let assembled ≝ assembly1 i in 558 let code_memory ≝ load_code_memory assembled in 559 let fetched ≝ fetch code_memory pc in 560 let 〈instr_pc, ticks〉 ≝ fetched in 561 \fst instr_pc = i. 562 # INSTR 563 % 564 [ @ (zero 16) 565  cases INSTR 566 ]. 567 568 lemma test: 624 (* prove later *) 625 axiom test: 569 626 ∀pc: Word. 570 627 ∀code_memory: BitVectorTrie Byte 16. … … 575 632 let 〈instr, pc〉 ≝ instr_pc in 576 633 instr = i. 577 # PC # CODE_MEMORY # INSTRUCTION578 whd579 whd in ⊢ (? → match % with [ _ ⇒ ? ])580 cases (next CODE_MEMORY PC)581 whd582 # PC1 # V1583 584 585 cases (fetch CODE_MEMORY PC)586 # INSTR_PC587 # TICKS588 cases (INSTRUCTION)589 [ # ADDR11590 # ENCODING_CHECK591 whd in ENCODING_CHECK;592 normalize593 cases (INSTR_PC)594 # INSTR595 # PC596 normalize597 598 599 # ENCODING600 normalize601 [ cases INSTR_PC602 # NEW_INSTRUCTION603 # PC604 normalize605 normalize in ENCODING;606  # ASSEMBLED607 whd608 634 609 635 lemma main_thm:
Note: See TracChangeset
for help on using the changeset viewer.