🍲 Dal_slot_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_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
| None ⇒ return? Dal_slot_repr.History.genesis
| Some slots_history ⇒ return? 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
| None ⇒ return? (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
| None ⇒ return? (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.
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
| None ⇒ return? Dal_slot_repr.History.genesis
| Some slots_history ⇒ return? 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
| None ⇒ return? (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
| None ⇒ return? (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.