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

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `rmsnorm-kernel-v1` v1.0.0.
///
/// RMSNorm kernel — root mean square layer normalization
/// Reference: Zhang & Sennrich (2019) Root Mean Square Layer Normalization
/// Reference: Touvron et al. (2023) Llama 2: Open Foundation and Fine-Tuned Chat Models
///
/// Implementors must provide all 1 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait RmsnormKernelV1 {
    /// `rmsnorm`: RMSNorm(x)_i = (x_i / RMS(x)) · γ_i where RMS(x) = √(Σ x_i² / n + ε)
    /// Domain: x ∈ ℝ^n, γ ∈ ℝ^n, ε > 0
    /// Codomain: ℝ^n
    /// Invariant: ‖RMSNorm(x)‖² / n ≈ ‖γ‖² / n (scale preservation)
    /// Invariant: RMSNorm(α·x) = sign(α) · RMSNorm(x) · γ (scale invariance)
    fn rmsnorm(&self, x: &[f32]) -> Vec<f32>;
}