Lean DRT

.github/workflows/ci.yml

@@ -15,7 +15,6 @@ jobs:
       matrix:
         toolchain:
           - stable
-
     steps:
       - name: Checkout cedar-spec
         uses: actions/checkout@v3
@@ -44,33 +43,55 @@ jobs:
           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
+    strategy:
+      matrix:
+        toolchain:
+          - stable
+    steps:
+      - name: Checkout cedar-spec
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Install Lean
+        shell: bash
+        run: |
+              wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
+              bash elan-init.sh -y
+      - name: Build
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake build Cedar
+      - name: Test
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake exe CedarUnitTests
+
   build_and_test_drt:
     name: Build and Test DRT
     runs-on: ubuntu-latest
     strategy:
       matrix:
         toolchain:
           - stable
-
     steps:
       - name: Checkout cedar-spec
         uses: actions/checkout@v3
         with:
           submodules: recursive
+      - name: Install Lean
+        shell: bash
+        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: Build Dafny def engine
-        working-directory: ./cedar-dafny
-        shell: bash
-        run: make compile-difftest
-      - name: Build cedar-dafny-java-wrapper
-        working-directory: ./cedar-dafny-java-wrapper
-        shell: bash
-        run: ./gradlew build dumpClasspath
       - name: rustup
         run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
       - name: cargo fmt (cedar-policy-generators)
@@ -85,46 +106,9 @@ jobs:
       - name: cargo rustc (cedar-policy-generators)
         working-directory: ./cedar-policy-generators
         run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose
-      - name: cargo rustc (cedar-drt)
-        working-directory: ./cedar-drt
-        run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose
-      - name: cargo rustc (cedar-drt/fuzz/)
-        working-directory: ./cedar-drt/fuzz
-        run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose
       - name: cargo test (cedar-policy-generators)
         working-directory: ./cedar-policy-generators
         run: cargo test --verbose
-      - name: cargo test (cedar-drt)
-        working-directory: ./cedar-drt
-        shell: bash
-        run: |
-             source ./set_env_vars.sh
-             export LD_LIBRARY_PATH=${LD_LIBRARY_PATH+$LD_LIBRARY_PATH:}$JAVA_HOME/lib/server
-             cargo test --verbose
-
-  build_cedar_lean:
-    name: Build cedar-lean
-    runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        toolchain:
-          - stable
-
-    steps:
-      - name: Checkout cedar-spec
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
-      - name: Install Lean
-        shell: bash
-        run: |
-              wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
-              bash elan-init.sh -y
-      - name: Build
-        working-directory: ./cedar-lean
-        shell: bash
-        run: source ~/.profile && lake build Cedar
-      - name: Test
-        working-directory: ./cedar-lean
+      - name: build.sh
         shell: bash
-        run: source ~/.profile && lake exe CedarUnitTests
+        run: source ~/.profile && ./build.sh

README.md

@@ -15,14 +15,21 @@ This repository contains the Dafny formalization of Cedar and infrastructure for
 
 To build the Dafny formalization and proofs:
 
-* Install Dafny 4.0, 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.
+* 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, following the instructions above
+* Install Dafny and Lean, following the instructions above.
 * `./build.sh`
 
+Note that the build for DRT has only been tested on **Amazon Linux 2**.
+
 ## Run
 
 To run DRT:

build.sh

@@ -4,19 +4,33 @@
 git submodule update --init
 
 # Set environment variables
-cd cedar-drt && source ./set_env_vars.sh
+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 formalization and extract Java code
-cd cedar-dafny && make compile-difftest
+# Build the Dafny Java wrapper
+cd cedar-dafny-java-wrapper
+./gradlew build dumpClasspath
 cd ..
 
-# Build the Java wrapper for DRT
-cd cedar-dafny-java-wrapper && ./gradlew build dumpClasspath
+# Build the Lean formalization and extract to static C libraries
+cd cedar-lean
+lake build Cedar:static DiffTest:static Std:static
 cd ..
 
 # Build DRT
 cd cedar-drt
 cargo build
-cargo test
-cd fuzz && RUSTFLAGS="--cfg=fuzzing" cargo build
+
+# Run integration tests
+source set_env_vars.sh
+cargo test -- --nocapture
+
+# Build inner fuzz crate
+cd fuzz && RUSTFLAGS="--cfg=fuzzing" cargo build
+cargo test

