Changeset 2057
 Timestamp:
 Jun 13, 2012, 1:30:57 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2032 r2057 1449 1449 ∀policy: Word → bool. 1450 1450 let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd program) x in 1451 ∀ppc. 1451 ∀ppc.∀ppc_ok. 1452 1452 ∀code_memory. 1453 1453 let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst program)) x (zero 16) in 1454 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ) in1454 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in 1455 1455 let pc ≝ sigma ppc in 1456 1456 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in … … 1459 1459 encoding_check code_memory pc pc_plus_len assembled → 1460 1460 fetch_many code_memory pc_plus_len pc instructions. 1461 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc # code_memory1461 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory 1462 1462 letin lookup_datalabels ≝ (λx.?) 1463 1463 letin pi ≝ (fst ???) … … 1483 1483 λsigma: Word → Word. 1484 1484 λpolicy: Word → bool. 1485 ∀ppc: Word. 1486 let 〈preamble, instr_list〉 ≝program in1485 ∀ppc: Word. ∀ppc_ok. 1486 let instr_list ≝ \snd program in 1487 1487 let pc ≝ sigma ppc in 1488 1488 let labels ≝ \fst (create_label_cost_map instr_list) in 1489 1489 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 1490 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ) in1490 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 1491 1491 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in 1492 1492 And (nat_of_bitvector … ppc ≤ instr_list → … … 1542 1542 let code_memory ≝ load_code_memory assembled in 1543 1543 let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 1544 ∀ppc. 1545 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in1544 ∀ppc.∀ppc_ok. 1545 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in 1546 1546 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 1547 1547 let pc ≝ sigma ppc in … … 1554 1554 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 1555 1555 #assembly_ok #Pair_eq destruct(Pair_eq) whd 1556 #ppc @pair_elim #pi #newppc #eq_fetch_pseudo_instruction1556 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 1557 1557 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd 1558 1558 lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] assembly_ok … … 1598 1598 ∀policy. 1599 1599 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 1600 ∀ppc. 1600 ∀ppc.∀ppc_ok. 1601 1601 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1602 1602 let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in … … 1605 1605 let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 1606 1606 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 1607 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in1607 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in 1608 1608 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 1609 1609 fetch_many code_memory (sigma newppc) (sigma ppc) instructions. 1610 * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc 1610 * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok 1611 1611 @pair_elim #labels #costs #create_label_map_refl 1612 1612 @pair_elim #assembled #costs' #assembled_refl … … 1624 1624 #len #assembledi #EQ4 #H 1625 1625 lapply (H ppc) >fetch_pseudo_refl #H 1626 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled))1627 >EQ4 #H1 cases H1626 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled)) 1627 >EQ4 #H1 cases (H ppc_ok) 1628 1628 #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 1629 1629 >fetch_pseudo_refl in H1; #assm @assm assumption … … 1773 1773 λM:internal_pseudo_address_map. 1774 1774 λcm. 1775 λs:PseudoStatus cm. 1775 λs:PseudoStatus cm. λppc_ok. 1776 1776 next_internal_pseudo_address_map0 ? 1777 (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) )) M cm s.1777 (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M cm s. 1778 1778 1779 1779 definition code_memory_of_pseudo_assembly_program: … … 2085 2085 definition ticks_of: 2086 2086 ∀p:pseudo_assembly_program. 2087 (Word → Word) → (Word → bool) → Word → nat × nat ≝ 2087 (Word → Word) → (Word → bool) → ∀ppc:Word. 2088 nat_of_bitvector … ppc < \snd p → nat × nat ≝ 2088 2089 λprogram: pseudo_assembly_program. 2089 2090 λsigma. 2090 2091 λpolicy. 2091 λppc: Word. 2092 let 〈preamble, pseudo〉 ≝program in2093 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in2092 λppc: Word. λppc_ok. 2093 let pseudo ≝ \snd program in 2094 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in 2094 2095 ticks_of0 program sigma policy ppc fetched. 2095 2096 … … 2288 2289 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 2289 2290 ∀ppc: Word. 2290 ∀ppc_in_bounds: nat_of_bitvector 16 ppc ≤\snd program.2291 ∀ppc_in_bounds: nat_of_bitvector 16 ppc < \snd program. 2291 2292 ∀pi. 2292 2293 ∀lookup_labels. … … 2294 2295 lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) → 2295 2296 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 2296 \fst (fetch_pseudo_instruction (\snd program) ppc ) = pi →2297 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi → 2297 2298 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 2298 2299 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). … … 2309 2310 @pair_elim #labels #costs' #create_label_cost_map_refl 2310 2311 <eq_pair_fst_snd #H lapply (H (refl …)) H #H 2311 lapply (H ppc ) H2312 lapply (H ppc ppc_in_bounds) H 2312 2313 @pair_elim #pi' #newppc #fetch_pseudo_refl' 2313 2314 @pair_elim #len #assembled #assembly1_refl #H … … 2321 2322 <sigma_newppc_refl 2322 2323 generalize in match fetch_pseudo_refl'; 2323 (* XXX: use ppc_in_bounds to get rid of the cases not_implemented in 2324 fetch_pseudo_instruction, as this is exactly what we need now! 2325 *) 2326 whd in match (fetch_pseudo_instruction ??); 2324 whd in match (fetch_pseudo_instruction ???); 2327 2325 @pair_elim #lbl #instr #nth_refl normalize nodelta 2328 #G cases (pair_destruct_right ?????? G) 2329 lapply (sigma_policy_specification_witness ppc) 2330 >program_refl normalize nodelta #policy_hyp 2331 cases policy_hyp policy_hyp #policy_hyp1 #_ 2332 >policy_hyp1 2333 [1: 2334 policy_hyp1 whd in match instruction_size; normalize nodelta 2335 <pi_refl' >(?: pi' = \fst (fetch_pseudo_instruction (\snd program) ppc)) 2336 [1: >program_refl % ] >fetch_pseudo_refl' % 2337 2: 2338 >program_refl in ppc_in_bounds; #relevant assumption 2339 ] 2326 #G cases (pair_destruct_right ?????? G) % 2340 2327 qed. 2341 2328
Note: See TracChangeset
for help on using the changeset viewer.