Changeset 2131 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 28, 2012, 12:55:05 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2129 r2131 146 146 ∀sigma: Word → Word. 147 147 ∀policy: Word → bool. 148 let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd program) x in 148 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 149 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 149 150 ∀ppc.∀ppc_ok. 150 151 ∀code_memory. … … 157 158 encoding_check code_memory pc pc_plus_len assembled → 158 159 fetch_many code_memory pc_plus_len pc instructions. 159 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory 160 #program #sigma #policy 161 @pair_elim #labels #costs #create_label_cost_map_refl 162 letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory 160 163 letin lookup_datalabels ≝ (λx.?) 161 164 letin pi ≝ (fst ???) … … 193 196 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 194 197 let code_memory ≝ load_code_memory assembled in 195 let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in198 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 196 199 ∀ppc.∀ppc_ok. 197 200 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in … … 213 216 >eq_fetch_pseudo_instruction 214 217 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<assembledi.?) → ?) 215 > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =216 (λx.address_of_word_labels_code_mem instr_list x)))217 [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl218 #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]219 218 >eq_assembly_1_pseudoinstruction 220 219 whd in ⊢ (% → ?); #assembly_ok … … 225 224 #spw1 #_ >spw1 spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f 226 225 >eq_fetch_pseudo_instruction whd in match instruction_size; 227 normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY*)226 normalize nodelta (*CSC: TRUE, NEEDS LEMMA *) 228 227 cases daemon 229 228  lapply (load_code_memory_ok assembled' ?) [ assumption ] … … 271 270 let code_memory ≝ load_code_memory assembled in 272 271 let data_labels ≝ construct_datalabels (\fst program) in 273 let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in272 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 274 273 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 275 274 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in … … 286 285 lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs') 287 286 normalize nodelta try assumption 288 @pair_elim #labels' #costs' #create_label_map_refl'#H287 >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H 289 288 lapply (H (sym_eq … assembled_refl)) H 290 289 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi)) … … 292 291 #len #assembledi #EQ4 #H 293 292 lapply (H ppc) >fetch_pseudo_refl #H 294 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled)) 293 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy) 294 >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) X 295 295 >EQ4 #H1 cases (H ppc_ok) 296 296 #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta … … 890 890 ∀lookup_labels. 891 891 ∀lookup_datalabels. 892 lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) → 892 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 893 lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) → 893 894 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 894 895 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi → … … 897 898 #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi 898 899 #lookup_labels #lookup_datalabels 900 @pair_elim #labels #costs #create_label_cost_map_refl 899 901 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl 900 902 normalize nodelta … … 905 907 lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs) 906 908 @pair_elim #preamble #instr_list #program_refl 907 @pair_elim #labels #costs' #create_label_cost_map_refl 909 lapply create_label_cost_map_refl; create_label_cost_map_refl 910 >program_refl in ⊢ (% → ?); #create_label_cost_map_refl 911 >create_label_cost_map_refl 908 912 <eq_pair_fst_snd #H lapply (H (refl …)) H #H 909 913 lapply (H ppc ppc_in_bounds) H
Note: See TracChangeset
for help on using the changeset viewer.