FFI call semantics about cryptol HOT 6 CLOSED

What precisely do you mean when you say "this behavior"?

Do you mean "preserve the internal state of rand.dylib in between invocations of rand"? This might be possible to guarantee in a limited context, but it would be fragile, since we don't preserve the internal state between module reloads. That is, this script would print three different random numbers:

:load rand.cry
rand ()
rand ()
rand ()

$ ~/Software/cryptol-3.0.0/bin/cryptol -b script1.icry 
Loading module Cryptol
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6
0x000000000000167e
0x0000000000002781

But this script would print the same number three times:

:load rand.cry
rand ()
:load rand.cry
rand ()
:load rand.cry
rand ()

$ ~/Software/cryptol-3.0.0/bin/cryptol -b script2.icry 
Loading module Cryptol
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6

Even if we restrict ourselves to a single-module-load assumption, it would be tricky to make particular guarantees about the order in which multiple calls to rand are invoked. As a example to illustrate what I mean, note that these two commands will return different answers depending on how your machine schedules threads:

$ ~/Software/cryptol-3.0.0/bin/cryptol -c "parmap rand [(), (), (), (), (), (), (), ()]" rand.cry +RTS -N8 -RTS
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
[0x00000000000041c6, 0x000000000000167e, 0x00000000000015fb,
 0x0000000000001cfb, 0x000000000000446b, 0x00000000000059e2,
 0x0000000000002781, 0x000000000000794b]

$ ~/Software/cryptol-3.0.0/bin/cryptol -c "parmap rand [(), (), (), (), (), (), (), ()]" rand.cry +RTS -N8 -RTS
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
[0x000000000000167e, 0x000000000000794b, 0x0000000000002781,
 0x00000000000041c6, 0x00000000000059e2, 0x000000000000446b,
 0x0000000000001cfb, 0x00000000000015fb]

This is a rather contrived example, but this issue could arise in more subtle ways. For instance, if you are lazily evaluating an infinite sequence, the order of evaluation might determine whether rand gets invoked in a certain order or not, and this could be difficult to predict.

This is all to say: I don't think we are planning to deliberately change the behavior of the Cryptol FFI to make something like a foreign rand declaration unusable, but anyone who wants to do this will need to take precautions so that they don't wind up with surprising results.

from cryptol.

In a nutshell, should I choose to include C functions that are stateful, what I want to know is what semantics can I depend on into the future. You point out that the state is not preserved over module reloads. Good to know, and of course, it makes a lot of sense. Lack of commitment to evaluation order when calling stateful C functions also makes sense. In the case in which one is producing pseudo random numbers, it may be okay that there is no a commitment to an explicit order. If there is no parallelism, can a user depend on reproducibility? Finally, when there is parallelism, one obviously cannot depend on reproducibility. May a user depend on the fact that calls to C code are atomic? Inquiring minds want to know.

from cryptol.

My gut feeling is that one should not do this sort of thing. The way I decide what's a "good" FFI function is if the same function could be implemented in Cryptol in some way (no matter how inefficient). If yes, then it's good, otherwise questionable. Of course, nothing prevents one from using questionable functions, and that might work OK for a paritcular configuration (e.g., fixed version of Cryptol/hardware/compilers etc), but this is threading on thin ice.

Btw, if the persistent state is not large, one option would be to modify the C function to pass it around (e.g., the seed for the random number generator).

from cryptol.

As a long time advocate of pure functional programming, this sort of thing is abhorrent to me too. But you know people are going to do this. The manual should let users know what they can depend on and emphasize the world of hurt they are entering into if they are not careful.

from cryptol.

I agree that we should document the pitfalls of using impure functions in the FFI somewhere. I'm not sure if we want to guarantee anything about the behavior of impure FFI functions at this point, other than a generic "you are on your own" disclaimer.

from cryptol.

I've submitted #1558 with a clarification to the reference manual.

from cryptol.