From 66438fb63978e0c76d90ca7a2341666eff775fba Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Tue, 26 Apr 2022 13:23:12 -0400 Subject: [PATCH 01/14] initial vector add zok frontend --- Cargo.lock | 63 ++++++++++++++++--- scripts/zx_tests/vector_add.zx | 6 ++ scripts/zx_tests/vector_add.zxf | 6 ++ src/front/zsharp/mod.rs | 24 ++++++- src/front/zsharp/term.rs | 14 +++++ .../ZoKrates/zokrates_stdlib/stdlib/EMBED.zok | 4 ++ 6 files changed, 109 insertions(+), 8 deletions(-) create mode 100644 scripts/zx_tests/vector_add.zx create mode 100644 scripts/zx_tests/vector_add.zxf diff --git a/Cargo.lock b/Cargo.lock index 30ac3424f..91b0e227f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -138,7 +138,7 @@ dependencies = [ "log", "num_cpus", "pairing", - "rand_core", + "rand_core 0.6.3", "rayon", "subtle", ] @@ -149,6 +149,15 @@ version = "1.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" +[[package]] +name = "bitmaps" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2" +dependencies = [ + "typenum", +] + [[package]] name = "bitvec" version = "0.22.3" @@ -202,7 +211,7 @@ dependencies = [ "ff", "group", "pairing", - "rand_core", + "rand_core 0.6.3", "subtle", ] @@ -246,6 +255,7 @@ dependencies = [ "good_lp", "hashconsing", "ieee754", + "im", "itertools 0.10.3", "lang-c", "lazy_static", @@ -441,7 +451,7 @@ dependencies = [ "bitvec", "byteorder", "ff_derive 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)", - "rand_core", + "rand_core 0.6.3", "subtle", ] @@ -578,7 +588,7 @@ checksum = "bc5ac374b108929de78460075f3dc439fa66df9d8fc77e8f12caa5165fcf0c89" dependencies = [ "byteorder", "ff", - "rand_core", + "rand_core 0.6.3", "subtle", ] @@ -630,6 +640,20 @@ version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9007da9cacbd3e6343da136e98b0d2df013f553d35bdec8b518f07bea768e19c" +[[package]] +name = "im" +version = "15.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "111c1983f3c5bb72732df25cddacee9b546d08325fb584b5ebd38148be7b0246" +dependencies = [ + "bitmaps", + "rand_core 0.5.1", + "rand_xoshiro", + "sized-chunks", + "typenum", + "version_check", +] + [[package]] name = "indexmap" version = "1.7.0" @@ -1009,7 +1033,7 @@ checksum = "2e7573632e6454cf6b99d7aac4ccca54be06da05aca2ef7423d22d27d4d4bcd8" dependencies = [ "libc", "rand_chacha", - "rand_core", + "rand_core 0.6.3", "rand_hc", ] @@ -1020,9 +1044,15 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" dependencies = [ "ppv-lite86", - "rand_core", + "rand_core 0.6.3", ] +[[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" @@ -1038,7 +1068,16 @@ version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d51e9f596de227fda2ea6c84607f5558e196eeaf43c986b724ba4fb8fdf497e7" dependencies = [ - "rand_core", + "rand_core 0.6.3", +] + +[[package]] +name = "rand_xoshiro" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a9fcdd2e881d02f1d9390ae47ad8e5696a9e4be7b547a1da2afbc61973217004" +dependencies = [ + "rand_core 0.5.1", ] [[package]] @@ -1191,6 +1230,16 @@ dependencies = [ "failure", ] +[[package]] +name = "sized-chunks" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e" +dependencies = [ + "bitmaps", + "typenum", +] + [[package]] name = "strsim" version = "0.8.0" diff --git a/scripts/zx_tests/vector_add.zx b/scripts/zx_tests/vector_add.zx new file mode 100644 index 000000000..7a778de25 --- /dev/null +++ b/scripts/zx_tests/vector_add.zx @@ -0,0 +1,6 @@ +from "EMBED" import vector_add + +def main() -> u32[5]: + u32[5] a = [1, 2, 3, 4, 5] + u32[5] b = [2, 3, 4, 5, 6] + return vector_add(a,b) diff --git a/scripts/zx_tests/vector_add.zxf b/scripts/zx_tests/vector_add.zxf new file mode 100644 index 000000000..de6e68a93 --- /dev/null +++ b/scripts/zx_tests/vector_add.zxf @@ -0,0 +1,6 @@ +from "EMBED" import vector_add + +def main() -> u32[5]: + u32[5] a = [1, 2, 3, 4, 5] + u32[5] b = [] + return vector_add(a,b) diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index 8ea80dfde..a7a748a02 100644 --- a/src/front/zsharp/mod.rs +++ 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,28 @@ impl<'ast> ZGen<'ast> { Ok(uint_lit(DFL_T.modulus().significant_bits(), 32)) } } + "vector_add" => { + if args.len() != 2 { + Err(format!( + "Got {} args to EMBED/vector_add, expected 2", + args.len() + )) + } else if generics.len() != 1 { + Err(format!( + "Got {} generic args to EMBED/vector_add, expected 1", + generics.len() + )) + } else { + assert!(args.iter().all(|t| { + let t_sort = t.type_(); + match t_sort { + Ty::Array(_, _) => true, + _ => false, + } + })); + vector_op(BV_ADD, args[0].clone(), args[1].clone()) + } + } _ => Err(format!("Unknown or unimplemented builtin '{}'", f_name)), } } diff --git a/src/front/zsharp/term.rs b/src/front/zsharp/term.rs index 3c8255f21..74e8065cd 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -908,6 +908,20 @@ 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)) => { + 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.clone()), t)) + } else { + panic!("Mismatched array types"); + } + } + _ => Err(format!("Cannot do vector_add on non-array types")), + } +} + pub struct ZSharp { values: Option>, } diff --git a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok b/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok index 84c5dc07d..1c61d29f2 100644 --- a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok +++ b/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok @@ -75,3 +75,7 @@ def u16_to_u32(u16 i) -> u32: def u8_to_u16(u8 i) -> u16: return 0u16 + +// vector functions +def vector_add(u32[N] a, u32[N] b) -> u32[N]: + return [0; N] \ No newline at end of file From b1cceff1477dcf18a648143c67976c550848d1c3 Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Tue, 26 Apr 2022 17:26:53 -0400 Subject: [PATCH 02/14] minor --- src/front/zsharp/mod.rs | 6 +----- src/front/zsharp/term.rs | 2 +- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index a7a748a02..1d039db31 100644 --- a/src/front/zsharp/mod.rs +++ b/src/front/zsharp/mod.rs @@ -319,10 +319,7 @@ impl<'ast> ZGen<'ast> { } else { assert!(args.iter().all(|t| { let t_sort = t.type_(); - match t_sort { - Ty::Array(_, _) => true, - _ => false, - } + matches!(t_sort, Ty::Array(_, _)) })); vector_op(BV_ADD, args[0].clone(), args[1].clone()) } @@ -913,7 +910,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 74e8065cd..60cbdbe87 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -918,7 +918,7 @@ pub fn vector_op(op: Op, a: T, b: T) -> Result { panic!("Mismatched array types"); } } - _ => Err(format!("Cannot do vector_add on non-array types")), + _ => Err("Cannot do vector_add on non-array types".to_string()), } } From f9619f45621dc820ce6d0eb77e718fee151c7d20 Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Wed, 27 Apr 2022 12:30:59 -0400 Subject: [PATCH 03/14] cfold -- incorrect --- src/ir/opt/cfold.rs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index c022a694a..c1cd2e489 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -5,6 +5,7 @@ use crate::ir::term::*; use circ_fields::FieldV; use lazy_static::lazy_static; use rug::Integer; +use std::collections::BTreeMap; use std::ops::DerefMut; use std::sync::RwLock; @@ -244,6 +245,26 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> Term { b.width() + w, )))) }), + Op::Map(op) => match *op.clone() { + BV_ADD => match (get(0).as_array_opt(), get(1).as_array_opt()) { + (Some(a), Some(b)) => { + let mut arr: Vec = Vec::new(); + for (a_ind, a_val) in &a.map { + let b_val = &b.map[&a_ind]; + arr.push(fold_cache(&term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))], cache)); + } + let new_arr = Array::new( + a.key_sort.clone(), + Box::new(a.key_sort.default_value()), + BTreeMap::new(), + a.size, + ); + Some(leaf_term(Op::Const(Value::Array(new_arr)))) + } + _ => None, + }, + _ => None, + }, _ => None, }; let new_t = { From a3d1f2f6d787c5735c5d29e9a2f350898f954fc4 Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Wed, 27 Apr 2022 12:43:01 -0400 Subject: [PATCH 04/14] minor comments --- scripts/zx_tests/vector_add.zx | 1 + src/front/zsharp/mod.rs | 5 +---- src/front/zsharp/term.rs | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/scripts/zx_tests/vector_add.zx b/scripts/zx_tests/vector_add.zx index 7a778de25..5ea611eac 100644 --- a/scripts/zx_tests/vector_add.zx +++ b/scripts/zx_tests/vector_add.zx @@ -3,4 +3,5 @@ from "EMBED" import vector_add def main() -> u32[5]: u32[5] a = [1, 2, 3, 4, 5] u32[5] b = [2, 3, 4, 5, 6] + assert(vector_add(a, b) == [3, 5, 7, 9, 11]) return vector_add(a,b) diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index 1d039db31..18213b285 100644 --- a/src/front/zsharp/mod.rs +++ b/src/front/zsharp/mod.rs @@ -317,10 +317,7 @@ impl<'ast> ZGen<'ast> { generics.len() )) } else { - assert!(args.iter().all(|t| { - let t_sort = t.type_(); - matches!(t_sort, Ty::Array(_, _)) - })); + assert!(args.iter().all(|t| matches!(t.type_(), Ty::Array(_, _)))); vector_op(BV_ADD, args[0].clone(), args[1].clone()) } } diff --git a/src/front/zsharp/term.rs b/src/front/zsharp/term.rs index 60cbdbe87..f5b430328 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -915,7 +915,7 @@ pub fn vector_op(op: Op, a: T, b: T) -> Result { let t = term![Op::Map(Box::new(op)); a.term, b.term]; Ok(T::new(Ty::Array(*a_s, a_ty.clone()), t)) } else { - panic!("Mismatched array types"); + panic!("Mismatched array types (this is a bug: type checking should have caught this!)"); } } _ => Err("Cannot do vector_add on non-array types".to_string()), From 49576d2c12a30dc64d8df19e885019ba5a76a085 Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Wed, 27 Apr 2022 17:01:10 -0400 Subject: [PATCH 05/14] updated cfold --- src/front/zsharp/mod.rs | 4 +++- src/ir/opt/cfold.rs | 41 +++++++++++++++++++++++++---------------- 2 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index 18213b285..8aa1bc03a 100644 --- a/src/front/zsharp/mod.rs +++ b/src/front/zsharp/mod.rs @@ -318,7 +318,9 @@ impl<'ast> ZGen<'ast> { )) } else { assert!(args.iter().all(|t| matches!(t.type_(), Ty::Array(_, _)))); - vector_op(BV_ADD, args[0].clone(), args[1].clone()) + let a = args.pop().unwrap(); + let b = args.pop().unwrap(); + vector_op(BV_ADD, a, b) } } _ => Err(format!("Unknown or unimplemented builtin '{}'", f_name)), diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index c1cd2e489..0b730fb94 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -245,24 +245,33 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> Term { b.width() + w, )))) }), - Op::Map(op) => match *op.clone() { - BV_ADD => match (get(0).as_array_opt(), get(1).as_array_opt()) { - (Some(a), Some(b)) => { - let mut arr: Vec = Vec::new(); - for (a_ind, a_val) in &a.map { - let b_val = &b.map[&a_ind]; - arr.push(fold_cache(&term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))], cache)); - } - let new_arr = Array::new( - a.key_sort.clone(), - Box::new(a.key_sort.default_value()), - BTreeMap::new(), - a.size, + Op::Map(op) => match (get(0).as_array_opt(), get(1).as_array_opt()) { + (Some(a), Some(b)) => { + assert!(a.size == b.size); + let mut new_map: BTreeMap = BTreeMap::new(); + for (a_ind, a_val) in &a.map { + let b_val = &b.map[&a_ind]; + let res = fold_cache( + &term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))], + cache, ); - Some(leaf_term(Op::Const(Value::Array(new_arr)))) + match res.as_value_opt() { + Some(r) => { + new_map.insert(a_ind.clone(), r.clone()); + } + None => { + panic!("Unale to constant constant fold idx: {}", a_ind); + } + } } - _ => None, - }, + let new_arr = Array::new( + a.key_sort.clone(), + Box::new(a.key_sort.default_value()), + new_map, + a.size, + ); + Some(leaf_term(Op::Const(Value::Array(new_arr)))) + } _ => None, }, _ => None, From 47fbdb8de827ddbc6f2fafec39a98a2242be874a Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Wed, 27 Apr 2022 17:02:01 -0400 Subject: [PATCH 06/14] lint --- src/ir/opt/cfold.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index 0b730fb94..b2a86973e 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -250,7 +250,7 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> Term { assert!(a.size == b.size); let mut new_map: BTreeMap = BTreeMap::new(); for (a_ind, a_val) in &a.map { - let b_val = &b.map[&a_ind]; + let b_val = &b.map[a_ind]; let res = fold_cache( &term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))], cache, From 3a065c021a295438856427ea2a9802c8e513ea6b Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Wed, 27 Apr 2022 21:14:45 -0400 Subject: [PATCH 07/14] tmp --- src/ir/opt/cfold.rs | 46 +++++++++++++++++++---------------- src/ir/term/mod.rs | 58 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 83 insertions(+), 21 deletions(-) diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index b2a86973e..32de2aaa3 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -248,28 +248,32 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> Term { Op::Map(op) => match (get(0).as_array_opt(), get(1).as_array_opt()) { (Some(a), Some(b)) => { assert!(a.size == b.size); - let mut new_map: BTreeMap = BTreeMap::new(); - for (a_ind, a_val) in &a.map { - let b_val = &b.map[a_ind]; - let res = fold_cache( - &term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))], - cache, - ); - match res.as_value_opt() { - Some(r) => { - new_map.insert(a_ind.clone(), r.clone()); - } - None => { - panic!("Unale to constant constant fold idx: {}", a_ind); - } - } + + for t in a. { + } - let new_arr = Array::new( - a.key_sort.clone(), - Box::new(a.key_sort.default_value()), - new_map, - a.size, - ); + + + + // let mut new_map: BTreeMap = BTreeMap::new(); + // for (a_ind, a_val) in &a.map { + // let b_val = &b.map[a_ind]; + // let res = &term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))]; + // match res.as_value_opt() { + // Some(r) => { + // new_map.insert(a_ind.clone(), r.clone()); + // } + // None => { + // panic!("Unale to constant constant fold idx: {}", a_ind); + // } + // } + // } + // let new_arr = Array::new( + // a.key_sort.clone(), + // Box::new(a.key_sort.default_value()), + // new_map, + // a.size, + // ); Some(leaf_term(Op::Const(Value::Array(new_arr)))) } _ => None, diff --git a/src/ir/term/mod.rs b/src/ir/term/mod.rs index ff910fce2..27f6206df 100644 --- a/src/ir/term/mod.rs +++ b/src/ir/term/mod.rs @@ -31,6 +31,7 @@ use log::debug; use rug::Integer; 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 +722,63 @@ 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 { + self.map.into_iter() + } +} + +/// Merge two Array Iterators +struct ArrayMerge { + left: Peekable>, + right: Peekable>, + left_dfl: Value, + right_dfl: Value, +} + +impl ArrayMerge { + 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: a.into_iter().peekable(), + right: b.into_iter().peekable(), + left_dfl: *a.default, + right_dfl: *b.default, + } + } + + pub fn peek(&self) -> (Option<&(Value, Value)>, Option<&(Value, Value)>) { + (self.left.peek(), self.right.peek()) + } + + pub fn left_next(&self) -> Option<(Value, Value)> { + self.left.next() + } + + pub fn right_next(&self) -> Option<(Value, Value)> { + self.right.next() + } + + pub fn next(&self) -> (Option<(Value, Value)>, Option<(Value, Value)>) { + (self.left.next(), self.right.next()) + } } impl Display for Value { From 123e691ad0b64b7529516f981febaa14f7d5815d Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Thu, 28 Apr 2022 00:03:48 -0400 Subject: [PATCH 08/14] array merge --- src/ir/opt/cfold.rs | 45 ++++++++++----------------- src/ir/term/mod.rs | 75 ++++++++++++++++++++++++++++++++++----------- 2 files changed, 74 insertions(+), 46 deletions(-) diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index 32de2aaa3..b9429963f 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -5,7 +5,6 @@ use crate::ir::term::*; use circ_fields::FieldV; use lazy_static::lazy_static; use rug::Integer; -use std::collections::BTreeMap; use std::ops::DerefMut; use std::sync::RwLock; @@ -247,34 +246,24 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> Term { }), Op::Map(op) => match (get(0).as_array_opt(), get(1).as_array_opt()) { (Some(a), Some(b)) => { - assert!(a.size == b.size); - - for t in a. { - + // 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); + } + } } - - - - // let mut new_map: BTreeMap = BTreeMap::new(); - // for (a_ind, a_val) in &a.map { - // let b_val = &b.map[a_ind]; - // let res = &term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))]; - // match res.as_value_opt() { - // Some(r) => { - // new_map.insert(a_ind.clone(), r.clone()); - // } - // None => { - // panic!("Unale to constant constant fold idx: {}", a_ind); - // } - // } - // } - // let new_arr = Array::new( - // a.key_sort.clone(), - // Box::new(a.key_sort.default_value()), - // new_map, - // a.size, - // ); - Some(leaf_term(Op::Const(Value::Array(new_arr)))) + Some(leaf_term(Op::Const(Value::Array(res)))) } _ => None, }, diff --git a/src/ir/term/mod.rs b/src/ir/term/mod.rs index 27f6206df..3ef0ef92c 100644 --- a/src/ir/term/mod.rs +++ b/src/ir/term/mod.rs @@ -725,19 +725,20 @@ impl Array { /// Iter pub fn into_iter(&self) -> std::collections::btree_map::IntoIter { - self.map.into_iter() + self.map.clone().into_iter() } } /// Merge two Array Iterators -struct ArrayMerge { - left: Peekable>, - right: Peekable>, +pub struct ArrayMerge { + left: Peekable>>, + right: Peekable>>, 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); @@ -757,27 +758,65 @@ impl ArrayMerge { } Self { - left: a.into_iter().peekable(), - right: b.into_iter().peekable(), + left: Box::new(a.into_iter()).peekable(), + right: Box::new(b.into_iter()).peekable(), left_dfl: *a.default, right_dfl: *b.default, } } - pub fn peek(&self) -> (Option<&(Value, Value)>, Option<&(Value, Value)>) { - (self.left.peek(), self.right.peek()) - } - - pub fn left_next(&self) -> Option<(Value, Value)> { - self.left.next() - } + /// Iter + pub fn into_iter(&mut self) -> Box> { + 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))) => { + if l_ind < r_ind { + left_next = true; + Some((l_ind.clone(), l_val.clone(), self.right_dfl.clone())) + } else if r_ind < l_ind { + right_next = true; + Some((r_ind.clone(), self.left_dfl.clone(), r_val.clone())) + } else { + 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, + }; - pub fn right_next(&self) -> Option<(Value, Value)> { - self.right.next() - } + if left_next { + self.left.next(); + } + if right_next { + self.right.next(); + } - pub fn next(&self) -> (Option<(Value, Value)>, Option<(Value, Value)>) { - (self.left.next(), self.right.next()) + res } } From d976738c04f20ac413abc337efa3cfde7d37c98a Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Fri, 29 Apr 2022 17:22:55 -0400 Subject: [PATCH 09/14] updated to match comments --- scripts/zx_tests/vadd_u16.zx | 7 +++++++ scripts/zx_tests/vadd_u32.zx | 7 +++++++ .../zx_tests/{vector_add.zxf => vadd_u32.zxf} | 4 ++-- scripts/zx_tests/vadd_u64.zx | 7 +++++++ scripts/zx_tests/vadd_u8.zx | 7 +++++++ scripts/zx_tests/vector_add.zx | 7 ------- src/front/zsharp/mod.rs | 8 ++++---- src/front/zsharp/term.rs | 6 +++--- src/ir/term/mod.rs | 19 +++++++++++-------- .../ZoKrates/zokrates_stdlib/stdlib/EMBED.zok | 11 ++++++++++- 10 files changed, 58 insertions(+), 25 deletions(-) create mode 100644 scripts/zx_tests/vadd_u16.zx create mode 100644 scripts/zx_tests/vadd_u32.zx rename scripts/zx_tests/{vector_add.zxf => vadd_u32.zxf} (55%) create mode 100644 scripts/zx_tests/vadd_u64.zx create mode 100644 scripts/zx_tests/vadd_u8.zx delete mode 100644 scripts/zx_tests/vector_add.zx 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/vector_add.zxf b/scripts/zx_tests/vadd_u32.zxf similarity index 55% rename from scripts/zx_tests/vector_add.zxf rename to scripts/zx_tests/vadd_u32.zxf index de6e68a93..22b985fbd 100644 --- a/scripts/zx_tests/vector_add.zxf +++ b/scripts/zx_tests/vadd_u32.zxf @@ -1,6 +1,6 @@ -from "EMBED" import vector_add +from "EMBED" import vadd_u32 def main() -> u32[5]: u32[5] a = [1, 2, 3, 4, 5] u32[5] b = [] - return vector_add(a,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/scripts/zx_tests/vector_add.zx b/scripts/zx_tests/vector_add.zx deleted file mode 100644 index 5ea611eac..000000000 --- a/scripts/zx_tests/vector_add.zx +++ /dev/null @@ -1,7 +0,0 @@ -from "EMBED" import vector_add - -def main() -> u32[5]: - u32[5] a = [1, 2, 3, 4, 5] - u32[5] b = [2, 3, 4, 5, 6] - assert(vector_add(a, b) == [3, 5, 7, 9, 11]) - return vector_add(a,b) diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index 8aa1bc03a..160533c02 100644 --- a/src/front/zsharp/mod.rs +++ b/src/front/zsharp/mod.rs @@ -305,21 +305,21 @@ impl<'ast> ZGen<'ast> { Ok(uint_lit(DFL_T.modulus().significant_bits(), 32)) } } - "vector_add" => { + "vadd_u8" | "vadd_u16" | "vadd_u32" | "vadd_u64" => { if args.len() != 2 { Err(format!( - "Got {} args to EMBED/vector_add, expected 2", + "Got {} args to EMBED/vadd_*, expected 2", args.len() )) } else if generics.len() != 1 { Err(format!( - "Got {} generic args to EMBED/vector_add, expected 1", + "Got {} generic args to EMBED/vadd_*, expected 1", generics.len() )) } else { assert!(args.iter().all(|t| matches!(t.type_(), Ty::Array(_, _)))); - let a = args.pop().unwrap(); let b = args.pop().unwrap(); + let a = args.pop().unwrap(); vector_op(BV_ADD, a, b) } } diff --git a/src/front/zsharp/term.rs b/src/front/zsharp/term.rs index f5b430328..6836d531b 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -909,16 +909,16 @@ 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) { + 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.clone()), t)) + 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_add on non-array types".to_string()), + _ => Err("Cannot do vector_op on non-array types".to_string()), } } diff --git a/src/ir/term/mod.rs b/src/ir/term/mod.rs index 3ef0ef92c..8f5662317 100644 --- a/src/ir/term/mod.rs +++ b/src/ir/term/mod.rs @@ -29,6 +29,7 @@ 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; @@ -768,16 +769,16 @@ impl ArrayMerge { /// Iter pub fn into_iter(&mut self) -> Box> { let mut acc: Vec<(Value, Value, Value)> = Vec::new(); - let mut next = self.next(); + let mut next = self.next_(); while let Some(n) = next { acc.push(n); - next = self.next(); + next = self.next_(); } Box::new(acc.into_iter()) } /// Next - pub fn next(&mut self) -> Option<(Value, Value, Value)> { + pub fn next_(&mut self) -> Option<(Value, Value, Value)> { let l_peek = self.left.peek(); let r_peek = self.right.peek(); @@ -785,19 +786,21 @@ impl ArrayMerge { let mut right_next = false; let res = match (l_peek, r_peek) { - (Some((l_ind, l_val)), Some((r_ind, r_val))) => { - if l_ind < r_ind { + (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())) - } else if r_ind < l_ind { + } + Ordering::Greater => { right_next = true; Some((r_ind.clone(), self.left_dfl.clone(), r_val.clone())) - } else { + } + 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())) diff --git a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok b/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok index 1c61d29f2..3650dda0d 100644 --- a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok +++ b/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok @@ -77,5 +77,14 @@ def u8_to_u16(u8 i) -> u16: return 0u16 // vector functions -def vector_add(u32[N] a, u32[N] b) -> u32[N]: +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 From 8887be7fe863bea51f9277d9aa8d7c713fce50ba Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Fri, 29 Apr 2022 17:25:54 -0400 Subject: [PATCH 10/14] Update Cargo.lock --- Cargo.lock | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.lock b/Cargo.lock index 91b0e227f..263ddf657 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -211,7 +211,7 @@ dependencies = [ "ff", "group", "pairing", - "rand_core 0.6.3", + "rand_core", "subtle", ] From 7057117dfbba70249051bcac6c4f155c397e899b Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Fri, 29 Apr 2022 17:26:41 -0400 Subject: [PATCH 11/14] remove Cargo lock --- Cargo.lock | 340 +++++++++++++++++++++++++++-------------------------- 1 file changed, 171 insertions(+), 169 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 91b0e227f..8f4dadf82 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -15,9 +15,9 @@ dependencies = [ [[package]] name = "addr2line" -version = "0.16.0" +version = "0.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3e61f2b7f93d2c7d2b08263acaa4a363b3e276806c68af6134c44f523bf1aacd" +checksum = "b9ecd88a8c8378ca913a680cd98f0f13ac67383d35993f86c90a70e3f137816b" dependencies = [ "gimli", ] @@ -50,18 +50,18 @@ dependencies = [ [[package]] name = "ansi_term" -version = "0.11.0" +version = "0.12.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ee49baf6cb617b853aa8d93bf420db2383fab46d314482ca2803b40d5fde979b" +checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" dependencies = [ "winapi", ] [[package]] name = "approx" -version = "0.5.0" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "072df7202e63b127ab55acfe16ce97013d5b97bf160489336d3f1840fd78e99e" +checksum = "cab112f0a86d568ea0e627cc1d6be74a1e9cd55214684db5561995f6dad897c6" dependencies = [ "num-traits", ] @@ -91,21 +91,21 @@ dependencies = [ [[package]] name = "autocfg" -version = "1.0.1" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a" +checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" [[package]] name = "az" -version = "1.1.2" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9d6dff4a1892b54d70af377bf7a17064192e822865791d812957f21e3108c325" +checksum = "f771a5d1f5503f7f4279a30f3643d3421ba149848b89ecaaec0ea2acf04a5ac4" [[package]] name = "backtrace" -version = "0.3.61" +version = "0.3.65" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e7a905d892734eea339e896738c14b9afce22b5318f64b951e70bf3844419b01" +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", ] @@ -229,9 +229,9 @@ checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610" [[package]] name = "cc" -version = "1.0.71" +version = "1.0.73" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "79c2681d6594606957bbb8631c4b90a7fcaaa72cdb714743a437b156d6a7eedd" +checksum = "2fff2a6927b3bb87f9595d67196a70493f627687a71d87a0d692242c33f58c11" [[package]] name = "cfg-if" @@ -297,9 +297,9 @@ dependencies = [ [[package]] name = "clap" -version = "2.33.3" +version = "2.34.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "37e58ac78573c40708d45522f0d80fa2f01cc4f9b4e2bf749807255454312002" +checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c" dependencies = [ "ansi_term", "atty", @@ -334,9 +334,9 @@ checksum = "245097e9a4535ee1e3e3931fcfcd55a796a44c643e8596ff6566d68f09b87bbc" [[package]] name = "crossbeam-channel" -version = "0.5.1" +version = "0.5.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "06ed27e177f16d65f0f0c22a213e17c696ace5dd64b14258b52f9417ccb52db4" +checksum = "5aaa7bd5fb665c6864b5f963dd9097905c54125909c7aa94c9e18507cdbe6c53" dependencies = [ "cfg-if", "crossbeam-utils", @@ -355,10 +355,11 @@ dependencies = [ [[package]] name = "crossbeam-epoch" -version = "0.9.5" +version = "0.9.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4ec02e091aa634e2c3ada4a392989e7c3116673ef0ac5b72232439094d73b7fd" +checksum = "1145cf131a2c6ba0615079ab6a638f7e1973ac9c2634fcbeaaad6114246efe8c" dependencies = [ + "autocfg", "cfg-if", "crossbeam-utils", "lazy_static", @@ -368,9 +369,9 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.5" +version = "0.8.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d82cfc11ce7f2c3faef78d8a684447b40d503d9681acebed6cb728d45940c4db" +checksum = "0bf124c720b7686e3c2663cf54062ab0f68a88af2fb6a030e87e30bf721fcb38" dependencies = [ "cfg-if", "lazy_static", @@ -430,9 +431,9 @@ version = "0.1.8" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "aa4da3c766cd7a0db8242e326e9e4e081edd567072893ed320008189715366a4" dependencies = [ - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", "synstructure", ] @@ -442,6 +443,15 @@ version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e88a8acf291dafb59c2d96e8f59828f3838bb1a70398823ade51a84de6a6deed" +[[package]] +name = "fastrand" +version = "1.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c3fcf0cee53519c866c09b5de1f6c56ff9d647101f81c1964fa632e148896cdf" +dependencies = [ + "instant", +] + [[package]] name = "ff" version = "0.11.0" @@ -451,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", ] @@ -462,9 +472,9 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e715451ab983be06481e927a275ec12372103ad426c7cb82cebfe14698ed4cf4" dependencies = [ "num-traits", - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] @@ -477,9 +487,9 @@ dependencies = [ "num-bigint", "num-integer", "num-traits", - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] @@ -491,16 +501,16 @@ dependencies = [ "num-bigint", "num-integer", "num-traits", - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] name = "fixedbitset" -version = "0.4.0" +version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "398ea4fabe40b9b0d885340a2a991a44c8a645624075ad966d21f88688e2b69e" +checksum = "279fb028e20b3c4c320317955b77c5e0c9701f05a1d309905d6fc702cdc5053e" [[package]] name = "fnv" @@ -544,9 +554,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.3" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7fcd999463524c52659517fe2cea98493cfe485d10565e7b0fb07dbba7ad2753" +checksum = "9be70c98951c83b8d2f8f60d7065fa6d5146873094452a1008da8c2f1e4205ad" dependencies = [ "cfg-if", "libc", @@ -555,15 +565,15 @@ dependencies = [ [[package]] name = "gimli" -version = "0.25.0" +version = "0.26.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f0a01e0497841a3b2db4f8afa483cce65f7e96a3498bd6c541734792aeac8fe7" +checksum = "78cc372d058dcf6d5ecd98510e7fbc9e5aec4d21de70f65fea8fecebcd881bd4" [[package]] name = "gmp-mpfr-sys" -version = "1.4.7" +version = "1.4.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a146a7357ce9573bdcc416fc4a99b960e166e72d8eaffa7c59966d51866b5bfb" +checksum = "b3d00b0ef965511028498a1668c4a6ef9b0b2501a4a5ab26fb8156408869306e" dependencies = [ "libc", "winapi", @@ -571,9 +581,9 @@ dependencies = [ [[package]] name = "good_lp" -version = "1.2.0" +version = "1.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c8fba2696c6b6fce795aa113be95338541a1e08e7a80fc06ceded3e152a9c3f" +checksum = "b51d78cbb7b734379eea7f811ddb33b2b13defefa1dab50068d7bc7f781a3056" dependencies = [ "coin_cbc", "fnv", @@ -588,7 +598,7 @@ checksum = "bc5ac374b108929de78460075f3dc439fa66df9d8fc77e8f12caa5165fcf0c89" dependencies = [ "byteorder", "ff", - "rand_core 0.6.3", + "rand_core", "subtle", ] @@ -604,10 +614,11 @@ dependencies = [ [[package]] name = "hashconsing" version = "1.3.0" -source = "git+https://github.com/alex-ozdemir/hashconsing.git?branch=phash#a74c1d01742580a16243b6805b647349abbdfe59" +source = "git+https://github.com/alex-ozdemir/hashconsing.git?branch=phash#e275caec0f645cb13db2f21298bbfdbc689d9912" dependencies = [ "lazy_static", "lru", + "serde", ] [[package]] @@ -642,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", @@ -656,14 +667,23 @@ dependencies = [ [[package]] name = "indexmap" -version = "1.7.0" +version = "1.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bc633605454125dec4b66843673f01c7df2b89479b32e0ed634e43a91cff62a5" +checksum = "0f647032dfaa1f8b6dc29bd3edb7bbef4861b8b8007ebb118d6db284fd59f6ee" dependencies = [ "autocfg", "hashbrown", ] +[[package]] +name = "instant" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" +dependencies = [ + "cfg-if", +] + [[package]] name = "itertools" version = "0.7.11" @@ -684,9 +704,9 @@ dependencies = [ [[package]] name = "itoa" -version = "0.4.8" +version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b71991ff56294aa922b450139ee08b3bfc70982c6b2c7562771375cf73542dd4" +checksum = "1aab8fc367588b89dcee83ab0fd66b72b50b72fa1904d7095045ace2b0c81c35" [[package]] name = "lang-c" @@ -702,15 +722,15 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.104" +version = "0.2.125" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b2f96d100e1cf1929e7719b7edb3b90ab5298072638fccd77be9ce942ecdfce" +checksum = "5916d2ae698f6de9bfb891ad7a8d65c09d232dc58cc4ac433c7da3b2fd84bc2b" [[package]] name = "log" -version = "0.4.14" +version = "0.4.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "51b9bbe6c47d51fc3e1a9b945965946b4c44142ab8792c50835a980d362c2710" +checksum = "6389c490849ff5bc16be905ae24bc913a9c8892e19b2341dbc175e14c341c2b8" dependencies = [ "cfg-if", ] @@ -732,10 +752,10 @@ checksum = "56a7d287fd2ac3f75b11f19a1c8a874a7d55744bd91f7a1b3e7cf87d4343c36d" dependencies = [ "beef", "fnv", - "proc-macro2 1.0.30", - "quote 1.0.10", + "proc-macro2 1.0.37", + "quote 1.0.18", "regex-syntax", - "syn 1.0.80", + "syn 1.0.92", "utf8-ranges", ] @@ -751,9 +771,9 @@ dependencies = [ [[package]] name = "lru" -version = "0.7.2" +version = "0.7.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "274353858935c992b13c0ca408752e2121da852d07dec7ce5f108c77dfa14d1f" +checksum = "32613e41de4c47ab04970c348ca7ae7382cf116625755af070b008a15516a889" dependencies = [ "hashbrown", ] @@ -772,21 +792,20 @@ checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a" [[package]] name = "memoffset" -version = "0.6.4" +version = "0.6.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "59accc507f1338036a0477ef61afdae33cde60840f4dfe481319ce3ad116ddf9" +checksum = "5aa361d4faea93603064a027415f07bd8e1d5c88c9fbf68bf56a285428fd79ce" dependencies = [ "autocfg", ] [[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]] @@ -821,9 +840,9 @@ dependencies = [ [[package]] name = "num_cpus" -version = "1.13.0" +version = "1.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "05499f3756671c15885fee9034446956fff3f243d6077b91e5767df161f766b3" +checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1" dependencies = [ "hermit-abi", "libc", @@ -831,18 +850,18 @@ dependencies = [ [[package]] name = "object" -version = "0.26.2" +version = "0.28.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "39f37e50073ccad23b6d09bcb5b263f4e76d3bb6038e4a3c08e52162ffa8abc2" +checksum = "40bec70ba014595f99f7aa110b84331ffe1ee9aece7fe6f387cc7e3ecda4d456" dependencies = [ "memchr", ] [[package]] name = "once_cell" -version = "1.9.0" +version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da32515d9f6e6e489d7bc9d84c71b060db7247dc035bbe44eac88cf87486d8d5" +checksum = "87f3e037eac156d1775da914196f0f37741a274155e34a0b7e427c35d2a2ecb9" [[package]] name = "opaque-debug" @@ -861,9 +880,9 @@ dependencies = [ [[package]] name = "paste" -version = "1.0.6" +version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0744126afe1a6dd7f394cb50a716dbe086cb06e255e53d8d0185d82828358fb5" +checksum = "0c520e05135d6e763148b6426a837e239041653ba7becd2e538c076c738025fc" [[package]] name = "pest" @@ -905,9 +924,9 @@ checksum = "99b8db626e31e5b81787b9783425769681b347011cc59471e33ea46d2ea0cf55" dependencies = [ "pest", "pest_meta", - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] @@ -933,9 +952,9 @@ dependencies = [ [[package]] name = "ppv-lite86" -version = "0.2.14" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3ca011bd0129ff4ae15cd04c4eef202cadf6c51c21e47aba319b4e0501db741" +checksum = "eb9f9e6e233e5c4a35559a617bf40a4ec447db2e84c20b55a6f83167b7e57872" [[package]] name = "proc-macro-error" @@ -944,9 +963,9 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" dependencies = [ "proc-macro-error-attr", - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", "version_check", ] @@ -956,8 +975,8 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" dependencies = [ - "proc-macro2 1.0.30", - "quote 1.0.10", + "proc-macro2 1.0.37", + "quote 1.0.18", "version_check", ] @@ -972,9 +991,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.30" +version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "edc3358ebc67bc8b7fa0c007f945b0b18226f78437d61bec735a9eb96b61ee70" +checksum = "ec757218438d5fda206afc041538b2f6d889286160d649a86a24d37e1235afd1" dependencies = [ "unicode-xid 0.2.2", ] @@ -996,9 +1015,9 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b22a693222d716a9587786f37ac3f6b4faedb5b80c23914e7303ff5a1d8016e9" dependencies = [ - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] @@ -1012,11 +1031,11 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.10" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38bc8cc6a5f2e3655e0899c1b848643b2562f853f114bfec7be120678e3ace05" +checksum = "a1feb54ed693b93a84e14094943b84b7c4eae204c512b7ccb95ab0c66d278ad1" dependencies = [ - "proc-macro2 1.0.30", + "proc-macro2 1.0.37", ] [[package]] @@ -1027,14 +1046,13 @@ checksum = "643f8f41a8ebc4c5dc4515c82bb8abd397b527fc20fd681b7c011c2aee5d44fb" [[package]] name = "rand" -version = "0.8.4" +version = "0.8.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2e7573632e6454cf6b99d7aac4ccca54be06da05aca2ef7423d22d27d4d4bcd8" +checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" dependencies = [ "libc", "rand_chacha", - "rand_core 0.6.3", - "rand_hc", + "rand_core", ] [[package]] @@ -1044,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" @@ -1062,29 +1074,20 @@ dependencies = [ "getrandom", ] -[[package]] -name = "rand_hc" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d51e9f596de227fda2ea6c84607f5558e196eeaf43c986b724ba4fb8fdf497e7" -dependencies = [ - "rand_core 0.6.3", -] - [[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]] name = "rayon" -version = "1.5.1" +version = "1.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c06aca804d41dbc8ba42dfd964f0d01334eceb64314b9ecf7c5fad5188a06d90" +checksum = "fd249e82c21598a9a426a4e00dd7adc1d640b22445ec8545feef801d1a74c221" dependencies = [ "autocfg", "crossbeam-deque", @@ -1094,31 +1097,30 @@ dependencies = [ [[package]] name = "rayon-core" -version = "1.9.1" +version = "1.9.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d78120e2c850279833f1dd3582f730c4ab53ed95aeaaaa862a2a5c71b1656d8e" +checksum = "9f51245e1e62e1f1629cbfec37b5793bbabcaeb90f30e94d2ba03564687353e4" dependencies = [ "crossbeam-channel", "crossbeam-deque", "crossbeam-utils", - "lazy_static", "num_cpus", ] [[package]] name = "redox_syscall" -version = "0.2.10" +version = "0.2.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8383f39639269cde97d255a32bdb68c047337295414940c68bdd30c2e13203ff" +checksum = "62f25bc4c7e55e0b0b7a1d43fb893f4fa1361d0abe38b9ce4f323c2adfe6ef42" dependencies = [ "bitflags", ] [[package]] name = "regex" -version = "1.5.4" +version = "1.5.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461" +checksum = "1a11647b6b25ff05a515cb92c365cec08801e83423a235b51e231e1808747286" dependencies = [ "aho-corasick", "memchr", @@ -1151,9 +1153,9 @@ dependencies = [ [[package]] name = "rug" -version = "1.13.0" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ee0c6e98de59509e62e09f3456b23cebb75dad21928882016f169bb628843459" +checksum = "f829d980ca193fa33fdd1decaebe72ec07cf2d8afdd0be60b3e5391f18014c91" dependencies = [ "az", "gmp-mpfr-sys", @@ -1168,9 +1170,9 @@ checksum = "7ef03e0a2b150c7a90d01faf6254c9c48a41e95fb2a8c2ac1c6f0d2b9aefc342" [[package]] name = "ryu" -version = "1.0.5" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "71d301d4193d031abdd79ff7e3dd721168a9572ef3fe51a1517aba235bd8f86e" +checksum = "73b4b750c782965c211b42f022f59af1fbceabdd026623714f104152f1ec149f" [[package]] name = "scopeguard" @@ -1180,29 +1182,29 @@ checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" [[package]] name = "serde" -version = "1.0.130" +version = "1.0.136" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f12d06de37cf59146fbdecab66aa99f9fe4f78722e3607577a5375d66bd0c913" +checksum = "ce31e24b01e1e524df96f1c2fdd054405f8d7376249a5110886fb4b658484789" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.130" +version = "1.0.136" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7bc1a1ab1961464eae040d96713baa5a724a8152c1222492465b54322ec508b" +checksum = "08597e7152fcd306f41838ed3e37be9eaeed2b61c42e2117266a554fab4662f9" dependencies = [ - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] name = "serde_json" -version = "1.0.68" +version = "1.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f690853975602e1bfe1ccbf50504d67174e3bcf340f23b5ea9992e0587a52d8" +checksum = "8e8d9fa5c3b304765ce1fd9c4c8a3de2c8db365a5b91be52f186efc675681d95" dependencies = [ "itoa", "ryu", @@ -1248,9 +1250,9 @@ checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" [[package]] name = "structopt" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "40b9788f4202aa75c240ecc9c15c65185e6a39ccdeb0fd5d008b98825464c87c" +checksum = "0c6b5c64445ba8094a6ab0c3cd2ad323e07171012d9c98b0b15651daf1787a10" dependencies = [ "clap", "lazy_static", @@ -1265,9 +1267,9 @@ checksum = "dcb5ae327f9cc13b68763b5749770cb9e048a99bd9dfdfa58d0cf05d5f64afe0" dependencies = [ "heck", "proc-macro-error", - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] @@ -1289,12 +1291,12 @@ dependencies = [ [[package]] name = "syn" -version = "1.0.80" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d010a1623fbd906d51d650a9916aaefc05ffa0e4053ff7fe601167f3e715d194" +checksum = "7ff7c592601f11445996a06f8ad0c27f094a58857c2f89e97974ab9235b92c52" dependencies = [ - "proc-macro2 1.0.30", - "quote 1.0.10", + "proc-macro2 1.0.37", + "quote 1.0.18", "unicode-xid 0.2.2", ] @@ -1304,9 +1306,9 @@ version = "0.12.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f" dependencies = [ - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", "unicode-xid 0.2.2", ] @@ -1318,13 +1320,13 @@ checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369" [[package]] name = "tempfile" -version = "3.2.0" +version = "3.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dac1c663cfc93810f88aed9b8941d48cabf856a1b111c29a40439018d870eb22" +checksum = "5cdb1ef4eaeeaddc8fbd371e5017057064af0911902ef36b39801f67cc6d79e4" dependencies = [ "cfg-if", + "fastrand", "libc", - "rand", "redox_syscall", "remove_dir_all", "winapi", @@ -1332,9 +1334,9 @@ dependencies = [ [[package]] name = "termcolor" -version = "1.1.2" +version = "1.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2dfed899f0eb03f32ee8c6a0aabdb8a7949659e3466561fc0adf54e26d88c5f4" +checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755" dependencies = [ "winapi-util", ] @@ -1363,9 +1365,9 @@ version = "1.0.30" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "aa32fd3f627f367fe16f893e2597ae3c05020f8bba2666a4e6ea73d377e5714b" dependencies = [ - "proc-macro2 1.0.30", - "quote 1.0.10", - "syn 1.0.80", + "proc-macro2 1.0.37", + "quote 1.0.18", + "syn 1.0.92", ] [[package]] @@ -1376,9 +1378,9 @@ checksum = "0685c84d5d54d1c26f7d3eb96cd41550adb97baed141a761cf335d3d33bcd0ae" [[package]] name = "typenum" -version = "1.14.0" +version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b63708a265f51345575b27fe43f9500ad611579e764c79edbc2037b1121959ec" +checksum = "dcf81ac59edc17cc8697ff311e8f5ef2d99fcbd9817b34cec66f90b6c3dfd987" [[package]] name = "ucd-trie" @@ -1388,9 +1390,9 @@ checksum = "56dee185309b50d1f11bfedef0fe6d036842e3fb77413abef29f8f8d1c5d4c1c" [[package]] name = "unicode-segmentation" -version = "1.8.0" +version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8895849a949e7845e06bd6dc1aa51731a103c42707010a5b591c0038fb73385b" +checksum = "7e8820f5d777f6224dc4be3632222971ac30164d4a258d595640799554ebfd99" [[package]] name = "unicode-width" @@ -1412,9 +1414,9 @@ checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3" [[package]] name = "utf8-ranges" -version = "1.0.4" +version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4ae116fef2b7fea257ed6440d3cfcff7f190865f170cdad00bb6465bf18ecba" +checksum = "7fcfc827f90e53a02eaef5e535ee14266c1d569214c6aa70133a624d8a3164ba" [[package]] name = "vec_map" @@ -1424,9 +1426,9 @@ checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" [[package]] name = "version_check" -version = "0.9.3" +version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5fecdca9a5291cc2b8dcf7dc02453fee791a280f3743cb0905f8822ae463b3fe" +checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" [[package]] name = "void" From 04d97852191d9f359d14ccb4cf2145ca332e5383 Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Sat, 14 May 2022 19:53:57 -0400 Subject: [PATCH 12/14] updated iterator --- src/front/zsharp/term.rs | 9 +-- src/ir/opt/cfold.rs | 43 +++++++----- src/ir/term/mod.rs | 146 +++++++++++++++++---------------------- 3 files changed, 91 insertions(+), 107 deletions(-) diff --git a/src/front/zsharp/term.rs b/src/front/zsharp/term.rs index 6836d531b..38cf37885 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -911,12 +911,9 @@ 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)) => { - 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!)"); - } + assert_eq!((a_s, a_ty.clone()), (b_s, b_ty.clone())); + 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()), } diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index b9429963f..d45215a1d 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -244,29 +244,36 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> 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, + 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, ); - match r.as_value_opt() { - Some(v) => { - res = res.clone().store(i, v.clone()); - } - None => { - panic!("Unable to constant fold idx: {}", i); + let merge = ArrayMerge::new(a, b); + 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.store(i.clone(), v.clone()); + } + None => { + panic!("Unable to constant fold idx: {}", i); + } } } + Some(leaf_term(Op::Const(Value::Array(res)))) } - Some(leaf_term(Op::Const(Value::Array(res)))) + _ => None, } - _ => None, - }, + } _ => None, }; let new_t = { diff --git a/src/ir/term/mod.rs b/src/ir/term/mod.rs index 8f5662317..3cfeeec09 100644 --- a/src/ir/term/mod.rs +++ b/src/ir/term/mod.rs @@ -725,100 +725,80 @@ impl Array { } /// Iter - pub fn into_iter(&self) -> std::collections::btree_map::IntoIter { - self.map.clone().into_iter() + pub fn iter(&self) -> std::collections::btree_map::Iter { + self.map.iter() } } /// Merge two Array Iterators -pub struct ArrayMerge { - left: Peekable>>, - right: Peekable>>, - left_dfl: Value, - right_dfl: Value, +pub struct ArrayMerge<'a> { + left: Peekable>, + right: Peekable>, + left_dfl: &'a Value, + right_dfl: &'a Value, } -impl ArrayMerge { +impl<'a> ArrayMerge<'a> { /// 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() - ); - } + 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: 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> { - 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())) + 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().clone(), self.right.peek().clone()) { + (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)) } - Ordering::Equal => { - left_next = true; - right_next = true; - Some((l_ind.clone(), l_val.clone(), r_val.clone())) + (None, Some(_)) => { + let (r_ind, r_val) = self.left.next().unwrap(); + Some((r_ind, &self.left_dfl, r_val)) } - }, - (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(); - } - + (None, None) => None, + }; res } } From c8608b31d38e682f4200c6b77434d14698c377d1 Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Sat, 14 May 2022 19:57:50 -0400 Subject: [PATCH 13/14] linting --- src/front/zsharp/term.rs | 2 +- src/ir/opt/cfold.rs | 2 +- src/ir/term/mod.rs | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/front/zsharp/term.rs b/src/front/zsharp/term.rs index 38cf37885..1ae7b6f4b 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -911,7 +911,7 @@ 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.clone())); + 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)) } diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index d45215a1d..8dd060004 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -255,7 +255,7 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache) -> Term { a.size, ); let merge = ArrayMerge::new(a, b); - for (i, va, vb) in merge.into_iter() { + 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, diff --git a/src/ir/term/mod.rs b/src/ir/term/mod.rs index 3cfeeec09..847202516 100644 --- a/src/ir/term/mod.rs +++ b/src/ir/term/mod.rs @@ -773,7 +773,7 @@ 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().clone(), self.right.peek().clone()) { + 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(); @@ -791,11 +791,11 @@ impl<'a> Iterator for ArrayMerge<'a> { }, (Some(_), None) => { let (l_ind, l_val) = self.left.next().unwrap(); - Some((l_ind, l_val, &self.right_dfl)) + 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)) + Some((r_ind, self.left_dfl, r_val)) } (None, None) => None, }; From 8c5d3f79f877105f957fbe786c6f7a6c9ef7d35d Mon Sep 17 00:00:00 2001 From: Edward Chen Date: Sat, 14 May 2022 22:27:47 -0400 Subject: [PATCH 14/14] fixed asserts --- Cargo.lock | 18 ++++++------------ src/ir/term/mod.rs | 6 +++--- 2 files changed, 9 insertions(+), 15 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 692e5b51a..8f4dadf82 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -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", ] @@ -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", ] @@ -598,7 +598,7 @@ checksum = "bc5ac374b108929de78460075f3dc439fa66df9d8fc77e8f12caa5165fcf0c89" dependencies = [ "byteorder", "ff", - "rand_core 0.6.3", + "rand_core", "subtle", ] @@ -1062,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" @@ -1086,7 +1080,7 @@ version = "0.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa" dependencies = [ - "rand_core 0.5.1", + "rand_core", ] [[package]] diff --git a/src/ir/term/mod.rs b/src/ir/term/mod.rs index 3d8b104d1..7596ea65a 100644 --- a/src/ir/term/mod.rs +++ b/src/ir/term/mod.rs @@ -742,19 +742,19 @@ 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, + a.size == b.size, "IR Arrays have different lengths: {}, {}", a.size, b.size ); assert!( - a.key_sort != b.key_sort, + 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(), + a.default.sort() == b.default.sort(), "IR Arrays default values have different key sorts: {}, {}", a.default.sort(), b.default.sort()