Questions about closures and exceptions

[dariusf]

Hi, I'm trying to understand how to specify closures in F*. I tried the following program (extended from the tutorial).

val new_counter: int -> St (unit -> St int)

let new_counter init =
  let r = ST.alloc init in
  fun () ->
    r := !r + 1;
    !r

let test () =
  let c : unit -> St int = new_counter 0 in
  let x = c () in
  let y = c () in
  assert (y > x) (* (Error 19) assertion failed; The SMT solver could not prove the query. *)

The proof doesn't go through automatically, which makes sense because of the type of c (shown). How can we specify that c has a mutable reference associated with it, and what its value is?

The PLDI 2013 paper has a solution involving heap permissions (section 3.3), which I understand has been replaced with the current hyper-heaps; can the solution be translated as well?

---

Here's another example involving exceptions.

exception A

val h : (unit -> Exn unit (requires True) (ensures (fun _ -> True))) -> ML int

let h g =
  try
    g (); 2
  with _ -> 1

let test1 () =
  let z = h (fun () -> raise A) in
  assert (z = 1) (* (Error 19) assertion failed; The SMT solver could not prove the query. *)

I figure I have to refine the type of h to describe the return value, but how is "g always raises" expressed? I couldn't find any exception examples in the tutorial or book.

Thanks!

[nikswamy]

Hi @dariusf

I'm surprised that a version of the old tutorial is accessible at the URL you gave. I was under the impression that the only version published is for archival reasons and it contains a disclaimer, i.e., https://fstar-lang.org/tutorial/old/tutorial.html#sec-note--this-version-outdated. Sorry about the multiple versions: we should reconcile or remove one of them.

Your first question about closures and state is a difficult topic. You can indeed adapt that example from the PLDI 13 paper (also not valid F* today) to FStar.HyperStack, the model using in Low*. But, even that will be quite cumbersome. For reasoning about monotonic state: this paper is relevant https://arxiv.org/abs/1707.02466 And for reasoning about permissions on resources, the most powerful way of doing that in F* is to use separation logic. See here: https://www.fstar-lang.org/papers/steel/ That said, I don't have a good pre-existing example to refer you to for closures with local monotonic state in Steel ... your question is a good prompt to create such an example.

[dariusf]

Ha, I saw the disclaimer at some point too, didn't realize they were different pages.

Thanks for the pointers! I found the "counters with local state" example in the SteelCore paper and roughly get how it would be specified, at least. The monotonic state paper also looks very interesting!