source: src/joint/Traces.ma @ 2556

Last change on this file since 2556 was 2556, checked in by tranquil, 8 years ago

in joint semantics and traces: added a last popped calling address to state_pc, in order to have a strong enough as_after_return in joint (due to graph languages having one-to-many predecessors)
in lineariseProof: one axiom left (tailcall case)

File size: 11.0 KB
Line 
1include "joint/semantics.ma".
2include "common/StructuredTraces.ma".
3
4record evaluation_params : Type[1] ≝
5 { globals: list ident
6 ; sparams:> sem_params
7 ; ev_genv: genv sparams globals
8(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
9 }.
10 
11
12
13record prog_params : Type[1] ≝
14 { prog_spars : sem_params
15 ; prog : joint_program prog_spars
16 ; stack_sizes : ident → option ℕ
17(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
18 }.
19
20lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l.
21#A #B #f #P #l elim l -l [*]
22#hd #tl #IH *
23[ #Phd %1{Phd}
24| #Ptl %2{(IH Ptl)}
25]
26qed.
27
28lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x.
29#A #P #l elim l -l [*] #hd #tl #IH *
30[ #Phd %{hd} %{Phd} %1 %
31| #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1}
32]
33qed.
34
35lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l.
36#A #P #l elim l -l [ #x *] #hd #tl #IH #x *
37[ #EQ >EQ #H %1{H}
38| #Intl #Px %2{(IH … Intl Px)}
39]
40qed.
41
42lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
43#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
44
45definition make_global : prog_params → evaluation_params
46
47λpars.
48let p ≝ prog pars in
49mk_evaluation_params
50  (prog_var_names … p)
51  (prog_spars pars)
52  (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
53 (* (prog_io pars) *).
54#s #H
55elim (find_symbol_exists … p s ?)
56[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
57@Exists_append_r
58@(Exists_mp … H) //
59qed.
60
61coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
62≝ make_global on _p : prog_params to evaluation_params.
63
64axiom BadMain : String.
65
66definition make_initial_state :
67 ∀pars: prog_params.res (state_pc pars) ≝
68λpars.let p ≝ prog pars in
69  let sem_globals : evaluation_params ≝ pars in
70  let ge ≝ ev_genv sem_globals in
71  let m ≝ alloc_mem … p in
72  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
73  let spp : xpointer ≝
74    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
75     pi2 … spb» in
76(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
77  let main ≝ prog_main … p in
78  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
79  (* use exit_pc as ra and call_dest_for_main as dest *)
80  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
81  ! st0_no_pc ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
82  let st0'' ≝ set_no_pc … st0_no_pc st0' in
83  ! bl ← block_of_call … ge (inl … main) st0'';
84  ! 〈i, fn〉 ← fetch_function … ge bl ;
85  match fn with
86  [ Internal ifn ⇒
87    ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
88    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
89    return mk_state_pc … st' pc' exit_pc
90  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
91  ].
92
93definition joint_classify_seq :
94  ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
95  λp,st,stmt.
96  match stmt with
97  [ CALL f args dest ⇒
98    match (! bl ← block_of_call … (ev_genv p) f st ;
99            fetch_function … (ev_genv p) bl) with
100    [ OK id_fn ⇒
101      match \snd id_fn with
102      [ Internal _ ⇒ cl_call
103      | External _ ⇒ cl_other
104      ]
105    | Error _ ⇒ cl_other
106    ]
107  | _ ⇒ cl_other
108  ].
109
110definition joint_classify_step :
111  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
112  λp,st,stmt.
113  match stmt with
114  [ step_seq s ⇒ joint_classify_seq p st s
115  | COND _ _ ⇒ cl_jump
116  ].
117
118definition joint_classify_final :
119  ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
120  λp,st,stmt.
121  match stmt with
122  [ GOTO _ ⇒ cl_other
123  | RETURN ⇒ cl_return
124  | TAILCALL _ f args ⇒
125    match (! bl ← block_of_call … (ev_genv p) f st ;
126            fetch_function … (ev_genv p) bl) with
127    [ OK id_fn ⇒
128      match \snd id_fn with
129      [ Internal _ ⇒ cl_tailcall
130      | External _ ⇒ cl_return
131      ]
132    | Error _ ⇒ cl_other
133    ]
134  ].
135
136definition joint_classify :
137  ∀p : evaluation_params.state_pc p → option status_class ≝
138  λp,st.
139  ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
140  match s with
141  [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
142  | final s ⇒ Some ? (joint_classify_final p st s)
143  | FCOND _ _ _ _ ⇒ Some ? cl_jump
144  ].
145
146definition no_call : ∀p,g.joint_seq p g → Prop ≝
147  λp,g,s.match s with
148  [ CALL _ _ _ ⇒ False
149  | _ ⇒ True
150  ].
151
152definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
153  λp,g,s.match s with
154  [ COST_LABEL _ ⇒ False
155  | _ ⇒ True
156  ].
157
158lemma no_call_advance : ∀p : evaluation_params.
159∀s,nxt.∀st : state_pc p.
160no_call p (globals p) s →
161eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st.
162#p * // #f #args #dest #nxt #st *
163qed.
164
165lemma no_call_other : ∀p : evaluation_params.∀st,s.
166no_call p (globals p) s →
167joint_classify_seq … st s = cl_other.
168#p #st * // #f #args #dest *
169qed.
170
171lemma cond_call_other :
172  ∀p,globals.∀P : joint_step p globals → Prop.
173  (∀a,lbltrue.P (COND … a lbltrue)) →
174  (∀f,args,dest.P (CALL … f args dest)) →
175  (∀s.no_call ?? s → P s) →
176  ∀s.P s.
177#p #globals #P #H1 #H2 #H3 * // * /2 by / qed.
178
179lemma joint_classify_call : ∀p : evaluation_params.∀st.
180  joint_classify p st = Some ? cl_call →
181  ∃i_f,f',args,dest,next,bl,i',fd'.
182  fetch_statement … (ev_genv p) (pc … st) =
183    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
184  block_of_call … (ev_genv p) f' st = OK ? bl ∧
185  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
186#p #st
187whd in match joint_classify; normalize nodelta
188inversion (fetch_statement … (ev_genv p) (pc … st))
189[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
190* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
191>m_return_bind normalize nodelta
192  [3: whd in match joint_classify_final; normalize nodelta
193    generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
194    normalize nodelta ]
195  #ABS destruct(ABS) ]
196@cond_call_other [ #a #lbl | #f' #args #dest | #s #s_no_call ] #nxt #fetch >m_return_bind
197normalize nodelta
198[ normalize in ⊢ (%→?); #ABS destruct(ABS)
199|3: whd in match joint_classify_step;
200  normalize nodelta >(no_call_other … s_no_call) #ABS destruct(ABS)
201]
202whd in match joint_classify_step; whd in match joint_classify_seq;
203normalize nodelta
204inversion (block_of_call ?????)
205[ #bl #block_of_c  >m_return_bind
206  inversion (fetch_function ???)
207  [ * #i' *
208    [ #fd' #fetch' #_
209      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
210      % [ %{block_of_c} % ]
211      whd in match fetch_internal_function; normalize nodelta
212      >fetch' %
213    ]
214  ]
215]
216#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
217qed.
218
219definition joint_after_ret : ∀p:evaluation_params.
220  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
221λp,s1,s2.
222match fetch_statement … (ev_genv p) (pc … s1) with
223[ OK x ⇒
224  match \snd x with
225  [ sequential s next ⇒
226    last_pop … s2 = pc … s1 ∧
227    pc … s2 = succ_pc p (pc … s1) next
228  | _ ⇒ False (* never happens *)
229  ]
230| _ ⇒ False (* never happens *)
231].
232
233definition joint_call_ident : ∀p:evaluation_params.
234  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
235(* this is a definition without a dummy ident :
236λp,st.
237match ?
238return λx.
239  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
240  match s with
241  [ sequential s next ⇒
242    match s with
243    [ step_seq s ⇒
244      match s with
245      [ CALL f' args dest ⇒
246        function_of_call … (ev_genv p) st f'
247      | _ ⇒ Error … [ ]
248      ]
249    | _ ⇒ Error … [ ]
250    ]
251  | _ ⇒ Error … [ ]
252  ] = x → ? with
253[ OK v ⇒ λ_.v
254| Error e ⇒ λABS.⊥
255] (refl …).
256@hide_prf
257elim (joint_classify_call … (pi2 … st))
258#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
259lapply ABS -ABS
260>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
261qed. *)
262(* with a dummy ident (which is never used as seen above in the commented script)
263   I think handling of the function is easier *)
264λp,st.
265let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
266match fetch_statement … (ev_genv p) (pc … st) with
267[ OK x ⇒
268  match \snd x with
269  [ sequential s next ⇒
270    match s with
271    [ step_seq s ⇒
272      match s with
273      [ CALL f' args dest ⇒
274        match
275          (! bl ← block_of_call … (ev_genv p) f' st;
276           fetch_internal_function … (ev_genv p) bl) with
277        [ OK i_f ⇒ \fst i_f
278        | _ ⇒ dummy
279        ]
280      | _ ⇒ dummy
281      ]
282    | _ ⇒ dummy
283    ]
284  | _ ⇒ dummy
285  ]
286| _ ⇒ dummy
287].
288
289definition joint_tailcall_ident : ∀p:evaluation_params.
290  (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
291λp,st.
292let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
293match fetch_statement … (ev_genv p) (pc … st) with
294[ OK x ⇒
295  match \snd x with
296  [ final s ⇒
297    match s with
298    [ TAILCALL _ f' args ⇒
299      match
300        (! bl ← block_of_call … (ev_genv p) f' st;
301         fetch_internal_function … (ev_genv p) bl) with
302      [ OK i_f ⇒ \fst i_f
303      | _ ⇒ dummy
304      ]
305    | _ ⇒ dummy
306    ]
307  | _ ⇒ dummy
308  ]
309| _ ⇒ dummy
310].
311
312definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
313*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
314[ #EQ destruct % #H %
315| * #NEQ % #ABS destruct elim (NEQ ?) %
316]
317qed.
318
319(*
320let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
321  match c with
322  [ Value x ⇒ OK … x
323  | Interact o f ⇒
324    ! i ← env o ;
325    io_evaluate O I X env (f i)
326  | Wrong e ⇒ Error … e
327  ].
328*)
329
330definition cost_label_of_stmt :
331  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
332  λp,s.match s with
333  [ sequential s _ ⇒
334    match s with
335    [ step_seq s ⇒
336      match s with
337      [ COST_LABEL lbl ⇒ Some ? lbl
338      | _ ⇒ None ?
339      ]
340    | _ ⇒ None ?
341    ]
342  | _ ⇒ None ?
343  ].
344
345
346lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
347no_cost_label p (globals p) s →
348cost_label_of_stmt … (sequential … s nxt) = None ?.
349#p * // #lbl #next *
350qed.
351
352definition joint_abstract_status :
353 ∀p : evaluation_params.
354 abstract_status ≝
355 λp.
356 mk_abstract_status
357   (* as_status ≝ *) (state_pc p)
358   (* as_execute ≝ *)
359    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
360   (* as_pc ≝ *) pcDeq
361   (* as_pc_of ≝ *) (pc …)
362   (* as_classify ≝ *) (joint_classify p)
363   (* as_label_of_pc ≝ *)
364    (λpc.
365      match fetch_statement … (ev_genv p) pc with
366      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
367      | _ ⇒ None ?
368      ])
369   (* as_after_return ≝ *) (joint_after_ret p)
370   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
371   (* as_call_ident ≝ *) (joint_call_ident p)
372   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracBrowser for help on using the repository browser.