ffi.lem

(*
  An oracle says how to perform an ffi call based on its internal
  state, represented by the type variable 'ffi.
*)
open import Pervasives
open import Pervasives_extra
open import Lib


type ffi_outcome = FFI_failed | FFI_diverged

type oracle_result 'ffi = Oracle_return of 'ffi * list word8 | Oracle_final of ffi_outcome
type oracle_function 'ffi = 'ffi -> list word8 -> list word8 -> oracle_result 'ffi
type oracle 'ffi = string -> oracle_function 'ffi

(* An I/O event, IO_event s bytes bytes2, represents the call of FFI function s with
* immutable input bytes and mutable input map fst bytes2,
* returning map snd bytes2 in the mutable array. *)

type io_event = IO_event of string * list word8 * (list (word8 * word8))

type final_event = Final_event of string * list word8 * list word8 * ffi_outcome

type ffi_state 'ffi =
<| oracle      : oracle 'ffi
 ; ffi_state   : 'ffi
 ; io_events   : list io_event
 |>

val initial_ffi_state : forall 'ffi. oracle 'ffi -> 'ffi -> ffi_state 'ffi
let initial_ffi_state oc ffi =
<| oracle      = oc
 ; ffi_state   = ffi
 ; io_events   = []
 |>

type ffi_result 'ffi = FFI_return of ffi_state 'ffi * list word8 | FFI_final of final_event

val call_FFI : forall 'ffi. ffi_state 'ffi -> string -> list word8 -> list word8 -> ffi_result 'ffi
let call_FFI st s conf bytes =
  if s <> "" then
    match st.oracle s st.ffi_state conf bytes with
    | Oracle_return ffi' bytes' ->
        if length bytes' = length bytes then
          (FFI_return
            <| st with ffi_state = ffi'
                    ; io_events =
                        st.io_events ++
                          [IO_event s conf (zipSameLength bytes bytes')]
            |>
            bytes')
        else FFI_final(Final_event s conf bytes FFI_failed)
    | Oracle_final outcome ->
          FFI_final(Final_event s conf bytes outcome)
    end
  else FFI_return st bytes

type outcome = Success | Resource_limit_hit | FFI_outcome of final_event

(* A program can Diverge, Terminate, or Fail. We prove that Fail is
   avoided. For Diverge and Terminate, we keep track of what I/O
   events are valid I/O events for this behaviour. *)
type behaviour 'ffi =
    (* There cannot be any non-returning FFI calls in a diverging
       exeuction. The list of I/O events can be finite or infinite,
       hence the llist (lazy list) type. *)
    Diverge of llist io_event
    (* Terminating executions can only perform a finite number of
       FFI calls. The execution can be terminated by a non-returning
       FFI call. *)
  | Terminate of outcome * list io_event
    (* Failure is a behaviour which we prove cannot occur for any
       well-typed program. *)
  | Fail

(* trace-based semantics can be recovered as an instance of oracle-based
 * semantics as follows. *)

val trace_oracle : oracle (llist io_event)
let trace_oracle s io_trace conf input =
  match lhd io_trace with
  | Just (IO_event s' conf' bytes2) ->
      if (s = s') && (map fst bytes2 = input) && (conf = conf') then
        Oracle_return (fromJust (ltl io_trace)) (map snd bytes2)
      else Oracle_final FFI_failed
  | _ -> Oracle_final FFI_failed
  end