Skip to content

Pass schema object as pointer to symcc targets #747

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
john-h-kastner-aws merged 3 commits into from
Sep 26, 2025
Merged

Pass schema object as pointer to symcc targets #747

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
de76c24
Pass schema object as pointer to symcc targets
john-h-kastner-aws Sep 15, 2025
87877dd
fmt
john-h-kastner-aws Sep 26, 2025
a7a040e
Fix CLI
john-h-kastner-aws Sep 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion cedar-drt/fuzz/fuzz_targets/symcc-smt-script-drt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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!(
Expand Down
3 changes: 2 additions & 1 deletion cedar-drt/fuzz/fuzz_targets/symcc-term-drt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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(
Expand Down
16 changes: 11 additions & 5 deletions cedar-drt/fuzz/fuzz_targets/symcc-term-roundtrip-abac-type-directed.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}"),
Expand All @@ -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(_) => (),
}
Expand Down
59 changes: 44 additions & 15 deletions cedar-lean-cli/src/analysis.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -457,10 +457,11 @@ fn policyset_vacuous(
let mut vr = Vec::new();

let lean_context = CedarLeanFfi::new();
let schema = lean_context.load_lean_schema_object(schema)?;
for req_env in req_envs {
if lean_context.run_check_always_allows(policyset, schema, req_env)? {
if lean_context.run_check_always_allows(policyset, schema.clone(), req_env)? {
vr.push(VacuityResult::MatchesAll);
} else if lean_context.run_check_always_denies(policyset, schema, req_env)? {
} else if lean_context.run_check_always_denies(policyset, schema.clone(), req_env)? {
vr.push(VacuityResult::MatchesNone);
} else {
vr.push(VacuityResult::MatchesSome);
Expand Down Expand Up @@ -518,6 +519,7 @@ fn compute_permit_shadowing_result(
})?;

let lean_context = CedarLeanFfi::new();
let schema = lean_context.load_lean_schema_object(schema)?;
for ((src_vr, tgt_vr), req_env) in zip(zip(src_vacuous_results, tgt_vacuous_results), req_envs)
{
match (src_vr, tgt_vr) {
Expand All @@ -534,10 +536,18 @@ fn compute_permit_shadowing_result(
results.push(ShadowingResult::TgtShadowsSrc)
}
(VacuityResult::MatchesSome, VacuityResult::MatchesSome) => {
let src_implies_tgt =
lean_context.run_check_implies(&src_pset, &tgt_pset, schema, req_env)?;
let tgt_implies_src =
lean_context.run_check_implies(&tgt_pset, &src_pset, schema, req_env)?;
let src_implies_tgt = lean_context.run_check_implies(
&src_pset,
&tgt_pset,
schema.clone(),
req_env,
)?;
let tgt_implies_src = lean_context.run_check_implies(
&tgt_pset,
&src_pset,
schema.clone(),
req_env,
)?;
match (src_implies_tgt, tgt_implies_src) {
(true, true) => results.push(ShadowingResult::Equivalent),
(true, _) => results.push(ShadowingResult::TgtShadowsSrc),
Expand Down Expand Up @@ -579,6 +589,7 @@ fn compute_forbid_overrides_shadow_result(
})?;

let lean_context = CedarLeanFfi::new();
let schema = lean_context.load_lean_schema_object(schema)?;
for ((forbid_vr, permit_vr), req_env) in zip(
zip(forbid_vacuous_results, permit_vacuous_results),
req_envs,
Expand All @@ -587,7 +598,7 @@ fn compute_forbid_overrides_shadow_result(
(VacuityResult::MatchesNone, _) | (VacuityResult::MatchesAll, _) | // forbid policy is vacous: does not apply or denies all
(_, VacuityResult::MatchesNone) | (_, VacuityResult::MatchesAll) => results.push(OverrideResult::NoResult), // permit policy is vacous: does not apply or allows all (no need to check overriding)
_ => {
if lean_context.run_check_implies(&permit_pset, &forbid_pset, schema, req_env)? {
if lean_context.run_check_implies(&permit_pset, &forbid_pset, schema.clone(), req_env)? {
results.push(OverrideResult::Overrides); // Every request allowed by permit is denied by forbid
} else {
results.push(OverrideResult::NoResult); // some request allowed by permit is not denies by forbid
Expand Down Expand Up @@ -619,6 +630,7 @@ fn compute_forbid_shadowing_result(
}
})?;
let lean_context = CedarLeanFfi::new();
let schema = lean_context.load_lean_schema_object(schema)?;
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
Expand All @@ -636,10 +648,18 @@ fn compute_forbid_shadowing_result(
results.push(ShadowingResult::TgtShadowsSrc) // Tgt policy denies all requests, Src denies some
}
(VacuityResult::MatchesSome, VacuityResult::MatchesSome) => {
let src_implies_tgt =
lean_context.run_check_implies(&src_pset, &tgt_pset, schema, req_env)?;
let tgt_implies_src =
lean_context.run_check_implies(&tgt_pset, &src_pset, schema, req_env)?;
let src_implies_tgt = lean_context.run_check_implies(
&src_pset,
&tgt_pset,
schema.clone(),
req_env,
)?;
let tgt_implies_src = lean_context.run_check_implies(
&tgt_pset,
&src_pset,
schema.clone(),
req_env,
)?;
match (src_implies_tgt, tgt_implies_src) {
(true, true) => results.push(ShadowingResult::Equivalent), // Equivalent
(true, _) => results.push(ShadowingResult::TgtShadowsSrc), // Tgt denies strictly more than Src
Expand Down Expand Up @@ -752,13 +772,22 @@ pub fn compare_policysets(
) -> Result<(), ExecError> {
let req_envs = OpenRequestEnv::any().to_request_envs(&schema)?;
let lean_context = CedarLeanFfi::new();
let schema = lean_context.load_lean_schema_object(&schema)?;
let comparison_results: Vec<PolicySetComparisonResult> = req_envs
.iter()
.map(|req_env| -> Result<PolicySetComparisonResult, ExecError> {
let fwd_implies =
lean_context.run_check_implies(&src_policyset, &tgt_policyset, &schema, req_env)?;
let bwd_implies =
lean_context.run_check_implies(&tgt_policyset, &src_policyset, &schema, req_env)?;
let fwd_implies = lean_context.run_check_implies(
&src_policyset,
&tgt_policyset,
schema.clone(),
req_env,
)?;
let bwd_implies = lean_context.run_check_implies(
&tgt_policyset,
&src_policyset,
schema.clone(),
req_env,
)?;
let status = match (fwd_implies, bwd_implies) {
(true, true) => PolicySetComparisonStatus::Equivalent,
(true, false) => PolicySetComparisonStatus::LessPermissive,
Expand Down
51 changes: 39 additions & 12 deletions cedar-lean-cli/src/symcc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,10 @@ pub fn run_check_never_errors(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
let mut results = Vec::new();
for req_env in req_envs.iter() {
results.push(lean_context.run_check_never_errors(&policy, &schema, req_env)?);
results.push(lean_context.run_check_never_errors(&policy, schema.clone(), req_env)?);
}
print_check_never_errors_results(&results, &req_envs, request_env);
Ok(())
Expand All @@ -43,9 +44,10 @@ pub fn run_check_always_allows(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
let mut results = Vec::new();
for req_env in req_envs.iter() {
results.push(lean_context.run_check_always_allows(&policyset, &schema, req_env)?);
results.push(lean_context.run_check_always_allows(&policyset, schema.clone(), req_env)?);
}
print_check_always_allows_results(&results, &req_envs, request_env);
Ok(())
Expand All @@ -59,9 +61,10 @@ pub fn run_check_always_denies(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
let mut results = Vec::new();
for req_env in req_envs.iter() {
results.push(lean_context.run_check_always_denies(&policyset, &schema, req_env)?);
results.push(lean_context.run_check_always_denies(&policyset, schema.clone(), req_env)?);
}
print_check_always_denies_results(&results, &req_envs, request_env);
Ok(())
Expand All @@ -76,12 +79,13 @@ pub fn run_check_equivalent(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
let mut results = Vec::new();
for req_env in req_envs.iter() {
results.push(lean_context.run_check_equivalent(
&src_policyset,
&tgt_policyset,
&schema,
schema.clone(),
req_env,
)?);
}
Expand All @@ -99,12 +103,13 @@ pub fn run_check_implies(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
let mut results = Vec::new();
for req_env in req_envs.iter() {
results.push(lean_context.run_check_implies(
&src_policyset,
&tgt_policyset,
&schema,
schema.clone(),
req_env,
)?);
}
Expand All @@ -120,12 +125,13 @@ pub fn run_check_disjoint(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
let mut results = Vec::new();
for req_env in req_envs.iter() {
results.push(lean_context.run_check_disjoint(
&src_policyset,
&tgt_policyset,
&schema,
schema.clone(),
req_env,
)?);
}
Expand All @@ -141,14 +147,15 @@ pub fn print_check_never_errors(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
for req_env in req_envs {
println!(";;");
println!(
";; SMTLib encoding for RequestEnv {}",
ReqEnv::Env(req_env.clone())
);
println!(";;");
lean_context.print_check_never_errors(&policy, &schema, &req_env)?;
lean_context.print_check_never_errors(&policy, schema.clone(), &req_env)?;
println!();
}
Ok(())
Expand All @@ -162,14 +169,15 @@ pub fn print_check_always_allows(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
for req_env in req_envs {
println!(";;");
println!(
";; SMTLib encoding for RequestEnv {}",
ReqEnv::Env(req_env.clone())
);
println!(";;");
lean_context.print_check_always_allows(&policyset, &schema, &req_env)?;
lean_context.print_check_always_allows(&policyset, schema.clone(), &req_env)?;
println!();
}
Ok(())
Expand All @@ -183,14 +191,15 @@ pub fn print_check_always_denies(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
for req_env in req_envs {
println!(";;");
println!(
";; SMTLib encoding for RequestEnv {}",
ReqEnv::Env(req_env.clone())
);
println!(";;");
lean_context.print_check_always_denies(&policyset, &schema, &req_env)?;
lean_context.print_check_always_denies(&policyset, schema.clone(), &req_env)?;
println!();
}
Ok(())
Expand All @@ -205,14 +214,20 @@ pub fn print_check_equivalent(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
for req_env in req_envs {
println!(";;");
println!(
";; SMTLib encoding for RequestEnv {}",
ReqEnv::Env(req_env.clone())
);
println!(";;");
lean_context.print_check_equivalent(&src_policyset, &tgt_policyset, &schema, &req_env)?;
lean_context.print_check_equivalent(
&src_policyset,
&tgt_policyset,
schema.clone(),
&req_env,
)?;
println!();
}
Ok(())
Expand All @@ -227,14 +242,20 @@ pub fn print_check_implies(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
for req_env in req_envs {
println!(";;");
println!(
";; SMTLib encoding for RequestEnv {}",
ReqEnv::Env(req_env.clone())
);
println!(";;");
lean_context.print_check_implies(&src_policyset, &tgt_policyset, &schema, &req_env)?;
lean_context.print_check_implies(
&src_policyset,
&tgt_policyset,
schema.clone(),
&req_env,
)?;
println!();
}
Ok(())
Expand All @@ -249,14 +270,20 @@ pub fn print_check_disjoint(
) -> Result<(), ExecError> {
let lean_context = CedarLeanFfi::new();
let req_envs = request_env.to_request_envs(&schema)?;
let schema = lean_context.load_lean_schema_object(&schema)?;
for req_env in req_envs {
println!(";;");
println!(
";; SMTLib encoding for RequestEnv {}",
ReqEnv::Env(req_env.clone())
);
println!(";;");
lean_context.print_check_disjoint(&src_policyset, &tgt_policyset, &schema, &req_env)?;
lean_context.print_check_disjoint(
&src_policyset,
&tgt_policyset,
schema.clone(),
&req_env,
)?;
println!();
}
Ok(())
Expand Down
Loading