An example that runs on llvm backend but does not on the Haskell backend.

[ChristianoBraga]

Guys, I know you are all overloaded with work, over 200 issues! But please take a look at the situation below.

The following K description runs just fine in the llvm backend but either loops or takes quite a while to finish in the Haskell backend.
This example is a simplification of Plutus semantics in K that arose while running the ML Proof Checker. Could you shed some light?

require "domains.md"
module TEST
 imports LIST
 imports K-EQUAL
 imports INT
 imports STRING

 syntax String ::= head(String) [function]
 rule head(S) => substrString(S, 0, 1)
 syntax String ::= tail(String) [function]
 rule tail(S) => substrString(S, 1, lengthString(S))

 syntax List ::= f(String, List) [function]
 rule f(S, L) =>
      #if S ==String ""
      #then (L)
      #else f(tail(S), (L ListItem(head(S))))
      #fi
endmodule

In LLVM:

$ kompile --backend llvm t.k --main-module TEST
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.
$ time krun -cPGM="f(\"ola\", .List)" --depth 0
<k>
  ListItem ( "o" )
  ListItem ( "l" )
  ListItem ( "a" ) ~> .
</k>

real    0m0.990s
user    0m2.462s
sys     0m0.133s

In Haskell:

$ kompile --backend haskell t.k --main-module TEST
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.

$ time krun -cPGM="f(\"ola\", .List)" --depth 0
^Ckore-exec: [12129483] Error (ErrorException):
    Error while communicating with the solver:
        fd:137: hFlush: resource vanished (Broken pipe)
    Solver exit code: -2
Created bug report: kore-exec.tar.gz
[Error] Critical: Backend crashed during rewriting with exit code 1

real    0m13.209s
user    0m16.102s
sys     0m0.606s

[dwightguth]

I believe the issue is that #if is not short circuiting, so it is always evaluating the recursive call even if the string is empty. This is not really a simple fix at all, even though it is unintuitive. I would recommend rewriting that rule as two rules with a side condition rather than a single rule with #if.

This is probably not going to get fixed anytime soon.

[ChristianoBraga]

Thank you

…

On Thu, Mar 10, 2022 at 2:20 PM Dwight Guth ***@***.***> wrote: I believe the issue is that #if is not short circuiting, so it is always evaluating the recursive call even if the string is empty. This is not really a simple fix at all, even though it is unintuitive. I would recommend rewriting that rule as two rules with a side condition rather than a single rule with #if. This is probably not going to get fixed anytime soon. — Reply to this email directly, view it on GitHub <#2995 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFNNCEKLTYBZTVD2JX7HFVLU7IVNPANCNFSM5QNHZIZQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[ChristianoBraga]

@ehildenb suggested I should leave this issue open. It is not blocking me because I changed #ift for rules. (My original intention was to get rid of conditional rules.)

[ana-pantilie]

Not clear if there's a sound way to solve this.

@xc93 Do you have any idea on how to do definedness checking on this? How do we encode short circuiting operations?

[virgil-serbanuta]

Would this work and be good enough (I may have misplaced some parenthesis)?

rule f(S, L) => (((S ==String "") #Equals true) #And (L)) #Or (#Not ((S ==String "") #Equals true) #And f(tail(S), (L ListItem(head(S)))))

This could be made to be more friendly by introducing a new ML operator/macro #IF which would be defined by #IF(C, TB, FB) === (C #And TB) #Or ((#Not C) #And FB) and which would be evaluated without expansion, in the expected way, by the Haskell backend.

[ehildenb]

Inductively/co-inductively discharge definedness check?

As I understand the problem, we have the rule:

rule f(S, L) => #if ... #then ... #else f(S', L') #fi

Then, it's trying to check #Ceil(#if .... #then ... #else f(S', L') #fi) in the case where the boolean condition is false (which it should have to do for soundness, even if evaluation is short-circuiting).

But in checking this #Ceil(...) conditino, it must also check #Ceil(f(S', L')), which in needs to evaluate f(S', L') a bit to do so, which leads to applying the rule again, which leads to yet another definedness check of f(S'', L'').

Is there a way we can coinductively or inductively discharge this definedness check? So once we go to check #Ceil(f(S', L')), we say "this is an instance of what we're already trying to prove, which is #Ceil(f(S, L)), and so we don't need to continue unfolding the #Ceil or the f here". @xc93 is this sound? If so, can you write a proof of it? This would allow us to use short-circuiting operators in Haskell backend in a safe manner.

[xc93]

I don't know what's the logical encoding of #if, but the #IF notation that @virgil-serbanuta suggested above looks very reasonable and supports short circuiting.

#IF(C, TB, FB) === (C #And TB) #Or ((#Not C) #And FB)

Here, C should be a predicate pattern (and not a Boolean value), that is, C is either #TOP or #BOTTOM. If we like to use a Boolean condition (true or false), we can define #BIF as follows:

#BIF(B, TB, FB) = #IF(#EQUALS(B, true), TB, FB)

Here, B should be something that always evaluates to a Boolean value, either true or false.

To check the definedness of #IF or #BIF patterns when C = #TOP or B = true, we only need to check the definedness of TB. It's logically sound. In fact, the following are logically valid statements:

#IMPLIES(#EQUALS(C, #TOP), #EQUALS(#IF(C, TB, FB), TB))
#IMPLIES(#EQUALS(B, true), #EQUALS(#BIF(B, TB, FB), TB))
#IMPLIES(#EQUALS(C, #BOTTOM), #EQUALS(#IF(C, TB, FB), FB))
#IMPLIES(#EQUALS(B, false), #EQUALS(#BIF(B, TB, FB), FB))

where C is a predicate and B is a Boolean value.

[dwightguth]

If you have an encoding that works for the haskell backend and provides the same results on all concrete inputs as the llvm backend, I would recommend simply writing a compilation pass in the k frontend that transforms #if into that encoding and running it on the haskell backend only.

[ehildenb]

@xc93 with this encoding, is it still true that #if ... is a function symbol or not?

If it's not the case, then maybe we cannot using the existing equational simplification engine of the Haskell backend for simplifying rules with #if ... at the top.

[dwightguth]

It is not, under this encoding, because it's not a symbol. It's an alias for an \or.

[xc93]

#IF is not a function symbol. In fact, it is not a symbol at all, but a notation. The reason is that even if the first argument is #BOTTOM, the result is not necessarily #BOTTOM. It is FB.
#BIF, however, does have a function symbol semantics. Instead of defining #BIF as a notation using #IF, I can instead define it directly as a function symbol with two axioms as follows:

symbol BIF(Bool, K, K) : K [function]
axiom BIF(true, k1, k2) = k1
axiom BIF(false, k2, k2) = k2

The two axioms guarantee that for all b, k1, k2, BIF(b, k1, k2) is a singleton pattern, matched by precisely one element (either k1 or k2, depending on b). That is, BIF is a function from Bool \times K \times K to K.

[dwightguth]

For what it's worth, it was never treated as a regular function symbol by the llvm backend, any more than the other short circuiting boolean operators were. They were all compiled down to native branch instructions. So I don't see why we can't treat them specially in the haskell backend also.

[dwightguth]

@xc93 that doesn't sound correct; again, if k1 is bottom but b is false, the result is k2. This is not true if if is a symbol.