ExtensionAPI is here!

.dockerignore

@@ -0,0 +1,23 @@
+_build/
+*~
+.DS_Store
+.directory
+front_end_processed_output.log
+log*.smt2
+.vscode
+smt-encodings/*
+benchmarks.csv
+raven/test/bugs
+raven/test/scratch
+raven/bench_results/*
+raven/test/concurrent/implementations
+raven/test/concurrent/templates/give-up-lock_wip.rav
+raven/test/iterated-star/linked_list_wip.rav
+raven/test/linked-lists
+raven/test/rec-preds/list_predicates_wip.rav
+raven/test/rec-preds/list_predicates2_wip.rav
+raven/raven.tar
+.git
+.git/*
+.gitignore
+.github

.gitignore

@@ -1,15 +1,8 @@
 _build/
 *~
-formalism/formalism.aux
-formalism/formalism.log
-formalism/formalism.synctex.gz
 .directory
-log*.smt2
 .vscode
 .DS_Store
+log*.smt2
 front_end_processed_output.log
-smt-encodings/*
-benchmarks.csv
-.dockerignore
-Dockerfile
-raven.tar
+benchmarks.csv

CHANGELOG

@@ -4,14 +4,47 @@ All notable changes to this project will be docmented in this file.
 
 ## [Unreleased]
 
-### Fixes
+
+## [1.1.0] - 2026-01-27
+
+### Added
+
+- Added ExtensionAPI as a way to modularly add and remove front-end features in Raven.
+- Added cmpxchg atomic operation.
+- Added a new cmdline option `--extension` which (presently) takes one of three values: `default`, `eris`, and `prophecy`. This option can be used to select which extension of Raven are active for a given run.
+
+### Changed
+
+- Upgraded [Array interface](test/arrays/array.rav) from an interface to a module.
+- Finished implementation of [rdcss](test/ext_prophecy/rdcss.rav)
+- Added expr_ext_rewrite_types, stmt_ext_rewrite_types to ExtAPI.
+- Added parser support for auCommit resources; enable 'helping'.
+- Expanded definition of "word-sized" types to more flexible types such as algebraic sums of base types.
+- Overhauled extensions to follow namespace-style convention.
+- Added support for helping by allowing auPred resources to refer to another proc; overhauling parser, type-checking and rewriting.
+- Updated syntax so that commitAU always requires at least two argument: token and a tuple of return values (if function returns nothing then it should be ()); and an optional third argument which is a tuple of the callable args (which goes as the middle argument). This optional argument becomes required if the token refers to a different procedure.
+
+
+### Fixed
+
+- Fixed bug in ComputeStats functionality with looking up abstract members without entering modules.
+- Fixed bug regarding missing quantifiers for auto lemmas with arguments.
+- Fixed two bugs in type checker related to interface aliasing (#35)
+- Fixed a bug causing a crash on datatype destructors 
+- Sanitizing JSON output in LSP mode.
+- Catch module-level var declarations in type checker rather than parser (#31).
+- Fix type-checking bug that allowed access to members of interfaces from outside of their scopes.
 
 ## [1.0.1] - 2025-11-22
 
+### Fixed
+
+- Supressed generating log files unless debug mode is used.
+
 - Fixed multiple redundant local variable declarations due to excessive havocing.
-- Variables declared inside while loops are now declared as local variables when while loops are rewritten to proc calls. (#29)
-- Fix missing locations in certain expressions being constructed
-- Fix SMT Backend crash with "_" ident (#22)
+- Variables declared inside while loops are now declared as local variables when while loops are rewritten to proc calls. (#29).
+- Fix missing locations in certain expressions being constructed.
+- Fix SMT Backend crash with "_" ident (#22).
 - Fix crash on FPU stmt in while loops (#27).
 - Added if_block before making call to while_loop proc.
 - Fix spurious type error when type-checking inherited modules (#25).

Dockerfile

@@ -0,0 +1,49 @@
+# --- Stage 1: Build Stage ---
+FROM ocaml/opam:alpine AS build
+
+# Install system dependencies (bash, m4, etc. required for many OCaml libs)
+USER root
+RUN apk add --no-cache bash m4 pkgconfig build-base gmp-dev
+
+# Switch back to the opam user to manage OCaml packages
+USER opam
+WORKDIR /home/opam/app
+
+# Update opam and install the build tool (Dune)
+RUN opam update && opam install dune -y
+
+RUN opam install z3 ocamlformat base stdio logs fmt cmdliner ppx_custom_printf ppx_compare ppx_hash ppx_sexp_conv ppx_let ppx_blob yojson -y --jobs=8
+
+# Copy Raven's source code into the container
+COPY --chown=opam:opam . .
+
+# Build the project
+# 'opam exec --' ensures the OCaml environment variables are set
+RUN opam install . --deps -j 8
+RUN eval $(opam env)
+RUN opam exec -- dune build
+
+# --- Stage 2: Runtime Stage ---
+# We use a fresh, tiny Alpine image for the final container
+FROM alpine:latest
+
+# 1. Install the C++ and Math libraries Z3 needs (found via ldd)
+RUN apk add --no-cache \
+    bash gmp \
+    libstdc++ libgcc
+
+WORKDIR /app
+
+# 1. Copy the Z3 binary from the opam switch
+COPY --from=build /home/opam/.opam/5.4/bin/z3 /usr/local/bin/z3
+
+# Copy the compiled binary from the 'build' stage
+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"]

README.md

@@ -1,5 +1,5 @@
 # Raven
-![Version 1.0.1](https://img.shields.io/badge/version-1.0.1-green.svg)
+![Version 1.1.0](https://img.shields.io/badge/version-1.1.0-green.svg)
 [![MIT licensed](https://img.shields.io/badge/license-MIT-blue.svg)](https://raw.githubusercontent.com/nyu-acsys/raven/master/LICENSE)
 [![Builds, tests & co](https://github.com/nyu-acsys/raven/actions/workflows/ci.yml/badge.svg?branch=main)](https://github.com/nyu-acsys/raven/actions/workflows/ci.yml)
 
@@ -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# ls /usr/local/bin
+raven  z3
+```
+
+
 ## 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,24 +95,44 @@ 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:
 ```
 $ raven test/concurrent/treiber_stack/treiber_stack_atomics.rav
-Raven version 1.0.1
+Raven version 1.x.y
 Verification successful.
 ```
 Here is a failing example:
 ```
 $ raven test/ci/back-end/fail/fpu_fail.rav
-Raven version 1.0.1
+Raven version 1.x.y
 [Error] File "test/ci/back-end/fail/fpu_fail.rav", line 7, columns 2-14:
 7 |   fpu(x.f, 4);
       ^^^^^^^^^^^^
 Verification Error: This update may not be frame-preserving.
 ```
 
-### Raven Verifier Manual
+
+## Extension API
+Raven also comes with a modular extension API which is designed for front-end designers to be able to extend Raven's syntax directly, to get a custom IVL for their specific domain. They can implement Raven extensions to encode new front-end features, adding custom types, expressions, and commands to the IVL.
+We provide extensive documentation along with a tutorial for this API at [lib/ext/README.md](lib/ext/README.md). We implement multiple different extensions and extensively document their code to demonstrate possibilities, and add several useful features to the language. At present, Raven comes with two optional extensions which can be selected via the command-line flag `--extension`:
+- ErrorCredits Extension (`eris`): This extension is available to prove error bounds for probablistic programs. Inspired from [Eris](https://dl.acm.org/doi/10.1145/3674635), we use this extension to verify a [collision-free hashmap](test/ext_error-credits/cf_hashmap.rav), and a [fault memory allocator](test/ext_error-credits/ec_dynamic_vec.rav). For example:
+```bash
+$ raven --extension eris test/ext_error-credits/ec_dynamic_vec.rav
+Raven version 1.x.y
+Verification successful.
+```
+
+- Prophecy Extension (`prophecy`): This extension implements _prophecy variables_ in Raven. For example:
+```bash
+$ raven --extension prophecy test/ext_prophecy/rdcss.rav
+Raven version 1.x.y
+Verification successful.
+```
+
+
+## Raven Verifier Manual
 ```
 RAVEN(1)                         Raven Manual                         RAVEN(1)
 
@@ -78,6 +154,9 @@ OPTIONS
        --color=WHEN (absent=auto)
            Colorize the output. WHEN must be one of auto, always or never.
 
+       --extension=VAL (absent=default)
+           Extension mode: default, eris, or prophecy.
+
        --lsp-mode
            Format error messages for LSP integration.
 
@@ -120,3 +199,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)

Raven.opam

@@ -25,6 +25,8 @@ depends: [
   "ppx_sexp_conv" {>= "0.14.3"}
   "ppx_let" {>= "0.16.0"}
   "ppx_blob" {>= "0.7.2"}
+  "sexplib" {>= "0.17.0"}
+  "yojson" {>= "2.2.2"}
   "odoc" {with-doc}
 ]
 build: [