[namasikanam]

There are a few new lemmas and four new operators:

• isprefix: whether one list is a prefix of the other list
• prefixes: the sets of all prefixes of a list
• interval: a consecutive subsequence of a list
• rfind: reverse finding (start from the end of the list)

Also, I reduced smt usage in some old proofs, as smt solving in those proof fails on my machine. I believe these updates only make proofs better :)

[strub]

@namasikanam Did you change some lemmas?

[fdupress]

The SHA3 one could be a smt(@List) that blows up with new lemmas. The stdlib failure is inside List itself, so likely one of the new lemmas. (Different SMT environment between @namasikanam's machine and the docker?)

[namasikanam]

I didn't change any statement of existing lemmas (only update some proofs when they are not running on my machine). I coudn't find smt(@List) in SHA3, either. Do not understand why sha-3 is broken. I will try to reproduce the failure in a local docker.

[strub]

I didn't change any statement of existing lemmas (only update some proofs when they are not running on my machine). I didn't find smt(@List). Do not understand why sha-3 is broken. I will try to reproduce the failure in a local docker.

Maybe the sha3 dev contains rogue smt?

[namasikanam]

Maybe the sha3 dev contains rogue smt?

I fixed the inconsistency in docker. I couldn't reproduce the failure for SHA3. But it turned out that the failure in SHA3 gets also resolved magically :)

[namasikanam]

I will always test within docker before creating a PR in the future :)