Add kani-slow feature gate and lower CI parallelism to 2

.github/workflows/ci.yml

@@ -377,24 +377,28 @@ jobs:
   # -------------------------------------------------------------------------
   # Kani formal verification — split into four parallel shards by layer so
   # the slowest one finishes within the hosted-runner budget.
-  # Observed wall-clock medians on main (per-job, --jobs 3):
-  #   kani-core:           ~15 min  (ffwd-core,                ~103 proofs)
-  #   kani-arrow:          ~19 min  (ffwd-arrow,                ~27 proofs;
-  #                                  SIMD/columnar accumulator proofs are
-  #                                  individually expensive — ~42s/proof)
-  #   kani-runtime-types:  ~?? min  (ffwd-runtime + ffwd-types,
-  #                                  ~55 orchestration-layer proofs)
-  #   kani-io-output:      ~?? min  (ffwd-io + ffwd-output +
-  #                                  ffwd-diagnostics + ffwd binary,
-  #                                  ~52 I/O-layer proofs)
-  # The previous monolithic kani-periphery shard (six crates, 107 proofs)
-  # was the long pole at ~21 minutes. The split keeps ownership boundaries
-  # clear while the 120-minute timeout on the two broad shards leaves room
-  # for cold-cache variance and hosted-runner throttling. Revisit this after
-  # collecting stable main-branch runtime history and tune the broad shards
-  # back toward the 90-minute core/arrow budget if the split remains stable.
-  # Each shard uses kissat and --jobs 3 — ubuntu-latest has 4 vCPUs; jobs=3
-  # leaves headroom for solver memory spikes while still using the runner.
+  #
+  # Fast vs slow proofs:
+  #   Proofs gated behind `kani-slow` feature (>30s solver time) run only
+  #   on push-to-main and ci:full PRs. PR CI runs fast proofs only (~5 min
+  #   wall-clock for core shard vs ~45+ min with slow proofs).
+  #
+  # Observed proof counts and timing constraints:
+  #   kani-core:           ~130 fast + ~15 slow proofs (ffwd-core + ffwd-kani)
+  #                        Slow: structural(unwind 65), cri(unwind 52), severity
+  #   kani-arrow:           24 proofs (ffwd-arrow) — all fast
+  #   kani-runtime-types:   63 proofs (ffwd-runtime + ffwd-types) — all fast
+  #   kani-io-output:       59 proofs (ffwd-io + ffwd-output +
+  #                        ffwd-diagnostics + ffwd binary) — all fast
+  #
+  # All shards use --jobs 2 (not 3 or 4). CBMC solver processes consume
+  # 3-5 GB each; at --jobs 3+ on 16 GB runners, memory pressure causes
+  # OOM kills or runner preemption (manifests as "runner shutdown signal"
+  # after only minutes). --jobs 2 keeps peak memory under ~10 GB.
+  #
+  # The core shard gets 120 min (slow proofs need it on main).
+  # Arrow gets 60 min (finishes in ~5 min, but needs compilation time).
+  # Runtime and IO shards get 120 min for cold-cache variance.
   # -------------------------------------------------------------------------
   kani-core:
     name: Kani proofs (core)
@@ -404,7 +408,7 @@ jobs:
       contains(github.event.pull_request.labels.*.name, 'ci:full') ||
       (github.event.pull_request.draft == false && needs.changes.outputs.kani_required == 'true')
     runs-on: ubuntu-latest
-    timeout-minutes: 90
+    timeout-minutes: 120
     steps:
       - uses: actions/checkout@v6
 
@@ -413,18 +417,19 @@ jobs:
           save-if: ${{ github.event_name == 'push' || !github.event.pull_request.draft }}
           key: kani-core
 
-      - name: Run Kani verification (ffwd-core)
+      - name: Run Kani verification (ffwd-core + ffwd-kani)
         uses: model-checking/kani-github-action@v1
         with:
           args: >-
             --solver kissat
-            --jobs 3
+            --jobs 2
             --output-format terse
             -Z function-contracts
             -Z mem-predicates
             -Z stubbing
             -p ffwd-kani
             -p ffwd-core
+            ${{ (github.event_name == 'push' || contains(github.event.pull_request.labels.*.name, 'ci:full')) && '--features kani-slow' || '' }}
 
   kani-arrow:
     name: Kani proofs (arrow)
@@ -434,7 +439,7 @@ jobs:
       contains(github.event.pull_request.labels.*.name, 'ci:full') ||
       (github.event.pull_request.draft == false && needs.changes.outputs.kani_required == 'true')
     runs-on: ubuntu-latest
