Implement stub sets for reusable stub groups

[feliperodri]

Add kani::stub_set! macro and #[kani::use_stub_set] attribute for defining reusable groups of stubs that can be applied to multiple proof harnesses without repeating individual #[kani::stub] annotations.

Resolves #2096.

Problem

When multiple proof harnesses need the same set of stubs (e.g., mocking I/O, randomness, or network calls), users must duplicate #[kani::stub(orig, repl)] annotations on every harness. This is verbose, error-prone, and makes it hard to maintain consistent stub configurations across a test suite.

Solution

kani::stub_set! macro

Defines a named, reusable group of stub pairs:

kani::stub_set! {
    pub my_io_stubs {
        stub(std::fs::read, mock_read)
        stub(std::fs::write, mock_write)
        use_stub_set(other_stubs)  // compose with other sets
    }
}

#[kani::use_stub_set] attribute

Applies a stub set to a harness:

#[kani::proof]
#[kani::use_stub_set(my_io_stubs)]
fn check_with_mocked_io() { ... }

Features

• Composition: Stub sets can include use_stub_set(other_set) entries to compose sets
• Visibility: pub modifier for cross-module access
• Combining: #[kani::use_stub_set] works alongside individual #[kani::stub] attributes
• Per-harness: Different harnesses can use different stub sets
• Circular reference detection: Errors on circular use_stub_set references

Implementation

• stub_set! generates a const with a #[kanitool::stub_set(...)] attribute encoding the stub pairs
• use_stub_set resolution in attributes.rs reads the attribute, resolves paths relative to the harness module, and expands the pairs into the harness's stub list
• Path resolution in resolve.rs extended to look up stub_set consts

Testing

5 tests covering:

• stub_set_basic.rs — basic stub set definition and usage
• stub_set_composed.rs — composing stub sets via use_stub_set entries
• stub_set_module.rs — cross-module access with pub visibility
• stub_set_per_harness.rs — different stub sets per harness
• stub_set_with_individual.rs — combining stub sets with individual #[kani::stub]

---

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[adpaco-aws]

Glad to see this feature becoming a reality!

Overall, it's looking great. We should add a couple test cases just to ensure no regressions in the future.