🇿 Zk_rollup_operation_repr.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.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_scalar.

Module price.
  Record record : Set := Build {
    id : Ticket_hash_repr.t;
    amount : Z.t;
  }.
  Definition with_id id (r : record) :=
    Build id r.(amount).
  Definition with_amount amount (r : record) :=
    Build r.(id) amount.
End price.
Definition price := price.record.

Module t.
  Record record : Set := Build {
    op_code : int;
    price : price;
    l1_dst : Signature.public_key_hash;
    rollup_id : Zk_rollup_repr.t;
    payload : array Zk_rollup_scalar.t;
  }.
  Definition with_op_code op_code (r : record) :=
    Build op_code r.(price) r.(l1_dst) r.(rollup_id) r.(payload).
  Definition with_price price (r : record) :=
    Build r.(op_code) price r.(l1_dst) r.(rollup_id) r.(payload).
  Definition with_l1_dst l1_dst (r : record) :=
    Build r.(op_code) r.(price) l1_dst r.(rollup_id) r.(payload).
  Definition with_rollup_id rollup_id (r : record) :=
    Build r.(op_code) r.(price) r.(l1_dst) rollup_id r.(payload).
  Definition with_payload payload (r : record) :=
    Build r.(op_code) r.(price) r.(l1_dst) r.(rollup_id) payload.
End t.
Definition t := t.record.

Definition int_to_scalar (x_value : int) : Zk_rollup_scalar.t :=
  Zk_rollup_scalar.of_z (Z.of_int x_value).

Definition pkh_to_scalar (x_value : Signature.public_key_hash)
  : Zk_rollup_scalar.t :=
  Zk_rollup_scalar.of_bits
    (Data_encoding.Binary.to_string_exn None
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding) x_value).

Definition ticket_hash_to_scalar (ticket_hash : Ticket_hash_repr.t)
  : Zk_rollup_scalar.t :=
  Zk_rollup_scalar.of_bits
    (Data_encoding.Binary.to_string_exn None Ticket_hash_repr.encoding
      ticket_hash).

Definition to_scalar_array (function_parameter : t)
  : Array.t Zk_rollup_scalar.t :=
  let '{|
    t.op_code := op_code;
      t.price := price;
      t.l1_dst := l1_dst;
      t.rollup_id := rollup_id;
      t.payload := payload
      |} := function_parameter in
  Array.concat
    [
      (* ❌ Arrays not handled. *)
      [
        int_to_scalar op_code;
        ticket_hash_to_scalar price.(price.id);
        Zk_rollup_scalar.of_z (Z.abs price.(price.amount));
        pkh_to_scalar l1_dst;
        Zk_rollup_repr.to_scalar rollup_id
      ];
      payload
    ].

Definition price_encoding : Data_encoding.encoding price :=
  Data_encoding.conv
    (fun (function_parameter : price) ⇒
      let '{| price.id := id; price.amount := amount |} := function_parameter in
      (id, amount))
    (fun (function_parameter : Ticket_hash_repr.t × Z.t) ⇒
      let '(id, amount) := function_parameter in
      {| price.id := id; price.amount := amount; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "id" Ticket_hash_repr.encoding)
      (Data_encoding.req None None "amount" Data_encoding.z_value)).

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{|
        t.op_code := op_code;
          t.price := price;
          t.l1_dst := l1_dst;
          t.rollup_id := rollup_id;
          t.payload := payload
          |} := function_parameter in
      (op_code, price, l1_dst, rollup_id, payload))
    (fun (function_parameter :
      int × price × Signature.public_key_hash × Zk_rollup_repr.t ×
        array Zk_rollup_scalar.t) ⇒
      let '(op_code, price, l1_dst, rollup_id, payload) := function_parameter in
      {| t.op_code := op_code; t.price := price; t.l1_dst := l1_dst;
        t.rollup_id := rollup_id; t.payload := payload; |}) None
    (Data_encoding.obj5
      (Data_encoding.req None None "op_code" Data_encoding.int31)
      (Data_encoding.req None None "price" price_encoding)
      (Data_encoding.req None None "l1_dst"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.req None None "rollup_id" Zk_rollup_repr.Address.encoding)
      (Data_encoding.req None None "payload" Plonk.scalar_array_encoding)).