🐆 Tx_rollup_state_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_state_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_state_repr.
The function [init_value] is valid.
Lemma init_value_is_valid ctxt tx_rollup :
Raw_context.Valid.t ctxt →
letP? ctxt := Tx_rollup_state_storage.init_value ctxt tx_rollup in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Tx_rollup_state_storage.init_value ctxt tx_rollup in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [find] is valid.
Lemma find_is_valid ctxt tx_rollup :
Raw_context.Valid.t ctxt →
letP? '(ctxt, state) := Tx_rollup_state_storage.find ctxt tx_rollup in
Raw_context.Valid.t ctxt ∧
Option.Forall Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, state) := Tx_rollup_state_storage.find ctxt tx_rollup in
Raw_context.Valid.t ctxt ∧
Option.Forall Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.
The function [get] is valid.
Lemma get_is_valid ctxt tx_rollup :
Raw_context.Valid.t ctxt →
letP? '(ctxt, state) := Tx_rollup_state_storage.get ctxt tx_rollup in
Raw_context.Valid.t ctxt ∧
Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, state) := Tx_rollup_state_storage.get ctxt tx_rollup in
Raw_context.Valid.t ctxt ∧
Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.
The function [assert_exist] is valid.
Lemma assert_exist_is_valid ctxt tx_rollup :
Raw_context.Valid.t ctxt →
letP? ctxt := Tx_rollup_state_storage.assert_exist ctxt tx_rollup in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Tx_rollup_state_storage.assert_exist ctxt tx_rollup in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [update] is valid.
Lemma update_is_valid ctxt tx_rollup t_value :
Raw_context.Valid.t ctxt →
Tx_rollup_state_repr.Valid.t t_value →
letP? ctxt := Tx_rollup_state_storage.update ctxt tx_rollup t_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tx_rollup_state_repr.Valid.t t_value →
letP? ctxt := Tx_rollup_state_storage.update ctxt tx_rollup t_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.