aprender-contracts 0.29.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
32
33
34
35
36
37
38
39
40

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `activation-kernel-v1` v1.0.0.
///
/// Activation functions — GELU, SiLU/Swish, ReLU kernels
/// Reference: Hendrycks & Gimpel (2016) Gaussian Error Linear Units (GELUs)
/// Reference: Ramachandran et al. (2017) Searching for Activation Functions (SiLU)
/// Reference: Nair & Hinton (2010) Rectified Linear Units Improve Restricted Boltzmann Machines
///
/// Implementors must provide all 3 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait ActivationKernelV1 {
    /// `gelu`: GELU(x) = x · Φ(x) ≈ 0.5x(1 + tanh(√(2/π)(x + 0.044715x³)))
    /// Domain: x ∈ ℝ
    /// Codomain: ℝ
    /// Invariant: GELU(x) → x as x → +∞
    /// Invariant: GELU(x) → 0 as x → -∞
    /// Invariant: GELU(0) = 0
    fn gelu(&self, x: f32) -> Vec<f32>;

    /// `relu`: ReLU(x) = max(0, x)
    /// Domain: x ∈ ℝ
    /// Codomain: [0, ∞)
    /// Invariant: ReLU(x) ≥ 0 (non-negativity)
    /// Invariant: ReLU(x) = x for x > 0
    /// Invariant: ReLU(x) = 0 for x ≤ 0
    fn relu(&self, x: f32) -> Vec<f32>;

    /// `silu`: SiLU(x) = x · σ(x) = x / (1 + exp(-x))
    /// Domain: x ∈ ℝ
    /// Codomain: ℝ
    /// Invariant: SiLU(x) → x as x → +∞
    /// Invariant: SiLU(x) → 0 as x → -∞
    /// Invariant: SiLU(0) = 0
    fn silu(&self, x: f32) -> Vec<f32>;
}