Task 13: Property test — convergence and no data loss #13

New issue

Closed

opened 2026-09-10 17:17:05 +00:00 by Cordy · 1 comment

Cordy commented

2026-09-10 17:17:05 +00:00

Owner

Depends on Task 12. This is the most valuable test in the repo. Expect it to find real bugs.

Goal

Generate random divergence on both sides and assert the two invariants that define a correct sync engine:

Convergence — after enough passes, both sides hold identical content at identical paths.
No data loss — every surviving file holds content that was actually written during the run. The engine never invents, truncates or corrupts data.

Files

Create: internal/sync/property_test.go

Shape of the test

func TestConvergence(t *testing.T) {
	for seed := int64(0); seed < 50; seed++ {
		seed := seed
		t.Run(fmt.Sprintf("seed-%d", seed), func(t *testing.T) {
			rng := rand.New(rand.NewSource(seed))
			// fresh MemFS + MemRemote + in-memory state store, Now pinned

			names := []string{"a.txt", "b.txt", "dir/c.txt"}
			written := map[string]bool{}

			for round := 0; round < 12; round++ {
				for i := 0; i < rng.Intn(3)+1; i++ {
					name := names[rng.Intn(len(names))]
					switch rng.Intn(4) {
					case 0: // local write
						body := fmt.Sprintf("local-%d-%d", seed, round)
						fs.Write(name, strings.NewReader(body), time.Now())
						written[body] = true
					case 1: // remote write
						body := fmt.Sprintf("remote-%d-%d", seed, round)
						rem.Put(name, strings.NewReader(body), time.Now())
						written[body] = true
					case 2:
						fs.Remove(name)
					case 3:
						rem.Delete(name)
					}
				}
				if _, err := e.SyncOnce(); err != nil {
					t.Fatalf("round %d: %v", round, err)
				}
			}

			// settle
			for i := 0; i < 5; i++ {
				if _, err := e.SyncOnce(); err != nil {
					t.Fatalf("settle: %v", err)
				}
			}

			// Invariant 1: same set of paths, same content on both sides.
			// Invariant 2: every surviving value is in `written`.
		})
	}
}

Collect non-directory entries from fs.Walk() and rem.List() into two maps, compare key sets and values, then assert every surviving value exists in written.

Steps

Write the test.
Run it: go test ./internal/sync/ -run TestConvergence -v
Fix whatever it finds — in the engine, never in the invariant. If a case is genuinely ambiguous, the correct resolution is a conflict copy, which preserves both versions and still satisfies invariant 2. Weakening the assertion is not an option; the assertion is the product requirement.
Commit: git commit -s -m "test(sync): property test for convergence and data preservation"
Raise the seed count to 500 and run once locally. Any new failure is a real bug — fix it, commit the fix separately, then set the count back to 50 so CI stays fast.

Acceptance criteria

50 seeds pass in CI.
500 seeds pass locally at least once.
No assertion has been weakened to make a seed pass.

Depends on Task 12. **This is the most valuable test in the repo.** Expect it to find real bugs. ## Goal Generate random divergence on both sides and assert the two invariants that define a correct sync engine: 1. **Convergence** — after enough passes, both sides hold identical content at identical paths. 2. **No data loss** — every surviving file holds content that was actually written during the run. The engine never invents, truncates or corrupts data. ## Files - Create: `internal/sync/property_test.go` ## Shape of the test ```go func TestConvergence(t *testing.T) { for seed := int64(0); seed < 50; seed++ { seed := seed t.Run(fmt.Sprintf("seed-%d", seed), func(t *testing.T) { rng := rand.New(rand.NewSource(seed)) // fresh MemFS + MemRemote + in-memory state store, Now pinned names := []string{"a.txt", "b.txt", "dir/c.txt"} written := map[string]bool{} for round := 0; round < 12; round++ { for i := 0; i < rng.Intn(3)+1; i++ { name := names[rng.Intn(len(names))] switch rng.Intn(4) { case 0: // local write body := fmt.Sprintf("local-%d-%d", seed, round) fs.Write(name, strings.NewReader(body), time.Now()) written[body] = true case 1: // remote write body := fmt.Sprintf("remote-%d-%d", seed, round) rem.Put(name, strings.NewReader(body), time.Now()) written[body] = true case 2: fs.Remove(name) case 3: rem.Delete(name) } } if _, err := e.SyncOnce(); err != nil { t.Fatalf("round %d: %v", round, err) } } // settle for i := 0; i < 5; i++ { if _, err := e.SyncOnce(); err != nil { t.Fatalf("settle: %v", err) } } // Invariant 1: same set of paths, same content on both sides. // Invariant 2: every surviving value is in `written`. }) } } ``` Collect non-directory entries from `fs.Walk()` and `rem.List()` into two maps, compare key sets and values, then assert every surviving value exists in `written`. ## Steps - [ ] **Write the test.** - [ ] **Run it:** `go test ./internal/sync/ -run TestConvergence -v` - [ ] **Fix whatever it finds — in the engine, never in the invariant.** If a case is genuinely ambiguous, the correct resolution is a conflict copy, which preserves both versions and still satisfies invariant 2. Weakening the assertion is not an option; the assertion *is* the product requirement. - [ ] **Commit:** `git commit -s -m "test(sync): property test for convergence and data preservation"` - [ ] **Raise the seed count to 500 and run once locally.** Any new failure is a real bug — fix it, commit the fix separately, then set the count back to 50 so CI stays fast. ## Acceptance criteria - 50 seeds pass in CI. - 500 seeds pass locally at least once. - No assertion has been weakened to make a seed pass.

