List type in specifications

[Calvin-L]

Right now specifications can have bags (i.e. multisets) and sets. Cozy can use lists in output implementations, but having lists in specifications would also be useful: often the order of insertion is important. This comes up especially in caches that employ least-recently-used eviction.

Wishlist:

• [x] List<_> type
• [x] list indexing xs[i] plus the usual operators (min, empty, ...)
• [x] list slicing xs[start:end]
• [x] sorting: sort xs to sort by natural order and sort {\x -> f(x)} xs to sort by another property
• [x] add_front, add_back, remove_front, and remove_back update operations (we may also want remove to remove an instance of a given element from the list)
• [ ] devise a good state maintenance sketch for lists (seems to be very hard!)

[prateekiiest]

can I work on this issue?

[mernst]

If you know what to do, then certainly. Please open a pull request with the fix. Thanks!

[izgzhen]

@Calvin-L I will help working out sort method for List type. I guess I need to:

• define new syntax
• define semantics in SMT solver
• define cost model
• codegen

[mernst]

@Calvin-L Does "devise a good state maintenance sketch" mean that one exists that is not good, or that none exists? (Also, in what file would that go? In state_maintenance.py? I didn't see anything about lists in there now.)

[Calvin-L]

Currently none exists. As a result, Cozy falls back to the default maintenance sketch, which is to recompute from scratch.