Pass schema object as pointer to symcc targets

cedar-drt/fuzz/fuzz_targets/symcc-smt-script-drt.rs

@@ -112,6 +112,7 @@ fuzz_target!(|input: FuzzTargetInput| {
     debug!("Policies: {policy}\n");
 
     if let Ok(schema) = Schema::try_from(input.schema) {
+        let lean_schema = lean_ffi.load_lean_schema_object(&schema).unwrap();
         for req_env in schema.request_envs() {
             if let Ok(sym_env) = SymEnv::new(&schema, &req_env) {
                 // We let Rust to drive the term generation as it's faster than Lean
@@ -130,7 +131,11 @@ fuzz_target!(|input: FuzzTargetInput| {
                     debug!("Lean asserts: {lean_asserts:#?}");
                     match (
                         smtlib_of_check_asserts(&rust_asserts),
-                        lean_ffi.smtlib_of_check_asserts(&lean_asserts, &schema, &req_env),
+                        lean_ffi.smtlib_of_check_asserts(
+                            &lean_asserts,
+                            lean_schema.clone(),
+                            &req_env,
+                        ),
                     ) {
                         (Ok(rust_smtlib), Ok(lean_smtlib)) => {
                             similar_asserts::assert_eq!(

cedar-drt/fuzz/fuzz_targets/symcc-term-drt.rs

@@ -90,6 +90,7 @@ fuzz_target!(|input: FuzzTargetInput| {
     debug!("Policies: {policy}\n");
 
     if let Ok(schema) = Schema::try_from(input.schema) {
+        let lean_schema = lean_ffi.load_lean_schema_object(&schema).unwrap();
         for req_env in schema.request_envs() {
             // The validator DRT property we've been testing is that
             // rust_passes_validation => lean_passes_validation
@@ -106,7 +107,7 @@ fuzz_target!(|input: FuzzTargetInput| {
                 match (
                     lean_ffi.asserts_of_check_always_allows_on_original(
                         &well_typed_policies.policy_set().clone().try_into().unwrap(),
-                        &schema,
+                        lean_schema.clone(),
                         &req_env,
                     ),
                     compile_well_typed_policies(

cedar-drt/fuzz/fuzz_targets/symcc-term-roundtrip-abac-type-directed.rs

@@ -88,15 +88,17 @@ fuzz_target!(|input: FuzzTargetInput| {
     debug!("Policies: {policyset}\n");
 
     if let Ok(schema) = Schema::try_from(input.schema) {
+        let lean_schema = lean_ffi.load_lean_schema_object(&schema).unwrap();
         for req_env in schema.request_envs() {
             // Compute's SMTLib Script Directly in one-pass from Lean
-            match lean_ffi.smtlib_of_check_always_allows(&policyset, &schema, &req_env) {
+            match lean_ffi.smtlib_of_check_always_allows(&policyset, lean_schema.clone(), &req_env)
+            {
                 Ok(smtlib1) => {
                     // Get intermediate term representation of the Asserts / Verification conditions from Lean
-                    match lean_ffi.asserts_of_check_always_allows(&policyset, &schema, &req_env) {
+                    match lean_ffi.asserts_of_check_always_allows(&policyset, lean_schema.clone(), &req_env) {
                         Ok(Ok(asserts)) => {
                             // Compute SMTLib script from the intermediate Assertions
-                            match lean_ffi.smtlib_of_check_asserts(&asserts, &schema, &req_env) {
+                            match lean_ffi.smtlib_of_check_asserts(&asserts, lean_schema.clone(), &req_env) {
                                 // The smtlib scripts should be identical. Otherwise serialization/deserialization may have altered the assertions
                                 Ok(smtlib2) => assert_eq!(Direct: smtlib1, Roundtripped: smtlib2, "Mismatch between direct smtlib and roundtripped term smtlib for {req_env:?}"),
                                 Err(e) => panic!("Roundtripped errored when direct smtlib request did not error. Error: {e}"),
@@ -109,9 +111,13 @@ fuzz_target!(|input: FuzzTargetInput| {
                 // The policy/schema produced an error in Lean
                 Err(e) => {
                     // Check that either the generation of asserts or checking the asserts errors
-                    match lean_ffi.asserts_of_check_always_allows(&policyset, &schema, &req_env) {
+                    match lean_ffi.asserts_of_check_always_allows(
+                        &policyset,
+                        lean_schema.clone(),
+                        &req_env,
+                    ) {
                         Ok(Ok(asserts)) => {
-                            match lean_ffi.smtlib_of_check_asserts(&asserts, &schema, &req_env) {
+                            match lean_ffi.smtlib_of_check_asserts(&asserts, lean_schema.clone(), &req_env) {
                                 Ok(_) => panic!("Roundtripped did not error when direct smtlib request errored. Error: {e}"),
                                 Err(_) => (),
                             }

cedar-lean-ffi/Cargo.toml

@@ -8,7 +8,7 @@ publish = false
 cedar-policy = { version = "*", path = "../cedar/cedar-policy", features = ["protobufs"] }
 cedar-policy-core = { version = "*", path = "../cedar/cedar-policy-core" }
 cedar-policy-symcc = { version = "*", path = "../cedar/cedar-policy-symcc" }
-lean-sys = { version = "0.0.8", default-features = false }
+lean-sys = { version = "0.0.9", default-features = false }
 serde = "1"
 serde_json = "1.0"
 thiserror = "2.0"

cedar-lean-ffi/protobuf_schema/Messages.proto

@@ -76,20 +76,17 @@ message RequestEnv {
 
 message CheckPolicyRequest {
     Policy policy = 1;
-    cedar_policy_validator.Schema schema = 2;
     RequestEnv request = 3;
 }
 
 message CheckPolicySetRequest {
     cedar_policy_core.PolicySet policySet = 1;
-    cedar_policy_validator.Schema schema = 2;
     RequestEnv request = 3;
 }
 
 message ComparePolicySetsRequest {
     cedar_policy_core.PolicySet srcPolicySet = 1;
     cedar_policy_core.PolicySet tgtPolicySet = 2;
-    cedar_policy_validator.Schema schema = 3;
     RequestEnv request = 4;
 }
 
@@ -297,6 +294,5 @@ message Asserts {
 
 message CheckAssertsRequest {
     Asserts asserts = 1;
-    cedar_policy_validator.Schema schema = 2;
     RequestEnv request = 3;
-}
+}

cedar-lean-ffi/src/err.rs

@@ -15,10 +15,14 @@
  */
 use thiserror::Error;
 
+use crate::lean_object::LeanObjectError;
+
 #[derive(Error, Debug)]
 pub enum FfiError {
     #[error("Error deserializing Lean backend output : {0}")]
     LeanDeserializationError(String),
-    #[error("Error occured in Lean backend : {0}")]
+    #[error("Error occurred in Lean backend : {0}")]
     LeanBackendError(String),
+    #[error(transparent)]
+    LeanObjectError(#[from] LeanObjectError),
 }