Changeset 2757 for src/RTLabs


Ignore:
Timestamp:
Mar 1, 2013, 7:13:49 PM (7 years ago)
Author:
tranquil
Message:

many things are still broken, but there is a partial backtrack on Structured traces's execute

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_abstract.ma

    r2724 r2757  
    201201 *)
    202202
    203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝
     203definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = 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. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
     207    match s return λs. RTLabs_classify s = 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. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝
     228definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → ident ≝
    229229λge,s.
    230230  match s with
    231231  [ mk_Sig s p ⇒
    232     match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with
     232    match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
    233233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234       match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
     234      match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = 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
     
    261261(* Roughly corresponding to as_classifier *)
    262262lemma RTLabs_notail' : ∀s.
    263   Some ? (RTLabs_classify s) = Some ? cl_tailcall →
     263  RTLabs_classify s = cl_tailcall →
    264264  False.
    265265#s #E @(RTLabs_notail … s)
     
    275275    RTLabs_deqset
    276276    (RTLabs_ext_state_to_pc ge)
    277     (λs. Some ? (RTLabs_classify s))
     277    (RTLabs_classify)
    278278    (RTLabs_pc_to_cost_label ge)
    279279    (RTLabs_after_return ge)
    280     (λs. RTLabs_is_final s ≠ None ?)
     280    (RTLabs_is_final)
    281281    (RTLabs_call_ident ge)
    282282    (λs. ⊥).
  • src/RTLabs/RTLabs_traces.ma

    r2728 r2757  
    726726qed.
    727727
    728 definition lift_classify : ∀s,c. RTLabs_classify s = c → Some ? (RTLabs_classify s) = Some ? c ≝ λs,c,E. eq_f … E.
    729 
    730728lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
    731729  ∀CL : RTLabs_classify s1 = cl_call.
    732730  as_execute (RTLabs_status ge) s1 s2 →
    733731  stack_preserved ge ends_with_ret s2 s3 →
    734   as_after_return (RTLabs_status ge) «s1,lift_classify … CL» s3.
     732  as_after_return (RTLabs_status ge) «s1,CL» s3.
    735733#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
    736734cases (rtlabs_call_inv … CL) #vf * #fn * #args * #dst * #stk * #m #E destruct
     
    840838(* Small syntax hack to avoid ambiguous input problems. *)
    841839definition myge : nat → nat → Prop ≝ ge.
    842 
    843 (* RTLabs_classify isn't exactly as_classifier *)
    844 definition lift_cl ≝ eq_f ?? (Some status_class).
    845840
    846841let rec make_label_return ge depth (s:RTLabs_ext_state ge)
     
    971966            (mk_trace_result ge …
    972967              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
    973                 ? (lift_cl … CL) ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
     968                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
    974969        (* otherwise use step case *)
    975970        | false ⇒ λCS.
     
    979974            replace_sub_trace … r' ?
    980975              (tal_step_call (RTLabs_status ge) (ends … r')
    981                 start' next' (new_state … r) (new_state … r') ? (lift_cl … CL) ?
     976                start' next' (new_state … r) (new_state … r') ? CL ?
    982977                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
    983978        ] (refl ??)
     
    990985            trace'
    991986            ?
    992             (tal_base_return (RTLabs_status ge) start' next' ? (lift_cl … CL))
     987            (tal_base_return (RTLabs_status ge) start' next' ? CL)
    993988            ?
    994989            ?)
     
    10351030| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    10361031| %{tr} %{EV} %
    1037 | %1 whd @(lift_cl … CL)
     1032| %1 whd @CL
    10381033| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
    10391034| @(well_cost_labelled_state_step  … EV) //
     
    10781073| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    10791074| %{tr} %{EV} %
    1080 | %2 whd @(lift_cl … CL)
     1075| %2 whd @CL
    10811076| @(well_cost_labelled_state_step  … EV) //
    10821077| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
    10831078| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
    1084 | @(lift_cl … CL)
     1079| @CL
    10851080| %{tr} %{EV} %
    10861081| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     
    12731268  state_bound_on_steps_to_cost s (S n) →
    12741269  ∀CL:RTLabs_classify s = cl_call.
    1275   as_after_return (RTLabs_status ge) «s, lift_cl … CL» s' →
     1270  as_after_return (RTLabs_status ge) «s, CL» s' →
    12761271  RTLabs_cost s' = false →
    12771272  state_bound_on_steps_to_cost s' n.
     
    14601455match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
    14611456[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
    1462     (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
     1457    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    14631458    rem rok
    14641459| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
    1465     (tac_step_default (RTLabs_status ge) ??? EVAL TAC (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
     1460    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
    14661461    WCL2 EV rem rok
    14671462].
     
    14721467  finite_prefix ge s'' →
    14731468  trace_label_return (RTLabs_status ge) s1 s'' →
    1474   as_after_return (RTLabs_status ge) «s, lift_cl … CALL» s'' →
     1469  as_after_return (RTLabs_status ge) «s, CALL» s'' →
    14751470  RTLabs_cost s'' = false →
    14761471  finite_prefix ge s ≝
     
    14781473match 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
    14791474[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    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)
     1475    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    14811476    rem rok
    14821477| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
    1483     (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)
     1478    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    14841479    WCL2 EV rem rok
    14851480].
     
    15331528                let TRACE_OK' ≝ ? in
    15341529                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
    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'
     1530                [ 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'
    15361531                | false ⇒ λCS.
    15371532                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
     
    15401535              ]
    15411536            | or_intror NO_TERMINATION ⇒
    1542                 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (lift_cl … CL))) ?? trace' ?
     1537                fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (CL))) ?? trace' ?
    15431538            ]
    15441539        | cl_return ⇒ λCL. ⊥
     
    15531548     %{0} % @wr_base //
    15541549| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    1555 | %1 @(lift_cl … CL)
     1550| %1 @(CL)
    15561551| 6,9,10,11: /3/
    15571552| cases TRACE_OK #H1 #H2 #H3 #H4
     
    16021597    ]
    16031598| @(RTLabs_notail … CL)
    1604 | %2 @(lift_cl … CL)
     1599| %2 @(CL)
    16051600| 21,22: %{tr} %{EV} %
    16061601| cases (bound_after_step … LABEL_LIMIT EV ?)
     
    17581753        [ witness TERMINATES ⇒
    17591754          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
    1760           twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (lift_cl … IS_CALL) ? (new_trace … tlr) ?
     1755          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (IS_CALL) ? (new_trace … tlr) ?
    17611756        ]
    17621757    | or_intror NO_TERMINATION ⇒
    1763         twp_diverges (RTLabs_status ge) s' next' (lift_cl … IS_CALL) ?
     1758        twp_diverges (RTLabs_status ge) s' next' (IS_CALL) ?
    17641759         (make_label_diverges ge next' trace' ORACLE ?
    17651760            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
     
    23562351    cases EX #tr * #EV #NX
    23572352    cases (eval_successor … EV)
    2358     [ * #CL' @⊥ cases (tal_return … (lift_cl … CL') tal') #EX' * #CL'' * #E1 #E2 destruct
     2353    [ * #CL' @⊥ cases (tal_return … (CL') tal') #EX' * #CL'' * #E1 #E2 destruct
    23592354      lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd
    23602355      #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
     
    23902385cases (eval_successor … EV)
    23912386[ * #CL2 #SC
    2392   cases (tal_return … (lift_cl … CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
     2387  cases (tal_return … (CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
    23932388  @notb_Prop % whd in match (tal_pc_list ?????); #IN
    23942389  lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
     
    26032598  [ >FN cases (state_fn_other … CL3' EX3)
    26042599    [ #CL3'' @⊥
    2605       cases (tal_return … (lift_cl … CL3'') tal3')
     2600      cases (tal_return … (CL3'') tal3')
    26062601      #EX3' * #CL3''' * #E1 #E2 destruct
    26072602      whd in IN:(?%); lapply IN @eqb_elim
     
    26562651    cases (state_fn_other … CL2' EX2)
    26572652    [ #CL3 @⊥
    2658       cases (tal_return … (lift_cl … CL3) tal3)
     2653      cases (tal_return … (CL3) tal3)
    26592654      #EX3 * #CL3' * #E1 #E2 destruct
    26602655      lapply (simplify_cl … CL3') #CL3''
Note: See TracChangeset for help on using the changeset viewer.