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 p g.∀ptr : cpointer. ∀fn,pt,s. fetch_function … ge ptr = OK … fn → point_of_pointer ? p … ptr = pt → stmt_at … (joint_if_code … fn) pt = Some ? s → fetch_statement ? p … ge ptr = OK … 〈fn, s〉. #p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3 whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind >EQ2 >EQ3 >m_return_bind % 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 curr_fn (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 p (globals p) (ev_genv p) curr_fn st hd) ; repeat_eval_seq_no_pc p env curr_fn 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 p (globals 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. definition code_compact : ∀p:sem_params.∀g.codeT p g → Prop ≝ λp,g,c.code_closed … c∧ ∀pt,ptr.code_has_point … c pt → ∃ptr'.pointer_of_point p p ptr pt = return ptr'. definition pointer_of_point_step_in_code : ∀p:sem_params.∀g. ∀c,pc,step,dst. code_compact p g c → step_in_code … c (point_of_pointer p p pc) step dst → Σpc'.pointer_of_point p p pc dst = return pc' ≝ λp,g,c,pc,step,dst,c_compact,step_in. match pointer_of_point p p pc dst return λx.pointer_of_point p p pc dst = x → ? with [ OK pc' ⇒ mk_Sig ?? pc' | Error e ⇒ λEQ.⊥ ] (refl …). cases step_in #nxt * #EQ1 #EQ2 cases c_compact -c_compact #c_closed #c_compact elim (c_compact dst pc ?) [ >EQ #pc' normalize #ABS destruct(ABS) | elim (c_closed … EQ1) #_ whd in ⊢ (%→?); >EQ2 #H @H ] qed. let rec pointer_of_point_in_code p g c pc dst b on b : ∀l.code_compact p g c → point_of_pointer p p pc ~❨b,l❩~> dst in c → Σpc'.pointer_of_point p p pc dst = return pc' ≝ match b return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr' with [ nil ⇒ λl,c_compact,in_code. match pointer_of_point p p pc dst return λx.pointer_of_point p p pc dst = x → ? with [ OK ptr' ⇒ mk_Sig ?? ptr' | Error e ⇒ λEQ.⊥ ] (refl …) | cons hd tl ⇒ λl.match l return λl.? → ? → Σptr'.? with [ nil ⇒ λc_compact,in_code.⊥ | cons mid rest ⇒ λc_compact,in_code. let mid_pc ≝ pointer_of_point_step_in_code … c pc hd mid c_compact ? in pi1 … (pointer_of_point_in_code ?? c mid_pc dst tl rest c_compact ?) ] ]. [ cases l in in_code; [2: #mid #rest * ] whd in ⊢ (%→?); #EQ' pointer_of_point_of_pointer [2: %] normalize #ABS destruct(ABS) | cases (pointer_of_point_in_code ?????????) #ptr' >pointer_of_point_uses_block [ #H @H |*:] cases mid_pc -mid_pc #mid_pc @pointer_of_point_block | elim in_code | cases mid_pc -mid_pc #mid_pc #EQ >(point_of_pointer_of_point … EQ) cases in_code #_ #H @H | cases in_code #H #_ @H ] qed. let rec produce_trace_any_any (p : evaluation_params) (st : state_pc p) fd (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 → ∀prf1 : code_compact p (globals p) (joint_if_code … fd). let src ≝ point_of_pointer p p (pc … st) in if list_not_empty ? b then ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ? else True → ∀prf2 : 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) fd b st = return st' → trace_any_any (joint_abstract_status p) st (mk_state_pc ? st' (pointer_of_point_in_code … prf1 prf2)) ≝ match b return λx.∀l,dst.?→?→?→?→?→?→?→? with [ nil ⇒ λl,dst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1. (taa_base (joint_abstract_status p) st) ⌈trace_any_any (joint_abstract_status p) st st ↦ ?⌉ | cons hd tl ⇒ λl. match l return λx.?→?→?→?→?→?→?→?→? with [ nil ⇒ λdst_pc,st',fd_prf,src_prf,dst_prf,in_code.⊥ | cons mid rest ⇒ λdst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1. let mid_pc ≝ pointer_of_point_step_in_code p ? (joint_if_code … fd) (pc … st) hd mid c_compact ? in match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) = x → ? with [ OK st_mid ⇒ λEQ2. let tr_tl ≝ produce_trace_any_any ? (mk_state_pc ? st_mid mid_pc) fd tl rest dst ??????? in (* works fast only in interactive mode: taa_step … tr_tl *) ? | Error _ ⇒ λEQ2.⊥ ] (refl …) ] ].[3: @(taa_step … tr_tl) |*:] try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc) try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code) try (cases all_other #hd_other #tl_other) [ whd whd in match eval_state; normalize nodelta >(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at) >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 >EQ_mid >EQ_mid_pc >m_return_bind % | whd %{fd} %{(sequential … hd nxt)} %{(no_call_nor_label_other … hd_other)} @(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at) |4: cases (pointer_of_point_in_code ?????????) #dst_pc cases l in in_code; [2: #mid #rest * ] whd in ⊢ (%→?); #EQ' pointer_of_point_of_pointer [2: %] lapply EQ1 -EQ1 normalize in ⊢ (%→%→?); #EQ1 #EQ'' destruct cases st // |5: >fetch_function_from_block_eq [ @fd_prf |*: ] @(pointer_of_point_block … EQ_mid_pc) |6: cases tl [ % ] #hd' #tl' @dst_prf |7: assumption |8,9: lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize nodelta [ #H @H | normalize #ABS destruct(ABS) ] |3: %* #H @H -H lapply tl_other lapply rest_in_code (* BUG? cases tl causes "Ill formed pattern" *) @(match tl with [ nil ⇒ ? | cons hd' tl' ⇒ ?]) cases rest [2,4: #mid' #rest'] [1,4: * ] [2: whd in ⊢ (%→?); #EQ' destruct(EQ') * | ** #nxt' * #at_mid #_ #_ * #mid_other #_ ] whd in ⊢ (??%?); [ lapply dst_prf ] whd in match as_label; whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta >(point_of_pointer_of_point … EQ_mid_pc) >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc)) >fd_prf >m_return_bind [ cases (stmt_at ????) [ #_ % ] #stmt #H @H | >at_mid >m_return_bind normalize nodelta @(no_call_nor_label_uncosted … mid_other) ] ] qed.