Changeset 2059 for src/ASM/PolicyFront.ma
 Timestamp:
 Jun 13, 2012, 3:44:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2048 r2059 128 128 ppc_pc_map → Prop ≝ 129 129 λprogram.λop.λp. 130 ∀i.i <program →130 ∀i.i ≤ program → 131 131 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in 132 132 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in 133 133 (*opc ≤ pc ∧*) jmpleq oj j. 134 134 135 135 (* this is the instruction size as determined by the jump length given *) 136 136 definition expand_relative_jump_internal_unsafe: … … 639 639 qed. 640 640 641 definition policy_equal ≝ 641 (* NOTE: we only compare the first elements here because otherwise the 642 * added = 0 → policy_equal property of jump_expansion_step doesn't hold: 643 * if we have not added anything to the pc, we only know the PC hasn't changed, 644 * there might still have been a short/medium jump change *) 645 definition policy_pc_equal ≝ 642 646 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 643 647 (∀n:ℕ.n ≤ program → 644 bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 = 645 bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉). 648 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 649 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). 650 651 definition policy_jump_equal ≝ 652 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 653 (∀n:ℕ.n < program → 654 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 655 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). 646 656 647 657 definition nec_plus_ultra ≝
Note: See TracChangeset
for help on using the changeset viewer.