Skip to main content

๐ŸŒฑ Seed_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
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.

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).