polyvoice 0.5.2

# FORMALISM.md — Concrete Verification Tools for polyvoice

## §1 Hoare Triples & Contracts

Every public function must document its contract as a Hoare triple:

```rust
/// { pre: !samples.is_empty() }
/// fn extract(samples: &[f32]) -> Result<Vec<f32>, Error>
/// { post: ret.is_ok() => ret.as_ref().unwrap().len() == EMBEDDING_DIM }
```

Use `debug_assert!` for cheap runtime precondition checks.

## §2 Newtypes & Typestate

Encode invariants in types to prevent invalid states at compile time.

### Newtype pattern
```rust
#[derive(Debug, Clone, Copy, PartialEq)]
pub struct Confidence(f32);

impl Confidence {
    pub fn new(v: f32) -> Option<Self> {
        (0.0..=1.0).contains(&v).then_some(Self(v))
    }
}
```

### Typestate pattern
```rust
// BAD: bool flag checked at runtime
struct Diarizer { enabled: bool, state: State }

// GOOD: two types, invalid states unrepresentable
struct InactiveDiarizer;
struct ActiveDiarizer { state: State }
```

## §3 PhantomData & Lifetime Encoding

Use `PhantomData` to encode unused generic parameters in structs.

## §4 Property-Based Testing

Use `proptest` to verify universal properties:

```toml
[dev-dependencies]
proptest = "1"
```

```rust
use proptest::prelude::*;

proptest! {
    #[test]
    fn cosine_similarity_range(a in vec(-1.0f32..=1.0, 256), b in vec(-1.0f32..=1.0, 256)) {
        let sim = cosine_similarity(&a, &b);
        prop_assert!(sim >= -1.0 && sim <= 1.0);
    }
}
```

## §5 Miri (Undefined Behavior Detection)

Run Miri on unsafe code:
```bash
cargo +nightly miri test
```

## §6 Kani (Model Checking)

For critical unsafe code, use Kani to prove absence of panics:
```bash
cargo +nightly kani --function my_unsafe_fn
```