Part 4 sessions 4-5: symbolic algebra, primes, and number theory

.github/workflows/verify.yml

@@ -1,7 +1,12 @@
 name: Verify
 
 # Deeper checks than ci.yml (which builds, tests and reports coverage):
-# randomized property tests, Kani model checking, and a strict lint pass.
+# randomized property tests, Kani model checking, Miri, and a strict lint
+# pass.
+#
+# Every `run:` here is quoted. An unquoted value containing a colon
+# followed by a space is parsed as a nested mapping, which makes the whole
+# file invalid and fails the run before any job starts.
 
 on:
   push:
@@ -21,55 +26,85 @@ jobs:
       - uses: dtolnay/rust-toolchain@stable
       - uses: Swatinem/rust-cache@v2
       - name: Run the property suite in release mode
-        run: cargo test --release --test properties
+        run: "cargo test --release --test properties"
+
+  clippy-strict:
+    name: Clippy (strict)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: clippy
+      - uses: Swatinem/rust-cache@v2
+      # Default lints are errors.
+      #
+      # The float-accuracy lints (float_cmp, lossy_float_literal,
+      # imprecise_flops, suboptimal_flops) are deliberately NOT enabled
+      # here. They are allow-by-default, and naming them with -W does not
+      # make them advisory: -D warnings denies the whole warning level, so
+      # every one they raise becomes an error. Enabling them alongside
+      # -D warnings produced 3429 errors, suboptimal_flops accounting for
+      # most of them. Rewriting those expressions as mul_add changes
+      # rounding, so they need review one at a time rather than a blanket
+      # gate. Run them manually when doing that work:
+      #   cargo clippy --all-targets -- -W clippy::suboptimal_flops
+      - name: Clippy
+        run: "cargo clippy --all-targets -- -D warnings"
 
   kani:
     name: Kani model checking
     runs-on: ubuntu-latest
+    # Thirteen harnesses at 24 to 68 seconds each, run in parallel with -j.
+    # Sequentially that is seven minutes; the bound is generous against a
+    # slower runner while still failing rather than holding a runner for the
+    # six-hour job default.
+    timeout-minutes: 45
     steps:
       - uses: actions/checkout@v4
+      # The seven harnesses CBMC cannot decide in a CI-sized budget are behind
+      # the `kani-slow` feature and are not enabled here. Every harness was
+      # timed individually against a five-minute budget; the split and the
+      # measured times are recorded in src/verification/mod.rs. Briefly:
+      # asserting panic-freedom or finiteness lands in well under a minute,
+      # while asserting a numeric relation between symbolic float expressions
+      # exceeds five minutes, because CBMC has to bit-blast the full mantissa
+      # of every intermediate.
       - uses: model-checking/kani-github-action@v1
         with:
-          args: --output-format terse
+          args: "-j --output-format terse"
 
   miri:
     name: Miri (UB check)
     runs-on: ubuntu-latest
+    timeout-minutes: 45
     steps:
       - uses: actions/checkout@v4
       - uses: dtolnay/rust-toolchain@nightly
         with:
           components: miri
       - uses: Swatinem/rust-cache@v2
-      - run: cargo miri setup
-      # The crate contains no `unsafe`, so Miri is a backstop rather than the
-      # primary check, and interpreting all 2700+ tests would dominate CI
-      # time. Scope it to the modules doing the heaviest index and slice
-      # arithmetic, where an out-of-bounds or aliasing mistake would surface.
+      - run: "cargo miri setup"
+      # The crate contains no `unsafe`, so Miri is a backstop rather than
+      # the primary check. It interprets at roughly a hundredth of native
+      # speed -- these 27 tests take twelve minutes -- so it is scoped to
+      # core::, the interval and dual-number arithmetic where index and slice
+      # reasoning is densest, rather than to the whole suite.
+      #
+      # Five tests in there carry #[cfg_attr(miri, ignore)]. Miri evaluates
+      # sin, exp and powi with its own implementations rather than the host's,
+      # and deliberately randomises the result within the slack the language
+      # allows, so a test asserting an exact float value fails under Miri
+      # whatever the code does. Those five are exactness assertions and are
+      # skipped here; they run everywhere else.
+      #
+      # A libtest filter is a substring match, not a path prefix, so a bare
+      # `core::` also selects `graph::core::` and `verification::core::` --
+      # brute-force combinatorial tests that Miri needs tens of minutes for.
+      # Skipping `::core::` anchors the filter to the top-level module: a
+      # top-level path starts with `core::` and so has nothing before it to
+      # match, while every nested one does.
       - name: Run core numerics tests under Miri
-        run: cargo miri test --lib -- core:: linalg:: spatial::
+        run: "cargo miri test --lib -- core:: --skip ::core::"
         env:
           MIRIFLAGS: "-Zmiri-strict-provenance"
-
-  clippy-strict:
-    name: Clippy (strict)
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-      - uses: dtolnay/rust-toolchain@stable
-        with:
-          components: clippy
-      - uses: Swatinem/rust-cache@v2
-      # Default lints are enforced as errors. The float-accuracy lints are
-      # advisory: `suboptimal_flops` alone fires ~2800 times across the
-      # numerics, and rewriting those expressions as `mul_add` changes
-      # rounding, so each one needs a deliberate review rather than a blanket
-      # denial.
-      - name: Clippy
-        run: >
-          cargo clippy --all-targets --
-          -D warnings
-          -W clippy::float_cmp
-          -W clippy::lossy_float_literal
-          -W clippy::imprecise_flops
-          -W clippy::suboptimal_flops

Cargo.toml

@@ -15,5 +15,11 @@ exclude = ["assets/", ".github/", "*.profraw"]
 
 [dependencies]
 
+[features]
+# Enables the Kani harnesses that CBMC cannot decide in a CI-sized budget.
+# See src/verification/mod.rs for the measured times and the reason for the
+# split. Off by default so `cargo kani` runs only the harnesses that finish.
+kani-slow = []
+
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }