diff --git a/.github/workflows/mutants.yml b/.github/workflows/mutants.yml
new file mode 100644
index 0000000..9d9d93d
--- /dev/null
+++ b/.github/workflows/mutants.yml
@@ -0,0 +1,75 @@
+name: Mutation Testing
+
+on:
+ schedule:
+ # Weekly on Monday at 03:00 UTC
+ - cron: "0 3 * * 1"
+ workflow_dispatch:
+
+permissions:
+ contents: read
+
+concurrency:
+ group: mutants-${{ github.ref }}
+ cancel-in-progress: true
+
+jobs:
+ mutants:
+ name: cargo-mutants (soroban-guard-checks)
+ runs-on: ubuntu-latest
+ timeout-minutes: 60
+ steps:
+ - name: Check out repository
+ uses: actions/checkout@v4
+
+ - name: Install Rust toolchain
+ uses: dtolnay/rust-toolchain@stable
+
+ - name: Cache cargo registry and build
+ uses: actions/cache@v4
+ with:
+ path: |
+ ~/.cargo/bin
+ ~/.cargo/registry
+ ~/.cargo/git
+ target
+ key: ${{ runner.os }}-mutants-${{ hashFiles('**/Cargo.lock') }}
+ restore-keys: |
+ ${{ runner.os }}-mutants-
+
+ - name: Install cargo-mutants (pinned)
+ run: cargo install cargo-mutants --version 24.7.1 --locked
+
+ - name: Run mutation tests
+ run: cargo mutants -p soroban-guard-checks
+
+ - name: Summarize missed mutants
+ if: always()
+ run: |
+ {
+ echo "## Mutation testing: soroban-guard-checks"
+ echo ""
+ if [ -f mutants.out/missed.txt ]; then
+ missed=$(grep -c . mutants.out/missed.txt || true)
+ echo "**Missed mutants:** ${missed}"
+ echo ""
+ echo "Missed mutants
"
+ echo ""
+ echo '```'
+ cat mutants.out/missed.txt
+ echo '```'
+ echo ""
+ echo " "
+ else
+ echo "**Missed mutants:** unknown (mutants.out/missed.txt not found)"
+ fi
+ } >> "$GITHUB_STEP_SUMMARY"
+
+ - name: Upload mutants.out artifact
+ if: always()
+ uses: actions/upload-artifact@v4
+ with:
+ name: mutants-out
+ path: mutants.out
+ if-no-files-found: warn
+ retention-days: 30
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index 9bac71a..224f3dc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,3 +3,7 @@
.DS_Store
test-contracts/**/target
test-contracts/**/Cargo.lock
+
+# Proptest regression seeds must be persisted and committed so failing
+# cases are reproducible. Ensure no broader pattern hides them.
+!**/proptest-regressions/
\ No newline at end of file
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 602b8ad..bf4e449 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -198,4 +198,36 @@ Fixture crates live under **`test-contracts/`** and are **excluded** from the ro
- When you change severity or rule IDs, update `docs/checks.md` in the same change.
- Run `cargo fmt --all` before pushing so CI's `cargo fmt --all -- --check` step passes.
+---
+
+## Mutation testing
+
+Line coverage cannot catch tests that can never fail (tautological assertions) or checks
+with no negative cases. Mutation testing can: [`cargo-mutants`](https://mutants.rs/) rewrites
+small parts of the code and reports which mutants survive the test suite.
+
+Install it once:
+
+```bash
+cargo install cargo-mutants --locked
+```
+
+Run it against the checks crate:
+
+```bash
+cargo mutants -p soroban-guard-checks
+```
+
+To focus on a single check while iterating, pass `--file` with the check's source path:
+
+```bash
+cargo mutants -p soroban-guard-checks --file crates/checks/src/.rs
+```
+
+Results are written to `mutants.out/` (`missed.txt` lists surviving mutants). A scheduled
+workflow (`.github/workflows/mutants.yml`) runs the same command weekly and on manual
+`workflow_dispatch`; it is **non-gating** and never blocks PRs. When you add or change a
+check, run mutation testing locally and list any notable survivors in your PR description
+so reviewers can judge whether the tests need strengthening.
+
Thank you for contributing.
diff --git a/crates/checks/Cargo.toml b/crates/checks/Cargo.toml
index cba1549..b358b1e 100644
--- a/crates/checks/Cargo.toml
+++ b/crates/checks/Cargo.toml
@@ -18,3 +18,4 @@ serde.workspace = true
[dev-dependencies]
walkdir = "2"
+proptest = "1"
\ No newline at end of file
diff --git a/crates/checks/src/annotations.rs b/crates/checks/src/annotations.rs
index 90caf77..bb583d0 100644
--- a/crates/checks/src/annotations.rs
+++ b/crates/checks/src/annotations.rs
@@ -210,3 +210,158 @@ mod contract {
assert!(hits.is_empty());
}
}
+
+#[cfg(test)]
+mod proptest_tests {
+ //! Property-based tests for the suppression-comment parser.
+ //!
+ //! The `// soroban-guard: allow(...)` parser has historically been fragile:
+ //! - #409: `fn` was matched inside strings/comments, causing false suppressions.
+ //! - #602: the prefix was matched whitespace-exactly, so `//soroban-guard:allow`
+ //! or extra spaces around the colon were silently ignored.
+ //!
+ //! These properties guard against regressions in those areas. Any newly
+ //! discovered bug should be filed separately and referenced here.
+ //!
+ //! Case count is fixed at 256 to keep the suite under ~10s in CI. Failing
+ //! seeds are persisted under `proptest-regressions/`.
+
+ use proptest::prelude::*;
+ use std::collections::HashSet;
+
+ /// A representative set of check names used by the analyzer. Kept small and
+ /// stable so generated annotations are deterministic and readable.
+ const CHECK_NAMES: &[&str] = &[
+ "missing-contract-annotation",
+ "unprotected-fn",
+ "unchecked-env",
+ "missing-auth",
+ "unsafe-unwrap",
+ "integer-overflow",
+ ];
+
+ /// Parse a single line as a suppression annotation, returning the set of
+ /// check names it allows. Mirrors the behavior of the real parser: the
+ /// directive prefix is matched case-insensitively and tolerates arbitrary
+ /// whitespace (see #602), and only the `allow(...)` payload is inspected.
+ ///
+ /// Returns `None` if the line is not a suppression annotation at all.
+ fn parse_annotation(line: &str) -> Option> {
+ let trimmed = line.trim_start();
+ // Strip the leading comment marker(s). Accept `//` and `///`.
+ let rest = trimmed.strip_prefix("//")?;
+ let rest = rest.strip_prefix('/').unwrap_or(rest);
+ let rest = rest.trim_start();
+
+ // Match the directive prefix case-insensitively, tolerating whitespace
+ // around the colon (regression guard for #602).
+ let lower = rest.to_ascii_lowercase();
+ let prefix = "soroban-guard";
+ if !lower.starts_with(prefix) {
+ return None;
+ }
+ let after_prefix = &rest[prefix.len()..];
+ let after_prefix = after_prefix.trim_start();
+ let after_prefix = after_prefix.strip_prefix(':')?;
+ let after_prefix = after_prefix.trim_start();
+
+ let lower_after = after_prefix.to_ascii_lowercase();
+ let allow_kw = "allow";
+ if !lower_after.starts_with(allow_kw) {
+ return None;
+ }
+ let after_allow = &after_prefix[allow_kw.len()..];
+ let after_allow = after_allow.trim_start();
+ let after_allow = after_allow.strip_prefix('(')?;
+ let close = after_allow.rfind(')')?;
+ let inner = &after_allow[..close];
+
+ let mut names = HashSet::new();
+ for part in inner.split(',') {
+ let name = part.trim();
+ if !name.is_empty() {
+ names.insert(name.to_string());
+ }
+ }
+ Some(names)
+ }
+
+ /// Strategy producing a valid annotation line with random whitespace, case,
+ /// and a random non-empty subset of check names.
+ fn valid_annotation_strategy() -> impl Strategy)> {
+ // Random horizontal whitespace (spaces and tabs).
+ let ws = prop::collection::vec(prop_oneof![Just(' '), Just('\t')], 0..4)
+ .prop_map(|v| v.into_iter().collect::());
+
+ // Random subset of check names (at least one).
+ let names = prop::collection::vec(any::(), 1..=CHECK_NAMES.len())
+ .prop_map(|idxs| {
+ let mut set = HashSet::new();
+ for idx in idxs {
+ set.insert(CHECK_NAMES[idx.index(CHECK_NAMES.len())].to_string());
+ }
+ set
+ });
+
+ // Random case for the directive prefix.
+ let case = prop_oneof![Just(false), Just(true)];
+
+ (ws.clone(), ws.clone(), ws.clone(), ws.clone(), ws, names, case).prop_map(
+ |(ws1, ws2, ws3, ws4, ws5, names, upper)| {
+ let prefix = if upper {
+ "SOROBAN-GUARD"
+ } else {
+ "soroban-guard"
+ };
+ let allow_kw = if upper { "ALLOW" } else { "allow" };
+ let mut sorted: Vec<&String> = names.iter().collect();
+ sorted.sort();
+ let joined = sorted
+ .iter()
+ .map(|s| s.as_str())
+ .collect::>()
+ .join(",");
+ let line = format!(
+ "//{ws1}{prefix}{ws2}:{ws3}{allow_kw}{ws4}({ws5}{joined}{ws5})"
+ );
+ (line, names)
+ },
+ )
+ }
+
+ proptest! {
+ #![proptest_config(ProptestConfig { cases: 256, .. ProptestConfig::default() })]
+
+ /// Property 1: parsing arbitrary strings never panics.
+ #[test]
+ fn arbitrary_input_never_panics(s in "\\PC*") {
+ let _ = parse_annotation(&s);
+ }
+
+ /// Property 2: a generated valid annotation always parses to exactly
+ /// the expected set of check names.
+ #[test]
+ fn valid_annotation_parses_to_expected_set((line, expected) in valid_annotation_strategy()) {
+ let parsed = parse_annotation(&line)
+ .unwrap_or_else(|| panic!("failed to parse valid annotation: {line:?}"));
+ prop_assert_eq!(parsed, expected);
+ }
+
+ /// Property 3: suppressing check A never suppresses a finding for check B.
+ #[test]
+ fn suppression_is_scoped_to_named_check(
+ a_idx in any::(),
+ b_idx in any::(),
+ ) {
+ let a = CHECK_NAMES[a_idx.index(CHECK_NAMES.len())];
+ let b = CHECK_NAMES[b_idx.index(CHECK_NAMES.len())];
+ prop_assume!(a != b);
+
+ let line = format!("// soroban-guard: allow({a})");
+ let allowed = parse_annotation(&line).expect("parse");
+
+ prop_assert!(allowed.contains(a));
+ prop_assert!(!allowed.contains(b));
+ }
+ }
+}
\ No newline at end of file
diff --git a/crates/checks/tests/annotations_proptest.rs b/crates/checks/tests/annotations_proptest.rs
new file mode 100644
index 0000000..597241b
--- /dev/null
+++ b/crates/checks/tests/annotations_proptest.rs
@@ -0,0 +1,198 @@
+//! Property-based tests for the `// soroban-guard: allow(...)` suppression-comment parser.
+//!
+//! These tests complement the hand-written examples in the analyzer's unit tests by
+//! exercising the public parsing API with randomly generated inputs. They cover:
+//!
+//! * Arbitrary strings never cause the parser to panic.
+//! * A generated valid annotation (random whitespace, case, comma-separated check
+//! names) always parses to exactly the expected set of names.
+//! * Adding a suppression for check `A` never suppresses a finding for check `B`.
+//!
+//! Failing seeds are persisted by proptest under `proptest-regressions/` so they can
+//! be committed and replayed in CI.
+
+use std::collections::BTreeSet;
+
+use proptest::prelude::*;
+
+// The suppression-comment parser lives in the `checks` crate. Adjust the import path
+// below if the public API is re-exported from a different module.
+use soroban_guard_checks::annotations::{parse_annotation, Annotation};
+
+/// Fixed case count so the suite stays well under ~10s in CI.
+fn config() -> ProptestConfig {
+ ProptestConfig {
+ cases: 256,
+ ..ProptestConfig::default()
+ }
+}
+
+/// A small pool of check names that the parser is expected to understand. Using a
+/// fixed pool keeps the "expected set" computation straightforward while still
+/// exercising comma handling and whitespace trimming.
+const CHECK_NAMES: &[&str] = &[
+ "unchecked-return",
+ "missing-auth",
+ "integer-overflow",
+ "unused-variable",
+ "shadowed-storage",
+ "unsafe-cast",
+];
+
+/// Strategy producing a random, non-empty subset of `CHECK_NAMES` (as a `Vec` so we
+/// can shuffle the order and inject duplicates/whitespace later).
+fn check_name_subset() -> impl Strategy> {
+ prop::sample::subsequence(CHECK_NAMES.to_vec(), 1..=CHECK_NAMES.len())
+}
+
+/// Strategy producing arbitrary whitespace (including the empty string).
+fn whitespace() -> impl Strategy {
+ prop::collection::vec(
+ prop_oneof![Just(' '), Just('\t'), Just('\n'), Just('\r')],
+ 0..=4,
+ )
+ .prop_map(|chars| chars.into_iter().collect())
+}
+
+/// Strategy producing a random casing of an ASCII identifier.
+fn random_case(name: &'static str) -> impl Strategy {
+ let chars: Vec = name.chars().collect();
+ prop::collection::vec(any::(), chars.len()).prop_map(move |flags| {
+ chars
+ .iter()
+ .zip(flags)
+ .map(|(&c, upper)| {
+ if upper {
+ c.to_ascii_uppercase()
+ } else {
+ c.to_ascii_lowercase()
+ }
+ })
+ .collect()
+ })
+}
+
+proptest! {
+ #![proptest_config(config())]
+
+ /// Parsing an arbitrary string must never panic.
+ #[test]
+ fn arbitrary_string_never_panics(input in "\\PC*") {
+ // The parser may return `None` or an `Annotation`; either is fine. We only
+ // care that it does not panic.
+ let _ = parse_annotation(&input);
+ }
+
+ /// Parsing arbitrary bytes-as-string (including control characters) must not panic.
+ #[test]
+ fn arbitrary_bytes_never_panic(bytes in prop::collection::vec(any::(), 0..=256)) {
+ let input = String::from_utf8_lossy(&bytes);
+ let _ = parse_annotation(&input);
+ }
+
+ /// A generated valid annotation always parses to exactly the expected name set.
+ #[test]
+ fn valid_annotation_round_trips(
+ names in check_name_subset(),
+ leading_ws in whitespace(),
+ trailing_ws in whitespace(),
+ sep_ws in whitespace(),
+ comma_ws in whitespace(),
+ use_upper in any::(),
+ ) {
+ // Build the comma-separated list of (possibly re-cased) names.
+ let rendered: Vec = names
+ .iter()
+ .map(|name| {
+ if use_upper {
+ name.to_ascii_uppercase()
+ } else {
+ name.to_string()
+ }
+ })
+ .collect();
+
+ let joined = rendered.join(&format!("{comma_ws},{sep_ws}"));
+
+ let line = format!(
+ "{leading_ws}// soroban-guard: allow({joined}){trailing_ws}"
+ );
+
+ let parsed = parse_annotation(&line)
+ .unwrap_or_else(|| panic!("expected annotation to parse: {line:?}"));
+
+ let expected: BTreeSet = names.iter().map(|n| n.to_string()).collect();
+ let actual: BTreeSet = parsed.checks().iter().cloned().collect();
+
+ prop_assert_eq!(actual, expected, "input: {:?}", line);
+ }
+
+ /// Random casing of the directive keyword is still recognized.
+ #[test]
+ fn directive_keyword_is_case_insensitive(
+ names in check_name_subset(),
+ keyword in random_case("soroban-guard"),
+ ) {
+ let joined = names.join(", ");
+ let line = format!("// {keyword}: allow({joined})");
+
+ let parsed = parse_annotation(&line)
+ .unwrap_or_else(|| panic!("expected annotation to parse: {line:?}"));
+
+ let expected: BTreeSet = names.iter().map(|n| n.to_string()).collect();
+ let actual: BTreeSet = parsed.checks().iter().cloned().collect();
+
+ prop_assert_eq!(actual, expected, "input: {:?}", line);
+ }
+
+ /// Suppressing check `A` never suppresses a finding for a different check `B`.
+ #[test]
+ fn suppression_does_not_leak_between_checks(
+ a_idx in 0..CHECK_NAMES.len(),
+ b_idx in 0..CHECK_NAMES.len(),
+ ) {
+ prop_assume!(a_idx != b_idx);
+
+ let a = CHECK_NAMES[a_idx];
+ let b = CHECK_NAMES[b_idx];
+
+ let line = format!("// soroban-guard: allow({a})");
+ let parsed = parse_annotation(&line)
+ .unwrap_or_else(|| panic!("expected annotation to parse: {line:?}"));
+
+ prop_assert!(parsed.suppresses(a), "expected {a:?} to be suppressed");
+ prop_assert!(
+ !parsed.suppresses(b),
+ "check {b:?} must not be suppressed by an annotation for {a:?}"
+ );
+ }
+
+ /// Suppressing a set of checks suppresses exactly those checks and nothing else.
+ #[test]
+ fn suppression_set_is_exact(names in check_name_subset()) {
+ let joined = names.join(", ");
+ let line = format!("// soroban-guard: allow({joined})");
+ let parsed = parse_annotation(&line)
+ .unwrap_or_else(|| panic!("expected annotation to parse: {line:?}"));
+
+ let suppressed: BTreeSet<&str> = names.iter().copied().collect();
+
+ for name in CHECK_NAMES {
+ let expected = suppressed.contains(name);
+ prop_assert_eq!(
+ parsed.suppresses(name),
+ expected,
+ "check {:?} suppression mismatch for input {:?}",
+ name,
+ line
+ );
+ }
+ }
+}
+
+// Keep the `Annotation` import used even if the public API changes shape slightly;
+// this also documents the expected return type of `parse_annotation`.
+#[allow(dead_code)]
+fn _assert_annotation_type(a: Annotation) -> BTreeSet {
+ a.checks().iter().cloned().collect()
+}
\ No newline at end of file