| 1 | (**************************************************************************) |
|---|
| 2 | (* ___ *) |
|---|
| 3 | (* ||M|| *) |
|---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
|---|
| 5 | (* ||T|| *) |
|---|
| 6 | (* ||I|| Developers: *) |
|---|
| 7 | (* ||T|| The HELM team. *) |
|---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
|---|
| 9 | (* \ / *) |
|---|
| 10 | (* \ / This file is distributed under the terms of the *) |
|---|
| 11 | (* v GNU General Public License Version 2 *) |
|---|
| 12 | (* *) |
|---|
| 13 | (**************************************************************************) |
|---|
| 14 | |
|---|
| 15 | include "arithmetics/nat.ma". |
|---|
| 16 | include "basics/types.ma". |
|---|
| 17 | include "basics/deqsets.ma". |
|---|
| 18 | include "../src/ASM/Util.ma". |
|---|
| 19 | |
|---|
| 20 | inductive FunctionName : Type[0] ≝ |
|---|
| 21 | | a_function_id : ℕ → FunctionName. |
|---|
| 22 | |
|---|
| 23 | inductive CallCostLabel : Type[0] ≝ |
|---|
| 24 | | a_call_label : ℕ → CallCostLabel. |
|---|
| 25 | |
|---|
| 26 | inductive ReturnPostCostLabel : Type[0] ≝ |
|---|
| 27 | | a_return_cost_label : ℕ → ReturnPostCostLabel. |
|---|
| 28 | |
|---|
| 29 | inductive NonFunctionalLabel : Type[0] ≝ |
|---|
| 30 | | a_non_functional_label : ℕ → NonFunctionalLabel. |
|---|
| 31 | |
|---|
| 32 | inductive CostLabel : Type[0] ≝ |
|---|
| 33 | | a_call : CallCostLabel → CostLabel |
|---|
| 34 | | a_return_post : ReturnPostCostLabel → CostLabel |
|---|
| 35 | | a_non_functional_label : NonFunctionalLabel → CostLabel. |
|---|
| 36 | |
|---|
| 37 | coercion a_call. |
|---|
| 38 | coercion a_return_post. |
|---|
| 39 | coercion a_non_functional_label. |
|---|
| 40 | |
|---|
| 41 | definition ret_act_label_to_cost_label : |
|---|
| 42 | (ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝ |
|---|
| 43 | λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b]. |
|---|
| 44 | |
|---|
| 45 | coercion ret_act_label_to_cost_label. |
|---|
| 46 | |
|---|
| 47 | definition call_act_label_to_cost_label : |
|---|
| 48 | (CallCostLabel + NonFunctionalLabel) → CostLabel ≝ |
|---|
| 49 | λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b]. |
|---|
| 50 | |
|---|
| 51 | coercion call_act_label_to_cost_label. |
|---|
| 52 | |
|---|
| 53 | inductive ActionLabel : Type[0] ≝ |
|---|
| 54 | | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel |
|---|
| 55 | | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel |
|---|
| 56 | | cost_act : option NonFunctionalLabel → ActionLabel |
|---|
| 57 | | init_act : ActionLabel. |
|---|
| 58 | |
|---|
| 59 | definition is_cost_label : ActionLabel → Prop ≝ |
|---|
| 60 | λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ]. |
|---|
| 61 | |
|---|
| 62 | inductive status_class : Type[0] ≝ |
|---|
| 63 | | cl_jump : status_class |
|---|
| 64 | | cl_io : status_class |
|---|
| 65 | | cl_other : status_class. |
|---|
| 66 | |
|---|
| 67 | record abstract_status : Type[2] ≝ |
|---|
| 68 | { as_status :> Type[0] |
|---|
| 69 | ; as_execute : ActionLabel → relation as_status |
|---|
| 70 | ; as_syntactical_succ : relation as_status |
|---|
| 71 | ; as_classify : as_status → status_class |
|---|
| 72 | ; is_call_post_label : as_status → bool |
|---|
| 73 | ; as_initial : as_status → bool |
|---|
| 74 | ; as_final : as_status → bool |
|---|
| 75 | ; is_io_entering : NonFunctionalLabel → bool |
|---|
| 76 | ; is_io_exiting : NonFunctionalLabel → bool |
|---|
| 77 | }. |
|---|
| 78 | |
|---|
| 79 | definition is_act_io_entering : abstract_status → ActionLabel → bool ≝ |
|---|
| 80 | λS,l.match l with |
|---|
| 81 | [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ] |
|---|
| 82 | | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false |
|---|
| 83 | | inr c' ⇒ is_io_entering S c'] |
|---|
| 84 | | None ⇒ false |
|---|
| 85 | ] |
|---|
| 86 | | cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ] |
|---|
| 87 | | init_act ⇒ false |
|---|
| 88 | ]. |
|---|
| 89 | |
|---|
| 90 | definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝ |
|---|
| 91 | λS,l.match l with |
|---|
| 92 | [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ] |
|---|
| 93 | | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false |
|---|
| 94 | | inr c' ⇒ is_io_exiting S c'] |
|---|
| 95 | | None ⇒ false |
|---|
| 96 | ] |
|---|
| 97 | | cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ] |
|---|
| 98 | | init_act ⇒ false |
|---|
| 99 | ]. |
|---|
| 100 | |
|---|
| 101 | |
|---|
| 102 | inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝ |
|---|
| 103 | | t_base : ∀st : S.raw_trace S st st |
|---|
| 104 | | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 105 | as_execute S l st1 st2 → raw_trace S st2 st3 → |
|---|
| 106 | raw_trace S st1 st3. |
|---|
| 107 | |
|---|
| 108 | definition is_cost_act : ActionLabel → Prop ≝ |
|---|
| 109 | λact.∃l.act = cost_act l. |
|---|
| 110 | |
|---|
| 111 | definition is_call_act : ActionLabel → Prop ≝ |
|---|
| 112 | λact.∃f,l.act = call_act f l. |
|---|
| 113 | |
|---|
| 114 | definition is_labelled_ret_act : ActionLabel → Prop ≝ |
|---|
| 115 | λact.∃l.act = ret_act (Some ? l). |
|---|
| 116 | |
|---|
| 117 | definition is_unlabelled_ret_act : ActionLabel → Prop ≝ |
|---|
| 118 | λact.act = ret_act (None ?). |
|---|
| 119 | |
|---|
| 120 | definition is_non_silent_cost_act : ActionLabel → Prop ≝ |
|---|
| 121 | λact. ∃l. act = cost_act (Some ? l). |
|---|
| 122 | |
|---|
| 123 | definition is_costlabelled_act : ActionLabel → Prop ≝ |
|---|
| 124 | λact.match act with [ call_act _ _ ⇒ True |
|---|
| 125 | | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] |
|---|
| 126 | | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] |
|---|
| 127 | | init_act ⇒ False |
|---|
| 128 | ]. |
|---|
| 129 | |
|---|
| 130 | inductive well_formed_trace (S : abstract_status) : |
|---|
| 131 | ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ |
|---|
| 132 | | wf_empty : ∀st: S.well_formed_trace … (t_base S st) |
|---|
| 133 | | wf_cons_no_jump : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 134 | ∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3. |
|---|
| 135 | well_formed_trace … tl → as_classify … st1 ≠ cl_jump → |
|---|
| 136 | well_formed_trace … (t_ind … prf … tl) |
|---|
| 137 | | wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel. |
|---|
| 138 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
|---|
| 139 | well_formed_trace … tl → is_non_silent_cost_act l → |
|---|
| 140 | well_formed_trace … (t_ind … prf … tl). |
|---|
| 141 | |
|---|
| 142 | let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S) |
|---|
| 143 | (t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝ |
|---|
| 144 | match t1 |
|---|
| 145 | return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3 |
|---|
| 146 | with |
|---|
| 147 | [ t_base st ⇒ λt2.t2 |
|---|
| 148 | | t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2) |
|---|
| 149 | ]. |
|---|
| 150 | |
|---|
| 151 | interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2). |
|---|
| 152 | |
|---|
| 153 | lemma append_associative : ∀S,st1,st2,st3,st4. |
|---|
| 154 | ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. |
|---|
| 155 | ∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3). |
|---|
| 156 | #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1 |
|---|
| 157 | [ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH % |
|---|
| 158 | qed. |
|---|
| 159 | |
|---|
| 160 | definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 → |
|---|
| 161 | raw_trace … st1 st3 → Prop≝ |
|---|
| 162 | λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3. |
|---|
| 163 | |
|---|
| 164 | definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 → |
|---|
| 165 | raw_trace … st1 st3 → Prop≝ |
|---|
| 166 | λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. |
|---|
| 167 | |
|---|
| 168 | inductive silent_trace (S : abstract_status) : |
|---|
| 169 | ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ |
|---|
| 170 | | silent_empty : ∀st : S.silent_trace … (t_base S st) |
|---|
| 171 | | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2. |
|---|
| 172 | ∀tl : raw_trace S st2 st3. silent_trace … tl → |
|---|
| 173 | silent_trace … (t_ind … prf … tl). |
|---|
| 174 | |
|---|
| 175 | inductive pre_measurable_trace (S : abstract_status) : |
|---|
| 176 | ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ |
|---|
| 177 | | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st) |
|---|
| 178 | | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 179 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
|---|
| 180 | as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → |
|---|
| 181 | pre_measurable_trace … (t_ind … prf … tl) |
|---|
| 182 | | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 183 | as_classify … st1 ≠ cl_io → |
|---|
| 184 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
|---|
| 185 | is_labelled_ret_act l → pre_measurable_trace … tl → |
|---|
| 186 | pre_measurable_trace … (t_ind … prf … tl) |
|---|
| 187 | | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 188 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
|---|
| 189 | as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 → |
|---|
| 190 | pre_measurable_trace … tl → |
|---|
| 191 | pre_measurable_trace … (t_ind … prf … tl) |
|---|
| 192 | | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. |
|---|
| 193 | ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. |
|---|
| 194 | ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. |
|---|
| 195 | as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io |
|---|
| 196 | → is_call_act l1 → ¬ is_call_post_label … st1 → |
|---|
| 197 | pre_measurable_trace … t1 → pre_measurable_trace … t2 → |
|---|
| 198 | as_syntactical_succ S st1 st4 → |
|---|
| 199 | is_unlabelled_ret_act l2 → |
|---|
| 200 | pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))). |
|---|