Cordy added this to the phase-1-engine milestone

2026-09-10 17:17:05 +00:00

Cordy added the

data-integrity

engine

labels

2026-09-10 17:17:05 +00:00

Cordy referenced this issue

2026-09-10 20:37:25 +00:00

Task 4: Platform-illegal filename detection #4

Cordy referenced this issue

2026-09-10 23:47:01 +00:00

Task 12: The engine cycle #12

Cordy commented

2026-09-11 00:13:24 +00:00

Author

Owner

Done

a0015bd test(sync): property test for convergence and data preservation
d1278e7 test(sync): property test asserts no modified version is lost

What was built

New internal/sync/property_test.go with TestConvergence: random divergence over 50 seeds (500 locally), fresh MemFS + MemRemote + in-memory state store, Now pinned, per the issue's shape.
Operation mix widened (Task 12 CV5 ruling) to add local renames — into/out of dir/, onto an existing name, self-renames, rename-then-write — with a missing source ignored via ignoreMissing (only io/fs.ErrNotExist, per R2).
Invariant 1 (same paths/content both sides) and Invariant 2 (every surviving value was written), read back through real Open/Get, never through state.
Fix round 1 (F1): invariant 2 strengthened with a per-sync preservation check — any value that changed since the last sync must still exist on both sides afterward (a conflict copy or rename target counts), closing the "lost version" blind spot.
Fix round 1 (F3): write bodies now include the operation index, so two writes never collide on identical bytes.

Tests

TestConvergence: 50/50 seeds pass; 500/500 passed locally once, both before and after the F1/F3 fix.
Red step shown with uncommitted scratch-copy engine mutations: A (truncated upload), B (settleMove bypass), C (delete-remote row dropped) at a0015bd; D/E/F (the three "never lose bytes" truth-table rows) at d1278e7 — each caught by the invariant it targets.
Full suite green: go vet ./... and go test ./... across remote, state, sync, vfs.
CI run #13 on d1278e7 — green, linux/arm64, Go 1.25.5.

Acceptance criteria

"50 seeds pass in CI." — met: CI run 13 green on d1278e7, go test -run TestConvergence 50/50.
"500 seeds pass locally at least once." — met: 500/500, both at a0015bd and again after the F1/F3 fix at d1278e7 (bound bumped locally, never committed).
"No assertion has been weakened to make a seed pass." — met: both invariants only strengthened (F1 preservation check, F3 unique bodies); the operation mix was widened, never narrowed.

Rulings

R2: MemFS/MemRemote wrap io/fs.ErrNotExist for a missing path; the engine treats it as already-done on delete.
R3: one SHA-256 hex function hashes content on both sides; an ETag is never compared to a content hash.
R4: the engine never overwrites an existing path making a conflict copy; ConflictName disambiguates with " 2", " 3", ...
R12: commit subjects are the issue's exact text, git commit -s, with the Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> trailer.
Task 13 Ruling (F1): invariant 2 as worded can't detect a lost version (mutations D/E/F each passed 50/50 on the committed test) — add a per-sync preservation check via one closure at every SyncOnce; landed as d1278e7.
Task 13 Ruling (F3): write bodies weren't unique per operation, hiding a misplaced/lost value from value-based checks — add the op index to each body format, same commit as F1.

