Skip to main content

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

The information below is for an old version of the document.
Document Type
This is an older version of an Internet-Draft whose latest revision state is "Replaced".
Author Marc Petit-Huguenin
Last updated 2021-11-07
Replaced by draft-petithuguenin-computerate-specification
RFC stream (None)
Formats
Stream Stream state (No stream defined)
Consensus boilerplate Unknown
RFC Editor Note (None)
IESG IESG state I-D Exists
Telechat date (None)
Responsible AD (None)
Send notices to (None)
draft-petithuguenin-computerate-specifying-15
Network Working Group                                  M. Petit-Huguenin
Internet-Draft                                    Impedance Mismatch LLC
Intended status: Experimental                            7 November 2021
Expires: 11 May 2022

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

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 11 May 2022.

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 11 May 2022                  [Page 1]
Internet-Draft           Computerate Specifying            November 2021

Table of Contents

   1.  Introduction  . . . . . . . . . . . . . . . . . . . . . . . .   5
   2.  Overview  . . . . . . . . . . . . . . . . . . . . . . . . . .   6
   3.  Terminology . . . . . . . . . . . . . . . . . . . . . . . . .   7
   4.  Private Specifications  . . . . . . . . . . . . . . . . . . .   8
     4.1.  Private Specifications for New Documents  . . . . . . . .  10
     4.2.  Private Specifications for Existing Documents . . . . . .  11
   5.  Self-Contained Specifications . . . . . . . . . . . . . . . .  13
     5.1.  PDU Descriptions  . . . . . . . . . . . . . . . . . . . .  13
       5.1.1.  PDU Examples  . . . . . . . . . . . . . . . . . . . .  13
       5.1.2.  Calculations from PDU . . . . . . . . . . . . . . . .  16
       5.1.3.  PDU Representations . . . . . . . . . . . . . . . . .  17
     5.2.  State Machines  . . . . . . . . . . . . . . . . . . . . .  17
     5.3.  Proofs  . . . . . . . . . . . . . . . . . . . . . . . . .  19
       5.3.1.  Wire Type vs Semantic Type  . . . . . . . . . . . . .  20
       5.3.2.  Data Format Conversion  . . . . . . . . . . . . . . .  22
       5.3.3.  Postel's Law  . . . . . . . . . . . . . . . . . . . .  23
       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  . . . . . . . . . . . . . . . . . .  33
         6.1.4.1.  Building a Typed Petri Net  . . . . . . . . . . .  34
         6.1.4.2.  Adding Time to a Typed Petri Net  . . . . . . . .  37
         6.1.4.3.  Verifying a Typed Petri Net . . . . . . . . . . .  38
         6.1.4.4.  Deriving a Type from a Typed Petri Net  . . . . .  39
       6.1.5.  Representations . . . . . . . . . . . . . . . . . . .  40
         6.1.5.1.  Bit Diagrams  . . . . . . . . . . . . . . . . . .  41
         6.1.5.2.  Message Sequence Charts . . . . . . . . . . . . .  42
     6.2.  Packages for Meta-Languages . . . . . . . . . . . . . . .  43
       6.2.1.  Meta-languages Defined in RFCs  . . . . . . . . . . .  46
         6.2.1.1.  Routing Policy Specification Language next
                 generation (RPSLng) . . . . . . . . . . . . . . . .  46
         6.2.1.2.  External Data Representation Standard (XDR) . . .  46
         6.2.1.3.  Formal Notation for RObust Header Compression
                 (ROHC-FN) . . . . . . . . . . . . . . . . . . . . .  46
         6.2.1.4.  Abstract Syntax Notation X (ASN.X)  . . . . . . .  46
         6.2.1.5.  Augmented BNF (ABNF)  . . . . . . . . . . . . . .  46
         6.2.1.6.  Routing Backus-Naur Form (RBNF) . . . . . . . . .  48
         6.2.1.7.  Data Modeling Language (YANG) . . . . . . . . . .  48
         6.2.1.8.  Concise Data Definition Language (CDDL) . . . . .  49
         6.2.1.9.  Structured Field Values for HTTP  . . . . . . . .  49
       6.2.2.  Externally Defined Meta-languages . . . . . . . . . .  49

Petit-Huguenin             Expires 11 May 2022                  [Page 2]
Internet-Draft           Computerate Specifying            November 2021

       6.2.3.  Ad-hoc Meta-languages . . . . . . . . . . . . . . . .  49
       6.2.4.  Draft Meta-Languages  . . . . . . . . . . . . . . . .  49
         6.2.4.1.  Augmented Packet Header Diagrams (APHD) . . . . .  49
         6.2.4.2.  Cosmogol  . . . . . . . . . . . . . . . . . . . .  51
     6.3.  Packages for Protocols  . . . . . . . . . . . . . . . . .  51
       6.3.1.  Type Transformations  . . . . . . . . . . . . . . . .  52
       6.3.2.  Codepoint Registries  . . . . . . . . . . . . . . . .  55
   7.  Exporting Specifications  . . . . . . . . . . . . . . . . . .  56
   8.  Standard Library  . . . . . . . . . . . . . . . . . . . . . .  58
     8.1.  Internal Modules  . . . . . . . . . . . . . . . . . . . .  58
       8.1.1.  Metanorma.Ietf  . . . . . . . . . . . . . . . . . . .  58
       8.1.2.  BitVector . . . . . . . . . . . . . . . . . . . . . .  59
       8.1.3.  Unsigned  . . . . . . . . . . . . . . . . . . . . . .  59
       8.1.4.  Dimension . . . . . . . . . . . . . . . . . . . . . .  60
       8.1.5.  BitDiagram  . . . . . . . . . . . . . . . . . . . . .  61
       8.1.6.  Transform . . . . . . . . . . . . . . . . . . . . . .  62
       8.1.7.  Tpn . . . . . . . . . . . . . . . . . . . . . . . . .  62
         8.1.7.1.  Building a TPN  . . . . . . . . . . . . . . . . .  62
         8.1.7.2.  Verifying a TPN . . . . . . . . . . . . . . . . .  65
         8.1.7.3.  Deriving a Type From a TPN  . . . . . . . . . . .  65
     8.2.  Meta-Language Packages  . . . . . . . . . . . . . . . . .  66
       8.2.1.  RFC 5234 (ABNF) . . . . . . . . . . . . . . . . . . .  66
         8.2.1.1.  Building an ABNF  . . . . . . . . . . . . . . . .  66
         8.2.1.2.  Generating and Verifying ABNF specifications  . .  67
         8.2.1.3.  Common Rules  . . . . . . . . . . . . . . . . . .  67
       8.2.2.  Augmented Packet Header Diagrams (APHD) . . . . . . .  67
     8.3.  Protocol Packages . . . . . . . . . . . . . . . . . . . .  68
       8.3.1.  RFC 791 (Internet Protocol) . . . . . . . . . . . . .  68
   9.  Informative References  . . . . . . . . . . . . . . . . . . .  68
   Appendix A.  Command Line Tools . . . . . . . . . . . . . . . . .  73
     A.1.  Installation  . . . . . . . . . . . . . . . . . . . . . .  73
     A.2.  Authoring a Computerate Specification . . . . . . . . . .  74
       A.2.1.  Using the Templates . . . . . . . . . . . . . . . . .  75
       A.2.2.  Converting an xml2rfc Document  . . . . . . . . . . .  75
       A.2.3.  Bibliography  . . . . . . . . . . . . . . . . . . . .  75
         A.2.3.1.  Build a Bibliography with Zotero  . . . . . . . .  75
         A.2.3.2.  Build a Bibliography Manually . . . . . . . . . .  76
     A.3.  Processing a Computerate Specification  . . . . . . . . .  76
       A.3.1.  Outputs . . . . . . . . . . . . . . . . . . . . . . .  77
     A.4.  Other Commands  . . . . . . . . . . . . . . . . . . . . .  77
     A.5.  Modified Tools  . . . . . . . . . . . . . . . . . . . . .  78
       A.5.1.  Idris2  . . . . . . . . . . . . . . . . . . . . . . .  78
       A.5.2.  asciidoctor . . . . . . . . . . . . . . . . . . . . .  78
       A.5.3.  metanorma . . . . . . . . . . . . . . . . . . . . . .  78
       A.5.4.  metanorma-ietf  . . . . . . . . . . . . . . . . . . .  79
       A.5.5.  mnconvert . . . . . . . . . . . . . . . . . . . . . .  79
       A.5.6.  xml2rfc . . . . . . . . . . . . . . . . . . . . . . .  79
       A.5.7.  idris2-vim  . . . . . . . . . . . . . . . . . . . . .  79

Petit-Huguenin             Expires 11 May 2022                  [Page 3]
Internet-Draft           Computerate Specifying            November 2021

     A.6.  Bugs and Workarounds  . . . . . . . . . . . . . . . . . .  80
     A.7.  TODO List . . . . . . . . . . . . . . . . . . . . . . . .  80
   Appendix B.  API Documentation  . . . . . . . . . . . . . . . . .  81
     B.1.  Package computerate-specifying  . . . . . . . . . . . . .  81
       B.1.1.  Module ComputerateSpecifying  . . . . . . . . . . . .  81
       B.1.2.  Module ComputerateSpecifying.BitDiagram . . . . . . .  81
       B.1.3.  Module ComputerateSpecifying.BitVector  . . . . . . .  82
       B.1.4.  Module ComputerateSpecifying.Dimension  . . . . . . .  83
       B.1.5.  Module ComputerateSpecifying.Metanorma.Ietf . . . . .  86
       B.1.6.  Module ComputerateSpecifying.Tpn  . . . . . . . . . .  90
       B.1.7.  Module ComputerateSpecifying.Unsigned . . . . . . . .  95
     B.2.  Package rfc5234 . . . . . . . . . . . . . . . . . . . . .  96
       B.2.1.  Module RFC5234  . . . . . . . . . . . . . . . . . . .  96
     B.3.  Package augmented-ascii-diagrams  . . . . . . . . . . . .  99
       B.3.1.  Module APHD . . . . . . . . . . . . . . . . . . . . . 100
     B.4.  Package rfc791  . . . . . . . . . . . . . . . . . . . . . 100
       B.4.1.  Module RFC791.Address . . . . . . . . . . . . . . . . 100
       B.4.2.  Module RFC791.IP  . . . . . . . . . . . . . . . . . . 100
   Appendix C.  Errata Statistics  . . . . . . . . . . . . . . . . . 102
   Appendix D.  Converting From a Colored Petri Net  . . . . . . . . 104
     D.1.  Convert Color Sets  . . . . . . . . . . . . . . . . . . . 105
       D.1.1.  Simple Color Sets . . . . . . . . . . . . . . . . . . 105
         D.1.1.1.  Unit Color Sets . . . . . . . . . . . . . . . . . 105
         D.1.1.2.  Boolean Color Sets  . . . . . . . . . . . . . . . 105
         D.1.1.3.  Integer Color Sets  . . . . . . . . . . . . . . . 106
         D.1.1.4.  Large Integer Color Sets  . . . . . . . . . . . . 106
         D.1.1.5.  Real Color Sets . . . . . . . . . . . . . . . . . 106
         D.1.1.6.  String Color Sets . . . . . . . . . . . . . . . . 107
         D.1.1.7.  Enumerated Color Sets . . . . . . . . . . . . . . 107
         D.1.1.8.  Index Color Sets  . . . . . . . . . . . . . . . . 107
       D.1.2.  Compound Color Sets . . . . . . . . . . . . . . . . . 108
         D.1.2.1.  Product Color Sets  . . . . . . . . . . . . . . . 108
         D.1.2.2.  Record Color Sets . . . . . . . . . . . . . . . . 108
         D.1.2.3.  List Color Sets . . . . . . . . . . . . . . . . . 108
         D.1.2.4.  Union Color Sets  . . . . . . . . . . . . . . . . 109
         D.1.2.5.  Subset Color Sets . . . . . . . . . . . . . . . . 109
         D.1.2.6.  Alias Color Sets  . . . . . . . . . . . . . . . . 109
       D.1.3.  Timed Color Sets  . . . . . . . . . . . . . . . . . . 109
       D.1.4.  Size of Color Sets  . . . . . . . . . . . . . . . . . 110
     D.2.  Convert Places  . . . . . . . . . . . . . . . . . . . . . 110
     D.3.  Convert Transitions . . . . . . . . . . . . . . . . . . . 111
       D.3.1.  Convert Arcs  . . . . . . . . . . . . . . . . . . . . 111
         D.3.1.1.  Convert Free Variables  . . . . . . . . . . . . . 111
         D.3.1.2.  Convert Input Arcs  . . . . . . . . . . . . . . . 111
         D.3.1.3.  Convert Inhibitor Arcs  . . . . . . . . . . . . . 112
         D.3.1.4.  Convert Reset Arcs  . . . . . . . . . . . . . . . 112
         D.3.1.5.  Convert Output Arcs . . . . . . . . . . . . . . . 112
       D.3.2.  Convert Transition Inscription  . . . . . . . . . . . 113

Petit-Huguenin             Expires 11 May 2022                  [Page 4]
Internet-Draft           Computerate Specifying            November 2021

         D.3.2.1.  Unification . . . . . . . . . . . . . . . . . . . 113
         D.3.2.2.  Guards  . . . . . . . . . . . . . . . . . . . . . 114
     D.4.  Convert Substitution Transitions  . . . . . . . . . . . . 114
     D.5.  Convert Fusion Places . . . . . . . . . . . . . . . . . . 115
   Appendix E.  Evidence-Based Answers . . . . . . . . . . . . . . . 115
     E.1.  Encoding Questions  . . . . . . . . . . . . . . . . . . . 116
       E.1.1.  Any Value of a Type is Evidence of Yes  . . . . . . . 117
       E.1.2.  Function Type As Implication  . . . . . . . . . . . . 118
       E.1.3.  Polymorphism  . . . . . . . . . . . . . . . . . . . . 120
       E.1.4.  Empty Type as No  . . . . . . . . . . . . . . . . . . 120
       E.1.5.  Sloppy Questions  . . . . . . . . . . . . . . . . . . 122
       E.1.6.  Product Type  . . . . . . . . . . . . . . . . . . . . 122
       E.1.7.  Sum Type  . . . . . . . . . . . . . . . . . . . . . . 123
       E.1.8.  Inductive Type  . . . . . . . . . . . . . . . . . . . 123
       E.1.9.  Pi Type . . . . . . . . . . . . . . . . . . . . . . . 124
       E.1.10. Sigma Type  . . . . . . . . . . . . . . . . . . . . . 124
       E.1.11. Equality Type . . . . . . . . . . . . . . . . . . . . 124
       E.1.12. Decidable Type  . . . . . . . . . . . . . . . . . . . 124
     E.2.  How to Find Evidence  . . . . . . . . . . . . . . . . . . 124
   Appendix F.  A Distributed Package Manager for Computerate
           Specifications  . . . . . . . . . . . . . . . . . . . . . 124
     F.1.  Distributed Source Repositories . . . . . . . . . . . . . 125
       F.1.1.  The "gits" Protocol . . . . . . . . . . . . . . . . . 125
       F.1.2.  The "mgit" and "mgits" Protocols  . . . . . . . . . . 125
       F.1.3.  Git Submodules as Dependencies  . . . . . . . . . . . 126
     F.2.  Distributed Artifact Manager  . . . . . . . . . . . . . . 127
       F.2.1.  Reproducible Build  . . . . . . . . . . . . . . . . . 127
       F.2.2.  Distributed Cache . . . . . . . . . . . . . . . . . . 127
     F.3.  Recursive Build . . . . . . . . . . . . . . . . . . . . . 128
       F.3.1.  Indexing Commits  . . . . . . . . . . . . . . . . . . 128
       F.3.2.  Building a Submodule  . . . . . . . . . . . . . . . . 128
       F.3.3.  Pinned Down Builds  . . . . . . . . . . . . . . . . . 129
   Appendix G.  Git Layout for Computerate Specifications  . . . . . 129
   Acknowledgements  . . . . . . . . . . . . . . . . . . . . . . . . 131
   Contributors  . . . . . . . . . . . . . . . . . . . . . . . . . . 131
   Changelog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
   Author's Address  . . . . . . . . . . . . . . . . . . . . . . . . 139

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.

Petit-Huguenin             Expires 11 May 2022                  [Page 5]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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.

Petit-Huguenin             Expires 11 May 2022                  [Page 6]
Internet-Draft           Computerate Specifying            November 2021

   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,
   Appendix B contains the reference manual for the standard library,
   Appendix D explains how to convert Colored Petri Nets in a form that
   can be used in specifications, Appendix E is a tutorial on using
   Programs and Types to prove propositions, Appendix F explains the
   distributed architecture of the standard library, and Appendix G
   describes the format of the files distributed in 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.

   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.

   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.

Petit-Huguenin             Expires 11 May 2022                  [Page 7]
Internet-Draft           Computerate Specifying            November 2021

   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".

   "Metanorma" is a trademark of Ribose Inc.

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 xml2rfc 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.

   The code in a computerate specification uses the programming language
   [Idris2] in literate programming [Knuth92] 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 in
   either a "code:[]" or a "code::[]" macro.  That code fragment must
   return a value of a type that implements respectively the "Show" or
   the "Pretty" 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.

Petit-Huguenin             Expires 11 May 2022                  [Page 8]
Internet-Draft           Computerate Specifying            November 2021

   2.  For each instance of a code macro, evaluates that fragment and
       replaces it 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]:

      > 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 code:[a1]ms, requests would be
      sent at times code:[a2].
      If the client has not received a response after code:[a3] ms, the
      client will consider the transaction to have timed out.

   is rendered as

Petit-Huguenin             Expires 11 May 2022                  [Page 9]
Internet-Draft           Computerate Specifying            November 2021

   "                                            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 1

   The Idris2 programming language has been chosen because its type
   system supports dependent and linear types [Brady17], 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.

Petit-Huguenin             Expires 11 May 2022                 [Page 10]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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 were made
   easier to implement because they follow the order a software
   developer will develop each component.

   Idris package description files can also be used in literate mode by
   using the ".lipkg" extension and using the ">" character at the
   beginning of each line that contains package syntax.  This permits to
   merge the top AsciiDoc document (which contains mostly includes of
   various sections written either as AsciiiDoc or literate documents)
   with the package description.

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 either done manually, or by using the "mnconvert" program
   distributed with the tooling (Appendix A.4).  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.

Petit-Huguenin             Expires 11 May 2022                 [Page 11]
Internet-Draft           Computerate Specifying            November 2021

   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
   copied.  The ifdef/endif directives prevents the text to be displayed
   there:

       ifdef::never[]
       // tag::para1[]

       Text that describes a functionality

       // end::para1[]
       endif::never[]

       > -- Code that implements that functionality.

   Then a self-include can insert the text inside the tags to a
   different place, without changing the order of the Idris code:

       include::Main.adoc[tag=para1]

   Another use for self-inclusion is to insert Idris code in an example
   or code block.  To do that, add the code directly as code in the
   source, and then self-include it in the block.  This guarantees that
   the example is always typechecked.  In that case the ">" character at
   the beginning of each lines is automatically escaped.

       > -- tag::proof[]
       > total currying : ((a, b) -> c) -> (a -> b -> c)
       > currying f = \x => \y => f (x, y)
       > -- end::proof[]

       ----
       include::MyFile.lidr[tag=proof]
       ----

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 12]
Internet-Draft           Computerate Specifying            November 2021

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.

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 13]
Internet-Draft           Computerate Specifying            November 2021

   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.

      > 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

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 14]
Internet-Draft           Computerate Specifying            November 2021

   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.

      > example1 : InternetHeader
      > example1 = MkInternetHeader 4 5 0 21 111 0 0 123 1

   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.

      example1' : InternetHeader
      example1' = MkInternetHeader 6 5 0 21 111 0 0 123 1

   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].

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

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 15]
Internet-Draft           Computerate Specifying            November 2021

   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.

       ....
       code::[example1]
       ....

   will generate the equivalent AsciiDoc text:

      ....
       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 |
      +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
      ....

   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 11 May 2022                 [Page 16]
