-
Notifications
You must be signed in to change notification settings - Fork 233
Improving the sequence library
Jay Bosamiya edited this page Oct 25, 2018
·
5 revisions
Summarizing some discussions about the sequence library, gathering pain points and areas for improvement.
Aymeric:
- Need to call Seq.equal explicitly (JP: not sure there's much hope about this)
- Redundancy between BufferViews and the endianness lemmas in FStar.Kremlin.Endianness
- Had to re-do because stuff wasn't in ulib (move FStar.Kremlin.Endianness?)
- Vale uses nat64 (incompatible with UInt64.t)
- Manual calls: index/append, index/slice... doesn't seem to trigger well
Chris:
The axiom profiler points to our old friend,
FStar.Seq.Properties.slice_slice
. @nik and I have looked atslice_slice
before and it looks completely innocent, but somehow it keeps showing up with enormous terms in a wide variety of situations. We believe it's not actually an infinite matching loop, but more of a large, yet, bounded matching explosion. Maybe it's time to figure out once and for all what's going on.
Tahina:
- Knew about the index_slice pattern with an unguarded forall in the post-condition.
- Claims that this: https://github.com/FStarLang/FStar/commit/a5df41ce315f0e38569c555c06327f3af577fd9f makes things behave better (but caused regressions, so not merged).
Jonathan:
- For the SHA algorithms, needed to add (with help from Tahina) these lemmas https://github.com/project-everest/hacl-star/blob/fstar-master/code/hash-new/Hacl.Hash.Lemmas.fst which make a lot of proofs go through more efficiently
- Note this bit: https://github.com/project-everest/hacl-star/blob/fstar-master/code/hash-new/Hacl.Hash.Core.SHA2.fst#L191 -- I had to call these lemmas myself and don't understand why index_slice didn't trigger properly
Bryan:
- Better organization and documentation of the sequence libraries (as well as guidance as to what goes in Base vs. Properties).
- Easier ways to opt into/out of SMT pats?
Jay:
- Patterns seem to break badly when combined with arithmetic (for example, see comment on line 48: https://github.com/jaybosamiya/poly1305-equivalence/blob/master/UsefulLemmas.fst#L48)
- Depending on whether you use
.[]
orindex
(or similarly for update), the patterns sometimes just break, with no clear indication of when/how (I don't have exact examples for this unfortunately). - Some lemmas that (imho) should have "obvious" patterns don't (eg: on
append_cons
). Possibly this is to curb explosion, but important to look into to increase productivity. - Agree 100% with the ability to opt-in/opt-out for patterns.
- Having a uniform style for the library (eg: all lemmas start with
lemma_{mostimportantfunc}_
) would be extremely useful for productivity. At the moment, the library is about 1500 LOC, and due to not having some kind of uniform style/documentation, it requires either mentally keeping track of all that exists (with its specific names "was itappend_cons
or was itlemma_append_cons
or was itcons_append
orlemma_cons_append
"), or re-reading the file multiple times. This is more of a styling issue, but it's good to keep in mind when we're working on improving it.