source: src/joint/semantics_blocks.ma @ 2869

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

some reorganization of definitions, and a new taaf_append_taaf

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