migration: phase 2.5 — requirement-driven oracle cases (no implementation reads) by yairfalse · Pull Request #50 · false-systems/syva

yairfalse · 2026-04-28T22:12:35Z

Phase 2.5 — requirement-driven oracle cases

Case roster delta

Block 010-019: 10 cases, file adapter × core.
Block 030-039: 10 cases, API adapter × core.
Block 040-049: 10 cases, cross-cutting core contracts.
Block 020-029 remains reserved for k8s adapter oracle work.

Hard-rule audit

Changes are limited to eval/.
Every harness YAML spec now has source, requirement, observable, and failure_means.
Source citations point to non-implementation docs/contracts: CLAUDE.md, SKILLS.md, and syva-proto/proto/syva_core.proto.
The harness schema now requires the new source-backed fields.

Contract gaps surfaced

Several NEG cases intentionally encode safer contracts that current docs imply but do not fully specify:
- case_042: same-zone AllowComm should be rejected.
- case_043: AllowComm with an unknown zone should return NotFound.
- case_048: path-like zone names should be rejected.
These three are #[ignore] by default until Yair decides whether the stricter contracts are accepted.
case_014 and case_015 expose read-surface gaps: current public ListZones does not reveal zone_type or allow_ptrace, so the oracle can only assert successful external registration.

Per-case first-run outcomes

No Linux/BPF core was available in this environment, so live-system cases skipped cleanly when core was required. Cases that validate adapter CLI failure behavior can pass without core if binaries are built; lifecycle cases remain environment-gated.

ID	Outcome	Source	Note
case_010-case_019	SKIP/PASS by environment	`CLAUDE.md:Architecture / syva-adapter-file`	Requirement is file adapter translating TOML policy into local core state; live core required for behavioral assertions.
case_030-case_039	SKIP/PASS by environment	`CLAUDE.md:Architecture / syva-adapter-api`	Requirement is REST adapter translating requests into local core state; live core and built adapter binary required.
case_040-case_049	SKIP/PASS by environment, with 041/042/043/048 ignored where noted	`syva-proto/proto/syva_core.proto` and `CLAUDE.md:Enforcement Semantics`	Cross-cutting requirements assert public RPC and status contracts; ignored cases are explicit pending contract decisions.

Verification

cargo test --manifest-path eval/oracle/Cargo.toml --no-run
ok

cargo test --manifest-path eval/oracle/Cargo.toml -- --list | grep -E 'case_(01[0-9]|03[0-9]|04[0-9])'
all 30 new cases listed

cargo run --manifest-path eval/harness/Cargo.toml -- --filter case_01
10/10 passed

cargo run --manifest-path eval/harness/Cargo.toml -- --filter case_03
10/10 passed

cargo run --manifest-path eval/harness/Cargo.toml -- --filter case_04
10/10 passed

git diff --check
ok

Failures interpretation

No runtime contract failures were observed locally because a live Linux/BPF core was not available. The suite is structured so those failures surface on the intended Linux run instead of being weakened to match current behavior.

Copilot

Pull request overview

This PR extends the eval/ contract-testing system by adding Phase 2.5 oracle cases and matching harness specs for local-core adapters (syva-file, syva-api) plus cross-cutting core behavior, along with new blackbox helpers inside the oracle to spawn adapters and perform simple HTTP polling.

Changes:

Add oracle test cases case_010–case_019, case_030–case_039, case_040–case_049 to eval/oracle.
Add harness YAML specs for the new cases so syva-harness can run them by ID.
Add new oracle helpers (temp policy dirs, adapter spawning/guarding, basic HTTP requests, polling helpers) and a tempfile dependency.

Reviewed changes

