Changeset 1042


Ignore:
Timestamp:
Jun 25, 2011, 2:30:07 AM (8 years ago)
Author:
sacerdot
Message:

Dead code removed.
Slow code uncommented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1041 r1042  
    12681268       sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    12691269
    1270 axiom assembly_ok_to_expand_pseudo_instruction_ok:
    1271  ∀program,pol,assembled,costs.
    1272   〈assembled,costs〉 = assembly program pol →
    1273    ∀ppc.
    1274     let code_memory ≝ load_code_memory assembled in
    1275     let preamble ≝ \fst program in   
    1276     let data_labels ≝ construct_datalabels preamble in
    1277     let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    1278     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    1279     let expansion ≝ pol ppc in
    1280     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1281      ∃instructions.
    1282       Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
    1283 
    12841270lemma fetch_assembly_pseudo2:
    12851271 ∀program,pol,ppc.
     
    19941980         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
    19951981         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
    1996 
    1997 
    1998 
    1999 lemma main_thm0:
    2000  ∀M,M',ps,ps',pol.
    2001   next_internal_pseudo_address_map M ps = Some … M' →
    2002   ∀H:ps' = execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
    2003    ∃n.
    2004       execute n (status_of_pseudo_status M ps pol)
    2005     = status_of_pseudo_status M' ps' ?.
    2006  [2: >H >execute_1_pseudo_instruction_preserves_code_memory @pol]
    2007  #M #M' #ps #ps' #pol
    2008  change with (next_internal_pseudo_address_map0 ???? = ? → ?)
    2009  generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps))
    2010  @pair_elim' #labels #costs #EQ1 normalize nodelta
    2011  whd in match execute_1_pseudo_instruction
    2012  @pair_elim' #pi #newppc #EQ2 normalize nodelta
    2013  cases pi in EQ2; normalize nodelta
    2014   [2: #ARG #MAP #H1 #H2 #EQ >MAP in EQ;
    2015  
    2016  
    2017  cases (execute_1_pseudo_instruction_preserves_code_memory ??) XX
    2018  cases (assembly ??) #assembled #costs normalize nodelta
    2019  cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta;
    2020  cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol
    2021  #MAP
    2022  cases (fetch_pseudo_instruction (\snd code_mem) ppc)
    2023 
    2024  change with
    2025   (? → ∃n.
    2026     execute n
    2027      (set_low_internal_ram ?
    2028        (set_high_internal_ram ?
    2029          (set_program_counter ?
    2030            (set_code_memory ?? ps (load_code_memory ?))
    2031           (sigma ? pol (program_counter ? ps)))
    2032         (high_internal_ram_of_pseudo_high_internal_ram M ?))
    2033       (low_internal_ram_of_pseudo_low_internal_ram M ?))
    2034    = set_low_internal_ram ?
    2035       (set_high_internal_ram ?
    2036         (set_program_counter ?
    2037           (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory ?))
    2038          (sigma ???))
    2039        ?)
    2040      ?)
    2041  change with (next_internal_pseudo_address_map0 ???? = ? → ?)
    2042  generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps))
    2043  @pair_elim' #labels #costs #EQ1 normalize nodelta
    2044  @pair_elim' #pi #newppc #EQ2
    2045  >execute_1_pseudo_instruction_preserves_code_memory
    2046  cases (assembly ??) #assembled #costs normalize nodelta
    2047  cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta;
    2048  cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol
    2049  #MAP
    2050  cases (fetch_pseudo_instruction (\snd code_mem) ppc)
    2051  
    2052  
    2053  (code_memory pseudo_assembly_program ps)
    2054  #MAP
    2055 
    2056  
    2057  
    2058  whd in ⊢ (? → ? → ??%? → ??%? → ?)
    2059  generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
    2060  cases (build_maps (code_memory … ps) pol)
    2061  #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
    2062  generalize in match pol; -pol;
    2063  @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%]
    2064  #EQ0 #pol normalize nodelta;
    2065  generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    2066   [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
    2067  * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
    2068  #H generalize in match (H ? (refl …)) -H; #H;
    2069  #MAP
    2070  #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
    2071  #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
    2072  change with
    2073   (∃n.
    2074     execute n
    2075      (set_low_internal_ram ?
    2076        (set_high_internal_ram ?
    2077          (set_program_counter ?
    2078            (set_code_memory ?? ps (load_code_memory assembled))
    2079           (sigma 〈preamble,instr_list〉 pol (program_counter ? ps)))
    2080         (high_internal_ram_of_pseudo_high_internal_ram M ?))
    2081       (low_internal_ram_of_pseudo_low_internal_ram M ?))
    2082    = set_low_internal_ram ?
    2083       (set_high_internal_ram ?
    2084         (set_program_counter ?
    2085           (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
    2086          (sigma ???))
    2087        ?)
    2088      ?)
    2089  whd in match (\snd 〈preamble,instr_list〉) in H;
    2090  whd in match (\fst 〈preamble,instr_list〉) in H;
    2091  whd in match (\snd 〈final_pc,assembled〉) in H;
    2092  whd in match (\snd 〈preamble,instr_list〉) in MAP;
    2093  -s s'' labels costs final_ppc final_pc;
    2094  letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps)
    2095  (* NICE STATEMENT HERE *)
    2096  generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
    2097  #K <K generalize in match K; -K;
    2098  (* STATEMENT WITH EQUALITY HERE *)
    2099  whd in ⊢ (???(?%?) → ?)
    2100  whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
    2101  cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ %
    2102  #pi #newppc normalize nodelta; #MAP * #instructions *;
    2103  cases pi in MAP; normalize nodelta;
    2104   [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0]
    2105     generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
    2106     normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    2107     #H2 >(eq_bv_eq … H2) >EQ %
    2108 (*  |6: (* Mov *) #arg1 #arg2
     1982  |6: (* Mov *) #arg1 #arg2
    21091983       #H1 #H2 #EQ %[@1]
    21101984       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     
    21191993       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    21201994       #result #flags
    2121        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)
    2122 (*  |5: (* Call *) #label #MAP
     1995       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
     1996  |5: (* Call *) #label #MAP
    21231997      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
    21241998      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
     
    23082182            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    23092183              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    2310 *)  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
     2184  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    23112185    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
    23122186       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     
    23182192       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
    23192193       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
    2320        normalize nodelta; #MAP; (*
     2194       normalize nodelta; #MAP;
    23212195       [1: change in ⊢ (? → %) with
    23222196        ((let 〈result,flags〉 ≝
     
    23302204        change in ⊢ (???% → ?) with
    23312205         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
    2332         >get_arg_8_set_clock *)
     2206        >get_arg_8_set_clock
    23332207       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
    23342208         [2,4: #abs @⊥ normalize in abs; destruct (abs)
     
    23492223       #result #flags
    23502224       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    2351     (*| (* INC *) #arg1 #H1 #H2 #EQ %[@1]
     2225    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
    23522226       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    23532227       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     
    23812255            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
    23822256            |
    2383             ] *)
    2384 
    2385 lemma main_thm:
    2386  ∀M,M',ps,pol.
    2387   next_internal_pseudo_address_map M ps = Some … M' →
    2388    ∃n.
    2389       execute n (status_of_pseudo_status M ps pol)
    2390     = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
    2391  [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
     2257            ]
     2258cases daemon (* EASY CASES TO BE COMPLETED *)
     2259qed.
Note: See TracChangeset for help on using the changeset viewer.