Internal error - expected simplified results

[virgil-serbanuta]

To reproduce:

kore-repl \
    --smt-timeout 4000 \
    --solver-transcript transcript.z3 \
    --repl-script kast.kscript \
    --bug-report internal-error \
    vdefinition.kore \
    --module FUNCTIONS-EXECUTE \
    --prove spec.kore \
    --spec-module PROOF-PROPOSE-ACTION-BOARDMEMBER \
    --output result.kore

then

stepf 50
step 100

kore.zip internal-error.tar.gz

Backend version:

$ kore-repl --version
Kore version 0.42.0.0
Git:
  revision: ec02c41d2ff5b970729cd980269a11b686e1e614 (dirty)
  branch:   master
  last commit:  Mon Mar 29 14:47:31 2021 -0500

[andreiburdusa]

I reshaped this case of returnIfResultSimplifiedOrContinue like this so I could use trace on intermediate results:

            | isTop resultTerm
              , Right condition <- termAsPredicate
              , resultPredicate == condition = do
                let orPattern =
                        OrPattern.fromPattern $
                            Pattern.fromCondition_ cond
                    cond =
                        Condition.markPredicateSimplifiedConditional
                            sideConditionRepresentation
                            resultPredicate
                unless (OrPattern.hasSimplifiedChildrenIgnoreConditions orPattern) $ do
                    traceM "\n-----------------------------------\n"
                    traceM . show . pretty $ predicate cond
                    traceM "\n"
                    traceM "\n-----------------------------------\n"
                return orPattern

The result looks like this:

-----------------------------------

