Skip to content

feat(llzk): more local invariants checks (array), refactor common checks - #1389

Open
Maschmalow wants to merge 2 commits into
opencompl:VERIFY-2026/llzk-07-struct-arrayfrom
Maschmalow:VERIFY-2026/llzk-07-struct-array
Open

Maschmalow wants to merge 2 commits into
opencompl:VERIFY-2026/llzk-07-struct-arrayfrom
Maschmalow:VERIFY-2026/llzk-07-struct-array

Conversation

@Maschmalow

Copy link
Copy Markdown
Contributor
  • added common LLZK type checks in Verifier.Basic and refactor existing usage
  • added array operations local invariants checks

@Maschmalow
Maschmalow marked this pull request as ready for review September 4, 2026 18:46

@tobiasgrosser tobiasgrosser left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

This LGTM. @AlexanderViand, what do you think?

AlexanderViand

This comment was marked as duplicate.

@AlexanderViand AlexanderViand left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I asked Claude to check this against LLZK (ba936ff) and it looks good, veir-opt seems to be a bit more permissive than llzk-opt, but that seems OK for now.

It would be nice to add some tests, but probably not super essential given that the source of truth is LLZK anyway.

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.

3 participants