SCM MVP-N

[gunbai-bot]

Auto-opened by session-dashboard for session deep-carp-676.
Pushing to scm-algebra advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

• TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

[gunbai-bot]

Both blocking findings of review 61418 verified against the code and fixed at 2f32c9b45b2. Both correct, and they turned out to be one fix.

1. Raw lists bypass the uniqueness guarantee. Correct, and worse than the finding states. The module carried an annotation asserting that store_corpus_manifest refuses a duplicate path "so the first match is THE match" — an assertion about a guarantee the signature did not carry. That is validation-by-comment standing exactly where construction was available. Your [a→X, a→Y] specimen is the proof: it merged successfully by silently selecting the first, and reversing the list changed the answer. All three sides now take CorpusManifestRecord, so the specimen is not expressible at the boundary.

2. Θ(N²). Correct, and §6 makes it unconditional, so there was nothing to weigh. Replaced with a sorted grouping join — tag each entry with its side, sort the three streams together by path, fold once, close a group when the path changes. path_state_in and merged_path_union are deleted rather than made faster: the union, the three lookups and the decision are the same traversal now, so there is nothing left for them to answer.

The two fixes are one fix. Assigning a group member to its side is total only because no side can hold two entries for one path. A raw list can hold exactly that; a record cannot. Your first finding is what makes the second one's implementation legal.

Two mutations aimed at the code the rework introduced, since the old table said nothing about it:

mutation	presence	del/mod	mod/del	complete pop	union
bare-locator equality	RED	RED	RED	RED	RED
first-wins conflicts	pass	pass	pass	RED	pass
last group never closed	RED	RED	RED	pass	RED
target side dropped from join	RED	RED	pass	RED	RED
as built	pass	pass	pass	pass	pass

441/0 across all SCM witness files. That is 442 minus one claim I deleted while reworking: the S == T "either operand is unobservable" claim called the merge with identical arguments twice, and repairing the swap would not have saved it — the arm is reached only when path_state_eq holds, that compares locators, and AuthoredSourceTarget carries a locator and nothing else. Its RED was unauthorable, so it asserted nothing while looking like coverage. Deleted, with the structural argument recorded in its place and the condition that brings it back. It was cited as evidence in the PR body, which is corrected there.

I did not add a claim for the uniqueness fix, on the same test: it is structural now, so its RED is unauthorable too.

— sent from deep-carp-676

[gunbai-bot]

Side-chat review, reworked at 6a13f0f24c1. Both findings verified by execution before acting; both correct.

1. A real claim lives where the decoration was. Deleting the S == T "either operand" claim was right — its operands are indistinguishable, so no input could red it. But the statement worth making was never about that arm's operand. It is about the whole law: read the four lines with source and target exchanged and each maps onto another, so the merged result must not depend on which side was handed in as source. That red is authorable — the tempting wrong law resolves a conflict by preferring one side (-X ours), which is asymmetric by construction.

2. Every mutation I had tested that the law refuses enough. None tested that it does not refuse too much. A law that conflicted on every path whose three sides were not all equal would have passed the entire previous table and been useless. The three all-present resolvable cases are now controlled — only the target moved, only the source moved, both moved to the same place.

And a defect in my own new claim, caught by running the mutation rather than reading the code. The first outcomes_agree compared merged entries by path alone while its annotation claimed path and locator — weaker than its own description — so the asymmetric-conflict mutation walked straight through the symmetry claim. Both directions produce an entry at a; they disagree only about which side's content it holds, which is the entire defect the claim exists to catch. Same lesson as the decoration it replaces: a claim is worth what its red proves, not what its annotation asserts. The repair reuses object_store's manifest_comparands rather than coining a private tuple beside the authority that already answers that question.

mutation	presence	del/mod	mod/del	complete	union	symmetry	only-one-moved
bare-locator equality	RED	RED	RED	RED	RED	RED	RED
first-wins conflicts	pass	pass	pass	RED	pass	pass	pass
last group never closed	RED	RED	RED	pass	RED	RED	pass
target side dropped from join	RED	RED	pass	RED	RED	RED	pass
prefer source on conflict	RED	RED	RED	RED	pass	RED	pass
conflict unless all three equal	RED	pass	pass	RED	pass	RED	RED
as built	pass	pass	pass	pass	pass	pass	pass

The over-conservative mutation is the only one in the table that reds only-one-moved — nothing before it could tell a correct wall from one that refuses everything.

— sent from deep-carp-676