carlos / platform Public

Reviewed 2af4eba4. No files modified; no tests run.

1. R4-1 — P1 — §7.2: G2 does not hold across DirStore handles sharing a directory.

The mutex belongs to each DirStore instance, despite the comment calling it process-wide (store.go:258). The comparison and filesystem replacement are separate operations (store.go:323, store.go:345).

A concrete interleaving with two handles on the same directory:

- Deploy reads pointer A, then reads no pipeline and passes authorization. - Its Put checks A’s ETag successfully, then pauses before writing the temporary file. - Through the second handle, an owner installs a pipeline and promotes B. Both operations finish. - Deploy resumes, writes its temporary file and renames it over B. It returns success.

G1 holds, but G2 fails: the pointer being replaced contains B, not the bytes deploy read. No restoration of A is needed. The same race permits a first promote to overwrite a newly created pointer and a rollback to overwrite an intervening promotion. A repeat promote writes nothing and is unaffected.

This is a supported configuration concern: both the console and direct CLI independently construct directory stores (console/main.go:482, cli.go:1948).

Correction: Qualify G2’s backend assumptions explicitly. For directory storage, either enforce that every writer shares one handle or provide coordination across handles/processes around the comparison and replacement. Include this interleaving in backend verification; a randomized test using one shared handle cannot expose it. This concerns single-object conditional writes, separately from Paul’s cross-object decision in §16.

1. R4-2 — P2 — §§7.2, 12: The randomized oracle rejects a write that satisfies G1 and G2.

§7.2 infers that a pipeline existing before the pointer read must be seen and cause refusal. §12 repeats that assertion while explicitly scheduling pipeline removal (spec:332, spec:528).

Consider an in-scope edge promotion:

- The handler and ladder read no pipeline. - An owner installs a pipeline naming edge. - Signer.Promote reads C’s pointer. - The pipeline is removed. - The authoritative hook reads no pipeline, authorizes, and the unchanged pointer permits the write.

GetPipeline returns nil for the removed object (pipeline.go:205). Both guarantees hold, yet §12 requires failure because the pipeline existed at the pointer read. Rollback has the same counterexample.

Correction: Base authorization assertions on the pipeline actually returned to the authoritative hook. Qualify the earlier-pipeline inference with continued presence through that read and the non-canary restriction. Record pointer-read, authorization-read and write events independently.

With that correction, moving the authoritative hook before the pointer read violates G1; an unconditional write violates G2 when another writer changes C between read and write. Require reproducible schedules demonstrating each mutant’s failure. As written, failures cannot establish mutation sensitivity because the correct mechanism also fails the oracle.

The three hook placements otherwise cover first, replacing and repeat promotes, rollback, and the handler’s proposal gate. I found no additional authorization-gap outcome outside the class already described; another ordering within that class is not a finding. S3’s conditional-write mechanism supports the stated comparison, unlike the multi-handle directory case. AWS conditional-write documentation

Verdict: request changes.