Changeset 1547 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 23, 2011, 11:08:42 PM (8 years ago)
Author:
sacerdot
Message:

Invariant on cost of one execution step strengthened.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r1541 r1547  
    126126qed.
    127127
    128 lemma set_args_8_ignores_clock:
     128lemma set_arg_8_ignores_clock:
    129129 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).
    130130#M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
    … …  
    132132qed.
    133133
    134 example set_program_counter_ignores_clock:
     134lemma set_program_counter_ignores_clock:
    135135  ∀M: Type[0].
    136136  ∀s: PreStatus M.
    … …  
    140140qed.
    141141
    142 example set_low_internal_ram_ignores_clock:
     142lemma set_low_internal_ram_ignores_clock:
    143143  ∀M: Type[0].
    144144  ∀s: PreStatus M.
    … …  
    148148qed.
    149149
    150 example set_8051_sfr_ignores_clock:
     150lemma set_8051_sfr_ignores_clock:
    151151  ∀M: Type[0].
    152152  ∀s: PreStatus M.
    … …  
    156156  #M #s #sfr #v %
    157157qed.
    158 
    159 axiom set_arg_8_ignores_clock:
    160   ∀M: Type[0].
    161   ∀s: PreStatus M.
    162   ∀arg.
    163   ∀val.
    164     clock M (set_arg_8 … s arg val) = clock … s.
    165158 
    166 example clock_set_clock:
     159lemma clock_set_clock:
    167160  ∀M: Type[0].
    168161  ∀s: PreStatus M.
    … …  
    172165qed.
    173166
    174 lemma tech_clocks_le:
    175  ∀M,s.∀t:Σs'. clock M s ≤ clock M s'. clock … s ≤ clock … t.
    176  #M #s * //
    177 qed.
    178 
    179167definition execute_1_preinstruction:
    180168 ∀ticks: nat × nat.
    181169 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A →
    182  ∀s:PreStatus M. Σs': PreStatus M. clock M s ≤ clock … s' ≝
     170 ∀s:PreStatus M.
     171  Σs': PreStatus M.
     172   Or (clock … s' - clock … s = \fst ticks)
     173      (clock … s' - clock … s = \snd ticks)
     174 ≝
    183175  λticks.
    184176  λA, M: Type[0].
    … …  
    188180  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
    189181  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
    190   match instr return λx. Σs': PreStatus M. clock … s ≤ clock … s' with
     182  match instr return λx. Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks)
     183   (clock … s' - clock … s = \snd ticks) with
    191184        [ ADD addr1 addr2 ⇒
    192185            let s ≝ add_ticks1 s in
    … …  
    269262            ]
    270263        | INC addr ⇒
    271             match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    272                                                            registr;
    273                                                            direct;
    274                                                            indirect;
    275                                                            dptr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
     264            match addr
     265            return
     266             λx. bool_to_Prop
     267              (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) →
     268               Σs': PreStatus M.
     269                Or (clock … s' - clock … s = \fst ticks)
     270                   (clock … s' - clock … s = \snd ticks)
     271             with
    276272              [ ACC_A ⇒ λacc_a: True.
    277273                let s' ≝ add_ticks1 s in
    … …  
    345341                s
    346342        | CLR addr ⇒
    347           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
     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
    348344            [ ACC_A ⇒ λacc_a: True.
    349345              let s ≝ add_ticks1 s in
    … …  
    358354            ] (subaddressing_modein … addr)
    359355        | CPL addr ⇒
    360           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
     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
    361357            [ ACC_A ⇒ λacc_a: True.
    362358                let s ≝ add_ticks1 s in
    … …  
    412408              set_8051_sfr ? s SFR_ACC_A new_acc
    413409        | PUSH addr ⇒
    414             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
     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
    415411              [ DIRECT d ⇒ λdirect: True.
    416412                let s ≝ add_ticks1 s in
    … …  
    589585                 let s ≝ add_ticks2 s in
    590586                  s
    591         ]. cases daemon (*
    592         (*14s*)
    593 (*    try assumption (*20s*)
     587        ]. (*15s*)
     588    try assumption (*20s*)
    594589    try % (*6s*)
    595590    try (
    596591      @ (execute_1_technical … (subaddressing_modein …))
    597592      @ I
    598     ) (*34s*) *)
    599  try assumption
     593    ) (*66s*)
    600594 try @le_n
     595 [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ //
     596 |*: cases daemon ]
     597(*
    601598 [2,6,10: normalize @I
    602599 |1,5: /by/ (* 81 seconds *)
    … …  
    666663qed.
    667664
    668 definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
     665definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat. Σs': Status. clock … s' - clock … s = \snd current ≝
    669666  λs0,instr_pc_ticks.
    670667    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    671668    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    672669    let s ≝ set_program_counter ? s0 pc in
    673       match instr return λ_.Σs': Status. clock … s0 ≤ clock … s' with
    674       [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
     670      match instr return λ_.Status with
     671      [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
    675672        (λx. λs.
    676673        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
    677674        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
    678675        | _ ⇒ λabsd. ⊥
    679         ] (subaddressing_modein … x)) instr s
     676        ] (subaddressing_modein … x)) instr s)
    680677     | ACALL addr ⇒
    681678          let s ≝ set_clock ? s (ticks + clock ? s) in
    682           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
     679          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s' - clock … s0 = ticks with
    683680            [ ADDR11 a ⇒ λaddr11: True.
    684681              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    … …  
    697694        | LCALL addr ⇒
    698695          let s ≝ set_clock ? s (ticks + clock ? s) in
    699           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
     696          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
    700697            [ ADDR16 a ⇒ λaddr16: True.
    701698              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    … …  
    711708        | MOVC addr1 addr2 ⇒
    712709          let s ≝ set_clock ? s (ticks + clock ? s) in
    713           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
     710          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
    714711            [ ACC_DPTR ⇒ λacc_dptr: True.
    715712              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    … …  
    738735        | LJMP addr ⇒
    739736          let s ≝ set_clock ? s (ticks + clock ? s) in
    740           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
     737          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
    741738            [ ADDR16 a ⇒ λaddr16: True.
    742739                set_program_counter ? s a
    … …  
    745742        | SJMP addr ⇒
    746743          let s ≝ set_clock ? s (ticks + clock ? s) in
    747           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
     744          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
    748745            [ RELATIVE r ⇒ λrelative: True.
    749746                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    … …  
    753750        | AJMP addr ⇒
    754751          let s ≝ set_clock ? s (ticks + clock ? s) in
    755           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
     752          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
    756753            [ ADDR11 a ⇒ λaddr11: True.
    757754              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    … …  
    764761            | _ ⇒ λother: False. ⊥
    765762            ] (subaddressing_modein … addr)
    766       ].
    767     try assumption
    768     [1,2: >set_program_counter_ignores_clock normalize nodelta
     763      ]. (*10s*)
     764    [||||||||*:try assumption]
     765    [1,2,3,4,5,7: @sig2 (*7s*)
     766    |8: cases (execute_1_preinstruction ??????) #a * #H @H]
     767    [2,3: >set_program_counter_ignores_clock normalize nodelta
    769768      >write_at_stack_pointer_ignores_clock
    770769      >set_8051_sfr_ignores_clock
    771770      >write_at_stack_pointer_ignores_clock
    772       >set_8051_sfr_ignores_clock
    773       change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/
    774     |3,4,5,6: >set_program_counter_ignores_clock normalize nodelta
    775      change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/
    776     |7,8: >set_8051_sfr_ignores_clock normalize nodelta change with (? ≤ ?+?)
    777       >set_program_counter_ignores_clock /by/]
    778 qed.
    779 
    780 definition execute_1: ∀s:Status. Σs':Status. clock … s ≤ clock … s' ≝
     771      >set_8051_sfr_ignores_clock >clock_set_clock
     772      >set_program_counter_ignores_clock
     773      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H] (*Andrea: ???*)
     774    |1,4,5,6: >set_program_counter_ignores_clock normalize nodelta
     775     >clock_set_clock >set_program_counter_ignores_clock
     776     cut (∀n,m. n+m-m = n) [1,3,5,7:#n #m /by/ |*: #H @H] (*Andrea: ???*)
     777    |7: >set_8051_sfr_ignores_clock normalize nodelta
     778      >clock_set_clock >set_program_counter_ignores_clock
     779      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]
     780    |8: >set_8051_sfr_ignores_clock normalize nodelta
     781      >set_program_counter_ignores_clock >clock_set_clock
     782      >set_program_counter_ignores_clock
     783      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]]
     784qed.
     785
     786definition current_instruction_cost ≝
     787  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
     788
     789definition execute_1: ∀s:Status. Σs':Status. clock … s' - clock … s = current_instruction_cost s ≝
    781790  λs: Status.
    782791    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
Note: See TracChangeset for help on using the changeset viewer.