Changeset 2948


Ignore:
Timestamp:
Mar 24, 2013, 9:17:42 PM (4 years ago)
Author:
campbell
Message:

Finish up measurable to structured proof, exposing the prefix and keeping
reasoning about the stack space purely in terms of the preserved
observables.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2947 r2948  
    280280  ]
    281281] qed.
    282    
    283    
     282
     283lemma callee_ext : ∀ge,s,S,M.
     284  cs_callee (pcs_to_cs RTLabs_pcsys ge) s = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) (mk_RTLabs_ext_state ge s S M).
     285#ge * //
     286qed.
     287
     288lemma int_state_change_ext : ∀ge,cs,s,S,M.
     289  intensional_state_change (pcs_to_cs RTLabs_pcsys ge) cs s =
     290  intensional_state_change (pcs_to_cs RTLabs_ext_pcsys ge) cs (mk_RTLabs_ext_state ge s S M).
     291#ge #cs #s #S #M
     292whd in ⊢ (??%%);
     293<callee_ext %
     294qed.
     295
    284296lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace.
    285297  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
     
    288300  ∃trace',S,M.
    289301    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
     302    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs trace' = 〈cs',itrace〉 ∧
    290303    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
    291304#ge #n0 elim n0
     
    293306  #E whd in E:(??%%); destruct
    294307  #CS %{[ ]}
    295   %{S} %{M} % [ % | @CS ]
     308  %{S} %{M} % [ % [ % | % ] | @CS ]
    296309| #n #IH * #s #S #M #trace #s' #cs #cs' #itrace #EX
    297310  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
     
    302315  #S' * #M' * #STEP' #STACK'
    303316  cases (IH (mk_RTLabs_ext_state ge s1 S' M') … EX' ITOT2 STACK')
    304   #tl' * #S'' * #M'' * #EX'' #STACK''
     317  #tl' * #S'' * #M'' * * #EX'' #ITOT'' #STACK''
    305318  %{(〈mk_RTLabs_ext_state … s S M,tr〉::tl')} %{S''} %{M''}
    306   %
     319  % [ %
    307320  [ whd in ⊢ (??%?);
    308321    change with (RTLabs_is_final s) in match (is_final ?????);
     
    312325    >STEP' whd in ⊢ (??%?);
    313326    >EX'' %
    314   | @STACK''
     327  | whd in ⊢ (??%?); <int_state_change_ext >ITOT1
     328    whd in ⊢ (??%?); >ITOT'' %
     329 ]| @STACK''
    315330  ]
    316331] qed.
     
    322337  ∃trace',S,M.
    323338    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
     339    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) [ ] trace' = 〈cs',itrace〉 ∧
    324340    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
    325341#p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT
     
    724740] qed.
    725741
    726 definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → stacksize_info → stacksize_info ≝
    727 λS,s1,s2,tlr,stack_cost,currentfn,initial.
    728   update_stacksize_info stack_cost initial (extract_call_ud_from_tlr S s1 s2 tlr currentfn).
    729 
     742(* TODO: move to somewhere common *)
     743definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝
     744λC,p,m.
     745  let g ≝ make_global … (pcs_exec … C) p in
     746  let C' ≝ pcs_to_cs C g in
     747  ! s0 ← make_initial_state … p;
     748  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
     749  return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉.
    730750
    731751
     
    740760  measurable RTLabs_pcsys p m n stack_cost max →
    741761  observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
    742   let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in
    743762  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
    744   state_at RTLabs_ext_pcsys p m = return sm
     763  exec_steps_with_obs RTLabs_ext_pcsys p m = return 〈sm, prefix〉
    745764  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    746   le (maximum (max_stack_of_tlr ??? tlr stack_cost fn midstack)) max ∧
     765  le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧
    747766  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
    748767#p #m #n #stack_cost #max #prefix #interesting
     
    752771* #s0 * #prefix' * #s1 * #interesting' * #s2
    753772letin ge ≝ (make_global … RTLabs_fullexec p)
    754 * * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #STACK
     773* * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #MAXSTACK
    755774whd in ⊢ (??%? → ?); >INIT
    756775whd in ⊢ (??%? → ?); >EXEC1
     
    764783cases (initial_states_OK' … INIT) #S * #M #INIT'
    765784cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT')
    766 #prefix'' * #S1 * #M1 *
     785#prefix'' * #S1 * #M1 * *
    767786lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
    768787lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
    769 letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #CALLSTACK1
     788letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #ITOT1' #CALLSTACK1
    770789cut (∃cs1'. cs1 = fn::cs1')
    771790[ >(cost_state_intensional_state_change … CS1) in CALLSTACK1;
     
    788807    change with (make_ext_initial_state p) in match (make_initial_state ????);
    789808    >INIT' whd in ⊢ (??%?);
    790     >EXEC1' %
     809    >EXEC1' whd in ⊢ (??%?); >ITOT1' %
    791810  | @tlr_sound_unrepeating
    792811    [ @SLge
     
    796815      ]
    797816    ]
    798  ]|
     817 ]| >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x)
    799818 ]| cut (length_tlr … tlr = n)
    800819    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
     
    804823    * //
    805824  ]
    806 ]
    807 
     825] qed.
     826
Note: See TracChangeset for help on using the changeset viewer.