Changeset 1591
 Timestamp:
 Dec 6, 2011, 5:24:45 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 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) 
src/ASM/Fetch.ma
r1555 r1591 3 3 include "ASM/ASM.ma". 4 4 5 definition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝ 6 λpmem: BitVectorTrie Byte 16. 7 λpc: Word. 8 〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉. 5 definition bitvector_max_nat ≝ 6 λlength: nat. 7 2^length. 8 9 definition code_memory_size ≝ bitvector_max_nat 16. 10 11 include "ASM/JMCoercions.ma". 12 13 axiom bitvector_lt_bitvector_max_nat: 14 ∀length: nat. 15 ∀v: BitVector length. 16 nat_of_bitvector length v < bitvector_max_nat length. 17 18 lemma word_lt_bitvector_max_nat: 19 ∀w: Word. 20 nat_of_bitvector … w < code_memory_size. 21 #w // 22 qed. 23 24 axiom w_lt_half_add_increment: 25 ∀length: nat. 26 ∀v: BitVector length. 27 ∀proof: nat_of_bitvector … v < bitvector_max_nat length  1. 28 nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))). 29 30 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. 31 nat_of_bitvector … program_counter < (code_memory_size  1) → 32 Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ≝ 33 λpmem: BitVectorTrie Byte 16. 34 λpc: Word. 35 λproof. 36 〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉. 37 @w_lt_half_add_increment @proof 38 qed. 9 39 10 40 (* timings taken from SIEMENS *) 11 41 12 definition fetch0: BitVectorTrie Byte 16 → Word × Byte → instruction × Word × nat ≝ 13 λpmem: BitVectorTrie Byte 16. 14 λpc_v. 15 let 〈pc,v〉 ≝ pc_v in 42 definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte → 43 nat_of_bitvector … program_counter < code_memory_size  24 (* 3 bytes *) → 44 Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝ 45 λpmem. 46 λpc. 47 λv. 48 λproof. 16 49 let 〈b,v〉 ≝ head … v in if b then 17 50 let 〈b,v〉 ≝ head … v in if b then … … 26 59 else 27 60 let 〈b,v〉≝ head … v in if b then 28 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉61 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉 29 62 else 30 63 〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉 … … 34 67 else 35 68 let 〈b,v〉≝ head … v in if b then 36 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉69 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 37 70 else 38 71 〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉 … … 46 79 else 47 80 let 〈b,v〉≝ head … v in if b then 48 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉81 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉 49 82 else 50 83 〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉 … … 54 87 else 55 88 let 〈b,v〉≝ head … v in if b then 56 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉89 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 57 90 else 58 91 〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉 … … 60 93 let 〈b,v〉≝ head … v in if b then 61 94 let 〈b,v〉≝ head … v in if b then 62 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉95 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉 63 96 else 64 97 let 〈b,v〉≝ head … v in if b then … … 67 100 else 68 101 let 〈b,v〉≝ head … v in if b then 69 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉102 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉 70 103 else 71 104 〈〈RealInstruction (DA … ACC_A), pc〉, 1〉 … … 75 108 〈〈RealInstruction (SETB … CARRY), pc〉, 1〉 76 109 else 77 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉78 else 79 let 〈b,v〉≝ head … v in if b then 80 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉81 else 82 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉110 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉 111 else 112 let 〈b,v〉≝ head … v in if b then 113 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 114 else 115 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉 83 116 else 84 117 let 〈b,v〉≝ head … v in if b then … … 90 123 else 91 124 let 〈b,v〉≝ head … v in if b then 92 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉125 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉 93 126 else 94 127 〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉 … … 98 131 〈〈RealInstruction (CLR … CARRY), pc〉, 1〉 99 132 else 100 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉101 else 102 let 〈b,v〉≝ head … v in if b then 103 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉104 else 105 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉133 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉 134 else 135 let 〈b,v〉≝ head … v in if b then 136 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 137 else 138 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉 106 139 else 107 140 let 〈b,v〉≝ head … v in if b then 108 141 let 〈b,v〉≝ head … v in if b then 109 142 let 〈b,v〉≝ head … v in if b then 110 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉111 else 112 let 〈b,v〉≝ head … v in if b then 113 let 〈b,v〉≝ head … v in if b then 114 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉115 else 116 let 〈b,v〉≝ head … v in if b then 117 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉118 else 119 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉143 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 144 else 145 let 〈b,v〉≝ head … v in if b then 146 let 〈b,v〉≝ head … v in if b then 147 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉 148 else 149 let 〈b,v〉≝ head … v in if b then 150 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 151 else 152 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 120 153 else 121 154 let 〈b,v〉≝ head … v in if b then … … 123 156 〈〈RealInstruction (CPL … CARRY), pc〉, 1〉 124 157 else 125 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉126 else 127 let 〈b,v〉≝ head … v in if b then 128 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉129 else 130 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉131 else 132 let 〈b,v〉≝ head … v in if b then 133 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉134 else 135 let 〈b,v〉≝ head … v in if b then 136 let 〈b,v〉≝ head … v in if b then 137 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉158 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉 159 else 160 let 〈b,v〉≝ head … v in if b then 161 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 162 else 163 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 164 else 165 let 〈b,v〉≝ head … v in if b then 166 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉 167 else 168 let 〈b,v〉≝ head … v in if b then 169 let 〈b,v〉≝ head … v in if b then 170 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉 138 171 else 139 172 〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉 … … 143 176 〈〈RealInstruction (INC … DPTR), pc〉, 2〉 144 177 else 145 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉146 else 147 let 〈b,v〉≝ head … v in if b then 148 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉149 else 150 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉178 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉 179 else 180 let 〈b,v〉≝ head … v in if b then 181 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 182 else 183 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 151 184 else 152 185 let 〈b,v〉≝ head … v in if b then … … 159 192 else 160 193 let 〈b,v〉≝ head … v in if b then 161 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉162 else 163 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉194 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉 195 else 196 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉 164 197 else 165 198 let 〈b,v〉≝ head … v in if b then … … 167 200 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉 168 201 else 169 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉170 else 171 let 〈b,v〉≝ head … v in if b then 172 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉173 else 174 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉175 else 176 let 〈b,v〉≝ head … v in if b then 177 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉178 else 179 let 〈b,v〉≝ head … v in if b then 180 let 〈b,v〉≝ head … v in if b then 181 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉182 else 183 let 〈b,v〉≝ head … v in if b then 184 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉202 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉 203 else 204 let 〈b,v〉≝ head … v in if b then 205 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 206 else 207 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉 208 else 209 let 〈b,v〉≝ head … v in if b then 210 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉 211 else 212 let 〈b,v〉≝ head … v in if b then 213 let 〈b,v〉≝ head … v in if b then 214 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉 215 else 216 let 〈b,v〉≝ head … v in if b then 217 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉 185 218 else 186 219 〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉 … … 190 223 〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉 191 224 else 192 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉193 else 194 let 〈b,v〉≝ head … v in if b then 195 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉196 else 197 let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉225 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 226 else 227 let 〈b,v〉≝ head … v in if b then 228 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 229 else 230 let 〈pc,b1〉≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉 198 231 else 199 232 let 〈b,v〉≝ head … v in if b then … … 201 234 let 〈b,v〉≝ head … v in if b then 202 235 let 〈b,v〉≝ head … v in if b then 203 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉204 else 205 let 〈b,v〉≝ head … v in if b then 206 let 〈b,v〉≝ head … v in if b then 207 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉208 else 209 let 〈b,v〉≝ head … v in if b then 210 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉211 else 212 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉236 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉 237 else 238 let 〈b,v〉≝ head … v in if b then 239 let 〈b,v〉≝ head … v in if b then 240 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉 241 else 242 let 〈b,v〉≝ head … v in if b then 243 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉 244 else 245 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉 213 246 else 214 247 let 〈b,v〉≝ head … v in if b then … … 216 249 〈〈JMP … INDIRECT_DPTR, pc〉, 2〉 217 250 else 218 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉219 else 220 let 〈b,v〉≝ head … v in if b then 221 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉222 else 223 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉251 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 252 else 253 let 〈b,v〉≝ head … v in if b then 254 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 255 else 256 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉 224 257 else 225 258 let 〈b,v〉≝ head … v in if b then … … 231 264 else 232 265 let 〈b,v〉≝ head … v in if b then 233 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉234 else 235 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉236 else 237 let 〈b,v〉≝ head … v in if b then 238 let 〈b,v〉≝ head … v in if b then 239 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉240 else 241 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉242 else 243 let 〈b,v〉≝ head … v in if b then 244 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉245 else 246 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉266 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 267 else 268 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 269 else 270 let 〈b,v〉≝ head … v in if b then 271 let 〈b,v〉≝ head … v in if b then 272 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 273 else 274 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 275 else 276 let 〈b,v〉≝ head … v in if b then 277 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 278 else 279 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉 247 280 else 248 281 let 〈b,v〉≝ head … v in if b then … … 255 288 else 256 289 let 〈b,v〉≝ head … v in if b then 257 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉258 else 259 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉260 else 261 let 〈b,v〉≝ head … v in if b then 262 let 〈b,v〉≝ head … v in if b then 263 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉264 else 265 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉266 else 267 let 〈b,v〉≝ head … v in if b then 268 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉269 else 270 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉290 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 291 else 292 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 293 else 294 let 〈b,v〉≝ head … v in if b then 295 let 〈b,v〉≝ head … v in if b then 296 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 297 else 298 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 299 else 300 let 〈b,v〉≝ head … v in if b then 301 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 302 else 303 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉 271 304 else 272 305 let 〈b,v〉≝ head … v in if b then … … 278 311 else 279 312 let 〈b,v〉≝ head … v in if b then 280 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉281 else 282 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉283 else 284 let 〈b,v〉≝ head … v in if b then 285 let 〈b,v〉≝ head … v in if b then 286 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉287 else 288 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉289 else 290 let 〈b,v〉≝ head … v in if b then 291 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉292 else 293 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉313 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 314 else 315 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 316 else 317 let 〈b,v〉≝ head … v in if b then 318 let 〈b,v〉≝ head … v in if b then 319 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 320 else 321 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 322 else 323 let 〈b,v〉≝ head … v in if b then 324 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 325 else 326 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉 294 327 else 295 328 let 〈b,v〉≝ head … v in if b then … … 303 336 else 304 337 let 〈b,v〉≝ head … v in if b then 305 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉306 else 307 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉338 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉 339 else 340 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉 308 341 else 309 342 let 〈b,v〉≝ head … v in if b then … … 314 347 else 315 348 let 〈b,v〉≝ head … v in if b then 316 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉317 else 318 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉349 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 350 else 351 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 319 352 else 320 353 let 〈b,v〉≝ head … v in if b then … … 326 359 else 327 360 let 〈b,v〉≝ head … v in if b then 328 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉329 else 330 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉361 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉 362 else 363 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉 331 364 else 332 365 let 〈b,v〉≝ head … v in if b then … … 337 370 else 338 371 let 〈b,v〉≝ head … v in if b then 339 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉340 else 341 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉372 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 373 else 374 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 342 375 else 343 376 let 〈b,v〉≝ head … v in if b then … … 350 383 else 351 384 let 〈b,v〉≝ head … v in if b then 352 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉385 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉 353 386 else 354 387 〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉 … … 358 391 〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉 359 392 else 360 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉361 else 362 let 〈b,v〉≝ head … v in if b then 363 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉364 else 365 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉393 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 394 else 395 let 〈b,v〉≝ head … v in if b then 396 let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 397 else 398 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 366 399 else 367 400 let 〈b,v〉≝ head … v in if b then … … 373 406 else 374 407 let 〈b,v〉≝ head … v in if b then 375 let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉408 let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉 376 409 else 377 410 〈〈RealInstruction (INC … ACC_A), pc〉, 1〉 … … 381 414 〈〈RealInstruction (RR … ACC_A), pc〉, 1〉 382 415 else 383 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pcin 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉384 else 385 let 〈b,v〉≝ head … v in if b then 386 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉416 let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 417 else 418 let 〈b,v〉≝ head … v in if b then 419 let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 387 420 else 388 421 〈〈RealInstruction (NOP …), pc〉, 1〉. 389 %. 422 try % 423 cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *) 390 424 qed. 391 425 392 definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝ 393 λpmem: BitVectorTrie Byte 16. 394 λpc: Word. 395 fetch0 pmem (next pmem pc). 426 definition fetch: BitVectorTrie Byte 16 → ∀program_counter: Word. 427 Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝ 428 λpmem: BitVectorTrie Byte 16. 429 λpc: Word. 430 let 〈word, byte〉 ≝ next pmem pc ? in 431 fetch0 pmem word byte ?. 432 cases daemon (* XXX: todo, proofs about size of pc *) 433 qed.
Note: See TracChangeset
for help on using the changeset viewer.