Revamped README, updated docker image

Author: EkanshdeepGupta

Dockerfile

@@ -38,11 +38,12 @@ WORKDIR /app
 COPY --from=build /home/opam/.opam/5.4/bin/z3 /usr/local/bin/z3
 
 # Copy the compiled binary from the 'build' stage
-# The path usually looks like _build/default/<path_to_source>/main.exe
-COPY --from=build /home/opam/app/_build/default/bin/raven.exe ./raven
+COPY --from=build /home/opam/app/_build/default/bin/raven.exe /usr/local/bin/raven
+
+
 
 # Copy repository of examples
 COPY --from=build /home/opam/app/test ./test
 
 # Set the command to run raven
-ENTRYPOINT ["./raven"]
+ENTRYPOINT ["raven"]

README.md

@@ -17,8 +17,63 @@ Raven ships with a [library](lib/library/resource_algebra.rav) of standard resou
 Raven's underlying meta-theory is based on the [Iris](https://iris-project.org/) separation logic framework. We simplify the Iris logic by carefully restricting its features (like higher-order quantification, impredicativity, and step-indexing). At the same time, we add complementary features like the higher-order module system to regain expressivity. The resulting logic is sufficiently expressive to verify complex concurrent algorithms, yet, amenable to robust SMT-based automation. The mechanization of Raven's program logic as an instance of the Iris framework is part of ongoing work.
 
 
+## Portable Usage (via Docker):
+We have made available a Docker image of Raven on DockerHub that can be directly executed without any installation, as follows:
+
+```bash
+$ docker run --rm ekanshdeepgupta/raven
+Raven version 1.x.y
+Verification successful.
+```
+
+This image comes pre-loaded with Raven's existing suite of examples. For example, we can run some existing examples:
+```bash
+$ docker run --rm ekanshdeepgupta/raven test/concurrent/lock/ticket-lock.rav
+Raven version 1.x.y
+Verification successful.
+
+$ docker run --rm ekanshdeepgupta/raven --extension prophecy test/ext_prophecy/lazy_coin.rav
+Raven version 1.x.y
+Verification successful.
+
+$ docker run --rm  ekanshdeepgupta/raven test/ci/front-end/fail/tuple.rav
+Raven version 1.x.y
+[Error] File "test/ci/front-end/fail/tuple.rav", line 7, columns 20-22:
+7 |     var zz: Int := x#2;
+                        ^^
+Type Error: Index out of bounds.
+```
+
+To examine these examples, we can run `cat` for example as follows:
+```bash
+$ docker run --rm --entrypoint cat ekanshdeepgupta/raven test/ci/front-end/bool_perm_ite.rav
+field f: Int
+
+proc p(x: Ref) {
+    inhale !true ? true : own(x.f, 1, 1.0);
+    exhale true ?  own(x.f, 1, 1.0) : true;
+}
+```
+The complete suite of Raven's examples can be browsed at [test](./test) in this repository.
+
+To run Raven on your own example files, say ./my/local/prog.rav, you can run:
+```bash
+$ docker run --rm -it -v $(pwd):/app/data -- ekanshdeepgupta/raven "/app/data/my/local/prog.rav"
+```
+
+To get our hands dirty, we can even access a shell inside the Docker image by executing:
+```bash
+$ docker run --rm -it --entrypoint /bin/bash ekanshdeepgupta/raven
+/app# raven --shh test/ci/back-end/inhale_exhale.rav
+Verification successful.
+
+/app# cd /usr/local/bin
+z3    raven
+```
+
+
 ## Installation
