diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9500ee9d0e6d6c991c365d4cff2e850588b0a0c6..027e79b70733a40dd633d2c7279715e2c5fdf1f5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -32,6 +32,13 @@ Coq 8.11 is no longer supported.
 - Rename `lookup_union_l` → `lookup_union_l'` and add `lookup_union_l`
   as the dual to `lookup_union_r`.
 - Add `map_seqZ` as the `Z` analogue of `map_seq`. (by Michael Sammler)
+- Add the `coq-stdpp-unstable` package for libraries that are not
+  deemed stable enough to be included in the main std++ library,
+  following the `coq-iris-unstable` package. This library is contained
+  in the `stdpp_unstable` folder. The `theories` folder was renamed
+  to `stdpp`.
+- Add an unstable `bitblast` tactic for solving equalities between integers
+  involving bitwise operations. (by Michael Sammler)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/README.md b/README.md
index d50a23592a8d4d77853f4b2c7e03c3a2c68b7ff5..06c5781d75308beb7a0fb2d360c0424e350cdd3a 100644
--- a/README.md
+++ b/README.md
@@ -65,6 +65,16 @@ To obtain a development version, add the Iris opam repository:
 Run `make -jN` in this directory to build the library, where `N` is the number
 of your CPU cores.  Then run `make install` to install the library.
 
+## Unstable libraries
+
+The `stdpp_unstable` folder contains a set of libraries that are not
+deemed stable enough to be included in the main std++ library. These
+libraries are available via the `coq-stdpp-unstable` opam package. For
+each library, there is a corresponding "tracking issue" in the std++
+issue tracker (also linked from the library itself) which tracks the
+work that still needs to be done before moving the library to std++.
+No stability guarantees whatsoever are made for this package.
+
 ## Contributing to std++
 
 If you want to report a bug, please use the
diff --git a/_CoqProject b/_CoqProject
index dc020706b9802fc1033d9a51ce07cdd32742f4f8..c5842c0298688ab5037c8d112a8b5876f501d607 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,7 @@
--Q theories stdpp
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q stdpp stdpp
+-Q stdpp_unstable stdpp.unstable
 # 'Global Hint Rewrite' not supported before Coq 8.14.
 -arg -w -arg -deprecated-hint-rewrite-without-locality
 # Fixing this one requires Coq 8.15.
@@ -6,51 +9,53 @@
 # Fixing this one requires Coq 8.13.
 -arg -w -arg -deprecated-syntactic-definition
 
-theories/options.v
-theories/base.v
-theories/tactics.v
-theories/option.v
-theories/fin_map_dom.v
-theories/boolset.v
-theories/fin_maps.v
-theories/fin.v
-theories/vector.v
-theories/pmap.v
-theories/stringmap.v
-theories/fin_sets.v
-theories/mapset.v
-theories/proof_irrel.v
-theories/hashset.v
-theories/pretty.v
-theories/countable.v
-theories/orders.v
-theories/natmap.v
-theories/strings.v
-theories/well_founded.v
-theories/relations.v
-theories/sets.v
-theories/listset.v
-theories/streams.v
-theories/gmap.v
-theories/gmultiset.v
-theories/prelude.v
-theories/listset_nodup.v
-theories/finite.v
-theories/numbers.v
-theories/nmap.v
-theories/zmap.v
-theories/coPset.v
-theories/coGset.v
-theories/lexico.v
-theories/propset.v
-theories/decidable.v
-theories/list.v
-theories/list_numbers.v
-theories/functions.v
-theories/hlist.v
-theories/sorting.v
-theories/infinite.v
-theories/nat_cancel.v
-theories/namespaces.v
-theories/telescopes.v
-theories/binders.v
+stdpp/options.v
+stdpp/base.v
+stdpp/tactics.v
+stdpp/option.v
+stdpp/fin_map_dom.v
+stdpp/boolset.v
+stdpp/fin_maps.v
+stdpp/fin.v
+stdpp/vector.v
+stdpp/pmap.v
+stdpp/stringmap.v
+stdpp/fin_sets.v
+stdpp/mapset.v
+stdpp/proof_irrel.v
+stdpp/hashset.v
+stdpp/pretty.v
+stdpp/countable.v
+stdpp/orders.v
+stdpp/natmap.v
+stdpp/strings.v
+stdpp/well_founded.v
+stdpp/relations.v
+stdpp/sets.v
+stdpp/listset.v
+stdpp/streams.v
+stdpp/gmap.v
+stdpp/gmultiset.v
+stdpp/prelude.v
+stdpp/listset_nodup.v
+stdpp/finite.v
+stdpp/numbers.v
+stdpp/nmap.v
+stdpp/zmap.v
+stdpp/coPset.v
+stdpp/coGset.v
+stdpp/lexico.v
+stdpp/propset.v
+stdpp/decidable.v
+stdpp/list.v
+stdpp/list_numbers.v
+stdpp/functions.v
+stdpp/hlist.v
+stdpp/sorting.v
+stdpp/infinite.v
+stdpp/nat_cancel.v
+stdpp/namespaces.v
+stdpp/telescopes.v
+stdpp/binders.v
+
+stdpp_unstable/bitblast.v
diff --git a/coq-stdpp-unstable.opam b/coq-stdpp-unstable.opam
new file mode 100644
index 0000000000000000000000000000000000000000..f0332325ee882f49e76753df2442735bb04b025e
--- /dev/null
+++ b/coq-stdpp-unstable.opam
@@ -0,0 +1,24 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The std++ team"
+license: "BSD-3-Clause"
+homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
+bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
+version: "dev"
+
+synopsis: "Unfinished std++ libraries"
+description: """
+This package contains libraries that have been proposed for inclusion in std++, but more
+work is needed before they are ready for this.
+"""
+tags: [
+  "logpath:stdpp.unstable"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+]
+
+build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_unstable" "install"]
diff --git a/coq-stdpp.opam b/coq-stdpp.opam
index 07b52f0d3c72002031b921788c96c1cc09286291..df7a0d05519f1e5a5f62cc35cff05015d167f39c 100644
--- a/coq-stdpp.opam
+++ b/coq-stdpp.opam
@@ -36,5 +36,5 @@ depends: [
   "coq" { (>= "8.12" & < "8.16~") | (= "dev") }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "stdpp" "-j%{jobs}%"]
