Theory Ffi

chapter ‹Generated by Lem from ‹semantics/ffi/ffi.lem›.›

theory "Ffi" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives"
  "LEM.Lem_pervasives_extra"
  "Lib"

begin 

― ‹‹open import Pervasives››
― ‹‹open import Pervasives_extra››
― ‹‹open import Lib››

― ‹‹ An oracle says how to perform an ffi call based on its internal state,
* represented by the type variable 'ffi. ››

datatype 'ffi oracle_result = Oracle_return " 'ffi " " 8 word list " | Oracle_diverge | Oracle_fail
type_synonym 'ffi oracle_function =" 'ffi ⇒ 8 word list ⇒ 8 word list ⇒ 'ffi oracle_result "
type_synonym 'ffi oracle0 =" string ⇒ 'ffi oracle_function "

― ‹‹ 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. ››

datatype io_event = IO_event " string " " 8 word list " " ( (8 word * 8 word)list)"

datatype ffi_outcome = FFI_diverged | FFI_failed
datatype final_event = Final_event " string " " 8 word list " " 8 word list " " ffi_outcome "

datatype_record 'ffi ffi_state =

 oracle0      ::" 'ffi oracle0 "
 
 ffi_state   ::" 'ffi "
 
 final_event ::"  final_event option "
 
 io_events   ::" io_event list "
 


― ‹‹val initial_ffi_state : forall 'ffi. oracle 'ffi -> 'ffi -> ffi_state 'ffi››
definition initial_ffi_state  :: "(string ⇒ 'ffi oracle_function)⇒ 'ffi ⇒ 'ffi ffi_state "  where 
     " initial_ffi_state oc ffi1 = (
(| oracle0      = oc
 , ffi_state   = ffi1
 , final_event = None
 , io_events   = ([])
 |) )"


― ‹‹val call_FFI : forall 'ffi. ffi_state 'ffi -> string -> list word8 -> list word8 -> ffi_state 'ffi * list word8››
definition call_FFI  :: " 'ffi ffi_state ⇒ string ⇒(8 word)list ⇒(8 word)list ⇒ 'ffi ffi_state*(8 word)list "  where 
     " call_FFI st s conf bytes = (
  if ((final_event   st) = None) ∧ ¬ (s = ('''')) then
    (case (oracle0   st) s(ffi_state   st) conf bytes of
      Oracle_return ffi' bytes' =>
        if List.length bytes' = List.length bytes then
          (( st (| ffi_state := ffi'
                    , io_events :=
                        ((io_events   st) @
                          [IO_event s conf (zipSameLength bytes bytes')])
            |)), bytes')
        else (( st (| final_event := (Some (Final_event s conf bytes FFI_failed)) |)), bytes)
    | Oracle_diverge =>
          (( st (| final_event := (Some (Final_event s conf bytes FFI_diverged)) |)), bytes)
    | Oracle_fail =>
        (( st (| final_event := (Some (Final_event s conf bytes FFI_failed)) |)), bytes)
    )
  else (st, bytes))"


datatype outcome = Success | Resource_limit_hit | FFI_outcome " 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. ››
datatype  behaviour =
    ― ‹‹ 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 "  io_event llist "
    ― ‹‹ Terminating executions can only perform a finite number of
       FFI calls. The execution can be terminated by a non-returning
       FFI call. ››
  | Terminate " outcome " " io_event list "
    ― ‹‹ 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)››
definition trace_oracle  :: " string ⇒(io_event)llist ⇒(8 word)list ⇒(8 word)list ⇒((io_event)llist)oracle_result "  where 
     " trace_oracle s io_trace conf input1 = (
  (case  lhd' io_trace of
    Some (IO_event s' conf' bytes2) =>
      if (s = s') ∧ ((List.map fst bytes2 = input1) ∧ (conf = conf')) then
        Oracle_return (Option.the (ltl' io_trace)) (List.map snd bytes2)
      else Oracle_fail
  | _ => Oracle_fail
  ))"

end