From 61d26a8a93684cc88ce21abc193fda00e86149b3 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 16 Dec 2024 15:39:10 -0800
Subject: [PATCH 1/2] Remove FStar.Ghost.Pull
---
ulib/.hints/FStar.Ghost.Pull.fsti.hints | 1 -
ulib/FStar.Cardinality.Cantor.fst | 2 +-
ulib/FStar.Cardinality.Universes.fst | 4 +--
ulib/FStar.Functions.fst | 14 +++++------
ulib/FStar.Functions.fsti | 30 +++++++++++-----------
ulib/FStar.Ghost.Pull.fsti | 33 -------------------------
6 files changed, 25 insertions(+), 59 deletions(-)
delete mode 100644 ulib/.hints/FStar.Ghost.Pull.fsti.hints
delete mode 100644 ulib/FStar.Ghost.Pull.fsti
diff --git a/ulib/.hints/FStar.Ghost.Pull.fsti.hints b/ulib/.hints/FStar.Ghost.Pull.fsti.hints
deleted file mode 100644
index 46e84f430d5..00000000000
--- a/ulib/.hints/FStar.Ghost.Pull.fsti.hints
+++ /dev/null
@@ -1 +0,0 @@
-[ "ˆ\\=O?uÞ\u000eÚ!ªk}\u000b", [] ]
\ No newline at end of file
diff --git a/ulib/FStar.Cardinality.Cantor.fst b/ulib/FStar.Cardinality.Cantor.fst
index 4f2ee440157..349cd6ee246 100644
--- a/ulib/FStar.Cardinality.Cantor.fst
+++ b/ulib/FStar.Cardinality.Cantor.fst
@@ -18,7 +18,7 @@ let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) =
let no_inj_powerset (a : Type) (f : powerset a -> a) : Lemma (~(is_inj f)) =
let aux () : Lemma (requires is_inj f) (ensures False) =
- let g : a -> powerset a = inverse_of_inj f (fun _ -> false) in
+ let g : a -> GTot (powerset a) = inverse_of_inj f (fun _ -> false) in
no_surj_powerset a g
in
Classical.move_requires aux ()
diff --git a/ulib/FStar.Cardinality.Universes.fst b/ulib/FStar.Cardinality.Universes.fst
index 146820b0387..5eb0e8bafa1 100644
--- a/ulib/FStar.Cardinality.Universes.fst
+++ b/ulib/FStar.Cardinality.Universes.fst
@@ -6,8 +6,8 @@ open FStar.Cardinality.Cantor
(* This type is an injection of all powersets of Type u (i.e. Type u -> bool
functions) into Type (u+1) *)
noeq
-type type_powerset : (Type u#a -> bool) -> Type u#(max (a+1) b) =
- | Mk : f:(Type u#a -> bool) -> type_powerset f
+type type_powerset : (Type u#a -> GTot bool) -> Type u#(max (a+1) b) =
+ | Mk : f:(Type u#a -> GTot bool) -> type_powerset f
let aux_inj_type_powerset (f1 f2 : powerset (Type u#a))
: Lemma (requires type_powerset u#a u#b f1 == type_powerset u#a u#b f2)
diff --git a/ulib/FStar.Functions.fst b/ulib/FStar.Functions.fst
index 4c4ab58e3e5..7410ff4326b 100644
--- a/ulib/FStar.Functions.fst
+++ b/ulib/FStar.Functions.fst
@@ -1,21 +1,21 @@
module FStar.Functions
-let inj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+let inj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
: Lemma (requires is_inj f /\ is_inj g)
(ensures is_inj (fun x -> g (f x)))
= ()
-let surj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+let surj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
: Lemma (requires is_surj f /\ is_surj g)
(ensures is_surj (fun x -> g (f x)))
= ()
-let bij_comp (#a #b #c : _) (f : a -> b) (g : b -> c) :
+let bij_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c) :
Lemma (requires is_bij f /\ is_bij g)
(ensures is_bij (fun x -> g (f x)))
= ()
-let lem_surj (#a #b : _) (f : a -> b) (y : b)
+let lem_surj (#a #b : _) (f : a -> GTot b) (y : b)
: Lemma (requires is_surj f) (ensures in_image f y)
= ()
@@ -30,11 +30,11 @@ let inverse_of_bij #a #b f =
assert (g0 (f x) == x)
in
Classical.forall_intro aux;
- Ghost.Pull.pull g0
+ g0
let inverse_of_inj #a #b f def =
(* f is a bijection into its image, obtain its inverse *)
- let f' : a -> image_of f = fun x -> f x in
+ let f' : a -> GTot (image_of f) = fun x -> f x in
let g_partial = inverse_of_bij #a #(image_of f) f' in
(* extend the inverse to the full domain b *)
let g : b -> GTot a =
@@ -43,4 +43,4 @@ let inverse_of_inj #a #b f def =
then g_partial y
else def
in
- Ghost.Pull.pull g
+ g
diff --git a/ulib/FStar.Functions.fsti b/ulib/FStar.Functions.fsti
index ff92a23fe47..9982dc4ddf5 100644
--- a/ulib/FStar.Functions.fsti
+++ b/ulib/FStar.Functions.fsti
@@ -3,51 +3,51 @@ module FStar.Functions
(* This module contains basic definitions and lemmas
about functions and sets. *)
-let is_inj (#a #b : _) (f : a -> b) : prop =
+let is_inj (#a #b : _) (f : a -> GTot b) : prop =
forall (x1 x2 : a). f x1 == f x2 ==> x1 == x2
-let is_surj (#a #b : _) (f : a -> b) : prop =
+let is_surj (#a #b : _) (f : a -> GTot b) : prop =
forall (y:b). exists (x:a). f x == y
-let is_bij (#a #b : _) (f : a -> b) : prop =
+let is_bij (#a #b : _) (f : a -> GTot b) : prop =
is_inj f /\ is_surj f
-let in_image (#a #b : _) (f : a -> b) (y : b) : prop =
+let in_image (#a #b : _) (f : a -> GTot b) (y : b) : prop =
exists (x:a). f x == y
-let image_of (#a #b : _) (f : a -> b) : Type =
+let image_of (#a #b : _) (f : a -> GTot b) : Type =
y:b{in_image f y}
(* g inverses f *)
-let is_inverse_of (#a #b : _) (g : b -> a) (f : a -> b) =
+let is_inverse_of (#a #b : _) (g : b -> GTot a) (f : a -> GTot b) =
forall (x:a). g (f x) == x
-let powerset (a:Type u#aa) : Type u#aa = a -> bool
+let powerset (a:Type u#aa) : Type u#aa = a -> GTot bool
-val inj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+val inj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
: Lemma (requires is_inj f /\ is_inj g)
(ensures is_inj (fun x -> g (f x)))
-val surj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+val surj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
: Lemma (requires is_surj f /\ is_surj g)
(ensures is_surj (fun x -> g (f x)))
-val bij_comp (#a #b #c : _) (f : a -> b) (g : b -> c) :
+val bij_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c) :
Lemma (requires is_bij f /\ is_bij g)
(ensures is_bij (fun x -> g (f x)))
-val lem_surj (#a #b : _) (f : a -> b) (y : b)
+val lem_surj (#a #b : _) (f : a -> GTot b) (y : b)
: Lemma (requires is_surj f) (ensures in_image f y)
(* An bijection has a perfect inverse. *)
-val inverse_of_bij (#a #b : _) (f : a -> b)
- : Ghost (b -> a)
+val inverse_of_bij (#a #b : _) (f : a -> GTot b)
+ : Ghost (b -> GTot a)
(requires is_bij f)
(ensures fun g -> is_bij g /\ g `is_inverse_of` f /\ f `is_inverse_of` g)
(* An injective function has an inverse (as long as the domain is non-empty),
and this inverse is surjective. *)
-val inverse_of_inj (#a #b : _) (f : a -> b{is_inj f}) (def : a)
- : Ghost (b -> a)
+val inverse_of_inj (#a #b : _) (f : a -> GTot b{is_inj f}) (def : a)
+ : Ghost (b -> GTot a)
(requires is_inj f)
(ensures fun g -> is_surj g /\ g `is_inverse_of` f)
diff --git a/ulib/FStar.Ghost.Pull.fsti b/ulib/FStar.Ghost.Pull.fsti
deleted file mode 100644
index 12c27879e95..00000000000
--- a/ulib/FStar.Ghost.Pull.fsti
+++ /dev/null
@@ -1,33 +0,0 @@
-module FStar.Ghost.Pull
-
-(**
- [pull] is an axiom.
-
- It type states that for any ghost function ``f``, we can exhibit a
- total function ``g`` that is pointwise equal to ``f``. However, it
- may not be possible, in general, to compute ``g`` in a way that
- enables it to be compiled by F*. So, ``pull f`` itself has ghost
- effect, indicating that applications of ``pull`` cannot be used in
- compilable code.
-
- Alternatively, one can think of `pull` as saying that the GTot
- effect is idempotent and non-dependent, meaning that if evaluating
- `f` on an argument `v:a`, exhibits an effect `GTot` and returns a
- result; then the effect does not depend on `v` and it can be
- subsumed to exhibiting the effect first and then computing `f v`
- purely.
-
- In other words, it "pulls" the effect out of `f`.
-
- pull is useful to mimic a kind of Tot/GTot effect polymorphism.
-
- E.g., if you have `f: a -> GTot b` and a `l:list a`
- you can do List.map (pull f) l : GTot (list b)
- *)
-val pull (#a:Type) (#b:a -> Type) (f: (x:a -> GTot (b x)))
- : GTot (x:a -> b x)
-
-val pull_equiv (#a:Type) (#b:a -> Type) (f: (x:a -> GTot (b x))) (x:a)
- : Lemma (ensures pull f x == f x)
- [SMTPat (pull f x)]
-
From 77f5528904df4be6c5d4253737f187d75ada4e0d Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 16 Dec 2024 16:02:14 -0800
Subject: [PATCH 2/2] snap
---
ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml | 9 +++------
ocaml/fstar-lib/generated/FStar_Functions.ml | 2 +-
2 files changed, 4 insertions(+), 7 deletions(-)
diff --git a/ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml b/ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml
index 83ef61cc385..bca8bdc5e0f 100644
--- a/ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml
+++ b/ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml
@@ -1,8 +1,5 @@
open Prims
type 'dummyV0 type_powerset =
- | Mk of (unit -> Prims.bool)
-let (uu___is_Mk : (unit -> Prims.bool) -> unit type_powerset -> Prims.bool) =
- fun uu___ -> fun projectee -> true
-let (__proj__Mk__item__f :
- (unit -> Prims.bool) -> unit type_powerset -> unit -> Prims.bool) =
- fun uu___ -> fun projectee -> match projectee with | Mk f -> f
\ No newline at end of file
+ | Mk of unit
+let (uu___is_Mk : unit -> unit type_powerset -> Prims.bool) =
+ fun uu___ -> fun projectee -> true
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Functions.ml b/ocaml/fstar-lib/generated/FStar_Functions.ml
index eb068c194ea..24561405f25 100644
--- a/ocaml/fstar-lib/generated/FStar_Functions.ml
+++ b/ocaml/fstar-lib/generated/FStar_Functions.ml
@@ -5,4 +5,4 @@ type ('a, 'b, 'f) is_bij = unit
type ('a, 'b, 'f, 'y) in_image = unit
type ('a, 'b, 'f) image_of = 'b
type ('a, 'b, 'g, 'f) is_inverse_of = unit
-type 'a powerset = 'a -> Prims.bool
\ No newline at end of file
+type 'a powerset = unit
\ No newline at end of file