Changeset 2571


Ignore:
Timestamp:
Jan 8, 2013, 5:46:04 PM (7 years ago)
Author:
campbell
Message:

Lots of little changes for cl_tailcall and classifier change.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2499 r2571  
    726726qed.
    727727
     728definition lift_classify : ∀s,c. RTLabs_classify s = c → Some ? (RTLabs_classify s) = Some ? c ≝ λs,c,E. eq_f … E.
     729
    728730lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
    729731  ∀CL : RTLabs_classify s1 = cl_call.
    730732  as_execute (RTLabs_status ge) s1 s2 →
    731733  stack_preserved ge ends_with_ret s2 s3 →
    732   as_after_return (RTLabs_status ge) «s1,CL» s3.
     734  as_after_return (RTLabs_status ge) «s1,lift_classify … CL» s3.
    733735#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
    734736cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
     
    838840(* Small syntax hack to avoid ambiguous input problems. *)
    839841definition myge : nat → nat → Prop ≝ ge.
     842
     843(* RTLabs_classify isn't exactly as_classifier *)
     844definition lift_cl ≝ eq_f ?? (Some status_class).
    840845
    841846let rec make_label_return ge depth (s:RTLabs_ext_state ge)
     
    958963           
    959964    | cl_call ⇒ λCL.
    960         let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
     965        let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
    961966        match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start' ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    962967        (* We're about to run into a label, use base case for call *)
     
    966971            (mk_trace_result ge …
    967972              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
    968                 ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
     973                ? (lift_cl … CL) ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
    969974        (* otherwise use step case *)
    970975        | false ⇒ λCS.
     
    974979            replace_sub_trace … r' ?
    975980              (tal_step_call (RTLabs_status ge) (ends … r')
    976                 start' next' (new_state … r) (new_state … r') ? CL ?
     981                start' next' (new_state … r) (new_state … r') ? (lift_cl … CL) ?
    977982                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
    978983        ] (refl ??)
     
    981986        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
    982987          ends_with_ret
    983           (mk_trace_result ge
     988          (mk_trace_result ge ???????
    984989            next'
    985990            trace'
    986991            ?
    987             (tal_base_return (RTLabs_status ge) start' next' ? CL)
     992            (tal_base_return (RTLabs_status ge) start' next' ? (lift_cl … CL))
    988993            ?
    989994            ?)
     995    | cl_tailcall ⇒ λCL. ⊥
    990996    ] (refl ? (RTLabs_classify start))
    991997   
     
    10291035| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    10301036| %{tr} %{EV} %
    1031 | %1 whd @CL
     1037| %1 whd @(lift_cl … CL)
    10321038| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
    10331039| @(well_cost_labelled_state_step  … EV) //
     
    10621068| @(well_cost_labelled_state_step  … EV) //
    10631069| @(well_cost_labelled_call … EV) //
     1070| skip
    10641071| cases (will_return_call … TERMINATES)
    10651072  #TM * #GT #_ @le_S_S_to_le
     
    10671074  @(transitive_le … TERMINATES_IN_TIME)
    10681075  @(monotonic_le_times_r 3 … GT)
     1076| @(RTLabs_notail … CL)
    10691077| whd @(will_return_notfn … TERMINATES) %1 @CL
    10701078| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    10711079| %{tr} %{EV} %
    1072 | %2 whd @CL
     1080| %2 whd @(lift_cl … CL)
    10731081| @(well_cost_labelled_state_step  … EV) //
    10741082| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
    10751083| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
    1076 | @CL
     1084| @(lift_cl … CL)
    10771085| %{tr} %{EV} %
    10781086| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     
    12651273  state_bound_on_steps_to_cost s (S n) →
    12661274  ∀CL:RTLabs_classify s = cl_call.
    1267   as_after_return (RTLabs_status ge) «s, CL» s' →
     1275  as_after_return (RTLabs_status ge) «s, lift_cl … CL» s' →
    12681276  RTLabs_cost s' = false →
    12691277  state_bound_on_steps_to_cost s' n.
     
    14521460match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
    14531461[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
    1454     (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
     1462    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
    14551463    rem rok
    14561464| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
    1457     (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
     1465    (tac_step_default (RTLabs_status ge) ??? EVAL TAC (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
    14581466    WCL2 EV rem rok
    14591467].
     
    14641472  finite_prefix ge s'' →
    14651473  trace_label_return (RTLabs_status ge) s1 s'' →
    1466   as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' →
     1474  as_after_return (RTLabs_status ge) «s, lift_cl … CALL» s'' →
    14671475  RTLabs_cost s'' = false →
    14681476  finite_prefix ge s ≝
     
    14701478match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
    14711479[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    1472     (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
     1480    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    14731481    rem rok
    14741482| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
    1475     (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
     1483    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    14761484    WCL2 EV rem rok
    14771485].
     
    15251533                let TRACE_OK' ≝ ? in
    15261534                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
    1527                 [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? CL ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
     1535                [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? (lift_cl … CL) ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
    15281536                | false ⇒ λCS.
    15291537                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
     
    15321540              ]
    15331541            | or_intror NO_TERMINATION ⇒
    1534                 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' CL) ?? trace' ?
     1542                fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (lift_cl … CL))) ?? trace' ?
    15351543            ]
    15361544        | cl_return ⇒ λCL. ⊥
     1545        | cl_tailcall ⇒ λCL. ⊥
    15371546        ] (refl ??)
    15381547    ] mtc0
     
    15441553     %{0} % @wr_base //
    15451554| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    1546 | %1 @CL
     1555| %1 @(lift_cl … CL)
    15471556| 6,9,10,11: /3/
    15481557| cases TRACE_OK #H1 #H2 #H3 #H4
     
    15921601    | @(not_return_to_not_final … EV) >CL % #E destruct
    15931602    ]
    1594 | %2 @CL
     1603| @(RTLabs_notail … CL)
     1604| %2 @(lift_cl … CL)
    15951605| 21,22: %{tr} %{EV} %
    15961606| cases (bound_after_step … LABEL_LIMIT EV ?)
     
    16091619  | //
    16101620  ]
     1621| cases (bound_after_step … LABEL_LIMIT EV ?)
     1622  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
     1623    inversion trace'
     1624    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
     1625      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
     1626      % >CL #E destruct
     1627    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
     1628      @wr_base //
     1629    ]
     1630    ]
     1631    | >CL #E destruct
     1632    ]
     1633  | //
     1634  | //
     1635  ]
    16111636| cases TRACE_OK #H1 #H2 #H3 #H4
    16121637  % [ @(well_cost_labelled_state_step … EV) //
     
    16171642    ]
    16181643] qed.
     1644
     1645lemma simplify_cl : ∀ge,s,c.
     1646  as_classifier (RTLabs_status ge) s c →
     1647  RTLabs_classify (Ras_state … s) = c.
     1648#ge * #s #S #M #c #CL
     1649whd in CL; whd in CL:(??%?);
     1650destruct //
     1651qed.
    16191652
    16201653(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
     
    16571690[ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
    16581691| @EV
    1659 | @(trace_any_call_call … T)
    1660 | cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // @(trace_any_call_call … T)
     1692| cases (trace_any_call_call … T) // #CL cases (RTLabs_notail' … CL)
     1693| cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') //
     1694  cases (trace_any_call_call … T) #CL
     1695  [ @simplify_cl @CL
     1696  | @⊥ @(RTLabs_notail' … CL)
     1697  ]
    16611698] qed.
    16621699
     
    17211758        [ witness TERMINATES ⇒
    17221759          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
    1723           twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
     1760          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (lift_cl … IS_CALL) ? (new_trace … tlr) ?
    17241761        ]
    17251762    | or_intror NO_TERMINATION ⇒
    1726         twp_diverges (RTLabs_status ge) s' next' IS_CALL ?
     1763        twp_diverges (RTLabs_status ge) s' next' (lift_cl … IS_CALL) ?
    17271764         (make_label_diverges ge next' trace' ORACLE ?
    17281765            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
     
    19211958      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
    19221959    ]
     1960| tal_base_tailcall s1 s2 s3 EX CL tlr ⇒ ⊥
    19231961].
    1924 
     1962@(RTLabs_notail' … CL)
     1963qed.
    19251964
    19261965(* We take an extra step so that we can always return a non-empty trace to
     
    20762115  | cl_other ⇒ ∀fn,l. P (rapc_state fn l)
    20772116  | cl_jump ⇒ ∀fn,l. P (rapc_state fn l)
     2117  | cl_tailcall ⇒ True
    20782118  ] → P (as_pc_of (RTLabs_status ge) s).
    20792119#ge #cl #P * *
     
    20862126] qed.
    20872127
     2128definition declassify_pc_cl ≝ λge,cl,P,s,s',EX,CL. declassify_pc ge cl P s s' EX (simplify_cl … CL).
     2129
    20882130lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
    20892131  as_execute (RTLabs_status ge) s s' →
     
    20942136  | cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
    20952137  | cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
     2138  | cl_tailcall ⇒ False
    20962139  ] .
    20972140#ge * #s #s' #EX #CL whd
    20982141@(declassify_pc … EX CL) whd
    2099 [ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | #fn #l %{fn} %{l} % ]
     2142[ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | @I | #fn #l %{fn} %{l} % ]
    21002143qed.
    21012144
     
    21402183| #s1 #s2 * #tr * #EX #NX #CL
    21412184| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
     2185| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
    21422186| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
    21432187| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
     
    21582202| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
    21592203  whd in CL CL'; >CL in CL'; #E destruct
     2204| #s1 #s2 #s3 #EX #CL' @⊥ @(RTLabs_notail' … CL')
    21602205| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
    21612206  whd in CL CL'; >CL in CL'; #E destruct
     
    22312276#ge #pre #post #CL #ret #callee #AF
    22322277cases pre in CL AF ⊢ %;
    2233 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
     2278* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??(??%)?);
    22342279    cases (next_instruction f) in CL;
    22352280    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
     
    22882333  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
    22892334  >(pc_label_eq … PC0 PC1) %1
     2335| #s1 #s2 #s3 #EX #CL #tlr #l1 #PC1 #G #NCS #IN @⊥ @(RTLabs_notail' … CL)
    22902336| #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
    22912337  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
    22922338  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
    22932339  | #NE #IN
    2294     lapply (declassify_pc' … EX CL) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1
     2340    lapply (declassify_pc' … EX (simplify_cl … CL)) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1
    22952341    [ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G
    22962342      lapply (pc_label_call_eq … PC1) #E destruct
     
    23032349  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
    23042350  | #NE #IN
    2305     cases (declassify_state … EX CL)
     2351    cases (declassify_state … EX (simplify_cl … CL))
    23062352    #f * #fs * #m * #S * #M #E destruct
    23072353    cut (l1 = next f)
     
    23102356    cases EX #tr * #EV #NX
    23112357    cases (eval_successor … EV)
    2312     [ * #CL' @⊥ cases (tal_return … CL' tal') #EX' * #CL'' * #E1 #E2 destruct
    2313       lapply (memb_single … IN) @(declassify_pc … EX' CL'') whd
     2358    [ * #CL' @⊥ cases (tal_return … (lift_cl … CL') tal') #EX' * #CL'' * #E1 #E2 destruct
     2359      lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd
    23142360      #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
    23152361    | * #l' * #AS #SC
     
    23442390cases (eval_successor … EV)
    23452391[ * #CL2 #SC
    2346   cases (tal_return … CL2 tal) #EX2 * #CL2' * #E1 #E2 destruct
     2392  cases (tal_return … (lift_cl … CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
    23472393  @notb_Prop % whd in match (tal_pc_list ?????); #IN
    23482394  lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
     
    23892435  as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4.
    23902436#ge * #s1 #S1 #M1 #CL1
    2391 cases (rtlabs_call_inv … CL1) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
     2437cases (rtlabs_call_inv … (simplify_cl … CL1)) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
    23922438* #s2 #S2 #M2 #CL2
    2393 cases (rtlabs_call_inv … CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
     2439cases (rtlabs_call_inv … (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
    23942440* * [ #f3 #fs3 #m3 #S3 #M3 | #a #b #c #d #e #f #g #h * | #a #b #c #d #e #f #g * | #r3 #S3 #M3 ]
    23952441* * [ 1,5: #f4 #fs4 #m4 #S4 #M4 | 2,6: #a #b #c #d #e #f #g #h * | 3,7: #a #b #c #d #e #f #g * | 4,8: #r4 #S4 #M4 ]
     
    24672513#ge #flX #s1X #s2X *
    24682514[ #s1 #s2 #EX *
    2469   [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL in CL'; #CL' destruct
     2515  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
    24702516  | #CL #CS #CL' @eq_true_to_b @memb_hd
    24712517  ]
    2472 | #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL in CL'; #CL' destruct
    2473 | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = cl_call) in CL; >CL in CL'; #CL' destruct
    2474 | #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = cl_call) in CL; >CL in CL'; #CL' destruct
     2518| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2519| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2520| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
     2521| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
    24752522| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
    24762523] qed.
     
    24802527  state_fn … pre = state_fn … post.
    24812528#ge * #pre #preS #preM * #post #postS #postM #CL #AF
    2482 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #fs * #m #E destruct
     2529cases (rtlabs_call_inv … (simplify_cl … CL)) #fd * #args * #dst * #fs * #m #E destruct
    24832530cases post in postM AF ⊢ %;
    24842531[ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF
     
    25282575[ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥
    25292576  whd in match (tal_pc_list ?????) in IN;
    2530   lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee
    2531   cases CL3 #CL3' @(declassify_pc … EX3 CL3') #fn #l
     2577  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
     2578  cases CL3 #CL3' @(declassify_pc_cl … EX3 CL3') #fn #l
    25322579  #IN' destruct
    25332580| #s2 #s4 #EX2 #CL2 #FN #IN @⊥
    2534   lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee
    2535   @(declassify_pc … EX2 CL2) whd #fn
     2581  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
     2582  @(declassify_pc_cl … EX2 CL2) whd #fn
    25362583  #IN' destruct
    25372584| #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN
     
    25392586  lapply (pc_after_return_eq … AF1 AF3 E FN) #PC
    25402587  @⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) //
     2588| #s1 #s2 #s3 #EX #CL #tlr #S1 #IN @⊥ @(RTLabs_notail' … CL)
    25412589| #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN
    25422590  whd in ⊢ (?% → ?); @eqb_elim
     
    25492597  ]
    25502598| #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN
    2551   change with (RTLabs_classify ? = ?) in CL1;
    2552   change with (RTLabs_classify ? = ?) in CL3;
     2599  lapply (simplify_cl … CL1) #CL1'
     2600  lapply (simplify_cl … CL3) #CL3'
    25532601  @eq_true_to_b @memb_cons
    25542602  @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1)
    2555   [ >FN cases (state_fn_other … CL3 EX3)
    2556     [ #CL3' @⊥
    2557       cases (tal_return … CL3' tal3')
    2558       #EX3' * #CL3'' * #E1 #E2 destruct
     2603  [ >FN cases (state_fn_other … CL3' EX3)
     2604    [ #CL3'' @⊥
     2605      cases (tal_return … (lift_cl … CL3'') tal3')
     2606      #EX3' * #CL3''' * #E1 #E2 destruct
    25592607      whd in IN:(?%); lapply IN @eqb_elim
    2560       [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3 #E destruct
    2561       | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1 >CL3' #E destruct
     2608      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
     2609      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1' >CL3'' #E destruct
    25622610      ]
    25632611    | //
    25642612    ]
    25652613  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
    2566     [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3 #E destruct
     2614    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
    25672615    | #NE #IN @IN
    25682616    ]
     
    25832631[ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥
    25842632  whd in match (tal_pc_list ?????) in IN;
    2585   lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee
    2586   cases CL2 #CL2' @(declassify_pc … EX2 CL2') #fn #l
     2633  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
     2634  cases CL2 #CL2' @(declassify_pc_cl … EX2 CL2') #fn #l
    25872635  #IN' destruct
    25882636| #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥
    2589   lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee
    2590   @(declassify_pc … EX2 CL2) whd #fn
     2637  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
     2638  @(declassify_pc_cl … EX2 CL2) whd #fn
    25912639  #IN' destruct
    25922640| #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥
    2593   cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
    2594   cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
     2641  cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
     2642  cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
    25952643  cases AF1
     2644| #s1 #s2 #s3 #EX #CL #tlr @⊥ @(RTLabs_notail' … CL)
    25962645| #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥
    2597   cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
    2598   cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
     2646  cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
     2647  cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
    25992648  cases AF1
    26002649| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
    2601   change with (RTLabs_classify ? = ?) in CL;
    2602   change with (RTLabs_classify ? = ?) in CL2;
     2650  lapply (simplify_cl … CL) #CL'
     2651  lapply (simplify_cl … CL2) #CL2'
    26032652  %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ]
    26042653  (* Now that we've inverted the first part of the trace, look for the repeat. *)
    2605   @(pc_after_call_repeats_aux … CL … AF1 CL2 CS2 EX1)
     2654  @(pc_after_call_repeats_aux … CL … AF1 CL2' CS2 EX1)
    26062655  [ >(state_fn_after_return … AF1)
    2607     cases (state_fn_other … CL2 EX2)
     2656    cases (state_fn_other … CL2' EX2)
    26082657    [ #CL3 @⊥
    2609       cases (tal_return … CL3 tal3)
     2658      cases (tal_return … (lift_cl … CL3) tal3)
    26102659      #EX3 * #CL3' * #E1 #E2 destruct
    2611       change with (RTLabs_classify ? = ?) in CL3';
     2660      lapply (simplify_cl … CL3') #CL3''
    26122661      whd in IN:(?%); lapply IN @eqb_elim
    2613       [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2 #E destruct
    2614       | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL >CL3' #E destruct
     2662      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
     2663      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL' >CL3'' #E destruct
    26152664      ]
    26162665    | //
    26172666    ]
    26182667  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
    2619     [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2 #E destruct
     2668    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
    26202669    | #NE #IN @IN
    26212670    ]
     
    26372686@(absurd ? IN')
    26382687@Prop_notb
    2639 @no_loops_in_tal assumption
     2688@no_loops_in_tal /2/
    26402689qed.
    26412690
     
    26762725| tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1
    26772726| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1)
     2727| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
    26782728| tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1))
    26792729| tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1)
    26802730].
     2731@(RTLabs_notail' … CL)
     2732qed.
    26812733
    26822734(* And join everything up to show that soundly labelled states give unrepeating
     
    27102762| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1.
    27112763    tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1)
     2764| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
    27122765| tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1.
    27132766    conj ?? (conj ???
     
    27172770    conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1))
    27182771].
    2719 [ @(no_repeats_of_calls … EX AF) [ assumption |
     2772[ @(RTLabs_notail' … CL)
     2773| @(no_repeats_of_calls … EX AF) [ assumption |
    27202774  @(tlr_sound … tlr) [ assumption | @(soundly_step … GE EX S1) ] ]
    2721 | @no_loops_in_tal // @CL
    2722 ] qed.
    2723 
     2775| @no_loops_in_tal // @simplify_cl @CL
     2776] qed.
     2777
  • src/RTLabs/abstract.ma

    r2511 r2571  
    201201 *)
    202202
    203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. RTLabs_classify s = cl_call) → RTLabs_ext_state ge → Prop ≝
     203definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝
    204204λge,s,s'.
    205205  match s with
    206206  [ mk_Sig s p ⇒
    207     match s return λs. RTLabs_classify s = cl_call → ? with
     207    match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
    208208    [ Callstate fd args dst stk m ⇒
    209209      λ_. match s' with
     
    219219   ] p
    220220 ].
    221 [ whd in H:(??%?);
     221[ whd in H:(??(??%)?);
    222222  cases (next_instruction f) in H;
    223223  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     
    226226] qed.
    227227
    228 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. RTLabs_classify s = cl_call) → ident ≝
     228definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝
    229229λge,s.
    230230  match s with
    231231  [ mk_Sig s p ⇒
    232     match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
     232    match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with
    233233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234       match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
     234      match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
    235235      [ Callstate fd _ _ _ _ ⇒
    236236        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
     
    243243    ] p
    244244  ].
    245 [ whd in H:(??%?);
     245[ whd in H:(??(??%)?);
    246246  cases (next_instruction f) in H;
    247247  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     
    251251] qed.
    252252
     253lemma RTLabs_notail : ∀s.
     254  RTLabs_classify s = cl_tailcall →
     255  False.
     256* [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ]
     257normalize
     258#a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     259qed.
     260
     261(* Roughly corresponding to as_classifier *)
     262lemma RTLabs_notail' : ∀s.
     263  Some ? (RTLabs_classify s) = Some ? cl_tailcall →
     264  False.
     265#s #E @(RTLabs_notail … s)
     266generalize in match (RTLabs_classify s) in E ⊢ %;
     267#c #E' destruct %
     268qed.
    253269
    254270definition RTLabs_status : genv → abstract_status ≝
     
    259275    RTLabs_deqset
    260276    (RTLabs_ext_state_to_pc ge)
    261     RTLabs_classify
     277    (λs. Some ? (RTLabs_classify s))
    262278    (RTLabs_pc_to_cost_label ge)
    263279    (RTLabs_after_return ge)
    264280    (λs. RTLabs_is_final s ≠ None ?)
    265     (RTLabs_call_ident ge).
    266 
    267 
     281    (RTLabs_call_ident ge)
     282    (λs. ⊥).
     283(* No tailcalls here for now. *)
     284cases s @RTLabs_notail'
     285qed.
    268286
    269287(* Allow us to move between the different notions of when a state is cost
Note: See TracChangeset for help on using the changeset viewer.