🕰️ Period_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.RPC_arg.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int64.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int32.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.RPC_arg.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int64.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int32.
Simplifly hypothesis Valid.t to work with lia
#[local] Ltac simpl_tezos_z H :=
repeat (simpl in H; autounfold with tezos_z in H);
try (rewrite Bool.andb_true_iff in H; destruct H).
Module Valid.
Definition t (period : Period_repr.t) : Prop :=
0 ≤ period ≤ Int64.max_int.
End Valid.
Module Internal.
#[global] Hint Unfold
Valid.t
Period_repr.Internal.create
Period_repr.Internal.mult_
Period_repr.Internal.add_
Period_repr.Internal.op_ltgt
Period_repr.Internal.op_eq
Period_repr.Internal.op_lt
Period_repr.Internal.op_gt
Period_repr.Internal.op_lteq
Period_repr.Internal.op_gteq
Period_repr.Internal.zero
Period_repr.Internal.one
: tezos_z.
Lemma encoding_is_valid
: Data_encoding.Valid.t Valid.t Period_repr.Internal.encoding.
Data_encoding.Valid.data_encoding_auto.
autounfold with tezos_z.
hauto q: on solve: lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
repeat (simpl in H; autounfold with tezos_z in H);
try (rewrite Bool.andb_true_iff in H; destruct H).
Module Valid.
Definition t (period : Period_repr.t) : Prop :=
0 ≤ period ≤ Int64.max_int.
End Valid.
Module Internal.
#[global] Hint Unfold
Valid.t
Period_repr.Internal.create
Period_repr.Internal.mult_
Period_repr.Internal.add_
Period_repr.Internal.op_ltgt
Period_repr.Internal.op_eq
Period_repr.Internal.op_lt
Period_repr.Internal.op_gt
Period_repr.Internal.op_lteq
Period_repr.Internal.op_gteq
Period_repr.Internal.zero
Period_repr.Internal.one
: tezos_z.
Lemma encoding_is_valid
: Data_encoding.Valid.t Valid.t Period_repr.Internal.encoding.
Data_encoding.Valid.data_encoding_auto.
autounfold with tezos_z.
hauto q: on solve: lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[compare] function is valid
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Period_repr.Internal.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
Compare.Valid.t (fun _ ⇒ True) id Period_repr.Internal.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
Helper lemmas
Lemma create_eq : ∀ {i : int64},
Valid.t i →
Period_repr.Internal.create i = Some i.
repeat (autounfold with tezos_z; simpl).
intros.
assert (Hi : i >=? 0 = true) by lia.
now rewrite Hi.
Qed.
Lemma create_eq_32 : ∀ {i : int32},
Valid.t i →
Period_repr.Internal.create (Int64.of_int32 i) = Some i.
unfold Int64.of_int32.
intros.
apply create_eq. assumption.
Qed.
Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Period_repr.Internal.rpc_arg.
unfold Valid.t.
simpl. autounfold with tezos_z.
unfold Period_repr.Internal.rpc_arg.
eapply RPC_arg.Valid.implies.
apply RPC_arg.Valid.uint63. simpl.
autounfold with tezos_z; lia.
Qed.
Lemma create_is_valid : ∀ {x : int64},
Int64.Valid.t x →
match Period_repr.Internal.create x with
| Some y ⇒ Valid.t y
| None ⇒ True
end.
Utils.tezos_z_autounfold. simpl.
intros. unfold Period_repr.Internal.create.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end.
simpl_tezos_z H.
repeat simpl_tezos_z Heqb.
repeat (autounfold with tezos_z; simpl).
{ lia. }
{ constructor. }
Qed.
Lemma mult__is_valid : ∀ {a b : Period_repr.t},
Valid.t a →
Valid.t b →
match Period_repr.Internal.mult_ a b with
| Some c ⇒ Valid.t c
| None ⇒ True
end.
#[local] Hint Unfold
two_pow_63
two_pow_64
max_int : lia_fin.
#[local] Hint Unfold normalize_int64 : tezos_z.
unfold Int64, "/Z"; simpl.
unfold
Period_repr.Internal.mult_,
Period_repr.Internal.op_ltgt,
Period_repr.Internal.zero,
Valid.t, Int64.mul, Int64.div, normalize_int64, mul, div; simpl.
intros a b [Ha1 Ha2] [Hb1 Hb2].
destruct (Z.eqb_spec a 0); simpl; [lia|].
remember ((a × b + two_pow_63) mod two_pow_64 - two_pow_63) as ab64.
remember ((ab64 / a + two_pow_63) mod two_pow_64 - two_pow_63) as aba64.
destruct (Z.eqb_spec aba64 b); simpl; [|auto]; split;
[|subst;autounfold with lia_fin; lia].
assert(b + two_pow_63 ≤ (ab64/a + two_pow_63) mod two_pow_64) by lia.
assert((ab64 / a + two_pow_63) mod two_pow_64 =
ab64 / a + two_pow_63 -
two_pow_64 × ((ab64 / a + two_pow_63) / two_pow_64)).
apply Z.mod_eq; [autounfold with lia_fin; lia].
assert(ab64 / a + two_pow_63 ≥ 0).
{
destruct(Z.leb_spec0 0 ab64).
- assert(ab64 / a ≥ 0) by (apply Z_div_ge0; lia).
unfold two_pow_63; lia.
- assert( -two_pow_63 ≤ ab64).
{
specialize(Int64.normalize_is_valid (a × b)%Z).
subst; autounfold with tezos_z; lia.
}
assert( -two_pow_63 ≤ ab64 / a ).
{
apply Zdiv_le_lower_bound; [lia|].
assert(- two_pow_63 × a ≤ - two_pow_63)
by (apply Z.le_mul_diag_l; [autounfold with lia_fin|]; lia); lia.
}
lia.
}
assert(0%Z ≤ two_pow_64 × ((ab64 / a + two_pow_63) / two_pow_64)).
apply Z.mul_nonneg_nonneg; [autounfold with lia_fin; lia|].
apply Zdiv_le_lower_bound; [autounfold with lia_fin|]; lia.
nia.
Qed.
Lemma mult__eq : ∀ {a b : Period_repr.t},
Valid.t a →
Valid.t b →
Int64.Valid.t (a × b)%Z →
Period_repr.Internal.mult_ a b = Some (a ×i64 b).
Utils.tezos_z_autounfold. simpl. unfold "/Z".
intros.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end.
assert ((((a × b + 9223372036854775808) mod 18446744073709551616 -
9223372036854775808) / a + 9223372036854775808)
mod 18446744073709551616 - 9223372036854775808 = b).
{
assert (Hnon0 : a ≠ 0) by lia.
clear Heqb0.
rewrite Z.mod_eq.
fold two_pow_63.
fold two_pow_64.
replace ((a × b + two_pow_63) mod two_pow_64 - two_pow_63)
with (Pervasives.normalize_int64 (a × b)) by reflexivity.
rewrite Int64.normalize_identity.
rewrite (Z.mul_comm a b).
rewrite (Z.div_mul).
{ Utils.tezos_z_auto. }
{ assumption. }
{ Utils.tezos_z_auto. }
{ lia. }
}
rewrite H2. rewrite Z.eqb_refl. simpl.
{ reflexivity. }
{ f_equal. lia. }
Qed.
Lemma add__is_valid : ∀ {a b : Period_repr.t},
Valid.t a →
Valid.t b →
match Period_repr.Internal.add_ a b with
| Some c ⇒ Valid.t c
| None ⇒ True
end.
unfold Period_repr.Internal.add_.
Utils.tezos_z_autounfold. simpl.
intros.
repeat match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end; try constructor; try lia.
rewrite Bool.orb_false_iff in Heqb0.
destruct Heqb0.
lia.
Qed.
End Internal.
Lemma of_seconds_is_valid : ∀ {secs : int64},
Valid.t secs →
match Period_repr.of_seconds secs with
| Pervasives.Ok y ⇒ Valid.t y
| Pervasives.Error _ ⇒ True
end.
unfold Period_repr.of_seconds.
repeat (Utils.tezos_z_autounfold; simpl).
intros.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end; simpl; try constructor; try lia.
Qed.
Lemma of_seconds_exn_is_valid : ∀ {secs : int64},
Valid.t secs →
Valid.t (Period_repr.of_seconds_exn secs).
unfold Period_repr.of_seconds_exn.
repeat (autounfold with tezos_z; simpl).
intros. simpl_tezos_z H.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end; try lia.
Qed.
Lemma mult_eq : ∀ {i : int32} {p : int64},
Valid.t i →
Valid.t p →
Int64.Valid.t (i × p)%Z →
Period_repr.mult i p = return? (i × p)%Z.
intros i p Hi Hp Hip.
unfold Period_repr.mult. simpl.
rewrite Internal.create_eq_32; try assumption.
rewrite Internal.mult__eq; trivial.
autounfold with tezos_z.
now rewrite Int64.normalize_identity.
Qed.
Lemma add_eq_helper : ∀ {p1 p2 : int64},
Valid.t p1 →
Valid.t p2 →
(p1 + p2 <? p1) || (p1 + p2 <? p2) = false.
autounfold with tezos_z. simpl.
intros.
simpl_tezos_z H.
simpl_tezos_z H0.
assert (H_p2 : p1 + p2 <? p1 = false) by lia.
assert (H_p1 : p1 + p2 <? p2 = false) by lia.
rewrite H_p2, H_p1.
reflexivity.
Qed.
Lemma add_eq : ∀ {p1 p2 : int64},
Valid.t p1 →
Valid.t p2 →
Int64.Valid.t (p1 + p2)%Z →
match Period_repr.add p1 p2 with
| Pervasives.Ok y ⇒ y = (p1 + p2)%Z
| Pervasives.Error _ ⇒ False
end.
intros p1 p2 H1 H2 H3.
unfold Period_repr.add.
repeat (autounfold with tezos_z; simpl).
repeat rewrite Int64.normalize_identity.
assert (H : (p1 + p2 <? p1) || (p1 + p2 <? p2) = false).
{ apply add_eq_helper; assumption. }
rewrite H. unfold "return?". constructor.
assumption.
Qed.
Lemma one_second_is_valid : Valid.t Period_repr.one_second.
cbv; intuition; discriminate H.
Qed.
Lemma one_minute_is_valid : Valid.t Period_repr.one_minute.
cbv. intuition; discriminate H.
Qed.
Lemma one_hour_is_valid : Valid.t Period_repr.one_hour.
cbv. intuition; discriminate H.
Qed.
Lemma encoding_is_valid
: Data_encoding.Valid.t Valid.t Period_repr.encoding.
exact Internal.encoding_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Valid.t i →
Period_repr.Internal.create i = Some i.
repeat (autounfold with tezos_z; simpl).
intros.
assert (Hi : i >=? 0 = true) by lia.
now rewrite Hi.
Qed.
Lemma create_eq_32 : ∀ {i : int32},
Valid.t i →
Period_repr.Internal.create (Int64.of_int32 i) = Some i.
unfold Int64.of_int32.
intros.
apply create_eq. assumption.
Qed.
Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Period_repr.Internal.rpc_arg.
unfold Valid.t.
simpl. autounfold with tezos_z.
unfold Period_repr.Internal.rpc_arg.
eapply RPC_arg.Valid.implies.
apply RPC_arg.Valid.uint63. simpl.
autounfold with tezos_z; lia.
Qed.
Lemma create_is_valid : ∀ {x : int64},
Int64.Valid.t x →
match Period_repr.Internal.create x with
| Some y ⇒ Valid.t y
| None ⇒ True
end.
Utils.tezos_z_autounfold. simpl.
intros. unfold Period_repr.Internal.create.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end.
simpl_tezos_z H.
repeat simpl_tezos_z Heqb.
repeat (autounfold with tezos_z; simpl).
{ lia. }
{ constructor. }
Qed.
Lemma mult__is_valid : ∀ {a b : Period_repr.t},
Valid.t a →
Valid.t b →
match Period_repr.Internal.mult_ a b with
| Some c ⇒ Valid.t c
| None ⇒ True
end.
#[local] Hint Unfold
two_pow_63
two_pow_64
max_int : lia_fin.
#[local] Hint Unfold normalize_int64 : tezos_z.
unfold Int64, "/Z"; simpl.
unfold
Period_repr.Internal.mult_,
Period_repr.Internal.op_ltgt,
Period_repr.Internal.zero,
Valid.t, Int64.mul, Int64.div, normalize_int64, mul, div; simpl.
intros a b [Ha1 Ha2] [Hb1 Hb2].
destruct (Z.eqb_spec a 0); simpl; [lia|].
remember ((a × b + two_pow_63) mod two_pow_64 - two_pow_63) as ab64.
remember ((ab64 / a + two_pow_63) mod two_pow_64 - two_pow_63) as aba64.
destruct (Z.eqb_spec aba64 b); simpl; [|auto]; split;
[|subst;autounfold with lia_fin; lia].
assert(b + two_pow_63 ≤ (ab64/a + two_pow_63) mod two_pow_64) by lia.
assert((ab64 / a + two_pow_63) mod two_pow_64 =
ab64 / a + two_pow_63 -
two_pow_64 × ((ab64 / a + two_pow_63) / two_pow_64)).
apply Z.mod_eq; [autounfold with lia_fin; lia].
assert(ab64 / a + two_pow_63 ≥ 0).
{
destruct(Z.leb_spec0 0 ab64).
- assert(ab64 / a ≥ 0) by (apply Z_div_ge0; lia).
unfold two_pow_63; lia.
- assert( -two_pow_63 ≤ ab64).
{
specialize(Int64.normalize_is_valid (a × b)%Z).
subst; autounfold with tezos_z; lia.
}
assert( -two_pow_63 ≤ ab64 / a ).
{
apply Zdiv_le_lower_bound; [lia|].
assert(- two_pow_63 × a ≤ - two_pow_63)
by (apply Z.le_mul_diag_l; [autounfold with lia_fin|]; lia); lia.
}
lia.
}
assert(0%Z ≤ two_pow_64 × ((ab64 / a + two_pow_63) / two_pow_64)).
apply Z.mul_nonneg_nonneg; [autounfold with lia_fin; lia|].
apply Zdiv_le_lower_bound; [autounfold with lia_fin|]; lia.
nia.
Qed.
Lemma mult__eq : ∀ {a b : Period_repr.t},
Valid.t a →
Valid.t b →
Int64.Valid.t (a × b)%Z →
Period_repr.Internal.mult_ a b = Some (a ×i64 b).
Utils.tezos_z_autounfold. simpl. unfold "/Z".
intros.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end.
assert ((((a × b + 9223372036854775808) mod 18446744073709551616 -
9223372036854775808) / a + 9223372036854775808)
mod 18446744073709551616 - 9223372036854775808 = b).
{
assert (Hnon0 : a ≠ 0) by lia.
clear Heqb0.
rewrite Z.mod_eq.
fold two_pow_63.
fold two_pow_64.
replace ((a × b + two_pow_63) mod two_pow_64 - two_pow_63)
with (Pervasives.normalize_int64 (a × b)) by reflexivity.
rewrite Int64.normalize_identity.
rewrite (Z.mul_comm a b).
rewrite (Z.div_mul).
{ Utils.tezos_z_auto. }
{ assumption. }
{ Utils.tezos_z_auto. }
{ lia. }
}
rewrite H2. rewrite Z.eqb_refl. simpl.
{ reflexivity. }
{ f_equal. lia. }
Qed.
Lemma add__is_valid : ∀ {a b : Period_repr.t},
Valid.t a →
Valid.t b →
match Period_repr.Internal.add_ a b with
| Some c ⇒ Valid.t c
| None ⇒ True
end.
unfold Period_repr.Internal.add_.
Utils.tezos_z_autounfold. simpl.
intros.
repeat match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end; try constructor; try lia.
rewrite Bool.orb_false_iff in Heqb0.
destruct Heqb0.
lia.
Qed.
End Internal.
Lemma of_seconds_is_valid : ∀ {secs : int64},
Valid.t secs →
match Period_repr.of_seconds secs with
| Pervasives.Ok y ⇒ Valid.t y
| Pervasives.Error _ ⇒ True
end.
unfold Period_repr.of_seconds.
repeat (Utils.tezos_z_autounfold; simpl).
intros.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end; simpl; try constructor; try lia.
Qed.
Lemma of_seconds_exn_is_valid : ∀ {secs : int64},
Valid.t secs →
Valid.t (Period_repr.of_seconds_exn secs).
unfold Period_repr.of_seconds_exn.
repeat (autounfold with tezos_z; simpl).
intros. simpl_tezos_z H.
match goal with
| [|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
end; try lia.
Qed.
Lemma mult_eq : ∀ {i : int32} {p : int64},
Valid.t i →
Valid.t p →
Int64.Valid.t (i × p)%Z →
Period_repr.mult i p = return? (i × p)%Z.
intros i p Hi Hp Hip.
unfold Period_repr.mult. simpl.
rewrite Internal.create_eq_32; try assumption.
rewrite Internal.mult__eq; trivial.
autounfold with tezos_z.
now rewrite Int64.normalize_identity.
Qed.
Lemma add_eq_helper : ∀ {p1 p2 : int64},
Valid.t p1 →
Valid.t p2 →
(p1 + p2 <? p1) || (p1 + p2 <? p2) = false.
autounfold with tezos_z. simpl.
intros.
simpl_tezos_z H.
simpl_tezos_z H0.
assert (H_p2 : p1 + p2 <? p1 = false) by lia.
assert (H_p1 : p1 + p2 <? p2 = false) by lia.
rewrite H_p2, H_p1.
reflexivity.
Qed.
Lemma add_eq : ∀ {p1 p2 : int64},
Valid.t p1 →
Valid.t p2 →
Int64.Valid.t (p1 + p2)%Z →
match Period_repr.add p1 p2 with
| Pervasives.Ok y ⇒ y = (p1 + p2)%Z
| Pervasives.Error _ ⇒ False
end.
intros p1 p2 H1 H2 H3.
unfold Period_repr.add.
repeat (autounfold with tezos_z; simpl).
repeat rewrite Int64.normalize_identity.
assert (H : (p1 + p2 <? p1) || (p1 + p2 <? p2) = false).
{ apply add_eq_helper; assumption. }
rewrite H. unfold "return?". constructor.
assumption.
Qed.
Lemma one_second_is_valid : Valid.t Period_repr.one_second.
cbv; intuition; discriminate H.
Qed.
Lemma one_minute_is_valid : Valid.t Period_repr.one_minute.
cbv. intuition; discriminate H.
Qed.
Lemma one_hour_is_valid : Valid.t Period_repr.one_hour.
cbv. intuition; discriminate H.
Qed.
Lemma encoding_is_valid
: Data_encoding.Valid.t Valid.t Period_repr.encoding.
exact Internal.encoding_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[compare] function is valid
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Period_repr.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
#[local] Definition is_ok_valid (x : M? int64) :=
match x with
| Pervasives.Ok y ⇒ Valid.t y
| Pervasives.Error _ ⇒ False
end.
#[local] Hint Unfold is_ok_valid : tezos_z.
Lemma add_is_valid : ∀ {a b : int64},
Valid.t a →
Valid.t b →
Valid.t (a + b)%Z →
is_ok_valid (Period_repr.add a b).
Local Hint Unfold Period_repr.add : tezos_z.
repeat (autounfold with tezos_z; simpl).
intros.
rewrite Int64.normalize_identity; try (repeat (autounfold with tezos_z; simpl); lia).
rewrite add_eq_helper; lia.
Qed.
Lemma mult_is_valid : ∀ {a b : int64},
Valid.t a →
Valid.t b →
Int64.Valid.t (a × b)%Z →
is_ok_valid (Period_repr.mult a b).
#[local] Hint Unfold Period_repr.mult Int64.Valid.t normalize_int64 : tezos_z.
autounfold with tezos_z; simpl;
intros;
rewrite Internal.create_eq; try (autounfold with tezos_z; lia);
rewrite Internal.mult__eq; try (autounfold with tezos_z; lia);
simpl; lia.
Qed.
Compare.Valid.t (fun _ ⇒ True) id Period_repr.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
#[local] Definition is_ok_valid (x : M? int64) :=
match x with
| Pervasives.Ok y ⇒ Valid.t y
| Pervasives.Error _ ⇒ False
end.
#[local] Hint Unfold is_ok_valid : tezos_z.
Lemma add_is_valid : ∀ {a b : int64},
Valid.t a →
Valid.t b →
Valid.t (a + b)%Z →
is_ok_valid (Period_repr.add a b).
Local Hint Unfold Period_repr.add : tezos_z.
repeat (autounfold with tezos_z; simpl).
intros.
rewrite Int64.normalize_identity; try (repeat (autounfold with tezos_z; simpl); lia).
rewrite add_eq_helper; lia.
Qed.
Lemma mult_is_valid : ∀ {a b : int64},
Valid.t a →
Valid.t b →
Int64.Valid.t (a × b)%Z →
is_ok_valid (Period_repr.mult a b).
#[local] Hint Unfold Period_repr.mult Int64.Valid.t normalize_int64 : tezos_z.
autounfold with tezos_z; simpl;
intros;
rewrite Internal.create_eq; try (autounfold with tezos_z; lia);
rewrite Internal.mult__eq; try (autounfold with tezos_z; lia);
simpl; lia.
Qed.