0%

Conformance Proof and Cross-Executor Parity

Goal

Prove that the closed logical product and its physical satisfaction maps preserve Ori semantics across every supported executor while keeping the evaluator independent.

Observation Model

The normalized observer reports logical identities and semantics: calls, ownership observations, retain/drop obligations, cleanup, user-drop boundaries, and unwind transitions. VM and compiled adapters translate their physical actions back to those stable identities for verification. Evaluator instrumentation reports the same logical observations from semantic execution, but it neither reads the physical maps nor serves as a second AIMS realization.

Proof-to-Implementation Bridge

This section absorbs the still-relevant VF-7 and current-executable verification work from the completed burden plan. Every closure, totality, identity, and satisfaction theorem has a concrete verifier or constructor obligation, a test family, and a durable proof-map row. The existing T1-T5 and composition theorems remain the foundation.

Matrix

Positive coverage spans normal and unwind control flow, user destructors, closures, protocols, aggregate fields, aliases, branches, joins, loops, TRMC-rewritten graphs, per-iteration allocations, owned and borrowed call contracts, external visibility, and thread reachability. Negative coverage corrupts each identity and map invariant independently and asserts rejection before execution.

Executor Gate

The harness follows the executor/capability surface that bytecode-vm actually ships. Every available evaluator, VM, LLVM/debug/release/AOT, native/WASM, and JIT leg must agree on observable results and normalized logical events and must be leak-clean. A capability intentionally deferred by bytecode-vm is represented as an explicit gate with an owning successor, never an unreported skip.

Completion Evidence

The full conformance probe returns PASS only when proof synchronization, verifier bridges, parity, logical-event correspondence, normal/unwind/user-drop coverage, adversarial rejection, and leak freedom are all green.

Work Items

  • Define a normalized logical observer over stable event, call, retain/drop, cleanup, user-drop, and unwind identities; evaluator instrumentation observes semantics independently and never consumes VM or compiled physical plans.
  • Complete the VF-7/current executable conformance bridge transferred from aims-burden-tracking: connect committed Lean invariants and closed-schema theorems to verifier checks, artifact construction, and the runtime observer with traceable proof-to-implementation rows.
  • Build the conformance harness and diagnostic entry point used by plan-level criteria, comparing evaluator, VM, LLVM/debug/release/AOT, native/WASM, and JIT projections that bytecode-vm actually ships or explicitly gates.
  • Run positive matrices for straight-line, branches, joins, loops, TRMC-rewritten graphs, per-iteration allocation, user drops, closures, protocols, aggregates, owned and borrowed calls, FFI/external visibility, normal return, and unwind.
  • Run adversarial matrices for missing/duplicate/stale identities, tampered fingerprints, invalid fused coverage, foreign satisfaction maps, incompatible call boundaries, illegal physical feedback, and deliberately divergent executor cleanup; every case must fail closed with actionable diagnostics.
  • Require observable result parity, normalized logical event correspondence, exact user-drop and unwind correspondence, satisfaction-map coverage, and leak freedom across the supported executor matrix; record any intentionally unavailable projection as an explicit bytecode-owned capability gate rather than silently skipping it.