Finite Data Structures

[AHaliq]

Finite Data Structures Experiments

Here we experiment implementing a Finite Map and Finite Set data structure. We tried 3 approaches

1. LinkedList and LinkedListNodup

These are our own defined structs and Iterator

The structs were tested with property based testing, verify with the following

cargo test

relevant files

• src/linkedlist/mod.rs
• tests/linkedlist_test.rs
• src/noduplist/mod.rs
• tests/linkedlistnodup_test.rs
• src/finset/linkedlistnodup.rs
• src/finmap/linkedlistnodup.rs

2. seq::Seq

An enum in the seq crate

The problem with seq is that it does not implement from_iter and its into_iter is implemented on a borrow of Self and not the type itself.

seq was intended to be used for modular reusable linked lists that can be composed with one another.

Our objective of making an encapsulated list-like data structure without having to manage sub lists is at odds with this design as evident with the numerous borrow checker errors in its development. The solution was to use alot of Copy and Box which goes against the point of Seq to begin with

relevant files

• src/seqlist/mod.rs

3. std::vec::Vec

Vec behaves exactly how we intended the list built on top of Seq supposed to

implementing finite map and finite set was very straightforward

leveraging sort and dedup functions to maintain unique elements in the structure

relevant files

• src/finset/vecset.rs
• src/finmap/vecmap.rs

Map and Set

The data structures themselves are defined with the following postconditions

We expressed them via the ensures macro

relevant files

• src/finset
• src/finmap

UPDATE

removed linkedlist and seq implementations

[AHaliq]

todo: look into property based testing

[spitters]

@AHaliq if you believe this is ready, you can remove the Draft status.
It would probably be good to remove LinkedList and Seq.
It's nice to see the experiments, but they should probably not be in the final version.
@franziskuskiefer Is hacspec/spec still the place where this should go, or is there a new version for hax?

[AHaliq]

the PR is ready. removed the Seq and LinkedList implementations

[annenkov]

Hi @AHaliq, the PR looks good! Looks like all the basic functionality is implemented. I think it is a very useful addition.

Just wanted to mention some small additions you might consider:

1. Implement Iterator (or IntoIterator for references). This would allow one to iterate over the contents without consuming the map/set.
2. add keys() and values(), but this is completely optional because it can be implemented using iterators. However, these methods are part of the standard collections, so they could be useful at some point.

[franziskuskiefer]

Thanks. I left a couple questions and suggestions.

[franziskuskiefer]

Please add some doc comments everywhere. Here should go what this crate is doing.

[franziskuskiefer]

What is this module doing? Please add some comments.

[franziskuskiefer]

keys and values functions usually return an iterator. You could also use a slice if iterators are too complex. What is the design rational behind using a vector here?

[AHaliq]

iterators are indeed complex, having to add lifetime variables to the trait and impl, seems like another battle with the borrowchecker.

I've also tried to look into slices, the issue is that the struct is a single vec of pairs, returning slices would require changing the struct to two parallel vecs one for keys another for values.

In light of this, should we change the struct? Or is Vec as a return type justified?

[franziskuskiefer]

insert usually returns the value that used to be in the map at k. What's the design rational behind returning a copy? Also, when returning the object itself, it should consume self. Similarly for remove.

[AHaliq]

   = help: message: For now, ensures clause don't work on function that have `&mut` inputs (see https://github.com/hacspec/hacspec-v2/issues/290)

If I understand your comment correctly, these functions ideally should mutate the struct rather than return a copy, however the design is as such due to the limitations in the ensures macro

Thus if this function were to return just the replaced value while being immutable, it is equivalent to get

[franziskuskiefer]

Similar comments to the map. What's the design rational for these functions, esp. in deviating from the common behaviour in Rust?

[AHaliq]

if its about not mutating the struct, again its due to the ensures macro

[spitters]

@AHaliq What is the status of this? I see you're waiting for some answers from @franziskuskiefer . Have you resolved his other suggestions?

[AHaliq]

@spitters yes, the other comments about the unecessary traits has been fixed but not pushed upstream yet. as for documentation, it would be best to finalize the functions before having to redo them again.