Research: FORVES2-style conditional semantic validation and proof-assumption audit for OwnIR #445

Classification

• Type: bounded research / semantic-validation architecture and proof-assumption audit
• Priority: P2 / backlog; research-only, no production checker or Coq integration by default
• Area: Roslyn → OwnIR semantic fidelity → contextual resource transitions and claimed diagnostic invariants → independent adjudication
• Prior art: costa-group/forves2 (Coq 8.16.1 / coq-bbv 1.4; EVM block equivalence under input constraints), FORVES, GASOL
• Related, not superseded: Research: COVA-inspired targeted path-condition oracle for ownership soundness (bounded spike) #431 (COVA-derived path feasibility oracle), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutation harness), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (Roslyn→OwnIR/ICFG fidelity), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (completeness/evidence semantics), Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (alias precision), Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425 (method-effect contract tests), P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 (first divergence)
• Default decision: do not port EVM semantics, build a whole-program symbolic executor, replace OwnIR, change production verdicts, or assume the published FORVES2 binary/kernel is fully formally verified.

Why FORVES2?

FORVES2's transferable architectural feature is conditional equivalence under explicit, justified input-state constraints. The source represents contextual conditions (equalities, strict and non-strict inequalities, literals including x + c) in disjunctive normal form; it offers dummy/syntactic/octagon implication-checker modes and compares symbolic stack, memory and storage states.

Pointers to inspected sources:

• constraints.v, context.v, octagon.v
• block_equiv_checker.v, block_equiv_checker_soundness.v
• tests.v (e.g. checking a conditional rewrite of LT under v0 < v1)

Important distinction: FORVES2 checks EVM block equivalence; it does not establish C# ownership/lifetime properties. Own.NET would need a separately defined abstract resource-state semantics (identity, acquire/release/use, aliases, transfers, exceptional exits). This issue asks whether the checking pattern gives measurable independent value, not whether FORVES2 can be used unchanged.

Trust / proof gap to audit before citing formal guarantees

A source-level inspection of FORVES2 found three Admitted obligations in block_equiv_checker.v, around lines 818–823, attached to mk_tools_1, which the main checker invokes. Other admissions include constraints.v's trivial satisfiability-checker placeholder and a dummy_sha3 test stub; some apparent Admitted tokens in optimizations/div_shl.v are inside comments. Different admissions must not be conflated.

Do not claim a complete executable proof or an exploit from these observations alone. Audit the concrete theorem/kernel dependency chain, extracted OCaml entrypoint, production/default configurations, and which admissions are reachable or trusted. Pin upstream commit(s). Where possible, build with the documented Coq toolchain and run Print Assumptions on the selected soundness theorem(s) plus coqchk; record unsupported or inconclusive states if compilation cannot be reproduced. Distinguish formal claims in the paper from guarantees actually obtained from pinned artifacts.

Research question

Can a tiny independent, context-aware validator detect a concrete OwnIR lowering/transfer/semantic-assumption defect that existing #405/#426/#430/#431 infrastructure cannot already adjudicate, while keeping every source→context and context→resource assertion explicitly justified?

Do not confuse:

