phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp_bitvector/definitions.v *)
Lemma bv_swrap_spec n (z i : Z):
  0 ≤ i →
  Z.testbit (bv_swrap n z) i =
    if bool_decide (i < Z.of_N n-1) then
      Z.testbit z i
    else
      Z.testbit z (Z.of_N n-1).
Proof.
  destruct (decide (0 < n)%N).
  - intros ?.
    unfold bv_swrap, bv_half_modulus, bv_modulus.
    replace (2 ^ Z.of_N n `div` 2) with (2 ^ (Z.of_N n - 1)). 2: {
      rewrite Z.pow_sub_r; lia.
    }
    case_bool_decide as Hi.
    + rewrite Z.sub_pow2_spec_low, bv_wrap_spec_low,
        Z.add_pow2_spec_low by lia.
      done.
    + destruct (decide (i = Z.of_N n - 1)) as [-> | Ineq].
      * rewrite Z.sub_pow2_spec_top, bv_wrap_spec_low, Z.add_pow2_spec_top by lia.
        by apply negb_involutive.
      * rewrite Z.sub_pow2_spec_high; [ | lia | | lia ]. 2: {
          replace (Z.succ (Z.of_N n - 1)) with (Z.of_N n) by lia.
          apply bv_wrap_in_range.
        }
        rewrite bv_wrap_spec_low by lia.
        rewrite Z.add_pow2_spec_top by lia.
        by apply negb_involutive.
  - intros ?.
    replace n with 0%N by lia.
    rewrite bool_decide_eq_false_2 by lia.
    unfold bv_swrap.
    rewrite bv_half_modulus_0, Z.add_0_r, Z.sub_0_r.
    unfold bv_wrap.
    change (bv_modulus 0) with 1.
    by rewrite Z.mod_1_r, Z.bits_0, Z.testbit_neg_r.
Qed.
(* stdpp_bitvector/definitions.v *)
(* The [BvWf] typeclass checks that the integer [z] can be
interpreted as a [n]-bit integer. [BvWf] is a typeclass such that it
can be automatically inferred for bitvector constants. *)
Class BvWf (n : N) (z : Z) : Prop
:=
    bv_wf : (0 <=? z) && (z <? bv_modulus n)
.
(* stdpp_bitvector/definitions.v *)
Instance bv_wf_pi n z : ProofIrrel (BvWf n z).
Proof. unfold BvWf. apply _. Qed.
(* stdpp_bitvector/definitions.v *)
Instance bv_wf_dec n z : Decision (BvWf n z).
Proof. unfold BvWf. apply _. Defined.
(* stdpp_bitvector/definitions.v *)
Ltac solve_BvWf
:=
  lazymatch goal with
    |- BvWf ?n ?v =>
      is_closed_term n;
      is_closed_term v;
      try (vm_compute; exact I);
      fail "Bitvector constant" v "does not fit into" n "bits"
  end.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wf_in_range n z:
  BvWf n z ↔ 0 ≤ z < bv_modulus n.
Proof. unfold BvWf. by rewrite andb_True, !Is_true_true, Z.leb_le, Z.ltb_lt. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_wf n z :
  BvWf n (bv_wrap n z).
Proof. apply bv_wf_in_range. apply bv_wrap_in_range. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wf_bitwise_op {n} op bop n1 n2 :
  (∀ k, Z.testbit (op n1 n2) k = bop (Z.testbit n1 k) (Z.testbit n2 k)) →
  (0 ≤ n1 → 0 ≤ n2 → 0 ≤ op n1 n2) →
  bop false false = false →
  BvWf n n1 →
  BvWf n n2 →
  BvWf n (op n1 n2).
Proof.
  intros Hbits Hnonneg Hop [? Hok1]%bv_wf_in_range [? Hok2]%bv_wf_in_range. apply bv_wf_in_range.
  split; [lia|].
  apply Z.bounded_iff_bits_nonneg; [lia..|]. intros l ?.
  eapply Z.bounded_iff_bits_nonneg in Hok1;[|try done; lia..].
  eapply Z.bounded_iff_bits_nonneg in Hok2;[|try done; lia..].
  by rewrite Hbits, Hok1, Hok2.
