typestate.fst

module Typestate

open FStar.Heap
open FStar.ST

type state = 
  | Open
  | Closed

type file = {
    name: string;
    state: ref state;
}

type isClosed file heap = (sel heap file.state) == Closed
type isOpen file heap = (sel heap file.state) == Open

val openHelper : file:file -> ST unit
    (requires (fun heap -> isClosed file heap))
    (ensures (fun heap _ heap' ->
        isOpen file heap'
        ))
let openHelper file =
    file.state := Open

val read : file:file -> ST int
    (requires (fun heap -> isOpen file heap))
    (ensures (fun heap _ heap' -> isOpen file heap'))
let read file =
    13

val computeBase : unit -> Tot int
let computeBase () =
    12

val readFromFile : file:file -> ST int
    (requires (fun heap -> isClosed file heap))
    (ensures (fun heap s heap' -> isClosed file heap'))
let readFromFile file =
    openHelper file;
    let x = computeBase () + read file in
    file.state := Closed;
    x

let () =
    let file1 = {
        name = "file1";
        state = alloc Closed;
    } in

    let y = readFromFile file1 in
    ()