🌱 Seed_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
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.

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 :=
  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; |}).

Definition compute_for_cycle
  (c_value : Raw_context.t) (revealed : Cycle_repr.t) (cycle : Cycle_repr.cycle)
  : M? (Raw_context.t × list Storage.Seed.unrevealed_nonce) :=
  match Cycle_repr.pred cycle with
  | None ⇒
    (* ❌ Assert instruction is not handled. *)
    assert (M? (Raw_context.t × list Storage.Seed.unrevealed_nonce)) false
  | Some previous_cycle ⇒
    let levels :=
      Level_storage.levels_with_commitments_in_cycle c_value revealed in
    let combine
      (function_parameter :
        Raw_context.t × Seed_repr.seed × list Storage.Seed.unrevealed_nonce)
      : Level_repr.t →
      M? (Raw_context.t × Seed_repr.seed × list Storage.Seed.unrevealed_nonce) :=
      let '(c_value, random_seed, 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 nonce_value ⇒
          let? c_value :=
            Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.remove_existing)
              c_value level in
          return?
            (c_value, (Seed_repr.nonce_value random_seed nonce_value),
              unrevealed)
        | Storage.Cycle.Unrevealed u_value ⇒
          let? c_value :=
            Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.remove_existing)
              c_value level in
          return? (c_value, random_seed, (cons u_value unrevealed))
        end in
    let? prev_seed :=
      Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) c_value previous_cycle in
    let seed_value := Seed_repr.deterministic_seed prev_seed in
    let? '(c_value, seed_value, unrevealed) :=
      List.fold_left_es combine (c_value, seed_value, nil) levels in
    let? c_value :=
      Storage.Seed.For_cycle.(Storage.FOR_CYCLE.init_value) c_value cycle
        seed_value in
    return? (c_value, unrevealed)
  end.

Definition for_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
  : M? Seed_repr.seed :=
  let preserved := Constants_storage.preserved_cycles ctxt in
  let current_level := Level_storage.current ctxt in
  let current_cycle := current_level.(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 :=
    match Cycle_repr.sub current_cycle preserved with
    | None ⇒ Cycle_repr.root_value
    | Some oldest ⇒ 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
  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
          let? ctxt :=
            Storage.Seed.For_cycle.(Storage.FOR_CYCLE.init_value) ctxt cycle
              seed_value in
          return? ((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 preserved := Constants_storage.preserved_cycles ctxt in
  match Cycle_repr.pred last_cycle with
  | None ⇒ return? (ctxt, nil)
  | Some revealed ⇒
    let inited_seed_cycle := Cycle_repr.add last_cycle (preserved +i 1) in
    compute_for_cycle ctxt revealed inited_seed_cycle
  end.