Skip to main content

🐆 Tx_rollup_l2_qty.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.

[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.
Lemma of_string_is_valid s q :
  Tx_rollup_l2_qty.of_string s = Some q
  Valid.t q.
Proof.
  unfold Tx_rollup_l2_qty.of_string;
  destruct of_string_opt eqn:Eoso; [|discriminate];
  hauto lq: on use: Int64.of_string_eq_some_implies_valid, of_int64_is_valid.
Qed.

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.
Lemma compact_encoding_is_valid :
  Data_encoding.Compact.Valid.t Valid.t Tx_rollup_l2_qty.compact_encoding.
Proof.
  intros.
  unfold Tx_rollup_l2_qty.compact_encoding.
  eapply Data_encoding.Compact.Valid.implies.
  eapply Data_encoding.Compact.Valid.conv_none.
  eapply Data_encoding.Compact.Valid.int64_value.
  intros. simpl.
  split;
    unfold Tx_rollup_l2_qty.of_int64_exn,
      Tx_rollup_l2_qty.of_int64,
      Tx_rollup_l2_qty.to_int64,
      Tx_rollup_l2_qty.op_lt;
    [lia|].
  now replace (x <i64 0) with false by lia.
Qed.
#[global] Hint Resolve compact_encoding_is_valid : Data_encoding_db.

[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 Compact.Valid.make.
  eapply 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.