Fine Grained Module Definitions

[Cameron-Low]

The goal of this PR is to introduce a new mechanism that permits the user to create a new module by slightly tweaking an existing module definition.

At present the draft has the following features:

• Introduce new module variables.
• Introduce new local variables.
• Delete/Modify/Add statements at particular code positions
• Delete branches (match support is not currently working fully)
• Modify branch conditions
• Insert new branches around a chunk of code
• Modify the return expression

Syntax (needs work) :

module N = M with {
  var x : t (* add new module variable *)
  proc f [
     var y  : s (* add new local variable *)
     cp +/-/~ { s } (* insert after/insert before/modify a statement *)
     cp -  (* delete a statement *)
     cp + ( e ) (* insert new if statement with condition `e` surrounding the suffix code block *)
     cp - ./?/#cstr (* delete all other branches except true/false/cstr *)
  ] res ~ ( e ) (* change the return expression *)
}

[fdupress]

Can you please edit the message above to add syntax for each of the transformations? This will help in reviewing, independently of also creating a wiki page.

[Cameron-Low]

This is now ready for review. I've made a wiki page to document the features present.

[fdupress]

This looks good to me. It does affect the non-interactive readability of scripts, so kind of increases the priority of proof documentation features.

As it stands, nothing forces usage, so this is fine to merge in order to allow engagement with the tool and user communities.

[strub]

I only have minor comments (see above). Also, squash your commits. But overall, we are good to go.