Changeset 2078
 Timestamp:
 Jun 14, 2012, 11:44:46 AM (6 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2073 r2078 768 768 #lbl #instr normalize nodelta >add_associative % 769 769 qed. 770 771 definition sigma_policy_specification ≝ 772 λprogram: pseudo_assembly_program. 773 λsigma: Word → Word. 774 λpolicy: Word → bool. 775 ∀ppc: Word. ∀ppc_ok. 776 let instr_list ≝ \snd program in 777 let pc ≝ sigma ppc in 778 let labels ≝ \fst (create_label_cost_map instr_list) in 779 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 780 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 781 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in 782 sigma (zero …) = zero … 783 ∧ 784 (nat_of_bitvector … ppc ≤ instr_list → 785 next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))) 786 ∧ 787 ( (nat_of_bitvector … ppc < instr_list → nat_of_bitvector … pc < nat_of_bitvector … next_pc) 788 ∨ (nat_of_bitvector … ppc = instr_list → next_pc = (zero …))). 770 789 771 790 definition assembly: 
src/ASM/AssemblyProof.ma
r2075 r2078 1479 1479 ]. 1480 1480 1481 definition sigma_policy_specification ≝1482 λprogram: pseudo_assembly_program.1483 λsigma: Word → Word.1484 λpolicy: Word → bool.1485 ∀ppc: Word. ∀ppc_ok.1486 let instr_list ≝ \snd program in1487 let pc ≝ sigma ppc in1488 let labels ≝ \fst (create_label_cost_map instr_list) in1489 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in1490 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in1491 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in1492 And (nat_of_bitvector … ppc ≤ instr_list →1493 next_pc = add 16 pc (bitvector_of_nat …1494 (instruction_size lookup_labels sigma policy ppc instruction)))1495 (Or (nat_of_bitvector … ppc < instr_list →1496 nat_of_bitvector … pc < nat_of_bitvector … next_pc)1497 (nat_of_bitvector … ppc = instr_list → next_pc = (zero …))).1498 1499 1481 (* This is a trivial consequence of fetch_assembly_pseudo + the proof that the 1500 1482 function that load the code in memory is correct. The latter is based 
src/ASM/Policy.ma
r2059 r2078 628 628 629 629 (* The glue between Policy and Assembly. *) 630 (*CSC: modified to really use the specification in Assembly.ma. 631 I have modified all that follows in vi without testing it in Matita. 632 Jaap, please repair it *) 630 633 definition jump_expansion': 631 634 ∀program:preamble × (Σl:list labelled_instruction.S (l) < 2^16). 632 option (Σsigma:Word → Word × bool. 633 ∀ppc: Word. ∀ppc_ok. 634 let pc ≝ \fst (sigma ppc) in 635 let labels ≝ \fst (create_label_cost_map (\snd program)) in 636 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in 637 let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in 638 let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 639 And (nat_of_bitvector … ppc ≤ \snd program → 640 next_pc = add ? pc (bitvector_of_nat … 641 (instruction_size lookup_labels (λx.\fst (sigma x)) (λx.\snd (sigma x)) ppc instruction))) 642 (Or (nat_of_bitvector … ppc < \snd program → 643 nat_of_bitvector … pc < nat_of_bitvector … next_pc) 644 (nat_of_bitvector … ppc = \snd program → next_pc = (zero …)))) ≝ 635 option (Σsigma_policy:(Word → Word) × (Word → bool). 636 let 〈sigma,policy〉≝ sigma_policy in 637 sigma_policy_specification program sigma policy 638 ≝ 645 639 λprogram. 646 640 let policy ≝ pi1 … (je_fixpoint (\snd program)) in … … 648 642 [ None ⇒ None ? 649 643  Some x ⇒ Some ? 650 «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 651 〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?» 644 «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 645 bitvector_of_nat 16 pc), 646 (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 647 jmpeqb jl long_jump)〉,?» 652 648 ]. 653 649 #ppc normalize nodelta cases daemon
Note: See TracChangeset
for help on using the changeset viewer.