Changing the SteelCore semantics and the Steel libraries to use tokens for invariants

[nikswamy]

In response to issue #2814 , this PR revises the monotonic state effect in FStar.MST and MSTTotal to use an explicit token for the witnessed predicate.

This change bubbles up through to Steel as an explicit token for invariants too.

Recapping the changes here, as discussed also on #2814

• The main change is that inv p is now also an explicit token of type Type0 and the i >--> p prop is no longer visible in the Steel.Memory interface.

• Additionally, the libraries that provide monotonic references are changed to provide their own witnessed tokens, rather than just providing prop-based witnesses.

• The new_invariant, with_invariant and with_invariant_g operations are no longer ghost, since this would allow them to reveal an erased (witnessed p) as a witnessed p and break the abstraction. Instead, with_invariant_g is now classified as SteelAtomic unobservable and with_invariariant is parametric in the observability flag of computation it takes as argument.

• All the Steel files (except one, noted below) in the F* repo work again without significant change. Also, the Zeta project is also not significantly impacted.

• However, the this change results in a loss of expressiveness since it is no longer possible to turn an invariant into an slprop/vprop. That is, pure (i >--> p) is no longer expressible in the Steel---you need an explicit invariant token inv p. This results in a change to the style used in specifying the invariant of a lock-coupling list in Steel.LockCoupling.fsti. That invariants is now phrased using a combination of a inductive type that simultaneously specifies the type of a list cell and the invariant that the lock protects, combined with a recursive predicate on that structure, where the two interact via the use of fractional permissions.

• We also have extraction support for invariant-related constructs in F*. It is important from the F* type checker's perspective that witnessed and hence inv is not an erasable type. However, for concrete executions, these tokens have no information content (since they are only eliminated by recall, an axiom). So, in FStar.Extraction.ML.Term, applying to extracting Steel to both OCaml and C, we now

  • extract inv p​ to unit​
  • extract (with_invariant_g ... (fun _ -> some ghost function)​) to ()​
  • extract (with_invariant ... f​) to f()​.

With these changes, the extraction behavior is mostly unchanged:

For example,

let test (_:unit)
  : STT (inv emp & nat) emp (fun _ -> emp)
  = let i = new_invariant emp in
    i, 17

is extracted to ML as

let (test : unit -> (unit * Prims.nat)) =
  fun uu___ -> ((), (Prims.of_int (17)))

and via krml (which does unit elimination) to C as

Prims_int TestDTup_test(void)
{
  return (krml_checked_int_t)17;
}

[tahina-pro]

Thanks Nik for merging.
I took care of pushing a release recording the last state of F* before merging this PR: https://github.com/FStarLang/FStar/releases/tag/v2023.02.01