Language contract and CI tightened per external review: E1009/E1011/E1012, mandatory oracle CI, proof budgets, CLI split

Author: Viktor Sovietov

.github/workflows/ci.yml

@@ -22,12 +22,34 @@ jobs:
       - run: cargo build --workspace --all-targets
       - run: cargo test --workspace
 
-  # INFRA-11: Soufflé is required only by the differential (Bool) jobs.
-  # Non-Soufflé exit harnesses (INFRA-6/7/8) run in `build` above.
-  # This job is wired here as a stub so the dependency is documented from day one.
-  souffle-diff:
+  # INFRA-11: the external differential oracles are MANDATORY here — a missing
+  # binary fails the job (STRATA_REQUIRE_ORACLES), it does not silently skip.
+  # `build` above stays oracle-free so the core loop is fast and hermetic;
+  # skip-if-absent remains a local-development courtesy only.
+  oracle-diff:
     runs-on: ubuntu-latest
-    if: false # TODO(INFRA-11): flip on once souffle is pinned/installed
+    env:
+      STRATA_REQUIRE_ORACLES: 1
     steps:
       - uses: actions/checkout@v4
-      - run: echo "souffle differential stub — see crates/strata-cli/tests/souffle_diff.rs"
+      - uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+      - name: Install clingo/gringo/clasp (Ubuntu; the clingo binary ships in the gringo package)
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y gringo clasp
+          clingo --version
+          gringo --version
+          clasp --version || true # clasp --version exits nonzero on some builds
+      - name: Install Soufflé 2.5 (pinned release .deb)
+        run: |
+          set -euo pipefail
+          curl -fsSL -o /tmp/souffle.deb \
+            https://github.com/souffle-lang/souffle/releases/download/2.5/x86_64-ubuntu-2404-souffle-2.5-Linux.deb
+          sudo apt-get install -y /tmp/souffle.deb
+          souffle --version
+      - name: Soufflé differential (Bool engine vs souffle, incl. fuzz)
+        run: cargo test -p strata-cli --test souffle_diff
+      - name: clingo/clasp differentials (ASP stack)
+        run: cargo test -p strata-asp

.github/workflows/gpu.yml

@@ -0,0 +1,25 @@
+name: gpu
+
+# The GPU differentials need CUDA hardware, which hosted runners don't have.
+# This workflow is manual (workflow_dispatch) and targets a self-hosted runner
+# labeled `gpu`; it exists so the GPU validation has a first-class, repeatable
+# entry point instead of living only in a shell history. Until such a runner is
+# registered, dispatching it simply queues — the honest state of affairs.
+on:
+  workflow_dispatch:
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  cuda-diff:
+    runs-on: [self-hosted, gpu]
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+      - name: GPU kernels vs CPU oracles (bit-exact)
+        run: cargo test -p strata-gpu --features cuda --release
+      - name: Record the environment the numbers came from
+        run: |
+          nvidia-smi
+          rustc --version

ARCHITECTURE.md

@@ -111,8 +111,9 @@ The reference interpreter is the oracle. Three overlapping checks defend it:
 2. **our Bool engine == Soufflé**, a differential harness that translates Core-IR
    to a Soufflé `.dl` program and compares results
    (`cargo test -p strata-cli --test souffle_diff`, needs `souffle`; skips
-   cleanly if absent). `Trop` is checked against an independent shortest-path
-   oracle instead.
+   cleanly if absent locally — the `oracle-diff` CI job makes it mandatory via
+   `STRATA_REQUIRE_ORACLES=1`). `Trop` is checked against an independent
+   shortest-path oracle instead.
 3. The probabilistic and ASP engines are themselves the slow, obviously-correct
    references (exact enumeration; reduct) that future fast/compiled/GPU methods
    must reproduce bit-for-bit.
@@ -131,7 +132,12 @@ validated bit-for-bit against a reference oracle:
   planner (cost-based ordering, hypertree decomposition, tensor-contraction
   width); radix/hypercube partition groundwork for multi-GPU; and the ASP
   grounding-simplification pass. Every kernel is diffed against an independent
-  CPU oracle.
+  CPU oracle. **Reproducibility caveat, stated plainly:** hosted CI has no
+  CUDA hardware, so the GPU differentials do not run under the badge — they
+  run on a CUDA machine via `cargo test -p strata-gpu --features cuda` (the
+  manual `gpu` workflow dispatches exactly that on a self-hosted runner).
+  On CPU-only checkouts the crate builds as a stub that returns
+  `GpuError::NotBuilt`.
 - **`strata-prob`** — knowledge compilation for режим B: provenance circuits
   (decomposable-AND / deterministic-OR), exact weighted model counting,
   reverse-mode gradients, top-k proofs, and a compilation cache — demonstrated

CONTRIBUTING.md

