source: src/joint/Traces.ma @ 2484

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

fixed Traces and semantics
added commutation record (not yet finished) and proofs in lineariseProof

File size: 9.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 ; exit: program_counter
8 ; ev_genv: genv sparams globals
9(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
10 }.
11 
12
13
14record prog_params : Type[1] ≝
15 { prog_spars : sem_params
16 ; prog : joint_program prog_spars
17 ; stack_sizes : (Σi.is_internal_function_of_program … prog i) → ℕ
18(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
19 }.
20
21lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l.
22#A #B #f #P #l elim l -l [*]
23#hd #tl #IH *
24[ #Phd %1{Phd}
25| #Ptl %2{(IH Ptl)}
26]
27qed.
28
29lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x.
30#A #P #l elim l -l [*] #hd #tl #IH *
31[ #Phd %{hd} %{Phd} %1 %
32| #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1}
33]
34qed.
35
36lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l.
37#A #P #l elim l -l [ #x *] #hd #tl #IH #x *
38[ #EQ >EQ #H %1{H}
39| #Intl #Px %2{(IH … Intl Px)}
40]
41qed.
42
43lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
44#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
45
46definition make_global : prog_params → evaluation_params
47
48λpars.
49(* Invariant: a -1 block is unused in common/Globalenvs *)
50let b ≝ mk_block Code (-1) in
51let ptr ≝ mk_program_counter «b, refl …» one in
52let p ≝ prog pars in
53mk_evaluation_params
54  (prog_var_names … p)
55  (prog_spars pars)
56  ptr
57  (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
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
69axiom BadMain : String.
70
71definition make_initial_state :
72 ∀pars: prog_params.res (state_pc pars) ≝
73λpars.let p ≝ prog pars in
74  let sem_globals : evaluation_params ≝ pars in
75  let ge ≝ ev_genv sem_globals in
76  let m ≝ alloc_mem … p in
77  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
78  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
79  let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
80  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
81(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
82  let main ≝ prog_main … p in
83  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
84  (* use exit sem_globals as ra and call_dest_for_main as dest *)
85  let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in
86  ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ;
87  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
88  ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
89  match ? return λx.description_of_function … main = x → ? with
90  [ Internal fn ⇒ λprf.
91    let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in
92    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
93    let pc' ≝ eval_internal_call_pc … ge main in
94    return mk_state_pc … st' pc'
95  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
96  ] (refl …).
97  [ @(description_of_internal_function … prf)
98  | cases spb normalize //
99  ]
100qed.
101
102definition joint_classify_seq :
103  ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
104  λp,st,stmt.
105  match stmt with
106  [ CALL f args dest ⇒
107    match function_of_call ?? (ev_genv p) st f with
108    [ OK fn ⇒
109      match description_of_function … fn with
110      [ Internal _ ⇒ cl_call
111      | External _ ⇒ cl_other
112      ]
113    | Error _ ⇒ cl_other
114    ]
115  | _ ⇒ cl_other
116  ].
117
118definition joint_classify_step :
119  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
120  λp,st,stmt.
121  match stmt with
122  [ step_seq s ⇒ joint_classify_seq p st s
123  | COND _ _ ⇒ cl_jump
124  ].
125
126definition joint_classify_final :
127  ∀p : evaluation_params.joint_fin_step p → status_class ≝
128  λp,stmt.
129  match stmt with
130  [ GOTO _ ⇒ cl_other
131  | RETURN ⇒ cl_return
132  | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
133  ].
134
135definition joint_classify :
136  ∀p : evaluation_params.state_pc p → status_class ≝
137  λp,st.
138  match fetch_statement ? p … (ev_genv p) (pc … st) with
139  [ OK f_s ⇒
140    match \snd f_s with
141    [ sequential s _ ⇒ joint_classify_step p st s
142    | final s ⇒ joint_classify_final p s
143    ]
144  | Error _ ⇒ cl_other
145  ].
146
147lemma joint_classify_call : ∀p : evaluation_params.∀st.
148  joint_classify p st = cl_call →
149  ∃f,f',args,dest,next,fn,fd.
150  fetch_statement ? p … (ev_genv p) (pc … st) =
151    OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
152  function_of_call … (ev_genv p) st f' = OK ? fn ∧
153  description_of_function … (ev_genv p) fn = Internal … fd.
154#p #st
155whd in match joint_classify; normalize nodelta
156inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta
157[ * #f * [| * [ #lbl || #b #f #args ]]
158  [ * [| #a #lbl #next ]
159    [ *
160      [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
161      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
162      | #ext ] #next
163      [ whd in match joint_classify_step; whd in match joint_classify_seq;
164        normalize nodelta
165        inversion (function_of_call ?????) normalize nodelta
166        [ #fn
167          inversion (description_of_function ?? fn) #fd
168          #EQfd
169        | #e
170        ] #EQfn
171      ]
172    ]
173  ]
174| #e
175] #EQfetch
176[|*: #ABS normalize in ABS; destruct(ABS) ]
177normalize nodelta #_
178%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd}
179%{EQfd} %{EQfn} %
180qed.
181
182definition joint_after_ret : ∀p:evaluation_params.
183  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
184λp,s1,s2.
185match fetch_statement ? p … (ev_genv p) (pc … s1) with
186[ OK x ⇒
187  match \snd x with
188  [ sequential s next ⇒
189    pc … s2 = succ_pc p p (pc … s1) next
190  | _ ⇒ False (* never happens *)
191  ]
192| _ ⇒ False (* never happens *)
193].
194
195definition joint_call_ident : ∀p:evaluation_params.
196  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
197(* this is a definition without a dummy ident :
198λp,st.
199match ?
200return λx.
201  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
202  match s with
203  [ sequential s next ⇒
204    match s with
205    [ step_seq s ⇒
206      match s with
207      [ CALL f' args dest ⇒
208        function_of_call … (ev_genv p) st f'
209      | _ ⇒ Error … [ ]
210      ]
211    | _ ⇒ Error … [ ]
212    ]
213  | _ ⇒ Error … [ ]
214  ] = x → ? with
215[ OK v ⇒ λ_.v
216| Error e ⇒ λABS.⊥
217] (refl …).
218@hide_prf
219elim (joint_classify_call … (pi2 … st))
220#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
221lapply ABS -ABS
222>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
223qed. *)
224(* with a dummy ident (which is never used as seen above in the commented script)
225   I think handling of the function is easier *)
226λp,st.
227let dummy : ident ≝ an_identifier ? one in
228match fetch_statement ? p … (ev_genv p) (pc … st) with
229[ OK x ⇒
230  match \snd x with
231  [ sequential s next ⇒
232    match s with
233    [ step_seq s ⇒
234      match s with
235      [ CALL f' args dest ⇒
236        match function_of_call … (ev_genv p) st f' with
237        [ OK f ⇒ f
238        | _ ⇒ dummy
239        ]
240      | _ ⇒ dummy
241      ]
242    | _ ⇒ dummy
243    ]
244  | _ ⇒ dummy
245  ]
246| _ ⇒ dummy
247].
248
249definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
250*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
251[ #EQ destruct % #H %
252| * #NEQ % #ABS destruct elim (NEQ ?) %
253]
254qed.
255
256(*
257let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
258  match c with
259  [ Value x ⇒ OK … x
260  | Interact o f ⇒
261    ! i ← env o ;
262    io_evaluate O I X env (f i)
263  | Wrong e ⇒ Error … e
264  ].
265*)
266
267definition cost_label_of_stmt :
268  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
269  λp,s.match s with
270  [ sequential s _ ⇒
271    match s with
272    [ step_seq s ⇒
273      match s with
274      [ COST_LABEL lbl ⇒ Some ? lbl
275      | _ ⇒ None ?
276      ]
277    | _ ⇒ None ?
278    ]
279  | _ ⇒ None ?
280  ].
281
282definition joint_abstract_status :
283 ∀p : evaluation_params.
284 abstract_status ≝
285 λp.
286 mk_abstract_status
287   (* as_status ≝ *) (state_pc p)
288   (* as_execute ≝ *)
289    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
290   (* as_pc ≝ *) pcDeq
291   (* as_pc_of ≝ *) (pc …)
292   (* as_classify ≝ *) (joint_classify p)
293   (* as_label_of_pc ≝ *)
294    (λpc.
295      match fetch_statement ? p … (ev_genv p) pc with
296      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
297      | _ ⇒ None ?
298      ])
299   (* as_after_return ≝ *) (joint_after_ret p)
300   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
301   (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracBrowser for help on using the repository browser.