formal(P-037): harnesses draw small-width symbolic inputs (u8 indices, guards < 3) so CBMC stops bit-blasting 64-bit fields

The first full Kani run spent minutes on the election solver harness with
symbolic usize callee indices and schedules; the harnesses now build
systems from u8 symbols through properties::symbolic (any_system,
any_election_system, any_schedule, any_index) and assume well-formedness.
Kernel types untouched; cargo test 35 passed; clippy clean.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QfeUtLRm6KFRWcTGQZxQQb

Author: claude

formal/p037-kernel/src/properties/election.rs

@@ -151,7 +151,8 @@ mod tests {
 
 #[cfg(kani)]
 mod proofs {
-    use crate::{elect, elect_with, import, Election, ElectionSystem, GuardBinding, MAX_COORDS};
+    use super::super::symbolic::{any_election_system, any_schedule};
+    use crate::{elect, elect_with, import, Election, GuardBinding};
 
     #[kani::proof]
     fn k4_import_is_monotone_and_conflict_propagates() {
@@ -168,11 +169,8 @@ mod proofs {
     #[kani::proof]
     #[kani::unwind(9)]
     fn k10_election_lfp_is_schedule_independent() {
-        let sys: ElectionSystem = kani::any();
-        kani::assume(sys.n >= 1 && sys.n <= MAX_COORDS && sys.well_formed());
-        let sched: [usize; MAX_COORDS] = kani::any();
-        kani::assume(sched.iter().all(|&i| i < sys.n));
-        kani::assume((0..sys.n).all(|i| sched.contains(&i)));
+        let sys = any_election_system();
+        let sched = any_schedule(sys.n);
         let jacobi = elect(&sys);
         assert!(jacobi.is_some(), "terminates within the height bound");
         assert_eq!(elect_with(&sys, &sched), jacobi);

formal/p037-kernel/src/properties/mod.rs

@@ -277,6 +277,121 @@ pub fn random_election_system(rng: &mut Rng, n: usize) -> ElectionSystem {
     ElectionSystem { n, coords }
 }
 
+/// Small-width symbolic inputs for the Kani harnesses.
+///
+/// CBMC bit-blasts every field, so a symbolic `usize` index costs 64 bits
+/// where two would do. The harnesses draw `u8` symbols, convert, and assume
+/// well-formedness — the kernel types are untouched.
+#[cfg(kani)]
+pub mod symbolic {
+    use super::DEAD;
+    use crate::{
+        Coord, Edge, Election, ElectionCoord, ElectionEdge, ElectionSystem, Guard, GuardBinding,
+        Shape, System, MAX_COORDS, MAX_EDGES,
+    };
+
+    /// A symbolic index below `n`.
+    pub fn any_index(n: usize) -> usize {
+        let v: u8 = kani::any();
+        kani::assume(usize::from(v) < n);
+        usize::from(v)
+    }
+
+    /// A guard index below 3.
+    fn any_guard() -> Guard {
+        let g: Guard = kani::any();
+        kani::assume(g < 3);
+        g
+    }
+
+    fn any_edge(n: usize) -> Option<Edge> {
+        let present: bool = kani::any();
+        present.then(|| Edge {
+            callee: any_index(n),
+            transform: kani::any(),
+            mask: kani::any(),
+        })
+    }
+
+    /// A well-formed system of 1..=3 coordinates with up to 2 edges each.
+    pub fn any_system() -> System {
+        let n = any_index(MAX_COORDS).saturating_add(1);
+        let mut coords = [DEAD; MAX_COORDS];
+        for c in coords.iter_mut().take(n) {
+            let split: bool = kani::any();
+            *c = Coord {
+                shape: if split {
+                    Shape::Split(0)
+                } else {
+                    Shape::Uncond
+                },
+                seed: kani::any(),
+                edges: [any_edge(n), any_edge(n)],
+            };
+        }
+        let sys = System { n, coords };
+        kani::assume(sys.well_formed());
+        sys
+    }
+
+    /// A fair per-pass schedule over `0..n`.
+    pub fn any_schedule(n: usize) -> [usize; MAX_COORDS] {
+        let s = [any_index(n), any_index(n), any_index(n)];
+        kani::assume((0..n).all(|i| s.contains(&i)));
+        s
+    }
+
+    fn any_election() -> Election {
+        match any_index(3) {
+            0 => Election::None,
+            1 => Election::One(any_guard()),
+            _ => Election::Conflict,
+        }
+    }
+
+    fn any_binding() -> GuardBinding {
+        match any_index(4) {
+            0 => GuardBinding::Const,
+            1 => GuardBinding::Opaque,
+            2 => GuardBinding::Id {
+                callee: any_guard(),
+                caller: any_guard(),
+            },
+            _ => GuardBinding::Neg {
+                callee: any_guard(),
+                caller: any_guard(),
+            },
+        }
+    }
+
+    fn any_election_edge(n: usize) -> Option<ElectionEdge> {
+        let present: bool = kani::any();
+        present.then(|| ElectionEdge {
+            callee: any_index(n),
+            binding: any_binding(),
+        })
+    }
+
+    /// A well-formed election system of 1..=3 coordinates.
+    pub fn any_election_system() -> ElectionSystem {
+        let n = any_index(MAX_COORDS).saturating_add(1);
+        let dead = ElectionCoord {
+            seed: Election::None,
+            edges: [None; MAX_EDGES],
+        };
+        let mut coords = [dead; MAX_COORDS];
+        for c in coords.iter_mut().take(n) {
+            *c = ElectionCoord {
+                seed: any_election(),
+                edges: [any_election_edge(n), any_election_edge(n)],
+            };
+        }
+        let sys = ElectionSystem { n, coords };
+        kani::assume(sys.well_formed());
+        sys
+    }
+}
+
 /// All permutations of `0..n` for `n ≤ 3`.
 #[must_use]
 pub fn permutations(n: usize) -> Vec<Vec<usize>> {

formal/p037-kernel/src/properties/refinement.rs

@@ -202,10 +202,9 @@ mod tests {
 
 #[cfg(kani)]
 mod proofs {
+    use super::super::symbolic::{any_index, any_system};
     use super::{no_unknown_seed, release_cells_have_no_edges};
-    use crate::{
-        lemma_guarded, lemma_today, solve, Cells, Grounding, System, Transfer, MAX_COORDS,
-    };
+    use crate::{lemma_guarded, lemma_today, solve, Cells, Grounding, Transfer, MAX_COORDS};
 
     #[kani::proof]
     fn k9_residual_bottom_lemma_all_three_groundings() {
@@ -218,8 +217,7 @@ mod proofs {
 
     #[kani::proof]
     fn k11_one_step_lax_simulation() {
-        let sys: System = kani::any();
-        kani::assume(sys.n >= 1 && sys.n <= MAX_COORDS && sys.well_formed());
+        let sys = any_system();
         let x: [Cells; MAX_COORDS] = kani::any();
         let [x0, x1, x2] = x;
         let cx = [
@@ -228,16 +226,14 @@ mod proofs {
             Cells::diag(x2.collapse()),
         ];
         let c = sys.collapsed();
-        let i: usize = kani::any();
-        kani::assume(i < sys.n);
+        let i = any_index(sys.n);
         assert!(sys.step(i, &x).collapse().leq(c.step(i, &cx).collapse()));
     }
 
     #[kani::proof]
     #[kani::unwind(21)]
     fn k11_lfp_lax_simulation_against_the_collapsed_system() {
-        let sys: System = kani::any();
-        kani::assume(sys.n >= 1 && sys.n <= MAX_COORDS && sys.well_formed());
+        let sys = any_system();
         let g = solve(&sys);
         let t = solve(&sys.collapsed());
         assert!(g.is_some() && t.is_some());
@@ -251,8 +247,7 @@ mod proofs {
     #[kani::proof]
     #[kani::unwind(21)]
     fn k11_lfp_lax_simulation_against_today_post_finalization() {
-        let sys: System = kani::any();
-        kani::assume(sys.n >= 1 && sys.n <= MAX_COORDS && sys.well_formed());
+        let sys = any_system();
         kani::assume(release_cells_have_no_edges(&sys) && no_unknown_seed(&sys));
         let g = solve(&sys);
         let t = solve(&sys.today());

formal/p037-kernel/src/properties/solver.rs

@@ -52,16 +52,14 @@ mod tests {
 
 #[cfg(kani)]
 mod proofs {
-    use crate::{solve, solve_with, System, MAX_COORDS};
+    use super::super::symbolic::{any_schedule, any_system};
+    use crate::{solve, solve_with};
 
     #[kani::proof]
     #[kani::unwind(21)]
     fn k10_lfp_is_a_schedule_independent_fixpoint() {
-        let sys: System = kani::any();
-        kani::assume(sys.n >= 1 && sys.n <= MAX_COORDS && sys.well_formed());
-        let sched: [usize; MAX_COORDS] = kani::any();
-        kani::assume(sched.iter().all(|&i| i < sys.n));
-        kani::assume((0..sys.n).all(|i| sched.contains(&i)));
+        let sys = any_system();
+        let sched = any_schedule(sys.n);
         let lfp = solve(&sys);
         assert!(lfp.is_some(), "terminates within the height bound");
         if let Some(x) = lfp {

formal/p037-kernel/src/properties/transforms.rs

@@ -85,7 +85,8 @@ mod tests {
 
 #[cfg(kani)]
 mod proofs {
-    use crate::{contribute, read, solve, Cells, Mask, Shape, System, Transform, MAX_COORDS};
+    use super::super::symbolic::any_system;
+    use crate::{contribute, read, solve, Cells, Mask, Shape, Transform};
 
     #[kani::proof]
     fn k3_reads_and_contributions_are_monotone() {
@@ -115,8 +116,7 @@ mod proofs {
     #[kani::proof]
     #[kani::unwind(21)]
     fn k12_uncond_coordinates_stay_diagonal() {
-        let sys: System = kani::any();
-        kani::assume(sys.n >= 1 && sys.n <= MAX_COORDS && sys.well_formed());
+        let sys = any_system();
         let x = solve(&sys);
         assert!(x.is_some(), "terminates within the height bound");
         if let Some(x) = x {