amadan

carlos / platform Public

infra: box evidence prefixes are create-only and never deleted; spec: plan 1b's decisions

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude 02bacc5ee0075dd352bc0823eb6d9e7ef155eafc parent 5352ae6
3 files changed, +127 −11
  • docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md +45 −0
  • infra/modules/deployment-buckets/main.tf +20 −11
  • infra/modules/deployment-buckets/tests/evidence.tftest.hcl +62 −0
diff --git a/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md b/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
index a28effa0a..0dce3ecb4 100644
--- a/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
+++ b/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
@@ -1794,3 +1794,48 @@ or data-loss path that depends on disk evidence.
|---|---|
| B4-1 P2 volume recording is still a runtime admission prerequisite through §8's gate | accepted: under H19, volume recording never gates execution, admission, relocation or recovery. The gate no longer checks it; a box's start re-checks only capability, floor and roster; recorder failure alerts and keeps a dead box's chores open; tested through start, row minting and recovery (§8, §10, §19) |
| B4-2 P3 summaries still describe the disk-dependent fence | accepted: the source-loss table discharges chores only on qualifying records (§5.8); the tofu note says `delete_on_termination` affects only discharge (§6); the one-box row fences on the `terminated` read alone (§7) |
+
+## 24. Notes from plan 1b (2026-10-06)
+
+Plan `docs/superpowers/plans/2026-10-06-region-ha-1b-claim-readers.md`
+builds the parts of rev 5.4 that need none of L1 to L20: enrollment
+evidence, §19's corrections, the agent publishing its identity record,
+the fence bound to the roster's `cloud`, volume records and the discharge
+check, the edges file following `op.exec`, and root's half of §5.10. All
+of it is dormant behind `CARLOS_REGION_HA`. It keeps every property above
+and settles five details:
+
+1. **Enrollment refuses one instance under two references (§5.1).** The
+ record's `box` field is not covered by AWS's signature, so box A's
+ record copied to B's key with that field rewritten still verifies.
+ `boxid.Enroll` refuses an instance the roster holds under another
+ reference, as well as a reference the roster holds for another
+ instance, counting entries in every state.
+2. **A positive stamp is the relocatable mark (§18's open question).**
+ Only relocatable hosts with a claim carry a stamp, so the edge's report
+ of two boxes at one positive stamp already concerns them alone. No
+ separate marker.
+3. **The edges file's claim reads (§5.4).** A relocatable host with no
+ claim is published as before, unstamped: §8's gate admits a second box
+ only once every host has a claim. A read that fails keeps the last
+ decision. Each read stands 10 minutes (H9), at most 256 reads a pass.
+4. **"The first record taken at enrollment" (§5.9)** is the earliest
+ volume record for the enrollment, observed within one hour of the
+ roster's enrollment time. A later first record cannot speak for a
+ volume attached and removed before it, so the chores stay open. And
+ (controller ruling, 2026-10-06) the newest record must be no more
+ than two hours older than the termination observation; otherwise the
+ chores stay open for the operator path.
+5. **No volume record from a `terminated` read.** Its mappings are empty
+ (§8 step 5's dev test), and recording it would list every volume as
+ removed.
+
+It also removes plan 1a's `Bind`, `BindKey`, `Verifier.Verify` and
+`activator.WarmCopyTrusted`, and makes every box-evidence prefix
+create-only and never deleted in the deployment bucket's policy.
+
+Controller rulings of 2026-10-06, on Paul's behalf: the edges file
+withholds a relocatable host when `op.exec` names another box or none
+(§5.4 as written); root's §5.10 refusal stays behind `CARLOS_REGION_HA`
+until claim D6 lands, then becomes unconditional; the `*.bind.json`
+statement and `operator_role_arns` stay until no root sets the variable.
diff --git a/infra/modules/deployment-buckets/main.tf b/infra/modules/deployment-buckets/main.tf
index 1d9991173..95c8362dc 100644
--- a/infra/modules/deployment-buckets/main.tf
+++ b/infra/modules/deployment-buckets/main.tf
@@ -60,14 +60,23 @@ resource "aws_s3_bucket_server_side_encryption_configuration" "data" {
}
}
-# --- Box records (region HA spec 1 §5.1) -----------------------------------
-# control/boxes/<id>.json binds a box's name to one AWS instance, and
-# control/boxes/<id>.bind.json is an operator's word for a legacy label.
-# Both are written once and never changed. Storage enforces that, so no
-# bug or stolen box credential can rebind a name to another machine.
+# --- Box evidence (region HA spec 1 §5.1, §5.9, §6) ------------------------
+# control/boxes/<ref>.json is a box's AWS-signed identity, the evidence its
+# enrollment reads. control/box-volumes/, control/box-enrollment/ and
+# control/box-fences/ are the volume records, membership confirmations
+# and termination fence records regional workers write. Every one is
+# written once and never changed or deleted. Storage enforces that, so no
+# bug or stolen box credential can rewrite the evidence behind a decision.
+# (control/boxes/*.bind.json is no longer written: enrollment replaced the
+# operator bind. Its statement stays harmless until operator_role_arns is
+# retired with it.)
#
-# EVERY statement here names control/boxes/ and nothing wider. A broad Deny
-# on this bucket has broken lease releases before.
+# EVERY statement here names one of these prefixes and nothing wider. A
+# broad Deny on this bucket has broken lease releases before.
+
+locals {
+ box_evidence_prefixes = ["control/boxes", "control/box-volumes", "control/box-enrollment", "control/box-fences"]
+}
resource "aws_s3_bucket_policy" "deployment_box_records" {
bucket = aws_s3_bucket.deployment.id
@@ -76,13 +85,13 @@ resource "aws_s3_bucket_policy" "deployment_box_records" {
Version = "2012-10-17"
Statement = [
{
- # A record or bind may be created, never replaced. The qualifier
- # leaves multipart preparation alone and still covers its completion.
+ # Evidence may be created, never replaced. The qualifier leaves
+ # multipart preparation alone and still covers its completion.
Sid = "BoxRecordsAreCreateOnly"
Effect = "Deny"
Principal = "*"
Action = "s3:PutObject"
- Resource = "${aws_s3_bucket.deployment.arn}/control/boxes/*"
+ Resource = [for p in local.box_evidence_prefixes : "${aws_s3_bucket.deployment.arn}/${p}/*"]
Condition = {
Null = { "s3:if-none-match" = "true" }
Bool = { "s3:ObjectCreationOperation" = "true" }
@@ -93,7 +102,7 @@ resource "aws_s3_bucket_policy" "deployment_box_records" {
Effect = "Deny"
Principal = "*"
Action = ["s3:DeleteObject", "s3:DeleteObjectVersion"]
- Resource = "${aws_s3_bucket.deployment.arn}/control/boxes/*"
+ Resource = [for p in local.box_evidence_prefixes : "${aws_s3_bucket.deployment.arn}/${p}/*"]
},
{
# With no operators named, the list is one ARN nobody has, so the
diff --git a/infra/modules/deployment-buckets/tests/evidence.tftest.hcl b/infra/modules/deployment-buckets/tests/evidence.tftest.hcl
new file mode 100644
index 000000000..020667739
--- /dev/null
+++ b/infra/modules/deployment-buckets/tests/evidence.tftest.hcl
@@ -0,0 +1,62 @@
+# Region HA spec 1 §6: every box-evidence prefix is create-only and never
+# deleted, and the Denies name those prefixes and nothing wider (a broad
+# Deny on this bucket once broke every lease release). Each statement is
+# checked whole: effect, principal, actions, condition and resources, so
+# turning a Deny into an Allow, dropping an action or loosening the
+# conditional-write condition fails here.
+
+mock_provider "aws" {}
+
+override_resource {
+ target = aws_s3_bucket.deployment
+ values = { arn = "arn:aws:s3:::dep" }
+}
+
+variables {
+ deployment_bucket_name = "dep"
+ data_bucket_name = "data"
+}
+
+run "evidence_prefixes_are_create_only_and_never_deleted" {
+ command = plan
+
+ assert {
+ condition = jsonencode([
+ for s in jsondecode(aws_s3_bucket_policy.deployment_box_records.policy).Statement : s if s.Sid == "BoxRecordsAreCreateOnly"
+ ]) == jsonencode([{
+ Action = "s3:PutObject"
+ Condition = {
+ Bool = { "s3:ObjectCreationOperation" = "true" }
+ Null = { "s3:if-none-match" = "true" }
+ }
+ Effect = "Deny"
+ Principal = "*"
+ Resource = [
+ "arn:aws:s3:::dep/control/boxes/*",
+ "arn:aws:s3:::dep/control/box-volumes/*",
+ "arn:aws:s3:::dep/control/box-enrollment/*",
+ "arn:aws:s3:::dep/control/box-fences/*",
+ ]
+ Sid = "BoxRecordsAreCreateOnly"
+ }])
+ error_message = "BoxRecordsAreCreateOnly must Deny, to everyone, every PutObject without If-None-Match on exactly the four box-evidence prefixes"
+ }
+
+ assert {
+ condition = jsonencode([
+ for s in jsondecode(aws_s3_bucket_policy.deployment_box_records.policy).Statement : s if s.Sid == "BoxRecordsAreNeverDeleted"
+ ]) == jsonencode([{
+ Action = ["s3:DeleteObject", "s3:DeleteObjectVersion"]
+ Effect = "Deny"
+ Principal = "*"
+ Resource = [
+ "arn:aws:s3:::dep/control/boxes/*",
+ "arn:aws:s3:::dep/control/box-volumes/*",
+ "arn:aws:s3:::dep/control/box-enrollment/*",
+ "arn:aws:s3:::dep/control/box-fences/*",
+ ]
+ Sid = "BoxRecordsAreNeverDeleted"
+ }])
+ error_message = "BoxRecordsAreNeverDeleted must Deny, to everyone, both delete actions on exactly the four box-evidence prefixes"
+ }
+}