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

@@ -268,7 +268,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 {
@@ -305,6 +305,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)),
         }
     }
@@ -891,7 +909,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,20 @@ 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)) => {
+            if a_s == b_s && a_ty == b_ty {
+                let t = term![Op::Map(Box::new(op)); a.term, b.term];
+                Ok(T::new(Ty::Array(a_s, a_ty), t))
+            } else {
+                panic!("Mismatched array types (this is a bug: type checking should have caught this!)");
+            }
+        }
+        _ => Err("Cannot do vector_op on non-array types".to_string()),
+    }
+}
+
 pub struct ZSharp {
     values: Option<HashMap<String, Integer>>,
 }

src/ir/opt/cfold.rs

@@ -244,6 +244,29 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache<Term>) -> Term {
                     b.width() + w,
                 ))))
             }),
+            Op::Map(op) => match (get(0).as_array_opt(), get(1).as_array_opt()) {
+                (Some(a), Some(b)) => {
+                    // TODO: extend for n-ary arrays
+                    let mut res = a.clone();
+                    let mut merge = ArrayMerge::new(a.clone(), b.clone());
+                    for (i, va, vb) in merge.into_iter() {
+                        let r = fold_cache(
+                            &term![*op.clone(); leaf_term(Op::Const(va.clone())), leaf_term(Op::Const(vb.clone()))],
+                            cache,
+                        );
+                        match r.as_value_opt() {
+                            Some(v) => {
+                                res = res.clone().store(i, v.clone());
+                            }
+                            None => {
+                                panic!("Unable to constant fold idx: {}", i);
+                            }
+                        }
+                    }
+                    Some(leaf_term(Op::Const(Value::Array(res))))
+                }
+                _ => None,
+            },
             _ => None,
         };
         let new_t = {

src/ir/term/mod.rs

@@ -29,8 +29,10 @@ use hashconsing::{HConsed, WHConsed};
 use lazy_static::lazy_static;
 use log::debug;
 use rug::Integer;
+use std::cmp::Ordering;
 use std::collections::BTreeMap;
 use std::fmt::{self, Debug, Display, Formatter};
+use std::iter::Peekable;
 use std::sync::{Arc, RwLock};
 
 pub mod bv;
@@ -721,6 +723,104 @@ impl Array {
         self.check_idx(idx);
         self.map.get(idx).unwrap_or(&*self.default).clone()
     }
+
+    /// Iter
+    pub fn into_iter(&self) -> std::collections::btree_map::IntoIter<Value, Value> {
+        self.map.clone().into_iter()
+    }
+}
+
+/// Merge two Array Iterators
+pub struct ArrayMerge {
+    left: Peekable<Box<std::collections::btree_map::IntoIter<Value, Value>>>,
+    right: Peekable<Box<std::collections::btree_map::IntoIter<Value, Value>>>,
+    left_dfl: Value,
+    right_dfl: Value,
+}
+
+impl ArrayMerge {
+    /// Create a new [ArrayMerge] from two [Array]s
+    pub fn new(a: Array, b: Array) -> Self {
+        if a.size != b.size {
+            panic!("IR Arrays have different lengths: {}, {}", a.size, b.size);
+        }
+        if a.key_sort != b.key_sort {
+            panic!(
+                "IR Arrays have different key sorts: {}, {}",
+                a.key_sort, b.key_sort
+            );
+        }
+        if a.default.sort() != b.default.sort() {
+            panic!(
+                "IR Arrays default values have different key sorts: {}, {}",
+                a.default.sort(),
+                b.default.sort()
+            );
+        }
+
+        Self {
+            left: Box::new(a.into_iter()).peekable(),
+            right: Box::new(b.into_iter()).peekable(),
+            left_dfl: *a.default,
+            right_dfl: *b.default,
+        }
+    }
+
+    /// Iter
+    pub fn into_iter(&mut self) -> Box<dyn Iterator<Item = (Value, Value, Value)>> {
+        let mut acc: Vec<(Value, Value, Value)> = Vec::new();
+        let mut next = self.next_();
+        while let Some(n) = next {
+            acc.push(n);
+            next = self.next_();
+        }
+        Box::new(acc.into_iter())
+    }
+
+    /// Next
+    pub fn next_(&mut self) -> Option<(Value, Value, Value)> {
+        let l_peek = self.left.peek();
+        let r_peek = self.right.peek();
+
+        let mut left_next = false;
+        let mut right_next = false;
+
+        let res = match (l_peek, r_peek) {
+            (Some((l_ind, l_val)), Some((r_ind, r_val))) => match l_ind.cmp(r_ind) {
+                Ordering::Less => {
+                    left_next = true;
+                    Some((l_ind.clone(), l_val.clone(), self.right_dfl.clone()))
+                }
+                Ordering::Greater => {
+                    right_next = true;
+                    Some((r_ind.clone(), self.left_dfl.clone(), r_val.clone()))
+                }
+                Ordering::Equal => {
+                    left_next = true;
+                    right_next = true;
+                    Some((l_ind.clone(), l_val.clone(), r_val.clone()))
+                }
+            },
+            (Some((l_ind, l_val)), None) => {
+                left_next = true;
+                Some((l_ind.clone(), l_val.clone(), self.right_dfl.clone()))
+            }
+            (None, Some((r_ind, r_val))) => {
+                right_next = true;
+                Some((r_ind.clone(), self.left_dfl.clone(), r_val.clone()))
+            }
+            (None, None) => None,
+        };
+
+        if left_next {
+            self.left.next();
+        }
+        if right_next {
+            self.right.next();
+        }
+
+        res
+    }
 }
 
 impl Display for Value {

third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok

@@ -75,3 +75,16 @@ def u16_to_u32(u16 i) -> u32:
 
 def u8_to_u16(u8 i) -> u16:
     return 0u16
+
+// vector functions
+def vadd_u8<N>(u8[N] a, u8[N] b) -> u8[N]:
+    return [0; N]
+
+def vadd_u16<N>(u16[N] a, u16[N] b) -> u16[N]:
+    return [0; N]
+
+def vadd_u32<N>(u32[N] a, u32[N] b) -> u32[N]:
+    return [0; N]
+
+def vadd_u64<N>(u64[N] a, u64[N] b) -> u64[N]:
+    return [0; N]