Booster crash: custom hooked Map is stripped of the element sort after LLVM simplification

[virgil-serbanuta]

I have a query that makes the booster backend stop with an error, while it works when querying the Haskell backend directly.

Bug report: bug-report.zip

Output:

...
[Info#proxy] Starting RPC server
[Info] Process request 1 execute
[Info#proxy] Starting execute request
[Rewrite] Stopped after 0 steps. @(hs-backend-booster-0.0.0-DpKnlYxxzPeBfB7OJwCE7f:Booster.Pattern.Rewrite library/Booster/Pattern/Rewrite.hs:559:18)
[Rewrite] No rules applicable for the pattern Term:
...
Conditions:
    \equalsTerm{}(_<=Int_("0", VarARG_0:SortInt{}), "true") @(hs-backend-booster-0.0.0-DpKnlYxxzPeBfB7OJwCE7f:Booster.Pattern.Rewrite library/Booster/Pattern/Rewrite.hs:559:18)
[Rewrite] Applied simplification @(hs-backend-booster-0.0.0-DpKnlYxxzPeBfB7OJwCE7f:Booster.Pattern.Rewrite library/Booster/Pattern/Rewrite.hs:559:18)
[Rewrite] Retrying with simplified pattern @(hs-backend-booster-0.0.0-DpKnlYxxzPeBfB7OJwCE7f:Booster.Pattern.Rewrite library/Booster/Pattern/Rewrite.hs:559:18)
[Rewrite] Stopped after 0 steps. @(hs-backend-booster-0.0.0-DpKnlYxxzPeBfB7OJwCE7f:Booster.Pattern.Rewrite library/Booster/Pattern/Rewrite.hs:559:18)
[Rewrite] No rules applicable for the pattern Term:
...
Conditions:
    \equalsTerm{}(_<=Int_("0", VarARG_0:SortInt{}), "true") @(hs-backend-booster-0.0.0-DpKnlYxxzPeBfB7OJwCE7f:Booster.Pattern.Rewrite library/Booster/Pattern/Rewrite.hs:559:18)
[Info#proxy] Booster Stuck at Depth {getNat = 0}
[Info#proxy] Simplifying booster state and falling back to Kore 
[Info#proxy] Simplifying execution state
[Info#booster] Simplifying a pattern
[Warn#proxy] Unexpected failure when calling Kore simplifier, returning original term

Also, I'm getting this python stack trace + error:

Traceback (most recent call last):
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kore/rpc.py", line 742, in _request
    return self._client.request(method, **params)
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kore/rpc.py", line 238, in request
    return self._default_client.request(method, **params)
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kore/rpc.py", line 315, in request
    self._check(data)
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kore/rpc.py", line 327, in _check
    raise JsonRpcError(**response['error'])
pyk.kore.rpc.JsonRpcError: Could not verify pattern

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/usr/lib/python3.10/runpy.py", line 196, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "/usr/lib/python3.10/runpy.py", line 86, in _run_code
    exec(code, run_globals)
  File "/mnt/data/runtime-verification/elrond-wasm-real-elrond/kmxwasm/src/kmxwasm/property.py", line 337, in <module>
    main(sys.argv[1:])
  File "/mnt/data/runtime-verification/elrond-wasm-real-elrond/kmxwasm/src/kmxwasm/property.py", line 333, in main
    action.run()
  File "/mnt/data/runtime-verification/elrond-wasm-real-elrond/kmxwasm/src/kmxwasm/property.py", line 133, in run
    raise result.exception
  File "/mnt/data/runtime-verification/elrond-wasm-real-elrond/kmxwasm/src/kmxwasm/property_testing/running.py", line 147, in run_claim
    tools.explorer.extend(
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kcfg/explore.py", line 390, in extend
    _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute(
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kcfg/explore.py", line 81, in cterm_execute
    er = self._kore_client.execute(
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kore/rpc.py", line 782, in execute
    result = self._request('execute', **params)
  File "/home/virgil/.cache/pypoetry/virtualenvs/kmxwasm-CAf7Hewu-py3.10/lib/python3.10/site-packages/pyk/kore/rpc.py", line 745, in _request
    raise KoreClientError(message=err.message, code=err.code, data=err.data) from err
pyk.kore.rpc.KoreClientError: Could not verify pattern
code= 2
message= Could not verify pattern
data= {'context': ['\\and (<unknown location>)', "symbol or alias 'Lbl'-LT-'generatedTop'-GT-'' (<unknown location>)", "symbol or alias 'Lbl'-LT-'foundry'-GT-'' (<unknown location>)", "symbol or alias 'Lbl'-LT-'mandos'-GT-'' (<unknown location>)", "symbol or alias 'Lbl'-LT-'elrond'-GT-'' (<unknown location>)", "symbol or alias 'Lbl'-LT-'node'-GT-'' (<unknown location>)", "symbol or alias 'Lbl'-LT-'callState'-GT-'' (<unknown location>)", "symbol or alias 'Lbl'-LT-'wasm'-GT-'' (<unknown location>)", "symbol or alias 'Lbl'-LT-'instrs'-GT-'' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'kseq' (<unknown location>)", "symbol or alias 'inj' (<unknown location>)", "symbol or alias 'Lblframe'UndsUndsUndsUndsUnds'WASM'Unds'Frame'Unds'Int'Unds'ValTypes'Unds'ValStack'Unds'MapIntToVal' (<unknown location>)", "symbol or alias 'Lbl'Unds'MapIntToVal'Unds'' (<unknown location>)", "symbol or alias 'Lbl'Unds'Int2Val'Pipe'-'-GT-Unds'' (<unknown location>)", '(/mnt/data/runtime-verification/elrond-wasm-real-elrond/.kbuild/kmxwasm-semantics/0a9b8db/target/v6.0.108-0-g33a37fee9f-dirty/haskell/definition.kore 1215:71, <unknown location>)'], 'error': 'Expecting sort SortVal{} but got SortKItem{}.'}

[geo2a]

We likely need to change how we internalize/externalize Map. The request involves a customized type-safe map, which is hooked. Booster just assumes that it is the same that the built-in untyped Map and "forgets" the sorts of keys and elements, externalizing them as KItem.

@virgil-serbanuta could you point me to the definition of the customized Map, for reference?

[virgil-serbanuta]

Here is one such map: https://github.com/runtimeverification/wasm-semantics/blob/master/data/map-int-to-int.k

[geo2a]

Steps to reproduce in the mx-backend repository:

Build the semantics:

<checkout mx-backend>
git checkout booster-issue-321
git submodule update --init
cd kmxwasm/k-src/mx-semantics/
git checkout booster-issue-321
git submodule update --init
cd deps/wasm-semantics/
git checkout booster-issue-321
cd ../../..
kbuild kompile llvm-library

Run the proof:

cd kmxwasm
poetry run python3 -m src.kmxwasm.property \
    --claim src/tests/integration/data/test_change_quorum-int2val-spec.json \
    --kcfg=../.property/kcfg.json \
    --booster

This should produce an error ending with:

'error': 'Expecting sort SortVal{} but got SortKItem{}.'

[geo2a]

I've managed to get much closer to the problem, and it's not what we though it was. Looks like the problem manifests when we apply the init_local rule with concrete arguments, which invokes the MapIntToVal:primitiveUpdate function rule from the MAP-INT-TO-VAL-PRIMITIVE-CONCRETE module. This is a concrete module and the function is sent tothe LLVM backend for evaluation. I guess the LLVM backend does not play well with the custom hooked map and slaps an injection into KItem in top of the elements. When the resulting term is attempted to be re-internalized in Booster, we get the sorting error above.

[geo2a]

This commit defines an LLVM<>Booster integration test that demonstrates the error. When given a concrete term representing a singleton custom MapInt2Int, the LLVM backend returns it as the untyped Map.

Reduced error message:

   1) LLVM hooked Map simplifications should preserve singleton maps
         ✗ <interactive> failed at test/llvm-integration/LLVM.hs:158:76
           after 1 test.

               ┏━━ test/llvm-integration/LLVM.hs ━━━
           154 ┃ mapKItemInjProp :: Internal.API -> Property
           155 ┃ mapKItemInjProp api = property $ do
           156 ┃     let k = wrapIntTerm 1
           157 ┃     let v = intTerm 2
           158 ┃     LLVM.simplifyTerm api testDef (elem k v) (SortApp "SortMapInt2Int" []) === elem k v
               ┃     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
               ┃     │ ━━━ Failed (- lhs) (+ rhs) ━━━
               ┃     │   Term
               ┃     │     KMapF

               ┃     │       KMapDefinition
               ┃     │         { symbolNames =
               ┃     │             KCollectionSymbolNames
               ┃     │               { unitSymbolName = "Lbl'Stop'MapInt2Int"
               ┃     │               , elementSymbolName = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'"
               ┃     │               , concatSymbolName = "Lbl'Unds'MapInt2Int'Unds'"
               ┃     │               }
               ┃     │         , keySortName = "SortWrappedInt"
               ┃     │         , elementSortName = "SortInt"
               ┃     │         , mapSortName = "SortMapInt2Int"
               ┃     │         } [
               ┃     │         (
               ┃     │           Term
               ┃     │             (SymbolApplicationF
               ┃     │                Symbol
               ┃     │                  { name = "LblwrapInt"
               ┃     │                  , sortVars = []
               ┃     │                  , argSorts = [ SortApp "SortInt" [] ]
               ┃     │                  , resultSort = SortApp "SortWrappedInt" []
               ┃     │                  , attributes =
               ┃     │                      SymbolAttributes
               ┃     │                        { symbolType = TotalFunction
               ┃     │                        , isIdem = Flag False
               ┃     │                        , isAssoc = Flag False
               ┃     │                        , isMacroOrAlias = Flag False
               ┃     │                        , hasEvaluators = Flag True
               ┃     │                        , collectionMetadata = Nothing
               ┃     │                        }
               ┃     │                  }
               ┃     │                []
               ┃     │                [ Term
               ┃     │                    (DomainValueF (SortApp "SortInt" []) "1")
               ┃     │                ])
               ┃     │         , Term
               ┃     │ -           DomainValueF (SortApp "SortKItem" []) "8\NUL"
               ┃     │ +           DomainValueF (SortApp "SortInt" []) "2"
               ┃     │         )
               ┃     │       ]
               ┃     │       Nothing

We can see that what was 2:WrappedInt Int2Int|-> 2 has been turned into 2:WrappedInt Int2Int|-> 2:KItem, resulting in a sort error.

[geo2a]

Seems related: runtimeverification/llvm-backend#788

[geo2a]

@virgil-serbanuta we'll need to bring somebody who actively works on the LLVM backend to advise. @Baltoli could you have a look?

[Baltoli]

runtimeverification/llvm-backend#788 is indeed related; I think this is the same underlying problem - thanks for the reminder @geo2a. I will need to remind myself of the solution again as it's been a while since I looked at it, but as I recall the gist of it is for us to implement a new set of collection hooks in the backend that behave correctly with respect to sorting in this way.

[jberthold]

Workaround has been merged (correcting the sorts of updated maps from the LLVM backend). Awaiting fix from LLVM backend library.

[geo2a]

A fix has been shipped inti the LLVM backend: runtimeverification/llvm-backend#914

We should revert the workaround and see what happens.

[goodlyrottenapple]

I've confirmed that with the latest k version, removing our injection fix works for the unit test we originally added to test this behaviour. Do we want to revert the injection fix or leave it in case someone still uses an old version of the llvm-backend?

[Baltoli]

Revert your fix, I think - we shouldn't generally be in the habit of supporting old releases in that way.