Updates for cedar#725

cedar-drt/fuzz/src/lib.rs

@@ -31,6 +31,7 @@ use cedar_policy_core::extensions::Extensions;
 pub use cedar_policy_validator::{ValidationErrorKind, ValidationMode, Validator, ValidatorSchema};
 pub use cedar_testing::cedar_test_impl::{
     time_function, CedarTestImplementation, ErrorComparisonMode, TestResult,
+    ValidationComparisonMode,
 };
 use libfuzzer_sys::arbitrary::{self, Unstructured};
 use log::info;
@@ -193,37 +194,27 @@ pub fn run_val_test(
 
     let definitional_res = custom_impl.validate(&schema, policies, mode);
 
-    // If `cedar-policy` does not return an error, then the spec should not return an error.
-    // This implies type soundness of the `cedar-policy` validator since type soundness of the
-    // spec is formally proven.
-    //
-    // In particular, we have proven that if the spec validator does not return an error (B),
-    // then there are no authorization-time errors modulo some restrictions (C). So (B) ==> (C).
-    // DRT checks that if the `cedar-policy` validator does not return an error (A), then neither
-    // does the spec validator (B). So (A) ==> (B). By transitivity then, (A) ==> (C).
-
-    if rust_res.validation_passed() {
-        match definitional_res {
-            TestResult::Failure(err) => {
-                // TODO(#175): For now, ignore cases where the Lean code returned an error due to
-                // an unknown extension function.
-                if !err.contains("jsonToExtFun: unknown extension function") {
-                    panic!(
-                        "Unexpected error\nPolicies:\n{}\nSchema:\n{:?}\nError: {err}",
-                        &policies, schema
-                    );
-                }
+    match definitional_res {
+        TestResult::Failure(err) => {
+            // TODO(#175): For now, ignore cases where the Lean code returned an error due to
+            // an unknown extension function.
+            if !err.contains("jsonToExtFun: unknown extension function") {
+                panic!(
+                    "Unexpected error\nPolicies:\n{}\nSchema:\n{:?}\nError: {err}",
+                    &policies, schema
+                );
             }
-            TestResult::Success(definitional_res) => {
-                // Even if the Rust validator succeeds, the definitional validator may
-                // return "impossiblePolicy" due to greater precision. In this case, the
-                // input policy is well-typed, although it is guaranteed to always evaluate
-                // to false.
-                if definitional_res.errors == vec!["impossiblePolicy".to_string()] {
-                    return;
-                }
-
-                // But the definitional validator should not return any other error.
+        }
+        TestResult::Success(definitional_res) => {
+            if rust_res.validation_passed() {
+                // If `cedar-policy` does not return an error, then the spec should not return an error.
+                // This implies type soundness of the `cedar-policy` validator since type soundness of the
+                // spec is formally proven.
+                //
+                // In particular, we have proven that if the spec validator does not return an error (B),
+                // then there are no authorization-time errors modulo some restrictions (C). So (B) ==> (C).
+                // DRT checks that if the `cedar-policy` validator does not return an error (A), then neither
+                // does the spec validator (B). So (A) ==> (B). By transitivity then, (A) ==> (C).
                 assert!(
                     definitional_res.validation_passed(),
                     "Mismatch for Policies:\n{}\nSchema:\n{:?}\ncedar-policy response: {:?}\nTest engine response: {:?}\n",
@@ -232,10 +223,22 @@ pub fn run_val_test(
                     rust_res,
                     definitional_res,
                 );
-
-                // TODO(#69): We currently don't check for a relationship between validation errors.
-                // E.g., the error reported by the definitional validator should be in the list
-                // of errors reported by the production validator, but we don't check this.
+            } else {
+                // If `cedar-policy` returns an error, then only check the spec response
+                // if the validation comparison mode is `AgreeOnAll`.
+                match custom_impl.validation_comparison_mode() {
+                    ValidationComparisonMode::AgreeOnAll => {
+                        assert!(
+                            !definitional_res.validation_passed(),
+                            "Mismatch for Policies:\n{}\nSchema:\n{:?}\ncedar-policy response: {:?}\nTest engine response: {:?}\n",
+                            &policies,
+                            schema,
+                            rust_res,
+                            definitional_res,
+                        );
+                    }
+                    ValidationComparisonMode::AgreeOnValid => {} // ignore
+                };
             }
         }
     }

cedar-drt/src/lean_impl.rs

@@ -333,10 +333,25 @@ impl CedarTestImplementation for LeanDefinitionalEngine {
             ValidationMode::Strict,
             "Lean definitional validator only supports `Strict` mode"
         );
-        self.validate(schema, policies)
+        let result = self.validate(schema, policies);
+        result.map(|res| {
+            // `impossiblePolicy` is considered a warning rather than an error,
+            // so it's safe to drop here (although this means it can't be used
+            // for differential testing, see #254)
+            let errors = res
+                .errors
+                .into_iter()
+                .filter(|x| x != "impossiblePolicy")
+                .collect();
+            TestValidationResult { errors, ..res }
+        })
     }
 
     fn error_comparison_mode(&self) -> ErrorComparisonMode {
         ErrorComparisonMode::PolicyIds
     }
+
+    fn validation_comparison_mode(&self) -> ValidationComparisonMode {
+        ValidationComparisonMode::AgreeOnValid
+    }
 }

cedar-drt/tests/integration_tests.rs

@@ -97,7 +97,5 @@ fn run_corpus_tests(custom_impl: &impl CedarTestImplementation) {
 fn integration_tests_on_def_impl() {
     let lean_def_impl = LeanDefinitionalEngine::new();
     run_integration_tests(&lean_def_impl);
-
-    // This test may fail due to differences in precision between the Rust & Lean validators (#226)
-    // run_corpus_tests(&lean_def_impl);
+    run_corpus_tests(&lean_def_impl);
 }