diff --git a/Cargo.lock b/Cargo.lock index 36c286b18..8f4dadf82 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -103,9 +103,9 @@ checksum = "f771a5d1f5503f7f4279a30f3643d3421ba149848b89ecaaec0ea2acf04a5ac4" [[package]] name = "backtrace" -version = "0.3.64" +version = "0.3.65" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e121dee8023ce33ab248d9ce1493df03c3b38a659b240096fcbd7048ff9c31f" +checksum = "11a17d453482a265fd5f8479f2a3f405566e6ca627837aaddb85af8b1ab8ef61" dependencies = [ "addr2line", "cc", @@ -138,7 +138,7 @@ dependencies = [ "log", "num_cpus", "pairing", - "rand_core 0.6.3", + "rand_core", "rayon", "subtle", ] @@ -211,7 +211,7 @@ dependencies = [ "ff", "group", "pairing", - "rand_core 0.6.3", + "rand_core", "subtle", ] @@ -433,7 +433,7 @@ checksum = "aa4da3c766cd7a0db8242e326e9e4e081edd567072893ed320008189715366a4" dependencies = [ "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", "synstructure", ] @@ -461,7 +461,7 @@ dependencies = [ "bitvec", "byteorder", "ff_derive 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)", - "rand_core 0.6.3", + "rand_core", "subtle", ] @@ -474,7 +474,7 @@ dependencies = [ "num-traits", "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] @@ -489,7 +489,7 @@ dependencies = [ "num-traits", "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] @@ -503,7 +503,7 @@ dependencies = [ "num-traits", "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] @@ -598,7 +598,7 @@ checksum = "bc5ac374b108929de78460075f3dc439fa66df9d8fc77e8f12caa5165fcf0c89" dependencies = [ "byteorder", "ff", - "rand_core 0.6.3", + "rand_core", "subtle", ] @@ -653,12 +653,12 @@ checksum = "9007da9cacbd3e6343da136e98b0d2df013f553d35bdec8b518f07bea768e19c" [[package]] name = "im" -version = "15.0.0" +version = "15.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "111c1983f3c5bb72732df25cddacee9b546d08325fb584b5ebd38148be7b0246" +checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9" dependencies = [ "bitmaps", - "rand_core 0.5.1", + "rand_core", "rand_xoshiro", "sized-chunks", "typenum", @@ -722,9 +722,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.123" +version = "0.2.125" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb691a747a7ab48abc15c5b42066eaafde10dc427e3b6ee2a1cf43db04c763bd" +checksum = "5916d2ae698f6de9bfb891ad7a8d65c09d232dc58cc4ac433c7da3b2fd84bc2b" [[package]] name = "log" @@ -755,7 +755,7 @@ dependencies = [ "proc-macro2 1.0.37", "quote 1.0.18", "regex-syntax", - "syn 1.0.91", + "syn 1.0.92", "utf8-ranges", ] @@ -801,12 +801,11 @@ dependencies = [ [[package]] name = "miniz_oxide" -version = "0.4.4" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a92518e98c078586bc6c934028adcca4c92a53d6a958196de835170a01d84e4b" +checksum = "d2b29bd4bc3f33391105ebee3589c19197c4271e3e5a9ec9bfe8127eeff8f082" dependencies = [ "adler", - "autocfg", ] [[package]] @@ -851,9 +850,9 @@ dependencies = [ [[package]] name = "object" -version = "0.27.1" +version = "0.28.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67ac1d3f9a1d3616fd9a60c8d74296f22406a238b6a72f5cc1e6f314df4ffbf9" +checksum = "40bec70ba014595f99f7aa110b84331ffe1ee9aece7fe6f387cc7e3ecda4d456" dependencies = [ "memchr", ] @@ -927,7 +926,7 @@ dependencies = [ "pest_meta", "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] @@ -966,7 +965,7 @@ dependencies = [ "proc-macro-error-attr", "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", "version_check", ] @@ -1018,7 +1017,7 @@ checksum = "b22a693222d716a9587786f37ac3f6b4faedb5b80c23914e7303ff5a1d8016e9" dependencies = [ "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] @@ -1053,7 +1052,7 @@ checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" dependencies = [ "libc", "rand_chacha", - "rand_core 0.6.3", + "rand_core", ] [[package]] @@ -1063,15 +1062,9 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" dependencies = [ "ppv-lite86", - "rand_core 0.6.3", + "rand_core", ] -[[package]] -name = "rand_core" -version = "0.5.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "90bde5296fc891b0cef12a6d03ddccc162ce7b2aff54160af9338f8d40df6d19" - [[package]] name = "rand_core" version = "0.6.3" @@ -1083,11 +1076,11 @@ dependencies = [ [[package]] name = "rand_xoshiro" -version = "0.4.0" +version = "0.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a9fcdd2e881d02f1d9390ae47ad8e5696a9e4be7b547a1da2afbc61973217004" +checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa" dependencies = [ - "rand_core 0.5.1", + "rand_core", ] [[package]] @@ -1160,9 +1153,9 @@ dependencies = [ [[package]] name = "rug" -version = "1.15.0" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ac804305677221f4c82469fd7eb8bfe00dd01420aa191197cb87d738520feef" +checksum = "f829d980ca193fa33fdd1decaebe72ec07cf2d8afdd0be60b3e5391f18014c91" dependencies = [ "az", "gmp-mpfr-sys", @@ -1204,7 +1197,7 @@ checksum = "08597e7152fcd306f41838ed3e37be9eaeed2b61c42e2117266a554fab4662f9" dependencies = [ "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] @@ -1276,7 +1269,7 @@ dependencies = [ "proc-macro-error", "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] @@ -1298,9 +1291,9 @@ dependencies = [ [[package]] name = "syn" -version = "1.0.91" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b683b2b825c8eef438b77c36a06dc262294da3d5a5813fac20da149241dcd44d" +checksum = "7ff7c592601f11445996a06f8ad0c27f094a58857c2f89e97974ab9235b92c52" dependencies = [ "proc-macro2 1.0.37", "quote 1.0.18", @@ -1315,7 +1308,7 @@ checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f" dependencies = [ "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", "unicode-xid 0.2.2", ] @@ -1374,7 +1367,7 @@ checksum = "aa32fd3f627f367fe16f893e2597ae3c05020f8bba2666a4e6ea73d377e5714b" dependencies = [ "proc-macro2 1.0.37", "quote 1.0.18", - "syn 1.0.91", + "syn 1.0.92", ] [[package]] diff --git a/scripts/zx_tests/vadd_u16.zx b/scripts/zx_tests/vadd_u16.zx new file mode 100644 index 000000000..6e7328f9e --- /dev/null +++ b/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) diff --git a/scripts/zx_tests/vadd_u32.zx b/scripts/zx_tests/vadd_u32.zx new file mode 100644 index 000000000..afeb9ea20 --- /dev/null +++ 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) diff --git a/scripts/zx_tests/vadd_u32.zxf b/scripts/zx_tests/vadd_u32.zxf new file mode 100644 index 000000000..22b985fbd --- /dev/null +++ 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) diff --git a/scripts/zx_tests/vadd_u64.zx b/scripts/zx_tests/vadd_u64.zx new file mode 100644 index 000000000..33e615984 --- /dev/null +++ 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) diff --git a/scripts/zx_tests/vadd_u8.zx b/scripts/zx_tests/vadd_u8.zx new file mode 100644 index 000000000..71bfaab78 --- /dev/null +++ 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) diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index b0cde48eb..d2654dd66 100644 --- a/src/front/zsharp/mod.rs +++ 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_::(&u.first).ok().and_then(const_bool) { diff --git a/src/front/zsharp/term.rs b/src/front/zsharp/term.rs index 4b5c66c1d..ebbac75b6 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -908,6 +908,17 @@ pub fn bit_array_le(a: T, b: T, n: usize) -> Result { )) } +pub fn vector_op(op: Op, a: T, b: T) -> Result { + 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>, } diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index 99a1e649f..b7e8f5fc0 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -266,6 +266,36 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> Term { b.width() + w, )))) }), + Op::Map(op) => { + assert!(t.cs.len() == 2); // TODO: extend for n-ary arrays + match (get(0).as_array_opt(), get(1).as_array_opt()) { + (Some(a), Some(b)) => { + let mut res = Array::new( + a.key_sort.clone(), + a.default.clone(), + Default::default(), + a.size, + ); + let merge = ArrayMerge::new(a, b); + for (i, va, vb) in merge { + 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.store(i.clone(), v.clone()); + } + None => { + panic!("Unable to constant fold idx: {}", i); + } + } + } + Some(leaf_term(Op::Const(Value::Array(res)))) + } + _ => None, + } + } _ => None, }; let new_t = { diff --git a/src/ir/term/mod.rs b/src/ir/term/mod.rs index 37b7b46cc..7596ea65a 100644 --- a/src/ir/term/mod.rs +++ b/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,84 @@ impl Array { self.check_idx(idx); self.map.get(idx).unwrap_or(&*self.default).clone() } + + /// Iter + pub fn iter(&self) -> std::collections::btree_map::Iter { + self.map.iter() + } +} + +/// Merge two Array Iterators +pub struct ArrayMerge<'a> { + left: Peekable>, + right: Peekable>, + left_dfl: &'a Value, + right_dfl: &'a Value, +} + +impl<'a> ArrayMerge<'a> { + /// Create a new [ArrayMerge] from two [Array]s + pub fn new(a: &'a Array, b: &'a Array) -> Self { + assert!( + a.size == b.size, + "IR Arrays have different lengths: {}, {}", + a.size, + b.size + ); + assert!( + a.key_sort == b.key_sort, + "IR Arrays have different key sorts: {}, {}", + a.key_sort, + b.key_sort, + ); + assert!( + a.default.sort() == b.default.sort(), + "IR Arrays default values have different key sorts: {}, {}", + a.default.sort(), + b.default.sort() + ); + + Self { + left: a.iter().peekable(), + right: b.iter().peekable(), + left_dfl: &*a.default, + right_dfl: &*b.default, + } + } +} + +impl<'a> Iterator for ArrayMerge<'a> { + type Item = (&'a Value, &'a Value, &'a Value); + fn next(&mut self) -> Option<(&'a Value, &'a Value, &'a Value)> { + let res: Option<(&'a Value, &'a Value, &'a Value)> = + match (self.left.peek(), self.right.peek()) { + (Some((l_ind, _l_val)), Some((r_ind, _r_val))) => match l_ind.cmp(r_ind) { + Ordering::Less => { + let (l_ind, l_val) = self.left.next().unwrap(); + Some((l_ind, l_val, self.right_dfl)) + } + Ordering::Greater => { + let (r_ind, r_val) = self.right.next().unwrap(); + Some((r_ind, self.left_dfl, r_val)) + } + Ordering::Equal => { + let (l_ind, l_val) = self.left.next().unwrap(); + let (_r_ind, r_val) = self.right.next().unwrap(); + Some((l_ind, l_val, r_val)) + } + }, + (Some(_), None) => { + let (l_ind, l_val) = self.left.next().unwrap(); + Some((l_ind, l_val, self.right_dfl)) + } + (None, Some(_)) => { + let (r_ind, r_val) = self.left.next().unwrap(); + Some((r_ind, self.left_dfl, r_val)) + } + (None, None) => None, + }; + res + } } impl Display for Value { diff --git a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok b/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok index 84c5dc07d..3650dda0d 100644 --- a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok +++ b/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(u8[N] a, u8[N] b) -> u8[N]: + return [0; N] + +def vadd_u16(u16[N] a, u16[N] b) -> u16[N]: + return [0; N] + +def vadd_u32(u32[N] a, u32[N] b) -> u32[N]: + return [0; N] + +def vadd_u64(u64[N] a, u64[N] b) -> u64[N]: + return [0; N] \ No newline at end of file