`call` causes state splitting

[hjorthjort]

The below screenshot of the execution graph in the Haskell backend shows the splitting at axiom 112, which is call. The splitting occurs in node 94 and 111.

This is when calling the "main" function of wrc20 after the module has been loaded.

Axiom 112

Kore (95)> axiom 112
\rewrites{SortGeneratedTopCell{}}(
    \and{SortGeneratedTopCell{}}(
        \top{SortGeneratedTopCell{}}(),
        Lbl'-LT-'generatedTop'-GT-'{}(
            Lbl'-LT-'ewasm'-GT-'{}(
                Var'Unds'23:SortEeiCell{},
                Lbl'-LT-'wasm'-GT-'{}(
                    Lbl'-LT-'k'-GT-'{}(
                        kseq{}(
                            /* Inj: */ inj{SortPlainInstr{}, SortKItem{}}(
                                Lblcall'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(
                                    VarTFIDX:SortIndex{}
                                )
                            ),
                            VarDotVar3:SortK{}
                        )
                    ),
                    Var'Unds'16:SortValstackCell{},
                    Lbl'-LT-'curFrame'-GT-'{}(
                        Var'Unds'0:SortLocalsCell{},
                        Var'Unds'1:SortLocalIdsCell{},
                        Lbl'-LT-'curModIdx'-GT-'{}(
                            /* Inj: */ inj{SortInt{}, SortOptionalInt{}}(
                                VarCUR:SortInt{}
                            )
                        ),
                        Var'Unds'2:SortLabelDepthCell{},
                        Var'Unds'3:SortLabelIdsCell{}
                    ),
                    Var'Unds'17:SortModuleRegistryCell{},
                    Var'Unds'18:SortModuleIdsCell{},
                    Lbl'-LT-'moduleInstances'-GT-'{}(
                        /* builtin: */
                        Lbl'Unds'ModuleInstCellMap'Unds'{}(
                            /* element: */ LblModuleInstCellMapItem{}(
                                Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
                                Lbl'-LT-'moduleInst'-GT-'{}(
                                    Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
                                    Var'Unds'4:SortExportsCell{},
                                    Var'Unds'5:SortTypeIdsCell{},
                                    Var'Unds'6:SortTypesCell{},
                                    Var'Unds'7:SortNextTypeIdxCell{},
                                    Lbl'-LT-'funcIds'-GT-'{}(VarIDS:SortMap{}),
                                    Lbl'-LT-'funcAddrs'-GT-'{}(
                                        /* builtin: */
                                        Lbl'Unds'Map'Unds'{}(
                                            /* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
                                                /* Inj: */ inj{SortInt{}, SortKItem{}}(
                                                    Lbl'Hash'ContextLookup'LParUndsCommUndsRParUnds'WASM-DATA'Unds'Int'Unds'Map'Unds'Index{}(
                                                        VarIDS:SortMap{},
                                                        VarTFIDX:SortIndex{}
                                                    )
                                                ),
                                                /* Inj: */ inj{SortInt{}, SortKItem{}}(
                                                    VarFADDR:SortInt{}
                                                )
                                            ),
                                            /* opaque child: */ VarDotVar7:SortMap{}
                                        )
                                    ),
                                    Var'Unds'8:SortNextFuncIdxCell{},
                                    Var'Unds'9:SortTabIdsCell{},
                                    Var'Unds'10:SortTabAddrsCell{},
                                    Var'Unds'11:SortMemIdsCell{},
                                    Var'Unds'12:SortMemAddrsCell{},
                                    Var'Unds'13:SortGlobIdsCell{},
                                    Var'Unds'14:SortGlobalAddrsCell{},
                                    Var'Unds'15:SortNextGlobIdxCell{}
                                )
                            ),
                            /* opaque child: */ VarDotVar5:SortModuleInstCellMap{}
                        )
                    ),
                    Var'Unds'19:SortNextModuleIdxCell{},
                    Var'Unds'20:SortMainStoreCell{},
                    Var'Unds'21:SortDeterministicMemoryGrowthCell{},
                    Var'Unds'22:SortNextFreshIdCell{}
                ),
                Var'Unds'24:SortParamstackCell{}
            ),
            VarDotVar0:SortGeneratedCounterCell{}
        )
    ),
    \and{SortGeneratedTopCell{}}(
        \top{SortGeneratedTopCell{}}(),
        Lbl'-LT-'generatedTop'-GT-'{}(
            Lbl'-LT-'ewasm'-GT-'{}(
                Var'Unds'23:SortEeiCell{},
                Lbl'-LT-'wasm'-GT-'{}(
                    Lbl'-LT-'k'-GT-'{}(
                        kseq{}(
                            /* Inj: */ inj{SortInstr{}, SortKItem{}}(
                                Lbl'LPar'invoke'UndsRParUnds'WASM'Unds'Instr'Unds'Int{}(
                                    VarFADDR:SortInt{}
                                )
                            ),
                            VarDotVar3:SortK{}
                        )
                    ),
                    Var'Unds'16:SortValstackCell{},
                    Lbl'-LT-'curFrame'-GT-'{}(
                        Var'Unds'0:SortLocalsCell{},
                        Var'Unds'1:SortLocalIdsCell{},
                        Lbl'-LT-'curModIdx'-GT-'{}(
                            /* Inj: */ inj{SortInt{}, SortOptionalInt{}}(
                                VarCUR:SortInt{}
                            )
                        ),
                        Var'Unds'2:SortLabelDepthCell{},
                        Var'Unds'3:SortLabelIdsCell{}
                    ),
                    Var'Unds'17:SortModuleRegistryCell{},
                    Var'Unds'18:SortModuleIdsCell{},
                    Lbl'-LT-'moduleInstances'-GT-'{}(
                        /* builtin: */
                        Lbl'Unds'ModuleInstCellMap'Unds'{}(
                            /* element: */ LblModuleInstCellMapItem{}(
                                Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
                                Lbl'-LT-'moduleInst'-GT-'{}(
                                    Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
                                    Var'Unds'4:SortExportsCell{},
                                    Var'Unds'5:SortTypeIdsCell{},
                                    Var'Unds'6:SortTypesCell{},
                                    Var'Unds'7:SortNextTypeIdxCell{},
                                    Lbl'-LT-'funcIds'-GT-'{}(VarIDS:SortMap{}),
                                    Lbl'-LT-'funcAddrs'-GT-'{}(
                                        /* builtin: */
                                        Lbl'Unds'Map'Unds'{}(
                                            /* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
                                                /* Inj: */ inj{SortInt{}, SortKItem{}}(
                                                    Lbl'Hash'ContextLookup'LParUndsCommUndsRParUnds'WASM-DATA'Unds'Int'Unds'Map'Unds'Index{}(
                                                        VarIDS:SortMap{},
                                                        VarTFIDX:SortIndex{}
                                                    )
                                                ),
                                                /* Inj: */ inj{SortInt{}, SortKItem{}}(
                                                    VarFADDR:SortInt{}
                                                )
                                            ),
                                            /* opaque child: */ VarDotVar7:SortMap{}
                                        )
                                    ),
                                    Var'Unds'8:SortNextFuncIdxCell{},
                                    Var'Unds'9:SortTabIdsCell{},
                                    Var'Unds'10:SortTabAddrsCell{},
                                    Var'Unds'11:SortMemIdsCell{},
                                    Var'Unds'12:SortMemAddrsCell{},
                                    Var'Unds'13:SortGlobIdsCell{},
                                    Var'Unds'14:SortGlobalAddrsCell{},
                                    Var'Unds'15:SortNextGlobIdxCell{}
                                )
                            ),
                            /* opaque child: */ VarDotVar5:SortModuleInstCellMap{}
                        )
                    ),
                    Var'Unds'19:SortNextModuleIdxCell{},
                    Var'Unds'20:SortMainStoreCell{},
                    Var'Unds'21:SortDeterministicMemoryGrowthCell{},
                    Var'Unds'22:SortNextFreshIdCell{}
                ),
                Var'Unds'24:SortParamstackCell{}
            ),
            VarDotVar0:SortGeneratedCounterCell{}
        )
    )
)

