🦏 Sc_rollup_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_storage.

Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Bitset.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.

The function [address_from_nonce] is valid.

Lemma address_from_nonce_is_valid ctxt nonce_value :
  Raw_context.Valid.t ctxt →
  Origination_nonce.Valid.t nonce_value →
  letP? '(ctxt, _) := Sc_rollup_storage.address_from_nonce ctxt nonce_value in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [originate] is valid.

Lemma originate_is_valid
  ctxt kind_value boot_sector parameters_ty genesis_commitment:
  Raw_context.Valid.t ctxt →
  letP? '(_, _, _, ctxt) :=
    Sc_rollup_storage.originate
      ctxt kind_value boot_sector parameters_ty genesis_commitment in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [kind_value] is valid.

Lemma kind_value_is_valid ctxt address :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Sc_rollup_storage.kind_value ctxt address in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [list_unaccounted] is valid.

Lemma list_unaccounted_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? _ := Sc_rollup_storage.list_unaccounted ctxt in
  True.
Proof.
Admitted.

The function [genesis_info] is valid.

Lemma genesis_info_is_valid ctxt rollup :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, info) := Sc_rollup_storage.genesis_info ctxt rollup in
  Raw_context.Valid.t ctxt ∧
  Sc_rollup_commitment_repr.V1.genesis_info.Valid.t info.
Proof.
Admitted.

The function [get_boot_sector] is valid.

Lemma get_boot_sector_is_valid ctxt rollup :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Sc_rollup_storage.get_boot_sector ctxt rollup in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [parameters_type] is valid.

Lemma parameters_type_is_valid ctxt rollup :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) := Sc_rollup_storage.parameters_type ctxt rollup in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

Module Dal_slot.

The function [slot_of_int_e] is valid.

  Lemma slot_of_int_e_is_valid n_value :
    Pervasives.Int.Valid.t n_value →
    letP? index := Sc_rollup_storage.Dal_slot.slot_of_int_e n_value in
    Dal_slot_repr.Index.Valid.t index.
  Proof.
  Admitted.

The function [fail_if_slot_index_invalid] is valid.

  Lemma fail_if_slot_index_invalid_is_valid ctxt slot_index :
    Raw_context.Valid.t ctxt →
    Dal_slot_repr.Index.Valid.t slot_index →
    letP? index :=
      Sc_rollup_storage.Dal_slot.fail_if_slot_index_invalid ctxt slot_index in
    Dal_slot_repr.Index.Valid.t index.
  Proof.
  Admitted.

The function [all_indexes] is valid.

  Lemma all_indexes_is_valid ctxt :
    Raw_context.Valid.t ctxt →
    letP? indexes := Sc_rollup_storage.Dal_slot.all_indexes ctxt in
    List.Forall Dal_slot_repr.Index.Valid.t indexes.
  Proof.
  Admitted.

The function [subscribed_slots_at_level] is valid.

  Lemma subscribed_slots_at_level_is_valid ctxt rollup level :
    Raw_context.Valid.t ctxt →
    Raw_level_repr.Valid.t level →
    letP? bitset :=
      Sc_rollup_storage.Dal_slot.subscribed_slots_at_level ctxt rollup level in
    Bitset.Valid.t bitset.
  Proof.
  Admitted.

The function [subscribe] is valid.

  Lemma subscribe_is_valid ctxt rollup slot_index :
    Raw_context.Valid.t ctxt →
    Dal_slot_repr.Index.Valid.t slot_index →
    letP? '(index, level, ctxt) :=
      Sc_rollup_storage.Dal_slot.subscribe ctxt rollup slot_index in
    Dal_slot_repr.Index.Valid.t index ∧
    Raw_level_repr.Valid.t level ∧
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.

The function [subscribed_slot_indices] is valid.

  Lemma subscribed_slot_indices_is_valid ctxt rollup level :
    Raw_context.Valid.t ctxt →
    Raw_level_repr.Valid.t level →
    letP? indexes :=
      Sc_rollup_storage.Dal_slot.subscribed_slot_indices ctxt rollup level in
    List.Forall Dal_slot_repr.Index.Valid.t indexes.
  Proof.
  Admitted.
End Dal_slot.