Autoharness: make --bounded-arguments bounds configurable and surface them in the output

[feliperodri]

Follow-up from #4691 (see this review thread). Towards #3832.

When --bounded-arguments is enabled, autoharness generates bounded nondeterministic values for slice and string arguments. The bounds are currently hardcoded constants (kani-compiler/src/kani_middle/transform/automatic.rs):

• AUTOHARNESS_SLICE_BOUND = 16 (max slice length)
• AUTOHARNESS_STR_BOUND = 4 (max string length in bytes)

Since these bounds are a key part of the verification guarantee a bounded harness provides, two improvements are worth pursuing:

1. Configurability

There is no way for a user to override the bounds today. Users may want a larger bound for stronger coverage (accepting longer runtimes) or a smaller one to fit a timeout. We should let them set the values, e.g. via CLI options such as --autoharness-slice-bound <N> / --autoharness-string-bound <N> (names TBD), threaded down to the codegen constants.

Considerations:

• The bounds should stay below the effective loop-unwinding bound (default 20) for loops over the slice/string to be fully unwound, or we should warn/adjust when they do not.
• Interaction with --default-unwind and --harness-timeout (larger bounds are more expensive; see the timeout issues already hit on slow runners in Autoharness: support slice and string arguments (bounded) #4691).

2. Transparency in the output

Currently the summary marks bounded harnesses (bounded) and prints:

Note: harnesses marked "(bounded)" use bounded nondeterministic values for some arguments (--bounded-arguments); their verification results only hold up to the bounds, i.e., bugs that require larger input values may be missed.

but it never states the actual bound values, so the reader cannot tell whether a slice was bounded at 16 or at some other value. We should surface the concrete bounds (e.g. "slices up to 16 elements, strings up to 4 bytes") in the note and/or per-harness output so the guarantee is explicit.

Related

• The optimum default values themselves deserve some investigation (coverage vs. solver cost); Autoharness: support slice and string arguments (bounded) #4691 already lowered the string bound from 8 to 4 to fit the default 60s harness timeout.