source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2851

Last change on this file since 2851 was 2851, checked in by piccolo, 7 years ago

partial commit

File size: 15.4 KB
Line 
1include "ERTLptr/ERTLptrToLTL.ma".
2include "ERTLptr/ERTLptr_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6include "common/AssocList.ma".
7
8
9
10(* Inefficient, replace with Trie lookup *)
11definition lookup_stack_cost ≝
12 λp.λid : ident.
13  assoc_list_lookup ? ℕ id (eq_identifier …) p.
14
15(*TO BE MOVED*)
16definition ERTLptr_status ≝
17λprog : ertlptr_program.λstack_sizes.
18joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
19
20definition LTL_status ≝
21λprog : ltl_program.λstack_sizes.
22joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
23
24axiom sigma_stored_pc : ertlptr_program → (block → label → list label) → 
25program_counter → program_counter.
26
27axiom sigma_fb_state: ertlptr_program → (block → label → list label) →
28 (block → label → list register) → list register →
29  state ERTLptr_semantics → state ERTLptr_semantics.
30
31axiom sigma_sb_state: ertlptr_program → (block → label → list label) →
32 (block → label → list register) → list register →
33  state LTL_semantics → state ERTLptr_semantics.
34
35definition dummy_state : state ERTLptr_semantics ≝
36mk_state ERTL_semantics
37   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
38
39definition dummy_state_pc : state_pc ERTLptr_semantics ≝
40mk_state_pc ? dummy_state (null_pc one) (null_pc one).
41
42
43definition sigma_fb_state_pc : ertlptr_program → (block → label → list label) →
44 (block → label → list register) →
45 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
46λprog,f_lbls,f_regs,st.
47let ge ≝ globalenv_noinit … prog in
48let globals ≝ prog_var_names … prog in
49match fetch_internal_function … ge (pc_block (pc … st)) with
50  [ OK y ⇒ ?
51  | Error e ⇒ dummy_state_pc
52  ].
53cases daemon qed.
54
55definition sigma_sb_state_pc : ertlptr_program → (block → label → list label) →
56 (block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
57λprog,f_lbls,f_regs,st.
58let ge ≝ globalenv_noinit … prog in
59let globals ≝ prog_var_names … prog in
60match fetch_internal_function … ge (pc_block (pc … st)) with
61  [ OK y ⇒ ?
62  | Error e ⇒ dummy_state_pc
63  ].
64cases daemon qed.
65
66
67definition ERTLptr_to_LTL_StatusSimulation :
68∀fix_comp : fixpoint_computer.
69∀colour : coloured_graph_computer.
70∀ prog : ertlptr_program.
71∀ f_lbls. ∀ f_regs. ∀f_bl_r.
72b_graph_transform_program_props ERTLptr_semantics LTL_semantics
73     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
74let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
75let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
76let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
77let stacksizes ≝ lookup_stack_cost … m in 
78status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
79λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood.
80    mk_status_rel ??
81    (* sem_rel ≝ *)
82         (λs1:ERTLptr_status ? ?
83          .λs2:LTL_status ? ?
84           .sigma_fb_state_pc prog f_lbls f_regs s1
85            =sigma_sb_state_pc prog f_lbls f_regs s2)
86    (* call_rel ≝ *) 
87       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
88          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
89           .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2))
90    (* sim_final ≝ *) ?.
91cases daemon
92qed.
93
94axiom as_label_ok :
95∀fix_comp,colour.
96∀prog.∀f_lbls,f_regs. ∀f_bl_r.
97∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
98     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
99∀st1,st2,fn,id,stmt.
100let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
101R st1 st2 → 
102fetch_statement ERTLptr_semantics (prog_var_names … prog)
103      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
104as_label ? st2 = as_label ? st1.
105
106
107
108
109(*
110(* Copy the proof too from previous pass *)
111axiom fetch_stmt_ok_sigma_state_ok :
112∀prog : ertlptr_program.
113∀ f_lbls,f_regs,id,fn,stmt,st.
114fetch_statement ERTLptr_semantics (prog_var_names … prog)
115    (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
116               return 〈id,fn,stmt〉 →
117let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
118                                               (f_regs (pc_block (pc … st)))) in
119st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
120sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
121*)
122
123lemma set_no_pc_eta:
124 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
125#P * //
126qed.
127
128lemma pc_of_label_eq :
129  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
130  ∀globals,ge,bl,i_fn,lbl.
131  fetch_internal_function ? ge bl = return i_fn →
132  pc_of_label pars globals ge bl lbl =
133    OK ? (pc_of_point ERTL_semantics bl lbl).
134#p #p' #globals #ge #bl #i_fn #lbl #EQf
135whd in match pc_of_label;
136normalize nodelta >EQf >m_return_bind %
137qed.
138
139lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
140 #T #x #y #EQ destruct %
141qed.
142
143
144axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
145∀prog.∀ f_lbls,f_regs.∀f_bl_r.
146∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
147     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
148∀st1,st2.
149let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
150R st1 st2 →
151pc_block (pc … st1) = pc_block (pc … st2).
152
153axiom pc_eq_sigma_commute : ∀fix_comp,colour.
154∀prog.∀ f_lbls,f_regs.∀f_bl_r.
155∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
156     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
157∀st1,st2.
158let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
159R st1 st2 →
160(pc … st1) = (pc … st2).
161
162
163axiom change_pc_sigma_commute : ∀fix_comp,colour.
164∀prog.∀ f_lbls,f_regs.∀f_bl_r.
165∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
166     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
167∀st1,st2.
168let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
169R st1 st2 →
170∀pc1,pc2.pc1 = pc2 →
171R (set_pc … pc1 st1) (set_pc … pc2 st2).
172(*
173axiom globals_commute : ∀fix_comp,colour.
174∀prog.
175∀p_out,m,n.
176∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
177prog_var_names … prog = prog_var_names … p_out.*)
178
179lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
180〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
181#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
182qed.
183
184include "joint/semantics_blocks.ma".
185include "ASM/Util.ma".
186
187lemma eval_cond_ok :
188∀fix_comp,colour.
189∀prog.
190∀ f_lbls,f_regs.∀f_bl_r.
191∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
192     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
193∀st1,st2,st1',f,fn,a,ltrue,lfalse.
194let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
195R st1 st2 →
196 fetch_statement ERTLptr_semantics …
197  (globalenv_noinit ? prog) (pc … st1) =
198    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
199let stacksizes ≝ lookup_stack_cost …
200                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 
201 eval_state ERTLptr_semantics
202   (prog_var_names … ℕ prog)
203   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
204   st1 = return st1' →
205as_costed (ERTLptr_status prog stacksizes) st1' →
206∃ st2'. R st1' st2' ∧
207∃taf : trace_any_any_free (LTL_status ? ?)
208st2 st2'.
209bool_to_Prop (taaf_non_empty … taf).
210#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
211#ltrue #lfalse #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta
212>EQfetch >m_return_bind
213whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
214whd in match eval_statement_advance; normalize nodelta
215change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
216#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
217#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
218lapply(fetch_statement_inv … EQfetch) * #EQfn #_
219[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
220| whd in match next; normalize nodelta
221]
222whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
223cases(b_graph_transform_program_fetch_statement … good … EQfetch)
224#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
225[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
226[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
227whd in match translate_step; normalize nodelta *** #blp #blm #bls *
228whd in ⊢ (% → ?); #EQbl
229whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
230#seq_pre_l
231letin stacksizes ≝ (lookup_stack_cost …
232                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
233letin p≝ (mk_prog_params LTL_semantics
234                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
235                         stacksizes)
236cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
237           pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
238           last_pop … st2' = last_pop … st2)
239   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
240#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
241>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
242>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
243whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
244>EQ in EQmid ⊢ %; -nxt1 #EQmid
245lapply(taaf_to_taa ???
246           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
247                                       seq_pre_l res_st2_pre_mid) ?)
248[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
249      whd in match (as_label ??); whd in match (as_pc_of ??);
250      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
251      >m_return_bind whd in match point_of_pc; normalize nodelta
252      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
253      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
254#taa_pre_mid whd in ⊢ (% → ?);
255cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
256                     return st2_cond )
257[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
258#st2_mid #EQst2_mid
259cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
260[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
261* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
262letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
263cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
264%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
265[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
266     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
267|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
268]
269qed.
270
271
272theorem ERTLptrToLTL_ok :
273∀fix_comp : fixpoint_computer.
274∀colour : coloured_graph_computer.
275∀p_in : ertlptr_program.
276let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
277let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
278let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
279(* what should we do with n? *)
280let stacksizes ≝ lookup_stack_cost m in
281∃[1] R.
282  status_simulation
283    (joint_status ERTLptr_semantics p_in stacksizes)
284    (joint_status LTL_semantics p_out stacksizes)
285    R.
286#fix_comp #colour #p_in
287cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
288          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
289#fregs * #f_lbls * #f_bl_r #good
290%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
291whd in match status_simulation; normalize nodelta
292whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
293whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
294change with
295  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
296#EQeval @('bind_inversion EQeval)
297** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
298#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
299cases stmt in EQfetch; -stmt
300[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
301#EQfetch
302change with (joint_classify ??) in
303                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
304[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
305  (* XXX
306  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
307  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
308  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
309  *) cases daemon
310| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
311          normalize nodelta #is_call_st1
312          (* XXX
313          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
314          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
315          #call_rel * #taa * #st2' * #sem_rel #eval_rel
316          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
317          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
318          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
319          *) cases daemon
320| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
321          normalize nodelta #n_costed
322          cases(eval_cond_ok  … good … EQst2 … EQfetch EQeval … n_costed)
323          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
324          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
325| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
326          normalize nodelta
327          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
328          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
329          % [% //] whd >(as_label_ok … good … st3) [%]
330          cases daemon (*needs lemma about preservation of fetch_statement *)
331|  cases fin_step in EQfetch;
332  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
333     >EQfetch normalize nodelta
334    cases (eval_goto_ok … good  … EQfetch EQeval)
335    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
336    % [% //] whd >(as_label_ok … good … st3) [%]
337    cases daemon (*needs lemma about preservation of fetch_statement *)
338  | (*RETURN*) #EQfetch
339     whd in match joint_classify; normalize nodelta
340    >EQfetch  normalize nodelta
341    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
342    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
343    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
344    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
345    % [2: assumption] % [2: %] % [2: assumption] % assumption
346  | (*TAILCALL*) *
347  ]
348]
349
Note: See TracBrowser for help on using the repository browser.