feat: std::all_of, std::any_of, std::none_of specs

README.md

@@ -2,6 +2,10 @@
 
 Specifications of the C++ standard library in BRiCk.
 
+The [all_of, any_of, and none_of specifications](rocq-brick-libstdcpp/proof/all_any_none_of/README.md)
+currently cover only the C++20 non-policy instantiations with
+`const unsigned char*` iterators and a `bool (*)(unsigned char)` predicate.
+
 ## Development
 
 To develop on these specifications, you'll need clang, the GNU C++ library (not

rocq-brick-libstdcpp/proof/all_any_none_of/README.md

@@ -0,0 +1,39 @@
+# `std::all_of`, `std::any_of`, and `std::none_of`
+
+## Fixed scope
+
+These specifications cover the C++20 non-execution-policy overloads instantiated
+with `const unsigned char*` iterators and a `bool (*)(unsigned char)` predicate.
+They do not cover arbitrary iterator types, other element types, functors,
+`std::ranges` algorithms, or overloads taking an execution policy.
+
+## Contracts
+
+[spec.v](spec.v) preserves ownership and contents of the selected byte slice.
+The predicate contract in [pred.v](pred.v) tracks separate resources through
+`I k`, where `k` counts predicate applications. The postconditions expose a count
+`k` satisfying `0 <= k <= length xs`; no exact call count, visit order, or
+short-circuit behavior is promised.
+
+[model.v](model.v) describes the Boolean results, including empty ranges.
+`test x = None` leaves the predicate result unspecified; a known decisive value
+can still determine the algorithm result. [hints.v](hints.v) relates total
+predicates to `forallb` and `existsb`.
+
+These are library contracts with verified clients, not proofs of the underlying
+libstdc++ implementations. The predicate must satisfy the supplied callback
+contract.
+
+## Clients
+
+[The tests](../../test/all_any_none_of) include 14 concrete clients, stateful
+counting clients for all three algorithms, an arbitrary-input `all_of` branch
+client, and a partial-predicate client. Separate proof files allow the expensive
+checks to compile in parallel.
+
+## References
+
+- [all_of](https://eel.is/c++draft/alg.all.of)
+- [any_of](https://eel.is/c++draft/alg.any.of)
+- [none_of](https://eel.is/c++draft/alg.none.of)
+- [Overloads and examples](https://en.cppreference.com/w/cpp/algorithm/all_any_none_of)

rocq-brick-libstdcpp/proof/all_any_none_of/hints.v

@@ -0,0 +1,36 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Export skylabs.auto.cpp.prelude.proof.
+Require Export skylabs.brick.libstdcpp.all_any_none_of.pred.
+
+NES.Begin all_any_none_of.
+
+Lemma all_value_function (f : Z -> bool) xs :
+  all_value (fun x => Some (f x)) xs = Some (forallb f xs).
+Proof.
+  unfold all_value.
+  induction xs as [|x xs IH]; simpl; first reflexivity.
+  destruct (f x); simpl in *.
+  - exact IH.
+  - reflexivity.
+Qed.
+
+Lemma any_value_function (f : Z -> bool) xs :
+  any_value (fun x => Some (f x)) xs = Some (existsb f xs).
+Proof.
+  unfold any_value.
+  induction xs as [|x xs IH]; simpl; first reflexivity.
+  destruct (f x); simpl in *.
+  - reflexivity.
+  - exact IH.
+Qed.
+
+Lemma none_value_function (f : Z -> bool) xs :
+  none_value (fun x => Some (f x)) xs = Some (negb (existsb f xs)).
+Proof. rewrite /none_value any_value_function. reflexivity. Qed.
+
+NES.End all_any_none_of.
+Import all_any_none_of.

rocq-brick-libstdcpp/proof/all_any_none_of/inc_all_any_none_of.cpp

@@ -0,0 +1,24 @@
+/**
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ */
+#include <algorithm>
+
+namespace {
+
+bool aanof_pred(unsigned char b) { return b != 0; }
+
+[[maybe_unused]] inline bool force_all_of(const unsigned char* first, const unsigned char* last) {
+  return std::all_of(first, last, &aanof_pred);
+}
+
+[[maybe_unused]] inline bool force_any_of(const unsigned char* first, const unsigned char* last) {
+  return std::any_of(first, last, &aanof_pred);
+}
+
+[[maybe_unused]] inline bool force_none_of(const unsigned char* first, const unsigned char* last) {
+  return std::none_of(first, last, &aanof_pred);
+}
+
+}  // namespace

rocq-brick-libstdcpp/proof/all_any_none_of/model.v

@@ -0,0 +1,54 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.prelude.base.
+Require Import skylabs.prelude.list_numbers.
+Require Import elpi.apps.NES.NES.
+
+#[local] Open Scope Z_scope.
+
+NES.Begin all_any_none_of.
+
+(* [None] permits either predicate result. *)
+Definition all_value (test : Z -> option bool) (xs : list Z) : option bool :=
+  if existsb (fun x => bool_decide (test x = Some false)) xs then Some false
+  else if forallb (fun x => bool_decide (test x = Some true)) xs then Some true
+  else None.
+
+Definition any_value (test : Z -> option bool) (xs : list Z) : option bool :=
+  if existsb (fun x => bool_decide (test x = Some true)) xs then Some true
+  else if forallb (fun x => bool_decide (test x = Some false)) xs then Some false
+  else None.
+
+Definition none_value (test : Z -> option bool) (xs : list Z) : option bool :=
+  negb <$> any_value test xs.
+
+Succeed Example empty_all : all_value (fun _ => None) [] = Some true := eq_refl.
+Succeed Example empty_any : any_value (fun _ => None) [] = Some false := eq_refl.
+Succeed Example empty_none : none_value (fun _ => None) [] = Some true := eq_refl.
+Succeed Example high_bytes_all :
+  all_value (fun x => Some (bool_decide (128 <= x))) [128; 255] = Some true := eq_refl.
+Succeed Example mixed_all :
+  all_value (fun x => Some (bool_decide (x <> 0))) [128; 0; 255] = Some false := eq_refl.
+Succeed Example mixed_any :
+  any_value (fun x => Some (bool_decide (x <> 0))) [128; 0; 255] = Some true := eq_refl.
+Succeed Example zero_none :
+  none_value (fun x => Some (bool_decide (x <> 0))) [0; 0] = Some true := eq_refl.
+Succeed Example singleton_all :
+  all_value (fun x => Some (bool_decide (x <> 0))) [0] = Some false := eq_refl.
+Succeed Example singleton_any :
+  any_value (fun x => Some (bool_decide (x <> 0))) [7] = Some true := eq_refl.
+Succeed Example singleton_none :
+  none_value (fun x => Some (bool_decide (x <> 0))) [7] = Some false := eq_refl.
+Succeed Example low_bytes_any :
+  any_value (fun x => Some (bool_decide (128 <= x))) [0; 127] = Some false := eq_refl.
+Succeed Example unknown_all : all_value (fun _ => None) [0] = None := eq_refl.
+Succeed Example unknown_any : any_value (fun _ => None) [0] = None := eq_refl.
+Succeed Example partial_all :
+  all_value (fun x => if bool_decide (x = 0) then Some false else None) [7; 0] = Some false := eq_refl.
+Succeed Example partial_any :
+  any_value (fun x => if bool_decide (x = 0) then None else Some true) [0; 7] = Some true := eq_refl.
+
+NES.End all_any_none_of.

rocq-brick-libstdcpp/proof/all_any_none_of/pred.v

@@ -0,0 +1,26 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.auto.cpp.specs.
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Export skylabs.brick.libstdcpp.all_any_none_of.model.
+
+NES.Begin all_any_none_of.
+
+(* [state k] describes the predicate's separate resources after [k] calls. *)
+#[global] Abbreviation predicate_spec xs test I :=
+  ((fun (values : list Z) (accepts : Z -> option bool) (state : Z -> mpred) =>
+    unmaterialized_fspec (tFunction Tbool [Tuchar])
+      (\with (k : Z)
+       \arg{x} "b" (Vint x)
+       \require (0 <= k)%Z
+       \require (k < lengthZ values)%Z
+       \require x ∈ values
+       \pre state k
+       \post{r : bool}[Vbool r] state (k + 1)%Z **
+         match accepts x with Some b => [| r = b |] | None => emp end))
+    xs test I) (only parsing).
+
+NES.End all_any_none_of.

rocq-brick-libstdcpp/proof/all_any_none_of/spec.v

@@ -0,0 +1,75 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.auto.cpp.specs.
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Export skylabs.brick.libstdcpp.all_any_none_of.hints.
+Require Import skylabs.brick.libstdcpp.all_any_none_of.inc_all_any_none_of_cpp.
+
+(* C++20 non-policy instantiations for const unsigned char* iterators and a
+   bool(unsigned char) function pointer. The selected bytes are preserved.
+   [test x = None] leaves that callback result unspecified. [I k] tracks
+   separate predicate state and exposes at most [length xs] calls, without
+   specifying visited positions, order, exact count, or short-circuiting. *)
+NES.Open all_any_none_of.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "std::all_of<const unsigned char*, bool (*)(unsigned char)>(const unsigned char*, const unsigned char*, bool (*)(unsigned char))"
+    as all_of_spec from inc_all_any_none_of_cpp.source with
+    (\arg{first} "__first" (Vptr first)
+     \with (n : Z)
+     \arg "__last" (Vptr (first .[ Tuchar ! n ]))
+     \arg{pred} "__pred" (Vptr pred)
+     \prepost{q xs} first |-> array_sliceR Tuchar 0 n (fun x => ucharR q x) xs
+     \with (test : Z -> option bool) (I : Z -> mpred)
+     \prepost pred |-> cptrR (predicate_spec xs test I)
+     \pre I 0%Z
+     \post{r : bool}[Vbool r]
+       Exists k : Z, [| (0 <= k <= lengthZ xs)%Z |] ** I k **
+         match all_value test xs with
+         | Some b => [| r = b |]
+         | None => emp
+         end).
+
+  cpp.spec "std::any_of<const unsigned char*, bool (*)(unsigned char)>(const unsigned char*, const unsigned char*, bool (*)(unsigned char))"
+    as any_of_spec from inc_all_any_none_of_cpp.source with
+    (\arg{first} "__first" (Vptr first)
+     \with (n : Z)
+     \arg "__last" (Vptr (first .[ Tuchar ! n ]))
+     \arg{pred} "__pred" (Vptr pred)
+     \prepost{q xs} first |-> array_sliceR Tuchar 0 n (fun x => ucharR q x) xs
+     \with (test : Z -> option bool) (I : Z -> mpred)
+     \prepost pred |-> cptrR (predicate_spec xs test I)
+     \pre I 0%Z
+     \post{r : bool}[Vbool r]
+       Exists k : Z, [| (0 <= k <= lengthZ xs)%Z |] ** I k **
+         match any_value test xs with
+         | Some b => [| r = b |]
+         | None => emp
+         end).
+
+  cpp.spec "std::none_of<const unsigned char*, bool (*)(unsigned char)>(const unsigned char*, const unsigned char*, bool (*)(unsigned char))"
+    as none_of_spec from inc_all_any_none_of_cpp.source with
+    (\arg{first} "__first" (Vptr first)
+     \with (n : Z)
+     \arg "__last" (Vptr (first .[ Tuchar ! n ]))
+     \arg{pred} "__pred" (Vptr pred)
+     \prepost{q xs} first |-> array_sliceR Tuchar 0 n (fun x => ucharR q x) xs
+     \with (test : Z -> option bool) (I : Z -> mpred)
+     \prepost pred |-> cptrR (predicate_spec xs test I)
+     \pre I 0%Z
+     \post{r : bool}[Vbool r]
+       Exists k : Z, [| (0 <= k <= lengthZ xs)%Z |] ** I k **
+         match none_value test xs with
+         | Some b => [| r = b |]
+         | None => emp
+         end).
+
+  Definition specs := all_of_spec ** any_of_spec ** none_of_spec.
+  #[global] Hint Opaque specs : typeclass_instances sl_opacity.
+  #[only(knowledge)] derive specs.
+End with_cpp.

rocq-brick-libstdcpp/proof/dune.inc

@@ -11,6 +11,18 @@
   	 (with-stderr-to inc_algorithms_cpp.v.stderr (run cpp2v -v %{input} -o inc_algorithms_cpp.v --no-elaborate --templates=inc_algorithms_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_algorithms.cpp))
 )
+(subdir all_any_none_of
+ (rule
+  (targets inc_all_any_none_of_cpp.v.stderr inc_all_any_none_of_cpp.v inc_all_any_none_of_cpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input inc_all_any_none_of.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to inc_all_any_none_of_cpp.v.stderr (run cpp2v -v %{input} -o inc_all_any_none_of_cpp.v --no-elaborate --templates=inc_all_any_none_of_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_all_any_none_of.cpp))
+)
 (subdir array
  (rule
   (targets inc_array_cpp.v.stderr inc_array_cpp.v inc_array_cpp_templates.v)

rocq-brick-libstdcpp/test/all_any_none_of/counting.cpp

@@ -0,0 +1,56 @@
+/**
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ */
+#include <algorithm>
+#include <cassert>
+
+unsigned int all_of_calls = 0;
+unsigned int any_of_calls = 0;
+unsigned int none_of_calls = 0;
+
+bool
+counted_all_nonzero(unsigned char byte) {
+    ++all_of_calls;
+    return byte != 0;
+}
+
+bool
+counted_any_nonzero(unsigned char byte) {
+    ++any_of_calls;
+    return byte != 0;
+}
+
+bool
+counted_none_nonzero(unsigned char byte) {
+    ++none_of_calls;
+    return byte != 0;
+}
+
+void
+all_of_counting_results() {
+    const unsigned char bytes[] = {1, 0, 2};
+    all_of_calls = 0;
+    const bool result = std::all_of(bytes, bytes + 3, counted_all_nonzero);
+    assert(result == false);
+    assert(all_of_calls <= 3);
+}
+
+void
+any_of_counting_results() {
+    const unsigned char bytes[] = {0, 7, 0};
+    any_of_calls = 0;
+    const bool result = std::any_of(bytes, bytes + 3, counted_any_nonzero);
+    assert(result == true);
+    assert(any_of_calls <= 3);
+}
+
+void
+none_of_counting_results() {
+    const unsigned char bytes[] = {0, 7, 0};
+    none_of_calls = 0;
+    const bool result = std::none_of(bytes, bytes + 3, counted_none_nonzero);
+    assert(result == false);
+    assert(none_of_calls <= 3);
+}