How to count implementation lines written in Vale?

[zpzigi]

In Vale's paper, implementation lines which consist of assembly instructions and control-flow code are calculated.
I've been building a system with Vale/Dafny and I am not sure how to calculate implementation lines.

For Dafny, dafny-line-count.py in IronFleet helps to calculate Spec and Proof lines.
Is there any similar script or tool for calculating implementation lines written in Vale?

Regards,

[Chris-Hawblitzel]

I don't know of any scripts, but there are some Vale command-line options that the paper relied on. The -reprint <...filename...> option pretty-prints a copy of the program, discarding comments and extra blank lines. Various other options, like -reprintSpecs=false, -reprintGhostDecls=false, -reprintGhostStmts=false, -reprintLoopInvs=false, and -reprintVerbatims=false omit proof-related code from the pretty-printed copy. Comparing the line count of the pretty-printed versions with and without some of these options can tell you the implementation and proof size. This is similar to the /rprint and /printMode:NoGhost options used by dafny-line-count.py.

We kept the trusted specifications in separate files for the purpose of measuring the "Spec" size. This is similar to the is_spec in dafny-line-count.py, which looks for specification files based on a filename convention.

[Chris-Hawblitzel]

Also, you might want to set -typecheck=false when reprinting. The typechecker, which was added after the original Vale paper, adds some clutter when elaborating names and expressions.