reach-sh/reach-lang

Sqrt fails formal verification

Gungy2 opened this issue · 5 comments

Gungy2 commented

Describe the error

There seems to be a bug in sqrt for formal verification. The following example fails verification (irrespective of the value of tokensToReturn.

To Reproduce

const tokensToReturn = (depositInvariant * stableTokenBalance) / slbTokenBalance;
require(sqrt(tokensToReturn) * sqrt(tokensToReturn) <= tokensToReturn, "Sqrt works");

Extra information

I am using the latest version of Reach. Also, may I please ask you to prioritize this, if at all possible? My Master thesis is due in about 2 weeks, and my project has been blocked by this bug for about 3 weeks now. Thank you so much!

jeapostrophe commented

What is the error you get?

Gungy2 commented

I think the conversation on Discord is also relevant.

Gungy2 commented

Alternatively, even easier:

export const main =
  Reach.App( () => {
    const A = Participant('A', { x: UInt });
    init();
      A.only(() => {
        const x = declassify(interact.x);
        assume(x > 0, "x too low");
      });
      A.publish(x);
      commit();
      assert(sqrt(x) * sqrt(x) <= x);
    }
  );

This gives:

  // Violation Witness

  const UInt.max = 4;

  const x/43 = "A".interact.x;
  //    ^ could = 3
  //      from: ./t/y/sqrt.rsh:5:34:property binding

  // Theorem Formalization

  const v51 = sqrtx/43;
  //    ^ would be 2
  const v54 = (v51 * v51) <= x/43;
  //    ^ would be false
  assert(v54);

  Verifying when NO participants are honest
Checked 5 theorems; 2 failures (and 1 omitted repeats) :'(
jeapostrophe commented

If you are not able to test or use the new SMT assertion, then you can change your code from using a require to using an enforce, which will make it happen at run-time.

  • ❤️1