Internet-Draft           Computerate Specifying            November 2021

      Note that the minimum value for a correct header is
      is code:\[sizeHeader `div` ihlUnit].

      > sizeHeader : Int
      > sizeHeader = 20

      > ihlUnit : Int
      > ihlUnit = 4

   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.

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.

Petit-Huguenin             Expires 11 May 2022                 [Page 17]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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

Petit-Huguenin             Expires 11 May 2022                 [Page 18]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 19]
Internet-Draft           Computerate Specifying            November 2021

5.3.1.  Wire Type vs Semantic 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
   types that are more abstract.  We call the former Wire Types, and the
   latter Semantic 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 semantic type:

Petit-Huguenin             Expires 11 May 2022                 [Page 20]
Internet-Draft           Computerate Specifying            November 2021

      > 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'

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

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

Petit-Huguenin             Expires 11 May 2022                 [Page 21]
Internet-Draft           Computerate Specifying            November 2021

   *  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:

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

   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.

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.

Petit-Huguenin             Expires 11 May 2022                 [Page 22]
Internet-Draft           Computerate Specifying            November 2021

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

      isXmlAndJsonSame: Iso (XML, DeltaXML) (JSON, DeltaJson)
        ...

   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.

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 23]
Internet-Draft           Computerate Specifying            November 2021

   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):

      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]

   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.

   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:

Petit-Huguenin             Expires 11 May 2022                 [Page 24]
Internet-Draft           Computerate Specifying            November 2021

      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

   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 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.

Petit-Huguenin             Expires 11 May 2022                 [Page 25]
Internet-Draft           Computerate Specifying            November 2021

   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,

   *  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

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 26]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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).

Petit-Huguenin             Expires 11 May 2022                 [Page 27]
Internet-Draft           Computerate Specifying            November 2021

   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.

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:

      > example : InternetHeader -> Block
      > example ih = ?example_rhs

      code::[example example1]

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

Petit-Huguenin             Expires 11 May 2022                 [Page 28]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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 xml2rfc v3 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

Petit-Huguenin             Expires 11 May 2022                 [Page 29]
Internet-Draft           Computerate Specifying            November 2021

      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
      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:

      > data InternetHeader : Type where
      >   MkInternetHeader :
      >     (version : BitVector 4) -> version = [O, I, O, O] =>
      >     (ihl : (Unsigned 4, Info)) -> snd ihl = Dimension.tetra =>
      >     (tos : Tos) ->
      >     (length : (Unsigned 16, Info)) ->
      >       snd length = Dimension.wyde =>
      >     (id : Unsigned 16) ->
      >     (flags : Flags) ->
      >     (offset : (Unsigned 13, Info)) ->
      >       snd offset = Dimension.octa =>
      >     (ttl : (Unsigned 8, Time)) -> snd ttl = Dimension.second =>
      >     (protocol : BitVector 16) ->
      >     (checksum : BitVector 16) ->
      >     (source : IP) ->
      >     (dest : IP) ->
      >     (options : List Option) ->
      >     (padding : BitVector n) ->
      >       n = pad 32 options => padding = bitVector {m=n} =>
      >     InternetHeader

   version:  This is bit-vector, but it always contains the same value,

Petit-Huguenin             Expires 11 May 2022                 [Page 30]
Internet-Draft           Computerate Specifying            November 2021

      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
      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.

   We can constrain the size of a field, like is done for the "padding"
   field above.  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".

Petit-Huguenin             Expires 11 May 2022                 [Page 31]
Internet-Draft           Computerate Specifying            November 2021

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

   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.

   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":

      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

Petit-Huguenin             Expires 11 May 2022                 [Page 32]
Internet-Draft           Computerate Specifying            November 2021

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:

      Size InternetHeader where
        size (MkInternetHeader version ihl tos length id flags offset
          ttl protocol checksum source dest options padding) =
            size version + size ihl +
            ...
            size padding

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

      > 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
      code:[fromDenominate minHeader tetra]

6.1.4.  Typed Petri Nets

   |  Never send a human to do a machine's job.
   |  
   |  -- Agent Smith in The Matrix (1999)

   A better solution than defining an adhoc type for our state machines,
   as explained in Section 5.2, is to use Petri Nets.

Petit-Huguenin             Expires 11 May 2022                 [Page 33]
Internet-Draft           Computerate Specifying            November 2021

   Concurrent systems can be represented using two different families of
   techniques, algebraic and graphical.  Algebraic techniques (e.g.,
   process calculi) are mathematically well-defined, but lack an
   intuitive representation that would be useful to developers not
   completely familiar with these techniques.

   On the other hand, graphical representations of concurrent systems
   (e.g., state machines) can be understood by a larger segment of
   developers, but generally lack a standardized and/or mathematical
   definition.

   Petri Nets are at the intersection of these two techniques.  They are
   typically graphical representations of concurrent processes, but are
   based on a well-defined mathematical theory.  One way to look at
   Petri Nets is as a way to group multiple state machines together.  A
   Petri Net also 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 (which can be
   seen as a way to group multiple Markov chains together).

   A Typed Petri Net (TPN) is an algebraic specification of a Petri Net,
   such as it can be expressed as an Idris value, and be easily reused
   for various purposes.  TPNs are based on Colored Petri Nets, as
   defined in [Jensen09] and [Aalst11].  [Jensen07] is a shorter
   introduction to Colored Petri Net that should be read first.
   Particularly, section 2 contains the various definition of the
   terminology that is used in this document, augmented as follow:

   *  The word Color is used instead of the word Colour.

   *  _unification_ is defined in the middle of the left column of page
      6.

   *  _free variable_ is defined in the middle of the right column of
      page 6.

   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 a TPN can also be designed so
   each part of the protocol is defined separately from the others,
   making it a Hierarchical TPN.

6.1.4.1.  Building a Typed Petri Net

   The following example of TPN is converted from Figure 7 in
   [Jensen07]:

Petit-Huguenin             Expires 11 May 2022                 [Page 34]
Internet-Draft           Computerate Specifying            November 2021

      > No : Type
      > No = Int

      > Data : Type
      > Data = String

      > NoxData : Type
      > NoxData = (No, Data)

      > namespace Sender
      >   export
      >   sender : Module [NoxData, NoxData, No] ()
      >   sender = do
      >     packetsToSend <- port "Packets To Send" NoxData Both
      >     nextSend <- place "NextSend" No {init=pure 1}
      >     a <- port "A" NoxData Out
      >     d <- port "D" No In
      >     transition "Send Packet"
      >       [input packetsToSend (No, Data) one,
      >        input nextSend No one]
      >       [(0, 0, 1, 0)]
      >       [output (No, Data) packetsToSend pure,
      >        output No nextSend pure,
      >        output (No, Data) a pure]
      >       (\((n, d), n') => pure ((n, d), n, (n, d)))
      >     transition "Receive Ack"
      >       [input nextSend No one,
      >        input d No one]
      >       empty
      >       [output No nextSend pure]
      >       (pure . snd)

   Similarly, the following example of TPN is converted from Figure 11
   in [Jensen07]:

Petit-Huguenin             Expires 11 May 2022                 [Page 35]
Internet-Draft           Computerate Specifying            November 2021

      > namespace Protocol
      >   export
      >   protocol : Top
      >   protocol = top $ do
      >     packetsToSend <- place "Packets To Send" NoxData
      >       {init=[(1, "COL"), (2, "OUR"), (3, "ED "), (4, "PET"),
      >       (5, "RI "), (6, "NET")]}
      >     dataReceived <- place "Data Received" Data {init=pure ""}
      >     a <- place "A" NoxData
      >     b <- place "B" NoxData
      >     c <- place "C" No
      >     d <- place "D" No
      >     instance "" sender [packetsToSend, a, d]
      >     instance "" network [a, b, c, d]
      >     instance "" receiver [dataReceived, b, c]

   In these examples, the "place", "port", "input", "output",
   "transition", and "instance" functions are the combinators used to
   define Typed Petri Net modules in computerate specifications and are
   described in Section 8.1.7.

   TPN modules are written as constants of type "Module xs ()", which is
   a Monad used to implement a deep embedded DSL.  The Monad ensures
   that places, ports and instances all have a unique name inside a
   module.  It also ensures that all places and ports used by
   transitions and instances are declared in the same module.  Finally
   it ensures that all ports exported by a module are correctly mapped
   to a local place or port when imported as an instance.

   Ultimately these combinators are not meant to be used as a way to
   directly design a TPN, as doing this is very tedious and error-prone.
   Instead the general advice is to use the graphical tool cpntools
   [Cpntools] to design a CPN and then to follow the step-by-step
   tutorial in Appendix D to convert it into a Typed Petri Net.
   Experience shows that, even for the simplest of protocols,
   systematically starting formalization by 1) designing a complete
   semantic type and 2) designing a top-level Petri Net, both in
   cpntools, is the most efficient way to proceed.

Petit-Huguenin             Expires 11 May 2022                 [Page 36]
Internet-Draft           Computerate Specifying            November 2021

      |  NOTE: It is planned to add to the tooling a graphical tool on
      |  top of TPN that will replace cpntools, which is starting to
      |  show its age.  To do so each combinator will be enhanced with
      |  values that contains the graphical properties (position, size,
      |  color,...) that the graphical tool will use to display a TPN.
      |  Conversely the graphical tool will be designed to modify these
      |  properties in the source code in response to a user interface
      |  action, like moving or resizing a place, port, transition or
      |  instance.  This will permit to continue to use the computerate
      |  specification as the storage format for a TPN, including its
      |  graphical representation.

6.1.4.2.  Adding Time to a Typed Petri Net

   Timed TPN are built by using Timed tokens (which are types wrapped
   into the "Timed" type) and by adding delays in transitions and arcs.

   The following is an example of an implementation in CPN of a timer,
   here that will timeout after 100 units of time:

                 _____
   +-------+ () /     \ () +-------+
   | start |-->| State |-->| stop  |
   | timer |    \     /    | timer |
   +-------+     `---'     +-------+
      |            | ()        ^
      |            V           |
      |       +---------+      |
      |       | timeout |      | ()@+100
      |       +---------+      |
      |            ^           |
      | ()@+100    | ()        |
      |          _____         |
      |         /     \        |
      +------->| Timer |-------+
                \     /
                 `---'

                                  Figure 2

   This CPN can be translated as the following Timed TPN:

Petit-Huguenin             Expires 11 May 2022                 [Page 37]
Internet-Draft           Computerate Specifying            November 2021

      > timer : Top
      > timer = top $ do
      >   state <- place "State" ()
      >   timer <- place "Timer" (Timed ())
      >   transition "start timer"
      >     empty
      >     empty
      >     [output () state pure,
      >      output () timer {delay=100} (\x => [timed x])]
      >     (pure . dup)
      >   transition "stop timer"
      >     [input state () one,
      >      input timer () {delay=100}
      >        (\case (x ::: []) => Just (untimed x); _ => Nothing)]
      >     empty
      >     empty
      >     (pure . fst)
      >   transition "timeout"
      >     [input state () one,
      >      input timer ()
      >        (\case (x ::: []) => Just (untimed x); _ => Nothing)]
      >     empty
      >     empty
      >     (pure . fst)

   Here the "Timer" place contains "Timed ()" values, which are added by
   the "start timer" transition.  The added token will enable the
   "timeout" transition only after 100 unit of time have passed.  Note
   that the clock used to calcualte enablement of transitions is
   discrete, so a simulation does not have to really wait for that time.
   The "timeout" transition also removes the token from the "Timer"
   place, effectively making sure that it does not trigger a second
   time.

   The "stop timer" transition is used when an event made that timer
   useless.  In that case we want to remove the token from the "Timer"
   place ahead of its expiration time, so it is not fired later.  This
   is the meaning of the delay inscription in the input arc, which is
   understood as a preemptive delay.

6.1.4.3.  Verifying a Typed Petri Net

   The TPN values created in Section 6.1.4.1 can be used to test, debug
   and validate a protocol.

Petit-Huguenin             Expires 11 May 2022                 [Page 38]
Internet-Draft           Computerate Specifying            November 2021

   This is done by running a simulation of the protocol.  The plan is
   that this simulation will be driven from the future graphical
   interface but meanwhile it is possible to directly call a set of
   functions.

   A simulation is executed when a succession of transitions occurs.  It
   starts by building an initial marking, which is done by using the
   "initialMarking" function on a top TPN.  For instance the command
   "initialMarking protocol" returns the following:

      [{(1, "COL"), (2, "OUR"), (3, "ED "), (4, "PET"), (5, "RI "),
      (6, "NET")}, {""}, {}, {}, {}, {}, {1}, {False, True}, {1}]

   After this each transition occurrence is composed of 3 steps:

   1.  Find the list of transitions that are enabled from the current
       marking:

      :let transitions = enabledTransitions marking top

   2.  Find the possible bindings for the transition selected.  There is
       only one transition possible for that TPN instance, so we can use
       it to list the bindings:

      :let bindings = bindings marking top (head transitions)

   3.  Create a new current marking from the transition and binding
       selected.  Again we have only one possible binding in this
       example, so we can use it to update the marking after applying
       the binding and transition:

      :let marking = bindings marking top (head transitions)
        (head bindings)

   We can then calculate the next occurrence by looping back to step
   (1).

   The simulation stops when there is no enabled transition for the
   current marking.

6.1.4.4.  Deriving a Type from a Typed Petri Net

   Designing and validating a Petri Net are essential tasks, but they
   cannot be directly used to guarantee that a process is following part
   or totality of this Petri Net.

Petit-Huguenin             Expires 11 May 2022                 [Page 39]
Internet-Draft           Computerate Specifying            November 2021

   To do so we need to generate a Sum type that encodes all the
   transitions as constructors.  This type then can be used to build a
   proof that a list of binding elements are valid according to that
   Petri Net.

   In CPN, a binding is a list of (name, value) tuples, making it easy
   to read.  In TPN we are using instead a tuple of the values as taken
   as input to the "Transition" inscription.  That means that the
   variables are identified by position in this tuple, instead of by
   name.

   The example below shows two constructors for the example Petri Net
   used in this document.

      sendPacket' : (NoxData, No) -> List (NoxData, No, NoxData)

      updateSendPacket : Marking xs -> (NoxData, No) -> Marking xs

      data T210 : Marking xs -> Type where
        Init : T210 (initialMarking top)
        SendPacket : (binding : (NoxData, No)) ->
                     (elem (fst binding) (packetToSend m)) =>
                     (elem (snd binding) (Ns m)) =>
                     (sendPacket' binding =
                       pure (fst binding, snd binding, fst binding)) =>
                     T210 m ->
                     T210 (updateSendPacket binding m)

   This type can then be used for various purposes, e.g. to draw a
   Message Sequence Chart as described in Section 6.1.5.2.

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 11 May 2022                 [Page 40]
Internet-Draft           Computerate Specifying            November 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:

      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"]

   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).

      code::[%runElab toBitDiagram names]

Petit-Huguenin             Expires 11 May 2022                 [Page 41]
Internet-Draft           Computerate Specifying            November 2021

6.1.5.2.  Message Sequence Charts

   Message Sequence Charts (MSC) are a common way to represent an
   example of execution of a protocol, 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 and thus cannot replace completely a description of the
   protocol by other means.

   There is 4 steps to generate automatically an MSC that is guaranteed
   to be conform to the specification:

   1.  Design a Colored Petri Net of the behavior of the protocol.  A
       Petri Net models all sides of a communications protocol,
       including the network itself, this is why it is the best way to
       generate an MSC.

   2.  Build a sequence of binding elements as described in
       Section 6.1.4.3.

   3.  Convert the TPN into a specialized type that guarantees that the
       list of (transition, binding) that represent the MSC to draw is
       valid according to the TPN.  This is explained in
       Section 6.1.4.4.

   E.g. the following instance typechecks with the generated type for
   the example CPN used in this document:

      test : T210 ?
      test = Init
             |> SendPacket ((1, "COL"), 1)
             |> TransmitPacket ((1, "COL"), True)
             |> ReceivePacket ((1, "COL"), "", 1)
             |> TransmitAck 1
             |> ReceiveAck (1, 1)

   5.  The last step is to pass that instance to a function that will
       generate the MSC:

      ....
      code::[generateMsc test [(A, D), (B, C)]]
      ....

Petit-Huguenin             Expires 11 May 2022                 [Page 42]
Internet-Draft           Computerate Specifying            November 2021

   The parameters of the "generateMsc" function are the list of bindings
   and the name of the Petri Net places between which lines will be
   drawn.  If for some reason the network manipulates the token between
   A and B, or B and C, the function will accordingly show that the
   packet is either lost, duplicated, delayed or even that a packet
   arrived from an unknown sender.

   It is also possible to pass a user-defined function that will take as
   parameter a token as sent by places A or C and convert it in a packet
   that is to be showed after the MSC itself.

   This function can be provided by the type of proofs described in
   Section 5.3.1.  That means that, as long as we have a proof of
   isomorphism between then, we can use Semantic Types directly in our
   TPN instead of Wire Types, making the model simpler.

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.

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 43]
Internet-Draft           Computerate Specifying            November 2021

   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 [Christiansen16] 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.

   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 11 May 2022                 [Page 44]
Internet-Draft           Computerate Specifying            November 2021

      import Data.Control.Isomorphism
      import Rfc5234.Abnf

      sdp : Abnf True
      sdp = rule "session-description" $
        do versionField
           originField
           sessionNameField
           (optional informationField)
           (optional uriField)
           (repeat many emailField)
           (repeat many phoneField)
           (optional connectionField)
           (repeat many bandwidthField)
           (repeat some timeDescription)
           (optional keyField)
           (repeat many attributeField)
           (repeat many mediaDescription)

      %runElab (generateType "SessionDescription" sdp)

      to : Sdp -> SessionDescription

      from : SessionDescription -> Abnf

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

      fromTo : (x : Sdp) -> from (to x) = x

   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:

      data DeltaSessionDescription : Type where
        ...

      same : Iso Sdp (SessionDescription, DeltaSessionDescription)
        ...

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 45]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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.  Meta-languages Defined in RFCs

   The following sections describe the support for meta-languages that
   are defined in an RFC.

6.2.1.1.  Routing Policy Specification Language next generation (RPSLng)

   Routing Policy Specification Language (RPSL) [RFC4012] is a formal
   language used to describe a view of the global routing policy in a
   single cooperatively maintained distributed database.

6.2.1.2.  External Data Representation Standard (XDR)

   External Data Representation (XDR) [RFC4506] is a formal language for
   the description and encoding of data.

6.2.1.3.  Formal Notation for RObust Header Compression (ROHC-FN)

   Formal Notation for RObust Header Compression (ROHC-FN) [RFC4997] is
   a formal notation new profiles within the ROHC framework.

6.2.1.4.  Abstract Syntax Notation X (ASN.X)

   Abstract Syntax Notation X (ASN.X) [RFC4912] is a semantically
   equivalent Extensible Markup Language (XML) representation for
   Abstract Syntax Notation One (ASN.1) specifications.

