🍃 Vdf.v
Environment
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.
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.