/* Sfu */
\and{_PREDICATE{}}(
    /* Sfc */
    \ceil{SortUsize{}, _PREDICATE{}}(
        /* Fn Sfc */
        Lblproject'Coln'Usize{}(
            /* Fn Sfc */
            kseq{}(
                /* Fn Sfc */
                LblMap'Coln'lookup{}(
                    /* Fl Fn D Sfa */ ConfigVarAddressToUserId:SortMap{},
                    /* Fl Fn D Sfc */
                    /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                        /* Fl Fn D Sfa */
                        Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                            /* Fl Fn D Sfa */ ConfigVarCallerAddress0:SortInt{}
                        )
                    )
                ),
                /* Fl Fn D Sfa Cl */ dotk{}()
            )
        )
    ),
    /* Spu */
    \and{_PREDICATE{}}(
        /* Sfc */
        \equals{SortBool{}, _PREDICATE{}}(
            /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
            /* Fl Fn D Sfc */
            Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                /* Fl Fn D Sfc */
                /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                    /* Fl Fn D Sfa */
                    Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                        /* Fl Fn D Sfa */ ConfigVarCallerAddress0:SortInt{}
                    )
                ),
                /* Fl Fn D Sfa */ ConfigVar'QuesUnds'Remainder:SortMap{}
            )
        ),
        /* Spu */
        \and{_PREDICATE{}}(
            /* Sfc */
            \equals{SortBool{}, _PREDICATE{}}(
                /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
                /* Fl Fn D Sfc */
                Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                    /* Fl Fn D Sfc */
                    /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                        /* Fl Fn D Sfa */
                        Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
                            /* Fl Fn D Sfa */
                            Lbl'UndsPlus'Int'Unds'{}(
                                /* Fl Fn D Sfa */
                                ConfigVarActionLastIndex:SortInt{},
                                /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                            )
                        )
                    ),
                    /* Fl Fn D Sfa */ ConfigVarActionData:SortMap{}
                )
            ),
            /* Spu */
            \and{_PREDICATE{}}(
                /* Sfc */
                \equals{SortBool{}, _PREDICATE{}}(
                    /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
                    /* Fl Fn D Sfc */
                    Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                        /* Fl Fn D Sfc */
                        /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                            /* Fl Fn D Sfa */
                            Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
                                /* Fl Fn D Sfa */
                                Lbl'UndsPlus'Int'Unds'{}(
                                    /* Fl Fn D Sfa */
                                    ConfigVarActionLastIndex:SortInt{},
                                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                                )
                            )
                        ),
                        /* Fl Fn D Sfa */ ConfigVarActionSigners:SortMap{}
                    )
                ),
                /* Spu */
                \and{_PREDICATE{}}(
                    /* Sfc */
                    \equals{SortBool{}, _PREDICATE{}}(
                        /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
                        /* Fl Fn D Sfc */
                        Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                            /* Fl Fn D Sfc */
                            /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                                /* Fl Fn D Sfa */ ConfigVarU:SortUsize{}
                            ),
                            /* Fl Fn D Sfa */
                            ConfigVar'QuesUnds'Remainder0:SortMap{}
                        )
                    ),
                    /* Spu */
                    \and{_PREDICATE{}}(
                        /* Sfc */
                        \equals{SortBool{}, _PREDICATE{}}(
                            /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"),
                            /* Fl Fn D Sfc */
                            Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                                /* Fl Fn D Sfc */
                                /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                                    /* Fl Fn D Sfa */
                                    Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarCallerAddress0:SortInt{}
                                    )
                                ),
                                /* Fl Fn D Sfa */
                                ConfigVarAddressToUserId:SortMap{}
                            )
                        ),
                        /* Spu */
                        \and{_PREDICATE{}}(
                            /* Sfc */
                            \equals{SortMap{}, _PREDICATE{}}(
                                /* Fl Fn D Sfa */ ConfigVarActionData:SortMap{},
                                /* Fn Sfc */
                                /* InternalMap: */ Lbl'Unds'Map'Unds'{}(
                                    /* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
                                        /* Fl Fn D Sfc */
                                        /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                                            /* Fl Fn D Sfa */
                                            Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
                                                /* Fl Fn D Sfa */
                                                Lbl'UndsPlus'Int'Unds'{}(
                                                    /* Fl Fn D Sfa */
                                                    ConfigVarActionLastIndex:SortInt{},
                                                    /* Fl Fn D Sfa Cl */
                                                    \dv{SortInt{}}("1")
                                                )
                                            )
                                        ),
                                        /* Fl Fn D Sfa */
                                        ConfigVarAction:SortKItem{}
                                    ),
                                    /* opaque child: */ /* Fl Fn D Sfa */
                                    ConfigVarActionData:SortMap{}
                                )
                            ),
                            /* Spc */
                            \and{_PREDICATE{}}(
                                /* Sfa */
                                \equals{SortInt{}, _PREDICATE{}}(
                                    /* Fl Fn D Sfa */
                                    ConfigVarActionLastIndex:SortInt{},
                                    /* Fl Fn D Sfa */
                                    Lbl'UndsPlus'Int'Unds'{}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarActionLastIndex:SortInt{},
                                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                                    )
                                ),
                                /* Spc */
                                \and{_PREDICATE{}}(
                                    /* Spc */
                                    \equals{SortMap{}, _PREDICATE{}}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarAddressToUserId:SortMap{},
                                        /* Fn Sfc */
                                        /* InternalMap: */ Lbl'Unds'Map'Unds'{}(
                                            /* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
                                                /* Fl Fn D Sfc */
                                                /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                                                    /* Fl Fn D Sfa */
                                                    Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                                                        /* Fl Fn D Sfa */
                                                        ConfigVarCallerAddress0:SortInt{}
                                                    )
                                                ),
                                                /* Fl Fn D Sfc */
                                                /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                                                    /* Fl Fn D Sfa */
                                                    ConfigVarU:SortUsize{}
                                                )
                                            ),
                                            /* opaque child: */ /* Fl Fn D Sfa */
                                            ConfigVar'QuesUnds'Remainder:SortMap{}
                                        )
                                    ),
                                    /* Spc */
                                    \equals{SortUsize{}, _PREDICATE{}}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarU:SortUsize{},
                                        /* Fn Sfc */
                                        Lblproject'Coln'Usize{}(
                                            /* Fn Sfc */
                                            kseq{}(
                                                /* Fn Sfc */
                                                LblMap'Coln'lookup{}(
                                                    /* Fl Fn D Sfa */
                                                    ConfigVarAddressToUserId:SortMap{},
                                                    /* Fl Fn D Sfc */
                                                    /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                                                        /* Fl Fn D Sfa */
                                                        Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                                                            /* Fl Fn D Sfa */
                                                            ConfigVarCallerAddress0:SortInt{}
                                                        )
                                                    )
                                                ),
                                                /* Fl Fn D Sfa Cl */ dotk{}()
                                            )
                                        )
                                    )
                                )
                            )
                        )
                    )
                )
            )
        )
    )
)

