Top level effects

Writer: JP. Following a discussion with: NS & CF on 05/02/2016.

This is still a proposal for making F*'s module-level/top-level effects sound.

For some discussion on this please see: https://github.com/FStarLang/FStar/issues/143

Top-level effects in F★

Module pre- and post-conditions

Each module directive can now have an effect and pre- and post-conditions. For instance:

module F: ST unit
  (fun h → ...)
  (fun h₀ () h₁ -> ...)

The post-condition is free to reference top-level bindings. For instance:

module F: ST unit
  (fun h → ...)
  (fun h₀ () h₁ -> Heap.get h₁ ctr = 0)

let ctr = Heap.alloc 0

It's as if the post-condition was written at the bottom of the file; for convenience, we keep everything grouped together.

Top-level effect have arbitrary pre- and post-conditions

Previously, top-level effects could only have trivial pre-conditions, and their post-conditions were discarded. Now:

module F: ST unit P Q

// { P₀ }
let x₁ = …
// { P₁ }
…
let xₙ = …
// { Pₙ }

We check that P ⇒ P₀ and that Pₙ => Q.

Soundness now depends on termination and proper link-time order

This comes with the caveat that if your module is in ST and its load doesn't terminate, then modules that depend on F may as well prove false. If you depend on modules whose top-level effect include DIV, then whatever you prove only holds as long as you can successfully extract and run your program and see it terminate without throwing.

Furthermore, the results are only valid as long as the OCaml link-time order is compatible with the F* dependency order. To that effect, if module G: ST unit (requires F.something) (ensures true), then extraction will generate:

F.ml:

let dummy = ()

G.ml:

let () = F.dummy

to make sure that OCaml errors out if the user messes up their ocamlopt invocation.

Backpatching

A module is actually free to backpatch another module:

module G: ST unit
  (requires true)
  (ensures (fun _ unit h₁ -> Heap.get h₁ F.ctr = 0))

let _ =
  F.ctr := 0

Interaction with monotonic references

Once G has backpatched F, then H may depend on the monotonic property hat the counter will always increase, through H's requires clause. However, every effectful function from H will have to testify said property (there is currently no syntactic sugar to automatically testify monotonic references that are in a module's pre-condition).