Skip to main content

# 🕰️ Period_repr.v

Proofs

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.

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.

[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.

[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.

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 yValid.t y
| NoneTrue
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 cValid.t c
| NoneTrue
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 cValid.t c
| NoneTrue
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 yValid.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 yy = (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 yValid.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.