# Provable Contracts System — Coverage Analysis
**Date:** 2026-02-23
**Project:** aprender + provable-contracts ecosystem
**Status:** 89 YAML contracts, 13,178 lines, 284 bindings (97.5% implemented)
---
## Executive Summary
The **provable-contracts** system is a comprehensive contract framework that formalizes ML/transformer math into YAML intermediaries, code generation, and Kani proof verification.
**Current Coverage:** 89 contracts across kernels, architectures, model families, and quantization
- **Kernel Class A-E:** All attention variants formalized (GQA, RMSNorm, SiLU, SwiGLU, RoPE, LayerNorm, GELU)
- **Model Families:** Qwen2, Qwen3, Qwen3.5, Qwen3-MoE (shapes + RoPE + config)
- **Data Contracts:** Tensor layout, quantization ordering, SafeTensors validation
- **Architecture Dispatch:** Per-architecture constraints (LayerNorm vs RMSNorm, GELU vs SiLU, etc.)
**Missing/Incomplete:**
1. **Tokenizer contracts** — special tokens, vocab size, BPE merge rules
2. **EOS/BOS/PAD token registry** — currently hardcoded per-model
3. **Chat template semantics** — template language, marker ordering
4. **Model metadata plausibility bounds** — vocab size ranges, position embeddings
5. **Cross-model equivalence** — consistency rules between SafeTensors and GGUF
---
## Critical Findings
### Finding 1: 89 YAML Contracts, 284 Bindings
- **Kernel contracts:** 26/26 complete with bindings
- **Architecture contracts:** 20/20 complete
- **ML algorithm contracts:** 16/16 complete
- **Data/format contracts:** 9/11 complete (2 partial)
- **E2E verification:** 4/8 complete (4 partial)
### Finding 2: ZERO Tokenizer Contracts
All special token IDs, vocab sizes, and BPE merge rules are hardcoded in Rust:
- No YAML contract for EOS/BOS/PAD token IDs per model
- No vocab size registry (Qwen2: 151643, LLaMA: 128000, Phi: 32064)
- No BPE merge rule validation
- Risk: Silent failures in token generation (infinite loops with wrong EOS)
### Finding 3: Missing Metadata Validation Contract
Plausibility bounds exist as ad-hoc checks but no formal contract:
- Vocab size bounds: 1000 < vocab < 500000
- Head dimension: must be even, typically 128
- RoPE theta: typically 10000, 100000, 1000000
- Max position: 512 to 1M
### Finding 4: Chat Template Format Not Formalized
6+ formats (ChatML, HF, Zephyr, Mistral) implemented in Rust with heuristic detection:
- detect_format_from_tokens() infers format from special_tokens
- No formal grammar or proof of correctness
- Risk: Silently wrong format → garbage token sequences
### Finding 5: Tensor Name Registry Incomplete
tensor-inventory-v1.yaml exists but missing per-architecture naming:
- GGUF standard names vary (model.embed_tokens vs token_embd)
- No Qwen, Mistral, Phi naming rules (only LLaMA)
- Critical for format conversion (GGUF → SafeTensors → APR)
---
## Detailed Inventory
### Tier 1: Kernel Contracts (26) ✅ COMPLETE
- attention-kernel-v1.yaml ✅
- gqa-kernel-v1.yaml ✅
- flash-attention-v1.yaml ✅
- activation-kernel-v1.yaml ✅
- gelu-kernel-v1.yaml ✅
- silu-kernel-v1.yaml ✅
- swiglu-kernel-v1.yaml ✅
- layernorm-kernel-v1.yaml ✅
- rmsnorm-kernel-v1.yaml ✅
- batchnorm-kernel-v1.yaml ✅
- rope-kernel-v1.yaml ✅
- absolute-position-v1.yaml ✅
- alibi-kernel-v1.yaml ✅
- matmul-kernel-v1.yaml ✅
- q4k-q6k-superblock-v1.yaml ✅
- f16-conversion-v1.yaml ✅
- cross-entropy-kernel-v1.yaml ✅
- softmax-kernel-v1.yaml ✅
- adamw-kernel-v1.yaml ✅
- lbfgs-kernel-v1.yaml ✅
- bias-add-v1.yaml ✅
- dropout-v1.yaml ✅
- attention-scaling-v1.yaml ✅
- linear-projection-v1.yaml ✅
- embedding-lookup-v1.yaml ✅
- embedding-algebra-v1.yaml ✅
### Tier 2: Architecture Contracts (20) ✅ COMPLETE
- arch-constraints-v1.yaml ✅
- model-config-algebra-v1.yaml ✅
- qwen2-shapes-v1.yaml ✅
- qwen35-shapes-v1.yaml ✅
- qwen35-hybrid-forward-v1.yaml ✅
- qwen3-shapes-v1.yaml ✅
- qwen3moe-shapes-v1.yaml ✅
- rope-kernel-v1.yaml ✅
- rope-extrapolation-v1.yaml ✅
- qk-norm-v1.yaml ✅
- gated-delta-net-v1.yaml ✅
### Tier 3: ML Algorithm Contracts (16) ✅ COMPLETE
- linear-models-v1.yaml ✅
- decision-tree-v1.yaml ✅
- random-forest-v1.yaml ✅
- gbm-v1.yaml ✅
- kmeans-kernel-v1.yaml ✅
- pca-v1.yaml ✅
- ica-v1.yaml ✅
- bayesian-v1.yaml ✅
- naive-bayes-v1.yaml ✅
- svm-v1.yaml ✅
- glm-v1.yaml ✅
- calibration-v1.yaml ✅
- metrics-classification-v1.yaml ✅
- metrics-regression-v1.yaml ✅
- metrics-clustering-v1.yaml ✅
- metrics-ranking-v1.yaml ✅
### Tier 4: Time Series / Specialized (8) ✅ COMPLETE
- arima-v1.yaml ✅
- drift-detection-v1.yaml ✅
- active-learning-v1.yaml ✅
- cma-es-kernel-v1.yaml ✅
- metaheuristics-v1.yaml ✅
- shannon-entropy-v1.yaml ✅
- optimization-v1.yaml ✅
- performance-grading-v1.yaml ✅
### Tier 5: Data/Format Contracts (11) — 9 COMPLETE, 2 PARTIAL
- aprender/tensor-layout-v1.yaml ✅
- aprender/quantized-dot-product-v1.yaml ✅
- aprender/binding.yaml ✅ (284 bindings, 97.5% implemented)
- aprender/kernel-fusion-v1.yaml ✅
- aprender/layer-parity-v1.yaml ✅
- format-parity-v1.yaml ✅
- kv-cache-equivalence-v1.yaml ✅
- kv-cache-sizing-v1.yaml ✅
- validated-tensor-v1.yaml ✅
- inference-pipeline-v1.yaml ⚠️ PARTIAL (missing tokenizer/generation)
- tensor-inventory-v1.yaml ⚠️ PARTIAL (only LLaMA names, missing Qwen/Mistral/Phi)
### Tier 6: E2E Verification (8) — 4 COMPLETE, 4 PARTIAL
- qwen2-e2e-verification-v1.yaml ✅
- qwen35-e2e-verification-v1.yaml ✅
- qwen3-e2e-verification-v1.yaml ✅
- qwen3moe-e2e-verification-v1.yaml ✅
- backend-dispatch-v1.yaml ⚠️ PARTIAL
- roofline-model-v1.yaml ⚠️ PARTIAL
- hybrid-layer-dispatch-v1.yaml ⚠️ PARTIAL
- kernel-launch-budget-v1.yaml ⚠️ PARTIAL
---
## CRITICAL GAPS
### Gap 1: Tokenizer Contracts (100% MISSING) ❌
**What's Hardcoded:**
- Qwen2 BPE merge rules in aprender/src/text/bpe/qwen2.rs
- LLaMA tokenizer in aprender/src/text/llama_tokenizer/mod.rs
- Chat template format detection (heuristic)
- Special token IDs scattered across format/converter/tokenizer_loader.rs
**Should Be Contracts:**
1. special-tokens-registry-v1.yaml — EOS/BOS/PAD per model
2. tokenizer-vocab-v1.yaml — Vocab size + merge rule ordering
3. chat-template-semantics-v1.yaml — Format grammar + execution
**Impact:**
- Missing EOS ID → infinite token generation loops
- Missing vocab validation → accepts 94.5% zero tensors (PMAT-234)
- Missing chat template → silent wrong format → garbage output
### Gap 2: Model Metadata Bounds (PARTIAL) ⚠️
**What's Hardcoded:**
Validation checks in format/converter/gguf_import.rs without contracts:
- vocab_size < 1000 || vocab_size > 500000 (ad-hoc)
- rope_theta checks (implicit)
- max_position validation (implicit)
**Should Be Contract:**
model-metadata-bounds-v1.yaml:
- Vocab size: 1000 < v < 500000
- Head dim: even, typically 64-512
- RoPE theta: 100 < theta < 1e7
- Max position: 512 to 1e6
- FFN expansion: intermediate > hidden
**Impact:**
- F-QA-008 metadata plausibility gate not formalized
- Cannot generate falsification tests
- Cannot enable Kani proofs
### Gap 3: Tensor Name Registry (PARTIAL) ⚠️
**Current State:**
tensor-inventory-v1.yaml exists but incomplete:
- Only LLaMA naming rules documented
- Missing GGUF standard variations
- Missing Qwen, Mistral, Phi naming
**Example Gap:**
```yaml
# MISSING: Per-architecture naming rules
qwen:
embedding: "model.embed_tokens.weight" # GGUF: "token_embd.weight"
q_proj: "model.layers.{i}.self_attn.q_proj.weight"
mlp_gate: "model.layers.{i}.mlp.gate_proj.weight"
mistral:
embedding: "model.embed_tokens.weight"
q_proj: "model.layers.{i}.self_attn.q_proj.weight"
mlp_gate: "model.layers.{i}.mlp.w1.weight"
```
**Impact:**
- apr convert fails on Qwen/Mistral (only LLaMA supported)
- Silent tensor name mismatches
### Gap 4: Chat Template Semantics (MISSING CONTRACT) ❌
**Current Implementation:**
- 6+ formats: ChatML, HF, Zephyr, Mistral, Phi, etc.
- Heuristic detection via detect_format_from_tokens()
- No formal grammar or proof
**Example Hardcoding:**
```rust
// src/text/chat_template/raw_template.rs
pub fn detect_format_from_tokens(special_tokens: &HashMap<String, u32>) -> TemplateFormat {
if special_tokens.contains_key("im_start") {
TemplateFormat::ChatML // Qwen
} else if special_tokens.contains_key("bos_token") {
TemplateFormat::HuggingFace
} // ... more heuristics
}
```
**Should Be Contract:**
chat-template-semantics-v1.yaml with:
- Formal grammar for each format
- Proof obligations for marker ordering
- Falsification tests
**Impact:**
- Currently heuristic detection can fail silently
- Cannot verify all markers present
- Cannot validate message ordering
### Gap 5: Format Equivalence (PARTIAL) ⚠️
**Current State:**
format-parity-v1.yaml exists but missing:
- No formal transposition proof (GGUF col-major → APR row-major)
- No quantization format equivalence (GGUF Q4_K vs APR Q4)
- No naming transformation rules
**Related Bugs:**
- GH-208: APR garbage from wrong transpose
- PMAT-234: SafeTensors 94.5% zeros accepted
- LAYOUT-001: Row-major contract not enforced
**Impact:**
- Format conversion unreliable
- Cannot publish with confidence
---
## Models Needing Contracts
### Special Token Registry Needed For:
1. Qwen2 (vocab: 151643, pad: 151643, eos: 151643, bos: 151644)
2. Qwen3 (vocab: 152000)
3. Qwen3-Coder (vocab: 152000)
4. Qwen3.5 (vocab: 152064)
5. LLaMA 3.2 (vocab: 128000, pad: 128001, eos: 128001, bos: 128000)
6. Mistral (vocab: 32000, pad: 0, eos: 2, bos: 1)
7. Phi-3 (vocab: 32064)
8. Whisper (vocab: 51864 multi-language)
### Tensor Name Registry Needed For:
1. Qwen (c_attn [QKV], c_proj [O], w2 [down], w1 [gate], c_fc [up])
2. Mistral (q_proj, k_proj, v_proj, o_proj, w1 [gate], v_proj [up], w2 [down])
3. Phi (q_proj, k_proj, v_proj, o_proj, fc1 [up], fc2 [down])
4. Whisper (q, k, v, out, mlp_0 [up], mlp_2 [down])
---
## Prioritization: Contracts to Create
### P0 — Publishing Blockers (MUST HAVE) 🔴
1. **special-tokens-registry-v1.yaml** (2 weeks)
- EOS/BOS/PAD IDs for all 101+ models
- Prevents infinite token generation loops
- Use in: aprender/src/format/converter/tokenizer_loader.rs
- Tests: proptest that token IDs < vocab_size
2. **model-metadata-bounds-v1.yaml** (1 week)
- Vocab size, head dim, rope_theta, max_position bounds
- Formalizes F-QA-008 metadata plausibility gate
- Use in: aprender/src/format/converter/gguf_import.rs
- Tests: falsification for each bound
3. **tokenizer-vocab-v1.yaml** (2 weeks)
- Per-model vocab size + BPE merge rule ordering
- Validates encoding consistency
- Use in: aprender/src/text/bpe/mod.rs
- Tests: proptest merge frequency monotonicity
### P1 — Quality Improvements (SHOULD HAVE) 🟠
4. **chat-template-semantics-v1.yaml** (2 weeks)
- Grammar for ChatML, HF, Mistral, Phi, Zephyr
- Replaces heuristic detection
- Use in: aprender/src/text/chat_template/mod.rs
- Tests: proptest format → tokens → decode roundtrip
5. **tensor-inventory-v1.yaml expansion** (1 week)
- Add Qwen, Mistral, Phi naming rules
- Complete GGUF standard names section
- Use in: aprender/src/format/converter/mod.rs
- Tests: proptest naming transformation consistency
6. **format-parity-v1.yaml expansion** (2 weeks)
- Add transposition proof (col-major → row-major)
- Add quantization equivalence (GGUF vs APR formats)
- Use in: aprender/src/format/converter/write.rs
- Tests: comparative property tests (GGUF vs APR outputs)
### P2 — Future Proofing (NICE TO HAVE) 🟡
7. **backend-dispatch-v1.yaml expansion** (2 weeks)
- GPU ↔ CPU numeric equivalence (tolerance bounds)
- Layout agreement (contiguous, aligned)
8. **kernel-launch-budget-v1.yaml** (2 weeks)
- GPU kernel cost model
- Automatic kernel selection
---
## Hardcoded Values in aprender/src
### Vocab Sizes (NO CONTRACT)
```rust
// Should move to special-tokens-registry-v1.yaml
const QWEN2_VOCAB: usize = 151643;
const QWEN3_VOCAB: usize = 152000;
const LLAMA3_VOCAB: usize = 128000;
const PHI3_VOCAB: usize = 32064;
const MISTRAL_VOCAB: usize = 32000;
```
### Special Token IDs (NO CONTRACT)
```rust
// Should move to special-tokens-registry-v1.yaml
// Currently in: format/converter/tokenizer_loader.rs
const QWEN2_PAD: u32 = 151643;
const QWEN2_EOS: u32 = 151643;
const QWEN2_BOS: u32 = 151644;
const LLAMA_PAD: u32 = 128001;
const LLAMA_EOS: u32 = 128001;
const LLAMA_BOS: u32 = 128000;
```
### RoPE Theta (IN CONTRACTS, incomplete)
```rust
// Qwen2: 1_000_000.0
// LLaMA: 500_000.0 (Llama-3.1 → 500k)
// Mistral: 10_000.0
// Should be: model-metadata-bounds-v1.yaml standardized values
```
### Chat Template Markers (NO CONTRACT)
```rust
// Currently: heuristic detection in detect_format_from_tokens()
// Should be: chat-template-semantics-v1.yaml
const MISTRAL_INST_START: &str = "[INST] ";
const MISTRAL_INST_END: &str = " [/INST]";
```
---
## Summary Table
| Kernels | 26 | 100% ✅ | No |
| Architecture | 20 | 100% ✅ | No |
| ML Algorithms | 16 | 100% ✅ | No |
| Time Series | 8 | 100% ✅ | No |
| Data/Format | 11 | 82% | No (2 partial) |
| E2E Verify | 8 | 50% | No |
| **Tokenizers** | **0** | **0% ❌** | **YES — P0** |
| **Metadata Bounds** | **0** | **0% ❌** | **YES — P0** |
| **Chat Templates** | **0** | **0% ❌** | **No (heuristic works)** |
| **Tensor Names** | **1 (partial)** | **33%** | **No (LLaMA works)** |
| **TOTAL** | **89** | **81%** | **2 P0 blockers** |
---
## References
- **Provable Contracts Dir:** `/home/noah/src/provable-contracts/`
- **89 YAML Contracts:** `/home/noah/src/provable-contracts/contracts/`
- **Binding Registry (284 bindings):** `/home/noah/src/provable-contracts/contracts/aprender/binding.yaml`
- **Model Config Algebra:** `/home/noah/src/provable-contracts/contracts/model-config-algebra-v1.yaml`
- **Architecture Constraints:** `/home/noah/src/provable-contracts/contracts/arch-constraints-v1.yaml`
- **Tensor Layout Contract:** `/home/noah/src/provable-contracts/contracts/aprender/tensor-layout-v1.yaml`