Laurel: avoid quantified modifies frames when using array theory by julesmt · Pull Request #1374 · strata-org/Strata

julesmt · 2026-06-16T01:13:40Z

Under --use-array-theory, a modifies clause naming only individual object
references is now encoded as a single quantifier-free heap equation instead of
a ∀-quantified frame, so the solver discharges it by array rewriting instead of
instantiating a quantifier per object/field.

∀ obj, fld. obj ≠ c ⇒ readField(old,obj,fld) == readField(new,obj,fld)   -- before
data(new) == store(data(old), c, select(data(new), c))                   -- now

The ∀ frame is unchanged for set-valued/empty modifies and when array theory is
off, so default behavior is untouched.

## 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>

keyboardDrummer · 2026-06-16T08:15:52Z

I found the term "array-theory" in this PR misleading because the PR does not directly use any SMT array theory. Instead, the PR relies on Core Map's which are not necessarily implemented using SMT array theory. In fact, I think Core is or at least was not using array theory for their maps, simply because it is or was not implemented yet.

keyboardDrummer

Very cool!

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).

keyboardDrummer · 2026-06-22T13:41:03Z

@keyboardDrummer-bot please resolve merge conflicts

…laurel-modifies-array-theory

keyboardDrummer · 2026-06-22T15:53:54Z

How come you can't make the enumerated encoding work with procedures that have a body? Suppose I have:

composite C { var x: int }
procedure creator() returns (c: C)
  ensures c#x == 3
  ensures fresh(c)
  modifies {}
  opaque
{
  c := new C;
  c#x := 3;
}

then that would translate to something like:

procedure creator() returns (c: C)
// c#x == 3
  ensures read($heap, c, C.x) == 3 
  
// fresh(c)
  ensures c.ref >= old($heap).nextRef

// modifies {}, enumerated encoding
  ensures $heap.data == old($heap).data 

// implicit postcondition stating that every output object is allocated in the new heap
  ensures c.ref < $heap.nextRef

which has the curious implication that read(old($heap), c, C.x) == 3, so the old heap contains data for an object that did not yet exist at the time of the old heap. However, I think that might not cause any issues. What issues did you run into?

julesmt · 2026-06-22T19:26:33Z

Yeah, I had pretty much the same example.
data == old data fails because the body writes the fresh row, even though fresh objects shouldn't count for modifies.

The pointwise frame dodges this with the obj < nextReference($heap_in) guard, which I can't keep without a quantifier, so I this is why I wanted to restrict the enumerated frame to bodiless procedures.

However to get it for bodies too, I split the jobs: callers assume the enumerated frame, and the body is checked separately by asserting the pointwise frame at every exit.

what do you think (see next commit) ? @keyboardDrummer

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.

keyboardDrummer · 2026-06-23T08:11:11Z

However to get it for bodies too, I split the jobs: callers assume the enumerated frame, and the body is checked separately by asserting the pointwise frame at every exit.
what do you think (see next commit) ? @keyboardDrummer

Brilliant!

…lauses

… frame

keyboardDrummer · 2026-06-23T18:38:46Z

This will have a few merge conflicts after #1352 merges. I'll try to resolve these before you get to it @julesmt

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.

fabiomadge

Independent soundness pass (built at 5caabd852, suite green). Sound: callers assume the enumerated frame (free) while the body proves only pointwise; enumerated is abstractly stronger (constrains unallocated rows) but the gap is confined to fresh objects the caller never observed (opaque refs + monotone, never-reused nextReference) — imprecision, not a derivable falsehood. Verified: unmodified objects preserved, modified ones not over-preserved, wildcard effects still propagate into a caller's frame.

One non-blocking note — loop + early return rejects legal code. A body writing only its framed object then returning inside a loop fails (modifies clause does not hold); the loopless analog verifies — the loop lacks a heap-frame invariant to discharge the old() assert. Sound, just imprecise.

kadirayk

IIUC body proves the quantified frame, callers assume the enumerated (quantifier-free) frame, which should be faster. The default case is untouched. Tests seem to cover the changes and tricky paths. LGTM!

julesmt requested a review from a team as a code owner June 16, 2026 01:13

github-actions Bot added Waiting-For-Review Laurel labels Jun 16, 2026

julesmt requested review from keyboardDrummer and stefanzetzsche June 16, 2026 01:16

keyboardDrummer reviewed Jun 16, 2026

