Tips and tricks to make VST proof development faster

[akinanop]

Dear VST developers and everyone who is using VST,

I am working on an industrial verification project that uses Verified Software Toolchain (until now we have ~300 loc verified, but we aim at ~1800 in the near future), and compilation times for common tactics became an issue. In particular, forward, forward_call, entailer! can take up to 1 min to execute. Since proofs range between 500 and 3000 loc, and these are very common tactics, the development becomes very slow and painful. Is this normal? Are there ways to speed up the process? Is there anyone from VST community who could share their expertise on this topic? It will be very much appreciated!

[MSoegtropIMC]

Hi Nika,

a few observations:

• VST frequently converts between different representations of the list of local variables, namely a list and a ptree and needs to provide a proof that both representations are equivalent. This can get quite slow if you have many local variables. Sometimes I replace the function which creates that proof with something else which is faster but doesn’t cover all cases, but I have to dig out the details. What generally helps more is to split functions with many variables in several pieces with fewer variables. Otherwise one would have to rewrite the VST automation such that it does the list -> ptree translation once at the start of the function. The main downside of that would be that the list of local variables would not be ununderstandable as it is any more - one would have to use tactics to inspect it.

• VST applies simpl and/or cbn to some subterms of your context, which can be slow up to taking a really long time (more in the astronomic than in the biblic sense). It helps to keep your context in a shape where “simpl in *” or “cbn in *” don’t take forever. This can be achieved e.g. by abstracting sub terms or by controling opacity of definitions.

• I tend to use entailer instead of entailer! and use special build tactics to preprocess / postprocess the goal such that entailer works.

• Do all the complicated part in separate lemmas - use VST just to prove that the C code implements an abstraction which is very close to the C code - then you spend less time in the VST part.

• Use the Ltac debugger to see what the tactics actually do.

• Tell your boss that a PC with a 5GHz CPU is well spent money.

I have very few cases where any of these tactics takes more than 5 seconds and usually it is below one second.

Best regards,

Michael

[akinanop]

Thanks for these suggestions!
Do I understand correctly the first point: you rewrite the C code to avoid many local variables? We work with legacy code that we prefer not to modify unless really necessary. What would be the optimal amount of vars?

Is the stuff you are working on publicly available? We would really appreciate if we could look at existing VST projects and learn from best practices, but I haven’t seen many around.

[MSoegtropIMC]

We verify code we write, so we can take this into account upfront. I would say it starts to get noticably slow beyond 20 local variables. Unfortunately the code I work on is proprietary. Did you look at e.g. the HMAC verification from Princeton? This is a verification of non trivial legacy code.

[akinanop]

It seems that the number of temp variables is indeed the main problem in my proof. With forward_call (which is typically slower than other tactics) it gets out of hand quite fast, it seems like exponentially fast, which is an issue. I tried reducing the number of local vars in one of my projects and that’s what I got when executing forward_call (with cleared context).