🥷 Sapling_validator.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.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Fixpoint check_and_update_nullifiers
(ctxt : Raw_context.t) (state_value : Sapling_storage.state)
(inputs : list Sapling.UTXO.input)
: M? (Raw_context.t × option Sapling_storage.state) :=
match inputs with
| [] ⇒ return? (ctxt, (Some state_value))
| cons input inputs ⇒
let? function_parameter :=
Sapling_storage.nullifiers_mem ctxt state_value
input.(Sapling.UTXO.input.nf) in
match function_parameter with
| (ctxt, true) ⇒ return? (ctxt, None)
| (ctxt, false) ⇒
let state_value :=
Sapling_storage.nullifiers_add state_value input.(Sapling.UTXO.input.nf)
in
check_and_update_nullifiers ctxt state_value inputs
end
end.
Definition verify_update
(ctxt : Raw_context.t) (state_value : Sapling_storage.state)
(transaction : Sapling_repr.transaction) (key_value : string)
: M? (Raw_context.t × option (Int64.t × Sapling_storage.state)) :=
if
((List.compare_length_with transaction.(Sapling.UTXO.transaction.inputs)
5208) ≤i 0) &&
((List.compare_length_with transaction.(Sapling.UTXO.transaction.outputs)
2019) ≤i 0)
then
let pass :=
List.for_all
(fun (output : Sapling.UTXO.output) ⇒
(Sapling.Ciphertext.get_memo_size
output.(Sapling.UTXO.output.ciphertext)) =i
state_value.(Sapling_storage.state.memo_size))
transaction.(Sapling.UTXO.transaction.outputs) in
if Pervasives.not pass then
return? (ctxt, None)
else
let? pass :=
Sapling_storage.root_mem ctxt state_value
transaction.(Sapling.UTXO.transaction.root) in
if Pervasives.not pass then
return? (ctxt, None)
else
let? function_parameter :=
check_and_update_nullifiers ctxt state_value
transaction.(Sapling.UTXO.transaction.inputs) in
match function_parameter with
| (ctxt, None) ⇒ return? (ctxt, None)
| (ctxt, Some state_value) ⇒
return?
(Sapling.Verification.with_verification_ctx
(fun (vctx : Sapling.Verification.t) ⇒
let pass :=
List.for_all
(fun (output : Sapling.UTXO.output) ⇒
Sapling.Verification.check_output vctx output)
transaction.(Sapling.UTXO.transaction.outputs) in
if Pervasives.not pass then
(ctxt, None)
else
let pass :=
List.for_all
(fun (input : Sapling.UTXO.input) ⇒
Sapling.Verification.check_spend vctx input
transaction.(Sapling.UTXO.transaction.root) key_value)
transaction.(Sapling.UTXO.transaction.inputs) in
if Pervasives.not pass then
(ctxt, None)
else
let pass :=
Sapling.Verification.final_check vctx transaction
key_value in
if Pervasives.not pass then
(ctxt, None)
else
let list_to_add :=
List.map
(fun (output : Sapling.UTXO.output) ⇒
(output.(Sapling.UTXO.output.cm),
output.(Sapling.UTXO.output.ciphertext)))
transaction.(Sapling.UTXO.transaction.outputs) in
let state_value :=
Sapling_storage.add state_value list_to_add in
(ctxt,
(Some
(transaction.(Sapling.UTXO.transaction.balance),
state_value)))))
end
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Fixpoint check_and_update_nullifiers
(ctxt : Raw_context.t) (state_value : Sapling_storage.state)
(inputs : list Sapling.UTXO.input)
: M? (Raw_context.t × option Sapling_storage.state) :=
match inputs with
| [] ⇒ return? (ctxt, (Some state_value))
| cons input inputs ⇒
let? function_parameter :=
Sapling_storage.nullifiers_mem ctxt state_value
input.(Sapling.UTXO.input.nf) in
match function_parameter with
| (ctxt, true) ⇒ return? (ctxt, None)
| (ctxt, false) ⇒
let state_value :=
Sapling_storage.nullifiers_add state_value input.(Sapling.UTXO.input.nf)
in
check_and_update_nullifiers ctxt state_value inputs
end
end.
Definition verify_update
(ctxt : Raw_context.t) (state_value : Sapling_storage.state)
(transaction : Sapling_repr.transaction) (key_value : string)
: M? (Raw_context.t × option (Int64.t × Sapling_storage.state)) :=
if
((List.compare_length_with transaction.(Sapling.UTXO.transaction.inputs)
5208) ≤i 0) &&
((List.compare_length_with transaction.(Sapling.UTXO.transaction.outputs)
2019) ≤i 0)
then
let pass :=
List.for_all
(fun (output : Sapling.UTXO.output) ⇒
(Sapling.Ciphertext.get_memo_size
output.(Sapling.UTXO.output.ciphertext)) =i
state_value.(Sapling_storage.state.memo_size))
transaction.(Sapling.UTXO.transaction.outputs) in
if Pervasives.not pass then
return? (ctxt, None)
else
let? pass :=
Sapling_storage.root_mem ctxt state_value
transaction.(Sapling.UTXO.transaction.root) in
if Pervasives.not pass then
return? (ctxt, None)
else
let? function_parameter :=
check_and_update_nullifiers ctxt state_value
transaction.(Sapling.UTXO.transaction.inputs) in
match function_parameter with
| (ctxt, None) ⇒ return? (ctxt, None)
| (ctxt, Some state_value) ⇒
return?
(Sapling.Verification.with_verification_ctx
(fun (vctx : Sapling.Verification.t) ⇒
let pass :=
List.for_all
(fun (output : Sapling.UTXO.output) ⇒
Sapling.Verification.check_output vctx output)
transaction.(Sapling.UTXO.transaction.outputs) in
if Pervasives.not pass then
(ctxt, None)
else
let pass :=
List.for_all
(fun (input : Sapling.UTXO.input) ⇒
Sapling.Verification.check_spend vctx input
transaction.(Sapling.UTXO.transaction.root) key_value)
transaction.(Sapling.UTXO.transaction.inputs) in
if Pervasives.not pass then
(ctxt, None)
else
let pass :=
Sapling.Verification.final_check vctx transaction
key_value in
if Pervasives.not pass then
(ctxt, None)
else
let list_to_add :=
List.map
(fun (output : Sapling.UTXO.output) ⇒
(output.(Sapling.UTXO.output.cm),
output.(Sapling.UTXO.output.ciphertext)))
transaction.(Sapling.UTXO.transaction.outputs) in
let state_value :=
Sapling_storage.add state_value list_to_add in
(ctxt,
(Some
(transaction.(Sapling.UTXO.transaction.balance),
state_value)))))
end
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).