Examples: HTLC and Linear Vesting

The Scalus repository has suites of proofs about four of its example validators. Two of them show the two ways to use a Lean workspace:

The other two are PaymentSplitterVerificationTest and MintingPolicyVerificationTest, for the one-shot minting policy.

Run Them

From a checkout of the Scalus repository, with elan and Z3 on the PATH (nix develop has both):

# Once, and after a change of the Lean sources: Scalus's Lean library, with Blaster and PlutusCore
(cd scalus-verification/src/main/lean && lake build)
# The vesting example's workspace, which shares the library's packages: seconds
(cd scalus-examples/jvm/src/test/lean/LinearVesting && lake build)
 
sbt "scalusExamplesJVM/verify scalus.examples.htlc.HtlcVerificationTest"
sbt "scalusExamplesJVM/verify scalus.examples.vesting.VestingVerificationTest"

With the kept results committed beside each suite, a run asks Lean only what changed, and takes about the time of compiling the examples. Proving everything again (SCALUS_KEPT_RESULTS=recalculate) takes about 2 minutes for vesting and 8 for HTLC.

HTLC

The hashed timelock contract  locks funds for a receiver who reveals a secret before a timeout, and lets the committer take them back after it. The suite states every rule of every script context the ledger can pass the validator (forAllData[ScriptContext]), with what it is about as a premise.

Proved of every script context, with no limit on its inputs, outputs or signatures:

• what the validator rejects before it reads the transaction: a spend of an output without a datum, any purpose but spending, a redeemer of neither action;
• a refund is rejected unless its validity range starts at the timeout or later (Your First Proof builds this one);
• a reveal is rejected unless its validity range ends by the timeout;
• an accepted reveal ends before any accepted refund begins, so there is no time at which both are valid.

The validator decides these by the time, before it searches the signatories, so Lean decides them for every context.

Proved of the contexts of at most two signatures. The rules that the validator decides by searching the signatories are stated of every context too, but Lean does not finish them there: those tests are tagged Unfinished. Each is stated again of the contexts of at most two signatures, with _limited in its name, where Lean proves it (Tuning Your Proof shows how):

• nobody but the committer refunds, and from the timeout on the committer can;
• nobody but the receiver reveals, a reveal of what is not a preimage is rejected, and up to the timeout the receiver can reveal;
• whether a bound of the validity range is inclusive does not matter.

Each property has a negative control beside it, and sample spends, decided by running the validator with the real hash, show that it accepts a refund and a reveal.

The suite states what is not proved, in its header:

• Nothing about the hash. To the solver, sha3_256 is a function it knows nothing about. So a proof holds whatever the function is, and says nothing about how hard a preimage is to find.
• Where the funds go. The validator asks for a signature and constrains no output.
• The published script’s bytes. The validator is compiled with the tactic’s options, not those of HtlcContract: see limitations.

Its workspace is temporary. The suite names no workspace and writes nothing into one. Each check is generated, run in a temporary directory, and removed. What persists is HtlcVerificationTest.proofs.json, the kept results, which let CI pass the suite without Lean. In the Scalus repository, the checks run in the workspace of Scalus’s own Lean library.

Linear Vesting

The vesting contract  releases an amount to a beneficiary linearly over a period. The suite proves three groups of statements, from the most general to the most specific:

• The schedule, linearVesting, for every datum and time: nothing is vested before the start; everything is vested from the end on; it returns, so it never divides by a zero duration; the vested amount does not decrease with time; and the contract stated in its body holds.
• The validator on every script context: it rejects an output without a datum, a withdrawal of a non-positive amount, and any purpose but spending.
• The validator on contexts of a few inputs and outputs: two of the three guarantees that spend states with Spec.ensures, that the beneficiary signed and that something is withdrawn, and the obligation that its call of the schedule owes. Sample withdrawals are accepted, and rejected unsigned or for more than is vested.

Statements that Lean does not finish are tagged Unfinished and left out of verify: the third guarantee, that what is not vested stays locked, and the statements on contexts of any size.

Its workspace is persistent, as Mixing UPLC and Lean Proofs describes. The suite overrides leanWorkspace with scalus-examples/jvm/src/test/lean/LinearVesting, a Lean project committed with the example:

• LinearVesting/Generated/ has every named statement of the suite as a Lean module, with its programs, written by leanExport, and Types.lean, the Lean types of the datum, the redeemer and the script context.
• LinearVesting/Proofs/Schedule.lean proves two of the statements by hand, as theorems of the generated propositions.
• Its lakefile.lean requires Scalus’s Lean library by its path, and sets packagesDir to the library’s, so Blaster and PlutusCore are built once for both workspaces.

Export the statements, and check the proofs by hand against the code as it is:

sbt "scalusExamplesJVM/leanExport scalus.examples.vesting.VestingVerificationTest"
(cd scalus-examples/jvm/src/test/lean/LinearVesting && lake build LinearVestingProofs)

Building the proofs takes a few minutes: each statement module runs its programs symbolically. In your own project, sbt leanProve runs the build, and sbt verify runs it after the suites.