docs(nip-fi): scope administrative expiry to the grant and stop rotation clearing it

Two defects found by running a bounded state model of the composed core +
LIFECYCLE machine in two encodings -- one holding every guard the documents
state plus the guards a careful implementer would infer, one holding only the
guards actually written. Both were invisible to four line-by-line readers
because reading supplies the missing rule unconsciously.

Defect 1: administrative expiry was escapable by rotation. LIFECYCLE said an
expired binding "remains durable and occupies both sides of the core partial
bijection", so it stays in the relation -- and core Rotate replaces one exact
"active" binding with "a fresh binding version" while no document said the
replacement inherits binding_not_after. Reading the expired binding as active
let rotation authority alone clear a bound only expiry authority had set;
reading it as inactive removed it from TargetEligible, letting
ProvisionBinding double-bind the identity or bind the administratively
terminated key to a different identity, violating FI-INV-01 -- the invariant
LIFECYCLE was leaning on. FI-LC-ADMIN-EXPIRY did not detect either: core Rotate
is authorized and version-checked, so the escape satisfied the oracle's own
wording.

Defect 2: nothing in the six files said what binding_not_after is a bound *on*.
Two reviewers resolved it in opposite directions -- one grant-scoped, one
identity-scoped -- and the readings differ by 25,200 reachable states. The
identity-scoped reading also makes RetirePair followed by ordinary enrollment an
escape, which under the grant-scoped reading is a legitimately new grant.

Repairs:

- Core Rotate states that it continues one grant onto a new key and preserves
  every profile-defined administrative bound as an opaque field core neither
  interprets nor clears.
- LIFECYCLE declares the bound grant-scoped, names the transitions that
  establish a new grant carrying no prior bound, and points identity-scoped
  deadlines at the capability projection in authoritative local-policy state,
  which already carries the revocation-bound machinery such a deadline needs.
  Encoding one here instead would put an authorization-relevant deadline in a
  store with no revocation bound.
- LIFECYCLE defines a binding with a reached bound as active for every core
  relation and eligibility test, closing the TargetEligible horn.
- Binding-creating transitions must declare continuation or establishment; the
  two cases partition that set with no remainder, so a future profile cannot
  add a creator whose bound semantics are undefined.
- FI-LC-ADMIN-EXPIRY gains the rotation-must-not-clear arm and the negative arm
  that retire-then-enroll yields an unbounded binding and is conformant, so the
  oracle no longer admits the violation it exists to catch.

Verification of the shipped bytes, not the intent: re-encoding the model from
this text gives 0 grant-scoped escapes (17,184 before) and 0 FI-INV-01/FI-INV-03
regressions over 282,528 states across all three enrollment policies. Each
clause was mutated separately and each goes red only for its own clause --
dropping the Rotate carry restores 21,216 escapes, and dropping the active
definition admits both FI-INV-01 violations. A clause that cannot be made to
fail is not a guard.

Co-authored-by: Tyler Longwell <tlongwell@squareup.com>
Signed-off-by: Tyler Longwell <tlongwell@squareup.com>

docs/nips/NIP-FI-LIFECYCLE.md

@@ -51,6 +51,27 @@ It also permits a core binding to carry `binding_not_after`, an optional
 administrative deadline. The pending lineage names one exact retired pair and
 binding version. There is at most one pending lineage per identity.
 
+`binding_not_after` bounds the grant represented by **one binding**; it is not a
+bound on the identity. Rotation continues the same grant: the replacement binding
+preserves the carried bound, and only expiry authority changes it. Retirement,
+revocation, disablement, re-enablement, provisioning, and ordinary enrollment
+establish a *new* grant that carries no prior bound — so retirement of a bound
+pair followed by ordinary enrollment under `attested-key` or `tofu` policy yields
+an unbounded binding, and that is conformant. A deadline that must survive the end
+of a grant — an identity-scoped access bound — belongs in the capability
+projection of authoritative local-policy state, which core already requires for
+any projection whose removal must close authority within a declared bound and
+which is reread at preparation, final admission, and every protected lease use.
+`binding_not_after` is not that mechanism and cannot substitute for it: it does
+not survive the end of the grant that carries it, so a deployment relying on it
+for identity-scoped expiry cannot claim a revocation bound for that expiry
+(`FI-LC-ADMIN-EXPIRY`).
+
+A binding carrying a reached bound is **active** for every core relation and
+eligibility test in this profile and in core, including the core partial
+bijection and `TargetEligible` below. It is ineligible for authorization, not
+absent from the binding relation.
+
 `X_D`, `Q_D`, and `binding_not_after` are deployment-local state. Their versions
 are revalidation dependencies, not contract identities. A change invalidates a
 prepared decision and every dependent lease unless complete final-admission
@@ -88,6 +109,14 @@ MUST leave all authoritative state unchanged (`FI-LC-ATOMIC`). Lease
 invalidation MAY be delivered asynchronously, but authorization use after the
 commit MUST recheck the advanced dependency before allowing an operation.
 
