Changeset 1710 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Feb 20, 2012, 10:04:54 AM (8 years ago)
Author:
mulligan
Message:

changes from friday afternoon

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1709 r1710  
    120120include alias "ASM/BitVectorTrie.ma".
    121121
     122definition ASM_classify00: ∀a. preinstruction a → status_class ≝
     123  λa, pre.
     124  match pre with
     125  [ RET ⇒ cl_return
     126  | RETI ⇒ cl_return
     127  | JZ _ ⇒ cl_jump
     128  | JNZ _ ⇒ cl_jump
     129  | JC _ ⇒ cl_jump
     130  | JNC _ ⇒ cl_jump
     131  | JB _ _ ⇒ cl_jump
     132  | JNB _ _ ⇒ cl_jump
     133  | JBC _ _ ⇒ cl_jump
     134  | CJNE _ _ ⇒ cl_jump
     135  | DJNZ _ _ ⇒ cl_jump
     136  | _ ⇒ cl_other
     137  ].
     138
    122139definition ASM_classify0: instruction → status_class ≝
    123   λi: instruction.
     140  λi.
    124141  match i with
    125    [ RealInstruction pre ⇒
    126      match pre with
    127       [ RET ⇒ cl_return
    128       | JZ _ ⇒ cl_jump
    129       | JNZ _ ⇒ cl_jump
    130       | JC _ ⇒ cl_jump
    131       | JNC _ ⇒ cl_jump
    132       | JB _ _ ⇒ cl_jump
    133       | JNB _ _ ⇒ cl_jump
    134       | JBC _ _ ⇒ cl_jump
    135       | CJNE _ _ ⇒ cl_jump
    136       | DJNZ _ _ ⇒ cl_jump
    137       | _ ⇒ cl_other
    138       ]
     142   [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
    139143   | ACALL _ ⇒ cl_call
    140144   | LCALL _ ⇒ cl_call
     
    163167definition execute_1_preinstruction':
    164168  ∀ticks: nat × nat.
    165   ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
     169  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
    166170  ∀s: PreStatus m cm.
    167171    Σs': PreStatus m cm.
    168172      And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
    169         (ASM_classify cm s' = cl_other → program_counter … s' = \fst (\snd (fetch … s))) ≝
     173        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝
    170174  λticks: nat × nat.
    171175  λa, m: Type[0]. λcm.
     
    175179  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
    176180  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
    177   match instr in preinstruction return λx. Σs': ?. ? with
    178         [ ADD addr1 addr2 ⇒
     181  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
     182    And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
     183      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with
     184        [ ADD addr1 addr2 ⇒ λinstr_refl.
    179185            let s ≝ add_ticks1 s in
    180186            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     
    185191            let s ≝ set_arg_8 … s ACC_A result in
    186192              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
    187         | ADDC addr1 addr2 ⇒
     193        | ADDC addr1 addr2 ⇒ λinstr_refl.
    188194            let s ≝ add_ticks1 s in
    189195            let old_cy_flag ≝ get_cy_flag ?? s in
     
    195201            let s ≝ set_arg_8 … s ACC_A result in
    196202              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
    197         | SUBB addr1 addr2 ⇒
     203        | SUBB addr1 addr2 ⇒ λinstr_refl.
    198204            let s ≝ add_ticks1 s in
    199205            let old_cy_flag ≝ get_cy_flag ?? s in
     
    205211            let s ≝ set_arg_8 … s ACC_A result in
    206212              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
    207         | ANL addr ⇒
     213        | ANL addr ⇒ λinstr_refl.
    208214          let s ≝ add_ticks1 s in
    209215          match addr with
     
    224230               set_flags … s and_val (None ?) (get_ov_flag ?? s)
    225231            ]
    226         | ORL addr ⇒
     232        | ORL addr ⇒ λinstr_refl.
    227233          let s ≝ add_ticks1 s in
    228234          match addr with
     
    243249               set_flags … s or_val (None ?) (get_ov_flag … s)
    244250            ]
    245         | XRL addr ⇒
     251        | XRL addr ⇒ λinstr_refl.
    246252          let s ≝ add_ticks1 s in
    247253          match addr with
     
    255261                set_arg_8 … s addr1 xor_val
    256262            ]
    257         | INC addr ⇒
    258             match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     263        | INC addr ⇒ λinstr_refl.
     264            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
    259265              [ ACC_A ⇒ λacc_a: True.
    260266                let s' ≝ add_ticks1 s in
     
    281287              | _ ⇒ λother: False. ⊥
    282288              ] (subaddressing_modein … addr)
    283         | NOP ⇒
     289        | NOP ⇒ λinstr_refl.
    284290           let s ≝ add_ticks2 s in
    285291            s
    286         | DEC addr ⇒
     292        | DEC addr ⇒ λinstr_refl.
    287293           let s ≝ add_ticks1 s in
    288294           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
    289295             set_arg_8 … s addr result
    290         | MUL addr1 addr2 ⇒
     296        | MUL addr1 addr2 ⇒ λinstr_refl.
    291297           let s ≝ add_ticks1 s in
    292298           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     
    298304           let s ≝ set_8051_sfr … s SFR_ACC_A low in
    299305             set_8051_sfr … s SFR_ACC_B high
    300         | DIV addr1 addr2 ⇒
     306        | DIV addr1 addr2 ⇒ λinstr_refl.
    301307           let s ≝ add_ticks1 s in
    302308           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     
    311317                   set_flags … s false (None Bit) false
    312318               ]
    313         | DA addr ⇒
     319        | DA addr ⇒ λinstr_refl.
    314320            let s ≝ add_ticks1 s in
    315321            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     
    327333              else
    328334                s
    329         | CLR addr ⇒
    330           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     335        | CLR addr ⇒ λinstr_refl.
     336          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
    331337            [ ACC_A ⇒ λacc_a: True.
    332338              let s ≝ add_ticks1 s in
     
    340346            | _ ⇒ λother: False. ⊥
    341347            ] (subaddressing_modein … addr)
    342         | CPL addr ⇒
    343           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     348        | CPL addr ⇒ λinstr_refl.
     349          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
    344350            [ ACC_A ⇒ λacc_a: True.
    345351                let s ≝ add_ticks1 s in
     
    359365            | _ ⇒ λother: False. ?
    360366            ] (subaddressing_modein … addr)
    361         | SETB b ⇒
     367        | SETB b ⇒ λinstr_refl.
    362368            let s ≝ add_ticks1 s in
    363369            set_arg_1 … s b false
    364         | RL _ ⇒ (* DPM: always ACC_A *)
     370        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    365371            let s ≝ add_ticks1 s in
    366372            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    367373            let new_acc ≝ rotate_left … 1 old_acc in
    368374              set_8051_sfr … s SFR_ACC_A new_acc
    369         | RR _ ⇒ (* DPM: always ACC_A *)
     375        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    370376            let s ≝ add_ticks1 s in
    371377            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    372378            let new_acc ≝ rotate_right … 1 old_acc in
    373379              set_8051_sfr … s SFR_ACC_A new_acc
    374         | RLC _ ⇒ (* DPM: always ACC_A *)
     380        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    375381            let s ≝ add_ticks1 s in
    376382            let old_cy_flag ≝ get_cy_flag ?? s in
     
    380386            let s ≝ set_arg_1 … s CARRY new_cy_flag in
    381387              set_8051_sfr … s SFR_ACC_A new_acc
    382         | RRC _ ⇒ (* DPM: always ACC_A *)
     388        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    383389            let s ≝ add_ticks1 s in
    384390            let old_cy_flag ≝ get_cy_flag ?? s in
     
    388394            let s ≝ set_arg_1 … s CARRY new_cy_flag in
    389395              set_8051_sfr … s SFR_ACC_A new_acc
    390         | SWAP _ ⇒ (* DPM: always ACC_A *)
     396        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    391397            let s ≝ add_ticks1 s in
    392398            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     
    394400            let new_acc ≝ nl @@ nu in
    395401              set_8051_sfr … s SFR_ACC_A new_acc
    396         | PUSH addr ⇒
    397             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     402        | PUSH addr ⇒ λinstr_refl.
     403            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
    398404              [ DIRECT d ⇒ λdirect: True.
    399405                let s ≝ add_ticks1 s in
     
    403409              | _ ⇒ λother: False. ⊥
    404410              ] (subaddressing_modein … addr)
    405         | POP addr ⇒
     411        | POP addr ⇒ λinstr_refl.
    406412            let s ≝ add_ticks1 s in
    407413            let contents ≝ read_at_stack_pointer ?? s in
     
    409415            let s ≝ set_8051_sfr … s SFR_SP new_sp in
    410416              set_arg_8 … s addr contents
    411         | XCH addr1 addr2 ⇒
     417        | XCH addr1 addr2 ⇒ λinstr_refl.
    412418            let s ≝ add_ticks1 s in
    413419            let old_addr ≝ get_arg_8 … s false addr2 in
     
    415421            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
    416422              set_arg_8 … s addr2 old_acc
    417         | XCHD addr1 addr2 ⇒
     423        | XCHD addr1 addr2 ⇒ λinstr_refl.
    418424            let s ≝ add_ticks1 s in
    419425            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     
    421427            let new_acc ≝ acc_nu @@ arg_nl in
    422428            let new_arg ≝ arg_nu @@ acc_nl in
    423             let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     429            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
    424430              set_arg_8 … s addr2 new_arg
    425         | RET ⇒
     431        | RET ⇒ λinstr_refl.
    426432            let s ≝ add_ticks1 s in
    427433            let high_bits ≝ read_at_stack_pointer ?? s in
     
    433439            let new_pc ≝ high_bits @@ low_bits in
    434440              set_program_counter … s new_pc
    435         | RETI ⇒
     441        | RETI ⇒ λinstr_refl.
    436442            let s ≝ add_ticks1 s in
    437443            let high_bits ≝ read_at_stack_pointer ?? s in
     
    443449            let new_pc ≝ high_bits @@ low_bits in
    444450              set_program_counter … s new_pc
    445         | MOVX addr ⇒
     451        | MOVX addr ⇒ λinstr_refl.
    446452          let s ≝ add_ticks1 s in
    447453          (* DPM: only copies --- doesn't affect I/O *)
     
    454460                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    455461            ]
    456         | MOV addr ⇒
     462        | MOV addr ⇒ λinstr_refl.
    457463          let s ≝ add_ticks1 s in
    458464          match addr with
     
    488494               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
    489495            ]
    490           | JC addr ⇒
     496          | JC addr ⇒ λinstr_refl.
    491497                  if get_cy_flag ?? s then
    492498                    let s ≝ add_ticks1 s in
     
    495501                    let s ≝ add_ticks2 s in
    496502                      s
    497             | JNC addr ⇒
     503            | JNC addr ⇒ λinstr_refl.
    498504                  if ¬(get_cy_flag ?? s) then
    499505                   let s ≝ add_ticks1 s in
     
    502508                   let s ≝ add_ticks2 s in
    503509                    s
    504             | JB addr1 addr2 ⇒
     510            | JB addr1 addr2 ⇒ λinstr_refl.
    505511                  if get_arg_1 … s addr1 false then
    506512                   let s ≝ add_ticks1 s in
     
    509515                   let s ≝ add_ticks2 s in
    510516                    s
    511             | JNB addr1 addr2 ⇒
     517            | JNB addr1 addr2 ⇒ λinstr_refl.
    512518                  if ¬(get_arg_1 … s addr1 false) then
    513519                   let s ≝ add_ticks1 s in
     
    516522                   let s ≝ add_ticks2 s in
    517523                    s
    518             | JBC addr1 addr2 ⇒
     524            | JBC addr1 addr2 ⇒ λinstr_refl.
    519525                  let s ≝ set_arg_1 … s addr1 false in
    520526                    if get_arg_1 … s addr1 false then
     
    524530                     let s ≝ add_ticks2 s in
    525531                      s
    526             | JZ addr ⇒
     532            | JZ addr ⇒ λinstr_refl.
    527533                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
    528534                     let s ≝ add_ticks1 s in
     
    531537                     let s ≝ add_ticks2 s in
    532538                      s
    533             | JNZ addr ⇒
     539            | JNZ addr ⇒ λinstr_refl.
    534540                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
    535541                     let s ≝ add_ticks1 s in
     
    538544                     let s ≝ add_ticks2 s in
    539545                      s
    540             | CJNE addr1 addr2 ⇒
     546            | CJNE addr1 addr2 ⇒ λinstr_refl.
    541547                  match addr1 with
    542548                    [ inl l ⇒
     
    563569                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    564570                    ]
    565             | DJNZ addr1 addr2 ⇒
     571            | DJNZ addr1 addr2 ⇒ λinstr_refl.
    566572              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
    567573              let s ≝ set_arg_8 … s addr1 result in
     
    572578                 let s ≝ add_ticks2 s in
    573579                  s
    574  |_ ⇒ ?            ]. (*15s*)
     580            ] (refl … instr).
    575581    try (cases(other))
    576582    try assumption (*20s*)
    577583    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    578584    try (
    579       @ (execute_1_technical … (subaddressing_modein …))
    580       @ I
     585      @(execute_1_technical … (subaddressing_modein …))
     586      @I
    581587    ) (*66s*)
    582     normalize nodelta /2 by or_introl, or_intror/ (*35s*)
    583     (*CSC: the times are now much longer. I suspect because the inclusion of
    584       all StatusProofs makes the search space larger :-( *)
     588    normalize nodelta %
     589    try (<instr_refl change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
     590    try (<instr_refl change with (cl_return = cl_other → ?) #absurd destruct(absurd))
     591    try (@or_introl //)
     592    try (@or_intror //)
     593    #_ /demod/ %
    585594qed.
    586595
     
    592601lemma execute_1_preinstruction_ok:
    593602 ∀ticks,a,m,cm,f,i,s.
    594   clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
    595   clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s.
     603  (clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
     604  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
     605    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
    596606 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
    597607qed.
     
    707717    #absurd normalize in absurd; try destruct(absurd) try %
    708718  |9:
    709    
    710     [1,2,3,4,5,7: @pi2 (*35s*)
    711     |8: cases daemon (*
    712     lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] …
     719    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
    713720        (λx. λs.
    714721        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    715722        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
    716723        | _ ⇒ λabsd. ⊥
    717         ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H *)
    718       (*XXX : propagate further *)
    719     |28,48,68,88,108,128: skip
    720     |*:
    721       try assumption
    722        normalize nodelta
    723        try // >clock_set_program_counter %
    724        try // destruct destruct (* XXX: for wilmer! *) >e1
    725        whd in match ASM_classify; normalize nodelta
    726        whd in match current_instruction; normalize nodelta
    727        whd in match current_instruction0; normalize nodelta
    728     [||||||||*:try assumption]
    729     |*: normalize nodelta try // (*17s*)
    730         >clock_set_program_counter // (* Andrea:??*) ]
     724        ] (subaddressing_modein … x)) instr' s) try @absd
     725    #clock_proof #classify_proof %
     726    [1:
     727      cases clock_proof #clock_proof' >clock_proof'
     728      destruct(INSTR_PC_TICKS) %
     729    |2:
     730      #classify_assm -clock_proof >classify_proof -classify_proof
     731      [1:
     732        normalize nodelta normalize <INSTR_PC_TICKS
     733        destruct(INSTR_PC) %
     734      |2:
     735        <classify_assm <INSTR_PC_TICKS destruct <e0 %
     736      ]
     737    ]
     738  ]
    731739qed.
    732740
     
    736744
    737745definition execute_1': ∀cm.∀s:Status cm.
    738   Σs':Status cm. clock ?? s' = current_instruction_cost cm s + clock … s ≝
     746  Σs':Status cm.
     747    And (clock ?? s' = current_instruction_cost cm s + clock … s)
     748      (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … s') ≝
    739749  λcm. λs: Status cm.
    740     let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    741      execute_1_0 cm s instr_pc_ticks.
     750  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     751    pi1 ?? (execute_1_0 cm s instr_pc_ticks).
     752  %
     753  [1:
     754    cases(execute_1_0 cm s instr_pc_ticks)
     755    #the_status * #clock_assm #_ @clock_assm
     756  |2:
     757    cases(execute_1_0 cm s instr_pc_ticks)
     758    #the_status * #_ #classify_assm #classify_assm'
     759    lapply(classify_assm ?)
     760    [1:
     761      change with (
     762        ASM_classify cm s = cl_other
     763      )
     764      assumption
     765    |2:
     766      #program_counter_refl >program_counter_refl %
     767    ]
     768  ]
     769qed.
    742770
    743771definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
    744772
    745 lemma execute_1_ok: ∀cm.∀s. clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
     773lemma execute_1_ok: ∀cm.∀s.
     774  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
     775    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)).
    746776 #cm #s whd in match execute_1; normalize nodelta @pi2
    747777qed-. (*x Andrea: indexing takes ages here *)
Note: See TracChangeset for help on using the changeset viewer.