Skip to content
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

Jump to bottom

Box: use a newtype in the model #229

Merged
merged 2 commits into from
Oct 6, 2024
Merged

Box: use a newtype in the model #229

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ded9f68
Box: use a newtype in the model
mtzguido Oct 6, 2024
b1237fd
ci: patch to dockerfiles before revamping this whole thing
mtzguido Oct 6, 2024
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
66 changes: 51 additions & 15 deletions lib/pulse/lib/Pulse.Lib.Box.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,20 +20,56 @@ open Pulse.Lib.Core

module R = Pulse.Lib.Reference

type box a = R.ref a
let pts_to b #p v = R.pts_to b #p v
#lang-pulse

noeq
type box a = | B : r:R.ref a -> box a

let pts_to b #p v = R.pts_to b.r #p v

let pts_to_is_slprop2 _ _ _ = ()
let alloc x = R.alloc x
let op_Bang b #v #p = R.op_Bang b #v #p
let op_Colon_Equals b x #v = R.op_Colon_Equals b x #v
let free b #v = R.free b #v
let share b = R.share b
let gather b = R.gather b
let share2 b = R.share2 b
let gather2 b = R.gather2 b
let pts_to_injective_eq b = R.pts_to_injective_eq b
let box_to_ref b = b

fn alloc (#a:Type0) (x:a)
requires emp
returns b : box a
ensures pts_to b x
{
let r = R.alloc x;
rewrite R.pts_to r x as pts_to (B r) x;
(B r);
}

fn op_Bang (#a:Type0) (b:box a) (#v:erased a) (#p:perm)
requires pts_to b #p v
returns x : a
ensures pts_to b #p v ** pure (reveal v == x)
{
unfold (pts_to b #p v);
let x = R.(!b.r);
fold (pts_to b #p v);
x
}

fn op_Colon_Equals (#a:Type0) (b:box a) (x:a) (#v:erased a)
requires pts_to b v
ensures pts_to b (hide x)
{
unfold (pts_to b v);
R.(b.r := x);
fold (pts_to b (hide x));
}

#lang-fstar // 'rewrite' below is not the keyword!

let free b #v = R.free b.r #v

let share b = R.share b.r
let gather b = R.gather b.r
let share2 b = R.share2 b.r
let gather2 b = R.gather2 b.r
let pts_to_injective_eq b = R.pts_to_injective_eq b.r
let box_to_ref b = b.r
let to_ref_pts_to #a b #p #v =
rewrite (pts_to b #p v) (R.pts_to b #p v) (slprop_equiv_refl _)
let to_box_pts_to #a r #p #v =
rewrite (R.pts_to r #p v) (pts_to r #p v) (slprop_equiv_refl _)
rewrite (pts_to b #p v) (R.pts_to b.r #p v) (slprop_equiv_refl _)
let to_box_pts_to #a b #p #v =
rewrite (R.pts_to b.r #p v) (pts_to b #p v) (slprop_equiv_refl _)
1 change: 1 addition & 0 deletions lib/pulse/lib/Pulse.Lib.Box.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ module T = FStar.Tactics.V2

module R = Pulse.Lib.Reference

new
val box ([@@@strictly_positive] a:Type0) : Type0

val pts_to (#a:Type0)
Expand Down
6 changes: 3 additions & 3 deletions lib/pulse/lib/Pulse.Lib.Primitives.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,8 @@ ensures

let cas r u v #i = Pulse.Lib.Core.as_atomic _ _ (cas_impl r u v #i)

let read_atomic_box b #n #p = read_atomic b #n #p
let read_atomic_box b #n #p = read_atomic b.r #n #p

let write_atomic_box b x #n = write_atomic b x #n
let write_atomic_box b x #n = write_atomic b.r x #n

let cas_box r u v #i = cas r u v #i
let cas_box b u v #i = cas b.r u v #i
4 changes: 2 additions & 2 deletions src/ci/ci.Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@ FROM ocaml/opam:ubuntu-22.04-ocaml-$ocaml_version

# CI dependencies for the Wasm11 test: node.js
RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sudo -E bash -
RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends nodejs
RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends nodejs libgmp-dev pkg-config

# install rust
RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang
RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang libgmp-dev pkg-config
RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli

ARG opamthreads=24
Expand Down
2 changes: 1 addition & 1 deletion src/ci/hierarchic.Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ FROM fstar:local-branch-$FSTAR_BRANCH

# CI dependencies for the Wasm11 test: node.js
RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sudo -E bash -
RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends nodejs
RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends nodejs libgmp-dev pkg-config

# install rust
RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
Expand Down
Loading