[Docs] [txt|pdf|xml|html] [Tracker] [Email] [Diff1] [Diff2] [Nits]

Versions: 00 01 02 03 04 05

Network Working Group                                  M. Petit-Huguenin
Internet-Draft                                    Impedance Mismatch LLC
Intended status: Experimental                            1 February 2021
Expires: 5 August 2021


                  The Computerate Specifying Paradigm
             draft-petithuguenin-computerate-specifying-05

Abstract

   This document specifies a paradigm named Computerate Specifying,
   designed to simultaneously document and formally specify
   communication protocols.  This paradigm can be applied to any
   document produced by any Standard Developing Organization (SDO), but
   this document targets specifically documents produced by the IETF.

Status of This Memo

   This Internet-Draft is submitted in full conformance with the
   provisions of BCP 78 and BCP 79.

   Internet-Drafts are working documents of the Internet Engineering
   Task Force (IETF).  Note that other groups may also distribute
   working documents as Internet-Drafts.  The list of current Internet-
   Drafts is at https://datatracker.ietf.org/drafts/current/.

   Internet-Drafts are draft documents valid for a maximum of six months
   and may be updated, replaced, or obsoleted by other documents at any
   time.  It is inappropriate to use Internet-Drafts as reference
   material or to cite them other than as "work in progress."

   This Internet-Draft will expire on 5 August 2021.

Copyright Notice

   Copyright (c) 2021 IETF Trust and the persons identified as the
   document authors.  All rights reserved.

   This document is subject to BCP 78 and the IETF Trust's Legal
   Provisions Relating to IETF Documents (https://trustee.ietf.org/
   license-info) in effect on the date of publication of this document.
   Please review these documents carefully, as they describe your rights
   and restrictions with respect to this document.  Code Components
   extracted from this document must include Simplified BSD License text
   as described in Section 4.e of the Trust Legal Provisions and are
   provided without warranty as described in the Simplified BSD License.




Petit-Huguenin            Expires 5 August 2021                 [Page 1]


Internet-Draft           Computerate Specifying            February 2021


Table of Contents

   1.  Introduction  . . . . . . . . . . . . . . . . . . . . . . . .   4
   2.  Overview  . . . . . . . . . . . . . . . . . . . . . . . . . .   5
   3.  Terminology . . . . . . . . . . . . . . . . . . . . . . . . .   5
   4.  Private Specifications  . . . . . . . . . . . . . . . . . . .   6
     4.1.  Private Specifications for New Documents  . . . . . . . .   9
     4.2.  Private Specifications for Existing Documents . . . . . .  10
   5.  Self-Contained Specifications . . . . . . . . . . . . . . . .  11
     5.1.  PDU Descriptions  . . . . . . . . . . . . . . . . . . . .  11
       5.1.1.  PDU Examples  . . . . . . . . . . . . . . . . . . . .  12
       5.1.2.  Calculations from PDU . . . . . . . . . . . . . . . .  15
       5.1.3.  PDU Representations . . . . . . . . . . . . . . . . .  16
     5.2.  State Machines  . . . . . . . . . . . . . . . . . . . . .  17
     5.3.  Proofs  . . . . . . . . . . . . . . . . . . . . . . . . .  18
       5.3.1.  Wire Type vs Abstract Type  . . . . . . . . . . . . .  19
       5.3.2.  Data Format Conversion  . . . . . . . . . . . . . . .  22
       5.3.3.  Postel's Law  . . . . . . . . . . . . . . . . . . . .  22
       5.3.4.  Implementability  . . . . . . . . . . . . . . . . . .  25
       5.3.5.  Termination . . . . . . . . . . . . . . . . . . . . .  26
       5.3.6.  Liveness  . . . . . . . . . . . . . . . . . . . . . .  26
   6.  Importing Specifications  . . . . . . . . . . . . . . . . . .  26
     6.1.  Common Modules  . . . . . . . . . . . . . . . . . . . . .  28
       6.1.1.  Generating AsciiDoc . . . . . . . . . . . . . . . . .  28
       6.1.2.  Common Data Types . . . . . . . . . . . . . . . . . .  29
       6.1.3.  Calculations  . . . . . . . . . . . . . . . . . . . .  33
       6.1.4.  Typed Petri Nets  . . . . . . . . . . . . . . . . . .  34
       6.1.5.  Representations . . . . . . . . . . . . . . . . . . .  36
         6.1.5.1.  Bit Diagrams  . . . . . . . . . . . . . . . . . .  37
         6.1.5.2.  Message Sequence Charts . . . . . . . . . . . . .  38
     6.2.  Packages for Meta-Languages . . . . . . . . . . . . . . .  38
       6.2.1.  Augmented BNF (ABNF)  . . . . . . . . . . . . . . . .  41
       6.2.2.  Augmented Packet Header Diagrams (APHD) . . . . . . .  42
       6.2.3.  Cosmogol  . . . . . . . . . . . . . . . . . . . . . .  44
     6.3.  Packages for Protocols  . . . . . . . . . . . . . . . . .  44
       6.3.1.  Type Transformations  . . . . . . . . . . . . . . . .  45
       6.3.2.  Extended Registries . . . . . . . . . . . . . . . . .  48
   7.  Exporting Specifications  . . . . . . . . . . . . . . . . . .  50
     7.1.  Standard Library  . . . . . . . . . . . . . . . . . . . .  50
     7.2.  Transclusions . . . . . . . . . . . . . . . . . . . . . .  52
     7.3.  Exporting Types and Functions . . . . . . . . . . . . . .  52
   8.  Standard Library  . . . . . . . . . . . . . . . . . . . . . .  52
     8.1.  Internal Modules  . . . . . . . . . . . . . . . . . . . .  52
       8.1.1.  AsciiDoc  . . . . . . . . . . . . . . . . . . . . . .  53
       8.1.2.  BitVector . . . . . . . . . . . . . . . . . . . . . .  53
       8.1.3.  Unsigned  . . . . . . . . . . . . . . . . . . . . . .  54
       8.1.4.  Dimension . . . . . . . . . . . . . . . . . . . . . .  54
       8.1.5.  BitDiagram  . . . . . . . . . . . . . . . . . . . . .  55



Petit-Huguenin            Expires 5 August 2021                 [Page 2]


Internet-Draft           Computerate Specifying            February 2021


       8.1.6.  Transform . . . . . . . . . . . . . . . . . . . . . .  55
       8.1.7.  Tpn . . . . . . . . . . . . . . . . . . . . . . . . .  56
     8.2.  Meta-Language Packages  . . . . . . . . . . . . . . . . .  56
       8.2.1.  Augmented Packet Header Diagrams (APHD) . . . . . . .  56
       8.2.2.  RFC 5234 (ABNF) . . . . . . . . . . . . . . . . . . .  56
     8.3.  Protocol Packages . . . . . . . . . . . . . . . . . . . .  56
       8.3.1.  RFC 791 (Internet Protocol) . . . . . . . . . . . . .  56
   9.  Bibliography  . . . . . . . . . . . . . . . . . . . . . . . .  56
   Appendix A.  Command Line Tools . . . . . . . . . . . . . . . . .  59
     A.1.  Installation  . . . . . . . . . . . . . . . . . . . . . .  60
       A.1.1.  Download the Docker Image . . . . . . . . . . . . . .  60
     A.2.  The "computerate" Command . . . . . . . . . . . . . . . .  60
       A.2.1.  Literate Files  . . . . . . . . . . . . . . . . . . .  61
       A.2.2.  Transclusions . . . . . . . . . . . . . . . . . . . .  61
       A.2.3.  IdrisDoc Generation . . . . . . . . . . . . . . . . .  62
       A.2.4.  Outputs . . . . . . . . . . . . . . . . . . . . . . .  62
       A.2.5.  Extended Registry . . . . . . . . . . . . . . . . . .  62
       A.2.6.  Bibliography  . . . . . . . . . . . . . . . . . . . .  63
         A.2.6.1.  Internet-Draft  . . . . . . . . . . . . . . . . .  63
         A.2.6.2.  RFC . . . . . . . . . . . . . . . . . . . . . . .  64
         A.2.6.3.  Email . . . . . . . . . . . . . . . . . . . . . .  65
         A.2.6.4.  IANA  . . . . . . . . . . . . . . . . . . . . . .  66
         A.2.6.5.  Web-Based Public Code Repositories  . . . . . . .  66
     A.3.  Idris REPL  . . . . . . . . . . . . . . . . . . . . . . .  66
     A.4.  Other Commands  . . . . . . . . . . . . . . . . . . . . .  67
     A.5.  Source Repositories . . . . . . . . . . . . . . . . . . .  67
     A.6.  Modified Tools  . . . . . . . . . . . . . . . . . . . . .  67
       A.6.1.  Idris2  . . . . . . . . . . . . . . . . . . . . . . .  67
       A.6.2.  asciidoctor . . . . . . . . . . . . . . . . . . . . .  68
       A.6.3.  metanorma . . . . . . . . . . . . . . . . . . . . . .  68
       A.6.4.  metanorma-ietf  . . . . . . . . . . . . . . . . . . .  68
       A.6.5.  idris2-vim  . . . . . . . . . . . . . . . . . . . . .  69
     A.7.  Bugs and Workarounds  . . . . . . . . . . . . . . . . . .  69
     A.8.  TODO List . . . . . . . . . . . . . . . . . . . . . . . .  70
   Appendix B.  Reference  . . . . . . . . . . . . . . . . . . . . .  71
     B.1.  Package computerate-specifying  . . . . . . . . . . . . .  71
       B.1.1.  Module ComputerateSpecifying.AsciiDoc . . . . . . . .  71
       B.1.2.  Module ComputerateSpecifying.BitDiagram . . . . . . .  72
       B.1.3.  Module ComputerateSpecifying.BitVector  . . . . . . .  73
       B.1.4.  Module ComputerateSpecifying.Dimension  . . . . . . .  74
       B.1.5.  Module ComputerateSpecifying.Tpn  . . . . . . . . . .  76
       B.1.6.  Module ComputerateSpecifying.Transform  . . . . . . .  77
       B.1.7.  Module ComputerateSpecifying.Unsigned . . . . . . . .  78
     B.2.  Package rfc5234 . . . . . . . . . . . . . . . . . . . . .  79
       B.2.1.  Module RFC5234.Core . . . . . . . . . . . . . . . . .  79
       B.2.2.  Module RFC5234.Main . . . . . . . . . . . . . . . . .  80
     B.3.  Package augmented-ascii-diagrams  . . . . . . . . . . . .  81
       B.3.1.  Module AAD.Main . . . . . . . . . . . . . . . . . . .  81



Petit-Huguenin            Expires 5 August 2021                 [Page 3]


Internet-Draft           Computerate Specifying            February 2021


     B.4.  Package rfc791  . . . . . . . . . . . . . . . . . . . . .  82
       B.4.1.  Module RFC791.Address . . . . . . . . . . . . . . . .  82
       B.4.2.  Module RFC791.IP  . . . . . . . . . . . . . . . . . .  83
   Appendix C.  Errata Statistics  . . . . . . . . . . . . . . . . .  84
   Acknowledgements  . . . . . . . . . . . . . . . . . . . . . . . .  86
   Contributors  . . . . . . . . . . . . . . . . . . . . . . . . . .  87
   Changelog . . . . . . . . . . . . . . . . . . . . . . . . . . . .  87
   Author's Address  . . . . . . . . . . . . . . . . . . . . . . . .  90

1.  Introduction

   If, as the unofficial IETF motto states, we believe that "running
   code" is an important part of the feedback provided to the
   standardization process, then as per the Curry-Howard equivalence
   [Curry-Howard] (that states that code and mathematical proofs are the
   same), we ought to also believe that "verified proof" is an equally
   important part of that feedback.  A verified proof is a mathematical
   proof of a logical proposition that was mechanically verified by a
   computer, as opposed to just peer-reviewed.

   The "Experiences with Protocol Description" paper from Pamela Zave
   [Zave11] gives three conclusions about the usage of formal
   specifications for a protocol standard.  The first conclusion states
   that informal methods (i.e. the absence of verified proofs) are
   inadequate for widely used protocols.  This document is based on the
   assumption that this conclusion is correct, so its validity will not
   be discussed further.

   The second conclusion states that formal specifications are useful
   even if they fall short of the "gold standard" of a complete formal
   specification.  We will show that a formal specification can be
   incrementally added to a document.

   The third conclusion from Zave's paper states that the normative
   English language should be paraphrasing the formal specification.
   The difficulty here is that to be able to keep the formal
   specification and the normative language synchronized at all times,
   these two should be kept as physically close as possible to each
   other.

   To do that we introduce the concept of "Computerate Specifying" (note
   that Computerate is a British English word).  "Computerate
   Specifying" is a play on "Literate Computing", itself a play on
   "Structured Computing" (see [Knuth92] page 99).  In the same way that
   Literate Programming enriches code by interspersing it with its own
   documentation, Computerate Specifying enriches a standard
   specification by interspersing it with code (or with proofs, as they
   are the same thing), making it a computerate specification.



Petit-Huguenin            Expires 5 August 2021                 [Page 4]


Internet-Draft           Computerate Specifying            February 2021


   Note that computerate specifying is not specific to the IETF, just
   like literate computing is not restricted to the combination of Tex
   and Pascal described in Knuth's paper.  What this document describes
   is a specific instance of computerate specifying that combines
   [AsciiDoc] as formatting language and [Idris2] as programming
   language with the goal of formally specifying IETF protocols.

2.  Overview

   The remaining of this document is divided in 3 parts:

   After the Terminology (Section 3) section starts a tutorial on how to
   write a specification.  This tutorial is meant to be read in
   sequence, as concepts defined in early part will not be repeated
   later.  On the other hand the tutorial is designed to present
   information progressively and mostly in order of complexity, so it is
   possible to start writing effective specifications without reading or
   understanding the whole tutorial.

   The tutorial begins by explaining how to write private specifications
   (Section 4), which are specifications that are not meant to be
   shared.  Then the tutorial continues by explaining how to write an
   self-contained specification (Section 5), which is a specification
   that contains Idris code that relies only on the Idris Standard
   Library.  Writing self-contained specifications is difficult and
   time-consuming, so the tutorial continues by explained how to import
   specifications (Section 6) that contain reusable types and code.  The
   tutorial ends with explanations on how to design a exportable
   specification (Section 7).

   After the tutorial come the description of all the packages and
   modules in the Computerate Specifying Standard Library (Section 8).

   Appendix A explains how to install and use the associated tooling,
   and Appendix B contains the reference manual for the standard
   library.

3.  Terminology

   Computerate Specification, Specification:  Literate Idris2 code
      embedded in an AsciiDoc document, containing both formal
      descriptions and human language texts, and which can be processed
      to produce documents in human language.

   Document:  Any text that contains the documentation of a protocol in
      the English language.  A document is the result of processing a
      specification.




Petit-Huguenin            Expires 5 August 2021                 [Page 5]


Internet-Draft           Computerate Specifying            February 2021


   Retrofitted Specification:  A specification created after a document
      was published such as the generated document coincides with the
      published document.

   In this document, the same word can be used either as an English word
   or as an Idris identifier used inside the text.  To explicitly
   differentiate them, the latter is always displayed like "this".  E.g.
   "IdrisDoc" is meant to convey the fact that IdrisDoc in that case is
   an Idris module or type.  On the other hand the word IdrisDoc refers
   to the IdrisDoc specification.

   Similarly blocks of code, including literate code, are always
   sandwiched between "<CODE BEGINS>" and "<CODE ENDS>".  Code blocks
   will be presented in their literate form only when necessary, i.e.
   when mixed AsciiDoc and Idris are required.  However, in a
   computerate specification, Idris code must in fact be used in its
   literate form.

   By convention an Idris function that returns a type and types
   themselves will always start with an uppercase letter.  Functions not
   returning a type start with a lowercase letter.

   For the standard library, the types names are also formed by taking
   the English word or expression, making the first letter of each word
   upper case, and removing any symbols like underscore, dash and space.
   Thus bitvector would become "Bitvector" after conversion as a type
   name but bit diagram would become "BitDiagram".

4.  Private Specifications

   Nowadays documents at the IETF are written in a format named xml2rfc
   v3 [RFC7991] but unfortunately making that format Computerable is not
   trivial, mostly because there is no simple solution to mix code and
   XML together in the same file.  Instead, the [AsciiDoc] format forms
   the basis for specifications as it permits the generation of
   documents in the xmlrfc v3 format (among other formats) and also
   because it can be enriched with code in the same file.

   AsciiRFC [I-D.ribose-asciirfc] and [Metanorma-IETF] describe a
   backend for the [Asciidoctor] tool that converts an AsciiDoc document
   into an xml2rfc v3 document.  The AsciiRFC document states various
   reasons why AsciiDoc is a superior format for the purpose of writing
   standards, so that will not be discussed further.  Note that the same
   team developed Asciidoctor backends [Metanorma] for other Standards
   Developing Organizations (SDO), making it easy to develop computerate
   specifications targeting the documents developed by these SDOs.





Petit-Huguenin            Expires 5 August 2021                 [Page 6]


Internet-Draft           Computerate Specifying            February 2021


   The code in a computerate specification uses the programming language
   [Idris2] in literate programming [Literate] mode using the Bird-
   style, by having each line of code starting with a ">" mark in the
   first column.

   That same symbol is also used by AsciiDoc as an alternate way of
   defining a blockquote [Blockquotes] way which is no longer available
   in a computerate specification.  Bird-style code will simply not
   appear in the rendered document.

   The result of Idris code execution can be inserted inside the
   AsciiDoc part of a specification by inserting that code fragment
   between the "{`" string and the "`}" strings.  That code fragment
   must return a value of a type that implements the "Show" interface.

   A computerate specification is processed by an Asciidoctor
   preprocessor that does the following:

   1.  Loads the whole specification as an Idris program, including
       importing modules.

   2.  For each instance of an inline code fragment, evaluates that
       fragment and replaces it (including the delimiters) by the result
       of that evaluation.

   3.  Continues with the normal processing of the modified
       specification.

   For instance the following document fragment taken from the
   computerate specification of [RFC8489]:





















Petit-Huguenin            Expires 5 August 2021                 [Page 7]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   > rto : Int
   > rto = 500
   >
   > rc : Nat
   > rc = 7
   >
   > rm : Int
   > rm = 16
   >
   > -- A stream of transmission times
   > transmissions : Int -> Int -> Stream Int
   > transmissions value rto = value :: transmissions (value + rto)
   >   (rto * 2)
   >
   > -- A specific transmission time
   > transmission : Int -> Nat -> Int
   > transmission timeout i = index i $ transmissions 0 timeout
   >
   > a1 : Int
   > a1 = rto
   >
   > a2 : String
   > a2 = concat (take (rc - 1) (map (\t => show t ++ " ms, ")
   >   (transmissions 0 rto))) ++ "and " ++ show (transmission rto
   >     (rc - 1)) ++ " ms"
   >
   > a3 : Int
   > a3 = transmission rto (rc - 1) + rto * rm

   For example, assuming an RTO of {`a1`}ms, requests would be sent at
   times {`a2`}.
   If the client has not received a response after {`a3`} ms, the
   client will consider the transaction to have timed out.
   <CODE ENDS>

                                  Figure 1

   is rendered as

   "                                            For example, assuming an
    RTO of 500ms, requests would be sent at times 0 ms, 500 ms, 1500 ms,
    3500 ms, 7500 ms, 15500 ms, and 31500 ms.  If the client has not
    received a response after 39500 ms, the client will consider the
    transaction to have timed out."

                                  Figure 2




