Skip to main content

🍬 Script_interpreter_logging.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Local_gas_counter.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Module kinstr_rewritek.
  Record record : Set := Build {
    apply :
      Script_typed_ir.stack_ty Script_typed_ir.kinstr
      Script_typed_ir.kinstr;
  }.
  Definition with_apply apply (r : record) :=
    Build apply.
End kinstr_rewritek.
Definition kinstr_rewritek := kinstr_rewritek.record.

Module failed_kinstr_cast.
  Record record : Set := Build {
    cast : Script_typed_ir.kinstr;
  }.
  Definition with_cast cast (r : record) :=
    Build cast.
End failed_kinstr_cast.
Definition failed_kinstr_cast := failed_kinstr_cast.record.

Records for the constructor parameters
Module ConstructorRecords_ex_split_kinstr.
  Module ex_split_kinstr.
    Module Ex_split_kinstr.
      Record record {cont_init_stack continuation reconstruct : Set} : Set := Build {
        cont_init_stack : cont_init_stack;
        continuation : continuation;
        reconstruct : reconstruct;
      }.
      Arguments record : clear implicits.
      Definition with_cont_init_stack
        {t_cont_init_stack t_continuation t_reconstruct} cont_init_stack
        (r : record t_cont_init_stack t_continuation t_reconstruct) :=
        Build t_cont_init_stack t_continuation t_reconstruct cont_init_stack
          r.(continuation) r.(reconstruct).
      Definition with_continuation
        {t_cont_init_stack t_continuation t_reconstruct} continuation
        (r : record t_cont_init_stack t_continuation t_reconstruct) :=
        Build t_cont_init_stack t_continuation t_reconstruct r.(cont_init_stack)
          continuation r.(reconstruct).
      Definition with_reconstruct
        {t_cont_init_stack t_continuation t_reconstruct} reconstruct
        (r : record t_cont_init_stack t_continuation t_reconstruct) :=
        Build t_cont_init_stack t_continuation t_reconstruct r.(cont_init_stack)
          r.(continuation) reconstruct.
    End Ex_split_kinstr.
    Definition Ex_split_kinstr_skeleton := Ex_split_kinstr.record.

    Module Ex_split_log.
      Record record {stack continuation reconstruct : Set} : Set := Build {
        stack : stack;
        continuation : continuation;
        reconstruct : reconstruct;
      }.
      Arguments record : clear implicits.
      Definition with_stack {t_stack t_continuation t_reconstruct} stack
        (r : record t_stack t_continuation t_reconstruct) :=
        Build t_stack t_continuation t_reconstruct stack r.(continuation)
          r.(reconstruct).
      Definition with_continuation {t_stack t_continuation t_reconstruct}
        continuation (r : record t_stack t_continuation t_reconstruct) :=
        Build t_stack t_continuation t_reconstruct r.(stack) continuation
          r.(reconstruct).
      Definition with_reconstruct {t_stack t_continuation t_reconstruct}
        reconstruct (r : record t_stack t_continuation t_reconstruct) :=
        Build t_stack t_continuation t_reconstruct r.(stack) r.(continuation)
          reconstruct.
    End Ex_split_log.
    Definition Ex_split_log_skeleton := Ex_split_log.record.

    Module Ex_split_loop_may_fail.
      Record record {body_init_stack body cont_init_stack continuation
        reconstruct : Set} : Set := Build {
        body_init_stack : body_init_stack;
        body : body;
        cont_init_stack : cont_init_stack;
        continuation : continuation;
        reconstruct : reconstruct;
      }.
      Arguments record : clear implicits.
      Definition with_body_init_stack
        {t_body_init_stack t_body t_cont_init_stack t_continuation t_reconstruct}
        body_init_stack
        (r :
          record t_body_init_stack t_body t_cont_init_stack t_continuation
            t_reconstruct) :=
        Build t_body_init_stack t_body t_cont_init_stack t_continuation
          t_reconstruct body_init_stack r.(body) r.(cont_init_stack)
          r.(continuation) r.(reconstruct).
      Definition with_body
        {t_body_init_stack t_body t_cont_init_stack t_continuation t_reconstruct}
        body
        (r :
          record t_body_init_stack t_body t_cont_init_stack t_continuation
            t_reconstruct) :=
        Build t_body_init_stack t_body t_cont_init_stack t_continuation
          t_reconstruct r.(body_init_stack) body r.(cont_init_stack)
          r.(continuation) r.(reconstruct).
      Definition with_cont_init_stack
        {t_body_init_stack t_body t_cont_init_stack t_continuation t_reconstruct}
        cont_init_stack
        (r :
          record t_body_init_stack t_body t_cont_init_stack t_continuation
            t_reconstruct) :=
        Build t_body_init_stack t_body t_cont_init_stack t_continuation
          t_reconstruct r.(body_init_stack) r.(body) cont_init_stack
          r.(continuation) r.(reconstruct).
      Definition with_continuation
        {t_body_init_stack t_body t_cont_init_stack t_continuation t_reconstruct}
        continuation
        (r :
          record t_body_init_stack t_body t_cont_init_stack t_continuation
            t_reconstruct) :=
        Build t_body_init_stack t_body t_cont_init_stack t_continuation
          t_reconstruct r.(body_init_stack) r.(body) r.(cont_init_stack)
          continuation r.(reconstruct).
      Definition with_reconstruct
        {t_body_init_stack t_body t_cont_init_stack t_continuation t_reconstruct}
        reconstruct
        (r :
          record t_body_init_stack t_body t_cont_init_stack t_continuation
            t_reconstruct) :=
        Build t_body_init_stack t_body t_cont_init_stack t_continuation
          t_reconstruct r.(body_init_stack) r.(body) r.(cont_init_stack)
          r.(continuation) reconstruct.
    End Ex_split_loop_may_fail.
    Definition Ex_split_loop_may_fail_skeleton := Ex_split_loop_may_fail.record.

    Module Ex_split_loop_may_not_fail.
      Record record {body_init_stack body continuation aft_body_stack_transform
        reconstruct : Set} : Set := Build {
        body_init_stack : body_init_stack;
        body : body;
        continuation : continuation;
        aft_body_stack_transform : aft_body_stack_transform;
        reconstruct : reconstruct;
      }.
      Arguments record : clear implicits.
      Definition with_body_init_stack
        {t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct} body_init_stack
        (r :
          record t_body_init_stack t_body t_continuation
            t_aft_body_stack_transform t_reconstruct) :=
        Build t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct body_init_stack r.(body) r.(continuation)
          r.(aft_body_stack_transform) r.(reconstruct).
      Definition with_body
        {t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct} body
        (r :
          record t_body_init_stack t_body t_continuation
            t_aft_body_stack_transform t_reconstruct) :=
        Build t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct r.(body_init_stack) body r.(continuation)
          r.(aft_body_stack_transform) r.(reconstruct).
      Definition with_continuation
        {t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct} continuation
        (r :
          record t_body_init_stack t_body t_continuation
            t_aft_body_stack_transform t_reconstruct) :=
        Build t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct r.(body_init_stack) r.(body) continuation
          r.(aft_body_stack_transform) r.(reconstruct).
      Definition with_aft_body_stack_transform
        {t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct} aft_body_stack_transform
        (r :
          record t_body_init_stack t_body t_continuation
            t_aft_body_stack_transform t_reconstruct) :=
        Build t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct r.(body_init_stack) r.(body) r.(continuation)
          aft_body_stack_transform r.(reconstruct).
      Definition with_reconstruct
        {t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct} reconstruct
        (r :
          record t_body_init_stack t_body t_continuation
            t_aft_body_stack_transform t_reconstruct) :=
        Build t_body_init_stack t_body t_continuation t_aft_body_stack_transform
          t_reconstruct r.(body_init_stack) r.(body) r.(continuation)
          r.(aft_body_stack_transform) reconstruct.
    End Ex_split_loop_may_not_fail.
    Definition Ex_split_loop_may_not_fail_skeleton :=
      Ex_split_loop_may_not_fail.record.

    Module Ex_split_if.
      Record record {left_init_stack left_branch right_init_stack right_branch
        continuation reconstruct : Set} : Set := Build {
        left_init_stack : left_init_stack;
        left_branch : left_branch;
        right_init_stack : right_init_stack;
        right_branch : right_branch;
        continuation : continuation;
        reconstruct : reconstruct;
      }.
      Arguments record : clear implicits.
      Definition with_left_init_stack
        {t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct} left_init_stack
        (r :
          record t_left_init_stack t_left_branch t_right_init_stack
            t_right_branch t_continuation t_reconstruct) :=
        Build t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct left_init_stack r.(left_branch)
          r.(right_init_stack) r.(right_branch) r.(continuation)
          r.(reconstruct).
      Definition with_left_branch
        {t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct} left_branch
        (r :
          record t_left_init_stack t_left_branch t_right_init_stack
            t_right_branch t_continuation t_reconstruct) :=
        Build t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct r.(left_init_stack) left_branch
          r.(right_init_stack) r.(right_branch) r.(continuation)
          r.(reconstruct).
      Definition with_right_init_stack
        {t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct} right_init_stack
        (r :
          record t_left_init_stack t_left_branch t_right_init_stack
            t_right_branch t_continuation t_reconstruct) :=
        Build t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct r.(left_init_stack) r.(left_branch)
          right_init_stack r.(right_branch) r.(continuation) r.(reconstruct).
      Definition with_right_branch
        {t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct} right_branch
        (r :
          record t_left_init_stack t_left_branch t_right_init_stack
            t_right_branch t_continuation t_reconstruct) :=
        Build t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct r.(left_init_stack) r.(left_branch)
          r.(right_init_stack) right_branch r.(continuation) r.(reconstruct).
      Definition with_continuation
        {t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct} continuation
        (r :
          record t_left_init_stack t_left_branch t_right_init_stack
            t_right_branch t_continuation t_reconstruct) :=
        Build t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct r.(left_init_stack) r.(left_branch)
          r.(right_init_stack) r.(right_branch) continuation r.(reconstruct).
      Definition with_reconstruct
        {t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct} reconstruct
        (r :
          record t_left_init_stack t_left_branch t_right_init_stack
            t_right_branch t_continuation t_reconstruct) :=
        Build t_left_init_stack t_left_branch t_right_init_stack t_right_branch
          t_continuation t_reconstruct r.(left_init_stack) r.(left_branch)
          r.(right_init_stack) r.(right_branch) r.(continuation) reconstruct.
    End Ex_split_if.
    Definition Ex_split_if_skeleton := Ex_split_if.record.

    Module Ex_split_failwith.
      Record record {location arg_ty cast : Set} : Set := Build {
        location : location;
        arg_ty : arg_ty;
        cast : cast;
      }.
      Arguments record : clear implicits.
      Definition with_location {t_location t_arg_ty t_cast} location
        (r : record t_location t_arg_ty t_cast) :=
        Build t_location t_arg_ty t_cast location r.(arg_ty) r.(cast).
      Definition with_arg_ty {t_location t_arg_ty t_cast} arg_ty
        (r : record t_location t_arg_ty t_cast) :=
        Build t_location t_arg_ty t_cast r.(location) arg_ty r.(cast).
      Definition with_cast {t_location t_arg_ty t_cast} cast
        (r : record t_location t_arg_ty t_cast) :=
        Build t_location t_arg_ty t_cast r.(location) r.(arg_ty) cast.
    End Ex_split_failwith.
    Definition Ex_split_failwith_skeleton := Ex_split_failwith.record.
  End ex_split_kinstr.
