source: src/common/FEMeasurable.ma @ 2618

Last change on this file since 2618 was 2618, checked in by campbell, 7 years ago

Tidy up measurable a little.

File size: 3.6 KB
Line 
1(* Show that measurable subtraces are preserved in the front-end. *)
2
3include "common/Measurable.ma".
4
5definition normal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝
6λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
7
8(* A record giving the languages and simulation results necessary to show that
9   measurability is preserved. *)
10
11record meas_sim : Type[2] ≝ {
12  ms_C1 : preclassified_system;
13  ms_C2 : preclassified_system;
14  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
15  ms_inv : ? → ? → Type[0];
16  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
17  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
18  sim_normal :
19    ∀g1,g2.
20    ∀INV:ms_inv g1 g2.
21    ∀s1,s1',s2,tr.
22    ms_rel g1 g2 INV s1 s1' →
23    normal_state ms_C1 g1 s1 →
24    ¬ pcs_labelled ms_C1 g1 s1 →
25    ∃n. after_n_steps (S n) … (pcs_exec ms_C1) g1 s1 (λs.normal_state ms_C1 g1 s ∧ ¬ pcs_labelled ms_C1 g1 s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
26    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
27      tr = tr' ∧
28      ms_rel g1 g2 INV s2 s2'
29    );
30  sim_call_return :
31    ∀g1,g2.
32    ∀INV:ms_inv g1 g2.
33    ∀s1,s1',s2,tr.
34    ms_rel g1 g2 INV s1 s1' →
35    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
36    ¬ pcs_labelled ms_C1 g1 s1 →
37    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
38    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
39      tr = tr' ∧
40      ms_rel g1 g2 INV s2 s2'
41    );
42  sim_cost :
43    ∀g1,g2.
44    ∀INV:ms_inv g1 g2.
45    ∀s1,s1',s2,tr.
46    ms_rel g1 g2 INV s1 s1' →
47    pcs_labelled ms_C1 g1 s1 →
48    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
49    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
50      tr = tr' ∧
51      ms_rel g1 g2 INV s2 s2'
52    );
53  sim_init :
54    ∀p1,p2,s,s'.
55    ms_compiled p1 p2 →
56    make_initial_state ?? ms_C1 p1 = OK ? s →
57    make_initial_state ?? ms_C2 p2 = OK ? s' →
58    ∃INV. ms_rel ?? INV s s'
59}.
60
61(* TODO: obs eq *)
62
63definition trace_starts : ∀S. execution S io_out io_in → S → Prop ≝
64λS,t,s. match t with [ e_step _ s' _ ⇒ s = s' | _ ⇒ False ].
65
66lemma prefix_preserved :
67  ∀MS:meas_sim.
68  ∀g1,g2.
69  ∀INV:ms_inv MS g1 g2.
70  ∀max_allowed_stack.
71  ∀trace,trace',s1,s1'.
72  trace_starts ? trace s1 →
73  trace_starts ? trace' s1' →
74  ms_rel MS g1 g2 INV s1 s1' →
75  ∀m,prefix,suffix.
76  split_trace ? trace m = Some ? 〈prefix,suffix〉 →
77  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →
78  ∃m',prefix',suffix'.
79  split_trace ? trace' m' = Some ? 〈prefix',suffix'〉 ∧
80  le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
81  ∃s2,s2'. trace_starts ? suffix s2 ∧ trace_starts ? suffix' s2' ∧
82    ms_rel MS g1 g2 INV s2 s2'.
83
84theorem measured_subtrace_preserved :
85  ∀MS:meas_sim.
86  ∀p1,p2,m,n,stack_cost,max.
87  ms_compiled MS p1 p2 →
88  measurable (ms_C1 MS) p1 m n stack_cost max →
89  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
90* #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init
91#p1 #p2 #m #n #stack_cost #max #compiled
92whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?)
93* #prefix * #suffix * #subtrace * #remainder
94* * * * #split1 #split2 #subtrace_ok #terminates #max_ok
95
96
Note: See TracBrowser for help on using the repository browser.