Petit-Huguenin            Expires 5 August 2021                 [Page 8]


Internet-Draft           Computerate Specifying            February 2021


   The Idris2 programming language has been chosen because its type
   system supports dependent and linear types [Type-Driven], and that
   type system is the language in which propositions are written.  The
   Idris2 programming also has reflection capabilities and support for
   meta-programming, also known as elaboration.

   Following Zave's second conclusion, computerate specifying is not
   restricted to the specification of protocols, or to property proving.
   There is a whole spectrum of formalism that can be introduced in a
   specification, and we will present it in the remaining sections by
   increasing order of complexity.  Note that because the specification
   language is a programming language, these usages are not exhaustive,
   and plenty of other usages can and will be found after the
   publication of this document.

   At the difference of an RFC which is immutable after publication, the
   types and code in a specification will be improved over time,
   especially as new properties are proved or disproved.  The latter
   will happen when a bug is discovered in a specification and a proof
   of negation is added to the specification, paving the way to a
   revision of the standard.

   A private specification is a specification that is not meant to be
   shared.  There is mostly two reasons for a specification to be kept
   private, as explained in the next sections.

4.1.  Private Specifications for New Documents

   In the simplest case, writing a specification with the goal of
   publishing the resulting document does not require sharing that
   specification.  This is quite similar to what was done with xml2rfc
   before the IETF adopted RFC 7991 as the canonical format for
   Internet-Drafts and RFCs; most people used xml2rfc to prepare their
   document, but did not share the xml2rfc file beyond the co-authors of
   the document.

   In that case writing a specification is straightforward: write the
   specification from scratch using AsciiDoc for the text and Idris for
   the formal parts.

   One effective rule to quickly discover that the Idris code and the
   AsciiDoc document are diverging is to keep both of them as close as
   possible to each other.  This is most effectively done by having the
   matching Idris code right after each AsciiDoc paragraph, such as it
   is then easy to compare each to the other.






Petit-Huguenin            Expires 5 August 2021                 [Page 9]


Internet-Draft           Computerate Specifying            February 2021


   Idris itself imposes an order in which types and code must be
   declared and defined, because it does not by default look for forward
   references.  Because, by the rule above, the text will follow the
   order the Idris code is organized, the document generated by such
   specification tends to be naturally easier to implement, because it
   induces the same workflow than a software implementer will follow
   when implementing the document.

   [RFC8489] and [RFC8656] are examples of standards that are easy to
   implement because are written in the order that a software developer
   will develop each component.

4.2.  Private Specifications for Existing Documents

   A second reason to write a private specification is for the purpose
   of doing a review of an existing document, most likely of an
   Internet-Draft during the standardization process.

   This is done by first turning the existing document into a
   specification by converting it into an AsciiDoc document, which can
   be done manually relatively easily.  After this step, the
   specification can be enriched by adding some Idris code and replacing
   some of the text with the execution of Idris code fragments.
   Comparing the original document with a document generated by
   processing the specification permits to validate that the original
   document is correct regarding the formalism introduced.

   Documents that are not generated from a specification do not always
   have a structure that follow the way a software developer will
   implement it.  When that is the case it will be difficult to add the
   Idris code right after a paragraph describing its functionality,
   because the final code may not type-check because of the lack of
   support for forward references.  It could be a signal that the text
   needs to be reorganized to be more software-development friendly.

   One alternative is to use a technique named self-inclusion, which is
   the possibility to change the order of paragraphs in an AsciiDoc
   document and thus keeping the Idris code in an order that type-
   checks.

   This is done by using tags to delimit the text that needs to be
   moved:









Petit-Huguenin            Expires 5 August 2021                [Page 10]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   // tag::para1[]
   Text that describes a functionality

   > -- Code that implements that functionality.
   // end::para1[]
   <CODE ENDS>

                                  Figure 3

   Then a self-include can move (instead of duplicating) the text inside
   the tags to a different place, without changing the order of the
   Idris code:

   <CODE BEGINS>
   include::Main.adoc[tag=para1]
   <CODE ENDS>

                                  Figure 4

   Note that the IETF Trust licences [TLP5] do not grant permission to
   distribute an annotated Internet-Draft as a whole so redistributing
   such specification would be a copyright license infringement.  But as
   in this case the specification is not meant to be distributed, there
   is no infringement possible.

5.  Self-Contained Specifications

   A self-contained specification is a specification where the Idris
   code does not use anything but the types and functions defined in its
   standard library, thus not requiring to install anything but Idris2
   itself.

   A specification uses Idris types to specify both how stream of bits
   are arranged to form valid Protocol Data Units (PDU) and how the
   exchange of PDUs between network elements is structured to form a
   valid protocol.  In addition a specification can be used to prove or
   disprove a variety of properties for these types.

5.1.  PDU Descriptions

   The PDUs in a communication protocol determines how data is laid out
   before it is sent over a communication link.  Generally a PDU is
   described only in the context of the layer that this particular
   protocol is operating at, e.g. an application protocol PDU only
   describes the data as sent over UDP or TCP, not over Ethernet or Wi-
   Fi.




Petit-Huguenin            Expires 5 August 2021                [Page 11]


Internet-Draft           Computerate Specifying            February 2021


   PDUs can generally be split into two broad categories, binary and
   text, and a protocol PDU mostly falls into one of these two
   categories.

   PDU descriptions can be defined as specifications for at least three
   reasons: the generation of examples that are correct by construction,
   correctness in displaying the result of calculations, and correctness
   in representing the structure of a PDU.  Independently of these
   reasons, a PDU description is a basic component of a specification
   that will probably be needed regardless.

5.1.1.  PDU Examples

   Examples in protocol documents are frequently incorrect, which proves
   to have a significant negative impact as they are too often misused
   as normative text.  See Appendix C for statistics about the frequency
   of incorrect examples in RFC errata.

   Ensuring example correctness is achieved by adding the result of a
   computation (the example) directly inside the document.  If that
   computation is done from a type that is (physically and conceptually)
   close to the normative text, then we gain some level of assurance
   that both the normative text and the derived examples will match.

   Generating an example that is correct by construction always starts
   by defining a type that describes the format of the data to display.
   The Internet Header Format in section 3.1 of [RFC0791] will be used
   in the following sections as example.

   In this section we start by defining an Idris type, using a
   Generalized Algebraic Data Type (GADT).  In that case we have only
   one constructor ("MkInternetHeader") which is defined as a Product
   Type that "concatenate" all the fields on the Internet Header.  One
   specific aspect of Idris types is that we can enrich the definition
   of each field with constraints that then have to be fulfilled when a
   value of that type will be built.















Petit-Huguenin            Expires 5 August 2021                [Page 12]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   data InternetHeader : Type where
     MkInternetHeader :
       (version : Int) -> version = 4 =>
       (ihl : Int) -> ihl >= 5 && ihl < 16 = True =>
       (tos : Int) -> tos >= 0 && tos <= 256 = True =>
       (length : Int) -> length >= (5 * 4) && length < 65536 = True =>
       (id : Int) -> id >= 0 && id < 65536 = True =>
       (flags : Int) -> flags >= 0 && flags < 16 = True =>
       (offset : Int) -> offset >= 0 && offset < 8192 = True =>
       (ttl : Int) -> ttl >= 0 && ttl < 256 = True =>
       (protocol : Int) -> protocol >= 0 && protocol < 256 = True =>
       InternetHeader
   <CODE ENDS>

                                  Figure 5

   where

   version:  This field is constrained to always contain the value 4.

   ihl:  Int is a builtin signed integer so it is constrained to contain
      only positive integers lower than 16.

   others:  Same, all the fields are constrained to unsigned integers
      fitting inside the number of bits defined in [RFC0791].

   An Idris type where the fields in a constructor are organized like
   the "InternetHeader" by ordering them in a sequence is called a Pi
   type - or, when there is no dependencies between fields as there is
   in "version = 4", a Product type.  Although there is no equivalence
   in most programming languages to a Pi type, Product types are known
   as classes in Java and struct in C.

   Another way to organize a type is called the Sum type, which is a
   type with multiple constructors that act as alternative.  Sum types
   can be used in C with a combination of struct and union, and since
   Java 14 by using sealed records.

   Sum types have a dependent counterpart named a Sigma type, which is a
   tuple in which the type of the second element depends on the value of
   the first element.  This is mostly returned by functions, with the
   returned Sigma type carrying both a value and a proof of the validity
   of that value.

   From that point it is possible to define a value that fulfills all
   the constraints.  The following values are taken from example 1 in
   [RFC0791] Appendix A.



Petit-Huguenin            Expires 5 August 2021                [Page 13]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   example1 : InternetHeader
   example1 = MkInternetHeader 4 5 0 21 111 0 0 123 1
   <CODE ENDS>

                                  Figure 6

   The "=>" symbol after a constraint indicates that Idris should try to
   automatically find a proof that this constraint is met by the values
   in the example, which it successfully does in the example above.

   The following example, where the constraints defined in the
   InternetHeader type are not met, will not type-check in Idris (an
   error message will be generated) and thus can not be used to generate
   an example.

   <CODE BEGINS>
   example1' : InternetHeader
   example1' = MkInternetHeader 6 5 0 21 111 0 0 123 1
   <CODE ENDS>

                                  Figure 7

   The next step is to define an Idris function that converts a value of
   the type "InternetHeader" into the kind of bit diagram that is showed
   in Appendix A of [RFC0791].

   <CODE BEGINS>
   Show InternetHeader where
     show (MkInternetHeader version ihl tos length id flags offset
       ttl protocol) = ?showPrec_rhs_1
   <CODE ENDS>

                                  Figure 8

   Here we implement the "Show" interface that permits to define the
   adhoc polymorphic function "show" for "InternetHeader", function that
   will convert the value into the right character string.  Idris names
   starting with a question mark like in "?showPrec_rhs_1" are so-called
   holes, which are placeholder for code to be written, while still
   permitting type-checking.

   After replacing the hole by the actual code, the following embedded
   code can be used in the document to generate an example that is
   correct by construction, at least up to mistakes in the specification
   (i.e. the constraints in "InternetHeader") and bugs in the "show"
   function.




Petit-Huguenin            Expires 5 August 2021                [Page 14]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   ....
   {`example1`}
   ....
   <CODE ENDS>

                                  Figure 9

   will generate the equivalent AsciiDoc text:

   <CODE BEGINS>
   ....
    0                   1                   2                   3
    0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |Ver= 4 |IHL= 5 |Type of Service|        Total Length = 21      |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |      Identification = 111     |Flg=0|   Fragment Offset = 0   |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |   Time = 123  |  Protocol = 1 |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   ....
   <CODE ENDS>

                                 Figure 10

   This generated example is similar to the first of the examples in
   appendix A of RFC 791.

5.1.2.  Calculations from PDU

   The previous section showed how to define a type that precisely
   describes a PDU, how to generates examples that are are values of
   that type, and how to insert them in a document.

   Our specification, which has the form of an Idris type, can be seen
   as a generalization of all the possible examples for that type.  Now
   that we went through the effort of precisely defining that type, it
   would be useful to use it to also calculate statements about that
   syntax.

   In RFC 791 the description of the field IHL states "[...]that the
   minimum value for a correct header is 5."  The origin of this number
   may be a little mysterious, so it is better to use a formula to
   calculate it and insert the result instead.

   Inserting a calculation is easy:




Petit-Huguenin            Expires 5 August 2021                [Page 15]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
    Note that the minimum value for a correct header is
    is \{`sizeHeader `div` ihlUnit`}.

    > sizeHeader : Int
    > sizeHeader = 20

    > ihlUnit : Int
    > ihlUnit = 4
   <CODE ENDS>

                                 Figure 11

   Here we can insert a code fragment that is using a function that is
   defined later in the document because the Idris code is evaluated
   before the document is processed.

   Note the difference with examples: The number "5" is not an example
   of value of the type "InternetHeader", but a property of that type.

   Systematically using the result of calculation on types in a
   specification makes it more resistant to mistakes that are introduced
   as result of modifications.

5.1.3.  PDU Representations

   The layout of a PDU, i.e. the size and order of the fields that
   compose it can be represented in a document in various forms.  One of
   them is just an enumeration of these fields in order, each field
   identified by a name and accompanied by some description of that
   field in the form of the number of bits it occupies in the PDU and
   how to interpret these bits.

   That layout can also be presented as text, as a list, as a table, as
   a bit diagram, at the convenience of the document author.  In all
   cases, some parts of the description of each field can be extracted
   from our Idris type just like we did in Section 5.1.2.

   RFC 791 section 3.1 represents the PDUs defined in it both as bit
   diagrams and as lists of fields.











Petit-Huguenin            Expires 5 August 2021                [Page 16]


Internet-Draft           Computerate Specifying            February 2021


5.2.  State Machines

   A network protocol, which is how the various PDUs defined in a
   document are exchanged between network elements, can always be
   understood as a set of state machines.  At the difference of PDUs,
   that are generally described in a way that is close to their Idris
   counterpart, state machines in a document are generally only
   described as text.

   Note that, just like an Idris representation of a PDU should also
   contain all the possible constraints on that PDU but not more, a
   state machine should contain all the possible constraints in the
   exchange of PDUs, but not less.

   This issue is most visible in one of the two state machines defined
   in RFC 791, the one for fragmenting IP packets (the other is for
   unfragmenting packets).  The text describes two different algorithms
   to fragment a packet but in that case each algorithm should be
   understood as one instance of a more general state machine.  That
   state machine describes all the possible sequences of fragments that
   can be generated by an algorithm that is compliant with RFC 791 and
   it would be an Idris type that is equivalent to the following
   algorithm:

   *  For a specific packet size, generate a list of all the binary
      values {b0,.., bN} with N being the packet size divided by 8 and
      rounded-up, and 0..N representing positional indexes for each of
      the 8 byte chunks of the packet.

   *  For each binary value in that list, generate a list of values that
      represents the number of consecutive bits of the same value (e.g..
      "0x110001011" generates a "[2, 3, 1, 1, 2]" list), each such
      sequence representing a given fragment

   *  Remove from that list of lists any list that contains a number
      that, after multiplication by 8, is higher than the maximum size
      of a fragment.

   *  For each remaining list in that list, generate the list of
      fragments, i.e with the correct offset, length and More bit.

   *  Generate all the possible permutations for each list of fragments.

   We can see that this state machine takes in account the fact that an
   IP packet can not only be fragmented in fragments of various sizes -
   as long as the constraints are respected - but also that these
   fragments can be sent in any order.




Petit-Huguenin            Expires 5 August 2021                [Page 17]


Internet-Draft           Computerate Specifying            February 2021


   Then the algorithms described in the document can be seen as
   generating a subset of all the possible list of fragments that can be
   generated by our state machine.  It is then easy to check that these
   algorithms cannot generate fragments lists that cannot be generated
   by our state machine.

   As a consequence, the unfragment state machine must be able to
   regenerate a valid unfragmented packet for any of the fragments list
   generated by our fragment state machine.  Furthermore, the unfragment
   state machine must also take in account fragment lists that are
   modified by the network (itself defined as a state machine) in the
   following ways:

   *  fragments can be dropped;

   *  the fragments order can change (this is already covered by the
      fact that our fragment state machine generates all possible
      orders);

   *  fragments can be duplicated multiple times;

   *  fragments can be delayed;

   *  fragments can be received that were never sent by the fragment
      state machine.

   Then the algorithm described in the document can be compared with the
   unfragment state machine to verify that all states and transitions
   are covered.

   Defining a state machine in Idris can be done in an ad-hoc way
   [Linear-Resources], particularly by using linear types that express
   resources' consumption.

5.3.  Proofs

   Under the Curry-Howard equivalence, the Idris types that we created
   to describe PDUs and state machine are formal logic propositions, and
   being able to construct values from these types (like we did for the
   examples), is proof that these propositions are true.  These are also
   called internal verifications [Stump16].

   External verifications are made of additional propositions (as Idris
   types) and proofs (as code for these types) with the goal of
   verifying additional properties.






Petit-Huguenin            Expires 5 August 2021                [Page 18]


Internet-Draft           Computerate Specifying            February 2021


   One kind of proofs that one would want in a specification are related
   to isomorphism, i.e. a guarantee that two or more descriptions of a
   PDU or a state machine contain exactly the same information, but
   there is others.

5.3.1.  Wire Type vs Abstract Type

   The Idris types that are used for generating examples, calculations
   or representations are generally very close to the bit structure of
   the PDU.  But some properties may be better expressed by defining
   more abstract types.  We call the former Wire Types, and the latter
   Abstract Types.

   As example, the type in Section 5.1.1 is a wire type, because it
   follows exactly the PDU layout.  But fragmentation can be more easily
   described using the following abstract type:



































Petit-Huguenin            Expires 5 August 2021                [Page 19]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   data InternetHeader' : Type where
     Full : (ihl : Int) -> ihl >= 5 && ihl < 16 = True =>
            (tos : Int) -> tos >= 0 && tos <= 256 = True =>
            (length : Int) -> length >= (5 * 4) &&
              length < 65536 = True =>
            (ttl : Int) -> ttl >= 0 && ttl < 256 = True =>
            (protocol : Int) -> protocol >= 0 &&
              protocol < 256 = True =>
            InternetHeader'
     First : (ihl : Int) -> ihl >= 5 && ihl < 16 = True =>
             (tos : Int) -> tos >= 0 && tos <= 256 = True =>
             (length : Int) -> length >= (5 * 4) &&
               length < 65536 = True =>
             (id : Int) -> id >= 0 && id < 65536 = True =>
             (ttl : Int) -> ttl >= 0 && ttl < 256 = True =>
             (protocol : Int) -> protocol >= 0 &&
               protocol < 256 = True =>
             InternetHeader'
     Next : (ihl : Int) -> ihl >= 5 && ihl < 16 = True =>
            (tos : Int) -> tos >= 0 && tos <= 256 = True =>
            (length : Int) -> length >= (5 * 4) &&
              length < 65536 = True =>
            (offset : Int) -> length > 0 &&
              length < 8192 = True =>
            (id : Int) -> id >= 0 && id < 65536 = True =>
            (ttl : Int) -> ttl >= 0 && ttl < 256 = True =>
            (protocol : Int) -> protocol >= 0 &&
              protocol < 256 = True =>
            InternetHeader'
     Last : (ihl : Int) -> ihl >= 5 && ihl < 16 = True =>
            (tos : Int) -> tos >= 0 && tos <= 256 = True =>
            (length : Int) -> length >= (5 * 4) &&
              length < 65536 = True =>
            (offset : Int) -> length > 0 &&
              length < 8192 = True =>
            (id : Int) -> id >= 0 && id < 65536 = True =>
            (ttl : Int) -> ttl >= 0 && ttl < 256 = True =>
            (protocol : Int) -> protocol >= 0 &&
              protocol < 256 = True =>
            InternetHeader'
   <CODE ENDS>

                                 Figure 12

   First the "version" field is eliminated, because it always contains
   the same constant.