cedar-drt/Cargo.toml

@@ -13,6 +13,7 @@ cedar-policy-core = { path = "../cedar/cedar-policy-core", version = "3.*", feat
 cedar-policy-validator = { path = "../cedar/cedar-policy-validator", version = "3.*", features = ["arbitrary"] }
 cedar-policy-formatter = { path = "../cedar/cedar-policy-formatter", version = "3.*" }
 jni = { version = "0.19.0", features = ["invocation"] }
+lean-sys = { version = "0.0.5", features = ["small_allocator"], default-features = false }
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"
 lazy_static = "1.4"

cedar-drt/README.md

@@ -26,5 +26,15 @@ The table below lists all available fuzz targets, including which component of t
 
 ## Logging
 
-If the fuzz targets are compiled with the `log` features, then they will log their entire corpus to the file pointed at in the `LOGFILE` environment variable. 
+If the fuzz targets are compiled with the `log` features, then they will log their entire corpus to the file pointed at in the `LOGFILE` environment variable.
 The sampling rate can be controlled by the `RATE` environment variable, which defaults to 100% if not set.
+
+
+## Debugging build failures
+
+If you run into weird build issues,
+1. Make sure you have run `source set_env_vars.sh`, which sets all the environment variables needed to run the Dafny and Lean definitional code.
+2. Try a `cargo clean` and rebuild.
+3. If the steps above don't help, then file [an issue](https://github.com/cedar-policy/cedar-spec/issues).
+
+If everything builds, but the integration tests are failing, then it may be helpful to set `RUST_BACKTRACE=1` and run `cargo test -- --nocapture` to print additional test information.

cedar-drt/build.rs

@@ -0,0 +1,7 @@
+use std::env;
+fn main() {
+    let lean_dir = env::var("LEAN_LIB_DIR").unwrap();
+    println!("cargo:rustc-link-search=native=../cedar-lean/build/lib");
+    println!("cargo:rustc-link-search=native={lean_dir}");
+    println!("cargo:rustc-link-search=native=../cedar-lean/lake-packages/std/build/lib");
+}

cedar-drt/fuzz/build.rs

@@ -0,0 +1,7 @@
+use std::env;
+fn main() {
+    let lean_dir = env::var("LEAN_LIB_DIR").unwrap();
+    println!("cargo:rustc-link-search=native=../../cedar-lean/build/lib");
+    println!("cargo:rustc-link-search=native={lean_dir}");
+    println!("cargo:rustc-link-search=native=../../cedar-lean/lake-packages/std/build/lib");
+}

cedar-drt/lean-toolchain

@@ -0,0 +1 @@
+../cedar-lean/lean-toolchain

cedar-drt/set_env_vars.sh

@@ -26,3 +26,9 @@ unset -f add_lib_to_path
 if [ -f "$(pwd)/../cedar-dafny-java-wrapper/build/libs/cedar-dafny-java-wrapper.jar" ]; then
     export CLASSPATH="$(< ../cedar-dafny-java-wrapper/build/runtimeClasspath.txt):$(pwd)/../cedar-dafny-java-wrapper/build/libs/cedar-dafny-java-wrapper.jar"
 fi
+
+# Set environment variables for Lean
+export LEAN_LIB_DIR=$(lean --print-libdir)
+export LD_LIBRARY_PATH=${LD_LIBRARY_PATH+$LD_LIBRARY_PATH:}$(lean --print-libdir)
+export DYLD_LIBRARY_PATH=${DYLD_LIBRARY_PATH+$DYLD_LIBRARY_PATH:}$(lean --print-libdir)
+export LD_PRELOAD=${LD_PRELOAD+$LD_PRELOAD:}$(lean --print-prefix)/lib/glibc/libm.so

cedar-drt/src/dafny_java_impl.rs

@@ -18,19 +18,18 @@
 //! implementation extracted from the Dafny specification.
 
 use crate::cedar_test_impl::*;
+use crate::definitional_request_types::*;
 use crate::logger::*;
 use cedar_policy::frontend::is_authorized::InterfaceResponse;
 use cedar_policy::integration_testing::{CustomCedarImpl, IntegrationTestValidationResult};
-pub use cedar_policy::Response;
 use cedar_policy_core::ast::{Expr, Value};
 pub use cedar_policy_core::*;
-pub use cedar_policy_validator::{ValidationMode, ValidationResult, ValidatorSchema};
+pub use cedar_policy_validator::{ValidationMode, ValidatorSchema};
 pub use entities::Entities;
 use jni::objects::{JObject, JString, JValue};
 use jni::{JNIVersion, JavaVM};
 use lazy_static::lazy_static;
 use log::info;
-use serde::{Deserialize, Serialize};
 
 /// Times to (de)serialize JSON content sent to / received from the Dafny-Java
 /// implementation.
@@ -67,50 +66,6 @@ lazy_static! {
     };
 }
 
