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

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `rope-kernel-v1` v1.0.0.
///
/// RoPE kernel — rotary position embeddings
/// Reference: Su et al. (2021) RoFormer: Enhanced Transformer with Rotary Position Embedding
///
/// Implementors must provide all 1 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait RopeKernelV1 {
    /// `rope`: RoPE(x, m)_{2k} = x_{2k}·cos(mθ_k) - x_{2k+1}·sin(mθ_k), RoPE(x, m)_{2k+1} = x_{2k}·sin(mθ_k) + x_{2k+1}·cos(mθ_k)
    /// Domain: x ∈ ℝ^d, m ∈ ℕ, θ_k = 10000^(-2k/d)
    /// Codomain: ℝ^d
    /// Invariant: ‖RoPE(x, m)‖ = ‖x‖ (norm preservation)
    /// Invariant: ⟨RoPE(q, m), RoPE(k, n)⟩ depends only on q, k, m-n (relative position)
    fn rope(&self, x: &[f32], m: &[f32]) -> Vec<f32>;
}