provable_contracts/traits/attention_kernel_v1.rs
1//! Auto-generated contract trait for `attention-kernel-v1`.
2//! Generated by: `pv scaffold --trait contracts/attention-kernel-v1.yaml`
3//! DO NOT EDIT — regenerate from YAML source.
4
5#![allow(clippy::doc_markdown)]
6
7/// Contract trait for `attention-kernel-v1` v1.0.0.
8///
9/// Scaled dot-product attention kernel
10/// Reference: Vaswani et al. (2017) Attention Is All You Need
11///
12/// Implementors must provide all 1 equation(s).
13/// Missing method = compile error. Wrong signature = compile error.
14pub trait AttentionKernelV1 {
15 /// `attention`: Attention(Q, K, V) = softmax(QK^T / √d_k) · V
16 /// Domain: Q ∈ ℝ^{n×d_k}, K ∈ ℝ^{m×d_k}, V ∈ ℝ^{m×d_v}
17 /// Codomain: ℝ^{n×d_v}
18 /// Invariant: Each row of attention weights sums to 1.0
19 /// Invariant: Attention weights ∈ (0,1)
20 /// Invariant: Output rows are convex combinations of V rows
21 fn attention(&self, q: &[f32], k: &[f32], v: &[f32]) -> Vec<f32>;
22}