🧮 Saturation_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Option.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
#[global] Hint Unfold
Saturation_repr.t
Saturation_repr.to_int
Saturation_repr.op_lt
Saturation_repr.op_lteq
Saturation_repr.op_gt
Saturation_repr.op_gteq
Saturation_repr.op_eq
Saturation_repr.equal
Saturation_repr.op_ltgt
Saturation_repr.compare
Saturation_repr.saturated
Saturation_repr.to_z
Saturation_repr.zero
Saturation_repr.one
Saturation_repr.shift_right
Saturation_repr.mul_fast
Saturation_repr.erem
Saturation_repr.ediv
: tezos_z.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Option.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
#[global] Hint Unfold
Saturation_repr.t
Saturation_repr.to_int
Saturation_repr.op_lt
Saturation_repr.op_lteq
Saturation_repr.op_gt
Saturation_repr.op_gteq
Saturation_repr.op_eq
Saturation_repr.equal
Saturation_repr.op_ltgt
Saturation_repr.compare
Saturation_repr.saturated
Saturation_repr.to_z
Saturation_repr.zero
Saturation_repr.one
Saturation_repr.shift_right
Saturation_repr.mul_fast
Saturation_repr.erem
Saturation_repr.ediv
: tezos_z.
[compare] function is valid
Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id Saturation_repr.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
We put the saturation operations which can be trivially converted to their
Z equivalent into the [tezos_z] hint database.
Module Valid.
Definition t (x : Saturation_repr.t) : Prop :=
0 ≤ x ≤ Saturation_repr.saturated.
#[global] Hint Unfold t : tezos_z.
Lemma decide {x} :
(0 <=? x) && (x <=? Saturation_repr.saturated) = true →
t x.
Proof.
rewrite Bool.andb_true_iff; lia.
Qed.
Lemma implies_int_valid x : t x → Pervasives.Int.Valid.t x.
Proof.
lia.
Qed.
End Valid.
Module Strictly_valid.
Definition t (x : Saturation_repr.t) : Prop :=
0 ≤ x < Saturation_repr.saturated.
#[global] Hint Unfold t : tezos_z.
Lemma implies_valid (x : Saturation_repr.t) : t x → Valid.t x.
lia.
Qed.
Lemma true_eq: ∀ {z : int},
Saturation_repr.Strictly_valid.t z →
Saturation_repr.op_gteq z 0 &&
Saturation_repr.op_lt z Saturation_repr.saturated = true.
intros; rewrite Bool.andb_true_iff; lia.
Qed.
End Strictly_valid.
Module Small_enough.
Definition t (x : Saturation_repr.t) : Prop :=
0 ≤ x ≤ 2147483647.
#[global] Hint Unfold t : tezos_z.
Lemma implies_valid (x : Saturation_repr.t) : t x → Valid.t x.
lia.
Qed.
End Small_enough.
Module Aux_lemmas.
Definition t (x : Saturation_repr.t) : Prop :=
0 ≤ x ≤ Saturation_repr.saturated.
#[global] Hint Unfold t : tezos_z.
Lemma decide {x} :
(0 <=? x) && (x <=? Saturation_repr.saturated) = true →
t x.
Proof.
rewrite Bool.andb_true_iff; lia.
Qed.
Lemma implies_int_valid x : t x → Pervasives.Int.Valid.t x.
Proof.
lia.
Qed.
End Valid.
Module Strictly_valid.
Definition t (x : Saturation_repr.t) : Prop :=
0 ≤ x < Saturation_repr.saturated.
#[global] Hint Unfold t : tezos_z.
Lemma implies_valid (x : Saturation_repr.t) : t x → Valid.t x.
lia.
Qed.
Lemma true_eq: ∀ {z : int},
Saturation_repr.Strictly_valid.t z →
Saturation_repr.op_gteq z 0 &&
Saturation_repr.op_lt z Saturation_repr.saturated = true.
intros; rewrite Bool.andb_true_iff; lia.
Qed.
End Strictly_valid.
Module Small_enough.
Definition t (x : Saturation_repr.t) : Prop :=
0 ≤ x ≤ 2147483647.
#[global] Hint Unfold t : tezos_z.
Lemma implies_valid (x : Saturation_repr.t) : t x → Valid.t x.
lia.
Qed.
End Small_enough.
Module Aux_lemmas.
111...1
Fixpoint positive_ones(n : nat) : positive :=
match n with
| Datatypes.O ⇒ xH
| Datatypes.S m ⇒ xI (positive_ones m)
end.
Lemma land_positive_ones : ∀ n p, (p ≤ positive_ones n)%positive
→ Pos.land p (positive_ones n) = N.pos p.
Proof.
induction n; intros p Hp; simpl in ×.
{ destruct p; lia. }
{ destruct p; simpl; try rewrite IHn; lia. }
Qed.
Lemma testbit_positive_ones_true : ∀ n i,
(i ≤ n)%nat → Pos.testbit_nat (positive_ones n) i = true.
induction n; intros; simpl; destruct i; try lia.
apply IHn; lia.
Qed.
Lemma testbit_positive_ones_false : ∀ n i,
(n < i)%nat → Pos.testbit_nat (positive_ones n) i = false.
induction n; intros.
{ destruct i; lia. }
{ simpl; destruct i; try lia.
apply IHn; lia.
}
Qed.
Lemma testbit_nat_bound_false : ∀ n i x,
(n < i)%nat → (x ≤ positive_ones n)%positive
→ Pos.testbit_nat x i = false.
induction n; intros.
{ simpl in ×.
assert ( x = 1%positive) by lia.
rewrite H1.
destruct i; lia.
}
{ destruct i as [|j]; try lia.
destruct x; simpl; auto;
simpl in H0;
apply IHn; lia.
}
Qed.
Lemma testbit_pos_true : ∀ p : positive,
∃ i : nat, Pos.testbit_nat p i = true.
induction p.
{ ∃ 0%nat; reflexivity. }
{ destruct IHp as [j Hj].
∃ (Datatypes.S j); exact Hj.
}
{ ∃ 0%nat; reflexivity. }
Qed.
Lemma testbit_nat_zero : ∀ x : N,
(∀ n, N.testbit_nat x n = false) → x = 0%N.
intros.
destruct x; auto.
simpl in H.
destruct (testbit_pos_true p) as [i Hi].
rewrite (H i) in Hi; discriminate.
Qed.
Lemma testbit_true_implies_positive : ∀ x,
(∃ i, N.testbit_nat x i = true) →
∃ q, x = Npos q.
intros x [i Hi].
destruct x; try discriminate.
∃ p; auto.
Qed.
match n with
| Datatypes.O ⇒ xH
| Datatypes.S m ⇒ xI (positive_ones m)
end.
Lemma land_positive_ones : ∀ n p, (p ≤ positive_ones n)%positive
→ Pos.land p (positive_ones n) = N.pos p.
Proof.
induction n; intros p Hp; simpl in ×.
{ destruct p; lia. }
{ destruct p; simpl; try rewrite IHn; lia. }
Qed.
Lemma testbit_positive_ones_true : ∀ n i,
(i ≤ n)%nat → Pos.testbit_nat (positive_ones n) i = true.
induction n; intros; simpl; destruct i; try lia.
apply IHn; lia.
Qed.
Lemma testbit_positive_ones_false : ∀ n i,
(n < i)%nat → Pos.testbit_nat (positive_ones n) i = false.
induction n; intros.
{ destruct i; lia. }
{ simpl; destruct i; try lia.
apply IHn; lia.
}
Qed.
Lemma testbit_nat_bound_false : ∀ n i x,
(n < i)%nat → (x ≤ positive_ones n)%positive
→ Pos.testbit_nat x i = false.
induction n; intros.
{ simpl in ×.
assert ( x = 1%positive) by lia.
rewrite H1.
destruct i; lia.
}
{ destruct i as [|j]; try lia.
destruct x; simpl; auto;
simpl in H0;
apply IHn; lia.
}
Qed.
Lemma testbit_pos_true : ∀ p : positive,
∃ i : nat, Pos.testbit_nat p i = true.
induction p.
{ ∃ 0%nat; reflexivity. }
{ destruct IHp as [j Hj].
∃ (Datatypes.S j); exact Hj.
}
{ ∃ 0%nat; reflexivity. }
Qed.
Lemma testbit_nat_zero : ∀ x : N,
(∀ n, N.testbit_nat x n = false) → x = 0%N.
intros.
destruct x; auto.
simpl in H.
destruct (testbit_pos_true p) as [i Hi].
rewrite (H i) in Hi; discriminate.
Qed.
Lemma testbit_true_implies_positive : ∀ x,
(∃ i, N.testbit_nat x i = true) →
∃ q, x = Npos q.
intros x [i Hi].
destruct x; try discriminate.
∃ p; auto.
Qed.
Index of max bit set to 1
Fixpoint max_one(p : positive) : nat :=
match p with
| xI q ⇒ Datatypes.S (max_one q)
| xO q ⇒ Datatypes.S (max_one q)
| xH ⇒ 0
end.
Lemma max_one_testbit_true : ∀ p,
Pos.testbit_nat p (max_one p) = true.
induction p.
{ simpl; apply IHp. }
{ simpl; apply IHp. }
{ reflexivity. }
Qed.
Lemma positive_ones_max_one_gt : ∀ p n,
(positive_ones n < p)%positive →
(n < max_one p)%nat.
induction p; intros.
{ simpl.
destruct n; try lia.
simpl in H.
assert (positive_ones n < p)%positive as G by lia.
pose (IHp _ G); lia.
}
{ destruct n; simpl; try lia.
simpl in H.
assert (positive_ones n < p)%positive as G by lia.
pose (IHp _ G); lia.
}
{ destruct n; lia. }
Qed.
Lemma small_enough_generic :
∀ n x, 0 ≤ x →
(land x (Zneg (BinPosDef.Pos.succ (positive_ones n))) =i 0)
= (x ≤i Zpos (positive_ones n)).
intros n x Hx.
rewrite Z.land_comm.
unfold Z.land.
destruct x; try lia; auto.
destruct (Z.le_gt_cases (Z.pos p) (Z.pos (positive_ones n))) as [Hle|Hge].
{ simpl. rewrite Pos.pred_N_succ.
unfold "=i", "<=i"; simpl.
rewrite (Zle_imp_le_bool _ _ Hle).
rewrite Z.eqb_eq.
unfold "<=" in Hle.
unfold "?=" in Hle.
rewrite Pos.compare_gt_iff in Hle.
rewrite <- Pos.le_nlt in Hle.
cut (Pos.ldiff p (positive_ones n) = 0)%N.
{ intro Hz; rewrite Hz; reflexivity. }
{ apply testbit_nat_zero; intro i.
rewrite Ndigits.Pdiff_semantics.
destruct (Nat.le_gt_cases i n) as [Hi|Hi].
{ rewrite testbit_positive_ones_true; auto.
apply Bool.andb_false_r.
}
{ rewrite (testbit_nat_bound_false n); auto. }
}
}
{ unfold "<" in Hge; unfold "?=" in Hge.
rewrite Pos.compare_lt_iff in Hge.
cut (∃ q, Pos.ldiff p (positive_ones n) = Npos q).
{ intros [q Hq].
rewrite Pos.pred_N_succ; simpl.
rewrite Hq; simpl.
symmetry; rewrite Z.leb_gt; auto.
}
{ apply testbit_true_implies_positive.
∃ (max_one p).
rewrite Ndigits.Pdiff_semantics.
rewrite max_one_testbit_true.
rewrite testbit_positive_ones_false; auto.
apply positive_ones_max_one_gt; auto.
}
}
Qed.
Lemma pos_land_le_r : ∀ x y,
(Pos.land x y ≤ Npos y)%N.
induction x; intros; (
simpl;
destruct y; try lia;
unfold Pos.Nsucc_double,
Pos.Ndouble;
destruct (Pos.land x y) eqn:G;
pose (IHx y) as Hy; rewrite G in Hy; lia).
Qed.
Lemma Zpos_le_to_pos_le :
∀ p q : positive,
Z.pos p ≤ Z.pos q → (p ≤ q)%positive.
intros; lia.
Qed.
Lemma Npos_le_to_pos_le :
∀ p q : positive,
(N.pos p ≤ N.pos q)%N → (p ≤ q)%positive.
intros; lia.
Qed.
Lemma pos_le_to_Npos_le :
∀ p q : positive,
(p ≤ q)%positive → (N.pos p ≤ N.pos q)%N.
intros; lia.
Qed.
End Aux_lemmas.
Module Unfold.
Import Saturation_repr.
Global Hint Unfold
Valid.t
Strictly_valid.t
Small_enough.t
add
compare
equal
erem
may_saturate_value
mul
mul_fast
mul_safe_value
of_int_opt
one
op_eq
op_gt
op_gteq
op_lt
op_lteq
op_ltgt
saturated
sub
to_int
to_z
zero
: tezos_z.
End Unfold.
Definition saturate (x : Z.t) : Z.t :=
Z.max (Z.min x Saturation_repr.saturated) 0.
#[global] Hint Unfold saturate : tezos_z.
Lemma saturate_eq : ∀ (a : BinInt.Z),
Saturation_repr.Valid.t a →
Saturation_repr.saturate a = a.
intros a Ha.
autounfold with tezos_z in ×.
unfold Saturation_repr.saturate.
rewrite Utils.BinInt_Z_min_eq; [|autounfold with tezos_z; lia].
rewrite Utils.BinInt_Z_max_eq; [|lia].
reflexivity.
Qed.
Lemma max_is_valid (x y : Saturation_repr.t)
: Valid.t x → Valid.t y → Valid.t (Saturation_repr.max x y).
intros.
unfold Saturation_repr.max.
now destruct (Saturation_repr.op_gteq _ _).
Qed.
Lemma max_eq x y : Saturation_repr.max x y = Z.max x y.
unfold Saturation_repr.max.
autounfold with tezos_z; cbn; autounfold with tezos_z.
match goal with
| [|- context[if ?e then _ else _]] ⇒ destruct e eqn:H
end; lia.
Qed.
Lemma min_is_valid (x y : Saturation_repr.t)
: Valid.t x → Valid.t y → Valid.t (Saturation_repr.min x y).
intros.
unfold Saturation_repr.min.
now destruct (Saturation_repr.op_gteq _ _).
Qed.
Lemma min_eq x y : Saturation_repr.min x y = Z.min x y.
unfold Saturation_repr.min.
autounfold with tezos_z; cbn; autounfold with tezos_z.
match goal with
| [|- context[if ?e then _ else _]] ⇒ destruct e eqn:H
end; lia.
Qed.
Lemma saturated_is_valid : Valid.t Saturation_repr.saturated.
now apply Valid.decide.
Qed.
Lemma of_int_opt_is_strictly_valid (i : int) :
match Saturation_repr.of_int_opt i with
| Some i ⇒ Strictly_valid.t i
| None ⇒ True
end.
unfold Saturation_repr.of_int_opt, "&&".
autounfold with tezos_z.
destruct (_ && _)%bool eqn:H_eq; simpl; trivial.
cbn in *; autounfold with tezos_z in ×.
lia.
Qed.
Lemma of_int_opt_eq (i : int) :
Strictly_valid.t i →
Saturation_repr.of_int_opt i = Some i.
autounfold with tezos_z; simpl.
destruct (op_andand _ _) eqn:?; try reflexivity.
rewrite Bool.andb_false_iff in ×.
lia.
Qed.
Lemma of_z_opt_is_strictly_valid (z : Z.t) :
match Saturation_repr.of_z_opt z with
| Some z ⇒ Strictly_valid.t z
| None ⇒ True
end.
apply of_int_opt_is_strictly_valid.
Qed.
Lemma of_z_opt_eq (z : Z.t) :
Saturation_repr.Strictly_valid.t z →
Saturation_repr.of_z_opt z = Some z.
Proof.
intro H.
unfold Saturation_repr.of_z_opt.
rewrite Z.to_int_eq by lia.
rewrite of_int_opt_eq; lia.
Qed.
Lemma safe_int_is_valid x : Valid.t (Saturation_repr.safe_int x).
unfold Saturation_repr.safe_int, Saturation_repr.saturate_if_undef.
assert (H := of_int_opt_is_strictly_valid x).
destruct (Saturation_repr.of_int_opt _).
{ now apply Strictly_valid.implies_valid. }
{ exact saturated_is_valid. }
Qed.
Lemma safe_int_eq : ∀ (i : int),
Strictly_valid.t i →
Saturation_repr.safe_int i = i.
Proof.
intros.
unfold Saturation_repr.safe_int.
now rewrite of_int_opt_eq.
Qed.
Lemma small_enough_eq :
∀ x, 0 ≤ x → Saturation_repr.small_enough x = (x ≤i 2147483647).
intros.
unfold Saturation_repr.small_enough.
unfold Saturation_repr.op_eq.
apply (Aux_lemmas.small_enough_generic 30); auto.
Qed.
Lemma mul_safe_exn_eq :
∀ (x : Saturation_repr.t), Small_enough.t x → Saturation_repr.mul_safe_exn x = x.
unfold Small_enough.t,
Saturation_repr.mul_safe_exn.
intros x [Hx1 Hx2].
rewrite small_enough_eq; auto; simpl.
destruct (_ ≤i _) eqn:?; lia.
Qed.
#[global] Hint Rewrite mul_safe_exn_eq : tezos_z.
Lemma mul_safe_exn_is_small_enough : ∀ x : Saturation_repr.t,
Small_enough.t x →
Small_enough.t (Saturation_repr.mul_safe_exn x).
intros.
rewrite mul_safe_exn_eq; auto.
Qed.
Lemma mul_safe_exn_is_valid : ∀ x : Saturation_repr.t,
Small_enough.t x → Valid.t (Saturation_repr.mul_safe_exn x).
intros.
apply Small_enough.implies_valid.
apply mul_safe_exn_is_small_enough; auto.
Qed.
Lemma mul_safe_of_int_exn_eq :
∀ (x : Saturation_repr.t), Small_enough.t x → Saturation_repr.mul_safe_of_int_exn x = x.
unfold Strictly_valid.t,
Saturation_repr.mul_safe_of_int_exn,
Saturation_repr.of_int_opt,
Saturation_repr.mul_safe_value,
Saturation_repr.op_gteq,
Saturation_repr.op_lt,
Saturation_repr.saturated,
Pervasives.max_int.
intros x [Hx_nonneg Hx_small].
rewrite Z.geb_leb.
rewrite (Zle_imp_le_bool _ _ Hx_nonneg); simpl.
assert (x < 4611686018427387903) as Hx_sat by lia.
rewrite <- Z.ltb_lt in Hx_sat.
unfold "<i"; simpl.
rewrite Hx_sat; simpl.
rewrite small_enough_eq; auto; simpl.
rewrite <- Z.leb_le in Hx_small.
unfold "<=i"; simpl.
now rewrite Hx_small.
Qed.
#[global] Hint Rewrite mul_safe_of_int_exn_eq : tezos_z.
Lemma mul_safe_of_int_exn_is_small_enough : ∀ x : Saturation_repr.t,
Small_enough.t x → Small_enough.t (Saturation_repr.mul_safe_of_int_exn x).
intros.
rewrite mul_safe_of_int_exn_eq; auto.
Qed.
Lemma mul_safe_of_int_exn_is_valid : ∀ x : Saturation_repr.t,
Small_enough.t x → Valid.t (Saturation_repr.mul_safe_of_int_exn x).
intros.
apply Small_enough.implies_valid.
apply mul_safe_of_int_exn_is_small_enough; auto.
Qed.
Lemma t_to_z_exn_to_z x :
Saturation_repr.Strictly_valid.t x →
Saturation_repr.t_to_z_exn (Saturation_repr.to_z x) = x.
intro.
unfold Saturation_repr.to_z, of_int.
unfold Saturation_repr.t_to_z_exn.
now rewrite of_z_opt_eq.
Qed.
Lemma add_is_valid : ∀ (x y : Saturation_repr.t),
Saturation_repr.Valid.t (Saturation_repr.add x y).
Proof.
intros.
unfold Saturation_repr.add.
step; lia.
Qed.
Lemma add_eq (x y : Saturation_repr.t) :
Valid.t x →
Valid.t y →
Saturation_repr.add x y = saturate (x + y)%Z.
intros.
unfold Saturation_repr.add, saturate; simpl.
destruct (_ ≥i _) eqn:Hle.
{ lia. }
{ rewrite Z.min_r; lia. }
Qed.
Lemma sub_valid : ∀ (x y : int),
Saturation_repr.Valid.t (Saturation_repr.sub x y).
lia.
Qed.
Lemma sub_eq : ∀ (x y : int),
Saturation_repr.Valid.t x →
Saturation_repr.Valid.t y →
Saturation_repr.sub x y = saturate (x - y).
intros.
unfold Saturation_repr.sub, saturate; simpl.
rewrite Z.min_l; [|lia].
unfold "-i", normalize_int.
rewrite Z.mod_small; lia.
Qed.
match p with
| xI q ⇒ Datatypes.S (max_one q)
| xO q ⇒ Datatypes.S (max_one q)
| xH ⇒ 0
end.
Lemma max_one_testbit_true : ∀ p,
Pos.testbit_nat p (max_one p) = true.
induction p.
{ simpl; apply IHp. }
{ simpl; apply IHp. }
{ reflexivity. }
Qed.
Lemma positive_ones_max_one_gt : ∀ p n,
(positive_ones n < p)%positive →
(n < max_one p)%nat.
induction p; intros.
{ simpl.
destruct n; try lia.
simpl in H.
assert (positive_ones n < p)%positive as G by lia.
pose (IHp _ G); lia.
}
{ destruct n; simpl; try lia.
simpl in H.
assert (positive_ones n < p)%positive as G by lia.
pose (IHp _ G); lia.
}
{ destruct n; lia. }
Qed.
Lemma small_enough_generic :
∀ n x, 0 ≤ x →
(land x (Zneg (BinPosDef.Pos.succ (positive_ones n))) =i 0)
= (x ≤i Zpos (positive_ones n)).
intros n x Hx.
rewrite Z.land_comm.
unfold Z.land.
destruct x; try lia; auto.
destruct (Z.le_gt_cases (Z.pos p) (Z.pos (positive_ones n))) as [Hle|Hge].
{ simpl. rewrite Pos.pred_N_succ.
unfold "=i", "<=i"; simpl.
rewrite (Zle_imp_le_bool _ _ Hle).
rewrite Z.eqb_eq.
unfold "<=" in Hle.
unfold "?=" in Hle.
rewrite Pos.compare_gt_iff in Hle.
rewrite <- Pos.le_nlt in Hle.
cut (Pos.ldiff p (positive_ones n) = 0)%N.
{ intro Hz; rewrite Hz; reflexivity. }
{ apply testbit_nat_zero; intro i.
rewrite Ndigits.Pdiff_semantics.
destruct (Nat.le_gt_cases i n) as [Hi|Hi].
{ rewrite testbit_positive_ones_true; auto.
apply Bool.andb_false_r.
}
{ rewrite (testbit_nat_bound_false n); auto. }
}
}
{ unfold "<" in Hge; unfold "?=" in Hge.
rewrite Pos.compare_lt_iff in Hge.
cut (∃ q, Pos.ldiff p (positive_ones n) = Npos q).
{ intros [q Hq].
rewrite Pos.pred_N_succ; simpl.
rewrite Hq; simpl.
symmetry; rewrite Z.leb_gt; auto.
}
{ apply testbit_true_implies_positive.
∃ (max_one p).
rewrite Ndigits.Pdiff_semantics.
rewrite max_one_testbit_true.
rewrite testbit_positive_ones_false; auto.
apply positive_ones_max_one_gt; auto.
}
}
Qed.
Lemma pos_land_le_r : ∀ x y,
(Pos.land x y ≤ Npos y)%N.
induction x; intros; (
simpl;
destruct y; try lia;
unfold Pos.Nsucc_double,
Pos.Ndouble;
destruct (Pos.land x y) eqn:G;
pose (IHx y) as Hy; rewrite G in Hy; lia).
Qed.
Lemma Zpos_le_to_pos_le :
∀ p q : positive,
Z.pos p ≤ Z.pos q → (p ≤ q)%positive.
intros; lia.
Qed.
Lemma Npos_le_to_pos_le :
∀ p q : positive,
(N.pos p ≤ N.pos q)%N → (p ≤ q)%positive.
intros; lia.
Qed.
Lemma pos_le_to_Npos_le :
∀ p q : positive,
(p ≤ q)%positive → (N.pos p ≤ N.pos q)%N.
intros; lia.
Qed.
End Aux_lemmas.
Module Unfold.
Import Saturation_repr.
Global Hint Unfold
Valid.t
Strictly_valid.t
Small_enough.t
add
compare
equal
erem
may_saturate_value
mul
mul_fast
mul_safe_value
of_int_opt
one
op_eq
op_gt
op_gteq
op_lt
op_lteq
op_ltgt
saturated
sub
to_int
to_z
zero
: tezos_z.
End Unfold.
Definition saturate (x : Z.t) : Z.t :=
Z.max (Z.min x Saturation_repr.saturated) 0.
#[global] Hint Unfold saturate : tezos_z.
Lemma saturate_eq : ∀ (a : BinInt.Z),
Saturation_repr.Valid.t a →
Saturation_repr.saturate a = a.
intros a Ha.
autounfold with tezos_z in ×.
unfold Saturation_repr.saturate.
rewrite Utils.BinInt_Z_min_eq; [|autounfold with tezos_z; lia].
rewrite Utils.BinInt_Z_max_eq; [|lia].
reflexivity.
Qed.
Lemma max_is_valid (x y : Saturation_repr.t)
: Valid.t x → Valid.t y → Valid.t (Saturation_repr.max x y).
intros.
unfold Saturation_repr.max.
now destruct (Saturation_repr.op_gteq _ _).
Qed.
Lemma max_eq x y : Saturation_repr.max x y = Z.max x y.
unfold Saturation_repr.max.
autounfold with tezos_z; cbn; autounfold with tezos_z.
match goal with
| [|- context[if ?e then _ else _]] ⇒ destruct e eqn:H
end; lia.
Qed.
Lemma min_is_valid (x y : Saturation_repr.t)
: Valid.t x → Valid.t y → Valid.t (Saturation_repr.min x y).
intros.
unfold Saturation_repr.min.
now destruct (Saturation_repr.op_gteq _ _).
Qed.
Lemma min_eq x y : Saturation_repr.min x y = Z.min x y.
unfold Saturation_repr.min.
autounfold with tezos_z; cbn; autounfold with tezos_z.
match goal with
| [|- context[if ?e then _ else _]] ⇒ destruct e eqn:H
end; lia.
Qed.
Lemma saturated_is_valid : Valid.t Saturation_repr.saturated.
now apply Valid.decide.
Qed.
Lemma of_int_opt_is_strictly_valid (i : int) :
match Saturation_repr.of_int_opt i with
| Some i ⇒ Strictly_valid.t i
| None ⇒ True
end.
unfold Saturation_repr.of_int_opt, "&&".
autounfold with tezos_z.
destruct (_ && _)%bool eqn:H_eq; simpl; trivial.
cbn in *; autounfold with tezos_z in ×.
lia.
Qed.
Lemma of_int_opt_eq (i : int) :
Strictly_valid.t i →
Saturation_repr.of_int_opt i = Some i.
autounfold with tezos_z; simpl.
destruct (op_andand _ _) eqn:?; try reflexivity.
rewrite Bool.andb_false_iff in ×.
lia.
Qed.
Lemma of_z_opt_is_strictly_valid (z : Z.t) :
match Saturation_repr.of_z_opt z with
| Some z ⇒ Strictly_valid.t z
| None ⇒ True
end.
apply of_int_opt_is_strictly_valid.
Qed.
Lemma of_z_opt_eq (z : Z.t) :
Saturation_repr.Strictly_valid.t z →
Saturation_repr.of_z_opt z = Some z.
Proof.
intro H.
unfold Saturation_repr.of_z_opt.
rewrite Z.to_int_eq by lia.
rewrite of_int_opt_eq; lia.
Qed.
Lemma safe_int_is_valid x : Valid.t (Saturation_repr.safe_int x).
unfold Saturation_repr.safe_int, Saturation_repr.saturate_if_undef.
assert (H := of_int_opt_is_strictly_valid x).
destruct (Saturation_repr.of_int_opt _).
{ now apply Strictly_valid.implies_valid. }
{ exact saturated_is_valid. }
Qed.
Lemma safe_int_eq : ∀ (i : int),
Strictly_valid.t i →
Saturation_repr.safe_int i = i.
Proof.
intros.
unfold Saturation_repr.safe_int.
now rewrite of_int_opt_eq.
Qed.
Lemma small_enough_eq :
∀ x, 0 ≤ x → Saturation_repr.small_enough x = (x ≤i 2147483647).
intros.
unfold Saturation_repr.small_enough.
unfold Saturation_repr.op_eq.
apply (Aux_lemmas.small_enough_generic 30); auto.
Qed.
Lemma mul_safe_exn_eq :
∀ (x : Saturation_repr.t), Small_enough.t x → Saturation_repr.mul_safe_exn x = x.
unfold Small_enough.t,
Saturation_repr.mul_safe_exn.
intros x [Hx1 Hx2].
rewrite small_enough_eq; auto; simpl.
destruct (_ ≤i _) eqn:?; lia.
Qed.
#[global] Hint Rewrite mul_safe_exn_eq : tezos_z.
Lemma mul_safe_exn_is_small_enough : ∀ x : Saturation_repr.t,
Small_enough.t x →
Small_enough.t (Saturation_repr.mul_safe_exn x).
intros.
rewrite mul_safe_exn_eq; auto.
Qed.
Lemma mul_safe_exn_is_valid : ∀ x : Saturation_repr.t,
Small_enough.t x → Valid.t (Saturation_repr.mul_safe_exn x).
intros.
apply Small_enough.implies_valid.
apply mul_safe_exn_is_small_enough; auto.
Qed.
Lemma mul_safe_of_int_exn_eq :
∀ (x : Saturation_repr.t), Small_enough.t x → Saturation_repr.mul_safe_of_int_exn x = x.
unfold Strictly_valid.t,
Saturation_repr.mul_safe_of_int_exn,
Saturation_repr.of_int_opt,
Saturation_repr.mul_safe_value,
Saturation_repr.op_gteq,
Saturation_repr.op_lt,
Saturation_repr.saturated,
Pervasives.max_int.
intros x [Hx_nonneg Hx_small].
rewrite Z.geb_leb.
rewrite (Zle_imp_le_bool _ _ Hx_nonneg); simpl.
assert (x < 4611686018427387903) as Hx_sat by lia.
rewrite <- Z.ltb_lt in Hx_sat.
unfold "<i"; simpl.
rewrite Hx_sat; simpl.
rewrite small_enough_eq; auto; simpl.
rewrite <- Z.leb_le in Hx_small.
unfold "<=i"; simpl.
now rewrite Hx_small.
Qed.
#[global] Hint Rewrite mul_safe_of_int_exn_eq : tezos_z.
Lemma mul_safe_of_int_exn_is_small_enough : ∀ x : Saturation_repr.t,
Small_enough.t x → Small_enough.t (Saturation_repr.mul_safe_of_int_exn x).
intros.
rewrite mul_safe_of_int_exn_eq; auto.
Qed.
Lemma mul_safe_of_int_exn_is_valid : ∀ x : Saturation_repr.t,
Small_enough.t x → Valid.t (Saturation_repr.mul_safe_of_int_exn x).
intros.
apply Small_enough.implies_valid.
apply mul_safe_of_int_exn_is_small_enough; auto.
Qed.
Lemma t_to_z_exn_to_z x :
Saturation_repr.Strictly_valid.t x →
Saturation_repr.t_to_z_exn (Saturation_repr.to_z x) = x.
intro.
unfold Saturation_repr.to_z, of_int.
unfold Saturation_repr.t_to_z_exn.
now rewrite of_z_opt_eq.
Qed.
Lemma add_is_valid : ∀ (x y : Saturation_repr.t),
Saturation_repr.Valid.t (Saturation_repr.add x y).
Proof.
intros.
unfold Saturation_repr.add.
step; lia.
Qed.
Lemma add_eq (x y : Saturation_repr.t) :
Valid.t x →
Valid.t y →
Saturation_repr.add x y = saturate (x + y)%Z.
intros.
unfold Saturation_repr.add, saturate; simpl.
destruct (_ ≥i _) eqn:Hle.
{ lia. }
{ rewrite Z.min_r; lia. }
Qed.
Lemma sub_valid : ∀ (x y : int),
Saturation_repr.Valid.t (Saturation_repr.sub x y).
lia.
Qed.
Lemma sub_eq : ∀ (x y : int),
Saturation_repr.Valid.t x →
Saturation_repr.Valid.t y →
Saturation_repr.sub x y = saturate (x - y).
intros.
unfold Saturation_repr.sub, saturate; simpl.
rewrite Z.min_l; [|lia].
unfold "-i", normalize_int.
rewrite Z.mod_small; lia.
Qed.
A simple check that small_enough bounds do not saturate
Fact mul_small_enough_bounds_do_not_saturate:
0 × 0 ≤ Saturation_repr.saturated ∧ 2147483647 × 2147483647 ≤ Saturation_repr.saturated.
lia.
Qed.
Lemma saturation_repr_valid_eq : ∀ (x: int),
Saturation_repr.Valid.t x ↔
(((0 <=? x) && (x <=? 4611686018427387903))%bool = true).
lia.
Qed.
#[global] Hint Rewrite saturation_repr_valid_eq : tezos_z.
Lemma mul_is_valid : ∀ (x y : int),
Saturation_repr.Valid.t x →
Saturation_repr.Valid.t y →
Saturation_repr.Valid.t (Saturation_repr.mul x y).
Proof.
Utils.tezos_z_autounfold; simpl.
intros x y Hx Hy.
repeat rewrite small_enough_eq; try lia; simpl.
(* Even if [x] appears first, we destruct it last to avoid generating two
distinct similar cases for positive and negative integers. *)
destruct (_ && _) eqn:?.
{ rewrite Bool.andb_true_iff in ×.
assert (0 ≤ x × y) by lia.
assert (x × y ≤ 2147483647 × 2147483647) by (apply Zmult_le_compat; lia).
destruct x; lia.
}
{ rewrite Bool.andb_false_iff in ×.
destruct (_ >? _) eqn:?; [destruct x; lia|].
assert (0 ≤ Pervasives.max_int ÷ x) by (autounfold with tezos_z; lia).
assert (Pervasives.max_int ÷ x ≤ Pervasives.max_int)
by (autounfold with tezos_z; apply Z.quot_le_upper_bound; lia).
assert (Pervasives.Int.Valid.t (Pervasives.max_int / x))
by (autounfold with tezos_z in *; lia).
assert (H_yx : y ≤ Pervasives.normalize_int (Pervasives.max_int ÷ x))
by (Utils.tezos_z_autounfold; lia).
rewrite Pervasives.normalize_identity in H_yx by lia.
assert (Pervasives.Int.Valid.t (x × y)%Z). {
Utils.tezos_z_autounfold.
split; [lia|].
assert (x × y ≤ x × (Pervasives.max_int ÷ x))
by (apply Zmult_le_compat; lia).
assert (x × (Pervasives.max_int ÷ x) ≤ Pervasives.max_int) by lia.
unfold Pervasives.max_int in *; lia.
}
assert (H_xy : 0 ≤ x × y ≤ Pervasives.max_int)
by (autounfold with tezos_z in *; lia).
destruct x; trivial;
now rewrite <- (Pervasives.normalize_identity (x := (_ × y)%Z)) in H_xy.
}
Qed.
Lemma mul_eq (x y : Saturation_repr.t) :
Valid.t x →
Valid.t y →
Saturation_repr.mul x y = saturate (x × y)%Z.
Proof.
intros.
unfold Saturation_repr.mul.
destruct x eqn:H_x_eq; [reflexivity | | lia].
assert (0 < x) by lia.
rewrite <- H_x_eq in *; clear H_x_eq.
repeat rewrite small_enough_eq by lia.
destruct (_ && _) eqn:?.
{ rewrite Bool.andb_true_iff in ×.
nia.
}
{ replace (Saturation_repr.saturated /i x)
with (Saturation_repr.saturated ÷ x)
by nia.
step; nia.
}
Qed.
Lemma scale_fast_valid : ∀ (x y : Saturation_repr.t),
Small_enough.t x →
Saturation_repr.Valid.t y →
Saturation_repr.Valid.t (Saturation_repr.scale_fast x y).
intros x y.
autorewrite with tezos_z.
intros Hx Hy.
Utils.tezos_z_autounfold.
unfold Saturation_repr.scale_fast.
autorewrite with tezos_z; try (autounfold with tezos_z; lia).
match goal with
[|- context[if ?e then _ else _]] ⇒ destruct e eqn:Eq_x
end; try lia.
rewrite Bool.andb_true_iff in ×.
repeat rewrite Z.leb_le in ×.
match goal with
[|- context[if ?e then _ else _]] ⇒ destruct e eqn:Eq_y
end; try Utils.tezos_z_auto; rewrite small_enough_eq in *;
try lia.
{ repeat rewrite Bool.andb_true_iff in ×.
repeat rewrite Z.leb_le in ×.
unfold Small_enough.t in Hx.
split; unfold op_star, normalize_int,
two_pow_62, two_pow_63; nia.
}
{ repeat rewrite Bool.andb_true_iff in *;
repeat rewrite Z.leb_le in ×.
match goal with
[|- context[if ?e then _ else _]] ⇒ destruct e eqn:Eq_y_lt
end; try Utils.tezos_z_auto.
unfold Small_enough.t in Hx.
unfold Pervasives.op_div in ×.
simpl in ×.
rewrite Z.gtb_ltb in ×.
rewrite Z.ltb_ge in ×.
unfold op_star.
{ rewrite Pervasives.normalize_identity in Eq_y_lt.
{ split; try apply Pervasives.normalize_never_exceeds.
nia.
}
{ nia. }
}
}
Qed.
Lemma scale_fast_eq : ∀ (x y : Saturation_repr.t),
Small_enough.t x → Valid.t y →
Saturation_repr.scale_fast x y = saturate (x × y)%Z.
unfold Saturation_repr.scale_fast.
intros x y [Hx1 Hx2] [Hy1 Hy2].
autounfold with tezos_z; simpl.
unfold saturate.
destruct (x =? 0) eqn:Hx.
{ rewrite Z.eqb_eq in Hx.
rewrite Hx; reflexivity.
}
{ rewrite small_enough_eq; auto.
destruct (y ≤i 2147483647) eqn:Hy3.
{ simpl in Hy3.
rewrite Z.leb_le in Hy3.
rewrite Pervasives.normalize_identity.
{ rewrite Z.max_l.
{ rewrite Z.min_l; auto.
unfold Saturation_repr.saturated,
Pervasives.max_int; nia.
}
{ unfold Saturation_repr.saturated,
Pervasives.max_int;
apply Z.min_glb; try nia.
}
}
{ unfold Pervasives.Int.Valid.t.
unfold Pervasives.min_int,
Pervasives.max_int; nia.
}
}
{ destruct (Z.gtb y) eqn:Hy4.
{ rewrite Z.gtb_lt in Hy4.
rewrite Pervasives.normalize_identity in Hy4.
{ unfold Saturation_repr.saturated,
Pervasives.max_int.
rewrite Z.max_l.
{ rewrite Z.min_r; auto; nia. }
{ apply Z.min_glb; lia. }
}
{ nia. }
}
{ rewrite Pervasives.normalize_identity in Hy4.
{ rewrite Z.gtb_ltb in Hy4.
rewrite Z.ltb_ge in Hy4.
assert (x × y ≤ 4611686018427387903) by nia.
rewrite Pervasives.normalize_identity; nia.
}
{ nia. }
}
}
}
Qed.
Lemma z_encoding_is_valid :
Data_encoding.Valid.t Strictly_valid.t Saturation_repr.z_encoding.
Data_encoding.Valid.data_encoding_auto.
intros; simpl; repeat split.
now apply Saturation_repr.t_to_z_exn_to_z.
Qed.
#[global] Hint Resolve z_encoding_is_valid : Data_encoding_db.
Lemma shift_right_is_valid : ∀ x y,
Valid.t x → 0 ≤ y → Valid.t (Saturation_repr.shift_right x y).
intros x y [Hx1 Hx2] Hy.
autounfold with tezos_z in ×.
unfold Saturation_repr.shift_right, lsr.
pose proof (Hx3 := Hx1).
rewrite <- Z.geb_le in Hx3.
rewrite Hx3.
split.
{ apply Z.shiftr_nonneg; auto. }
{ rewrite Z.shiftr_div_pow2; lia. }
Qed.
Lemma shift_right_eq : ∀ x y,
0 ≤ x →
Saturation_repr.shift_right x y = Z.shiftr x y.
intros x y Hx.
unfold Saturation_repr.shift_right, lsr.
rewrite <- Z.geb_le in Hx.
rewrite Hx; reflexivity.
Qed.
Lemma shift_left_is_valid : ∀ x y,
Valid.t x → y ≤ 0 → Valid.t (Saturation_repr.shift_left x y).
intros x y [Hx1 Hx2] Hy.
autounfold with tezos_z in ×.
unfold Saturation_repr.shift_left,
Saturation_repr.op_lt,
Saturation_repr.saturated,
Pervasives.max_int,
"<i".
simpl. cbn.
destruct (Z.ltb _ x); try lia.
unfold Pervasives.lsl, Pervasives.land.
rewrite Z.land_comm.
unfold Z.land.
unfold two_pow_63.
unfold BinInt.Z.sub.
unfold BinInt.Z.add.
unfold Z.opp.
unfold Z.pos_sub.
assert (0 ≤ Z.shiftl x y) by
(apply Z.shiftl_nonneg; auto).
destruct (Z.shiftl x y) eqn:G; try lia.
split.
{ rewrite Pervasives.normalize_identity; try lia.
autounfold with tezos_z; split; try lia.
unfold Z.of_N.
destruct (Pos.land _ _) eqn:G1; try lia.
apply Pos2Z.pos_le_pos.
pose proof (Aux_lemmas.pos_land_le_r
(Pos.pred_double 4611686018427387904) p ).
assert (Z.pos p ≤ x).
{ rewrite <- G.
rewrite Z.shiftl_div_pow2; nia.
}
apply Aux_lemmas.Zpos_le_to_pos_le; lia.
}
{ lia. }
Qed.
Lemma shift_left_eq : ∀ x y, 0 ≤ x →
Saturation_repr.shift_left x y =
Z.min Saturation_repr.saturated (Z.shiftl x y).
Proof.
intros x y Hx.
unfold Saturation_repr.shift_left,
Saturation_repr.op_lt.
match goal with
| |- context [if ?e then _ else _] ⇒
destruct e eqn:G; simpl in G
end.
{ rewrite Z.min_l; auto.
rewrite Z.ltb_lt in G.
unfold Saturation_repr.saturated,
Pervasives.max_int in ×.
unfold Saturation_repr.shift_right, lsr in G.
simpl in G.
destruct (Z.le_ge_cases 0 y).
{ rewrite Z.shiftl_mul_pow2; auto.
rewrite Z.shiftr_div_pow2 in G; auto.
assert (0 < 2 ^ y) by (apply Z.pow_pos_nonneg; lia).
nia.
}
{ rewrite Z.shiftl_div_pow2; auto.
rewrite Z.shiftr_mul_pow2 in G; auto.
assert (0 < 2 ^ (- y)) by (apply Z.pow_pos_nonneg; lia).
nia.
}
}
{ unfold Pervasives.lsl.
unfold normalize_int.
assert (Z.shiftl x y ≤ Saturation_repr.saturated).
{ rewrite Z.ltb_ge in G.
unfold Saturation_repr.saturated,
Pervasives.max_int in ×.
unfold Saturation_repr.shift_right, lsr in G.
simpl in G.
destruct (Z.le_ge_cases 0 y).
{ rewrite Z.shiftl_mul_pow2; auto.
rewrite Z.shiftr_div_pow2 in G; auto.
assert (0 < 2 ^ y) by (apply Z.pow_pos_nonneg; lia).
nia.
}
{ rewrite Z.shiftl_div_pow2; auto.
rewrite Z.shiftr_mul_pow2 in G; auto.
assert (0 < 2 ^ (- y)) by (apply Z.pow_pos_nonneg; lia).
nia.
}
}
rewrite Z.min_r; auto.
unfold land.
assert (Z.land (Z.shiftl x y) (two_pow_63 - 1) =
Z.shiftl x y).
{ rewrite <- (Z.shiftl_nonneg _ y) in Hx.
unfold Z.land.
destruct (Z.shiftl x y) eqn:G1; try lia.
simpl.
unfold Z.of_N.
assert (9223372036854775807%positive
= Aux_lemmas.positive_ones 62) as G2 by auto.
rewrite G2.
rewrite Aux_lemmas.land_positive_ones; auto.
apply Aux_lemmas.Zpos_le_to_pos_le.
unfold Saturation_repr.saturated,
Pervasives.max_int in H; lia.
}
rewrite H0.
unfold Saturation_repr.saturated,
Pervasives.max_int,
two_pow_62,
two_pow_63 in ×.
rewrite <- (Z.shiftl_nonneg _ y) in Hx.
lia.
}
Qed.
Lemma mul_fast_is_valid : ∀ x y,
Small_enough.t x → Small_enough.t y →
Valid.t (Saturation_repr.mul_fast x y).
nia.
Qed.
Lemma mul_fast_eq : ∀ x y,
Small_enough.t x → Small_enough.t y →
Saturation_repr.mul_fast x y = (x × y)%Z.
nia.
Qed.
Lemma succ_is_valid : ∀ x,
Valid.t (Saturation_repr.succ x).
intros; apply add_is_valid.
Qed.
Lemma succ_eq : ∀ x, Valid.t x →
Saturation_repr.succ x = saturate (1 + x)%Z.
intros; apply add_eq; lia.
Qed.
Lemma erem_is_valid : ∀ x y,
0 ≤ x → Valid.t y → 0 ≠ y →
Valid.t (Saturation_repr.erem x y).
lia.
Qed.
Lemma erem_eq : ∀ x y,
0 ≤ x → Valid.t y → 0 ≠ y →
Saturation_repr.erem x y = BinInt.Z.rem x y.
lia.
Qed.
Lemma ediv_is_valid : ∀ x y,
Valid.t x → 0 < y →
Valid.t (Saturation_repr.ediv x y).
intros; unfold Saturation_repr.ediv, "/i".
rewrite Pervasives.normalize_identity; nia.
Qed.
Lemma ediv_eq : ∀ x y,
Valid.t x → 0 < y →
Saturation_repr.ediv x y = x / y.
Proof.
intros; unfold Saturation_repr.ediv, "/i".
rewrite Pervasives.normalize_identity; nia.
Qed.
0 × 0 ≤ Saturation_repr.saturated ∧ 2147483647 × 2147483647 ≤ Saturation_repr.saturated.
lia.
Qed.
Lemma saturation_repr_valid_eq : ∀ (x: int),
Saturation_repr.Valid.t x ↔
(((0 <=? x) && (x <=? 4611686018427387903))%bool = true).
lia.
Qed.
#[global] Hint Rewrite saturation_repr_valid_eq : tezos_z.
Lemma mul_is_valid : ∀ (x y : int),
Saturation_repr.Valid.t x →
Saturation_repr.Valid.t y →
Saturation_repr.Valid.t (Saturation_repr.mul x y).
Proof.
Utils.tezos_z_autounfold; simpl.
intros x y Hx Hy.
repeat rewrite small_enough_eq; try lia; simpl.
(* Even if [x] appears first, we destruct it last to avoid generating two
distinct similar cases for positive and negative integers. *)
destruct (_ && _) eqn:?.
{ rewrite Bool.andb_true_iff in ×.
assert (0 ≤ x × y) by lia.
assert (x × y ≤ 2147483647 × 2147483647) by (apply Zmult_le_compat; lia).
destruct x; lia.
}
{ rewrite Bool.andb_false_iff in ×.
destruct (_ >? _) eqn:?; [destruct x; lia|].
assert (0 ≤ Pervasives.max_int ÷ x) by (autounfold with tezos_z; lia).
assert (Pervasives.max_int ÷ x ≤ Pervasives.max_int)
by (autounfold with tezos_z; apply Z.quot_le_upper_bound; lia).
assert (Pervasives.Int.Valid.t (Pervasives.max_int / x))
by (autounfold with tezos_z in *; lia).
assert (H_yx : y ≤ Pervasives.normalize_int (Pervasives.max_int ÷ x))
by (Utils.tezos_z_autounfold; lia).
rewrite Pervasives.normalize_identity in H_yx by lia.
assert (Pervasives.Int.Valid.t (x × y)%Z). {
Utils.tezos_z_autounfold.
split; [lia|].
assert (x × y ≤ x × (Pervasives.max_int ÷ x))
by (apply Zmult_le_compat; lia).
assert (x × (Pervasives.max_int ÷ x) ≤ Pervasives.max_int) by lia.
unfold Pervasives.max_int in *; lia.
}
assert (H_xy : 0 ≤ x × y ≤ Pervasives.max_int)
by (autounfold with tezos_z in *; lia).
destruct x; trivial;
now rewrite <- (Pervasives.normalize_identity (x := (_ × y)%Z)) in H_xy.
}
Qed.
Lemma mul_eq (x y : Saturation_repr.t) :
Valid.t x →
Valid.t y →
Saturation_repr.mul x y = saturate (x × y)%Z.
Proof.
intros.
unfold Saturation_repr.mul.
destruct x eqn:H_x_eq; [reflexivity | | lia].
assert (0 < x) by lia.
rewrite <- H_x_eq in *; clear H_x_eq.
repeat rewrite small_enough_eq by lia.
destruct (_ && _) eqn:?.
{ rewrite Bool.andb_true_iff in ×.
nia.
}
{ replace (Saturation_repr.saturated /i x)
with (Saturation_repr.saturated ÷ x)
by nia.
step; nia.
}
Qed.
Lemma scale_fast_valid : ∀ (x y : Saturation_repr.t),
Small_enough.t x →
Saturation_repr.Valid.t y →
Saturation_repr.Valid.t (Saturation_repr.scale_fast x y).
intros x y.
autorewrite with tezos_z.
intros Hx Hy.
Utils.tezos_z_autounfold.
unfold Saturation_repr.scale_fast.
autorewrite with tezos_z; try (autounfold with tezos_z; lia).
match goal with
[|- context[if ?e then _ else _]] ⇒ destruct e eqn:Eq_x
end; try lia.
rewrite Bool.andb_true_iff in ×.
repeat rewrite Z.leb_le in ×.
match goal with
[|- context[if ?e then _ else _]] ⇒ destruct e eqn:Eq_y
end; try Utils.tezos_z_auto; rewrite small_enough_eq in *;
try lia.
{ repeat rewrite Bool.andb_true_iff in ×.
repeat rewrite Z.leb_le in ×.
unfold Small_enough.t in Hx.
split; unfold op_star, normalize_int,
two_pow_62, two_pow_63; nia.
}
{ repeat rewrite Bool.andb_true_iff in *;
repeat rewrite Z.leb_le in ×.
match goal with
[|- context[if ?e then _ else _]] ⇒ destruct e eqn:Eq_y_lt
end; try Utils.tezos_z_auto.
unfold Small_enough.t in Hx.
unfold Pervasives.op_div in ×.
simpl in ×.
rewrite Z.gtb_ltb in ×.
rewrite Z.ltb_ge in ×.
unfold op_star.
{ rewrite Pervasives.normalize_identity in Eq_y_lt.
{ split; try apply Pervasives.normalize_never_exceeds.
nia.
}
{ nia. }
}
}
Qed.
Lemma scale_fast_eq : ∀ (x y : Saturation_repr.t),
Small_enough.t x → Valid.t y →
Saturation_repr.scale_fast x y = saturate (x × y)%Z.
unfold Saturation_repr.scale_fast.
intros x y [Hx1 Hx2] [Hy1 Hy2].
autounfold with tezos_z; simpl.
unfold saturate.
destruct (x =? 0) eqn:Hx.
{ rewrite Z.eqb_eq in Hx.
rewrite Hx; reflexivity.
}
{ rewrite small_enough_eq; auto.
destruct (y ≤i 2147483647) eqn:Hy3.
{ simpl in Hy3.
rewrite Z.leb_le in Hy3.
rewrite Pervasives.normalize_identity.
{ rewrite Z.max_l.
{ rewrite Z.min_l; auto.
unfold Saturation_repr.saturated,
Pervasives.max_int; nia.
}
{ unfold Saturation_repr.saturated,
Pervasives.max_int;
apply Z.min_glb; try nia.
}
}
{ unfold Pervasives.Int.Valid.t.
unfold Pervasives.min_int,
Pervasives.max_int; nia.
}
}
{ destruct (Z.gtb y) eqn:Hy4.
{ rewrite Z.gtb_lt in Hy4.
rewrite Pervasives.normalize_identity in Hy4.
{ unfold Saturation_repr.saturated,
Pervasives.max_int.
rewrite Z.max_l.
{ rewrite Z.min_r; auto; nia. }
{ apply Z.min_glb; lia. }
}
{ nia. }
}
{ rewrite Pervasives.normalize_identity in Hy4.
{ rewrite Z.gtb_ltb in Hy4.
rewrite Z.ltb_ge in Hy4.
assert (x × y ≤ 4611686018427387903) by nia.
rewrite Pervasives.normalize_identity; nia.
}
{ nia. }
}
}
}
Qed.
Lemma z_encoding_is_valid :
Data_encoding.Valid.t Strictly_valid.t Saturation_repr.z_encoding.
Data_encoding.Valid.data_encoding_auto.
intros; simpl; repeat split.
now apply Saturation_repr.t_to_z_exn_to_z.
Qed.
#[global] Hint Resolve z_encoding_is_valid : Data_encoding_db.
Lemma shift_right_is_valid : ∀ x y,
Valid.t x → 0 ≤ y → Valid.t (Saturation_repr.shift_right x y).
intros x y [Hx1 Hx2] Hy.
autounfold with tezos_z in ×.
unfold Saturation_repr.shift_right, lsr.
pose proof (Hx3 := Hx1).
rewrite <- Z.geb_le in Hx3.
rewrite Hx3.
split.
{ apply Z.shiftr_nonneg; auto. }
{ rewrite Z.shiftr_div_pow2; lia. }
Qed.
Lemma shift_right_eq : ∀ x y,
0 ≤ x →
Saturation_repr.shift_right x y = Z.shiftr x y.
intros x y Hx.
unfold Saturation_repr.shift_right, lsr.
rewrite <- Z.geb_le in Hx.
rewrite Hx; reflexivity.
Qed.
Lemma shift_left_is_valid : ∀ x y,
Valid.t x → y ≤ 0 → Valid.t (Saturation_repr.shift_left x y).
intros x y [Hx1 Hx2] Hy.
autounfold with tezos_z in ×.
unfold Saturation_repr.shift_left,
Saturation_repr.op_lt,
Saturation_repr.saturated,
Pervasives.max_int,
"<i".
simpl. cbn.
destruct (Z.ltb _ x); try lia.
unfold Pervasives.lsl, Pervasives.land.
rewrite Z.land_comm.
unfold Z.land.
unfold two_pow_63.
unfold BinInt.Z.sub.
unfold BinInt.Z.add.
unfold Z.opp.
unfold Z.pos_sub.
assert (0 ≤ Z.shiftl x y) by
(apply Z.shiftl_nonneg; auto).
destruct (Z.shiftl x y) eqn:G; try lia.
split.
{ rewrite Pervasives.normalize_identity; try lia.
autounfold with tezos_z; split; try lia.
unfold Z.of_N.
destruct (Pos.land _ _) eqn:G1; try lia.
apply Pos2Z.pos_le_pos.
pose proof (Aux_lemmas.pos_land_le_r
(Pos.pred_double 4611686018427387904) p ).
assert (Z.pos p ≤ x).
{ rewrite <- G.
rewrite Z.shiftl_div_pow2; nia.
}
apply Aux_lemmas.Zpos_le_to_pos_le; lia.
}
{ lia. }
Qed.
Lemma shift_left_eq : ∀ x y, 0 ≤ x →
Saturation_repr.shift_left x y =
Z.min Saturation_repr.saturated (Z.shiftl x y).
Proof.
intros x y Hx.
unfold Saturation_repr.shift_left,
Saturation_repr.op_lt.
match goal with
| |- context [if ?e then _ else _] ⇒
destruct e eqn:G; simpl in G
end.
{ rewrite Z.min_l; auto.
rewrite Z.ltb_lt in G.
unfold Saturation_repr.saturated,
Pervasives.max_int in ×.
unfold Saturation_repr.shift_right, lsr in G.
simpl in G.
destruct (Z.le_ge_cases 0 y).
{ rewrite Z.shiftl_mul_pow2; auto.
rewrite Z.shiftr_div_pow2 in G; auto.
assert (0 < 2 ^ y) by (apply Z.pow_pos_nonneg; lia).
nia.
}
{ rewrite Z.shiftl_div_pow2; auto.
rewrite Z.shiftr_mul_pow2 in G; auto.
assert (0 < 2 ^ (- y)) by (apply Z.pow_pos_nonneg; lia).
nia.
}
}
{ unfold Pervasives.lsl.
unfold normalize_int.
assert (Z.shiftl x y ≤ Saturation_repr.saturated).
{ rewrite Z.ltb_ge in G.
unfold Saturation_repr.saturated,
Pervasives.max_int in ×.
unfold Saturation_repr.shift_right, lsr in G.
simpl in G.
destruct (Z.le_ge_cases 0 y).
{ rewrite Z.shiftl_mul_pow2; auto.
rewrite Z.shiftr_div_pow2 in G; auto.
assert (0 < 2 ^ y) by (apply Z.pow_pos_nonneg; lia).
nia.
}
{ rewrite Z.shiftl_div_pow2; auto.
rewrite Z.shiftr_mul_pow2 in G; auto.
assert (0 < 2 ^ (- y)) by (apply Z.pow_pos_nonneg; lia).
nia.
}
}
rewrite Z.min_r; auto.
unfold land.
assert (Z.land (Z.shiftl x y) (two_pow_63 - 1) =
Z.shiftl x y).
{ rewrite <- (Z.shiftl_nonneg _ y) in Hx.
unfold Z.land.
destruct (Z.shiftl x y) eqn:G1; try lia.
simpl.
unfold Z.of_N.
assert (9223372036854775807%positive
= Aux_lemmas.positive_ones 62) as G2 by auto.
rewrite G2.
rewrite Aux_lemmas.land_positive_ones; auto.
apply Aux_lemmas.Zpos_le_to_pos_le.
unfold Saturation_repr.saturated,
Pervasives.max_int in H; lia.
}
rewrite H0.
unfold Saturation_repr.saturated,
Pervasives.max_int,
two_pow_62,
two_pow_63 in ×.
rewrite <- (Z.shiftl_nonneg _ y) in Hx.
lia.
}
Qed.
Lemma mul_fast_is_valid : ∀ x y,
Small_enough.t x → Small_enough.t y →
Valid.t (Saturation_repr.mul_fast x y).
nia.
Qed.
Lemma mul_fast_eq : ∀ x y,
Small_enough.t x → Small_enough.t y →
Saturation_repr.mul_fast x y = (x × y)%Z.
nia.
Qed.
Lemma succ_is_valid : ∀ x,
Valid.t (Saturation_repr.succ x).
intros; apply add_is_valid.
Qed.
Lemma succ_eq : ∀ x, Valid.t x →
Saturation_repr.succ x = saturate (1 + x)%Z.
intros; apply add_eq; lia.
Qed.
Lemma erem_is_valid : ∀ x y,
0 ≤ x → Valid.t y → 0 ≠ y →
Valid.t (Saturation_repr.erem x y).
lia.
Qed.
Lemma erem_eq : ∀ x y,
0 ≤ x → Valid.t y → 0 ≠ y →
Saturation_repr.erem x y = BinInt.Z.rem x y.
lia.
Qed.
Lemma ediv_is_valid : ∀ x y,
Valid.t x → 0 < y →
Valid.t (Saturation_repr.ediv x y).
intros; unfold Saturation_repr.ediv, "/i".
rewrite Pervasives.normalize_identity; nia.
Qed.
Lemma ediv_eq : ∀ x y,
Valid.t x → 0 < y →
Saturation_repr.ediv x y = x / y.
Proof.
intros; unfold Saturation_repr.ediv, "/i".
rewrite Pervasives.normalize_identity; nia.
Qed.
[Saturation_repr.n_encoding] is valid
Lemma n_encoding_is_valid :
Data_encoding.Valid.t Strictly_valid.t Saturation_repr.n_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros; simpl; repeat split.
{ lia. }
{ now apply Saturation_repr.t_to_z_exn_to_z. }
Qed.
#[global] Hint Resolve n_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t Strictly_valid.t Saturation_repr.n_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros; simpl; repeat split.
{ lia. }
{ now apply Saturation_repr.t_to_z_exn_to_z. }
Qed.
#[global] Hint Resolve n_encoding_is_valid : Data_encoding_db.
[safe_int] is idempotent
Lemma safe_int_idemp (x : int) :
Saturation_repr.safe_int (Saturation_repr.safe_int x) = Saturation_repr.safe_int x.
Proof.
unfold Saturation_repr.safe_int,
Saturation_repr.saturate_if_undef,
Saturation_repr.of_int_opt,
Saturation_repr.saturate_if_undef.
cbn.
match goal with
| |- context [if ?e then Some x else None] ⇒
ez destruct e eqn:H_cond
end.
now rewrite H_cond.
Qed.
Saturation_repr.safe_int (Saturation_repr.safe_int x) = Saturation_repr.safe_int x.
Proof.
unfold Saturation_repr.safe_int,
Saturation_repr.saturate_if_undef,
Saturation_repr.of_int_opt,
Saturation_repr.saturate_if_undef.
cbn.
match goal with
| |- context [if ?e then Some x else None] ⇒
ez destruct e eqn:H_cond
end.
now rewrite H_cond.
Qed.