Deferred

F2 (minor): no fixpoint / state-store assertion — an engine that livelocks or lets state drift from bytes would still pass.
F4 (minor): the failure history can log a delete/rename that was actually a no-op (missing source).
The inner-loop op-count redraw and the unreachable end-of-test history dump on t.Fatalf predate this task and come from the issue's own sketch.

Implemented and reviewed by Claude (subagent-driven), landed on main after review and green CI.

**Done** - [a0015bd](http://192.168.10.245/Cordy/cairn-desktop/commit/a0015bd06b04e8290c4247864ae78377b2d8127d) test(sync): property test for convergence and data preservation - [d1278e7](http://192.168.10.245/Cordy/cairn-desktop/commit/d1278e7578d3e21a51c15e748929f52cc948b7bf) test(sync): property test asserts no modified version is lost **What was built** - New `internal/sync/property_test.go` with `TestConvergence`: random divergence over 50 seeds (500 locally), fresh MemFS + MemRemote + in-memory state store, Now pinned, per the issue's shape. - Operation mix widened (Task 12 CV5 ruling) to add local renames — into/out of `dir/`, onto an existing name, self-renames, rename-then-write — with a missing source ignored via `ignoreMissing` (only `io/fs.ErrNotExist`, per R2). - Invariant 1 (same paths/content both sides) and Invariant 2 (every surviving value was written), read back through real Open/Get, never through state. - Fix round 1 (F1): invariant 2 strengthened with a per-sync preservation check — any value that changed since the last sync must still exist on both sides afterward (a conflict copy or rename target counts), closing the "lost version" blind spot. - Fix round 1 (F3): write bodies now include the operation index, so two writes never collide on identical bytes. **Tests** - `TestConvergence`: 50/50 seeds pass; 500/500 passed locally once, both before and after the F1/F3 fix. - Red step shown with uncommitted scratch-copy engine mutations: A (truncated upload), B (settleMove bypass), C (delete-remote row dropped) at a0015bd; D/E/F (the three "never lose bytes" truth-table rows) at d1278e7 — each caught by the invariant it targets. - Full suite green: `go vet ./...` and `go test ./...` across remote, state, sync, vfs. - CI run [#13](http://192.168.10.245/Cordy/cairn-desktop/actions/runs/13) on d1278e7 — green, linux/arm64, Go 1.25.5. **Acceptance criteria** - "50 seeds pass in CI." — met: CI run 13 green on d1278e7, `go test -run TestConvergence` 50/50. - "500 seeds pass locally at least once." — met: 500/500, both at a0015bd and again after the F1/F3 fix at d1278e7 (bound bumped locally, never committed). - "No assertion has been weakened to make a seed pass." — met: both invariants only strengthened (F1 preservation check, F3 unique bodies); the operation mix was widened, never narrowed. **Rulings** - R2: MemFS/MemRemote wrap `io/fs.ErrNotExist` for a missing path; the engine treats it as already-done on delete. - R3: one SHA-256 hex function hashes content on both sides; an ETag is never compared to a content hash. - R4: the engine never overwrites an existing path making a conflict copy; ConflictName disambiguates with " 2", " 3", ... - R12: commit subjects are the issue's exact text, `git commit -s`, with the `Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>` trailer. - Task 13 Ruling (F1): invariant 2 as worded can't detect a lost version (mutations D/E/F each passed 50/50 on the committed test) — add a per-sync preservation check via one closure at every SyncOnce; landed as d1278e7. - Task 13 Ruling (F3): write bodies weren't unique per operation, hiding a misplaced/lost value from value-based checks — add the op index to each body format, same commit as F1. **Deferred** - F2 (minor): no fixpoint / state-store assertion — an engine that livelocks or lets state drift from bytes would still pass. - F4 (minor): the failure history can log a delete/rename that was actually a no-op (missing source). - The inner-loop op-count redraw and the unreachable end-of-test history dump on `t.Fatalf` predate this task and come from the issue's own sketch. _Implemented and reviewed by Claude (subagent-driven), landed on main after review and green CI._

Cordy closed this issue

2026-09-11 00:13:29 +00:00