Changeset 2101 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Jun 19, 2012, 4:43:50 PM (7 years ago)
Author:
boender
Message:
  • renamed medium to absolute jump
  • revised proofs of policy, some daemons removed
  • reverted earlier change in extralib, bounded quantification now again uses lt
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2059 r2101  
    1212  ∀old_policy:(Σpolicy:ppc_pc_map.
    1313    And (And (And (And (out_of_program_none program policy)
    14     (jump_not_in_policy program policy))
     14    (not_jump_default program policy))
    1515    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    1616    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
     
    2121    [ None ⇒ nec_plus_ultra program old_policy
    2222    | Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p)
    23        (jump_not_in_policy program p))
    24        (policy_increase program old_policy p))
    25        (no_ch = true → policy_compact program labels p))
     23       (not_jump_default program p))
     24       (jump_increase program old_policy p))
     25       (no_ch = true → sigma_compact program labels p))
    2626       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    2727       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
    28        (no_ch = true → policy_pc_equal program old_policy p))
    29        (policy_jump_equal program old_policy p → no_ch = true))
     28       (no_ch = true → sigma_pc_equal program old_policy p))
     29       (sigma_jump_equal program old_policy p → no_ch = true))
    3030       (\fst p < 2^16)
    3131    ])
     
    3737      let 〈added,policy〉 ≝ x in
    3838      And (And (And (And (And (And (And (And (out_of_program_none prefix policy)
    39       (jump_not_in_policy prefix policy))
    40       (policy_increase prefix old_sigma policy))
    41       (policy_compact_unsafe prefix labels policy))
    42       (policy_safe prefix labels added old_sigma policy))
     39      (not_jump_default prefix policy))
     40      (jump_increase prefix old_sigma policy))
     41      (sigma_compact_unsafe prefix labels policy))
     42      (sigma_safe prefix labels added old_sigma policy))
    4343      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    4444      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    45       (added = 0 → policy_pc_equal prefix old_sigma policy))
    46       (policy_jump_equal prefix old_sigma policy → added = 0))
     45      (added = 0 → sigma_pc_equal prefix old_sigma policy))
     46      (sigma_jump_equal prefix old_sigma policy → added = 0))
    4747    program
    4848    (λprefix.λx.λtl.λprf.λacc.
     
    165165                (* USE: added = 0 → policy_pc_equal *)
    166166                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
    167                 [2,4,6,8: cases daemon (* XXX *) ]
     167                [2,4,6,8: lapply ((pi2 ?? labels) x)
     168                  whd in match address_of_word_labels_code_mem;
     169                  normalize nodelta cases daemon (* XXX *) ]
    168170                [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
    169171                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     
    177179                |1,3,9,11: #_ normalize nodelta @refl
    178180                ]
    179              |2,5: whd in match short_jump_cond; whd in match medium_jump_cond;
     181             |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
    180182                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
    181183                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
     
    192194                cases (get_index' bool 2 0 flags) normalize nodelta
    193195                #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
    194              |3,6: whd in match short_jump_cond; whd in match medium_jump_cond;
     196             |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    195197                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
    196198                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
Note: See TracChangeset for help on using the changeset viewer.