[Haskell-Performance] kevm proof slow with extra side conditions

[ehildenb]

Please Prepare Test Data

I have a specification on KEVM: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/benchmarks/storagevar03-spec.k

This can be run with: make tests/specs/benchmarks/storagevar03-spec.k.prove after building KEVM.

It has some side-conditions for validity on the input state: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/benchmarks/storagevar03-spec.k#L116. But these side-conditions are actually not needed (the lines CONTRACT_ID >Int 0 andBool notBool #isPrecompiledAccount(CONTRACT_ID, BYZANTIUM)), so I removed them.

Removing these 4 conditions (on CONTRACT_ID and CALLEE_ID) ends up improving the performance by ~2.5X.

So it seems that having these extra side-conditions is causing a big performance slowdown.

I've attached 2 bug reports:

• kevm-bug-storagevar03-with-conditions.tar.gz, which is run with the extra conditions as linked above, which takes 269.4s on my machine.
• kevm-bug-storagevar03-without-conditions.tar.gz which is run with those conditions removed and takes 117.31s my machine.

These conditions should not change their simplification status through the whole proof beyond startup, so I guess I'm wondering why it takes so much longer to run with these extra conditions. We should try evaluating them once, and then basically know that they can't be simplified any further throughout the rest of execution (so should not try).

[ehildenb]

@F-WRunTime it seems that it cannot detect that I'm a member of the org? https://github.com/runtimeverification/haskell-backend/actions/runs/3148634684/jobs/5119382938

[ehildenb]

Also, it seems to create too many jobs:

[ehildenb]

dummy comment to trigger workflow

[ehildenb]

Test me.

[ehildenb]

Test me.

[jberthold]

Ran the two tarballs in a separate ticket #3303 . Nothing immediately suspicious in the profiles, but the top consumers differ to significant extent:

with-conditions

COST CENTRE	MODULE	SRC	%time	%alloc
hashWithSalt	Kore.Internal.TermLike.TermLike	src/Kore/Internal/TermLike/TermLike.hs:698:5-77	4.7	4.7
hashWithSalt1	Data.Hashable.Class	Data/Hashable/Class.hs:271:1-45	1.8	1.4
ravel	Data.Generics.Internal.VL.Lens	src/Data/Generics/Internal/VL/Lens.hs:66:1-42	1.8	1.6
guardAgainstBottom	Kore.TopBottom	src/Kore/TopBottom.hs:45:1-49	1.4	0.8
addConditionWithReplacements	Kore.Internal.SideCondition	src/Kore/Internal/SideCondition.hs:(310,1)-(333,29)	1.4	1.0
simplifySubstitutionWorker	Kore.Simplify.SubstitutionSimplifier	src/Kore/Simplify/SubstitutionSimplifier.hs:(267,1)-(399,78)	1.4	1.8
unionWith	Data.Map.Strict.Internal	src/Data/Map/Strict/Internal.hs:(990,1)-(996,35)	1.4	0.8
compare	Data.InternedText	src/Data/InternedText.hs:(82,5)-(86,61)	1.4	0.0
liftSimplifier	Kore.Simplify.Simplify	src/Kore/Simplify/Simplify.hs:192:5-42	1.3	1.7
compare	Kore.Rewrite.RewritingVariable	src/Kore/Rewrite/RewritingVariable.hs:75:25-27	1.2	0.0
fmap	Kore.Internal.Predicate	src/Kore/Internal/Predicate.hs:171:21-27	1.2	0.3
repIso	Data.Generics.Internal.Profunctor.Iso	src/Data/Generics/Internal/Profunctor/Iso.hs:38:1-20	1.1	2.6
substitute	Kore.Internal.TermLike.TermLike	src/Kore/Internal/TermLike/TermLike.hs:(850,5)-(948,57)	1.1	1.4

without-conditions

COST CENTRE	MODULE	SRC	%time	%alloc
hashWithSalt	Kore.Internal.TermLike.TermLike	src/Kore/Internal/TermLike/TermLike.hs:698:5-77	8.4	8.8
addConditionWithReplacements	Kore.Internal.SideCondition	src/Kore/Internal/SideCondition.hs:(310,1)-(333,29)	3.6	2.4
liftSimplifier	Kore.Simplify.Simplify	src/Kore/Simplify/Simplify.hs:192:5-42	3.0	4.3
hashWithSalt1	Data.Hashable.Class	Data/Hashable/Class.hs:271:1-45	2.2	2.4
fmap	Kore.Internal.Predicate	src/Kore/Internal/Predicate.hs:171:21-27	1.5	0.5
ravel	Data.Generics.Internal.VL.Lens	src/Data/Generics/Internal/VL/Lens.hs:66:1-42	1.4	1.3
compare	Data.InternedText	src/Data/InternedText.hs:(82,5)-(86,61)	1.3	0.0
project	Kore.Internal.Predicate	src/Kore/Internal/Predicate.hs:(325,5)-(327,67)	1.2	4.8
compare	Kore.Internal.TermLike.TermLike	src/Kore/Internal/TermLike/TermLike.hs:(692,5)-(695,29)	1.2	0.0
simplifySubstitutionWorker	Kore.Simplify.SubstitutionSimplifier	src/Kore/Simplify/SubstitutionSimplifier.hs:(267,1)-(399,78)	1.1	1.3

[ana-pantilie]

Blocked on #3113, because the highest cost center is hashing. After that is fixed, we should reinvestigate.