Skip to main content

🍃 Vdf.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Int64.

Parameter form_size_bytes : int.

Parameter discriminant_size_bytes : int.

Parameter discriminant : Set.

Parameter challenge : Set.

Parameter result : Set.

Parameter proof : Set.

Definition difficulty : Set := Int64.t.

Parameter discriminant_to_bytes : discriminant bytes.

Parameter discriminant_of_bytes_opt : bytes option discriminant.

Parameter challenge_to_bytes : challenge bytes.

Parameter challenge_of_bytes_opt : bytes option challenge.

Parameter result_to_bytes : result bytes.

Parameter result_of_bytes_opt : bytes option result.

Parameter proof_to_bytes : proof bytes.

Parameter proof_of_bytes_opt : bytes option proof.

Parameter generate_discriminant : option Bytes.t int discriminant.

Parameter generate_challenge : discriminant Bytes.t challenge.

Parameter prove : discriminant challenge difficulty result × proof.

Parameter verify :
  discriminant challenge difficulty result proof bool.