Formal Card-Game Systems
r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope
On this page

Registry and lifecycle: evidence scope

Current availability, a captured ability instance and a detached continuation have different authority. The lifetime lesson and registry reference explain why an earlier successful lookup is insufficient for every later action.

Separate current admission from historical capture

The full profile retains normalized source identities, activity epochs, admission, pending state, loss/restoration and detached continuation. Source and event constructors are typed inputs. The pinned rendering behavior used by selected identity/provenance checks is part of their correspondence scope; it is not a theorem about arbitrary textual encodings.

The selected registry and lifecycle configurations include prepared assertions and actual finite state exploration. Their evidence records name the configured behavior and bounds. A selector-only control does not become a stateful lifecycle execution, and a composition model containing registry state does not automatically qualify every registry branch.

Read supplied facts at their boundary

Definitions, source presence, activity decisions, provider responses, captured frames and historical witnesses have separate roles. A detached instance can retain enough historical context to continue while losing permission to address a retired live object. Pending loss and restoration must be assessed against the actual epoch and source conditions.

The finite checks investigate their selected catalogs, objects, instances and schedules. They do not establish correctness for arbitrary providers or unlimited registry histories.

What the control distinguishes

The family control fails its intended named assertion after one explicit variant change. Its ordinary companion, actual configuration and evidence class identify the supported comparison. A complete typed counterexample retains all values; repeated values are linked through the static value pool rather than truncated.

The source inventory keeps all selected counterparts, with unmeasured branch reachability recorded separately. No full-game implementation, arbitrary-string equivalence or universal activity/lifecycle theorem follows from these results.

Selected results

The records below show an ordinary finite configuration and the explicit control pair where applicable. Each record retains its own class and review status. The full list follows.

reference-profile/ref-action-completion-reaction: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: ASourceSafety, AActionPaymentSafety, ACheckpointSafety, AStepSafety, ACompletionSafety, AHistorySafety, AOuterSafety, AEventuallyReturns.

Input revision
2
Evidence class
finite-state-exploration
Failed observation or property
None; completed check
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "Reactive-completion-reaction.cfg", "constants": [["AScenario", "\"completion-reaction\""], ["AMutation", "\"none\""], ["PaidAmounts", "{ 0 }"], ["PaidMoves", "{ FALSE }"]], "definition_overrides": {}, "fingerprint_polynomial": 0, "finite_domain": "Exact initial-state, constructor and fixture definitions in this hash-bound module closure.", "heap_mib": 512, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
Outer schedules, procedure adapters, provider facts, metadata and exact caller/transaction/receipt identities are the selected finite composition fixtures.; Applicable costs, permissions, allocation and valid candidate/payment witnesses are the exact supplied finite fixtures; no general payment interpreter is supplied.; Registered role/zone/event constructors, normalized source/provenance identities, provider facts and pinned renderer behavior are restricted to the selected finite contexts.; Activity, legality, current-effect, payment and exact caller/child completion witnesses are supplied in the selected model; external ability interpretation is outside scope.
Fairness
ASpec == AInit /\ [][ANext]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(ANext)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 271, "generated": 347, "queue": 0}
Configured behavior
ASpec
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["AScenario", "\"completion-reaction\""], ["AMutation", "\"none\""], ["PaidAmounts", "{ 0 }"], ["PaidMoves", "{ FALSE }"]]
Definition overrides
None
Symmetry
None
State view
None

This evidence applies to the exact configured finite model. It is not an unbounded proof or an implementation conformance result.

Download this package’s source and reproduction bundle.

No counterexample trace was produced.

Reproduce this check and inspect its exact inputs
java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx512m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=ref-action-completion-reaction -Dformalwiki.input=f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -suppressMessages 2216,2217,2218 -metadir states -postCondition FormalWikiTrace!Capture -config Reactive-completion-reaction.cfg ActionCompositionMC

reference-profile/ref-registry-uniqueness-ordinary: success; actual TLC exit 0.

Prepared assertions: the listed calculations passed for these selected inputs; no exhaustive arithmetic theorem is claimed.

