source: src/joint/semantics_blocks.ma @ 2817

Last change on this file since 2817 was 2817, checked in by sacerdot, 7 years ago

Repaired after Paolo's commit.

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