Fix #653 and other bugs with iterated substitution (#716)

*Issue #, if available:* #653

*Description of changes:* The use of `substFvars` for repeated
substitution is unsound whenever either (a) the substituted expressions
are not guaranteed to use only `fvars` that do not appear in the
substitution list or (b) the substituted expressions contain bound
variables. This PR instead adds simulatenous substitution operators that
safely substitute multiple free variables at once, with both `bvar`-safe
and standard versions. It classifies each place where iterated
substitution was used as safe or requiring one of the new functions,
adding an appropriate comment for each to make the assumptions explicit
(for example, for some cases, the substituted terms are closed, so it
safe to use a non-lifting substitution function).
It includes tests that formerly failed illustrating soundness issues
with the prior approach: for the Lambda partial evaluator, for
`substFvarsFromState`, for the precondition generation, closure capture,
and procedure call capture.


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: Josh Cohen <cohenjo@amazon.com>

Fix bug in handling of blocks that occur in expresssions (#672)

### Changes
- Fix bug in handling of blocks that occur in expressions. The heart of
the problem was that `transformStmt`, which does not update the
substitution map, was being called from inside `transformExpr` when it
was handling a block, leading to missing substitutions. A second but
smaller bug was a statement ordering bug that occurred when handling
calls.

### Testing
- Added test-case


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: Josh Cohen <36058610+joscoh@users.noreply.github.com>

Add exhaustive tracking for Python class methods (#698)

Add `exhaustive` tracking for Python class methods.

Add `@exhaustive` decorator for pyspec classes.

The current settings are:

- User-defined classes: always exhaustive
- Pyspec classes: exhaustive controlled by ClassDef.exhaustive field
(defaults to false; models should aim for `true`)
- Types from annotations only: not exhaustive, unmodeled methods become
Hole
- Primitives (str, int, bool): not exhaustive, methods like
lower()/startswith() become Hole



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

Use globally unique bound variable names in SMT encoding (#681)

## Summary
- Always generate `$__bv{N}` names for quantifier-bound variables
instead of reusing user-provided names
- This guarantees globally unique bound variable names across all
quantifiers.

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

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Pass source metadata to subexpressions in Python/Specs/ToLaurel (#663)

Pass source metadata to subexpressions in Python/Specs/ToLaurel


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: Juneyoung Lee <lebjuney@amazon.com>
Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>

Add support for IfExpr in Python->Laurel translation (#649)

*Description of changes:* This PR adds support for IfExpr in
Python->Laurel translation.


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

feat(SMT): avoid redundant reset, globally unique quantified var name…

…s, more smtReservedKeywords (#632)

This pull request adds a few more syntactic constraints to SMT generated
code for supporting internal benchmarks.
* Removes redundant `(reset)` calls (to make it consistent, this was
applied not only to Core pipeline but also B3 pipeline)
* To avoid `$__bvN` quantified variables having duplicated names across
different formula (which is a valid SMT in general but more tailored for
internal use case) this adds `bvCounter` to `SMT.Context`.
* Adds more predefined theory symbols to `smtReservedKeywords`.
* To avoid an unfortunate case where "tN" and "fN" may overlap with
user-defined Sort, add `$__` to their prefixes.

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: Shilpi Goel <shigoel@gmail.com>

Add collectTypeRefs for TCore (#630)

*Description of changes:* This PR adds collectTypeRefs for TCore, which
fix the bug of unrecognized dependency between Box and Any.
Thanks @keyboardDrummer.

This PR replaces #618


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

Change eq semantics for binders in Lambda (#633)

*Issue #, if available:*

*Description of changes:* Change semantics for equality to avoid
returning `false` when two lambda or quantifier bodies are syntactically
different, because this says nothing about whether or not they are
semantically distinct. For example, `\x.if true then 0 else 1` and
`\x.0` are syntactically different but semantically equal. This PR
changes the semantics so that equalities of terms containing binders
only reduce if they are syntactically equal; otherwise the semantics is
stuck.

Note that we will need to change the typing rules to prove progress,
since evaluation can now get stuck on well-typed terms. But we will have
to determine whether that involves a direct change to the typing rules,
a change to canonical values, etc and it should be finalized once the
type system is fully settled (it may change as a result of the future
denotational semantics).


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: Josh Cohen <cohenjo@amazon.com>

Eliminate Python dependency from CBMC pipeline (#576)

The CBMC backend relied on a Python post-processing step
(process_json.py) to merge a 4000-line defaults.json of built-in symbols
into the Lean-generated symbol table before passing it to symtab2gb.
This made the pipeline harder to maintain, required Python as a runtime
dependency, and kept critical symbol definitions outside of Lean where
they could not benefit from type checking.

*Description of changes:*

Generate all 38 CBMC built-in symbols directly in Lean
(DefaultSymbols.lean), parameterized by ArchConfig and module name, and
emit the symbol table in the {"symbolTable": ...} wrapper that symtab2gb
expects. This turns the pipeline into a simple two-step flow (strata →
symtab2gb) with no Python intermediary.

Remove the now-unused Python scripts (process_json.py, defaults.py),
defaults.json, and legacy shell wrappers (run_strata_cbmc.sh,
compare_cbmc_json.sh). Update all pipeline scripts and documentation to
reflect the simplified flow.

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: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>