aprender-contracts 0.34.0

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
24
25
26
27
28
29
30
31

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `cross-entropy-kernel-v1` v1.0.0.
///
/// Cross-entropy kernel — log-sum-exp stable cross-entropy loss
/// Reference: Shannon (1948) A Mathematical Theory of Communication
/// Reference: Milakov & Gimelshein (2018) Online normalizer calculation for softmax
///
/// Implementors must provide all 2 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait CrossEntropyKernelV1 {
    /// `cross_entropy`: CE(targets, logits) = -sum(targets_i * log_softmax(logits)_i)
    /// Domain: targets in {0,1}^n with sum=1, logits in R^n, n >= 2
    /// Codomain: CE in [0, +inf)
    /// Invariant: CE >= 0 (non-negativity)
    /// Invariant: CE(one_hot(k), logits) = -log_softmax(logits)_k
    /// Invariant: CE(p, p_logits) = H(p) when p = softmax(p_logits)
    fn cross_entropy(&self, targets: &[f32], logits: &[f32]) -> Vec<f32>;

    /// `log_softmax`: log_softmax(x)_i = x_i - max(x) - log(sum(exp(x_j - max(x))))
    /// Domain: x in R^n, n >= 1
    /// Codomain: log_softmax(x) in (-inf, 0]
    /// Invariant: log_softmax(x)_i <= 0 for all i
    /// Invariant: exp(log_softmax(x)) = softmax(x)
    /// Invariant: log_sum_exp trick preserves numerical stability
    fn log_softmax(&self, x: &[f32]) -> Vec<f32>;
}