End ConstructorRecords_ex_split_kinstr.
Import ConstructorRecords_ex_split_kinstr.

Reserved Notation "'ex_split_kinstr.Ex_split_kinstr".
Reserved Notation "'ex_split_kinstr.Ex_split_log".
Reserved Notation "'ex_split_kinstr.Ex_split_loop_may_fail".
Reserved Notation "'ex_split_kinstr.Ex_split_loop_may_not_fail".
Reserved Notation "'ex_split_kinstr.Ex_split_if".
Reserved Notation "'ex_split_kinstr.Ex_split_failwith".

Inductive ex_split_kinstr : Set :=
| Ex_split_kinstr : 'ex_split_kinstr.Ex_split_kinstr ex_split_kinstr
| Ex_split_log : 'ex_split_kinstr.Ex_split_log ex_split_kinstr
| Ex_split_loop_may_fail :
  'ex_split_kinstr.Ex_split_loop_may_fail ex_split_kinstr
| Ex_split_loop_may_not_fail :
  'ex_split_kinstr.Ex_split_loop_may_not_fail ex_split_kinstr
| Ex_split_if : 'ex_split_kinstr.Ex_split_if ex_split_kinstr
| Ex_split_halt : Alpha_context.Script.location ex_split_kinstr
| Ex_split_failwith : 'ex_split_kinstr.Ex_split_failwith ex_split_kinstr

where "'ex_split_kinstr.Ex_split_kinstr" :=
  (ex_split_kinstr.Ex_split_kinstr_skeleton Script_typed_ir.stack_ty
    Script_typed_ir.kinstr (Script_typed_ir.kinstr Script_typed_ir.kinstr))
and "'ex_split_kinstr.Ex_split_log" :=
  (ex_split_kinstr.Ex_split_log_skeleton Script_typed_ir.stack_ty
    Script_typed_ir.kinstr (Script_typed_ir.kinstr Script_typed_ir.kinstr))
and "'ex_split_kinstr.Ex_split_loop_may_fail" :=
  (ex_split_kinstr.Ex_split_loop_may_fail_skeleton Script_typed_ir.stack_ty
    Script_typed_ir.kinstr Script_typed_ir.stack_ty Script_typed_ir.kinstr
    (Script_typed_ir.kinstr Script_typed_ir.kinstr Script_typed_ir.kinstr))
and "'ex_split_kinstr.Ex_split_loop_may_not_fail" :=
  (ex_split_kinstr.Ex_split_loop_may_not_fail_skeleton Script_typed_ir.stack_ty
    Script_typed_ir.kinstr Script_typed_ir.kinstr
    (Script_typed_ir.stack_ty M? Script_typed_ir.stack_ty)
    (Script_typed_ir.kinstr Script_typed_ir.kinstr Script_typed_ir.kinstr))
and "'ex_split_kinstr.Ex_split_if" :=
  (ex_split_kinstr.Ex_split_if_skeleton Script_typed_ir.stack_ty
    Script_typed_ir.kinstr Script_typed_ir.stack_ty Script_typed_ir.kinstr
    Script_typed_ir.kinstr
    (Script_typed_ir.kinstr Script_typed_ir.kinstr
    Script_typed_ir.kinstr Script_typed_ir.kinstr))
and "'ex_split_kinstr.Ex_split_failwith" :=
  (ex_split_kinstr.Ex_split_failwith_skeleton Alpha_context.Script.location
    Script_typed_ir.ty failed_kinstr_cast).

Module ex_split_kinstr.
  Include ConstructorRecords_ex_split_kinstr.ex_split_kinstr.
  Definition Ex_split_kinstr := 'ex_split_kinstr.Ex_split_kinstr.
  Definition Ex_split_log := 'ex_split_kinstr.Ex_split_log.
  Definition Ex_split_loop_may_fail := 'ex_split_kinstr.Ex_split_loop_may_fail.
  Definition Ex_split_loop_may_not_fail :=
    'ex_split_kinstr.Ex_split_loop_may_not_fail.
  Definition Ex_split_if := 'ex_split_kinstr.Ex_split_if.
  Definition Ex_split_failwith := 'ex_split_kinstr.Ex_split_failwith.
End ex_split_kinstr.

Inductive ex_init_stack_ty : Set :=
| Ex_init_stack_ty :
  Script_typed_ir.stack_ty Script_typed_ir.kinstr ex_init_stack_ty.

Fixpoint stack_prefix_preservation_witness_split_input
  (w_value : Script_typed_ir.stack_prefix_preservation_witness)
  (s_value : Script_typed_ir.stack_ty) : Script_typed_ir.stack_ty :=
  match (w_value, s_value) with
  | (Script_typed_ir.KPrefix _ _ w_value, Script_typed_ir.Item_t _ s_value)
    stack_prefix_preservation_witness_split_input w_value s_value
  | (Script_typed_ir.KRest, s_value)s_value
  | _unreachable_gadt_branch
  end.

Fixpoint stack_prefix_preservation_witness_split_output
  (w_value : Script_typed_ir.stack_prefix_preservation_witness)
  (s_value : Script_typed_ir.stack_ty) : Script_typed_ir.stack_ty :=
  match (w_value, s_value) with
  | (Script_typed_ir.KPrefix _ a_value w_value, s_value)
    Script_typed_ir.Item_t a_value
      (stack_prefix_preservation_witness_split_output w_value s_value)
  | (Script_typed_ir.KRest, s_value)s_value
  end.

Definition assert_some {A : Set} (v_value : option A) : M? A :=
  match v_value with
  | NoneError_monad.error_value (Build_extensible "Asserted" unit tt)
  | Some x_valuereturn? x_value
  end.

