Skip to content

test(property): exercise resource rename via OpApply - #668

Merged
JeroenSoeters merged 2 commits into
mainfrom
test/rename-via-apply-rebased
Aug 22, 2026
Merged

test(property): exercise resource rename via OpApply#668
JeroenSoeters merged 2 commits into
mainfrom
test/rename-via-apply-rebased

Conversation

@JeroenSoeters

Copy link
Copy Markdown
Collaborator

Summary

Supersedes #505: naxty's rename-via-OpApply property coverage, semantically rebased onto the rewritten deterministic harness (#656/#657) with the changes-requested review and the adversarial-review addendum on that PR addressed. The base commit keeps naxty's authorship; the second commit is the review-driven rework.

What carries over from #505: rename folded into OpApply (an optional per-apply rename overlay), the CurrentLabel/PreviousLabel slot overlay, overlay-aware slot resolution, snapshot-based label revert, and the rename invariants (ViolationRenameOldLabelStillPresent, ViolationRenameLabelDriftFromNativeID).

What changed against the review:

  • No IdentityOnlyInvariants. FullChaos runs rename with the full invariant suite; the drift-code edits the original branch made are gone with the machinery test(blackbox): compute drift end states deterministically instead of tolerating a sync window #656 deleted.
  • Identity is verified from the engine's own reporting, not the model's optimistic bookkeeping. The model tracks KSUIDs alongside NativeIDs (both come back on every resource update); an update RU that changes either identity is flagged before the model adopts the new value; and a successful command that carried a rename must contain a success update RU at the renamed label — a destroy+recreate produces a create RU there instead. These surface as violations at AssertAllInvariants.
  • Labels are overlay-aware end to end. The rename folds into the label overrides before the forma is built, so child $res references to a renamed slot carry the new label — which also lifts the parents-only rename restriction (any slot can be renamed now, including referenced parents and cross-stack providers). Failure-injection programming addresses slots by index instead of round-tripping through default labels, so injection keeps firing after a rename. The cancel path's snapshot lookup resolves renamed labels.
  • No label collisions by construction. Rename labels embed the operation's sequence position, so two renames in a sequence can never draw the same label, and the old-label invariant gained an identity guard so a slot legitimately renamed onto a freed label is not flagged.
  • Renames are recorded before property predictions, so the template's NAME resolves to the new label the engine persists, and unmentioned-slot reverts in failed/canceled commands restore the overlay a dropped rename would otherwise leak into the model.
  • The focused test cannot pass vacuously. TestProperty_RenameViaApply drains between operations (single-stack admission conflicts otherwise reject most rename-carrying applies) and asserts at least one rename was accepted across the run.

Verified locally: package unit tests green, TestProperty_RenameViaApply green at 25 checks with 6 renames exercised, TestProperty_FullChaos green at 25 checks (~12s/iteration, unchanged from the pre-rename baseline) under the full invariant suite.

Known limitation: under FullChaos, rename-carrying applies land at a low rate (stack-overlap admission rejections are normal chaos behavior), so chaos-path rename coverage accumulates over CI's 100-check runs rather than every run exercising many renames. The focused test provides the deterministic coverage.

naxty and others added 2 commits August 22, 2026 12:32
Rename is a kind of update — the engine emits OperationUpdate for a
label-only change — so the property tests model it as a rename overlay
on OpApply rather than as a separate operation kind.

What lands:

- Operation gets RenameSlotIndex / RenameNewLabel fields, optional on
  OpApply. When set on an apply that targets an existing slot, the
  forma carries Label=NewLabel and Alias=<slot's current label> for
  that one resource. Combined with the per-apply property template,
  an update naturally models label-only, property-only, or both.
- Generator: with EnableRename on, ~33% of OpApply draws pick one
  parent slot from ResourceIDs to rename and a fresh label. Parent-
  slot restriction stays because the forma builder doesn't thread
  label overrides through ParentLabelForStack — renaming a parent
  with children would leave the children's resolvable references at
  the parent's old label.
