Merge pull request #56 from mtzguido/misc

Misc

lib/pulse/core/PulseCore.FractionalPermission.fst

@@ -18,51 +18,14 @@ module PulseCore.FractionalPermission
 
 include FStar.Real
 
-open FStar.Real
-
 /// This module defines fractional permissions, to be used with Steel references
 
 /// A fractional permission is a real value between 0 (excluded) and 1.
 /// 1 represents full ownership, while any fraction corresponds to a shared
 /// permission.
-/// Note: Does not use real literals, but rather the wrappers one, zero, two, …
-/// Real literals are currently not supported by Meta-F*'s reflection framework
+///
+/// We do not in fact restrict to <= 1 here, so there are no additional constraints
+/// when writing something like `p1+p2`, but every library does in fact limit
+/// permissions to 1.0R.
 [@@ erasable]
 type perm : Type0 = r:real { r >. zero }
-
-// /// A reference is only safely writeable if we have full permission
-// let writeable (p: perm) : prop = p == one
-
-// /// Helper around splitting a permission in half
-// let half_perm (p: perm) : Tot perm = p /. two
-
-// /// Helper to combine two permissions into one
-// let sum_perm (p1 p2: perm) : Tot perm = p1 +. p2
-
-// /// Helper to compare two permissions
-// let lesser_equal_perm (p1 p2:perm) : prop = p1 <=. p2
-
-// let lesser_perm (p1 p2:perm) : prop = p1 <. p2
-
-// /// Wrapper around the full permission value
-// let full_perm : perm = 1.0R
-
-// /// Complement of a permission
-// let comp_perm (p:perm{p `lesser_perm` full_perm}) : GTot perm =
-//   1.0R -. p
-
-// /// A convenience lemma
-// let sum_halves (p:perm)
-//   : Lemma (sum_perm (half_perm p) (half_perm p) == p)
-//           [SMTPat (sum_perm (half_perm p) (half_perm p))]
-//   = assert (forall (r:real). r /. 2.0R +. r /. 2.0R == r)
-
-// let sum_comp (p:perm{p `lesser_perm` full_perm})
-//   : Lemma (sum_perm p (comp_perm p) == full_perm)
-//           [SMTPat (sum_perm p (comp_perm p))]
-//   = ()
-
-// let sum_lemma (f1 f2 : perm)
-//   : Lemma (sum_perm (half_perm f1) (half_perm f2) == half_perm (sum_perm f1 f2))
-//           [SMTPat (sum_perm (half_perm f1) (half_perm f2))]
-//   = assert (forall x y. (x +. y) /. 2.0R == x /. 2.0R +. y /. 2.0R)

share/pulse/examples/dice/Makefile

@@ -47,7 +47,7 @@ test-c: verify
 # files. If so, then this %.ast rule will be generic and can move to
 # share/pulse/Makefile.include-base.
 %.ast:
-	$(FSTAR) --admit_smt_queries true --warn_error -241 --codegen Extension $(subst .ast,, $(notdir $@)) --extract_module $(basename $(subst .ast,, $(notdir $@)))
+	$(FSTAR) $(OTHERFLAGS) --admit_smt_queries true --warn_error -241 --codegen Extension $(subst .ast,, $(notdir $@)) --extract_module $(basename $(subst .ast,, $(notdir $@)))
 
 DPE_FILES = EngineTypes.fst \
   EngineCore.fst \