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

#![allow(clippy::doc_markdown)]

/// Contract trait for `silu-kernel-v1` v1.0.0.
///
/// SiLU kernel — sigmoid linear unit activation function
/// Reference: Ramachandran et al. (2017) Searching for Activation Functions
/// Reference: Elfwing et al. (2018) Sigmoid-Weighted Linear Units
///
/// Implementors must provide all 2 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait SiluKernelV1 {
    /// `sigmoid`: sigmoid(x) = 1 / (1 + exp(-x))
    /// Domain: x in R
    /// Codomain: sigmoid(x) in (0, 1)
    /// Invariant: sigmoid(0) = 0.5
    /// Invariant: sigmoid(-x) = 1 - sigmoid(x) (symmetry)
    fn sigmoid(&self, x: &[f32]) -> Vec<f32>;

    /// `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 (zero preservation)
    /// Invariant: SiLU(x) > -0.279 for all x (global minimum at x ~ -1.278)
    /// Invariant: SiLU(x) ~ x for large positive x (asymptotic linearity)
    /// Invariant: SiLU is monotonic for x > 0
    fn silu(&self, x: &[f32]) -> Vec<f32>;
}