Changeset 2078 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 14, 2012, 11:44:46 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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
Note: See TracChangeset
for help on using the changeset viewer.