Changeset 1705


Ignore:
Timestamp:
Feb 16, 2012, 6:05:45 PM (6 years ago)
Author:
campbell
Message:

Checkpoint RTLabs labelling soundness work.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1682 r1705  
    1919| Returnstate _ _ _ _ ⇒ cl_return
    2020].
     21
     22definition is_cost_label : statement → bool ≝
     23λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
    2124
    2225definition RTLabs_cost : state → bool ≝
     
    910913qed.
    911914
     915(* Define a notion of sound labellings of RTLabs programs. *)
     916
     917let rec successors (s : statement) : list label ≝
     918match s with
     919[ St_skip l ⇒ [l]
     920| St_cost _ l ⇒ [l]
     921| St_const _ _ l ⇒ [l]
     922| St_op1 _ _ _ _ _ l ⇒ [l]
     923| St_op2 _ _ _ _ l ⇒ [l]
     924| St_load _ _ _ l ⇒ [l]
     925| St_store _ _ _ l ⇒ [l]
     926| St_call_id _ _ _ l ⇒ [l]
     927| St_call_ptr _ _ _ l ⇒ [l]
     928(*
     929| St_tailcall_id _ _ ⇒ [ ]
     930| St_tailcall_ptr _ _ ⇒ [ ]
     931*)
     932| St_cond _ l1 l2 ⇒ [l1; l2]
     933| St_jumptable _ ls ⇒ ls
     934| St_return ⇒ [ ]
     935].
     936
     937definition actual_successor : state → option label ≝
     938λs. match s with
     939[ State f fs m ⇒ Some ? (next f)
     940| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
     941| Returnstate _ _ _ _ ⇒ None ?
     942].
     943
     944lemma nth_opt_Exists : ∀A,n,l,a.
     945  nth_opt A n l = Some A a →
     946  Exists A (λa'. a' = a) l.
     947#A #n elim n
     948[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
     949| #m #IH *
     950  [ #a #E normalize in E; destruct
     951  | #a #l #a' #E %2 @IH @E
     952  ]
     953] qed.
     954
     955lemma eval_successor : ∀ge,f,fs,m,tr,s'.
     956  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
     957  RTLabs_classify s' = cl_return ∨
     958  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
     959#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
     960whd in ⊢ (??%? → ?);
     961generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
     962[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     963| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     964| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     965| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     966| #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     967| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     968| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     969| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     970| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     971| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
     972| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
     973  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
     974  whd in ⊢ (??%? → ?);
     975  generalize in ⊢ (??(?%)? → ?);
     976  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
     977  [ #e #E normalize in E; destruct
     978  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
     979  ]
     980| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
     981] qed.
     982
     983definition steps_for_statement : statement → nat ≝
     984λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
     985
     986inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
     987| stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l (S n)
     988| stlb_step : ∀l,n,H.
     989    let stmt ≝ lookup_present … g l H in
     990    (∀l'. Exists label (λl0. l0 = l') (successors stmt) → steps_to_label_bound g l' n) →
     991    steps_to_label_bound g l (steps_for_statement stmt + n).
     992   
     993discriminator nat.
     994
     995lemma steps_to_label_bound_inv_step : ∀g,l,n.
     996  steps_to_label_bound g l n →
     997  ∀H.
     998  let stmt ≝ lookup_present … g l H in
     999  ¬ (bool_to_Prop (is_cost_label stmt)) →
     1000  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
     1001    ∃n'. n = n' + steps_for_statement stmt ∧
     1002          steps_to_label_bound g l' n').
     1003#g #l0 #n0 #H1 inversion H1
     1004[ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)
     1005| #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC #l' #EX
     1006  % [2: % [ @commutative_plus | @IH // ] ]
     1007] qed.
     1008
     1009definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
     1010
     1011let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
     1012  soundly_labelled_pc (f_graph fn) (f_entry fn).
    9121013
    9131014
     
    9211022| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
    9221023].
     1024
    9231025definition frame_steps_to_label_bound : frame → nat → Prop ≝
    9241026λf. steps_to_label_bound (f_graph (func f)) (next f).
    9251027
    9261028inductive state_steps_to_label_bound : state → nat → Prop ≝
    927 | sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) (n*2)
    928 | sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S (n*2))
    929 | sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S (n*2))
     1029| sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) n
     1030| sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S n)
     1031| sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S n)
    9301032.
     1033
     1034lemma state_steps_to_label_bound_zero : ∀s.
     1035  ¬ state_steps_to_label_bound s O.
     1036#s % #H inversion H
     1037[ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
     1038  inversion H52
     1039  [ #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
     1040  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 normalize in H74; destruct
     1041  ]
     1042| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
     1043| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
     1044] qed.
     1045
     1046lemma eval_steps : ∀ge,f,fs,m,tr,s'.
     1047  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
     1048  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
     1049  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 ].
     1050#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
     1051whd in ⊢ (??%? → ?);
     1052generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
     1053[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
     1054| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
     1055| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1056| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1057| #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1058| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1059| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
     1060| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
     1061| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
     1062| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
     1063| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
     1064  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
     1065  whd in ⊢ (??%? → ?);
     1066  generalize in ⊢ (??(?%)? → ?);
     1067  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
     1068  [ #e #E normalize in E; destruct
     1069  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
     1070  ]
     1071| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
     1072] qed.
     1073
     1074lemma state_steps_to_label_bound_step : ∀ge,s,tr,s',n.
     1075  state_steps_to_label_bound s (S n) →
     1076  eval_statement ge s = Value ??? 〈tr, s'〉 →
     1077  RTLabs_cost s = false →
     1078  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
     1079   state_steps_to_label_bound s' n.
     1080#ge #s #tr #s' #n #STEPS inversion STEPS
     1081[ #f #fs #m #m #FS #E1 #E2 #_ destruct
     1082  #EVAL cases (eval_successor … EVAL)
     1083  [ /3/
     1084  | * #l * #S1 #S2 #NC %2
     1085    cases (steps_to_label_bound_inv_step … FS … l S2)
     1086    [ 2: change with (RTLabs_cost (State f fs m)) in ⊢ (?(?%)); >NC % // ]
     1087    #n'
     1088    inversion (eval_perserves … EVAL)
     1089    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct
     1090      >(eval_steps … EVAL) * >commutative_plus #En normalize in En;
     1091      whd in S1:(??%?);
     1092      #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
     1093      %1 @H
     1094    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
     1095      >(eval_steps … EVAL) * >commutative_plus #En normalize in En;
     1096      whd in S1:(??%?);
     1097      #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
     1098      %2 //
     1099    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29
     1100      destruct
     1101    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
     1102      normalize in S1; destruct
     1103    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct
     1104    ]
     1105  ]
     1106| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
     1107  /3/
     1108| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
     1109  #EVAL #NC %2 inversion (eval_perserves … EVAL)
     1110  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
     1111  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
     1112  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
     1113  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
     1114  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
     1115    %1 whd in FS ⊢ %;
     1116    inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct ]
     1117    #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE
     1118    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
     1119    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
     1120    @FS
     1121  ]
     1122] qed.
     1123 
    9311124
    9321125(*
     
    10171210  (LABEL_LIMIT: state_steps_to_label_bound s n)
    10181211  on n : finite_prefix ge s ≝
    1019 match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
    1020 [ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ?
    1021 | S n' ⇒ 
    1022     match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S (S n')) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
     1212match n return λn. state_steps_to_label_bound s n → finite_prefix ge s with
     1213[ O ⇒ λLABEL_LIMIT. ⊥
     1214| S n' ⇒
     1215    match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_steps_to_label_bound s (S n') → finite_prefix ge s with
    10231216    [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
    10241217    | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
     
    10291222                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
    10301223            | false ⇒ λCS.
    1031                 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ?? LABEL_LIMIT in
     1224                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ??? in
    10321225                fp_add_default ge ?? CL fs ? CS
    10331226            ] (refl ??)
    10341227        | cl_jump ⇒ λCL.
    10351228            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
    1036         | cl_call ⇒ λCL.
     1229        | cl_call ⇒ λCL.?(*
    10371230            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
    10381231            [ or_introl TERMINATES ⇒
     
    10481241            | or_intror NO_TERMINATION ⇒
    10491242                fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')
    1050             ]
     1243            ]*)
    10511244        | cl_return ⇒ λCL. ⊥
    10521245        ] (refl ??)
    10531246    | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
    1054     ]
    1055 ] STATE_COSTLABELLED NO_TERMINATION LABEL_LIMIT.
    1056 [
    1057 | 2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
     1247    ] STATE_COSTLABELLED NO_TERMINATION
     1248] LABEL_LIMIT.
     1249[ cases (state_steps_to_label_bound_zero s) /2/
     1250| (* TODO: how do we know that we're not at the final state? *)
    10581251| @(absurd ?? NO_TERMINATION)
    10591252     %{0} % @wr_base //
    10601253| @(well_cost_labelled_jump … EV) //
     1254| 5,6,8,9,10: /2/
     1255|
     1256| @(well_cost_labelled_state_step … EV) //
     1257| @(not_to_not … NO_TERMINATION)
     1258  * #depth * #TERM %{depth} % @wr_step /2/
     1259| cases (state_steps_to_label_bound_step … LABEL_LIMIT EV ?)
     1260
     1261@(well_cost_labelled_call … EV) //
     1262|
     1263 2,14: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
    10611264| 5,6,8: /2/
    10621265|
    1063 |
    1064 | @(well_cost_labelled_state_step … EV) //
    1065 | @(well_cost_labelled_call … EV) //
     1266|*)
    10661267| 12,13,14: /2/
    10671268| @(well_cost_labelled_state_step … EV) //
  • src/RTLabs/syntax.ma

    r1680 r1705  
    9696
    9797
    98 (* Define a notion of sound labellings of RTLabs programs. *)
    99 
    100 let rec successors (s : statement) : list label ≝
    101 match s with
    102 [ St_skip l ⇒ [l]
    103 | St_cost _ l ⇒ [l]
    104 | St_const _ _ l ⇒ [l]
    105 | St_op1 _ _ _ _ _ l ⇒ [l]
    106 | St_op2 _ _ _ _ l ⇒ [l]
    107 | St_load _ _ _ l ⇒ [l]
    108 | St_store _ _ _ l ⇒ [l]
    109 | St_call_id _ _ _ l ⇒ [l]
    110 | St_call_ptr _ _ _ l ⇒ [l]
    111 (*
    112 | St_tailcall_id _ _ ⇒ [ ]
    113 | St_tailcall_ptr _ _ ⇒ [ ]
    114 *)
    115 | St_cond _ l1 l2 ⇒ [l1; l2]
    116 | St_jumptable _ ls ⇒ ls
    117 | St_return ⇒ [ ]
    118 ].
    119 
    120 definition is_cost_label : statement → bool ≝
    121 λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
    122 
    123 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
    124 | stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l n
    125 | stlb_step : ∀l,n,H.
    126     (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' n) →
    127     steps_to_label_bound g l (S n).
    128    
    129 discriminator nat.
    130 
    131 lemma steps_to_label_bound_inv_step : ∀g,l,n.
    132   steps_to_label_bound g l n →
    133   ∀H. ¬ (bool_to_Prop (is_cost_label (lookup_present … g l H))) →
    134     (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' (pred n)).
    135 #g #l0 #n0 #H1 inversion H1
    136 [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)
    137 | #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC @IH
    138 ] qed.
    139 
    140 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
    141 
    142 let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
    143   soundly_labelled_pc (f_graph fn) (f_entry fn).
    144 
Note: See TracChangeset for help on using the changeset viewer.