Line Editing, History and Basic Completion for CryptoVerif's Interactive Mode

Using the ‘readline wrapper’ rlwrap we can introduce line editing, history and also some very basic completion support to the interactive mode in CryptoVerif without the need to modify CryptoVerif itself. The completion is therefore very basic and has no context at all.

To use it, run cryptoverif preceeded with rlwrap.

Line Editing and Non-Persistent History

Simply run

rlwrap cryptoverif some_file.cv

Line Editing and Persistent History

Giving an absolute filename leads to a shared history between all CryptoVerif calls, a relative filename only to a shared history between all calls in the same directory.

rlwrap --history-filename ~/.rlwrap_hist_cryptoverif cryptoverif some_file.cv

Adding Completion

For use with the basic completion feature of rlwrap we prepared a file containing all possible keywords, commands, parameters, and the equivalences defined in default.cvl.

Please note that this completion does not have any context.

Copy Completion File to Home Directory

To install the completion file to a hidden file in your home directory you can use

make install

Use Completion

The full command to use CryptoVerif with this feature is

rlwrap --history-filename ~/.rlwrap_hist_cryptoverif --break-chars "(){}[],+=&^%$#@"";|\\" --file ~/.rlwrap_cryptoverif_completion.conf cryptoverif some_file.cv

Use It In A Script

The Bash script rlwrap.bash can be used in scripts to call CryptoVerif with the rlwrap wrapper. Use it as follows:

• set some variables to modify the behavior, they are set with reasonable defaults:
  • RLWRAP_HIST_FILE: location of the file to which command history should be written, and from which it should be read
  • RLWRAP_GLOBAL_COMPLETION_FILE: location of a file with completion chunks, defaults to the file present in this repository
  • RLWRAP_LOCAL_COMPLETION_FILE: location of a second file with completion chunks, defaults to the file rlwrap_cryptoverif_completion.conf in the current directory of the calling script; this is meant to be used for completion chunks custom to a CryptoVerif project
• in your own Bash script, source the file rlwrap.bash, for example with

. ./cryptoverif-completion/rlwrap.bash

• call CryptoVerif with ${RLWRAP_CMD} cryptoverif

Adding an Alias in Your Shell

Because this is quite long we suggest adding an alias to your shell configuration. In ZSH this can look like this:

# --break-chars is just the default without ' and - because they are
# part of some chunks we want to complete
alias cryptoverif='rlwrap --history-filename ~/.rlwrap_hist_cryptoverif --break-chars "(){}[],+=&^%$#@"";|\\" --file ~/.rlwrap_cryptoverif_completion.conf cryptoverif'

Changing Completion Chunks

The file rlwrap_cryptoverif_completion_with_comments.conf contains the chunks with some comments where they have been found in CryptoVerif's code or in the manual. These comments must be removed, otherwise rlwrap will pick them up as completion chunks, which is why there is the file rlwrap_cryptoverif_completion.conf.

If you ever change something in rlwrap_cryptoverif_completion_with_comments.conf you can produce the file without comments by using:

make all

And then copy it to the right destination with

make install