Ignore:
Timestamp:
Jun 16, 2011, 11:27:48 PM (10 years ago)
Author:
sacerdot
Message:

Proof restored.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r987 r988  
    15331533
    15341534axiom low_internal_ram_write_at_stack_pointer:
    1535  ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     1535 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    15361536  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
    15371537  low_internal_ram ? s2 = low_internal_ram T2 s3 →
    15381538  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
    15391539  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    1540   bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
     1540  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
    15411541   low_internal_ram T1
    15421542     (write_at_stack_pointer ?
    … …  
    15591559       
    15601560axiom high_internal_ram_write_at_stack_pointer:
    1561  ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     1561 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    15621562  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
    15631563  high_internal_ram ? s2 = high_internal_ram T2 s3 →
    15641564  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
    15651565  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    1566   bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
     1566  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
    15671567   high_internal_ram T1
    15681568     (write_at_stack_pointer ?
    … …  
    17981798
    17991799lemma main_thm:
    1800  ∀M,M',ps,s,s''.
     1800 ∀M,M',ps,s,s'',pol.
    18011801  next_internal_pseudo_address_map M ps = Some … M' →
    1802   status_of_pseudo_status M ps = Some … s →
    1803   status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
     1802  status_of_pseudo_status M ps pol = Some … s →
     1803  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = Some … s'' →
    18041804   ∃n. execute n s = s''.
    1805  #M #M' #ps #s #s''
    1806  generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
     1805 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
     1806 #M #M' #ps #s #s'' #pol
     1807 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol)
    18071808 whd in ⊢ (? → ? → ??%? → ??%? → ?)
    18081809 >execute_1_pseudo_instruction_preserves_code_memory
    1809  generalize in match (refl … (assembly (code_memory … ps)))
    1810  generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
    1811  cases (build_maps (code_memory … ps))
     1810 generalize in match (refl … (assembly (code_memory … ps) pol))
     1811 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
     1812 cases (build_maps (code_memory … ps) pol)
    18121813 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
    1813  generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
     1814 generalize in match pol; -pol;
     1815 @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%]
     1816 #EQ0 #pol normalize nodelta;
    18141817 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    18151818  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
    … …  
    18261829         (set_program_counter ?
    18271830           (set_code_memory ?? ps (load_code_memory assembled))
    1828           (sigma 〈preamble,instr_list〉 (program_counter ? ps)))
     1831          (sigma 〈preamble,instr_list〉 pol (program_counter ? ps)))
    18291832        (high_internal_ram_of_pseudo_high_internal_ram M ?))
    18301833      (low_internal_ram_of_pseudo_low_internal_ram M ?))
    … …  
    18331836        (set_program_counter ?
    18341837          (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
    1835          (sigma ??))
     1838         (sigma ???))
    18361839       ?)
    18371840     ?)
    … …  
    18411844 whd in match (\snd 〈preamble,instr_list〉) in MAP;
    18421845 -s s'' labels costs final_ppc final_pc;
    1843  letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps)
     1846 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps)
    18441847 (* NICE STATEMENT HERE *)
    18451848 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
    … …  
    18711874  |5: (* Call *) #label #MAP
    18721875      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
    1873       whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
     1876      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
    18741877       [ (* short *) #abs @⊥ destruct (abs)
    18751878       |3: (* long *) #H1 #H2 #EQ %[@1]
    18761879           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    18771880           change in ⊢ (? → ??%?) with (execute_1_0 ??)
    1878            cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     1881           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    18791882           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    18801883           >H2b >(eq_instruction_to_eq … H2a)
    … …  
    18851888           change with
    18861889            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
    1887                 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
     1890                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
    18881891           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
    1889            generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
     1892           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
    18901893           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
    18911894           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
    … …  
    18981901              >set_clock_set_low_internal_ram
    18991902              @low_internal_ram_write_at_stack_pointer
    1900                [ % | %
     1903               [ >EQ0 @pol | % | %
    19011904               | @(pair_destruct_2 … EQ1)
    19021905               | @(pair_destruct_2 … EQ2)
    … …  
    19121915              >set_clock_set_high_internal_ram
    19131916              @high_internal_ram_write_at_stack_pointer
    1914                [ % | %
     1917               [ >EQ0 @pol | % | %
    19151918               | @(pair_destruct_2 … EQ1)
    19161919               | @(pair_destruct_2 … EQ2)
    … …  
    19261929              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
    19271930              >external_ram_write_at_stack_pointer %
    1928             | change with (? = sigma ?(address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
     1931            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
    19291932              >EQ0 %
    19301933            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
    … …  
    19861989  |4: (* Jmp *) #label #MAP
    19871990      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
    1988       whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
     1991      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
    19891992       [3: (* long *) #H1 #H2 #EQ %[@1]
    19901993           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    19911994           change in ⊢ (? → ??%?) with (execute_1_0 ??)
    1992            cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     1995           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    19931996           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    19941997           >H2b >(eq_instruction_to_eq … H2a)
    … …  
    20002003            (refl ?
    20012004             (sub_16_with_carry
    2002               (sigma 〈preamble,instr_list〉 (program_counter … ps))
    2003               (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
     2005              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
     2006              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
    20042007              false))
    20052008           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
    … …  
    20092012           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    20102013           change in ⊢ (? → ??%?) with (execute_1_0 ??)
    2011            cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2014           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    20122015           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    20132016           >H2b >(eq_instruction_to_eq … H2a)
    … …  
    20152018           whd in ⊢ (???% → ?);
    20162019           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    2017            change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
    2018            generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
     2020           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
     2021           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
    20192022           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
    2020            @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
     2023           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
    20212024           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    20222025       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    20232026         generalize in match
    20242027          (refl …
    2025             (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
     2028            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
    20262029         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
    20272030         generalize in match
    20282031          (refl …
    2029             (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
     2032            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
    20302033         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
    20312034         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
    … …  
    20332036         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
    20342037         change in ⊢ (? →??%?) with (execute_1_0 ??)
    2035            cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2038           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    20362039           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    20372040           >H2b >(eq_instruction_to_eq … H2a)
    … …  
    20392042           whd in ⊢ (???% → ?);
    20402043           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
    2041            change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    2042            generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
     2044           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
     2045           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
    20432046           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
    20442047           generalize in match (refl … (split bool 4 4 pc_bu))
    … …  
    20492052           generalize in match
    20502053            (refl …
    2051              (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
     2054             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
    20522055             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
    20532056           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
    20542057           @split_eq_status try %
    2055             [ change with (? = sigma ? (address_of_word_labels ps label))
     2058            [ change with (? = sigma ?? (address_of_word_labels ps label))
    20562059              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    20572060            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
Note: See TracChangeset for help on using the changeset viewer.