Skip to main content

🇿 Zk_rollup_apply.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
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) bool)
  (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.ex_token.Ex_token.ticketer := ticketer;
          Ticket_token.ex_token.Ex_token.contents_type := contents_type;
          Ticket_token.ex_token.Ex_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 (ticket_size >i 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_token.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)).