+Every transition that creates a binding MUST state whether it **continues** an
+existing grant, and therefore preserves that grant's administrative bound, or
+**establishes** a new grant carrying no prior bound. The two cases partition the
+binding-creating transitions with no remainder: core rotation continues, and
+provisioning, re-enablement, and ordinary enrollment establish. A profile that
+adds a binding-creating transition without this declaration cannot claim
+conformance (`FI-LC-CLAIM`).
+
 `TargetEligible(i, k, allow_disabled)` means that `k` is not revoked, `(i, k)`
 is not retired, neither `i` nor `k` has an active binding, and `i` is not
 disabled unless `allow_disabled` is true. Every new target key requires fresh,
@@ -168,9 +197,11 @@ SetAdministrativeExpiry(i, k, old_version, binding_not_after?):
 This transition changes neither side of the pair nor its provenance. Setting,
 replacing, or clearing the bound advances the binding version. At equality the
 binding is ineligible but remains durable and occupies both sides of the core
-partial bijection. Only this or another applicable privileged transition can
-restore access; ordinary authorization cannot renew the bound
-(`FI-LC-ADMIN-EXPIRY`).
+partial bijection. This transition is the only expiry authority: no other
+transition in this profile or in core sets, replaces, or clears the bound, and
+core rotation carries it onto the replacement binding unchanged. Only this or
+another applicable privileged transition can restore access; ordinary
+authorization cannot renew the bound (`FI-LC-ADMIN-EXPIRY`).
 
 ## One-shot lineage and concurrency
 
@@ -195,7 +226,7 @@ denied case.
 
 | ID | Setup and required result |
 |---|---|
-| `FI-LC-CLAIM` | For a fixed profile set, compare complete discovery bytes across attested-key, TOFU, and provisioned configurations and across lifecycle states: they are identical. If one protected ingress omits lifecycle gates or uses a different lifecycle lineage, the domain cannot advertise the profile and the uncovered ingress fails closed. |
+| `FI-LC-CLAIM` | For a fixed profile set, compare complete discovery bytes across attested-key, TOFU, and provisioned configurations and across lifecycle states: they are identical. If one protected ingress omits lifecycle gates or uses a different lifecycle lineage, the domain cannot advertise the profile and the uncovered ingress fails closed. If any claimed profile defines a binding-creating transition that declares neither grant continuation nor grant establishment, the domain cannot advertise that profile. |
 | `FI-LC-ORDINARY-GATES` | Fresh assertion and proof for a disabled identity, an identity with pending lineage, and a binding at administrative-expiry equality each deny without changing lifecycle state. |
 | `FI-LC-AUTHORITY` | An ordinary assertion plus valid Nostr proof, but no transition-specific authority, cannot perform any transition; mutation of any authority-bound field denies. |
 | `FI-LC-ATOMIC` | Inject failure at each transition write boundary; no binding, tombstone, disabled fact, lineage, history entry, or dependency version is partially committed. |
@@ -203,7 +234,7 @@ denied case.
 | `FI-LC-PROVISION` | Ordinary first use in provisioned mode denies; authorized provisioning creates one binding and no lease; later current ordinary admission may use it. |
 | `FI-LC-DISABLE` | Disabling an active identity atomically disables it, retires its exact pair, records exact lineage, and closes subsequent lease use; replay is idempotent and preserves lineage. |
 | `FI-LC-REENABLE` | Re-enablement creates an eligible proven binding in the same commit that clears disabled state; absent or wrong expected lineage and a clear-only attempt deny. |
-| `FI-LC-ADMIN-EXPIRY` | Before the bound the binding may authorize; at equality it denies while still occupying the relation; only an authorized version-checked update changes the bound. |
+| `FI-LC-ADMIN-EXPIRY` | Before the bound the binding may authorize; at equality it denies while still occupying the relation, so a target eligibility test for either side of that pair fails. Rotating the expired binding to a new key carries the bound: the replacement denies at the same instant. No non-expiry transition clears it. Only an authorized version-checked update by the expiry authority changes the bound. Conversely, retirement, revocation, or re-enablement of the bound pair followed by an authorized or ordinary new grant produces an unbounded binding, which is the required result and not an escape. |
 | `FI-LC-QD-ONCE` | Two concurrent re-enablings consume the same `Q_D` lineage; exactly one commits and the loser leaves every authoritative store unchanged. |
 | `FI-LC-RACE` | Race each transition against prepared ordinary admission and lease use; no operation authorizes after observing the advanced lifecycle or binding dependency. |
 

docs/nips/NIP-FI.md

@@ -416,7 +416,11 @@ any policy-required current matching issuer attestation. [FI-TRACE-LIFECYCLE-AUT
   non-retired target key, retires the old pair, and creates a fresh binding
   version. The replacement provenance is `attested-key` when current matching
   issuer attestation was validated and `provisioned` otherwise. Rotation does
-  not globally revoke the old key.
+  not globally revoke the old key. Rotation continues one grant onto a new key
+  rather than establishing a new one: the replacement preserves every
+  profile-defined administrative bound carried by the binding it replaces, as an
+  opaque field core neither interprets nor clears. Only the authority that set
+  such a bound can change it. [FI-TRACE-LIFECYCLE-AUTHORITY]
 
 Failure or stale state causes no partial mutation. Ordinary authorization cannot
 perform or undo these transitions. Extended disablement, re-enablement,