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
25
26
27
28
29

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

#![allow(clippy::doc_markdown)]

/// Contract trait for `matmul-kernel-v1` v1.0.0.
///
/// Matrix multiplication kernel — general and quantized variants
/// Reference: Goto & van de Geijn (2008) Anatomy of High-Performance Matrix Multiplication
/// Reference: Dettmers et al. (2022) LLM.int8(): 8-bit Matrix Multiplication for Transformers
///
/// Implementors must provide all 2 equation(s).
/// Missing method = compile error. Wrong signature = compile error.
pub trait MatmulKernelV1 {
    /// `matmul`: C_{ij} = Σ_k A_{ik} · B_{kj}
    /// Domain: A ∈ ℝ^{m×p}, B ∈ ℝ^{p×n}
    /// Codomain: C ∈ ℝ^{m×n}
    /// Invariant: C has shape (m, n)
    /// Invariant: Matmul is associative: (AB)C = A(BC)
    /// Invariant: Matmul distributes over addition: A(B+C) = AB + AC
    fn matmul(&self, a: &[f32], b: &[f32]) -> Vec<f32>;

    /// `quantized_dot`: q_dot(a, b, s_a, s_b) = s_a · s_b · Σ_k a_k · b_k
    /// Domain: a, b ∈ ℤ^n (int8), s_a, s_b ∈ ℝ (scales)
    /// Codomain: ℝ
    /// Invariant: |q_dot - f32_dot| ≤ quantization_error_bound
    fn quantized_dot(&self, b: &[f32], s_b: f32) -> Vec<f32>;
}