[KIP] - Partial SMT hook syntax

[Baltoli]

Motivation

This issue summarises a threaded conversation on Slack; the original messages can be found here.

Currently, our syntax for SMT hook encodings is fully constructive; in smtlib as used by Z3, this means that partial functions cannot be specified as SMT hooks. Only total functions can be used as hooks.

Our original motivation for this change is in the issues related to the semantics of integer exponentiation around #2225. When developing that PR, we identified the need for a partial SMT encoding of integer exponentiation when both the base and exponent are positive integers:

(ite (and (< 0 #1) (< 0 #2)) (to_int (^ #1 #2)) ???)

Because the hook must be defined constructively, there is no valid term to fill the ??? hole. @daejunpark offered the axiomatic definition:

(declare-fun intExp (Int Int) Int)
(assert
  (forall
    ( (X Int) (N Int) )
    (implies
      (and (< 0 X) (< 0 N))
      (= (intExp X N) (to_int (^ X N))))))

Unfortunately, this partial definition is not compatible with our SMT hook syntax. It would be useful to have an auxiliary syntax that permits a declaration and series of axioms that define a partial function.

Example K Code

[smt-hook-decl((declare-fun intExp (Int Int) Int)), smt-hook-axiom((forall ((X Int) ...)]

Potential Alternatives/Work-arounds

The alternative approach is to define additional functions in an SMT prelude, but we don't want to be doing this at all (per @ehildenb), so adding new hook syntax is likely to be the most sensible option.

[ehildenb]

We should have the K code use K rules for specifying the SMT axioms, not directly in the attributes as much as possible. The attributes in K have their own special parser and I think it can quickly become too hard to encode. Besides, we should strive to present as much in K directly as possible.

What I suggested on Slack was the addition of something like non-executable axiom or smt-only axiom for rules, like this:

syntax Int ::= Int "^Int" Int [smtlib(kExpInt), function]

syntax Int ::= smtExp(Int, Int) [smt-hook((to_int (^ #1 #2))), function, no-evaluators, private]

rule I1 ^Int I2 => smtExp(I1, I2) requires 0 <Int I1 andBool 0 <Int I2 [smt-lemma, smt-only]

So that we can send arbitrary horn clauses (as conditional rules) to the SMT solver as axioms for symbols, but only require from K additional support for smt-only attribute (backend change, they basically just need to ignore these rules, we could also call it non-executable).

This is a very minimal change to make, and we already have support for smt-lemma.

[Baltoli]

That makes sense to me. What is kExpInt in your code example?

[daejunpark]

That makes sense to me. What is kExpInt in your code example?

It serves as a symbol declaration. Whenever a new symbol appears in smtlib(), the backend automatically generates a declaration of the symbol in the smt query.

[ehildenb]

We should probably just add support for no-execute or non-executable attribute on rules. This is more broadly useful (and probably simpler) than the specific smt-only attribute.

The non-executable attribute on a rule means that the backends should not try to use that rule for rewriting.

[Baltoli]

Current status:

• The [non-executable] attribute is nearly done:
  • LLVM backend support is merged (Add support for [non-executable] attribute llvm-backend#478)
  • Haskell backend support blocked on a clarification (Add NonExecutable attribute haskell-backend#2945)
  • Frontend tests written; waiting for same clarification (Tests for [non-executable] attribute #2400)

Once these are all merged, the partial SMT hooks listed above can be implemented along with tests that the correct clauses are being sent to Z3.

[Baltoli]

Per Nikolaj's comment on my issue here, it turns out that Z3 is unable to prove assertions in the format that the Haskell backend is generating for this proof.

In the short term, we agreed in the K frontend meeting that the most sensible thing to do is to keep the failing test disabled. The remaining solutions are:

• Implement support for non-executable in the Java backend as well as LLVM / Haskell (presumably we don't want to be doing this).
• Audit the way that the Haskell backend emits constraints for integer problems involving exponentiation. This may be fragile with respect to future changes in Z3.