source: src/joint/semantics_blocks.ma @ 2529

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

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File size: 4.0 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 : evaluation_params.λcurr_id,curr_fn.
13  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
14
15definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
16
17let rec produce_trace_any_any
18  (p : evaluation_params)
19  (st : state_pc p)
20  curr_id curr_fn
21  (b : list (joint_seq p (globals p))) on b :
22  ∀l : list (code_point p).
23  ∀dst : code_point p.
24  ∀st' : state p.
25  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
26    return 〈curr_id, curr_fn〉 →
27  let src ≝ point_of_pc p (pc … st) in
28  if list_not_empty ? b then
29    ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
30  else
31    True →
32  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
33  All ? (λx.And (no_call … x) (no_cost_label … x)) b →
34  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
35  trace_any_any (joint_abstract_status p) st
36    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
37  return λb.∀l,dst.?→?→?→?→?→?→?
38  with
39  [ nil ⇒
40    λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
41    (taa_base (joint_abstract_status p) st)
42    ⌈trace_any_any ??? ↦ ?⌉
43  | cons hd tl ⇒
44    λl.
45    match l return λx.∀dst,st'.?→?→?→?→?→? with
46    [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
47    | cons mid rest ⇒
48      λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
49      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
50      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
51      return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
52      trace_any_any (joint_abstract_status p) st
53        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with
54      [ Value st_mid ⇒ λEQ2.
55        let tr_tl ≝ produce_trace_any_any ?
56            (mk_state_pc ? st_mid mid_pc)
57            curr_id curr_fn tl rest dst ?????? in
58        taa_step … tr_tl
59      | _ ⇒ λEQ2.⊥
60      ] (refl …)
61    ]
62  ].
63[ whd in EQ1 : (??%%);
64  cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct
65  >pc_of_point_of_pc cases st //
66| @in_code
67|3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
68]
69change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
70>EQ2 in EQ1; >m_return_bind
71cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
72cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
73#EQ1
74try assumption
75[ whd whd in match eval_state; normalize nodelta
76  >(fetch_statement_eq … fd_prf EQ_stmt_at)
77  >m_return_bind
78  whd in match eval_statement_no_pc; normalize nodelta
79  >EQ2 >m_return_bind
80  whd in match eval_statement_advance; normalize nodelta
81  >(no_call_advance … hd_no_call)
82  whd in match next; normalize nodelta
83  whd in match succ_pc; normalize nodelta
84  >EQ_mid %
85| whd whd in ⊢ (??%?);
86  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta
87  @(no_call_other … hd_no_call)
88| whd in ⊢ (?%);
89  whd in match as_label; normalize nodelta
90  %* #H @H -H whd in ⊢ (??%?);
91  whd in match (as_pc_of ??);
92  inversion (fetch_statement ????) normalize nodelta
93  [2: // ]
94  ** #i' #f' #stmt' #EQ
95  elim (fetch_statement_inv … EQ)
96  >fd_prf
97  whd in ⊢ (??%?→?); #EQ destruct(EQ)
98  whd in ⊢ (%→?);
99  whd in match (point_of_pc ??); >point_of_offset_of_point
100  #EQ'
101  cases tl in tl_other rest_in_code;
102  [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ)
103    >EQ' in dst_prf; >m_return_bind #H @H
104  | #hd' #tl' ** #_ #hd_no_cost' #_
105    cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_
106    >EQ_stmt_at' in EQ'; #EQ' destruct(EQ')
107    @(no_label_uncosted … hd_no_cost')
108  ]
109| >dst_prf cases (list_not_empty ??) %
110| normalize nodelta >point_of_pc_of_point assumption
111]
112qed.
Note: See TracBrowser for help on using the repository browser.