Decode Z3 models containing sets#2422
Conversation
|
hi! Thanks for doing this. Can you provide some more documentation on exactly what you've added parsing for and what you've left unhandled? Ideally pointing to some z3 docs on what it emits if you were able to find those. |
Vedthakar
force-pushed
the
decode-z3-set-models
branch
from
2ef2796 to
3d35134
Compare
|
Thanks for the suggestion — I've added documentation to The docs now distinguish between: Existing support (via
Support added in this PR (via
The documentation also calls out the intentionally unsupported cases and the corresponding I've added references to the SMT-LIB The coverage table and references now live in the module-level docs in |
Signed-off-by: Ved Thakar <ved06.thakar@gmail.com>
Vedthakar
force-pushed
the
decode-z3-set-models
branch
from
be7811d to
25f0eca
Compare
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 82.39% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 87.90% Status: PASSED ✅ Details
|
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 82.39% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 87.90% Status: PASSED ✅ Details
|
|
I also have to ask here how much of this change was implemented by an LLM. As noted on the issue, one should be able to make a reasonable implementation, but I need to maintain a high standard of confidence that model decoding is in fact correct. I want to know if you feel you can vouch for the correctness of this code. |
| @@ -0,0 +1,52 @@ | |||
| thread 'rustc' panicked at /rustc-dev/e0e95a71872dfe9e15d22bddea9ac45c85ddda1a/compiler/rustc_middle/src/query/on_disk_cache.rs:663:9: | |||
There was a problem hiding this comment.
Is including these files intentional?
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 82.18% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 87.90% Status: PASSED ✅ Details
|
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 82.18% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 87.90% Status: PASSED ✅ Details
|
3 participants
Fixes #2415 by adding support for decoding Z3 set models in SymCC.
Previously, model decoding could fail on valid Z3 set representations such as:
((as const (Set Bool)) true)
(store ...)
(lambda ...)
(_ as-array k!N)
This change adds support for decoding these set encodings, reconstructing finite Cedar sets from Z3 models, and introduces explicit errors for unsupported or non-finite set models.
Also adds test coverage for the reported Z3 set model formats and associated error cases.
Closes #2415
Checklist for requesting a review
The change in this PR is (choose one, and delete the other options):
A breaking change requiring a major version bump to cedar-policy (e.g., changes to the signature of an existing API).
A backwards-compatible change requiring a minor version bump to cedar-policy (e.g., addition of a new API).
A bug fix or other functionality change requiring a patch to cedar-policy.
A change "invisible" to users (e.g., documentation, changes to "internal" crates like cedar-policy-core, cedar-validator, etc.)
A change (breaking or otherwise) that only impacts unreleased or experimental code.
I confirm that this PR (choose one, and delete the other options):
Updates the "Unreleased" section of the CHANGELOG with a description of my change (required for major/minor version bumps).
Does not update the CHANGELOG because my change does not significantly impact released code.
I confirm that cedar-spec (choose one, and delete the other options):
Does not require updates because my change does not impact the Cedar formal model or DRT infrastructure.
Requires updates, and I have made / will make these updates myself.
Requires updates, but I do not plan to make them in the near future.
I'm not sure how my change impacts cedar-spec.
I confirm that docs.cedarpolicy.com (choose one, and delete the other options):
Does not require updates because my change does not impact the Cedar language specification.
Requires updates, and I have made / will make these updates myself.
I'm not sure how my change impacts the documentation.
One minor note: depending on Cedar maintainer preference, they may consider this a feature request implementation rather than a pure bug fix because the issue is labeled feature-request. If someone comments on that, it's normal, but I'd still mark it as a patch-level functionality change exactly as you've done.