include "joint/blocks.ma". include "joint/Traces.ma". (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ match b with [ nil ⇒ [ ] | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl ].*) lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer. ∀fn,pt,s. fetch_function … ge ptr = OK … fn → point_of_pointer ? p … ptr = OK … pt → stmt_at … (joint_if_code … fn) pt = Some ? s → fetch_statement ? p … ge ptr = OK … s. #p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3 whd in match fetch_statement; normalize nodelta >EQ2 >m_return_bind >EQ1 >m_return_bind >EQ3 % qed. include alias "basics/logic.ma". lemma io_evaluate_bind : ∀O,I,X,Y,env. ∀m : IO O I X.∀f : X → IO O I Y. io_evaluate O I Y env (! x ← m ; f x) = ! x ← io_evaluate O I X env m ; io_evaluate O I Y env (f x). #O #I #X #Y #env #m elim m [ #o #g #IH #f whd in match (! x ← Interact ????? ; ?); change with (! y ← ? ; ?) in ⊢ (??%(????%?)); >m_bind_bind @m_bind_ext_eq #i @IH | #x #f % | #e #f % ] qed. lemma fetch_function_from_block_eq : ∀p,g,ge. ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 → fetch_function p g ge ptr1 = fetch_function p g ge ptr2. #p #g #ge #ptr1 #ptr2 #EQ whd in match fetch_function; normalize nodelta >EQ @m_bind_ext_eq // qed. let rec repeat_eval_seq_no_pc (p : evaluation_params) env (l : list (joint_seq p (globals p))) on l : state p → res (state p) ≝ λst.match l with [ nil ⇒ return st | cons hd tl ⇒ ! st' ← io_evaluate … (env st) (eval_seq_no_pc (globals p) p (ev_genv p) st hd) ; repeat_eval_seq_no_pc p env tl st' ]. lemma err_to_io_evaluate : ∀O,I,X,env,m. io_evaluate O I X env (err_to_io … m) = m. #O#I#X#env * // qed. definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ]. definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝ λp,g,s.match s with [ COST_LABEL _ ⇒ false | CALL_ID _ _ _ ⇒ false | extension_call _ ⇒ false | _ ⇒ true ]. lemma no_call_nor_label_proceed : ∀p : evaluation_params. ∀st : state p. ∀s. no_call_nor_label p (globals p) s → eval_seq_pc (globals p) p (ev_genv p) st s = return Proceed ???. #p #st * // [ #f #args #dest | #c ] * qed. lemma no_call_nor_label_other : ∀p : evaluation_params.∀s. no_call_nor_label p (globals p) s → step_classifier … s = cl_other. #p * // [ #f #args #dest | #c ] * qed. lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt. no_call_nor_label p (globals p) s → cost_label_of_stmt … (sequential … s nxt) = None ?. #p * // #lbl#next * qed. let rec produce_trace_any_any (p : evaluation_params) (st : state_pc p) fd (src : code_point p) (b : list (joint_seq p (globals p))) on b : ∀l : list (code_point p). ∀dst : code_point p. ∀st' : state p. fetch_function p ? (ev_genv p) (pc … st) = return fd → point_of_pointer p p (pc … st) = return src → if list_not_empty ? b then ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ? else True → src ~❨b, l❩~> dst in joint_if_code … fd → All ? (λx.bool_to_Prop (no_call_nor_label … x)) b → repeat_eval_seq_no_pc p (io_env p) b st = return st' → trace_any_any (joint_abstract_status p) st (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝ match b return λx.?→?→?→?→?→?→?→?→?→? with [ nil ⇒ λl,dst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1. (taa_base (joint_abstract_status p) st) ⌈trace_any_any (joint_abstract_status p) st st ↦ trace_any_any (joint_abstract_status p) st (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉ | cons hd tl ⇒ λl. match l return λx.?→?→?→?→?→?→?→?→? with [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥ | cons mid rest ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1. match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ? with [ OK st_mid ⇒ λEQ2. taa_step (joint_abstract_status p) st ? (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ??? (produce_trace_any_any ? (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid)) fd mid tl rest dst ???????) | Error _ ⇒ λEQ2.⊥ ] (refl …) ] ]. [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ cases st in src_prf EQ1; -st #st #pc #src_prf normalize in ⊢ (%→?); #EQ1 destruct >(pointer_of_point_of_pointer … src_prf) % | elim in_code |12: lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize #ABS destruct(ABS) |*: elim in_code * #nxt * #EQ3 #EQ4 #Hrest elim all_other #hd_other #tl_other [ whd whd in match eval_state; normalize nodelta >(fetch_statement_eq … fd_prf src_prf EQ3) >m_return_bind whd in match eval_statement; normalize nodelta whd in match eval_step; normalize nodelta >m_bind_bind >(no_call_nor_label_proceed … hd_other) >m_return_bind >m_bind_bind >io_evaluate_bind >EQ2 >m_return_bind >m_return_bind whd in match succ_pc; normalize nodelta >m_bind_bind >src_prf >m_return_bind >m_return_bind whd in match eval_step_flow; normalize nodelta whd in ⊢ (??%%); >EQ4 >EQ2 % | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)} cases all_other #hd_other #_ whd in match stmt_classifier; normalize nodelta @no_call_nor_label_other assumption | %* #H @H -H whd in ⊢ (??%?); cases tl in Hrest tl_other; [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') * lapply dst_prf whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta whd in match point_of_pointer; normalize nodelta >point_of_offset_of_point >m_return_bind >fetch_function_from_block_eq [ >fd_prf >m_return_bind cases (stmt_at ????) [ #_ % | #stmt #H @H ] | % | ] | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6 #_ * #hd_other' #_ >fetch_statement_eq try assumption [ @no_call_nor_label_uncosted assumption | whd in match (as_pc_of ??); whd in ⊢ (??%?); >point_of_offset_of_point % ] ] | change with (! x ← ?;?) in EQ1 : (??%?); >EQ2 in EQ1; #H @H | assumption | assumption | cases (list_not_empty ??) [ assumption | % ] | @point_of_pointer_of_point |