Changeset 2499

Timestamp:

Nov 28, 2012, 12:52:12 PM (8 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:

• Traces.ma (modified) (65 diffs)
• abstract.ma (added)
• semantics.ma (modified) (4 diffs)

src/RTLabs/Traces.ma

@@ -1 +1 @@
 
-include "RTLabs/semantics.ma".
+include "RTLabs/abstract.ma".
 include "RTLabs/CostSpec.ma".
 include "RTLabs/CostMisc.ma".
-include "common/StructuredTraces.ma".
 include "common/Executions.ma".
-include "utilities/deqsets.ma".
 include "utilities/listb.ma".
 
-discriminator status_class.
-
-(* We augment states with a stack of function blocks (i.e. pointers) so that we
-   can make sensible "program counters" for the abstract state definition, along
-   with a proof that we will get the correct code when we do the lookup (which
-   is done to find cost labels given a pc).
-   
-   Adding them to the semantics is an alternative, more direct approach.
-   However, it makes animating the semantics extremely difficult, because it
-   is hard to avoid normalising and displaying irrelevant parts of the global
-   environment and proofs.
-   
-   We use blocks rather than identifiers because the global environments go
-
-     identifier → block → definition
-   
-   and we'd have to introduce backwards lookups to find identifiers for
-   function pointers.
- *)
-
-definition Ras_Fn_Match ≝
-λge,state,fn_stack.
-  match state with
-  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
-  | Callstate fd _ _ fs _ ⇒
-      match fn_stack with
-      [ nil ⇒ False
-      | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
-        All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
-      ]
-  | Returnstate _ _ fs _ ⇒ 
-      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
-  | Finalstate _ ⇒ fn_stack = [ ]
-  ].
-
-record RTLabs_state (ge:genv) : Type[0] ≝ {
-  Ras_state :> state;
-  Ras_fn_stack : list block;
-  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
-}.
-
-(* Given a plain step of the RTLabs semantics, give the next state along with
-   the shadow stack of function block numbers.  Carefully defined so that the
-   coercion back to the plain state always reduces. *)
-definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
-  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
-λge,s,s',t,EX. mk_RTLabs_state ge s' 
- (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)
- ?.
-cases s' in EX ⊢ %;
-[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
-  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
-    whd cases stk in mtc ⊢ %; [ * ]
-    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
-    | @M2 ]
-  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
-  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
-    whd cases stk in mtc ⊢ %; [ * ]
-    #hd #tl #H @H
-  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
-  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
-    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
-    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
-  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
-  ]
-| -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
-  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
-  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
-    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
-    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
-  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
-  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
-  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
-  ]
-| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
-  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
-  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
-  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
-    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H 
-  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
-  ]
-| #r #EX whd @refl
-] qed.
-
-
-(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
-       will be added later (LTL → LIN). *)
-
-definition RTLabs_classify : state → status_class ≝
-λs. match s with
-[ State f _ _ ⇒
-    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
-    [ St_cond _ _ _ ⇒ cl_jump
-(*    | St_jumptable _ _ ⇒ cl_jump*)
-    | _ ⇒ cl_other
-    ]
-| Callstate _ _ _ _ _ ⇒ cl_call
-| Returnstate _ _ _ _ ⇒ cl_return
-| Finalstate _ ⇒ cl_other
-].
-
-(* As with is_cost_label/cost_label_of we define a boolean function as well
-   as one which extracts the cost label so that we can use it in hypotheses
-   without naming the cost label. *)
-
-definition RTLabs_cost : state → bool ≝
-λs. match s with
-[ State f fs m ⇒
-    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
-| _ ⇒ false
-].
-
-definition RTLabs_cost_label : state → option costlabel ≝
-λs. match s with
-[ State f fs m ⇒
-    cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
-| _ ⇒ None ?
-].
-
-(* "Program counters" need to identify the current state, either as a pair of
-   the function and current instruction, or the function being entered or
-   left.  Functions are identified by their function pointer block because 
-   this avoids introducing functions to map back pointers to function ids using
-   the global environment.  (See the comment at the start of this file, too.)
-   
-   Calls also get the caller's instruction label (or None for the initial call)
-   so that we can distinguish different calls.  This is used only for the
-   t.*_unrepeating property, which includes the pc for call states.
-    *)
-
-inductive RTLabs_pc : Type[0] ≝
-| rapc_state : block → label → RTLabs_pc
-| rapc_call : option label → block → RTLabs_pc
-| rapc_ret : option block → RTLabs_pc
-| rapc_fin : RTLabs_pc
-.
-
-definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
-λx,y. match x with
-[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
-| rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒
-    eqb ? o1 o2
-    ∧ eq_block b1 b2
-  | _ ⇒ false ]
-| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ]
-| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
-].
-
-definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
-whd in match RTLabs_pc_eq;
-* [ #b1 #l1 | #bl1 #b1 | #ob1 | ]
-* [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ]
-normalize nodelta
-[ @eq_block_elim [ #E destruct | * #NE ] ]
-[ @eq_identifier_elim [ #E destruct | *: * #NE ] ]
-[ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ]
-[ @eq_block_elim [ #E destruct | * #NE ] ]
-normalize % #E destruct try (cases (NE (refl ??))) @refl
-qed.
-
-definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝
-λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒
-match s' return λs'. Ras_Fn_Match ? s' ? → ? with
-[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
-| 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 ]
-| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
-| Finalstate _ ⇒ λmtc. rapc_fin
-] mtc0 ].
-whd in mtc; cases mtc
-qed.
-
-definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
-λge,pc.
-match pc with
-[ rapc_state b l ⇒
-  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
-    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
-| _ ⇒ None ?
-].
-
-(* After returning from a function, we should be ready to execute the next
-   instruction of the caller and the shadow stack should be preserved (we have
-   to take the top element off because the Callstate includes the callee); *or*
-   we're in the final state.
- *)
-
-definition RTLabs_after_return : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → RTLabs_state ge → Prop ≝
-λge,s,s'.
-  match s with
-  [ mk_Sig s p ⇒
-    match s return λs. RTLabs_classify s = cl_call → ? with
-    [ Callstate fd args dst stk m ⇒
-      λ_. match s' with
-      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
-          next h = next f ∧
-          f_graph (func h) = f_graph (func f) ∧
-          match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]
-      | Finalstate r ⇒ stk = [ ]
-      | _ ⇒ False
-      ]
-   | State f fs m ⇒ λH.⊥
-   | _ ⇒ λH.⊥
-   ] p
- ].
-[ whd in H:(??%?);
-  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
-  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
-| normalize in H; destruct
-| normalize in H; destruct
-] qed.
-
-definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → ident ≝
-λge,s.
-  match s with
-  [ mk_Sig s p ⇒
-    match s return λs':RTLabs_state ge. RTLabs_classify s' = cl_call → ident with
-    [ mk_RTLabs_state s' stk mtc0 ⇒
-      match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
-      [ Callstate fd _ _ _ _ ⇒
-        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
-        [ nil ⇒ λmtc. ⊥
-        | cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ?
-        ]
-      | State f _ _ ⇒ λ_. λH.⊥
-      | _ ⇒ λ_. λH.⊥
-      ] mtc0
-    ] p
-  ].
-[ whd in H:(??%?);
-  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
-  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
-| 4,5: normalize in H; destruct (H)
-| cases mtc
-| cases mtc #FFP #_ >FFP % #E destruct (E)
-] qed.
-
-
-definition RTLabs_status : genv → abstract_status ≝
-λge.
-  mk_abstract_status
-    (RTLabs_state ge)
-    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
-    RTLabs_deqset
-    (RTLabs_state_to_pc ge)
-    RTLabs_classify
-    (RTLabs_pc_to_cost_label ge)
-    (RTLabs_after_return ge)
-    (λs. RTLabs_is_final s ≠ None ?)
-    (RTLabs_call_ident ge).
 
 (* Allow us to move between the different notions of when a state is cost
    labelled. *)
 
-lemma RTLabs_costed : ∀ge. ∀s:RTLabs_state ge.
+lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
   RTLabs_cost s = true ↔
   as_costed (RTLabs_status ge) s.
@@ -275 +20 @@
   cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
   whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
-  >(lookup_lookup_present … nok)
-  whd in ⊢ (?(??%?)(?(??%?)));
+  whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
+  >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
   % cases (lookup_present ?? (f_graph func) ??) normalize
   #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
@@ -299 +44 @@
 ] qed.
 
-lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_state ge.
+lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
   RTLabs_cost s = false →
   ¬ as_costed (RTLabs_status ge) s.
@@ -718 +463 @@
   RTLabs_classify s = cl_jump →
   ∃f,fs,m. s = State f fs m ∧ 
-  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
-  (∃r,l1,l2. stmt = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
+  (∃r,l1,l2. next_instruction f = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
 *
 [ #f #fs #m #E
   %{f} %{fs} %{m} %
   [ @refl
-  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
+  | whd in E:(??%?); cases (next_instruction f) in E ⊢ %;
     try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
     (*[ %1*) %{A} %{B} %{C} @refl
@@ -751 +495 @@
   lapply (Hbody (next fr) (next_ok fr))
   generalize in ⊢ (?(???%) → ?);
+  change with (next_instruction fr) in match (lookup_present ?????);
   >Estmt #LP' #WS
   cases (andb_Prop_true … WS) #H1 #H2 [ @H1 | @H2 ]
@@ -777 +522 @@
   ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
 * [ #f #fs #m whd in ⊢ (??%? → ?);
-    cases (lookup_present … (next f) (next_ok f)) normalize
+    cases (next_instruction f) normalize
     try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
   | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
@@ -808 +553 @@
 (* Extend our information about steps to states extended with the shadow stack. *)
 
-inductive state_rel_ext : ∀ge:genv. RTLabs_state ge → RTLabs_state ge → Prop ≝
-| 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')
-| 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')
-| 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')
-| 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')
-| 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')
-| 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')
+inductive state_rel_ext : ∀ge:genv. RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
+| 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')
+| 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')
+| 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')
+| 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')
+| 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')
+| 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')
 .
 
@@ -858 +603 @@
  *)
 
-inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_state ge → Prop ≝
-| 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)
-| 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)
-| 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)
+inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ext_state ge → Prop ≝
+| 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)
+| 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)
+| 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)
 .
 
-inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_state ge → RTLabs_state ge → Prop ≝
+inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
 | sp_normal : ∀fs,S,s1,s2.
     stack_of_state ge fs S s1 →
@@ -873 +618 @@
     frame_rel f f' →
     stack_of_state ge (f::fs) (fn::S) s1 →
-    stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (State f' fs m) (fn::S) M)
+    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (State f' fs m) (fn::S) M)
 | sp_stop : ∀s1,r,M.
     stack_of_state ge [ ] [ ] s1 →
-    stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (Finalstate r) [ ] M)
+    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (Finalstate r) [ ] M)
 | sp_top : ∀fd,args,dst,m,r,fn,M1,M2.
-    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)
+    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)
 .
 
