.gitignore

@@ -15,6 +15,7 @@
 .coq-native/
 Makefile.coq
 Makefile.coq.conf
+_CoqProject
 _CoqProject.*
 Makefile.package.*
 .Makefile.package.*
@@ -22,3 +23,6 @@ Makefile.package.*
 html/
 builddep/
 _opam
+_build/
+*.install
+config/local-flags

.gitlab-ci.yml

@@ -6,6 +6,8 @@ stages:
 variables:
   CPU_CORES: "10"
   OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+  # Avoid needlessly increasing our TCB with native_compute
+  COQEXTRAFLAGS: "-native-compiler no"
 
 .only_branches: &only_branches
   only:
@@ -42,10 +44,11 @@ variables:
 
 ## Build jobs
 
-build-coq.8.16.1:
+# The newest version runs with timing.
+build-coq.9.0.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.16.1"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     CI_COQCHK: "1"
@@ -55,38 +58,38 @@ build-coq.8.16.1:
   - fp-timing
   interruptible: false
 
-build-coq.8.16.1-mr:
+# The newest version also runs in MRs, without timing.
+build-coq.9.0.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.16.1"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
-build-coq.8.15.2:
+# Also ensure Dune works (broken on older Coq versions due to Stdlib split).
+build-coq.9.0.0-dune:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.2"
-    DENY_WARNINGS: "1"
+    OPAM_PINS: "coq version 9.0.0   dune version 3.18.1"
+    MAKE_TARGET: "dune"
 
-build-coq.8.14.1:
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.14.1"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"
 
-build-coq.8.13.2:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.2"
+    OPAM_PINS: "coq version 8.19.1"
     DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"
 
-build-coq.8.12.2:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.18.0:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.12.2"
+    OPAM_PINS: "coq version 8.18.0"
     DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"

Makefile

@@ -3,9 +3,19 @@ all: Makefile.coq
 	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 
