🕰️ Period_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.RPC_arg.
Require TezosOfOCaml.Environment.V7.Proofs.Int64.
Require TezosOfOCaml.Environment.V7.Proofs.Int32.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.RPC_arg.
Require TezosOfOCaml.Environment.V7.Proofs.Int64.
Require TezosOfOCaml.Environment.V7.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.
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.
In some definitions we need the period to be non-zero.
Definition non_zero (period : Period_repr.t) : Prop :=
1 ≤ period ≤ Int64.max_int.
#[global] Hint Unfold t non_zero : tezos_z.
1 ≤ period ≤ Int64.max_int.
#[global] Hint Unfold t non_zero : tezos_z.
[non_zero] is a particular case of [Valid.t].
Lemma non_zero_implies_t (period : Period_repr.t) :
non_zero period → t period.
Proof.
lia.
Qed.
End Valid.
Module Internal.
#[global] Hint Unfold
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.
non_zero period → t period.
Proof.
lia.
Qed.
End Valid.
Module Internal.
#[global] Hint Unfold
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.
Proof.
intros.
unfold Period_repr.Internal.mult_, Period_repr.Internal.op_ltgt; simpl.
destruct negb eqn:?; [|lia].
destruct negb eqn:? in |- *; [trivial|].
assert ((a ×i64 b) /i64 a = (a ×i64 b) ÷ a)
by (apply Int64.normalize_identity; nia).
assert (a ×i64 b = a ×Z b) by lia.
lia.
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).
Proof.
intros.
unfold Period_repr.Internal.mult_, Period_repr.Internal.op_ltgt; simpl.
destruct negb eqn:?.
{ replace ((a ×i64 b) /i64 a) with ((a ×i64 b) ÷ a)
by (rewrite <- Int64.normalize_identity; nia).
replace (a ×i64 b) with (a ×Z b) by lia.
destruct negb eqn:H_neq in |- *; [|trivial].
nia.
}
{ now replace a with 0 by 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.
#[global] Hint Unfold
Period_repr.create
Period_repr.mult_
Period_repr.add_
Period_repr.op_ltgt
Period_repr.op_eq
Period_repr.op_lt
Period_repr.op_gt
Period_repr.op_lteq
Period_repr.op_gteq
Period_repr.zero
Period_repr.one
: tezos_z.
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.
Proof.
intros.
unfold Period_repr.Internal.mult_, Period_repr.Internal.op_ltgt; simpl.
destruct negb eqn:?; [|lia].
destruct negb eqn:? in |- *; [trivial|].
assert ((a ×i64 b) /i64 a = (a ×i64 b) ÷ a)
by (apply Int64.normalize_identity; nia).
assert (a ×i64 b = a ×Z b) by lia.
lia.
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).
Proof.
intros.
unfold Period_repr.Internal.mult_, Period_repr.Internal.op_ltgt; simpl.
destruct negb eqn:?.
{ replace ((a ×i64 b) /i64 a) with ((a ×i64 b) ÷ a)
by (rewrite <- Int64.normalize_identity; nia).
replace (a ×i64 b) with (a ×Z b) by lia.
destruct negb eqn:H_neq in |- *; [|trivial].
nia.
}
{ now replace a with 0 by 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.
#[global] Hint Unfold
Period_repr.create
Period_repr.mult_
Period_repr.add_
Period_repr.op_ltgt
Period_repr.op_eq
Period_repr.op_lt
Period_repr.op_gt
Period_repr.op_lteq
Period_repr.op_gteq
Period_repr.zero
Period_repr.one
: tezos_z.
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.