Network Working Group M. Petit-Huguenin Internet-Draft Impedance Mismatch LLC Intended status: Experimental 28 March 2021 Expires: 29 September 2021 The Computerate Specifying Paradigm draft-petithuguenin-computerate-specifying-07 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 29 September 2021. Copyright Notice Copyright (c) 2021 IETF Trust and the persons identified as the document authors. All rights reserved. This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/ license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Code Components extracted from this document must include Simplified BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Simplified BSD License. Petit-Huguenin Expires 29 September 2021 [Page 1] Internet-Draft Computerate Specifying March 2021 Table of Contents 1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 5 2. Overview . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3. Terminology . . . . . . . . . . . . . . . . . . . . . . . . . 6 4. Private Specifications . . . . . . . . . . . . . . . . . . . 7 4.1. Private Specifications for New Documents . . . . . . . . 10 4.2. Private Specifications for Existing Documents . . . . . . 11 5. Self-Contained Specifications . . . . . . . . . . . . . . . . 12 5.1. PDU Descriptions . . . . . . . . . . . . . . . . . . . . 12 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 . . . . . . . . . . . . . 19 5.3.2. Data Format Conversion . . . . . . . . . . . . . . . 22 5.3.3. Postel's Law . . . . . . . . . . . . . . . . . . . . 22 5.3.4. Implementability . . . . . . . . . . . . . . . . . . 25 5.3.5. Termination . . . . . . . . . . . . . . . . . . . . . 26 5.3.6. Liveness . . . . . . . . . . . . . . . . . . . . . . 26 6. Importing Specifications . . . . . . . . . . . . . . . . . . 26 6.1. Common Modules . . . . . . . . . . . . . . . . . . . . . 28 6.1.1. Generating AsciiDoc . . . . . . . . . . . . . . . . . 28 6.1.2. Common Data Types . . . . . . . . . . . . . . . . . . 29 6.1.3. Calculations . . . . . . . . . . . . . . . . . . . . 33 6.1.4. Typed Petri Nets . . . . . . . . . . . . . . . . . . 34 6.1.4.1. Designing a Typed Petri Net . . . . . . . . . . . 35 6.1.4.2. Using a Typed Petri Net . . . . . . . . . . . . . 38 6.1.5. Representations . . . . . . . . . . . . . . . . . . . 39 6.1.5.1. Bit Diagrams . . . . . . . . . . . . . . . . . . 39 6.1.5.2. Message Sequence Charts . . . . . . . . . . . . . 40 6.2. Packages for Meta-Languages . . . . . . . . . . . . . . . 42 6.2.1. Augmented BNF (ABNF) . . . . . . . . . . . . . . . . 45 6.2.2. Augmented Packet Header Diagrams (APHD) . . . . . . . 46 6.2.3. Cosmogol . . . . . . . . . . . . . . . . . . . . . . 48 6.3. Packages for Protocols . . . . . . . . . . . . . . . . . 48 6.3.1. Type Transformations . . . . . . . . . . . . . . . . 49 6.3.2. Extended Registries . . . . . . . . . . . . . . . . . 52 7. Exporting Specifications . . . . . . . . . . . . . . . . . . 54 7.1. Standard Library . . . . . . . . . . . . . . . . . . . . 54 7.2. Transclusions . . . . . . . . . . . . . . . . . . . . . . 55 7.3. Exporting Types and Functions . . . . . . . . . . . . . . 56 8. Standard Library . . . . . . . . . . . . . . . . . . . . . . 56 8.1. Internal Modules . . . . . . . . . . . . . . . . . . . . 56 8.1.1. AsciiDoc . . . . . . . . . . . . . . . . . . . . . . 56 8.1.2. BitVector . . . . . . . . . . . . . . . . . . . . . . 57 8.1.3. Unsigned . . . . . . . . . . . . . . . . . . . . . . 57 Petit-Huguenin Expires 29 September 2021 [Page 2] Internet-Draft Computerate Specifying March 2021 8.1.4. Dimension . . . . . . . . . . . . . . . . . . . . . . 57 8.1.5. BitDiagram . . . . . . . . . . . . . . . . . . . . . 59 8.1.6. Transform . . . . . . . . . . . . . . . . . . . . . . 59 8.1.7. Tpn . . . . . . . . . . . . . . . . . . . . . . . . . 60 8.2. Meta-Language Packages . . . . . . . . . . . . . . . . . 61 8.2.1. Augmented Packet Header Diagrams (APHD) . . . . . . . 61 8.2.2. RFC 5234 (ABNF) . . . . . . . . . . . . . . . . . . . 61 8.3. Protocol Packages . . . . . . . . . . . . . . . . . . . . 61 8.3.1. RFC 791 (Internet Protocol) . . . . . . . . . . . . . 62 9. Informative References . . . . . . . . . . . . . . . . . . . 62 Appendix A. Command Line Tools . . . . . . . . . . . . . . . . . 65 A.1. Installation . . . . . . . . . . . . . . . . . . . . . . 66 A.1.1. Download the Docker Image . . . . . . . . . . . . . . 66 A.2. The "computerate" Command . . . . . . . . . . . . . . . . 66 A.2.1. Literate Files . . . . . . . . . . . . . . . . . . . 67 A.2.2. Transclusions . . . . . . . . . . . . . . . . . . . . 67 A.2.3. IdrisDoc Generation . . . . . . . . . . . . . . . . . 68 A.2.4. Outputs . . . . . . . . . . . . . . . . . . . . . . . 68 A.2.5. Extended Registry . . . . . . . . . . . . . . . . . . 68 A.2.6. Bibliography . . . . . . . . . . . . . . . . . . . . 68 A.2.6.1. Internet-Draft . . . . . . . . . . . . . . . . . 69 A.2.6.2. RFC . . . . . . . . . . . . . . . . . . . . . . . 70 A.2.6.3. Email . . . . . . . . . . . . . . . . . . . . . . 71 A.2.6.4. IANA . . . . . . . . . . . . . . . . . . . . . . 71 A.2.6.5. Web-Based Public Code Repositories . . . . . . . 72 A.3. Idris REPL . . . . . . . . . . . . . . . . . . . . . . . 72 A.4. Other Commands . . . . . . . . . . . . . . . . . . . . . 73 A.5. Source Repositories . . . . . . . . . . . . . . . . . . . 73 A.6. Modified Tools . . . . . . . . . . . . . . . . . . . . . 73 A.6.1. Idris2 . . . . . . . . . . . . . . . . . . . . . . . 73 A.6.2. asciidoctor . . . . . . . . . . . . . . . . . . . . . 74 A.6.3. metanorma . . . . . . . . . . . . . . . . . . . . . . 74 A.6.4. metanorma-ietf . . . . . . . . . . . . . . . . . . . 74 A.6.5. idris2-vim . . . . . . . . . . . . . . . . . . . . . 74 A.7. Bugs and Workarounds . . . . . . . . . . . . . . . . . . 75 A.8. TODO List . . . . . . . . . . . . . . . . . . . . . . . . 75 Appendix B. Reference . . . . . . . . . . . . . . . . . . . . . 76 B.1. Package computerate-specifying . . . . . . . . . . . . . 76 B.1.1. Module ComputerateSpecifying.AsciiDoc . . . . . . . . 77 B.1.2. Module ComputerateSpecifying.BitDiagram . . . . . . . 78 B.1.3. Module ComputerateSpecifying.BitVector . . . . . . . 78 B.1.4. Module ComputerateSpecifying.Dimension . . . . . . . 80 B.1.5. Module ComputerateSpecifying.Tpn . . . . . . . . . . 82 B.1.6. Module ComputerateSpecifying.Transform . . . . . . . 85 B.1.7. Module ComputerateSpecifying.Unsigned . . . . . . . . 86 B.2. Package rfc5234 . . . . . . . . . . . . . . . . . . . . . 86 B.2.1. Module RFC5234.Core . . . . . . . . . . . . . . . . . 86 B.2.2. Module RFC5234.Main . . . . . . . . . . . . . . . . . 87 Petit-Huguenin Expires 29 September 2021 [Page 3] Internet-Draft Computerate Specifying March 2021 B.3. Package augmented-ascii-diagrams . . . . . . . . . . . . 88 B.3.1. Module AAD.Main . . . . . . . . . . . . . . . . . . . 88 B.4. Package rfc791 . . . . . . . . . . . . . . . . . . . . . 90 B.4.1. Module RFC791.Address . . . . . . . . . . . . . . . . 90 B.4.2. Module RFC791.IP . . . . . . . . . . . . . . . . . . 90 Appendix C. Errata Statistics . . . . . . . . . . . . . . . . . 92 Appendix D. Converting From a Colored Petri Net . . . . . . . . 93 D.1. Convert Color Sets . . . . . . . . . . . . . . . . . . . 94 D.1.1. Simple Color Sets . . . . . . . . . . . . . . . . . . 94 D.1.1.1. Unit Color Sets . . . . . . . . . . . . . . . . . 94 D.1.1.2. Boolean Color Sets . . . . . . . . . . . . . . . 94 D.1.1.3. Integer Color Sets . . . . . . . . . . . . . . . 95 D.1.1.4. Large Integer Color Sets . . . . . . . . . . . . 95 D.1.1.5. Real Color Sets . . . . . . . . . . . . . . . . . 96 D.1.1.6. String Color Sets . . . . . . . . . . . . . . . . 96 D.1.1.7. Enumerated Color Sets . . . . . . . . . . . . . . 97 D.1.1.8. Index Color Sets . . . . . . . . . . . . . . . . 97 D.1.2. Compound Color Sets . . . . . . . . . . . . . . . . . 97 D.1.2.1. Product Color Sets . . . . . . . . . . . . . . . 97 D.1.2.2. Record Color Sets . . . . . . . . . . . . . . . . 98 D.1.2.3. List Color Sets . . . . . . . . . . . . . . . . . 98 D.1.2.4. Union Color Sets . . . . . . . . . . . . . . . . 98 D.1.2.5. Subset Color Sets . . . . . . . . . . . . . . . . 99 D.1.2.6. Alias Color Sets . . . . . . . . . . . . . . . . 99 D.1.3. Timed Color Sets . . . . . . . . . . . . . . . . . . 99 D.2. Convert Places . . . . . . . . . . . . . . . . . . . . . 99 D.3. Convert Transitions . . . . . . . . . . . . . . . . . . . 100 D.3.1. Convert Input Arcs . . . . . . . . . . . . . . . . . 100 D.3.2. Convert Inhibitor Arcs . . . . . . . . . . . . . . . 100 D.3.3. Convert Reset Arcs . . . . . . . . . . . . . . . . . 100 D.3.4. Convert Output Arcs . . . . . . . . . . . . . . . . . 100 D.3.5. Convert Transitions with Time . . . . . . . . . . . . 100 D.3.6. Convert Transitions with Priorities . . . . . . . . . 100 Appendix E. Evidence-Based Answers . . . . . . . . . . . . . . . 101 E.1. Encoding Questions . . . . . . . . . . . . . . . . . . . 102 E.1.1. Any Value of a Type is Evidence of Yes . . . . . . . 103 E.1.2. Function Type As Implication . . . . . . . . . . . . 103 E.1.3. Polymorphism . . . . . . . . . . . . . . . . . . . . 105 E.1.4. Empty Type as No . . . . . . . . . . . . . . . . . . 106 E.1.5. Sloppy Questions . . . . . . . . . . . . . . . . . . 108 E.1.6. Product Type . . . . . . . . . . . . . . . . . . . . 108 E.1.7. Sum Type . . . . . . . . . . . . . . . . . . . . . . 109 E.1.8. Pi Type . . . . . . . . . . . . . . . . . . . . . . . 110 E.1.9. Sigma Type . . . . . . . . . . . . . . . . . . . . . 110 E.1.10. Inductive Type . . . . . . . . . . . . . . . . . . . 110 E.1.11. Equality Type . . . . . . . . . . . . . . . . . . . . 110 E.1.12. Decidable Type . . . . . . . . . . . . . . . . . . . 110 E.2. How to Find Evidence . . . . . . . . . . . . . . . . . . 110 Petit-Huguenin Expires 29 September 2021 [Page 4] Internet-Draft Computerate Specifying March 2021 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . 110 Contributors . . . . . . . . . . . . . . . . . . . . . . . . . . 111 Changelog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 Author's Address . . . . . . . . . . . . . . . . . . . . . . . . 114 1. Introduction If, as the unofficial IETF motto states, we believe that "running code" is an important part of the feedback provided to the standardization process, then as per the Curry-Howard equivalence [Curry-Howard] (that states that code and mathematical proofs are the same), we ought to also believe that "verified proof" is an equally important part of that feedback. A verified proof is a mathematical proof of a logical proposition that was mechanically verified by a computer, as opposed to just peer-reviewed. The "Experiences with Protocol Description" paper from Pamela Zave [Zave11] gives three conclusions about the usage of formal specifications for a protocol standard. The first conclusion states that informal methods (i.e. the absence of verified proofs) are inadequate for widely used protocols. This document is based on the assumption that this conclusion is correct, so its validity will not be discussed further. The second conclusion states that formal specifications are useful even if they fall short of the "gold standard" of a complete formal specification. We will show that a formal specification can be incrementally added to a document. The third conclusion from Zave's paper states that the normative English language should be paraphrasing the formal specification. The difficulty here is that to be able to keep the formal specification and the normative language synchronized at all times, these two should be kept as physically close as possible to each other. To do that we introduce the concept of "Computerate Specifying" (note that Computerate is a British English word). "Computerate Specifying" is a play on "Literate Computing", itself a play on "Structured Computing" (see [Knuth92] page 99). In the same way that Literate Programming enriches code by interspersing it with its own documentation, Computerate Specifying enriches a standard specification by interspersing it with code (or with proofs, as they are the same thing), making it a computerate specification. 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 Petit-Huguenin Expires 29 September 2021 [Page 5] Internet-Draft Computerate Specifying March 2021 is a specific instance of computerate specifying that combines [AsciiDoc] as formatting language and [Idris2] as programming language with the goal of formally specifying IETF protocols. 2. Overview The remaining of this document is divided in 3 parts: After the Terminology (Section 3) section starts a tutorial on how to write a specification. This tutorial is meant to be read in sequence, as concepts defined in early part will not be repeated later. On the other hand the tutorial is designed to present information progressively and mostly in order of complexity, so it is possible to start writing effective specifications without reading or understanding the whole tutorial. The tutorial begins by explaining how to write private specifications (Section 4), which are specifications that are not meant to be shared. Then the tutorial continues by explaining how to write an self-contained specification (Section 5), which is a specification that contains Idris code that relies only on the Idris Standard Library. Writing self-contained specifications is difficult and time-consuming, so the tutorial continues by explained how to import specifications (Section 6) that contain reusable types and code. The tutorial ends with explanations on how to design a exportable specification (Section 7). After the tutorial come the description of all the packages and modules in the Computerate Specifying Standard Library (Section 8). Appendix A explains how to install and use the associated tooling, Appendix B contains the reference manual for the standard library, Appendix D explains how to reuse Colored Petri Nets in a specification, and Appendix E is a tutorial on using Programs and Types to prove propositions. 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 Petit-Huguenin Expires 29 September 2021 [Page 6] Internet-Draft Computerate Specifying March 2021 was published such as the generated document coincides with the published document. In this document, the same word can be used either as an English word or as an Idris identifier used inside the text. To explicitly differentiate them, the latter is always displayed like "this". E.g. "IdrisDoc" is meant to convey the fact that IdrisDoc in that case is an Idris module or type. On the other hand the word IdrisDoc refers to the IdrisDoc specification. Similarly blocks of code, including literate code, are always sandwiched between "" and "". Code blocks will be presented in their literate form only when necessary, i.e. when mixed AsciiDoc and Idris are required. However, in a computerate specification, Idris code must in fact be used in its literate form. By convention an Idris function that returns a type and types themselves will always start with an uppercase letter. Functions not returning a type start with a lowercase letter. For the standard library, the types names are also formed by taking the English word or expression, making the first letter of each word upper case, and removing any symbols like underscore, dash and space. Thus bitvector would become "Bitvector" after conversion as a type name but bit diagram would become "BitDiagram". 4. Private Specifications Nowadays documents at the IETF are written in a format named xml2rfc v3 [RFC7991] but unfortunately making that format Computerable is not trivial, mostly because there is no simple solution to mix code and XML together in the same file. Instead, the [AsciiDoc] format forms the basis for specifications as it permits the generation of documents in the xmlrfc v3 format (among other formats) and also because it can be enriched with code in the same file. AsciiRFC [I-D.ribose-asciirfc] and [Metanorma-IETF] describe a backend for the [Asciidoctor] tool that converts an AsciiDoc document into an xml2rfc v3 document. The AsciiRFC document states various reasons why AsciiDoc is a superior format for the purpose of writing standards, so that will not be discussed further. Note that the same team developed Asciidoctor backends [Metanorma] for other Standards Developing Organizations (SDO), making it easy to develop computerate specifications targeting the documents developed by these SDOs. Petit-Huguenin Expires 29 September 2021 [Page 7] Internet-Draft Computerate Specifying March 2021 The code in a computerate specification uses the programming language [Idris2] in literate programming [Literate] mode using the Bird- style, by having each line of code starting with a ">" mark in the first column. That same symbol is also used by AsciiDoc as an alternate way of defining a blockquote [Blockquotes] way which is no longer available in a computerate specification. Bird-style code will simply not appear in the rendered document. The result of Idris code execution can be inserted inside the AsciiDoc part of a specification by inserting that code fragment between the "{`" string and the "`}" strings. That code fragment must return a value of a type that implements the "Show" interface. A computerate specification is processed by an Asciidoctor preprocessor that does the following: 1. Loads the whole specification as an Idris program, including importing modules. 2. For each instance of an inline code fragment, evaluates that fragment and replaces it (including the delimiters) by the result of that evaluation. 3. Continues with the normal processing of the modified specification. For instance the following document fragment taken from the computerate specification of [RFC8489]: Petit-Huguenin Expires 29 September 2021 [Page 8] Internet-Draft Computerate Specifying March 2021 > rto : Int > rto = 500 > > rc : Nat > rc = 7 > > rm : Int > rm = 16 > > -- A stream of transmission times > transmissions : Int -> Int -> Stream Int > transmissions value rto = value :: transmissions (value + rto) > (rto * 2) > > -- A specific transmission time > transmission : Int -> Nat -> Int > transmission timeout i = index i $ transmissions 0 timeout > > a1 : Int > a1 = rto > > a2 : String > a2 = concat (take (rc - 1) (map (\t => show t ++ " ms, ") > (transmissions 0 rto))) ++ "and " ++ show (transmission rto > (rc - 1)) ++ " ms" > > a3 : Int > a3 = transmission rto (rc - 1) + rto * rm For example, assuming an RTO of {`a1`}ms, requests would be sent at times {`a2`}. If the client has not received a response after {`a3`} ms, the client will consider the transaction to have timed out. is rendered as " For example, assuming an RTO of 500ms, requests would be sent at times 0 ms, 500 ms, 1500 ms, 3500 ms, 7500 ms, 15500 ms, and 31500 ms. If the client has not received a response after 39500 ms, the client will consider the transaction to have timed out." Figure 1 Petit-Huguenin Expires 29 September 2021 [Page 9] Internet-Draft Computerate Specifying March 2021 The Idris2 programming language has been chosen because its type system supports dependent and linear types [Type-Driven], and that type system is the language in which propositions are written. The Idris2 programming also has reflection capabilities and support for meta-programming, also known as elaboration. Following Zave's second conclusion, computerate specifying is not restricted to the specification of protocols, or to property proving. There is a whole spectrum of formalism that can be introduced in a specification, and we will present it in the remaining sections by increasing order of complexity. Note that because the specification language is a programming language, these usages are not exhaustive, and plenty of other usages can and will be found after the publication of this document. At the difference of an RFC which is immutable after publication, the types and code in a specification will be improved over time, especially as new properties are proved or disproved. The latter will happen when a bug is discovered in a specification and a proof of negation is added to the specification, paving the way to a revision of the standard. A private specification is a specification that is not meant to be shared. There is mostly two reasons for a specification to be kept private, as explained in the next sections. 4.1. Private Specifications for New Documents In the simplest case, writing a specification with the goal of publishing the resulting document does not require sharing that specification. This is quite similar to what was done with xml2rfc before the IETF adopted RFC 7991 as the canonical format for Internet-Drafts and RFCs; most people used xml2rfc to prepare their document, but did not share the xml2rfc file beyond the co-authors of the document. In that case writing a specification is straightforward: write the specification from scratch using AsciiDoc for the text and Idris for the formal parts. One effective rule to quickly discover that the Idris code and the AsciiDoc document are diverging is to keep both of them as close as possible to each other. This is most effectively done by having the matching Idris code right after each AsciiDoc paragraph, such as it is then easy to compare each to the other. Petit-Huguenin Expires 29 September 2021 [Page 10] Internet-Draft Computerate Specifying March 2021 Idris itself imposes an order in which types and code must be declared and defined, because it does not by default look for forward references. Because, by the rule above, the text will follow the order the Idris code is organized, the document generated by such specification tends to be naturally easier to implement, because it induces the same workflow than a software implementer will follow when implementing the document. [RFC8489] and [RFC8656] are examples of standards that are easy to implement because are written in the order that a software developer will develop each component. 4.2. Private Specifications for Existing Documents A second reason to write a private specification is for the purpose of doing a review of an existing document, most likely of an Internet-Draft during the standardization process. This is done by first turning the existing document into a specification by converting it into an AsciiDoc document, which can be done manually relatively easily. After this step, the specification can be enriched by adding some Idris code and replacing some of the text with the execution of Idris code fragments. Comparing the original document with a document generated by processing the specification permits to validate that the original document is correct regarding the formalism introduced. Documents that are not generated from a specification do not always have a structure that follow the way a software developer will implement it. When that is the case it will be difficult to add the Idris code right after a paragraph describing its functionality, because the final code may not type-check because of the lack of support for forward references. It could be a signal that the text needs to be reorganized to be more software-development friendly. One alternative is to use a technique named self-inclusion, which is the possibility to change the order of paragraphs in an AsciiDoc document and thus keeping the Idris code in an order that type- checks. This is done by using tags to delimit the text that needs to be moved: Petit-Huguenin Expires 29 September 2021 [Page 11] Internet-Draft Computerate Specifying March 2021 // tag::para1[] Text that describes a functionality > -- Code that implements that functionality. // end::para1[] Then a self-include can move (instead of duplicating) the text inside the tags to a different place, without changing the order of the Idris code: include::Main.adoc[tag=para1] Note that the IETF Trust licences [TLP5] do not grant permission to distribute an annotated Internet-Draft as a whole so redistributing such specification would be a copyright license infringement. But as in this case the specification is not meant to be distributed, there is no infringement possible. 5. Self-Contained Specifications A self-contained specification is a specification where the Idris code does not use anything but the types and functions defined in its standard library, thus not requiring to install anything but Idris2 itself. A specification uses Idris types to specify both how stream of bits are arranged to form valid Protocol Data Units (PDU) and how the exchange of PDUs between network elements is structured to form a valid protocol. In addition a specification can be used to prove or disprove a variety of properties for these types. 5.1. PDU Descriptions The PDUs in a communication protocol determines how data is laid out before it is sent over a communication link. Generally a PDU is described only in the context of the layer that this particular protocol is operating at, e.g. an application protocol PDU only describes the data as sent over UDP or TCP, not over Ethernet or Wi- Fi. PDUs can generally be split into two broad categories, binary and text, and a protocol PDU mostly falls into one of these two categories. Petit-Huguenin Expires 29 September 2021 [Page 12] Internet-Draft Computerate Specifying March 2021 PDU descriptions can be defined as specifications for at least three reasons: the generation of examples that are correct by construction, correctness in displaying the result of calculations, and correctness in representing the structure of a PDU. Independently of these reasons, a PDU description is a basic component of a specification that will probably be needed regardless. 5.1.1. PDU Examples Examples in protocol documents are frequently incorrect, which proves to have a significant negative impact as they are too often misused as normative text. See Appendix C for statistics about the frequency of incorrect examples in RFC errata. Ensuring example correctness is achieved by adding the result of a computation (the example) directly inside the document. If that computation is done from a type that is (physically and conceptually) close to the normative text, then we gain some level of assurance that both the normative text and the derived examples will match. Generating an example that is correct by construction always starts by defining a type that describes the format of the data to display. The Internet Header Format in section 3.1 of [RFC0791] will be used in the following sections as example. In this section we start by defining an Idris type, using a Generalized Algebraic Data Type (GADT). In that case we have only one constructor ("MkInternetHeader") which is defined as a Product Type that "concatenate" all the fields on the Internet Header. One specific aspect of Idris types is that we can enrich the definition of each field with constraints that then have to be fulfilled when a value of that type will be built. 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 Petit-Huguenin Expires 29 September 2021 [Page 13] Internet-Draft Computerate Specifying March 2021 where version: This field is constrained to always contain the value 4. ihl: Int is a builtin signed integer so it is constrained to contain only positive integers lower than 16. others: Same, all the fields are constrained to unsigned integers fitting inside the number of bits defined in [RFC0791]. An Idris type where the fields in a constructor are organized like the "InternetHeader" by ordering them in a sequence is called a Pi type - or, when there is no dependencies between fields as there is in "version = 4", a Product type. Although there is no equivalence in most programming languages to a Pi type, Product types are known as classes in Java and struct in C. Another way to organize a type is called the Sum type, which is a type with multiple constructors that act as alternative. Sum types can be used in C with a combination of struct and union, and since Java 14 by using sealed records. Sum types have a dependent counterpart named a Sigma type, which is a tuple in which the type of the second element depends on the value of the first element. This is mostly returned by functions, with the returned Sigma type carrying both a value and a proof of the validity of that value. From that point it is possible to define a value that fulfills all the constraints. The following values are taken from example 1 in [RFC0791] Appendix A. 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. Petit-Huguenin Expires 29 September 2021 [Page 14] Internet-Draft Computerate Specifying March 2021 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. 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. .... {`example1`} .... will generate the equivalent AsciiDoc text: Petit-Huguenin Expires 29 September 2021 [Page 15] Internet-Draft Computerate Specifying March 2021 .... 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: Note that the minimum value for a correct header is is \{`sizeHeader `div` ihlUnit`}. > sizeHeader : Int > sizeHeader = 20 > ihlUnit : Int > ihlUnit = 4 Petit-Huguenin Expires 29 September 2021 [Page 16] Internet-Draft Computerate Specifying March 2021 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. 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 Petit-Huguenin Expires 29 September 2021 [Page 17] Internet-Draft Computerate Specifying March 2021 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 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; Petit-Huguenin Expires 29 September 2021 [Page 18] Internet-Draft Computerate Specifying March 2021 * 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. 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 29 September 2021 [Page 19] Internet-Draft Computerate Specifying March 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 29 September 2021 [Page 20] Internet-Draft Computerate Specifying March 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. Petit-Huguenin Expires 29 September 2021 [Page 21] Internet-Draft Computerate Specifying March 2021 5.3.2. Data Format Conversion For documents that describe a conversion between different data layouts, having a proof that guarantees that no information is lost in the process can be beneficial. For instance, we observe that syntax encoding tends to be replaced each ten years or so by something "better". Here again isomorphism can tell us exactly what kind of information we lost and gained during that replacement. Here, for example, the definition of a function that would verify an isomorphism between an XML format and a JSON format: 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. Petit-Huguenin Expires 29 September 2021 [Page 22] Internet-Draft Computerate Specifying March 2021 Postel's law proposes an informal way of defining that wiggle room by actually having two different specifications, one that defines a data layout for the purpose of sending it, and another one that defines a data layout for the purpose of receiving that data layout. Existing documents express that dichotomy in the form of the usage of SHOULD/SHOULD NOT/RECOMMENDED/NOT RECOMMENDED [RFC2119] keywords. For example the SDP spec says that "[t]he sequence CRLF (0x0d0a) is used to end a line, although parsers SHOULD be tolerant and also accept lines terminated with a single newline character." This directly infers two specifications, one used to define an SDP when sending it, that enforces using only CRLF, and a second specification, used to define an SDP when receiving it (or parsing it), that accepts both CRLF and LF. Note that the converse is not necessarily true, i.e. not all usages of these keywords are related to Postel's Law. To ensure that the differences between the sending specification and the receiving specification do not create interoperability problems, we can use a variant of isomorphism, as shown in the following example (data constructors and code elided): 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. Petit-Huguenin Expires 29 September 2021 [Page 23] Internet-Draft Computerate Specifying March 2021 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: 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 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. Petit-Huguenin Expires 29 September 2021 [Page 24] Internet-Draft Computerate Specifying March 2021 5.3.4. Implementability When applied, the techniques described in Section 5.1 and Section 5.2 result in a set of types that represents the whole protocol. These types can be assembled together, using another set of types, to represent a simulation of that protocol that covers all sending and receiving processes. The types can then be implemented, and that implementation acts as a proof that this protocol is actually implementable. To make these pieces of code composable, a specification is split in multiple modules, each one represented as a unique function. The type of each of these functions is derived from the state machines described in Section 5.2, by bundling together all the inputs of the state machine as the input for that function, and bundling all the outputs of the state machine as the output of this function. For instance the IP layer is really 4 different functions: * A function that converts between a byte array and a tree representation (parsing). * A function that takes a tree representation and a maximum MTU and returns a list of tree representations, each one fitting inside the MTU. * A function that accumulates tree representations of an IP fragment until a tree representation of a full IP packet can be returned. * A function that convert a tree representation into a byte array. The description of each function is incomplete, as in addition to the input and the output listed, these functions needs some ancillary data, in the form of: * state, which is basically values stored between evaluations of a function, * 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. Petit-Huguenin Expires 29 September 2021 [Page 25] Internet-Draft Computerate Specifying March 2021 5.3.5. Termination Proving that a protocol does not loop is equivalent to proving that a implementation of the types for that protocol does not loop either i.e., terminates. This is done by using the type described in Section 5.3.4 and making sure that it type-check when the "total" keyword is used. 5.3.6. Liveness A protocol may never terminate - in fact most of the time the server side of a protocol is a loop - but it still can do some useful work in that loop. This property is called liveness. 6. Importing Specifications | NOTE: The code for the libraries described in that section is | not yet ready to be published. One of the ultimate goals of this document is to convince authors to use the techniques described there to write their documents. Because doing so requires a lot of efforts, an important intermediate goal is to show authors that the benefits of Computerate Specifying are worth learning and becoming proficient in these techniques. The best way to reach that intermediate goal is to apply these technique to documents that are in the process of being published by the IETF and if issues are found, report them to the authors. Doing that on published RFCs, especially just after their publication, would be unnecessarily mean. On the other hand doing that on all Internet-Drafts as they are published would not be scalable. The best place to do a Computerate Specifying oriented review is when a document enters IETF Last Call. These reviews would then be indistinguishable from the reviews done by an hypothetical Formal Specification Directorate. An argument can be made that, ultimately, writing a specification for a document could be an activity too specialized, just like Security reviews are, and that an actual Directorate should be assembled. 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: Petit-Huguenin Expires 29 September 2021 [Page 26] Internet-Draft Computerate Specifying March 2021 * General types and common presentations. E.g., bit diagrams are a very common way of presenting data, and so reusable types and functions to generate and compare them would accelerate a formalization. The libraries in that category are explained in Section 6.1, in Section 8.1, and its associated reference in Appendix B. * Types and common representations for meta-languages. A few meta- languages are used in documents to formalize some parts of them, so having libraries to formalize these meta-languages also helps accelerating their verification. The libraries in that category are explained in Section 6.2, in Section 8.2, and its associated reference in Appendix B. * Types and common representation for common protocols. Most documents are about modifying or defined new usages for existing protocols, which is why it makes sense to establish libraries of these existing protocols for reuse. The libraries in that category are explained in Section 6.3, in Section 8.3, and its associated reference in Appendix B. Together these libraries form the Computerate Specifying Standard Library (Section 8). These libraries are in fact computerate specifications that, instead of being private, are designed to export types and code and be imported in other computerate specifications. Section 7 describes how to build an specification that can be exported. The types and code in a computerate specification form an Idris package, which is a collection of Idris modules. An Idris module form a namespace hierarchy for the types and functions defined in it and is physically stored as a file. Different types of specification can be combined, for instance an exporting library may import from another specification, and this recursively until importing specifications that are both self- contained and exporting. For convenience each public computerate specification, including the one behind this document, is available as an individual git repository. There is exactly one Idris package per git repository. Appendix A.5 explains how to gain access to these computerate specifications. Petit-Huguenin Expires 29 September 2021 [Page 27] Internet-Draft Computerate Specifying March 2021 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 {`example example1`} In the example above, the "example" function converts an "InternetHeader" value into an "AsciiDoc" block, which is automatically serialized as AsciiDoc text. The "AsciiDoc" module is not limited to generating examples, but can be used to generate any AsciiDoc structure from Idris code. E.g., the tables in Appendix C are generated using that technique. 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. Petit-Huguenin Expires 29 September 2021 [Page 28] Internet-Draft Computerate Specifying March 2021 Using an intermediary type will also permit to correctly generate AsciiDoc that can generate an xmlrfc 3 file that supports both text and graphical versions of a figure. This will be done by having AsciiDoc blocks converted into elements that contains both the 72 column formatted text and an equivalent SVG file, even for code source (instead of using the element). 6.1.2. Common Data Types The type in Section 5.1.1 seems a good representation of the structure of the Internet Header, but the origin of a lot of the values in the constraints does not seems very obvious, and as such are still prone to errors. E.g., the calculation in Section 5.1.2 could be better if it was using the type itself as a source for the calculated data. It also may be more convenient to use types that already have some of the properties we need, instead of having to add a bunch of constraints to the "Int" type. The truth of the matter is that the Idris standard library contains very few predefined types that are useful to specify the syntax of communication protocols. E.g., none of the builtin types ("Int", "Integer", "Double", "Char", "String", etc) are really suitable to describe a PDU syntax, and so should be avoided. For this reason, it is preferable to use the types provided by the Computerate Specifying standard library. We are going to redefine the "InternetHeader" type, but using three modules from the standard library: BitVector: A sequence of bits, or bit-vector, is the most primitive type with which a packet can be described. This module provides a type "BitVector n" that represents a sequence of bit of fixed size "n". The module also provides a set of functions that permits to manipulate bit-vectors. See Section 8.1.2 for a description of the "BitVector" module. Unsigned: The "Unsigned" module provides a type "Unsigned n" that is 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 Petit-Huguenin Expires 29 September 2021 [Page 29] Internet-Draft Computerate Specifying March 2021 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, Data)) -> snd ihl = tetra => (tos : BitVector 8) -> (length : (Unsigned 16, Data)) -> snd length = byte => (id : Unsigned 16) -> (flags : BitVector 3) -> (offset : Unsigned 13, Data)) -> snd offset = octa => (ttl : (Unsigned 8, Time)) -> snd ttl = second => (protocol : BitVector 16) -> (checksum : BitVector 16) -> (source : BitVector 32) -> (dest : BitVector 32) -> (options : List Option) -> (padding : BitVector n) -> InternetHeader version: This is bit-vector, but it always contains the same value, so a constraint states that. Because bit-vectors are not integers, the value must be expressed by a list of "O" (for 0) and "I" (for 1) constructors. ihl: This is an unsigned integer with a size of 4 bits. It is 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. Petit-Huguenin Expires 29 September 2021 [Page 30] Internet-Draft Computerate Specifying March 2021 length: This is an unsigned number with a size of 16 bits, a "Data" dimension and a "byte" unit (8 bits). After casting as denominate numbers, subtracting "ihl" from "length" gives directly the size of the payload, without risk of scaling error. id: This is an unsigned integer. Comparisons and calculations are possible on this field. offset: This is an unsigned number with a length of 13 bits, a "Data" dimension and an "octa" unit (64 bits). Again, adding or subtracting this value after casting to another of the same dimension is guaranteed to return the correct value. ttl: This is a denominate number with "Time" as dimension and "second" as unit. options: This is a variable length field that contains a list of options, which are defined in a separate type named "Option". padding: This is a bit-vector whose length is variable. The "byte", "wyde", "octa", and "tetra" units are precisely defined in [TAOCP]. As we can see the noise in the definition of our type is greatly reduced by using these specialized types, which in turn permits to add even more constraints. We can even constrain the size of a field, like is done for the "padding" field below. In that case the length is calculated in the first constraint by calling the "pad" function, function that calculates the number of bits needed to pad a value of a type that implements the "Size" interface to a word boundary, here 32 bits. The second constraint checks that whatever the length of the padding field is, it is always equal to a zero-filled bit-vector, as returned by the function "bitVector". Petit-Huguenin Expires 29 September 2021 [Page 31] Internet-Draft Computerate Specifying March 2021 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 Dimensions can also be combined to seamlessly build more complex dimensions. For example, all "length" values of sent packets can be added up during a period of time, while keeping beginning and ending times as denominate numbers: dividing the "length" sum by the difference between the end time and the begin time gives us directly the data speed in bits per second (or whatever unit we prefer), with the guarantee that Idris will not let us mix oranges and apples. Here's an example of Sum type that implements some of the variants for an "Option" in an "InternetHeader": Petit-Huguenin Expires 29 September 2021 [Page 32] Internet-Draft Computerate Specifying March 2021 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 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: Show InternetHeader where size (MkInternetHeader version ihl tos length id flags offset ttl protocol checksum source dest options padding) = size version + size ihl + ... size padding We can then define a minimal header, and insert its size, using the right unit, in the document: Petit-Huguenin Expires 29 September 2021 [Page 33] Internet-Draft Computerate Specifying March 2021 > minHeader : Data > minHeader = size $ MkInternetHeader [O, I, O, O] > (5, tetra) > (MkTos 0 [O] [O] [O] [O, O]) > (1000, wyde) > 0 > (MkFlags bitVector bitVector bitVector) > (0, octa) > (64, second) > bitVector > bitVector > (A [O] bitVector bitVector) > (A [O] bitVector bitVector) > [] > [] Note that the minimum value for a correct header is {`fromDenominate (size ih) tetra`} 6.1.4. Typed Petri Nets A better solution than defining an adhoc type for our state machines, as explained in Section 5.2, is to use Petri Nets. 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. A TPN is an algebraic specification of a Petri Net, such as a Petri Net can be expressed as an Idris type, and so easily reused for various purposes. In fact Idris type and code replace the file format used in traditional Petri Net software and will be extended to support graphical visualizations and interactions. Petit-Huguenin Expires 29 September 2021 [Page 34] Internet-Draft Computerate Specifying March 2021 A Petri Net has the advantage that the same graph can be reused to derive other Petri Nets, e.g., Timed Petri Nets (that can be used to collect performance metrics) or Stochastic Petri Nets. A TPN that covers a whole protocol (i.e. client, network, and server) is useful to prove the properties listed in Section 5.3.4, Section 5.3.5, and Section 5.3.6. But the TPN is also designed in a way that each of these parts can be defined separately from the others, making it a Hierarchical TPN. 6.1.4.1. Designing a Typed Petri Net This specification defines a DSL that permits describing a Typed Petri Net (TPN) which is heavily influenced by Colored Petri Nets [CPN] (CPN). The following example of TPN is translated from figure 5.1 of [CPN]: Petit-Huguenin Expires 29 September 2021 [Page 35] Internet-Draft Computerate Specifying March 2021 No : Type No = Int Data : Type Data = String NoxData : Type NoxData = (No, Data) packetsToSend : Ellipse packetsToSend = Port "Packets To Send" NoxData Both nextSend : Ellipse nextSend = Place "NextSend" No (pure 1) a : Ellipse a = Port "A" NoxData Out d : Ellipse d = Port "D" No In export sender : Module ? ? sender = MkModule "Sender" |> AddPort packetsToSend |> AddPlace nextSend |> AddPort a |> AddPort d |> AddTransition (MkTransition "Send Packet" [MkInput packetsToSend (No, Data) pure, MkInput nextSend No pure] [MkOutput (No, Data) packetsToSend pure, MkOutput No nextSend pure, MkOutput (No, Data) a pure] (\((n, d), n') => if n == n' then pure ((n, d), n, (n, d)) else empty)) |> AddTransition (MkTransition "Receive Ack" [MkInput nextSend No pure, MkInput d No pure] [MkOutput No nextSend pure] (\(k, n) => pure n)) The "Ellipse", "Input", "Output", and "Transition" types are the basic types used to describe Typed Petri Nets in computerate specifications and are described in Section 8.1.7. Petit-Huguenin Expires 29 September 2021 [Page 36] Internet-Draft Computerate Specifying March 2021 The "Module" and "Instance" types are used to describe hierarchical TPNs, as in the following example translated from Figure 5.4 of [CPN]. packetsToSend : Ellipse packetsToSend = Place "Packets To Send" NoxData [(1, "COL"), (2, "OUR"), (3, "ED "), (4, "PET"), (5, "RI "), (6, "NET")] dataReceived : Ellipse dataReceived = Place "Data Received" Data (pure "") a : Ellipse a = Place "A" NoxData empty b : Ellipse b = Place "B" NoxData empty : Ellipse c = Place "C" No empty d : Ellipse d = Place "D" No empty export top : Instance [] top = MkInstance (MkModule "top module" |> AddPlace packetsToSend |> AddPlace dataReceived |> AddPlace a |> AddPlace b |> AddPlace c |> AddPlace d |> AddInstance (MkInstance sender [packetsToSend, a, d]) |> AddInstance (MkInstance network [a, b, c, d]) |> AddInstance (MkInstance receiver [b, dataReceived, c]) ) [] | NOTE: For the time being there is no graphical tool available | to directly design, test and debug a Typed Petri Net stored in | a specification. So for now the best alternative is to use the | graphical tool [Cpntools] to design a CPN and then to follow | the step-by-step tutorial (Appendix D) to convert it into a | Typed Petri Net. Petit-Huguenin Expires 29 September 2021 [Page 37] Internet-Draft Computerate Specifying March 2021 6.1.4.2. Using a Typed Petri Net The TPN values created in the previous section are useful to test, debug and validate a protocol, but they cannot be directly used to guarantee that a process is following part or totality of this Petri Net. To do so we need to generate a Sum type that encodes all the transitions as constructors. This type then can serve as a proof that a list of (transition, binding) tuples are valid according to that Petri Net. A binding is the allocation of values to all the variables used in a transition. 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. This example below shows two constructors for the example Petri Net used in this document. sendPacket' : (NOxDATA, NO) -> List (NOxDATA, NO, NOxDATA) updateSendPacket : Marking -> (NOxDATA, NO) -> Marking data T210 : Marking -> Type where Init : T210 initMarking SendPacket : (binding : (NOxDATA, NO)) -> (Elem (fst binding) (pts m)) => (Elem (snd binding) (ns m)) => (sendPacket' binding = pure (fst binding, snd binding, fst binding)) => T210 m -> T210 (updateSendPacket binding m) A "Marking" is an Idris record containing the current values for all the places in a TPN. The "Init" constructor builds an initial marking. Then the "SendPacket" constructor and the other constructors (not shown here) are used to validate a sequence of bindings. 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 Petit-Huguenin Expires 29 September 2021 [Page 38] Internet-Draft Computerate Specifying March 2021 transition using that binding is deterministic. Finally each transition updates the marking according to the output arcs, i.e removing and adding tokens. This type can then be used for various purposes, e.g. to draw a Message Sequence Char 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. 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: Petit-Huguenin Expires 29 September 2021 [Page 39] Internet-Draft Computerate Specifying March 2021 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). {`%runElab toBitDiagram names`} 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 5 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. Convert the CPN into a TPN as described in Section 6.1.4.1. Petit-Huguenin Expires 29 September 2021 [Page 40] Internet-Draft Computerate Specifying March 2021 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.2. 4. Construct an instance of the previous type as a proof that the selected list of (transition, binding) is valid. 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: .... {`generateMsc test [(A, D), (B, C)]`} .... 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. Petit-Huguenin Expires 29 September 2021 [Page 41] Internet-Draft Computerate Specifying March 2021 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. When a PDU is described with a formal language, we end up with two descriptions, one using the Idris dependent type (and used to generate examples) and the other using the formal language. Proving isomorphism requires generating an Idris type from the formal language instance, which is done using an Idris elaborator script. In Idris, Elaborator Reflection [Elab] is a metaprogramming facility that permits writing code generating type declarations and code (including proofs) automatically. For instance the ABNF language is itself defined using ABNF, so after converting that ABNF into an instance of the Syntax type (which is an holder for a list of instances of the Rule type), it is possible to generate a suite of types that represents the same language: Petit-Huguenin Expires 29 September 2021 [Page 42] Internet-Draft Computerate Specifying March 2021 > abnf : Syntax > abnf = MkSyntax [ > "rulelist" `Eq` (Repeat (Just 1) Nothing (Group (Altern > (TermName "rule") (Group (Concat (Repeat Nothing Nothing > (TermName "c-wsp")) (TermName "c-nl") [])) []))), > ... > ] > > %runElab (generateType "Abnf" abnf) 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 29 September 2021 [Page 43] Internet-Draft Computerate Specifying March 2021 import Data.Control.Isomorphism sdp : Syntax sdp = MkSyntax [ "session-description" `Eq` (Concat (TermName "version-field") (TermName "origin-field") [ TermName "session-name-field", Optional (TermName "information-field"), Optional (TermName "uri-field"), Repeat Nothing Nothing (TermName "email-field"), Repeat Nothing Nothing (TermName "phone-field"), Optional (TermName "connection-field"), Repeat Nothing Nothing (TermName "bandwidth-field"), Repeat (Just 1) Nothing (TermName "time-description"), Optional (TermName "key-field"), Repeat Nothing Nothing (TermName "attribute-field"), Repeat Nothing Nothing (TermName "media-description") ]), ... ] %runElab (generateType "Sdp" sdp) same : Iso Sdp SessionDescription same = MkIso to from toFrom fromTo where to : Sdp -> SessionDescription from : SessionDescription -> Abnf toFrom : (x : SessionDescription ) -> to (from x) = x fromTo : (x : Sdp) -> from (to x) = x As stated in Section 5.3.1, the Idris type and the type generated from the formal language are not always isomorphic, because some constraints cannot be expressed in that formal language. In that case isomorphism can be used to precisely define what is missing information in the formal language type. To do so, the generated type is augmented with a delta type, like so: Petit-Huguenin Expires 29 September 2021 [Page 44] Internet-Draft Computerate Specifying March 2021 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. An interesting comment in [Momot16] states that if the input of an application is too complex to be expressed in ABNF without adding comments, it is too complex to be safe. The technique described in this section can be used to evaluate the safety of such ABNF by clearly specifying the impact of these additional comments. Idris elaborator scripts will be developed for each formal languages. The following sections describe how these formal languages have been or will be themselves be converted into types with the goal of importing them in computerate specifications. 6.2.1. Augmented BNF (ABNF) Augmented Backus-Naur Form (ABNF) [RFC5234] is a formal language used to describe a text based data layout. An ABNF can be described by defining a value for the types from the "RFC5234.Main" module: rulename : Rule rulename = "rulename" `Eq` (Concat (TermDec 97 []) (TermDec 98 []) [TermDec 99 []]) That value can then be inserted in a document, which will convert it as a proper ABNF, so Petit-Huguenin Expires 29 September 2021 [Page 45] Internet-Draft Computerate Specifying March 2021 [source,abnf] ---- {`rulename`} ---- is rendered as rulename = %d97 %d98 %d99 Figure 2 See Section 8.2.2 for details on that package. 6.2.2. Augmented Packet Header Diagrams (APHD) Augmented Packet Header Diagram (APHD) [I-D.mcquistin-augmented-ascii-diagrams] is a formal language used to describe an augmented bit diagram in a machine-readable format. It can be seen as an extension to the self-contained bit diagram in Section 5.1.3, where more information are extracted from the Idris type, and more properties are carried in the list of properties: * From the Idris type: - The size of a field in the Idris type is converted into the field's width. - The size constraints in Idris are converted into a variable size field (Section 4.1). - A constraint that reduces the possible values (like for the version field) is converted into a constraint on field value (Section 4.4). - Alternative constructors (i.e., a Sum type) generate a presence predicate (Section 4.2). * From the additional structure: - The name of the PDU. - The name of each field - The eventual short name for each field, with the same constraint than in Section 5. Petit-Huguenin Expires 29 September 2021 [Page 46] Internet-Draft Computerate Specifying March 2021 - 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 29 September 2021 [Page 47] Internet-Draft Computerate Specifying March 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.3. Cosmogol Cosmogol [I-D.bortzmeyer-language-state-machines] is a formal language designed to define states machines. The Internet-Draft will be retrofitted as a computerate specification to provide an internal Domain Specific Language (DSL) that permits specifying an instance of that language. As a Petri Net can be seen as a set of state machines, it will be possible to extract part of a Petri Net and generate the equivalent state machine in Cosmogol format. 6.3. Packages for Protocols Petit-Huguenin Expires 29 September 2021 [Page 48] Internet-Draft Computerate Specifying March 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 29 September 2021 [Page 49] Internet-Draft Computerate Specifying March 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 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 Petit-Huguenin Expires 29 September 2021 [Page 50] Internet-Draft Computerate Specifying March 2021 automatically send a warning when the cache needs to be refreshed. The interactive command ":gc " 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 29 September 2021 [Page 51] Internet-Draft Computerate Specifying March 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 dcp) At this point using elaboration caching would permit to check that the new type indeed uses the "Dscp" type instead of the old "Tos" type. 6.3.2. Extended Registries | NOTE: The mechanisms described in this section requires Type | Providers that are not yet available in Idris2. Until then, | the constants built by future type providers can be populated | by hand. At the difference of the previous section, that describes how to formalize the unplanned evolution of a protocol, most protocols are designed with the potentiality of evolution, also known as extensibility. These potentialities are generally expressed as values for some fields that will be later assigned to a new meaning. The meaning for a new value will be defined in a new document, with all the documents giving new meanings to a field easily locatable in a registry. Following up on our previous example, RFC 791 defines IP Options only for values 0, 1, 7, 68, 131, 136, and 137. These values, together with new values defined by other documents, are listed in the IP Option Numbers IANA registry. E.g., that IANA registry also defines, among others, value 25 in RFC 4782. The values that are part of a registry are designed to be used with the protocol that defined that registry, so it makes sense to synthesise a Sum type of all these values in the computerate specification for the document that defined that registry. Petit-Huguenin Expires 29 September 2021 [Page 52] Internet-Draft Computerate Specifying March 2021 Building that Sum type can be done by applying transformations to the original type, just like when modifying a protocol in a new specification. The difference is that the list of types that will be used in the Sum type needs be collected from the registry, and updated each time the registry is updated. Idris has a mechanism to read external data during type-checking (a feature known as Type Provider), mechanism that could be used to read the content of the registry. A registry generally contains the codepoint that identifies a new value and the name of the document that defines that value, but unfortunately the protocol registries do not contain enough information to automatically find the Idris2 type that matches a specific codepoint. For instance IANA is the organization that is maintaining the registries for the IETF. The "IP Option Numbers" is an example of a registry that contains the list of all the IP Options that can be carried by the Internet Protocol. E.g., in that registry RFC 1191 contains the description for multiple entries in the registry, and so an additional mechanism is needed to find the Idris2 type for each of them. That additional mechanism is abstracted as an extended registry that complements the existing registry, but for the sole purpose of finding the exact type to use for each codepoint to generate that Sum type. Building an "InternetHeader" type that contains all the IP Options defined at the time of type-checking looks like this; %provide (ipParameter : List (String, Decl)) with registry ("https://www.iana.org/assignments/ip-parameters/" ++ "ip-parameters.xhtml#ip-parameters-2") %runELab traverse (add transform internetHeader Add) (type registry) The "%provide" statement reads both the IANA registry and its associated extended registry and stores the result in the "ipParameter" constant. Then the "%runElab" statement repetitively adds the types retrieved to the "InternetHeader" type. Instead of having to manually maintain the extended registries, they can be automatically updated by information coming from the type- checking of the types in the respective computerate specifications that define new values, by binding a specific entry in a registry with the type in the specification. Petit-Huguenin Expires 29 September 2021 [Page 53] Internet-Draft Computerate Specifying March 2021 The mechanism used is also based on a type provider, but this time to update the extended registry instead of reading from it: %provide (mtur: ()) with extendRegistry ("https://www.iana.org/assignments/ip-parameters/" ++ "ip-parameters.xhtml#ip-parameters-2") "11" mtuR %provide (mtut : ()) with extendRegistry ("https://www.iana.org/assignments/ip-parameters/" ++ "ip-parameters.xhtml#ip-parameters-2") "12" mtuT Here the statements bind the types defined in "mtuR" and "mtuT" to codepoints 11 and 12 in the extended registry of IANA's IP Option Numbers registry. The next time the code is type-checked, it will add constructors for these two IP Options. 7. Exporting Specifications | NOTE: The infrastructure for sharing the git repositories for | exported packages is not ready yet. 7.1. Standard Library Computerate specifications can formalize their content to make it reusable as a building block for other specifications. A specification that organizes its content along the guidelines presented in this section can become a part of the Computerate Specification Standard Library. To be part of the Standard Library, specifications must be organized in 4 components: Code: This is the formalization of the content of the standard as an Idris package i.e., a set of Idris modules (i.e. files) that exports some or all of the types and functions defined in it. The code of these Idris modules is generally interspersed with the content of the standard to form literate code. Tutorial: This is a document section that guides the reader step by step in the use of the Idris package in a Computerate Specification. A tutorial may import the package itself to validate the examples provided as part of the tutorial. This section is considered informative. Petit-Huguenin Expires 29 September 2021 [Page 54] Internet-Draft Computerate Specifying March 2021 Description: This is a document section that explains the Idris package as a whole i.e, grouping explanations by feature. Reference: This is a document section that is auto-generated from the structured comments in the types and functions of the code Idris package. It lists all the types and functions in alphabetic order, including the comments on parameters. This document is itself an Idris package that is part of the Standard Library, Section 7 contains the tutorial part of that package, Section 8.1 forms its description part, and Appendix B contains its reference. For a retrofitted document, the code will be mixed with the existing standard to produce a Computerate Specification but the tutorial, description and reference parts cannot be added to that standard, so they have to be part of a separate document. It can be a new specification written for the express purpose of documenting that package. This is the case for this specification, which documents a selection of retrofitted Computerate Specifications that are part of the Standard Library. E.g., Section 6.2.1, and Section 8.2.2 are respectively the tutorial and the description for [RFC5234]. For a new document, the four components should be part of it. E.g., in this document Section 6.1.5.1, Section 8.1.5, and Appendix B.1.2 are respectively the tutorial, description, and reference for the "BitDiagram" module. 7.2. Transclusions RFCs, Internet-Drafts and standard documents published by other SDOs did not start their life as computerate specifications, so to be able to use them as Idris packages they will need to be progressively retrofitted. This is done by converting the documents into an AsciiDoc documents and then enriching them with code, in the same way that would have been done if the standard was developed directly as a computerate specification. Converting the whole document in AsciiDoc and enriching it with code, instead of just maintaining a library of code, seems a waste of resources. The reason for doing so is to be able to verify that the rendered text is equivalent to the original standard, which will validate the examples and formal languages. Retrofitted specifications will also be made available as individual git repositories as they are converted. Petit-Huguenin Expires 29 September 2021 [Page 55] Internet-Draft Computerate Specifying March 2021 Because the IETF Trust does not permit modifying an RFC as a whole (except for translation purposes), a retrofitted RFC uses transclusion, a mechanism that includes parts of a separate document at runtime. This way, a retrofitted RFC is distributed as two separate files, the original RFC in text form, and a computerate specification that contains only code and transclusions. Transclusions use are explained in Appendix A.2.2. 7.3. Exporting Types and Functions Types and functions are exported by using the "export" keyword. Type constructors, interface functions and type functions implementation can be additionally exported by prepending the keyword "public" to the "export" keyword. Additionally, types that may be transformed should be declared as explained in Section 6.3.2, i.e. by wrapping them first in a exported function that uses a quote declaration, then generating them locally using a "declare" elaboration. 8. Standard Library | NOTE: The libraries described in that section are not yet | available. 8.1. Internal Modules 8.1.1. AsciiDoc The AsciiDoc module provides a way to programmatically build an AsciiDoc document without having to worry about the particular formatting details. Note that, at the difference of the AsciiDoc rendering process that tries very hard to render a document in any circumstances, the types in this module are meant to only generate a correct document. E.g., the string "this is {`N "*bold*""}bold` will be rendered as "this is *bold*". If the intent was to render the "bold" word in bold, then the string should have been "this is {`Bold "bold""}`. Petit-Huguenin Expires 29 September 2021 [Page 56] Internet-Draft Computerate Specifying March 2021 8.1.2. BitVector The Computerate Specifying Library provides a number of types and functions aimed at defining and manipulating the data types that are commonly found in Protocol Data Units (PDU). The most elementary type of data is the bit-vector, which is a list of individual bits. Bit-vectors are not always sufficient to describe the subtleties the data types carried in a PDU, and several more precise types are built on top of them. See Section 8.1.3 for unsigned integers. "BitVector" is a dependent type representing a list of bits, indexed by the number of bits contained in that list. The type is inspired by Chapter 6 of [Kroening16] and by [Brinkmann02]. A value of type "BitVector n" can be built as a series of zeros ("bitVector") or can be built by using a list of "O" (for 0) and "I" (for 1) constructors. E.g., "[O, I, O, O]" builds a bit-vector of type "BitVector 4" with a value equivalent to 0b0100. Bit-vectors can be compared for equality, but they are not ordered. They also are not numbers and arithmetics operations cannot be applied to them. Bit-vectors can be concatenated ("concat"), a smaller bit-vector can be extracted from an existing bit-vector ("extract"), or a bit-vector can be extended by adding a number of zeros in front of it ("extend"). The usual unary bitwise ("shiftL", "shiftR", "not") operations are defined for bit-vectors, as well as binary bitwise operations between two bit-vectors of the same size ("and", "or", "xor") Finally it is possible to convert the bit at a specific position in a bit-vector into a "Bool" value ("test"). 8.1.3. Unsigned A value of type "Unsigned n" encodes an unsigned integer as a "BitVector" of length "n". 8.1.4. Dimension This module permits to manipulate denominate numbers, which are numbers associated with a unit. Examples of denominate numbers are "cast (5, meter / second)" (which uses a unit of speed), or "cast (10, meter * meter * meter)" (which uses a unit of volume). Petit-Huguenin Expires 29 September 2021 [Page 57] Internet-Draft Computerate Specifying March 2021 In this module a denominate number is a value of type "Denominate xs". It carries one number as a fraction. Its type is indexed over a list of dimensions, each associated with an exponent number. All together this type can represent any unit that is based directly or indirectly from the base dimensions defined in the "Dimension" type. Denominate numbers are constructed by passing a tuple made of a number (either an "Integer" or a "Double") and a unit to the "cast" function. E.g., "cast (5, megabit)" will build the denominate number 5 with the "megabit" unit. Dimensionless denominate numbers can be constructed by using the "none" unit, as in "cast (10, none)" Denominate numbers can be converted back into a tuple with the "fromDenominate" function. Denominate numbers can be added, subtracted or negated (respectively "+", "-", and "neg"). All these operations can only be done on denominate numbers with the same exact dimension, and the result will also carry the same dimension. This prevents what is colloquially known as mixing apples and oranges. For the same reason, adding a number to a non-dimensionless denominate number is equally impossible. The "*", "/", and "recip" operations respectively multiply, divide and calculate the reciprocal of denominate numbers. These operations can be done on denominate number that have different types, and the result dimension will be derived from the dimension of the arguments. E.g. multiplying "cast (5, meter)" by "cast (6, meter)" will return the equivalent of "cast (30, meter * meter)". Also multiplying a denominate number by a (dimensionless) number is possible e.g., as in multiplying "cast (5, meter)" by "cast (10, none)", which will return the equivalent of "cast (50, meter)". Ultimately we want to insert in a computerate specification the value of a denominate number, together with its unit, as text, which is done by implementing the "Show" interface on a denominate number in its tuple form. E.g. "fromDenominate (cast (5, meter / second)) (kilometer / hour)" can be directly inserted in a document and will be substituted with the string "18 km/h". For each dimension we define a list of constants that represents units of that dimension. Units that uses a prefix are automatically generated, which is the case for SI units for the "Time" dimension (i.e., from "yoctosecond" to "yottasecond"), SI units (only positive Petit-Huguenin Expires 29 September 2021 [Page 58] Internet-Draft Computerate Specifying March 2021 powers of 10) for the "Data" dimension (i.e., from "kilobit" to "yottabit"), and IEC units (positive powers of 2) for the "Data" dimension (i.e., from "kibibit" to "yobibit"). Additional constants like "minute", "hour", "day", "byte", "wyde", "tetra", "octa", etc, complement the standard units. The "byte", "wyde", "tetra", and "octa" units are defined in page 4 of [TAOCP]. 8.1.5. BitDiagram A bit diagram displays a graphical representation of a data layout at the bit level. The "BitDiagram" type is used to build BitDiagrams values. The "toAsciiDoc" function converts a "BitDiagram" value into an AsciiDoc Literal Block which can be inserted directly in the document. Adhoc types can also be used to generate a bit diagram, by passing that type to the "toDiagram" function and the returned value to the "toAsciiDoc" function. The "toDiagram" function will build a field only for types that have an implementation for the "Size" interface. The function "toDiagram" also takes an auxiliary Type "Names" that associate names with these types. 8.1.6. Transform This module permits to manipulate values that are in the very generic form of trees. These manipulations consist of removing, or replacing a selected value or values in that tree. The values to manipulate are selected using a path, which is a series of instructions used to move the focus of the manipulation up, down and sideway in the tree and to apply a predicate until a set of values are chosen. 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. Petit-Huguenin Expires 29 September 2021 [Page 59] Internet-Draft Computerate Specifying March 2021 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. Th "ND" type is an alias to the Non-Deterministic Monad. It is used to represent a returned type that can contain zero, one, or more values, as is the case for most functions stored in TPN values: * For an input arc it represents the fact that some values from the place can be filtered out. * For a transition it represents the fact that values from the input arcs may not unify, or that a guard condition is not met. * For an output arc it represents the fact that even if a transition is enabled, no token may be added. It may also be used to add more than one token to the destination place. The "MultiSet" type permits to build multisets. It is parametrized by the type of the values that will be stored in the multiset. "MS" is an alias for "MultiSet". The "Place" constructor 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. Alternatively the "Port" constructor can be used to build a Petri Net port, which is used to define the interface of a Petri Net module. The "Type_" function returns the type of an "Ellipse". The "Input" type builds an input arc for a transition. An input arc takes tokens from a place and has a type (which can be different from the type of the place). The inscription is a function that chooses the tokens (including none) and generate zero or one value of the input arc type. The type of the codomain of the function is different from the type of the place to permit to do some manipulation on the token itself. The "output" function is used to extract that "Type". The "Output" type builds an output arc for a transition. An output arc takes the binding created by a transition, convert it using the inscription (including generating none) and insert the result in the destination place. Petit-Huguenin Expires 29 September 2021 [Page 60] Internet-Draft Computerate Specifying March 2021 The order of the parameters is the inverse of the "Input" type to show that the function codomain is the type of the place. The "input" function extracts that type from the output arc. The "Transition" type builds a transition by putting together input arcs, output arcs and a function that returns zero binding if the transition is not enabled or one binding to be fed to the output arcs function if the transition is enabled. The "InputType" and "OutputType" functions build the type of the tuple used respectively as domain and codomain of the "Transition" function. The "outputs" and "inputs" functions extract the respective lists from a "Transaction". The "Module" type groups together places, ports, transitions and instances of other modules into a module. The "Instance" type is used to instantiate a module inside a module, by binding places or ports to sockets. A socket is the name given to a port, when used on the outside of a module. A value of type "Instance []" is a top-level TPN, i.e. an instance of a module without ports. The "initialMarking", "enabledTransitions", "bindings", and "transition" functions are used to execute a scenario on a top-level TPN by respectively: building an initial marking; finding all the enabled transitions; for a transition find all the possible bindings and finally generating a new marking using a binding. 8.2. Meta-Language Packages 8.2.1. Augmented Packet Header Diagrams (APHD) The "augmented-ascii-diagram" Idris package provides a set of modules that permits to generate parts of AsciiDoc documents that are conform to the [I-D.mcquistin-augmented-ascii-diagrams] specification. The "AAD.Pdu" type is used to define a PDU. 8.2.2. RFC 5234 (ABNF) TBD. 8.3. Protocol Packages Petit-Huguenin Expires 29 September 2021 [Page 61] Internet-Draft Computerate Specifying March 2021 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", . [AsciiDoc] "AsciiDoc", . [Asciidoctor] "Asciidoctor", . [Bennett15] Bennett, B., "Logically fallacious: the ultimate collection of over 300 logical fallacies", 2015. [Blockquotes] "Markdown-style blockquotes", . [Bornat05] Bornat, R., "Proof and disproof in formal logic: an introduction for programmers", Oxford; New York: Oxford University Press, 2005. [Brinkmann02] Brinkmann, R. and R. Drechsler, "RTL-datapath verification using integer linear programming", In Proceedings of the 2002 Asia and South Pacific Design Automation Conference. IEEE Computer Society, 2002, . [CPN] Jensen, K. and L. Kristensen, "Coloured Petri Nets: Modelling and Validation of Concurrent Systems", Springer Dordrecht ; New York, 2009, . [Cpntools] "CPN Tools: A tool for editing, simulating, and analyzing Colored Petri nets", . Petit-Huguenin Expires 29 September 2021 [Page 62] Internet-Draft Computerate Specifying March 2021 [Curry-Howard] "Curry-Howard correspondence", . [Elab] Christiansen, D. and E. Brady, "Elaborator reflection: extending Idris in Idris", In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. ACM Press-Association for Computing Machinery, 2016, . [I-D.bortzmeyer-language-state-machines] Bortzmeyer, S., "Cosmogol: a language to describe finite state machines", Work in Progress, Internet-Draft, draft- bortzmeyer-language-state-machines-01, 1 November 2006, . [I-D.mcquistin-augmented-ascii-diagrams] McQuistin, S., Band, V., Jacob, D., and C. Perkins, "Describing Protocol Data Units with Augmented Packet Header Diagrams", Work in Progress, Internet-Draft, draft- mcquistin-augmented-ascii-diagrams-06, 1 July 2020, . [I-D.ribose-asciirfc] Tse, R., Nicholas, N., and P. Brasolin, "AsciiRFC: Authoring Internet-Drafts And RFCs Using AsciiDoc", Work in Progress, Internet-Draft, draft-ribose-asciirfc-08, 1 April 2018, . [Idris2] "Idris2: A Language with Dependent Types", . [Knuth92] Knuth, D., "Literate Programming", Center for the Study of Language and Information, 1992. [Kroening16] Kroening, D. and O. Strichman, "Decision Procedures: An Algorithmic Point of View", Springer Berlin, 2017. [Linear-Resources] "Linear Resources", . Petit-Huguenin Expires 29 September 2021 [Page 63] Internet-Draft Computerate Specifying March 2021 [Literate] "Literate Programming", . [Metanorma] "Metanorma", . [Metanorma-IETF] "Metanorma-IETF", . [Mimram20] Mimram, S., "Program = Proof", 2020. [Momot16] Momot, F., Bratus, S., Hallberg, S., and M. Patterson, "The Seven Turrets of Babel: A Taxonomy of LangSec Errors and How to Expunge Them.", In: 2016 IEEE Cybersecurity Development (SecDev), 2016, . [Nederpelt14] Nederpelt, R. and H. Geuvers, "Type theory and formal proof: an introduction", Cambridge; New York: Cambridge University Press, 2014. [RFC-Guide] "RFC Style Guide", . [RFC0761] Postel, J., "DoD standard Transmission Control Protocol", RFC 0761, DOI 10.17487/RFC0761, January 1980, . [RFC0791] Postel, J., "Internet Protocol", RFC 0791, DOI 10.17487/RFC0791, September 1981, . [RFC2119] Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, DOI 10.17487/RFC2119, March 1997, . [RFC5234] Crocker, D., Ed. and P. Overell, "Augmented BNF for Syntax Specifications: ABNF", RFC 5234, DOI 10.17487/RFC5234, January 2008, . Petit-Huguenin Expires 29 September 2021 [Page 64] Internet-Draft Computerate Specifying March 2021 [RFC5246] Dierks, T. and E. Rescorla, "The Transport Layer Security (TLS) Protocol Version 1.2", RFC 5246, DOI 10.17487/RFC5246, August 2008, . [RFC7991] Hoffman, P., "The "xml2rfc" Version 3 Vocabulary", RFC 7991, DOI 10.17487/RFC7991, December 2016, . [RFC8446] Rescorla, E., "The Transport Layer Security (TLS) Protocol Version 1.3", RFC 8446, DOI 10.17487/RFC8446, August 2018, . [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, . [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, . [Stump16] Stump, A., "Verified Functional Programming in Agda", ACM Books series, 2016. [TAOCP] Knuth, D., "The Art Of Computer Programming", Addison- Wesley Pearson Education, 2005. [TLP5] "Legal Provisions Relating to IETF Documents", . [Type-Driven] Brady, E., "Type-Driven Development with Idris", Manning Shelter Island, 2017. [Zave11] Zave, P., "Experiences with Protocol Description", Workshop on Rigorous Protocol Engineering (WRiPE'11), 2011, . Appendix A. Command Line Tools Petit-Huguenin Expires 29 September 2021 [Page 65] Internet-Draft Computerate Specifying March 2021 A.1. Installation The computerate command line tools are run inside a Docker image, so the first step is to install the Docker software or verify that it is up to date (https://docs.docker.com/install/). Note that for the usage described in this document there is no need for Docker EE or for having a Docker account. The following instructions assume a Unix based OS, i.e. Linux or MacOS. Lines separated by a "\" character are meant to be executed as one single line, with the "\" character removed. A.1.1. Download the Docker Image To install the computerate tools, the fastest way is to download and install the Docker image using BitTorrent. The BitTorrent magnet URI for the version distributed with this version of the document is: magnet:?xt=urn:btih:9e508a23ed60f8bdb16f4c056554a5d77e639d8a&dn=tools -07.tar.xz After this, the image can be loaded in Docker as follow: docker load -i tools-07.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. A.2. The "computerate" Command The Docker image main command is "computerate", which takes the same parameters as the "metanorma" command from the Metanorma tooling: docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ computerate/tools computerate -t ietf -x txt The differences with the "metanorma" command are explained in the following sections. Petit-Huguenin Expires 29 September 2021 [Page 66] Internet-Draft Computerate Specifying March 2021 A.2.1. Literate Files The "computerate" command can process Literate Idris files (files with a "lidr" extension, aka lidr files), in addition to AsciiDoc files (files with an "adoc" extension, aka adoc files). When a lidr file is processed, all embedded code fragments (text between prefix "{`" and suffix "`}") are evaluated in the context of the Idris code contained in this file. Each code fragment (including the prefix and suffix) are then substituted by the result of that evaluation. The "computerate" command can process included lidr files in the same way. The embedded code fragments in the imported file are processed in the context of the included lidr file, not in the context of the including file. Idris modules (either from an idr or lidr file) can be imported the usual way. The literate code (which is all the text that is starting by a ">" symbol in column 1) in a lidr file will not be part of the rendered document. A.2.2. Transclusions The "computerate" command can process transclusions, a special form of AsciiDoc "include" that takes a range of lines as parameters: include::rfc5234.txt[lines=26..35] Here the "include" macro will be replaced by the content of lines 26 to 35 (included) of [RFC5234]. The "sub" parameter permits modifying the copied content according to a regular expression. For instance the following converts references into the AsciiDoc format: include::rfc5234.txt[lines=121..131,sub="/\[([^\]])\]/<<\1>>/"] In the following example, the text is converted into a note: include::rfc5234.txt[lines=151,sub="/^.*$/NOTE: \0/"] Petit-Huguenin Expires 29 September 2021 [Page 67] Internet-Draft Computerate Specifying March 2021 A.2.3. IdrisDoc Generation The "computerate" can include in a document the result of the generation of the IdrisDoc for a package. This is done by including a line like this: include::computerate-specifying.ipkg[leveloffset=+2] The "leveloffset" attribute is used to adjust the level of the section generated, as the sections generated always have the level 2. A.2.4. Outputs Instead of generating a file based on the name of the input file, the "computerate" command generates a file based on the ":name:" attribute in the header of the document. In addition to the "txt", "html", "xml", and "rfc" output formats supported by "metanorma", the "computerate" command can also be used to generate for the "pdf" and "json" formats by using these names with the "-x" command line parameter. If the type of document passed to the "computerate" command (options "-t" or "--type") is one of the following, then the document will be processed directly using "asciidoctor", and not "metanorma": "html, "html5, "xhtml", "xhtml5", "docbook", "docbook5", "manpage", "pdf", and "revealjs". The asciidoctor-diagram extension is available in this mode with the following supported diagram types: "actdiag", "blockdiag", "ditaa", "graphviz", "meme", "mscgen", "nwdiag", "plantuml", and "seqdiag". A.2.5. Extended Registry | NOTE: More to come on the exact mechanism used to share the | extended repositories. A.2.6. Bibliography Because most references are stable, there is not much point in retrieving them each time the document is processed, even with the help of a cache, so lookup of external references is disabled. The following command can be used to fetch an RFC reference: tools relaton fetch "IETF(RFC.2119)" --type IETF >ietf.xml Petit-Huguenin Expires 29 September 2021 [Page 68] Internet-Draft Computerate Specifying March 2021 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 Additionally the following sections show how to manually format some common types of bibliographic items, most of then adapted from [RFC-Guide]. A.2.6.1. Internet-Draft Petit-Huguenin Expires 29 September 2021 [Page 69] Internet-Draft Computerate Specifying March 2021 [%bibitem] === {blank} id:: RFC-STYLE title.content:: RFC Style Guide contributor:: contributor.person.name.completename.content:: Heather Flanagan contributor.role.type:: author contributor:: contributor.person.name.completename.content:: Sandy Ginoza contributor.role.type:: author date.type:: published date.on:: 2014-07-20 link:: link.type:: TXT link.content:: https://www.ietf.org/.../draft-flanagan-style-03.txt docid:: docid.type:: Work docid.id:: in Progress docid:: docid.type:: Internet-Draft docid.id:: draft-flanagan-style-03 A.2.6.2. RFC Petit-Huguenin Expires 29 September 2021 [Page 70] Internet-Draft Computerate Specifying March 2021 [%bibitem] === {blank} id:: RFC-STYLE2 title.content:: RFC Style Guide contributor:: contributor.person.name.completename.content:: Heather Flanagan contributor.role.type:: author contributor:: contributor.person.name.completename.content:: Sandy Ginoza contributor.role.type:: author date.type:: published date.on:: 2014-09 link:: link.type:: src link.content:: http://www.rfc-editor.org/info/rfc7322 docid:: docid.type:: RFC docid.id:: 7322 docid:: docid.type:: DOI docid.id:: 10.17487/RFC7322 A.2.6.3. Email [%bibitem] === {blank} id:: reftag title.content:: Subject: Subject line contributor:: contributor.person.name.completename.content:: A. Sender contributor.role.type:: author date.type:: published date.on:: 2014-09-05 link:: link.type:: src link.content:: https://mailarchive.ietf.org/.../Ed4OHwozljyjklpAE/ docid:: docid.type:: message to the docid.id:: listname mailing list A.2.6.4. IANA Petit-Huguenin Expires 29 September 2021 [Page 71] Internet-Draft Computerate Specifying March 2021 [%bibitem] === {blank} id:: IANA-IKE title.content:: Internet Key Exchange (IKE) Attributes contributor.person.name.completename.content:: IANA contributor.role.type:: author link:: link.type:: src link.content:: http://www.iana.org/assignments/ipsec-registry A.2.6.5. Web-Based Public Code Repositories [%bibitem] === {blank} id:: pysaml2 title.content:: Python implementation of SAML2 date.type:: published date.on:: 2018-03-01 docid:: docid.type:: commit docid.id:: 7135d53 link:: link.type:: src link.content:: https://github.com/IdentityPython/pysaml2 A.3. Idris REPL idr and lidr files can be loaded directly in the Idris REPL for debugging: docker run --rm -it -u $(id -u):$(id -g) -v $(pwd):/computerate \ computerate/tools idris2 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 Petit-Huguenin Expires 29 September 2021 [Page 72] Internet-Draft Computerate Specifying March 2021 A.4. Other Commands For convenience, the docker image provides the latest version of the xml2rfc, aspell, and idnits tools. docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ computerate/tools xml2rfc docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ computerate/tools idnits --help docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ computerate/tools aspell The Docker image also contains a extended version of git that will be used to retrieve the computerate specifications as explained in Appendix A.5. A.5. Source Repositories | NOTE: More to come on the exact mechanism used to retrieve the | source repositories. A.6. Modified Tools The following sections list the tools distributed in the Docker image that have been modified for integration with the "computerate" tool. A.6.1. Idris2 URL: https://github.com/idris-lang/Idris2.git Version: 0.3.0 commit ec77ad2 Modifications: * 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. * "--mkdoc " generates the package documentation in AsciiDoc on stdout. * 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 marks. Petit-Huguenin Expires 29 September 2021 [Page 73] Internet-Draft Computerate Specifying March 2021 A.6.2. asciidoctor URL: https://github.com/asciidoctor/asciidoctor.git Version: 2.0.12 Modifications: * Process lidr and lipkg files. * Preprocessor for Idris literate source. * Include processor for transclusions. A.6.3. metanorma URL: https://github.com/metanorma/metanorma Version: 1.2.7 Modifications: * Generate the filename from the name header attribute. * Process files with lidr and lipkg extensions. A.6.4. metanorma-ietf URL: https://github.com/metanorma/metanorma-ietf Version: 2.2.9 Modifications: * Remove the
wrapper in elements. * Fix the content of the generated so it is displayed correctly in html and pdf outputs. * Fix empty RFC number. * Add generation of json file. * Generates DOI, RFC and Internet-Draft references. Truncate the date according to type. * Do not add content in xrefs. A.6.5. idris2-vim URL: https://github.com/edwinb/idris2-vim Version: commit 964cebe Modifications: * the "IdrisGenerateCache" command (mapped to _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 29 September 2021 [Page 74] Internet-Draft Computerate Specifying March 2021 A.7. Bugs and Workarounds Installation: * The current version of Docker in Ubuntu fails, but this can be fixed with the following commands: sudo apt-get install containerd.io=1.2.6-3 sudo systemctl restart docker.service 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: * Multiline address results in one line. * 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 computerate: * code blocks escape a '>' in the first column. The workaround is to insert a space before the '>'. A.8. TODO List Idris2: * Add documentation support for all types in TTImp. * ":gc!" should update the file. * "%cacheElab" should check hashes. * Add a way to generate a hole name. Petit-Huguenin Expires 29 September 2021 [Page 75] Internet-Draft Computerate Specifying March 2021 * Literate ipkg to merge the Main.adoc and ipkg files. metanorma: * Merge bibliographies. * Extract bibliography from computerate specification. * Generate xml2rfc element. * Generate .rfc.xml and err file with the same name. * Generate rfc.xml as xml and xml under another extension so the xml2rfc file can be directly submitted to the IETF secretariat. computerate: * Generate sourcecode blocks from existing code. * Pass surrounding line for embedded code so the Asciidoc module can process constrained elements. * Implement self-inclusion to reorder a document. * Backport embedded blocks from Coriander. vim: * Starting vim in docker often result in an invalid terminal size when a file is loaded. Using the following command line solves the problem: docker run --rm -it -u $(id -u):$(id -g) -e COLUMNS=$(tput cols) \ -e LINES=$(tput lines) -v $(pwd):/computerate computerate/tools \ vim rfc2adoc: * This future tool will be able to convert an xml2rfc v3 file into an AsciiDoc file. It will also be able to update an already converted file without losing the Idris annotations. Appendix B. Reference | NOTE: The code for the libraries described in that section is | not yet ready to be published. B.1. Package computerate-specifying The Builtin Computerate Specification Standard Library. Version: 0.1 Author(s): Marc Petit-Huguenin Dependencies: augmented-ascii-diagrams, rfc5234 Petit-Huguenin Expires 29 September 2021 [Page 76] Internet-Draft Computerate Specifying March 2021 B.1.1. Module ComputerateSpecifying.AsciiDoc A module to generate valid AsciiDoc. data Block : Type A block of text Implements Show. Admonition : Block Example : Block Listing : Block Literal : List String -> Block Passthrough : Block Quote : Block Sidebar : Block Source : (lang : Maybe String) -> List String -> Block Stem : Block Table : Block Verse : Block Paragraph : (lines : List Line) -> length lines > 0 = True => Block record Document An AsciiDoc document constructor: MkDocument data Inline : Type A type for inline text. Lit : String -> Inline Italic : List Inline -> Inline Bold : List Inline -> Inline Petit-Huguenin Expires 29 September 2021 [Page 77] Internet-Draft Computerate Specifying March 2021 Subscript : List Inline -> Inline Superscript : List Inline -> Inline Monospace : List Inline -> Inline Highlight : List Inline -> Inline Custom : String -> List Inline -> Inline Attribute : String -> Inline Link : (uri : String) -> (text : List Inline) -> (attributes : List String) -> Inline uri: The URI text: The text attributes: Additional attributes Xref : String -> List Inline -> List String -> Inline Code : String -> Inline Embedded code. data Line : Type MkLine : (inlines : List Inline) -> length inlines > 0 = True => Line B.1.2. Module ComputerateSpecifying.BitDiagram data BitDiagram : List String -> Type Field : (name : String) -> (size : Nat) -> size > 0 && size * 2 > length name = True => BitDiagram names -> elem name names = False => BitDiagram (name :: names) Last : (name : String) -> (size : Nat) -> size > 0 && size * 2 > length name = True => BitDiagram [name] data Names : Type -> Type toAsciiDoc : BitDiagram names -> Block toDiagram : (t : Type) -> Names t -> BitDiagram _ B.1.3. Module ComputerateSpecifying.BitVector (++) : BitVector n -> BitVector m -> BitVector (n + m) Concatene the second bit-vector after the first one. Petit-Huguenin Expires 29 September 2021 [Page 78] Internet-Draft Computerate Specifying March 2021 data Bit : Type O : Bit I : Bit data BitVector : Nat -> Type A vector of bit that can be pattern matched. Implements DecEq, Eq, Size. Nil : BitVector Z (::) : Bit -> BitVector n -> BitVector (S n) and : (1 _ : BitVector m) -> (1 _ : BitVector m) -> BitVector m Bitwise and between bit-vectors of identical size. bitVector : {m : Nat} -> BitVector m Build an empty bit-vector 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 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 Petit-Huguenin Expires 29 September 2021 [Page 79] Internet-Draft Computerate Specifying March 2021 Return a boolean that is True if the bit at position m is set. xor : (1 _ : BitVector m) -> (1 _ : BitVector m) -> BitVector m Bitwise xor between bit-vectors of identical size. B.1.4. Module ComputerateSpecifying.Dimension A module that defines types, constants and operations on denominate numbers. (*) : Denominate xs -> Denominate ys -> Denominate (merge' xs ys) The multiplication operation between denominate numbers. (+) : Denominate xs -> Denominate xs -> Denominate xs The addition operation between denominate numbers. (-) : Denominate xs -> Denominate xs -> Denominate xs The subtraction operation between denominate numbers. (/) : Denominate xs -> Denominate ys -> Denominate (merge' xs (recip' ys)) The division operation between denominate numbers. Data : Type The type of a denominate number for the data dimension. data Denominate : List (Dimension, Int) -> Type A denominate number. MkDenominate : (x : Integer) -> (y : Integer) -> {xs : List (Dimension, Int)} -> Denominate xs Construct a denominate number as a fraction. Dimensionless : Type The type of a dimensionless denominate number interface Size a An interface to retrieve the size in bits of a type. Implemented by List, (s, x). size : a -> Data Return the size of a in bit. Time : Type The type of a denominate number for the time dimension. bit : Data Petit-Huguenin Expires 29 September 2021 [Page 80] Internet-Draft Computerate Specifying March 2021 Bit, the base unit of data. byte : Data The byte unit, as 8 bits. day : Time The day, as unit of time. fromDenominate : (value : Denominate xs) -> (unit : Denominate xs) -> (Double, Denominate xs) Convert a denominate number into a tuple made of the dimensionless value (as a "Double") calculated after applying a unit, and that unit. value: the value to convert. unit: the unit to use for the conversion. elaboration generate bin "bit" "Data" Generate all the IEC units based on the bit, from kibibit to yobibit. elaboration generate dec "bit" "Data" Generate all the SI units based on the bit, from kilobit to yottabit. elaboration generate si "second" "Time" Generates all the SI units based on the second, from yoctosecond to yottasecond. hour : Time The hour, as unit of time. minute : Time The minute, as unit of time. neg : Denominate xs -> Denominate xs The negation operation of a denominate number. none : Dimensionless The unit for a dimensionless denominate number. octa : Data The octa unit, as 64 bits. recip : Denominate xs -> Denominate (recip' xs) The reciprocal operation of a denominate number. second : Time Petit-Huguenin Expires 29 September 2021 [Page 81] Internet-Draft Computerate Specifying March 2021 Second, the base unit of time. tetra : Data The tetra unit, as 32 bits. wyde : Data The wyde unit, as 16 bits. B.1.5. Module ComputerateSpecifying.Tpn A module that defines types for Petri Net. data Direction : Type In : Direction Out : Direction Both : Direction data Ellipse : Type Implements Eq. Place : String -> (type : Type) -> (init : MS type) -> Ellipse An ellipse is either a place or a port/socket. type: The type of the tokens stored in the place. init: A function to initialize the place. Port : String -> (type : Type) -> (dir : Direction) -> Ellipse A port. type: The type of the tokens stored in the port. dir: The direction of the port. data Input : Type MkInput : (ellipse : Ellipse) -> (output : Type) -> (inscription : Type_ ellipse -> ND output) -> Input An input arc. ellipse: The ellipse from which tokens are removed. output: The type of the tokens after applying the inscription. inscription: A function that converts the tokens from the place into the output type. InputType : List Input -> Type Calculate the combined type of a list of inputs. data Instance : List Ellipse -> Type Petit-Huguenin Expires 29 September 2021 [Page 82] Internet-Draft Computerate Specifying March 2021 A module instance. MkInstance : (mod : Module xs ys) -> (maps : List Ellipse) -> length ys = length maps => Instance maps An instance of a module mod: The module. maps: The list of mapping between sockets and places or ports. MS : Type -> Type An alias for a MultiSet data Module : (xs : List Ellipse) -> (ys : List Ellipse) -> Type A module. MkModule : (name : String) -> Module [] [] Build an empty module. AddPlace : (x : Ellipse) -> Module xs ys -> Module (x :: xs) ys Declare a new place or port local to this module. AddPort : (x : Ellipse) -> Module xs ys -> Module xs (x :: ys) AddTransition : (t : Transition) -> Module xs ys -> all (\(MkInput s _ _) : ? => elem s (xs ++ ys)) (inputs t) = True => all (\(MkOutput _ s _) : ? => elem s (xs ++ ys)) (outputs t) = True => Module xs ys Declare a new transition, checking that the places used are declared in this module. AddInstance : (i : Instance zs) -> Module xs ys -> all (\x : ? => elem x (xs ++ ys)) zs = True => Module xs ys Declare a new instance of a module, checking that the places used are declared in this module. MultiSet : Type -> Type A MultiSet ND : Type -> Type Non-determinism monad. data Output : Type MkOutput : (input : Type) -> (ellipse : Ellipse) -> (inscription : input -> MS (Type_ ellipse)) -> Output An output arc. input: The type of the values from the transition. inscription: a function that generates the tokens to be Petit-Huguenin Expires 29 September 2021 [Page 83] Internet-Draft Computerate Specifying March 2021 inserted in the place. OutputType : List Output -> Type Calculate the combined type of a list of outputs. data Transition : Type MkTransition : (name : String) -> (inputs : List Input) -> (outputs : List Output) -> (transition : InputType inputs -> ND (OutputType outputs)) -> Transition A transition. name: The name of the transition inputs: The list of inputs. outputs: The list of outputs. transition: A function that chooses and converts between a tuple made of the type of all the inputs into a tuple made of the type of all the outputs. Type_ : Ellipse -> Type Retrieve the type of token that can be stored in the place. Types : List Type -> Type Convert a list of types into a tuple of types. bindings : Marking -> Instance [] -> Transition -> List Binding List all the bindings from a making and a transition. enabledTransitions : Marking -> Instance [] -> List Transition List all the enabled transitions from a marking. initialMarking : Instance [] -> Marking Builds an initial marking. input : Output -> Type inputs : Transition -> List Input isSocket : Ellipse -> Bool mappings : Instance xs -> List Ellipse output : Input -> Type outputs : Transition -> List Output transition : Marking -> Instance [] -> Transition -> Binding -> Marking Petit-Huguenin Expires 29 September 2021 [Page 84] Internet-Draft Computerate Specifying March 2021 Transition to a new marking (|>) : a -> (a -> b) -> b Chain functions on the opposite direction of `$'. Fixity: Left associative, precedence 0 B.1.6. Module ComputerateSpecifying.Transform A module to transform values structured as trees, with specialization to transform types via elaboration. data Path : Type A selection path add : (tree : a) -> (path : Path) -> (added : b) -> a Add a value as a sibling to values in a tree that are selected by a path. tree: The tree to modify. 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. Petit-Huguenin Expires 29 September 2021 [Page 85] Internet-Draft Computerate Specifying March 2021 tree: The tree to modify. path: The path used to select the values. replacement: The value to used as replacement. B.1.7. Module ComputerateSpecifying.Unsigned An unsigned number with a length. data Unsigned : (m : Nat) -> Type An unsigned integer is just a wrapper around a bit-vector of the same size. For sanity sake, this type always assumes that the value of a bit is 2 ^ m - 1, with m the size of the unsigned int. In other words the first bit is the MSB, the last bit (the closer to Nil) is the LSB. Implements Num, Integral, Eq, Ord, Size. MkUnsigned : BitVector m -> Unsigned m B.2. Package rfc5234 Version: 0.1 Author(s): Marc Petit-Huguenin B.2.1. Module RFC5234.Core The ABNF Core rules. alpha : Rule An ASCII alphabetic character. bit : Rule A "0" or "1" ASCII character. char : Rule Any ASCII character, starting at SOH and ending at DEL. cr : Rule A Carriage Return ASCII character. crlf : Rule A Carriage Return ASCII character, followed by the Line Feed ASCII character. ctl : Rule Any ASCII control character. Petit-Huguenin Expires 29 September 2021 [Page 86] Internet-Draft Computerate Specifying March 2021 digit : Rule Any ASCII digit. dquote : Rule A double-quote ASCII character. hexdig : Rule Any hexadecimal ASCII character, in lower and upper case. htab : Rule A Horizontal Tab ASCII character. lf : Rule A Line Feed ASCII character. lwsp : Rule A potentially empty string of space, horizontal tab, or line terminators, that last one followed by a space or horizontal tab. octet : Rule A 8-bit value. sp : Rule An ASCII space. vchar : Rule A printable ASCII character. wsp : Rule A potentially empty string of space, or horizontal tab. B.2.2. Module RFC5234.Main A module to generate a valid ABNF. data Form : Type Implements Show. TermName : String -> Form TermHex : Int -> List Int -> Form TermDec : Int -> List Int -> Form TermBin : Int -> List Int -> Form TermString : String -> Form Petit-Huguenin Expires 29 September 2021 [Page 87] Internet-Draft Computerate Specifying March 2021 Concat : Form -> Form -> List Form -> Form Altern : Form -> Form -> List Form -> Form TermHexRange : Int -> Int -> Form TermDecRange : Int -> Int -> Form TermBinRange : Int -> Int -> Form Group : Form -> Form Repeat : Maybe Int -> Maybe Int -> Form -> Form Optional : Form -> Form data Rule : Type An ABNF rule. Implements Show. Eq : (name : String) -> (form : Form) -> Rule Construct a rule. Inc : String -> Form -> Rule Construct an incremental rule. data Syntax : Type A list of rules. Implements Show. MkSyntax : List Rule -> Syntax B.3. Package augmented-ascii-diagrams Version: 0.1 Author(s): Marc Petit-Huguenin Dependencies: rfc5234 B.3.1. Module AAD.Main A module to generate augmented packet header diagrams. data BoolExpr : List Name -> Type A boolean expression Implements ShowPrec, Show. Petit-Huguenin Expires 29 September 2021 [Page 88] Internet-Draft Computerate Specifying March 2021 Equ : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) Neq : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) Gt : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) Gte : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) Lt : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) Lte : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) And : BoolExpr xs -> BoolExpr ys -> BoolExpr (xs ++ ys) Or : BoolExpr xs -> BoolExpr ys -> BoolExpr (xs ++ ys) Not : BoolExpr xs -> BoolExpr xs data Expr : List Name -> Type An expression Implements ShowPrec, Show. Val : Nat -> Expr [] Var : (n : Name) -> Expr [n] Mul : Expr xs -> Expr ys -> Expr (xs ++ ys) Div : Expr xs -> Expr ys -> Expr (xs ++ ys) Mod : Expr xs -> Expr ys -> Expr (xs ++ ys) Exp : Expr xs -> Expr ys -> Expr (xs ++ ys) Add : Expr xs -> Expr ys -> Expr (xs ++ ys) Sub : Expr xs -> Expr ys -> Expr (xs ++ ys) ITE : BoolExpr xs -> Expr ys -> Expr zs -> Expr (xs ++ ys ++ zs) data Name : Type A name MkName : Maybe String -> String -> Name Petit-Huguenin Expires 29 September 2021 [Page 89] Internet-Draft Computerate Specifying March 2021 B.4. Package rfc791 Version: 0.1 Author(s): Marc Petit-Huguenin Dependencies: computerate-specifying B.4.1. Module RFC791.Address This module provides types for Internet Protocol Address. data IP : Type An IP address. Implements Size. A : (h : BitVector 1) -> h = [O] => (net : BitVector 7) -> (host : BitVector 24) -> IP A class A address. B : (h : BitVector 2) -> h = [I, O] => (net : BitVector 14) -> (host : BitVector 16) -> IP A class B address. C : (h : BitVector 3) -> h = [I, I, O] => (net : BitVector 21) -> (host : BitVector 8) -> IP A class C address. B.4.2. Module RFC791.IP Types for the Internet Protocol. data Flags : Type Flags. Implements Size. MkFlags : (reserved : BitVector 1) -> reserved = bitVector => (df : BitVector 1) -> (mf : BitVector 1) -> Flags data InternetHeader : Type Internet Protocol Header. Implements Size. MkInternetHeader : (version : BitVector 4) -> version = [O, I, O, O] => (ihl : (Unsigned 4, Data)) -> snd ihl = tetra => (tos : Tos) -> (length : (Unsigned 16, Data)) -> snd length = wyde => Petit-Huguenin Expires 29 September 2021 [Page 90] Internet-Draft Computerate Specifying March 2021 (id : Unsigned 16) -> (flags : Flags) -> (offset : (Unsigned 13, Data)) -> snd offset = octa => (ttl : (Unsigned 8, Time)) -> snd ttl = second => (protocol : BitVector 16) -> (checksum : BitVector 16) -> (source : IP) -> (dest : IP) -> (options : List Option) -> (padding : BitVector n) -> InternetHeader data Option : Type Internet Protocol Header Options. Implements Size. Eoo : (flag : BitVector 1) -> flag = [O] => (class : BitVector 2) -> class = [O, O] => (number : BitVector 5) -> number = [O, O, O, O, O] => Option End of Options. Noop : (flag : BitVector 1) -> flag = [O] => (class : BitVector 2) -> class = [O, O] => (number : BitVector 5) -> number = [O, O, O, I, O] => Option No operation. Security : (flag : BitVector 1) -> flag = [I] => (class : BitVector 2) -> class = [O, O] => (number : BitVector 5) -> number = [O, O, O, I, O] => (length : Unsigned 8) -> length = 11 => (s : BitVector 16) -> (c : BitVector 16) -> (h : BitVector 16) -> (tcc : BitVector 24) -> Option Security Option. Lssr : (flag : BitVector 1) -> flag = [I] => (class : BitVector 2) -> class = [O, O] => (number : BitVector 5) -> number = [O, O, O, I, I] => (length : Unsigned 8) -> (pointer : Unsigned 8) -> pointer >= 4 = True => Option Loose Source and Record Route Option. data Tos : Type Type of Service Implements Size. MkTos : (precedence : Unsigned 3) -> (delay : BitVector 1) -> (throughput : BitVector 1) -> (reliability : BitVector 1) -> (reserved : BitVector 2) -> reserved = bitVector => Tos internetHeader : List Decl Petit-Huguenin Expires 29 September 2021 [Page 91] Internet-Draft Computerate Specifying March 2021 Appendix C. Errata Statistics In an effort to quantify the potential benefits of using formal methods at the IETF, an effort to relabel the Errata database is under way. The relabeling uses the following labels: +==========+==============================================+ | 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 29 September 2021 [Page 92] Internet-Draft Computerate Specifying March 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 library_tpn (Section 8.1.7) module, as explained in the following sections. Colored Petri Nets are explained in [CPN] and in [Cpntools]. [Aalst11] is also a good introduction to Colored Petri Nets. Petit-Huguenin Expires 29 September 2021 [Page 93] Internet-Draft Computerate Specifying March 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 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 bool color set. The bool color set can be replaced by the "Bool" type. Petit-Huguenin Expires 29 September 2021 [Page 94] Internet-Draft Computerate Specifying March 2021 B : Type B = Bool 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 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 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: Petit-Huguenin Expires 29 September 2021 [Page 95] Internet-Draft Computerate Specifying March 2021 data SmallLargeInt : Type where MkSmallLargeInt : (i : Integer) -> i >= 1 && i <= 10 = True => SmallInt D.1.1.5. Real Color Sets See http://cpntools.org/2018/01/09/real-color-sets/ for the definition of the real color set. The real color set can be replaced by the "Double" type. R : Type R = Double 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 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 Petit-Huguenin Expires 29 September 2021 [Page 96] Internet-Draft Computerate Specifying March 2021 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 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 index color set. An index color set can be implemented as a dependent type: data PH : Type where MkPH : (i : Nat) -> i >= 1 && i <= 5 => 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 product color set. The product color set can be replaced by the "Pair" type, which can also be represented as a tuple. Petit-Huguenin Expires 29 September 2021 [Page 97] Internet-Draft Computerate Specifying March 2021 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 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 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 => ShortBoolList D.1.2.4. Union Color Sets See http://cpntools.org/2018/01/09/union-color-sets/ for the definition of the union color set. The union color set can be replaced by a Sum type. Petit-Huguenin Expires 29 September 2021 [Page 98] Internet-Draft Computerate Specifying March 2021 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 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 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 TBD. D.2. Convert Places Converting a CPN Place is straightforward. It is represented as the TPN constructor "Place" of type "Ellipse". * The name of the place goes into the first parameter of the constructor. * The color, after conversion as explained in Appendix D.1. goes into the second parameter. Petit-Huguenin Expires 29 September 2021 [Page 99] Internet-Draft Computerate Specifying March 2021 * The marking initialization, after convertion into a multiset of the place type, goes into the third parameter. An empty marking initialization uses the "empty" expression. E.g., the "Packets To Send" Place in Figure 2.1 of [CPN] can be translated as follow: packetsToSend : Ellipse packetsToSend = Place "Packets To Send" NoxData [(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. D.3. Convert Transitions TBD. D.3.1. Convert Input Arcs TBD. D.3.2. Convert Inhibitor Arcs TBD. D.3.3. Convert Reset Arcs TBD. D.3.4. Convert Output Arcs TBD. D.3.5. Convert Transitions with Time TBD. D.3.6. Convert Transitions with Priorities TBD. Petit-Huguenin Expires 29 September 2021 [Page 100] Internet-Draft Computerate Specifying March 2021 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". * 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. Petit-Huguenin Expires 29 September 2021 [Page 101] Internet-Draft Computerate Specifying March 2021 * 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 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. Petit-Huguenin Expires 29 September 2021 [Page 102] Internet-Draft Computerate Specifying March 2021 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. 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 Petit-Huguenin Expires 29 September 2021 [Page 103] Internet-Draft Computerate Specifying March 2021 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) 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: Petit-Huguenin Expires 29 September 2021 [Page 104] Internet-Draft Computerate Specifying March 2021 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 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_). Petit-Huguenin Expires 29 September 2021 [Page 105] Internet-Draft Computerate Specifying March 2021 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 Here we cannot complete the program because we cannot produce a value of type Void, and that's because Int has Yes as answer. Petit-Huguenin Expires 29 September 2021 [Page 106] Internet-Draft Computerate Specifying March 2021 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 29 September 2021 [Page 107] Internet-Draft Computerate Specifying March 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 has 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. Petit-Huguenin Expires 29 September 2021 [Page 108] Internet-Draft Computerate Specifying March 2021 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 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: Petit-Huguenin Expires 29 September 2021 [Page 109] Internet-Draft Computerate Specifying March 2021 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. Pi Type TBD. E.1.9. Sigma Type TBD. E.1.10. Inductive Type TBD. E.1.11. Equality Type TBD. E.1.12. Decidable Type TBD. E.2. How to Find Evidence TBD Acknowledgements Thanks to Jim Kleck, Eric Petit-Huguenin, Nicolas Gironi, Stephen McQuistin, and Greg Skinner for the comments, suggestions, questions, and testing that helped improve this document and its associated tooling. Thanks to Ronald Tse and the Ribose team for the metanorma and relaton tools and their diligence in fixing bugs and implementing improvements. Petit-Huguenin Expires 29 September 2021 [Page 110] Internet-Draft Computerate Specifying March 2021 Contributors Stephane Bryant Email: stephane.ml.bryant@gmail.com Changelog 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. - 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. Petit-Huguenin Expires 29 September 2021 [Page 111] Internet-Draft Computerate Specifying March 2021 * Tooling: - Fix idrisdoc when generating multiplicity. - Upgrade asciidoctor to 2.0.12. - Upgrade xml2rfc to 3.5.0. - xml2rfc --validation option makes patch unnecessary. - Upgrade metanorma (1.2.5) and dependencies. - The tooling docker image is now distributed as a BitTorrent. - Idnits upgraded to 2.16.05. * Library: - Use linear types in some BitVector functions. draft-petithuguenin-computerate-specifying-04: * Document: - Sections 2, 3, 4 and 5 have been completely reorganized, edited, and extended as a tutorial. - New Terminology section. - Add a new Standard Library section, that contains the description of all the Idris modules and external packages that will be available for developing specifications. - Improve bibliography. - Extend the CLI section to cover: o New features. o Bibliography templates. o Complete bugs and TODO lists. - Generate IdrisDoc of standard library packages and modules as a new appendix. - Update errata stats. - More compact changelog. - Many modifications following Stephane's reviews. * 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. Petit-Huguenin Expires 29 September 2021 [Page 112] Internet-Draft Computerate Specifying March 2021 - Add support for asciidoctor outputs, including revealjs and diagrams. - Embedding code must now return a value that implements "Show". String values are then stripped of their first and last double- quotes. - Fix bug where transcluded text is converted into ASCII art. - Embedded code in examples in lidr files can now be escaped with "\". - Replace Idris with Idris2 version 0.2.1. - Update metanorma to 1.1.4. - Update metanorma-ietf to 2.2.2. - Update xml2rfc to 3.0.0. - Downgrade idnits to 2.16.04. - Decommission the Docker image in dat://78f80c850af509e0cd3fd7bd 6f5d0dd527a861d783e05574bbd040f0502da3c6. * Library: - Decommission the RFC 5234 library for complete rewrite. draft-petithuguenin-computerate-specifying-03: * Document: - Notes are now correctly displayed. - Add "Implementations Oriented Standards" section. - Add "Extended Registries" section and appendix. - Add paragraph about hierarchical petri nets. - Convert "Verified Code" section into a top level section, and expand it. - Add "Implementation-Oriented Standards" section. * Tooling: - Many bug fixes in metanorma-ietf. - 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. Petit-Huguenin Expires 29 September 2021 [Page 113] Internet-Draft Computerate Specifying March 2021 - Status is now experimental. - Many nits. - Fix incorrect errata stats. - Move acknowledgment section at the end. - Rewrite the APHD section (formerly known as AAD) to match draft-mcquistin-augmented-diagrams-01. - Fix non-ascii characters in the references. - Intermediate AsciiDoc representation for serializers. * Tooling - xmlrfc3 is now the default extension. - "docName" and "category" attributes are now generated, and the "prepTime" is removed. - Update xml2rfc to 2.35.0. - Remove LanguageTool. - Update Metanorma to version 0.3.17. - Update Asciidoctor to 2.0.10. - Update list of Working Groups. * Library - No update. draft-petithuguenin-computerate-specifying-01: * Document - New changelog appendix. - Fix incorrect reference, formatting in Idris code. - Add option to remove container in all "docker run" command. - Add explanations to use the Idris REPL and VIM inside the Docker image. - Add placeholders for ASN.1 and RELAX NG languages. - New Errata appendix. - 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 Petit-Huguenin Expires 29 September 2021 [Page 114] Internet-Draft Computerate Specifying March 2021 Marc Petit-Huguenin Impedance Mismatch LLC Email: marc@petit-huguenin.org URI: hallway@jabber.ietf.org/MPH Petit-Huguenin Expires 29 September 2021 [Page 115]