source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2845

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

ERTLptr to LTL correctness proof started

File size: 17.5 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.
72∀p_out,m,n.
73ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉 →
74let stacksizes ≝ lookup_stack_cost … m in
75b_graph_transform_program_props ERTLptr_semantics LTL_semantics
76     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
77status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
78λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r,p_out,m,n,EQ.
79λgood.
80    mk_status_rel ??
81    (* sem_rel ≝ *) (λs1:ERTLptr_status prog ?.
82       λs2: LTL_status ? ?.
83        sigma_fb_state_pc prog f_lbls f_regs s1 = sigma_sb_state_pc prog f_lbls f_regs s2)
84    (* call_rel ≝ *) 
85       (λs1:Σs.as_classifier … s cl_call.
86        λs2:Σs.as_classifier … s cl_call.
87         pc … s1 =sigma_stored_pc prog f_lbls (pc … s2))
88    (* sim_final ≝ *) ?.
89cases daemon
90qed.
91
92axiom as_label_ok :
93∀fix_comp,colour.
94∀prog.
95∀p_out,m,n.
96∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
97∀f_lbls,f_regs.
98∀f_bl_r.
99∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
100     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
101∀st1,st2,fn,id,stmt.
102let stack_sizes ≝ lookup_stack_cost m in
103let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
104R st1 st2 →
105fetch_statement ERTLptr_semantics (prog_var_names … prog)
106      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
107as_label (LTL_status p_out stack_sizes) st2 =
108 as_label (ERTLptr_status prog stack_sizes) st1.
109
110
111
112(*
113(* Copy the proof too from previous pass *)
114axiom fetch_stmt_ok_sigma_state_ok :
115∀prog : ertlptr_program.
116∀ f_lbls,f_regs,id,fn,stmt,st.
117fetch_statement ERTLptr_semantics (prog_var_names … prog)
118    (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
119               return 〈id,fn,stmt〉 →
120let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
121                                               (f_regs (pc_block (pc … st)))) in
122st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
123sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
124*)
125
126lemma set_no_pc_eta:
127 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
128#P * //
129qed.
130
131lemma pc_of_label_eq :
132  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
133  ∀globals,ge,bl,i_fn,lbl.
134  fetch_internal_function ? ge bl = return i_fn →
135  pc_of_label pars globals ge bl lbl =
136    OK ? (pc_of_point ERTL_semantics bl lbl).
137#p #p' #globals #ge #bl #i_fn #lbl #EQf
138whd in match pc_of_label;
139normalize nodelta >EQf >m_return_bind %
140qed.
141
142lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
143 #T #x #y #EQ destruct %
144qed.
145
146
147axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
148∀prog.
149∀p_out,m,n.
150∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
151∀ f_lbls,f_regs.
152∀f_bl_r.
153∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
154     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
155∀st1,st2.
156let stack_sizes ≝ lookup_stack_cost m in
157let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
158R st1 st2 →
159pc_block (pc … st1) = pc_block (pc … st2).
160
161axiom change_pc_sigma_commute : ∀fix_comp,colour.
162∀prog.
163∀p_out,m,n.
164∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
165∀ f_lbls,f_regs.
166∀f_bl_r.
167∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
168     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
169∀st1,st2.
170let stack_sizes ≝ lookup_stack_cost m in
171let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
172R st1 st2 →
173∀pc1,pc2.pc1 = pc2 →
174R (set_pc … pc1 st1) (set_pc … pc2 st2).
175
176axiom globals_commute : ∀fix_comp,colour.
177∀prog.
178∀p_out,m,n.
179∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
180prog_var_names … prog = prog_var_names … p_out.
181
182include "joint/semantics_blocks.ma".
183include "ASM/Util.ma".
184
185lemma eval_cond_ok :
186∀fix_comp,colour.
187∀prog.
188∀p_out,m,n.
189∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
190∀ f_lbls,f_regs.
191∀f_bl_r.
192∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
193     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
194∀st1,st2,st1',f,fn,a,ltrue,lfalse.
195let stack_sizes ≝ lookup_stack_cost m in
196let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
197R st1 st2 →
198 fetch_statement ERTLptr_semantics …
199  (globalenv_noinit ? prog) (pc … st1) =
200    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
201 eval_state ERTLptr_semantics
202   (prog_var_names … ℕ prog)
203   (ev_genv … (mk_prog_params ERTLptr_semantics prog stack_sizes))
204   st1 = return st1' →
205as_costed (ERTLptr_status prog stack_sizes) st1' →
206∃ st2'. R st1' st2' ∧
207∃taf : trace_any_any_free (LTL_status p_out stack_sizes)
208st2 st2'.
209bool_to_Prop (taaf_non_empty … taf).
210#fix_comp #colour #prog #transf_prog #stack_size #maxstack #EQtransf_prog
211#f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a #ltrue #lfalse
212#Rst1st2
213#EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
214whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
215whd in match eval_statement_advance; normalize nodelta
216change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
217#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
218#bv >set_no_pc_eta
219#EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
220 lapply(fetch_statement_inv … EQfetch) * #EQfn #_
221[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
222| whd in match next; normalize nodelta
223]
224whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) -EQ -st1'
225#n_cost
226cases(b_graph_transform_program_fetch_statement … good … EQfetch)
227#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
228[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
229[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
230whd in match translate_step; normalize nodelta * #bl *
231whd in ⊢ (% → ?); inversion (〈?,?〉) * #blp #blm #bls #EQ #EQbl >EQbl -bl
232letin p≝ (mk_prog_params LTL_semantics (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) (lookup_stack_cost stack_size))
233whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l
234cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
235           pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧
236           last_pop … st2' = last_pop … st2)
237   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
238#st2_pre_cond ** #res_st2_pre_cond #EQpc_st2_pre_cond #EQlast_pop_st2_pre_cond
239>(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) in EQt_fn1; #EQt_fn1
240
241xxxxxxxxxxxxxxxxxxxxxxxxxxxx
242
243lapply(taaf_to_taa ???
244    (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_cond EQt_fn1 seq_pre_l res_st2_pre_cond) ?)
245 
246   @(map_eval ??? mid1) lapply blp whd in match p; normalize nodelta
247   whd in match (globals ?); whd in match prog_var_names; normalize nodelta
248   change with (prog_var_names ??) in match (globals ??);
249
250lapply(produce_trace_any_any_free p st2 ?????
251
252
253%{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)}
254[ @ltrue |3: @lfalse]
255% [1,3: @(change_pc_sigma_commute … EQtransf_prog … good … Rst1st2)
256        <(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) %]
257
258
259
260 -bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2
261*** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
262#nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
263whd in EQmid1 : (??%%); destruct(EQmid1)
264%{(taaf_step_jump … (taa_base …) …) I}
265[2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 
266      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
267      >EQcond %
268|3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc;
269      normalize nodelta whd in match fetch_statement; normalize nodelta
270      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
271      >EQcond >m_return_bind normalize nodelta >m_return_bind
272      whd in match eval_statement_advance; normalize nodelta
273      change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
274      cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1
275      >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool)
276      #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta
277      >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto;
278      normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1
279      >(pc_of_label_eq … EQt_fn1) >m_return_bind %
280|*: lapply n_cost whd in match as_costed; normalize nodelta
281    [ cut((mk_state_pc ERTL_semantics
282   (sigma_state prog f_lbls f_regs
283    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
284     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
285   (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
286   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
287   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
288    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
289    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
290    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %]
291    #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
292    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
293    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *)
294    | cut((mk_state_pc ERTL_semantics
295   (sigma_state prog f_lbls f_regs
296    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
297     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
298   (succ_pc ERTL_semantics (pc ERTLptr_semantics st2)
299    (point_of_succ ERTLptr_semantics
300     (point_of_pc ERTLptr_semantics
301      (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
302   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
303   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
304    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
305     (point_of_succ ERTLptr_semantics
306      (point_of_pc ERTLptr_semantics
307       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
308    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
309    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ
310    >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
311    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
312     (point_of_succ ERTLptr_semantics
313      (point_of_pc ERTLptr_semantics
314       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
315    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *)
316]
317qed.*)
318
319
320theorem ERTLptrToLTL_ok :
321∀fix_comp : fixpoint_computer.
322∀colour : coloured_graph_computer.
323∀p_in : ertlptr_program.
324let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in
325(* what should we do with n? *)
326let stacksizes ≝ lookup_stack_cost m in
327∃[1] R.
328  status_simulation
329    (joint_status ERTLptr_semantics p_in stacksizes)
330    (joint_status LTL_semantics p_out stacksizes)
331    R.
332#fix_comp #colour #p_in
333@pair_elim * #p_out #m #n #EQp_out whd
334cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
335          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
336#fregs * #f_lbls * #f_bl_r #good
337%{(ERTLptr_to_LTL_StatusSimulation … EQp_out … good)}
338whd in match status_simulation; normalize nodelta
339whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
340whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
341change with
342  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
343#EQeval @('bind_inversion EQeval)
344** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
345#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
346cases stmt in EQfetch; -stmt
347[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
348#EQfetch
349change with (joint_classify ??) in
350                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
351[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
352  (* XXX
353  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
354  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
355  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
356  *) cases daemon
357| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
358          normalize nodelta #is_call_st1
359          (* XXX
360          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
361          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
362          #call_rel * #taa * #st2' * #sem_rel #eval_rel
363          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
364          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
365          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
366          *) cases daemon
367| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
368          normalize nodelta #n_costed
369          cases(eval_cond_ok … EQp_out … good … EQst2 … EQfetch EQeval … n_costed)
370          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
371          whd >EQst2' >(as_label_ok fix_comp colour … EQp_out … good … EQst2') [%] cases daemon (*TODO*)
372| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
373          normalize nodelta
374          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
375          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
376          % [% //] whd >(as_label_ok … good … st3) [%]
377          cases daemon (*needs lemma about preservation of fetch_statement *)
378|  cases fin_step in EQfetch;
379  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
380     >EQfetch normalize nodelta
381    cases (eval_goto_ok … good  … EQfetch EQeval)
382    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
383    % [% //] whd >(as_label_ok … good … st3) [%]
384    cases daemon (*needs lemma about preservation of fetch_statement *)
385  | (*RETURN*) #EQfetch
386     whd in match joint_classify; normalize nodelta
387    >EQfetch  normalize nodelta
388    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
389    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
390    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
391    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
392    % [2: assumption] % [2: %] % [2: assumption] % assumption
393  | (*TAILCALL*) *
394  ]
395]
396
Note: See TracBrowser for help on using the repository browser.