6.2.1.5.  Augmented BNF (ABNF)

   Augmented Backus-Naur Form (ABNF) [RFC5234] is a formal language that
   can be used to describe a text based PDU.

   An ABNF specification can be described by the functions defined in
   the "RFC5234.Abnf" module, each of them mapping one of the operators
   defined in Section 3 of [RFC5234].

   For instance the following definition:

Petit-Huguenin             Expires 11 May 2022                 [Page 46]
Internet-Draft           Computerate Specifying            November 2021

      > alpha : Abnf True
      > alpha = rule "ALPHA" $ hexRange 0x41 0x5a <|> hexRange 0x61 0x7a

   is equivalent to the ABNF rule:

      ALPHA =  %x41-5A / %x61-7A

   Using this language permits to generate an ABNF specification that is
   guaranteed to be syntactically correct.  But the language imposes
   constraints that go beyond mere syntax and also guarantee that the
   generated ABNF specification is semantically correct.

   For instance the following ABNF is syntactically correct but it will
   take an infinite amount of time to parse something with it:

      total
      bad : Abnf True
      bad = bad "a"

   Here the use of the "total" keyword will ensure that the Idris
   typechecker will reject specifications that will loop forever.

   On the other hand this language can describe the parsing of infinite
   streams.  For instance the following matches an infinite sequence of
   "a" or "A":

      total
      good : Abnf True
      good = "a" good

   Together, the functions used to describe an ABNF specification form a
   DSL with deep embedding.  Because of this deep embedding, the
   resulting internal structure can be used in various ways.

   The primary use of that internal structure is to format a textual
   representation of the ABNF specification that can be directly
   inserted in the documentation part of a computerate specification.
   The internal structure implements the "Pretty" interface of the
   "Prettyprinting" module to format automatically the output.

   By default the ABNF specification is displayed exactly as entered.

   A secondary use of that internal structure is as an index on the
   `"Valid`" type, which permits to build proofs that specific strings
   are valid according to an ABNF grammar.  But ABNF cannot always
   encode all the constraints needed to describe a PDU.  An example of
   that is the following subset of the ABNF defined in
   [I-D.rivest-sexp]:

Petit-Huguenin             Expires 11 May 2022                 [Page 47]
Internet-Draft           Computerate Specifying            November 2021

      sexp  =  list / token

      list  =  "(" sexp ")"

      token =  1*DIGIT ":" *OCTET

   In the "token" rule the constraint that the actual number of OCTET
   terminal values allowed is provided by the number on the left of the
   colon cannot be encoded in ABNF.  Because of that a valid example of
   a Sexp should be built from a separate type:

      > data Sexp : Type where
      >   (>>) : Sexp -> Sexp -> Sexp
      >   T : String -> Sexp

   Then a function with type "Sexp -> (s : List Int ** Valid s sexp))"
   can be implemented to generate examples that are by construction
   valid according to the ABNF, and that can be directly inserted in the
   document, such as:

      > example : Sexp -> (s : List Int ** Valid s Main.sexp)
      > -- code elided

      \code::[example (do (T "a"); (T "bc"); (do (T "def")))]

   will generate:

      (1:a2:bc(3:def))

   The ABNF DSL and the ability of building proofs for examples subsume
   most of the existing ABNF verification tools, making them redundant.

   The "RFC5234.Core" module contains the definitions for common ABNF
   rules and is meant to be imported by computerate specifications that
   define ABNF specification that use them.

   See Section 8.2.1 for details on the "rfc5234" package that contains
   the "RFC5234" and "RFC5234.Core" modules.

6.2.1.6.  Routing Backus-Naur Form (RBNF)

   Routing Backus-Naur Form (RBNF) [RFC5511] is a formal language used
   to specify routing protocols.

6.2.1.7.  Data Modeling Language (YANG)

   YANG [RFC6020] is a data modeling language used to model
   configuration and state data.

Petit-Huguenin             Expires 11 May 2022                 [Page 48]
Internet-Draft           Computerate Specifying            November 2021

6.2.1.8.  Concise Data Definition Language (CDDL)

   CDDL [RFC8610] is notational convention to express Concise Binary
   Object Representation (CBOR) data structures.

6.2.1.9.  Structured Field Values for HTTP

   Structured Field Values for HTTP [RFC8941] is a common syntax for
   HTTP header and trailers fields that is more restrictive than
   traditional HTTP field values.

6.2.2.  Externally Defined Meta-languages

   The following sections describe the support for meta-languages that
   are used in RFCs but that were defined outside the IETF.

   TBD.

6.2.3.  Ad-hoc Meta-languages

   The following sections describe the support for meta-languages that
   are used in RFCs but that are defined in an ad-hoc fashion, generally
   in the same RFC.

   TBD.

6.2.4.  Draft Meta-Languages

   The following sections describes the support for meta-languages that
   are were defined in Internet-Drafts that are still in development.

6.2.4.1.  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).

