Changeset 2024 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 7, 2012, 3:20:53 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2021 r2024 1517 1517 ∀sigma: Word → Word. 1518 1518 ∀policy: Word → bool. 1519 let lookup_labels ≝ λx:Identifier. sigma (address_of_word_labels_code_mem (\snd program) x)in1519 let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd program) x in 1520 1520 ∀ppc. 1521 1521 ∀code_memory. 1522 let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst program)) x (zero 16) in1522 let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst program)) x (zero 16) in 1523 1523 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 1524 1524 let pc ≝ sigma ppc in … … 1610 1610 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 1611 1611 let code_memory ≝ load_code_memory assembled in 1612 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x)in1612 let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 1613 1613 ∀ppc. 1614 1614 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in … … 1672 1672 let code_memory ≝ load_code_memory assembled in 1673 1673 let data_labels ≝ construct_datalabels (\fst program) in 1674 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x)in1674 let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 1675 1675 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 1676 1676 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in … … 2347 2347 2348 2348 (*CSC: ???*) 2349 (* XXX: we need a precondition here stating that the PPC is within the 2350 bounds of the instruction list in order for Jaap's specification to 2351 apply. 2352 *) 2349 2353 lemma snd_assembly_1_pseudoinstruction_ok: 2350 2354 ∀program: pseudo_assembly_program. … … 2353 2357 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 2354 2358 ∀ppc: Word. 2359 ∀ppc_in_bounds: nat_of_bitvector 16 ppc ≤ \snd program. 2355 2360 ∀pi. 2356 2361 ∀lookup_labels. 2357 2362 ∀lookup_datalabels. 2358 lookup_labels = (λx. sigma(address_of_word_labels_code_mem (\snd program) x)) →2363 lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) → 2359 2364 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 2360 2365 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 2361 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels 2366 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 2362 2367 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2363 #program #sigma #policy #sigma_policy_specification_witness #ppc #p i2368 #program #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi 2364 2369 #lookup_labels #lookup_datalabels 2365 2370 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl … … 2385 2390 <sigma_newppc_refl 2386 2391 generalize in match fetch_pseudo_refl'; 2392 (* XXX: use ppc_in_bounds to get rid of the cases not_implemented in 2393 fetch_pseudo_instruction, as this is exactly what we need now! 2394 *) 2387 2395 whd in match (fetch_pseudo_instruction ??); 2388 2396 @pair_elim #lbl #instr #nth_refl normalize nodelta 2389 #G cases (pair_destruct_right ?????? G) % 2397 #G cases (pair_destruct_right ?????? G) 2398 lapply (sigma_policy_specification_witness ppc) 2399 >program_refl normalize nodelta #policy_hyp 2400 cases policy_hyp policy_hyp #policy_hyp1 #_ 2401 >policy_hyp1 2402 [1: 2403 policy_hyp1 whd in match instruction_size; normalize nodelta 2404 <pi_refl' >(?: pi' = \fst (fetch_pseudo_instruction (\snd program) ppc)) 2405 [1: >program_refl % ] >fetch_pseudo_refl' % 2406 2: 2407 >program_refl in ppc_in_bounds; #relevant assumption 2408 ] 2390 2409 qed. 2391 2410
Note: See TracChangeset
for help on using the changeset viewer.