@@ -39,7 +39,12 @@ The differential fuzzer's program count is tunable:
 STRATA_SOUFFLE_FUZZ_N=10000 cargo test -p strata-cli --test souffle_diff fuzz_bool_vs_souffle
 ```
 
-If `souffle` is not on `PATH`, the Soufflé jobs skip cleanly rather than fail.
+If `souffle` is not on `PATH`, the Soufflé jobs skip cleanly rather than fail —
+a local-development courtesy only. In CI the `oracle-diff` job installs Soufflé
+pinned to a release .deb and clingo/gringo/clasp from the distro (versions
+logged in the job output) and sets `STRATA_REQUIRE_ORACLES=1`, which turns a
+missing oracle into a hard failure: a green badge means the external
+differentials actually ran.
 
 ## The bar for a change (what CI enforces)
 

README.md

@@ -23,7 +23,9 @@ phases (see [ARCHITECTURE.md](ARCHITECTURE.md)).
 > (stable model) solver for `@asp` modules. Cross-checked against
 > [Soufflé](https://souffle-lang.github.io/) and fuzzed (10k random programs,
 > naive vs semi-naive and vs Soufflé). **The whole shipped grammar executes**;
-> the GPU backend runs beside this stack, validated bit-for-bit against it.
+> the GPU backend runs beside this stack, validated bit-for-bit against it on
+> CUDA hardware (`--features cuda`; hosted CI runs the CPU stub — see
+> [Beyond the CPU pipeline](ARCHITECTURE.md#beyond-the-cpu-pipeline)).
 
 ## Quick start
 
@@ -156,7 +158,10 @@ strata-cli     the `strata` binary
 `strata-front` and `strata-check` are siblings that both depend only on
 `strata-ir`; the engine crates (`strata-gpu`, `strata-terms`, `strata-prob`)
 sit beside `strata-eval` and are validated bit-for-bit against the reference
-stack. See [ARCHITECTURE.md](ARCHITECTURE.md) for the full picture and
+stack — for `strata-gpu` that validation needs CUDA hardware
+(`cargo test -p strata-gpu --features cuda`; hosted CI runs the CPU stub, so
+the badge does not cover the GPU differentials). See
+[ARCHITECTURE.md](ARCHITECTURE.md) for the full picture and
 [CONTRIBUTING.md](CONTRIBUTING.md) to build and test.
 
 ## Correctness

crates/strata-asp/src/clasp.rs

@@ -82,6 +82,9 @@ mod tests {
     fn assert_clasp_agrees(rules: &[Rule], facts: &[(String, Vec<Val>)], cons: &[Vec<Literal>]) {
         let g = ground(rules, facts, cons).unwrap();
         let Some(clasp) = solve_with("clasp", &g) else {
+            if std::env::var_os("STRATA_REQUIRE_ORACLES").is_some() {
+                panic!("clasp not installed — but STRATA_REQUIRE_ORACLES is set");
+            }
             eprintln!("skipping: clasp not installed");
             return;
         };

crates/strata-asp/src/lib.rs

@@ -250,6 +250,12 @@ fn for_each_assignment(
     mut emit: impl FnMut(&HashMap<String, Val>),
 ) -> Result<(), AspError> {
     let k = vars.len();
+    // An empty universe grounds a rule with variables to nothing at all —
+    // zero assignments, not an index panic (the `strata check`-ok /
+    // `strata run`-panic hole an external review's follow-up found).
+    if k > 0 && universe.is_empty() {
+        return Ok(());
+    }
     let u = universe.len().max(1);
     // universe^k, bounded.
     let total = (0..k)
@@ -454,6 +460,20 @@ fn least_model(n_atoms: usize, rules: &[(usize, &[usize])]) -> HashSet<usize> {
 #[cfg(test)]
 mod tests {
     use super::*;
+
+    #[test]
+    fn empty_universe_grounds_a_var_rule_to_nothing() {
+        // No constants anywhere: a rule with variables has zero instantiations
+        // (never an index panic), and the empty model is the one stable model.
+        use strata_ir::high::program::{atom, var, Literal, Rule};
+        let rules = vec![Rule {
+            head: atom("p", vec![var("X")]),
+            body: vec![Literal::Neg(atom("q", vec![var("X")]))],
+        }];
+        let models = solve(&rules, &[], &[]).expect("solve");
+        assert_eq!(models.len(), 1);
+        assert!(models[0].is_empty(), "the empty model is stable");
+    }
     use strata_ir::high::program::{atom, var, Rule};
 
     fn a(pred: &str) -> Atom {

crates/strata-asp/tests/ablation.rs

@@ -156,6 +156,16 @@ fn ablate(name: &str, graphs: &[Graph], effort: impl Fn(u64, u64) -> u64) {
     eprintln!("ablation [{name}] effort — baseline {base}, GNN {gnn}, anti {anti}");
 }
 
+/// Under `STRATA_REQUIRE_ORACLES` (the oracle CI job), a missing external
+/// oracle is a hard failure — the differential must actually run. Locally,
+/// absence skips cleanly (INFRA-11).
+fn skip_or_die(what: &str) {
+    if std::env::var_os("STRATA_REQUIRE_ORACLES").is_some() {
+        panic!("{what} — but STRATA_REQUIRE_ORACLES is set, the oracle differential must run");
+    }
+    eprintln!("skipping: {what}");
+}
+
 #[test]
 fn gnn_ablation_two_regimes() {
     let mut rng = Rng(0x5EED_5EED);
@@ -167,7 +177,7 @@ fn gnn_ablation_two_regimes() {
         colors: 3,
     };
     if run(&program(&probe, Guide::None), false).is_none() {
-        eprintln!("skipping ablation: clingo not installed");
+        skip_or_die("ablation: clingo not installed");
         return;
     }
 

crates/strata-asp/tests/clingo_diff.rs

@@ -113,6 +113,16 @@ fn fact2(pred: &str, a: i64, b: i64) -> GroundAtom {
     (pred.to_string(), vec![Val::Int(a), Val::Int(b)])
 }
 
+/// Under `STRATA_REQUIRE_ORACLES` (the oracle CI job), a missing external
+/// oracle is a hard failure — the differential must actually run. Locally,
+/// absence skips cleanly (INFRA-11).
+fn skip_or_die(what: &str) {
+    if std::env::var_os("STRATA_REQUIRE_ORACLES").is_some() {
+        panic!("{what} — but STRATA_REQUIRE_ORACLES is set, the oracle differential must run");
+    }
+    eprintln!("skipping: {what}");
+}
+
 /// Assert our reference answer sets equal clingo's, projected to `show_pred`.
 /// Skips if clingo is unavailable.
 fn assert_agrees(
@@ -124,11 +134,11 @@ fn assert_agrees(
     show_pred: &str,
 ) {
     let Some(c_models) = clingo_models(lp) else {
-        eprintln!("skipping {name}: clingo not installed");
+        skip_or_die(&format!("{name}: clingo not installed"));
         return;
     };
     let Some(ours) = our_models(rules, facts, cons, show_pred) else {
-        eprintln!("skipping {name}: clasp not installed");
+        skip_or_die(&format!("{name}: clasp not installed"));
         return;
     };
     assert_eq!(

crates/strata-check/src/diagnostics.rs

@@ -29,10 +29,24 @@ pub mod codes {
     /// exact probabilistic provenance through recursion. Carries the nearest
     /// allowed alternative in its message (D9/I4).
     pub const TABLE_2_4_FORBIDDEN: DiagCode = DiagCode(1008);
+    /// A fact's `::` annotation does not fit the predicate's declared
+    /// annotation: an integer weight belongs on `Trop` only, a probability on
+    /// `Bool`/`Prov`/`Prov_k` only and inside [0, 1], and a `Trop` fact must
+    /// carry a weight.
+    pub const FACT_ANNOTATION_MISMATCH: DiagCode = DiagCode(1009);
     /// A fact on a `neural` predicate is not probabilistic: a neural predicate's
     /// ground atoms are a model's soft outputs, so they must carry a probability
     /// (`p :: n(...)`), never be asserted as certain.
     pub const NEURAL_FACT_NOT_SOFT: DiagCode = DiagCode(1010);
+    /// A construct that has no meaning under `@asp` (stable-model semantics):
+    /// `::` fact annotations, `input` declarations, queries, `neural`
+    /// predicates, compound fact arguments. Refused by name, never silently
+    /// dropped.
+    pub const ASP_UNSUPPORTED: DiagCode = DiagCode(1011);
+    /// A predicate is declared more than once with a conflicting signature —
+    /// silently letting the last declaration win would make every other check
+    /// order-dependent.
+    pub const CONFLICTING_DECLARATION: DiagCode = DiagCode(1012);
 
     pub const ALL: &[(DiagCode, &str)] = &[
         (UNDECLARED_PRED, "check.undeclared-predicate"),
@@ -43,7 +57,10 @@ pub mod codes {
         (NOT_EXECUTABLE, "check.not-executable-annotation"),
         (SEMIRING_CONFLICT, "check.semiring-conflict"),
         (TABLE_2_4_FORBIDDEN, "check.table-2.4-forbidden"),
+        (FACT_ANNOTATION_MISMATCH, "check.fact-annotation-mismatch"),
         (NEURAL_FACT_NOT_SOFT, "check.neural-fact-not-soft"),
+        (ASP_UNSUPPORTED, "check.asp-unsupported"),
+        (CONFLICTING_DECLARATION, "check.conflicting-declaration"),
     ];
 }