Bind :sat and :prove counter example in REPL

[weaversa]

Cryptol 1 had this ability. Can we have it in the latest?

I would like both the satisfiability of the theorem and the counterexample to be bound to a tuple in the REPL. Say, sat_ or some user supplied variable, like the 'x' I supply below. Seeing as :let is not yet supported, this may have to wait a bit.

For example, Cryptol> :sat (x:[10]) -> x == x ((x : [10]) -> x == x) 0 = True would give a new value, sat_ = (True, 0)

Cryptol> :sat (x:[10]) -> x+1 == x Unsatisfiable. would give a new value, sat_ = (False, undefined)

Thanks, Sean

[kiniry]

I like the idea, though the magic of a pre-defined REPL variable is a bit ick. ;)

[weaversa]

If 'sat' and 'prove' were top level functions instead of ':' commands, one could do :let result = (sat \x:[10] -> x == x) Or, even make use of the results in .cry specifications.

Regardless, there needs to be some way to make use of the counterexamples besides copy&paste!

[LeventErkok]

sat/prove cannot be promoted to top-level functions. There are many good reasons for this, but just imagine what their type would be. Nothing you can sensibly write in Cryptol, if you expect it to generate counterexamples. (Aside from the fact that these are impure actions, and thus can't fit into the functional subset of Cryptol.)

But here's even a better reason. Let's say you could do that, and have: prove :: ([8] -> Bit) -> Bit as a monomorphic instance of such a magic function; ignoring the whole issue of model generation. Consider:

f : [8] -> Bit
f x = if prove f then False else True

what would prove f return?

You don't want to go down that rabbit hole.

I think Sean's original idea of binding to a "magic variable" is the only viable solution; as ugly as it is.

(Note that the situation in Haskell/SBV is fundamentally different; since the type of prove/sat there is behind the IO paywall: Thus the type-system prevents you from writing things like the above. Unless you're willing to add a similar monadic-layer on top of the Cryptol type-system, there's really no good way of supporting such functions as first class citizens.)

[weaversa]

I don’t think the type of ‘sat’ and ‘prove’ affect the type checker, but rather the type of the functions they are given to act on, which are always monomorphic and expressible in Cryptol.

To pick a little, what does this already accepted and perfectly valid cryptol function return?

f : [8] -> [8] f x = f x

Also, I personally have no qualms about ‘sat' and ‘prove' being unpure. In fact, they could be named ‘impure_sat' and ‘impure_prove', to make the notion clear.

~Sean

On Aug 7, 2014, at 4:40 PM, Levent Erkok notifications@github.com wrote:

sat/prove cannot be promoted to top-level functions. There are many good reasons for this, but just imagine what their type would be. Nothing you can sensibly write in Cryptol, if you expect it to generate counterexamples. (Aside from the fact that these are impure actions, and thus can't fit into the functional subset of Cryptol.)

But here's even a better reason. Let's say you could do that, and have: prove :: ([8] -> Bit) -> Bit as a monomorphic instance of such a magic function; ignoring the whole issue of model generation. Consider:

f : [8] -> Bit f x = if prove f then False else True what would prove f return?

You don't want to go down that rabbit hole.

I think Sean's original idea of binding to a "magic variable" is the only viable solution; as ugly as it is.

(Note that the situation in Haskell/SBV is fundamentally different; since the type of prove/sat there is behind the IO paywall: Thus the type-system prevents you from writing things like the above. Unless you're willing to add a similar monadic-layer on top of the Cryptol type-system, there's really no good way of supporting such functions as first class citizens.)

— Reply to this email directly or view it on GitHub.

[LeventErkok]

It's not about implementation Sean; it's about decidability. Also, there's no type that can be assigned to this alleged prove and sat that'd satisfy your needs. (There's no option type, for instance, in case there's no model. So, how would you distinguish the two? No case statements either.)

Also, how would you symbolically simulate a call to prove or sat itself? Maybe you can get away with a reference-implementation done in Cryptol itself. Again, ignoring models, it could read something like:

  prove f = ~zero == [f x | x <- domain f]

for an appropriate definition of a built-in function domain. But that's definitely not going to work for anything that's remotely interesting, just from a cardinailty perspective, even if you could assign it a passable type.

The other alternative would be to introduce these as "magic," i.e., language primitives; that cannot be symbolically simulated, nor can be assigned any valid type. But that's like the ML guys doing IO underneath you and telling you you got a string; it only works so far and eventually everything blows; especially within the de-facto lazy semantics Cryptol has with respect to evaluation. That'd definitely be the wrong thing to do.

But Galwegians are smart folks; and maybe they'll prove me wrong!

[weaversa]

'prove' and 'sat' could be functions that take some number of inputs and produce a tuple. So,

sat : {a, b} a -> (Bit, b)

Here the first bit in the returned tuple is used to denote whether or not the formula was SAT (True) or UNSAT (False), the second argument is the counterexample if the formula was SAT, and could be 'undefined' otherwise. So, there is no need for an 'option type'.

I don't know how to symbolically simulate a call to the symbolic simulator :-) I like your idea that they are 'magic' and can't be symbolically simulated.

I just think how neat it would be to have Cryptol functions interact with 'sat' and 'prove'. Thanks for continuing to think it through with me.

On Thu, Aug 7, 2014 at 9:15 PM, Levent Erkok notifications@github.com wrote:

It's not about implementation Sean; it's about decidability. Also, there's no type that can be assigned to this alleged prove and sat that'd satisfy your needs. (There's no option type, for instance, in case there's no model. So, how would you distinguish the two? No case statements either.)

Also, how would you symbolically simulate a call to prove or sat itself? Maybe you can get away with a reference-implementation done in Cryptol itself. Again, ignoring models, it could read something like:

prove f = ~zero == [f x | x <- domain f]

for an appropriate definition of a built-in function domain. But that's definitely not going to work for anything that's remotely interesting, just from a cardinailty perspective, even if you could assign it a passable type.

The other alternative would be to introduce these as "magic," i.e., language primitives; that cannot be symbolically simulated, nor can be assigned any valid type. But that's like the ML guys doing IO underneath you and telling you you got a string; it only works so far and eventually everything blows; especially within the de-facto lazy semantics Cryptol has with respect to evaluation. That'd definitely be the wrong thing to do.

But Galwegians are smart folks; and maybe they'll prove me wrong!

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/66#issuecomment-51553048.

[LeventErkok]

I guess you mean something like:

sat : fin a => (a -> Bit) -> (Bit, a)

Though I'm not sure if the type-checker will be happy with such a fin predicate in a non-word context. It could create a whole bunch of constraints to confuse the unsuspecting user.

The "magic" part of leaving it un-simulatable is not just an issue of not knowing how to do it, or do it efficiently; but rather the introduction of a clearly non-pure call into an otherwise functional language. Sort of like unsafePerformIO in Haskell. Once you make that deal, I'm afraid you'll find lots of things break.

This discussion reminded me of an older idea, which I thought was still present in some form; though I haven't been in touch with that part of the work for obvious reasons. The idea being you need some sort of a scripting language to do such proofs, and Cryptol, Java, C, LLVM, etc. being the different parts that you can plugin and perform cross-language-equivalence checking. That way, you can clearly separate the boundaries, and doing all the proof development outside of Cryptol; like it really should be. Galois site still lists SAW as a project, so maybe that's the key here; assuming some rudimentary part of SAW can be open-sourced as well, of course.

This is the story Haskell/SBV uses by the way; where the Symbolic monad gives you the "pure" symbolically simulatable world, while the Haskell level prove/sat functions give you the programmable proof engine world; keeping the two separate via the type-system.

I think anything less will suffer from the ML/Scheme syndrome, where things are pure unless they aren't. I don't think that's a model Cryptol should follow.

[weaversa]

There is a lot of work being put into the SAW right now. And, yeah, these kinds of things can be done with that.

On Fri, Aug 8, 2014 at 3:52 AM, Levent Erkok notifications@github.com wrote:

I guess you mean something like:

sat : fin a => (a -> Bit) -> (Bit, a)

Though I'm not sure if the type-checker will be happy with such a fin predicate in a non-word context. It could create a whole bunch of constraints to confuse the unsuspecting user.

The "magic" part of leaving it un-simulatable is not just an issue of not knowing how to do it, or do it efficiently; but rather the introduction of a clearly non-pure call into an otherwise functional language. Sort of like unsafePerformIO in Haskell. Once you make that deal, I'm afraid you'll find lots of things break.

This discussion reminded me of an older idea, which I thought was still present in some form; though I haven't been in touch with that part of the work for obvious reasons. The idea being you need some sort of a scripting language to do such proofs, and Cryptol, Java, C, LLVM, etc. being the different parts that you can plugin and perform cross-language-equivalence checking. That way, you can clearly separate the boundaries, and doing all the proof development outside of Cryptol; like it really should be. Galois site still lists SAW as a project, so maybe that's the key here; assuming some rudimentary part of SAW can be open-sourced as well, of course.

This is the story Haskell/SBV uses by the way; where the Symbolic monad gives you the "pure" symbolically simulatable world, while the Haskell level prove/sat functions give you the programmable proof engine world; keeping the two separate via the type-system.

I think anything less will suffer from the ML/Scheme syndrome, where things are pure unless they aren't. I don't think that's a model Cryptol should follow.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/66#issuecomment-51573131.

[kiniry]

Assigning to @atomb since SAW is his baby and this aligns with ongoing work there.

FWIW, I agree that "magic" is the possibly the right approach if we begin to lift commands into expressions. That being said, I think that SAW is the right place for this, not Cryptol.

[weaversa]

Binding the :sat and :prove results to a variable in the Cryptol interpreter would be much appreciated.

On Tue, Aug 12, 2014 at 8:04 PM, Joseph Kiniry notifications@github.com wrote:

Assigning to @atomb https://github.com/atomb since SAW is his baby and this aligns with ongoing work there.

FWIW, I agree that "magic" is the possibly the right approach if we begin to lift commands into expressions. That being said, I think that SAW is the right place for this, not Cryptol.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/66#issuecomment-51994477.

[acfoltzer]

This is added in ceb084c. Binding undefined to a variable is tricky since it's polymorphic, but since this is a command where we can play somewhat fast and loose with the types, we have the following behavior.

After a call to :sat, the variable it is bound to:

• False : Bit if the formula is unsat
• x : t, where x is the satisfying assignment if the formula is satisfiable and has exactly one argument of type t
• (x1, x2, ...) : (t1, t2, ...) where x1, x2 ... are the satisfying assignments of a multi-argument sat formula. They're just tupled up, so to get the first argument, do it.1, etc.

:prove works much the same, binding it to True when the theorem is proved, and binding the counterexample if it has one.

Note that this patch also binds the result of other interpreter evaluation to it as well, and adds let as in #6, so if you want to hang on to your counterexamples, do something like:

Cryptol> :prove p
Cryptol> let cex = p

@weaversa, let me know if this looks good to you.

[weaversa]

Hi,

I really like the result (and all interpreter calls) being bound to ‘it’. I also really like the existence of ‘let’. Thank you for working to fix things up!

However, I strongly suggest the result of :sat and :prove return either a tuple or record so that result of the calls can be distinguished from the counter example. Below are two calls to :sat. One is satisfiable and the other is unsatisfiable, but they both bind the same result to ‘it’, making it impossible to programmatically tell whether or not the call was satisfiable or not.

Really, undefined is unnecessary, if the result is Unsatisfiable/Q.E.D, the counter example could be anything. Folks just have to know to obey the result before asking for the counter example — using 'undefined’ would just make sure they obey.

Cryptol> :sat \x -> x == False (\x -> x == False) False = True Cryptol> :t it it : Bit Cryptol> it False

Cryptol> :sat (x:Bit) -> True == False Unsatisfiable. Cryptol> :t it it : Bit Cryptol> it False

I don’t understand why I can’t bind expressions using ‘undefined’. The following (! swapped with @) works fine in the old cryptol. Is there some inherit reason why this can’t be done, or is it something on the list?

Cryptol> ([False]#undefined)!0 False Cryptol> let x = ([False]#undefined)!0 [error] unbound symbol: (at :1:18--1:27, undefined)

Thanks, Sean

On Aug 19, 2014, at 8:27 PM, Adam C. Foltzer notifications@github.com wrote:

This is added in ceb084c. Binding undefined to a variable is tricky since it's polymorphic, but since this is a command where we can play somewhat fast and loose with the types, we have the following behavior.

After a call to :sat, the variable it is bound to:

False : Bit if the formula is unsat x : t, where x is the satisfying assignment if the formula is satisfiable and has exactly one argument of type t (x1, x2, ...) : (t1, t2, ...) where x1, x2 ... are the satisfying assignments of a multi-argument sat formula. They're just tupled up, so to get the first argument, do it.1, etc. :prove works much the same, binding it to True when the theorem is proved, and binding the counterexample if it has one.

Note that this patch also binds the result of other interpreter evaluation to it as well, and adds let as in #6, so if you want to hang on to your counterexamples, do something like:

Cryptol> :prove p Cryptol> let cex = p @weaversa, let me know if this looks good to you.

— Reply to this email directly or view it on GitHub.

[acfoltzer]

I really like the result (and all interpreter calls) being bound to ‘it’. I also really like the existence of ‘let’. Thank you for working to fix things up!

You’re quite welcome!

However, I strongly suggest the result of :sat and :prove return either a tuple or record so that result of the calls can be distinguished from the counter example. Below are two calls to :sat. One is satisfiable and the other is unsatisfiable, but they both bind the same result to ‘it’, making it impossible to programmatically tell whether or not the call was satisfiable or not.

Ah, that’s a great point, I didn’t hit that ambiguity in the cases I tried out. I think a record is a good solution for making it unambiguous. I’ll work on implementing that today.

If you’re looking for something that could be programmatically manipulated, maybe there’s another interface we could provide as well? We don’t want you to have to parse the REPL…

I don’t understand why I can’t bind expressions using ‘undefined’. The following (! swapped with @) works fine in the old cryptol. Is there some inherit reason why this can’t be done, or is it something on the list?

There’s no inherent reason, but the implementation would have to choose some arbitrary type to instantiate it at, and I’d like to stick with the least arbitrary solution possible. I think the idea of a record is the best choice, though.

[weaversa]

<<If you’re looking for something that could be programmatically manipulated, maybe there’s another interface we could provide as well? We don’t want you to have to parse the REPL…>>

Good point! How is "Cryptol as a library" coming along?

On Wed, Aug 20, 2014 at 1:05 PM, Adam C. Foltzer notifications@github.com wrote:

I really like the result (and all interpreter calls) being bound to ‘it’. I also really like the existence of ‘let’. Thank you for working to fix things up!

You’re quite welcome!

However, I strongly suggest the result of :sat and :prove return either a tuple or record so that result of the calls can be distinguished from the counter example. Below are two calls to :sat. One is satisfiable and the other is unsatisfiable, but they both bind the same result to ‘it’, making it impossible to programmatically tell whether or not the call was satisfiable or not.

Ah, that’s a great point, I didn’t hit that ambiguity in the cases I tried out. I think a record is a good solution for making it unambiguous. I’ll work on implementing that today.

If you’re looking for something that could be programmatically manipulated, maybe there’s another interface we could provide as well? We don’t want you to have to parse the REPL…

I don’t understand why I can’t bind expressions using ‘undefined’. The following (! swapped with @) works fine in the old cryptol. Is there some inherit reason why this can’t be done, or is it something on the list?

There’s no inherent reason, but the implementation would have to choose some arbitrary type to instantiate it at, and I’d like to stick with the least arbitrary solution possible. I think the idea of a record is the best choice, though.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/66#issuecomment-52808840.

[weaversa]

<<the implementation would have to choose some arbitrary type to instantiate it at, and I’d like to stick with the least arbitrary solution possible. I think the idea of a record is the best choice, though.>> To me, the least arbitrary solution is to type 'undefined' as though it were the counter example...that is, the same type of the inputs to the :sat or :prove command.

So, in the future we could have something like,

Satisfiable Example:

Cryptol> :sat (x:[2], y:[2]) -> (x < y) ((x : [2], y : [2]) -> x < y) (0, 1) = True Cryptol> :t it it : {res = True, cex = (0, 1) : ([2], [2])} : {res : Bit, cex : ([2], [2])} Cryptol> it {res = True, cex = (0, 1)} Cryptol> it.res True Cryptol> it.cex (0, 1)

Unsatisfiable Example: Cryptol> :sat (x:[2], y:[2]) -> (x < 0) Unsatisfiable. Cryptol :t it it : {res = False, cex = undefined : ([2], [2])} : {res : Bit, cex : ([2], [2])} Cryptol> it

Run-time error: undefined Cryptol> it.res False Cryptol> it.cex

Run-time error: undefined

On Wed, Aug 20, 2014 at 1:07 PM, Sean Weaver weaversa@gmail.com wrote:

<<If you’re looking for something that could be programmatically manipulated, maybe there’s another interface we could provide as well? We don’t want you to have to parse the REPL…>>

Good point! How is "Cryptol as a library" coming along?

On Wed, Aug 20, 2014 at 1:05 PM, Adam C. Foltzer <notifications@github.com

wrote:

I really like the result (and all interpreter calls) being bound to ‘it’. I also really like the existence of ‘let’. Thank you for working to fix things up!

You’re quite welcome!

However, I strongly suggest the result of :sat and :prove return either a tuple or record so that result of the calls can be distinguished from the counter example. Below are two calls to :sat. One is satisfiable and the other is unsatisfiable, but they both bind the same result to ‘it’, making it impossible to programmatically tell whether or not the call was satisfiable or not.

Ah, that’s a great point, I didn’t hit that ambiguity in the cases I tried out. I think a record is a good solution for making it unambiguous. I’ll work on implementing that today.

If you’re looking for something that could be programmatically manipulated, maybe there’s another interface we could provide as well? We don’t want you to have to parse the REPL…

I don’t understand why I can’t bind expressions using ‘undefined’. The following (! swapped with @) works fine in the old cryptol. Is there some inherit reason why this can’t be done, or is it something on the list?

There’s no inherent reason, but the implementation would have to choose some arbitrary type to instantiate it at, and I’d like to stick with the least arbitrary solution possible. I think the idea of a record is the best choice, though.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/66#issuecomment-52808840.

[acfoltzer]

I went around on this design a few times, trying to avoid introducing more ambiguities. Here's the current leading idea, implemented in b1c4527:

If a formula is unsatisfiable, no matter its arguments, we get back a record that just has a result field:

Cryptol> :sat \(x : [8]) -> x == 0 && x == 1
Unsatisfiable.
Cryptol> :t it
it : {result : Bit}
Cryptol> it
{result = False}

If a formula is satisfiable and...

... has no arguments, we get back something similar:

Cryptol> :sat True
True = True
Cryptol> :t it
it : {result : Bit}
Cryptol> it
{result = True}

... has exactly one argument, we get that argument in an arg field:

Cryptol> :sat \(x : [8]) -> x == 5
(\(x : [8]) -> x == 5) 5 = True
Cryptol> :t it
it : {result : Bit, arg : [8]}
Cryptol> it
{result = True, arg = 5}

... has more than one argument, we get the arguments tupled up in an args (not arg) field:

Cryptol> :sat \(x : [8]) (y : [8]) -> x < y
(\(x : [8]) (y : [8]) -> x < y) 0 1 = True
Cryptol> :t it
it : {result : Bit, args : ([8], [8])}
Cryptol> it
{result = True, args = (0, 1)}

I'm not really happy about having a different field name for the one-argument case, and no field for the no-argument case, but it comes down to avoiding ambiguity between the three satisfiable cases.

[acfoltzer]

Commit 9346db2 has new behavior. In the case of unsat or proved, rather than leaving out the argument fields, we keep them in as undefined:

Cryptol> :sat \(x : [8]) -> x == 0 && x == 1
Unsatisfiable.
Cryptol> :t it
it : {result : Bit, arg1 : [8]}
Cryptol> it

Run-time error: no satisfying assignment available
Cryptol> it.result
False

Rather than having distinct no-arg, one-arg, and multi-arg cases, we now use an argN convention that's uniform:

Cryptol> :sat \(x : [8]) -> x == 5
(\(x : [8]) -> x == 5) 5 = True
Cryptol> :t it
it : {result : Bit, arg1 : [8]}
Cryptol> it
{result = True, arg1 = 5}

Cryptol> :sat \(x : [8]) (y : [8]) -> x < y
(\(x : [8]) (y : [8]) -> x < y) 0 1 = True
Cryptol> :t it
it : {result : Bit, arg1 : [8], arg2 : [8]}
Cryptol> it
{result = True, arg1 = 0, arg2 = 1}

[dylanmc]

I nominate this issue for closing. Anyone object?

[acfoltzer]

I'm going to wait to close this until we get :allSat integrated, as there's likely to be some debate about how those results are presented.

[weaversa]

ping

[acfoltzer]

D'oh, forgot to close this, sorry!

Cryptol> :sat \x -> x == 0x4
(\x -> x == 0x4) 0x4 = True
Cryptol> :t it
it : {result : Bit, arg1 : [4]}
Cryptol> it
{result = True, arg1 = 0x4}
Cryptol> :sat \x -> x == 0x4 && x == 0x5
Unsatisfiable
Cryptol> :t it
it : {result : Bit, arg1 : [4]}
Cryptol> it

Run-time error: no satisfying assignment available
Cryptol> :set satNum=all
Cryptol> :sat \x -> x != 0x4
(\x -> x != 0x4) 0x0 = True
(\x -> x != 0x4) 0x1 = True
(\x -> x != 0x4) 0x2 = True
(\x -> x != 0x4) 0x3 = True
(\x -> x != 0x4) 0x5 = True
(\x -> x != 0x4) 0x6 = True
(\x -> x != 0x4) 0x7 = True
(\x -> x != 0x4) 0x8 = True
(\x -> x != 0x4) 0x9 = True
(\x -> x != 0x4) 0xa = True
(\x -> x != 0x4) 0xb = True
(\x -> x != 0x4) 0xc = True
(\x -> x != 0x4) 0xd = True
(\x -> x != 0x4) 0xe = True
(\x -> x != 0x4) 0xf = True
Cryptol> :t it
it : [15]{result : Bit, arg1 : [4]}
Cryptol> it
[{result = True, arg1 = 0x0}, {result = True, arg1 = 0x1},
 {result = True, arg1 = 0x2}, {result = True, arg1 = 0x3},
 {result = True, arg1 = 0x5}, {result = True, arg1 = 0x6},
 {result = True, arg1 = 0x7}, {result = True, arg1 = 0x8},
 {result = True, arg1 = 0x9}, {result = True, arg1 = 0xa},
 {result = True, arg1 = 0xb}, {result = True, arg1 = 0xc},
 {result = True, arg1 = 0xd}, {result = True, arg1 = 0xe},
 {result = True, arg1 = 0xf}]