revert to a fixed version of the original

the version pulled in from the paper gave completely different results

examples/eq_paper.rs

@@ -2,8 +2,8 @@
 #![no_main]
 #![no_std]
 
-extern crate klee;
 extern crate panic_abort;
+extern crate klee;
 use klee::{kassert, kassume, ksymbol};
 
 #[derive(Debug, Copy, Clone)]
@@ -33,79 +33,85 @@ const F: bool = false;
 
 #[no_mangle]
 fn main() {
-  let mut DATA: [Data; HORIZON] =
-    unsafe { core::mem::uninitialized() };
+  let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
   ksymbol!(&mut DATA, "DATA");
 
-  let mut STATE = S8001;
-  let mut STATE_H: [State; HORIZON] =
-    unsafe { core::mem::uninitialized() }; // STATE_HISTORY
-  let mut CNTR: u32 =
-    unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR
+  let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
 
-  // TIMEOUT_CNTR_HISTORY
-  let mut CNTR_H: [u32; HORIZON] =
-    unsafe { core::mem::uninitialized() };
+  let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
 
-  for i in 0..HORIZON {
-    eq(&mut STATE, &mut CNTR, &mut DATA[i]);
+  let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+  let mut STATE = S8001;
 
-    STATE_H[i] = STATE; // update STATE history
-    CNTR_H[i] = CNTR; // update CNTR history
+  for i in 0..HORIZON {
+    eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
+    STATE_H[i] = STATE;
+    CNTR_H[i] = TIMEOUT_CNTR;
+
+    // invariants
+    // (1) S8000 -> a & b
+    // ensures that Enable implies that both a and b are true
+    // this is the main safety condition
+    if STATE == S8000 {
+      kassert!(DATA[i].a & DATA[i].b);
+    }
 
-    // (1) !a | !b -> !S8000
+    // (2) !a | !b -> !S8000
+    // ensures that if any input is false we cannot enter the Enable state
+    // this can also be seen as a safty condition
+    // (can it be derived from the first condition, but we keep is as
+    // an indication that the verification works as expected)
+    // Indeed the number of spanned paths remains the same
+    // (with or without the below assertion, so its proven redundant by KLEE)
     if !DATA[i].a | !DATA[i].b {
       kassert!(!(STATE == S8000));
     }
 
-    // (2) S8000 -> a & b
-    if STATE == S8000 {
-      kassert!(DATA[i].a & DATA[i].b);
+    // S8001 -> !a & !b
+    // we can only stay or enter the Init state unless either (or both) inputs are false
+    if STATE == S8001 {
+      kassert!(!DATA[i].a | !DATA[i].b);
     }
 
+    // transition invariants
     if i > 0 {
       match STATE_H[i - 1] {
-        // (3)
         C001 | C002 | C003 => {
-          kassert!(
-            (STATE == S8001)
-              | (STATE == STATE_H[i - 1])
-          );
+          // (3)
+          // transitions from error
+          kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
         }
-        // (4)
         S8005 => {
-          kassert!(
-            (STATE == S8001)
-              | (STATE == C003)
-              | (STATE == STATE_H[i - 1])
-          );
+            // (4)
+          kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
         }
         _ => (),
       }
     }
 
+    // // DISCREPANCY related invariants
     match STATE {
+      // Error -> timeout
       // (5)
-      C001 | C002 | C003 => kassert!(CNTR == 0),
+      C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
 
       S8004 | S8005 | S8014 => {
         // (6)
+        // remaining in a waiting state decreases the counter
         if i > 0 {
-          if STATE_H[i - 1] == STATE {
-            kassert!(CNTR_H[i] < CNTR_H[i - 1]);
+          if STATE_H[i - 1] == STATE_H[i] {
+            kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
           }
         }
       }
       _ => {}
     }
+
+    unsafe { core::ptr::read_volatile(&STATE_H[i]) };
   }
 }
 
-fn eq(
-  STATE: &mut State,
-  TIMEOUT_CNTR: &mut u32,
-  data: &Data,
-) {
+fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
   *STATE = match STATE {
     S8000 => match (data.a, data.b) {
       (F, F) => S8001,