gustavo-grieco/abdk-math-64.64-verification
Formal verification effort for proving the ABDK Math 64.64 library properties using Echidna/hevm/Certora
The Great Verification of ABDK Math 64.64
This repository contains an ongoing effort to verify the key mathematical properties implemented by ABDK Math 64x64 using Echidna (powered by hevm). The invariants were directly extracted from the crytic-properties repository.
Status
When an invariant is explored using the symbolic engine in verification mode, there a few possible results:
- Verified ✅ The code was fully explored, without any issues on the translation or during solving. As expected, no counterexamples.
- Passed 👍 The code was fully explored without detecting any counterexamples, but the SMT solver cannot determine the answer to some of the queries (e.g. it timed out), so the assertion could still fail.
- Failed 💥 The exploration revealed a counterexample that was successfully replayed in concrete mode.
- Error ❌ A bug or a missing feature blocks the exploration or solving of some paths.
- Timeout ⏳ There are scalability issues preventing the creation of the model to explore all the program paths.
The following table shows the verification status of each invariant using Echidna/hevm and the Certora Prover:
| Invariant | hevm | Certora |
|---|---|---|
prove_abs_negative(int128) |
✅ | ✅ |
prove_abs_positive(int128) |
✅ | ✅ |
prove_abs_subadditivity(int128,int128) |
✅ | ✅ |
prove_abs_multiplicativeness(int128, int128) |
👍 | ✅ |
prove_add_commutative(int128,int128) |
✅ | ✅ |
prove_add_associative(int128,int128,int128) |
✅ | ✅ |
prove_add_identity(int128) |
✅ | ✅ |
prove_add_values(int128,int128) |
✅ | ✅ |
prove_add_range(int128,int128) |
✅ | ✅ |
prove_sub_equivalence_to_addition(int128,int128) |
✅ | ✅ |
prove_sub_non_commutative(int128,int128) |
✅ | ✅ |
prove_sub_identity(int128) |
✅ | ✅ |
prove_sub_neutrality(int128,int128) |
✅ | ✅ |
prove_sub_values(int128,int128) |
✅ | ✅ |
prove_sub_range(int128,int128) |
✅ | ✅ |
prove_neg_double_negation(int128) |
✅ | ✅ |
prove_neg_identity(int128) |
✅ | ✅ |
prove_mul_commutative(int128,int128) |
✅ | ✅ |
prove_mul_identity(int128) |
✅ | ✅ |
prove_mul_range(int128,int128) |
✅ | ✅ |
prove_mul_values(int128, int128) |
👍 | ✅ |
prove_mul_associative(int128, int128, int128) |
👍 | ✅ |
prove_mul_distributive(int128, int128, int128) |
❓ | ✅ |
prove_div_div_by_zero(int128) |
✅ | ✅ |
prove_div_division_identity(int128) |
✅ | ✅ |
prove_div_division_num_zero(int128) |
✅ | ✅ |
prove_div_maximum_numerator(int128) |
✅ | ✅ |
prove_div_range(int128,int128) |
✅ | ✅ |
prove_div_negative_divisor(int128,int128) |
👍 | ✅ |
prove_div_values(int128,int128) |
👍 | ✅ |
prove_inv_division(int128) |
✅ | ✅ |
prove_inv_sign(int128) |
✅ | ✅ |
prove_inv_values(int128) |
✅ | ✅ |
prove_inv_double_inverse(int128) |
👍 | ✅ |
prove_inv_identity(int128) |
❓ | ✅ |
prove_inv_multiplication(int128, int128) |
❓ | ❌ |
prove_avg_one_value(int128) |
✅ | ✅ |
prove_avg_operand_order(int128,int128) |
✅ | ✅ |
prove_avg_values_in_range(int128,int128) |
✅ | ✅ |
prove_gavg_one_value(int128) |
👍 | ⏳ |
prove_gavg_operand_order(int128, int128) |
❓ | ✅ |
prove_gavg_values_in_range(int128, int128) |
❓ | ⏳ |
prove_pow_zero_exponent(int128) |
✅ | ✅ |
prove_pow_zero_base(uint256) |
✅ | ✅ |
prove_pow_one_exponent(int128) |
✅ | ✅ |
prove_pow_base_one(uint256) |
✅ | ✅ |
prove_pow_maximum_base(uint256) |
✅ | ✅ |
prove_pow_values(int128, uint256) |
❓ | ⏳ |
prove_pow_sign(int128, uint256) |
❓ | ⏳ |
prove_sqrt_negative(int128) |
✅ | ✅ |
prove_sqrt_inverse_mul(int128) |
❓ | ⏳ |
prove_sqrt_inverse_pow(int128) |
❓ | ⏳ |
prove_sqrt_distributive(int128, int128) |
❓ | ⏳ |
prove_log2_negative(int128) |
✅ | ✅ |
prove_log2_distributive_mul(int128, int128) |
❓ | ❌ |
prove_ln_negative(int128) |
✅ | ✅ |
prove_exp2_equivalence_pow(uint256) |
❓ | ❌ |
prove_exp2_inverse(int128) |
❓ | ❌ |
prove_exp2_negative_exponent(int128) |
❓ | ❌ |
prove_exp_negative_exponent(int128) |
❓ | ❌ |
Verified by at least one tool: 46/60 (76.67%)
The following invariants have known counterexamples, found either by fuzzing (Echidna) or formal verification (Certora):
| Invariant | Found by |
|---|---|
prove_inv_division_noncommutativity(int128, int128) |
Certora |
prove_pow_high_exponent(int128, uint256) |
Echidna |
prove_pow_product_same_base(int128, uint256, uint256) |
Echidna |
prove_pow_power_of_an_exponentiation(int128, uint256, uint256) |
Echidna |
prove_pow_distributive(int128, int128, uint256) |
Echidna |
prove_log2_power(int128, uint256) |
Echidna |
prove_ln_distributive_mul(int128, int128) |
Echidna |
prove_ln_power(int128, uint256) |
Echidna |
prove_exp_inverse(int128) |
Echidna |
Counterexamples found: 9
These tables are going to be updated over time as more invariants are verified.
How To Run
If you want to run a preliminary fuzzing campaign, use:
make fuzz
To re-run the currently verified tests, execute:
make verify
If you want to run the verification of a single property, use T like this:
make verify T=prove_abs_negative
To make sure the verification works as expected, please install Echidna from its latest master revision and Bitwuzla 0.8.2.
Alternatively, hevm or certora can be used directly, even selecting an invariant:
make verify-hevm T=prove_abs_negative
make verify-certora T=prove_abs_negative
Changes
We made a few small modifications to this codebase:
- Adapted the header for using Foundry libraries and remappings.
- Commented out properties without arguments. These are actually unit tests and will be converted into Foundry tests.
- Applied minor formatting changes.
- Replaced some auxiliary functions such as
most_significant_bitswith loop-less equivalents.
Oh, Just One More Thing
If an emergency arises and an invariant does not hold, please open an issue in our tracker (even verified invariants can still reveal bugs). To contact the author directly, please use this form.