Changeset 2218 for src

Timestamp:

Jul 19, 2012, 6:45:49 PM (9 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:

• RTLabs/CostSpec.ma (added)
• RTLabs/Traces.ma (modified) (11 diffs)
• common/Pointers.ma (modified) (1 diff)

src/RTLabs/Traces.ma

@@ -1 +1 @@
 
 include "RTLabs/semantics.ma".
+include "RTLabs/CostSpec.ma".
 include "common/StructuredTraces.ma".
 
@@ -91 +92 @@
 ] qed.
 
-(*
-definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
-  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
-λge,s,s',t.
-match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge with
-[ State f fs m ⇒ λEX. mk_RTLabs_state ge (State f fs m) (Ras_fn_stack … s) ?
-| 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) ?
-| Returnstate rtv dst fs m ⇒ λEX. mk_RTLabs_state ge (Returnstate rtv dst fs m) (tail … (Ras_fn_stack … s)) ?
-| Finalstate r ⇒ λEX. mk_RTLabs_state ge (Finalstate r) [ ] ?
-].
-[ cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
-  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
-    whd cases stk in mtc ⊢ %; [ * ]
-    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
-    | @M2 ]
-  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
-  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
-    whd cases stk in mtc ⊢ %; [ * ]
-    #hd #tl #H @H
-  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
-  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
-    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
-    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
-  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
-  ]
-| cases (func_block_of_exec … EX) #func_block #FFP
-  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
-  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
-    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
-    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
-  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
-  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
-  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
-  ]
-| cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
-  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
-  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
-  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
-    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H 
-  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
-  ]
-| whd @refl
-] qed.*)
 
 (* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
@@ -155 +109 @@
 ].
 
-(* We define a straight "is this a cost label" pair of functions, which is
-   convenient for most of our uses here (because we can make a hypothesis of
-   it without naming the label), and a pair which return the label to fit the
-   definition of abstract_status. *)
-   
-definition is_cost_label : statement → bool ≝
-λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
+(* As with is_cost_label/cost_label_of we define a boolean function as well
+   as one which extracts the cost label so that we can use it in hypotheses
+   without naming the cost label. *)
 
 definition RTLabs_cost : state → bool ≝
@@ -170 +120 @@
 ].
 
-definition cost_label_of : statement → option costlabel ≝
-λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ].
-
 definition RTLabs_cost_label : state → option costlabel ≝
 λs. match s with
@@ -180 +127 @@
 ].
 
+(* "Program counters" need to identify the current state, either as a pair of
+   the function and current instruction, or the function being entered or
+   left.  Functions are identified by their function pointer block because 
+   this avoids introducing functions to map back pointers to function ids using
+   the global environment.  (See the comment at the start of this file, too.) *)
+
 inductive RTLabs_pc : Type[0] ≝
 | rapc_state : block → label → RTLabs_pc
@@ -186 +139 @@
 | rapc_fin : RTLabs_pc
 .
-
-definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
-#x #y @eq_block_elim
-[ #E destruct /2/
-| * #NE % #E destruct cases (NE (refl ??))
-] qed. 
 
 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
@@ -697 +644 @@
   ]
 ] qed.
-
-(* We require that labels appear after branch instructions and at the start of
-   functions.  The first is required for preciseness, the latter for soundness.
-   We will make a separate requirement for there to be a finite number of steps
-   between labels to catch loops for soundness (is this sufficient?). *)
-
-definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
-λf,s. match s return λs. labels_present ? s → Prop with
-[ St_cond _ l1 l2 ⇒ λH.
-    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
-    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
-| St_jumptable _ ls ⇒ λH.
-    (* I did have a dependent version of All here, but it's a pain. *)
-    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
-| _ ⇒ λ_. True
-]. whd in H;
-[ @(proj1 … H)
-| @(proj2 … H)
-] qed.
-
-definition well_cost_labelled_fn : internal_function → Prop ≝
-λf. (∀l. ∀H:present … (f_graph f) l.
-         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
-    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
-[ @lookup_lookup_present | cases (f_entry f) // ] qed.
 
 (* We need to ensure that any code we come across is well-cost-labelled.  We may
@@ -1406 +1328 @@
 | witness : T → inhabited T.
 
-(* We also require that program's traces are soundly labelled: for any state
-   in the execution, we can give a distance to a labelled state or termination.
-   
-   Note that this differs from the syntactic notions in earlier languages
-   because it is a global property.  In principle, we would have a loop broken
-   only by a call to a function (which necessarily has a label) and no local
-   cost label.
- *)
-
-let rec nth_state ge s
-  (trace: flat_trace io_out io_in ge s)
-  n
-  on n : option state ≝
-match n with
-[ O ⇒ Some ? s
-| S n' ⇒
-  match trace with
-  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
-  | _ ⇒ None ?
-  ]
-].
-
-definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
-λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
-
-lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
-  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
-  soundly_labelled_trace ge s' trace'.
-#ge #s #tr #s' #EV #trace' #H
-#n cases (H (S n)) #m #H' %{m} @H'
-qed.
 
 (* Define a notion of sound labellings of RTLabs programs. *)
-
-let rec successors (s : statement) : list label ≝
-match s with
-[ St_skip l ⇒ [l]
-| St_cost _ l ⇒ [l]
-| St_const _ _ _ l ⇒ [l]
-| St_op1 _ _ _ _ _ l ⇒ [l]
-| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
-| St_load _ _ _ l ⇒ [l]
-| St_store _ _ _ l ⇒ [l]
-| St_call_id _ _ _ l ⇒ [l]
-| St_call_ptr _ _ _ l ⇒ [l]
-(*
-| St_tailcall_id _ _ ⇒ [ ]
-| St_tailcall_ptr _ _ ⇒ [ ]
-*)
-| St_cond _ l1 l2 ⇒ [l1; l2]
-| St_jumptable _ ls ⇒ ls
-| St_return ⇒ [ ]
-].
 
 definition actual_successor : state → option label ≝
@@ -1506 +1377 @@
 | #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
 ] qed.
-
-definition steps_for_statement : statement → nat ≝
-λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
-
-inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
-| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
-| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
-with bound_on_steps_to_cost1 : label → nat → Prop ≝
-| bostc_step : ∀l,n,H.
-    let stmt ≝ lookup_present … g l H in
-    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
-          bound_on_steps_to_cost g l' n) →
-    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
 
 (*
@@ -1687 +1545 @@
 
 
-
-definition soundly_labelled_fn : internal_function → Prop ≝
-λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
 
 definition soundly_labelled_ge : genv → Prop ≝
@@ -2115 +1970 @@
 ] qed.
 
-definition well_cost_labelled_program : RTLabs_program → Prop ≝
-  λp. All ? (λx. let 〈id,fd〉 ≝ x in
-                 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
 (*
 theorem program_trace_exists :

src/common/Pointers.ma

@@ -42 +42 @@
 * * #z whd in ⊢ (??%?); >eqZb_z_z @refl
 qed.
+
+definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
+#x #y @eq_block_elim
+[ #E destruct /2/
+| * #NE % #E destruct cases (NE (refl ??))
+] qed. 
 
 (* This is only required for full 8051 memory spaces.