From 61d26a8a93684cc88ce21abc193fda00e86149b3 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner 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 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