🇿 Zk_rollup_apply.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_transfer.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_parameters.

Init function; without side-effects in Coq

Definition init_module : unit :=
  let description := "ZK rollups will be enabled in a future proposal." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.zk_rollup_disabled" "ZK rollups are disabled" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Zk_rollup_feature_disabled" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Zk_rollup_feature_disabled" unit tt) in
  let description := "The value of [nb_ops] should never be negative." in
  Error_monad.register_error_kind Error_monad.Permanent
    "operation.zk_rollup_negative_nb_ops"
    "ZK rollups negative number of operations" description
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format) "%s") description))
    Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Zk_rollup_negative_nb_ops" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Zk_rollup_negative_nb_ops" unit tt).

Definition assert_feature_enabled (ctxt : Alpha_context.context) : M? unit :=
  Error_monad.error_unless (Alpha_context.Constants.zk_rollup_enable ctxt)
    (Build_extensible "Zk_rollup_feature_disabled" unit tt).

Definition originate {A : Set}
  (ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
  (public_parameters : Plonk.public_parameters)
  (circuits_info :
    Alpha_context.Zk_rollup.Account.SMap.(Map.S.t)
      Alpha_context.Zk_rollup.Account.circuit_info)
  (init_state : Array.t Bls.Primitive.Fr.(S.PRIME_FIELD.t)) (nb_ops : int)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list A) :=
  let? '_ := assert_feature_enabled ctxt in
  let? '_ :=
    Error_monad.error_when (nb_ops <i 0)
      (Build_extensible "Zk_rollup_negative_nb_ops" unit tt) in
  Error_monad.Lwt_result_syntax.op_letplus
    (Alpha_context.Zk_rollup.originate ctxt
      {|
        Alpha_context.Zk_rollup.Account.static.public_parameters :=
          public_parameters;
        Alpha_context.Zk_rollup.Account.static.state_length :=
          Array.length init_state;
        Alpha_context.Zk_rollup.Account.static.circuits_info := circuits_info;
        Alpha_context.Zk_rollup.Account.static.nb_ops := nb_ops; |} init_state)
    (fun function_parameter ⇒
      let '(ctxt, originated_zk_rollup, storage_size) := function_parameter in
      let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
      let result_value :=
        Apply_results.Zk_rollup_origination_result
          {|
            Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
              := nil;
            Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
              := originated_zk_rollup;
            Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
              := consumed_gas;
            Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.storage_size
              := storage_size; |} in
      (ctxt, result_value, nil)).

[parse_ticket ~ticketer ~contents ~ty ctxt] reconstructs a ticket from individual parts submitted as part of a Zk_rollup_publish operation.

