From 16b2364af272011576e29f205df48c6b43d341f2 Mon Sep 17 00:00:00 2001 From: Abdul Haliq Date: Thu, 7 Dec 2023 13:00:54 +0100 Subject: [PATCH 1/4] fin: project init --- Cargo.toml | 1 + findatastructures/Cargo.toml | 16 ++++++++++++++++ findatastructures/src/lib.rs | 7 +++++++ 3 files changed, 24 insertions(+) create mode 100644 findatastructures/Cargo.toml create mode 100644 findatastructures/src/lib.rs diff --git a/Cargo.toml b/Cargo.toml index 4e06422..6ed5129 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -23,4 +23,5 @@ members = [ "pasta", "halo2", "weierstrass-curves", + "findatastructures", ] diff --git a/findatastructures/Cargo.toml b/findatastructures/Cargo.toml new file mode 100644 index 0000000..9b1cc5d --- /dev/null +++ b/findatastructures/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "findatastructures" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + + +[lib] +path = "src/lib.rs" + +[dependencies] +hax-lib-macros = { git = "https://github.com/hacspec/hax.git" } + +[dev-dependencies] +findatastructures = { path = "." } diff --git a/findatastructures/src/lib.rs b/findatastructures/src/lib.rs new file mode 100644 index 0000000..f3f5f02 --- /dev/null +++ b/findatastructures/src/lib.rs @@ -0,0 +1,7 @@ +mod finmap; +mod finset; + +pub use finmap::FinMap; +pub use finmap::FinMapVec; +pub use finset::FinSet; +pub use finset::FinSetVec; From 51030a57e0a2e4fecfb0aeb36ad18ade511474c9 Mon Sep 17 00:00:00 2001 From: Abdul Haliq Date: Thu, 7 Dec 2023 13:01:46 +0100 Subject: [PATCH 2/4] fin: implement finset --- findatastructures/src/finset/mod.rs | 29 +++++ findatastructures/src/finset/vecset.rs | 168 +++++++++++++++++++++++++ 2 files changed, 197 insertions(+) create mode 100644 findatastructures/src/finset/mod.rs create mode 100644 findatastructures/src/finset/vecset.rs diff --git a/findatastructures/src/finset/mod.rs b/findatastructures/src/finset/mod.rs new file mode 100644 index 0000000..6f0daad --- /dev/null +++ b/findatastructures/src/finset/mod.rs @@ -0,0 +1,29 @@ +pub trait FinSet: PartialEq + Clone { + /// The type of values in the set + type V; + + /// Create a new empty set + fn new() -> Self; + /// Check if the set contains a value + fn contains(&self, v: &Self::V) -> bool; + /// Insert a value into the set + fn insert(&self, v: Self::V) -> Self; + /// Remove a value from the set + fn remove(&self, v: &Self::V) -> Self; + /// Check if the set is empty + fn is_empty(&self) -> bool; + /// Get the number of values in the set + fn len(&self) -> usize; + + /// Create a union with another set + fn union(&self, other: &Self) -> Self; + /// Create an intersection with another set + fn intersection(&self, other: &Self) -> Self; + /// Create a difference with another set + fn difference(&self, other: &Self) -> Self; + /// Create a symmetric difference with another set + fn symmetric_difference(&self, other: &Self) -> Self; +} + +pub mod vecset; +pub use vecset::FinSetVec; diff --git a/findatastructures/src/finset/vecset.rs b/findatastructures/src/finset/vecset.rs new file mode 100644 index 0000000..5943bcd --- /dev/null +++ b/findatastructures/src/finset/vecset.rs @@ -0,0 +1,168 @@ +use crate::finset::FinSet; +use hax_lib_macros as hax; +use std::vec::Vec; + +/// A set implemented as a `Vec` with no duplicates +#[derive(Clone, PartialEq)] +pub struct FinSetVec +where + V: Clone + PartialEq + Ord, +{ + vec: Vec, +} + +impl FinSet for FinSetVec +where + V: Copy + PartialEq + Ord, +{ + /// The type of values in the set + type V = V; + + /// Create a new empty set + #[hax::ensures(|result| + forall(|v : Self::V| !result.contains(&v) && + result.is_empty() && + forall(|v : Self::V| result.remove(&v) == result) && + (result.len() == 0)) + )] + fn new() -> Self { + FinSetVec { vec: Vec::new() } + } + + /// Check if the set contains a value + #[hax::ensures(|result| + (result == !self.is_empty()) && + (result == (self.remove(v).len() == self.len() - 1)) + )] + fn contains(&self, v: &V) -> bool { + self.vec.contains(v) + } + + /// Insert a value into the set + #[hax::ensures(|result| + result.contains(v) && + !result.is_empty() && + (!self.contains(v) == (result.remove(v) == self)) && + (self.len() <= result.len() && result.len() <= self.len() + 1) && + (result.remove(v) == self) && + (result.insert(v) == result) + )] + fn insert(&self, v: V) -> Self { + let mut new = self.clone(); + if new.is_empty() || !new.contains(&v) { + new.vec.push(v); + } + new + } + + /// Remove a value from the set + #[hax::ensures(|result| + ((result.len() == self.len()) == !self.contains(v)) && + (self.len() - 1 <= result.len() && result.len() <= self.len()) && + (result.insert(v) == self) && + (result.remove(v) == result) + )] + fn remove(&self, v: &Self::V) -> Self { + let mut new = self.clone(); + new.vec.retain(|x| x != v); + new + } + + /// Check if the set is empty + #[hax::ensures(|result| + forall(|v : Self::V| result == !self.contains(&v)) && + forall(|v : Self::V| result == (self.remove(v) == self)) && + (result == (self.len() == 0)) + )] + fn is_empty(&self) -> bool { + self.vec.is_empty() + } + + /// Get the number of values in the set + #[hax::ensures(|result| + (self.is_empty() == (result == 0)) && + result >= 0 + )] + fn len(&self) -> usize { + self.vec.len() + } + + /// Create a union with another set + #[hax::ensures(|result| + forall(|v : Self::V| self.contains(&v) && other.contains(&v) == result.contains(&v)) && + (other != self || result == self) && + (result == other.union(self)) && + forall(|s : Self| self.union(other.union(s)) == (self.union(other)).union(s)) + )] + fn union(&self, other: &Self) -> Self { + let mut new = self.clone(); + new.vec.extend(other.vec.iter().cloned()); + new.vec.sort(); + new.vec.dedup(); + new + } + + /// Create an intersection with another set + #[hax::ensures(|result| + forall(|v : Self::V| self.contains(&v) && other.contains(&v) == result.contains(&v)) && + (other != self || result == self) && + (result == other.intersection(self)) && + forall(|s : Self| self.intersection(other.intersection(s)) == (self.intersection(other)).intersection(s)) + )] + fn intersection(&self, other: &Self) -> Self { + let mut new = self.clone(); + new.vec.retain(|x| other.contains(x)); + new + } + + /// Create a difference with another set + #[hax::ensures(|result| + forall(|v : Self::V| self.contains(&v) && !other.contains(&v) == result.contains(&v)) && + (other != self || result.is_empty()) + )] + fn difference(&self, other: &Self) -> Self { + let mut new = self.clone(); + let other = other.clone(); + new.vec.retain(|x| !other.contains(x)); + new + } + + /// Create a symmetric difference with another set + #[hax::ensures(|result| + forall(|v : Self::V| (self.contains(&v) != other.contains(&v)) == result.contains(&v)) && + (other != self || result.is_empty()) && + (result == other.symmetric_difference(self)) && + forall(|s : Self| self.symmetric_difference(other.symmetric_difference(s)) == (self.symmetric_difference(other)).symmetric_difference(s)) && + (result == self.union(other).difference(self.intersection(other))) + )] + fn symmetric_difference(&self, other: &Self) -> Self { + self.difference(other).union(&other.difference(self)) + } +} + +impl IntoIterator for FinSetVec +where + V: Clone + PartialEq + Ord, +{ + type Item = V; + type IntoIter = std::vec::IntoIter; + + /// Create an iterator over a set + fn into_iter(self) -> Self::IntoIter { + self.vec.into_iter() + } +} + +impl FromIterator for FinSetVec +where + V: Copy + Clone + PartialEq + Ord, +{ + /// Create a set from an iterator + fn from_iter>(iter: I) -> Self { + let mut new = FinSetVec::new(); + new.vec = iter.into_iter().collect(); + new.vec.sort(); + new.vec.dedup(); + new + } +} From 2ea57208328927f436e801ed1ad9e35c753199d6 Mon Sep 17 00:00:00 2001 From: Abdul Haliq Date: Thu, 7 Dec 2023 13:03:11 +0100 Subject: [PATCH 3/4] fin: implement finmap --- findatastructures/src/finmap/mod.rs | 24 +++++ findatastructures/src/finmap/vecmap.rs | 138 +++++++++++++++++++++++++ 2 files changed, 162 insertions(+) create mode 100644 findatastructures/src/finmap/mod.rs create mode 100644 findatastructures/src/finmap/vecmap.rs diff --git a/findatastructures/src/finmap/mod.rs b/findatastructures/src/finmap/mod.rs new file mode 100644 index 0000000..91871bc --- /dev/null +++ b/findatastructures/src/finmap/mod.rs @@ -0,0 +1,24 @@ +pub trait FinMap: PartialEq + Clone { + /// The type of keys in the map + type K; + /// The type of values in the map + type V; + + /// Create a new empty map + fn new() -> Self; + /// Check if the map contains a key + fn contains_key(&self, k: &Self::K) -> bool; + /// Insert a key-value pair into the map + fn insert(&self, k: Self::K, v: Self::V) -> Self; + /// Get the value associated with a key + fn get(&self, k: &Self::K) -> Option<&Self::V>; + /// Remove a key-value pair from the map + fn remove(&self, k: &Self::K) -> Self; + /// Check if the map is empty + fn is_empty(&self) -> bool; + /// Get the number of key-value pairs in the map + fn len(&self) -> usize; +} + +pub mod vecmap; +pub use vecmap::FinMapVec; diff --git a/findatastructures/src/finmap/vecmap.rs b/findatastructures/src/finmap/vecmap.rs new file mode 100644 index 0000000..b91d66e --- /dev/null +++ b/findatastructures/src/finmap/vecmap.rs @@ -0,0 +1,138 @@ +use crate::finmap::FinMap; +use hax_lib_macros as hax; +use std::vec::Vec; + +/// A set implemented as a `Vec` with no duplicates +#[derive(Clone, PartialEq)] +pub struct FinMapVec +where + K: Copy + PartialEq + Ord, + V: Copy + PartialEq, +{ + vec: Vec<(K, V)>, +} + +impl FinMap for FinMapVec +where + K: Copy + PartialEq + Ord, + V: Copy + PartialEq, +{ + /// The type of keys in the map + type K = K; + /// The type of values in the map + type V = V; + + /// Create a new empty map + #[hax::ensures(|result| + forall(|k : Self::K| !result.contains_key(k)) && + result.is_empty() && + forall(|k : Self::K| result.get(k) == None) && + forall(|k : Self::K| result.remove(k) == result) && + (result.len() == 0) + )] + fn new() -> Self { + FinMapVec { vec: Vec::new() } + } + + /// Check if the map contains a key + #[hax::ensures(|result| + (!result || !self.is_empty()) && + (result == (self.get(k) != None)) && + (result == (self.remove(k).len() == self.len() - 1)) && + forall(|v : Self::V| !result == (self.insert(k, v).remove(k) == self)) + )] + fn contains_key(&self, k: &K) -> bool { + self.vec.iter().any(|(k2, _)| k == k2) + } + + /// Insert a key-value pair into the map + #[hax::ensures(|result| + result.contains_key(k) && + !result.is_empty() && + (result.get(k) == Some(v)) && + (result.remove(k).get(k) == None) && + (self.len() <= result.len() && result.len() <= self.len() + 1) && + forall(|v2 : Self::V| result.insert(k, v2) == self.insert(k, v2)) + )] + fn insert(&self, k: K, v: V) -> Self { + let mut new = self.clone(); + if new.is_empty() || !new.contains_key(&k) { + new.vec.push((k, v)); + } + new + } + + /// Get the value associated with a key + #[hax::ensures(|result| + ((result == None) == !self.contains_key(k)) && + ((result != None) == !self.is_empty()) && + ((result != None) == (self.remove(k).len() == self.len() - 1)) && + ((result == None) == (self.remove(k).len() == self.len())) + )] + fn get(&self, k: &K) -> Option<&V> { + self.vec.iter().find(|(k2, _)| k == k2).map(|(_, v)| v) + } + + /// Remove a key-value pair from the map + #[hax::ensures(|result| + ((result.len() == self.len()) == !self.contains_key(k)) && + ((result.len() == self.len()) == (self.get(k) == None)) && + (self.len() - 1 <= result.len() && result.len() <= self.len()) && + (result.remove(k) == result) && + forall(|v : Self::V| result.insert(k, v) = self.insert(k, v)) + )] + fn remove(&self, k: &K) -> Self { + let mut new = self.clone(); + new.vec.retain(|(k2, _)| k != k2); + new + } + + /// Check if the map is empty + #[hax::ensures(|result| + forall(|k : Self::K| result == !result.contains_key(k)) && + forall(|k : Self::K| result == (self.get(k) == None)) && + forall(|k : Self::K| result == (self.remove(k) == self)) && + (result == (self.len() == 0)) + )] + fn is_empty(&self) -> bool { + self.vec.is_empty() + } + + /// Get the number of key-value pairs in the map + #[hax::ensures(|result| + (self.is_empty() == (result == 0)) && + (result >= 0) + )] + fn len(&self) -> usize { + self.vec.len() + } +} + +impl IntoIterator for FinMapVec +where + K: Copy + PartialEq + Ord, + V: Copy + PartialEq, +{ + type Item = (K, V); + type IntoIter = std::vec::IntoIter; + + /// Create an iterator over the map + fn into_iter(self) -> Self::IntoIter { + self.vec.into_iter() + } +} + +impl FromIterator<(K, V)> for FinMapVec +where + K: Copy + PartialEq + Ord, + V: Copy + PartialEq, +{ + /// Create a new map from an iterator + fn from_iter>(iter: I) -> Self { + let mut new = FinMapVec::new(); + new.vec = iter.into_iter().collect(); + new.vec.sort_by(|(k1, _), (k2, _)| k1.cmp(k2)); + new.vec.dedup_by(|(k1, _), (k2, _)| k1 == k2); + new + } +} From 79318072a496443d628ee5864a973bd65b7f3446 Mon Sep 17 00:00:00 2001 From: Abdul Haliq Date: Sat, 9 Dec 2023 09:30:05 +0100 Subject: [PATCH 4/4] fin: implement iterator on borrows --- findatastructures/src/finmap/mod.rs | 4 ++++ findatastructures/src/finmap/vecmap.rs | 28 ++++++++++++++++++++++++++ findatastructures/src/finset/vecset.rs | 13 ++++++++++++ 3 files changed, 45 insertions(+) diff --git a/findatastructures/src/finmap/mod.rs b/findatastructures/src/finmap/mod.rs index 91871bc..62a8695 100644 --- a/findatastructures/src/finmap/mod.rs +++ b/findatastructures/src/finmap/mod.rs @@ -18,6 +18,10 @@ pub trait FinMap: PartialEq + Clone { fn is_empty(&self) -> bool; /// Get the number of key-value pairs in the map fn len(&self) -> usize; + /// Get the keys in the map + fn keys(&self) -> Vec<&Self::K>; + /// Get the values in the map + fn values(&self) -> Vec<&Self::V>; } pub mod vecmap; diff --git a/findatastructures/src/finmap/vecmap.rs b/findatastructures/src/finmap/vecmap.rs index b91d66e..6438e3a 100644 --- a/findatastructures/src/finmap/vecmap.rs +++ b/findatastructures/src/finmap/vecmap.rs @@ -106,6 +106,20 @@ where fn len(&self) -> usize { self.vec.len() } + + #[hax::ensures(|result| + forall(|v: Self::V| result.contains(&v) == self.contains_key(&v)) + )] + fn keys(&self) -> Vec<&Self::K> { + self.into_iter().map(|(k, _)| k).collect() + } + + #[hax::ensures(|result| + forall(|k: Self::K| result.contains(&k) == self.get(&k).is_some()) + )] + fn values(&self) -> Vec<&Self::V> { + self.into_iter().map(|(_, v)| v).collect() + } } impl IntoIterator for FinMapVec @@ -122,6 +136,20 @@ where } } +impl<'a, K, V> IntoIterator for &'a FinMapVec +where + K: Copy + PartialEq + Ord, + V: Copy + PartialEq, +{ + type Item = &'a (K, V); + type IntoIter = std::slice::Iter<'a, (K, V)>; + + /// Create an iterator over the map + fn into_iter(self) -> Self::IntoIter { + self.vec.iter() + } +} + impl FromIterator<(K, V)> for FinMapVec where K: Copy + PartialEq + Ord, diff --git a/findatastructures/src/finset/vecset.rs b/findatastructures/src/finset/vecset.rs index 5943bcd..9e3b252 100644 --- a/findatastructures/src/finset/vecset.rs +++ b/findatastructures/src/finset/vecset.rs @@ -153,6 +153,19 @@ where } } +impl<'a, V> IntoIterator for &'a FinSetVec +where + V: Copy + PartialEq + Ord, +{ + type Item = &'a V; + type IntoIter = std::slice::Iter<'a, V>; + + /// Create an iterator over a set + fn into_iter(self) -> Self::IntoIter { + self.vec.iter() + } +} + impl FromIterator for FinSetVec where V: Copy + Clone + PartialEq + Ord,