Petit-Huguenin            Expires 5 August 2021                [Page 20]


Internet-Draft           Computerate Specifying            February 2021


   Then the "flags" and "offset" fields are reorganized so to provide
   four different alternate packets:

   *  The "Full" constructor represents an unfragmented packet.  It is
      isomorphic to a "MkInternetHeader" with a "flags" and "offset"
      values of 0.

   *  The 'First' constructor represents the first fragment of a packet.
      It is isomorphic to a "MkInternetHeader" with a "flags" value of 1
      and "offset" value of 0.

   *  The 'Next' constructor represents a intermediate fragments of a
      packet.  It is isomorphic to a "MkInternetHeader" with a "flags"
      value of 1 and "offset" value different than 0.

   *  Finally the 'Last' constructor represents the last fragment of a
      packet.  It is isomorphic to a "MkInternetHeader" with a "flags"
      value of 0 and "offset" value different than 0.

   One of the main issue of having two types for the same data is
   ensuring that they both contains the same information, i.e. that they
   are isomorphic.  To ensure that these two types are carrying the same
   information we need to define and implement four functions that, all
   together, prove that the types are isomorphic.  This is done by
   defining the 4 types below, as propositions to be proven:

   <CODE BEGINS>
   total
   to : InternetHeader -> InternetHeader'

   total
   from : InternetHeader' -> InternetHeader

   total
   toFrom : (x : InternetHeader') -> to (from x) = x

   total
   fromTo : (x : InternetHeader) -> from (to x) = x
   <CODE ENDS>

                                 Figure 13

   Successfully implementing these functions will prove that the two
   types are isomorphic.  Note the usage of the "total" keyword to
   ensure that these are proofs and not mere programs.






Petit-Huguenin            Expires 5 August 2021                [Page 21]


Internet-Draft           Computerate Specifying            February 2021


5.3.2.  Data Format Conversion

   For documents that describe a conversion between different data
   layouts, having a proof that guarantees that no information is lost
   in the process can be beneficial.  For instance, we observe that
   syntax encoding tends to be replaced each ten years or so by
   something "better".  Here again isomorphism can tell us exactly what
   kind of information we lost and gained during that replacement.

   Here, for example, the definition of a function that would verify an
   isomorphism between an XML format and a JSON format:

   <CODE BEGINS>
   isXmlAndJsonSame: Iso (XML, DeltaXML) (JSON, DeltaJson)
     ...
   <CODE ENDS>

                                 Figure 14

   DeltaXML expresses what is gained by switching from XML to JSON, and
   DeltaJson expresses what is lost.

5.3.3.  Postel's Law

   |  Be conservative in what you do, be liberal in what you accept from
   |  others.
   |
   |  -- Jon Postel - RFC 761

   One of the downsides of having specifications is that there is no
   wiggle room possible when implementing them.  An implementation
   either conforms to the specification or does not.

   One analogy would be specifying a pair of gears.  If one decides to
   have both of them made with tolerances that are too small, then it is
   very likely that they will not be able to move when put together.  A
   bit of slack is needed to get the gear smoothly working together but
   more importantly the cost of making these gears is directly
   proportional to their tolerance.  There is an inflexion point where
   the cost of an high precision gear outweighs its purpose.

   We have a similar issue when implementing a specification, where
   having an absolutely conform implementation may cost more money than
   it is worth spending.  On the other hand a specification exists for
   the purpose of interoperability, so we need some guidelines on what
   to ignore in a specification to make it cost effective.





Petit-Huguenin            Expires 5 August 2021                [Page 22]


Internet-Draft           Computerate Specifying            February 2021


   Postel's law proposes an informal way of defining that wiggle room by
   actually having two different specifications, one that defines a data
   layout for the purpose of sending it, and another one that defines a
   data layout for the purpose of receiving that data layout.

   Existing documents express that dichotomy in the form of the usage of
   SHOULD/SHOULD NOT/RECOMMENDED/NOT RECOMMENDED [RFC2119] keywords.
   For example the SDP spec says that "[t]he sequence CRLF (0x0d0a) is
   used to end a line, although parsers SHOULD be tolerant and also
   accept lines terminated with a single newline character."  This
   directly infers two specifications, one used to define an SDP when
   sending it, that enforces using only CRLF, and a second
   specification, used to define an SDP when receiving it (or parsing
   it), that accepts both CRLF and LF.

   Note that the converse is not necessarily true, i.e. not all usages
   of these keywords are related to Postel's Law.

   To ensure that the differences between the sending specification and
   the receiving specification do not create interoperability problems,
   we can use a variant of isomorphism, as shown in the following
   example (data constructors and code elided):

   <CODE BEGINS>
   data Sending : Type where

   data Receiving : Type where

   to : Sending -> List Receiving

   from : Receiving -> Sending

   toFrom : (y : Receiving) -> Elem y (to (from y))

   fromTo : (y : Sending) -> True = all (== y) [from x | x <- to y]
   <CODE ENDS>

                                 Figure 15

   Here we define two data types, one that describes the data layout
   that is permitted to be sent ("Sending") and one that describes the
   data layout that is permitted to be received ("Receiving").  For each
   data layout that is possible to send, there is one or more matching
   receiving data layouts.  This is expressed by the function "to" that
   takes as input one Sending value and returns a list of Receiving
   values.





Petit-Huguenin            Expires 5 August 2021                [Page 23]


Internet-Draft           Computerate Specifying            February 2021


   Conversely, the "from" function maps a Receiving data layout onto a
   Sending data layout.  Note the asymmetry there, which prevents using
   a standard proof of isomorphism.

   Then the "toFrom" and "fromTo" proofs verify that there is no
   interoperability issue by guaranteeing that each Receiving value maps
   to one and only one Sending instance and that this mapping is
   isomorphic.

   All of this will provide a clear guidance of when and where to use a
   SHOULD keyword or its variants, without loss of interoperability.

   As an trivial example, the following proves that accepting LF
   characters in addition to CRLF characters as end of line markers does
   not break interoperability:

   <CODE BEGINS>
   data Sending : Type where
     S_CRLF : Sending

   Eq Sending where
     (==) S_CRLF S_CRLF = True

   data Receiving : Type where
     R_CRLF : Receiving
     R_LF : Receiving

   to : Sending -> List Receiving
   to S_CRLF = [R_CRLF, R_LF]

   from : Receiving -> Sending
   from R_CRLF = S_CRLF
   from R_LF = S_CRLF

   toFrom : (y : Receiving) -> Elem y (to (from y))
   toFrom R_CRLF = Here
   toFrom R_LF = There Here

   fromTo : (y : Sending) -> True = all (== y) [from x | x <- to y]
   fromTo S_CRLF = Refl
   <CODE ENDS>

                                 Figure 16








Petit-Huguenin            Expires 5 August 2021                [Page 24]


Internet-Draft           Computerate Specifying            February 2021


   Postel's Law is not limited to the interpretation of PDUs as a state
   machine on the receiving side can also be designed to accept more
   than than what a sending state machine can produce.  A similar
   isomorphism proof can be used to ensure that this is done without
   loss of interoperability.

5.3.4.  Implementability

   When applied, the techniques described in Section 5.1 and Section 5.2
   result in a set of types that represents the whole protocol.  These
   types can be assembled together, using another set of types, to
   represent a simulation of that protocol that covers all sending and
   receiving processes.

   The types can then be implemented, and that implementation acts as a
   proof that this protocol is actually implementable.

   To make these pieces of code composable, a specification is split in
   multiple modules, each one represented as a unique function.  The
   type of each of these functions is derived from the state machines
   described in Section 5.2, by bundling together all the inputs of the
   state machine as the input for that function, and bundling all the
   outputs of the state machine as the output of this function.

   For instance the IP layer is really 4 different functions:

   *  A function that converts between a byte array and a tree
      representation (parsing).

   *  A function that takes a tree representation and a maximum MTU and
      returns a list of tree representations, each one fitting inside
      the MTU.

   *  A function that accumulates tree representations of an IP fragment
      until a tree representation of a full IP packet can be returned.

   *  A function that convert a tree representation into a byte array.

   The description of each function is incomplete, as in addition to the
   input and the output listed, these functions needs some ancillary
   data, in the form of:

   *  state, which is basically values stored between evaluations of a
      function,







Petit-Huguenin            Expires 5 August 2021                [Page 25]


Internet-Draft           Computerate Specifying            February 2021


   *  an optional signal, that can be used as an API request or
      response.  As timers are a fundamental building block for
      communication protocols, one common uses for that signal are to
      request the arming of a timer, and to receive the indication of
      the expiration of that timer.

5.3.5.  Termination

   Proving that a protocol does not loop is equivalent to proving that a
   implementation of the types for that protocol does not loop either
   i.e., terminates.  This is done by using the type described in
   Section 5.3.4 and making sure that it type-check when the "total"
   keyword is used.

5.3.6.  Liveness

   A protocol may never terminate - in fact most of the time the server
   side of a protocol is a loop - but it still can do some useful work
   in that loop.  This property is called liveness.

6.  Importing Specifications

      |  NOTE: The code for the libraries described in that section is
      |  not yet ready to be published.

   One of the ultimate goals of this document is to convince authors to
   use the techniques described there to write their documents.  Because
   doing so requires a lot of efforts, an important intermediate goal is
   to show authors that the benefits of Computerate Specifying are worth
   learning and becoming proficient in these techniques.

   The best way to reach that intermediate goal is to apply these
   technique to documents that are in the process of being published by
   the IETF and if issues are found, report them to the authors.  Doing
   that on published RFCs, especially just after their publication,
   would be unnecessarily mean.  On the other hand doing that on all
   Internet-Drafts as they are published would not be scalable.

   The best place to do a Computerate Specifying oriented review is when
   a document enters IETF Last Call.  These reviews would then be
   indistinguishable from the reviews done by an hypothetical Formal
   Specification Directorate.  An argument can be made that, ultimately,
   writing a specification for a document could be an activity too
   specialized, just like Security reviews are, and that an actual
   Directorate should be assembled.






Petit-Huguenin            Expires 5 August 2021                [Page 26]


Internet-Draft           Computerate Specifying            February 2021


   Alas, it is clear that writing a specification from scratch (as in
   Section 5) for an existing document takes far more time than the Last
   Call duration would allow.  On the other hand the work needed could
   be greatly reduced if, instead of writing that specification from
   scratch, libraries of code would be available for the parts that are
   reusable between successive specifications.  These libraries fall
   into 3 categories:

   *  General types and common presentations.  E.g., bit diagrams are a
      very common way of presenting data, and so reusable types and
      functions to generate and compare them would accelerate a
      formalization.  The libraries in that category are explained in
      Section 6.1, in Section 8.1, and its associated reference in
      Appendix B.

   *  Types and common representations for meta-languages.  A few meta-
      languages are used in documents to formalize some parts of them,
      so having libraries to formalize these meta-languages also helps
      accelerating their verification.  The libraries in that category
      are explained in Section 6.2, in Section 8.2, and its associated
      reference in Appendix B.

   *  Types and common representation for common protocols.  Most
      documents are about modifying or defined new usages for existing
      protocols, which is why it makes sense to establish libraries of
      these existing protocols for reuse.  The libraries in that
      category are explained in Section 6.3, in Section 8.3, and its
      associated reference in Appendix B.

   Together these libraries form the Computerate Specifying Standard
   Library (Section 8).

   These libraries are in fact computerate specifications that, instead
   of being private, are designed to export types and code and be
   imported in other computerate specifications.  Section 7 describes
   how to build an specification that can be exported.

   The types and code in a computerate specification form an Idris
   package, which is a collection of Idris modules.  An Idris module
   form a namespace hierarchy for the types and functions defined in it
   and is physically stored as a file.

   Different types of specification can be combined, for instance an
   exporting library may import from another specification, and this
   recursively until importing specifications that are both self-
   contained and exporting.





Petit-Huguenin            Expires 5 August 2021                [Page 27]


Internet-Draft           Computerate Specifying            February 2021


   For convenience each public computerate specification, including the
   one behind this document, is available as an individual git
   repository.  There is exactly one Idris package per git repository.
   Appendix A.5 explains how to gain access to these computerate
   specifications.

6.1.  Common Modules

   This document is itself generated from a computerate specification
   that contains data types and functions that can be reused in future
   specifications, and as a whole is part of the standard library for
   computerate specifying.  The following sections describes the Idris
   modules defined in that specification.

6.1.1.  Generating AsciiDoc

   The code described in Section 5 directly generates text that is to be
   embedded inside an AsciiDoc document.  This is fine for small
   examples but AsciiDoc has quite a lot of escaping rules that are
   difficult to use in a consistent manner.

   For this reason the specification behind this document provides a
   module named "AsciiDoc" that contains a set of types that can be used
   to guarantee that the AsciiDoc text generated is compliant with its
   specification.  All these types implement the "Show" interface so
   they can be directly returned by the embedded code.

   So instead of implementing a show function, a function returning an
   instance of one of the types can be executed directly as embedded
   code:

   <CODE BEGINS>
   > example : InternetHeader -> Block
   > example ih = ?example_rhs

   {`example example1`}
   <CODE ENDS>

                                 Figure 17

   In the example above, the "example" function converts an
   "InternetHeader" value into an "AsciiDoc" block, which is
   automatically serialized as AsciiDoc text.

   The "AsciiDoc" module is not limited to generating examples, but can
   be used to generate any AsciiDoc structure from Idris code.  E.g.,
   the tables in Appendix C are generated using that technique.




Petit-Huguenin            Expires 5 August 2021                [Page 28]


Internet-Draft           Computerate Specifying            February 2021


   Section 8.1.1 provides a description of the "AsciiDoc" module.

      |  NOTE: Similarly the RFC Editor has rules on how to present
      |  source code and examples in a document, particularly about how
      |  lines longer than 72 characters should be folded.  A module
      |  similar to the "AsciiDoc" module will be developed to apply
      |  these rules transparently.

   Using an intermediary type will also permit to correctly generate
   AsciiDoc that can generate an xmlrfc 3 file that supports both text
   and graphical versions of a figure.  This will be done by having
   AsciiDoc blocks converted into <artwork> elements that contains both
   the 72 column formatted text and an equivalent SVG file, even for
   code source (instead of using the <sourcecode> element).

6.1.2.  Common Data Types

   The type in Section 5.1.1 seems a good representation of the
   structure of the Internet Header, but the origin of a lot of the
   values in the constraints does not seems very obvious, and as such
   are still prone to errors.  E.g., the calculation in Section 5.1.2
   could be better if it was using the type itself as a source for the
   calculated data.

   It also may be more convenient to use types that already have some of
   the properties we need, instead of having to add a bunch of
   constraints to the "Int" type.

   The truth of the matter is that the Idris standard library contains
   very few predefined types that are useful to specify the syntax of
   communication protocols.  E.g., none of the builtin types ("Int",
   "Integer", "Double", "Char", "String", etc) are really suitable to
   describe a PDU syntax, and so should be avoided.  For this reason, it
   is preferable to use the types provided by the Computerate Specifying
   standard library.

   We are going to redefine the "InternetHeader" type, but using three
   modules from the standard library:

   BitVector:  A sequence of bits, or bit-vector, is the most primitive
      type with which a packet can be described.  This module provides a
      type "BitVector n" that represents a sequence of bit of fixed size
      "n".  The module also provides a set of functions that permits to
      manipulate bit-vectors.  See Section 8.1.2 for a description of
      the "BitVector" module.

   Unsigned:  The "Unsigned" module provides a type "Unsigned n" that is




Petit-Huguenin            Expires 5 August 2021                [Page 29]


Internet-Draft           Computerate Specifying            February 2021


      built on top of the "BitVector" module.  In addition of the
      properties of a bit-vector, an "Unsigned n" is considered a number
      and so all the integer operations applies to it.  See
      Section 8.1.3 for a description of the "Unsigned" module.

   Dimension:  Some numbers (also called denominate numbers) are used in
      conjunction with a so-called unit of measure.  The "Dimension"
      module provides a way to associate a dimension, in the form of a
      unit of measure, to an Idris number, including to the numbers
      defined in the "Unsigned" module.  The "Dimension" module provides
      two dimensions, Data (with bit, octet, etc, as units of
      information) and Time (with second, millisecond, etc, as unit of
      time).  See Section 8.1.4 for a description of the "Dimension"
      module.

   A redefinition of the type in Section 5.1.1 using the types in these
   modules would look like this:

   <CODE BEGINS>
   data InternetHeader : Type where
     MkInternetHeader :
       (version : BitVector 4) -> version = [O, I, O, O] =>
       (ihl : (Unsigned 4, Data)) -> snd ihl = tetra =>
       (tos : BitVector 8) ->
       (length : (Unsigned 16, Data)) -> snd length = byte =>
       (id : Unsigned 16) ->
       (flags : BitVector 3) ->
       (offset : Unsigned 13, Data)) -> snd offset = octa =>
       (ttl : (Unsigned 8, Time)) -> snd ttl = second =>
       (protocol : BitVector 16) ->
       (checksum : BitVector 16) ->
       (source : BitVector 32) ->
       (dest : BitVector 32) ->
       (options : List Option) ->
       (padding : BitVector n) ->
       InternetHeader
   <CODE ENDS>

                                 Figure 18

   version:  This is bit-vector, but it always contains the same value,
      so a constraint states that.  Because bit-vectors are not
      integers, the value must be expressed by a list of "O" (for 0) and
      "I" (for 1) constructors.

   ihl:  This is an unsigned integer with a size of 4 bits.  It is





Petit-Huguenin            Expires 5 August 2021                [Page 30]


