Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typechecker query / issue? #930

Open
martin-d2 opened this issue Oct 13, 2020 · 10 comments
Open

Typechecker query / issue? #930

martin-d2 opened this issue Oct 13, 2020 · 10 comments
Labels
typechecker Issues related to type-checking Cryptol code.

Comments

@martin-d2
Copy link

Hey Galois 😄 👋

In Cryptol 2.9.1:

  y : {r} (fin r) => [r+1]
  y = `(2^^r)

Cryptol complains that it doesn't know at compile-time that width(2^^r) is small enough to fit in r+1 bits, for all r. I think that's because it can't evaluate 2^^r until it sees r, which it doesn't see till run-time. This seems perfectly reasonable.
So you can add the constraint, and

  y : {r} (fin r, width (2^^r)==r+1) => [r+1]
  y = `(2^^r)

compiles perfectly.

Given

  x : {r} (fin r) => [r]
  x = `(2^^r-1)

Cryptol complains that is doesn't know at compile-time that width(2^^r-1) is small enough to fit in r bits, similar to before. But this time, if you add the minimum constraint it needs, it still barfs. Adding the constraint (width(2^^r-1)==r) doesn't work, because Cryptol somehow doesn't see that the 2^^r-1 in the constraint is equal to the 2^^r-1 in the function definition(!) One resolution is as follows:

  x : {r} (fin r, width(2^^r-1)<=r) => [r]
  x = `(2^^r-1)

I'm not quite sure why replacing the equality with an inequality forces it down a different logical pathway, but apparently it does. I think this counts as a bug(?), because I believe Cryptol should be able to deduce A>=B from A==B in all circumstances.

Any thoughts?

Thanks :-)

Martin

@brianhuffman
Copy link
Contributor

To see what's going on here, we can get Cryptol to show the queries and responses between the typechecker and the solver by entering :set tc-debug = 2.

Now, after the usual preamble of define-fun declarations, the y : {r} (fin r, width (2^^r)==r+1) => [r+1] version gives this successful result (note the unsat, which indicates that no counterexample exists).

PROVE IMP
  VARIABLES
    [send->] (push 1 )
    [<-recv] success
    [send->] (declare-fun kv0 () InfNat )
    [<-recv] success
    [send->] (assert (cryVar kv0 ) )
    [<-recv] success
  ASSUMPTIONS
    [send->] (assert (cryAssume (cryFin kv0 ) ) )
    [<-recv] success
    [send->] (assert (cryAssume (cryEq (cryWidth (cryExp (cryNat 2 ) kv0 ) ) (cryAdd (cryNat 1 ) kv0 ) ) ) )
    [<-recv] success
  PROVE
    [send->] (push 1 )
    [<-recv] success
    [send->] (assert (cryProve (cryGeq (cryAdd (cryNat 1 ) kv0 ) (cryWidth (cryExp (cryNat 2 ) kv0 ) ) ) ) )
    [<-recv] success
    [send->] (check-sat )
    [<-recv] unsat
    [send->] (pop 1 )
    [<-recv] success
  [send->] (pop 1 )
  [<-recv] success
[send->] (exit )

On the other hand, y : {r} (fin r, width (2^^r-1)==r) => [r] version give this unsuccessful result (note the sat).

PROVE IMP
  VARIABLES
    [send->] (push 1 )
    [<-recv] success
    [send->] (declare-fun kv0 () InfNat )
    [<-recv] success
    [send->] (assert (cryVar kv0 ) )
    [<-recv] success
  ASSUMPTIONS
    [send->] (assert (cryAssume (cryFin kv0 ) ) )
    [<-recv] success
    [send->] (assert (cryAssume (cryEq (cryWidth (crySub (cryExp (cryNat 2 ) kv0 ) (cryNat 1 ) ) ) kv0 ) ) )
    [<-recv] success
  PROVE
    [send->] (push 1 )
    [<-recv] success
    [send->] (assert (cryProve (cryGeq kv0 (cryWidth (crySub (cryExp (cryNat 2 ) kv0 ) (cryNat 1 ) ) ) ) ) )
    [<-recv] success
    [send->] (check-sat )
    [<-recv] sat
    [send->] (pop 1 )
    [<-recv] success
  [send->] (pop 1 )
  [<-recv] success
[send->] (exit )

