source: src/RTLabs/Traces.ma @ 1583

include "RTLabs/semantics.ma".
include "common/StructuredTraces.ma".

discriminator status_class.

(* 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
].

definition RTLabs_cost : state → bool ≝
λs. match s with
[ State f fs m ⇒
    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
    [ St_cost c l ⇒ true
    | _ ⇒ false
    ]
| _ ⇒ false
].

definition RTLabs_status : genv → abstract_status ≝
λge.
  mk_abstract_status
    state
    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
    (λs,c. RTLabs_classify s = c)
    (λs. RTLabs_cost s = true)
    (λs,s'. match s with
      [ dp 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 ]
          | _ ⇒ False
          ]
        | State f fs m ⇒ λH.⊥
        | _ ⇒ λH.⊥
        ] p
      ]).
[ normalize in H; destruct
| 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 destruct
] qed.

(* Before attempting to construct a structured trace, let's show that we can
   form flat traces with evidence that they were constructed from an execution.
   
   For now we don't consider I/O. *)


coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).

(* add I/O? *)
coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.

let corec make_flat_trace ge s
  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
  flat_trace io_out io_in ge s ≝
let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
match e return λx. e = x → ? with
[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
| e_wrong m ⇒ λE. ft_wrong … s m ?
| e_interact o f ⇒ λE. ⊥
] (refl ? e).
[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
    >(?:is_final ????? = RTLabs_is_final s1) //
    lapply (refl ? (RTLabs_is_final s1))
    cases (RTLabs_is_final s1) in ⊢ (???% → %);
    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
    ]
  | *: #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E destruct @refl
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E
      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
      destruct
      inversion H
      [ #a #b #c #E1 destruct
      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
      | #m #E1 destruct
      ]
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E;
  cases (eval_statement ge s)
  [ #O #K whd in ⊢ (??%? → ?); #E destruct
  | * #tr1 #s1 whd in ⊢ (??%? → ?);
    cases (is_final ?????)
    [ whd in ⊢ (??%? → ?); #E destruct
    | #i whd in ⊢ (??%? → ?); #E destruct
    ]
  | #m whd in ⊢ (??%? → ?); #E destruct @refl
  ]
| whd in E:(??%?); >E in H; #H
  inversion H
  [ #a #b #c #E destruct
  | #a #b #c #d #E1 destruct
  | #m #E1 destruct
  ]
] qed.

let corec make_whole_flat_trace p s
  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
  (I:make_initial_state ??? p = OK ? s) :
  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
let ge ≝ make_global … p in
let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
match e return λx. e = x → ? with
[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
| e_wrong m ⇒ λE. ⊥
| e_interact o f ⇒ λE. ⊥
] (refl ? e).
[ whd in E:(??%?); >exec_inf_aux_unfold in E; 
  whd in ⊢ (??%? → ?);
  >(?:is_final ????? = RTLabs_is_final s) //
  lapply (refl ? (RTLabs_is_final s))
  cases (RTLabs_is_final s) in ⊢ (???% → %);
  [ #_ whd in ⊢ (??%? → ?); #E destruct
  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
  ]
| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
    [ #a #b #c #E1 destruct
    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
      @H1
    | #m #E1 destruct
    ]
  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
  ]
| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
] qed.

(* Need a way to choose whether a called function terminates.  Then,
     if the initial function terminates we generate a purely inductive structured trace,
     otherwise we start generating the coinductive one, and on every function call
       use the choice method again to decide whether to step over or keep going.

Not quite what we need - have to decide on seeing each label whether we will see
another or hit a non-terminating call?

Also - need the notion of well-labelled in order to break loops.



outline:

 does function terminate?
 - yes, get (bound on the number of steps until return), generate finite
        structure using bound as termination witness
 - no,  get (¬ bound on steps to return), start building infinite trace out of
        finite steps.  At calls, check for termination, generate appr. form.

generating the finite parts:

We start with the status after the call has been executed; well-labelling tells
us that this is a labelled state.  Now we want to generate a trace_label_return
and also return the remainder of the flat trace.

*)

(* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from
   [s] we reach the return state for the current function.  [depth] performs
   the call/return counting necessary for handling deeper function calls.
   It should be zero at the top level. *)
inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
| nir_step : ∀n,s,tr,s',depth,EX,trace.
    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
    nth_is_return ge n depth s' trace →
    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
| nir_call : ∀n,s,tr,s',depth,EX,trace.
    RTLabs_classify s = cl_call →
    nth_is_return ge n (S depth) s' trace →
    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
| nir_ret : ∀n,s,tr,s',depth,EX,trace.
    RTLabs_classify s = cl_return →
    nth_is_return ge n depth s' trace →
    nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace)
    (* Note that we require the ability to make a step after the return (this
       corresponds to somewhere that will be guaranteed to be a label at the
       end of the compilation chain). *)
| nir_base : ∀s,tr,s',EX,trace.
    RTLabs_classify s = cl_return →
    nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace)
.

discriminator nat.

(* Find time until a nested call completes. *)
lemma nth_is_return_down : ∀ge,n,depth,s,trace.
  nth_is_return ge n (S depth) s trace →
  ∃m. nth_is_return ge m depth s trace.
