aprender-contracts 0.31.2

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
30
31
32
33
34

use serde::{Deserialize, Serialize};
use std::collections::BTreeMap;

/// Typed shape contract for compositional verification across contract boundaries.
///
/// Used in `Equation.assumes` and `Equation.guarantees` to create
/// mechanically verifiable edges in the dependency graph. The COMPOSITION-001
/// lint gate unifies `guarantees.shapes` with downstream `assumes.shapes`
/// to prove end-to-end pipeline shape consistency.
#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct ShapeContract {
    /// Named shape bindings, e.g. `{"output": {"dims": ["batch", "seq", "config.hidden_size"]}}`.
    #[serde(default)]
    pub shapes: BTreeMap<String, ShapeExpr>,
    /// Constraints that must hold, e.g. `["config.hidden_size % config.num_heads == 0"]`.
    #[serde(default)]
    pub constraints: Vec<String>,
    /// Which upstream contract provides these shapes (assumes only).
    #[serde(default)]
    pub from_contract: Option<String>,
    /// Which upstream equation provides these shapes (assumes only).
    #[serde(default)]
    pub from_equation: Option<String>,
}

/// A tensor shape expression with dimension list and optional dtype.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ShapeExpr {
    /// Dimension expressions, e.g. `["batch", "seq", "config.num_heads * config.head_dim"]`.
    pub dims: Vec<String>,
    /// Optional dtype constraint, e.g. `"config.compute_dtype"` or `"f32"`.
    #[serde(default)]
    pub dtype: Option<String>,
}