source: src/joint/StatusSimulationHelper.ma @ 2851

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

partial commit

File size: 6.6 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/semanticsUtils.ma".
16include "joint/Traces.ma".
17include "common/StatusSimulation.ma".
18include "joint/semantics_blocks.ma".
19
20lemma set_no_pc_eta:
21 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
22#P * //
23qed.
24
25lemma pc_of_label_eq :
26  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
27  ∀globals,ge,bl,i_fn,lbl.
28  fetch_internal_function ? ge bl = return i_fn →
29  pc_of_label pars globals ge bl lbl =
30    OK ? (pc_of_point pars bl lbl).
31#p #p' #globals #ge #bl #i_fn #lbl #EQf
32whd in match pc_of_label;
33normalize nodelta >EQf >m_return_bind %
34qed.
35
36let rec bind_new_arity (B : Type[0]) (b : B) (E : Type[0]) (x : bind_new B E) on x : ℕ ≝
37match x with
38[bret y ⇒ 0
39|bnew f ⇒ 1 + bind_new_arity … b … (f b)
40].
41
42lemma bcompile_ok : ∀U,R,E,fresh,b.
43
44
45lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
46∀prog : joint_program P_in.
47∀stack_sizes.
48∀ f_lbls,f_regs.∀f_bl_r.∀init.
49∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
50let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
51let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
52let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
53∀st1,st1' : joint_abstract_status prog_pars_in.
54∀st2 : joint_abstract_status prog_pars_out.
55∀f,fn,a,ltrue,lfalse.
56∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
57R st1 st2 →
58 fetch_statement P_in …
59  (globalenv_noinit ? prog) (pc … st1) =
60    return 〈f, fn,  sequential … (COND P_in … a ltrue) lfalse〉 →
61 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
62            st1 = return st1' →
63as_costed (joint_abstract_status prog_pars_in) st1' →
64(*(∀mid1.∃st2'.
65   repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2)
66           = return (st_no_pc … st2') ∧
67           pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
68           last_pop … st2' = last_pop … st2)) → *)
69∃ st2'. R st1' st2' ∧
70∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
71bool_to_Prop (taaf_non_empty … taf).
72#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2
73#f #fn #a #ltrue #lfalse #R #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta
74>EQfetch >m_return_bind
75whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
76whd in match eval_statement_advance; normalize nodelta
77#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
78#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
79lapply(fetch_statement_inv … EQfetch) * #EQfn #_
80[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
81| whd in match next; normalize nodelta
82]
83whd in ⊢ (??%% → ?); #EQ destruct(EQ) #n_cost
84cases(b_graph_transform_program_fetch_statement … good … EQfetch)
85#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); #Hinit (*cases (f_bl_r ?) normalize nodelta
86[2,4: #r #tl] whd in ⊢ (%→?); #EQ >EQ -init_data
87>if_merge_right in ⊢ (% → ?); [2,4: %] *)
88* #labs * #regs
89(*[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *]*)
90** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls *
91whd in ⊢ (% → ?); #EQbl
92whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
93#seq_pre_l
94letin trans_prog  ≝ (b_graph_transform_program P_in P_out init prog)
95letin prog_pars_out ≝ (mk_prog_params P_out trans_prog stack_sizes)
96cases(? : ∃st2'.
97           repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2)
98           = return (st_no_pc … st2') ∧
99           pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
100           last_pop … st2' = last_pop … st2)
101   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
102#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
103>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
104>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
105whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
106>EQ in EQmid ⊢ %; -nxt1 #EQmid
107lapply(taaf_to_taa ???
108           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
109                                       seq_pre_l res_st2_pre_mid) ?)
110[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
111      whd in match (as_label ??); whd in match (as_pc_of ??);
112      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
113      >m_return_bind whd in match point_of_pc; normalize nodelta
114      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
115      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
116#taa_pre_mid whd in ⊢ (% → ?);
117cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
118                     return st2_cond )
119[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
120#st2_mid #EQst2_mid
121cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
122[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
123* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
124letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
125cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
126%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
127[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
128     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
129|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
130]
131qed.
Note: See TracBrowser for help on using the repository browser.