Skip to content

Research: Beni-inspired ownership differential oracle and obligation-mutant validation #455

New issue
New issue
Open
Open
Research: Beni-inspired ownership differential oracle and obligation-mutant validation#455

Description

@PhysShell
PhysShell
opened on Nov 9, 2026

Classification

Why Beni is relevant

Beni is a pre-1.0 functional language/compiler written in Zig. The useful part for Own.NET is not the language surface but its ownership subsystem: Beni preserves value semantics while allowing selected list/record operations to lower to in-place mutation only when a static ownership checker proves that the old value cannot be observed afterwards.

The ownership requirements make the policy unusually strict:

  • every destructive write gets an ownership verdict;
  • there is no silent-copy / runtime-refcount / slower-algorithm fallback when safety cannot be established;
  • the checker reasons about holders, aliases, evaluation order, closures, retained runtime values, foreign/JS boundaries, branches, paths/fields, and interprocedural summaries;
  • the stated soundness contract is essentially: for every accepted write, nothing except the write's result may subsequently observe the base's pre-write identity/state.

Primary source:

This is a useful neighboring design point for Own.NET because the question is analogous even though the language semantics differ: when may an optimization/ownership verdict be trusted despite aliases, paths, retained values and interprocedural effects?

The more interesting part: executable Lean ownership oracle

Beni contains a separate Lean 4 project under proofs/ownership/. Its README describes:

  • a typed ANF language;
  • a value-semantics interpreter;
  • an in-place interpreter;
  • an ownership checker based on per-function summaries;
  • a differential oracle that executes accepted generated programs in both interpreters;
  • bounded enumeration and targeted generated programs;
  • deliberate checker mutants / required negative controls;
  • proof statements and an audit path.

Crucially, upstream explicitly says this is not a certified ownership checker: three soundness statements still contain sorry, and the main theorem is proved only from one of them. Finite campaigns are described as evidence, not proof.

Primary sources:

At the inspected revision, the retained results report a shipping-compiler differential bridge with 116,650 inputs and 43,185 translated/value-checked cases, alongside forward/reverse leads and zero interpreter-confirmed unsafe original leads in that campaign. These are upstream measurements, not independent validation and not a whole-language soundness proof.

Transferable pattern

The strongest idea is the test architecture:

source/generated program
        |
        v
 ownership checker
        |
   accepted only
      /     \
     v       v
value semantics   optimized/destructive semantics
     \       /
      compare
        |
        +--> minimized counterexample / first divergence

Then deliberately weaken a soundness obligation, e.g.:

  • drop an escape propagation;
  • forget a live alias / retained capture;
  • weaken branch-join handling;
  • forget a result-position holder;
  • mishandle a construction/view sharing relation;
  • treat an incomplete/unknown case as harmless.

A mutant is useful only if an independent corpus/oracle exposes an accepted semantic disagreement. This is much stronger than treating code coverage or a single aggregate mutation score as analyzer adequacy.

Research question

Can Own.NET gain materially better soundness evidence by adapting Beni's value-vs-optimized differential oracle plus obligation-oriented mutants, without duplicating #405/#433/#451 or building a second full analyzer?

The goal is not to make Own.NET imitate Beni's ownership policy. The goal is to test whether the same validation shape can expose defects in Own.NET's own ownership/resource semantics.

Bounded investigation

0. No-duplication map first

Read and pin the current state of:

Identify exactly what is missing. If Beni contributes only naming or another implementation of already-covered ideas, close as ALREADY-COVERED / NO-INCREMENTAL-VALUE.

1. Extract Beni's verification architecture, not its implementation

At the pinned Beni revision, document:

  • what the production checker accepts/rejects/pends;
  • what the Lean model actually represents and what it omits;
  • the value-semantics vs in-place-semantics comparison contract;
  • how per-function summaries enter the oracle;
  • how bounded enumeration differs from random generation and targeted templates;
  • how required mutants/negative controls are defined;
  • which claims are theorem-backed, empirically checked, assumed, or still sorry.

Produce a small evidence-boundary table rather than a generic language summary.

2. Map the pattern to one Own.NET semantic seam

Choose one existing, already-modeled ownership/resource operation with an independent expected semantics and a production implementation seam, preferably reusing #433/#405 fixtures.

Candidate shapes:

  • branch/join loses one feasible ownership state;
  • alias/resource identity is confused across update/release/use;
  • a retained value/capture remains observable after an operation assumed exclusive;
  • a may effect is accidentally promoted to must;
  • an incomplete/unknown call/effect is accidentally treated as safe;
  • result/receiver identity is mishandled across a transfer.

Do not create a general second C# interpreter.

3. Minimal differential oracle experiment

If and only if a distinct seam exists, build or reuse the smallest independent executable semantics that can evaluate that seam twice:

  1. reference/value semantics: conservative behavior that never relies on the optimization/ownership assumption under test;
  2. production-like/optimized semantics: behavior using the ownership decision or abstract transfer being tested.

For every accepted/safe decision in the selected subset, compare:

  • observable result;
  • resource/ownership state;
  • relevant trace;
  • error/terminal status;
  • identity relationships where semantically meaningful.

A disagreement should shrink to a minimal fixture and feed #269-style first-divergence evidence where possible.

If the distinction cannot be represented independently of production code, STOP rather than creating two copies of the same bug.

4. Obligation-oriented mutants

Reuse #405 infrastructure where possible. Add only mutants tied to the selected semantic obligation. Candidate families inspired by Beni:

  • escape/retention mutant: forget one holder/capture;
  • branch mutant: lose one incoming feasible state at join;
  • alias/path mutant: treat overlapping paths as disjoint;
  • result-position mutant: forget that old state remains reachable beside a returned/result path;
  • summary mutant: omit one read/write/consume effect from a callee summary;
  • unknown mutant: convert incomplete/unsupported to a safe/no-effect interpretation.

Classification must remain per-mutant/per-case, e.g. Detected / Missed / Invalid / Equivalent / Infra-error. Do not compress the result into a vanity mutation score.

5. Bounded enumeration before more fuzzing

If the selected semantics has a small finite shape, enumerate a deliberately tiny grammar/cartesian product over:

  • alias/no-alias;
  • one/two branches;
  • before/after use;
  • retained/not-retained result;
  • one/two resources or paths;
  • known/unknown summary;
  • safe/unsafe near-neighbor pairs.

The purpose is to guarantee coverage of chosen semantic combinations, not to claim exhaustive C# coverage.

Random/property-based generation is additive only after the bounded target space is explicit.

6. Evidence and decision

For each tested rule/mutant record:

Final disposition: ALREADY-COVERED / RESEARCH-ONLY / GO-NARROW / STOP.

Acceptance criteria

Non-goals

Licensing / provenance note

GitHub currently does not detect a repository license for canassa/beni at the inspected revision. Treat the upstream code as read-only prior art unless licensing is clarified. Adapt ideas and independently reimplement experiments; do not copy implementation code.

Why this may be worth doing

Beni is unusually valuable related work because it places four things next to each other in one living compiler:

  1. an explicit destructive-update soundness contract;
  2. a production ownership checker;
  3. an independent executable semantic model with differential checking;
  4. obligation-oriented negative controls/mutants plus bounded enumeration.

That combination is directly relevant to Own.NET's current problem: not merely producing ownership verdicts, but producing credible evidence that the verdict engine still rejects the right counterexamples when individual semantic obligations are weakened.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions