Skip to content

Conversation

@jberthold
Copy link
Member

Improves #4117 and removes temporary workaround #4133

The injection matcher was biased towards variable matching before, and returned a Fail prematurely if this failed.
The new preference is to check for unevaluated functions that return a supersort first (to return indeterminate), before trying to match a rule variable with supersort. If the source sorts are unrelated, the match can immediately fail.

@jberthold
Copy link
Member Author

jberthold commented Jan 29, 2026

KEVM Performance test

Test HOTFIX-indeterminate-match-for-supersort-function-under-injection time master-aa2aeb9b8 time (HOTFIX-indeterminate-match-for-supersort-function-under-injection/master-aa2aeb9b8) time
mcd-structured/flopper-dent-guy-same-pass-rough-spec.k 191.22 245.68 0.7783295343536307
mcd-structured/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k 222.91 282.18 0.7899567651853426
mcd/flipper-ttl-pass-spec.k 52.46 63.09 0.8315105404977017
mcd-structured/flopper-tick-pass-rough-spec.k 101.74 117.81 0.8635939224174518
mcd-structured/flopper-kick-pass-rough-spec.k 94.62 106.87 0.8853747543744737
mcd-structured/flapper-yank-pass-rough-spec.k 114.0 125.03 0.9117811725185956
mcd/flipper-bids-pass-rough-spec.k 95.14 100.97 0.9422600772506685
mcd/end-cash-pass-rough-spec.k 254.15 266.29 0.9544106049795336
mcd-structured/flipper-bids-pass-rough-spec.k 73.32 76.65 0.956555772994129
mcd-structured/dsvalue-read-pass-spec.k 64.36 67.28 0.9565992865636147
erc20/ds/transfer-failure-2-b-spec.k 59.87 62.09 0.9642454501530036
mcd/dai-adduu-fail-rough-spec.k 65.22 62.97 1.0357313006193425
erc20/hkg/transfer-failure-1-spec.k 75.25 72.53 1.0375017234247896
benchmarks/encodepacked-keccak01-spec.k 61.21 58.95 1.0383375742154368
erc20/hkg/transferFrom-success-1-spec.k 74.64 71.45 1.0446466060181945
mcd-structured/flipper-addu48u48-fail-rough-spec.k 66.57 63.67 1.0455473535416993
mcd/dai-symbol-pass-spec.k 66.32 63.19 1.04953315398006
mcd/flopper-kick-pass-rough-spec.k 141.88 118.35 1.198817068018589
TOTAL 1874.88 2025.05 0.9258438063257697

@jberthold
Copy link
Member Author

Confirmed that the booster-dev tests for EVM-semantics are now passing (3 failures before).

@jberthold jberthold merged commit 830d8c3 into master Jan 29, 2026
6 checks passed
@jberthold jberthold deleted the HOTFIX-indeterminate-match-for-supersort-function-under-injection branch January 29, 2026 21:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants