Changeset 1971 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 20, 2012, 10:34:31 PM (7 years ago)
Author:
sacerdot
Message:
  1. Interpret.ma: we need to prove \sigma (execute_preinstruction s) = execute_preinstruction (\sigma s)

Thus execute_preinstruction cannot be defined using Russell.
Changed, but the proof of the properties still uses Russell
(with a trick...)

  1. AssemblyProofSplit?: the preinstruction case of the main theorem moved to a main lemma which is also proved using the Russell trick. This seems very promising ATM.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1969 r1971  
    112112include alias "ASM/BitVectorTrie.ma".
    113113
    114 definition execute_1_preinstruction':
     114definition execute_1_preinstruction:
    115115  ∀ticks: nat × nat.
    116116  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
    117   ∀s: PreStatus m cm.
    118     Σs': PreStatus m cm.
    119       And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
    120         (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝
     117  ∀s: PreStatus m cm. PreStatus m cm ≝
    121118  λticks: nat × nat.
    122119  λa, m: Type[0]. λcm.
     
    126123  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
    127124  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
    128   match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
    129     And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
    130       (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with
     125  match instr in preinstruction return λx. x = instr → PreStatus m cm with
    131126        [ ADD addr1 addr2 ⇒ λinstr_refl.
    132127            let s ≝ add_ticks1 s in
     
    533528      @I
    534529    ) (*66s*)
     530qed.
     531
     532definition execute_1_preinstruction_ok':
     533  ∀ticks: nat × nat.
     534  ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a.
     535  ∀s: PreStatus m cm.
     536    Σs': PreStatus m cm.
     537      (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in
     538      (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
     539        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝
     540  λticks: nat × nat.
     541  λa, m: Type[0]. λcm.
     542  λaddr_of: a → PreStatus m cm → Word.
     543  λinstr: preinstruction a.
     544  λs: PreStatus m cm.
     545  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
     546  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
     547  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
     548    ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
     549      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with
     550        [ ADD addr1 addr2 ⇒ λinstr_refl.
     551            let s ≝ add_ticks1 s in
     552            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     553                                                   (get_arg_8 … s false addr2) false in
     554            let cy_flag ≝ get_index' ? O  ? flags in
     555            let ac_flag ≝ get_index' ? 1 ? flags in
     556            let ov_flag ≝ get_index' ? 2 ? flags in
     557            let s ≝ set_arg_8 … s ACC_A result in
     558              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     559        | ADDC addr1 addr2 ⇒ λinstr_refl.
     560            let s ≝ add_ticks1 s in
     561            let old_cy_flag ≝ get_cy_flag ?? s in
     562            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     563                                                   (get_arg_8 … s false addr2) old_cy_flag in
     564            let cy_flag ≝ get_index' ? O ? flags in
     565            let ac_flag ≝ get_index' ? 1 ? flags in
     566            let ov_flag ≝ get_index' ? 2 ? flags in
     567            let s ≝ set_arg_8 … s ACC_A result in
     568              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     569        | SUBB addr1 addr2 ⇒ λinstr_refl.
     570            let s ≝ add_ticks1 s in
     571            let old_cy_flag ≝ get_cy_flag ?? s in
     572            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
     573                                                   (get_arg_8 … s false addr2) old_cy_flag in
     574            let cy_flag ≝ get_index' ? O ? flags in
     575            let ac_flag ≝ get_index' ? 1 ? flags in
     576            let ov_flag ≝ get_index' ? 2 ? flags in
     577            let s ≝ set_arg_8 … s ACC_A result in
     578              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     579        | ANL addr ⇒ λinstr_refl.
     580          let s ≝ add_ticks1 s in
     581          match addr with
     582            [ inl l ⇒
     583              match l with
     584                [ inl l' ⇒
     585                  let 〈addr1, addr2〉 ≝ l' in
     586                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     587                    set_arg_8 … s addr1 and_val
     588                | inr r ⇒
     589                  let 〈addr1, addr2〉 ≝ r in
     590                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     591                    set_arg_8 … s addr1 and_val
     592                ]
     593            | inr r ⇒
     594              let 〈addr1, addr2〉 ≝ r in
     595              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
     596               set_flags … s and_val (None ?) (get_ov_flag ?? s)
     597            ]
     598        | ORL addr ⇒ λinstr_refl.
     599          let s ≝ add_ticks1 s in
     600          match addr with
     601            [ inl l ⇒
     602              match l with
     603                [ inl l' ⇒
     604                  let 〈addr1, addr2〉 ≝ l' in
     605                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     606                    set_arg_8 … s addr1 or_val
     607                | inr r ⇒
     608                  let 〈addr1, addr2〉 ≝ r in
     609                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     610                    set_arg_8 … s addr1 or_val
     611                ]
     612            | inr r ⇒
     613              let 〈addr1, addr2〉 ≝ r in
     614              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
     615               set_flags … s or_val (None ?) (get_ov_flag … s)
     616            ]
     617        | XRL addr ⇒ λinstr_refl.
     618          let s ≝ add_ticks1 s in
     619          match addr with
     620            [ inl l' ⇒
     621              let 〈addr1, addr2〉 ≝ l' in
     622              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     623                set_arg_8 … s addr1 xor_val
     624            | inr r ⇒
     625              let 〈addr1, addr2〉 ≝ r in
     626              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     627                set_arg_8 … s addr1 xor_val
     628            ]
     629        | INC addr ⇒ λinstr_refl.
     630            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with
     631              [ ACC_A ⇒ λacc_a: True. λEQaddr.
     632                let s' ≝ add_ticks1 s in
     633                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
     634                 set_arg_8 … s' ACC_A result
     635              | REGISTER r ⇒ λregister: True. λEQaddr.
     636                let s' ≝ add_ticks1 s in
     637                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     638                 set_arg_8 … s' (REGISTER r) result
     639              | DIRECT d ⇒ λdirect: True. λEQaddr.
     640                let s' ≝ add_ticks1 s in
     641                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     642                 set_arg_8 … s' (DIRECT d) result
     643              | INDIRECT i ⇒ λindirect: True. λEQaddr.
     644                let s' ≝ add_ticks1 s in
     645                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     646                 set_arg_8 … s' (INDIRECT i) result
     647              | DPTR ⇒ λdptr: True. λEQaddr.
     648                let s' ≝ add_ticks1 s in
     649                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
     650                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
     651                let s ≝ set_8051_sfr … s' SFR_DPL bl in
     652                 set_8051_sfr … s' SFR_DPH bu
     653              | _ ⇒ λother: False. ⊥
     654              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
     655        | NOP ⇒ λinstr_refl.
     656           let s ≝ add_ticks2 s in
     657            s
     658        | DEC addr ⇒ λinstr_refl.
     659           let s ≝ add_ticks1 s in
     660           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
     661             set_arg_8 … s addr result
     662        | MUL addr1 addr2 ⇒ λinstr_refl.
     663           let s ≝ add_ticks1 s in
     664           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     665           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
     666           let product ≝ acc_a_nat * acc_b_nat in
     667           let ov_flag ≝ product ≥ 256 in
     668           let low ≝ bitvector_of_nat 8 (product mod 256) in
     669           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
     670           let s ≝ set_8051_sfr … s SFR_ACC_A low in
     671             set_8051_sfr … s SFR_ACC_B high
     672        | DIV addr1 addr2 ⇒ λinstr_refl.
     673           let s ≝ add_ticks1 s in
     674           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     675           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
     676             match acc_b_nat with
     677               [ O ⇒ set_flags … s false (None Bit) true
     678               | S o ⇒
     679                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
     680                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
     681                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
     682                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
     683                   set_flags … s false (None Bit) false
     684               ]
     685        | DA addr ⇒ λinstr_refl.
     686            let s ≝ add_ticks1 s in
     687            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     688              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
     689                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
     690                let cy_flag ≝ get_index' ? O ? flags in
     691                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     692                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
     693                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     694                    let new_acc ≝ nu @@ acc_nl' in
     695                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
     696                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
     697                  else
     698                    s
     699              else
     700                s
     701        | CLR addr ⇒ λinstr_refl.
     702          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
     703            [ ACC_A ⇒ λacc_a: True. λEQaddr.
     704              let s ≝ add_ticks1 s in
     705               set_arg_8 … s ACC_A (zero 8)
     706            | CARRY ⇒ λcarry: True. λEQaddr.
     707              let s ≝ add_ticks1 s in
     708               set_arg_1 … s CARRY false
     709            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
     710              let s ≝ add_ticks1 s in
     711               set_arg_1 … s (BIT_ADDR b) false
     712            | _ ⇒ λother: False. ⊥
     713            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     714        | CPL addr ⇒ λinstr_refl.
     715          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
     716            [ ACC_A ⇒ λacc_a: True. λEQaddr.
     717                let s ≝ add_ticks1 s in
     718                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     719                let new_acc ≝ negation_bv ? old_acc in
     720                 set_8051_sfr … s SFR_ACC_A new_acc
     721            | CARRY ⇒ λcarry: True. λEQaddr.
     722                let s ≝ add_ticks1 s in
     723                let old_cy_flag ≝ get_arg_1 … s CARRY true in
     724                let new_cy_flag ≝ ¬old_cy_flag in
     725                 set_arg_1 … s CARRY new_cy_flag
     726            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
     727                let s ≝ add_ticks1 s in
     728                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
     729                let new_bit ≝ ¬old_bit in
     730                 set_arg_1 … s (BIT_ADDR b) new_bit
     731            | _ ⇒ λother: False. ?
     732            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     733        | SETB b ⇒ λinstr_refl.
     734            let s ≝ add_ticks1 s in
     735            set_arg_1 … s b false
     736        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     737            let s ≝ add_ticks1 s in
     738            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     739            let new_acc ≝ rotate_left … 1 old_acc in
     740              set_8051_sfr … s SFR_ACC_A new_acc
     741        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     742            let s ≝ add_ticks1 s in
     743            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     744            let new_acc ≝ rotate_right … 1 old_acc in
     745              set_8051_sfr … s SFR_ACC_A new_acc
     746        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     747            let s ≝ add_ticks1 s in
     748            let old_cy_flag ≝ get_cy_flag ?? s in
     749            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     750            let new_cy_flag ≝ get_index' ? O ? old_acc in
     751            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
     752            let s ≝ set_arg_1 … s CARRY new_cy_flag in
     753              set_8051_sfr … s SFR_ACC_A new_acc
     754        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     755            let s ≝ add_ticks1 s in
     756            let old_cy_flag ≝ get_cy_flag ?? s in
     757            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     758            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
     759            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
     760            let s ≝ set_arg_1 … s CARRY new_cy_flag in
     761              set_8051_sfr … s SFR_ACC_A new_acc
     762        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     763            let s ≝ add_ticks1 s in
     764            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     765            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     766            let new_acc ≝ nl @@ nu in
     767              set_8051_sfr … s SFR_ACC_A new_acc
     768        | PUSH addr ⇒ λinstr_refl.
     769            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with
     770              [ DIRECT d ⇒ λdirect: True. λEQaddr.
     771                let s ≝ add_ticks1 s in
     772                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     773                let s ≝ set_8051_sfr … s SFR_SP new_sp in
     774                  write_at_stack_pointer … s d
     775              | _ ⇒ λother: False. ⊥
     776              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     777        | POP addr ⇒ λinstr_refl.
     778            let s ≝ add_ticks1 s in
     779            let contents ≝ read_at_stack_pointer ?? s in
     780            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     781            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     782              set_arg_8 … s addr contents
     783        | XCH addr1 addr2 ⇒ λinstr_refl.
     784            let s ≝ add_ticks1 s in
     785            let old_addr ≝ get_arg_8 … s false addr2 in
     786            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     787            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
     788              set_arg_8 … s addr2 old_acc
     789        | XCHD addr1 addr2 ⇒ λinstr_refl.
     790            let s ≝ add_ticks1 s in
     791            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     792            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     793            let new_acc ≝ acc_nu @@ arg_nl in
     794            let new_arg ≝ arg_nu @@ acc_nl in
     795            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
     796              set_arg_8 … s addr2 new_arg
     797        | RET ⇒ λinstr_refl.
     798            let s ≝ add_ticks1 s in
     799            let high_bits ≝ read_at_stack_pointer ?? s in
     800            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     801            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     802            let low_bits ≝ read_at_stack_pointer ?? s in
     803            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     804            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     805            let new_pc ≝ high_bits @@ low_bits in
     806              set_program_counter … s new_pc
     807        | RETI ⇒ λinstr_refl.
     808            let s ≝ add_ticks1 s in
     809            let high_bits ≝ read_at_stack_pointer ?? s in
     810            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     811            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     812            let low_bits ≝ read_at_stack_pointer ?? s in
     813            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     814            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     815            let new_pc ≝ high_bits @@ low_bits in
     816              set_program_counter … s new_pc
     817        | MOVX addr ⇒ λinstr_refl.
     818          let s ≝ add_ticks1 s in
     819          (* DPM: only copies --- doesn't affect I/O *)
     820          match addr with
     821            [ inl l ⇒
     822              let 〈addr1, addr2〉 ≝ l in
     823                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     824            | inr r ⇒
     825              let 〈addr1, addr2〉 ≝ r in
     826                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     827            ]
     828        | MOV addr ⇒ λinstr_refl.
     829          let s ≝ add_ticks1 s in
     830          match addr with
     831            [ inl l ⇒
     832              match l with
     833                [ inl l' ⇒
     834                  match l' with
     835                    [ inl l'' ⇒
     836                      match l'' with
     837                        [ inl l''' ⇒
     838                          match l''' with
     839                            [ inl l'''' ⇒
     840                              let 〈addr1, addr2〉 ≝ l'''' in
     841                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     842                            | inr r'''' ⇒
     843                              let 〈addr1, addr2〉 ≝ r'''' in
     844                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     845                            ]
     846                        | inr r''' ⇒
     847                          let 〈addr1, addr2〉 ≝ r''' in
     848                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     849                        ]
     850                    | inr r'' ⇒
     851                      let 〈addr1, addr2〉 ≝ r'' in
     852                       set_arg_16 … s (get_arg_16 … s addr2) addr1
     853                    ]
     854                | inr r ⇒
     855                  let 〈addr1, addr2〉 ≝ r in
     856                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
     857                ]
     858            | inr r ⇒
     859              let 〈addr1, addr2〉 ≝ r in
     860               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
     861            ]
     862          | JC addr ⇒ λinstr_refl.
     863                  if get_cy_flag ?? s then
     864                    let s ≝ add_ticks1 s in
     865                      set_program_counter … s (addr_of addr s)
     866                  else
     867                    let s ≝ add_ticks2 s in
     868                      s
     869            | JNC addr ⇒ λinstr_refl.
     870                  if ¬(get_cy_flag ?? s) then
     871                   let s ≝ add_ticks1 s in
     872                     set_program_counter … s (addr_of addr s)
     873                  else
     874                   let s ≝ add_ticks2 s in
     875                    s
     876            | JB addr1 addr2 ⇒ λinstr_refl.
     877                  if get_arg_1 … s addr1 false then
     878                   let s ≝ add_ticks1 s in
     879                    set_program_counter … s (addr_of addr2 s)
     880                  else
     881                   let s ≝ add_ticks2 s in
     882                    s
     883            | JNB addr1 addr2 ⇒ λinstr_refl.
     884                  if ¬(get_arg_1 … s addr1 false) then
     885                   let s ≝ add_ticks1 s in
     886                    set_program_counter … s (addr_of addr2 s)
     887                  else
     888                   let s ≝ add_ticks2 s in
     889                    s
     890            | JBC addr1 addr2 ⇒ λinstr_refl.
     891                  let s ≝ set_arg_1 … s addr1 false in
     892                    if get_arg_1 … s addr1 false then
     893                     let s ≝ add_ticks1 s in
     894                      set_program_counter … s (addr_of addr2 s)
     895                    else
     896                     let s ≝ add_ticks2 s in
     897                      s
     898            | JZ addr ⇒ λinstr_refl.
     899                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
     900                     let s ≝ add_ticks1 s in
     901                      set_program_counter … s (addr_of addr s)
     902                    else
     903                     let s ≝ add_ticks2 s in
     904                      s
     905            | JNZ addr ⇒ λinstr_refl.
     906                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
     907                     let s ≝ add_ticks1 s in
     908                      set_program_counter … s (addr_of addr s)
     909                    else
     910                     let s ≝ add_ticks2 s in
     911                      s
     912            | CJNE addr1 addr2 ⇒ λinstr_refl.
     913                  match addr1 with
     914                    [ inl l ⇒
     915                        let 〈addr1, addr2'〉 ≝ l in
     916                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
     917                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
     918                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
     919                            let s ≝ add_ticks1 s in
     920                            let s ≝ set_program_counter … s (addr_of addr2 s) in
     921                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     922                          else
     923                            let s ≝ add_ticks2 s in
     924                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     925                    | inr r' ⇒
     926                        let 〈addr1, addr2'〉 ≝ r' in
     927                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
     928                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
     929                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
     930                            let s ≝ add_ticks1 s in
     931                            let s ≝ set_program_counter … s (addr_of addr2 s) in
     932                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     933                          else
     934                            let s ≝ add_ticks2 s in
     935                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     936                    ]
     937            | DJNZ addr1 addr2 ⇒ λinstr_refl.
     938              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
     939              let s ≝ set_arg_8 … s addr1 result in
     940                if ¬(eq_bv ? result (zero 8)) then
     941                 let s ≝ add_ticks1 s in
     942                  set_program_counter … s (addr_of addr2 s)
     943                else
     944                 let s ≝ add_ticks2 s in
     945                  s
     946            ] (refl … instr).
     947    try (cases(other))
     948    try assumption (*20s*)
     949    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
     950    try (
     951      @(execute_1_technical … (subaddressing_modein …))
     952      @I
     953    ) (*66s*)
     954    whd in match execute_1_preinstruction;
    535955    normalize nodelta %
    536     try (<instr_refl change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
    537     try (<instr_refl change with (cl_return = cl_other → ?) #absurd destruct(absurd))
     956    [21,22,23,24: (* DIV *)
     957     normalize nodelta in p;
     958    |7,8,9,10,11,12,13,14,15,16, (* INC *)
     959     71,72,73,74,75,76, (* CLR *)
     960     77,78,79,80,81,82, (* CPL *)
     961     99,100: (* PUSH *)
     962      lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b
     963    |93,94: (* MOV *)
     964      cases addr * normalize nodelta
     965       [1,2,4,5: * normalize nodelta
     966        [1,2,4,5: * normalize nodelta
     967         [1,2,4,5: * normalize nodelta
     968          [1,2,4,5: * normalize nodelta ]]]]
     969       #arg1 #arg2
     970    |65,66, (* ANL *)
     971     67,68, (* ORL *)
     972     95,96: (* MOVX*)
     973      cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta
     974    |59,60: (* CJNE *)
     975      cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta
     976      cases (¬(eq_bv ???)) normalize nodelta
     977    |69,70: (* XRL *)
     978      cases addr normalize nodelta * #addr1 #addr2 normalize nodelta
     979    ]
     980    try (>p normalize nodelta
     981         try (>p1 normalize nodelta
     982              try (>p2 normalize nodelta
     983                   try (>p3 normalize nodelta
     984                        try (>p4 normalize nodelta
     985                             try (>p5 normalize nodelta))))))
     986    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
     987    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
    538988    try (@or_introl //)
    539989    try (@or_intror //)
    540     #_ /demod/ %
    541 qed.
    542 
    543 definition execute_1_preinstruction:
    544   ∀ticks: nat × nat.
    545   ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
    546   PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'.
    547  
     990    try (#_ /demod/ %)
     991    try (#_ //)   
     992    [ <set_arg_8_ok @or_introl //
     993    |*: <set_arg_1_ok @or_introl // ]
     994qed.
     995
    548996lemma execute_1_preinstruction_ok:
    549997 ∀ticks,a,m,cm,f,i,s.
     
    551999  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
    5521000    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
    553  #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
     1001 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) //
    5541002qed.
    5551003
Note: See TracChangeset for help on using the changeset viewer.