Skip to main content

🧮 Saturation_repr.v

Proofs

See code, Gitlab , OCaml

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

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.
    rewrite Bool.andb_true_iff; lia.
  Qed.

  Lemma implies_int_valid x : t x Pervasives.Int.Valid.t x.
    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.OxH
    | Datatypes.S mxI (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 qDatatypes.S (max_one q)
    | xO qDatatypes.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 iStrictly_valid.t i
  | NoneTrue
  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 zStrictly_valid.t z
  | NoneTrue
  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.
  intro H.
  unfold Saturation_repr.of_z_opt, to_int.
  rewrite Pervasives.normalize_identity.
  { now apply of_int_opt_eq. }
  { now apply Valid.implies_int_valid,
      Strictly_valid.implies_valid.
  }
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.
  Utils.tezos_z_autounfold. simpl. intros.
  unfold Saturation_repr.safe_int.
  unfold Saturation_repr.saturate_if_undef.
  rewrite of_int_opt_eq; auto.
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).
  Utils.tezos_z_autounfold. simpl. intros.
  match goal with
    [|- context[if ?e then _ else _]] ⇒ destruct e eqn:Eq_x
  end; try 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.div_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; trivial.
    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.
    destruct (_ >i _) eqn:?; 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.
        rewrite Pervasives.normalize_identity; 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.
  destruct (Z.ltb _ x); try lia.
  unfold lsl, 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).
  intros x y Hx.
  unfold Saturation_repr.shift_left,
    Saturation_repr.op_lt.
  destruct (_ <i _) eqn:G; simpl in G.
  { 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 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.
    rewrite Z.mod_small; try lia.
    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.