-Raven requires [`opam`](https://opam.ocaml.org/) (>= 2.1.0) as well as OCaml (>= 4.12.0) and various OCaml libraries. See [`dune-project`](dune-project) for the full list of dependencies. Raven and all its depdencies other than `opam` can be installed by running the following sequence of commmands.
+To install Raven locally, it requires [`opam`](https://opam.ocaml.org/) (>= 2.1.0) as well as OCaml (>= 4.12.0) and various OCaml libraries. See [`dune-project`](dune-project) for the full list of dependencies. Raven and all its depdencies other than `opam` can be installed by running the following sequence of commmands.
 ```
 $ git clone https://github.com/nyu-acsys/raven.git
 $ cd ./raven
@@ -30,6 +85,7 @@ $ dune build; dune install; dune runtest
 
 A [Visual Studio Code extension](https://github.com/nyu-acsys/raven-lang) for IDE integration is also available.
 
+
 ## Examples
 Several examples of Raven programs can be found in the [test](test) folder. The [ci](test/ci) folder contains many small examples that can be used to learn Raven's syntax for specific features. Complete verified implementations of concurrent data structures can be found in the [concurrent](test/concurrent) folder. Here are a few notable ones to get started, in roughly increasing order of complexity:
 1. [spin_lock](test/concurrent/lock/spin-lock.rav)
@@ -39,6 +95,7 @@ Several examples of Raven programs can be found in the [test](test) folder. The
 1. [give-up template](test/concurrent/templates/give-up.rav)
 1. [bplustree](test/concurrent/templates/bplustree.rav)
 
+
 ## Usage
 The Raven verifier can be executed on a file `test/concurrent/treiber_stack/treiber_stack_atomics.rav` as follows:
 ```
@@ -56,6 +113,7 @@ Raven version 1.0.1
 Verification Error: This update may not be frame-preserving.
 ```
 
+
 ### Raven Verifier Manual
 ```
 RAVEN(1)                         Raven Manual                         RAVEN(1)
@@ -123,3 +181,12 @@ COMMON OPTIONS
        --version
            Show version information.
 ```
+
+## Scientific Background
+
+For a detailed discussion of the motivation and theory behind Raven, including empirical evaluation, please refer to our paper:
+
+> **Raven: An SMT-Based Concurrency Verifier** 
+> Ekanshdeep Gupta, Nisarg Patel, and Thomas Wies.  
+> *In Computer Aided Verification (CAV), 2025.* 
+> **DOI:** [10.1007/978-3-031-98668-0_4](https://doi.org/10.1007/978-3-031-98668-0_4)

bin/raven.ml

@@ -318,6 +318,7 @@ let main () input_files no_greeting no_library typecheck_only lsp_mode base_dir
   }
   in
   let _ = 
+    (* [EXT] Overwriting which extensions are activated. *)
     Ext.overwrite_ext(Ext.module_map extension_mode);
   in
   try `Ok (parse_and_check_all config input_files) with

lib/ext/README.md

@@ -17,6 +17,14 @@ module SampleExt (Cont: ExtApi.Ext) : ExtApi.Ext
 These are higher-order modules that accept, as a parameter, another extension module implementing the `ExtApi.Ext` interface. This allows us to "stack" these extensions on top of each other, and conveniently adjust the exact set of features we want to support when we compile Raven. This happens in `lib/ext/ext.ml`.
 
 
+## Using Current Extensions
+
+We have added two new optional extensions, Prophecy extension and ErrorCredits extension. These can be selected by using the new `--extension` command-line flag which takes one of three values: `default | prophecy | eris`. For example:
+
+`raven --extension prophecy test/ext_prophecy/clairvoyant_coin.rav` 
+`raven --extension eris test/ext_error-credits/ec_examples.rav`
+
+
 ## Creating a New Extension
 
 An extension typically consists of 3 files, and may contain a 4th file. For a new extension say `SampleExt`, these files are:
@@ -58,7 +66,9 @@ Once the programmer has created the extension such that it successfully compiles
   a. add a new module `SampleExtInstance` that instantiates `SampleExt` with an existing extension and introduce it into the chain of extensions. Typically, newer extensions should be added towards the end as the "outermost" instantiations.
   b. update the definition of `module Ext: ExtApi.Ext` to refer to the new instance `SampleExtInstance`.
 
-5. Run `dune build; dune install` to compile Raven with the new extension.
+5. There is a function `Ext.overwrite_ext` that can be used to set which extensions are active. At present it is called from the `main` function in [raven.ml](../../bin/raven.ml). This can be modified to change which stack of extensions is active.
+
+6. Run `dune build; dune install` to compile Raven with the new extension.
 
 That's it! 
 - With the updated parser, Raven front-end will support the newly defined syntax.

raven_docker.tar

@@ -0,0 +1,10 @@
+  $ dune exec -- raven --shh --extension prophecy ./rdcss.rav
+  [Warning] File "./rdcss.rav", line 617, column 8 to line 623, column 5:
+  617 |     ) : (
+                ^
+  No witnesses could be computed for: token^6
+  [Warning] File "./rdcss.rav", line 617, column 8 to line 623, column 5:
+  617 |     ) : (
+                ^
+  No witnesses could be computed for: tid_ghost_winner^6
+  Verification successful.