🇿 Zk_rollup_parameters.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.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.

Module deposit_parameters.
  Record record : Set := Build {
    ex_ticket : Ticket_scanner.ex_ticket;
    zkru_operation : Alpha_context.Zk_rollup.Operation.t;
  }.
  Definition with_ex_ticket ex_ticket (r : record) :=
    Build ex_ticket r.(zkru_operation).
  Definition with_zkru_operation zkru_operation (r : record) :=
    Build r.(ex_ticket) zkru_operation.
End deposit_parameters.
Definition deposit_parameters := deposit_parameters.record.

Definition get_deposit_parameters {a : Set}
  (ty_value : Script_typed_ir.ty)
  (contents : Script_typed_ir.pair (Script_typed_ir.ticket a) bytes)
  : M? deposit_parameters :=
  match (ty_value, contents) with
  |
    (Script_typed_ir.Pair_t (Script_typed_ir.Ticket_t ty_value _)
      Script_typed_ir.Bytes_t _ _, (ticket, op_bytes)) ⇒
    match
      Data_encoding.Binary.of_bytes_opt
        Alpha_context.Zk_rollup.Operation.encoding op_bytes with
    | None ⇒
      Error_monad.error_value
        (Build_extensible "Wrong_deposit_parameters" unit tt)
    | Some zkru_operation ⇒
      return?
        {|
          deposit_parameters.ex_ticket :=
            Ticket_scanner.Ex_ticket ty_value ticket;
          deposit_parameters.zkru_operation := zkru_operation; |}
    end
  | _ ⇒ unreachable_gadt_branch
  end.