Proposal: Observation–Invariant Consistency Checking for Abstract Interpretation

This issue proposes a small, test-oriented API to check whether a runtime observation (expressed as a set of constraints) is consistent with Prevail’s computed abstract invariant at a given program point.

This is intentionally abstract-interpretation focused: it is a semantic cross-check that helps validate transfer functions, invariant construction, and modeling assumptions by comparing them against observed executions.

Why this issue exists

The previous discussion suffered from ambiguous terminology (I used the wrong terms). This issue aims to pin down the intended relation precisely, so we can discuss implementation details without talking past each other.

Problem statement (abstract interpretation view)

Prevail computes invariants $A_L$ at program points $L$ (e.g., pre/post instruction labels). In practice, we often have runtime observations:

• Sometimes we have a complete concrete state $\sigma$.
• More commonly, we have a partial observation $o$ (only some registers, only pointer type+offset fields, only “changed” locations, etc.).

We want a well-defined, maintainable check to answer:

“Is this observed execution (or partial observation of it) ruled out by the invariant at $L$?”

If it is ruled out, that’s a strong semantic mismatch signal:

• the VM semantics (interpreter/JIT) may be wrong, or
• the abstract semantics (transfer function / constraints) may be wrong.

Terminology and intended relation

Standard AI vocabulary:

• Abstract state / invariant $A_L$: the abstract element computed by Prevail at label $L$.
• Concretization $\gamma(A_L)$: the set of concrete states represented by $A_L$.
• Concrete state $\sigma$: a full VM snapshot at a program point.
• Partial observation $o$: a set of reported facts about the runtime state.
  It denotes a set of possible concrete states $\Sigma(o)$ consistent with those facts.

The key check: consistency / satisfiability

For runtime checking we primarily want:

$$ \Sigma(o) \cap \gamma(A_L) \neq \emptyset $$

Interpretation: “There exists at least one concrete state that both matches the observation and is allowed by the invariant.”

Operationally (in abstract domain terms), if we map the observation to an abstract element $C_L$:

$$ (A_L \sqcap C_L) \neq \bot $$

This is the consistency (a.k.a. satisfiability / feasibility) check.

Why not the lattice order check by default?

The relation

$$ C_L \sqsubseteq A_L $$

answers a different question (“do my constraints entail the invariant?”) and is typically too strong when $C_L$ is built from a partial observation (missing facts behave like $\top$).

This mismatch in intent/terminology is what caused confusion previously.

Goals

• Provide a stable API to check observations against invariants at a label.
• Support checking both pre and post invariants.
• Make the default semantics be consistency (meet-not-bottom).
• Reuse Prevail’s existing string constraint vocabulary (as used by YAML tests).
• Provide actionable diagnostics on failure.

Non-goals

• This is not a new acceptance criterion for verification.
• This is not an attempt to expose the entire abstract domain as a public API.
• This does not define a new constraint language.

Existing building blocks in Prevail

Prevail already has most of the required machinery:

• AnalysisResult stores per-label invariants, including pre and post.
• StringInvariant is a set of textual constraints.
• EbpfDomain::from_constraints(...) converts constraint strings into an abstract element.
• EbpfDomain supports meet/intersection (operator&) and bottom checks (is_bottom()).

Proposed API

C++ API (preferred)

Expose a check that makes the intended semantics explicit:

namespace prevail {

enum class InvariantPoint {
    pre,
    post,
};

enum class ObservationCheckMode {
    // Default: supports partial observations.
    consistent,
    // Optional: only useful when the observation is near-complete.
    entailed,
};

struct ObservationCheckResult {
    bool ok;
    std::string message;
};

[[nodiscard]]
ObservationCheckResult check_observation_at_label(
    const AnalysisResult& result,
    const Label& label,
    InvariantPoint point,
    const StringInvariant& observation,
    ObservationCheckMode mode = ObservationCheckMode::consistent);

}

Semantics:

• Convert observation to EbpfDomain C_L.
• Select EbpfDomain A_L as the chosen invariant (pre or post).
• If mode==consistent: return ok iff !(A_L & C_L).is_bottom().
• If mode==entailed: return ok iff C_L <= A_L.

C ABI (optional)

If a C harness needs it, provide a wrapper around the same semantics using an opaque analysis context.

Labels and constraint format

• Labels: use Prevail’s existing printed label format (e.g., entry, exit, 12, foo/12, etc.).
• Constraints: reuse the existing string constraint vocabulary from YAML tests.

Important: an observation may be partial.

• Omitted constraints are fine.
• Malformed constraints or self-contradictory constraints should be treated as errors.

Diagnostics

On failure, return a message that includes:

• label and whether it was pre/post,
• whether the check was consistent or entailed,
• the observation constraints,
• the invariant rendered back to constraints (when helpful),
• a short explanation (e.g., “meet is bottom: contradiction”).

Soundness and scope

This API is validation-only:

• It does not change verification outcomes.
• It provides a way to detect semantic mismatches by checking that observed behavior is not excluded by the invariant.

Use cases (examples)

VM/JIT instrumentation during fuzzing

An instrumented interpreter can call out before each instruction, emit a (partial) observation constraint set, and ask Prevail whether it is consistent with the pre-invariant at that label.

Reference harness (example usage):
https://github.com/iovisor/ubpf/blob/main/libfuzzer/libfuzz_harness.cc

Regression tests that check intermediate states

YAML-driven tests can include intermediate “require/observation” points to assert that the analyzer’s invariants are compatible with expected intermediate observations.

Prior art

• Previous implementation attempt: Implement ebpf_check_constraints_at_label #729
  • Key takeaway: meet-not-bottom semantics matches partial observations; entailment is often the wrong question.

Proposed next steps

1. Implement check_observation_at_label (C++ API) using existing AnalysisResult, EbpfDomain::from_constraints, and operator&.
2. Add a small number of targeted tests:
   • consistent accepts partial-but-compatible observations,
   • consistent rejects contradictory observations,
   • (optional) entailed behaves as a stricter mode.