source: src/joint/semantics_blocks.ma @ 2967

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

fixed semantics_blocks

File size: 7.2 KB
Line 
1include "joint/blocks.ma".
2include "joint/Traces.ma".
3include "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
11definition 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
15lemma 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
22lemma 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 ⊢ (?(??%?)(??%?));
39whd in match eval_statement_no_pc;
40whd in match fetch_statement; normalize nodelta >EQfetch >m_return_bind
41>m_return_bind >EQstmt_at >m_return_bind normalize nodelta
42% [2: % ]
43whd in ⊢ (??%?); normalize nodelta >EQeval whd in ⊢ (??%%);
44@eq_f whd in ⊢ (??%?); @eq_f2 [2: %]
45whd in match succ_pc; normalize nodelta @eq_f @EQdst
46qed.
47
48let 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]
113change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
114>EQ2 in EQ1; >m_return_bind
115cases in_code -in_code #mid' * #rest' ** #EQ1 #step_in cases (step_in)
116#nxt * #EQ_stmt_at #EQ_mid' #rest_in_code
117normalize nodelta
118#EQ3 destruct skip (mid_pc)
119try 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]
133qed.
134
135definition 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 *)
155definition 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
172lapply (coerced_step_list_in_code … prf)
173inversion 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]
180qed.
Note: See TracBrowser for help on using the repository browser.