# Commit-Level Contract Enforcement & Asset Contracts

> Sub-spec of [pmat-spec.md](../pmat-spec.md) | Component 25

## Root-Cause Analysis: Why Contracts Don't Gate Commits

Five Whys (2026-04-05):

1. **Why can developers commit code that violates provable-contracts?**
   Pre-commit hooks check formatting and complexity, not contract obligations.
2. **Why don't pre-commit hooks check contracts?**
   `pmat work` has `contract.json` (DbC v5.0) and `provable-contracts` has
   separate YAML — two parallel systems that never merge at commit time.
3. **Why two parallel systems?**
   `pmat work` was built for task-level falsification; `provable-contracts`
   for kernel-level formal verification. Neither enforces the other at git boundary.
4. **Why is the git boundary unguarded?**
   Contract verification was assumed to be a CI concern, not a commit concern.
5. **Why isn't CI sufficient?**
   CI runs minutes after commit. Developer has context-switched. AWS Cedar
   (ICSE 2025) documents "proof brittleness" — proofs break from unrelated
   commits. The fix: **shift-left** to commit time.

**The fix:** Unify both contract systems under a single commit-level enforcement
pipeline. Extend to non-code assets with layout contracts. All checks O(1)
from cached metrics — no cold verification in the commit path.

---

## Design Principles

### O(1) Firm Requirement

**Every pre-commit check MUST complete in < 30ms from cached data.** No check
may invoke `cargo build`, `cargo test`, `pv lint` (cold), or network calls.
All verification data pre-computed during development and cached in `.pmat/`.

| Check Category | Data Source | Latency |
|----------------|------------|---------|
| Contract obligation status | `.pmat/contract-cache.json` | < 5ms |
| L-level ratchet | `.pmat/verification-levels.json` | < 3ms |
| Asset layout validation | `.pmat/asset-layout-cache.json` | < 10ms |
| Binding diff lookup | `.pmat/binding-index.json` | < 5ms |
| Staleness gate | File mtime comparison | < 1ms |

**Staleness policy:** >7 days = warning, >30 days = error. Emergency bypass:
`git commit --no-verify` (logged in `.pmat-metrics/bypass-log.jsonl`).

### Provable-Contracts as Single Source of Truth

All enforcement flows through provable-contracts YAML. `pmat work` contract.json
becomes a **derived view** — generated from and validated against authoritative YAML.

### rmedia Grid Protocol Paradigm

Non-code assets follow the rmedia model: **content never exists without a
placement contract**. Every README section, Dockerfile block, SVG group, and
book chapter occupies a named slot with typed constraints.

---

## Phase 1: Work Item to YAML Contract Generation

When `pmat work start` creates a work item, it generates both `contract.json`
(DbC v5.0) and `contracts/work/<ID>.yaml` (provable-contracts schema), bridging
task-level falsification with the verification ladder.

**Mapping:** `require[]` → preconditions, `ensure[]` → postconditions,
`invariant[]` → invariants, `falsification_method` → `falsification_tests[].method`,
`verification_level` → `verification_summary.target_level`.

**Cache population:** `pmat work start` and `pmat work checkpoint` write
`.pmat/contract-cache.json` with active work item status, obligation counts,
and verification timestamps for O(1) pre-commit lookup.

**CLI:** `pv validate contracts/work/<ID>.yaml` validates schema,
`pv score` scores quality, `pv audit` checks traceability chain.

---

## Phase 2: Verification Level Monotonicity Ratchet

Each binding in `binding.yaml` carries a verification level (L0-L5). The
ratchet ensures levels **never decrease**, preventing deletion of Kani
harnesses or Lean proofs.

**Mechanism:** Pre-commit reads `.pmat/verification-levels.json` (O(1)),
looks up affected bindings for staged files, blocks if any L-level decreased,
warns if stale (>7 days).

