Changeset 1575 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 29, 2011, 2:21:39 PM (8 years ago)
Author:
mulligan
Message:

Changes to specifications on execute functions

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r1573 r1575  
    170170 ∀s:PreStatus M.
    171171  Σs': PreStatus M.
    172    Or (clock … s' - clock … s = \fst ticks)
    173       (clock … s' - clock … s = \snd ticks)
     172   And
     173   (Or (clock … s' - clock … s = \fst ticks)
     174      (clock … s' - clock … s = \snd ticks))
     175   (clock … s ≤ clock … s')
    174176 ≝
    175177  λticks.
    … …  
    180182  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
    181183  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
    182   match instr return λx. Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks)
    183    (clock … s' - clock … s = \snd ticks) with
     184  match instr return λx.
     185    Σs': PreStatus M.
     186      And
     187        (Or (clock … s' - clock … s = \fst ticks)
     188            (clock … s' - clock … s = \snd ticks))
     189                (clock … s ≤ clock … s') with
    184190        [ ADD addr1 addr2 ⇒
    185191            let s ≝ add_ticks1 s in
    … …  
    267273              (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) →
    268274               Σs': PreStatus M.
    269                 Or (clock … s' - clock … s = \fst ticks)
    270                    (clock … s' - clock … s = \snd ticks)
     275                And
     276                (Or (clock … s' - clock … s = \fst ticks)
     277                   (clock … s' - clock … s = \snd ticks))
     278                (clock … s ≤ clock … s')
    271279             with
    272280              [ ACC_A ⇒ λacc_a: True.
    … …  
    341349                s
    342350        | CLR addr ⇒
    343           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks) (clock … s' - clock … s = \snd ticks) with
     351          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) →
     352              Σs': PreStatus M.
     353                              And
     354                (Or (clock … s' - clock … s = \fst ticks)
     355                   (clock … s' - clock … s = \snd ticks))
     356                (clock … s ≤ clock … s') with
    344357            [ ACC_A ⇒ λacc_a: True.
    345358              let s ≝ add_ticks1 s in
    … …  
    354367            ] (subaddressing_modein … addr)
    355368        | CPL addr ⇒
    356           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks) (clock … s' - clock … s = \snd ticks) with
     369          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) →
     370            Σs': PreStatus M.
     371                           And
     372                (Or (clock … s' - clock … s = \fst ticks)
     373                   (clock … s' - clock … s = \snd ticks))
     374                (clock … s ≤ clock … s') with
    357375            [ ACC_A ⇒ λacc_a: True.
    358376                let s ≝ add_ticks1 s in
    … …  
    408426              set_8051_sfr ? s SFR_ACC_A new_acc
    409427        | PUSH addr ⇒
    410             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks) (clock … s' - clock … s = \snd ticks) with
     428            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) →
     429              Σs': PreStatus M.
     430                And
     431                (Or (clock … s' - clock … s = \fst ticks)
     432                   (clock … s' - clock … s = \snd ticks))
     433                (clock … s ≤ clock … s') with
    411434              [ DIRECT d ⇒ λdirect: True.
    412435                let s ≝ add_ticks1 s in
    … …  
    593616    ) (*66s*)
    594617 try @le_n
    595  [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ //
    596  |*: cases daemon ]
    597 (*
    598  [2,6,10: normalize @I
    599  |1,5: /by/ (* 81 seconds *)
    600  |9:
    601    normalize nodelta <set_flags_ignores_clock >set_arg_8_ignores_clock
    602    >clock_set_clock //
    603  |23:
    604    normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
    605    >set_8051_sfr_ignores_clock >clock_set_clock //
    606  |21,24:
    607    normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
    608    >clock_set_clock //
    609  |25,26,28:
    610    normalize nodelta //
    611  |30,32,35:
    612    normalize nodelta //
    613  |13,14,15,16,18:
    614    normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
    615  |17:
    616    normalize nodelta >set_8051_sfr_ignores_clock >clock_set_clock //
    617  |3,4,7,8,11,12,19,20,33,36: cases daemon
    618  |27,29,31,34,37:
    619    normalize nodelta >set_program_counter_ignores_clock >clock_set_clock //
    620  |22:
    621    normalize nodelta <set_flags_ignores_clock >clock_set_clock //
    622  [9: (* normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
    623      >clock_set_clock // *) (* segfault now *)
    624  |32,34: cases l #either normalize nodelta cases either
    625       #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
    626       >clock_set_clock //
    627  |36,48: cases addr #either normalize nodelta cases either
    628       #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
    629       >clock_set_clock // (* XXX: change addr to l *)
    630  |44: cases l2 #either normalize nodelta
    631       [2: cases either #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
    632           >clock_set_clock //
    633       |1: cases either #addr cases addr #addr1 #addr2 normalize nodelta
    634           >set_arg_8_ignores_clock >clock_set_clock //
    635       ] (* XXX: change l2 to l *)
    636  |5: cases (sub_8_with_carry (get_arg_8 M s1 true addr) (bitvector_of_nat 8 1) false)
    637      #result #flags normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
    638  |37: cases addr
    639  |20,21,30,31: (* XXX: segfault here *)
    640  |1,2,3: /by/ (*41s*)
    641  |4,6,7,8,10,11,12,13,14,15: /by/ (*6s*)
    642  |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*9s*)
    643  |33,35,39,41,43,54,55,56: /by/ (*6s*)
    644  |57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*)
    645  (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
    646  |*:cases daemon] *)
     618 [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ /2 by or_introl/
     619 | /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ //
     620 |*: cases daemon (* XXX: easy? *) ]
    647621qed.
    648622
    … …  
    663637qed.
    664638
    665 definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat. Σs': Status. clock … s' - clock … s = \snd current ≝
     639definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat.
     640  Σs': Status. And (clock … s' - clock … s = \snd current) (clock … s ≤ clock … s') ≝
    666641  λs0,instr_pc_ticks.
    667642    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    668643    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    669644    let s ≝ set_program_counter ? s0 pc in
    670       match instr return λ_.Status with
    671       [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
     645      match instr return λ_. Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     646      [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
    672647        (λx. λs.
    673         match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
     648        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    674649        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
    675650        | _ ⇒ λabsd. ⊥
    676651        ] (subaddressing_modein … x)) instr s)
    677      | ACALL addr ⇒
     652      | MOVC addr1 addr2 ⇒
    678653          let s ≝ set_clock ? s (ticks + clock ? s) in
    679           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s' - clock … s0 = ticks with
    680             [ ADDR11 a ⇒ λaddr11: True.
    681               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    682               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    683               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    684               let s ≝ write_at_stack_pointer ? s pc_bl in
    685               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    686               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    687               let s ≝ write_at_stack_pointer ? s pc_bu in
    688               let 〈thr, eig〉 ≝ split ? 3 8 a in
    689               let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    690               let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    691                 set_program_counter ? s new_addr
    692             | _ ⇒ λother: False. ⊥
    693             ] (subaddressing_modein … addr)
    694         | LCALL addr ⇒
    695           let s ≝ set_clock ? s (ticks + clock ? s) in
    696           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
    697             [ ADDR16 a ⇒ λaddr16: True.
    698               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    699               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    700               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    701               let s ≝ write_at_stack_pointer ? s pc_bl in
    702               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    703               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    704               let s ≝ write_at_stack_pointer ? s pc_bu in
    705                 set_program_counter ? s a
    706             | _ ⇒ λother: False. ⊥
    707             ] (subaddressing_modein … addr)
    708         | MOVC addr1 addr2 ⇒
    709           let s ≝ set_clock ? s (ticks + clock ? s) in
    710           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
     654          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) →
     655            Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
    711656            [ ACC_DPTR ⇒ λacc_dptr: True.
    712657              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    … …  
    726671            | _ ⇒ λother: False. ⊥
    727672            ] (subaddressing_modein … addr2)
    728         | JMP _ ⇒ (* DPM: always indirect_dptr *)
     673      | JMP _ ⇒ (* DPM: always indirect_dptr *)
    729674          let s ≝ set_clock ? s (ticks + clock ? s) in
    730675          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    … …  
    733678          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
    734679            set_program_counter ? s new_pc
    735         | LJMP addr ⇒
     680      | LJMP addr ⇒
    736681          let s ≝ set_clock ? s (ticks + clock ? s) in
    737           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
     682          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) →
     683            Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
    738684            [ ADDR16 a ⇒ λaddr16: True.
    739685                set_program_counter ? s a
    740686            | _ ⇒ λother: False. ⊥
    741687            ] (subaddressing_modein … addr)
    742         | SJMP addr ⇒
     688      | SJMP addr ⇒
    743689          let s ≝ set_clock ? s (ticks + clock ? s) in
    744           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
     690          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) →
     691            Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
    745692            [ RELATIVE r ⇒ λrelative: True.
    746693                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    … …  
    748695            | _ ⇒ λother: False. ⊥
    749696            ] (subaddressing_modein … addr)
    750         | AJMP addr ⇒
     697      | AJMP addr ⇒
    751698          let s ≝ set_clock ? s (ticks + clock ? s) in
    752           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
     699          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) →
     700            Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
    753701            [ ADDR11 a ⇒ λaddr11: True.
    754702              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    … …  
    761709            | _ ⇒ λother: False. ⊥
    762710            ] (subaddressing_modein … addr)
     711      | ACALL addr ⇒
     712          let s ≝ set_clock ? s (ticks + clock ? s) in
     713          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) →
     714            Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     715            [ ADDR11 a ⇒ λaddr11: True.
     716              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     717              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     718              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     719              let s ≝ write_at_stack_pointer ? s pc_bl in
     720              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     721              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     722              let s ≝ write_at_stack_pointer ? s pc_bu in
     723              let 〈thr, eig〉 ≝ split ? 3 8 a in
     724              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
     725              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
     726                set_program_counter ? s new_addr
     727            | _ ⇒ λother: False. ⊥
     728            ] (subaddressing_modein … addr)
     729        | LCALL addr ⇒
     730          let s ≝ set_clock ? s (ticks + clock ? s) in
     731          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) →
     732            Σs':Status. And (clock … s' - clock … s0 = ticks) (clock … s0 ≤ clock … s') with
     733            [ ADDR16 a ⇒ λaddr16: True.
     734              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     735              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     736              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     737              let s ≝ write_at_stack_pointer ? s pc_bl in
     738              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     739              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     740              let s ≝ write_at_stack_pointer ? s pc_bu in
     741                set_program_counter ? s a
     742            | _ ⇒ λother: False. ⊥
     743            ] (subaddressing_modein … addr)
    763744      ]. (*10s*)
     745    cases daemon (* XXX: problem with russell here *)
     746(*
    764747    [||||||||*:try assumption]
    765748    [1,2,3,4,5,7: @sig2 (*7s*)
    … …  
    781764      >set_program_counter_ignores_clock >clock_set_clock
    782765      >set_program_counter_ignores_clock
    783       cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]]
     766      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]] *)
    784767qed.
    785768
    … …  
    788771    \snd (fetch (code_memory … s) (program_counter … s)).
    789772
    790 definition execute_1: ∀s:Status. Σs':Status. clock … s' - clock … s = current_instruction_cost s ≝
     773definition execute_1: ∀s:Status.
     774  Σs':Status. And (clock … s' - clock … s = current_instruction_cost s) (clock … s ≤ clock … s') ≝
    791775  λs: Status.
    792776    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
Note: See TracChangeset for help on using the changeset viewer.