Skip to main content

🍬 Script_interpreter.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  let trace_encoding :=
    (let arg := Data_encoding.list_value in
    fun (eta :
      Data_encoding.encoding
        (Alpha_context.Script.location × Alpha_context.Gas.t ×
          list Alpha_context.Script.expr)) ⇒ arg None eta)
      (Data_encoding.obj3
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "gas" Alpha_context.Gas.encoding)
        (Data_encoding.req None None "stack"
          (Data_encoding.list_value None Alpha_context.Script.expr_encoding)))
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "michelson_v1.script_rejected" "Script failed"
      "A FAILWITH instruction was reached" None
      (Data_encoding.obj3
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.req None None "with" Alpha_context.Script.expr_encoding)
        (Data_encoding.opt None None "trace" trace_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Reject" then
            let '(loc_value, v_value, trace_value) :=
              cast
                (Alpha_context.Script.location × Alpha_context.Script.expr ×
                  option Script_typed_ir.execution_trace) payload in
            Some (loc_value, v_value, trace_value)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × Alpha_context.Script.expr ×
          option Script_typed_ir.execution_trace) ⇒
        let '(loc_value, v_value, trace_value) := function_parameter in
        Build_extensible "Reject"
          (Alpha_context.Script.location × Alpha_context.Script.expr ×
            option Script_typed_ir.execution_trace)
          (loc_value, v_value, trace_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "michelson_v1.script_overflow" "Script failed (overflow error)"
      "A FAIL instruction was reached due to the detection of an overflow" None
      (Data_encoding.obj2
        (Data_encoding.req None None "location"
          Alpha_context.Script.location_encoding)
        (Data_encoding.opt None None "trace" trace_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Overflow" then
            let '(loc_value, trace_value) :=
              cast
                (Alpha_context.Script.location ×
                  option Script_typed_ir.execution_trace) payload in
            Some (loc_value, trace_value)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Script.location × option Script_typed_ir.execution_trace)
        ⇒
        let '(loc_value, trace_value) := function_parameter in
        Build_extensible "Overflow"
          (Alpha_context.Script.location ×
            option Script_typed_ir.execution_trace) (loc_value, trace_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "michelson_v1.runtime_error" "Script runtime error"
      "Toplevel error for all runtime script errors" None
      (Data_encoding.obj2
        (Data_encoding.req None None "contract_handle"
          Alpha_context.Contract.encoding)
        (Data_encoding.req None None "contract_code"
          (Data_encoding.constant "Deprecated")))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Runtime_contract_error" then
            let contract := cast Alpha_context.Contract.t payload in
            Some (contract, tt)
          else None
        end)
      (fun (function_parameter : Alpha_context.Contract.t × unit) ⇒
        let '(contract, _) := function_parameter in
        Build_extensible "Runtime_contract_error" Alpha_context.Contract.t
          contract) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.bad_contract_parameter"
      "Contract supplied an invalid parameter"
      "Either no parameter was supplied to a contract with a non-unit parameter type, a non-unit parameter was passed to an account, or a parameter was supplied of the wrong type"
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "contract" Alpha_context.Contract.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Bad_contract_parameter" then
            let c_value := cast Alpha_context.Contract.t payload in
            Some c_value
          else None
        end)
      (fun (c_value : Alpha_context.Contract.t) ⇒
        Build_extensible "Bad_contract_parameter" Alpha_context.Contract.t
          c_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "michelson_v1.cannot_serialize_failure"
      "Not enough gas to serialize argument of FAILWITH"
      "Argument of FAILWITH was too big to be serialized with the provided gas"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Cannot_serialize_failure" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Cannot_serialize_failure" unit tt) in
  Error_monad.register_error_kind Error_monad.Temporary
    "michelson_v1.cannot_serialize_storage"
    "Not enough gas to serialize execution storage"
    "The returned storage was too big to be serialized with the provided gas"
    None Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Cannot_serialize_storage" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Cannot_serialize_storage" unit tt).

