🇿 Zk_rollup_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Zk_rollup_account_repr.

The function [originate] is valid.

Lemma originate_is_valid ctxt static init_state :
  Raw_context.Valid.t ctxt →
  Zk_rollup_account_repr.static.Valid.t static →
  letP? '(ctxt, _, _) := Zk_rollup_storage.originate ctxt static init_state in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [_exists] is valid.

Lemma _exists_is_valid ctxt rollup :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Zk_rollup_storage._exists ctxt rollup in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.