🥷 Sapling_storage.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.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module COMMITMENTS.
Record signature : Set := {
init_value : Raw_context.t → Storage.Sapling.id → Raw_context.t;
default_root : Sapling.Hash.t;
get_root :
Raw_context.t → Storage.Sapling.id → M? (Raw_context.t × Sapling.Hash.t);
add :
Raw_context.t → Storage.Sapling.id → list Sapling.Commitment.t →
int64 → M? (Raw_context.t × int);
get_from :
Raw_context.t → Storage.Sapling.id → int64 →
M? (list Sapling.Commitment.t);
}.
End COMMITMENTS.
Definition COMMITMENTS := COMMITMENTS.signature.
Module Commitments.
Module H := Sapling.Hash.
Definition pow2 (h_value : int) : int64 := Int64.shift_left 1 h_value.
Definition max_height : int := 32.
Definition max_size : int64 := pow2 max_height.
Definition assert_node (node_value : int64) (height : int) : M? unit :=
let first_of_height := pow2 (max_height -i height) in
let first_of_next_height := Int64.shift_left first_of_height 1 in
if
(node_value ≥i64 first_of_height) &&
(node_value <i64 first_of_next_height)
then
Error_monad.Result_syntax.return_unit
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition assert_height (height : int) : M? unit :=
if (height ≥i 0) && (height ≤i max_height) then
Error_monad.Result_syntax.return_unit
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition assert_pos (pos : int64) (height : int) : M? unit :=
if (pos ≥i64 0) && (pos ≤i64 (pow2 height)) then
Error_monad.Result_syntax.return_unit
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition default_root : H.t := H.uncommitted max_height.
Definition init_value
: Raw_context.t → Storage.Sapling.id → Raw_context.t :=
Storage.Sapling.commitments_init.
Definition get_root_height
(ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
(height : int) : M? (Raw_context.t × H.t) :=
let? '_ := assert_node node_value height in
let? '_ := assert_height height in
let? function_parameter :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctx, id) node_value in
match function_parameter with
| (ctx, None) ⇒
let hash_value := H.uncommitted height in
return? (ctx, hash_value)
| (ctx, Some hash_value) ⇒ return? (ctx, hash_value)
end.
Definition _left (node_value : int64) : int64 := node_value ×i64 2.
Definition _right (node_value : int64) : int64 := (node_value ×i64 2) +i64 1.
Fixpoint split_at {A : Set} (n_value : int64) (l_value : list A)
: list A × list A :=
if n_value =i64 0 then
(nil, l_value)
else
match l_value with
| [] ⇒ (nil, l_value)
| cons x_value xs ⇒
let '(l1, l2) := split_at (Int64.pred n_value) xs in
((cons x_value l1), l2)
end.
#[bypass_check(guard)]
Fixpoint insert
(ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
(height : int) (pos : int64) (cms : list Sapling.Commitment.t)
{struct height} : M? (Raw_context.t × int × H.t) :=
let? '_ := assert_node node_value height in
let? '_ := assert_height height in
let? '_ := assert_pos pos height in
match (height, cms) with
| (_, []) ⇒
let? '(ctx, h_value) := get_root_height ctx id node_value height in
return? (ctx, 0, h_value)
| (0, cons cm []) ⇒
let h_value := H.of_commitment cm in
let? '(ctx, size_value) :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
(ctx, id) node_value h_value in
return? (ctx, size_value, h_value)
| _ ⇒
let height := height -i 1 in
let? '(ctx, size_children, hl, hr) :=
if pos <i64 (pow2 height) then
let _at := (pow2 height) -i64 pos in
let '(cml, cmr) := split_at _at cms in
let? '(ctx, size_l, hl) :=
insert ctx id (_left node_value) height pos cml in
let? '(ctx, size_r, hr) :=
insert ctx id (_right node_value) height 0 cmr in
return? (ctx, (size_l +i size_r), hl, hr)
else
let? '(ctx, hl) := get_root_height ctx id (_left node_value) height in
let pos := pos -i64 (pow2 height) in
let? '(ctx, size_r, hr) :=
insert ctx id (_right node_value) height pos cms in
return? (ctx, size_r, hl, hr) in
let h_value := H.merkle_hash height hl hr in
let? '(ctx, size_value, _existing) :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctx, id) node_value h_value in
return? (ctx, (size_value +i size_children), h_value)
end.
#[bypass_check(guard)]
Fixpoint fold_from_height {A : Set}
(ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
(pos : int64) (f_value : A → Sapling.Hash.t → A) (acc_value : A)
(height : int) {struct height} : M? A :=
let? '_ := assert_node node_value height in
let? '_ := assert_height height in
let? '_ := assert_pos pos height in
let? function_parameter :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctx, id) node_value in
match function_parameter with
| (_ctx, None) ⇒ return? acc_value
| (_ctx, Some h_value) ⇒
if height =i 0 then
return? (f_value acc_value h_value)
else
let full_value := pow2 (height -i 1) in
if pos <i64 full_value then
let? acc_value :=
fold_from_height ctx id (_left node_value) pos f_value acc_value
(height -i 1) in
fold_from_height ctx id (_right node_value) 0 f_value acc_value
(height -i 1)
else
let pos := pos -i64 full_value in
fold_from_height ctx id (_right node_value) pos f_value acc_value
(height -i 1)
end.
Definition root_node : int64 := 1.
Definition get_root (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? (Raw_context.t × H.t) := get_root_height ctx id root_node max_height.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(cms : list Sapling.Commitment.t) (pos : int64)
: M? (Raw_context.t × int) :=
let l_value := List.length cms in
if l_value ≤i 1000 then
let n' := pos +i64 (Int64.of_int l_value) in
if n' ≤i64 max_size then
let? '(ctx, size_value, _h) :=
insert ctx id root_node max_height pos cms in
return? (ctx, size_value)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition get_from
(ctx : Raw_context.t) (id : Storage.Sapling.id) (pos : int64)
: M? (list Sapling.Commitment.t) :=
let? l_value :=
fold_from_height ctx id root_node pos
(fun (acc_value : list Sapling.Commitment.t) ⇒
fun (c_value : Sapling.Hash.t) ⇒
cons (H.to_commitment c_value) acc_value) nil max_height in
return? (List.rev l_value).
(* Commitments *)
Definition module :=
{|
COMMITMENTS.init_value := init_value;
COMMITMENTS.default_root := default_root;
COMMITMENTS.get_root := get_root;
COMMITMENTS.add := add;
COMMITMENTS.get_from := get_from
|}.
End Commitments.
Definition Commitments : COMMITMENTS := Commitments.module.
Module Ciphertexts.
Definition init_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
: Raw_context.t := Storage.Sapling.ciphertexts_init ctx id.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(c_value : Sapling.Ciphertext.t) (pos : int64) : M? (Raw_context.t × int) :=
Storage.Sapling.Ciphertexts.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
(ctx, id) pos c_value.
#[bypass_check(guard)]
Definition get_from
(ctx : Raw_context.t) (id : Storage.Sapling.id) (offset : int64)
: M? (Raw_context.t × list Sapling.Ciphertext.t) :=
let fix aux (function_parameter : Raw_context.t × list Sapling.Ciphertext.t)
{struct function_parameter}
: int64 → M? (Raw_context.t × list Sapling.Ciphertext.t) :=
let '(ctx, acc_value) := function_parameter in
fun (pos : int64) ⇒
let? '(ctx, c_value) :=
Storage.Sapling.Ciphertexts.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctx, id) pos in
match c_value with
| None ⇒ return? (ctx, (List.rev acc_value))
| Some c_value ⇒ aux (ctx, (cons c_value acc_value)) (Int64.succ pos)
end in
aux (ctx, nil) offset.
End Ciphertexts.
Module Nullifiers.
Definition init_value
: Raw_context.t → Storage.Sapling.id → Raw_context.t :=
Storage.Sapling.nullifiers_init.
Definition size_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? int64 :=
Storage.Sapling.Nullifiers_size.(Storage_sigs.Single_data_storage.get)
(ctx, id).
Definition mem
(ctx : Raw_context.t) (id : Storage.Sapling.id) (nf : Sapling.Nullifier.t)
: M? (Raw_context.t × bool) :=
Storage.Sapling.Nullifiers_hashed.(Storage_sigs.Carbonated_data_set_storage.mem)
(ctx, id) nf.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(nfs : list Sapling.Nullifier.t) : M? (Raw_context.t × Z.t) :=
if (List.compare_length_with nfs 1000) ≤i 0 then
let? nf_start_pos := size_value ctx id in
let? '(ctx, nf_end_pos, size_value) :=
List.fold_right_es
(fun (nf : Sapling.Nullifier.t) ⇒
fun (function_parameter : Raw_context.t × int64 × Z.t) ⇒
let '(ctx, pos, acc_size) := function_parameter in
let? '(ctx, size_value) :=
Storage.Sapling.Nullifiers_hashed.(Storage_sigs.Carbonated_data_set_storage.init_value)
(ctx, id) nf in
let? ctx :=
Storage.Sapling.Nullifiers_ordered.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
(ctx, id) pos nf in
return?
(ctx, (Int64.succ pos), (acc_size +Z (Z.of_int size_value))))
nfs (ctx, nf_start_pos, Z.zero) in
let? ctx :=
Storage.Sapling.Nullifiers_size.(Storage_sigs.Single_data_storage.update)
(ctx, id) nf_end_pos in
return? (ctx, size_value)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
#[bypass_check(guard)]
Definition get_from
(ctx : Raw_context.t) (id : Storage.Sapling.id) (offset : int64)
: M? (list Sapling.Nullifier.t) :=
let fix aux (acc_value : list Sapling.Nullifier.t) (pos : int64)
{struct pos} : M? (list Sapling.Nullifier.t) :=
let? function_parameter :=
Storage.Sapling.Nullifiers_ordered.(Storage_sigs.Non_iterable_indexed_data_storage.find)
(ctx, id) pos in
match function_parameter with
| None ⇒ return? (List.rev acc_value)
| Some c_value ⇒ aux (cons c_value acc_value) (Int64.succ pos)
end in
aux nil offset.
End Nullifiers.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module COMMITMENTS.
Record signature : Set := {
init_value : Raw_context.t → Storage.Sapling.id → Raw_context.t;
default_root : Sapling.Hash.t;
get_root :
Raw_context.t → Storage.Sapling.id → M? (Raw_context.t × Sapling.Hash.t);
add :
Raw_context.t → Storage.Sapling.id → list Sapling.Commitment.t →
int64 → M? (Raw_context.t × int);
get_from :
Raw_context.t → Storage.Sapling.id → int64 →
M? (list Sapling.Commitment.t);
}.
End COMMITMENTS.
Definition COMMITMENTS := COMMITMENTS.signature.
Module Commitments.
Module H := Sapling.Hash.
Definition pow2 (h_value : int) : int64 := Int64.shift_left 1 h_value.
Definition max_height : int := 32.
Definition max_size : int64 := pow2 max_height.
Definition assert_node (node_value : int64) (height : int) : M? unit :=
let first_of_height := pow2 (max_height -i height) in
let first_of_next_height := Int64.shift_left first_of_height 1 in
if
(node_value ≥i64 first_of_height) &&
(node_value <i64 first_of_next_height)
then
Error_monad.Result_syntax.return_unit
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition assert_height (height : int) : M? unit :=
if (height ≥i 0) && (height ≤i max_height) then
Error_monad.Result_syntax.return_unit
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition assert_pos (pos : int64) (height : int) : M? unit :=
if (pos ≥i64 0) && (pos ≤i64 (pow2 height)) then
Error_monad.Result_syntax.return_unit
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition default_root : H.t := H.uncommitted max_height.
Definition init_value
: Raw_context.t → Storage.Sapling.id → Raw_context.t :=
Storage.Sapling.commitments_init.
Definition get_root_height
(ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
(height : int) : M? (Raw_context.t × H.t) :=
let? '_ := assert_node node_value height in
let? '_ := assert_height height in
let? function_parameter :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctx, id) node_value in
match function_parameter with
| (ctx, None) ⇒
let hash_value := H.uncommitted height in
return? (ctx, hash_value)
| (ctx, Some hash_value) ⇒ return? (ctx, hash_value)
end.
Definition _left (node_value : int64) : int64 := node_value ×i64 2.
Definition _right (node_value : int64) : int64 := (node_value ×i64 2) +i64 1.
Fixpoint split_at {A : Set} (n_value : int64) (l_value : list A)
: list A × list A :=
if n_value =i64 0 then
(nil, l_value)
else
match l_value with
| [] ⇒ (nil, l_value)
| cons x_value xs ⇒
let '(l1, l2) := split_at (Int64.pred n_value) xs in
((cons x_value l1), l2)
end.
#[bypass_check(guard)]
Fixpoint insert
(ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
(height : int) (pos : int64) (cms : list Sapling.Commitment.t)
{struct height} : M? (Raw_context.t × int × H.t) :=
let? '_ := assert_node node_value height in
let? '_ := assert_height height in
let? '_ := assert_pos pos height in
match (height, cms) with
| (_, []) ⇒
let? '(ctx, h_value) := get_root_height ctx id node_value height in
return? (ctx, 0, h_value)
| (0, cons cm []) ⇒
let h_value := H.of_commitment cm in
let? '(ctx, size_value) :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
(ctx, id) node_value h_value in
return? (ctx, size_value, h_value)
| _ ⇒
let height := height -i 1 in
let? '(ctx, size_children, hl, hr) :=
if pos <i64 (pow2 height) then
let _at := (pow2 height) -i64 pos in
let '(cml, cmr) := split_at _at cms in
let? '(ctx, size_l, hl) :=
insert ctx id (_left node_value) height pos cml in
let? '(ctx, size_r, hr) :=
insert ctx id (_right node_value) height 0 cmr in
return? (ctx, (size_l +i size_r), hl, hr)
else
let? '(ctx, hl) := get_root_height ctx id (_left node_value) height in
let pos := pos -i64 (pow2 height) in
let? '(ctx, size_r, hr) :=
insert ctx id (_right node_value) height pos cms in
return? (ctx, size_r, hl, hr) in
let h_value := H.merkle_hash height hl hr in
let? '(ctx, size_value, _existing) :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(ctx, id) node_value h_value in
return? (ctx, (size_value +i size_children), h_value)
end.
#[bypass_check(guard)]
Fixpoint fold_from_height {A : Set}
(ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
(pos : int64) (f_value : A → Sapling.Hash.t → A) (acc_value : A)
(height : int) {struct height} : M? A :=
let? '_ := assert_node node_value height in
let? '_ := assert_height height in
let? '_ := assert_pos pos height in
let? function_parameter :=
Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctx, id) node_value in
match function_parameter with
| (_ctx, None) ⇒ return? acc_value
| (_ctx, Some h_value) ⇒
if height =i 0 then
return? (f_value acc_value h_value)
else
let full_value := pow2 (height -i 1) in
if pos <i64 full_value then
let? acc_value :=
fold_from_height ctx id (_left node_value) pos f_value acc_value
(height -i 1) in
fold_from_height ctx id (_right node_value) 0 f_value acc_value
(height -i 1)
else
let pos := pos -i64 full_value in
fold_from_height ctx id (_right node_value) pos f_value acc_value
(height -i 1)
end.
Definition root_node : int64 := 1.
Definition get_root (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? (Raw_context.t × H.t) := get_root_height ctx id root_node max_height.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(cms : list Sapling.Commitment.t) (pos : int64)
: M? (Raw_context.t × int) :=
let l_value := List.length cms in
if l_value ≤i 1000 then
let n' := pos +i64 (Int64.of_int l_value) in
if n' ≤i64 max_size then
let? '(ctx, size_value, _h) :=
insert ctx id root_node max_height pos cms in
return? (ctx, size_value)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition get_from
(ctx : Raw_context.t) (id : Storage.Sapling.id) (pos : int64)
: M? (list Sapling.Commitment.t) :=
let? l_value :=
fold_from_height ctx id root_node pos
(fun (acc_value : list Sapling.Commitment.t) ⇒
fun (c_value : Sapling.Hash.t) ⇒
cons (H.to_commitment c_value) acc_value) nil max_height in
return? (List.rev l_value).
(* Commitments *)
Definition module :=
{|
COMMITMENTS.init_value := init_value;
COMMITMENTS.default_root := default_root;
COMMITMENTS.get_root := get_root;
COMMITMENTS.add := add;
COMMITMENTS.get_from := get_from
|}.
End Commitments.
Definition Commitments : COMMITMENTS := Commitments.module.
Module Ciphertexts.
Definition init_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
: Raw_context.t := Storage.Sapling.ciphertexts_init ctx id.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(c_value : Sapling.Ciphertext.t) (pos : int64) : M? (Raw_context.t × int) :=
Storage.Sapling.Ciphertexts.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
(ctx, id) pos c_value.
#[bypass_check(guard)]
Definition get_from
(ctx : Raw_context.t) (id : Storage.Sapling.id) (offset : int64)
: M? (Raw_context.t × list Sapling.Ciphertext.t) :=
let fix aux (function_parameter : Raw_context.t × list Sapling.Ciphertext.t)
{struct function_parameter}
: int64 → M? (Raw_context.t × list Sapling.Ciphertext.t) :=
let '(ctx, acc_value) := function_parameter in
fun (pos : int64) ⇒
let? '(ctx, c_value) :=
Storage.Sapling.Ciphertexts.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(ctx, id) pos in
match c_value with
| None ⇒ return? (ctx, (List.rev acc_value))
| Some c_value ⇒ aux (ctx, (cons c_value acc_value)) (Int64.succ pos)
end in
aux (ctx, nil) offset.
End Ciphertexts.
Module Nullifiers.
Definition init_value
: Raw_context.t → Storage.Sapling.id → Raw_context.t :=
Storage.Sapling.nullifiers_init.
Definition size_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? int64 :=
Storage.Sapling.Nullifiers_size.(Storage_sigs.Single_data_storage.get)
(ctx, id).
Definition mem
(ctx : Raw_context.t) (id : Storage.Sapling.id) (nf : Sapling.Nullifier.t)
: M? (Raw_context.t × bool) :=
Storage.Sapling.Nullifiers_hashed.(Storage_sigs.Carbonated_data_set_storage.mem)
(ctx, id) nf.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(nfs : list Sapling.Nullifier.t) : M? (Raw_context.t × Z.t) :=
if (List.compare_length_with nfs 1000) ≤i 0 then
let? nf_start_pos := size_value ctx id in
let? '(ctx, nf_end_pos, size_value) :=
List.fold_right_es
(fun (nf : Sapling.Nullifier.t) ⇒
fun (function_parameter : Raw_context.t × int64 × Z.t) ⇒
let '(ctx, pos, acc_size) := function_parameter in
let? '(ctx, size_value) :=
Storage.Sapling.Nullifiers_hashed.(Storage_sigs.Carbonated_data_set_storage.init_value)
(ctx, id) nf in
let? ctx :=
Storage.Sapling.Nullifiers_ordered.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
(ctx, id) pos nf in
return?
(ctx, (Int64.succ pos), (acc_size +Z (Z.of_int size_value))))
nfs (ctx, nf_start_pos, Z.zero) in
let? ctx :=
Storage.Sapling.Nullifiers_size.(Storage_sigs.Single_data_storage.update)
(ctx, id) nf_end_pos in
return? (ctx, size_value)
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
#[bypass_check(guard)]
Definition get_from
(ctx : Raw_context.t) (id : Storage.Sapling.id) (offset : int64)
: M? (list Sapling.Nullifier.t) :=
let fix aux (acc_value : list Sapling.Nullifier.t) (pos : int64)
{struct pos} : M? (list Sapling.Nullifier.t) :=
let? function_parameter :=
Storage.Sapling.Nullifiers_ordered.(Storage_sigs.Non_iterable_indexed_data_storage.find)
(ctx, id) pos in
match function_parameter with
| None ⇒ return? (List.rev acc_value)
| Some c_value ⇒ aux (cons c_value acc_value) (Int64.succ pos)
end in
aux nil offset.
End Nullifiers.
Bounded queue of roots. The full size is initialized with the default
uncommitted root, that's why roots storage doesn't need to be carbonated.
A maximum of one new root is added per protocol level.
If multiple transactions for the same shielded pool are processed during the
same contract call or several calls in the same block, only the last root
will be stored.
This property prevents transactions in the same block from depending on each
other and guarantees that a transaction will be valid for a least two hours
(hence the 120 size) after being forged.
Module Roots.
Definition size_value : int32 := 120.
Definition get (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? Sapling.Hash.t :=
let? pos :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
in
Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.get)
(ctx, id) pos.
#[bypass_check(guard)]
Definition init_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? Raw_context.t :=
let fix aux (ctx : Raw_context.t) (pos : int32) {struct pos}
: M? Raw_context.t :=
if pos <i32 0 then
return? ctx
else
let? ctx :=
Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
(ctx, id) pos Commitments.(COMMITMENTS.default_root) in
aux ctx (Int32.pred pos) in
let? ctx := aux ctx (Int32.pred size_value) in
let? ctx :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.init_value)
(ctx, id) 0 in
let level := (Raw_context.current_level ctx).(Level_repr.t.level) in
Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.init_value)
(ctx, id) level.
#[bypass_check(guard)]
Definition mem
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(root_value : Sapling.Hash.t) : M? bool :=
let? start_pos :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
in
let fix aux (pos : int32) {struct pos} : M? bool :=
let? hash_value :=
Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.get)
(ctx, id) pos in
if (Sapling.Hash.compare hash_value root_value) =i 0 then
return? true
else
let pos := Int32.pred pos in
let pos :=
if pos <i32 0 then
Int32.pred size_value
else
pos in
if pos =i32 start_pos then
return? false
else
aux pos in
aux start_pos.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(root_value : Sapling.Hash.t) : M? Raw_context.t :=
let? pos :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
in
let level := (Raw_context.current_level ctx).(Level_repr.t.level) in
let? stored_level :=
Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.get)
(ctx, id) in
if Raw_level_repr.op_eq stored_level level then
Error_monad.op_gtpipeeq
(Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.add)
(ctx, id) pos root_value) Error_monad.ok
else
let? ctx :=
Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.update)
(ctx, id) level in
let pos := Int32.rem (Int32.succ pos) size_value in
let? ctx :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.update)
(ctx, id) pos in
Error_monad.op_gtpipeeq
(Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.add)
(ctx, id) pos root_value) Error_monad.ok.
End Roots.
Definition size_value : int32 := 120.
Definition get (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? Sapling.Hash.t :=
let? pos :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
in
Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.get)
(ctx, id) pos.
#[bypass_check(guard)]
Definition init_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? Raw_context.t :=
let fix aux (ctx : Raw_context.t) (pos : int32) {struct pos}
: M? Raw_context.t :=
if pos <i32 0 then
return? ctx
else
let? ctx :=
Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
(ctx, id) pos Commitments.(COMMITMENTS.default_root) in
aux ctx (Int32.pred pos) in
let? ctx := aux ctx (Int32.pred size_value) in
let? ctx :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.init_value)
(ctx, id) 0 in
let level := (Raw_context.current_level ctx).(Level_repr.t.level) in
Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.init_value)
(ctx, id) level.
#[bypass_check(guard)]
Definition mem
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(root_value : Sapling.Hash.t) : M? bool :=
let? start_pos :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
in
let fix aux (pos : int32) {struct pos} : M? bool :=
let? hash_value :=
Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.get)
(ctx, id) pos in
if (Sapling.Hash.compare hash_value root_value) =i 0 then
return? true
else
let pos := Int32.pred pos in
let pos :=
if pos <i32 0 then
Int32.pred size_value
else
pos in
if pos =i32 start_pos then
return? false
else
aux pos in
aux start_pos.
Definition add
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(root_value : Sapling.Hash.t) : M? Raw_context.t :=
let? pos :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
in
let level := (Raw_context.current_level ctx).(Level_repr.t.level) in
let? stored_level :=
Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.get)
(ctx, id) in
if Raw_level_repr.op_eq stored_level level then
Error_monad.op_gtpipeeq
(Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.add)
(ctx, id) pos root_value) Error_monad.ok
else
let? ctx :=
Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.update)
(ctx, id) level in
let pos := Int32.rem (Int32.succ pos) size_value in
let? ctx :=
Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.update)
(ctx, id) pos in
Error_monad.op_gtpipeeq
(Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.add)
(ctx, id) pos root_value) Error_monad.ok.
End Roots.
This type links the permanent state stored in the context at the specified
id together with the ephemeral diff managed by the Michelson
interpreter. After a successful execution the diff can be applied to update
the state at id. The first time a state is created its id is None, one will
be assigned after the first application.
Module state.
Record record : Set := Build {
id : option Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t);
diff : Sapling_repr.diff;
memo_size : Sapling_repr.Memo_size.t;
}.
Definition with_id id (r : record) :=
Build id r.(diff) r.(memo_size).
Definition with_diff diff (r : record) :=
Build r.(id) diff r.(memo_size).
Definition with_memo_size memo_size (r : record) :=
Build r.(id) r.(diff) memo_size.
End state.
Definition state := state.record.
Definition empty_diff : Sapling_repr.diff :=
{| Sapling_repr.diff.commitments_and_ciphertexts := nil;
Sapling_repr.diff.nullifiers := nil; |}.
Definition empty_state
(id : option Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
(memo_size : Sapling_repr.Memo_size.t) (function_parameter : unit) : state :=
let '_ := function_parameter in
{| state.id := id; state.diff := empty_diff; state.memo_size := memo_size; |}.
Record record : Set := Build {
id : option Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t);
diff : Sapling_repr.diff;
memo_size : Sapling_repr.Memo_size.t;
}.
Definition with_id id (r : record) :=
Build id r.(diff) r.(memo_size).
Definition with_diff diff (r : record) :=
Build r.(id) diff r.(memo_size).
Definition with_memo_size memo_size (r : record) :=
Build r.(id) r.(diff) memo_size.
End state.
Definition state := state.record.
Definition empty_diff : Sapling_repr.diff :=
{| Sapling_repr.diff.commitments_and_ciphertexts := nil;
Sapling_repr.diff.nullifiers := nil; |}.
Definition empty_state
(id : option Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
(memo_size : Sapling_repr.Memo_size.t) (function_parameter : unit) : state :=
let '_ := function_parameter in
{| state.id := id; state.diff := empty_diff; state.memo_size := memo_size; |}.
Returns a state from an existing id.
Definition state_from_id (ctxt : Raw_context.t) (id : Storage.Sapling.id)
: M? (state × Raw_context.t) :=
let? memo_size :=
Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.get) (ctxt, id)
in
return?
({| state.id := Some id; state.diff := empty_diff;
state.memo_size := memo_size; |}, ctxt).
Definition rpc_arg : RPC_arg.t Storage.Sapling.id := Storage.Sapling.rpc_arg.
Definition get_memo_size (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? int :=
Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.get) (ctx, id).
Definition init_value
(ctx : Raw_context.t) (id : Storage.Sapling.id) (memo_size : int)
: M? Raw_context.t :=
let ctx :=
Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.add) (ctx, id)
memo_size in
let ctx :=
Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.add)
(ctx, id) Int64.zero in
let ctx := Commitments.(COMMITMENTS.init_value) ctx id in
let ctx := Nullifiers.init_value ctx id in
let? ctx := Roots.init_value ctx id in
Error_monad.op_gtpipeeq (Ciphertexts.init_value ctx id) Error_monad.ok.
Definition sapling_apply_diff_cost (inputs : int) (outputs : int)
: Saturation_repr.t :=
Saturation_repr.add (Saturation_repr.safe_int 1300000)
(Saturation_repr.add
(Saturation_repr.scale_fast (Saturation_repr.mul_safe_of_int_exn 5000)
(Saturation_repr.safe_int inputs))
(Saturation_repr.scale_fast (Saturation_repr.mul_safe_of_int_exn 55000)
(Saturation_repr.safe_int outputs))).
: M? (state × Raw_context.t) :=
let? memo_size :=
Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.get) (ctxt, id)
in
return?
({| state.id := Some id; state.diff := empty_diff;
state.memo_size := memo_size; |}, ctxt).
Definition rpc_arg : RPC_arg.t Storage.Sapling.id := Storage.Sapling.rpc_arg.
Definition get_memo_size (ctx : Raw_context.t) (id : Storage.Sapling.id)
: M? int :=
Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.get) (ctx, id).
Definition init_value
(ctx : Raw_context.t) (id : Storage.Sapling.id) (memo_size : int)
: M? Raw_context.t :=
let ctx :=
Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.add) (ctx, id)
memo_size in
let ctx :=
Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.add)
(ctx, id) Int64.zero in
let ctx := Commitments.(COMMITMENTS.init_value) ctx id in
let ctx := Nullifiers.init_value ctx id in
let? ctx := Roots.init_value ctx id in
Error_monad.op_gtpipeeq (Ciphertexts.init_value ctx id) Error_monad.ok.
Definition sapling_apply_diff_cost (inputs : int) (outputs : int)
: Saturation_repr.t :=
Saturation_repr.add (Saturation_repr.safe_int 1300000)
(Saturation_repr.add
(Saturation_repr.scale_fast (Saturation_repr.mul_safe_of_int_exn 5000)
(Saturation_repr.safe_int inputs))
(Saturation_repr.scale_fast (Saturation_repr.mul_safe_of_int_exn 55000)
(Saturation_repr.safe_int outputs))).
Applies a diff to a state id stored in the context. Updates Commitments,
Ciphertexts and Nullifiers using the diff and updates the Roots using the
new Commitments tree.
Definition apply_diff
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(diff_value : Sapling_repr.diff) : M? (Raw_context.t × Z.t) :=
let nb_commitments :=
List.length diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) in
let nb_nullifiers := List.length diff_value.(Sapling_repr.diff.nullifiers) in
let sapling_cost := sapling_apply_diff_cost nb_nullifiers nb_commitments in
let? ctx := Raw_context.consume_gas ctx sapling_cost in
let? cm_start_pos :=
Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.get)
(ctx, id) in
let cms :=
List.rev_map Pervasives.fst
diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) in
let? '(ctx, size_value) :=
Commitments.(COMMITMENTS.add) ctx id cms cm_start_pos in
let? ctx :=
Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.update)
(ctx, id) (cm_start_pos +i64 (Int64.of_int nb_commitments)) in
let? '(ctx, _ct_end_pos, size_value) :=
List.fold_right_es
(fun (function_parameter : Sapling.Commitment.t × Sapling.Ciphertext.t) ⇒
let '(_cm, cp) := function_parameter in
fun (function_parameter : Raw_context.t × int64 × Z.t) ⇒
let '(ctx, pos, acc_size) := function_parameter in
let? '(ctx, size_value) := Ciphertexts.add ctx id cp pos in
return? (ctx, (Int64.succ pos), (acc_size +Z (Z.of_int size_value))))
diff_value.(Sapling_repr.diff.commitments_and_ciphertexts)
(ctx, cm_start_pos, (Z.of_int size_value)) in
let? '(ctx, size_nf) :=
Nullifiers.add ctx id diff_value.(Sapling_repr.diff.nullifiers) in
let size_value := size_value +Z size_nf in
match diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) with
| [] ⇒ return? (ctx, size_value)
| cons _ _ ⇒
let? '(ctx, root_value) := Commitments.(COMMITMENTS.get_root) ctx id in
let? ctx := Roots.add ctx id root_value in
return? (ctx, size_value)
end.
Definition add (function_parameter : state)
: list (Sapling.Commitment.t × Sapling.Ciphertext.t) → state :=
let '{|
state.id := id;
state.diff := diff_value;
state.memo_size := memo_size
|} := function_parameter in
fun (cm_cipher_list : list (Sapling.Commitment.t × Sapling.Ciphertext.t)) ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(List.for_all
(fun (function_parameter :
Sapling.Commitment.t × Sapling.Ciphertext.t) ⇒
let '(_cm, cipher) := function_parameter in
(Sapling.Ciphertext.get_memo_size cipher) =i memo_size)
cm_cipher_list) in
{| state.id := id;
state.diff :=
Sapling_repr.diff.with_commitments_and_ciphertexts
(Pervasives.op_at (List.rev cm_cipher_list)
diff_value.(Sapling_repr.diff.commitments_and_ciphertexts))
diff_value; state.memo_size := memo_size; |}.
Definition root_mem (ctx : Raw_context.t) (function_parameter : state)
: Sapling.Hash.t → M? bool :=
let '{| state.id := id |} := function_parameter in
fun (tested_root : Sapling.Hash.t) ⇒
match id with
| Some id ⇒ Roots.mem ctx id tested_root
| None ⇒
return?
((Sapling.Hash.compare tested_root
Commitments.(COMMITMENTS.default_root)) =i 0)
end.
Definition nullifiers_mem (ctx : Raw_context.t) (function_parameter : state)
: Sapling.Nullifier.t → M? (Raw_context.t × bool) :=
let '{| state.id := id; state.diff := diff_value |} := function_parameter in
fun (nf : Sapling.Nullifier.t) ⇒
let exists_in_diff :=
List._exists
(fun (v_value : Sapling.Nullifier.t) ⇒
(Sapling.Nullifier.compare nf v_value) =i 0)
diff_value.(Sapling_repr.diff.nullifiers) in
if exists_in_diff then
return? (ctx, true)
else
match id with
| None ⇒ return? (ctx, false)
| Some id ⇒ Nullifiers.mem ctx id nf
end.
Definition nullifiers_add (function_parameter : state)
: Sapling.Nullifier.t → state :=
let '{|
state.id := id;
state.diff := diff_value;
state.memo_size := memo_size
|} := function_parameter in
fun (nf : Sapling.Nullifier.t) ⇒
{| state.id := id;
state.diff :=
Sapling_repr.diff.with_nullifiers
(cons nf diff_value.(Sapling_repr.diff.nullifiers)) diff_value;
state.memo_size := memo_size; |}.
Definition root : Set := Sapling.Hash.t.
Definition root_encoding : Data_encoding.t Sapling.Hash.t :=
Sapling.Hash.encoding.
Definition get_diff
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(op_staroptstar : option int64)
: option int64 → unit → M? (Sapling.Hash.t × Sapling_repr.diff) :=
let offset_commitment :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ 0
end in
fun (op_staroptstar : option int64) ⇒
let offset_nullifier :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ 0
end in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
if
Pervasives.not
((Sapling.Commitment.valid_position offset_commitment) &&
(Sapling.Commitment.valid_position offset_nullifier))
then
Pervasives.failwith "Invalid argument."
else
let? commitments :=
Commitments.(COMMITMENTS.get_from) ctx id offset_commitment in
let? root_value := Roots.get ctx id in
let? nullifiers := Nullifiers.get_from ctx id offset_nullifier in
let? '(_ctx, ciphertexts) :=
Ciphertexts.get_from ctx id offset_commitment in
match List.combine tt commitments ciphertexts with
| Pervasives.Error _ ⇒
return? (Pervasives.failwith "Invalid argument.")
| Pervasives.Ok commitments_and_ciphertexts ⇒
return?
(root_value,
{|
Sapling_repr.diff.commitments_and_ciphertexts :=
commitments_and_ciphertexts;
Sapling_repr.diff.nullifiers := nullifiers; |})
end.
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(diff_value : Sapling_repr.diff) : M? (Raw_context.t × Z.t) :=
let nb_commitments :=
List.length diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) in
let nb_nullifiers := List.length diff_value.(Sapling_repr.diff.nullifiers) in
let sapling_cost := sapling_apply_diff_cost nb_nullifiers nb_commitments in
let? ctx := Raw_context.consume_gas ctx sapling_cost in
let? cm_start_pos :=
Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.get)
(ctx, id) in
let cms :=
List.rev_map Pervasives.fst
diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) in
let? '(ctx, size_value) :=
Commitments.(COMMITMENTS.add) ctx id cms cm_start_pos in
let? ctx :=
Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.update)
(ctx, id) (cm_start_pos +i64 (Int64.of_int nb_commitments)) in
let? '(ctx, _ct_end_pos, size_value) :=
List.fold_right_es
(fun (function_parameter : Sapling.Commitment.t × Sapling.Ciphertext.t) ⇒
let '(_cm, cp) := function_parameter in
fun (function_parameter : Raw_context.t × int64 × Z.t) ⇒
let '(ctx, pos, acc_size) := function_parameter in
let? '(ctx, size_value) := Ciphertexts.add ctx id cp pos in
return? (ctx, (Int64.succ pos), (acc_size +Z (Z.of_int size_value))))
diff_value.(Sapling_repr.diff.commitments_and_ciphertexts)
(ctx, cm_start_pos, (Z.of_int size_value)) in
let? '(ctx, size_nf) :=
Nullifiers.add ctx id diff_value.(Sapling_repr.diff.nullifiers) in
let size_value := size_value +Z size_nf in
match diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) with
| [] ⇒ return? (ctx, size_value)
| cons _ _ ⇒
let? '(ctx, root_value) := Commitments.(COMMITMENTS.get_root) ctx id in
let? ctx := Roots.add ctx id root_value in
return? (ctx, size_value)
end.
Definition add (function_parameter : state)
: list (Sapling.Commitment.t × Sapling.Ciphertext.t) → state :=
let '{|
state.id := id;
state.diff := diff_value;
state.memo_size := memo_size
|} := function_parameter in
fun (cm_cipher_list : list (Sapling.Commitment.t × Sapling.Ciphertext.t)) ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(List.for_all
(fun (function_parameter :
Sapling.Commitment.t × Sapling.Ciphertext.t) ⇒
let '(_cm, cipher) := function_parameter in
(Sapling.Ciphertext.get_memo_size cipher) =i memo_size)
cm_cipher_list) in
{| state.id := id;
state.diff :=
Sapling_repr.diff.with_commitments_and_ciphertexts
(Pervasives.op_at (List.rev cm_cipher_list)
diff_value.(Sapling_repr.diff.commitments_and_ciphertexts))
diff_value; state.memo_size := memo_size; |}.
Definition root_mem (ctx : Raw_context.t) (function_parameter : state)
: Sapling.Hash.t → M? bool :=
let '{| state.id := id |} := function_parameter in
fun (tested_root : Sapling.Hash.t) ⇒
match id with
| Some id ⇒ Roots.mem ctx id tested_root
| None ⇒
return?
((Sapling.Hash.compare tested_root
Commitments.(COMMITMENTS.default_root)) =i 0)
end.
Definition nullifiers_mem (ctx : Raw_context.t) (function_parameter : state)
: Sapling.Nullifier.t → M? (Raw_context.t × bool) :=
let '{| state.id := id; state.diff := diff_value |} := function_parameter in
fun (nf : Sapling.Nullifier.t) ⇒
let exists_in_diff :=
List._exists
(fun (v_value : Sapling.Nullifier.t) ⇒
(Sapling.Nullifier.compare nf v_value) =i 0)
diff_value.(Sapling_repr.diff.nullifiers) in
if exists_in_diff then
return? (ctx, true)
else
match id with
| None ⇒ return? (ctx, false)
| Some id ⇒ Nullifiers.mem ctx id nf
end.
Definition nullifiers_add (function_parameter : state)
: Sapling.Nullifier.t → state :=
let '{|
state.id := id;
state.diff := diff_value;
state.memo_size := memo_size
|} := function_parameter in
fun (nf : Sapling.Nullifier.t) ⇒
{| state.id := id;
state.diff :=
Sapling_repr.diff.with_nullifiers
(cons nf diff_value.(Sapling_repr.diff.nullifiers)) diff_value;
state.memo_size := memo_size; |}.
Definition root : Set := Sapling.Hash.t.
Definition root_encoding : Data_encoding.t Sapling.Hash.t :=
Sapling.Hash.encoding.
Definition get_diff
(ctx : Raw_context.t) (id : Storage.Sapling.id)
(op_staroptstar : option int64)
: option int64 → unit → M? (Sapling.Hash.t × Sapling_repr.diff) :=
let offset_commitment :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ 0
end in
fun (op_staroptstar : option int64) ⇒
let offset_nullifier :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ 0
end in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
if
Pervasives.not
((Sapling.Commitment.valid_position offset_commitment) &&
(Sapling.Commitment.valid_position offset_nullifier))
then
Pervasives.failwith "Invalid argument."
else
let? commitments :=
Commitments.(COMMITMENTS.get_from) ctx id offset_commitment in
let? root_value := Roots.get ctx id in
let? nullifiers := Nullifiers.get_from ctx id offset_nullifier in
let? '(_ctx, ciphertexts) :=
Ciphertexts.get_from ctx id offset_commitment in
match List.combine tt commitments ciphertexts with
| Pervasives.Error _ ⇒
return? (Pervasives.failwith "Invalid argument.")
| Pervasives.Ok commitments_and_ciphertexts ⇒
return?
(root_value,
{|
Sapling_repr.diff.commitments_and_ciphertexts :=
commitments_and_ciphertexts;
Sapling_repr.diff.nullifiers := nullifiers; |})
end.