source: src/common/FEMeasurable.ma @ 2649

Last change on this file since 2649 was 2644, checked in by campbell, 8 years ago

Commit some work on FEMeasurable before trying to do something nicer
than exec_inf_aux/split_trace.

File size: 7.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
66(* TODO: too many of these lemmas, slim it down*)
67
68lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
69  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 →
70  ∃a'. a = 〈tr,s〉::a' ∧
71  ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨
72  (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)).
73#fx #g #tr #s #n #a #b
74>exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?);
75cases (is_final … s)
76[ whd in ⊢ (??%? → ?); cases (split_trace ?????)
77  [ #E whd in E:(??%%); destruct
78  | * #a' #b' #E whd in E:(??%%); destruct
79    %{a'} %{(refl ??)} %1 %{(refl ??)} %
80  ]
81| #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct
82  %{[ ]} %{(refl ??)} %2 %{r} /4/
83] qed.
84
85lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b.
86  split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 →
87  ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧
88  ∃a'. a = 〈tr,s'〉::a' ∧
89  ((is_final … fx g s' = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s')) n = Some ? 〈a',b〉) ∨
90  (∃r. is_final … fx g s' = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s')).
91#fx #g #s #n #a #b
92cases (step … fx g s)
93[ #o #i whd in ⊢ (??%? → ?); #E destruct
94| * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split
95| #err #E whd in E:(??%%); destruct
96] qed.
97
98lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b.
99  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 →
100  a = [〈tr,s〉] ∧
101  ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨
102  (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)).
103#fx #g #tr #s #a #b #split
104cases (split_trace_S … split)
105#a' * #E1 *
106[ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)}
107  %1 %{notfinal} %
108| * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)}
109  %2 %{r} %{final} %
110] qed.
111 
112
113lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
114  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 →
115  ∃a'. a = 〈tr,s〉::a' ∧
116  is_final … fx g s = None ? ∧
117  ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧
118  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉.
119#fx #g #tr #s #n #a #b #splitSS
120cases (split_trace_S … splitSS)
121#a' * #E1 *
122[ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ]
123  cases (step … s) in splitS ⊢ %;
124  [ #o #i #E whd in E:(??%%); destruct
125  | * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS
126  | #m  #E whd in E:(??%%); destruct
127  ]
128| * #r * * * #final #En #Ea #Eb destruct
129] qed.
130
131(* WIP commented out
132lemma prefix_preserved :
133  ∀MS:meas_sim.
134  ∀g1,g2.
135  ∀INV:ms_inv MS g1 g2.
136  ∀max_allowed_stack.
137  ∀s1,s1',tr,tr'.
138  ms_rel MS g1 g2 INV s1 s1' →
139 
140  let trace ≝ (exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr,s1〉)) in
141  let trace' ≝ (exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr',s1'〉)) in
142 
143  ∀m,prefix,suffix.
144  split_trace … trace m = Some ? 〈prefix,suffix〉 →
145  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →
146
147  ∃m',prefix',suffix'.
148    split_trace … trace' m' = Some ? 〈prefix',suffix'〉 ∧
149    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
150 
151  ∃s2,s2',tr2,tr2'.
152    suffix = exec_inf_aux ?? (pcs_exec …  (ms_C1 MS)) g1 (Value … 〈tr2,s2〉) ∧
153    suffix' = exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr2',s2'〉) ∧
154    ms_rel MS g1 g2 INV s2 s2'.
155* #C1 #C2 #compiled #inv #stack #rel #sim_normal #sim_call_return #sim_cost #sim_init
156#g1 #g2 #INV #max #s1 #s1' #tr #tr' #REL
157letin trace ≝ (exec_inf_aux ?????)
158letin trace' ≝ (exec_inf_aux ?????)
159#m0
160@(nat_elim1 m0)
161*
162[ #_ #prefix #suffix #split whd in split:(??%?); destruct
163  #max_ok %{0} %{[]} %{trace'}
164  % [ % // | %{s1} %{s1'} %{tr} %{tr'} /3/ ]
165| *
166  [ (* m = 1; just extracts the current state *)
167    #_ #prefix #suffix #split #max_ok
168    cases (split_trace_1 … split) #E1 #foo
169    %{1} %{[〈tr',s1'〉]} %{(exec_inf_aux … (step … s1'))}
170    % [ %
171 #m #IH #prefix #suffix #split #max_ok
172  (* clean up first step? *)
173  cases (true_or_false_Prop … (pcs_labelled … s1))
174  [ #CS cases (split_trace_S … split) #trace1 * #Etrace *
175    [ * #notfinal #split1
176    lapply (sim_cost … REL CS)
177    [ 3: whd in match (after_n_steps ????? s1 ??);
178      >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?);
179lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?);
180[
181| #CL
182
183theorem measured_subtrace_preserved :
184  ∀MS:meas_sim.
185  ∀p1,p2,m,n,stack_cost,max.
186  ms_compiled MS p1 p2 →
187  measurable (ms_C1 MS) p1 m n stack_cost max →
188  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
189* #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init
190#p1 #p2 #m #n #stack_cost #max #compiled
191whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?)
192* #prefix * #suffix * #subtrace * #remainder
193* * * * #split1 #split2 #subtrace_ok #terminates #max_ok
194
195*)
Note: See TracBrowser for help on using the repository browser.