Changeset 1642 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Jan 12, 2012, 6:16:50 PM (9 years ago)
Author:
mulligan
Message:

finished big proof in all but two cases

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r1604 r1642  
    424424  let 〈word, byte〉 ≝ next pmem pc in
    425425    fetch0 pmem word byte.
    426 
    427 let rec fetch_program_counter_n
    428   (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
    429     on n: Word ≝
    430   match n with
    431   [ O ⇒ program_counter
    432   | S n ⇒
    433     let tail_pc ≝ fetch_program_counter_n n code_memory program_counter in
    434     let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
    435       program_counter
    436   ].
Note: See TracChangeset for help on using the changeset viewer.