Internet-Draft           Computerate Specifying            February 2021


      associated with a dimension, here the "Data" dimension, which is
      constrained to use the "tetra" unit (32-bit words).  Basically a
      denominate number can only be added or subtracted with numbers
      with the same dimension (but not necessarily with the same unit).
      E.g. adding the "ihl" value with the "ttl" value will be rejected
      by Idris, because that operation does not make sense.  A
      denominate number can also be divided or multiplied by a
      dimensionless number.

   tos, flags, protocol, source, dest:  These are defined as bit-
      vectors, because they are not really numbers - they do not need to
      be compared, or be part of a calculation.  The number in this type
      (and all the others) is the number of bits allocated.

   length:  This is an unsigned number with a size of 16 bits, a "Data"
      dimension and a "byte" unit (8 bits).  After casting as denominate
      numbers, subtracting "ihl" from "length" gives directly the size
      of the payload, without risk of scaling error.

   id:  This is an unsigned integer.  Comparisons and calculations are
      possible on this field.

   offset:  This is an unsigned number with a length of 13 bits, a
      "Data" dimension and an "octa" unit (64 bits).  Again, adding or
      subtracting this value after casting to another of the same
      dimension is guaranteed to return the correct value.

   ttl:  This is a denominate number with "Time" as dimension and
      "second" as unit.

   options:  This is a variable length field that contains a list of
      options, which are defined in a separate type named "Option".

   padding:  This is a bit-vector whose length is variable.

   The "byte", "wyde", "octa", and "tetra" units are precisely defined
   in [TAOCP].

   As we can see the noise in the definition of our type is greatly
   reduced by using these specialized types, which in turn permits to
   add even more constraints.










Petit-Huguenin            Expires 5 August 2021                [Page 31]


Internet-Draft           Computerate Specifying            February 2021


   We can even constrain the size of a field, like is done for the
   "padding" field below.  In that case the length is calculated in the
   first constraint by calling the "pad" function, function that
   calculates the number of bits needed to pad a value of a type that
   implements the "Size" interface to a word boundary, here 32 bits.
   The second constraint checks that whatever the length of the padding
   field is, it is always equal to a zero-filled bit-vector, as returned
   by the function "bitVector".

   <CODE BEGINS>
   data InternetHeader : Type where
     MkInternetHeader :
       (version : BitVector 4) -> version = [O, I, O, O] =>
       (ihl : (Unsigned 4, Data)) -> snd ihl = tetra =>
       (tos : Tos) ->
       (length : (Unsigned 16, Data)) -> snd length = octet =>
       (id : Unsigned 16) ->
       (flags : Flags) ->
       (offset : Unsigned 13, Data)) -> snd offset = octa =>
       (ttl : (Unsigned 8, Time)) -> snd ttl = second =>
       (protocol : BitVector 16) ->
       (checksum : BitVector 16) ->
       (source : BitVector 32) ->
       (dest : BitVector 32) ->
       (options : List Option) ->
       (padding : BitVector n) ->
         n = pad 32 options => padding = bitVector =>
       InternetHeader
   <CODE ENDS>

                                 Figure 19

   Dimensions can also be combined to seamlessly build more complex
   dimensions.  For example, all "length" values of sent packets can be
   added up during a period of time, while keeping beginning and ending
   times as denominate numbers: dividing the "length" sum by the
   difference between the end time and the begin time gives us directly
   the data speed in bits per second (or whatever unit we prefer), with
   the guarantee that Idris will not let us mix oranges and apples.

   Here's an example of Sum type that implements some of the variants
   for an "Option" in an "InternetHeader":









Petit-Huguenin            Expires 5 August 2021                [Page 32]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   data Option : Type where
     Eoo : (flag : BitVector 1) -> flag = [O] =>
           (class : BitVector 2) -> class = [O, O] =>
           (number : BitVector 5) -> number = [O, O, O, O, O] =>
           Option
     Noop : (flag : BitVector 1) -> flag = [O] =>
            (class : BitVector 2) -> class = [O, O] =>
            (number : BitVector 5) -> number = [O, O, O, I, O] =>
            Option
     Security : (flag : BitVector 1) -> flag = [I] =>
                (class : BitVector 2) -> class = [O, O] =>
                (number : BitVector 5) -> number = [O, O, O, I, O] =>
                (length : Unsigned 8) -> length = 11 =>
                (s : BitVector 16) ->
                (c : BitVector 16) ->
                (h : BitVector 16) ->
                (tcc : BitVector 24) ->
                Option
     Lssr : (flag : BitVector 1) -> flag = [I] =>
            (class : BitVector 2) -> class = [O, O] =>
            (number : BitVector 5) -> number = [O, O, O, I, I] =>
            (length : Unsigned 8) ->
            (pointer : Unsigned 8) -> pointer >= 4 = True =>
            Option
   <CODE ENDS>

                                 Figure 20

6.1.3.  Calculations

   The imported types that we are using in the definition of our types
   all implement the "Size" interface, which provides a definition for
   the adhoc polymorphic function "size", function that returns the size
   of a field as a dimensional number of dimension "Data".  This
   interface can be implemented for the type "InternetHeader" by making
   its size the sum of the size of all its fields:

   <CODE BEGINS>
   Show InternetHeader where
     size (MkInternetHeader version ihl tos length id flags offset ttl
       protocol checksum source dest options padding) = size version +
         size ihl +
         ...
         size padding
   <CODE ENDS>

                                 Figure 21



Petit-Huguenin            Expires 5 August 2021                [Page 33]


Internet-Draft           Computerate Specifying            February 2021


   We can then define a minimal header, and insert its size, using the
   right unit, in the document:

   <CODE BEGINS>
   > minHeader : Data
   > minHeader = size $ MkInternetHeader [O, I, O, O]
   >   (5, tetra)
   >   (MkTos 0 [O] [O] [O] [O, O])
   >   (1000, wyde)
   >   0
   >   (MkFlags bitVector bitVector bitVector)
   >   (0, octa)
   >   (64, second)
   >   bitVector
   >   bitVector
   >   (A [O] bitVector bitVector)
   >   (A [O] bitVector bitVector)
   >   []
   >   []

   Note that the minimum value for a correct header is
   {`fromDenominate (size ih) tetra`}
   <CODE ENDS>

                                 Figure 22

6.1.4.  Typed Petri Nets

   A better solution than defining an adhoc type for our state machines,
   as explained in Section 5.2, is to use Petri Nets.  This
   specification defines a DSL that permits describing a Typed Petri Net
   (TPN) which is heavily influenced by Coloured Petri Nets [CPN] (CPN).
   The original CPN adds some restriction on the types that can be used
   in a Petri Net because of limitations in the underlying programming
   language, SML.  As the underlying programming used in TPN, Idris,
   does not have these limitations, any well-formed Idris type
   (including polymorphic, linear and dependent types) can be directly
   used in TPN.

   Here's an example of TPN from figure 2.10 in [CPN]:











Petit-Huguenin            Expires 5 August 2021                [Page 34]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   NO : Type
   NO = Int

   DATA : Type
   DATA = String

   NOxDATA : Type
   NOxDATA = (NO, DATA)

   PTS : Place
   PTS = MkPlace "Packets To Send" NOxDATA (\() => [(1, "COL"),
     (2, "OUR"), (3, "ED "), (4, "PET"), (5, "RI "), (6, "NET")])

   NS : Place
   NS = MkPlace "NextSend" NO (\() => [1])

   A : Place
   A = MkPlace "A" NOxDATA (\() => [])

   input1 : Input
   input1 = MkInput PTS (NO, DATA) pure

   input2 : Input
   input2 = MkInput NS NO pure

   output1 : Output
   output1 = MkOutput PTS (NO, DATA) pure

   output2 : Output
   output2 = MkOutput NS NO pure

   output3 : Output
   output3 = MkOutput A (NO, DATA) pure

   sendPacket : Transition
   sendPacket = MkTransition [input1, input2] [output1, output2,
     output3] (\((n, d), n') => if n == n'
                                then pure ((n, d), n, (n, d))
                                else empty)
   <CODE ENDS>

                                 Figure 23

      |  NOTE: The DSL is being currently designed, so the example shows
      |  the generated values.





Petit-Huguenin            Expires 5 August 2021                [Page 35]


Internet-Draft           Computerate Specifying            February 2021


   From there it is easy to generate (using the non-deterministic monad
   in Idris) an interpreter for debugging and simulation purposes:

   <CODE BEGINS>
   interpret : MS NOxDATA -> MS NO -> MS NOxDATA ->
     ND (MS NOxDATA, MS NO, MS NOxDATA)
   interpret pts ns a = do
     (pts1, pts2) <- sel pts
     (ns1, ns2) <- sel ns
     i1 <- input input1 pts1
     i2 <- input input2 ns1
     (pts3, ns3, a3) <- transition sendPacket (i1, i2)
     let o1 = output output1 pts3
     let o2 = output output2 ns3
     let o3 = output output3 a3
     pure (o1 ++ pts2, o2 ++ ns2, o3 ++ a)
   <CODE ENDS>

                                 Figure 24

   A Petri Net has the advantage that the same graph can be reused to
   derive other Petri Nets, e.g., Timed Petri Nets (that can be used to
   collect performance metrics) or Stochastic Petri Nets.

   A TPN that covers a whole protocol (i.e. client, network, and server)
   is useful to prove the properties listed in Section 5.3.4,
   Section 5.3.5, and Section 5.3.6.  But the TPN is also designed in a
   way that each of these parts can be defined separately from the
   others, making it a Hierarchical TPN.

6.1.5.  Representations

   Another usage of our Idris type would be to generate a textual
   representation of that type.

   Figure 4 in RFC 791 is a good example of a representation of a data
   layout, here as a bit diagram.  Because we already have an Idris type
   which is describing exactly the same thing, the idea of syntax
   representation is to convert that type into text, and insert it in
   place of the bit diagram.

   For each textual representation of a type, it is possible to write a
   function that takes as parameter this type and generate an "AsciiDoc"
   value that can then be inserted in the document.







Petit-Huguenin            Expires 5 August 2021                [Page 36]


Internet-Draft           Computerate Specifying            February 2021


   Some document uses representations that are unique to this document
   but often multiple documents share the same representation and so
   that function can be also shared between them.  A set of such
   functions is available as part of the Computerate Specification
   standard library,

6.1.5.1.  Bit Diagrams

   The bit diagram is one of the most frequently used representation of
   a PDU specification in documents, so a function to convert an Idris
   type into a bit diagram is provided as part of the standard library.

   That function takes as parameters an Idris type, a structure
   containing additional informations, and returns an "AsciiDoc" value
   that can be inserted in the document.

   The additional structure is a list of the properties associated to
   each field that are needed to generate the bit diagram.  For a bit
   diagram the only property is a character string containing the name
   of the field.

   For our "InternetHeader" type, that additional structure would look
   like this:

   <CODE BEGINS>
   names : Pdu
   names = MkPdu `{{MkInternetHeader}} [
     MkField "Version",
     MkField "IHL",
     MKField "Type of Service",
     MkField "Total Length",
     MkField "Identification",
     MkField "Flags",
     MkField "Fragment Offset",
     MkField "Time to Live",
     MkField "Protocol"]
   <CODE ENDS>

                                 Figure 25

   The Pdu type takes care of verifying that each name is unique in the
   structure, and that each name length does not exceed "2 * (size
   field) - 1", so it is guaranteed to fit in the bit diagram cell.

   After that it is just a matter of inserting the function call in the
   document (the "%runElab" keyword indicates that the Idris code is
   using reflection elaboration, which is used to inspect a type).




Petit-Huguenin            Expires 5 August 2021                [Page 37]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   {`%runElab toBitDiagram names`}
   <CODE ENDS>

                                 Figure 26

6.1.5.2.  Message Sequence Charts

   Message Sequence Charts are a common way to represent an example of
   execution of a Petri Net, i.e. of the interactions between the
   underlying state machines.  Although sequence charts are often
   implicitly used to describe a protocol, that description can only be
   partial.

   Nonetheless, this is a very common way to show state machine related
   examples in a document, so a library will permit to specify an
   execution in a Petri Net (i.e. a list of Transitions and their
   Bindings), and convert it into a message sequence chart that can be
   inserted into the document.  Optionally the message sequence chart
   generated can be followed by an ordered list of the messages
   themselves.

6.2.  Packages for Meta-Languages

   When different representations of a specification share some common
   characteristics, it is usual to generalize them into a formal
   language.

   One shared limitation of these languages is that they cannot always
   formalize all the constraints of a specific data layout, so they have
   to be enriched with comments.  One consequence of this is that they
   cannot be used as a replacement for the Idris types described in
   Section 5.1.1 or Section 6.1.2, types that are purposely designed to
   be as complete as possible.

   Another consequence is the proliferation of these languages, with
   each new formal language trying to integrate more constraints than
   the previous ones.  For that reason Computerate Specifying does not
   favor one formal language over the others, and will try to provide
   code to help use all of them.

   Similarly to what was explained in Section 5.1 a set of types can be
   designed and then used to type-check instance of that formal
   language, and convert them into a textual representation.  Most of
   the formal languages used at the IETF already come with a set of
   tools that permits to verify that the text representation in an RFC
   is syntactically correct, so that type does not add much to that.




Petit-Huguenin            Expires 5 August 2021                [Page 38]


Internet-Draft           Computerate Specifying            February 2021


   On the other hand that type can be the target of a converter from an
   ad-hoc type.  This will ensure that the generated instance of the
   formal language matches the specification, which is something that
   external tools cannot do.

   When a PDU is described with a formal language, we end up with two
   descriptions, one using the Idris dependent type (and used to
   generate examples) and the other using the formal language.

   Proving isomorphism requires generating an Idris type from the formal
   language instance, which is done using an Idris elaborator script.

   In Idris, Elaborator Reflection [Elab] is a metaprogramming facility
   that permits writing code generating type declarations and code
   (including proofs) automatically.

   For instance the ABNF language is itself defined using ABNF, so after
   converting that ABNF into an instance of the Syntax type (which is an
   holder for a list of instances of the Rule type), it is possible to
   generate a suite of types that represents the same language:

   <CODE BEGINS>
   > abnf : Syntax
   > abnf = MkSyntax [
   >   "rulelist" `Eq` (Repeat (Just 1) Nothing (Group (Altern
   >     (TermName "rule") (Group (Concat (Repeat Nothing Nothing
   >     (TermName "c-wsp")) (TermName "c-nl") [])) []))),
   >     ...
   >   ]
   >
   > %runElab (generateType "Abnf" abnf)
   <CODE ENDS>

                                 Figure 27

   The result of the elaboration can then be used to construct a value
   of type Iso, which requires four total functions, two for the
   conversion between types, and another two to prove that sequencing
   the conversions results in the same original value.

   The following example generates an Idris type "SessionDescription"
   from the SDP ABNF.  It then proves that this type and the Sdp type
   contain exactly the same information (the proofs themselves have been
   removed, leaving only the propositions):







Petit-Huguenin            Expires 5 August 2021                [Page 39]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   import Data.Control.Isomorphism

   sdp : Syntax
   sdp = MkSyntax [
     "session-description" `Eq` (Concat (TermName "version-field")
       (TermName "origin-field") [
         TermName "session-name-field",
         Optional (TermName "information-field"),
         Optional (TermName "uri-field"),
         Repeat Nothing Nothing (TermName "email-field"),
         Repeat Nothing Nothing (TermName "phone-field"),
         Optional (TermName "connection-field"),
         Repeat Nothing Nothing (TermName "bandwidth-field"),
         Repeat (Just 1) Nothing (TermName "time-description"),
         Optional (TermName "key-field"),
         Repeat Nothing Nothing (TermName "attribute-field"),
         Repeat Nothing Nothing (TermName "media-description")
         ]),
     ...
     ]

   %runElab (generateType "Sdp" sdp)

   same : Iso Sdp SessionDescription
   same = MkIso to from toFrom fromTo
     where
       to : Sdp -> SessionDescription

       from : SessionDescription -> Abnf

       toFrom : (x : SessionDescription ) -> to (from x) = x

       fromTo : (x : Sdp) -> from (to x) = x
   <CODE ENDS>

                                 Figure 28

   As stated in Section 5.3.1, the Idris type and the type generated
   from the formal language are not always isomorphic, because some
   constraints cannot be expressed in that formal language.  In that
   case isomorphism can be used to precisely define what is missing
   information in the formal language type.  To do so, the generated
   type is augmented with a delta type, like so:







Petit-Huguenin            Expires 5 August 2021                [Page 40]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   data DeltaSessionDescription : Type where
     ...

   same : Iso Sdp (SessionDescription, DeltaSessionDescription)
     ...
   <CODE ENDS>

                                 Figure 29

   Then the DeltaSessionDescription type can be modified to include the
   missing information until the same function type checks.  After this
   we have a guarantee that we know all about the constraints that
   cannot be encoded in that formal language, and can check manually
   that each of them are described as comments.

   An interesting comment in [Momot16] states that if the input of an
   application is too complex to be expressed in ABNF without adding
   comments, it is too complex to be safe.  The technique described in
   this section can be used to evaluate the safety of such ABNF by
   clearly specifying the impact of these additional comments.

   Idris elaborator scripts will be developed for each formal languages.

   The following sections describe how these formal languages have been
   or will be themselves be converted into types with the goal of
   importing them in computerate specifications.

6.2.1.  Augmented BNF (ABNF)

   Augmented Backus-Naur Form (ABNF) [RFC5234] is a formal language used
   to describe a text based data layout.

   An ABNF can be described by defining a value for the types from the
   "RFC5234.Main" module:

   <CODE BEGINS>
   rulename : Rule
   rulename = "rulename" `Eq` (Concat (TermDec 97 []) (TermDec 98 [])
     [TermDec 99 []])
   <CODE ENDS>

                                 Figure 30

   That value can then be inserted in a document, which will convert it
   as a proper ABNF, so





Petit-Huguenin            Expires 5 August 2021                [Page 41]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
    [source,abnf]
    ----
    {`rulename`}
    ----
   <CODE ENDS>

                                 Figure 31

   is rendered as

   rulename = %d97 %d98 %d99

                                 Figure 32

   See Section 8.2.2 for details on that package.

6.2.2.  Augmented Packet Header Diagrams (APHD)

   Augmented Packet Header Diagram (APHD)
   [I-D.mcquistin-augmented-ascii-diagrams] is a formal language used to
   describe an augmented bit diagram in a machine-readable format.

   It can be seen as an extension to the self-contained bit diagram in
   Section 5.1.3, where more information are extracted from the Idris
   type, and more properties are carried in the list of properties:

   *  From the Idris type:

      -  The size of a field in the Idris type is converted into the
         field's width.

      -  The size constraints in Idris are converted into a variable
         size field (Section 4.1).

      -  A constraint that reduces the possible values (like for the
         version field) is converted into a constraint on field value
         (Section 4.4).

      -  Alternative constructors (i.e., a Sum type) generate a presence
         predicate (Section 4.2).

   *  From the additional structure:

      -  The name of the PDU.

      -  The name of each field




Petit-Huguenin            Expires 5 August 2021                [Page 42]


Internet-Draft           Computerate Specifying            February 2021


      -  The eventual short name for each field, with the same
         constraint than in Section 5.

      -  The Bit unit to use to display the size for each field.

      -  The description for each field.

   The description for each field is a value of "AsciiDoc" type, which
   permits to correctly format it.  In addition, it is possible to
   insert calculation or even other type representation in the
   description by using an "AsciiDoc" type that works similarly than
   code embedding.

   Reusing the type in Section 6.1.2, the conversion process would
   partially look like this:

   <CODE BEGINS>
   > ipv4 : AphdPdu
   > ipv4 = MkAphd `{{MkInternetHeader}} "IPv4 Header" [
   >   MkField "Version" (Just "V") Bit [(MkSentence "This is a" ++
   >     "fixed-width field, whose full label is shown in the " ++
   >     "diagram.  The field's width --), MkCode(`(size version)),
   >     MkSentence(" bits -- is given in  the label of the " ++
   >     "description list, separated from the field's label " ++
   >     "by a colon.")],
   > ...
   > ]

   {`%runElab toAphd names`}
   <CODE ENDS>

                                 Figure 33

   and is rendered as:

















Petit-Huguenin            Expires 5 August 2021                [Page 43]


Internet-Draft           Computerate Specifying            February 2021


   An IPv4 Header is formatted as follows:
    0                   1                   2                   3
    0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |Version|   IHL |    DSCP   |ECN|         Total Length          |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |         Identification        |Flags|     Fragment Offset     |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   | Time to Live  |    Protocol   |        Header Checksum        |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                         Source Address                        |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                      Destination Address                      |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                            Options                          ...
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   |                                                               :
   :                            Payload                            :
   :                                                               |
   +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+

   where:

   Version (V): 4 bits.  This is a fixed-width field, whose full label
     is shown in the diagram.  The field's width -- 4 bits -- is given
     in the label of the description list, separated from the field's
     label by a colon.
    ...

                                 Figure 34

6.2.3.  Cosmogol

   Cosmogol [I-D.bortzmeyer-language-state-machines] is a formal
   language designed to define states machines.  The Internet-Draft will
   be retrofitted as a computerate specification to provide an internal
   Domain Specific Language (DSL) that permits specifying an instance of
   that language.

   As a Petri Net can be seen as a set of state machines, it will be
   possible to extract part of a Petri Net and generate the equivalent
   state machine in Cosmogol format.

6.3.  Packages for Protocols







Petit-Huguenin            Expires 5 August 2021                [Page 44]


Internet-Draft           Computerate Specifying            February 2021


6.3.1.  Type Transformations

   Protocols evolve over time, and the documents that standardize them
   also need to evolve with them.  Each SDO has a specific set of
   methods to do so, from having the possibility of modifying a
   document, to systematically releasing a complete new document when a
   modification is needed.  The IETF uses a combination of methods to
   update the documents that define a protocol.

   One such method is to release a new document that completely replaces
   ("obsoletes") an existing protocol.  E.g., TLS 1.2 [RFC5246] was
   completely replaced by TLS 1.3 [RFC8446] such as there is no need to
   read RFC 5246 to be able to implement RFC 8446.

   Alternatively only part of a protocol needs modification, so the
   method used in that case is to issue a new document that only updates
   that specific part.  E.g., RFC 2474 updates only the definition of
   the ToS field in the Internet Header defined in RFC 791, so reading
   both documents is required to implement the Internet Protocol.  These
   two methods can be combined together, like was done for RFC 2474.
   RFC 2474 obsoleted RFC 1349 and RFC 1349 was the original update for
   RFC 791.

   Systematically updating a protocol in new documents instead of
   replacing it means that sometimes a lot of different documents has to
   be read before implementing a modern implementation of a specific
   protocol.  E.g., the DNS was originally defined in RFC 1034 and 1035,
   but was updated by more than 30 documents since, requiring to read
   all of them to implement that protocol.

   In the DNS example we are not even counting definitions of codepoints
   as protocol updates.  This is the third method used at the IETF to
   evolve a standard, by defining new codepoints and their associated
   data.  That last method will be explored in more detail in
   Section 6.3.2, so the remaining of this section can focus on the two
   other methods.

   Writing a computerate specification for a new document or a document
   that obsoletes another one is straightforward, as the specification
   will contain all the types that are needed to formalize it.  On the
   other hand it is less clear what should go into a specification that
   updates another one.

   A simplistic solution is to copy the whole Idris content from the
   original specification into the new one and modify that new content,
   but this creates a few problems:





Petit-Huguenin            Expires 5 August 2021                [Page 45]


Internet-Draft           Computerate Specifying            February 2021


   Firstly the content from the original specification will have to be
   copied again each time it was modified, as computerate specifications
   are meant to evolve, even if the underlying document did not.

   Secondly the size of the code should be roughly proportional to the
   size of the document itself, so the actual update is made obvious
   from the content.

   So instead of manually copying the content, an Idris elaboration can
   be used to copy it automatically and apply the minimal modifications
   needed at the same time.

   But first the specification that will be updated needs to be
   prepared, by encapsulating the types in a function that will be used
   to generate the types themselves:

   <CODE BEGINS>
   export
   internetHeader : List Decl
   internetHeader = `[
   ||| InternetHeader
   export
   data InternetHeader : Type where
     MkInternetHeader :
       (version : BitVector 4) -> version = [O, I, O, O] =>
       (ihl : (Unsigned 4, Data)) -> snd ihl = tetra =>
       (tos : Tos) ->
       (length : (Unsigned 16, Data)) -> snd length = octet =>
       (id : Unsigned 16) ->
       (flags : Flags) ->
       (offset : Unsigned 13, Data)) -> snd offset = octa =>
       (ttl : (Unsigned 8, Time)) -> snd ttl = second =>
       (protocol : BitVector 16) ->
       (checksum : BitVector 16) ->
       (source : BitVector 32) ->
       (dest : BitVector 32) ->
       (options : List Option) ->
       (padding : BitVector n) ->
         n = pad 32 options => padding = bitVector =>
       InternetHeader
       ]
   %runElab declare internetHeader
   <CODE ENDS>

                                 Figure 35






Petit-Huguenin            Expires 5 August 2021                [Page 46]


Internet-Draft           Computerate Specifying            February 2021


   This code behaves exactly like the previous definition, with the
   major difference that the documentation is not generated for that
   type.  Idris2 has been enhanced with the possibility to cache the
   result of an elaboration directly in the source code, and to
   automatically send a warning when the cache needs to be refreshed.
   The interactive command ":gc <line>" automatically generates the code
   followed by a "%cacheElab" line that indicates where the code
   generated ends, something like this:

   <CODE BEGINS>
   %runElab declare internetHeader
   export
   ||| InternetHeader
   data InternetHeader : Type where
     MkInternetHeader :
       (version : BitVector 4) -> version = [O, I, O, O] =>
       (ihl : (Unsigned 4, Data)) -> snd ihl = tetra =>
       (tos : Tos) ->
       (length : (Unsigned 16, Data)) -> snd length = octet =>
       (id : Unsigned 16) ->
       (flags : Flags) ->
       (offset : Unsigned 13, Data)) -> snd offset = octa =>
       (ttl : (Unsigned 8, Time)) -> snd ttl = second =>
       (protocol : BitVector 16) ->
       (checksum : BitVector 16) ->
       (source : BitVector 32) ->
       (dest : BitVector 32) ->
       (options : List Option) ->
       (padding : BitVector n) ->
         n = pad 32 options => padding = bitVector =>
       InternetHeader
   %cacheElab 1506359842985480550 1506359842985480550
   <CODE ENDS>

                                 Figure 36

   The numbers on the "%cacheElab" line are hashes of, respectively, the
   elaboration code and the generated text and permit to detect if
   either were modified since the last time the code was cached.

   With that we can import the definition of the "InternetHeader" type
   and clone in in our new specification:

   <CODE BEGINS>
   import RFC791.IP

   %runElab declare internetHeader
   <CODE ENDS>



Petit-Huguenin            Expires 5 August 2021                [Page 47]


Internet-Draft           Computerate Specifying            February 2021


                                 Figure 37

   The modification needed by the new document can be done by replacing
   the "ToS" field by the newly defined "DSField", using the "replace"
   function:

   <CODE BEGINS>
   import RFC791.IP
   import ComputerateSpecifying.Transform

   dscp : List Decl
   dscp = `[
   public export
   data Dscp : Type where
     MkDscp : (dscp : BitVector 6) ->
              (reserved : BitVector 2) -> reserved = bitVector =>
              Dscp
     ]
   %runElab declare dscp

   %runElab declare (add mypath internetHeader dcp)
   <CODE ENDS>

                                 Figure 38

   At this point using elaboration caching would permit to check that
   the new type indeed uses the "Dscp" type instead of the old "Tos"
   type.

6.3.2.  Extended Registries

      |  NOTE: The mechanisms described in this section requires Type
      |  Providers that are not yet available in Idris2.  Until then,
      |  the constants built by future type providers can be populated
      |  by hand.

   At the difference of the previous section, that describes how to
   formalize the unplanned evolution of a protocol, most protocols are
   designed with the potentiality of evolution, also known as
   extensibility.  These potentialities are generally expressed as
   values for some fields that will be later assigned to a new meaning.

   The meaning for a new value will be defined in a new document, with
   all the documents giving new meanings to a field easily locatable in
   a registry.






Petit-Huguenin            Expires 5 August 2021                [Page 48]


Internet-Draft           Computerate Specifying            February 2021


   Following up on our previous example, RFC 791 defines IP Options only
   for values 0, 1, 7, 68, 131, 136, and 137.  These values, together
   with new values defined by other documents, are listed in the IP
   Option Numbers IANA registry.  E.g., that IANA registry also defines,
   among others, value 25 in RFC 4782.

   The values that are part of a registry are designed to be used with
   the protocol that defined that registry, so it makes sense to
   synthesise a Sum type of all these values in the computerate
   specification for the document that defined that registry.

   Building that Sum type can be done by applying transformations to the
   original type, just like when modifying a protocol in a new
   specification.  The difference is that the list of types that will be
   used in the Sum type needs be collected from the registry, and
   updated each time the registry is updated.

   Idris has a mechanism to read external data during type-checking (a
   feature known as Type Provider), mechanism that could be used to read
   the content of the registry.  A registry generally contains the
   codepoint that identifies a new value and the name of the document
   that defines that value, but unfortunately the protocol registries do
   not contain enough information to automatically find the Idris2 type
   that matches a specific codepoint.

   For instance IANA is the organization that is maintaining the
   registries for the IETF.  The "IP Option Numbers" is an example of a
   registry that contains the list of all the IP Options that can be
   carried by the Internet Protocol.  E.g., in that registry RFC 1191
   contains the description for multiple entries in the registry, and so
   an additional mechanism is needed to find the Idris2 type for each of
   them.

   That additional mechanism is abstracted as an extended registry that
   complements the existing registry, but for the sole purpose of
   finding the exact type to use for each codepoint to generate that Sum
   type.

   Building an "InternetHeader" type that contains all the IP Options
   defined at the time of type-checking looks like this;

   <CODE BEGINS>
   %provide (ipParameter : List (String, Decl)) with registry
     ("https://www.iana.org/assignments/ip-parameters/" ++
     "ip-parameters.xhtml#ip-parameters-2")

   %runELab traverse (add transform internetHeader Add) (type registry)
   <CODE ENDS>



Petit-Huguenin            Expires 5 August 2021                [Page 49]


Internet-Draft           Computerate Specifying            February 2021


                                 Figure 39

   The "%provide" statement reads both the IANA registry and its
   associated extended registry and stores the result in the
   "ipParameter" constant.  Then the "%runElab" statement repetitively
   adds the types retrieved to the "InternetHeader" type.

   Instead of having to manually maintain the extended registries, they
   can be automatically updated by information coming from the type-
   checking of the types in the respective computerate specifications
   that define new values, by binding a specific entry in a registry
   with the type in the specification.

   The mechanism used is also based on a type provider, but this time to
   update the extended registry instead of reading from it:

   <CODE BEGINS>
   %provide (mtur: ()) with extendRegistry
     ("https://www.iana.org/assignments/ip-parameters/" ++
     "ip-parameters.xhtml#ip-parameters-2")
     "11" mtuR
   %provide (mtut : ()) with extendRegistry
     ("https://www.iana.org/assignments/ip-parameters/" ++
     "ip-parameters.xhtml#ip-parameters-2")
     "12" mtuT
   <CODE ENDS>

                                 Figure 40

   Here the statements bind the types defined in "mtuR" and "mtuT" to
   codepoints 11 and 12 in the extended registry of IANA's IP Option
   Numbers registry.

   The next time the code in Figure 39 is type-checked, it will add
   constructors for these two IP Options.

7.  Exporting Specifications

      |  NOTE: The infrastructure for sharing the git repositories for
      |  exported packages is not ready yet.

7.1.  Standard Library

   Computerate specifications can formalize their content to make it
   reusable as a building block for other specifications.  A
   specification that organizes its content along the guidelines
   presented in this section can become a part of the Computerate
   Specification Standard Library.



Petit-Huguenin            Expires 5 August 2021                [Page 50]


Internet-Draft           Computerate Specifying            February 2021


   To be part of the Standard Library, specifications must be organized
   in 4 components:

   Code:  This is the formalization of the content of the standard as an
      Idris package i.e., a set of Idris modules (i.e. files) that
      exports some or all of the types and functions defined in it.  The
      code of these Idris modules is generally interspersed with the
      content of the standard to form literate code.

   Tutorial:  This is a document section that guides the reader step by
      step in the use of the Idris package in a Computerate
      Specification.  A tutorial may import the package itself to
      validate the examples provided as part of the tutorial.  This
      section is considered informative.

   Description:  This is a document section that explains the Idris
      package as a whole i.e, grouping explanations by feature.

   Reference:  This is a document section that is auto-generated from
      the structured comments in the types and functions of the code
      Idris package.  It lists all the types and functions in alphabetic
      order, including the comments on parameters.

   This document is itself an Idris package that is part of the Standard
   Library, Section 7 contains the tutorial part of that package,
   Section 8.1 forms its description part, and Appendix B contains its
   reference.

   For a retrofitted document, the code will be mixed with the existing
   standard to produce a Computerate Specification but the tutorial,
   description and reference parts cannot be added to that standard, so
   they have to be part of a separate document.  It can be a new
   specification written for the express purpose of documenting that
   package.  This is the case for this specification, which documents a
   selection of retrofitted Computerate Specifications that are part of
   the Standard Library.  E.g., Section 6.2.1, and Section 8.2.2 are
   respectively the tutorial and the description for [RFC5234].

   For a new document, the four components should be part of it.  E.g.,
   in this document Section 6.1.5.1, Section 8.1.5, and Appendix B.1.2
   are respectively the tutorial, description, and reference for the
   "BitDiagram" module.









Petit-Huguenin            Expires 5 August 2021                [Page 51]


Internet-Draft           Computerate Specifying            February 2021


7.2.  Transclusions

   RFCs, Internet-Drafts and standard documents published by other SDOs
   did not start their life as computerate specifications, so to be able
   to use them as Idris packages they will need to be progressively
   retrofitted.  This is done by converting the documents into an
   AsciiDoc documents and then enriching them with code, in the same way
   that would have been done if the standard was developed directly as a
   computerate specification.

   Converting the whole document in AsciiDoc and enriching it with code,
   instead of just maintaining a library of code, seems a waste of
   resources.  The reason for doing so is to be able to verify that the
   rendered text is equivalent to the original standard, which will
   validate the examples and formal languages.

   Retrofitted specifications will also be made available as individual
   git repositories as they are converted.

   Because the IETF Trust does not permit modifying an RFC as a whole
   (except for translation purposes), a retrofitted RFC uses
   transclusion, a mechanism that includes parts of a separate document
   at runtime.  This way, a retrofitted RFC is distributed as two
   separate files, the original RFC in text form, and a computerate
   specification that contains only code and transclusions.
   Transclusions use are explained in Appendix A.2.2.

7.3.  Exporting Types and Functions

   Types and functions are exported by using the "export" keyword.  Type
   constructors, interface functions and type functions implementation
   can be additionally exported by prepending the keyword "public" to
   the "export" keyword.

   Additionally, types that may be transformed should be declared as
   explained in Section 6.3.2, i.e. by wrapping them first in a exported
   function that uses a quote declaration, then generating them locally
   using a "declare" elaboration.

8.  Standard Library

      |  NOTE: The libraries described in that section are not yet
      |  available.

8.1.  Internal Modules






Petit-Huguenin            Expires 5 August 2021                [Page 52]


Internet-Draft           Computerate Specifying            February 2021


8.1.1.  AsciiDoc

   The AsciiDoc module provides a way to programmatically build an
   AsciiDoc document without having to worry about the particular
   formatting details.

   Note that, at the difference of the AsciiDoc rendering process that
   tries very hard to render a document in any circumstances, the types
   in this module are meant to only generate a correct document.

   E.g., the string "this is {`N "*bold*""}bold` will be rendered as
   "this is *bold*".  If the intent was to render the "bold" word in
   bold, then the string should have been "this is {`Bold "bold""}`.

8.1.2.  BitVector

   The Computerate Specifying Library provides a number of types and
   functions aimed at defining and manipulating the data types that are
   commonly found in Protocol Data Units (PDU).  The most elementary
   type of data is the bit-vector, which is a list of individual bits.
   Bit-vectors are not always sufficient to describe the subtleties the
   data types carried in a PDU, and several more precise types are built
   on top of them.  See Section 8.1.3 for unsigned integers.

   "BitVector" is a dependent type representing a list of bits, indexed
   by the number of bits contained in that list.  The type is inspired
   by Chapter 6 of [Kroening16] and by [Brinkmann02].

   A value of type "BitVector n" can be built as a series of zeros
   ("bitVector") or can be built by using a list of "O" (for 0) and "I"
   (for 1) constructors.  E.g., "[O, I, O, O]" builds a bit-vector of
   type "BitVector 4" with a value equivalent to 0b0100.

   Bit-vectors can be compared for equality, but they are not ordered.
   They also are not numbers and arithmetics operations cannot be
   applied to them.

   Bit-vectors can be concatenated ("concat"), a smaller bit-vector can
   be extracted from an existing bit-vector ("extract"), or a bit-vector
   can be extended by adding a number of zeros in front of it
   ("extend").

   The usual unary bitwise ("shiftL", "shiftR", "not") operations are
   defined for bit-vectors, as well as binary bitwise operations between
   two bit-vectors of the same size ("and", "or", "xor")

   Finally it is possible to convert the bit at a specific position in a
   bit-vector into a "Bool" value ("test").



Petit-Huguenin            Expires 5 August 2021                [Page 53]


Internet-Draft           Computerate Specifying            February 2021


8.1.3.  Unsigned

   A value of type "Unsigned n" encodes an unsigned integer as a
   "BitVector" of length "n".

8.1.4.  Dimension

   This module permits to manipulate denominate numbers, which are
   numbers associated with a unit.  Examples of denominate numbers are
   "cast (5, meter / second)" (which uses a unit of speed), or "cast
   (10, meter * meter * meter)" (which uses a unit of volume).

   In this module a denominate number is a value of type "Denominate
   xs".  It carries one number as a fraction.  Its type is indexed over
   a list of dimensions, each associated with an exponent number.  All
   together this type can represent any unit that is based directly or
   indirectly from the base dimensions defined in the "Dimension" type.

   Denominate numbers are constructed by passing a tuple made of a
   number (either an "Integer" or a "Double") and a unit to the "cast"
   function.  E.g., "cast (5, megabit)" will build the denominate number
   5 with the "megabit" unit.

   Dimensionless denominate numbers can be constructed by using the
   "none" unit, as in "cast (10, none)"

   Denominate numbers can be converted back into a tuple with the
   "fromDenominate" function.

   Denominate numbers can be added, subtracted or negated (respectively
   "+", "-", and "neg").  All these operations can only be done on
   denominate numbers with the same exact dimension, and the result will
   also carry the same dimension.  This prevents what is colloquially
   known as mixing apples and oranges.

   For the same reason, adding a number to a non-dimensionless
   denominate number is equally impossible.

   The "*", "/", and "recip" operations respectively multiply, divide
   and calculate the reciprocal of denominate numbers.  These operations
   can be done on denominate number that have different types, and the
   result dimension will be derived from the dimension of the arguments.
   E.g. multiplying "cast (5, meter)" by "cast (6, meter)" will return
   the equivalent of "cast (30, meter * meter)".

   Also multiplying a denominate number by a (dimensionless) number is
   possible e.g., as in multiplying "cast (5, meter)" by "cast (10,
   none)", which will return the equivalent of "cast (50, meter)".



