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

Objects and lifetime: evidence scope

Physical identity, a current object occurrence and a historical reference have different lifetimes. The identity lesson makes that distinction with two items. The full reference also retains control, counters, hosting, movement and observation boundaries; the small teaching model does not discharge those contracts.

Preserve the identity at each boundary

An object identifier can be retired while the physical card remains. A later occurrence can have a successor relation without becoming the target of every earlier instruction. Current controller, owner and effect executor are separate inputs. A move can also preserve an occurrence when its exact location/visibility conditions permit that behavior.

The selected full-profile checks investigate their configured combinations of these fields. Inspect the actual source and bounds: a finite fixture over a prepared relocation is a different class of evidence from exploring an entire relocation protocol.

What the controls distinguish

The identity controls deliberately change an occurrence/reference rule and fail the intended named property. The tutorial’s implicit-follow variant redirects a target without the explicit lineage update. That failure illustrates its own narrow invariant; it does not establish all hosting, visibility or controller behavior in the full reference.

Other checks retain stationary objects, historical records and allocation bounds. A successful check is tied to its exact initial state and permitted actions, including the choice to disable terminal deadlock reporting where an exhausted finite scenario is expected.

Observation is a separate claim

An internal object record can contain information that a participant is not permitted to inspect. Current visibility, historical knowledge and information projection must be read in their own contexts. The existence of a concealed-state field is not a hidden-information noninterference proof.

The source mapping and selected finite comparisons preserve the observed profile distinctions. Generic identifiers, histories, provider inputs and branches outside the explored bounds remain explicit limitations. No complete engine or arbitrary object-lifetime 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-control-checks: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, PhysicalUniqueness, HostIntegrity, ControlAssertions, ControlCompleted.

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": "ControlChecksMC.cfg", "constants": [["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- ControlCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"]], "definition_overrides": {"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "ControlCommands", "InitialState": "DummyInitial"}, "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
Object identifiers, ownership/control, relocation and visibility inputs are well-shaped finite records in this profile; general information noninterference is outside scope.
Fairness
ControlSpec == ControlInit /\ [][ControlNext]_mcvars /\ WF_pc(pc = 0 /\ pc' = 1)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 14, "generated": 25, "queue": 0}
Configured behavior
ControlSpec
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- ControlCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"]]
Definition overrides
{"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "ControlCommands", "InitialState": "DummyInitial"}
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-control-checks -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 ControlChecksMC.cfg ControlChecksMC

reference-profile/ref-identity-renewal-ordinary: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, PhysicalUniqueness, HostIntegrity, RuntimeAssertions, PureRuntimeContracts, Completed.

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": "IdentityRenewalVariantMC-ordinary.cfg", "constants": [["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- NoCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"], ["mcvars <- ControlFirstVariables"]], "definition_overrides": {"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "NoCommands", "InitialState": "DummyInitial", "mcvars": "ControlFirstVariables"}, "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
Object identifiers, ownership/control, relocation and visibility inputs are well-shaped finite records in this profile; general information noninterference is outside scope.
Fairness
SpecMC == InitMC /\ [][NextMC]_mcvars /\ WF_mcvars(AdvanceMC)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 66, "generated": 92, "queue": 0}
Configured behavior
SpecMC
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- NoCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"], ["mcvars <- ControlFirstVariables"]]
Definition overrides
{"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "NoCommands", "InitialState": "DummyInitial", "mcvars": "ControlFirstVariables"}
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-identity-renewal-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 IdentityRenewalVariantMC-ordinary.cfg IdentityRenewalVariantMC

reference-profile/ref-identity-renewal-defective: safety-counterexample; actual TLC exit 12.

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

Checked properties: TypeOK, PhysicalUniqueness, HostIntegrity, RuntimeAssertions, PureRuntimeContracts, Completed.

Input revision
2
Evidence class
finite-state-exploration
Failed observation or property
RuntimeAssertions
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "IdentityRenewalVariantMC-defective.cfg", "constants": [["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- NoCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"], ["Relocate <- DefectBodyIdentityRenewalVariant"], ["mcvars <- ControlFirstVariables"]], "definition_overrides": {"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "NoCommands", "InitialState": "DummyInitial", "Relocate": "DefectBodyIdentityRenewalVariant", "mcvars": "ControlFirstVariables"}, "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
Object identifiers, ownership/control, relocation and visibility inputs are well-shaped finite records in this profile; general information noninterference is outside scope.
Fairness
SpecMC == InitMC /\ [][NextMC]_mcvars /\ WF_mcvars(AdvanceMC)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 33, "generated": 33, "queue": 25}
Configured behavior
SpecMC
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- NoCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"], ["Relocate <- DefectBodyIdentityRenewalVariant"], ["mcvars <- ControlFirstVariables"]]
Definition overrides
{"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "NoCommands", "InitialState": "DummyInitial", "Relocate": "DefectBodyIdentityRenewalVariant", "mcvars": "ControlFirstVariables"}
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-identity-renewal-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-identity-renewal-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 IdentityRenewalVariantMC-defective.cfg IdentityRenewalVariantMC

All associated configurations

Result

Class

Outcome

ref-control-checks

finite-state-exploration

success

ref-hosting-checks

finite-state-exploration

success

ref-identity-renewal-defective

finite-state-exploration

safety-counterexample

ref-identity-renewal-ordinary

finite-state-exploration

success

ref-runtime-checks

finite-state-exploration

success

ref-setup-checks

finite-state-exploration

success

ref-visibility-checks

finite-state-exploration

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.