- Executor: after FormaFromPoolResources / FormaFromStackResources
  builds the forma, the rename overlay flips the matching resource's
  Label/Alias and calls RecordRename on success. Snapshot revert on
  cancel/failure picks up CurrentLabel/PreviousLabel via the existing
  snapshot path (ResourceSnapshot gained those fields).
- StateModel:
  - LabelForResource, LabelForSlot, FindExistingResourceWithNativeID,
    NativeIDsByLabel, resolveResourceUpdateSlot all honour the
    CurrentLabel overlay so post-rename outcome resolution, drift
    tracking, and invariant checks match the renamed slot.
  - RecordRename retargets pending entries in ManagedDriftedResources
    (keyed by NativeID, ResourceLabel rewritten to the new label) so
    HasPendingManagedDriftForResource keeps matching after a rename.
  - LabelOverrides is consulted by every FormaFrom*Resources caller
    (executeApply, executeDestroy, executeSetTTLPolicy, SetupStacks,
    FormaFromResourceIDs) so subsequent ops see the renamed label.

- Invariants: new CheckRenameInvariants asserts (a) no managed
  inventory row carries a slot's PreviousLabel and (b) for every
  tracked NativeID, the inventory row's Label matches the slot's
  CurrentLabel-aware label. Wired into AssertAllInvariants alongside
  the existing duplicate-NativeID guard. New
  ViolationRenameOldLabelStillPresent and
  ViolationRenameLabelDriftFromNativeID kinds.

- New TestProperty_RenameViaApply runs the OpApply-with-rename path
  in isolation (single stack, no chaos) so any rename regression
  points squarely at the rename code rather than at chaos
  interactions. 50 rapid iterations pass locally.

- TestProperty_FullChaos keeps EnableRename off for now. Folding
  rename into Apply doesn't fix the harness's expected-State /
  Properties prediction drift under cancel × ForceReconcile ×
  partial-success applies (the drift fires even on slots that were
  never renamed; rename simply expands rapid's op space enough to
  reach those orderings sooner). Tightening the harness prediction
  model is a separate gap.

- Makefile test-property target's -run pattern includes
  TestProperty_RenameViaApply in the 50-iteration tier alongside the
  existing sequential/concurrent tests.
…ad label overlays end to end

The rename overlay is now folded into the label overrides before the forma
is built, so child $res references to a renamed slot carry the new label,
and any slot (not just parents) can be renamed. Rename labels embed the
operation's sequence position, making label reuse within a sequence
impossible by construction.

Identity preservation is verified from the engine's own reporting instead
of trusting the model's optimistic bookkeeping: the model tracks KSUIDs
alongside NativeIDs, an update RU that changes either identity is flagged
before the model adopts the new value, and a successful command that
carried a rename must contain the update RU the alias path produces —
its absence means the rename was dropped or executed as destroy+recreate.
The old-label invariant gained an identity guard so a different slot
legitimately renamed onto a freed label is not flagged, and the positive
check now asserts KSUID stability per tracked NativeID.

Failed or canceled commands restore the rename overlay for snapshotted
slots that produced no resource update, and the cancel path's snapshot
lookup honours renamed labels. Failure-injection programming addresses
slots by index rather than round-tripping through default labels, so
injection keeps working after a rename.

FullChaos runs with rename enabled under the full invariant suite, and
the focused rename test asserts at least one rename was accepted across
the run so a rename path that rejects everything cannot pass vacuously.
@JeroenSoeters
JeroenSoeters force-pushed the test/rename-via-apply-rebased branch from 7cd4880 to 9cabcb2 Compare August 22, 2026 19:32
@JeroenSoeters
JeroenSoeters merged commit 88fce62 into main Aug 22, 2026
56 of 57 checks passed
@JeroenSoeters
JeroenSoeters deleted the test/rename-via-apply-rebased branch August 22, 2026 20:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants