Changeset 2499 for src/RTLabs


Ignore:
Timestamp:
Nov 28, 2012, 12:52:12 PM (7 years ago)
Author:
campbell
Message:

Separate out the RTLabs abstract status record from the proofs about
structured traces. Tidy up "next instruction" references from
the semantics.

Location:
src/RTLabs
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2439 r2499  
    11
    2 include "RTLabs/semantics.ma".
     2include "RTLabs/abstract.ma".
    33include "RTLabs/CostSpec.ma".
    44include "RTLabs/CostMisc.ma".
    5 include "common/StructuredTraces.ma".
    65include "common/Executions.ma".
    7 include "utilities/deqsets.ma".
    86include "utilities/listb.ma".
    97
    10 discriminator status_class.
    11 
    12 (* We augment states with a stack of function blocks (i.e. pointers) so that we
    13    can make sensible "program counters" for the abstract state definition, along
    14    with a proof that we will get the correct code when we do the lookup (which
    15    is done to find cost labels given a pc).
    16    
    17    Adding them to the semantics is an alternative, more direct approach.
    18    However, it makes animating the semantics extremely difficult, because it
    19    is hard to avoid normalising and displaying irrelevant parts of the global
    20    environment and proofs.
    21    
    22    We use blocks rather than identifiers because the global environments go
    23 
    24      identifier → block → definition
    25    
    26    and we'd have to introduce backwards lookups to find identifiers for
    27    function pointers.
    28  *)
    29 
    30 definition Ras_Fn_Match ≝
    31 λge,state,fn_stack.
    32   match state with
    33   [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
    34   | Callstate fd _ _ fs _ ⇒
    35       match fn_stack with
    36       [ nil ⇒ False
    37       | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
    38         All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
    39       ]
    40   | Returnstate _ _ fs _ ⇒
    41       All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
    42   | Finalstate _ ⇒ fn_stack = [ ]
    43   ].
    44 
    45 record RTLabs_state (ge:genv) : Type[0] ≝ {
    46   Ras_state :> state;
    47   Ras_fn_stack : list block;
    48   Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
    49 }.
    50 
    51 (* Given a plain step of the RTLabs semantics, give the next state along with
    52    the shadow stack of function block numbers.  Carefully defined so that the
    53    coercion back to the plain state always reduces. *)
    54 definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
    55   eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
    56 λge,s,s',t,EX. mk_RTLabs_state ge s'
    57  (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)
    58  ?.
    59 cases s' in EX ⊢ %;
    60 [ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
    61   [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    62     whd cases stk in mtc ⊢ %; [ * ]
    63     #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
    64     | @M2 ]
    65   | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
    66   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    67     whd cases stk in mtc ⊢ %; [ * ]
    68     #hd #tl #H @H
    69   | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
    70   | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
    71     cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
    72     [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
    73   | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    74   ]
    75 | -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
    76   whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    77   [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    78   | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
    79     cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
    80     [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
    81   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    82   | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
    83   | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
    84   | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    85   ]
    86 | -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    87   [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    88   | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
    89   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    90   | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
    91     cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
    92   | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
    93   | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    94   ]
    95 | #r #EX whd @refl
    96 ] qed.
    97 
    98 
    99 (* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
    100        will be added later (LTL → LIN). *)
    101 
    102 definition RTLabs_classify : state → status_class ≝
    103 λs. match s with
    104 [ State f _ _ ⇒
    105     match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
    106     [ St_cond _ _ _ ⇒ cl_jump
    107 (*    | St_jumptable _ _ ⇒ cl_jump*)
    108     | _ ⇒ cl_other
    109     ]
    110 | Callstate _ _ _ _ _ ⇒ cl_call
    111 | Returnstate _ _ _ _ ⇒ cl_return
    112 | Finalstate _ ⇒ cl_other
    113 ].
    114 
    115 (* As with is_cost_label/cost_label_of we define a boolean function as well
    116    as one which extracts the cost label so that we can use it in hypotheses
    117    without naming the cost label. *)
    118 
    119 definition RTLabs_cost : state → bool ≝
    120 λs. match s with
    121 [ State f fs m ⇒
    122     is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
    123 | _ ⇒ false
    124 ].
    125 
    126 definition RTLabs_cost_label : state → option costlabel ≝
    127 λs. match s with
    128 [ State f fs m ⇒
    129     cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
    130 | _ ⇒ None ?
    131 ].
    132 
    133 (* "Program counters" need to identify the current state, either as a pair of
    134    the function and current instruction, or the function being entered or
    135    left.  Functions are identified by their function pointer block because
    136    this avoids introducing functions to map back pointers to function ids using
    137    the global environment.  (See the comment at the start of this file, too.)
    138    
    139    Calls also get the caller's instruction label (or None for the initial call)
    140    so that we can distinguish different calls.  This is used only for the
    141    t.*_unrepeating property, which includes the pc for call states.
    142     *)
    143 
    144 inductive RTLabs_pc : Type[0] ≝
    145 | rapc_state : block → label → RTLabs_pc
    146 | rapc_call : option label → block → RTLabs_pc
    147 | rapc_ret : option block → RTLabs_pc
    148 | rapc_fin : RTLabs_pc
    149 .
    150 
    151 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
    152 λx,y. match x with
    153 [ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
    154 | rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒
    155     eqb ? o1 o2
    156     ∧ eq_block b1 b2
    157   | _ ⇒ false ]
    158 | rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ]
    159 | rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
    160 ].
    161 
    162 definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
    163 whd in match RTLabs_pc_eq;
    164 * [ #b1 #l1 | #bl1 #b1 | #ob1 | ]
    165 * [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ]
    166 normalize nodelta
    167 [ @eq_block_elim [ #E destruct | * #NE ] ]
    168 [ @eq_identifier_elim [ #E destruct | *: * #NE ] ]
    169 [ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ]
    170 [ @eq_block_elim [ #E destruct | * #NE ] ]
    171 normalize % #E destruct try (cases (NE (refl ??))) @refl
    172 qed.
    173 
    174 definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝
    175 λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒
    176 match s' return λs'. Ras_Fn_Match ? s' ? → ? with
    177 [ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
    178 | Callstate _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
    179 | Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
    180 | Finalstate _ ⇒ λmtc. rapc_fin
    181 ] mtc0 ].
    182 whd in mtc; cases mtc
    183 qed.
    184 
    185 definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
    186 λge,pc.
    187 match pc with
    188 [ rapc_state b l ⇒
    189   match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
    190     match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
    191 | _ ⇒ None ?
    192 ].
    193 
    194 (* After returning from a function, we should be ready to execute the next
    195    instruction of the caller and the shadow stack should be preserved (we have
    196    to take the top element off because the Callstate includes the callee); *or*
    197    we're in the final state.
    198  *)
    199 
    200 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → RTLabs_state ge → Prop ≝
    201 λge,s,s'.
    202   match s with
    203   [ mk_Sig s p ⇒
    204     match s return λs. RTLabs_classify s = cl_call → ? with
    205     [ Callstate fd args dst stk m ⇒
    206       λ_. match s' with
    207       [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
    208           next h = next f ∧
    209           f_graph (func h) = f_graph (func f) ∧
    210           match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]
    211       | Finalstate r ⇒ stk = [ ]
    212       | _ ⇒ False
    213       ]
    214    | State f fs m ⇒ λH.⊥
    215    | _ ⇒ λH.⊥
    216    ] p
    217  ].
    218 [ whd in H:(??%?);
    219   cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
    220   normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
    221 | normalize in H; destruct
    222 | normalize in H; destruct
    223 ] qed.
    224 
    225 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → ident ≝
    226 λge,s.
    227   match s with
    228   [ mk_Sig s p ⇒
    229     match s return λs':RTLabs_state ge. RTLabs_classify s' = cl_call → ident with
    230     [ mk_RTLabs_state s' stk mtc0 ⇒
    231       match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
    232       [ Callstate fd _ _ _ _ ⇒
    233         match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
    234         [ nil ⇒ λmtc. ⊥
    235         | cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ?
    236         ]
    237       | State f _ _ ⇒ λ_. λH.⊥
    238       | _ ⇒ λ_. λH.⊥
    239       ] mtc0
    240     ] p
    241   ].
    242 [ whd in H:(??%?);
    243   cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
    244   normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
    245 | 4,5: normalize in H; destruct (H)
    246 | cases mtc
    247 | cases mtc #FFP #_ >FFP % #E destruct (E)
    248 ] qed.
    249 
    250 
    251 definition RTLabs_status : genv → abstract_status ≝
    252 λge.
    253   mk_abstract_status
    254     (RTLabs_state ge)
    255     (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
    256     RTLabs_deqset
    257     (RTLabs_state_to_pc ge)
    258     RTLabs_classify
    259     (RTLabs_pc_to_cost_label ge)
    260     (RTLabs_after_return ge)
    261     (λs. RTLabs_is_final s ≠ None ?)
    262     (RTLabs_call_ident ge).
    2638
    2649(* Allow us to move between the different notions of when a state is cost
    26510   labelled. *)
    26611
    267 lemma RTLabs_costed : ∀ge. ∀s:RTLabs_state ge.
     12lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
    26813  RTLabs_cost s = true ↔
    26914  as_costed (RTLabs_status ge) s.
     
    27520  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
    27621  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
    277   >(lookup_lookup_present … nok)
    278   whd in ⊢ (?(??%?)(?(??%?)));
     22  whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
     23  >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
    27924  % cases (lookup_present ?? (f_graph func) ??) normalize
    28025  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
     
    29944] qed.
    30045
    301 lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_state ge.
     46lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
    30247  RTLabs_cost s = false →
    30348  ¬ as_costed (RTLabs_status ge) s.
     
    718463  RTLabs_classify s = cl_jump →
    719464  ∃f,fs,m. s = State f fs m ∧
    720   let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
    721   (∃r,l1,l2. stmt = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
     465  (∃r,l1,l2. next_instruction f = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
    722466*
    723467[ #f #fs #m #E
    724468  %{f} %{fs} %{m} %
    725469  [ @refl
    726   | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
     470  | whd in E:(??%?); cases (next_instruction f) in E ⊢ %;
    727471    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
    728472    (*[ %1*) %{A} %{B} %{C} @refl
     
    751495  lapply (Hbody (next fr) (next_ok fr))
    752496  generalize in ⊢ (?(???%) → ?);
     497  change with (next_instruction fr) in match (lookup_present ?????);
    753498  >Estmt #LP' #WS
    754499  cases (andb_Prop_true … WS) #H1 #H2 [ @H1 | @H2 ]
     
    777522  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
    778523* [ #f #fs #m whd in ⊢ (??%? → ?);
    779     cases (lookup_present … (next f) (next_ok f)) normalize
     524    cases (next_instruction f) normalize
    780525    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
    781526  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
     
    808553(* Extend our information about steps to states extended with the shadow stack. *)
    809554
    810 inductive state_rel_ext : ∀ge:genv. RTLabs_state ge → RTLabs_state ge → Prop ≝
    811 | xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (State f fs m) S M) (mk_RTLabs_state ge (State f' fs m') S M')
    812 | xto_call : ∀ge,f,fs,m,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (State f fs m) S M) (mk_RTLabs_state ge (Callstate fd args dst (f'::fs) m) (fn::S) M')
    813 | xfrom_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_state ge (Callstate (Internal ? fn) args dst fs m) S M) (mk_RTLabs_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
    814 | xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) (mk_RTLabs_state ge (Returnstate rtv dst fs m') S M')
    815 | xfrom_ret : ∀ge,f,fs,rtv,dst,f',m,S,M,M'. next f = next f' → frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_state ge (State f' fs m) S M')
    816 | xfinish : ∀ge,r,dst,m,M,M'. state_rel_ext ge (mk_RTLabs_state ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) [ ] M) (mk_RTLabs_state ge (Finalstate r) [ ] M')
     555inductive state_rel_ext : ∀ge:genv. RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
     556| xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (State f' fs m') S M')
     557| xto_call : ∀ge,f,fs,m,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (Callstate fd args dst (f'::fs) m) (fn::S) M')
     558| xfrom_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Callstate (Internal ? fn) args dst fs m) S M) (mk_RTLabs_ext_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
     559| xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m') S M')
     560| xfrom_ret : ∀ge,f,fs,rtv,dst,f',m,S,M,M'. next f = next f' → frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_ext_state ge (State f' fs m) S M')
     561| xfinish : ∀ge,r,dst,m,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) [ ] M) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M')
    817562.
    818563
     
    858603 *)
    859604
    860 inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_state ge → Prop ≝
    861 | sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_state ge (State f fs m) (fn::S) M)
    862 | sos_Callstate : ∀fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_state ge (Callstate fd args dst (f::fs) m) (fn::fn'::S) M)
    863 | sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_state ge (Returnstate rtv dst fs m) S M)
     605inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ext_state ge → Prop ≝
     606| sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M)
     607| sos_Callstate : ∀fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Callstate fd args dst (f::fs) m) (fn::fn'::S) M)
     608| sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m) S M)
    864609.
    865610
    866 inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_state ge → RTLabs_state ge → Prop ≝
     611inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
    867612| sp_normal : ∀fs,S,s1,s2.
    868613    stack_of_state ge fs S s1 →
     
    873618    frame_rel f f' →
    874619    stack_of_state ge (f::fs) (fn::S) s1 →
    875     stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (State f' fs m) (fn::S) M)
     620    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (State f' fs m) (fn::S) M)
    876621| sp_stop : ∀s1,r,M.
    877622    stack_of_state ge [ ] [ ] s1 →
    878     stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (Finalstate r) [ ] M)
     623    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (Finalstate r) [ ] M)
    879624| sp_top : ∀fd,args,dst,m,r,fn,M1,M2.
    880     stack_preserved ge doesnt_end_with_ret (mk_RTLabs_state ge (Callstate fd args dst [ ] m) [fn] M1) (mk_RTLabs_state ge (Finalstate r) [ ] M2)
     625    stack_preserved ge doesnt_end_with_ret (mk_RTLabs_ext_state ge (Callstate fd args dst [ ] m) [fn] M1) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M2)
    881626.
    882627
     
    897642
    898643lemma stack_preserved_final : ∀ge,e,r,S,M,s.
    899   ¬stack_preserved ge e (mk_RTLabs_state ge (Finalstate r) S M) s.
     644  ¬stack_preserved ge e (mk_RTLabs_ext_state ge (Finalstate r) S M) s.
    900645#ge #e #r #S #M #s % #H inversion H
    901646[ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
     
    938683   returning. *)
    939684
    940 lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_state ge.∀cl.
     685lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_ext_state ge.∀cl.
    941686  RTLabs_classify s1 = cl →
    942687  as_execute (RTLabs_status ge) s1 s2 →
     
    949694#ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX)
    950695[ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
    951   whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
     696  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
    952697| #ge #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
    953   whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
     698  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
    954699| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
    955700  * #s3 #S3 #M3 #SP inversion SP
     
    969714  ]
    970715| #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct
    971   whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) /2/
     716  whd in match (RTLabs_classify ?); cases (next_instruction f) /2/
    972717| #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd
    973718  cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) //
     
    975720] qed.
    976721
    977 lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_state ge.∀s2,tr.
     722lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_ext_state ge.∀s2,tr.
    978723  ∀EV:eval_statement ge s1 = Value … 〈tr,s2〉.
    979724  as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV).
     
    981726qed.
    982727
    983 lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.
     728lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
    984729  ∀CL : RTLabs_classify s1 = cl_call.
    985730  as_execute (RTLabs_status ge) s1 s2 →
     
    1019764   of the termination proof is respected. *)
    1020765record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
    1021   (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
     766  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
    1022767  (original_terminates: will_return ge depth start full)
    1023   (T:RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
     768  (T:RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
    1024769{
    1025   new_state : RTLabs_state ge;
     770  new_state : RTLabs_ext_state ge;
    1026771  remainder : flat_trace io_out io_in ge new_state;
    1027772  cost_labelled : well_cost_labelled_state new_state;
     
    1039784   encountering a label. *)
    1040785record sub_trace_result (ge:genv) (depth:nat)
    1041   (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
     786  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
    1042787  (original_terminates: will_return ge depth start full)
    1043   (T:trace_ends_with_ret → RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
     788  (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
    1044789{
    1045790  ends : trace_ends_with_ret;
     
    1051796   the size of the termination proof might need to be relaxed, too. *)
    1052797
    1053 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
     798definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    1054799  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
    1055800    will_return_end … TM1 = will_return_end … TM2 →
     
    1080825] qed.
    1081826
    1082 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
     827definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    1083828  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
    1084829    will_return_end … TM1 = will_return_end … TM2 →
     
    1094839definition myge : nat → nat → Prop ≝ ge.
    1095840
    1096 let rec make_label_return ge depth (s:RTLabs_state ge)
     841let rec make_label_return ge depth (s:RTLabs_ext_state ge)
    1097842  (trace: flat_trace io_out io_in ge s)
    1098843  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    1135880
    1136881
    1137 and make_label_label ge depth (s:RTLabs_state ge)
     882and make_label_label ge depth (s:RTLabs_ext_state ge)
    1138883  (trace: flat_trace io_out io_in ge s)
    1139884  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    1158903
    1159904
    1160 and make_any_label ge depth (s0:RTLabs_state ge)
     905and make_any_label ge depth (s0:RTLabs_ext_state ge)
    1161906  (trace: flat_trace io_out io_in ge s0)
    1162907  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    1172917[ O ⇒ λTERMINATES_IN_TIME. ⊥
    1173918| S TIME ⇒ λTERMINATES_IN_TIME.
    1174   match s0 return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
     919  match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
    1175920                                      well_cost_labelled_state s →
    1176921                                      ∀TM:will_return ??? trace.
    1177922                                      myge ? (times 3 (will_return_length ??? trace TM)) →
    1178923                                      sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
    1179   with [ mk_RTLabs_state s stk mtc0 ⇒ λtrace.
     924  with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace.
    1180925  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
    1181926                               well_cost_labelled_state s →
    1182927                               ∀TM:will_return ??? trace.
    1183928                               myge ? (times 3 (will_return_length ??? trace TM)) →
    1184                                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
     929                               sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
    1185930  [ ft_stop st FINAL ⇒
    1186931      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
    1187932
    1188933  | ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    1189     let start' ≝ mk_RTLabs_state ge start stk mtc in
     934    let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
    1190935    let next' ≝ next_state ? start' ?? EV in
    1191936    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
     
    13421087(* We can initialise TIME with a suitably large value based on the length of the
    13431088   termination proof. *)
    1344 let rec make_label_return' ge depth (s:RTLabs_state ge)
     1089let rec make_label_return' ge depth (s:RTLabs_ext_state ge)
    13451090  (trace: flat_trace io_out io_in ge s)
    13461091  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    13861131lemma eval_successor : ∀ge,f,fs,m,tr,s'.
    13871132  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
    1388   (RTLabs_classify s' = cl_return ∧ successors (lookup_present … (f_graph (func f)) (next f) (next_ok f)) = [ ]) ∨
    1389   ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
     1133  (RTLabs_classify s' = cl_return ∧ successors (next_instruction f) = [ ]) ∨
     1134  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (next_instruction f)).
    13901135#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
    13911136whd in ⊢ (??%? → ?);
    1392 generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
     1137generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?)
    13931138[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    13941139| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     
    14911236lemma eval_steps : ∀ge,f,fs,m,tr,s'.
    14921237  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
    1493   steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
     1238  steps_for_statement (next_instruction f) =
    14941239  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
    14951240#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
    14961241whd in ⊢ (??%? → ?);
    1497 generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
     1242generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?)
    14981243[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
    14991244| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
     
    15171262] qed.
    15181263
    1519 lemma bound_after_call : ∀ge.∀s,s':RTLabs_state ge.∀n.
     1264lemma bound_after_call : ∀ge.∀s,s':RTLabs_ext_state ge.∀n.
    15201265  state_bound_on_steps_to_cost s (S n) →
    15211266  ∀CL:RTLabs_classify s = cl_call.
     
    16761421   use the fact that the trace is soundly labelled to achieve this. *)
    16771422
    1678 record remainder_ok (ge:genv) (s:RTLabs_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
     1423record remainder_ok (ge:genv) (s:RTLabs_ext_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
    16791424  ro_well_cost_labelled: well_cost_labelled_state s;
    16801425  ro_soundly_labelled: soundly_labelled_state s;
     
    16831428}.
    16841429
    1685 inductive finite_prefix (ge:genv) : RTLabs_state ge → Prop ≝
    1686 | fp_tal : ∀s,s':RTLabs_state ge.
     1430inductive finite_prefix (ge:genv) : RTLabs_ext_state ge → Prop ≝
     1431| fp_tal : ∀s,s':RTLabs_ext_state ge.
    16871432           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
    16881433           ∀t:flat_trace io_out io_in ge s'.
    16891434           remainder_ok ge s' t →
    16901435           finite_prefix ge s
    1691 | fp_tac : ∀s1,s2,s3:RTLabs_state ge.
     1436| fp_tac : ∀s1,s2,s3:RTLabs_ext_state ge.
    16921437           trace_any_call (RTLabs_status ge) s1 s2 →
    16931438           well_cost_labelled_state s2 →
     
    16981443.
    16991444
    1700 definition fp_add_default : ∀ge. ∀s,s':RTLabs_state ge.
     1445definition fp_add_default : ∀ge. ∀s,s':RTLabs_ext_state ge.
    17011446  RTLabs_classify s = cl_other →
    17021447  finite_prefix ge s' →
     
    17141459].
    17151460
    1716 definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_state ge.
     1461definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_ext_state ge.
    17171462  as_execute (RTLabs_status ge) s s1 →
    17181463  ∀CALL:RTLabs_classify s = cl_call.
     
    17451490  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
    17461491
    1747 let rec finite_segment ge (s:RTLabs_state ge) n trace
     1492let rec finite_segment ge (s:RTLabs_ext_state ge) n trace
    17481493  (ORACLE: termination_oracle)
    17491494  (TRACE_OK: remainder_ok ge s trace)
     
    17551500[ O ⇒ λLABEL_LIMIT. ⊥
    17561501| S n' ⇒
    1757   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'.
    1758     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
     1502  match s return λs:RTLabs_ext_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_ext_state s0 stk mtc0 ⇒ λtrace'.
     1503    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_ext_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_ext_state ge s ? mtc) with
    17591504    [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
    17601505    | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
    1761         let start' ≝ mk_RTLabs_state ge start stk mtc in
     1506        let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
    17621507        let next' ≝ next_state ge start' next tr EV in
    17631508        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
     
    18791624*)
    18801625
    1881 let corec make_label_diverges ge (s:RTLabs_state ge)
     1626let corec make_label_diverges ge (s:RTLabs_ext_state ge)
    18821627  (trace: flat_trace io_out io_in ge s)
    18831628  (ORACLE: termination_oracle)
     
    18901635[ ex_intro n B ⇒
    18911636    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
    1892       return λs:RTLabs_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
     1637      return λs:RTLabs_ext_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
    18931638    with
    18941639    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
     
    19161661] qed.
    19171662
    1918 lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_state ge.
     1663lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_ext_state ge.
    19191664  as_execute (RTLabs_status ge) s1 s2 →
    19201665  make_initial_state p = OK ? s1 →
     
    19471692qed.
    19481693
    1949 let rec whole_structured_trace_exists ge p (s:RTLabs_state ge)
     1694let rec whole_structured_trace_exists ge p (s:RTLabs_ext_state ge)
    19501695  (ORACLE: termination_oracle)
    19511696  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     
    19561701    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
    19571702    trace_whole_program_exists (RTLabs_status ge) s ≝
    1958 match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
     1703match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
    19591704                   make_initial_state p = OK ? s →
    19601705                   well_cost_labelled_state s →
    19611706                   soundly_labelled_state s →
    19621707                   trace_whole_program_exists (RTLabs_status ge) s with
    1963 [ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace.
     1708[ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace.
    19641709match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
    19651710                             make_initial_state p = OK state s →
    19661711                             well_cost_labelled_state s →
    19671712                             soundly_labelled_state s →
    1968                              trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with
     1713                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_ext_state ge s stk mtc) with
    19691714[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
    19701715    let IS_CALL ≝ initial_state_is_call … INITIAL in
    1971     let s' ≝ mk_RTLabs_state ge s stk mtc in
     1716    let s' ≝ mk_RTLabs_ext_state ge s stk mtc in
    19721717    let next' ≝ next_state ge s' next tr EV in
    19731718    match ORACLE ge O next trace' with
     
    20141759qed.
    20151760
    2016 definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_state (make_global p) ≝
    2017 λp,s,I. mk_RTLabs_state (make_global p) s [init_state_is p s I] ?.
     1761definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝
     1762λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?.
    20181763cases (init_state_is p s I) #b
    20191764cases s
     
    20831828
    20841829
    2085 lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
     1830lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
    20861831  as_execute (RTLabs_status ge) s s' →
    20871832  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
     
    21031848] qed.
    21041849
    2105 let rec deprop_as_execute ge (s,s':RTLabs_state ge)
     1850let rec deprop_as_execute ge (s,s':RTLabs_ext_state ge)
    21061851  (X:as_execute (RTLabs_status ge) s s')
    21071852: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
     
    21321877
    21331878(* Extract a flat trace from a structured one. *)
    2134 let rec flat_trace_of_label_return ge (s,s':RTLabs_state ge)
     1879let rec flat_trace_of_label_return ge (s,s':RTLabs_ext_state ge)
    21351880  (tr:trace_label_return (RTLabs_status ge) s s')
    21361881on tr :
     
    21431888    (flat_trace_of_label_return ge s2 s3 tlr)
    21441889]
    2145 and flat_trace_of_label_label ge ends (s,s':RTLabs_state ge)
     1890and flat_trace_of_label_label ge ends (s,s':RTLabs_ext_state ge)
    21461891  (tr:trace_label_label (RTLabs_status ge) ends s s')
    21471892on tr :
     
    21501895[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
    21511896]
    2152 and flat_trace_of_any_label ge ends (s,s':RTLabs_state ge)
     1897and flat_trace_of_any_label ge ends (s,s':RTLabs_ext_state ge)
    21531898  (tr:trace_any_label (RTLabs_status ge) ends s s')
    21541899on tr :
     
    21811926(* We take an extra step so that we can always return a non-empty trace to
    21821927   satisfy the guardedness condition in the cofixpoint. *)
    2183 let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_state ge) et
     1928let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ext_state ge) et
    21841929  (tr:trace_any_call (RTLabs_status ge) s s')
    21851930  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
    21861931on tr :
    21871932  partial_flat_trace io_out io_in ge s s'' ≝
    2188 match tr return λs,s':RTLabs_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
     1933match tr return λs,s':RTLabs_ext_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
    21891934[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
    21901935| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
     
    22021947] EX''.
    22031948
    2204 let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_state ge) et
     1949let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ext_state ge) et
    22051950  (tr:trace_label_call (RTLabs_status ge) s s')
    22061951  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
     
    22141959   to take care to satisfy the guardedness condition by witnessing the fact that
    22151960   the partial traces are non-empty. *)
    2216 let corec flat_trace_of_label_diverges ge (s:RTLabs_state ge)
     1961let corec flat_trace_of_label_diverges ge (s:RTLabs_ext_state ge)
    22171962  (tr:trace_label_diverges (RTLabs_status ge) s)
    22181963: flat_trace io_out io_in ge s ≝
    2219 match tr return λs:RTLabs_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
     1964match tr return λs:RTLabs_ext_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
    22201965[ tld_step sx sy tll tld ⇒
    2221   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 ⇒
     1966  match sy in RTLabs_ext_state return λsy:RTLabs_ext_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_ext_state sy' stk mtc0 ⇒
    22221967    λtll.
    2223     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
     1968    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_ext_state ge s2 stk mtc) → flat_trace ??? s1 with
    22241969    [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    2225     | 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)
     1970    | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)
    22261971    ] mtc0 ] tll tld
    22271972| tld_base s1 s2 s3 tlc EX CL tld ⇒
    2228   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 ⇒
     1973  match s3 in RTLabs_ext_state return λs3:RTLabs_ext_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_ext_state s3' stk mtc0 ⇒
    22291974    λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    2230       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
     1975      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_ext_state ge s3 stk mtc) → flat_trace ??? s1 with
    22311976      [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    2232       | 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)
     1977      | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)
    22331978      ] mtc0
    22341979    ]
     
    22371982(* Helper to keep adding the partial trace without violating the guardedness
    22381983   condition. *)
    2239 and add_partial_flat_trace ge (s:state) (s':RTLabs_state ge)
     1984and add_partial_flat_trace ge (s:state) (s':RTLabs_ext_state ge)
    22401985: partial_flat_trace io_out io_in ge s s' →
    22411986  trace_label_diverges (RTLabs_status ge) s' →
    22421987  flat_trace io_out io_in ge s ≝
    2243 match 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 ⇒
    2244 λ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
     1988match s' return λs':RTLabs_ext_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_ext_state sx stk mtc ⇒
     1989λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s' ? mtc) → flat_trace io_out io_in ge s with
    22451990[ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
    2246 | 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)
     1991| pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_ext_state ge s3 stk mtc) tr' tr)
    22471992] mtc ]
    22481993.
     
    22792024] qed.
    22802025
    2281 let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
     2026let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
    22822027  (str:trace_label_diverges (RTLabs_status ge) s)
    22832028  (tr:flat_trace io_out io_in ge s)
     
    22862031qed.
    22872032
    2288 let rec flat_trace_of_whole_program ge (s:RTLabs_state ge)
     2033let rec flat_trace_of_whole_program ge (s:RTLabs_ext_state ge)
    22892034  (tr:trace_whole_program (RTLabs_status ge) s)
    22902035on tr : flat_trace io_out io_in ge s ≝
    2291 match tr return λs:RTLabs_state ge.λtr. flat_trace io_out io_in ge s with
     2036match tr return λs:RTLabs_ext_state ge.λtr. flat_trace io_out io_in ge s with
    22922037[ twp_terminating s1 s2 sf CL EX tlr F ⇒
    22932038    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
     
    23002045].
    23012046
    2302 let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
     2047let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
    23032048  (str:trace_whole_program (RTLabs_status ge) s)
    23042049  (tr:flat_trace io_out io_in ge s)
     
    23232068(* Some results to invert the classification of states *)
    23242069
    2325 lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_state ge.
     2070lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ext_state ge.
    23262071  as_execute (RTLabs_status ge) s s' →
    23272072  RTLabs_classify s = cl →
     
    23342079#ge #cl #P * *
    23352080[ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
    2336   cases (lookup_present ???? (next_ok f)) normalize
     2081  cases (next_instruction f) normalize
    23372082  #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
    23382083| #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
     
    23412086] qed.
    23422087
    2343 lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_state ge.
     2088lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
    23442089  as_execute (RTLabs_status ge) s s' →
    23452090  RTLabs_classify s = cl →
     
    23552100qed.
    23562101
    2357 lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_state ge.
     2102lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
    23582103  as_execute (RTLabs_status ge) s s' →
    23592104  RTLabs_classify s = cl →
    23602105  match cl with
    2361   [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_state ge (Callstate fd args dst fs m) S M
    2362   | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_state ge (Returnstate ret dst fs m) S M
    2363   | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_state ge (State f fs m) S M
     2106  [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate fd args dst fs m) S M
     2107  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M
     2108  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M
    23642109  ] .
    23652110#ge #cl * * [ #f #fs #m | #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
     
    23672112whd in CL:(??%?);
    23682113[ cut (cl = cl_other ∨ cl = cl_jump)
    2369   [ cases (lookup_present … (next_ok … f)) in CL;
     2114  [ cases (next_instruction f) in CL;
    23702115    normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
    23712116  * #E >E %{f} %{fs} %{m} %{S} %{M} %
     
    23832128  ].
    23842129#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
    2385 cases (lookup_present … (next_ok f)) //
     2130cases (next_instruction f) //
    23862131qed.
    23872132
     
    24502195
    24512196lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
    2452   graph_fn ge (state_fn ge (mk_RTLabs_state ge (State f fs m) S M)) g →
     2197  graph_fn ge (state_fn ge (mk_RTLabs_ext_state ge (State f fs m) S M)) g →
    24532198  g = f_graph (func f).
    24542199#ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
     
    24592204
    24602205lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
    2461   let s ≝ mk_RTLabs_state ge (State f fs m) S M in
     2206  let s ≝ mk_RTLabs_ext_state ge (State f fs m) S M in
    24622207  ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
    24632208  actual_successor s' = Some ? l →
    24642209  state_fn ge s = state_fn ge (next_state ge s s' tr EV).
    24652210#ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
    2466 change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
    2467 inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_state ge (State f fs m) ? M) … EV))
     2211change with (Ras_state ? (next_state ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
     2212inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV))
    24682213[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
    24692214| #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
     
    24872232cases pre in CL AF ⊢ %;
    24882233* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
    2489     cases (lookup_present ???? (next_ok f)) in CL;
     2234    cases (next_instruction f) in CL;
    24902235    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
    24912236  | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
     
    25062251] qed.
    25072252
    2508 lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_state ge. ∀l.
     2253lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀l.
    25092254  actual_successor s = Some ? l →
    25102255  pc_label (as_pc_of (RTLabs_status ge) s) l.
     
    25882333   a trace_any_label. *)
    25892334
    2590 lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal.
     2335lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀fl,tal.
    25912336  soundly_labelled_state s1 →
    25922337  RTLabs_classify s1 = cl_other →
     
    26092354     isn't and we get a loop of successor instruction labels that breaks the
    26102355     soundness of the cost labelling. *)
    2611   cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
     2356  cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
    26122357  [ * #H @H
    26132358    cases (memb_exists … IN) #left * #right #E
    26142359    @(All_split … (tal_tail_not_costed … tal CS2) … E)
    26152360  | (* Now show that the loop invalidates soundness. *)
    2616     cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f))
     2361    cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f))
    26172362    [ %1 ] #PC1
    26182363    cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2)
     
    26752420whd in ⊢ (??%% → ?); #E destruct try %
    26762421[ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
     2422  change with (lookup_present … next2 nok1) in match (next_instruction ?);
    26772423  cases (lookup_present … next2 nok1)
    26782424  normalize //
     
    26982444#CS lapply (proj2 … (RTLabs_costed …) … CS)
    26992445whd in ⊢ (??%? → %);
    2700 [ whd in ⊢ (? → ??%?); cases (lookup_present … (next_ok f)) normalize
     2446[ whd in ⊢ (? → ??%?); cases (next_instruction f) normalize
    27012447  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct %
    27022448| *: #E destruct
  • src/RTLabs/semantics.ma

    r2475 r2499  
    4949definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
    5050
     51definition next_instruction : frame → statement ≝
     52λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f).
     53
    5154definition init_locals : list (register × typ) → register_env val ≝
    5255foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
     
    8992match st return λ_. IO ??? with
    9093[ State f fs m ⇒
    91   let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
     94  let s ≝ next_instruction f in
    9295  match s return λs. labels_present ? s → IO ??? with
    9396  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
     
    271274  whd in ⊢ (??%? → ?);
    272275  generalize in ⊢ (??(?%)? → ?);
    273   cases (lookup_present LabelTag statement (f_graph func) next next_ok)
     276  cases (next_instruction ?)
    274277  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    275278  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
     
    314317[ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
    315318  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
    316   cases (lookup_present … nok)
     319  cases (next_instruction ?)
    317320  (* Function call cases. *)
    318321  [ 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
Note: See TracChangeset for help on using the changeset viewer.