Copilot reviewed 32 out of 33 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
eval/oracle/src/main.rs	Adds adapter/process/HTTP helpers and implements Phase 2.5 oracle cases (010–019, 030–039, 040–049).
eval/oracle/Cargo.toml	Adds `tempfile` dependency for temp policy directory helpers.
eval/oracle/Cargo.lock	Updates lockfile for new `tempfile` dep and resolves `syva-proto` deps.
eval/harness/cases/case_010_file_adapter_startup_toml_registers_zone.yaml	Harness spec for file-adapter startup reconcile contract.
eval/harness/cases/case_011_file_adapter_runtime_toml_add_registers_zone.yaml	Harness spec for file-adapter runtime add contract.
eval/harness/cases/case_012_file_adapter_toml_remove_removes_zone.yaml	Harness spec for file-adapter remove contract.
eval/harness/cases/case_013_file_adapter_toml_modify_updates_policy.yaml	Harness spec for file-adapter modify/update contract.
eval/harness/cases/case_014_file_adapter_privileged_zone_type_registers.yaml	Harness spec for privileged zone_type acceptance via file adapter.
eval/harness/cases/case_015_file_adapter_ptrace_capability_registers.yaml	Harness spec for CAP_SYS_PTRACE acceptance via file adapter.
eval/harness/cases/case_016_file_adapter_rejects_core_and_cp_flags_together.yaml	Harness spec for syva-file flag mutual exclusion.
eval/harness/cases/case_017_file_adapter_rejects_missing_target_flag.yaml	Harness spec for syva-file requiring exactly one target mode.
eval/harness/cases/case_018_file_adapter_malformed_toml_does_not_poison_valid_policy.yaml	Harness spec for malformed TOML isolation behavior.
eval/harness/cases/case_019_file_adapter_retries_until_core_socket_appears.yaml	Harness spec for syva-file retrying until core socket exists.
eval/harness/cases/case_030_api_post_zone_registers_in_core.yaml	Harness spec for API adapter POST creating a zone in local-core mode.
eval/harness/cases/case_031_api_list_zones_matches_core_names.yaml	Harness spec for API adapter list reflecting core ListZones.
eval/harness/cases/case_032_api_get_zone_matches_core_view.yaml	Harness spec for API adapter get reflecting core view.
eval/harness/cases/case_033_api_put_zone_updates_core_view.yaml	Harness spec for API adapter put/update behavior in local-core mode.
eval/harness/cases/case_034_api_delete_zone_removes_from_core.yaml	Harness spec for API adapter delete removing zone in core.
eval/harness/cases/case_035_api_malformed_json_returns_4xx_without_core_change.yaml	Harness spec for malformed JSON yielding 4xx without state change.
eval/harness/cases/case_036_api_get_missing_zone_returns_404.yaml	Harness spec for 404 on missing zone in local-core mode.
eval/harness/cases/case_037_api_rejects_core_and_cp_flags_together.yaml	Harness spec for syva-api flag mutual exclusion.
eval/harness/cases/case_038_api_returns_5xx_while_core_is_down_then_recovers.yaml	Harness spec for API behavior during core outage + recovery (skippable).
eval/harness/cases/case_039_api_missing_core_socket_waits_without_crashing.yaml	Harness spec for syva-api tolerating missing core socket at startup.
eval/harness/cases/case_040_register_100_zones_succeeds_and_status_counts_them.yaml	Harness spec for registering 100 zones and verifying status/list.
eval/harness/cases/case_041_register_past_max_zones_fails_cleanly.yaml	Harness spec for max_zones overflow failure behavior (stress/ignored).
eval/harness/cases/case_042_allow_comm_same_zone_is_invalid_argument.yaml	Harness spec for rejecting same-zone AllowComm.
eval/harness/cases/case_043_allow_comm_unknown_zone_is_not_found.yaml	Harness spec for rejecting unknown-zone AllowComm.
eval/harness/cases/case_044_status_zones_active_matches_list_zones_len.yaml	Harness spec for consistency between status and list.
eval/harness/cases/case_045_status_uptime_is_monotonic.yaml	Harness spec for monotonic uptime.
eval/harness/cases/case_046_rapid_register_remove_same_name_leaves_zone_absent.yaml	Harness spec for churn register/remove leaving no residue.
eval/harness/cases/case_047_register_zone_empty_name_is_invalid_argument.yaml	Harness spec for rejecting empty zone name.
eval/harness/cases/case_048_register_zone_path_traversal_name_is_invalid_argument.yaml	Harness spec for rejecting path-like zone names.
eval/harness/cases/case_049_list_zones_during_churn_returns_consistent_snapshots.yaml	Harness spec for ListZones snapshot structural consistency under churn.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-04-28T22:20:03Z

+fn target_bin(bin_name: &str) -> anyhow::Result<PathBuf> {
+    let path = workspace_root()?
+        .join("target")
+        .join("debug")
+        .join(bin_name);


target_bin assumes binaries live under <workspace>/target/debug/ and ignores common variations like CARGO_TARGET_DIR, --release builds, target triples, and Windows .exe suffix. This can make adapter-related cases unexpectedly SKIP/fail even when the binaries are built. Consider resolving the target dir/profile from env (e.g. CARGO_TARGET_DIR, PROFILE) and handling platform-specific executable names, or allowing an explicit env override for each adapter binary path.

Copilot · 2026-04-28T22:20:03Z

+    let (status_code, body) =
+        http_request(addr, "POST", "/v1/zones", Some("{not-json")).expect("post malformed");
+    assert!((400..500).contains(&status_code), "{status_code}: {body}");
+    let after = list_zones(&mut c).await.expect("list after").len();
+    assert_eq!(before, after);


This case asserts the total ListZones length is unchanged after a malformed request. If the oracle is run with multiple tests concurrently (default cargo test behavior) or against a core with other activity, unrelated zone churn can make this flaky. Prefer asserting that the specific zone name you attempted to create is still absent (or run this case with enforced single-threading).

Copilot · 2026-04-28T22:20:04Z

+        .await
+        .expect_err("same-zone comm must fail");
+    assert_eq!(err.code(), tonic::Code::InvalidArgument);
+    remove_zone(&mut c, &name, false).await.ok();


AllowComm currently succeeds for same-zone pairs in syva-core (there is no same-zone validation in the gRPC handler / ingest path), so this expect_err + InvalidArgument assertion will fail on a live core. If the stricter contract is intentional but not yet implemented, consider marking the case #[ignore] (or skipping) until core behavior matches.

Copilot · 2026-04-28T22:20:04Z

+        .await
+        .expect_err("phantom comm must fail");
+    assert_eq!(err.code(), tonic::Code::NotFound);
+    remove_zone(&mut c, &name, false).await.ok();


syva-core maps unknown-zone errors from allow_comm_local to tonic::Code::Internal today (the gRPC handler wraps the ingest error with Status::internal(...)), so asserting NotFound here will fail on a live core. If the desired contract is NotFound, core needs to translate this error accordingly; otherwise update/relax the oracle expectation or mark the case ignored until the contract is decided.

Copilot · 2026-04-28T22:20:04Z

+    let zones = list_zones(&mut c).await.expect("list");
+    let s = status(&mut c).await.expect("status");
+    assert_eq!(s.zones_active as usize, zones.len());
+    for name in &names {


This asserts Status.zones_active exactly equals a preceding ListZones length. If the oracle suite is run with parallel tests or against a shared core with concurrent zone churn, the two RPCs can observe different snapshots and make this flaky. Consider either filtering/counting only the zones created by this case or polling until the values converge within a short timeout.

Copilot · 2026-04-28T22:20:04Z

+                policy: Some(empty_policy()),
+            })
+            .await
+            .expect_err("path-like zone name must fail");
+        assert_eq!(err.code(), tonic::Code::InvalidArgument, "name={bad}");


