Strange behavior of proof mode

[kheradmand]

I am using k-legacy the latest commit. I have the following definition and spec:

module TEST
    syntax Val ::= "@undef" 
    syntax Val ::= NUVal
    syntax NUVal ::=  "@val" "("Int","Int","Bool")"

    configuration
    <T>
        <k> $PGM:Val </k>
    </T>

    rule @val(I:Int,_,_) => I
endmodule

module SPEC
  imports TEST

 rule <k> V:NUVal => I:Int </k>

endmodule

The proof does no go through. However, if I change the rule from rule @val(I:Int,_,_) => I to rule <k> @val(I:Int,_,_) => I </k> It goes through. In both case, if I give for example @val(1,2,false) as the input to krun it correctly gives me 1 as the output. I am wondering whether it is a bug or a feature?

[ehildenb]

This seems related to the example I gave @andreistefanescu of --search not giving all the results I expected. I guess the problem is that associative unification is not supported, specifically the associative operator here is _~>_, and the original rule:

    rule @val(I,_,_) => I

is translated to:

    rule <k> @val(I,_,_) => I ~> _ </k>

So it's trying to unify V:NUVal and @val(I,_,_) ~> _, and failing because the unification engine doesn't try to infer that _ unifies with .KList.

@andreistefanescu can you confirm that it's the same issue I had?

[ehildenb]

Here is the example I had:

module TEST-SYNTAX
    imports DOMAINS
    syntax Foo ::= "foo" | "bar"
                 | "foo1" | "foo2"
                 | "bar1" | "bar2"
                 | "fooSplit"
                 | "symbolicFoo" [function]
    rule symbolicFoo => ?F:Foo [symbolicFoo]
endmodule
module TEST
    imports TEST-SYNTAX
    configuration <k> $PGM:Foo </k>
    rule foo => foo1 [symbFoo1]
    rule bar => bar1 [symbFoo2]
    // or equivalently
    // rule F:Foo => foo1 requires F ==K foo [symbFoo1]
    // rule F:Foo => bar1 requires F ==K bar [symbFoo2]
    rule fooSplit => foo2 [fooSplit1]
    rule fooSplit => bar2 [fooSplit2]
endmodule

And similarly, if I did krun --search on the program symbolicFoo, it would get stuck instead of giving four solutions. However, if I wrap the rules in <k> tags, eg:

    rule <k> foo => foo1 </k> [symbFoo1]
    rule <k> bar => bar1 </k> [symbFoo2]

it works.

[andreistefanescu]

It's the same bug as @ehildenb reported. I should fix it :-)