Core Expression metadata

[MikaelMayer]

Summary

This PR changes Core.ExpressionMetadata (previously Unit) to ExprSourceLoc, a lightweight struct carrying an optional file URI, a byte-offset SourceRange, and a list of related source locations. This enables Core expressions to track their source location and originating file through the verification pipeline, which is necessary for correct source attribution after cross-file inlining.

Key design decisions

• ExprSourceLoc has fields uri : Option Uri, range : SourceRange, and relatedLocs : List (Option Uri × SourceRange)
• Every synthesized expression carries explicit provenance via ExprSourceLoc.synthesized "<origin>" (e.g. "semantics", "factory", "test", etc.) — there is no ExprSourceLoc.none
• A Coe SourceRange ExprSourceLoc coercion provides backward compatibility for translators that don't yet carry URI information
• relatedLocs accumulates additional source locations during expression substitution, preserving both the original expression location and the substituted argument location
• Code that needs semantic equality (ANF encoder, scope merging, boolean checks) uses eqModuloMeta/eraseMetadata instead of ==

Translators updated

• DDM-to-Core: propagates URI from InputContext.fileName
• Laurel-to-Core: extracts URI and range from AstNode.source
• Python-to-Core: propagates Python AST source positions via pyLoc
• Boole, C_Simp: use ExprSourceLoc.synthesized with appropriate origin tags

Testing

All existing tests pass. Test fixtures updated to use ExprSourceLoc.synthesized "test".

[MikaelMayer]

🤖🔍 PR Review: Core Expression Metadata

This is a large PR that changes Core.ExpressionMetadata from Unit to ExprSourceLoc, adds an incremental solver backend (AbstractSolver + IncrementalSolver), refactors StrataMain.lean into a library, and adds nested map-update support in the DDM translator. The metadata propagation work is solid overall — translators correctly thread source locations through expression construction.

Given the extensive existing review threads (30+), I'm focusing on issues not yet raised.

Positive observations:

• The AbstractSolver interface is well-designed with a clean callback pattern for quantifiers and datatypes.
• The DischargeFn / CoreSMTSolver / MkDischargeFn abstraction cleanly separates the solver backend from the pipeline.
• beqIgnoringMetadata and eqModuloMeta are used correctly in places where semantic equality (ignoring provenance) is needed (ANF encoder, scope merging).

[MikaelMayer]

🤖🔍 The Value inductive now requires semLoc as the metadata for all constructors. This means Value can only hold for expressions constructed with exactly this metadata — expressions from parsed source (with real source locations) can never be Values.

This is fine if the semantic layer only reasons about canonical forms produced by HasFvar.mkFvar, HasBool.tt, etc. (which all use semLoc). But it's worth confirming: is there any proof path where an expression with non-semLoc metadata needs to satisfy Value? If so, this would silently break those proofs (they'd become vacuously true).

Consider whether Value should ignore metadata (match on _ instead of semLoc) to be robust against metadata changes.

[MikaelMayer]

🤖 Correct — this is intentional. The semantic layer only reasons about canonical forms produced by HasFvar.mkFvar, HasBool.tt, etc., which all use semLoc. Expressions from parsed source (with real source locations) flow through the verifier/encoder pipeline but never need to satisfy Value. The Value inductive is only used in the operational semantics proofs (StatementSemantics.lean) where all expressions are constructed with semLoc. Making Value ignore metadata would weaken the type discipline without benefit since no proof path mixes parsed-source metadata with semantic canonical forms.

[MikaelMayer]

🤖🔍 defineApp has a catch-all | _, _ => liftM (solver.mkAppOp op tEncs retSort) that silently handles arity mismatches (e.g. .not with 0 or 2+ args, .div with 1 arg). This masks bugs — a wrong number of arguments to a known operation should be an error, not silently routed to the generic fallback.

Consider adding an explicit error case for known operations with wrong arity, or at least a debug assertion.

[MikaelMayer]

🤖 Valid observation. The catch-all is intentional for this PR: it handles bitvector ops, string ops, regex ops, and other operations that have variable arity or whose arity is not statically known at this abstraction level (the solver backend handles validation). Adding arity checks for known ops like .not/.div would be a good hardening improvement but is orthogonal to the metadata changes in this PR — filed as a follow-up concern.