Definition ifailwith : Script_interpreter_defs.ifailwith_type :=
  {|
    Script_interpreter_defs.ifailwith_type.ifailwith A B :=
      fun (logger : option Script_typed_ir.logger) ⇒
        fun (function_parameter :
          Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
          ⇒
          let '(ctxt, _) := function_parameter in
          fun (gas : Local_gas_counter.local_gas_counter) ⇒
            fun (kloc : Alpha_context.Script.location) ⇒
              fun (tv : Script_typed_ir.ty) ⇒
                fun (accu_value : A) ⇒
                  let ctxt := Local_gas_counter.update_context gas ctxt in
                  let? '(v_value, _ctxt) :=
                    Error_monad.trace_value
                      (Build_extensible "Cannot_serialize_failure" unit tt)
                      (Script_ir_translator.unparse_data ctxt
                        Script_ir_translator.Optimized tv accu_value) in
                  let v_value := Micheline.strip_locations v_value in
                  let? log := Script_interpreter_defs.get_log logger in
                  Error_monad.fail
                    (Build_extensible "Reject"
                      (Alpha_context.Script.location ×
                        Micheline.canonical Alpha_context.Script.prim ×
                        option Script_typed_ir.execution_trace)
                      (kloc, v_value, log)); |}.

Axiom log : {a s r f : Set},
  Script_typed_ir.logger × Script_typed_ir.logging_event
  Script_interpreter_defs.step_type a s r f.

Axiom klog : {a s r f : Set},
  Script_typed_ir.logger
  Local_gas_counter.outdated_context × step_constants
  Local_gas_counter.local_gas_counter Script_typed_ir.continuation
  Script_typed_ir.continuation a s
  M?
    (r × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter).

Reserved Notation "'kmap_exit".
Reserved Notation "'kmap_enter".
Reserved Notation "'klist_exit".
Reserved Notation "'klist_enter".
Reserved Notation "'kloop_in_left".
Reserved Notation "'kloop_in".
Reserved Notation "'kiter".
Reserved Notation "'ilist_map".
Reserved Notation "'ilist_iter".
Reserved Notation "'iset_iter".
Reserved Notation "'imap_map".
Reserved Notation "'imap_iter".
Reserved Notation "'imul_teznat".
Reserved Notation "'imul_nattez".
Reserved Notation "'ilsl_nat".
Reserved Notation "'ilsr_nat".
Reserved Notation "'iexec".

#[bypass_check(guard)]
Fixpoint {a s r f : Set}
  (g_value : Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
  (gas : Local_gas_counter.local_gas_counter)
  (ks0 : Script_typed_ir.continuation) (accu_value : a) (stack_value : s)
  {struct gas}
  : M?
    (r × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter) :=
  let kmap_exit {m n o a b g h} := 'kmap_exit m n o a b g h in
  let kmap_enter {j k a b c d e} := 'kmap_enter j k a b c d e in
  let klist_exit {i j a b c d} := 'klist_exit i j a b c d in
  let klist_enter {j b a c d e} := 'klist_enter j b a c d e in
  let kloop_in_left {a b g e f} := 'kloop_in_left a b g e f in
  let kloop_in {a s r f} := 'kloop_in a s r f in
  let kiter {b a s r f} := 'kiter b a s r f in
  let '(ctxt, _) := g_value in
  match Script_interpreter_defs.consume_control gas ks0 with
  | None
    Error_monad.fail (Build_extensible "Operation_quota_exceeded" unit tt)
  | Some gas
    match (ks0, accu_value, stack_value) with
    | (Script_typed_ir.KLog ks logger, _, _)
      let '[logger, ks] :=
        cast [Script_typed_ir.logger ** Script_typed_ir.continuation]
          [logger, ks] in
      klog logger g_value gas ks0 ks accu_value stack_value
    | (Script_typed_ir.KNil, accu_value, stack_value)
      let '[stack_value, accu_value] := cast [f ** r] [stack_value, accu_value]
        in
      Pervasives.Ok (accu_value, stack_value, ctxt, gas)
    | (Script_typed_ir.KCons k_value ks, _, _)
      let '[ks, k_value] :=
        cast [Script_typed_ir.continuation ** Script_typed_ir.kinstr]
          [ks, k_value] in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.KLoop_in ki ks', accu_value, stack_value)
      let 'existT _ [__0, __1] [stack_value, accu_value, ks', ki] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__0, __1]
            [__0 × __1 ** bool ** Script_typed_ir.continuation **
              Script_typed_ir.kinstr]) [stack_value, accu_value, ks', ki] in
      kloop_in g_value gas ks0 ki ks' accu_value stack_value
    | (Script_typed_ir.KReturn stack' ks, _, _)
      let 'existT _ __KReturn_'s [ks, stack'] :=
        cast_exists (Es := Set)
          (fun __KReturn_'s[Script_typed_ir.continuation ** __KReturn_'s])
          [ks, stack'] in
      next g_value gas ks accu_value stack'
    | (Script_typed_ir.KMap_head f_value ks, _, _)
      let 'existT _ __KMap_head_'b [ks, f_value] :=
        cast_exists (Es := Set)
          (fun __KMap_head_'b
            [Script_typed_ir.continuation ** a __KMap_head_'b]) [ks, f_value]
        in
      next g_value gas ks (f_value accu_value) stack_value
    | (Script_typed_ir.KLoop_in_left ki ks', accu_value, _)
      let 'existT _ [__2, __3] [accu_value, ks', ki] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__2, __3]
            [Script_typed_ir.union __2 __3 ** Script_typed_ir.continuation **
              Script_typed_ir.kinstr]) [accu_value, ks', ki] in
      kloop_in_left g_value gas ks0 ki ks' accu_value stack_value
    | (Script_typed_ir.KUndip x_value ks, _, _)
      let 'existT _ __KUndip_'b [ks, x_value] :=
        cast_exists (Es := Set)
          (fun __KUndip_'b[Script_typed_ir.continuation ** __KUndip_'b])
          [ks, x_value] in
      next g_value gas ks x_value (accu_value, stack_value)
    | (Script_typed_ir.KIter body xs ks, _, _)
      let 'existT _ __KIter_'a [ks, xs, body] :=
        cast_exists (Es := Set)
          (fun __KIter_'a
            [Script_typed_ir.continuation ** list __KIter_'a **
              Script_typed_ir.kinstr]) [ks, xs, body] in
      let extra := (body, xs) in
      kiter Script_interpreter_defs.id g_value gas extra ks accu_value
        stack_value
    | (Script_typed_ir.KList_enter_body body xs ys len ks, _, _)
      let 'existT _ [__KList_enter_body_'b, __KList_enter_body_'a]
        [ks, len, ys, xs, body] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__KList_enter_body_'b, __KList_enter_body_'a]
            [Script_typed_ir.continuation ** int ** list __KList_enter_body_'b
              ** list __KList_enter_body_'a ** Script_typed_ir.kinstr])
          [ks, len, ys, xs, body] in
      let extra := (body, xs, ys, len) in
      klist_enter Script_interpreter_defs.id g_value gas extra ks accu_value
        stack_value
    | (Script_typed_ir.KList_exit_body body xs ys len ks, _, stack_value)
      let 'existT _ [__4, __5, __KList_exit_body_'a]
        [stack_value, ks, len, ys, xs, body] :=
        cast_exists (Es := [Set ** Set ** Set])
          (fun '[__4, __5, __KList_exit_body_'a]
            [__4 × __5 ** Script_typed_ir.continuation ** int ** list a **
              list __KList_exit_body_'a ** Script_typed_ir.kinstr])
          [stack_value, ks, len, ys, xs, body] in
      let extra := (body, xs, ys, len) in
      klist_exit Script_interpreter_defs.id g_value gas extra ks accu_value
        stack_value
    | (Script_typed_ir.KMap_enter_body body xs ys ks, _, _)
      let 'existT _
        [__KMap_enter_body_'a, __KMap_enter_body_'c, __KMap_enter_body_'b]
        [ks, ys, xs, body] :=
        cast_exists (Es := [Set ** Set ** Set])
          (fun
            '[__KMap_enter_body_'a, __KMap_enter_body_'c, __KMap_enter_body_'b]
            ⇒
            [Script_typed_ir.continuation **
              Script_typed_ir.map __KMap_enter_body_'a __KMap_enter_body_'c **
              list (__KMap_enter_body_'a × __KMap_enter_body_'b) **
              Script_typed_ir.kinstr]) [ks, ys, xs, body] in
      let extra := (body, xs, ys) in
      kmap_enter Script_interpreter_defs.id g_value gas extra ks accu_value
        stack_value
    | (Script_typed_ir.KMap_exit_body body xs ys yk ks, _, stack_value)
      let 'existT _ [__6, __7, __KMap_exit_body_'a, __KMap_exit_body_'b]
        [stack_value, ks, yk, ys, xs, body] :=
        cast_exists (Es := [Set ** Set ** Set ** Set])
          (fun '[__6, __7, __KMap_exit_body_'a, __KMap_exit_body_'b]
            [__6 × __7 ** Script_typed_ir.continuation ** __KMap_exit_body_'a **
              Script_typed_ir.map __KMap_exit_body_'a a **
              list (__KMap_exit_body_'a × __KMap_exit_body_'b) **
              Script_typed_ir.kinstr]) [stack_value, ks, yk, ys, xs, body] in
      let extra := (body, xs, ys, yk) in
      kmap_exit Script_interpreter_defs.id g_value gas extra ks accu_value
        stack_value
    | (Script_typed_ir.KView_exit orig_step_constants ks, _, _)
      let '[ks, orig_step_constants] :=
        cast [Script_typed_ir.continuation ** Script_typed_ir.step_constants]
          [ks, orig_step_constants] in
      let g_value := ((Pervasives.fst g_value), orig_step_constants) in
      next g_value gas ks accu_value stack_value
    end
  end

with step {a s r f : Set}
  (g_value : Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
  (gas : Local_gas_counter.local_gas_counter) (i_value : Script_typed_ir.kinstr)
  (ks : Script_typed_ir.continuation) (accu_value : a) (stack_value : s)
  {struct gas}
  : M?
    (r × f × Local_gas_counter.outdated_context ×
      Local_gas_counter.local_gas_counter) :=
  let ilist_map {e a b c d f} := 'ilist_map e a b c d f in
  let ilist_iter {e a b c d} := 'ilist_iter e a b c d in
  let iset_iter {e a b c d} := 'iset_iter e a b c d in
  let imap_map {e f a b c d g} := 'imap_map e f a b c d g in
  let imap_iter {e f a b c d} := 'imap_iter e f a b c d in
  let imul_teznat {b e f} := 'imul_teznat b e f in
  let imul_nattez {b e f} := 'imul_nattez b e f in
  let ilsl_nat {b e f} := 'ilsl_nat b e f in
  let ilsr_nat {b e f} := 'ilsr_nat b e f in
  let iexec {g b e f} := 'iexec g b e f in
  let '(ctxt, sc) := g_value in
  match Script_interpreter_defs.consume_instr gas i_value accu_value stack_value
    with
  | None
    Error_monad.fail (Build_extensible "Operation_quota_exceeded" unit tt)
  | Some gas
    match (i_value, accu_value, stack_value) with
    | (Script_typed_ir.ILog _ event logger k_value, _, _)
      let '[k_value, logger, event] :=
        cast
          [Script_typed_ir.kinstr ** Script_typed_ir.logger **
            Script_typed_ir.logging_event] [k_value, logger, event] in
      log (logger, event) g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IHalt _, _, _)
      next g_value gas ks accu_value stack_value
    | (Script_typed_ir.IDrop _ k_value, _, stack_value)
      let 'existT _ [__22, __23] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__22, __23][__22 × __23 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(accu_value, stack_value) := stack_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IDup _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      step g_value gas k_value ks accu_value (accu_value, stack_value)
    | (Script_typed_ir.ISwap _ k_value, _, stack_value)
      let 'existT _ [__24, __25] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__24, __25][__24 × __25 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(top, stack_value) := stack_value in
      step g_value gas k_value ks top (accu_value, stack_value)
    | (Script_typed_ir.IConst _ v_value k_value, _, _)
      let 'existT _ __IConst_'ty [k_value, v_value] :=
        cast_exists (Es := Set)
          (fun __IConst_'ty[Script_typed_ir.kinstr ** __IConst_'ty])
          [k_value, v_value] in
      step g_value gas k_value ks v_value (accu_value, stack_value)
    | (Script_typed_ir.ICons_some _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      step g_value gas k_value ks (Some accu_value) stack_value
    | (Script_typed_ir.ICons_none _ k_value, _, _)
      let 'existT _ __ICons_none_'b k_value :=
        cast_exists (Es := Set) (fun __ICons_none_'bScript_typed_ir.kinstr)
          k_value in
      step g_value gas k_value ks (None : option __ICons_none_'b)
        (accu_value, stack_value)
    |
      (Script_typed_ir.IIf_none {|
        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
          |}, accu_value, stack_value)
      let 'existT _ [__27, __28, __26]
        [stack_value, accu_value, k_value, branch_if_some, branch_if_none] :=
        cast_exists (Es := [Set ** Set ** Set])
          (fun '[__27, __28, __26]
            [__27 × __28 ** option __26 ** Script_typed_ir.kinstr **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, branch_if_some, branch_if_none] in
      match accu_value with
      | None
        let '(accu_value, stack_value) := stack_value in
        step g_value gas branch_if_none (Script_typed_ir.KCons k_value ks)
          accu_value stack_value
      | Some v_value
        step g_value gas branch_if_some (Script_typed_ir.KCons k_value ks)
          v_value stack_value
      end
    |
      (Script_typed_ir.IOpt_map {|
        Script_typed_ir.kinstr.IOpt_map.kinfo := _;
          Script_typed_ir.kinstr.IOpt_map.body := body;
          Script_typed_ir.kinstr.IOpt_map.k := k_value
          |}, accu_value, _)
      let 'existT _ [__29, __IOpt_map_'b] [accu_value, k_value, body] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__29, __IOpt_map_'b]
            [option __29 ** Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [accu_value, k_value, body] in
      match accu_value with
      | None
        step g_value gas k_value ks (None : option __IOpt_map_'b) stack_value
      | Some v_value
        let ks' :=
          Script_typed_ir.KMap_head
            (Option.some : __IOpt_map_'b option __IOpt_map_'b)
            (Script_typed_ir.KCons k_value ks) in
        step g_value gas body ks' v_value stack_value
      end
    | (Script_typed_ir.ICons_pair _ k_value, _, stack_value)
      let 'existT _ [__30, __31] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__30, __31][__30 × __31 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(b_value, stack_value) := stack_value in
      step g_value gas k_value ks (accu_value, b_value) stack_value
    | (Script_typed_ir.IUnpair _ k_value, accu_value, _)
      let 'existT _ [__32, __33] [accu_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__32, __33][__32 × __33 ** Script_typed_ir.kinstr])
          [accu_value, k_value] in
      let '(a_value, b_value) := accu_value in
      step g_value gas k_value ks a_value (b_value, stack_value)
    | (Script_typed_ir.ICar _ k_value, accu_value, _)
      let 'existT _ [__34, __35] [accu_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__34, __35][__34 × __35 ** Script_typed_ir.kinstr])
          [accu_value, k_value] in
      let '(a_value, _) := accu_value in
      step g_value gas k_value ks a_value stack_value
    | (Script_typed_ir.ICdr _ k_value, accu_value, _)
      let 'existT _ [__36, __37] [accu_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__36, __37][__36 × __37 ** Script_typed_ir.kinstr])
          [accu_value, k_value] in
      let '(_, b_value) := accu_value in
      step g_value gas k_value ks b_value stack_value
    | (Script_typed_ir.ICons_left _ k_value, _, _)
      let 'existT _ __ICons_left_'b k_value :=
        cast_exists (Es := Set) (fun __ICons_left_'bScript_typed_ir.kinstr)
          k_value in
      step g_value gas k_value ks
        ((Script_typed_ir.L accu_value) :
          Script_typed_ir.union a __ICons_left_'b) stack_value
    | (Script_typed_ir.ICons_right _ k_value, _, _)
      let 'existT _ __ICons_right_'a k_value :=
        cast_exists (Es := Set) (fun __ICons_right_'aScript_typed_ir.kinstr)
          k_value in
      step g_value gas k_value ks
        ((Script_typed_ir.R accu_value) :
          Script_typed_ir.union __ICons_right_'a a) stack_value
    |
      (Script_typed_ir.IIf_left {|
        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
          |}, accu_value, _)
      let 'existT _ [__38, __39]
        [accu_value, k_value, branch_if_right, branch_if_left] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__38, __39]
            [Script_typed_ir.union __38 __39 ** Script_typed_ir.kinstr **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [accu_value, k_value, branch_if_right, branch_if_left] in
      match accu_value with
      | Script_typed_ir.L v_value
        step g_value gas branch_if_left (Script_typed_ir.KCons k_value ks)
          v_value stack_value
      | Script_typed_ir.R v_value
        step g_value gas branch_if_right (Script_typed_ir.KCons k_value ks)
          v_value stack_value
      end
    | (Script_typed_ir.ICons_list _ k_value, _, stack_value)
      let 'existT _ __40 [stack_value, k_value] :=
        cast_exists (Es := Set)
          (fun __40
            [Script_typed_ir.boxed_list a × __40 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(tl, stack_value) := stack_value in
      let accu_value := Script_list.cons_value accu_value tl in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.INil _ k_value, _, _)
      let 'existT _ __INil_'b k_value :=
        cast_exists (Es := Set) (fun __INil_'bScript_typed_ir.kinstr)
          k_value in
      let stack_value := (accu_value, stack_value) in
      let accu_value {E : Set} : Script_typed_ir.boxed_list E :=
        Script_list.empty in
      step g_value gas k_value ks (accu_value (E := __INil_'b)) stack_value
    |
      (Script_typed_ir.IIf_cons {|
        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
          |}, accu_value, stack_value)
      let 'existT _ [__42, __43, __41]
        [stack_value, accu_value, k_value, branch_if_nil, branch_if_cons] :=
        cast_exists (Es := [Set ** Set ** Set])
          (fun '[__42, __43, __41]
            [__42 × __43 ** Script_typed_ir.boxed_list __41 **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr **
              Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, branch_if_nil, branch_if_cons] in
      match accu_value.(Script_typed_ir.boxed_list.elements) with
      | []
        let '(accu_value, stack_value) := stack_value in
        step g_value gas branch_if_nil (Script_typed_ir.KCons k_value ks)
          accu_value stack_value
      | cons hd tl
        let tl :=
          {| Script_typed_ir.boxed_list.elements := tl;
            Script_typed_ir.boxed_list.length :=
              accu_value.(Script_typed_ir.boxed_list.length) -i 1; |} in
        step g_value gas branch_if_cons (Script_typed_ir.KCons k_value ks) hd
          (tl, stack_value)
      end
    | (Script_typed_ir.IList_map _ body k_value, accu_value, stack_value)
      let 'existT _ [__45, __46, __44, __IList_map_'b]
        [stack_value, accu_value, k_value, body] :=
        cast_exists (Es := [Set ** Set ** Set ** Set])
          (fun '[__45, __46, __44, __IList_map_'b]
            [__45 × __46 ** Script_typed_ir.boxed_list __44 **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, body] in
      (ilist_map (f := __IList_map_'b)) Script_interpreter_defs.id g_value gas
        (body, k_value) ks accu_value stack_value
    | (Script_typed_ir.IList_size _ k_value, accu_value, _)
      let 'existT _ __47 [accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __47
            [Script_typed_ir.boxed_list __47 ** Script_typed_ir.kinstr])
          [accu_value, k_value] in
      let list_value := accu_value in
      let len :=
        Alpha_context.Script_int.abs
          (Alpha_context.Script_int.of_int
            list_value.(Script_typed_ir.boxed_list.length)) in
      step g_value gas k_value ks len stack_value
    | (Script_typed_ir.IList_iter _ body k_value, accu_value, stack_value)
      let 'existT _ [__49, __50, __48] [stack_value, accu_value, k_value, body]
        :=
        cast_exists (Es := [Set ** Set ** Set])
          (fun '[__49, __50, __48]
            [__49 × __50 ** Script_typed_ir.boxed_list __48 **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, body] in
      ilist_iter Script_interpreter_defs.id g_value gas (body, k_value) ks
        accu_value stack_value
    | (Script_typed_ir.IEmpty_set _ ty k_value, _, _)
      let 'existT _ __IEmpty_set_'b [k_value, ty] :=
        cast_exists (Es := Set)
          (fun __IEmpty_set_'b
            [Script_typed_ir.kinstr ** Script_typed_ir.comparable_ty])
          [k_value, ty] in
      let res :=
        (Script_set.empty :
          Script_typed_ir.comparable_ty Script_typed_ir.set __IEmpty_set_'b)
          ty in
      let stack_value := (accu_value, stack_value) in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.ISet_iter _ body k_value, accu_value, stack_value)
      let 'existT _ [__52, __53, __51] [stack_value, accu_value, k_value, body]
        :=
        cast_exists (Es := [Set ** Set ** Set])
          (fun '[__52, __53, __51]
            [__52 × __53 ** Script_typed_ir.set __51 ** Script_typed_ir.kinstr
              ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, body] in
      iset_iter Script_interpreter_defs.id g_value gas (body, k_value) ks
        accu_value stack_value
    | (Script_typed_ir.ISet_mem _ k_value, _, stack_value)
      let 'existT _ __54 [stack_value, k_value] :=
        cast_exists (Es := Set)
          (fun __54[Script_typed_ir.set a × __54 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(set, stack_value) := stack_value in
      let res := Script_set.mem accu_value set in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.ISet_update _ k_value, _, stack_value)
      let 'existT _ __55 [stack_value, k_value] :=
        cast_exists (Es := Set)
          (fun __55
            [bool × (Script_typed_ir.set a × __55) ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(presence, (set, stack_value)) := stack_value in
      let res := Script_set.update accu_value presence set in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.ISet_size _ k_value, accu_value, _)
      let 'existT _ __56 [accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __56[Script_typed_ir.set __56 ** Script_typed_ir.kinstr])
          [accu_value, k_value] in
      let res := Script_set.size_value accu_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IEmpty_map _ ty k_value, _, _)
      let 'existT _ [__IEmpty_map_'b, __IEmpty_map_'c] [k_value, ty] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__IEmpty_map_'b, __IEmpty_map_'c]
            [Script_typed_ir.kinstr ** Script_typed_ir.comparable_ty])
          [k_value, ty] in
      let stack_value := (accu_value, stack_value) in
      let res :=
        (Script_map.empty :
          Script_typed_ir.comparable_ty
          Script_typed_ir.map __IEmpty_map_'b __IEmpty_map_'c) ty in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMap_map _ body k_value, accu_value, stack_value)
      let 'existT _ [__59, __60, __57, __58, __IMap_map_'c]
        [stack_value, accu_value, k_value, body] :=
        cast_exists (Es := [Set ** Set ** Set ** Set ** Set])
          (fun '[__59, __60, __57, __58, __IMap_map_'c]
            [__59 × __60 ** Script_typed_ir.map __57 __58 **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, body] in
      (imap_map (g := __IMap_map_'c)) Script_interpreter_defs.id g_value gas
        (body, k_value) ks accu_value stack_value
    | (Script_typed_ir.IMap_iter _ body k_value, accu_value, stack_value)
      let 'existT _ [__63, __64, __61, __62]
        [stack_value, accu_value, k_value, body] :=
        cast_exists (Es := [Set ** Set ** Set ** Set])
          (fun '[__63, __64, __61, __62]
            [__63 × __64 ** Script_typed_ir.map __61 __62 **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, body] in
      imap_iter Script_interpreter_defs.id g_value gas (body, k_value) ks
        accu_value stack_value
    | (Script_typed_ir.IMap_mem _ k_value, _, stack_value)
      let 'existT _ [__65, __66] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__65, __66]
            [Script_typed_ir.map a __65 × __66 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(map, stack_value) := stack_value in
      let res := Script_map.mem accu_value map in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMap_get _ k_value, _, stack_value)
      let 'existT _ [__67, __68] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__67, __68]
            [Script_typed_ir.map a __67 × __68 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(map, stack_value) := stack_value in
      let res := Script_map.get accu_value map in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMap_update _ k_value, _, stack_value)
      let 'existT _ [__69, __70] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__69, __70]
            [option __69 × (Script_typed_ir.map a __69 × __70) **
              Script_typed_ir.kinstr]) [stack_value, k_value] in
      let '(v_value, (map, stack_value)) := stack_value in
      let key_value := accu_value in
      let res := Script_map.update key_value v_value map in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMap_get_and_update _ k_value, _, stack_value)
      let 'existT _ [__71, __72] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__71, __72]
            [option __71 × (Script_typed_ir.map a __71 × __72) **
              Script_typed_ir.kinstr]) [stack_value, k_value] in
      let key_value := accu_value in
      let '(v_value, (map, rest)) := stack_value in
      let map' := Script_map.update key_value v_value map in
      let v' := Script_map.get key_value map in
      step g_value gas k_value ks v' (map', rest)
    | (Script_typed_ir.IMap_size _ k_value, accu_value, _)
      let 'existT _ [__73, __74] [accu_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__73, __74]
            [Script_typed_ir.map __73 __74 ** Script_typed_ir.kinstr])
          [accu_value, k_value] in
      let res := Script_map.size_value accu_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IEmpty_big_map _ tk tv k_value, _, _)
      let 'existT _ [__IEmpty_big_map_'b, __IEmpty_big_map_'c] [k_value, tv, tk]
        :=
        cast_exists (Es := [Set ** Set])
          (fun '[__IEmpty_big_map_'b, __IEmpty_big_map_'c]
            [Script_typed_ir.kinstr ** Script_typed_ir.ty **
              Script_typed_ir.comparable_ty]) [k_value, tv, tk] in
      let ebm :=
        (Script_ir_translator.empty_big_map (a := __IEmpty_big_map_'b)
          (b := __IEmpty_big_map_'c)) tk tv in
      step g_value gas k_value ks ebm (accu_value, stack_value)
    | (Script_typed_ir.IBig_map_mem _ k_value, _, stack_value)
      let 'existT _ __76 [stack_value, k_value] :=
        cast_exists (Es := Set)
          (fun __76
            [Script_typed_ir.big_map × __76 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(map, stack_value) := stack_value in
      let key_value := accu_value in
      let? '(res, ctxt, gas) :=
        Local_gas_counter.use_gas_counter_in_context ctxt gas
          (fun (ctxt : Alpha_context.context) ⇒
            Script_ir_translator.big_map_mem ctxt key_value map) in
      step (ctxt, sc) gas k_value ks res stack_value
    | (Script_typed_ir.IBig_map_get _ k_value, _, stack_value)
      let 'existT _ [__77, __78] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__77, __78]
            [Script_typed_ir.big_map × __78 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      let '(map, stack_value) := stack_value in
      let key_value := accu_value in
      let? '(res, ctxt, gas) :=
        Local_gas_counter.use_gas_counter_in_context ctxt gas
          (fun (ctxt : Alpha_context.context) ⇒
            Script_ir_translator.big_map_get ctxt key_value map) in
      step (ctxt, sc) gas k_value ks (res : option __77) stack_value
    | (Script_typed_ir.IBig_map_update _ k_value, _, stack_value)
      let 'existT _ [__79, __80] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__79, __80]
            [option __79 × (Script_typed_ir.big_map × __80) **
              Script_typed_ir.kinstr]) [stack_value, k_value] in
      let key_value := accu_value in
      let '(maybe_value, (map, stack_value)) := stack_value in
      let? '(big_map, ctxt, gas) :=
        Local_gas_counter.use_gas_counter_in_context ctxt gas
          (fun (ctxt : Alpha_context.context) ⇒
            Script_ir_translator.big_map_update ctxt key_value maybe_value map)
        in
      step (ctxt, sc) gas k_value ks big_map stack_value
    | (Script_typed_ir.IBig_map_get_and_update _ k_value, _, stack_value)
      let 'existT _ [__81, __82] [stack_value, k_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__81, __82]
            [option __81 × (Script_typed_ir.big_map × __82) **
              Script_typed_ir.kinstr]) [stack_value, k_value] in
      let key_value := accu_value in
      let '(v_value, (map, stack_value)) := stack_value in
      let? '((v', map'), ctxt, gas) :=
        Local_gas_counter.use_gas_counter_in_context ctxt gas
          (fun (ctxt : Alpha_context.context) ⇒
            Script_ir_translator.big_map_get_and_update ctxt key_value v_value
              map) in
      step (ctxt, sc) gas k_value ks v' (map', stack_value)
    |
      (Script_typed_ir.IAdd_seconds_to_timestamp _ k_value, accu_value,
        stack_value)
      let 'existT _ __83 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __83
            [Alpha_context.Script_timestamp.t × __83 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let n_value := accu_value in
      let '(t_value, stack_value) := stack_value in
      let result_value :=
        Alpha_context.Script_timestamp.add_delta t_value n_value in
      step g_value gas k_value ks result_value stack_value
    |
      (Script_typed_ir.IAdd_timestamp_to_seconds _ k_value, accu_value,
        stack_value)
      let 'existT _ __84 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __84
            [Alpha_context.Script_int.num × __84 **
              Alpha_context.Script_timestamp.t ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let t_value := accu_value in
      let '(n_value, stack_value) := stack_value in
      let result_value :=
        Alpha_context.Script_timestamp.add_delta t_value n_value in
      step g_value gas k_value ks result_value stack_value
    |
      (Script_typed_ir.ISub_timestamp_seconds _ k_value, accu_value, stack_value)
      ⇒
      let 'existT _ __85 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __85
            [Alpha_context.Script_int.num × __85 **
              Alpha_context.Script_timestamp.t ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let t_value := accu_value in
      let '(s_value, stack_value) := stack_value in
      let result_value :=
        Alpha_context.Script_timestamp.sub_delta t_value s_value in
      step g_value gas k_value ks result_value stack_value
    | (Script_typed_ir.IDiff_timestamps _ k_value, accu_value, stack_value)
      let 'existT _ __86 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __86
            [Alpha_context.Script_timestamp.t × __86 **
              Alpha_context.Script_timestamp.t ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let t1 := accu_value in
      let '(t2, stack_value) := stack_value in
      let result_value := Alpha_context.Script_timestamp.diff_value t1 t2 in
      step g_value gas k_value ks result_value stack_value
    | (Script_typed_ir.IConcat_string_pair _ k_value, accu_value, stack_value)
      ⇒
      let 'existT _ __87 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __87
            [Alpha_context.Script_string.t × __87 **
              Alpha_context.Script_string.t ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let s_value := Alpha_context.Script_string.concat_pair x_value y_value in
      step g_value gas k_value ks s_value stack_value
    | (Script_typed_ir.IConcat_string _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast
          [Script_typed_ir.boxed_list Alpha_context.Script_string.t **
            Script_typed_ir.kinstr] [accu_value, k_value] in
      let ss := accu_value in
      let total_length :=
        List.fold_left
          (fun (acc_value : S.t) ⇒
            fun (s_value : Alpha_context.Script_string.t) ⇒
              S.add acc_value
                (S.safe_int (Alpha_context.Script_string.length s_value)))
          S.zero ss.(Script_typed_ir.boxed_list.elements) in
      let? gas :=
        Local_gas_counter.consume gas
          (Script_interpreter_defs.Interp_costs.concat_string total_length) in
      let s_value :=
        Alpha_context.Script_string.concat
          ss.(Script_typed_ir.boxed_list.elements) in
      step g_value gas k_value ks s_value stack_value
    | (Script_typed_ir.ISlice_string _ k_value, accu_value, stack_value)
      let 'existT _ __88 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __88
            [Alpha_context.Script_int.num ×
              (Alpha_context.Script_string.t × __88) **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let offset := accu_value in
      let '(length, (s_value, stack_value)) := stack_value in
      let s_length := Z.of_int (Alpha_context.Script_string.length s_value) in
      let offset := Alpha_context.Script_int.to_zint offset in
      let length := Alpha_context.Script_int.to_zint length in
      if (offset <Z s_length) && ((offset +Z length) Z s_length) then
        let s_value :=
          Alpha_context.Script_string.sub s_value (Z.to_int offset)
            (Z.to_int length) in
        step g_value gas k_value ks (Some s_value) stack_value
      else
        step g_value gas k_value ks
          (None : option Alpha_context.Script_string.t) stack_value
    | (Script_typed_ir.IString_size _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_string.t ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let s_value := accu_value in
      let result_value :=
        Alpha_context.Script_int.abs
          (Alpha_context.Script_int.of_int
            (Alpha_context.Script_string.length s_value)) in
      step g_value gas k_value ks result_value stack_value
    | (Script_typed_ir.IConcat_bytes_pair _ k_value, accu_value, stack_value)
      let 'existT _ __89 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __89[bytes × __89 ** bytes ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let s_value := Bytes.cat x_value y_value in
      step g_value gas k_value ks s_value stack_value
    | (Script_typed_ir.IConcat_bytes _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Script_typed_ir.boxed_list bytes ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let ss := accu_value in
      let total_length :=
        List.fold_left
          (fun (acc_value : S.t) ⇒
            fun (s_value : bytes) ⇒
              S.add acc_value (S.safe_int (Bytes.length s_value))) S.zero
          ss.(Script_typed_ir.boxed_list.elements) in
      let? gas :=
        Local_gas_counter.consume gas
          (Script_interpreter_defs.Interp_costs.concat_string total_length) in
      let s_value :=
        Bytes.concat Bytes.empty ss.(Script_typed_ir.boxed_list.elements) in
      step g_value gas k_value ks s_value stack_value
    | (Script_typed_ir.ISlice_bytes _ k_value, accu_value, stack_value)
      let 'existT _ __90 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __90
            [Alpha_context.Script_int.num × (bytes × __90) **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let offset := accu_value in
      let '(length, (s_value, stack_value)) := stack_value in
      let s_length := Z.of_int (Bytes.length s_value) in
      let offset := Alpha_context.Script_int.to_zint offset in
      let length := Alpha_context.Script_int.to_zint length in
      if (offset <Z s_length) && ((offset +Z length) Z s_length) then
        let s_value := Bytes.sub s_value (Z.to_int offset) (Z.to_int length) in
        step g_value gas k_value ks (Some s_value) stack_value
      else
        step g_value gas k_value ks (None : option bytes) stack_value
    | (Script_typed_ir.IBytes_size _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [bytes ** Script_typed_ir.kinstr] [accu_value, k_value] in
      let s_value := accu_value in
      let result_value :=
        Alpha_context.Script_int.abs
          (Alpha_context.Script_int.of_int (Bytes.length s_value)) in
      step g_value gas k_value ks result_value stack_value
    | (Script_typed_ir.IAdd_tez _ k_value, accu_value, stack_value)
      let 'existT _ __91 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __91
            [Alpha_context.Tez.t × __91 ** Alpha_context.Tez.t **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let? res := Alpha_context.Tez.op_plusquestion x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.ISub_tez _ k_value, accu_value, stack_value)
      let 'existT _ __92 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __92
            [Alpha_context.Tez.t × __92 ** Alpha_context.Tez.t **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Tez.sub_opt x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.ISub_tez_legacy _ k_value, accu_value, stack_value)
      let 'existT _ __93 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __93
            [Alpha_context.Tez.t × __93 ** Alpha_context.Tez.t **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let? res := Alpha_context.Tez.op_minusquestion x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMul_teznat kinfo_value k_value, accu_value, stack_value)
      ⇒
      let 'existT _ __94 [stack_value, accu_value, k_value, kinfo_value] :=
        cast_exists (Es := Set)
          (fun __94
            [Alpha_context.Script_int.num × __94 ** Alpha_context.Tez.t **
              Script_typed_ir.kinstr ** Script_typed_ir.kinfo])
          [stack_value, accu_value, k_value, kinfo_value] in
      imul_teznat None g_value gas (kinfo_value, k_value) ks accu_value
        stack_value
    | (Script_typed_ir.IMul_nattez kinfo_value k_value, accu_value, stack_value)
      ⇒
      let 'existT _ __95 [stack_value, accu_value, k_value, kinfo_value] :=
        cast_exists (Es := Set)
          (fun __95
            [Alpha_context.Tez.t × __95 ** Alpha_context.Script_int.num **
              Script_typed_ir.kinstr ** Script_typed_ir.kinfo])
          [stack_value, accu_value, k_value, kinfo_value] in
      imul_nattez None g_value gas (kinfo_value, k_value) ks accu_value
        stack_value
    | (Script_typed_ir.IOr _ k_value, accu_value, stack_value)
      let 'existT _ __96 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __96[bool × __96 ** bool ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      step g_value gas k_value ks (x_value || y_value) stack_value
    | (Script_typed_ir.IAnd _ k_value, accu_value, stack_value)
      let 'existT _ __97 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __97[bool × __97 ** bool ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      step g_value gas k_value ks (x_value && y_value) stack_value
    | (Script_typed_ir.IXor _ k_value, accu_value, stack_value)
      let 'existT _ __98 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __98[bool × __98 ** bool ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Compare.Bool.(Compare.S.op_ltgt) x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.INot _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [bool ** Script_typed_ir.kinstr] [accu_value, k_value] in
      let x_value := accu_value in
      step g_value gas k_value ks (Pervasives.not x_value) stack_value
    | (Script_typed_ir.IIs_nat _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let x_value := accu_value in
      let res := Alpha_context.Script_int.is_nat x_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IAbs_int _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let x_value := accu_value in
      let res := Alpha_context.Script_int.abs x_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IInt_nat _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let x_value := accu_value in
      let res := Alpha_context.Script_int.int_value x_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.INeg _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let x_value := accu_value in
      let res := Alpha_context.Script_int.neg x_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IAdd_int _ k_value, accu_value, stack_value)
      let 'existT _ __102 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __102
            [Alpha_context.Script_int.num × __102 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.add x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IAdd_nat _ k_value, accu_value, stack_value)
      let 'existT _ __103 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __103
            [Alpha_context.Script_int.num × __103 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.add_n x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.ISub_int _ k_value, accu_value, stack_value)
      let 'existT _ __106 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __106
            [Alpha_context.Script_int.num × __106 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.sub x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMul_int _ k_value, accu_value, stack_value)
      let 'existT _ __109 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __109
            [Alpha_context.Script_int.num × __109 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.mul x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMul_nat _ k_value, accu_value, stack_value)
      let 'existT _ __111 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __111
            [Alpha_context.Script_int.num × __111 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.mul_n x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IEdiv_teznat _ k_value, accu_value, stack_value)
      let 'existT _ __112 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __112
            [Alpha_context.Script_int.num × __112 ** Alpha_context.Tez.t **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let x_value :=
        Alpha_context.Script_int.of_int64 (Alpha_context.Tez.to_mutez x_value)
        in
      let result_value :=
        match Alpha_context.Script_int.ediv x_value y_value with
        | NoneNone
        | Some (q_value, r_value)
          match
            ((Alpha_context.Script_int.to_int64 q_value),
              (Alpha_context.Script_int.to_int64 r_value)) with
          | (Some q_value, Some r_value)
            match
              ((Alpha_context.Tez.of_mutez q_value),
                (Alpha_context.Tez.of_mutez r_value)) with
            | (Some q_value, Some r_value)Some (q_value, r_value)
            | _
              (* ❌ Assert instruction is not handled. *)
              assert (option (Alpha_context.Tez.tez × Alpha_context.Tez.tez))
                false
            end
          | _
            (* ❌ Assert instruction is not handled. *)
            assert (option (Alpha_context.Tez.tez × Alpha_context.Tez.tez))
              false
          end
        end in
      step g_value gas k_value ks result_value stack_value
    | (Script_typed_ir.IEdiv_tez _ k_value, accu_value, stack_value)
      let 'existT _ __113 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __113
            [Alpha_context.Tez.t × __113 ** Alpha_context.Tez.t **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let x_value :=
        Alpha_context.Script_int.abs
          (Alpha_context.Script_int.of_int64
            (Alpha_context.Tez.to_mutez x_value)) in
      let y_value :=
        Alpha_context.Script_int.abs
          (Alpha_context.Script_int.of_int64
            (Alpha_context.Tez.to_mutez y_value)) in
      let result_value :=
        match Alpha_context.Script_int.ediv_n x_value y_value with
        | NoneNone
        | Some (q_value, r_value)
          match Alpha_context.Script_int.to_int64 r_value with
          | None
            (* ❌ Assert instruction is not handled. *)
            assert
              (option (Alpha_context.Script_int.num × Alpha_context.Tez.tez))
              false
          | Some r_value
            match Alpha_context.Tez.of_mutez r_value with
            | None
              (* ❌ Assert instruction is not handled. *)
              assert
                (option (Alpha_context.Script_int.num × Alpha_context.Tez.tez))
                false
            | Some r_valueSome (q_value, r_value)
            end
          end
        end in
      step g_value gas k_value ks result_value stack_value
    | (Script_typed_ir.IEdiv_int _ k_value, accu_value, stack_value)
      let 'existT _ __116 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __116
            [Alpha_context.Script_int.num × __116 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.ediv x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IEdiv_nat _ k_value, accu_value, stack_value)
      let 'existT _ __118 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __118
            [Alpha_context.Script_int.num × __118 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.ediv_n x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.ILsl_nat kinfo_value k_value, accu_value, stack_value)
      let 'existT _ __119 [stack_value, accu_value, k_value, kinfo_value] :=
        cast_exists (Es := Set)
          (fun __119
            [Alpha_context.Script_int.num × __119 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr **
              Script_typed_ir.kinfo])
          [stack_value, accu_value, k_value, kinfo_value] in
      ilsl_nat None g_value gas (kinfo_value, k_value) ks accu_value stack_value
    | (Script_typed_ir.ILsr_nat kinfo_value k_value, accu_value, stack_value)
      let 'existT _ __120 [stack_value, accu_value, k_value, kinfo_value] :=
        cast_exists (Es := Set)
          (fun __120
            [Alpha_context.Script_int.num × __120 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr **
              Script_typed_ir.kinfo])
          [stack_value, accu_value, k_value, kinfo_value] in
      ilsr_nat None g_value gas (kinfo_value, k_value) ks accu_value stack_value
    | (Script_typed_ir.IOr_nat _ k_value, accu_value, stack_value)
      let 'existT _ __121 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __121
            [Alpha_context.Script_int.num × __121 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.logor x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IAnd_nat _ k_value, accu_value, stack_value)
      let 'existT _ __122 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __122
            [Alpha_context.Script_int.num × __122 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.logand x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IAnd_int_nat _ k_value, accu_value, stack_value)
      let 'existT _ __123 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __123
            [Alpha_context.Script_int.num × __123 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.logand x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IXor_nat _ k_value, accu_value, stack_value)
      let 'existT _ __124 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __124
            [Alpha_context.Script_int.num × __124 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let res := Alpha_context.Script_int.logxor x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.INot_int _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let x_value := accu_value in
      let res := Alpha_context.Script_int.lognot x_value in
      step g_value gas k_value ks res stack_value
    |
      (Script_typed_ir.IIf {|
        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
          |}, accu_value, stack_value)
      let 'existT _ [__126, __127]
        [stack_value, accu_value, k_value, branch_if_false, branch_if_true] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__126, __127]
            [__126 × __127 ** bool ** Script_typed_ir.kinstr **
              Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value, branch_if_false, branch_if_true] in
      let '(res, stack_value) := stack_value in
      if accu_value then
        step g_value gas branch_if_true (Script_typed_ir.KCons k_value ks) res
          stack_value
      else
        step g_value gas branch_if_false (Script_typed_ir.KCons k_value ks) res
          stack_value
    | (Script_typed_ir.ILoop _ body k_value, _, _)
      let '[k_value, body] :=
        cast [Script_typed_ir.kinstr ** Script_typed_ir.kinstr] [k_value, body]
        in
      let ks := Script_typed_ir.KLoop_in body (Script_typed_ir.KCons k_value ks)
        in
      next g_value gas ks accu_value stack_value
    | (Script_typed_ir.ILoop_left _ bl br, _, _)
      let '[br, bl] :=
        cast [Script_typed_ir.kinstr ** Script_typed_ir.kinstr] [br, bl] in
      let ks := Script_typed_ir.KLoop_in_left bl (Script_typed_ir.KCons br ks)
        in
      next g_value gas ks accu_value stack_value
    | (Script_typed_ir.IDip _ b_value k_value, _, stack_value)
      let 'existT _ [__132, __133] [stack_value, k_value, b_value] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__132, __133]
            [__132 × __133 ** Script_typed_ir.kinstr ** Script_typed_ir.kinstr])
          [stack_value, k_value, b_value] in
      let ign := accu_value in
      let ks := Script_typed_ir.KUndip ign (Script_typed_ir.KCons k_value ks) in
      let '(accu_value, stack_value) := stack_value in
      step g_value gas b_value ks accu_value stack_value
    | (Script_typed_ir.IExec _ k_value, _, stack_value)
      let 'existT _ __135 [stack_value, k_value] :=
        cast_exists (Es := Set)
          (fun __135
            [Script_typed_ir.lambda × __135 ** Script_typed_ir.kinstr])
          [stack_value, k_value] in
      iexec None g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IApply _ capture_ty k_value, _, stack_value)
      let 'existT _ __138 [stack_value, k_value, capture_ty] :=
        cast_exists (Es := Set)
          (fun __138
            [Script_typed_ir.lambda × __138 ** Script_typed_ir.kinstr **
              Script_typed_ir.ty]) [stack_value, k_value, capture_ty] in
      let capture := accu_value in
      let '(lam, stack_value) := stack_value in
      let? '(lam', ctxt, gas) :=
        Script_interpreter_defs.apply ctxt gas capture_ty capture lam in
      step (ctxt, sc) gas k_value ks lam' stack_value
    | (Script_typed_ir.ILambda _ lam k_value, _, _)
      let '[k_value, lam] :=
        cast [Script_typed_ir.kinstr ** Script_typed_ir.lambda] [k_value, lam]
        in
      step g_value gas k_value ks lam (accu_value, stack_value)
    | (Script_typed_ir.IFailwith _ kloc tv, _, _)
      let '[tv, kloc] :=
        cast [Script_typed_ir.ty ** Alpha_context.Script.location] [tv, kloc] in
      let '{|
        Script_interpreter_defs.ifailwith_type.ifailwith := ifailwith |} :=
        ifailwith in
      ifailwith _ _ None g_value gas kloc tv accu_value
    | (Script_typed_ir.ICompare _ ty k_value, _, stack_value)
      let 'existT _ __139 [stack_value, k_value, ty] :=
        cast_exists (Es := Set)
          (fun __139
            [a × __139 ** Script_typed_ir.kinstr **
              Script_typed_ir.comparable_ty]) [stack_value, k_value, ty] in
      let a_value := accu_value in
      let '(b_value, stack_value) := stack_value in
      let r_value :=
        Alpha_context.Script_int.of_int
          (Script_comparable.compare_comparable ty a_value b_value) in
      step g_value gas k_value ks r_value stack_value
    | (Script_typed_ir.IEq _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let a_value := accu_value in
      let a_value :=
        Alpha_context.Script_int.compare a_value Alpha_context.Script_int.zero
        in
      let a_value := a_value =i 0 in
      step g_value gas k_value ks a_value stack_value
    | (Script_typed_ir.INeq _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let a_value := accu_value in
      let a_value :=
        Alpha_context.Script_int.compare a_value Alpha_context.Script_int.zero
        in
      let a_value := a_value i 0 in
      step g_value gas k_value ks a_value stack_value
    | (Script_typed_ir.ILt _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let a_value := accu_value in
      let a_value :=
        Alpha_context.Script_int.compare a_value Alpha_context.Script_int.zero
        in
      let a_value := a_value <i 0 in
      step g_value gas k_value ks a_value stack_value
    | (Script_typed_ir.ILe _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let a_value := accu_value in
      let a_value :=
        Alpha_context.Script_int.compare a_value Alpha_context.Script_int.zero
        in
      let a_value := a_value i 0 in
      step g_value gas k_value ks a_value stack_value
    | (Script_typed_ir.IGt _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let a_value := accu_value in
      let a_value :=
        Alpha_context.Script_int.compare a_value Alpha_context.Script_int.zero
        in
      let a_value := a_value >i 0 in
      step g_value gas k_value ks a_value stack_value
    | (Script_typed_ir.IGe _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.Script_int.num ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let a_value := accu_value in
      let a_value :=
        Alpha_context.Script_int.compare a_value Alpha_context.Script_int.zero
        in
      let a_value := a_value i 0 in
      step g_value gas k_value ks a_value stack_value
    | (Script_typed_ir.IPack _ ty k_value, _, _)
      let '[k_value, ty] :=
        cast [Script_typed_ir.kinstr ** Script_typed_ir.ty] [k_value, ty] in
      let value_value := accu_value in
      let? '(bytes_value, ctxt, gas) :=
        Local_gas_counter.use_gas_counter_in_context ctxt gas
          (fun (ctxt : Alpha_context.context) ⇒
            Script_ir_translator.pack_data ctxt ty value_value) in
      step (ctxt, sc) gas k_value ks bytes_value stack_value
    | (Script_typed_ir.IUnpack _ ty k_value, accu_value, _)
      let 'existT _ __IUnpack_'a [accu_value, k_value, ty] :=
        cast_exists (Es := Set)
          (fun __IUnpack_'a
            [bytes ** Script_typed_ir.kinstr ** Script_typed_ir.ty])
          [accu_value, k_value, ty] in
      let bytes_value := accu_value in
      let? '(opt, ctxt, gas) :=
        Local_gas_counter.use_gas_counter_in_context ctxt gas
          (fun (ctxt : Alpha_context.context) ⇒
            (Script_interpreter_defs.unpack :
              Alpha_context.context Script_typed_ir.ty bytes
              M? (option __IUnpack_'a × Alpha_context.context)) ctxt ty
              bytes_value) in
      step (ctxt, sc) gas k_value ks opt stack_value
    | (Script_typed_ir.IAddress _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Script_typed_ir.typed_contract ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let
        'Script_typed_ir.Typed_contract {|
          Script_typed_ir.typed_contract.Typed_contract.address := address
            |} := accu_value in
      step g_value gas k_value ks address stack_value
    |
      (Script_typed_ir.IContract kinfo_value t_value entrypoint k_value,
        accu_value, _)
      let '[accu_value, k_value, entrypoint, t_value, kinfo_value] :=
        cast
          [Script_typed_ir.address ** Script_typed_ir.kinstr **
            Alpha_context.Entrypoint.t ** Script_typed_ir.ty **
            Script_typed_ir.kinfo]
          [accu_value, k_value, entrypoint, t_value, kinfo_value] in
      let addr := accu_value in
      let entrypoint_opt :=
        if
          Alpha_context.Entrypoint.is_default
            addr.(Script_typed_ir.address.entrypoint)
        then
          Some entrypoint
        else
          if Alpha_context.Entrypoint.is_default entrypoint then
            Some addr.(Script_typed_ir.address.entrypoint)
          else
            None in
      match entrypoint_opt with
      | Some entrypoint
        let ctxt := Local_gas_counter.update_context gas ctxt in
        let? '(ctxt, maybe_contract) :=
          Script_ir_translator.parse_contract_for_script ctxt
            kinfo_value.(Script_typed_ir.kinfo.iloc) t_value
            addr.(Script_typed_ir.address.destination) entrypoint in
        let '(gas, ctxt) :=
          Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
        let accu_value := maybe_contract in
        step (ctxt, sc) gas k_value ks accu_value stack_value
      | None
        step (ctxt, sc) gas k_value ks
          (None : option Script_typed_ir.typed_contract) stack_value
      end
    | (Script_typed_ir.ITransfer_tokens kinfo_value k_value, _, stack_value)
      let 'existT _ __141 [stack_value, k_value, kinfo_value] :=
        cast_exists (Es := Set)
          (fun __141
            [Alpha_context.Tez.t × (Script_typed_ir.typed_contract × __141) **
              Script_typed_ir.kinstr ** Script_typed_ir.kinfo])
          [stack_value, k_value, kinfo_value] in
      let p_value := accu_value in
      let
        '(amount,
          (Script_typed_ir.Typed_contract {|
            Script_typed_ir.typed_contract.Typed_contract.arg_ty := arg_ty;
              Script_typed_ir.typed_contract.Typed_contract.address := address
              |}, stack_value)) := stack_value in
      let '{|
        Script_typed_ir.address.destination := destination;
          Script_typed_ir.address.entrypoint := entrypoint
          |} := address in
      let? '(accu_value, ctxt, gas) :=
        Script_interpreter_defs.transfer (ctxt, sc) gas amount
          kinfo_value.(Script_typed_ir.kinfo.iloc) arg_ty p_value destination
          entrypoint in
      step (ctxt, sc) gas k_value ks accu_value stack_value
    | (Script_typed_ir.IImplicit_account _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.public_key_hash ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let key_value := accu_value in
      let arg_ty := Script_typed_ir.unit_t in
      let address :=
        {|
          Script_typed_ir.address.destination :=
            Alpha_context.Destination.Contract
              (Alpha_context.Contract.implicit_contract key_value);
          Script_typed_ir.address.entrypoint :=
            Alpha_context.Entrypoint.default; |} in
      let res :=
        Script_typed_ir.Typed_contract
          {| Script_typed_ir.typed_contract.Typed_contract.arg_ty := arg_ty;
            Script_typed_ir.typed_contract.Typed_contract.address := address; |}
        in
      step g_value gas k_value ks res stack_value
    |
      (Script_typed_ir.IView _
        (Script_typed_ir.View_signature {|
          Script_typed_ir.view_signature.View_signature.name := name;
            Script_typed_ir.view_signature.View_signature.input_ty := input_ty;
            Script_typed_ir.view_signature.View_signature.output_ty := output_ty
            |}) k_value, _, stack_value)
      let 'existT _ [__142, __IView_'b]
        [stack_value, k_value, output_ty, input_ty, name] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__142, __IView_'b]
            [Script_typed_ir.address × __142 ** Script_typed_ir.kinstr **
              Script_typed_ir.ty ** Script_typed_ir.ty **
              Alpha_context.Script_string.t])
          [stack_value, k_value, output_ty, input_ty, name] in
      let input := accu_value in
      let '(addr, stack_value) := stack_value in
      let c_value := addr.(Script_typed_ir.address.destination) in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let return_none (ctxt : Alpha_context.context)
        : M?
          (r × f × Local_gas_counter.outdated_context ×
            Local_gas_counter.local_gas_counter) :=
        let '(gas, ctxt) :=
          Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
        step (ctxt, sc) gas k_value ks (None : option __IView_'b) stack_value in
      match c_value with
      | Alpha_context.Destination.Contract c_value
        let? '(ctxt, script_opt) :=
          Alpha_context.Contract.get_script ctxt c_value in
        match script_opt with
        | Nonereturn_none ctxt
        | Some script
          let?
            '(Script_ir_translator.Ex_script
              (Script_typed_ir.Script {|
                Script_typed_ir.script.Script.storage := storage_value;
                  Script_typed_ir.script.Script.storage_type := storage_type;
                  Script_typed_ir.script.Script.views := views
                  |}), ctxt) :=
            Script_ir_translator.parse_script None ctxt true true script in
          let 'existT _ __Ex_script_'b
            [ctxt, views, storage_type, storage_value] :=
            cast_exists (Es := Set)
              (fun __Ex_script_'b
                [Alpha_context.context ** Script_typed_ir.view_map **
                  Script_typed_ir.ty ** __Ex_script_'b])
              [ctxt, views, storage_type, storage_value] in
          let? ctxt :=
            Alpha_context.Gas.consume ctxt
              (Script_interpreter_defs.Interp_costs.view_get name views) in
          match Script_map.get name views with
          | Nonereturn_none ctxt
          | Some view
            let view_result :=
              Script_ir_translator.parse_view_returning None ctxt true
                storage_type view in
            let? '(Script_ir_translator.Ex_view f_value, ctxt) :=
              Error_monad.trace_eval
                (fun (function_parameter : unit) ⇒
                  let '_ := function_parameter in
                  Build_extensible "Ill_typed_contract"
                    (Micheline.canonical Alpha_context.Script.prim ×
                      Script_tc_errors.type_map)
                    ((Micheline.strip_locations
                      view.(Script_typed_ir.view.view_code)), nil)) view_result
              in
            match f_value with
            |
              Script_typed_ir.Lam {|
                Script_typed_ir.kdescr.kloc := kloc;
                  Script_typed_ir.kdescr.kbef :=
                    Script_typed_ir.Item_t bef_ty
                      Script_typed_ir.Bot_t;
                  Script_typed_ir.kdescr.kaft :=
                    Script_typed_ir.Item_t aft_ty
                      Script_typed_ir.Bot_t;
                  Script_typed_ir.kdescr.kinstr := kinstr
                  |} _script_view
              let? 'Script_typed_ir.Ty_ex_c pair_ty :=
                Script_typed_ir.pair_t kloc input_ty storage_type in
              let io_ty :=
                Gas_monad.Syntax.op_letstar
                  (Script_ir_translator.ty_eq Script_tc_errors.Fast kloc aft_ty
                    output_ty)
                  (fun out_eq
                    Gas_monad.Syntax.op_letplus
                      (Script_ir_translator.ty_eq Script_tc_errors.Fast kloc
                        bef_ty pair_ty) (fun in_eq(out_eq, in_eq))) in
              let? '(eq_value, ctxt) := Gas_monad.run ctxt io_ty in
              match eq_value with
              | Pervasives.Error Script_tc_errors.Inconsistent_types_fast
                return_none ctxt
              | Pervasives.Ok (Script_ir_translator.Eq, Script_ir_translator.Eq)
                ⇒
                let kkinfo := Script_typed_ir.kinfo_of_kinstr k_value in
                match kkinfo.(Script_typed_ir.kinfo.kstack_ty) with
                | Script_typed_ir.Item_t _ s_value
                  let kstack_ty := Script_typed_ir.Item_t output_ty s_value in
                  let kkinfo :=
                    Script_typed_ir.kinfo.with_kstack_ty kstack_ty kkinfo in
                  let ks :=
                    Script_typed_ir.KCons
                      (Script_typed_ir.ICons_some kkinfo k_value) ks in
                  let? '(ctxt, balance) :=
                    Alpha_context.Contract.get_balance_carbonated ctxt c_value
                    in
                  let '(gas, ctxt) :=
                    Local_gas_counter.local_gas_counter_and_outdated_context
                      ctxt in
                  step
                    (ctxt,
                      {|
                        Script_typed_ir.step_constants.source :=
                          sc.(Script_typed_ir.step_constants.self);
                        Script_typed_ir.step_constants.payer :=
                          sc.(Script_typed_ir.step_constants.payer);
                        Script_typed_ir.step_constants.self := c_value;
                        Script_typed_ir.step_constants.amount :=
                          Alpha_context.Tez.zero;
                        Script_typed_ir.step_constants.balance := balance;
                        Script_typed_ir.step_constants.chain_id :=
                          sc.(Script_typed_ir.step_constants.chain_id);
                        Script_typed_ir.step_constants.now :=
                          sc.(Script_typed_ir.step_constants.now);
                        Script_typed_ir.step_constants.level :=
                          sc.(Script_typed_ir.step_constants.level); |}) gas
                    kinstr
                    (Script_typed_ir.KView_exit sc
                      (Script_typed_ir.KReturn stack_value ks))
                    (input, storage_value)
                    (Script_typed_ir.EmptyCell, Script_typed_ir.EmptyCell)
                | _unreachable_gadt_branch
                end
              end
            | _unreachable_gadt_branch
            end
          end
        end
      | Alpha_context.Destination.Tx_rollup _return_none ctxt
      end
    |
      (Script_typed_ir.ICreate_contract {|
        Script_typed_ir.kinstr.ICreate_contract.kinfo := _;
          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
          |}, accu_value, stack_value)
      let 'existT _ [__143, __144]
        [stack_value, accu_value, k_value, code, storage_type] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__143, __144]
            [Alpha_context.Tez.t × (__143 × __144) **
              option Alpha_context.public_key_hash ** Script_typed_ir.kinstr **
              Alpha_context.Script.expr ** Script_typed_ir.ty])
          [stack_value, accu_value, k_value, code, storage_type] in
      let delegate := accu_value in
      let '(credit, (init_value, stack_value)) := stack_value in
      let? '(res, contract, ctxt, gas) :=
        Script_interpreter_defs.create_contract g_value gas storage_type code
          delegate credit init_value in
      let stack_value :=
        ({|
          Script_typed_ir.address.destination :=
            Alpha_context.Destination.Contract contract;
          Script_typed_ir.address.entrypoint :=
            Alpha_context.Entrypoint.default; |}, stack_value) in
      step (ctxt, sc) gas k_value ks res stack_value
    | (Script_typed_ir.ISet_delegate _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [option Alpha_context.public_key_hash ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let delegate := accu_value in
      let operation := Script_typed_ir.Delegation delegate in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let? '(ctxt, nonce_value) := Alpha_context.fresh_internal_nonce ctxt in
      let piop :=
        Script_typed_ir.Internal_operation
          {|
            Script_typed_ir.internal_operation.source :=
              sc.(Script_typed_ir.step_constants.self);
            Script_typed_ir.internal_operation.operation := operation;
            Script_typed_ir.internal_operation.nonce := nonce_value; |} in
      let res :=
        {| Script_typed_ir.operation.piop := piop;
          Script_typed_ir.operation.lazy_storage_diff :=
            (None : option Alpha_context.Lazy_storage.diffs); |} in
      let '(gas, ctxt) :=
        Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
      step (ctxt, sc) gas k_value ks res stack_value
    | (Script_typed_ir.IBalance _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let '(gas, ctxt) :=
        Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
      let g_value := (ctxt, sc) in
      step g_value gas k_value ks sc.(Script_typed_ir.step_constants.balance)
        (accu_value, stack_value)
    | (Script_typed_ir.ILevel _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      step g_value gas k_value ks sc.(Script_typed_ir.step_constants.level)
        (accu_value, stack_value)
    | (Script_typed_ir.INow _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      step g_value gas k_value ks sc.(Script_typed_ir.step_constants.now)
        (accu_value, stack_value)
    | (Script_typed_ir.IMin_block_time _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let min_block_time :=
        Alpha_context.Script_int.abs
          (Alpha_context.Script_int.of_int64
            (Alpha_context.Period.to_seconds
              (Alpha_context.Constants.minimal_block_delay ctxt))) in
      let new_stack := (accu_value, stack_value) in
      step g_value gas k_value ks min_block_time new_stack
    | (Script_typed_ir.ICheck_signature _ k_value, accu_value, stack_value)
      let 'existT _ __145 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __145
            [Script_typed_ir.signature × (bytes × __145) **
              Alpha_context.public_key ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let key_value := accu_value in
      let '(signature, (message, stack_value)) := stack_value in
      let res :=
        Script_typed_ir.Script_signature.check None key_value signature message
        in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IHash_key _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.public_key ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let key_value := accu_value in
      let res :=
        Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) key_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IBlake2b _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [bytes ** Script_typed_ir.kinstr] [accu_value, k_value] in
      let bytes_value := accu_value in
      let hash_value := Raw_hashes.blake2b bytes_value in
      step g_value gas k_value ks hash_value stack_value
    | (Script_typed_ir.ISha256 _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [bytes ** Script_typed_ir.kinstr] [accu_value, k_value] in
      let bytes_value := accu_value in
      let hash_value := Raw_hashes.sha256 bytes_value in
      step g_value gas k_value ks hash_value stack_value
    | (Script_typed_ir.ISha512 _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [bytes ** Script_typed_ir.kinstr] [accu_value, k_value] in
      let bytes_value := accu_value in
      let hash_value := Raw_hashes.sha512 bytes_value in
      step g_value gas k_value ks hash_value stack_value
    | (Script_typed_ir.ISource _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let destination :=
        Alpha_context.Destination.Contract
          sc.(Script_typed_ir.step_constants.payer) in
      let res :=
        {| Script_typed_ir.address.destination := destination;
          Script_typed_ir.address.entrypoint :=
            Alpha_context.Entrypoint.default; |} in
      step g_value gas k_value ks res (accu_value, stack_value)
    | (Script_typed_ir.ISender _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let destination :=
        Alpha_context.Destination.Contract
          sc.(Script_typed_ir.step_constants.source) in
      let res :=
        {| Script_typed_ir.address.destination := destination;
          Script_typed_ir.address.entrypoint :=
            Alpha_context.Entrypoint.default; |} in
      step g_value gas k_value ks res (accu_value, stack_value)
    | (Script_typed_ir.ISelf _ ty entrypoint k_value, _, _)
      let '[k_value, entrypoint, ty] :=
        cast
          [Script_typed_ir.kinstr ** Alpha_context.Entrypoint.t **
            Script_typed_ir.ty] [k_value, entrypoint, ty] in
      let destination :=
        Alpha_context.Destination.Contract
          sc.(Script_typed_ir.step_constants.self) in
      let address :=
        {| Script_typed_ir.address.destination := destination;
          Script_typed_ir.address.entrypoint := entrypoint; |} in
      let res :=
        Script_typed_ir.Typed_contract
          {| Script_typed_ir.typed_contract.Typed_contract.arg_ty := ty;
            Script_typed_ir.typed_contract.Typed_contract.address := address; |}
        in
      step g_value gas k_value ks res (accu_value, stack_value)
    | (Script_typed_ir.ISelf_address _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let destination :=
        Alpha_context.Destination.Contract
          sc.(Script_typed_ir.step_constants.self) in
      let res :=
        {| Script_typed_ir.address.destination := destination;
          Script_typed_ir.address.entrypoint :=
            Alpha_context.Entrypoint.default; |} in
      step g_value gas k_value ks res (accu_value, stack_value)
    | (Script_typed_ir.IAmount _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let stack_value := (accu_value, stack_value) in
      let accu_value := sc.(Script_typed_ir.step_constants.amount) in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IDig _ _n n' k_value, _, _)
      let 'existT _ [__IDig_'b, __IDig_'d, __IDig_'u, __IDig_'c, __IDig_'t]
        [k_value, n', _n] :=
        cast_exists (Es := [Set ** Set ** Set ** Set ** Set])
          (fun '[__IDig_'b, __IDig_'d, __IDig_'u, __IDig_'c, __IDig_'t]
            [Script_typed_ir.kinstr **
              Script_typed_ir.stack_prefix_preservation_witness ** int])
          [k_value, n', _n] in
      let '((accu_value, stack_value), x_value) :=
        Script_interpreter_defs.interp_stack_prefix_preserving_operation
          (fun (v_value : __IDig_'b) ⇒
            fun (stack_value : __IDig_'c × __IDig_'t) ⇒ (stack_value, v_value))
          n' accu_value stack_value in
      let stack_value := ((accu_value, stack_value) : __IDig_'d × __IDig_'u) in
      let accu_value := x_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IDug _ _n n' k_value, _, stack_value)
      let 'existT _ [__146, __147, __IDug_'d, __IDug_'u, __IDug_'c, __IDug_'t]
        [stack_value, k_value, n', _n] :=
        cast_exists (Es := [Set ** Set ** Set ** Set ** Set ** Set])
          (fun '[__146, __147, __IDug_'d, __IDug_'u, __IDug_'c, __IDug_'t]
            [__146 × __147 ** Script_typed_ir.kinstr **
              Script_typed_ir.stack_prefix_preservation_witness ** int])
          [stack_value, k_value, n', _n] in
      let v_value := accu_value in
      let '(accu_value, stack_value) := stack_value in
      let '((accu_value, stack_value), _) :=
        Script_interpreter_defs.interp_stack_prefix_preserving_operation
          (fun (accu_value : __IDug_'c) ⇒
            fun (stack_value : __IDug_'t) ⇒
              ((v_value, (accu_value, stack_value)), tt)) n' accu_value
          stack_value in
      step g_value gas k_value ks (accu_value : __IDug_'d)
        (stack_value : __IDug_'u)
    | (Script_typed_ir.IDipn _ _n n' b_value k_value, _, _)
      let 'existT _ [__IDipn_'c, __IDipn_'t] [k_value, b_value, n', _n] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__IDipn_'c, __IDipn_'t]
            [Script_typed_ir.kinstr ** Script_typed_ir.kinstr **
              Script_typed_ir.stack_prefix_preservation_witness ** int])
          [k_value, b_value, n', _n] in
      let '(accu_value, stack_value, restore_prefix) :=
        (Script_interpreter_defs.kundip :
          Script_typed_ir.stack_prefix_preservation_witness a s
          Script_typed_ir.kinstr
          __IDipn_'c × __IDipn_'t × Script_typed_ir.kinstr) n' accu_value
          stack_value k_value in
      let ks := Script_typed_ir.KCons restore_prefix ks in
      step g_value gas b_value ks accu_value stack_value
    | (Script_typed_ir.IDropn _ _n n' k_value, _, _)
      let 'existT _ [__IDropn_'b, __IDropn_'u] [k_value, n', _n] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__IDropn_'b, __IDropn_'u]
            [Script_typed_ir.kinstr **
              Script_typed_ir.stack_prefix_preservation_witness ** int])
          [k_value, n', _n] in
      let stack_value :=
        let fix aux {a b s t : Set}
          (w_value : Script_typed_ir.stack_prefix_preservation_witness)
          (accu_value : a) (stack_value : s) {struct w_value} : b × t :=
          match (w_value, accu_value, stack_value) with
          | (Script_typed_ir.KRest, accu_value, stack_value)
            let '[stack_value, accu_value] :=
              cast [t ** b] [stack_value, accu_value] in
            (accu_value, stack_value)
          | (Script_typed_ir.KPrefix _ w_value, _, stack_value)
            let 'existT _ [__294, __295] [stack_value, w_value] :=
              cast_exists (Es := [Set ** Set])
                (fun '[__294, __295]
                  [__294 × __295 **
                    Script_typed_ir.stack_prefix_preservation_witness])
                [stack_value, w_value] in
            let '(accu_value, stack_value) := stack_value in
            aux w_value accu_value stack_value
          end in
        (aux :
          Script_typed_ir.stack_prefix_preservation_witness a s
          __IDropn_'b × __IDropn_'u) n' accu_value stack_value in
      let '(accu_value, stack_value) := stack_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.ISapling_empty_state _ memo_size k_value, _, _)
      let '[k_value, memo_size] :=
        cast [Script_typed_ir.kinstr ** Alpha_context.Sapling.Memo_size.t]
          [k_value, memo_size] in
      let state_value := Alpha_context.Sapling.empty_state None memo_size tt in
      step g_value gas k_value ks state_value (accu_value, stack_value)
    |
      (Script_typed_ir.ISapling_verify_update _ k_value, accu_value, stack_value)
      ⇒
      let 'existT _ __148 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __148
            [Alpha_context.Sapling.state × __148 **
              Alpha_context.Sapling.transaction ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let transaction := accu_value in
      let '(state_value, stack_value) := stack_value in
      let address :=
        Alpha_context.Contract.to_b58check
          sc.(Script_typed_ir.step_constants.self) in
      let sc_chain_id :=
        Script_typed_ir.Script_chain_id.make
          sc.(Script_typed_ir.step_constants.chain_id) in
      let chain_id := Script_typed_ir.Script_chain_id.to_b58check sc_chain_id in
      let anti_replay := Pervasives.op_caret address chain_id in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let? '(ctxt, balance_state_opt) :=
        Alpha_context.Sapling.verify_update ctxt state_value transaction
          anti_replay in
      let '(gas, ctxt) :=
        Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
      match balance_state_opt with
      | Some (balance, state_value)
        let state_value :=
          Some
            ((Bytes.of_string transaction.(Sapling.UTXO.transaction.bound_data)),
              ((Alpha_context.Script_int.of_int64 balance), state_value)) in
        step (ctxt, sc) gas k_value ks state_value stack_value
      | None
        step (ctxt, sc) gas k_value ks
          (None :
            option
              (Script_typed_ir.pair bytes
                (Script_typed_ir.pair Alpha_context.Script_int.num
                  Alpha_context.Sapling.state))) stack_value
      end
    |
      (Script_typed_ir.ISapling_verify_update_deprecated _ k_value, accu_value,
        stack_value)
      let 'existT _ __149 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __149
            [Alpha_context.Sapling.state × __149 **
              Sapling_repr.legacy_transaction ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let transaction := accu_value in
      let '(state_value, stack_value) := stack_value in
      let address :=
        Alpha_context.Contract.to_b58check
          sc.(Script_typed_ir.step_constants.self) in
      let sc_chain_id :=
        Script_typed_ir.Script_chain_id.make
          sc.(Script_typed_ir.step_constants.chain_id) in
      let chain_id := Script_typed_ir.Script_chain_id.to_b58check sc_chain_id in
      let anti_replay := Pervasives.op_caret address chain_id in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let? '(ctxt, balance_state_opt) :=
        Alpha_context.Sapling.Legacy.verify_update ctxt state_value transaction
          anti_replay in
      let '(gas, ctxt) :=
        Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
      match balance_state_opt with
      | Some (balance, state_value)
        let state_value :=
          Some ((Alpha_context.Script_int.of_int64 balance), state_value) in
        step (ctxt, sc) gas k_value ks state_value stack_value
      | None
        step (ctxt, sc) gas k_value ks
          (None :
            option
              (Script_typed_ir.pair Alpha_context.Script_int.num
                Alpha_context.Sapling.state)) stack_value
      end
    | (Script_typed_ir.IChainId _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let stack_value := (accu_value, stack_value) in
      let accu_value :=
        Script_typed_ir.Script_chain_id.make
          sc.(Script_typed_ir.step_constants.chain_id) in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IVoting_power _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Alpha_context.public_key_hash ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let key_hash := accu_value in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let? '(ctxt, power) := Alpha_context.Vote.get_voting_power ctxt key_hash
        in
      let power :=
        Alpha_context.Script_int.abs (Alpha_context.Script_int.of_int64 power)
        in
      let '(gas, ctxt) :=
        Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
      step (ctxt, sc) gas k_value ks power stack_value
    | (Script_typed_ir.ITotal_voting_power _ k_value, _, _)
      let k_value := cast Script_typed_ir.kinstr k_value in
      let ctxt := Local_gas_counter.update_context gas ctxt in
      let? '(ctxt, power) := Alpha_context.Vote.get_total_voting_power ctxt in
      let power :=
        Alpha_context.Script_int.abs (Alpha_context.Script_int.of_int64 power)
        in
      let '(gas, ctxt) :=
        Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
      let g_value := (ctxt, sc) in
      step g_value gas k_value ks power (accu_value, stack_value)
    | (Script_typed_ir.IKeccak _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [bytes ** Script_typed_ir.kinstr] [accu_value, k_value] in
      let bytes_value := accu_value in
      let hash_value := Raw_hashes.keccak256 bytes_value in
      step g_value gas k_value ks hash_value stack_value
    | (Script_typed_ir.ISha3 _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [bytes ** Script_typed_ir.kinstr] [accu_value, k_value] in
      let bytes_value := accu_value in
      let hash_value := Raw_hashes.sha3_256 bytes_value in
      step g_value gas k_value ks hash_value stack_value
    | (Script_typed_ir.IAdd_bls12_381_g1 _ k_value, accu_value, stack_value)
      let 'existT _ __150 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __150
            [Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t) ×
              __150 **
              Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t) **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let accu_value :=
        Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.add) x_value
          y_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IAdd_bls12_381_g2 _ k_value, accu_value, stack_value)
      let 'existT _ __151 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __151
            [Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.t) ×
              __151 **
              Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.t) **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let accu_value :=
        Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.add) x_value
          y_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IAdd_bls12_381_fr _ k_value, accu_value, stack_value)
      let 'existT _ __152 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __152
            [Script_typed_ir.Script_bls.Fr.t × __152 **
              Script_typed_ir.Script_bls.Fr.t ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let accu_value := Script_typed_ir.Script_bls.Fr.add x_value y_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IMul_bls12_381_g1 _ k_value, accu_value, stack_value)
      let 'existT _ __153 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __153
            [Script_typed_ir.Script_bls.Fr.t × __153 **
              Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t) **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let accu_value :=
        Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.mul) x_value
          y_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IMul_bls12_381_g2 _ k_value, accu_value, stack_value)
      let 'existT _ __154 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __154
            [Script_typed_ir.Script_bls.Fr.t × __154 **
              Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.t) **
              Script_typed_ir.kinstr]) [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let accu_value :=
        Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.mul) x_value
          y_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IMul_bls12_381_fr _ k_value, accu_value, stack_value)
      let 'existT _ __155 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __155
            [Script_typed_ir.Script_bls.Fr.t × __155 **
              Script_typed_ir.Script_bls.Fr.t ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let accu_value := Script_typed_ir.Script_bls.Fr.mul x_value y_value in
      step g_value gas k_value ks accu_value stack_value
    | (Script_typed_ir.IMul_bls12_381_fr_z _ k_value, accu_value, stack_value)
      ⇒
      let 'existT _ __157 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __157
            [Script_typed_ir.Script_bls.Fr.t × __157 **
              Alpha_context.Script_int.num ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let x_value := accu_value in
      let '(y_value, stack_value) := stack_value in
      let x_value :=
        Script_typed_ir.Script_bls.Fr.of_z
          (Alpha_context.Script_int.to_zint x_value) in
      let res := Script_typed_ir.Script_bls.Fr.mul x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IMul_bls12_381_z_fr _ k_value, accu_value, stack_value)
      ⇒
      let 'existT _ __159 [stack_value, accu_value, k_value] :=
        cast_exists (Es := Set)
          (fun __159
            [Alpha_context.Script_int.num × __159 **
              Script_typed_ir.Script_bls.Fr.t ** Script_typed_ir.kinstr])
          [stack_value, accu_value, k_value] in
      let y_value := accu_value in
      let '(x_value, stack_value) := stack_value in
      let x_value :=
        Script_typed_ir.Script_bls.Fr.of_z
          (Alpha_context.Script_int.to_zint x_value) in
      let res := Script_typed_ir.Script_bls.Fr.mul x_value y_value in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.IInt_bls12_381_fr _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast [Script_typed_ir.Script_bls.Fr.t ** Script_typed_ir.kinstr]
          [accu_value, k_value] in
      let x_value := accu_value in
      let res :=
        Alpha_context.Script_int.of_zint
          (Script_typed_ir.Script_bls.Fr.to_z x_value) in
      step g_value gas k_value ks res stack_value
    | (Script_typed_ir.INeg_bls12_381_g1 _ k_value, accu_value, _)
      let '[accu_value, k_value] :=
        cast
          [Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t) **
            Script_typed_ir.kinstr] [accu_value, k_value] in
      let x_value := accu_value in
      let accu_value :=
        Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.negate)
          x_value in
      step g_value gas k_value