| Transition | Allowed? | Rationale |
|-----------|----------|-----------|
| L1→L2, L2→L3, L3→L4 | Yes | Progress |
| L3→L2, L4→L3 | **BLOCKED** | Regression |
| Any→L0 | **BLOCKED** | Total regression |

**Escape hatch:** `pmat comply ratchet-override --binding <fn> --from L4 --to L2
--reason "..." --work-item <ID>` writes signed entry to
`.pmat-metrics/ratchet-overrides.jsonl`, expires in 14 days. CB-1330 violation
if unrecovered by expiry.

**Basis:** Agent Behavioral Contracts (arXiv:2602.22302) Drift Bounds Theorem;
Gradual Verification (Bader et al., TOPLAS).

---

## Phase 3: Asset Layout Contracts

Non-code assets use the **container model**: every asset has named **slots**
with ID, order, type, required flag, and constraints.

### Seven Asset Types

| CB Check | Asset | Key Enforcement |
|----------|-------|-----------------|
| CB-1320 | README.md | 10 slots (7 required), ordering, accuracy, cross-refs |
| CB-1321 | Dockerfile | No `:latest`, no `curl\|bash`, multi-stage, pinned deps |
| CB-1322 | SVG | ViewBox validation, 6-color palette, element budget, WCAG |
| CB-1323 | forjar.yaml | DAG acyclicity, template resolution, no plaintext secrets |
| CB-1324 | mdBook | SUMMARY link integrity, code block compilation, cross-refs |
| CB-1325 | CHANGELOG | Keep-a-Changelog format, semver ordering |
| CB-1326 | Badges | Required set present, URLs live, header placement |

Each asset type has a contract YAML defining slots, constraints, and
falsification tests. Contracts follow the provable-contracts schema with
`surface: asset-layout` and enforcement levels.

**README (CB-1320):** Slots: header, badges, description, installation, usage,
benchmarks, architecture, api, contributing, license, footer. Accuracy checks
via regex matching against `pmat --version`, `cargo test` output, and coverage
data. Cross-ref validation ensures claimed files exist.

**Dockerfile (CB-1321):** Instruction blocks map to slots: base-image,
dependencies, build-stage, runtime-stage. Security checks: no `curl|bash`,
no root USER, pinned apt versions.

**O(1) cache:** All asset validation runs during `pmat work checkpoint` or
`pmat asset validate`. Results cached in `.pmat/asset-layout-cache.json` for
pre-commit lookup.

---

## Phase 4: Differential Obligation Verification

Full contract verification is expensive. At commit time, only obligations whose
bound functions were modified need re-checking.

**Mechanism:** `git diff --cached --name-only` → lookup in
`.pmat/binding-index.json` (file→binding reverse index) → check cached verdicts
for affected obligations → PASS/FAIL from cache.

**Binding index:** Maps source files to their contract bindings and
obligations. Maps asset files to layout contracts. Rebuilt by
`pmat comply refresh-bindings` or `pmat comply refresh-contracts`.

**Basis:** Mugnier et al. (OOPSLA 2025) documents proof brittleness from
whole-contract reverification; AWS Cedar (ICSE 2025) confirms targeted
verification eliminates this.

---

## Phase 5: Assume-Guarantee Chains for Concurrent Work

