Skip to content

Conversation

@shazqadeer
Copy link
Contributor

@shazqadeer shazqadeer commented Jan 20, 2026

Call to pure action is treated specially on the disappearing layer of the caller. At lower layers, the gate is asserted during invariant checking. But at the disappearing layer, the gate is assumed during invariant checking and asserted during refinement checking. This PR introduces a special pure action Assert which can be used as an alternative to the assert statement with the behavior explained above. As a result, the semantics of assert statements becomes simple; they are asserted during invariant checking and assumed during refinement checking.

@shazqadeer shazqadeer merged commit 23f70c0 into master Jan 21, 2026
8 of 9 checks passed
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.

2 participants