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 `swiglu-kernel-v1`.
//! Generated by: `pv scaffold --trait contracts/swiglu-kernel-v1.yaml`
//! DO NOT EDIT — regenerate from YAML source.

#![allow(clippy::doc_markdown)]

/// Contract trait for `swiglu-kernel-v1` v1.0.0.
///
/// SwiGLU kernel — gated linear unit with SiLU activation
/// Reference: Shazeer (2020) GLU Variants Improve Transformer
/// Reference: Ramachandran et al. (2017) Searching for Activation Functions
///
/// Implementors must provide all 2 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait SwigluKernelV1 {
    /// `silu`: SiLU(x) = x * sigmoid(x) = x / (1 + exp(-x))
    /// Domain: x in R
    /// Codomain: SiLU(x) in (-0.279, +inf)
    /// Invariant: SiLU(0) = 0
    /// Invariant: SiLU(x) > -0.279 for all x (global minimum)
    /// Invariant: SiLU is monotonic for x > 0
    fn silu(&self, x: &[f32]) -> Vec<f32>;

    /// `swiglu`: SwiGLU(x, W, V, b, c) = SiLU(xW + b) * (xV + c)
    /// Domain: x in R^d, W in R^{d x h}, V in R^{d x h}, b in R^h, c in R^h
    /// Codomain: SwiGLU(x) in R^h
    /// Invariant: SwiGLU(0, W, V, 0, 0) = 0 (zero preservation)
    /// Invariant: Decomposable as gate * value where gate = SiLU(xW+b)
    fn swiglu(&self, x: &[f32], w: &[f32], v: &[f32], b: &[f32], c: &[f32]) -> Vec<f32>;
}