Add observation/invariant consistency checks + YAML support

[Alan-Jowett]

Addresses #728.

Purpose
Add a small, test-oriented API to check whether a runtime observation (expressed as string constraints) is consistent with Prevail’s computed abstract invariants at a specific program point. This is intended as a semantic cross-check for validating transfer functions/invariant construction against observed executions (including partial observations).

What changed

• Extend analysis results to support checking observations against pre/post invariants.
• Add YAML schema + runner support so YAML fixtures can express and validate observation points.
• Add a new observe.yaml fixture and accompanying tests.
• Add documentation describing the abstract-vs-concrete comparison and intended semantics.

Semantics
The default check is “consistent” (i.e., meet-not-bottom / satisfiable): an observation passes if it is not ruled out by the invariant at that label.

Testing

• Updates are exercised via the Catch2 YAML test harness (src/test/test_yaml.cpp) and new fixture test-data/observe.yaml.

Notes
This does not change verification acceptance criteria; it is a validation/debugging aid for analysis soundness and model alignment.

Summary by CodeRabbit

• New Features

  • Added observation-vs-invariant checking at program entry/exit with "consistent" and "entailed" modes and convenient before/after queries.

• Tests

  • Extended YAML test framework to declare, parse, and run observation checks; added observe test suite and comprehensive test data; updated schema to validate observe entries and exception fixtures.

• Documentation

  • Added guide describing observation checks, modes, examples, and diagnostics.

_{✏️ Tip: You can customize this high-level summary in your review settings.}

[coderabbitai]

Walkthrough

Adds observation–invariant consistency checks: new enums/structs, AnalysisResult methods to check observations at pre/post program points (consistent vs entailed), YAML test-harness parsing and runner integration for observe cases, schema updates, test data, and documentation.

Changes

Cohort / File(s)	Summary
API Design & Types src/result.hpp	Adds InvariantPoint, ObservationCheckMode, ObservationCheckResult; extends InvariantMapPair with post; declares AnalysisResult::check_observation_at_label, is_consistent_before, is_consistent_after.
API Implementation src/result.cpp	Implements check_observation_at_label handling pre/post selection, bottom/unreachable invariants, consistent vs entailed modes, and the two is_consistent_* helpers.
Test Types src/test/ebpf_yaml.hpp	Adds TestCase::Observation (label, point, mode, constraints), observations, and optional expected_exception / actual_exception fields to test types.
Test Parsing & Runner src/test/ebpf_yaml.cpp	Adds YAML parsers (parse_label_scalar, parse_point, parse_mode, parse_observations), captures observe nodes and expected_exception, populates TestCase.observations, and integrates observation checks and exception handling into run_yaml_test_case.
Test Registration & Data src/test/test_yaml.cpp, test-data/observe.yaml	Registers observe.yaml in the test suite and adds test-data/observe.yaml with multiple observe cases covering consistent/entailed checks and error scenarios.
Schema & Docs test-schema.yaml, docs/compare-abstract-to-concrete-state.md	Updates test schema to permit observe and expected-exception branches; adds documentation describing observation–invariant checking semantics, API, and YAML usage.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~22 minutes

Possibly related issues

• Observation–Invariant consistency checking API (abstract interpretation cross-check) #728: Adds the observation–invariant consistency-check API and YAML support that this PR implements.

Possibly related PRs

• Consolidate verification logic, fail-fast printing #932: Related changes to AnalysisResult/result APIs that this PR extends.
• Use DYNAMIC_SECTION for yaml tests #924: Modifies the YAML test runner (run_yaml_test_case) similar to this PR's test-runner changes.

Suggested reviewers

• dthaler

