Introduce condition mode to simplify modifiesClauses#1406
Closed
keyboardDrummer wants to merge 17 commits into
Closed
Introduce condition mode to simplify modifiesClauses#1406keyboardDrummer wants to merge 17 commits into
keyboardDrummer wants to merge 17 commits into
Conversation
## Summary - Periodic merge of `main` into `main2` to keep main2 up to date with core improvements - 46 new commits from main since PR #1346 (mostly repo-removal PRs: #1339, #1351, #1343, #1329, #1334, plus code changes) - All conflicts resolved by keeping main2's versions (sub-repos stay local, no module migration, preserves main2-only features like Procedure.Body sum type, transparent procs, array axiomatization) - Fixed duplicate StrataDDM git entries that auto-merged into `docs/api/lake-manifest.json` and `docs/verso/lake-manifest.json` --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com> Co-authored-by: Michael Tautschnig <mt@debian.org> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com> Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com> Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com> Co-authored-by: thanhnguyen-aws <ntson@amazon.com> Co-authored-by: Fabio Madge <fmadge@amazon.com> Co-authored-by: Joe Hendrix <joehx@amazon.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: June Lee <lebjuney@amazon.com> Co-authored-by: David Deng <daviddenghaotian@gmail.com> Co-authored-by: David Deng <htd@amazon.com> Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> Co-authored-by: Mikael Mayer <mimayere@amazon.com> Co-authored-by: Remy Willems <rwillems@amazon.com> Co-authored-by: keyboardDrummer-bot <keyboarddrummer.bot@gmail.com> Co-authored-by: Sagar Joshi <72283186+sagjoshi@users.noreply.github.com>
Each `LaurelPass.run` now receives `LaurelTranslateOptions`, instead of passes being parameterized at construction. `LaurelTranslateOptions` moves into `LaurelPass`, the pipeline threads the options into every pass, and the `comesBefore` lists no longer carry an arbitrary placeholder argument. No behavioural change: every pass ignores the new argument here.
Under `--use-array-theory` the heap `Map` is an SMT array, so for a `modifies` clause naming only individual references we can emit an enumerated, quantifier-free frame (`buildEnumeratedFrame`: overwrite the named rows) instead of the `∀`-based `buildPointwiseFrame`. The dispatch (`onlyIndividualRefs`) is restricted to bodiless procedures: a body that allocates cannot prove the whole-array equality, so bodies keep the pointwise frame, whose `< nextReference` guard tolerates allocation.
Structural #guards that the enumerated frame is quantifier-free while the pointwise frame is not (ModifiesFrameQuantifierFreeTest), the array-theory path including allocating bodies (T2c), and a perf/completeness regression for a chained spec procedure (T2e).
…laurel-modifies-array-theory
For an individual-ref modifies clause under array theory, callers now assume the quantifier-free enumerated frame as a free ensures, while the body proves the allocation-tolerant pointwise frame via asserts inserted before every exit, so callers never assume the quantifier. This drops the bodiless-only restriction: allocating bodies and writes-via-calls verify, and illegal writes are still rejected.
Merge reviewed-kbd-will-merge-to-main into PR1374-kiro. Resolution kept the reviewed branch's generic LaurelPass/PassMeta pass framework, but threads the LaurelTranslateOptions argument as the first parameter of each pass's run (options-first), per review preference. Preserved the PR's enumeratedModifiesClauses option and its threading through modifiesClausesTransformPass. Dropped the PR's now-superseded translateInvokeOnAxiom (invokeOn-axiom generation is handled by ContractPass on the reviewed branch). Also documents that enumeratedModifiesClauses has no effect when the procedure's modifies clause contains sets.
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
4 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.
Built on top of #1374. Will take out of draft when that merges.