feat(contracts/ci/docs): property testing, fuzz targets, runbooks, WASM size tracking

.github/workflows/test.yml

@@ -563,6 +563,12 @@ jobs:
         run: cargo build --target wasm32-unknown-unknown --release
         working-directory: contracts/predict-iq
 
+      - name: Print unoptimized WASM size
+        run: |
+          size=$(wc -c < target/wasm32-unknown-unknown/release/predict_iq.wasm)
+          echo "Unoptimized WASM size: $size bytes (budget: ${{ env.WASM_SIZE_LIMIT_BYTES }} bytes)"
+        working-directory: contracts/predict-iq
+
       - name: Optimize WASM
         run: |
           soroban contract optimize \
@@ -580,6 +586,36 @@ jobs:
           fi
         working-directory: contracts/predict-iq
 
+  contract-fuzz:
+    name: Contract Fuzz Tests (libFuzzer, 60 s per target)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install nightly Rust + cargo-fuzz
+        run: |
+          rustup toolchain install nightly
+          cargo +nightly install cargo-fuzz
+
+      - name: Fuzz fuzz_place_bet
+        run: cargo +nightly fuzz run fuzz_place_bet -- -max_total_time=60
+        working-directory: contracts/predict-iq
+
+      - name: Fuzz fuzz_resolve_market
+        run: cargo +nightly fuzz run fuzz_resolve_market -- -max_total_time=60
+        working-directory: contracts/predict-iq
+
+      - name: Fuzz fuzz_withdraw
+        run: cargo +nightly fuzz run fuzz_withdraw -- -max_total_time=60
+        working-directory: contracts/predict-iq
+
+      - name: Upload crash artifacts
+        if: failure()
+        uses: actions/upload-artifact@v4
+        with:
+          name: fuzz-crashes
+          path: contracts/predict-iq/fuzz/artifacts/
+
   api-cache-tests:
     name: API Cache Tests (Redis)
     runs-on: ubuntu-latest

CHANGELOG.md

@@ -1,3 +1,18 @@
+## [Unreleased]
+
+### Contract WASM Size Tracking
+
+Size is measured on the optimized binary produced by `soroban contract optimize`.
+The CI `build-optimized` job prints both unoptimized and optimized sizes on every
+build so contributors can track the trend. The enforced budget is **65,536 bytes**
+(64 KB), configured as `WASM_SIZE_LIMIT_BYTES` in `.github/workflows/test.yml`.
+
+| Release | Optimized WASM size |
+|---------|---------------------|
+| v1.0.1  | (tracking begins — run `cargo build --target wasm32-unknown-unknown --release` and `soroban contract optimize` locally to measure) |
+
+---
+
 ## [1.0.1](https://github.com/popsman01/predictIQ/compare/v1.0.0...v1.0.1) (2026-05-27)
 
 

contracts/predict-iq/Cargo.toml

@@ -14,6 +14,7 @@ soroban-sdk = { workspace = true }
 soroban-sdk = { workspace = true, features = ["testutils"] }
 rand = { workspace = true }
 serde_json = { workspace = true }
+proptest = "1"
 
 [features]
 testutils = ["soroban-sdk/testutils"]

contracts/predict-iq/INVARIANTS.md

@@ -0,0 +1,152 @@
+# Contract Invariants
+
+This document enumerates the financial and state-machine invariants that the
+`predict-iq` Soroban contract must uphold at all times. Violating any of these
+invariants constitutes a critical bug.
+
+---
+
+## 1. Stake Conservation
+
+**Statement:** The sum of all per-outcome stakes for a market equals the
+market's `total_staked` field at every observable state boundary (after each
+bet, after each refund, after each payout claim).
+
+```
+∀ market m:  Σ outcome_stake(m, o) for o in 0..m.num_outcomes  ==  m.total_staked
+```
+
+**Why:** `total_staked` drives payout calculations; a discrepancy would allow
+over-payment or under-payment.
+
+**Enforced by:** `invariants_test.rs`, `property_invariants_test.rs`
+(proptest Props 1 & 5).
+
+---
+
+## 2. Non-Negative Stakes
+
+**Statement:** `total_staked` and every `outcome_stake` are always `≥ 0`.
+
+**Why:** Negative values would indicate funds were created from nothing.
+
+**Enforced by:** `property_invariants_test.rs` (Prop 4).
+
+---
+
+## 3. State Machine Irreversibility
+
+The market status follows a directed acyclic graph (DAG). Backwards transitions
+are forbidden.
+
+```
+Active
+  ├─► PendingResolution ──► Resolved   (terminal)
+  ├─► Disputed          ──► Resolved   (terminal)
+  └─► Cancelled                        (terminal)
+```
+
+**Rules:**
+- `Resolved` and `Cancelled` are terminal — no further status changes are
+  allowed once a market reaches either state.
+- A market in `PendingResolution` or `Disputed` cannot return to `Active`.
+- Only `Active` markets accept new bets.
+
+**Enforced by:** `test_resolution_state_machine.rs`,
+`property_invariants_test.rs` (Props 2 & 3).
+
+---
+
+## 4. Bet Acceptance Window
+
+Bets are only accepted when:
+- Market status is `Active`, **and**
+- Current ledger timestamp `< market.deadline`, **and**
+- Current ledger timestamp `< market.resolution_deadline`
+
+**Enforced by:** `bets_fuzz_test.rs` (Props 4 & 5),
+`property_invariants_test.rs` (Prop 3).
+
+---
+
+## 5. Payout Upper Bound
+
+After resolution, the total amount distributed to winners must not exceed
+`total_staked`. The platform fee creates a small shortfall (funds go to the
+protocol treasury) so the bound is:
+
+```
+total_payouts ≤ total_staked
+```
+
+**Why:** Any excess would require the contract to create tokens, which is
+impossible; the real failure mode is a logic error that directs more funds to
+a single winner than were contributed.
+
+---
+
+## 6. Fee Integrity
+
+The platform fee is collected once per bet at placement time. No fee is applied
+at withdrawal or payout. The net stake recorded is:
+
+```
+net_stake = amount - floor(amount * fee_bps / 10_000)
+```
+
+The fee amount is transferred to the protocol treasury address at bet time.
+
+---
+
+## 7. Refund Idempotency
+
+Calling `withdraw_refund` more than once for the same `(bettor, market_id,
+outcome)` must not yield additional funds. The first call drains the stake
+record to zero; subsequent calls are no-ops (or return an error).
+
+---
+
+## Formal Verification Notes
+
+The most critical invariant for formal treatment is **Stake Conservation**
+(§1) because it ties together every mutation path (place_bet, cancel,
+resolve, claim_payout, withdraw_refund).
+
+### Certora Prover
+
+Certora's Prover can verify Soroban contracts compiled to WebAssembly using
+its EVM-agnostic bytecode backend (in preview as of 2025). Suggested specs:
+
+```certora
+rule stakeConservation(method f) {
+    env e;
+    uint64 mid;
+    mathint before = sumOutcomeStakes(mid);
+    calldataarg args;
+    f(e, args);
+    mathint after = sumOutcomeStakes(mid);
+    assert after == to_mathint(getMarket(mid).total_staked);
+}
+```
+
+Track Certora's Soroban support at: https://docs.certora.com
+
+### KEVM
+
+KEVM can formally verify WASM semantics. For the payout logic the recommended
+approach is:
+
+1. Extract the `claim_payout` and `withdraw_refund` functions as standalone
+   WASM modules.
+2. Write K specifications asserting the stake cell decreases by exactly the
+   computed payout, with no overflow.
+3. Run with `kprove` against the WASM semantics module.
+
+KEVM repository: https://github.com/runtimeverification/wasm-semantics
+
+### Priority
+
+Given the WASM toolchain maturity timeline, the recommended order is:
+1. Expand proptest coverage (done — `property_invariants_test.rs`)
+2. Add cargo-fuzz targets (done — `fuzz/` directory)
+3. Engage Certora when Soroban WASM backend reaches GA

