Document that foreign functions should be pure

[yav]

We should add note to the FFI section to make it explicit that our intention is that foreign function are pure (i.e., do not have observable side effects).

[ramsdell]

Let me expand on this request.

The RefMan in the cryptol repository gives its readers no hint as to the fact that the order in which FFI calls are evaluated can influence the meaning of an expression. For example, suppose there is a C function called count that has some internal state, and it increments an integer with each call, ignores its input, and returns the integer. After loading this into cryptol

foreign count: [32] -> [32]
 
seq : [10][32]
seq = [ count i | i <- [0 .. 9 : [32]] ]

and typing seq ! 2; seq you get a different answer than had you started by typing seq.

Please expand the FFI section in the RefMan to help readers understand why this happens so they understand why one should not load functions with observable state.

[RyanGlScott]

Done in #1558.