Changeset 1622 for src/ASM/ASMCosts.ma
- Timestamp:
- Dec 16, 2011, 10:09:12 AM (9 years ago)
- File:
-
- 1 edited
-
src/ASM/ASMCosts.ma (modified) (5 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1621 r1622 100 100 program_counter = fetch_program_counter_n (S n) code_memory (zero 16) ∧ 101 101 nat_of_bitvector 16 program_counter ≤ program_size ∧ 102 nat_of_bitvector 16 tail_program_counter ≤nat_of_bitvector 16 program_counter.102 nat_of_bitvector 16 tail_program_counter < nat_of_bitvector 16 program_counter. 103 103 104 104 definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝ … … 176 176 qed. 177 177 178 axiom dubious: 179 ∀m, n, o, p: nat. 180 1 ≤ p → n ≤ m → m - n ≤ S o → m - (n + p) ≤ o. 181 182 lemma subaddressing_mod_elim: 183 ∀T:Type[2]. 184 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19,addr,p. 185 ∀Q: addressing_mode → T → Prop. 186 (∀w. Q (ADDR11 w) (P1 w)) → 187 Q addr (match addr 188 in addressing_mode 189 return λx:addressing_mode.(is_in 1 [[addr11]] x→T) 190 with 191 [ADDR11 (x:Word11) ⇒ λH:True. P1 x 192 |ADDR16 _ ⇒ λH:False. P2 H 193 |DIRECT _ ⇒ λH:False. P3 H 194 |INDIRECT _ ⇒ λH:False. P4 H 195 |EXT_INDIRECT _ ⇒ λH:False. P5 H 196 |ACC_A ⇒ λH:False. P6 H 197 |REGISTER _ ⇒ λH:False. P7 H 198 |ACC_B ⇒ λH:False. P8 H 199 |DPTR ⇒ λH:False. P9 H 200 |DATA _ ⇒ λH:False. P10 H 201 |DATA16 _ ⇒ λH:False. P11 H 202 |ACC_DPTR ⇒ λH:False. P12 H 203 |ACC_PC ⇒ λH:False. P13 H 204 |EXT_INDIRECT_DPTR ⇒ λH:False. P14 H 205 |INDIRECT_DPTR ⇒ λH:False. P15 H 206 |CARRY ⇒ λH:False. P16 H 207 |BIT_ADDR _ ⇒ λH:False. P17 H 208 |N_BIT_ADDR _ ⇒ λH:False. P18 H 209 |RELATIVE _ ⇒ λH:False. P19 H 210 ] p). 211 #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13 212 #P14 #P15 #P16 #P17 #P18 #P19 213 * try #x1 try #x2 try #x3 try #x4 214 try (@⊥ assumption) normalize @x4 178 let rec member_addressing_mode_tag 179 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) 180 on v: Prop ≝ 181 match v with 182 [ VEmpty ⇒ False 183 | VCons n' hd tl ⇒ 184 match eq_a hd a with 185 [ true ⇒ True 186 | false ⇒ member_addressing_mode_tag n' tl a 187 ] 188 ]. 189 190 let rec subaddressing_mode_elim_type 191 (T: Type[2]) (n: nat) (v: Vector addressing_mode_tag n) 192 (Q: addressing_mode → T → Prop) 193 on v: 194 (∀n. ∀v. Word11 → member_addressing_mode_tag n v addr11 → T) → 195 (∀n. ∀v. Word → member_addressing_mode_tag n v addr16 → T) → 196 (∀n. ∀v. Byte → member_addressing_mode_tag n v direct → T) → 197 (∀n. ∀v. Bit → member_addressing_mode_tag n v indirect → T) → 198 (∀n. ∀v. Bit → member_addressing_mode_tag n v ext_indirect → T) → 199 (∀n. ∀v. member_addressing_mode_tag n v acc_a → T) → 200 (∀n. ∀v. BitVector 3 → member_addressing_mode_tag n v registr → T) → 201 (∀n. ∀v. member_addressing_mode_tag n v acc_b → T) → 202 (∀n. ∀v. member_addressing_mode_tag n v dptr → T) → 203 (∀n. ∀v. Byte → member_addressing_mode_tag n v data → T) → 204 (∀n. ∀v. Word → member_addressing_mode_tag n v data16 → T) → 205 (∀n. ∀v. member_addressing_mode_tag n v acc_dptr → T) → 206 (∀n. ∀v. member_addressing_mode_tag n v acc_pc → T) → 207 (∀n. ∀v. member_addressing_mode_tag n v ext_indirect_dptr → T) → 208 (∀n. ∀v. member_addressing_mode_tag n v indirect_dptr → T) → 209 (∀n. ∀v. member_addressing_mode_tag n v carry → T) → 210 (∀n. ∀v. Byte → member_addressing_mode_tag n v bit_addr → T) → 211 (∀n. ∀v. Byte → member_addressing_mode_tag n v n_bit_addr → T) → 212 (∀n. ∀v. Byte → member_addressing_mode_tag n v relative → T) → Prop ≝ 213 match v return λm: nat. λv': Vector addressing_mode_tag m. v ≃ v' → ? with 214 [ VEmpty ⇒ λv_refl. 215 λp_addr11. λp_addr16. λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. 216 λp_register. λp_acc_b. λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. 217 λp_ext_indirect_dptr. λp_indirect_dptr. λp_carry. λp_bit_addr. 218 λp_n_bit_addr. λp_relative. False 219 (* ∀addr:v. Q addr (match addr with *) 220 | VCons n' hd tl ⇒ λv_refl. 221 λp_addr11. λp_addr16: ∀n. ∀v. Word → member_addressing_mode_tag n v addr16 → T. 222 λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. λp_register. λp_acc_b. 223 λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. λp_ext_indirect_dptr. 224 λp_indirect_dptr. λp_carry. λp_bit_addr. λp_n_bit_addr. λp_relative. 225 match hd return λa: addressing_mode_tag. a = hd → Prop with 226 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 n v w ?)) → 227 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 228 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 229 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 230 p_relative) 231 | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 n v w ?)) → 232 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 233 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 234 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 235 p_relative) 236 | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct n v w ?)) → 237 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 238 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 239 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 240 p_relative) 241 | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect n v w ?)) → 242 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 243 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 244 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 245 p_relative) 246 | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect n v w ?)) → 247 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 248 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 249 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 250 p_relative) 251 | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a n v ?)) → 252 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 253 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 254 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 255 p_relative) 256 | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register n v w ?)) → 257 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 258 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 259 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 260 p_relative) 261 | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b n v ?)) → 262 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 263 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 264 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 265 p_relative) 266 | dptr ⇒ λhd_refl. (Q DPTR (p_dptr n v ?)) → 267 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 268 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 269 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 270 p_relative) 271 | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data n v w ?)) → 272 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 273 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 274 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 275 p_relative) 276 | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 n v w ?)) → 277 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 278 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 279 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 280 p_relative) 281 | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr n v ?)) → 282 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 283 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 284 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 285 p_relative) 286 | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc n v ?)) → 287 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 288 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 289 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 290 p_relative) 291 | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr n v ?)) → 292 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 293 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 294 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 295 p_relative) 296 | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr n v ?)) → 297 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 298 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 299 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 300 p_relative) 301 | carry ⇒ λhd_refl. (Q CARRY (p_carry n v ?)) → 302 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 303 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 304 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 305 p_relative) 306 | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr n v w ?)) → 307 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 308 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 309 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 310 p_relative) 311 | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr n v w ?)) → 312 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 313 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 314 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 315 p_relative) 316 | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative n v w ?)) → 317 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 318 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 319 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 320 p_relative) 321 ] (refl … hd) 322 ] (refl_jmeq … v). 323 324 lemma subaddressing_mode_elim: 325 ∀T:Type[2]. 326 ∀P1: Word11 → T. 327 ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T. 328 ∀addr: addressing_mode. 329 ∀p: is_in 1 [[ addr11 ]] addr. 330 ∀Q: addressing_mode → T → Prop. 331 (∀w. Q (ADDR11 w) (P1 w)) → 332 Q addr ( 333 match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with 334 [ ADDR11 (x:Word11) ⇒ λH:True. P1 x 335 | ADDR16 _ ⇒ λH:False. P2 H 336 | DIRECT _ ⇒ λH:False. P3 H 337 | INDIRECT _ ⇒ λH:False. P4 H 338 | EXT_INDIRECT _ ⇒ λH:False. P5 H 339 | ACC_A ⇒ λH:False. P6 H 340 | REGISTER _ ⇒ λH:False. P7 H 341 | ACC_B ⇒ λH:False. P8 H 342 | DPTR ⇒ λH:False. P9 H 343 | DATA _ ⇒ λH:False. P10 H 344 | DATA16 _ ⇒ λH:False. P11 H 345 | ACC_DPTR ⇒ λH:False. P12 H 346 | ACC_PC ⇒ λH:False. P13 H 347 | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H 348 | INDIRECT_DPTR ⇒ λH:False. P15 H 349 | CARRY ⇒ λH:False. P16 H 350 | BIT_ADDR _ ⇒ λH:False. P17 H 351 | N_BIT_ADDR _ ⇒ λH:False. P18 H 352 | RELATIVE _ ⇒ λH:False. P19 H 353 ] p). 354 #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13 355 #P14 #P15 #P16 #P17 #P18 #P19 356 * try #x1 try #x2 try #x3 try #x4 357 try (@⊥ assumption) normalize @x4 215 358 qed. 216 359 360 include alias "arithmetics/nat.ma". 361 362 lemma lt_n_o_to_plus_m_n_lt_plus_m_o: 363 ∀m, n, o: nat. 364 n < o → m + n < m + o. 365 #m #n #o #assm /2 by monotonic_le_plus_r/ 366 qed. 367 368 axiom fetch_program_counter_n_technical: 369 ∀code_memory: BitVectorTrie Byte 16. 370 ∀program_counter, program_counter': Word. 371 ∀instruction: instruction. 372 ∀ticks, n: nat. 373 program_counter' = \snd (\fst (fetch code_memory program_counter)) → 374 program_counter' = fetch_program_counter_n (S n) code_memory (zero …) → 375 program_counter = fetch_program_counter_n n code_memory (zero …). 376 217 377 let rec block_cost 218 378 (code_memory: BitVectorTrie Byte 16) (program_counter: Word) 219 379 (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) 220 380 (good_program_witness: good_program code_memory program_counter total_program_size) 221 on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size→ nat ≝222 match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size→ nat with381 on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝ 382 match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with 223 383 [ O ⇒ λbase_case. 0 224 384 | S program_size' ⇒ λrecursive_case. … … 229 389 [ RealInstruction instruction ⇒ λreal_instruction. 230 390 match instruction return λx. x = instruction → ? with 231 [ RET ⇒ λ ret.ticks232 | JC relative ⇒ λ jc.ticks233 | JNC relative ⇒ λ jnc.ticks234 | JB bit_addr relative ⇒ λ jb.ticks235 | JNB bit_addr relative ⇒ λ jnb.ticks236 | JBC bit_addr relative ⇒ λ jbc.ticks237 | JZ relative ⇒ λ jz.ticks238 | JNZ relative ⇒ λ jnz.ticks239 | CJNE src_trgt relative ⇒ λ cjne. ticks240 | DJNZ src_trgt relative ⇒ λ djnz. ticks241 | _ ⇒ λ alt.391 [ RET ⇒ λinstr. ticks 392 | JC relative ⇒ λinstr. ticks 393 | JNC relative ⇒ λinstr. ticks 394 | JB bit_addr relative ⇒ λinstr. ticks 395 | JNB bit_addr relative ⇒ λinstr. ticks 396 | JBC bit_addr relative ⇒ λinstr. ticks 397 | JZ relative ⇒ λinstr. ticks 398 | JNZ relative ⇒ λinstr. ticks 399 | CJNE src_trgt relative ⇒ λinstr. ticks 400 | DJNZ src_trgt relative ⇒ λinstr. ticks 401 | _ ⇒ λinstr. 242 402 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 243 403 ] (refl … instruction) 244 | ACALL addr ⇒ λ acall.404 | ACALL addr ⇒ λinstr. 245 405 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 246 | AJMP addr ⇒ λ ajmp. ticks247 | LCALL addr ⇒ λ lcall.406 | AJMP addr ⇒ λinstr. ticks 407 | LCALL addr ⇒ λinstr. 248 408 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 249 | LJMP addr ⇒ λ ljmp. ticks250 | SJMP addr ⇒ λ sjmp. ticks251 | JMP addr ⇒ λ jmp. (* XXX: actually a call due to use with fptrs *)409 | LJMP addr ⇒ λinstr. ticks 410 | SJMP addr ⇒ λinstr. ticks 411 | JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) 252 412 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 253 | MOVC src trgt ⇒ λ movc.413 | MOVC src trgt ⇒ λinstr. 254 414 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 255 415 ] (refl … instruction) … … 257 417 ] 258 418 ]. 259 [1: -block_cost -eta62747 -program_size419 [1: 260 420 generalize in match good_program_witness; 261 421 whd in match good_program; normalize nodelta 262 422 cases FETCH normalize nodelta 263 cases acall normalize nodelta 264 @(subaddressing_mod_elim Prop ??????????????????? addr 265 (subaddressing_modein ? [[addr11]] addr) 266 (λ_.λP. P → total_program_size-nat_of_bitvector 16 program_counter'≤program_size')) 267 268 cases addr #subaddressing_mode cases subaddressing_mode 269 try (#assm #absurd normalize in absurd; cases absurd) 270 try (#absurd normalize in absurd; cases absurd) 271 normalize nodelta 423 cases instr normalize nodelta 424 @subaddressing_mode_elim #new_addr 272 425 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 273 cases (split … 3 8 assm) #thr #eig normalize nodelta426 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 274 427 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta 275 428 #assm cases assm #ignore … … 277 430 #program_counter_eq' #program_counter_lt_total_program_size 278 431 #fetch_n_leq_program_counter' 279 lapply(dubious total_program_size (nat_of_bitvector … program_counter') 280 program_size' ? ? ? ?) 281 [2: assumption ] 432 @(transitive_le 433 total_program_size 434 ((S program_size') + nat_of_bitvector … program_counter) 435 (program_size' + nat_of_bitvector … program_counter') recursive_case) 436 whd in ⊢ (?%?); 437 change with ( 438 program_size' + (nat_of_bitvector … program_counter) < 439 program_size' + (nat_of_bitvector … program_counter')) 440 @lt_n_o_to_plus_m_n_lt_plus_m_o 441 >(fetch_program_counter_n_technical code_memory program_counter 442 program_counter' instruction ticks n) 443 /2 by pair_destruct_2/ 444 |3,5,7,9,11: 445 (* XXX etc. need the subaddressing_mode_elim generalizing *) 446 |2: 447 generalize in match good_program_witness; 448 whd in match (good_program code_memory program_counter total_program_size); 449 cases FETCH normalize nodelta 450 cases instr normalize nodelta 451 @subaddressing_mode_elim #new_addr 452 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 453 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 454 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta 455 #assm cases assm #ignore #good_program_counter 456 whd in match (good_program code_memory program_counter' total_program_size); 457 cases(fetch code_memory program_counter') #instruction_program_counter'' #ticks'' 458 cases(instruction_program_counter'') #instruction'' #program_counter'' normalize nodelta 459 282 460 [2: 283 461 (* generalize in match good_program_witness; *)
Note: See TracChangeset
for help on using the changeset viewer.
