source: src/ASM/OC_traces_to_exec.ma @ 3363

Last change on this file since 3363 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 5.3 KB
Line 
1include "ASM/Interpret2.ma".
2include "common/FlatTraces.ma".
3
4lemma OC_class_to_uncosted' : ∀loc.
5let S ≝ OC_abstract_status loc in
6∀st,cl.as_classify S st = cl →
7match cl with
8[ cl_other ⇒ True | _ ⇒ ¬as_costed … st ].
9#loc #st #cl * @OC_class_to_uncosted qed.
10
11lemma status_class_dep_match_elim'' :
12∀A : Type[0].∀P : A → Prop.∀Q : status_class → Type[0].
13∀c_return,c_jump,c_call,c_tailcall,c_other.
14∀cl.∀d : Q cl.
15(cl = cl_return → ∀d' : Q cl_return.d' ≃ d → P (c_return d')) →
16(cl = cl_jump → ∀d' : Q cl_jump.d' ≃ d →P (c_jump d')) →
17(cl = cl_call → ∀d' : Q cl_call.d' ≃ d →P (c_call d')) →
18(cl = cl_tailcall → ∀d' : Q cl_tailcall.d' ≃ d →P (c_tailcall d')) →
19(cl = cl_other → ∀d' : Q cl_other.d' ≃ d → P (c_other d')) →
20P (match cl return λcl.Q cl → A with
21   [ cl_return ⇒ c_return
22   | cl_jump ⇒ c_jump
23   | cl_call ⇒ c_call
24   | cl_tailcall ⇒ c_tailcall
25   | cl_other ⇒ c_other
26   ] d).
27#A #P #Q #c1 #c2 #c3 #c4 #c5 * /2 by / qed.
28
29lemma execute_plus : ∀n1,n2,cm,s.execute (n1+n2) cm s = execute n2 cm (execute n1 cm s).
30#n1 elim n1 -n1 [//] #n1 #IH #n2 #cm #s whd in match (S ? + ?); whd in ⊢ (??%?);
31>IH % qed.
32
33lemma OC_ft_to_execute :
34∀p : labelled_object_code.
35∀st1,st2 : Status (cm p).∀ft : flat_trace (OC_abstract_status p) st1 st2.
36execute (ft_length … ft) ? st1 = st2.
37#p #st1 #st2 #ft elim ft -st2
38[ % ]
39#st2 #st3 #pre * #no_result #ex #ncost #IH
40change with (1 + ?) in match (ft_length ????);
41>commutative_plus >execute_plus >IH @ex
42qed.
43
44lemma OC_ft_to_exec :
45∀p : labelled_object_code.
46∀st1,st2 : Status (cm p).∀ft : flat_trace (OC_abstract_status p) st1 st2.
47let C ≝ OC_preclassified_system p in
48let g ≝ make_global … C p in
49let C' ≝ pcs_to_cs C g in
50∃tr.
51exec_steps (ft_length … ft) io_out io_in C' g st1 = return 〈tr, st2〉 ∧
52intensional_trace_of_trace C' [ ] tr = ft_stack_observables … ft.
53#p #st1 #st2 #ft elim ft -st2 normalize nodelta
54[ %{[ ]} % % ]
55#st2 #st3 #pre whd in ⊢ (%→?); * #no_result #EQ_ex #cost * #tr * #H1 #H2
56%{(tr @ [ 〈st2, ?〉 ])}
57[2:
58% whd in match (ft_length ????);
59[ cut (∀n.S n = n + 1) [//] #aux >aux -aux
60  @(exec_steps_join … H1) whd in ⊢ (??%?);
61  change with (OC_result p st2)
62    in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
63  >no_result in ⊢ (??%?); normalize nodelta
64  >m_return_bind >EQ_ex in ⊢ (??%?); %
65] |*: ]
66>int_trace_append' @pair_elim' @pair_elim'
67>H2 whd in match (intensional_trace_of_trace ???);
68@pair_elim' normalize nodelta
69whd in match (intensional_state_change ???);
70@status_class_dep_match_elim''
71change with (as_classify (OC_abstract_status p) st2) in ⊢ (??%?→?); #cl
72[4: cases (absurd ? cl (OC_exclude_tailcall …)) ]
73#callee #callee_eq
74@sym_eq
75whd in match (ft_stack_observables ????); @pair_elim' normalize nodelta
76>(status_class_dep_match_rewrite … cl) normalize nodelta
77lapply (OC_class_to_uncosted' … cl) normalize nodelta
78[2,4: #_ @eq_f @eq_f >append_nil cases (as_label ? st2) // ]
79#ncost >(not_costed_no_label … ncost) >append_nil
80cases (\fst (ft_stack_observables … pre)) [2,4: #f #stack' ]
81normalize nodelta [ % |3: >append_nil % ]
82cases (? : callee I = as_call_ident … «st2, cl») try %
83lapply callee_eq whd in match (cs_callee ??);
84change with (as_classify (OC_abstract_status p) st2) in
85  ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?)?→?);
86change with (λprf.as_call_ident ? «st2, (λ_.?) prf») in
87  ⊢ (????%→?); generalize in  ⊢ (????(λ_.??(????(%?)))→?);
88lapply (refl ? (match as_classify … st2 with [ cl_call ⇒ True | _ ⇒ False ]))
89try >cl in ⊢ (??%?→?); * #f #EQ' >EQ' %
90qed.
91
92axiom OC_tlr_to_execute :
93∀p : labelled_object_code.
94∀st1,st2 : Status (cm p).∀tlr : trace_label_return (OC_abstract_status p) st1 st2.
95execute (tlr_length … tlr) ? st1 = st2.
96
97axiom OC_tlr_to_exec :
98∀p : labelled_object_code.
99∀st1,st2 : Status (cm p).∀tlr : trace_label_return (OC_abstract_status p) st1 st2.
100let C ≝ OC_preclassified_system p in
101let g ≝ make_global … C p in
102let C' ≝ pcs_to_cs C g in
103∀f,stack.
104∃tr.
105exec_steps (tlr_length … tlr) io_out io_in C' g st1 = return 〈tr, st2〉 ∧
106intensional_trace_of_trace C' (f :: stack) tr =
107 〈stack, observables_trace_label_return … tlr f〉.
108
109lemma OC_traces_to_observables :
110∀p : labelled_object_code.
111let init ≝ initialise_status … (cm p) in
112∀st1,st2 : Status (cm p).
113∀ft : flat_trace (OC_abstract_status p) init st1.
114∀tlr : trace_label_return (OC_abstract_status p) st1 st2.
115∀fn.ft_current_function … ft = Some ? fn →
116let C ≝ OC_preclassified_system p in
117observables C p (ft_length … ft) (tlr_length … tlr) =
118  return 〈ft_observables … ft, observables_trace_label_return … tlr fn〉.
119#p #st1 #st2 #ft #tlr #fn #EQ_fn
120whd
121cases (OC_ft_to_exec … ft) #tr1 * #exec1 #eq_tr1
122letin stack ≝ (tail … (\fst (ft_stack_observables … ft)))
123cut (\fst (ft_stack_observables … ft) = fn :: tail … (\fst (ft_stack_observables … ft)))
124[ lapply EQ_fn whd in ⊢ (??%?→?); whd in match ft_stack; normalize nodelta
125  cases (\fst (ft_stack_observables … ft)) normalize
126  [2: #f' #stack ] #EQ destruct % ] #EQ_stack
127cases (OC_tlr_to_exec … tlr fn stack) #tr2 * #exec2 #eq_tr2
128
129whd in match observables; normalize nodelta >m_return_bind
130>exec1 >m_return_bind >exec2 >m_return_bind
131>eq_tr1 @pair_elim' >EQ_stack
132>eq_tr2 %
133qed.
Note: See TracBrowser for help on using the repository browser.