🍲 Dal_slot_storage.v

Proofs

See code, Gitlab , OCaml

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.

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.