Contract architecture

Four contracts, each implementing rules that were proved before they were coded. The test suite is the bridge: every test names the theorem or the sourced provision it discharges.

The design rule

Where the formal development and convenience disagree, the development wins. Two examples worth stating plainly.

The payment leg has no redemption queue and cannot be given one, because the queue is compliant only when scoped to the fund token. A queue on the payment leg would need a regulator extension.

The yield leg's holders bear loss first, because a share is a share. An earlier version of the economic model paid them a fixed yield, which quietly made them creditors and moved the loss to the protocol. The contract implements the share.

Running the suite

cd dore-contracts
yarn install
npx hardhat test

Twenty-four tests, all passing. The names are the specification.

What is tested, and what is not on-chain at all

The suite is 24 Hardhat tests over 476 lines of Solidity — three contracts (DrUSD, SdrUSD, FacilityRegistry), one library (LiquidationWaterfall, exercised through a thin test wrapper), and every test names the Lean theorem or ADGM provision it discharges — so a failing test points at a specific claim made elsewhere on this site rather than at a vague regression.

Covered by tests: the settlement gate refusing early settlement, replay and collection by a non-beneficiary; drUSD backing held exactly across many operations and par redemption with no queue; sdrUSD paying no more than the pro-rata share, pricing a redemption at request time, and making holders bear loss rather than the protocol; a full stake → settle → accrue → queue → claim cycle; and the liquidation waterfall paying holders first, capped at par, conserving the pool exactly.

Now the part that matters more. These three contracts and one library implement the token and settlement layer only. Much of what this documentation describes has no Solidity representation whatsoever:

Three further limits, stated plainly:

• No third-party audit. A passing suite the authors wrote is a strong internal gate and is not an audit.
• Nothing is deployed. There is no deployment script, no network configuration and no address on any chain, testnet included.
• No fuzzing or invariant testing. The tests are example-based. The invariants they check are proved in Lean over all inputs, but the Solidity is checked only at the points the tests visit.

Access control and trust assumptions

There is no access control in any of these contracts. No Ownable, no AccessControl, no role modifiers, no require(msg.sender == …) anywhere in the four sources. Every state-changing function is permissionless as written.

This is disclosed rather than buried because it changes what the test suite means: the tests establish that the logic is correct, not that the authority is constrained.

Two consequences an integrator must not miss:

• reserve in drUSD is a counter, not custody. It moves only when mint and redeem move it. isFullyBacked() is therefore a structural identity in this implementation, not evidence that off-chain assets exist. See verify the reserve for what that does and does not prove.
• nav() <= backing() is a property of the accrueSettled path, not an unconditional invariant, because the bare accrue bypasses the transfer.

Nothing here is deployed, so no value is at risk from the above. It has to be resolved — by adding roles, removing accrue, and driving reserve from an attested feed — before anything is.

Upgradeability, and the absence of a kill switch

There is no proxy, no initializer, no upgradeTo, and no pause anywhere in the sources. The contracts are non-upgradeable by omission rather than by design — nobody chose immutability as a security property; it is simply what you get when no upgrade mechanism is written.

SdrUSD additionally binds three immutable fields in its constructor — the payment-leg address, the facility registry, and the cycle length. Those cannot be changed after deployment by any means.

Two things follow that an integrator or allocator should weigh:

• A defect found after deployment cannot be patched. The remedy would be to deploy new contracts and migrate, with everything that implies for holders.
• There is no emergency stop. No pause, no circuit breaker, no way to halt minting or accrual while a problem is investigated.

Neither is a criticism of the current code, which is a reference implementation that is not deployed. Both are decisions that have to be made deliberately — upgradeable with a timelock and a named authority, or immutable with a migration plan — before anything goes live. Neither decision has been made.