🐆 Tx_rollup_state_storage.v

Proofs

See code, Gitlab , OCaml

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.

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.

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.

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.

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.

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.