[K-Improvement] Allow importing module as trusted

[virgil-serbanuta]

Per the Examples above please provide some Improvement Suggestions

Motivation

Sometimes, when proving a claim, it is useful to use other claims.

As an example, for the Multisig proofs, there were claims describing what each endpoint does, then there were claims which described how the endpoints interacted (e.g. one was saying that no matter what endpoint a certain user called, it was impossible to do anything without help from other users).

Another example: usually, when proving equality lemmas, a "start => done" lemma is enough. However, some lemmas require proofs that are more complex, these proofs may use other lemmas.

It is usually desirable to prove all these lemmas. But, with the current K, there are only imperfect options:

1. Put all claims in a module and have K prove all of them at once, which also allows using the claims to prove other claims. This also ensures that any circular dependencies between lemmas are properly handled. However, this is impractical for larger collections of lemmas.
2. Have two versions of each claim, one for proving and another one marked as [trusted] and use module imports to ensure that there are no circular dependencies. This works, but maintaining identical versions of lemmas may be tedious.
3. For each claim, have a rewrite rule that applies it. This is similar to the above, but has the drawback that it can be applied at the first step of proving a claim, and it care in order to make sure that there are no circular dependencies.

Example

I would like to be able to import claim modules as trusted, e.g.

module A
  imports trusted B
  claim a => end
endmodule

module B
  claim b => end
endmodule

This would work in the same way as:

module A
  claim a => end
  claim b => end  [trusted]
endmodule

module B
  claim b => end
endmodule

Documentation

Users can import modules with claims as trusted with imports trusted MODULE-NAME. This imports all the claims available in B, but adds the [trusted] attribute to them. These claims would only be available in the module that imports them directly. Note that, with the following imports:

module A
  import B
  import C
endmodule
module B
  import trusted C
endmodule
module C
endmodule

the trusted lemmas from C are only available in B. However, when using A as the main module to prove, lemmas from C are available and need to be proved because of the direct import.

Potential Alternatives

One alternative would be to use external tools to preprocess claim files one way or another, creating [trusted] duplicates for claims and ensuring that all claims are available where needed.

[Baltoli]

@virgil-serbanuta we discussed this yesterday and had a follow-up question that will help us figure out the best way to implement this (i.e. whether it becomes a core language feature imports trusted or whether we implement it as a preprocessing step elsewhere).

For the project you'd like this feature to be available, how are you running the proofs in question? Via kprove, pyk prove or some custom proving logic implemented in Pyk?

[virgil-serbanuta]

At the moment, we are proving the claims mentioned above either with kprove, or with a thin pyk-based tool that basically just calls kprove. We may move to pyk prove in the future. We have no plans for using custom proving logic in pyk, but we may do that if it helps and it's not too involved.

FWIW, my current plan if nothing else works is to make a tool that duplicates the modules containing the claims, adding the [trusted] attribute, something like a.k

module A
  claim stuff
endmodule

would become a.k

module A
  claim stuff
endmodule

module A-TRUSTED
  claim stuff [trusted]
endmodule

and then I would rely on the checks that run on Github to keep the trusted claims up to date.

[Baltoli]

@Baltoli write this up into a new issue; consensus is the best thing to do here is write Pyk tooling to manage the dependency graph.

[virgil-serbanuta]

I will try to describe what I am trying to do as best as I can with the limited time I have now.

Let me take a simple example. I had a lemma that looks something like this (it's more complex now):

  rule log2Int(N) <Int M => true requires N <Int 2 ^Int 1000 andBool 1000 <Int M

IIRC z3 doesn't know how to handle log2Int and ^Int (if it does, I can find other examples involving divInt and modInt, which are poorly handled).

In order to prove this, I will likely need the following lemmas, or something similar (I didn't think much about this, I may be wrong):

  rule N <Int 2 ^Int (log2Int(N) +Int 1) => true
  rule 2 ^Int log2Int(N) <=Int N

In turn, these are likely to need other lemmas.

While working on previous contracts I had a script that generated both claims and simplification rules for these, claims were grouped in "levels", and, when proving each level, I had access to the simplification rules from the previous levels. This ensured that no claim proves itself and mostly worked. However, it was complicated and hard to maintain, and there were cases when this did not work.

The problem was that the simplification rules from the previous levels were applied always, and sometimes I needed more fine-grained control over what is being applied. This was solvable: for each simplification rule I would skip generating the actual rule until the end of this process, then I just added a constructor + a rewrite rule + a claim + a trusted claim for each lemma, and I would import the trusted claim when I needed it for proving. Then I just needed to add a constructor invocation of the rule in my proof, the trusted claim would apply properly, and it would add whatever I needed to the side condition.

However, this meant that I had a tree of claims that I needed to manage safely.

The current project seems to be going in the same direction, so I filed this issue.

[virgil-serbanuta]

FWIW, the above also applied to proofs about code execution, e.g. I had claims summarizing functions, they imported each other, and they were imported by higher level proofs. However, this is not currently needed for the kasmer project.

[Baltoli]

Thanks @virgil-serbanuta, that's really helpful context. My high-level summary of what we need to implement in Pyk here is a mechanism for specifying (in code, or in configuration) the dependency graph between these levelized modules. Then, we can define a new kind of prover (or extend an existing one) that can walk the dependency graph and prove your claims in the correct order.

We can use the dependency graph information to then automate the construction of appropriate trusted claims when proving later specifications, so that you don't have to go through that manual process of constructing claims.