From 8b682e1bb375a296fc4cf4e483d87416e2a66bb7 Mon Sep 17 00:00:00 2001 From: Thomas Hill Date: Thu, 9 Jul 2026 17:14:53 -0700 Subject: [PATCH 1/3] symcc: add SymSchema for amortized SymEntities across request envs Wrap SymEntities inner BTreeMap in Arc for cheap cloning. Add SymSchema struct that precomputes SymEntities once per schema and produces SymEnv instances via sym_env(), reusing the shared entities. Callers checking many request environments against the same schema (e.g. policy subsumption with large action lists) avoid rebuilding symbolic entities per environment: - without SymSchema: ~3.7s/env - with SymSchema: ~0.9ms/env + 1.86s one-time build Signed-off-by: Thomas Hill --- cedar-policy-symcc/CHANGELOG.md | 5 + cedar-policy-symcc/src/lib.rs | 2 +- cedar-policy-symcc/src/symcc.rs | 2 +- cedar-policy-symcc/src/symcc/encoder.rs | 17 +-- cedar-policy-symcc/src/symcc/env.rs | 54 ++++++++- .../src/symcc/interpretation.rs | 4 +- cedar-policy-symcc/src/symcc/symbolizer.rs | 4 +- cedar-policy-symcc/tests/integration_tests.rs | 108 +++++++++++++++++- 8 files changed, 177 insertions(+), 19 deletions(-) diff --git a/cedar-policy-symcc/CHANGELOG.md b/cedar-policy-symcc/CHANGELOG.md index e317cf2b97..2f76d2f613 100644 --- a/cedar-policy-symcc/CHANGELOG.md +++ b/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 diff --git a/cedar-policy-symcc/src/lib.rs b/cedar-policy-symcc/src/lib.rs index 1ecf80c3d1..573b41c159 100644 --- a/cedar-policy-symcc/src/lib.rs +++ b/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`]. diff --git a/cedar-policy-symcc/src/symcc.rs b/cedar-policy-symcc/src/symcc.rs index 7219250780..508aadef79 100644 --- a/cedar-policy-symcc/src/symcc.rs +++ b/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; diff --git a/cedar-policy-symcc/src/symcc/encoder.rs b/cedar-policy-symcc/src/symcc/encoder.rs index 125ae21c89..ffb8422234 100644 --- a/cedar-policy-symcc/src/symcc/encoder.rs +++ b/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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::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: SymEntities(Arc::new(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); let entity_type_name = EntityTypeName::from_str("User").unwrap(); diff --git a/cedar-policy-symcc/src/symcc/env.rs b/cedar-policy-symcc/src/symcc/env.rs index 4135c68887..2402d653c2 100644 --- a/cedar-policy-symcc/src/symcc/env.rs +++ b/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}, @@ -114,13 +115,13 @@ impl SymEntityData { } #[derive(Clone, Debug, PartialEq, Eq, Ord, PartialOrd)] -pub struct SymEntities(pub BTreeMap); +pub struct SymEntities(pub Arc>); impl Deref for SymEntities { type Target = BTreeMap; fn deref(&self) -> &Self::Target { - &self.0 + self.0.as_ref() } } @@ -366,9 +367,9 @@ impl SymEntities { SymEntityData::of_action_type(act_ty, act_tys.clone(), schema), )) }); - Ok(SymEntities( + Ok(SymEntities(Arc::new( e_data.into_iter().chain(a_data).collect::>()?, - )) + ))) } } @@ -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: SymEntities, +} + +impl SymSchema { + /// Builds the symbolic entities for `schema` once, up front. + pub fn new(schema: &Schema) -> crate::err::Result { + Ok(Self { + schema: schema.clone(), + entities: 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 { + 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 diff --git a/cedar-policy-symcc/src/symcc/interpretation.rs b/cedar-policy-symcc/src/symcc/interpretation.rs index c45e3c070b..033e4e8e32 100644 --- a/cedar-policy-symcc/src/symcc/interpretation.rs +++ b/cedar-policy-symcc/src/symcc/interpretation.rs @@ -304,12 +304,12 @@ impl SymEntityData { impl SymEntities { /// Interpret a [`SymEntities`] with the given interpretation. pub fn interpret(&self, interp: &Interpretation<'_>) -> SymEntities { - SymEntities( + SymEntities(Arc::new( self.0 .iter() .map(|(ent, data)| (ent.clone(), data.interpret(interp))) .collect(), - ) + )) } } diff --git a/cedar-policy-symcc/src/symcc/symbolizer.rs b/cedar-policy-symcc/src/symcc/symbolizer.rs index b1e6f6c33a..0e7951c3b0 100644 --- a/cedar-policy-symcc/src/symcc/symbolizer.rs +++ b/cedar-policy-symcc/src/symcc/symbolizer.rs @@ -403,12 +403,12 @@ impl SymEntities { )) }); - Ok(SymEntities( + Ok(SymEntities(Arc::new( entities .into_iter() .chain(actions) .collect::>()?, - )) + ))) } } diff --git a/cedar-policy-symcc/tests/integration_tests.rs b/cedar-policy-symcc/tests/integration_tests.rs index 5ad5294b3b..b369f7212d 100644 --- a/cedar-policy-symcc/tests/integration_tests.rs +++ b/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.0, &env_b.entities.0)); + // 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:?}" + ); +} From c9076e0d13a1105875497b2e03c4dbcbfbb76d67 Mon Sep 17 00:00:00 2001 From: Thomas Hill Date: Fri, 10 Jul 2026 01:35:06 -0700 Subject: [PATCH 2/3] symcc: move Arc from SymEntities inner to SymEnv/SymSchema field MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SymEntities reverted to a plain BTreeMap wrapper — the Arc now lives on SymEnv.entities and SymSchema.entities, keeping SymEntities a value type while preserving cheap Arc-clone sharing in SymSchema::sym_env(). Signed-off-by: Thomas Hill --- cedar-policy-symcc/src/symcc/encoder.rs | 16 ++++++++-------- cedar-policy-symcc/src/symcc/env.rs | 16 ++++++++-------- cedar-policy-symcc/src/symcc/interpretation.rs | 6 +++--- cedar-policy-symcc/src/symcc/symbolizer.rs | 6 +++--- cedar-policy-symcc/tests/integration_tests.rs | 2 +- 5 files changed, 23 insertions(+), 23 deletions(-) diff --git a/cedar-policy-symcc/src/symcc/encoder.rs b/cedar-policy-symcc/src/symcc/encoder.rs index ffb8422234..bd441e7485 100644 --- a/cedar-policy-symcc/src/symcc/encoder.rs +++ b/cedar-policy-symcc/src/symcc/encoder.rs @@ -766,7 +766,7 @@ mod unit_tests { async fn declare_type() { let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); encoder @@ -779,7 +779,7 @@ mod unit_tests { async fn declare_entity_type() { let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); let ety = cedar_policy::EntityTypeName::from_str("User").unwrap(); @@ -792,7 +792,7 @@ mod unit_tests { async fn declare_empty_record_type() { let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); encoder.declare_record_type(vec![]).await.unwrap(); @@ -802,7 +802,7 @@ mod unit_tests { async fn declare_record_type() { let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); encoder @@ -815,7 +815,7 @@ mod unit_tests { async fn encode_bool_type() { let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); encoder.encode_type(&TermType::Bool).await.unwrap(); @@ -825,7 +825,7 @@ mod unit_tests { async fn encode_string_type() { let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); encoder.encode_type(&TermType::String).await.unwrap(); @@ -835,7 +835,7 @@ mod unit_tests { async fn encode_uuf() { let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); let my_uuf = crate::symcc::op::Uuf { @@ -851,7 +851,7 @@ mod unit_tests { use cedar_policy::EntityUid; let symenv = SymEnv { request: SymRequest::empty_sym_req(), - entities: SymEntities(Arc::new(BTreeMap::new())), + entities: Arc::new(SymEntities(BTreeMap::new())), }; let mut encoder = Encoder::new(&symenv, Vec::::new()).unwrap(); let entity_type_name = EntityTypeName::from_str("User").unwrap(); diff --git a/cedar-policy-symcc/src/symcc/env.rs b/cedar-policy-symcc/src/symcc/env.rs index 2402d653c2..fb50878c19 100644 --- a/cedar-policy-symcc/src/symcc/env.rs +++ b/cedar-policy-symcc/src/symcc/env.rs @@ -115,13 +115,13 @@ impl SymEntityData { } #[derive(Clone, Debug, PartialEq, Eq, Ord, PartialOrd)] -pub struct SymEntities(pub Arc>); +pub struct SymEntities(pub BTreeMap); impl Deref for SymEntities { type Target = BTreeMap; fn deref(&self) -> &Self::Target { - self.0.as_ref() + &self.0 } } @@ -174,7 +174,7 @@ pub struct SymEnv { /// Symbolic request pub request: SymRequest, /// Symbolic entities - pub entities: SymEntities, + pub entities: Arc, } impl SymEnv { @@ -367,9 +367,9 @@ impl SymEntities { SymEntityData::of_action_type(act_ty, act_tys.clone(), schema), )) }); - Ok(SymEntities(Arc::new( + Ok(SymEntities( e_data.into_iter().chain(a_data).collect::>()?, - ))) + )) } } @@ -404,7 +404,7 @@ impl SymEnv { pub fn of_env(ty_env: &Environment<'_>) -> Result { 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)?), }) } } @@ -430,7 +430,7 @@ impl SymEnv { #[derive(Debug, Clone)] pub struct SymSchema { schema: Schema, - entities: SymEntities, + entities: Arc, } impl SymSchema { @@ -438,7 +438,7 @@ impl SymSchema { pub fn new(schema: &Schema) -> crate::err::Result { Ok(Self { schema: schema.clone(), - entities: SymEntities::of_schema(schema.as_ref())?, + entities: Arc::new(SymEntities::of_schema(schema.as_ref())?), }) } diff --git a/cedar-policy-symcc/src/symcc/interpretation.rs b/cedar-policy-symcc/src/symcc/interpretation.rs index 033e4e8e32..556409c785 100644 --- a/cedar-policy-symcc/src/symcc/interpretation.rs +++ b/cedar-policy-symcc/src/symcc/interpretation.rs @@ -304,12 +304,12 @@ impl SymEntityData { impl SymEntities { /// Interpret a [`SymEntities`] with the given interpretation. pub fn interpret(&self, interp: &Interpretation<'_>) -> SymEntities { - SymEntities(Arc::new( + SymEntities( self.0 .iter() .map(|(ent, data)| (ent.clone(), data.interpret(interp))) .collect(), - )) + ) } } @@ -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), } } diff --git a/cedar-policy-symcc/src/symcc/symbolizer.rs b/cedar-policy-symcc/src/symcc/symbolizer.rs index 0e7951c3b0..68837694d2 100644 --- a/cedar-policy-symcc/src/symcc/symbolizer.rs +++ b/cedar-policy-symcc/src/symcc/symbolizer.rs @@ -403,12 +403,12 @@ impl SymEntities { )) }); - Ok(SymEntities(Arc::new( + Ok(SymEntities( entities .into_iter() .chain(actions) .collect::>()?, - ))) + )) } } @@ -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)?), }) } } diff --git a/cedar-policy-symcc/tests/integration_tests.rs b/cedar-policy-symcc/tests/integration_tests.rs index b369f7212d..5b1a45450b 100644 --- a/cedar-policy-symcc/tests/integration_tests.rs +++ b/cedar-policy-symcc/tests/integration_tests.rs @@ -2558,7 +2558,7 @@ fn sym_schema_reuse_across_envs() { 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.0, &env_b.entities.0)); + 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()); } From 4c0a13b0502e2400c0d3b1b2a8ea8c325d6db21a Mon Sep 17 00:00:00 2001 From: Thomas Hill Date: Thu, 16 Jul 2026 15:39:25 -0700 Subject: [PATCH 3/3] symcc: rename SymSchema to CompiledSchema MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rename SymSchema -> CompiledSchema to better reflect that the schema itself isn't symbolic — the entities are. CompiledSchema parallels CompiledPolicy, which similarly wraps a type-checked artifact plus its symbolic representation. Signed-off-by: Thomas Hill --- cedar-policy-symcc/CHANGELOG.md | 2 +- cedar-policy-symcc/src/lib.rs | 2 +- cedar-policy-symcc/src/symcc.rs | 2 +- cedar-policy-symcc/src/symcc/env.rs | 10 +++--- cedar-policy-symcc/tests/integration_tests.rs | 36 ++++++++++--------- 5 files changed, 28 insertions(+), 24 deletions(-) diff --git a/cedar-policy-symcc/CHANGELOG.md b/cedar-policy-symcc/CHANGELOG.md index 2f76d2f613..9c229573f4 100644 --- a/cedar-policy-symcc/CHANGELOG.md +++ b/cedar-policy-symcc/CHANGELOG.md @@ -10,7 +10,7 @@ Cedar Language Version: TBD ### Added -- `SymSchema` type that precomputes symbolic entities once per schema and produces +- `CompiledSchema` type that precomputes symbolic entities once per schema and produces `SymEnv` instances via `sym_env()`, avoiding expensive per-environment rebuilds. ### Fixed diff --git a/cedar-policy-symcc/src/lib.rs b/cedar-policy-symcc/src/lib.rs index 573b41c159..43f6be957e 100644 --- a/cedar-policy-symcc/src/lib.rs +++ b/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, SymSchema}; +pub use symcc::{CompiledSchema, Env, SmtLibScript, SymEnv}; impl SymEnv { /// Constructs a new [`SymEnv`] from the given [`Schema`] and [`RequestEnv`]. diff --git a/cedar-policy-symcc/src/symcc.rs b/cedar-policy-symcc/src/symcc.rs index 508aadef79..b054b2d1ce 100644 --- a/cedar-policy-symcc/src/symcc.rs +++ b/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, SymSchema}; +pub use env::{CompiledSchema, Environment, SymEnv}; pub use interpretation::Interpretation; pub use result::CompileError; pub use smtlib_script::SmtLibScript; diff --git a/cedar-policy-symcc/src/symcc/env.rs b/cedar-policy-symcc/src/symcc/env.rs index fb50878c19..61a21c770d 100644 --- a/cedar-policy-symcc/src/symcc/env.rs +++ b/cedar-policy-symcc/src/symcc/env.rs @@ -423,17 +423,17 @@ impl SymEnv { /// 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 +/// schema, not on any particular request environment. [`CompiledSchema`] computes it /// once so it can be reused across many request environments via -/// [`SymSchema::sym_env`], which is significantly cheaper than rebuilding the +/// [`CompiledSchema::sym_env`], which is significantly cheaper than rebuilding the /// symbolic entities per environment (as [`SymEnv::new`] does). #[derive(Debug, Clone)] -pub struct SymSchema { +pub struct CompiledSchema { schema: Schema, entities: Arc, } -impl SymSchema { +impl CompiledSchema { /// Builds the symbolic entities for `schema` once, up front. pub fn new(schema: &Schema) -> crate::err::Result { Ok(Self { @@ -454,7 +454,7 @@ impl SymSchema { /// [`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. + // Guarded by test compiled_schema_sym_env_matches_sym_env_new. pub fn sym_env(&self, req_env: &RequestEnv) -> crate::err::Result { let env = Environment::from_request_env(req_env, self.schema.as_ref()) .ok_or_else(|| crate::err::Error::ActionNotInSchema(req_env.action().to_string()))?; diff --git a/cedar-policy-symcc/tests/integration_tests.rs b/cedar-policy-symcc/tests/integration_tests.rs index 5b1a45450b..36be09214d 100644 --- a/cedar-policy-symcc/tests/integration_tests.rs +++ b/cedar-policy-symcc/tests/integration_tests.rs @@ -17,7 +17,8 @@ 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, SymEnv, SymSchema, + err::CompileError, solver::LocalSolver, CedarSymCompiler, CompiledPolicySet, CompiledSchema, + SymEnv, }; use cool_asserts::assert_matches; use std::collections::HashMap; @@ -2533,40 +2534,43 @@ async fn template_linked_policy_unsupported() { ); } -/// `SymSchema::sym_env` reuses shared symbolic entities across request envs +/// `CompiledSchema::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() { +fn compiled_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 reused = CompiledSchema::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 +/// Multiple `sym_env` calls on the same `CompiledSchema` share the same `Arc`'d /// entities and each produce a result equal to a fresh `SymEnv::new`. #[test] -fn sym_schema_reuse_across_envs() { +fn compiled_schema_reuse_across_envs() { let schema = sample_schema(); - let sym_schema = SymSchema::new(&schema).unwrap(); + let compiled_schema = CompiledSchema::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(); + let env_a = compiled_schema.sym_env(&req_env).unwrap(); + let env_b = compiled_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 +/// End-to-end example: use `CompiledSchema` to amortize `SymEntities` across /// request environments when calling `check_implies_opt`. #[tokio::test] -async fn sym_schema_check_implies_opt_example() { +async fn compiled_schema_check_implies_opt_example() { let schema = sample_schema(); let mut pset_a = PolicySet::new(); pset_a @@ -2594,11 +2598,11 @@ async fn sym_schema_check_implies_opt_example() { "Thing", )]; - let sym_schema = SymSchema::new(&schema).unwrap(); + let compiled_schema = CompiledSchema::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 sym_env = compiled_schema.sym_env(req_env).unwrap(); let compiled_a = CompiledPolicySet::compile_with_custom_symenv( &pset_a, req_env, @@ -2621,14 +2625,14 @@ async fn sym_schema_check_implies_opt_example() { } } -/// `SymSchema::sym_env` must surface `ActionNotInSchema` when the request env +/// `CompiledSchema::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() { +fn compiled_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) + let err = CompiledSchema::new(&schema) .unwrap() .sym_env(&req_env) .unwrap_err();