symcc: add SymSchema for amortized SymEntities across request envs

cedar-policy-symcc/CHANGELOG.md

@@ -8,6 +8,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 Cedar Language Version: TBD
 
+### Added
+
+- `SymSchema` type that precomputes symbolic entities once per schema and produces
+  `SymEnv` instances via `sym_env()`, avoiding expensive per-environment rebuilds.
+
 ### Fixed
 
 - Fix errors decoding models from Z3. The model decoder now accepts hexadecimal bitvectors

cedar-policy-symcc/src/lib.rs

@@ -47,7 +47,7 @@ pub use symcc::term_type;
 pub use symcc::type_abbrevs;
 pub use symcc::verifier::Asserts;
 pub use symcc::Interpretation;
-pub use symcc::{Env, SmtLibScript, SymEnv};
+pub use symcc::{Env, SmtLibScript, SymEnv, SymSchema};
 
 impl SymEnv {
     /// Constructs a new [`SymEnv`] from the given [`Schema`] and [`RequestEnv`].

cedar-policy-symcc/src/symcc.rs

@@ -65,7 +65,7 @@ pub use concretizer::ConcretizeError;
 pub use concretizer::Env;
 pub use decoder::DecodeError;
 pub use encoder::EncodeError;
-pub use env::{Environment, SymEnv};
+pub use env::{Environment, SymEnv, SymSchema};
 pub use interpretation::Interpretation;
 pub use result::CompileError;
 pub use smtlib_script::SmtLibScript;

cedar-policy-symcc/src/symcc/encoder.rs

@@ -760,12 +760,13 @@ mod unit_tests {
     use super::Encoder;
     use crate::symcc::term_type::TermType;
     use std::collections::BTreeMap;
+    use std::sync::Arc;
 
     #[tokio::test]
     async fn declare_type() {
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         encoder
@@ -778,7 +779,7 @@ mod unit_tests {
     async fn declare_entity_type() {
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         let ety = cedar_policy::EntityTypeName::from_str("User").unwrap();
@@ -791,7 +792,7 @@ mod unit_tests {
     async fn declare_empty_record_type() {
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         encoder.declare_record_type(vec![]).await.unwrap();
@@ -801,7 +802,7 @@ mod unit_tests {
     async fn declare_record_type() {
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         encoder
@@ -814,7 +815,7 @@ mod unit_tests {
     async fn encode_bool_type() {
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         encoder.encode_type(&TermType::Bool).await.unwrap();
@@ -824,7 +825,7 @@ mod unit_tests {
     async fn encode_string_type() {
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         encoder.encode_type(&TermType::String).await.unwrap();
@@ -834,7 +835,7 @@ mod unit_tests {
     async fn encode_uuf() {
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         let my_uuf = crate::symcc::op::Uuf {
@@ -850,7 +851,7 @@ mod unit_tests {
         use cedar_policy::EntityUid;
         let symenv = SymEnv {
             request: SymRequest::empty_sym_req(),
-            entities: SymEntities(BTreeMap::new()),
+            entities: Arc::new(SymEntities(BTreeMap::new())),
         };
         let mut encoder = Encoder::new(&symenv, Vec::<u8>::new()).unwrap();
         let entity_type_name = EntityTypeName::from_str("User").unwrap();

cedar-policy-symcc/src/symcc/env.rs

@@ -29,6 +29,7 @@ use super::tags::SymTags;
 use super::term::{Term, TermPrim, TermVar};
 use super::term_type::TermType;
 use super::type_abbrevs::*;
+use cedar_policy::{RequestEnv, Schema};
 use cedar_policy_core::validator::ValidatorSchema;
 use cedar_policy_core::validator::{
     types::{Attributes, OpenTag, Type},
@@ -173,7 +174,7 @@ pub struct SymEnv {
     /// Symbolic request
     pub request: SymRequest,
     /// Symbolic entities
-    pub entities: SymEntities,
+    pub entities: Arc<SymEntities>,
 }
 
 impl SymEnv {
@@ -403,7 +404,7 @@ impl SymEnv {
     pub fn of_env(ty_env: &Environment<'_>) -> Result<Self, CompileError> {
         Ok(SymEnv {
             request: SymRequest::of_request_type(&ty_env.req_ty)?,
-            entities: SymEntities::of_schema(ty_env.schema)?,
+            entities: Arc::new(SymEntities::of_schema(ty_env.schema)?),
         })
     }
 }
@@ -419,6 +420,51 @@ impl SymEnv {
 // `RequestType` that are only used in `Cedar/SymCC/Env.lean`, so we define
 // them here.
 
+/// A [`Schema`] paired with its precomputed [`SymEntities`].
+///
+/// Building [`SymEntities`] from a schema is expensive and depends only on the
+/// schema, not on any particular request environment. [`SymSchema`] computes it
+/// once so it can be reused across many request environments via
+/// [`SymSchema::sym_env`], which is significantly cheaper than rebuilding the
+/// symbolic entities per environment (as [`SymEnv::new`] does).
+#[derive(Debug, Clone)]
+pub struct SymSchema {
+    schema: Schema,
+    entities: Arc<SymEntities>,
+}
+
+impl SymSchema {
+    /// Builds the symbolic entities for `schema` once, up front.
+    pub fn new(schema: &Schema) -> crate::err::Result<Self> {
+        Ok(Self {
+            schema: schema.clone(),
+            entities: Arc::new(SymEntities::of_schema(schema.as_ref())?),
+        })
+    }
+
+    /// The [`Schema`] this symbolic schema was built from.
+    pub fn schema(&self) -> &Schema {
+        &self.schema
+    }
+
+    /// Returns a [`SymEnv`] for `req_env`, reusing the precomputed [`SymEntities`].
+    ///
+    /// Only the (cheap) symbolic request is built per call; the (expensive)
+    /// symbolic entities are shared via a reference-counted clone. The resulting
+    /// [`SymEnv`] is identical to one built by [`SymEnv::new`] for the same
+    /// schema and request environment.
+    // INVARIANT: must produce the same SymEnv as SymEnv::of_env / SymEnv::new.
+    // Guarded by test sym_schema_sym_env_matches_sym_env_new.
+    pub fn sym_env(&self, req_env: &RequestEnv) -> crate::err::Result<SymEnv> {
+        let env = Environment::from_request_env(req_env, self.schema.as_ref())
+            .ok_or_else(|| crate::err::Error::ActionNotInSchema(req_env.action().to_string()))?;
+        Ok(SymEnv {
+            request: SymRequest::of_request_type(&env.req_ty)?,
+            entities: self.entities.clone(),
+        })
+    }
+}
+
 // TODO: test this
 
 // Convenience functions

cedar-policy-symcc/src/symcc/interpretation.rs

@@ -317,7 +317,7 @@ impl SymEnv {
     /// Interpret a [`SymEnv`] with the given interpretation.
     pub fn interpret(&self, interp: &Interpretation<'_>) -> SymEnv {
         SymEnv {
-            entities: self.entities.interpret(interp),
+            entities: Arc::new(self.entities.interpret(interp)),
             request: self.request.interpret(interp),
         }
     }

cedar-policy-symcc/src/symcc/symbolizer.rs

@@ -426,7 +426,7 @@ impl SymEnv {
             .ok_or(SymbolizeError::IllFormedTypeEnv)?;
         Ok(SymEnv {
             request: SymRequest::from_request(&type_env, &env.request)?,
-            entities: SymEntities::from_entities(&type_env, &env.entities)?,
+            entities: Arc::new(SymEntities::from_entities(&type_env, &env.entities)?),
         })
     }
 }

cedar-policy-symcc/tests/integration_tests.rs

@@ -17,10 +17,11 @@ use std::str::FromStr;
  */
 use cedar_policy::{EntityUid, Policy, PolicyId, PolicySet, Schema, SlotId, Template, Validator};
 use cedar_policy_symcc::{
-    err::CompileError, solver::LocalSolver, CedarSymCompiler, CompiledPolicySet,
+    err::CompileError, solver::LocalSolver, CedarSymCompiler, CompiledPolicySet, SymEnv, SymSchema,
 };
 use cool_asserts::assert_matches;
 use std::collections::HashMap;
+use std::sync::Arc;
 
 mod utils;
 use utils::Environments;
@@ -2531,3 +2532,108 @@ async fn template_linked_policy_unsupported() {
         ))
     );
 }
+
+/// `SymSchema::sym_env` reuses shared symbolic entities across request envs
+/// instead of rebuilding them per env (as `SymEnv::new` does), and its doc
+/// claims the result is *identical* to `SymEnv::new`. Every other test builds
+/// envs via `SymEnv::new`, so this is the sole guard that the cheaper reuse
+/// path has not diverged. `sample_schema`'s entity hierarchy (`Thing in
+/// Account`) exercises the shared ancestor tables.
+#[test]
+fn sym_schema_sym_env_matches_sym_env_new() {
+    let schema = sample_schema();
+    let req_env = utils::req_env_from_strs("Identity", "Action::\"view\"", "Thing");
+    let reused = SymSchema::new(&schema).unwrap().sym_env(&req_env).unwrap();
+    let fresh = SymEnv::new(&schema, &req_env).unwrap();
+    assert_eq!(reused, fresh);
+}
+
+/// Multiple `sym_env` calls on the same `SymSchema` share the same `Arc`'d
+/// entities and each produce a result equal to a fresh `SymEnv::new`.
+#[test]
+fn sym_schema_reuse_across_envs() {
+    let schema = sample_schema();
+    let sym_schema = SymSchema::new(&schema).unwrap();
+    let req_env = utils::req_env_from_strs("Identity", "Action::\"view\"", "Thing");
+    let env_a = sym_schema.sym_env(&req_env).unwrap();
+    let env_b = sym_schema.sym_env(&req_env).unwrap();
+    // Both reuse the same underlying entities (Arc pointer equality).
+    assert!(Arc::ptr_eq(&env_a.entities, &env_b.entities));
+    // And both match a fresh build.
+    assert_eq!(env_a, SymEnv::new(&schema, &req_env).unwrap());
+}
+
+/// End-to-end example: use `SymSchema` to amortize `SymEntities` across
+/// request environments when calling `check_implies_opt`.
+#[tokio::test]
+async fn sym_schema_check_implies_opt_example() {
+    let schema = sample_schema();
+    let mut pset_a = PolicySet::new();
+    pset_a
+        .add(
+            Policy::parse(
+                Some(PolicyId::from_str("a").unwrap()),
+                r#"permit(principal, action == Action::"view", resource);"#,
+            )
+            .unwrap(),
+        )
+        .unwrap();
+    let mut pset_b = PolicySet::new();
+    pset_b
+        .add(
+            Policy::parse(
+                Some(PolicyId::from_str("b").unwrap()),
+                r#"permit(principal, action == Action::"view", resource);"#,
+            )
+            .unwrap(),
+        )
+        .unwrap();
+    let request_envs = vec![utils::req_env_from_strs(
+        "Identity",
+        "Action::\"view\"",
+        "Thing",
+    )];
+
+    let sym_schema = SymSchema::new(&schema).unwrap();
+    let mut compiler = CedarSymCompiler::new(LocalSolver::cvc5().unwrap()).unwrap();
+
+    for req_env in &request_envs {
+        let sym_env = sym_schema.sym_env(req_env).unwrap();
+        let compiled_a = CompiledPolicySet::compile_with_custom_symenv(
+            &pset_a,
+            req_env,
+            &schema,
+            sym_env.clone(),
+        )
+        .unwrap();
+        let compiled_b = CompiledPolicySet::compile_with_custom_symenv(
+            &pset_b,
+            req_env,
+            &schema,
+            sym_env.clone(),
+        )
+        .unwrap();
+        let implies = compiler
+            .check_implies_opt(&compiled_a, &compiled_b)
+            .await
+            .unwrap();
+        assert!(implies);
+    }
+}
+
+/// `SymSchema::sym_env` must surface `ActionNotInSchema` when the request env
+/// names an action absent from the schema, rather than panicking or building a
+/// bogus env.
+#[test]
+fn sym_schema_sym_env_rejects_unknown_action() {
+    let schema = sample_schema();
+    let req_env = utils::req_env_from_strs("Identity", "Action::\"nonexistent\"", "Thing");
+    let err = SymSchema::new(&schema)
+        .unwrap()
+        .sym_env(&req_env)
+        .unwrap_err();
+    assert!(
+        matches!(err, cedar_policy_symcc::err::Error::ActionNotInSchema(_)),
+        "expected ActionNotInSchema, got {err:?}"
+    );
+}