This is a first attempt at using formal verification tools to confirm that calculations in a contract are safe and will always result in a reasonable outcome. If anyone has advice or corrections, I would really appreciate it.
Back story to help understand where this code comes from:
For the current AnyHedge contract, we have always worked to ensure that money never gets locked up through some unexpected edge case. There are a few parts to that:
Ensuring that the execution inside the contract is as simple as possible (externalizing as much as possible to the setup of the contract). I won’t discuss this point here.
Ensuring that a given space of values passed into contract execution will always result in a valid and meaningful outcome. This is the main point I would like to share.
In the past, I did 2) by establishing basic safe boundaries for every individual step of the contract (for example, a price must be in the closed interval
[0, MAX_PRICE]), and then manually back-propagating boundaries from the outputs back to the inputs, with the final result being a list of required assurances for each input (for example, total input sats must be in the closed interval ‘[DUST, MAX_DESIRED_CONTRACT_SATS]’. The result was some time-consuming, hard to follow diagrams like the following:
With the development of an AnyHedge contract that allows leveraged shorts, I did step 1) above, but decided that I should look for something more standard for the validation step. Through past discussion with Tobias Ruck and also a little discussion with ChatGPT, I decided to try Z3-Prover.
Long story short, I came up with 1000 lines of code that accomplish the following (I’m 80% confident):
- Safety validation for AnyHedge 0.11 (current version), given a set of inputs that follow strict, but simple rules.
- Same safety validation for AnyHedge 2.0 (leveraged shorts)
- Same safety validation for AnyHedge 2.0, but applied at a higher level where the inputs are user-level inputs instead of raw contract inputs
- Confirmation of specific expected min/max boundaries (this is something like basic unit testing, but using the proof system)
This is a first attempt at using automated verification tools. If anyone has advice or corrections, I would really appreciate it.