Definition parse_ticket
  (ticketer : Alpha_context.Contract.t)
  (contents : Micheline.canonical Alpha_context.Script.prim)
  (ty_value : Micheline.canonical Alpha_context.Script.prim)
  (ctxt : Alpha_context.context)
  : M? (Alpha_context.context × Ticket_token.ex_token) :=
  let? '(Script_ir_translator.Ex_comparable_ty contents_type, ctxt) :=
    Script_ir_translator.parse_comparable_ty ctxt
      (Micheline.root_value ty_value) in
  let 'existT _ __Ex_comparable_ty_'a [ctxt, contents_type] :=
    cast_exists (Es := Set)
      (fun __Ex_comparable_ty_'a ⇒
        [Alpha_context.context ** Script_typed_ir.comparable_ty])
      [ctxt, contents_type] in
  let? '(contents, ctxt) :=
    ((Script_ir_translator.parse_comparable_data None ctxt contents_type
      (Micheline.root_value contents)) :
      M? (__Ex_comparable_ty_'a × Alpha_context.context)) in
  return?
    (ctxt,
      (Ticket_token.Ex_token
        {| Ticket_token.parsed_token.ticketer := ticketer;
          Ticket_token.parsed_token.contents_type := contents_type;
          Ticket_token.parsed_token.contents := contents; |})).

Definition publish {A : Set}
  (ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
  (zk_rollup : Alpha_context.Zk_rollup.t)
  (l2_ops :
    list
      (Alpha_context.Zk_rollup.Operation.t ×
        option Alpha_context.Zk_rollup.Ticket.t))
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list A) :=
  let? '_ := assert_feature_enabled ctxt in
  let? '_ :=
    Error_monad.error_unless
      (List.for_all
        (fun (function_parameter :
          Alpha_context.Zk_rollup.Operation.t ×
            option Alpha_context.Zk_rollup.Ticket.t) ⇒
          let '(l2_op, _ticket_opt) := function_parameter in
          l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
          ≤Z Z.zero) l2_ops) (Build_extensible "Deposit_as_external" unit tt)
    in
  let? '(ctxt, l2_ops_with_ticket_hashes) :=
    List.fold_left_map_es
      (fun (ctxt : Alpha_context.context) ⇒
        fun (function_parameter :
          Alpha_context.Zk_rollup.Operation.t ×
            option Alpha_context.Zk_rollup.Ticket.t) ⇒
          let '(l2_op, ticket_opt) := function_parameter in
          match ticket_opt with
          | None ⇒
            let? '_ :=
              Error_monad.error_unless
                (l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
                =Z Z.zero) (Build_extensible "Invalid_deposit_amount" unit tt)
              in
            return? (ctxt, (l2_op, None))
          |
            Some {|
              Alpha_context.Zk_rollup.Ticket.t.contents := contents;
                Alpha_context.Zk_rollup.Ticket.t.ty := ty_value;
                Alpha_context.Zk_rollup.Ticket.t.ticketer := ticketer
                |} ⇒
            let? '_ :=
              Error_monad.error_when
                (l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)
                =Z Z.zero) (Build_extensible "Invalid_deposit_amount" unit tt)
              in
            let? '(ctxt, ticket_token) :=
              parse_ticket ticketer contents ty_value ctxt in
            let? '(receiver_ticket_hash, ctxt) :=
              Ticket_balance_key.of_ex_token ctxt
                (Alpha_context.Destination.Contract
                  (Contract_repr.Implicit
                    l2_op.(Alpha_context.Zk_rollup.Operation.t.l1_dst)))
                ticket_token in
            let? '(source_ticket_hash, ctxt) :=
              Ticket_balance_key.of_ex_token ctxt
                (Alpha_context.Destination.Zk_rollup zk_rollup) ticket_token in
            let? '_ :=
              Error_monad.error_unless
                (Alpha_context.Ticket_hash.equal
                  l2_op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id)
                  source_ticket_hash)
                (Build_extensible "Invalid_deposit_ticket" unit tt) in
            return? (ctxt, (l2_op, (Some receiver_ticket_hash)))
          end) ctxt l2_ops in
  Error_monad.Lwt_result_syntax.op_letplus
    (Alpha_context.Zk_rollup.add_to_pending ctxt zk_rollup
      l2_ops_with_ticket_hashes)
    (fun function_parameter ⇒
      let '(ctxt, paid_storage_size_diff) := function_parameter in
      let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
      let result_value :=
        Apply_results.Zk_rollup_publish_result
          {|
            Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
              := nil;
            Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
              := consumed_gas;
            Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
              := paid_storage_size_diff; |} in
      (ctxt, result_value, nil)).

Definition transaction_to_zk_rollup {A B : Set}
  (ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
  (parameters : Script_typed_ir.pair (Script_typed_ir.ticket A) bytes)
  (dst_rollup : Alpha_context.Zk_rollup.t) (since : Alpha_context.context)
  : M?
    (Alpha_context.context ×
      Apply_internal_results.successful_internal_operation_result × list B) :=
  let? '_ := assert_feature_enabled ctxt in
  let? '{|
    Zk_rollup_parameters.deposit_parameters.ex_ticket := ex_ticket;
      Zk_rollup_parameters.deposit_parameters.zkru_operation := zkru_operation
      |} := Zk_rollup_parameters.get_deposit_parameters parameters_ty parameters
    in
  let? '(ticket_size, ctxt) := Ticket_scanner.ex_ticket_size ctxt ex_ticket in
  let limit := Alpha_context.Constants.tx_rollup_max_ticket_payload_size ctxt in
  let? '_ :=
    Error_monad.error_when (Saturation_repr.op_gtexclamation ticket_size limit)
      (Build_extensible "Ticket_payload_size_limit_exceeded"
        Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded
        {|
          Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded.payload_size
            := ticket_size;
          Alpha_context.Zk_rollup.Errors.Ticket_payload_size_limit_exceeded.limit
            := limit; |}) in
  let '(ex_token, ticket_amount) :=
    Ticket_scanner.ex_token_and_amount_of_ex_ticket ex_ticket in
  let? '(ticket_hash, ctxt) :=
    Ticket_balance_key.of_ex_token ctxt
      (Alpha_context.Destination.Zk_rollup dst_rollup) ex_token in
  let ticket_amount := Script_int.to_zint ticket_amount in
  let? '_ :=
    Error_monad.error_unless
      (ticket_amount =Z
      zkru_operation.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount))
      (Build_extensible "Invalid_deposit_amount" unit tt) in
  let? '_ :=
    Error_monad.error_unless
      (Alpha_context.Ticket_hash.equal ticket_hash
        zkru_operation.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id))
      (Build_extensible "Invalid_deposit_ticket" unit tt) in
  let? '(receiver_ticket_hash, ctxt) :=
    Ticket_balance_key.of_ex_token ctxt
      (Alpha_context.Destination.Contract
        (Contract_repr.Implicit
          zkru_operation.(Alpha_context.Zk_rollup.Operation.t.l1_dst))) ex_token
    in
  Error_monad.Lwt_result_syntax.op_letplus
    (Alpha_context.Zk_rollup.add_to_pending ctxt
      zkru_operation.(Alpha_context.Zk_rollup.Operation.t.rollup_id)
      [ (zkru_operation, (Some receiver_ticket_hash)) ])
    (fun function_parameter ⇒
      let '(ctxt, paid_storage_size_diff) := function_parameter in
      let result_value :=
        Apply_internal_results.ITransaction_result
          (Apply_internal_results.Transaction_to_zk_rollup_result
            {|
              Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.ticket_hash
                := ticket_hash;
              Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.balance_updates
                := nil;
              Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.consumed_gas
                := Alpha_context.Gas.consumed since ctxt;
              Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.paid_storage_size_diff
                := paid_storage_size_diff; |}) in
      (ctxt, result_value, nil)).