View reviewed changes

Comment thread Strata/Languages/Laurel/HeapParameterization.lean Outdated

Comment thread Strata/Languages/Laurel/ModifiesClauses.lean Outdated

Comment thread Strata/Languages/Laurel/ModifiesClauses.lean

Comment thread Strata/Languages/Laurel/ModifiesClauses.lean Outdated

julesmt mentioned this pull request Jun 18, 2026

Laurel: allow modifies clauses to specify new field values #1388

Open

julesmt added 3 commits June 19, 2026 15:51

julesmt force-pushed the julesmt/features/laurel-modifies-array-theory branch from bf25905 to d5ece2c Compare June 19, 2026 22:59

julesmt requested review from fabiomadge and keyboardDrummer June 19, 2026 23:00

keyboardDrummer mentioned this pull request Jun 22, 2026

fix(laurel): synthesizing heap well-formedness conditions in HeapParameterization #1396

Closed

keyboardDrummer changed the base branch from main2 to reviewed-kbd-will-merge-to-main June 22, 2026 13:40

Merge branch 'reviewed-kbd-will-merge-to-main' into julesmt/features/…

21fa8f9

…laurel-modifies-array-theory

keyboardDrummer enabled auto-merge June 22, 2026 14:29

keyboardDrummer reviewed Jun 23, 2026

View reviewed changes

julesmt added 5 commits June 23, 2026 09:41

Laurel: scope pointwise frame to its usage branch

a826a38

Laurel: rename translate option useArrayTheory to enumeratedModifiesC…

e327cb5

…lauses

Laurel: document that set-valued modifies clauses keep the quantified…

debf7fe

… frame

Laurel: rename buildPointwiseFrame to buildQuantifiedFrame

2d04b8f

Laurel: drop redundant useEnumeratedFrame defaults in helpers

622f60c

julesmt requested a review from keyboardDrummer June 23, 2026 17:43

keyboardDrummer reviewed Jun 23, 2026

View reviewed changes

Comment thread Strata/Languages/Laurel/LaurelPass.lean

julesmt changed the title ~~Laurel: quantifier-free modifies frame under --use-array-theory~~ Laurel: avoid quantified modifies frames when using array theory Jun 23, 2026

julesmt force-pushed the julesmt/features/laurel-modifies-array-theory branch from cc440f0 to 5caabd8 Compare June 23, 2026 20:42

keyboardDrummer approved these changes Jun 24, 2026

View reviewed changes

github-actions Bot added Has 1 approval and removed Waiting-For-Review labels Jun 24, 2026

keyboardDrummer reviewed Jun 24, 2026

View reviewed changes

Comment thread Strata/Languages/Laurel/ModifiesClauses.lean

github-actions Bot added Waiting-For-Review and removed Has 1 approval labels Jun 24, 2026

keyboardDrummer mentioned this pull request Jun 25, 2026

Introduce condition mode to simplify modifiesClauses #1406

Closed

fabiomadge reviewed Jun 25, 2026

View reviewed changes

fabiomadge approved these changes Jun 25, 2026

View reviewed changes

github-actions Bot added Has 1 approval and removed Waiting-For-Review labels Jun 25, 2026

kadirayk approved these changes Jun 25, 2026

View reviewed changes

github-actions Bot removed the Has 1 approval label Jun 25, 2026

keyboardDrummer added this pull request to the merge queue Jun 25, 2026

Merged via the queue into reviewed-kbd-will-merge-to-main with commit 0a4a29b Jun 25, 2026
21 checks passed

keyboardDrummer deleted the julesmt/features/laurel-modifies-array-theory branch June 25, 2026 13:46

Uh oh!

Conversation

julesmt commented Jun 16, 2026

Uh oh!

keyboardDrummer commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

keyboardDrummer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

keyboardDrummer commented Jun 22, 2026

Uh oh!

keyboardDrummer commented Jun 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

julesmt commented Jun 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

keyboardDrummer commented Jun 23, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

keyboardDrummer commented Jun 23, 2026

Uh oh!

Uh oh!

Uh oh!

fabiomadge left a comment

Choose a reason for hiding this comment

Uh oh!

kadirayk left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

keyboardDrummer commented Jun 16, 2026 •

edited

Loading

keyboardDrummer commented Jun 22, 2026 •

edited

Loading

julesmt commented Jun 22, 2026 •

edited

Loading