 Timestamp:
 May 17, 2012, 12:25:41 AM (8 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1938 r1962 127 127 cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks 128 128 #classify_assm #classify_assm' @classify_assm' assumption 129 qed .129 qed. 130 130 131 131 lemma nat_of_bitvector_lt_bound: 
src/ASM/Interpret.ma
r1951 r1962 972 972 [1,2,3,4,5,6,7,8: 973 973 normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS % 974 try // 974 try // (*CSC: Veeery slow*) 975 975 s destruct(INSTR_PC) <instr_refl whd 976 976 try (#absurd normalize in absurd; try destruct(absurd) try %) % 
src/ASM/StatusProofs.ma
r1959 r1962 81 81 qed. 82 82 83 exampleget_arg_8_set_program_counter:83 lemma get_arg_8_set_program_counter: 84 84 ∀n.∀l:Vector addressing_mode_tag (S n). 85 85 ∀T,cm,s,pc,b.∀arg:l. … … 184 184 qed. *) 185 185 186 exampleset_arg_8_set_program_counter:186 lemma set_arg_8_set_program_counter: 187 187 ∀n:nat. 188 188 ∀l:Vector addressing_mode_tag (S n).
Note: See TracChangeset
for help on using the changeset viewer.