Skip to main content

🍃 Sapling.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Bytes.
Require Proto_alpha.Environment.Data_encoding.
Require Proto_alpha.Environment.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.