User-defined Set simplification rule not applied

[ehildenb]

On K master commit (72d33ae0e0), the following very simple spec does not work. This affects some KEVM proofs which are being ported.

requires "domains.md"

module TEST
    imports INT
    imports SET

    configuration <k> $PGM:Step </k>

    syntax Step ::= run ( Set ) | done ( Set )

    rule <k> run(S) => done(S) ... </k>

    syntax Bool ::= pred ( Int ) [function, no-evaluators]

    rule .Set -Set _ => .Set [simplification]
    rule (SetItem(X) REST) -Set SetItem(Y) => SetItem(X) (REST -Set SetItem(Y)) requires pred(X) andBool notBool pred(Y) [simplification]

    rule pred(X) => false requires 1 <=Int X andBool X <=Int 9 [simplification]
endmodule

module TEST-SPEC
    imports TEST

    claim <k> run(SetItem(1) -Set SetItem(X)) => done(SetItem(1)) ... </k> requires pred(X)

endmodule

To reproduce the failure:

kompile --backend haskell test.k --main-module TEST --syntax-module TEST
kprove test.k --def-module TEST --spec-module TEST-SPEC

[geo2a]

I modified introduced names for all rules in the example:

requires "domains.md"

module TEST
    imports INT
    imports SET

    configuration <k> $PGM:Step </k>

    syntax Step ::= run ( Set ) | done ( Set )

    rule [step]: <k> run(S) => done(S) ... </k>

    syntax Bool ::= pred ( Int ) [function, no-evaluators]

    rule [set.diff.empty]: .Set -Set _ => .Set [simplification]
    rule [set.diff.concat]: (SetItem(X) REST) -Set SetItem(Y) => SetItem(X) (REST -Set SetItem(Y)) requires pred(X) andBool notBool pred(Y) [simplification]

    rule [pred.false]: pred(X) => false requires 1 <=Int X andBool X <=Int 9 [simplification]
endmodule

module TEST-SPEC
    imports TEST

    claim <k> run(SetItem(1) -Set SetItem(X)) => done(SetItem(1)) ... </k> requires pred(X)

endmodule

To see which equations are applied by kore-exec, I set the KORE_EXEC_OPTS environmental variable:

export KORE_EXEC_OPTS="--log ${LOG_FILE} --debug-equation TEST.step --debug-equation TEST.set.diff.empty --debug-equation TEST.set.diff.concat --debug-equation TEST.pred.false

After running kprove, the first entry in the log file reports an attempt to apply rule pred.false (line 18):

    (DebugAttemptEquation) while applying equation at /home/geo2a/Workspace/RV/kore/georgy/test.k:18:24-18:77:
    equation is not applicable:
    could not infer the equation requirement:
        /* Spa */
        \equals{SortBool{}, _PREDICATE{}}(
            /* Fl Fn D Spa */
            Lbl'Unds'andBool'Unds'{}(
                /* Fl Fn D Spa */
                Lbl'Unds-LT-Eqls'Int'Unds'{}(
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1"),
                    /* Fl Fn D Sfa */ RuleVarX:SortInt{}
                ),
                /* Fl Fn D Spa */
                Lbl'Unds-LT-Eqls'Int'Unds'{}(
                    /* Fl Fn D Sfa */ RuleVarX:SortInt{},
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("9")
                )
            ),
            /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true")
        )
    and the matching requirement:
        /* D Sfa */ \top{_PREDICATE{}}()
    from the side condition:
        Assumed true condition:
            /* D Sfa */ \top{_PREDICATE{}}()
        Term replacements:
        Assumed to be defined:

I looks like the kore-exec is saying that it can't infer the requirement 1 <=Int X andBool X <=Int 9 from #Top? I tried both kore-exec-v0.48 and kore-exec-v0.47 --- both return the same result.

Interestingly, kore-exec only logs attempts of applying this equation, i.e. there is no log entries for the other ones I asked to debug. I tried giving only one --debug-equation option, but it did not help.

[geo2a]

This problem is most likely related to simplification rules that operate over sort Set. Here is a working example that is similar in structure, but does not use Set:

requires "domains.md"

module TEST
    imports INT

    configuration <k> $PGM:Step </k>

    syntax Step ::= run ( Int ) | done ( Int )
    rule [step]: <k> run(S) => done(S) ... </k>

    syntax Bool ::= pred ( Int ) [function, no-evaluators]
    syntax Int ::= f (Int, Int) [function, no-evaluators]

    rule [pred.false]: pred(X) => false requires 1 <=Int X andBool X <=Int 9 [simplification]
    rule [f.rule]: f(X, Y) => 4 requires pred(X) andBool notBool pred(Y) [simplification]
endmodule

module TEST-SPEC
    imports TEST

    claim <k> run(f(X, 7)) => done(4) ... </k> requires pred(X)
endmodule

[ana-pantilie]

@ehildenb Do you know when this issue started appearing? I think I know what's going on, but I'm confused about why this is recent (or maybe it isn't?).

[ehildenb]

It never worked as far as I know.

[ana-pantilie]

Experiment: remove https://github.com/kframework/kore/blob/25c91ec03dcac3e8ded17cdad505f2e2554038c5/kore/src/Kore/Builtin/Set.hs#L369 and give this test another try.

[ana-pantilie]

I forgot to add during our debugging meeting, @geo2a , but I think this issue actually describes two separate issues:

1. Find a way to make user-defined Set simplification rules get attempted, here we should focus on removing the symbolic case from the backend and see what support we need from the frontend
2. Figure out why the concat rule doesn't apply when it's marked [simplification]; you noticed that it has something to do with matching, and we need to debug it further