Definition of CakeML's observational semantics, in particular traces of calls over the Foreign-Function Interface (FFI).
ffi.lem: An oracle says how to perform an ffi call based on its internal state, represented by the type variable 'ffi.
simpleIO.lem: A simple instantiation of the ffi type.