New invariant without test = lie. Add failing test first.
Name test so it cites the invariant:
TestV7_RefundIdempotent
.
5. VERIFY
Fix code. Run test. Must pass. Run full suite. Must not regress.
6. LOG
Commit spec edit + test + code fix together.
Commit msg:
backprop §B. + §V.:
.
WHAT MAKES A GOOD INVARIANT
Testable in code (grep-able or assert-able).
Scoped to a behavior, not a file.
Stated positively when possible (
! hold
over
⊥ forbid
).
References §I surface where it applies.
Bad
V8: code should be correct.
Good
V8: ∀ pg_query ! params interpolated via driver, ⊥ string concat.
WHEN NOT TO ADD §V
Bug was purely mechanical typo with no class (
i++
vs
i--
in throwaway).
Fix is a one-time migration.
Root cause is external dep (upgrade deps instead, note in §C).
Still append §B entry — record that this failure mode was considered. Future bug with same smell → §B search shows precedent.
OUTPUT SHAPE
Every backprop run produces:
§B entry (always).
§V entry (usually).
Test file (when §V added).
Code fix.
One commit.
No dashboards. No log files. SPEC.md + git is the full history.