When multiple work items touch overlapping code, one commit can break another's
assumptions. Work contracts declare dependencies via `assumes` (references
another contract's obligation) and `guarantees` (obligations this item ensures).

**Pre-commit validation:** Load active contracts → build dependency DAG →
for each modified file, find affected guarantees → check if other work items
assume those guarantees → block if guarantee broken (from cache).

**Conflict resolution:** Error message names the affected work item and
offers options: re-verify (`pmat work checkpoint`), override
(`pmat comply ratchet-override`), or bypass (`--no-verify`).

**Basis:** Pacti (ACM TCPS 2025) algebraic A/G operations; Dewes & Dimitrova
(AAAI 2025) quantitative A/G for multi-agent coordination; Dardik & Kang
(2025) compositional inductive invariant inference.

---

## Phase 6: `pmat query` Provable-Contract Enrichment

Six new flags make contract status a first-class search dimension:

| Flag | Description |
|------|-------------|
| `--contracts` | Enrich results with contract binding status |
| `--contract-gaps` | Show functions without contracts |
| `--min-level L3` | Filter: only functions at or above this level |
| `--max-level L1` | Filter: only functions at or below this level |
| `--contract-score` | Sort by contract quality score |
| `--asset-contracts` | Include non-code assets in results |

**O(1) architecture:** `ContractIndex` lazy-loaded from `.pmat/binding-index.json`
on first `--contracts` query (~500KB, <50ms load). Subsequent lookups O(1)
per result via HashMap.

**Relevance scoring:** `score = base_relevance * 0.7 + contract_signal * 0.3`.
`--contract-gaps` surfaces most undercontracted functions first.

**Composition:** All flags compose with existing enrichment (--churn, --faults,
--duplicates, --entropy, -G, --coverage, --coverage-gaps).

---

## Pre-Commit Hook Integration

All phases share a single pre-commit entry point reading cached data only.

| Phase | Max Latency | Data Source |
|-------|------------|------------|
| Format/complexity/SATD | 15ms | `.pmat-metrics/` |
| Work contract validity | 5ms | `.pmat/contract-cache.json` |
| L-level ratchet | 3ms | `.pmat/verification-levels.json` |
| Asset layout | 10ms | `.pmat/asset-layout-cache.json` |
| Differential obligations | 5ms | `.pmat/binding-index.json` |
| Assume-guarantee chains | 7ms | `.pmat/contract-cache.json` |
| **Total** | **< 45ms** | **All from cache** |

**Cache refresh:** `pmat work checkpoint <ID>` (during development),
`pmat comply refresh-contracts` (after binding changes),
`pmat asset validate` (after asset edits).

---

## Phase 7: Hook Subsystem Consolidation

### Root Cause (Five Whys)

170 hook-related commits in pmat with ~38 bug-fixes — fix-break-fix cycle.
**Why:** 6 independent codepaths write to `.git/hooks/` with no coordination
(`hook_manager.rs`, `git_hooks.rs`, `scaffold/hooks.rs`, `hooks_command.rs`,
`tdg_hooks.rs`, `hooks_stack_handler.rs`). **Why:** No hook ownership model.
**Consequence:** 72 `--no-verify` bypasses across 8 PAIML repos.

### 14 Problem Classes from Git History Audit

| # | Problem | Severity |
|---|---------|----------|
| H-1 | 6 conflicting writers, 0 coordination | Critical |
| H-2 | Non-atomic file writes (`fs::write`, not rename) | Medium |
| H-3 | Timestamps in generated hooks (non-deterministic) | Medium |
| H-4 | TOCTOU race conditions (check-then-write) | Medium |
| H-5 | Shell injection via template substitution | Medium-High |
| H-6 | HashMap non-deterministic serialization | Low-Medium |
| H-7 | Hardcoded `~/src` path assumption | Medium |
| H-8 | Self-contradictory SATD enforcement rules | Low-Medium |
| H-9 | `$?` capture fragility across shells | Low |
| H-10 | Missing `.git` directory verification | Low-Medium |
| H-11 | Inconsistent backup behavior (skip vs overwrite) | Low |
| H-12 | Read-modify-write race on cache files | Low-Medium |
| H-13 | Non-UTF-8 path collision (maps to empty string) | Low |
| H-14 | Hardcoded stack repo list | Low |

### Design Rules (CB-1333..1337)

| Rule | CB Check | Requirement | Falsification |
|------|----------|-------------|---------------|
| HR-1 Single Writer | CB-1333 | All writes through `HookRegistry` (`BTreeMap<String, HookSection>`) | `grep -rn 'fs::write.*hooks' src/ \| grep -v hook_registry.rs` → empty |
| HR-2 Atomic Writes | CB-1334 | Write-then-rename, never `fs::write()` to hook path | Kill during write → file is old or new, never partial |
| HR-3 Deterministic | CB-1335 | No timestamps, no HashMap iteration, byte-identical output | Two consecutive installs → `diff` → zero diff |
| HR-4 No Injection | CB-1336 | Template substitution escapes shell metacharacters | Set path to `$(whoami)` → literal in output |
| HR-5 Performance | CB-1337 | Pre-commit p95 < 45ms | `.pmat-metrics/hook-timing.json` tracked per run |

---

## Phase 8: Falsify Leak Remediation

### Root Cause (Five Whys)

Contracts exist that don't catch bugs because YAML→codegen→binding→call-site
is a 4-step manual pipeline where each stage leaks. `pv` commands are
fire-and-forget with no closed-loop regeneration.

### 7 Leak Classes from Provable-Contracts Git History

| Leak | Class | Evidence | Design Rule | CB Check |
|------|-------|----------|-------------|----------|
| L-1 | Ghost Bindings | 28,206 stripped in PMAT-106 (97% ghosts) | `pv infer` verified against AST before write | CB-1338 |
| L-2 | Placeholder Preconditions | 507 `!is_empty()` in PMAT-129/131 | Zero placeholder ratio for domain-specific equations | CB-1339 |
| L-3 | Zero Enforcement | Fleet avg 0.01 penetration in PMAT-133 | Repos with binding.yaml require ≥10% call-site penetration | CB-1340 |
| L-4 | Codegen Fidelity | Stale codegen, hardcoded var names | `pv codegen --check` dry-run diff in CI | CB-1211 |
| L-5 | Spec Number Inflation | 22 falsified claims in pv-spec.md | Spec numbers generated from `pv status --json` | CB-1341 |
| L-6 | Parser/Domain Bugs | `domain_to_params()` garbage names | `pv codegen --check` compiles own output | CB-1342 |
| L-7 | Assertion Placement | Preconditions before early-return guards | Preconditions placed AFTER argument validation | CB-1343 |

### Quantitative Progress

| Metric | Peak Inflated | Honest (After Strip) | Current |
|--------|--------------|---------------------|---------|
| Bindings | 28,206 | 540 (97% ghosts) | ~17,000 (verified) |
| Unique assertions | 1 (`!is_empty()`) | — | 500 domain-specific |
| Repos with enforcement | "26/26 Grade A" | 7/26 | ~18/26 |
| Enforcement rate | implied 100% | ~1% | ~60% (kaizen Grade A) |

### Dogfood Results (2026-04-06, pmat v3.11.1 + CB-1340 per-crate, falsified)

| Repo | Pass | Warn | Fail | CB-1354 | CB-1340 | Notes |
|------|------|------|------|---------|---------|-------|
| pmat | **78** | 5 | 1 | **4/4** | **39.3%** PASS (5928), 0 test fails | 99.7% pub fn + private fn waves ongoing. |
| aprender | **74** | 13 | **2** | **4/4** | 43.8% agg, apr-cli:**63%** [CLI] FAIL | FAIL: File Health + CB-1340. #686 open |
| trueno | **66** | 17 | 3 | 2/4 | Skip (no binding) | FAIL: File Health, CB-200, CB-1308 |
| realizar | **67** | 18 | **0** | 3/4 | Skip | **Zero FAIL** maintained |

**Falsification (this session):** Initial `contract_` pattern matched struct
field names (`contract_value`, `contract_name`, `contract_failures`), inflating
apr-cli from honest **63%** to false **148%**. Fixed: now matches only
`contract_pre_*`, `contract_post_*`, `#[contract`, `debug_assert!`, `requires!`,
`ensures!`. apr-cli correctly **FAILS** at 63% < 95% threshold — real gap
exposed, paiml/aprender#686 still open.

### apr-cli QA Summary (2026-04-06)

13 issues resolved (11 code fixes + 2 verified-already-fixed):

| Category | Issues | Status |
|----------|--------|--------|
| Network/offline | #663, #666 | Fixed: --offline blocks network ops |
| Server endpoints | #664, #671, #672 | Fixed: banner, CORS, JSON 404 |
| Output quality | #662, #665, #669 | Fixed: NO_COLOR, max_tokens cap, glob filter |
| Process signals | #667 | Fixed: SIGPIPE reset |
| Stale files | #668 | Fixed: rosetta_temp skip |
| UX | #660, #677 | Fixed: GGUF metadata, showcase exit code |
| Asset compliance | #675 | Fixed: SVG accessibility, README <h1> |

**Remaining open (18 total, down from 30):** GPU bugs (#573 CPU dequant path,
#471 MoE hang, #620 parity contradiction, #641 rosetta 0 tokens), infra (#477
cuda gate, #560 wgpu fallback), perf (#386 SIMD dequant, #434 OOM quantize,
#478 32B OOM), features (#326 BERT, #367 InternLM, #393 hetero training,
#428 online SGD, #540 Grade A refactor, #537 bug-hunter findings, #566
finetune metrics, #574 tracing, #575 Whisper).

### Five Whys: Why Doesn't pmat comply Catch apr-cli Bugs?

56 bugs fixed on aprender — 35 (63%) were contract-catchable. Root cause:
pmat comply checks contract *infrastructure* (YAML existence), not *behavior*
(does code obey?). `#[contract]` proc_macro exists and works — aprender root
at 35% penetration (honest, post-falsification). apr-cli at 63% needs 95%.
Gap: 48 command handlers need per-command Level A coverage (#686).

| Defect Class | Count | Contract Catchable? | Fix |
|-------------|-------|--------------------|----|
| Silent failure (exit 0) | 11 | **YES** — postcondition on exit code | `#[contract(ensures = "exit != 0 on error")]` |
| Wrong output | 11 | **PARTIAL** — type constraints, not semantics | Bounded model checking (Kani L4) |
| Flag ignored | 10 | **YES** — behavioral preconditions | `#[contract(requires = "offline => !network")]` |
| Missing feature | 6 | **NO** — contracts verify, not specify | Spec-driven development |
| Missing guard | 5 | **YES** — input preconditions | `#[contract(requires = "!path.ends_with(.enc)")]` |
| Format leak | 3 | **YES** — output postconditions | `#[contract(ensures = "!msg.contains(type_name)")]` |

### apr-cli Level A Enforcement Policy (2026-04-06)

**MANDATORY: ALL 48 apr-cli commands require Level A fixes ONLY.**

Level A = TDG Grade A (score 0.0–0.2) + L3 provable-contracts enforcement
(build.rs + traits + `#[contract]` proc_macro). No command ships at Grade B
or below. No command ships without provable-contracts coverage.

**Enforcement chain** (via `../provable-contracts`):

| Requirement | Threshold | Enforcement |
|-------------|-----------|-------------|
| TDG Grade | **A** (0.0–0.2) for every command handler | `pmat analyze complexity --file` |
| Contract YAML | Every command in `contracts/aprender/apr-*.yaml` | `pv lint` |
| Enforcement level | **L3 minimum** (build.rs + traits) for all 48 commands | CB-1208 |
| `#[contract]` annotation | **100%** of command entry points (`dispatch_core_command` arms) | CB-1203 |
| Precondition coverage | Domain-specific (not placeholder) for all equations | CB-1210, CB-1211 |
| Postcondition coverage | Exit code + output validity for all commands | CB-1214 E2 |
| Falsification tests | Every command has ≥1 FALSIFY test | Contract YAML `falsification_tests` |
| Kani harness | All proof obligations at L4+ for critical paths | CB-1205 |

**Per-command contract requirements:**

| Command Class | Contract YAML | Required Annotations |
|---------------|--------------|---------------------|
| ReadOnly (28 cmds) | `apr-cli-operations-v1` | `#[contract(ensures = "no_side_effects")]` on handler |
| Mutating (16 cmds) | `apr-cli-operations-v1` | `#[contract(requires = "output_path.is_some()")]`, `#[contract(ensures = "exit != 0 on error")]` |
| LongRunning (4 cmds: run, serve, chat, tui) | `apr-serve-v1`, `apr-chat-session-v1` | `#[contract(ensures = "graceful_shutdown")]`, `#[contract(ensures = "resource_cleanup")]` |
| Sampling (run, serve) | `apr-cli-sampling-v1` | `#[contract(requires = "temperature >= 0.0")]`, `#[contract(ensures = "deterministic if seed set")]` |
| Data (tokenize, pipeline, data) | `apr-data-pipeline-v1` | `#[contract(ensures = "roundtrip_fidelity")]` |
| Training (train plan/apply/watch/sweep) | `apr-finetune-v1` | `#[contract(ensures = "loss_monotonic")]`, `#[contract(requires = "valid_config")]` |
| Format (import, export, convert) | `apr-format-safety-v1` | `#[contract(ensures = "format_valid")]`, `#[contract(requires = "input_exists")]` |
| GPU (compile, ptx, ptx-map, parity) | `apr-gpu-backend-v1` | `#[contract(ensures = "gpu_parity")]`, `#[contract(requires = "backend_available")]` |

**Graduation criteria** (command moves from open→closed):

1. Contract YAML exists with domain-specific pre/postconditions (not placeholders)
2. `#[contract]` proc_macro annotation on handler entry point
3. Binding in `contracts/aprender/binding.yaml` with `status: implemented`
4. ≥1 falsification test in contract YAML
5. TDG score ≤ 0.2 (Grade A) on handler function
6. `pmat comply check` passes with 0 FAIL on the command's contract

**What this replaces:** The previous P0–P2 tiered approach allowed Grade B/C
commands to ship. That approach produced 56 bugs in aprender, 35 of which
were contract-catchable. Level A enforcement eliminates the "ship now, contract
later" pattern that caused 63% of preventable defects.

**Tracking issues** (filed 2026-04-06):
- paiml/aprender#686 — Master: 0 `#[contract]` in apr-cli crate (48 commands)
- paiml/aprender#687 — 4 contracts stuck at L4, need L5 (Lean proofs)
- paiml/aprender#688 — ReadOnly commands (28) need no_side_effects annotation
- paiml/aprender#689 — Mutating commands (16) need exit-code postconditions
- paiml/aprender#690 — LongRunning commands (4) need graceful_shutdown
- paiml/aprender#691 — CB-1340 should report per-crate penetration (pmat enhancement)
- paiml/aprender#697 — Cross-subcmd GPU parity contract (parity vs ptx-map, #620)
- paiml/aprender#698 — `apr run --gpu` must use CUDA Q4K not CPU dequant (#573)
- paiml/aprender#699 — rosetta compare-inference exits 0 with 0 tokens (#641)

### Recommendations (P0)

1. Annotate all 48 command handlers with `#[contract]` (apr-cli entry points: #686)
2. Upgrade apr-cli bindings to L3 in `binding.yaml` (4 stuck at L4→L5: #687)
3. Add `exit != 0 on error` postcondition to all 48 commands (11 silent failures)
4. Behavioral preconditions for flag handling (10 flag-ignored bugs)

---

## TDG Integration

Extend TDG to grade non-code assets contributing to project-level aggregate:

| Asset | TDG Dimensions | Weight |
|-------|----------------|--------|
| README.md | Completeness 40%, accuracy 30%, freshness 20%, links 10% | 0.15 |
| Dockerfile | Security 40%, layers 30%, pinning 20%, metadata 10% | 0.05 |
| SVG | Structure 50%, accessibility 30%, palette 20% | 0.02 |
| CHANGELOG | Format 50%, version consistency 30%, completeness 20% | 0.03 |
| forjar.yaml | DAG validity 40%, secrets 30%, templates 30% | 0.05 |

---

## CB Check Summary

26 checks across 8 phases (falsified from 29). Phase 3: CB-1320..1326 (asset layout — README,
Dockerfile, SVG, forjar, mdBook, CHANGELOG, badges). Phase 2: CB-1330
(L-level ratchet). Phase 1: CB-1331 (work YAML validity). Phase 7:
CB-1333..1337 (hook safety — single writer, atomic, deterministic, no injection,
p95 < 45ms). Phase 8: CB-1338..1343 (no ghosts, no placeholders, penetration
≥10%, spec from tooling, codegen compiles). Phase 4: CB-1350..1351
(differential obligations). Phase 5: CB-1352..1353 (A/G chains, cycle detection).
Phase 6: CB-1354 (contract query readiness).

---

## pmat Self-Enforcement (Eat Your Own Dogfood)

**Gap:** pmat enforces contracts on other repos but barely on itself — 0.4%
penetration (53 call sites / 15,073 functions). Target: ≥10%.

**Phase 1 (done):** Added `debug_assert!` to 7 critical scoring/query paths:
`handle_score` (composite range), `compute_composite` (sub-score ranges),
`handle_query` (limit/query preconditions), `handle_check` (path exists),
`handle_analyze_tdg` (threshold range), `score_contract` (5-dim range),
`lint_contract` (min_score range + passed/error consistency),
`handle_rust_project_score` (earned ≤ possible), `AgentContextIndex::save`
(non-empty index).

**Phase 2-4 (done):** Automated bulk enforcement across 700+ files. Path
existence preconditions, non-empty string checks, score range postconditions,
limit/count positivity checks. Covers handlers, services, models, scaffold,
MCP tools, quality gates, TDG, workflow, utils. **Counted: 14,841 = 98.5%. Falsified honest: 6,102 = 40.5%.**

| Mechanism | Sites | Verdict |
|-----------|-------|---------|
| `debug_assert!` with real condition | 6,102 | **MIXED** — !is_empty (3207), range (224), other (733). path.exists (1938) is **WRONG** for virtual paths — 2255 test failures |
| `#[contract]` proc_macro | 5,455 | Compile-time binding — 25 bindings, 5 equations. No runtime check |
| `debug_assert!(true, ...)` | 3,631 | **NO-OP** — never fails, zero enforcement value |

**Test validation (cargo test --lib): 2,255 failures** from `path.exists()`
assertions on virtual/in-memory paths (file classifiers, parsers, models).
These assertions are WRONG — paths used as logical identifiers don't need
to exist on disk. Honest real enforcement after removing wrong assertions:
~4,164 / 15,073 = **27.6%** (is_empty + range + other, minus bad path checks).

## Implementation Status

**Detection layer: complete.** 26 CB checks, 165+ tests, dogfooded on 4 repos.
**Infrastructure: 8/8 phases complete** (R-1..R-10 remediation closed, R-3
deferred). Phase 3 `asset_validator.rs` (R-10), Phase 6 `contract_index.rs`
(R-9). HookRegistry deferred — detection via CB-1333..1337 sufficient.

---

## References

Mugnier (OOPSLA 2025, proof brittleness), Chakarov (ICSE 2025, Cedar),
AWS (CACM 2024, correctness practices), Ma (ICSE 2025, SpecGen),
Incer (ACM TCPS 2025, Pacti A/G), Groce (ASE 2018, falsification-driven).
Tools: mdschema, hadolint, rumdl, standard-readme.

---

## Version History

| Version | Date | Changes |
|---------|------|---------|
| 3.16 | 2026-04-07 | **All pub fn covered**: 200→11 uncovered via 30+ sub-agents. 38.4% (5784). 0 failures. |
| 3.14 | 2026-04-06 | Tests green: removed wrong assertions. Honest baseline 36.9%. |
| 3.5-3.8 | 2026-04-06 | Falsified `contract_` pattern, per-crate CB-1340, self-enforcement 0.2% → 11%. |
| 1.0–3.4 | 2026-04-05 | Phases 1-8, remediation, apr-cli Level A. |
