🥷 Sapling_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.
: 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).
: 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).