forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
runtimeFFIScript.sml
40 lines (30 loc) · 912 Bytes
/
runtimeFFIScript.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
(*
Logical model of the Runtime module's exit function calls.
*)
open preamble
cfHeapsBaseTheory
val _ = new_theory"runtimeFFI";
val ffi_exit_def = Define `
ffi_exit (conf:word8 list) (bytes:word8 list) () = SOME(FFIdiverge:unit ffi_result)
`
Theorem ffi_exit_length:
ffi_exit (conf:word8 list) (bytes:word8 list) u = SOME (FFIreturn bytes' args')
==> LENGTH bytes' = LENGTH bytes
Proof
Cases_on `u` \\ rw[ffi_exit_def]
QED
(* FFI part for the runtime *)
val encode_def = Define `encode = K (List []):unit -> ffi`;
val decode_def = Define `decode = (K(SOME ())):ffi -> unit option`
val encode_11 = prove(
``!x y. encode x = encode y <=> x = y``,
rw [encode_def]);
Theorem decode_encode:
decode(encode cls) = SOME cls
Proof
rw[decode_def,encode_def]
QED
val runtime_ffi_part_def = Define`
runtime_ffi_part = (encode,decode,
[("exit",ffi_exit)])`;
val _ = export_theory();