Petit-Huguenin            Expires 5 August 2021                [Page 54]


Internet-Draft           Computerate Specifying            February 2021


   Ultimately we want to insert in a computerate specification the value
   of a denominate number, together with its unit, as text, which is
   done by implementing the "Show" interface on a denominate number in
   its tuple form.  E.g. "fromDenominate (cast (5, meter / second))
   (kilometer / hour)" can be directly inserted in a document and will
   be substituted with the string "18 km/h".

   For each dimension we define a list of constants that represents
   units of that dimension.  Units that uses a prefix are automatically
   generated, which is the case for SI units for the "Time" dimension
   (i.e., from "yoctosecond" to "yottasecond"), SI units (only positive
   powers of 10) for the "Data" dimension (i.e., from "kilobit" to
   "yottabit"), and IEC units (positive powers of 2) for the "Data"
   dimension (i.e., from "kibibit" to "yobibit").

   Additional constants like "minute", "hour", "day", "byte", "wyde",
   "tetra", "octa", etc, complement the standard units.  The "byte",
   "wyde", "tetra", and "octa" units are defined in page 4 of [TAOCP].

8.1.5.  BitDiagram

   A bit diagram displays a graphical representation of a data layout at
   the bit level.

   The "BitDiagram" type is used to build BitDiagrams values.

   The "toAsciiDoc" function converts a "BitDiagram" value into an
   AsciiDoc Literal Block which can be inserted directly in the
   document.

   Adhoc types can also be used to generate a bit diagram, by passing
   that type to the "toDiagram" function and the returned value to the
   "toAsciiDoc" function.  The "toDiagram" function will build a field
   only for types that have an implementation for the "Size" interface.
   The function "toDiagram" also takes an auxiliary Type "Names" that
   associate names with these types.

8.1.6.  Transform

   This module permits to manipulate values that are in the very generic
   form of trees.  These manipulations consist of removing, or replacing
   a selected value or values in that tree.

   The values to manipulate are selected using a path, which is a series
   of instructions used to move the focus of the manipulation up, down
   and sideway in the tree and to apply a predicate until a set of
   values are chosen.




Petit-Huguenin            Expires 5 August 2021                [Page 55]


Internet-Draft           Computerate Specifying            February 2021


   The values selected are then either removed or replaced by a new
   value.  The rest of the tree stays unmodified.

   This mechanism is very generic and can be applied to any tree, but it
   is meant to modify the types defined in the
   "Language.Reflection.TTImp" and "Language.Reflection.TT" standard
   modules, with the goal of generating types that are derived from
   existing types.

8.1.7.  Tpn

   This module permits to build Petri Nets and then derive types from
   that Petri net, types that can be used to ensure that a protocol
   implementation follows that Petri Net.

8.2.  Meta-Language Packages

8.2.1.  Augmented Packet Header Diagrams (APHD)

   The "augmented-ascii-diagram" Idris package provides a set of modules
   that permits to generate parts of AsciiDoc documents that are conform
   to the [I-D.mcquistin-augmented-ascii-diagrams] specification.

   The "AAD.Pdu" type is used to define a PDU.

8.2.2.  RFC 5234 (ABNF)

   TBD.

8.3.  Protocol Packages

8.3.1.  RFC 791 (Internet Protocol)

   TBD.

9.  Bibliography

   [AsciiBib] "AsciiBib", <https://www.relaton.com/specs/asciibib/>.

   [AsciiDoc] "AsciiDoc", <https://en.wikipedia.org/wiki/AsciiDoc/>.

   [Asciidoctor]
              "Asciidoctor", <https://asciidoctor.org/docs/user-manual>.

   [Blockquotes]
              "Markdown-style blockquotes",
              <https://asciidoctor.org/docs/user-manual/#markdown-style-
              blockquotes>.



Petit-Huguenin            Expires 5 August 2021                [Page 56]


Internet-Draft           Computerate Specifying            February 2021


   [Brinkmann02]
              Brinkmann, R. and R. Drechsler, "RTL-datapath verification
              using integer linear programming", In Proceedings of the
              2002 Asia and South Pacific Design Automation Conference.
              IEEE Computer Society, 2002,
              <http://dl.acm.org/citation.cfm?id=835389>.

   [CPN]      Jensen, K. and L. Kristensen, "Coloured Petri Nets:
              Modelling and Validation of Concurrent Systems", Springer
              Dordrecht ; New York, 2009.

   [Curry-Howard]
              "Curry-Howard correspondence",
              <https://en.wikipedia.org/wiki/Curry-
              Howard_correspondence>.

   [Elab]     Christiansen, D. and E. Brady, "Elaborator reflection:
              extending Idris in Idris", In Proceedings of the 21st ACM
              SIGPLAN International Conference on Functional
              Programming. ACM Press-Association for Computing
              Machinery, 2016, <https://research-repository.st-
              andrews.ac.uk/bitstream/handle/10023/9522/
              elab_reflection_paper.pdf>.

   [I-D.bortzmeyer-language-state-machines]
              Bortzmeyer, S., "Cosmogol: a language to describe finite
              state machines", Work in Progress, Internet-Draft, draft-
              bortzmeyer-language-state-machines-01, 1 November 2006,
              <https://tools.ietf.org/html/draft-bortzmeyer-language-
              state-machines-01>.

   [I-D.mcquistin-augmented-ascii-diagrams]
              McQuistin, S., Band, V., Jacob, D., and C. Perkins,
              "Describing Protocol Data Units with Augmented Packet
              Header Diagrams", Work in Progress, Internet-Draft, draft-
              mcquistin-augmented-ascii-diagrams-06, 1 July 2020,
              <http://www.ietf.org/internet-drafts/draft-mcquistin-
              augmented-ascii-diagrams-06.txt>.

   [I-D.ribose-asciirfc]
              Tse, R., Nicholas, N., and P. Brasolin, "AsciiRFC:
              Authoring Internet-Drafts And RFCs Using AsciiDoc", Work
              in Progress, Internet-Draft, draft-ribose-asciirfc-08, 1
              April 2018, <http://www.ietf.org/internet-drafts/draft-
              ribose-asciirfc-08.txt>.

   [Idris2]   "Idris2: A Language with Dependent Types",
              <https://idris2.readthedocs.io/en/latest/>.



Petit-Huguenin            Expires 5 August 2021                [Page 57]


Internet-Draft           Computerate Specifying            February 2021


   [Knuth92]  Knuth, D., "Literate Programming", Center for the Study of
              Language and Information, 1992.

   [Kroening16]
              Kroening, D. and O. Strichman, "Decision Procedures: An
              Algorithmic Point of View", Springer Berlin, 2017.

   [Linear-Resources]
              "Linear Resources",
              <https://idris2.readthedocs.io/en/latest/app/linear.html>.

   [Literate] "Literate Programming",
              <https://idris2.readthedocs.io/en/latest/reference/
              literate.html>.

   [Metanorma]
              "Metanorma", <https://www.metanorma.com/>.

   [Metanorma-IETF]
              "Metanorma-IETF",
              <https://www.metanorma.com/author/ietf/>.

   [Momot16]  Momot, F., Bratus, S., Hallberg, S., and M. Patterson,
              "The Seven Turrets of Babel: A Taxonomy of LangSec Errors
              and How to Expunge Them.", In: 2016 IEEE Cybersecurity
              Development (SecDev), 2016,
              <http://ieeexplore.ieee.org/document/7839788/>.

   [RFC-Guide]
              "RFC Style Guide",
              <https://www.rfc-editor.org/styleguide/part2/>.

   [RFC0761]  Postel, J., "DoD standard Transmission Control Protocol",
              RFC 0761, DOI 10.17487/RFC0761, January 1980,
              <https://www.rfc-editor.org/info/rfc761>.

   [RFC0791]  Postel, J., "Internet Protocol", RFC 0791,
              DOI 10.17487/RFC0791, September 1981,
              <https://www.rfc-editor.org/info/rfc791>.

   [RFC2119]  Bradner, S., "Key words for use in RFCs to Indicate
              Requirement Levels", BCP 14, RFC 2119,
              DOI 10.17487/RFC2119, March 1997,
              <https://www.rfc-editor.org/info/rfc2119>.

   [RFC5234]  Crocker, D., Ed. and P. Overell, "Augmented BNF for Syntax
              Specifications: ABNF", RFC 5234, DOI 10.17487/RFC5234,
              January 2008, <https://www.rfc-editor.org/info/rfc5234>.



Petit-Huguenin            Expires 5 August 2021                [Page 58]


