Repository navigation
TR-11: new CRUX contracts (define) (TRACE-001) #4566
Description
Spec TRACE-001 v1.2 (docs/specifications/TRACE-001-tracing-consumers.md, operator 2026-09-27), row TR-11. Minted by the cop (aprender-77) under the single-minter rule. Epic #3598 (0.71.0; milestone rules in §4.1).
| EV | Row | Work | Contract | Done when (all must hold) | deps | K̂ |
|---|---|---|---|---|---|---|
| 4 | TR-11 new CRUX contracts (define) | Four contracts in the existing schema (syscall-trace, golden-trace, kernel-profile, op-attribution) with equations E-S1..E-S3, gap_effect: unmeasured, Kani obligations KANI-CRUX-D, KANI-CRUX-J, every competitor arm pinned (version + digest) or Refused{reason}, falsifiers planted |
four crux-F-NN-* |
pv validate counts the new obligations; 0 anonymous obligations; each planted falsifier RED |
05, 10 | 120 |
Hard rules §5 (R-1..R-7) and STOP conditions §7 (S-1..S-9) apply. A row that misses its cut moves on with slipped_from:; if it serves an exit criterion (V1/V2/V6/V7), the move needs an operator ruling.
Activity
fix(crux): F-23 INV-003 gets a falsifier, FALSIFY-003 gets an obligat…
noahgift commentedon Oct 14, 2026
merged into #5314 (master ticket for epic #4000; triage rule 7b, 2026-10-14). It is a checklist row there; reopen this issue when work on it starts or its PR opens.