[Optimism/KEVM] ByteArray concat simplification breaks back-end

[PetarMax]

In the context of the Optimism engagement, the following simplification

rule 
  { BA1:ByteArray #Equals BA2:ByteArray } =>
    { concatHead(BA1):ByteArray #Equals concatHead(BA2):ByteArray } #And 
    { concatTail(BA1):ByteArray #Equals concatTail(BA2):ByteArray }
  requires 
    #sizeByteArray(concatHead(BA1)) =/=K #sizeByteArray(BA1) 
    orBool #sizeByteArray(concatHead(BA2)) =/=K #sizeByteArray(BA2)
  [simplification]

breaks the backend with the message

    kore-exec: [5500634] Error (ErrorException):
    Could not make sort
        SortBool{}
    match sort
        SortBytes{}
    This is a program bug!

The two functions that it uses, concatHead and concatTail, operate on KEVM ByteArrays and are defined as follows:

                         // Leftmost operand in a concat
    syntax ByteArray ::= concatHead(ByteArray) [function, total]
                         // Rest of concat
                       | concatTail(ByteArray) [function, total]

    rule concatHead(BA1 ++ _) => concatHead(BA1) [simplification(40)]
    rule concatHead(BA)       => BA              [simplification    ]

    rule concatTail(BA1 ++ BA2) => concatTail(BA1) ++ BA2 [simplification(40)]
    rule concatTail(_)          => .ByteArray             [simplification    ]

The problem should be reproducible by checking out the foundry-tests-calldata-petar branch of the Optimism audit repo, uncommenting the above simplification in the lemma file and then executing:

cd optimism_foundry
forge b
./run-prove-lemmas.sh

[ana-pantilie]

@PetarMax please also generate a bug report and attach here.

[PetarMax]

Yes, here it is. kore-exec.tar.gz

[ana-pantilie]

Issue is inside matcher, it is constructing a false substitution instead of failing. It should sort-check when adding a substitution.

Relevant tracing (when matching the LHS of the simplification rule with the following term, we get VarBA2 := true which is obviously false):

Start
Left: /* Spa */
\equals{SortBytes{}, Q0}(
    /* Fl Fn D Sfa */ EquationVarBA1:SortBytes{},
    /* Fl Fn D Sfa */ EquationVarBA2:SortBytes{}
)
Actual term:
/* Spa */
\equals{SortBool{}, SortBool{}}(
    /* Fl Fn D Sfa */
    Lbl'Unds-LT-'Int'Unds'{}(
        /* Fl Fn D Sfa */
        Lbl'UndsStar'Int'Unds'{}(
            /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("32"),
            /* Fl Fn D Sfa */ RuleVarITER'Unds'COUNT'Unds'S:SortInt{}
        ),
        /* Fl Fn D Sfa */
        Lbl'UndsPlus'Int'Unds'{}(
            /* Fl Fn D Sfa */
            Lbl'Hash'sizeByteArray'LParUndsRParUnds'EVM-TYPES'Unds'Int'Unds'ByteArray{}(
                /* Fl Fn D Sfa */
                RuleVarVV6'UndsUnds'data'Unds'3c5818c8:SortBytes{}
            ),
            /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("9")
        )
    ),
    /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true")
)

Pred:
/* D Sfa */ \top{_}()
Subst:

    Variable: SomeVariableNameElement (ElementVariableName {unElementVariableName = EquationVariableName (VariableName {base = InternedId {getInternedId = "VarBA", internedIdLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 23467, column = 32})}, counter = Just (Element 1)})})
    Term: /* Fl Fn D Sfa */
Lbl'Unds-LT-'Int'Unds'{}(
    /* Fl Fn D Sfa */
    Lbl'UndsStar'Int'Unds'{}(
        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("32"),
        /* Fl Fn D Sfa */ RuleVarITER'Unds'COUNT'Unds'S:SortInt{}
    ),
    /* Fl Fn D Sfa */
    Lbl'UndsPlus'Int'Unds'{}(
        /* Fl Fn D Sfa */
        Lbl'Hash'sizeByteArray'LParUndsRParUnds'EVM-TYPES'Unds'Int'Unds'ByteArray{}(
            /* Fl Fn D Sfa */ RuleVarVV6'UndsUnds'data'Unds'3c5818c8:SortBytes{}
        ),
        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("9")
    )
)
----------------

    Variable: SomeVariableNameElement (ElementVariableName {unElementVariableName = EquationVariableName (VariableName {base = InternedId {getInternedId = "VarBA", internedIdLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 23467, column = 51})}, counter = Just (Element 2)})})
    Term: /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true")
----------------

Equation:
Just (SourceLocation {location = Location {start = Just (LineColumn {line = 202, column = 10}), end = Just (LineColumn {line = 206, column = 75})}, source = Source {unSource = Just "/Users/petarmax/Projects/RV/_audits_Ethereum-optimism_optimism/optimism_foundry/optimism-lemmas.k"}})