Add "Procedure" section to protocol spec.

[nathan-at-least]

A Procedure section will specify "canonical" storage structures and algorithms which implement the protocol. For example, there should be an inductive procedure for "Verify Block".

Implementations may use different data structures/algorithms, and this section should strive to define the simplest to specify data structures and algorithms, rather than the most efficient. If there is a discrepency between an efficient real-world implementation and an algorithm here which affects the protocol, then we need to go through a rigorous process for altering the protocol if we deem it necessary. If there's a discrepency in implementation vs "canonical algorithm" that does not affect the protocol, then the canonical algorithm should either be simplified until there's no discrepency, or we add a footnote about the discrepency, or we change the canonical algorithm to be more complex.

Also, a given canonical algorithm/data-structures will imply a set of invariants / preconditions / postconditions. Those should be explicitly documented also in this spec.

[daira]

I am wary of overspecification by taking this approach.

[daira]

I'm happy with the current style of specification. Some things (e.g. the note encryption) are specified using canonical algorithms; others are not.