Skip to content

Adds Unbounded Integer Type - #1033

Merged
ArquintL merged 8 commits into
masterfrom
arquintl-unbounded-int
Jun 2, 2026
Merged

Adds Unbounded Integer Type#1033
ArquintL merged 8 commits into
masterfrom
arquintl-unbounded-int

Conversation

@ArquintL

@ArquintL ArquintL commented Jun 2, 2026

Copy link
Copy Markdown
Member

Adds integer as an explicit unbounded integer type while leaving int and uint unchanged so far

Contains some changes from #1014 and #1015

@copilot summary:
This PR introduces integer as an explicit unbounded integer ghost type, while keeping int and uint behavior unchanged. In addition, it rejects bitwise and shift operators on values of type integer and adds regression tests for the new type behavior.

ArquintL and others added 3 commits June 2, 2026 09:57
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Copilot AI review requested due to automatic review settings June 2, 2026 03:07

This comment was marked as outdated.

ArquintL and others added 2 commits June 2, 2026 11:41
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
@ArquintL
ArquintL requested a review from jcp19 June 2, 2026 03:46
@viperproject viperproject deleted a comment from Copilot AI Jun 2, 2026
@ArquintL

ArquintL commented Jun 2, 2026

Copy link
Copy Markdown
Member Author

I've reverted the last two commits as they result in several CI failures that would all require a proper type inference mechanism, i.e., the one that #1014 will introduce. In the interest of keeping this PR small, I'm avoiding this change, which means that assigning an integer to an int in ghost code won't result in a type-error for now as int uses unbounded semantics.

@jcp19 jcp19 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.

LGTM, but I am a bit surprised about the new syntax for perm being included here. That is fine by me, but we should at least add more tests (e.g., show that it produces the expected values at verification time)

Co-authored-by: João Pereira <joaopereira.19@gmail.com>
@ArquintL
ArquintL enabled auto-merge (squash) June 2, 2026 09:14
@ArquintL
ArquintL merged commit eff4f89 into master Jun 2, 2026
3 checks passed
@ArquintL
ArquintL deleted the arquintl-unbounded-int branch June 2, 2026 09:31
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