Add SAW command to simplify verification of FFI functions

[bboston7]

Given that FFI functions map to Cryptol functions in a known way, we should be able to synthesize SAW specs and not have to manually specify memory layouts, preconditions, postconditions, etc. A couple potential ways we could go about it are:

• A command called something like synthesize_ffi_spec that would return a SAW spec to be used with llvm_verify. Or,
• A command called something like llvm_ffi_verify that takes the Cryptol and FFI implementations, overrides, ProofScript, etc. and preforms the verification itself, much like llvm_verify.

---

Motivation behind this issue (copied from #1842 (comment)):

Currently the Cryptol FFI lets you write C implementations of some Cryptol functions, but there is no easy way to verify that those C implementations are actually correct. You could write a separate Cryptol spec for the foreign function, write some SAW script to set up verification for the C code, then run SAW on it, but given that Cryptol already knows the format of the arguments and return value for the foreign function, this process could be automated. So the idea would be to 1) allow the user to define a Cryptol implementation of functions marked foreign in addition to the C implementation, and 2) add some SAW command like ffi_verify which would, given the name of a Cryptol foreign function, automatically set up and verify the C implementation against the Cryptol version.

[eddywestbrook]

I feel like the one could call the other. That is, llvm_ffi_verify could use synthesize_ffi_spec to do its setup. If so, then it might make sense to implement both, starting with the synthesize_ffi_spec command, and expose both to the user. This idea would also give you a nice way to decompose the work into two steps.

[bboston7]

Great idea! Both are useful in different circumstances, so I'll add both commands!

[qsctr]

This is related to GaloisInc/cryptol#1397

[qsctr]

@andreistefanescu said that it might be easier to do x86 rather than llvm verification in this case, since the Cryptol FFI implementations are already in .so/.dll format.

[RyanGlScott]

I'm rather confused on the motivation behind this issue. Is the idea that you want to verify a function in an x86 binary? If so, then llvm_verify_x86 already gives you what you need, correct? Do you even need to involve the Cryptol FFI at that point?

Sorry if I am missing something obvious here.

[qsctr]

Currently the Cryptol FFI lets you write C implementations of some Cryptol functions, but there is no easy way to verify that those C implementations are actually correct. You could write a separate Cryptol spec for the foreign function, write some SAW script to set up verification for the C code, then run SAW on it, but given that Cryptol already knows the format of the arguments and return value for the foreign function, this process could be automated. So the idea would be to 1) allow the user to define a Cryptol implementation of functions marked foreign in addition to the C implementation, and 2) add some SAW command like ffi_verify which would, given the name of a Cryptol foreign function, automatically set up and verify the C implementation against the Cryptol version.

[RyanGlScott]

Ah, OK. I think the key thing I was missing is that you are proposing a way to accompany FFI declarations with additional Cryptol code as a sort of meta-specification for what the Cryptol FFI function should do. Once you have that, then everything else in this issue could be implemented as machinery on top of what SAW can already do. For instance, once you have the Cryptol meta-specification, verifying that the FFI code meets the meta-spec could be done by calling llvm_verify_x86 under the hood.

Is this understanding correct?

[qsctr]

Yes, that's correct. GaloisInc/cryptol#1397 covers the Cryptol end of things. I've copied the motivation up to the issue description, feel free to edit if anything is not clear.