SMT encoding errors in #1197

[atomb]

PR #1197 fails CI with some SMT encoding errors. I asked Kiro for a diagnosis, and got the following.

Root Cause

The error 🚨 SMT Encoding Error! Unimplemented encoding for type var $__ty7 occurs because the PrecondElim transformation generates precondition assertions for polymorphic Sequence operations (select, update, take, drop) without applying the type substitution from the call site.

The pipeline order is: PrecondElim → typeCheck → symbolicEval → SMT encoding.

When PrecondElim generates a bounds-check assertion for a call like Sequence.select(state_out, 0) where state_out : Sequence bv32:

1. It extracts the precondition from seqSelectFunc, which is defined with type variable %a (e.g., 0 <= i && i < Sequence.length(s) where Sequence.length has type Sequence %a → int)
2. It substitutes the value arguments (state_out for s, 0 for i) via substitutePrecondition
3. But it does not substitute the type variable %a with the concrete type bv32

The resulting assertion still contains %a in the type annotations of operators like Sequence.length. When the type checker processes this, it creates fresh type variables ($__ty7) but can't always resolve them to concrete types — especially when:

• The argument expression itself has a polymorphic type annotation (e.g., Sequence.empty with type Sequence %a)
• The call is inside a polymorphic function body (e.g., Seq_lib_insert<T>)

When the SMT encoder encounters the unresolved $__ty7, it fails because ctx.tySubst has no binding for it.

The Fix

The fix should be in Strata/DL/Lambda/Preconditions.lean, in the collectWFObligations function. After substituting value arguments into the precondition, it should also compute and apply the type substitution derived from the call site.

Specifically, in the callObligations branch where it processes a function call:

let callObligations := match Factory.callOfLFunc F e with
  | some (op, args, func) =>
    if func.preconditions.isEmpty then []
    else
      let md := e.metadata
      -- NEW: Compute type substitution from the call site
      let tySubst := func.computeTypeSubst op args |>.getD Subst.empty
      func.preconditions.map fun precond =>
        let substedPrecond := substitutePrecondition precond.expr func.inputs args
        -- NEW: Apply type substitution to resolve polymorphic type variables
        let substedPrecond := substedPrecond.applySubst tySubst
        { funcName := func.name.name
          obligation := wrapImplications implications substedPrecond
          callSiteMetadata := md
          precondMetadata := precond.md : WFObligation T }
  | none => []

The computeTypeSubst function already exists and handles both annotated operators (via opTypeSubst) and unannotated ones (via argument type matching). After type checking, the .op node at the call site will have a concrete type annotation (e.g., Sequence bv32 → int → bv32 for Sequence.select), so opTypeSubst will produce the correct substitution [%a → bv32].

However, there's a subtlety: PrecondElim runs before type checking, so the .op node might not have a fully instantiated type annotation yet. The computeTypeSubst fallback uses argument types (arg.typeOf), which also might not be available pre-type-checking.

This means the fix might need to be in a different place — either:

1. Move precondition type resolution to the type checker: After type checking resolves all type variables, have the type checker apply the resolved substitution to precondition assertions. This is complex.

2. Move PrecondElim to run after type checking (or add a post-type-check fixup pass): The comment in PrecondElim.lean says it must run before type checking "since in the presence of polymorphic preconditions, the resulting assertions have type variables that must be unified." But the current approach of relying on the type checker to resolve them isn't working for all cases.

3. Make the SMT encoder handle unresolved type variables gracefully: When encountering an unresolved type variable in a precondition obligation, treat it as an uninterpreted sort. This is the simplest fix but might produce weaker verification results.

4. Have PrecondElim use the callee's type annotation to derive the type substitution: Even before type checking, the callee .op node might have a type annotation from the parser/elaborator. If Sequence.select is called as Sequence.select(state_out, 0), the Boole translator might have set the type annotation on the Sequence.select operator to Sequence bv32 → int → bv32. In that case, opTypeSubst would work.

The most likely correct fix is option 4 — use LFunc.computeTypeSubst (which calls opTypeSubst) in collectWFObligations to derive the type substitution from the callee's type annotation, then apply it to the precondition. This works because:

• The Boole/Core parser typically annotates .op nodes with instantiated types
• opTypeSubst unifies the instantiated type against the generic type to get the substitution
• For cases where the annotation isn't available (pre-type-check), the fallback uses argument types

For the polymorphic function body case (Seq_lib_insert<T>), the type substitution would map %a → T (or %a → $__ty7 after type checking), which still leaves a type variable. For this case, the SMT encoder would need to handle it — either by treating the WF procedure's type parameters as uninterpreted sorts, or by not generating bounds-check obligations for calls within polymorphic function bodies (deferring them to concrete call sites).

Two Failing Tests

1. sha256_compact_indexed.lean — The #guard_msgs expected output doesn't include the new out-of-bounds access check obligations. The test needs its expected output updated, AND the SMT encoding error needs to be fixed.

2. seq_slicing.lean — Same issue: the seqOutOfBoundsSeed test's #guard_msgs doesn't account for the new bounds-check obligation that now appears (with the SMT encoding error).

Summary of Required Changes

1. Strata/DL/Lambda/Preconditions.lean — In collectWFObligations, apply the type substitution (from LFunc.computeTypeSubst) to the precondition expression after value substitution. This resolves type variables for concrete call sites.

2. Strata/Languages/Core/SMTEncoder.lean — For the polymorphic function body case (where type variables genuinely can't be resolved), either:

   • Treat unresolved type variables as uninterpreted sorts (add them to ctx.sorts and use a constr TermType), or
   • Skip encoding obligations that contain unresolved type variables (report as "unknown" rather than error)

3. Test files — After the fix, update the #guard_msgs expected output in both sha256_compact_indexed.lean and seq_slicing.lean to reflect the correct behavior (either the obligations pass, or they're reported differently).