Daml design-to-test proof map

Use this page when a design statement says “proven by.” Each row links the on-ledger choice to the smallest Daml Script that demonstrates the stated property and gives a focused command. Run commands from trading-tests/.

cd trading-tests
dpm test -p <exact-test-name>

Read the fixture before trusting the claim

The repository has two kinds of Daml fixture:

The four *WorkflowTests.daml suites use MockRegistry. They prove DEX choice choreography, authority, contract consumption/recreation, and the allocation specification passed to settlement. They do not prove real holding balances.
Rows that claim real value movement point to suites using CantonDex.Registry.V2 holdings, including PoolLiquidityRulesTests.daml, PoolRoundingTests.daml, PoolStateInvariantTests.daml, RealRegistryDvpTests.daml, RegistryConservationTests.daml, RfqSettlementTests.daml, and the real-value lifecycle tests. These can prove locked backing, exact balance movement, release, and conservation in Daml Script.

Neither fixture starts a Canton participant or drives the HTTP API, browser, or external wallet. Those are separate integration proofs.

Pair listing metadata

Source: DexPair and its operator-controlled update choices.

Claim	Executable proof	Focused command
Fee model, active flag, trading mode, and readers recreate one successor listing and preserve unrelated fields.	`testDexPairLifecycleUpdates`	`dpm test -p testDexPairLifecycleUpdates`
The registry admin observes the pair but cannot exercise the operator-controlled update.	`testDexPairUpdatesRequireOperator`	`dpm test -p testDexPairUpdatesRequireOperator`
Maker/taker fee counters accumulate the configured arithmetic; no test claims those counters move or collect assets.	`testDexPairRecordsMatchedTradeFees`	`dpm test -p testDexPairRecordsMatchedTradeFees`

active and tradingMode are not settlement gates in this reference. That is a dependency fact visible in the source: PoolRules and OrderMatchExecution do not fetch or accept a DexPair contract. The tests above intentionally prove listing behavior only; do not cite them as pause/enforcement tests.

AMM pool

Core sources:

pricing and ratio math — ratioMatchedDeposit and constantProductOut;
exact quote construction and swap — PoolRules_RequestSwap, PoolRules_Swap;
add/remove DvP — PoolLiquidityRules_SettleAddLiquidity, PoolLiquidityRules_SettleRemoveLiquidity;
real allocation and batch implementation — AllocationFactory, SettlementFactory.

Claim	Executable proof	Focused command
Swap output rounds down and does not reduce `x*y` through decimal overpayment.	`testSwapOutputRoundsDownToKeepConstantProduct`	`dpm test -p testSwapOutputRoundsDownToKeepConstantProduct`
The Daml-built request specification reaches `PoolRules_Swap` and its mock settlement choice against the same bound state and slices.	`testPoolSwapViaRequestSwap`	`dpm test -p testPoolSwapViaRequestSwap`
A context-requiring V2 registry consumes actual trader backing and creates the output holding; a changed signed output is rejected.	`testRealRegistryDvpSwapSettles`	`dpm test -p testRealRegistryDvpSwapSettles`
A stale add-liquidity quote cannot settle against a successor pool state.	`testStaleQuoteRejected`	`dpm test -p testStaleQuoteRejected`
Add liquidity moves real base/quote backing and mints real LP holdings in one DvP flow.	`testDvpAddLiquidity`	`dpm test -p testDvpAddLiquidity`
Off-ratio excess is returned rather than donated or used to mint shares.	`testDvpAddOffRatioRefundsExcess`	`dpm test -p testDvpAddOffRatioRefundsExcess`
Complete LP redemption drains multiple slices, returns real assets, burns every LP holding, and changes state to `Unfunded`.	`testDvpMultiSliceRemove`	`dpm test -p testDvpMultiSliceRemove`
Pool initialization, pause, and resume are actual state transitions; pause rejects a swap and resume preserves reserve and LP-supply accounting.	`testPoolFullLifecycle`	`dpm test -p testPoolFullLifecycle`
Aggregate reserves equal the active slice sums after add, swap, and complete remove.	`testReconcileAfterAddSwapRemove`	`dpm test -p testReconcileAfterAddSwapRemove`
Liquidity settlement requires both operator and LP registrar authority.	`testSettleRequiresCoControl`	`dpm test -p testSettleRequiresCoControl`

Resting orders

Source path: OrderFundingRequest_Bind → Order_Fund → OrderMatchExecution_Execute or Order_Cancel.

