🐆 Tx_rollup_l2_qty.v

Proofs

[compare] function is valid

Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Tx_rollup_l2_qty.compare.
Proof.
Compare.valid_auto.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Module Valid.

The validity predicate: a quantity is always within the int64 bounds and greater or equal to zero.

  Definition t (v : Tx_rollup_l2_qty.t) : Prop :=
    Int64.Valid.non_negative v.
  #[global] Hint Unfold t : tezos_z.
End Valid.

Module Add_unfold_to_tezos_z.
  Import Tx_rollup_l2_qty.

  #[global] Hint Unfold
    op_eq
    op_ltgt
    op_lt
    op_lteq
    op_gteq
    op_gt
    compare
    equal
    max
    min
    zero
    one
    to_int64
    to_z
    : tezos_z.
End Add_unfold_to_tezos_z.

The output of [of_int64] is valid. [of_int64] returns `None` if the argument is negative.

Lemma of_int64_is_valid q q' :
  Int64.Valid.t q →
  Tx_rollup_l2_qty.of_int64 q = Some q' →
  Valid.t q'.
Proof.
  unfold Tx_rollup_l2_qty.of_int64.
  step; [discriminate|].
  intros.
  replace q' with q by congruence.
  lia.
Qed.

[of_int64] behaves as the identity function.

Lemma of_int64_eq q :
  Valid.t q →
  Tx_rollup_l2_qty.of_int64 q = Some q.
Proof.
  unfold Tx_rollup_l2_qty.of_int64.
  step; lia.
Qed.

[of_int64_exn] builds a quantity from an int64 and raises `Invalid_argument` on negative quantities. [of_int64_exn] behaves as the identity function.

Lemma of_int64_exn_eq q :
  Valid.t q →
  Tx_rollup_l2_qty.of_int64_exn q = q.
Proof.
  intros.
  unfold Tx_rollup_l2_qty.of_int64_exn.
  now rewrite of_int64_eq.
Qed.

[to_int64] converts a quantity to int64, it behaves as the identity function.

Lemma to_int64_eq (q : Tx_rollup_l2_qty.t) :
Tx_rollup_l2_qty.to_int64 q = q.
Proof.
reflexivity.
Qed.

[to_z] converts a quantity to Z, behaves as the identity function.

Lemma to_z_eq (q : Tx_rollup_l2_qty.t) :
Tx_rollup_l2_qty.to_z q = q.
Proof.
reflexivity.
Qed.

The output of [of_string] is valid. [of_string] parses a quantity from a string. Returns `None` if the string is not a valid quantity representation.

The function [to_string] and [of_string] are inverses.

Lemma to_of_string s q :
  Tx_rollup_l2_qty.of_string s = Some q →
  Tx_rollup_l2_qty.to_string q = s.
Proof.
  unfold
    Tx_rollup_l2_qty.of_string,
    Tx_rollup_l2_qty.to_string,
    Tx_rollup_l2_qty.of_int64;
    specialize (Int64.to_string_of_string_opt s) as H;
    destruct of_string_opt; [|discriminate];
  hauto lq: on.
Qed.

The function [of_string] and [to_string] are inverses.

Lemma of_to_string q :
  Valid.t q →
  Tx_rollup_l2_qty.of_string (Tx_rollup_l2_qty.to_string q) = Some q.
Proof.
  unfold
    Tx_rollup_l2_qty.of_string,
    Tx_rollup_l2_qty.to_string;
  destruct of_string_opt eqn:Eoso;
    rewrite Int64.of_string_opt_to_string in Eoso; [|discriminate];
    injection Eoso as Eoso; rewrite Eoso; apply of_int64_eq.
Qed.

[Tx_rollup_l2_qty.compact_encoding] is a valid compact encoding.

[Tx_rollup_l2_qty.encoding] is a valid encodind.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Tx_rollup_l2_qty.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  apply Data_encoding.Compact.Valid.make.
  eapply Data_encoding.Compact.Valid.implies.
  apply compact_encoding_is_valid.
  trivial.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

The [sub] operator returns valid values. Returns None on subtraction underflow.

Lemma sub_is_valid q1 q2 q :
  Valid.t q1 →
  Valid.t q2 →
  Tx_rollup_l2_qty.sub q1 q2 = Some q →
  Valid.t q.
Proof.
  intros H1 H2;
  unfold
    Tx_rollup_l2_qty.sub,
    Tx_rollup_l2_qty.op_lteq;
  simpl;
  destruct (_ <=? _) eqn:E; [|discriminate];
  intros H; injection H as H; lia.
Qed.

The [sub] operator returns the substraction.

Lemma sub_eq q1 q2 q :
  Valid.t q1 →
  Valid.t q2 →
  Tx_rollup_l2_qty.sub q1 q2 = Some q →
  q = q1 -Z q2.
Proof.
  intros H1 H2;
  unfold
    Tx_rollup_l2_qty.sub,
    Tx_rollup_l2_qty.op_lteq;
  simpl;
  destruct (_ <=? _) eqn:E; [|discriminate];
  intros H; injection H as H; lia.
Qed.

The [add] operator returns valid values. Returns None on addition overflow.

Lemma add_is_valid q1 q2 q :
  Valid.t q1 →
  Valid.t q2 →
  Tx_rollup_l2_qty.add q1 q2 = Some q →
  Valid.t q.
Proof.
  intros H1 H2;
  unfold
    Tx_rollup_l2_qty.add,
    Tx_rollup_l2_qty.op_lt;
  simpl;
  destruct (_ <? _) eqn:E; [discriminate|].
  intros H; injection H as H; lia.
Qed.

The [add] operator returns the additions.

Lemma add_eq q1 q2 q :
  Valid.t q1 →
  Valid.t q2 →
  Tx_rollup_l2_qty.add q1 q2 = Some q →
  q = q1 +Z q2.
Proof.
  intros H1 H2;
  unfold
    Tx_rollup_l2_qty.add,
    Tx_rollup_l2_qty.op_lt;
  simpl;
  destruct (_ <? _) eqn:E; [discriminate|].
  intros H; injection H as H; lia.
Qed.