fix: cleanup

thomashart17 · Sep 7, 2023 · d45aae6 · d45aae6
1 parent 6b6cd61
commit d45aae6
Showing 1 changed file with 4 additions and 31 deletions.
diff --git a/src/rust-jobs/add/lib.rs b/src/rust-jobs/add/lib.rs
@@ -1,45 +1,18 @@
 // #[cfg(feature = "feature_no_std")]
 #![no_std]
 pub use sea;
-use sea::println;
 
 // Entry point for the proof
 #[no_mangle]
 pub extern "C" fn entrypt() {
     test_test1();
-    test_test2();
 }
 
 #[no_mangle]
 fn test_test1() {
-    println!("Hello, test1!");
-    let v = sea::nd_i32();
-    sea::assume(v >= 1);
-    let res = add(v, 7);
+    let mut x: i32 = sea::nd_i32();
+    sea::assume(x < 10);
+    x += 4;
 
-    if v > 0 {
-        sea::sassert!(res > 7);
-    } else {
-        sea::sassert!(res <= 7);
-    }
-}
-
-#[no_mangle]
-fn test_test2() {
-    println!("Hello, test2!");
-    let v = sea::nd_i32();
-    sea::assume(v >= 1);
-    let res = add(v, 8);
-
-    if v > 0 {
-        sea::sassert!(res > 8);
-    } else {
-        sea::sassert!(res <= 8);
-    }
-}
-
-// Function being verified
-#[no_mangle]
-fn add(x: i32, y: i32) -> i32 {
-    x + y
+    sea::sassert!(x < 14);
 }