test(fv): Add target programs for quantifiers feat

test_programs/formal_verify_failure/exists_big_element_sum/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "exists_big_element_sum"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]

test_programs/formal_verify_failure/exists_big_element_sum/src/main.nr

@@ -0,0 +1,10 @@
+#[requires(exists(|i| 0 <= i < 20 & arr[i] > 100))]
+#[ensures(result > 100)] // We require that an element bigger than 100 exists in the array.
+// Therefore we expect the sum to be bigger than 100.
+fn main(arr: [u16; 20]) -> pub u64 {
+    let mut sum: u64 = 0;
+    for i in 0..20 {
+        sum += arr[i] as u64;
+    }
+    sum
+}

test_programs/formal_verify_failure/exists_zero_in_array/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "exists_zero_in_array"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]

test_programs/formal_verify_failure/exists_zero_in_array/src/main.nr

@@ -0,0 +1,9 @@
+#[requires(exists(|i| (0 <= i < 7) & (arr[i] == 0) ) )]
+#[ensures(result == 0)]
+fn main(arr: [u8; 7]) -> pub u64 {
+    let mut mul: u64 = 0;
+    for i in 0..7 {
+        mul *= arr[i] as u64;
+    }
+    mul
+}

test_programs/formal_verify_failure/forall_max_is_max/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "forall_max_is_max"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]

test_programs/formal_verify_failure/forall_max_is_max/src/main.nr

@@ -0,0 +1,5 @@
+#[requires(forall(|i, j| 0 <= i < j < 15 ==> v[i] <= v[j]))]
+#[ensures(forall(|i| 0 <= i < 15 ==> v[i] <= result))]
+fn main(v: [u64; 15], k: u64) -> pub u64 {
+    v[14] // The array is sorted and this is the last element, therefore it's the maximum element.  
+}

test_programs/formal_verify_failure/forall_sum_of_evens/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "forall_sum_of_evens"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]

test_programs/formal_verify_failure/forall_sum_of_evens/src/main.nr

@@ -0,0 +1,12 @@
+#[requires(forall(|i| 0 <= i < 10 ==> arr[i] % 2 == 0) 
+            & forall(|i| 0 <= i < 10 ==> arr[i] < 100) )]
+#[ensures((result % 2 == 0) & (result < 1000))]
+// The sum of an array which constist of even elements upper bounded by 100
+// will be even and upper bounded by 1000
+fn foo(arr: [u32; 10]) -> pub u32 {
+    let mut sum = 0;
+    for i in 0..10 {
+        sum += arr[i];
+    }
+    sum
+}