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

Object operations and instructions: evidence scope

Two operations can lead to the same area while differing in identity renewal, permission, cost or event publication. The operation lesson and instruction reference explain those distinctions before the evidence is assessed.

Inspect the actual operation

The full reference separates admission, payment, state change, child procedures and completion. A move, deployment, retirement or transformation can preserve different fields and require different authority. An instruction’s caller cannot resume merely because one visible object has arrived at its destination.

Prepared operation assertions and finite procedure drivers retain different evidence classes. Read the checked property and exact selected source; an association with this family is not a statement that every instruction was executed.

A retained warning narrows the result

One prepared fixture retains a checker warning that an EXCEPT update targets an absent field. That update is a no-op in the selected value. It cannot count as successful mutation sensitivity for that field. The warning is retained with its result, and the independent source review records the limitation.

The separate family negative control changes a payment-admission guard and reaches its intended assertion failure. It does not rely on the no-op update as its discriminating mutation. Compare the named override and ordinary companion rather than treating every failed or warning-bearing attempt as interchangeable.

Supplied semantics remain explicit

Object and metadata validity, legal destinations, applicable permissions, actual payments and instruction receipts are supplied at defined boundaries. The selected checks investigate only the configured finite combinations. They do not establish a general prose interpreter, arbitrary card effects, complete runtime support or universal termination.

Every selected source counterpart remains available for inspection. Unmeasured branch reachability is recorded separately from preserved source and finite graph correspondence.

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

Completed finite check: no counterexample trace was produced.

Checked properties: ProceduresInvariant8, EventuallyReturns8.

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": "OperationProceduresMC.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
Permission, destination, effect, candidate-state and completion witnesses are supplied at their documented boundaries; an operation source listing is not a general interpreter.
Fairness
SpecProcedures8 == InitProcedures8 /\ [][NextProcedures8]_q8 /\ WF_q8(NextProcedures8)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 2816, "generated": 3008, "queue": 0}
Configured behavior
SpecProcedures8
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-operation-procedures -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 OperationProceduresMC.cfg OperationProceduresMC

reference-profile/ref-operation-admission-ordinary: success; actual TLC exit 0.

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

Checked properties: Block8Assertions.

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": "OperationAdmissionVariantMC-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
Permission, destination, effect, candidate-state and completion witnesses are supplied at their documented boundaries; an operation source listing is not a general interpreter.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 8, "generated": 16, "queue": 0}
Configured behavior
Spec8
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-operation-admission-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 OperationAdmissionVariantMC-ordinary.cfg OperationAdmissionVariantMC

reference-profile/ref-operation-admission-defective: safety-counterexample; actual TLC exit 12.

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

Checked properties: Block8Assertions.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
Block8Assertions
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "OperationAdmissionVariantMC-defective.cfg", "constants": [["PayActivation8 <- DefectBodyOperationAdmissionVariant"]], "definition_overrides": {"PayActivation8": "DefectBodyOperationAdmissionVariant"}, "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
Permission, destination, effect, candidate-state and completion witnesses are supplied at their documented boundaries; an operation source listing is not a general interpreter.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
null
Configured behavior
Spec8
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["PayActivation8 <- DefectBodyOperationAdmissionVariant"]]
Definition overrides
{"PayActivation8": "DefectBodyOperationAdmissionVariant"}
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-operation-admission-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-operation-admission-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 OperationAdmissionVariantMC-defective.cfg OperationAdmissionVariantMC

All associated configurations

Result

Class

Outcome

ref-operation-admission-defective

prepared-assertions

safety-counterexample

ref-operation-admission-ordinary

prepared-assertions

success

ref-operation-checks

prepared-assertions

success

ref-operation-procedures

finite-state-exploration

success

ref-retirement-checks

finite-state-exploration

success

ref-target-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.