Exposing vector_add to zok frontend

scripts/zx_tests/vadd_u16.zx

@@ -0,0 +1,7 @@
+from "EMBED" import vadd_u16
+
+def main() -> u16[5]:
+    u16[5] a = [1, 2, 3, 4, 5]
+    u16[5] b = [2, 3, 4, 5, 6]
+    assert(vadd_u16(a, b) == [3, 5, 7, 9, 11])
+    return vadd_u16(a,b)

scripts/zx_tests/vadd_u32.zx

@@ -0,0 +1,7 @@
+from "EMBED" import vadd_u32
+
+def main() -> u32[5]:
+    u32[5] a = [1, 2, 3, 4, 5]
+    u32[5] b = [2, 3, 4, 5, 6]
+    assert(vadd_u32(a, b) == [3, 5, 7, 9, 11])
+    return vadd_u32(a,b)

scripts/zx_tests/vadd_u32.zxf

@@ -0,0 +1,6 @@
+from "EMBED" import vadd_u32
+
+def main() -> u32[5]:
+    u32[5] a = [1, 2, 3, 4, 5]
+    u32[5] b = []
+    return vadd_u32(a,b)

scripts/zx_tests/vadd_u64.zx

@@ -0,0 +1,7 @@
+from "EMBED" import vadd_u64
+
+def main() -> u64[5]:
+    u64[5] a = [1, 2, 3, 4, 5]
+    u64[5] b = [2, 3, 4, 5, 6]
+    assert(vadd_u64(a, b) == [3, 5, 7, 9, 11])
+    return vadd_u64(a,b)

scripts/zx_tests/vadd_u8.zx

@@ -0,0 +1,7 @@
+from "EMBED" import vadd_u8
+
+def main() -> u8[5]:
+    u8[5] a = [1, 2, 3, 4, 5]
+    u8[5] b = [2, 3, 4, 5, 6]
+    assert(vadd_u8(a, b) == [3, 5, 7, 9, 11])
+    return vadd_u8(a,b)

src/front/zsharp/mod.rs

@@ -296,7 +296,7 @@ impl<'ast> ZGen<'ast> {
             "bit_array_le" => {
                 if args.len() != 2 {
                     Err(format!(
-                        "Got {} args to EMBED/bit_array_le, expected 1",
+                        "Got {} args to EMBED/bit_array_le, expected 2",
                         args.len()
                     ))
                 } else if generics.len() != 1 {
@@ -333,6 +333,24 @@ impl<'ast> ZGen<'ast> {
                     Ok(uint_lit(DFL_T.modulus().significant_bits(), 32))
                 }
             }
+            "vadd_u8" | "vadd_u16" | "vadd_u32" | "vadd_u64" => {
+                if args.len() != 2 {
+                    Err(format!(
+                        "Got {} args to EMBED/vadd_*, expected 2",
+                        args.len()
+                    ))
+                } else if generics.len() != 1 {
+                    Err(format!(
+                        "Got {} generic args to EMBED/vadd_*, expected 1",
+                        generics.len()
+                    ))
+                } else {
+                    assert!(args.iter().all(|t| matches!(t.type_(), Ty::Array(_, _))));
+                    let b = args.pop().unwrap();
+                    let a = args.pop().unwrap();
+                    vector_op(BV_ADD, a, b)
+                }
+            }
             _ => Err(format!("Unknown or unimplemented builtin '{}'", f_name)),
         }
     }
@@ -924,7 +942,6 @@ impl<'ast> ZGen<'ast> {
         } else {
             debug!("Expr: {}", e.span().as_str());
         }
-
         match e {
             ast::Expression::Ternary(u) => {
                 match self.expr_impl_::<true>(&u.first).ok().and_then(const_bool) {

src/front/zsharp/term.rs

@@ -908,6 +908,17 @@ pub fn bit_array_le(a: T, b: T, n: usize) -> Result<T, String> {
     ))
 }
 
+pub fn vector_op(op: Op, a: T, b: T) -> Result<T, String> {
+    match (a.ty, b.ty) {
+        (Ty::Array(a_s, a_ty), Ty::Array(b_s, b_ty)) => {
+            assert_eq!((a_s, a_ty.clone()), (b_s, b_ty));
+            let t = term![Op::Map(Box::new(op)); a.term, b.term];
+            Ok(T::new(Ty::Array(a_s, a_ty), t))
+        }
+        _ => Err("Cannot do vector_op on non-array types".to_string()),
+    }
+}
+
 pub struct ZSharp {
     values: Option<HashMap<String, Integer>>,
 }