Re: [isabelle] Efficient Lookups in Lists



There are several possible solutions.

0. If your application is executable you may be able to generate ML code from it and run it completely independently of Isabelle. The speedup will be about 100. If it is almost executable, it may be worth making it fully executable (eg an implementation of finite sets as lists is already in the Library).

1. You, as you say, bypass the the simplifier by writing an oracle, i.e. trusted piece of ML code that checks if an element is in a list/set. This is probably the quick an dirty solution (although you need to familiarize yourself with oracles).

2. You explicitly use some efficient data structure rather than a list or set, eg a binary tree. This is completely safe, requires no low-level coding, but you will need to develop the efficient data structure (the theory BinarySearchTree in the AFP may provide much of what you need) and will need to use it rather than the abstract type of list/function/set (which should not complicate proofs much).

3. Alternative 0 can also be used "locally" by compiling executable goals like "a mem [...]" into ML and executing them there. The development version of Isabelle contains a proof method "evaluation" which does just this. However, currently it can only be used to solve a goal outright and it is not integrated with other proof tools. More flexible versions are in preparation.

4. You can use "reflection" to translate you list/function/set problem into some efficient data structure and execute it there. In contrast to alternative 2 you only do this reflection at specific points (when you need to solve expensive goals) but otherwise work with the usual mathematical types of lists/sets/etc. Efficiency is guaranteed as in 3.

Thanks for bringing this up. Efficient executability is an important issue we are working on at the moment. Challenge problems are welcome.

Tobias

Jan Olaf Blech schrieb:
Hi,

We use Isabelle/HOL in a compiler runtime verification environment. The verification process comprises "lookup operations" in lists, function updates and sets, i.e. proving lemmata of the following form:

lemma "a mem [...,a,...]"
lemma "f (...,a:= b,...) a = b"
lemma "a : {...,a,...}"

If the lists, function updates, and sets grow large, these lookups take up almost all of the time of a verification run. In our current version we instantiate Isabelle's simplifier with some simple rules like

   "x  = a | x : A ==> x : insert a A"

to achieve time linear to the size of the underlying structure the lookup is conducted on. However a lookup still takes quite long: several minutes for a list of a few thousand elements. For the verification of some relatively small programs thousands of lookups are needed in structures containing thousands of elements.

Is anyone aware of a technique to do this faster?

What do you think of "bypassing" Isabelle's simplifier to make such lookups faster? One problem is probably that we would "spoil" the Isabelle implementation and the "trusted computing base" would grow larger.

Regards

Jan Olaf Blech





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.