Internet-Draft           Computerate Specifying            February 2021


   [RFC5246]  Dierks, T. and E. Rescorla, "The Transport Layer Security
              (TLS) Protocol Version 1.2", RFC 5246,
              DOI 10.17487/RFC5246, August 2008,
              <https://www.rfc-editor.org/info/rfc5246>.

   [RFC7991]  Hoffman, P., "The "xml2rfc" Version 3 Vocabulary",
              RFC 7991, DOI 10.17487/RFC7991, December 2016,
              <https://www.rfc-editor.org/info/rfc7991>.

   [RFC8446]  Rescorla, E., "The Transport Layer Security (TLS) Protocol
              Version 1.3", RFC 8446, DOI 10.17487/RFC8446, August 2018,
              <https://www.rfc-editor.org/info/rfc8446>.

   [RFC8489]  Petit-Huguenin, M., Salgueiro, G., Rosenberg, J., Wing,
              D., Mahy, R., and P. Matthews, "Session Traversal
              Utilities for NAT (STUN)", RFC 8489, DOI 10.17487/RFC8489,
              February 2020, <https://www.rfc-editor.org/info/rfc8489>.

   [RFC8656]  Reddy, T., Ed., Johnston, A., Ed., Matthews, P., and J.
              Rosenberg, "Traversal Using Relays around NAT (TURN):
              Relay Extensions to Session Traversal Utilities for NAT
              (STUN)", RFC 8656, DOI 10.17487/RFC8656, February 2020,
              <https://www.rfc-editor.org/info/rfc8656>.

   [Stump16]  Stump, A., "Verified Functional Programming in Agda", ACM
              Books series, 2016.

   [TAOCP]    Knuth, D., "The Art Of Computer Programming", Addison-
              Wesley Pearson Education, 2005.

   [TLP5]     "Legal Provisions Relating to IETF Documents",
              <https://trustee.ietf.org/license-info/IETF-TLP-5.htm>.

   [Type-Driven]
              Brady, E., "Type-Driven Development with Idris", Manning
              Shelter Island, 2017.

   [Zave11]   Zave, P., "Experiences with Protocol Description",
              Workshop on Rigorous Protocol Engineering (WRiPE'11),
              2011, <https://www.researchgate.net/profile/Pamela_Zave/pu
              blication/266230560_Experiences_with_Protocol_Description/
              links/56eaf9fb08ae9dcdd82a6590.pdf>.

Appendix A.  Command Line Tools







Petit-Huguenin            Expires 5 August 2021                [Page 59]


Internet-Draft           Computerate Specifying            February 2021


A.1.  Installation

   The computerate command line tools are run inside a Docker image, so
   the first step is to install the Docker software or verify that it is
   up to date (https://docs.docker.com/install/).

   Note that for the usage described in this document there is no need
   for Docker EE or for having a Docker account.

   The following instructions assume a Unix based OS, i.e. Linux or
   MacOS.  Lines separated by a "\" character are meant to be executed
   as one single line, with the "\" character removed.

A.1.1.  Download the Docker Image

   To install the computerate tools, the fastest way is to download and
   install the Docker image using BitTorrent.  The BitTorrent magnet URI
   for the version distributed with this version of the document is:

   magnet:?xt=urn:btih:20d184da7a740dfecbb8b29464aa87610f95a316&dn=tools
   -05.tar.xz

   After this, the image can be loaded in Docker as follow:

   docker load -i tools-05.tar.xz

                                 Figure 41

   Note that a new version of the tooling is released at the same time a
   new version of this document is released, each time with a new
   BitTorrent magnet URI.

A.2.  The "computerate" Command

   The Docker image main command is "computerate", which takes the same
   parameters as the "metanorma" command from the Metanorma tooling:

   docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \
     computerate/tools computerate -t ietf -x txt <file>

                                 Figure 42

   The differences with the "metanorma" command are explained in the
   following sections.







Petit-Huguenin            Expires 5 August 2021                [Page 60]


Internet-Draft           Computerate Specifying            February 2021


A.2.1.  Literate Files

   The "computerate" command can process Literate Idris files (files
   with a "lidr" extension, aka lidr files), in addition to AsciiDoc
   files (files with an "adoc" extension, aka adoc files).  When a lidr
   file is processed, all embedded code fragments (text between prefix
   "{`" and suffix "`}") are evaluated in the context of the Idris code
   contained in this file.  Each code fragment (including the prefix and
   suffix) are then substituted by the result of that evaluation.

   The "computerate" command can process included lidr files in the same
   way.  The embedded code fragments in the imported file are processed
   in the context of the included lidr file, not in the context of the
   including file.  Idris modules (either from an idr or lidr file) can
   be imported the usual way.

   The literate code (which is all the text that is starting by a ">"
   symbol in column 1) in a lidr file will not be part of the rendered
   document.

A.2.2.  Transclusions

   The "computerate" command can process transclusions, a special form
   of AsciiDoc "include" that takes a range of lines as parameters:

   <CODE BEGINS>
   include::rfc5234.txt[lines=26..35]
   <CODE ENDS>

                                 Figure 43

   Here the "include" macro will be replaced by the content of lines 26
   to 35 (included) of [RFC5234].

   The "sub" parameter permits modifying the copied content according to
   a regular expression.  For instance the following converts references
   into the AsciiDoc format:

   <CODE BEGINS>
   include::rfc5234.txt[lines=121..131,sub="/\[([^\]])\]/<<\1>>/"]
   <CODE ENDS>

                                 Figure 44

   In the following example, the text is converted into a note:






Petit-Huguenin            Expires 5 August 2021                [Page 61]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   include::rfc5234.txt[lines=151,sub="/^.*$/NOTE: \0/"]
   <CODE ENDS>

                                 Figure 45

A.2.3.  IdrisDoc Generation

   The "computerate" can include in a document the result of the
   generation of the IdrisDoc for a package.  This is done by including
   a line like this:

   <CODE BEGINS>
   include::computerate-specifying.ipkg[leveloffset=+2]
   <CODE ENDS>

                                 Figure 46

   The "leveloffset" attribute is used to adjust the level of the
   section generated, as the sections generated always have the level 2.

A.2.4.  Outputs

   Instead of generating a file based on the name of the input file, the
   "computerate" command generates a file based on the ":name:"
   attribute in the header of the document.

   In addition to the "txt", "html", "xml", and "rfc" output formats
   supported by "metanorma", the "computerate" command can also be used
   to generate for the "pdf" and "json" formats by using these names
   with the "-x" command line parameter.

   If the type of document passed to the "computerate" command (options
   "-t" or "--type") is one of the following, then the document will be
   processed directly using "asciidoctor", and not "metanorma": "html,
   "html5, "xhtml", "xhtml5", "docbook", "docbook5", "manpage", "pdf",
   and "revealjs".  The asciidoctor-diagram extension is available in
   this mode with the following supported diagram types: "actdiag",
   "blockdiag", "ditaa", "graphviz", "meme", "mscgen", "nwdiag",
   "plantuml", and "seqdiag".

A.2.5.  Extended Registry

      |  NOTE: More to come on the exact mechanism used to share the
      |  extended repositories.






Petit-Huguenin            Expires 5 August 2021                [Page 62]


Internet-Draft           Computerate Specifying            February 2021


A.2.6.  Bibliography

   Because most references are stable, there is not much point in
   retrieving them each time the document is processed, even with the
   help of a cache, so lookup of external references is disabled.

   The following command can be used to fetch an RFC reference:

   tools relaton fetch "IETF(RFC.2119)" --type IETF >ietf.xml

                                 Figure 47

   Then ietf.xml file needs to be edited by removing the first two
   lines.  After this the xml file can be converted into a AsciiDoc
   document:

   tools relaton convert ietf.xml -f asciibib

                                 Figure 48

   This will generate an ietf.adoc file that can be copied in the
   bibliography section.  Note that section level of the bibliographic
   item needs to be one up the section level of the bibliography
   section.

   One exception is a reference to a standard document that is under
   development, like an Internet-Draft.

   In that case the best way is to have a separate script that fetch,
   edit and convert Internet-Drafts as separate files.  Then these files
   can be inserted dynamically in the bibliography section using
   includes.

   The command to retrieve an Internet-Draft reference is as follow:

   tools relaton fetch "IETF(I-D.bortzmeyer-language-state-machines)" \
    --type IETF >bortzmeyer-language-state-machines.adoc

                                 Figure 49

   Additionally the following sections show how to manually format some
   common types of bibliographic items, most of then adapted from
   [RFC-Guide].

A.2.6.1.  Internet-Draft






Petit-Huguenin            Expires 5 August 2021                [Page 63]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   [%bibitem]
   === {blank}
   id:: RFC-STYLE
   title.content:: RFC Style Guide
   contributor::
   contributor.person.name.completename.content:: Heather Flanagan
   contributor.role.type:: author
   contributor::
   contributor.person.name.completename.content:: Sandy Ginoza
   contributor.role.type:: author
   date.type:: published
   date.on:: 2014-07-20
   link::
   link.type:: TXT
   link.content:: https://www.ietf.org/.../draft-flanagan-style-03.txt
   docid::
   docid.type:: Work
   docid.id:: in Progress
   docid::
   docid.type:: Internet-Draft
   docid.id:: draft-flanagan-style-03
   <CODE ENDS>

                                 Figure 50

A.2.6.2.  RFC
























Petit-Huguenin            Expires 5 August 2021                [Page 64]


Internet-Draft           Computerate Specifying            February 2021


   <CODE BEGINS>
   [%bibitem]
   === {blank}
   id:: RFC-STYLE2
   title.content:: RFC Style Guide
   contributor::
   contributor.person.name.completename.content:: Heather Flanagan
   contributor.role.type:: author
   contributor::
   contributor.person.name.completename.content:: Sandy Ginoza
   contributor.role.type:: author
   date.type:: published
   date.on:: 2014-09
   link::
   link.type:: src
   link.content:: http://www.rfc-editor.org/info/rfc7322
   docid::
   docid.type:: RFC
   docid.id:: 7322
   docid::
   docid.type:: DOI
   docid.id:: 10.17487/RFC7322
   <CODE ENDS>

                                 Figure 51

A.2.6.3.  Email

   <CODE BEGINS>
   [%bibitem]
   === {blank}
   id:: reftag
   title.content:: Subject: Subject line
   contributor::
   contributor.person.name.completename.content:: A. Sender
   contributor.role.type:: author
   date.type:: published
   date.on:: 2014-09-05
   link::
   link.type:: src
   link.content:: https://mailarchive.ietf.org/.../Ed4OHwozljyjklpAE/
   docid::
   docid.type:: message to the
   docid.id:: listname mailing list
   <CODE ENDS>

                                 Figure 52




Petit-Huguenin            Expires 5 August 2021                [Page 65]


Internet-Draft           Computerate Specifying            February 2021


A.2.6.4.  IANA

   <CODE BEGINS>
   [%bibitem]
   === {blank}
   id:: IANA-IKE
   title.content:: Internet Key Exchange (IKE) Attributes
   contributor.person.name.completename.content:: IANA
   contributor.role.type:: author
   link::
   link.type:: src
   link.content:: http://www.iana.org/assignments/ipsec-registry
   <CODE ENDS>

                                 Figure 53

A.2.6.5.  Web-Based Public Code Repositories

   <CODE BEGINS>
   [%bibitem]
   === {blank}
   id:: pysaml2
   title.content:: Python implementation of SAML2
   date.type:: published
   date.on:: 2018-03-01
   docid::
   docid.type:: commit
   docid.id:: 7135d53
   link::
   link.type:: src
   link.content:: https://github.com/IdentityPython/pysaml2
   <CODE ENDS>

                                 Figure 54

A.3.  Idris REPL

   idr and lidr files can be loaded directly in the Idris REPL for
   debugging:

   docker run --rm -it -u $(id -u):$(id -g) -v $(pwd):/computerate \
     computerate/tools idris2 <lidr-file>

                                 Figure 55

   It is possible to directly modify the source code in the REPL by
   entering the ":e" command, which will load the file in an instance of
   VIM preconfigured to interact with the REPL.



Petit-Huguenin            Expires 5 August 2021                [Page 66]


Internet-Draft           Computerate Specifying            February 2021


   The "idris2-vim" add-ons (which provides interactive commands and
   syntax coloring) is augmented with a feature that permits to use both
   Idris and AsciiDoc syntax coloring.  To enable it, add the following
   line at the end of all lidr file:

   > -- vim:filetype=lidris2.asciidoc

                                 Figure 56

A.4.  Other Commands

   For convenience, the docker image provides the latest version of the
   xml2rfc, aspell, and idnits tools.

   docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \
     computerate/tools xml2rfc
   docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \
     computerate/tools idnits --help
   docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \
     computerate/tools aspell

                                 Figure 57

   The Docker image also contains a extended version of git that will be
   used to retrieve the computerate specifications as explained in
   Appendix A.5.

A.5.  Source Repositories

      |  NOTE: More to come on the exact mechanism used to retrieve the
      |  source repositories.

A.6.  Modified Tools

   The following sections list the tools distributed in the Docker image
   that have been modified for integration with the "computerate" tool.

A.6.1.  Idris2

   URL:  https://github.com/idris-lang/Idris2.git
   Version:  0.3.0 commit 05c9029
   Modifications:

   *  The interactive command ":gc" permits to display the result of an
      elaboration.
   *  The types in TTImp can carry the documentation for the types that
      will be generated from them.




Petit-Huguenin            Expires 5 August 2021                [Page 67]


Internet-Draft           Computerate Specifying            February 2021


   *  The "%cacheElab" directive permits to cache the result of an
      elaboration in the source code instead of been regenerated at each
      type-checking.
   *  A new idris2 wrapper sets the correct mappings for recursive
      build.
   *  "--mkdoc <ipkg-file>" generates the package documentation in
      AsciiDoc on stdout.
   *  Elaborations can be exported and documented.
   *  "package" and "depends" in ipkg file can use quoted strings.
   *  "--depends" lists the dependencies.
   *  "--map <package>=<dir>" maps between a package and a directory.
   *  "--paths" now displays the paths after modification.
   *  Fix boolean operators precedence.
   *  Replace the literate processor by a faster one.  Remove support
      for reversed Bird marks.

A.6.2.  asciidoctor

   URL:  https://github.com/asciidoctor/asciidoctor.git
   Version:  2.0.12
   Modifications:

   *  Process lidr and lipkg files.
   *  Preprocessor for Idris literate source.
   *  Include processor for transclusions.

A.6.3.  metanorma

   URL:  https://github.com/metanorma/metanorma
   Version:  1.2.5
   Modifications:

   *  Generate the filename from the name header attribute.
   *  Process files with lidr and lipkg extensions.

A.6.4.  metanorma-ietf

   URL:  https://github.com/metanorma/metanorma-ietf
   Version:  2.2.8
   Modifications:

   *  Fix the content of the generated <sourcecode> so it is displayed
      correctly in html and pdf outputs.
   *  Fix empty RFC number.
   *  Add generation of json file.
   *  Generates DOI, RFC and Internet-Draft references.  Truncate the
      date according to type.
   *  Do not add content in xrefs.



Petit-Huguenin            Expires 5 August 2021                [Page 68]


Internet-Draft           Computerate Specifying            February 2021


A.6.5.  idris2-vim

   URL:  https://github.com/edwinb/idris2-vim
   Version:  commit 964cebe
   Modifications:

   *  the "IdrisGenerateCache" command (mapped to <LocalLeader>_z) on a
      "%runElab line" displays the result of the elaboration.
   *  Support for lidris2 files.
   *  Syntax colouring for document language in lidris2.

A.7.  Bugs and Workarounds

   Installation:

   *  The current version of Docker in Ubuntu fails, but this can be
      fixed with the following commands:

   sudo apt-get install containerd.io=1.2.6-3
   sudo systemctl restart docker.service

                                 Figure 58

   Idris2:

   *  :gc is currently broken.
   *  Docstrings are not generated correctly.
   *  Interactive commands are missing or not working well with literate
      code.
   *  Changing the installation prefix requires two installations.
   *  Documentation not generated for namespaces and records.
   *  Recursive build incomplete.

   metanorma:

   *  RFC and I-D references are not correctly generated by relaton.
      The workaround is to remove the IETF docid and to add the
      following:

   docid::
   docid.type:: BCP
   docid.id:: 37
   docid::
   docid.type:: RFC
   docid.id:: 5237

                                 Figure 59




Petit-Huguenin            Expires 5 August 2021                [Page 69]


Internet-Draft           Computerate Specifying            February 2021


   computerate:

   *  code blocks escape a '>' in the first column.  The workaround is
      to insert a space before the '>'.

A.8.  TODO List

   Idris2:

   *  Add documentation support for all types in TTImp.
   *  ":gc!" should update the file.
   *  "%cacheElab" should check hashes.
   *  Add a way to generate a hole name.
   *  Literate ipkg to merge the Main.adoc and ipkg files.

   metanorma:

   *  Merge bibliographies.
   *  Extract bibliography from computerate specification.
   *  Generate xml2rfc <contact> element.
   *  Generate .rfc.xml and err file with the same name.
   *  Generate rfc.xml as xml and xml under another extension so the
      xml2rfc file can be directly submitted to the IETF secretariat.

   computerate:

   *  Generate sourcecode blocks from existing code.
   *  Pass surrounding line for embedded code so the Asciidoc module can
      process constrained elements.
   *  Implement self-inclusion to reorder a document.
   *  Backport embedded blocks from Coriander.

   vim:

   *  Starting vim in docker often result in an invalid terminal size
      when a file is loaded.  Using the following command line solves
      the problem:

   docker run --rm -it -u $(id -u):$(id -g) -e COLUMNS=$(tput cols) \
   -e LINES=$(tput lines) -v $(pwd):/computerate computerate/tools \
   vim <lidr-file>

                                 Figure 60

   rfc2adoc:






Petit-Huguenin            Expires 5 August 2021                [Page 70]


Internet-Draft           Computerate Specifying            February 2021


   *  This future tool will be able to convert an xml2rfc v3 file into
      an AsciiDoc file.  It will also be able to update an already
      converted file without losing the Idris annotations.

Appendix B.  Reference

      |  NOTE: The code for the libraries described in that section is
      |  not yet ready to be published.

B.1.  Package computerate-specifying

   The Builtin Computerate Specification Standard Library.

   Version:  0.1
   Author(s):  Marc Petit-Huguenin
   Dependencies:  augmented-ascii-diagrams, rfc5234

B.1.1.  Module ComputerateSpecifying.AsciiDoc

   A module to generate valid AsciiDoc.

   data Block : Type
      A block of text

      Implements Show.

      Admonition : Block

      Example : Block

      Listing : Block

      Literal : List String -> Block

      Passthrough : Block

      Quote : Block

      Sidebar : Block

      Source : (lang : Maybe String) -> List String -> Block

      Stem : Block

      Table : Block

      Verse : Block




Petit-Huguenin            Expires 5 August 2021                [Page 71]


Internet-Draft           Computerate Specifying            February 2021


      Paragraph : (lines : List Line) -> length lines > 0 = True =>
      Block

   data Inline : Type
      A type for inline text.

      Lit : String -> Inline

      Italic : List Inline -> Inline

      Bold : List Inline -> Inline

      Subscript : List Inline -> Inline

      Superscript : List Inline -> Inline

      Monospace : List Inline -> Inline

      Highlight : List Inline -> Inline

      Custom : String -> List Inline -> Inline

      Attribute : String -> Inline

      Link : (uri : String) -> (text : List Inline) ->
      (attributes : List String) -> Inline
         uri:  The URI
         text:  The text
         attributes:  Additional attributes

      Xref : String -> List Inline -> List String -> Inline

      Code : String -> Inline
         Embedded code.

   data Line : Type
      MkLine : (inlines : List Inline) ->
      length inlines > 0 = True => Line

B.1.2.  Module ComputerateSpecifying.BitDiagram

   data BitDiagram : List String -> Type
      Field : (name : String) -> (size : Nat) ->
      size > 0 && size * 2 > length name = True =>
      BitDiagram names -> elem name names = False =>
      BitDiagram (name :: names)





Petit-Huguenin            Expires 5 August 2021                [Page 72]


Internet-Draft           Computerate Specifying            February 2021


      Last : (name : String) -> (size : Nat) ->
      size > 0 && size * 2 > length name = True => BitDiagram [name]

   data Names : Type -> Type

   toAsciiDoc : BitDiagram names -> Block

   toDiagram : (t : Type) -> Names t -> BitDiagram _

B.1.3.  Module ComputerateSpecifying.BitVector

   (++) : BitVector n -> BitVector m -> BitVector (n + m)
      Concatene the second bit-vector after the first one.

   data Bit : Type
      O : Bit

      I : Bit

   data BitVector : Nat -> Type
      A vector of bit that can be pattern matched.

      Implements DecEq, Eq, Size.

      Nil : BitVector Z

      (::) : Bit -> BitVector n -> BitVector (S n)

   and : (1 _ : BitVector m) -> (1 _ : BitVector m) -> BitVector m
      Bitwise and between bit-vectors of identical size.

   bitVector : {m : Nat} -> BitVector m
      Build an empty bit-vector

   extend : (n : Nat) -> BitVector m -> BitVector (plus n m)
      Extend a bit-vector by n zero bits on the left side.

   extract : (p : Nat) -> (q : Nat) -> (prf1 : p LTE q) =>
   BitVector m -> (prf2 : q LTE m) => BitVector (q minus p)
      Extract a bit-vector.

      p:  The position of the first bit to extract.
      q:  The position of the next to last bit to extract.

   not : (1 _ : BitVector m) -> BitVector m
      Bitwise not of a bit-vector.

   or : (1 _ : BitVector m) -> (1 _ : BitVector m) -> BitVector m



Petit-Huguenin            Expires 5 August 2021                [Page 73]


Internet-Draft           Computerate Specifying            February 2021


      Bitwise or between bit-vectors of identical size.

   shiftL : (n : Nat) -> BitVector m -> (prf : n LTE m) =>
   BitVector (plus (minus m n) n)
      Shift the bit-vector to the left by n bits, inserting zeros.

   shiftR : (n : Nat) -> {m : Nat} -> BitVector m ->
   (prf : n LTE m) => BitVector (plus (minus m n) n)
      Shift the bit-vector to the right by n bits, inserting zeros.

   test : (1 m : Nat) -> (1 _ : BitVector n) -> (prf : m LT n) =>
   Bool
      Return a boolean that is True if the bit at position m is set.

   xor : (1 _ : BitVector m) -> (1 _ : BitVector m) -> BitVector m
      Bitwise xor between bit-vectors of identical size.

B.1.4.  Module ComputerateSpecifying.Dimension

   A module that defines types, constants and operations on denominate
   numbers.

   (*) : Denominate xs -> Denominate ys -> Denominate (merge' xs ys)
      The multiplication operation between denominate numbers.

   (+) : Denominate xs -> Denominate xs -> Denominate xs
      The addition operation between denominate numbers.

   (-) : Denominate xs -> Denominate xs -> Denominate xs
      The subtraction operation between denominate numbers.

   (/) : Denominate xs -> Denominate ys ->
   Denominate (merge' xs (recip' ys))
      The division operation between denominate numbers.

   Data : Type
      The type of a denominate number for the data dimension.

   data Denominate : List (Dimension, Int) -> Type
      A denominate number.

      MkDenominate : (x : Integer) -> (y : Integer) ->
      {xs : List (Dimension, Int)} -> Denominate xs
         Construct a denominate number as a fraction.

   Dimensionless : Type
      The type of a dimensionless denominate number




Petit-Huguenin            Expires 5 August 2021                [Page 74]


Internet-Draft           Computerate Specifying            February 2021


   interface Size a
      An interface to retrieve the size in bits of a type.

      Implemented by List, (s, x).

      size : a -> Data
         Return the size of a in bit.

   Time : Type
      The type of a denominate number for the time dimension.

   bit : Data
      Bit, the base unit of data.

   byte : Data
      The byte unit, as 8 bits.

   day : Time
      The day, as unit of time.

   fromDenominate : (value : Denominate xs) ->
   (unit : Denominate xs) -> (Double, Denominate xs)
      Convert a denominate number into a tuple made of the dimensionless
      value (as a "Double") calculated after applying a unit, and that
      unit.

      value:  the value to convert.
      unit:  the unit to use for the conversion.

   elaboration generate bin "bit" "Data"
      Generate all the IEC units based on the bit, from kibibit to
      yobibit.

   elaboration generate dec "bit" "Data"
      Generate all the SI units based on the bit, from kilobit to
      yottabit.

   elaboration generate si "second" "Time"
      Generates all the SI units based on the second, from yoctosecond
      to yottasecond.

   hour : Time
      The hour, as unit of time.

   minute : Time
      The minute, as unit of time.

   neg : Denominate xs -> Denominate xs



Petit-Huguenin            Expires 5 August 2021                [Page 75]


Internet-Draft           Computerate Specifying            February 2021


      The negation operation of a denominate number.

   none : Dimensionless
      The unit for a dimensionless denominate number.

   octa : Data
      The octa unit, as 64 bits.

   recip : Denominate xs -> Denominate (recip' xs)
      The reciprocal operation of a denominate number.

   second : Time
      Second, the base unit of time.

   tetra : Data
      The tetra unit, as 32 bits.

   wyde : Data
      The wyde unit, as 16 bits.

B.1.5.  Module ComputerateSpecifying.Tpn

   A module that defines types for Petri Net.

   Colour : Place -> Type
      Retrieve the type of token that can be stored in the place.

   data Input : Type
      MkInput : (place : Place) -> (output : Type) ->
      (inscription : Colour place -> ND output) -> Input
         An input arc.

         place:  The place from which tokens are removed.
         output:  The type of the token extracted.
         inscription:  A function that chooses and converts the tokens
            from the place.

   InputType : List Input -> Type
      Calculate the combined type of a list of inputs.

   MS : Type -> Type
      A multiset.

   ND : Type -> Type
      Non-determinism monad.

   data Output : Type




Petit-Huguenin            Expires 5 August 2021                [Page 76]


Internet-Draft           Computerate Specifying            February 2021


      MkOutput : (place : Place) -> (input : Type) ->
      (inscription : input -> MS (Colour place)) -> Output
         An output arc.

         place:  The place to which tokens are inserted.
         inscription:  a function that generates the tokens to be
            inserted in the place.

   OutputType : List Output -> Type
      Calculate the combined type of a list of outputs.

   data Place : Type
      MkPlace : String -> (colour : Type) ->
      (init : () -> MS colour) -> Place
         A place.

         colour:  The type of the tokens stored in the place.
         init:  A function to initialize the place.

   data Transition : Type
      MkTransition : (inputs : List Input) ->
      (outputs : List Output) ->
      (transition : InputType inputs -> ND (OutputType outputs)) ->
      Transition
         A transition.

         inputs:  The list of inputs.
         outputs:  The list of outputs.
         transition:  A function that chooses and converts between a
            tuple made of the type of all the inputs into a tuple made
            of the type of all the outputs.

   Types : List Type -> Type
      Convert a list of types into a tuple of types.

B.1.6.  Module ComputerateSpecifying.Transform

   A module to transform values structured as trees, with specialization
   to transform types via elaboration.

   data Path : Type
      A selection path

   add : (tree : a) -> (path : Path) -> (added : b) -> a
      Add a value as a sibling to values in a tree that are selected by
      a path.

      tree:  The tree to modify.



Petit-Huguenin            Expires 5 August 2021                [Page 77]


Internet-Draft           Computerate Specifying            February 2021


      path:  The path used to select the values.
      added:  The value to add

   extendRegistry : (registry : String) -> (codepoint : String) ->
   (type : Decl) -> IO (Provider ())
      Add a binding between a codepoint and a type in an extended
      registry

      registry:  The registry that needs to be extended.
      codepoint:  The codepoint to bind the type to.
      type:  The type associated with the codepoint

   registry : (registry : String) ->
   IO (Provider (List (String, Decl)))
      Retrieve an extended registry content, as a list of tuples made of
      a codepoint and a type.

      registry:  The registry to retrieve.

   remove : (tree : a) -> (path : Path) -> a
      Remove the values in a tree as selected by a path.

      tree:  The tree to modify.
      path:  The path used to select the values.

   replace : (tree : a) -> (path : Path) -> (replacement : b) -> a
      Replace values selected by a path on a tree.

      tree:  The tree to modify.
      path:  The path used to select the values.
      replacement:  The value to used as replacement.

B.1.7.  Module ComputerateSpecifying.Unsigned

   An unsigned number with a length.

   data Unsigned : (m : Nat) -> Type
      An unsigned integer is just a wrapper around a bit-vector of the
      same size.

      For sanity sake, this type always assumes that the value of a bit
      is 2 ^ m - 1, with m the size of the unsigned int.  In other words
      the first bit is the MSB, the last bit (the closer to Nil) is the
      LSB.

      Implements Num, Integral, Eq, Ord, Size.

      MkUnsigned : BitVector m -> Unsigned m



Petit-Huguenin            Expires 5 August 2021                [Page 78]


Internet-Draft           Computerate Specifying            February 2021


B.2.  Package rfc5234

   Version:  0.1
   Author(s):  Marc Petit-Huguenin

B.2.1.  Module RFC5234.Core

   The ABNF Core rules.

   alpha : Rule
      An ASCII alphabetic character.

   bit : Rule
      A "0" or "1" ASCII character.

   char : Rule
      Any ASCII character, starting at SOH and ending at DEL.

   cr : Rule
      A Carriage Return ASCII character.

   crlf : Rule
      A Carriage Return ASCII character, followed by the Line Feed ASCII
      character.

   ctl : Rule
      Any ASCII control character.

   digit : Rule
      Any ASCII digit.

   dquote : Rule
      A double-quote ASCII character.

   hexdig : Rule
      Any hexadecimal ASCII character, in lower and upper case.

   htab : Rule
      A Horizontal Tab ASCII character.

   lf : Rule
      A Line Feed ASCII character.

   lwsp : Rule
      A potentially empty string of space, horizontal tab, or line
      terminators, that last one followed by a space or horizontal tab.

   octet : Rule



Petit-Huguenin            Expires 5 August 2021                [Page 79]


Internet-Draft           Computerate Specifying            February 2021


      A 8-bit value.

   sp : Rule
      An ASCII space.

   vchar : Rule
      A printable ASCII character.

   wsp : Rule
      A potentially empty string of space, or horizontal tab.

B.2.2.  Module RFC5234.Main

   A module to generate a valid ABNF.

   data Form : Type
      Implements Show.

      TermName : String -> Form

      TermHex : Int -> List Int -> Form

      TermDec : Int -> List Int -> Form

      TermBin : Int -> List Int -> Form

      TermString : String -> Form

      Concat : Form -> Form -> List Form -> Form

      Altern : Form -> Form -> List Form -> Form

      TermHexRange : Int -> Int -> Form

      TermDecRange : Int -> Int -> Form

      TermBinRange : Int -> Int -> Form

      Group : Form -> Form

      Repeat : Maybe Int -> Maybe Int -> Form -> Form

      Optional : Form -> Form

   data Rule : Type
      An ABNF rule.

      Implements Show.



Petit-Huguenin            Expires 5 August 2021                [Page 80]


Internet-Draft           Computerate Specifying            February 2021


      Eq : (name : String) -> (form : Form) -> Rule
         Construct a rule.

      Inc : String -> Form -> Rule
         Construct an incremental rule.

   data Syntax : Type
      A list of rules.

      Implements Show.

      MkSyntax : List Rule -> Syntax

B.3.  Package augmented-ascii-diagrams

   Version:  0.1
   Author(s):  Marc Petit-Huguenin
   Dependencies:  rfc5234

B.3.1.  Module AAD.Main

   A module to generate augmented packet header diagrams.

   data BoolExpr : List Name -> Type
      A boolean expression

      Implements ShowPrec, Show.

      Equ : Expr xs -> Expr ys -> BoolExpr (xs ++ ys)

      Neq : Expr xs -> Expr ys -> BoolExpr (xs ++ ys)

      Gt : Expr xs -> Expr ys -> BoolExpr (xs ++ ys)

      Gte : Expr xs -> Expr ys -> BoolExpr (xs ++ ys)

      Lt : Expr xs -> Expr ys -> BoolExpr (xs ++ ys)

      Lte : Expr xs -> Expr ys -> BoolExpr (xs ++ ys)

      And : BoolExpr xs -> BoolExpr ys -> BoolExpr (xs ++ ys)

      Or : BoolExpr xs -> BoolExpr ys -> BoolExpr (xs ++ ys)

      Not : BoolExpr xs -> BoolExpr xs

   data Expr : List Name -> Type
      An expression



Petit-Huguenin            Expires 5 August 2021                [Page 81]


Internet-Draft           Computerate Specifying            February 2021


      Implements ShowPrec, Show.

      Val : Nat -> Expr []

      Var : (n : Name) -> Expr [n]

      Mul : Expr xs -> Expr ys -> Expr (xs ++ ys)

      Div : Expr xs -> Expr ys -> Expr (xs ++ ys)

      Mod : Expr xs -> Expr ys -> Expr (xs ++ ys)

      Exp : Expr xs -> Expr ys -> Expr (xs ++ ys)

      Add : Expr xs -> Expr ys -> Expr (xs ++ ys)

      Sub : Expr xs -> Expr ys -> Expr (xs ++ ys)

      ITE : BoolExpr xs -> Expr ys -> Expr zs ->
      Expr (xs ++ ys ++ zs)

   data Name : Type
      A name

      MkName : Maybe String -> String -> Name

B.4.  Package rfc791

   Version:  0.1
   Author(s):  Marc Petit-Huguenin
   Dependencies:  computerate-specifying

B.4.1.  Module RFC791.Address

   This module provides types for Internet Protocol Address.

   data IP : Type
      An IP address.

      Implements Size.

      A : (h : BitVector 1) -> h = [O] => (net : BitVector 7) ->
      (host : BitVector 24) -> IP
         A class A address.

      B : (h : BitVector 2) -> h = [I, O] => (net : BitVector 14) ->
      (host : BitVector 16) -> IP
         A class B address.



Petit-Huguenin            Expires 5 August 2021                [Page 82]


Internet-Draft           Computerate Specifying            February 2021


      C : (h : BitVector 3) -> h = [I, I, O] =>
      (net : BitVector 21) -> (host : BitVector 8) -> IP
         A class C address.

B.4.2.  Module RFC791.IP

   Types for the Internet Protocol.

   data Flags : Type
      Flags.

      Implements Size.

      MkFlags : (reserved : BitVector 1) -> reserved = bitVector =>
      (df : BitVector 1) -> (mf : BitVector 1) -> Flags

   data InternetHeader : Type
      Internet Protocol Header.

      Implements Size.

      MkInternetHeader : (version : BitVector 4) ->
      version = [O, I, O, O] => (ihl : (Unsigned 4, Data)) ->
      snd ihl = tetra => (tos : Tos) ->
      (length : (Unsigned 16, Data)) -> snd length = wyde =>
      (id : Unsigned 16) -> (flags : Flags) ->
      (offset : (Unsigned 13, Data)) -> snd offset = octa =>
      (ttl : (Unsigned 8, Time)) -> snd ttl = second =>
      (protocol : BitVector 16) -> (checksum : BitVector 16) ->
      (source : IP) -> (dest : IP) -> (options : List Option) ->
      (padding : BitVector n) -> InternetHeader

   data Option : Type
      Internet Protocol Header Options.

      Implements Size.

      Eoo : (flag : BitVector 1) -> flag = [O] =>
      (class : BitVector 2) -> class = [O, O] =>
      (number : BitVector 5) -> number = [O, O, O, O, O] => Option
         End of Options.

      Noop : (flag : BitVector 1) -> flag = [O] =>
      (class : BitVector 2) -> class = [O, O] =>
      (number : BitVector 5) -> number = [O, O, O, I, O] => Option
         No operation.





Petit-Huguenin            Expires 5 August 2021                [Page 83]


Internet-Draft           Computerate Specifying            February 2021


      Security : (flag : BitVector 1) -> flag = [I] =>
      (class : BitVector 2) -> class = [O, O] =>
      (number : BitVector 5) -> number = [O, O, O, I, O] =>
      (length : Unsigned 8) -> length = 11 => (s : BitVector 16) ->
      (c : BitVector 16) -> (h : BitVector 16) ->
      (tcc : BitVector 24) -> Option
         Security Option.

      Lssr : (flag : BitVector 1) -> flag = [I] =>
      (class : BitVector 2) -> class = [O, O] =>
      (number : BitVector 5) -> number = [O, O, O, I, I] =>
      (length : Unsigned 8) -> (pointer : Unsigned 8) ->
      pointer >= 4 = True => Option
         Loose Source and Record Route Option.

   data Tos : Type
      Type of Service

      Implements Size.

      MkTos : (precedence : Unsigned 3) -> (delay : BitVector 1) ->
      (throughput : BitVector 1) -> (reliability : BitVector 1) ->
      (reserved : BitVector 2) -> reserved = bitVector => Tos

   internetHeader : List Decl

Appendix C.  Errata Statistics

   In an effort to quantify the potential benefits of using formal
   methods at the IETF, an effort to relabel the Errata database is
   under way.

   The relabeling uses the following labels:


















Petit-Huguenin            Expires 5 August 2021                [Page 84]


Internet-Draft           Computerate Specifying            February 2021


        +==========+==============================================+
        | Label    | Description                                  |
        +==========+==============================================+
        | AAD      | Error in an ASCII bit diagram                |
        +----------+----------------------------------------------+
        | ABNF     | Error in an ABNF                             |
        +----------+----------------------------------------------+
        | Absent   | The errata was probably removed              |
        +----------+----------------------------------------------+
        | ASN.1    | Error in ASN.1                               |
        +----------+----------------------------------------------+
        | C        | Error in C code                              |
        +----------+----------------------------------------------+
        | Diagram  | Error in a generic diagram                   |
        +----------+----------------------------------------------+
        | Example  | An example does not match the normative text |
        +----------+----------------------------------------------+
        | Formula  | Error preventable by using Idris code        |
        +----------+----------------------------------------------+
        | FSM      | Error in a State machine                     |
        +----------+----------------------------------------------+
        | Ladder   | Error in a ladder diagram                    |
        +----------+----------------------------------------------+
        | Rejected | The erratum was rejected                     |
        +----------+----------------------------------------------+
        | Text     | Error in the text itself, no remedy          |
        +----------+----------------------------------------------+
        | TLS      | Error in the TLS language                    |
        +----------+----------------------------------------------+
        | XML      | Error in an XML Schema                       |
        +----------+----------------------------------------------+

                                  Table 1

   At the time of publication the first 1600 errata, which represents
   25.93% of the total, have been relabeled.  On these, 135 were
   rejected and 51 were deleted, leaving 1414 valid errata.














Petit-Huguenin            Expires 5 August 2021                [Page 85]


Internet-Draft           Computerate Specifying            February 2021


                     +=========+=======+============+
                     | Label   | Count | Percentage |
                     +=========+=======+============+
                     | Text    | 977   | 69.09%     |
                     +---------+-------+------------+
                     | Formula | 118   | 8.34%      |
                     +---------+-------+------------+
                     | Example | 112   | 7.92%      |
                     +---------+-------+------------+
                     | ABNF    | 71    | 5.02%      |
                     +---------+-------+------------+
                     | AAD     | 49    | 3.46%      |
                     +---------+-------+------------+
                     | ASN.1   | 40    | 2.82%      |
                     +---------+-------+------------+
                     | C       | 13    | 0.91%      |
                     +---------+-------+------------+
                     | FSM     | 13    | 0.91%      |
                     +---------+-------+------------+
                     | XML     | 12    | 0.84%      |
                     +---------+-------+------------+
                     | Diagram | 6     | 0.42%      |
                     +---------+-------+------------+
                     | TLS     | 2     | 0.14%      |
                     +---------+-------+------------+
                     | Ladder  | 1     | 0.07%      |
                     +---------+-------+------------+

                                 Table 2

   Note that as the relabeling is done in in order of erratum number, at
   this point it covers mostly older RFCs.  A change in tooling (e.g.
   ABNF verifiers) means that these numbers may drastically change as
   more errata are relabeled.  But at this point it seems that 31.89% of
   errata could have been prevented with a more pervasive use of formal
   methods.

Acknowledgements

   Thanks to Jim Kleck, Eric Petit-Huguenin, Nicolas Gironi, Stephen
   McQuistin, and Greg Skinner for the comments, suggestions, questions,
   and testing that helped improve this document and its associated
   tooling.

   Thanks to Ronald Tse and the Ribose team for the metanorma and
   relaton tools and their diligence in fixing bugs and implementing
   improvements.




Petit-Huguenin            Expires 5 August 2021                [Page 86]


Internet-Draft           Computerate Specifying            February 2021


Contributors

   Stephane Bryant

   Email: stephane.ml.bryant@gmail.com

Changelog

   draft-petithuguenin-computerate-specifying-05:

   *  Document:
      -  Update installation instructions for BitTorrent.
      -  Removed text related to the dat tool.
      -  Modifications following Stephane's review.
      -  Add XMPP address.

   *  Tooling:
      -  Fix idrisdoc when generating multiplicity.
      -  Upgrade asciidoctor to 2.0.12.
      -  Upgrade xml2rfc to 3.5.0.
      -  xml2rfc --validation option makes patch unnecessary.
      -  Upgrade metanorma (1.2.5) and dependencies.
      -  The tooling docker image is now distributed as a BitTorrent.
      -  Idnits upgraded to 2.16.05.

   *  Library:
      -  Use linear types in some BitVector functions.

   draft-petithuguenin-computerate-specifying-04:

   *  Document:
      -  Sections 2, 3, 4 and 5 have been completely reorganized,
         edited, and extended as a tutorial.
      -  New Terminology section.
      -  Add a new Standard Library section, that contains the
         description of all the Idris modules and external packages that
         will be available for developing specifications.
      -  Improve bibliography.
      -  Extend the CLI section to cover:
         o  New features.
         o  Bibliography templates.
         o  Complete bugs and TODO lists.
      -  Generate IdrisDoc of standard library packages and modules as a
         new appendix.
      -  Update errata stats.
      -  More compact changelog.
      -  Many modifications following Stephane's reviews.




Petit-Huguenin            Expires 5 August 2021                [Page 87]


Internet-Draft           Computerate Specifying            February 2021


   *  Tooling:
      -  Additional metanorma features:
         o  Generate json file.
      -  Various bug fixes in metanorma and relaton.
      -  Additional Idris2 features:
         o  Generate elaboration cache command.
         o  Elaboration cache implementation.
         o  IdrisDoc generation.
         o  Some TTImp types can carry comments.
         o  Quoted package names in ipkg.
         o  List dependencies.
         o  Package mapping.
         o  Faster literate processing.
      -  Idris2 wrapper to load local packages.
      -  New include processor to generate IdrisDoc.
      -  Process multiple fragments on each line.
      -  Add support for asciidoctor outputs, including revealjs and
         diagrams.
      -  Embedding code must now return a value that implements "Show".
         String values are then stripped of their first and last double-
         quotes.
      -  Fix bug where transcluded text is converted into ASCII art.
      -  Embedded code in examples in lidr files can now be escaped with
         "\".
      -  Replace Idris with Idris2 version 0.2.1.
      -  Update metanorma to 1.1.4.
      -  Update metanorma-ietf to 2.2.2.
      -  Update xml2rfc to 3.0.0.
      -  Downgrade idnits to 2.16.04.
      -  Decommission the Docker image in dat://78f80c850af509e0cd3fd7bd
         6f5d0dd527a861d783e05574bbd040f0502da3c6.

   *  Library:
      -  Decommission the RFC 5234 library for complete rewrite.

   draft-petithuguenin-computerate-specifying-03:

   *  Document:
      -  Notes are now correctly displayed.
      -  Add "Implementations Oriented Standards" section.
      -  Add "Extended Registries" section and appendix.
      -  Add paragraph about hierarchical petri nets.
      -  Convert "Verified Code" section into a top level section, and
         expand it.
      -  Add "Implementation-Oriented Standards" section.

   *  Tooling:
      -  Many bug fixes in metanorma-ietf.



Petit-Huguenin            Expires 5 August 2021                [Page 88]


Internet-Draft           Computerate Specifying            February 2021


      -  Update xml2rfc to 2.40.1.
      -  Rebuilding text for an RFC with xml2rfc now uses pagination.
      -  Update metanorma-ietf to version 2.0.5.
      -  The "computerate" command can directly generate PDF files.
      -  Add support in xml2rfc for generating PDF files.
      -  Add asciidoctor-revealjs.
      -  Update metanorma to version 1.0.0.
      -  Update metanorma-cli to version 1.2.10.1.

   *  Library:
      -  No update

   draft-petithuguenin-computerate-specifying-02:

   *  Document
      -  Switch to rfcxml3.
      -  Status is now experimental.
      -  Many nits.
      -  Fix incorrect errata stats.
      -  Move acknowledgment section at the end.
      -  Rewrite the APHD section (formerly known as AAD) to match
         draft-mcquistin-augmented-diagrams-01.
      -  Fix non-ascii characters in the references.
      -  Intermediate AsciiDoc representation for serializers.

   *  Tooling
      -  xmlrfc3 is now the default extension.
      -  "docName" and "category" attributes are now generated, and the
         "prepTime" is removed.
      -  Update xml2rfc to 2.35.0.
      -  Remove LanguageTool.
      -  Update Metanorma to version 0.3.17.
      -  Update Asciidoctor to 2.0.10.
      -  Update list of Working Groups.

   *  Library
      -  No update.

   draft-petithuguenin-computerate-specifying-01:

   *  Document
      -  New changelog appendix.
      -  Fix incorrect reference, formatting in Idris code.
      -  Add option to remove container in all "docker run" command.
      -  Add explanations to use the Idris REPL and VIM inside the
         Docker image.
      -  Add placeholders for ASN.1 and RELAX NG languages.
      -  New Errata appendix.



Petit-Huguenin            Expires 5 August 2021                [Page 89]


Internet-Draft           Computerate Specifying            February 2021


      -  Nits.
      -  Improve Syntax Examples section.

   *  Tooling
      -  Update Metanorma to version 0.3.16
      -  Update MetaNorma-cli to version 1.2.7.1
      -  Switch to patched version of Idris 1.3.2 that supports remote
         REPL in Docker.
      -  Add VIM and idris-vim extension.
      -  Remove some debug statements.

   *  Library
      -  No update

Author's Address

   Marc Petit-Huguenin
   Impedance Mismatch LLC

   Email: marc@petit-huguenin.org
   URI:   hallway@jabber.ietf.org/MPH






























Petit-Huguenin            Expires 5 August 2021                [Page 90]


Html markup produced by rfcmarkup 1.129d, available from https://tools.ietf.org/tools/rfcmarkup/