🥷 Sapling_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.V7.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.

Definition transaction : Set := Sapling.UTXO.transaction.

Definition legacy_transaction : Set := Sapling.UTXO.Legacy.transaction.

Definition transaction_encoding : Data_encoding.t Sapling.UTXO.transaction :=
  Sapling.UTXO.transaction_encoding.

Module diff.
  Record record : Set := Build {
    commitments_and_ciphertexts :
      list (Sapling.Commitment.t × Sapling.Ciphertext.t);
    nullifiers : list Sapling.Nullifier.t;
  }.
  Definition with_commitments_and_ciphertexts commitments_and_ciphertexts
    (r : record) :=
    Build commitments_and_ciphertexts r.(nullifiers).
  Definition with_nullifiers nullifiers (r : record) :=
    Build r.(commitments_and_ciphertexts) nullifiers.
End diff.
Definition diff := diff.record.

Definition diff_encoding : Data_encoding.encoding diff :=
  Data_encoding.conv
    (fun (d_value : diff) ⇒
      (d_value.(diff.commitments_and_ciphertexts), d_value.(diff.nullifiers)))
    (fun (function_parameter :
      list (Sapling.Commitment.t × Sapling.Ciphertext.t) ×
        list Sapling.Nullifier.t) ⇒
      let '(commitments_and_ciphertexts, nullifiers) := function_parameter in
      let '_ :=
        match commitments_and_ciphertexts with
        | [] ⇒ tt
        | cons (_cm_hd, ct_hd) rest ⇒
          let memo_size := Sapling.Ciphertext.get_memo_size ct_hd in
          List.iter
            (fun (function_parameter :
              Sapling.Commitment.t × Sapling.Ciphertext.t) ⇒
              let '(_cm, ct) := function_parameter in
              (* ❌ Assert instruction is not handled. *)
              assert unit ((Sapling.Ciphertext.get_memo_size ct) =i memo_size))
            rest
        end in
      {| diff.commitments_and_ciphertexts := commitments_and_ciphertexts;
        diff.nullifiers := nullifiers; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "commitments_and_ciphertexts"
        (Data_encoding.list_value None
          (Data_encoding.tup2 Sapling.Commitment.encoding
            Sapling.Ciphertext.encoding)))
      (Data_encoding.req None None "nullifiers"
        (Data_encoding.list_value None Sapling.Nullifier.encoding))).

Module Memo_size.
  Definition t : Set := int.

  Definition encoding : Data_encoding.encoding int := Data_encoding.uint16.

  Definition equal : int → int → bool := Compare.Int.op_eq.

  Definition max_uint16 : int := 65535.

  Definition max_uint16_z : Z.t := Z.of_int max_uint16.

  Definition err {A : Set} : Pervasives.result A string :=
    Pervasives.Error
      (Pervasives.op_caret "a positive 16-bit integer (between 0 and "
        (Pervasives.op_caret (Pervasives.string_of_int max_uint16) ")")).

  Definition parse_z (z_value : Z.t) : Pervasives.result int string :=
    if (Z.zero ≤Z z_value) && (z_value ≤Z max_uint16_z) then
      Pervasives.Ok (Z.to_int z_value)
    else
      err.

  Definition unparse_to_z : int → Z.t := Z.of_int.

  Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
    let '_ := function_parameter in
    Cache_memory_helpers.op_exclamationexclamation 0.
End Memo_size.

Definition transaction_get_memo_size (transaction : Sapling.UTXO.transaction)
  : option int :=
  match transaction.(Sapling.UTXO.transaction.outputs) with
  | [] ⇒ None
  | cons {| Sapling.UTXO.output.ciphertext := ciphertext |} _ ⇒
    Some (Sapling.Ciphertext.get_memo_size ciphertext)
  end.

Definition input_in_memory_size : Saturation_repr.t :=
  let cv_size := Cache_memory_helpers.string_size_gen 32 in
  let nf_size := Cache_memory_helpers.string_size_gen 32 in
  let rk_size := Cache_memory_helpers.string_size_gen 32 in
  let proof_i_size := Cache_memory_helpers.string_size_gen ((48 +i 96) +i 48) in
  let signature_size := Cache_memory_helpers.string_size_gen 64 in
  Cache_memory_helpers.op_plusexclamation
    (Cache_memory_helpers.op_plusexclamation
      (Cache_memory_helpers.op_plusexclamation
        (Cache_memory_helpers.op_plusexclamation
          (Cache_memory_helpers.op_plusexclamation
            (Cache_memory_helpers.op_plusexclamation
              Cache_memory_helpers.header_size
              (Cache_memory_helpers.op_starquestion
                Cache_memory_helpers.word_size 5)) cv_size) nf_size) rk_size)
      proof_i_size) signature_size.