+# Generate the _CoqProject file.
+_CoqProject: gen_CoqProject.sh config/paths config/flags config/source-list $(wildcard config/local-flags)
+	@./$< > $@
+
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	@#echo "Forwarding $@"
@@ -17,7 +27,7 @@ clean: Makefile.coq
 	+@$(MAKE) -f Makefile.coq clean
 	@# Make sure not to enter the `_opam` folder.
 	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq .lia.cache builddep/*
+	rm -f Makefile.coq .lia.cache builddep/* _CoqProject
 .PHONY: clean
 
 # Create Coq Makefile.
@@ -52,4 +62,4 @@ build-dep: builddep
 
 # Some files that do *not* need to be forwarded to Makefile.coq.
 # ("::" lets Makefile.local overwrite this.)
-Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
+Makefile Makefile.local config/paths config/flags config/source-list config/local-flags $(OPAMFILES):: ;

Makefile.coq.local

@@ -4,6 +4,11 @@ NO_TEST:=
 # use MAKE_REF=1 to generate new reference files
 MAKE_REF:=
 
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
 real-all: style $(if $(NO_TEST),,test)
 
@@ -24,8 +29,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | grep -E '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -41,17 +44,16 @@ tests/.coqdeps.d: $(TESTFILES)
 # - Either compare the result with the reference file, or move it over the reference file.
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
-	$(HIDE)if test -f $*".$(COQ_MINOR_VERSION).ref"; then \
-	    REF=$*".$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF=$*".ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(MAKE_REF), [make ref],) $< (ref: $$REF)" && \
+	$(HIDE)REF=$*".ref" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
 	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
-	  sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE") && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
+	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

README.md

@@ -26,26 +26,27 @@ Importing std++ has some side effects as the library sets some global options.
 Notably:
 
 * `Generalizable All Variables`: This option enables implicit generalization in
-  arguments of the form `` `{...}`` (i.e., anonymous arguments).  Unfortunately, it
-  also enables implicit generalization in `Instance`.  We think that the fact
-  that both behaviors are coupled together is a
-  [bug in Coq](https://github.com/coq/coq/issues/6030).
+  arguments of the form `` `{...}`` (i.e., anonymous arguments) and in terms of
+  shape `` `{}``/`` `[]``/`` `()``. See [Coq's
+  manual](https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#implicit-generalization)
+  for further details.
 * The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
   `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
   [`base.v`](theories/base.v) for further details.
-* It blocks `simpl` on all operations involving integers `Z` (by setting
-  `Arguments op : simpl never`). We do this because `simpl` tends to expose
-  the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
-  As a consequence of blocking `simpl`, due to
-  [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
-  becomes unreliable. We do not consider this an issue since we use `lia` (for
-  which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* It blocks `simpl` on all operations involving `Z`, `N`, and `positive` (by
+  setting `Arguments op : simpl never`). We do this because `simpl` tends to
+  expose the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+* It sets `intuition_solver` to `auto`. The default is `auto with *`, which is
+  very expensive.
 
 ## Prerequisites
 
 This version is known to compile with:
 
- - Coq version 8.12.2 / 8.13.2 / 8.14.1 / 8.15.2 / 8.16.1
+ - Coq version 8.18.0 / 8.19.1 / 8.20.1 / 9.0.0
+
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
 
 ## Installing via opam
 
@@ -92,9 +93,12 @@ your account.  Then you can fork the
 [Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
 changes in your fork, and create a merge request.
 
+Please refer to [our style guide](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/style_guide.md)
+for code formatting and naming policies.
+
 ## Common problems
 
-On Windows, differences in line endings may cause tests to fail. This can be 
+On Windows, differences in line endings may cause tests to fail. This can be
 fixed by setting Git's autocrlf option to true:
 
     git config --global core.autocrlf true

config/flags

+# Specification for custom Rocq compilation flags.
+# Syntax:
+# - One flag per line with no leading/trailing blanks.
+# - Empty lines and lines starting with '#' are ignored.
+
+# Fixing this one requires Coq 8.19
+-w
+-argument-scope-delimiter
+
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-w
+-notation-incompatible-prefix
+
+# We can't do this migration yet until we require Coq 9.0
+-w
+-deprecated-from-Coq
+-w
+-deprecated-dirpath-Coq

config/paths

+# Search paths for all packages.
+# Each line should be of the form "<PACKAGE> <LOGICAL_PATH>",
+# where <PACKAGE> is the name of a directory that matches the
+# corresponding package name.
+stdpp stdpp
+stdpp_bitvector stdpp.bitvector
+stdpp_unstable stdpp.unstable

_CoqProject → config/source-list

-# 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
-# Avoid needlessly increasing our trusted code base with native_compute
--arg -native-compiler -arg no
-# 'Global Hint Rewrite' not supported before Coq 8.14.
--arg -w -arg -deprecated-hint-rewrite-without-locality
-# Fixing this one requires Coq 8.15.
--arg -w -arg -deprecated-typeclasses-transparency-without-locality
-# Fixing this one requires Coq 8.13.
--arg -w -arg -deprecated-syntactic-definition
+# List of source files included in the libraries.
 
 stdpp/options.v
 stdpp/base.v
@@ -50,6 +39,11 @@ stdpp/lexico.v
 stdpp/propset.v
 stdpp/decidable.v
 stdpp/list.v
+stdpp/list_basics.v
+stdpp/list_relations.v
+stdpp/list_monad.v
+stdpp/list_misc.v
+stdpp/list_tactics.v
 stdpp/list_numbers.v
 stdpp/functions.v
 stdpp/hlist.v
@@ -59,7 +53,10 @@ stdpp/nat_cancel.v
 stdpp/namespaces.v
 stdpp/telescopes.v
 stdpp/binders.v
+stdpp/ssreflect.v
+
+stdpp_bitvector/definitions.v
+stdpp_bitvector/tactics.v
+stdpp_bitvector/bitvector.v
 
 stdpp_unstable/bitblast.v
-stdpp_unstable/bitvector.v
-stdpp_unstable/bitvector_tactics.v

coq-lint.sh

-#!/bin/bash
+#!/bin/sh
 set -e
 ## A simple shell script checking for some common Coq issues.
 
 FILE="$1"
 
-if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
     echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
     echo "Please add 'Global' or 'Local' as appropriate."
     echo

coq-stdpp-bitvector.opam

+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: "A library for bitvectors based on std++"
+description: """
+This library provides the `bv n` type for representing n-bit bitvectors (i.e.,
+fixed-size integers with n bits). It comes with definitions for the standard operations
+(e.g., the operations exposed by SMT-LIB) and some basic automation for solving bitvector
+goals based on the lia tactic.
+"""
+tags: [
+  "logpath:stdpp.bitvector"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+]
+
+build: ["./make-package" "stdpp_bitvector" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_bitvector" "install"]

coq-stdpp-unstable.opam

@@ -18,6 +18,7 @@ tags: [
 
 depends: [
   "coq-stdpp" {= version}
+  "coq-stdpp-bitvector" {= version}
 ]
 
 build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]

coq-stdpp.opam

@@ -33,7 +33,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.12" & < "8.17~") | (= "dev") }
+  "coq" { (>= "8.18" & < "9.1~") | (= "dev") }
 ]
 
 build: ["./make-package" "stdpp" "-j%{jobs}%"]

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Editors relying on `_CoqProject` files for their configuration are supported.
+A suitable `_CoqProject` file is generated by `dune build`. Note that you must
+invoke `dune` manually to make sure that the dependencies of the file you are
+stepping through are up-to-date. To build a single file, you can use, e.g.,
+`dune build stdpp/options.vo`. To build only the `stdpp` folder, you can do
+`dune build stdpp`.
+
+Alternatively, you can configure your editor to invoke `dune coq top` instead
+of `coqtop`, but that is non-trivial for most editors.
+
+### Extra `_CoqProject` flags
+
+If file `config/local-flags` exists, then its contents is added at the end of
+the generated `_CoqProject` file. This can be useful when the library is built
+together with its dependencies (e.g., the Rocq standard library) as part of a
+dune workspace build. Note that the file can be generated with a dune rule.

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   ; Configure coqc flags.
+   (flags (:standard %{read-lines:flags.dune})))))
+
+(rule
+ (action
+  (with-stdout-to flags.dune
+   (pipe-stdout
+    (cat config/flags)
+    (bash "grep '^[^#]\\+'")))))
+
+(rule
+ (deps
+  (glob_files config/*))
+ (mode promote)
+ (action
+  (with-stdout-to _CoqProject
+   (run ./gen_CoqProject.sh))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)

gen_CoqProject.sh

+#!/bin/sh
+set -e
+# Script generating the contents of [_CoqProject] based on files [config/*].
+# We use standard dune variable DUNE_SOURCEROOT to determine if the build
+# system is dune. In a dune build, the [_CoqProject] is solely used for editor
+# support.
+
+echo "# Generated file, edit [config/*] instead."
+
+echo
+echo "# Search paths"
+# Adding "-Q " prefix to all non-empty, non-comment lines of [config/paths].
+cat config/paths | grep "^[^#]\+" | sed "s/^/-Q /"
+# When building with dune, we also add the corresponding paths under dune's
+# [_build] directory. This is done by adding the prefix "-Q $PWD/" to all
+# non-empty, non-comment lines of [config/paths]. So for instance, this will
+# complement an entry of the form "-Q dir coqdir" produced above, with an
+# entry "-Q $PWD/dir coqdir". This relies on the fact that dune runs (a copy
+# of) the current script in the corresponding path under [_build]. This is
+# where ".vo" files actually end up in a dune build. Note that paths without
+# the "$PWD/" prefix are given first, so that editors find the original ".v"
+# sources (e.g., for "jump to definition") instead of their copy under the
+# [_build] directory.
+if [ -n "$DUNE_SOURCEROOT" ]; then
+  cat config/paths | grep "^[^#]\+" | sed "s,^,-Q $PWD/,"
+fi
+
+echo
+echo "# Flags"
+# Adding "-arg " prefix to all non-empty, non-comment lines of [config/flags].
+cat config/flags | grep "^[^#]\+" | sed "s/^/-arg /"
+
+# Potential extra flags.
+if [ -f config/local-flags ]; then
+  echo
+  # We take the whole file; no need to strip comments.
+  cat config/local-flags
+fi
+
+# The list of source files is only needed for [coq_makefile] builds.
+if [ -z "$DUNE_SOURCEROOT" ]; then
+  echo
+  echo "# Sources"
+  # Take only non-empty, non-comment lines of [config/source-list].
+  cat config/source-list | grep "^[^#]\+"
+fi

make-package

-#!/bin/bash
+#!/bin/sh
 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!
 
+# Make sure we get a GNU version of make.
+# This is exactly how opam determines which make executable to use.
+OS=$(uname)
+MAKE="make"
+if [ $OS == "FreeBSD" ] || [ $OS == "OpenBSD" ] ||\
+       [ $OS == "NetBSD" ] || [ $OS == "DragonFly" ]; then
+    MAKE="gmake"
+fi
+
 PROJECT="$1"
 shift
 
 COQFILE="_CoqProject.$PROJECT"
 MAKEFILE="Makefile.package.$PROJECT"
 
+# Ensure we have an up-to-date _CoqProject file.
+$MAKE _CoqProject
+
 if ! grep -E -q "^$PROJECT/" _CoqProject; then
     echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
     exit 1
@@ -26,7 +38,7 @@ grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
 "${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
 
 # Run build
-make -f "$MAKEFILE" "$@"
+$MAKE -f "$MAKEFILE" "$@"
 
 # Cleanup
 rm -f ".$MAKEFILE.d" "$MAKEFILE"*

stdpp/boolset.v

@@ -17,6 +17,10 @@ Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
 Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
+Global Instance boolset_cprod {A B} :
+  CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
+
 Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
 Proof.
   split; [split; [split| |]|].
@@ -31,6 +35,19 @@ Qed.
 Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
 
-Typeclasses Opaque boolset_elem_of.
+Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
+  x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof. apply andb_True. Qed.
+
+Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
+  SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
+  SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
+Proof.
+  intros ??; constructor.
+  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
+    (set_unfold_elem_of x.2 X2 Q).
+Qed.
+
+Global Typeclasses Opaque boolset_elem_of.
 Global Opaque boolset_empty boolset_singleton boolset_union
-  boolset_intersection boolset_difference.
+  boolset_intersection boolset_difference boolset_cprod.