Petit-Huguenin             Expires 11 May 2022                 [Page 49]
Internet-Draft           Computerate Specifying            November 2021

      -  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

      -  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:

      > 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`}

   and is rendered as:

Petit-Huguenin             Expires 11 May 2022                 [Page 50]
Internet-Draft           Computerate Specifying            November 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 3

6.2.4.2.  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 11 May 2022                 [Page 51]
Internet-Draft           Computerate Specifying            November 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 11 May 2022                 [Page 52]
Internet-Draft           Computerate Specifying            November 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:

      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

Petit-Huguenin             Expires 11 May 2022                 [Page 53]
Internet-Draft           Computerate Specifying            November 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:

      %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

   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:

      import RFC791.IP

      %runElab declare internetHeader

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

Petit-Huguenin             Expires 11 May 2022                 [Page 54]
Internet-Draft           Computerate Specifying            November 2021

      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 dscp)

   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.  Codepoint Registries

   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.

   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
   synthesize a Sum type of all these values in the computerate
   specification for the document that defined that registry.

   When new codepoints are defined after the RFC holding the registry
   definition is published, the specification for that RFC must be
   modified to reference the new type defined in the specification of
   the RFC (or other document) that contains the codepoint definition.

Petit-Huguenin             Expires 11 May 2022                 [Page 55]
Internet-Draft           Computerate Specifying            November 2021

   As example, the type for the option field in the Internet Protocol
   header could be defined like this:

      data Option : Type where
        EoolOption : (codepoint : BitVector 8) -> codepoint = 0 =>
         Option
        NopOption : (codepoint : BitVector 8) -> codepoint = 1 =>
         Option
        ...
        UnknownOption : (codepoint : BitVector 8) ->
          (length : Unsigned 8) ->
          (data : Vect (BitVector 8) length) -> Option

   Then a new codepoint is defined like this in the specification for
   RFC 1103:

      public export
      data DoDBasicSecurity : Type where
        MkDoDBasicSecurity :
          (codepoint : BitVector 8) -> (codepoint = 130) =>
          (length : Unsigned 8) ->
          (level : BitVector 8) ->
          (flags : Vect (BitVector 8) (length - 1)) ->
          DoDBasicSecurity

   Finally a dependency to the specification of RFC 1103 is added to the
   specification for RFC 791, and the Option type is modified as follow:

      data Option : Type where
        EoolOption : (codepoint : BitVector 8) -> codepoint = 0 =>
          Option
        NopOption : (codepoint : BitVector 8) -> codepoint = 1 =>
          Option
        ...
        DoDBasicSecurityOption : DoDBasicSecurity -> Option
        UnknownOption : (codepoint : BitVector 8) ->
          (length : Unsigned 8) ->
          (data : Vect (BitVector 8) length) -> Option

   This type actually acts as a codepoint registry that mirrors the
   equivalent IANA registry.

7.  Exporting Specifications

   An exporting specification is either a self-contained or an importing
   specification that exports an Idris package and its documentation for
   reuse by importing specifications.

Petit-Huguenin             Expires 11 May 2022                 [Page 56]
Internet-Draft           Computerate Specifying            November 2021

   Such specification exports 4 or 5 components:

   An Idris package:  This is the binary actifacts that the code in an
      importing specification will use.  E.g., this is what a
      specification using ABNF will use to define the ABNF specific to
      the standard described in that document.

      The Idris package is built from the lipkg file that doubles as the
      Asciidoc root document.  The "modules" statement in that file
      lists all the idr and lidr files that will compose that package.

   A tutorial:  This is a document that guides the reader step by step
      in the use of the Idris package.  This document may contain
      examples, example that may themselves be generated by the Idris
      API.

      The tutorial is an adoc or lidr file.  Using an lidr file makes
      writing examples easier, but the code in that file is not part of
      either the Idris package or the API documentation.

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

      This is the document part of the lipkg files that compose the API
      documentation.

   An API documentation:  This is a document that lists all the Idris
      types and functions in alphabetic order, together with structured
      comments, for the Idris package.

      This document is automatically generated from the structured Idris
      comments in the idr and lidr files that compose the reference
      document.

   An eventual bibliography:  This document (or documents if both
      normative and informative bibliographies are needed) contains the
      bibliographic items cited in the other exported documents.

   An exporting specification can be defined in an original computerate
   specification or in a retrofitted specification (RFC or I-D that was
   later enriched with Idris code).  But an RFC cannot be modified, and
   the authors of an I-D may be different from the authors of the Idris
   code and unwilling to integrate the documentation in their document.
   Because of that there is multiple scenarios on how to publish the
   documentation for an Idris API:

   In the same document:  This is possible when the specification is

Petit-Huguenin             Expires 11 May 2022                 [Page 57]
Internet-Draft           Computerate Specifying            November 2021

      under the control of the same authors.  In this document, the
      documentation for the modules that compose the Computerate
      Specification Standard Library are published in this document,
      with the tutorials in Section 6, the references in Section 8.1 and
      the API documentations in Appendix B.

   In an separate document:  The tutorial, reference and API
      documentation documents can simply be included in a separate
      Internet-Draft whose sole purpose is to carry that documentation.

   In the Standard Library:  Some retrofitted specifications are deemed
      essential for authors of specifications, so the documentation for
      these retrofitted specification is part of this document.  This is
      the case for the ABNF documentation (Section 6.2.1.5,
      Section 8.2.1, and Appendix B.2) and the APHD documentation
      (Section 6.2.4.1, Section 8.2.2, and Appendix B.3).

8.  Standard Library

   The following modules are available in the Docker image:

   *  ComputerateSpecifying

   *  ComputerateSpecifying.Metanorma.Ietf

   *  ComputerateSpecifying.Metanorma.Tpn

8.1.  Internal Modules

8.1.1.  Metanorma.Ietf

   The MetaNorma.Ietf module provides a way to programmatically build an
   AsciiDoc document without having to worry about the particular
   formatting details.  The types in this library are not meant to be
   used directly, but as the return type of functions in modules that
   generates text for insertion in a document.

   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 enforce the generation of AsciiDoc that results
   in valid xml2rfc v3 document.

   The "Text", "Must", "MustNot", "Required", "Shall", "ShallNot",
   "Should", "ShouldNot", "Recommended", "May", "Optional", "HardBreak",
   "Contact", "Comment", "Italic", "Link", "Index", "Citation", "Bold",
   "Subscript", "Superscript", "Monospace", "Unicode", "Cross", and
   "Attribute" constructors are used to build individual inline
   elements.

Petit-Huguenin             Expires 11 May 2022                 [Page 58]
Internet-Draft           Computerate Specifying            November 2021

   The "Paragraph" constructor is used to build a paragraph, and is
   composed from a list of inline elements.

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 so 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").

8.1.3.  Unsigned

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

Petit-Huguenin             Expires 11 May 2022                 [Page 59]
Internet-Draft           Computerate Specifying            November 2021

8.1.4.  Dimension

   This module permits to manipulate denominate numbers, which are
   numbers associated with a unit.  Examples of denominate numbers are
   "(5, meter / second)" (which uses a unit of speed), or "(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 the fraction of two Integer.  Its type
   is indexed over a list of dimensions in canonical order, 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.

   A unit dimension can be chosen as one of the predefined physical
   dimensions, "Time" and "Length".

   The non-physical unit dimension "Info" (for "unit of information") is
   also defined.

   It is also possible to define other non-physical unit dimensions as
   needed:

      apple : Denominate [(Q "Apple", 1)]
      apple = MkDenominate 1 1

   Finally dimensionless numbers (i.e., denominate numbers with type
   "Dimensionless") can be constructed by using the "none" unit, as in
   "(10, none)".  The "fromInteger" and "fromDouble" functions also
   construct dimensionless numbers.

   Denominate numbers are constructed by using the "toDenominate"
   function on a tuple made of a number and a unit.  E.g., "toDenominate
   (5, megabit)" will build the denominate number 5 with the "megabit"
   unit.  The "cast" can also be used when the type of the returned
   value can be inferred.

   For simplicity, examples of denominate numbers in this document are
   given in their tuple form.

   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.

Petit-Huguenin             Expires 11 May 2022                 [Page 60]
Internet-Draft           Computerate Specifying            November 2021

   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
   resulting dimension will be derived from the respective dimension of
   the arguments.  E.g. multiplying "(5, meter)" by "(6, meter)" will
   return the equivalent of "(30, meter * meter)".

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

   Denominate numbers can be converted into a "Double" value by using
   the "fromDenominate" function.  The second parameter of the function
   is the unit that we want the result expressed in.  E.g.,
   "fromDenominate (toDenominate (5, meter / second)) (kilometer /
   hour)" will return 18.0, which is 5 meters per second expressed in
   kilometers per hour.

   Denominate numbers can also be converted into rounded down Int by
   using the "fromDenominateToInt" function.

   Ultimately we want to insert a denominate number, together with its
   unit, as text in a computerate specification.  This is done by using
   a tuple made of the denominate number and of the expected unit.
   E.g., code:ComputerateSpecifying/Dimension.lidr["(toDenominate (2,
   byte), bit)"] will insert "16 bits" in the text.

   For each dimension that is useful for Internet standards (time,
   length, and information) a list of constants that represents units of
   that dimension are pre-defined.

   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
   "Info" dimension (i.e., from "kilobit" to "yottabit"), and IEC units
   (positive powers of 2) for the "Info" 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 [Knuth05].

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.

Petit-Huguenin             Expires 11 May 2022                 [Page 61]
Internet-Draft           Computerate Specifying            November 2021

   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.

   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

   The "Tpn" module permits to build Typed Petri Nets.  It is designed
   to mimic Hierarchical Colored Petri Nets so conversions could be done
   mechanically.

8.1.7.1.  Building a TPN

   The "Timed" type is used as a wrapper around another type when its
   values need to be associated with time, with the "timed" and
   "untimed" functions used to respectively unwrap and wrap a value.

   The "input" function builds an input arc for a transition.  The
   inscription is a function that takes one or more tokens as input and
   generates an optional value of the input arc type.  The optionality
   of the output type permits to decide if the tokens can or cannot be
   used in the transition.

Petit-Huguenin             Expires 11 May 2022                 [Page 62]
Internet-Draft           Computerate Specifying            November 2021

   The "one" function can be used when a unique token is to be taken
   from the place and passed to the function.

   The type of the codomain of that function may be different from the
   type of the place to permit to do some manipulation on the token
   itself.

   These two features can be combined together by using pattern matching
   inside the inscription.

   The delay value (which defaults to 0) in an input arc indicates a
   preemptive time from which a "Timed" wrapped token will enable the
   transition.

   The "inhibitor" function builds an inhibitor arc for a transition.
   An inhibitor arc is a variant of input arcs that can trigger a
   transition only if the place it is connected is empty.

   The "reset" function builds a reset arc for a transition.  A reset
   arc is a variant of input arcs that always trigger a transition
   regardless of the content of the connected place, and that will empty
   the connected place when triggered.

   The "output" function builds an output arc for a transition.  An
   output arc takes a value of the type created by a transition,
   converts it using the function (acting as inscription) into a list of
   tokens and insert that list in the destination place.  The list of
   tokens can be empty if no token has to be added, or can contain one
   or more tokens.

   The order of the parameters of that function is the inverse of the
   "input" function to show that the function codomain is the type of
   the place.

   An output arc can contain a delay value (which defaults to 0) that
   will be added to any token that is wrapped in the "Timed" type.

   The "Module" Monad is used to group together places, ports,
   transitions and instances of other modules into a module by using the
   "do" notation.

   The "place" function builds a Petri Net place, which is a structure
   that holds state in the form of tokens.  A place has a name, a type
   (or color) and an initial content which defaults to emptyness.

Petit-Huguenin             Expires 11 May 2022                 [Page 63]
Internet-Draft           Computerate Specifying            November 2021

   Alternatively the "port" function can be used to build a Petri Net
   port, which is used to define the interface of a Petri Net module
   and, like a place, has a name and a type.  A port does not have an
   initial content but contains the direction tokens are allowed to flow
   between an outer module instance and a module definition.

   Note that the names carried by most elements on a TPN are only used
   for documentation purpose.  That means that a name can be empty or
   can be used multiple times.

   The "transition" function brings together input arcs (including
   inhibitor and reset arcs), output arcs, and the function that will
   convert input tokens into output tokens.

   The "unifications" list contains a 4-tuples in the form (input-index,
   data-index, input-index, data-index).  Each input-index is an index
   in the list of inputs.  Each data index is an index in the tuple
   representing the codomain of the inscription.  The value of the first
   input-index/data-index will be unified with the value of the second
   input-index/data-index.

   The "instance" function imports another module in this module and
   assign a local Place or Port to each Port imported from that module.

   Note that using an instance of a module is different from using a
   module directly.  A port is a temporary placeholder for a place, so a
   port needs at some point to be mapped to a place, that will contain
   the actual state.  The is the role of an instance to do that mapping.

   Finally the "top" function wraps a module that has no exported ports,
   so it can be used as input to the functions described in the next
   section.

   The core of TPN is implemented by the functions described above.  It
   is possible to combine these functions to build more complex
   functions to simplify the construction of a TPN, or to implement
   variants of CPN.  In any case these complex functions are always
   transformed into core functions, making the simulators and other
   processes that take as input a TPN simpler to implement and
   independent from these complex functions.  The functions in the
   following paragraphs are built that way.

   The "free" function adds the possibility of using a free variable as
   part of the inscription on a transition.  Using a free variable
   requires that its type implements the interface "Enum".

Petit-Huguenin             Expires 11 May 2022                 [Page 64]
Internet-Draft           Computerate Specifying            November 2021

   The "addStep", "addPriorities", and "addTime" functions add the
   transitions and places needed to implements the global step,
   transition priorities, and time features to an existing TPN.

8.1.7.2.  Verifying a TPN

   The "Marking" type describes a marking, which is a set of places and
   their content.  It represents the global state of the system
   described by a TPN.  A marking is indexed over the list of types of
   the places in it, such as we can guarantee that the marking structure
   never changes when transitions are fired.

   The initial state of the system is generated by the "initialMarking"
   function.

   A "Transition" represents the unique path through modules to a
   transition.

   The "enabledTransitions" function generates a list of all the
   transitions that are enabled by a specific marking.

   A "Binding" is a tuple that has the same size as the number of input
   arcs and that contains a token from each of the respective places
   such as substituting the input places in a transition by places that
   contain only that value will still enable the transition.

   The "bindings" function lists all the possible bindings for a
   specific marking and an enabled transition.

   The "transition" function transforms a marking into a new marking by
   applying a specific binding to a transition.

8.1.7.3.  Deriving a Type From a TPN

   The "deriveType" function takes a top-level TPN (as an instance of
   the type "Top") and generates the declaration of a new Sum type, with
   one constructor per transition, plus one constructor for the initial
   marking.  This type then can serve to define a proof that a list of
   (transition, binding) tuples are valid according to that Petri Net.

   On the generated type, the "Init" constructor builds an initial
   marking.  Then each other constructors are used to validate a
   sequence of binding elements.  Each non-initial constructor carries a
   set of proofs, one per input arc that prove that the binding is
   originating from the places in the marking, and one that prove that
   this transition is enabled, by showing that the transition using that
   binding is deterministic.  Finally each transition updates the
   marking according to the output arcs, i.e removing and adding tokens.

Petit-Huguenin             Expires 11 May 2022                 [Page 65]
Internet-Draft           Computerate Specifying            November 2021

8.2.  Meta-Language Packages

8.2.1.  RFC 5234 (ABNF)

   The "RFC5234" module permits to build ABNF grammars.  It is designed
   to mimic closely the syntax described in [RFC5234].

8.2.1.1.  Building an ABNF

   All ABNF elements use the Idris type "Abnf Bool".  The index must be
   set to "True" if the element is consuming one or more characters,
   "False" if not.  This is the mechanism that permits to verify that an
   ABNF specification can be used to parse in finite time.

   The section numbers below refer to sections in [RFC5234].

   Giving a name to an element, as defined in section 2.2, uses the
   "rule" function.  It takes the name of the rule and an ABNF element
   as parameters.

   Concatenation of elements, as defined in section 3.1, uses the "(>>)"
   infix operator or the "do" notation to sequence elements.

   Alternation of elements, as defined in section 3.2, uses the "<|>"
   infix operator to define alternative between elements.

   Grouping of elements, as defined in section 3.5, uses the "group"
   function.  It takes an element as parameter.

   Variable repetition of elements, as defined in section 3.6, uses the
   "repeat" function.  This function takes a value of type
   "Text.Quantity" and an ABNF element as parameters.  In additional to
   the quantities defined in the "Text.Quantity" modules, the "many" and
   "some" can be used as equivalent to respectively "*" and "1*".

   A sequence repetition for an exact number of repetitions, as defined
   in section 3.7, uses the "exact" function.  This function takes the
   number of repetitions and an element as parameters.

   Optional element, as defined in section 3.8, uses the "optional"
   function.  This function takes an element as parameter.

   Terminal values, as defined in section 2.3, use the "binTerm",
   "decTerm", "hexTerm", "binTerms", "decTerms", "hexTerms", and
   "string" functions.  The "binTerm", "decTerm", and "hexTerm"
   functions take one parameter, which is the terminal value.  The
   "bin", "dec", and "hex" prefixes refers to the encoding that will be
   used to display the equivalent ABNF, not to the encoding that is used

Petit-Huguenin             Expires 11 May 2022                 [Page 66]
Internet-Draft           Computerate Specifying            November 2021

   for the parameter value, which is independent.  Similarly the
   "binTerms", "decTerms", and "hexTerms" functions take one parameter,
   which is a non-empty list of terminal values.  The "string" function
   takes a string of US-ASCII character as parameter.

   Value range alternative, as defined in section 3.4, uses the
   "binRange", "decRange", and "hexRange" functions.  It takes two
   parameters as lower and higher bounds for the range.  Alternatives
   are generated in reverse order if the first parameter has an higher
   value than the value of the second parameter.

8.2.1.2.  Generating and Verifying ABNF specifications

   A value of "Abnf" is automatically converted in its text form when
   used with one of the code macros.  When using the inline macro, the
   ABNF is formatted using the "Asciidoc" interface.  When using the
   block macro, the ABNF is formatted using the "Pretty" interface,
   which follows the same presentation format than used in RFC 5234.

   The "Valid string grammar" type permits to build a proof that a
   string is valid according to a specific ABNF grammar.  Such proof can
   then be directly inserted in the document by using the inline code
   macro, which will display the verified example.  In cases where the
   length of the example exceeds the maximum allowed width of a rendered
   document, using the block code macro will format the string according
   to [RFC8792].

8.2.1.3.  Common Rules

   The "RFC5234.Core" module contains a set of common rules that are
   often reused by ABNF.

8.2.2.  Augmented Packet Header Diagrams (APHD)

   This module defines a DSL that permits to define binary PDUs.  These
   definition can then be used in a document to generate bit diagrams
   and field definitions that are conform to the
   [I-D.mcquistin-augmented-ascii-diagrams].  These in turn can be
   processed by the tooling desribed in the Internet-Draft.

   A PDU is inserted in a document by using the inline code macro
   (code:depends/augmented-ascii-diagrams/APHD.lidr[]).

Petit-Huguenin             Expires 11 May 2022                 [Page 67]
Internet-Draft           Computerate Specifying            November 2021

8.3.  Protocol Packages

8.3.1.  RFC 791 (Internet Protocol)

   TBD.

9.  Informative References

   [Aalst11]  Aalst, W. V. D. and C. Stahl, "Modeling Business
              Processes: A Petri Net-Oriented Approach", Cambridge,
              Mass:MIT Press, 2011.

   [AsciiBib] "AsciiBib", (accessed August 20, 2020),
              <https://www.relaton.com/specs/asciibib/>.

   [AsciiDoc] Wikipedia, The Free Encyclopedia, s.v., "AsciiDoc",
              (accessed August 20, 2020),
              <https://en.wikipedia.org/wiki/AsciiDoc/>.

   [Asciidoctor]
              "Asciidoctor", (accessed August 20, 2020),
              <https://asciidoctor.org/docs/user-manual>.

   [Bennett15]
              Bennett, B., "Logically Fallacious: The Ultimate
              Collection of Over 300 Logical Fallacies", 2015.

   [Blockquotes]
              "Markdown-style blockquotes", (accessed August 20, 2020),
              <https://asciidoctor.org/docs/user-manual/#markdown-style-
              blockquotes>.

   [Bornat05] Bornat, R., "Proof and Disproof in Formal Logic: An
              Introduction for Programmers", Oxford ; New York:Oxford
              University Press, 2005.

   [Brady17]  Brady, E., "Type-Driven Development with Idris", Shelter
              Island, NY:Manning Publications Co, 2017.

   [Brinkmann02]
              Brinkmann, R. and R. Drechsler, "RTL-Datapath Verification
              using Integer Linear Programming", IEEE Computer Society,
              2002, <http://dl.acm.org/citation.cfm?id=835389>.

Petit-Huguenin             Expires 11 May 2022                 [Page 68]
Internet-Draft           Computerate Specifying            November 2021

   [Christiansen16]
              Christiansen, D. and E. C. Brady, "Elaborator reflection:
              Extending Idris in Idris", ACM Press-Association for
              Computing Machinery, 2016, <https://research-
              repository.st-andrews.ac.uk/bitstream/handle/10023/9522/
              elab_reflection_paper.pdf>.

   [Community20]
              Community, T. M., "The Lean Mathematical Library", 20
              January 2020, <http://arxiv.org/abs/1910.09336>.

   [Copyright]
              "Machine-readable debian/copyright file", (accessed August
              20, 2020), <https://www.debian.org/doc/packaging-manuals/
              copyright-format/1.0/>.

   [Cpntools] "CPN Tools: A tool for editing, simulating, and analyzing
              Colored Petri nets", (accessed August 20, 2020),
              <http://cpntools.org/>.

   [Curry-Howard]
              Wikipedia, The Free Encyclopedia, s.v., "Curry-Howard
              correspondence", (accessed August 20, 2020),
              <https://en.wikipedia.org/wiki/Curry-
              Howard_correspondence>.

   [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, 13 November 2006,
              <https://datatracker.ietf.org/doc/draft-bortzmeyer-
              language-state-machines>.

   [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-09, 25 October 2021,
              <https://datatracker.ietf.org/doc/draft-mcquistin-
              augmented-ascii-diagrams>.

   [I-D.ribose-asciirfc]
              Tse, R., Nicholas, N., Lau, J., and P. Brasolin,
              "AsciiRFC: Authoring Internet-Drafts And RFCs Using
              AsciiDoc", Work in Progress, Internet-Draft, draft-ribose-
              asciirfc-08, 17 April 2018,
              <https://datatracker.ietf.org/doc/draft-ribose-asciirfc>.

Petit-Huguenin             Expires 11 May 2022                 [Page 69]
Internet-Draft           Computerate Specifying            November 2021

   [I-D.rivest-sexp]
              Rivest, R. L., "S-Expressions", Work in Progress,
              Internet-Draft, draft-rivest-sexp-00.txt, 4 May 1997,
              <https://people.csail.mit.edu/rivest/Sexp.txt>.

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

   [Jensen07] Jensen, K., Kristensen, L., and L. Wells, "Coloured Petri
              Nets and CPN Tools for modelling and validation of
              concurrent systems", 31 May 2007,
              <http://webdiis.unizar.es/~lrecalde/doctorado/
              bibliografia/coloreadas.pdf>.

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

   [Knuth05]  Knuth, D. E., "The Art of Computer Programming", Upper
              Saddle River, NJ:Addison-Wesley, 2005.

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

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

   [Linear-Resources]
              "Linear Resources", (accessed August 20, 2020),
              <https://idris2.readthedocs.io/en/latest/app/linear.html>.

   [Metanorma]
              "Metanorma", (accessed August 20, 2020),
              <https://www.metanorma.com/>.

   [Metanorma-IETF]
              "Metanorma-IETF", (accessed August 20, 2020),
              <https://www.metanorma.com/author/ietf/>.

   [Mimram20] Mimram, S., "Program = Proof", 2020,
              <http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/
              teaching/INF551/course.pdf>.

Petit-Huguenin             Expires 11 May 2022                 [Page 70]
Internet-Draft           Computerate Specifying            November 2021

   [Minutes]  "Trust Meeting Minutes Tuesday March 16, 2021", (accessed
              May 24, 2021), <https://trustee.ietf.org/wp-content/
              uploads/2021-03-16-trust-minutes.pdf>.

   [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", Boston, MA, USA:IEEE, November
              2016, <http://ieeexplore.ieee.org/document/7839788/>.

   [Nederpelt14]
              Nederpelt and H. Geuvers, "Type Theory and Formal Proof:
              An Introduction", Cambridge ; New York:Cambridge
              University Press, 2014.

   [RFC-Guide]
              "RFC Style Guide", (accessed August 20, 2020),
              <https://www.rfc-editor.org/styleguide/part2/>.

   [rfc-prolog]
              Petit-Huguenin, M., "RFC Prolog database", 28 August 2021,
              <git://shalmaneser.org/rfc-prolog>.

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

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

   [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>.

   [RFC4012]  Blunk, L., Damas, J., Parent, F., and A. Robachevsky,
              "Routing Policy Specification Language next generation
              (RPSLng)", RFC 4012, DOI 10.17487/RFC4012, March 2005,
              <https://www.rfc-editor.org/info/rfc4012>.

   [RFC4506]  Eisler, M., "XDR: External Data Representation Standard",
              RFC 4506, DOI 10.17487/RFC4506, May 2006,
              <https://www.rfc-editor.org/info/rfc4506>.

   [RFC4912]  Legg, S., "Abstract Syntax Notation X (ASN.X)", RFC 4912,
              DOI 10.17487/RFC4912, July 2007,
              <https://www.rfc-editor.org/info/rfc4912>.

Petit-Huguenin             Expires 11 May 2022                 [Page 71]
Internet-Draft           Computerate Specifying            November 2021

   [RFC4997]  Pelletier, G. and R. Finking, "Formal Notation for RObust
              Header Compression (ROHC-FN)", RFC 4997,
              DOI 10.17487/RFC4997, July 2007,
              <https://www.rfc-editor.org/info/rfc4997>.

   [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>.

   [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>.

   [RFC5511]  Farrel, A., "Routing Backus-Naur Form (RBNF): A Syntax
              Used to Form Encoding Rules in Various Routing Protocol
              Specifications", RFC 5511, DOI 10.17487/RFC5511, April
              2009, <https://www.rfc-editor.org/info/rfc5511>.

   [RFC6020]  Björklund, M., "YANG - A Data Modeling Language for the
              Network Configuration Protocol (NETCONF)", RFC 6020,
              DOI 10.17487/RFC6020, October 2010,
              <https://www.rfc-editor.org/info/rfc6020>.

   [RFC6940]  Jennings, C., Lowekamp, B., Rescorla, E., Baset, S., and
              H. Schulzrinne, "REsource LOcation And Discovery (RELOAD)
              Base Protocol", RFC 6940, DOI 10.17487/RFC6940, January
              2014, <https://www.rfc-editor.org/info/rfc6940>.

   [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>.

   [RFC8610]  Birkholz, H., Vigano, C., and C. Bormann, "Concise Data
              Definition Language (CDDL): A Notational Convention to
              Express Concise Binary Object Representation (CBOR) and
              JSON Data Structures", RFC 8610, DOI 10.17487/RFC8610,
              June 2019, <https://www.rfc-editor.org/info/rfc8610>.

Petit-Huguenin             Expires 11 May 2022                 [Page 72]
Internet-Draft           Computerate Specifying            November 2021

   [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>.

   [RFC8792]  Watsen, K., Auerswald, E., Farrel, A., and Q. Wu,
              "Handling Long Lines in Content of Internet-Drafts and
              RFCs", RFC 8792, DOI 10.17487/RFC8792, June 2020,
              <https://www.rfc-editor.org/info/rfc8792>.

   [RFC8941]  Nottingham, M. and P. Kamp, "Structured Field Values for
              HTTP", RFC 8941, DOI 10.17487/RFC8941, February 2021,
              <https://www.rfc-editor.org/info/rfc8941>.

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

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

   [Zave11]   Zave, P., Laboratories, T., and F. Park, "Experiences with
              Protocol Description", 2011,
              <https://www.researchgate.net/profile/Pamela_Zave/publicat
              ion/266230560_Experiences_with_Protocol_Description/
              links/56eaf9fb08ae9dcdd82a6590.pdf>.

   [Zotero]   "Zotero | Your personal research assistant", (accessed Oct
              06, 2021), <https://www.zotero.org/>.

Appendix A.  Command Line Tools

   |  Creation is in part merely the business of forgoing the great and
   |  small distractions.
   |  
   |  -- E. B. White

   The tooling supporting the techniques described in this document is
   designed to maximize the productivity by permitting to work
   disconnected from the Internet most of the time and from the World
   Wide Web at all times.

A.1.  Installation

   The computerate command line tools are run from 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/).

Petit-Huguenin             Expires 11 May 2022                 [Page 73]
Internet-Draft           Computerate Specifying            November 2021

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

   The Docker image is distributed as a BitTorrent, so a BitTorrent
   client is also needed to download the image.

   No other tools beyond these are needed after the image is installed,
   as it contains everything that is needed for the whole life cycle of
   computerate specifications, including git and the vim text editor.

   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.

   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:a4ba5275e0e52ce15a1896dacb5cfc0252c5dbff&dn=tools
   -15.tar.xz

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

      docker load -i tools-15.tar.xz

   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.

   After the first installation it is recommended to create an alias to
   make the use of the tools easier.  This can be done by installing the
   /opt/tools in your path:

      docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \
        computerate/tools computerate cp /opt/tools .
      sudo mv tools /usr/bin/

   The subsequent examples in this appendix will use this alias.

A.2.  Authoring a Computerate Specification

   The following sections explain how to use the various tools that are
   needed to author and process a computerate specification, but does
   not explain how a computerate specification should be formatted.

   Examples of formatting are available in the templates provided in the
   Docker image.

Petit-Huguenin             Expires 11 May 2022                 [Page 74]
Internet-Draft           Computerate Specifying            November 2021

A.2.1.  Using the Templates

   Writing a computerate specification from scratch is time-consuming,
   so a simpler way if to either duplicate an existing one, or to start
   with the templates that are provided in the Docker image.  Using the
   templates has the advantage that they also contain examples that are
   kept up to date with the tools and the specification.

   Run the following command to create a directory containing a
   computerate specification ready to be modified:

      tools cp -a /opt/computerate-template my-spec

A.2.2.  Converting an xml2rfc Document

   Another method to create a computerate specification is to start from
   an existing xml2rfc v3 (or v2 after conversion) document and to
   convert it.  The mnconvert tool, which is distributed in the Docker
   image, provides this facility:

      tools mnconvert <xml2rfc file>

   Note that the resulting document is not technically a computerate
   specification, as it does not contain Idris code.  The templates
   provided in the Docker image are useful to modify such converted
   document into a proper computerate specification.

A.2.3.  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 in computerate is
   disabled.

A.2.3.1.  Build a Bibliography with Zotero

   The simplest way to build a bibliography for a computerate document
   is to use [Zotero] and an [AsciiBib] exporter.

   After installing Zotero, the file "/opt/AsciiBib.js" from the Docker
   image must be copied in the "data/translators" directory where Zotero
   was installed.

Petit-Huguenin             Expires 11 May 2022                 [Page 75]
Internet-Draft           Computerate Specifying            November 2021

   To build a bibliography for an Internet-Draft, first create a new
   collection in Zotero and add items in it.  Then click-right on this
   collection, choose "Export Collection...", select the "AsciiBib
   format" and the directory where the computerate document is located.
   Then the last step is to add an "include::<collection>.adoc[]"
   statement in the computerate document.

   Note that not all types of of bibliographic items are yet converted
   into AsciiBib.  Other items can be added manually to the document as
   explained in the following section.

A.2.3.2.  Build a Bibliography Manually

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

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

   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

   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

A.3.  Processing a Computerate Specification

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

      tools computerate -t ietf -x txt <file>

Petit-Huguenin             Expires 11 May 2022                 [Page 76]
Internet-Draft           Computerate Specifying            November 2021

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

A.3.1.  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 "info" 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.4.  Other Commands

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

      tools idris2 <lidr-file>

   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.

   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

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

Petit-Huguenin             Expires 11 May 2022                 [Page 77]
Internet-Draft           Computerate Specifying            November 2021

      tools xml2rfc
      tools idnits --help
      tools aspell
      tools mnconvert

A.5.  Modified Tools

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

A.5.1.  Idris2

   URL:  https://github.com/idris-lang/Idris2.git
   Version:  0.5.1 commit 38e48be
   Modifications:

   *  Files with lipkg extension are processed as .ipkg literate files.
   *  An Idris file can be used in scripting mode by adding a shebang
      line.
   *  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.
   *  The "%cacheElab" directive permits to cache the result of an
      elaboration in the source code instead of been regenerated at each
      type-checking.
   *  The "--dg asciidoc" option can be used to generate on stdout the
      package documentation in AsciiDoc instead of HTML.
   *  Elaborations can be exported and documented.
   *  "package" and "depends" in ipkg file can use quoted strings.
   *  "--paths" now displays the paths after modification.
   *  Replace the literate processor by a faster one.  Remove support
      for reversed Bird style.

A.5.2.  asciidoctor

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

   *  Preprocessor and include processor for Idris literate source.
   *  Include processor for IdrisDoc generation.

A.5.3.  metanorma

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

Petit-Huguenin             Expires 11 May 2022                 [Page 78]
Internet-Draft           Computerate Specifying            November 2021

   *  Pass attribute "validate" when validating file.
   *  Generate the filename from the name header attribute.
   *  Process files with lidr and lipkg extensions.

A.5.4.  metanorma-ietf

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

   *  Fix transliteration.
   *  Fix < processing.
   *  Ignore obsolete rfc/@number.
   *  Insert seriesInfos in correct order.
   *  Add generation of json file.

A.5.5.  mnconvert

   URL:  https://github.com/metanorma/mnconvert
   Version:  1.11.0
   Modifications:

   *  Add format=rfc to references passthrough.
   *  Fix references, date.
   *  The resulting is formatted with one sentence per line.

A.5.6.  xml2rfc

   URL:  https://svn.ietf.org/svn/tools/xml2rfc /trunk
   Version:  3.11.1
   Modifications:

   *  Add appendices to JSON file.

A.5.7.  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.

Petit-Huguenin             Expires 11 May 2022                 [Page 79]
Internet-Draft           Computerate Specifying            November 2021

A.6.  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

   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 record fields.

   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 4

A.7.  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.

Petit-Huguenin             Expires 11 May 2022                 [Page 80]
Internet-Draft           Computerate Specifying            November 2021

Appendix B.  API Documentation

B.1.  Package computerate-specifying

   The Computerate Specification Standard Library.

   Version:  0.15
   Author(s):  Marc Petit-Huguenin
   Dependencies:  contrib

B.1.1.  Module ComputerateSpecifying

   A module with generic types that can be used to track identifiers and
   references.

   data Either' : (ty1 : List String -> List String -> Type) ->
   (ty2 : List String -> List String -> Type) ->
   (ids : List String) -> (refs : List String) -> Type
      Right : ty1 ids refs -> Either' ty1 ty2 ids refs

      Left : ty2 ids refs -> Either' ty1 ty2 ids refs

   data List' : (ty : List String -> List String -> Type) ->
   List String -> List String -> Type
      Nil : List' ty [] []

      (::) : ty ids refs -> List' ty idss refss ->
      checkUnique ids idss = True =>
      List' ty (ids ++ idss) (refs ++ refss)

   data Maybe' : (ty : List String -> List String -> Type) ->
   (ids : List String) -> (refs : List String) -> Type
      An optional value indexed by a list of identifiers and a list of
      references.

      Just : ty ids refs -> Maybe' ty ids refs

      Nothing : Maybe' ty [] []

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 11 May 2022                 [Page 81]
Internet-Draft           Computerate Specifying            November 2021

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

   data Names : Type -> Type

   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 a bit-vector filled with O values.

      m:  The length of the bitvector

   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 11 May 2022                 [Page 82]
Internet-Draft           Computerate Specifying            November 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 for 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 Denominate : List (Dimension, Int) -> Type
      A denominate number.

      Implements Asciidoc.

      MkDenominate : (x : Integer) -> (y : Integer) ->
      {xs : List (Dimension, Int)} -> Denominate xs

   data Dimension : Type
      The base dimensions, which includes the seven physical dimensions
      plus the user-defined quantity dimension.

      T : Dimension

Petit-Huguenin             Expires 11 May 2022                 [Page 83]
Internet-Draft           Computerate Specifying            November 2021

         Time.

      L : Dimension
         Length.

      M : Dimension
         Mass.

      I : Dimension
         Electric current.

      H : Dimension
         Thermodynamic temperature (tHeta).

      N : Dimension
         Amount of substance.

      J : Dimension
         Luminous intensity

      Q : (name : String) -> Dimension
         Quantity

      name:  Different quantities must be identified by different names.

   Dimensionless : Type
      The type of a dimensionless denominate number

   Info : Type
      The type of a denominate number for the information dimension.

   Length : Type
      The type of a denominate number for the length dimension.

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

      Implemented by List, (s, x).

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

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

   bit : Info
      Bit, the base unit of data.

Petit-Huguenin             Expires 11 May 2022                 [Page 84]
Internet-Draft           Computerate Specifying            November 2021

   byte : Info
      The byte unit, as 8 bits.

   day : Time
      The day, as unit of time.

   fromDenominate : (value : Denominate xs) ->
   (unit : Denominate xs) -> Double
      Convert a denominate number into a double calculated after
      applying a unit.

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

   fromDenominateToInt : (value : Denominate xs) ->
   (unit : Denominate xs) -> Int
      Convert a denominate number into a double calculated after
      applying a unit.

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

   fromDouble : Double -> {default 9 p : Nat} -> Denominate []
      Build a dimensionless denominate number from a double.

   fromInteger : Integer -> Denominate []
      Build a dimensionless denominate number from an integer.

   elaboration generate bin "bit" "Info"
      Generate all the IEC units of information, from kibibit to
      yobibit.

   elaboration generate dec "bit" "Info"
      Generate all the SI units of information, from kilobit to
      yottabit.

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

   hour : Time
      The hour, as unit of time.

   insert' : (Dimension, Int) -> (xs : List (Dimension, Int)) ->
   List (Dimension, Int)

   merge' : List (Dimension, Int) -> List (Dimension, Int) ->
   List (Dimension, Int)

Petit-Huguenin             Expires 11 May 2022                 [Page 85]
Internet-Draft           Computerate Specifying            November 2021

   meter : Length
      Meter, the base unit of length.

   minute : Time
      The minute, as unit of time.

   neg : Denominate xs -> Denominate xs
      The negation operation of a denominate number.

   none : Dimensionless
      The unit for a dimensionless denominate number.

   octa : Info
      The octa unit, as 64 bits.

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

   recip' : List (Dimension, Int) -> List (Dimension, Int)

   second : Time
      Second, the base unit of time.

   tetra : Info
      The tetra unit, as 32 bits.

   toDenominate : (Denominate [], Denominate xs) -> Denominate xs
      Build a denominate number from a tuple made of a dimensionless
      number and a unit.

   wyde : Info
      The wyde unit, as 16 bits.

B.1.5.  Module ComputerateSpecifying.Metanorma.Ietf

   A module used to generate an AsciiDoc fragment that can be inserted
   in a metanorma-ietf document with the goal of generating a valid
   xml2rfc v3 document.

   interface Asciidoc a
      Implemented by CrossFormat, CitationFormat, Inline, Block, List1,
      String, Int, Double.

      asciidoc : a -> String

   data Block : Type
      A block of text

Petit-Huguenin             Expires 11 May 2022                 [Page 86]
Internet-Draft           Computerate Specifying            November 2021

      Implements Asciidoc.

      Paragraph : (anchor : Maybe String) ->
      {default False keepWithNext : Bool} ->
      {default False keepWithPrevious : Bool} -> List1 Inline ->
      Block

      Source : (anchor : Maybe String) ->
      {default Nothing filename : Maybe String} ->
      {default Nothing type : Maybe String} ->
      {default Nothing markers : Maybe Bool} ->
      (src : Maybe String) -> (content : List String) -> Block

      Literal : (anchor : Maybe String) ->
      {default Nothing filename : Maybe String} ->
      {default Nothing type : Maybe String} ->
      (src : Maybe String) ->
      {default Nothing align : Maybe String} ->
      {default Nothing alt : Maybe String} -> Doc () -> Block

      Unordered : (anchor : Maybe String) ->
      {default (Just "1") type : Maybe String} ->
      {default (Just "1") start : Maybe String} ->
      (group : Maybe String) ->
      {default (Just "normal") spacing : Maybe String} ->
      {default (Just "adaptive") indent : Maybe String} ->
      List1 Line -> Block

      Definition : (anchor : Maybe String) ->
      {default (Just Normal) spacing : Maybe Spacing} ->
      {default (Just False) newline : Maybe Bool} ->
      {default (Just 3) indent : Maybe Int} ->
      (term : DefinitionTerm) -> (desc : DefinitionDef) -> Block

   data CitationFormat : Type
      Implements Asciidoc.

      Of : CitationFormat

      Comma : CitationFormat

      Parens : CitationFormat

      Bare : CitationFormat

   data CrossFormat : Type
      Implements Eq, Asciidoc.

Petit-Huguenin             Expires 11 May 2022                 [Page 87]
Internet-Draft           Computerate Specifying            November 2021

      Counter : CrossFormat

      Title : CrossFormat

      Default : CrossFormat

   data DefinitionDef : Type
      MkDefinitionDef : (anchor : Maybe String) ->
      (inline : List1 Inline) -> DefinitionDef

   data DefinitionTerm : Type
      MkDefinitionTerm : (anchor : Maybe String) ->
      (inline : List1 Inline) -> DefinitionTerm

   data Inline : Type
      Type to build inline elements.

      Implements Asciidoc.

      Text : String -> Inline
         Plain text.

      Must : Inline

      MustNot : Inline

      Required : Inline

      Shall : Inline

      ShallNot : Inline

      Should : Inline

      ShouldNot : Inline

      Recommended : Inline

      May : Inline

      Optional : Inline

      HardBreak : Inline
         An hard break.  NOTE: Not currently supported by metanorma-
         ietf.

      Contact : (initials : String) -> (surname : String) ->
      (fullname : String) -> Inline

Petit-Huguenin             Expires 11 May 2022                 [Page 88]
Internet-Draft           Computerate Specifying            November 2021

         Contact information.  NOTE: Not currently supported by
         metanorma-ietf.

      Comment : (anchor : Maybe String) -> (source : Maybe String) ->
      {default True display : Bool} -> (content : List Inline) ->
      Inline
         A comment.  NOTE: Not currently supported by metanorma-ietf.

         anchor:  An optional anchor.
         source:  An optional author for the comment.
         display:  False to prevent the comment to be rendered.
         content:  The comment itself.

      Italic : List Inline -> Inline
         A list of inline elements to be rendered in italics.

      Link : (target : String) -> (text : List Inline) -> Inline
         An embedded URI.

         target:  The URI.
         text:  Optional text to be rendered.

      Index : (item : String) ->
      {default Nothing subitem : Maybe String} ->
      {default False primary : Bool} -> Inline
         An indexed term.

      Citation : (target : String) -> (fragment : Maybe String) ->
      {default Of format : CitationFormat} ->
      (content : Maybe String) -> Inline
         A citation, i.e. a crossreference to a bibliographic reference.
         NOTE: Not currently supported by metanorma-ietf.

         target:  The anchor for the bibliographic reference.

      Bold : List Inline -> Inline
         A list of inline elements to be rendered in bold.

      Subscript : List Inline -> Inline
         A list of inline elements to be rendered in subscript.

      Superscript : List Inline -> Inline
         A list of inline elements to be rendered in superscript.

      Monospace : List Inline -> Inline
         A list of inline elements to be rendered in monospace.

      Unicode : Inline

Petit-Huguenin             Expires 11 May 2022                 [Page 89]
Internet-Draft           Computerate Specifying            November 2021

         One or more unicode characters.  NOTE: Not currently supported
         by metanorma-ietf.

      Cross : (target : String) ->
      {default Nothing format : Maybe CrossFormat} ->
      (content : List Inline) -> Inline
         A crossreference to an anchor in this document.

         target:  The URI.

      Attribute : String -> Inline
         An AsciiDoc attribute

   data Line : Type
      MkLine : (anchor : Maybe String) -> Line

B.1.6.  Module ComputerateSpecifying.Tpn

   A module that defines types for Petri Net.

   (>>) : Module xs a -> Module ys b -> Module (xs ++ ys) b

   (>>=) : Module xs a -> (a -> Module ys b) -> Module (xs ++ ys) b

   data Dir : Type
      The direction of the tokens exchanged between a port and a socket.

      In : Dir
         Tokens are moved outside the module.

      Out : Dir
         Tokens are moved inside the module.

      Both : Dir
         Tokens are moved in both directions.

   data Ellipse : Type -> Type
      Place : (n : String) -> (ty : Type) -> (c : Show ty) =>
      (init : List ty) -> Ellipse ty

      Port : (n : String) -> (ty : Type) -> (dir : Dir) -> Ellipse ty

   interface Enum a
      An interface to enumerate values for types that have a small
      number of possible values.

      Implemented by Bool.

Petit-Huguenin             Expires 11 May 2022                 [Page 90]
Internet-Draft           Computerate Specifying            November 2021

      enum : List a

   data InputArc : Type
      MkInputArc : (ellipse : Ellipse t) -> (output : Type) ->
      {default 0 delay : Nat} ->
      (inscription : List1 t -> Maybe output) -> InputArc

      InhibitorArc : (ellipse : Ellipse t) -> InputArc

      ResetArc : (ellipse : Ellipse t) -> InputArc

   InputType : List InputArc -> Type

   data Module : Vect k Type -> Type -> Type
      A module.

      AddPlace : (e : Ellipse t) -> Module [] (Ellipse t)

      AddPort : (e : Ellipse t) -> Module [t] (Ellipse t)

      AddTransition : (name : String) -> (is : List InputArc) -> (uni
      : List (Fin (length is), (Nat, (Fin (length is), Nat)))) ->
      (os : List OutputArc) -> (tis : Type) -> (tos : Type) ->
      (tis -> Maybe tos) -> {default 0 delay : Nat} -> Module [] ()

      AddInstance : (name : String) -> (mod : Module xs ()) ->
      (map : EllipseList xs) -> Module [] ()

      Bind : Module xs a -> (a -> Module xs' b) ->
      Module (xs ++ xs') b

   data OutputArc : Type
      MkOutputArc : (input : Type) -> (ellipse : Ellipse t) ->
      {default 0 delay : Nat} -> (inscription : input -> List t) ->
      OutputArc

   OutputType : List OutputArc -> Type

   data Timed : Type -> Type
      A wrapper that converts a type into a timed type.

      Implements Show.

      MkTimed : a -> {default 0 time : Nat} -> Timed a

   data Top : Type
      The type of a top TPN module.

Petit-Huguenin             Expires 11 May 2022                 [Page 91]
Internet-Draft           Computerate Specifying            November 2021

      MkTop : Module [] _ -> Top

   data Transition : Type
      MkTransition : List Int -> Int -> Transition

   addPriorities : Top -> Top
      Adds transitions to a top TPN such as the priority annotation on
      transitions is taken in account.  Not implemented yet

   addStep : Top -> Top
      Adds a new global place and transitions to a top TPN such as that
      global place contains the number of steps.  Not implemented yet

   addTime : Top -> Top
      Adds a new global place and transitions to a top TPN such as that
      global place contains the current time.  Not implemented yet

   bindings : Marking xs -> Top -> Transition -> List Binding
      List all the bindings from a marking and a transition.  Not
      implemented yet.

   deriveType : Top -> List Decl
      Not implemented yet.

   doTransition : Marking xs -> Top -> Transition -> Binding ->
   Marking xs
      Transition to a new marking Not implemented yet.

   enabledTransitions : Top -> Marking xs -> List Transition
      List all the enabled transitions in a top TPN from a specific
      marking.  Not implemented yet.

   free : (t : Type) -> Show t => Enum t => (is : List InputArc) ->
   (os : List OutputArc) ->
   ((t, InputType is) -> Maybe (OutputType os)) -> Module [] ()
      Declare a transition with one free variable.

   inhibitor : (ellipse : Ellipse t) -> InputArc
      An inhibitor arc.

      ellipse:  The ellipse that, when empty, will trigger the
         transition.

   initialMarking : Top -> (p * (ys : Vect p Type * Marking ys))
      Builds an initial marking.

Petit-Huguenin             Expires 11 May 2022                 [Page 92]
Internet-Draft           Computerate Specifying            November 2021

   input : (ellipse : Ellipse t) -> (output : Type) ->
   {default 0 delay : Nat} ->
   (inscription : List1 t -> Maybe output) -> InputArc
      An input arc.

      ellipse:  The ellipse from which tokens are removed.
      output:  The type of the tokens after applying the inscription.
      delay:  The delay from which the transition can be preempted,
         defaults to 0.
      inscription:  A function that converts the tokens from the place
         into the output type.

   instance : (name : String) -> (mod : Module xs ()) ->
   (mappings : EllipseList xs) -> Module [] ()
      Declare an instance of a module.

      name:  The name of the instance, for documentation purpose.
      mod:  The module to import.
      mappings:  The list of local port or place, each mapping to a port
         exported by the imported module.

   one : List1 a -> Maybe a
      A function to use on an input arc to pass a single value without
      additional constraints.

   output : (input : Type) -> (ellipse : Ellipse t) ->
   {default 0 delay : Nat} -> (inscription : input -> List t) ->
   OutputArc
      An output arc.

      input:  The type of the values from the transition.
      ellipse:  The ellipse into which tokens are inserted.
      delay:  The delay added by the arc, defaults to 0.
      inscription:  a function that generates the tokens to be inserted
         in the place.

   place : (name : String) -> (ty : Type) -> Show ty =>
   {default empty init : List ty} -> Module [] (Ellipse ty)
      Declare a place local to this module.

      name:  The name of the place, for documentation purpose.
      init:  The initial list of tokens, defaults to the empty list.

   port : (name : String) -> (ty : Type) -> (dir : Dir) ->
   Module [ty] (Ellipse ty)
      Declare a port local to this module.

      name:  The name of the port, for documentation purpose.

Petit-Huguenin             Expires 11 May 2022                 [Page 93]
Internet-Draft           Computerate Specifying            November 2021

      dir:  The direction of the tokens.

   reset : (ellipse : Ellipse t) -> InputArc
      An inhibitor arc.

      ellipse:  The ellipse that will be emptied when the transition
         will be triggered.

   timed : a -> {default 0 time : Nat} -> Timed a
      Wrap a value into a timed value.

      time:  The time of this token, defaults to 0.

   top : Module [] _ -> Top
      A top is a module with an empty list of ports.  Only top values
      can be used in simulations.

   transition : (name : String) -> (inputs : List InputArc) ->
   (unifications : List (Fin (length inputs), (Nat, (Fin (length
   inputs), Nat)))) -> (outputs : List OutputArc) ->
   (inscription : InputType inputs -> Maybe (OutputType outputs)) ->
   {default 0 delay : Nat} -> Module [] ()
      Declare a transition.

      name:  The name of the transition, for documentation purpose.
      inputs:  The list of input arcs.
      unifications:  The list of unifications between input values.
      outputs:  The list of output arcs.
      inscription:  A function that converts the input tokens into
         output tokens.
      delay:  The delay added by the transition.

   untimed : (v : Timed a) -> a
      Unwrap a timed value into a value.

      v:  the timed value to unwrap.

      == 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.

Petit-Huguenin             Expires 11 May 2022                 [Page 94]
Internet-Draft           Computerate Specifying            November 2021

      tree:  The tree to modify.
      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.

Petit-Huguenin             Expires 11 May 2022                 [Page 95]
Internet-Draft           Computerate Specifying            November 2021

      MkUnsigned : BitVector m -> Unsigned m

B.2.  Package rfc5234

   Version:  0.2
   Author(s):  Marc Petit-Huguenin
   Dependencies:  computerate-specifying, contrib

B.2.1.  Module RFC5234

   A module to generate a valid ABNF.

   () : {c1 : Bool} -> {c2 : Bool} -> Abnf c1 -> Lazy (Abnf c2) ->
   Abnf (c1 && c2)
      Declare the alternation of two ABNF rules.

   (>>) : {c1 : Bool} -> {c2 : Bool} -> Abnf c1 ->
   inf c1 (Abnf c2) -> Abnf (c1 || c2)
      Declare the concatenation of two ABNF rules.  The "do" notation
      uses that operator.

   data Valid : (l : List Int) -> (g : Abnf c) -> Type
      Implements Asciidoc, Pretty.

      VEmpty : Valid [] Empty

      VTerminal : (x : Int) -> Valid [x] (Terminal x)

      VThenEat : Valid xs l -> Valid ys r ->
      Valid (xs ++ ys) (ThenEat l r)

      VThenEmpty : Valid xs l -> Valid ys r ->
      Valid (xs ++ ys) (ThenEmpty l r)

      VAltLeft : Valid xs l -> Valid xs (Alt l r)

      VAltRight : Valid xs r -> Valid xs (Alt l r)

      VStar :
      Valid xs (Alt Empty (ThenEat e (Repeat Nothing Nothing e))) ->
      Valid xs (Repeat Nothing Nothing e)

   binRange : (f : Int) -> (t : Int) -> Abnf True
      Declare a range of alternative values to be displayed in binary.

      f:  The first value of the range.
      t:  The last value of the range.

Petit-Huguenin             Expires 11 May 2022                 [Page 96]
Internet-Draft           Computerate Specifying            November 2021

   binTerm : (v : Int) -> Abnf True
      Declare an ABNF terminal value to be displayed in binary.

      v:  The value

   binTerms : (vs : List1 Int) -> Abnf True
      Declare a concatenated string of ABNF terminal values to be
      displayed in binary.

      vs:  The values

   comment : String -> Abnf False
      Add a comment

   decRange : (f : Int) -> (t : Int) -> Abnf True
      Declare a range of alternative values to be displayed in decimal.

      f:  The first value of the range.
      t:  The last value of the range.

   decTerm : (v : Int) -> Abnf True
      Declare an ABNF terminal value to be displayed in decimal.

      v:  The value

   decTerms : (vs : List1 Int) -> Abnf True
      Declare a concatenated string of ABNF terminal values to be
      displayed in decimal.

      vs:  The values

   empty : Abnf False

   exact : Nat -> Abnf c -> Abnf c
      Declare a specific repetition of ABNF rules.

   group : Abnf c -> Abnf c
      Declare a sequence group of ABNF rules.

   hexRange : (f : Int) -> (t : Int) -> Abnf True
      Declare a range of alternative values to be displayed in
      hexadecimal.

      f:  The first value of the range.
      t:  The last value of the range.

   hexTerm : (v : Int) -> Abnf True
      Declare an ABNF terminal value to be displayed in hexadecimal.

Petit-Huguenin             Expires 11 May 2022                 [Page 97]
Internet-Draft           Computerate Specifying            November 2021

      v:  The value

   hexTerms : (vs : List1 Int) -> Abnf True
      Declare a concatenated string of ABNF terminal values to be
      displayed in hexadecimal.

      vs:  The values

   inc : (n : String) -> (d : Abnf c) -> Abnf c
      Declare an incremental ABNF Rule.

      n:  The name of the rule.
      d:  The definition of the rule

   many : Quantity
      A repetition quantity equivalent to `"*`".

   optional : {c : Bool} -> Abnf c -> Abnf c
      Declare an optional sequence of ABNF rules.

   repeat : (q : Quantity) -> Abnf c -> Abnf c
      Declare a variable repetition of ABNF rules.

      q:  The repetition quantity.

   rule : (n : String) -> (d : Abnf c) -> Abnf c
      Declare an ABNF Rule. # d The definition of the rule

      n:  The name of the rule.

   some : Quantity
      A repetition quantity equivalent to `"1*`".

   string : (s : String) -> Abnf (isSucc (length s))
      Declare an ABNF literal text string.

      s:  The string.

      == Module RFC5234.Core

   The ABNF Core rules.  These rules can be used directly in an ABNF
   grammar by using the name of the function.

   alpha : Abnf True
      An ASCII alphabetic character.

   bit : Abnf True
      A "0" or "1" ASCII character.

