Ignore:
Timestamp:
Jun 10, 2011, 2:19:09 AM (9 years ago)
Author:
sacerdot
Message:

Comment, Cost, ADD, ADC cases done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r929 r930  
    18141814qed.
    18151815
     1816axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
     1817
     1818lemma get_register_set_program_counter:
     1819 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
     1820 #T #s #pc %
     1821qed.
     1822
     1823lemma get_8051_sfr_set_program_counter:
     1824 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
     1825 #T #s #pc %
     1826qed.
     1827
     1828lemma get_bit_addressable_sfr_set_program_counter:
     1829 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
     1830 #T #s #pc %
     1831qed.
     1832
     1833lemma low_internal_ram_set_program_counter:
     1834 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
     1835 #T #s #pc %
     1836qed.
     1837
     1838lemma get_arg_8_set_program_counter:
     1839 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
     1840  ∀T,s,pc,b.∀arg:l.
     1841   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
     1842 [2,3: cases arg; *; normalize //]
     1843 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
     1844qed.
     1845
     1846lemma get_arg_8_set_code_memory:
     1847 ∀T1,T2,s,code_mem,b,arg.
     1848   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
     1849 #T1 #T2 #s #code_mem #b #arg %
     1850qed.
     1851
     1852lemma set_code_memory_set_flags:
     1853 ∀T1,T2,s,f1,f2,f3,code_mem.
     1854  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
     1855   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
     1856 #T1 #T2 #s #f1 #f2 #f3 #code_mem whd in ⊢ (??(???%?)%)
     1857 cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
     1858qed.
     1859
     1860lemma set_program_counter_set_flags:
     1861 ∀T1,s,f1,f2,f3,pc.
     1862  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
     1863   set_flags … (set_program_counter … s pc) f1 f2 f3.
     1864 #T1 #s #f1 #f2 #f3 #pc whd in ⊢ (??(??%?)%)
     1865 cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
     1866qed.
     1867
     1868lemma program_counter_set_flags:
     1869 ∀T1,s,f1,f2,f3.
     1870  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
     1871 #T1 #s #f1 #f2 #f3 whd in ⊢ (??(??%)?) cases (split ????) #nu #nl %
     1872qed.
     1873
     1874axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps.
     1875
    18161876lemma main_thm:
    18171877 ∀ticks_of.
     
    18301890    #abs @⊥ normalize in abs; destruct (abs) ]
    18311891 * #labels #costs generalize in match (refl … (code_memory … ps))
    1832  cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ normalize nodelta;
     1892 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
    18331893 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    18341894  [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ]
     
    18501910 #K <K generalize in match K; -K;
    18511911 (* STATEMENT WITH EQUALITY HERE *)
    1852  whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta;
     1912 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ0 normalize nodelta;
    18531913 cases (fetch_pseudo_instruction instr_list (program_counter … ps))
    18541914 #pi #newppc normalize nodelta; * #instructions *;
    18551915 cases pi normalize nodelta;
    1856   [ (* Instruction *)
    1857   | (* Comment *) #comment #H1 #H2 #EQ %[@0] >EQ
    1858     whd in ⊢ (???(???(??%)))
    1859     normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1
    1860     >K1 in H2; whd in ⊢ (% → ?) #H2 <(eq_bv_to_eq … H2)
    1861    
    1862   | (* Cost *)
    1863   | (* Jmp *)
    1864   | (* Call *)
    1865   | (* Mov *)
    1866   ]
    1867 qed.
     1916  [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0]
     1917    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     1918    #H2 >(eq_bv_to_eq … H2) >ignore_clock in EQ; #EQ >EQ %
     1919  |4: (* Jmp *)
     1920  |5: (* Call *)
     1921  |6: (* Mov *)
     1922  | (* Instruction *) -pi; *
     1923    [1,2: (* ADD, ADDC *) #arg1 #arg2 #H1 #H2 #EQ %[1,3:@1]
     1924       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     1925       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     1926       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     1927       * #H2a whd in ⊢ (% → ?) #H2b
     1928       >ignore_clock in EQ;
     1929       >(eq_instruction_to_eq … H2a)
     1930       whd in ⊢ (???% → ??%?);
     1931       >ignore_clock
     1932       >get_arg_8_set_program_counter [2,4:%]
     1933       >get_arg_8_set_program_counter [2,4:%]
     1934       >get_arg_8_set_program_counter [2,4:%]
     1935       >get_arg_8_set_program_counter [2,4:%]
     1936       >get_arg_8_set_code_memory
     1937       >get_arg_8_set_program_counter [2,4:%]
     1938       >get_arg_8_set_program_counter [2,4:%]
     1939       >get_arg_8_set_code_memory
     1940       cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags
     1941       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
     1942       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
     1943    |
Note: See TracChangeset for help on using the changeset viewer.