Research: map domain-theoretic fixed-point assumptions to Own.NET's ownership analysis #450

Classification

• Type: bounded research / formal-semantics documentation
• Priority: P3 / backlog; not a production implementation request
• Reference: Tom de Jong, Domain theory and denotational semantics (MGS 2023)
• Area: ownership abstract-state meaning, dataflow iteration, least fixed points, solver assumptions
• Related, not superseded: Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 (IKOS-inspired independent soundness oracle/operator audit), P-037 kernel: solve_with / lfp_chaotic returns Some(non-fixpoint) on an unfair schedule #368 (P-037 unfair-schedule non-fixpoint counterexample), Research: mine G# for reusable CFG/dataflow/analyzer patterns #365 (G# CFG/dataflow patterns), Research: evaluate LLZK dataflow lattices, SourceRef and IR validators #444 (LLZK lattice review), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (evidence/completeness)

Why

Own.NET has an ownership-analysis dataflow solver and a separate formal P-037 kernel; it already uses lattices and fixpoint iteration. The MGS notes offer a precise introductory account of partial orders, directed approximations, continuous functions, least fixed points, denotational semantics of recursion, soundness, and computational adequacy.

The interesting question is not whether Own.NET should adopt PCF/Scott's model or reimplement its engine. It is whether we can state exactly which mathematical assumptions justify our existing analysis and distinguish proved contracts from implementation/test assumptions.

Important semantic distinction: the bottom element in PCF denotational semantics can represent nontermination/undefined results, whereas bottom in a typical may-analysis state lattice denotes no reachable concrete states; top can represent an unknown set of states. These meanings must not be silently equated. Likewise, a domain-theoretic least-fixpoint theorem does not establish soundness of a C# ownership analyzer without a concrete/abstract semantic relation and suitable transfer assumptions.

Research question

Can a short, source-pinned domain-theoretic note make the current solver's ordering, convergence and partiality/completeness contracts more explicit, reveal one concrete missing proof obligation or misleading assumption, or confirm that existing specifications already cover them?

This is a specification/assumption-mapping ticket, not #433's independent concrete-state oracle, operator mutation suite, or a new diagnostic.

Bounded plan

1. Check overlap first. Read Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433, P-037 kernel: solve_with / lfp_chaotic returns Some(non-fixpoint) on an unfair schedule #368, the existing P-037 formal kernel notes/proofs, and the active Rust analysis/worklist implementation. If the mapping already exists, cross-link and close this issue without producing a parallel document.
2. Define a tiny semantic vocabulary with citations. For the actual Own.NET abstract state and solver, identify the order ⊑, bottom/top (where defined), joins, transfer functions, and the result reported on incomplete analysis. Keep unreachable, unknown, nontermination, budget exceeded, and safe diagnostic outcome conceptually distinct. State explicitly which concepts are outside the current model.
3. Map the fixed-point assumptions. Separate:
   • monotonicity of transfers and the join/operator properties actually relied on;
   • finite-height convergence vs Scott-continuity/Kleene iteration (use only the theorem whose prerequisites are satisfied);
   • synchronous vs chaotic/worklist iteration and fairness/coverage of the schedule;
   • terminated-at-a-fixpoint vs stopped-by-budget/partial result;
   • model-level soundness vs diagnostic-level correctness/completeness.
     Treat P-037 kernel: solve_with / lfp_chaotic returns Some(non-fixpoint) on an unfair schedule #368 as known prior evidence about missing schedule fairness, not an invitation to reproduce its bug or reopen it.
4. Walk one small ownership example through concrete reachable states, abstraction, branch/merge and (only if relevant) a loop; explicitly label unmodeled C# effects and what the example cannot prove. Prefer existing Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 fixtures instead of inventing a separate harness.
5. Conclude with a decision: (a) existing contracts suffice, (b) one or more precisely located, independently actionable proof/spec gaps deserving follow-up, or (c) STOP because the lecture material provides no additional engineering leverage.

Deliverable / acceptance criteria

• A brief (roughly 2–4 pages) source-pinned technical note or a concise update to an existing formal note; no new standalone theory framework.
• Table: mathematical notion → actual Own.NET type/operator/solver location → required hypothesis → currently enforced/proved/tested/assumed/unknown → practical consequence.
• Explicit distinction between PCF denotational semantics and abstract interpretation/dataflow; no claim of a direct correctness proof for arbitrary C#.
• One hand-reviewable worked example and a falsifiable statement of its limitations.
• Links to Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 and P-037 kernel: solve_with / lfp_chaotic returns Some(non-fixpoint) on an unfair schedule #368 with a clear non-duplication boundary.
• Final verdict: ALREADY-COVERED / ACTIONABLE-GAP / RESEARCH-ONLY / STOP; new implementation or proof work only through separate, narrowly scoped issues if justified.

Non-goals / stop conditions

No PCF interpreter, language rewrite, new lattice/solver, proof-assistant migration, production optimization, CI gate, or general proof of analyzer soundness. No duplicate oracle/property/mutation work from #433. Do not confuse mathematical soundness claims with a passing finite test suite.

Source: MGS 2023 lecture notes and exercises (Scott model of PCF, least fixed points, soundness/adequacy).