Compute hashes correctly when constructing internalised collections #568
Conversation
|
We must have a testing harness for this, and multiple tests! Ideally unit and integration! |
geo2a
force-pushed
the
georgy/fix-collection-hashes
branch
from
3dcf217
to
3d58ba3
Compare
|
Yeah, I'm adding unit tests now. |
|
KEVM performance at commit b7aac44 with 3 workers. The numbers may be skewed and the code is still wrong anyway. I'm rerunning with 3d58ba3 and 1 worker.
|
library/Booster/Pattern/Base.hs
Outdated
| (keyVals', rest') = case rest of | ||
| Just (KMap def' kvs r) | def' == def -> (kvs, r) | ||
| Just (KMap def' kvs r) | def' == def -> (sortAndDeduplicate kvs, r) |
There was a problem hiding this comment.
(nit) probably not necessary to deduplicate here, as this list comes from a KMap (with this change, we add an invariant that the list should always be sorted and without duplicates)
There was a problem hiding this comment.
True. I've added this only because of this unit test that manually constructs a nested KMap with a broken invariant. This should never happen thought, so probably safe to remove the call to sortAndDeduplicate form here and also from the same case in KSet.
| Gen.int (Range.linear 0 1024) | ||
| let setTerm = makeKSetNoRest xs | ||
| res <- LLVM.simplifyTerm api testDef setTerm (SortApp "SortSet" []) | ||
| res === Right (setAsConcat . map wrapIntTerm $ xs) |
There was a problem hiding this comment.
The way this is failing in CI indicates that the smart constructor for SymbolApplication is not generating the expected KSet (both res and the setAsConcat result are not KSets).
There was a problem hiding this comment.
Thanks for the thorough investigation @jberthold. I have to admit I though the test would ensure that the LLVM backend does not change the ordering of concrete sets (or would detect if it did), but upon introducing the changes, we are already comparing two internalised sets, which now de-duplicate and sort themselves, so I'm not sure if this test is helpful in the end.
test/llvm-integration/LLVM.hs
Outdated
| , concatSymbolName = "Lbl'Unds'Set'Unds'" | ||
| } | ||
| , elementSortName = "SortKItem" | ||
| , listSortName = "SortList" |
There was a problem hiding this comment.
| , listSortName = "SortList" | |
| , listSortName = "SortSet" |
There was a problem hiding this comment.
As it turns out, there is more to fix... the definition in the LLVM.hs file does not have the collection metadata on SortSet and the (SetItem, _Set_, .Set).
The whole definition is outdated and we should update it (see displayTestDef).
After adding the metadata locally, I found that setAsConcat is not generating the right thing...
test/llvm-integration/LLVM.hs
Outdated
| foldl1' | ||
| ( \x y -> | ||
| SymbolApplication | ||
| (defSymbols Map.! sortSetKSet.symbolNames.concatSymbolName) | ||
| [] | ||
| [singletonSet x, singletonSet y] | ||
| ) |
There was a problem hiding this comment.
As I found after fixing the metadata for SortSet, this will produce nested sets when applied to a list with more than two elements: [1, 2, 3] maps to { 3, {2, 1}} (paraphrased) (thanks to the generous KItem sorting, this is even -almost- allowed, but the construction does not have the required injections).
| foldl1' | |
| ( \x y -> | |
| SymbolApplication | |
| (defSymbols Map.! sortSetKSet.symbolNames.concatSymbolName) | |
| [] | |
| [singletonSet x, singletonSet y] | |
| ) | |
| foldl1' | |
| ( \x y -> | |
| SymbolApplication | |
| (defSymbols Map.! sortSetKSet.symbolNames.concatSymbolName) | |
| [] | |
| [x, y] | |
| ) . map singletonSet |
|
KEVM performance at commit 3d58ba3 with 1 worker
|
geo2a
force-pushed
the
georgy/fix-collection-hashes
branch
from
500715b
to
9f5ed34
Compare
This PR fixes a bug in the computation of the synthesis bottom-up hash attribute of
Terms representing internalised maps and sets.These hashes are used in the
Eqinstance forTermto quilcky check if two terms are equal, akin to a Merkle tree.Summary of changes:
KMapandKSetpattern-synonyms compute the hashes;foldl'rather thanfoldrin some of the cases, as we should use the left fold for data as rule of thumb for better performance. I did not check the impact of this commit specifically though;