🌱 Seed_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.State_hash.
Inductive seed : Set :=
| B : State_hash.t → seed.
Inductive t : Set :=
| T : State_hash.t → t.
Inductive sequence : Set :=
| S : State_hash.t → sequence.
Definition nonce : Set := bytes.
Definition vdf_setup : Set := Vdf.discriminant × Vdf.challenge.
Definition vdf_solution : Set := Vdf.result × Vdf.proof.
Definition seed_to_bytes (x_value : seed) : bytes :=
let seed_to_state_hash (function_parameter : seed) : State_hash.t :=
let 'B b_value := function_parameter in
b_value in
State_hash.to_bytes (seed_to_state_hash x_value).
Definition vdf_setup_encoding
: Data_encoding.encoding (Vdf.discriminant × Vdf.challenge) :=
let vdf_discriminant_encoding :=
Data_encoding.conv_with_guard Vdf.discriminant_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF discriminant could not be deserialised"
(Vdf.discriminant_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.discriminant_size_bytes) in
let vdf_challenge_encoding :=
Data_encoding.conv_with_guard Vdf.challenge_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF challenge could not be deserialised"
(Vdf.challenge_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
Data_encoding.tup2 vdf_discriminant_encoding vdf_challenge_encoding.
Definition vdf_solution_encoding
: Data_encoding.encoding (Vdf.result × Vdf.proof) :=
let vdf_result_encoding :=
Data_encoding.conv_with_guard Vdf.result_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF result could not be deserialised"
(Vdf.result_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
let vdf_proof_encoding :=
Data_encoding.conv_with_guard Vdf.proof_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF proof could not be deserialised"
(Vdf.proof_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
Data_encoding.tup2 vdf_result_encoding vdf_proof_encoding.
Definition pp_solution
(ppf : Format.formatter) (solution : Vdf.result × Vdf.proof) : unit :=
let '(result_value, proof_value) := solution in
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "VDF result: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "@[<v 2>VDF result: %a")
Hex.pp (Hex.of_bytes None (Vdf.result_to_bytes result_value)) in
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "VDF proof: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "@,VDF proof: %a")
Hex.pp (Hex.of_bytes None (Vdf.proof_to_bytes proof_value)) in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format) "@]").
Definition nonce_encoding : Data_encoding.encoding Bytes.t :=
Data_encoding.Fixed.bytes_value Constants_repr.nonce_length.
Definition zero_bytes : bytes := Bytes.make Nonce_hash.size_value "000" % char.
Definition state_hash_encoding : Data_encoding.encoding State_hash.t :=
Data_encoding.conv State_hash.to_bytes State_hash.of_bytes_exn None
(Data_encoding.Fixed.bytes_value Nonce_hash.size_value).
Definition seed_encoding : Data_encoding.encoding seed :=
Data_encoding.conv
(fun (function_parameter : seed) ⇒
let 'B b_value := function_parameter in
b_value) (fun (b_value : State_hash.t) ⇒ B b_value) None
state_hash_encoding.
Definition update_seed_aux (function_parameter : seed) : bytes → seed :=
let 'B state_value := function_parameter in
fun (nonce_value : bytes) ⇒
B
(State_hash.hash_bytes None
[ State_hash.to_bytes state_value; nonce_value ]).
Definition initialize_new (function_parameter : seed) : list bytes → t :=
let 'B state_value := function_parameter in
fun (append : list bytes) ⇒
T
(State_hash.hash_bytes None
(cons (State_hash.to_bytes state_value) (cons zero_bytes append))).
Definition xor_higher_bits (i_value : int32) (b_value : bytes) : bytes :=
let higher := TzEndian.get_int32 b_value 0 in
let r_value := Int32.logxor higher i_value in
let res := Bytes.copy b_value in
let '_ := TzEndian.set_int32 res 0 r_value in
res.
Definition sequence_value (function_parameter : t) : int32 → sequence :=
let 'T state_value := function_parameter in
fun (n_value : int32) ⇒
(fun (b_value : bytes) ⇒ S (State_hash.hash_bytes None [ b_value ]))
(xor_higher_bits n_value (State_hash.to_bytes state_value)).
Definition take (function_parameter : sequence) : bytes × sequence :=
let 'S state_value := function_parameter in
let b_value := State_hash.to_bytes state_value in
let h_value := State_hash.hash_bytes None [ b_value ] in
((State_hash.to_bytes h_value), (S h_value)).
#[bypass_check(guard)]
Definition take_int32 (s_value : sequence) (bound : int32) : int32 × sequence :=
if bound ≤i32 0 then
Pervasives.invalid_arg "Seed_repr.take_int32"
else
let drop_if_over := Int32.max_int -i32 (Int32.rem Int32.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int32 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int32 bytes_value 0 in
let r_value :=
if r_value =i32 Int32.min_int then
0
else
Int32.abs r_value in
if r_value ≥i32 drop_if_over then
loop s_value
else
let v_value := Int32.rem r_value bound in
(v_value, s_value) in
loop s_value.
#[bypass_check(guard)]
Definition take_int64 (s_value : sequence) (bound : int64) : int64 × sequence :=
if bound ≤i64 0 then
Pervasives.invalid_arg "Seed_repr.take_int64"
else
let drop_if_over := Int64.max_int -i64 (Int64.rem Int64.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int64 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int64 bytes_value 0 in
let r_value :=
if r_value =i64 Int64.min_int then
0
else
Int64.abs r_value in
if r_value ≥i64 drop_if_over then
loop s_value
else
let v_value := Int64.rem r_value bound in
(v_value, s_value) in
loop s_value.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.State_hash.
Inductive seed : Set :=
| B : State_hash.t → seed.
Inductive t : Set :=
| T : State_hash.t → t.
Inductive sequence : Set :=
| S : State_hash.t → sequence.
Definition nonce : Set := bytes.
Definition vdf_setup : Set := Vdf.discriminant × Vdf.challenge.
Definition vdf_solution : Set := Vdf.result × Vdf.proof.
Definition seed_to_bytes (x_value : seed) : bytes :=
let seed_to_state_hash (function_parameter : seed) : State_hash.t :=
let 'B b_value := function_parameter in
b_value in
State_hash.to_bytes (seed_to_state_hash x_value).
Definition vdf_setup_encoding
: Data_encoding.encoding (Vdf.discriminant × Vdf.challenge) :=
let vdf_discriminant_encoding :=
Data_encoding.conv_with_guard Vdf.discriminant_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF discriminant could not be deserialised"
(Vdf.discriminant_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.discriminant_size_bytes) in
let vdf_challenge_encoding :=
Data_encoding.conv_with_guard Vdf.challenge_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF challenge could not be deserialised"
(Vdf.challenge_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
Data_encoding.tup2 vdf_discriminant_encoding vdf_challenge_encoding.
Definition vdf_solution_encoding
: Data_encoding.encoding (Vdf.result × Vdf.proof) :=
let vdf_result_encoding :=
Data_encoding.conv_with_guard Vdf.result_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF result could not be deserialised"
(Vdf.result_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
let vdf_proof_encoding :=
Data_encoding.conv_with_guard Vdf.proof_to_bytes
(fun (b_value : Bytes.t) ⇒
Option.to_result "VDF proof could not be deserialised"
(Vdf.proof_of_bytes_opt b_value)) None
(Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
Data_encoding.tup2 vdf_result_encoding vdf_proof_encoding.
Definition pp_solution
(ppf : Format.formatter) (solution : Vdf.result × Vdf.proof) : unit :=
let '(result_value, proof_value) := solution in
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "VDF result: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "@[<v 2>VDF result: %a")
Hex.pp (Hex.of_bytes None (Vdf.result_to_bytes result_value)) in
let '_ :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "VDF proof: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))) "@,VDF proof: %a")
Hex.pp (Hex.of_bytes None (Vdf.proof_to_bytes proof_value)) in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format) "@]").
Definition nonce_encoding : Data_encoding.encoding Bytes.t :=
Data_encoding.Fixed.bytes_value Constants_repr.nonce_length.
Definition zero_bytes : bytes := Bytes.make Nonce_hash.size_value "000" % char.
Definition state_hash_encoding : Data_encoding.encoding State_hash.t :=
Data_encoding.conv State_hash.to_bytes State_hash.of_bytes_exn None
(Data_encoding.Fixed.bytes_value Nonce_hash.size_value).
Definition seed_encoding : Data_encoding.encoding seed :=
Data_encoding.conv
(fun (function_parameter : seed) ⇒
let 'B b_value := function_parameter in
b_value) (fun (b_value : State_hash.t) ⇒ B b_value) None
state_hash_encoding.
Definition update_seed_aux (function_parameter : seed) : bytes → seed :=
let 'B state_value := function_parameter in
fun (nonce_value : bytes) ⇒
B
(State_hash.hash_bytes None
[ State_hash.to_bytes state_value; nonce_value ]).
Definition initialize_new (function_parameter : seed) : list bytes → t :=
let 'B state_value := function_parameter in
fun (append : list bytes) ⇒
T
(State_hash.hash_bytes None
(cons (State_hash.to_bytes state_value) (cons zero_bytes append))).
Definition xor_higher_bits (i_value : int32) (b_value : bytes) : bytes :=
let higher := TzEndian.get_int32 b_value 0 in
let r_value := Int32.logxor higher i_value in
let res := Bytes.copy b_value in
let '_ := TzEndian.set_int32 res 0 r_value in
res.
Definition sequence_value (function_parameter : t) : int32 → sequence :=
let 'T state_value := function_parameter in
fun (n_value : int32) ⇒
(fun (b_value : bytes) ⇒ S (State_hash.hash_bytes None [ b_value ]))
(xor_higher_bits n_value (State_hash.to_bytes state_value)).
Definition take (function_parameter : sequence) : bytes × sequence :=
let 'S state_value := function_parameter in
let b_value := State_hash.to_bytes state_value in
let h_value := State_hash.hash_bytes None [ b_value ] in
((State_hash.to_bytes h_value), (S h_value)).
#[bypass_check(guard)]
Definition take_int32 (s_value : sequence) (bound : int32) : int32 × sequence :=
if bound ≤i32 0 then
Pervasives.invalid_arg "Seed_repr.take_int32"
else
let drop_if_over := Int32.max_int -i32 (Int32.rem Int32.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int32 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int32 bytes_value 0 in
let r_value :=
if r_value =i32 Int32.min_int then
0
else
Int32.abs r_value in
if r_value ≥i32 drop_if_over then
loop s_value
else
let v_value := Int32.rem r_value bound in
(v_value, s_value) in
loop s_value.
#[bypass_check(guard)]
Definition take_int64 (s_value : sequence) (bound : int64) : int64 × sequence :=
if bound ≤i64 0 then
Pervasives.invalid_arg "Seed_repr.take_int64"
else
let drop_if_over := Int64.max_int -i64 (Int64.rem Int64.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int64 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int64 bytes_value 0 in
let r_value :=
if r_value =i64 Int64.min_int then
0
else
Int64.abs r_value in
if r_value ≥i64 drop_if_over then
loop s_value
else
let v_value := Int64.rem r_value bound in
(v_value, s_value) in
loop s_value.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_nonce_length" "Unexpected nonce length"
"Nonce length is incorrect."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Nonce length is not "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" bytes long as it should."
CamlinternalFormatBasics.End_of_format)))
"Nonce length is not %i bytes long as it should.")
Constants_repr.nonce_length)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_nonce_length" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_nonce_length" unit tt).
Definition make_nonce (nonce_value : bytes) : M? bytes :=
if (Bytes.length nonce_value) ≠i Constants_repr.nonce_length then
Error_monad.error_value (Build_extensible "Unexpected_nonce_length" unit tt)
else
return? nonce_value.
Definition hash_value (nonce_value : bytes) : Nonce_hash.t :=
Nonce_hash.hash_bytes None [ nonce_value ].
Definition check_hash (nonce_value : bytes) (hash_value : Nonce_hash.t)
: bool :=
((Bytes.length nonce_value) =i Constants_repr.nonce_length) &&
(Nonce_hash.equal (Nonce_hash.hash_bytes None [ nonce_value ]) hash_value).
Definition nonce_hash_key_part : Nonce_hash.t → list string → list string :=
Nonce_hash.to_path.
Definition initial_nonce_0 : bytes := zero_bytes.
Definition initial_nonce_hash_0 : Nonce_hash.t := hash_value initial_nonce_0.
Definition deterministic_seed (seed_value : seed) : seed :=
update_seed_aux seed_value zero_bytes.
#[bypass_check(guard)]
Definition initial_seeds (initial_seed : option State_hash.t) (n_value : int)
: list seed :=
let fix loop (acc_value : list seed) (elt_value : seed) (i_value : int)
{struct i_value} : list seed :=
if i_value =i 1 then
List.rev (cons elt_value acc_value)
else
loop (cons elt_value acc_value) (deterministic_seed elt_value)
(i_value -i 1) in
let first_seed :=
match initial_seed with
| Some initial_seed ⇒ update_seed_aux (B initial_seed) initial_nonce_0
| None ⇒ B (State_hash.hash_bytes None nil)
end in
loop nil first_seed n_value.
Definition nonce_discriminant : bytes :=
Bytes.of_string "Tezos_generating_vdf_discriminant".
Definition nonce_challenge : bytes :=
Bytes.of_string "Tezos_generating_vdf_challenge".
Definition generate_vdf_setup (seed_discriminant : seed) (seed_challenge : seed)
: Vdf.discriminant × Vdf.challenge :=
let size_value := Vdf.discriminant_size_bytes in
let seed_value :=
seed_to_bytes (update_seed_aux seed_discriminant nonce_discriminant) in
let discriminant := Vdf.generate_discriminant (Some seed_value) size_value in
let input := seed_to_bytes (update_seed_aux seed_challenge nonce_challenge) in
let challenge := Vdf.generate_challenge discriminant input in
(discriminant, challenge).
Definition verify (function_parameter : Vdf.discriminant × Vdf.challenge)
: Vdf.difficulty → Vdf.result × Vdf.proof → option bool :=
let '(discriminant, challenge) := function_parameter in
fun (vdf_difficulty : Vdf.difficulty) ⇒
fun (solution : Vdf.result × Vdf.proof) ⇒
let '(result_value, proof_value) := solution in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Vdf.verify discriminant challenge vdf_difficulty result_value
proof_value).
Definition vdf_to_seed {A : Set}
(seed_challenge : seed) (solution : Vdf.result × A) : seed :=
let '(result_value, _) := solution in
update_seed_aux seed_challenge (Vdf.result_to_bytes result_value).
Inductive seed_status : Set :=
| RANDAO_seed : seed_status
| VDF_seed : seed_status.
Definition seed_status_encoding : Data_encoding.encoding seed_status :=
let to_bool (function_parameter : seed_status) : bool :=
match function_parameter with
| RANDAO_seed ⇒ false
| VDF_seed ⇒ true
end in
let of_bool (t_value : bool) : seed_status :=
if t_value then
VDF_seed
else
RANDAO_seed in
Data_encoding.conv to_bool of_bool None Data_encoding.bool_value.
Definition compare_vdf_solution {A B : Set}
(solution : Vdf.result × A) (solution' : Vdf.result × B) : int :=
let '(result_value, _) := solution in
let '(result', _) := solution' in
Compare.Bytes.(Compare.S.compare) (Vdf.result_to_bytes result_value)
(Vdf.result_to_bytes result').
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_nonce_length" "Unexpected nonce length"
"Nonce length is incorrect."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Nonce length is not "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" bytes long as it should."
CamlinternalFormatBasics.End_of_format)))
"Nonce length is not %i bytes long as it should.")
Constants_repr.nonce_length)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_nonce_length" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_nonce_length" unit tt).
Definition make_nonce (nonce_value : bytes) : M? bytes :=
if (Bytes.length nonce_value) ≠i Constants_repr.nonce_length then
Error_monad.error_value (Build_extensible "Unexpected_nonce_length" unit tt)
else
return? nonce_value.
Definition hash_value (nonce_value : bytes) : Nonce_hash.t :=
Nonce_hash.hash_bytes None [ nonce_value ].
Definition check_hash (nonce_value : bytes) (hash_value : Nonce_hash.t)
: bool :=
((Bytes.length nonce_value) =i Constants_repr.nonce_length) &&
(Nonce_hash.equal (Nonce_hash.hash_bytes None [ nonce_value ]) hash_value).
Definition nonce_hash_key_part : Nonce_hash.t → list string → list string :=
Nonce_hash.to_path.
Definition initial_nonce_0 : bytes := zero_bytes.
Definition initial_nonce_hash_0 : Nonce_hash.t := hash_value initial_nonce_0.
Definition deterministic_seed (seed_value : seed) : seed :=
update_seed_aux seed_value zero_bytes.
#[bypass_check(guard)]
Definition initial_seeds (initial_seed : option State_hash.t) (n_value : int)
: list seed :=
let fix loop (acc_value : list seed) (elt_value : seed) (i_value : int)
{struct i_value} : list seed :=
if i_value =i 1 then
List.rev (cons elt_value acc_value)
else
loop (cons elt_value acc_value) (deterministic_seed elt_value)
(i_value -i 1) in
let first_seed :=
match initial_seed with
| Some initial_seed ⇒ update_seed_aux (B initial_seed) initial_nonce_0
| None ⇒ B (State_hash.hash_bytes None nil)
end in
loop nil first_seed n_value.
Definition nonce_discriminant : bytes :=
Bytes.of_string "Tezos_generating_vdf_discriminant".
Definition nonce_challenge : bytes :=
Bytes.of_string "Tezos_generating_vdf_challenge".
Definition generate_vdf_setup (seed_discriminant : seed) (seed_challenge : seed)
: Vdf.discriminant × Vdf.challenge :=
let size_value := Vdf.discriminant_size_bytes in
let seed_value :=
seed_to_bytes (update_seed_aux seed_discriminant nonce_discriminant) in
let discriminant := Vdf.generate_discriminant (Some seed_value) size_value in
let input := seed_to_bytes (update_seed_aux seed_challenge nonce_challenge) in
let challenge := Vdf.generate_challenge discriminant input in
(discriminant, challenge).
Definition verify (function_parameter : Vdf.discriminant × Vdf.challenge)
: Vdf.difficulty → Vdf.result × Vdf.proof → option bool :=
let '(discriminant, challenge) := function_parameter in
fun (vdf_difficulty : Vdf.difficulty) ⇒
fun (solution : Vdf.result × Vdf.proof) ⇒
let '(result_value, proof_value) := solution in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Vdf.verify discriminant challenge vdf_difficulty result_value
proof_value).
Definition vdf_to_seed {A : Set}
(seed_challenge : seed) (solution : Vdf.result × A) : seed :=
let '(result_value, _) := solution in
update_seed_aux seed_challenge (Vdf.result_to_bytes result_value).
Inductive seed_status : Set :=
| RANDAO_seed : seed_status
| VDF_seed : seed_status.
Definition seed_status_encoding : Data_encoding.encoding seed_status :=
let to_bool (function_parameter : seed_status) : bool :=
match function_parameter with
| RANDAO_seed ⇒ false
| VDF_seed ⇒ true
end in
let of_bool (t_value : bool) : seed_status :=
if t_value then
VDF_seed
else
RANDAO_seed in
Data_encoding.conv to_bool of_bool None Data_encoding.bool_value.
Definition compare_vdf_solution {A B : Set}
(solution : Vdf.result × A) (solution' : Vdf.result × B) : int :=
let '(result_value, _) := solution in
let '(result', _) := solution' in
Compare.Bytes.(Compare.S.compare) (Vdf.result_to_bytes result_value)
(Vdf.result_to_bytes result').