91 lines
3.6 KiB
Markdown
91 lines
3.6 KiB
Markdown
|
# M2.7 — `mem verify` — edge closure
|
|||
|
|
|
|||
|
|
| Field | Value |
|
|||
|
|
|---|---|
|
|||
|
|
| Phase | M2 — Projections |
|
|||
|
|
| Size | S — under 1 day |
|
|||
|
|
| Status | ⬜ Not started |
|
|||
|
|
| Flags | — |
|
|||
|
|
| Spec | inlined below |
|
|||
|
|
| Blocks | M2.6 |
|
|||
|
|
|
|||
|
|
## Goal
|
|||
|
|
|
|||
|
|
Assert the provenance graph is well-formed, so a memory with no traceable
|
|||
|
|
evidence is caught rather than believed.
|
|||
|
|
|
|||
|
|
## Facts (inlined — no spec read needed)
|
|||
|
|
|
|||
|
|
Invariants, checked against the log and the database independently:
|
|||
|
|
|
|||
|
|
1. Every L1 `memory` record has at least one L0 parent. A memory with no evidence
|
|||
|
|
came from somewhere the record does not explain.
|
|||
|
|
2. Every `parents` sha resolves to a node that exists.
|
|||
|
|
3. Every `evidence` sha appears as a parent of at least one memory. Evidence that
|
|||
|
|
nothing cites was written for no reason.
|
|||
|
|
4. `evidence` count equals `gate.update == true` count (also M1.6 a2, re-checked
|
|||
|
|
here across the whole project rather than one run).
|
|||
|
|
5. No edge is self-referential; no cycles.
|
|||
|
|
6. Levels are consistent: an L1 node's parents are L0; an L2 node's are L1.
|
|||
|
|
|
|||
|
|
Invariant 6 is the one that catches a tier confusion, and it is the one most
|
|||
|
|
likely to break when M3.1 adds the L2 pass — an L2 node accidentally parented to
|
|||
|
|
L0 evidence would still look plausible in the vault.
|
|||
|
|
|
|||
|
|
`mem verify` is a read-only diagnostic. It never repairs; repair is `mem rebuild`.
|
|||
|
|
|
|||
|
|
## Steps
|
|||
|
|
|
|||
|
|
1. `mem verify --project P [--db] [--log]`, defaulting to both.
|
|||
|
|
2. Check invariants 1–6, collecting **all** violations rather than failing on the
|
|||
|
|
first — one run should tell you everything wrong.
|
|||
|
|
3. Report per violation: invariant, level, sha, run id, and the log line number.
|
|||
|
|
4. Exit non-zero on any violation.
|
|||
|
|
5. `--format json` for machine consumption.
|
|||
|
|
|
|||
|
|
## Acceptance
|
|||
|
|
|
|||
|
|
- A clean project reports zero violations, exit 0.
|
|||
|
|
- Each invariant has a fixture that violates it and is detected.
|
|||
|
|
- All violations are reported in one run, not just the first.
|
|||
|
|
|
|||
|
|
## Verify
|
|||
|
|
|
|||
|
|
**Harness:** hand-built log fixtures, one per invariant, plus a clean one.
|
|||
|
|
|
|||
|
|
**Integration test** — `tests/it_verify.rs`:
|
|||
|
|
1. `a1_clean_passes` — the good fixture, zero violations, exit 0.
|
|||
|
|
2. `a2_orphan_memory` — L1 with empty `parents`; detected as invariant 1.
|
|||
|
|
3. `a3_dangling_parent` — parent sha not present; invariant 2.
|
|||
|
|
4. `a4_uncited_evidence` — evidence nothing references; invariant 3.
|
|||
|
|
5. `a5_evidence_gate_mismatch` — 3 update-gates but 2 evidence records;
|
|||
|
|
invariant 4.
|
|||
|
|
6. `a6_cycle` — A parents B, B parents A; invariant 5.
|
|||
|
|
7. `a7_level_mismatch` — L2 node parented directly to an L0 node; invariant 6.
|
|||
|
|
8. `a8_reports_all` — a fixture violating three invariants at once; assert all
|
|||
|
|
three appear in one run's output.
|
|||
|
|
9. `a9_db_and_log_agree` — introduce a violation in the database only; assert
|
|||
|
|
`--db` catches it and `--log` does not, proving the two checks are independent.
|
|||
|
|
|
|||
|
|
**Command:** `cargo test -p mem-cli verify`
|
|||
|
|
|
|||
|
|
**False pass:**
|
|||
|
|
- Checking the database only. The log is authoritative; a log-level violation
|
|||
|
|
that rebuild happens to smooth over is still a bug in the writer, and
|
|||
|
|
assertion 9 is what keeps the two checks honest.
|
|||
|
|
- Failing fast on the first violation. It passes every single-violation fixture
|
|||
|
|
and makes assertion 8 impossible, which in practice means three rebuild cycles
|
|||
|
|
to find three problems.
|
|||
|
|
|
|||
|
|
## Traps
|
|||
|
|
|
|||
|
|
- Treating invariant 3 as fatal. Uncited evidence is a real smell, but a
|
|||
|
|
legitimate case exists: the final turn updates memory and the run is cut short
|
|||
|
|
before the memory record flushes. Report it, and let the gate decide severity.
|
|||
|
|
- Skipping invariant 6 because L2 does not exist yet. It is cheap now and it is
|
|||
|
|
precisely what M3.1 will break.
|
|||
|
|
|
|||
|
|
---
|
|||
|
|
|
|||
|
|
Background: [DESIGN.md](../DESIGN.md) — tier model, Verification
|