-----------------------------------

Note that it's marked as fully simplified on top although it contains partially simplified children

[ttuegel]

Note that it's marked as fully simplified on top although it contains partially simplified children

I don't think this is important.

The unsimplified conditions are mostly substitution-like. I think the problem is that we ended up here without ever calling the condition simplifier.

[andreiburdusa]

The predicate given to TermLike.simplify:

/* Spu */
\and{_PREDICATE{}}(
    /* Sfc */
    \ceil{SortUsize{}, _PREDICATE{}}(
        /* Fn Sfc */
        Lblproject'Coln'Usize{}(
            /* Fn Sfc */
            kseq{}(
                /* Fn Sfc */
                LblMap'Coln'lookup{}(
                    /* Fl Fn D Sfa */ ConfigVarAddressToUserId:SortMap{},
                    /* Fl Fn D Sfc */
                    /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                        /* Fl Fn D Sfa */
                        Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                            /* Fl Fn D Sfa */ ConfigVarCallerAddress0:SortInt{}
                        )
                    )
                ),
                /* Fl Fn D Sfa Cl */ dotk{}()
            )
        )
    ),
    /* Spu */
    \and{_PREDICATE{}}(
        /* Sfc */
        \equals{SortBool{}, _PREDICATE{}}(
            /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
            /* Fl Fn D Sfc */
            Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                /* Fl Fn D Sfc */
                /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                    /* Fl Fn D Sfa */
                    Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                        /* Fl Fn D Sfa */ ConfigVarCallerAddress0:SortInt{}
                    )
                ),
                /* Fl Fn D Sfa */ ConfigVar'QuesUnds'Remainder:SortMap{}
            )
        ),
        /* Spu */
        \and{_PREDICATE{}}(
            /* Sfc */
            \equals{SortBool{}, _PREDICATE{}}(
                /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
                /* Fl Fn D Sfc */
                Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                    /* Fl Fn D Sfc */
                    /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                        /* Fl Fn D Sfa */
                        Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
                            /* Fl Fn D Sfa */
                            Lbl'UndsPlus'Int'Unds'{}(
                                /* Fl Fn D Sfa */
                                ConfigVarActionLastIndex:SortInt{},
                                /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                            )
                        )
                    ),
                    /* Fl Fn D Sfa */ ConfigVarActionData:SortMap{}
                )
            ),
            /* Spu */
            \and{_PREDICATE{}}(
                /* Sfc */
                \equals{SortBool{}, _PREDICATE{}}(
                    /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
                    /* Fl Fn D Sfc */
                    Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                        /* Fl Fn D Sfc */
                        /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                            /* Fl Fn D Sfa */
                            Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
                                /* Fl Fn D Sfa */
                                Lbl'UndsPlus'Int'Unds'{}(
                                    /* Fl Fn D Sfa */
                                    ConfigVarActionLastIndex:SortInt{},
                                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                                )
                            )
                        ),
                        /* Fl Fn D Sfa */ ConfigVarActionSigners:SortMap{}
                    )
                ),
                /* Spu */
                \and{_PREDICATE{}}(
                    /* Sfc */
                    \equals{SortBool{}, _PREDICATE{}}(
                        /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
                        /* Fl Fn D Sfc */
                        Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                            /* Fl Fn D Sfc */
                            /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                                /* Fl Fn D Sfa */ ConfigVarU:SortUsize{}
                            ),
                            /* Fl Fn D Sfa */
                            ConfigVar'QuesUnds'Remainder0:SortMap{}
                        )
                    ),
                    /* Spu */
                    \and{_PREDICATE{}}(
                        /* Sfc */
                        \equals{SortBool{}, _PREDICATE{}}(
                            /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"),
                            /* Fl Fn D Sfc */
                            Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
                                /* Fl Fn D Sfc */
                                /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                                    /* Fl Fn D Sfa */
                                    Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarCallerAddress0:SortInt{}
                                    )
                                ),
                                /* Fl Fn D Sfa */
                                ConfigVarAddressToUserId:SortMap{}
                            )
                        ),
                        /* Spu */
                        \and{_PREDICATE{}}(
                            /* Sfc */
                            \equals{SortMap{}, _PREDICATE{}}(
                                /* Fl Fn D Sfa */ ConfigVarActionData:SortMap{},
                                /* Fn Sfc */
                                /* InternalMap: */ Lbl'Unds'Map'Unds'{}(
                                    /* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
                                        /* Fl Fn D Sfc */
                                        /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                                            /* Fl Fn D Sfa */
                                            Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
                                                /* Fl Fn D Sfa */
                                                Lbl'UndsPlus'Int'Unds'{}(
                                                    /* Fl Fn D Sfa */
                                                    ConfigVarActionLastIndex:SortInt{},
                                                    /* Fl Fn D Sfa Cl */
                                                    \dv{SortInt{}}("1")
                                                )
                                            )
                                        ),
                                        /* Fl Fn D Sfa */
                                        ConfigVarAction:SortKItem{}
                                    ),
                                    /* opaque child: */ /* Fl Fn D Sfa */
                                    ConfigVarActionData:SortMap{}
                                )
                            ),
                            /* Spc */
                            \and{_PREDICATE{}}(
                                /* Sfa */
                                \equals{SortInt{}, _PREDICATE{}}(
                                    /* Fl Fn D Sfa */
                                    ConfigVarActionLastIndex:SortInt{},
                                    /* Fl Fn D Sfa */
                                    Lbl'UndsPlus'Int'Unds'{}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarActionLastIndex:SortInt{},
                                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                                    )
                                ),
                                /* Spc */
                                \and{_PREDICATE{}}(
                                    /* Spc */
                                    \equals{SortMap{}, _PREDICATE{}}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarAddressToUserId:SortMap{},
                                        /* Fn Sfc */
                                        /* InternalMap: */ Lbl'Unds'Map'Unds'{}(
                                            /* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
                                                /* Fl Fn D Sfc */
                                                /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                                                    /* Fl Fn D Sfa */
                                                    Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                                                        /* Fl Fn D Sfa */
                                                        ConfigVarCallerAddress0:SortInt{}
                                                    )
                                                ),
                                                /* Fl Fn D Sfc */
                                                /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                                                    /* Fl Fn D Sfa */
                                                    ConfigVarU:SortUsize{}
                                                )
                                            ),
                                            /* opaque child: */ /* Fl Fn D Sfa */
                                            ConfigVar'QuesUnds'Remainder:SortMap{}
                                        )
                                    ),
                                    /* Spc */
                                    \equals{SortUsize{}, _PREDICATE{}}(
                                        /* Fl Fn D Sfa */
                                        ConfigVarU:SortUsize{},
                                        /* Fn Sfc */
                                        Lblproject'Coln'Usize{}(
                                            /* Fn Sfc */
                                            kseq{}(
                                                /* Fn Sfc */
                                                LblMap'Coln'lookup{}(
                                                    /* Fl Fn D Sfa */
                                                    ConfigVarAddressToUserId:SortMap{},
                                                    /* Fl Fn D Sfc */
                                                    /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                                                        /* Fl Fn D Sfa */
                                                        Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                                                            /* Fl Fn D Sfa */
                                                            ConfigVarCallerAddress0:SortInt{}
                                                        )
                                                    )
                                                ),
                                                /* Fl Fn D Sfa Cl */ dotk{}()
                                            )
                                        )
                                    )
                                )
                            )
                        )
                    )
                )
            )
        )
    )
)

The predicate not completely simplified that causes the error:

\equals{SortMap{}, _PREDICATE{}}(
    /* Fl Fn D Sfa */ ConfigVarAddressToUserId:SortMap{},
    /* Fn Sfc */
    /* InternalMap: */ Lbl'Unds'Map'Unds'{}(
        /* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
            /* Fl Fn D Sfc */
            /* Inj: */ inj{SortAddress{}, SortKItem{}}(
                /* Fl Fn D Sfa */
                Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
                    /* Fl Fn D Sfa */ ConfigVarCallerAddress0:SortInt{}
                )
            ),
            /* Fl Fn D Sfc */
            /* Inj: */ inj{SortUsize{}, SortKItem{}}(
                /* Fl Fn D Sfa */ ConfigVarU:SortUsize{}
            )
        ),
        /* opaque child: */ /* Fl Fn D Sfa */
        ConfigVar'QuesUnds'Remainder:SortMap{}
    )
)

[ttuegel]

This would be fixed by #2400.