-#[derive(Debug, Serialize)]
-struct RequestForDefEngine<'a> {
-    request: &'a ast::Request,
-    policies: &'a ast::PolicySet,
-    entities: &'a Entities,
-}
-
-#[derive(Debug, Serialize, Deserialize)]
-pub struct DefinitionalAuthResponse {
-    serialization_nanos: i64,
-    deserialization_nanos: i64,
-    auth_nanos: i64,
-    response: InterfaceResponse,
-}
-
-#[derive(Debug, Serialize)]
-struct EvalRequestForDefEngine<'a> {
-    request: &'a ast::Request,
-    entities: &'a Entities,
-    expr: &'a ast::Expr,
-    expected: Option<&'a ast::Expr>,
-}
-
-#[derive(Debug, Serialize, Deserialize, Clone, Copy)]
-#[repr(transparent)]
-struct DefinitionalEvalResponse {
-    matches: bool,
-}
-
-#[derive(Debug, Serialize)]
-struct RequestForDefValidator<'a> {
-    schema: &'a ValidatorSchema,
-    policies: &'a ast::PolicySet,
-    mode: ValidationMode,
-}
-
-#[derive(Debug, Deserialize)]
-pub struct DefinitionalValResponse {
-    serialization_nanos: i64,
-    deserialization_nanos: i64,
-    validation_nanos: i64,
-    response: ValidationInterfaceResponse,
-}
-
 /// The lifetime parameter 'j is the lifetime of the JVM instance
 pub struct JavaDefinitionalEngine<'j> {
     /// Thread attached to the JVM

cedar-drt/src/definitional_request_types.rs

@@ -0,0 +1,66 @@
+/*
+ * Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      https://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+use crate::cedar_test_impl::*;
+use cedar_policy::frontend::is_authorized::InterfaceResponse;
+pub use cedar_policy_core::*;
+pub use cedar_policy_validator::{ValidationMode, ValidatorSchema};
+pub use entities::Entities;
+use serde::{Deserialize, Serialize};
+
+#[derive(Debug, Serialize)]
+pub struct RequestForDefEngine<'a> {
+    pub request: &'a ast::Request,
+    pub policies: &'a ast::PolicySet,
+    pub entities: &'a Entities,
+}
+
+#[derive(Debug, Serialize, Deserialize)]
+pub struct DefinitionalAuthResponse {
+    pub serialization_nanos: i64,
+    pub deserialization_nanos: i64,
+    pub auth_nanos: i64,
+    pub response: InterfaceResponse,
+}
+
+#[derive(Debug, Serialize)]
+pub struct EvalRequestForDefEngine<'a> {
+    pub request: &'a ast::Request,
+    pub entities: &'a Entities,
+    pub expr: &'a ast::Expr,
+    pub expected: Option<&'a ast::Expr>,
+}
+
+#[derive(Debug, Serialize, Deserialize, Clone, Copy)]
+#[repr(transparent)]
+pub struct DefinitionalEvalResponse {
+    pub matches: bool,
+}
+
+#[derive(Debug, Serialize)]
+pub struct RequestForDefValidator<'a> {
+    pub schema: &'a ValidatorSchema,
+    pub policies: &'a ast::PolicySet,
+    pub mode: ValidationMode,
+}
+
+#[derive(Debug, Deserialize)]
+pub struct DefinitionalValResponse {
+    pub serialization_nanos: i64,
+    pub deserialization_nanos: i64,
+    pub validation_nanos: i64,
+    pub response: ValidationInterfaceResponse,
+}