Definition kinstr_split
  (s_value : Script_typed_ir.stack_ty) (i_value : Script_typed_ir.kinstr)
  : M? ex_split_kinstr :=
  let dummy := Micheline.dummy_location in
  match (i_value, s_value) with
  | (Script_typed_ir.IDrop loc_value k_value, Script_typed_ir.Item_t _a s_value)
    ⇒
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IDrop loc_value k_value; |})
  |
    (Script_typed_ir.IDup loc_value k_value,
      Script_typed_ir.Item_t a_value s_value)
    let s_value :=
      Script_typed_ir.Item_t a_value (Script_typed_ir.Item_t a_value s_value) in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IDup loc_value k_value; |})
  |
    (Script_typed_ir.ISwap loc_value k_value,
      Script_typed_ir.Item_t a_value (Script_typed_ir.Item_t b_value s_value))
    ⇒
    let s_value :=
      Script_typed_ir.Item_t b_value (Script_typed_ir.Item_t a_value s_value) in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISwap loc_value k_value; |})
  | (Script_typed_ir.IConst loc_value a_value x_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t a_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IConst loc_value a_value x_value k_value; |})
  |
    (Script_typed_ir.ICons_pair loc_value k_value,
      Script_typed_ir.Item_t a_value (Script_typed_ir.Item_t b_value s_value))
    ⇒
    let? 'Script_typed_ir.Ty_ex_c c_value :=
      Script_typed_ir.pair_t dummy a_value b_value in
    let s_value := Script_typed_ir.Item_t c_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICons_pair loc_value k_value; |})
  |
    (Script_typed_ir.ICar loc_value k_value,
      Script_typed_ir.Item_t (Script_typed_ir.Pair_t a_value _b _meta _) s_value)
    ⇒
    let s_value := Script_typed_ir.Item_t a_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICar loc_value k_value; |})
  |
    (Script_typed_ir.ICdr loc_value k_value,
      Script_typed_ir.Item_t (Script_typed_ir.Pair_t _a b_value _meta _) s_value)
    ⇒
    let s_value := Script_typed_ir.Item_t b_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICdr loc_value k_value; |})
  |
    (Script_typed_ir.IUnpair loc_value k_value,
      Script_typed_ir.Item_t (Script_typed_ir.Pair_t a_value b_value _meta _)
        s_value)
    let s_value :=
      Script_typed_ir.Item_t a_value (Script_typed_ir.Item_t b_value s_value) in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IUnpair loc_value k_value; |})
  |
    (Script_typed_ir.ICons_some loc_value k_value,
      Script_typed_ir.Item_t a_value s_value)
    let? o_value := Script_typed_ir.option_t dummy a_value in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICons_some loc_value k_value; |})
  | (Script_typed_ir.ICons_none loc_value a_value k_value, s_value)
    let? o_value := Script_typed_ir.option_t dummy a_value in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICons_none loc_value a_value k_value; |})
  |
    (Script_typed_ir.IIf_none {|
      Script_typed_ir.kinstr.IIf_none.loc := loc_value;
        Script_typed_ir.kinstr.IIf_none.branch_if_none := branch_if_none;
        Script_typed_ir.kinstr.IIf_none.branch_if_some := branch_if_some;
        Script_typed_ir.kinstr.IIf_none.k := k_value
        |},
      Script_typed_ir.Item_t (Script_typed_ir.Option_t a_value _meta _) s_value)
    ⇒
    return?
      (Ex_split_if
        {| ex_split_kinstr.Ex_split_if.left_init_stack := s_value;
          ex_split_kinstr.Ex_split_if.left_branch := branch_if_none;
          ex_split_kinstr.Ex_split_if.right_init_stack :=
            Script_typed_ir.Item_t a_value s_value;
          ex_split_kinstr.Ex_split_if.right_branch := branch_if_some;
          ex_split_kinstr.Ex_split_if.continuation := k_value;
          ex_split_kinstr.Ex_split_if.reconstruct :=
            fun (branch_if_none : Script_typed_ir.kinstr) ⇒
              fun (branch_if_some : Script_typed_ir.kinstr) ⇒
                fun (k_value : Script_typed_ir.kinstr) ⇒
                  Script_typed_ir.IIf_none
                    {| Script_typed_ir.kinstr.IIf_none.loc := loc_value;
                      Script_typed_ir.kinstr.IIf_none.branch_if_none :=
                        branch_if_none;
                      Script_typed_ir.kinstr.IIf_none.branch_if_some :=
                        branch_if_some;
                      Script_typed_ir.kinstr.IIf_none.k := k_value; |}; |})
  |
    (Script_typed_ir.IOpt_map {|
      Script_typed_ir.kinstr.IOpt_map.loc := loc_value;
        Script_typed_ir.kinstr.IOpt_map.body := body;
        Script_typed_ir.kinstr.IOpt_map.k := k_value
        |},
      Script_typed_ir.Item_t (Script_typed_ir.Option_t a_value _meta _) s_value)
    ⇒
    return?
      (Ex_split_loop_may_not_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_not_fail.body_init_stack :=
            Script_typed_ir.Item_t a_value s_value;
          ex_split_kinstr.Ex_split_loop_may_not_fail.body := body;
          ex_split_kinstr.Ex_split_loop_may_not_fail.continuation := k_value;
          ex_split_kinstr.Ex_split_loop_may_not_fail.aft_body_stack_transform :=
            fun (function_parameter : Script_typed_ir.stack_ty) ⇒
              match function_parameter with
              | Script_typed_ir.Item_t b_value s_value
                let? o_value := Script_typed_ir.option_t dummy b_value in
                return? (Script_typed_ir.Item_t o_value s_value)
              | _unreachable_gadt_branch
              end;
          ex_split_kinstr.Ex_split_loop_may_not_fail.reconstruct :=
            fun (body : Script_typed_ir.kinstr) ⇒
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.IOpt_map
                  {| Script_typed_ir.kinstr.IOpt_map.loc := loc_value;
                    Script_typed_ir.kinstr.IOpt_map.body := body;
                    Script_typed_ir.kinstr.IOpt_map.k := k_value; |}; |})
  |
    (Script_typed_ir.ICons_left loc_value b_value k_value,
      Script_typed_ir.Item_t a_value s_value)
    let? 'Script_typed_ir.Ty_ex_c c_value :=
      Script_typed_ir.union_t dummy a_value b_value in
    let s_value := Script_typed_ir.Item_t c_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICons_left loc_value b_value k_value; |})
  |
    (Script_typed_ir.ICons_right loc_value a_value k_value,
      Script_typed_ir.Item_t b_value s_value)
    let? 'Script_typed_ir.Ty_ex_c c_value :=
      Script_typed_ir.union_t dummy a_value b_value in
    let s_value := Script_typed_ir.Item_t c_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICons_right loc_value a_value k_value; |})
  |
    (Script_typed_ir.IIf_left {|
      Script_typed_ir.kinstr.IIf_left.loc := loc_value;
        Script_typed_ir.kinstr.IIf_left.branch_if_left := branch_if_left;
        Script_typed_ir.kinstr.IIf_left.branch_if_right := branch_if_right;
        Script_typed_ir.kinstr.IIf_left.k := k_value
        |},
      Script_typed_ir.Item_t (Script_typed_ir.Union_t a_value b_value _meta _)
        s_value)
    return?
      (Ex_split_if
        {|
          ex_split_kinstr.Ex_split_if.left_init_stack :=
            Script_typed_ir.Item_t a_value s_value;
          ex_split_kinstr.Ex_split_if.left_branch := branch_if_left;
          ex_split_kinstr.Ex_split_if.right_init_stack :=
            Script_typed_ir.Item_t b_value s_value;
          ex_split_kinstr.Ex_split_if.right_branch := branch_if_right;
          ex_split_kinstr.Ex_split_if.continuation := k_value;
          ex_split_kinstr.Ex_split_if.reconstruct :=
            fun (branch_if_left : Script_typed_ir.kinstr) ⇒
              fun (branch_if_right : Script_typed_ir.kinstr) ⇒
                fun (k_value : Script_typed_ir.kinstr) ⇒
                  Script_typed_ir.IIf_left
                    {| Script_typed_ir.kinstr.IIf_left.loc := loc_value;
                      Script_typed_ir.kinstr.IIf_left.branch_if_left :=
                        branch_if_left;
                      Script_typed_ir.kinstr.IIf_left.branch_if_right :=
                        branch_if_right;
                      Script_typed_ir.kinstr.IIf_left.k := k_value; |}; |})
  |
    (Script_typed_ir.ICons_list loc_value k_value,
      Script_typed_ir.Item_t _a (Script_typed_ir.Item_t l_value s_value))
    let s_value := Script_typed_ir.Item_t l_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICons_list loc_value k_value; |})
  | (Script_typed_ir.INil loc_value a_value k_value, s_value)
    let? l_value := Script_typed_ir.list_t dummy a_value in
    let s_value := Script_typed_ir.Item_t l_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INil loc_value a_value k_value; |})
  |
    (Script_typed_ir.IIf_cons {|
      Script_typed_ir.kinstr.IIf_cons.loc := loc_value;
        Script_typed_ir.kinstr.IIf_cons.branch_if_cons := branch_if_cons;
        Script_typed_ir.kinstr.IIf_cons.branch_if_nil := branch_if_nil;
        Script_typed_ir.kinstr.IIf_cons.k := k_value
        |},
      Script_typed_ir.Item_t ((Script_typed_ir.List_t a_value _meta) as l_value)
        s_value)
    return?
      (Ex_split_if
        {|
          ex_split_kinstr.Ex_split_if.left_init_stack :=
            Script_typed_ir.Item_t a_value
              (Script_typed_ir.Item_t l_value s_value);
          ex_split_kinstr.Ex_split_if.left_branch := branch_if_cons;
          ex_split_kinstr.Ex_split_if.right_init_stack := s_value;
          ex_split_kinstr.Ex_split_if.right_branch := branch_if_nil;
          ex_split_kinstr.Ex_split_if.continuation := k_value;
          ex_split_kinstr.Ex_split_if.reconstruct :=
            fun (branch_if_cons : Script_typed_ir.kinstr) ⇒
              fun (branch_if_nil : Script_typed_ir.kinstr) ⇒
                fun (k_value : Script_typed_ir.kinstr) ⇒
                  Script_typed_ir.IIf_cons
                    {| Script_typed_ir.kinstr.IIf_cons.loc := loc_value;
                      Script_typed_ir.kinstr.IIf_cons.branch_if_cons :=
                        branch_if_cons;
                      Script_typed_ir.kinstr.IIf_cons.branch_if_nil :=
                        branch_if_nil;
                      Script_typed_ir.kinstr.IIf_cons.k := k_value; |}; |})
  |
    (Script_typed_ir.IList_map loc_value body ty_value k_value,
      Script_typed_ir.Item_t (Script_typed_ir.List_t a_value _meta) s_value)
    let s_value := Script_typed_ir.Item_t a_value s_value in
    return?
      (Ex_split_loop_may_not_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_not_fail.body_init_stack := s_value;
          ex_split_kinstr.Ex_split_loop_may_not_fail.body := body;
          ex_split_kinstr.Ex_split_loop_may_not_fail.continuation := k_value;
          ex_split_kinstr.Ex_split_loop_may_not_fail.aft_body_stack_transform :=
            fun (function_parameter : Script_typed_ir.stack_ty) ⇒
              match function_parameter with
              | Script_typed_ir.Item_t b_value s_value
                let? l_value := Script_typed_ir.list_t dummy b_value in
                return? (Script_typed_ir.Item_t l_value s_value)
              | _unreachable_gadt_branch
              end;
          ex_split_kinstr.Ex_split_loop_may_not_fail.reconstruct :=
            fun (body : Script_typed_ir.kinstr) ⇒
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.IList_map loc_value body ty_value k_value; |})
  |
    (Script_typed_ir.IList_iter loc_value ty_value body k_value,
      Script_typed_ir.Item_t (Script_typed_ir.List_t a_value _meta) s_value)
    return?
      (Ex_split_loop_may_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_fail.body_init_stack :=
            Script_typed_ir.Item_t a_value s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.body := body;
          ex_split_kinstr.Ex_split_loop_may_fail.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.continuation := k_value;
          ex_split_kinstr.Ex_split_loop_may_fail.reconstruct :=
            fun (body : Script_typed_ir.kinstr) ⇒
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.IList_iter loc_value ty_value body k_value; |})
  |
    (Script_typed_ir.IList_size loc_value k_value,
      Script_typed_ir.Item_t _l s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IList_size loc_value k_value; |})
  | (Script_typed_ir.IEmpty_set loc_value a_value k_value, s_value)
    let? b_value := Script_typed_ir.set_t dummy a_value in
    let s_value := Script_typed_ir.Item_t b_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEmpty_set loc_value a_value k_value; |})
  |
    (Script_typed_ir.ISet_iter loc_value a_value body k_value,
      Script_typed_ir.Item_t _b s_value)
    let? asa := assert_some a_value in
    return?
      (Ex_split_loop_may_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_fail.body_init_stack :=
            Script_typed_ir.Item_t asa s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.body := body;
          ex_split_kinstr.Ex_split_loop_may_fail.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.continuation := k_value;
          ex_split_kinstr.Ex_split_loop_may_fail.reconstruct :=
            fun (body : Script_typed_ir.kinstr) ⇒
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.ISet_iter loc_value a_value body k_value; |})
  |
    (Script_typed_ir.ISet_mem loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISet_mem loc_value k_value; |})
  |
    (Script_typed_ir.ISet_update loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISet_update loc_value k_value; |})
  |
    (Script_typed_ir.ISet_size loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISet_size loc_value k_value; |})
  | (Script_typed_ir.IEmpty_map loc_value cty vty k_value, s_value)
    let? asvty := assert_some vty in
    let? m_value := Script_typed_ir.map_t dummy cty asvty in
    let s_value := Script_typed_ir.Item_t m_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEmpty_map loc_value cty vty k_value; |})
  |
    (Script_typed_ir.IMap_map loc_value ty_value body k_value,
      Script_typed_ir.Item_t (Script_typed_ir.Map_t kty vty _meta) s_value)
    let? asty := assert_some ty_value in
    match asty with
    | Script_typed_ir.Map_t key_ty _ _
      let? 'Script_typed_ir.Ty_ex_c p_value :=
        Script_typed_ir.pair_t dummy key_ty vty in
      return?
        (Ex_split_loop_may_not_fail
          {|
            ex_split_kinstr.Ex_split_loop_may_not_fail.body_init_stack :=
              Script_typed_ir.Item_t p_value s_value;
            ex_split_kinstr.Ex_split_loop_may_not_fail.body := body;
            ex_split_kinstr.Ex_split_loop_may_not_fail.continuation := k_value;
            ex_split_kinstr.Ex_split_loop_may_not_fail.aft_body_stack_transform
              :=
              fun (function_parameter : Script_typed_ir.stack_ty) ⇒
                match function_parameter with
                | Script_typed_ir.Item_t b_value s_value
                  let? m_value := Script_typed_ir.map_t dummy kty b_value in
                  return? (Script_typed_ir.Item_t m_value s_value)
                | _unreachable_gadt_branch
                end;
            ex_split_kinstr.Ex_split_loop_may_not_fail.reconstruct :=
              fun (body : Script_typed_ir.kinstr) ⇒
                fun (k_value : Script_typed_ir.kinstr) ⇒
                  Script_typed_ir.IMap_map loc_value ty_value body k_value; |})
    | _unreachable_gadt_branch
    end
  |
    (Script_typed_ir.IMap_iter loc_value kvty body k_value,
      Script_typed_ir.Item_t _ stack_value)
    let? askvty := assert_some kvty in
    return?
      (Ex_split_loop_may_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_fail.body_init_stack :=
            Script_typed_ir.Item_t askvty stack_value;
          ex_split_kinstr.Ex_split_loop_may_fail.body := body;
          ex_split_kinstr.Ex_split_loop_may_fail.cont_init_stack := stack_value;
          ex_split_kinstr.Ex_split_loop_may_fail.continuation := k_value;
          ex_split_kinstr.Ex_split_loop_may_fail.reconstruct :=
            fun (body : Script_typed_ir.kinstr) ⇒
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.IMap_iter loc_value kvty body k_value; |})
  |
    (Script_typed_ir.IMap_mem loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMap_mem loc_value k_value; |})
  |
    (Script_typed_ir.IMap_get loc_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t (Script_typed_ir.Map_t _kty vty _meta) s_value))
    ⇒
    let? o_value := Script_typed_ir.option_t dummy vty in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMap_get loc_value k_value; |})
  |
    (Script_typed_ir.IMap_update loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMap_update loc_value k_value; |})
  |
    (Script_typed_ir.IMap_get_and_update loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMap_get_and_update loc_value k_value; |})
  |
    (Script_typed_ir.IMap_size loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMap_size loc_value k_value; |})
  | (Script_typed_ir.IEmpty_big_map loc_value cty ty_value k_value, s_value)
    let? b_value := Script_typed_ir.big_map_t dummy cty ty_value in
    let s_value := Script_typed_ir.Item_t b_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEmpty_big_map loc_value cty ty_value k_value; |})
  |
    (Script_typed_ir.IBig_map_mem loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IBig_map_mem loc_value k_value; |})
  |
    (Script_typed_ir.IBig_map_get loc_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t (Script_typed_ir.Big_map_t _kty vty _meta)
          s_value))
    let? o_value := Script_typed_ir.option_t dummy vty in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IBig_map_get loc_value k_value; |})
  |
    (Script_typed_ir.IBig_map_update loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IBig_map_update loc_value k_value; |})
  |
    (Script_typed_ir.IBig_map_get_and_update loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IBig_map_get_and_update loc_value k_value; |})
  |
    (Script_typed_ir.IConcat_string loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.string_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IConcat_string loc_value k_value; |})
  |
    (Script_typed_ir.IConcat_string_pair loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IConcat_string_pair loc_value k_value; |})
  |
    (Script_typed_ir.ISlice_string loc_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value)))
    let s_value :=
      Script_typed_ir.Item_t Script_typed_ir.option_string_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISlice_string loc_value k_value; |})
  |
    (Script_typed_ir.IString_size loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IString_size loc_value k_value; |})
  |
    (Script_typed_ir.IConcat_bytes loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bytes_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IConcat_bytes loc_value k_value; |})
  |
    (Script_typed_ir.IConcat_bytes_pair loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IConcat_bytes_pair loc_value k_value; |})
  |
    (Script_typed_ir.ISlice_bytes loc_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value)))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.option_bytes_t s_value
      in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISlice_bytes loc_value k_value; |})
  |
    (Script_typed_ir.IBytes_size loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IBytes_size loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_seconds_to_timestamp loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_seconds_to_timestamp loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_timestamp_to_seconds loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.timestamp_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_timestamp_to_seconds loc_value k_value; |})
  |
    (Script_typed_ir.ISub_timestamp_seconds loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.timestamp_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISub_timestamp_seconds loc_value k_value; |})
  |
    (Script_typed_ir.IDiff_timestamps loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IDiff_timestamps loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_tez loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_tez loc_value k_value; |})
  |
    (Script_typed_ir.ISub_tez loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.option_mutez_t s_value
      in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISub_tez loc_value k_value; |})
  |
    (Script_typed_ir.ISub_tez_legacy loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISub_tez_legacy loc_value k_value; |})
  |
    (Script_typed_ir.IMul_teznat loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.mutez_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_teznat loc_value k_value; |})
  |
    (Script_typed_ir.IMul_nattez loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_nattez loc_value k_value; |})
  |
    (Script_typed_ir.IEdiv_teznat loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value :=
      Script_typed_ir.Item_t Script_typed_ir.option_pair_mutez_mutez_t s_value
      in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEdiv_teznat loc_value k_value; |})
  |
    (Script_typed_ir.IEdiv_tez loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value :=
      Script_typed_ir.Item_t Script_typed_ir.option_pair_nat_mutez_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEdiv_tez loc_value k_value; |})
  | (Script_typed_ir.IOr loc_value k_value, Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IOr loc_value k_value; |})
  | (Script_typed_ir.IAnd loc_value k_value, Script_typed_ir.Item_t _ s_value)
    ⇒
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAnd loc_value k_value; |})
  | (Script_typed_ir.IXor loc_value k_value, Script_typed_ir.Item_t _ s_value)
    ⇒
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IXor loc_value k_value; |})
  | (Script_typed_ir.INot loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INot loc_value k_value; |})
  |
    (Script_typed_ir.IIs_nat loc_value k_value, Script_typed_ir.Item_t _ s_value)
    ⇒
    let s_value := Script_typed_ir.Item_t Script_typed_ir.option_nat_t s_value
      in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IIs_nat loc_value k_value; |})
  | (Script_typed_ir.INeg loc_value k_value, Script_typed_ir.Item_t _ s_value)
    ⇒
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INeg loc_value k_value; |})
  |
    (Script_typed_ir.IAbs_int loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAbs_int loc_value k_value; |})
  |
    (Script_typed_ir.IInt_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IInt_nat loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_int loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_int loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_nat loc_value k_value; |})
  |
    (Script_typed_ir.ISub_int loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISub_int loc_value k_value; |})
  |
    (Script_typed_ir.IMul_int loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_int loc_value k_value; |})
  |
    (Script_typed_ir.IMul_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_nat loc_value k_value; |})
  |
    (Script_typed_ir.IEdiv_int loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value :=
      Script_typed_ir.Item_t Script_typed_ir.option_pair_int_nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEdiv_int loc_value k_value; |})
  |
    (Script_typed_ir.IEdiv_nat loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t a_value s_value))
    let? 'Script_typed_ir.Ty_ex_c p_value :=
      Script_typed_ir.pair_t dummy a_value Script_typed_ir.nat_t in
    let? o_value := Script_typed_ir.option_t dummy p_value in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEdiv_nat loc_value k_value; |})
  |
    (Script_typed_ir.ILsl_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ILsl_nat loc_value k_value; |})
  |
    (Script_typed_ir.ILsr_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ILsr_nat loc_value k_value; |})
  |
    (Script_typed_ir.IOr_nat loc_value k_value, Script_typed_ir.Item_t _ s_value)
    ⇒
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IOr_nat loc_value k_value; |})
  |
    (Script_typed_ir.IAnd_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAnd_nat loc_value k_value; |})
  |
    (Script_typed_ir.IAnd_int_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAnd_int_nat loc_value k_value; |})
  |
    (Script_typed_ir.IXor_nat loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IXor_nat loc_value k_value; |})
  |
    (Script_typed_ir.INot_int loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INot_int loc_value k_value; |})
  |
    (Script_typed_ir.IIf {|
      Script_typed_ir.kinstr.IIf.loc := loc_value;
        Script_typed_ir.kinstr.IIf.branch_if_true := branch_if_true;
        Script_typed_ir.kinstr.IIf.branch_if_false := branch_if_false;
        Script_typed_ir.kinstr.IIf.k := k_value
        |}, Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_if
        {| ex_split_kinstr.Ex_split_if.left_init_stack := s_value;
          ex_split_kinstr.Ex_split_if.left_branch := branch_if_true;
          ex_split_kinstr.Ex_split_if.right_init_stack := s_value;
          ex_split_kinstr.Ex_split_if.right_branch := branch_if_false;
          ex_split_kinstr.Ex_split_if.continuation := k_value;
          ex_split_kinstr.Ex_split_if.reconstruct :=
            fun (branch_if_true : Script_typed_ir.kinstr) ⇒
              fun (branch_if_false : Script_typed_ir.kinstr) ⇒
                fun (k_value : Script_typed_ir.kinstr) ⇒
                  Script_typed_ir.IIf
                    {| Script_typed_ir.kinstr.IIf.loc := loc_value;
                      Script_typed_ir.kinstr.IIf.branch_if_true :=
                        branch_if_true;
                      Script_typed_ir.kinstr.IIf.branch_if_false :=
                        branch_if_false;
                      Script_typed_ir.kinstr.IIf.k := k_value; |}; |})
  |
    (Script_typed_ir.ILoop loc_value body k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_loop_may_fail
        {| ex_split_kinstr.Ex_split_loop_may_fail.body_init_stack := s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.body := body;
          ex_split_kinstr.Ex_split_loop_may_fail.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.continuation := k_value;
          ex_split_kinstr.Ex_split_loop_may_fail.reconstruct :=
            fun (body : Script_typed_ir.kinstr) ⇒
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.ILoop loc_value body k_value; |})
  |
    (Script_typed_ir.ILoop_left loc_value kl kr,
      Script_typed_ir.Item_t (Script_typed_ir.Union_t a_value b_value _meta _)
        s_value)
    return?
      (Ex_split_loop_may_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_fail.body_init_stack :=
            Script_typed_ir.Item_t a_value s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.body := kl;
          ex_split_kinstr.Ex_split_loop_may_fail.cont_init_stack :=
            Script_typed_ir.Item_t b_value s_value;
          ex_split_kinstr.Ex_split_loop_may_fail.continuation := kr;
          ex_split_kinstr.Ex_split_loop_may_fail.reconstruct :=
            fun (kl : Script_typed_ir.kinstr) ⇒
              fun (kr : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.ILoop_left loc_value kl kr; |})
  |
    (Script_typed_ir.IDip loc_value body ty_value k_value,
      Script_typed_ir.Item_t a_value s_value)
    return?
      (Ex_split_loop_may_not_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_not_fail.body_init_stack := s_value;
          ex_split_kinstr.Ex_split_loop_may_not_fail.body := body;
          ex_split_kinstr.Ex_split_loop_may_not_fail.continuation := k_value;
          ex_split_kinstr.Ex_split_loop_may_not_fail.aft_body_stack_transform :=
            fun (s_value : Script_typed_ir.stack_ty) ⇒
              return? (Script_typed_ir.Item_t a_value s_value);
          ex_split_kinstr.Ex_split_loop_may_not_fail.reconstruct :=
            fun (body : Script_typed_ir.kinstr) ⇒
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.IDip loc_value body ty_value k_value; |})
  |
    (Script_typed_ir.IExec loc_value sty k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t (Script_typed_ir.Lambda_t _ b_value _meta)
          s_value))
    let s_value := Script_typed_ir.Item_t b_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IExec loc_value sty k_value; |})
  |
    (Script_typed_ir.IApply loc_value ty_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t
          (Script_typed_ir.Lambda_t (Script_typed_ir.Pair_t _ a_value _ _)
            b_value _) s_value))
    let? l_value := Script_typed_ir.lambda_t dummy a_value b_value in
    let s_value := Script_typed_ir.Item_t l_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IApply loc_value ty_value k_value; |})
  |
    (Script_typed_ir.ILambda loc_value ((Script_typed_ir.Lam desc _) as l_value)
      k_value, s_value)
    match
      (desc.(Script_typed_ir.kdescr.kbef), desc.(Script_typed_ir.kdescr.kaft))
      with
    |
      (Script_typed_ir.Item_t a_value Script_typed_ir.Bot_t,
        Script_typed_ir.Item_t b_value Script_typed_ir.Bot_t)
      let? lam := Script_typed_ir.lambda_t dummy a_value b_value in
      let s_value := Script_typed_ir.Item_t lam s_value in
      return?
        (Ex_split_kinstr
          {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
            ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
            ex_split_kinstr.Ex_split_kinstr.reconstruct :=
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.ILambda loc_value l_value k_value; |})
    | _unreachable_gadt_branch
    end
  |
    (Script_typed_ir.ILambda loc_value
      ((Script_typed_ir.LamRec desc _) as l_value) k_value, s_value)
    match
      (desc.(Script_typed_ir.kdescr.kbef), desc.(Script_typed_ir.kdescr.kaft))
      with
    |
      (Script_typed_ir.Item_t a_value
        (Script_typed_ir.Item_t (Script_typed_ir.Lambda_t _ _ _)
          Script_typed_ir.Bot_t),
        Script_typed_ir.Item_t b_value Script_typed_ir.Bot_t)
      let? lam := Script_typed_ir.lambda_t dummy a_value b_value in
      let s_value := Script_typed_ir.Item_t lam s_value in
      return?
        (Ex_split_kinstr
          {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
            ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
            ex_split_kinstr.Ex_split_kinstr.reconstruct :=
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.ILambda loc_value l_value k_value; |})
    | _unreachable_gadt_branch
    end
  | (Script_typed_ir.IFailwith location arg_ty, _)
    return?
      (Ex_split_failwith
        {| ex_split_kinstr.Ex_split_failwith.location := location;
          ex_split_kinstr.Ex_split_failwith.arg_ty := arg_ty;
          ex_split_kinstr.Ex_split_failwith.cast :=
            {|
              failed_kinstr_cast.cast :=
                Script_typed_ir.IFailwith location arg_ty; |}; |})
  |
    (Script_typed_ir.ICompare loc_value ty_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICompare loc_value ty_value k_value; |})
  | (Script_typed_ir.IEq loc_value k_value, Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEq loc_value k_value; |})
  | (Script_typed_ir.INeq loc_value k_value, Script_typed_ir.Item_t _ s_value)
    ⇒
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INeq loc_value k_value; |})
  | (Script_typed_ir.ILt loc_value k_value, Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ILt loc_value k_value; |})
  | (Script_typed_ir.IGt loc_value k_value, Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IGt loc_value k_value; |})
  | (Script_typed_ir.ILe loc_value k_value, Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ILe loc_value k_value; |})
  | (Script_typed_ir.IGe loc_value k_value, Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IGe loc_value k_value; |})
  |
    (Script_typed_ir.IAddress loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.address_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAddress loc_value k_value; |})
  |
    (Script_typed_ir.IContract loc_value ty_value code k_value,
      Script_typed_ir.Item_t _ s_value)
    let? c_value := Script_typed_ir.contract_t dummy ty_value in
    let? o_value := Script_typed_ir.option_t dummy c_value in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IContract loc_value ty_value code k_value; |})
  |
    (Script_typed_ir.ITransfer_tokens loc_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value)))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.operation_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ITransfer_tokens loc_value k_value; |})
  |
    (Script_typed_ir.IView loc_value
      ((Script_typed_ir.View_signature {|
        Script_typed_ir.view_signature.View_signature.output_ty := output_ty
          |}) as view_signature) sty k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let? b_value := Script_typed_ir.option_t dummy output_ty in
    let s_value := Script_typed_ir.Item_t b_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IView loc_value view_signature sty k_value; |})
  |
    (Script_typed_ir.IImplicit_account loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value :=
      Script_typed_ir.Item_t Script_typed_ir.contract_unit_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IImplicit_account loc_value k_value; |})
  |
    (Script_typed_ir.ICreate_contract {|
      Script_typed_ir.kinstr.ICreate_contract.loc := loc_value;
        Script_typed_ir.kinstr.ICreate_contract.storage_type := storage_type;
        Script_typed_ir.kinstr.ICreate_contract.code := code;
        Script_typed_ir.kinstr.ICreate_contract.k := k_value
        |},
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value)))
    return?
      (Ex_split_kinstr
        {|
          ex_split_kinstr.Ex_split_kinstr.cont_init_stack :=
            Script_typed_ir.Item_t Script_typed_ir.operation_t
              (Script_typed_ir.Item_t Script_typed_ir.address_t s_value);
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICreate_contract
                {| Script_typed_ir.kinstr.ICreate_contract.loc := loc_value;
                  Script_typed_ir.kinstr.ICreate_contract.storage_type :=
                    storage_type;
                  Script_typed_ir.kinstr.ICreate_contract.code := code;
                  Script_typed_ir.kinstr.ICreate_contract.k := k_value; |}; |})
  |
    (Script_typed_ir.ISet_delegate loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.operation_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISet_delegate loc_value k_value; |})
  | (Script_typed_ir.INow loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.timestamp_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INow loc_value k_value; |})
  | (Script_typed_ir.IBalance loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.mutez_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IBalance loc_value k_value; |})
  | (Script_typed_ir.ILevel loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ILevel loc_value k_value; |})
  |
    (Script_typed_ir.ICheck_signature loc_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value)))
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ICheck_signature loc_value k_value; |})
  |
    (Script_typed_ir.IHash_key loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.key_hash_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IHash_key loc_value k_value; |})
  |
    (Script_typed_ir.IPack loc_value ty_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bytes_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IPack loc_value ty_value k_value; |})
  |
    (Script_typed_ir.IUnpack loc_value ty_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let? o_value := Script_typed_ir.option_t dummy ty_value in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IUnpack loc_value ty_value k_value; |})
  | (Script_typed_ir.IBlake2b loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IBlake2b loc_value k_value; |})
  | (Script_typed_ir.ISha256 loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISha256 loc_value k_value; |})
  | (Script_typed_ir.ISha512 loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISha512 loc_value k_value; |})
  | (Script_typed_ir.ISource loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.address_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISource loc_value k_value; |})
  | (Script_typed_ir.ISender loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.address_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISender loc_value k_value; |})
  | (Script_typed_ir.ISelf loc_value ty_value ep k_value, s_value)
    let? c_value := Script_typed_ir.contract_t dummy ty_value in
    let s_value := Script_typed_ir.Item_t c_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISelf loc_value ty_value ep k_value; |})
  | (Script_typed_ir.ISelf_address loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.address_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISelf_address loc_value k_value; |})
  | (Script_typed_ir.IAmount loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.mutez_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAmount loc_value k_value; |})
  | (Script_typed_ir.ISapling_empty_state loc_value memo_size k_value, s_value)
    ⇒
    return?
      (Ex_split_kinstr
        {|
          ex_split_kinstr.Ex_split_kinstr.cont_init_stack :=
            Script_typed_ir.Item_t (Script_typed_ir.sapling_state_t memo_size)
              s_value; ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISapling_empty_state loc_value memo_size k_value;
          |})
  |
    (Script_typed_ir.ISapling_verify_update_deprecated loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t state_ty s_value))
    let? 'Script_typed_ir.Ty_ex_c pair_ty :=
      Script_typed_ir.pair_t dummy Script_typed_ir.int_t state_ty in
    let? ty_value := Script_typed_ir.option_t dummy pair_ty in
    return?
      (Ex_split_kinstr
        {|
          ex_split_kinstr.Ex_split_kinstr.cont_init_stack :=
            Script_typed_ir.Item_t ty_value s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISapling_verify_update_deprecated loc_value
                k_value; |})
  |
    (Script_typed_ir.ISapling_verify_update loc_value k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t state_ty s_value))
    let? 'Script_typed_ir.Ty_ex_c int_state_ty :=
      Script_typed_ir.pair_t dummy Script_typed_ir.int_t state_ty in
    let? 'Script_typed_ir.Ty_ex_c pair_ty :=
      Script_typed_ir.pair_t dummy Script_typed_ir.bytes_t int_state_ty in
    let? ty_value := Script_typed_ir.option_t dummy pair_ty in
    let s_value := Script_typed_ir.Item_t ty_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISapling_verify_update loc_value k_value; |})
  | (Script_typed_ir.IDig loc_value n_value p_value k_value, s_value)
    match stack_prefix_preservation_witness_split_input p_value s_value with
    | Script_typed_ir.Item_t b_value s_value
      let s_value :=
        stack_prefix_preservation_witness_split_output p_value s_value in
      let s_value := Script_typed_ir.Item_t b_value s_value in
      return?
        (Ex_split_kinstr
          {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
            ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
            ex_split_kinstr.Ex_split_kinstr.reconstruct :=
              fun (k_value : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.IDig loc_value n_value p_value k_value; |})
    | _unreachable_gadt_branch
    end
  |
    (Script_typed_ir.IDug loc_value n_value p_value k_value,
      Script_typed_ir.Item_t a_value s_value)
    let s_value := stack_prefix_preservation_witness_split_input p_value s_value
      in
    let s_value := Script_typed_ir.Item_t a_value s_value in
    let s_value :=
      stack_prefix_preservation_witness_split_output p_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IDug loc_value n_value p_value k_value; |})
  | (Script_typed_ir.IDipn loc_value n_value p_value k1 k2, s_value)
    return?
      (Ex_split_loop_may_not_fail
        {|
          ex_split_kinstr.Ex_split_loop_may_not_fail.body_init_stack :=
            stack_prefix_preservation_witness_split_input p_value s_value;
          ex_split_kinstr.Ex_split_loop_may_not_fail.body := k1;
          ex_split_kinstr.Ex_split_loop_may_not_fail.continuation := k2;
          ex_split_kinstr.Ex_split_loop_may_not_fail.aft_body_stack_transform :=
            fun (s_value : Script_typed_ir.stack_ty) ⇒
              return?
                (stack_prefix_preservation_witness_split_output p_value s_value);
          ex_split_kinstr.Ex_split_loop_may_not_fail.reconstruct :=
            fun (k1 : Script_typed_ir.kinstr) ⇒
              fun (k2 : Script_typed_ir.kinstr) ⇒
                Script_typed_ir.IDipn loc_value n_value p_value k1 k2; |})
  | (Script_typed_ir.IDropn loc_value n_value p_value k_value, s_value)
    let s_value := stack_prefix_preservation_witness_split_input p_value s_value
      in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IDropn loc_value n_value p_value k_value; |})
  | (Script_typed_ir.IChainId loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.chain_id_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IChainId loc_value k_value; |})
  | (Script_typed_ir.INever location, Script_typed_ir.Item_t arg_ty _)
    return?
      (Ex_split_failwith
        {| ex_split_kinstr.Ex_split_failwith.location := location;
          ex_split_kinstr.Ex_split_failwith.arg_ty := arg_ty;
          ex_split_kinstr.Ex_split_failwith.cast :=
            {| failed_kinstr_cast.cast := Script_typed_ir.INever location; |};
          |})
  |
    (Script_typed_ir.IVoting_power loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IVoting_power loc_value k_value; |})
  | (Script_typed_ir.ITotal_voting_power loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ITotal_voting_power loc_value k_value; |})
  | (Script_typed_ir.IKeccak loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IKeccak loc_value k_value; |})
  | (Script_typed_ir.ISha3 loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISha3 loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_bls12_381_g1 loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_bls12_381_g1 loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_bls12_381_g2 loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_bls12_381_g2 loc_value k_value; |})
  |
    (Script_typed_ir.IAdd_bls12_381_fr loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IAdd_bls12_381_fr loc_value k_value; |})
  |
    (Script_typed_ir.IMul_bls12_381_g1 loc_value k_value,
      Script_typed_ir.Item_t g1 (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t g1 s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_bls12_381_g1 loc_value k_value; |})
  |
    (Script_typed_ir.IMul_bls12_381_g2 loc_value k_value,
      Script_typed_ir.Item_t g2 (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t g2 s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_bls12_381_g2 loc_value k_value; |})
  |
    (Script_typed_ir.IMul_bls12_381_fr loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_bls12_381_fr loc_value k_value; |})
  |
    (Script_typed_ir.IMul_bls12_381_z_fr loc_value k_value,
      Script_typed_ir.Item_t fr (Script_typed_ir.Item_t _ s_value))
    let s_value := Script_typed_ir.Item_t fr s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_bls12_381_z_fr loc_value k_value; |})
  |
    (Script_typed_ir.IMul_bls12_381_fr_z loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMul_bls12_381_fr_z loc_value k_value; |})
  |
    (Script_typed_ir.IInt_bls12_381_fr loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.int_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IInt_bls12_381_fr loc_value k_value; |})
  | (Script_typed_ir.INeg_bls12_381_g1 loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INeg_bls12_381_g1 loc_value k_value; |})
  | (Script_typed_ir.INeg_bls12_381_g2 loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INeg_bls12_381_g2 loc_value k_value; |})
  | (Script_typed_ir.INeg_bls12_381_fr loc_value k_value, s_value)
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.INeg_bls12_381_fr loc_value k_value; |})
  |
    (Script_typed_ir.IPairing_check_bls12_381 loc_value k_value,
      Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IPairing_check_bls12_381 loc_value k_value; |})
  | (Script_typed_ir.IComb loc_value n_value p_value k_value, s_value)
    let fix aux
      (s_value : Script_typed_ir.stack_ty)
      (w_value : Script_typed_ir.comb_gadt_witness)
      : M? Script_typed_ir.stack_ty :=
      match (w_value, s_value) with
      | (Script_typed_ir.Comb_one, s_value)return? s_value
      |
        (Script_typed_ir.Comb_succ w_value,
          Script_typed_ir.Item_t a_value s_value)
        let? function_parameter := aux s_value w_value in
        match function_parameter with
        | Script_typed_ir.Item_t c_value t_value
          let? 'Script_typed_ir.Ty_ex_c p_value :=
            Script_typed_ir.pair_t dummy a_value c_value in
          return? (Script_typed_ir.Item_t p_value t_value)
        | _unreachable_gadt_branch
        end
      | _unreachable_gadt_branch
      end in
    let? s_value := aux s_value p_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IComb loc_value n_value p_value k_value; |})
  | (Script_typed_ir.IUncomb loc_value n_value p_value k_value, s_value)
    let fix aux
      (s_value : Script_typed_ir.stack_ty)
      (w_value : Script_typed_ir.uncomb_gadt_witness)
      : Script_typed_ir.stack_ty :=
      match (w_value, s_value) with
      | (Script_typed_ir.Uncomb_one, s_value)s_value
      |
        (Script_typed_ir.Uncomb_succ w_value,
          Script_typed_ir.Item_t
            (Script_typed_ir.Pair_t a_value b_value _meta _) s_value)
        let s_value := aux (Script_typed_ir.Item_t b_value s_value) w_value in
        Script_typed_ir.Item_t a_value s_value
      | _unreachable_gadt_branch
      end in
    let s_value := aux s_value p_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IUncomb loc_value n_value p_value k_value; |})
  |
    (Script_typed_ir.IComb_get loc_value n_value p_value k_value,
      Script_typed_ir.Item_t c_value s_value)
    let fix aux
      (c_value : Script_typed_ir.ty)
      (w_value : Script_typed_ir.comb_get_gadt_witness)
      : Script_typed_ir.ty_ex_c :=
      match (w_value, c_value) with
      | (Script_typed_ir.Comb_get_zero, c_value)
        Script_typed_ir.Ty_ex_c c_value
      | (Script_typed_ir.Comb_get_one, Script_typed_ir.Pair_t hd _tl _meta _)
        Script_typed_ir.Ty_ex_c hd
      |
        (Script_typed_ir.Comb_get_plus_two w_value,
          Script_typed_ir.Pair_t _hd tl _meta _)aux tl w_value
      | _unreachable_gadt_branch
      end in
    let s_value :=
      let 'Script_typed_ir.Ty_ex_c ty_value := aux c_value p_value in
      Script_typed_ir.Item_t ty_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IComb_get loc_value n_value p_value k_value; |})
  |
    (Script_typed_ir.IComb_set loc_value n_value p_value k_value,
      Script_typed_ir.Item_t a_value (Script_typed_ir.Item_t b_value s_value))
    ⇒
    let fix aux
      (a_value : Script_typed_ir.ty) (b_value : Script_typed_ir.ty)
      (w_value : Script_typed_ir.comb_set_gadt_witness)
      : M? Script_typed_ir.ty_ex_c :=
      match (w_value, b_value) with
      | (Script_typed_ir.Comb_set_zero, _)
        return? (Script_typed_ir.Ty_ex_c a_value)
      | (Script_typed_ir.Comb_set_one, Script_typed_ir.Pair_t _hd tl _meta _)
        Script_typed_ir.pair_t dummy a_value tl
      |
        (Script_typed_ir.Comb_set_plus_two w_value,
          Script_typed_ir.Pair_t hd tl _meta _)
        let? 'Script_typed_ir.Ty_ex_c c_value := aux a_value tl w_value in
        Script_typed_ir.pair_t dummy hd c_value
      | _unreachable_gadt_branch
      end in
    let? 'Script_typed_ir.Ty_ex_c c_value := aux a_value b_value p_value in
    let s_value := Script_typed_ir.Item_t c_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IComb_set loc_value n_value p_value k_value; |})
  | (Script_typed_ir.IDup_n loc_value n_value p_value k_value, s_value)
    let fix aux
      (s_value : Script_typed_ir.stack_ty)
      (w_value : Script_typed_ir.dup_n_gadt_witness)
      : Script_typed_ir.ty_ex_c :=
      match (w_value, s_value) with
      | (Script_typed_ir.Dup_n_succ w_value, Script_typed_ir.Item_t _ s_value)
        ⇒ aux s_value w_value
      | (Script_typed_ir.Dup_n_zero, Script_typed_ir.Item_t a_value _)
        Script_typed_ir.Ty_ex_c a_value
      | _unreachable_gadt_branch
      end in
    let s_value :=
      let 'Script_typed_ir.Ty_ex_c ty_value := aux s_value p_value in
      Script_typed_ir.Item_t ty_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IDup_n loc_value n_value p_value k_value; |})
  |
    (Script_typed_ir.ITicket loc_value cty k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let? some_cty := assert_some cty in
    let? t_value :=
      Error_monad.op_gtgtquestion (Script_typed_ir.ticket_t dummy some_cty)
        (Script_typed_ir.option_t loc_value) in
    let s_value := Script_typed_ir.Item_t t_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ITicket loc_value cty k_value; |})
  |
    (Script_typed_ir.ITicket_deprecated loc_value cty k_value,
      Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value))
    let? some_cty := assert_some cty in
    let? t_value := Script_typed_ir.ticket_t dummy some_cty in
    let s_value := Script_typed_ir.Item_t t_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ITicket_deprecated loc_value cty k_value; |})
  | (Script_typed_ir.IRead_ticket loc_value a_value k_value, s_value)
    let? asa := assert_some a_value in
    let? 'Script_typed_ir.Ty_ex_c p_value :=
      Script_typed_ir.pair_t dummy asa Script_typed_ir.nat_t in
    let? 'Script_typed_ir.Ty_ex_c t_value :=
      Script_typed_ir.pair_t dummy Script_typed_ir.address_t p_value in
    let s_value := Script_typed_ir.Item_t t_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IRead_ticket loc_value a_value k_value; |})
  |
    (Script_typed_ir.ISplit_ticket loc_value k_value,
      Script_typed_ir.Item_t t_value (Script_typed_ir.Item_t _ s_value))
    let? 'Script_typed_ir.Ty_ex_c p_value :=
      Script_typed_ir.pair_t dummy t_value t_value in
    let? o_value := Script_typed_ir.option_t dummy p_value in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ISplit_ticket loc_value k_value; |})
  |
    (Script_typed_ir.IJoin_tickets loc_value ty_value k_value,
      Script_typed_ir.Item_t (Script_typed_ir.Pair_t t_value _t _meta _) s_value)
    ⇒
    let? o_value := Script_typed_ir.option_t dummy t_value in
    let s_value := Script_typed_ir.Item_t o_value s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IJoin_tickets loc_value ty_value k_value; |})
  |
    (Script_typed_ir.IOpen_chest loc_value k_value,
      Script_typed_ir.Item_t _
        (Script_typed_ir.Item_t _ (Script_typed_ir.Item_t _ s_value)))
    let s_value :=
      Script_typed_ir.Item_t Script_typed_ir.union_bytes_bool_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IOpen_chest loc_value k_value; |})
  | (Script_typed_ir.IMin_block_time loc_value k_value, s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.nat_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IMin_block_time loc_value k_value; |})
  |
    (Script_typed_ir.IEmit {|
      Script_typed_ir.kinstr.IEmit.loc := loc_value;
        Script_typed_ir.kinstr.IEmit.tag := tag;
        Script_typed_ir.kinstr.IEmit.ty := ty_value;
        Script_typed_ir.kinstr.IEmit.unparsed_ty := unparsed_ty;
        Script_typed_ir.kinstr.IEmit.k := k_value
        |}, Script_typed_ir.Item_t _ s_value)
    let s_value := Script_typed_ir.Item_t Script_typed_ir.operation_t s_value in
    return?
      (Ex_split_kinstr
        {| ex_split_kinstr.Ex_split_kinstr.cont_init_stack := s_value;
          ex_split_kinstr.Ex_split_kinstr.continuation := k_value;
          ex_split_kinstr.Ex_split_kinstr.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.IEmit
                {| Script_typed_ir.kinstr.IEmit.loc := loc_value;
                  Script_typed_ir.kinstr.IEmit.tag := tag;
                  Script_typed_ir.kinstr.IEmit.ty := ty_value;
                  Script_typed_ir.kinstr.IEmit.unparsed_ty := unparsed_ty;
                  Script_typed_ir.kinstr.IEmit.k := k_value; |}; |})
  | (Script_typed_ir.IHalt loc_value, _s)return? (Ex_split_halt loc_value)
  |
    (Script_typed_ir.ILog loc_value _stack_ty event logger continuation,
      stack_value)
    return?
      (Ex_split_log
        {| ex_split_kinstr.Ex_split_log.stack := stack_value;
          ex_split_kinstr.Ex_split_log.continuation := continuation;
          ex_split_kinstr.Ex_split_log.reconstruct :=
            fun (k_value : Script_typed_ir.kinstr) ⇒
              Script_typed_ir.ILog loc_value s_value event logger k_value; |})
  | _unreachable_gadt_branch
  end.

