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

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `gqa-kernel-v1` v1.0.0.
///
/// GQA kernel — grouped query attention with KV head broadcasting
/// Reference: Ainslie et al. (2023) GQA: Training Generalized MQT Models
/// 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 GqaKernelV1 {
    /// `gqa`: GQA(Q, K, V) = softmax(Q_g * K_h^T / sqrt(d_k)) * V_h
    /// Domain: Q in R^{n x d}, K in R^{s x d}, V in R^{s x d_v}, num_heads > 0, num_kv_heads > 0
    /// Codomain: GQA(Q, K, V) in R^{n x d}
    /// Invariant: Attention weights sum to 1 per query position (normalization)
    /// Invariant: Output is convex combination of V rows per head
    /// Invariant: GQA(kv_heads=num_heads) = standard MHA
    /// Invariant: num_heads must be divisible by num_kv_heads
    fn gqa(&self, q: &[f32], k: &[f32], v: &[f32]) -> Vec<f32>;
}