[1486] | 1 | include "ASM/ASM.ma". |
---|
| 2 | include "ASM/Arithmetic.ma". |
---|
| 3 | include "ASM/Fetch.ma". |
---|
| 4 | include "ASM/Interpret.ma". |
---|
[1560] | 5 | include "common/StructuredTraces.ma". |
---|
[1486] | 6 | |
---|
[1642] | 7 | let rec fetch_program_counter_n |
---|
| 8 | (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word) |
---|
| 9 | on n: option Word ≝ |
---|
| 10 | match n with |
---|
| 11 | [ O ⇒ Some … program_counter |
---|
| 12 | | S n ⇒ |
---|
| 13 | match fetch_program_counter_n n code_memory program_counter with |
---|
| 14 | [ None ⇒ None … |
---|
| 15 | | Some tail_pc ⇒ |
---|
| 16 | let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in |
---|
| 17 | if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then |
---|
| 18 | Some … program_counter |
---|
| 19 | else |
---|
| 20 | None Word (* XXX: overflow! *) |
---|
| 21 | ] |
---|
| 22 | ]. |
---|
[1621] | 23 | |
---|
[1642] | 24 | definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝ |
---|
[1621] | 25 | λcode_memory: BitVectorTrie Byte 16. |
---|
[1639] | 26 | λprogram_size: nat. |
---|
[1621] | 27 | λprogram_counter: Word. |
---|
[1642] | 28 | (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧ |
---|
| 29 | nat_of_bitvector 16 program_counter < program_size. |
---|
[1639] | 30 | |
---|
[1642] | 31 | definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝ |
---|
[1621] | 32 | λcode_memory: BitVectorTrie Byte 16. |
---|
| 33 | λtotal_program_size: nat. |
---|
[1642] | 34 | ∀program_counter: Word. |
---|
| 35 | ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. |
---|
| 36 | let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in |
---|
[1621] | 37 | match instruction with |
---|
| 38 | [ RealInstruction instr ⇒ |
---|
| 39 | match instr with |
---|
| 40 | [ RET ⇒ True |
---|
| 41 | | JC relative ⇒ True (* XXX: see below *) |
---|
| 42 | | JNC relative ⇒ True (* XXX: see below *) |
---|
| 43 | | JB bit_addr relative ⇒ True |
---|
| 44 | | JNB bit_addr relative ⇒ True |
---|
| 45 | | JBC bit_addr relative ⇒ True |
---|
| 46 | | JZ relative ⇒ True |
---|
| 47 | | JNZ relative ⇒ True |
---|
| 48 | | CJNE src_trgt relative ⇒ True |
---|
| 49 | | DJNZ src_trgt relative ⇒ True |
---|
| 50 | | _ ⇒ |
---|
[1642] | 51 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
| 52 | nat_of_bitvector … program_counter' < total_program_size |
---|
[1621] | 53 | ] |
---|
| 54 | | LCALL addr ⇒ |
---|
| 55 | match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with |
---|
| 56 | [ ADDR16 addr ⇒ λaddr16: True. |
---|
[1642] | 57 | reachable_program_counter code_memory total_program_size addr ∧ |
---|
| 58 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
| 59 | nat_of_bitvector … program_counter' < total_program_size |
---|
[1621] | 60 | | _ ⇒ λother: False. ⊥ |
---|
| 61 | ] (subaddressing_modein … addr) |
---|
| 62 | | ACALL addr ⇒ |
---|
| 63 | match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with |
---|
| 64 | [ ADDR11 addr ⇒ λaddr11: True. |
---|
[1642] | 65 | let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in |
---|
[1621] | 66 | let 〈thr, eig〉 ≝ split … 3 8 addr in |
---|
| 67 | let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in |
---|
| 68 | let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in |
---|
[1642] | 69 | reachable_program_counter code_memory total_program_size new_program_counter ∧ |
---|
| 70 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
| 71 | nat_of_bitvector … program_counter' < total_program_size |
---|
[1621] | 72 | | _ ⇒ λother: False. ⊥ |
---|
| 73 | ] (subaddressing_modein … addr) |
---|
| 74 | | AJMP addr ⇒ |
---|
| 75 | match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with |
---|
| 76 | [ ADDR11 addr ⇒ λaddr11: True. |
---|
[1642] | 77 | let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in |
---|
[1621] | 78 | let 〈nu, nl〉 ≝ split … 4 4 pc_bu in |
---|
| 79 | let bit ≝ get_index' … O ? nl in |
---|
| 80 | let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in |
---|
| 81 | let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in |
---|
| 82 | let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in |
---|
[1642] | 83 | reachable_program_counter code_memory total_program_size new_program_counter |
---|
[1621] | 84 | | _ ⇒ λother: False. ⊥ |
---|
| 85 | ] (subaddressing_modein … addr) |
---|
| 86 | | LJMP addr ⇒ |
---|
| 87 | match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with |
---|
| 88 | [ ADDR16 addr ⇒ λaddr16: True. |
---|
[1642] | 89 | reachable_program_counter code_memory total_program_size addr |
---|
[1621] | 90 | | _ ⇒ λother: False. ⊥ |
---|
| 91 | ] (subaddressing_modein … addr) |
---|
| 92 | | SJMP addr ⇒ |
---|
| 93 | match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with |
---|
| 94 | [ RELATIVE addr ⇒ λrelative: True. |
---|
[1642] | 95 | let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in |
---|
| 96 | reachable_program_counter code_memory total_program_size new_program_counter |
---|
[1621] | 97 | | _ ⇒ λother: False. ⊥ |
---|
| 98 | ] (subaddressing_modein … addr) |
---|
[1645] | 99 | | JMP addr ⇒ (* XXX: JMP is used for fptrs and unconstrained *) |
---|
| 100 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
| 101 | nat_of_bitvector … program_counter' < total_program_size |
---|
[1621] | 102 | | MOVC src trgt ⇒ |
---|
[1642] | 103 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
| 104 | nat_of_bitvector … program_counter' < total_program_size |
---|
[1621] | 105 | ]. |
---|
| 106 | cases other |
---|
| 107 | qed. |
---|
[1597] | 108 | |
---|
[1646] | 109 | lemma is_in_tl_to_is_in_cons_hd_tl: |
---|
[1624] | 110 | ∀n: nat. |
---|
| 111 | ∀the_vect: Vector addressing_mode_tag n. |
---|
| 112 | ∀h: addressing_mode_tag. |
---|
| 113 | ∀element: addressing_mode. |
---|
| 114 | is_in n the_vect element → is_in (S n) (h:::the_vect) element. |
---|
| 115 | #n #the_vect #h #element #assm |
---|
| 116 | normalize cases (is_a h element) normalize nodelta |
---|
| 117 | // |
---|
| 118 | qed. |
---|
| 119 | |
---|
[1646] | 120 | axiom is_in_subvector_is_in_supervector: |
---|
[1625] | 121 | ∀m, n: nat. |
---|
| 122 | ∀subvector: Vector addressing_mode_tag m. |
---|
[1646] | 123 | ∀element: addressing_mode. |
---|
[1625] | 124 | ∀supervector: Vector addressing_mode_tag n. |
---|
| 125 | subvector_with … eq_a subvector supervector → |
---|
| 126 | is_in m subvector element → is_in n supervector element. |
---|
| 127 | |
---|
[1622] | 128 | let rec member_addressing_mode_tag |
---|
| 129 | (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) |
---|
| 130 | on v: Prop ≝ |
---|
| 131 | match v with |
---|
| 132 | [ VEmpty ⇒ False |
---|
| 133 | | VCons n' hd tl ⇒ |
---|
[1623] | 134 | bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a |
---|
[1622] | 135 | ]. |
---|
| 136 | |
---|
| 137 | let rec subaddressing_mode_elim_type |
---|
[1625] | 138 | (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m) |
---|
[1622] | 139 | (Q: addressing_mode → T → Prop) |
---|
[1625] | 140 | (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T) |
---|
| 141 | (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T) |
---|
| 142 | (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T) |
---|
| 143 | (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T) |
---|
| 144 | (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T) |
---|
| 145 | (p_acc_a: is_in m fixed_v ACC_A → T) |
---|
| 146 | (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T) |
---|
| 147 | (p_acc_b: is_in m fixed_v ACC_B → T) |
---|
| 148 | (p_dptr: is_in m fixed_v DPTR → T) |
---|
| 149 | (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T) |
---|
| 150 | (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T) |
---|
| 151 | (p_acc_dptr: is_in m fixed_v ACC_DPTR → T) |
---|
| 152 | (p_acc_pc: is_in m fixed_v ACC_PC → T) |
---|
| 153 | (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T) |
---|
| 154 | (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T) |
---|
| 155 | (p_carry: is_in m fixed_v CARRY → T) |
---|
| 156 | (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T) |
---|
| 157 | (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T) |
---|
| 158 | (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T) |
---|
| 159 | (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) |
---|
| 160 | on v: Prop ≝ |
---|
| 161 | match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with |
---|
[1623] | 162 | [ VEmpty ⇒ λm_refl. λv_refl. |
---|
[1625] | 163 | ∀addr: addressing_mode. ∀p: is_in m fixed_v addr. |
---|
[1623] | 164 | Q addr ( |
---|
[1625] | 165 | match addr return λx: addressing_mode. is_in … fixed_v x → T with |
---|
[1624] | 166 | [ ADDR11 x ⇒ p_addr11 x |
---|
| 167 | | ADDR16 x ⇒ p_addr16 x |
---|
| 168 | | DIRECT x ⇒ p_direct x |
---|
| 169 | | INDIRECT x ⇒ p_indirect x |
---|
| 170 | | EXT_INDIRECT x ⇒ p_ext_indirect x |
---|
| 171 | | ACC_A ⇒ p_acc_a |
---|
| 172 | | REGISTER x ⇒ p_register x |
---|
| 173 | | ACC_B ⇒ p_acc_b |
---|
| 174 | | DPTR ⇒ p_dptr |
---|
| 175 | | DATA x ⇒ p_data x |
---|
| 176 | | DATA16 x ⇒ p_data16 x |
---|
| 177 | | ACC_DPTR ⇒ p_acc_dptr |
---|
| 178 | | ACC_PC ⇒ p_acc_pc |
---|
[1623] | 179 | | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr |
---|
[1624] | 180 | | INDIRECT_DPTR ⇒ p_indirect_dptr |
---|
| 181 | | CARRY ⇒ p_carry |
---|
| 182 | | BIT_ADDR x ⇒ p_bit_addr x |
---|
| 183 | | N_BIT_ADDR x ⇒ p_n_bit_addr x |
---|
| 184 | | RELATIVE x ⇒ p_relative x |
---|
[1623] | 185 | ] p) |
---|
| 186 | | VCons n' hd tl ⇒ λm_refl. λv_refl. |
---|
[1625] | 187 | let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11 |
---|
| 188 | p_addr16 p_direct p_indirect p_ext_indirect p_acc_a |
---|
| 189 | p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr |
---|
| 190 | p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry |
---|
| 191 | p_bit_addr p_n_bit_addr p_relative n' tl ? |
---|
[1623] | 192 | in |
---|
| 193 | match hd return λa: addressing_mode_tag. a = hd → ? with |
---|
[1624] | 194 | [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call |
---|
| 195 | | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call |
---|
| 196 | | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call |
---|
| 197 | | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call |
---|
| 198 | | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call |
---|
| 199 | | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call |
---|
| 200 | | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call |
---|
| 201 | | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call |
---|
| 202 | | dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call |
---|
| 203 | | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call |
---|
| 204 | | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call |
---|
| 205 | | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call |
---|
| 206 | | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call |
---|
[1623] | 207 | | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call |
---|
[1624] | 208 | | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call |
---|
| 209 | | carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call |
---|
| 210 | | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call |
---|
| 211 | | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call |
---|
| 212 | | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call |
---|
[1622] | 213 | ] (refl … hd) |
---|
[1624] | 214 | ] (refl … n) (refl_jmeq … v). |
---|
| 215 | [20: |
---|
[1625] | 216 | generalize in match proof; destruct |
---|
| 217 | whd in match (subvector_with … eq_a (hd:::tl) fixed_v); |
---|
| 218 | cases (mem … eq_a m fixed_v hd) normalize nodelta |
---|
| 219 | [1: |
---|
| 220 | whd in match (subvector_with … eq_a tl fixed_v); |
---|
| 221 | #assm assumption |
---|
| 222 | |2: |
---|
| 223 | normalize in ⊢ (% → ?); |
---|
| 224 | #absurd cases absurd |
---|
| 225 | ] |
---|
| 226 | ] |
---|
[1646] | 227 | @(is_in_subvector_is_in_supervector … proof) |
---|
[1625] | 228 | destruct @I |
---|
[1623] | 229 | qed. |
---|
[1621] | 230 | |
---|
[1645] | 231 | lemma subaddressing_mode_elim': |
---|
[1624] | 232 | ∀T: Type[2]. |
---|
[1645] | 233 | ∀n: nat. |
---|
| 234 | ∀o: nat. |
---|
| 235 | ∀Q: addressing_mode → T → Prop. |
---|
| 236 | ∀fixed_v: Vector addressing_mode_tag (n + o). |
---|
| 237 | ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. |
---|
| 238 | ∀v1: Vector addressing_mode_tag n. |
---|
| 239 | ∀v2: Vector addressing_mode_tag o. |
---|
| 240 | ∀fixed_v_proof: fixed_v = v1 @@ v2. |
---|
| 241 | ∀subaddressing_mode_proof. |
---|
| 242 | subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7 |
---|
| 243 | P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof. |
---|
| 244 | #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 |
---|
| 245 | #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof |
---|
| 246 | cases daemon |
---|
| 247 | qed. |
---|
| 248 | |
---|
| 249 | axiom subaddressing_mode_elim: |
---|
| 250 | ∀T: Type[2]. |
---|
[1625] | 251 | ∀m: nat. |
---|
[1645] | 252 | ∀n: nat. |
---|
| 253 | ∀Q: addressing_mode → T → Prop. |
---|
[1625] | 254 | ∀fixed_v: Vector addressing_mode_tag m. |
---|
| 255 | ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. |
---|
[1624] | 256 | ∀v: Vector addressing_mode_tag n. |
---|
[1625] | 257 | ∀proof. |
---|
| 258 | subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 |
---|
| 259 | P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. |
---|
[1624] | 260 | |
---|
| 261 | (* |
---|
[1622] | 262 | lemma subaddressing_mode_elim: |
---|
| 263 | ∀T:Type[2]. |
---|
| 264 | ∀P1: Word11 → T. |
---|
| 265 | ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T. |
---|
| 266 | ∀addr: addressing_mode. |
---|
| 267 | ∀p: is_in 1 [[ addr11 ]] addr. |
---|
| 268 | ∀Q: addressing_mode → T → Prop. |
---|
| 269 | (∀w. Q (ADDR11 w) (P1 w)) → |
---|
| 270 | Q addr ( |
---|
| 271 | match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with |
---|
| 272 | [ ADDR11 (x:Word11) ⇒ λH:True. P1 x |
---|
| 273 | | ADDR16 _ ⇒ λH:False. P2 H |
---|
| 274 | | DIRECT _ ⇒ λH:False. P3 H |
---|
| 275 | | INDIRECT _ ⇒ λH:False. P4 H |
---|
| 276 | | EXT_INDIRECT _ ⇒ λH:False. P5 H |
---|
| 277 | | ACC_A ⇒ λH:False. P6 H |
---|
| 278 | | REGISTER _ ⇒ λH:False. P7 H |
---|
| 279 | | ACC_B ⇒ λH:False. P8 H |
---|
| 280 | | DPTR ⇒ λH:False. P9 H |
---|
| 281 | | DATA _ ⇒ λH:False. P10 H |
---|
| 282 | | DATA16 _ ⇒ λH:False. P11 H |
---|
| 283 | | ACC_DPTR ⇒ λH:False. P12 H |
---|
| 284 | | ACC_PC ⇒ λH:False. P13 H |
---|
| 285 | | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H |
---|
| 286 | | INDIRECT_DPTR ⇒ λH:False. P15 H |
---|
| 287 | | CARRY ⇒ λH:False. P16 H |
---|
| 288 | | BIT_ADDR _ ⇒ λH:False. P17 H |
---|
| 289 | | N_BIT_ADDR _ ⇒ λH:False. P18 H |
---|
| 290 | | RELATIVE _ ⇒ λH:False. P19 H |
---|
| 291 | ] p). |
---|
| 292 | #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13 |
---|
| 293 | #P14 #P15 #P16 #P17 #P18 #P19 |
---|
| 294 | * try #x1 try #x2 try #x3 try #x4 |
---|
| 295 | try (@⊥ assumption) normalize @x4 |
---|
[1624] | 296 | qed. *) |
---|
[1621] | 297 | |
---|
[1622] | 298 | include alias "arithmetics/nat.ma". |
---|
| 299 | |
---|
[1621] | 300 | let rec block_cost |
---|
| 301 | (code_memory: BitVectorTrie Byte 16) (program_counter: Word) |
---|
| 302 | (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) |
---|
[1642] | 303 | (reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter) |
---|
| 304 | (good_program_witness: good_program code_memory total_program_size) |
---|
| 305 | on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝ |
---|
[1622] | 306 | match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with |
---|
[1642] | 307 | [ O ⇒ λbase_case. ⊥ |
---|
[1621] | 308 | | S program_size' ⇒ λrecursive_case. |
---|
| 309 | let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in |
---|
| 310 | match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with |
---|
| 311 | [ None ⇒ |
---|
| 312 | match instruction return λx. x = instruction → ? with |
---|
[1639] | 313 | [ RealInstruction real_instruction ⇒ λreal_instruction_refl. |
---|
| 314 | match real_instruction return λx. x = real_instruction → ? with |
---|
[1622] | 315 | [ RET ⇒ λinstr. ticks |
---|
| 316 | | JC relative ⇒ λinstr. ticks |
---|
| 317 | | JNC relative ⇒ λinstr. ticks |
---|
| 318 | | JB bit_addr relative ⇒ λinstr. ticks |
---|
| 319 | | JNB bit_addr relative ⇒ λinstr. ticks |
---|
| 320 | | JBC bit_addr relative ⇒ λinstr. ticks |
---|
| 321 | | JZ relative ⇒ λinstr. ticks |
---|
| 322 | | JNZ relative ⇒ λinstr. ticks |
---|
| 323 | | CJNE src_trgt relative ⇒ λinstr. ticks |
---|
| 324 | | DJNZ src_trgt relative ⇒ λinstr. ticks |
---|
| 325 | | _ ⇒ λinstr. |
---|
[1642] | 326 | ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ? |
---|
[1639] | 327 | ] (refl … real_instruction) |
---|
[1622] | 328 | | ACALL addr ⇒ λinstr. |
---|
[1642] | 329 | ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ? |
---|
[1622] | 330 | | AJMP addr ⇒ λinstr. ticks |
---|
| 331 | | LCALL addr ⇒ λinstr. |
---|
[1642] | 332 | ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ? |
---|
[1622] | 333 | | LJMP addr ⇒ λinstr. ticks |
---|
| 334 | | SJMP addr ⇒ λinstr. ticks |
---|
| 335 | | JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) |
---|
[1642] | 336 | ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ? |
---|
[1622] | 337 | | MOVC src trgt ⇒ λinstr. |
---|
[1642] | 338 | ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ? |
---|
[1621] | 339 | ] (refl … instruction) |
---|
| 340 | | Some _ ⇒ ticks |
---|
| 341 | ] |
---|
| 342 | ]. |
---|
[1642] | 343 | [1: |
---|
| 344 | cases reachable_program_counter_witness #_ #hyp |
---|
| 345 | @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …)) |
---|
| 346 | @(le_to_lt_to_lt … base_case hyp) |
---|
| 347 | |2: |
---|
| 348 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 349 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
| 350 | <FETCH normalize nodelta <instr normalize nodelta |
---|
[1645] | 351 | @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr |
---|
[1642] | 352 | cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta |
---|
| 353 | cases (split … 3 8 new_addr) #thr #eig normalize nodelta |
---|
| 354 | cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' |
---|
| 355 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
| 356 | @(transitive_le |
---|
| 357 | total_program_size |
---|
| 358 | ((S program_size') + nat_of_bitvector … program_counter) |
---|
| 359 | (program_size' + nat_of_bitvector … program_counter') recursive_case) |
---|
| 360 | normalize in match (S program_size' + nat_of_bitvector … program_counter); |
---|
| 361 | >plus_n_Sm |
---|
| 362 | @monotonic_le_plus_r |
---|
| 363 | change with ( |
---|
| 364 | nat_of_bitvector … program_counter < |
---|
| 365 | nat_of_bitvector … program_counter') |
---|
| 366 | assumption |
---|
| 367 | |3: |
---|
| 368 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 369 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
| 370 | <FETCH normalize nodelta <instr normalize nodelta |
---|
[1645] | 371 | @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr |
---|
[1642] | 372 | cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta |
---|
| 373 | cases (split … 3 8 new_addr) #thr #eig normalize nodelta |
---|
| 374 | cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' |
---|
| 375 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
| 376 | % |
---|
| 377 | [1: |
---|
| 378 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
| 379 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
| 380 | >(le_to_leb_true … program_counter_lt') % |
---|
| 381 | |2: |
---|
| 382 | assumption |
---|
| 383 | ] |
---|
| 384 | |4: |
---|
| 385 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 386 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
| 387 | <FETCH normalize nodelta <instr normalize nodelta |
---|
[1645] | 388 | @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr |
---|
[1642] | 389 | * * * * #n' |
---|
| 390 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
| 391 | @(transitive_le |
---|
| 392 | total_program_size |
---|
| 393 | ((S program_size') + nat_of_bitvector … program_counter) |
---|
| 394 | (program_size' + nat_of_bitvector … program_counter') recursive_case) |
---|
| 395 | normalize in match (S program_size' + nat_of_bitvector … program_counter); |
---|
| 396 | >plus_n_Sm |
---|
| 397 | @monotonic_le_plus_r |
---|
| 398 | change with ( |
---|
| 399 | nat_of_bitvector … program_counter < |
---|
| 400 | nat_of_bitvector … program_counter') |
---|
| 401 | assumption |
---|
| 402 | |5: |
---|
| 403 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 404 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
| 405 | <FETCH normalize nodelta <instr normalize nodelta |
---|
[1645] | 406 | @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr |
---|
[1642] | 407 | * * * * #n' |
---|
| 408 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
| 409 | % |
---|
| 410 | [1: |
---|
| 411 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
| 412 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
| 413 | >(le_to_leb_true … program_counter_lt') % |
---|
| 414 | |2: |
---|
| 415 | assumption |
---|
| 416 | ] |
---|
[1645] | 417 | |6,8: (* JMP and MOVC *) |
---|
[1642] | 418 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 419 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
| 420 | <FETCH normalize nodelta <instr normalize nodelta |
---|
| 421 | try(<real_instruction_refl <instr normalize nodelta) * |
---|
| 422 | #pc_pc_lt_hyp' #pc_tps_lt_hyp' |
---|
| 423 | @(transitive_le |
---|
| 424 | total_program_size |
---|
| 425 | ((S program_size') + nat_of_bitvector … program_counter) |
---|
| 426 | (program_size' + nat_of_bitvector … program_counter') recursive_case) |
---|
| 427 | normalize in match (S program_size' + nat_of_bitvector … program_counter); |
---|
| 428 | >plus_n_Sm |
---|
| 429 | @monotonic_le_plus_r |
---|
| 430 | change with ( |
---|
| 431 | nat_of_bitvector … program_counter < |
---|
| 432 | nat_of_bitvector … program_counter') |
---|
| 433 | assumption |
---|
[1645] | 434 | |7,9: |
---|
[1642] | 435 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 436 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
[1645] | 437 | <FETCH normalize nodelta <instr normalize nodelta * |
---|
[1642] | 438 | #program_counter_lt' #program_counter_lt_tps' % |
---|
[1645] | 439 | [1,3: |
---|
[1642] | 440 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
| 441 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
| 442 | >(le_to_leb_true … program_counter_lt') % |
---|
[1645] | 443 | |2,4: |
---|
[1642] | 444 | assumption |
---|
| 445 | ] |
---|
| 446 | |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53, |
---|
| 447 | 55,57,59,61,63: |
---|
| 448 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 449 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
[1645] | 450 | <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta * |
---|
[1642] | 451 | #program_counter_lt' #program_counter_lt_tps' % |
---|
[1645] | 452 | try assumption |
---|
| 453 | [*: |
---|
[1642] | 454 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
| 455 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
| 456 | >(le_to_leb_true … program_counter_lt') % |
---|
| 457 | ] |
---|
| 458 | |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52, |
---|
| 459 | 54,56,58,60,62: |
---|
| 460 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
| 461 | lapply(good_program_witness program_counter reachable_program_counter_witness) |
---|
| 462 | <FETCH normalize nodelta |
---|
| 463 | <real_instruction_refl <instr normalize nodelta * |
---|
| 464 | #pc_pc_lt_hyp' #pc_tps_lt_hyp' |
---|
| 465 | @(transitive_le |
---|
| 466 | total_program_size |
---|
| 467 | ((S program_size') + nat_of_bitvector … program_counter) |
---|
| 468 | (program_size' + nat_of_bitvector … program_counter') recursive_case) |
---|
| 469 | normalize in match (S program_size' + nat_of_bitvector … program_counter); |
---|
| 470 | >plus_n_Sm |
---|
| 471 | @monotonic_le_plus_r |
---|
| 472 | change with ( |
---|
| 473 | nat_of_bitvector … program_counter < |
---|
| 474 | nat_of_bitvector … program_counter') |
---|
| 475 | assumption |
---|
| 476 | ] |
---|
| 477 | qed. |
---|
| 478 | |
---|
[1646] | 479 | lemma fetch_program_counter_n_Sn: |
---|
[1645] | 480 | ∀instruction: instruction. |
---|
| 481 | ∀program_counter, program_counter': Word. |
---|
| 482 | ∀ticks, n: nat. |
---|
| 483 | ∀code_memory: BitVectorTrie Byte 16. |
---|
| 484 | Some … program_counter = fetch_program_counter_n n code_memory (zero 16) → |
---|
| 485 | 〈instruction,program_counter',ticks〉 = fetch code_memory program_counter → |
---|
[1646] | 486 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' → |
---|
| 487 | Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …). |
---|
| 488 | #instruction #program_counter #program_counter' #ticks #n #code_memory |
---|
| 489 | #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp |
---|
| 490 | whd in match (fetch_program_counter_n (S n) code_memory (zero …)); |
---|
| 491 | <fetch_program_counter_n_hyp normalize nodelta |
---|
| 492 | <fetch_hyp normalize nodelta |
---|
| 493 | change with ( |
---|
| 494 | leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter') |
---|
| 495 | ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter')); |
---|
| 496 | >(le_to_leb_true … lt_hyp) % |
---|
| 497 | qed. |
---|
| 498 | |
---|
[1645] | 499 | let rec traverse_code_internal |
---|
[1646] | 500 | (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
| 501 | (program_counter: Word) (fixed_program_size: nat) (program_size: nat) |
---|
| 502 | (reachable_program_counter_witness: |
---|
| 503 | ∀lbl: costlabel. |
---|
| 504 | ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → |
---|
| 505 | reachable_program_counter code_memory fixed_program_size program_counter) |
---|
| 506 | (good_program_witness: good_program code_memory fixed_program_size) |
---|
| 507 | on program_size: identifier_map CostTag nat ≝ |
---|
| 508 | match program_size with |
---|
| 509 | [ O ⇒ empty_map … |
---|
| 510 | | S program_size ⇒ |
---|
| 511 | let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in |
---|
| 512 | let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in |
---|
| 513 | match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with |
---|
| 514 | [ None ⇒ λlookup_refl. cost_mapping |
---|
| 515 | | Some lbl ⇒ λlookup_refl. |
---|
| 516 | let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size cost_labels ? good_program_witness ? in |
---|
[1645] | 517 | add … cost_mapping lbl cost |
---|
[1646] | 518 | ] (refl … (lookup_opt … program_counter cost_labels)) |
---|
[1645] | 519 | ]. |
---|
[1646] | 520 | [1: |
---|
| 521 | @(reachable_program_counter_witness lbl) |
---|
| 522 | assumption |
---|
| 523 | |2: |
---|
[1645] | 524 | // |
---|
[1646] | 525 | |3: |
---|
[1645] | 526 | assumption |
---|
[1642] | 527 | ] |
---|
[1639] | 528 | qed. |
---|
[1486] | 529 | |
---|
| 530 | definition traverse_code ≝ |
---|
[1645] | 531 | λcode_memory: BitVectorTrie Byte 16. |
---|
[1646] | 532 | λcost_labels: BitVectorTrie costlabel 16. |
---|
[1486] | 533 | λprogram_size: nat. |
---|
[1646] | 534 | λreachable_program_counter_witness: |
---|
| 535 | ∀lbl: costlabel. |
---|
| 536 | ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → |
---|
| 537 | reachable_program_counter code_memory program_size program_counter. |
---|
[1645] | 538 | λgood_program_witness: good_program code_memory program_size. |
---|
[1646] | 539 | traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness. |
---|
[1486] | 540 | |
---|
| 541 | definition compute_costs ≝ |
---|
| 542 | λprogram: list Byte. |
---|
[1557] | 543 | λcost_labels: BitVectorTrie costlabel 16. |
---|
[1486] | 544 | λhas_main: bool. |
---|
[1646] | 545 | λreachable_program_counter_witness: |
---|
| 546 | ∀lbl: costlabel. |
---|
| 547 | ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → |
---|
| 548 | reachable_program_counter (load_code_memory program) (|program| + 1) program_counter. |
---|
[1645] | 549 | λgood_program_witness: good_program (load_code_memory program) (|program| + 1). |
---|
| 550 | let program_size ≝ |program| + 1 in |
---|
| 551 | let code_memory ≝ load_code_memory program in |
---|
[1646] | 552 | traverse_code code_memory cost_labels program_size reachable_program_counter_witness ?. |
---|
| 553 | @good_program_witness |
---|
[1645] | 554 | qed. |
---|