Changeset 2894


Ignore:
Timestamp:
Mar 16, 2013, 9:08:18 PM (7 years ago)
Author:
campbell
Message:

Some progress on showing that the change to structured traces preserves
observables.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/MeasurableToStructured.ma

    r2893 r2894  
    190190] qed.
    191191
     192lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
     193  eval_statement ge s = return 〈tr,s'〉 →
     194  ∃S,M. eval_ext_statement ge s = return 〈tr,mk_RTLabs_ext_state … s' S M〉.
     195#ge #s #tr #s' #EV
     196whd in match (eval_ext_statement ??);
     197letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
     198cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
     199[ // ]
     200generalize in match f; -f
     201>EV #next #NEXT whd in ⊢ (??(λ_.??(λ_.??%?)));
     202lapply (NEXT … (refl ??))
     203cases (next s' tr ?) #s'' #S'' #M'' #E destruct %{S''} %{M''} %
     204qed.
     205
    192206lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.
    193207  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
    … …  
    255269] qed.
    256270
     271lemma int_trace_split : ∀C,t1,t2,callstack,cs2,obs.
     272  intensional_trace_of_trace C callstack (t1@t2) = 〈cs2,obs〉 →
     273  ∃cs1,t1',t2'.
     274  intensional_trace_of_trace C callstack t1 = 〈cs1,t1'〉 ∧
     275  intensional_trace_of_trace C cs1 t2 = 〈cs2,t2'〉 ∧
     276  obs = t1'@t2'.
     277#C #t1 #t2 #cs0 #cs2 #obs >int_trace_append'
     278cases (intensional_trace_of_trace C cs0 t1) #cs1 #t1'
     279normalize nodelta #E %{cs1} %{t1'}
     280cases (intensional_trace_of_trace C cs1 t2) in E ⊢ %; #cs2 #t2'
     281normalize nodelta #E destruct
     282%{t2'}
     283/3/
     284qed.
     285
     286definition cs_change : trace_ends_with_ret → ident → list ident → list ident → Prop ≝ λends,fn,cs,cs'.
     287match ends with
     288[ ends_with_ret ⇒ cs = cs'
     289| doesnt_end_with_ret ⇒ fn::cs = cs'
     290].
     291
     292lemma as_exec_eq_step : ∀ge,s1,s2,tr,s2'.
     293  as_execute (RTLabs_status ge) s1 s2 →
     294  step io_out io_in RTLabs_ext_fullexec ge s1 = Value ??? 〈tr,s2'〉 →
     295  s2 = s2'.
     296#ge #s1 #s2 #tr #s2' * #tr * #EX
     297whd in ⊢ (? → ??%? → ?);
     298letin f ≝ (next_state ge s1) change with (f (Ras_state … s2) tr EX) in ⊢ (??%? → ?);
     299generalize in ⊢ (??(%???)? → ??(?%)? → ?); >EX in ⊢ (% → % → ??(match % with [_⇒?|_⇒?|_⇒?]?)? → ?);
     300#next #NEXT whd in ⊢ (??%? → ?); #E destruct >NEXT %
     301qed.
     302
     303include alias "basics/logic.ma". (* For ∧ *)
     304
     305let rec eq_end_tlr ge s trace' s' tlr s'' on tlr :
     306  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
     307  s' = s'' ≝ ?
     308and eq_end_tll ge s trace' s' ends tll s'' on tll :
     309  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
     310  s' = s'' ≝ ?
     311and eq_end_tal ge s trace' s' ends tal s'' on tal :
     312  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
     313  s' = s'' ≝ ?.
     314[ cases tlr
     315  [ #s1 #s2 #tll @eq_end_tll
     316  | #s1 #s2 #s3 #tll #tlr' #EX
     317    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1
     318    <(eq_end_tll … EX1) #EX2 #E
     319    @(eq_end_tlr … EX2)
     320  ]
     321| cases tll
     322  #ends' #s1 #s2 #tal #CS
     323  @eq_end_tal
     324| cases tal
     325  [ #s1 #s2 #EX #CL #CS whd in ⊢ (??(?%?????)? → ?); #EX'
     326    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
     327    whd in EX':(??%%); destruct
     328    @(as_exec_eq_step … EX ST)
     329  | #s1 #s2 #EX #CL #EX'
     330    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
     331    whd in EX':(??%%); destruct
     332    @(as_exec_eq_step … EX ST)
     333  | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #EX'
     334    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
     335    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
     336    @(eq_end_tlr … tlr … EX')
     337  | #s1 #s2 #s3 #EX #CL #tlr #EX'
     338    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
     339    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
     340    @(eq_end_tlr … tlr … EX')
     341  | #ends #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal' #EX'
     342    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
     343    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
     344    cases (exec_steps_split … EX') #trace1 * #trace2 * #s5 * * #EX2 #EX3 #E3
     345    lapply (eq_end_tlr … tlr … EX2) #E4 <E4 in EX3; #EX3
     346    @(eq_end_tal … EX3)
     347  | #ends #s1 #s2 #s3 #EX #tal' #CL #CS #EX'
     348    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
     349    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
     350    @(eq_end_tal … EX')
     351  ]
     352] qed.
     353
     354definition maybe_label ≝
     355λge,s,obs.
     356  match as_label (RTLabs_status ge) s with
     357  [ None ⇒ obs
     358  | Some cl ⇒ (IEVcost cl)::obs
     359  ].
     360
     361lemma definitely_maybe_label : ∀ge,s,CS,tl.
     362  (IEVcost (as_label_safe (RTLabs_status ge) «s,CS»))::tl = maybe_label ge s tl.
     363#ge #s #CS #tl
     364whd in ⊢ (???%); whd in match (as_label_safe ??);
     365>(opt_to_opt_safe … CS) in ⊢ (???%);
     366%
     367qed.
     368
     369lemma only_plain_step_events_is_one_cost : ∀ge,s,tr,s'.
     370  eval_statement ge s = Value ??? 〈tr,s'〉 →
     371  (∃cl. tr = [EVcost cl] ∧ RTLabs_cost_label s = Some ? cl) ∨
     372  (tr = [ ] ∧ RTLabs_cost_label s = None ?).
     373#ge *
     374[ #f #fs #m #tr #s' whd in ⊢ (??%? → ?);
     375  whd in match (RTLabs_cost_label ?); generalize in ⊢ (??(?%)? → ?);
     376  cases (next_instruction f)
     377  [ #l #LP normalize nodelta #E whd in E:(??%%); destruct %2 % %
     378  | #cl #l #LP #E whd in E:(??%%); destruct % %{cl} % %
     379  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct %2 % %
     380  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
     381  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
     382  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
     383  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
     384  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 % %
     385  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok * #fd #fid #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ? Efd) #b * #Ev' #Efn %2 % %
     386  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct %2 % %
     387  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result ?) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %2 % %
     388  ]
     389| #vf * #fn #args #retdst #stk #m #tr #s'
     390  whd in ⊢ (??%? → ?);
     391  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
     392    #E destruct %2 % %
     393  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct %2 % %
     394  ]
     395| #v #r * [2: #f #fs ] #m #tr #s'
     396  whd in ⊢ (??%? → ?);
     397  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %2 % %
     398  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct %2 % % | *: normalize #a try #b destruct ] ]
     399  ]
     400| #r #tr #s' normalize #E destruct
     401] qed.
     402
     403lemma drop_exec_ext : ∀ge,s,tr,s'.
     404  eval_ext_statement ge s = return 〈tr,s'〉 →
     405  eval_statement ge s = return 〈tr,Ras_state … s'〉.
     406#ge #s #tr #s'
     407whd in ⊢ (??%? → ?);
     408letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
     409cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
     410[ // ]
     411generalize in match f; -f
     412cases (eval_statement ge s)
     413[ #o #k #n #N #E whd in E:(??%%); destruct
     414| * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
     415| #m #n #N #E whd in E:(??%%); destruct
     416] qed.
     417
     418lemma RTLabs_as_label : ∀ge,s.
     419  RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s.
     420cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
     421#ge * *
     422[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
     423  whd in ⊢ (???%);
     424  whd in match (as_pc_of ??);
     425  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
     426  whd in ⊢ (???%); >M1 whd in ⊢ (???%);
     427  whd in ⊢ (??%?); change with (lookup_present ?????) in match (next_instruction ?);
     428  >(lookup_lookup_present … nok) whd in ⊢ (??%%);
     429  %
     430| #vf #fd #args #dst #fs #m * [*] #func #stk #mtc whd in ⊢ (??%%); %
     431| #v #dst #fs #m * [2: #fn #stk] #mtc %
     432| // #r #stk #mtc %
     433] qed.
     434
    257435 
     436
     437lemma step_cost_event : ∀ge,s,tr,s',obs.
     438  step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
     439  maybe_label ge s obs = intensional_events_of_events tr@obs.
     440#ge #s #tr #s' #obs #ST
     441cases (only_plain_step_events_is_one_cost … (drop_exec_ext … ST))
     442[ * #cl * #E1 #CS whd in ⊢ (??%?);
     443  <RTLabs_as_label >CS destruct %
     444| * #E #CS whd in ⊢ (??%?);
     445  <RTLabs_as_label >CS destruct %
     446] qed.
     447
     448lemma call_ret_event : ∀ge,s,tr,s',obs.
     449  step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
     450  (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) →
     451  maybe_label ge s obs = obs ∧ tr = [ ].
     452#ge * *
     453[ #f #fs #m #S #M #tr #s' #obs #ST * whd in match (as_classify ??);
     454  cases (next_instruction f) normalize
     455  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct
     456| #fid * #fn #args #retdst #stk #m #S #M #tr #s' #obs #ST #_
     457  letin s ≝ (Callstate ??????)
     458  cut (RTLabs_cost_label s = None ?)
     459  [ 1,3: // ] #CS %
     460  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
     461  lapply (drop_exec_ext … ST)
     462  whd in ⊢ (??%? → ?);
     463  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
     464    #E destruct %
     465  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
     466  ]
     467| #v #r * [2: #f #fs ] #m #S #M #tr #s' #obs
     468  letin s ≝ (Returnstate ????) #ST #_
     469  cut (RTLabs_cost_label s = None ?)
     470  [ 1,3: // ] #CS %
     471  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
     472  lapply (drop_exec_ext … ST)
     473  whd in ⊢ (??%? → ?);
     474  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %
     475  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct % | *: normalize #a try #b destruct ] ]
     476  ]
     477| #r #S #M #tr #s' #obs normalize #E destruct
     478] qed.
     479
     480lemma itot_call : ∀C,cs,s,rem,cs',trace.
     481  ∀CL:match cs_classify C s with [ cl_call ⇒ True | _ ⇒ False ].
     482  intensional_trace_of_trace C cs (〈s,E0〉::rem) = 〈cs',trace〉 →
     483  ∃trace'.
     484    trace = (IEVcall (cs_callee C s CL))::trace' ∧
     485    intensional_trace_of_trace C (cs_callee C s CL :: cs) rem = 〈cs',trace'〉.
     486#C #cs #s #rem #cs' #trace #CL
     487whd in ⊢ (??%? → ?);
     488@generalize_callee cases (cs_classify C s) in CL ⊢ %; *
     489#name whd in ⊢ (??%? → ?); cases (intensional_trace_of_trace C (name I::cs) rem)
     490#cs' #trace' #E whd in E:(??%?); destruct %{trace'} % %
     491qed.
     492
     493(* WIP
     494lemma as_call_cs_callee : ∀ge,s,CL,CL'.
     495  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
     496#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
     497destruct cases S in M CL' ⊢ %; [ * ] #fn' #S' * #M1 #M' #CL'
     498whd in ⊢ (??%%); cases (symbol_for_block ??)
     499
     500
     501(* observables_trace_label_label emits the cost label for the first step of the
     502   enclosed tal, so we have to add that label if it exists to the front of the
     503   events from the structured trace *)
     504let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr :
     505  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s'〉 →
     506  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →
     507  pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
     508and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
     509  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 →
     510  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
     511  pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
     512and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
     513  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 →
     514  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
     515  maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
     516[ cases tlr
     517  [ #s1 #s2 #tll @eq_obs_tll
     518  | #s1 #s2 #s3 #tll #tlr #EX #ITOT
     519    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 #EX2 #E
     520    >E in ITOT; #ITOT cases (int_trace_split … ITOT) #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
     521    lapply (eq_end_tll … EX1) #E2 <E2 in EX1; #EX1
     522    cases (eq_obs_tll … EX1 ITOT1) #ITOT1' #CS_CH whd in CS_CH; <CS_CH in ITOT2 EX2; <E2 #ITOT2 #EX2
     523    cases (eq_obs_tlr … EX2 ITOT2) #E3 #E4 destruct % %
     524  ]
     525| cases tll #ends' #s1 #s2 #tal #CS #EX #ITOT whd in ⊢ (?(??%?)?);
     526  whd in ⊢ (?(??(??%?)?)?) ; >(definitely_maybe_label … CS)
     527  @(eq_obs_tal … EX ITOT)
     528| cases tal
     529  [ #s1 #s2 #ST * #CL #CS #EX
     530    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
     531    whd in EX:(??%?); destruct
     532    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?);
     533    whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?);
     534    whd in ⊢ (? → ? → ?(??(???%)?)?);
     535    >CL #call whd in ⊢ (??%? → ?); #E destruct
     536    % [ 1,3: @(step_cost_event … ST') | 2,4: % ]
     537  | #s1 #s2 #ST #CL #EX
     538    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
     539    whd in EX:(??%?); destruct
     540    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?);
     541    whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?);
     542    whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct
     543    cases (call_ret_event … ST')
     544    [ #E1 #E2 >E1 >E2 % %
     545    | skip
     546    | %2 @CL
     547    ]
     548  | #s1 #s2 #s3 #ST #CL #AF #tlr #CS #EX
     549    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
     550    whd in EX:(??%?); destruct cases (call_ret_event … ST')
     551    [ #E1 #E2 >E1 >E2 | skip | %1 @CL ] #ITOT
     552    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ]
     553    #obs' * #E3 #ITOT'
     554    <(as_exec_eq_step … ST ST') in EX; #EX
     555    cases (eq_obs_tlr … EX ITOT')
     556    #OBS' #E4 <E4 %
     557    [ >E3 <OBS' whd in ⊢ (??%?);
     558
     559   
     560   
     561
     562] qed.
     563*)
     564
     565
    258566
    259567(* I'm not entirely certain that existentially quantifying fn is the right thing
    … …  
    295603  ]
    296604| @WCLge
    297 | * #s2' #rem #_ #tlr #STACK #_
     605| * #s2' #rem #_ #tlr #LEN #STACK #_
    298606%{s1'} %{s2'} % [2: %{tlr}
    299607% [ % [ %

  • src/RTLabs/RTLabs_partial_traces.ma

    r2840 r2894  
    106106#ST' whd in ⊢ (??%?); %
    107107qed.
     108
     109let rec length_flat_trace O I ge s (t:flat_trace O I ge s) on t : nat ≝
     110match t with
     111[ ft_stop _ ⇒ 0
     112| ft_step _ _ _ _ t' ⇒ S (length_flat_trace … t')
     113].
    108114
    109115
    … …  
    633639] qed.
    634640
     641(* Measure the number of steps in the structured trace so that we know it's the
     642   same execution that we started with.  TODO: move  *)
     643let rec length_tlr (S:abstract_status) s1 s2 (tlr:trace_label_return S s1 s2) on tlr : nat ≝
     644match tlr with
     645[ tlr_base _ _ tll ⇒ length_tll … tll
     646| tlr_step _ _ _ tll tlr' ⇒ length_tll … tll + length_tlr … tlr'
     647]
     648and length_tll (S:abstract_status) e s1 s2 (tll:trace_label_label S e s1 s2) on tll : nat ≝
     649match tll with
     650[ tll_base _ _ _ tal _ ⇒ length_tal … tal
     651]
     652and length_tal (AS:abstract_status) e s1 s2 (tal:trace_any_label AS e s1 s2) on tal : nat ≝
     653match tal with
     654[ tal_base_not_return _ _ _ _ _ ⇒ 1
     655| tal_base_return _ _ _ _ ⇒ 1
     656| tal_base_call _ _ _ _ _ _ tlr _ ⇒ S (length_tlr … tlr)
     657| tal_base_tailcall _ _ _ _ _ tlr ⇒ S (length_tlr … tlr)
     658| tal_step_call _ _ _ _ _ _ _ _ tlr _ tal' ⇒ S (length_tlr … tlr + length_tal … tal')
     659| tal_step_default _ _ _ _ _ tal' _ _ ⇒ S (length_tal … tal')
     660].
     661
     662
     663
    635664(* Don't need to know that labels break loops because we have termination. *)
    636665
    … …  
    641670  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
    642671  (original_terminates: will_return ge depth start full)
    643   (T:RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
     672  (T:RTLabs_ext_state ge → Type[0]) (length:∀s. T s → nat) (limit:nat) : Type[0] ≝
    644673{
    645674  new_state : RTLabs_ext_state ge;
    … …  
    647676  cost_labelled : well_cost_labelled_state new_state;
    648677  new_trace : T new_state;
     678  tr_length : plus (length … new_trace) (length_flat_trace … remainder) = length_flat_trace … full;
    649679  stack_ok : stack_preserved ge ends start new_state;
    650680  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
    … …  
    661691  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
    662692  (original_terminates: will_return ge depth start full)
    663   (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
     693  (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0])
     694  (length:∀e,s. T e s → nat)
     695  (limit:nat) : Type[0] ≝
    664696{
    665697  ends : trace_ends_with_ret;
    666   trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
     698  trace_res :> trace_result ge depth ends start full original_terminates (T ends) (length ends) limit
    667699}.
    668700
    … …  
    671703   the size of the termination proof might need to be relaxed, too. *)
    672704
    673 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    674   ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
     705definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 →
     706  ∀r:trace_result ge d e s1 t1 TM1 T1 ln1 l1.
    675707    will_return_end … TM1 = will_return_end … TM2 →
    676     T2 (new_state … r) →
     708    ∀trace:T2 (new_state … r).
     709    ln2 (new_state … r) trace + length_flat_trace … (remainder … r) = length_flat_trace … t2 →
    677710    stack_preserved ge e s2 (new_state … r) →
    678     trace_result ge d e s2 t2 TM2 T2 l2 ≝
    679 λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
    680   mk_trace_result ge d e s2 t2 TM2 T2 l2
     711    trace_result ge d e s2 t2 TM2 T2 ln2 l2 ≝
     712λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP.
     713  mk_trace_result ge d e s2 t2 TM2 T2 ln2 l2
    681714    (new_state … r)
    682715    (remainder … r)
    683716    (cost_labelled … r)
    684717    trace
     718    LN
    685719    SP
    686720    ?
    … …  
    691725cases e in r ⊢ %;
    692726[ <TME -TME * cases d in TM1 TM2 ⊢ %;
    693   [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
    694   | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
     727  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); #TMS @TMS
     728  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
    695729    %{TMa} % // @(transitive_le … lGE) @L1
    696730  ]
    697 | <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
     731| <TME -TME * #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %);
    698732   * #TMa * #L1 #TME
    699733    %{TMa} % // @(transitive_le … lGE) @L1
    700734] qed.
    701735
    702 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    703   ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
     736definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 →
     737  ∀r:sub_trace_result ge d s1 t1 TM1 T1 ln1 l1.
    704738    will_return_end … TM1 = will_return_end … TM2 →
    705     T2 (ends … r) (new_state … r) →
     739    ∀trace:T2 (ends … r) (new_state … r).
     740    ? (*XXX matita infers this, but won't check it ?! *) + length_flat_trace … (remainder … r) = length_flat_trace ???? t2 →
    706741    stack_preserved ge (ends … r) s2 (new_state … r) →
    707     sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
    708 λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
    709   mk_sub_trace_result ge d s2 t2 TM2 T2 l2
     742    sub_trace_result ge d s2 t2 TM2 T2 ln2 l2 ≝
     743λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP.
     744  mk_sub_trace_result ge d s2 t2 TM2 T2 ln2 l2
    710745    (ends … r)
    711     (replace_trace … lGE … r TME trace SP).
     746    (replace_trace … lGE … r TME trace LN SP).
    712747
    713748(* Small syntax hack to avoid ambiguous input problems. *)
    714749definition myge : nat → nat → Prop ≝ ge.
     750
     751lemma crappyhack : ∀tlr,rem1,tr,tal,rem2:nat.
     752  tlr+rem1 = tr → tal + rem2 = rem1 → S (tlr + tal) + rem2 = S tr.
     753#tlr #rem1 #tr #tal #rem2 #E1 #E2 destruct <associative_plus %
     754qed.
    715755
    716756let rec make_label_return ge depth (s:RTLabs_ext_state ge)
    … …  
    724764  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
    725765              (trace_label_return (RTLabs_status ge) s)
    726               (will_return_length … TERMINATES) ≝
     766              (length_tlr (RTLabs_status ge) s)
     767              (will_return_length … TERMINATES) ≝
    727768             
    728769match TIME return λTIME. TIME ≥ ? → ? with
    … …  
    737778            TERMINATES
    738779            TIME ? in
    739   match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
    740                             trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
     780  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) (length_tll (RTLabs_status ge) x s) ? →
     781                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) ? (will_return_length … TERMINATES) with
    741782  [ ends_with_ret ⇒ λr.
    742       replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
     783      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) ? (stack_ok … r)
    743784  | doesnt_end_with_ret ⇒ λr.
    744785      let r' ≝ make_label_return ge depth (new_state … r)
    … …  
    749790        replace_trace … r' ?
    750791          (tlr_step (RTLabs_status ge) s (new_state … r)
    751             (new_state … r') (new_trace … r) (new_trace … r')) ?
     792            (new_state … r') (new_trace … r) (new_trace … r')) ??
    752793  ] (trace_res … r)
    753794
    … …  
    765806  on TIME : sub_trace_result ge depth s trace TERMINATES
    766807              (λends. trace_label_label (RTLabs_status ge) ends s)
     808              (λends. length_tll (RTLabs_status ge) ends s)
    767809              (will_return_length … TERMINATES) ≝
    768810             
    … …  
    773815let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
    774816  replace_sub_trace … r ?
    775     (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
     817    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) ? (stack_ok … r)
    776818
    777819] TERMINATES_IN_TIME
    … …  
    787829  on TIME : sub_trace_result ge depth s0 trace TERMINATES
    788830              (λends. trace_any_label (RTLabs_status ge) ends s0)
     831              (λends. length_tal (RTLabs_status ge) ends s0)
    789832              (will_return_length … TERMINATES) ≝
    790833
    791834match TIME return λTIME. TIME ≥ ? → ? with
    792835[ O ⇒ λTERMINATES_IN_TIME. ⊥
    793 | S TIME ⇒ λTERMINATES_IN_TIME.
     836| S TIME ⇒ λTERMINATES_IN_TIME. 
    794837  match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
    795838                                      well_cost_labelled_state s →
    796839                                      ∀TM:will_return ??? trace.
    797840                                      myge ? (times 3 (will_return_length ??? trace TM)) →
    798                                       sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
     841                                      sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (λends. length_tal (RTLabs_status ge) ends s) (will_return_length … TM)
    799842  with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace.
    800843  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
    … …  
    802845                               ∀TM:will_return ??? trace.
    803846                               myge ? (times 3 (will_return_length ??? trace TM)) →
    804                                sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
     847                               sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (λends. length_tal (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
    805848  [ ft_stop st ⇒
    806849      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
    … …  
    809852    let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
    810853    let next' ≝ next_state ? start' ?? EV in
    811     match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     854    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    812855    [ cl_other ⇒ λCL.
    813         match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     856        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    814857        (* We're about to run into a label. *)
    815858        [ true ⇒ λCS.
    816             mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     859            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    817860              doesnt_end_with_ret
    818861              (mk_trace_result ge … next' trace' ?
    819                 (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??)
     862                (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ???)
    820863        (* An ordinary step, keep going. *)
    821864        | false ⇒ λCS.
    822865            let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
    823                 replace_sub_trace ????????????? r ?
     866                replace_sub_trace ??????????????? r ?
    824867                  (tal_step_default (RTLabs_status ge) (ends … r)
    825                      start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?
     868                     start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ??
    826869        ] (refl ??)
    827870       
    828871    | cl_jump ⇒ λCL.
    829         mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     872        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    830873          doesnt_end_with_ret
    831874          (mk_trace_result ge … next' trace' ?
    832             (tal_base_not_return (RTLabs_status ge) start' next' ???) ??)
     875            (tal_base_not_return (RTLabs_status ge) start' next' ???) ???)
    833876           
    834877    | cl_call ⇒ λCL.
    835878        let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
    836         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
     879        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 ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    837880        (* We're about to run into a label, use base case for call *)
    838881        [ true ⇒ λCS.
    839             mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     882            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    840883            doesnt_end_with_ret
    841884            (mk_trace_result ge …
    842885              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
    843                 ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
     886                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ???)
    844887        (* otherwise use step case *)
    845888        | false ⇒ λCS.
    … …  
    850893              (tal_step_call (RTLabs_status ge) (ends … r')
    851894                start' next' (new_state … r) (new_state … r') ? CL ?
    852                 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
     895                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ??
    853896        ] (refl ??)
    854897
    855898    | cl_return ⇒ λCL.
    856         mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     899        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    857900          ends_with_ret
    858           (mk_trace_result ge ???????
     901          (mk_trace_result ge ????????
    859902            next'
    860903            trace'
    861904            ?
    862905            (tal_base_return (RTLabs_status ge) start' next' ? CL)
     906            ?
    863907            ?
    864908            ?)
    … …  
    872916| //
    873917| //
    874 | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
    875 | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
     918| @(tr_length … r)
     919| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #GT #_ @(le_S_to_le … GT)
     920| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #_ #EEQ //
     921| <(tr_length … r) <(tr_length … r') @associative_plus
    876922| @(stack_preserved_join … (stack_ok … r)) //
    877923| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
    878 | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
     924| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #LT #_
    879925  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    880926  @(transitive_le …  (3*(will_return_length … TERMINATES)))
    … …  
    888934| //
    889935| @(proj1 … (RTLabs_costed …)) //
     936| @(tr_length … r)
    890937| @le_S_S_to_le @TERMINATES_IN_TIME
    891938| @(wrl_nonzero … TERMINATES_IN_TIME)
    … …  
    900947| @(will_return_return … CL TERMINATES)
    901948| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     949| %
    902950| %{tr} %{EV} @refl
    903951| @(well_cost_labelled_state_step  … EV) //
    904952| whd @(will_return_notfn … TERMINATES) %2 @CL
    905953| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     954| %
    906955| %{tr} %{EV} %
    907956| %1 whd @CL
    908957| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
    909958| @(well_cost_labelled_state_step  … EV) //
    910 | whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
     959| whd cases (terminates ????????? r) #TMr * #LTr #EQr %{TMr} %
    911960  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
    912961    #TMx * #LT' #_ @LT'
    … …  
    915964  ]
    916965| @(stack_preserved_step ge start' ?? CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
     966| whd in ⊢ (???%); <(tr_length … r) %
    917967| %{tr} %{EV} %
    918968| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
    919969| @(cost_labelled … r)
    920970| skip
    921 | cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
     971| cases r #ns #rm #WS #TLR #SP #LN * #TM * #LT #_ @le_S_to_le
    922972  @(transitive_lt … LT)
    923973  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
    924 | cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
     974| cases r #ns #rm #WS #TLR #SP #LN * #TM * #_ #EQ <EQ
    925975  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
    926976| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
    927977| %{tr} %{EV} %
     978| @(crappyhack ????? (tr_length … r) (tr_length … r'))
    928979| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
    929980| @(cost_labelled … r)
    930 | cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
     981| cases r #H72 #H73 #H74 #H75 #HX #LN * #HY * #GT #H78
    931982  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    932983  cases (will_return_call … TERMINATES) in GT;
    … …  
    947998| whd @(will_return_notfn … TERMINATES) %1 @CL
    948999| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     1000| %
    9491001| %{tr} %{EV} %
    9501002| %2 whd @CL
    … …  
    9541006| @CL
    9551007| %{tr} %{EV} %
     1008| whd in ⊢ (??%%); @eq_f @(tr_length … r)
    9561009| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    9571010| @(well_cost_labelled_state_step  … EV) //
    … …  
    9711024  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    9721025  (TERMINATES: will_return ge depth s trace)
    973   : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
     1026  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (length_tlr (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
    9741027make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
    9751028  (2 + 3 * will_return_length … TERMINATES) ?.
Note: See TracChangeset for help on using the changeset viewer.