[isabelle] Efficient Lookups in Lists


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.


Jan Olaf Blech

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