fix(verify): correct modifies-array call-site argument binding#7
Open
kondylidou wants to merge 1 commit into
Open
fix(verify): correct modifies-array call-site argument binding#7kondylidou wants to merge 1 commit into
kondylidou wants to merge 1 commit into
Conversation
joscoh
reviewed
Jul 21, 2026
| return modifiesArgs ++ readOnlyArgs | ||
|
|
||
| /-- `@[reachCheck]` on `assert`/`cover` marks a reachability check. Core's DDM grammar | ||
| used to have a dedicated `ReachCheck` category for this; it was folded into the |
Contributor
There was a problem hiding this comment.
Nit, but comments should be stateless
| Regression test for a caller/callee pair where the callee both `modifies` an | ||
| array-typed global (threaded through the call site as an extra `inout` | ||
| argument) and takes a plain `int` input that is referenced in its own | ||
| `ensures` clause. This combination used to make `gen_smt_vcs_boole` mis-bind |
…rata quicksort.lean and similar Boole programs (a caller `modifies` an array global and calls a callee that both `modifies` that same array and takes a plain `int` parameter referenced in its own `ensures`) crashed `gen_smt_vcs_boole` with a hard type error: the callee's `int` formal got bound to the caller's array argument instead. Root cause: `CallArg.replaceInArgs` (Strata's Core/Statement.lean) rewrites a call's argument list with type-checked expressions by walking the arg list and consuming one resolved expression per `.inArg`. But `getInputExprs` (which produced those resolved expressions) emits one expression per `.inArg` *and* per `.inoutArg`, since modifies-globals are threaded through as `.inoutArg`. `replaceInArgs` skipped over `.inoutArg` without consuming its slot, so every argument after the first modifies global got shifted by one position. This was already fixed upstream (strata-org/Strata commit 0de296da) as part of an unrelated typechecker-soundness proof, but Strata-Boole's pinned revision predated it by about an hour. Bumping the pin to current `origin/main` pulls in a month of otherwise-unrelated churn, most notably: `Option MetadataAnn` replacing the single-purpose `ReachCheck` category and being threaded onto most Core DDM statement/command ops (arity shift at ~25 call sites in Verify.lean), and three operator tokens renamed off the identifier-collision path (`>>s`->`ashr`, `<s/<=s/>s/>=s`->`slt/sle/sgt/sge`) which broke `bitvector_ops.lean`'s literal syntax. Both are fixed here; `stack_array_based.lean`'s `#guard_msgs` output is regenerated for the resulting label-numbering drift. Adds quicksort.lean as a permanent regression test for the modifies-array + call-site scenario, fully proved (no `sorry`).
kondylidou
force-pushed
the
fix/partition-modifies-global-threading
branch
from
July 21, 2026 20:24
8aed202 to
bae1d9d
Compare
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
gen_smt_vcs_boolecrashed with a hard type error on any Boole programwhere a caller
modifiesan array-typed global and calls a callee thatalso
modifiesthat global and takes a plainintparameter referencedin its own
ensuresclause (e.g.Quicksort/Partition). The callee'sintformal was getting bound to the caller's array argument instead ofthe actual
intargument, producing errors like:Root cause
CallArg.replaceInArgs(Strata'sCore/Statement.lean) rewrites a call'sargument list with type-checked expressions by walking it and consuming
one resolved expression per
.inArg. ButgetInputExprs— which producedthose resolved expressions — emits one expression per
.inArgand per.inoutArg(modifies-globals are threaded through as.inoutArg).replaceInArgssilently skipped.inoutArgwithout consuming its slot,so every argument after the first modifies-global shifted one position.
This was already fixed upstream (
strata-org/Strata@0de296da) as a sideeffect of an unrelated typechecker-soundness proof
Changes
Stratarevision to currentorigin/main, which pullsin the upstream fix.
broke this repo — both fixed here:
Option MetadataAnn(replacing the old single-purposeReachCheckcategory) got threaded onto most Core DDM statement/command ops.
Updated ~25 affected pattern matches in
StrataBoole/Verify.lean.identifier-collision path (
>>s→ashr,<s/<=s/>s/>=s→slt/sle/sgt/sge). Updatedbitvector_ops.lean.stack_array_based.lean's#guard_msgsoutput forincidental obligation-label renumbering from the version bump.
quicksort.lean: a permanent, fully-proved (nosorry)regression test for the modifies-array + call-site scenario.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.