1. Path feasibility (#431): can the claimed branch/path be reached?
2. Conditional equivalence (this issue): under trustworthy input constraints, are two bounded transitions/representations equivalent for the modeled observations?
3. Ownership property (potential follow-on): after a transition, is an operation such as use/release permitted on this resource identity?

Showing C => P is useful only if C is independently justified by the program semantics. An unjustified context must not result in a safe/proven outcome.

Bounded plan

0. Inventory, source pinning, overlap gate

• Pin Own.NET commit, runtime and available Python/Rust analysis modes; inventory existing source→OwnIR diagnostics, semantic mutations, evidence schema and first-divergence instrumentation.
• Pin FORVES2 commit, extract the exact conditional-equivalence contract, supported constraints and symbolic-state observations. Note that FORVES2 handles EVM jump-free sequences with contextual assumptions; do not call it a full CFG/program prover.
• Map overlap to Research: COVA-inspired targeted path-condition oracle for ownership soundness (bounded spike) #431/Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405/Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430/Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 and select one genuinely different seam. If this is just another path-condition solver or a duplicate mutation harness, STOP / NO-GO.

1. Independent small semantic corpus (6–10 cases)

Pre-register source-level expected behavior before comparing with Own.NET's answers. Reuse existing fixtures where possible. Include pairs for:

• same unchanged guard across branches vs reassignment that invalidates its fact;
• conditional Dispose then Use on same resource identity vs unrelated instance;
• alias assignment and use after release; changed alias/receiver identity;
• using or try/finally cleanup including an exceptional edge only where faithfully modeled;
• branch join with differing resource states;
• unresolved/virtual call, unsupported expression and a deliberately omitted context fact.

For each example record: executable/source oracle, relevant C# assumptions (including dispatch, exception and alias semantics), expected states/diagnostics, OwnIR facts, baseline verdict/evidence, and first representational divergence.

2. Conditional micro-validator (only if corpus shows incremental value)

Prototype as an isolated test-only checker over a deliberately tiny transition language, preferably consuming existing OwnIR/test fixture facts. Do not adopt Coq, Z3 or external runtimes merely for aesthetics.

Suggested contract:

• Input: two explicitly bounded transitions/representations, initial resource state and validated contextual assumptions C, observations to compare, and provenance/completeness of all facts.
• Output: EQUIVALENT_UNDER_ASSUMPTIONS, COUNTEREXAMPLE_IN_MODEL, or UNKNOWN / INCOMPLETE / UNSUPPORTED, with constraints, witnesses if any, proof/model boundary, replay metadata and runtime.
• Equivalence must cover the modeled observable state (resource identity/state and relevant exceptional behavior), not mere agreement on a diagnostic label.
• No closed-world inference from missing edges/callees; preserve unknown states and distinct may/must interpretations.
• A counterexample in an abstraction is not automatically an executable C# defect. Independently replay/adjudicate it.

Optional: small SMT queries for finite, faithful models. Independently check any proposed rewrite/equivalence and force explicit timeout/unknown results. Never translate unknown into safe, infeasible, or proven.

3. Adversarial checks / proof discipline

• Drop or falsify one incoming contextual condition: validator must not continue claiming conditional proof under unvalidated assumptions.
• Break alias/resource identity; force an unresolved call, truncated CFG, exception edge or budget exhaustion.
• Mutate a state transition or lowering rule to introduce a known bug; confirm the independent check detects at least one targeted mutation without consulting Own.NET's own diagnostic as oracle.
• Distinguish trusted assumptions, verified premises, merely assumed stubs, unsupported features, and any formally undischarged proof obligations.
• No promotion to production Safe, warning suppression or PROVEN based on solver agreement, unavailable facts, or upstream paper wording.

4. Compare incremental utility and decide

Per case: source oracle, baseline, independent result, disagreement attribution, exact boundary where information is lost, reproducible commands, runtime and completeness. Identify one confirmed incremental Own.NET semantic failure/evidence benefit or report negative evidence and stop. Do not claim population precision/recall from the small handpicked set.

Acceptance / stop criteria

• Source-pinned FORVES2 architecture note: contextual implication, checker contracts, jump-free limitation, EVM↔C# portability boundary.
• Explicit Admitted / trusted-assumption audit of the soundness theorem and checker path; Coq build / Print Assumptions / coqchk if feasible, or documented inability to establish it.
• Clear separation from Research: COVA-inspired targeted path-condition oracle for ownership soundness (bounded spike) #431 feasibility oracle and Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405/Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430/Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 existing tests/evidence.
• 6–10 independently adjudicated positive/negative/adversarial cases, or justified early STOP if no novel seam exists.
• If checker is built: documented assumptions, bounded semantics, tri-state/multi-status results, replayable artifacts, and adversarial uncertainty tests.
• Measurable incremental semantic failure/evidence improvement or honest NO-GO.
• Final outcome STOP / RESEARCH ONLY / FOLLOW-UP CANDIDATE; production follow-up only after independently confirmed benefit.

Non-goals

No FORVES2/Coq port, EVM checker dependency, new general SMT framework, full C# proof kernel, production safety verdict changes, extra mutation harness, unbounded symbolic execution or rewrite of ownership engine. GPL/AGPL licensing must be reviewed before any future code reuse; research-level ideas do not justify importing upstream implementation.

Deliverable: short evidence-backed GO/NO-GO report with pinned upstream sources, proof-assumption audit and (if justified) one independently reproduced conditional OwnIR semantic counterexample.