Changeset 3156


Ignore:
Timestamp:
Apr 17, 2013, 3:24:22 PM (4 years ago)
Author:
campbell
Message:

Rebuild prefix traces in back-end's preferred form.

Location:
src
Files:
1 deleted
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r3145 r3156  
    624624] qed.
    625625
    626 (* TODO: move to somewhere common *)
    627 definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝
    628 λC,p,m.
    629   let g ≝ make_global … (pcs_exec … C) p in
    630   let C' ≝ pcs_to_cs C g in
    631   ! s0 ← make_initial_state … p;
    632   ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
    633   return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉.
    634 
    635 
    636 (* I'm not entirely certain that existentially quantifying fn is the right thing
    637    to do.  In principle we must provide the right one to satisfy the condition
    638    about observables, but perhaps we ought to show how to produce it explicitly.
    639    *)
    640 
     626(* We need to put the prefix of the measurable trace into the back-end's
     627   preferred form of flat trace.  For some reason this is backwards.
     628   
     629   As well as forming the trace itself, we need to show that the definition
     630   for extracting observables and the call stack for stack space gives the same
     631   answer, and that a side condition from the fact that the program is well cost
     632   labelled is fulfilled (I don't think that is strictly necessary, but allows
     633   the simulation results for structured traces to be reused for the flat
     634   ones). *)
     635
     636include "common/StatusSimulation.ma".
     637
     638(* Backwards version of exec_steps_S *)
     639
     640lemma exec_steps_snoc_inv : ∀O,I,fx,g,n,s,trace,s''.
     641  exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 →
     642  ∃tr',s',liat.
     643    is_final … fx g s' = None ? ∧
     644    trace = liat@[〈s',tr'〉] ∧
     645    step … fx g s' = Value … 〈tr',s''〉 ∧
     646    exec_steps n O I fx g s = OK … 〈liat,s'〉.
     647#O #I #fx #g #n elim n
     648[ #s #trace #s''
     649  whd in ⊢ (??%? → ?);
     650  lapply (refl ? (is_final … s))
     651  cases (is_final … s) in ⊢ (???% → %);
     652  [ #NF | #r #F #EXEC whd in EXEC:(??%%); destruct ]
     653  whd in ⊢ (??%? → ?);
     654  lapply (refl ? (step … s))
     655  cases (step … s) in ⊢ (???% → %);
     656  [ #o #k #_ #EXEC whd in EXEC:(??%%); destruct | 3: #m #_ #EXEC whd in EXEC:(??%%); destruct ]
     657  * #tr' #s' #STEP whd in ⊢ (??%% → ?); #E destruct
     658  %{tr'} %{s} %{[ ]} % [ % [ % [ @NF | % ] | @STEP ] | % ]
     659| #m #IH
     660  #s #trace #s''
     661  whd in ⊢ (??%? → ?);
     662  lapply (refl ? (is_final … s))
     663  cases (is_final … s) in ⊢ (???% → %);
     664  [ #NF | #r #F #EXEC whd in EXEC:(??%%); destruct ]
     665  whd in ⊢ (??%? → ?);
     666  lapply (refl ? (step … s))
     667  cases (step … s) in ⊢ (???% → %);
     668  [ #o #k #_ #EXEC whd in EXEC:(??%%); destruct | 3: #m #_ #EXEC whd in EXEC:(??%%); destruct ]
     669  * #tr' #s' #STEP whd in ⊢ (??%% → ?);
     670  lapply (refl ? (exec_steps (S m) O I fx g s')) cases (exec_steps … s') in ⊢ (???% → %);
     671  [2: #m #_ #E whd in E:(??%?); destruct ]
     672  * #trace' #s''' #EXEC' #E whd in E:(??%%); destruct
     673  cases (IH … EXEC') #tr'' * #s''' * #liat * * * #NF' #E destruct #STEP' #EXEC''
     674  %{tr''} %{s'''} %{(〈s,tr'〉::liat)} % [ % [ % [ @NF' | % ] | @STEP' ]|
     675    whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >EXEC'' %
     676  ]
     677] qed.
     678
     679lemma RTLabs_step_tr_matches_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
     680  eval_statement ge s = Value … 〈tr,s'〉 →
     681  intensional_events_of_events tr = option_to_list … (! l ← as_label (RTLabs_status ge) s; return IEVcost l).
     682#ge #s #tr #s' #EV
     683cases (only_plain_step_events_is_one_cost … EV)
     684[ * #cl * #E1 #CS >E1 <RTLabs_as_label >CS %
     685| * #E1 >E1 #CS <RTLabs_as_label >CS %
     686] qed.
     687
     688lemma RTLabs_return_not_label : ∀ge,s.
     689  as_classify (RTLabs_status ge) s = cl_return →
     690  as_label … s = None ?.
     691#ge * *
     692[ #f #fs #m #S #M whd in ⊢ (??%? → ?); cases (next_instruction f) normalize nodelta #a try #b try #c try #d try #e try #f try #g try #h try #i destruct
     693| #a #b #c #d #e #f #g #h #E whd in E:(??%?); destruct
     694| #a #b #c #d * [2: #e #f] #g #h %
     695| //
     696] qed.
     697
     698lemma RTLabs_call_not_label : ∀ge,s.
     699  as_classify (RTLabs_status ge) s = cl_call →
     700  as_label … s = None ?.
     701#ge * *
     702[ #f #fs #m #S #M whd in ⊢ (??%? → ?); cases (next_instruction f) normalize nodelta #a try #b try #c try #d try #e try #f try #g try #h try #i destruct
     703| #a #b #c #d #e #f * [*] #g #h #i #j %
     704| #a #b #c #d * [2: #e #f] #g #h %
     705| //
     706] qed.
     707
     708(* The main part of showing the the observables and call stack are the same. *)
     709
     710lemma extend_ft_stack_observables : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀ft,cs',cs,itr,itr',tr,H1,H2.
     711  eval_statement ge s2 = Value … 〈tr,s3〉 →
     712  ft_stack_observables (RTLabs_status ge) s1 s2 ft = 〈cs',itr'〉 →
     713  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcs ge) cs' [〈s2,tr〉] = 〈cs,itr〉 →
     714  ft_stack_observables (RTLabs_status ge) s1 s3 (ft_advance (RTLabs_status ge) s1 s2 s3 ft H1 H2) = 〈cs,itr'@itr〉.
     715#ge #s1 #s2 #s3 #ft #cs' #cs #itr #itr' #tr #H1 #H2 #EVAL #FT
     716whd in ⊢ (??%? → ?); @pair_elim #cs1 #itr1 #ITR1
     717whd in ⊢ (??%? → ?); #ITR2 destruct >(RTLabs_step_tr_matches_label … EVAL) >append_nil
     718whd in ⊢ (??%?); >FT -FT
     719whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); cases (as_classify (RTLabs_status ge) s2) in ⊢ (???% → %);
     720#CL whd in ⊢ (??%?);
     721[ cases cs' in ITR1 ⊢ %; [2: #fn #cs1 ]
     722  whd in ⊢ (??%? → ??%?);
     723  generalize in ⊢ (??(?%)? → ?);
     724  change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??);
     725  >CL #f whd in ⊢ (??%? → ?); #E destruct >(RTLabs_return_not_label … CL) %
     726| whd in ITR1:(??%?); lapply ITR1 generalize in ⊢ (??(?%)? → ?);
     727  change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??);
     728  >CL #f whd in ⊢ (??%? → ?); #E destruct %
     729| cut (match cs_classify (pcs_to_cs RTLabs_ext_pcs ge) s2 with [ cl_call ⇒ True | _ ⇒ False ])
     730  [ change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??); >CL % ]
     731  #CL'
     732  >(as_call_cs_callee … CL') change with (cs_callee (pcs_to_cs RTLabs_ext_pcs ge) s2 CL') in match (cs_callee ???);
     733  whd in ITR1:(??%?); lapply ITR1 @(generalize_callee … CL')
     734  change with (cs_classify (pcs_to_cs RTLabs_ext_pcs ge) s2) in match (as_classify ??) in CL;
     735  >CL in CL' ⊢ %; * #f whd in ⊢ (
     736  ??%? → ?); #E destruct
     737  >(RTLabs_call_not_label ?? CL) %
     738| cases (RTLabs_notail … CL)
     739| whd in ITR1:(??%?); lapply ITR1 generalize in ⊢ (??(?%)? → ?);
     740  change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??);
     741  >CL #f whd in ⊢ (??%? → ?); #E destruct %
     742] qed.
     743
     744(* The side condition concerning cost labelling. *)
     745
     746lemma RTLabs_enforce_costedness : ∀ge,tr. ∀s,s':RTLabs_ext_state ge.
     747  well_cost_labelled_state (Ras_state … s) →
     748  eval_statement ge s = Value … 〈tr,s'〉 →
     749  enforce_costedness (RTLabs_status ge) s s'.
     750#ge #tr #s #s' #WCL #EVAL
     751lapply (well_cost_labelled_jump … EVAL WCL)
     752whd in ⊢ (? → %); whd in match (is_cl_jump ??);
     753change with (RTLabs_classify s) in match (as_classify ??);
     754cases (RTLabs_classify s) //
     755#H @(proj1 … (RTLabs_costed …)) @H %
     756qed.
     757
     758lemma well_cost_labelled_exec_ext_steps : ∀n,g. ∀s:RTLabs_ext_state g.∀trace.∀s':RTLabs_ext_state g.
     759  well_cost_labelled_ge g →
     760  exec_steps n ?? RTLabs_ext_fullexec g s = OK ? 〈trace,s'〉 →
     761  well_cost_labelled_state s →
     762  well_cost_labelled_state s'.
     763#n #g elim n
     764[ #s #trace #s' #_ #E whd in E:(??%%); destruct //
     765| #m #IH #s #trace #s' #WCLge #EX
     766  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
     767  #WCLs @(IH … WCLge … EX')
     768  @(well_cost_labelled_state_step … (drop_exec_ext … STEP) WCLge WCLs)
     769] qed.
     770
     771lemma build_back_end_flat_trace : ∀ge,n,s0,tr,s1,cs,itr.
     772  exec_steps n … RTLabs_ext_fullexec ge s0 = return 〈tr,s1〉 →
     773  well_cost_labelled_ge ge →
     774  well_cost_labelled_state (Ras_state … s0) →
     775  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcs ge) [ ] tr = 〈cs,itr〉 →
     776  ∃ft:flat_trace (RTLabs_status ge) s0 s1.
     777    ft_stack_observables … ft = 〈cs,itr〉.
     778#ge #n elim n
     779[ #s0 #tr #s1 #cs #itr #EXEC #_ #_ #ITOT
     780  whd in EXEC:(??%%); destruct whd in ITOT:(??%%); destruct
     781  %{(ft_start …)} %
     782| #m #IH #s0 #tr #s1 #cs #itr #EXEC #WCLge #WCL0
     783  cases (exec_steps_snoc_inv … EXEC)
     784  #tr' * #s' * #liat * * * #NF #E #STEP #EXEC' destruct
     785  >int_trace_append' @pair_elim #cs1 #itr1 @pair_elim #cs2 #itr2 #ITOT2 #ITOT1
     786  #E destruct
     787  cases (IH … EXEC' WCLge WCL0 ITOT1)
     788  #ft #FT %{(ft_advance … ft ??)}
     789  [ @(RTLabs_enforce_costedness … (drop_exec_ext … STEP))
     790    @(well_cost_labelled_exec_ext_steps … EXEC') //
     791  | @(as_eval_ext_statement … STEP)
     792  | @(extend_ft_stack_observables … FT ITOT2) @drop_exec_ext @STEP
     793  ]
     794] qed.
     795
     796
     797(* Now bring the parts together. *)
    641798
    642799theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting.
     
    644801  measurable RTLabs_pcs p m n stack_cost max →
    645802  observables RTLabs_pcs p m n = return 〈prefix,interesting〉 →
    646   ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
    647   exec_steps_with_obs RTLabs_ext_pcs p m = return 〈sm, prefix〉 ∧
     803  ∃s0,sm,sn,fn.
     804  make_ext_initial_state p = return s0 ∧
     805  ∃ft:flat_trace (RTLabs_status (make_global p)) s0 sm.
     806  ft_current_function … ft = Some … fn ∧
     807  ft_observables … ft = prefix ∧
     808  ∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
    648809  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    649810  le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧
     
    686847| * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?);
    687848>RETURNS_END #E destruct
    688 %{s1'} %{s2'} %{fn} %{tlr}
    689 % [ % [ %
    690   [ whd in ⊢ (??%?);
    691     change with (make_ext_initial_state p) in match (make_initial_state ????);
    692     >INIT' whd in ⊢ (??%?);
    693     >EXEC1' whd in ⊢ (??%?); >ITOT1' %
    694   | @tlr_sound_unrepeating
     849%{(mk_RTLabs_ext_state (make_global p) s0 S M)} %{s1'} %{s2'} %{fn} %{INIT'}
     850cases (build_back_end_flat_trace … EXEC1' WCLge ? ITOT1')
     851[2: @(proj1 … (well_cost_labelled_initial … INIT WCLP)) ]
     852#ft #FTobs %{ft} % [ % [ whd in ⊢ (??%?); whd in match (ft_stack ????); >FTobs % | whd in ⊢ (??%?); >FTobs % ] ]
     853%{tlr}
     854% [ %
     855  [ @tlr_sound_unrepeating
    695856    [ @SLge
    696857    | @(soundly_labelled_exec_steps … EXEC1)
     
    699860      ]
    700861    ]
    701  ]| >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x)
     862  | >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x)
    702863 ]| cut (length_tlr … tlr = n)
    703864    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
     
    708869  ]
    709870] qed.
    710 
  • src/correctness.ma

    r3145 r3156  
    2323  let ctrace ≝ costlabels_of_observables itrace in
    2424  Σ_{l ∈ ctrace}(costmap l).
     25
     26definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝
     27λC,p,m.
     28  let g ≝ make_global … (pcs_exec … C) p in
     29  let C' ≝ pcs_to_cs C g in
     30  ! s0 ← make_initial_state … p;
     31  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
     32  return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉.
    2533
    2634definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝
     
    8593
    8694(* atm they are all axioms *)
    87 include "RTLabs/RTLabsExecToTrace.ma".
    8895include "RTLabs/RTLabsToRTLAxiom.ma".
    8996include "RTL/RTL_separate_to_overflow.ma".
     
    166173#ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
    167174#OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
    168 #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
     175#ra_s0 * #ra_s1 * #ra_s2 * #fn * #ra_init * #ra_ft * * #ra_ft_fn #ra_ft_obs * #ra_tlr * * #ra_unrepeating #ra_max #ra_obs'
    169176>OBS -ra_meas
    170 cases (produce_rtlabs_flat_trace … ra_exec_prefix)
    171 #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
    172177%{prefix} %{subtrace} %{fn} %[%]
    173 %{ra_init_ok ra_max}
    174 %{ra_unrepeating EQ_ra_pref_obs ra_obs'}
    175 (* fn is the current function ... *) cases daemon
     178%{ra_init ra_max}
     179%{ra_unrepeating ra_ft_obs ra_ft_fn ra_obs'}
    176180qed.
    177181
Note: See TracChangeset for help on using the changeset viewer.