@@ -897 +642 @@
 
 lemma stack_preserved_final : ∀ge,e,r,S,M,s.
-  ¬stack_preserved ge e (mk_RTLabs_state ge (Finalstate r) S M) s.
+  ¬stack_preserved ge e (mk_RTLabs_ext_state ge (Finalstate r) S M) s.
 #ge #e #r #S #M #s % #H inversion H
 [ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
@@ -938 +683 @@
    returning. *)
 
-lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_state ge.∀cl.
+lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_ext_state ge.∀cl.
   RTLabs_classify s1 = cl →
   as_execute (RTLabs_status ge) s1 s2 →
@@ -949 +694 @@
 #ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX)
 [ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
-  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
+  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
 | #ge #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
-  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
+  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
 | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
   * #s3 #S3 #M3 #SP inversion SP
@@ -969 +714 @@
   ] 
 | #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct
-  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) /2/
+  whd in match (RTLabs_classify ?); cases (next_instruction f) /2/
 | #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd
   cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) //
@@ -975 +720 @@
 ] qed.
 
-lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_state ge.∀s2,tr.
+lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_ext_state ge.∀s2,tr.
   ∀EV:eval_statement ge s1 = Value … 〈tr,s2〉.
   as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV).
@@ -981 +726 @@
 qed.
 
-lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.
+lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
   ∀CL : RTLabs_classify s1 = cl_call.
   as_execute (RTLabs_status ge) s1 s2 →
@@ -1019 +764 @@
    of the termination proof is respected. *)
 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
-  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
+  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
   (original_terminates: will_return ge depth start full)
-  (T:RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
+  (T:RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
 {
-  new_state : RTLabs_state ge;
+  new_state : RTLabs_ext_state ge;
   remainder : flat_trace io_out io_in ge new_state;
   cost_labelled : well_cost_labelled_state new_state;
@@ -1039 +784 @@
    encountering a label. *)
 record sub_trace_result (ge:genv) (depth:nat)
-  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
+  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
   (original_terminates: will_return ge depth start full)
-  (T:trace_ends_with_ret → RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
+  (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
 {
   ends : trace_ends_with_ret;
@@ -1051 +796 @@
    the size of the termination proof might need to be relaxed, too. *)
 
-definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
+definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
   ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
     will_return_end … TM1 = will_return_end … TM2 →
@@ -1080 +825 @@
 ] qed.
 
-definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
+definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
   ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
     will_return_end … TM1 = will_return_end … TM2 →
@@ -1094 +839 @@
 definition myge : nat → nat → Prop ≝ ge.
 
-let rec make_label_return ge depth (s:RTLabs_state ge)
+let rec make_label_return ge depth (s:RTLabs_ext_state ge)
   (trace: flat_trace io_out io_in ge s)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
@@ -1135 +880 @@
 
 
-and make_label_label ge depth (s:RTLabs_state ge)
+and make_label_label ge depth (s:RTLabs_ext_state ge)
   (trace: flat_trace io_out io_in ge s)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
@@ -1158 +903 @@
 
 
-and make_any_label ge depth (s0:RTLabs_state ge)
+and make_any_label ge depth (s0:RTLabs_ext_state ge)
   (trace: flat_trace io_out io_in ge s0)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
@@ -1172 +917 @@
 [ O ⇒ λTERMINATES_IN_TIME. ⊥
 | S TIME ⇒ λTERMINATES_IN_TIME.
-  match s0 return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
+  match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
                                       well_cost_labelled_state s →
                                       ∀TM:will_return ??? trace.
                                       myge ? (times 3 (will_return_length ??? trace TM)) →
                                       sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
-  with [ mk_RTLabs_state s stk mtc0 ⇒ λtrace.
+  with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace.
   match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
                                well_cost_labelled_state s →
                                ∀TM:will_return ??? trace.
                                myge ? (times 3 (will_return_length ??? trace TM)) →
-                               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
+                               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
   [ ft_stop st FINAL ⇒
       λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
 
   | ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
-    let start' ≝ mk_RTLabs_state ge start stk mtc in
+    let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
     let next' ≝ next_state ? start' ?? EV in
     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
@@ -1342 +1087 @@
 (* We can initialise TIME with a suitably large value based on the length of the
    termination proof. *)
-let rec make_label_return' ge depth (s:RTLabs_state ge)
+let rec make_label_return' ge depth (s:RTLabs_ext_state ge)
   (trace: flat_trace io_out io_in ge s)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
@@ -1386 +1131 @@
 lemma eval_successor : ∀ge,f,fs,m,tr,s'.
   eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
-  (RTLabs_classify s' = cl_return ∧ successors (lookup_present … (f_graph (func f)) (next f) (next_ok f)) = [ ]) ∨
-  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
+  (RTLabs_classify s' = cl_return ∧ successors (next_instruction f) = [ ]) ∨
+  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (next_instruction f)).
 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
 whd in ⊢ (??%? → ?);
-generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
+generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?)
 [ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
 | #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
@@ -1491 +1236 @@
 lemma eval_steps : ∀ge,f,fs,m,tr,s'.
   eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
-  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
+  steps_for_statement (next_instruction f) =
   match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
 whd in ⊢ (??%? → ?);
-generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
+generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?)
 [ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
 | #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
@@ -1517 +1262 @@
 ] qed.
 
-lemma bound_after_call : ∀ge.∀s,s':RTLabs_state ge.∀n.
+lemma bound_after_call : ∀ge.∀s,s':RTLabs_ext_state ge.∀n.
   state_bound_on_steps_to_cost s (S n) →
   ∀CL:RTLabs_classify s = cl_call.
@@ -1676 +1421 @@
    use the fact that the trace is soundly labelled to achieve this. *)
 
-record remainder_ok (ge:genv) (s:RTLabs_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
+record remainder_ok (ge:genv) (s:RTLabs_ext_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
   ro_well_cost_labelled: well_cost_labelled_state s;
   ro_soundly_labelled: soundly_labelled_state s;
@@ -1683 +1428 @@
 }.
 
-inductive finite_prefix (ge:genv) : RTLabs_state ge → Prop ≝
-| fp_tal : ∀s,s':RTLabs_state ge.
+inductive finite_prefix (ge:genv) : RTLabs_ext_state ge → Prop ≝
+| fp_tal : ∀s,s':RTLabs_ext_state ge.
            trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
            ∀t:flat_trace io_out io_in ge s'.
            remainder_ok ge s' t →
            finite_prefix ge s
-| fp_tac : ∀s1,s2,s3:RTLabs_state ge.
+| fp_tac : ∀s1,s2,s3:RTLabs_ext_state ge.
            trace_any_call (RTLabs_status ge) s1 s2 →
            well_cost_labelled_state s2 →
@@ -1698 +1443 @@
 .
 
-definition fp_add_default : ∀ge. ∀s,s':RTLabs_state ge.
+definition fp_add_default : ∀ge. ∀s,s':RTLabs_ext_state ge.
   RTLabs_classify s = cl_other →
   finite_prefix ge s' →
@@ -1714 +1459 @@
 ].
 
-definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_state ge.
+definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_ext_state ge.
   as_execute (RTLabs_status ge) s s1 →
   ∀CALL:RTLabs_classify s = cl_call.
@@ -1745 +1490 @@
   inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
 
-let rec finite_segment ge (s:RTLabs_state ge) n trace
+let rec finite_segment ge (s:RTLabs_ext_state ge) n trace
   (ORACLE: termination_oracle)
   (TRACE_OK: remainder_ok ge s trace)
@@ -1755 +1500 @@
 [ O ⇒ λLABEL_LIMIT. ⊥
 | S n' ⇒ 
-  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'.
-    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
+  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'.
+    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
     [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
     | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
-        let start' ≝ mk_RTLabs_state ge start stk mtc in
+        let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
         let next' ≝ next_state ge start' next tr EV in
         match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
@@ -1879 +1624 @@
 *)
 
-let corec make_label_diverges ge (s:RTLabs_state ge)
+let corec make_label_diverges ge (s:RTLabs_ext_state ge)
   (trace: flat_trace io_out io_in ge s)
   (ORACLE: termination_oracle)
@@ -1890 +1635 @@
 [ ex_intro n B ⇒
     match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
-      return λs:RTLabs_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
+      return λs:RTLabs_ext_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
     with
     [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
@@ -1916 +1661 @@
 ] qed.
 
-lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_state ge.
+lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_ext_state ge.
   as_execute (RTLabs_status ge) s1 s2 →
   make_initial_state p = OK ? s1 →
@@ -1947 +1692 @@
 qed.
 
-let rec whole_structured_trace_exists ge p (s:RTLabs_state ge)
+let rec whole_structured_trace_exists ge p (s:RTLabs_ext_state ge)
   (ORACLE: termination_oracle)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
@@ -1956 +1701 @@
     ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
     trace_whole_program_exists (RTLabs_status ge) s ≝ 
-match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
+match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
                    make_initial_state p = OK ? s →
                    well_cost_labelled_state s →
                    soundly_labelled_state s →
                    trace_whole_program_exists (RTLabs_status ge) s with
-[ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace. 
+[ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace. 
 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
                              make_initial_state p = OK state s →
                              well_cost_labelled_state s →
                              soundly_labelled_state s →
-                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with
+                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_ext_state ge s stk mtc) with
 [ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
     let IS_CALL ≝ initial_state_is_call … INITIAL in
-    let s' ≝ mk_RTLabs_state ge s stk mtc in
+    let s' ≝ mk_RTLabs_ext_state ge s stk mtc in
     let next' ≝ next_state ge s' next tr EV in
     match ORACLE ge O next trace' with
@@ -2014 +1759 @@
 qed.
 
-definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_state (make_global p) ≝
-λp,s,I. mk_RTLabs_state (make_global p) s [init_state_is p s I] ?.
+definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝
+λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?.
 cases (init_state_is p s I) #b
 cases s
@@ -2083 +1828 @@
 
 
-lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
+lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
   as_execute (RTLabs_status ge) s s' →
   ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
@@ -2103 +1848 @@
 ] qed.
 
-let rec deprop_as_execute ge (s,s':RTLabs_state ge)
+let rec deprop_as_execute ge (s,s':RTLabs_ext_state ge)
   (X:as_execute (RTLabs_status ge) s s')
 : Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
@@ -2132 +1877 @@
 
 (* Extract a flat trace from a structured one. *)
-let rec flat_trace_of_label_return ge (s,s':RTLabs_state ge)
+let rec flat_trace_of_label_return ge (s,s':RTLabs_ext_state ge)
   (tr:trace_label_return (RTLabs_status ge) s s')
 on tr :
@@ -2143 +1888 @@
     (flat_trace_of_label_return ge s2 s3 tlr)
 ]
-and flat_trace_of_label_label ge ends (s,s':RTLabs_state ge)
+and flat_trace_of_label_label ge ends (s,s':RTLabs_ext_state ge)
   (tr:trace_label_label (RTLabs_status ge) ends s s')
 on tr :
@@ -2150 +1895 @@
 [ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
 ]
-and flat_trace_of_any_label ge ends (s,s':RTLabs_state ge)
+and flat_trace_of_any_label ge ends (s,s':RTLabs_ext_state ge)
   (tr:trace_any_label (RTLabs_status ge) ends s s')
 on tr :
@@ -2181 +1926 @@
 (* We take an extra step so that we can always return a non-empty trace to
    satisfy the guardedness condition in the cofixpoint. *)
-let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_state ge) et
+let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ext_state ge) et
   (tr:trace_any_call (RTLabs_status ge) s s')
   (EX'':eval_statement ge s' = Value … 〈et,s''〉)
 on tr :
   partial_flat_trace io_out io_in ge s s'' ≝ 
-match tr return λs,s':RTLabs_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
+match tr return λs,s':RTLabs_ext_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
 [ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
 | tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
@@ -2202 +1947 @@
 ] EX''.
 
-let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_state ge) et
+let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ext_state ge) et
   (tr:trace_label_call (RTLabs_status ge) s s')
   (EX'':eval_statement ge s' = Value … 〈et,s''〉)
@@ -2214 +1959 @@
    to take care to satisfy the guardedness condition by witnessing the fact that
    the partial traces are non-empty. *)
-let corec flat_trace_of_label_diverges ge (s:RTLabs_state ge)
+let corec flat_trace_of_label_diverges ge (s:RTLabs_ext_state ge)
   (tr:trace_label_diverges (RTLabs_status ge) s)
 : flat_trace io_out io_in ge s ≝
-match tr return λs:RTLabs_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
+match tr return λs:RTLabs_ext_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
 [ tld_step sx sy tll tld ⇒ 
-  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 ⇒
+  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 ⇒
     λtll.
-    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
+    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
     [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
-    | 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)
+    | 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)
     ] mtc0 ] tll tld
 | tld_base s1 s2 s3 tlc EX CL tld ⇒ 
-  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 ⇒
+  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 ⇒
     λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
-      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
+      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
       [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
-      | 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)
+      | 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)
       ] mtc0
     ]
@@ -2237 +1982 @@
 (* Helper to keep adding the partial trace without violating the guardedness
    condition. *)
-and add_partial_flat_trace ge (s:state) (s':RTLabs_state ge)
+and add_partial_flat_trace ge (s:state) (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 ≝
-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 ⇒ 
-λ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
+match 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 ⇒ 
+λ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
 [ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
-| 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)
+| 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)
 ] mtc ]
 . 
@@ -2279 +2024 @@
 ] qed.
 
-let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
+let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
   (str:trace_label_diverges (RTLabs_status ge) s)
   (tr:flat_trace io_out io_in ge s)
@@ -2286 +2031 @@
 qed. 
 
-let rec flat_trace_of_whole_program ge (s:RTLabs_state ge)
+let rec flat_trace_of_whole_program ge (s:RTLabs_ext_state ge)
   (tr:trace_whole_program (RTLabs_status ge) s)
 on tr : flat_trace io_out io_in ge s ≝
-match tr return λs:RTLabs_state ge.λtr. flat_trace io_out io_in ge s with
+match tr return λs:RTLabs_ext_state ge.λtr. flat_trace io_out io_in ge s with
 [ twp_terminating s1 s2 sf CL EX tlr F ⇒
     match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
@@ -2300 +2045 @@
 ].
 
-let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
+let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
   (str:trace_whole_program (RTLabs_status ge) s)
   (tr:flat_trace io_out io_in ge s)
@@ -2323 +2068 @@
 (* Some results to invert the classification of states *)
 
-lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_state ge.
+lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ext_state ge.
   as_execute (RTLabs_status ge) s s' →
   RTLabs_classify s = cl →
@@ -2334 +2079 @@
 #ge #cl #P * *
 [ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
-  cases (lookup_present ???? (next_ok f)) normalize
+  cases (next_instruction f) normalize
   #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
 | #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
@@ -2341 +2086 @@
 ] qed.
 
-lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_state ge.
+lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
   as_execute (RTLabs_status ge) s s' →
   RTLabs_classify s = cl →
@@ -2355 +2100 @@
 qed.
 
-lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_state ge.
+lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
   as_execute (RTLabs_status ge) s s' →
   RTLabs_classify s = cl →
   match cl with
-  [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_state ge (Callstate fd args dst fs m) S M
-  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_state ge (Returnstate ret dst fs m) S M
-  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_state ge (State f fs m) S M
+  [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate fd args dst fs m) S M
+  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M
+  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M
   ] .
 #ge #cl * * [ #f #fs #m | #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
@@ -2367 +2112 @@
 whd in CL:(??%?);
 [ cut (cl = cl_other ∨ cl = cl_jump)
-  [ cases (lookup_present … (next_ok … f)) in CL; 
+  [ cases (next_instruction f) in CL; 
     normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
   * #E >E %{f} %{fs} %{m} %{S} %{M} %
@@ -2383 +2128 @@
   ].
 #f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
-cases (lookup_present … (next_ok f)) //
+cases (next_instruction f) //
 qed.
 
@@ -2450 +2195 @@
 
 lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
-  graph_fn ge (state_fn ge (mk_RTLabs_state ge (State f fs m) S M)) g →
+  graph_fn ge (state_fn ge (mk_RTLabs_ext_state ge (State f fs m) S M)) g →
   g = f_graph (func f).
 #ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
@@ -2459 +2204 @@
 
 lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
-  let s ≝ mk_RTLabs_state ge (State f fs m) S M in
+  let s ≝ mk_RTLabs_ext_state ge (State f fs m) S M in
   ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
   actual_successor s' = Some ? l →
   state_fn ge s = state_fn ge (next_state ge s s' tr EV).
 #ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
-change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
-inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_state ge (State f fs m) ? M) … EV))
+change with (Ras_state ? (next_state ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
+inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV))
 [ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
 | #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
@@ -2487 +2232 @@
 cases pre in CL AF ⊢ %;
 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
-    cases (lookup_present ???? (next_ok f)) in CL;
+    cases (next_instruction f) in CL;
     normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
   | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
@@ -2506 +2251 @@
 ] qed.
 
-lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_state ge. ∀l.
+lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀l.
   actual_successor s = Some ? l →
   pc_label (as_pc_of (RTLabs_status ge) s) l.
@@ -2588 +2333 @@
    a trace_any_label. *)
 
-lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal.
+lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀fl,tal.
   soundly_labelled_state s1 →
   RTLabs_classify s1 = cl_other →
@@ -2609 +2354 @@
      isn't and we get a loop of successor instruction labels that breaks the
      soundness of the cost labelling. *)
-  cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
+  cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
   [ * #H @H
     cases (memb_exists … IN) #left * #right #E
     @(All_split … (tal_tail_not_costed … tal CS2) … E)
   | (* Now show that the loop invalidates soundness. *)
-    cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f))
+    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))
     [ %1 ] #PC1
     cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2)
@@ -2675 +2420 @@
 whd in ⊢ (??%% → ?); #E destruct try %
 [ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
+  change with (lookup_present … next2 nok1) in match (next_instruction ?);
   cases (lookup_present … next2 nok1)
   normalize //
@@ -2698 +2444 @@
 #CS lapply (proj2 … (RTLabs_costed …) … CS)
 whd in ⊢ (??%? → %);
-[ whd in ⊢ (? → ??%?); cases (lookup_present … (next_ok f)) normalize
+[ whd in ⊢ (? → ??%?); cases (next_instruction f) normalize
   #A try #B try #C try #D try #E try #F try #G try #H try #I destruct %
 | *: #E destruct

src/RTLabs/semantics.ma

@@ -49 +49 @@
 definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
 
+definition next_instruction : frame → statement ≝
+λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f).
+
 definition init_locals : list (register × typ) → register_env val ≝
 foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
@@ -89 +92 @@
 match st return λ_. IO ??? with
 [ State f fs m ⇒
-  let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in 
+  let s ≝ next_instruction f in 
   match s return λs. labels_present ? s → IO ??? with
   [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
@@ -271 +274 @@
   whd in ⊢ (??%? → ?);
   generalize in ⊢ (??(?%)? → ?);
-  cases (lookup_present LabelTag statement (f_graph func) next next_ok)
+  cases (next_instruction ?)
   [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
   | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
@@ -314 +317 @@
 [ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
   whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
-  cases (lookup_present … nok)
+  cases (next_instruction ?)
   (* Function call cases. *)
   [ 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