fix(verify): correct modifies-array call-site argument binding - #7
Closed
kondylidou wants to merge 5 commits into
Closed
fix(verify): correct modifies-array call-site argument binding#7kondylidou wants to merge 5 commits into
kondylidou wants to merge 5 commits 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
Collaborator
Author
|
@joscoh can this be merged now? |
joscoh
previously approved these changes
Aug 18, 2026
| private def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement := do | ||
| match s with | ||
| | .varStatement m ds => | ||
| | .varStatement m _annots ds => |
Contributor
There was a problem hiding this comment.
Not blocking, but slightly better to use an underscore if the variable is unused IMO
The Boole grammar elaboration via #strata_gen recurses more deeply on x86-64 than on ARM64 due to larger native stack frames; the Lean runtime aborts with "Stack overflow detected" at the default 8 MB task stack. Set weakLeanArgs = ["--tstack=32768"] (32 MB) as recommended by the runtime's own error hint. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
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 program where acaller modifies an array-typed global and calls a callee that also modifies that
global and takes a plain
intparameter referenced in its ownensuresclause(e.g. Quicksort/Partition). The callee's
intformal was getting bound to thecaller's array argument instead of the actual
intargument:Application type mismatch: «A@1» has type SmtArray Int Int
but is expected to have type Int in GE.ge «A@1»
Root cause:
CallArg.replaceInArgs(Strata'sCore/Statement.lean) rewrites acall's argument list by consuming one resolved expression per
.inArg. ButgetInputExprsemits one expression per.inArgand per.inoutArg(modifies-globals are threaded as
.inoutArg).replaceInArgsskipped.inoutArgwithout consuming its slot, so every argument after the first modifies-global
shifted by one position.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.