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

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

File:
1 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:
Note: See TracChangeset for help on using the changeset viewer.