Skip to content

Infrastructure changes from PR 385#426

Merged
keyboardDrummer merged 1 commit intomainfrom
remy/infraChangesFrom385
Feb 26, 2026
Merged

Infrastructure changes from PR 385#426
keyboardDrummer merged 1 commit intomainfrom
remy/infraChangesFrom385

Conversation

@keyboardDrummer
Copy link
Contributor

@keyboardDrummer keyboardDrummer commented Feb 16, 2026 •
edited by fabiomadge
Loading

Contains a subset of the changes from #385, rebased on current main.

DDM Infrastructure

  • Add NewlineSepBy separator and SyntaxDef.passthrough variant
  • Replace fromIonName?/toIonName with fromCategoryName? for category-based lookup
  • Add newline formatting case in ArgF.mformatM
  • Update Java/Lean codegen for new constructs
  • Comment parsing fix in Parser.lean

Lambda/SMT Bug Fixes

  • Add liftBVars with cutoff parameter for correct de Bruijn index shifting
  • Add substFvarLifting/substFvarsLifting for substitution under binders (doc comment clarifies that to's bvars must refer to binders outside e)
  • Fix multi-argument function SMT encoding (was hardcoded to unary)
  • Add Map type to SMT Array encoding

Testing

  • LExprWFTests.lean: tests for substFvarLifting
  • SMTEncoderTests.lean: updated for multi-arg encoding
  • Functions.lean: multi-argument function test + quantifier-in-body test

Review feedback addressed

  • The ≤ → < precedence change from the previous version has been removed (it was incorrect)
  • Doc comment added to substFvarLifting per review feedback

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@keyboardDrummer keyboardDrummer requested a review from a team as a code owner February 16, 2026 10:20
@keyboardDrummer keyboardDrummer mentioned this pull request Feb 16, 2026
Merged
joehendrix
joehendrix reviewed Feb 16, 2026
View reviewed changes
joehendrix
joehendrix reviewed Feb 16, 2026
View reviewed changes
joehendrix
joehendrix requested changes Feb 16, 2026
View reviewed changes
Copy link
Contributor

@joehendrix joehendrix left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR bundles infrastructure improvements including a new NewlineSepBy separator, SMT encoding fixes for multi-argument functions and Map types, and a substFvarLifting utility for de Bruijn index handling.

Two issues were found (the second is minor):

  • Precedence bug in Format.lean:321: Changing ≤ to < drops parentheses needed to preserve same-precedence grouping and non-default associativity — e.g., (true ==> false) ==> true formats as true ==> false ==> true, which parses as a different proposition.
  • substFvarLifting limitation in LExprWF.lean:334: The liftBVars call uses default cutoff 0, which incorrectly shifts bvars in the replacement term that refer to binders shared with the target expression; the current SMT encoder call site is safe but the restriction should be documented or addressed with a cutoff parameter.

aqjune-aws
aqjune-aws reviewed Feb 16, 2026
View reviewed changes
@keyboardDrummer
Copy link
Contributor Author

keyboardDrummer commented Feb 17, 2026

Leaving the comments for @fabiomadge since I extracted this code from his PR.

@fabiomadge fabiomadge force-pushed the remy/infraChangesFrom385 branch from cc88a4c to 54897c3 Compare February 25, 2026 03:02
@fabiomadge fabiomadge mentioned this pull request Feb 25, 2026
Merged
@fabiomadge fabiomadge force-pushed the remy/infraChangesFrom385 branch 2 times, most recently from 9b0e6d0 to a179ab3 Compare February 25, 2026 04:26
@fabiomadge
Copy link
Contributor

fabiomadge commented Feb 25, 2026 •
edited
Loading

Rebased on current main and addressed all review feedback:

  • Precedence bug (Format.lean): The ≤ → < change has been removed. The new branch was built from jverify-strata-backend which never had this change.
  • substFvarLifting doc (LExprWF.lean): Added a doc comment clarifying that to's bvars must refer to binders outside e, not within it.
  • Map encoding (SMTEncoder.lean): The hardcoded Map → Array in lMonoTyToSMTString and DL/SMT/Encoder.lean have been removed. On main, Map types work as uninterpreted sorts and the Laurel heap tests pass without Array theory. Map/Array encoding changes will come in with the Laurel feature PRs where they're needed.
  • panic! on bvars in substFvarsLifting: Not added — the only call site (SMTEncoder) intentionally passes bvars as substitution targets. The doc comment documents the contract instead.
  • DDM grammar spacing changes: Dropped (stale against current main). Can be a separate follow-up.

Tests added: LExprWFTests.lean (substFvarLifting), Functions.lean (multi-arg functions + quantifier-in-body).

Current state: 20 files, 394 insertions. All 406 tests pass.

@fabiomadge
DDM infrastructure + Lambda/SMT bug fixes
76ba04f 
DDM changes:
- Add NewlineSepBy separator and SyntaxDef.passthrough variant
- Replace fromIonName?/toIonName with fromCategoryName? for category-based lookup
- Add newline formatting case in ArgF.mformatM
- Update Java/Lean codegen for new constructs
- Comment parsing fix in Parser.lean

Lambda/SMT changes:
- Add liftBVars with cutoff parameter for correct de Bruijn index shifting
- Add substFvarLifting/substFvarsLifting for substitution under binders
- Fix multi-argument function SMT encoding (was hardcoded to unary)
- Add Map type to SMT Array encoding

Note: Laurel tests will fail until the Laurel grammar is updated to match
the new DDM SyntaxDef structure (done in the follow-up Laurel API PR).
@fabiomadge fabiomadge force-pushed the remy/infraChangesFrom385 branch from a179ab3 to 76ba04f Compare February 25, 2026 05:03
joehendrix
joehendrix approved these changes Feb 26, 2026
View reviewed changes
Copy link
Contributor

@joehendrix joehendrix left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me.

@keyboardDrummer keyboardDrummer added this pull request to the merge queue Feb 26, 2026
Merged via the queue into main with commit f0dad81 Feb 26, 2026
15 checks passed
@keyboardDrummer keyboardDrummer deleted the remy/infraChangesFrom385 branch February 26, 2026 18:03
github-merge-queue bot pushed a commit that referenced this pull request Feb 26, 2026
@fabiomadge @andrewmwells-amazon
Laurel API: precondition → preconditions, postcondition → postconditi…
2341cf8 
…ons (#481)

Part of the incremental split of #385. Can be merged independently of
#426.

### Changes

Converts Laurel's `Procedure` from a single precondition to a list of
preconditions, and `Body.Abstract` from a single postcondition to a
list. This enables multiple `requires`/`ensures` clauses per procedure,
which is needed by the upcoming constrained types and contract features.

**Laurel.lean:**
- `precondition : WithMetadata StmtExpr` → `preconditions : List
(WithMetadata StmtExpr)`
- `Body.Abstract postcondition` → `Body.Abstract (postconditions : List
...)`
- `Body.Opaque postcondition` → `Body.Opaque postconditions` (name only,
already a list)
- Reorder `Parameter` struct, add `Repr` instances

**Adapted callers:**
- `ConcreteToAbstractTreeTranslator` — parse `Option OptionalRequires`
into list
- `LaurelToCoreTranslator` — iterate over preconditions list, generate
indexed labels for multiple preconditions
- `HeapParameterization` — fold over preconditions/postconditions lists
- `LaurelFormat` — format preconditions/postconditions lists, relocate
`formatDeterminism`
- `PythonToLaurel`, `Specs/ToLaurel` — adapt to new field names

**LiftExpressionAssignments.lean:**
- Process block-in-expression non-last elements left-to-right via
`transformStmt` instead of right-to-left via `transformExprDiscarded`
- Remove now-unused `transformExprDiscarded`

### Testing

All existing Laurel, Python, and Core tests pass. No new tests needed —
this is a structural refactor with no new features.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fabiomadge fabiomadge fabiomadge left review comments

@joehendrix joehendrix joehendrix approved these changes

@aqjune-aws aqjune-aws aqjune-aws approved these changes

@andrewmwells-amazon andrewmwells-amazon Awaiting requested review from andrewmwells-amazon

Assignees

@fabiomadge fabiomadge

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@keyboardDrummer @fabiomadge @joehendrix @aqjune-aws