Changeset 1682


Ignore:
Timestamp:
Feb 9, 2012, 1:22:33 PM (6 years ago)
Author:
campbell
Message:

Complete proof for as_after_return for RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1681 r1682  
    446446
    447447(* The preservation of (most of) the stack is useful to show as_after_return.
    448    This is a partial closure of the state_rel relation in semantics.ma - we only
    449    accumulate information up to the first return. *)
     448   We do this by showing that during the execution of a function the lower stack
     449   frames never change, and that after returning from the function we preserve
     450   the identity of the next instruction to execute.
     451 *)
     452
     453inductive stack_of_state : list frame → state → Prop ≝
     454| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
     455| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
     456| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
     457.
     458
    450459inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
    451 | sp_normal : ∀f,f',fs,m,m'. frame_rel f f' → stack_preserved doesnt_end_with_ret (State f fs m) (State f' fs m')
    452 | sp_to_call : ∀f,f',fs,m,m',fd,args,dst. frame_rel f f' → stack_preserved doesnt_end_with_ret (State f fs m) (Callstate fd args dst (f'::fs) m')
    453 (* Remember that this is one *after* the state just considered, so the trace
    454    doesn't end with return, the return is the next state *)
    455 | sp_to_return : ∀f,fs,m,rtv,dst,m'. stack_preserved doesnt_end_with_ret (State f fs m) (Returnstate rtv dst fs m')
    456 | sp_from_return : ∀f,f',fs,m,rtv,dst,m'. (next f = next f') → frame_rel f f' → stack_preserved ends_with_ret (Returnstate rtv dst (f::fs) m) (State f' fs m')
    457 (* A combination of the above *)
    458 | sp_over_return : ∀f1,f2,f3,fs,m,m'. (next f2 = next f3) → frame_rel f2 f3 → stack_preserved ends_with_ret (State f1 (f2::fs) m) (State f3 fs m').
    459 
    460 lemma frame_rel_trans : transitive ? frame_rel.
    461 #x #y #z *
    462 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 inversion H10
    463 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 destruct //
    464 qed.
     460| sp_normal : ∀fs,s1,s2.
     461    stack_of_state fs s1 →
     462    stack_of_state fs s2 →
     463    stack_preserved doesnt_end_with_ret s1 s2
     464| sp_finished : ∀s1,f,f',fs,m.
     465    next f = next f' →
     466    stack_of_state (f::fs) s1 →
     467    stack_preserved ends_with_ret s1 (State f' fs m).
     468
     469discriminator list.
     470
     471lemma stack_of_state_eq : ∀fs,fs',s.
     472  stack_of_state fs s →
     473  stack_of_state fs' s →
     474  fs = fs'.
     475#fs0 #fs0' #s0 *
     476[ #f #fs #m #H inversion H
     477  #a #b #c #d #e #g try #h try #i try #j destruct @refl
     478| #fd #args #dst #f #fs #m #H inversion H
     479  #a #b #c #d #e #g try #h try #i try #j destruct @refl
     480| #rtv #dst #fs #m #H inversion H
     481  #a #b #c #d #e #g try #h try #i try #j destruct @refl
     482] qed.
    465483
    466484lemma stack_preserved_join : ∀e,s1,s2,s3.
     
    469487  stack_preserved e s1 s3.
    470488#e1 #s1 #s2 #s3 #H1 inversion H1
    471 [ #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct #H2 inversion H2
    472   [ #f2 #f2' #fs2 #m2 #m2' #F2 #E1 #E2 #E3 #E4 destruct % /2/
    473   | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct %2 /2/
    474   | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct /2/
    475   | #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H145 #H146 destruct
    476   | #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H148 #H149 #H150 destruct /2/
    477   ]
    478 | #f #f' #fs #m #m' #fd #args #dst #F #E1 #E2 #E3 #E4 destruct #H2 inversion H2
    479   [ #f2 #f2' #fs2 #m2 #m2' #F2 #H2' #E1 #E2 #E3 destruct
    480   | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct
    481   | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct
    482   | #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H145 #H146 destruct
    483   | #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H148 #H149 destruct
    484   ]
    485 | #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct #H2 inversion H2
    486   [ #f2 #f2' #fs2 #m2 #m2' #F2 #H2' #E1 #E2 #E3 destruct
    487   | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
    488   | #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 destruct
    489   | #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H151 #H152 destruct /2/
    490   | #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H154 #H155 destruct
    491   ]
    492 | #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct
    493 | #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 destruct
    494 ] qed.
    495 
    496 lemma stack_preserved_ret : ∀ge,s1,s2,tr.
     489[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
     490  #H2 inversion H2
     491  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
     492    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
     493  | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct
     494    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
     495  ]
     496| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
     497] qed.
     498
     499lemma stack_preserved_return : ∀ge,s1,s2,tr.
    497500  RTLabs_classify s1 = cl_return →
    498501  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
     
    506509  [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct
    507510  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
    508     whd in EV:(??%?); destruct @sp_from_return cases f //
     511    whd in EV:(??%?); destruct @(sp_finished ? f) //
    509512  ]
    510513] qed.
     
    532535cases (rtlabs_call_inv … CL)
    533536#fd * #args * #dst * #stk * #m #E destruct
     537inversion SP
     538[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
     539| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
     540  inversion (eval_perserves … EV)
     541  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
     542  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
     543  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
     544    inversion S
     545    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
     546    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
     547    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
     548    ]
     549  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
     550  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
     551  ]
     552] qed.
     553 
     554lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
     555  ∀CL : RTLabs_classify s1 = cl_call.
     556  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
     557  stack_preserved ends_with_ret s2 s3 →
     558  as_after_return (RTLabs_status ge) «s1,CL» s3.
     559#ge #s1 #s2 #s3 #tr #CL #EV #S23
     560cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
     561inversion S23
     562[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
     563| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
     564  inversion (eval_perserves … EV)
     565  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
     566  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
     567  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
     568    inversion S
     569    [ #fy #fsy #my #E1 #E2 #E3 destruct @N
     570    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
     571    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
     572    ]
     573  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
     574  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
     575  ]
     576] qed.
    534577
    535578(* Don't need to know that labels break loops because we have termination. *)
     
    749792     this can't happen *)
    750793| @(will_return_return … CL TERMINATES)
    751 | /2/
     794| /2 by stack_preserved_return/
    752795| %{tr} @EV
    753796| @(well_cost_labelled_state_step  … EV) //
     
    758801| @(well_cost_labelled_jump … EV) //
    759802| @(well_cost_labelled_state_step  … EV) //
    760 | @sp_over_return
     803| @(stack_preserved_call … EV (stack_ok … r)) //
    761804| %{tr} @EV
    762 |  (* TODO oh dear *)
     805| @RTLabs_after_call //
    763806| cases (will_return_call … TERMINATES) #H @le_S_to_le
    764 | cases r #H1 #H2 #H3 #H4 * #H5
     807| cases r #H1 #H2 #H3 #H4 #H5 * #H6
    765808  cases (will_return_call … CL TERMINATES)
    766809  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
    767 | (* TODO oh dear *)
     810| @RTLabs_after_call //
    768811| %{tr} @EV
     812| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
    769813| @(cost_labelled … r)
    770 | cases r #H72 #H73 #H74 #H75 * #H76 #H78
     814| cases r #H72 #H73 #H74 #H75 #HX * #H76 #H78
    771815  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    772816  cases (will_return_call … TERMINATES) in H78;
     
    785829  @(monotonic_le_times_r 3 … GT)
    786830| whd @(will_return_notfn … TERMINATES) %1 @CL
     831| @(stack_preserved_step … EV) /2/
    787832| %{tr} @EV
    788833| %2 whd @CL
     
    791836| @CL
    792837| %{tr} @EV
     838| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
    793839| @(well_cost_labelled_state_step  … EV) //
    794840| %1 @CL
     
    813859  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    814860  (TERMINATES: will_return ge depth s trace)
    815   : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
     861  : trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
    816862make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
    817863  (2 + 3 * will_return_length … TERMINATES) ?.
Note: See TracChangeset for help on using the changeset viewer.