Definition SMap :=
  Map.Make
    {|
      Compare.COMPARABLE.compare := String.compare
    |}.

Definition insert {A : Set} (s_value : String.t) (x_value : A)
  : SMap.(Map.S.t) (list A) → SMap.(Map.S.t) (list A) :=
  SMap.(Map.S.update) s_value
    (fun (function_parameter : option (list A)) ⇒
      match function_parameter with
      | None ⇒ Some [ x_value ]
      | Some l_value ⇒ Some (cons x_value l_value)
      end).

Definition collect_pending_ops_inputs {A : Set}
  (zk_rollup : Alpha_context.Zk_rollup.t)
  (account : Alpha_context.Zk_rollup.Account.t)
  (rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
  (pending_ops_and_pis :
    list
      ((Alpha_context.Zk_rollup.Operation.t × A) ×
        (String.t × Alpha_context.Zk_rollup.Update.op_pi)))
  : M?
    (SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
      Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t) ×
      list bool) :=
  let? '(rev_pi_map, new_state, fees, rev_exit_validites) :=
    List.fold_left_es
      (fun (function_parameter :
        SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
          Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t) ×
          list bool) ⇒
        let '(rev_pi_map, old_state, fees, rev_exit_validites) :=
          function_parameter in
        fun (function_parameter :
          (Alpha_context.Zk_rollup.Operation.t × A) ×
            (String.t × Alpha_context.Zk_rollup.Update.op_pi)) ⇒
          let '((l2_op, _ticket_hash_opt), (name, sent_pi)) :=
            function_parameter in
          let new_state :=
            sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.new_state) in
          let? '_ :=
            Error_monad.error_unless
              ((Array.length new_state) =i
              account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.state_length))
              (Build_extensible "Inconsistent_state_update" unit tt) in
          let pi :=
            Alpha_context.Zk_rollup.Circuit_public_inputs.Pending_op
              {|
                Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.old_state
                  := old_state;
                Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.new_state
                  := new_state;
                Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.fee
                  := sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.fee);
                Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.exit_validity
                  :=
                  sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.exit_validity);
                Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.zk_rollup
                  := zk_rollup;
                Alpha_context.Zk_rollup.Circuit_public_inputs.pending_op_public_inputs.l2_op
                  := l2_op; |} in
          let rev_pi_map :=
            insert name
              (Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
              rev_pi_map in
          return?
            (rev_pi_map, new_state,
              (Bls.Primitive.Fr.(S.PRIME_FIELD.add) fees
                sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.fee)),
              (cons sent_pi.(Alpha_context.Zk_rollup.Update.op_pi.exit_validity)
                rev_exit_validites)))
      (rev_pi_map,
        account.(Alpha_context.Zk_rollup.Account.t.dynamic).(Alpha_context.Zk_rollup.Account.dynamic.state),
        Bls.Primitive.Fr.(S.PRIME_FIELD.zero), nil) pending_ops_and_pis in
  return? (rev_pi_map, new_state, fees, (List.rev rev_exit_validites)).

