🍃 Sapling.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Module Ciphertext.
  Axiom encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.Ciphertext.encoding.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Ciphertext.

Module Commitment.
  Axiom encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.Commitment.encoding.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Commitment.

Module CV.
  Axiom encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.CV.encoding.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End CV.

Module Hash.
  Axiom encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.Hash.encoding.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Hash.

Module Nullifier.
  Axiom encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.Nullifier.encoding.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Nullifier.

Module UTXO.
  Axiom input_encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.UTXO.input_encoding.
  #[global] Hint Resolve input_encoding_is_valid : Data_encoding_db.

  Axiom output_encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.UTXO.output_encoding.
  #[global] Hint Resolve output_encoding_is_valid : Data_encoding_db.

  Axiom transaction_encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.UTXO.transaction_encoding.
  #[global] Hint Resolve transaction_encoding_is_valid : Data_encoding_db.

  Axiom binding_sig_encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Sapling.UTXO.binding_sig_encoding.
  #[global] Hint Resolve binding_sig_encoding_is_valid : Data_encoding_db.
End UTXO.