Proving properties

In the last chapter, we proved one property on the square function: panic freedom.

This contract stipulates that, given a small input, the function will return a value: it will not panic or diverge. We could enrich the contract of square with a post-condition about the fact it is an increasing function:

#[hax_lib::requires(x < 16)]
#[hax_lib::ensures(|res| res >= x)]
#[hax_lib::lean::proof("by unfold square; hax_bv_decide")]
fn square(x: u8) -> u8 {
    x * x
}

This works as well.

The property that we prove above demonstrates a very simple case of a proof using hax and Lean. For a more complex example, a version of the Barrett example is available in the examples section of hax.