🍃 Sapling.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.Int64.
Module Ciphertext.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
Parameter get_memo_size : t → int.
End Ciphertext.
Module Commitment.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
Parameter valid_position : int64 → bool.
End Commitment.
Module CV.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
End CV.
Module Hash.
Parameter t : Set.
Parameter compare : t → t → int.
Parameter encoding : Data_encoding.t t.
Parameter to_bytes : t → Bytes.t.
Parameter of_bytes_exn : Bytes.t → t.
Parameter uncommitted : int → t.
Parameter merkle_hash : int → t → t → t.
Parameter of_commitment : Commitment.t → t.
Parameter to_commitment : t → Commitment.t.
End Hash.
Module Nullifier.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
Parameter compare : t → t → int.
End Nullifier.
Module UTXO.
Parameter rk : Set.
Parameter spend_proof : Set.
Parameter spend_sig : Set.
Parameter output_proof : Set.
Module input.
Record record : Set := Build {
cv : CV.t;
nf : Nullifier.t;
rk : rk;
proof_i : spend_proof;
signature : spend_sig }.
Definition with_cv cv (r : record) :=
Build cv r.(nf) r.(rk) r.(proof_i) r.(signature).
Definition with_nf nf (r : record) :=
Build r.(cv) nf r.(rk) r.(proof_i) r.(signature).
Definition with_rk rk (r : record) :=
Build r.(cv) r.(nf) rk r.(proof_i) r.(signature).
Definition with_proof_i proof_i (r : record) :=
Build r.(cv) r.(nf) r.(rk) proof_i r.(signature).
Definition with_signature signature (r : record) :=
Build r.(cv) r.(nf) r.(rk) r.(proof_i) signature.
End input.
Definition input := input.record.
Parameter input_encoding : Data_encoding.t input.
Module output.
Record record : Set := Build {
cm : Commitment.t;
proof_o : output_proof;
ciphertext : Ciphertext.t }.
Definition with_cm cm (r : record) :=
Build cm r.(proof_o) r.(ciphertext).
Definition with_proof_o proof_o (r : record) :=
Build r.(cm) proof_o r.(ciphertext).
Definition with_ciphertext ciphertext (r : record) :=
Build r.(cm) r.(proof_o) ciphertext.
End output.
Definition output := output.record.
Parameter output_encoding : Data_encoding.t output.
Parameter binding_sig : Set.
Module transaction.
Record record : Set := Build {
inputs : list input;
outputs : list output;
binding_sig : binding_sig;
balance : Int64.t;
root : Hash.t;
bound_data : string }.
Definition with_inputs inputs (r : record) :=
Build inputs r.(outputs) r.(binding_sig) r.(balance) r.(root)
r.(bound_data).
Definition with_outputs outputs (r : record) :=
Build r.(inputs) outputs r.(binding_sig) r.(balance) r.(root)
r.(bound_data).
Definition with_binding_sig binding_sig (r : record) :=
Build r.(inputs) r.(outputs) binding_sig r.(balance) r.(root)
r.(bound_data).
Definition with_balance balance (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) balance r.(root)
r.(bound_data).
Definition with_root root (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) root
r.(bound_data).
Definition with_bound_data bound_data (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) r.(root)
bound_data.
End transaction.
Definition transaction := transaction.record.
Parameter transaction_encoding : Data_encoding.t transaction.
Parameter binding_sig_encoding : Data_encoding.t binding_sig.
Module Legacy.
Definition transaction_new : Set := transaction.
Module transaction.
Record record : Set := Build {
inputs : list input;
outputs : list output;
binding_sig : binding_sig;
balance : Int64.t;
root : Hash.t }.
Definition with_inputs inputs (r : record) :=
Build inputs r.(outputs) r.(binding_sig) r.(balance) r.(root).
Definition with_outputs outputs (r : record) :=
Build r.(inputs) outputs r.(binding_sig) r.(balance) r.(root).
Definition with_binding_sig binding_sig (r : record) :=
Build r.(inputs) r.(outputs) binding_sig r.(balance) r.(root).
Definition with_balance balance (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) balance r.(root).
Definition with_root root (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) root.
End transaction.
Definition transaction := transaction.record.
Parameter transaction_encoding : Data_encoding.t transaction.
Parameter cast : transaction → transaction_new.
End Legacy.
End UTXO.
Module Verification.
Parameter t : Set.
Parameter with_verification_ctx : ∀ {a : Set}, (t → a) → a.
Parameter check_spend : t → UTXO.input → Hash.t → string → bool.
Parameter check_output : t → UTXO.output → bool.
Parameter final_check : t → UTXO.transaction → string → bool.
End Verification.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.Int64.
Module Ciphertext.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
Parameter get_memo_size : t → int.
End Ciphertext.
Module Commitment.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
Parameter valid_position : int64 → bool.
End Commitment.
Module CV.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
End CV.
Module Hash.
Parameter t : Set.
Parameter compare : t → t → int.
Parameter encoding : Data_encoding.t t.
Parameter to_bytes : t → Bytes.t.
Parameter of_bytes_exn : Bytes.t → t.
Parameter uncommitted : int → t.
Parameter merkle_hash : int → t → t → t.
Parameter of_commitment : Commitment.t → t.
Parameter to_commitment : t → Commitment.t.
End Hash.
Module Nullifier.
Parameter t : Set.
Parameter encoding : Data_encoding.t t.
Parameter compare : t → t → int.
End Nullifier.
Module UTXO.
Parameter rk : Set.
Parameter spend_proof : Set.
Parameter spend_sig : Set.
Parameter output_proof : Set.
Module input.
Record record : Set := Build {
cv : CV.t;
nf : Nullifier.t;
rk : rk;
proof_i : spend_proof;
signature : spend_sig }.
Definition with_cv cv (r : record) :=
Build cv r.(nf) r.(rk) r.(proof_i) r.(signature).
Definition with_nf nf (r : record) :=
Build r.(cv) nf r.(rk) r.(proof_i) r.(signature).
Definition with_rk rk (r : record) :=
Build r.(cv) r.(nf) rk r.(proof_i) r.(signature).
Definition with_proof_i proof_i (r : record) :=
Build r.(cv) r.(nf) r.(rk) proof_i r.(signature).
Definition with_signature signature (r : record) :=
Build r.(cv) r.(nf) r.(rk) r.(proof_i) signature.
End input.
Definition input := input.record.
Parameter input_encoding : Data_encoding.t input.
Module output.
Record record : Set := Build {
cm : Commitment.t;
proof_o : output_proof;
ciphertext : Ciphertext.t }.
Definition with_cm cm (r : record) :=
Build cm r.(proof_o) r.(ciphertext).
Definition with_proof_o proof_o (r : record) :=
Build r.(cm) proof_o r.(ciphertext).
Definition with_ciphertext ciphertext (r : record) :=
Build r.(cm) r.(proof_o) ciphertext.
End output.
Definition output := output.record.
Parameter output_encoding : Data_encoding.t output.
Parameter binding_sig : Set.
Module transaction.
Record record : Set := Build {
inputs : list input;
outputs : list output;
binding_sig : binding_sig;
balance : Int64.t;
root : Hash.t;
bound_data : string }.
Definition with_inputs inputs (r : record) :=
Build inputs r.(outputs) r.(binding_sig) r.(balance) r.(root)
r.(bound_data).
Definition with_outputs outputs (r : record) :=
Build r.(inputs) outputs r.(binding_sig) r.(balance) r.(root)
r.(bound_data).
Definition with_binding_sig binding_sig (r : record) :=
Build r.(inputs) r.(outputs) binding_sig r.(balance) r.(root)
r.(bound_data).
Definition with_balance balance (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) balance r.(root)
r.(bound_data).
Definition with_root root (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) root
r.(bound_data).
Definition with_bound_data bound_data (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) r.(root)
bound_data.
End transaction.
Definition transaction := transaction.record.
Parameter transaction_encoding : Data_encoding.t transaction.
Parameter binding_sig_encoding : Data_encoding.t binding_sig.
Module Legacy.
Definition transaction_new : Set := transaction.
Module transaction.
Record record : Set := Build {
inputs : list input;
outputs : list output;
binding_sig : binding_sig;
balance : Int64.t;
root : Hash.t }.
Definition with_inputs inputs (r : record) :=
Build inputs r.(outputs) r.(binding_sig) r.(balance) r.(root).
Definition with_outputs outputs (r : record) :=
Build r.(inputs) outputs r.(binding_sig) r.(balance) r.(root).
Definition with_binding_sig binding_sig (r : record) :=
Build r.(inputs) r.(outputs) binding_sig r.(balance) r.(root).
Definition with_balance balance (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) balance r.(root).
Definition with_root root (r : record) :=
Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) root.
End transaction.
Definition transaction := transaction.record.
Parameter transaction_encoding : Data_encoding.t transaction.
Parameter cast : transaction → transaction_new.
End Legacy.
End UTXO.
Module Verification.
Parameter t : Set.
Parameter with_verification_ctx : ∀ {a : Set}, (t → a) → a.
Parameter check_spend : t → UTXO.input → Hash.t → string → bool.
Parameter check_output : t → UTXO.output → bool.
Parameter final_check : t → UTXO.transaction → string → bool.
End Verification.