Improving erasure

[nikswamy]

Working with erased types in F* can be quite cumbersome. Can we identify some of the pain points and find ways to improve it?

Here's a start:

Inference of implicit arguments that have ghost effect does not work, even when the resulting type is non-informative.

//We have a simple indexed type
type t (n:nat) = m:nat{m == n}

//And a function that takes the index as an implicit argument
//returning a non-informative type, e.g., unit, Type, G.erased ...
let f (#x:nat) (y:t x) : unit = ()

//Now, if you call f with an explicit argument, it's fine
let test (x:G.erased nat) (y:t (G.reveal x)) : unit = f #(Ghost.reveal x) y

//But, leave it implicit and although F* infers the same elaboration
//as the term above it rejects it
[@expect_failure]
let test2 (x:G.erased nat) (y:t (G.reveal x)) : unit = f y

This is now fixed in master, see examples/micro-benchmarks/GhostImplicits.fst. The idea is that in phase1, we allow implicit arguments to be resolved to ghost computations, since in phase2 the elaborated term will be checked again for effect correctness.

That said, in computationally relevant contexts, code like test2 is still rejected.

//But, if you have a function that is not computationally irrelevant,
//then instantiating its implicits to ghost terms should fail
let g (#x:nat) (y:t x) : nat = y

//But, leave it implicit and although F* infers the same elaboration
//as the term above it rejects it
[@(expect_failure [34])]
let test3 (x:G.erased nat) (y:t (G.reveal x)) : nat = g y

The set of erased types is fixed

Currently, this is the class of types that F* will erase:

   must_erase ::= unit
               | Type
               | FStar.Ghost.erased t
               | x:must_erase{t'}            //any refinement of a must_erase type
               | t1..tn -> PURE must_erase _ //any pure function returning a must_erase type
               | t1..tn -> GHOST t' _        //any ghost function

If you have some other type that you would like to erase, aside from wrapping that type in Ghost.erased, you're out of luck.

The module FStar.Ghost and its main type erased have special status in the compiler. Instead, let's make the notion of must_erase types extemsible using an attribute.

Specifically, let's add an attribute FStar.Pervasives.must_erase which can be used to decorate an inductive type definition.

E.g., one could write

[@must_erase]
type t = {
   a:nat;
   b:bool
}

A must_erase type comes with the following elimination restriction:

• Any pattern matching on a value of a must-erase type has Ghost effect. E.g, you can only define projectors for the fields of t above in the Ghost effect, not in Pure. This is analogous to a restriction on eliminating Prop to Type in Coq.

In return, F* will treat t as non-informative in computationally relevant contexts and erase it during extraction.

The benefit is that in computationally irrelevant contexts, constructing and destructing t's is easy: there's no need to go via the indirection of a Ghost.reveal and Ghost.hide.

By giving special treatment to the must_erase attribute, we no longer need to give special status to FStar.Ghost.erased. It can simply be defined as:

[@must_erase]
type erased a = { v : a }

Ghost.reveal and hide need to be written explicitly

With the use of must_erase attribute, perhaps our reliance on Ghost.erased and its corresponding reveal/hide will be reduced. However, I expect we will continue to use Ghost.erased, e.g., to easily define must_erase variants of existing types. E.g., erased nats, or erased lists etc.

How about extending our existing (though limited) support for the b2t coercion to allow implicitly coercing between a and erased a (via hide) and back via reveal?

This may make erasure more palatable ... but perhaps also harder to predict.

Erasure is type directed rather than semantic

Going back to this example:

//But, if you have a function that is not computationally irrelevant,
//then instantiating its implicits to ghost terms should fail
let g (#x:nat) (y:t x) : nat = y

//But, leave it implicit and although F* infers the same elaboration
//as the term above it rejects it
[@(expect_failure [34])]
let test3 (x:G.erased nat) (y:t (G.reveal x)) : nat = g y

One could argue that test3 (or its elaboration g #(Ghost.reveal x) y) should succeed, since g really does not depend on the value of x at all.

This one is harder to solve. Should the programmer have instead explicitly requested erasure by writing

let h (#x:erased nat) (y:t (G.reveal x)) : nat = y

? But that's much more cumbersome to write. Perhaps with coercion insertion for reveal/hide it might not be so bad

let h (#x:erased nat) (y:t x) : nat = y

Other problems with erasure?

[nikswamy]

Points raised during an F* weekly call:

• Tahina mentions that must_erase could be used to do inductive predicates more easily.

• Guido mentions that must_erase should imply noeq. We also discussed that typechecking pattern matching should be careful about unfolding types, perhaps by using the type of the pattern rather than the type of the scrutineer to drive the restricted pattern matching on must_erase types.

• Jay mentions that having some reuse of Tot and GTot, perhaps with some kind of effect polymorphism for just these two cases?

• Denis mentions that to use must_erase with in steel, we may need to revise canonizers to use GTot monoids, rather than Tot monoids. Danel mentioned that he has an experiment to use erased resources already: https://github.com/FStarLang/FStar/blob/danel_lowstar_lens/ulib/LowStar.Resource.Erased.fst https://github.com/FStarLang/FStar/blob/danel_lowstar_lens/ulib/LowStar.RST.Erased.fst https://github.com/FStarLang/FStar/blob/danel_lowstar_lens/ulib/LowStar.RST.LinkedList.Erased.fst

• Guido has a branch with some support for extensible coercions. We could apply this to reveal/hide

  • Some discussion about this:
    • Would be very useful, e.g. Jay reports writing 297 reveals in his doubly linked list code (!)
    • Aseem noted that inserting reveals would incur implicit ghost effects which may be counterintuitive
    • We should find a way to report better localized effect inconsistency errors, blaming the smallest subterm

• Antoine mentioned using erasing top-level terms using noextract/inline_for_extraction

  • The combination is used for removing unused function definitions (perhaps noextract could be implied by inline_for_extraction)

• Antoine mentioned that crypto code uses a mixture of ghost (unconditional erasure), ideal (conditional erasure), and real code. Could there be language support for conditional erasure?

• What about ghost state?

  • ref (erased t)? Santiago may have some experience using this

---

Main takeaways for now

• I will implement the must_erase attribute
• Guido will add reveal/hide to coercion insertion work

Meanwhile, please feel free to write in with more insights about how erasure works today and how it might work better in the future.

[mtzguido]

I revived my coercions branch and added logic for hide/reveal. The following file works in guido_coerce:

module Coercions

open FStar.Ghost

[@(expect_failure [34])]
let test0 (x: erased int) : Tot int = x

let test1 (x: erased int) : GTot int = x

let test2 (x:int) : erased int = x

let test3 (x:erased int) : erased int = x

let test4 (x:erased int) : GTot (erased int) = x

let test5 (x:int) : GTot (erased int) = x

Though unrelated to this issue, there's also inspect_ln/pack_ln for tactics, the following works too:

module Coercions

open FStar.Tactics

let tm : term = Tv_App (Tv_App (`op_Addition) (`1, Q_Explicit)) (`2, Q_Explicit)

let basic : int =
  match tm with
  | Tv_App l _ -> 1
  | _ -> 2

let one : option term =
  match tm with
  | Tv_App l _ -> begin match l with
                  | Tv_App _ (x, _) -> Some x
                  | _ -> None
                  end
  | _ -> None

let two : option term =
  match tm with
  | Tv_App _ (x, _) -> Some x
  | _ -> None

But no deep matches (yet), as discussed

[jaybosamiya]

@mtzguido a good test for usability in Tot functions that call lemmas might be the following:

assume val p : int -> prop
assume val foo (x:int) : Lemma (ensures (p x))

let bar (x:erased int) : Tot unit =
  foo (reveal x);
  assert (p (reveal x))

let test_bar (x:erased int) : Tot unit =
  foo x;
  assert (p x)

I think this should be covered by test 2, but I thought I'd still request it be added to the list of tests, since it tests coercion at the point of application (I'm unaware if this is relevant to how coercion works, which is why I requested this test be added).

I believe the rest of the cases where reveal/hide is used within the doubly linked list code is covered by all of your tests.

[mtzguido]

Thanks Jay. Indeed those work too, and I added them.

[nikswamy]

This looks great @mtzguido ... thanks! Do you want to create a pull request towards merging this to master?

[mtzguido]

Yes! Doing so now.

[mtzguido]

1851