source: src/joint/semantics_blocks.ma @ 2217

Last change on this file since 2217 was 2186, checked in by tranquil, 8 years ago

updated joint semantics

File size: 6.8 KB
Line 
1include "joint/blocks.ma".
2include "joint/Traces.ma".
3
4(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
5  match b with
6  [ nil ⇒ [ ]
7  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
8  ].*)
9
10lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
11  ∀fn,pt,s.
12  fetch_function … ge ptr = OK … fn →
13  point_of_pointer ? p … ptr = OK … pt →
14  stmt_at … (joint_if_code … fn) pt = Some ? s →
15  fetch_statement ? p … ge ptr = OK … s.
16#p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
17whd in match fetch_statement; normalize nodelta >EQ2 >m_return_bind
18>EQ1 >m_return_bind >EQ3 %
19qed.
20
21include alias "basics/logic.ma".
22lemma io_evaluate_bind : ∀O,I,X,Y,env.
23∀m : IO O I X.∀f : X → IO O I Y.
24io_evaluate O I Y env (! x ← m ; f x) =
25! x ← io_evaluate O I X env m ;
26io_evaluate O I Y env (f x).
27#O #I #X #Y #env #m elim m
28[ #o #g #IH #f whd in match (! x ← Interact ????? ; ?);
29  change with (! y ← ? ; ?) in ⊢ (??%(????%?));
30  >m_bind_bind @m_bind_ext_eq #i @IH
31| #x #f %
32| #e #f %
33]
34qed.
35
36lemma fetch_function_from_block_eq :
37  ∀p,g,ge.
38  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
39  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
40#p #g #ge #ptr1 #ptr2 #EQ
41whd in match fetch_function; normalize nodelta >EQ
42@m_bind_ext_eq // qed.
43
44let rec repeat_eval_seq_no_pc
45  (p : evaluation_params) env
46  (l : list (joint_seq p (globals p))) on l :
47  state p → res (state p) ≝
48  λst.match l with
49  [ nil ⇒ return st
50  | cons hd tl ⇒
51    ! st' ← io_evaluate … (env st) (eval_seq_no_pc (globals p) p (ev_genv p) st hd) ;
52    repeat_eval_seq_no_pc p env tl st'
53  ].
54
55lemma err_to_io_evaluate : ∀O,I,X,env,m.
56  io_evaluate O I X env (err_to_io … m) = m.
57#O#I#X#env * // qed.
58
59definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
60
61definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝
62  λp,g,s.match s with
63  [ COST_LABEL _ ⇒ false
64  | CALL_ID _ _ _ ⇒ false
65  | extension_call _ ⇒ false
66  | _ ⇒ true
67  ].
68
69lemma no_call_nor_label_proceed : ∀p : evaluation_params.
70∀st : state p. ∀s.
71no_call_nor_label p (globals p) s →
72eval_seq_pc (globals p) p (ev_genv p) st s = return Proceed ???.
73#p #st * // [ #f #args #dest | #c ] *
74qed.
75
76lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
77no_call_nor_label p (globals p) s →
78step_classifier … s = cl_other.
79#p * // [ #f #args #dest | #c ] *
80qed.
81
82lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
83no_call_nor_label p (globals p) s →
84cost_label_of_stmt … (sequential … s nxt) = None ?.
85#p * // #lbl#next *
86qed.
87
88let rec produce_trace_any_any
89  (p : evaluation_params)
90  (st : state_pc p) fd
91  (src : code_point p)
92  (b : list (joint_seq p (globals p))) on b :
93  ∀l : list (code_point p).
94  ∀dst : code_point p.
95  ∀st' : state p.
96  fetch_function p ? (ev_genv p) (pc … st) = return fd →
97  point_of_pointer p p (pc … st) = return src →
98  if list_not_empty ? b then
99    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
100  else
101    True →
102  src ~❨b, l❩~> dst in joint_if_code … fd →
103  All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
104  repeat_eval_seq_no_pc p (io_env p) b st = return st' →
105  trace_any_any (joint_abstract_status p) st
106    (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝
107  match b
108  return λx.?→?→?→?→?→?→?→?→?→?
109  with
110  [ nil ⇒
111    λl,dst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
112    (taa_base (joint_abstract_status p) st)
113      ⌈trace_any_any (joint_abstract_status p) st st ↦
114       trace_any_any (joint_abstract_status p) st
115        (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉
116  | cons hd tl ⇒
117    λl.
118    match l return λx.?→?→?→?→?→?→?→?→? with
119    [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥
120    | cons mid rest ⇒
121      λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
122      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd)
123      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ?
124      with
125      [ OK st_mid ⇒ λEQ2.
126        taa_step (joint_abstract_status p) st ?
127          (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ???
128          (produce_trace_any_any ?
129            (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid))
130            fd mid tl rest dst ???????)
131      | Error _ ⇒ λEQ2.⊥
132      ] (refl …)
133    ]
134  ].
135  [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ
136    cases st in src_prf EQ1; -st #st #pc
137    #src_prf normalize in ⊢ (%→?); #EQ1 destruct
138    >(pointer_of_point_of_pointer … src_prf) %
139  | elim in_code
140  |12: lapply EQ1 whd in ⊢ (??%?→?);
141    >EQ2 normalize #ABS destruct(ABS)
142  |*:
143    elim in_code
144    * #nxt * #EQ3 #EQ4 #Hrest
145    elim all_other
146    #hd_other #tl_other
147    [ whd whd in match eval_state; normalize nodelta
148      >(fetch_statement_eq … fd_prf src_prf EQ3) >m_return_bind
149      whd in match eval_statement; normalize nodelta
150      whd in match eval_step; normalize nodelta
151      >m_bind_bind
152      >(no_call_nor_label_proceed … hd_other) >m_return_bind
153      >m_bind_bind
154      >io_evaluate_bind >EQ2 >m_return_bind
155      >m_return_bind
156      whd in match succ_pc; normalize nodelta
157      >m_bind_bind >src_prf >m_return_bind >m_return_bind
158      whd in match eval_step_flow; normalize nodelta
159      whd in ⊢ (??%%); >EQ4
160      >EQ2 %
161    | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)}
162      cases all_other #hd_other #_
163      whd in match stmt_classifier; normalize nodelta
164      @no_call_nor_label_other assumption
165    | %* #H @H -H whd in ⊢ (??%?);
166      cases tl in Hrest tl_other;
167      [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') *
168        lapply dst_prf
169        whd in match (as_pc_of ??);
170        whd in match fetch_statement; normalize nodelta
171        whd in match point_of_pointer; normalize nodelta
172        >point_of_offset_of_point
173        >m_return_bind
174        >fetch_function_from_block_eq
175        [ >fd_prf
176          >m_return_bind
177          cases (stmt_at ????)
178          [ #_ %
179          | #stmt #H @H
180          ]
181        | %
182        |
183        ]
184      | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6
185        #_ * #hd_other' #_
186        >fetch_statement_eq try assumption
187        [ @no_call_nor_label_uncosted assumption
188        | whd in match (as_pc_of ??);
189          whd in ⊢ (??%?);
190          >point_of_offset_of_point %
191        ]
192      ]
193    | change with (! x ← ?;?) in EQ1 : (??%?);
194      >EQ2 in EQ1; #H @H
195    | assumption
196    | assumption
197    | cases (list_not_empty ??) [ assumption | % ]
198    | @point_of_pointer_of_point
199    | <fd_prf @fetch_function_from_block_eq %
200    ]
201  ]
202qed.
Note: See TracBrowser for help on using the repository browser.