🍲 Dal_apply.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Dal_apply.

Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [assert_dal_feature_enabled] is valid.

Lemma assert_dal_feature_enabled_is_valid ctxt
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? _ := Dal_apply.assert_dal_feature_enabled ctxt in
  True.
Proof.
  unfold Dal_apply.assert_dal_feature_enabled.
  hauto l: on.
Qed.

The function [only_if_dal_feature_enabled] is valid.

Lemma only_if_dal_feature_enabled_is_valid {A : Set} (P : A → Prop)
  ctxt default f
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_default : ∀ ctxt,
    Raw_context.Valid.t ctxt →
    P (default ctxt)
  )
  (H_f : ∀ ctxt,
    Raw_context.Valid.t ctxt →
    P (f ctxt)
  ) :
  P (Dal_apply.only_if_dal_feature_enabled ctxt default f).
Proof.
  unfold Dal_apply.only_if_dal_feature_enabled.
  hauto lq: on.
Qed.

The function [slot_of_int_e] is valid.

Lemma slot_of_int_e_is_valid n
  (H_n : Pervasives.Int.Valid.t n) :
  letP? slot := Dal_apply.slot_of_int_e n in
  Dal_slot_repr.Index.Valid.t slot.
Proof.
  unfold Dal_apply.slot_of_int_e.
  pose proof (Dal_slot_repr.Index.of_int_is_valid n).
  step; [scongruence |].
Admitted.

The function [validate_publish_slot_header] is valid.

Lemma validate_publish_slot_header_is_valid ctxt slot
  (H_ctxt : Raw_context.Valid.t ctxt)
  (* (H_slot : Dal_slot_repr.Valid.t slot) *) :
  letP? _ := Dal_apply.validate_publish_slot_header ctxt slot in
  True.
Proof.
  unfold Dal_apply.validate_publish_slot_header.
  eapply Error.split_letP. {
    now apply assert_dal_feature_enabled_is_valid.
  }
  intros.
  eapply Error.split_letP. {
    apply slot_of_int_e_is_valid; lia.
  }
  intros.
  unfold error_unless. cbn.
  step; [| hauto lq: on].
  simpl.

Admitted.

The function [apply_publish_slot_header] is valid.

Lemma apply_publish_slot_header_is_valid ctxt slot
  (H_ctxt : Raw_context.Valid.t ctxt)
  (* (H_slot : Dal_slot_repr.Valid.t slot) *) :
  letP? ctxt := Dal_apply.apply_publish_slot_header ctxt slot in
  Raw_context.Valid.t ctxt.
Proof.
  unfold Dal_apply.apply_publish_slot_header.
  eapply Error.split_letP. {
    now apply assert_dal_feature_enabled_is_valid.
  }
  intros.
  eapply Error.split_letP.
Admitted.

The function [dal_finalisation] is valid.

Lemma dal_finalisation_is_valid ctxt
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(ctxt, endorsment) := Dal_apply.finalisation ctxt in
  Raw_context.Valid.t ctxt.
Proof.
  unfold Dal_apply.finalisation.
  apply only_if_dal_feature_enabled_is_valid; try easy.
  intros.
  eapply Error.split_letP. {
Admitted.