It does seem weird that these two queries would give a different result, because they both have the same form: Assume cryEq x y and then try to prove cryGeq y x. Shouldn't this be easy? It's more complicated than it looks, for a couple of reasons. First, the presence of the width and ^^ functions (translated to smt-lib as uninterpreted functions cryWidth and cryExp) makes the solver necessarily incomplete, and introduces the possibility of spurious counterexamples. Second, the cryptol predicates == and >= operate in a logic of partial functions; instead of just meaning logical equality, cryEq is defined by cases over a datatype, and asserts that either both arguments are inf or both the same natural number, and also that both arguments are defined, as you can see earlier in the tc-debug output:

[send->] (define-fun cryEq ((x InfNat ) (y InfNat ) ) MaybeBool (ite (or (isErr x ) (isErr y ) ) cryErrProp (cryBool (ite (isFin x ) (ite (isFin y ) (= (value x ) (value y ) ) false ) (not (isFin y ) ) ) ) ) )

So basically what's happening is that the solver isn't clever enough to prove one of the queries that we send it, and it returns a spurious counterexample instead. We could complain that the solver is not clever enough, but maybe we could do something to make its job a bit easier.

@brianhuffman
Copy link
Contributor

I should also mention that the reason why the last variation with y : {r} (fin r, width (2^^r-1)<=r) => [r] works is that the assumed constraint is exactly the same as the constraint needed by the body of the definition, so Cryptol discharges it without even sending it to the solver.

@yav
Copy link
Member

yav commented Oct 13, 2020

@brianhuffman if you have any ideas on useful ad-hoc properties that might help, potentially useful locations in the typechecker are:

  • tWidth in SimpType, if we want to rewrite specific occurrences of width, or
  • maybe something in Solver.Numeric.Interval which is what we use to estimate bounds on variables

@brianhuffman
Copy link
Contributor

It might help me understand what the solver is doing wrong if I could see what the spurious satisfying assignment the solver came up with in this case. Do we have a way to do that? Or maybe I should just cut-and-paste the tc-debug output into an .smt2 file that I can run separately with z3?

@yav
Copy link
Member

yav commented Oct 13, 2020

I usually just do the copy paste, but it might be nice to have something more structured. The interaction with the external solver is in src/Cryptol/TypeCheck/Solver/SMT.hs

@brianhuffman
Copy link
Contributor

I should point out another data point: Change the type signature from y : {r} (fin r, width (2^^r-1)==r) => [r] to y : {r, s} (fin r, width (2^^r-1)==s) => [s], and the solver can handle it easily. So I think part of the problem is that the equality assumption width (2^^r-1)==r contains an instance of the rhs inside the lhs, so z3 is (rightfully) very timid about using it, because it's worried about getting stuck in an infinite loop. Normally z3 can be quite aggressive about unfolding or computing the transitive closure of term equalities, but not in this case.

@robdockins
Copy link
Contributor

I imagine it's because the cryWidth function falls back on an uninterpreted function after 64 bits, and the solver chooses a spurious counterexample.

@robdockins
Copy link
Contributor

We could probably add an axiom that related cryWidth and cryExp and might help with these situations.

@brianhuffman
Copy link
Contributor

One idea would be an axiom stating that width a <= b iff a < 2^^b. Then the width (2^^r-1)<=r goal would be simplified to 2^^r - 1 < 2^^r, which I'd guess z3 could handle.

@brianhuffman brianhuffman added the typechecker Issues related to type-checking Cryptol code. label Oct 13, 2020
@robdockins
Copy link
Contributor

Yeah, that might work, and I think it would play OK with Z3's universal axiom triggering mechanism. I suppose we could also have, e.g., a <= width b iff 2^^a <= b (although I'd have to do some hard thinking about the exact inequalities to use).

robdockins added a commit that referenced this issue Apr 5, 2021
This fixes issue #734, and partially addresses #930.
The basic issue with 734 was that the solver was chosing
spurious counterexamples for the exponent function; in particular,
models where the output was not at least 1.  The fairly restricted
axiom we add here just says that the exponent function is at least
as large as its base for positive inputs.
robdockins added a commit that referenced this issue Apr 6, 2021
This fixes issue #734, and partially addresses #930.
The basic issue with 734 was that the solver was chosing
spurious counterexamples for the exponent function; in particular,
models where the output was not at least 1.  The fairly restricted
axiom we add here just says that the exponent function is at least
as large as its base for positive inputs.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
typechecker Issues related to type-checking Cryptol code.
Projects
None yet
Development

No branches or pull requests

4 participants