Merge pull request #7 from Progmasoft/feature/native-property-engine

Add a native property-testing engine with choice-sequence shrinking

32 files changed, 4144 insertions, 17 deletions

diff --git a/.clang-format b/.clang-format
index 907da4cb..05a21827 100644
--- a/.clang-format
+++ b/.clang-format
@@ -2,9 +2,9 @@
 # SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
 
 ---
-# Visual X# C++20 format profile, pinned to LLVM/Clang 23.1.0.
+# Progmasoft C++ Style format profile, pinned to LLVM/Clang 23.1.0.
 # Naming is intentionally outside clang-format and remains governed by the
-# existing Visual X# PascalCase/camelCase conventions.
+# PascalCase/camelCase conventions of Progmasoft C++ Style.
 Language: Cpp
 BasedOnStyle: LLVM
 Standard: c++20
diff --git a/docs/Readme.md b/docs/Readme.md
index 89995f45..d8e9730e 100644
--- a/docs/Readme.md
+++ b/docs/Readme.md
@@ -3,7 +3,8 @@
 
 Catch3 combines the upstream Catch2-compatible runner and API with
 Progmasoft's C++20 extensions. Start with the [tutorial](tutorial.md#top),
-then read [what Catch3 adds](progmasoft-catch3.md) and
+then read [what Catch3 adds](progmasoft-catch3.md),
+[native property testing](progmasoft-properties.md), [the roadmap](progmasoft-roadmap.md) and
 [why the two API families remain distinct](why-catch3.md). The compatibility
 pages below retain real `catch2/` include paths, `Catch2::` CMake targets,
 and upstream version history; renaming those would make examples incorrect.
diff --git a/docs/progmasoft-catch3.md b/docs/progmasoft-catch3.md
index 55114f32..30ea7a15 100644
--- a/docs/progmasoft-catch3.md
+++ b/docs/progmasoft-catch3.md
@@ -8,6 +8,14 @@ namespace.
 
 ## Property testing
 