+install: ["./make-package" "stdpp" "install"]
diff --git a/make-package b/make-package
new file mode 100755
index 0000000000000000000000000000000000000000..55c051a9f6b9b3d25936782b46e6b55dc35fa4ab
--- /dev/null
+++ b/make-package
@@ -0,0 +1,32 @@
+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! egrep -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+egrep "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | egrep -v "^-Q " >> "$COQFILE"
+# Get the files.
+egrep "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*
diff --git a/theories/base.v b/stdpp/base.v
similarity index 100%
rename from theories/base.v
rename to stdpp/base.v
diff --git a/theories/binders.v b/stdpp/binders.v
similarity index 100%
rename from theories/binders.v
rename to stdpp/binders.v
diff --git a/theories/boolset.v b/stdpp/boolset.v
similarity index 100%
rename from theories/boolset.v
rename to stdpp/boolset.v
diff --git a/theories/coGset.v b/stdpp/coGset.v
similarity index 100%
rename from theories/coGset.v
rename to stdpp/coGset.v
diff --git a/theories/coPset.v b/stdpp/coPset.v
similarity index 100%
rename from theories/coPset.v
rename to stdpp/coPset.v
diff --git a/theories/countable.v b/stdpp/countable.v
similarity index 100%
rename from theories/countable.v
rename to stdpp/countable.v
diff --git a/theories/decidable.v b/stdpp/decidable.v
similarity index 100%
rename from theories/decidable.v
rename to stdpp/decidable.v
diff --git a/theories/fin.v b/stdpp/fin.v
similarity index 100%
rename from theories/fin.v
rename to stdpp/fin.v
diff --git a/theories/fin_map_dom.v b/stdpp/fin_map_dom.v
similarity index 100%
rename from theories/fin_map_dom.v
rename to stdpp/fin_map_dom.v
diff --git a/theories/fin_maps.v b/stdpp/fin_maps.v
similarity index 100%
rename from theories/fin_maps.v
rename to stdpp/fin_maps.v
diff --git a/theories/fin_sets.v b/stdpp/fin_sets.v
similarity index 100%
rename from theories/fin_sets.v
rename to stdpp/fin_sets.v
diff --git a/theories/finite.v b/stdpp/finite.v
similarity index 100%
rename from theories/finite.v
rename to stdpp/finite.v
diff --git a/theories/functions.v b/stdpp/functions.v
similarity index 100%
rename from theories/functions.v
rename to stdpp/functions.v
diff --git a/theories/gmap.v b/stdpp/gmap.v
similarity index 100%
rename from theories/gmap.v
rename to stdpp/gmap.v
diff --git a/theories/gmultiset.v b/stdpp/gmultiset.v
similarity index 100%
rename from theories/gmultiset.v
rename to stdpp/gmultiset.v
diff --git a/theories/hashset.v b/stdpp/hashset.v
similarity index 100%
rename from theories/hashset.v
rename to stdpp/hashset.v
diff --git a/theories/hlist.v b/stdpp/hlist.v
similarity index 100%
rename from theories/hlist.v
rename to stdpp/hlist.v
diff --git a/theories/infinite.v b/stdpp/infinite.v
similarity index 100%
rename from theories/infinite.v
rename to stdpp/infinite.v
diff --git a/theories/lexico.v b/stdpp/lexico.v
similarity index 100%
rename from theories/lexico.v
rename to stdpp/lexico.v
diff --git a/theories/list.v b/stdpp/list.v
similarity index 100%
rename from theories/list.v
rename to stdpp/list.v
diff --git a/theories/list_numbers.v b/stdpp/list_numbers.v
similarity index 100%
rename from theories/list_numbers.v
rename to stdpp/list_numbers.v
diff --git a/theories/listset.v b/stdpp/listset.v
similarity index 100%
rename from theories/listset.v
rename to stdpp/listset.v
diff --git a/theories/listset_nodup.v b/stdpp/listset_nodup.v
similarity index 100%
rename from theories/listset_nodup.v
rename to stdpp/listset_nodup.v
diff --git a/theories/mapset.v b/stdpp/mapset.v
similarity index 100%
rename from theories/mapset.v
rename to stdpp/mapset.v
diff --git a/theories/namespaces.v b/stdpp/namespaces.v
similarity index 100%
rename from theories/namespaces.v
rename to stdpp/namespaces.v
diff --git a/theories/nat_cancel.v b/stdpp/nat_cancel.v
similarity index 100%
rename from theories/nat_cancel.v
rename to stdpp/nat_cancel.v
diff --git a/theories/natmap.v b/stdpp/natmap.v
similarity index 100%
rename from theories/natmap.v
rename to stdpp/natmap.v
diff --git a/theories/nmap.v b/stdpp/nmap.v
similarity index 100%
rename from theories/nmap.v
rename to stdpp/nmap.v
diff --git a/theories/numbers.v b/stdpp/numbers.v
similarity index 100%
rename from theories/numbers.v
rename to stdpp/numbers.v
diff --git a/theories/option.v b/stdpp/option.v
similarity index 100%
rename from theories/option.v
rename to stdpp/option.v
diff --git a/theories/options.v b/stdpp/options.v
similarity index 100%
rename from theories/options.v
rename to stdpp/options.v
diff --git a/theories/orders.v b/stdpp/orders.v
similarity index 100%
rename from theories/orders.v
rename to stdpp/orders.v
diff --git a/theories/pmap.v b/stdpp/pmap.v
similarity index 100%
rename from theories/pmap.v
rename to stdpp/pmap.v
diff --git a/theories/prelude.v b/stdpp/prelude.v
similarity index 100%
rename from theories/prelude.v
rename to stdpp/prelude.v
diff --git a/theories/pretty.v b/stdpp/pretty.v
similarity index 100%
rename from theories/pretty.v
rename to stdpp/pretty.v
diff --git a/theories/proof_irrel.v b/stdpp/proof_irrel.v
similarity index 100%
rename from theories/proof_irrel.v
rename to stdpp/proof_irrel.v
diff --git a/theories/propset.v b/stdpp/propset.v
similarity index 100%
rename from theories/propset.v
rename to stdpp/propset.v
diff --git a/theories/relations.v b/stdpp/relations.v
similarity index 100%
rename from theories/relations.v
rename to stdpp/relations.v
diff --git a/theories/sets.v b/stdpp/sets.v
similarity index 100%
rename from theories/sets.v
rename to stdpp/sets.v
diff --git a/theories/sorting.v b/stdpp/sorting.v
similarity index 100%
rename from theories/sorting.v
rename to stdpp/sorting.v
diff --git a/theories/streams.v b/stdpp/streams.v
similarity index 100%
rename from theories/streams.v
rename to stdpp/streams.v
diff --git a/theories/stringmap.v b/stdpp/stringmap.v
similarity index 100%
rename from theories/stringmap.v
rename to stdpp/stringmap.v
diff --git a/theories/strings.v b/stdpp/strings.v
similarity index 100%
rename from theories/strings.v
rename to stdpp/strings.v
diff --git a/theories/tactics.v b/stdpp/tactics.v
similarity index 100%
rename from theories/tactics.v
rename to stdpp/tactics.v
diff --git a/theories/telescopes.v b/stdpp/telescopes.v
similarity index 100%
rename from theories/telescopes.v
rename to stdpp/telescopes.v
diff --git a/theories/vector.v b/stdpp/vector.v
similarity index 100%
rename from theories/vector.v
rename to stdpp/vector.v
diff --git a/theories/well_founded.v b/stdpp/well_founded.v
similarity index 100%
rename from theories/well_founded.v
rename to stdpp/well_founded.v
diff --git a/theories/zmap.v b/stdpp/zmap.v
similarity index 100%
rename from theories/zmap.v
rename to stdpp/zmap.v
diff --git a/stdpp_unstable/bitblast.v b/stdpp_unstable/bitblast.v
new file mode 100644
index 0000000000000000000000000000000000000000..d8f71e5ac5943467cfdc8d58d23ce0bd1c973c43
--- /dev/null
+++ b/stdpp_unstable/bitblast.v
@@ -0,0 +1,528 @@
+(* This file is still experimental. See its tracking issue
+https://gitlab.mpi-sws.org/iris/stdpp/-/issues/141 for details on remaining
+issues before stabilization. This file is maintained by Michael Sammler. *)
+From Coq Require Import ssreflect.
+From Coq.btauto Require Export Btauto.
+From stdpp Require Export tactics numbers list.
+From stdpp Require Import options.
+
+(** * [bitblast] tactic: Solve integer goals by bitwise reasoning *)
+(** This file provides the [bitblast] tactic for bitwise reasoning
+about [Z] via [Z.testbit]. Concretely, [bitblast] first turns an
+equality [a = b] into [∀ n, Z.testbit a n = Z.testbit a b], then
+simplifies the [Z.testbit] expressions using lemmas like
+[Z.testbit (Z.land a b) n = Z.testbit a n && Z.testbit b n], or
+[Z.testbit (Z.ones z) n = bool_decide (0 ≤ n < z) || bool_decide (z < 0 ∧ 0 ≤ n)]
+and finally simplifies the resulting boolean expression by performing case
+distinction on all [bool_decide] in the goal and pruning impossible cases.
+
+This library provides the following variants of the [bitblast] tactic:
+- [bitblast]: applies the bitblasting technique described above to the goal.
+  If the goal already contains a [Z.testbit], the first step (which introduces
+  [Z.testbit] to prove equalities between [Z]) is skipped.
+- [bitblast as n] behaves the same as [bitblast], but it allows naming the [n]
+  introduced in the first step. Fails if the goal is not an equality between [Z].
+- [bitblast H] applies the simplification of [Z.testbit] in the hypothesis [H]
+  (but does not perform case distinction).
+- [bitblast H with n as H'] deduces from the equality [H] of the form [z1 = z2]
+  that the [n]-th bit of [z1] and [z2] are equal, simplifies the resulting
+  equation, and adds it as the hypothesis [H'].
+- [bitblast H with n] is the same as [bitblast H with n as H'], but using a fresh
+  name for [H'].
+
+See also https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Z/bitblast.v
+for another implementation of the same idea.
+*)
+
+(** * Settings *)
+Local Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
+
+Local Open Scope Z_scope.
+
+(** * Helper lemmas to upstream *)
+Lemma Nat_eqb_eq n1 n2 :
+  (n1 =? n2)%nat = bool_decide (n1 = n2).
+Proof. case_bool_decide; [by apply Nat.eqb_eq | by apply Nat.eqb_neq]. Qed.
+Lemma Z_eqb_eq n1 n2 :
+  (n1 =? n2)%Z = bool_decide (n1 = n2).
+Proof. case_bool_decide; [by apply Z.eqb_eq | by apply Z.eqb_neq]. Qed.
+Lemma Z_testbit_pos_testbit p n :
+  (0 ≤ n)%Z →
+  Z.testbit (Z.pos p) n = Pos.testbit p (Z.to_N n).
+Proof. by destruct n, p. Qed.
+
+Lemma negb_forallb {A} (ls : list A) f :
+   negb (forallb f ls) = existsb (negb ∘ f) ls.
+Proof. induction ls; [done|]; simpl. rewrite negb_andb. congruence. Qed.
+
+Lemma Z_bits_inj'' a b :
+  a = b → (∀ n : Z, 0 ≤ n → Z.testbit a n = Z.testbit b n).
+Proof. apply Z.bits_inj_iff'. Qed.
+
+Lemma tac_tactic_in_hyp (P1 P2 : Prop) :
+  P1 → (P1 → P2) → P2.
+Proof. eauto. Qed.
+(** TODO: replace this with [do [ tac ] in H] from ssreflect? *)
+Tactic Notation "tactic" tactic3(tac) "in" ident(H) :=
+  let H' := fresh in
+  unshelve epose proof (tac_tactic_in_hyp _ _ H _) as H'; [shelve|
+    tac; let H := fresh H in intros H; exact H |];
+  clear H; rename H' into H.
+
+(** ** bitranges *)
+Fixpoint pos_to_bit_ranges_aux (p : positive) : (nat * nat) * list (nat * nat) :=
+  match p with
+  | xH => ((0, 1)%nat, [])
+  | xO p' =>
+      let x := pos_to_bit_ranges_aux p' in
+      ((S x.1.1, x.1.2), prod_map S id <$> x.2)
+  | xI p' =>
+      let x := pos_to_bit_ranges_aux p' in
+      if (x.1.1 =? 0)%nat then
+        ((0%nat, S x.1.2), prod_map S id <$> x.2)
+      else
+        ((0%nat, 1%nat), prod_map S id <$> (x.1 :: x.2))
+  end.
+
+(** [pos_to_bit_ranges p] computes the list of (start, length) pairs
+describing which bits of [p] are [1]. The following examples show the
+behavior of [pos_to_bit_ranges]: *)
+(* Compute (pos_to_bit_ranges 1%positive). (** 0b  1  [(0, 1)] *) *)
+(* Compute (pos_to_bit_ranges 2%positive). (** 0b 10  [(1, 1)] *) *)
+(* Compute (pos_to_bit_ranges 3%positive). (** 0b 11  [(0, 2)] *) *)
+(* Compute (pos_to_bit_ranges 4%positive). (** 0b100  [(2, 1)] *) *)
+(* Compute (pos_to_bit_ranges 5%positive). (** 0b101  [(0, 1); (2, 1)] *) *)
+(* Compute (pos_to_bit_ranges 6%positive). (** 0b110  [(1, 2)] *) *)
+(* Compute (pos_to_bit_ranges 7%positive). (** 0b111  [(0, 3)] *) *)
+(* Compute (pos_to_bit_ranges 21%positive). (** 0b10101  [(0, 1); (2, 1); (4, 1)] *) *)
+
+Definition pos_to_bit_ranges (p : positive) : list (nat * nat) :=
+  let x := pos_to_bit_ranges_aux p in x.1::x.2.
+
+Lemma pos_to_bit_ranges_spec p rs :
+  pos_to_bit_ranges p = rs →
+  (∀ n, Pos.testbit p n ↔ ∃ r, r ∈ rs ∧ (N.of_nat r.1 ≤ n ∧ n < N.of_nat r.1 + N.of_nat r.2)%N).
+Proof.
+  unfold pos_to_bit_ranges => <-.
+  elim: p => //; csimpl.
+  - move => p IH n. rewrite Nat_eqb_eq. case_match; subst.
+    + split; [|done] => _. case_match.
+      all: eexists _; split; [by apply elem_of_list_here|] => /=; lia.
+    + rewrite {}IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
+      * (* r = (pos_to_bit_ranges_aux p).1 *)
+        case_bool_decide as Heq; simplify_eq/=.
+        -- eexists _. split; [by apply elem_of_list_here|] => /=. lia.
+        -- eexists _. split. { apply elem_of_list_further. apply elem_of_list_here. }
+          simplify_eq/=. lia.
+      * (* r ∈ (pos_to_bit_ranges_aux p).2 *)
+        case_bool_decide as Heq; simplify_eq/=.
+        -- eexists _. split. { apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+           simplify_eq/=. lia.
+        -- eexists _. split. { do 2 apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+           simplify_eq/=. lia.
+      * eexists _. split; [by apply elem_of_list_here|]. case_bool_decide as Heq; simplify_eq/=; lia.
+      * case_bool_decide as Heq; simplify_eq/=.
+        -- move: Hin => /= /elem_of_list_fmap[?[??]]; subst. eexists _. split; [by apply elem_of_list_further |].
+           simplify_eq/=. lia.
+        -- rewrite -fmap_cons in Hin. move: Hin => /elem_of_list_fmap[?[??]]; subst. naive_solver lia.
+  - move => p IH n. case_match; subst.
+    + split; [done|] => -[[l h][/elem_of_cons[?|/(elem_of_list_fmap_2 _ _ _)[[??][??]]]?]]; simplify_eq/=; lia.
+    + rewrite IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
+      * eexists _. split; [by apply elem_of_list_here|] => /=; lia.
+      * eexists _. split. { apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+        destruct r; simplify_eq/=. lia.
+      * eexists _. split; [by apply elem_of_list_here|] => /=; lia.
+      * move: Hin => /elem_of_list_fmap[r'[??]]; subst. eexists _. split; [by apply elem_of_list_further|].
+         destruct r'; simplify_eq/=. lia.
+  - move => n. setoid_rewrite elem_of_list_singleton. case_match; split => //; subst; naive_solver lia.
+Qed.
+
+Definition Z_to_bit_ranges (z : Z) : list (nat * nat) :=
+  match z with
+  | Z0 => []
+  | Z.pos p => pos_to_bit_ranges p
+  | Z.neg p => []
+  end.
+
+Lemma Z_to_bit_ranges_spec z n rs :
+  (0 ≤ n)%Z →
+  (0 ≤ z)%Z →
+  Z_to_bit_ranges z = rs →
+  Z.testbit z n ↔ Exists (λ r, Z.of_nat r.1 ≤ n ∧ n < Z.of_nat r.1 + Z.of_nat r.2) rs.
+Proof.
+  move => /= ??.
+  destruct z => //=.
+  + move => <-. rewrite Z.bits_0 Exists_nil. done.
+  + move => /pos_to_bit_ranges_spec Hbit. rewrite Z_testbit_pos_testbit // Hbit Exists_exists. naive_solver lia.
+Qed.
+
+(** * [simpl_bool] *)
+Ltac simpl_bool_cbn := cbn [andb orb negb].
+
+Ltac simpl_bool :=
+  repeat match goal with
+         | |- context C [true && ?b] => simpl_bool_cbn
+         | |- context C [false && ?b] => simpl_bool_cbn
+         | |- context C [true || ?b] => simpl_bool_cbn
+         | |- context C [false || ?b] => simpl_bool_cbn
+         | |- context C [negb true] => simpl_bool_cbn
+         | |- context C [negb false] => simpl_bool_cbn
+         | |- context C [?b && true] => rewrite (Bool.andb_true_r b)
+         | |- context C [?b && false] => rewrite (Bool.andb_false_r b)
+         | |- context C [?b || true] => rewrite (Bool.orb_true_r b)
+         | |- context C [?b || false] => rewrite (Bool.orb_false_r b)
+         | |- context C [xorb ?b true] => rewrite (Bool.xorb_true_r b)
+         | |- context C [xorb ?b false] => rewrite (Bool.xorb_false_r b)
+         | |- context C [xorb true ?b] => rewrite (Bool.orb_true_l b)
+         | |- context C [xorb false ?b] => rewrite (Bool.orb_false_l b)
+         end.
+
+(** * [simplify_bitblast_index] *)
+Create HintDb simplify_bitblast_index_db discriminated.
+
+Hint Rewrite
+  Z.sub_add
+  Z.add_simpl_r
+  : simplify_bitblast_index_db.
+
+Local Ltac simplify_bitblast_index := autorewrite with simplify_bitblast_index_db.
+
+(** * Main typeclasses for bitblast *)
+Create HintDb bitblast discriminated.
+Global Hint Constants Opaque : bitblast.
+Global Hint Variables Opaque : bitblast.
+
+(** ** [IsPowerOfTwo] *)
+Class IsPowerOfTwo (z n : Z) := {
+  is_power_of_two_proof : z = 2 ^ n;
+}.
+Global Arguments is_power_of_two_proof _ _ {_}.
+Global Hint Mode IsPowerOfTwo + - : bitblast.
+Lemma is_power_of_two_pow2 n :
+  IsPowerOfTwo (2 ^ n) n.
+Proof. constructor. done. Qed.
+Global Hint Resolve is_power_of_two_pow2 | 10 : bitblast.
+Lemma is_power_of_two_const n p :
+  (∀ x, [(n, 1%nat)] = x → prod_map Z.of_nat id <$> Z_to_bit_ranges (Z.pos p) = x) →
+  IsPowerOfTwo (Z.pos p) n.
+Proof.
+  move => Hn. constructor. have {}Hn := Hn _ ltac:(done).
+  apply Z.bits_inj_iff' => i ?.
+  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done|lia|done].
+  move: Hn => /(fmap_cons_inv _ _ _)[[n' ?][?/=[[??][/(@eq_sym _ _ _)/fmap_nil_inv->->]]]]. subst.
+  rewrite Exists_cons Exists_nil /=.
+  rewrite Z.pow2_bits_eqb ?Z_eqb_eq ?bool_decide_spec; lia.
+Qed.
+Global Hint Extern 10 (IsPowerOfTwo (Z.pos ?p) _) =>
+  lazymatch isPcst p with | true => idtac end;
+  simple notypeclasses refine (is_power_of_two_const _ _ _);
+   let H := fresh in intros ? H; vm_compute; apply H
+  : bitblast.
+
+(** ** [BitblastBounded] *)
+Class BitblastBounded (z n : Z) := {
+  bitblast_bounded_proof : 0 ≤ z < 2 ^ n;
+}.
+Global Arguments bitblast_bounded_proof _ _ {_}.
+Global Hint Mode BitblastBounded + - : bitblast.
+
+Global Hint Extern 10 (BitblastBounded _ _) =>
+  constructor; first [ split; [lia|done] | done]
+  : bitblast.
+
+(** ** [Bitblast] *)
+Class Bitblast (z n : Z) (b : bool) := {
+  bitblast_proof : Z.testbit z n = b;
+}.
+Global Arguments bitblast_proof _ _ _ {_}.
+Global Hint Mode Bitblast + + - : bitblast.
+
+Definition BITBLAST_TESTBIT := Z.testbit.
+Lemma bitblast_id z n :
+  Bitblast z n (bool_decide (0 ≤ n) && BITBLAST_TESTBIT z n).
+Proof. constructor. case_bool_decide => //=. rewrite Z.testbit_neg_r //; lia. Qed.
+Global Hint Resolve bitblast_id | 1000 : bitblast.
+Lemma bitblast_id_bounded z z' n :
+  BitblastBounded z z' →
+  Bitblast z n (bool_decide (0 ≤ n < z') && BITBLAST_TESTBIT z n).
+Proof.
+  move => [Hb]. constructor.
+  move: (Hb) => /Z_bounded_iff_bits_nonneg' Hn.
+  case_bool_decide => //=.
+  destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
+  apply Hn; try lia.
+  destruct (decide (0 ≤ z')) => //.
+  rewrite Z.pow_neg_r in Hb; lia.
+Qed.
+Global Hint Resolve bitblast_id_bounded | 990 : bitblast.
+Lemma bitblast_0 n :
+  Bitblast 0 n false.
+Proof. constructor. by rewrite Z.bits_0. Qed.
+Global Hint Resolve bitblast_0 | 10 : bitblast.
+Lemma bitblast_pos p n rs b :
+  (∀ x, rs = x → (λ p, (Z.of_nat p.1, Z.of_nat p.1 + Z.of_nat p.2)) <$> Z_to_bit_ranges (Z.pos p) = x) →
+  existsb (λ '(r1, r2), bool_decide (r1 ≤ n ∧ n < r2)) rs = b →
+  Bitblast (Z.pos p) n b.
+Proof.
+  move => Hr <-. constructor. rewrite -(Hr rs) //.
+  destruct (decide (0 ≤ n)). 2: {
+    rewrite Z.testbit_neg_r; [|lia]. elim: (Z_to_bit_ranges (Z.pos p)) => // [??]; csimpl => <-.
+    case_bool_decide => //; lia.
+  }
+  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done..]. rewrite existb_True Exists_fmap.
+  f_equiv => -[??] /=. by rewrite bool_decide_spec.
+Qed.
+Global Hint Extern 10 (Bitblast (Z.pos ?p) _ _) =>
+  lazymatch isPcst p with | true => idtac end;
+  simple notypeclasses refine (bitblast_pos _ _ _ _ _ _);[shelve|
+   let H := fresh in intros ? H; vm_compute; apply H |
+   cbv [existsb]; exact eq_refl]
+  : bitblast.
+Lemma bitblast_neg p n rs b :
+  (∀ x, rs = x → (λ p, (Z.of_nat p.1, Z.of_nat p.1 + Z.of_nat p.2)) <$> Z_to_bit_ranges (Z.pred (Z.pos p)) = x) →
+  forallb (λ '(r1, r2), bool_decide (n < r1 ∨ r2 ≤ n)) rs = b →
+  Bitblast (Z.neg p) n (bool_decide (0 ≤ n) && b).
+Proof.
+  move => Hr <-. constructor. rewrite -(Hr rs) //.
+  case_bool_decide => /=; [|rewrite Z.testbit_neg_r; [done|lia]].
+  have -> : Z.neg p = Z.lnot (Z.pred (Z.pos p)).
+  { rewrite -Pos2Z.opp_pos. have := Z.add_lnot_diag (Z.pred (Z.pos p)). lia. }
+  rewrite Z.lnot_spec //. symmetry. apply negb_sym.
+  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done|lia|done].
+  rewrite negb_forallb existb_True Exists_fmap.
+  f_equiv => -[??] /=. rewrite negb_True bool_decide_spec. lia.
+Qed.
+Global Hint Extern 10 (Bitblast (Z.neg ?p) _ _) =>
+  lazymatch isPcst p with | true => idtac end;
+  simple notypeclasses refine (bitblast_neg _ _ _ _ _ _);[shelve|shelve|
+   let H := fresh in intros ? H; vm_compute; apply H |
+   cbv [forallb]; exact eq_refl]
+    : bitblast.
+Lemma bitblast_land z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.land z1 z2) n (b1 && b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.land_spec. Qed.
+Global Hint Resolve bitblast_land | 10 : bitblast.
+Lemma bitblast_lor z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.lor z1 z2) n (b1 || b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.lor_spec. Qed.
+Global Hint Resolve bitblast_lor | 10 : bitblast.
+Lemma bitblast_lxor z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.lxor z1 z2) n (xorb b1 b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.lxor_spec. Qed.
+Global Hint Resolve bitblast_lxor | 10 : bitblast.
+Lemma bitblast_shiftr z1 z2 n b1 :
+  Bitblast z1 (n + z2) b1 →
+  Bitblast (z1 ≫ z2) n (bool_decide (0 ≤ n) && b1).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide => /=; [by rewrite Z.shiftr_spec| rewrite Z.testbit_neg_r //; lia].
+Qed.
+Global Hint Resolve bitblast_shiftr | 10 : bitblast.
+Lemma bitblast_shiftl z1 z2 n b1 :
+  Bitblast z1 (n - z2) b1 →
+  Bitblast (z1 ≪ z2) n (bool_decide (0 ≤ n) && b1).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide => /=; [by rewrite Z.shiftl_spec| rewrite Z.testbit_neg_r //; lia].
+Qed.
+Global Hint Resolve bitblast_shiftl | 10 : bitblast.
+Lemma bitblast_lnot z1 n b1 :
+  Bitblast z1 n b1 →
+  Bitblast (Z.lnot z1) n (bool_decide (0 ≤ n) && negb b1).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide => /=; [by rewrite Z.lnot_spec| rewrite Z.testbit_neg_r //; lia].
+Qed.
+Global Hint Resolve bitblast_lnot | 10 : bitblast.
+Lemma bitblast_ldiff z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.ldiff z1 z2) n (b1 && negb b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.ldiff_spec. Qed.
+Global Hint Resolve bitblast_ldiff | 10 : bitblast.
+Lemma bitblast_ones z1 n :
+  Bitblast (Z.ones z1) n (bool_decide (0 ≤ n < z1) || bool_decide (z1 < 0 ∧ 0 ≤ n)).
+Proof.
+  constructor. case_bool_decide; [by apply Z.ones_spec_low|] => /=.
+  case_bool_decide.
+  - rewrite Z.ones_equiv Z.pow_neg_r; [|lia]. apply Z.bits_m1. lia.
+  - destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
+    apply Z.ones_spec_high; lia.
+Qed.
+Global Hint Resolve bitblast_ones | 10 : bitblast.
+Lemma bitblast_pow2 n n' :
+  Bitblast (2 ^ n') n (bool_decide (n = n' ∧ 0 ≤ n)).
+Proof.
+  constructor. case_bool_decide; destruct_and?; subst; [by apply Z.pow2_bits_true|].
+  destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
+  apply Z.pow2_bits_false. lia.
+Qed.
+Global Hint Resolve bitblast_pow2 | 10 : bitblast.
+Lemma bitblast_setbit z1 n b1 n' :
+  Bitblast (Z.lor z1 (2 ^ n')) n b1 →
+  Bitblast (Z.setbit z1 n') n b1.
+Proof. by rewrite Z.setbit_spec'. Qed.
+Global Hint Resolve bitblast_setbit | 10 : bitblast.
+Lemma bitblast_mod z1 z2 z2' n b1 :
+  IsPowerOfTwo z2 z2' →
+  Bitblast z1 n b1 →
+  (* Coq 8.14 changed the definition of [x `mod` 0] from [0] to [x],
+  so we have to use the following definition to be compatible with
+  both Coq 8.12 and Coq 8.14. The [z2' < 0] case is hopefully not
+  common in practice. *)
+  (* TODO: After dropping support for Coq 8.14, switch to the following definition: *)
+  (* Bitblast (z1 `mod` z2) n ((bool_decide (z2' < 0 ∧ 0 ≤ n) || bool_decide (n < z2')) && b1). *)
+  Bitblast (z1 `mod` z2) n ((bool_decide (z2' < 0 ∧ 0 ≤ n) && Z.testbit (z1 `mod` 0) n)
+                            || (bool_decide (n < z2') && b1)).
+Proof.
+  move => [->] [<-]. constructor.
+  case_bool_decide => /=. { rewrite Z.pow_neg_r ?bool_decide_false /= ?orb_false_r; [done|lia..]. }
+  destruct (decide (0 ≤ n)). 2: { rewrite !Z.testbit_neg_r ?andb_false_r //; lia. }
+  rewrite -Z.land_ones; [|lia]. rewrite Z.land_spec Z_ones_spec; [|lia..].
+  by rewrite andb_comm.
+Qed.
+Global Hint Resolve bitblast_mod | 10 : bitblast.
+(* TODO: What are good instances for +? Maybe something based on Z_add_nocarry_lor? *)
+Lemma bitblast_add_0 z1 z2 b1 b2 :
+  Bitblast z1 0 b1 →
+  Bitblast z2 0 b2 →
+  Bitblast (z1 + z2) 0 (xorb b1 b2).
+Proof. move => [<-] [<-]. constructor. apply Z.add_bit0. Qed.
+Global Hint Resolve bitblast_add_0 | 5 : bitblast.
+Lemma bitblast_add_1 z1 z2 b10 b11 b20 b21 :
+  Bitblast z1 0 b10 →
+  Bitblast z2 0 b20 →
+  Bitblast z1 1 b11 →
+  Bitblast z2 1 b21 →
+  Bitblast (z1 + z2) 1 (xorb (xorb b11 b21) (b10 && b20)).
+Proof. move => [<-] [<-] [<-] [<-]. constructor. apply Z.add_bit1. Qed.
+Global Hint Resolve bitblast_add_1 | 5 : bitblast.
+Lemma bitblast_clearbit z n b m :
+  Bitblast z n b →
+  Bitblast (Z.clearbit z m) n (bool_decide (n ≠ m) && b).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide; subst => /=.
+  - by apply Z.clearbit_neq.
+  - by apply Z.clearbit_eq.
+Qed.
+Global Hint Resolve bitblast_clearbit | 10 : bitblast.
+
+
+(** * Tactics *)
+
+(** ** Helper definitions and lemmas for the tactics *)
+Definition BITBLAST_BOOL_DECIDE := @bool_decide.
+Global Arguments BITBLAST_BOOL_DECIDE _ {_}.
+
+Lemma tac_bitblast_bool_decide_true G (P : Prop) `{!Decision P} :
+  P →
+  G true →
+  G (bool_decide P).
+Proof. move => ??. by rewrite bool_decide_eq_true_2. Qed.
+Lemma tac_bitblast_bool_decide_false G (P : Prop) `{!Decision P} :
+  ¬ P →
+  G false →
+  G (bool_decide P).
+Proof. move => ??. by rewrite bool_decide_eq_false_2. Qed.
+Lemma tac_bitblast_bool_decide_split G (P : Prop) `{!Decision P} :
+  (P → G true) →
+  (¬ P → G false) →
+  G (bool_decide P).
+Proof. move => ??. case_bool_decide; eauto. Qed.
+
+(** ** Core tactics *)
+Ltac bitblast_done :=
+  solve [ first [ done | lia | btauto ] ].
+
+(** [bitblast_blast_eq] applies to goals of the form [Z.testbit _ _ = ?x] and bitblasts the
+  Z.testbit using the [Bitblast] typeclass. *)
+Ltac bitblast_blast_eq :=
+  lazymatch goal with |- Z.testbit _ _ = _ => idtac end;
+  etrans; [ notypeclasses refine (bitblast_proof _ _ _); typeclasses eauto with bitblast | ];
+  simplify_bitblast_index;
+  exact eq_refl.
+
+(** [bitblast_bool_decide_simplify] get rids of unnecessary bool_decide in the goal. *)
+Ltac bitblast_bool_decide_simplify :=
+  repeat lazymatch goal with
+         | |- context [@bool_decide ?P ?Dec] =>
+             pattern (@bool_decide P Dec);
+             lazymatch goal with
+             | |- ?G _ =>
+                 first [
+                     refine (@tac_bitblast_bool_decide_true G P Dec _ _); [lia|];
+                     simpl_bool_cbn
+                   |
+                     refine (@tac_bitblast_bool_decide_false G P Dec _ _); [lia|];
+                     simpl_bool_cbn
+                   |
+                     change_no_check (G (@BITBLAST_BOOL_DECIDE P Dec))
+               ]
+             end;
+             cbv beta
+         end;
+  (** simpl_bool contains rewriting so it can be quite slow and thus we only do it at the end. *)
+  simpl_bool;
+  lazymatch goal with
+  | |- ?G => let x := eval unfold BITBLAST_BOOL_DECIDE in G in change_no_check x
+  end.
+
+(** [bitblast_bool_decide_split] performs a case distinction on a bool_decide in the goal. *)
+Ltac bitblast_bool_decide_split :=
+  lazymatch goal with
+  | |- context [@bool_decide ?P ?Dec] =>
+      pattern (@bool_decide P Dec);
+      lazymatch goal with
+      | |- ?G _ =>
+          refine (@tac_bitblast_bool_decide_split G P Dec _ _) => ?; cbv beta; simpl_bool
+      end
+  end.
+
+(** [bitblast_unfold] bitblasts all [Z.testbit] in the goal. *)
+Ltac bitblast_unfold :=
+  repeat lazymatch goal with
+  | |- context [Z.testbit ?z ?n] =>
+      pattern (Z.testbit z n);
+      simple refine (eq_rec_r _ _ _); [shelve| |bitblast_blast_eq]; cbv beta
+  end;
+  lazymatch goal with
+  | |- ?G => let x := eval unfold BITBLAST_TESTBIT in G in change_no_check x
+  end.
+
+(** [bitblast_raw] bitblasts all [Z.testbit] in the goal and simplifies the result. *)
+Ltac bitblast_raw :=
+  bitblast_unfold;
+  bitblast_bool_decide_simplify;
+  try bitblast_done;
+  repeat (bitblast_bool_decide_split; bitblast_bool_decide_simplify; try bitblast_done).
+
+(** ** Tactic notations *)
+Tactic Notation "bitblast" "as" ident(i) :=
+  apply Z.bits_inj_iff'; intros i => ?; bitblast_raw.
+
+Tactic Notation "bitblast" :=
+  lazymatch goal with
+  | |- context [Z.testbit _ _] => idtac
+  | _ => apply Z.bits_inj_iff' => ??
+  end;
+  bitblast_raw.
+
+Tactic Notation "bitblast" ident(H) :=
+  tactic bitblast_unfold in H;
+  tactic bitblast_bool_decide_simplify in H.
+Tactic Notation "bitblast" ident(H) "with" constr(i) "as" ident(H') :=
+  lazymatch type of H with
+  (* We cannot use [efeed pose proof] since this causes weird failures
+  in combination with [Set Mangle Names]. *)
+  | @eq Z _ _ => pose proof (Z_bits_inj'' _ _ H i) as H'; efeed specialize H'; [try bitblast_done..|]
+  | ∀ x, _ => pose proof (H i) as H'; efeed specialize H'; [try bitblast_done..|]
+  end; bitblast H'.
+Tactic Notation "bitblast" ident(H) "with" constr(i) :=
+  let H' := fresh "H" in bitblast H with i as H'.
diff --git a/tests/bitblast.ref b/tests/bitblast.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/bitblast.v b/tests/bitblast.v
new file mode 100644
index 0000000000000000000000000000000000000000..540082beaed716825e8b64297ad1666ffce86c90
--- /dev/null
+++ b/tests/bitblast.v
@@ -0,0 +1,39 @@
+From stdpp.unstable Require Import bitblast.
+
+Local Open Scope Z_scope.
+
+Goal ∀ x a k,
+  Z.land x (Z.land (Z.ones k) (Z.ones k) ≪ a) =
+  Z.land (Z.land (x ≫ a) (Z.ones k)) (Z.ones k) ≪ a.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ i,
+  1 ≪ i = Z.land (Z.ones 1) (Z.ones 1) ≪ i.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ N k,
+  0 ≤ k ≤ N → Z.ones N ≫ (N - k) = Z.ones k.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ z,
+  Z.land z (-1) = z.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ z,
+  Z.land z 0x20000 = 0 →
+  Z.land (z ≫ 17) (Z.ones 1) = 0.
+Proof.
+  intros ? Hz. bitblast as n.
+  by bitblast Hz with (n + 17).
+Qed.
+
+Goal ∀ z, 0 ≤ z < 2 ^ 64 →
+   Z.land z 0xfff0000000000007 = 0 ↔ z < 2 ^ 52 ∧ z `mod` 8 = 0.
+Proof.
+  intros z ?. split.
+  - intros Hx. split.
+    + apply Z_bounded_iff_bits_nonneg; [lia..|]. intros n ?. bitblast.
+      by bitblast Hx with n.
+    + bitblast as n. by bitblast Hx with n.
+  - intros [H1 H2]. bitblast as n. by bitblast H2 with n.
+Qed.