🐆 Tx_rollup_l2_qty.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.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.
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.
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.
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.
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.
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.
Tx_rollup_l2_qty.to_int64 q = q.
Proof.
reflexivity.
Qed.
[to_z] converts a quantity to Z, behaves as the identity function.
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.
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.
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.
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.
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 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.
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.
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.
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.
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.