Changeset 1675 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Feb 6, 2012, 3:33:52 PM (8 years ago)
Author:
campbell
Message:

Some work on sound labelled for RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

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