🦏 Sc_rollup_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_storage.

Require TezosOfOCaml.Environment.V8.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 parameters_ty genesis_commitment:
  Raw_context.Valid.t ctxt →
  letP? '(_, _, _, ctxt) :=
    Sc_rollup_storage.originate
      ctxt kind_value 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 [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.