Skip to main content

🐆 Tx_rollup_l2_context.v

Proofs

See code, Gitlab , OCaml

The encoding [metadata_encoding] is valid.
Lemma metadata_encoding_is_valid :
  Data_encoding.Valid.t Tx_rollup_l2_context_sig.metadata.Valid.t
    Tx_rollup_l2_context.metadata_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Admitted.
#[global] Hint Resolve metadata_encoding_is_valid : Data_encoding_db.

Module key.
  Module Valid.
Validity predicate for [key].
    Definition t (x : Tx_rollup_l2_context.key) : Prop :=
      match x with
      | Tx_rollup_l2_context.Address_metadata address
        Tx_rollup_l2_context_sig.address_index.Valid.t address
      | Tx_rollup_l2_context.Address_countTrue
      | Tx_rollup_l2_context.Address_index _True
      | Tx_rollup_l2_context.Ticket_countTrue
      | Tx_rollup_l2_context.Ticket_index _True
      | Tx_rollup_l2_context.Ticket_ledger ticket address
        Tx_rollup_l2_context_sig.ticket_index.Valid.t ticket
        Tx_rollup_l2_context_sig.address_index.Valid.t address
      end.
  End Valid.
End key.

Module packed_key.
  Module Valid.
Validity predicate for [packed_key].
    Definition t (x : Tx_rollup_l2_context.packed_key) : Prop :=
      match x with
      | Tx_rollup_l2_context.Key keykey.Valid.t key
      end.
  End Valid.
End packed_key.

The encoding [packed_key_encoding] is valid.
Lemma packed_key_encoding_is_valid :
  Data_encoding.Valid.t packed_key.Valid.t
    Tx_rollup_l2_context.packed_key_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros [[]] ?; simpl in *; try easy.
  destruct_all Tx_rollup_l2_context_sig.ticket_index; simpl in *; try easy.
  repeat split; try lia.
  easy.
Qed.
#[global] Hint Resolve packed_key_encoding_is_valid : Data_encoding_db.

Type corresponding to a [key].
Validity predicate for the type corresponding to a [key].
The generator of encodings [value_encoding] is valid.
Lemma value_encoding_is_valid key :
  Data_encoding.Valid.t (key_to_Set.Valid.t key)
    (Tx_rollup_l2_context.value_encoding (a := key_to_Set key) key).
Proof.
  destruct key; simpl; rewrite cast_eval;
    Data_encoding.Valid.data_encoding_auto.
  { lia. }
  { lia. }
  { intros [] ?; simpl in *; try easy.
    split; lia.
  }
Qed.
#[global] Hint Resolve value_encoding_is_valid : Data_encoding_db.

