Refactor asserting/Asserting to use in syntax and remove function definitions#47
Closed
jcp19 wants to merge 2 commits into
Closed
Refactor asserting/Asserting to use in syntax and remove function definitions#47jcp19 wants to merge 2 commits into
in syntax and remove function definitions#47jcp19 wants to merge 2 commits into
Conversation
Delete all pure helper functions named asserting/Asserting and rewrite every usage with Gobra's built-in asserting expression (asserting <assertion> in <expression>), introduced in viperproject/gobra#1036.
Remove the parentheses around the assertion of an asserting expression when the assertion is simple enough that removal is unambiguous (keeping them only for quantified or let-bearing assertions). Also place the synthesized Unit/util.Unit return value on its own line.
jcp19
pushed a commit
that referenced
this pull request
Jul 4, 2026
Gobra now supports `asserting <cond> in <expr>` natively (viperproject/gobra#1036), so replace calls to the Asserting helper functions with asserting expressions and drop the definitions that are no longer used (refinementguard, resalgebra, and the program_proofs_example_10_2 experiments). This adopts the rewrites from PR #47. The one exception (which made PR #47's CI fail with termination errors at dicts.gobra:117) is the fact established inside dicts' `Remove`: `Union`'s termination proof needs `ys intersection domain(d) == ys` to be available when Remove's body is inlined at the recursive call sites, which works with the `util.Asserting` call but not with an `asserting` expression. Keep `util.Asserting` there (and in the two evaluation copies of dicts), and hence keep its definition in both util packages. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KscwsNqoA4o7nkNjcLbGCB
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
2 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.
Summary
This PR refactors the
asserting/Assertinghelper functions across the codebase to use Gobra'sinexpression syntax instead ofletbindings, and removes the now-redundant function definitions from utility modules.Key Changes
Syntax modernization: Converted all
asserting(condition)calls fromlet _ := asserting(...)patterns toasserting (...) inexpressions, which is more idiomatic in GobraReturn type consistency: Added explicit
in Unit{}returns where needed to ensure proper type alignment with the new syntaxFunction removal: Deleted deprecated
asserting/Assertingfunction definitions from:util/util.gobraevaluation/experiments/standard_library/util/util.gobrarefinementguard/util.gobrafull.gobra,last_half.gobra,first_half.gobra,minimal.gobra)Whitespace normalization: Added consistent spacing around
assertingcalls (e.g.,asserting (...)instead ofasserting(...))Files Modified
resalgebra/product.gobra- Multiple asserting calls refactoredresalgebra/ra.gobra- Asserting calls in query functions updatedresalgebra/loc.gobra- Frame lemma asserting calls refactoredrefinementguard/lii.gobra- Asserting calls converted toinsyntaxdicts/dicts.gobra- Dictionary operation asserting calls updatedseqs/seqs.gobra- Sequence operation asserting calls updatedsets/sets.gobra- Set operation asserting calls updatedImplementation Details
The refactoring maintains semantic equivalence while improving code clarity. The
insyntax is more explicit about the scope and sequencing of assertions within proof expressions, making the code easier to read and maintain.https://claude.ai/code/session_01PwdWmKZjxyysaGtdgYU5La