-    timeout-minutes: 90
+    timeout-minutes: 60
     steps:
       - uses: actions/checkout@v6
 
@@ -446,14 +451,11 @@ jobs:
       - name: Run Kani verification (ffwd-arrow --lib)
         # ffwd-arrow has a binary with required-features that cargo-kani
         # cannot skip, so verify only the library target.
-        # --jobs 4: arrow proofs are the heaviest per-proof (up to ~90s each
-        # on the make_string_view/scatter families) so saturating all 4
-        # vCPUs here gives more wall-clock return than on the other shards.
         uses: model-checking/kani-github-action@v1
         with:
           args: >-
             --solver kissat
-            --jobs 4
+            --jobs 2
             --output-format terse
             -Z function-contracts
             -Z mem-predicates
@@ -485,7 +487,7 @@ jobs:
         with:
           args: >-
             --solver kissat
-            --jobs 3
+            --jobs 2
             --output-format terse
             -Z function-contracts
             -Z mem-predicates
@@ -518,7 +520,7 @@ jobs:
         with:
           args: >-
             --solver kissat
-            --jobs 3
+            --jobs 2
             --output-format terse
             -Z function-contracts
             -Z mem-predicates

crates/ffwd-core/Cargo.toml

@@ -5,6 +5,11 @@ edition.workspace = true
 rust-version.workspace = true
 publish = false
 
+[features]
+# Gate expensive Kani proofs (>30s solver time) so PR CI stays fast.
+# Push-to-main and nightly runs use --features kani-slow to verify everything.
+kani-slow = []
+
 [lib]
 doctest = false
 

crates/ffwd-core/src/cri.rs

@@ -893,6 +893,9 @@ mod verification {
     }
 
     /// Prove the configurable plain-text field wrapper path never panics.
+    ///
+    /// Gated behind `kani-slow`: [u8; 48] symbolic + unwind 52 takes >60s.
+    #[cfg(feature = "kani-slow")]
     #[kani::proof]
     #[kani::unwind(52)]
     #[kani::solver(kissat)]
