Changeset 2685 for src/common


Ignore:
Timestamp:
Feb 21, 2013, 11:38:36 AM (7 years ago)
Author:
campbell
Message:

Progress on measurable trace preservation: prefix preserves observable
intensional events (costs and calls).

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2678 r2685  
    33include "common/Measurable.ma".
    44
    5 definition normal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝
     5definition pnormal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝
    66λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
    77
    8 lemma normal_state_inv : ∀C,g,s.
    9   normal_state C g s →
     8lemma pnormal_state_inv : ∀C,g,s.
     9  pnormal_state C g s →
    1010  pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump.
    1111#C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ *
     12qed.
     13
     14lemma normal_state_p : ∀C,g,s.
     15  pnormal_state C g s = normal_state (pcs_to_cs C g) s.
     16//
    1217qed.
    1318
     
    2631  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
    2732  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
    28   ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
    29   ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2);
     33  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2;
     34  ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_labelled ms_C1 g1 s1 = pcs_labelled ms_C2 g2 s2;
     35  ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2;
     36  ms_rel_callee : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → ∀H,H'. pcs_callee ms_C1 g1 s1 H = pcs_callee ms_C2 g2 s2 H';
    3037
    3138  (* These hold in (at least) the languages of interest for measurable subtraces *)
    32   ms_labelled_normal_1 : ∀g1,s1. bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C1 g1 s1);
    33   ms_labelled_normal_2 : ∀g2,s2. bool_to_Prop (pcs_labelled ms_C2 g2 s2) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
     39  ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1;
     40  ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2;
    3441  ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall;
    3542
     
    4451    ∀s1,s1'.
    4552    ms_rel g1 g2 INV s1 s1' →
    46     normal_state ms_C1 g1 s1 →
     53    pnormal_state ms_C1 g1 s1 →
    4754    ¬ pcs_labelled ms_C1 g1 s1 →
    4855    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    49     ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
     56    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
    5057      tr = tr' ∧
    5158      ms_rel g1 g2 INV s2 s2' ∧
     
    6067    ¬ pcs_labelled ms_C1 g1 s1 →
    6168    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    62     ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
     69    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
    6370      tr = tr' ∧
    6471      ms_rel g1 g2 INV s2 s2'
     
    8491
    8592(* TODO: obs eq *)
    86 
     93(*
    8794lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
    8895  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
    89   normal_state C g s1 →
     96  pnormal_state C g s1 →
    9097  stack_after (pcs_to_cs C g stack) current trace = current.
    9198#C #g #s1 #trace #s2 #stack #current #EXEC
     
    95102whd in ⊢ (??%?); generalize in match (cs_stack ??);
    96103whd in match (cs_classify ??);
    97 cases (normal_state_inv … N)
     104cases (pnormal_state_inv … N)
    98105#CL >CL #f %
    99106qed.
     
    101108lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
    102109  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
    103   normal_state C g s1 →
     110  pnormal_state C g s1 →
    104111  max_stack (pcs_to_cs C g stack) current trace = current.
    105112#C #g #s1 #trace #s2 #stack #current #EXEC
     
    109116whd in ⊢ (??%?); generalize in match (cs_stack ??);
    110117whd in match (cs_classify ??);
    111 cases (normal_state_inv … N)
     118cases (pnormal_state_inv … N)
    112119#CL >CL #f %
    113120qed.
     
    161168 cases (inv s2) // * ]| // ]
    162169qed.
    163 
     170*)
    164171(* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
    165172   observables? *)
    166173
     174lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'.
     175  exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 →
     176  ∃tr. trace = [〈s,tr〉].
     177#O #I #fx #g #s #trace #s' #EXEC
     178cases (exec_steps_S … EXEC)
     179#nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct
     180%{tr} %
     181qed.
     182
     183lemma all_1 : ∀A.∀P:A → bool.∀x.
     184  P x = all A P [x].
     185#A #P #x whd in ⊢ (???%); cases (P x) //
     186qed.
    167187
    168188(* WIP commented out*)
     
    171191  ∀g,g'.
    172192  ∀INV:ms_inv MS g g'.
    173   ∀max_allowed_stack.
    174193  ∀s1,s1'.
    175194  ms_rel MS g g' INV s1 s1' →
     
    178197  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
    179198  pcs_labelled (ms_C1 MS) g sf →
    180   le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →
    181199
    182200  ∃m',prefix',sf'.
    183201    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
    184     le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧
    185  
     202
     203    intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧
    186204    ms_rel MS g g' INV sf sf'.
    187 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init
    188 #g #g' #INV #max #s1 #s1' #REL
     205* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init
     206#g #g' #INV #s1 #s1' #REL
    189207#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
    190 generalize in match 0; (* current stack level *)
     208generalize in match [ ]; (* current call stack *)
    191209elim m0
    192210[ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
    193   #max_ok %{0} %{[]} %{s1'}
     211  %{0} %{[]} %{s1'}
    194212  % [ % // | // ]
    195 | #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK
     213| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf
    196214  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
    197215  cases (true_or_false_Prop … (pcs_labelled … s1))
     
    200218    #AFTER1'
    201219    cases (after_n_exec_steps … AFTER1')
    202     #prefix' * #s2' * #EXEC1' * #Etrace #R2
    203     cut (normal_state C1 g s1) [ @(proj1 … (labelled_normal1 …)) assumption ] #N1
    204     cut (normal_state C2 g' s1') [ @(proj1 … (labelled_normal2 …)) @(proj1 … (rel_labelled … REL)) assumption ] #N1'
    205     cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
    206     [ 2: @(transitive_le … MAX_OK) >E1 cases daemon (* <max_stack_append
    207       >(stack_normal_step … EXEC1 N1)
    208       >(stack_normal_step … EXEC1' N1')
    209       @max_r //*)
    210     ]
    211     #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     220    #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2
     221    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
     222    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
     223    cases (IH current_stack … R2 … EXEC2 CSf)
     224    #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
    212225    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
    213226    % [ % [ @(exec_steps_join … EXEC1') @EXEC''
    214       | <max_stack_append @to_max
    215         [ >(max_stack_normal_step … EXEC1' N1')
    216           lapply MAX_OK >E1 cases daemon (* <max_stack_append
    217           >(max_stack_normal_step … EXEC1 N1)
    218           #H /2 by le_maxl/*)
    219         | @MAX'' ] ]
    220       | @R''
     227      | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
     228        cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
     229        <all_1 assumption
     230      ]| assumption
    221231      ]
    222232 
    223233  | #NCS
    224     cases (true_or_false_Prop (normal_state C1 g s1))
     234    cases (true_or_false_Prop (pnormal_state C1 g s1))
    225235    [ #NORMAL
    226236      (* XXX should set things up so that notb_Prop isn't needed *)
    227237      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
    228238      #n' #AFTER1'
    229       cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * * #Etrace #R2 #_ (* measure *)
    230       cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
    231       [ 2: cases daemon ] (* XXX *)
    232       #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     239      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
     240      cases (IH current_stack … R2 … EXEC2 CSf)
     241      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
    233242      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
    234243      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
    235         | <max_stack_append @to_max
    236           [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
    237             lapply MAX_OK >E1 <max_stack_append
    238             >(max_stack_normal_step … EXEC1 N1)
    239             #H /2 by le_maxl/*)
    240           | @MAX'' ] ]
     244        | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     245          [ assumption
     246          | cases prefix' in EXEC1' INV ⊢ %;
     247            [ //
     248            | * #sx #trx #tl #EXEC1' #INV
     249              <(exec_steps_first … EXEC1')
     250              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
     251              @INV
     252            ]
     253          | @OBS'' ] ]
    241254        | @R''
    242255        ]
    243256    | #CALLRET
    244       cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
    245       [ 2: whd in CALLRET:(?%); whd in match (normal_state ???) in CALLRET;
     257      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
     258      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
    246259        lapply (no_tailcalls … s1)
    247260        cases (pcs_classify … s1) in CALLRET ⊢ %;
    248         normalize * #H #H' try % try cases (H I)
    249         cases H' /2/ ]
     261        [ 1,3: #_ #_ /2/
     262        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
     263        ]
     264      ] * #CL
     265      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
     266      [2,4: >CL %]
    250267      #m' #AFTER1'
    251       cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * #Etrace #R2
    252       cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
    253       [ 2: cases daemon ] (* XXX *)
    254       #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     268      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
     269      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
     270      | letin next_stack ≝ (tail … current_stack)
     271      ]
     272      cases (IH next_stack … R2 … EXEC2 CSf)
     273      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
    255274      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
    256       % [ % [ @(exec_steps_join … EXEC1') @EXEC''
    257         | <max_stack_append @to_max
    258           [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
    259             lapply MAX_OK >E1 <max_stack_append
    260             >(max_stack_normal_step … EXEC1 N1)
    261             #H /2 by le_maxl/*)
    262           | @MAX'' ] ]
    263         | @R''
     275      % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC''
     276        | destruct cases (exec_steps_S … EXEC1')
     277          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     278          destruct
     279          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     280          [1,3: whd in match (cs_classify ??); >CL %
     281          |2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     282          | @INV
     283          | assumption
     284          | @(rel_callee … REL)
     285          ]
     286        | destruct cases (exec_steps_S … EXEC1')
     287          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     288          destruct
     289          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     290          [ whd in match (cs_classify ??); >CL %
     291          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     292          | @INV
     293          | assumption
     294          ]
    264295        ]
     296      | 2,4: @R''
     297      ]
    265298    ]
    266299  ]
    267 qed.
     300] qed.
    268301       
    269302     
  • src/common/Measurable.ma

    r2670 r2685  
    1111  cs_labelled : state … cs_exec cs_global → bool;
    1212  cs_classify : state … cs_exec cs_global → status_class;
    13   cs_stack : ∀s. match cs_classify … s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
     13  cs_callee : ∀s. match cs_classify … s with [ cl_call ⇒ True | _ ⇒ False ] → ident
    1414}.
    1515
     
    2525λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
    2626
    27 definition measure_stack_aux ≝
    28 λC. (λx. λstr:cs_state … C × trace.
    29     let 〈current,max_stack〉 ≝ x in
    30     let 〈s,tr〉 ≝ str in
    31     let new ≝
    32       match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
    33       [ cl_call ⇒ λsc. current + sc I
    34       | cl_return ⇒ λsc. current - sc I
    35       | _ ⇒ λ_. current
    36       ] (cs_stack C s) in
    37     〈new, max max_stack new〉).
    38 
    39 definition measure_stack : ∀C. nat → list (cs_state … C × trace) → nat × nat ≝
    40 λC,current.
    41   foldl … (measure_stack_aux C) 〈current,0〉.
    42 
    43 definition stack_after : ∀C. nat → list (cs_state … C × trace) → nat ≝
    44 λC,current,x. \fst (measure_stack C current x).
    45 
    46 definition max_stack : ∀C. nat → list (cs_state … C × trace) → nat ≝
    47 λC,current,x. \snd (measure_stack C current x).
     27(* For intensional_event; should separate out definition *)
     28include "common/StatusSimulation.ma".
     29
     30definition intensional_event_of_event : event → list intensional_event ≝
     31λev. match ev with
     32[ EVcost l ⇒ [ IEVcost l ]
     33| EVextcall _ _ _ ⇒ [ ]  (* No equivalent, but there shouldn't be any for now *)
     34].
     35
     36definition intensional_events_of_events : trace → list intensional_event ≝
     37λtr. flatten ? (map ?? intensional_event_of_event tr).
     38
     39let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
     40match trace with
     41[ nil ⇒ 〈callstack, [ ]〉
     42| cons str tl ⇒
     43  let 〈s,tr〉 ≝ str in
     44  let 〈callstack, call_event〉 ≝
     45    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
     46    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
     47    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
     48    | _ ⇒ λ_. 〈callstack, [ ]〉
     49    ] (cs_callee C s) in
     50  let other_events ≝ intensional_events_of_events tr in
     51  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
     52    〈callstack, call_event@other_events@rem〉
     53].
     54
     55definition normal_state : ∀C:classified_system. cs_state … C → bool ≝
     56λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
     57
     58lemma normal_state_inv : ∀C,s.
     59  normal_state C s →
     60  cs_classify C s = cl_other ∨ cs_classify C s = cl_jump.
     61#C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ *
     62qed.
     63
     64lemma int_trace_of_normal : ∀C,callstack,s,tr,trace.
     65  normal_state C s →
     66  intensional_trace_of_trace C callstack (〈s,tr〉::trace) =
     67    (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in
     68      〈stk', (intensional_events_of_events tr)@tl〉).
     69#C #callstack #s #tr #trace #NORMAL
     70whd in ⊢ (??%?);
     71generalize in match (cs_callee C s);
     72cases (normal_state_inv … NORMAL)
     73#CL >CL normalize nodelta #_
     74cases (intensional_trace_of_trace C callstack trace)
     75#callstack' #tl normalize nodelta
     76%
     77qed.
     78
     79lemma flatten_append : ∀A,l1,l2.
     80  flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
     81#A #l1 #l2
     82elim l1
     83[ %
     84| #h #t #IH whd in ⊢ (??%(??%?));
     85  change with (flatten ??) in match (foldr ?????); >IH
     86  change with (flatten ??) in match (foldr ?????);
     87  >associative_append %
     88] qed.
     89
     90
     91lemma int_events_append : ∀tr1,tr2.
     92  intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2).
     93#tr1 #tr2
     94change with (flatten ??) in ⊢ (??%(??%%));
     95<map_append >flatten_append %
     96qed.
     97
     98
     99lemma int_trace_irr : ∀C,callstack,s,trace.
     100  normal_state C s →
     101  intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace.
     102#C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL)
     103cases (intensional_trace_of_trace ???) //
     104qed.
     105
     106lemma int_trace_append : ∀C,callstack,s,t1,t2,trace.
     107  normal_state C s →
     108  intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace).
     109#C #callstack #s #t1 #t2 #trace #NORMAL
     110>(int_trace_of_normal … NORMAL)
     111>(int_trace_of_normal … NORMAL)
     112>(int_trace_of_normal … NORMAL)
     113cases (intensional_trace_of_trace ???) #callstack' #trace'
     114normalize nodelta
     115>int_events_append
     116>associative_append %
     117qed.
     118
     119lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'.
     120  normal_state C s →
     121  all … (λstr. normal_state C' (\fst str)) trace →
     122  intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' →
     123  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
     124#C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL'
     125>(int_trace_of_normal … NORMAL)
     126cases (intensional_trace_of_trace C callstack rem) #callstack' #trace'
     127#REM whd in ⊢ (??%?);
     128elim trace in NORMAL' ⊢ %;
     129[ #_ @REM
     130| * #s' #tr' #tl #IH #NORMAL'
     131  cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl
     132  >int_trace_of_normal
     133  [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%);
     134    >int_events_append >associative_append %
     135  | @NORMALs
     136  ]
     137] qed.
     138
     139lemma int_trace_append' : ∀C,t1,t2,callstack.
     140  intensional_trace_of_trace C callstack (t1@t2) =
     141    (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in
     142     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in
     143     〈cs'', t1'@t2'〉).
     144#C #t1 #t2 elim t1
     145[ #callstack whd in match ([ ]@t2); whd in ⊢ (???%);
     146  cases (intensional_trace_of_trace ???) #cs' #trace' %
     147| * #s #tr #tl #IH
     148  #callstack
     149  whd in match (intensional_trace_of_trace ???);
     150  whd in match (intensional_trace_of_trace ???);
     151  generalize in match (cs_callee C s);
     152  cases (cs_classify C s)
     153  normalize nodelta #callee
     154  [ cases callstack [2: #cshd #cdtl] normalize nodelta ]
     155  >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl'
     156  normalize nodelta
     157  cases (intensional_trace_of_trace C ? t2) #cs'' #tl''
     158  normalize nodelta >associative_append >associative_append
     159  %
     160] qed.
     161
     162lemma int_trace_normal_cs : ∀C,callstack,trace.
     163  all ? (λstr. normal_state C (\fst str)) trace →
     164  callstack = \fst (intensional_trace_of_trace C callstack trace).
     165#C #callstack #trace elim trace
     166[ //
     167| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
     168  >(int_trace_of_normal … N1)
     169  >(IH Ntl) in ⊢ (??%?);
     170  cases (intensional_trace_of_trace ???) /2/
     171] qed.
     172
     173lemma int_trace_append_normal : ∀C,t1,t2,callstack.
     174  all ? (λstr. normal_state C (\fst str)) t1 →
     175  intensional_trace_of_trace C callstack (t1@t2) =
     176    (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in
     177     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in
     178     〈cs'', t1'@t2'〉).
     179#C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack)
     180lapply (int_trace_normal_cs C callstack t1 NORMAL)
     181cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct //
     182qed.
     183
     184lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'.
     185  cs_classify C s = cl_return →
     186  cs_classify C' s' = cl_return →
     187  all ? (λstr. normal_state C' (\fst str)) trace' →
     188  intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' →
     189  let trace ≝ 〈s',tr〉::trace' in
     190  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
     191#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E
     192whd
     193whd in ⊢ (??%%); normalize nodelta
     194generalize in match (cs_callee C s); generalize in match (cs_callee C' s');
     195>CL >CL' normalize nodelta #_ #_
     196cases callstack in E ⊢ %; [2: #stkhd #stktl]
     197normalize nodelta
     198cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta
     199>(int_trace_append_normal … NORMAL) normalize nodelta
     200cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
     201destruct @eq_f @eq_f
     202whd in match (gather_trace ??); >int_events_append
     203>associative_append @eq_f
     204elim trace in NORMAL ⊢ %;
     205[ 1,3: #_ %
     206| 2,4:
     207  * #s1 #tr1 #tl #IH
     208  #N cases (andb_Prop_true … N) #N1 #Ntl
     209  whd in match (gather_trace ??); >int_events_append
     210  >associative_append >(IH Ntl)
     211  >(int_trace_of_normal … N1)
     212  cases (intensional_trace_of_trace ?? tl)
     213  #cs' #tl' >associative_append %
     214] qed.
     215
     216lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop.
     217  (∀f. P f (f H)) →
     218  P (cs_callee C s) (cs_callee C s H).
     219#C #s #H #P #f @f
     220qed.
     221
     222lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'.
     223  cs_classify C s = cl_call →
     224  cs_classify C' s' = cl_call →
     225  all ? (λstr. normal_state C' (\fst str)) trace' →
     226  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
     227  cs_callee C s H = cs_callee C' s' H' →
     228  let trace ≝ 〈s',tr〉::trace' in
     229  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
     230#C #C' #callstack #s #s' #tr #trace #rem #rem' #H #H' #CL #CL' #NORMAL
     231whd in ⊢ (? → ? → %);
     232whd in ⊢ (? → ? → ??%%); normalize nodelta
     233@generalize_callee
     234@generalize_callee
     235>CL in H ⊢ %; * >CL' in H' ⊢ %; * normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
     236cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
     237>(int_trace_append_normal … NORMAL) normalize nodelta
     238cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
     239destruct @eq_f @eq_f
     240whd in match (gather_trace ??); >int_events_append
     241>associative_append @eq_f
     242elim trace in NORMAL ⊢ %;
     243[ 1,3: #_ %
     244| 2,4:
     245  * #s1 #tr1 #tl #IH
     246  #N cases (andb_Prop_true … N) #N1 #Ntl
     247  whd in match (gather_trace ??); >int_events_append
     248  >associative_append >(IH Ntl)
     249  >(int_trace_of_normal … N1)
     250  cases (intensional_trace_of_trace ?? tl)
     251  #cs' #tl' >associative_append %
     252] qed.
     253 
     254
     255definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
     256λcosts,start.
     257  foldl ?? (λx. λev.
     258    match ev with
     259    [ IEVcall id ⇒
     260        let 〈current_stack,max_stack〉 ≝ x in
     261        let new_stack ≝ current_stack + costs id in
     262        〈new_stack, max new_stack max_stack〉
     263    | IEVret id ⇒
     264        let 〈current_stack,max_stack〉 ≝ x in
     265        〈current_stack - costs id, max_stack〉
     266    | _ ⇒ x
     267    ]) 〈start,start〉.
     268
     269definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝
     270λcosts, start, trace. \snd (measure_stack costs start trace).
    48271
    49272lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
     
    55278| #h #t #IH' #acc #H @IH' @IH @H
    56279] qed.
    57 
     280(*
    58281lemma max_stack_step : ∀C,a,m,a',m',tr,s.
    59282  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
     
    107330  >IH %
    108331] qed.
    109  
     332*) 
    110333
    111334(* Check that the trace ends with the return from the starting function and one
     
    140363  pcs_labelled : ∀g. state … pcs_exec g → bool;
    141364  pcs_classify : ∀g. state … pcs_exec g → status_class;
    142   pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
     365  pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident
    143366}.
    144367
    145 definition pcs_to_cs : ∀C:preclassified_system. global … C → (ident → nat) → classified_system ≝
    146 λC,g,stack_cost.
    147   mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?).
     368definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝
     369λC,g.
     370  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).
    148371
    149372(* FIXME: this definition is unreasonable because it presumes we can easily
     
    158381λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
    159382  let g ≝ make_global … (pcs_exec … C) p in
    160   let C' ≝ pcs_to_cs C g stack_cost in
     383  let C' ≝ pcs_to_cs C g in
    161384  make_initial_state … p = OK ? s0 ∧
    162385  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
     
    164387  trace_is_label_to_return C' interesting ∧
    165388  bool_to_Prop (will_return' C' interesting) ∧
    166   le (max_stack C' 0 (prefix@interesting)) max_allowed_stack.
     389  le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
    167390
    168391(* TODO: probably ought to be elsewhere; use exec_steps instead
  • src/common/SmallstepExec.ma

    r2682 r2685  
    540540qed.
    541541
     542lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
     543  exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
     544  s = s1.
     545#n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
     546lapply (exec_steps_length … EXEC) #E normalize in E; destruct
     547cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
     548%
     549qed.
     550
    542551lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
    543552  after_n_steps n O I fx g s inv P →
    544   ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'.
     553  ∃trace,s'.
     554    exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧
     555    bool_to_Prop (all ? (λstr. inv (\fst str)) (tail … trace)) ∧
     556    P (gather_trace ? trace) s'.
    545557#n elim n
    546 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER
     558[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % [ %{(refl ??)} % | @AFTER ]
    547559| #m #IH #O #I #fx #g #s #inv #P #AFTER
    548560  cases (after_1_of_n_steps … AFTER)
    549561  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
    550562  cases (IH … AFTER')
    551   #tl * #s' * #STEPS #p
     563  #tl * #s' * * #STEPS #INV' #p
    552564  %{(〈s,tr1〉::tl)} %{s'} %
    553   [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
     565  [ %
     566    [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %
     567    | cases tl in STEPS INV INV' ⊢ %; [ // | * #sx #trx #t #STEPS #INV #INV'
     568      <(exec_steps_first … STEPS) whd in ⊢ (?%); >INV //
     569      >(exec_steps_length … STEPS) %
     570      ]
     571    ]
     572  | // ]
    554573] qed.
    555574
     
    588607  destruct %
    589608] qed.
    590 
    591 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
    592   exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
    593   s = s1.
    594 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
    595 lapply (exec_steps_length … EXEC) #E normalize in E; destruct
    596 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
    597 %
    598 qed.
    599609
    600610(* Show that it corresponds to split_trace … (exec_inf …).
Note: See TracChangeset for help on using the changeset viewer.