Document proptest support for property tests

docs/build/guides/testing/fuzzing.mdx

@@ -7,7 +7,7 @@ sidebar_position: 7
 
 Fuzzing is the process of providing random data to programs to identify unexpected behavior, such as crashes and panics.
 
-Fuzz tests can also be written as property tests that instead of seeking to identify panics and crashes, assert on some property remaining true. Fuzzing as demonstrated here and elsewhere in these docs will use principles from both property testing and fuzzing, but will only use the term fuzzing to refer to both.
+This page covers fuzz testing, primarily with `cargo-fuzz`. Property testing with `proptest` is a related but distinct approach: it also generates random input, but runs as ordinary tests under `cargo test` and asserts that some property holds, rather than only searching for crashes and panics. See [How to Write Property Tests](#how-to-write-property-tests) below.
 
 The following steps can be used in any Stellar contract workspace. If experimenting, try them in the [increment example]. The contract has an `increment` function that increases a counter value by one on every invocation.
 
@@ -163,6 +163,59 @@ To measure code coverage of regular Rust tests, see [Code Coverage].
 
 :::
 
+## How to Write Property Tests
+
+Property tests, like fuzz tests, exercise a contract with randomly generated input, but they run as ordinary `#[test]`s under `cargo test`. No nightly toolchain, no separate fuzz crate, and no special runner are required.
+
+1. Add the `proptest` and `proptest-arbitrary-interop` crates as dev-dependencies of the contract crate.
+
+   ```toml
+   [dev-dependencies]
+   proptest = "1"
+   proptest-arbitrary-interop = "0.1"
+   ```
+
+2. Soroban contract types can only be constructed from an `Env`, which a `proptest` strategy doesn't have access to, so contract types are generated the same way as for fuzzing: through the `SorobanArbitrary::Prototype` pattern (see [Accepting Soroban Types as Input with the `SorobanArbitrary` Trait]). But `proptest` generates values from `Strategy`s, not from `Arbitrary` implementations, so it cannot consume a `Prototype` directly. The [proptest-arbitrary-interop] crate's `arb` function bridges the gap, turning any `Arbitrary` type, including every `SorobanArbitrary::Prototype`, into a `Strategy`.
+
+   The pattern mirrors the fuzz test pattern: generate the prototype with `arb::<<T as SorobanArbitrary>::Prototype>()`, then convert it to the real, `Env`-hosted contract type with `.into_val(&env)` inside the test body, where an `Env` is available.
+
+3. Write the property test. For example, generating an `Address`:
+
+   ```rust
+   use proptest::prelude::*;
+   use proptest_arbitrary_interop::arb;
+   use soroban_sdk::testutils::arbitrary::SorobanArbitrary;
+   use soroban_sdk::{Address, Env, IntoVal};
+
+   proptest! {
+       #[test]
+       fn test_deposit(
+           address_proto in arb::<<Address as SorobanArbitrary>::Prototype>(),
+           deposit_amount in 0i128..=i128::MAX,
+       ) {
+           let env = Env::default();
+           let address: Address = address_proto.into_val(&env);
+           // call the contract with `address` and `deposit_amount`
+       }
+   }
+   ```
+
+   Generated `Address` prototypes always convert to contract addresses, never to account (`G...`) addresses. A property test that also needs account addresses must construct them itself with `Address::from_str`.
+
+4. Run it like any other test.
+
+   ```text
+   cargo test
+   ```
+
+:::info
+
+Shrinking is degraded across this bridge. When a property test fails, `proptest` tries to shrink the failing input to a smaller, simpler one, but it does so by truncating the generated bytes and rebuilding a new value from them, rather than shrinking the value itself. As a result, the "shrunk" failing input `proptest` reports is generally a different input, not a smaller version of the first one that failed.
+
+:::
+
+See the [SorobanArbitrary proptest module] for the full reference documentation, including a second example that generates a custom `#[contracttype]` struct.
+
 [increment example]: https://github.com/stellar/soroban-examples/blob/main/increment/src/lib.rs
 [Differential Testing with Test Snapshots]: ./differential-tests-with-test-snapshots.mdx
 [stellar contract fetch]: ../../../tools/cli/stellar-cli.mdx#stellar-contract-fetch
@@ -173,3 +226,6 @@ To measure code coverage of regular Rust tests, see [Code Coverage].
 [Rust Fuzz Book]: https://rust-fuzz.github.io/book
 [Code Coverage]: code-coverage.mdx
 [Coverage Gutters]: https://marketplace.visualstudio.com/items?itemName=ryanluker.vscode-coverage-gutters
+[proptest-arbitrary-interop]: https://docs.rs/proptest-arbitrary-interop
+[SorobanArbitrary proptest module]: https://docs.rs/soroban-sdk/latest/soroban_sdk/testutils/proptest/index.html
+[Accepting Soroban Types as Input with the `SorobanArbitrary` Trait]: ../../smart-contracts/example-contracts/fuzzing.mdx#accepting-soroban-types-as-input-with-the-sorobanarbitrary-trait

docs/build/smart-contracts/example-contracts/fuzzing.mdx

@@ -778,6 +778,16 @@ Property tests are similar to fuzz tests in that they generate randomized input.
 
 The great benefit of property tests though is that they can be included in standard Rust test suites and require no extra tooling to execute. One might take advantage of this by interactively fuzzing to discover deep bugs, then convert fuzz tests to property tests to help prevent regressions.
 
-The [`proptest.rs`] file is a translation of `fuzz_target_1.rs` to a property test.
+The bridge works because `proptest` generates values from `Strategy`s, not from `Arbitrary` implementations directly. The [`proptest-arbitrary-interop`] crate's `arb` function converts any `Arbitrary` type into a `Strategy`, and since every `SorobanArbitrary::Prototype` implements `Arbitrary`, the same prototype values used for fuzzing above can feed a property test directly.
+
+:::info
+
+Shrinking is degraded across this bridge: `proptest`'s shrinker truncates the generated bytes and rebuilds a new value from them, rather than shrinking the value itself, so a "shrunk" failing input is generally a different failing input, not a smaller version of the first one that failed.
+
+:::
+
+The [`proptest.rs`] file is a translation of `fuzz_target_1.rs` to a property test. For a general how-to on writing property tests, see [How to Write Property Tests], and for the full API reference, see the [SorobanArbitrary proptest module].
 
 [`proptest.rs`]: https://github.com/stellar/soroban-examples/tree/v23.0.0/fuzzing/src/proptest.rs
+[How to Write Property Tests]: ../../guides/testing/fuzzing.mdx#how-to-write-property-tests
+[SorobanArbitrary proptest module]: https://docs.rs/soroban-sdk/latest/soroban_sdk/testutils/proptest/index.html