Changeset 2896


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

Complete part of measurable to structured subtraces proof that
shows observables are preserved.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2895 r2896  
    4545] (next_state ge s).
    4646//
     47qed.
     48
     49lemma drop_exec_ext : ∀ge,s,tr,s'.
     50  eval_ext_statement ge s = return 〈tr,s'〉 →
     51  eval_statement ge s = return 〈tr,Ras_state … s'〉.
     52#ge #s #tr #s'
     53whd in ⊢ (??%? → ?);
     54letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
     55cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
     56[ // ]
     57generalize in match f; -f
     58cases (eval_statement ge s)
     59[ #o #k #n #N #E whd in E:(??%%); destruct
     60| * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
     61| #m #n #N #E whd in E:(??%%); destruct
     62] qed.
     63
     64lemma as_eval_ext_statement : ∀ge,s,tr,s'.
     65  eval_ext_statement ge s = Value … 〈tr,s'〉 →
     66  as_execute (RTLabs_status ge) s s'.
     67#ge #s #tr #s' #EX
     68whd %{tr} %{(drop_exec_ext … EX)}
     69whd in EX:(??%?);
     70letin ns ≝ (next_state ge s) in EX; #EX
     71change with (ns s' tr ?) in match (next_state ge s s' tr ?);
     72generalize in match (drop_exec_ext ?????);
     73#EX'
     74generalize in match ns in EX ⊢ %; -ns >EX' #ns whd in ⊢ (??%? → %);
     75#E destruct @e1
    4776qed.
    4877
     
    216245qed.
    217246
    218 lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.
     247lemma intensional_state_change_State : ∀ge,cs,f,fs,m.
     248  intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (State f fs m) = 〈cs,[ ]〉.
     249#ge #cs #f #fs #m
     250whd in ⊢ (??%?);
     251generalize in match (cs_callee ??);
     252whd in match (cs_classify ??); cases (next_instruction f) //
     253qed.
     254
     255(* TODO move*)
     256lemma All2_tail : ∀A,B,P,a,b.
     257  All2 A B P a b →
     258  All2 A B P (tail A a) (tail B b).
     259#A #B #P * [2: #ah #at] * [2,4: #bh #bt]
     260* //
     261qed.
     262
     263lemma final_pre_S : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
     264  eval_statement ge s = Value ??? 〈tr,s'〉 →
     265  match s' with [Finalstate _ ⇒ Ras_fn_stack … s = [ ] | _ ⇒ True].
     266#ge #s #tr #s' #EV
     267cases (extend_RTLabs_eval_statement … EV) #S * #M #EV'
     268inversion (eval_preserves_ext … (as_eval_ext_statement … EV'))
     269[ 6: #ge' #r #dst #m #M1 #M2 #E1 #E2 #E3 #E4 destruct whd %
     270| *: #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 try #x15 try #x16 try #x17 try #x18 destruct //
     271] qed.
     272
     273lemma extend_RTLabs_step : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s',cs.
     274  eval_statement ge s = Value … 〈tr,s'〉 →
     275  All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) cs →
     276  ∃S',M'.
     277    eval_ext_statement ge s = Value … 〈tr,mk_RTLabs_ext_state … s' S' M'〉 ∧
     278    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S' (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s')).
     279#ge #s #tr #s' #cs #EV #STACK
     280whd in match (eval_ext_statement ??);
     281letin ns ≝ (next_state ge s)
     282cut (∀s',t,EV. Ras_state … (ns s' t EV) = s' ∧
     283  match s' with
     284   [ State _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s
     285   | Callstate fid _ _ _ _ _ ⇒ ∃b. symbol_for_block … ge b = Some ? fid ∧ Ras_fn_stack … (ns s' t EV) = b::(Ras_fn_stack … s)
     286   | Returnstate _ _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = tail … (Ras_fn_stack … s)
     287   | Finalstate _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s
     288   ])
     289[ #s'' #t #EV' % [ % |
     290    cases s'' in EV' ⊢ %; //
     291    [ #fid #fn #args #ret #fs #m #EV''
     292      %{(func_block_of_exec … EV'')} %
     293      [ cases (func_block_of_exec … EV'') #b * #FS #FFP
     294        @(symbol_for_block_fn … FS FFP)
     295      | %
     296      ]
     297    | #r #EV whd lapply (final_pre_S … EV) whd in ⊢ (% → ?); #E >E %
     298    ]
     299  ]
     300]
     301generalize in match ns; -ns
     302>EV #next #NEXT cases (NEXT … (refl ??))
     303lapply (refl ? (next s' tr (refl ??)))
     304cases (next s' tr ?) in ⊢ (???% → ?);
     305#s'' #S'' #M''
     306#Enext1 >Enext1 #Enext2 destruct #Snext %{S''} %{M''}
     307%
     308[ whd in ⊢ (??%%); >Enext1 %
     309| cases s' in Snext ⊢ %;
     310  [ #f #fs #m whd in ⊢ (% → ?); #E destruct
     311    >intensional_state_change_State @STACK
     312  | #fid #fn #args #ret #fs #m whd in ⊢ (% → ?); * #b * #SYM #ES destruct
     313    whd in match (intensional_state_change ???);
     314    whd in match (cs_callee ???);
     315    % [ @SYM | @STACK ]
     316  | #rv #rr #fs #m whd in ⊢ (% → ?); #ES destruct
     317    whd in match (intensional_state_change ???);
     318    >(?:\fst ? = tail ? cs)
     319    [2: cases cs // ]
     320    @All2_tail
     321    @STACK
     322  | #r whd in ⊢ (% → ?); #E destruct
     323    whd in match (intensional_state_change ???);
     324    @STACK
     325  ]
     326] qed.
     327   
     328   
     329lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace.
    219330  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
    220   ∃trace',S,M. exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉.
     331  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs trace = 〈cs',itrace〉 →
     332  All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (Ras_state … s))) →
     333  ∃trace',S,M.
     334    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
     335    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
    221336#ge #n0 elim n0
    222 [ #s #trace #s' #E whd in E:(??%%); destruct %{[ ]} cases s #s' #S #M
    223   %{S} %{M} %
    224 | #n #IH #s #trace #s' #EX
     337[ * #s #S #M #trace #s' #cs #cs' #itrace #E whd in E:(??%%); destruct
     338  #E whd in E:(??%%); destruct
     339  #CS %{[ ]}
     340  %{S} %{M} % [ % | @CS ]
     341| #n #IH * #s #S #M #trace #s' #cs #cs' #itrace #EX
    225342  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
    226   lapply (refl ? (eval_ext_statement ge s))
    227   whd in ⊢ (???% → ?);
    228   change with (eval_statement ge s) in STEP:(??%?);
    229   letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
    230   cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
    231   [ // ]
    232   generalize in match f; -f
    233   >STEP #next #NEXT whd in ⊢ (???% → ?); letin s1' ≝ (next s1 tr ?) #STEP'
    234   <(NEXT … (refl ??)) in EX'; #EX'
    235   cases (IH s1' … EX')
    236   #tl' * #S'' * #M'' #STEPS''
    237   %{(〈s,tr〉::tl')} %{S''} %{M''}
    238   whd in ⊢ (??%?);
    239   change with (RTLabs_is_final s) in match (is_final ?????);
    240   change with (RTLabs_is_final s) in match (is_final ?????) in NF;
    241   >NF whd in ⊢ (??%?);
    242   change with (eval_ext_statement ??) in match (step ?????);
    243   >STEP' whd in ⊢ (??%?);
    244   >STEPS'' %
    245 ] qed.
     343  >E whd in ⊢ (??%? → ?); @pair_elim #cs1 #itrace1 #ITOT1
     344  whd in ⊢ (??%? → ?); @pair_elim #cs2 #itrace2 #ITOT2 #E' destruct
     345  #STACK
     346  cases (extend_RTLabs_step ge (mk_RTLabs_ext_state ge s S M) ??? STEP STACK)
     347  #S' * #M' * #STEP' #STACK'
     348  cases (IH (mk_RTLabs_ext_state ge s1 S' M') … EX' ITOT2 STACK')
     349  #tl' * #S'' * #M'' * #EX'' #STACK''
     350  %{(〈mk_RTLabs_ext_state … s S M,tr〉::tl')} %{S''} %{M''}
     351  %
     352  [ whd in ⊢ (??%?);
     353    change with (RTLabs_is_final s) in match (is_final ?????);
     354    change with (RTLabs_is_final s) in match (is_final ?????) in NF;
     355    >NF whd in ⊢ (??%?);
     356    change with (eval_ext_statement ??) in match (step ?????);
     357    >STEP' whd in ⊢ (??%?);
     358    >EX'' %
     359  | @STACK''
     360  ]
     361] qed.
     362
     363lemma extend_initial_RTLabs_exec_steps : ∀p. let ge ≝ make_global p in ∀n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs',itrace.
     364  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
     365  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) [ ] trace = 〈cs',itrace〉 →
     366  make_ext_initial_state p = OK ? s →
     367  ∃trace',S,M.
     368    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
     369    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
     370#p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT
     371@(extend_RTLabs_exec_steps … EXEC ITOT)
     372cases (bind_inversion ????? INIT) -INIT #m * #E1 #INIT
     373cases (bind_as_inversion ????? INIT) -INIT #b * #Eb #INIT
     374cases (bind_as_inversion ????? INIT) -INIT #f * #Ef #INIT
     375whd in INIT:(??%%); lapply (Ras_fn_match … s) destruct
     376* * #FS #FFP #_
     377% [ >(symbol_for_block_fn … FS FFP) % | % ]
     378qed.
    246379
    247380lemma label_to_return_state_labelled : ∀C,n,s,trace,s'.
     
    304437lemma as_exec_eq_step : ∀ge,s1,s2,tr,s2'.
    305438  as_execute (RTLabs_status ge) s1 s2 →
    306   step io_out io_in RTLabs_ext_fullexec ge s1 = Value ??? 〈tr,s2'〉 →
    307   s2 = s2'.
    308 #ge #s1 #s2 #tr #s2' * #tr * #EX
    309 whd in ⊢ (? → ??%? → ?);
    310 letin f ≝ (next_state ge s1) change with (f (Ras_state … s2) tr EX) in ⊢ (??%? → ?);
    311 generalize in ⊢ (??(%???)? → ??(?%)? → ?); >EX in ⊢ (% → % → ??(match % with [_⇒?|_⇒?|_⇒?]?)? → ?);
    312 #next #NEXT whd in ⊢ (??%? → ?); #E destruct >NEXT %
     439  step io_out io_in RTLabs_fullexec ge (Ras_state … s1) = Value ??? 〈tr,s2'〉 →
     440  Ras_state … s2 = s2'.
     441#ge #s1 #s2 #tr #s2' * #tr * #EX #NX
     442change with (eval_statement ge (Ras_state … s1)) in ⊢ (??%? → ?); >EX #E destruct
     443%
    313444qed.
    314445
     
    316447
    317448let rec eq_end_tlr ge s trace' s' tlr s'' on tlr :
    318   exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
    319   s' = s'' ≝ ?
     449  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
     450  (Ras_state … s') = s'' ≝ ?
    320451and eq_end_tll ge s trace' s' ends tll s'' on tll :
    321   exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
    322   s' = s'' ≝ ?
     452  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
     453  (Ras_state … s') = s'' ≝ ?
    323454and eq_end_tal ge s trace' s' ends tal s'' on tal :
    324   exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
    325   s' = s'' ≝ ?.
     455  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
     456  (Ras_state … s') = s'' ≝ ?.
    326457[ cases tlr
    327458  [ #s1 #s2 #tll @eq_end_tll
     
    413544] qed.
    414545
    415 lemma drop_exec_ext : ∀ge,s,tr,s'.
    416   eval_ext_statement ge s = return 〈tr,s'〉 →
    417   eval_statement ge s = return 〈tr,Ras_state … s'〉.
    418 #ge #s #tr #s'
    419 whd in ⊢ (??%? → ?);
    420 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
    421 cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
    422 [ // ]
    423 generalize in match f; -f
    424 cases (eval_statement ge s)
    425 [ #o #k #n #N #E whd in E:(??%%); destruct
    426 | * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
    427 | #m #n #N #E whd in E:(??%%); destruct
    428 ] qed.
    429 
    430546lemma RTLabs_as_label : ∀ge,s.
    431547  RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s.
     
    448564
    449565lemma step_cost_event : ∀ge,s,tr,s',obs.
    450   step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
     566  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
    451567  maybe_label ge s obs = intensional_events_of_events tr@obs.
    452568#ge #s #tr #s' #obs #ST
    453 cases (only_plain_step_events_is_one_cost … (drop_exec_ext … ST))
     569cases (only_plain_step_events_is_one_cost … ST)
    454570[ * #cl * #E1 #CS whd in ⊢ (??%?);
    455571  <RTLabs_as_label >CS destruct %
     
    470586
    471587lemma call_ret_event : ∀ge,s,tr,s',obs.
    472   step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
     588  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
    473589  (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) →
    474590  maybe_label ge s obs = obs ∧ tr = [ ].
     
    482598  [ 1,3: // ] #CS %
    483599  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
    484   lapply (drop_exec_ext … ST)
     600  lapply ST
    485601  whd in ⊢ (??%? → ?);
    486602  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
     
    493609  [ 1,3: // ] #CS %
    494610  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
    495   lapply (drop_exec_ext … ST)
     611  lapply ST
    496612  whd in ⊢ (??%? → ?);
    497613  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %
     
    502618
    503619lemma as_call_cs_callee : ∀ge,s,CL,CL'.
    504   as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
     620  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcsys ge) (Ras_state … s) CL'.
    505621#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
    506622destruct %
     
    514630    intensional_trace_of_trace C (cs_callee C s CL :: cs) rem = 〈cs',trace'〉.
    515631#C #cs #s #rem #cs' #trace #CL
    516 whd in ⊢ (??%? → ?);
     632whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
    517633@generalize_callee cases (cs_classify C s) in CL ⊢ %; *
    518634#name whd in ⊢ (??%? → ?); cases (intensional_trace_of_trace C (name I::cs) rem)
     
    522638lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs.
    523639  as_classifier (RTLabs_status ge) s cl_other →
    524   step … RTLabs_ext_pcsys ge s = Value ??? 〈tr,s'〉 →
    525   intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs (〈s,tr〉::rem) = 〈cs',obs〉 →
     640  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
     641  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs (〈Ras_state … s,tr〉::rem) = 〈cs',obs〉 →
    526642  ∃obs'.
    527643    obs = (intensional_events_of_events tr) @ obs' ∧
    528     intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs rem = 〈cs',obs'〉.
     644    intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs rem = 〈cs',obs'〉.
    529645#ge #cs #s #tr #s' #rem #cs #obs #CL #EX
    530 whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (% → ?);
    531 whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_ext_pcsys ge) ?) in CL:(??%?);
     646whd in ⊢ (??%? → ?);
     647whd in match (intensional_state_change (pcs_to_cs RTLabs_pcsys ge) ??);
     648generalize in match (cs_callee ??) in ⊢ (% → ?);
     649whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcsys ge) ?) in CL:(??%?);
    532650>CL #name whd in ⊢ (??%? → ?);
    533651cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct
     
    539657   events from the structured trace *)
    540658let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr :
    541   exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s'〉 →
    542   intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →
     659  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 →
     660  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →
    543661  pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
    544662and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
    545   exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 →
    546   intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
     663  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
     664  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
    547665  pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
    548666and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
    549   exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 →
    550   intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
     667  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
     668  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
    551669  maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
    552670[ cases tlr
     
    566684    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
    567685    whd in EX:(??%?); destruct
    568     whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?);
    569     whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?);
     686    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
     687    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
     688    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
    570689    whd in ⊢ (? → ? → ?(??(???%)?)?);
    571690    >CL #call whd in ⊢ (??%? → ?); #E destruct
     
    574693    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
    575694    whd in EX:(??%?); destruct
    576     whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?);
    577     whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?);
     695    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
     696    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
     697    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
    578698    whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct
    579699    cases (call_ret_event … ST')
     
    586706    whd in EX:(??%?); destruct cases (call_ret_event … ST')
    587707    [ #E1 #E2 >E1 >E2 | skip | %1 @CL ] #ITOT
    588     cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ]
     708    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
    589709    #obs' * #E3 #ITOT'
    590710    <(as_exec_eq_step … ST ST') in EX; #EX
     
    599719    cases (call_ret_event … ST')
    600720    [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT
    601     cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ]
     721    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
    602722    #obs' * #E4 #ITOT'
    603723    <(as_exec_eq_step … ST ST') in EX; #EX
     
    649769] qed.
    650770
     771lemma cost_state_intensional_state_change : ∀ge,s,cs.
     772  RTLabs_cost s →
     773  \fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s) = cs.
     774#ge *
     775[ #f #fs #m #cs //
     776| #fid #fn #args #ret #fs #m #cs *
     777| #rv #rr #fs #m #cs *
     778| #r #cs *
     779] qed.
     780
     781
    651782
    652783(* I'm not entirely certain that existentially quantifying fn is the right thing
     
    676807whd in ⊢ (??%? → ?); >EXEC1
    677808whd in ⊢ (??%? → ?); >EXEC2
    678 whd in ⊢ (??%? → ?); @breakup_pair #E whd in E:(??%%); destruct
     809whd in ⊢ (??%? → ?);
     810@pair_elim #cs1 #prefix1 #ITOT1
     811lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting'))
     812cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting') in ⊢ (???% → %);
     813#cs2 #interesting'' #ITOT2
     814#E whd in E:(??%%); destruct
    679815cases (initial_states_OK' … INIT) #S * #M #INIT'
    680 cases (extend_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1)
    681 #prefix'' * #S1 * #M1
     816cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT')
     817#prefix'' * #S1 * #M1 *
    682818lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
    683819lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
    684 letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1'
     820letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #CALLSTACK1
     821cut (∃cs1'. cs1 = fn::cs1')
     822[ >(cost_state_intensional_state_change … CS1) in CALLSTACK1;
     823  cases cs1 [ * ] #fn' #cs1' * >FN #Efn destruct #_ %{cs1'} %
     824] * #cs1' #Ecs destruct
    685825cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END
    686826lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
     
    712852      <plus_n_O @(λx.x) ]
    713853    #LEN' <LEN' in EXEC2; #EXEC2
    714     cases (extend_RTLabs_exec_steps ?? s1' … EXEC2) #interesting'''
    715     lapply (eq_obs_tlr ????????? EXEC2)
     854    lapply (eq_obs_tlr ????????? EXEC2 ITOT2)
     855    * //
    716856  ]
    717857]]
  • src/common/Globalenvs.ma

    r2895 r2896  
    458458| % #E destruct
    459459] qed.
     460
     461(* For *functions* the mapping between identifiers and blocks is a bijection,
     462   but to show that we have to keep more invariants about the environment. *)
     463axiom symbol_for_block_fn : ∀F,genv,b,f,id.
     464  find_symbol F genv id = Some ? b →
     465  find_funct_ptr F genv b = Some ? f →
     466  symbol_for_block F genv b = Some ? id.
    460467
    461468(* The mapping of blocks to symbols is total for functions. *)
  • src/common/Measurable.ma

    r2800 r2896  
    4242λtr. flatten ? (map ?? intensional_event_of_event tr).
    4343
     44definition intensional_state_change ≝
     45λC,callstack,s.
     46    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
     47    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
     48    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
     49    | _ ⇒ λ_. 〈callstack, [ ]〉
     50    ] (cs_callee C s).
     51
    4452let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
    4553match trace with
     
    4755| cons str tl ⇒
    4856  let 〈s,tr〉 ≝ str in
    49   let 〈callstack, call_event〉 ≝
    50     match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
    51     [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
    52     | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
    53     | _ ⇒ λ_. 〈callstack, [ ]〉
    54     ] (cs_callee C s) in
     57  let 〈callstack, call_event〉 ≝ intensional_state_change C callstack s in
    5558  let other_events ≝ intensional_events_of_events tr in
    5659  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
     
    7376      〈stk', (intensional_events_of_events tr)@tl〉).
    7477#C #callstack #s #tr #trace #NORMAL
    75 whd in ⊢ (??%?);
     78whd in ⊢ (??%?); whd in match (intensional_state_change ???);
    7679generalize in match (cs_callee C s);
    7780cases (normal_state_inv … NORMAL)
     
    141144| * #s #tr #tl #IH
    142145  #callstack
    143   whd in match (intensional_trace_of_trace ???);
    144   whd in match (intensional_trace_of_trace ???);
     146  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
     147  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
    145148  generalize in match (cs_callee C s);
    146149  cases (cs_classify C s)
     
    185188#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E
    186189whd
    187 whd in ⊢ (??%%); normalize nodelta
     190whd in ⊢ (??%%);
     191whd in match (intensional_state_change ???);
     192whd in match (intensional_state_change C' ??);
     193normalize nodelta
    188194generalize in match (cs_callee C s); generalize in match (cs_callee C' s');
    189195>CL >CL' normalize nodelta #_ #_
     
    223229#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
    224230whd in ⊢ (? → ? → %);
    225 whd in ⊢ (? → ? → ??%%); normalize nodelta
     231whd in ⊢ (? → ? → ??%%);
     232whd in match (intensional_state_change ???);
     233whd in match (intensional_state_change C' ??);
     234normalize nodelta
    226235@generalize_callee
    227236@generalize_callee
Note: See TracChangeset for help on using the changeset viewer.