- Timestamp:
- Jun 7, 2011, 2:56:39 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r889 r890 698 698 qed. 699 699 700 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) 701 (encoding: list Byte) on encoding: Prop ≝ 702 match encoding with 703 [ nil ⇒ final_pc = pc 704 | cons hd tl ⇒ 705 let 〈new_pc, byte〉 ≝ next code_memory pc in 706 hd = byte ∧ encoding_check code_memory new_pc final_pc tl 707 ]. 708 709 axiom eq_bv_refl: ∀n,v. eq_bv n v v = true. 710 711 (* 700 712 lemma test: 701 713 ∀pc,i. … … 705 717 let 〈instr_pc, ticks〉 ≝ fetched in 706 718 eq_instruction (\fst instr_pc)) i = true. 707 #pc #i cases i #arg try #arg2 whd in ⊢ (??%?) 719 *) 720 lemma test: 721 ∀pc,i,code_memory. 722 let assembled ≝ assembly1 i in 723 let len ≝ length … assembled in 724 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 725 let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in 726 let 〈instr_pc, ticks〉 ≝ fetched in 727 let 〈instr,pc'〉 ≝ instr_pc in 728 (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. 729 #pc #i #code_memory cases i [8: *] 730 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] 731 [47,48,49: |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg 732 [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58, 733 59,60,63,64,65,66,67: #ARG] 734 [1: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2 735 736 [7: #arg2] 737 738 whd 739 [ @(list_addressing_mode_tags_elim_prop … arg) whd try % 740 @(list_addressing_mode_tags_elim_prop … arg2) whd try % 741 * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??) 742 whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 >eq_instruction_refl @eq_bv_refl 743 |6: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX 744 * #H1 * #H2 #H3 whd in H3; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??) 745 whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 <H3 >eq_instruction_refl @eq_bv_refl 746 |7: @(list_addressing_mode_tags_elim_prop … arg) whd try % 747 * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??) 748 |3,5: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX 749 750 @split_elim 751 752 753 whd in ⊢ (??%?) 708 754 [2,4: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX 709 755 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) … … 1297 1343 | 1298 1344 1299 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)1300 (encoding: list Byte) on encoding: Prop ≝1301 match encoding with1302 [ nil ⇒ final_pc = pc1303 | cons hd tl ⇒1304 let 〈new_pc, byte〉 ≝ next code_memory pc in1305 hd = byte ∧ encoding_check code_memory new_pc final_pc tl1306 ].1307 1308 1345 definition assembly_specification: 1309 1346 ∀assembly_program: pseudo_assembly_program.
Note: See TracChangeset
for help on using the changeset viewer.