source: src/joint/Traces.ma @ 2645

Last change on this file since 2645 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 10.2 KB
Line 
1include "joint/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
49let spars ≝ prog_spars pars in
50let genv ≝ globalenv_noinit ? p in
51let get_pc_lbl ≝ λid,lbl.
52  ! bl ← block_of_funct_id … spars genv id ;
53  pc_of_label … genv bl lbl in
54mk_evaluation_params
55  (prog_var_names … p)
56  spars
57  (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl)
58 (* (prog_io pars) *).
59#s #H
60elim (find_symbol_exists … p s ?)
61[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
62@Exists_append_r
63@(Exists_mp … H) //
64qed.
65
66coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
67≝ make_global on _p : prog_params to evaluation_params.
68
69definition make_initial_state :
70 ∀pars: prog_params.res (state_pc pars) ≝
71λpars.let p ≝ prog pars in
72  let sem_globals : evaluation_params ≝ pars in
73  let ge ≝ ev_genv sem_globals in
74  let m0 ≝ alloc_mem … p in
75  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
76  let spp : xpointer ≝
77    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
78     pi2 … spb» in
79(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
80  let main ≝ prog_main … p in
81  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
82  (* use exit_pc as ra and call_dest_for_main as dest *)
83  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
84  ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) (prog_main … p) st0' ;
85  let st0'' ≝ set_no_pc … st0_no_pc st0' in
86  ! bl ← block_of_call … ge (inl … main) st0'';
87  ! 〈i, fn〉 ← fetch_function … ge bl ;
88  match fn with
89  [ Internal ifn ⇒
90    ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
91    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
92    return mk_state_pc … st' pc' exit_pc
93  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
94  ].
95cases m0 in H; #m1 #m2 #m3 #H
96whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
97@(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by Zlt_to_Zle_to_Zlt/
98qed.
99
100definition joint_classify_step :
101  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
102  λp,st,stmt.
103  match stmt with
104  [ step_seq _ ⇒ cl_other
105  | CALL f args dest ⇒
106    match (! bl ← block_of_call … (ev_genv p) f st ;
107            fetch_function … (ev_genv p) bl) with
108    [ OK id_fn ⇒
109      match \snd id_fn with
110      [ Internal _ ⇒ cl_call
111      | External _ ⇒ cl_other
112      ]
113    | Error _ ⇒ cl_other
114    ]
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_cost_label : ∀p,g.joint_seq p g → Prop ≝
147  λp,g,s.match s with
148  [ COST_LABEL _ ⇒ False
149  | _ ⇒ True
150  ].
151
152lemma joint_classify_call : ∀p : evaluation_params.∀st.
153  joint_classify p st = Some ? cl_call →
154  ∃i_f,f',args,dest,next,bl,i',fd'.
155  fetch_statement … (ev_genv p) (pc … st) =
156    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
157  block_of_call … (ev_genv p) f' st = OK ? bl ∧
158  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
159#p #st
160whd in match joint_classify; normalize nodelta
161inversion (fetch_statement … (ev_genv p) (pc … st))
162[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
163* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
164>m_return_bind normalize nodelta
165  [3: whd in match joint_classify_final; normalize nodelta
166    generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
167    normalize nodelta ]
168  #ABS destruct(ABS) ]
169* [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
170normalize nodelta
171[2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
172whd in match joint_classify_step;
173normalize nodelta
174inversion (block_of_call ?????)
175[ #bl #block_of_c  >m_return_bind
176  inversion (fetch_function ???)
177  [ * #i' *
178    [ #fd' #fetch' #_
179      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
180      % [ %{block_of_c} % ]
181      whd in match fetch_internal_function; normalize nodelta
182      >fetch' %
183    ]
184  ]
185]
186#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
187qed.
188
189definition joint_after_ret : ∀p:evaluation_params.
190  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
191λp,s1,s2.
192match fetch_statement … (ev_genv p) (pc … s1) with
193[ OK x ⇒
194  match \snd x with
195  [ sequential s next ⇒
196    last_pop … s2 = pc … s1 ∧
197    pc … s2 = succ_pc p (pc … s1) next
198  | _ ⇒ False (* never happens *)
199  ]
200| _ ⇒ False (* never happens *)
201].
202
203definition joint_call_ident : ∀p:evaluation_params.
204  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
205(* this is a definition without a dummy ident :
206λp,st.
207match ?
208return λx.
209  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
210  match s with
211  [ sequential s next ⇒
212    match s with
213    [ step_seq s ⇒
214      match s with
215      [ CALL f' args dest ⇒
216        function_of_call … (ev_genv p) st f'
217      | _ ⇒ Error … [ ]
218      ]
219    | _ ⇒ Error … [ ]
220    ]
221  | _ ⇒ Error … [ ]
222  ] = x → ? with
223[ OK v ⇒ λ_.v
224| Error e ⇒ λABS.⊥
225] (refl …).
226@hide_prf
227elim (joint_classify_call … (pi2 … st))
228#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
229lapply ABS -ABS
230>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
231qed. *)
232(* with a dummy ident (which is never used as seen above in the commented script)
233   I think handling of the function is easier *)
234λp,st.
235let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
236match fetch_statement … (ev_genv p) (pc … st) with
237[ OK x ⇒
238  match \snd x with
239  [ sequential s next ⇒
240    match s with
241    [ step_seq s ⇒
242      match s with
243      [ CALL f' args dest ⇒
244        match
245          (! bl ← block_of_call … (ev_genv p) f' st;
246           fetch_internal_function … (ev_genv p) bl) with
247        [ OK i_f ⇒ \fst i_f
248        | _ ⇒ dummy
249        ]
250      | _ ⇒ dummy
251      ]
252    | _ ⇒ dummy
253    ]
254  | _ ⇒ dummy
255  ]
256| _ ⇒ dummy
257].
258
259definition joint_tailcall_ident : ∀p:evaluation_params.
260  (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
261λp,st.
262let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
263match fetch_statement … (ev_genv p) (pc … st) with
264[ OK x ⇒
265  match \snd x with
266  [ final s ⇒
267    match s with
268    [ TAILCALL _ f' args ⇒
269      match
270        (! bl ← block_of_call … (ev_genv p) f' st;
271         fetch_internal_function … (ev_genv p) bl) with
272      [ OK i_f ⇒ \fst i_f
273      | _ ⇒ dummy
274      ]
275    | _ ⇒ dummy
276    ]
277  | _ ⇒ dummy
278  ]
279| _ ⇒ dummy
280].
281
282definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
283*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
284[ #EQ destruct % #H %
285| * #NEQ % #ABS destruct elim (NEQ ?) %
286]
287qed.
288
289(*
290let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
291  match c with
292  [ Value x ⇒ OK … x
293  | Interact o f ⇒
294    ! i ← env o ;
295    io_evaluate O I X env (f i)
296  | Wrong e ⇒ Error … e
297  ].
298*)
299
300definition cost_label_of_stmt :
301  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
302  λp,s.match s with
303  [ sequential s _ ⇒
304    match s with
305    [ step_seq s ⇒
306      match s with
307      [ COST_LABEL lbl ⇒ Some ? lbl
308      | _ ⇒ None ?
309      ]
310    | _ ⇒ None ?
311    ]
312  | _ ⇒ None ?
313  ].
314
315
316lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
317no_cost_label p (globals p) s →
318cost_label_of_stmt … (sequential … s nxt) = None ?.
319#p * // #lbl #next *
320qed.
321
322definition joint_abstract_status :
323 ∀p : evaluation_params.
324 abstract_status ≝
325 λp.
326 mk_abstract_status
327   (* as_status ≝ *) (state_pc p)
328   (* as_execute ≝ *)
329    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
330   (* as_pc ≝ *) pcDeq
331   (* as_pc_of ≝ *) (pc …)
332   (* as_classify ≝ *) (joint_classify p)
333   (* as_label_of_pc ≝ *)
334    (λpc.
335      match fetch_statement … (ev_genv p) pc with
336      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
337      | _ ⇒ None ?
338      ])
339   (* as_after_return ≝ *) (joint_after_ret p)
340   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
341   (* as_call_ident ≝ *) (joint_call_ident p)
342   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracBrowser for help on using the repository browser.