source: src/common/FEMeasurable.ma @ 2608

Last change on this file since 2608 was 2597, checked in by campbell, 8 years ago

Some work in progress on measurable subtrace preservation.

File size: 3.5 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 : ? → ? → Prop;
16  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
17  sim_normal :
18    ∀g1,g2.
19    ∀INV:ms_inv g1 g2.
20    ∀s1,s1',s2,tr.
21    ms_rel g1 g2 INV s1 s1' →
22    normal_state ms_C1 g1 s1 →
23    ¬ pcs_labelled ms_C1 g1 s1 →
24    ∃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〉) →
25    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
26      tr = tr' ∧
27      ms_rel g1 g2 INV s2 s2'
28    );
29  sim_call_return :
30    ∀g1,g2.
31    ∀INV:ms_inv g1 g2.
32    ∀s1,s1',s2,tr.
33    ms_rel g1 g2 INV s1 s1' →
34    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
35    ¬ pcs_labelled ms_C1 g1 s1 →
36    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
37    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
38      tr = tr' ∧
39      ms_rel g1 g2 INV s2 s2'
40    );
41  sim_cost :
42    ∀g1,g2.
43    ∀INV:ms_inv g1 g2.
44    ∀s1,s1',s2,tr.
45    ms_rel g1 g2 INV s1 s1' →
46    pcs_labelled ms_C1 g1 s1 →
47    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
48    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
49      tr = tr' ∧
50      ms_rel g1 g2 INV s2 s2'
51    );
52  sim_init :
53    ∀p1,p2,s,s'.
54    ms_compiled p1 p2 →
55    make_initial_state ?? ms_C1 p1 = OK ? s →
56    make_initial_state ?? ms_C2 p2 = OK ? s' →
57    ∃INV. ms_rel ?? INV s s'
58}.
59
60(* TODO: obs eq *)
61
62definition trace_starts : ∀S. execution S io_out io_in → S → Prop ≝
63λS,t,s. match t with [ e_step _ s' _ ⇒ s = s' | _ ⇒ False ].
64
65lemma prefix_preserved :
66  ∀MS:meas_sim.
67  ∀g1,g2.
68  ∀INV:ms_inv MS g1 g2.
69  ∀max_allowed_stack.
70  ∀trace,trace',s1,s1'.
71  trace_starts ? trace s1 →
72  trace_starts ? trace' s1' →
73  ms_rel MS g1 g2 INV s1 s1' →
74  ∀m,prefix,suffix.
75  split_trace (ms_C1 MS) ? trace m = Some ? 〈prefix,suffix〉 →
76  le (max_stack (ms_C1 MS) prefix) max_allowed_stack →
77  ∃m',prefix',suffix'.
78  split_trace (ms_C2 MS) ? trace' m' = Some ? 〈prefix',suffix'〉 ∧
79  le (max_stack (ms_C1 MS) prefix') max_allowed_stack ∧
80  ∃s2,s2'. trace_starts ? suffix s2 ∧ trace_starts ? suffix' s2' ∧
81    ms_rel g1 g2 INV s2 s2'.
82
83theorem measured_subtrace_preserved :
84  ∀MS:meas_sim.
85  ∀p1,p2,m,n,stack_cost,max.
86  ms_compiled MS p1 p2 →
87  measurable (ms_C1 MS) p1 m n stack_cost max →
88  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
89* #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init
90#p1 #p2 #m #n #stack_cost #max #compiled
91whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?)
92* #prefix * #suffix * #subtrace * #remainder
93* * * * #split1 #split2 #subtrace_ok #terminates #max_ok
94
95
Note: See TracBrowser for help on using the repository browser.