Making Reals erasable, and providing a reflection API for real literals

[mtzguido]

Our FStar.Real module did not make much sense, in that it supported decidable operations (like equality) over arbitrary reals, and a total of_string operation to make a real from a string (although this was uninterpreted logically, so not unsound, but it also did not have a runtime implementation).

This PR makes the real type erasable, and removes the of_string operation and the extraction rules for reals (which would never be triggered now).

It also adds them to the vconst view that Meta-F* exposes.

[mtzguido]

This will help in using literal real permissions in pulse, replacing half_perm (half_perm full_perm) by 0.25R, etc. In fact, just using coercions between reals and perms almost does the trick, except that it requires many more rewrites since Pulse will not unify real_to_perm 1.0 and full_perm (though it may soon, if we make it call the unifier).

[mtzguido]

Updated to put the comparison operations in prop instead of GTot bool. Conceptually, putting them in GTot bool would make use of the strong excluded middle axiom, which a user may want to avoid. Though with the current interface it does not really make a difference (one can only construct rational combinations of 1 and sqrt(2), so it could in fact be decidable).

But, with more ways to construct reals (if we do not restrict to a computable subset, which I expect we won't as we are using Z3's real theory), it may be that one can recover the strong excluded middle from these GTot bool operations. I have a hard time thinking how such a proof would go... but using prop feels like the right thing to do.

It does impact Pulse slightly, the following patch would be needed:

diff --git a/lib/pulse/core/PulseCore.FractionalPermission.fst b/lib/pulse/core/PulseCore.FractionalPermission.fst
index 5ec4d7e2..b5d61535 100644
--- a/lib/pulse/core/PulseCore.FractionalPermission.fst
+++ b/lib/pulse/core/PulseCore.FractionalPermission.fst
@@ -31,4 +31,4 @@ noeq type perm : Type0 =
 /// A reference is only safely writeable if we have full permission
-let writeable (p: perm) : GTot bool =
-  MkPerm?.v p = one
+let writeable (p: perm) : prop =
+  MkPerm?.v p == one
 
@@ -43,6 +43,6 @@ let sum_perm (p1 p2: perm) : Tot perm =
 /// Helper to compare two permissions
-let lesser_equal_perm (p1 p2:perm) : GTot bool =
+let lesser_equal_perm (p1 p2:perm) : prop =
   MkPerm?.v p1 <=.  MkPerm?.v p2
 
-let lesser_perm (p1 p2:perm) : GTot bool =
+let lesser_perm (p1 p2:perm) : prop =
   MkPerm?.v p1 <.  MkPerm?.v p2
diff --git a/lib/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst b/lib/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst
index 4b44db28..069d4332 100644
--- a/lib/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst
+++ b/lib/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst
@@ -137,6 +137,2 @@ type knowledge (#v:Type) (#p:preorder v) (anchors:anchor_rel p) =
 
-let b2p (b:bool)
-  : prop
-  = b == true
-
 /// Fractional permissions are composable when their sum <= 1.0
@@ -147,4 +143,4 @@ let perm_opt_composable (p0 p1:option perm)
     | Some p, None
-    | None, Some p -> b2p (p `lesser_equal_perm` full_perm)
-    | Some p0, Some p1 -> b2p (sum_perm p0 p1 `lesser_equal_perm` full_perm)
+    | None, Some p -> p `lesser_equal_perm` full_perm
+    | Some p0, Some p1 -> sum_perm p0 p1 `lesser_equal_perm` full_perm
 
diff --git a/lib/pulse/lib/Pulse.Lib.PCM.Fraction.fst b/lib/pulse/lib/Pulse.Lib.PCM.Fraction.fst
index f0a04952..83a4f271 100755
--- a/lib/pulse/lib/Pulse.Lib.PCM.Fraction.fst
+++ b/lib/pulse/lib/Pulse.Lib.PCM.Fraction.fst
@@ -45,3 +45,3 @@ let mk_frame_preserving_upd_none
 
-let perm_ok p : prop = (p.v <=. one == true)
+let perm_ok p : prop = p.v <=. one
 
diff --git a/share/pulse/examples/by-example/PulseTutorial.Ref.fst b/share/pulse/examples/by-example/PulseTutorial.Ref.fst
index 92593edb..45b082c1 100755
--- a/share/pulse/examples/by-example/PulseTutorial.Ref.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.Ref.fst
@@ -207,3 +207,3 @@ ensures
 fn max_perm #a (r:ref a) #p anything
-requires pts_to r #p 'v ** pure (not (p `lesser_equal_perm` full_perm))
+requires pts_to r #p 'v ** pure (~(p `lesser_equal_perm` full_perm))
 returns _:squash False`

Seems not too bad... thoughts?

[gebner]

Does it make sense to keep the ghost to_string function? Is there any way to execute it?

[mtzguido]

Ah good point. There's no implementation nor axioms, so probably best to just drop it.

[mtzguido]

Downstream PRs:

• FractionalPermission: Fixes for new F* real interface steel#170
• Fixes for new real numbers interface in F* pulse#50

Will merge once we confirm Steel & friends are not badly broken by this