amadan
carlos / platform Public
| Earlier finding | Disposition | Evidence and remaining work | |---|---|---| | 1. Incarnation check | FIXED; DECLINED-AGREE on version pinning | §8.2:595 brackets each download and retry, withholding output until check B. This uses the identity validated by provision.go:2777 and claim.go:192. The stronger version-pinning mechanism remains unnecessary for the reported race. | | 2. Socket on stdin | FIXED | §8.3:638 specifies socket stdin/stdout and journal stderr, explicitly replacing claimunit_template.go:19. This matches systemd’s socket activation contract. https://www.freedesktop.org/software/systemd/man/257/systemd.socket.html | | 3. Progress versus completion ack | FIXED | §9.1:728 removes both acknowledgement routes. The ambiguity cannot occur. | | 4. Late writes after lost | FIXED for terminal arbitration | §5.8:416 makes lost logical closure: late chunks are ignored, and competing results use the same create-only key. store.go:794 supplies the required condition. The separate expiry-boundary problem remains under finding 13. | | 5. Cleanup reopens election | FIXED | §5.9:456 retains picked beyond the acceptance window. Later requests are rejected by age. Conditional creation is implemented at store.go:794. | | 6. “Showed none” after rejection | FIXED | §5.5:289 buffers and verifies before stdout, avoiding the irreversible writes in db.go:427. | | 7. Stored-ciphertext bound | PARTLY — P2 | §5.7:375 now accounts for retained output and noncurrent versions, but “gone two days after creation at most” is still false. The bucket is versioned at deployment-buckets/main.tf:23. S3 rounds eligibility to midnight UTC; noncurrent age starts when the successor is created; deletion can occur later. Fix: describe lifecycle eligibility and eventual reclamation, without a hard two-day deletion guarantee. A hard deadline requires a different reclamation mechanism. This is a failure of the revised mechanism, separate from the already-flagged provisional ruling. https://docs.aws.amazon.com/AmazonS3/latest/userguide/intro-lifecycle-rules.html, https://docs.aws.amazon.com/AmazonS3/latest/userguide/lifecycle-expire-general-considerations.html | | 8. Disk reservations | FIXED for the reported admission/restart defects | §5.7:385 removes the timeout escape and retains reservations until unit termination. §8.3:675 adds disconnect cancellation. The existing cancellable operations are db.go:418 and CheckDBContext, at check.go:44; the implementation must use that variant, not CheckDB, which supplies a background context. | | 9. Worker readiness | FIXED | §7.1:493 requires a real-unit probe, reserves its third connection, and skips probes during orphan blocking. This extends the armed-worker precedent at movesoffline.go:254. | | 10. Incomplete snapshot evidence | FIXED | §7.1:519 checks incomplete evidence first and requires both flags for either refusal. This matches snapshot.go:137, snapshot.go:182, and EvidenceComplete at snapshot.go:219. | | 11. Separate store endpoints | DECLINED-AGREE | §12:908 explicitly limits support to the existing endpoint model. Both clients use the process-wide endpoint: store.go:712, endpoint.go:146, s3compat.go:40. | | 12. Census classifications | FIXED | §13:937 uses supported classes, includes both runner callers, and requires removal rows and rulings. These match plan14rootreads_test.go:478, the existing J4 entry at plan14-root-reads.tsv:202, and the nonrecord precedent at movesofflinecensus_test.go:12. | | 13. Completion deletes terminal evidence | PARTLY — P2 | Completion no longer deletes anything, but §5.8:427 permits independent lifecycle deletion, while follow has no maximum age. If result.json disappears before the retained request and picked, a follow call can create lost for a completed read. The condition in store.go:794 permits creation over a current delete marker. Fix: establish a common logical follow/write cutoff before any lifecycle eligibility; after it, never synthesize another result. Test result-first expiry and concurrent housekeeping. https://docs.aws.amazon.com/AmazonS3/latest/userguide/conditional-writes.html | | 14. Cleanup removes follow identity | PARTLY — P2 | I6:173 promises equal lifetimes, but per-object lifecycle expiry cannot provide them. A request created before midnight and output created after midnight can have expiry dates a day apart. Once the request disappears, §9.1:740 returns 404 for retained output. Fix: guarantee identity through an explicit retrieval interval shorter than lifecycle eligibility, and stop promising availability for every retained object. For fallback housekeeping, specify request-last, retryable deletion—the existing implementation does so at runs/store.go:128. | | 15. Full db gate hides record-changed | FIXED | §9.1:732 separates admission from follow/cancel authorization. It avoids the current-record refusals at apidb.go:132, following the retained-request precedent at apirunsfollow.go:126. |
For the seven invariants in §5.2:166:
| Invariant | Disposition | Check | |---|---|---| | I1 Immutable | PARTLY | All listed protocol PUTs are conditional creates, and acknowledgements are gone. However, §5.8’s housekeeping deletes lack an enforced boundary separating them from still-permitted follow/cancel calls. Calling the pass “housekeeping” does not establish that boundary. Findings 13–14 remain relevant. | | I2 Expiry is the store’s | NOT FIXED | The stated timing is inaccurate; the fallback explicitly deletes objects itself; and a lazily ended read need not have a terminal result after 22 minutes. No route cutoff establishes the claim that cleanup touches objects “which nothing reads.” | | I3 One owner | FIXED for cooperating participants | Conditional creation of picked elects one owner, including a console expiry claim. A lost response does not elect two owners, but recovery from it is incomplete: new finding 16. This is protocol ownership, not authenticated writer identity. | | I4 One end | PARTLY | Competing result creates correctly arbitrate owner versus lost while the key remains present. Finding 13 shows how lifecycle expiry can reopen that decision. | | I5 Acceptance | PARTLY | Buffering, authenticated decryption, sequence checks and the sealed hash protect against incomplete or inconsistent output. They do not prove that the named owner wrote it: new finding 18. | | I6 Identity | PARTLY | The signed-request follow gate fixes current-record dependence. Equal physical lifetimes are not established: finding 14. | | I7 Time is decided lazily | PARTLY | lost can be retried through conditional creation. The two-write expired transition lacks recovery, and abandoned reads have no specified admission-counter expiry: new findings 16–17. |
The “closed by” table therefore holds for 3, 4, 5 and 15, subject to the retained-key boundary above. It does not fully close 7, 13 or 14.
The chunk read-back rule at §5.3:217 correctly preserves sealed bytes across ambiguous retries. Conditional-create support itself is available on S3 and MinIO; the missing recovery concerns picked, not that primitive. https://docs.aws.amazon.com/AmazonS3/latest/userguide/conditional-writes.html, https://github.com/minio/minio/blob/master/cmd/erasure-object-conditional_test.go
For the queue, current-plus-previous-hour listing covers requests behind the box’s clock across an hour boundary. A request in the next hour, within the permitted future skew, becomes discoverable when the box crosses that boundary; the 30-second poll still leaves it within the box’s acceptance window. I found no additional permanent omission caused solely by hour partitioning under the stated skew bound.
- P2 — Lazy expiry can strand a read between its two writes.
The console creates picked=expired, then crashes or fails to create result.json. Subsequent follow calls find picked, so the “no picked” expiry branch no longer applies. There is no owning box whose deadline supplies the normal lost transition. A lost successful PUT response causes the same problem: “create failed” does not establish that a box owns the read.
Existing code explicitly handles uncertain write outcomes: apirunsfollow.go:94 documents them, and host/runs.go:270 reads ownership back after an unsuccessful pickup response. The new design specifies equivalent recovery only for chunks.
Fix: make every follow call reconcile an existing console-expiry marker with a missing result. After ambiguous or conflicting picked writes, read the marker and distinguish console expiry, this exact box attempt, and another owner. Test a crash between the writes and a committed picked whose response is lost.
- P2 — Abandoned reads have no specified way to release console admission slots.
Admit reads while boxes are busy, then let their CLIs disappear before pickup. No follow calls remain to create expired; no box owns them; lifecycle deletion cannot update the console’s in-memory counters. The design gives no counter-release rule. Two abandoned reads can exhaust a person’s allowance; sixteen can exhaust the console’s until restart.
The existing token budget is not a sufficient precedent: it explicitly expires entries while admitting subsequent requests at authcli.go:229. Existing runs also have independent expiry processing at runsweep.go:98.
Fix: give admission reservations a bounded lifetime independent of CLI polling. Reconcile or expire them during subsequent admissions or a local timer, using pickup and owner deadlines. This need not introduce protocol deletes. Test abandoned queued reads, abandoned picked reads, and recovery without restarting the console.
- P2 — The new non-owner forgery claim contradicts the sealing mechanism.
Spec: §5.9:457, I5:172, versus §5.6:322.
A non-owner can read the public reply key, create forged chunks, then win the result.json create with a matching sealed hash and the legitimate owner’s box name. The owner’s later failed result loses. The CLI’s specified checks accept the forged, internally consistent answer.
Every box has deployment-bucket write authority at region-host/main.tf:166. Sealing at crypto.go:206 uses the recipient’s public key and a freshly generated sender key; it supplies no owner credential. A key path and a box string cannot establish authorship.
Fix: align I3/I5, §5.9 and T4 with §5.6’s explicitly accepted trust boundary: consistency is checked, but a compromised deployment writer can forge an answer. If non-owner forgery resistance is required instead, add authenticated owner publication. Test forged chunks together with a forged matching result, rather than chunk substitution alone.
Reviewed at 20524df4c65542a2f5c196903981e0fc62d22ee4. Static review; no runtime acceptance tests or file changes. Platform module code at both cited release tags was inspected. Current flagship refs and deployment-state assertions remain unverified: GitHub retrieval failed, and the available infrastructure checkout is dated October 6.
REVISE