Definition collect_pivate_batch_inputs
  (zk_rollup : Alpha_context.Zk_rollup.t)
  (account : Alpha_context.Zk_rollup.Account.t)
  (rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
  (update : Alpha_context.Zk_rollup.Update.t)
  (prev_state : Alpha_context.Zk_rollup.State.t)
  (fees : Bls.Primitive.Fr.(S.PRIME_FIELD.t))
  : M?
    (SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
      Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t)) :=
  let is_private
    (function_parameter : option Alpha_context.Zk_rollup.Account.circuit_info)
    : bool :=
    match function_parameter with
    | Some Alpha_context.Zk_rollup.Account.Private ⇒ true
    | _ ⇒ false
    end in
  List.fold_left_es
    (fun (function_parameter :
      SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
        Alpha_context.Zk_rollup.State.t × Bls.Primitive.Fr.(S.PRIME_FIELD.t)) ⇒
      let '(rev_pi_map, old_state, fees) := function_parameter in
      fun (function_parameter :
        string × Alpha_context.Zk_rollup.Update.private_inner_pi) ⇒
        let '(name, sent_pi) := function_parameter in
        let? '_ :=
          Error_monad.error_unless
            (is_private
              (Alpha_context.Zk_rollup.Account.SMap.(Map.S.find) name
                account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.circuits_info)))
            (Build_extensible "Invalid_circuit" unit tt) in
        let new_state :=
          sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.new_state) in
        let? '_ :=
          Error_monad.error_unless
            ((Array.length new_state) =i
            account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.state_length))
            (Build_extensible "Inconsistent_state_update" unit tt) in
        let pi :=
          Alpha_context.Zk_rollup.Circuit_public_inputs.Private_batch
            {|
              Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.old_state
                := old_state;
              Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.new_state
                := new_state;
              Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.fees
                :=
                sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.fees);
              Alpha_context.Zk_rollup.Circuit_public_inputs.private_batch_public_inputs.zk_rollup
                := zk_rollup; |} in
        let rev_pi_map :=
          insert name
            (Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
            rev_pi_map in
        return?
          (rev_pi_map, new_state,
            (Bls.Primitive.Fr.(S.PRIME_FIELD.add) fees
              sent_pi.(Alpha_context.Zk_rollup.Update.private_inner_pi.fees))))
    (rev_pi_map, prev_state, fees)
    update.(Alpha_context.Zk_rollup.Update.t.private_pis).

Definition collect_fee_inputs
  (prev_state : Alpha_context.Zk_rollup.State.t)
  (update : Alpha_context.Zk_rollup.Update.t)
  (fees : Bls.Primitive.Fr.(S.PRIME_FIELD.t))
  (rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
  : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
    Alpha_context.Zk_rollup.State.t :=
  let old_state := prev_state in
  let new_state :=
    update.(Alpha_context.Zk_rollup.Update.t.fee_pi).(Alpha_context.Zk_rollup.Update.fee_pi.new_state)
    in
  let pi :=
    Alpha_context.Zk_rollup.Circuit_public_inputs.Fee
      {|
        Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.old_state
          := old_state;
        Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.new_state
          := new_state;
        Alpha_context.Zk_rollup.Circuit_public_inputs.fee_public_inputs.fees :=
          fees; |} in
  let rev_pi_map :=
    insert "fee"
      (Alpha_context.Zk_rollup.Circuit_public_inputs.to_scalar_array pi)
      rev_pi_map in
  (rev_pi_map, new_state).

Definition collect_inputs {A : Set}
  (zk_rollup : Alpha_context.Zk_rollup.t)
  (account : Alpha_context.Zk_rollup.Account.t)
  (rev_pi_map : SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))))
  (pending_ops_and_pis :
    list
      ((Alpha_context.Zk_rollup.Operation.t × A) ×
        (String.t × Alpha_context.Zk_rollup.Update.op_pi)))
  (update : Alpha_context.Zk_rollup.Update.t)
  : M?
    (SMap.(Map.S.t) (list (array Bls.Primitive.Fr.(S.PRIME_FIELD.t))) ×
      list bool × Alpha_context.Zk_rollup.State.t) :=
  let? '(rev_pi_map, new_state, fees, exit_validities) :=
    collect_pending_ops_inputs zk_rollup account rev_pi_map pending_ops_and_pis
    in
  let? '(rev_pi_map, new_state, fees) :=
    collect_pivate_batch_inputs zk_rollup account rev_pi_map update new_state
      fees in
  let '(rev_pi_map, new_state) :=
    collect_fee_inputs new_state update fees rev_pi_map in
  let pi_map := SMap.(Map.S.map) List.rev rev_pi_map in
  return? (pi_map, exit_validities, new_state).

