Research: Mercury mode/determinism/unique-mode checking as prior art for OwnIR ownership contracts (kill-first) #454

Classification

Research / P3 backlog / bounded source-backed prior-art study · NO production implementation authorized.

Study Mercury as a compiler-design reference for Own.NET's existing Roslyn → OwnIR → ownership/effects/aliasing pipeline. Do not port Mercury, change OwnIR or analyzer semantics, introduce a solver/runtime dependency, edit diagnostics, CI, benchmarks or roadmap on the strength of this issue.

Why Mercury, specifically?

The Mercury compiler statically checks three complementary kinds of contracts:

1. Mode / instantiation analysis: per-call argument-state transitions, notably in: ground → ground and out: free → ground; the compiler may reorder goals based on dependencies.
2. Determinism checking: det (exactly one solution), semidet (zero or one), multi (one or more), nondet (zero or more). These count logic solutions, not thread-scheduling or runtime determinism.
3. Unique modes: uo: free → unique, ui: unique → unique, di: unique → dead and mostly-unique variants; tied to linearity, update and explicit state threading (e.g., IO).

Critical caveat: the Mercury reference manual explicitly says unique modes are not fully implemented: nested uniqueness and unique-input modes are unsupported, and general dead-value reuse is not implemented. Its modes chapter also notes limitations around partially instantiated structures and alias tracking. Treat design intentions separately from shipped guarantees.

Primary references:

• Mercury Modes
• Mercury Determinism
• Mercury Unique modes
• Mercury implementation limitations
• Mercury source / compiler

Questions to answer

A. Mode analysis vs Own.NET effect/state facts

• Is there an actual gap in how our current OwnIR/MOS records a parameter's before → after state (initialized, borrowed, consumed, escaped, returned, may-alias) across calls?
• Distinguish Mercury's logical instantiation state from C# definite assignment, ref/out parameters, aliasing, disposal and ownership. No direct equivalence claims.
• Inspect source and find one small, representative compiler mode-checking path; write a grounded mapping table: Mercury concept / guarantee / implementation limit → current Own.NET fact / current gap / concrete false-positive or false-negative risk.

B. Determinism vs ownership reasoning

• Identify whether zero/one/multiple possible logical solutions suggests anything useful for Own.NET's path/call-summary interpretation; explicitly contrast with exceptions, early return, loops and concurrent nondeterminism in C#.
• Require at least one positive and one negative micro-example showing why this concept would or would not add diagnostic precision. If it cannot be translated meaningfully, KILL this direction.

C. Unique modes vs borrow/consume/alias

• Analyze di / ui / uo / dead / mostly_unique and backtracking assumptions as design inspiration, not proof of a Rust-like ownership system.
• Compare only against Own.NET's existing ownership state transitions and alias facts.
• Account for Mercury's actual limits: no nested uniqueness, no ui in current implementation, no general compile-time garbage collection/reuse; do not benchmark unimplemented optimizations.

Approach / kill-first gates

1. Reuse audit first: inspect existing Own.NET Roslyn lowering, OwnIR facts, MOS summaries, diagnostics and challenge fixtures. Record current behavior; don't infer gaps from names.
2. Source-backed notes: identify real Mercury declarations and compiler implementation (with stable commit/path references) supporting each claim.
3. Tiny C# fixture set, paper-first: at most 3 contrasting examples: (i) producer/consumer/borrow or out/definite-assignment; (ii) deterministic-looking call with early-failure/exception/path ambiguity; (iii) unique owner with alias or state handoff. Expected outputs must be framed relative to current Own.NET behavior; don't invent new error IDs.
4. Write an explicit REUSE IDEA / PARK / NO-GO decision for each concept. If existing analysis covers it or the translation from logic semantics to imperative C# is invalid, stop.
5. Optional coding and tests need a separate GO; nothing here permits a Mercury build, runtime dependency, changes to current diagnostics, or CI.

Related work / avoid duplicates

• #438 SPDS field-stack aliasing
• #429 WALA demand-driven alias precision
• #434 Heros IFDS/IDE
• #449 abstract object graph/state joins
• #395 heap-effect summaries
• #366 ownership-handoff across concurrency

This issue is about contracts and static checking design, not a new alias solver, a new abstract state implementation, concurrency analysis, or compiler rewrite.

Definition of Done

• Source-linked semantics table (mode / determinism / uniqueness), including unsupported/incomplete features.
• Verified mapping to existing OwnIR/MOS/ownership analysis; explicit no-benefit cases.
• Bounded 3-example matrix with expected observable analyzer differences or reason for NO-GO.
• Separate and defensible REUSE / PARK / NO-GO verdicts plus estimated integration cost/risks.
• No production code, no dependency changes, no benchmark/CI change, no promises of automatic ownership correctness.

Success = learn something verifiable about our current checker, not acquire a new language stack.