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

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `attention-kernel-v1` v1.0.0.
///
/// Scaled dot-product attention kernel
/// Reference: Vaswani et al. (2017) Attention Is All You Need
///
/// Implementors must provide all 1 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait AttentionKernelV1 {
    /// `attention`: Attention(Q, K, V) = softmax(QK^T / √d_k) · V
    /// Domain: Q ∈ ℝ^{n×d_k}, K ∈ ℝ^{m×d_k}, V ∈ ℝ^{m×d_v}
    /// Codomain: ℝ^{n×d_v}
    /// Invariant: Each row of attention weights sums to 1.0
    /// Invariant: Attention weights ∈ (0,1)
    /// Invariant: Output rows are convex combinations of V rows
    fn attention(&self, q: &[f32], k: &[f32], v: &[f32]) -> Vec<f32>;
}