Changeset 936 for src


Ignore:
Timestamp:
Jun 10, 2011, 4:20:47 PM (9 years ago)
Author:
sacerdot
Message:

Ticks are now handled correctly everywhere and the main proof takes care of
them.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r935 r936  
    834834  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
    835835
     836definition ticks_of_instruction ≝
     837 λi.
     838  let trivial_code_memory ≝ assembly1 i in
     839  let trivial_status ≝ load_code_memory trivial_code_memory in
     840   \snd (fetch trivial_status (zero ?)).
     841
    836842axiom fetch_assembly:
    837843  ∀pc,i,code_memory,assembled.
    … …  
    842848      let 〈instr_pc, ticks〉 ≝ fetched in
    843849      let 〈instr,pc'〉 ≝ instr_pc in
    844        (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
     850       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
    845851(* #pc #i #code_memory #assembled cases i [8: *]
    846852 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
    … …  
    876882     let 〈instr_pc, ticks〉 ≝ fetched in
    877883     let 〈instr,pc'〉 ≝ instr_pc in
    878       eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl].
     884      eq_instruction instr i = true ∧
     885      ticks = (ticks_of_instruction i) ∧
     886      fetch_many code_memory final_pc pc' tl].
    879887
    880888lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
    … …  
    887895
    888896axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
     897
     898axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
    889899
    890900lemma fetch_assembly_pseudo:
    … …  
    906916    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
    907917    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
    908     cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % //
    909     >(eq_bv_to_eq … K2) @IH @H2 ]
     918    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
     919    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try % //
     920    [ @eqb_true_to_eq <(eq_instruction_to_eq … K1) // | >(eq_bv_to_eq … K3) @IH @H2 ]
    910921qed.
    911922
    … …  
    16021613qed.
    16031614
    1604 definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
     1615definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
    16051616  λprogram: pseudo_assembly_program.
    16061617  λppc: Word.
    1607     let 〈preamble, pseudo〉 ≝ program in
    1608     let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
     1618  λfetched.
    16091619    match fetched with
    16101620    [ Instruction instr ⇒
    … …  
    16641674        | long_jump ⇒ 〈4, 4〉
    16651675        ]
    1666       | ADD arg1 arg2 ⇒
    1667         let trivial_code_memory ≝ assembly1 (ADD ? arg1 arg2) in
    1668         let trivial_status ≝ load_code_memory trivial_code_memory in
    1669         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1670           〈0, ticks〉
     1676      | ADD arg1 arg2 ⇒
     1677        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     1678         〈ticks, ticks〉
    16711679      | ADDC arg1 arg2 ⇒
    1672         let trivial_code_memory ≝ assembly1 (ADDC ? arg1 arg2) in
    1673         let trivial_status ≝ load_code_memory trivial_code_memory in
    1674         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1675           〈0, ticks〉
     1680        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
     1681         〈ticks, ticks〉
    16761682      | SUBB arg1 arg2 ⇒
    1677         let trivial_code_memory ≝ assembly1 (SUBB ? arg1 arg2) in
    1678         let trivial_status ≝ load_code_memory trivial_code_memory in
    1679         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1680           〈0, ticks〉
     1683        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
     1684         〈ticks, ticks〉
    16811685      | INC arg ⇒
    1682         let trivial_code_memory ≝ assembly1 (INC ? arg) in
    1683         let trivial_status ≝ load_code_memory trivial_code_memory in
    1684         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1685           〈0, ticks〉
     1686        let ticks ≝ ticks_of_instruction (INC ? arg) in
     1687         〈ticks, ticks〉
    16861688      | DEC arg ⇒
    1687         let trivial_code_memory ≝ assembly1 (DEC ? arg) in
    1688         let trivial_status ≝ load_code_memory trivial_code_memory in
    1689         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1690           〈0, ticks〉
     1689        let ticks ≝ ticks_of_instruction (DEC ? arg) in
     1690         〈ticks, ticks〉
    16911691      | MUL arg1 arg2 ⇒
    1692         let trivial_code_memory ≝ assembly1 (MUL ? arg1 arg2) in
    1693         let trivial_status ≝ load_code_memory trivial_code_memory in
    1694         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1695           〈0, ticks〉
     1692        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
     1693         〈ticks, ticks〉
    16961694      | DIV arg1 arg2 ⇒
    1697         let trivial_code_memory ≝ assembly1 (DIV ? arg1 arg2) in
    1698         let trivial_status ≝ load_code_memory trivial_code_memory in
    1699         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1700           〈0, ticks〉
     1695        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
     1696         〈ticks, ticks〉
    17011697      | DA arg ⇒
    1702         let trivial_code_memory ≝ assembly1 (DA ? arg) in
    1703         let trivial_status ≝ load_code_memory trivial_code_memory in
    1704         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1705           〈0, ticks〉
     1698        let ticks ≝ ticks_of_instruction (DA ? arg) in
     1699         〈ticks, ticks〉
    17061700      | ANL arg ⇒
    1707         let trivial_code_memory ≝ assembly1 (ANL ? arg) in
    1708         let trivial_status ≝ load_code_memory trivial_code_memory in
    1709         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1710           〈0, ticks〉
     1701        let ticks ≝ ticks_of_instruction (ANL ? arg) in
     1702         〈ticks, ticks〉
    17111703      | ORL arg ⇒
    1712         let trivial_code_memory ≝ assembly1 (ORL ? arg) in
    1713         let trivial_status ≝ load_code_memory trivial_code_memory in
    1714         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1715           〈0, ticks〉
     1704        let ticks ≝ ticks_of_instruction (ORL ? arg) in
     1705         〈ticks, ticks〉
    17161706      | XRL arg ⇒
    1717         let trivial_code_memory ≝ assembly1 (XRL ? arg) in
    1718         let trivial_status ≝ load_code_memory trivial_code_memory in
    1719         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1720           〈0, ticks〉
     1707        let ticks ≝ ticks_of_instruction (XRL ? arg) in
     1708         〈ticks, ticks〉
    17211709      | CLR arg ⇒
    1722         let trivial_code_memory ≝ assembly1 (CLR ? arg) in
    1723         let trivial_status ≝ load_code_memory trivial_code_memory in
    1724         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1725           〈0, ticks〉
     1710        let ticks ≝ ticks_of_instruction (CLR ? arg) in
     1711         〈ticks, ticks〉
    17261712      | CPL arg ⇒
    1727         let trivial_code_memory ≝ assembly1 (CPL ? arg) in
    1728         let trivial_status ≝ load_code_memory trivial_code_memory in
    1729         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1730           〈0, ticks〉
     1713        let ticks ≝ ticks_of_instruction (CPL ? arg) in
     1714         〈ticks, ticks〉
    17311715      | RL arg ⇒
    1732         let trivial_code_memory ≝ assembly1 (RL ? arg) in
    1733         let trivial_status ≝ load_code_memory trivial_code_memory in
    1734         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1735           〈0, ticks〉
     1716        let ticks ≝ ticks_of_instruction (RL ? arg) in
     1717         〈ticks, ticks〉
    17361718      | RLC arg ⇒
    1737         let trivial_code_memory ≝ assembly1 (RLC ? arg) in
    1738         let trivial_status ≝ load_code_memory trivial_code_memory in
    1739         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1740           〈0, ticks〉
     1719        let ticks ≝ ticks_of_instruction (RLC ? arg) in
     1720         〈ticks, ticks〉
    17411721      | RR arg ⇒
    1742         let trivial_code_memory ≝ assembly1 (RR ? arg) in
    1743         let trivial_status ≝ load_code_memory trivial_code_memory in
    1744         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1745           〈0, ticks〉
     1722        let ticks ≝ ticks_of_instruction (RR ? arg) in
     1723         〈ticks, ticks〉
    17461724      | RRC arg ⇒
    1747         let trivial_code_memory ≝ assembly1 (RRC ? arg) in
    1748         let trivial_status ≝ load_code_memory trivial_code_memory in
    1749         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1750           〈0, ticks〉
     1725        let ticks ≝ ticks_of_instruction (RRC ? arg) in
     1726         〈ticks, ticks〉
    17511727      | SWAP arg ⇒
    1752         let trivial_code_memory ≝ assembly1 (SWAP ? arg) in
    1753         let trivial_status ≝ load_code_memory trivial_code_memory in
    1754         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1755           〈0, ticks〉
     1728        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
     1729         〈ticks, ticks〉
    17561730      | MOV arg ⇒
    1757         let trivial_code_memory ≝ assembly1 (MOV ? arg) in
    1758         let trivial_status ≝ load_code_memory trivial_code_memory in
    1759         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1760           〈0, ticks〉
     1731        let ticks ≝ ticks_of_instruction (MOV ? arg) in
     1732         〈ticks, ticks〉
    17611733      | MOVX arg ⇒
    1762         let trivial_code_memory ≝ assembly1 (MOVX ? arg) in
    1763         let trivial_status ≝ load_code_memory trivial_code_memory in
    1764         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1765           〈0, ticks〉
     1734        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
     1735         〈ticks, ticks〉
    17661736      | SETB arg ⇒
    1767         let trivial_code_memory ≝ assembly1 (SETB ? arg) in
    1768         let trivial_status ≝ load_code_memory trivial_code_memory in
    1769         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1770           〈0, ticks〉
     1737        let ticks ≝ ticks_of_instruction (SETB ? arg) in
     1738         〈ticks, ticks〉
    17711739      | PUSH arg ⇒
    1772         let trivial_code_memory ≝ assembly1 (PUSH ? arg) in
    1773         let trivial_status ≝ load_code_memory trivial_code_memory in
    1774         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1775           〈0, ticks〉
     1740        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
     1741         〈ticks, ticks〉
    17761742      | POP arg ⇒
    1777         let trivial_code_memory ≝ assembly1 (POP ? arg) in
    1778         let trivial_status ≝ load_code_memory trivial_code_memory in
    1779         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1780           〈0, ticks〉
     1743        let ticks ≝ ticks_of_instruction (POP ? arg) in
     1744         〈ticks, ticks〉
    17811745      | XCH arg1 arg2 ⇒
    1782         let trivial_code_memory ≝ assembly1 (XCH ? arg1 arg2) in
    1783         let trivial_status ≝ load_code_memory trivial_code_memory in
    1784         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1785           〈0, ticks〉
     1746        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
     1747         〈ticks, ticks〉
    17861748      | XCHD arg1 arg2 ⇒
    1787         let trivial_code_memory ≝ assembly1 (XCHD ? arg1 arg2) in
    1788         let trivial_status ≝ load_code_memory trivial_code_memory in
    1789         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1790           〈0, ticks〉
     1749        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
     1750         〈ticks, ticks〉
    17911751      | RET ⇒
    1792         let trivial_code_memory ≝ assembly1 (RET ?) in
    1793         let trivial_status ≝ load_code_memory trivial_code_memory in
    1794         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1795           〈0, ticks〉
     1752        let ticks ≝ ticks_of_instruction (RET ?) in
     1753         〈ticks, ticks〉
    17961754      | RETI ⇒
    1797         let trivial_code_memory ≝ assembly1 (RETI ?) in
    1798         let trivial_status ≝ load_code_memory trivial_code_memory in
    1799         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1800           〈0, ticks〉
     1755        let ticks ≝ ticks_of_instruction (RETI ?) in
     1756         〈ticks, ticks〉
    18011757      | NOP ⇒
    1802         let trivial_code_memory ≝ assembly1 (NOP ?) in
    1803         let trivial_status ≝ load_code_memory trivial_code_memory in
    1804         let ticks ≝ \snd (fetch trivial_status (zero ?)) in
    1805           〈0, ticks〉
     1758        let ticks ≝ ticks_of_instruction (NOP ?) in
     1759         〈ticks, ticks〉
    18061760      ]
    18071761    | Comment comment ⇒ 〈0, 0〉
    … …  
    18141768qed.
    18151769
    1816 axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
     1770definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
     1771  λprogram: pseudo_assembly_program.
     1772  λppc: Word.
     1773    let 〈preamble, pseudo〉 ≝ program in
     1774    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
     1775     ticks_of0 program ppc fetched.
    18171776
    18181777lemma get_register_set_program_counter:
    … …  
    18441803qed.
    18451804
    1846 lemma set_arg_8_set_program_counter:
    1847   ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
    1848   ∀T,s.∀pc:Word.∀b:l.
    1849    set_arg_8 T (set_program_counter … s pc) b = set_arg_8 … s b.
    1850  [2,3: cases b; *; normalize //]
    1851  #n #l #prf #T #s #pc #b * *;
    1852 qed.
    1853 
    18541805lemma get_arg_8_set_code_memory:
    18551806 ∀T1,T2,s,code_mem,b,arg.
    … …  
    18771828 #T1 #s #f1 #f2 #f3 %
    18781829qed.
    1879 
    1880 axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps.
    18811830
    18821831lemma eq_rect_Type1_r:
    … …  
    18921841
    18931842lemma main_thm:
    1894  ∀ticks_of.
    18951843 ∀ps,s,s''.
    18961844  status_of_pseudo_status ps = Some … s →
    1897   status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' →
     1845  status_of_pseudo_status (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
    18981846   ∃n. execute n s = s''.
    1899  #ticks_of #ps #s #s''
     1847 #ps #s #s''
    19001848 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
    19011849 whd in ⊢ (? → ??%? → ??%? → ?)
    … …  
    19171865  (∃n.
    19181866    execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
    1919    = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?)
     1867   = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) ?)
    19201868 whd in match (\snd 〈preamble,instr_list〉) in H;
    19211869 whd in match (\fst 〈preamble,instr_list〉) in H;
    19221870 whd in match (\snd 〈final_pc,assembled〉) in H;
    19231871 -s s'' labels costs final_ppc final_pc;
    1924  letin ps' ≝ (execute_1_pseudo_instruction ticks_of ps)
     1872 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps)
    19251873 (* NICE STATEMENT HERE *)
    19261874 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
    19271875 #K <K generalize in match K; -K;
    19281876 (* STATEMENT WITH EQUALITY HERE *)
    1929  whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ0 normalize nodelta;
     1877 whd in ⊢ (???(?%?) → ?)
     1878 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
    19301879 cases (fetch_pseudo_instruction instr_list (program_counter … ps))
    19311880 #pi #newppc normalize nodelta; * #instructions *;
    … …  
    19331882  [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0]
    19341883    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    1935     #H2 >(eq_bv_to_eq … H2) >ignore_clock in EQ; #EQ >EQ %
     1884    #H2 >(eq_bv_to_eq … H2) >EQ %
    19361885  |4: (* Jmp *)
    19371886  |5: (* Call *)
    … …  
    19421891       change in ⊢ (? → ??%?) with (execute_1_0 ??)
    19431892       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    1944        * #H2a whd in ⊢ (% → ?) #H2b
    1945        >ignore_clock in EQ;
    1946        >(eq_instruction_to_eq … H2a)
    1947        whd in ⊢ (???% → ??%?);
    1948        >ignore_clock
     1893       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     1894       >H2b >(eq_instruction_to_eq … H2a)
     1895       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
    19491896       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
    19501897       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
    … …  
    19521899       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    19531900       #result #flags
    1954        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; %
     1901       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) %
    19551902    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
    19561903       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    19571904       change in ⊢ (? → ??%?) with (execute_1_0 ??)
    19581905       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    1959        * #H2a whd in ⊢ (% → ?) #H2b
    1960        >ignore_clock in EQ;
    1961        >(eq_instruction_to_eq … H2a)
    1962        whd in ⊢ (???% → ??%?);
    1963        >ignore_clock
     1906       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     1907       >H2b >(eq_instruction_to_eq … H2a)
     1908       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
    19641909       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
    19651910       [1,2,3,4: cases (half_add ???) #carry #result
    19661911       | cases (half_add ???) #carry #bl normalize nodelta;
    19671912         cases (full_add ????) #carry' #bu normalize nodelta ]
    1968         #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
     1913        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
    19691914        [5: %
    1970         |1: >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
    1971 
    1972         XXX
    1973           %
    1974  
     1915        |1:

  • src/ASM/Interpret.ma

    r928 r936  
    159159include alias "ASM/BitVectorTrie.ma".
    160160
    161 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
     161definition execute_1_preinstruction:
     162 ∀ticks: nat × nat.
     163 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
     164  λticks.
    162165  λA, M: Type[0].
    163166  λaddr_of: A → (PreStatus M) → Word.
    164167  λinstr: preinstruction A.
    165168  λs: PreStatus M.
     169  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
     170  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
    166171  match instr with
    167172        [ ADD addr1 addr2 ⇒
     173            let s ≝ add_ticks1 s in
    168174            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
    169175                                                   (get_arg_8 ? s false addr2) false in
    … …  
    174180              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    175181        | ADDC addr1 addr2 ⇒
     182            let s ≝ add_ticks1 s in
    176183            let old_cy_flag ≝ get_cy_flag ? s in
    177184            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
    … …  
    183190              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    184191        | SUBB addr1 addr2 ⇒
     192            let s ≝ add_ticks1 s in
    185193            let old_cy_flag ≝ get_cy_flag ? s in
    186194            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
    … …  
    192200              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    193201        | ANL addr ⇒
     202          let s ≝ add_ticks1 s in
    194203          match addr with
    195204            [ inl l ⇒
    … …  
    210219            ]
    211220        | ORL addr ⇒
     221          let s ≝ add_ticks1 s in
    212222          match addr with
    213223            [ inl l ⇒
    … …  
    228238            ]
    229239        | XRL addr ⇒
     240          let s ≝ add_ticks1 s in
    230241          match addr with
    231242            [ inl l' ⇒
    … …  
    239250            ]
    240251        | INC addr ⇒
     252            let s ≝ add_ticks1 s in
    241253            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    242254                                                           registr;
    … …  
    264276              ] (subaddressing_modein … addr)
    265277        | DEC addr ⇒
     278           let s ≝ add_ticks1 s in
    266279           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
    267280             set_arg_8 ? s addr result
    268281        | MUL addr1 addr2 ⇒
     282           let s ≝ add_ticks1 s in
    269283           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    270284           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
    … …  
    276290             set_8051_sfr ? s SFR_ACC_B high
    277291        | DIV addr1 addr2 ⇒
     292           let s ≝ add_ticks1 s in
    278293           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    279294           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
    … …  
    288303               ]
    289304        | DA addr ⇒
     305            let s ≝ add_ticks1 s in
    290306            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    291307              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
    … …  
    303319                s
    304320        | CLR addr ⇒
     321          let s ≝ add_ticks1 s in
    305322          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    306323            [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
    … …  
    310327            ] (subaddressing_modein … addr)
    311328        | CPL addr ⇒
     329          let s ≝ add_ticks1 s in
    312330          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    313331            [ ACC_A ⇒ λacc_a: True.
    … …  
    325343            | _ ⇒ λother: False. ?
    326344            ] (subaddressing_modein … addr)
    327         | SETB b ⇒ set_arg_1 ? s b false
     345        | SETB b ⇒
     346            let s ≝ add_ticks1 s in
     347            set_arg_1 ? s b false
    328348        | RL _ ⇒ (* DPM: always ACC_A *)
     349            let s ≝ add_ticks1 s in
    329350            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    330351            let new_acc ≝ rotate_left … 1 old_acc in
    331352              set_8051_sfr ? s SFR_ACC_A new_acc
    332353        | RR _ ⇒ (* DPM: always ACC_A *)
     354            let s ≝ add_ticks1 s in
    333355            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    334356            let new_acc ≝ rotate_right … 1 old_acc in
    335357              set_8051_sfr ? s SFR_ACC_A new_acc
    336358        | RLC _ ⇒ (* DPM: always ACC_A *)
     359            let s ≝ add_ticks1 s in
    337360            let old_cy_flag ≝ get_cy_flag ? s in
    338361            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    … …  
    342365              set_8051_sfr ? s SFR_ACC_A new_acc
    343366        | RRC _ ⇒ (* DPM: always ACC_A *)
     367            let s ≝ add_ticks1 s in
    344368            let old_cy_flag ≝ get_cy_flag ? s in
    345369            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    … …  
    349373              set_8051_sfr ? s SFR_ACC_A new_acc
    350374        | SWAP _ ⇒ (* DPM: always ACC_A *)
     375            let s ≝ add_ticks1 s in
    351376            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    352377            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
    … …  
    354379              set_8051_sfr ? s SFR_ACC_A new_acc
    355380        | PUSH addr ⇒
     381            let s ≝ add_ticks1 s in
    356382            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    357383              [ DIRECT d ⇒ λdirect: True.
    … …  
    362388              ] (subaddressing_modein … addr)
    363389        | POP addr ⇒
     390            let s ≝ add_ticks1 s in
    364391            let contents ≝ read_at_stack_pointer ? s in
    365392            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    … …  
    367394              set_arg_8 ? s addr contents
    368395        | XCH addr1 addr2 ⇒
     396            let s ≝ add_ticks1 s in
    369397            let old_addr ≝ get_arg_8 ? s false addr2 in
    370398            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    … …  
    372400              set_arg_8 ? s addr2 old_acc
    373401        | XCHD addr1 addr2 ⇒
     402            let s ≝ add_ticks1 s in
    374403            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    375404            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
    … …  
    379408              set_arg_8 ? s addr2 new_arg
    380409        | RET ⇒
     410            let s ≝ add_ticks1 s in
    381411            let high_bits ≝ read_at_stack_pointer ? s in
    382412            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    … …  
    388418              set_program_counter ? s new_pc
    389419        | RETI ⇒
     420            let s ≝ add_ticks1 s in
    390421            let high_bits ≝ read_at_stack_pointer ? s in
    391422            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    … …  
    397428              set_program_counter ? s new_pc
    398429        | MOVX addr ⇒
     430          let s ≝ add_ticks1 s in
    399431          (* DPM: only copies --- doesn't affect I/O *)
    400432          match addr with
    … …  
    407439            ]
    408440        | MOV addr ⇒
     441          let s ≝ add_ticks1 s in
    409442          match addr with
    410443            [ inl l ⇒
    … …  
    441474          | JC addr ⇒
    442475                  if get_cy_flag ? s then
    443                       set_program_counter ? s (addr_of addr s)
     476                   let s ≝ add_ticks1 s in
     477                    set_program_counter ? s (addr_of addr s)
    444478                  else
     479                   let s ≝ add_ticks2 s in
    445480                    s
    446481            | JNC addr ⇒
    447482                  if ¬(get_cy_flag ? s) then
    448                       set_program_counter ? s (addr_of addr s)
     483                   let s ≝ add_ticks1 s in
     484                    set_program_counter ? s (addr_of addr s)
    449485                  else
     486                   let s ≝ add_ticks2 s in
    450487                    s
    451488            | JB addr1 addr2 ⇒
    452489                  if get_arg_1 ? s addr1 false then
    453                       set_program_counter ? s (addr_of addr2 s)
     490                   let s ≝ add_ticks1 s in
     491                    set_program_counter ? s (addr_of addr2 s)
    454492                  else
     493                   let s ≝ add_ticks2 s in
    455494                    s
    456495            | JNB addr1 addr2 ⇒
    457496                  if ¬(get_arg_1 ? s addr1 false) then
    458                       set_program_counter ? s (addr_of addr2 s)
     497                   let s ≝ add_ticks1 s in
     498                    set_program_counter ? s (addr_of addr2 s)
    459499                  else
     500                   let s ≝ add_ticks2 s in
    460501                    s
    461502            | JBC addr1 addr2 ⇒
    462503                  let s ≝ set_arg_1 ? s addr1 false in
    463504                    if get_arg_1 ? s addr1 false then
    464                         set_program_counter ? s (addr_of addr2 s)
     505                     let s ≝ add_ticks1 s in
     506                      set_program_counter ? s (addr_of addr2 s)
    465507                    else
     508                     let s ≝ add_ticks2 s in
    466509                      s
    467510            | JZ addr ⇒
    468511                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
    469                         set_program_counter ? s (addr_of addr s)
     512                     let s ≝ add_ticks1 s in
     513                      set_program_counter ? s (addr_of addr s)
    470514                    else
     515                     let s ≝ add_ticks2 s in
    471516                      s
    472517            | JNZ addr ⇒
    473518                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
    474                         set_program_counter ? s (addr_of addr s)
     519                     let s ≝ add_ticks1 s in
     520                      set_program_counter ? s (addr_of addr s)
    475521                    else
     522                     let s ≝ add_ticks2 s in
    476523                      s
    477524            | CJNE addr1 addr2 ⇒
    … …  
    482529                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    483530                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     531                            let s ≝ add_ticks1 s in
    484532                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    485533                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    486534                          else
     535                            let s ≝ add_ticks2 s in
    487536                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    488537                    | inr r' ⇒
    … …  
    491540                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    492541                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     542                            let s ≝ add_ticks1 s in
    493543                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    494544                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    495545                          else
     546                            let s ≝ add_ticks2 s in
    496547                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    497548                    ]
    … …  
    500551              let s ≝ set_arg_8 ? s addr1 result in
    501552                if ¬(eq_bv ? result (zero 8)) then
    502                     set_program_counter ? s (addr_of addr2 s)
     553                 let s ≝ add_ticks1 s in
     554                  set_program_counter ? s (addr_of addr2 s)
    503555                else
     556                 let s ≝ add_ticks2 s in
    504557                  s
    505         | NOP ⇒ s
     558        | NOP ⇒
     559           let s ≝ add_ticks2 s in
     560            s
    506561        ].
    507562    try assumption
    … …  
    517572    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    518573    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    519     let s ≝ set_clock ? s (clock ? s + ticks) in
    520574    let s ≝ set_program_counter ? s pc in
    521575    let s ≝
    522576      match instr with
    523       [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?
     577      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
    524578        (λx. λs.
    525579        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
    … …  
    528582        ] (subaddressing_modein … x)) instr s
    529583      | ACALL addr ⇒
     584          let s ≝ set_clock ? s (ticks + clock ? s) in
    530585          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    531586            [ ADDR11 a ⇒ λaddr11: True.
    … …  
    544599            ] (subaddressing_modein … addr)
    545600        | LCALL addr ⇒
     601          let s ≝ set_clock ? s (ticks + clock ? s) in
    546602          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    547603            [ ADDR16 a ⇒ λaddr16: True.
    … …  
    557613            ] (subaddressing_modein … addr)
    558614        | MOVC addr1 addr2 ⇒
     615          let s ≝ set_clock ? s (ticks + clock ? s) in
    559616          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
    560617            [ ACC_DPTR ⇒ λacc_dptr: True.
    … …  
    576633            ] (subaddressing_modein … addr2)
    577634        | JMP _ ⇒ (* DPM: always indirect_dptr *)
     635          let s ≝ set_clock ? s (ticks + clock ? s) in
    578636          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    579637          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    … …  
    582640            set_program_counter ? s new_pc
    583641        | LJMP addr ⇒
     642          let s ≝ set_clock ? s (ticks + clock ? s) in
    584643          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    585644            [ ADDR16 a ⇒ λaddr16: True.
    … …  
    588647            ] (subaddressing_modein … addr)
    589648        | SJMP addr ⇒
     649          let s ≝ set_clock ? s (ticks + clock ? s) in
    590650          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    591651            [ RELATIVE r ⇒ λrelative: True.
    … …  
    595655            ] (subaddressing_modein … addr)
    596656        | AJMP addr ⇒
     657          let s ≝ set_clock ? s (ticks + clock ? s) in
    597658          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    598659            [ ADDR11 a ⇒ λaddr11: True.
    … …  
    666727    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
    667728
    668 definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
     729definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
    669730  λticks_of.
    670731  λs.
    671732  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    672733  let ticks ≝ ticks_of (program_counter ? s) in
    673   let s ≝ set_clock ? s (clock ? s + ticks) in
    674734  let s ≝ set_program_counter ? s pc in
    675735  let s ≝
    676736    match instr with
    677     [ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    678     | Comment cmt ⇒ s
     737    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
     738    | Comment cmt ⇒
     739       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
     740        s
    679741    | Cost cst ⇒ s
    680     | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
     742    | Jmp jmp ⇒
     743       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
     744        set_program_counter ? s (address_of_word_labels s jmp)
    681745    | Call call ⇒
     746      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    682747      let a ≝ address_of_word_labels s call in
    683748      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    … …  
    690755        set_program_counter ? s a
    691756    | Mov dptr ident ⇒
     757      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    692758      let preamble ≝ \fst (code_memory ? s) in
    693759      let data_labels ≝ construct_datalabels preamble in
    … …  
    706772    ].
    707773
    708 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat) (s: PseudoStatus) on n: PseudoStatus ≝
     774let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
    709775  match n with
    710776    [ O ⇒ s
Note: See TracChangeset for help on using the changeset viewer.