🍲 Dal_slot_storage.v
Proofs
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Dal_slot_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Dal_slot_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
The function [find] is valid.
Lemma find_is_valid ctxt level
(H_ctxt : Raw_context.Valid.t ctxt)
(H_level : Raw_level_repr.Valid.t level) :
letP? slots := Dal_slot_storage.find ctxt level in
Option.Forall (List.Forall Dal_slot_repr.Valid.t) slots.
Proof.
Admitted.
The function [finalize_current_slots] is valid.
Lemma finalize_current_slots_is_valid ctxt
(H_ctxt : Raw_context.Valid.t ctxt) :
let ctxt := Dal_slot_storage.finalize_current_slots ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [compute_available_slots] is valid.
Lemma compute_available_slots_is_valid ctxt seen_slots
(H_ctxt : Raw_context.Valid.t ctxt)
(H_seen_slots : List.Forall Dal_slot_repr.Valid.t seen_slots) :
let '(slots, available) :=
Dal_slot_storage.compute_available_slots ctxt seen_slots in
List.Forall Dal_slot_repr.Valid.t slots /\
Dal_endorsement_repr.Valid.t available.
Proof.
Admitted.
The function [get_slots_history] is valid.
Lemma get_slots_history_is_valid ctxt
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? _ := Dal_slot_storage.get_slots_history ctxt in
True.
Proof.
Admitted.
The function [update_skip_list] is valid.
Lemma update_skip_list_is_valid ctxt confirmed_slots
(H_ctxt : Raw_context.Valid.t ctxt)
(H_confirmed_slots : List.Forall Dal_slot_repr.Valid.t confirmed_slots) :
letP? ctxt := Dal_slot_storage.update_skip_list ctxt confirmed_slots in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [finalize_pending_slots] is valid.
Lemma finalize_pending_slots_is_valid ctxt
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, slot) := Dal_slot_storage.finalize_pending_slots ctxt in
Raw_context.Valid.t ctxt /\
Dal_endorsement_repr.Valid.t slot.
Proof.
Admitted.