Research: evaluate LLZK dataflow lattices, SourceRef and IR validators #444

Classification

• Type: research / architecture
• Priority: P3, research-only (not on the critical path)
• Implementation intent: none; compare existing patterns before proposing code changes
• External project: project-llzk/llzk-lib (Apache-2.0)
• Related: Research: mine G# for reusable CFG/dataflow/analyzer patterns #365 (G# CFG/dataflow/analyzer donor review). Avoid duplicating its generic CFG/lattice scope.

Motivation

LLZK-lib is an MLIR-based IR and analysis infrastructure for zero-knowledge circuit programs, not a C# ownership analyzer. It is interesting specifically as a small, concrete reference for:

1. separating dataflow facts from user-facing validation diagnostics;
2. tracking references to fields/aggregate values and conservatively handling unknown array indices;
3. testing invariant-checking and diagnostic passes independently of transformations.

This is not a proposal to replace OwnIR with MLIR, adopt LLZK as a dependency, or use ZK proving backends for .NET. The only useful outcome would be a demonstrably better local design or a concrete checker for an existing Own.NET problem.

Source-code targets to inspect

A. May/must facts and separate diagnostics

• MemberOverwriteAnalysis.cpp
• LLZKValidationPasses.cpp
• Member-write diagnostic tests

LLZK maintains mayWrites and mustWrites; at joins it unions the former and intersects the latter. A dedicated pass reports missing/overwritten writes, including a note pointing to the previous write.

Own.NET comparison: inspect current ownership/Dispose facts and diagnostics. Do we already separate possibly disposed from definitely disposed through branches and loops? Where is evidence/provenance attached to diagnostics? Identify a concrete missed diagnostic or false positive before recommending any change.

B. Field/array reference provenance and conservative alias overlap

• SourceRefLattice.cpp
• ConstraintDependencyGraph.cpp
• SourceRefTests.cpp

LLZK models references into aggregate storage, field/array accesses, ranges, and potential overlaps. Tests explicitly cover symbolic indices and half-open/dynamic ranges.

Own.NET comparison: inspect current OwnIR access paths, alias facts, member-sensitive writes, array/index modeling and conservative fallback for unknown indices. Determine whether there is a specific gap for x.Field, nested paths, array elements, or alias invalidation. Do not equate ZK struct/array semantics with managed heap, ref, Span<T>, or CollectionsMarshal.

C. Independent IR validation / test harness

• Validation passes
• lit/FileCheck tests
• Analysis unit tests

Own.NET comparison: would a small, independent OwnIR validator catch an actual class of malformed lowering or lost facts before the ownership solver runs? Keep structural IR validity distinct from semantic soundness: validating IR invariants alone does not prove Roslyn → OwnIR lowering preserved program semantics.

Scope / method

• Inspect the three donor areas above, citing exact classes/functions and existing tests.
• Find Own.NET's current corresponding code/tests first; document what is already implemented to avoid duplicate work.
• Compare may/must joins, provenance, unknown-target conservatism, convergence, and diagnostic evidence.
• If a gap exists, give a minimal C# reproducer + expected/actual Own.NET result, or a minimal malformed-OwnIR fixture an independent validator would reject.
• Produce one small decision table: donor mechanism | current equivalent | demonstrated gap | cost | use now / later / reject.
• If proposing follow-up work, link a separate implementation issue with measurable tests; do not refactor or add dependencies under this research ticket.

Non-goals

• MLIR migration or redesigning OwnIR to resemble LLZK;
• incorporating LLZK C++ code, ZK-specific dialects, Picus/R1CS/SMT backends;
• generic abstract-interpretation framework work without a real failing case;
• merging this with Research: mine G# for reusable CFG/dataflow/analyzer patterns #365 or postponing current Own.NET milestones.

Acceptance / exit criteria

Close with a brief review that answers:

1. Is the may/must and validator split already covered by Own.NET? If not, what concrete defect is exposed?
2. Is LLZK's SourceRef model relevant beyond existing OwnIR/alias design, with at least one meaningful C# repro?
3. Would an independent validator prevent a known invalid lowering/fact-loss case? Precisely which invariant?
4. What is the cost/benefit and decision for each area?

Success: one evidenced, narrowly scoped improvement candidate or a documented no-action conclusion. No production patch required.