Qed.
(* stdpp_bitvector/definitions.v *)
(* * Definition of [bv n] *)
Record bv (n : N)
:= BV {
  bv_unsigned : Z;
  bv_is_wf : BvWf n bv_unsigned;
}.
(* stdpp_bitvector/definitions.v *)
Definition bv_signed {n} (b : bv n)
:= bv_swrap n (bv_unsigned b).
(* stdpp_bitvector/definitions.v *)
Lemma bv_eq n (b1 b2 : bv n) :
  b1 = b2 ↔ b1.(bv_unsigned) = b2.(bv_unsigned).
Proof.
  destruct b1, b2. unfold bv_unsigned. split; [ naive_solver|].
  intros. subst. f_equal. apply proof_irrel.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_neq n (b1 b2 : bv n) :
  b1 ≠ b2 ↔ b1.(bv_unsigned) ≠ b2.(bv_unsigned).
Proof. unfold not. by rewrite bv_eq. Qed.
(* stdpp_bitvector/definitions.v *)
Instance bv_unsigned_inj n : Inj (=) (=) (@bv_unsigned n).
Proof. intros ???. by apply bv_eq. Qed.
(* stdpp_bitvector/definitions.v *)
Definition Z_to_bv_checked (n : N) (z : Z) : option (bv n)
:=
  H ← guard (BvWf n z); Some (@BV n z H).
(* stdpp_bitvector/definitions.v *)
Definition Z_to_bv (n : N) (z : Z) : bv n :=
  @BV n (bv_wrap n z) _.
Next Obligation. apply bv_wrap_wf. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma Z_to_bv_unsigned n z:
  bv_unsigned (Z_to_bv n z) = bv_wrap n z.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma Z_to_bv_signed n z:
  bv_signed (Z_to_bv n z) = bv_swrap n z.
Proof. apply bv_swrap_wrap. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma Z_to_bv_small n z:
  0 ≤ z < bv_modulus n →
  bv_unsigned (Z_to_bv n z) = z.
Proof. rewrite Z_to_bv_unsigned. apply bv_wrap_small. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_unsigned_BV n z Hwf:
  bv_unsigned (@BV n z Hwf) = z.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_signed_BV n z Hwf:
  bv_signed (@BV n z Hwf) = bv_swrap n z.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_unsigned_in_range n (b : bv n):
  0 ≤ bv_unsigned b < bv_modulus n.
Proof. apply bv_wf_in_range. apply bv_is_wf. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_bv_unsigned n (b : bv n):
  bv_wrap n (bv_unsigned b) = bv_unsigned b.
Proof. rewrite bv_wrap_small; [done|apply bv_unsigned_in_range]. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma Z_to_bv_bv_unsigned n (b : bv n):
  Z_to_bv n (bv_unsigned b) = b.
Proof. apply bv_eq. by rewrite Z_to_bv_unsigned, bv_wrap_bv_unsigned. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_eq_wrap n (b1 b2 : bv n) :
  b1 = b2 ↔ bv_wrap n b1.(bv_unsigned) = bv_wrap n b2.(bv_unsigned).
Proof.
  rewrite !bv_wrap_small; [apply bv_eq | apply bv_unsigned_in_range..].
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_neq_wrap n (b1 b2 : bv n) :
  b1 ≠ b2 ↔ bv_wrap n b1.(bv_unsigned) ≠ bv_wrap n b2.(bv_unsigned).
Proof. unfold not. by rewrite bv_eq_wrap. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_eq_signed n (b1 b2 : bv n) :
  b1 = b2 ↔ bv_signed b1 = bv_signed b2.
Proof.
  split; [naive_solver |].
  unfold bv_signed, bv_swrap. intros ?.
  assert (bv_wrap n (bv_unsigned b1 + bv_half_modulus n)
          = bv_wrap n (bv_unsigned b2 + bv_half_modulus n)) as ?%bv_wrap_add_inj by lia.
  by apply bv_eq_wrap.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_signed_in_range n (b : bv n):
  n ≠ 0%N →
  - bv_half_modulus n ≤ bv_signed b < bv_half_modulus n.
Proof. apply bv_swrap_in_range. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_unsigned_spec_high i n (b : bv n) :
  Z.of_N n ≤ i →
  Z.testbit (bv_unsigned b) i = false.
Proof.
  intros ?. pose proof (bv_unsigned_in_range _ b). unfold bv_modulus in *.
  eapply Z.bounded_iff_bits_nonneg; [..|done]; lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_unsigned_N_0 (b : bv 0):
  bv_unsigned b = 0.
