Skip to content

Correctly erase functions. #204

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gebner merged 1 commit into from
Jun 25, 2025
Merged

Correctly erase functions. #204

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions lib/steel/Steel.Effect.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion lib/steel/Steel.Loops.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions lib/steel/Steel.Loops.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)))
Expand Down
14 changes: 7 additions & 7 deletions lib/steel/Steel.ST.Loops.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)))
Expand All @@ -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)))
Expand All @@ -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)))
Expand Down Expand Up @@ -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)))
Expand All @@ -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)))
Expand All @@ -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)))
Expand Down
4 changes: 2 additions & 2 deletions lib/steel/Steel.ST.Loops.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)))
Expand Down
15 changes: 5 additions & 10 deletions lib/steel/c/Steel.ST.C.Types.Scalar.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
Loading