🚥 Pre-merge checks | ✅ 2 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 0.00% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (2 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly summarizes the main change: adding observation/invariant consistency checks and YAML support for testing.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing touches

• 📝 Generate docstrings

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

Actionable comments posted: 3

🤖 Fix all issues with AI agents

In `@docs/proposal-issue-728-compare-abstract-to-concrete-state.md`:
- Around line 170-178: Replace bare URLs with markdown link syntax: update the
"Reference harness (example usage):
https://github.com/iovisor/ubpf/blob/main/libfuzzer/libfuzz_harness.cc" and
"Previous implementation attempt: https://github.com/vbpf/prevail/pull/729"
lines to use descriptive links like "Reference harness (example usage):
[libfuzz_harness.cc](https://github.com/iovisor/ubpf/blob/main/libfuzzer/libfuzz_harness.cc)"
and "Previous implementation attempt: [prevail PR
`#729`](https://github.com/vbpf/prevail/pull/729)" so the markdown linter (MD034)
is satisfied and rendering is cleaner.

In `@src/result.cpp`:
- Around line 42-47: The error message in the ObservationCheckMode::entailed
branch is inverted relative to the check observed_state <= abstract_state;
update the failure message to state that the observation does not entail the
invariant (e.g. "Observation does not entail the invariant (C ⊑ A is false)" or
"Observation does not entail the invariant (C_L ⊑ A_L is false)") so it matches
the semantics used by observed_state and abstract_state and the proposed
condition C_L <= A_L.

In `@src/test/ebpf_yaml.cpp`:
- Around line 153-177: In parse_observations, validate the required
"constraints" node before calling item["constraints"].as<vector<string>>():
check that item["constraints"] is defined and not null (and optionally
IsSequence()), and if missing or of wrong type throw a descriptive
std::runtime_error (e.g. "observe item missing required 'constraints' sequence
at label ..."); then safely convert to vector<string> and pass to
read_invariant. This change should be applied inside the loop that processes
each item in parse_observations to prevent YAML-cpp from throwing a generic
exception.

[coderabbitai]

Actionable comments posted: 3

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

src/result.hpp (1)

13-55: Clarify entailment direction in the public API contract.

The new API exposes ObservationCheckMode::entailed but doesn’t state whether it checks C ⊑ A or A ⊑ C. Add a short doc comment near the enum or method to prevent misuse.

Proposed fix

 enum class ObservationCheckMode {
     // Default: supports partial observations.
     consistent,
-    // Stricter: useful only when the observation is near-complete.
+    // Stricter: ok iff observation entails invariant (C ⊑ A); useful only when the observation is near-complete.
     entailed,
 };

As per coding guidelines, clarify analysis semantics for auditability.

🤖 Fix all issues with AI agents

In `@docs/compare-abstract-to-concrete-state.md`:
- Line 3: Replace the plain URL text "Related issue:
https://github.com/vbpf/prevail/issues/728" with a proper Markdown link—e.g.,
"Related issue: [`#728`](https://github.com/vbpf/prevail/issues/728)"—so the issue
is rendered as a clickable link in the document.

In `@src/test/ebpf_yaml.cpp`:
- Around line 100-123: The parse_label_scalar function accepts numeric labels
but doesn’t reject negative indices; after parsing the string to int with
std::stoi in parse_label_scalar, add an explicit check that index >= 0 and throw
a std::runtime_error("Invalid observation label: " + s) if it is negative so
Label{index} is only constructed for non-negative instruction indices; refer to
parse_label_scalar, the stoi call and the Label{index} construction when making
the change.

In `@src/test/ebpf_yaml.hpp`:
- Around line 19-25: The header declares struct Observation and the public
symbol std::vector<Observation> observations but doesn't include <vector>, so
add the missing include directive for the C++ vector header at the top of the
file; ensure <vector> is included alongside other includes so Observation and
observations compile when this header is included standalone.

[coveralls]

Pull Request Test Coverage Report for Build 21261651282

Warning: This coverage report may be inaccurate.

This pull request's base commit is no longer the HEAD commit of its target branch. This means it includes changes from outside the original pull request, including, potentially, unrelated coverage changes.

• For more information on this, see Tracking coverage changes with pull request builds.
• To avoid this issue with future PRs, see these Recommended CI Configurations.
• For a quick fix, rebase this PR at GitHub. Your next report should be accurate.

Details

• 124 of 148 (83.78%) changed or added relevant lines in 5 files are covered.
• 1 unchanged line in 1 file lost coverage.
• Overall coverage decreased (-0.05%) to 86.613%

---

Changes Missing Coverage	Covered Lines	Changed/Added Lines	%
src/result.cpp	21	29	72.41%
src/test/ebpf_yaml.cpp	100	116	86.21%

Files with Coverage Reduction	New Missed Lines	%
src/test/ebpf_yaml.cpp	1	78.77%

Totals
Change from base Build 21034306281:	-0.05%
Covered Lines:	9155
Relevant Lines:	10570

---

💛 - Coveralls

[coderabbitai]

Actionable comments posted: 2

🤖 Fix all issues with AI agents

In `@docs/compare-abstract-to-concrete-state.md`:
- Line 9: The sentence "This is an abstract-interpretation focused feature: it
acts as a **semantic cross-check**..." needs tightened wording and hyphenation:
change to "This abstract-interpretation–focused feature acts as a semantic
cross-check..." (use an en dash or hyphenate consistently as your style guide
prefers) and remove duplicated sentence-starters "If" in the following
conditional sentences (the block referenced around lines 99–103) by collapsing
or rephrasing them into one clear conditional clause; update the phrasing so
transfer-function/invariant clauses read smoothly (e.g., "it validates transfer
functions, invariant construction, and modeling assumptions against observed
executions") while keeping the emphasis on "semantic cross-check."

In `@src/test/ebpf_yaml.cpp`:
- Around line 156-187: Add deterministic YAML test fixtures exercising
parse_observations and its error branches: create fixtures where observe is
non-sequence, where an observe item is not a map, where an item is missing the
"constraints" field, and where "constraints" exists but is not a sequence of
strings so the error messages in parse_observations are hit; also add valid
observe entries that exercise both ObservationCheckMode outcomes (e.g., modes
that trigger "consistent" and "entailed" handling) by supplying labels via
parse_label_scalar, points via parse_point, modes via parse_mode, and constraint
lists that make read_invariant produce both sound (pass) and unsound (fail)
results. Name or comment each YAML fixture clearly so tests assert the expected
exception for the invalid cases and expected pass/fail behavior for the two
valid cases.

[coderabbitai]

Actionable comments posted: 4

🤖 Fix all issues with AI agents

In `@docs/compare-abstract-to-concrete-state.md`:
- Around line 30-48: The error message in check_observation_at_label is
inverted: when the code tests the relation observed_state <= abstract_state
(checking C ⊑ A) it logs "Observation does not entail the invariant"; update the
message to accurately reflect the checked relation, e.g. "Invariant does not
entail the observation (C ⊑ A is false)" or equivalent wording mentioning C and
A, by modifying the error string emitted in check_observation_at_label where
observed_state and abstract_state are compared.

In `@src/result.hpp`:
- Around line 25-28: The struct ObservationCheckResult currently leaves members
uninitialized by default; update the declaration of ObservationCheckResult so
that the bool member ok has a default value (e.g., ok = false) and consider
default-initializing message as well to ensure safe default construction; modify
the ObservationCheckResult definition to set these member defaults directly on
the ok and message members.

In `@test-schema.yaml`:
- Around line 7-64: Remove the overlapping `expected-exception` property from
the first `oneOf` branch so the standard branch (which requires `test-case`,
`pre`, `code`, `post`) only matches fixtures without exceptions; specifically
delete the `expected-exception` entry under `properties` in the first `oneOf`
branch so that the second branch remains the sole matcher for exception fixtures
and the `oneOf` ambiguity is resolved.
- Around line 49-53: The observe.at schema currently only allows strings but
parse_label_scalar accepts numeric instruction indices, so update the schema for
"observe.at" to accept either a string or an integer (e.g., change type from
"string" to a oneOf/anyOf allowing {"type":"string"} and {"type":"integer"})
while preserving the existing enum constraint for "point"; then add a test
fixture under test-data that includes an unquoted numeric instruction index
(e.g., at: 5) to validate the parser path exercised by parse_label_scalar.