Module Make.
  Import Proto_alpha.Tx_rollup_l2_context.Make.

  Section Make.
    Context `{FArgs}
      (P_t : S_t Prop)
      (with_post : {a : Set}, (a Prop) S_m a Prop)
      (H_S : Tx_rollup_l2_storage_sig.STORAGE.Valid.t P_t (@with_post) S).

    Arguments with_post {_}.

The module [Syntax] is valid.
    Lemma Syntax_is_valid :
      Tx_rollup_l2_context_sig.SYNTAX.Valid.t (@with_post) Syntax.
    Proof.
      sfirstorder.
    Qed.

The function [bls_verify] is valid.
    Lemma bls_verify_is_valid l signature :
      with_post (fun _True) (bls_verify l signature).
    Proof.
      sfirstorder.
    Qed.

The function [unwrap_or] is valid.
    Lemma unwrap_or_is_valid {a : Set} (P : a Prop) (opt : option a) err
      (H_opt : Option.Forall P opt)
      (H_err : Error.not_internal [err]) :
      with_post P (unwrap_or opt err).
    Proof.
      destruct opt; simpl in *; now apply Syntax_is_valid.
    Qed.

The function [serialize_key] is valid.
    Lemma serialize_key_is_valid key_value
      (H_key_value : key.Valid.t key_value) :
      with_post (fun _True) (serialize_key key_value).
    Proof.
      unfold serialize_key, unwrap_or.
      destruct packed_key_encoding_is_valid.
      pose proof (of_bytes_opt_to_bytes_opt
        (Tx_rollup_l2_context.Key key_value) H_key_value
      ).
      destruct Data_encoding.Binary.to_bytes_opt; [|contradiction].
      now apply Syntax_is_valid.
    Qed.

The function [serialize_value] is valid.
    Lemma serialize_value_is_valid {a : Set} (P : a Prop) encoding value
      (H_encoding : Data_encoding.Valid.t P encoding)
      (H_value : P value) :
      with_post (fun _True) (serialize_value encoding value).
    Proof.
      unfold serialize_value, unwrap_or.
      destruct H_encoding.
      pose proof (of_bytes_opt_to_bytes_opt value H_value).
      destruct Data_encoding.Binary.to_bytes_opt; now apply Syntax_is_valid.
    Qed.

The function [deserialize_value] is valid.
    Lemma deserialize_value_is_valid {a : Set} (P : a Prop) encoding value
      (H_encoding : Data_encoding.Valid.t P encoding) :
      with_post P (deserialize_value encoding value).
    Proof.
      unfold deserialize_value, unwrap_or.
      destruct H_encoding.
      pose proof (to_bytes_opt_of_bytes_opt value).
      destruct Data_encoding.Binary.of_bytes_opt; now apply Syntax_is_valid.
    Qed.

The function [get] is valid.
    Lemma get_is_valid ctxt key_value
      (H_ctxt : P_t ctxt)
      (H_key_value : key.Valid.t key_value) :
      with_post (Option.Forall (key_to_Set.Valid.t key_value))
        (get ctxt key_value).
    Proof.
      unfold get.
      eapply Syntax_is_valid. {
        now apply serialize_key_is_valid.
      }
      intros.
      eapply Syntax_is_valid. {
        now apply H_S.
      }
      intros [] ?.
      { eapply Syntax_is_valid. {
          apply deserialize_value_is_valid.
          apply value_encoding_is_valid.
        }
        intros.
        now apply Syntax_is_valid.
      }
      { now apply Syntax_is_valid. }
    Qed.

The function [set] is valid.
    Lemma set_is_valid ctxt key_value value
      (H_ctxt : P_t ctxt)
      (H_key_value : key.Valid.t key_value)
      (H_value : key_to_Set.Valid.t key_value value) :
      with_post P_t (set ctxt key_value value).
    Proof.
      unfold set.
      eapply Syntax_is_valid. {
        now apply serialize_key_is_valid.
      }
      intros.
      eapply Syntax_is_valid. {
        apply serialize_value_is_valid with (P := key_to_Set.Valid.t key_value);
          try easy.
        apply value_encoding_is_valid.
      }
      intros.
      now apply H_S.
    Qed.

The function [remove] is valid.
    Lemma remove_is_valid ctxt key_value
      (H_ctxt : P_t ctxt)
      (H_key_value : key.Valid.t key_value) :
      with_post P_t (remove ctxt key_value).
    Proof.
      unfold remove.
      eapply Syntax_is_valid. {
        now apply serialize_key_is_valid.
      }
      intros.
      now apply H_S.
    Qed.

The function [Address_metadata.get] is valid.
    Lemma Address_metadata_get_is_valid ctxt index
      (H_ctxt : P_t ctxt)
      (H_index : Tx_rollup_l2_context_sig.address_index.Valid.t index) :
      with_post (Option.Forall Tx_rollup_l2_context_sig.metadata.Valid.t)
        (Address_metadata.get ctxt index).
    Proof.
      unfold Address_metadata.get.
      now apply get_is_valid with
        (key_value := Tx_rollup_l2_context.Address_metadata index).
    Qed.

The module [Address_metadata] is valid.
    Lemma Address_metadata_is_valid :
      Tx_rollup_l2_context_sig.ADDRESS_METADATA.Valid.t P_t (@with_post)
        Address_metadata.
    Proof.
      constructor; intros; simpl.
      { grep Address_metadata.get.
        now apply Address_metadata_get_is_valid.
      }
      { grep Address_metadata.incr_counter.
        unfold Address_metadata.incr_counter.
        eapply Syntax_is_valid. {
          now apply Address_metadata_get_is_valid.
        }
        intros [] ?; simpl in ×.
        { eapply Syntax_is_valid with (P := fun _True). {
            destruct (_ >=? _); simpl; now apply Syntax_is_valid.
          }
          intros.
          apply set_is_valid; simpl; try easy.
          constructor; simpl.
          lia.
        }
        { now apply Syntax_is_valid. }
      }
      { grep Address_metadata.init_with_public_key.
        unfold Address_metadata.init_with_public_key.
        eapply Syntax_is_valid. {
          now apply Address_metadata_get_is_valid.
        }
        intros [] ?; simpl in ×.
        { now apply Syntax_is_valid. }
        { now apply set_is_valid. }
      }
    Qed.

The function [Address_index.count] is valid.
    Lemma Address_index_count_is_valid ctxt
      (H_ctxt : P_t ctxt) :
      with_post Int32.Valid.non_negative (Address_index.count ctxt).
    Proof.
      eapply Syntax_is_valid. {
        now apply get_is_valid with
          (key_value := Tx_rollup_l2_context.Address_count).
      }
      now intros [] ?.
    Qed.

The function [Address_index.associate_index] is valid.
    Lemma Address_index_associate_index_is_valid ctxt addr
      (H_ctxt : P_t ctxt) :
      with_post
        (fun '(ctxt, index)
          P_t ctxt
          Tx_rollup_l2_context_sig.address_index.Valid.t index
        )
        (Address_index.associate_index ctxt addr).
    Proof.
      unfold Address_index.associate_index.
      eapply Syntax_is_valid. {
        now apply Address_index_count_is_valid.
      }
      intros i_value H_i_value.
      eapply Syntax_is_valid with
        (P := fun _Int32.succ i_value i_value). {
        destruct (_ i32 _) eqn:?; simpl; apply Syntax_is_valid; [lia|easy].
      }
      intros.
      unfold Indexable.index_exn, Indexable.index_value.
      eapply Syntax_is_valid. {
        apply set_is_valid; try easy.
        destruct (_ i32 _) eqn:?; simpl; lia.
      }
      intros.
      eapply Syntax_is_valid. {
        apply set_is_valid; simpl; try easy.
        lia.
      }
      intros.
      split; try easy.
      destruct (_ i32 _) eqn:?; simpl; lia.
    Qed.

The function [Address_index.get] is valid.
    Lemma Address_index_get_is_valid ctxt addr
      (H_ctxt : P_t ctxt) :
      with_post (Option.Forall Tx_rollup_l2_context_sig.address_index.Valid.t)
        (Address_index.get ctxt addr).
    Proof.
      unfold Address_index.get.
      now apply get_is_valid with
        (key_value := Tx_rollup_l2_context.Address_index addr).
    Qed.

The module [Address_index] is valid.
    Lemma Address_index_is_valid :
      Tx_rollup_l2_context_sig.INDEX.Valid.t
        P_t (@with_post)
        Tx_rollup_l2_context_sig.address_index.Valid.t
        Address_index.
    Proof.
      constructor; intros; simpl.
      { grep Address_index.init_counter.
        unfold Address_index.init_counter.
        now apply set_is_valid.
      }
      { grep Address_index.get.
        now apply Address_index_get_is_valid.
      }
      { grep Address_index.get_or_associate_index.
        unfold Address_index.get_or_associate_index.
        eapply Syntax_is_valid. {
          now apply Address_index_get_is_valid.
        }
        intros [] ?; simpl in ×.
        { now apply Syntax_is_valid. }
        { eapply Syntax_is_valid. {
            now apply Address_index_associate_index_is_valid.
          }
          now intros; Tactics.destruct_pairs.
        }
      }
      { grep Address_index.count.
        now apply Address_index_count_is_valid.
      }
    Qed.

The function [Ticket_index.count] is valid.
    Lemma Ticket_index_count_is_valid ctxt
      (H_ctxt : P_t ctxt) :
      with_post Int32.Valid.non_negative (Ticket_index.count ctxt).
    Proof.
      eapply Syntax_is_valid. {
        now apply get_is_valid with
          (key_value := Tx_rollup_l2_context.Ticket_count).
      }
      now intros [] ?.
    Qed.

The function [Ticket_index.associate_index] is valid.
    Lemma Ticket_index_associate_index_is_valid ctxt addr
      (H_ctxt : P_t ctxt) :
      with_post
        (fun '(ctxt, index)
          P_t ctxt
          Tx_rollup_l2_context_sig.ticket_index.Valid.t index
        )
        (Ticket_index.associate_index ctxt addr).
    Proof.
      unfold Ticket_index.associate_index.
      eapply Syntax_is_valid. {
        now apply Ticket_index_count_is_valid.
      }
      intros i_value H_i_value.
      eapply Syntax_is_valid with
        (P := fun _Int32.succ i_value i_value). {
        destruct (_ i32 _) eqn:?; simpl; apply Syntax_is_valid; [lia|easy].
      }
      intros.
      unfold Indexable.index_exn, Indexable.index_value.
      eapply Syntax_is_valid. {
        apply set_is_valid; try easy.
        destruct (_ i32 _) eqn:?; simpl; lia.
      }
      intros.
      eapply Syntax_is_valid. {
        apply set_is_valid; simpl; try easy.
        lia.
      }
      intros.
      split; try easy.
      destruct (_ i32 _) eqn:?; simpl; lia.
    Qed.

The function [Ticket_index.get] is valid.
    Lemma Ticket_index_get_is_valid ctxt addr
      (H_ctxt : P_t ctxt) :
      with_post (Option.Forall Tx_rollup_l2_context_sig.ticket_index.Valid.t)
        (Ticket_index.get ctxt addr).
    Proof.
      unfold Ticket_index.get.
      now apply get_is_valid with
        (key_value := Tx_rollup_l2_context.Ticket_index addr).
    Qed.

The module [Ticket_index] is valid.
    Lemma Ticket_index_is_valid :
      Tx_rollup_l2_context_sig.INDEX.Valid.t
        P_t (@with_post)
        Tx_rollup_l2_context_sig.ticket_index.Valid.t
        Ticket_index.
    Proof.
      constructor; intros; simpl.
      { grep Ticket_index.init_counter.
        unfold Ticket_index.init_counter.
        now apply set_is_valid.
      }
      { grep Ticket_index.get.
        now apply Ticket_index_get_is_valid.
      }
      { grep Ticket_index.get_or_associate_index.
        unfold Ticket_index.get_or_associate_index.
        eapply Syntax_is_valid. {
          now apply Ticket_index_get_is_valid.
        }
        intros [] ?; simpl in ×.
        { now apply Syntax_is_valid. }
        { eapply Syntax_is_valid. {
            now apply Ticket_index_associate_index_is_valid.
          }
          now intros; Tactics.destruct_pairs.
        }
      }
      { grep Ticket_index.count.
        now apply Ticket_index_count_is_valid.
      }
    Qed.

The function [Ticket_ledger.get_opt] is valid.
    Lemma Ticket_ledger_get_opt_is_valid ctxt tidx aidx
      (H_ctxt : P_t ctxt)
      (H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
      (H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
      with_post (Option.Forall Tx_rollup_l2_qty.Valid.t)
        (Ticket_ledger.get_opt ctxt tidx aidx).
    Proof.
      unfold Ticket_ledger.get_opt.
      now apply get_is_valid with
        (key_value := Tx_rollup_l2_context.Ticket_ledger tidx aidx).
    Qed.

The function [Ticket_ledger.get] is valid.
    Lemma Ticket_ledger_get_is_valid ctxt tidx aidx
      (H_ctxt : P_t ctxt)
      (H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
      (H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
      with_post Tx_rollup_l2_qty.Valid.t (Ticket_ledger.get ctxt tidx aidx).
    Proof.
      unfold Ticket_ledger.get.
      eapply Syntax_is_valid. {
        now apply Ticket_ledger_get_opt_is_valid.
      }
      now intros [] ?; simpl in ×.
    Qed.

The function [Ticket_ledger.set] is valid.
    Lemma Ticket_ledger_set_is_valid ctxt tidx aidx qty
      (H_ctxt : P_t ctxt)
      (H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
      (H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx)
      (H_qty : Tx_rollup_l2_qty.Valid.t qty) :
      with_post P_t (Ticket_ledger.set ctxt tidx aidx qty).
    Proof.
      unfold Ticket_ledger.set.
      now apply set_is_valid.
    Qed.

The function [Ticket_ledger.remove] is valid.
    Lemma Ticket_ledger_remove_is_valid ctxt tidx aidx
      (H_ctxt : P_t ctxt)
      (H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
      (H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
      with_post P_t (Ticket_ledger.remove ctxt tidx aidx).
    Proof.
      unfold Ticket_ledger.remove.
      now apply remove_is_valid.
    Qed.

The module [Ticket_ledger] is valid.
    Lemma Ticket_ledger_is_valid :
      Tx_rollup_l2_context_sig.TICKET_LEDGER.Valid.t
        P_t (@with_post)
        Ticket_ledger.
    Proof.
      constructor; intros; simpl.
      { grep Ticket_ledger.get.
        now apply Ticket_ledger_get_is_valid.
      }
      { grep Ticket_ledger.credit.
        eapply Syntax_is_valid. {
          now apply Ticket_ledger_get_is_valid.
        }
        intros.
        step.
        { apply Ticket_ledger_set_is_valid; try easy.
          hauto l: on use: Tx_rollup_l2_qty.add_is_valid.
        }
        { now apply Syntax_is_valid. }
      }
      { grep Ticket_ledger.spend.
        eapply Syntax_is_valid. {
          now apply Ticket_ledger_get_is_valid.
        }
        intros.
        step.
        { step; [
            apply Ticket_ledger_set_is_valid |
            apply Ticket_ledger_remove_is_valid
          ]; try easy.
          hauto l: on use: Tx_rollup_l2_qty.sub_is_valid.
        }
        { now apply Syntax_is_valid. }
      }
    Qed.

The functor [functor] is valid.
    Lemma functor_is_valid :
      Tx_rollup_l2_context_sig.CONTEXT.Valid.t P_t (@with_post) functor.
    Proof.
      constructor; simpl.
      { apply Syntax_is_valid. }
      { apply bls_verify_is_valid. }
      { apply Address_metadata_is_valid. }
      { apply Address_index_is_valid. }
      { apply Ticket_index_is_valid. }
      { apply Ticket_ledger_is_valid. }
    Qed.
  End Make.
End Make.

The functor [Make] is valid.
Lemma Make_is_valid {S_t : Set} {S_m : Set Set}
  (P_t : S_t Prop)
  (with_post : {a : Set}, (a Prop) S_m a Prop)
  (S : Tx_rollup_l2_storage_sig.STORAGE (t := S_t) (m := S_m))
  (H_S : Tx_rollup_l2_storage_sig.STORAGE.Valid.t P_t (@with_post) S) :
  Tx_rollup_l2_context_sig.CONTEXT.Valid.t P_t (@with_post)
    (Tx_rollup_l2_context.Make S).
Proof.
  now apply Make.functor_is_valid.
Qed.