Changeset 2062 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 13, 2012, 5:00:35 PM (8 years ago)
Author:
sacerdot
Message:

Everything repaired (broken because of new proof obligation for fetch).

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r2056 r2062  
    12221222
    12231223definition execute_1_pseudo_instruction:
    1224  (Word → nat × nat) → ∀cm. ∀s:PseudoStatus cm.
     1224 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm.
    12251225   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
    12261226    PseudoStatus cm
    12271227≝
    1228   λticks_of,cm,s,pc_ok.
     1228  λcm,ticks_of,s,pc_ok.
    12291229  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
    1230   let ticks ≝ ticks_of (program_counter … s) in
     1230  let ticks ≝ ticks_of (program_counter … s) pc_ok in
    12311231   execute_1_pseudo_instruction0 ticks cm s instr pc.
    12321232
Note: See TracChangeset for help on using the changeset viewer.