Skip to main content

🍲 Dal_slot_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.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Dal_endorsement_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Definition find (ctxt : Raw_context.t) (level : Raw_level_repr.t)
  : M?
    (option
      Storage.Dal.Slot_headers.(Storage_sigs.Non_iterable_indexed_data_storage.value)) :=
  Storage.Dal.Slot_headers.(Storage_sigs.Non_iterable_indexed_data_storage.find)
    ctxt level.

Definition finalize_current_slots (ctxt : Raw_context.t) : Raw_context.t :=
  let current_level := Raw_context.current_level ctxt in
  let slots := Raw_context.Dal.candidates ctxt in
  match slots with
  | []ctxt
  | cons _ _
    Storage.Dal.Slot_headers.(Storage_sigs.Non_iterable_indexed_data_storage.add)
      ctxt current_level.(Level_repr.t.level) slots
  end.

Definition compute_available_slots
  (ctxt : Raw_context.t) (seen_slots : list Dal_slot_repr.t)
  : list Dal_slot_repr.t × Dal_endorsement_repr.t :=
  let fold_available_slots
    (function_parameter : list Dal_slot_repr.t × Dal_endorsement_repr.t)
    : Dal_slot_repr.t list Dal_slot_repr.t × Dal_endorsement_repr.t :=
    let '(rev_slots, available_slots) := function_parameter in
    fun (slot : Dal_slot_repr.t) ⇒
      if
        Raw_context.Dal.is_slot_available ctxt
          slot.(Dal_slot_repr.t.id).(Dal_slot_repr.id.index)
      then
        ((cons slot rev_slots),
          (Dal_endorsement_repr.commit available_slots
            slot.(Dal_slot_repr.t.id).(Dal_slot_repr.id.index)))
      else
        (rev_slots, available_slots) in
  List.fold_left fold_available_slots (nil, Dal_endorsement_repr.empty)
    seen_slots.

Definition get_slots_history (ctxt : Raw_context.t)
  : M? Dal_slot_repr.Slots_history.t :=
  let? function_parameter :=
    Storage.Dal.Slots_history.(Storage_sigs.Single_data_storage.find) ctxt in
  match function_parameter with
  | Nonereturn? Dal_slot_repr.Slots_history.genesis
  | Some slots_historyreturn? slots_history
  end.

Definition update_skip_list
  (ctxt : Raw_context.t) (confirmed_slots : list Dal_slot_repr.slot)
  : M? Raw_context.t :=
  let? slots_history := get_slots_history ctxt in
  let? slots_history :=
    Dal_slot_repr.Slots_history.add_confirmed_slots_no_cache slots_history
      confirmed_slots in
  Error_monad.op_gtpipeeq
    (Storage.Dal.Slots_history.(Storage_sigs.Single_data_storage.add) ctxt
      slots_history) Error_monad.ok.

Definition finalize_pending_slots (ctxt : Raw_context.t)
  : M? (Raw_context.t × Dal_endorsement_repr.t) :=
  let '{| Level_repr.t.level := raw_level |} := Raw_context.current_level ctxt
    in
  let '{| Constants_parametric_repr.t.dal := dal |} :=
    Raw_context.constants ctxt in
  let? res :=
    Raw_level_repr.sub raw_level
      dal.(Constants_parametric_repr.dal.endorsement_lag) in
  match res with
  | Nonereturn? (ctxt, Dal_endorsement_repr.empty)
  | Some level_endorsed
    let? function_parameter :=
      Storage.Dal.Slot_headers.(Storage_sigs.Non_iterable_indexed_data_storage.find)
        ctxt level_endorsed in
    match function_parameter with
    | Nonereturn? (ctxt, Dal_endorsement_repr.empty)
    | Some seen_slots
      let '(rev_confirmed_slots, available_slots) :=
        compute_available_slots ctxt seen_slots in
      let confirmed_slots := List.rev rev_confirmed_slots in
      let? ctxt := update_skip_list ctxt confirmed_slots in
      let ctxt :=
        Storage.Dal.Slot_headers.(Storage_sigs.Non_iterable_indexed_data_storage.remove)
          ctxt level_endorsed in
      return? (ctxt, available_slots)
    end
  end.