Pulse tutorial at POPL 24: initial commit

.devcontainer/devcontainer.json

@@ -0,0 +1,22 @@
+{
+  "name": "Steel devcontainer",
+  "image": "mtzguido/steel-devcontainer:latest",
+  // "build": {
+  //   "dockerfile": "minimal.Dockerfile"
+  // },
+  "customizations": {
+    "vscode": {
+      "extensions": [
+        "FStarLang.fstar-vscode-assistant"
+      ]
+    }
+  },
+  "remoteEnv": {
+  },
+  // Runs only once when container is prepared
+  "onCreateCommand": "",
+  // Runs periodically and/or when content of repo changes
+  "updateContentCommand": "ln -s ~/steel steel",
+  // These run only when the container is assigned to a user
+  "postCreateCommand": "",
+}

.devcontainer/minimal.Dockerfile

@@ -0,0 +1,93 @@
+# This file is used to build the steel-devcontainer image which we
+# routinely push to DockerHub. It will not be rebuilt by rebuilding only
+# the devcontainer. An alternative is replacing the "image" field in
+# the devcontainer with a "build" field, but that would make everyone
+# rebuild the container (and FStar, and Pulse) everytime, which is very
+# expensive.
+
+FROM ubuntu:latest
+
+SHELL ["/bin/bash", "-c"]
+
+# Base dependencies: opam
+# CI dependencies: jq (to identify F* branch)
+# python3 (for interactive tests)
+# libicu (for .NET, cf. https://aka.ms/dotnet-missing-libicu )
+RUN apt-get update \
+    && apt-get install -y --no-install-recommends \
+      ca-certificates \
+      curl \
+      wget \
+      git \
+      gnupg \
+      sudo \
+      python3 \
+      python-is-python3 \
+      libicu70 \
+      libgmp-dev \
+      opam \
+      vim \
+    && apt-get clean -y
+# FIXME: libgmp-dev should be installed automatically by opam,
+# but it is not working, so just adding it above.
+
+# Create a new user and give them sudo rights
+ARG USER=vscode
+RUN useradd -d /home/$USER -s /bin/bash -m $USER
+RUN echo "$USER ALL=NOPASSWD: ALL" >> /etc/sudoers
+USER $USER
+ENV HOME /home/$USER
+WORKDIR $HOME
+RUN mkdir -p $HOME/bin
+
+# Make sure ~/bin is in the PATH
+RUN echo 'export PATH=$HOME/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
+
+# Install OCaml
+ARG OCAML_VERSION=4.12.0
+RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
+RUN opam option depext-run-installs=true
+ENV OPAMYES=1
+RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
+
+# Get compiled Z3
+RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \
+ && unzip z3-4.8.5-x64-ubuntu-16.04.zip \
+ && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 $HOME/bin/z3 \
+ && rm -r z3-4.8.5-*
+
+# Get F* and build (branch pulse-tutorial)
+RUN eval $(opam env) \
+ && source $HOME/.profile \
+ && git clone --depth=1 https://github.com/FStarLang/FStar -b pulse-tutorial \
+ && cd FStar/ \
+ && make -j$(nproc) ADMIT=1 \
+ && ln -s $(realpath bin/fstar.exe) $HOME/bin/fstar.exe
+
+ENV FSTAR_HOME $HOME/FStar
+
+# Get karamel master and build
+RUN eval $(opam env) \
+ && source $HOME/.profile \
+ && git clone --depth=1 https://github.com/FStarLang/karamel \
+ && cd karamel/ \
+ && .docker/build/install-other-deps.sh \
+ && make -j$(nproc)
+
+ENV KRML_HOME $HOME/karamel
+
+# Get Steel/Pulse and build (branch pulse-tutorial)
+RUN eval $(opam env) \
+ && source $HOME/.profile \
+ && git clone --depth=1 https://github.com/FStarLang/steel -b pulse-tutorial \
+ && cd steel/ \
+ && make -j$(nproc) \
+ && make -j$(nproc) -C share/steel/examples/pulse
+
+ENV STEEL_HOME $HOME/steel
+
+# Instrument .bashrc to set the opam switch. Note that this
+# just appends the *call* to eval $(opam env) in these files, so we
+# compute the new environments fter the fact. Calling opam env here
+# would perhaps thrash some variables set by the devcontainer infra.
+RUN echo 'eval $(opam env --set-switch)' | tee --append $HOME/.bashrc

.devcontainer/rebuild-container-and-deploy.sh

