Ghost constructors

[RustanLeino]

This RFC proposes that each constructor of a datatype can be declared to be ghost.
Declaring a constructor to be ghost limits usage of that constructor to ghost contexts and auto-initialization.
It also restricts discriminators and destructors in compiled contexts, so that it is never necessary at run time to check if a value is of a ghost variant.

[robin-aws]

Interesting idea! I'm a bit worried that this is an unintuitive interpretation of the ghost keyword in this context though. I found it surprising to read that a ghost constructor can in fact be compiled and referenced at runtime, but you are just not allowed to "do anything" with the value.

I'd love to see a motivating example where just using /definiteAssignment:3 results in really sub-optimal code to model this manually.

[robin-aws]

It sounds like this paragraph is the key motivation for this feature, so consider pulling it up to the beginning of the document. :)

Do we have any other use cases for ghost constructors in mind? It would be worth spelling out alternative ways of ensuring storage is always initialized. I recently discovered the undocumented new T[n] (i => ...) syntax for initializing arrays, which presumably could be used to explicitly assign an initial value when T is not auto-initializable. You would then have to manually spell out the pre-conditions that prevent such values from being read and used in any way, of course.

[RustanLeino]

Yes, this is the main motivating example. Here's another plausible use:

You may develop a model that uses several different variants of a datatype, say Red, Green, Yellow, and Blue. But in your running program, you only ever want to store Green or Blue values. To make sure of this, you can mark Green and Yellow as ghost constructors.

[robin-aws]

Is this an attempt to prevent ghost constructors from being used in any expression? I worry that just the fact that you can successfully read such a value at runtime already allows control flow that shouldn't be, and that this construction will be unsound in a subtle way. It sounds like the following program would be valid and halt at runtime, but I would expect the myArray[0] reference to be rejected statically, if I am trying to soundly avoid ever reading uninitialized storage:

datatype D = ghost G(x: int) | D0(y: int) | D1(z: int)

method Main() {
  var myArray := new D[5];
  var shouldNotReferenceThisAtRuntime := myArray[0];
  expect false;
}

[RustanLeino]

The rules are intended to ensure soundness. You can read and copy these "uninitialized" values at run time, but there's no way to, at run time, determine whether or not you're holding a value that has been initialized.

The assignment shouldNotReferenceThisAtRuntime := myArray[0]; in your example is legal and causes no problem at run time. If the compiler decides to initialize myArray[0] with a G value, then myArray[0] is essentially some rubbish that you should do anything with. But it's fine and safe to copy this rubbish into another variable.

(Btw, not that it changes the example, but just to point out that the compiler is also free to initialize myArray[0] with a D0 or D1 value. Still, there's no way to determine at run time if that's what the compiler did.)