Changeset 3396 for LTS/Language.ma


Ignore:
Timestamp:
Nov 15, 2013, 2:51:50 PM (6 years ago)
Author:
piccolo
Message:

correctness proof in developping

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3394 r3396  
    1717include "basics/lists/list.ma".
    1818include "../src/utilities/option.ma".
     19include "basics/jmeq.ma".
    1920
    2021record instr_params : Type[1] ≝
     
    8485lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) →
    8586(i1 ≠ i2 → P false) → P (eq_instructions p i1 i2).
     87#P #p #i1 elim i1
     88[ * normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
     89  (* destruct(EQ) gives no choice for ID(instructions_discr) *) cases daemon ]
    8690cases daemon (*TODO*)
    8791qed.
     
    175179    store ? st' = mem → code … st' = f_body … env_it →
    176180     cont … st' =
    177        〈(ret_act (match r_lb with [Some lb ⇒ Some ? (inl ?? lb)
    178                                   | None ⇒ None ?])),cd〉 :: (cont … st) → 
     181       〈(ret_act r_lb),cd〉 :: (cont … st) → 
    179182    io_info … st = false →  (io_info … st') = false →
    180     execute_l … (call_act f (inl ?? (f_lab ?? env_it))) st st'
     183    execute_l … (call_act f (f_lab ?? env_it)) st st'
    181184| ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t →
    182185   cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' →
     
    354357λx.〈a_return_cost_label x,S x〉.
    355358
     359record call_post_info (p : instr_params) : Type[0] ≝
     360{ gen_labels : list CostLabel
     361; t_code : Instructions p
     362; fresh : ℕ
     363; lab_map : associative_list DEQCostLabel CostLabel
     364; lab_to_keep : list CostLabel
     365}.
     366
    356367let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i :
    357 ((list CostLabel) × (Instructions p)) × (ℕ × (associative_list DEQCostLabel CostLabel)) ≝
     368list CostLabel → call_post_info p ≝
     369λabs.
    358370match i with
    359 [ EMPTY ⇒ 〈nil ?,EMPTY p,n,nil ?〉
    360 | RETURN x ⇒ 〈nil ?,RETURN … x,n,nil ?〉
     371[ EMPTY ⇒ mk_call_post_info ? abs (EMPTY …) n (nil ?) (nil ?)
     372| RETURN x ⇒ mk_call_post_info ? abs (RETURN … x) n (nil ?) (nil ?)
    361373| SEQ x lab instr ⇒
    362    let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … instr n in
     374   let ih ≝ call_post_trans … instr n abs in
    363375   match lab with
    364    [ None ⇒ 〈l1,SEQ … x (None ?) instr1,n1,m1〉
    365    | Some lbl ⇒ 〈nil CostLabel,SEQ … x (Some ? lbl) instr1, n1, update_list ?? m1 lbl (lbl :: l1) 〉
     376   [ None ⇒ mk_call_post_info ? (gen_labels … ih) (SEQ … x (None ?) (t_code … ih))
     377             (fresh … ih) (lab_map … ih) (lab_to_keep … ih)
     378   | Some lbl ⇒
     379      mk_call_post_info ? (nil ?) (SEQ … x (Some ? lbl) (t_code …  ih)) (fresh … ih)
     380      (〈a_non_functional_label lbl,(a_non_functional_label lbl :: (gen_labels … ih))〉 :: (lab_map … ih))
     381      (lab_to_keep … ih)
    366382   ]
    367383| COND x ltrue i1 lfalse i2 i3 ⇒
    368    let 〈l3,instr3,n3,m3〉 ≝ call_post_trans … i3 n in
    369    let 〈l2,instr2,n2,m2〉 ≝ call_post_trans … i2 n3 in
    370    let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n2 in
    371   〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3,n1,
    372     update_list DEQCostLabel CostLabel
    373       (update_list DEQCostLabel CostLabel (m1 @ m2 @ m3) ltrue (ltrue :: (l1 @ l3)))
    374       lfalse (lfalse :: (l2 @ l3))〉
     384   let ih3 ≝ call_post_trans … i3 n abs in
     385   let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in
     386   let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in
     387   mk_call_post_info ? (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3))
     388    (fresh … ih1) 
     389    (〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉::
     390      〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉::
     391       ((lab_map … ih1) @ (lab_map …  ih2) @ (lab_map … ih3)))
     392    ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3))
    375393| LOOP x ltrue i1 lfalse i2 ⇒
    376    let 〈l2,instr2,n2,m2〉 ≝ call_post_trans … i2 n in
    377    let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n2 in
    378    〈nil ?,LOOP … x ltrue instr1 lfalse instr2,n1,
    379       update_list DEQCostLabel CostLabel
    380          (update_list DEQCostLabel CostLabel (m1 @ m2) ltrue (ltrue :: l1))
    381          lfalse (lfalse :: l2)〉
     394   let ih2 ≝ call_post_trans … i2 n abs in
     395   let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in
     396   mk_call_post_info ? (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1)
     397    (〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉 ::
     398     〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉 ::
     399      ((lab_map … ih1) @ (lab_map … ih2)))
     400    ((lab_to_keep … ih1) @ (lab_to_keep … ih2))
    382401| CALL f act_p r_lb i1 ⇒
    383    let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n in
     402   let ih ≝ call_post_trans … i1 n abs in
    384403   match r_lb with
    385    [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label n1 in
    386             〈(a_return_post l')::l1,CALL … f act_p (Some ? l') instr1,f'',m1〉
    387    | Some lbl ⇒ 〈nil ?,CALL ? f act_p (Some ? lbl) instr1,n1,update_list ?? m1 lbl (lbl :: l1)〉
     404   [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label (fresh … ih) in
     405       mk_call_post_info ? ((a_return_post l')::(gen_labels … ih))
     406         (CALL … f act_p (Some ? l') (t_code … ih))  f'' (lab_map … ih) (lab_to_keep … ih)
     407   | Some lbl ⇒
     408      mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih)
     409       (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih))
     410       (a_return_post lbl :: lab_to_keep … ih)
    388411   ]
    389412| IO lin io lout i1 ⇒
    390     let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n in
    391     〈nil ?,IO ? lin io lout instr1,n1,update_list ?? (update_list ?? m1 lout (lout :: l1)) lin [lin]〉
    392 ].
    393 
     413    let ih ≝ call_post_trans … i1 n abs in
     414    mk_call_post_info ? (nil ?) (IO ? lin io lout (t_code … ih)) (fresh … ih)
     415     (〈a_non_functional_label lout,(a_non_functional_label lout :: (gen_labels … ih))〉 ::
     416      〈a_non_functional_label lin,[a_non_functional_label lin]〉 :: (lab_map … ih)) (lab_to_keep … ih)
     417].
     418
     419
     420let rec call_post_clean (p : instr_params) (i : Instructions p) on i :
     421associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
     422option ((list CostLabel) × (Instructions p)) ≝
     423λm,keep,abs.
     424 match i with
     425[ EMPTY ⇒ Some ? 〈abs,EMPTY …〉
     426| RETURN x ⇒ Some ? 〈abs,RETURN … x〉
     427| SEQ x lab instr ⇒
     428   ! 〈l,i1〉 ← call_post_clean … instr m keep abs;
     429   match lab with
     430   [ None ⇒ return 〈l,SEQ … x (None ?) i1〉
     431   | Some lbl ⇒ if ((get_element … m lbl) == lbl :: l)
     432                then return 〈nil ?,SEQ … x (Some ? lbl) i1〉
     433                else None ?
     434   ]
     435| COND x ltrue i1 lfalse i2 i3 ⇒
     436    ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs;
     437    ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3;
     438    ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3;
     439    if ((get_element … m ltrue) == ltrue :: l1) ∧
     440       ((get_element … m lfalse) == lfalse :: l2)
     441    then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉
     442    else None ?
     443| LOOP x ltrue i1 lfalse i2 ⇒
     444   ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs;
     445   ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?);
     446   if ((get_element … m ltrue) == ltrue :: l1) ∧
     447      ((get_element … m lfalse) == lfalse :: l2)
     448   then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉
     449   else None ?
     450| CALL f act_p r_lb i1 ⇒
     451  ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs;
     452  match r_lb with
     453  [ None ⇒ return 〈l1,CALL … f act_p (None ?) instr1〉
     454  | Some lbl ⇒ if ((a_return_post lbl ∈ keep))
     455               then if ((get_element … m lbl) == lbl :: l1)
     456                    then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉
     457                    else None ?
     458               else return 〈(a_return_post lbl) :: l1,CALL … f act_p (None ?) instr1〉
     459  ]
     460| IO lin io lout i1 ⇒
     461   ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs;
     462   if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin])
     463   then return 〈nil ?,IO … lin io lout instr1〉
     464   else None ?   
     465].
     466
     467let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B)
     468(l2 : list C) (f : A → B → C → A) on l1 : option A≝
     469match l1 with
     470[ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ]
     471| cons x xs ⇒
     472        match l2 with
     473        [ nil ⇒ None ?
     474        | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f);
     475                      return f ih x y
     476        ]
     477].
     478
     479definition is_silent_cost_act_b : ActionLabel → bool ≝
     480λact. match act with
     481 [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false].
     482
     483definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝
     484λc1,c2.
     485match c1 with
     486[ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false]
     487| ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
     488                                                      | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
     489                                                      ]
     490                            | _ ⇒ false
     491                            ]
     492| cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
     493                                                        | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
     494                                                        ]
     495                             | _ ⇒ false
     496                             ]
     497| init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false]
     498].
     499
     500definition ret_costed_abs : list CostLabel → option ReturnPostCostLabel → option CostLabel ≝
     501λkeep,x.
     502 match x with
     503              [ Some lbl ⇒ if (a_return_post lbl) ∈ keep then return (a_return_post lbl)
     504                           else None ?
     505              | None ⇒ None ?
     506              ].
     507
     508definition check_continuations : ∀p : instr_params.
     509∀l1,l2 : list (ActionLabel × (Instructions p)).
     510associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
     511option (Prop × (list CostLabel)) ≝
     512λp,cont1,cont2,m,abs,keep.
     513foldr2 ??? 〈True,abs〉 cont1 cont2
     514 (λx,y,z.
     515   match call_post_clean p (\snd z) m keep (\snd x) with
     516   [ None ⇒ 〈False,nil ?〉
     517   | Some w ⇒
     518      match \fst y with
     519       [ ret_act opt_x ⇒
     520           match ret_costed_abs keep opt_x with
     521           [ Some lbl ⇒ 〈\fst y = \fst z ∧\fst x ∧ \snd w = \snd y ∧
     522                               get_element … m lbl = lbl :: (\fst w),(nil ?)〉
     523           | None ⇒
     524              〈\fst z = ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉
     525           ]
     526       | cost_act opt_x ⇒
     527           match opt_x with
     528           [ None ⇒ 〈\fst y = \fst z ∧ \fst x ∧ \snd w = \snd y,\fst w〉
     529           | Some xx ⇒ 〈\fst y = \fst z ∧\fst x ∧ \snd w = \snd y ∧
     530                               get_element … m xx = xx :: (\fst w),(nil ?)〉]
     531       | _ ⇒ (* dummy *) 〈False,nil ?〉]]).
     532
     533definition state_rel : ∀p.
     534associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
     535relation (state p) ≝ λp,m,l,keep,st1,st2.
     536match check_continuations ? (cont ? st1) (cont … st2) m (nil ?) keep with
     537[ Some x ⇒ let 〈prf1,l'〉 ≝ x in
     538           prf1 ∧ call_post_clean … (code … st2) m keep l' = return 〈l,(code … st1)〉
     539           ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2
     540| None ⇒ False
     541].
     542
     543include "Simulation.ma".
     544
     545let rec len (S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace S st1 st2)
     546on t : ℕ ≝
     547match t with
     548[ t_base s ⇒ O
     549| t_ind s1 s2 s3 l prf lt ⇒ (len … lt) + 1
     550].
     551(*
     552lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3).
     553#n1 #n2 #n3 normalize @leb_elim normalize
     554[ @leb_elim normalize
     555  [ #H1 #H2 @leb_elim normalize
     556    [ @leb_elim normalize // * #H @⊥ @H assumption 
     557    | @leb_elim normalize
     558      [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption
     559      | * #H @⊥ @H assumption
     560      ]
     561    ]
     562  | #H1 #H2 @leb_elim normalize
     563    [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption
     564    | @leb_elim normalize
     565      [ #_ * #H @⊥ @H assumption
     566      | * #H @⊥ @H @(transitive_le … H2)
     567*)
     568let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝
     569match i with
     570[ EMPTY ⇒ O
     571| RETURN x ⇒ O
     572| SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in
     573                    match lab with
     574                    [ None ⇒ n
     575                    | Some l ⇒
     576                        match l with
     577                        [ a_non_functional_label n' ⇒ S (max n n') ]
     578                    ]
     579| COND x ltrue i1 lfalse i2 i3 ⇒
     580  let n1 ≝ compute_max_n … i1 in
     581  let n2 ≝ compute_max_n … i2 in
     582  let n3 ≝ compute_max_n … i3 in
     583  let mx ≝ max (max n1 n2) n3 in
     584  match ltrue with
     585  [ a_non_functional_label lt ⇒
     586    match lfalse with
     587    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
     588| LOOP x ltrue i1 lfalse i2 ⇒
     589   let n1 ≝ compute_max_n … i1 in
     590   let n2 ≝ compute_max_n … i2 in
     591   let mx ≝ max n1 n2 in
     592   match ltrue with
     593  [ a_non_functional_label lt ⇒
     594    match lfalse with
     595    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
     596| CALL f act_p r_lb i1 ⇒
     597   let n ≝ compute_max_n … i1 in
     598   match r_lb with
     599   [ None ⇒ n
     600   | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ]
     601   ]
     602| IO lin io lout i1 ⇒
     603  let n ≝ compute_max_n … i1 in
     604  match lin with
     605  [a_non_functional_label l1 ⇒
     606    match lout with
     607    [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ]
     608].
     609
     610
     611lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
     612n ≥ compute_max_n … i1 →
     613∀info,l.call_post_trans p i1 n l = info →
     614call_post_clean … (t_code … info) (lab_map … info) (lab_to_keep … info) l
     615 = return 〈gen_labels … info,i1〉.
     616cases daemon (*TODO*)
     617qed.
     618
     619definition trans_prog : ∀p,p'.Program p p' →
     620(Program p p') × (associative_list DEQCostLabel CostLabel) × (list CostLabel)≝
     621λp,p',prog.
     622let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in
     623let 〈t_env,n,m,keep〉 ≝ (foldr ??
     624           (λi,x.let 〈t_env,n,m,keep〉 ≝ x in
     625           let info ≝ call_post_trans … (f_body … i) n (nil ?) in
     626                   〈(mk_env_item … (f_name … i) (f_pars … i) (f_lab … i)
     627                                  (t_code … info) (f_ret … i)) :: t_env,
     628                     fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 ::
     629                                     ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉)
     630          (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in
     631〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 .
     632
     633discriminator option.
     634
     635definition map_labels_on_trace :
     636(associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝
     637λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l.
     638
     639lemma map_labels_on_trace_append:
     640 ∀m,l1,l2. map_labels_on_trace m (l1@l2) =
     641  map_labels_on_trace m l1 @ map_labels_on_trace m l2.
     642 #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH //
     643qed.
     644
     645lemma correctness : ∀p,p',prog.
     646let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     647∀s1,s2,s1' : state p.∀l.
     648∀t : raw_trace (operational_semantics … p' prog) s1 s2.
     649state_rel … m l keep s1 s1' →
     650∃l'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
     651state_rel  … m l' keep s2 s2' ∧
     652l @ (map_labels_on_trace m (get_costlabels_of_trace … t)) =
     653  (get_costlabels_of_trace … t') @ l'
     654∧ len … t = len … t'.
     655#p #p' #prog @pair_elim * #trans_prog #m #keep #EQtrans
     656#s1 #s2 #s1' #l #t lapply l -l lapply s1' -s1' elim t
     657[ #st #s1' #l #H %{l} %{s1'} %{(t_base …)} % [2: %] %{H} normalize // ]
     658#st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
     659[ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
     660  #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #_ destruct #tl #IH #s1' #l1
     661  whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11
     662  whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
     663  inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
     664  normalize nodelta inversion (foldr2 ???????) [ #_ *] * #H1 #l2 #EQHl2
     665  >m_return_bind normalize nodelta
     666 
     667  inversion (call_post_clean ?????) [ #_ **** ]
     668  * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
     669  cases lab1 in Hio11 Hl1 EQcont11 H; normalize nodelta
     670 
     671  [ whd in match is_silent_cost_act_b; normalize nodelta
     672    cases lab1 in H Hio11; normalize nodelta
     673    [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct]
     674    * normalize nodelta [2: #x #H #Hio11 #EQ destruct] #H #Hio11 #_
     675    inversion(call_post_clean ?????)
     676    [ #_ *** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta *****
     677    #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11
     678    whd in match (call_post_clean ?????) in ⊢ (% → ?); whd in ⊢ (??%% → ?);
     679    inversion(code … s1')
     680    [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     681       destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
     682    normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
     683    cases(IH (mk_state ? new_code' new_cont' (store … s1') false)  l1 ?)
     684    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
     685        normalize nodelta % // % // >EQcode_c_st12 % // ] #l3 * #st3' * #t' **
     686    #Hst3st12' #EQcost #EQlen %{l3} %{st3'} %{(t_ind … (cost_act (None ?)) … t')}
     687    [ whd @(empty ????? 〈(cost_act (None ?)),?〉)
     688      [3: @hide_prf assumption |4: @hide_prf @EQconts1' |*: ] @hide_prf //
     689      [ <EQio #H2 @⊥ lapply(Hio11 H2) * #F #eq destruct | % *]  ] %
     690    [ %{Hst3st12'} whd in match (get_costlabels_of_trace ????); 
     691      whd in match (get_costlabels_of_trace ????) in ⊢ (???%); //
     692    | whd in match (len ????); whd in match (len ????) in ⊢ (???%);
     693      >EQlen %
     694    ]
     695  | #non_sil_lab1 normalize nodelta inversion(call_post_clean ?????) [ #_ ****]
     696    * #l3 #code' #EQcall' normalize nodelta inversion(ret_costed_abs ??)
     697    [2: #x #H2 @⊥ cases lab1 in Hl1 H2; normalize
     698        [ #f #c #_
     699        | #x * #ABS @⊥ @ABS %
     700        | #x #_
     701        | #_
     702        ]
     703        #EQ destruct(EQ) ]
     704    #Hlab1 normalize nodelta ***** #EQ destruct(EQ) #HH1 #EQ destruct(EQ)
     705    >EQcode11  inversion(code … s1')
     706    [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     707       destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
     708    normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
     709    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?)
     710    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
     711        normalize nodelta % // % // % // >EQcall' % ] #l4 * #st3' * #t' **
     712        #Hst3st3' #EQcost #EQlen %{l4} %{st3'} %{(t_ind … lab1 … t')}
     713        [ whd @(empty ????? 〈lab1,?〉)
     714        [3: @hide_prf assumption |4: assumption |*:] @hide_prf // #H3 @Hio11 >EQio @H3]
     715        % [2: whd in match (len ????); whd in match (len ????) in ⊢ (???%);
     716              >EQlen % ]
     717        %{Hst3st3'} >associative_append <EQcost <associative_append
     718        >map_labels_on_trace_append <associative_append @eq_f2 //
     719        cases new_code' in EQcall';
     720        [| #y | #seq #opt_l #i1 | #cond #ltrue #i_true #lfalse #i_false #i1
     721         | #cond #ltrue #i_true #lfalse #ifalse | #f #act_p #ret_opt #i | #l_in #io #l_out #i ]
     722        whd in match (call_post_clean ?????);
     723        [1,2: #EQ destruct(EQ) //
     724       
     725       
     726         whd in match (get_costlabels_of_trace ??? ?) in ⊢ (??%%);
     727       
     728         @eq_f2  whd in ⊢ (??%?);
     729         
     730 
     731 
     732cases daemon (*TODO*)
     733qed.
Note: See TracChangeset for help on using the changeset viewer.