KaniStrategy has no label for symbolic-f32-array harnesses, the dominant DSP verification technique — 7 of rmedia's 8 real Kani proofs are unrepresentable #2530

Summary

KaniStrategy offers four variants. None of them describes the technique that
7 of the 8 #[kani::proof] harnesses in paiml/rmedia actually use: a
fixed-length array of symbolic IEEE-754 f32, constrained to is_finite()
plus a magnitude bound, with transcendentals evaluated concretely (not stubbed).

Because strategy is a hard enum, a contract that names this technique fails to
parse at all — and every other check pv validate would apply to that
contract then passes vacuously. In rmedia this is not hypothetical:
contracts/audio-defect-v1.yaml declares 8 real, wired-up Kani harnesses and
pv validate reports it as "Kernel contract has no kani_harnesses", because
serde aborts on strategy before the harness list is ever seen. The reported
error is a downstream consequence of the vocabulary gap, not the actual defect.

The four existing variants and why each is a mislabel

crates/aprender-contracts/src/schema/types.rs:501-506:

#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum KaniStrategy {
    Exhaustive,
    StubFloat,
    Compositional,
    BoundedInt,
}

The codegen bodies in crates/aprender-contracts/src/kani_gen/strategies.rs
are the authoritative semantics — each writes its own definition into the
generated harness:

stub_float is the closest, and it is still a false statement about the
harness: it asserts transcendental stubbing that does not happen. That
distinction is load-bearing — it is the difference between "this proof is
modulo a float axiomatization" and "this proof discharges the real IEEE-754
arithmetic", which is exactly what a reader consults strategy to learn.

Evidence: the actual harnesses

All 8 #[kani::proof] sites in rmedia live in
crates/rmedia-core/src/audio_defect/. Seven share one shape. Representative,
clipping.rs:203-218:

#[cfg(kani)]
#[kani::proof]
fn verify_clip_totality() {
    const N: usize = 8;
    let mut samples = [0.0f32; N];          // fixed-length array, not Vec
    for s in samples.iter_mut() {
        *s = kani::any();                    // symbolic f32
        kani::assume(s.is_finite());         // finite domain
        kani::assume(s.abs() <= 4.0);        // magnitude bound
    }
    let r = detect_clipping(&samples, 1, 1.0);
    kani::assert(r.clip_count <= samples.len(), "clip_count <= samples.len()");
    let sum: usize = r.clip_runs.iter().map(|(_, len)| len).sum();
    kani::assert(sum == r.clip_count, "runs sum to clip_count");
}

The full census:

One of eight is expressible. This is not an rmedia-local quirk — it is what
bounded model checking of any signal-processing kernel looks like: a short
symbolic window of real samples, constrained finite and in-range, fed to the
unmodified kernel.

Reproduction

$ pv --version
pv 0.49.0

$ cd rmedia && pv validate contracts/audio-defect-v1.yaml; echo "EXIT=$?"
error: Failed to parse YAML: kani_harnesses[0].strategy: unknown variant `bounded_array`,
  expected one of `exhaustive`, `stub_float`, `compositional`, `bounded_int`
  at line 193 column 15
EXIT=1

Then, after removing the unknown value so the file parses, the 8 harnesses
become visible and the contract validates — same file, same harnesses, the only
difference being whether the enum could name the strategy.

Requested change

Add one variant:

pub enum KaniStrategy {
    Exhaustive,
    StubFloat,
    Compositional,
    BoundedInt,
    /// Symbolic IEEE-754 floats over a fixed-length window, constrained to
    /// `is_finite()` and a magnitude bound. Transcendentals are NOT stubbed —
    /// the proof discharges real float arithmetic. Contrast `stub_float`,
    /// which axiomatizes exp/log/sin/cos.
    BoundedFloat,
}

with a generate_bounded_float_body mirroring generate_bounded_int_body
(strategies.rs:133) but emitting Vec<f32> with is_finite() and
|x| <= bound assumptions, and no stub attributes.

One variant, not two. rmedia's contract currently spells two invented names,
bounded_array (3 harnesses) and bounded_float (2 harnesses), but the code
census above shows both denote the same technique — the author was drawing a
shape/domain distinction the harnesses do not actually make. Array-shape
([T; N] vs symbolic-length Vec<T>) is an axis orthogonal to element domain
and is already carried by bound; it does not need its own strategy variant.
Please do not add bounded_array.

Interim state in rmedia

rmedia will not mislabel these harnesses as stub_float or bounded_int to
buy a parse. The five affected entries omit the optional strategy key —
strategy: Option<KaniStrategy> with #[serde(default)] (types.rs:485-486),
so None is a legal "unlabelled" state and generate_default_body
(strategies.rs:165) already emits a finite-f32 body — with a
# TODO(aprender#NNN) recording the intended value and a pointer to this issue.
They will be set to bounded_float when it lands.

Two further harnesses — verify_dropout_min_len and verify_classify_fcap —
already carry strategy: bounded_int, which parses but is equally untrue
(their inputs are symbolic f32). Those are tracked separately in rmedia
because they do not block the parse; they are counted here as evidence that the
gap silently produces wrong metadata as well as unparseable metadata. pv has
no way to catch that class today: the enum accepts bounded_int for an f32
harness because nothing cross-checks strategy against the harness body.