runtimeverification / hs-backend-booster

Accelerates K Framework's Haskell backend
BSD 3-Clause "New" or "Revised" License
7 stars 0 forks source link

Compute hashes correctly when constructing internalised collections #568

Closed geo2a closed 7 months ago

geo2a commented 7 months ago

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 Eq instance for Term to quilcky check if two terms are equal, akin to a Merkle tree.

Summary of changes:

ehildenb commented 7 months ago

We must have a testing harness for this, and multiple tests! Ideally unit and integration!

geo2a commented 7 months ago

Yeah, I'm adding unit tests now.

geo2a commented 7 months ago

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.

Test georgy-fix-collection-hashes time master-bafee82 time (georgy-fix-collection-hashes/master-bafee82) time
kontrol/test-emitcontracttest-testexpectemit-0-spec.k 53.79 116.85 0.4603337612323492
kontrol/test-storetest-testaccesses-0-spec.k 54.16 115.96 0.467057606071059
kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k 52.53 71.11 0.7387146674166785
mcd/flipper-ttl-pass-spec.k 59.66 78.15 0.7634037108125399
kontrol/test-allowchangestest-testallow_fail-0-spec.k 55.79 66.72 0.8361810551558753
kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k 81.23 96.83 0.8388929050913974
erc20/hkg/transferFrom-success-1-spec.k 66.82 77.02 0.867566865749156
mcd/vat-slip-pass-rough-spec.k 121.16 126.05 0.9612058706862356
kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k 51.62 49.78 1.036962635596625
mcd/vat-addui-fail-rough-spec.k 85.58 81.8 1.0462102689486552
erc20/ds/transferFrom-failure-1-a-spec.k 93.67 89.46 1.0470601386094345
mcd/vat-subui-fail-rough-spec.k 95.21 89.88 1.059301290609702
erc20/hkg/transferFrom-success-2-spec.k 77.34 66.35 1.165636774679729
kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k 70.87 57.4 1.2346689895470384
kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k 71.36 52.58 1.3571700266260935
kontrol/test-expectcalltest-testexpectregularcall-0-spec.k 117.04 51.96 2.252501924557352
TOTAL 1207.83 1287.9 0.9378290239925459
geo2a commented 7 months ago

KEVM performance at commit https://github.com/runtimeverification/hs-backend-booster/commit/3d58ba36c7870f9156f4cd2964f58add73c8133b with 1 worker

Test georgy-fix-collection-hashes time master-bafee82 time (georgy-fix-collection-hashes/master-bafee82) time
mcd/flopper-file-pass-rough-spec.k 439.37 463.1 0.9487583675232131
erc20/hkg/transferFrom-success-1-spec.k 64.09 66.82 0.9591439688715955
erc20/ds/transferFrom-failure-2-c-spec.k 57.93 55.79 1.038358128696899
erc20/ds/transferFrom-success-1-spec.k 98.77 94.32 1.0471798134011874
TOTAL 660.16 680.03 0.970780700851433