[hjorthjort]

To reproduce

This was discovered on commit 96f3642e6e3917d38bf827aa5a8f80dc97030542 on the ewasm-semantics repository

From directory ewasm-semantics/verification/wrc20, the following command: make test KPROVE_OPTS="--haskell-backend-command 'kore-repl --repl-script repl-script'"

[ehildenb]

What does the associated K rule look like?

[hjorthjort]

What does the associated K rule look like?

    syntax PlainInstr ::= "call" Index
 // ----------------------------------
    rule <k> call TFIDX => ( invoke FADDR ) ... </k>
         <curModIdx> CUR </curModIdx>
         <moduleInst>
           <modIdx> CUR </modIdx>
           <funcIds> IDS </funcIds>
           <funcAddrs> ... #ContextLookup(IDS , TFIDX) |-> FADDR ... </funcAddrs>
           ...
         </moduleInst>

[ehildenb]

Hmmmm, I wonder if it's splitting on the #ContextLookup function evaluation, since that's the only function evaluation in that rule. Otherwise everything looks like normal Map lookups.

Though it's also a nested Map lookup, so maybe the haskell backend doesn't handle the nested case very well. What do the resulting states have different about them?

[hjorthjort]

That's probably what is going on. Although the lookups in question are using TFIDX that is definitely in IDS, either in the concrete base map, or in a Map:update somewhere. It kind of seems like the equality checks are failing, i.e., it can't decide equality for the TFIDX and any of the keys.

I'm wondering if it will help adding a smtlib for #ContextLookup.

Another thing that might be tripping up the backend is that the rules for #ContextLookup are in different modules, on in data.md and one in wasm-text.md.

[ehildenb]

Well, I think what's more likely is that the backend is not fully evaluating #ContextLookup before trying to do the lookup. You can check if it's the case by sequencing the rules some more and seeing if you get the same state splitting:

    rule <k> call TFIDX => #call #ContextLookup(IDS, TFIDX) ... </k>
         <curModIdx> CUR </curModIdx>
         <moduleInst>
           <modIdx> CUR </modIdx>
           <funcIds> IDS </funcIds>
           ...
         </moduleInst>

    rule <k> #call FID => ( invoke FADDR ) ... </k>
         <curModIdx> CUR </curModIdx>
         <moduleInst>
           <modIdx> CUR </modIdx>
           <funcIds> IDS </funcIds>
           <funcAddrs> ... FID |-> FADDR ... </funcAddrs>
           ...
         </moduleInst>

[ehildenb]

A more general solution to this would be to find a way to eliminate #ContextLookup altogether (assuming the above attempt works).

[hjorthjort]

I'll try that.

Yes, ideally #ContextLookup would be part of a pre-processing, converting from the text format to the basic format.