Stabilized Performance: improved harnessing

[YoshikiTakashima]

Description of changes:

This change improves performance by doing the following by removing sources of performance instability in PropProof's harnessing (crate::test_runner and macros)

Resolved issues:

Works towards #1608

Call-outs:

This change alters the public API of crate::test_runner::Config, and henceforth has the risk of breaking potential customer code. However, crawled data suggests that interaction with this API is mostly done through the use of $config in the macros. (src/sugar.rs). We turn this off with appropriate adjustments in the macros (Kani was already not using this data) so any customer code that is using #![proptest_config(...)] still works. However, if the customer code directly interacts with the 2 deleted parameters of Config, then we will fail to type check

• Tracking: #1716 The mitigation will be to put unwind bounds per function or other more fine-grained units of code so that we can stop the unrolling problem.

Separately, some commits were reverted (see enums). Reviewers should ignore https://github.com/model-checking/kani/pull/1715/commits/129be91649f0218cc83c91a6d588c7ac37b4313a and https://github.com/model-checking/kani/pull/1715/commits/987953c2c4c666e0866b9b53e49da07f36ea9135

Testing:

• How is this change tested? Performance: External test with enum (implementation coming soon) Still works with proptest_config attributes:

• Is this a refactor change? No.

Checklist

• [x] Each commit message has a non-empty body, explaining why the change was made
• [x] Methods or procedures are documented
• [x] Regression or unit tests are included, or existing tests cover the modified code
• [x] My PR is restricted to a single feature or bugfix

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

[YoshikiTakashima]

@danielsn Would you mind taking a look?