feat(kernel): always-on composite cross-entity verification + self-heal floor (ARN-92)#325
Merged
Merged
Conversation
…of (ARN-92) The L1 model lowered ModelGuard::CrossEntityState to constant false, so a cross-entity-gated transition (e.g. Publish gated on a file being Ready) was never offered during exploration — its target state was unreachable and any safety/liveness obligation behind the gate passed vacuously, with a dead-transition special-case papering over it. Split guard evaluation into two predicates: evaluate_guard (local enablement — cross-entity stays false, keeping no_deadlock/no_further_transitions sound) and guard_may_hold (state-space exploration — cross-entity is a free/nondeterministic boolean, so the guarded edge IS offered and its target + properties are explored non-vacuously). Remove the cross-entity special-case from find_dead_transitions. Supersedes the merged exemption band-aid (#317) with the real proof. ADR-0149. temper-verify: 103 passed, cross_entity_abstract green; 4 existing cross-entity specs hold (Agent L1 15->18 states, 0 dead). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ped-reaction (ADR-0150) temper verify now builds composite scope automatically for a multi-entity spec dir (seeds = roots of each weakly-connected component of the trigger graph) and runs the joint cross-entity BFS as a first-class GATING cascade step. Adds a no_dropped_reaction property: a triggered reaction whose target action is disabled at the target's current state is a counterexample. create resolvers are exempt; a per-trigger drop_ok=true opts out an intentional best-effort drop. Honest budget (incomplete, never silent pass). Single-spec/stdin stays per-entity. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ite verification Composite cross-entity verification (ADR-0150) found 4 dropped-reaction bugs in the kernel filesystem specs: - Workspace usage accounting dropped when the workspace was Frozen/Archived. Fix: a Frozen/Archived workspace rejects new writes — File.StreamUpdated is guarded on the owning Workspace being Active, and the $value PUT handler rejects the write BEFORE persisting bytes when the workspace is not Active (no bytes-written- but-state-rejected seam). - FileVersion double-supersede: Supersede is now idempotent (Superseded -> Superseded). - File.RecordVersion back-pointer dropped before Ready: accepted from Created as a state-preserving self-loop (recording a version pointer must not advance lifecycle). Composite verify on os-apps/temper-fs/specs now PASSES with no dropped reactions. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ss-entity ref, integration-never-silent
Three pieces the in-session self-heal rests on:
- Guard identity in errors (ADR-0151): a failed IOA guard now names which guard
and field failed ("guard cross_entity_state on 'landing_file_id' requires
status in [Ready,Locked], found <missing>") instead of a generic
"not valid from state X". Guard::check_detailed returns the first failing
sub-guard; TransitionResult carries it; entity_actor renders it. This is the
agent-facing contract that lets an in-session agent self-heal.
- Required cross-entity ref (ARN-92 #2): a `required` attr threaded parser ->
StateVarMetadata -> JIT Guard -> cross_entity; an empty REQUIRED scalar/list
ref now FAILS its cross_entity_state guard instead of passing vacuously, while
optional relations stay vacuous-true.
- Integration failure is never silent (ADR-0152): an integration returning
success:false with no declared on_failure propagates (inline) or dispatches a
deterministic compensating Fail (background) instead of being dropped; a
surfaced critical metric + Observe event when no recovery edge exists. The
durable transition can't be rolled back post-commit, so it's compensation, not
rollback (respects the async write path).
temper-server 519 lib tests, temper-jit 306, temper-spec; cascade + composite
ALL PASSED; temper-jit has no temper-verify dep.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The always-on composite cross-entity verification feature (+4189 LOC, reviewed PASS, clippy clean) modestly increases tracked debt metrics, all legitimate: +8 PROD_PRINTLN (the 'temper verify' composite report output — seed/PASS/INCOMPLETE lines), +1 file >500/>1000 (the composite model), +1 clippy-allow, +1 // ci-ok unwrap (infallible lock). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… transitions
A12079ef guarded File.StreamUpdated with
`cross_entity_state required_status = ["Active"]` to make a Frozen/Archived
Workspace reject new writes. That allowlist was stricter than the intent: it
also required the Workspace to EXIST and resolve to Active, so system-doc and
bootstrap Files whose owning Workspace is not resolvable at write time could
never advance Created -> Ready. This broke two temper-platform install tests.
Intended semantic: reject a write ONLY when the Workspace exists and is
Frozen/Archived; a missing/empty/unresolved Workspace must ALLOW the write.
Two root-cause fixes:
1. Add a `forbidden_status` (denylist) mode to the `cross_entity_state` guard,
threaded through every layer: temper-spec (types, toml parser, translate,
TLA+ render, lint render), temper-jit (CrossEntityStateIn + builder +
failure message), temper-verify (model types/builder, composite
guard_cross_entity_ok, SMT encoding), and the runtime resolver. A resolvable
target passes iff (allowlist empty OR status in allowlist) AND status not in
denylist. A non-empty ref to an unresolvable target: allowlist-constrained or
`required` -> reject; denylist-only and optional -> allow. The File guard is
now `forbidden_status = ["Frozen", "Archived"]`. For the in-scope Workspace
states {Active, Frozen, Archived} this is drop-suppression-equivalent to the
old allowlist, so composite verification still PASSES with no dropped
reactions; the difference is only the missing/unresolved case.
2. Fix a latent replay bug exposed by the guard. EntityActor::replay_events
re-evaluated each stored event's guard with a context that does not
reconstruct related entities, so a cross-entity-guarded transition was
silently dropped on replay — a File that committed Created -> Ready
rehydrated back to Created. A persisted event is committed history: replay
now re-derives effects via the new TransitionTable::replay_effects (no
re-gating) and always honors the durably-stored to_status.
Verified: the two temper-platform install tests pass; file_value_fast_path
(the 4-bug-fix proof, incl. Frozen-rejects-write) still 17/17; composite
`temper verify --specs-dir os-apps/temper-fs/specs` PASSES (File scope 132
joint states, no dropped reactions); new tests prove a Frozen/forbidden target
still rejects, an unresolvable target allows (optional) / rejects (required),
and a committed cross-entity-guarded transition survives replay.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
The Temper kernel floor under the Katagami re-architecture: the engine proves cross-entity validity and gives agents a verifiable self-heal contract, so determinism-critical work lives in verified state machines rather than glue. Off post-#324 main (ARN-87/89 already landed).
The changes
guard_may_hold(exploration) vsevaluate_guard=false(local enablement); cross-entity guards aren't vacuously false, L1 proofs are non-vacuous.no_dropped_reactionproperty, gating only on realViolated. Large products report INCOMPLETE (warn), never a vacuous hard-fail; single-entity specs untouched. Cannot newly break a previously-green app.requiredattr into the model builder.Verification
Independent pre-merge review: PASS, no findings (regression-risk, guard-semantics, DST, compensation, dep-hygiene, band-aids). Live-verified
temper verifypasses on realos-apps/temper-fs(composite green, 132 joint states, no dropped reactions). Suites green: temper-verify 72 + composite, temper-cli 112, temper-jit 47, temper-server 519, required_ref 3; clippy clean. Readability baseline updated intentionally (modest, legitimate increases from the verifier feature; see chore commit).Linear: ARN-92.