#[bypass_check(guard)]
Fixpoint kinstr_final_stack_type
  (s_value : Script_typed_ir.stack_ty) (i_value : Script_typed_ir.kinstr)
  {struct i_value} : M? (option Script_typed_ir.stack_ty) :=
  let? function_parameter := kinstr_split s_value i_value in
  match function_parameter with
  |
    Ex_split_kinstr {|
      ex_split_kinstr.Ex_split_kinstr.cont_init_stack := cont_init_stack;
        ex_split_kinstr.Ex_split_kinstr.continuation := continuation
        |} ⇒ kinstr_final_stack_type cont_init_stack continuation
  |
    Ex_split_log {|
      ex_split_kinstr.Ex_split_log.stack := stack_value;
        ex_split_kinstr.Ex_split_log.continuation := continuation
        |} ⇒ kinstr_final_stack_type stack_value continuation
  |
    Ex_split_loop_may_fail {|
      ex_split_kinstr.Ex_split_loop_may_fail.cont_init_stack := cont_init_stack;
        ex_split_kinstr.Ex_split_loop_may_fail.continuation := continuation
        |} ⇒ kinstr_final_stack_type cont_init_stack continuation
  |
    Ex_split_loop_may_not_fail {|
      ex_split_kinstr.Ex_split_loop_may_not_fail.body_init_stack := body_init_stack;
        ex_split_kinstr.Ex_split_loop_may_not_fail.body := body;
        ex_split_kinstr.Ex_split_loop_may_not_fail.continuation := continuation;
        ex_split_kinstr.Ex_split_loop_may_not_fail.aft_body_stack_transform :=
          aft_body_stack_transform
        |} ⇒
    let? function_parameter := kinstr_final_stack_type body_init_stack body in
    match function_parameter with
    | Some after_body
      let? before_k := aft_body_stack_transform after_body in
      kinstr_final_stack_type before_k continuation
    | Nonereturn? None
    end
  |
    Ex_split_if {|
      ex_split_kinstr.Ex_split_if.left_init_stack := left_init_stack;
        ex_split_kinstr.Ex_split_if.left_branch := left_branch;
        ex_split_kinstr.Ex_split_if.right_init_stack := right_init_stack;
        ex_split_kinstr.Ex_split_if.right_branch := right_branch;
        ex_split_kinstr.Ex_split_if.continuation := continuation
        |} ⇒
    let? function_parameter :=
      kinstr_final_stack_type left_init_stack left_branch