Definition perform_exits
  (ctxt : Alpha_context.context)
  (exits :
    list
      ((Alpha_context.Zk_rollup.Operation.t × option Alpha_context.Ticket_hash.t)
        × bool)) : M? (Alpha_context.context × Z.t) :=
  List.fold_left_es
    (fun (function_parameter : Alpha_context.context × Z.t) ⇒
      let '(ctxt, storage_diff) := function_parameter in
      fun (function_parameter :
        (Alpha_context.Zk_rollup.Operation.t ×
          option Alpha_context.Ticket_hash.t) × bool) ⇒
        let '((op, ticket_hash_opt), exit_validity) := function_parameter in
        match ticket_hash_opt with
        | None ⇒
          let? '_ :=
            Error_monad.error_unless
              (Z.zero =Z
              op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount))
              (Build_extensible "Invalid_deposit_amount" unit tt) in
          return? (ctxt, storage_diff)
        | Some receiver_ticket_hash ⇒
          if exit_validity then
            let? amount :=
              Option.value_e
                (Ticket_amount.of_zint
                  (Z.abs
                    op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.amount)))
                (Error_monad.trace_of_error
                  (Build_extensible "Invalid_deposit_amount" unit tt)) in
            let? '(ctxt, diff_value) :=
              Ticket_transfer.transfer_ticket_with_hashes ctxt
                op.(Alpha_context.Zk_rollup.Operation.t.price).(Alpha_context.Zk_rollup.Operation.price.id)
                receiver_ticket_hash amount in
            return? (ctxt, (diff_value +Z storage_diff))
          else
            return? (ctxt, storage_diff)
        end) (ctxt, Z.zero) exits.

Definition update {A : Set}
  (ctxt_before_op : Alpha_context.context) (ctxt : Alpha_context.context)
  (zk_rollup : Alpha_context.Zk_rollup.t)
  (update : Alpha_context.Zk_rollup.Update.t)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list A) :=
  let? '_ := assert_feature_enabled ctxt in
  let rev_pi_map {B : Set} : SMap.(Map.S.t) B :=
    SMap.(Map.S.empty) in
  let? '(ctxt, account) := Alpha_context.Zk_rollup.account ctxt zk_rollup in
  let update_public_length :=
    List.length update.(Alpha_context.Zk_rollup.Update.t.pending_pis) in
  let? '(ctxt, pending_list_length) :=
    Alpha_context.Zk_rollup.get_pending_length ctxt zk_rollup in
  let min_pending_to_process :=
    Alpha_context.Constants.zk_rollup_min_pending_to_process ctxt in
  let? '_ :=
    Error_monad.error_when
      ((update_public_length <i pending_list_length) &&
      (update_public_length <i min_pending_to_process))
      (Build_extensible "Pending_bound" unit tt) in
  let? '(ctxt, pending_ops) :=
    Alpha_context.Zk_rollup.get_prefix ctxt zk_rollup update_public_length in
  let pending_ops_and_pis :=
    List.combine_drop pending_ops
      update.(Alpha_context.Zk_rollup.Update.t.pending_pis) in
  let? '(pi_map, exit_validities, new_state) :=
    collect_inputs zk_rollup account rev_pi_map pending_ops_and_pis update in
  let verified :=
    Plonk.verify_multi_circuits
      account.(Alpha_context.Zk_rollup.Account.t.static).(Alpha_context.Zk_rollup.Account.static.public_parameters)
      (SMap.(Map.S.bindings) pi_map)
      update.(Alpha_context.Zk_rollup.Update.t.proof) in
  let? '_ :=
    Error_monad.error_unless verified
      (Build_extensible "Invalid_verification" unit tt) in
  let? ctxt :=
    Alpha_context.Zk_rollup.update ctxt zk_rollup update_public_length
      (Alpha_context.Zk_rollup.Account.t.with_dynamic
        (Alpha_context.Zk_rollup.Account.dynamic.with_state new_state
          account.(Alpha_context.Zk_rollup.Account.t.dynamic)) account) in
  let exits := List.combine_drop pending_ops exit_validities in
  let? '(ctxt, exits_paid_storage_size_diff) := perform_exits ctxt exits in
  let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
  let result_value :=
    Apply_results.Zk_rollup_update_result
      {|
        Apply_results.successful_manager_operation_result.Zk_rollup_update_result.balance_updates
          := nil;
        Apply_results.successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
          := consumed_gas;
        Apply_results.successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
          := exits_paid_storage_size_diff; |} in
  return? (ctxt, result_value, nil).