Proof.
  pose proof bv_unsigned_in_range 0 b as H.
  rewrite bv_modulus_0 in H. lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_signed_N_0 (b : bv 0):
  bv_signed b = 0.
Proof. unfold bv_signed. by rewrite bv_unsigned_N_0, bv_swrap_0. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_swrap_bv_signed n (b : bv n):
  bv_swrap n (bv_signed b) = bv_signed b.
Proof.
  destruct (decide (n = 0%N)); subst.
  { by rewrite bv_signed_N_0, bv_swrap_0. }
  apply bv_swrap_small. by apply bv_signed_in_range.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma Z_to_bv_checked_bv_unsigned n (b : bv n):
  Z_to_bv_checked n (bv_unsigned b) = Some b.
Proof.
  unfold Z_to_bv_checked. case_guard; simplify_option_eq.
  - f_equal. by apply bv_eq.
  - by pose proof bv_is_wf b.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma Z_to_bv_checked_Some n a (b : bv n):
  Z_to_bv_checked n a = Some b ↔ a = bv_unsigned b.
Proof.
  split.
  - unfold Z_to_bv_checked. case_guard; [|done]. intros ?. by simplify_option_eq.
  - intros ->. apply Z_to_bv_checked_bv_unsigned.
Qed.
(* stdpp_bitvector/definitions.v *)
(* * Typeclass instances for [bv n] *)
Instance bv_eq_dec n : EqDecision (bv n) := λ '(@BV _ v1 p1) '(@BV _ v2 p2),
   match decide (v1 = v2) with
   | left eqv => left _
   | right eqv => right _
   end.
Next Obligation.
  (* TODO: Can we get a better proof term here? *)
  intros n b1 v1 p1 ? b2 v2 p2 ????. subst.
  rewrite (proof_irrel p1 p2). exact eq_refl.
Defined.
(* stdpp_bitvector/definitions.v *)
Instance bv_countable n : Countable (bv n)
:=
  inj_countable bv_unsigned (Z_to_bv_checked n) (Z_to_bv_checked_bv_unsigned n).
(* stdpp_bitvector/definitions.v *)
Instance bv_finite n : Finite (bv n) :=
  {| enum := Z_to_bv n <$> (seqZ 0 (bv_modulus n)) |}.
Next Obligation.
  intros n. apply NoDup_alt. intros i j x.
  rewrite !list_lookup_fmap.
  intros [? [[??]%lookup_seqZ ?]]%fmap_Some.
  intros [? [[??]%lookup_seqZ Hz]]%fmap_Some. subst.
  apply bv_eq in Hz. rewrite !Z_to_bv_small in Hz; lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_1_ind (P : bv 1 → Prop) :
  P (@BV 1 1 I) → P (@BV 1 0 I) → ∀ b : bv 1, P b.
Proof.
  intros ??. apply Forall_finite. repeat constructor.
  - by assert ((@BV 1 0 I) = (Z_to_bv 1 (Z.of_nat 0 + 0))) as <- by by apply bv_eq.
  - by assert ((@BV 1 1 I) = (Z_to_bv 1 (Z.of_nat 1 + 0))) as <- by by apply bv_eq.
Qed.
(* stdpp_bitvector/definitions.v *)
(* * [bv_saturate]: Add range facts about bit vectors to the context *)
Lemma bv_unsigned_in_range_alt n (b : bv n):
  -1 < bv_unsigned b < bv_modulus n.
