Merge pull request #10 from nyu-acsys/dev

Raven 1.0 release!

.github/workflows/ci.yml

@@ -0,0 +1,37 @@
+name: Builds, tests & co
+
+on:
+  pull_request:
+  push:
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+permissions: read-all
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - macos-latest
+          - ubuntu-latest
+        ocaml-compiler:
+          - "5.1"
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout tree
+        uses: actions/checkout@v4
+
+      - name: Set-up OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - run: opam install . --deps-only --with-test
+
+      - run: opam exec -- dune build
+
+      - run: opam exec -- dune runtest

.gitignore

@@ -1,8 +1,11 @@
 _build/
-dune-project
-*.smt2
 *~
 formalism/formalism.aux
 formalism/formalism.log
 formalism/formalism.synctex.gz
-.directory
+.directory
+log*.smt2
+.vscode
+.DS_Store
+front_end_processed_output.log
+smt-encodings/*

.ocamlformat

@@ -1,2 +1,2 @@
 profile = default
-version = 0.22.4
+version = 0.26.2

LICENSE

@@ -0,0 +1,11 @@
+Copyright 2024
+  Ekanshdeep Gupta ([email protected])
+  Nisarg Patel ([email protected])
+  Thomas Wies ([email protected])
+
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

README.md

@@ -1,25 +1,114 @@
 # Raven
+![Version 1.0](https://img.shields.io/badge/version-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=dev)](https://github.com/nyu-acsys/raven/actions/workflows/ci.yml)
 
-The Resource Algebra Verification ENgine.
+<img align="right" width="150" src="logo.png"/>
 
-Link to the Google Doc: https://docs.google.com/document/d/1AvU88AoWAMsv9lBCK980P7-cjkXOWbE_DJupAi3tK6c/edit?usp=sharing
+Raven (Resource Algebra Verification ENgine) is an SMT-based deductive verifier for concurrent separation logic. Raven supports features like invariants, custom user-defined resource algebras ("monoids"), and a powerful higher-order module system that enables code and proof re-use. Raven also has smart heuristics that automate many low-level details, and an inlined style of development that interleaves code and proof. This streamlines the process of co-developing a program alongside its proof of correctness.
 
-## Dependencies
+Raven provides a highly-automated, user-friendly front-end that draws heavily from projects like [Dafny](https://github.com/dafny-lang/dafny) and [Viper](https://www.pm.inf.ethz.ch/research/viper.html). Raven has a sizeable, and growing [collection](test/concurrent) of verified implementations of fine-grained concurrent data structures commonly found in the literature and as well as real systems.
 
-- opam, version >= 2.1.2
+These implementations are then translated to first-order logic and passed to the [Z3](https://github.com/Z3Prover/z3) SMT-solver to determine whether the user-provided input verifies successfully.
 
-- ocaml, version >= 4.14.0
+Raven also ships with a [library](lib/library/resource_algebra.rav) of standard resource algebra implementations, as well as higher-order resource algebra constructors that embody commonly occuring patterns in proofs of concurrent data structures. This helps the user get started with proofs quickly.
 
-- dune, version >= 3.7.1
+Raven's underlying separation logic is based on the [Iris](https://iris-project.org/) separation logic framework. We vastly simplify the Iris logic by carefully restricting its most higher-order features (like impredicativity and step-indexing). This results in a sufficiently expressive logic that is amenable to robust SMT-based automation. Developing a formal proof of Raven's compatibility with Iris is part of ongoing-work.
 
-- base, version >= 0.15.1
+## Installation
+Raven can be installed by running the following sequence of commmands. It requires [opam](https://opam.ocaml.org/).
+```
+$ git clone https://github.com/nyu-acsys/raven.git
+$ cd ./raven
+$ opam switch create raven 5.2.0
+$ opam switch raven
+$ opam install . --deps
+$ dune build; dune install; dune runtest
+```
 
-- stdio, version >= 0.15
+## Examples
+Several examples can be found in the [test](test) folder. The [ci](test/ci) folder contains many small example that can be used to learn Raven 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)
+1. [monotonic_counter](test/concurrent/counter/counter_monotonic.rav)
+1. [treiber_stack](test/concurrent/treiber_stack/treiber_stack_atomics.rav)
+1. [atomic_resource_counter](test/comparison/arc_atomics.rav)
+1. [bplustree](test/concurrent/templates/bplustree.rav)
+1. [give-up template](test/concurrent/templates/give-up.rav)
 
-- ppx_custom_printf >= 0.15.0
+## Usage
+Raven 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
+Verification successful.
+```
+Here is a failing example:
+```
+$ raven test/ci/back-end/fail/fpu_fail.rav
+Raven version 1.
+[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.
+```
 
-- ppx_compare >= 0.15.0
+### Raven Manual
+```
+RAVEN(1)                         Raven Manual                         RAVEN(1)
 
-- ppx_hash >= 0.15.0
+NAME
+       raven
 
-- ppx_sexp_conv >= 0.15.1
+SYNOPSIS
+       raven [OPTION]… [INPUT]…
+
+ARGUMENTS
+       INPUT
+           Input file.
+
+OPTIONS
+       --color=WHEN (absent=auto)
+           Colorize the output. WHEN must be one of auto, always or never.
+
+       --lsp-mode
+           Format error messages for LSP integration.
+
+       --nostdlib
+           Skip standard library.
+
+       -q, --quiet
+           Be quiet. Takes over -v and --verbosity.
+
+       --shh
+           Suppress greeting.
+
+       --smt-info
+           Let Z3 produce diagostic output.
+
+       --smt-timeout=VAL (absent=10000)
+           Timeout for SMT solver in ms.
+
+       --stats
+           Output only program stats: concrete instruction steps, ghost
+           instruction steps, and number of specification formulae
+
+       --typeonly
+           Only type-check input program but do not verify it.
+
+       -v, --verbose
+           Increase verbosity. Repeatable, but more than twice does not bring
+           more.
+
+       --verbosity=LEVEL (absent=warning)
+           Be more or less verbose. LEVEL must be one of quiet, error,
+           warning, info or debug. Takes over -v.
+
+COMMON OPTIONS
+       --help[=FMT] (default=auto)
+           Show this help in format FMT. The value FMT must be one of auto,
+           pager, groff or plain. With auto, the format is pager or plain
+           whenever the TERM env var is dumb or undefined.
+
+       --version
+           Show version information.
+```

Raven.opam

@@ -0,0 +1,37 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Raven"
+description:
+  "An intermediate verification language and deductive verifier based on concurrent separation logic."
+depends: [
+  "ocaml" {>= "4.12.0"}
+  "dune" {>= "3.12" & >= "3.12"}
+  "z3" {>= "4.13.0"}
+  "ocamlformat" {>= "0.26.2"}
+  "base" {>= "0.14"}
+  "stdio" {>= "0.14"}
+  "logs" {>= "0.7.0"}
+  "fmt" {>= "0.9.0"}
+  "cmdliner" {>= "1.2.0"}
+  "ppx_custom_printf" {>= "0.14.1"}
+  "ppx_compare" {>= "0.14.0"}
+  "ppx_hash" {>= "0.14.0"}
+  "ppx_sexp_conv" {>= "0.14.3"}
+  "ppx_let" {>= "0.16.0"}
+  "ppx_blob" {>= "0.7.2"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]

bin/dune

@@ -1,4 +1,22 @@
 (executable
-  (name raven)
-  (libraries base config util ast frontend)
-  (preprocess (pps ppx_custom_printf)))
+ (name raven)
+ (public_name raven)
+ (libraries
+  base
+  cmdliner
+  fmt
+  fmt.cli
+  fmt.tty
+  logs
+  logs.cli
+  logs.fmt
+  config
+  util
+  ast
+  frontend
+  rewrites
+  backend
+  library)
+ (preprocess
+  (pps ppx_custom_printf))
+ (modes byte exe))