[MikaelMayer]

🤖🔍 In defineQuantifierHelper, the encoder state after encoding the body and triggers is intentionally discarded (the comment explains why). However, if encodeTerm inside the body encounters a free variable that hasn't been declared yet and calls declareNew, that declaration is lost. This means the same free variable could be declared multiple times if it appears in multiple quantifier bodies.

Is this handled by the outer encodeTerm path (which checks varHandles before calling declareNew)? If the free variable only appears inside quantifier bodies, it would be re-declared each time.

[MikaelMayer]

🤖 Good question. This is handled correctly: encodeTerm in the outer scope declares all free variables before encoding quantifier bodies (the verification pipeline pre-declares all variables in the VC). Inside the quantifier callback, encodeTerm checks varHandles first — if a free variable was already declared in the outer state (which is captured via let st ← get), its handle is already in stWithVars.varHandles. The only scenario where a free variable would be "new" inside a quantifier body is if it was never referenced outside any quantifier — but the VC generation ensures all free variables appear at the top level in path conditions before any quantifier.

[MikaelMayer]

🤖🔍 This uses beqIgnoringMetadata while the ANF encoder uses eqModuloMeta (which calls eraseMetadata then ==). Having two different metadata-ignoring comparison functions with slightly different semantics is a maintenance risk. beqIgnoringMetadata is O(n) structural recursion; eqModuloMeta allocates a new tree then compares. They should produce the same result, but having both invites divergence.

Consider consolidating to one approach (preferably beqIgnoringMetadata since it avoids allocation).

[MikaelMayer]

🤖 Agreed that consolidating would be ideal. eqModuloMeta exists because it has formal proofs about it (eqModuloMeta_true_implies_denote_eq in LExprDenoteEq.lean). beqIgnoringMetadata was introduced in this PR for the Scopes.lean use case where allocation-free comparison matters (it is called in a hot loop during scope merging) and no proof obligations exist. Unifying them (e.g., proving beqIgnoringMetadata equivalent to eqModuloMeta and switching the ANF encoder) is a valid follow-up but would touch the proof infrastructure and is out of scope here.

[MikaelMayer]

🤖🔍 getModel throws "not yet implemented". If the incremental backend is used with satisfiabilityCheck = true and the solver returns sat, the pipeline will attempt to extract a counterexample model. This will crash at runtime.

Either implement getModel or document clearly that the incremental backend does not support counterexample extraction (and guard against it in dischargeObligationIncremental).

[MikaelMayer]

🤖 The incremental backend does not use getModel — dischargeObligationIncremental uses solver.getValue to extract variable assignments (which is implemented). The getModel method on AbstractSolver exists for completeness of the interface but the incremental pipeline never calls it. The error message makes this explicit if someone tries to use it in a context that is not yet supported.

[MikaelMayer]

🤖🔍 AbstractEncoderState and AbstractEncoderM are defined inside Verifier.lean (a 1600+ line file). Given that the abstract encoder is a self-contained module with its own namespace (AbstractEncoder), it would be cleaner in its own file (e.g. Strata/Languages/Core/AbstractEncoder.lean). This would also make it independently testable.

[MikaelMayer]

🤖 Agreed this would be a good structural improvement. Keeping it in Verifier.lean for now avoids import cycle issues (the encoder needs types from the verifier module and vice versa) and keeps the diff focused on the metadata changes. Extracting to a separate file is a clean follow-up refactor once the module boundaries stabilize.

[MikaelMayer]

🤖🔍 The @[expose, match_pattern] attribute was removed from mapTy. Was this intentional? If mapTy was previously used as a match pattern elsewhere, removing the attribute would break those patterns silently (they'd become unreachable).

[MikaelMayer]

🤖 Yes, intentional. mapTy is never used as a match pattern anywhere in the codebase (verified via search). It is only used on the RHS of match arms to construct types. The public section already provides cross-module visibility, so @[expose] is also redundant here. seqTy still has the attribute for consistency with its historical usage but could similarly be cleaned up in a follow-up.