fix(theorem): partial-eval constraint body before visiting (cross-submission capture)

[jsboige]

Summary

Fixes a crash in Theorem.AssertConstraints when the constraint lambda captures a local declared in a different .NET Interactive / Polyglot Notebooks submission.

Theorem.AssertConstraints now runs PartialEvaluator.PartialEval on each constraint body before ExpressionVisitor.Visit. This folds host-captured constants (locals declared outside the theorem parameter scope, e.g. in a different .NET Interactive submission or closure) into literal ConstantExpressions, sidestepping the reflective MemberExpression resolution in ExpressionVisitor.VisitMember that crashed across dynamic-assembly boundaries.

Bug

In .NET Interactive / Polyglot Notebooks, each cell compiles as a separate dynamic assembly (Submission#N). When a constraint lambda captures a local declared in another submission, VisitMember resolved the FieldInfo on the lambda submission type while the closure target carried the declaring submission type:

System.ArgumentException: Field 'b0' defined on type 'Submission#N' is
not a field on the target object of type 'Submission#M'

This was invisible in xUnit (single-assembly) because the closure and the field live in the same assembly there.

Repro (manual, .NET Interactive)

Two consecutive cells in a .NET Interactive notebook (Polyglot Notebooks):

// Cell 1 (submission #N)
var b = 5;          // local declared here

// Cell 2 (submission #M)
var t = Z3.Linq.Theorem.Z3;
var x = t.IntConst();
t.Assert(t.And(x >= 0, x <= b));   // captures `b` from cell 1
var s = t.Solve();                  // <-- crashes here

Before the fix, Solve() raised ArgumentException: Field 'b0' defined on type 'Submission#N' is not a field on the target object of type 'Submission#M'.

After the fix, Solve() returns the expected model x = 0.

Fix

Theorem.AssertConstraints now calls PartialEvaluator.PartialEval on each constraint body before handing it to ExpressionVisitor.Visit. The partial evaluator folds host-captured constants (locals declared outside the theorem parameter scope) into literal ConstantExpressions, so VisitMember is never asked to resolve them reflectively.

// before
foreach (var constraint in body)
//   constraint.Accept(this.ExpressionVisitor);

// after
foreach (var constraint in body)
{
    var partial = PartialEvaluator.PartialEval(constraint, ...);
    partial.Accept(this.ExpressionVisitor);
}

The fix is a no-op for same-assembly captures (PartialEval folds them to the same literal VisitMember would have produced via reflection), so all existing xUnit tests pass unchanged.

Subtrees referencing the theorem parameter (e.g. t.Values[i]) are preserved — they are not evaluable without a parameter binding and are left for the visitor to handle.

.gitignore

Adds .deploy/ to the ignore list — used by dotnet publish -o .deploy for the polyglot repro infrastructure.

Tests

This repository has no xUnit test infrastructure covering the cross-submission capture scenario (the bug is invisible there by construction — single-assembly), so no new test is included. The repro above is the canonical failing case and is exercised in the companion pedagogical repository (MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8b-Theorie-PAC-Lean.ipynb family + the standalone polyglot-repro/CrossSubmissionCaptureRepro.ipynb reproduction).

Notes

Cherry-picked from a downstream fork (MyIntelligenceAgency/Z3.Linq, branch fix/c805-fc44dfa-partial-eval-cross-submission). The companion reproduction notebook and downstream .csproj glue are intentionally not included in this PR — they belong in the downstream pedagogical repo, not here.

[HowardvanRooijen]

Very interesting - revisiting your suggestion in #29 has been on my backlog for a while - especially as we could leverage some agentic AI to help with any of the integration.

[jsboige]

Thanks Howard — read your note on #29 and the stack (congrats on the sweep, #110 looks like the right capstone). Three quick things on this PR:

Scope reframed beyond .NET Interactive. Now that Polyglot Notebooks are dropped upstream, I want to be explicit that this fix is not Interactive-specific: any host that compiles expression trees with closures across assembly boundaries — dynamic assemblies (Submission#N is just the common case), plugin architectures, add-in models — hits the same reflective MemberExpression crash in VisitMember. Interactive was merely the repro surface. The community fork (Polyglossy/interactive) also keeps that surface alive for notebooks.

Test, as offered. A real test for this rides with the test-project PR I promised on #29 rather than ballooning this one: the honest xUnit reproduction needs the closure field to live on a foreign type, which single-assembly tests cannot produce by construction — so the design is a small compiled-on-the-fly assembly (Roslyn scripting) that captures a local and hands the constraint across, making the pre-fix ArgumentException visible in the suite. This branch stays minimal on purpose.

Targeting. The two scoping questions from #29 still stand (main vs staging branch, anything to leave alone) — happy to aim this and the upcoming PRs at the tip of your stack if that saves you rebase work; on our side the drift adaptation is agent-driven, matching the workflow you described.

[jsboige]

The reproduction I offered earlier is in — and it landed one branch over rather than inside this PR, to keep the fix diff surgical (this branch still touches exactly the two files).

Where it lives: test/c805-cross-submission — this PR's branch plus a self-contained xUnit test project. The test compiles two chained C# scripts (Roslyn scripting — the same compiler .NET Interactive uses for its cells), so the captured local and the constraint lambda land in two different dynamic assemblies (Submission#0 / Submission#1): exactly the tree shape a single-assembly suite cannot produce by construction.

Red on main (same test project carried onto vanilla main):

Failed CrossSubmissionCaptureTests.Solve_ConstraintCapturingLocalFromPreviousSubmission_ReturnsModel
  Error Message:
   System.ArgumentException : Field 'b' defined on type 'Submission#0' is not a field on the target object which is of type 'Submission#1'.
  Stack Trace:
     at System.Reflection.RtFieldInfo.GetValue(Object obj)
   at Z3.Linq.ExpressionVisitor.VisitMember(...) ExpressionVisitor.cs:line 358
   at Z3.Linq.Theorem.AssertConstraints[T](...) Theorem.cs:line 166
   at Z3.Linq.Theorem`1.Solve() Theorem{T}.cs:line 39

1 failed / 0 passed — the exact exception from the wild, down to the submission numbering.

Green on this PR's branch: 1 passed / 0 failed, same test, same machine, only the partial-eval change in between.

The single added dependency is Microsoft.CodeAnalysis.CSharp.Scripting, in the test project only — it is the reproduction mechanism, another reason it stays off the fix branch. Happy to fold the branch into this PR, or rebase it on top of the test-infrastructure PR (#111) once that lands — your call; either way it's a fast-forward from where it sits.