From c1ce71eae63e668e17d13eb98de3380b2642fb67 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 24 Jun 2025 15:04:20 -0700 Subject: [PATCH] Correctly erase functions. --- lib/steel/Steel.Effect.fsti | 4 ++-- lib/steel/Steel.Loops.fst | 2 +- lib/steel/Steel.Loops.fsti | 8 ++++---- lib/steel/Steel.ST.Loops.fst | 14 +++++++------- lib/steel/Steel.ST.Loops.fsti | 4 ++-- lib/steel/c/Steel.ST.C.Types.Scalar.fsti | 15 +++++---------- 6 files changed, 21 insertions(+), 26 deletions(-) diff --git a/lib/steel/Steel.Effect.fsti b/lib/steel/Steel.Effect.fsti index a396ddfff..73924990a 100644 --- a/lib/steel/Steel.Effect.fsti +++ b/lib/steel/Steel.Effect.fsti @@ -334,12 +334,12 @@ effect SteelT (a:Type) (pre:pre_t) (post:post_t a) = val par (#aL:Type u#a) (#aR:Type u#a) (#preL:vprop) - (#postL:aL -> vprop) + (#postL:aL -> GTot vprop) // (#lpreL:req_t preL) // (#lpostL:ens_t preL aL postL) ($f:unit -> SteelT aL preL postL) // lpreL lpostL) (#preR:vprop) - (#postR:aR -> vprop) + (#postR:aR -> GTot vprop) // (#lpreR:req_t preR) // (#lpostR:ens_t preR aR postR) ($g:unit -> SteelT aR preR postR) // lpreR lpostR) diff --git a/lib/steel/Steel.Loops.fst b/lib/steel/Steel.Loops.fst index 4e78a919b..87a6b9993 100644 --- a/lib/steel/Steel.Loops.fst +++ b/lib/steel/Steel.Loops.fst @@ -25,7 +25,7 @@ val for_loop' (start:US.t) (finish:US.t { US.v start <= US.v finish }) (current:US.t { US.v start <= US.v current /\ US.v current <= US.v finish }) - (inv: nat_at_most finish -> vprop) + (inv: nat_at_most finish -> GTot vprop) (body: (i:u32_between start finish -> SteelT unit diff --git a/lib/steel/Steel.Loops.fsti b/lib/steel/Steel.Loops.fsti index c7f1e5e3b..f6a32aa13 100644 --- a/lib/steel/Steel.Loops.fsti +++ b/lib/steel/Steel.Loops.fsti @@ -30,7 +30,7 @@ let u32_between (s f:US.t) /// for_loop: for (i = start; i < finish; i++) inv { body i } val for_loop (start:US.t) (finish:US.t { US.v start <= US.v finish }) - (inv: nat_at_most finish -> vprop) + (inv: nat_at_most finish -> GTot vprop) (body: (i:u32_between start finish -> SteelT unit @@ -45,8 +45,8 @@ noextract let for_loop_full (start:US.t) (finish:US.t { US.v start <= US.v finish }) - (inv: nat_at_most finish -> vprop) - (inv_sel: (i:nat_at_most finish) -> t_of (inv i) -> prop) + (inv: nat_at_most finish -> GTot vprop) + (inv_sel: (i:nat_at_most finish) -> t_of (inv i) -> GTot prop) (body: (i:u32_between start finish -> Steel unit @@ -77,7 +77,7 @@ let for_loop_full /// while_loop: while (cond()) { body () } -val while_loop (inv: Ghost.erased bool -> vprop) +val while_loop (inv: Ghost.erased bool -> GTot vprop) (cond: (unit -> SteelT bool (AT.h_exists inv) (fun b -> inv b))) diff --git a/lib/steel/Steel.ST.Loops.fst b/lib/steel/Steel.ST.Loops.fst index b2222fad2..b285ef984 100644 --- a/lib/steel/Steel.ST.Loops.fst +++ b/lib/steel/Steel.ST.Loops.fst @@ -45,7 +45,7 @@ let for_loop' (start:US.t) let for_loop (start:US.t) (finish:US.t { US.v start <= US.v finish }) - (inv: nat_at_most finish -> vprop) + (inv: nat_at_most finish -> GTot vprop) (body: (i:u32_between start finish -> STT unit @@ -74,7 +74,7 @@ let exists_to_h_exists (#a:Type) #o (p:a -> vprop) = let w = elim_exists () in intro_h_exists w p -let coerce_cond (inv: Ghost.erased bool -> vprop) +let coerce_cond (inv: Ghost.erased bool -> GTot vprop) (cond: (unit -> STT bool (exists_ inv) (fun b -> inv b))) @@ -84,7 +84,7 @@ let coerce_cond (inv: Ghost.erased bool -> vprop) intro_exists_erased w inv; cond () -let coerce_body (inv: Ghost.erased bool -> vprop) +let coerce_body (inv: Ghost.erased bool -> GTot vprop) (body: (unit -> STT unit (inv true) (fun _ -> exists_ inv))) @@ -96,7 +96,7 @@ let coerce_body (inv: Ghost.erased bool -> vprop) return b /// while_loop: while (cond()) { body () } -let while_loop' (inv: Ghost.erased bool -> vprop) +let while_loop' (inv: Ghost.erased bool -> GTot vprop) ($cond: (unit -> STT bool (exists_ inv) (fun b -> inv b))) @@ -124,7 +124,7 @@ let e_exists_to_exists (#a:Type) #o (p:a -> vprop) intro_exists #a (reveal (reveal w)) p let lift_cond_exists_to_e_exists - (inv: bool -> vprop) + (inv: bool -> GTot vprop) (cond: (unit -> STT bool (exists_ inv) (fun b -> inv b))) @@ -137,7 +137,7 @@ let lift_cond_exists_to_e_exists b let lift_body_exists_to_e_exists - (inv: bool -> vprop) + (inv: bool -> GTot vprop) (body: (unit -> STT unit (inv true) (fun _ -> exists_ inv))) @@ -150,7 +150,7 @@ let lift_body_exists_to_e_exists /// while_loop: while (cond()) { body () } -let while_loop (inv: bool -> vprop) +let while_loop (inv: bool -> GTot vprop) (cond: (unit -> STT bool (exists_ inv) (fun b -> inv b))) diff --git a/lib/steel/Steel.ST.Loops.fsti b/lib/steel/Steel.ST.Loops.fsti index 98b4eb51d..9da228569 100644 --- a/lib/steel/Steel.ST.Loops.fsti +++ b/lib/steel/Steel.ST.Loops.fsti @@ -28,7 +28,7 @@ let u32_between (s f:US.t) /// for_loop: for (i = start; i < finish; i++) inv { body i } val for_loop (start:US.t) (finish:US.t { US.v start <= US.v finish }) - (inv: nat_at_most finish -> vprop) + (inv: nat_at_most finish -> GTot vprop) (body: (i:u32_between start finish -> STT unit @@ -39,7 +39,7 @@ val for_loop (start:US.t) (fun _ -> inv (US.v finish)) /// while_loop: while (cond()) { body () } -val while_loop (inv: bool -> vprop) +val while_loop (inv: bool -> GTot vprop) (cond: (unit -> STT bool (exists_ inv) (fun b -> inv b))) diff --git a/lib/steel/c/Steel.ST.C.Types.Scalar.fsti b/lib/steel/c/Steel.ST.C.Types.Scalar.fsti index cd705185f..df3f234b6 100644 --- a/lib/steel/c/Steel.ST.C.Types.Scalar.fsti +++ b/lib/steel/c/Steel.ST.C.Types.Scalar.fsti @@ -111,16 +111,11 @@ let read (#t: Type) (#v: Ghost.erased (scalar_t t)) (r: ref (scalar t)) : ST t (fun v1 -> forall v0 p . (* {:pattern (mk_fraction (scalar t) (mk_scalar v0) p)} *) Ghost.reveal v == mk_fraction (scalar t) (mk_scalar v0) p ==> v0 == v1) = let v0 = FStar.IndefiniteDescription.indefinite_description_tot _ (fun v0 -> exists p . Ghost.reveal v == mk_fraction (scalar t) (mk_scalar v0) p) in let p = FStar.IndefiniteDescription.indefinite_description_tot _ (fun p -> Ghost.reveal v == mk_fraction (scalar t) (mk_scalar (Ghost.reveal v0)) p) in - let prf v0' p' : Lemma - (requires (Ghost.reveal v == mk_fraction (scalar t) (mk_scalar v0') p')) - (ensures (v0' == Ghost.reveal v0 /\ p' == Ghost.reveal p)) - = mk_scalar_inj (Ghost.reveal v0) v0' p p' - in - let prf' v0' p' : Lemma - (Ghost.reveal v == mk_fraction (scalar t) (mk_scalar v0') p' ==> (v0' == Ghost.reveal v0 /\ p' == Ghost.reveal p)) - = Classical.move_requires (prf v0') p' - in - Classical.forall_intro_2 prf'; + introduce forall v0' p'. + Ghost.reveal v == mk_fraction (scalar t) (mk_scalar v0') p' ==> + v0' == Ghost.reveal v0 /\ p' == Ghost.reveal p with + introduce _ ==> _ with _. + mk_scalar_inj (Ghost.reveal v0) v0' p p'; rewrite (pts_to _ _) (pts_to r (mk_fraction (scalar t) (mk_scalar (Ghost.reveal v0)) p)); let v1 = read0 r in rewrite (pts_to _ _) (pts_to r v);