syva-core RegisterZone currently only validates zone_name is non-empty; it does not reject path-like names containing / or ... As written, these expect_err/InvalidArgument assertions will fail on a live core unless core-side name validation is added. If the stricter contract is intentional but not yet implemented, consider marking this case #[ignore] (or skipping) until core behavior matches.

yairfalse · 2026-04-28T22:27:51Z

Addressed the six review comments in 4f467ac:

target_bin now supports explicit per-binary overrides via SYVA_ORACLE_<BIN>_BIN, honors CARGO_TARGET_DIR, honors SYVA_ORACLE_PROFILE / PROFILE, handles platform executable suffixes, and searches target-triple subdirectories.
case_035 no longer compares global ListZones length. It asserts the specific rejected zone name remains absent, so unrelated concurrent zone churn cannot make it flaky.
case_044 no longer assumes two adjacent RPCs observe the same instant. It polls briefly for Status.zones_active and ListZones().len() to converge.
case_042, case_043, and case_048 keep the stricter contract assertions, but are now #[ignore] by default because current core behavior is known not to satisfy them yet:
- same-zone AllowComm currently succeeds,
- unknown-zone AllowComm currently maps to Internal,
- path-like zone names are currently accepted.

Verification after fixes:

cargo test --manifest-path eval/oracle/Cargo.toml --no-run
ok

cargo test --manifest-path eval/oracle/Cargo.toml -- --list | grep -E 'case_(01[0-9]|03[0-9]|04[0-9])'
all 30 new cases listed

cargo run --manifest-path eval/harness/Cargo.toml -- --filter case_01
10/10 passed

cargo run --manifest-path eval/harness/Cargo.toml -- --filter case_03
10/10 passed

cargo run --manifest-path eval/harness/Cargo.toml -- --filter case_04
10/10 passed

git diff --check
ok

migration: phase 2.5 oracle adapter cases

0ca25b8

yairfalse requested a review from Copilot April 28, 2026 22:14

Copilot started reviewing on behalf of yairfalse April 28, 2026 22:14 View session

Copilot AI reviewed Apr 28, 2026

View reviewed changes

fix phase 2.5 oracle review issues

4f467ac

add source-backed oracle spec fields

6f05672

yairfalse changed the title ~~migration: phase 2.5 — oracle cases for adapter and cross-cutting requirements~~ migration: phase 2.5 — requirement-driven oracle cases (no implementation reads) Apr 28, 2026

yairfalse merged commit f8c03b2 into main Apr 28, 2026
6 checks passed

yairfalse deleted the migration/phase-2-5-oracle-adapter-cases branch April 28, 2026 22:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

migration: phase 2.5 — requirement-driven oracle cases (no implementation reads)#50

migration: phase 2.5 — requirement-driven oracle cases (no implementation reads)#50
yairfalse merged 3 commits into
mainfrom
migration/phase-2-5-oracle-adapter-cases

yairfalse commented Apr 28, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Apr 28, 2026

Uh oh!

Copilot AI Apr 28, 2026

Uh oh!

Copilot AI Apr 28, 2026

Uh oh!

Copilot AI Apr 28, 2026

Uh oh!

Copilot AI Apr 28, 2026

Uh oh!

Copilot AI Apr 28, 2026

Uh oh!

yairfalse commented Apr 28, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

yairfalse commented Apr 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Phase 2.5 — requirement-driven oracle cases

Case roster delta

Hard-rule audit

Contract gaps surfaced

Per-case first-run outcomes

Verification

Failures interpretation

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 28, 2026

Choose a reason for hiding this comment

Uh oh!

yairfalse commented Apr 28, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

yairfalse commented Apr 28, 2026 •

edited

Loading