Changeset 1591 for src/ASM/ASMCosts.ma
- Timestamp:
- Dec 6, 2011, 5:24:45 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1587 r1591 72 72 mk_abstract_status 73 73 Status 74 (λs,s'. eject …(execute_1 s) = s')74 (λs,s'. (execute_1 s) = s') 75 75 (λs,class. ASM_classify s = class) 76 76 (current_instruction_is_labelled cost_labels) … … 91 91 // 92 92 qed. 93 94 axiom size:95 ∀a: Type[0].96 ∀n: nat.97 BitVectorTrie Byte 16 → nat.98 99 (* XXX: need some precondition about pc not being too "big" to avoid overflow *)100 axiom fetch_pc_lt_new_pc:101 ∀mem: BitVectorTrie Byte 16.102 ∀pc: Word.103 ∀proof: nat_of_bitvector … pc < size Byte 16 mem.104 nat_of_bitvector … pc < nat_of_bitvector … (\snd (\fst (fetch … mem pc))).105 93 106 94 axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o: … … 108 96 m - n ≤ m - S o → S m - n ≤ m - o. 109 97 110 axiomstrengthened_invariant:98 lemma strengthened_invariant: 111 99 ∀code_memory: BitVectorTrie Byte 16. 112 ∀program_size: nat. 113 ∀code_memory_size: nat. 100 ∀total_program_size: nat. 114 101 ∀new_program_counter: Word. 115 102 ∀program_counter: Word. 116 code_memory_size ≤ size Byte 16 code_memory → 117 program_size < code_memory_size → 118 let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … program_size))) in 103 total_program_size ≤ code_memory_size → 104 let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in 119 105 Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) → 120 106 new_program_counter = \snd (\fst (fetch … code_memory program_counter)) → 121 nat_of_bitvector … program_counter < program_size → 122 nat_of_bitvector … new_program_counter < program_size. 107 nat_of_bitvector … program_counter ≤ total_program_size → 108 nat_of_bitvector … new_program_counter ≤ total_program_size. 109 #code_memory #total_program_size #new_program_counter #program_counter 110 #relation_total_program_code_memory_size #end_instruction_is_ok 111 #new_program_counter_from_fetch #program_counter_within_program 112 >new_program_counter_from_fetch 113 lapply (sig2 ? ? (fetch code_memory program_counter)) #assm 114 123 115 124 116 (* XXX: use memoisation here in the future *) 125 117 let rec block_cost 126 118 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 127 (program_counter: Word) (program_size: nat) ( code_memory_size: nat)128 (size_invariant: code_memory_size ≤ size Byte 16 code_memory)129 (pc_invariant: nat_of_bitvector … program_counter < code_memory_size)119 (program_counter: Word) (program_size: nat) (total_program_size: nat) 120 (size_invariant: total_program_size ≤ code_memory_size) 121 (pc_invariant: nat_of_bitvector … program_counter < total_program_size) 130 122 (final_instr_invariant: 131 let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … initial_program_size))) in123 let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in 132 124 Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return)) 133 on program_size: initial_program_size - nat_of_bitvector … program_counter < program_size → nat ≝134 match program_size return λprogram_size: nat. initial_program_size - nat_of_bitvector … program_counter < program_size → nat with125 on program_size: total_program_size - nat_of_bitvector … program_counter < program_size → nat ≝ 126 match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter < program_size → nat with 135 127 [ O ⇒ λabsurd. ⊥ 136 128 | S program_size ⇒ λrecursive_case. 137 let ticks ≝ \snd (fetch … code_memory p c) in138 let instr ≝ \fst (\fst (fetch … mem pc)) in139 let newpc ≝ \snd (\fst (fetch … mem pc)) in129 let ticks ≝ \snd (fetch … code_memory program_counter) in 130 let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in 131 let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in 140 132 match lookup_opt … newpc cost_labels return λx: option costlabel. nat with 141 133 [ None ⇒ … … 143 135 match classify return λx. ∀classify_refl: x = classify. nat with 144 136 [ cl_jump ⇒ λclassify_refl. ticks 145 | cl_call ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)137 | cl_call ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 146 138 | cl_return ⇒ λclassify_refl. ticks 147 | cl_other ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)139 | cl_other ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 148 140 ] (refl … classify) 149 141 | Some _ ⇒ ticks … … 153 145 cases(lt_to_not_zero … absurd) 154 146 |2,4: 155 cut(nat_of_bitvector … p c< nat_of_bitvector … newpc)147 cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc) 156 148 [1,3: 157 @fetch_pc_lt_new_pc 149 @fetch_pc_lt_new_pc (* XXX: now @sig2 from fetch's russell type *) 158 150 lapply(transitive_lt 159 151 (nat_of_bitvector 16 pc)
Note: See TracChangeset
for help on using the changeset viewer.