Proof. pose proof (bv_unsigned_in_range _ b). lia. Qed.
(* stdpp_bitvector/definitions.v *)
Ltac bv_saturate
:=
  repeat match goal with b : bv _ |- _ => first [
     clear b | (* Clear if unused *)
     (* We use [bv_unsigned_in_range_alt] instead of
     [bv_unsigned_in_range] since hypothesis of the form [0 ≤ ... < ...]
     can cause significant slowdowns in
     [Z.euclidean_division_equations_cleanup] due to
     https://github.com/coq/coq/pull/17984 . *)
     learn_hyp (bv_unsigned_in_range_alt _ b) |
     learn_hyp (bv_signed_in_range _ b)
  ] end.
(* stdpp_bitvector/definitions.v *)
Ltac bv_saturate_unsigned
:=
  repeat match goal with b : bv _ |- _ => first [
     clear b | (* Clear if unused *)
     (* See comment in [bv_saturate]. *)
     learn_hyp (bv_unsigned_in_range_alt _ b)
  ] end.
(* stdpp_bitvector/definitions.v *)
(* * Operations on [bv n] *)
Definition bv_0 (n : N) :=
  @BV n 0 _.
Next Obligation.
  intros n. apply bv_wf_in_range. split; [done| apply bv_modulus_pos].
Qed.
(* stdpp_bitvector/definitions.v *)
Instance bv_inhabited n : Inhabited (bv n)
:= populate (bv_0 n).
(* stdpp_bitvector/definitions.v *)
Definition bv_succ {n} (x : bv n) : bv n
:=
  Z_to_bv n (Z.succ (bv_unsigned x)).
(* stdpp_bitvector/definitions.v *)
Definition bv_pred {n} (x : bv n) : bv n
:=
  Z_to_bv n (Z.pred (bv_unsigned x)).
(* stdpp_bitvector/definitions.v *)
Definition bv_add {n} (x y : bv n) : bv n
:= (* SMT: bvadd *)
  Z_to_bv n (Z.add (bv_unsigned x) (bv_unsigned y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_sub {n} (x y : bv n) : bv n
:= (* SMT: bvsub *)
  Z_to_bv n (Z.sub (bv_unsigned x) (bv_unsigned y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_opp {n} (x : bv n) : bv n
:= (* SMT: bvneg *)
  Z_to_bv n (Z.opp (bv_unsigned x)).
(* stdpp_bitvector/definitions.v *)
Definition bv_mul {n} (x y : bv n) : bv n
:= (* SMT: bvmul *)
  Z_to_bv n (Z.mul (bv_unsigned x) (bv_unsigned y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_divu {n} (x y : bv n) : bv n := (* SMT: bvudiv *)
  @BV n (Z.div (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
  intros n x y. apply bv_wf_in_range. bv_saturate.
  destruct (decide (bv_unsigned y = 0)) as [->|?].
  { rewrite Zdiv_0_r. lia. }
  split; [ apply Z.div_pos; lia |].
  apply (Z.le_lt_trans _ (bv_unsigned x)); [|lia].
  apply Z.div_le_upper_bound; [ lia|]. nia.
Qed.
(* stdpp_bitvector/definitions.v *)
Definition bv_modu {n} (x y : bv n) : bv n := (* SMT: bvurem *)
  @BV n (Z.modulo (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
  intros n x y. apply bv_wf_in_range. bv_saturate.
  destruct (decide (bv_unsigned y = 0)) as [->|?].
  { rewrite Zmod_0_r. lia. }
  split; [ apply Z.mod_pos; lia |].
  apply (Z.le_lt_trans _ (bv_unsigned x)); [|lia].
  apply Z.mod_le; lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Definition bv_divs {n} (x y : bv n) : bv n
:=
  Z_to_bv n (Z.div (bv_signed x) (bv_signed y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_quots {n} (x y : bv n) : bv n
:= (* SMT: bvsdiv *)
  Z_to_bv n (Z.quot (bv_signed x) (bv_signed y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_mods {n} (x y : bv n) : bv n
:= (* SMT: bvsmod *)
  Z_to_bv n (Z.modulo (bv_signed x) (bv_signed y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_rems {n} (x y : bv n) : bv n
:= (* SMT: bvsrem *)
  Z_to_bv n (Z.rem (bv_signed x) (bv_signed y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_shiftl {n} (x y : bv n) : bv n
:= (* SMT: bvshl *)
  Z_to_bv n (Z.shiftl (bv_unsigned x) (bv_unsigned y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_shiftr {n} (x y : bv n) : bv n := (* SMT: bvlshr *)
  @BV n (Z.shiftr (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
  intros n x y. apply bv_wf_in_range. bv_saturate.
  split; [ apply Z.shiftr_nonneg; lia|].
  rewrite Z.shiftr_div_pow2; [|lia].
  apply (Z.le_lt_trans _ (bv_unsigned x)); [|lia].
  pose proof (Z.pow_pos_nonneg 2 (bv_unsigned y)).
  apply Z.div_le_upper_bound; [ lia|]. nia.
Qed.
(* stdpp_bitvector/definitions.v *)
Definition bv_ashiftr {n} (x y : bv n) : bv n
:= (* SMT: bvashr *)
  Z_to_bv n (Z.shiftr (bv_signed x) (bv_unsigned y)).
(* stdpp_bitvector/definitions.v *)
Definition bv_or {n} (x y : bv n) : bv n := (* SMT: bvor *)
  @BV n (Z.lor (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
  intros. eapply bv_wf_bitwise_op; [ apply Z.lor_spec |
    by intros; eapply Z.lor_nonneg | done | apply bv_is_wf..].
Qed.
(* stdpp_bitvector/definitions.v *)
Definition bv_and {n} (x y : bv n) : bv n := (* SMT: bvand *)
  @BV n (Z.land (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
  intros. eapply bv_wf_bitwise_op; [ apply Z.land_spec |
    intros; eapply Z.land_nonneg; by left | done | apply bv_is_wf..].
Qed.
(* stdpp_bitvector/definitions.v *)
Definition bv_xor {n} (x y : bv n) : bv n := (* SMT: bvxor *)
  @BV n (Z.lxor (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
  intros. eapply bv_wf_bitwise_op; [ apply Z.lxor_spec |
    intros; eapply Z.lxor_nonneg; naive_solver | done | apply bv_is_wf..].
Qed.
(* stdpp_bitvector/definitions.v *)
Definition bv_not {n} (x : bv n) : bv n
:= (* SMT: bvnot *)
  Z_to_bv n (Z.lnot (bv_unsigned x)).
(* stdpp_bitvector/definitions.v *)
(* [bv_zero_extends z b] extends [b] to [z] bits with 0. If [z] is
smaller than [n], [b] is truncated. Note that [z] gives the resulting
size instead of the number of bits to add (as SMTLIB does) to avoid a
type-level [_ + _] *)
Definition bv_zero_extend {n} (z : N) (b : bv n) : bv z
:= (* SMT: zero_extend *)
  Z_to_bv z (bv_unsigned b).
(* stdpp_bitvector/definitions.v *)
Definition bv_sign_extend {n} (z : N) (b : bv n) : bv z
:= (* SMT: sign_extend *)
  Z_to_bv z (bv_signed b).
(* stdpp_bitvector/definitions.v *)
(* s is start index and l is length. Note that this is different from
extract in SMTLIB which uses [extract (inclusive upper bound)
(inclusive lower bound)]. The version here is phrased in a way that
makes it impossible to use an upper bound that is lower than the lower
bound. *)
Definition bv_extract {n} (s l : N) (b : bv n) : bv l
:=
  Z_to_bv l (bv_unsigned b ≫ Z.of_N s).
(* stdpp_bitvector/definitions.v *)
(* Note that we should always have n1 + n2 = n, but we use a parameter to avoid a type-level (_ + _) *)
Definition bv_concat n {n1 n2} (b1 : bv n1) (b2 : bv n2) : bv n
:= (* SMT: concat *)
  Z_to_bv n (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
(* stdpp_bitvector/definitions.v *)
Definition bv_to_little_endian m n (z : Z) : list (bv n)
:=
  (λ b, Z_to_bv n b) <$> Z_to_little_endian m (Z.of_N n) z.
(* stdpp_bitvector/definitions.v *)
Definition little_endian_to_bv n (bs : list (bv n)) : Z
:=
  little_endian_to_Z (Z.of_N n) (bv_unsigned <$> bs).
(* stdpp_bitvector/definitions.v *)
(* * Operations on [bv n] and Z *)
Definition bv_add_Z {n} (x : bv n) (y : Z) : bv n
:=
  Z_to_bv n (Z.add (bv_unsigned x) y).
(* stdpp_bitvector/definitions.v *)
Definition bv_sub_Z {n} (x : bv n) (y : Z) : bv n
:=
  Z_to_bv n (Z.sub (bv_unsigned x) y).
(* stdpp_bitvector/definitions.v *)
Definition bv_mul_Z {n} (x : bv n) (y : Z) : bv n
:=
  Z_to_bv n (Z.mul (bv_unsigned x) y).
(* stdpp_bitvector/definitions.v *)
Definition bv_seq {n} (x : bv n) (len : Z) : list (bv n)
:=
  (bv_add_Z x) <$> seqZ 0 len.
(* stdpp_bitvector/definitions.v *)
(* * Operations on [bv n] and bool *)
Definition bool_to_bv (n : N) (b : bool) : bv n
:=
  Z_to_bv n (bool_to_Z b).
(* stdpp_bitvector/definitions.v *)
Definition bv_to_bits {n} (b : bv n) : list bool
:=
  (λ i, Z.testbit (bv_unsigned b) i) <$> seqZ 0 (Z.of_N n).
(* stdpp_bitvector/definitions.v *)
Notation "- x"
:= (bv_opp x) : bv_scope.
(* stdpp_bitvector/definitions.v *)
(* This adds number notations into [bv_scope].
If the number literal is positive or 0, it gets expanded to [BV _ {num} _].
If the number literal is negative, it gets expanded as [Z_to_bv _ {num}].
In the negative case, the notation is parsing only and the [Z_to_bv] call will be
printed explicitly. *)
Inductive bv_number_notation
:= BVNumNonNeg (z : Z) | BVNumNeg (z : Z).
(* stdpp_bitvector/definitions.v *)
Definition bv_number_notation_to_Z (n : bv_number_notation) : option Z
:=
  match n with
  | BVNumNonNeg z => Some z
  (** Don't use the notation for negative numbers for printing. *)
  | BVNumNeg z => None
  end.
(* stdpp_bitvector/definitions.v *)
Definition Z_to_bv_number_notation (z : Z)
:=
  match z with
  | Zneg _ => BVNumNeg z
  | _ => BVNumNonNeg z
  end.
(* stdpp_bitvector/definitions.v *)
Class BvWrapSimplify (n : N) (z z' : Z)
:= {
  bv_wrap_simplify_proof : bv_wrap n z = bv_wrap n z';
}.
(* stdpp_bitvector/definitions.v *)
(* Default instance to end search. *)
Lemma bv_wrap_simplify_id n z :
  BvWrapSimplify n z z.
Proof. by constructor. Qed.
(* stdpp_bitvector/definitions.v *)
(* [bv_wrap_simplify_bv_wrap] performs the actual simplification. *)
Lemma bv_wrap_simplify_bv_wrap n z z' :
  BvWrapSimplify n z z' →
  BvWrapSimplify n (bv_wrap n z) z'.
Proof. intros [->]. constructor. by rewrite bv_wrap_bv_wrap. Qed.
(* stdpp_bitvector/definitions.v *)
(* The rest of the instances propagate [BvWrapSimplify]. *)
Lemma bv_wrap_simplify_succ n z z' :
  BvWrapSimplify n z z' →
  BvWrapSimplify n (Z.succ z) (Z.succ z').
Proof.
  intros [Hz]. constructor. by rewrite <-bv_wrap_succ_idemp, Hz, bv_wrap_succ_idemp.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_simplify_pred n z z' :
  BvWrapSimplify n z z' →
  BvWrapSimplify n (Z.pred z) (Z.pred z').
Proof.
  intros [Hz]. constructor. by rewrite <-bv_wrap_pred_idemp, Hz, bv_wrap_pred_idemp.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_simplify_opp n z z' :
  BvWrapSimplify n z z' →
  BvWrapSimplify n (- z) (- z').
Proof.
  intros [Hz]. constructor. by rewrite <-bv_wrap_opp_idemp, Hz, bv_wrap_opp_idemp.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_simplify_add n z1 z1' z2 z2' :
  BvWrapSimplify n z1 z1' →
  BvWrapSimplify n z2 z2' →
  BvWrapSimplify n (z1 + z2) (z1' + z2').
Proof.
  intros [Hz1] [Hz2]. constructor.
  by rewrite <-bv_wrap_add_idemp, Hz1, Hz2, bv_wrap_add_idemp.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_simplify_sub n z1 z1' z2 z2' :
  BvWrapSimplify n z1 z1' →
  BvWrapSimplify n z2 z2' →
  BvWrapSimplify n (z1 - z2) (z1' - z2').
Proof.
  intros [Hz1] [Hz2]. constructor.
  by rewrite <-bv_wrap_sub_idemp, Hz1, Hz2, bv_wrap_sub_idemp.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_simplify_mul n z1 z1' z2 z2' :
  BvWrapSimplify n z1 z1' →
  BvWrapSimplify n z2 z2' →
  BvWrapSimplify n (z1 * z2) (z1' * z2').
Proof.
  intros [Hz1] [Hz2]. constructor.
  by rewrite <-bv_wrap_mul_idemp, Hz1, Hz2, bv_wrap_mul_idemp.
Qed.
(* stdpp_bitvector/definitions.v *)
(* [bv_wrap_simplify_left] applies for goals of the form [bv_wrap n z1 = _] and
 tries to simplify them by removing any [bv_wrap] inside z1. *)
Ltac bv_wrap_simplify_left
:=
  lazymatch goal with |- bv_wrap _ _ = _ => idtac end;
  etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _);
            typeclasses eauto with bv_wrap_simplify_db | ]
.
(* stdpp_bitvector/definitions.v *)
(* [bv_wrap_simplify] applies for goals of the form [bv_wrap n z1 = bv_wrap n z2] and
[bv_swrap n z1 = bv_swrap n z2] and tries to simplify them by removing any [bv_wrap]
and [bv_swrap] inside z1 and z2. *)
Ltac bv_wrap_simplify
:=
  unfold bv_signed, bv_swrap;
  try match goal with | |- _ - _ = _ - _ => f_equal end;
  bv_wrap_simplify_left;
  symmetry;
  bv_wrap_simplify_left;
  symmetry.
(* stdpp_bitvector/definitions.v *)
Ltac bv_wrap_simplify_solve
:=
  bv_wrap_simplify; f_equal; lia.
(* stdpp_bitvector/definitions.v *)
Lemma bv_0_unsigned :
    bv_unsigned (bv_0 n) = 0.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_0_signed :
    bv_signed (bv_0 n) = 0.
Proof. unfold bv_0. by rewrite bv_signed_BV, bv_swrap_0. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_succ_unsigned b :
    bv_unsigned (bv_succ b) = bv_wrap n (Z.succ (bv_unsigned b)).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_succ_signed b :
    bv_signed (bv_succ b) = bv_swrap n (Z.succ (bv_signed b)).
Proof. unfold bv_succ. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_pred_unsigned b :
    bv_unsigned (bv_pred b) = bv_wrap n (Z.pred (bv_unsigned b)).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_pred_signed b :
    bv_signed (bv_pred b) = bv_swrap n (Z.pred (bv_signed b)).
Proof. unfold bv_pred. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_unsigned b1 b2 :
    bv_unsigned (b1 + b2) = bv_wrap n (bv_unsigned b1 + bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_signed b1 b2 :
    bv_signed (b1 + b2) = bv_swrap n (bv_signed b1 + bv_signed b2).
Proof. unfold bv_add. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sub_unsigned b1 b2 :
    bv_unsigned (b1 - b2) = bv_wrap n (bv_unsigned b1 - bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sub_signed b1 b2 :
    bv_signed (b1 - b2) = bv_swrap n (bv_signed b1 - bv_signed b2).
Proof. unfold bv_sub. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_opp_unsigned b :
    bv_unsigned (- b) = bv_wrap n (- bv_unsigned b).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_opp_signed b :
    bv_signed (- b) = bv_swrap n (- bv_signed b).
Proof. unfold bv_opp. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_mul_unsigned b1 b2 :
    bv_unsigned (b1 * b2) = bv_wrap n (bv_unsigned b1 * bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_mul_signed b1 b2 :
    bv_signed (b1 * b2) = bv_swrap n (bv_signed b1 * bv_signed b2).
Proof. unfold bv_mul. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_divu_unsigned b1 b2 :
    bv_unsigned (b1 `divu` b2) = bv_unsigned b1 `div` bv_unsigned b2.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_divu_signed b1 b2 :
    bv_signed (b1 `divu` b2) = bv_swrap n (bv_unsigned b1 `div` bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_modu_unsigned b1 b2 :
    bv_unsigned (b1 `modu` b2) = bv_unsigned b1 `mod` bv_unsigned b2.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_modu_signed b1 b2 :
    bv_signed (b1 `modu` b2) = bv_swrap n (bv_unsigned b1 `mod` bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_divs_unsigned b1 b2 :
    bv_unsigned (b1 `divs` b2) = bv_wrap n (bv_signed b1 `div` bv_signed b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_divs_signed b1 b2 :
    bv_signed (b1 `divs` b2) = bv_swrap n (bv_signed b1 `div` bv_signed b2).
Proof. unfold bv_divs. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_quots_unsigned b1 b2 :
    bv_unsigned (b1 `quots` b2) = bv_wrap n (bv_signed b1 `quot` bv_signed b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_quots_signed b1 b2 :
    bv_signed (b1 `quots` b2) = bv_swrap n (bv_signed b1 `quot` bv_signed b2).
Proof. unfold bv_quots. rewrite Z_to_bv_signed. done. Qed.