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.

Contract	Job	Governing rule
`DrUSD`	the payment leg	full backing at all times; redemption at par, on demand
`SdrUSD`	the yield leg	pro-rata share; fair-share burn; queue matched to the facility cycle
`FacilityRegistry`	the settlement gate	no settlement before due; append-only receipts
`LiquidationWaterfall`	distribution on failure	holders first, capped at par

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, 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 four contracts implement the token and settlement layer only. Much of what this documentation describes has no Solidity representation whatsoever:

Not on-chain	Where it actually lives
Collateral, pledges, priority, the double-pledge refusal	Lean only — `whr_double_pledge_rejected` and friends
Insurance, reinsurance, recovery and the waterfall of protection	Lean only — `insuranceRecovery`, `stacked_protection_le_loss`
The monitor and its receipt-based verdicts	Lean only — `CorpusLink.lean`
The legal feasibility engine	Lean only — `LegalEngine.lean`
Borrowing base, advance rate, eligibility	Lean only — `Facility.lean`
The entire physical pipeline: production, purchase, custody, transport, assay	Not modelled in Solidity; see the pipeline

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.