Definition ciphertext_size : int → Saturation_repr.t :=
  let cv_size := Cache_memory_helpers.string_size_gen 32 in
  let epk_size := Cache_memory_helpers.string_size_gen 32 in
  let nonce_enc_size := Cache_memory_helpers.string_size_gen 24 in
  let payload_out_size :=
    Cache_memory_helpers.string_size_gen ((32 +i 32) +i 16) in
  let nonce_out_size := Cache_memory_helpers.string_size_gen 24 in
  let fixed_payload_data_size := (((11 +i 8) +i 32) +i 16) +i 4 in
  fun (memo_size : int) ⇒
    let payload_size :=
      Cache_memory_helpers.string_size_gen
        (memo_size +i fixed_payload_data_size) in
    Cache_memory_helpers.op_plusexclamation
      (Cache_memory_helpers.op_plusexclamation
        (Cache_memory_helpers.op_plusexclamation
          (Cache_memory_helpers.op_plusexclamation
            (Cache_memory_helpers.op_plusexclamation
              (Cache_memory_helpers.op_plusexclamation
                (Cache_memory_helpers.op_plusexclamation
                  Cache_memory_helpers.header_size
                  (Cache_memory_helpers.op_starquestion
                    Cache_memory_helpers.word_size 6)) cv_size) epk_size)
            payload_size) nonce_enc_size) payload_out_size) nonce_out_size.

Definition output_in_memory_size : int → Saturation_repr.t :=
  let cm_size := Cache_memory_helpers.string_size_gen 32 in
  let proof_o_size := Cache_memory_helpers.string_size_gen ((48 +i 96) +i 48) in
  fun (memo_size : int) ⇒
    Cache_memory_helpers.op_plusexclamation
      (Cache_memory_helpers.op_plusexclamation
        (Cache_memory_helpers.op_plusexclamation
          (Cache_memory_helpers.op_plusexclamation
            Cache_memory_helpers.header_size
            (Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size
              3)) cm_size) proof_o_size) (ciphertext_size memo_size).

Returns an approximation of the in-memory size of a Sapling transaction.

Definition transaction_in_memory_size (transaction : Sapling.UTXO.transaction)
  : Saturation_repr.t :=
  let binding_sig_size := Cache_memory_helpers.string_size_gen 64 in
  let balance_size := Cache_memory_helpers.int64_size in
  let root_size := Cache_memory_helpers.string_size_gen 32 in
  let inputs := List.length transaction.(Sapling.UTXO.transaction.inputs) in
  let outputs := List.length transaction.(Sapling.UTXO.transaction.outputs) in
  let memo_size := Option.value_value (transaction_get_memo_size transaction) 0
    in
  let bound_data_size :=
    Cache_memory_helpers.string_size
      transaction.(Sapling.UTXO.transaction.bound_data) in
  Cache_memory_helpers.op_plusexclamation
    (Cache_memory_helpers.op_plusexclamation
      (Cache_memory_helpers.op_plusexclamation
        (Cache_memory_helpers.op_plusexclamation
          (Cache_memory_helpers.op_plusexclamation
            (Cache_memory_helpers.op_plusexclamation
              (Cache_memory_helpers.op_plusexclamation
                Cache_memory_helpers.header_size
                (Cache_memory_helpers.op_starquestion
                  Cache_memory_helpers.word_size 5))
              (Cache_memory_helpers.op_starquestion
                (Cache_memory_helpers.list_cell_size input_in_memory_size)
                inputs))
            (Cache_memory_helpers.op_starquestion
              (Cache_memory_helpers.list_cell_size
                (output_in_memory_size memo_size)) outputs)) binding_sig_size)
        balance_size) root_size) bound_data_size.

Returns an approximation of the in-memory size of a Sapling diff.

Definition diff_in_memory_size (function_parameter : diff)
  : Saturation_repr.t :=
  let '{|
    diff.commitments_and_ciphertexts := commitments_and_ciphertexts;
      diff.nullifiers := nullifiers
      |} := function_parameter in
  let cms_and_cts := List.length commitments_and_ciphertexts in
  let nfs := List.length nullifiers in
  let cm_size := Cache_memory_helpers.string_size_gen 32 in
  let nf_size := Cache_memory_helpers.string_size_gen 32 in
  let memo_size :=
    match commitments_and_ciphertexts with
    | [] ⇒ 0
    | cons (_, ct) _ ⇒ Sapling.Ciphertext.get_memo_size ct
    end in
  Cache_memory_helpers.op_plusexclamation
    (Cache_memory_helpers.op_plusexclamation
      (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
        (Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size 2))
      (Cache_memory_helpers.op_starquestion
        (Cache_memory_helpers.list_cell_size
          (Cache_memory_helpers.boxed_tup2 cm_size (ciphertext_size memo_size)))
        cms_and_cts))
    (Cache_memory_helpers.op_starquestion
      (Cache_memory_helpers.list_cell_size nf_size) nfs).