@@ -0,0 +1,8 @@
+#!/bin/bash
+
+set -eux
+
+# Cache off since we pull from upstream branches that change
+docker build --no-cache -f .devcontainer/minimal.Dockerfile -t mtzguido/steel-devcontainer .
+
+docker push mtzguido/steel-devcontainer

Hello.fst

@@ -0,0 +1,12 @@
+module Hello
+
+open Pulse.Lib.Pervasives
+
+```pulse
+fn test (x:unit)
+  requires emp
+  ensures emp
+{
+  ()
+} 
+```

README.md

@@ -0,0 +1,77 @@
+Pulse tutorial at POPL 24
+=========================
+
+Getting started (with Codespaces)
+---------------------------------
+
+To get a Pulse environment, you can create a codespace in this repo.
+Click the '<>Code' button above and start a new codespace.
+
+![Creating a Codespace](img/create.png)
+
+You should be greeted, after a minute or two, by a VS Code instance
+running in your browser displaying this same README.
+
+![Loading screen](img/starting.png)
+
+![Opened Codespace](img/vscode.png)
+
+If you prefer a local UI instead of the browser, you can "open"
+the Codespace from your local VS Code installation like so:
+
+![Local open](img/local-open.png)
+
+Everything is still running on Github's servers.
+
+Running locally with VS Code
+----------------------------
+
+(Not recommended for the tutorial, it will take more time to set up.)
+
+If you would like to run the tutorial locally, without relying on Github
+Codespaces, you can clone this repository and open it in VS Code. VS
+Code will suggest reopening the repository in the devcontainer. Or you
+can manually run the command 'Dev Containers: Rebuild and Reopen in
+Container'.
+
+This will download a docker image to your machine and start a container.
+It may be a lot slower than Github Codespaces depending on your internet
+connnection.
+
+You need the Docker extension installed for this. If you are using
+Windows, it should be installed within WSL.
+
+Basic commands
+--------------
+
+The VS Code instance will have the [F* VS Code extension installed](https://github.com/FStarLang/fstar-vscode-assistant). You can read the manual there,
+but the most important things to know are the following:
+
+* Fly-check on opening: When a file is opened, F* will, by default, 
+  fly-check the entire entire contents of the file,
+  stopping at the first error. Any errors will be reported in the problem pane
+  and as "squigglies". Symbols are resolved and hover and jump-to-definition
+  tools should work.
+
+* F*: Check to position: The key-binding `Ctrl+.` advances the checker up to the
+  F* definition that encloses the current cursor position, fully checking.
+
+* F*: Light check to position: The key-binding `Ctrl+Shift+.` advances the checker by
+  light-checking the document up to the F* definition enclosing the current cursor position.
+  This is useful if you want to quickly advance the checker past a chunk of document which
+  might otherwise take a long time to check.
+
+* F*: Restart: The key-binding `Ctrl+; Ctrl+.` restarts the F* session for the current document,
+  rewindind the checker to the top of the document and rescanning it to load any dependences
+  that may have changed, and fly-checking it to load symbols.
+
+* Check file on save: When the file is saved, or when doing `Ctrl+s`, the
+  checker is advanced in full checking mode to the end of the document.
+  This is equivalent to doing `Ctrl+.` on the last line of the document.
+
+* 'F12' will jump to the definition of the symbol under the cursor.
+
+Note, although checking the document proceeds in a linear, top-down fashion, at no point is any
+fragment of the document locked. You can keep editing a document while F* is checking some prefix 
+of it.
+

Steel.fst.config.json

@@ -0,0 +1,15 @@
+{
+  "fstar_exe": "${FSTAR_HOME}/bin/fstar.exe",
+  "options": [
+    "--load_cmxs",
+    "steel",
+    "--warn_error",
+    "-249"
+  ],
+  "include_dirs": [
+    "steel/lib/steel",
+    "steel/lib/steel/pulse",
+    "steel/share/steel/examples/pulse/lib",
+    "tutorial"
+  ]
+}

tutorial/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "pulse_tutorial_test"
+version = "0.1.0"
+
+[lib]
+path = "voting.rs"
+test = true

tutorial/Majority_main.ml

@@ -0,0 +1,10 @@
+let _ =
+  let arr = Array.make 4 0 in
+  Array.set arr 0 1;
+  Array.set arr 1 0;
+  Array.set arr 2 0;
+  Array.set arr 3 0;
+  let maj = PulseTutorial_Algorithms.majority () () arr (Stdint.Uint64.of_int 4) in
+  match maj with
+  | None -> print_string "No majority\n"
+  | Some cand -> Printf.printf "%d had majority\n" cand