Deprecate Dafny formalization (#219)

Co-authored-by: Craig Disselkoen <[email protected]>

.github/ISSUE_TEMPLATE/feature_request.yml

@@ -14,7 +14,6 @@ body:
       description: What component of the Cedar specification does this feature relate to?
       multiple: true
       options:
-        - Dafny formalization
         - Lean formalization
         - DRT target(s)
         - DRT generator(s)

.github/workflows/ci.yml

@@ -3,46 +3,7 @@ name: Build cedar-spec
 on:
   pull_request:
 
-env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
-
 jobs:
-  build_and_test_dafny:
-    name: Build and Test Dafny
-    runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        toolchain:
-          - stable
-    steps:
-      - name: Checkout cedar-spec
-        uses: actions/checkout@v3
-      - name: Install Z3
-        shell: bash
-        run: |
-          wget -q --show-progress https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-glibc-2.35.zip
-          unzip z3-4.12.1-x64-glibc-2.35.zip
-          echo "$(pwd)/z3-4.12.1-x64-glibc-2.35/bin" >> $GITHUB_PATH
-      - name: Audit Dafny files
-        shell: bash
-        working-directory: ./cedar-dafny
-        run : |
-          dotnet tool restore
-          sudo apt-get install ack
-          find . -path test -prune -o -name '*.dfy' | xargs -I {} sh -c "printf '%s: ' {} && (dotnet tool run dafny audit {} | ack --passthru --nocolor '0 findings')"
-      - name: verify dafny
-        working-directory: ./cedar-dafny
-        run: make GEN_STATS=1 verify
-      - name: test dafny
-        working-directory: ./cedar-dafny
-        run: make test
-      - name: log resource usage
-        working-directory: ./cedar-dafny
-        run: |
-          dotnet tool restore
-          dotnet tool run dafny-reportgenerator summarize-csv-results --max-resource-count 10000000 . || true
-
   build_and_test_lean:
     name: Build and Test Lean
     runs-on: ubuntu-latest
@@ -86,12 +47,6 @@ jobs:
         run: |
               wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
               bash elan-init.sh -y
-      - name: Get Java 17
-        uses: actions/setup-java@v3
-        with:
-          distribution: 'corretto'
-          java-version: '17'
-          cache: 'gradle'
       - name: rustup
         run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
       - name: cargo fmt (cedar-policy-generators)

.gitignore

@@ -11,18 +11,6 @@
 # Don't check IntelliJ module files
 *.iml
 
-
-# cedar-dafny build artifacts
-cedar-dafny/.dotnet
-cedar-dafny/.local
-cedar-dafny/.nuget
-cedar-dafny/build
-cedar-dafny/TestResults
-
-# cedar-dafny-java-wrapper build artifacts
-cedar-dafny-java-wrapper/build
-cedar-dafny-java-wrapper/.gradle
-
 # cedar-drt build artifacts
 cedar-drt/target
 cedar-drt/Cargo.lock

Dockerfile

@@ -3,7 +3,7 @@ FROM amazonlinux:2 AS prepare
 
 RUN yum update -y \
   && yum install -y \
-	curl clang tar zip unzip python3 git xz java-1.8.0-openjdk-devel.x86_64 \
+	curl clang tar zip unzip python3 git xz \
 	make wget \
   && yum clean all
 
@@ -17,19 +17,6 @@ RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs > /tmp/rustup.sh \
 # Install cargo-fuzz
 RUN . ~/.profile; cargo install cargo-fuzz
 
-# Setup DOTNET toolchain
-RUN mkdir /opt/dotnet \
-  && wget -q https://dot.net/v1/dotnet-install.sh -O /opt/dotnet/dotnet-install.sh \
-  && chmod +x /opt/dotnet/dotnet-install.sh \
-  && /opt/dotnet/dotnet-install.sh --channel 6.0
-ENV PATH="/root/.dotnet/:$PATH"
-
-# Setup Java/Gradle toolchain
-RUN mkdir /opt/gradle \
-  && wget -q "https://services.gradle.org/distributions/gradle-8.1.1-bin.zip" -O /opt/gradle/gradle.zip \
-  && unzip /opt/gradle/gradle.zip -d /opt/gradle/
-ENV PATH="/opt/gradle/gradle-8.1.1/bin/:$PATH"
-
 # Install Lean
 RUN wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh && sh elan-init.sh -y
 

README.md

@@ -1,31 +1,24 @@
 # Cedar Specification
 
-This repository contains the Dafny formalization of Cedar and infrastructure for performing differential randomized testing (DRT) between the formalization and Rust production implementation available in [cedar](https://github.com/cedar-policy/cedar).
+This repository contains the formalization of Cedar and infrastructure for performing differential randomized testing (DRT) between the formalization and Rust production implementation available in [cedar](https://github.com/cedar-policy/cedar).
 
 ## Repository Structure
 
 * [`cedar-lean`](./cedar-lean) contains the Lean formalization of, and proofs about, Cedar.
-* [`cedar-dafny`](./cedar-dafny) contains the Dafny formalization of, and proofs about, Cedar.
-* [`cedar-dafny-java-wrapper`](./cedar-dafny-java-wrapper) contains the Java interface for DRT.
 * [`cedar-drt`](./cedar-drt) contains code for fuzzing, property-based testing, and differential testing of Cedar.
 * [`cedar-policy-generators`](./cedar-policy-generators) contains code for generating schemas, entities, policies, and requests using the [arbitrary](https://docs.rs/arbitrary/latest/arbitrary/index.html#) crate.
 * `cedar` is a git submodule, pinned to the associated commit of [cedar](https://github.com/cedar-policy/cedar).
 
 ## Build
 
-To build the Dafny formalization and proofs:
-
-* Install Dafny, following the instructions [here](https://github.com/dafny-lang/dafny/wiki/INSTALL). Our proofs expect Z3 version 4.12.1, so if you have another copy of Z3 installed locally, you may need to adjust your PATH.
-* `cd cedar-dafny && make verify test`
-
 To build the Lean formalization and proofs:
 
 * Install Lean, following the instructions [here](https://leanprover.github.io/lean4/doc/setup.html).
 * `cd cedar-lean && lake build Cedar`
 
 To build the DRT framework:
 
-* Install Dafny and Lean, following the instructions above.
+* Install Lean, following the instructions above.
 * `./build.sh`
 
 Note that the build for DRT has only been tested on **Amazon Linux 2**.
@@ -42,16 +35,6 @@ Available targets are described in the README in the `cedar-drt` directory.
 
 Additional commands available with `cargo fuzz help`.
 
-## Checking Proof Stability
-
-You can measure the complexity of Dafny proofs using [dafny-reportgenerator](https://github.com/dafny-lang/dafny-reportgenerator/).
-For example, the commands below check that all proofs have a [resource count](https://dafny.org/dafny/VerificationOptimization/VerificationOptimization#identifying-difficult-assertions) under 10M, which is our informal threshold for when a proof is "too expensive" and likely to break with future changes to Dafny and/or Z3.
-
-```bash
-cd cedar-dafny && make verify GEN_STATS=1
-dotnet tool run dafny-reportgenerator summarize-csv-results --max-resource-count 10000000 .
-```
-
 ## Security
 
 See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.

build.sh

@@ -10,16 +10,6 @@ cd cedar-drt
 source set_env_vars.sh
 cd ..
 
-# Build the Dafny formalization and extract to Java code
-cd cedar-dafny
-make compile-difftest
-cd ..
-
-# Build the Dafny Java wrapper
-cd cedar-dafny-java-wrapper
-./gradlew build dumpClasspath
-cd ..
-
 # Build the Lean formalization and extract to static C libraries
 cd cedar-lean
 lake build Cedar:static DiffTest:static Std:static