3.6 KiB
3.6 KiB
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:
- Every L1
memoryrecord has at least one L0 parent. A memory with no evidence came from somewhere the record does not explain. - Every
parentssha resolves to a node that exists. - Every
evidencesha appears as a parent of at least one memory. Evidence that nothing cites was written for no reason. evidencecount equalsgate.update == truecount (also M1.6 a2, re-checked here across the whole project rather than one run).- No edge is self-referential; no cycles.
- 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
mem verify --project P [--db] [--log], defaulting to both.- Check invariants 1–6, collecting all violations rather than failing on the first — one run should tell you everything wrong.
- Report per violation: invariant, level, sha, run id, and the log line number.
- Exit non-zero on any violation.
--format jsonfor 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:
a1_clean_passes— the good fixture, zero violations, exit 0.a2_orphan_memory— L1 with emptyparents; detected as invariant 1.a3_dangling_parent— parent sha not present; invariant 2.a4_uncited_evidence— evidence nothing references; invariant 3.a5_evidence_gate_mismatch— 3 update-gates but 2 evidence records; invariant 4.a6_cycle— A parents B, B parents A; invariant 5.a7_level_mismatch— L2 node parented directly to an L0 node; invariant 6.a8_reports_all— a fixture violating three invariants at once; assert all three appear in one run's output.a9_db_and_log_agree— introduce a violation in the database only; assert--dbcatches it and--logdoes 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 — tier model, Verification