Behavior catalogue
Generated from the reviewed semantic case inventory. Reviewed feature and known-corner-case inventory derived from C01-C60/W01-W09, docs, tests, and all positive portable scenarios. Evidence describes bounded observations; this is not an exhaustive input or schedule proof. Native binding cases are catalogued separately.
These links describe registered evidence and its scope. They are not a fresh test result or a claim of exhaustive coverage. See the validation guide for how a completed run is established.
All supported ports replay the shared histories through their native drivers. TypeScript replay tests · Go replay tests · Rust replay tests · Python replay tests.
| Case | Behavior | Model and regression evidence | Shared replay evidence |
|---|---|---|---|
| C01.no-cache-plumbing | disabled calls bypass policy and caches | passThroughSkipsCacheMachinery: Disabled/outside/closed calls make zero policy, key, cache read, or cache write operations in the presence-bit model; no clock claim. disabledAndRequestCallsKeepTheirOwnLifetimesTest: The introductory profile alternates disabled calls and separate request-local pairs across a source change; results and source/read/write counts establish those lifetimes. This does not separately observe key construction or runtime policy. closedScopeCallerBypassesLayersAndAdmitsNoJobTest: A closed-scope caller starts an unbounded bypass source without policy lookup, cache reads, shadow admission or fallback-error diagnostics. | scope / disabled-bypass dark-layers / closed-scope-bypasses-dark-work core/disabledAndRequestCallsKeepTheirOwnLifetimesTest dark-layers/closedScopeCallerBypassesLayersAndAdmitsNoJobTest |
| C01.no-deadline | outside calls have no fallback deadline or sharing | outsideSourcesHaveNoDeadline: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. outsideAndInvalidOutsideCallsIgnoreDeadlineAndSharingTest: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. | source-budgets / outside-calls-skip-source-deadlines-sharing-and-publication source-budgets/outsideAndInvalidOutsideCallsIgnoreDeadlineAndSharingTest |
| C02.nested-memo | nested enable and disable preserve outer memo | nestedDisablePreservesMemoTest: Nested enable/disable leaves the outer memo available on reenable. | scope / nested-memo-hit |
| C02.reenabled-memo | reenabling inside disabled scope reuses memo and preserves siblings | nestedCloseAndDisabledBypassKeepOuterMemoTest: One nested enabled, disabled, and reenabled history preserves the root value; other sibling histories remain generated replay evidence. | scope / reenabled-memo-hit scope/nestedCloseAndDisabledBypassKeepOuterMemoTest |
| C03.late-publication | late old-scope value cannot enter a replacement scope | requestValueBelongsToCurrentScope: A memo value belongs to the currently open scope; replacement scope receives no late old value. lateResultCannotEnterReplacementScopeTest: A memo value belongs to the currently open scope; replacement scope receives no late old value. closedScopesHaveNoMemo: Closed slots contain no memo/flight, and a replacement probe starts new source work after the old source settles. lateSourceCannotPopulateReplacementTest: Closed slots contain no memo/flight, and a replacement probe starts new source work after the old source settles. | scope / replacement-miss-after-late-source scope/lateSourceCannotPopulateReplacementTest |
| C03.detached-bypass | Calls using a closed outer context bypass caching | passThroughSkipsCacheMachinery: Outside/closed calls have no key, policy, or cache effects in the presence-bit model; source deadlines are not modeled here. | scope / detached-bypass |
| C04.pending-policy | policy resolution after scope closure is pass-through | policyReplyAfterCloseBypassesRequestTest: A provider released after root closure invokes source outside caching and writes no memo. | scope / policy-reply-after-close scope/policyReplyAfterCloseBypassesRequestTest |
| C05.participating-publication | untracked source fills remote local and request layers | untrackedSourcePublishesToAllParticipatingLayersTest: untracked source fills remote local and request layers. This check covers the bounded model clause: untrackedSourcePublishesToAllParticipatingLayersTest. Host representations and other feature combinations retain separate fixed/native evidence. untrackedSourcePublicationIsProbedInAllThreeLayersTest: One untracked source fills the request memo, the local layer and Redis; a same-scope memo hit, a fresh-context local hit and an other-instance remote hit each return the published value with no second source. Tracked validation and detached scopes retain separate evidence. | layers / source-publication-probed-in-all-three-layers layers/untrackedSourcePublicationIsProbedInAllThreeLayersTest |
| C05.first-hit | local hit stops new shadow work | darkSourcePublishesLocalBeforeShadowWriteTest: A later request/local hit bypasses remote reads and new shadow admission. Foreground validated remote bytes may warm local storage, but the detached diagnostic source never does: a differing diagnostic value preserves the served/local value or leaves an unpopulated local layer cold. darkSourcePublishesRequestBeforeShadowWriteTest: A later request/local hit bypasses remote reads and new shadow admission. Foreground validated remote bytes may warm local storage, but the detached diagnostic source never does: a differing diagnostic value preserves the served/local value or leaves an unpopulated local layer cold. validatedRemoteHitStopsFurtherShadowTest: A later request/local hit bypasses remote reads and new shadow admission. Foreground validated remote bytes may warm local storage, but the detached diagnostic source never does: a differing diagnostic value preserves the served/local value or leaves an unpopulated local layer cold. servedDiagnosticSourceDoesNotPopulateLocalTest: A later request/local hit bypasses remote reads and new shadow admission. Foreground validated remote bytes may warm local storage, but the detached diagnostic source never does: a differing diagnostic value preserves the served/local value or leaves an unpopulated local layer cold. | shadow-layers / dark-local-source-publication-stops-later-shadow shadow-layers / dark-request-source-publication-is-scope-local shadow-layers / validated-remote-hit-warms-local-and-stops-shadow shadow-layers / served-diagnostic-source-never-publishes-local shadow-layers/darkSourcePublishesLocalBeforeShadowWriteTest shadow-layers/darkSourcePublishesRequestBeforeShadowWriteTest shadow-layers/servedDiagnosticSourceDoesNotPopulateLocalTest shadow-layers/validatedRemoteHitStopsFurtherShadowTest |
| C06.null-request | null remains a value in request cache | requestFalsyValuesRemainDistinctAndReusableTest: null remains a value in request cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | scope / memo-value:6 runtime-boundaries/requestFalsyValuesRemainDistinctAndReusableTest |
| C06.null-local | null remains a value in local cache | localFalsyValuesRemainDistinctAndReusableTest: null remains a value in local cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / local-value:6 runtime-boundaries/localFalsyValuesRemainDistinctAndReusableTest |
| C06.null-remote | null remains a value in remote cache | remoteFalsyValuesRemainDistinctAndReusableTest: null remains a value in remote cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / remote-value:6 runtime-boundaries/remoteFalsyValuesRemainDistinctAndReusableTest |
| C06.false-request | false remains a value in request cache | requestFalsyValuesRemainDistinctAndReusableTest: false remains a value in request cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | scope / memo-value:7 runtime-boundaries/requestFalsyValuesRemainDistinctAndReusableTest |
| C06.false-local | false remains a value in local cache | localFalsyValuesRemainDistinctAndReusableTest: false remains a value in local cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / local-value:7 runtime-boundaries/localFalsyValuesRemainDistinctAndReusableTest |
| C06.false-remote | false remains a value in remote cache | remoteFalsyValuesRemainDistinctAndReusableTest: false remains a value in remote cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. falsyRemoteValuesAreServedFromRemoteTest: With the local layer disabled, a false source result is written to Redis and the next same-key call is a remote hit returning false. The zero and empty-string results share this schedule; host encodings remain fixed-scenario evidence. | policy / remote-value:7 runtime-boundaries/remoteFalsyValuesRemainDistinctAndReusableTest policy/falsyRemoteValuesAreServedFromRemoteTest |
| C06.zero-request | zero remains a value in request cache | requestFalsyValuesRemainDistinctAndReusableTest: zero remains a value in request cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | scope / memo-value:8 runtime-boundaries/requestFalsyValuesRemainDistinctAndReusableTest |
| C06.zero-local | zero remains a value in local cache | localFalsyValuesRemainDistinctAndReusableTest: zero remains a value in local cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / local-value:8 runtime-boundaries/localFalsyValuesRemainDistinctAndReusableTest |
| C06.zero-remote | zero remains a value in remote cache | remoteFalsyValuesRemainDistinctAndReusableTest: zero remains a value in remote cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. falsyRemoteValuesAreServedFromRemoteTest: With the local layer disabled, a zero source result is written to Redis and the next same-key call is a remote hit returning zero. The false and empty-string results share this schedule; host encodings remain fixed-scenario evidence. | policy / remote-value:8 runtime-boundaries/remoteFalsyValuesRemainDistinctAndReusableTest policy/falsyRemoteValuesAreServedFromRemoteTest |
| C06.empty-string-request | empty string remains a value in request cache | requestFalsyValuesRemainDistinctAndReusableTest: empty string remains a value in request cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | scope / memo-value:9 runtime-boundaries/requestFalsyValuesRemainDistinctAndReusableTest |
| C06.empty-string-local | empty string remains a value in local cache | localFalsyValuesRemainDistinctAndReusableTest: empty string remains a value in local cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / local-value:9 runtime-boundaries/localFalsyValuesRemainDistinctAndReusableTest |
| C06.empty-string-remote | empty string remains a value in remote cache | remoteFalsyValuesRemainDistinctAndReusableTest: empty string remains a value in remote cache. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. falsyRemoteValuesAreServedFromRemoteTest: After the earlier key reaches its fresh boundary, an empty-string source result refills Redis and the next same-key call is a remote hit returning the empty string. The false and zero results share this schedule; host encodings remain fixed-scenario evidence. | policy / remote-value:9 runtime-boundaries/remoteFalsyValuesRemainDistinctAndReusableTest policy/falsyRemoteValuesAreServedFromRemoteTest |
| C06.absent-request | undefined is a memoized value | absentValueIsMemoizedTest: The explicit absent value code is memoized and reused without a second source. | scope / memo-value:5 scope/absentValueIsMemoizedTest |
| C06.absent-local | absent result remains cacheable in local storage | absentValueIsStoredAndReusedTest: A source absent value is published and the subsequent local hit reuses it; this regression does not probe remote-only reuse. | policy / local-value:5 policy/absentValueIsStoredAndReusedTest |
| C06.absent-remote | absent result remains cacheable in remote storage | remoteAbsenceAndLiteralTextStayDistinctTest: absent result remains cacheable in remote storage. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / remote-value:5 runtime-boundaries/remoteAbsenceAndLiteralTextStayDistinctTest |
| C07.scope-isolation | concurrent outer request scopes retain independent flights and memo | separateRequestRootsRetainIndependentValuesTest: concurrent outer request scopes retain independent flights and memo. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | scope / independent-scope-overlap layers/separateRequestRootsRetainIndependentValuesTest |
| C07.no-capacity-limit | request memo has no process local capacity cap | requestMemoExceedsLocalCapacityTest: Three request identities remain memoized with zero process-local capacity; a bounded independence check, not an unbounded allocation claim. | layers / request-memo-exceeds-local-capacity layers/requestMemoExceedsLocalCapacityTest |
| C08.shared-capacity | shared local capacity spans operation identities | capacityIsPerInstance: Capacity applies across operation identities within each instance, with a concrete eviction probe after recency promotion. localReadPromotesBeforeEvictionTest: Capacity applies across operation identities within each instance, with a concrete eviction probe after recency promotion. | layers / lru-eviction-probed layers/localReadPromotesBeforeEvictionTest |
| C08.instance-capacity | instances isolate local storage and registered flights | oneInstanceEvictionCannotEvictAnotherInstanceTest: instances isolate local storage and registered flights. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. sourceOwnershipNeverCrossesKeyOrInstance: instances isolate local storage and registered flights. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | layers / capacity-is-per-instance layers / different-instances-own-distinct-flights layers/oneInstanceEvictionCannotEvictAnotherInstanceTest |
| C08.read-promotes | Reading an entry promotes it before a later LRU eviction | localReadPromotesBeforeEvictionTest: A middle local hit promotes recency, and subsequent probes distinguish which operation identity was evicted. | layers / lru-read-promotes layers / promoted-value-survives-eviction layers/localReadPromotesBeforeEvictionTest |
| C09.fixed-local-ttl | Local hits preserve insertion expiry; the exact TTL boundary expires | localHitDoesNotRenewInsertionTtlTest: A hit at 500ms leaves the original 1000ms insertion deadline; the exact-boundary probe starts a new source. localHitsRespectInsertionExpiry: Independent local-hit receipts retain observation time and insertion expiry; each recorded hit occurred strictly before that fixed expiry. localBoundaryIsExclusive: Finite symbolic cases compare the canonical local-expiry judgment with the independently stated strict observation-before-expiry inequality. localGridUsesWholeMilliseconds: Finite submillisecond examples independently check flooring insertion and observation times before local age comparison; this is the grid decision, not an entire native clock implementation. localEntryExpiresAfterItsTtlTest: In the composed source-budgets profile a local entry published at settlement is served to a same-key enabled call one millisecond before its 1000ms insertion expiry and no longer at the exact boundary, where the next call starts a source; the deterministic regression pins the public result and loader count at both instants. localEntryExpiresAtItsInsertionTtlTest: An untracked source warms the local slot for its 1 s insertion TTL; the transient caller hits at 999 ms and reads again at exactly 1000 ms, so the boundary is exclusive. localEntryExpiresAtItsInsertionTtlTest: A dark-invalid-shadow caller's source settles and warms the local slot for 60 s; the hit at that insertion and the miss at exactly 60 000 ms after it (the drivers' 60 s advance) make the boundary exclusive. | policy / local-hit-preserves-insertion-expiry policy/localHitDoesNotRenewInsertionTtlTest source-budgets/localEntryExpiresAfterItsTtlTest recovery-read/localEntryExpiresAtItsInsertionTtlTest shadow-layers/localEntryExpiresAtItsInsertionTtlTest |
| C09.wall-rollback | local expiry uses monotonic time across application wall rollback | wallRollbackDoesNotExtendLocalTtlTest: Local expiry advances on elapsed time despite wall-clock rollback. | policy / rollback-preserves-live-local policy / rollback-does-not-extend-local-ttl policy/wallRollbackDoesNotExtendLocalTtlTest |
| C09.insertion-age | nearly expired remote hit warms local for its full insertion TTL | remoteHitStartsFullLocalInsertionTtlTest: nearly expired remote hit warms local for its full insertion TTL. This check covers the bounded model clause: remoteHitStartsFullLocalInsertionTtlTest. Host representations and other feature combinations retain separate fixed/native evidence. remoteHitWarmsLocalForTheReplysLocalTtlTest: A remote hit warms local storage for the reply's local TTL (2 s), not for the frame's remaining freshness (1 s): the entry still serves locally after the freshness has passed. This check covers the bounded model clause: remoteHitWarmsLocalForTheReplysLocalTtlTest. | policy / remote-hit-local-ttl-outlives-remote-freshness policy/remoteHitStartsFullLocalInsertionTtlTest policy/remoteHitWarmsLocalForTheReplysLocalTtlTest |
| C10.zero-capacity | zero local capacity retains coalescing but no settled value | zeroCapacityHasNoLocalValues: Zero capacity stores no local values, shares concurrent work, and starts a new source after settlement. zeroCapacityKeepsSharingWithoutStorageTest: Zero capacity stores no local values, shares concurrent work, and starts a new source after settlement. | layers / zero-capacity-still-shares layers / zero-capacity-reloads layers/zeroCapacityKeepsSharingWithoutStorageTest |
| C11.process-inspection | Public process-coalescing snapshots count only registered leaders and process followers for the selected instance, report the oldest monotonic registration age, and clear when callers settle even while raw source or shadow work continues. | inspectionTracksKeysFollowersAndOldestLeaderTest: Two live keys and request/process followers produce two leaders and one process follower. Success removes the oldest key and selects the remaining age; rejection empties the snapshot. inspectionIsPerInstanceAndUsesMonotonicTimeTest: Two instances retain separate live counts and monotonic ages despite wall rollback; settling instance zero leaves instance one active. inspectionExcludesRequestOnlyAndUncoalescedWorkTest: Pending request-only shared work and pending coalesce:false sources both remain absent from process snapshots. inspectionClearsTimedOutCallersWhileRawWorkRemainsTest: Source timeout clears leader/follower counts before held raw effects settle. A retry has its own live snapshot, unchanged by the abandoned source and read completing. inspectionExcludesUnfinishedShadowAfterCallerSuccessTest: A successful caller clears process ownership while its admitted dark job still holds serialization and then transport completion. inspectionsDescribeLiveLeaders: At each public inspection the leader count equals independently selected pending shared sources of the requested instance. inspectionsCountOnlyProcessFollowers: At each public inspection the follower count equals pending callers whose admission receipt joined process scope on the requested instance. inspectionAgeUsesTheOldestLiveMonotonicStart: At each public inspection the age is absent if no shared source remains; otherwise it equals a live source age and is at least every other live age, using monotonic start receipts. | dark-layers / inspection-counts-process-followers-and-oldest dark-layers / inspection-isolates-instances-and-wall-shifts dark-layers / inspection-excludes-request-and-uncoalesced dark-layers / inspection-clears-timeout-before-raw-settlement dark-layers / inspection-excludes-unfinished-shadow dark-layers/inspectionTracksKeysFollowersAndOldestLeaderTest dark-layers/inspectionIsPerInstanceAndUsesMonotonicTimeTest dark-layers/inspectionExcludesRequestOnlyAndUncoalescedWorkTest dark-layers/inspectionClearsTimedOutCallersWhileRawWorkRemainsTest dark-layers/inspectionExcludesUnfinishedShadowAfterCallerSuccessTest |
| C11.distinct-keys | different keys own independent flights | pendingSourcesKeepEntityAndOperationIdentityTest: different keys own independent flights. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. sourceOwnershipNeverCrossesKeyOrInstance: different keys own independent flights. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / cross-key-overlap layers/pendingSourcesKeepEntityAndOperationIdentityTest |
| C11.one-registered-flight | Eligible concurrent same-key calls share one registered source | oneRegisteredSource: At most one source has registered ownership in the one-key effects profile. Abandoned external work is distinct. runtimeLocalTtlEnablesSharingWithoutRemoteTtlTest: The newly enabled local layer makes two pending same-key calls share one source, and retains its Absent result for a later local hit without any Redis read/write. coalescedPairPublishesOneReusableValueTest: Two controlled same-key call pairs, separated by an external source change, share one initial source and reuse its published local value. pendingRequestFlightIsJoinedBeforeMemoReadTest: A coalescing caller joins the request flight registered under its row before the memo is read, although an independent source has since memoized a value into that row; the joined caller completes with the flight's value. coalescingCallerJoinsPendingFlightBeforeSeededFrameTest: A coalescing caller joins the flight registered for its identity before reading the remote layer; a frame seeded while the flight is pending does not serve it. This check covers the bounded model clause: coalescingCallerJoinsPendingFlightBeforeSeededFrameTest. uncoalescedPublicationDoesNotPreemptTheRegisteredLeaderTest: An independent source settles beside a registered dark leader; a later coalescing caller still joins that leader and receives its result rather than the independent result. | policy / coalesced-result dark-layers / uncoalesced-publication-keeps-dark-leader runtime-boundaries/runtimeLocalTtlEnablesSharingWithoutRemoteTtlTest core/coalescedPairPublishesOneReusableValueTest scope/pendingRequestFlightIsJoinedBeforeMemoReadTest layers/coalescingCallerJoinsPendingFlightBeforeSeededFrameTest dark-layers/uncoalescedPublicationDoesNotPreemptTheRegisteredLeaderTest |
| C12.separate-request-memos | request misses join one process flight then memoize separately | requestMissesShareProcessAndMemoizeSeparatelyTest: Two request scopes join one process source and both reuse their separate memos after shared settlement. | layers / request-misses-share-process-flight layers/requestMissesShareProcessAndMemoizeSeparatelyTest |
| C13.uncoalesced-caching | coalescing off keeps settled caching | independentLocalCallsStillReuseSettledValueTest: coalescing off keeps settled caching. This check covers the bounded model clause: independentLocalCallsStillReuseSettledValueTest. Host representations and other feature combinations retain separate fixed/native evidence. disabledSharingDoesNotJoinRegisteredFlightTest: Once a runtime reply disables sharing, a caller does not join the request flight an earlier shared caller registered under the same memo slot; its independent source memoizes, and the memo keeps the last settled value. independentSourceIsNotRegisteredForLaterSharingTest: A source started with coalescing off is registered under no memo row, so a later caller whose reply coalesces starts its own source instead of joining it. defaultSharingJoinsRegisteredLeaderOverWarmedLocalTest: A reply that disables sharing starts its own source beside the registered leader; once its value has warmed local storage, a reply that shares again joins the leader rather than hitting the entry. This check covers the bounded model clause: defaultSharingJoinsRegisteredLeaderOverWarmedLocalTest. uncoalescedCallerReadsAloneTest: A caller whose reply disables coalescing dispatches its own remote read beside the registered shared leader for the same identity; its hit is judged first and admits the job, and the leader's later hit drops as a duplicate. | policy / uncoalesced-local-settled-hit policy / uncoalesced-remote-settled-hit scope / uncoalesced-request-settled-hit policy/independentLocalCallsStillReuseSettledValueTest runtime-boundaries/disabledSharingDoesNotJoinRegisteredFlightTest scope/independentSourceIsNotRegisteredForLaterSharingTest runtime-boundaries/defaultSharingJoinsRegisteredLeaderOverWarmedLocalTest admission/uncoalescedCallerReadsAloneTest |
| C13.local-last-writer | independent local publication is last writer wins | independentLocalPublicationUsesLastCompletionTest: independent local publication is last writer wins. This check covers the bounded model clause: independentLocalPublicationUsesLastCompletionTest. Host representations and other feature combinations retain separate fixed/native evidence. independentFailureKeepsSettledLocalValueTest: In the policy profile with coalescing off and no remote layer, two callers on one key start their own sources; the first completes and publishes locally, the second settles with the source error and is not a local writer: the third call is served the entry the earlier completed source published, without a third source. No remote or memo claim. independentFailureKeepsLocalValueWhenRemoteFailsTest: Two uncoalesced sources begin after remote misses. The first publishes locally and remotely; the second rejects with no stale-recovery classifier configured, so it cannot recover the newer refill. With remote reads then failing, the retry still serves the surviving local value without a third source or remote read. This exposes local deletion on the active remote-chain failure path. rejectedSourceLeavesPublishedLocalEntryTest: In the composed source-budgets profile a source that settles with the source error completes its caller with that error and leaves the local entry an earlier accepted source published: the next enabled call is served locally without a third source. The rejected source is a bypass (outside) one, since a source that may warm local starts only while no live entry exists; no remote or memo claim. republishedEqualValueRestampsLocalExpiryTest: In the composed source-budgets profile the source started at the exact 1000ms expiry of a local entry republishes the same value and stamps a new insertion expiry: an enabled call one millisecond before the second boundary is served locally without a third source. Distinguishes a publication that skips an equal value from one that replaces it; no remote or memo claim. | policy / independent-local-last-completion-probed policy/independentLocalPublicationUsesLastCompletionTest policy/independentFailureKeepsSettledLocalValueTest policy/independentFailureKeepsLocalValueWhenRemoteFailsTest source-budgets/rejectedSourceLeavesPublishedLocalEntryTest source-budgets/republishedEqualValueRestampsLocalExpiryTest |
| C13.remote-last-writer | independent remote publication is last writer wins | independentRemotePublicationUsesLastCompletionTest: independent remote publication is last writer wins. This check covers the bounded model clause: independentRemotePublicationUsesLastCompletionTest. Host representations and other feature combinations retain separate fixed/native evidence. remoteHitPromotesIntoNewlyEnabledLocalLayerTest: A remote hit warms the newly enabled local layer; another already-running remote-only source then replaces Redis while the captured local value remains unchanged, distinguished by later local-enabled and remote-only reads. | policy / independent-remote-last-completion-probed policy/independentRemotePublicationUsesLastCompletionTest runtime-boundaries/remoteHitPromotesIntoNewlyEnabledLocalLayerTest |
| C14.inactive-layers | inactive serving layers do not coalesce | inheritedDisabledSharingNeverJoins: A caller released under inherited-disabled sharing never joins a flight: with no active serving layer it starts its own source, whatever flight is pending. inheritedFalseKeepsIndependentMemoizingSourcesTest: Two concurrent callers under inherited false sharing start two sources (s.o.loaders == 2): inactive serving layers do not coalesce. | policy / inactive-layers-independent-sources |
| C15.shared-error-retry | rejected request flight is shared then removed for retry | rejectedFlightAllowsRetryTest: One rejected source supplies both request followers, then a later call starts another source. | scope / shared-rejection scope / rejected-flight-retry scope/rejectedFlightAllowsRetryTest |
| C16.null-inherits | null provider inherits operation defaults | nullProviderRetainsEveryBaselineLeafTest: The omitted overlay representation preserves every baseline leaf. Literal null-to-omission normalization is exercised by the portable fixed scenario, not this abstract valid-policy model. nullProviderInheritsConfiguredServingAndDefaultSharingTest: Actual null provider response preserves configured remoteTTL/full omitted ramp/default sharing; existing runtime-policy leafwise invariant covers other leaves. | runtime-boundaries / null-provider-inherits-serving-and-sharing runtime-boundaries/nullProviderInheritsConfiguredServingAndDefaultSharingTest |
| C16.sparse-leaves | Runtime overlays replace only supplied leaves | runtimeOverlayIsLeafWise: Independently checks all eight captured leaves against runtime/base precedence without calling the transition resolve helper. This valid-overlay abstraction does not classify malformed host values. sparseLocalOverridePreservesRemoteAndFeaturesTest: Runtime overlays replace only supplied leaves. This check covers the bounded model clause: sparseLocalOverridePreservesRemoteAndFeaturesTest. Host representations and other feature combinations retain separate fixed/native evidence. | policy / sparse-empty-provider-inherits-local-hit policy / sparse-empty-provider-inherits-remote-hit |
| C16.ttl-implies-ramp | A configured TTL with omitted ramp enables the layer fully | configuredTtlImpliesDefaultFullRamp: When both runtime and static ramps are omitted and resolved TTL is positive, independently require a full ramp. runtimeLocalTtlWithoutRampActivatesLayerTest: A configured TTL with omitted ramp enables the layer fully. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. runtimeRemoteTtlWithoutRampActivatesLayerTest: A configured TTL with omitted ramp enables the layer fully. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. runtimeLocalTtlAddsEarlierLayerToRemoteFixtureTest: A runtime local TTL adds a full-ramp local layer to an initially remote-only operation, capturing source publication into both layers; a source completion while a later policy reply is held is retained and served locally without another Redis read. runtimeLocalTtlEnablesSharingWithoutRemoteTtlTest: Runtime local TTL activates local caching and default sharing even when the remote client exists but no remote TTL is configured. | runtime-boundaries / runtime-ttl-implies-ramp:local runtime-boundaries / runtime-ttl-implies-ramp:remote runtime-boundaries/runtimeLocalTtlWithoutRampActivatesLayerTest runtime-boundaries/runtimeRemoteTtlWithoutRampActivatesLayerTest runtime-boundaries/runtimeLocalTtlAddsEarlierLayerToRemoteFixtureTest runtime-boundaries/runtimeLocalTtlEnablesSharingWithoutRemoteTtlTest |
| C17.library-defaults | Request memoization, recovery, and shadow default off; coalescing defaults on | featureLibraryDefaults: When both layers of policy omit each feature, independently require request/recovery/shadow off and coalescing on. omittedPolicyUsesLibraryDefaultsTest: Request memoization, recovery, and shadow default off; coalescing defaults on. This check covers the bounded model clause: omittedPolicyUsesLibraryDefaultsTest. Host representations and other feature combinations retain separate fixed/native evidence. omittedRampAndSharingUseLibraryDefaultsTest: Request memoization, recovery, and shadow default off; coalescing defaults on. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | runtime-boundaries / default-ramp-and-sharing runtime-boundaries/omittedRampAndSharingUseLibraryDefaultsTest |
| C17.disable-keeps-entry | runtime ramp changes preserve existing entries | disablingPolicyDoesNotEvictInsertedEntriesTest: runtime ramp changes preserve existing entries. This check covers the bounded model clause: disablingPolicyDoesNotEvictInsertedEntriesTest. Host representations and other feature combinations retain separate fixed/native evidence. disablingServingKeepsExistingLocalForReenablementTest: runtime ramp changes preserve existing entries. This check covers the bounded model clause: disablingServingKeepsExistingLocalForReenablementTest. Host representations and other feature combinations retain separate fixed/native evidence. | policy / serving-disabled-preserves-existing-local policy/disablingServingKeepsExistingLocalForReenablementTest |
| C18.captured-insertion | pending invocation keeps insertion TTL snapshot | existingLocalEntryKeepsInsertionTtl: An invocation captures its TTL before later overlay changes; the installed local TTL remains the insertion value. policyChangeDuringInvocationTest: An invocation captures its TTL before later overlay changes; the installed local TTL remains the insertion value. | policy / publication-after-policy-change |
| C18.captured-shadow-fill | dark fill preserves accepted runtime TTL and retention after policy changes | darkFillRetainsPolicyThroughSerializationTest: The job captures fresh60s/retention120s. Runtime policy changes to fresh120s/retention180s while its caller source and then serialization are held; dispatched write TTL remains120000ms. At that physical expiry a serving probe under the newer logical policy rejects its source and reports recovery miss, proving the old value was not retained for180s. darkFillCarriesCapturedRetentionOnTheHeldPathTest: A held dark fill dispatches with the retention captured at admission despite a later policy reply. | shadow-layers / dark-fill-policy-snapshot-controls-physical-expiry dark-layers / held-dark-fill-keeps-captured-retention shadow-layers/darkFillRetainsPolicyThroughSerializationTest dark-layers/darkFillCarriesCapturedRetentionOnTheHeldPathTest |
| C18.existing-leader | runtime reenabling joins the registered flight before a newer local hit | sharedSourcesKeepRegistration: Independent completion/failure cannot remove the shared leader registration; a reenabled caller joins that leader before a newer local hit. independentCompletionKeepsRegisteredLeaderTest: Independent completion/failure cannot remove the shared leader registration; a reenabled caller joins that leader before a newer local hit. independentFailureKeepsRegisteredLeaderTest: Independent completion/failure cannot remove the shared leader registration; a reenabled caller joins that leader before a newer local hit. | policy / join-after-policy-change policy/independentCompletionKeepsRegisteredLeaderTest policy/independentFailureKeepsRegisteredLeaderTest |
| C19.memo-bypass | request policy bypass retains memo for later reenabling | falseRequestLeafPreservesMemoForReenablementTest: request policy bypass retains memo for later reenabling. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. bypassedRequestFailureIsAttributedToLocalTest: A call whose reply disables the request layer starts its source inside the cache (its scope is open) but memoizes nothing: its failure is attributed to the shared layers' fallback and both memo rows stay untouched. | scope / memo-after-policy-bypass runtime-boundaries/falseRequestLeafPreservesMemoForReenablementTest scope/bypassedRequestFailureIsAttributedToLocalTest |
| C20.provider-failure | provider failure fails open without caching | providerFailureBypassesAndPreservesExistingLocalTest: provider failure fails open without caching. This check covers the bounded model clause: providerFailureBypassesAndPreservesExistingLocalTest. Host representations and other feature combinations retain separate fixed/native evidence. | policy / provider-failure-preserves-existing-local policy/providerFailureBypassesAndPreservesExistingLocalTest |
| C20.invalid-invocation-policy | invalid runtime remoteReadTimeoutMs bypasses all cache layers | invalidReadBudgetBypassesAllCachingTest: An invalid read budget causes two separate sources and no reads, local storage, or remote publication. | policy / invalid-read-budget-bypasses-caching policy/invalidReadBudgetBypassesAllCachingTest |
| C21.invalid-layer | invalid local TTL leaves valid remote serving available | invalidLocalTtlStillServesFreshRemoteTest: invalid local TTL leaves valid remote serving available. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / invalid-local-ttl-preserves-remote-hit policy/invalidLocalTtlStillServesFreshRemoteTest |
| C21.invalid-recovery | invalid optional staleOnErrorMaxAgeSec preserves fresh remote serving | recoveryAgeEqualToFreshTtlStillServesFreshRemoteTest: invalid optional staleOnErrorMaxAgeSec preserves fresh remote serving. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. negativeRecoveryAgeStillServesFreshRemoteTest: invalid optional staleOnErrorMaxAgeSec preserves fresh remote serving. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / invalid-recovery-retention:23 policy / invalid-recovery-retention:24 policy/recoveryAgeEqualToFreshTtlStillServesFreshRemoteTest policy/negativeRecoveryAgeStillServesFreshRemoteTest |
| C21.invalid-shadow | invalid optional shadow preserves fresh remote serving | invalidShadowPreservesNormalServingTest: Invalid shadow ramp leaves normal source publication and subsequent remote serving available, with no shadow outcome. | policy / invalid-shadow-preserves-serving policy/invalidShadowPreservesNormalServingTest |
| C21.invalid-dark-shadow | invalid optional shadow disables dark reads while retaining local publication | invalidShadowKeepsLocalPublicationTest: Shadow ramp101 disables optional dark work while valid local policy remains active; source success is reusable locally by a later serving-enabled invocation, with zero Redis reads/writes or diagnostic jobs. | shadow-layers / invalid-dark-shadow-preserves-local-source-publication shadow-layers/invalidShadowKeepsLocalPublicationTest |
| C22.freshness-boundary | remote exact fresh TTL expires | lastFreshAgeSkipsSourceTest: Zero-age evidence also closes fresh-side boundary; exact F continues to use independent tests. lastFreshReadDoesNotInvokeSourceTest: remote exact fresh TTL expires exactRemoteFreshBoundaryStartsSourceTest: remote exact fresh TTL expires. This check covers the bounded model clause: exactRemoteFreshBoundaryStartsSourceTest. Host representations and other feature combinations retain separate fixed/native evidence. freshBoundaryIsExclusive: Finite symbolic timestamp and TTL domains independently characterize nonnegative fresh age strictly below the fresh ceiling. remoteHitsRespectAcquiredFreshness: For each policy-profile read receipt, a remote hit requires eligible physically retained storage and nonnegative acquired wall-clock age strictly below the captured fresh TTL. The assertion states the age inequalities independently of the transition helper; it does not cover tracked frame decoding or shadow admission. remoteHitBeforeBoundaryDoesNotRenewFreshnessTest: A public untracked remote read hits at age 500 ms, then the same retained frame misses at exact age 1000 ms without renewal from the first hit. One source refills with a distinct value and a later read reuses it; local caching is disabled. | recovery / fresh-zero-age-skips-source recovery / last-fresh-age-skips-source policy / remote-exact-fresh-boundary-miss policy/exactRemoteFreshBoundaryStartsSourceTest recovery/lastFreshReadDoesNotInvokeSourceTest policy/remoteHitBeforeBoundaryDoesNotRenewFreshnessTest |
| C22.physical-vs-logical | runtime changes preserve in-flight physical TTL and affect later freshness | increasedFreshTtlCanReusePhysicallyRetainedValueTest: runtime changes preserve in-flight physical TTL and affect later freshness. This check covers the bounded model clause: increasedFreshTtlCanReusePhysicallyRetainedValueTest. Host representations and other feature combinations retain separate fixed/native evidence. increasedFreshTtlCannotResurrectExpiredStorageTest: runtime changes preserve in-flight physical TTL and affect later freshness. This check covers the bounded model clause: increasedFreshTtlCannotResurrectExpiredStorageTest. Host representations and other feature combinations retain separate fixed/native evidence. | policy / increased-fresh-ttl-reuses-retained-frame policy / increased-fresh-ttl-cannot-resurrect-expired-storage policy/increasedFreshTtlCanReusePhysicallyRetainedValueTest policy/increasedFreshTtlCannotResurrectExpiredStorageTest |
| C23.library-read-budget | library read deadline precedence | libraryReadBudgetIsFiftyMillisecondsTest: Default read remains pending before 50ms and starts a fresh 10ms source budget at exactly 50ms. | effects / initial-budget:0 effects/libraryReadBudgetIsFiftyMillisecondsTest |
| C23.instance-read-budget | instance read deadline precedence | instanceReadBudgetOverridesLibraryTest: Initial instance read budget20 overrides library50; no source at10, read timeout and full source starts at20, source value survives without refill. | effects / initial-budget:1 effects/instanceReadBudgetOverridesLibraryTest |
| C23.operation-read-budget | operation read deadline precedence | operationReadBudgetOverridesInstanceTest: Initial operation read budget10 overrides instance20; read timeout starts source at10 and source value survives without refill. | effects / initial-budget:2 effects/operationReadBudgetOverridesInstanceTest |
| C23.runtime-read-budget | Runtime read deadline precedence applies to new work; an admitted shadow job retains its captured read budget for confirmation | confirmationKeepsCapturedReadBudgetTest: An admitted job keeps its 5 ms read budget when runtime policy changes to 20 ms before C1 dispatch. That C1 expires at its captured budget; a subsequently admitted job advertises the new 20 ms budget. runtimeReadBudgetOverridesOperationTest: Initial runtime read budget30 overrides operation10 and instance20; no source at20, timeout starts source at30. | shadow-read-deadlines / confirmation-keeps-captured-read-budget effects / initial-budget:3 shadow-read-deadlines/confirmationKeepsCapturedReadBudgetTest effects/runtimeReadBudgetOverridesOperationTest |
| C23.source-start | fallback deadline starts after remote read completes | readTimeoutStartsIndependentSourceDeadlineTest: Two shared callers consume one read timeout, then get the full source budget and no remote refill. | effects / read-timeout-starts-source |
| C23.default-source-budget | library source deadline defaults to sixty seconds | defaultSourceBudgetExpiresAtSixtySecondsTest: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. | source-budgets / default-source-budget-expires-at-sixty-seconds source-budgets/defaultSourceBudgetExpiresAtSixtySecondsTest |
| C24.follower-read | late follower inherits remaining read deadline | followerKeepsAcceptedReadBudgetTest: A later runtime budget change and follower do not replace the leader read's accepted 30ms budget. | effects / follower-keeps-read-budget |
| C24.follower-source | late follower inherits remaining fallback deadline | followersKeepTheirOwnersOutcome: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. lateFollowerUsesLeadersRemainingBudgetTest: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. sourceOwnersMatchContract: Each source-budgets source is owned by the call selected at beginCall or policy release, as reconstructed from the preceding public event rather than source ownership fields. followerKeepsAcquiredOwner: A policy release while a registered source exists maps the released caller to that previously registered owner, preserving the leader execution. | source-budgets / late-follower-keeps-leaders-remaining-source-budget source-budgets/lateFollowerUsesLeadersRemainingBudgetTest |
| C24.independent-reads | uncoalesced remote reads own independent remaining budgets | independentReadDeadlinesStartSeparateSourcesTest: Two uncoalesced reads started 1ms apart expire separately and start separate sources. | independent / independent-read-budgets independent / one-read-times-out-before-another |
| C25.late-source-rejected | late resolve loses to deadline before timer delivery | lateSourceResultIsADeadlineErrorTest: A resolve arriving after its deadline was reached undelivered completes the caller with a deadline error, holds no dump and reports one fallback error with the 10 ms duration. acceptedSourcesSettledBeforeTheirDeadline: A resolve that accepts reports a fallback duration below the source budget: acceptance is strictly before the deadline, one step over the input and the latest event. sourceBoundaryIsExclusive: Finite symbolic elapsed-time/budget domains independently characterize finite acceptance strictly before the deadline and the negative unbounded sentinel; monotonic source ordering is checked by connection records. acceptedSourcesMatchContract: Successful values in the source-budgets profile satisfy the separately captured source owner, start and budget, including the outside-call unbounded sentinel. | effects / late-resolve |
| C25.late-rejection | late reject loses to deadline before timer delivery | lateSourceResultIsADeadlineErrorTest: A source result arriving after its deadline was reached undelivered is a deadline error: DEADLINE_ERROR on the caller, no dump, one fallback error and a 10 ms fallback duration. deadlines::arrival is one arm for a resolve and a reject; the reject side is pinned at the read by lateReadRejectionUsesDeadlineCategoryTest and by the late-reject witness. | effects / late-reject effects/lateSourceResultIsADeadlineErrorTest |
| C25.abandoned-overlap | timeout releases flight while old loader continues | timedOutLoaderOverlapsNewFlightTest: A timeout caller and pending new caller coexist with one abandoned and one registered source. abandonedSourceCannotReplaceSuccessfulRetryTest: First source times out, retry source2 succeeds and publishes, then abandoned source1 settles. Both original timeout and retry result remain unchanged and a later local probe returns2 without a third source. | effects / abandoned-overlap source-budgets / abandoned-source-cannot-replace-successful-retry source-budgets/abandonedSourceCannotReplaceSuccessfulRetryTest |
| C26.unbounded-source | disabled fallback deadline accepts later source settlement | unboundedEnabledSourcePublishesAfterSixtySecondsTest: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. | source-budgets / unbounded-enabled-source-publishes-after-sixty-seconds source-budgets/unboundedEnabledSourcePublishesAfterSixtySecondsTest |
| C26.publication-ownership | accepted serialization and write outlive fallback deadline | acceptedSourcesSettledBeforeTheirDeadline: Every accepted result was settled strictly before its deadline, so a held dump or write always belongs to a source accepted in time; the publication then outlives the deadline. writeRequiresAcceptedSource: Accepted serialization and dispatched write may remain pending beyond source deadline, then return the source value. acceptedWriteOutlivesDeadlineTest: Accepted serialization and dispatched write may remain pending beyond source deadline, then return the source value. | effects / serialize-outlives-deadline effects / publication-after-deadline |
| C26.decode-ownership | fresh decoding is outside the source deadline | acquiredDecodeSurvivesInvalidationAndDeadlineTest: Accepted fresh decode survives later invalidation and elapsed read/source-sized budget without starting source or cancelling the acquired read. | effects / decode-outlives-deadline |
| C27.key-failure | key construction failure runs source with its enabled deadline | onlyEnabledValidCallsResolvePolicy: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. invalidKeyStillKeepsEnabledSourceDeadlineTest: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. | source-budgets / invalid-enabled-key-preserves-source-deadline source-budgets/invalidKeyStillKeepsEnabledSourceDeadlineTest |
| C27.dump-failure | dump failure returns source and does not retain value | dumpFailurePreservesSourceTest: Serialization failure returns source value and dispatches no write. | effects / dump-failure-preserves-value |
| C27.write-failure | write failure returns source and does not retain value | writeFailurePreservesSourceTest: Failed write preserves the source value and does not commit remote storage in this adapter fixture. | effects / write-failure-preserves-value |
| C27.local-read-failure | Failed local reads skip reuse and local publication | failedLocalReadSkipsReuseAndPublication: A local read failure forbids local reuse and publication; local failures are modeled as injected environment health, without a real public fault-injection replay. localReadFailureContinuesToRemoteTest: Failed local reads skip reuse and local publication. This check covers the bounded model clause: localReadFailureContinuesToRemoteTest. Host representations and other feature combinations retain separate fixed/native evidence. localReadFailureSuppressesSourcePublicationTest: Failed local reads skip reuse and local publication. This check covers the bounded model clause: localReadFailureSuppressesSourcePublicationTest. Host representations and other feature combinations retain separate fixed/native evidence. faultedReadNeverUsesLocal: One-step statement over the library records: a call admitted under an armed fault is served from its scope's memo or from the remote frame, or owns a source whose captured local TTL is 0, so no later settlement of that source publishes locally even after the fault clears. The no-warm half of the rule (a faulted remote hit leaves local storage as it was) is a written equivalence pinned by localReadFailureFallsThroughAndPreservesOldLocalTest, not by this invariant. Real local storage remains behind a native exception/clock-failure injection seam; no elapsed-time or concurrent-source claim. localReadFailureFallsThroughAndPreservesOldLocalTest: Real local storage remains behind a native exception/clock-failure injection seam. Distinct request and transient public probes check the old local value, accepted caller result and request-only memo; read failure remains publication-ineligible after the injected fault is cleared. No elapsed-time or concurrent-source claim. localReadFailureSkipsSourcePublicationButMemoizesTest: Real local storage remains behind a native exception/clock-failure injection seam. Distinct request and transient public probes check the old local value, accepted caller result and request-only memo; read failure remains publication-ineligible after the injected fault is cleared. No elapsed-time or concurrent-source claim. | local-failure / failed-local-read-preserves-old-value-and-memoizes-remote local-failure / failed-local-read-suppresses-later-source-publication local-failure/localReadFailureFallsThroughAndPreservesOldLocalTest local-failure/localReadFailureSkipsSourcePublicationButMemoizesTest |
| C27.local-write-failure | A failed local write preserves the accepted source result | failedLocalWritePreservesAcceptedResult: A local write failure preserves the accepted result; local failures are modeled as injected environment health, without a real public fault-injection replay. localWriteFailurePreservesSourceAndMemoTest: A failed local write preserves the accepted source result. This check covers the bounded model clause: localWriteFailurePreservesSourceAndMemoTest. Host representations and other feature combinations retain separate fixed/native evidence. localWriteFailurePreservesRemoteHitTest: A failed local write preserves the accepted source result. This check covers the bounded model clause: localWriteFailurePreservesRemoteHitTest. Host representations and other feature combinations retain separate fixed/native evidence. faultedSettlementPublishesNothingLocally: One-step statement over the library records: the source a settlement names carries no local TTL under an armed fault, so the publication warms nothing while the callers receive the result and the request memo and remote refill proceed. Real local storage remains behind a native exception/clock-failure injection seam; no elapsed-time or concurrent-source claim. callsKeepSourceOutcome: Every owned caller's value is its source's recorded result, so a withdrawn local write never changes an accepted caller result; the surviving request memo and the remote refill are asserted by the regression. Real local storage remains behind a native exception/clock-failure injection seam; no elapsed-time or concurrent-source claim. localWriteFailureKeepsSourceAndRequestMemoTest: Real local storage remains behind a native exception/clock-failure injection seam. Distinct request and transient public probes check the old local value, accepted caller result and request-only memo; read failure remains publication-ineligible after the injected fault is cleared. No elapsed-time or concurrent-source claim. | local-failure / failed-local-write-keeps-result-and-request-memo local-failure/localWriteFailureKeepsSourceAndRequestMemoTest |
| C28.no-refill-after-read-failure | remote read timeout suppresses refill and late read | remoteFailureNeverRefills: Remote read failure prevents refill in the layer presence abstraction. readTimeoutStartsIndependentSourceDeadlineTest: Timeout suppresses refill; a late read accepted only after elapsed budget starts source and cannot be decoded into a hit. lateReadCannotBecomeHitTest: Timeout suppresses refill; a late read accepted only after elapsed budget starts source and cannot be decoded into a hit. failedReadPreservesPreviouslyStoredBytesTest: After a tracked value is stored, an injected read failure returns the changed source without another write; a later healthy read returns the original stored value. This is a read-error example, not a timeout/late-read schedule. | effects / failed-read-no-refill effects / abandoned-read-settles core/failedReadPreservesPreviouslyStoredBytesTest |
| C28.untracked-local-publication | untracked read failure still permits active local publication | remoteReadFailureStillPublishesUntrackedLocalAndRequestTest: untracked read failure still permits active local publication. This check covers the bounded model clause: remoteReadFailureStillPublishesUntrackedLocalAndRequestTest. Host representations and other feature combinations retain separate fixed/native evidence. untrackedReadFailureStillWarmsActiveLocalTest: untracked read failure still permits active local publication. This check covers the bounded model clause: untrackedReadFailureStillWarmsActiveLocalTest. Host representations and other feature combinations retain separate fixed/native evidence. | policy / failed-untracked-read-still-warms-local policy/untrackedReadFailureStillWarmsActiveLocalTest |
| C29.missing-redis-local | missing remote adapter leaves valid local serving available | absentRemoteHasNoAdapterEffects: Missing adapter creates no remote effects; valid local storage is still filled and reused. absentRemotePreservesLocalReuseTest: Missing adapter creates no remote effects; valid local storage is still filled and reused. | layers / absent-remote-preserves-local-reuse layers/absentRemotePreservesLocalReuseTest |
| C29.missing-redis-maintenance | Missing Redis surfaces a maintenance error while local reuse remains valid | absentRemoteMaintenancePreservesLocalReuseTest: Missing-remote maintenance returns its distinct error, invokes no remote adapter, and preserves a later local hit. | layers / absent-remote-maintenance-preserves-local layers/absentRemoteMaintenancePreservesLocalReuseTest |
| C29.maintenance-failure | explicit invalidation surfaces mutation failure | failedInvalidationPreservesExistingMarkerTest: An explicit invalidation failure returns mutation_error while external marker probes preserve absence or prior cutoff and remaining lifetime. failedInvalidationDoesNotCreateMarkerTest: An explicit invalidation failure returns mutation_error while external marker probes preserve absence or prior cutoff and remaining lifetime. | recovery-read / failed-maintenance-preserves-existing-marker recovery-read / failed-maintenance-preserves-absent-marker recovery-read/failedInvalidationPreservesExistingMarkerTest recovery-read/failedInvalidationDoesNotCreateMarkerTest |
| C30.observer-isolation | observer failures cannot change cache or source outcomes | observerFailuresCannotPreventCacheHitTest: Observer callback failure preserves cached value, accepted source publication and original source error. Model abstracts contained callback failure; existing witness conditions need final-public-consequence tightening (reported root). observerFailuresCannotPreventPublicationTest: Observer callback failure preserves cached value, accepted source publication and original source error. Model abstracts contained callback failure; existing witness conditions need final-public-consequence tightening (reported root). observerFailuresCannotReplaceSourceErrorTest: Observer callback failure preserves cached value, accepted source publication and original source error. Model abstracts contained callback failure; existing witness conditions need final-public-consequence tightening (reported root). | effects / observer-failure-hit effects / observer-failure-publication effects / observer-failure-source-error effects/observerFailuresCannotPreventCacheHitTest effects/observerFailuresCannotPreventPublicationTest effects/observerFailuresCannotReplaceSourceErrorTest |
| C31.tracked-no-local-fill | tracked refill suppresses local until a Redis hit warms it | trackedRemoteFallbackSuppressesLocalPublication: Tracked source after semantic remote miss cannot publish to local storage. trackedRefillIsReadAgainBeforeLocalReuseTest: A second public caller after a tracked refill returns the stored value only after a fresh remote read; the completed history observes the read count at that decision. trackedSourceWaitsForValidatedReadToWarmLocalTest: Tracked source leaves local empty; a later validated remote hit warms it and the next local hit avoids remote. trackedSourceNeedsRemoteValidationBeforeLocalReuseTest: Tracked source success memoizes in its request but requires remote read/decode before another scope can warm local; the subsequent transient caller reuses local. | layers / tracked-refill-needs-remote-validation layers / validated-tracked-hit-warms-local recovery-read / tracked-source-requires-validation-before-local-reuse recovery-read/trackedSourceNeedsRemoteValidationBeforeLocalReuseTest layers/trackedSourceWaitsForValidatedReadToWarmLocalTest layers/trackedRefillIsReadAgainBeforeLocalReuseTest |
| C32.grouped-invalidation | one invalidation fences all tracked operation variants only for its entity | invalidationGroupsOperationsButPreservesAcquiredCachesTest: one invalidation fences all tracked operation variants only for its entity. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. invalidationRefillsFromCurrentSourceTest: For one tracked entity/operation, a public invalidation separates a prior cache hit from a refill with the updated source. Multi-operation grouping remains covered by the other case evidence. | layers / invalidation-fences-both-operations layers/invalidationGroupsOperationsButPreservesAcquiredCachesTest core/invalidationRefillsFromCurrentSourceTest |
| C32.untracked-unaffected | untracked Redis values ignore invalidation markers | untrackedReadsIgnoreGroupedInvalidationTest: untracked Redis values ignore invalidation markers. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | layers / untracked-ignores-watermark layers/untrackedReadsIgnoreGroupedInvalidationTest |
| C34.first-fence | observed future fence suppresses serialization and refill | observedFutureFenceSkipsRefillTest: observed future fence suppresses serialization and refill refillAtFenceEqualitySkipsWriteTest: observed future fence suppresses serialization and refill absentReplyWithFutureFenceBlocksRefillTest: An observed future fence carried by a normalized adapter reply suppresses serialization and refill of the accepted source; the following read finds no stored value. Fence equality and invalidation-issued fences keep their tracked-invalidation regressions. | effects / normalized-fence-blocks-publication effects/absentReplyWithFutureFenceBlocksRefillTest |
| C34.second-fence | tracked refill rechecks clock after serialization | rollbackDuringDumpRechecksObservedFenceTest: Rollback during serialization makes the second observed-fence check skip native write while preserving source result. fillFenceIsRejudgedAfterAWallRollbackTest: A wall rollback after serialization starts prevents a held dark write from dispatching below its captured fence. | effects / dump-rechecks-fence-after-rollback dark-layers / held-dark-fill-rechecks-fence-after-rollback dark-layers/fillFenceIsRejudgedAfterAWallRollbackTest |
| C34.write-timestamp | admitted tracked refill timestamps after serialization | writeStampAfterSerializationClearsInterveningFenceTest: Serialization is held across invalidation and a wall-clock advance; native write stamp must clear the intervening watermark, verified by a subsequent public cache hit. | effects / write-stamp-after-serialization effects/writeStampAfterSerializationClearsInterveningFenceTest |
| C35.delayed-old-write | delayed old write is fenced after invalidation | staleValueAfterInvalidationIsFenced: Safety is conditional on the explicit future-buffer, stale-write-delay, and writer-lead bounds in the model. acquiredAfterInvalidationDoesNotServeStale: Safety is conditional on the explicit future-buffer, stale-write-delay, and writer-lead bounds in the model. delayedWriteRemainsFencedTest: A dispatched old write completing after invalidation does not become a readable tracked hit on the next call. acquisitionAfterInvalidationRejectsOldBytesTest: Stale-write guarantee requires documented buffer >= stale work delay + writer clock lead; regression is conditional on those model bounds. staleWriteAtCoveredDelayEqualityRemainsFencedTest: Stale-write guarantee requires documented buffer >= stale work delay + writer clock lead; regression is conditional on those model bounds. freshWriteBeyondBufferBecomesReadableTest: Stale-write guarantee requires documented buffer >= stale work delay + writer clock lead; regression is conditional on those model bounds. | effects / delayed-fenced-write |
| C36.acquired-fresh | acquired tracked snapshot survives later invalidation | acquiredDecodeSurvivesInvalidationAndDeadlineTest: The acquired fresh snapshot survives a later invalidation before asynchronous decode returns. acceptedFreshDecodeSurvivesOtherInvalidationTest: An already acquired snapshot still returns while a later independent call observes invalidation and starts source. acquiredSnapshotSurvivesLaterInvalidationTest: acquired tracked snapshot survives later invalidation | independent / acquired-fresh-decode-survives-invalidation |
| C36.acquired-local | invalidation preserves acquired local value | invalidationGroupsOperationsButPreservesAcquiredCachesTest: A remote watermark change fences later remote reads while earlier local and request values remain reusable. | layers / invalidation-preserves-local-hit layers/invalidationGroupsOperationsButPreservesAcquiredCachesTest |
| C36.acquired-request | invalidation preserves acquired request value | invalidationGroupsOperationsButPreservesAcquiredCachesTest: A remote watermark change fences later remote reads while earlier local and request values remain reusable. | layers / invalidation-preserves-request-hit layers/invalidationGroupsOperationsButPreservesAcquiredCachesTest |
| C37.physical-cap | tracked retention has a one hour physical cap | trackedWritesRespectPhysicalCap: Native write TTL is capped at 3600000ms, and a public read at that physical deadline starts another source even with longer logical freshness. sourcesCarryCappedAdmittedRetention: Every pending source captured either no retention or the maximum admitted before its caller's admission, capped at 3600000ms for a tracked entity: the per-write pairing with the admitted maximum that the profile's write-TTL invariant cannot state once the authority caps it. trackedPhysicalRetentionExpiresAtCapTest: Native write TTL is capped at 3600000ms, and a public read at that physical deadline starts another source even with longer logical freshness. untrackedRetentionIsNotCappedTest: The untracked twin of the cap: a 4 h policy retention is written in full, so the one-hour cap is a tracked-storage rule, not a write ceiling. | recovery-read / tracked-physical-cap-expires-before-logical-freshness recovery-read/trackedPhysicalRetentionExpiresAtCapTest recovery-read/untrackedRetentionIsNotCappedTest |
| C37.logical-age-unclamped | tracked stale retention cap does not clamp logical recovery age | recoveryReturnMatchesAcquiredContract: An externally retained candidate older than the physical cap but younger than the captured logical maximum is served after source failure; no new write is credited. physicalCapDoesNotClampLogicalRecoveryTest: An externally retained candidate older than the physical cap but younger than the captured logical maximum is served after source failure; no new write is credited. | recovery-read / logical-recovery-age-exceeds-physical-cap recovery-read/physicalCapDoesNotClampLogicalRecoveryTest |
| C38.marker-transition | A watermark cutoff never moves backwards | rollbackCannotLowerInvalidationWatermarkTest: A second invalidation after wall rollback does not lower the existing watermark; exact Redis retention remains vector/integration evidence. successfulCutoffIsExactMaximum: Successful invalidation keeps the larger prior valid cutoff or newly proposed buffered cutoff; selected prior future markers are verified on real servers. futureCutoffDoesNotMoveBackwardsTest: Successful invalidation keeps the larger prior valid cutoff or newly proposed buffered cutoff; selected prior future markers are verified on real servers. | recovery/rollbackCannotLowerInvalidationWatermarkTest invalidation/existing future cutoff never moves backwards |
| C39.reject-before-mutation | Invalid watermark arguments reject before mutation | argumentValidationIsExact: All15 selected invalid raw argument forms preserve all12 complete input Redis states. Absence, malformed and valid strings, ordered list content, finite TTL and persistence are asserted; no repair occurs after invalid input. rejectedInputPreservesEntireRedisState: All15 selected invalid raw argument forms preserve all12 complete input Redis states. Absence, malformed and valid strings, ordered list content, finite TTL and persistence are asserted; no repair occurs after invalid input. rejectedFractionPreservesOrderedListTest: All15 selected invalid raw argument forms preserve all12 complete input Redis states. Absence, malformed and valid strings, ordered list content, finite TTL and persistence are asserted; no repair occurs after invalid input. rejectedUnsafeSumPreservesPersistentMalformedTextTest: All15 selected invalid raw argument forms preserve all12 complete input Redis states. Absence, malformed and valid strings, ordered list content, finite TTL and persistence are asserted; no repair occurs after invalid input. newlineAndPlusAreNotDecimalGrammarTest: All15 selected invalid raw argument forms preserve all12 complete input Redis states. Absence, malformed and valid strings, ordered list content, finite TTL and persistence are asserted; no repair occurs after invalid input. | invalidation/negative buffer rejects before mutation invalidation/fractional buffer rejects before mutation invalidation/over-limit buffer rejects before mutation invalidation/exponent timestamp rejects before mutation invalidation/negative timestamp rejects before mutation invalidation/unsafe sum rejects before mutation invalidation/negative buffer preserves absent state invalidation/negative buffer preserves malformed finite string invalidation/negative buffer preserves malformed persistent string invalidation/negative buffer preserves finite list contents invalidation/negative buffer preserves persistent list contents invalidation/fractional buffer preserves absent state invalidation/fractional buffer preserves malformed finite string invalidation/fractional buffer preserves malformed persistent string invalidation/fractional buffer preserves finite list contents invalidation/fractional buffer preserves persistent list contents invalidation/over-limit buffer preserves absent state invalidation/over-limit buffer preserves malformed finite string invalidation/over-limit buffer preserves malformed persistent string invalidation/over-limit buffer preserves finite list contents invalidation/over-limit buffer preserves persistent list contents invalidation/exponent timestamp preserves absent state invalidation/exponent timestamp preserves malformed finite string invalidation/exponent timestamp preserves malformed persistent string invalidation/exponent timestamp preserves finite list contents invalidation/exponent timestamp preserves persistent list contents invalidation/negative timestamp preserves absent state invalidation/negative timestamp preserves malformed finite string invalidation/negative timestamp preserves malformed persistent string invalidation/negative timestamp preserves finite list contents invalidation/negative timestamp preserves persistent list contents invalidation/unsafe sum preserves absent state invalidation/unsafe sum preserves malformed finite string invalidation/unsafe sum preserves malformed persistent string invalidation/unsafe sum preserves finite list contents invalidation/unsafe sum preserves persistent list contents |
| C40.first-stale | first stale age is recoverable without shared publication | recoveredStaleHasNoSharedPublication: At exact fresh boundary F=2, authorized failure returns stale with no remote/local/shadow publication; later age does not revoke the returned value. servedValueCanAgeTest: At exact fresh boundary F=2, authorized failure returns stale with no remote/local/shadow publication; later age does not revoke the returned value. firstStaleAgeRetainsWithoutDecodingTest: first stale age is recoverable without shared publication retentionStartsAtFreshBoundary: Finite symbolic domains independently characterize initial stale retention as fresh ceiling <= age < maximum; frame/fence validity remains a profile responsibility. | recovery / first-stale-age-recovers-without-publication |
| C40.last-stale | last millisecond before M is recoverable | lastRecoveryMillisecondIsServedTest: last millisecond before M is recoverable lastRecoveryAgeStillServesTest: last millisecond before M is recoverable | recovery / last-recovery-age-serves recovery/lastRecoveryMillisecondIsServedTest |
| C40.maximum-age | maximum age is not retained for recovery | retainedCandidateWasEligible: Every retained candidate has initial age strictly below M; therefore age exactly M cannot be retained. maximumAgeAtReadDoesNotDecodeTest: maximum age is not retained for recovery exactMaximumAgeDoesNotRetainTest: maximum age is not retained for recovery initiallyTooOldCannotRecoverAfterRollbackTest: Initial rejected bytes stay unavailable after the clock makes their age eligible before authorized source failure. The final error, no decode, and single initial read distinguish initial retention from failure-time age checking alone. | recovery / maximum-age-read-preserves-source-error recovery/maximumAgeAtReadDoesNotDecodeTest |
| C40.future-rejected | future age is not retained for recovery | retainedCandidateWasEligible: Retained candidates have nonnegative stale age; a directly seeded future frame takes a plain miss without retention. futureFrameIsNotRetainedTest: Retained candidates have nonnegative stale age; a directly seeded future frame takes a plain miss without retention. initiallyFutureCannotRecoverAfterClockAdvanceTest: Initial rejected bytes stay unavailable after the clock makes their age eligible before authorized source failure. The final error, no decode, and single initial read distinguish initial retention from failure-time age checking alone. futureFrameIsNeverFreshOrRetained: Receipt of the initial read: the frame stamp and the observing clock are recorded at the read, and a frame stamped after that clock is classified neither fresh nor retained, with the inequality restated on the recorded pair. The model keeps no future check of its own on this path, so the receipt is what catches a shared age rule that stops rejecting future stamps. | recovery / future-read-preserves-source-error |
| C41.success-skips-decode | source success skips retained candidate decoding | sourceSuccessDoesNotDecodeCandidate: Source success precludes any candidate decoding. acceptedSourceNeverDecodesRetainedBytesTest: source success skips retained candidate decoding | recovery / source-success-skips-stale-decode |
| C41.denial-keeps-error | denied recovery preserves source error without decoding | operationDenialReplacesInstanceAllowTest: An operation denial over instance allow preserves ordinary source error and does not start candidate decode. deniedRecoveryNeverDecodesRetainedBytesTest: denied recovery preserves source error without decoding | recovery / operation-denial-overrides-instance-allow recovery/operationDenialReplacesInstanceAllowTest |
| C41.classifier-failure | recovery error overrides allow policy safely | classifierErrorPreservesSourceWithoutDecodeTest: A failing recovery classifier preserves the source error without decoding retained bytes or publishing them. | recovery / classifier-error-keeps-error-without-decode recovery/classifierErrorPreservesSourceWithoutDecodeTest |
| C42.allow-override | recovery allow overrides deny policy safely | operationAllowReplacesInstanceDenialTest: An operation allow classifier overrides instance denial for an ordinary source error and produces one successful retained recovery. | recovery / operation-allow-overrides-instance-denial recovery/operationAllowReplacesInstanceDenialTest |
| C42.timeout-only-default | default classifier rejects ordinary errors | defaultRejectsOrdinaryFailureTest: The inherited timeout-only classifier preserves ordinary source error without custom classification or decode. | recovery / default-denies-ordinary-error recovery/defaultRejectsOrdinaryFailureTest |
| C42.propagated-timeout | default classifier accepts a timeout propagated by source | defaultRecoversPropagatedTimeoutTest: A timeout error propagated by source is recovered by the default classifier without invoking a custom classifier. | recovery / default-recovers-propagated-timeout recovery/defaultRecoversPropagatedTimeoutTest |
| C42.explicit-denial | explicit denial replaces default timeout recovery | explicitDenialReplacesDefaultTest: Explicit operation or instance denial preserves timeout and avoids decode. instanceDenialReplacesTimeoutOnlyDefaultTest: Explicit operation or instance denial preserves timeout and avoids decode. | recovery / explicit-denial-overrides-timeout recovery/explicitDenialReplacesDefaultTest recovery/instanceDenialReplacesTimeoutOnlyDefaultTest |
| C43.coalesced-once | coalesced recovery classifies and decodes once | coalescedRecoveryClassifiesAndDecodesOnceTest: Three callers across two request scopes share one read, source, classifier decision and decode; all receive the recovered value with one served diagnostic and no remote write. | recovery / coalesced-recovery recovery/coalescedRecoveryClassifiesAndDecodesOnceTest |
| C43.request-memo | recovered value memoizes only in its request scope | closedScopesHaveNoMemo: Recovered value is reusable only in attached live request scope; closure prevents late memo publication. recoveredValueMemoizesOnlyInAttachedRequestTest: Recovered value is reusable only in attached live request scope; closure prevents late memo publication. closedRequestCannotReceiveLateRecoveryMemoTest: Recovered value is reusable only in attached live request scope; closure prevents late memo publication. recoveredStaleHasNoSharedPublication: Recovered stale results do not publish into shared local or remote caches or schedule shadow work. recoveredResultsNeverPublishShared: A same-scope public probe reuses recovered value; another scope performs remote work, distinguishing request memo from local publication. compressedRecoveryMemoizesWithoutLocalPublicationTest: A same-scope public probe reuses recovered value; another scope performs remote work, distinguishing request memo from local publication. closingAnotherScopeKeepsThisScopesMemoTest: A memo row belongs to its scope: closing another scope leaves this scope's memoized value, which a same-scope caller reuses without a read; the request-only publication of a recovered value rests on rows being per scope. recoveredFlightCompletesEveryOwner: After a served recovery decode, every caller the flight owned that was pending receives the value its retained candidate decodes to and every other caller keeps its outcome. This establishes shared caller results; request-memo publication remains covered by the case's other evidence. recoveredFlightMemoIsReusedByBothRequestsTest: Two request scopes sharing recovery each reuse the recovered result in a subsequent public call, with one read/source/decode and no shared writes. | recovery / recovered-value-request-hit recovery / recovery-memoizes-both-requests recovery-read / tracked-compressed-recovery-is-request-only recovery-read/compressedRecoveryMemoizesWithoutLocalPublicationTest recovery-read/closingAnotherScopeKeepsThisScopesMemoTest recovery/recoveredValueMemoizesOnlyInAttachedRequestTest recovery/closedRequestCannotReceiveLateRecoveryMemoTest recovery/recoveredFlightMemoIsReusedByBothRequestsTest |
| C43.independent-values | uncoalesced recovery preserves each caller's independently acquired bytes | independentRecoveryKeepsDistinctSnapshotsTest: Two independent callers retain different values and return those exact values despite invalidation and reverse decode completion. independentRecoveriesServeDistinctAcquiredSnapshotsTest: Two uncoalesced callers acquire different stale frames before their sources fail; after invalidation each recovery serves the bytes its own read retained, with two reads, two sources, two decodes and no writes. | independent / distinct-retained-recovery-values independent / independent-source-error-identities independent/independentRecoveriesServeDistinctAcquiredSnapshotsTest |
| C44.retained-invalidation | recovery uses acquired snapshot after invalidation and replacement | independentRecoveryKeepsDistinctSnapshotsTest: Retained acquired bytes survive replacement for another caller and later invalidation; each caller still returns its own snapshot. replacementDoesNotChangeRetainedRecoveryTest: recovery uses acquired snapshot after invalidation and replacement retainedBytesSurviveRedisDeletionAndFenceTest: recovery uses acquired snapshot after invalidation and replacement retainedCompressedRecoverySurvivesInvalidationTest: A candidate acquired before invalidation recovers and memoizes in its request, while a new request must observe the fence and preserve its different source error. retainedSnapshotMatchesAcquisition: The recovery-read profile captures maximum age from pre-admission policy, then projects read settlement into a retained owner, modeled payload identity and timestamp. Accepted policy and later retained candidates must match those independent records. Raw/compressed encoding identity is abstracted. retainedSnapshotMatchesAcquisition: At a step that dispatches a read in the recovery profile, the new flight's retained snapshot carries the pre-step frame's stamp, its code or none, and the pre-step policy's retention as its maximum; later invalidation and replacement leave the snapshot alone. | recovery / retained-across-invalidation recovery / replacement-cannot-change-recovered-value recovery-read / retained-compressed-recovery-survives-fence-new-request-misses recovery-read/retainedCompressedRecoverySurvivesInvalidationTest recovery/replacementDoesNotChangeRetainedRecoveryTest |
| C44.retained-expiry | expired remote storage cannot revoke retained stale snapshot | retainedSnapshotSurvivesPhysicalExpiryTest: A call retains otherwise eligible bytes before their physical expiration; its recovery succeeds afterward, while a new request observes absence and preserves its own source error. | recovery-read / retained-snapshot-survives-physical-expiry-new-read-misses recovery-read/retainedSnapshotSurvivesPhysicalExpiryTest |
| C44.no-reread | read failure never causes a recovery reread | recoveryUsesSingleRedisRead: One initial read at most; failed read retains no candidate, never begins recovery, and preserves source rejection. readFailureNeverRetains: One initial read at most; failed read retains no candidate, never begins recovery, and preserves source rejection. readFailureNeverAttemptsRecovery: One initial read at most; failed read retains no candidate, never begins recovery, and preserves source rejection. failedReadSkipsRecoveryTest: One initial read at most; failed read retains no candidate, never begins recovery, and preserves source rejection. initialReadFailureSkipsRecoveryClassificationTest: read failure never causes a recovery reread | recovery / failed-initial-read-skips-recovery recovery/initialReadFailureSkipsRecoveryClassificationTest |
| C45.maximum-age-exclusive | After asynchronous decoding, age exactly M preserves the source error | servedStaleIsStrictlyWithinMaxAge: Return-event age must be < M and nonnegative; crossing to exact M during decode preserves source rejection and writes no request memo. decodingAtMaxAgeRejectsTest: Return-event age must be < M and nonnegative; crossing to exact M during decode preserves source rejection and writes no request memo. maximumAgeAfterDecodePreservesSourceTest: Distinguish equality after decode from greater-than-M; do not count the same fixed scenario twice as independent evidence. recoveredValueWasWithinAcceptedAge: At the settlement that serves a recovered value, the recovery connection model checks the retained snapshot's stamp against the pre-step wall clock: nonnegative age, strictly below the captured maximum. One-step restatement of the former profile receipt. recoveryBoundaryIsExclusive: Finite symbolic domains independently characterize recovery age as nonnegative and strictly below the acquired maximum, including equality rejection. | recovery / exact-maximum-after-decode-rejects recovery/maximumAgeAfterDecodePreservesSourceTest |
| C45.recheck-after-decode | stale candidate crossing M during decoding preserves source error | servedStaleIsStrictlyWithinMaxAge: Return-event age must be < M and nonnegative; crossing to exact M during decode preserves source rejection and writes no request memo. decodingAtMaxAgeRejectsTest: Return-event age must be < M and nonnegative; crossing to exact M during decode preserves source rejection and writes no request memo. | recovery / expired-during-decode |
| C45.captured-policy | pending recovery keeps its age snapshot while later calls use new policy | recoveryPolicyIsCapturedPerCallerTest: Two acquired candidates retain their own max-age snapshots; after decode delay the older policy serves while the newer shorter policy preserves that caller's source error. recoveryReturnMatchesAcquiredContract: A served recovery result after releaseLoad must match the acquired snapshot owner and modeled payload and satisfy its captured maximum at the pre-settlement wall clock. Single-active-call profile. independentRecoveryMatchesContract: A served independent recovery decode returns the selected caller snapshot payload under its captured maximum and current wall clock, including reversed completion schedules. independentRecoveryAtCapturedAgeBoundaryTest: The shorter captured policy rejects at its exact maximum age while a longer-policy decode remains pending; subsequent decode serves only the longer-policy caller and neither recovery writes shared state. | independent / independent-recovery-age-boundary independent/independentRecoveryAtCapturedAgeBoundaryTest |
| C45.preserve-source-error | recovery deserialization failure preserves original error | failedRecoveryPreservesDeadlineErrorTest: Recovery load failure preserves the original deadline result and emits deserialization_error. recoveryDecodeFailureKeepsSourceOutcomeTest: Verification outcome enum checks source-vs-recovery error category; portable fixed driver/native errors carry exact original identity. | independent / failed-recovery-keeps-source-error recovery/failedRecoveryPreservesDeadlineErrorTest |
| C45.rollback-future | wall rollback during recovery decode rejects a now future snapshot | rollbackDuringRetainedDecodeRejectsFutureSnapshotTest: Wall rollback during decode makes the retained snapshot future and preserves the original deadline with recovery miss/no age sample. rollbackToFutureCandidateRejectsTest: wall rollback during recovery decode rejects a now future snapshot | recovery / rollback-rejects-retained-future recovery/rollbackDuringRetainedDecodeRejectsFutureSnapshotTest |
| C45.failed-fresh-not-stale | failed fresh deserialization is never retried as stale recovery | freshDecodeFailureCannotBeRetriedAsRecoveryTest: failed fresh deserialization is never retried as stale recovery | recovery / failed-fresh-decode-is-not-recovery recovery/freshDecodeFailureCannotBeRetriedAsRecoveryTest |
| C46.ignore-late-source | default timeout recovery ignores late successful loader | lateSuccessCannotReplaceRecoveredValueTest: Late successful source cannot replace timeout recovery or create dump/write effects. | recovery / recovery-abandoned-overlap recovery / recovery-late-source-settles recovery/lateSuccessCannotReplaceRecoveredValueTest |
| C47.requires-hook | shadow requires an outcome observer | missingHookHasNoShadowEffects: Without the outcome hook no dark cache/read/load/write machinery runs; caller still returns its source value. missingHookSkipsDarkJobTest: Without the outcome hook no dark cache/read/load/write machinery runs; caller still returns its source value. | shadow / missing-hook-skips-job |
| C47.requires-capacity | shadow global capacity drops another key instead of queueing | capacityIsPerInstance: Per-instance capacity bounds admitted jobs; a full instance drops its next key while another instance can admit. fullInstanceDoesNotBlockOtherInstanceTest: Per-instance capacity bounds admitted jobs; a full instance drops its next key while another instance can admit. deduplicatedJobKeepsIndependentCallerSourcesTest: A dark job dropped for a live job of its identity leaves the caller's own source to complete with its value: a drop never queues and never touches the caller. servedAndDarkJobsShareCapacityButNotSourceOwnershipTest: A served-hit job and dark job jointly fill two per-instance slots, so another key is dropped while its independent caller source still runs. At60000ms the dark-source wait releases its slot, but a timed-out served raw source still consumes the other. A distinct-key probe is dropped until that raw source settles, after which another probe admits. Late settlements do not replace served hits or fill expired jobs. fullInstanceDropsAnotherKeyWhileTheC0ReadIsHeldTest: A held C0 read keeps its instance slot occupied: another key is dropped there while the same key on another instance is admitted. | admission / full-capacity-drop shadow-layers / mixed-shadow-capacity-retains-only-owned-source dark-layers / held-dark-capacity-is-instance-local shadow-layers/servedAndDarkJobsShareCapacityButNotSourceOwnershipTest admission/fullInstanceDoesNotBlockOtherInstanceTest dark-layers/fullInstanceDropsAnotherKeyWhileTheC0ReadIsHeldTest |
| C47.requires-cohort | shadow cohort excludes equality and admits just above its exact sample | shadowCohortBelowDoesNotAdmitTest: For the tracked key{urn🆔0}#ShadowLayers and independent shadow FNV numerator3203834406, thresholds exactly one uint32unit below/equal/above the sample produce no-read/no-job below/equal and an actual C0 read/fill serialization above. Caller success remains independent of diagnostic admission. shadowCohortEqualityDoesNotAdmitTest: For the tracked key{urn🆔0}#ShadowLayers and independent shadow FNV numerator3203834406, thresholds exactly one uint32unit below/equal/above the sample produce no-read/no-job below/equal and an actual C0 read/fill serialization above. Caller success remains independent of diagnostic admission. shadowCohortAboveAdmitsTest: For the tracked key{urn🆔0}#ShadowLayers and independent shadow FNV numerator3203834406, thresholds exactly one uint32unit below/equal/above the sample produce no-read/no-job below/equal and an actual C0 read/fill serialization above. Caller success remains independent of diagnostic admission. | shadow-layers / shadow-cohort-below-does-not-admit shadow-layers / shadow-cohort-equality-does-not-admit shadow-layers / shadow-cohort-above-admits shadow-layers/shadowCohortBelowDoesNotAdmitTest shadow-layers/shadowCohortEqualityDoesNotAdmitTest shadow-layers/shadowCohortAboveAdmitsTest |
| C48.source-disabled | shadow source observes disabled caching scope | jobsAreDiagnostic: Served-hit detached shadow sources observe disabled caching; all their outcomes remain diagnostic with no dump/write effects in this profile. | admission / coalesced-hit-one-job |
| C48.ordinary-miss | ordinary remote miss does not schedule shadow source | ordinaryServingMissDoesNotAdmitDiagnosticSourceTest: A serving-enabled remote miss with shadow100 starts exactly one enabled caller source; source success fills normally and a later no-shadow serving probe returns that value. No disabled diagnostic source or shadow verdict occurs. | shadow-layers / ordinary-serving-miss-has-no-diagnostic-source shadow-layers/ordinaryServingMissDoesNotAdmitDiagnosticSourceTest |
| C49.dark-source-reuse | ramped down shadow fills from the same caller source | fillsRequireMissAndAcceptedSource: Every held dump or write belongs to a job whose C0 found nothing and whose source was accepted: ramped-down dark work fills from the caller's own source, never a detached one, and only after that source settled. darkReadBeforeSourceWaitsForItTest: A dark C0 miss released before the source holds no dump and reports nothing until the source resolves; the fill then follows from the accepted caller result. | shadow / outcome:filled shadow/darkReadBeforeSourceWaitsForItTest |
| C49.dark-no-delay | dark read does not delay caller source result | sourceWorkBeforeDeadlineStillReadsTest: The source resolves while the dark C0 read is still held: the caller completes with its value at once and the job's read stays pending. darkReadBeforeSourceWaitsForItTest: The dark C0 read settles before the source: the caller stays pending until its own source resolves, then completes with that value. | shadow / source-before-c0 |
| C50.custom-equal | shadow comparator equal outcome is diagnostic | explicitEqualityOverridesValuesTest: Explicit equal comparator overrides unequal values and yields one match and age sample. | shadow / custom-equal-overrides-values |
| C50.custom-unequal | shadow comparator unequal outcome is diagnostic | explicitInequalityRequiresConfirmationTest: Explicit unequal comparator overrides equal values, requires C1 confirmation, and only then yields mismatch/warning. | shadow / custom-unequal-confirms-equal-values |
| C50.comparator-error | shadow comparator error outcome is diagnostic | comparisonFailureKeepsCallerTest: Comparator error emits comparison_error without changing already acquired caller result or recording age. | shadow / outcome:comparison_error |
| C51.changed-confirmation | served hit shadow superseded remains diagnostic | identicalTextAndBinaryBytesConfirmMismatchTest: A mismatch requires exactly one C1 read returning the C0 bytes; changed or absent C1 bytes are a supersession. The superseded outcome itself is defined by the confirmation judgment. sameDecodedValueWithDifferentBytesIsSupersededTest: The common confirmation rule is checked on the dark generated profile and on served-hit fixed scenarios; this witness does not establish source detachment. darkC0ReplacedBeforeConfirmationIsSupersededTest: In the composed shadow-layers profile a dark job's fresh C0 (value 1) differs from its source (value 2) and the frame was replaced (value 2) before the confirmation read, so the second read finds other bytes and the job ends superseded: one decode, two reads, no dump, the caller completing with its source value. A dark job, not a served hit; no repair claim. | shadow / different-c1-bytes-supersede shadow-layers/darkC0ReplacedBeforeConfirmationIsSupersededTest |
| C51.confirmation-age | shadow confirmation compares payload bytes after C0 freshness expires | confirmationPastFreshnessKeepsOriginalPayloadAndAgeTest: C0=1 is acquired fresh and retained; source2 compares unequal and C1 is held. Advancing application time exactly60000ms crosses F while elapsed job time and physical retention stay unchanged. C1 matching bytes confirm mismatch with read count2, no repair, source caller2 preserved and age60000ms. retainedC0AgeIsSampledAtTheVerdictTest: A C0 acquired one millisecond inside freshness remains the comparison snapshot, and its confirmed mismatch reports the age at the later verdict. | shadow / shadow-confirmation-past-freshness-preserves-payload-and-age dark-layers / held-dark-c0-age-at-verdict shadow/confirmationPastFreshnessKeepsOriginalPayloadAndAgeTest dark-layers/retainedC0AgeIsSampledAtTheVerdictTest |
| C51.confirmation-rollback | shadow confirmation preserves payload comparison across wall clock rollback | confirmationRollbackKeepsPayloadAndClampsAgeTest: After fresh C0/source inequality starts C1, application time rolls backward1000ms. The now-future C1 still confirms identical payload bytes, preserves source caller2, writes nothing and emits mismatch with age clamped0 and remote_shadow future offset1000ms. | shadow / shadow-confirmation-rollback-keeps-payload-and-reports-offset shadow/confirmationRollbackKeepsPayloadAndClampsAgeTest |
| C51.payload-representation | Identical UTF-8 bytes confirm across text and binary representations | identicalTextAndBinaryBytesConfirmMismatchTest: Text and binary C0/C1 representations with identical UTF-8 bytes confirm mismatch; the byte identity is a finite fixture encoding. | shadow / text-to-binary-confirmation shadow / binary-to-text-confirmation |
| C51.bytes-not-decoded-value | Different payload bytes supersede even if they decode to the same value | sameDecodedValueWithDifferentBytesIsSupersededTest: Padding changes C1 bytes even when decoded value is equal, so the model produces superseded. | shadow / different-bytes-same-value-superseded |
| C52.present-not-repaired | ramped down present C0 is diagnosed without repair | fillsRequireMissAndAcceptedSource: Every held dump or write belongs to a job whose C0 found nothing: a present C0 is never repaired, whatever the comparison verdict. darkPresentC0NeverBecomesLocalPublicationTest: Fresh present C0=1 and caller source=2 produce a confirmed mismatch with one C1 read and zero Redis writes. Local publication of2 belongs only to the caller source; diagnostic work never repairs the present C0. | shadow-layers / dark-present-c0-never-publishes-local shadow-layers/darkPresentC0NeverBecomesLocalPublicationTest |
| C52.undecodable-not-repaired | dark present undecodable value is never repaired | fillsRequireMissAndAcceptedSource: Every held dump or write belongs to a job whose C0 found nothing: a present C0 whose decode fails ends deserialization_error with no fill. undecodableDarkC0IsNeverRepairedTest: A held decode failure for a present dark C0 ends the job without serializing a replacement or changing the source result. | shadow / outcome:deserialization_error shadow / present-undecodable-c0-is-not-repaired dark-layers / undecodable-held-dark-c0-is-not-repaired dark-layers/undecodableDarkC0IsNeverRepairedTest |
| C53.fill-fenced | ramped down shadow fill respects observed fence | fillsClearTheirFence: A held write was stamped after the fence its job's C0 read observed: the fence recheck at dump release (remote_writes::dispatch) is judged one step later, so a fenced fill outcome has no write. fenceRejudgedAtDumpReleaseAfterRollbackTest: The fence a miss observed is judged again when the dump is released: a wall rollback below it between settlement and release ends the job fill_fenced with no write, the caller keeping its value. fillAtTheWatermarkInstantIsFencedTest: A dark fill at the acquired watermark instant returns the source result without starting serialization. | shadow / outcome:fill_fenced dark-layers / dark-fill-at-watermark-is-fenced shadow/fenceRejudgedAtDumpReleaseAfterRollbackTest dark-layers/fillAtTheWatermarkInstantIsFencedTest |
| C53.confirmation-fails-open | shadow confirmation failure does not repair cache | fillsRequireMissAndAcceptedSource: A confirmation read fails only for a job whose C0 was present, and every held fill belongs to a job whose C0 found nothing, so a confirmation failure never initiates a repair; caller preservation is separately replayed. | shadow / outcome:confirmation_error |
| C54.deduplication | shadow admission drops duplicate work | oneJobPerIdentity: At most one live job per identity; another same-key eligible hit drops even when capacity is not full. duplicateDropsBeforeCapacityIsFullTest: At most one live job per identity; another same-key eligible hit drops even when capacity is not full. deduplicatedJobKeepsIndependentCallerSourcesTest: Same-key dark calls with coalesce=false create two independently controlled sources but one C0 read/job. The second settles to 2 without a fill; the owner settles to 1, fills once, and a later serving probe returns 1 while each caller retains its own result. | admission / duplicate-with-free-capacity shadow-layers / dark-job-dedup-preserves-independent-source-values shadow-layers/deduplicatedJobKeepsIndependentCallerSourcesTest admission/duplicateDropsBeforeCapacityIsFullTest |
| C54.source-ownership | shadow timeout retains capacity until external source settles | timeoutRetainsSourceCapacityTest: Job timeout keeps raw source capacity live until source settlement, which releases it without changing caller or emitting another outcome. servedAndDarkJobsShareCapacityButNotSourceOwnershipTest: A served-hit job and dark job jointly fill two per-instance slots, so another key is dropped while its independent caller source still runs. At60000ms the dark-source wait releases its slot, but a timed-out served raw source still consumes the other. A distinct-key probe is dropped until that raw source settles, after which another probe admits. Late settlements do not replace served hits or fill expired jobs. | admission / source-timeout-keeps-slot shadow-layers / mixed-shadow-capacity-retains-only-owned-source shadow-layers/servedAndDarkJobsShareCapacityButNotSourceOwnershipTest admission/timeoutRetainsSourceCapacityTest |
| C54.decode-ownership | shadow decode retains capacity after timeout until raw load settles | timedOutDarkDecodeKeepsCapacityUntilRawReleaseTest: A dark decode retains capacity across the whole-job timeout, starts no late confirmation, and permits admission after raw release. timeoutRetainsDecodeCapacityTest: Job timeout keeps raw decode capacity live until load settlement; no later confirmation is started. lateDecodeCannotStartConfirmationTest: This witness proves late-effect suppression; existing admission decode-timeout-keeps-slot proves capacity ownership. | dark-layers / timed-out-dark-decode-retains-capacity-until-raw-release admission / decode-timeout-keeps-slot shadow / late-shadow-decode-cannot-start-c1 dark-layers/timedOutDarkDecodeKeepsCapacityUntilRawReleaseTest admission/timeoutRetainsDecodeCapacityTest |
| C54.read-ownership | shadow confirmation read retains capacity after its separate read deadline | jobDeadlineThenReadDeadlineReportsOneVerdictTest: A 10 ms whole-job deadline reports timeout while a 20 ms read remains live; the later read deadline requests cancellation without a second verdict, and raw ownership persists until release. c1ReadDeadlineKeepsRawCapacityTest: A separately bounded C1 read reports confirmation_error and requests cancellation at 5 ms; its raw read still rejects a competing key until released. The caller keeps its value and a later key is admitted without any second verdict. lateConfirmationCannotEmitAnotherVerdictTest: This older witness isolates late-effect suppression after the job deadline; shadow-read-deadlines separately proves the read deadline and raw-capacity boundary. | shadow-read-deadlines / job-then-read-timeout-has-one-verdict shadow-read-deadlines / c1-read-timeout-retains-raw-capacity shadow / late-c1-cannot-emit-second-verdict shadow-read-deadlines/jobDeadlineThenReadDeadlineReportsOneVerdictTest shadow-read-deadlines/c1ReadDeadlineKeepsRawCapacityTest |
| C54.comparison-budget | Comparison work can exhaust the job deadline before confirmation | slowComparisonTimesOutBeforeConfirmationTest: Successful or failing comparator work reaching the job budget produces timeout before any confirmation read; caller result remains unchanged. slowComparisonFailureStillTimesOutTest: Successful or failing comparator work reaching the job budget produces timeout before any confirmation read; caller result remains unchanged. | shadow / comparison-crosses-deadline:9 shadow / comparison-crosses-deadline:10 |
| C54.expired-before-start | A dark job already expired before deferred work starts must issue no Redis read | expiredSourceWorkSkipsRedis: At 9ms source work, deferred read can start and source settlement can succeed; at exactly 10ms, no Redis read starts and late success/rejection gives the source deadline. These fixtures observe later timer progress only in complete 10ms windows. sourceWorkBeforeDeadlineStillReadsTest: At 9ms source work, deferred read can start and source settlement can succeed; at exactly 10ms, no Redis read starts and late success/rejection gives the source deadline. These fixtures observe later timer progress only in complete 10ms windows. sourceWorkAtDeadlineSkipsDeferredReadTest: At 9ms source work, deferred read can start and source settlement can succeed; at exactly 10ms, no Redis read starts and late success/rejection gives the source deadline. These fixtures observe later timer progress only in complete 10ms windows. expiredDeferredJobRetainsSourceRejectionDeadlineTest: At 9ms source work, deferred read can start and source settlement can succeed; at exactly 10ms, no Redis read starts and late success/rejection gives the source deadline. These fixtures observe later timer progress only in complete 10ms windows. | shadow / source-work-before-deadline-dispatches-read shadow / source-work-exhausts-deferred-job shadow / expired-job-source-resolve-keeps-deadline shadow / expired-job-source-reject-keeps-deadline |
| C55.miss-discriminator | adapter miss with stray frame fields preserves only trustworthy miss metadata | missDiscriminatorWinsOverFrameFieldsTest: A miss discriminator wins over stray frame fields and starts source without decode; other metadata trust rules remain the adapterReply/releaseRead transition. | effects / reply:14 |
| C55.unknown-reason | adapter unknown reason with valid fence preserves only trustworthy miss metadata | unknownReasonKeepsValidFenceTest: Unknown reason is normalized to unclassified while a valid future fence still suppresses serialization. | effects / reply:7 |
| C55.ignore-untracked-fence | adapter untracked fence preserves only trustworthy miss metadata | untrackedReplyCannotCarryFenceTest: Untracked reply strips observed fence and normalizes reason, allowing serialization. untrackedFencedReplyRefillsAndIsReadableTest: An untracked watermark-fenced reply is normalized to an unclassified miss with zero fence; one source refill is subsequently readable without a second source. | effects / untracked-demotes-fenced-reply effects/untrackedFencedReplyRefillsAndIsReadableTest |
| C56.cooperative-cancel | read deadline requests cooperative cancellation once for the shared execution | confirmationReadBudgetStartsAtItsOwnDispatchTest: C1 starts after 4 ms of earlier work and receives its full 5 ms read budget. It remains live at overall 8 ms and requests exactly one cancellation with confirmation_error at 9 ms. readTimeoutStartsIndependentSourceDeadlineTest: One shared read deadline requests one cancellation for two pending callers. | shadow-read-deadlines / confirmation-read-budget-starts-at-dispatch effects / read-timeout-starts-source shadow-read-deadlines/confirmationReadBudgetStartsAtItsOwnDispatchTest |
| C56.late-read | late read fulfillment checks deadline before timer delivery | lateReadCannotBecomeHitTest: A reply observed after elapsed read budget cannot start fresh decode even before timer delivery. lateReadRejectionUsesDeadlineCategoryTest: late read fulfillment checks deadline before timer delivery The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | effects / read-late-settlement |
| C56.clear-read-timer | successful read does not request cancellation after its timer is cleared | acquiredDecodeSurvivesInvalidationAndDeadlineTest: A read accepted before deadline does not request cancellation when decoding later crosses the budget. successfulReadClearsDeadlineBeforeDecodeTest: successful read does not request cancellation after its timer is cleared The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | effects / successful-read-has-no-late-cancel |
| C57.recovery-age | recovery age is sampled after asynchronous decode and only on served outcome | agesRequireRecovery: Witness checks successful decode age against observed diagnostic; existing agesRequireRecovery invariant checks no nonserved age samples. | recovery / recovery-age-sampled-at-successful-decode |
| C57.shadow-age | shadow mismatch samples original frame age at verdict | confirmationKeepsOriginalAgeTest: A mismatch records C0's age at verdict, not the replacement C1 timestamp. retainedC0AgeIsSampledAtTheVerdictTest: A C0 acquired one millisecond inside freshness remains the comparison snapshot, and its confirmed mismatch reports the age at the later verdict. | shadow / age-at-verdict dark-layers / held-dark-c0-age-at-verdict dark-layers/retainedC0AgeIsSampledAtTheVerdictTest |
| C57.clamp-age | shadow verdict age clamps application clock rollback to zero | ageClampsAfterWallRollbackTest: A match age sample after wall rollback clamps to zero. confirmationRollbackKeepsPayloadAndClampsAgeTest: A held C1 confirmation after1000ms wall rollback still confirms mismatch, and reported retained-C0 age is exactly0 rather than a negative or absolute duration. | shadow / age-clamped-after-rollback shadow / shadow-confirmation-rollback-keeps-payload-and-reports-offset shadow/confirmationRollbackKeepsPayloadAndClampsAgeTest |
| C57.future-offset | serving future offset uses the observing layer and positive seconds | futureFrameReportsPositiveObservingOffsetTest: Serving future frame emits one remote futureOffset at +1000 modeled milliseconds, projected as +1 public second, skips serializer and preserves source error. Dark and confirmation observing locations remain outside this model. confirmationRollbackKeepsPayloadAndClampsAgeTest: A successful C1 read of now-future bytes reports exactly one futureTimestampOffset event with namespace urn, useCase Behavior, keyType id, layer remote_shadow and offset1000ms. The frame remains a valid C1 payload-identity participant and confirms mismatch without repair. futureDarkAcquisitionReportsOffsetAndFillsMissTest: A fresh seeded C0 becomes1000ms future after wall rollback. Dark acquisition emits exactly one futureTimestampOffset event labeled urn/Behavior/id/remote_shadow with1000ms; it treats the frame as semantic miss, never decodes it, and may fill from accepted source2. futureLateDarkReadKeepsTimeoutAndReportsOffsetTest: A raw dark read returns after the10ms job/caller deadline but inside its separate60s read budget. Its now-future frame emits remote_shadow offset990ms while caller timeout and single job timeout verdict remain; no decode, serialization or write can resume. rollbackMakesTheSeededFrameFutureAndReportsItsOffsetTest: A wall rollback makes a seeded C0 future-dated; the held dark read reports the remote_shadow offset, skips decode and permits a source fill. | effects / event:futureOffset effects / future-offset-observing-layer-positive-seconds shadow / shadow-confirmation-rollback-keeps-payload-and-reports-offset shadow / future-dark-c0-reports-offset-and-fills-semantic-miss shadow / late-dark-read-reports-offset-without-reviving-job dark-layers / future-dark-c0-reports-offset-and-fills effects/futureFrameReportsPositiveObservingOffsetTest shadow/confirmationRollbackKeepsPayloadAndClampsAgeTest shadow/futureDarkAcquisitionReportsOffsetAndFillsMissTest shadow/futureLateDarkReadKeepsTimeoutAndReportsOffsetTest dark-layers/rollbackMakesTheSeededFrameFutureAndReportsItsOffsetTest |
| C58.shared-trail | coalesced remote failure records one leader trail and one follower event | coalescedFailureKeepsOneLeaderAndFollowerTrailTest: Two coalesced callers share one failed read/source trail. Public event ordering includes one remote request, one process follower, remote cache_read error then fallback error, with both original caller errors. | effects / shared-failure-preserves-leader-and-follower-trail effects/coalescedFailureKeepsOneLeaderAndFollowerTrailTest |
| C58.recovered-failure | recovered source failure remains a fallback diagnostic | recoveredValueKeepsOriginalFallbackDiagnosticTest: Successful retained recovery preserves one original remote fallback error diagnostic, one classifier/decode and served outcome with no shared publication. | recovery / recovery-keeps-source-failure-trail recovery/recoveredValueKeepsOriginalFallbackDiagnosticTest |
| C59.remote-includes-decode | remote get duration includes fresh decoding without spending a source budget | readDurationIncludesDecodeTest: Remote get duration includes delayed fresh decode while accepted decoding starts no source budget. acquiredDecodeSurvivesInvalidationAndDeadlineTest: Remote get duration includes delayed fresh decode while accepted decoding starts no source budget. | effects / duration:load |
| C59.source-excludes-publication | accepted publication time is separate from reported source duration | sourceDurationExcludesPublicationTest: Source duration stays at its accepted settlement interval while serialization has a separate later duration. | effects / duration:dump |
| C60.logging-default-off | Omitting the logging flag leaves mismatch warnings disabled | omittedLoggingKeepsMismatchMetricsOnlyTest: The comparator fixture omits logging entirely. Confirmed mismatch still emits one age sample and verdict, with zero warning and zero configuration failure; public action history never includes a false logging reply. | shadow / omitted-logging-defaults-off shadow / omitted-shadow-logging-keeps-mismatch-metrics-only shadow/omittedLoggingKeepsMismatchMetricsOnlyTest |
| C60.logging-enabled | mismatch warning enabled with mismatch verdict | explicitInequalityRequiresConfirmationTest: Confirmed mismatch warns only after C1; accepted enabled logging remains in effect despite later policy disable. acceptedLoggingSurvivesPolicyChangeTest: Confirmed mismatch warns only after C1; accepted enabled logging remains in effect despite later policy disable. | shadow / mismatch-logging:true |
| C60.no-warning-on-match | mismatch warning enabled with match verdict | warningsRequireMismatch: Warnings never exceed the confirmed mismatches, so a match adds none. This constrains warnings for match but does not test every logger implementation. | shadow / enabled-logging-match-has-no-warning |
| C60.no-warning-on-superseded | mismatch warning enabled with superseded verdict | warningsRequireMismatch: Warnings never exceed the confirmed mismatches, so a supersession adds none. | shadow / enabled-logging-superseded-has-no-warning |
| C60.invalid-logging-policy | Malformed runtime mismatch logging records configuration failure and leaves an eligible job active with logging off | invalidLoggingCannotBeCaptured: An invalid logging flag is never captured as enabled. Admission still records one configuration error, comparison reaches mismatch, and no warning is emitted. invalidLoggingKeepsComparisonWithoutWarningTest: An invalid logging flag is never captured as enabled. Admission still records one configuration error, comparison reaches mismatch, and no warning is emitted. | shadow / invalid-logging-compares-without-warning |
| W01.key-identity | Construct interoperable logical, value, and watermark keys | successfulKeysHaveOneOperationDelimiter: UTF-8 percent escaping with uppercase hex and URI-safe punctuation, one operation delimiter, ordered raw arguments, frame suffix, and tracked watermark grouping; all ASCII plus bounded Unicode sequences moved through every identity/argument component. Caller-supplied configuration omission belongs to native construction tests. encodingSeparatesReservedDelimitersTest: UTF-8 percent escaping with uppercase hex and URI-safe punctuation, one operation delimiter, ordered raw arguments, frame suffix, and tracked watermark grouping; all ASCII plus bounded Unicode sequences moved through every identity/argument component. Caller-supplied configuration omission belongs to native construction tests. surrogatePairEncodesOneFourByteScalarTest: UTF-8 percent escaping with uppercase hex and URI-safe punctuation, one operation delimiter, ordered raw arguments, frame suffix, and tracked watermark grouping; all ASCII plus bounded Unicode sequences moved through every identity/argument component. Caller-supplied configuration omission belongs to native construction tests. trackedArgumentsDoNotChangeWatermarkTest: UTF-8 percent escaping with uppercase hex and URI-safe punctuation, one operation delimiter, ordered raw arguments, frame suffix, and tracked watermark grouping; all ASCII plus bounded Unicode sequences moved through every identity/argument component. Caller-supplied configuration omission belongs to native construction tests. | protocol/keyVectors/* |
| W01.invalid-identity | Reject unsupported key identities, including tracked component braces, namespace braces and unpaired UTF-16 code units in escaped identities. | keyAcceptanceRespectsTextAndHashTagDomain: Reject unpaired UTF-16 units in each encoded component, namespace braces in either mode, and keyType/id braces only when tracked. Raw unit overrides construct actual malformed native inputs; removed properties and host type errors remain fixed/native API boundaries. rejectedKeysExposeNoPartialIdentity: Reject unpaired UTF-16 units in each encoded component, namespace braces in either mode, and keyType/id braces only when tracked. Raw unit overrides construct actual malformed native inputs; removed properties and host type errors remain fixed/native API boundaries. malformedUtf16RejectsInsteadOfReplacementTest: Reject unpaired UTF-16 units in each encoded component, namespace braces in either mode, and keyType/id braces only when tracked. Raw unit overrides construct actual malformed native inputs; removed properties and host type errors remain fixed/native API boundaries. bracesDependOnEntityTrackingTest: Reject unpaired UTF-16 units in each encoded component, namespace braces in either mode, and keyType/id braces only when tracked. Raw unit overrides construct actual malformed native inputs; removed properties and host type errors remain fixed/native API boundaries. | protocol/invalidKeyVectors/* |
| W02.sorted-arguments | Normalize scalar arguments with prescribed UTF-16 name ordering, omission, formatting and escaping; preserve explicitly supplied ordered argument pairs. | normalizedNamesAreOrderedAndValuesAssociated: Separate normalized records from caller-ordered key pairs: omit Absent, retain null/false/true/empty/literal text, sort UTF-16 names including astral versus BMP order, preserve prototype-like own names and exact signed safe integers/bigints with magnitude fitting i64. Float shortest-decimal/scientific/-0/nonfinite and arbitrary bigint width are explicit native binding boundaries. normalizedIntegersRetainExactMagnitude: Separate normalized records from caller-ordered key pairs: omit Absent, retain null/false/true/empty/literal text, sort UTF-16 names including astral versus BMP order, preserve prototype-like own names and exact signed safe integers/bigints with magnitude fitting i64. Float shortest-decimal/scientific/-0/nonfinite and arbitrary bigint width are explicit native binding boundaries. normalizedNamesUseUtf16OrderingTest: Separate normalized records from caller-ordered key pairs: omit Absent, retain null/false/true/empty/literal text, sort UTF-16 names including astral versus BMP order, preserve prototype-like own names and exact signed safe integers/bigints with magnitude fitting i64. Float shortest-decimal/scientific/-0/nonfinite and arbitrary bigint width are explicit native binding boundaries. normalizedPrimitivesPreserveFalsyAndOmittedValuesTest: Separate normalized records from caller-ordered key pairs: omit Absent, retain null/false/true/empty/literal text, sort UTF-16 names including astral versus BMP order, preserve prototype-like own names and exact signed safe integers/bigints with magnitude fitting i64. Float shortest-decimal/scientific/-0/nonfinite and arbitrary bigint width are explicit native binding boundaries. signedBigintsPreserveEveryDecimalDigitTest: Separate normalized records from caller-ordered key pairs: omit Absent, retain null/false/true/empty/literal text, sort UTF-16 names including astral versus BMP order, preserve prototype-like own names and exact signed safe integers/bigints with magnitude fitting i64. Float shortest-decimal/scientific/-0/nonfinite and arbitrary bigint width are explicit native binding boundaries. orderedKeyArgumentsRetainDuplicatesTest: Separate normalized records from caller-ordered key pairs: omit Absent, retain null/false/true/empty/literal text, sort UTF-16 names including astral versus BMP order, preserve prototype-like own names and exact signed safe integers/bigints with magnitude fitting i64. Float shortest-decimal/scientific/-0/nonfinite and arbitrary bigint width are explicit native binding boundaries. | protocol/normalizeArgsVectors/* |
| W03.cohort-assignment | Serving and shadow cohorts use their specified independent deterministic assignment | cohortNumeratorsAreUnsignedAndBoundariesStrict: Compute FNV-1a over UTF-16 units of logical key plus local/remote/shadow discriminator with XOR and modulo-2^32 multiplication. Generated exact numerators are converted only to the public percent representation. Strict admission is checked in Quint; runtime-boundaries and shadow-layers replay actual equal/below/above policy consequences. publishedCohortNumeratorsRemainStableTest: Compute FNV-1a over UTF-16 units of logical key plus local/remote/shadow discriminator with XOR and modulo-2^32 multiplication. Generated exact numerators are converted only to the public percent representation. Strict admission is checked in Quint; runtime-boundaries and shadow-layers replay actual equal/below/above policy consequences. | protocol/rampVectors/* |
| W04.frame-encoding | Encode version, timestamp, UTF-8 and binary payloads in interoperable frames | encodedFrameKeepsHeaderAndPayload: Concrete version-1 header and big-endian timestamp bytes, text UTF-16 replacement and binary identity across the declared finite byte/code-unit inputs; actual frame bytes checked in both ports. payloadUnpairedSurrogateUsesReplacementTest: Concrete version-1 header and big-endian timestamp bytes, text UTF-16 replacement and binary identity across the declared finite byte/code-unit inputs; actual frame bytes checked in both ports. | protocol/frameVectors/* |
| W04.tracked-decoder | Classify tracked frames and malformed watermarks with specified precedence | nilValueIsValueAbsent: Abstract reply/frame/watermark/encoding classes check classification precedence; exact bytes and host numeric boundaries remain vectors. fenceCanPrecedeEncodingError: Abstract reply/frame/watermark/encoding classes check classification precedence; exact bytes and host numeric boundaries remain vectors. malformedWatermarkPrecedesEncodingError: Abstract reply/frame/watermark/encoding classes check classification precedence; exact bytes and host numeric boundaries remain vectors. trackedZeroTimestampIsNotHit: Abstract reply/frame/watermark/encoding classes check classification precedence; exact bytes and host numeric boundaries remain vectors. encodingErrorRequiresSupportedFrame: Abstract reply/frame/watermark/encoding classes check classification precedence; exact bytes and host numeric boundaries remain vectors. fencedEncodingTest: Abstract reply/frame/watermark/encoding classes check classification precedence; exact bytes and host numeric boundaries remain vectors. malformedWatermarkTest: Abstract reply/frame/watermark/encoding classes check classification precedence; exact bytes and host numeric boundaries remain vectors. trackedHitsStrictlyClearValidFence: Tracked decoder matrix covers missing/short/unsupported/zero/supported frames, decimal watermark validity and payload tags; paired miss metadata and exact decoded scalar/byte output are replayed. Invalid host reply object types stay in the existing abstraction and native binding tests. absentValueKeepsItsOwnClassification: Tracked decoder matrix covers missing/short/unsupported/zero/supported frames, decimal watermark validity and payload tags; paired miss metadata and exact decoded scalar/byte output are replayed. Invalid host reply object types stay in the existing abstraction and native binding tests. trackedFencePrecedesEncodingErrorTest: Tracked decoder matrix covers missing/short/unsupported/zero/supported frames, decimal watermark validity and payload tags; paired miss metadata and exact decoded scalar/byte output are replayed. Invalid host reply object types stay in the existing abstraction and native binding tests. | protocol/trackedDecodeVectors/* |
| W04.untracked-decoder | Classify untracked frames without applying watermarks | untrackedIgnoresMalformedWatermarkTest: Untracked decoder ignores watermark content and permits zero timestamp while preserving byte/scalar output and payload-encoding errors in its finite frame matrix. decodedTextContainsOnlyScalars: Untracked decoder ignores watermark content and permits zero timestamp while preserving byte/scalar output and payload-encoding errors in its finite frame matrix. | protocol/untrackedDecodeVectors/* |
| W04.invalid-timestamps | Reject unsafe, negative or fractional timestamps before mutation | writerRejectsInvalidNumericDomain: Writer rejects negative, fractional, first-unsafe, NaN and positive/negative infinity inputs; native bindings convert explicit numeric tags only, while Quint computes rejection. | protocol/invalidTimestampVectors/* |
| W05.duration-bounds | Round native write durations up within the supported positive bound | acceptedDurationWithinCeiling: Rational finite inputs and explicit nonfinite tags distinguish ceil-to-positive-integer acceptance through 365 days, exclusive overflow, zero and invalid inputs; actual adapter-level duration APIs replay the Quint prediction. physicalDurationRoundsUpWithinBoundTest: Rational finite inputs and explicit nonfinite tags distinguish ceil-to-positive-integer acceptance through 365 days, exclusive overflow, zero and invalid inputs; actual adapter-level duration APIs replay the Quint prediction. | protocol/durationVectors/* |
| W06.envelope-markers | Escape raw marker bytes while decoding supported legacy envelopes | rawEscapeIsLossless: Fifteen explicit raw binary prefixes cover marker escaping, single-prefix unescape, unknown legacy zero prefixes and corrupt-marked fallback; native wrappers replay every result. escapeConsumesExactlyOnePrefix: Fifteen explicit raw binary prefixes cover marker escaping, single-prefix unescape, unknown legacy zero prefixes and corrupt-marked fallback; native wrappers replay every result. unknownZeroPrefixPassesThroughUnchanged: A binary payload whose leading zero is followed by nothing or by a byte above 2 is legacy raw data: the read outcome is passthrough with every byte returned. Complements the one-prefix unescape invariant; together they cover every zero-prefixed vector input. escapedCompressedMarkerRemainsLiteralTest: Fifteen explicit raw binary prefixes cover marker escaping, single-prefix unescape, unknown legacy zero prefixes and corrupt-marked fallback; native wrappers replay every result. unknownLegacyZeroPrefixRemainsUntouchedTest: Fifteen explicit raw binary prefixes cover marker escaping, single-prefix unescape, unknown legacy zero prefixes and corrupt-marked fallback; native wrappers replay every result. corruptCompressionPreservesMarkedBytesTest: Fifteen explicit raw binary prefixes cover marker escaping, single-prefix unescape, unknown legacy zero prefixes and corrupt-marked fallback; native wrappers replay every result. | protocol/envelopeVectors/* |
| W06.compressed-decode | Decode fixed compressed UTF-8 and binary envelopes | readFailuresPreserveOriginalBinary: Both markers decode ten independently verified raw-block codec fixtures, including malformed UTF-8 and BOM/scalar boundaries; three rejected codec headers and injected output limits retain exact original marked bytes. Arbitrary zstd streams, dictionaries and windows are native boundaries. successfulReadRespectsMarkerAndLimit: Both markers decode ten independently verified raw-block codec fixtures, including malformed UTF-8 and BOM/scalar boundaries; three rejected codec headers and injected output limits retain exact original marked bytes. Arbitrary zstd streams, dictionaries and windows are native boundaries. corruptCompressionPreservesMarkedBytesTest: Both markers decode ten independently verified raw-block codec fixtures, including malformed UTF-8 and BOM/scalar boundaries; three rejected codec headers and injected output limits retain exact original marked bytes. Arbitrary zstd streams, dictionaries and windows are native boundaries. decoderLimitKeepsRawBytesTest: Both markers decode ten independently verified raw-block codec fixtures, including malformed UTF-8 and BOM/scalar boundaries; three rejected codec headers and injected output limits retain exact original marked bytes. Arbitrary zstd streams, dictionaries and windows are native boundaries. | protocol/compressedDecodeVectors/* |
| W07.compression-selection | Compress only at the byte threshold and only when stored size shrinks | compressionUsesByteThresholdAndStrictShrink: Fourteen concrete payloads cross three UTF-8 byte thresholds and three injected maximum-output caps. Each native level-3 codec byte count is independently verified; Quint computes each binding selection, strict shrink against escaped raw bytes, marker and stored size. Native compressed-size differences may produce different compression diagnostics but preserve logical payload. utf8ThresholdCountsBytesTest: Fourteen concrete payloads cross three UTF-8 byte thresholds and three injected maximum-output caps. Each native level-3 codec byte count is independently verified; Quint computes each binding selection, strict shrink against escaped raw bytes, marker and stored size. Native compressed-size differences may produce different compression diagnostics but preserve logical payload. compressionTieKeepsRawRepresentationTest: Fourteen concrete payloads cross three UTF-8 byte thresholds and three injected maximum-output caps. Each native level-3 codec byte count is independently verified; Quint computes each binding selection, strict shrink against escaped raw bytes, marker and stored size. Native compressed-size differences may produce different compression diagnostics but preserve logical payload. shrinkComparedWithEscapedRawBytesTest: Fourteen concrete payloads cross three UTF-8 byte thresholds and three injected maximum-output caps. Each native level-3 codec byte count is independently verified; Quint computes each binding selection, strict shrink against escaped raw bytes, marker and stored size. Native compressed-size differences may produce different compression diagnostics but preserve logical payload. thresholdPrecedesWriteLimitTest: Fourteen concrete payloads cross three UTF-8 byte thresholds and three injected maximum-output caps. Each native level-3 codec byte count is independently verified; Quint computes each binding selection, strict shrink against escaped raw bytes, marker and stored size. Native compressed-size differences may produce different compression diagnostics but preserve logical payload. writeLimitPrecedesCompressionTest: Fourteen concrete payloads cross three UTF-8 byte thresholds and three injected maximum-output caps. Each native level-3 codec byte count is independently verified; Quint computes each binding selection, strict shrink against escaped raw bytes, marker and stored size. Native compressed-size differences may produce different compression diagnostics but preserve logical payload. | protocol/compressionWriteVectors/* |
| W08.legacy-reading | Disabling new compression does not disable reading previously compressed values | readDoesNotConsultNewWritePolicy: The envelope reader ignores the model new-write policy input. Its native helper has no policy argument; combine primitive vectors with the actual compression:false recovery-read cached compressed history for the cache binding. disabledNewWritesStillReadLegacyCompressionTest: The envelope reader ignores the model new-write policy input. Its native helper has no policy argument; combine primitive vectors with the actual compression:false recovery-read cached compressed history for the cache binding. compressedRecoveryMemoizesWithoutLocalPublicationTest: Actual cache with new compression writes disabled still decodes the acquired compressed stale candidate and memoizes only in its request scope. This connects the unconditional envelope reader to resolved cache policy. | recovery-read / tracked-compressed-recovery-is-request-only recovery-read/compressedRecoveryMemoizesWithoutLocalPublicationTest protocol/compressedDecodeVectors/* |
| W04.strict-fence | Reject a tracked frame equal to its watermark | fenceCanPrecedeEncodingError: Tracked supported positive frames at equality are fenced; zero timestamp cannot yield a hit. trackedZeroTimestampIsNotHit: Tracked supported positive frames at equality are fenced; zero timestamp cannot yield a hit. servedSnapshotClearedObservedFence: Every served tracked snapshot has timestamp strictly above its acquired watermark. trackedHitsStrictlyClearValidFence: Tracked hit requires positive timestamp strictly greater than an observed valid watermark. A distinguishing equality regression rejects before unsupported payload encoding. trackedFencePrecedesEncodingErrorTest: Tracked hit requires positive timestamp strictly greater than an observed valid watermark. A distinguishing equality regression rejects before unsupported payload encoding. fenceBoundaryIsExclusive: Finite symbolic timestamp/watermark domains independently characterize strict timestamp-greater-than-fence acceptance; wire numeric validation is separate. frameAtTheWatermarkIsFencedFromTheDarkReadTest: A frame stamped exactly at the watermark is fenced from the dark read; after time advances, the source starts a fill instead of decoding the fenced frame. | dark-layers / dark-frame-at-watermark-is-fenced dark-layers/frameAtTheWatermarkIsFencedFromTheDarkReadTest protocol/trackedDecodeVectors/equal timestamp is fenced |
| C38.retention | Preserve persistence and longer TTLs while meeting the required retention floor | successfulRetentionMeetsBothFloors: Finite results meet the two-hour floor and cutoff-relative value-retention horizon exactly, preserve longer string TTL and preserve string persistence. stringsKeepExistingRetention: Finite results meet the two-hour floor and cutoff-relative value-retention horizon exactly, preserve longer string TTL and preserve string persistence. finiteRetentionIsExact: Finite results meet the two-hour floor and cutoff-relative value-retention horizon exactly, preserve longer string TTL and preserve string persistence. absentMarkerGetsRetentionFloorTest: Finite results meet the two-hour floor and cutoff-relative value-retention horizon exactly, preserve longer string TTL and preserve string persistence. longBufferExtendsRequiredRetentionTest: Finite results meet the two-hour floor and cutoff-relative value-retention horizon exactly, preserve longer string TTL and preserve string persistence. | invalidation/absent marker gets the two hour floor invalidation/large buffer extends retention beyond the floor invalidation/existing longer TTL never shrinks invalidation/persistent valid marker stays persistent |
| C38.marker-repair | Malformed strings preserve their existing retention; unrelated Redis types receive finite repair | stringsKeepExistingRetention: Malformed/unsafe/empty string values repair to canonical watermarks while retaining string TTL/persistence rules; ordered-list wrong types repair to finite required TTL without inheriting unrelated retention. unrelatedTypesReceiveFiniteRepair: Malformed/unsafe/empty string values repair to canonical watermarks while retaining string TTL/persistence rules; ordered-list wrong types repair to finite required TTL without inheriting unrelated retention. persistentMalformedStringStaysPersistentTest: Malformed/unsafe/empty string values repair to canonical watermarks while retaining string TTL/persistence rules; ordered-list wrong types repair to finite required TTL without inheriting unrelated retention. wrongTypeLongTtlIsNotInheritedTest: Malformed/unsafe/empty string values repair to canonical watermarks while retaining string TTL/persistence rules; ordered-list wrong types repair to finite required TTL without inheriting unrelated retention. wrongTypePersistenceIsNotInheritedTest: Malformed/unsafe/empty string values repair to canonical watermarks while retaining string TTL/persistence rules; ordered-list wrong types repair to finite required TTL without inheriting unrelated retention. emptyStringRetentionIsPreservedTest: Malformed/unsafe/empty string values repair to canonical watermarks while retaining string TTL/persistence rules; ordered-list wrong types repair to finite required TTL without inheriting unrelated retention. | invalidation/malformed finite marker is repaired with longer TTL preserved invalidation/malformed persistent marker stays persistent invalidation/wrong type persistent marker gets finite repair invalidation/wrong type marker does not preserve unrelated TTL |
| C39.numeric-limits | Accept the maximum valid future buffer and safe timestamp sum | argumentValidationIsExact: Maximum365day buffer and maximum safe timestamp/sum accepted with exact canonical decimal output; surrounding invalid boundary forms have separate preservation evidence. maximumBufferAndTimestampSumAreAcceptedTest: Maximum365day buffer and maximum safe timestamp/sum accepted with exact canonical decimal output; surrounding invalid boundary forms have separate preservation evidence. | invalidation/maximum future buffer is supported invalidation/maximum safe sum is supported |
| C38.buffer-cutoff | Add the requested future buffer to the invalidation timestamp | successfulCutoffIsExactMaximum: Without a greater prior cutoff, timestamp plus requested future buffer becomes the exact marker value; long buffers also change retention. longBufferExtendsRequiredRetentionTest: Without a greater prior cutoff, timestamp plus requested future buffer becomes the exact marker value; long buffers also change retention. | invalidation/buffer determines marker cutoff |
| C39.decimal-normalization | Normalize accepted leading-zero decimal watermark arguments | outputIsCanonicalDecimalString: Leading-zero decimal arguments are accepted and output zero/positive watermark text is canonical; valid prior values can still dominate the buffered proposal. decimalZerosAreCanonicalizedTest: Leading-zero decimal arguments are accepted and output zero/positive watermark text is canonical; valid prior values can still dominate the buffered proposal. | invalidation/leading decimal zeros are canonicalized |
| C16.explicit-null-leaf | Explicit null coalesce is invalid and bypasses existing cached entries without replacing them | invalidInvocationPolicyNeverTouchesStorage: Malformed boolean leaves are abstracted as invalid invocation admission. The check asserts no storage effects and retained memo; the fixed scenario binds actual JSON null to this invalid branch. invalidBooleanOverlayBypassesAndPreservesMemoTest: Malformed boolean leaves are abstracted as invalid invocation admission. The check asserts no storage effects and retained memo; the fixed scenario binds actual JSON null to this invalid branch. explicitNullCoalesceBypassesWithoutReplacingRemoteTest: Explicit null coalesce is invalid and bypasses existing cached entries without replacing them. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | runtime-boundaries / bypass-preserves-cache:null-coalesce runtime-boundaries/explicitNullCoalesceBypassesWithoutReplacingRemoteTest |
| C31.local-only-publication | Tracked local-only calls retain eligible local source publication | trackedWithoutRemoteStillPublishesLocalTest: Tracked local-only calls retain eligible local source publication. This check covers the bounded model clause: trackedWithoutRemoteStillPublishesLocalTest. Host representations and other feature combinations retain separate fixed/native evidence. trackedWithoutRemotePublishesReusableLocalTest: Tracked local-only calls retain eligible local source publication. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | layers / tracked-local-only-hit layers/trackedWithoutRemotePublishesReusableLocalTest |
| C31.ramped-down-publication | Tracked calls excluded from remote serving retain eligible local source publication | trackedWithoutRemoteStillPublishesLocalTest: Tracked calls excluded from remote serving retain eligible local source publication. This check covers the bounded model clause: trackedWithoutRemoteStillPublishesLocalTest. Host representations and other feature combinations retain separate fixed/native evidence. | layers / tracked-remote-disabled-local-hit |
| W04.malformed-text | Direct and decompressed text use maximal-subpart UTF-8 replacement without BOM removal; binary remains exact | decodedTextContainsOnlyScalars: Pure UTF-8 maximal-subpart consumption and UTF-16 writer replacement compute expected Unicode scalars/bytes; finite lead/continuation/truncation/overlong/surrogate/ceiling/BOM inputs replay against real codecs. Zstd wrapper binding uses separate generated envelope cases. maximalSubpartConsumesAcceptedPrefixOnceTest: Pure UTF-8 maximal-subpart consumption and UTF-16 writer replacement compute expected Unicode scalars/bytes; finite lead/continuation/truncation/overlong/surrogate/ceiling/BOM inputs replay against real codecs. Zstd wrapper binding uses separate generated envelope cases. malformedSurrogateBytesRemainSeparateErrorsTest: Pure UTF-8 maximal-subpart consumption and UTF-16 writer replacement compute expected Unicode scalars/bytes; finite lead/continuation/truncation/overlong/surrogate/ceiling/BOM inputs replay against real codecs. Zstd wrapper binding uses separate generated envelope cases. payloadUnpairedSurrogateUsesReplacementTest: Pure UTF-8 maximal-subpart consumption and UTF-16 writer replacement compute expected Unicode scalars/bytes; finite lead/continuation/truncation/overlong/surrogate/ceiling/BOM inputs replay against real codecs. Zstd wrapper binding uses separate generated envelope cases. | protocol/trackedDecodeVectors/ protocol/untrackedDecodeVectors/ protocol/compressedDecodeVectors/* |
| C27.decode-failure-refill | A failed fresh decode falls through to the source and may refill Redis when the read itself granted publication authority. | decodeFailureMayRefillTest: A failed fresh decode falls through to the source and may refill Redis when the read itself granted publication authority. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | effects / failed-decode-refills |
| C33.reject-future-before-decode | At initial serving or recovery acquisition, a future-dated frame is rejected before deserialization; later shadow confirmation has a separate payload-identity contract. | futureFrameDoesNotCarryMissFenceTest: The model rejects an acquired future frame and excludes it from recovery; generated rollback evidence exercises future rejection, while fixed scenarios exercise direct future timestamps before deserialization. | policy / rollback-rejects-future-remote recovery/futureFrameDoesNotCarryMissFenceTest |
| C33.reject-unsafe-before-decode | An unsafe frame timestamp is rejected before deserialization or stale-candidate retention. | invalidFrameNeverBecomesRecoveryCandidateTest: Verification model abstracts invalid frame structure; wire vectors separately distinguish unsafe timestamps from malformed/version/encoding fields. unsafeTimestampSkipsSerializerAndAllowsRefillTest: A real frame with timestamp 2^53+1 and supported payload encoding never reaches the serializer; source refill remains allowed and is verified by a later public hit. Payload envelope decoding precedes core timestamp validation; this case does not assert timestamp validation before payload encoding checks. unsafeTimestampAtTheWatermarkStillRefillsTest: An unsafe stamp above a watermark raised at the same instant is visible and never fresh: the read holds no decode and its miss refills unfenced with the policy retention. | recovery-read / unsafe-timestamp-skips-serializer-and-refills recovery-read/unsafeTimestampSkipsSerializerAndAllowsRefillTest recovery-read/unsafeTimestampAtTheWatermarkStillRefillsTest |
| C33.reject-version-before-decode | An unsupported frame version is rejected before payload deserialization. | unsupportedFramePrecedesEncodingError: The decoder classifies unsupported frame versions before consulting payload encoding. Fixed cache-path scenarios establish that this miss skips application deserialization. unsupportedVersionSkipsSerializerAndAllowsRefillTest: Unsupported version-2 bytes never reach the serializer; source refill remains allowed and a subsequent independent request reads the new value. unsupportedVersionUnderRaisedWatermarkIsAFencedMissTest: An unsupported-version frame under a watermark raised at the same instant is read as a miss that carries the fence: no decode is held and the refill stamped at that instant is fenced out, so nothing is dumped or written. | recovery-read / unsupported-version-skips-serializer-and-refills recovery-read/unsupportedVersionSkipsSerializerAndAllowsRefillTest recovery-read/unsupportedVersionUnderRaisedWatermarkIsAFencedMissTest |
| C45.recheck-before-decode | A retained candidate reaching its exclusive maximum age before source failure is rejected without starting its decode. | maximumAgeBeforeDecodePreservesSourceTest: This bounded regression retains a candidate at M-1, advances to M before source rejection, and checks a source-error result with no load and one recovery miss. The separate recovery-read replay and required witness additionally bind compressed bytes and original source-error identity. maximumAgeBeforeDecodeSkipsLoadingTest: This abstract regression advances a retained candidate to its maximum age before the recovery check, preserving the source-rejection category without decoding or request publication. The separate recovery-read replay and required witness additionally bind compressed bytes and original source-error identity. maximumAgeBeforeDecodeKeepsOriginalErrorTest: A compressed retained candidate acquired at M-1 reaches M before source rejection; the original source error survives without decompression/serializer work or shared publication. | recovery-read / maximum-before-decode-preserves-original-error-without-load recovery-read/maximumAgeBeforeDecodeKeepsOriginalErrorTest recovery/maximumAgeBeforeDecodePreservesSourceTest |
| C50.served-match-diagnostic | A served-hit shadow match keeps the originally returned value and emits a match without cache repair. | callsKeepAcquiredValue: A served-hit shadow match keeps the originally returned value and emits a match without cache repair. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. jobsAreDiagnostic: A served-hit shadow match keeps the originally returned value and emits a match without cache repair. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | admission / outcome:match |
| C50.served-mismatch-diagnostic | A confirmed served-hit shadow mismatch keeps the originally returned value and does not repair the cache. | callsKeepAcquiredValue: A confirmed served-hit shadow mismatch keeps the originally returned value and does not repair the cache. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. jobsAreDiagnostic: A confirmed served-hit shadow mismatch keeps the originally returned value and does not repair the cache. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | admission / outcome:mismatch |
| C53.source-error-keeps-caller | A detached shadow source failure reports its diagnostic outcome without replacing the value already served to the caller. | callsKeepAcquiredValue: A detached shadow source failure reports its diagnostic outcome without replacing the value already served to the caller. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. jobsAreDiagnostic: A detached shadow source failure reports its diagnostic outcome without replacing the value already served to the caller. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | admission / outcome:source_error |
| C20.invalid-coalesce | An invalid runtime coalesce leaf bypasses every layer and sharing rather than inheriting or coercing the invalid value. | invalidInvocationPolicyNeverTouchesStorage: The core model abstracts malformed invocation-level leaves as invalid admission and checks bypass plus preserved memo. Fixed scenarios supply the actual malformed coalesce/requestLocal values. invalidBooleanOverlayBypassesAndPreservesMemoTest: The core model abstracts malformed invocation-level leaves as invalid admission and checks bypass plus preserved memo. Fixed scenarios supply the actual malformed coalesce/requestLocal values. invalidCoalesceBypassesWithoutReplacingRemoteTest: An invalid runtime coalesce leaf bypasses every layer and sharing rather than inheriting or coercing the invalid value.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. invalidBooleanLeavesBypassAllCaching: An invalid runtime coalesce leaf bypasses every layer and sharing rather than inheriting or coercing the invalid value.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | runtime-boundaries / bypass-preserves-cache:invalid-coalesce runtime-boundaries/invalidCoalesceBypassesWithoutReplacingRemoteTest |
| C20.invalid-request-local | An invalid runtime requestLocal leaf bypasses every layer rather than disabling only request memoization. | invalidInvocationPolicyNeverTouchesStorage: The core model abstracts malformed invocation-level leaves as invalid admission and checks bypass plus preserved memo. Fixed scenarios supply the actual malformed coalesce/requestLocal values. invalidBooleanOverlayBypassesAndPreservesMemoTest: The core model abstracts malformed invocation-level leaves as invalid admission and checks bypass plus preserved memo. Fixed scenarios supply the actual malformed coalesce/requestLocal values. invalidRequestLocalBypassesWithoutReplacingRemoteTest: An invalid runtime requestLocal leaf bypasses every layer rather than disabling only request memoization.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. invalidBooleanLeavesBypassAllCaching: An invalid runtime requestLocal leaf bypasses every layer rather than disabling only request memoization.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | runtime-boundaries / bypass-preserves-cache:invalid-request-local runtime-boundaries/invalidRequestLocalBypassesWithoutReplacingRemoteTest |
| C42.operation-denial | An operation recovery denial replaces an instance allow predicate and preserves the original source failure. | operationDenialReplacesInstanceAllowTest: An operation recovery denial replaces an instance allow predicate and preserves the original source failure. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | recovery / operation-denial-overrides-instance-allow recovery/operationDenialReplacesInstanceAllowTest |
| C54.dump-ownership | A timed-out shadow job retains its capacity while its serialization is unfinished; late serialization cannot initiate a write. | timedOutDarkDumpKeepsCapacityUntilRawReleaseTest: Generated dark-layers history now requires a competing key to be dropped after the job timeout and admitted only after the raw dump settles; the late dump dispatches no write. lateFillSerializationCannotDispatchWriteTest: This witness proves late-effect suppression only. Fixed capacity probes must remain attached to this case. | dark-layers / timed-out-dark-dump-retains-capacity-until-raw-release shadow / late-shadow-dump-cannot-dispatch-write dark-layers/timedOutDarkDumpKeepsCapacityUntilRawReleaseTest |
| C54.write-ownership | A timed-out shadow job retains its capacity while a dispatched write is unfinished; late completion cannot produce a second outcome. | timedOutDarkWriteKeepsCapacityUntilRawReleaseTest: Generated dark-layers history now requires a competing key to be dropped after the job timeout and admitted only after the dispatched raw write settles, with no second verdict. lateFillWriteCannotEmitAnotherVerdictTest: This witness proves post-timeout completion does not alter result/verdict; fixed capacity probe proves retained slot. | dark-layers / timed-out-dark-write-retains-capacity-until-raw-release shadow / late-shadow-write-cannot-change-caller-or-verdict dark-layers/timedOutDarkWriteKeepsCapacityUntilRawReleaseTest |
| C54.dark-read-ownership | A timed-out dark read retains capacity until the raw read settles, and its late result cannot initiate decoding or publication. | readBeforeDeadlineCanFillAndCancelsItsTimerTest: A C0 released at 4 ms inside a 5 ms read budget can fill from the completed caller source; subsequent time advancement emits no read cancellation or timeout verdict. c0ReadDeadlineKeepsRawCapacityTest: A separately bounded C0 read reports redis_error at 5 ms while the caller keeps its source value; another key is dropped until the raw adapter operation settles, after which a new job is admitted without late decode or fill. timedOutDarkReadKeepsCapacityUntilRawReleaseTest: Generated dark-layers history requires capacity retention after the whole-job timeout while C0 is held, followed by admission after raw release. The shadow-read-deadlines profile independently checks the separate read-deadline capacity boundary. lateDarkReadCannotStartDecodeOrFillTest: This witness proves late-effect suppression only. Capacity retention is a separate fixed-scenario observation for the dark read. | shadow-read-deadlines / timely-shadow-read-cancels-deadline-and-fills shadow-read-deadlines / c0-read-timeout-retains-raw-capacity dark-layers / timed-out-dark-read-retains-capacity-until-raw-release shadow / late-c0-cannot-start-new-shadow-work shadow-read-deadlines/readBeforeDeadlineCanFillAndCancelsItsTimerTest shadow-read-deadlines/c0ReadDeadlineKeepsRawCapacityTest dark-layers/timedOutDarkReadKeepsCapacityUntilRawReleaseTest |
| C06.absent-distinct-from-text | An absent value and the literal string undefined remain distinct cacheable results. | requestAbsenceAndLiteralTextStayDistinctTest: Both actual absence and literal string undefined settle as independent same-key source results and are distinguished by subsequent request/local/remote reads. localAbsenceAndLiteralTextStayDistinctTest: Both actual absence and literal string undefined settle as independent same-key source results and are distinguished by subsequent request/local/remote reads. remoteAbsenceAndLiteralTextStayDistinctTest: Both actual absence and literal string undefined settle as independent same-key source results and are distinguished by subsequent request/local/remote reads. | runtime-boundaries / absent-distinct-from-text:request runtime-boundaries / absent-distinct-from-text:local runtime-boundaries / absent-distinct-from-text:remote runtime-boundaries/requestAbsenceAndLiteralTextStayDistinctTest runtime-boundaries/localAbsenceAndLiteralTextStayDistinctTest runtime-boundaries/remoteAbsenceAndLiteralTextStayDistinctTest |
| C24.independent-source-budgets | Uncoalesced same-key callers each receive their full source budget from their own source start; one timeout does not shorten another budget. | eachSourceKeepsItsFullBudget: Two uncoalesced same-key callers start sources five milliseconds apart. First timeout does not cancel the second, which can succeed at elapsed11 or time out at its own elapsed15 deadline. Both reads acquire fenced storage, so recovery cannot mask shortened deadlines. Clock advance delivers modeled due timers; no timer-undelivered acceptance claim. staggeredSourceStartsKeepIndependentBudgetsTest: Two uncoalesced same-key callers start sources five milliseconds apart. First timeout does not cancel the second, which can succeed at elapsed11 or time out at its own elapsed15 deadline. Both reads acquire fenced storage, so recovery cannot mask shortened deadlines. Clock advance delivers modeled due timers; no timer-undelivered acceptance claim. staggeredSourcesExpireAtTheirOwnDeadlineTest: Two uncoalesced same-key callers start sources five milliseconds apart. First timeout does not cancel the second, which can succeed at elapsed11 or time out at its own elapsed15 deadline. Both reads acquire fenced storage, so recovery cannot mask shortened deadlines. Clock advance delivers modeled due timers; no timer-undelivered acceptance claim. independentSourceOriginsMatchContract: The independent profile reconstructs source starts and caller ownership from preceding read/decode events or owned read deadlines during time advance, then compares actual modeled source origins and call-to-source links. Read-deadline correctness remains a profile obligation. | independent / later-source-survives-earlier-deadline independent / later-source-expires-at-own-deadline independent/staggeredSourceStartsKeepIndependentBudgetsTest independent/staggeredSourcesExpireAtTheirOwnDeadlineTest |
| C23.policy-does-not-spend-source-budget | Waiting for runtime policy does not consume the subsequent source budget. | acceptedSourceRespectsItsOwnStart: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. heldPolicyDoesNotSpendSourceBudgetTest: Held policy and source gates, eight callers, and local-only storage exercise default/unbounded/ten-millisecond budgets. Public result and subsequent local reuse distinguish source deadline ownership, pre-source policy time, and enabled key-error behavior; no remote/read/shadow timing claim. sourceOriginsMatchContract: Each source-budgets source start projects the preceding external clock and captured mode into a separate start/budget record; the executing profile fields must agree. | source-budgets / policy-wait-does-not-spend-source-budget source-budgets/heldPolicyDoesNotSpendSourceBudgetTest |
| C30.original-source-error | Observer failure preserves the identity of the original source rejection. | observerFailuresCannotReplaceSourceErrorTest: Observer failure preserves the identity of the original source rejection. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | effects / observer-failure-source-error effects/observerFailuresCannotReplaceSourceErrorTest |
| C54.unbounded-source-bounded-shadow | Disabling the caller source deadline leaves detached shadow work subject to a finite job deadline. | unboundedCallerSurvivesDarkJobDeadlineTest: At the finite60000ms dark-job deadline an explicitly unbounded caller remains pending. A same-key second dark read is admitted, proving release of the old diagnostic slot; the first source later returns its value without late fill, while the second can start its own fill. | shadow-layers / unbounded-caller-outlives-released-dark-job shadow-layers/unboundedCallerSurvivesDarkJobDeadlineTest |
| C54.unowned-caller-releases-slot | An expired dark job can release its capacity while an independently owned unbounded caller source continues. | lateDarkReadCannotStartDecodeOrFillTest: The caller's source settles before its dark job's budget expires and the late C0 read then drains with no decode, fill or detached source; the profile runs one caller at a time and does not model slot reuse or finite-versus-unbounded source budgets. The separate shadow-layers regression and required witness establish slot release with an explicitly unbounded caller by admitting a second same-key dark read. unboundedCallerSurvivesDarkJobDeadlineTest: At the finite60000ms dark-job deadline an explicitly unbounded caller remains pending. A same-key second dark read is admitted, proving release of the old diagnostic slot; the first source later returns its value without late fill, while the second can start its own fill. | shadow-layers / unbounded-caller-outlives-released-dark-job shadow-layers/unboundedCallerSurvivesDarkJobDeadlineTest |
| C53.dark-propagated-timeout | A timeout error returned by the caller source is a dark source failure, distinct from expiration of the shadow job deadline. | darkPropagatedTimeoutIsSourceFailureTest: The single dark caller source rejects its exact controlled nested timeout object at time0. Caller classification remains original source error and the diagnostic verdict is source_error, with no classification/recovery/serialization/write or own deadline event. | shadow-layers / dark-propagated-timeout-is-source-error shadow-layers/darkPropagatedTimeoutIsSourceFailureTest |
| C53.served-propagated-timeout | A timeout error returned by a detached source is a source-error verdict, distinct from expiration of the shadow job deadline. | servedPropagatedTimeoutPreservesHitTest: The detached served-hit source runs with caching disabled and rejects its controlled nested timeout at time0. The caller keeps its already served C0=1 and the job reports source_error, with no write or own job deadline event. | shadow-layers / served-propagated-timeout-preserves-hit shadow-layers/servedPropagatedTimeoutPreservesHitTest |
| C49.local-publication | Dark work never publishes C0 into process-local storage; eligible local publication uses only the caller source result. | darkPresentC0NeverBecomesLocalPublicationTest: With request memo disabled, a present C0=1 cannot satisfy a later dark caller before source settlement; source=2 alone becomes the subsequent local hit. A separate absent-C0 history proves source publication precedes the held shadow fill write and a local hit stops new shadow admission. darkSourcePublishesLocalBeforeShadowWriteTest: With request memo disabled, a present C0=1 cannot satisfy a later dark caller before source settlement; source=2 alone becomes the subsequent local hit. A separate absent-C0 history proves source publication precedes the held shadow fill write and a local hit stops new shadow admission. localPublicationStopsLaterDarkWorkTest: A dark caller publishes its successful source locally before the held fill; a subsequent local hit starts neither another source nor dark read. | shadow-layers / dark-present-c0-never-publishes-local shadow-layers / dark-local-source-publication-stops-later-shadow dark-layers / dark-source-local-publication-stops-job shadow-layers/darkSourcePublishesLocalBeforeShadowWriteTest shadow-layers/darkPresentC0NeverBecomesLocalPublicationTest dark-layers/localPublicationStopsLaterDarkWorkTest |
| C49.request-publication | Dark work never publishes C0 into request memoization; memoization uses only the caller source result. | darkPresentC0NeverBecomesRequestPublicationTest: With local disabled, present C0=1 cannot satisfy a same-scope caller before source settlement; source=2 alone becomes that scope's memo hit. A sibling scope starts an independent source. The absent-C0 history proves request publication precedes held shadow fill. darkSourcePublishesRequestBeforeShadowWriteTest: With local disabled, present C0=1 cannot satisfy a same-scope caller before source settlement; source=2 alone becomes that scope's memo hit. A sibling scope starts an independent source. The absent-C0 history proves request publication precedes held shadow fill. | shadow-layers / dark-present-c0-never-publishes-request shadow-layers / dark-request-source-publication-is-scope-local shadow-layers/darkSourcePublishesRequestBeforeShadowWriteTest shadow-layers/darkPresentC0NeverBecomesRequestPublicationTest |
| C49.job-dedup-keeps-independent-sources | Deduplicating a dark diagnostic job does not coalesce independent ramped-out caller sources. | deduplicatedJobKeepsIndependentCallerSourcesTest: Same-key dark calls with coalesce=false create two independently controlled sources but one C0 read/job. The second settles to 2 without a fill; the owner settles to 1, fills once, and a later serving probe returns 1 while each caller retains its own result. | shadow-layers / dark-job-dedup-preserves-independent-source-values shadow-layers/deduplicatedJobKeepsIndependentCallerSourcesTest |
| C49.no-stale-recovery | A ramped-out caller never serves a dark stale candidate, even when its recovery classifier would allow stale recovery. | darkFailureDoesNotUseEligibleStaleBytesTest: Dark acquisition sees physical C0 exactly F=60000ms old and younger than M=120000ms, with an always-allow recovery classifier. Source rejection preserves that one original error, emits source_error, and performs no classification, deserialization, recovery, or write. | shadow-layers / dark-eligible-stale-c0-never-recovers shadow-layers/darkFailureDoesNotUseEligibleStaleBytesTest |
| C47.recovery-skips-shadow | A recovered value, including absence, does not admit served-hit shadow work. | recoveredStaleHasNoSharedPublication: The stale model keeps a zero-shadow-job projection after recovery but does not model otherwise eligible shadow admission. The fixed selected-shadow/absent-recovery scenario supplies the discriminating implementation check. recoveredAbsenceSkipsSelectedShadowTest: With tracked stale bytes, a selected 100% shadow policy, installed outcome hook and available capacity, source failure recovers the retained value, including absence. Recovery and its same-request memo probe start no diagnostic source/read/job and publish no remote/local value; an independent request repeats source failure and recovery for the absence case. recoveredValueSkipsSelectedShadowTest: With tracked stale bytes, a selected 100% shadow policy, installed outcome hook and available capacity, source failure recovers the retained value, including absence. Recovery and its same-request memo probe start no diagnostic source/read/job and publish no remote/local value; an independent request repeats source failure and recovery for the absence case. | recovery-read / recovered-absence-skips-selected-shadow-and-memoizes recovery-read / recovered-value-skips-selected-shadow-and-memoizes recovery-read/recoveredAbsenceSkipsSelectedShadowTest recovery-read/recoveredValueSkipsSelectedShadowTest |
| C47.coalesced-hit-one-job | Coalesced callers sharing one remote hit admit only one detached shadow source. | coalescedHitAdmitsOneJobTest: Coalesced callers sharing one remote hit admit only one detached shadow source. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | admission / coalesced-hit-one-job admission/coalescedHitAdmitsOneJobTest |
| C52.future-miss-may-fill | A future C0 is a semantic miss; after caller success a dark job may fill from that source subject to its observed fence. | futureDarkAcquisitionReportsOffsetAndFillsMissTest: A future C0 is a semantic miss; after caller success a dark job may fill from that source subject to its observed fence. rollbackMakesTheSeededFrameFutureAndReportsItsOffsetTest: A wall rollback makes a seeded C0 future-dated; the held dark read reports the remote_shadow offset, skips decode and permits a source fill. | shadow / future-dark-c0-fills-without-decoding dark-layers / future-dark-c0-reports-offset-and-fills dark-layers/rollbackMakesTheSeededFrameFutureAndReportsItsOffsetTest |
| C52.expired-miss-may-fill | An expired C0 is a semantic miss; a dark job may fill from the accepted caller source. | expiredC0CanFillAndServeNewValueTest: C0=1 acquired exactly at freshness age60000ms is a semantic miss despite physical presence. Source=2 fills once without decoding old bytes; a later serving probe reads2 and starts no new source. c0AcquisitionsRespectFreshness: At the step that releases a read, a surviving job acquired the frame exactly when it was visible and strictly younger than the freshness at that instant (nonnegative age strictly below the ceiling); later comparison and C1 confirmation do not reclassify the acquired C0. c0AtExactFreshnessBoundaryRefillsTest: A public C1 confirmation completes using retained bytes at age 60000 ms. A subsequent job reacquires the same stored bytes as C0 at exact freshness age 60000 ms, does not decode them, and fills once from the accepted caller source. This checks C0 reacquisition rather than changing the prior job's retained decision. staleVisibleFrameDeclinedByTheDarkReadFillsUnfencedTest: A stale but visible C0 is declined without retaining a fence; invalidation after that read does not stop the captured fill from dispatching and completing. | shadow-layers / expired-c0-miss-fills-source-and-serves-probe dark-layers / stale-visible-dark-c0-fills-unfenced shadow-layers/expiredC0CanFillAndServeNewValueTest shadow/c0AtExactFreshnessBoundaryRefillsTest dark-layers/staleVisibleFrameDeclinedByTheDarkReadFillsUnfencedTest |
| C53.acquired-miss-no-reread | A dark job uses its acquired C0 miss and observed fence without rereading C0 after an external replacement. | acquiredMissDoesNotRereadBeforeFillTest: An absent C0 is acquired, external storage is then seeded to1, and source=2 fills without rereading/reclassifying C0. Read count stays1 through write completion; a later serving probe observes2. | shadow-layers / acquired-c0-miss-does-not-reread-before-fill shadow-layers/acquiredMissDoesNotRereadBeforeFillTest |
| C51.retained-candidate-not-reclassified | An initially accepted C0 remains a comparison candidate after its freshness expires; confirmation checks payload identity. | retainedFreshC0StillComparesAfterFreshnessBoundaryTest: C0 is acquired at age59999ms, then source=2 settles exactly at F=60000ms before the60000ms job deadline. Retained C0=1 is decoded once, one C1 payload read confirms mismatch, caller gets2, and no fill occurs. | shadow-layers / retained-fresh-c0-compares-after-freshness-boundary shadow-layers/retainedFreshC0StillComparesAfterFreshnessBoundaryTest |
| C13.request-last-writer | Disabling coalescing preserves request memoization; independent successful completions replace its value in settlement order. | independentRequestMemoUsesLastCompletionTest: Disabling coalescing preserves request memoization; independent successful completions replace its value in settlement order.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. memoFollowsLatestSuccessfulSettlement: Disabling coalescing preserves request memoization; independent successful completions replace its value in settlement order.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. rejectedIndependentSourceKeepsMemoizedValueTest: A failed independent completion neither replaces nor clears the memoized value: the row keeps the last successful settlement and a later call in the same scope is served from it without a new source. | scope / independent-request-last-completion-probed scope/independentRequestMemoUsesLastCompletionTest scope/rejectedIndependentSourceKeepsMemoizedValueTest |
| C16.runtime-enables-coalescing | Omitted runtime coalesce preserves a configured false default; explicit true replaces that default and enables eligible sharing. | inheritedFalseStartsBothSourcesBeforeSettlementTest: An omitted runtime sharing leaf preserves the configured false baseline: two request callers start independent sources before either settles. runtimeTrueEnablesSharingOverFalseDefaultTest: Explicit runtime coalesce true replaces an operation default of false and enables eligible sharing.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. inheritedFalseKeepsIndependentMemoizingSourcesTest: Omitted runtime coalesce inherits the configured false default; two independent completions retain their own results and memoize the last successful settlement. inheritedDisabledSharingNeverJoins: At each admission with an omitted sharing leaf and configured false baseline, the caller starts independent work instead of joining an existing flight. | runtime-boundaries / runtime-enables-sharing runtime-boundaries / inherited-false-request-last-writer runtime-boundaries/runtimeTrueEnablesSharingOverFalseDefaultTest runtime-boundaries/inheritedFalseKeepsIndependentMemoizingSourcesTest runtime-boundaries/inheritedFalseStartsBothSourcesBeforeSettlementTest |
| C03.late-recovery-publication | Late stale recovery returns to original callers but cannot populate a closed or replacement request scope. | closedRequestCannotReceiveLateRecoveryMemoTest: Late stale recovery returns to original callers but cannot populate a closed or replacement request scope. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. closedContextsStayEmpty: Closing the attached request during held recovery decode permits the caller result but prevents request/local publication, distinguished by a new-scope read. closedRequestCannotReceiveCompressedRecoveryTest: Closing the attached request during held recovery decode permits the caller result but prevents request/local publication, distinguished by a new-scope read. | recovery / closed-recovery-does-not-memoize-another-scope recovery-read / closed-request-recovery-keeps-new-request-cold recovery-read/closedRequestCannotReceiveCompressedRecoveryTest recovery/closedRequestCannotReceiveLateRecoveryMemoTest |
| C54.instance-isolation | Shadow capacity and job identity deduplication apply within each cache instance independently. | capacityIsPerInstance: Shadow capacity and job identity deduplication apply within each cache instance independently. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. fullInstanceDoesNotBlockOtherInstanceTest: Shadow capacity and job identity deduplication apply within each cache instance independently. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. fullMixedInstanceDoesNotBlockAnotherInstanceTest: A served and a dark job fill instance0; its third key is dropped, while the same key on instance1 admits a C0 read. Recorded source contexts distinguish the disabled served source from enabled independent caller sources. sameKeyCallersOnTwoInstancesKeepSeparateFlightsTest: Same-key callers on distinct instances start distinct sources and dark reads; settling one leaves the other pending. | admission / per-instance-deduplication admission / other-instance-full-admission shadow-layers / mixed-shadow-capacity-is-per-instance dark-layers / dark-flights-are-instance-local shadow-layers/fullMixedInstanceDoesNotBlockAnotherInstanceTest admission/fullInstanceDoesNotBlockOtherInstanceTest dark-layers/sameKeyCallersOnTwoInstancesKeepSeparateFlightsTest |
| C18.captured-shadow-admission | Disabling shadow prevents new admission while an already admitted comparison retains its captured policy. | admittedComparisonSurvivesPolicyDisableTest: Disabling shadow prevents new admission while an already admitted comparison retains its captured policy. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. capturedShadowPolicySurvivesPolicyChangeTest: A caller admitted under a selected shadow policy keeps its admission when the policy is disabled before its decode completes, and one admitted under a disabled policy gains none when it is re-enabled: the selection is captured with the read, not read at the hit. | shadow / admitted-job-keeps-shadow-policy admission / accepted-shadow-policy admission/capturedShadowPolicySurvivesPolicyChangeTest |
| C36.independent-invalidation-snapshots | Independent tracked reads acquired before and after invalidation keep their own snapshot and fencing outcomes. | acceptedFreshDecodeSurvivesOtherInvalidationTest: Independent tracked reads acquired before and after invalidation keep their own snapshot and fencing outcomes. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. independentSnapshotsMatchAcquisition: Each independent caller retains its admitted maximum and separately projected read-time payload, timestamp and acquisition wall clock whenever a candidate is retained; callers do not borrow another acquisition. | independent / acquired-fresh-decode-survives-invalidation |
| C55.legacy-reply-normalization | Null, primitive, legacy, and kindless metadata-only replies that are not valid frames normalize to safe misses without trusting stray watermark metadata. | nullReplyRefillsAndIsReadableTest: Null, primitive, obsolete discriminator and kindless replies are semantic misses, permit one refill, and a subsequent public read hits the written value. primitiveReplyRefillsAndIsReadableTest: Null, primitive, obsolete discriminator and kindless replies are semantic misses, permit one refill, and a subsequent public read hits the written value. legacyReplyRefillsAndIsReadableTest: Null, primitive, obsolete discriminator and kindless replies are semantic misses, permit one refill, and a subsequent public read hits the written value. kindlessReplyRefillsAndIsReadableTest: Null, primitive, obsolete discriminator and kindless replies are semantic misses, permit one refill, and a subsequent public read hits the written value. | effects / normalized-reply-allows-refill:1 effects / normalized-reply-allows-refill:2 effects / normalized-reply-allows-refill:4 effects/nullReplyRefillsAndIsReadableTest effects/primitiveReplyRefillsAndIsReadableTest effects/legacyReplyRefillsAndIsReadableTest effects/kindlessReplyRefillsAndIsReadableTest |
| C55.invalid-fence-discarded | Missing, negative, fractional, or unsafe miss watermarks are discarded and cannot authorize fencing metadata. | missingFenceRefillsAndIsReadableTest: Missing, negative, fractional and unsafe fences do not suppress refill; resulting native value is readable on the subsequent call. Valid semantic miss categories are preserved where present. negativeFenceRefillsAndIsReadableTest: Missing, negative, fractional and unsafe fences do not suppress refill; resulting native value is readable on the subsequent call. Valid semantic miss categories are preserved where present. fractionalFenceRefillsAndIsReadableTest: Missing, negative, fractional and unsafe fences do not suppress refill; resulting native value is readable on the subsequent call. Valid semantic miss categories are preserved where present. unsafeFenceRefillsAndIsReadableTest: Missing, negative, fractional and unsafe fences do not suppress refill; resulting native value is readable on the subsequent call. Valid semantic miss categories are preserved where present. | effects / normalized-reply-allows-refill:8 effects / normalized-reply-allows-refill:9 effects / normalized-reply-allows-refill:10 effects / normalized-reply-allows-refill:11 effects/missingFenceRefillsAndIsReadableTest effects/negativeFenceRefillsAndIsReadableTest effects/fractionalFenceRefillsAndIsReadableTest effects/unsafeFenceRefillsAndIsReadableTest |
| C55.valid-fence-independent-of-cause | A valid tracked watermark survives normalization independently of a recognized miss cause and constrains later publication. | validMissWatermarksArePreserved: A valid future fence suppresses serialization despite an absent cause; zero-fence expired metadata permits serialization. Protocol invariants separately require valid metadata retention for semantic misses. absentReplyWithFutureFenceBlocksRefillTest: A tracked absent-reason reply with a valid future fence retains that fence through normalization; the accepted source is served without serialization, and the next public read misses and starts a second source. expiredZeroFenceReplyRefillsAndIsReadableTest: A tracked expired-reason reply with a zero fence is normalized to an expired miss with no retained fence; one source refill is serialized and written, and the next public read hits it without a second source. | effects / normalized-reply-fences-refill:12 effects / normalized-reply-allows-refill:13 effects/absentReplyWithFutureFenceBlocksRefillTest effects/expiredZeroFenceReplyRefillsAndIsReadableTest |
| C55.frame-ignores-miss-metadata | A valid frame without a miss discriminator remains a frame despite stray miss-reason or fence fields. | frameWithoutMissDiscriminatorIgnoresMetadataTest: The scheduled regression asserts the frame is served without a source. Generated reply15 is an additional required input category, not by itself proof that a frame was served. | effects / reply:15 |
| C19.exact-serving-cohort | A serving ramp excludes a key at equality with its cohort sample and includes it just above that sample, independently for each layer. | localCohortEqualityLeavesNoValueForLaterAdmissionTest: A local call at exact cohort equality bypasses storage; the next above-sample call starts a source and remains pending instead of finding a value published by the bypassed call. localCohortEqualityBypassesBeforeAboveSampleCachesTest: One fixed independently published canonical key numerator per serving layer, strict below/equality/above integer sample thresholds bound to floating percentage inputs; full FNV/hash key construction stays W03 wire-vector authority. remoteCohortEqualityBypassesBeforeAboveSampleCachesTest: One fixed independently published canonical key numerator per serving layer, strict below/equality/above integer sample thresholds bound to floating percentage inputs; full FNV/hash key construction stays W03 wire-vector authority. equalAndLowerCohortsNeverTraverse: One fixed independently published canonical key numerator per serving layer, strict below/equality/above integer sample thresholds bound to floating percentage inputs; full FNV/hash key construction stays W03 wire-vector authority. | runtime-boundaries / exact-serving-cohort:local runtime-boundaries / exact-serving-cohort:remote runtime-boundaries/localCohortEqualityBypassesBeforeAboveSampleCachesTest runtime-boundaries/localCohortEqualityLeavesNoValueForLaterAdmissionTest runtime-boundaries/remoteCohortEqualityBypassesBeforeAboveSampleCachesTest |
| C45.compressed-candidate | Retained compressed bytes follow the same recovery and no-shared-publication rules; decompression failure preserves the source error. | recoveredResultsNeverPublishShared: The modeled input domain includes valid/corrupt compressed bytes; retained recovery either serves the decoded value with request-only publication or preserves the indexed original source error. Compression algorithm correctness remains vector/native evidence. compressedRecoveryMemoizesWithoutLocalPublicationTest: The modeled input domain includes valid/corrupt compressed bytes; retained recovery either serves the decoded value with request-only publication or preserves the indexed original source error. Compression algorithm correctness remains vector/native evidence. corruptCompressedRecoveryKeepsOriginalSourceErrorTest: The modeled input domain includes valid/corrupt compressed bytes; retained recovery either serves the decoded value with request-only publication or preserves the indexed original source error. Compression algorithm correctness remains vector/native evidence. untrackedCompressedRecoveryDoesNotWarmLocalTest: The modeled input domain includes valid/corrupt compressed bytes; retained recovery either serves the decoded value with request-only publication or preserves the indexed original source error. Compression algorithm correctness remains vector/native evidence. compressedRecoveryRechecksMaximumAfterDecodeTest: The modeled input domain includes valid/corrupt compressed bytes; retained recovery either serves the decoded value with request-only publication or preserves the indexed original source error. Compression algorithm correctness remains vector/native evidence. | recovery-read / tracked-compressed-recovery-is-request-only recovery-read / corrupt-compressed-recovery-keeps-original-error recovery-read / untracked-compressed-recovery-does-not-warm-local recovery-read / compressed-recovery-crossing-maximum-keeps-original-error recovery-read/compressedRecoveryMemoizesWithoutLocalPublicationTest recovery-read/corruptCompressedRecoveryKeepsOriginalSourceErrorTest recovery-read/untrackedCompressedRecoveryDoesNotWarmLocalTest recovery-read/compressedRecoveryRechecksMaximumAfterDecodeTest |
| C28.encoding-error-suppresses-refill | Unsupported payload encoding is a read failure that suppresses Redis refill for both tracked and untracked calls. | trackedEncodingFailureSuppressesRefillTest: Unsupported encoding is classified after presence/fence checks and denies remote refill; source success remains visible, and untracked local publication remains eligible. untrackedEncodingFailureStillPublishesLocalTest: Unsupported encoding is classified after presence/fence checks and denies remote refill; source success remains visible, and untracked local publication remains eligible. encodingFailedReadLeavesNoCandidateTest: An encoding-failed read retains no recovery snapshot: the source failure that follows is unclassified, completes the caller with the source's own error, reports no recovery label and refills nothing. | recovery-read / tracked-encoding-error-denies-refill-and-local-reuse recovery-read / untracked-encoding-error-denies-refill-keeps-local-reuse recovery-read/trackedEncodingFailureSuppressesRefillTest recovery-read/untrackedEncodingFailureStillPublishesLocalTest recovery-read/encodingFailedReadLeavesNoCandidateTest |
| C22.adapter-frame-expiry | An adapter-returned frame is served through the last fresh millisecond, but at its exact freshness ceiling it is an expired miss that permits source refill and later cache reuse. | frameReplyAtLastFreshMillisecondHitsTest: The queued adapter frame stamped at100000ms is decoded and served at age59999ms, without source, refill or miss diagnostic. staleFrameReplyExpiresRefillsAndIsReadableTest: At age60000ms the queued frame is rejected before decoding with one expired miss and no future offset; source success is serialized, written for60000ms, and reused by a subsequent public call without another source. staleFrameRepliesReportExpired: The independently stated property uses the raw acquired frame stamp, wall sample and monotonic read deadline to require the expired diagnostic for each timely stale queued frame reply. | effects / adapter-frame-last-fresh-millisecond-hits effects / adapter-frame-exact-expiry-refills-and-reuses effects/frameReplyAtLastFreshMillisecondHitsTest effects/staleFrameReplyExpiresRefillsAndIsReadableTest |
| C22.freshness-after-read | Logical remote freshness is evaluated at read settlement, so age accumulated during the bounded read can make a frame stale. | freshnessUsesReadSettlement: Read acquisition samples the settlement wall clock; a frame initially fresh becomes stale during the held read and subsequently recovers after source rejection. freshnessAfterHeldReadTest: Read acquisition samples the settlement wall clock; a frame initially fresh becomes stale during the held read and subsequently recovers after source rejection. heldReadJustBeforeFreshnessBoundaryStillHitsTest: Read acquisition samples the settlement wall clock; a frame initially fresh becomes stale during the held read and subsequently recovers after source rejection. | recovery-read / read-settlement-crosses-freshness-and-recovers recovery-read / read-settlement-before-freshness-hits recovery-read/freshnessAfterHeldReadTest recovery-read/heldReadJustBeforeFreshnessBoundaryStillHitsTest |
| C58.failure-categories | Read, policy, load, dump, and write failures retain their stable phase-specific diagnostic classification while their documented fail-open path continues. Source rejections and deadlines record a fallback diagnostic at the layer running the source while preserving the caller failure. | readFailureKeepsCategoryAndDeniesRefillTest: Each added model regression requires the phase label alongside its source-result and write/no-write consequence. Fixed scenarios additionally check policy-resolution diagnostics. decodeFailureKeepsCategoryAndAllowsRefillTest: Each added model regression requires the phase label alongside its source-result and write/no-write consequence. Fixed scenarios additionally check policy-resolution diagnostics. dumpFailureKeepsCategoryAndSourceValueTest: Each added model regression requires the phase label alongside its source-result and write/no-write consequence. Fixed scenarios additionally check policy-resolution diagnostics. writeFailureKeepsCategoryAndSourceValueTest: Each added model regression requires the phase label alongside its source-result and write/no-write consequence. Fixed scenarios additionally check policy-resolution diagnostics. sourceDeadlineExpiresTheDarkJobAndAttributesToTheLocalLayerTest: A shared source/job deadline ends dark work once, attributes the failed active-local source to local, and permits a subsequent same-scope retry. transientRequestOnlySourceFailureIsAttributedToRequestLayerTest: A transient request with no shared layer attributes its dark source rejection to request_local despite having no persistent model memo slot. | effects / error:cache_read effects / error:serialization_load effects / error:serialization_dump effects / error:cache_write dark-layers / dark-source-deadline-attributed-to-local dark-layers / transient-request-dark-error-uses-request-layer dark-layers/sourceDeadlineExpiresTheDarkJobAndAttributesToTheLocalLayerTest dark-layers/transientRequestOnlySourceFailureIsAttributedToRequestLayerTest |
| C58.request-follower-trail | Request followers report request-local coalescing without repeating lower cache traversal or the leader error trail. | sharedFailureHasOneAttributedErrorTest: Request followers report request-local coalescing without repeating lower cache traversal or the leader error trail. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | scope / one-error-for-request-followers scope/sharedFailureHasOneAttributedErrorTest |
| C58.late-rejection-not-recounted | A source deadline records one failure; a later rejection of the abandoned loader does not emit another fallback failure. | lateSourceCannotRepeatFailureMetricTest: A source deadline records one failure; a later rejection of the abandoned loader does not emit another fallback failure. The cited property covers its bounded modeled clause; exact values, adapter errors and unmodeled combinations retain their separate evidence. | effects / late-rejection-does-not-repeat-error |
| C59.compression-read-telemetry | Previously compressed reads report decompression success or failure even when new compression writes are disabled. | freshCompressedReadReportsDecompressionTest: Previously compressed inputs emit exact decompressed or fallback_raw diagnostics at decode start; later public completion distinguishes successful hit from source fallback while new compression writes remain disabled. corruptCompressedReadReportsRawFallbackTest: Previously compressed inputs emit exact decompressed or fallback_raw diagnostics at decode start; later public completion distinguishes successful hit from source fallback while new compression writes remain disabled. | recovery-read / fresh-compressed-hit-reports-decompression recovery-read / corrupt-compressed-read-reports-fallback-with-source-result recovery-read/freshCompressedReadReportsDecompressionTest recovery-read/corruptCompressedReadReportsRawFallbackTest |
| C60.logging-explicit-off | Explicitly disabling mismatch logging suppresses warnings while preserving a confirmed mismatch verdict. | warningsRequireMismatch: A confirmed mismatch with an explicitly disabled logging flag has no warning. Omitted/default logging and malformed flags have separate named cases. explicitFalseLoggingOverridesEnabledDefaultTest: A logging-enabled fixture receives an explicit false runtime reply before admission. Confirmed mismatch and age metric remain, while warning and configuration-error counts remain zero. | shadow / mismatch-logging:false shadow / explicit-false-shadow-logging-overrides-enabled-default shadow/explicitFalseLoggingOverridesEnabledDefaultTest |
| C40.fenced-candidate | A fenced initial value is not retained or decoded for recovery; an allowed failure remains the original source error. | fencedInitialBytesNeverRecoverTest: A fenced initial value is not retained or decoded for recovery; an allowed failure remains the original source error. fencedFrameNeverBecomesRecoveryCandidateTest: A fenced initial value is not retained or decoded for recovery; an allowed failure remains the original source error. | recovery / fenced-read-does-not-retain recovery/fencedInitialBytesNeverRecoverTest |
| C45.rollback-below-fresh | After retaining stale bytes, wall rollback to a nonnegative age below the fresh ceiling still permits recovery; only future age or the exclusive maximum rejects. | rollbackBelowFreshCeilingStillRecoversTest: After retaining stale bytes, wall rollback to a nonnegative age below the fresh ceiling still permits recovery; only future age or the exclusive maximum rejects. rollbackBelowFreshAgeStillRecoversTest: After retaining stale bytes, wall rollback to a nonnegative age below the fresh ceiling still permits recovery; only future age or the exclusive maximum rejects. rollbackCanRecoverRetainedBytesTest: Direct canonical-rule example accepts nonnegative recovery age below the fresh ceiling. Actual retention followed by rollback is exercised by the profile evidence. | recovery / rollback-below-fresh-age-still-recovers recovery/rollbackBelowFreshCeilingStillRecoversTest |
| C53.dark-read-error-keeps-caller | A failed dark C0 read completes the diagnostic job but an independent caller source can still succeed; no decode or fill follows the failed read. | darkReadErrorCannotReplaceCallerSourceTest: A failed dark C0 read completes the diagnostic job but an independent caller source can still succeed; no decode or fill follows the failed read. unsupportedEncodingFailsTheDarkReadTest: An unsupported frame encoding ends the dark read as redis_error while the caller receives its independently resolved source value. | shadow / dark-read-error-still-allows-source-result dark-layers / unsupported-encoding-ends-dark-read dark-layers/unsupportedEncodingFailsTheDarkReadTest |
| C53.dark-source-error | A rejected dark caller source is preserved as the caller failure, emits source_error, and never decodes or fills C0. | sourceErrorDoesNotDecodePresentDarkBytesTest: A rejected dark caller source is preserved as the caller failure, emits source_error, and never decodes or fills C0. rejectedDarkSourceSeedsNoLayerTest: A rejected dark source returns SOURCE_ERROR, emits source_error and starts no decode or fill; a same-scope retry starts a new source and dark read. | shadow / dark-source-error-never-decodes-or-fills dark-layers / rejected-dark-source-seeds-no-layer dark-layers/rejectedDarkSourceSeedsNoLayerTest |
| C52.fenced-miss-may-fill | A fenced C0 is a semantic miss; a source-success fill may proceed once its own timestamp clears the observed fence, without decoding C0. | fencedDarkBytesCanAdmitNewerFillTest: A fenced C0 is a semantic miss; a source-success fill may proceed once its own timestamp clears the observed fence, without decoding C0. | shadow / fenced-dark-c0-can-fill-after-cutoff |
| C51.fenced-confirmation | A watermark-fenced C1 supersedes an unequal C0/source comparison without repair, warning, or value-age verdict. | fencedConfirmationNeverRepairsTest: A watermark-fenced C1 supersedes an unequal C0/source comparison without repair, warning, or value-age verdict. | shadow / fenced-c1-supersedes-without-repair |
| C51.future-confirmation | A future-dated C1 still participates in payload confirmation after C0 was accepted; identical bytes confirm mismatch without cache repair. | futureConfirmationStillComparesBytesTest: A future-dated C1 still participates in payload confirmation after C0 was accepted; identical bytes confirm mismatch without cache repair. | shadow / future-c1-confirms-payload-without-repair |
| C50.equal-skips-confirmation | A semantic C0/source match emits match without issuing a C1 read or repairing the cache. | binarySnapshotComparesDecodedValueTest: A semantic C0/source match emits match without issuing a C1 read or repairing the cache. darkC0EqualToSourceIsAMatchTest: In the composed shadow-layers profile a dark job whose fresh C0 decodes to the caller source's value ends match after one decode with no confirmation read (the read count stays at the C0 read) and holds no dump; the caller completes with its source value. Public inputs only; no served-hit or repair claim. | shadow / equal-comparison-skips-c1 shadow-layers/darkC0EqualToSourceIsAMatchTest |
| C53.fill-serialization-error | A dark fill serialization failure emits fill_error without dispatching a Redis write and preserves the accepted caller result. | fillSerializationFailureNeverDispatchesWriteTest: A dark fill serialization failure emits fill_error without dispatching a Redis write and preserves the accepted caller result. dumpFaultEndsTheFillWithoutReplacingTheCallerResultTest: A failed held dark dump records fill_error without a remote write and preserves the source result already delivered to the caller. | shadow / fill-serialization-error-preserves-caller dark-layers / held-dark-dump-error-preserves-source dark-layers/dumpFaultEndsTheFillWithoutReplacingTheCallerResultTest |
| C53.fill-write-error | A dispatched dark Redis write failure emits fill_error and preserves the accepted caller result; it does not retry or emit a second verdict. | fillWriteFailurePreservesCallerResultTest: A dispatched dark Redis write failure emits fill_error and preserves the accepted caller result; it does not retry or emit a second verdict. | shadow / fill-write-error-preserves-caller |
| C34.observed-fence-snapshot | A conditional refill uses the miss-time observed fence; later invalidation can fence a dispatched write on subsequent reads without retroactively rewriting that miss. | laterInvalidationDoesNotRewriteMissFenceTest: A conditional refill uses the miss-time observed fence; later invalidation can fence a dispatched write on subsequent reads without retroactively rewriting that miss. laterInvalidationDoesNotRewriteObservedMissFenceTest: A miss captures the absent watermark baseline before invalidation. Source publication still dispatches at the later watermark timestamp; a new request rejects that now-fenced write, proving both captured-refill authority and subsequent fence visibility. staleVisibleFrameDeclinedByTheDarkReadFillsUnfencedTest: A stale but visible C0 is declined without retaining a fence; invalidation after that read does not stop the captured fill from dispatching and completing. | recovery-read / later-invalidation-keeps-captured-miss-fence-new-read-fences-write dark-layers / stale-visible-dark-c0-fills-unfenced recovery-read/laterInvalidationDoesNotRewriteObservedMissFenceTest dark-layers/staleVisibleFrameDeclinedByTheDarkReadFillsUnfencedTest |
| C38.value-work-does-not-extend-marker | Ordinary tracked reads and complete value writes do not create, advance, or extend invalidation watermarks. | readsAndValueWritesDoNotMoveWatermarkTest: This regression checks cutoff preservation only; it does not model marker existence or TTL. The separate recovery-read regressions and required witnesses probe continued marker absence or unchanged cutoff and expiry across ordinary reads and value writes, with real-server protocol integration remaining additional evidence. ordinaryValueWorkDoesNotCreateMarkerTest: External marker cutoff and TTL probes before/after ordinary tracked reads and value writes distinguish missing-marker creation, cutoff movement and lifetime extension. Controlled adapter observation, not a proof of native Redis internals. ordinaryValueWorkDoesNotExtendMarkerTest: External marker cutoff and TTL probes before/after ordinary tracked reads and value writes distinguish missing-marker creation, cutoff movement and lifetime extension. Controlled adapter observation, not a proof of native Redis internals. expiredMarkerIsGoneTest: A marker's lifetime ends at its two-hour floor: the probe reads no marker at that instant and the next invalidation stamps a fresh floor marker at the new cutoff, so an expired marker is neither read nor extended. lapsedMarkerUnfencesTheFrameStampedAtItsCutoffTest: Once a marker's lifetime lapses, the frame stamped exactly at its cutoff is no longer fenced: a tracked read finds it stale under the two-hour freshness and holds no decode, the loader's failure retains it as the recovery candidate, and the held decode serves it with no write, so a lapsed marker fences nothing on the public channels. expiredMarkersFenceNothing: A marker no longer in force fences nothing: its entity's watermark is at the zero baseline once the marker's lifetime lapsed, so only an invalidation, never ordinary work or a lapsed marker, keeps a watermark in force. | recovery-read / ordinary-value-work-preserves-absent-marker recovery-read / ordinary-value-work-preserves-marker-cutoff-and-expiry recovery-read/ordinaryValueWorkDoesNotCreateMarkerTest recovery-read/ordinaryValueWorkDoesNotExtendMarkerTest recovery-read/expiredMarkerIsGoneTest recovery-read/lapsedMarkerUnfencesTheFrameStampedAtItsCutoffTest |
| C51.identical-payload-confirmation | An unequal C0/source comparison is reported as mismatch only when one successful C1 read returns the same payload bytes, including equivalent text/binary representations; the cache is never repaired. | identicalTextAndBinaryBytesConfirmMismatchTest: Shared confirmation rule; source detachment and caller-path differences have separate cases. | shadow / same-c1-bytes-confirm-mismatch |
| C05.request-hit-stops-traversal | A request memo hit skips local and remote traversal and source execution | firstHitStopsLowerTraversal: A request memo hit skips local and remote traversal and source execution. This check covers the bounded model clause: firstHitStopsLowerTraversal. Host representations and other feature combinations retain separate fixed/native evidence. untrackedSourcePublishesToAllParticipatingLayersTest: A request memo hit skips local and remote traversal and source execution. This check covers the bounded model clause: untrackedSourcePublishesToAllParticipatingLayersTest. Host representations and other feature combinations retain separate fixed/native evidence. | layers / request-hit-stops-lower-traversal |
| C05.local-hit-stops-traversal | A local hit skips remote reads and source execution while warming an eligible request memo | firstHitStopsLowerTraversal: A local hit skips remote reads and source execution while warming an eligible request memo. This check covers the bounded model clause: firstHitStopsLowerTraversal. Host representations and other feature combinations retain separate fixed/native evidence. localHitWarmsRequestAndSkipsRemoteTest: A local hit skips remote reads and source execution while warming an eligible request memo. This check covers the bounded model clause: localHitWarmsRequestAndSkipsRemoteTest. Host representations and other feature combinations retain separate fixed/native evidence. runtimeLocalTtlAddsEarlierLayerToRemoteFixtureTest: An earlier local value suppresses remote read/decode and source execution after a runtime TTL overlay adds local serving. localValueSurvivesSourceChangeTest: Two enabled local calls around an external source update return the original value with one local source execution in the introductory profile. No request-memo warming claim. servedLayerValueMatchesCache: After each public local, coalesced or remote call in the introductory profile, the served layer holds exactly the returned value and a semantic miss leaves that layer readable. The receipt reads the input record, not the transition helpers; it makes no claim about request-memo warming or remote read counts. | layers / local-hit-stops-remote-and-source runtime-boundaries/runtimeLocalTtlAddsEarlierLayerToRemoteFixtureTest core/localValueSurvivesSourceChangeTest |
| C16.reenable-default-coalescing | Reenabling a shared serving layer over the disabled baseline retains library coalescing when its leaf is omitted | reenablingDisabledBaselineKeepsDefaultCoalescingTest: Reenabling a shared serving layer over the disabled baseline retains library coalescing when its leaf is omitted. This check covers the bounded model clause: reenablingDisabledBaselineKeepsDefaultCoalescingTest. Host representations and other feature combinations retain separate fixed/native evidence. disabledBaselineRampedUpKeepsDefaultSharingTest: Reenabling a shared serving layer over the disabled baseline retains library coalescing when its leaf is omitted. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | runtime-boundaries / disabled-baseline-default-sharing runtime-boundaries/disabledBaselineRampedUpKeepsDefaultSharingTest |
| C17.explicit-feature-kill-switch | Explicit zero or false runtime feature leaves replace inherited request, recovery, and shadow enablement while preserving omitted coalescing policy | explicitOffReplacesInheritedFeaturesTest: Explicit zero or false runtime feature leaves replace inherited request, recovery, and shadow enablement while preserving omitted coalescing policy. This check covers the bounded model clause: explicitOffReplacesInheritedFeaturesTest. Host representations and other feature combinations retain separate fixed/native evidence. fullFeatureKillSwitchKeepsOmittedSharingAndRetainedMemoTest: Explicit zero or false runtime feature leaves replace inherited request, recovery, and shadow enablement while preserving omitted coalescing policy. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | runtime-boundaries / full-feature-kill-switch runtime-boundaries/fullFeatureKillSwitchKeepsOmittedSharingAndRetainedMemoTest |
| C21.invalid-remote-ttl | Invalid remote TTL preserves valid local serving | invalidRemoteTtlPreservesLocalServingTest: Invalid remote TTL preserves valid local serving. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. | policy / invalid-remote-ttl-preserves-local-hit policy/invalidRemoteTtlPreservesLocalServingTest |
| C21.invalid-local-ramp | Invalid local ramps suppress local caching while a valid remote layer remains usable | invalidLocalRampPreservesRemoteTest: Invalid local ramp preserves valid remote hits. This check covers the bounded model clause: invalidLocalRampPreservesRemoteTest. Host representations and other feature combinations retain separate fixed/native evidence. | policy / invalid-local-ramp-preserves-remote-hit policy/invalidLocalRampPreservesRemoteTest |
| C21.invalid-remote-ramp | Invalid remote ramp preserves valid local hits | invalidRemoteRampPreservesLocalTest: Invalid remote ramp preserves valid local hits. This check covers the bounded model clause: invalidRemoteRampPreservesLocalTest. Host representations and other feature combinations retain separate fixed/native evidence. | policy / invalid-remote-ramp-preserves-local-hit policy/invalidRemoteRampPreservesLocalTest |
| C27.source-error-no-publication | A rejected source preserves its failure and publishes no successful value to participating cache layers | sourceFailureNeverPublishes: A rejected source preserves its failure and publishes no successful value to participating cache layers. This check covers the bounded model clause: sourceFailureNeverPublishes. Host representations and other feature combinations retain separate fixed/native evidence. rejectedSourceNeverPublishesTest: A rejected source preserves its failure and publishes no successful value to participating cache layers. This check covers the bounded model clause: rejectedSourceNeverPublishesTest. Host representations and other feature combinations retain separate fixed/native evidence. storageHoldsAcceptedValuesOnly: The local slot, the remote frame and every memo row hold no value or an accepted one, so a rejected source publishes and memoizes nothing and an error code is never stored. Real local storage remains behind a native exception/clock-failure injection seam; no elapsed-time or concurrent-source claim. sourceFailureKeepsPreviouslyAcceptedStorageTest: Real local storage remains behind a native exception/clock-failure injection seam. Distinct request and transient public probes check the old local value, accepted caller result and request-only memo; read failure remains publication-ineligible after the injected fault is cleared. No elapsed-time or concurrent-source claim. rejectedSourceDoesNotSeedLocalTest: A source rejected on an empty local store seeds nothing: the transient call that follows misses locally, reads remote again and starts its own source, so the rejected result never becomes a local publication. Healthy storage throughout; no memo, elapsed-time or concurrent-source claim. rejectedDarkSourceSeedsNoLayerTest: A rejected dark caller seeds neither request memo nor local storage; the next same-scope call starts a fresh source and dark read. | local-failure / rejected-source-preserves-previous-local-publication dark-layers / rejected-dark-source-seeds-no-layer local-failure/sourceFailureKeepsPreviouslyAcceptedStorageTest local-failure/rejectedSourceDoesNotSeedLocalTest dark-layers/rejectedDarkSourceSeedsNoLayerTest |
| C09.fractional-clock-grid | Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times. | fractionalInsertionExpiresAtWholeMillisecondTest: Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. fractionalConstructionKeepsCommonInstanceGridTest: Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. nonzeroOriginKeepsWholeMillisecondBoundaryTest: Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. integerInsertionRetainsFullTtlTest: Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times.. The deterministic regression checks the public result and subsequent reuse for this bounded fixture. clockIsOnTheGrid: Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times. The clock the layers read is the integer projection of the raw ticks, spelled without the clock module, so a precise-clock substitution violates it. callsServeLiveEntriesOrRunTheSource: Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times. At a call step the caller served its instance's live entry (strictly before the entry's grid expiry) and started no source, or ran its source, returned the offered value and left the entry stamped from this grid instant for the local TTL. publicCallsMatchSources: Local insertion and expiry use the common process monotonic whole-millisecond grid, including fractional insertion times and cache instances constructed at different fractional times. One source per loader, every owned caller completed by its own source's outcome and every entry the value of a source on its instance, so the public observation agrees with the library records. | local-clock / fractional-insertion-expiry local-clock / shared-instance-grid local-clock/fractionalInsertionExpiresAtWholeMillisecondTest local-clock/fractionalConstructionKeepsCommonInstanceGridTest local-clock/nonzeroOriginKeepsWholeMillisecondBoundaryTest local-clock/integerInsertionRetainsFullTtlTest |
| C23.later-dark-budget-origins | A later dark caller and its shadow job receive full budgets from their own starts. | pendingDeadlinesAreFuture: Positive budgets remain strictly in the future after registration; time advancement delivers due work before observation. laterDarkSourceKeepsItsWholeBudgetTest: The caller and dark job start at 10 ms; immediate source success publishes locally for another request scope while the dark read remains held without timing out. | dark-layers / later-dark-source-keeps-own-budget dark-layers/laterDarkSourceKeepsItsWholeBudgetTest |
| C54.later-served-job-budget-origin | A later served-hit shadow job receives its full budget from admission, independent of process uptime. | pendingDeadlinesAreFuture: Positive budgets remain strictly in the future after registration; time advancement delivers due work before observation. laterServedShadowKeepsItsWholeBudgetTest: After admission at 10 ms, source rejection at 11 ms reports source_error and the caller retains its served value. A clock-origin budget would report timeout. | admission / later-served-shadow-keeps-own-job-budget admission/laterServedShadowKeepsItsWholeBudgetTest |