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

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `layernorm-kernel-v1` v1.0.0.
///
/// LayerNorm kernel — layer normalization with affine transform
/// Reference: Ba et al. (2016) Layer Normalization
/// Reference: Ioffe & Szegedy (2015) Batch Normalization
///
/// Implementors must provide all 2 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait LayernormKernelV1 {
    /// `layernorm`: LN(x)_i = gamma_i * (x_i - mu) / sqrt(sigma^2 + eps) + beta_i
    /// Domain: x in R^d, gamma in R^d, beta in R^d, eps > 0
    /// Codomain: LN(x) in R^d
    /// Invariant: mean(LN(x)) = mean(beta) when gamma = 1 (centering)
    /// Invariant: var(LN(x)) = 1 when gamma = 1, beta = 0 (standardization)
    /// Invariant: LN is invariant to input shift: LN(x + c) = LN(x)
    fn layernorm(&self, x: &[f32], gamma: &[f32]) -> Vec<f32>;

    /// `statistics`: mu = (1/d) * sum(x_i), sigma^2 = (1/d) * sum((x_i - mu)^2)
    /// Domain: x in R^d, d >= 1
    /// Codomain: mu in R, sigma^2 in R_>=0
    /// Invariant: sigma^2 >= 0 (non-negative variance)
    /// Invariant: sigma^2 = 0 iff x is constant
    fn statistics(&self, x: &[f32]) -> Vec<f32>;
}