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

Schema and setup: evidence scope

A well-shaped metadata row does not by itself create a legal starting game. The setup lesson introduces the records, areas and actors. The characteristics and zones entries explain how consumers interpret those values.

Supplied inputs stay part of the contract

Canonical names, numeric parts, subtype sets, metadata tables, deck order and profile choices require well-shaped inputs. A projection that reads a field is not a validator for every possible TLA+ value. Named role, area and event constructors describe the selected finite profile; they are not an unrestricted text parser.

Absent numbers, present zeroes and values supplied in context remain different cases. Concealed location and face information constrain what a participant can inspect. Internal metadata availability does not grant observation rights.

What the control distinguishes

The schema/setup control changes one named rule in an explicit variant and is admitted only when the intended assertion fails. Follow its ordinary companion and definition override. Prepared assertions demonstrate the listed examples; transition models support only their configured reachable states.

The scope inventory retains every selected source counterpart and records unmeasured branch reachability separately. These results do not establish arbitrary deck construction, every possible metadata table, a complete setup implementation or general information-flow security.

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-setup-checks: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: SetupMCType, SetupMCConservation, SetupMCDecisionOrder, SetupMCBothHandsBeforeRedraw, SetupMCGameStartsLast, SetupMCFinished, SetupMCEventuallyDone.

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": "SetupChecksMC.cfg", "constants": [], "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
Object identifiers, ownership/control, relocation and visibility inputs are well-shaped finite records in this profile; general information noninterference is outside scope.; The selected finite metadata, role, zone, face and setup constructors are supplied exactly; arbitrary strings or metadata tables are outside this checking scope.
Fairness
SetupMCSpec == /\ SetupMCInit /\ [][SetupMCNext]_setupVars /\ WF_setupVars(SetupMCProgress)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 134, "generated": 170, "queue": 0}
Configured behavior
SetupMCSpec
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[]
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-setup-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 SetupChecksMC.cfg SetupChecksMC

reference-profile/ref-type-ownership-ordinary: success; actual TLC exit 0.

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

Checked properties: Block3Assertions.

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": "TypeOwnershipVariantMC-ordinary.cfg", "constants": [], "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
The selected finite metadata, role, zone, face and setup constructors are supplied exactly; arbitrary strings or metadata tables are outside this checking scope.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 10, "generated": 20, "queue": 0}
Configured behavior
Spec3
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[]
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-type-ownership-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 TypeOwnershipVariantMC-ordinary.cfg TypeOwnershipVariantMC

reference-profile/ref-type-ownership-defective: safety-counterexample; actual TLC exit 12.

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

Checked properties: Block3Assertions.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
Block3Assertions
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "TypeOwnershipVariantMC-defective.cfg", "constants": [["BarrierInstructionOwnerKindValid <- DefectBodyTypeOwnershipVariant"]], "definition_overrides": {"BarrierInstructionOwnerKindValid": "DefectBodyTypeOwnershipVariant"}, "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
The selected finite metadata, role, zone, face and setup constructors are supplied exactly; arbitrary strings or metadata tables are outside this checking scope.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
null
Configured behavior
Spec3
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["BarrierInstructionOwnerKindValid <- DefectBodyTypeOwnershipVariant"]]
Definition overrides
{"BarrierInstructionOwnerKindValid": "DefectBodyTypeOwnershipVariant"}
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-type-ownership-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-type-ownership-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 TypeOwnershipVariantMC-defective.cfg TypeOwnershipVariantMC

All associated configurations

Result

Class

Outcome

ref-definition-checks

prepared-assertions

success

ref-location-checks

prepared-assertions

success

ref-schema-checks

prepared-assertions

success

ref-setup-checks

finite-state-exploration

success

ref-type-checks

prepared-assertions

success

ref-type-ownership-defective

prepared-assertions

safety-counterexample

ref-type-ownership-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.