Remove FFI interface from cedar-cli and create new create cedar-lean-ffi which can be used in both cedar-cli and cedar-drt.

cedar-lean-cli/Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "cedar-lean-cli"
+edition = "2021"
+version = "0.1.0"
+publish = false
+
+[dependencies]
+cedar-policy = { version = "4.4.0", features = ["protobufs"] }
+cedar-lean-ffi = { path = "../cedar-lean-ffi", version ="4.4.0" }
+clap = { version = "4.5.36", features = ["derive"] }
+serde = "1"
+serde_json = "1.0"
+thiserror = "2.0"
+itertools = "0.14.0"
+miette = "7.6.0"
+prettytable-rs = "0.10"
+
+[profile.release]

cedar-cli/README.md → cedar-lean-cli/README.md

@@ -1,4 +1,4 @@
-# Cedar CLI
+# Cedar Lean CLI
 
 This directory contains a command line interface (CLI) for interacting with the Lean formalization of Cedar. This CLI uses [`Cedar`](https://github.com/cedar-policy/cedar) to parse policies, schemas, entities, and requests and then uses the Lean formalization of Cedar to perform validation, evaluation, authorization, and analysis.
 
@@ -45,21 +45,20 @@ cp -r include/google/ /usr/local/include/
 
 ### Build this CLI
 
-Use the following commands to build `cedar-cli`
+Use the following commands to build `cedar-lean-cli`
 
 ```
-cd cedar-spec                                       # enter the cedar-spec directory of this repository
-git clone https://github.com/cedar-policy/cedar.git # Clone Cedar locally (Required for building the CLI's protobuf messages)
-
-cd cedar-cli                                        # Enter this directory
+cd cedar-lean-ffi                                   # Enter the cedar-lean-ffi library directory
 source set_env_vars.sh                              # Updates environment variables with Lean's library location
 ./build_lean_lib.sh                                 # Build the Lean model of Cedar
+
+cd ../cedar-lean-cli                                     # Enter this directory
 cargo install --path .                              # Build and install this CLI
 ```
 
-Consider adding `source set_env_vars.sh` to your `~/.bashrc` or `~/.profile` to ensure Lean's library path is automatically exported in all new terminal sessions.
+Consider adding `source <path-to-cedar-spec>/cedar-lean-ffi/set_env_vars.sh` to your `~/.bashrc` or `~/.profile` to ensure Lean's library path is automatically exported in all new terminal sessions.
 
-If you try to run `cedar-cli` and get the error `cedar-cli: error while loading shared libraries: libleanshared.so: cannot open shared object file: No such file or directory` you need to run `source set_env_vars.sh`
+If you try to run `cedar-lean-cli` and get the error `cedar-lean-cli: error while loading shared libraries: libleanshared.so: cannot open shared object file: No such file or directory` you need to run `source set_env_vars.sh`.
 
 ## Usage
 
@@ -71,10 +70,10 @@ This CLI implements 4 high-level commands `analyze`, `evaluate`, `validate`, and
 * The `symcc` command gives access to Cedar's Symbolic Compiler---a lower level interface to Cedar's analysis capabilities.
 
 ```
-> cedar-cli --help
+> cedar-lean-cli --help
 Command Line Interface for Cedar Lean
 
-Usage: cedar-cli <COMMAND>
+Usage: cedar-lean-cli <COMMAND>
 
 Commands:
   analyze   Run the Cedar Analyzer
@@ -96,10 +95,10 @@ The `analyze` command provides two sub-commands `policies` and `compare`.
 * The `compare` command takes two policysets `source` and `target` and determines for each "type" of request if the `source` policyset is equivalent, less permissive, more permissive, or incomparable to the `target` policyset (in terms of the requests allowed by each policyset).
 
 ```
-> cedar-cli analyze --help
+> cedar-lean-cli analyze --help
 Run the Cedar Analyzer
 
-Usage: cedar-cli analyze <COMMAND>
+Usage: cedar-lean-cli analyze <COMMAND>
 
 Commands:
   policies  Analyze a PolicySet
@@ -144,10 +143,10 @@ The `symcc` command provides an interface to access Cedar's Symbolic Compiler. T
 * `check-disjoint`:Compares two policy sets `source` and `target`; Checks if `source` and `taget` allow disjoint sets of authorization requests.
 
 ```
-> cedar-cli symcc --help
+> cedar-lean-cli symcc --help
 Run the Cedar Symbolic Compiler
 
-Usage: cedar-cli symcc <COMMAND>
+Usage: cedar-lean-cli symcc <COMMAND>
 
 Commands:
   check-never-errors   Check if the provided Policy never errors
@@ -187,10 +186,10 @@ The `evaluate` command provides two sub-commands `authorize` and `evaluate`.
 * The `evaluate` sub-command evalutes a cedar expression (and optionally compares the evaluated expression to a cedar value).
 
 ```
-> cedar-cli evaluate --help
+> cedar-lean-cli evaluate --help
 Evaluate a Cedar PolicySet or Expression
 
-Usage: cedar-cli evaluate <COMMAND>
+Usage: cedar-lean-cli evaluate <COMMAND>
 
 Commands:
   authorize  Check if a given PolicySet allows or denies a Request
@@ -210,10 +209,10 @@ The `validate` command provides four sub-commands `policy-set`, `level`, `reques
 * The `entities` sub-command validates a set of entities against a given Schema.
 
 ```
-> cedar-cli validate --help
+> cedar-lean-cli validate --help
 Validate PolicySets, Entities, or Requests against a Schema
 
-Usage: cedar-cli validate <COMMAND>
+Usage: cedar-lean-cli validate <COMMAND>
 
 Commands:
   policy-set  Validate a PolicySet against a Schema

cedar-cli/src/analysis.rs → cedar-lean-cli/src/analysis.rs

@@ -13,9 +13,9 @@
  * See the License for the specific language governing permissions and
  * limitations under the License.
  */
-use crate::lean_ffi::LeanDefinitionalEngine;
 use crate::util::{AnalyzePolicyFindingsSer, OpenRequestEnv};
 use crate::{err::ExecError, util::RequestEnvSer};
+use cedar_lean_ffi::CedarLeanFfi;
 use cedar_policy::{Effect, Policy, PolicyId, PolicySet, RequestEnv, Schema};
 use itertools::Itertools;
 use prettytable::{Attr, Cell, Row, Table};
@@ -450,7 +450,7 @@ fn policyset_vacuous(
 ) -> Result<Vec<VacuityResult>, ExecError> {
     let mut vr = Vec::new();
 
-    let lean_context = LeanDefinitionalEngine::new();
+    let lean_context = CedarLeanFfi::new();
     for req_env in req_envs {
         if lean_context.run_check_always_allows(policyset, schema, req_env)? {
             if negate {
@@ -521,7 +521,7 @@ fn compute_permit_shadowing_result(
         }
     })?;
 
-    let lean_context = LeanDefinitionalEngine::new();
+    let lean_context = CedarLeanFfi::new();
     for ((src_vr, tgt_vr), req_env) in zip(zip(src_vacuous_results, tgt_vacuous_results), req_envs)
     {
         match (src_vr, tgt_vr) {
@@ -582,7 +582,7 @@ fn compute_forbid_overrides_shadow_result(
         }
     })?;
 
-    let lean_context = LeanDefinitionalEngine::new();
+    let lean_context = CedarLeanFfi::new();
     for ((forbid_vr, permit_vr), req_env) in zip(
         zip(forbid_vacuous_results, permit_vacuous_results),
         req_envs,
@@ -622,7 +622,7 @@ fn compute_forbid_shadowing_result(
             error: Box::new(err),
         }
     })?;
-    let lean_context = LeanDefinitionalEngine::new();
+    let lean_context = CedarLeanFfi::new();
     for ((src_vr, tgt_vr), req_env) in zip(zip(src_vacuous_results, tgt_vacuous_results), req_envs)
     {
         // Forbid vacuity results are computed on them as if they were permit policies
@@ -755,7 +755,7 @@ pub fn compare_policysets(
     json_output: bool,
 ) -> Result<(), ExecError> {
     let req_envs = OpenRequestEnv::any().to_request_envs(&schema)?;
-    let lean_context = LeanDefinitionalEngine::new();
+    let lean_context = CedarLeanFfi::new();
     let comparison_results: Vec<PolicySetComparisonResult> = req_envs
         .iter()
         .map(|req_env| -> Result<PolicySetComparisonResult, ExecError> {

cedar-cli/src/cli_enums.rs → cedar-lean-cli/src/cli_enums.rs

@@ -204,7 +204,6 @@ impl util::OpenRequestEnv {
 #[derive(ValueEnum, Clone, Debug, Serialize)]
 pub(crate) enum ValidationMode {
     Strict,
-    Permissive,
 }
 
 #[derive(Clone, Debug, Serialize, Subcommand)]

cedar-cli/src/err.rs → cedar-lean-cli/src/err.rs

@@ -27,6 +27,7 @@ pub enum ContentType {
     PolicySet,
     Request,
     Schema,
+    SchemaJSON,
 }
 
 /// The element of a RequestEnvironment that was involved in the error
@@ -97,8 +98,6 @@ pub enum ExecError {
         action_name: String,
         resource_type: String,
     },
-    #[error("Error deserializing Lean backend output")]
-    LeanDeserializationError,
-    #[error("Error occured in Lean backend : {0}")]
-    LeanBackendError(String),
+    #[error(transparent)]
+    LeanFFIError(#[from] cedar_lean_ffi::FfiError),
 }

cedar-cli/src/evaluation.rs → cedar-lean-cli/src/evaluation.rs

@@ -14,34 +14,34 @@
  * limitations under the License.
  */
 use crate::err::ExecError;
-use crate::lean_ffi::LeanDefinitionalEngine;
-use cedar_policy::{Entities, Expression, PolicySet, Request};
+use cedar_lean_ffi::CedarLeanFfi;
+use cedar_policy::{Decision, Entities, Expression, PolicySet, Request};
 
 /// Use the lean_ffi to check if the `policyset` allows the given `request`.
 pub fn check_is_authorized(
     policyset: &PolicySet,
     entities: &Entities,
     request: &Request,
 ) -> Result<(), ExecError> {
-    let lean_context = LeanDefinitionalEngine::new();
+    let lean_context = CedarLeanFfi::new();
     let auth_response = lean_context.is_authorized(policyset, entities, request)?;
-    let decision = match auth_response.decision.as_str() {
-        "allow" => "allowed",
-        "deny" => "denied",
-        _ => return Err(ExecError::LeanDeserializationError),
-    };
-    println!("Authorization request was {decision}.\n");
-    if decision == "denied" && auth_response.determining_policies.mk.l.len() == 0 {
-        print!("This request was implicitly denied as this request matched no policies")
-    } else {
-        print!("This was {decision} due to the following policies:");
+    match auth_response.decision() {
+        Decision::Deny if auth_response.determining_policies().len() == 0 => {
+            print!("This request was implicitly denied as this request matched no policies")
+        }
+        Decision::Deny => {
+            print!("This request was denies as it matched the following policies:")
+        }
+        Decision::Allow => {
+            print!("This request was allowed as it matched the following policies:")
+        }
     }
-    for policy in auth_response.determining_policies.mk.l {
+    for policy in auth_response.determining_policies() {
         print!(" {policy}");
     }
     println!();
     print!("The following policies did not contribute to the decision as they errored during evaluation:");
-    for policy in auth_response.erroring_policies.mk.l {
+    for policy in auth_response.erroring_policies() {
         print!(" {policy}");
     }
     println!();
@@ -56,23 +56,20 @@ pub fn evaluate(
     request: &Request,
     expected_output: Option<&Expression>,
 ) -> Result<(), ExecError> {
-    let lean_context = LeanDefinitionalEngine::new();
+    let lean_context = CedarLeanFfi::new();
     match expected_output {
         Some(output_expr) => {
-            match lean_context.check_evaluate(input_expr, entities, request, output_expr) {
-                Ok(res) => {
-                    if res {
-                        println!("Input expression evaluated to the expected output expression.")
-                    } else {
-                        println!(
-                            "Input expression did not evaluate to the expected output expression."
-                        )
-                    }
-                    Ok(())
-                }
-                Err(e) => Err(e),
+            let res = lean_context.check_evaluate(input_expr, entities, request, output_expr)?;
+            if res {
+                println!("Input expression evaluated to the expected output expression.")
+            } else {
+                println!("Input expression did not evaluate to the expected output expression.")
             }
+            Ok(())
+        }
+        None => {
+            lean_context.print_evaluation(input_expr, entities, request)?;
+            Ok(())
         }
-        None => lean_context.print_evaluation(input_expr, entities, request),
     }
 }

cedar-cli/src/lib.rs → cedar-lean-cli/src/lib.rs

@@ -19,8 +19,6 @@ mod cli_enums;
 mod cli_exec;
 mod err;
 mod evaluation;
-mod lean_ffi;
-mod messages;
 mod symcc;
 mod util;
 mod validation;

cedar-cli/src/main.rs → cedar-lean-cli/src/main.rs

@@ -13,7 +13,7 @@
  * See the License for the specific language governing permissions and
  * limitations under the License.
  */
-use cedar_cli::CliArgs;
+use cedar_lean_cli::CliArgs;
 use clap::Parser;
 use std::process::ExitCode;