Petit-Huguenin             Expires 11 May 2022                 [Page 98]
Internet-Draft           Computerate Specifying            November 2021

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

   cr : Abnf True
      A Carriage Return ASCII character.

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

   ctl : Abnf True
      Any ASCII control character.

   digit : Abnf True
      Any ASCII digit.

   dquote : Abnf True
      A double-quote ASCII character.

   hexdig : Abnf True
      Any hexadecimal ASCII character, including lower and upper case.

   htab : Abnf True
      An ASCII horizontal tab.

   lf : Abnf True
      A Line Feed ASCII character.

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

   octet : Abnf True
      A 8-bit value.

   sp : Abnf True
      A ASCII space.

   vchar : Abnf True
      A printable ASCII character.

   wsp : Abnf True
      A space or horizontal tab.

B.3.  Package augmented-ascii-diagrams

   The Augmented Packet Header Diagrams package

Petit-Huguenin             Expires 11 May 2022                 [Page 99]
Internet-Draft           Computerate Specifying            November 2021

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

B.3.1.  Module APHD

   A DSL to describe Augmented Packet Header Diagrams.

B.4.  Package rfc791

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

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.

      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 {m = 1} => (df : BitVector 1) ->
      (mf : BitVector 1) -> Flags

Petit-Huguenin             Expires 11 May 2022                [Page 100]
Internet-Draft           Computerate Specifying            November 2021

   data InternetHeader : Type
      Internet Protocol Header.

      MkInternetHeader : (version : BitVector 4) ->
      version = [O, I, O, O] => (ihl : (Unsigned 4, Info)) ->
      snd ihl = Dimension.tetra => (tos : Tos) ->
      (length : (Unsigned 16, Info)) ->
      snd length = Dimension.wyde => (id : Unsigned 16) ->
      (flags : Flags) -> (offset : (Unsigned 13, Info)) ->
      snd offset = Dimension.octa => (ttl : (Unsigned 8, Time)) ->
      snd ttl = Dimension.second => (protocol : BitVector 16) ->
      (checksum : BitVector 16) -> (source : IP) -> (dest : IP) ->
      (options : List Option) -> (padding : BitVector n) ->
      n = pad 32 options => padding = bitVector {m = 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.

      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

Petit-Huguenin             Expires 11 May 2022                [Page 101]
Internet-Draft           Computerate Specifying            November 2021

      Implements Size.

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

   pad : Size x => Nat -> x -> Nat

Appendix C.  Errata Statistics

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

   The relabeling uses the following labels:

Petit-Huguenin             Expires 11 May 2022                [Page 102]
Internet-Draft           Computerate Specifying            November 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 11 May 2022                [Page 103]
Internet-Draft           Computerate Specifying            November 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.

Appendix D.  Converting From a Colored Petri Net

   As explained in this document, for now the workflow is to prepare a
   Colored Petri Net with the cpntools software, and then manually
   translate that Petri Net into an Idris Type using the "Tpn"
   (Section 8.1.7) module, as explained in the following sections.

   Colored Petri Nets are explained in [Jensen09] and in [Cpntools].
   [Aalst11] is also a good introduction to Colored Petri Nets.

Petit-Huguenin             Expires 11 May 2022                [Page 104]
Internet-Draft           Computerate Specifying            November 2021

D.1.  Convert Color Sets

   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 language 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 a
   TPN.

   The following sections explain how to convert a CPN Color Set into an
   Idris type.  It refers to webpages at [Cpntools], and the Idris
   examples shown below are translations of the CPN ML examples in these
   pages.  CPN's with clauses can be translated as added constraints to
   simple dependent types.

      |  NOTE: In Idris, types and constructors share the same
      |  namespace, so they need to have different names.  Also types
      |  (including functions that return a value of type "Type") and
      |  constructors start with an uppercase letter.

D.1.1.  Simple Color Sets

D.1.1.1.  Unit Color Sets

   See http://cpntools.org/2018/01/09/unit-color-set/ for the definition
   of the CPN unit color set.

   The unit color set can be replaced by the "()" type:

      > U : Type
      > U = ()

   For int color sets using a with clause, a dependent type can be
   created:

      > data E = MkE

D.1.1.2.  Boolean Color Sets

   See http://cpntools.org/2018/01/09/boolean-color-set/ for the
   definition of the CPN bool color set.

   The bool color set can be replaced by the "Bool" type.

      > B : Type
      > B = Bool

Petit-Huguenin             Expires 11 May 2022                [Page 105]
Internet-Draft           Computerate Specifying            November 2021

   For bool color sets using a with clause, a dependent type can be
   created:

      > data Answer = No | Yes

D.1.1.3.  Integer Color Sets

   See http://cpntools.org/2018/01/09/integer-color-sets/ for the
   definition of the CPN int color set.

   The int colour set can be replaced by the "Int" type.

      > INT : Type
      > INT = Int

   For int color sets using a with clause, a dependent type can be
   created:

      > data SmallInt : Type where
      >   MkSmallInt : (i : Int) -> i >= 1 && i <= 10 = True => SmallInt

D.1.1.4.  Large Integer Color Sets

   See http://cpntools.org/2018/01/09/large-integer-color-sets/ for the
   definition of the CPN intinf color set.

   The intinf colour set can be replaced by the "Integer" type.

      > INTINF : Type
      > INTINF = Integer

   For intint color sets using a with clause, a dependent type can be
   created:

      > data SmallLargeInt : Type where
      >   MkSmallLargeInt : (i : Integer) -> i >= 1 && i <= 10 = True =>
      >     SmallLargeInt

D.1.1.5.  Real Color Sets

   See http://cpntools.org/2018/01/09/real-color-sets/ for the
   definition of the CPN real color set.

   The real color set can be replaced by the "Double" type.

      > R : Type
      > R = Double

Petit-Huguenin             Expires 11 May 2022                [Page 106]
Internet-Draft           Computerate Specifying            November 2021

   For real color sets using a with clause, a dependent type can be
   created:

      > data SomeReal : Type where
      >   MkSomeReal : (d : Double) -> d >= 1.0 && d <= 10.0 = True =>
      >     SomeReal

D.1.1.6.  String Color Sets

   See http://cpntools.org/2018/01/09/string-color-sets/ for the
   definition of the CPN string color set.

   The string color set can be replaced by the "String" type.

      > S : Type
      > S = String

   For string color sets using a with clause, a dependent type can be
   created:

      > data LowerString : Type where
      >   MkLowerString : (s : String) ->
      >     all (\c => c >= 'a' && c <= 'z') (unpack s) = True =>
      >     LowerString

   Similarly for string color sets using an and clause:

      > data SmallString : Type where
      >   MkSmallString : (s : String) ->
      >     all (\c => c >= 'a' && c <= 'd') (unpack s) = True =>
      >     length s >= 3 && length s <= 9 = True =>
      >     SmallString

D.1.1.7.  Enumerated Color Sets

   See http://cpntools.org/2018/01/09/enumeration-color-set/ for the
   definition of the CPN with color set.

   A with color set can be implemented as a Sum type:

      > data Day = Mon | Tues | Wed | Thurs | Fri | Sat | Sun

D.1.1.8.  Index Color Sets

   See http://cpntools.org/2018/01/09/index-color-sets/ for the
   definition of the CPN index color set.

   An index color set can be implemented as a dependent type:

Petit-Huguenin             Expires 11 May 2022                [Page 107]
Internet-Draft           Computerate Specifying            November 2021

      > data PH : Type where
      >   MkPH : (i : Nat) -> i >= 1 && i <= 5 = True => PH

D.1.2.  Compound Color Sets

   Compound color sets are color sets that combine simple colors sets
   and compound color sets together.

D.1.2.1.  Product Color Sets

   See http://cpntools.org/2018/01/09/product-color-sets/ for the
   definition of the CPN product color set.

   The product color set can be replaced by the "Pair a b" type, which
   can also be represented as a tuple.

      > P : Type
      > P = (U, I)

D.1.2.2.  Record Color Sets

   See http://cpntools.org/2018/01/09/record-color-sets/ for the
   definition of the CPN record color set.

   The record color set can be replaced by a record type.

      > record PACK where
      >   se : SITES
      >   re : SITES
      >   no : INT

D.1.2.3.  List Color Sets

   See http://cpntools.org/2018/01/09/list-color-sets/ for the
   definition of the CPN list color set.

   The list color set can be replaced by a "List a" type.

      > INTlist : Type
      > INTlist = List INT

   For list color sets using a with clause, a dependent type can be
   created:

      > data ShortBoolList : Type where
      >   MkShortBoolList : (l : List Bool) ->
      >     length l <= 2 && length l >= 4 = True =>
      >     ShortBoolList

Petit-Huguenin             Expires 11 May 2022                [Page 108]
Internet-Draft           Computerate Specifying            November 2021

D.1.2.4.  Union Color Sets

   See http://cpntools.org/2018/01/09/union-color-sets/ for the
   definition of the CPN union color set.

   The union color set can be replaced by a Sum type.

      > data Packet : Type where
      >   Data_ : DATA -> Packet
      >   Ack : Packet

D.1.2.5.  Subset Color Sets

   See http://cpntools.org/2018/01/09/subset-color-sets/ for the
   definition of the CPN subset color set.

   A subset color set can be replaced by a dependent type:

      > data EvenInt : Type where
      >   MkEvenInt : (i : Int) -> i `mod` 2 = 0 => EvenInt

D.1.2.6.  Alias Color Sets

   See http://cpntools.org/2018/01/09/alias-color-sets/ for the
   definition of the CPN alias color set.

   The alias color set can be replaced by a type function:

      > WholeNumber : Type
      > WholeNumber = INT

      > DayOff : Type
      > DayOff = Weekend

D.1.3.  Timed Color Sets

   See http://cpntools.org/2018/01/09/timed-color-sets/ for the
   definition of CPN timed color sets.

   To convert a Timed color set, just wrap it in the "Timed a" type.

      > IT : Type
      > IT = Timed Int

      > P2 : Type
      > P2 = Timed (Bool, IT)

Petit-Huguenin             Expires 11 May 2022                [Page 109]
Internet-Draft           Computerate Specifying            November 2021

D.1.4.  Size of Color Sets

   See http://cpntools.org/2018/01/09/size-and-complexity-of-color-sets/
   for the definition of the size of CPN color sets.

   In a TPN, types that are considered small should have an
   implementation of "Enum a" that enumerates all the possible values
   for that type.

   Here's the implementation for the type Day defined above:

      > Enum Day where
      >   enum = [Mon, Tues, Wed, Thurs, Fri, Sat, Sun]

D.2.  Convert Places

   See http://cpntools.org/2018/01/09/place-inscriptions/ for the
   definition of CPN places.

   Converting a CPN Place is straightforward.  It is done by using the
   function "place".

   *  The name of the place goes into the first parameter of the
      function.  Note that all places in a module must have different
      name.

   *  The color, after conversion as explained in Appendix D.1, goes
      into the second parameter.

   *  The marking initialization, after conversion into a "List a" of
      the place type, goes into the implicit parameter "init", which by
      default takes the "empty" value.

   E.g., the "Packets To Send" Place in Figure 1 of [Jensen07] can be
   translated as follow:

      >   packetsToSend <- place "Packets To Send" NoxData
      >     {init=[(1, "COL"), (2, "OUR"), (3, "ED "),
      >     (4, "PET"), (5, "RI "), (6, "NET")]}

   Note that some of the tokens in use in Petri Net places are meant to
   represent network PDUs.  It is recommended to use for that abstract
   types instead of wire types and to provide a proof of isomorphism as
   explained in Section 5.3.1.

Petit-Huguenin             Expires 11 May 2022                [Page 110]
Internet-Draft           Computerate Specifying            November 2021

D.3.  Convert Transitions

   See http://cpntools.org/2018/01/09/transition-inscriptions/ for the
   definition of CPN transitions.

   Converting a CPN transition into a TPN transition is done by using
   the "transition" function.  This function takes 4 parameters: a name,
   a list of input arcs, a list of output arcs and a function that
   combines both unification of bindings and the execution of the
   transition's guard.

   In a Timed TPN, the implicit delay parameter can be set to the time
   that will be added to be tokens generated by this transition.

   Before starting the conversion, CPN doubled-headed arcs need to to be
   duplicated, once as an input arc and once as an output arc, but with
   the same inscription.

D.3.1.  Convert Arcs

   See http://cpntools.org/2018/01/09/arc-inscriptions/ for the
   definition of CPN arcs.

D.3.1.1.  Convert Free Variables

   A free variable can be added to a transition by using the "free"
   function instead of the "transition" and passing the type of the free
   variables as first parameter.  In that case the value of the free
   variable (which is randomly selected from the possible values for the
   type

   E.g., the use of the free variable "success" of top of Figure 1 of
   [Jensen07] can be translated as follow:

      >   free Bool
      >     [input a NoxData one]
      >     [output NoxData b pure]
      >     (\(success, n, d) => if success then pure (n, d) else empty)

D.3.1.2.  Convert Input Arcs

   Before the CPN input arc conversion, arcs that can take multiple
   tokens at once from a place must be duplicated, one for each token.

   Each TPN input arc is built by the "input" function.  This function
   takes 3 parameters: a place, a type, and a function that is converted
   from the inscription.

Petit-Huguenin             Expires 11 May 2022                [Page 111]
Internet-Draft           Computerate Specifying            November 2021

   In a Timed TPN, the implicit delay parameter can be set to the
   preemptive time that a timed token can be that be removed from the
   place.

   The type of the TPN input arc must be a tuple of the type of each
   variable used by the CPN input arc inscription.  The domain of the
   function is the type of the place, its codomain is the type of the
   input arc.

   The function itself takes as input one token from the place and
   returns an optional tuple of values, one for each variable.  The
   returned value is optional so the function can indicate that no token
   are valid for that transition.

   E.g., the input arc in the top left of Figure 1 of [Jensen07] can be
   translated as follow:

      >     input packetsToSend NoxData one

   In that case the function, defined as a lambda, can be simplified as
   just "pure".

D.3.1.3.  Convert Inhibitor Arcs

   Although they are not described in the cpntools web site, inhibitor
   arcs are implemented in cpntools.

   Each TPN inhibitor arc is built by the "inhibitor" function.  This
   function does not carry an inscription and must be considered as
   generating a "()" token when the place is empty.

D.3.1.4.  Convert Reset Arcs

   Although they are not described in the cpntools web site, reset arcs
   are implemented in cpntools.

   Each TPN reset arc is built by the "reset" function.  This function
   does not carry an inscription and must be considered as always
   generating a "()" token that will empty the place when the transition
   is triggered.

D.3.1.5.  Convert Output Arcs

   Each TPN output arc is built by the "output" function.  This function
   takes 3 parameters: a type, a place, and the function that is
   converted from the function.

Petit-Huguenin             Expires 11 May 2022                [Page 112]
Internet-Draft           Computerate Specifying            November 2021

   In a Timed TPN, the implicit delay parameter can be set to the time
   that will be added to be tokens generated by this arc.

   The type of the TPN output arc must be a tuple of the type of each
   variables used by the CPN arc inscription.

   The function itself takes as input a tuple of values, one for each
   variable used by the CPN arc function, and returns a list of values
   to be inserted in the place.  The returned value is a list so 0, one
   or more token can be inserted at once.,

   E.g., the output arc in the arc in the bottom right left of Figure 1
   of [Jensen07] can be translated as follow:

      >     output (NO, NO) c (\(n, k) =>
      >       if n == k then pure (k + 1) else (pure k))

D.3.2.  Convert Transition Inscription

   The function in a TPN transition is assembled from two parts in the
   CPN transition: from the unification of variables defined in CPN
   input arcs with the same name and from the guard boolean expression.

D.3.2.1.  Unification

   The variables to unify are all the variables that hold the same name
   but in different input arc inscriptions.

   To unify two variables, first they need each to be transformed into a
   pair of indexes.  The first element of the pair is the index of the
   input that contains the variable.  The second element is the index of
   the variable in the codomain of the inscription in that input.

   Then 2 pairs of elements can be converted in a 4-tuple that express
   the constraint that these two variables must be unified.  Finally the
   4-tuplaes are added to a list of all the unifications needed for that
   transition.

   E.g., the unification part for the transition in the top left of
   Figure 1 of [Jensen07] can be translated as follow:

   Here the first pair (0, 0) means the No in the NoxData pair in the
   first input.  The second pair, (1. 0), means the (unique) No in the
   second input.

Petit-Huguenin             Expires 11 May 2022                [Page 113]
Internet-Draft           Computerate Specifying            November 2021

      >   transition "send packet"
      >     [input packetsToSend NoxData one,
      >      input nextSend NO one]
      >     [(0, 0, 1, 0)]
      >     [output NoxData packetsToSend pure,
      >      output NO nextSend pure,
      >      output NoxData a pure]
      >     (\((n, d), n') => pure ((n, d), n, (n, d)))

   Here "n" is coming from the "packetsToSend" place, whereas "n'" is
   coming from the "nextSend" place.

D.3.2.2.  Guards

   See http://cpntools.org/2018/01/09/guards/ for the definition of CPN
   guards.

   Converting guards is straightforward, as the boolean expression is
   simply tested and returns empty if the result is false.

   E.g., the guard on the left side of Figure 42 of [Jensen07] can be
   translated as follow:

      >   transition "remove packet"
      >     [input packetsToSend NoxData one,
      >      input nextSend NO one]
      >     empty
      >     [output NO nextSend pure]
      >     (\((n, d), k) => if n < k then pure n else empty)

D.4.  Convert Substitution Transitions

   See http://cpntools.org/2018/01/09/substitution-transitions/ for the
   definition of CPN substitution transitions.

   A CPN substitution transition is called an instance in TPN.  An
   instance is how a reusable module is inserted into another module.

   A substitution is created by moving places, transitions, and
   instances from an existing module into a new module.  Then places
   that will be shared with another module are modified into ports, with
   the same type.

   Then a new instance referencing that new module is inserted in place
   of the places, transitions, and instances that were removed in the
   original module.

Petit-Huguenin             Expires 11 May 2022                [Page 114]
Internet-Draft           Computerate Specifying            November 2021

   Finally the mapping list in the new instance must list either ports
   or places that are to be mapped to the port exported by the new
   instance.  In CPN the places and ports that are mapped to the ports
   exported by a module in an instance are called sockets.

D.5.  Convert Fusion Places

   See http://cpntools.org/2018/01/09/fusion-places/ for the definition
   of CON fusion places.

   A fusion place, which is the duplication of a place where all
   duplicates share the same content, is used in CPN either in the same
   module, or in different modules.

   The former case exists only to help some user interface issues, so a
   fusion places in the same module can safely use a unique TPN place.

   For the latter case, each fusion place must be converted into a TPN
   port of the modules where they are used.  Then the mapping for that
   port in the TPN instance that use these modules must reference the
   same local port.  This process must continue up to the level where
   all the ports for the fusion places converge, and have a unique place
   mapped to all these ports.

Appendix E.  Evidence-Based Answers

   This document uses a special interpretation of Programs and Types
   that permits to build evidence-based answers to the kind of questions
   that a network protocol designer would be asking of its designs.

   Although that interpretation is not new, few textbooks are available
   to concretely learn it and even when available, these textbooks
   generally take the long road by choosing to teach first Constructive
   Logic and then apply these teaching to Programs and Types.  As there
   is in fact an even longer road that would take from Fibred Category
   Theory to Constructive Logic and then to Programs and Types, it is
   reasonable to think that there should be a shortcut there that would
   permit to start directly with Programs and Types, especially when the
   target audience is programmers, a segment of the technical population
   that is known to dislike mathematics.

   Still, the mathematically inclined or the non-programmer can look at
   [Nederpelt14], [Bornat05], or [Mimram20] for an approach based on
   mathematics.

   Basically the goals of that interpretation of Program and Types are:

   *  To answer any question with either "Yes", "No", or "Don't know".

Petit-Huguenin             Expires 11 May 2022                [Page 115]
Internet-Draft           Computerate Specifying            November 2021

   *  To ensure that any "Yes" or "No" answer is provided with evidence.
   *  To use programming to achieve these goals.

   The kind of questions that a network protocol designer may want to
   get that kind of evidence-based questions for are many:

   *  Is my new version of the protocol safe to interoperate with the
      previous versions?
   *  Is the protocol free of deadlock?
   *  Is there corner cases that I neglected to take in account.
   *  Is that faster but more efficient protocol equivalent to the
      slower but simpler original protocol?

   Notice that when we talk about evidence-based answers, we exclude by
   definition any answer that has a probability different of 0.0 or 1.0,
   and furthermore exclude evidence-free answers like the ones given by
   AI/ML.

   As a consequence, we have to admit that there are questions that do
   not have an evidence-based answer.  That could be for a short list of
   reasons:

   *  We did not looked in the literature yet if there is an existing
      answer to a particular question.
   *  Nobody yet tried to find an answer to that question.
   *  Nobody found an answer to the question yet.
   *  There is no answer to that question.

   There is clearly a question of locality of our knowledge at play
   here, and we are not pretending to get to some absolute truth with
   this technique.

E.1.  Encoding Questions

   In the 90s came this new idea that it was possible to use the C++
   type system to encode calculations.  A famous example was generating
   all the prime numbers during the compilation of a C++ program.  The
   result was provided as a result of compiling the program, and the
   compiled program itself was irrelevant to get that result.  This was
   done by reinterpreting the type system into a computational system.

   Here we are going to do the same thing, and reinterpret the type
   system of a programming language, Idris, as a way to encode our
   questions.

   As we will see, to be able to do this reinterpretation, the type
   system needs to be stronger than in a traditional programming
   language so to be able to encode a large variety of questions.  We

Petit-Huguenin             Expires 11 May 2022                [Page 116]
Internet-Draft           Computerate Specifying            November 2021

   will also see that, paradoxically, the computational power of our
   programming language needs to be reduced to be sure that the evidence
   of our answers is valid.

   One defining feature of that programming language is that the
   compilation step that in traditional programming languages is
   monolithic, is here split in 2 separate steps:

   *  The typechecking step takes a set of source files and verifies
      that all values in these sources (including the code as a value of
      the function type) can be assigned to the correct type.  Because
      of the complexity of the type system, an Idris interpreter is used
      to evaluate expressions during the typechecking step.

   *  The code generation step generates executable code.

   As our interpretation relies only on what happens in the typechecking
   step, we have no use for the second step of the compilation process.

E.1.1.  Any Value of a Type is Evidence of Yes

   The cornerstone of our new interpretation is that the evidence that
   the answer of a question is Yes is an value of the type that encodes
   that question.  We will see later that the evidence that the answer
   is No is the inability to produce a value of a type.

   Although there is no real usage for these, if we interpret the basic
   types in our programming languages as questions, then the answers to
   these are always Yes, because we can always find a value for these
   types:

      1 : Int

      "s" : String

   In Idris a value of a type is written first, then followed by a colon
   and by the type of that value.

   Note that it does not matter if you can find one or two millions
   different pieces of evidence - the answer is still Yes. The exact
   value we pick as evidence is absolutely irrelevant, which is
   something that may seems strange to a programmer.

   This is why basic types are not really interesting in our
   interpretation, as their answer is always Yes.

Petit-Huguenin             Expires 11 May 2022                [Page 117]
Internet-Draft           Computerate Specifying            November 2021

E.1.2.  Function Type As Implication

   Idris is a pure functional programming language, so functions are
   first class citizens of the language, and their type is called a
   Function Type.

   The interpretation of a Function Type is that of an implication.
   Implications are a form of "if P then Q" statement, that says
   something about the relationship between two other Types, here P and
   Q.

   In Idris the Function Type is represented as an arrow that separate
   the first type (sometimes called the domain of the function) from the
   second type (sometimes called the codomain of the function).

      P -> Q

   To answer the question "P -> Q" we need to find a value of that type.
   An value of a Function Type is a program, so a program that takes
   values of P as parameter and returns a value of Q is an evidence that
   the answer to "P -> Q" is Yes. Another equivalent reading would be
   "Assuming that we can provide values for P and values for Q, then can
   we provide a function that typechecks?"

   Notice again that there maybe many programs that fulfill that
   condition but again that is irrelevant, as we need only one to serve
   as evidence.

   We can easily produce an evidence of that, let's say using Int and
   String as our types:

      \x => "a" : Int -> String

   The expression on the left of the colon is a lambda expression. "x"
   will be bound to whatever value of Int will be passed as parameter,
   and the function will return True.

   Note that this works only because Idris is a pure functional
   language, meaning that a function can only use the values passed as
   parameters in its evaluation of the returned value.  Side effects or
   global variables are not available in a pure functional language.

   A function in Idris can only take one parameter, but it is possible
   to return a function, which permits to simulate a multi-parameter
   function (this is known as currying):

      \x => \y => True : Int -> (String -> Bool)

Petit-Huguenin             Expires 11 May 2022                [Page 118]
Internet-Draft           Computerate Specifying            November 2021

   Function types associate to the right, so the parenthesis in the
   example above is not really necessary.

   Functions in Idris can also take a function as parameter, which will
   permit to encode the classical question:

   "Socrates is a human, all humans are mortals, is Socrates a mortal?"

   We can encode this in the Idris type system:

      data Human : Type

      data Mortal : Type

      isSocratesMortal : Human -> (Human -> Mortal) -> Mortal

   Notice that here the parenthesis are mandatory.  The question can be
   read like this:

   "Assuming Socrates is a Human, and assuming that all Humans are
   Mortals, then is Socrates a Mortal?"

   The evidence is easy to find:

      isSocratesMortal : Human -> (Human -> Mortal) -> Mortal
      isSocratesMortal = \h => \f => f h

   One important point is that we are not trying to say that Socrates is
   a Human (maybe he was an alien).  Similarly we are not trying to say
   that there is an absolute rule that all humans are mortals (in fact
   there is evidence that, at the time of writing, the human author of
   this document was immortal).

   What we are saying is that assuming that we have evidence of a human
   (Socrates in that case) and assuming that we have evidence that all
   humans are mortals, then the only conclusion is that, Yes, Socrates
   is mortal, and the evidence for this is the program "\h => \f => f
   h".

   Note that in a function definition, the parameters can be moved to
   the left hand side (LHS) of the equal sign, like this:

      isSocratesMortal : Human -> (Human -> Mortal) -> Mortal
      isSocratesMortal h f = f h

Petit-Huguenin             Expires 11 May 2022                [Page 119]
Internet-Draft           Computerate Specifying            November 2021

E.1.3.  Polymorphism

   In some cases, questions can be made more general and still have a
   unique answer.  This is the case for the question explored in the
   previous section, where the question can be generalized to something
   called syllogism (also known as _Modus Ponens_).

   Polymorphism permits to substitute a type with a value that
   represents any type.  Thus finding an evidence shows that the answer
   is Yes for a whole family of related questions.

   Here we express that new generic question (the answer is the same) as
   this:

      syllogism : p -> (p -> q) -> q
      syllogism x f = f x

   An identifier that starts with a lowercase character in an Idris type
   stands for all possible types.

   Here we have evidence that a question with this particular shape can
   always be answered with Yes.

E.1.4.  Empty Type as No

   We saw previously that any value of a type is evidence of the Yes
   answer to the question encoded in that type.  So the absence of a
   value for a type is evidence that the answer is No.

   We have a problem here, as the evidence of No is that we cannot
   provide an evidence.  But, from our local point of view, there is no
   difference between the fact that there is no evidence, and the fact
   that we did not searched hard enough for the evidence.

   We can work around this by using a property of implication, which is
   that only a type with a No answer can imply a type with a No answer.
   So if we can implement a function (the Yes answer to the implication)
   between a type and an empty type (i.e., a type with a No answer),
   then we know that the former type is empty and that the answer it
   represents is also No.

   Idris provides an empty type for that: Void (not to be confused with
   the Java type Void, which is not an empty type).

      noEvidence: Int -> Void
      noEvidence x = ?aa

Petit-Huguenin             Expires 11 May 2022                [Page 120]
Internet-Draft           Computerate Specifying            November 2021

   Here we cannot complete the program because we cannot produce a value
   of type Void, and that's because Int has Yes as answer.

   In Idris names that starts with a question mark are called holes and
   stand for a part of the program that we cannot or did not yet
   complete.

      data Empty : Type where

      emptyIsNo : Empty -> Void
      emptyIsNo x impossible

   Here we can write a program that shows that that "Empty" is
   equivalent to "Void", this program acting as evidence that there is
   no evidence for "Empty", and so that the answer is No.

   Programmers will again be intrigued that a program that typechecks
   cannot be executed or tested.

   The possibility of defining a type like Void that does not have any
   values by definition is one of the reason we need a different type
   system that used in most programming languages (most programming
   languages permits the use of "null" as value for any type).

   We also touched on the fact that our programming language must be
   less powerful than usual, and it is also related to the answer No.

   An implication to a type that contains at least one value is a
   function that returns that value.  But there is two cases where that
   function could not return that value, and thus acts as if the
   returned type is empty, and thus represents No instead of Yes.

   The first case is if the function crashes because it does not know
   how to handle the value passed as parameter.  A simple example
   example would be a function that divide 1 by the parameter - if the
   parameter is zero then the function will crashes and for the purpose
   of our interpretation is equivalent to an evidence of No because no
   value will be returned.  To prevent that problem our programming
   language should be covering all inputs values, i.e. not typecheck if
   there is cases not covered.

   The second case is when, for some reason, the code get stuck inside
   the function e.g., because of an infinite loop.  That would again be
   equivalent to an evidence of No.

   Idris prevents these two cases by using the "total" keyword, which
   basically turns Idris into a non-Turing Complete language.

Petit-Huguenin             Expires 11 May 2022                [Page 121]
Internet-Draft           Computerate Specifying            November 2021

   Note that there is no way to possibility to write code that will
   detect for any possible code if it will loop or not.  That's why
   Idris may reject some code that will not loop, but it will never
   accept code that will loop.

E.1.5.  Sloppy Questions

   Because there is not much difference between a No answer without
   evidence and not finding an answer, it's often useful to check and
   recheck that the question really expresses what we intended.

   In the previous section we showed that syllogisms always have an
   answer of Yes. There is a series of fallacies [Bennett15] that are
   closely related to syllogisms, and here's one of them:

      syllogism : p -> (q -> p) -> q

   That can be read as "Assuming Socrates is a Human, and assuming that
   all Mortal are Humans, then is Socrates a Mortal?"  It may seems
   obvious that we cannot answer that question, so we may be able to get
   a No answer by rewriting the question that way:

      syllogistic_fallacy : (p -> (q -> p) -> q) -> Void

   But in spite of our efforts, we cannot provide an evidence of that,
   which means that it is time to look closer at our question.

   The issue is that for this to be a fallacy, we need to assume that
   there is no evidence that all Humans are Mortals, which the previous
   question does not say.  With this modified question, we can now
   produce a evidence that it is indeed a fallacy:

      syllogistic_fallacy : ((p -> q) -> Void) ->
                              (p -> (q -> p) -> q) -> Void
      syllogistic_fallacy f g = f (\x => g x (\y => x))

E.1.6.  Product Type

   The Product type permits to combine two or more questions such as the
   question represented by this type will have an answer of Yes only if
   all the questions also have an answer of Yes.

   The simplest Product type in Idris is the tuple, which is represented
   as a list of types separated by commas and enclosed in parentheses:

      product : (String, Int, Char) -> Bool
      product : (x, y, z) -> True

Petit-Huguenin             Expires 11 May 2022                [Page 122]
Internet-Draft           Computerate Specifying            November 2021

   The evidence has the same form as the type.

   We can also provide evidence that the form above is equivalent to its
   curried form in general, and vice-versa:

      curry : ((a, b) -> c) -> (a -> b -> c)
      curry f x y = f (x, y)

      uncurry : (a -> b -> c) -> ((a, b) -> c)
      uncurry f x = f (fst x) (snd x)

E.1.7.  Sum Type

   The Sum type is a way to combine two or more questions such as the
   question represented by the Sum type will have an answer of Yes if at
   least one of the questions have an answer of Yes.

   The simplest Sum type for two questions in Idris is "Either a b".

      sum : Either String Void -> Bool
      sum x = True

   We can combine Sum and Product types to reorganize a question and
   show evidence that the answer is general.

      dist : (a, Either b c) -> (Either a b, Either a c)
      dist x = (Left (fst x), Left (fst x))

   Sum and Product combined with negation gives us more general answers:

      dm1 : (Either (a -> Void) (b -> Void)) -> ((a, b) -> Void)
      dm1 (Left x) y = x (fst y)
      dm1 (Right x) y = x (snd y)

      dm2 : (a -> Void, b -> Void) -> ((Either a b) -> Void)
      dm2 x (Left y) = fst x y
      dm2 x (Right y) = snd x y

      dm3 : ((Either a b) -> Void) -> (a -> Void, b -> Void)
      dm3 f = (\x => f (Left x), \x => f (Right x))

E.1.8.  Inductive Type

   TBD.

Petit-Huguenin             Expires 11 May 2022                [Page 123]
Internet-Draft           Computerate Specifying            November 2021

E.1.9.  Pi Type

   TBD.

E.1.10.  Sigma Type

   TBD.

E.1.11.  Equality Type

   TBD.

E.1.12.  Decidable Type

   TBD.

E.2.  How to Find Evidence

   TBD

Appendix F.  A Distributed Package Manager for Computerate
             Specifications

   |  Any organization that designs a system (defined broadly) will
   |  produce a design whose structure is a copy of the organization's
   |  communication structure.
   |  
   |  -- Melvin E. Conway

   One long-term goal of this document is to establish a library of
   exported specifications for network protocols, much like the Lean
   Mathematical Library [Community20].  But unlike mathlib, which is
   built as a single git repository hosted in GitHub, the computerate
   library is built to mirror the intended distributed design of the
   Internet.

   Computerate specifications are composed of code, so using a git
   repository to store that code and its evolution seems the right
   choice.  But instead of using a single repository, each computerate
   specification is stored into a separate git repository.  This permits
   to let each contributor choose how they will provide a public access
   to each git repository, anywhere in the spectrum from hosting
   providers (GitHub, GitLab, BitBucket...) to distributed services
   (IPFS, Radicle...), and including self-hosted servers (Gitolite,
   GitLab...).

Petit-Huguenin             Expires 11 May 2022                [Page 124]
Internet-Draft           Computerate Specifying            November 2021

   Be able to export specifications would be useless without the ability
   to import other specifications.  This requires the use of
   dependencies, such as the graph of dependencies between
   specifications will grow until it mirrors the graph of normative
   references between standards documents.

   Here also we eschew the usual solution to that issue, which is using
   a centralized artifact repository (Maven, Gem, Apt, ...), in favor of
   a distributed solution, both for the storage of the binary artifacts
   and for the resources needed to build and verify them.

   The solutions developed to fulfill these requirements ensure better
   availability, scalability and freedom than if it was designed as a
   single GitHub repository.

F.1.  Distributed Source Repositories

F.1.1.  The "gits" Protocol

   |  It's not that I have something to hide.  I have nothing I want you
   |  to see.
   |  
   |  -- Amanda Seyfried's character in Anon (2018)

   Among all transport protocols that can be used to fetch commits, the
   Git protocol is the fastest as it runs directly over a TCP
   connection.  It is directly implemented by the "git daemon" command.
   For this reason it is the best choice to make public a git repository
   in read-only mode.

   But, although everyone can fetch commits from such a repository, the
   transfer of the commits themselves is not encrypted.  The "gits"
   transport protocol solves that issue by replacing the TCP connection
   by a TLS connection.  On the client side, the remote helper "git-
   remote-gits" is provided as part of the tooling.  On the server side,
   the simplest solution is to use "stunnel" together with "git daemon".

F.1.2.  The "mgit" and "mgits" Protocols

   The mgit protocol provides an indirection to a list of git URLs, all
   pointing to identical mirrors of the same repository.  An mgit URL
   provides scalability, reliability, and the ability of adding and
   removing git mirrors without having to changing the URL itself.  Note
   that mirrors can use any kind of git URL (http, ssh, git, etc...),
   including gits URLs.

Petit-Huguenin             Expires 11 May 2022                [Page 125]
Internet-Draft           Computerate Specifying            November 2021

   An mgit URL has the format "mgit://<random>", where <random> is a 40
   hexadecimal characters string.  Such URL is very stable, and can be
   published in a document for the purpose of retrieving the git
   repository holding the computerate specification that was used to
   generate that document.

   Internally that string is used as the index to store the list of URLs
   pointing to the git mirrors in a RELOAD [RFC6940] P2P Overlay.  Note
   that storing such list of URLs in the overlay requires credentials.

   The remote helper "git-remote-mgit" is provided as part of the
   tooling.  When used to fetch commit, it first contacts the overlay to
   retrieve the list of mirrors, then choose one randomly and fetch the
   commits from there.  If the mirror does not respond, then another
   mirror is randomly selected from the list, until all mirrors have be
   tried.

   The "git-remote-mgits" remote helper behaves similarly, but always
   excludes URLs that do not encrypt the transport.

F.1.3.  Git Submodules as Dependencies

   A specification is a set of files that, together, are used as input
   to a process that generate a document.  The subset of Idris files in
   that set forms an Idris Package.  One and only one Idris package is
   stored per Git repository.

   For specifications defined by this document, dependencies to other
   Idris Packages are defined by adding the Git repositories storing
   these repositories as Git submodules.  This permits to distribute the
   graph of dependencies between each repository, without requiring a
   separate way of storing that information.  The downside of doing that
   is that a new commit needs to be created to change the URL of a
   submodule.

   In the traditional use of a submodule, 1) the URL to the Git
   repository together with 2) the commit that needs to be checked out
   in that repository, are the two pieces of information that are
   stored.

   Instead of using a traditional "https" URL for the submodule, we use
   an "mgits" URL which brings a better reliability and availability,
   together with the ability to add or remove mirrors without having to
   create a new commit.

Petit-Huguenin             Expires 11 May 2022                [Page 126]
Internet-Draft           Computerate Specifying            November 2021

F.2.  Distributed Artifact Manager

F.2.1.  Reproducible Build

   We are storing binary artifacts in a distributed cache that is
   colocated with each git repository.

   Because the size of a cache cannot be unbounded, we need to be able
   to rebuild any artifact at any time from any commit in a git
   repository, and ensure that the artifact built for a commit stays the
   same regardless of when and where it is built.

   We solve this issue by making all specification builds reproducible.
   In that context, reproducible means that building binary artifacts
   now or in 10 years will result in two sets of artifacts that are bit-
   exact identical.

   That property permits to identifies each build by the commit-id of
   the commit of the source that was used to build it.

   A clear consequence of this is that the Idris compiler and its
   runtime (chezscheme) should be available as source on the same
   commit, and should be part of the build.  The simplest way to
   guarantee that is that these tools are also available as git
   submodules.

F.2.2.  Distributed Cache

   We use the git-lfs extension storage, when available, to store the
   binary artifacts.

   When a build ends successfully, all the artifacts created in the
   source tree, which are easily recognizable because they are the files
   that are not already managed by git (ignoring the content of the
   .gitignore file), are packed in a file (zip, tar...) and uploaded
   into the git-lfs server, using the SHA256 hash of the commit-id of
   the source tree as OID.

   The first step of a build is to try to retrieve the artifacts from
   the git-lfs storage, using the current commit-id.  If that succeeds,
   the zip file retrieved is expanded, such as the artifacts are
   installed in the source tree exactly as they are after a successful
   build.  If that fails then the build proceeds as usual.

Petit-Huguenin             Expires 11 May 2022                [Page 127]
Internet-Draft           Computerate Specifying            November 2021

F.3.  Recursive Build

   Building a specification generally starts with building dependencies,
   as defined by submodules.  Because submodules may themselves have
   submodules, the build becomes recursive.

   Building a specification recursively from source would take a long
   time, so we take advantage of the distributed caches to download the
   binary artifacts instead when they are available.

   To do so we need first to index the git repositories specifications
   by their commit-id.

F.3.1.  Indexing Commits

   We are using of one of the properties of a commit-id, which is a hash
   of the content of a commit, including the date and time, and the
   commit-id of the previous commit.  That property is that a commit-id
   is a statistically globally unique identifier for the content of that
   commit, meaning that if the same commit-id lives in different
   repositories, they will still points to the exact same content.  That
   means that by building an index for all the commit-ids of interest,
   we can associate each of them with the list of git repositories that
   contain it.

   We are doing this indexation again in a distributed way, using the
   same RELOAD P2P overlay used in Appendix F.1.2.

   Each time commits for a computerate specification are pushed in a git
   repository that have a public access, our "mgits" git remote helper
   is used as a wrapper for the actual URI:

   mgits::gitolite3@example.org:computerate-specifying.git

   The "computerate" wrapper stores each commit pushed in the P2P
   overlay as index, with the gitolite3@example.org:computerate-
   specifying.git URL in the associated RELOAD Array.  If the Array for
   a specific commit already exist, the URL is added to that Array if
   the URL is not already there.

F.3.2.  Building a Submodule

   Before building a submodule, the build process queries the P2P
   Overlay using the commit-id of the submodule as index.  That returns
   a list of git URLs, each pointing to a git repositories that hold
   that particular commit.  The build process chooses one of these, and
   tries to download the binary artifacts, as explained in
   Appendix F.2.2.  If the artifacts are not available, the sources

Petit-Huguenin             Expires 11 May 2022                [Page 128]
Internet-Draft           Computerate Specifying            November 2021

   files are retrieved from one of the git repositories, and the build
   is applied to each submodule before building that submodule.

F.3.3.  Pinned Down Builds

   The whole process would require to start the typechecking of any
   specification that is not yet cached by rebuilding the Idris compiler
   and the chezscheme runtime.  This is why it is permitted to pin down
   some builds in the distributed cache, i.e. they are never candidate
   for removal, which would make them always available.

Appendix G.  Git Layout for Computerate Specifications

   In most cases computerate specifications cannot be distributed
   because the IETF Trust declined to grant a license for that purpose
   (see item 5 in [Minutes]).  Thus any distribution of a computerate
   specification would be a copyright infringement.

   To work around that limitation, computerate specifications are not
   distributed as an annotated RFC or Internet-Draft, but as a set of
   files colocated with the RFC/I-D, using transclusions to merge the
   files only when a specification is checked out by Git.

   A new git command "git computerate" is distributed with the tooling,
   and permits to manage a distributable repository containing a
   specification.

   The content of such Git repository can be seen as conversions between
   3 states:

   *  The reference file contains an RFC or Internet-Draft, exactly as
      stored in the RFC Editor or IETF Secretariat databases.  For the
      time being, only the text version of these documents is used, as
      the xml2rfc v3 version for I-Ds is not canonical, or even existing
      in the first place.

   *  The computerate specification, which is composed of at least one
      file with the .lipkg extension, and a set of optional .adoc and
      .lidr files, all of them included from the .lipkg file.  These
      files only exist on a checked out repository and are never pushed
      or pulled from or to a remote.

   *  The transcluded specification, which is composed of the exact same
      set of files than above, but with the copyrighted text replaced by
      transclusions.  These files are the one that are pulled and pushed
      to and from a remote.

   There is 4 different conversions taking place between these states:

Petit-Huguenin             Expires 11 May 2022                [Page 129]
Internet-Draft           Computerate Specifying            November 2021

   From reference file to computerate specification:  The "convert"
      subcommand takes an RFC or I-D in text format, stores it in the
      current git repository under the name ".reference.txt" and
      generates an initial computerate specification named "Main.lipkg".
      That same program can optionally take as parameter the set of
      existing files for the computerate specification and calculate a
      patchset to be applied when a new version of an Internet-Draft is
      submitted, when the RFC is published, or when an erratum for that
      RFC is verified.

   From computerate specification to reference file:  The "computerate"
      program takes the computerate specification files and convert them
      into a reference file.  See Appendix A.3 for the usage.

   From computerate specification to transcluded specification:  the
      "clean" program takes one of the computerate specification files,
      the reference file, and replaces this computerate specification
      file by substituting all the text that also exist in the reference
      file by transclusions.

   From transcluded specification to computerate specification:  the "sm
      udge" program takes a transcluded specification file, the
      reference file and replace this transcluded specification file by
      substituting the transclusions with the text in the reference
      file.

   In addition, a diff program can compare two text versions of the same
   RFC or Internet-Drafts, but excluding the differences in formatting.
   When an RFC or I-D is converted to a computerate specification, which
   itself is converted back to a text document, a diff of the original
   text and of the generated text should result in no difference.
   Similarly a computerate specification converted as text and then
   converted back into a computerate specification should be equal to
   the original computerate specification.  This goes beyond the
   capability of the "rfcdiff" program, e.g., by ignoring how sentences
   are wrapped-up in a paragraph.

   Similarly the clean and smudge programs should be able to convert
   back and forth between the computerate specification and the
   transcluded specification without loss of information.  These two
   programs are executed automatically by git when a specification file
   is either checked-out or staged.

   Note that it is crucial to understand that the act of merging
   reference file and transcluded file must only be done on a local
   computer, so to not infringe on the IETF Trust copyright.  This makes
   Git web interfaces like GitHub less useful than for other types of
   files, as such web interface can only display the transcluded file.

Petit-Huguenin             Expires 11 May 2022                [Page 130]
Internet-Draft           Computerate Specifying            November 2021

   The package management system for computerate specifications
   described in Appendix F does not rely on the availability of a web
   interface for the git repositories.

   It is recommended to populate a "copyright" file [Copyright],
   colocated with each computerate specification, that contains the
   exact license used for each file in the repository,

Acknowledgements

   Thanks to Jim Kleck, Eric Petit-Huguenin, Nicolas Gironi, Stephen
   McQuistin, Greg Skinner, and Raluca Toth 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.

Contributors

   Stéphane Bryant

   Email: stephane.ml.bryant@gmail.com

Changelog

   draft-petithuguenin-computerate-specifying-15:

   *  Document:
      -  Rework the RFC5234 module in sections 8.2.1 and B.2.1.
      -  Rewrite of section 7 "Exporting Specifications".
      -  Rename appendix B to "API Documentation".
      -  Rework the Dimension module in sections 8.1.4 and B.1.4.

   *  Tooling:
      -  Update xml2rfc to 3.11.1.
      -  Add "impl" parameter to code macros to pass the name of a
         Pretty or Asciidoc implementation.
      -  Added pdfattach/pdfdetach tools.
      -  Update metanorma-ietf to 2.5.0.1.
      -  Update metanorma to 1.4.0.
      -  The Dimension module is distributed with the tooling.
      -  The code:[] macro now requires a value of a type that
         implements the ComputerateSpecifying.Metanorma.Ietf.Asciidoc
         interface.
      -  Add the id2xml tool.

Petit-Huguenin             Expires 11 May 2022                [Page 131]
Internet-Draft           Computerate Specifying            November 2021

   *  Template:
      -  Converted the examples in Literate to use the Asciidoc
         interface.
      -  Add example of ABNF.

   *  Library:
      -  Add user-defined dimensions to the Dimension module.
      -  Add type to prove that a string is valid for a specific ABNF in
         package rfc5234.

   draft-petithuguenin-computerate-specifying-14:

   *  Document:
      -  Reorganized the CLI appendix, as most of text related to the
         AsciiDoc content of a specification moved to the templates.
      -  Indent examples instead of using <CODE BEGINS>/<CODE END>.
      -  Update of the Abnf tutorial (section 6.2.1.4).
      -  Update of the Abnf reference (section 8.2.2).
      -  Update of the Abnf IdrisDoc (section B.2).

   *  Tooling:
      -  Update metanorma to 1.2.12.
      -  Distribution of templates in the docker image.
      -  An include with a computerate I-D as target now insert a
         bibliographic item for that I-D.
      -  Distribution of a Zotero exporter for AsciiBib in the docker
         image.
      -  Code fragments are now inserted using the new "code" macros.
      -  mnconvert now generates one line of text per sentence.
      -  Replaced rfc2mn by mnconvert.
      -  Update metanorma-ietf to 2.4.4.
      -  The rfc5234 package is now distributed in the Docker image.

   draft-petithuguenin-computerate-specifying-13:

   *  Document:
      -  Update of the TPN simulation tutorial (section 6.1.4.3).
      -  Update of the TPN reference to align with the Tpn module
         (section B.1.7.1).
      -  Reorganization of section D, adding text for Substitution
         Transitions and Fusion Places.
      -  More dogfooding by having the examples in appendix D
         typechecked when the document is built.

   *  Tooling:
      -  Update xml2rfc to 3.10.0.
      -  Update metanorma-ietf to 2.4.2.
      -  Update metanorma to 1.3.11.

Petit-Huguenin             Expires 11 May 2022                [Page 132]
Internet-Draft           Computerate Specifying            November 2021

      -  Update Idris2 to 0.5.1.
      -  The Tpn module is now distributed in the Docker image.

   *  Library:
      -  Because the domain of the input inscription is now a list, the
         function has to be run on the permutation-subsets of the
         content instead of on the content itself, which is a
         significant difference.  So to permit to use constraint
         propagation with backtracking the unification is now specified
         separately from the transition inscription.
      -  Input arc inscriptions now takes a non-empty list as input
         parameter, which in in line with CPN behavior.  The "one"
         function can be used in replacement for "pure".
      -  Free variables are now generated instead of having to manually
         convert them.  The type of a free variable must implement
         "Enum".
      -  "Marking" implements "Show".
      -  Implemented "initialMarking".
      -  Naming stuff is hard enough, so uniqueness of names in a TPN is
         no longer mandatory.
      -  A TPN module is now indexed over the list of the port types it
         exports.

   draft-petithuguenin-computerate-specifying-12:

   *  Document:
      -  TPN documentation update:
         o  Now supports Timed TPN.
         o  A Monadic DSL replaces the direct access to constructors,
            making the syntax more compact and readable.
         o  The text in sections 6.1.4.1, the new 6.1.4.2, 8.1.7.1,
            B.1.6, and appendix D is updated to reflect these
            modifications.
      -  Update list of meta-languages.

   *  Tooling:
      -  Modify xml2rfc to add the appendices in the info file.
      -  Update metanorma-ietf to 2.4.1.
      -  Update metanorma to 1.3.10.

   draft-petithuguenin-computerate-specifying-11:

   *  Document:
      -  Add a section for each formal language defined in an RFC.
      -  More explanations on escaping, literate ipkg and self-
         inclusion.

   *  Tooling:

Petit-Huguenin             Expires 11 May 2022                [Page 133]
Internet-Draft           Computerate Specifying            November 2021

      -  Remove temporary files before processing.
      -  Update idnits to 2.17.00.
      -  Backticks inside code fragment are correctly processed.
      -  Update metanorma to 1.3.9.1.
      -  Files with .lipkg extension are also processed as literate
         files.  This permits to have a top adoc file also containing an
         Idris package definition.

   draft-petithuguenin-computerate-specifying-10:

   *  Document:
      -  Renamed and reworked the AsciiDoc library as Metanorma.Ietf.
      -  New ComputerateSpecifying module for common types.
      -  Align I-D references with the RFC Editor Style Guide.

   *  Tooling:
      -  A subset of the computerate specifying standard library is now
         distributed in the Docker image.  Currently the Metanorma.Ietf
         module is the only module distributed.
      -  Update asciidoctor to 2.0.16.
      -  Base image is now Debian bullseye-slim.
      -  Remove transclusion processor.
      -  Insert SeriesInfo in correct order (BCP|STD|FYI, RFC|Internet-
         Draft, DOI).
      -  Process correctly literate error.
      -  Processing of Idris files is done only once.
      -  Remove useless metanorma patches.
      -  Update Idris2 to 0.4.0.
      -  Update xml2rfc to 3.9.1.
      -  Update metanorma to 1.3.9.
      -  Update metanorma-ietf to 2.4.0

   draft-petithuguenin-computerate-specifying-09:

   *  Document:
      -  New design for codepoint registries.
      -  Transclusions are now implicit.
      -  New appendix G explains how git is used to legally distribute
         retrofitted specifications after the IETF Trust rejected a
         request for a license.
      -  Improved bibliography.

   *  Tooling:
      -  The include directive for lidr file now supports range, tag and
         tags attributes.  This permits to copy the actual code into a
         block.
      -  The "--dg asciidoc" option for idris2 generates the
         documentation in AsciiDoc instead of HTML.

Petit-Huguenin             Expires 11 May 2022                [Page 134]
Internet-Draft           Computerate Specifying            November 2021

      -  Update asciidoctor to 2.0.15.
      -  Update metanorma to 1.3.3.
      -  Update metanorma-ietf to 2.3.2.

   draft-petithuguenin-computerate-specifying-08:

   *  Document:
      -  Most of the bibliography is now generated from a Zotero
         collection, resulting in a better and easier to maintain
         bibliography.
      -  Nits.
      -  Explanations on how to convert a CPN transition into a TPN
         transition.
      -  New appendix F describing the distributed system for the
         computerate specifications library.
      -  Improvements in the TPN Tutorial, Reference and IdrisDoc.

   *  Tooling:
      -  Add rfc2mn tool to convert an xml2rfc file into an AsciiDoc
         document.
      -  Update asciidoctor to 2.0.14
      -  Update metanorma to 1.3.0.
      -  Update metanorma-ietf to 2.3.0.
      -  Update xml2rfc to 3.7.0.
      -  Multiline problem in postal address is fixed in metanorma.
      -  Default figure wrapping problem is fixed in metanorma.

   draft-petithuguenin-computerate-specifying-07:

   *  Document:
      -  New text for Sum type, Product type.
      -  Text explaining how to convert a CPN Place into a TPN Place.
      -  Typed Petri Nets are now hierarchical.

   *  Tooling:
      -  Idris can now run shebang files.
      -  Update xml2rfc to 3.6.0.
      -  Update metanorma to 1.2.7.
      -  Update metanorma-ietf to 2.2.9.

   draft-petithuguenin-computerate-specifying-06:

   *  Document:
      -  Rename abstract type as semantic type, and coloured petri nets
         as colored petri net.
      -  Remove figure wrapper from all source code, and added markers
         when missing.

Petit-Huguenin             Expires 11 May 2022                [Page 135]
Internet-Draft           Computerate Specifying            November 2021

      -  Rewrite and extension of sections 6.1.4 and 6.1.5.2 to show how
         to generate a Message Sequence Chart from a Petri Net.
      -  New step by step explanation on how to manually convert a CPN
         into a TPN as appendix D.
      -  New tutorial on Evidence-Based Answers as appendix E.

   *  Tooling:
      -  Generated sourcecode elements are no longer wrapped by default
         in a figure element.

   *  Library:
      -  Update of the "Tpn" module.

   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.

Petit-Huguenin             Expires 11 May 2022                [Page 136]
Internet-Draft           Computerate Specifying            November 2021

      -  Generate IdrisDoc of standard library packages and modules as a
         new appendix.
      -  Update errata stats.
      -  More compact changelog.
      -  Many modifications following Stephane's reviews.

   *  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.

Petit-Huguenin             Expires 11 May 2022                [Page 137]
Internet-Draft           Computerate Specifying            November 2021

      -  Convert "Verified Code" section into a top level section, and
         expand it.
      -  Add "Implementation-Oriented Standards" section.

   *  Tooling:
      -  Many bug fixes in metanorma-ietf.
      -  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.

Petit-Huguenin             Expires 11 May 2022                [Page 138]
Internet-Draft           Computerate Specifying            November 2021

      -  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.
      -  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 11 May 2022                [Page 139]