Claim	Executable proof	Focused command
Trader intent becomes an operator-bound pending order, then a trader-authored allocation is attached to it.	`testOrderFundingFlow`	`dpm test -p testOrderFundingFlow`
A match outside either signed limit fails.	`testOrderMatchEnforcesLimitPrice`	`dpm test -p testOrderMatchEnforcesLimitPrice`
Settlement and both partial-order roll-forwards occur atomically.	`testOrderMatchRollsOrdersForwardAtomically`	`dpm test -p testOrderMatchRollsOrdersForwardAtomically`
A real partial fill can spend only the funding budget carried into its next allocation iteration.	`testPartialFillUsesRolledFundingBudget`	`dpm test -p testPartialFillUsesRolledFundingBudget`
Cancelling a funded order consumes the real allocation and returns its locked holding unlocked.	`testOrderCancelReleasesRealFunding`	`dpm test -p testOrderCancelReleasesRealFunding`
Trader controls pre-bind cancel; operator controls reject.	`testOrderFundingRequestCancelAndRejectAuthority`	`dpm test -p testOrderFundingRequestCancelAndRejectAuthority`
Operator can abort an unexecuted match proposal without touching referenced orders or allocations.	`testOrderMatchExecutionAbort`	`dpm test -p testOrderMatchExecutionAbort`

RFQ and OTC

Source path: Rfq_Accept creates a MatchedTrade; MatchedTrade_RequestAllocations and MatchedTrade_Settle move its value, while MatchedTrade_Cancel is the abandoned-trade exit.

Claim	Executable proof	Focused command
RFQ accept ranks quotes and records a policy receipt on the resulting trade; it does not move balances yet.	`testRfqAcceptProducesMatchedTradeWithReceipt`	`dpm test -p testRfqAcceptProducesMatchedTradeWithReceipt`
Accepted RFQ terms settle against real holdings with exact balance deltas and no stranded locks.	`testRfqBuySettlesAgainstRealHoldings`	`dpm test -p testRfqBuySettlesAgainstRealHoldings`
The inherited RFQ deadline blocks later settlement; the failed transaction leaves the allocations and locked funds unchanged.	`testExpiryBetweenAcceptAndSettleBlocksTheSettle`	`dpm test -p testExpiryBetweenAcceptAndSettleBlocksTheSettle`
A cross-admin OTC trade uses per-admin batches but remains one atomic Daml transaction.	`testMatchedTradeSettlesPerAdminLegSubsets`	`dpm test -p testMatchedTradeSettlesPerAdminLegSubsets`
Cancelling a proposed trade archives its requests/allocations and returns real sender backing without executing the leg.	`testMatchedTradeCancelReleasesRealFunding`	`dpm test -p testMatchedTradeCancelReleasesRealFunding`
Trader controls RFQ cancellation; dealer controls quote withdrawal.	`testRfqCancelAndQuoteWithdrawAuthority`	`dpm test -p testRfqCancelAndQuoteWithdrawAuthority`

Token Standard safety properties used by every surface

Claim	Executable proof	Focused command
Executor-supplied extra legs cannot exceed locked allocation backing.	`testExtraLegBeyondBackingRejected`	`dpm test -p testExtraLegBeyondBackingRejected`
Roll-forward carries actual locked backing, not an accounting-only budget.	`testRollForwardCarriesLockedBacking`	`dpm test -p testRollForwardCarriesLockedBacking`
An uncommitted allocation is withdrawable only by its authorizer.	`testUncommittedAllocationWithdrawsOnlyAsAuthorizer`	`dpm test -p testUncommittedAllocationWithdrawsOnlyAsAuthorizer`
A committed allocation is authorizer-withdrawable after its deadline, but not before.	`testCommittedAllocationWithdrawsOnlyAfterDeadline`	`dpm test -p testCommittedAllocationWithdrawsOnlyAfterDeadline`
A deadline-free committed pool allocation is not unilaterally withdrawable.	`testCommittedAllocationWithoutDeadlineCannotBeWithdrawn`	`dpm test -p testCommittedAllocationWithoutDeadlineCannotBeWithdrawn`

Run by module, then run everything

cd trading-tests
dpm test --files CantonDex/Tests/DexPairTests.daml
dpm test --files CantonDex/Tests/LifecycleChoiceTests.daml
dpm test --files CantonDex/Tests/PoolLiquidityRulesTests.daml
dpm test --files CantonDex/Tests/RealRegistryDvpTests.daml
dpm test

The final command is the release check. A focused test explains one invariant; the complete suite catches interactions between workflows.

Where to read next: Builder guide · Workflow design · Testing reference