Changeset 2297


Ignore:
Timestamp:
Aug 16, 2012, 6:03:21 PM (7 years ago)
Author:
campbell
Message:

Nicer form of steps until cost label bound in RTLabs.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2294 r2297  
    5959].
    6060
    61 definition steps_for_statement : statement → nat ≝
    62 λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
     61(* To show that the labelling is sound we need a bound on the number of
     62   instructions in the current function until the next cost label. *)
    6363
    64 inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
    65 | bostc_here : ∀l,n,H.
    66     is_cost_label (lookup_present … g l H) →
    67     bound_on_steps_to_cost g l n
    68 | bostc_later : ∀l,n,H.
    69     ¬ is_cost_label (lookup_present … g l H) →
    70     bound_on_steps_to_cost1 g l n →
    71     bound_on_steps_to_cost g l n
    72 with bound_on_steps_to_cost1 : label → nat → Prop ≝
    73 | bostc_step : ∀l,n,H.
     64inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝
     65| boitc_step : ∀l,n,H.
    7466    let stmt ≝ lookup_present … g l H in
    7567    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
    76           bound_on_steps_to_cost g l' n) →
    77     bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
     68          bound_on_instrs_to_cost' g l' n) →
     69    bound_on_instrs_to_cost g l (S n)
     70with bound_on_instrs_to_cost' : label → nat → Prop ≝
     71| boitc_here : ∀l,n,H.
     72    is_cost_label (lookup_present … g l H) →
     73    bound_on_instrs_to_cost' g l n
     74| boitc_later : ∀l,n,H.
     75    ¬ is_cost_label (lookup_present … g l H) →
     76    bound_on_instrs_to_cost g l n →
     77    bound_on_instrs_to_cost' g l n.
    7878
    7979definition soundly_labelled_fn : internal_function → Prop ≝
    80 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
     80λf. ∀l. present … (f_graph f) l → ∃n. bound_on_instrs_to_cost (f_graph f) l n.
    8181
    8282definition well_cost_labelled_program : RTLabs_program → Prop ≝
  • src/RTLabs/Traces.ma

    r2296 r2297  
    13851385] qed.
    13861386
    1387 (*
    1388 lemma steps_to_label_bound_inv : ∀g,l,n.
    1389   steps_to_label_bound g l n →
    1390   ∀H. let stmt ≝ lookup_present … g l H in
    1391   ∃n'. n = steps_for_statement stmt + n' ∧
    1392   (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
    1393         (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
    1394         steps_to_label_bound g l' n').
    1395 #g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
    1396 % [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
     1387(* Establish a link between the number of instructions until the next cost
     1388   label and the number of states. *)
     1389
     1390
     1391definition steps_for_statement : statement → nat ≝
     1392λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
     1393
     1394inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
     1395| bostc_here : ∀l,n,H.
     1396    is_cost_label (lookup_present … g l H) →
     1397    bound_on_steps_to_cost g l n
     1398| bostc_later : ∀l,n,H.
     1399    ¬ is_cost_label (lookup_present … g l H) →
     1400    bound_on_steps_to_cost1 g l n →
     1401    bound_on_steps_to_cost g l n
     1402with bound_on_steps_to_cost1 : label → nat → Prop ≝
     1403| bostc_step : ∀l,n,H.
     1404    let stmt ≝ lookup_present … g l H in
     1405    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
     1406          bound_on_steps_to_cost g l' n) →
     1407    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
     1408
     1409let rec bound_on_steps_succ g l n (H:bound_on_steps_to_cost g l n) on H
     1410 : bound_on_steps_to_cost g l (S n) ≝
     1411match H with
     1412[ bostc_here l n Pr Cs ⇒ ?
     1413| bostc_later l n H' CS B ⇒ ?
     1414] and bound_on_steps1_succ g l n (H:bound_on_steps_to_cost1 g l n) on H
     1415: bound_on_steps_to_cost1 g l (S n) ≝
     1416match H with
     1417[ bostc_step l n Pr Sc ⇒ ?
     1418].
     1419[ %1 //
     1420| %2 /2/
     1421| >plus_n_Sm % /3/
     1422] qed.
     1423
     1424let rec bound_on_steps_stmt g l n P (H:bound_on_steps_to_cost1 g l (plus (steps_for_statement (lookup_present … g l P)) n))
     1425: bound_on_steps_to_cost1 g l (S (S n)) ≝ ?.
     1426cases (lookup_present ? statement ???) in H; /2/
    13971427qed.
    1398   *) 
    1399 
    1400 (*
    1401 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
    1402 
    1403 let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
    1404   soundly_labelled_pc (f_graph fn) (f_entry fn).
    1405 
    1406 
    1407 definition soundly_labelled_frame : frame → Prop ≝
    1408 λf. soundly_labelled_pc (f_graph (func f)) (next f).
    1409 
    1410 definition soundly_labelled_state : state → Prop ≝
    1411 λs. match s with
    1412 [ State f _ _ ⇒ soundly_labelled_frame f
    1413 | Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
    1414 | Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
    1415 ].
    1416 *)
     1428
     1429let rec bound_on_instrs_to_steps g l n
     1430  (B:bound_on_instrs_to_cost g l n)
     1431on B : bound_on_steps_to_cost1 g l (times n 2) ≝ ?
     1432and bound_on_instrs_to_steps' g l n
     1433  (B:bound_on_instrs_to_cost' g l n)
     1434on B : bound_on_steps_to_cost g l (times n 2) ≝ ?.
     1435[ cases B #l' #n' #H #EX @bound_on_steps_stmt [ @H | % #l'' #SC @bound_on_instrs_to_steps' @EX @SC ]
     1436| cases B
     1437  [ #l' #n' #H #CS %1 //
     1438  | #l' #n' #H #CS #B' %2 [ @H | @CS | @bound_on_instrs_to_steps @B' ]
     1439  ]
     1440] qed.
     1441
     1442
    14171443definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
    14181444λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
     
    15701596whd in ⊢ (% → ?); * #SLF #_
    15711597cases (SLF (next f) (next_ok f)) #n #B1
    1572 %{n} % @B1
     1598% [2: % /2/ | skip ]
    15731599qed.
    15741600
Note: See TracChangeset for help on using the changeset viewer.