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

Checkpoint composition: evidence scope

A child finishing, a checkpoint draining and the original caller accepting a return are distinct conditions. Start with composition and assumptions and the checkpoint reference.

Inspect the join between procedures

The full profile retains exact caller, transaction, child and receipt identities, plus ordering between payment, instructions, reactions and return. A locally valid child result cannot authorize a different suspended caller. A completion publication must also occur at its designated boundary rather than merely somewhere in the trace.

The selected composed configurations combine these boundaries under explicit finite schedules. Their configured behavior identifies prepared assertion probes, actual reachable-state drivers and additional finite selectors. A shared name or imported definition does not establish that every component branch was reached.

Outer schedules remain assumptions

The model supplies particular procedure adapters, metadata, providers and schedules. These are inspectable inputs, not evidence that a general engine or external scheduler implements them. The selected baseline ends at its recorded composition cutoff; later research work receives no acceptance through this release.

The ordinary results and finite graph comparisons concern exact starting states and labelled transitions within those configurations. They do not prove universal completion or every possible interleaving outside the admitted models.

Read the complete negative trace

The composition control reaches the intended named safety violation. Its large state contains nested catalogs, snapshots, frames and histories. The trace view retains every captured state, edge and typed value through a complete shared pool. A small displayed audit field can help explain the failure, but it is not a substitute for that full capture.

Compare the exact negative configuration and ordinary companion. Observation selectors and deliberately defective variants retain different purposes. Source preservation, branch reachability, finite checking, correspondence and implementation conformance remain separate claims.

Read the composition counterexample

The deliberately defective ref-completion-publication-defective variant stops at captured state 144. One failed conjunct of ACompletionSafety becomes visible by following three fields in qT11:

Captured field

Actual value at state 144

Why it matters

completionCommitCount

1

The one-commit condition applies.

completionEvent.id

2

This identifies the designated completion event.

DOMAIN completionEvents

{2, 3}

The recorded event map has an extra key.

The property requires that domain to equal the singleton {completionEvent.id}, which is {2} in this state. {2, 3} does not satisfy that conjunct. The counterexample therefore does not require the commit counter to become two: its extra recorded publication is enough to violate the named property.

Inspect the complete captured state 144, then its full qT11 value, the designated completion event, and the complete completion-event map. Every other captured field and all earlier states remain available in the same trace.

This reading bridge explains actual retained values from the named defective variant. It is not an ordinary play example, a replacement for the full state, or a new model run.

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-completion-publication-ordinary: 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": "CompletionPublicationVariantMC-ordinary.cfg", "constants": [["AScenario", "\"empty\""], ["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.
Fairness
ASpec == AInit /\ [][ANext]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(ANext)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 204, "generated": 236, "queue": 0}
Configured behavior
ASpec
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["AScenario", "\"empty\""], ["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-completion-publication-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 CompletionPublicationVariantMC-ordinary.cfg CompletionPublicationVariantMC

reference-profile/ref-completion-publication-defective: safety-counterexample; actual TLC exit 12.

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

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

Input revision
2
Evidence class
finite-state-exploration
Failed observation or property
ACompletionSafety
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "CompletionPublicationVariantMC-defective.cfg", "constants": [["AScenario", "\"empty\""], ["AMutation", "\"repeated-completion-publication\""], ["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.
Fairness
ASpec == AInit /\ [][ANext]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(ANext)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 144, "generated": 154, "queue": 0}
Configured behavior
ASpec
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["AScenario", "\"empty\""], ["AMutation", "\"repeated-completion-publication\""], ["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.

Ordinary companion: reference-profile/ref-completion-publication-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-completion-publication-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 CompletionPublicationVariantMC-defective.cfg CompletionPublicationVariantMC

All associated configurations

Result

Class

Outcome

ref-action-completion-reaction

finite-state-exploration

success

ref-action-composition

finite-state-exploration

success

ref-action-cost-reaction

finite-state-exploration

success

ref-additional-checks

prepared-assertions

success

ref-committed-composition

finite-state-exploration

success

ref-completion-order-checks

finite-state-exploration

success

ref-completion-publication-defective

finite-state-exploration

safety-counterexample

ref-completion-publication-ordinary

finite-state-exploration

success

ref-connected-timing

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.