add json and protobuf serialization of some tpe types + fix#922
Merged
victornicolet merged 2 commits intomainfrom Apr 8, 2026
Merged
add json and protobuf serialization of some tpe types + fix#922victornicolet merged 2 commits intomainfrom
victornicolet merged 2 commits intomainfrom
Conversation
…es validation split between entities and actions Signed-off-by: Victor Nicolet <victornl@amazon.com>
Contributor
Author
|
Building cedar-spec-drt will fail until #921 is merged. |
victornicolet
commented
Apr 3, 2026
| @@ -89,6 +94,13 @@ def requestIsValid (env : TypeEnv) (req : PartialRequest) : Bool := | |||
| def entitiesIsValid (env : TypeEnv) (es : PartialEntities) : Bool := | |||
| (es.toList.all entityIsValid) && (env.acts.toList.all instanceOfActionSchema) | |||
| where | |||
Contributor
Author
There was a problem hiding this comment.
There is a fix here that I think is necessary. What I don't understand fully is what kind of pairs of TypeEnv and PartialEntities were valid before, if any. Let me know if I'm missing something
Contributor
There was a problem hiding this comment.
I think it can be valid as long as the type of every action is declared as an entity type. This is inconsistent with how we normally think about schemas, but it's not really a problem.
See
cedar-spec/cedar-lean/UnitTest/TPE.lean
Lines 73 to 76 in b5763d1
I agree with this fix, but I don't think it will have any consequences for the proofs/algorithms
john-h-kastner-aws
approved these changes
Apr 3, 2026
…nicolet/tpe-ffi-lean
lianah
approved these changes
Apr 7, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This adds some serialization/deserialization utilities for some TPE entities to build the FFI for
TPE.isAuthorized.Also makes a small change in
cedar-lean/Cedar/TPE/Input.lean: previously, theentitiesIsValidfunction would validate all entities in thePartialEntitiesagainst only the entity schema. If an action is in thePartialEntities, validation would fail. But the validation also requires the actions to be in partial entities (env.acts.toList.all instanceOfActionSchemaandinstanceOfActionSchematries to find the action in thePartialEntities). The Rust side automatically inserts the actions in the partial entities as far as I understand.