test(property): exercise resource rename via OpApply

Makefile

@@ -298,7 +298,7 @@ stage-oidc-fixtures:
 
 ## test-property: Run property tests (FullChaos 100 iterations, others 50)
 test-property:
-	go test -C tests/blackbox -tags=property -run 'TestProperty_Sequential|TestProperty_Concurrent' -v -count=1 -rapid.checks=50 -timeout=60m
+	go test -C tests/blackbox -tags=property -run 'TestProperty_Sequential|TestProperty_Concurrent|TestProperty_RenameViaApply|TestRenameViaApply_Deterministic' -v -count=1 -rapid.checks=50 -timeout=60m
 	go test -C tests/blackbox -tags=property -run TestProperty_FullChaos -v -count=1 -rapid.checks=100 -timeout=60m
 
 ## mutation-test: Run mutation testing across all unit-tested packages and generate report

tests/blackbox/generators.go

@@ -40,7 +40,7 @@ func OperationSequenceGen(config PropertyTestConfig) *rapid.Generator[[]Operatio
 		count := rapid.IntRange(config.OperationCount.Min, config.OperationCount.Max).Draw(t, "count")
 		ops := make([]Operation, count)
 		for i := range ops {
-			ops[i] = SingleOperationGen(config).Draw(t, fmt.Sprintf("op-%d", i))
+			ops[i] = SingleOperationGen(config, i).Draw(t, fmt.Sprintf("op-%d", i))
 		}
 
 		// Enforce OpCrashAgent constraints: at most once, not first or last.
@@ -60,15 +60,17 @@ func OperationSequenceGen(config PropertyTestConfig) *rapid.Generator[[]Operatio
 }
 
 // SingleOperationGen returns a rapid generator that produces a single operation
-// whose kind and parameters respect the given config.
-func SingleOperationGen(config PropertyTestConfig) *rapid.Generator[Operation] {
+// whose kind and parameters respect the given config. seq is the operation's
+// position in the sequence; it parameterizes draws that must be unique per
+// operation (rename labels).
+func SingleOperationGen(config PropertyTestConfig, seq int) *rapid.Generator[Operation] {
 	return rapid.Custom(func(t *rapid.T) Operation {
 		kinds := allowedKinds(config)
 		kindIdx := rapid.IntRange(0, len(kinds)-1).Draw(t, "kind")
 		kind := kinds[kindIdx]
 
 		op := Operation{Kind: kind}
-		fillOperationFields(t, &op, config)
+		fillOperationFields(t, &op, config, seq)
 		return op
 	})
 }
@@ -163,7 +165,7 @@ func drawnOutcomeGen(t *rapid.T, label string) DrawnOutcome {
 }
 
 // fillOperationFields populates the kind-specific fields on the operation.
-func fillOperationFields(t *rapid.T, op *Operation, config PropertyTestConfig) {
+func fillOperationFields(t *rapid.T, op *Operation, config PropertyTestConfig, seq int) {
 	pool := resourcePoolForConfig(config)
 	slotCount := slotCountForConfig(config, pool)
 
@@ -188,6 +190,23 @@ func fillOperationFields(t *rapid.T, op *Operation, config PropertyTestConfig) {
 			op.ResourceIDs = resourceIDsGen(t, config.ResourceCount, 1)
 		}
 		op.Properties = resourcePropsGen(t)
+		// RFC-0041: with rename enabled, OpApply optionally carries a rename
+		// overlay for one slot from ResourceIDs. The executor only honours
+		// the overlay if that slot is StateExists at execution time
+		// (otherwise rename is a no-op). Combined with the property template
+		// above this lets a single apply model an update as label-only,
+		// property-only, or both. The label embeds the operation's sequence
+		// position, so no two renames in a sequence can produce the same
+		// label — label reuse would make slot resolution ambiguous.
+		op.RenameSlotIndex = -1
+		if config.EnableRename && len(op.ResourceIDs) > 0 {
+			if rapid.IntRange(0, 2).Draw(t, "applyRenameRoll") == 0 {
+				op.RenameSlotIndex = renameSlotIndexFromIDs(t, op.ResourceIDs)
+				if op.RenameSlotIndex >= 0 {
+					op.RenameNewLabel = fmt.Sprintf("renamed-%d", seq)
+				}
+			}
+		}
 		if config.EnableFailures {
 			op.DrawnOutcomes = make(map[string]DrawnOutcome)
 			for i := 0; i < slotCount; i++ {
@@ -523,3 +542,15 @@ func subsequenceGen(t *rapid.T, values []string, label string) []string {
 	}
 	return result
 }
+
+// renameSlotIndexFromIDs picks one slot from `ids` to rename as part of an
+// OpApply. Any slot is eligible: the forma builders thread label overrides
+// through parent references, so renaming a slot that others reference keeps
+// their `$res` blocks pointing at the current label. Returns -1 when `ids`
+// is empty — the caller treats that as "no rename on this apply".
+func renameSlotIndexFromIDs(t *rapid.T, ids []int) int {
+	if len(ids) == 0 {
+		return -1
+	}
+	return rapid.SampledFrom(ids).Draw(t, "applyRenameSlot")
+}

tests/blackbox/generators_test.go

@@ -326,7 +326,7 @@ func TestResponseSequenceGen(t *testing.T) {
 				StackCount:     2,
 			}
 			op := Operation{Kind: OpApply}
-			fillOperationFields(rt, &op, config)
+			fillOperationFields(rt, &op, config, 0)
 
 			require.NotNil(t, op.DrawnOutcomes, "DrawnOutcomes should be non-nil when EnableFailures=true")
 			// Should have entries for all resource slots in the target stack.
@@ -347,7 +347,7 @@ func TestResponseSequenceGen(t *testing.T) {
 				StackCount:     2,
 			}
 			op := Operation{Kind: OpApply}
-			fillOperationFields(rt, &op, config)
+			fillOperationFields(rt, &op, config, 0)
 
 			assert.Nil(t, op.DrawnOutcomes, "DrawnOutcomes should be nil when EnableFailures=false")
 		})
@@ -368,7 +368,7 @@ func TestResponseSequenceGen(t *testing.T) {
 
 			// We need a pool for onDependents to be set.
 			op := Operation{Kind: OpDestroy}
-			fillOperationFields(rt, &op, config)
+			fillOperationFields(rt, &op, config, 0)
 
 			require.NotNil(t, op.DrawnOutcomes, "DrawnOutcomes should be non-nil for OpDestroy with EnableFailures")
 

tests/blackbox/harness.go

@@ -54,6 +54,12 @@ type TestHarness struct {
 	cancel     context.CancelFunc
 	pluginsDir string
 
+	// RenamesAccepted counts renames the agent accepted across all rapid
+	// iterations. Tests that enable rename assert it is non-zero after
+	// rapid.Check so a broken rename path cannot pass vacuously (a rejected
+	// or no-op rename executes no rename at all).
+	RenamesAccepted int
+
 	// Agent subprocess
 	agentCmd     *exec.Cmd
 	agentLogFile *os.File

tests/blackbox/invariants.go

@@ -18,13 +18,17 @@ import (
 type ViolationKind int
 
 const (
-	ViolationPhantomResource        ViolationKind = iota // in inventory but not in cloud
-	ViolationOrphanedResource                            // in cloud but not in inventory
-	ViolationPropertyMismatch                            // inventory and cloud properties differ
-	ViolationCommandNotTerminal                          // command not in terminal state
-	ViolationResolvableNotResolved                       // resolvable $ref not properly resolved
-	ViolationModelInventoryMismatch                      // model expected state doesn't match inventory
-	ViolationDuplicateNativeID                           // two or more inventory rows share a NativeID (RFC-0041)
+	ViolationPhantomResource              ViolationKind = iota // in inventory but not in cloud
+	ViolationOrphanedResource                                  // in cloud but not in inventory
+	ViolationPropertyMismatch                                  // inventory and cloud properties differ
+	ViolationCommandNotTerminal                                // command not in terminal state
+	ViolationResolvableNotResolved                             // resolvable $ref not properly resolved
+	ViolationModelInventoryMismatch                            // model expected state doesn't match inventory
+	ViolationDuplicateNativeID                                 // two or more inventory rows share a NativeID (RFC-0041)
+	ViolationRenameOldLabelStillPresent                        // after rename, inventory still has a row at the old label (RFC-0041)
+	ViolationRenameLabelDriftFromNativeID                      // inventory row's label diverges from the slot's CurrentLabel for the same NativeID (RFC-0041)
+	ViolationRenameIdentityChanged                             // a successful update RU changed the resource's NativeID or KSUID (RFC-0041)
+	ViolationRenameRecreatedResource                           // a renamed slot was fulfilled by a create — rename must be an in-place update (RFC-0041)
 )
 
 // Violation describes a single invariant violation.
@@ -726,3 +730,111 @@ func CheckOperationLogInvariants(opLog []testcontrol.OperationLogEntry) []Violat
 
 	return violations
 }
+
+// CheckRenameInvariants verifies RFC-0041 invariants after one or more
+// renames. For every slot whose PreviousLabel is non-empty (a rename
+// landed on it), the inventory must NOT carry a row at the old
+// (Stack, Type, PreviousLabel) tuple with that slot's identity — that
+// would mean the rename left the old row behind instead of renaming the
+// existing one. The identity guard (NativeID/KSUID match) keeps a
+// different slot legitimately renamed onto the freed label from being
+// flagged.
+//
+// Also: for every managed inventory row whose NativeID the model tracks
+// (via SetNativeID), the row's Label must equal the slot's current label,
+// and its KSUID must match the tracked KSUID. This is the positive
+// identity-preservation check: rename keeps the (NativeID, KSUID) pair
+// stable, and the slot's CurrentLabel overlay must match what's in cloud.
+func CheckRenameInvariants(model *StateModel, inventory []pkgmodel.Resource) []Violation {
+	var violations []Violation
+	if model == nil {
+		return violations
+	}
+
+	// Index inventory rows by (stack, type, label) for O(1) lookup.
+	type key struct{ stack, typ, label string }
+	rows := make(map[key]pkgmodel.Resource, len(inventory))
+	for _, r := range inventory {
+		rows[key{stack: r.Stack, typ: r.Type, label: r.Label}] = r
+	}
+
+	for _, stack := range model.Stacks {
+		for slotIdx, res := range stack.Resources {
+			if res == nil || res.PreviousLabel == "" {
+				continue
+			}
+			// Determine the resource type by consulting the pool when one is
+			// present; otherwise default to Test::Generic::Resource.
+			resType := "Test::Generic::Resource"
+			if model.Pool != nil && slotIdx < len(model.Pool.Slots) {
+				resType = model.Pool.Slots[slotIdx].Type
+			}
+			oldKey := key{stack: stack.Label, typ: resType, label: res.PreviousLabel}
+			hit, present := rows[oldKey]
+			if !present || !hit.Managed {
+				continue
+			}
+			// Identity guard: only flag the row if it belongs to this slot's
+			// lineage. A different slot renamed onto the freed label is legal.
+			stackIdx := model.StackIndexByLabel(stack.Label)
+			trackedNativeID := model.GetNativeID(stackIdx, slotIdx)
+			trackedKsuid := model.GetKsuid(stackIdx, slotIdx)
+			sameLineage := (trackedNativeID != "" && hit.NativeID == trackedNativeID) ||
+				(trackedKsuid != "" && hit.Ksuid == trackedKsuid)
+			if !sameLineage {
+				continue
+			}
+			violations = append(violations, Violation{
+				Kind: ViolationRenameOldLabelStillPresent,
+				Message: fmt.Sprintf(
+					"slot %d (stack %s, type %s) was renamed away from %q but a managed inventory row still carries that label (ksuid=%s, nativeID=%s)",
+					slotIdx, stack.Label, resType, res.PreviousLabel, hit.Ksuid, hit.NativeID,
+				),
+			})
+		}
+	}
+
+	// Identity-preservation check via NativeID. For each inventory row whose
+	// NativeID the model has tracked, compare its label to the slot's
+	// CurrentLabel-aware label. Mismatch means a rename either didn't reach
+	// inventory or got reverted without the model's overlay rolling back.
+	nativeIDToSlot := make(map[string][2]int, len(model.NativeIDs))
+	for k, nid := range model.NativeIDs {
+		var stackIdx, slotIdx int
+		fmt.Sscanf(k, "%d:%d", &stackIdx, &slotIdx)
+		nativeIDToSlot[nid] = [2]int{stackIdx, slotIdx}
+	}
+	for _, r := range inventory {
+		if !r.Managed || r.NativeID == "" {
+			continue
+		}
+		slot, tracked := nativeIDToSlot[r.NativeID]
+		if !tracked {
+			continue
+		}
+		expectedLabel := model.LabelForResource(slot[0], slot[1])
+		if r.Label != expectedLabel {
+			violations = append(violations, Violation{
+				Kind: ViolationRenameLabelDriftFromNativeID,
+				Message: fmt.Sprintf(
+					"inventory row NativeID=%s carries label=%q but the model expects label=%q for slot (stack %d, slot %d)",
+					r.NativeID, r.Label, expectedLabel, slot[0], slot[1],
+				),
+			})
+		}
+		// KSUID stability: the row for a tracked NativeID must carry the
+		// KSUID the model recorded for that slot. A fresh KSUID under the
+		// same NativeID means a rename minted a new resource identity.
+		if trackedKsuid := model.GetKsuid(slot[0], slot[1]); trackedKsuid != "" && r.Ksuid != "" && r.Ksuid != trackedKsuid {
+			violations = append(violations, Violation{
+				Kind: ViolationRenameIdentityChanged,
+				Message: fmt.Sprintf(
+					"inventory row NativeID=%s label=%q carries ksuid=%s but the model tracked ksuid=%s for slot (stack %d, slot %d)",
+					r.NativeID, r.Label, r.Ksuid, trackedKsuid, slot[0], slot[1],
+				),
+			})
+		}
+	}
+
+	return violations
+}

tests/blackbox/invariants_rename_test.go

@@ -9,6 +9,8 @@ package blackbox
 import (
 	"testing"
 
+	"github.com/stretchr/testify/require"
+
 	pkgmodel "github.com/platform-engineering-labs/formae/pkg/model"
 	"github.com/platform-engineering-labs/formae/tests/testcontrol"
 )
@@ -61,3 +63,58 @@ func TestCheckInvariants_SingleRowPerNativeID_OK(t *testing.T) {
 		}
 	}
 }
+
+// After a rename, a managed inventory row at the slot's previous label is a
+// violation only when it belongs to that slot's lineage (same NativeID or
+// KSUID). A different slot legitimately renamed onto the freed label must
+// not be flagged.
+func TestCheckRenameInvariants_OldLabelIdentityGuard(t *testing.T) {
+	model := NewStateModel(1, 3)
+	model.ApplyCreated(0, []int{1}, "")
+	model.SetNativeID(0, 1, "test-42")
+	model.SetKsuid(0, 1, "K_B")
+	model.RecordRename(0, 1, "renamed-0")
+	model.RecordRename(0, 1, "renamed-1") // PreviousLabel is now "renamed-0"
+
+	// Another lineage's row occupies the freed label: legal, not flagged.
+	reused := []pkgmodel.Resource{
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-0", NativeID: "test-77", Ksuid: "K_OTHER", Managed: true},
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-1", NativeID: "test-42", Ksuid: "K_B", Managed: true},
+	}
+	require.Empty(t, CheckRenameInvariants(model, reused),
+		"a different lineage on the freed label must not be flagged")
+
+	// The slot's own lineage still on the old label: the rename leaked it.
+	// Fires the old-label check and, because the tracked NativeID carries
+	// the wrong label, the positive label-drift check as well.
+	leaked := []pkgmodel.Resource{
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-0", NativeID: "test-42", Ksuid: "K_B", Managed: true},
+	}
+	violations := CheckRenameInvariants(model, leaked)
+	kinds := make(map[ViolationKind]bool, len(violations))
+	for _, v := range violations {
+		kinds[v.Kind] = true
+	}
+	require.True(t, kinds[ViolationRenameOldLabelStillPresent], "leaked old-label row must be flagged: %v", violations)
+}
+
+// For a tracked NativeID the inventory row must carry both the current
+// label and the tracked KSUID — a fresh KSUID under the same NativeID means
+// the rename minted a new resource identity.
+func TestCheckRenameInvariants_KsuidStability(t *testing.T) {
+	model := NewStateModel(1, 3)
+	model.ApplyCreated(0, []int{1}, "")
+	model.SetNativeID(0, 1, "test-42")
+	model.SetKsuid(0, 1, "K_B")
+	model.RecordRename(0, 1, "renamed-0")
+
+	inventory := []pkgmodel.Resource{
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-0", NativeID: "test-42", Ksuid: "K_FRESH", Managed: true},
+	}
+	violations := CheckRenameInvariants(model, inventory)
+	require.Len(t, violations, 1)
+	require.Equal(t, ViolationRenameIdentityChanged, violations[0].Kind)
+
+	inventory[0].Ksuid = "K_B"
+	require.Empty(t, CheckRenameInvariants(model, inventory))
+}

tests/blackbox/operations.go

@@ -95,6 +95,19 @@ type Operation struct {
 	// nil map means no failure injection (all succeed).
 	DrawnOutcomes map[string]DrawnOutcome
 
+	// For OpApply: optional rename overlay. When RenameSlotIndex >= 0 and
+	// the slot is currently StateExists, the apply additionally renames the
+	// slot — the constructed forma carries Label=RenameNewLabel and
+	// Alias=<slot's current label> for that one resource. Combined with the
+	// usual property-template path this lets a single apply model:
+	//   - property change only (RenameSlotIndex = -1)
+	//   - label change only (RenameSlotIndex set, Properties left at the
+	//     same template that produced the current state)
+	//   - both (RenameSlotIndex set, Properties template changed)
+	// (RFC-0041.)
+	RenameSlotIndex int
+	RenameNewLabel  string
+
 	// Set during execution to track ordering.
 	SequenceNum int
 }
@@ -133,6 +146,23 @@ type ResourceSnapshot struct {
 	SlotIndex  int
 	State      ResourceState
 	Properties string
+	// CurrentLabel/PreviousLabel capture the rename overlay at snapshot time
+	// so a failed/canceled OpRename can be unwound. Without these a rename
+	// that was accepted then rejected during execution would leave the
+	// model's CurrentLabel pointing at a label the engine never persisted.
+	CurrentLabel  string
+	PreviousLabel string
+}
+
+// PendingRename records that a command carried a rename overlay: the forma
+// declared the slot under NewLabel with Alias set to OldLabel. On a
+// successful command the engine must have performed it as an in-place update
+// (an update RU carrying OldLabel); the drain asserts that.
+type PendingRename struct {
+	StackIndex int
+	SlotIndex  int
+	OldLabel   string
+	NewLabel   string
 }
 
 // AcceptedCommand tracks a command that was accepted by the agent during the chaos phase.
@@ -141,7 +171,8 @@ type AcceptedCommand struct {
 	Snapshots      []ResourceSnapshot // pre-command state for revert on cancel
 	OpLogSize      int                // operation log length immediately after acceptance
 	RequestedSlots []ResourceSlotRef
-	IsReconcile    bool // true if the command was reconcile mode (properties = full desired state)
+	IsReconcile    bool           // true if the command was reconcile mode (properties = full desired state)
+	Rename         *PendingRename // set when the command carried a rename overlay
 	// Resolved is true when the cancel handler has already processed this
 	// command. The command remains in AcceptedCommands so that
 	// DrainPendingCommands can include its outcome when resolving conflicts
@@ -194,6 +225,10 @@ type PropertyTestConfig struct {
 	// EnableCrashInjection allows OpCrashAgent operations (kill -9 + restart).
 	EnableCrashInjection bool
 
+	// EnableRename allows OpRename operations (RFC-0041). When set the
+	// generator may draw a rename for any slot currently in StateExists.
+	EnableRename bool
+
 	// StackCount is the number of independent stacks (1 for sequential tests, 2-3 for concurrent).
 	StackCount int
 }