A simple CakeML CF spec involving references

ex2Script.sml

open preamble basis

val _ = translation_extends "basisProg";

val ex2 = process_topdecs`
  fun ex2 x r = let val r' = ref r in r := x; !r' end`;

val () = append_prog ex2;

val st2 = get_ml_prog_state();

val ex2_spec = Q.prove(`
  !xv rv.
   app (p:'ffi ffi_proj) ^(fetch_v "ex2" st2) [xv; rv]
   (REF rv x'v) (POSTv v. SEP_EXISTS r'v. & (v = rv) * REF rv xv * REF r'v rv)`,
  xcf "ex2" st2 \\
  xlet `POSTv r'v. REF rv x'v * REF r'v rv` THEN1 (xref \\ xsimpl) \\
  xlet `POSTv uv. &UNIT_TYPE () uv * REF rv xv * REF r'v rv`
  >- ( xapp \\ xsimpl )
  \\ xapp
  \\ xsimpl
  \\ qexists_tac`r'v`
  \\ xsimpl);