@@ -1128,6 +1131,9 @@ mod verification {
     ///   - verify_write_json_line_no_prefix_quote_escape
     ///   - verify_write_json_line_no_prefix_backslash_escape
     ///   - verify_write_json_line_no_prefix_control_escape
+    ///
+    /// Gated behind `kani-slow`: unwind 52 through JSON escaping takes >30s.
+    #[cfg(feature = "kani-slow")]
     #[kani::proof]
     #[kani::unwind(52)]
     fn verify_write_json_line_parametric() {
@@ -1228,19 +1234,24 @@ mod verification {
     }
 
     /// Oracle equivalence: `json_escape_bytes` matches `ffwd_kani::bytes::json_escape_oracle`
-    /// for all byte-slice inputs of length at most 16.
+    /// for all byte-slice inputs of length at most 8.
     ///
     /// # Oracle Design Note
     /// The oracle is a golden copy (see `ffwd_kani::bytes::json_escape_oracle` docs).
     /// This proof provides no-panic and output-bound guarantees, but would not detect
     /// shared logic bugs in both implementations.
+    /// Bounded to 8 bytes (from 16) to keep solver under 30s. Each byte can
+    /// expand to 6 chars (\uXXXX), so worst case = 48 output bytes.
+    ///
+    /// Gated behind `kani-slow`: [u8; 8] + unwind 50 through escape logic ~30s.
+    #[cfg(feature = "kani-slow")]
     #[kani::proof]
-    #[kani::unwind(100)]
+    #[kani::unwind(50)]
     pub(super) fn verify_json_escape_bytes_vs_oracle() {
-        let src: [u8; 16] = kani::any();
-        let len: usize = kani::any_where(|&l| l <= 16);
+        let src: [u8; 8] = kani::any();
+        let len: usize = kani::any_where(|&l| l <= 8);
 
-        let mut prod_dst = Vec::with_capacity(16 * 6);
+        let mut prod_dst = Vec::with_capacity(8 * 6);
         let ora_result = json_escape_oracle(&src[..len]);
         json_escape_bytes(&src[..len], &mut prod_dst);
 

crates/ffwd-core/src/framer.rs

@@ -200,6 +200,9 @@ mod verification {
     }
 
     /// Prove NewlineFramer line ranges are valid sub-ranges of input.
+    ///
+    /// Gated behind `kani-slow`: [u8; 32] symbolic + unwind 34 + kissat takes >30s.
+    #[cfg(feature = "kani-slow")]
     #[kani::solver(kissat)]
     #[kani::proof]
     #[kani::unwind(34)]

crates/ffwd-core/src/json_scanner.rs

@@ -2621,6 +2621,9 @@ mod verification {
 
     /// next_quote on a single block: if found, the position has a set bit
     /// in the bitmask. If not found, no bits are set in [from, end).
+    ///
+    /// Gated behind `kani-slow`: symbolic u64 bitmask + 66-unwind takes >30s.
+    #[cfg(feature = "kani-slow")]
     #[kani::proof]
     #[kani::unwind(66)] // inner None-branch loop: up to 64 iterations (end≤64) + 2 margin
     #[kani::solver(kissat)]

crates/ffwd-core/src/otlp.rs

@@ -1531,6 +1531,10 @@ mod verification {
     /// Prove parse_severity ONLY returns non-Unspecified for the 10
     /// recognized level strings (6 standard + 4 aliases, any case).
     /// No false positives.
+    ///
+    /// Gated behind `kani-slow`: 10 case-insensitive comparisons over
+    /// symbolic [u8; 8] takes ~59s in the solver.
+    #[cfg(feature = "kani-slow")]
     #[kani::proof]
     #[kani::unwind(9)] // eq_ignore_case_match: Zip over ≤8-byte targets + 1 terminator
     pub(super) fn verify_parse_severity_no_false_positives() {
@@ -1942,13 +1946,15 @@ mod verification {
     }
 
     /// Prove hex_decode rejects inputs where hex length != 2 * output length.
+    /// Uses a fixed-size stack array to avoid heap allocation (Vec) which
+    /// causes CBMC to spend 800s+ modeling the allocator.
     #[kani::proof]
+    #[kani::unwind(36)]
     fn verify_hex_decode_rejects_wrong_length() {
-        // Any length mismatch should return false
         let hex_len: usize = kani::any_where(|&l: &usize| l <= 34 && l != 32);
-        let hex = vec![b'a'; hex_len];
+        let hex = [b'a'; 34];
         let mut out = [0u8; 16];
-        assert!(!hex_decode(&hex, &mut out));
+        assert!(!hex_decode(&hex[..hex_len], &mut out));
     }
 
     // -----------------------------------------------------------------------
@@ -2151,19 +2157,22 @@ mod verification {
     /// then encode_varint for the length, then extends with the data slice.
     /// With the stub, tag and length each append 1-10 bytes, plus data_len
     /// bytes of payload.
+    /// Bounded to 4 data bytes (vs 8) to keep solver under 60s.
+    /// unwind(12) covers the stub's up-to-10-iteration loop (11 unwinds)
+    /// plus the data comparison and extend_from_slice loops.
     #[kani::proof]
     #[kani::stub(encode_varint, encode_varint_stub)]
     #[kani::unwind(12)]
     fn verify_encode_bytes_field_content_compositional() {
         let field_number: u32 = kani::any();
         kani::assume(field_number > 0 && field_number <= 100);
-        let data_len: usize = kani::any_where(|&l: &usize| l <= 8);
-        let data: [u8; 8] = kani::any();
+        let data_len: usize = kani::any_where(|&l: &usize| l <= 4);
+        let data: [u8; 4] = kani::any();
 
         let mut buf = Vec::new();
         encode_bytes_field(&mut buf, field_number, &data[..data_len]);
 
-        // Tag (1-10) + length varint (1-10) + data (0-8) = 2-28 bytes
+        // Tag (1-10) + length varint (1-10) + data (0-4) = 2-24 bytes
         assert!(buf.len() >= 2 + data_len && buf.len() <= 20 + data_len);
 
         // Last data_len bytes must be the exact input data
@@ -2237,6 +2246,9 @@ mod verification {
 
     /// Oracle equivalence: `skip_field` matches `ffwd_kani::proto::skip_field_oracle`
     /// for all bounded byte inputs and valid wire types, including the EOF boundary.
+    ///
+    /// Gated behind `kani-slow`: [u8; 32] symbolic + varint decode loops takes >30s.
+    #[cfg(feature = "kani-slow")]
     #[kani::proof]
     #[kani::unwind(22)]
     pub(super) fn verify_skip_field_vs_oracle() {
@@ -2277,6 +2289,9 @@ mod verification {
 
     /// No-panic proof: `skip_field` never panics for any bounded input and any wire type
     /// (including unsupported values).
+    ///
+    /// Gated behind `kani-slow`: [u8; 32] symbolic + unwind 36 takes >30s.
+    #[cfg(feature = "kani-slow")]
     #[kani::proof]
     #[kani::unwind(36)]
     pub(super) fn verify_skip_field_no_panic() {