Changeset 1036
 Timestamp:
 Jun 22, 2011, 11:38:55 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1035 r1036 1284 1284 axiom fetch_assembly_pseudo2: 1285 1285 ∀program,pol,ppc. 1286 let 〈labels,costs〉 ≝ build_maps program pol in 1286 (* let 〈labels,costs〉 ≝ build_maps program pol in *) 1287 1287 let assembled ≝ \fst (assembly program pol) in 1288 1288 let code_memory ≝ load_code_memory assembled in … … 2014 2014 generalize in match EQ EQ; 2015 2015 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 ⊢ (∀_.??%? → ?) 2017 2017 * #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 2018 2032 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 2047 n H2; whd in ⊢ (% → ?) 2048 #H2*) >(eq_bv_eq … H2) >EQ % 2020 2049 2021 2050 lemma main_thm0:
Note: See TracChangeset
for help on using the changeset viewer.