+Catch3 has two property APIs. [Native property testing](progmasoft-properties.md#top)
+with `ForAll` and strategies is the full engine: every combination of
+strategies shrinks, failures replay from a token and from an example database,
+and it adds state machines, statistics, targeted search and differential and
+metamorphic oracles. New tests should use it. The value-shrinking
+`CheckProperty` API described here remains supported for existing tests.
+[The roadmap](progmasoft-roadmap.md#top) lists what comes next.
+
 `<Progmasoft/Catch3.hpp>` is the umbrella header. It brings in Catch2's
 `catch_all.hpp` as well as the Progmasoft extensions, so it is convenient but
 increases compile time. Include individual headers when a translation unit only
@@ -108,11 +116,10 @@ Invalid factory arguments, such as an empty alphabet or a minimum above its
 maximum, throw `std::invalid_argument`; a client built without exceptions
 gets the message on standard error followed by `std::abort`.
 
-State-machine commands, parallel trials, mapped or filtered generators, and
-adaptive shrinking are deliberately not implied by this module; they need
-their own deterministic contracts and tests before being added. Shrinking a
-composite value is greedy and local like scalar shrinking: it finds a small
-counterexample, not a provably smallest one.
+Mapped, filtered and dependent generators and state machines are not part of
+this module; the strategies of [native property testing](progmasoft-properties.md#top)
+provide them. Shrinking a composite value here is greedy and local like scalar
+shrinking: it finds a small counterexample, not a provably smallest one.
 
 ## Snapshots
 
diff --git a/docs/progmasoft-properties.md b/docs/progmasoft-properties.md
new file mode 100644
index 00000000..8042b85b
--- /dev/null
+++ b/docs/progmasoft-properties.md
@@ -0,0 +1,230 @@
+<a id="top"></a>
+# Native property testing
+
+`<Progmasoft/Catch3/ForAll.hpp>` is Catch3's own property-testing engine. It
+needs no third-party library. Catch2's support for RapidCheck through
+RapidCheck's own Catch integration keeps working as before, but the Progmasoft
+additions do not build on RapidCheck. The engine goes beyond it where property
+tests usually stop being practical:
+
+- **Shrinking of the recorded choices.** Every combination of strategies
+  shrinks, including `Map`, `Filter`, `FlatMap` and state machines, and a
+  shrunk input always satisfies the filters and dependencies that built it.
+- **An example database.** Failures found once are replayed first on the next
+  run, on any machine that shares the directory, until they are fixed.
+- **Targeted search.** `Target` scores guide a search towards inputs that
+  random sampling rarely reaches.
+- **Coverage requirements.** `Cover` fails a property whose inputs reach an
+  interesting case too rarely.
+- **Ready-made oracles.** `Equivalent`, `Metamorphic`, `RoundTrip` and
+  `Idempotent` check properties that need no expected result.
+- **No exceptions required.** `CATCH3_PROPERTY_ASSERT` returns from the body;
+  the engine never throws.
+
+The older `CheckProperty` and `Generator` API of
+[Progmasoft Catch3 additions](progmasoft-catch3.md#top) remains supported
+and unchanged.
+
+## A first property
+
+```cpp
+#include <Progmasoft/Catch3.hpp>
+
+using namespace Progmasoft::Catch3;
+
+TEST_CASE( "reversing twice gives the original", "[property]" ) {
+    CATCH3_CHECK_FOR_ALL(
+        Gen::Vectors( Gen::Integers<int>() ),
+        []( const std::vector<int>& values ) {
+            auto copy = values;
+            std::reverse( copy.begin(), copy.end() );
+            std::reverse( copy.begin(), copy.end() );
+            return copy == values;
+        } );
+}
+```
+
+`ForAll([options,] strategy..., body)` draws one value from each strategy and
+passes them to the body. The body returns `bool`, or returns `void` and uses
+the property macros:
+
+```cpp
+CATCH3_CHECK_FOR_ALL(
+    Gen::Integers<int>( -1000, 1000 ), Gen::Integers<int>( 1, 50 ),
+    []( int value, int divisor ) {
+        CATCH3_PROPERTY_ASSUME( value % divisor == 0 ); // otherwise discard
+        Note( "quotient", value / divisor );           // part of the report
+        CATCH3_PROPERTY_ASSERT( value / divisor * divisor == value );
+    } );
+```
+
+`CATCH3_CHECK_FOR_ALL` and `CATCH3_REQUIRE_FOR_ALL` report through Catch2's
+normal assertion path. `ForAll` itself returns a `PropertyResult` for code
+that wants to inspect it. Catch2's own `CHECK` and `REQUIRE` should not be
+used inside a property body: the engine runs the body many times while it
+shrinks, and every run would be reported.
+
+## Strategies
+
+A `Strategy<T>` builds values of `T`. All strategies live in
+`Progmasoft::Catch3::Gen`:
+
+| Strategy | Values | Shrinks towards |
+| --- | --- | --- |
+| `Integers<T>(min, max)` | integers of the range | the value closest to zero |
+| `Booleans()` | `true`, `false` | `false` |
+| `Floats<T>(FloatOptions)` | finite values of the range; NaN and infinities on request | zero or the bound closest to it, then integral values |
+| `Characters(alphabet)`, `PrintableCharacters()` | characters | the first character of the alphabet |
+| `Strings(character, range)`, `Utf8Strings(range, min, max)` | byte strings; UTF-8 text without surrogates | shorter text, simpler characters |
+| `Vectors(element, range)`, `UniqueVectors`, `Sets`, `Maps` | collections | fewer and simpler elements |
+| `Optionals(value)` | `std::nullopt` or a value | `std::nullopt` |
+| `Tuples(a, b, ...)`, `Construct<T>(a, b, ...)` | tuples, and objects built with braces | each component |
+| `Permutations(values)` | orderings of a list | the original order |
+| `Just(value)`, `SampledFrom(values)` | fixed values | the first value |
+| `OneOf(a, b, ...)`, `Frequency({ {weight, strategy}, ... })` | one of several strategies | the first strategy |
+| `Lazy(factory)`, `Recursive(base, extend, depth)` | self-referential and recursive structures | a leaf |
+
+Every strategy has `Map(function)`, `Filter(predicate)` and
+`FlatMap(function)`. `FlatMap` draws a value and then a second strategy that
+depends on it, for example a size and then a vector of exactly that size.
+
+A `SizeRange{ minimum, maximum }` bounds a collection. Without a maximum the
+length grows with the size of the trial, which rises from 0 to 100 over the
+first half of the trials, so the first trials try small inputs.
+
+## How shrinking works
+
+Each strategy builds its value from a sequence of choices, small integers that
+a `ChoiceSource` hands out. During a trial the engine records them. When a
+trial fails, the engine does not shrink the value; it shrinks the recorded
+choices and replays them through the same strategies. Choice 0 is always the
+simplest decision, and a shorter sequence is simpler than a longer one. Five
+passes repeat until none helps or `MaxShrinkSteps` replays are used:
+
+1. delete blocks of 16, 8, 4, 2 and 1 choices, which drops collection
+   elements and command steps;
+2. set blocks to zero;
+3. lower each choice by binary search, then by single steps for conditions
+   that are not monotone;
+4. swap neighbours that are out of order;
+5. move a unit from a choice to a later one, for sums such as `x + y > 10`.
+
+Because the strategies are replayed, the shrunk input is always one the
+strategies can produce: a filter is still satisfied, a dependent size still
+matches its vector, a state machine still respects its preconditions. That is
+the difference from shrinking values directly.
+
+The report shows the minimized input, the reason, the notes, and a replay
+token:
+
+```text
+property failed after 37 trials; failing trial 37, root seed 3359259219, shrink checks 112
+counterexample: { 0, 100 }
+reason: property returned false
+replay: set PropertyOptions::Replay to "c3.3c.0-0-2s"
+```
+
+Setting `PropertyOptions::Replay` to the token runs exactly that input once,
+without trials or shrinking.
+
+## Options
+
+| Field | Default | Meaning |
+| --- | --- | --- |
+| `Trials` | 100 | valid trials to run |
+| `Seed` | fixed | root seed; every trial derives its own seed from it |
+| `MaxShrinkSteps` | 1000 | replays the shrinker may use |
+| `Replay` | none | run only the input of a replay token |
+| `MaxDiscardRatio` | 10 | discarded trials allowed per requested trial before the property gives up |
+| `TargetSteps` | 500 | steps of targeted search when the body calls `Target` |
+| `DatabasePath` | none | directory of the example database; otherwise `CATCH3_PROPERTY_DATABASE` |
+| `Name` | test name and line | names the property in the database |
+| `ShowStatistics` | false | adds the `Classify` and `Cover` counts to a passing report |
+
+## Statistics and coverage requirements
+
+`Classify(condition, label)` counts how often a condition held. `Cover(percent,
+condition, label)` also requires a percentage: a property whose inputs rarely
+reach an interesting case fails with `kInsufficientCoverage` instead of
+passing on easy inputs.
+
+```cpp
+Cover( 10.0, values.empty(), "empty" );
+Cover( 30.0, values.size() > 10, "long" );
+```
+
+## Targeted search
+
+`Target(score, label)` reports a score. After the regular trials the engine
+takes the highest-scoring input of each label and mutates its choices one at a
+time, keeping a mutation when the score rises. Inputs that random sampling
+almost never reaches, such as a long chain of operations or a value near an
+overflow, become reachable when a score measures the distance to them.
+
+## The example database
+
+With `DatabasePath`, or the `CATCH3_PROPERTY_DATABASE` environment variable,
+the engine stores the replay token of every minimized failure in a file named
+after the property. The next run replays those tokens before any new trial, so
+a failure found once, on any machine that shares the directory, is checked
+first until it is fixed; a stored example that passes is removed. The engine
+never fails a test because the directory is missing or unwritable.
+
+## Model-based testing
+
+`<Progmasoft/Catch3/Stateful.hpp>` runs random sequences of commands against a
+model and the system under test side by side:
+
+```cpp
+using Model = std::deque<int>;
+
+Command<Model, Queue> push{
+    "push",
+    []( const Model& ) {
+        return Gen::Integers<int>( 0, 100 ).Map( []( int value ) {
+            return Action<Model, Queue>{
+                "push(" + std::to_string( value ) + ")",
+                [value]( Model& model, Queue& queue ) {
+                    model.push_back( value );
+                    queue.Push( value );
+                    CATCH3_PROPERTY_ASSERT( queue.Size() == model.size() );
+                } };
+        } );
+    } };
+
+const auto result = CheckStateful<Model, Queue>(
+    options, [] { return Model{}; },
+    []( const Model& ) { return Queue{}; },
+    { push, pop } );
+```
+
+A command builds its action from the current model, so arguments can depend on
+the state, and its precondition decides whether it may run. A failing sequence
+shrinks to fewer steps with simpler arguments; the report lists the steps, for
+example `{ push(0), push(0), push(0), push(0) }`.
+
+## Ready-made oracles
+
+`<Progmasoft/Catch3/Relations.hpp>` provides bodies for properties that need
+no specification of the expected result:
+
+| Body | Checks |
+| --- | --- |
+| `Equivalent(reference, candidate)` | differential testing: both return the same result |
+| `Metamorphic(function, transform, relation)` | `relation(f(x), f(transform(x)))` |
+| `RoundTrip(encode, decode)` | `decode(encode(x)) == x` |
+| `Idempotent(function)` | `f(f(x)) == f(x)` |
+
+```cpp
+CATCH3_CHECK_FOR_ALL( Gen::Vectors( Gen::Integers<int>() ),
+                      Equivalent( ReferenceSort, FastSort ) );
+```
+
+A mismatch reports both results as notes.
+
+## Compatibility
+
+The engine is C++20 and part of the `Progmasoft::Catch3` library target. It
+does not change Catch2's runner, reporters, command line, or the `Catch`
+namespace, and it needs no exceptions: a client built without them gets the
+same results, except that an exception thrown by a body cannot be caught.
diff --git a/docs/progmasoft-roadmap.md b/docs/progmasoft-roadmap.md
new file mode 100644
index 00000000..4b18a6c7
--- /dev/null
+++ b/docs/progmasoft-roadmap.md
@@ -0,0 +1,90 @@
+<a id="top"></a>
+# Catch3 roadmap
+
+Catch3 grows from a Catch2-compatible test framework into a testing toolkit:
+unit testing, property testing, mocking, coverage, mutation testing, test
+generation and test selection, driven by a runner of its own. Two rules hold
+for every step:
+
+- **Catch2 stays compatible.** The `Catch` namespace, the `catch2/` headers,
+  the macros, the command line and the reporters keep working unchanged. New
+  capabilities live under `Progmasoft::Catch3` and `Progmasoft/Catch3/`.
+- **Nothing is claimed before it is tested.** A feature is listed as done when
+  its tests run in CI on Windows, Linux and macOS.
+
+The steps are ordered by what each one builds on.
+
+| Step | Capability | State |
+| --- | --- | --- |
+| 1 | Native property testing: choice-sequence shrinking, combinators, state machines, statistics, targeted search, example database, differential and metamorphic oracles | done; see [Native property testing](progmasoft-properties.md#top) |
+| 2 | The `catch3` runner | planned |
+| 3 | Mocking | planned |
+| 4 | Per-test code coverage | planned |
+| 5 | Change-impact test selection and test prioritization | planned |
+| 6 | Mutation testing | planned |
+| 7 | Coverage-, mutation- and history-guided test generation | planned |
+
+## 2. The `catch3` runner
+
+Catch2's runner executes the tests of one binary in one process. The features
+that follow need more: they run many binaries, each test in isolation, under
+coverage or mutation, and decide which tests to run and in which order. The
+`catch3` runner is a separate program that drives Catch2 test binaries from
+the outside, so existing binaries need no change:
+
+- it discovers test cases with `--list-tests --reporter json` and runs them
+  with `--reporter json`, both stable parts of Catch2's command line;
+- it runs tests in parallel processes, shards them across machines, enforces
+  per-test timeouts, isolates crashes, and retries flaky tests with a record
+  of every attempt;
+- it keeps a history of results and durations, the input for prioritization;
+- it writes JUnit XML, JSON and a terminal report, and keeps Catch2's exit
+  codes;
+- its command line is parsed by a hand-written, typed parser, like the other
+  Progmasoft tools.
+
+## 3. Mocking
+
+Mocks that report through Catch2's assertion path: expectations with call
+counts, argument matchers built on Catch2's matchers, sequences, and actions,
+for virtual interfaces and for free functions behind a seam. Unexpected calls
+and unmet expectations fail the test case that owns the mock.
+
+## 4. Per-test code coverage
+
+The runner runs each test case of an instrumented binary on its own and keeps
+one coverage profile per test: LLVM source-based coverage with Clang and GCC's
+gcov format with GCC. The result is a map from each test to the lines and
+branches it reaches, plus the usual combined report.
+
+## 5. Change-impact selection and prioritization
+
+With the per-test map, the runner selects the tests whose covered lines a
+change touches, taking the change from Git, and runs those first. Ordering
+uses failure history, duration and coverage of the change, so that a failing
+run fails early. A full run remains one option away, and the selection is
+reported, never silent.
+
+## 6. Mutation testing
+
+The runner makes small changes to the code under test, such as a flipped
+comparison or a removed call, rebuilds, and runs the tests that cover the
+changed line. A mutation that no test detects points at a missing assertion.
+The per-test coverage map keeps this affordable: only covering tests run for
+each mutant.
+
+## 7. Test generation
+
+The property engine already records choice sequences. Test generation feeds
+those sequences from three sources:
+
+- **coverage-guided:** choice sequences that reach new coverage are kept and
+  mutated further, as a fuzzer keeps inputs, so property tests explore code
+  that random inputs miss;
+- **mutation-guided:** inputs are searched for that tell a surviving mutant
+  from the original program, and become new regression examples;
+- **incremental:** examples found in earlier runs, kept in the example
+  database, seed the next run, so the search continues where it stopped.
+
+Generated examples are written as ordinary Catch2 test cases or stored replay
+tokens, so they run without the generator.
diff --git a/docs/why-catch3.md b/docs/why-catch3.md
index 8c900ac7..9be7a5f7 100644
--- a/docs/why-catch3.md
+++ b/docs/why-catch3.md
@@ -15,19 +15,19 @@ Catch2 runner.
 
 | Area | Catch2 compatibility engine | Progmasoft Catch3 additions |
 | --- | --- | --- |
-| Test execution | Catch2's existing runner, reporters, command-line interface, and test registration | `CATCH3_CHECK_PROPERTY` reports property outcomes through Catch2's assertion path |
+| Test execution | Catch2's existing runner, reporters, command-line interface, and test registration | `CATCH3_CHECK_FOR_ALL` and `CATCH3_CHECK_PROPERTY` report property outcomes through Catch2's assertion path |
 | Public include path | Existing `catch2/...` headers | `Progmasoft/Catch3.hpp` and focused `Progmasoft/Catch3/...` headers |
 | C++ baseline | Existing Catch2 target remains at C++14 | The added property API requires C++20 |
 | Randomness | Catch2's existing behavior is unchanged | A specified SplitMix64 sequence provides deterministic trial seeds and unbiased bounded integer sampling |
-| Generated values | No change to existing Catch2 generators | Initial integer/boolean strategies, custom generator callbacks, and bounded greedy shrinking |
+| Generated values | No change to existing Catch2 generators | Strategies for numbers, text, collections and structures with `Map`, `Filter` and `FlatMap`; shrinking of recorded choices, so every combination shrinks; replay tokens and an example database; state machines, `Classify`/`Cover` statistics, targeted search, and differential and metamorphic oracles |
 | Build identity | Existing `Catch2` target and APIs remain available | Separate `Progmasoft::Catch3` CMake target and `//src/Progmasoft:catch3` Bazel target |
 | Source terms | Catch2-originated source retains its upstream BSL-1.0 terms | Progmasoft-authored additions state their own SPDX license in each file |
 
-The current property runner handles one generated value per property. Shrinking
-is deterministic and bounded, but greedy rather than globally minimal. There is
-not yet built-in support for state-machine properties, mapped or filtered generators,
-discard/classification policies, parallel execution, or a standalone Catch3
-runner. Those features are not implied by the initial API.
+Properties take any number of generated values. Shrinking is deterministic and
+bounded, but local rather than globally minimal. Parallel trials and a
+standalone Catch3 runner do not exist yet; [the roadmap](progmasoft-roadmap.md#top)
+orders them with mocking, per-test coverage, test selection, mutation testing
+and test generation.
 
 ## Compatibility policy
 
diff --git a/premake5.lua b/premake5.lua
index ca773a60..7b5b1835 100644
--- a/premake5.lua
+++ b/premake5.lua
@@ -62,6 +62,9 @@ project "ProgmasoftCatch3"
     targetdir "build/premake/bin/%{cfg.buildcfg}"
     objdir "build/premake/obj/ProgmasoftCatch3/%{cfg.buildcfg}"
     files {
+        "src/Progmasoft/ChoiceShrinker.cpp",
+        "src/Progmasoft/Context.cpp",
+        "src/Progmasoft/PropertyEngine.cpp",
         "src/Progmasoft/Results.cpp",
         "src/Progmasoft/Results.hpp",
         "src/Progmasoft/Snapshot.cpp",
@@ -83,8 +86,11 @@ project "ProgmasoftPropertyTests"
     files {
         "tests/Progmasoft/Generators.tests.cpp",
         "tests/Progmasoft/Property.tests.cpp",
+        "tests/Progmasoft/ForAll.tests.cpp",
         "tests/Progmasoft/Results.tests.cpp",
         "tests/Progmasoft/Snapshot.tests.cpp",
+        "tests/Progmasoft/Stateful.tests.cpp",
+        "tests/Progmasoft/Strategy.tests.cpp",
         "src/Progmasoft/**.hpp",
     }
     includedirs { "src", generated_include }
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5eec18e9..cc3af6e7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -363,6 +363,9 @@ add_library(Catch2::Catch2 ALIAS Catch2)
 # Progmasoft's compiled C++20 utilities are separate from Catch2's
 # compatibility engine, which retains its existing C++14 baseline.
 add_library(ProgmasoftCatch3 STATIC
+  "${CATCH_DIR}/src/Progmasoft/ChoiceShrinker.cpp"
+  "${CATCH_DIR}/src/Progmasoft/Context.cpp"
+  "${CATCH_DIR}/src/Progmasoft/PropertyEngine.cpp"
   "${CATCH_DIR}/src/Progmasoft/Results.cpp"
   "${CATCH_DIR}/src/Progmasoft/Snapshot.cpp"
   "${CATCH_DIR}/src/Progmasoft/XmlWriter.cpp"
diff --git a/src/Progmasoft/BUILD.bazel b/src/Progmasoft/BUILD.bazel
index 14a67bf6..b053c277 100644
--- a/src/Progmasoft/BUILD.bazel
+++ b/src/Progmasoft/BUILD.bazel
@@ -7,6 +7,9 @@ package(default_visibility = ["//visibility:public"])
 cc_library(
     name = "catch3",
     srcs = [
+        "ChoiceShrinker.cpp",
+        "Context.cpp",
+        "PropertyEngine.cpp",
         "Results.cpp",
         "Snapshot.cpp",
         "XmlWriter.cpp",
@@ -16,6 +19,7 @@ cc_library(
         "Catch3/Assertions.hpp",
         "Catch3/Detail/InvalidArgument.hpp",
         "Catch3/Detail/Sequence.hpp",
+        "Catch3/ForAll.hpp",
         "Catch3/Generator.hpp",
         "Catch3/Generators/Boolean.hpp",
         "Catch3/Generators/Element.hpp",
@@ -25,8 +29,16 @@ cc_library(
         "Catch3/Generators/Vector.hpp",
         "Catch3/Property.hpp",
         "Catch3/Random.hpp",
+        "Catch3/Relations.hpp",
         "Catch3/Results.hpp",
         "Catch3/Snapshot.hpp",
+        "Catch3/Stateful.hpp",
+        "Catch3/Strategy/ChoiceSource.hpp",
+        "Catch3/Strategy/Containers.hpp",
+        "Catch3/Strategy/Context.hpp",
+        "Catch3/Strategy/Engine.hpp",
+        "Catch3/Strategy/Numeric.hpp",
+        "Catch3/Strategy/Strategy.hpp",
         "Catch3/XmlWriter.hpp",
     ],
     copts = select({
diff --git a/src/Progmasoft/Catch3.hpp b/src/Progmasoft/Catch3.hpp
index 5fca369a..a1db1db7 100644
--- a/src/Progmasoft/Catch3.hpp
+++ b/src/Progmasoft/Catch3.hpp
@@ -6,6 +6,7 @@
 #include <catch2/catch_all.hpp>
 
 #include <Progmasoft/Catch3/Assertions.hpp>
+#include <Progmasoft/Catch3/ForAll.hpp>
 #include <Progmasoft/Catch3/Generator.hpp>
 #include <Progmasoft/Catch3/Generators/Boolean.hpp>
 #include <Progmasoft/Catch3/Generators/Element.hpp>
@@ -15,6 +16,13 @@
 #include <Progmasoft/Catch3/Generators/Vector.hpp>
 #include <Progmasoft/Catch3/Property.hpp>
 #include <Progmasoft/Catch3/Random.hpp>
+#include <Progmasoft/Catch3/Relations.hpp>
 #include <Progmasoft/Catch3/Results.hpp>
 #include <Progmasoft/Catch3/Snapshot.hpp>
+#include <Progmasoft/Catch3/Stateful.hpp>
+#include <Progmasoft/Catch3/Strategy/ChoiceSource.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <Progmasoft/Catch3/Strategy/Numeric.hpp>
+#include <Progmasoft/Catch3/Strategy/Strategy.hpp>
 #include <Progmasoft/Catch3/XmlWriter.hpp>
diff --git a/src/Progmasoft/Catch3/Assertions.hpp b/src/Progmasoft/Catch3/Assertions.hpp
index 668c086d..61fef04a 100644
--- a/src/Progmasoft/Catch3/Assertions.hpp
+++ b/src/Progmasoft/Catch3/Assertions.hpp
@@ -5,8 +5,14 @@
 #include <catch2/catch_message.hpp>
 #include <catch2/catch_test_macros.hpp>
 
+#include <catch2/interfaces/catch_interfaces_capture.hpp>
+
+#include <Progmasoft/Catch3/ForAll.hpp>
 #include <Progmasoft/Catch3/Property.hpp>
 #include <Progmasoft/Catch3/Snapshot.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+
+#include <string>
 
 /// Runs a property and reports its replay seed and minimized counterexample.
 #define CATCH3_CHECK_PROPERTY( ... )                            \
@@ -25,3 +31,30 @@
         INFO( catch3SnapshotResult.Message );                               \
         CHECK( catch3SnapshotResult.Succeeded() );                          \
     } while ( false )
+
+/// Runs ForAll( [options,] strategy..., body ) under the name of the
+/// current test case, which keys the example database, and reports the
+/// result through Catch2: the minimized counterexample, its notes and its
+/// replay token on failure.
+#define CATCH3_CHECK_FOR_ALL( ... )                                          \
+    do {                                                                     \
+        const ::Progmasoft::Catch3::Detail::PropertyNameScope catch3Name(    \
+            ::Catch::getResultCapture().getCurrentTestName() + ":" +         \
+            std::to_string( __LINE__ ) );                                    \
+        const auto catch3ForAllResult =                                      \
+            ::Progmasoft::Catch3::ForAll( __VA_ARGS__ );                     \
+        INFO( catch3ForAllResult.Describe() );                               \
+        CHECK( catch3ForAllResult.Succeeded() );                             \
+    } while ( false )
+
+/// As CATCH3_CHECK_FOR_ALL, but ends the test case on failure.
+#define CATCH3_REQUIRE_FOR_ALL( ... )                                        \
+    do {                                                                     \
+        const ::Progmasoft::Catch3::Detail::PropertyNameScope catch3Name(    \
+            ::Catch::getResultCapture().getCurrentTestName() + ":" +         \
+            std::to_string( __LINE__ ) );                                    \
+        const auto catch3ForAllResult =                                      \
+            ::Progmasoft::Catch3::ForAll( __VA_ARGS__ );                     \
+        INFO( catch3ForAllResult.Describe() );                               \
+        REQUIRE( catch3ForAllResult.Succeeded() );                           \
+    } while ( false )
diff --git a/src/Progmasoft/Catch3/ForAll.hpp b/src/Progmasoft/Catch3/ForAll.hpp
new file mode 100644
index 00000000..e41bfdb6
--- /dev/null
+++ b/src/Progmasoft/Catch3/ForAll.hpp
@@ -0,0 +1,191 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#pragma once
+
+#include <Progmasoft/Catch3/Property.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <Progmasoft/Catch3/Strategy/Engine.hpp>
+#include <Progmasoft/Catch3/Strategy/Strategy.hpp>
+#include <exception>