tests: basic kani harnesses for Var and Lit

.github/workflows/rustsat.yml

@@ -52,3 +52,16 @@ jobs:
           curl -O https://media.christophjabs.info/gimsatul-1-1-2
           chmod +x gimsatul-1-1-2
           RS_EXT_SOLVER=./gimsatul-1-1-2 cargo test --test external_solver --verbose -- --ignored
+
+  kani:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
+        with:
+          submodules: "recursive"
+      - name: Cargo kani
+        uses: model-checking/kani-github-action@v1
+        with:
+          args: '-p rustsat'
+

Cargo.toml

@@ -102,3 +102,6 @@ name = "print-lits"
 [profile.profiling]
 inherits = "release"
 debug = 1
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

src/types.rs

@@ -60,7 +60,7 @@ impl Var {
     /// If `idx > Var::MAX_IDX`.
     #[must_use]
     pub fn new(idx: u32) -> Var {
-        assert!(idx < Var::MAX_IDX, "variable index too high");
+        assert!(idx <= Var::MAX_IDX, "variable index too high");
         Var { idx }
     }
 
@@ -259,6 +259,15 @@ impl fmt::Debug for Var {
     }
 }
 
+#[cfg(kani)]
+impl kani::Arbitrary for Var {
+    fn any() -> Self {
+        let idx = u32::any();
+        kani::assume(idx <= Var::MAX_IDX);
+        Var::new(idx)
+    }
+}
+
 /// More easily creates variables. Mainly used in tests.
 ///
 /// # Examples
@@ -574,6 +583,14 @@ impl fmt::Debug for Lit {
     }
 }
 
+#[cfg(kani)]
+impl kani::Arbitrary for Lit {
+    fn any() -> Self {
+        let var = Var::any();
+        var.lit(bool::any())
+    }
+}
+
 /// More easily creates literals. Mainly used in tests.
 ///
 /// # Examples
@@ -1224,3 +1241,20 @@ mod tests {
         assert_eq!(res, ground_truth);
     }
 }
+
+#[cfg(kani)]
+mod proofs {
+    #[kani::proof]
+    fn pos_lit() {
+        let var: super::Var = kani::any();
+        let lit = var.pos_lit();
+        assert_eq!(var, lit.var());
+    }
+
+    #[kani::proof]
+    fn neg_lit() {
+        let var: super::Var = kani::any();
+        let lit = var.neg_lit();
+        assert_eq!(var, lit.var());
+    }
+}