🐆 Tx_rollup_l2_storage_sig.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_storage_sig.
Module SYNTAX.
Module Valid.
Import Proto_alpha.Tx_rollup_l2_storage_sig.SYNTAX.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_storage_sig.
Module SYNTAX.
Module Valid.
Import Proto_alpha.Tx_rollup_l2_storage_sig.SYNTAX.
Validity predicate for the signature [SYNTAX].
Record t {m : Set → Set}
(* Verifies a post-condition on the result of a monadic expression. *)
(with_post : ∀ {a : Set}, (a → Prop) → m a → Prop)
(M : Tx_rollup_l2_storage_sig.SYNTAX (m := m)) :
Prop := {
op_letplus {a b : Set} (x : m a) (f : a → b)
(P : a → Prop) (Q : b → Prop) :
with_post P x →
(∀ x, P x → Q (f x)) →
with_post Q (M.(op_letplus) x f);
op_letstar {a b : Set} (x : m a) (f : a → m b)
(P : a → Prop) (Q : b → Prop) :
with_post P x →
(∀ x, P x → with_post Q (f x)) →
with_post Q (M.(op_letstar) x f);
fail {a : Set} (err : Error_monad._error) (P : a → Prop) :
Error.not_internal [err] →
with_post P (M.(fail) err);
catch {a b : Set} (x : m a) (f : a → m b)
(handler : Error_monad._error → m b)
(P : a → Prop) (Q : b → Prop) :
with_post P x →
(∀ x, P x → with_post Q (f x)) →
(∀ err, with_post Q (handler err)) →
with_post Q (M.(catch) x f handler);
_return {a : Set} (x : a) (P : a → Prop) :
P x →
with_post P (M.(_return) x);
list_fold_left_m {a b : Set} (f : a → b → m a) (acc : a) (l : list b)
(P_acc : a → Prop) (P_item : b → Prop) :
(∀ acc item,
P_acc acc →
P_item item →
with_post P_acc (f acc item)
) →
P_acc acc →
List.Forall P_item l →
with_post P_acc (M.(list_fold_left_m) f acc l);
}.
End Valid.
End SYNTAX.
Module STORAGE.
Module Valid.
Import Proto_alpha.Tx_rollup_l2_storage_sig.STORAGE.
(* Verifies a post-condition on the result of a monadic expression. *)
(with_post : ∀ {a : Set}, (a → Prop) → m a → Prop)
(M : Tx_rollup_l2_storage_sig.SYNTAX (m := m)) :
Prop := {
op_letplus {a b : Set} (x : m a) (f : a → b)
(P : a → Prop) (Q : b → Prop) :
with_post P x →
(∀ x, P x → Q (f x)) →
with_post Q (M.(op_letplus) x f);
op_letstar {a b : Set} (x : m a) (f : a → m b)
(P : a → Prop) (Q : b → Prop) :
with_post P x →
(∀ x, P x → with_post Q (f x)) →
with_post Q (M.(op_letstar) x f);
fail {a : Set} (err : Error_monad._error) (P : a → Prop) :
Error.not_internal [err] →
with_post P (M.(fail) err);
catch {a b : Set} (x : m a) (f : a → m b)
(handler : Error_monad._error → m b)
(P : a → Prop) (Q : b → Prop) :
with_post P x →
(∀ x, P x → with_post Q (f x)) →
(∀ err, with_post Q (handler err)) →
with_post Q (M.(catch) x f handler);
_return {a : Set} (x : a) (P : a → Prop) :
P x →
with_post P (M.(_return) x);
list_fold_left_m {a b : Set} (f : a → b → m a) (acc : a) (l : list b)
(P_acc : a → Prop) (P_item : b → Prop) :
(∀ acc item,
P_acc acc →
P_item item →
with_post P_acc (f acc item)
) →
P_acc acc →
List.Forall P_item l →
with_post P_acc (M.(list_fold_left_m) f acc l);
}.
End Valid.
End SYNTAX.
Module STORAGE.
Module Valid.
Import Proto_alpha.Tx_rollup_l2_storage_sig.STORAGE.
Validity predicate for the signature [STORAGE].
Record t {t : Set} {m : Set → Set}
(P_t : t → Prop)
(* Verifies a post-condition on the result of a monadic expression. *)
(with_post : ∀ {a : Set}, (a → Prop) → m a → Prop)
(M : Tx_rollup_l2_storage_sig.STORAGE (t := t) (m := m)) :
Prop := {
Syntax : SYNTAX.Valid.t (@with_post) M.(Syntax);
get storage key :
P_t storage →
with_post (fun _ ⇒ True) (M.(get) storage key);
set storage key value :
P_t storage →
with_post P_t (M.(set) storage key value);
remove storage key :
P_t storage →
with_post P_t (M.(remove) storage key);
}.
End Valid.
End STORAGE.
(P_t : t → Prop)
(* Verifies a post-condition on the result of a monadic expression. *)
(with_post : ∀ {a : Set}, (a → Prop) → m a → Prop)
(M : Tx_rollup_l2_storage_sig.STORAGE (t := t) (m := m)) :
Prop := {
Syntax : SYNTAX.Valid.t (@with_post) M.(Syntax);
get storage key :
P_t storage →
with_post (fun _ ⇒ True) (M.(get) storage key);
set storage key value :
P_t storage →
with_post P_t (M.(set) storage key value);
remove storage key :
P_t storage →
with_post P_t (M.(remove) storage key);
}.
End Valid.
End STORAGE.