source: src/common/FEMeasurable.ma @ 2668

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

Intermediate measurable proof check-in before I change its traces again.

File size: 8.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  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
19  ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2);
20  sim_normal :
21    ∀g1,g2.
22    ∀INV:ms_inv g1 g2.
23    ∀s1,s1',s2,tr.
24    ms_rel g1 g2 INV s1 s1' →
25    normal_state ms_C1 g1 s1 →
26    ¬ pcs_labelled ms_C1 g1 s1 →
27    ∃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〉) →
28    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
29      tr = tr' ∧
30      ms_rel g1 g2 INV s2 s2'
31    );
32  sim_call_return :
33    ∀g1,g2.
34    ∀INV:ms_inv g1 g2.
35    ∀s1,s1',s2,tr.
36    ms_rel g1 g2 INV s1 s1' →
37    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
38    ¬ pcs_labelled ms_C1 g1 s1 →
39    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
40    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
41      tr = tr' ∧
42      ms_rel g1 g2 INV s2 s2'
43    );
44  sim_cost :
45    ∀g1,g2.
46    ∀INV:ms_inv g1 g2.
47    ∀s1,s1',s2,tr.
48    ms_rel g1 g2 INV s1 s1' →
49    pcs_labelled ms_C1 g1 s1 →
50    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
51    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
52      tr = tr' ∧
53      ms_rel g1 g2 INV s2 s2'
54    );
55  sim_init :
56    ∀p1,p2,s,s'.
57    ms_compiled p1 p2 →
58    make_initial_state ?? ms_C1 p1 = OK ? s →
59    make_initial_state ?? ms_C2 p2 = OK ? s' →
60    ∃INV. ms_rel ?? INV s s'
61}.
62
63(* TODO: obs eq *)
64
65definition trace_starts : ∀S. execution S io_out io_in → S → Prop ≝
66λS,t,s. match t with [ e_step _ s' _ ⇒ s = s' | _ ⇒ False ].
67
68(* TODO: too many of these lemmas, slim it down*)
69
70lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
71  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 →
72  ∃a'. a = 〈tr,s〉::a' ∧
73  ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨
74  (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)).
75#fx #g #tr #s #n #a #b
76>exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?);
77cases (is_final … s)
78[ whd in ⊢ (??%? → ?); cases (split_trace ?????)
79  [ #E whd in E:(??%%); destruct
80  | * #a' #b' #E whd in E:(??%%); destruct
81    %{a'} %{(refl ??)} %1 %{(refl ??)} %
82  ]
83| #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct
84  %{[ ]} %{(refl ??)} %2 %{r} /4/
85] qed.
86
87lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b.
88  split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 →
89  ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧
90  ∃a'. a = 〈tr,s'〉::a' ∧
91  ((is_final … fx g s' = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s')) n = Some ? 〈a',b〉) ∨
92  (∃r. is_final … fx g s' = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s')).
93#fx #g #s #n #a #b
94cases (step … fx g s)
95[ #o #i whd in ⊢ (??%? → ?); #E destruct
96| * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split
97| #err #E whd in E:(??%%); destruct
98] qed.
99
100lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b.
101  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 →
102  a = [〈tr,s〉] ∧
103  ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨
104  (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)).
105#fx #g #tr #s #a #b #split
106cases (split_trace_S … split)
107#a' * #E1 *
108[ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)}
109  %1 %{notfinal} %
110| * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)}
111  %2 %{r} %{final} %
112] qed.
113 
114
115lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
116  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 →
117  ∃a'. a = 〈tr,s〉::a' ∧
118  is_final … fx g s = None ? ∧
119  ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧
120  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉.
121#fx #g #tr #s #n #a #b #splitSS
122cases (split_trace_S … splitSS)
123#a' * #E1 *
124[ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ]
125  cases (step … s) in splitS ⊢ %;
126  [ #o #i #E whd in E:(??%%); destruct
127  | * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS
128  | #m  #E whd in E:(??%%); destruct
129  ]
130| * #r * * * #final #En #Ea #Eb destruct
131] qed.
132
133lemma stack_labelled_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
134  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
135  pcs_labelled C g s1 →
136  stack_after (pcs_to_cs C g stack) current trace = current.
137#C #g #s1 #trace #s2 #stack #current #EXEC
138cases (exec_steps_S … EXEC)
139#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
140#CS
141whd in ⊢ (??%?); whd in match (cs_classify ??); >CS
142
143
144(* WIP commented out*)
145lemma prefix_preserved :
146  ∀MS:meas_sim.
147  ∀g,g'.
148  ∀INV:ms_inv MS g g'.
149  ∀max_allowed_stack.
150  ∀s1,s1'.
151  ms_rel MS g g' INV s1 s1' →
152
153  ∀m,prefix,sf.
154  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
155  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →
156
157  ∃m',prefix',sf'.
158    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
159    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧
160 
161    ms_rel MS g g' INV sf sf'.
162* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #sim_normal #sim_call_return #sim_cost #sim_init
163#g #g' #INV #max #s1 #s1' #REL
164#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
165generalize in match 0; (* current stack level *)
166@(nat_elim1 m0)
167*
168[ #_ #current_stack #s1 #s1' #REL #prefix #sf #exec whd in exec:(??%?); destruct
169  #max_ok %{0} %{[]} %{s1'}
170  % [ % // | // ]
171| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #exec #max_ok
172  cases (true_or_false_Prop … (pcs_labelled … s1))
173  [ #CS
174    cases (exec_steps_split 1 … exec) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
175    lapply (sim_cost … s2 ? REL CS ?)
176    [ @(exec_steps_after_n_noinv … EXEC1) % | skip ]
177    #AFTER'
178    cases (after_n_exec_steps … AFTER')
179    #prefix' * #s2' * #EXEC1' * #Etrace #R2
180    cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 ?)
181    [ 2: // | 3: @(transitive_le … max_ok) >E1 <max_stack_append
182
183     @le_maxr
184    #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
185    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
186    % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | cases daemon ] | @R2
187  |
188    %{trace1 }
189
190  cases (exec_steps_S … exec) #notfinal * #tr' * #s' * #tl * * #E #STEP #EXEC'
191  cases (true_or_false_Prop … (pcs_labelled … s1))
192  [ #CS lapply (sim_cost … s' tr' REL CS ?)
193    [ @(exec_steps_after_n_noinv … whd >notfinal whd >STEP whd % ]
194    #AFTER %{1}
195    [ 3: whd in match (after_n_steps ????? s1 ??);
196      >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?);
197lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?);
198[
199| #CL
200
201theorem measured_subtrace_preserved :
202  ∀MS:meas_sim.
203  ∀p1,p2,m,n,stack_cost,max.
204  ms_compiled MS p1 p2 →
205  measurable (ms_C1 MS) p1 m n stack_cost max →
206  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
207* #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init
208#p1 #p2 #m #n #stack_cost #max #compiled
209whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?)
210* #prefix * #suffix * #subtrace * #remainder
211* * * * #split1 #split2 #subtrace_ok #terminates #max_ok
212
213*)
Note: See TracBrowser for help on using the repository browser.