1 | include "joint/blocks.ma". |
---|
2 | include "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 | |
---|
10 | lemma 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 |
---|
17 | whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind |
---|
18 | >EQ2 >EQ3 >m_return_bind % |
---|
19 | qed. |
---|
20 | |
---|
21 | include alias "basics/logic.ma". |
---|
22 | lemma io_evaluate_bind : ∀O,I,X,Y,env. |
---|
23 | ∀m : IO O I X.∀f : X → IO O I Y. |
---|
24 | io_evaluate O I Y env (! x ← m ; f x) = |
---|
25 | ! x ← io_evaluate O I X env m ; |
---|
26 | io_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 | ] |
---|
34 | qed. |
---|
35 | |
---|
36 | lemma 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 |
---|
41 | whd in match fetch_function; normalize nodelta >EQ |
---|
42 | @m_bind_ext_eq // qed. |
---|
43 | |
---|
44 | let 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 | |
---|
55 | lemma 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 | |
---|
59 | definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ]. |
---|
60 | |
---|
61 | definition 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 | |
---|
69 | lemma no_call_nor_label_proceed : ∀p : evaluation_params. |
---|
70 | ∀st : state p. ∀s. |
---|
71 | no_call_nor_label p (globals p) s → |
---|
72 | eval_seq_pc p (globals p) (ev_genv p) st s = return Proceed ???. |
---|
73 | #p #st * // [ #f #args #dest | #c ] * |
---|
74 | qed. |
---|
75 | |
---|
76 | lemma no_call_nor_label_other : ∀p : evaluation_params.∀s. |
---|
77 | no_call_nor_label p (globals p) s → |
---|
78 | step_classifier … s = cl_other. |
---|
79 | #p * // [ #f #args #dest | #c ] * |
---|
80 | qed. |
---|
81 | |
---|
82 | lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt. |
---|
83 | no_call_nor_label p (globals p) s → |
---|
84 | cost_label_of_stmt … (sequential … s nxt) = None ?. |
---|
85 | #p * // #lbl#next * |
---|
86 | qed. |
---|
87 | |
---|
88 | definition 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 | |
---|
92 | definition 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 …). |
---|
103 | cases step_in #nxt * #EQ1 #EQ2 |
---|
104 | cases c_compact -c_compact #c_closed #c_compact |
---|
105 | elim (c_compact dst pc ?) |
---|
106 | [ >EQ #pc' normalize #ABS destruct(ABS) |
---|
107 | | elim (c_closed … EQ1) #_ whd in ⊢ (%→?); |
---|
108 | >EQ2 #H @H |
---|
109 | ] |
---|
110 | qed. |
---|
111 | |
---|
112 | let 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' ≝ |
---|
116 | match b |
---|
117 | return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr' |
---|
118 | with |
---|
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 | ] |
---|
147 | qed. |
---|
148 | |
---|
149 | let 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) |*:] |
---|
197 | try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc) |
---|
198 | try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code) |
---|
199 | try (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 | (* BUG? cases tl causes "Ill formed pattern" *) |
---|
235 | @(match tl with [ nil ⇒ ? | cons hd' tl' ⇒ ?]) |
---|
236 | cases rest [2,4: #mid' #rest'] |
---|
237 | [1,4: * ] |
---|
238 | [2: whd in ⊢ (%→?); #EQ' destruct(EQ') * |
---|
239 | | ** #nxt' * #at_mid #_ #_ * #mid_other #_ |
---|
240 | ] |
---|
241 | whd in ⊢ (??%?); |
---|
242 | [ lapply dst_prf ] |
---|
243 | whd in match as_label; |
---|
244 | whd in match (as_pc_of ??); |
---|
245 | whd in match fetch_statement; |
---|
246 | normalize nodelta |
---|
247 | >(point_of_pointer_of_point … EQ_mid_pc) |
---|
248 | >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc)) |
---|
249 | >fd_prf >m_return_bind |
---|
250 | [ cases (stmt_at ????) [ #_ % ] |
---|
251 | #stmt #H @H |
---|
252 | | >at_mid >m_return_bind normalize nodelta |
---|
253 | @(no_call_nor_label_uncosted … mid_other) |
---|
254 | ] |
---|
255 | ] |
---|
256 | qed. |
---|