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.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Dal_attestation_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_slot_headers (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_slot_headers (ctxt : Raw_context.t)
  : Raw_context.t :=
  let current_level := Raw_context.current_level ctxt in
  let slot_headers := Raw_context.Dal.candidates ctxt in
  match slot_headers with
  | []ctxt
  | cons _ _
    Storage.Dal.Slot.Headers.(Storage_sigs.Non_iterable_indexed_data_storage.add)
      ctxt current_level.(Level_repr.t.level) slot_headers
  end.

Definition compute_available_slot_headers
  (ctxt : Raw_context.t) (seen_slot_headers : list Dal_slot_repr.Header.t)
  : list Dal_slot_repr.Header.t × Dal_attestation_repr.t :=
  let fold_available_slots
    (function_parameter : list Dal_slot_repr.Header.t × Dal_attestation_repr.t)
    : Dal_slot_repr.Header.t
    list Dal_slot_repr.Header.t × Dal_attestation_repr.t :=
    let '(rev_slot_headers, available_slot_headers) := function_parameter in
    fun (slot : Dal_slot_repr.Header.t) ⇒
      if
        Raw_context.Dal.is_slot_index_available ctxt
          slot.(Dal_slot_repr.Header.t.id).(Dal_slot_repr.Header.id.index)
      then
        ((cons slot rev_slot_headers),
          (Dal_attestation_repr.commit available_slot_headers
            slot.(Dal_slot_repr.Header.t.id).(Dal_slot_repr.Header.id.index)))
      else
        (rev_slot_headers, available_slot_headers) in
  List.fold_left fold_available_slots (nil, Dal_attestation_repr.empty)
    seen_slot_headers.

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

Definition update_skip_list
  (ctxt : Raw_context.t) (confirmed_slot_headers : list Dal_slot_repr.Header.t)
  : M? Raw_context.t :=
  let? slots_history := get_slot_headers_history ctxt in
  let? slots_history :=
    Dal_slot_repr.History.add_confirmed_slot_headers_no_cache slots_history
      confirmed_slot_headers in
  Error_monad.op_gtpipeeq
    (Storage.Dal.Slot.History.(Storage_sigs.Single_data_storage.add) ctxt
      slots_history) Error_monad.ok.

Definition finalize_pending_slot_headers (ctxt : Raw_context.t)
  : M? (Raw_context.t × Dal_attestation_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? level_attested :=
    Raw_level_repr.sub raw_level
      dal.(Constants_parametric_repr.dal.attestation_lag) in
  match level_attested with
  | Nonereturn? (ctxt, Dal_attestation_repr.empty)
  | Some level_attested
    let? function_parameter :=
      Storage.Dal.Slot.Headers.(Storage_sigs.Non_iterable_indexed_data_storage.find)
        ctxt level_attested in
    match function_parameter with
    | Nonereturn? (ctxt, Dal_attestation_repr.empty)
    | Some seen_slots
      let '(rev_confirmed_slot_headers, available_slot_headers) :=
        compute_available_slot_headers ctxt seen_slots in
      let confirmed_slot_headers := List.rev rev_confirmed_slot_headers in
      let? ctxt := update_skip_list ctxt confirmed_slot_headers in
      let ctxt :=
        Storage.Dal.Slot.Headers.(Storage_sigs.Non_iterable_indexed_data_storage.remove)
          ctxt level_attested in
      return? (ctxt, available_slot_headers)
    end
  end.