aprender-contracts 0.31.1

Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

//! Auto-generated contract trait for `softmax-kernel-v1`.
//! Generated by: `pv scaffold --trait contracts/softmax-kernel-v1.yaml`
//! DO NOT EDIT — regenerate from YAML source.

#![allow(clippy::doc_markdown)]

/// Contract trait for `softmax-kernel-v1` v1.0.0.
///
/// Softmax kernel — numerically stable exponential normalization
/// Reference: Bridle (1990) Training Stochastic Model Recognition Algorithms as Networks
/// Reference: Milakov & Gimelshein (2018) Online normalizer calculation for softmax
///
/// Implementors must provide all 1 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait SoftmaxKernelV1 {
    /// `softmax`: σ(x)_i = exp(x_i - max(x)) / Σ_j exp(x_j - max(x))
    /// Domain: x ∈ ℝ^n, n ≥ 1
    /// Codomain: σ(x) ∈ (0,1)^n
    /// Invariant: Σ σ(x)_i = 1.0 (normalization)
    /// Invariant: σ(x)_i > 0 for all i (strict positivity)
    /// Invariant: argmax(σ(x)) = argmax(x) (order preservation)
    fn softmax(&self, x: &[f32]) -> Vec<f32>;
}