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