Skip to content

Model and proofs for unknown attribute extension to TPE - #1015

Open
john-h-kastner-aws wants to merge 4 commits into
mainfrom
tpe-lean-model
Open

john-h-kastner-aws wants to merge 4 commits into
mainfrom
tpe-lean-model

Conversation

@john-h-kastner-aws

@john-h-kastner-aws john-h-kastner-aws commented Sep 2, 2026 •

Copy link
Copy Markdown
Contributor

Lean model and proofs for

cedar-policy/cedar#2547

This makes the minimal update to the protobuf to keep DRT working. Future PRs will update DRT to generate and transmit fine-grained partial attributes

Extends the TPE model so that `has`, `hasTag`, `in`, `==`, and `is`
reduce to literals when type information in the schema (plus
error-freedom) is enought to reach a concrete value.

Signed-off-by: jkastner <jkastner@amazon.com>
Signed-off-by: jkastner <jkastner@amazon.com>
Signed-off-by: jkastner <jkastner@amazon.com>
Signed-off-by: jkastner <jkastner@amazon.com>
Base automatically changed from tpe-has-reduction-proof to main September 23, 2026 18:22
@victornicolet
victornicolet requested review from lianah, luxas and victornicolet and removed request for lianah, luxas and victornicolet September 28, 2026 17:58

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant