Standardize function naming: rename asserting to Asserting#48
Merged
Conversation
Two changes in Gobra broke this library: - viperproject/gobra#1024 replaced the predicate-constructor delimiters !<...!> with {...}. Update the oneshotInv constructor uses in resalgebra/oneshot_test.gobra accordingly. - viperproject/gobra#1036 lifted `asserting` expressions from Viper, making `asserting` a reserved keyword. Rename the user-defined `asserting` helper functions (and their call sites) to `Asserting` in resalgebra and in the program_proofs_example_10_2 evaluation experiments, matching the naming already used in util and refinementguard. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KscwsNqoA4o7nkNjcLbGCB
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
Per review feedback: when the asserted fact is the entire returned
expression, `return Asserting(cond)` is cleaner than
`return asserting cond in Unit{}`, since Asserting already returns
Unit{}. Revert the tail-position rewrites accordingly (sets, seqs,
dicts, resalgebra, the standard_library evaluation copies, and the
full/last_half experiments), restoring the Asserting definitions in
resalgebra and those two experiment files. Mid-chain uses keep the
native `asserting ... in` expression.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KscwsNqoA4o7nkNjcLbGCB
jcp19
marked this pull request as ready for review
July 5, 2026 10:49
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 standardizes the naming convention for the assertion helper function across the codebase by renaming
assertingtoAsserting(PascalCase). This aligns with Go naming conventions where exported functions use PascalCase.Key Changes
Renamed
assertingfunction toAssertingin all files where it is defined:evaluation/experiments/program_proofs_example_10_2/full/full.gobraevaluation/experiments/program_proofs_example_10_2/last_half/last_half.gobraevaluation/experiments/program_proofs_example_10_2/first_half/first_half.gobraevaluation/experiments/program_proofs_example_10_2/minimal/minimal.gobraUpdated all call sites to use
Assertinginstead ofasserting:resalgebra/product.gobra(40+ occurrences)resalgebra/loc.gobra(8 occurrences)resalgebra/ra.gobra(7 occurrences)resalgebra/oneshot_test.gobra(updated template syntax from!<...!>to{...})Implementation Details
The function signature remains unchanged:
This is a pure verification helper that requires its boolean argument to be true and returns a
Unitvalue. The rename improves consistency with Go naming conventions and makes the codebase more idiomatic.https://claude.ai/code/session_01KscwsNqoA4o7nkNjcLbGCB