๐ฑ Seed_storage.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_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.State_hash.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.State_hash.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Records for the constructor parameters
Module ConstructorRecords_seed_computation_status.
Module seed_computation_status.
Module Vdf_revelation_stage.
Record record {seed_discriminant seed_challenge : Set} : Set := Build {
seed_discriminant : seed_discriminant;
seed_challenge : seed_challenge;
}.
Arguments record : clear implicits.
Definition with_seed_discriminant {t_seed_discriminant t_seed_challenge}
seed_discriminant (r : record t_seed_discriminant t_seed_challenge) :=
Build t_seed_discriminant t_seed_challenge seed_discriminant
r.(seed_challenge).
Definition with_seed_challenge {t_seed_discriminant t_seed_challenge}
seed_challenge (r : record t_seed_discriminant t_seed_challenge) :=
Build t_seed_discriminant t_seed_challenge r.(seed_discriminant)
seed_challenge.
End Vdf_revelation_stage.
Definition Vdf_revelation_stage_skeleton := Vdf_revelation_stage.record.
End seed_computation_status.
End ConstructorRecords_seed_computation_status.
Import ConstructorRecords_seed_computation_status.
Reserved Notation "'seed_computation_status.Vdf_revelation_stage".
Inductive seed_computation_status : Set :=
| Nonce_revelation_stage : seed_computation_status
| Vdf_revelation_stage :
'seed_computation_status.Vdf_revelation_stage โ seed_computation_status
| Computation_finished : seed_computation_status
where "'seed_computation_status.Vdf_revelation_stage" :=
(seed_computation_status.Vdf_revelation_stage_skeleton Seed_repr.seed
Seed_repr.seed).
Module seed_computation_status.
Include ConstructorRecords_seed_computation_status.seed_computation_status.
Definition Vdf_revelation_stage :=
'seed_computation_status.Vdf_revelation_stage.
End seed_computation_status.
Module Unknown.
Record record : Set := Build {
oldest : Cycle_repr.t;
cycle : Cycle_repr.t;
latest : Cycle_repr.t;
}.
Definition with_oldest oldest (r : record) :=
Build oldest r.(cycle) r.(latest).
Definition with_cycle cycle (r : record) :=
Build r.(oldest) cycle r.(latest).
Definition with_latest latest (r : record) :=
Build r.(oldest) r.(cycle) latest.
End Unknown.
Definition Unknown := Unknown.record.
Module seed_computation_status.
Module Vdf_revelation_stage.
Record record {seed_discriminant seed_challenge : Set} : Set := Build {
seed_discriminant : seed_discriminant;
seed_challenge : seed_challenge;
}.
Arguments record : clear implicits.
Definition with_seed_discriminant {t_seed_discriminant t_seed_challenge}
seed_discriminant (r : record t_seed_discriminant t_seed_challenge) :=
Build t_seed_discriminant t_seed_challenge seed_discriminant
r.(seed_challenge).
Definition with_seed_challenge {t_seed_discriminant t_seed_challenge}
seed_challenge (r : record t_seed_discriminant t_seed_challenge) :=
Build t_seed_discriminant t_seed_challenge r.(seed_discriminant)
seed_challenge.
End Vdf_revelation_stage.
Definition Vdf_revelation_stage_skeleton := Vdf_revelation_stage.record.
End seed_computation_status.
End ConstructorRecords_seed_computation_status.
Import ConstructorRecords_seed_computation_status.
Reserved Notation "'seed_computation_status.Vdf_revelation_stage".
Inductive seed_computation_status : Set :=
| Nonce_revelation_stage : seed_computation_status
| Vdf_revelation_stage :
'seed_computation_status.Vdf_revelation_stage โ seed_computation_status
| Computation_finished : seed_computation_status
where "'seed_computation_status.Vdf_revelation_stage" :=
(seed_computation_status.Vdf_revelation_stage_skeleton Seed_repr.seed
Seed_repr.seed).
Module seed_computation_status.
Include ConstructorRecords_seed_computation_status.seed_computation_status.
Definition Vdf_revelation_stage :=
'seed_computation_status.Vdf_revelation_stage.
End seed_computation_status.
Module Unknown.
Record record : Set := Build {
oldest : Cycle_repr.t;
cycle : Cycle_repr.t;
latest : Cycle_repr.t;
}.
Definition with_oldest oldest (r : record) :=
Build oldest r.(cycle) r.(latest).
Definition with_cycle cycle (r : record) :=
Build r.(oldest) cycle r.(latest).
Definition with_latest latest (r : record) :=
Build r.(oldest) r.(cycle) latest.
End Unknown.
Definition Unknown := Unknown.record.
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "seed.unknown_seed"
"Unknown seed" "The requested seed is not available"
(Some
(fun (ppf : Format.formatter) โ
fun (function_parameter :
Cycle_repr.t ร Cycle_repr.t ร Cycle_repr.cycle) โ
let '(oldest, cycle, latest) := function_parameter in
if Cycle_repr.op_lt cycle oldest then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The seed for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has been cleared from the context (oldest known seed is for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"The seed for cycle %a has been cleared from the context (oldest known seed is for cycle %a)")
Cycle_repr.pp cycle Cycle_repr.pp oldest
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The seed for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has not been computed yet (latest known seed is for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"The seed for cycle %a has not been computed yet (latest known seed is for cycle %a)")
Cycle_repr.pp cycle Cycle_repr.pp latest))
(Data_encoding.obj3
(Data_encoding.req None None "oldest" Cycle_repr.encoding)
(Data_encoding.req None None "requested" Cycle_repr.encoding)
(Data_encoding.req None None "latest" Cycle_repr.encoding))
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Unknown" then
let '{|
Unknown.oldest := oldest;
Unknown.cycle := cycle;
Unknown.latest := latest
|} := cast Unknown payload in
Some (oldest, cycle, latest)
else None
end)
(fun (function_parameter : Cycle_repr.t ร Cycle_repr.t ร Cycle_repr.cycle)
โ
let '(oldest, cycle, latest) := function_parameter in
Build_extensible "Unknown" Unknown
{| Unknown.oldest := oldest; Unknown.cycle := cycle;
Unknown.latest := latest; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"vdf.too_early_revelation" "Too early VDF revelation"
"VDF revelation before the end of the nonce revelation period" None
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Too_early_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) โ
let '_ := function_parameter in
Build_extensible "Too_early_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "vdf.unverified_result"
"Unverified VDF" "VDF verification failed"
(Some
(fun (ppf : Format.formatter) โ
fun (function_parameter : unit) โ
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"A correct VDF result and Wesolowski's proof are expected"
CamlinternalFormatBasics.End_of_format)
"A correct VDF result and Wesolowski's proof are expected")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Unverified_vdf" then
Some tt
else None
end)
(fun (function_parameter : unit) โ
let '_ := function_parameter in
Build_extensible "Unverified_vdf" unit tt) in
Error_monad.register_error_kind Error_monad.Branch "vdf.previously_revealed"
"Previously revealed VDF" "Duplicate VDF revelation in cycle" None
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Already_accepted" then
Some tt
else None
end)
(fun (function_parameter : unit) โ
let '_ := function_parameter in
Build_extensible "Already_accepted" unit tt).
Definition purge_nonces_and_get_unrevealed
(ctxt : Raw_context.t) (cycle : Cycle_repr.t)
: M? (Raw_context.t ร list Storage.Seed.unrevealed_nonce) :=
let? levels := Level_storage.levels_with_commitments_in_cycle ctxt cycle in
let combine
(function_parameter : Raw_context.t ร list Storage.Seed.unrevealed_nonce)
: Level_repr.t โ M? (Raw_context.t ร list Storage.Seed.unrevealed_nonce) :=
let '(c_value, unrevealed) := function_parameter in
fun (level : Level_repr.t) โ
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
c_value level in
match function_parameter with
| Storage.Cycle.Revealed _ โ
Error_monad.Lwt_result_syntax.op_letplus
(Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.remove_existing)
c_value level) (fun c_value โ (c_value, unrevealed))
| Storage.Cycle.Unrevealed u_value โ
Error_monad.Lwt_result_syntax.op_letplus
(Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.remove_existing)
c_value level) (fun c_value โ (c_value, (cons u_value unrevealed)))
end in
List.fold_left_es combine (ctxt, nil) levels.
Definition compute_randao (ctxt : Raw_context.t) : M? Raw_context.t :=
let current_cycle := (Level_storage.current ctxt).(Level_repr.t.cycle) in
let preserved := Constants_storage.preserved_cycles ctxt in
let? cycle_computed := Cycle_repr.add current_cycle (preserved +i 1) in
let seed_computed :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.mem) ctxt cycle_computed in
match
(((Cycle_repr.pred current_cycle), (Cycle_repr.pred cycle_computed)),
match ((Cycle_repr.pred current_cycle), (Cycle_repr.pred cycle_computed))
with
| (Some prev_cycle, Some prev_cycle_computed) โ
Pervasives.not seed_computed
| _ โ false
end) with
| ((Some prev_cycle, Some prev_cycle_computed), true) โ
let? levels :=
Level_storage.levels_with_commitments_in_cycle ctxt prev_cycle in
let? prev_seed :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt prev_cycle_computed in
let combine (function_parameter : Raw_context.t ร Seed_repr.seed)
: Level_repr.t โ M? (Raw_context.t ร Seed_repr.seed) :=
let '(c_value, random_seed) := function_parameter in
fun (level : Level_repr.t) โ
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
c_value level in
match function_parameter with
| Storage.Cycle.Revealed nonce_value โ
return? (c_value, (Seed_repr.update_seed_aux random_seed nonce_value))
| Storage.Cycle.Unrevealed _ โ return? (c_value, random_seed)
end in
let seed_value := Seed_repr.deterministic_seed prev_seed in
let? '(c_value, seed_value) :=
List.fold_left_es combine (ctxt, seed_value) levels in
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.init_value) c_value cycle_computed
seed_value
| ((_, _), _) โ return? ctxt
end.
Definition get_seed_computation_status (ctxt : Raw_context.t)
: M? seed_computation_status :=
let current_level := Level_storage.current ctxt in
let current_cycle := current_level.(Level_repr.t.cycle) in
let nonce_revelation_threshold :=
Constants_storage.nonce_revelation_threshold ctxt in
if
current_level.(Level_repr.t.cycle_position) <i32 nonce_revelation_threshold
then
return? Nonce_revelation_stage
else
let? status := Storage.Seed.get_status ctxt in
match status with
| Seed_repr.RANDAO_seed โ
let preserved := Constants_storage.preserved_cycles ctxt in
let? cycle_computed := Cycle_repr.add current_cycle (preserved +i 1) in
let? previous_cycle := Cycle_repr.add current_cycle preserved in
let? seed_discriminant :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt previous_cycle in
let? seed_challenge :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt cycle_computed in
return?
(Vdf_revelation_stage
{|
seed_computation_status.Vdf_revelation_stage.seed_discriminant :=
seed_discriminant;
seed_computation_status.Vdf_revelation_stage.seed_challenge :=
seed_challenge; |})
| Seed_repr.VDF_seed โ return? Computation_finished
end.
Definition check_vdf
(ctxt : Raw_context.t) (vdf_solution : Seed_repr.vdf_solution) : M? unit :=
let? r_value := get_seed_computation_status ctxt in
let? '(seed_discriminant, seed_challenge) :=
match r_value with
| Computation_finished โ
Error_monad.error_value (Build_extensible "Already_accepted" unit tt)
| Nonce_revelation_stage โ
Error_monad.error_value (Build_extensible "Too_early_revelation" unit tt)
|
Vdf_revelation_stage {|
seed_computation_status.Vdf_revelation_stage.seed_discriminant :=
seed_discriminant;
seed_computation_status.Vdf_revelation_stage.seed_challenge :=
seed_challenge
|} โ return? (seed_discriminant, seed_challenge)
end in
let? stored :=
Storage.Seed.VDF_setup.(Storage_sigs.Single_data_storage.find) ctxt in
let? '(ctxt, setup) :=
match stored with
| None โ
let setup := Seed_repr.generate_vdf_setup seed_discriminant seed_challenge
in
let ctxt :=
Storage.Seed.VDF_setup.(Storage_sigs.Single_data_storage.add) ctxt setup
in
return? (ctxt, setup)
| Some setup โ return? (ctxt, setup)
end in
let? '_ :=
Error_monad.error_unless
(Option.value_value
(Seed_repr.verify setup (Constants_storage.vdf_difficulty ctxt)
vdf_solution) false) (Build_extensible "Unverified_vdf" unit tt) in
return? tt.
Definition update_seed
(ctxt : Raw_context.t) (vdf_solution : Seed_repr.vdf_solution)
: M? Raw_context.t :=
let current_cycle := (Level_storage.current ctxt).(Level_repr.t.cycle) in
let preserved := Constants_storage.preserved_cycles ctxt in
let? cycle_computed := Cycle_repr.add current_cycle (preserved +i 1) in
let? seed_challenge :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt cycle_computed in
let new_seed := Seed_repr.vdf_to_seed seed_challenge vdf_solution in
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.update) ctxt cycle_computed new_seed
Seed_repr.VDF_seed.
Definition raw_for_cycle : Raw_context.t โ Cycle_repr.t โ M? Seed_repr.seed :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get).
Definition for_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
: M? Seed_repr.seed :=
let preserved := Constants_storage.preserved_cycles ctxt in
let max_slashing_period := Constants_storage.max_slashing_period ctxt in
let current_cycle := (Level_storage.current ctxt).(Level_repr.t.cycle) in
let? latest :=
if Cycle_repr.op_eq current_cycle Cycle_repr.root_value then
Cycle_repr.add current_cycle (preserved +i 1)
else
Cycle_repr.add current_cycle preserved in
let? oldest :=
let? res := Cycle_repr.sub current_cycle (max_slashing_period -i 1) in
match res with
| None โ return? Cycle_repr.root_value
| Some oldest โ return? oldest
end in
let? '_ :=
Error_monad.error_unless
((Cycle_repr.op_lteq oldest cycle) && (Cycle_repr.op_lteq cycle latest))
(Build_extensible "Unknown" Unknown
{| Unknown.oldest := oldest; Unknown.cycle := cycle;
Unknown.latest := latest; |}) in
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt cycle.
Definition init_value
(initial_seed : option State_hash.t) (ctxt : Raw_context.t)
: M? Raw_context.t :=
let preserved := Constants_storage.preserved_cycles ctxt in
let? ctxt :=
Storage.Seed_status.(Storage_sigs.Single_data_storage.init_value) ctxt
Seed_repr.RANDAO_seed in
Error_monad.op_gtpipeeqquestion
(List.fold_left_es
(fun (function_parameter : int ร Raw_context.t) โ
let '(c_value, ctxt) := function_parameter in
fun (seed_value : Seed_repr.seed) โ
let cycle := Cycle_repr.of_int32_exn (Int32.of_int c_value) in
Error_monad.Lwt_result_syntax.op_letplus
(Storage.Seed.For_cycle.(Storage.FOR_CYCLE.init_value) ctxt cycle
seed_value) (fun ctxt โ ((c_value +i 1), ctxt))) (0, ctxt)
(Seed_repr.initial_seeds initial_seed (preserved +i 2))) Pervasives.snd.
Definition cycle_end (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
: M? (Raw_context.t ร list Storage.Seed.unrevealed_nonce) :=
let ctxt :=
Storage.Seed.VDF_setup.(Storage_sigs.Single_data_storage.remove) ctxt in
match Cycle_repr.pred last_cycle with
| None โ return? (ctxt, nil)
| Some previous_cycle โ purge_nonces_and_get_unrevealed ctxt previous_cycle
end.
Definition remove_for_cycle
: Raw_context.t โ Cycle_repr.t โ M? Raw_context.t :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.remove_existing).
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "seed.unknown_seed"
"Unknown seed" "The requested seed is not available"
(Some
(fun (ppf : Format.formatter) โ
fun (function_parameter :
Cycle_repr.t ร Cycle_repr.t ร Cycle_repr.cycle) โ
let '(oldest, cycle, latest) := function_parameter in
if Cycle_repr.op_lt cycle oldest then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The seed for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has been cleared from the context (oldest known seed is for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"The seed for cycle %a has been cleared from the context (oldest known seed is for cycle %a)")
Cycle_repr.pp cycle Cycle_repr.pp oldest
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The seed for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has not been computed yet (latest known seed is for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"The seed for cycle %a has not been computed yet (latest known seed is for cycle %a)")
Cycle_repr.pp cycle Cycle_repr.pp latest))
(Data_encoding.obj3
(Data_encoding.req None None "oldest" Cycle_repr.encoding)
(Data_encoding.req None None "requested" Cycle_repr.encoding)
(Data_encoding.req None None "latest" Cycle_repr.encoding))
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Unknown" then
let '{|
Unknown.oldest := oldest;
Unknown.cycle := cycle;
Unknown.latest := latest
|} := cast Unknown payload in
Some (oldest, cycle, latest)
else None
end)
(fun (function_parameter : Cycle_repr.t ร Cycle_repr.t ร Cycle_repr.cycle)
โ
let '(oldest, cycle, latest) := function_parameter in
Build_extensible "Unknown" Unknown
{| Unknown.oldest := oldest; Unknown.cycle := cycle;
Unknown.latest := latest; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"vdf.too_early_revelation" "Too early VDF revelation"
"VDF revelation before the end of the nonce revelation period" None
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Too_early_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) โ
let '_ := function_parameter in
Build_extensible "Too_early_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "vdf.unverified_result"
"Unverified VDF" "VDF verification failed"
(Some
(fun (ppf : Format.formatter) โ
fun (function_parameter : unit) โ
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"A correct VDF result and Wesolowski's proof are expected"
CamlinternalFormatBasics.End_of_format)
"A correct VDF result and Wesolowski's proof are expected")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Unverified_vdf" then
Some tt
else None
end)
(fun (function_parameter : unit) โ
let '_ := function_parameter in
Build_extensible "Unverified_vdf" unit tt) in
Error_monad.register_error_kind Error_monad.Branch "vdf.previously_revealed"
"Previously revealed VDF" "Duplicate VDF revelation in cycle" None
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) โ
match function_parameter with
| Build_extensible tag _ payload โ
if String.eqb tag "Already_accepted" then
Some tt
else None
end)
(fun (function_parameter : unit) โ
let '_ := function_parameter in
Build_extensible "Already_accepted" unit tt).
Definition purge_nonces_and_get_unrevealed
(ctxt : Raw_context.t) (cycle : Cycle_repr.t)
: M? (Raw_context.t ร list Storage.Seed.unrevealed_nonce) :=
let? levels := Level_storage.levels_with_commitments_in_cycle ctxt cycle in
let combine
(function_parameter : Raw_context.t ร list Storage.Seed.unrevealed_nonce)
: Level_repr.t โ M? (Raw_context.t ร list Storage.Seed.unrevealed_nonce) :=
let '(c_value, unrevealed) := function_parameter in
fun (level : Level_repr.t) โ
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
c_value level in
match function_parameter with
| Storage.Cycle.Revealed _ โ
Error_monad.Lwt_result_syntax.op_letplus
(Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.remove_existing)
c_value level) (fun c_value โ (c_value, unrevealed))
| Storage.Cycle.Unrevealed u_value โ
Error_monad.Lwt_result_syntax.op_letplus
(Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.remove_existing)
c_value level) (fun c_value โ (c_value, (cons u_value unrevealed)))
end in
List.fold_left_es combine (ctxt, nil) levels.
Definition compute_randao (ctxt : Raw_context.t) : M? Raw_context.t :=
let current_cycle := (Level_storage.current ctxt).(Level_repr.t.cycle) in
let preserved := Constants_storage.preserved_cycles ctxt in
let? cycle_computed := Cycle_repr.add current_cycle (preserved +i 1) in
let seed_computed :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.mem) ctxt cycle_computed in
match
(((Cycle_repr.pred current_cycle), (Cycle_repr.pred cycle_computed)),
match ((Cycle_repr.pred current_cycle), (Cycle_repr.pred cycle_computed))
with
| (Some prev_cycle, Some prev_cycle_computed) โ
Pervasives.not seed_computed
| _ โ false
end) with
| ((Some prev_cycle, Some prev_cycle_computed), true) โ
let? levels :=
Level_storage.levels_with_commitments_in_cycle ctxt prev_cycle in
let? prev_seed :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt prev_cycle_computed in
let combine (function_parameter : Raw_context.t ร Seed_repr.seed)
: Level_repr.t โ M? (Raw_context.t ร Seed_repr.seed) :=
let '(c_value, random_seed) := function_parameter in
fun (level : Level_repr.t) โ
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
c_value level in
match function_parameter with
| Storage.Cycle.Revealed nonce_value โ
return? (c_value, (Seed_repr.update_seed_aux random_seed nonce_value))
| Storage.Cycle.Unrevealed _ โ return? (c_value, random_seed)
end in
let seed_value := Seed_repr.deterministic_seed prev_seed in
let? '(c_value, seed_value) :=
List.fold_left_es combine (ctxt, seed_value) levels in
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.init_value) c_value cycle_computed
seed_value
| ((_, _), _) โ return? ctxt
end.
Definition get_seed_computation_status (ctxt : Raw_context.t)
: M? seed_computation_status :=
let current_level := Level_storage.current ctxt in
let current_cycle := current_level.(Level_repr.t.cycle) in
let nonce_revelation_threshold :=
Constants_storage.nonce_revelation_threshold ctxt in
if
current_level.(Level_repr.t.cycle_position) <i32 nonce_revelation_threshold
then
return? Nonce_revelation_stage
else
let? status := Storage.Seed.get_status ctxt in
match status with
| Seed_repr.RANDAO_seed โ
let preserved := Constants_storage.preserved_cycles ctxt in
let? cycle_computed := Cycle_repr.add current_cycle (preserved +i 1) in
let? previous_cycle := Cycle_repr.add current_cycle preserved in
let? seed_discriminant :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt previous_cycle in
let? seed_challenge :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt cycle_computed in
return?
(Vdf_revelation_stage
{|
seed_computation_status.Vdf_revelation_stage.seed_discriminant :=
seed_discriminant;
seed_computation_status.Vdf_revelation_stage.seed_challenge :=
seed_challenge; |})
| Seed_repr.VDF_seed โ return? Computation_finished
end.
Definition check_vdf
(ctxt : Raw_context.t) (vdf_solution : Seed_repr.vdf_solution) : M? unit :=
let? r_value := get_seed_computation_status ctxt in
let? '(seed_discriminant, seed_challenge) :=
match r_value with
| Computation_finished โ
Error_monad.error_value (Build_extensible "Already_accepted" unit tt)
| Nonce_revelation_stage โ
Error_monad.error_value (Build_extensible "Too_early_revelation" unit tt)
|
Vdf_revelation_stage {|
seed_computation_status.Vdf_revelation_stage.seed_discriminant :=
seed_discriminant;
seed_computation_status.Vdf_revelation_stage.seed_challenge :=
seed_challenge
|} โ return? (seed_discriminant, seed_challenge)
end in
let? stored :=
Storage.Seed.VDF_setup.(Storage_sigs.Single_data_storage.find) ctxt in
let? '(ctxt, setup) :=
match stored with
| None โ
let setup := Seed_repr.generate_vdf_setup seed_discriminant seed_challenge
in
let ctxt :=
Storage.Seed.VDF_setup.(Storage_sigs.Single_data_storage.add) ctxt setup
in
return? (ctxt, setup)
| Some setup โ return? (ctxt, setup)
end in
let? '_ :=
Error_monad.error_unless
(Option.value_value
(Seed_repr.verify setup (Constants_storage.vdf_difficulty ctxt)
vdf_solution) false) (Build_extensible "Unverified_vdf" unit tt) in
return? tt.
Definition update_seed
(ctxt : Raw_context.t) (vdf_solution : Seed_repr.vdf_solution)
: M? Raw_context.t :=
let current_cycle := (Level_storage.current ctxt).(Level_repr.t.cycle) in
let preserved := Constants_storage.preserved_cycles ctxt in
let? cycle_computed := Cycle_repr.add current_cycle (preserved +i 1) in
let? seed_challenge :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt cycle_computed in
let new_seed := Seed_repr.vdf_to_seed seed_challenge vdf_solution in
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.update) ctxt cycle_computed new_seed
Seed_repr.VDF_seed.
Definition raw_for_cycle : Raw_context.t โ Cycle_repr.t โ M? Seed_repr.seed :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get).
Definition for_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
: M? Seed_repr.seed :=
let preserved := Constants_storage.preserved_cycles ctxt in
let max_slashing_period := Constants_storage.max_slashing_period ctxt in
let current_cycle := (Level_storage.current ctxt).(Level_repr.t.cycle) in
let? latest :=
if Cycle_repr.op_eq current_cycle Cycle_repr.root_value then
Cycle_repr.add current_cycle (preserved +i 1)
else
Cycle_repr.add current_cycle preserved in
let? oldest :=
let? res := Cycle_repr.sub current_cycle (max_slashing_period -i 1) in
match res with
| None โ return? Cycle_repr.root_value
| Some oldest โ return? oldest
end in
let? '_ :=
Error_monad.error_unless
((Cycle_repr.op_lteq oldest cycle) && (Cycle_repr.op_lteq cycle latest))
(Build_extensible "Unknown" Unknown
{| Unknown.oldest := oldest; Unknown.cycle := cycle;
Unknown.latest := latest; |}) in
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt cycle.
Definition init_value
(initial_seed : option State_hash.t) (ctxt : Raw_context.t)
: M? Raw_context.t :=
let preserved := Constants_storage.preserved_cycles ctxt in
let? ctxt :=
Storage.Seed_status.(Storage_sigs.Single_data_storage.init_value) ctxt
Seed_repr.RANDAO_seed in
Error_monad.op_gtpipeeqquestion
(List.fold_left_es
(fun (function_parameter : int ร Raw_context.t) โ
let '(c_value, ctxt) := function_parameter in
fun (seed_value : Seed_repr.seed) โ
let cycle := Cycle_repr.of_int32_exn (Int32.of_int c_value) in
Error_monad.Lwt_result_syntax.op_letplus
(Storage.Seed.For_cycle.(Storage.FOR_CYCLE.init_value) ctxt cycle
seed_value) (fun ctxt โ ((c_value +i 1), ctxt))) (0, ctxt)
(Seed_repr.initial_seeds initial_seed (preserved +i 2))) Pervasives.snd.
Definition cycle_end (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
: M? (Raw_context.t ร list Storage.Seed.unrevealed_nonce) :=
let ctxt :=
Storage.Seed.VDF_setup.(Storage_sigs.Single_data_storage.remove) ctxt in
match Cycle_repr.pred last_cycle with
| None โ return? (ctxt, nil)
| Some previous_cycle โ purge_nonces_and_get_unrevealed ctxt previous_cycle
end.
Definition remove_for_cycle
: Raw_context.t โ Cycle_repr.t โ M? Raw_context.t :=
Storage.Seed.For_cycle.(Storage.FOR_CYCLE.remove_existing).