First attempt at semi-formal validation regarding safety boundaries on contract calculations

Technical
,
#1

TLDR:

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:

  1. 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.

  2. 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:

image
image1324×555 75.9 KB

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.

1 Like
#2

Some key details

In case you are just reading and not going to go deep into the code, here are some of the key points:

  1. You can establish a named, abstract value:
short_liquidation_price = Int('short_liquidation_price')
  1. Then you can make assertions about the value

For example the range of allowed values:

short_liquidation_price >= MIN_PRICE
short_liquidation_price <= MAX_PRICE

or a calculation that the value is involved in:

unsafe_short_sats_out == nominal_composite / clamped_price

:point_up_2: Note that this == is not a simple boolean here. It is establishing a symbolic relationship exactly as we think of it mathematically.

  1. Then you can use a logic assertion, in the same way that basic mathematical proofs are done, to check whether your set of guarantees is enough to ensure that the contract will always execute safely.

The specific assertion is:

<input guarantees> ==> <safety requirements>

The proof is found by confirming that there is no solution to the negation of the assertion (a.k.a. propositional logic):

<input guarantees> AND (not <safety requirements>)
should have no solutions

I’m still not 100% sure that I’m using the correct construction for the proof. Again, if you have advice or corrections, I would really appreciate it.

1 Like