Changeset 2218


Ignore:
Timestamp:
Jul 19, 2012, 6:45:49 PM (5 years ago)
Author:
campbell
Message:

Separate out cost properties required of RTLabs programs from the
structured traces proofs. Tidy up a bit.

Location:
src
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2184 r2218  
    11
    22include "RTLabs/semantics.ma".
     3include "RTLabs/CostSpec.ma".
    34include "common/StructuredTraces.ma".
    45
     
    9192] qed.
    9293
    93 (*
    94 definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
    95   eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
    96 λge,s,s',t.
    97 match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge with
    98 [ State f fs m ⇒ λEX. mk_RTLabs_state ge (State f fs m) (Ras_fn_stack … s) ?
    99 | Callstate fd args dst fs m ⇒ λEX. mk_RTLabs_state ge (Callstate fd args dst fs m) (func_block_of_exec … EX::Ras_fn_stack … s) ?
    100 | Returnstate rtv dst fs m ⇒ λEX. mk_RTLabs_state ge (Returnstate rtv dst fs m) (tail … (Ras_fn_stack … s)) ?
    101 | Finalstate r ⇒ λEX. mk_RTLabs_state ge (Finalstate r) [ ] ?
    102 ].
    103 [ cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    104   [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    105     whd cases stk in mtc ⊢ %; [ * ]
    106     #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
    107     | @M2 ]
    108   | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
    109   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    110     whd cases stk in mtc ⊢ %; [ * ]
    111     #hd #tl #H @H
    112   | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
    113   | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
    114     cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
    115     [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
    116   | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    117   ]
    118 | cases (func_block_of_exec … EX) #func_block #FFP
    119   whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    120   [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    121   | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
    122     cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
    123     [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
    124   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    125   | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
    126   | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
    127   | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    128   ]
    129 | cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    130   [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    131   | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
    132   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    133   | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
    134     cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
    135   | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
    136   | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    137   ]
    138 | whd @refl
    139 ] qed.*)
    14094
    14195(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
     
    155109].
    156110
    157 (* We define a straight "is this a cost label" pair of functions, which is
    158    convenient for most of our uses here (because we can make a hypothesis of
    159    it without naming the label), and a pair which return the label to fit the
    160    definition of abstract_status. *)
    161    
    162 definition is_cost_label : statement → bool ≝
    163 λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
     111(* As with is_cost_label/cost_label_of we define a boolean function as well
     112   as one which extracts the cost label so that we can use it in hypotheses
     113   without naming the cost label. *)
    164114
    165115definition RTLabs_cost : state → bool ≝
     
    170120].
    171121
    172 definition cost_label_of : statement → option costlabel ≝
    173 λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ].
    174 
    175122definition RTLabs_cost_label : state → option costlabel ≝
    176123λs. match s with
     
    180127].
    181128
     129(* "Program counters" need to identify the current state, either as a pair of
     130   the function and current instruction, or the function being entered or
     131   left.  Functions are identified by their function pointer block because
     132   this avoids introducing functions to map back pointers to function ids using
     133   the global environment.  (See the comment at the start of this file, too.) *)
     134
    182135inductive RTLabs_pc : Type[0] ≝
    183136| rapc_state : block → label → RTLabs_pc
     
    186139| rapc_fin : RTLabs_pc
    187140.
    188 
    189 definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
    190 #x #y @eq_block_elim
    191 [ #E destruct /2/
    192 | * #NE % #E destruct cases (NE (refl ??))
    193 ] qed.
    194141
    195142definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
     
    697644  ]
    698645] qed.
    699 
    700 (* We require that labels appear after branch instructions and at the start of
    701    functions.  The first is required for preciseness, the latter for soundness.
    702    We will make a separate requirement for there to be a finite number of steps
    703    between labels to catch loops for soundness (is this sufficient?). *)
    704 
    705 definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
    706 λf,s. match s return λs. labels_present ? s → Prop with
    707 [ St_cond _ l1 l2 ⇒ λH.
    708     is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
    709     is_cost_label (lookup_present … (f_graph f) l2 ?) = true
    710 | St_jumptable _ ls ⇒ λH.
    711     (* I did have a dependent version of All here, but it's a pain. *)
    712     All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
    713 | _ ⇒ λ_. True
    714 ]. whd in H;
    715 [ @(proj1 … H)
    716 | @(proj2 … H)
    717 ] qed.
    718 
    719 definition well_cost_labelled_fn : internal_function → Prop ≝
    720 λf. (∀l. ∀H:present … (f_graph f) l.
    721          well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
    722     is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
    723 [ @lookup_lookup_present | cases (f_entry f) // ] qed.
    724646
    725647(* We need to ensure that any code we come across is well-cost-labelled.  We may
     
    14061328| witness : T → inhabited T.
    14071329
    1408 (* We also require that program's traces are soundly labelled: for any state
    1409    in the execution, we can give a distance to a labelled state or termination.
    1410    
    1411    Note that this differs from the syntactic notions in earlier languages
    1412    because it is a global property.  In principle, we would have a loop broken
    1413    only by a call to a function (which necessarily has a label) and no local
    1414    cost label.
    1415  *)
    1416 
    1417 let rec nth_state ge s
    1418   (trace: flat_trace io_out io_in ge s)
    1419   n
    1420   on n : option state ≝
    1421 match n with
    1422 [ O ⇒ Some ? s
    1423 | S n' ⇒
    1424   match trace with
    1425   [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
    1426   | _ ⇒ None ?
    1427   ]
    1428 ].
    1429 
    1430 definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
    1431 λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
    1432 
    1433 lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
    1434   soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
    1435   soundly_labelled_trace ge s' trace'.
    1436 #ge #s #tr #s' #EV #trace' #H
    1437 #n cases (H (S n)) #m #H' %{m} @H'
    1438 qed.
    14391330
    14401331(* Define a notion of sound labellings of RTLabs programs. *)
    1441 
    1442 let rec successors (s : statement) : list label ≝
    1443 match s with
    1444 [ St_skip l ⇒ [l]
    1445 | St_cost _ l ⇒ [l]
    1446 | St_const _ _ _ l ⇒ [l]
    1447 | St_op1 _ _ _ _ _ l ⇒ [l]
    1448 | St_op2 _ _ _ _ _ _ _ l ⇒ [l]
    1449 | St_load _ _ _ l ⇒ [l]
    1450 | St_store _ _ _ l ⇒ [l]
    1451 | St_call_id _ _ _ l ⇒ [l]
    1452 | St_call_ptr _ _ _ l ⇒ [l]
    1453 (*
    1454 | St_tailcall_id _ _ ⇒ [ ]
    1455 | St_tailcall_ptr _ _ ⇒ [ ]
    1456 *)
    1457 | St_cond _ l1 l2 ⇒ [l1; l2]
    1458 | St_jumptable _ ls ⇒ ls
    1459 | St_return ⇒ [ ]
    1460 ].
    14611332
    14621333definition actual_successor : state → option label ≝
     
    15061377| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
    15071378] qed.
    1508 
    1509 definition steps_for_statement : statement → nat ≝
    1510 λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
    1511 
    1512 inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
    1513 | bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
    1514 | bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
    1515 with bound_on_steps_to_cost1 : label → nat → Prop ≝
    1516 | bostc_step : ∀l,n,H.
    1517     let stmt ≝ lookup_present … g l H in
    1518     (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
    1519           bound_on_steps_to_cost g l' n) →
    1520     bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
    15211379
    15221380(*
     
    16871545
    16881546
    1689 
    1690 definition soundly_labelled_fn : internal_function → Prop ≝
    1691 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
    16921547
    16931548definition soundly_labelled_ge : genv → Prop ≝
     
    21151970] qed.
    21161971
    2117 definition well_cost_labelled_program : RTLabs_program → Prop ≝
    2118   λp. All ? (λx. let 〈id,fd〉 ≝ x in
    2119                  match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
    21201972(*
    21211973theorem program_trace_exists :
  • src/common/Pointers.ma

    r2185 r2218  
    4242* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4343qed.
     44
     45definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
     46#x #y @eq_block_elim
     47[ #E destruct /2/
     48| * #NE % #E destruct cases (NE (refl ??))
     49] qed.
    4450
    4551(* This is only required for full 8051 memory spaces.
Note: See TracChangeset for help on using the changeset viewer.