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.