fix(test): model oracle test fails instead of skipping as a pass (P0-4)

[hyperpolymath]

ULTRAPLAN P0-4 — the Lean↔Rust model-oracle correspondence test no longer passes when the oracle is missing. Stacked on P0-3 (base chore/lean-4-34-1).

Defect

tests/model_oracle_correspondence.rs returned (reported ok) when no oracle binary was found. rust-cli.yml and compilation_tests.yml run cargo test without building the oracle, and lean-verification.yml ran cargo test before building it, so most green runs never compared anything. locate_oracle() also silently fell back to the default path when VSH_MODEL_ORACLE pointed at nothing.

Change

• The test is #[ignore = "needs Lean model_oracle — build with just build-model-oracle, run with --ignored"]: shown as ignored, never as ok.
• When run, a missing oracle panics. A set-but-invalid VSH_MODEL_ORACLE panics instead of falling back.
• Asserts sequences_run > 0 and checked_probes > 0, and prints both.
• lean-verification.yml and Justfile test-correspondence-model pass --ignored --nocapture.

Evidence

Run	Result
cargo test	rc=0 — 786 passed, 0 failed, 15 ignored (the oracle test moved from "passed" to "ignored")
oracle built on v4.34.1, --ignored --nocapture	rc=0 — 1218 probes agreed across 196 non-empty sequences (of 200 generated)
negative control VSH_MODEL_ORACLE=/nonexistent … --ignored	rc=101 — VSH_MODEL_ORACLE is set to "/nonexistent", which is not a file
default oracle binary moved away, --ignored	rc=101 — Lean model oracle not found at …

cargo fmt --check and clippy are clean. CHANGELOG.adoc:48-55 (a historical entry) still says the test "skips cleanly", so a new changelog entry may be wanted.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 57 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 57aaf64e-4d43-483d-b34e-1731a7682fce

📥 Commits

Reviewing files that changed from the base of the PR and between 53ae47f and 182a723.

📒 Files selected for processing (3)

• .github/workflows/lean-verification.yml
• Justfile
• impl/rust-cli/tests/model_oracle_correspondence.rs

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Autopilot is currently an internal CodeRabbit preview.

---

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.}

[github-actions]

🔍 Hypatia Security Scan

Findings: 118 issues detected

Severity	Count
🔴 Critical	9
🟠 High	27
🟡 Medium	82

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage"
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync"
  },
  {
    "line": 38,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 44,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/cflite_batch.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/cflite_batch.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 45,
    "reason": "job in .github/workflows/cflite_pr.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/cflite_pr.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 20,
    "reason": "job in .github/workflows/instant-sync.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/instant-sync.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 83,
    "reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 52,
    "reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/label-triage.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 88,
    "reason": "workflow .github/workflows/compilation_tests.yml:88 step `Run ignored tests (stress)` swallows non-zero exit via `continue-on-error: true` — failures will be masked",
    "type": "RE005",
    "file": ".github/workflows/compilation_tests.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence