diff --git a/_CoqProject b/_CoqProject
index c5842c0298688ab5037c8d112a8b5876f501d607..21efbb37bde9121aed8850a6c8a28396bb40a97c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -59,3 +59,5 @@ stdpp/telescopes.v
 stdpp/binders.v
 
 stdpp_unstable/bitblast.v
+stdpp_unstable/bitvector.v
+stdpp_unstable/bitvector_tactics.v
diff --git a/stdpp_unstable/bitvector.v b/stdpp_unstable/bitvector.v
new file mode 100644
index 0000000000000000000000000000000000000000..5908a2cbc658ef6c434ec9e505e45d3b559e4002
--- /dev/null
+++ b/stdpp_unstable/bitvector.v
@@ -0,0 +1,1331 @@
+(** This file is still experimental. See its tracking issue
+https://gitlab.mpi-sws.org/iris/stdpp/-/issues/145 for details on remaining
+issues before stabilization. This file is maintained by Michael Sammler. *)
+From stdpp Require Export numbers.
+From stdpp Require Import countable finite.
+From stdpp Require Import options.
+
+(** * bitvector library *)
+(** This file provides the [bv n] type for representing [n]-bit
+integers with the standard operations. It also provides the
+[bv_saturate] tactic for learning facts about the range of bit vector
+variables in context. More extensive automation can be found in
+[bitvector_auto.v].
+
+Additionally, this file provides the [bvn] type for representing a
+bitvector of arbitrary size. *)
+
+(** * Settings *)
+Local Open Scope Z_scope.
+
+(** * Preliminary definitions *)
+Definition bv_modulus (n : N) : Z := 2 ^ (Z.of_N n).
+Definition bv_half_modulus (n : N) : Z := bv_modulus n `div` 2.
+Definition bv_wrap (n : N) (z : Z) : Z := z `mod` bv_modulus n.
+Definition bv_swrap (n : N) (z : Z) : Z := bv_wrap n (z + bv_half_modulus n) - bv_half_modulus n.
+
+Lemma bv_modulus_pos n :
+  0 < bv_modulus n.
+Proof. apply Z.pow_pos_nonneg; lia. Qed.
+Lemma bv_modulus_gt_1 n :
+  n ≠ 0%N →
+  1 < bv_modulus n.
+Proof. intros ?. apply Z.pow_gt_1; lia. Qed.
+Lemma bv_half_modulus_nonneg n :
+  0 ≤ bv_half_modulus n.
+Proof. apply Z.div_pos; [|done]. pose proof bv_modulus_pos n. lia. Qed.
+
+Lemma bv_modulus_add n1 n2 :
+  bv_modulus (n1 + n2) = bv_modulus n1 * bv_modulus n2.
+Proof. unfold bv_modulus. rewrite N2Z.inj_add. eapply Z.pow_add_r; lia. Qed.
+
+Lemma bv_half_modulus_twice n:
+  n ≠ 0%N →
+  bv_half_modulus n + bv_half_modulus n = bv_modulus n.
+Proof.
+  intros. unfold bv_half_modulus, bv_modulus.
+  rewrite Z.add_diag. symmetry. apply Z_div_exact_2; [lia|].
+  rewrite <-Z.pow_pred_r by lia. rewrite Z.mul_comm. by apply Z.mod_mul.
+Qed.
+
+Lemma bv_half_modulus_lt_modulus n:
+  bv_half_modulus n < bv_modulus n.
+Proof.
+  pose proof bv_modulus_pos n.
+  apply Z_div_lt; [done| lia].
+Qed.
+
+Lemma bv_modulus_le_mono n m:
+  (n ≤ m)%N →
+  bv_modulus n ≤ bv_modulus m.
+Proof. intros. apply Z.pow_le_mono; [done|lia]. Qed.
+Lemma bv_half_modulus_le_mono n m:
+  (n ≤ m)%N →
+  bv_half_modulus n ≤ bv_half_modulus m.
+Proof. intros. apply Z.div_le_mono; [done|]. by apply bv_modulus_le_mono. Qed.
+
+Lemma bv_modulus_0:
+  bv_modulus 0 = 1.
+Proof. done. Qed.
+Lemma bv_half_modulus_0:
+  bv_half_modulus 0 = 0.
+Proof. done. Qed.
+
+Lemma bv_half_modulus_twice_mult n:
+  bv_half_modulus n + bv_half_modulus n = (Z.of_N n `min` 1) * bv_modulus n.
+Proof. destruct (decide (n = 0%N)); subst; [ rewrite bv_half_modulus_0 | rewrite bv_half_modulus_twice]; lia. Qed.
+
+Lemma bv_wrap_in_range n z:
+  0 ≤ bv_wrap n z < bv_modulus n.
+Proof. apply Z.mod_pos_bound. apply bv_modulus_pos. Qed.
+
+Lemma bv_swrap_in_range n z:
+  n ≠ 0%N →
+  - bv_half_modulus n ≤ bv_swrap n z < bv_half_modulus n.
+Proof.
+  intros ?. unfold bv_swrap.
+  pose proof bv_half_modulus_twice n.
+  pose proof bv_wrap_in_range n (z + bv_half_modulus n).
+  lia.
+Qed.
+
+Lemma bv_wrap_small n z :
+  0 ≤ z < bv_modulus n → bv_wrap n z = z.
+Proof. intros. by apply Z.mod_small. Qed.
+
+Lemma bv_swrap_small n z :
+  - bv_half_modulus n ≤ z < bv_half_modulus n →
+  bv_swrap n z = z.
+Proof.
+  intros Hrange. unfold bv_swrap.
+  destruct (decide (n = 0%N)); subst.
+  { rewrite bv_half_modulus_0 in Hrange. lia. }
+  pose proof bv_half_modulus_twice n.
+  rewrite bv_wrap_small by lia. lia.
+Qed.
+
+Lemma bv_wrap_0 n :
+  bv_wrap n 0 = 0.
+Proof. done. Qed.
+Lemma bv_swrap_0 n :
+  bv_swrap n 0 = 0.
+Proof.
+  pose proof bv_half_modulus_lt_modulus n.
+  pose proof bv_half_modulus_nonneg n.
+  unfold bv_swrap. rewrite bv_wrap_small; lia.
+Qed.
+
+Lemma bv_wrap_idemp n b : bv_wrap n (bv_wrap n b) = bv_wrap n b.
+Proof. unfold bv_wrap. by rewrite Zmod_mod. Qed.
+
+Definition bv_wrap_factor (n : N) (x z : Z) :=
+  x = - z `div` bv_modulus n.
+
+Lemma bv_wrap_factor_intro n z :
+  ∃ x, bv_wrap_factor n x z ∧ bv_wrap n z = z + x * bv_modulus n.
+Proof.
+  eexists _. split; [done|].
+  pose proof (bv_modulus_pos n). unfold bv_wrap. rewrite Z.mod_eq; lia.
+Qed.
+
+Lemma bv_wrap_add_modulus c n z:
+  bv_wrap n (z + c * bv_modulus n) = bv_wrap n z.
+Proof. apply Z_mod_plus_full. Qed.
+Lemma bv_wrap_add_modulus_1 n z:
+  bv_wrap n (z + bv_modulus n) = bv_wrap n z.
+Proof. rewrite <-(bv_wrap_add_modulus 1 n z). f_equal. lia. Qed.
+Lemma bv_wrap_sub_modulus c n z:
+  bv_wrap n (z - c * bv_modulus n) = bv_wrap n z.
+Proof. rewrite <-(bv_wrap_add_modulus (-c) n z). f_equal. lia. Qed.
+Lemma bv_wrap_sub_modulus_1 n z:
+  bv_wrap n (z - bv_modulus n) = bv_wrap n z.
+Proof. rewrite <-(bv_wrap_add_modulus (-1) n z). done. Qed.
+
+Lemma bv_wrap_add_idemp n x y :
+  bv_wrap n (bv_wrap n x + bv_wrap n y) = bv_wrap n (x + y).
+Proof. symmetry. apply Zplus_mod. Qed.
+Lemma bv_wrap_add_idemp_l n x y :
+  bv_wrap n (bv_wrap n x + y) = bv_wrap n (x + y).
+Proof. apply Zplus_mod_idemp_l. Qed.
+Lemma bv_wrap_add_idemp_r n x y :
+  bv_wrap n (x + bv_wrap n y) = bv_wrap n (x + y).
+Proof. apply Zplus_mod_idemp_r. Qed.
+
+Lemma bv_wrap_opp_idemp n x :
+  bv_wrap n (- bv_wrap n x) = bv_wrap n (- x).
+Proof.
+  unfold bv_wrap. pose proof (bv_modulus_pos n).
+  destruct (decide (x `mod` bv_modulus n = 0)) as [Hx|Hx].
+  - rewrite !Z.mod_opp_l_z; [done |lia|done|lia|by rewrite Hx].
+  - rewrite !Z.mod_opp_l_nz, Z.mod_mod;
+      [done|lia|lia|done|lia|by rewrite Z.mod_mod by lia].
+Qed.
+
+Lemma bv_wrap_mul_idemp n x y :
+  bv_wrap n (bv_wrap n x * bv_wrap n y) = bv_wrap n (x * y).
+Proof. etrans; [| apply Zmult_mod_idemp_r]. apply Zmult_mod_idemp_l. Qed.
+Lemma bv_wrap_mul_idemp_l n x y :
+  bv_wrap n (bv_wrap n x * y) = bv_wrap n (x * y).
+Proof. apply Zmult_mod_idemp_l. Qed.
+Lemma bv_wrap_mul_idemp_r n x y :
+  bv_wrap n (x * bv_wrap n y) = bv_wrap n (x * y).
+Proof. apply Zmult_mod_idemp_r. Qed.
+
+Lemma bv_wrap_sub_idemp n x y :
+  bv_wrap n (bv_wrap n x - bv_wrap n y) = bv_wrap n (x - y).
+Proof.
+  by rewrite <-!Z.add_opp_r, <-bv_wrap_add_idemp_r,
+    bv_wrap_opp_idemp, bv_wrap_add_idemp.
+ Qed.
+Lemma bv_wrap_sub_idemp_l n x y :
+  bv_wrap n (bv_wrap n x - y) = bv_wrap n (x - y).
+Proof. by rewrite <-!Z.add_opp_r, bv_wrap_add_idemp_l. Qed.
+Lemma bv_wrap_sub_idemp_r n x y :
+  bv_wrap n (x - bv_wrap n y) = bv_wrap n (x - y).
+Proof.
+  by rewrite <-!Z.add_opp_r, <-bv_wrap_add_idemp_r,
+    bv_wrap_opp_idemp, bv_wrap_add_idemp_r.
+Qed.
+
+Lemma bv_wrap_succ_idemp n x :
+  bv_wrap n (Z.succ (bv_wrap n x)) = bv_wrap n (Z.succ x).
+Proof. by rewrite <-!Z.add_1_r, bv_wrap_add_idemp_l. Qed.
+Lemma bv_wrap_pred_idemp n x :
+  bv_wrap n (Z.pred (bv_wrap n x)) = bv_wrap n (Z.pred x).
+Proof. by rewrite <-!Z.sub_1_r, bv_wrap_sub_idemp_l. Qed.
+
+Lemma bv_wrap_add_inj n x1 x2 y :
+  bv_wrap n x1 = bv_wrap n x2 ↔ bv_wrap n (x1 + y) = bv_wrap n (x2 + y).
+Proof.
+  split; intros Heq.
+  - by rewrite <-bv_wrap_add_idemp_l, Heq, bv_wrap_add_idemp_l.
+  - pose proof (bv_wrap_factor_intro n (x1 + y)) as [f1[? Hx1]].
+    pose proof (bv_wrap_factor_intro n (x2 + y)) as [f2[? Hx2]].
+    assert (x1 = x2 + f2 * bv_modulus n - f1 * bv_modulus n) as -> by lia.
+    by rewrite bv_wrap_sub_modulus, bv_wrap_add_modulus.
+Qed.
+
+Lemma bv_swrap_wrap n z:
+  bv_swrap n (bv_wrap n z) = bv_swrap n z.
+Proof. unfold bv_swrap, bv_wrap. by rewrite Zplus_mod_idemp_l. Qed.
+
+Lemma bv_wrap_bv_wrap n1 n2 bv :
+  (n1 ≤ n2)%N →
+  bv_wrap n1 (bv_wrap n2 bv) = bv_wrap n1 bv.
+Proof.
+  intros ?. unfold bv_wrap.
+  rewrite <-Znumtheory.Zmod_div_mod; [done| apply bv_modulus_pos.. |].
+  unfold bv_modulus. eexists (2 ^ (Z.of_N n2 - Z.of_N n1)).
+  rewrite <-Z.pow_add_r by lia. f_equal. lia.
+Qed.
+
+Lemma bv_wrap_land n z :
+  bv_wrap n z = Z.land z (Z.ones (Z.of_N n)).
+Proof. by rewrite Z.land_ones by lia. Qed.
+Lemma bv_wrap_spec n z i:
+  0 ≤ i →
+  Z.testbit (bv_wrap n z) i = bool_decide (i < Z.of_N n) && Z.testbit z i.
+Proof.
+  intros ?. rewrite bv_wrap_land, Z.land_spec, Z.ones_spec by lia.
+  case_bool_decide; simpl; by rewrite ?andb_true_r, ?andb_false_r.
+Qed.
+Lemma bv_wrap_spec_low n z i:
+  0 ≤ i < Z.of_N n →
+  Z.testbit (bv_wrap n z) i = Z.testbit z i.
+Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [done|]. lia. Qed.
+Lemma bv_wrap_spec_high n z i:
+  Z.of_N n ≤ i →
+  Z.testbit (bv_wrap n z) i = false.
+Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [|done]. lia. Qed.
+
+(** * [BvWf] *)
+(** 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)
+.
+Global Hint Mode BvWf + + : typeclass_instances.
+Global Instance bv_wf_pi n z : ProofIrrel (BvWf n z).
+Proof. unfold BvWf. apply _. Qed.
+Global Instance bv_wf_dec n z : Decision (BvWf n z).
+Proof. unfold BvWf. apply _. Defined.
+
+Typeclasses Opaque BvWf.
+
+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.
+Global Hint Extern 10 (BvWf _ _) => solve_BvWf : typeclass_instances.
+
+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.
+
+Lemma bv_wrap_wf n z :
+  BvWf n (bv_wrap n z).
+Proof. apply bv_wf_in_range. apply bv_wrap_in_range. Qed.
+
+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.
+
+(** * Definition of [bv n] *)
+Record bv (n : N) := BV {
+  bv_unsigned : Z;
+  bv_is_wf : BvWf n bv_unsigned;
+}.
+Global Arguments bv_unsigned {_}.
+Global Arguments bv_is_wf {_}.
+Global Arguments BV _ _ {_}.
+Add Printing Constructor bv.
+
+Global Arguments bv_unsigned : simpl never.
+
+Definition bv_signed {n} (b : bv n) := bv_swrap n (bv_unsigned b).
+
+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.
+
+Lemma bv_neq n (b1 b2 : bv n) :
+  b1 ≠ b2 ↔ b1.(bv_unsigned) ≠ b2.(bv_unsigned).
+Proof. unfold not. by rewrite bv_eq. Qed.
+
+Definition Z_to_bv_checked (n : N) (z : Z) : option (bv n) :=
+  guard (BvWf n z) as H; Some (@BV n z H).
+
+Program Definition Z_to_bv (n : N) (z : Z) : bv n :=
+  @BV n (bv_wrap n z) _.
+Next Obligation. apply bv_wrap_wf. Qed.
+
+Lemma Z_to_bv_unsigned n z:
+  bv_unsigned (Z_to_bv n z) = bv_wrap n z.
+Proof. done. Qed.
+
+Lemma Z_to_bv_signed n z:
+  bv_signed (Z_to_bv n z) = bv_swrap n z.
+Proof. apply bv_swrap_wrap. Qed.
+
+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.
+
+Lemma bv_unsigned_BV n z Hwf:
+  bv_unsigned (@BV n z Hwf) = z.
+Proof. done. Qed.
+
+Lemma bv_signed_BV n z Hwf:
+  bv_signed (@BV n z Hwf) = bv_swrap n z.
+Proof. done. Qed.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+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.
+
+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.
+
+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_option_guard.
+  - f_equal. by apply bv_eq.
+  - by pose proof bv_is_wf b.
+Qed.
+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_option_guard; [|done]. intros ?. by simplify_eq.
+  - intros ->. apply Z_to_bv_checked_bv_unsigned.
+Qed.
+
+(** * Typeclass instances for [bv n] *)
+Global Program 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.
+Next Obligation. intros. by injection. Qed.
+
+Global Instance bv_countable n : Countable (bv n) :=
+  inj_countable bv_unsigned (Z_to_bv_checked n) (Z_to_bv_checked_bv_unsigned n).
+
+Global Program 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.
+Next Obligation.
+  intros n x. apply elem_of_list_lookup. eexists (Z.to_nat (bv_unsigned x)).
+  rewrite list_lookup_fmap. apply fmap_Some. eexists _.
+  pose proof (bv_unsigned_in_range _ x). split.
+  - apply lookup_seqZ. split; [done|]. rewrite Z2Nat.id; lia.
+  - apply bv_eq. rewrite Z_to_bv_small; rewrite Z2Nat.id; lia.
+Qed.
+
+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.
+
+(** * [bv_saturate]: Add range facts about bit vectors to the context *)
+Ltac bv_saturate :=
+  repeat match goal with b : bv _ |- _ => first [
+     clear b | (* Clear if unused *)
+     learn_hyp (bv_unsigned_in_range _ b) |
+     learn_hyp (bv_signed_in_range _ b)
+  ] end.
+
+Ltac bv_saturate_unsigned :=
+  repeat match goal with b : bv _ |- _ => first [
+     clear b | (* Clear if unused *)
+     learn_hyp (bv_unsigned_in_range _ b)
+  ] end.
+
+(** * Operations on [bv n] *)
+Program Definition bv_0 (n : N) :=
+  @BV n 0 _.
+Next Obligation.
+  intros n. apply bv_wf_in_range. split; [done| apply bv_modulus_pos].
+Qed.
+Global Instance bv_inhabited n : Inhabited (bv n) := populate (bv_0 n).
+
+Definition bv_succ {n} (x : bv n) : bv n :=
+  Z_to_bv n (Z.succ (bv_unsigned x)).
+Definition bv_pred {n} (x : bv n) : bv n :=
+  Z_to_bv n (Z.pred (bv_unsigned x)).
+
+Definition bv_add {n} (x y : bv n) : bv n := (* SMT: bvadd *)
+  Z_to_bv n (Z.add (bv_unsigned x) (bv_unsigned y)).
+Definition bv_sub {n} (x y : bv n) : bv n := (* SMT: bvsub *)
+  Z_to_bv n (Z.sub (bv_unsigned x) (bv_unsigned y)).
+Definition bv_opp {n} (x : bv n) : bv n := (* SMT: bvneg *)
+  Z_to_bv n (Z.opp (bv_unsigned x)).
+
+Definition bv_mul {n} (x y : bv n) : bv n := (* SMT: bvmul *)
+  Z_to_bv n (Z.mul (bv_unsigned x) (bv_unsigned y)).
+Program 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.
+Program 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.
+Definition bv_divs {n} (x y : bv n) : bv n :=
+  Z_to_bv n (Z.div (bv_signed x) (bv_signed y)).
+Definition bv_quots {n} (x y : bv n) : bv n := (* SMT: bvsdiv *)
+  Z_to_bv n (Z.quot (bv_signed x) (bv_signed y)).
+Definition bv_mods {n} (x y : bv n) : bv n := (* SMT: bvsmod *)
+  Z_to_bv n (Z.modulo (bv_signed x) (bv_signed y)).
+Definition bv_rems {n} (x y : bv n) : bv n := (* SMT: bvsrem *)
+  Z_to_bv n (Z.rem (bv_signed x) (bv_signed y)).
+
+Definition bv_shiftl {n} (x y : bv n) : bv n := (* SMT: bvshl *)
+  Z_to_bv n (Z.shiftl (bv_unsigned x) (bv_unsigned y)).
+Program 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.
+Definition bv_ashiftr {n} (x y : bv n) : bv n := (* SMT: bvashr *)
+  Z_to_bv n (Z.shiftr (bv_signed x) (bv_unsigned y)).
+
+Program 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.
+Program 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.
+Program 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.
+Program Definition bv_not {n} (x : bv n) : bv n := (* SMT: bvnot *)
+  Z_to_bv n (Z.lnot (bv_unsigned x)).
+
+(* [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 [_ + _] *)
+Program Definition bv_zero_extend {n} (z : N) (b : bv n) : bv z := (* SMT: zero_extend *)
+  Z_to_bv z (bv_unsigned b).
+
+Program Definition bv_sign_extend {n} (z : N) (b : bv n) : bv z := (* SMT: sign_extend *)
+  Z_to_bv z (bv_signed b).
+
+(* 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).
+
+(* Note that we should always have n1 + n2 = n, but we use a parameter to avoid a type-level (_ + _) *)
+Program 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)).
+
+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.
+
+Definition little_endian_to_bv n (bs : list (bv n)) : Z :=
+  little_endian_to_Z (Z.of_N n) (bv_unsigned <$> bs).
+
+(** * 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).
+Definition bv_sub_Z {n} (x : bv n) (y : Z) : bv n :=
+  Z_to_bv n (Z.sub (bv_unsigned x) y).
+Definition bv_mul_Z {n} (x : bv n) (y : Z) : bv n :=
+  Z_to_bv n (Z.mul (bv_unsigned x) y).
+
+Definition bv_seq {n} (x : bv n) (len : Z) : list (bv n) :=
+  (bv_add_Z x) <$> seqZ 0 len.
+
+(** * Operations on [bv n] and bool *)
+Definition bool_to_bv (n : N) (b : bool) : bv n :=
+  Z_to_bv n (bool_to_Z b).
+
+Definition bv_to_bits {n} (b : bv n) : list bool :=
+  (λ i, Z.testbit (bv_unsigned b) i) <$> seqZ 0 (Z.of_N n).
+
+(** * Notation for [bv] operations *)
+Declare Scope bv_scope.
+Delimit Scope bv_scope with bv.
+Bind Scope bv_scope with bv.
+
+Infix "+" := bv_add : bv_scope.
+Infix "-" := bv_sub : bv_scope.
+Notation "- x" := (bv_opp x) : bv_scope.
+Infix "*" := bv_mul : bv_scope.
+Infix "`divu`" := bv_divu (at level 35) : bv_scope.
+Infix "`modu`" := bv_modu (at level 35) : bv_scope.
+Infix "`divs`" := bv_divs (at level 35) : bv_scope.
+Infix "`quots`" := bv_quots (at level 35) : bv_scope.
+Infix "`mods`" := bv_mods (at level 35) : bv_scope.
+Infix "`rems`" := bv_rems (at level 35) : bv_scope.
+Infix "≪" := bv_shiftl : bv_scope.
+Infix "≫" := bv_shiftr : bv_scope.
+Infix "`ashiftr`" := bv_ashiftr (at level 35) : bv_scope.
+
+Infix "`+Z`" := bv_add_Z (at level 50) : bv_scope.
+Infix "`-Z`" := bv_sub_Z (at level 50) : bv_scope.
+Infix "`*Z`" := bv_mul_Z (at level 40) : bv_scope.
+
+(** * [bv_wrap_simplify]: typeclass-based automation for simplifying [bv_wrap] *)
+(** The [bv_wrap_simplify] tactic removes [bv_wrap] where possible by
+using the fact that [bv_wrap n (bv_warp n z) = bv_wrap n z]. The main
+use case for this tactic is for proving the lemmas about the
+operations of [bv n] below. Users should use the more extensive
+automation provided by [bitvector_auto.v]. *)
+Create HintDb bv_wrap_simplify_db discriminated.
+Global Hint Constants Opaque : bv_wrap_simplify_db.
+Global Hint Variables Opaque : bv_wrap_simplify_db.
+
+Class BvWrapSimplify (n : N) (z z' : Z) := {
+  bv_wrap_simplify_proof : bv_wrap n z = bv_wrap n z';
+}.
+Global Arguments bv_wrap_simplify_proof _ _ _ {_}.
+Global Hint Mode BvWrapSimplify + + - : bv_wrap_simplify_db.
+
+(** Default instance to end search. *)
+Lemma bv_wrap_simplify_id n z :
+  BvWrapSimplify n z z.
+Proof. by constructor. Qed.
+Global Hint Resolve bv_wrap_simplify_id | 1000 : bv_wrap_simplify_db.
+
+(** [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.
+Global Hint Resolve bv_wrap_simplify_bv_wrap | 10 : bv_wrap_simplify_db.
+
+(** 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.
+Global Hint Resolve bv_wrap_simplify_succ | 10 : bv_wrap_simplify_db.
+
+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.
+Global Hint Resolve bv_wrap_simplify_pred | 10 : bv_wrap_simplify_db.
+
+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.
+Global Hint Resolve bv_wrap_simplify_opp | 10 : bv_wrap_simplify_db.
+
+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.
+Global Hint Resolve bv_wrap_simplify_add | 10 : bv_wrap_simplify_db.
+
+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.
+Global Hint Resolve bv_wrap_simplify_sub | 10 : bv_wrap_simplify_db.
+
+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.
+Global Hint Resolve bv_wrap_simplify_mul | 10 : bv_wrap_simplify_db.
+
+(** [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 | ]
+.
+
+(** [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.
+
+Ltac bv_wrap_simplify_solve :=
+  bv_wrap_simplify; f_equal; lia.
+
+
+(** * Lemmas about [bv n] operations *)
+
+(** ** Unfolding lemmas for the operations. *)
+Section unfolding.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+
+  Lemma bv_0_unsigned :
+    bv_unsigned (bv_0 n) = 0.
+  Proof. done. Qed.
+  Lemma bv_0_signed :
+    bv_signed (bv_0 n) = 0.
+  Proof. unfold bv_0. by rewrite bv_signed_BV, bv_swrap_0. Qed.
+
+  Lemma bv_succ_unsigned b :
+    bv_unsigned (bv_succ b) = bv_wrap n (Z.succ (bv_unsigned b)).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_pred_unsigned b :
+    bv_unsigned (bv_pred b) = bv_wrap n (Z.pred (bv_unsigned b)).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_add_unsigned b1 b2 :
+    bv_unsigned (b1 + b2) = bv_wrap n (bv_unsigned b1 + bv_unsigned b2).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_sub_unsigned b1 b2 :
+    bv_unsigned (b1 - b2) = bv_wrap n (bv_unsigned b1 - bv_unsigned b2).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_opp_unsigned b :
+    bv_unsigned (- b) = bv_wrap n (- bv_unsigned b).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_mul_unsigned b1 b2 :
+    bv_unsigned (b1 * b2) = bv_wrap n (bv_unsigned b1 * bv_unsigned b2).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_divu_unsigned b1 b2 :
+    bv_unsigned (b1 `divu` b2) = bv_unsigned b1 `div` bv_unsigned b2.
+  Proof. done. Qed.
+  Lemma bv_divu_signed b1 b2 :
+    bv_signed (b1 `divu` b2) = bv_swrap n (bv_unsigned b1 `div` bv_unsigned b2).
+  Proof. done. Qed.
+
+  Lemma bv_modu_unsigned b1 b2 :
+    bv_unsigned (b1 `modu` b2) = bv_unsigned b1 `mod` bv_unsigned b2.
+  Proof. done. Qed.
+  Lemma bv_modu_signed b1 b2 :
+    bv_signed (b1 `modu` b2) = bv_swrap n (bv_unsigned b1 `mod` bv_unsigned b2).
+  Proof. done. Qed.
+
+  Lemma bv_divs_unsigned b1 b2 :
+    bv_unsigned (b1 `divs` b2) = bv_wrap n (bv_signed b1 `div` bv_signed b2).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_quots_unsigned b1 b2 :
+    bv_unsigned (b1 `quots` b2) = bv_wrap n (bv_signed b1 `quot` bv_signed b2).
+  Proof. done. Qed.
+  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.
+
+  Lemma bv_mods_unsigned b1 b2 :
+    bv_unsigned (b1 `mods` b2) = bv_wrap n (bv_signed b1 `mod` bv_signed b2).
+  Proof. done. Qed.
+  Lemma bv_mods_signed b1 b2 :
+    bv_signed (b1 `mods` b2) = bv_swrap n (bv_signed b1 `mod` bv_signed b2).
+  Proof. unfold bv_mods. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_rems_unsigned b1 b2 :
+    bv_unsigned (b1 `rems` b2) = bv_wrap n (bv_signed b1 `rem` bv_signed b2).
+  Proof. done. Qed.
+  Lemma bv_rems_signed b1 b2 :
+    bv_signed (b1 `rems` b2) = bv_swrap n (bv_signed b1 `rem` bv_signed b2).
+  Proof. unfold bv_rems. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_shiftl_unsigned b1 b2 :
+    bv_unsigned (b1 ≪ b2) = bv_wrap n (bv_unsigned b1 ≪ bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_shiftl_signed b1 b2 :
+    bv_signed (b1 ≪ b2) = bv_swrap n (bv_unsigned b1 ≪ bv_unsigned b2).
+  Proof. unfold bv_shiftl. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_shiftr_unsigned b1 b2 :
+    bv_unsigned (b1 ≫ b2) = bv_unsigned b1 ≫ bv_unsigned b2.
+  Proof. done. Qed.
+  Lemma bv_shiftr_signed b1 b2 :
+    bv_signed (b1 ≫ b2) = bv_swrap n (bv_unsigned b1 ≫ bv_unsigned b2).
+  Proof. done. Qed.
+
+  Lemma bv_ashiftr_unsigned b1 b2 :
+    bv_unsigned (b1 `ashiftr` b2) = bv_wrap n (bv_signed b1 ≫ bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_ashiftr_signed b1 b2 :
+    bv_signed (b1 `ashiftr` b2) = bv_swrap n (bv_signed b1 ≫ bv_unsigned b2).
+  Proof. unfold bv_ashiftr. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_or_unsigned b1 b2 :
+    bv_unsigned (bv_or b1 b2) = Z.lor (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_or_signed b1 b2 :
+    bv_signed (bv_or b1 b2) = bv_swrap n (Z.lor (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_and_unsigned b1 b2 :
+    bv_unsigned (bv_and b1 b2) = Z.land (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_and_signed b1 b2 :
+    bv_signed (bv_and b1 b2) = bv_swrap n (Z.land (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_xor_unsigned b1 b2 :
+    bv_unsigned (bv_xor b1 b2) = Z.lxor (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_xor_signed b1 b2 :
+    bv_signed (bv_xor b1 b2) = bv_swrap n (Z.lxor (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+
+  Lemma bv_not_unsigned b :
+    bv_unsigned (bv_not b) = bv_wrap n (Z.lnot (bv_unsigned b)).
+  Proof. done. Qed.
+  Lemma bv_not_signed b :
+    bv_signed (bv_not b) = bv_swrap n (Z.lnot (bv_unsigned b)).
+  Proof. unfold bv_not. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_zero_extend_unsigned' z b :
+    bv_unsigned (bv_zero_extend z b) = bv_wrap z (bv_unsigned b).
+  Proof. done. Qed.
+  (* [bv_zero_extend_unsigned] is the version that we want, but it
+  only holds with a precondition. *)
+  Lemma bv_zero_extend_unsigned z b :
+    (n ≤ z)%N →
+    bv_unsigned (bv_zero_extend z b) = bv_unsigned b.
+  Proof.
+    intros ?. rewrite bv_zero_extend_unsigned', bv_wrap_small; [done|].
+    bv_saturate. pose proof (bv_modulus_le_mono n z). lia.
+  Qed.
+  Lemma bv_zero_extend_signed z b :
+    bv_signed (bv_zero_extend z b) = bv_swrap z (bv_unsigned b).
+  Proof. unfold bv_zero_extend. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_sign_extend_unsigned z b :
+    bv_unsigned (bv_sign_extend z b) = bv_wrap z (bv_signed b).
+  Proof. done. Qed.
+  Lemma bv_sign_extend_signed' z b :
+    bv_signed (bv_sign_extend z b) = bv_swrap z (bv_signed b).
+  Proof. unfold bv_sign_extend. rewrite Z_to_bv_signed. done. Qed.
+  (* [bv_sign_extend_signed] is the version that we want, but it
+  only holds with a precondition. *)
+  Lemma bv_sign_extend_signed z b :
+    (n ≤ z)%N →
+    bv_signed (bv_sign_extend z b) = bv_signed b.
+  Proof.
+    intros ?. rewrite bv_sign_extend_signed'.
+    destruct (decide (n = 0%N)); subst.
+    { by rewrite bv_signed_N_0, bv_swrap_0. }
+    apply bv_swrap_small. bv_saturate.
+    pose proof bv_half_modulus_le_mono n z. lia.
+  Qed.
+
+  Lemma bv_extract_unsigned s l b :
+    bv_unsigned (bv_extract s l b) = bv_wrap l (bv_unsigned b ≫ Z.of_N s).
+  Proof. done. Qed.
+  Lemma bv_extract_signed s l b :
+    bv_signed (bv_extract s l b) = bv_swrap l (bv_unsigned b ≫ Z.of_N s).
+  Proof. unfold bv_extract. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_concat_unsigned' m  n2 b1 (b2 : bv n2) :
+    bv_unsigned (bv_concat m b1 b2) = bv_wrap m (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
+  Proof. done. Qed.
+  (* [bv_concat_unsigned] is the version that we want, but it
+  only holds with a precondition. *)
+  Lemma bv_concat_unsigned m n2 b1 (b2 : bv n2) :
+    (m = n + n2)%N →
+    bv_unsigned (bv_concat m b1 b2) = Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2).
+  Proof.
+    intros ->. rewrite bv_concat_unsigned', bv_wrap_small; [done|].
+    apply Z.bounded_iff_bits_nonneg'; [lia | |].
+    { apply Z.lor_nonneg. bv_saturate. split; [|lia]. apply Z.shiftl_nonneg. lia. }
+    intros k ?. rewrite Z.lor_spec, Z.shiftl_spec; [|lia].
+    apply orb_false_intro; (eapply Z.bounded_iff_bits_nonneg; [..|done]); bv_saturate; try lia.
+    - apply (Z.lt_le_trans _ (bv_modulus n)); [lia|]. apply Z.pow_le_mono_r; lia.
+    - apply (Z.lt_le_trans _ (bv_modulus n2)); [lia|]. apply Z.pow_le_mono_r; lia.
+  Qed.
+  Lemma bv_concat_signed m n2 b1 (b2 : bv n2) :
+    bv_signed (bv_concat m b1 b2) = bv_swrap m (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
+  Proof. unfold bv_concat. rewrite Z_to_bv_signed. done. Qed.
+
+  Lemma bv_add_Z_unsigned b z :
+    bv_unsigned (b `+Z` z) = bv_wrap n (bv_unsigned b + z).
+  Proof. done. Qed.
+  Lemma bv_add_Z_signed b z :
+    bv_signed (b `+Z` z) = bv_swrap n (bv_signed b + z).
+  Proof. unfold bv_add_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+
+  Lemma bv_sub_Z_unsigned b z :
+    bv_unsigned (b `-Z` z) = bv_wrap n (bv_unsigned b - z).
+  Proof. done. Qed.
+  Lemma bv_sub_Z_signed b z :
+    bv_signed (b `-Z` z) = bv_swrap n (bv_signed b - z).
+  Proof. unfold bv_sub_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+
+  Lemma bv_mul_Z_unsigned b z:
+    bv_unsigned (b `*Z` z) = bv_wrap n (bv_unsigned b * z).
+  Proof. done. Qed.
+  Lemma bv_mul_Z_signed b z :
+    bv_signed (b `*Z` z) = bv_swrap n (bv_signed b * z).
+  Proof. unfold bv_mul_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+End unfolding.
+
+(** ** Properties of bv operations *)
+Section properties.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+  Local Open Scope bv_scope.
+
+  Lemma bv_sub_add_opp b1 b2:
+    b1 - b2 = b1 + - b2.
+  Proof.
+    apply bv_eq. unfold bv_sub, bv_add, bv_opp. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+
+  Global Instance bv_add_assoc : Assoc (=) (@bv_add n).
+  Proof.
+    intros ???. unfold bv_add. apply bv_eq. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+
+  Global Instance bv_mul_assoc : Assoc (=) (@bv_mul n).
+  Proof.
+    intros ???. unfold bv_mul. apply bv_eq. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+
+  Lemma bv_add_0_l b1 b2 :
+    bv_unsigned b1 = 0 →
+    b1 + b2 = b2.
+  Proof.
+    intros Hb. apply bv_eq.
+    rewrite bv_add_unsigned, Hb, Z.add_0_l, bv_wrap_small; [done|apply bv_unsigned_in_range].
+  Qed.
+
+  Lemma bv_add_0_r b1 b2 :
+    bv_unsigned b2 = 0 →
+    b1 + b2 = b1.
+  Proof.
+    intros Hb. apply bv_eq.
+    rewrite bv_add_unsigned, Hb, Z.add_0_r, bv_wrap_small; [done|apply bv_unsigned_in_range].
+  Qed.
+
+  Lemma bv_add_Z_0 b : b `+Z` 0 = b.
+  Proof.
+    unfold bv_add_Z. rewrite Z.add_0_r.
+    apply bv_eq. apply Z_to_bv_small. apply bv_unsigned_in_range.
+  Qed.
+
+  Lemma bv_add_Z_add_r b m o:
+    b `+Z` (m + o) = (b `+Z` o) `+Z` m.
+  Proof.
+    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
+     bv_wrap_simplify_solve.
+  Qed.
+
+  Lemma bv_add_Z_add_l b m o:
+    b `+Z` (m + o) = (b `+Z` m) `+Z` o.
+  Proof.
+    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
+     bv_wrap_simplify_solve.
+  Qed.
+
+  Lemma bv_add_Z_succ b m:
+    b `+Z` Z.succ m = (b `+Z` 1) `+Z` m.
+  Proof.
+    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+
+  Lemma bv_add_Z_inj_l b i j:
+    0 ≤ i < bv_modulus n →
+    0 ≤ j < bv_modulus n →
+    b `+Z` i = b `+Z` j ↔ i = j.
+  Proof.
+    intros ??. split; [|naive_solver].
+    intros Heq%bv_eq. rewrite !bv_add_Z_unsigned, !(Z.add_comm (bv_unsigned _)) in Heq.
+    by rewrite <-bv_wrap_add_inj, !bv_wrap_small in Heq.
+  Qed.
+
+  Lemma bv_opp_not b:
+    - b `-Z` 1 = bv_not b.
+  Proof.
+    apply bv_eq.
+    rewrite bv_not_unsigned, bv_sub_Z_unsigned, bv_opp_unsigned, <-Z.opp_lnot.
+    bv_wrap_simplify_solve.
+  Qed.
+
+  Lemma bv_and_comm b1 b2:
+    bv_and b1 b2 = bv_and b2 b1.
+  Proof. apply bv_eq. by rewrite !bv_and_unsigned, Z.land_comm. Qed.
+
+  Lemma bv_or_comm b1 b2:
+    bv_or b1 b2 = bv_or b2 b1.
+  Proof. apply bv_eq. by rewrite !bv_or_unsigned, Z.lor_comm. Qed.
+
+  Lemma bv_or_0_l b1 b2 :
+    bv_unsigned b1 = 0 →
+    bv_or b1 b2 = b2.
+  Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_l. Qed.
+
+  Lemma bv_or_0_r b1 b2 :
+    bv_unsigned b2 = 0 →
+    bv_or b1 b2 = b1.
+  Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_r. Qed.
+
+  Lemma bv_extract_0_unsigned l b:
+    bv_unsigned (bv_extract 0 l b) = bv_wrap l (bv_unsigned b).
+  Proof. rewrite bv_extract_unsigned, Z.shiftr_0_r. done. Qed.
+
+  Lemma bv_extract_0_bv_add_distr l b1 b2:
+    (l ≤ n)%N →
+    bv_extract 0 l (bv_add b1 b2) = bv_add (bv_extract 0 l b1) (bv_extract 0 l b2).
+  Proof.
+    intros ?.
+    apply bv_eq. rewrite !bv_extract_0_unsigned, !bv_add_unsigned, !bv_extract_0_unsigned.
+    rewrite bv_wrap_bv_wrap by done.
+    bv_wrap_simplify_solve.
+  Qed.
+
+  Lemma bv_concat_0 m n2 b1 (b2 : bv n2) :
+    bv_unsigned b1 = 0 →
+    bv_concat m b1 b2 = bv_zero_extend m b2.
+  Proof.
+    intros Hb1. apply bv_eq.
+    by rewrite bv_zero_extend_unsigned', bv_concat_unsigned', Hb1, Z.shiftl_0_l, Z.lor_0_l.
+  Qed.
+
+  Lemma bv_zero_extend_idemp b:
+    bv_zero_extend n b = b.
+  Proof. apply bv_eq. by rewrite bv_zero_extend_unsigned. Qed.
+
+  Lemma bv_sign_extend_idemp b:
+    bv_sign_extend n b = b.
+  Proof. apply bv_eq_signed. by rewrite bv_sign_extend_signed. Qed.
+End properties.
+
+(** ** Lemmas about [bv_to_little] and [bv_of_little] *)
+Section little.
+
+  Lemma bv_to_litte_endian_unsigned m n z:
+    0 ≤ m →
+    bv_unsigned <$> bv_to_little_endian m n z = Z_to_little_endian m (Z.of_N n) z.
+  Proof.
+    intros ?. apply list_eq. intros i. unfold bv_to_little_endian.
+    rewrite list_lookup_fmap, list_lookup_fmap.
+    destruct (Z_to_little_endian m (Z.of_N n) z !! i) eqn: Heq; [simpl |done].
+    rewrite Z_to_bv_small; [done|].
+    eapply (Forall_forall (λ z, _ ≤ z < _)); [ |by eapply elem_of_list_lookup_2].
+    eapply Z_to_little_endian_bound; lia.
+  Qed.
+
+  Lemma bv_to_little_endian_to_bv m n bs:
+    m = Z.of_nat (length bs) →
+    bv_to_little_endian m n (little_endian_to_bv n bs) = bs.
+  Proof.
+    intros ->. eapply (fmap_inj bv_unsigned). { intros ???. by apply bv_eq. }
+    rewrite bv_to_litte_endian_unsigned; [|lia].
+    apply Z_to_little_endian_to_Z; [by rewrite fmap_length | lia |].
+    apply Forall_forall. intros ? [?[->?]]%elem_of_list_fmap_2. apply bv_unsigned_in_range.
+  Qed.
+
+  Lemma little_endian_to_bv_to_little_endian m n z:
+    0 ≤ m →
+    little_endian_to_bv n (bv_to_little_endian m n z) = z `mod` 2 ^ (m * Z.of_N n).
+  Proof.
+    intros ?. unfold little_endian_to_bv.
+    rewrite bv_to_litte_endian_unsigned; [|lia].
+    apply little_endian_to_Z_to_little_endian; lia.
+  Qed.
+
+  Lemma bv_to_little_endian_length m n z :
+    0 ≤ m →
+    length (bv_to_little_endian m n z) = Z.to_nat m.
+  Proof.
+    intros ?. unfold bv_to_little_endian. rewrite fmap_length.
+    apply Nat2Z.inj. rewrite Z_to_little_endian_length, ?Z2Nat.id; try lia.
+  Qed.
+
+  Lemma little_endian_to_bv_bound n bs :
+    0 ≤ little_endian_to_bv n bs < 2 ^ (Z.of_nat (length bs) * Z.of_N n).
+  Proof.
+    unfold little_endian_to_bv. rewrite <-(fmap_length bv_unsigned bs).
+    apply little_endian_to_Z_bound; [lia|].
+    apply Forall_forall. intros ? [? [-> ?]]%elem_of_list_fmap.
+    apply bv_unsigned_in_range.
+  Qed.
+
+  Lemma Z_to_bv_little_endian_to_bv_to_little_endian x m n (b : bv x):
+    0 ≤ m →
+    x = (Z.to_N m * n)%N →
+    Z_to_bv x (little_endian_to_bv n (bv_to_little_endian m n (bv_unsigned b))) = b.
+  Proof.
+    intros ? ->. rewrite little_endian_to_bv_to_little_endian, Z.mod_small; [| |lia].
+    - apply bv_eq. rewrite Z_to_bv_small; [done|]. apply bv_unsigned_in_range.
+    - pose proof bv_unsigned_in_range _ b as Hr. unfold bv_modulus in Hr.
+      by rewrite N2Z.inj_mul, Z2N.id in Hr.
+  Qed.
+
+  Lemma bv_to_little_endian_lookup_Some m n z (i : nat) x:
+    0 ≤ m → bv_to_little_endian m n z !! i = Some x ↔
+      Z.of_nat i < m ∧ x = Z_to_bv n (z ≫ (Z.of_nat i * Z.of_N n)).
+  Proof.
+    unfold bv_to_little_endian. intros Hm. rewrite list_lookup_fmap, fmap_Some.
+    split.
+    - intros [?[[??]%Z_to_little_endian_lookup_Some ?]]; [|lia..]; subst. split; [done|].
+      rewrite <-bv_wrap_land. apply bv_eq. by rewrite !Z_to_bv_unsigned, bv_wrap_bv_wrap.
+    - intros [?->]. eexists _. split; [apply Z_to_little_endian_lookup_Some; try done; lia| ].
+      rewrite <-bv_wrap_land. apply bv_eq. by rewrite !Z_to_bv_unsigned, bv_wrap_bv_wrap.
+  Qed.
+
+  Lemma little_endian_to_bv_spec n bs i b:
+    0 ≤ i → n ≠ 0%N →
+    bs !! Z.to_nat (i `div` Z.of_N n) = Some b →
+    Z.testbit (little_endian_to_bv n bs) i = Z.testbit (bv_unsigned b) (i `mod` Z.of_N n).
+  Proof.
+    intros ???. unfold little_endian_to_bv. apply little_endian_to_Z_spec; [lia|lia| |].
+    { apply Forall_fmap. apply Forall_true. intros ?; simpl. apply bv_unsigned_in_range. }
+    rewrite list_lookup_fmap. apply fmap_Some. naive_solver.
+  Qed.
+End little.
+
+(** ** Lemmas about [bv_seq] *)
+Section bv_seq.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+
+  Lemma bv_seq_length b len:
+    length (bv_seq b len) = Z.to_nat len.
+  Proof. unfold bv_seq. by rewrite fmap_length, seqZ_length. Qed.
+
+  Lemma bv_seq_succ b m:
+    0 ≤ m →
+    bv_seq b (Z.succ m) = b :: bv_seq (b `+Z` 1) m.
+  Proof.
+    intros. unfold bv_seq. rewrite seqZ_cons by lia. csimpl.
+    rewrite bv_add_Z_0. f_equal.
+    assert (Z.succ 0 = 1 + 0) as -> by lia.
+    rewrite <-fmap_add_seqZ, <-list_fmap_compose, Z.pred_succ. apply list_fmap_ext.
+    intros i x. simpl. by rewrite bv_add_Z_add_l.
+  Qed.
+
+  Lemma NoDup_bv_seq b z:
+    0 ≤ z ≤ bv_modulus n →
+    NoDup (bv_seq b z).
+  Proof.
+    intros ?. apply NoDup_alt. intros i j b'. unfold bv_seq. rewrite !list_lookup_fmap.
+    intros [?[[??]%lookup_seqZ ?]]%fmap_Some ; simplify_eq.
+    intros [?[[->?]%lookup_seqZ ?%bv_add_Z_inj_l]]%fmap_Some; lia.
+  Qed.
+End bv_seq.
+
+(** ** Lemmas about [bv] and [bool] *)
+Section bv_bool.
+  Implicit Types (b : bool).
+
+  Lemma bool_to_bv_unsigned n b:
+    n ≠ 0%N →
+    bv_unsigned (bool_to_bv n b) = bool_to_Z b.
+  Proof.
+    intros ?. pose proof (bv_modulus_gt_1 n).
+    apply Z_to_bv_small. destruct b; simpl; lia.
+  Qed.
+
+  Lemma bv_extract_bool_to_bv n n2 b:
+    n ≠ 0%N → n2 ≠ 0%N →
+    bv_extract 0 n (bool_to_bv n2 b) = bool_to_bv n b.
+  Proof.
+    intros ??. apply bv_eq. pose proof (bv_modulus_gt_1 n).
+    rewrite bv_extract_unsigned, !bool_to_bv_unsigned, Z.shiftr_0_r by done.
+    rewrite bv_wrap_small; [done|]. destruct b; simpl; lia.
+  Qed.
+
+  Lemma bv_not_bool_to_bv b:
+    bv_not (bool_to_bv 1 b) = bool_to_bv 1 (negb b).
+  Proof. apply bv_eq. by destruct b. Qed.
+
+  Lemma bool_decide_bool_to_bv_0 b:
+    bool_decide (bv_unsigned (bool_to_bv 1 b) = 0) = negb b.
+  Proof. by destruct b. Qed.
+  Lemma bool_decide_bool_to_bv_1 b:
+    bool_decide (bv_unsigned (bool_to_bv 1 b) = 1) = b.
+  Proof. by destruct b. Qed.
+End bv_bool.
+
+Section bv_bits.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+
+  Lemma bv_to_bits_length b : length (bv_to_bits b) = N.to_nat n.
+  Proof. unfold bv_to_bits. rewrite fmap_length, seqZ_length, <-Z_N_nat, N2Z.id. done. Qed.
+
+  Lemma bv_to_bits_lookup_Some b i x:
+    bv_to_bits b !! i = Some x ↔ (i < N.to_nat n)%nat ∧ x = Z.testbit (bv_unsigned b) (Z.of_nat i).
+  Proof.
+    unfold bv_to_bits. rewrite list_lookup_fmap, fmap_Some.
+    split.
+    - intros [?[?%lookup_seqZ?]]. naive_solver lia.
+    - intros [??]. eexists _. split; [|done]. apply lookup_seqZ. lia.
+  Qed.
+
+  Global Instance bv_to_bits_inj : Inj eq eq (@bv_to_bits n).
+  Proof.
+    unfold bv_to_bits. intros x y Hf.
+    apply bv_eq_wrap. apply Z.bits_inj_iff'. intros i Hi.
+    rewrite !bv_wrap_spec; [|lia..]. case_bool_decide; simpl; [|done].
+    eapply list_fmap_inj_1 in Hf; [done|]. apply elem_of_seqZ. lia.
+  Qed.
+End bv_bits.
+
+
+(** * [bvn] *)
+Record bvn := bv_to_bvn {
+  bvn_n : N;
+  bvn_val : bv bvn_n;
+}.
+Global Arguments bv_to_bvn {_} _.
+Add Printing Constructor bvn.
+
+Definition bvn_unsigned (b : bvn) := bv_unsigned (b.(bvn_val)).
+
+Lemma bvn_eq (b1 b2 : bvn) :
+  b1 = b2 ↔ b1.(bvn_n) = b2.(bvn_n) ∧ bvn_unsigned b1 = bvn_unsigned b2.
+Proof. split; [ naive_solver|]. destruct b1, b2; simpl; intros [??]. subst. f_equal. by apply bv_eq. Qed.
+
+Global Program Instance bvn_eq_dec : EqDecision bvn := λ '(@bv_to_bvn n1 b1) '(@bv_to_bvn n2 b2),
+   cast_if_and (decide (n1 = n2)) (decide (bv_unsigned b1 = bv_unsigned b2)).
+(* TODO: The following does not compute to eq_refl*)
+Next Obligation. intros. apply bvn_eq. naive_solver. Qed.
+Next Obligation. intros. intros ?%bvn_eq. naive_solver. Qed.
+Next Obligation. intros. intros ?%bvn_eq. naive_solver. Qed.
+
+Definition bvn_to_bv (n : N) (b : bvn) : option (bv n) :=
+  match decide (b.(bvn_n) = n) with
+  | left eq => Some (eq_rect (bvn_n b) (λ n0 : N, bv n0) (bvn_val b) n eq)
+  | right _ => None
+  end.
+Global Arguments bvn_to_bv !_ !_ /.
+
+Global Coercion bv_to_bvn : bv >-> bvn.
+
+(** * Opaqueness *)
+(** We mark all functions on bitvectors as opaque. *)
+Global Hint Opaque Z_to_bv
+       bv_0 bv_succ bv_pred
+       bv_add bv_sub bv_opp
+       bv_mul bv_divu bv_modu
+       bv_divs bv_quots bv_mods bv_rems
+       bv_shiftl bv_shiftr bv_ashiftr bv_or
+       bv_and bv_xor bv_not bv_zero_extend
+       bv_sign_extend bv_extract bv_concat
+       bv_add_Z bv_sub_Z bv_mul_Z
+       bool_to_bv bv_to_bits : typeclass_instances.
+Global Opaque Z_to_bv
+       bv_0 bv_succ bv_pred
+       bv_add bv_sub bv_opp
+       bv_mul bv_divu bv_modu
+       bv_divs bv_quots bv_mods bv_rems
+       bv_shiftl bv_shiftr bv_ashiftr bv_or
+       bv_and bv_xor bv_not bv_zero_extend
+       bv_sign_extend bv_extract bv_concat
+       bv_add_Z bv_sub_Z bv_mul_Z
+       bool_to_bv bv_to_bits.
diff --git a/stdpp_unstable/bitvector_tactics.v b/stdpp_unstable/bitvector_tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..4efcc067358d322782a56282664b563a3938c40e
--- /dev/null
+++ b/stdpp_unstable/bitvector_tactics.v
@@ -0,0 +1,521 @@
+(** This file is still experimental. See its tracking issue
+https://gitlab.mpi-sws.org/iris/stdpp/-/issues/146 for details on remaining
+issues before stabilization. This file is maintained by Michael Sammler. *)
+From stdpp.unstable Require Export bitvector.
+From stdpp.unstable Require Import bitblast.
+From stdpp Require Import options.
+
+(** * bitvector tactics *)
+(** This file provides tactics for the bitvector library in
+[bitvector.v]. In particular, it provides integration of bitvectors
+with the [bitblast] tactic and tactics for simplifying and solving
+bitvector expressions. The main tactic provided by this library is
+[bv_simplify] which performs the following steps:
+
+1. Simplify the goal by rewriting with the [bv_simplify] database.
+2. If the goal is an (in)equality (= or ≠) between bitvectors, turn it into
+an (in)equality between their unsigned values. (Using unsigned values here
+rather than signed is somewhat arbitrary but works well enough in practice.)
+3. Unfold [bv_unsigned] and [bv_signed] of operations on [bv n] to
+operations on [Z].
+4. Simplify the goal by rewriting with the [bv_unfolded_simplify]
+database.
+
+This file provides the following variants of the [bv_simplify] tactic:
+- [bv_simplify] applies the simplification procedure to the goal.
+- [bv_simplify H] applies the simplification procedure to the hypothesis [H].
+- [bv_simplify select pat] applies the simplification procedure to the hypothesis
+  matching [pat].
+
+- [bv_simplify_arith] applies the simplification procedure to the goal and
+  additionally rewrites with the [bv_unfolded_to_arith] database to turn the goal
+  into a more suitable shape for calling [lia].
+- [bv_simplify_arith H] same as [bv_simplify_arith], but in the hypothesis [H].
+- [bv_simplify_arith select pat] same as [bv_simplify_arith], but in the
+  hypothesis matching [pat].
+
+- [bv_solve] simplifies the goal using [bv_simplify_arith], learns bounds facts
+  about bitvector variables in the context and tries to solve the goal using [lia].
+
+This automation assumes that [lia] can handle [`mod`] and [`div`] as can be enabled
+via the one of the following flags:
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+or
+Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
+or
+Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).
+See https://coq.github.io/doc/master/refman/addendum/micromega.html#coq:tacn.zify
+for details.
+*)
+
+(** * Settings *)
+Local Open Scope Z_scope.
+
+(** * General tactics *)
+Ltac unfold_lets_in_context :=
+  repeat match goal with
+         | H := _ |- _ => unfold H in *; clear H
+         end.
+
+Tactic Notation "reduce_closed" constr(x) :=
+  is_closed_term x;
+  let r := eval vm_compute in x in
+  change_no_check x with r in *
+.
+
+(** * bitblast instances *)
+Lemma bitblast_bool_to_Z b n:
+  Bitblast (bool_to_Z b) n (bool_decide (n = 0) && b).
+Proof.
+  constructor. destruct b; simpl_bool; repeat case_bool_decide;
+    subst; try done; rewrite ?Z.bits_0; by destruct n.
+Qed.
+Global Hint Resolve bitblast_bool_to_Z | 10 : bitblast.
+
+Lemma bitblast_bounded_bv_unsigned n (b : bv n):
+  BitblastBounded (bv_unsigned b) (Z.of_N n).
+Proof. constructor. apply bv_unsigned_in_range. Qed.
+Global Hint Resolve bitblast_bounded_bv_unsigned | 15 : bitblast.
+
+Lemma bitblast_bv_wrap z1 n n1 b1:
+  Bitblast z1 n b1 →
+  Bitblast (bv_wrap n1 z1) n (bool_decide (n < Z.of_N n1) && b1).
+Proof.
+  intros [<-]. constructor.
+  destruct (decide (0 ≤ n)); [by rewrite bv_wrap_spec| rewrite !Z.testbit_neg_r; [|lia..]; btauto].
+Qed.
+Global Hint Resolve bitblast_bv_wrap | 10 : bitblast.
+
+(* The following two lemmas are proven using [bitblast]. *)
+Lemma bv_extract_concat_later m n1 n2 s l (b1 : bv n1) (b2 : bv n2):
+  (n2 ≤ s)%N →
+  (m = n1 + n2)%N →
+  bv_extract s l (bv_concat m b1 b2) = bv_extract (s - n2) l b1.
+Proof.
+  intros ? ->. apply bv_eq.
+  rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
+  bitblast. f_equal. lia.
+Qed.
+Lemma bv_extract_concat_here m n1 n2 s (b1 : bv n1) (b2 : bv n2):
+  s = 0%N →
+  (m = n1 + n2)%N →
+  bv_extract s n2 (bv_concat m b1 b2) = b2.
+Proof.
+  intros -> ->. apply bv_eq.
+  rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
+  bitblast. f_equal. lia.
+Qed.
+
+(** * [bv_simplify] rewrite database *)
+(** The [bv_simplify] database collects rewrite rules that rewrite
+bitvectors into other bitvectors. *)
+Create HintDb bv_simplify discriminated. (* Technically not necessary for rewrite db. *)
+Hint Rewrite @bv_concat_0 using done : bv_simplify.
+Hint Rewrite @bv_extract_concat_later @bv_extract_concat_here using lia : bv_simplify.
+Hint Rewrite @bv_extract_bool_to_bv using lia : bv_simplify.
+Hint Rewrite @bv_not_bool_to_bv : bv_simplify.
+Hint Rewrite bool_decide_bool_to_bv_0 bool_decide_bool_to_bv_1 : bv_simplify.
+
+(** * [bv_unfold] *)
+Create HintDb bv_unfold_db discriminated.
+Global Hint Constants Opaque : bv_unfold_db.
+Global Hint Variables Opaque : bv_unfold_db.
+Global Hint Extern 1 (TCFastDone ?P) => (change P; fast_done) : bv_unfold_db.
+Global Hint Transparent BvWf andb Is_true Z.ltb Z.leb Z.compare Pos.compare
+  Pos.compare_cont bv_modulus Z.pow Z.pow_pos Pos.iter Z.mul Pos.mul Z.of_N
+  : bv_unfold_db.
+
+Notation bv_suwrap signed := (if signed then bv_swrap else bv_wrap).
+
+Class BvUnfold (n : N) (signed : bool) (wrapped : bool) (b : bv n) (z : Z) := {
+    bv_unfold_proof : ((if signed then bv_signed else bv_unsigned) b) =
+                        (if wrapped then bv_suwrap signed n z else z);
+}.
+Global Arguments bv_unfold_proof {_ _ _} _ _ {_}.
+Global Hint Mode BvUnfold + + + + - : bv_unfold_db.
+
+(** [BV_UNFOLD_BLOCK] is a marker that this occurence of [bv_signed]
+or [bv_unsigned] has already been simplified. *)
+Definition BV_UNFOLD_BLOCK {A} (x : A) : A := x.
+
+Lemma bv_unfold_end s w n b :
+  BvUnfold n s w b ((if s then BV_UNFOLD_BLOCK bv_signed else BV_UNFOLD_BLOCK bv_unsigned) b).
+Proof.
+  constructor. unfold BV_UNFOLD_BLOCK.
+  destruct w, s; by rewrite ?bv_wrap_bv_unsigned, ?bv_swrap_bv_signed.
+Qed.
+Global Hint Resolve bv_unfold_end | 1000 : bv_unfold_db.
+Lemma bv_unfold_BV s w n z Hwf :
+  BvUnfold n s w (@BV _ z Hwf) (if w then z else if s then bv_swrap n z else z).
+Proof.
+  constructor. unfold bv_unsigned.
+  destruct w, s; simpl; try done; by rewrite bv_wrap_small by by apply bv_wf_in_range.
+Qed.
+Global Hint Resolve bv_unfold_BV | 10 : bv_unfold_db.
+Lemma bv_unfold_bv_0 s w n :
+  BvUnfold n s w (bv_0 n) 0.
+Proof. constructor. destruct w, s; rewrite ?bv_0_signed, ?bv_0_unsigned, ?bv_swrap_0; done. Qed.
+Global Hint Resolve bv_unfold_bv_0 | 10 : bv_unfold_db.
+Lemma bv_unfold_Z_to_bv s w n z :
+  BvUnfold n s w (Z_to_bv _ z) (if w then z else bv_suwrap s n z).
+Proof. constructor. destruct w, s; rewrite ?Z_to_bv_signed, ?Z_to_bv_unsigned; done. Qed.
+Global Hint Resolve bv_unfold_Z_to_bv | 10 : bv_unfold_db.
+Lemma bv_unfold_succ s w n b z :
+  BvUnfold n s true b z →
+  BvUnfold n s w (bv_succ b) (if w then Z.succ z else bv_suwrap s n (Z.succ z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_succ_signed, ?bv_succ_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_succ | 10 : bv_unfold_db.
+Lemma bv_unfold_pred s w n b z :
+  BvUnfold n s true b z →
+  BvUnfold n s w (bv_pred b) (if w then Z.pred z else bv_suwrap s n (Z.pred z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_pred_signed, ?bv_pred_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_pred | 10 : bv_unfold_db.
+Lemma bv_unfold_add s w n b1 b2 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s true b2 z2 →
+  BvUnfold n s w (bv_add b1 b2) (if w then z1 + z2 else bv_suwrap s n (z1 + z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_add_signed, ?bv_add_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_add | 10 : bv_unfold_db.
+Lemma bv_unfold_sub s w n b1 b2 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s true b2 z2 →
+  BvUnfold n s w (bv_sub b1 b2) (if w then z1 - z2 else bv_suwrap s n (z1 - z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_sub_signed, ?bv_sub_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_sub | 10 : bv_unfold_db.
+Lemma bv_unfold_opp s w n b z :
+  BvUnfold n s true b z →
+  BvUnfold n s w (bv_opp b) (if w then - z else bv_suwrap s n (- z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_opp_signed, ?bv_opp_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_opp | 10 : bv_unfold_db.
+Lemma bv_unfold_mul s w n b1 b2 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s true b2 z2 →
+  BvUnfold n s w (bv_mul b1 b2) (if w then z1 * z2 else bv_suwrap s n (z1 * z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_mul_signed, ?bv_mul_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_mul | 10 : bv_unfold_db.
+Lemma bv_unfold_divu s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_divu b1 b2) (if w then z1 `div` z2 else if s then bv_swrap n (z1 `div` z2) else z1 `div` z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_divu_signed, ?bv_divu_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_divu b1 b2)) as Hr. rewrite bv_divu_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_divu | 10 : bv_unfold_db.
+Lemma bv_unfold_modu s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_modu b1 b2) (if w then z1 `mod` z2 else if s then bv_swrap n (z1 `mod` z2) else z1 `mod` z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_modu_signed, ?bv_modu_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_modu b1 b2)) as Hr. rewrite bv_modu_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_modu | 10 : bv_unfold_db.
+Lemma bv_unfold_divs s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_divs b1 b2) (if w then z1 `div` z2 else bv_suwrap s n (z1 `div` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_divs_signed, ?bv_divs_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_divs | 10 : bv_unfold_db.
+Lemma bv_unfold_quots s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_quots b1 b2) (if w then z1 `quot` z2 else bv_suwrap s n (z1 `quot` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_quots_signed, ?bv_quots_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_quots | 10 : bv_unfold_db.
+Lemma bv_unfold_mods s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_mods b1 b2) (if w then z1 `mod` z2 else bv_suwrap s n (z1 `mod` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_mods_signed, ?bv_mods_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_mods | 10 : bv_unfold_db.
+Lemma bv_unfold_rems s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_rems b1 b2) (if w then z1 `rem` z2 else bv_suwrap s n (z1 `rem` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_rems_signed, ?bv_rems_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_rems | 10 : bv_unfold_db.
+Lemma bv_unfold_shiftl s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_shiftl b1 b2) (if w then z1 ≪ z2 else bv_suwrap s n (z1 ≪ z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_shiftl_signed, ?bv_shiftl_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_shiftl | 10 : bv_unfold_db.
+Lemma bv_unfold_shiftr s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_shiftr b1 b2) (if w then z1 ≫ z2 else if s then bv_swrap n (z1 ≫ z2) else (z1 ≫ z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_shiftr_signed, ?bv_shiftr_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_shiftr b1 b2)) as Hr. rewrite bv_shiftr_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_shiftr | 10 : bv_unfold_db.
+Lemma bv_unfold_ashiftr s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_ashiftr b1 b2) (if w then z1 ≫ z2 else bv_suwrap s n (z1 ≫ z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_ashiftr_signed, ?bv_ashiftr_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_ashiftr | 10 : bv_unfold_db.
+Lemma bv_unfold_or s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_or b1 b2) (if w then Z.lor z1 z2 else if s then bv_swrap n (Z.lor z1 z2) else Z.lor z1 z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_or_signed, ?bv_or_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_or b1 b2)) as Hr. rewrite bv_or_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_or | 10 : bv_unfold_db.
+Lemma bv_unfold_and s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_and b1 b2) (if w then Z.land z1 z2 else if s then bv_swrap n (Z.land z1 z2) else Z.land z1 z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_and_signed, ?bv_and_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_and b1 b2)) as Hr. rewrite bv_and_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_and | 10 : bv_unfold_db.
+Lemma bv_unfold_xor s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_xor b1 b2) (if w then Z.lxor z1 z2 else if s then bv_swrap n (Z.lxor z1 z2) else Z.lxor z1 z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_xor_signed, ?bv_xor_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_xor b1 b2)) as Hr. rewrite bv_xor_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_xor | 10 : bv_unfold_db.
+Lemma bv_unfold_not s w n b z :
+  BvUnfold n false false b z →
+  BvUnfold n s w (bv_not b) (if w then Z.lnot z else bv_suwrap s n (Z.lnot z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_not_signed, ?bv_not_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_not | 10 : bv_unfold_db.
+Lemma bv_unfold_zero_extend s w n n' b z `{!TCFastDone (n' <=? n = true)%N} :
+  BvUnfold n' false false b z →
+  BvUnfold n s w (bv_zero_extend n b) (if w then z else if s then bv_swrap n z else z).
+Proof.
+  intros [Hz]. constructor. unfold TCFastDone in *. rewrite ->?N.leb_le in *.
+  destruct w, s; rewrite ?bv_zero_extend_signed, ?bv_zero_extend_unsigned, ?Hz by done;
+    try bv_wrap_simplify_solve.
+  - rewrite <-Hz, bv_wrap_small; [done|]. bv_saturate. pose proof (bv_modulus_le_mono n' n). lia.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_zero_extend | 10 : bv_unfold_db.
+Lemma bv_unfold_sign_extend s w n n' b z `{!TCFastDone (n' <=? n = true)%N} :
+  BvUnfold n' true false b z →
+  BvUnfold n s w (bv_sign_extend n b) (if w then z else if s then z else bv_wrap n z).
+Proof.
+  intros [Hz]. constructor. unfold TCFastDone in *. rewrite ->?N.leb_le in *.
+  destruct w, s; rewrite ?bv_sign_extend_signed, ?bv_sign_extend_unsigned, ?Hz by done;
+    try bv_wrap_simplify_solve.
+  - subst. rewrite <-(bv_sign_extend_signed n) at 2 by done. by rewrite bv_swrap_bv_signed, bv_sign_extend_signed.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_sign_extend | 10 : bv_unfold_db.
+Lemma bv_unfold_extract s w n n' n1 b z :
+  BvUnfold n' false false b z →
+  BvUnfold n s w (bv_extract n1 n b) (if w then z ≫ Z.of_N n1 else bv_suwrap s n (z ≫ Z.of_N n1)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_extract_signed, ?bv_extract_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_extract | 10 : bv_unfold_db.
+Lemma bv_unfold_concat s w n n1 n2 b1 b2 z1 z2 `{!TCFastDone (n = n1 + n2)%N} :
+  BvUnfold n1 false false b1 z1 →
+  BvUnfold n2 false false b2 z2 →
+  BvUnfold n s w (bv_concat n b1 b2) (if w then Z.lor (z1 ≪ Z.of_N n2) z2 else if s then  bv_swrap n (Z.lor (z1 ≪ Z.of_N n2) z2) else Z.lor (z1 ≪ Z.of_N n2) z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor. unfold TCFastDone in *.
+  destruct w, s; rewrite ?bv_concat_signed, ?bv_concat_unsigned, ?Hz1, ?Hz2 by done;
+    try bv_wrap_simplify_solve.
+  - subst. rewrite <-(bv_concat_unsigned (n1 + n2)) at 2 by done.
+    by rewrite bv_wrap_bv_unsigned, bv_concat_unsigned.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_concat | 10 : bv_unfold_db.
+Lemma bv_unfold_add_Z s w n b1 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s w (bv_add_Z b1 z2) (if w then z1 + z2 else bv_suwrap s n (z1 + z2)).
+Proof.
+  intros [Hz1]. constructor.
+  destruct w, s; rewrite ?bv_add_Z_signed, ?bv_add_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_add_Z | 10 : bv_unfold_db.
+Lemma bv_unfold_sub_Z s w n b1 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s w (bv_sub_Z b1 z2) (if w then z1 - z2 else bv_suwrap s n (z1 - z2)).
+Proof.
+  intros [Hz1]. constructor.
+  destruct w, s; rewrite ?bv_sub_Z_signed, ?bv_sub_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_sub_Z | 10 : bv_unfold_db.
+Lemma bv_unfold_mul_Z s w n b1 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s w (bv_mul_Z b1 z2) (if w then z1 * z2 else bv_suwrap s n (z1 * z2)).
+Proof.
+  intros [Hz1]. constructor.
+  destruct w, s; rewrite ?bv_mul_Z_signed, ?bv_mul_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_mul_Z | 10 : bv_unfold_db.
+
+Ltac bv_unfold_eq :=
+  lazymatch goal with
+  | |- @bv_unsigned ?n ?b = ?z =>
+      simple notypeclasses refine (@bv_unfold_proof n false false b z _)
+  | |- @bv_signed ?n ?b = ?z =>
+      simple notypeclasses refine (@bv_unfold_proof n true false b z _)
+  end;
+  typeclasses eauto with bv_unfold_db.
+Ltac bv_unfold :=
+  repeat (match goal with
+            (* TODO: Detect if there is a bv_wrap around the
+            bv_unsigned (like after applying bv_eq_wrapped) *)
+          | |- context [@bv_unsigned ?n ?b] =>
+              pattern (@bv_unsigned n b);
+              simple refine (eq_rec_r _ _ _); [shelve| |bv_unfold_eq]; cbn beta
+          | |- context [@bv_signed ?n ?b] =>
+              pattern (@bv_signed n b);
+              simple refine (eq_rec_r _ _ _); [shelve| |bv_unfold_eq]; cbn beta
+          end); unfold BV_UNFOLD_BLOCK.
+
+(** * [bv_unfolded_simplify] rewrite database *)
+(** The [bv_unfolded_simplify] database collects rewrite rules that
+should be used to simplify the goal after Z is bv_unfolded. *)
+Create HintDb bv_unfolded_simplify discriminated. (* Technically not necessary for rewrite db. *)
+Hint Rewrite Z.shiftr_0_r Z.lor_0_r Z.lor_0_l : bv_unfolded_simplify.
+Hint Rewrite Z.land_ones using lia : bv_unfolded_simplify.
+Hint Rewrite bv_wrap_bv_wrap using lia : bv_unfolded_simplify.
+Hint Rewrite Z_to_bv_small using unfold bv_modulus; lia : bv_unfolded_simplify.
+
+(** * [bv_unfolded_to_arith] rewrite database *)
+(** The [bv_unfolded_to_arith] database collects rewrite rules that
+convert bitwise operations to arithmetic operations in preparation for lia. *)
+Create HintDb bv_unfolded_to_arith discriminated. (* Technically not necessary for rewrite db. *)
+Hint Rewrite <-Z.opp_lnot : bv_unfolded_to_arith.
+Hint Rewrite Z.shiftl_mul_pow2 Z.shiftr_div_pow2 using lia : bv_unfolded_to_arith.
+
+(** * Reduction of closed terms *)
+Ltac reduce_closed_N_tac := idtac.
+Ltac reduce_closed_N :=
+  idtac;
+  reduce_closed_N_tac;
+  repeat match goal with
+  | |- context [N.add ?a ?b] => progress reduce_closed (N.add a b)
+  | H : context [N.add ?a ?b] |- _ => progress reduce_closed (N.add a b)
+  end.
+
+Ltac reduce_closed_bv_simplify_tac := idtac.
+Ltac reduce_closed_bv_simplify :=
+  idtac;
+  reduce_closed_bv_simplify_tac;
+  (* reduce closed logical operators that lia does not understand *)
+  repeat match goal with
+  | |- context [Z.lor ?a ?b] => progress reduce_closed (Z.lor a b)
+  | H : context [Z.lor ?a ?b] |- _ => progress reduce_closed (Z.lor a b)
+  | |- context [Z.land ?a ?b] => progress reduce_closed (Z.land a b)
+  | H : context [Z.land ?a ?b] |- _ => progress reduce_closed (Z.land a b)
+  | |- context [Z.lxor ?a ?b] => progress reduce_closed (Z.lxor a b)
+  | H : context [Z.lxor ?a ?b] |- _ => progress reduce_closed (Z.lxor a b)
+  end.
+
+(** * [bv_simplify] tactic *)
+Tactic Notation "bv_simplify" :=
+  unfold_lets_in_context;
+  (* We need to reduce operations on N in indices of bv because
+  otherwise lia can get confused (it does not perform unification when
+  finding identical subterms). This sometimes leads to problems
+  with length of lists of bytes. *)
+  reduce_closed_N;
+  autorewrite with bv_simplify;
+  first [apply bv_eq_wrap | apply bv_neq_wrap | idtac];
+  bv_unfold;
+  autorewrite with bv_unfolded_simplify.
+
+Tactic Notation "bv_simplify" ident(H) :=
+  unfold_lets_in_context;
+  autorewrite with bv_simplify in H;
+  first [ apply bv_eq in H | apply bv_neq in H | idtac ];
+  tactic bv_unfold in H;
+  autorewrite with bv_unfolded_simplify in H.
+Tactic Notation "bv_simplify" "select" open_constr(pat) :=
+  select pat (fun H => bv_simplify H).
+
+Tactic Notation "bv_simplify_arith" :=
+  bv_simplify;
+  autorewrite with bv_unfolded_to_arith;
+  reduce_closed_bv_simplify.
+Tactic Notation "bv_simplify_arith" ident(H) :=
+  bv_simplify H;
+  autorewrite with bv_unfolded_to_arith in H;
+  reduce_closed_bv_simplify.
+Tactic Notation "bv_simplify_arith" "select" open_constr(pat) :=
+  select pat (fun H => bv_simplify_arith H).
+
+(** * [bv_solve] tactic *)
+Ltac bv_solve_unfold_tac := idtac.
+Ltac bv_solve :=
+  bv_simplify_arith;
+  (* we unfold signed so we just need to saturate unsigned *)
+  bv_saturate_unsigned;
+  bv_solve_unfold_tac;
+  unfold bv_signed, bv_swrap, bv_wrap, bv_half_modulus, bv_modulus, bv_unsigned in *;
+  simpl;
+  lia.
+
+Class BvSolve (P : Prop) : Prop := bv_solve_proof : P.
+Global Hint Extern 1 (BvSolve ?P) => (change P; bv_solve) : typeclass_instances.
diff --git a/tests/bitvector.ref b/tests/bitvector.ref
new file mode 100644
index 0000000000000000000000000000000000000000..5320c9c6ddbaea2b6a872a98f40f2ec202ab91f1
--- /dev/null
+++ b/tests/bitvector.ref
@@ -0,0 +1,19 @@
+"notation_test"
+     : string
+BV 10 3 = BV 10 5
+     : Prop
+The command has indeed failed with message:
+The term "BV 10 5" has type "bv 10" while it is expected to have type "bv 2".
+BV 2 3 = BV 10 5
+     : Prop
+The command has indeed failed with message:
+Unable to satisfy the following constraints:
+
+?bv_is_wf : "BvWf 2 4"
+
+"bvn_to_bv_test"
+     : string
+1 goal
+  
+  ============================
+  Some (BV 2 3) = Some (BV 2 3)
diff --git a/tests/bitvector.v b/tests/bitvector.v
new file mode 100644
index 0000000000000000000000000000000000000000..4f64bbadf772e29c03681ca28532b57d111fc383
--- /dev/null
+++ b/tests/bitvector.v
@@ -0,0 +1,11 @@
+From stdpp Require Import strings.
+From stdpp.unstable Require Import bitvector.
+
+Check "notation_test".
+Check (BV 10 3 = BV 10 5).
+Fail Check (BV 2 3 = BV 10 5).
+Check (BV 2 3 =@{bvn} BV 10 5).
+Fail Goal (BV 2 4 = BV 2 5).
+
+Check "bvn_to_bv_test".
+Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.
diff --git a/tests/bitvector_tactics.ref b/tests/bitvector_tactics.ref
new file mode 100644
index 0000000000000000000000000000000000000000..cb9e104d779e226257918ae9df0cca54c040b91d
--- /dev/null
+++ b/tests/bitvector_tactics.ref
@@ -0,0 +1,66 @@
+1 goal
+  
+  a : Z
+  ============================
+  bv_wrap 64 (a + 1) = bv_wrap 64 (Z.succ a)
+1 goal
+  
+  l, r, xs : bv 64
+  data : list (bv 64)
+  H : bv_unsigned l < bv_unsigned r
+  H0 : bv_unsigned r ≤ Z.of_nat (length data)
+  H1 : bv_unsigned xs + Z.of_nat (length data) * 8 < 2 ^ 52
+  ============================
+  bv_wrap 64
+    (bv_unsigned xs +
+     (bv_unsigned l + bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1) *
+     8) < 2 ^ 52
+2 goals
+  
+  l, r : bv 64
+  data : list (bv 64)
+  H : bv_unsigned l < bv_unsigned r
+  H0 : bv_unsigned r ≤ Z.of_nat (length data)
+  H1 : ¬ bv_swrap 128 (bv_unsigned l) >=
+         bv_swrap 128
+           (bv_wrap 64
+              (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 +
+               bv_unsigned l + 0))
+  ============================
+  bv_unsigned l <
+  bv_wrap 64
+    (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 + bv_unsigned l +
+     0)
+
+goal 2 is:
+ bv_wrap 64
+   (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 + bv_unsigned l +
+    0) ≤ Z.of_nat (length data)
+1 goal
+  
+  r1 : bv 64
+  H : bv_unsigned r1 ≠ 22
+  ============================
+  bv_wrap 64 (bv_unsigned r1 + 18446744073709551593 + 1) ≠ bv_wrap 64 0
+1 goal
+  
+  i, n : bv 64
+  H : bv_unsigned i < bv_unsigned n
+  H0 : bv_wrap 64
+         (bv_unsigned n + bv_wrap 64 (- bv_wrap 64 (bv_unsigned i + 1) - 1) +
+          1) ≠ 0
+  ============================
+  bv_wrap 64 (bv_unsigned i + 1) < bv_unsigned n
+1 goal
+  
+  b : bv 16
+  v : bv 64
+  ============================
+  bv_wrap 64
+    (Z.lor (Z.land (bv_unsigned v) 18446744069414649855)
+       (bv_wrap 64 (bv_unsigned b ≪ 16))) =
+  bv_wrap 64
+    (Z.lor
+       (bv_wrap (16 * 2) (bv_unsigned v ≫ Z.of_N (16 * 2)) ≪ Z.of_N (16 * 2))
+       (Z.lor (bv_unsigned b ≪ Z.of_N (16 * 1))
+          (bv_wrap (16 * 1) (bv_unsigned v))))
diff --git a/tests/bitvector_tactics.v b/tests/bitvector_tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..b5b2f6f50b8b48f218b9b52490a2d3bdc269a4fb
--- /dev/null
+++ b/tests/bitvector_tactics.v
@@ -0,0 +1,75 @@
+From stdpp Require Import strings.
+From stdpp.unstable Require Import bitblast bitvector_tactics.
+Unset Mangle Names.
+
+Local Open Scope Z_scope.
+Local Open Scope bv_scope.
+
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+
+(** * Smoke tests *)
+
+(** Simple test *)
+Goal ∀ a : Z, Z_to_bv 64 a `+Z` 1 = Z_to_bv 64 (Z.succ a).
+Proof.
+  intros. bv_simplify. Show.
+  Restart.
+  intros. bv_solve.
+Qed.
+
+(** More complex test *)
+Goal ∀ l r xs : bv 64, ∀ data : list (bv 64),
+    bv_unsigned l < bv_unsigned r →
+    bv_unsigned r ≤ Z.of_nat (length data) →
+    bv_unsigned xs + Z.of_nat (length data) * 8 < 2 ^ 52 →
+    bv_unsigned (xs + (bv_extract 0 64 (bv_zero_extend 128 l) +
+                       bv_extract 0 64 (bv_zero_extend 128 ((r - l) ≫ BV 64 1))) * BV 64 8) < 2 ^ 52.
+Proof.
+  intros. bv_simplify_arith. Show.
+  Restart.
+  intros. bv_solve.
+Qed.
+
+(** Testing simplification in hypothesis *)
+Goal ∀ l r : bv 64, ∀ data : list (bv 64),
+  bv_unsigned l < bv_unsigned r →
+  bv_unsigned r ≤ Z.of_nat (length data) →
+  ¬ bv_signed (bv_zero_extend 128 l) >=
+    bv_signed (bv_zero_extend 128 (bv_zero_extend 128 ((r - l) ≫ BV 64 1 + l + BV 64 0))) →
+  bv_unsigned l < bv_unsigned ((r - l) ≫ BV 64 1 + l + BV 64 0) ≤ Z.of_nat (length data).
+Proof.
+  intros. bv_simplify_arith select (¬ _ >= _). bv_simplify_arith.
+  split. (* We need to split since the [_ < _ ≤ _] notation differs between Coq versions. *) Show.
+  Restart.
+  intros. bv_simplify_arith select (¬ _ >= _). bv_solve.
+Qed.
+
+(** Testing inequality in goal. *)
+Goal ∀ r1 : bv 64,
+  bv_unsigned r1 ≠ 22 →
+  bv_extract 0 64 (bv_zero_extend 128 r1 + BV 128 0xffffffffffffffe9 + BV 128 1) ≠ BV 64 0.
+Proof.
+  intros. bv_simplify. Show.
+  Restart.
+  intros. bv_solve.
+Qed.
+
+(** Testing inequality in hypothesis. *)
+Goal ∀ i n : bv 64,
+  bv_unsigned i < bv_unsigned n →
+  bv_extract 0 64 (bv_zero_extend 128 n + bv_zero_extend 128 (bv_not (bv_extract 0 64 (bv_zero_extend 128 i)
+          + BV 64 1)) + BV 128 1) ≠ BV 64 0 →
+  bv_unsigned (bv_extract 0 64 (bv_zero_extend 128 i) + BV 64 1) < bv_unsigned n.
+Proof.
+  intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_simplify. Show.
+  Restart.
+  intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_solve.
+Qed.
+
+(** Testing combination of bitvector and bitblast. *)
+Goal ∀ b : bv 16, ∀ v : bv 64,
+  bv_or (bv_and v (BV 64 0xffffffff0000ffff)) (bv_zero_extend 64 b ≪ BV 64 16) =
+  bv_concat 64 (bv_extract (16 * (1 + 1)) (16 * 2) v) (bv_concat (16 * (1 + 1)) b (bv_extract 0 (16 * 1) v)).
+Proof.
+  intros. bv_simplify. Show. bitblast.
+Qed.