#ge #n elim n
(* It's impossible to run out of time... *)
[ #depth #s #trace #H inversion H
  [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
  | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
  | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
  ]
| #n' #IH #depth #s #trace #H inversion H
  [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    cases (IH depth s1' trace1 ?)
    [ #m' #H' %{(S m')} %1 //
    | //
    ]
  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    cases (IH (S depth) s1' trace1 ?)
    [ #m' #H' %{(S m')} %2 //
    | //
    ]
  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    cases (depth1) in H2 ⊢ %;
    [ #H2 %{O} %4 //
    | #depth' #H2 cases (IH depth' s1' trace1 ?)
      [ #m' #H' %{(S m')} %3 //
      | //
      ]
    ]
  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
  ]
] qed.

lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
  RTLabs_classify s = cl_call →
  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
  ∃m. nth_is_return ge m O s' trace.
#ge #n #s #tr #s' #EX #trace #CLASS #H 
inversion H
[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
  -H2 destruct >H1 in CLASS; #E destruct
| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
  @nth_is_return_down //
| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
  -H2 destruct
| #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
] qed.

lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace.
  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
  nth_is_return ge (pred n) O s' trace.
#ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM
[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct
| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
| #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct
| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct //
| #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct
| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
| #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
] qed.

(* We require that labels appear after branch instructions and at the start of
   functions.  The first is required for preciseness, the latter for soundness.
   We will make a separate requirement for there to be a finite number of steps
   between labels to catch loops for soundness (is this sufficient?). *)

definition is_cost_label : statement → Prop ≝
λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ].

let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝
match l return λl.All A P l → Prop with
[ nil ⇒ λ_. True
| cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)
] H. 

definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
λf,s. match s return λs. labels_present ? s → Prop with
[ St_cond _ l1 l2 ⇒ λH.
    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
    is_cost_label (lookup_present … (f_graph f) l2 ?)
| St_jumptable _ ls ⇒ λH.
    All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H
| _ ⇒ λ_. True
]. whd in H;
[ @(proj1 … H)
| @(proj2 … H)
] qed.

definition well_cost_labelled_fn : internal_function → Prop ≝
λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s.
          well_cost_labelled_statement f s (f_closed f …)) ∧
    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
[ 2: @H | skip | cases (f_entry f) // ] qed.

(* We need to ensure that any code we come across is well-cost-labelled.  We may
   get function code from either the global environment or the state. *)

definition well_cost_labelled_ge : genv → Prop ≝
λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.

definition well_cost_labelled_state : state → Prop ≝
λs. match s with
[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
                          All ? (λf. well_cost_labelled_fn (func f)) fs
| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
].

lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
  eval_statement ge s = Value ??? 〈tr,s'〉 →
  well_cost_labelled_ge ge →
  well_cost_labelled_state s →
  well_cost_labelled_state s'.
#ge #s #tr' #s' #EV cases (eval_perserves … EV)
[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
| #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
] qed.

(* Don't need to know that labels break loops because we have termination. *)

record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
  new_state : state;
  termination_count : nat;
  remainder : flat_trace io_out io_in ge new_state;
  terminates : nth_is_return ge termination_count O new_state remainder;
  cost_labelled : well_cost_labelled_state new_state;
  new_trace : T new_state
}.

definition replace_new_trace : ∀ge,T1,T2.
  ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝
λge,T1,T2,r,trace.
  mk_make_result ge T2
    (new_state … r)
    (termination_count … r)
    (remainder … r)
    (terminates … r)
    (cost_labelled … r)
    trace.

let rec make_label_return n ge s
  (trace: flat_trace io_out io_in ge s)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
  (TERMINATES: nth_is_return ge n O s trace)
  : make_result ge (trace_label_return (RTLabs_status ge) s) ≝

  let r ≝ make_label_label n ge s trace ???? in
  match new_trace … r with
  [ dp ends tll ⇒
    match ends return λx. trace_label_label ? x ?? → ? with
    [ ends_with_ret ⇒ λtll.
        replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
    | doesnt_end_with_ret ⇒ λtll.
        let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
                   (remainder … r) ??? (terminates … r) in
          replace_new_trace … r'
            (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
    ] tll
  ]

and make_label_label n ge s
  (trace: flat_trace io_out io_in ge s)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
  (TERMINATES: nth_is_return ge n O s trace)
  : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
let r ≝ make_any_label n ge s trace ??? in
match new_trace … r with
[ dp ends tr ⇒
  replace_new_trace ??? r
    (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL))
]

and make_any_label n ge s
  (trace: flat_trace io_out io_in ge s)
  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
  (TERMINATES: nth_is_return ge n O s trace)
  : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝
match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with
[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
    match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
    [ cl_other ⇒ λCL.
        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
        [ true ⇒ λCS.
            mk_make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???))
        | false ⇒ λCS.
            let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in
            match new_trace … r with
            [ dp ends trc ⇒
                replace_new_trace ??? r
                  (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??))
            ]
        ] (refl ??)
    | cl_jump ⇒ λCL. ?
    | cl_call ⇒ λCL. ?
    | cl_return ⇒ λCL. ?
    ] (refl ? (RTLabs_classify start))
| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
] STATE_COSTLABELLED TERMINATES.

[ //
| //
| @(trace_label_label_label … tll)
| //
| //
| //
| //
| //
| //
| //
|
|
|
|
| @(nth_is_return_notfn … TERMINATES) %1 @CL
| @(well_cost_labelled_state_step  … EV) //
| %{tr} @EV
|
| @CS
| %{tr} @EV
| @CL
| % whd in ⊢ (% → ?); >CS #E destruct
| @(well_cost_labelled_state_step … EV) //
| @(nth_is_return_notfn … TERMINATES) %1 @CL
| inversion TERMINATES
  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct
  ]
|


  
(* FIXME: there's trouble at the end of the program because we can't make a step
   away from the final return. *)