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
32
33
34
35
36
37
38
39
40
41
42
43

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `adamw-kernel-v1` v1.0.0.
///
/// AdamW kernel — Adam optimizer with decoupled weight decay
/// Reference: Loshchilov & Hutter (2017) Decoupled Weight Decay Regularization
/// Reference: Kingma & Ba (2014) Adam: A Method for Stochastic Optimization
///
/// Implementors must provide all 4 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait AdamwKernelV1 {
    /// `adam_moments`: m_t = beta1 * m_{t-1} + (1 - beta1) * g_t
    /// Domain: g_t in R^d, m_0 = 0, beta1 in (0, 1)
    /// Codomain: m_t in R^d
    /// Invariant: m_t is exponential moving average of gradients
    /// Invariant: |m_t| bounded by max(|g_1|, ..., |g_t|) when beta1 < 1
    fn adam_moments(&self, g_t: &[f32]) -> Vec<f32>;

    /// `adam_variance`: v_t = beta2 * v_{t-1} + (1 - beta2) * g_t^2
    /// Domain: g_t in R^d, v_0 = 0, beta2 in (0, 1)
    /// Codomain: v_t in R_>=0^d
    /// Invariant: v_t >= 0 (non-negative second moment)
    /// Invariant: v_t is exponential moving average of squared gradients
    fn adam_variance(&self, g_t: &[f32]) -> Vec<f32>;

    /// `bias_correction`: m_hat_t = m_t / (1 - beta1^t), v_hat_t = v_t / (1 - beta2^t)
    /// Domain: t >= 1, beta1 in (0,1), beta2 in (0,1)
    /// Codomain: m_hat_t in R^d, v_hat_t in R_>=0^d
    /// Invariant: Correction factor > 1 for all t >= 1
    /// Invariant: Correction approaches 1 as t -> inf
    fn bias_correction(&self, input: &[f32]) -> Vec<f32>;

    /// `weight_update`: theta_t = theta_{t-1} - lr * (m_hat_t / (sqrt(v_hat_t) + eps) + lambda * theta_{t-1})
    /// Domain: theta in R^d, lr > 0, lambda >= 0, eps > 0
    /// Codomain: theta_t in R^d
    /// Invariant: Weight decay applied AFTER Adam update (decoupled)
    /// Invariant: Update finite when inputs finite and eps > 0
    fn weight_update(&self, theta: &[f32]) -> Vec<f32>;
}