🐆 Tx_rollup_l2_context_sig.v

Proofs

See code, Gitlab , OCaml

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

Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context_sig.
Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Bls.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Indexable.
Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_qty.

The index [Ticket_indexable] is valid.

Lemma Ticket_indexable_is_valid :
  Indexable.INDEXABLE.Valid.t Tx_rollup_l2_context_sig.Ticket_indexable.
Proof.
  apply Indexable.Make_is_valid.
  constructor; simpl.
  { Data_encoding.Valid.data_encoding_auto. }
  { Compare.valid_auto. }
Qed.

Module address_index.
  Module Valid.

Validity predicate for [address_index].

    Definition t (x : Tx_rollup_l2_context_sig.address_index) : Prop :=
      Indexable.Index.Valid.t x.
  End Valid.
End address_index.

Module ticket_index.
  Module Valid.

Validity predicate for [ticket_index].

    Definition t (x : Tx_rollup_l2_context_sig.ticket_index) : Prop :=
      Indexable.Index.Valid.t x.
  End Valid.
End ticket_index.

Module metadata.
  Module Valid.
    Import Proto_alpha.Tx_rollup_l2_context_sig.metadata.

Validity predicate for [metadata].

    Record t (x : Tx_rollup_l2_context_sig.metadata) : Prop := {
      counter : Int64.Valid.t x.(counter);
    }.
  End Valid.
End metadata.

Module SYNTAX.
  Module Valid.
    Import Proto_alpha.Tx_rollup_l2_context_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_context_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);
      op_letstarquestion {a b : Set}
        (x : Pervasives.result a Error_monad._error) (f : a → m b) :
        M.(op_letstarquestion) x f =
        match x with
        | Pervasives.Ok value ⇒ f value
        | Pervasives.Error err ⇒ M.(fail) err
        end;
      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);
      fail_unless condition err :
        M.(fail_unless) condition err =
        if condition then
          M.(Tx_rollup_l2_context_sig.SYNTAX._return) tt
        else
          M.(Tx_rollup_l2_context_sig.SYNTAX.fail) err;
      fail_when condition err :
        M.(fail_when) condition err =
        if condition then
          M.(Tx_rollup_l2_context_sig.SYNTAX.fail) err
        else
          M.(Tx_rollup_l2_context_sig.SYNTAX._return) tt;
    }.
    Arguments t {_}.
  End Valid.
End SYNTAX.

Module ADDRESS_METADATA.
  Module Valid.
    Import Proto_alpha.Tx_rollup_l2_context_sig.ADDRESS_METADATA.

Validity predicate for the signature [ADDRESS_METADATA].

    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_context_sig.ADDRESS_METADATA (t := t) (m := m)) :
      Prop := {
      get ctxt index :
        P_t ctxt →
        address_index.Valid.t index →
        with_post (Option.Forall metadata.Valid.t) (M.(get) ctxt index);
      incr_counter ctxt index :
        P_t ctxt →
        address_index.Valid.t index →
        with_post P_t (M.(incr_counter) ctxt index);
      init_with_public_key ctxt index pk :
        P_t ctxt →
        address_index.Valid.t index →
        with_post P_t (M.(init_with_public_key) ctxt index pk);
    }.
  End Valid.
End ADDRESS_METADATA.

Module INDEX.
  Module Valid.
    Import Proto_alpha.Tx_rollup_l2_context_sig.INDEX.

Validity predicate for the signature [INDEX].

    Record t {t : Set} {m : Set → Set} {hash index : 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)
      (P_index : index → Prop)
      (M :
        Tx_rollup_l2_context_sig.INDEX
          (t := t) (m := m) (hash := hash) (index := index)
      ) :
      Prop := {
      init_counter ctxt :
        P_t ctxt →
        with_post P_t (M.(init_counter) ctxt);
      get ctxt hash :
        P_t ctxt →
        with_post (Option.Forall P_index) (M.(get) ctxt hash);
      get_or_associate_index ctxt hash :
        P_t ctxt →
        with_post (fun '(ctxt, _, index) ⇒ P_t ctxt ∧ P_index index)
          (M.(get_or_associate_index) ctxt hash);
      count ctxt :
        P_t ctxt →
        with_post Int32.Valid.non_negative (M.(count) ctxt);
    }.
  End Valid.
End INDEX.

Module TICKET_LEDGER.
  Module Valid.
    Import Proto_alpha.Tx_rollup_l2_context_sig.TICKET_LEDGER.

Validity predicate for the signature [TICKET_LEDGER].

    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_context_sig.TICKET_LEDGER (t := t) (m := m)) :
      Prop := {
      get ctxt ticket address :
        P_t ctxt →
        ticket_index.Valid.t ticket →
        address_index.Valid.t address →
        with_post Tx_rollup_l2_qty.Valid.t (M.(get) ctxt ticket address);
      credit ctxt ticket address qty :
        P_t ctxt →
        ticket_index.Valid.t ticket →
        address_index.Valid.t address →
        Tx_rollup_l2_qty.Valid.t qty →
        with_post P_t (M.(credit) ctxt ticket address qty);
      spend ctxt ticket address qty :
        P_t ctxt →
        ticket_index.Valid.t ticket →
        address_index.Valid.t address →
        Tx_rollup_l2_qty.Valid.t qty →
        with_post P_t (M.(spend) ctxt ticket address qty);
    }.
  End Valid.
End TICKET_LEDGER.

Module CONTEXT.
  Module Valid.
    Import Proto_alpha.Tx_rollup_l2_context_sig.CONTEXT.

Validity predicate for the signature [CONTEXT].

    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_context_sig.CONTEXT (t := t) (m := m)) :
      Prop := {
      Syntax : SYNTAX.Valid.t (@with_post) M.(Syntax);
      bls_verify l signature :
        with_post (fun _ ⇒ True) (M.(bls_verify) l signature);
      Address_metadata :
        ADDRESS_METADATA.Valid.t P_t (@with_post) M.(Address_metadata);
      Address_index :
        INDEX.Valid.t P_t (@with_post) address_index.Valid.t M.(Address_index);
      Ticket_index :
        INDEX.Valid.t P_t (@with_post) ticket_index.Valid.t M.(Ticket_index);
      Ticket_ledger :
        TICKET_LEDGER.Valid.t P_t (@with_post) M.(Ticket_ledger);
    }.
  End Valid.
End CONTEXT.