rewrite symcc's extractor.rs to better correspond to the Lean #2089
Conversation
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
cdisselkoen
requested review from
emina,
john-h-kastner-aws,
katherine-hough and
lianah
| default: udf.default.clone(), | ||
| arg: udf.arg.clone(), | ||
| out: udf.out, | ||
| default: match &udf.out { | ||
| TermType::Set { ty } => factory::set_of([], (**ty).clone()), | ||
| _ => udf.default, | ||
| }, | ||
| ..udf |
There was a problem hiding this comment.
I suspect this in particular is the bug fix
There was a problem hiding this comment.
I see, before it used the default value in the model instead of setting it to the empty set for entities not in the footprint. Can line 106 ever happen? The ancestor function always returns a Set and this only gets called for ancestors.
There was a problem hiding this comment.
Yeah it probably can't, so putting anything is sound. We just do what the Lean does, and therefore enjoy the Lean soundness proofs
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 97.30% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 86.12% Status: PASSED ✅ Details
|
| assert_implies(&mut compiler, &pset1, &pset2, &envs).await; | ||
| assert_does_not_imply(&mut compiler, &pset2, &pset1, &envs).await; |
There was a problem hiding this comment.
I assume these also assert something about the decoded counter example?
Assuming it does, it might still be useful to have a direct test for decoding a supposed cycle. (easier to debug if it starts failing, can't change depending on cvc5 version or change to the smt query).
There was a problem hiding this comment.
Yes, they check that the counterexample's request and entities both validate against the schema (although they do not actually check the authorization behavior of the counterexample).
I'll look into making a unit test for decoding
There was a problem hiding this comment.
Spent an hour and cannot get a test which succeeds with the right footprint and fails with the wrong footprint -- must be doing something wrong when trying to initialize the SymEnv and Interpretation that SymEnv::extract() requires. Will delay this testing idea to a future PR.
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 97.44% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 86.13% Status: PASSED ✅ Details
|
Description of changes
Rewrites SymCC's extractor.rs to better correspond to Lean's Extractor.lean. In the process, fixes a bug (the added test case in this PR was failing but is now fixed).
Issue #, if available
Checklist for requesting a review
The change in this PR is (choose one, and delete the other options):
cedar-policy.I confirm that this PR (choose one, and delete the other options):
I confirm that
cedar-spec(choose one, and delete the other options):I confirm that
docs.cedarpolicy.com(choose one, and delete the other options):