Skip to content

Repair batched evaluation proof#833

Open
john-h-kastner-aws wants to merge 5 commits intomainfrom
repair-batched-eval
Open

Repair batched evaluation proof#833
john-h-kastner-aws wants to merge 5 commits intomainfrom
repair-batched-eval

Conversation

@john-h-kastner-aws
Copy link
Contributor

@john-h-kastner-aws john-h-kastner-aws commented Jan 22, 2026 •
edited
Loading

cedar-lean/Cedar/Thm/TPE/BatchedEvaluator.lean was not imported in any other files, so what look like unintentionally committed changes in #736 were not detected. Fortunately nothing substantial about TPE or batched eval has changed, so fixing the proof is straightforward.

cdisselkoen
cdisselkoen approved these changes Jan 22, 2026
View reviewed changes
Copy link
Contributor

@cdisselkoen cdisselkoen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should also rename the file

@john-h-kastner-aws
Copy link
Contributor Author

john-h-kastner-aws commented Jan 22, 2026 •
edited
Loading

Also make the checkThm script stricter to check that all submodules of Thm are always imported by their parents. It's a little over-eager and flags false positives where the submodule is eventually imported into Cedar.Thm, but these are easy enough to fix, so I think it's worth enforcing this.

john-h-kastner-aws and others added 5 commits January 23, 2026 16:28
@john-h-kastner-aws
repair batched evaluation proof
38a8ab2 
Signed-off-by: John Kastner <jkastner@amazon.com>
@john-h-kastner-aws
recursive checkThm
e5eb486 
Signed-off-by: John Kastner <jkastner@amazon.com>
@john-h-kastner-aws
stricter recursive import check
03f3cf3 
Signed-off-by: John Kastner <jkastner@amazon.com>
@john-h-kastner-aws
Restore \n in expected import text
01e4fcc
@john-h-kastner-aws
rebase and add import
d0b828e 
Signed-off-by: John Kastner <jkastner@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@cdisselkoen cdisselkoen cdisselkoen approved these changes

@lianah lianah Awaiting requested review from lianah

At least 2 approving reviews are required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@john-h-kastner-aws @cdisselkoen