🦏 Sc_rollup_storage.v
Proofs
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.
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.
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.
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.
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.
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.
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.
Raw_context.Valid.t ctxt →
letP? '(_, ctxt) := Sc_rollup_storage.parameters_type ctxt rollup in
Raw_context.Valid.t ctxt.
Proof.
Admitted.