Skip to main content

🐆 Tx_rollup_l2_storage_sig.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_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.

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.