Changeset 1705 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Feb 16, 2012, 6:05:45 PM (8 years ago)
Author:
campbell
Message:

Checkpoint RTLabs labelling soundness work.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r1680 r1705  
    9696
    9797
    98 (* Define a notion of sound labellings of RTLabs programs. *)
    99 
    100 let rec successors (s : statement) : list label ≝
    101 match s with
    102 [ St_skip l ⇒ [l]
    103 | St_cost _ l ⇒ [l]
    104 | St_const _ _ l ⇒ [l]
    105 | St_op1 _ _ _ _ _ l ⇒ [l]
    106 | St_op2 _ _ _ _ l ⇒ [l]
    107 | St_load _ _ _ l ⇒ [l]
    108 | St_store _ _ _ l ⇒ [l]
    109 | St_call_id _ _ _ l ⇒ [l]
    110 | St_call_ptr _ _ _ l ⇒ [l]
    111 (*
    112 | St_tailcall_id _ _ ⇒ [ ]
    113 | St_tailcall_ptr _ _ ⇒ [ ]
    114 *)
    115 | St_cond _ l1 l2 ⇒ [l1; l2]
    116 | St_jumptable _ ls ⇒ ls
    117 | St_return ⇒ [ ]
    118 ].
    119 
    120 definition is_cost_label : statement → bool ≝
    121 λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
    122 
    123 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
    124 | stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l n
    125 | stlb_step : ∀l,n,H.
    126     (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' n) →
    127     steps_to_label_bound g l (S n).
    128    
    129 discriminator nat.
    130 
    131 lemma steps_to_label_bound_inv_step : ∀g,l,n.
    132   steps_to_label_bound g l n →
    133   ∀H. ¬ (bool_to_Prop (is_cost_label (lookup_present … g l H))) →
    134     (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' (pred n)).
    135 #g #l0 #n0 #H1 inversion H1
    136 [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)
    137 | #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC @IH
    138 ] qed.
    139 
    140 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
    141 
    142 let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
    143   soundly_labelled_pc (f_graph fn) (f_entry fn).
    144 
Note: See TracChangeset for help on using the changeset viewer.