provable_contracts/schema/
composition.rs

1use serde::{Deserialize, Serialize};
2use std::collections::BTreeMap;
3
4/// Typed shape contract for compositional verification across contract boundaries.
5///
6/// Used in `Equation.assumes` and `Equation.guarantees` to create
7/// mechanically verifiable edges in the dependency graph. The COMPOSITION-001
8/// lint gate unifies `guarantees.shapes` with downstream `assumes.shapes`
9/// to prove end-to-end pipeline shape consistency.
10#[derive(Debug, Clone, Default, Serialize, Deserialize)]
11pub struct ShapeContract {
12    /// Named shape bindings, e.g. `{"output": {"dims": ["batch", "seq", "config.hidden_size"]}}`.
13    #[serde(default)]
14    pub shapes: BTreeMap<String, ShapeExpr>,
15    /// Constraints that must hold, e.g. `["config.hidden_size % config.num_heads == 0"]`.
16    #[serde(default)]
17    pub constraints: Vec<String>,
18    /// Which upstream contract provides these shapes (assumes only).
19    #[serde(default)]
20    pub from_contract: Option<String>,
21    /// Which upstream equation provides these shapes (assumes only).
22    #[serde(default)]
23    pub from_equation: Option<String>,
24}
25
26/// A tensor shape expression with dimension list and optional dtype.
27#[derive(Debug, Clone, Serialize, Deserialize)]
28pub struct ShapeExpr {
29    /// Dimension expressions, e.g. `["batch", "seq", "config.num_heads * config.head_dim"]`.
30    pub dims: Vec<String>,
31    /// Optional dtype constraint, e.g. `"config.compute_dtype"` or `"f32"`.
32    #[serde(default)]
33    pub dtype: Option<String>,
34}
provable_contracts/schema/composition.rs

provable_contracts/schema/
composition.rs