Checked properties: SAssertionsSA.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
None; completed check
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "RegistryUniquenessVariantMC-ordinary.cfg", "constants": [["PaidAmounts", "{ 0 , 1 }"], ["PaidMoves", "{ TRUE , FALSE }"]], "definition_overrides": {}, "fingerprint_polynomial": 0, "finite_domain": "Exact initial-state, constructor and fixture definitions in this hash-bound module closure.", "heap_mib": 512, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
Registered role/zone/event constructors, normalized source/provenance identities, provider facts and pinned renderer behavior are restricted to the selected finite contexts.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 11, "generated": 22, "queue": 0}
Configured behavior
SSpecSA
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["PaidAmounts", "{ 0 , 1 }"], ["PaidMoves", "{ TRUE , FALSE }"]]
Definition overrides
None
Symmetry
None
State view
None

This evidence applies to the exact configured finite model. It is not an unbounded proof or an implementation conformance result.

Download this package’s source and reproduction bundle.

No counterexample trace was produced.

Reproduce this check and inspect its exact inputs
java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx512m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=ref-registry-uniqueness-ordinary -Dformalwiki.input=f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -suppressMessages 2216,2217,2218 -metadir states -postCondition FormalWikiTrace!Capture -config RegistryUniquenessVariantMC-ordinary.cfg RegistryUniquenessVariantMC

reference-profile/ref-registry-uniqueness-defective: safety-counterexample; actual TLC exit 12.

Deliberately defective variant: this retained counterexample belongs to the named negative control.

Checked properties: SAssertionsSA.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
SAssertionsSA
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "RegistryUniquenessVariantMC-defective.cfg", "constants": [["PaidAmounts", "{ 0 , 1 }"], ["PaidMoves", "{ TRUE , FALSE }"], ["CatalogValidSA <- DefectBodyRegistryUniquenessVariant"]], "definition_overrides": {"CatalogValidSA": "DefectBodyRegistryUniquenessVariant"}, "fingerprint_polynomial": 0, "finite_domain": "Exact initial-state, constructor and fixture definitions in this hash-bound module closure.", "heap_mib": 512, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
Registered role/zone/event constructors, normalized source/provenance identities, provider facts and pinned renderer behavior are restricted to the selected finite contexts.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
null
Configured behavior
SSpecSA
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["PaidAmounts", "{ 0 , 1 }"], ["PaidMoves", "{ TRUE , FALSE }"], ["CatalogValidSA <- DefectBodyRegistryUniquenessVariant"]]
Definition overrides
{"CatalogValidSA": "DefectBodyRegistryUniquenessVariant"}
Symmetry
None
State view
None

This evidence applies to the exact configured finite model. It is not an unbounded proof or an implementation conformance result.

Download this package’s source and reproduction bundle.

Ordinary companion: reference-profile/ref-registry-uniqueness-ordinary.

Reproduce this check and inspect its exact inputs
java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx512m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=ref-registry-uniqueness-defective -Dformalwiki.input=f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -suppressMessages 2216,2217,2218 -metadir states -postCondition FormalWikiTrace!Capture -config RegistryUniquenessVariantMC-defective.cfg RegistryUniquenessVariantMC

All associated configurations

Result

Class

Outcome

ref-action-completion-reaction

finite-state-exploration

success

ref-action-cost-reaction

finite-state-exploration

success

ref-activity-checks

finite-state-exploration

success

ref-detached-checks

finite-state-exploration

success

ref-pending-checks

finite-state-exploration

success

ref-registry-availability

finite-state-exploration

success

ref-registry-checks

prepared-assertions

success

ref-registry-composition

finite-state-exploration

success

ref-registry-uniqueness-defective

prepared-assertions

safety-counterexample

ref-registry-uniqueness-ordinary

prepared-assertions

success

Follow an associated result for its exact source, configuration, bounds, warnings, complete trace when one exists, and reproduction bundle. An association identifies scope; it does not measure individual source-branch reachability.