Changeset 1036


Ignore:
Timestamp:
Jun 22, 2011, 11:38:55 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1035 r1036  
    12841284axiom fetch_assembly_pseudo2:
    12851285 ∀program,pol,ppc.
    1286   let 〈labels,costs〉 ≝ build_maps program pol in
     1286(*  let 〈labels,costs〉 ≝ build_maps program pol in *)
    12871287  let assembled ≝ \fst (assembly program pol) in
    12881288  let code_memory ≝ load_code_memory assembled in
     
    20142014 generalize in match EQ -EQ;
    20152015 generalize in match (refl … (code_memory pseudo_assembly_program ps))
    2016  generalize in match pol generalize in ⊢ (∀_.??%? → ?)
     2016 generalize in match pol -pol; generalize in ⊢ (∀_.??%? → ?)
    20172017 * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
     2018 (* Dependent types madness ends here *)
     2019 letin ppc ≝ (program_counter … ps)
     2020 generalize in match (fetch_assembly_pseudo2 ? pol ppc)
     2021 letin assembled ≝ (\fst (assembly ? pol))
     2022 letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
     2023 letin lookup_datalabels ≝ (λx. lookup … x (construct_datalabels preamble) (zero 16))
     2024 @pair_elim' #pi #newppc #EQ2
     2025 letin instructions ≝
     2026  (expand_pseudo_instruction ? pol ppc lookup_labels lookup_datalabels
     2027    (sigma ? pol ppc) (refl …) (refl …) (refl …))
     2028 change with (fetch_many ???? → ?) #H1
     2029 change in EQ2 with (fetch_pseudo_instruction instr_list ppc = ?)
     2030 change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
     2031 >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE
    20182032 
    2019 
     2033 XX
     2034 
     2035 whd in match execute_1_pseudo_instruction
     2036 
     2037 whd in match expand_pseudo_instruction  normalize nodelta;
     2038 whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0
     2039 normalize in match (\snd 〈preamble,instr_list〉);
     2040 cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ %
     2041 #pi #newppc normalize nodelta; #MAP
     2042 cases pi in MAP; normalize nodelta;
     2043  [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0]
     2044    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
     2045    (*
     2046    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i
     2047n H2; whd in ⊢ (% → ?)
     2048    #H2*) >(eq_bv_eq … H2) >EQ %
    20202049
    20212050lemma main_thm0:
Note: See TracChangeset for help on using the changeset viewer.