source: src/joint/semantics_blocks.ma @ 2422

Last change on this file since 2422 was 2422, checked in by tranquil, 7 years ago

adapted joint to cl_call f

File size: 8.5 KB
Line 
1include "joint/blocks.ma".
2include "joint/Traces.ma".
3
4(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
5  match b with
6  [ nil ⇒ [ ]
7  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
8  ].*)
9
10lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv p g.∀ptr : cpointer.
11  ∀fn,pt,s.
12  fetch_function … ge ptr = OK … fn →
13  point_of_pointer ? p … ptr = pt →
14  stmt_at … (joint_if_code … fn) pt = Some ? s →
15  fetch_statement ? p … ge ptr = OK … 〈fn, s〉.
16#p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
17whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
18>EQ2 >EQ3 >m_return_bind %
19qed.
20
21include alias "basics/logic.ma".
22lemma io_evaluate_bind : ∀O,I,X,Y,env.
23∀m : IO O I X.∀f : X → IO O I Y.
24io_evaluate O I Y env (! x ← m ; f x) =
25! x ← io_evaluate O I X env m ;
26io_evaluate O I Y env (f x).
27#O #I #X #Y #env #m elim m
28[ #o #g #IH #f whd in match (! x ← Interact ????? ; ?);
29  change with (! y ← ? ; ?) in ⊢ (??%(????%?));
30  >m_bind_bind @m_bind_ext_eq #i @IH
31| #x #f %
32| #e #f %
33]
34qed.
35
36lemma fetch_function_from_block_eq :
37  ∀p,g,ge.
38  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
39  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
40#p #g #ge #ptr1 #ptr2 #EQ
41whd in match fetch_function; normalize nodelta >EQ
42@m_bind_ext_eq // qed.
43
44let rec repeat_eval_seq_no_pc
45  (p : evaluation_params) env curr_fn
46  (l : list (joint_seq p (globals p))) on l :
47  state p → res (state p) ≝
48  λst.match l with
49  [ nil ⇒ return st
50  | cons hd tl ⇒
51    ! st' ← io_evaluate … (env st) (eval_seq_no_pc p (globals p) (ev_genv p) curr_fn st hd) ;
52    repeat_eval_seq_no_pc p env curr_fn tl st'
53  ].
54
55lemma err_to_io_evaluate : ∀O,I,X,env,m.
56  io_evaluate O I X env (err_to_io … m) = m.
57#O#I#X#env * // qed.
58
59definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
60
61definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝
62  λp,g,s.match s with
63  [ COST_LABEL _ ⇒ false
64  | CALL_ID _ _ _ ⇒ false
65  | extension_call _ ⇒ false
66  | _ ⇒ true
67  ].
68
69lemma no_call_nor_label_proceed : ∀p : evaluation_params.
70∀st : state p. ∀s.
71no_call_nor_label p (globals p) s →
72eval_seq_pc p (globals p) (ev_genv p) st s = return Proceed ???.
73#p #st * // [ #f #args #dest | #c ] *
74qed.
75
76lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
77no_call_nor_label p (globals p) s →
78step_classifier … s = cl_other.
79#p * // [ #f #args #dest | #c ] *
80qed.
81
82lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
83no_call_nor_label p (globals p) s →
84cost_label_of_stmt … (sequential … s nxt) = None ?.
85#p * // #lbl#next *
86qed.
87
88definition code_compact : ∀p:sem_params.∀g.codeT p g → Prop ≝
89  λp,g,c.code_closed … c∧
90    ∀pt,ptr.code_has_point … c pt → ∃ptr'.pointer_of_point p p ptr pt = return ptr'.
91
92definition pointer_of_point_step_in_code : ∀p:sem_params.∀g.
93  ∀c,pc,step,dst.
94  code_compact p g c → step_in_code … c (point_of_pointer p p pc) step dst →
95  Σpc'.pointer_of_point p p pc dst = return pc' ≝
96  λp,g,c,pc,step,dst,c_compact,step_in.
97  match pointer_of_point p p pc dst
98  return λx.pointer_of_point p p pc dst = x → ?
99  with
100  [ OK pc' ⇒ mk_Sig ?? pc'
101  | Error e ⇒ λEQ.⊥
102  ] (refl …).
103cases step_in #nxt * #EQ1 #EQ2
104cases c_compact -c_compact #c_closed #c_compact
105elim (c_compact dst pc ?)
106[ >EQ #pc' normalize #ABS destruct(ABS)
107| elim (c_closed … EQ1) #_ whd in ⊢ (%→?);
108  >EQ2 #H @H
109]
110qed.
111
112let rec pointer_of_point_in_code
113  p g c pc dst b on b :
114  ∀l.code_compact p g c → point_of_pointer p p pc ~❨b,l❩~> dst in c →
115  Σpc'.pointer_of_point p p pc dst = return pc' ≝
116match b
117return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr'
118with
119[ nil ⇒
120  λl,c_compact,in_code.
121  match pointer_of_point p p pc dst
122  return λx.pointer_of_point p p pc dst = x → ? with
123  [ OK ptr' ⇒ mk_Sig ?? ptr'
124  | Error e ⇒ λEQ.⊥
125  ] (refl …)
126| cons hd tl ⇒
127  λl.match l return λl.? → ? → Σptr'.? with
128  [ nil ⇒ λc_compact,in_code.⊥
129  | cons mid rest ⇒ λc_compact,in_code.
130    let mid_pc ≝ pointer_of_point_step_in_code … c pc hd mid c_compact ? in
131    pi1 … (pointer_of_point_in_code ?? c mid_pc dst tl rest c_compact ?)
132  ]
133].
134[ cases l in in_code; [2: #mid #rest * ]
135  whd in ⊢ (%→?); #EQ' <EQ' in EQ; >pointer_of_point_of_pointer [2: %]
136  normalize #ABS destruct(ABS)
137| cases (pointer_of_point_in_code ?????????)
138  #ptr' >pointer_of_point_uses_block
139  [ #H @H |*:]
140  cases mid_pc -mid_pc #mid_pc @pointer_of_point_block
141| elim in_code
142| cases mid_pc -mid_pc #mid_pc #EQ
143  >(point_of_pointer_of_point … EQ)
144  cases in_code #_ #H @H
145| cases in_code #H #_ @H
146]
147qed.
148
149let rec produce_trace_any_any
150  (p : evaluation_params)
151  (st : state_pc p) fd
152  (b : list (joint_seq p (globals p))) on b :
153  ∀l : list (code_point p).
154  ∀dst : code_point p.
155  ∀st' : state p.
156  fetch_function p ? (ev_genv p) (pc … st) = return fd →
157  ∀prf1 : code_compact p (globals p) (joint_if_code … fd).
158  let src ≝ point_of_pointer p p (pc … st) in
159  if list_not_empty ? b then
160    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
161  else
162    True →
163  ∀prf2 : src ~❨b, l❩~> dst in joint_if_code … fd.
164  All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
165  repeat_eval_seq_no_pc p (io_env p) fd b st = return st' →
166  trace_any_any (joint_abstract_status p) st
167    (mk_state_pc ? st' (pointer_of_point_in_code … prf1 prf2)) ≝
168  match b
169  return λx.∀l,dst.?→?→?→?→?→?→?→?
170  with
171  [ nil ⇒
172    λl,dst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
173    (taa_base (joint_abstract_status p) st)
174      ⌈trace_any_any (joint_abstract_status p) st st ↦ ?⌉
175  | cons hd tl ⇒
176    λl.
177    match l return λx.?→?→?→?→?→?→?→?→? with
178    [ nil ⇒ λdst_pc,st',fd_prf,src_prf,dst_prf,in_code.⊥
179    | cons mid rest ⇒
180      λdst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
181      let mid_pc ≝
182        pointer_of_point_step_in_code p ? (joint_if_code … fd) (pc … st)
183          hd mid c_compact ? in
184      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd)
185      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) = x → ?
186      with
187      [ OK st_mid ⇒ λEQ2.
188        let tr_tl ≝ produce_trace_any_any ?
189            (mk_state_pc ? st_mid mid_pc)
190            fd tl rest dst ??????? in
191        (* works fast only in interactive mode:
192        taa_step … tr_tl *) ?
193      | Error _ ⇒ λEQ2.⊥
194      ] (refl …)
195    ]
196  ].[3: @(taa_step … tr_tl) |*:]
197try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc)
198try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code)
199try (cases all_other #hd_other #tl_other)
200[ whd whd in match eval_state; normalize nodelta
201  >(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
202  >m_return_bind
203  whd in match eval_statement; normalize nodelta
204  whd in match eval_step; normalize nodelta
205  >m_bind_bind
206  >(no_call_nor_label_proceed … hd_other) >m_return_bind
207  >m_bind_bind
208  >io_evaluate_bind >EQ2 >m_return_bind
209  >m_return_bind
210  whd in match succ_pc; normalize nodelta
211  >EQ_mid >EQ_mid_pc >m_return_bind %
212| whd %{fd} %{(sequential … hd nxt)}
213  %{(no_call_nor_label_other … hd_other)}
214  @(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
215|4: cases (pointer_of_point_in_code ?????????)
216  #dst_pc
217  cases l in in_code; [2: #mid #rest * ]
218  whd in ⊢ (%→?); #EQ' <EQ'
219  >pointer_of_point_of_pointer [2: %] lapply EQ1 -EQ1
220  normalize in ⊢ (%→%→?);
221  #EQ1 #EQ'' destruct cases st //
222|5: >fetch_function_from_block_eq [ @fd_prf |*: ]
223  @(pointer_of_point_block … EQ_mid_pc)
224|6: cases tl [ % ] #hd' #tl' @dst_prf
225|7: assumption
226|8,9:
227  lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize nodelta
228  [ #H @H
229  | normalize #ABS destruct(ABS)
230  ]
231|3:
232  %* #H @H -H
233  lapply tl_other lapply rest_in_code
234  cases tl [2: #hd' #tl' ]
235  cases rest [2,4: #mid' #rest']
236  [2,3: * ]
237  [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
238  | ** #nxt' * #at_mid #_ #_ * #mid_other #_
239  ]
240  whd in ⊢ (??%?);
241  [ lapply dst_prf ]
242  whd in match as_label;
243  whd in match (as_pc_of ??);
244  whd in match fetch_statement;
245  normalize nodelta
246  >(point_of_pointer_of_point … EQ_mid_pc)
247  >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc))
248  >fd_prf >m_return_bind
249  [ cases (stmt_at ????) [ #_ % ]
250    #stmt #H @H
251  | >at_mid >m_return_bind normalize nodelta
252    @(no_call_nor_label_uncosted … mid_other)
253  ]
254]
255qed.
Note: See TracBrowser for help on using the repository browser.