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

Catch3's own property engine, independent of RapidCheck, next to the
existing CheckProperty API, which stays unchanged.

Strategies (Progmasoft/Catch3/Strategy/): a Strategy<T> builds a value
from a ChoiceSource, a stream of integer choices where 0 is always the
simplest decision. Gen:: provides Integers, Booleans, Floats (ranges,
NaN and infinities on request, edge values), Characters, Strings,
Utf8Strings, Vectors, UniqueVectors, Sets, Maps, Optionals, Tuples,
Construct, Permutations, Just, SampledFrom, OneOf, Frequency, Lazy and
Recursive; every strategy has Map, Filter and FlatMap.

Shrinking: the engine records the choices of a failing trial and
shrinks them, not the value, with deletion and zeroing of blocks,
binary search per choice with a neighbour step for non-monotone
conditions, sorting and moving value between neighbours. Replaying the
shrunk choices through the same strategies means mapped, filtered,
dependent and stateful inputs all shrink, and a shrunk input still
satisfies its filters.

ForAll([options,] strategy..., body) runs the trials (size rising over
the first half), then a targeted search when the body calls Target,
then checks Cover requirements. A failure report carries the
minimized input, the notes and a replay token (PropertyOptions::Replay)
that runs exactly that input. An example database (DatabasePath or
CATCH3_PROPERTY_DATABASE) replays stored failures first and drops them
once they pass. Bodies return bool, or void with CATCH3_PROPERTY_ASSERT
and CATCH3_PROPERTY_ASSUME, which return instead of throwing; Note,
Classify, Cover and Target record into a per-thread trial record.
CATCH3_CHECK_FOR_ALL and CATCH3_REQUIRE_FOR_ALL report through Catch2
and name the property after the test case for the database.

CheckStateful runs model-based command sequences against a model and
the system under test; preconditions and state-dependent arguments are
replayed during shrinking. Relations.hpp provides Equivalent
(differential), Metamorphic, RoundTrip and Idempotent bodies.

PropertyOptions, PropertyStatus, PropertyFailure and PropertyResult
gain fields and statuses at their ends (kInsufficientCoverage,
kGaveUp); existing designated initializers and reports are unchanged.
The engine's untemplated parts are compiled in ChoiceShrinker.cpp,
PropertyEngine.cpp and Context.cpp, and every build system (Bazel,
CMake, Meson, Xmake, Premake) lists the new files and tests.

Docs: progmasoft-properties.md describes the engine,
progmasoft-roadmap.md the steps that follow (the standalone catch3
runner, mocking, per-test coverage, change-impact selection and
prioritization, mutation testing, guided test generation). The
.clang-format comment names Progmasoft C++ Style instead of Visual X#.

Verified with clang-cl 23 through CMake: ProgmasoftSelfTest passes, 57
test cases and 75,461 assertions, including the shrinking results
(1001 for x <= 1000, { 10 }, { 0, 0, 0 } through FlatMap, 102 through
a filter, { 0, 100 } for two arguments, four push(0) steps for a
queue that drops its fourth element, { 0, 0 } for a sort that loses
duplicates) and the database, replay, coverage and discard behaviour.

5 files changed, 341 insertions, 13 deletions

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