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

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `flash-attention-v1` v1.0.0.
///
/// Flash Attention — IO-aware exact attention with tiling
/// Reference: Dao et al. (2022) FlashAttention: Fast and Memory-Efficient Exact Attention with IO-Awareness
/// Reference: Dao (2023) FlashAttention-2: Faster Attention with Better Parallelism and Work Partitioning
///
/// Implementors must provide all 1 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait FlashAttentionV1 {
    /// `flash_attention`: FlashAttn(Q, K, V) = softmax(QK^T / √d_k) · V (computed in tiles)
    /// Domain: Q ∈ ℝ^{N×d}, K ∈ ℝ^{N×d}, V ∈ ℝ^{N×d}
    /// Codomain: ℝ^{N×d}
    /// Invariant: Output = standard attention output (exact, not approximate)
    /// Invariant: Memory usage O(N) not O(N²)
    /// Invariant: Online softmax: running max and sum across tiles
    fn flash_attention(&self, q: &[f32], k: &[f32], v: &[f32]) -> Vec<f32>;
}