Changeset 1588 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Dec 6, 2011, 11:21:37 AM (8 years ago)
Author:
sacerdot
Message:

All goals generated by Russell for execute_1* are now closed, mostly by
automation. Since automation does not work on equational goals that contain
equations, I was forced to change every (?) Russel definition into triples:
fun' with Sigma type as a type; fun as @eject of fun'; fun_ok as @sig2 of fun'.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r1587 r1588  
    1818 cases b
    1919 normalize
    20  //
    2120 # K
     21 try %
    2222 cases (eq_true_false K)
    2323qed.
    … …  
    126126qed.
    127127
    128 lemma set_arg_8_ignores_clock:
    129  ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).
    130 #M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
    131 #a #E >E //
    132 qed.
    133 
    134128lemma set_program_counter_ignores_clock:
    135129  ∀M: Type[0].
    … …  
    163157    clock … (set_8051_sfr ? s sfr v) = clock … s.
    164158  #M #s #sfr #v %
    165 qed.
    166 
    167 lemma set_arg_1_ignores_clock:
    168   ∀m: Type[0].
    169   ∀s: PreStatus m.
    170   ∀addr: [[bit_addr; carry]].
    171   ∀bit: Bit.
    172     clock … (set_arg_1 m s addr bit) = clock … s.
    173   #m #s #addr #bit
    174   whd in match set_arg_1; normalize nodelta
    175   cases addr #subaddressing_mode
    176   cases subaddressing_mode
    177   try #assm1 try #assm2
    178   try (normalize in assm2; cases assm2)
    179   try (normalize in assm1; cases assm1)
    180   normalize nodelta
    181   cases (split bool 4 4 (get_8051_sfr m s SFR_PSW))
    182   #nu #nl normalize nodelta
    183   [ @set_8051_sfr_ignores_clock
    184   | cases(split … 1 3 nu)
    185     #ignore #three_bits normalize nodelta
    186     cases(get_index_v … 4 nu 0 ?)
    187     normalize nodelta
    188     [ <set_bit_addressable_sfr_ignores_clock | >set_low_internal_ram_ignores_clock ] %
    189   ]
    190 qed.
    191 
    192 lemma set_arg_16_ignores_clock:
    193   ∀m: Type[0].
    194   ∀s: PreStatus m.
    195   ∀w: Word.
    196   ∀addr: [[dptr]].
    197     clock … (set_arg_16 m s w addr) = clock … s.
    198   #m #s #w #addr
    199   whd in match set_arg_16; normalize nodelta
    200   cases addr #subaddressing_modein
    201   cases subaddressing_modein
    202   try #assm1 try #assm2
    203   try (normalize in assm2; cases assm2)
    204   try (normalize in assm1; cases assm1)
    205   normalize nodelta
    206   cases (split … 8 8 w) #bu #bl normalize nodelta
    207   >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock %
    208159qed.
    209160
    … …  
    228179qed.
    229180
    230 definition execute_1_preinstruction:
     181definition execute_1_preinstruction':
    231182  ∀ticks: nat × nat.
    232183  ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
    … …  
    279230                  let 〈addr1, addr2〉 ≝ l' in
    280231                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    281                     eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
     232                    set_arg_8 ? s addr1 and_val
    282233                | inr r ⇒
    283234                  let 〈addr1, addr2〉 ≝ r in
    284235                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    285                     eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
     236                    set_arg_8 ? s addr1 and_val
    286237                ]
    287238            | inr r ⇒
    288239              let 〈addr1, addr2〉 ≝ r in
    289240              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
    290                 eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s and_val (None ?) (get_ov_flag ? s))
     241               set_flags ? s and_val (None ?) (get_ov_flag ? s)
    291242            ]
    292243        | ORL addr ⇒
    … …  
    294245          match addr with
    295246            [ inl l ⇒
    296               match l return λ_. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
     247              match l with
    297248                [ inl l' ⇒
    298249                  let 〈addr1, addr2〉 ≝ l' in
    299250                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    300                     eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
     251                    set_arg_8 ? s addr1 or_val
    301252                | inr r ⇒
    302253                  let 〈addr1, addr2〉 ≝ r in
    303254                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    304                     eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
     255                    set_arg_8 ? s addr1 or_val
    305256                ]
    306257            | inr r ⇒
    307258              let 〈addr1, addr2〉 ≝ r in
    308259              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
    309                 eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s or_val (None ?) (get_ov_flag ? s))
     260               set_flags ? s or_val (None ?) (get_ov_flag ? s)
    310261            ]
    311262        | XRL addr ⇒
    … …  
    315266              let 〈addr1, addr2〉 ≝ l' in
    316267              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    317                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
     268                set_arg_8 ? s addr1 xor_val
    318269            | inr r ⇒
    319270              let 〈addr1, addr2〉 ≝ r in
    320271              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    321                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
     272                set_arg_8 ? s addr1 xor_val
    322273            ]
    323274        | INC addr ⇒
    … …  
    326277                let s' ≝ add_ticks1 s in
    327278                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
    328                  eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' ACC_A result)
     279                 set_arg_8 ? s' ACC_A result
    329280              | REGISTER r ⇒ λregister: True.
    330281                let s' ≝ add_ticks1 s in
    331282                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    332                  eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (REGISTER r) result)
     283                 set_arg_8 ? s' (REGISTER r) result
    333284              | DIRECT d ⇒ λdirect: True.
    334285                let s' ≝ add_ticks1 s in
    335286                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    336                  eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (DIRECT d) result)
     287                 set_arg_8 ? s' (DIRECT d) result
    337288              | INDIRECT i ⇒ λindirect: True.
    338289                let s' ≝ add_ticks1 s in
    339290                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    340                  eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (INDIRECT i) result)
     291                 set_arg_8 ? s' (INDIRECT i) result
    341292              | DPTR ⇒ λdptr: True.
    342293                let s' ≝ add_ticks1 s in
    … …  
    344295                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
    345296                let s ≝ set_8051_sfr ? s' SFR_DPL bl in
    346                   eject (PreStatus m) (λx. clock … s' = clock … x) (set_8051_sfr ? s' SFR_DPH bu)
     297                 set_8051_sfr ? s' SFR_DPH bu
    347298              | _ ⇒ λother: False. ⊥
    348299              ] (subaddressing_modein … addr)
    … …  
    353304           let s ≝ add_ticks1 s in
    354305           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
    355              eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr result)
     306             set_arg_8 ? s addr result
    356307        | MUL addr1 addr2 ⇒
    357308           let s ≝ add_ticks1 s in
    … …  
    397348            [ ACC_A ⇒ λacc_a: True.
    398349              let s ≝ add_ticks1 s in
    399                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s ACC_A (zero 8))
     350               set_arg_8 ? s ACC_A (zero 8)
    400351            | CARRY ⇒ λcarry: True.
    401352              let s ≝ add_ticks1 s in
    402                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY false)
     353               set_arg_1 ? s CARRY false
    403354            | BIT_ADDR b ⇒ λbit_addr: True.
    404355              let s ≝ add_ticks1 s in
    405                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) false)
     356               set_arg_1 ? s (BIT_ADDR b) false
    406357            | _ ⇒ λother: False. ⊥
    407358            ] (subaddressing_modein … addr)
    … …  
    412363                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    413364                let new_acc ≝ negation_bv ? old_acc in
    414                   eject (PreStatus m) (λx. clock … s = clock … x) (set_8051_sfr ? s SFR_ACC_A new_acc)
     365                 set_8051_sfr ? s SFR_ACC_A new_acc
    415366            | CARRY ⇒ λcarry: True.
    416367                let s ≝ add_ticks1 s in
    417368                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
    418369                let new_cy_flag ≝ ¬old_cy_flag in
    419                   eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY new_cy_flag)
     370                 set_arg_1 ? s CARRY new_cy_flag
    420371            | BIT_ADDR b ⇒ λbit_addr: True.
    421372                let s ≝ add_ticks1 s in
    422373                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
    423374                let new_bit ≝ ¬old_bit in
    424                   eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) new_bit)
     375                 set_arg_1 ? s (BIT_ADDR b) new_bit
    425376            | _ ⇒ λother: False. ?
    426377            ] (subaddressing_modein … addr)
    … …  
    480431            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    481432            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
    482               eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr2 old_acc)
     433              set_arg_8 ? s addr2 old_acc
    483434        | XCHD addr1 addr2 ⇒
    484435            let s ≝ add_ticks1 s in
    … …  
    515466            [ inl l ⇒
    516467              let 〈addr1, addr2〉 ≝ l in
    517                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     468                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    518469            | inr r ⇒
    519470              let 〈addr1, addr2〉 ≝ r in
    520                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     471                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    521472            ]
    522473        | MOV addr ⇒
    … …  
    533484                            [ inl l'''' ⇒
    534485                              let 〈addr1, addr2〉 ≝ l'''' in
    535                                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     486                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    536487                            | inr r'''' ⇒
    537488                              let 〈addr1, addr2〉 ≝ r'''' in
    538                                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     489                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    539490                            ]
    540491                        | inr r''' ⇒
    541492                          let 〈addr1, addr2〉 ≝ r''' in
    542                             eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
     493                            set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
    543494                        ]
    544495                    | inr r'' ⇒
    545496                      let 〈addr1, addr2〉 ≝ r'' in
    546                         eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
     497                       set_arg_16 ? s (get_arg_16 ? s addr2) addr1
    547498                    ]
    548499                | inr r ⇒
    549500                  let 〈addr1, addr2〉 ≝ r in
    550                     eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
     501                   set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
    551502                ]
    552503            | inr r ⇒
    553504              let 〈addr1, addr2〉 ≝ r in
    554                 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
     505               set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
    555506            ]
    556507          | JC addr ⇒
    … …  
    638589                 let s ≝ add_ticks2 s in
    639590                  s
    640         ]. (*15s*) (*
     591        ]. (*15s*)
    641592    try (cases(other))
    642593    try assumption (*20s*)
    643     try % (*6s*)
     594    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    644595    try (
    645596      @ (execute_1_technical … (subaddressing_modein …))
    646597      @ I
    647598    ) (*66s*)
    648     try (<set_arg_8_ignores_clock normalize nodelta /demod/ %)
    649     try (/demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ %)
    650     try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %)
    651     try (normalize nodelta <set_flags_ignores_clock /demod/ %)
    652     try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus)
    653     try (/demod/ normalize nodelta >clock_set_clock @commutative_plus)
    654     try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus)
    655     try (/demod/ normalize nodelta >clock_set_clock <set_arg_8_ignores_clock @commutative_plus)
    656     try (/demod/ normalize nodelta >set_arg_1_ignores_clock >clock_set_clock @commutative_plus)
    657     try (normalize nodelta >clock_set_clock >set_arg_1_ignores_clock >clock_set_clock %)
    658     try (normalize nodelta <set_arg_8_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)
    659     try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %)
    660     try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %)
    661     try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %) *) (* XXX: for convenience *)
    662     cases daemon
     599    normalize nodelta /2 by or_introl, or_intror/ (*35s*)
     600qed.
     601
     602definition execute_1_preinstruction:
     603  ∀ticks: nat × nat.
     604  ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
     605  PreStatus m → PreStatus m ≝ execute_1_preinstruction'.
     606 
     607lemma execute_1_preinstruction_ok:
     608 ∀ticks,a,m,f,i,s.
     609  clock ? (execute_1_preinstruction ticks a m f i s) = \fst ticks + clock … s ∨
     610  clock ? (execute_1_preinstruction ticks a m f i s) = \snd ticks + clock … s.
     611 #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @sig2
    663612qed.
    664613
    … …  
    669618    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    670619    let s ≝ set_program_counter ? s0 pc in
    671       match instr return λ_. Σs': Status. clock … s' = ticks + clock … s0 with
    672       [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
     620      match instr return λ_.Status with
     621      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
    673622        (λx. λs.
    674623        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    675624        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
    676625        | _ ⇒ λabsd. ⊥
    677         ] (subaddressing_modein … x)) instr s)
     626        ] (subaddressing_modein … x)) instr s
    678627      | MOVC addr1 addr2 ⇒
    679628          let s ≝ set_clock ? s (ticks + clock ? s) in
    … …  
    763712            ] (subaddressing_modein … addr)
    764713      ]. (*10s*)
    765     try (cases(other))
    766     [2: normalize nodelta
    767         >set_program_counter_ignores_clock
    768         >write_at_stack_pointer_ignores_clock
    769         >set_8051_sfr_ignores_clock
    770         >write_at_stack_pointer_ignores_clock
    771         >set_8051_sfr_ignores_clock >clock_set_clock
    772         >set_program_counter_ignores_clock %
    773     |*:  cases daemon
    774     ]
    775 (*
    776714    [||||||||*:try assumption]
    777     [1,2,3,4,5,7: @sig2 (*7s*)
    778     |8: cases (execute_1_preinstruction ??????) #a * #H @H]
    779     [2,3: >set_program_counter_ignores_clock normalize nodelta
    780       >write_at_stack_pointer_ignores_clock
    781       >set_8051_sfr_ignores_clock
    782       >write_at_stack_pointer_ignores_clock
    783       >set_8051_sfr_ignores_clock >clock_set_clock
    784       >set_program_counter_ignores_clock
    785       cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H] (*Andrea: ???*)
    786     |1,4,5,6: >set_program_counter_ignores_clock normalize nodelta
    787      >clock_set_clock >set_program_counter_ignores_clock
    788      cut (∀n,m. n+m-m = n) [1,3,5,7:#n #m /by/ |*: #H @H] (*Andrea: ???*)
    789     |7: >set_8051_sfr_ignores_clock normalize nodelta
    790       >clock_set_clock >set_program_counter_ignores_clock
    791       cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]
    792     |8: >set_8051_sfr_ignores_clock normalize nodelta
    793       >set_program_counter_ignores_clock >clock_set_clock
    794       >set_program_counter_ignores_clock
    795       cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]] *)
     715    [1,2,3,4,5,7: @sig2 (*35s*)
     716    |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?
     717        (λx. λs.
     718        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
     719        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
     720        | _ ⇒ λabsd. ⊥
     721        ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H
     722    |*: normalize nodelta try // (*17s*)
     723        >set_program_counter_ignores_clock // (* Andrea:??*) ]
    796724qed.
    797725
    … …  
    800728    \snd (fetch (code_memory … s) (program_counter … s)).
    801729
    802 definition execute_1: ∀s:Status.
     730definition execute_1': ∀s:Status.
    803731  Σs':Status. clock … s' = current_instruction_cost s + clock … s ≝
    804732  λs: Status.
    805733    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
    806734     execute_1_0 s instr_pc_ticks.
     735
     736definition execute_1: Status → Status ≝ execute_1'.
     737
     738lemma execute_1_ok: ∀s. clock … (execute_1 s) = current_instruction_cost s + clock … s.
     739 #s whd in match execute_1; normalize nodelta @sig2
     740qed-. (*x Andrea: indexing takes ages here *)
    807741
    808742definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
Note: See TracChangeset for help on using the changeset viewer.