Changeset 1910 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Apr 27, 2012, 5:48:20 PM (9 years ago)
Author:
mulligan
Message:

Finished proof modulo termination argument

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1909 r1910  
    927927qed.
    928928
     929definition program_counter_after_other ≝
     930  λprogram_counter. (* XXX: program counter after fetching *)
     931  λinstruction.
     932    if is_unconditional_jump instruction then
     933      compute_target_of_unconditional_jump program_counter instruction
     934    else
     935      program_counter.
     936
    929937definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
    930938  Σs': Status cm.
    931939    And (clock ?? s' = \snd current + clock … s)
    932       (if is_unconditional_jump (\fst (\fst current)) then
     940      (ASM_classify0 (\fst (\fst current)) = cl_other →
    933941        program_counter ? ? s' =
    934           compute_target_of_unconditional_jump (\snd (\fst current)) (\fst (\fst current))
    935        else
    936         (ASM_classify0 (\fst (\fst current)) = cl_other →
    937           program_counter ? ? s' = \snd (\fst current))) ≝
     942          program_counter_after_other (\snd (\fst current)) (\fst (\fst current))) ≝
    938943  λcm,s0,instr_pc_ticks.
    939944    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
     
    10541059    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    10551060      And (clock ?? s' = current_instruction_cost cm s + clock … s)
    1056         (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then
     1061        (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
    10571062          program_counter ? ? s' =
    1058             compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))
    1059          else
    1060           (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
    1061             program_counter ? ? s' = \snd (\fst instr_pc_ticks))) ≝
     1063            program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))) ≝
    10621064  λcm. λs: Status cm.
    10631065  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     
    10791081  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    10801082    (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
    1081       (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then
    1082          program_counter ? cm (execute_1 cm s) =
    1083            compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))
    1084        else
    1085          (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
    1086            (program_counter ? cm (execute_1 cm s)) = \snd (\fst instr_pc_ticks)))
     1083      (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
     1084        program_counter ? cm (execute_1 cm s) =
     1085          program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))).
    10871086(*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
    10881087  #cm #s normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.