Changeset 2044


Ignore:
Timestamp:
Jun 12, 2012, 10:52:37 AM (5 years ago)
Author:
campbell
Message:

PCs for RTLabs structured traces.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2025 r2044  
    44
    55discriminator status_class.
     6
     7(* We augment states with a stack of function blocks (i.e. pointers) so that we
     8   can make sensible "program counters" for the abstract state definition, along
     9   with a proof that we will get the correct code when we do the lookup (which
     10   is done to find cost labels given a pc).
     11   
     12   Adding them to the semantics is an alternative, more direct approach.
     13   However, it makes animating the semantics extremely difficult, because it
     14   is hard to avoid normalising and displaying irrelevant parts of the global
     15   environment and proofs.
     16   
     17   We use blocks rather than identifiers because the global environments go
     18
     19     identifier → block → definition
     20   
     21   and we'd have to introduce backwards lookups to find identifiers for
     22   function pointers.
     23 *)
     24
     25definition Ras_Fn_Match ≝
     26λge,state,fn_stack.
     27  match state with
     28  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
     29  | Callstate fd _ _ fs _ ⇒
     30      match fn_stack with
     31      [ nil ⇒ False
     32      | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
     33        All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
     34      ]
     35  | Returnstate _ _ fs _ ⇒
     36      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
     37  | Finalstate _ ⇒ fn_stack = [ ]
     38  ].
     39
     40record RTLabs_state (ge:genv) : Type[0] ≝ {
     41  Ras_state :> state;
     42  Ras_fn_stack : list block;
     43  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
     44}.
     45
     46(* Given a plain step of the RTLabs semantics, give the next state along with
     47   the shadow stack of function block numbers.  Carefully defined so that the
     48   coercion back to the plain state always reduces. *)
     49definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
     50  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
     51λge,s,s',t,EX. mk_RTLabs_state ge s'
     52 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
     53 ?.
     54cases s' in EX ⊢ %;
     55[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
     56  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     57    whd cases stk in mtc ⊢ %; [ * ]
     58    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
     59    | @M2 ]
     60  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
     61  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     62    whd cases stk in mtc ⊢ %; [ * ]
     63    #hd #tl #H @H
     64  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
     65  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
     66    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
     67    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
     68  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
     69  ]
     70| -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
     71  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
     72  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     73  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
     74    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
     75    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
     76  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     77  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
     78  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
     79  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
     80  ]
     81| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
     82  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     83  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
     84  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     85  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
     86    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
     87  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
     88  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
     89  ]
     90| #r #EX whd @refl
     91] qed.
     92
     93(*
     94definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
     95  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
     96λge,s,s',t.
     97match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge with
     98[ State f fs m ⇒ λEX. mk_RTLabs_state ge (State f fs m) (Ras_fn_stack … s) ?
     99| Callstate fd args dst fs m ⇒ λEX. mk_RTLabs_state ge (Callstate fd args dst fs m) (func_block_of_exec … EX::Ras_fn_stack … s) ?
     100| Returnstate rtv dst fs m ⇒ λEX. mk_RTLabs_state ge (Returnstate rtv dst fs m) (tail … (Ras_fn_stack … s)) ?
     101| Finalstate r ⇒ λEX. mk_RTLabs_state ge (Finalstate r) [ ] ?
     102].
     103[ cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
     104  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     105    whd cases stk in mtc ⊢ %; [ * ]
     106    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
     107    | @M2 ]
     108  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
     109  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     110    whd cases stk in mtc ⊢ %; [ * ]
     111    #hd #tl #H @H
     112  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
     113  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
     114    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
     115    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
     116  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
     117  ]
     118| cases (func_block_of_exec … EX) #func_block #FFP
     119  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
     120  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     121  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
     122    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
     123    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
     124  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     125  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
     126  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
     127  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
     128  ]
     129| cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
     130  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     131  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
     132  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     133  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
     134    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
     135  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
     136  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
     137  ]
     138| whd @refl
     139] qed.*)
    6140
    7141(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
     
    46180].
    47181
    48 (* At the moment we don't need to talk about the program counter, so we just
    49    use unit. *)
    50 definition unit_deqset ≝ mk_DeqSet unit (λ_.λ_. true) ?.
    51 * * % //
     182inductive RTLabs_pc : Type[0] ≝
     183| rapc_state : block → label → RTLabs_pc
     184| rapc_call : block → RTLabs_pc
     185| rapc_ret : option block → RTLabs_pc
     186| rapc_fin : RTLabs_pc
     187.
     188
     189definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
     190#x #y @eq_block_elim
     191[ #E destruct /2/
     192| * #NE % #E destruct cases (NE (refl ??))
     193] qed.
     194
     195definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
     196λx,y. match x with
     197[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
     198| rapc_call b1 ⇒ match y with [ rapc_call b2 ⇒ eq_block b1 b2 | _ ⇒ false ]
     199| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eq_option block_eq b1 b2 | _ ⇒ false ]
     200| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
     201].
     202
     203definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
     204whd in match RTLabs_pc_eq; whd in match eq_option; whd in match block_eq;
     205* [ #b1 #l1 | #b1 | * [2: #b1 ] | ]
     206* [ 1,5,9,13,17: #b2 #l2 | 2,6,10,14,18: #b2 | 3,7,11,15,19: * [2,4,6,8,10: #b2] | *: ]
     207normalize nodelta
     208[ 1,7,13: @eq_block_elim [ 1,3,5: #E destruct | *: * #NE ] ]
     209[ 1,4: @eq_identifier_elim [ 1,3: #E destruct | *: * #NE ] ]
     210normalize % #E destruct try (cases (NE (refl ??))) @refl
    52211qed.
     212
     213definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝
     214λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒
     215match s' return λs'. Ras_Fn_Match ? s' ? → ? with
     216[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
     217| Callstate _ _ _ _ _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call b ]
     218| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
     219| Finalstate _ ⇒ λmtc. rapc_fin
     220] mtc0 ].
     221whd in mtc; cases mtc
     222qed.
     223
     224definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
     225λge,pc.
     226match pc with
     227[ rapc_state b l ⇒
     228  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
     229    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
     230| _ ⇒ None ?
     231].
    53232
    54233definition RTLabs_status : genv → abstract_status ≝
    55234λge.
    56235  mk_abstract_status
    57     state
    58     (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
    59     unit_deqset
    60     (λ_. it)
     236    (RTLabs_state ge)
     237    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
     238    RTLabs_deqset
     239    (RTLabs_state_to_pc ge)
    61240    (λs,c. RTLabs_classify s = c)
    62     RTLabs_cost_label
     241    (RTLabs_pc_to_cost_label ge)
    63242    (λs,s'. match s with
    64243      [ mk_Sig s p ⇒
     
    85264   labelled. *)
    86265
    87 lemma RTLabs_costed : ∀ge,s.
    88   RTLabs_cost s = true
     266lemma RTLabs_costed : ∀ge. ∀s:RTLabs_state ge.
     267  RTLabs_cost s = true
    89268  as_costed (RTLabs_status ge) s.
    90 #ge *
    91 [ * #func #locals #next #nok #b #r #fs #m
    92   whd in ⊢ (??%? → %); whd in ⊢ (? → ?(??%?));
    93   cases (lookup_present ?? (f_graph func) ??) normalize
     269cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
     270#ge * *
     271[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
     272  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
     273  whd in match (as_pc_of ??);
     274  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
     275  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
     276  >(lookup_lookup_present … nok)
     277  whd in ⊢ (?(??%?)(?(??%?)));
     278  % cases (lookup_present ?? (f_graph func) ??) normalize
    94279  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
    95   % #E' destruct
    96 | normalize #fd #args #r #fs #m #E destruct
    97 | normalize #A #B #C #D #E destruct
    98 | normalize #A #B destruct
    99 ] qed.
    100 
    101 lemma costed_RTLabs : ∀ge,s.
    102   as_costed (RTLabs_status ge) s →
    103   RTLabs_cost s = true.
    104 #ge
    105 cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #H
    106 *
    107 [ * #func #locals #next #nok #b #r #fs #m
    108   whd in ⊢ (% → ??%?); whd in ⊢ (?(??%?) → ?);
    109   cases (lookup_present ?? (f_graph func) ??) normalize //
    110   #A try #B try #C try #D try #E try #F try #G try #I try #J cases (H ?) //
    111 | *: normalize #A #B try #C try #D try #E try #F cases (H ?) //
    112 ] qed.
    113 
    114 lemma RTLabs_not_cost : ∀ge,s.
     280  try (% #E' destruct)
     281  cases (NONE ?) assumption
     282| #fd #args #dst #fs #m #stk #mtc %
     283  [ #E normalize in E; destruct
     284  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
     285    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
     286    #H cases (NONE H)
     287  ]
     288| #v #dst #fs #m #stk #mtc %
     289  [ #E normalize in E; destruct
     290  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
     291    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
     292    #H cases (NONE H)
     293  ]
     294| #r #stk #mtc %
     295  [ #E normalize in E; destruct
     296  | #E normalize in E; cases (NONE E)
     297  ]
     298] qed.
     299
     300lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_state ge.
    115301  RTLabs_cost s = false →
    116302  ¬ as_costed (RTLabs_status ge) s.
    117 #ge *
    118 [ * #func #locals #next #nok #b #r #fs #m
    119   whd in ⊢ (??%? → ?%); whd in ⊢ (? → ?(?(??%?)));
    120   cases (lookup_present ?? (f_graph func) ??) normalize
    121   #A try #B try #C try #D try #E try #F try #G try #H try #I destruct
    122   % * #J @J @refl
    123 | *: normalize #A #B try #C try #D try #E try #F % * #G @G @refl
    124 ] qed.
     303#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
     304qed.
    125305
    126306(* Before attempting to construct a structured trace, let's show that we can
     
    547727
    548728definition well_cost_labelled_ge : genv → Prop ≝
    549 λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
     729λge. ∀b,f. find_funct_ptr ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
    550730
    551731definition well_cost_labelled_state : state → Prop ≝
     
    656836cases fd
    657837[ #fn whd in ⊢ (??%? → % → ?);
    658   @bind_res_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)
     838  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
    659839  #m' #b whd in ⊢ (??%? → ?); #E' destruct
    660840  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
     
    671851   frames never change, and that after returning from the function we preserve
    672852   the identity of the next instruction to execute.
     853   
     854   Note: since this was first written I've introduced the shadow stack of
     855   function blocks.  It might be possible to replace some or all of the stack
     856   preservation with that.
    673857 *)
    674858
     
    8241008] qed.
    8251009 
    826 lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
     1010lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.∀tr.
    8271011  ∀CL : RTLabs_classify s1 = cl_call.
    8281012  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
    8291013  stack_preserved ends_with_ret s2 s3 →
    8301014  as_after_return (RTLabs_status ge) «s1,CL» s3.
    831 #ge #s1 #s2 #s3 #tr #CL #EV #S23
     1015#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #tr #CL #EV #S23
    8321016cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
     1017whd
    8331018inversion S23
    8341019[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
    835 | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
     1020| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct whd
    8361021  inversion (eval_preserves … EV)
    8371022  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
     
    8701055   of the termination proof is respected. *)
    8711056record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
    872   (start:state) (full:flat_trace io_out io_in ge start)
     1057  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
    8731058  (original_terminates: will_return ge depth start full)
    874   (T:state → Type[0]) (limit:nat) : Type[0] ≝
     1059  (T:RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
    8751060{
    876   new_state : state;
     1061  new_state : RTLabs_state ge;
    8771062  remainder : flat_trace io_out io_in ge new_state;
    8781063  cost_labelled : well_cost_labelled_state new_state;
     
    8821067               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
    8831068               | S d ⇒ ΣTM:will_return ge d new_state remainder.
    884                          limit > will_return_length … TM
     1069                         gt limit (will_return_length … TM)
    8851070                         will_return_end … original_terminates = will_return_end … TM
    8861071               ]
     
    8901075   encountering a label. *)
    8911076record sub_trace_result (ge:genv) (depth:nat)
    892   (start:state) (full:flat_trace io_out io_in ge start)
     1077  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
    8931078  (original_terminates: will_return ge depth start full)
    894   (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝
     1079  (T:trace_ends_with_ret → RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
    8951080{
    8961081  ends : trace_ends_with_ret;
     
    9021087   the size of the termination proof might need to be relaxed, too. *)
    9031088
    904 definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
     1089definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    9051090  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
    9061091    will_return_end … TM1 = will_return_end … TM2 →
     
    9311116] qed.
    9321117
    933 definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
     1118definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    9341119  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
    9351120    will_return_end … TM1 = will_return_end … TM2 →
     
    9451130definition myge : nat → nat → Prop ≝ ge.
    9461131
    947 let rec make_label_return ge depth s
     1132let rec make_label_return ge depth (s:RTLabs_state ge)
    9481133  (trace: flat_trace io_out io_in ge s)
    9491134  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    9551140  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
    9561141              (trace_label_return (RTLabs_status ge) s)
    957               (will_return_length … TERMINATES) ≝
     1142              (will_return_length … TERMINATES) ≝ 
    9581143             
    9591144match TIME return λTIME. TIME ≥ ? → ? with
     
    9861171
    9871172
    988 and make_label_label ge depth s
     1173and make_label_label ge depth (s:RTLabs_state ge)
    9891174  (trace: flat_trace io_out io_in ge s)
    9901175  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    10091194
    10101195
    1011 and make_any_label ge depth s
    1012   (trace: flat_trace io_out io_in ge s)
     1196and make_any_label ge depth (s0:RTLabs_state ge)
     1197  (trace: flat_trace io_out io_in ge s0)
    10131198  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    1014   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    1015   (TERMINATES: will_return ge depth s trace)
     1199  (STATE_COSTLABELLED: well_cost_labelled_state s0)  (* functions in the state *)
     1200  (TERMINATES: will_return ge depth s0 trace)
    10161201  (TIME: nat)
    10171202  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
    1018   on TIME : sub_trace_result ge depth s trace TERMINATES
    1019               (λends. trace_any_label (RTLabs_status ge) ends s)
     1203  on TIME : sub_trace_result ge depth s0 trace TERMINATES
     1204              (λends. trace_any_label (RTLabs_status ge) ends s0)
    10201205              (will_return_length … TERMINATES) ≝
    10211206
     
    10231208[ O ⇒ λTERMINATES_IN_TIME. ⊥
    10241209| S TIME ⇒ λTERMINATES_IN_TIME.
    1025 
    1026   match trace return λs,trace. well_cost_labelled_state s →
     1210  match s0 return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
     1211                                      well_cost_labelled_state s →
     1212                                      ∀TM:will_return ??? trace.
     1213                                      myge ? (times 3 (will_return_length ??? trace TM)) →
     1214                                      sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
     1215  with [ mk_RTLabs_state s stk mtc0 ⇒ λtrace.
     1216  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
     1217                               well_cost_labelled_state s →
    10271218                               ∀TM:will_return ??? trace.
    10281219                               myge ? (times 3 (will_return_length ??? trace TM)) →
    1029                                sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
     1220                               sub_trace_result ge depth (mk_RTLabs_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_state ge s stk mtc)) (will_return_length … TM) with
    10301221  [ ft_stop st FINAL ⇒
    1031       λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
    1032 
    1033   | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    1034     match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     1222      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
     1223
     1224  | ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
     1225    let start' ≝ mk_RTLabs_state ge start stk mtc in
     1226    let next' ≝ next_state ? start' ?? EV in
     1227    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
    10351228    [ cl_other ⇒ λCL.
    1036         match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     1229        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
    10371230        (* We're about to run into a label. *)
    10381231        [ true ⇒ λCS.
    1039             mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
     1232            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
    10401233              doesnt_end_with_ret
    1041               (mk_trace_result ge … next trace' ?
    1042                 (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) ??)
     1234              (mk_trace_result ge … next' trace' ?
     1235                (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??)
    10431236        (* An ordinary step, keep going. *)
    10441237        | false ⇒ λCS.
    1045             let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
    1046                 replace_sub_trace r ?
     1238            let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
     1239                replace_sub_trace ????????????? r ?
    10471240                  (tal_step_default (RTLabs_status ge) (ends … r)
    1048                      start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
     1241                     start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?
    10491242        ] (refl ??)
    10501243       
    10511244    | cl_jump ⇒ λCL.
    1052         mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
     1245        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
    10531246          doesnt_end_with_ret
    1054           (mk_trace_result ge … next trace' ?
    1055             (tal_base_not_return (RTLabs_status ge) start next ???) ??)
     1247          (mk_trace_result ge … next' trace' ?
     1248            (tal_base_not_return (RTLabs_status ge) start' next' ???) ??)
    10561249           
    10571250    | cl_call ⇒ λCL.
    1058         let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
    1059         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
     1251        let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
     1252        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
    10601253        (* We're about to run into a label, use base case for call *)
    10611254        [ true ⇒ λCS.
    1062             mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
     1255            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
    10631256            doesnt_end_with_ret
    10641257            (mk_trace_result ge …
    1065               (tal_base_call (RTLabs_status ge) start next (new_state … r)
    1066                 ? CL ? (new_trace … r) (RTLabs_costed … CS)) ??)
     1258              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
     1259                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
    10671260        (* otherwise use step case *)
    10681261        | false ⇒ λCS.
     
    10721265            replace_sub_trace … r' ?
    10731266              (tal_step_call (RTLabs_status ge) (ends … r')
    1074                 start next (new_state … r) (new_state … r') ? CL ?
     1267                start' next' (new_state … r) (new_state … r') ? CL ?
    10751268                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
    10761269        ] (refl ??)
    10771270
    10781271    | cl_return ⇒ λCL.
    1079         mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
     1272        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
    10801273          ends_with_ret
    10811274          (mk_trace_result ge …
    1082             next
     1275            next'
    10831276            trace'
    10841277            ?
    1085             (tal_base_return (RTLabs_status ge) start next ? CL)
     1278            (tal_base_return (RTLabs_status ge) start' next' ? CL)
    10861279            ?
    10871280            ?)
    10881281    ] (refl ? (RTLabs_classify start))
    10891282   
    1090   | ft_wrong start m NF EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
     1283  | ft_wrong start m NF EV ⇒ λmtc,STATE_COSTLABELLED,TERMINATES. ⊥
    10911284 
    1092   ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
     1285  ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
    10931286] TERMINATES_IN_TIME.
    10941287
     
    10991292| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
    11001293| @(stack_preserved_join … (stack_ok … r)) //
    1101 | @(costed_RTLabs ge) @(trace_label_label_label … (new_trace … r))
     1294| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
    11021295| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
    11031296  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
     
    11111304| @le_n
    11121305| //
    1113 | @RTLabs_costed //
     1306| @(proj1 … (RTLabs_costed …)) //
    11141307| @le_S_S_to_le @TERMINATES_IN_TIME
    11151308| @(wrl_nonzero … TERMINATES_IN_TIME)
     
    11231316  ]
    11241317| @(will_return_return … CL TERMINATES)
    1125 | /2 by stack_preserved_return/
    1126 | %{tr} @EV
     1318| @(stack_preserved_return … EV) //
     1319| %{tr} %{EV} @refl
    11271320| @(well_cost_labelled_state_step  … EV) //
    11281321| whd @(will_return_notfn … TERMINATES) %2 @CL
    1129 | @stack_preserved_step /2/
    1130 | %{tr} @EV
     1322| @(stack_preserved_step … EV) /2/
     1323| %{tr} %{EV} %
    11311324| %1 whd @CL
    1132 | @RTLabs_costed @(well_cost_labelled_jump … EV) //
     1325| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
    11331326| @(well_cost_labelled_state_step  … EV) //
    11341327| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
     
    11391332  ]
    11401333| @(stack_preserved_call … EV (stack_ok … r)) //
    1141 | %{tr} @EV
    1142 | @RTLabs_after_call //
     1334| %{tr} %{EV} %
     1335| @(RTLabs_after_call … next') [2: @EV | skip | // ]
    11431336| @(cost_labelled … r)
    11441337| skip
     
    11471340  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
    11481341| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
    1149   cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' //
    1150 | @RTLabs_after_call //
    1151 | %{tr} @EV
     1342  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
     1343| @(RTLabs_after_call … next') [2: @EV | skip | // ]
     1344| %{tr} %{EV} %
    11521345| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
    11531346| @(cost_labelled … r)
     
    11691362| whd @(will_return_notfn … TERMINATES) %1 @CL
    11701363| @(stack_preserved_step … EV) /2/
    1171 | %{tr} @EV
     1364| %{tr} %{EV} %
    11721365| %2 whd @CL
    11731366| @(well_cost_labelled_state_step  … EV) //
    11741367| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
    1175 | cases (will_return_notfn … TERMINATES) #TM * #_ #EQ //
     1368| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
    11761369| @CL
    1177 | %{tr} @EV
     1370| %{tr} %{EV} %
    11781371| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
    11791372| @(well_cost_labelled_state_step  … EV) //
     
    11931386(* We can initialise TIME with a suitably large value based on the length of the
    11941387   termination proof. *)
    1195 let rec make_label_return' ge depth s
     1388let rec make_label_return' ge depth (s:RTLabs_state ge)
    11961389  (trace: flat_trace io_out io_in ge s)
    11971390  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    14061599] qed.
    14071600
    1408 lemma bound_after_call : ∀ge,s,s',n.
     1601lemma bound_after_call : ∀ge.∀s,s':RTLabs_state ge.∀n.
    14091602  state_bound_on_steps_to_cost s (S n) →
    14101603  ∀CL:RTLabs_classify s = cl_call.
     
    14121605  RTLabs_cost s' = false →
    14131606  state_bound_on_steps_to_cost s' n.
    1414 #ge #s #s' #n #H inversion H
     1607#ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); -stk -stk' lapply CL -CL inversion H
    14151608[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
    14161609  #fn * #args * #dst * #stk * #m' #E destruct
     
    14991692
    15001693definition soundly_labelled_ge : genv → Prop ≝
    1501 λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
     1694λge. ∀b,f. find_funct_ptr ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
    15021695
    15031696definition soundly_labelled_state : state → Prop ≝
     
    15701763   use the fact that the trace is soundly labelled to achieve this. *)
    15711764
    1572 record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
     1765record remainder_ok (ge:genv) (s:RTLabs_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
    15731766  ro_well_cost_labelled: well_cost_labelled_state s;
    15741767  ro_soundly_labelled: soundly_labelled_state s;
     
    15781771}.
    15791772
    1580 inductive finite_prefix (ge:genv) : state → Prop ≝
    1581 | fp_tal : ∀s,s'.
     1773inductive finite_prefix (ge:genv) : RTLabs_state ge → Prop ≝
     1774| fp_tal : ∀s,s':RTLabs_state ge.
    15821775           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
    15831776           ∀t:flat_trace io_out io_in ge s'.
    15841777           remainder_ok ge s' t →
    15851778           finite_prefix ge s
    1586 | fp_tac : ∀s1,s2,s3,tr.
     1779| fp_tac : ∀s1,s2,s3:RTLabs_state ge.
    15871780           trace_any_call (RTLabs_status ge) s1 s2 →
    15881781           well_cost_labelled_state s2 →
    1589            eval_statement ge s2 = Value ??? 〈tr,s3〉
     1782           as_execute (RTLabs_status ge) s2 s3
    15901783           ∀t:flat_trace io_out io_in ge s3.
    15911784           remainder_ok ge s3 t →
     
    15931786.
    15941787
    1595 definition fp_add_default : ∀ge,s,s'.
     1788definition fp_add_default : ∀ge. ∀s,s':RTLabs_state ge.
    15961789  RTLabs_classify s = cl_other →
    15971790  finite_prefix ge s' →
    1598   (∃t. eval_statement ge s = Value ??? 〈t,s'〉)
     1791  as_execute (RTLabs_status ge) s s'
    15991792  RTLabs_cost s' = false →
    16001793  finite_prefix ge s ≝
    16011794λge,s,s',OTHER,fp.
    1602 match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
     1795match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
    16031796[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
    16041797    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    16051798    rem rok
    1606 | fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr
     1799| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
    16071800    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
    16081801    WCL2 EV rem rok
    16091802].
    16101803
    1611 definition fp_add_terminating_call : ∀ge,s,s1,s''.
    1612   (∃t. eval_statement ge s = Value ??? 〈t,s1〉)
     1804definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_state ge.
     1805  as_execute (RTLabs_status ge) s s1
    16131806  ∀CALL:RTLabs_classify s = cl_call.
    16141807  finite_prefix ge s'' →
     
    16181811  finite_prefix ge s ≝
    16191812λge,s,s1,s'',EVAL,CALL,fp.
    1620 match fp return λs''.λ_. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
     1813match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
    16211814[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    16221815    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    16231816    rem rok
    1624 | fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr
     1817| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
    16251818    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    16261819    WCL2 EV rem rok
     
    16401833  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
    16411834
    1642 let rec finite_segment ge s n trace
     1835let rec finite_segment ge (s:RTLabs_state ge) n trace
    16431836  (ORACLE: termination_oracle)
    16441837  (TRACE_OK: remainder_ok ge s trace)
     
    16461839  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    16471840  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
    1648   on n : finite_prefix ge s ≝
     1841  on n : finite_prefix ge s ≝ 
    16491842match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
    16501843[ O ⇒ λLABEL_LIMIT. ⊥
    1651 | S n' ⇒
    1652     match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
    1653     [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
    1654     | ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT.
     1844| S n' ⇒
     1845  match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace'.
     1846    match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_state ge s ? mtc) with
     1847    [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
     1848    | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
     1849        let start' ≝ mk_RTLabs_state ge start stk mtc in
     1850        let next' ≝ next_state ge start' next tr EV in
    16551851        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
    16561852        [ cl_other ⇒ λCL.
     
    16581854            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
    16591855            [ true ⇒ λCS.
    1660                 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) trace' TRACE_OK'
     1856                fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK'
    16611857            | false ⇒ λCS.
    1662                 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    1663                 fp_add_default ge ?? CL fs ? CS
     1858                let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
     1859                fp_add_default ge start' next' CL fs ? CS
    16641860            ] (refl ??)
    16651861        | cl_jump ⇒ λCL.
    1666             fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' ?
     1862            fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ?
    16671863        | cl_call ⇒ λCL.
    1668             match ORACLE ge O next trace' return λ_. finite_prefix ge start with
     1864            match ORACLE ge O next trace' return λ_. finite_prefix ge start' with
    16691865            [ or_introl TERMINATES ⇒
    16701866              match TERMINATES with [ witness TERMINATES ⇒
    1671                 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
     1867                let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
    16721868                let TRACE_OK' ≝ ? in
    1673                 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
    1674                 [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) (RTLabs_costed … CS)) (remainder … tlr) TRACE_OK'
     1869                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
     1870                [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? CL ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
    16751871                | false ⇒ λCS.
    16761872                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
     
    16791875              ]
    16801876            | or_intror NO_TERMINATION ⇒
    1681                 fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EV trace' ?
     1877                fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' CL) ?? trace' ?
    16821878            ]
    16831879        | cl_return ⇒ λCL. ⊥
    16841880        ] (refl ??)
    1685     | ft_wrong start m NF EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
    1686     ] TRACE_OK
     1881    | ft_wrong start m NF EV ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
     1882    ] mtc0
     1883  ] trace TRACE_OK
    16871884] LABEL_LIMIT.
    16881885[ cases (state_bound_on_steps_to_cost_zero s) /2/
     
    16901887| @(absurd ?? (ro_no_termination … TRACE_OK))
    16911888     %{0} % @wr_base //
    1692 | @RTLabs_costed @(well_cost_labelled_jump … EV) /2/
    1693 | 5,6,8,9,10,11: /3/
    1694 | % [ @(well_cost_labelled_state_step … EV) /2/
    1695     | @(soundly_labelled_state_step … EV) /2/
     1889| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
     1890| 5,6,9,10,11: /3/
     1891| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
     1892  % [ @(well_cost_labelled_state_step … EV) //
     1893    | @(soundly_labelled_state_step … EV) //
    16961894    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
    1697     | @(still_not_wrong … EV) /2/
     1895    | @(still_not_wrong … EV) //
    16981896    | @(not_return_to_not_final … EV) >CL % #E destruct
    16991897    ]
    1700 | /2/
    1701 | @(bound_after_call ge … LABEL_LIMIT CL ? CS)
    1702   @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
     1898| @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
     1899| @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
     1900| @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)
     1901  @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
    17031902| % [ /2/
    17041903    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
    1705       @(soundly_labelled_state_step … EV) /2/
     1904      @(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK)
    17061905    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
    17071906      @wr_call //
     
    17091908      cases (terminates … tlr) //
    17101909    | @(will_return_not_wrong … TERMINATES)
    1711       [ @(still_not_wrong … EV) /2/
     1910      [ @(still_not_wrong … EV) @(ro_not_undefined … TRACE_OK)
    17121911      | cases (terminates … tlr) //
    17131912      ]
     
    17161915      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
    17171916      | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
    1718       | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
     1917      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct whd in S:(??%); -next' -s0
    17191918        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
    17201919        inversion (eval_preserves … EV)
    1721         [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ]
    1722         #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
     1920        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 @⊥ -next destruct ]
     1921        #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
    17231922        inversion S
    17241923        [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
     
    17301929      ]
    17311930    ]
    1732 | @(well_cost_labelled_state_step … EV) /2/
    1733 | @(well_cost_labelled_call … EV) /2/
     1931| @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK)
     1932| @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    17341933| /2/
    1735 | % [ @(well_cost_labelled_state_step … EV) /2/
     1934| %{tr} %{EV} %
     1935| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
     1936  % [ @(well_cost_labelled_state_step … EV) /2/
    17361937    | @(soundly_labelled_state_step … EV) /2/
    17371938    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
     
    17401941    | @(not_return_to_not_final … EV) >CL % #E destruct
    17411942    ]
    1742 | 19,20,21: /2/
     1943| %2 @CL
     1944| 21,22: %{tr} %{EV} %
    17431945| cases (bound_after_step … LABEL_LIMIT EV ?)
    17441946  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
     
    17651967  | //
    17661968  ]
    1767 | % [ @(well_cost_labelled_state_step … EV) /2/
    1768     | @(soundly_labelled_state_step … EV) /2/
     1969| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
     1970  % [ @(well_cost_labelled_state_step … EV) //
     1971    | @(soundly_labelled_state_step … EV) //
    17691972    | @(not_to_not … (ro_no_termination … TRACE_OK))
    17701973      * #depth * #TERM %{depth} % @wr_step /2/
     
    17841987*)
    17851988
    1786 let corec make_label_diverges ge s
     1989let corec make_label_diverges ge (s:RTLabs_state ge)
    17871990  (trace: flat_trace io_out io_in ge s)
    17881991  (ORACLE: termination_oracle)
     
    17951998[ ex_intro n B ⇒
    17961999    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
    1797       return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
     2000      return λs:RTLabs_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
    17982001    with
    17992002    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
    18002003        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    1801             tld_step (RTLabs_status ge) s s' (tll_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) T'
     2004            tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T'
    18022005(*
    18032006        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
     
    18052008            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
    18062009        ]*)
    1807     | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
     2010    | fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
    18082011        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    1809             tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) ?? T'
     2012            tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T'
    18102013(*
    18112014        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
     
    18152018    ] STATEMENT_COSTLABEL
    18162019].
    1817 [ @(costed_RTLabs ge) @(trace_any_label_label … T)
    1818 | %{tr} @EV
     2020[ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
     2021| @EV
    18192022| @(trace_any_call_call … T)
    1820 | @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
     2023| cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // @(trace_any_call_call … T)
    18212024] qed.
    18222025
     
    18522055qed.
    18532056
    1854 let rec whole_structured_trace_exists ge p s
    1855   (trace: flat_trace io_out io_in ge s)
     2057let rec whole_structured_trace_exists ge p (s:RTLabs_state ge)
    18562058  (ORACLE: termination_oracle)
    18572059  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    18582060  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    1859   : ∀INITIAL: make_initial_state p = OK ? s.
     2061  : ∀trace: flat_trace io_out io_in ge s.
     2062    ∀INITIAL: make_initial_state p = OK state s.
    18602063    ∀NOT_WRONG: not_wrong ??? s trace.
    18612064    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
    18622065    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
    1863     trace_whole_program_exists (RTLabs_status ge) s ≝
    1864 match trace return λs,trace. make_initial_state p = OK ? s →
     2066    trace_whole_program_exists (RTLabs_status ge) s ≝
     2067match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
     2068                   make_initial_state p = OK ? s →
     2069                   not_wrong ??? s trace →
     2070                   well_cost_labelled_state s →
     2071                   soundly_labelled_state s →
     2072                   trace_whole_program_exists (RTLabs_status ge) s with
     2073[ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace.
     2074match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
     2075                             make_initial_state p = OK state s →
    18652076                             not_wrong ??? s trace →
    18662077                             well_cost_labelled_state s →
    18672078                             soundly_labelled_state s →
    1868                              trace_whole_program_exists (RTLabs_status ge) s with
    1869 [ ft_step s tr next EV trace' ⇒ λINITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
     2079                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with
     2080[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
    18702081    let IS_CALL ≝ initial_state_is_call … INITIAL in
     2082    let s' ≝ mk_RTLabs_state ge s stk mtc in
     2083    let next' ≝ next_state ge s' next tr EV in
    18712084    match ORACLE ge O next trace' with
    18722085    [ or_introl TERMINATES ⇒
    18732086        match TERMINATES with
    18742087        [ witness TERMINATES ⇒
    1875           let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
    1876           twp_terminating (RTLabs_status ge) s next (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
     2088          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
     2089          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
    18772090        ]
    1878     | or_intror NO_TERMINATION ⇒
    1879         twp_diverges (RTLabs_status ge) s next IS_CALL ?
    1880          (make_label_diverges ge next trace' ORACLE ?
     2091    | or_intror NO_TERMINATION ⇒ 
     2092        twp_diverges (RTLabs_status ge) s' next' IS_CALL ?
     2093         (make_label_diverges ge next' trace' ORACLE ?
    18812094            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
    18822095    ]
    1883 | ft_stop st FINAL ⇒ λINITIAL,NOT_WRONG. ⊥
    1884 | ft_wrong start m NF EV ⇒ λINITIAL,NOT_WRONG. ⊥
    1885 ].
     2096| ft_stop st FINAL ⇒ λmtc,INITIAL,NOT_WRONG. ⊥
     2097| ft_wrong start m NF EV ⇒ λmtc,INITIAL,NOT_WRONG. ⊥
     2098] mtc0 ].
    18862099[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
    18872100  cases FINAL #E @E @refl
    1888 | %{tr} @EV
     2101| %{tr} %{EV} %
    18892102| @(after_the_initial_call_is_the_final_state … INITIAL EV)
    18902103  @(stack_ok … tlr)
    18912104| @(well_cost_labelled_state_step … EV) //
    18922105| @(well_cost_labelled_call … EV) //
    1893 | %{tr} @EV
     2106| %{tr} %{EV} %
    18942107| @(well_cost_labelled_call … EV) //
    18952108| % [ @(well_cost_labelled_state_step … EV) //
     
    19292142*)
    19302143
     2144lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
     2145  as_execute (RTLabs_status ge) s s' →
     2146  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
     2147#ge #s #s' * #tr * #EX #_ %{tr} @EX
     2148qed.
     2149
    19312150(* as_execute might be in Prop, but because the semantics is deterministic
    19322151   we can retrieve the event trace anyway. *)
    1933 let rec deprop_as_execute ge s s'
    1934   (X:as_execute (RTLabs_status ge) s s')
     2152
     2153let rec deprop_execute ge (s,s':state)
     2154  (X:∃t. eval_statement ge s = Value … 〈t,s'〉)
    19352155: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
    1936 match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = ? with
     2156match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
    19372157[ Value ts ⇒ λY. «fst … ts, ?»
    19382158| _ ⇒ λY. ⊥
     
    19412161| cases Y #trP #E destruct @refl
    19422162] qed.
     2163
     2164let rec deprop_as_execute ge (s,s':RTLabs_state ge)
     2165  (X:as_execute (RTLabs_status ge) s s')
     2166: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
     2167deprop_execute ge s s' ?.
     2168cases X #tr * #EX #_ %{tr} @EX
     2169qed.
    19432170
    19442171(* A non-empty finite section of a flat_trace *)
     
    19642191
    19652192(* Extract a flat trace from a structured one. *)
    1966 let rec flat_trace_of_label_return ge s s'
     2193let rec flat_trace_of_label_return ge (s,s':RTLabs_state ge)
    19672194  (tr:trace_label_return (RTLabs_status ge) s s')
    19682195on tr :
     
    19752202    (flat_trace_of_label_return ge s2 s3 tlr)
    19762203]
    1977 and flat_trace_of_label_label ge ends s s'
     2204and flat_trace_of_label_label ge ends (s,s':RTLabs_state ge)
    19782205  (tr:trace_label_label (RTLabs_status ge) ends s s')
    19792206on tr :
     
    19822209[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
    19832210]
    1984 and flat_trace_of_any_label ge ends s s'
     2211and flat_trace_of_any_label ge ends (s,s':RTLabs_state ge)
    19852212  (tr:trace_any_label (RTLabs_status ge) ends s s')
    19862213on tr :
     
    20132240(* We take an extra step so that we can always return a non-empty trace to
    20142241   satisfy the guardedness condition in the cofixpoint. *)
    2015 let rec flat_trace_of_any_call ge s s' s'' et
     2242let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_state ge) et
    20162243  (tr:trace_any_call (RTLabs_status ge) s s')
    20172244  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
    20182245on tr :
    2019   partial_flat_trace io_out io_in ge s s'' ≝
    2020 match tr return λs,s'.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
     2246  partial_flat_trace io_out io_in ge s s'' ≝ 
     2247match tr return λs,s':RTLabs_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
    20212248[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
    20222249| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
     
    20342261] EX''.
    20352262
    2036 let rec flat_trace_of_label_call ge s s' s'' et
     2263let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_state ge) et
    20372264  (tr:trace_label_call (RTLabs_status ge) s s')
    20382265  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
     
    20462273   to take care to satisfy the guardedness condition by witnessing the fact that
    20472274   the partial traces are non-empty. *)
    2048 let corec flat_trace_of_label_diverges ge s
     2275let corec flat_trace_of_label_diverges ge (s:RTLabs_state ge)
    20492276  (tr:trace_label_diverges (RTLabs_status ge) s)
    20502277: flat_trace io_out io_in ge s ≝
    2051 match tr with
     2278match tr return λs:RTLabs_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
    20522279[ tld_step sx sy tll tld ⇒
    2053     match flat_trace_of_label_label ge … tll with
    2054     [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    2055     | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
    2056     ] tld
    2057 | tld_base s1 s2 s3 tlc EX CL tld ⇒
    2058     match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    2059       match flat_trace_of_label_call … tlc EX' with
    2060       [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    2061       | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
    2062       ] tld
    2063     ]
     2280  match sy in RTLabs_state return λsy:RTLabs_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_state sy' stk mtc0 ⇒
     2281    λtll.
     2282    match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s2 stk mtc) → flat_trace ??? s1 with
     2283    [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
     2284    | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_state ge s3 stk mtc) tr' tld)
     2285    ] mtc0 ] tll tld
     2286| tld_base s1 s2 s3 tlc EX CL tld ⇒
     2287  match s3 in RTLabs_state return λs3:RTLabs_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_state s3' stk mtc0 ⇒
     2288    λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
     2289      match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s3 stk mtc) → flat_trace ??? s1 with
     2290      [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
     2291      | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_state ge s3 stk mtc) tr' tld)
     2292      ] mtc0
     2293    ]
     2294  ] EX tld
    20642295]
    20652296(* Helper to keep adding the partial trace without violating the guardedness
    20662297   condition. *)
    2067 and add_partial_flat_trace ge s s'
    2068   (ptr:partial_flat_trace io_out io_in ge s s')
    2069   (tr:trace_label_diverges (RTLabs_status ge) s')
    2070 : flat_trace io_out io_in ge s ≝
    2071 match ptr with
    2072 [ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flat_trace_of_label_diverges ge s' tr)
    2073 | pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr)
    2074 ] tr
    2075 .
     2298and add_partial_flat_trace ge (s:state) (s':RTLabs_state ge)
     2299: partial_flat_trace io_out io_in ge s s' →
     2300  trace_label_diverges (RTLabs_status ge) s' →
     2301  flat_trace io_out io_in ge s ≝
     2302match s' return λs':RTLabs_state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_state sx stk mtc ⇒
     2303λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s' ? mtc) → flat_trace io_out io_in ge s with
     2304[ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
     2305| pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_state ge s3 stk mtc) tr' tr)
     2306] mtc ]
     2307.
     2308
    20762309
    20772310coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
     
    21282361] qed.
    21292362
    2130 let corec diverging_traces_have_unique_flat_trace ge s
     2363let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
    21312364  (str:trace_label_diverges (RTLabs_status ge) s)
    21322365  (tr:flat_trace io_out io_in ge s)
     
    21352368qed.
    21362369
    2137 let rec flat_trace_of_whole_program ge s
     2370let rec flat_trace_of_whole_program ge (s:RTLabs_state ge)
    21382371  (tr:trace_whole_program (RTLabs_status ge) s)
    21392372on tr : flat_trace io_out io_in ge s ≝
    2140 match tr with
     2373match tr return λs:RTLabs_state ge.λtr. flat_trace io_out io_in ge s with
    21412374[ twp_terminating s1 s2 sf CL EX tlr F ⇒
    2142     match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 
    2143       ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … sf F))
     2375    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
     2376      ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))
    21442377    ]
    21452378| twp_diverges s1 s2 CL EX tld ⇒
     
    21492382].
    21502383
    2151 let corec whole_traces_have_unique_flat_trace ge s
     2384let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
    21522385  (str:trace_whole_program (RTLabs_status ge) s)
    21532386  (tr:flat_trace io_out io_in ge s)
  • src/RTLabs/semantics.ma

    r2025 r2044  
    256256.
    257257
    258 lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop.
     258lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Type[0].
    259259  (∀a. e = OK A a → f a = OK ? v → P v) →
    260260  (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v).
     
    305305] qed.
    306306
     307(* Show that, in principle at least, we can calculate which function we called
     308   on a transition. The proof is a functional inversion similar to eval_preserves,
     309   above. *)
     310
     311definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m.
     312  eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 →
     313  Σb:block. find_funct_ptr … ge b = Some ? fd.
     314#ge *
     315[ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
     316  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     317  cases (lookup_present … nok)
     318  (* Function call cases. *)
     319  [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct
     320    [ %{v} @Efd
     321    | cases v in Efd;
     322      [ 5: * #pty #b #pc #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
     323           [ #E @E | #E normalize in E; destruct ]
     324      | *: normalize #A try #B try #C destruct
     325      ]
     326    ]
     327  (* and everything else cannot occur, but we need to work through the
     328     definition to find the resulting state to demonstrate that. *)
     329  | #l #LP whd in ⊢ (??%? → ?); #E destruct
     330  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct
     331  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct
     332  | #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
     333  | #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
     334  | #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
     335  | #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
     336  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
     337  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct ] | *: #vl #E whd in E:(??%?); destruct ]
     338  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct
     339  ]
     340| * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m'
     341  whd in ⊢ (??%? → ?);
     342  [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     343    #E destruct
     344  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
     345  ]
     346| #v #r * [2: #f #fs ] #m #tr #fd' #args' #dst' #fs' #m'
     347  whd in ⊢ (??%? → ?);
     348  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
     349  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct | *: normalize #a try #b destruct ] ]
     350  ]
     351| #r #tr #fd' #args' #dst' #fs' #m'
     352  normalize #E destruct
     353] qed.
     354
    307355
    308356lemma initial_state_is_not_final : ∀p,s.
  • src/common/IOMonad.ma

    r1976 r2044  
    367367
    368368(* Inversion when injecting errors into IO monad. *)
    369 lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     369lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0].
    370370  (∀a. e = OK A a → f a = OK B v → P v) →
    371371  (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
     
    376376] qed.
    377377
    378 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     378lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0].
    379379  (∀a. e = Value ??? a → f a = Value ??? v → P v) →
    380380  (bindIO O I A B e f = Value ??? v → P v).
  • src/common/StructuredTraces.ma

    r1976 r2044  
    250250(* Version in Prop for showing existence. *)
    251251coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
    252   | tld_step:
     252  | tld_step':
    253253      ∀status_initial: S.
    254254      ∀status_labelled: S.
     
    256256          trace_label_diverges_exists S status_labelled →
    257257            trace_label_diverges_exists S status_initial
    258   | tld_base:
     258  | tld_base':
    259259      ∀status_initial: S.
    260260      ∀status_pre_fun_call: S.
Note: See TracChangeset for help on using the changeset viewer.