1 | include "joint/blocks.ma". |
---|
2 | include "joint/Traces.ma". |
---|
3 | include "joint/semanticsUtils.ma". |
---|
4 | |
---|
5 | (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ |
---|
6 | match b with |
---|
7 | [ nil ⇒ [ ] |
---|
8 | | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl |
---|
9 | ].*) |
---|
10 | |
---|
11 | definition repeat_eval_seq_no_pc ≝ |
---|
12 | λp.λpars : evaluation_params p.λcurr_id. |
---|
13 | m_fold … (eval_seq_no_pc … (ev_genv … pars) curr_id). |
---|
14 | |
---|
15 | lemma repeat_eval_seq_no_pc_append : |
---|
16 | ∀p,pars,curr_id,L1,L2,s. |
---|
17 | repeat_eval_seq_no_pc p pars curr_id (L1@L2) s = |
---|
18 | ! s' ← repeat_eval_seq_no_pc p pars curr_id L1 s; |
---|
19 | repeat_eval_seq_no_pc p pars curr_id L2 s' ≝ |
---|
20 | λp,pars,curr_id.m_fold_append …. |
---|
21 | |
---|
22 | lemma produce_step_trace : |
---|
23 | ∀p : prog_params. |
---|
24 | ∀st : state_pc p. |
---|
25 | ∀curr_id,curr_fn. |
---|
26 | ∀s : joint_seq p (globals … p). |
---|
27 | ∀dst : code_point p. |
---|
28 | ∀st' : state p. |
---|
29 | fetch_internal_function … (ev_genv … p) (pc_block (pc … st)) = |
---|
30 | return 〈curr_id, curr_fn〉 → |
---|
31 | let src ≝ point_of_pc p (pc … st) in |
---|
32 | step_in_code … (joint_if_code … curr_fn) src s dst → |
---|
33 | eval_seq_no_pc p (globals … p) (ev_genv … p) curr_id s st = return st' → |
---|
34 | as_execute (joint_abstract_status p) st |
---|
35 | (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ∧ |
---|
36 | as_classifier (joint_abstract_status p) st cl_other. |
---|
37 | #p #st#curr_id #curr_fn #s #dst #st' #EQfetch * #nxt * #EQstmt_at #EQdst |
---|
38 | #EQeval whd in ⊢ (?%%); whd in ⊢ (?(??%?)(??%?)); |
---|
39 | whd in match eval_statement_no_pc; |
---|
40 | whd in match fetch_statement; normalize nodelta >EQfetch >m_return_bind |
---|
41 | >m_return_bind >EQstmt_at >m_return_bind normalize nodelta |
---|
42 | % [2: % ] |
---|
43 | whd in ⊢ (??%?); normalize nodelta >EQeval whd in ⊢ (??%%); |
---|
44 | @eq_f whd in ⊢ (??%?); @eq_f2 [2: %] |
---|
45 | whd in match succ_pc; normalize nodelta @eq_f @EQdst |
---|
46 | qed. |
---|
47 | |
---|
48 | let rec produce_trace_any_any_free_aux |
---|
49 | (p : prog_params) |
---|
50 | (st : state_pc p) |
---|
51 | curr_id curr_fn |
---|
52 | (b : list (joint_seq p (globals … p))) on b : |
---|
53 | ∀l : list (code_point p). |
---|
54 | ∀dst : code_point p. |
---|
55 | ∀st' : state p. |
---|
56 | fetch_internal_function … (ev_genv … p) (pc_block (pc … st)) = |
---|
57 | return 〈curr_id, curr_fn〉 → |
---|
58 | let src ≝ point_of_pc p (pc … st) in |
---|
59 | seq_list_in_code … (joint_if_code … curr_fn) src b l dst → |
---|
60 | repeat_eval_seq_no_pc … p curr_id b st = return st' → |
---|
61 | Σtaaf : trace_any_any_free (joint_abstract_status p) st |
---|
62 | (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). |
---|
63 | (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝ |
---|
64 | match b |
---|
65 | return λb.∀l,dst.?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf)) |
---|
66 | with |
---|
67 | [ nil ⇒ |
---|
68 | λl,dst,st',fd_prf,in_code,EQ1. |
---|
69 | «taaf_base (joint_abstract_status p) st |
---|
70 | ⌈trace_any_any_free ??? ↦ ?⌉,?» |
---|
71 | | cons hd tl ⇒ |
---|
72 | λl. |
---|
73 | match l return λx.∀dst,st'.?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with |
---|
74 | [ nil ⇒ λdst,st',fd_prf,in_code.⊥ |
---|
75 | | cons _ rest ⇒ λdst. |
---|
76 | let mid ≝ match rest with [ nil ⇒ dst | cons mid _ ⇒ mid ] in |
---|
77 | λst',fd_prf,in_code,EQ1. |
---|
78 | let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in |
---|
79 | match eval_seq_no_pc … (ev_genv … p) curr_id hd st |
---|
80 | return λx.eval_seq_no_pc … (ev_genv … p) curr_id hd st = x → |
---|
81 | Σtaaf : trace_any_any_free (joint_abstract_status p) st |
---|
82 | (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). |
---|
83 | (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with |
---|
84 | [ OK st_mid ⇒ λEQ2. |
---|
85 | let tr_tl ≝ produce_trace_any_any_free_aux ? |
---|
86 | (mk_state_pc ? st_mid mid_pc (last_pop … st)) |
---|
87 | curr_id curr_fn tl rest dst ???? in |
---|
88 | «taaf_cons … tr_tl ?,?» |
---|
89 | | _ ⇒ λEQ2.⊥ |
---|
90 | ] (refl …) |
---|
91 | ] |
---|
92 | ]. |
---|
93 | @hide_prf |
---|
94 | [1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ] |
---|
95 | whd in EQ1 : (??%%); |
---|
96 | cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * #ABS destruct ] * #_ #EQ destruct |
---|
97 | >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta * |
---|
98 | | cases in_code #a * #b ** #ABS destruct |
---|
99 | |11: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1) |
---|
100 | |4: cases tr_tl -tr_tl #tr_tl * #_ #H |
---|
101 | @if_elim [2: #_ % ] #G lapply (H G) -H -G |
---|
102 | cases tl in in_code; [ #_ * ] |
---|
103 | #hd' #tl' * #mid' * #rest' ** #EQ * #nxt * #EQstmt_at #EQ_nxt |
---|
104 | * #mid'' * #rest'' ** #EQ' * #nxt' * #EQstmt_at' #EQnxt' |
---|
105 | normalize nodelta -mid_pc destruct |
---|
106 | #_ #_ % whd in ⊢ (%→?); |
---|
107 | whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??); |
---|
108 | >fetch_statement_eq [2: whd in match point_of_pc; |
---|
109 | normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:] |
---|
110 | normalize nodelta * #ABS @ABS % |
---|
111 | |7: % [2: #_ %] #_ @taaf_cons_non_empty |
---|
112 | ] |
---|
113 | change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1; |
---|
114 | >EQ2 in EQ1; >m_return_bind |
---|
115 | cases in_code -in_code #mid' * #rest' ** #EQ1 #step_in cases (step_in) |
---|
116 | #nxt * #EQ_stmt_at #EQ_mid' #rest_in_code |
---|
117 | normalize nodelta |
---|
118 | #EQ3 destruct skip (mid_pc) |
---|
119 | try assumption |
---|
120 | [ whd whd in ⊢ (??%?); |
---|
121 | >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta % |
---|
122 | |*: |
---|
123 | cases tl in rest_in_code; |
---|
124 | [1,3: * #EQ4 #EQ5 destruct normalize nodelta |
---|
125 | |*: #hd' #tl' * #mid'' * #rest'' ** #EQ4 #step_in' #rest_in_code' |
---|
126 | destruct normalize nodelta |
---|
127 | ] |
---|
128 | [1,3: @(proj1 … (produce_step_trace … fd_prf … EQ2)) assumption |
---|
129 | |2: %[%] @point_of_pc_of_point |
---|
130 | |4: >point_of_pc_of_point %[| %[| %{rest_in_code'} %{step_in'} %]] |
---|
131 | ] |
---|
132 | ] |
---|
133 | qed. |
---|
134 | |
---|
135 | definition produce_trace_any_any_free : |
---|
136 | ∀p : prog_params. |
---|
137 | ∀st : state_pc p. |
---|
138 | ∀curr_id,curr_fn. |
---|
139 | ∀b : list (joint_seq p (globals … p)). |
---|
140 | ∀l : list (code_point p). |
---|
141 | ∀dst : code_point p. |
---|
142 | ∀st' : state p. |
---|
143 | fetch_internal_function … (ev_genv … p) (pc_block (pc … st)) = |
---|
144 | return 〈curr_id, curr_fn〉 → |
---|
145 | let src ≝ point_of_pc p (pc … st) in |
---|
146 | seq_list_in_code … (joint_if_code … curr_fn) src b l dst → |
---|
147 | repeat_eval_seq_no_pc … p curr_id b st = return st' → |
---|
148 | Σtaaf :trace_any_any_free (joint_abstract_status p) st |
---|
149 | (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). |
---|
150 | (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝ |
---|
151 | λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3. |
---|
152 | produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3. |
---|
153 | |
---|
154 | (* when a seq_list is coerced to a step_block *) |
---|
155 | definition produce_trace_any_any_free_coerced : |
---|
156 | ∀p : prog_params. |
---|
157 | ∀st : state_pc p. |
---|
158 | ∀curr_id,curr_fn. |
---|
159 | ∀b : list (joint_seq p (globals … p)). |
---|
160 | ∀l : list (code_point p). |
---|
161 | ∀dst : code_point p. |
---|
162 | ∀st' : state p. |
---|
163 | fetch_internal_function … (ev_genv … p) (pc_block (pc … st)) = |
---|
164 | return 〈curr_id, curr_fn〉 → |
---|
165 | let src ≝ point_of_pc p (pc … st) in |
---|
166 | src ~❨b, l❩~> dst in joint_if_code … curr_fn → |
---|
167 | repeat_eval_seq_no_pc … p curr_id b st = return st' → |
---|
168 | trace_any_any_free (joint_abstract_status p) st |
---|
169 | (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝ |
---|
170 | λp,st,curr_id,curr_fn,b.?. |
---|
171 | #l #dst #st' #fd_prf #prf |
---|
172 | lapply (coerced_step_list_in_code … prf) |
---|
173 | inversion b normalize nodelta |
---|
174 | [ #_ #in_code whd in ⊢ (??%%→?); #EQ destruct |
---|
175 | cases (produce_step_trace … fd_prf … in_code (refl …)) |
---|
176 | #H #G |
---|
177 | %2{(taa_base …)} assumption |
---|
178 | | #hd #tl #_ #EQ <EQ -hd -tl #H1 #H2 @(produce_trace_any_any_free …) assumption |
---|
179 | ] |
---|
180 | qed. |
---|