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

Costs and payment: evidence scope

A final amount, an admitted payment and a completed procedure answer different questions. The payment lesson starts with one wallet and one attempt. The cost reference explains the arithmetic. This page concerns the larger reference profile as well as that instructional specialization.

The full profile retains signed intermediate amounts, a single final floor, allocation and permission inputs, atomic commitment, and a barrier before the waiting procedure can continue. A result about a pure cost expression does not establish the correctness of an effect interpreter or a resource provider.

Read the ordinary result with its configured behavior

Some selected checks evaluate prepared records or calculations and then stutter. Others explore reachable protocol states. Inspect the evidence class and configured specification for each result. A prepared arithmetic check can discriminate a final floor from an early floor without being an exhaustive theorem over every integer or modifier sequence.

Payment and completion models also depend on explicit boundaries: which units are available, which permissions authorize spending, which transaction is committing, and what completion witness the caller accepts. The selected finite values and provider contracts belong to the result. They do not authorize a different currency, allocation policy or outer schedule.

What the control distinguishes

The cost control removes the final floor in its named variant. Its intended assertion failure shows sensitivity to that change for the selected inputs. Delayed-use teaching controls answer a different question: whether commitment records use before completion. Legal payment witnesses use an observation condition to stop after an ordinary execution; that condition is not a correctness requirement of the payment system.

Inspect the exact definition override and ordinary companion before comparing outcomes. A syntax error, unexpected warning or missing capture cannot substitute for the named semantic failure.

Limits that remain visible

The public source preserves the selected contracts. A family association does not establish that every branch or parameter domain was exercised. Unmeasured branch reachability is recorded separately from source preservation. General interpretation of cost text, unrestricted resource providers, implementation conformance and unbounded termination require their own evidence.

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-cost-clamp-ordinary: success; actual TLC exit 0.

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

Checked properties: AllAssertions.

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": "CostClampVariantMC-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
Applicable costs, permissions, allocation and valid candidate/payment witnesses are the exact supplied finite fixtures; no general payment interpreter is supplied.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 1, "generated": 2, "queue": 0}
Configured behavior
Spec
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-cost-clamp-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 CostClampVariantMC-ordinary.cfg CostClampVariantMC

reference-profile/ref-cost-clamp-defective: safety-counterexample; actual TLC exit 12.

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

Checked properties: AllAssertions.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
AllAssertions
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "CostClampVariantMC-defective.cfg", "constants": [["ModifiedCost <- DefectBodyCostClampVariant"]], "definition_overrides": {"ModifiedCost": "DefectBodyCostClampVariant"}, "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
Applicable costs, permissions, allocation and valid candidate/payment witnesses are the exact supplied finite fixtures; no general payment interpreter is supplied.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
null
Configured behavior
Spec
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["ModifiedCost <- DefectBodyCostClampVariant"]]
Definition overrides
{"ModifiedCost": "DefectBodyCostClampVariant"}
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-cost-clamp-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-cost-clamp-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 CostClampVariantMC-defective.cfg CostClampVariantMC

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-commitment-publication

finite-state-exploration

success

ref-committed-composition

finite-state-exploration

success

ref-cost-clamp-defective

prepared-assertions

safety-counterexample

ref-cost-clamp-ordinary

prepared-assertions

success

ref-definition-checks

prepared-assertions

success

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