`size(List)` function cannot be encoded to smt despite having smtlib attribute

[dwightguth]

I am attaching a tarball with the definition.kore and spec.kore that are required to reproduce. You can run the example with:

kore-exec definition.kore --module VERIFICATION --prove spec.kore --spec-module SUM-TO-N-SPEC

If you inspect definition.kore, you will see the following SMT lemma:

rule 0 <= size(_:List) => true [simplification, smt-lemma]

However, the final state returned by the backend includes the following constraint:

  {
    true
  #Equals
    size ( WS:List ) <Int -1
  }

It ought to be able to disprove this state using the smt lemma, however, it does not. I imagine this is due to a failure to translate the size symbol, as indicated by the following warnings:

kore-exec: [6744874] Warning (WarnSymbolSMTRepresentation):
    Cannot translate symbol despite being given an SMT-LIB expression
        Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}
Context:
    (DebugEvaluateCondition) while evaluating predicate
        (InfoReachability) while simplifying the claim
kore-exec: [6758258] Warning (WarnSymbolSMTRepresentation):
    Cannot translate symbol despite being given an SMT-LIB expression
        Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}
Context:
    (DebugEvaluateCondition) while evaluating predicate
        (InfoReachability) while checking the implication

The prover generates a large number of this type of warning. No other warnings are generated, so I'm unclear what the issue is. bug-report.tar.gz

[jberthold]

I managed to drastically cut down the definition file attached here, definition-cut-down.kore.txt

Essentially, the presence of a certain no-junk axiom for a user-defined list variant (WS) seems to lead to the removal of SMT-lib symbols for a number of List related functions. I will have to take another deep-dive into the old code to find out why that is.

Also note:

1. there is a duplicate simplification rule 0 <= size(_:List) => true [simplification, smt-lemma], but that's not the reason for the failure
2. The warning is also shown when loading the definition.kore into kore-rpc (during the initial SMT check that the lemmas are consistent).

[jberthold]

So... after inspecting the source code for the SMT bindings, I came to conclude that the no-junk axiom, which was generated from the _WS_ and .WS is in fact invalid:

  axiom{} \or{SortList{}} (\exists{SortList{}} (X0:SortInt{}, \exists{SortList{}} (X1:SortList{}, Lbl'Unds'WS'Unds'{}(X0:SortInt{}, X1:SortList{}))), LbldotWS{}(), \bottom{SortList{}}()) [constructor{}()] // no junk

Isn't this saying that anything of SortList is constructed by using either the _WS_ or the .WS constructor? How about other ways to construct a list, like ListItem or .List?

@dwightguth may I ask what the K source code for symbols _WS_ and .WS looks like? (Source code location: evm-types.md, lines 230 and 231) Are these probably generated from a List directive in K?

What happens then is that the legacy backend extracts the constructors from the (incomplete) no-junk axiom and then removes the symbols relating to the original SortList (among them, the now-missing smt_seq_len).

I have created https://github.com/runtimeverification/k/issues/4150 to track this issue. I don't think macro syntax should be considered when generating no junk axioms.

As a work-around for your particular issue, could you use a subsort instead of SortList directly for your WordStack definition?