contracts/predict-iq/README.md

@@ -2,6 +2,55 @@
 
 Soroban smart contract for the PredictIQ prediction market platform.
 
+## Fuzzing
+
+The `fuzz/` directory contains [cargo-fuzz](https://github.com/rust-fuzz/cargo-fuzz)
+targets for the three primary entry points. Fuzzing requires a nightly toolchain
+and the `cargo-fuzz` binary.
+
+### Setup
+
+```bash
+rustup toolchain install nightly
+cargo install cargo-fuzz
+```
+
+### Running a target
+
+```bash
+# From contracts/predict-iq/
+cargo +nightly fuzz run fuzz_place_bet
+cargo +nightly fuzz run fuzz_resolve_market
+cargo +nightly fuzz run fuzz_withdraw
+```
+
+Run with a time limit (CI uses 60 s):
+
+```bash
+cargo +nightly fuzz run fuzz_place_bet -- -max_total_time=60
+```
+
+### Targets
+
+| Target | Entry point | What it fuzzes |
+|--------|-------------|----------------|
+| `fuzz_place_bet` | `place_bet` | Arbitrary outcome, amount, timestamp |
+| `fuzz_resolve_market` | `resolve_market` | Arbitrary market ID and winning outcome |
+| `fuzz_withdraw` | `withdraw_refund` | Arbitrary market ID on a cancelled market |
+
+### Corpus and crashes
+
+Corpora are stored in `fuzz/corpus/<target>/` (gitignored). Crash-inducing
+inputs found during a run are written to `fuzz/artifacts/<target>/` and must be
+added as regression tests under `src/modules/` before the crash is considered
+fixed.
+
+### CI
+
+The `contract-fuzz` CI job (`.github/workflows/test.yml`) runs each target for
+**60 seconds** using libFuzzer on every push to `main` / `develop`. Crashes
+upload to the `fuzz-crashes` GitHub Actions artifact.
+
 ## WASM Size Limit
 
 The contract enforces a **64 KB (65,536 bytes)** WASM size limit. This is an internal budget target stricter than Soroban's actual limit, ensuring the contract remains performant and deployable across all networks. The limit is configured in `.github/workflows/test.yml` as `WASM_SIZE_LIMIT_BYTES` and checked during the build-optimized job.

contracts/predict-iq/fuzz/.gitignore

@@ -0,0 +1,3 @@
+corpus
+artifacts
+coverage

contracts/predict-iq/fuzz/Cargo.toml

@@ -0,0 +1,37 @@
+[package]
+name = "predict-iq-fuzz"
+version = "0.0.1"
+edition = "2021"
+publish = false
+
+[package.metadata]
+cargo-fuzz = true
+
+[[bin]]
+name = "fuzz_place_bet"
+path = "fuzz_targets/fuzz_place_bet.rs"
+test = false
+doc = false
+
+[[bin]]
+name = "fuzz_resolve_market"
+path = "fuzz_targets/fuzz_resolve_market.rs"
+test = false
+doc = false
+
+[[bin]]
+name = "fuzz_withdraw"
+path = "fuzz_targets/fuzz_withdraw.rs"
+test = false
+doc = false
+
+[dependencies]
+libfuzzer-sys = "0.4"
+
+[dependencies.predict-iq]
+path = ".."
+features = ["testutils"]
+
+[dependencies.soroban-sdk]
+version = "26.0.1"
+features = ["testutils"]