🍃 Pvss_secp256k1.v

Environment

Gitlab , OCaml

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

Require Proto_alpha.Environment.S.

Parameter Included_PVSS_proof : Set.

Parameter Included_PVSS_Clear_share_t : Set.

Parameter Included_PVSS_Commitment_t : Set.

Parameter Included_PVSS_Encrypted_share_t : Set.

Parameter Included_PVSS_Public_key_t : Set.

Parameter Included_PVSS_Secret_key_t : Set.

Parameter Included_PVSS :
  S.PVSS (proof := Included_PVSS_proof)
    (Clear_share_t := Included_PVSS_Clear_share_t)
    (Commitment_t := Included_PVSS_Commitment_t)
    (Encrypted_share_t := Included_PVSS_Encrypted_share_t)
    (Public_key_t := Included_PVSS_Public_key_t)
    (Secret_key_t := Included_PVSS_Secret_key_t).

Definition proof := Included_PVSS.(S.PVSS.proof).

Definition Clear_share := Included_PVSS.(S.PVSS.Clear_share).

Definition Commitment := Included_PVSS.(S.PVSS.Commitment).

Definition Encrypted_share := Included_PVSS.(S.PVSS.Encrypted_share).

Definition Public_key := Included_PVSS.(S.PVSS.Public_key).

Definition Secret_key := Included_PVSS.(S.PVSS.Secret_key).

Definition proof_encoding : Data_encoding.t proof :=
  Included_PVSS.(S.PVSS.proof_encoding).

Definition check_dealer_proof :
  list Encrypted_share.(S.PVSS_ELEMENT.t) →
  list Commitment.(S.PVSS_ELEMENT.t) → proof →
  list Public_key.(S.PVSS_PUBLIC_KEY.t) → bool :=
  Included_PVSS.(S.PVSS.check_dealer_proof).

Definition check_revealed_share :
  Encrypted_share.(S.PVSS_ELEMENT.t) → Clear_share.(S.PVSS_ELEMENT.t) →
  Public_key.(S.PVSS_PUBLIC_KEY.t) → proof → bool :=
  Included_PVSS.(S.PVSS.check_revealed_share).

Definition reconstruct :
  list Clear_share.(S.PVSS_ELEMENT.t) → list int →
  Public_key.(S.PVSS_PUBLIC_KEY.t) := Included_PVSS.(S.PVSS.reconstruct).