match the code from the paper exactly

examples/eq_paper.rs

 #![allow(non_snake_case)]
 #![no_main]
+#![no_std]
 
+
+extern crate panic_abort;
 extern crate klee;
 use klee::{kassert, kassume, ksymbol};
 
@@ -34,109 +37,67 @@ fn main() {
   let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
   ksymbol!(&mut DATA, "DATA");
 
-  let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
-
-  let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
-
-  let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
   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
+  // TIMEOUT_CNTR_HISTORY
+  let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
 
   for i in 0..HORIZON {
-    periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
-    STATE_H[i] = STATE;
-    CNTR_H[i] = TIMEOUT_CNTR;
-
-    // invariants
-    // 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);
-    }
+    eq(&mut STATE, &mut CNTR, &mut DATA[i]);
+
+    STATE_H[i] = STATE; // update STATE history
+    CNTR_H[i] = CNTR; // update CNTR history
 
-    // !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)
+    // (1) !a | !b -> !S8000
     if !DATA[i].a | !DATA[i].b {
       kassert!(!(STATE == S8000));
     }
     
-    // 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);
+    // (2) S8000 -> a & b
+    if STATE == S8000 {
+      kassert!(DATA[i].a & DATA[i].b);
     }
     
-    // transition invariants
     if i > 0 {
       match STATE_H[i - 1] {
+        // (3)
         C001 | C002 | C003 => {
-          // transitions from error
-          kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+          kassert!(
+              (STATE == S8001) 
+            | (STATE == STATE_H[i - 1])
+          );
         }
+        // (4)
         S8005 => {
-          kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
+          kassert!(
+            (STATE == S8001) 
+          | (STATE == C003) 
+          | (STATE == STATE_H[i - 1])
+          );
         }
         _ => (),
       }
     }
 
-    // // DISCREPANCY related invariants
     match STATE {
-      // Error -> timeout
-      C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+      // (5)
+      C001 | C002 | C003 => kassert!(CNTR == 0),
 
       S8004 | S8005 | S8014 => {
-        // // remaining in a waiting state decreases the counter
+        // (6)
         if i > 0 {
-          if STATE_H[i - 1] == STATE_H[i] {
-            kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
+          if STATE_H[i - 1] == STATE {
+            kassert!(CNTR_H[i] < CNTR_H[i - 1]);
           }
         }
-        // // Waiting states -> !timeout
-        // // Waiting states implies that TIMEOUT_CNTR has not yet expired
-        // // and that the time remaining is not longer than the DISCREPANCY
-        //   kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
-        // kassert!(TIMEOUT_CNTR <= DISCREPANCY);
       }
       _ => {}
     }
+  }
+}
 
-    // // liveness?
-    // if i == HORIZON - 1 {
-    //   let mut ok = false;
-    //   for j in 0..=i {
-    //     if STATE_H[j] == S8001 {
-    //       ok = true;
-    //     }
-    //   }
-    //   kassert!(ok);
-    // }
-
-    // if i > 0 {
-    //   match STATE_H[i - 1] {
-    //     C001 | C002 | C003 | S8005 => {
-    //       // no (immediate) transition from error / recover to Enable state
-    //       kassert!(!(STATE == S8000));
-    //     }
-    //     _ => {
-    //       // liveness from Init and Wait states, Enable is ensured
-    //       if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
-    //         kassert!(STATE == S8000);
-    //       }
-    //     }
-    //   }
-    // }
-
-    unsafe { core::ptr::read_volatile(&STATE_H[i]) };
-  }
-}
-
-fn periodic(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,