idnits 2.17.1 draft-petithuguenin-computerate-specifying-04.txt: Checking boilerplate required by RFC 5378 and the IETF Trust (see https://trustee.ietf.org/license-info): ---------------------------------------------------------------------------- No issues found here. Checking nits according to https://www.ietf.org/id-info/1id-guidelines.txt: ---------------------------------------------------------------------------- No issues found here. Checking nits according to https://www.ietf.org/id-info/checklist : ---------------------------------------------------------------------------- ** The document seems to lack a Security Considerations section. ** The document seems to lack an IANA Considerations section. (See Section 2.2 of https://www.ietf.org/id-info/checklist for how to handle the case when there are no actions for IANA.) ** There is 1 instance of too long lines in the document, the longest one being 4 characters in excess of 72. == There are 14 instances of lines with non-RFC2606-compliant FQDNs in the document. == There are 2 instances of lines with non-RFC6890-compliant IPv4 addresses in the document. If these are example addresses, they should be changed. ** The document seems to lack a both a reference to RFC 2119 and the recommended RFC 2119 boilerplate, even if it appears to use RFC 2119 keywords. RFC 2119 keyword, line 984: '... SHOULD/SHOULD NOT/RECOMMENDED/NOT RECOMMENDED [RFC2119] keywords....' RFC 2119 keyword, line 986: '...although parsers SHOULD be tolerant an...' RFC 2119 keyword, line 1035: '... SHOULD keyword or its variants, wit...' Miscellaneous warnings: ---------------------------------------------------------------------------- == The copyright year in the IETF Trust and authors Copyright Line does not match the current year == Line 1916 has weird spacing: '...iven in the l...' -- The document date (September 12, 2020) is 1322 days in the past. Is this intentional? Checking references for intended status: Experimental ---------------------------------------------------------------------------- -- Missing reference section? 'Curry-Howard' on line 2551 looks like a reference -- Missing reference section? 'Zave11' on line 2675 looks like a reference -- Missing reference section? 'Knuth92' on line 2589 looks like a reference -- Missing reference section? 'AsciiDoc' on line 2530 looks like a reference -- Missing reference section? 'Idris2' on line 2586 looks like a reference -- Missing reference section? 'RFC7991' on line 2643 looks like a reference -- Missing reference section? 'I-D.ribose-asciirfc' on line 2579 looks like a reference -- Missing reference section? 'Metanorma-IETF' on line 2607 looks like a reference -- Missing reference section? 'Asciidoctor' on line 2532 looks like a reference -- Missing reference section? 'Metanorma' on line 2604 looks like a reference -- Missing reference section? 'Literate' on line 2600 looks like a reference -- Missing reference section? 'Blockquotes' on line 2535 looks like a reference -- Missing reference section? 'RFC8489' on line 2651 looks like a reference -- Missing reference section? 'Type-Driven' on line 2671 looks like a reference -- Missing reference section? 'RFC8656' on line 2656 looks like a reference -- Missing reference section? 'TLP5' on line 2668 looks like a reference -- Missing reference section? 'RFC0791' on line 2621 looks like a reference -- Missing reference section? 'Linear-Resources' on line 2596 looks like a reference -- Missing reference section? 'Stump16' on line 2662 looks like a reference -- Missing reference section? 'RFC2119' on line 2625 looks like a reference -- Missing reference section? 'TAOCP' on line 2665 looks like a reference -- Missing reference section? 'CPN' on line 2547 looks like a reference -- Missing reference section? 'Elab' on line 2556 looks like a reference -- Missing reference section? 'Momot16' on line 2611 looks like a reference -- Missing reference section? 'RFC5234' on line 2777 looks like a reference -- Missing reference section? 'I-D.mcquistin-augmented-ascii-diagrams' on line 2571 looks like a reference -- Missing reference section? 'I-D.bortzmeyer-language-state-machines' on line 2564 looks like a reference -- Missing reference section? 'RFC5246' on line 2634 looks like a reference -- Missing reference section? 'RFC8446' on line 2647 looks like a reference -- Missing reference section? 'Kroening16' on line 2592 looks like a reference -- Missing reference section? 'Brinkmann02' on line 2540 looks like a reference -- Missing reference section? 'AsciiBib' on line 2528 looks like a reference -- Missing reference section? 'RFC-Guide' on line 2881 looks like a reference -- Missing reference section? 'RFC761' on line 2639 looks like a reference -- Missing reference section? 'O' on line 3902 looks like a reference -- Missing reference section? 'I' on line 3902 looks like a reference Summary: 4 errors (**), 0 flaws (~~), 4 warnings (==), 37 comments (--). Run idnits with the --verbose option for more detailed information about the items above. -------------------------------------------------------------------------------- 2 Network Working Group M. Petit-Huguenin 3 Internet-Draft Impedance Mismatch LLC 4 Intended status: Experimental September 12, 2020 5 Expires: March 16, 2021 7 The Computerate Specifying Paradigm 8 draft-petithuguenin-computerate-specifying-04 10 Abstract 12 This document specifies a paradigm named Computerate Specifying, 13 designed to simultaneously document and formally specify 14 communication protocols. This paradigm can be applied to any 15 document produced by any Standard Developing Organization (SDO), but 16 this document targets specifically documents produced by the IETF. 18 Status of This Memo 20 This Internet-Draft is submitted in full conformance with the 21 provisions of BCP 78 and BCP 79. 23 Internet-Drafts are working documents of the Internet Engineering 24 Task Force (IETF). Note that other groups may also distribute 25 working documents as Internet-Drafts. The list of current Internet- 26 Drafts is at https://datatracker.ietf.org/drafts/current/. 28 Internet-Drafts are draft documents valid for a maximum of six months 29 and may be updated, replaced, or obsoleted by other documents at any 30 time. It is inappropriate to use Internet-Drafts as reference 31 material or to cite them other than as "work in progress." 33 This Internet-Draft will expire on March 16, 2021. 35 Copyright Notice 37 Copyright (c) 2020 IETF Trust and the persons identified as the 38 document authors. All rights reserved. 40 This document is subject to BCP 78 and the IETF Trust's Legal 41 Provisions Relating to IETF Documents (https://trustee.ietf.org/ 42 license-info) in effect on the date of publication of this document. 43 Please review these documents carefully, as they describe your rights 44 and restrictions with respect to this document. Code Components 45 extracted from this document must include Simplified BSD License text 46 as described in Section 4.e of the Trust Legal Provisions and are 47 provided without warranty as described in the Simplified BSD License. 49 Table of Contents 51 1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 4 52 2. Overview . . . . . . . . . . . . . . . . . . . . . . . . . . 5 53 3. Terminology . . . . . . . . . . . . . . . . . . . . . . . . . 5 54 4. Private Specifications . . . . . . . . . . . . . . . . . . . 6 55 4.1. Private Specifications for New Documents . . . . . . . . 9 56 4.2. Private Specifications for Existing Documents . . . . . . 10 57 5. Self-Contained Specifications . . . . . . . . . . . . . . . . 11 58 5.1. PDU Descriptions . . . . . . . . . . . . . . . . . . . . 11 59 5.1.1. PDU Examples . . . . . . . . . . . . . . . . . . . . 12 60 5.1.2. Calculations from PDU . . . . . . . . . . . . . . . . 15 61 5.1.3. PDU Representations . . . . . . . . . . . . . . . . . 16 62 5.2. State Machines . . . . . . . . . . . . . . . . . . . . . 17 63 5.3. Proofs . . . . . . . . . . . . . . . . . . . . . . . . . 18 64 5.3.1. Wire Type vs Abstract Type . . . . . . . . . . . . . 19 65 5.3.2. Data Format Conversion . . . . . . . . . . . . . . . 22 66 5.3.3. Postel's Law . . . . . . . . . . . . . . . . . . . . 22 67 5.3.4. Implementability . . . . . . . . . . . . . . . . . . 25 68 5.3.5. Termination . . . . . . . . . . . . . . . . . . . . . 26 69 5.3.6. Liveness . . . . . . . . . . . . . . . . . . . . . . 26 70 6. Importing Specifications . . . . . . . . . . . . . . . . . . 26 71 6.1. Common Modules . . . . . . . . . . . . . . . . . . . . . 28 72 6.1.1. Generating AsciiDoc . . . . . . . . . . . . . . . . . 28 73 6.1.2. Common Data Types . . . . . . . . . . . . . . . . . . 29 74 6.1.3. Calculations . . . . . . . . . . . . . . . . . . . . 33 75 6.1.4. Typed Petri Nets . . . . . . . . . . . . . . . . . . 34 76 6.1.5. Representations . . . . . . . . . . . . . . . . . . . 36 77 6.1.5.1. Bit Diagrams . . . . . . . . . . . . . . . . . . 37 78 6.1.5.2. Message Sequence Charts . . . . . . . . . . . . . 38 79 6.2. Packages for Meta-Languages . . . . . . . . . . . . . . . 38 80 6.2.1. Augmented BNF (ABNF) . . . . . . . . . . . . . . . . 41 81 6.2.2. Augmented Packet Header Diagrams (APHD) . . . . . . . 42 82 6.2.3. Cosmogol . . . . . . . . . . . . . . . . . . . . . . 44 83 6.3. Packages for Protocols . . . . . . . . . . . . . . . . . 44 84 6.3.1. Type Transformations . . . . . . . . . . . . . . . . 45 85 6.3.2. Extended Registries . . . . . . . . . . . . . . . . . 48 86 7. Exporting Specifications . . . . . . . . . . . . . . . . . . 50 87 7.1. Standard Library . . . . . . . . . . . . . . . . . . . . 50 88 7.2. Transclusions . . . . . . . . . . . . . . . . . . . . . . 52 89 7.3. Exporting Types and Functions . . . . . . . . . . . . . . 52 90 8. Standard Library . . . . . . . . . . . . . . . . . . . . . . 52 91 8.1. Internal Modules . . . . . . . . . . . . . . . . . . . . 52 92 8.1.1. AsciiDoc . . . . . . . . . . . . . . . . . . . . . . 53 93 8.1.2. BitVector . . . . . . . . . . . . . . . . . . . . . . 53 94 8.1.3. Unsigned . . . . . . . . . . . . . . . . . . . . . . 54 95 8.1.4. Dimension . . . . . . . . . . . . . . . . . . . . . . 54 96 8.1.5. BitDiagram . . . . . . . . . . . . . . . . . . . . . 55 97 8.1.6. Transform . . . . . . . . . . . . . . . . . . . . . . 55 98 8.1.7. Tpn . . . . . . . . . . . . . . . . . . . . . . . . . 56 99 8.2. Meta-Language Packages . . . . . . . . . . . . . . . . . 56 100 8.2.1. Augmented Packet Header Diagrams (APHD) . . . . . . . 56 101 8.2.2. RFC 5234 (ABNF) . . . . . . . . . . . . . . . . . . . 56 102 8.3. Protocol Packages . . . . . . . . . . . . . . . . . . . . 56 103 8.3.1. RFC 791 (Internet Protocol) . . . . . . . . . . . . . 56 104 9. Bibliography . . . . . . . . . . . . . . . . . . . . . . . . 56 105 Appendix A. Command Line Tools . . . . . . . . . . . . . . . . . 60 106 A.1. Installation . . . . . . . . . . . . . . . . . . . . . . 60 107 A.1.1. Download the Docker Image . . . . . . . . . . . . . . 60 108 A.2. The "computerate" Command . . . . . . . . . . . . . . . . 61 109 A.2.1. Literate Files . . . . . . . . . . . . . . . . . . . 61 110 A.2.2. Transclusions . . . . . . . . . . . . . . . . . . . . 61 111 A.2.3. IdrisDoc Generation . . . . . . . . . . . . . . . . . 62 112 A.2.4. Outputs . . . . . . . . . . . . . . . . . . . . . . . 62 113 A.2.5. Extended Registry . . . . . . . . . . . . . . . . . . 63 114 A.2.6. Bibliography . . . . . . . . . . . . . . . . . . . . 63 115 A.2.6.1. Internet-Draft . . . . . . . . . . . . . . . . . 64 116 A.2.6.2. RFC . . . . . . . . . . . . . . . . . . . . . . . 64 117 A.2.6.3. Email . . . . . . . . . . . . . . . . . . . . . . 65 118 A.2.6.4. IANA . . . . . . . . . . . . . . . . . . . . . . 66 119 A.2.6.5. Web-Based Public Code Repositories . . . . . . . 66 120 A.3. Idris REPL . . . . . . . . . . . . . . . . . . . . . . . 66 121 A.4. Other Commands . . . . . . . . . . . . . . . . . . . . . 67 122 A.5. Source Repositories . . . . . . . . . . . . . . . . . . . 67 123 A.6. Modified Tools . . . . . . . . . . . . . . . . . . . . . 68 124 A.6.1. Idris2 . . . . . . . . . . . . . . . . . . . . . . . 68 125 A.6.2. xml2rfc . . . . . . . . . . . . . . . . . . . . . . . 69 126 A.6.3. asciidoctor . . . . . . . . . . . . . . . . . . . . . 69 127 A.6.4. metanorma . . . . . . . . . . . . . . . . . . . . . . 69 128 A.6.5. metanorma-ietf . . . . . . . . . . . . . . . . . . . 69 129 A.6.6. relaton-bib . . . . . . . . . . . . . . . . . . . . . 69 130 A.6.7. git . . . . . . . . . . . . . . . . . . . . . . . . . 70 131 A.6.8. idris2-vim . . . . . . . . . . . . . . . . . . . . . 70 132 A.7. Bugs and Workarounds . . . . . . . . . . . . . . . . . . 70 133 A.8. TODO List . . . . . . . . . . . . . . . . . . . . . . . . 71 134 Appendix B. Reference . . . . . . . . . . . . . . . . . . . . . 72 135 B.1. Package computerate-specifying . . . . . . . . . . . . . 72 136 B.1.1. Module ComputerateSpecifying.AsciiDoc . . . . . . . . 72 137 B.1.2. Module ComputerateSpecifying.BitDiagram . . . . . . . 74 138 B.1.3. Module ComputerateSpecifying.BitVector . . . . . . . 74 139 B.1.4. Module ComputerateSpecifying.Dimension . . . . . . . 75 140 B.1.5. Module ComputerateSpecifying.Tpn . . . . . . . . . . 77 141 B.1.6. Module ComputerateSpecifying.Transform . . . . . . . 79 142 B.1.7. Module ComputerateSpecifying.Unsigned . . . . . . . . 80 143 B.2. Package rfc5234 . . . . . . . . . . . . . . . . . . . . . 80 144 B.2.1. Module RFC5234.Core . . . . . . . . . . . . . . . . . 80 145 B.2.2. Module RFC5234.Main . . . . . . . . . . . . . . . . . 81 146 B.3. Package augmented-ascii-diagrams . . . . . . . . . . . . 82 147 B.3.1. Module AAD.Main . . . . . . . . . . . . . . . . . . . 82 148 B.4. Package rfc791 . . . . . . . . . . . . . . . . . . . . . 83 149 B.4.1. Module RFC791.Address . . . . . . . . . . . . . . . . 84 150 B.4.2. Module RFC791.IP . . . . . . . . . . . . . . . . . . 84 151 Appendix C. Errata Statistics . . . . . . . . . . . . . . . . . 85 152 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . 87 153 Contributors . . . . . . . . . . . . . . . . . . . . . . . . . . 88 154 Changelog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 155 Author's Address . . . . . . . . . . . . . . . . . . . . . . . . 90 157 1. Introduction 159 If, as the unofficial IETF motto states, we believe that "running 160 code" is an important part of the feedback provided to the 161 standardization process, then as per the Curry-Howard equivalence 162 [Curry-Howard] (that states that code and mathematical proofs are the 163 same), we ought to also believe that "verified proof" is an equally 164 important part of that feedback. A verified proof is a mathematical 165 proof of a logical proposition that was mechanically verified by a 166 computer, as opposed to just peer-reviewed. 168 The "Experiences with Protocol Description" paper from Pamela Zave 169 [Zave11] gives three conclusions about the usage of formal 170 specifications for a protocol standard. The first conclusion states 171 that informal methods (i.e. the absence of verified proofs) are 172 inadequate for widely used protocols. This document is based on the 173 assumption that this conclusion is correct, so its validity will not 174 be discussed further. 176 The second conclusion states that formal specifications are useful 177 even if they fall short of the "gold standard" of a complete formal 178 specification. We will show that a formal specification can be 179 incrementally added to a document. 181 The third conclusion from Zave's paper states that the normative 182 English language should be paraphrasing the formal specification. 183 The difficulty here is that to be able to keep the formal 184 specification and the normative language synchronized at all times, 185 these two should be kept as physically close as possible to each 186 other. 188 To do that we introduce the concept of "Computerate Specifying" (note 189 that Computerate is a British English word). "Computerate 190 Specifying" is a play on "Literate Computing", itself a play on 191 "Structured Computing" (see [Knuth92] page 99). In the same way that 192 Literate Programming enriches code by interspersing it with its own 193 documentation, Computerate Specifying enriches a standard 194 specification by interspersing it with code (or with proofs, as they 195 are the same thing), making it a computerate specification. 197 Note that computerate specifying is not specific to the IETF, just 198 like literate computing is not restricted to the combination of Tex 199 and Pascal described in Knuth's paper. What this document describes 200 is a specific instance of computerate specifying that combines 201 [AsciiDoc] as formatting language and [Idris2] as programming 202 language with the goal of formally specifying IETF protocols. 204 2. Overview 206 The remaining of this document is divided in 3 parts: 208 After the Terminology (Section 3) section starts a tutorial on how to 209 write a specification. This tutorial is meant to be read in 210 sequence, as concepts defined in early part will not be repeated 211 later. On the other hand the tutorial is designed to present 212 information progressively and mostly in order of complexity, so it is 213 possible to start writing effective specifications without reading or 214 understanding the whole tutorial. 216 The tutorial begins by explaining how to write private specifications 217 (Section 4), which are specifications that are not meant to be 218 shared. Then the tutorial continues by explaining how to write an 219 self-contained specification (Section 5), which is a specification 220 that contains Idris code that relies only on the Idris Standard 221 Library. Writing self-contained specifications is difficult and 222 time-consuming, so the tutorial continues by explained how to import 223 specifications (Section 6) that contain reusable types and code. The 224 tutorial ends with explanations on how to design a exportable 225 specification (Section 7). 227 After the tutorial come the description of all the packages and 228 modules in the Computerate Specifying Standard Library (Section 8). 230 Appendix A explains how to install and use the associated tooling, 231 and Appendix B contains the reference manual for the standard 232 library. 234 3. Terminology 236 Computerate Specification, Specification: Literate Idris2 code 237 embedded in an AsciiDoc document, containing both formal 238 descriptions and human language texts, and which can be processed 239 to produce documents in human language. 241 Document: Any text that contains the documentation of a protocol in 242 the English language. A document is the result of processing a 243 specification. 245 Retrofitted Specification: A specification created after a document 246 was published such as the generated document coincides with the 247 published document. 249 In this document, the same word can be used either as an English word 250 or as an Idris identifier used inside the text. To explicitly 251 differentiate them, the latter is always displayed like "this". E.g. 252 "IdrisDoc" is meant to convey the fact that IdrisDoc in that case is 253 an Idris module or type. On the other hand the word IdrisDoc refers 254 to the IdrisDoc specification. 256 Similarly blocks of code, including literate code, are always 257 sandwiched between "" and "". Code blocks 258 will be presented in their literate form only when necessary, i.e. 259 when mixed AsciiDoc and Idris are required. However, in a 260 computerate specification, Idris code must in fact be used in its 261 literate form. 263 By convention an Idris function that returns a type and types 264 themselves will always start with an uppercase letter. Functions not 265 returning a type start with a lowercase letter. 267 For the standard library, the types names are also formed by taking 268 the English word or expression, making the first letter of each word 269 upper case, and removing any symbols like underscore, dash and space. 270 Thus bitvector would become "Bitvector" after conversion as a type 271 name but bit diagram would become "BitDiagram". 273 4. Private Specifications 275 Nowadays documents at the IETF are written in a format named xml2rfc 276 v3 [RFC7991] but unfortunately making that format Computerable is not 277 trivial, mostly because there is no simple solution to mix code and 278 XML together in the same file. Instead, the [AsciiDoc] format forms 279 the basis for specifications as it permits the generation of 280 documents in the xmlrfc v3 format (among other formats) and also 281 because it can be enriched with code in the same file. 283 AsciiRFC [I-D.ribose-asciirfc] and [Metanorma-IETF] describe a 284 backend for the [Asciidoctor] tool that converts an AsciiDoc document 285 into an xml2rfc v3 document. The AsciiRFC document states various 286 reasons why AsciiDoc is a superior format for the purpose of writing 287 standards, so that will not be discussed further. Note that the same 288 team developed Asciidoctor backends [Metanorma] for other Standards 289 Developing Organizations (SDO), making it easy to develop computerate 290 specifications targeting the documents developed by these SDOs. 292 The code in a computerate specification uses the programming language 293 [Idris2] in literate programming [Literate] mode using the Bird- 294 style, by having each line of code starting with a ">" mark in the 295 first column. 297 That same symbol is also used by AsciiDoc as an alternate way of 298 defining a blockquote [Blockquotes] way which is no longer available 299 in a computerate specification. Bird-style code will simply not 300 appear in the rendered document. 302 The result of Idris code execution can be inserted inside the 303 AsciiDoc part of a specification by inserting that code fragment 304 between the "{`" string and the "`}" strings. That code fragment 305 must return a value that implements the "Show" interface. 307 A computerate specification is processed by an Asciidoctor 308 preprocessor that does the following: 310 1. Loads the whole specification as an Idris program, including 311 importing modules. 313 2. For each instance of an inline code fragment, evaluates that 314 fragment and replaces it (including the delimiters) by the result 315 of that evaluation. 317 3. Continues with the normal processing of the modified 318 specification. 320 For instance the following document fragment taken from the 321 computerate specification of [RFC8489]: 323 324 > rto : Int 325 > rto = 500 326 > 327 > rc : Nat 328 > rc = 7 329 > 330 > rm : Int 331 > rm = 16 332 > 333 > -- A stream of transmission times 334 > transmissions : Int -> Int -> Stream Int 335 > transmissions value rto = value :: transmissions (value + rto) 336 > (rto * 2) 337 > 338 > -- A specific transmission time 339 > transmission : Int -> Nat -> Int 340 > transmission timeout i = index i $ transmissions 0 timeout 341 > 342 > a1 : Int 343 > a1 = rto 344 > 345 > a2 : String 346 > a2 = concat (take (rc - 1) (map (\t => show t ++ " ms, ") 347 > (transmissions 0 rto))) ++ "and " ++ show (transmission rto 348 > (rc - 1)) ++ " ms" 349 > 350 > a3 : Int 351 > a3 = transmission rto (rc - 1) + rto * rm 353 For example, assuming an RTO of {`a1`}ms, requests would be sent at 354 times {`a2`}. 355 If the client has not received a response after {`a3`} ms, the 356 client will consider the transaction to have timed out. 357 359 Figure 1 361 is rendered as 363 " For example, assuming an 364 RTO of 500ms, requests would be sent at times 0 ms, 500 ms, 1500 ms, 365 3500 ms, 7500 ms, 15500 ms, and 31500 ms. If the client has not 366 received a response after 39500 ms, the client will consider the 367 transaction to have timed out." 369 Figure 2 371 The Idris2 programming language has been chosen because its type 372 system supports dependent and linear types [Type-Driven], and that 373 type system is the language in which propositions are written. The 374 Idris2 programming also has reflection capabilities and support for 375 meta-programming, also known as elaboration. 377 Following Zave's second conclusion, computerate specifying is not 378 restricted to the specification of protocols, or to property proving. 379 There is a whole spectrum of formalism that can be introduced in a 380 specification, and we will present it in the remaining sections by 381 increasing order of complexity. Note that because the specification 382 language is a programming language, these usages are not exhaustive, 383 and plenty of other usages can and will be found after the 384 publication of this document. 386 At the difference of an RFC which is immutable after publication, the 387 types and code in a specification will be improved over time, 388 especially as new properties are proved or disproved. The latter 389 will happen when a bug is discovered in a specification and a proof 390 of negation is added to the specification, paving the way to a 391 revision of the standard. 393 A private specification is a specification that is not meant to be 394 shared. There is mostly two reasons for a specification to be kept 395 private, as explained in the next sections. 397 4.1. Private Specifications for New Documents 399 In the simplest case, writing a specification with the goal of 400 publishing the resulting document does not require sharing that 401 specification. This is quite similar to what was done with xml2rfc 402 before the IETF adopted RFC 7991 as the canonical format for 403 Internet-Drafts and RFCs; most people used xml2rfc to prepare their 404 document, but did not share the xml2rfc file beyond the co-authors of 405 the document. 407 In that case writing a specification is straightforward: write the 408 specification from scratch using AsciiDoc for the text and Idris for 409 the formal parts. 411 One effective rule to quickly discover that the Idris code and the 412 AsciiDoc document are diverging is to keep both of them as close as 413 possible to each other. This is most effectively done by having the 414 matching Idris code right after each AsciiDoc paragraph, such as it 415 is then easy to compare each to the other. 417 Idris itself imposes an order in which types and code must be 418 declared and defined, because it does not by default look for forward 419 references. Because, by the rule above, the text will follow the 420 order the Idris code is organized, the document generated by such 421 specification tends to be naturally easier to implement, because it 422 induces the same workflow than a software implementer will follow 423 when implementing the document. 425 [RFC8489] and [RFC8656] are examples of standards that are easy to 426 implement because are written in the order that a software developer 427 will develop each component. 429 4.2. Private Specifications for Existing Documents 431 A second reason to write a private specification is for the purpose 432 of doing a review of an existing document, most likely of an 433 Internet-Draft during the standardization process. 435 This is done by first turning the existing document into a 436 specification by converting it into an AsciiDoc document, which can 437 be done manually relatively easily. After this step, the 438 specification can be enriched by adding some Idris code and replacing 439 some of the text with the execution of Idris code fragments. 440 Comparing the original document with a document generated by 441 processing the specification permits to validate that the original 442 document is correct regarding the formalism introduced. 444 Documents that are not generated from a specification do not always 445 have a structure that follow the way a software developer will 446 implement it. When that is the case it will be difficult to add the 447 Idris code right after a paragraph describing its functionality, 448 because the final code may not type-check because of the lack of 449 support for forward references. It could be a signal that the text 450 needs to be reorganized to be more software-development friendly. 452 One alternative is to use a technique named self-inclusion, which is 453 the possibility to change the order of paragraphs in an AsciiDoc 454 document and thus keeping the Idris code in an order that type- 455 checks. 457 This is done by using tags to delimit the text that needs to be 458 moved: 460 461 // tag::para1[] 462 Text that describes a functionality 464 > -- Code that implements that functionality. 465 // end::para1[] 466 468 Figure 3 470 Then a self-include can move (instead of duplicating) the text inside 471 the tags to a different place, without changing the order of the 472 Idris code: 474 475 include::Main.adoc[tag=para1] 476 478 Figure 4 480 Note that the IETF Trust licences [TLP5] do not grant permission to 481 distribute an annotated Internet-Draft as a whole so redistributing 482 such specification would be a copyright license infringement. But as 483 in this case the specification is not meant to be distributed, there 484 is no infringement possible. 486 5. Self-Contained Specifications 488 A self-contained specification is a specification where the Idris 489 code does not use anything but the types and functions defined in its 490 standard library, thus not requiring to install anything but Idris2 491 itself. 493 A specification uses Idris types to specify both how stream of bits 494 are arranged to form valid Protocol Data Units (PDU) and how the 495 exchange of PDUs between network elements is structured to form a 496 valid protocol. In addition a specification can be used to prove or 497 disprove a variety of properties for these types. 499 5.1. PDU Descriptions 501 The PDUs in a communication protocol determines how data is laid out 502 before it is sent over a communication link. Generally a PDU is 503 described only in the context of the layer that this particular 504 protocol is operating at, e.g. an application protocol PDU only 505 describes the data as sent over UDP or TCP, not over Ethernet or Wi- 506 Fi. 508 PDUs can generally be split into two broad categories, binary and 509 text, and a protocol PDU mostly falls into one of these two 510 categories. 512 PDU descriptions can be defined as specifications for at least three 513 reasons: the generation of examples that are correct by construction, 514 correctness in displaying the result of calculations, and correctness 515 in representing the structure of a PDU. 517 5.1.1. PDU Examples 519 Examples in protocol documents are frequently incorrect, which proves 520 to have a significant negative impact as they are too often misused 521 as normative text. See Appendix C for statistics about the frequency 522 of incorrect examples in RFC errata. 524 Ensuring example correctness is achieved by adding the result of a 525 computation (the example) directly inside the document. If that 526 computation is done from a type that is (physically and conceptually) 527 close to the normative text, then we gain some level of assurance 528 that both the normative text and the derived examples will match. 530 Generating an example that is correct by construction always starts 531 by defining a type that describes the format of the data to display. 532 The Internet Header Format in section 3.1 of [RFC0791] will be used 533 in the following sections as example. 535 In this section we start by defining an Idris type, using a 536 Generalized Algebraic Data Type (GADT). In that case we have only 537 one constructor ("MkInternetHeader") which is defined as a Product 538 Type that "concatenate" all the fields on the Internet Header. One 539 specific aspect of Idris types is that we can enrich the definition 540 of each field with constraints that then have to be fulfilled when a 541 value of that type will be built. 543 544 data InternetHeader : Type where 545 MkInternetHeader : 546 (version : Int) -> version = 4 => 547 (ihl : Int) -> ihl >= 5 && ihl < 16 = True => 548 (tos : Int) -> tos >= 0 && tos <= 256 = True => 549 (length : Int) -> length >= (5 * 4) && length < 65536 = True => 550 (id : Int) -> id >= 0 && id < 65536 = True => 551 (flags : Int) -> flags >= 0 && flags < 16 = True => 552 (offset : Int) -> offset >= 0 && offset < 8192 = True => 553 (ttl : Int) -> ttl >= 0 && ttl < 256 = True => 554 (protocol : Int) -> protocol >= 0 && protocol < 256 = True => 555 InternetHeader 556 558 Figure 5 560 where 562 version: This field is constrained to always contain the value 4. 564 ihl: Int is a builtin signed integer so it is constrained to contain 565 only positive integers lower than 16. 567 others: Same, all the fields are constrained to unsigned integers 568 fitting inside the number of bits defined in [RFC0791]. 570 An Idris type where the fields in a constructor are organized like 571 the "InternetHeader" by ordering them in a sequence is called a Pi 572 type - or, when there is no dependencies between fields as there is 573 in "version = 4", a Product type. Although there is no equivalence 574 in most programming languages to a Pi type, Product types are known 575 as classes in Java and struct in C. 577 Another way to organize a type is called the Sum type, which is a 578 type with multiple constructors that act as alternative. Sum types 579 can be used in C with a combination of struct and union, and since 580 Java 14 by using sealed records. 582 Sum types have a dependent counterpart named a Sigma type, which is a 583 tuple in which the type of the second element depends on the value of 584 the first element. This is mostly returned by functions, with the 585 returned Sigma type carrying both a value and a proof of the validity 586 of that value. 588 From that point it is possible to define a value that fulfills all 589 the constraints. The following values are taken from example 1 in 590 [RFC0791] Appendix A. 592 593 example1 : InternetHeader 594 example1 = MkInternetHeader 4 5 0 21 111 0 0 123 1 595 597 Figure 6 599 The "=>" symbol after a constraint indicates that Idris should try to 600 automatically find a proof that this constraint is met by the values 601 in the example, which it successfully does in the example above. 603 The following example, where the constraints defined in the 604 InternetHeader type are not met, will not type-check in Idris (an 605 error message will be generated) and thus can not be used to generate 606 an example. 608 609 example1' : InternetHeader 610 example1' = MkInternetHeader 6 5 0 21 111 0 0 123 1 611 613 Figure 7 615 The next step is to define an Idris function that converts a value of 616 the type "InternetHeader" into the kind of bit diagram that is showed 617 in Appendix A of [RFC0791]. 619 620 Show InternetHeader where 621 show (MkInternetHeader version ihl tos length id flags offset 622 ttl protocol) = ?showPrec_rhs_1 623 625 Figure 8 627 Here we implement the "Show" interface that permits to define the 628 adhoc polymorphic function "show" for "InternetHeader", function that 629 will convert the value into the right character string. Idris names 630 starting with a question mark like in "?showPrec_rhs_1" are so-called 631 holes, which are placeholder for code to be written, while still 632 permitting type-checking. 634 After replacing the hole by the actual code, the following embedded 635 code can be used in the document to generate an example that is 636 correct by construction, at least up to mistakes in the specification 637 (i.e. the constraints in "InternetHeader") and bugs in the "show" 638 function. 640 641 .... 642 {`example1`} 643 .... 644 646 Figure 9 648 will generate the equivalent AsciiDoc text: 650 651 .... 652 0 1 2 3 653 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 654 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 655 |Ver= 4 |IHL= 5 |Type of Service| Total Length = 21 | 656 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 657 | Identification = 111 |Flg=0| Fragment Offset = 0 | 658 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 659 | Time = 123 | Protocol = 1 | 660 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 661 .... 662 664 Figure 10 666 This generated example is similar to the first of the examples in 667 appendix A of RFC 791. 669 5.1.2. Calculations from PDU 671 The previous section showed how to define a type that precisely 672 describes a PDU, how to generates examples that are are values of 673 that type, and how to insert them in a document. 675 Our specification, which has the form of an Idris type, can be seen 676 as a generalization of all the possible examples for that type. Now 677 that we went through the effort of precisely defining that type, it 678 would be useful to use it to also calculate statements about that 679 syntax. 681 In RFC 791 the description of the field IHL states "[...]that the 682 minimum value for a correct header is 5." The origin of this number 683 may be a little mysterious, so it is better to use a formula to 684 calculate it and insert the result instead. 686 Inserting a calculation is easy: 688 689 Note that the minimum value for a correct header is 690 is \{`sizeHeader `div` ihlUnit`}. 692 > sizeHeader : Int 693 > sizeHeader = 20 695 > ihlUnit : Int 696 > ihlUnit = 4 697 699 Figure 11 701 Here we can insert a code fragment that is using a function that is 702 defined later in the document because the Idris code is evaluated 703 before the document is processed. 705 Note the difference with examples: The number "5" is not an example 706 of value of the type "InternetHeader", but a property of that type. 708 Systematically using the result of calculation on types in a 709 specification makes it more resistant to mistakes that are introduced 710 as result of modifications. 712 5.1.3. PDU Representations 714 The layout of a PDU, i.e. the size and order of the fields that 715 compose it can be represented in a document in various forms. One of 716 them is just an enumeration of these fields in order, each field 717 identified by a name and accompanied by some description of that 718 field in the form of the number of bits it occupies in the PDU and 719 how to interpret these bits. 721 That layout can also be presented as text, as a list, as a table, as 722 a bit diagram, at the convenience of the document author. In all 723 cases, some parts of the description of each field can be extracted 724 from our Idris type just like we did in Section 5.1.2. 726 RFC 791 section 3.1 represents the PDUs defined in it both as bit 727 diagrams and as lists of fields. 729 5.2. State Machines 731 A network protocol, which is how the various PDUs defined in a 732 document are exchanged between network elements, can always be 733 understood as a set of state machines. At the difference of PDUs, 734 that are generally described in a way that is close to their Idris 735 counterpart, state machines in a document are generally only 736 described as text. 738 Note that, just like an Idris representation of a PDU should also 739 contain all the possible constraints on that PDU but not more, a 740 state machine should contain all the possible constraints in the 741 exchange of PDUs, but not less. 743 This issue is most visible in one of the two state machines defined 744 in RFC 791, the one for fragmenting IP packets (the other is for 745 unfragmenting packets). The text describes two different algorithms 746 to fragment a packet but in that case each algorithm should be 747 understood as one instance of a more general state machine. That 748 state machine describes all the possible sequences of fragments that 749 can be generated by an algorithm that is compliant with RFC 791 and 750 it would be an Idris type that is equivalent to the following 751 algorithm: 753 * For a specific packet size, generate a list of all the binary 754 values between 0 and the packet size divided by 8 and rounded-up. 756 * For each binary value in that list, generate a list of values that 757 represents the number of consecutive bits of the same value (e.g.. 758 "0x110001011" generates a "[2, 3, 1, 1, 2]" list). 760 * Remove from that list of lists any list that contains a number 761 that, after multiplication by 8, is higher than the maximum size 762 of a fragment. 764 * For each remaining list in that list, generate the list of 765 fragments, i.e with the correct offset, length and More bit. 767 * Generate all the possible permutations for each list of fragments. 769 We can see that this state machine takes in account the fact that an 770 IP packet can not only be fragmented in fragments of various sizes - 771 as long as the constraints are respected - but also that these 772 fragments can be sent in any order. 774 Then the algorithms described in the document can be seen as 775 generating a subset of all the possible list of fragments that can be 776 generated by our state machine. It is then easy to check that these 777 algorithms cannot generate fragments lists that cannot be generated 778 by our state machine. 780 As a consequence, the unfragment state machine must be able to 781 regenerate a valid unfragmented packet for any of the fragments list 782 generated by our fragment state machine. Furthermore, the unfragment 783 state machine must also take in account fragment lists that are 784 modified by the network (itself defined as a state machine) in the 785 following ways: 787 * fragments can be dropped; 789 * the fragments order can change (this is already covered by the 790 fact that our fragment state machine generates all possible 791 orders); 793 * fragments can be duplicated multiple times; 795 * fragments can be delayed; 797 * fragments can be received that were never sent by the fragment 798 state machine. 800 Then the algorithm described in the document can be compared with the 801 unfragment state machine to verify that all states and transitions 802 are covered. 804 Defining a state machine in Idris can be done in an ad-hoc way 805 [Linear-Resources], particularly by using linear types that express 806 resources' consumption. 808 5.3. Proofs 810 Under the Curry-Howard equivalence, the Idris types that we created 811 to describe PDUs and state machine are formal logic propositions, and 812 be able to construct values from these types (like we did for the 813 examples), is proof that these propositions are true. These are also 814 called internal verifications [Stump16]. 816 External verifications are made of additional propositions (as Idris 817 types) and proofs (as code for these types) with the goal of 818 verifying additional properties. 820 One kind of proofs that one would want in a specification are related 821 to isomorphism, i.e. a guarantee that two or more descriptions of a 822 PDU or a state machine contain exactly the same information, but 823 there is others. 825 5.3.1. Wire Type vs Abstract Type 827 The Idris types that are used for generating examples, calculations 828 or representations are generally very close to the bit structure of 829 the PDU. But some properties may be better expressed by defining 830 more abstract types. We call the former Wire Types, and the latter 831 Abstract Types. 833 As example, the type in Section 5.1.1 is a wire type, because it 834 follows exactly the PDU layout. But fragmentation can be more easily 835 described using the following abstract type: 837 838 data InternetHeader' : Type where 839 Full : (ihl : Int) -> ihl >= 5 && ihl < 16 = True => 840 (tos : Int) -> tos >= 0 && tos <= 256 = True => 841 (length : Int) -> length >= (5 * 4) && 842 length < 65536 = True => 843 (ttl : Int) -> ttl >= 0 && ttl < 256 = True => 844 (protocol : Int) -> protocol >= 0 && 845 protocol < 256 = True => 846 InternetHeader' 847 First : (ihl : Int) -> ihl >= 5 && ihl < 16 = True => 848 (tos : Int) -> tos >= 0 && tos <= 256 = True => 849 (length : Int) -> length >= (5 * 4) && 850 length < 65536 = True => 851 (id : Int) -> id >= 0 && id < 65536 = True => 852 (ttl : Int) -> ttl >= 0 && ttl < 256 = True => 853 (protocol : Int) -> protocol >= 0 && 854 protocol < 256 = True => 855 InternetHeader' 856 Next : (ihl : Int) -> ihl >= 5 && ihl < 16 = True => 857 (tos : Int) -> tos >= 0 && tos <= 256 = True => 858 (length : Int) -> length >= (5 * 4) && 859 length < 65536 = True => 860 (offset : Int) -> length > 0 && 861 length < 8192 = True => 862 (id : Int) -> id >= 0 && id < 65536 = True => 863 (ttl : Int) -> ttl >= 0 && ttl < 256 = True => 864 (protocol : Int) -> protocol >= 0 && 865 protocol < 256 = True => 866 InternetHeader' 867 Last : (ihl : Int) -> ihl >= 5 && ihl < 16 = True => 868 (tos : Int) -> tos >= 0 && tos <= 256 = True => 869 (length : Int) -> length >= (5 * 4) && 870 length < 65536 = True => 871 (offset : Int) -> length > 0 && 872 length < 8192 = True => 873 (id : Int) -> id >= 0 && id < 65536 = True => 874 (ttl : Int) -> ttl >= 0 && ttl < 256 = True => 875 (protocol : Int) -> protocol >= 0 && 876 protocol < 256 = True => 877 InternetHeader' 878 880 Figure 12 882 First the "version" field is eliminated, because it always contains 883 the same constant. 885 Then the "flags" and "offset" fields are reorganized so to provide 886 four different alternate packets: 888 * The "Full" constructor represents an unfragmented packet. It is 889 isomorphic to a "MkInternetHeader" with a "flags" and "offset" 890 values of 0. 892 * The 'First' constructor represents the first fragment of a packet. 893 It is isomorphic to a "MkInternetHeader" with a "flags" value of 1 894 and "offset" value of 0. 896 * The 'Next' constructor represents a intermediate fragments of a 897 packet. It is isomorphic to a "MkInternetHeader" with a "flags" 898 value of 1 and "offset" value different than 0. 900 * Finally the 'Last' constructor represents the last fragment of a 901 packet. It is isomorphic to a "MkInternetHeader" with a "flags" 902 value of 0 and "offset" value different than 0. 904 One of the main issue of having two types for the same data is 905 ensuring that they both contains the same information, i.e. that they 906 are isomorphic. To ensure that these two types are carrying the same 907 information we need to define and implement four functions that, all 908 together, prove that the types are isomorphic. This is done by 909 defining the 4 types below, as propositions to be proven: 911 912 total 913 to : InternetHeader -> InternetHeader' 915 total 916 from : InternetHeader' -> InternetHeader 918 total 919 toFrom : (x : InternetHeader') -> to (from x) = x 921 total 922 fromTo : (x : InternetHeader) -> from (to x) = x 923 925 Figure 13 927 Successfully implementing these functions will prove that the two 928 types are isomorphic. Note the usage of the "total" keyword to 929 ensure that these are proofs and not mere programs. 931 5.3.2. Data Format Conversion 933 For documents that describe a conversion between different data 934 layouts, having a proof that guarantees that no information is lost 935 in the process can be beneficial. For instance, we observe that 936 syntax encoding tends to be replaced each ten years or so by 937 something "better". Here again isomorphism can tell us exactly what 938 kind of information we lost and gained during that replacement. 940 Here, for example, the definition of a function that would verify an 941 isomorphism between an XML format and a JSON format: 943 944 isXmlAndJsonSame: Iso (XML, DeltaXML) (JSON, DeltaJson) 945 ... 946 948 Figure 14 950 DeltaXML expresses what is gained by switching from XML to JSON, and 951 DeltaJson expresses what is lost. 953 5.3.3. Postel's Law 955 | Be conservative in what you do, be liberal in what you accept from 956 | others. 957 | 958 | -- Jon Postel - RFC 761 960 One of the downsides of having specifications is that there is no 961 wiggle room possible when implementing them. An implementation 962 either conforms to the specification or does not. 964 One analogy would be specifying a pair of gears. If one decides to 965 have both of them made with tolerances that are too small, then it is 966 very likely that they will not be able to move when put together. A 967 bit of slack is needed to get the gear smoothly working together but 968 more importantly the cost of making these gears is directly 969 proportional to their tolerance. There is an inflexion point where 970 the cost of an high precision gear outweighs its purpose. 972 We have a similar issue when implementing a specification, where 973 having an absolutely conform implementation may cost more money than 974 it is worth spending. On the other hand a specification exists for 975 the purpose of interoperability, so we need some guidelines on what 976 to ignore in a specification to make it cost effective. 978 Postel's law proposes an informal way of defining that wiggle room by 979 actually having two different specifications, one that defines a data 980 layout for the purpose of sending it, and another one that defines a 981 data layout for the purpose of receiving that data layout. 983 Existing documents express that dichotomy in the form of the usage of 984 SHOULD/SHOULD NOT/RECOMMENDED/NOT RECOMMENDED [RFC2119] keywords. 985 For example the SDP spec says that "[t]he sequence CRLF (0x0d0a) is 986 used to end a line, although parsers SHOULD be tolerant and also 987 accept lines terminated with a single newline character." This 988 directly infers two specifications, one used to define an SDP when 989 sending it, that enforces using only CRLF, and a second 990 specification, used to define an SDP when receiving it (or parsing 991 it), that accepts both CRLF and LF. 993 Note that the converse is not necessarily true, i.e. not all usages 994 of these keywords are related to Postel's Law. 996 To ensure that the differences between the sending specification and 997 the receiving specification do not create interoperability problems, 998 we can use a variant of isomorphism, as shown in the following 999 example (data constructors and code elided): 1001 1002 data Sending : Type where 1004 data Receiving : Type where 1006 to : Sending -> List Receiving 1008 from : Receiving -> Sending 1010 toFrom : (y : Receiving) -> Elem y (to (from y)) 1012 fromTo : (y : Sending) -> True = all (== y) [from x | x <- to y] 1013 1015 Figure 15 1017 Here we define two data types, one that describes the data layout 1018 that is permitted to be sent ("Sending") and one that describes the 1019 data layout that is permitted to be received ("Receiving"). For each 1020 data layout that is possible to send, there is one or more matching 1021 receiving data layouts. This is expressed by the function "to" that 1022 takes as input one Sending value and returns a list of Receiving 1023 values. 1025 Conversely, the "from" function maps a Receiving data layout onto a 1026 Sending data layout. Note the asymmetry there, which prevents using 1027 a standard proof of isomorphism. 1029 Then the "toFrom" and "fromTo" proofs verify that there is no 1030 interoperability issue by guaranteeing that each Receiving value maps 1031 to one and only one Sending instance and that this mapping is 1032 isomorphic. 1034 All of this will provide a clear guidance of when and where to use a 1035 SHOULD keyword or its variants, without loss of interoperability. 1037 As an trivial example, the following proves that accepting LF 1038 characters in addition to CRLF characters as end of line markers does 1039 not break interoperability: 1041 1042 data Sending : Type where 1043 S_CRLF : Sending 1045 Eq Sending where 1046 (==) S_CRLF S_CRLF = True 1048 data Receiving : Type where 1049 R_CRLF : Receiving 1050 R_LF : Receiving 1052 to : Sending -> List Receiving 1053 to S_CRLF = [R_CRLF, R_LF] 1055 from : Receiving -> Sending 1056 from R_CRLF = S_CRLF 1057 from R_LF = S_CRLF 1059 toFrom : (y : Receiving) -> Elem y (to (from y)) 1060 toFrom R_CRLF = Here 1061 toFrom R_LF = There Here 1063 fromTo : (y : Sending) -> True = all (== y) [from x | x <- to y] 1064 fromTo S_CRLF = Refl 1065 1067 Figure 16 1069 Postel's Law is not limited to the interpretation of PDUs as a state 1070 machine on the receiving side can also be designed to accept more 1071 than than what a sending state machine can produce. A similar 1072 isomorphism proof can be used to ensure that this is done without 1073 loss of interoperability. 1075 5.3.4. Implementability 1077 When applied, the techniques described in Section 5.1 and Section 5.2 1078 result in a set of types that represents the whole protocol. These 1079 types can be assembled together, using another set of types, to 1080 represent a simulation of that protocol that covers all sending and 1081 receiving processes. 1083 The types can then be implemented, and that implementation acts as a 1084 proof that this protocol is actually implementable. 1086 To make these pieces of code composable, a specification is split in 1087 multiple modules, each one represented as a unique function. The 1088 type of each of these functions is derived from the state machines 1089 described in Section 5.2, by bundling together all the inputs of the 1090 state machine as the input for that function, and bundling all the 1091 outputs of the state machine as the output of this function. 1093 For instance the IP layer is really 4 different functions: 1095 * A function that converts between a byte array and a tree 1096 representation (parsing). 1098 * A function that takes a tree representation and a maximum MTU and 1099 returns a list of tree representations, each one fitting inside 1100 the MTU. 1102 * A function that accumulates tree representations of an IP fragment 1103 until a tree representation of a full IP packet can be returned. 1105 * A function that convert a tree representation into a byte array. 1107 The description of each function is incomplete, as in addition to the 1108 input and the output listed, these functions needs some ancillary 1109 data, in the form of: 1111 * state, which is basically values stored between evaluations of a 1112 function, 1114 * an optional signal, that can be used as an API request or 1115 response. As timers are a fundamental building block for 1116 communication protocols, one common uses for that signal are to 1117 request the arming of a timer, and to receive the indication of 1118 the expiration of that timer. 1120 5.3.5. Termination 1122 Proving that a protocol does not loop is equivalent to proving that a 1123 implementation of the types for that protocol does not loop either 1124 i.e., terminates. This is done by using the type described in 1125 Section 5.3.4 and making sure that it type-check when the "total" 1126 keyword is used. 1128 5.3.6. Liveness 1130 A protocol may never terminate - in fact most of the time the server 1131 side of a protocol is a loop - but it still can do some useful work 1132 in that loop. This property is called liveness. 1134 6. Importing Specifications 1136 | NOTE: The code for the libraries described in that section is 1137 | not yet ready to be published. 1139 One of the ultimate goals of this document is to convince authors to 1140 use the techniques described there to write their documents. Because 1141 doing so requires a lot of efforts, an important intermediate goal is 1142 to show authors that the benefits of Computerate Specifying are worth 1143 learning and becoming proficient in these techniques. 1145 The best way to reach that intermediate goal is to apply these 1146 technique to documents that are in the process of being published by 1147 the IETF and if issues are found, report them to the authors. Doing 1148 that on published RFCs, especially just after their publication, 1149 would be unnecessarily mean. On the other hand doing that on all 1150 Internet-Drafts as they are published would not be scalable. 1152 The best place to do a Computerate Specifying oriented review is when 1153 a document enters IETF Last Call. These reviews would then be 1154 indistinguishable from the reviews done by an hypothetical Formal 1155 Specification Directorate. An argument can be made that, ultimately, 1156 writing a specification for a document could be an activity too 1157 specialized, just like Security reviews are, and that an actual 1158 Directorate should be assembled. 1160 Alas, it is clear that writing a specification from scratch (as in 1161 Section 5) for an existing document takes far more time than the Last 1162 Call duration would allow. On the other hand the work needed could 1163 be greatly reduced if, instead of writing that specification from 1164 scratch, libraries of code would be available for the parts that are 1165 reusable between successive specifications. These libraries fall 1166 into 3 categories: 1168 * General types and common presentations. E.g., bit diagrams are a 1169 very common way of presenting data, and so reusable types and 1170 functions to generate and compare them would accelerate a 1171 formalization. The libraries in that category are explained in 1172 Section 6.1, in Section 8.1, and its associated reference in 1173 Appendix B. 1175 * Types and common representations for meta-languages. A few meta- 1176 languages are used in documents to formalize some parts of them, 1177 so having libraries to formalize these meta-languages also helps 1178 accelerating their verification. The libraries in that category 1179 are explained in Section 6.2, in Section 8.2, and its associated 1180 reference in Appendix B. 1182 * Types and common representation for common protocols. Most 1183 documents are about modifying or defined new usages for existing 1184 protocols, which is why it makes sense to establish libraries of 1185 these existing protocols for reuse. The libraries in that 1186 category are explained in Section 6.3, in Section 8.3, and its 1187 associated reference in Appendix B. 1189 Together these libraries form the Computerate Specifying Standard 1190 Library (Section 8). 1192 These libraries are in fact computerate specifications that, instead 1193 of being private, are designed to export types and code and be 1194 imported in other computerate specifications. Section 7 describes 1195 how to build an specification that can be exported. 1197 The types and code in a computerate specification form an Idris 1198 package, which is a collection of Idris modules. An Idris module 1199 form a namespace hierarchy for the types and functions defined in it 1200 and is physically stored as a file. 1202 Different types of specification can be combined, for instance an 1203 exporting library may import from another specification, and this 1204 recursively until importing specifications that are both self- 1205 contained and exporting. 1207 For convenience each public computerate specification, including the 1208 one behind this document, is available as an individual git 1209 repository. There is exactly one Idris package per git repository. 1210 Appendix A.5 explains how to gain access to these computerate 1211 specifications. 1213 6.1. Common Modules 1215 This document is itself generated from a computerate specification 1216 that contains data types and functions that can be reused in future 1217 specifications, and as a whole is part of the standard library for 1218 computerate specifying. The following sections describes the Idris 1219 modules defined in that specification. 1221 6.1.1. Generating AsciiDoc 1223 The code described in Section 5 directly generates text that is to be 1224 embedded inside an AsciiDoc document. This is fine for small 1225 examples but AsciiDoc has quite a lot of escaping rules that are 1226 difficult to use in a consistent manner. 1228 For this reason the specification behind this document provides a 1229 module named "AsciiDoc" that contains a set of types that can be used 1230 to guarantee that the AsciiDoc text generated is compliant with its 1231 specification. All these types implement the "Show" interface so 1232 they can be directly returned by the embedded code. 1234 So instead of implementing a show function, a function returning an 1235 instance of one of the types can be executed directly as embedded 1236 code: 1238 1239 > example : InternetHeader -> Block 1240 > example ih = ?example_rhs 1242 {`example example1`} 1243 1245 Figure 17 1247 In the example above, the "example" function converts an 1248 "InternetHeader" value into an "AsciiDoc" block, which is 1249 automatically serialized as AsciiDoc text. 1251 The "AsciiDoc" module is not limited to generating examples, but can 1252 be used to generate any AsciiDoc structure from Idris code. E.g., 1253 the tables in Appendix C are generated using that technique. 1255 Section 8.1.1 provides a description of the "AsciiDoc" module. 1257 | NOTE: Similarly the RFC Editor has rules on how to present 1258 | source code and examples in a document, particularly about how 1259 | lines longer than 72 characters should be folded. A module 1260 | similar to the "AsciiDoc" module will be developed to apply 1261 | these rules transparently. 1263 Using an intermediary type will also permit to correctly generate 1264 AsciiDoc that can generate an xmlrfc 3 file that supports both text 1265 and graphical versions of a figure. This will be done by having 1266 AsciiDoc blocks converted into elements that contains both 1267 the 72 column formatted text and an equivalent SVG file, even for 1268 code source (instead of using the element). 1270 6.1.2. Common Data Types 1272 The type in Section 5.1.1 seems a good representation of the 1273 structure of the Internet Header, but the origin of a lot of the 1274 values in the constraints does not seems very obvious, and as such 1275 are still prone to errors. E.g., the calculation in Section 5.1.2 1276 could be better if it was using the type itself as a source for the 1277 calculated data. 1279 It also may be more convenient to use types that already have some of 1280 the properties we need, instead of having to add a bunch of 1281 constraints to the "Int" type. 1283 The truth of the matter is that the Idris standard library contains 1284 very few predefined types that are useful to specify the syntax of 1285 communication protocols. E.g., none of the builtin types ("Int", 1286 "Integer", "Double", "Char", "String", etc) are really suitable to 1287 describe a PDU syntax, and so should be avoided. For this reason, it 1288 is preferable to use the types provided by the Computerate Specifying 1289 standard library. 1291 We are going to redefine the "InternetHeader" type, but using three 1292 modules from the standard library: 1294 BitVector: A sequence of bits, or bit-vector, is the most primitive 1295 type with which a packet can be described. This module provides a 1296 type "BitVector n" that represents a sequence of bit of fixed size 1297 "n". The module also provides a set of functions that permits to 1298 manipulate bit-vectors. See Section 8.1.2 for a description of 1299 the "BitVector" module. 1301 Unsigned: The "Unsigned" module provides a type "Unsigned n" that is 1302 built on top of the "BitVector" module. In addition of the 1303 properties of a bit-vector, an "Unsigned n" is considered a number 1304 and so all the integer operations applies to it. See 1305 Section 8.1.3 for a description of the "Unsigned" module. 1307 Dimension: Some numbers (also called denominate numbers) are used in 1308 conjunction with a so-called unit of measure. The "Dimension" 1309 module provides a way to associate a dimension, in the form of a 1310 unit of measure, to an Idris number, including to the numbers 1311 defined in the "Unsigned" module. The "Dimension" module provides 1312 two dimensions, Data (with bit, octet, etc, as units of 1313 information) and Time (with second, millisecond, etc, as unit of 1314 time). See Section 8.1.4 for a description of the "Dimension" 1315 module. 1317 A redefinition of the type in Section 5.1.1 using the types in these 1318 modules would look like this: 1320 1321 data InternetHeader : Type where 1322 MkInternetHeader : 1323 (version : BitVector 4) -> version = [O, I, O, O] => 1324 (ihl : (Unsigned 4, Data)) -> snd ihl = tetra => 1325 (tos : BitVector 8) -> 1326 (length : (Unsigned 16, Data)) -> snd length = byte => 1327 (id : Unsigned 16) -> 1328 (flags : BitVector 3) -> 1329 (offset : Unsigned 13, Data)) -> snd offset = octa => 1330 (ttl : (Unsigned 8, Time)) -> snd ttl = second => 1331 (protocol : BitVector 16) -> 1332 (checksum : BitVector 16) -> 1333 (source : BitVector 32) -> 1334 (dest : BitVector 32) -> 1335 (options : List Option) -> 1336 (padding : BitVector n) -> 1337 InternetHeader 1338 1340 Figure 18 1342 version: This is bit-vector, but it always contains the same value, 1343 so a constraint states that. Because bit-vectors are not 1344 integers, the value must be expressed by a list of "O" (for 0) and 1345 "I" (for 1) constructors. 1347 ihl: This is an unsigned integer with a size of 4 bits. It is 1348 associated with a dimension, here the "Data" dimension, which is 1349 constrained to use the "tetra" unit (32-bit words). Basically a 1350 denominate number can only be added or subtracted with numbers 1351 with the same dimension (but not necessarily with the same unit). 1352 E.g. adding the "ihl" value with the "ttl" value will be rejected 1353 by Idris, because that operation does not make sense. A 1354 denominate number can also be divided or multiplied by a 1355 dimensionless number. 1357 tos, flags, protocol, source, dest: These are defined as bit- 1358 vectors, because they are not really numbers - they do not need to 1359 be compared, or be part of a calculation. The number in this type 1360 (and all the others) is the number of bits allocated. 1362 length: This is an unsigned number with a size of 16 bits, a "Data" 1363 dimension and a "byte" unit (8 bits). After casting as denominate 1364 numbers, subtracting "ihl" from "length" gives directly the size 1365 of the payload, without risk of scaling error. 1367 id: This is an unsigned integer. Comparisons and calculations are 1368 possible on this field. 1370 offset: This is an unsigned number with a length of 13 bits, a 1371 "Data" dimension and an "octa" unit (64 bits). Again, adding or 1372 subtracting this value after casting to another of the same 1373 dimension is guaranteed to return the correct value. 1375 ttl: This is a denominate number with "Time" as dimension and 1376 "second" as unit. 1378 options: This is a variable length field that contains a list of 1379 options, which are defined in a separate type named "Option". 1381 padding: This is a bit-vector whose length is variable. 1383 The "byte", "wyde", "octa", and "tetra" units are precisely defined 1384 in [TAOCP]. 1386 As we can see the noise in the definition of our type is greatly 1387 reduced by using these specialized types, which in turn permits to 1388 add even more constraints. 1390 We can even constrain the size of a field, like is done for the 1391 "padding" field below. In that case the length is calculated in the 1392 first constraint by calling the "pad" function, function that 1393 calculates the number of bits needed to pad a value of a type that 1394 implements the "Size" interface to a word boundary, here 32 bits. 1395 The second constraint checks that whatever the length of the padding 1396 field is, it is always equal to a zero-filled bit-vector, as returned 1397 by the function "bitVector". 1399 1400 data InternetHeader : Type where 1401 MkInternetHeader : 1402 (version : BitVector 4) -> version = [O, I, O, O] => 1403 (ihl : (Unsigned 4, Data)) -> snd ihl = tetra => 1404 (tos : Tos) -> 1405 (length : (Unsigned 16, Data)) -> snd length = octet => 1406 (id : Unsigned 16) -> 1407 (flags : Flags) -> 1408 (offset : Unsigned 13, Data)) -> snd offset = octa => 1409 (ttl : (Unsigned 8, Time)) -> snd ttl = second => 1410 (protocol : BitVector 16) -> 1411 (checksum : BitVector 16) -> 1412 (source : BitVector 32) -> 1413 (dest : BitVector 32) -> 1414 (options : List Option) -> 1415 (padding : BitVector n) -> 1416 n = pad 32 options => padding = bitVector => 1417 InternetHeader 1418 1420 Figure 19 1422 Dimensions can also be combined to seamlessly build more complex 1423 dimensions. For example, all "length" values of sent packets can be 1424 added up during a period of time, while keeping beginning and ending 1425 times as denominate numbers: dividing the "length" sum by the 1426 difference between the end time and the begin time gives us directly 1427 the data speed in bits per second (or whatever unit we prefer), with 1428 the guarantee that Idris will not let us mix oranges and apples. 1430 Here's an example of Sum type that implements some of the variants 1431 for an "Option" in an "InternetHeader": 1433 1434 data Option : Type where 1435 Eoo : (flag : BitVector 1) -> flag = [O] => 1436 (class : BitVector 2) -> class = [O, O] => 1437 (number : BitVector 5) -> number = [O, O, O, O, O] => 1438 Option 1439 Noop : (flag : BitVector 1) -> flag = [O] => 1440 (class : BitVector 2) -> class = [O, O] => 1441 (number : BitVector 5) -> number = [O, O, O, I, O] => 1442 Option 1443 Security : (flag : BitVector 1) -> flag = [I] => 1444 (class : BitVector 2) -> class = [O, O] => 1445 (number : BitVector 5) -> number = [O, O, O, I, O] => 1446 (length : Unsigned 8) -> length = 11 => 1447 (s : BitVector 16) -> 1448 (c : BitVector 16) -> 1449 (h : BitVector 16) -> 1450 (tcc : BitVector 24) -> 1451 Option 1452 Lssr : (flag : BitVector 1) -> flag = [I] => 1453 (class : BitVector 2) -> class = [O, O] => 1454 (number : BitVector 5) -> number = [O, O, O, I, I] => 1455 (length : Unsigned 8) -> 1456 (pointer : Unsigned 8) -> pointer >= 4 = True => 1457 Option 1458 1460 Figure 20 1462 6.1.3. Calculations 1464 The imported types that we are using in the definition of our types 1465 all implement the "Size" interface, which provides a definition for 1466 the adhoc polymorphic function "size", function that returns the size 1467 of a field as a dimensional number of dimension "Data". This 1468 interface can be implemented for the type "InternetHeader" by making 1469 its size the sum of the size of all its fields: 1471 1472 Show InternetHeader where 1473 size (MkInternetHeader version ihl tos length id flags offset ttl 1474 protocol checksum source dest options padding) = size version + 1475 size ihl + 1476 ... 1477 size padding 1478 1480 Figure 21 1482 We can then define a minimal header, and insert its size, using the 1483 right unit, in the document: 1485 1486 > minHeader : Data 1487 > minHeader = size $ MkInternetHeader [O, I, O, O] 1488 > (5, tetra) 1489 > (MkTos 0 [O] [O] [O] [O, O]) 1490 > (1000, wyde) 1491 > 0 1492 > (MkFlags bitVector bitVector bitVector) 1493 > (0, octa) 1494 > (64, second) 1495 > bitVector 1496 > bitVector 1497 > (A [O] bitVector bitVector) 1498 > (A [O] bitVector bitVector) 1499 > [] 1500 > [] 1502 Note that the minimum value for a correct header is 1503 {`fromDenominate (size ih) tetra`} 1504 1506 Figure 22 1508 6.1.4. Typed Petri Nets 1510 A better solution than defining an adhoc type for our state machines, 1511 as explained in Section 5.2, is to use Petri Nets. This 1512 specification defines a DSL that permits describing a Typed Petri Net 1513 (TPN) which is heavily influenced by Coloured Petri Nets [CPN] (CPN). 1514 The original CPN adds some restriction on the types that can be used 1515 in a Petri Net because of limitations in the underlying programming 1516 language, SML. As the underlying programming used in TPN, Idris, 1517 does not have these limitations, any well-formed Idris type 1518 (including polymorphic, linear and dependent types) can be directly 1519 used in TPN. 1521 Here's an example of TPN from figure 2.10 in [CPN]: 1523 1524 NO : Type 1525 NO = Int 1527 DATA : Type 1528 DATA = String 1530 NOxDATA : Type 1531 NOxDATA = (NO, DATA) 1533 PTS : Place 1534 PTS = MkPlace "Packets To Send" NOxDATA (\() => [(1, "COL"), 1535 (2, "OUR"), (3, "ED "), (4, "PET"), (5, "RI "), (6, "NET")]) 1537 NS : Place 1538 NS = MkPlace "NextSend" NO (\() => [1]) 1540 A : Place 1541 A = MkPlace "A" NOxDATA (\() => []) 1543 input1 : Input 1544 input1 = MkInput PTS (NO, DATA) pure 1546 input2 : Input 1547 input2 = MkInput NS NO pure 1549 output1 : Output 1550 output1 = MkOutput PTS (NO, DATA) pure 1552 output2 : Output 1553 output2 = MkOutput NS NO pure 1555 output3 : Output 1556 output3 = MkOutput A (NO, DATA) pure 1558 sendPacket : Transition 1559 sendPacket = MkTransition [input1, input2] [output1, output2, 1560 output3] (\((n, d), n') => if n == n' 1561 then pure ((n, d), n, (n, d)) 1562 else empty) 1563 1565 Figure 23 1567 | NOTE: The DSL is being currently designed, so the example shows 1568 | the generated values. 1570 From there it is easy to generate (using the non-deterministic monad 1571 in Idris) an interpreter for debugging and simulation purposes: 1573 1574 interpret : MS NOxDATA -> MS NO -> MS NOxDATA -> 1575 ND (MS NOxDATA, MS NO, MS NOxDATA) 1576 interpret pts ns a = do 1577 (pts1, pts2) <- sel pts 1578 (ns1, ns2) <- sel ns 1579 i1 <- input input1 pts1 1580 i2 <- input input2 ns1 1581 (pts3, ns3, a3) <- transition sendPacket (i1, i2) 1582 let o1 = output output1 pts3 1583 let o2 = output output2 ns3 1584 let o3 = output output3 a3 1585 pure (o1 ++ pts2, o2 ++ ns2, o3 ++ a) 1586 1588 Figure 24 1590 A Petri Net has the advantage that the same graph can be reused to 1591 derive other Petri Nets, e.g., Timed Petri Nets (that can be used to 1592 collect performance metrics) or Stochastic Petri Nets. 1594 A TPN that covers a whole protocol (i.e. client, network, and server) 1595 is useful to prove the properties listed in Section 5.3.4, 1596 Section 5.3.5, and Section 5.3.6. But the TPN is also designed in a 1597 way that each of these parts can be defined separately from the 1598 others, making it a Hierarchical TPN. 1600 6.1.5. Representations 1602 Another usage of our Idris type would be to generate a textual 1603 representation of that type. 1605 Figure 4 in RFC 791 is a good example of a representation of a data 1606 layout, here as a bit diagram. Because we already have an Idris type 1607 which is describing exactly the same thing, the idea of syntax 1608 representation is to convert that type into text, and insert it in 1609 place of the bit diagram. 1611 For each textual representation of a type, it is possible to write a 1612 function that takes as parameter this type and generate an "AsciiDoc" 1613 value that can then be inserted in the document. 1615 Some document uses representations that are unique to this document 1616 but often multiple documents share the same representation and so 1617 that function can be also shared between them. A set of such 1618 functions is available as part of the Computerate Specification 1619 standard library, 1621 6.1.5.1. Bit Diagrams 1623 The bit diagram is one of the most frequently used representation of 1624 a PDU specification in documents, so a function to convert an Idris 1625 type into a bit diagram is provided as part of the standard library. 1627 That function takes as parameters an Idris type, a structure 1628 containing additional informations, and returns an "AsciiDoc" value 1629 that can be inserted in the document. 1631 The additional structure is a list of the properties associated to 1632 each field that are needed to generate the bit diagram. For a bit 1633 diagram the only property is a character string containing the name 1634 of the field. 1636 For our "InternetHeader" type, that additional structure would look 1637 like this: 1639 1640 names : Pdu 1641 names = MkPdu `{{MkInternetHeader}} [ 1642 MkField "Version", 1643 MkField "IHL", 1644 MKField "Type of Service", 1645 MkField "Total Length", 1646 MkField "Identification", 1647 MkField "Flags", 1648 MkField "Fragment Offset", 1649 MkField "Time to Live", 1650 MkField "Protocol"] 1651 1653 Figure 25 1655 The Pdu type takes care of verifying that each name is unique in the 1656 structure, and that each name length does not exceed "2 * (size 1657 field) - 1", so it is guaranteed to fit in the bit diagram cell. 1659 After that it is just a matter of inserting the function call in the 1660 document (the "%runElab" keyword indicates that the Idris code is 1661 using reflection elaboration, which is used to inspect a type). 1663 1664 {`%runElab toBitDiagram names`} 1665 1667 Figure 26 1669 6.1.5.2. Message Sequence Charts 1671 Message Sequence Charts are a common way to represent an example of 1672 execution of a Petri Net, i.e. of the interactions between the 1673 underlying state machines. Although sequence charts are often 1674 implicitly used to describe a protocol, that description can only be 1675 partial. 1677 Nonetheless, this is a very common way to show state machine related 1678 examples in a document, so a library will permit to specify an 1679 execution in a Petri Net (i.e. a list of Transitions and their 1680 Bindings), and convert it into a message sequence chart that can be 1681 inserted into the document. Optionally the message sequence chart 1682 generated can be followed by an ordered list of the messages 1683 themselves. 1685 6.2. Packages for Meta-Languages 1687 When different representations of a specification share some common 1688 characteristics, it is usual to generalize them into a formal 1689 language. 1691 One shared limitation of these languages is that they cannot always 1692 formalize all the constraints of a specific data layout, so they have 1693 to be enriched with comments. One consequence of this is that they 1694 cannot be used as a replacement for the Idris types described in 1695 Section 5.1.1 or Section 6.1.2, types that are purposely designed to 1696 be as complete as possible. 1698 Another consequence is the proliferation of these languages, with 1699 each new formal language trying to integrate more constraints than 1700 the previous ones. For that reason Computerate Specifying does not 1701 favor one formal language over the others, and will try to provide 1702 code to help use all of them. 1704 Similarly to what was explained in Section 5.1 a set of types can be 1705 designed and then used to type-check instance of that formal 1706 language, and convert them into a textual representation. Most of 1707 the formal languages used at the IETF already come with a set of 1708 tools that permits to verify that the text representation in an RFC 1709 is syntactically correct, so that type does not add much to that. 1711 On the other hand that type can be the target of a converter from an 1712 ad-hoc type. This will ensure that the generated instance of the 1713 formal language matches the specification, which is something that 1714 external tools cannot do. 1716 When a PDU is described with a formal language, we end up with two 1717 descriptions, one using the Idris dependent type (and used to 1718 generate examples) and the other using the formal language. 1720 Proving isomorphism requires generating an Idris type from the formal 1721 language instance, which is done using an Idris elaborator script. 1723 In Idris, Elaborator Reflection [Elab] is a metaprogramming facility 1724 that permits writing code generating type declarations and code 1725 (including proofs) automatically. 1727 For instance the ABNF language is itself defined using ABNF, so after 1728 converting that ABNF into an instance of the Syntax type (which is an 1729 holder for a list of instances of the Rule type), it is possible to 1730 generate a suite of types that represents the same language: 1732 1733 > abnf : Syntax 1734 > abnf = MkSyntax [ 1735 > "rulelist" `Eq` (Repeat (Just 1) Nothing (Group (Altern 1736 > (TermName "rule") (Group (Concat (Repeat Nothing Nothing 1737 > (TermName "c-wsp")) (TermName "c-nl") [])) []))), 1738 > ... 1739 > ] 1740 > 1741 > %runElab (generateType "Abnf" abnf) 1742 1744 Figure 27 1746 The result of the elaboration can then be used to construct a value 1747 of type Iso, which requires four total functions, two for the 1748 conversion between types, and another two to prove that sequencing 1749 the conversions results in the same original value. 1751 The following example generates an Idris type "SessionDescription" 1752 from the SDP ABNF. It then proves that this type and the Sdp type 1753 contain exactly the same information (the proofs themselves have been 1754 removed, leaving only the propositions): 1756 1757 import Data.Control.Isomorphism 1759 sdp : Syntax 1760 sdp = MkSyntax [ 1761 "session-description" `Eq` (Concat (TermName "version-field") 1762 (TermName "origin-field") [ 1763 TermName "session-name-field", 1764 Optional (TermName "information-field"), 1765 Optional (TermName "uri-field"), 1766 Repeat Nothing Nothing (TermName "email-field"), 1767 Repeat Nothing Nothing (TermName "phone-field"), 1768 Optional (TermName "connection-field"), 1769 Repeat Nothing Nothing (TermName "bandwidth-field"), 1770 Repeat (Just 1) Nothing (TermName "time-description"), 1771 Optional (TermName "key-field"), 1772 Repeat Nothing Nothing (TermName "attribute-field"), 1773 Repeat Nothing Nothing (TermName "media-description") 1774 ]), 1775 ... 1776 ] 1778 %runElab (generateType "Sdp" sdp) 1780 same : Iso Sdp SessionDescription 1781 same = MkIso to from toFrom fromTo 1782 where 1783 to : Sdp -> SessionDescription 1785 from : SessionDescription -> Abnf 1787 toFrom : (x : SessionDescription ) -> to (from x) = x 1789 fromTo : (x : Sdp) -> from (to x) = x 1790 1792 Figure 28 1794 As stated in Section 5.3.1, the Idris type and the type generated 1795 from the formal language are not always isomorphic, because some 1796 constraints cannot be expressed in that formal language. In that 1797 case isomorphism can be used to precisely define what is missing 1798 information in the formal language type. To do so, the generated 1799 type is augmented with a delta type, like so: 1801 1802 data DeltaSessionDescription : Type where 1803 ... 1805 same : Iso Sdp (SessionDescription, DeltaSessionDescription) 1806 ... 1807 1809 Figure 29 1811 Then the DeltaSessionDescription type can be modified to include the 1812 missing information until the same function type checks. After this 1813 we have a guarantee that we know all about the constraints that 1814 cannot be encoded in that formal language, and can check manually 1815 that each of them are described as comments. 1817 An interesting comment in [Momot16] states that if the input of an 1818 application is too complex to be expressed in ABNF without adding 1819 comments, it is too complex to be safe. The technique described in 1820 this section can be used to evaluate the safety of such ABNF by 1821 clearly specifying the impact of these additional comments. 1823 Idris elaborator scripts will be developed for each formal languages. 1825 The following sections describe how these formal languages have been 1826 or will be themselves be converted into types with the goal of 1827 importing them in computerate specifications. 1829 6.2.1. Augmented BNF (ABNF) 1831 Augmented Backus-Naur Form (ABNF) [RFC5234] is a formal language used 1832 to describe a text based data layout. 1834 An ABNF can be described by defining a value for the types from the 1835 "RFC5234.Main" module: 1837 1838 rulename : Rule 1839 rulename = "rulename" `Eq` (Concat (TermDec 97 []) (TermDec 98 []) 1840 [TermDec 99 []]) 1841 1843 Figure 30 1845 That value can then be inserted in a document, which will convert it 1846 as a proper ABNF, so 1847 1848 [source,abnf] 1849 ---- 1850 {`rulename`} 1851 ---- 1852 1854 Figure 31 1856 is rendered as 1858 rulename = %d97 %d98 %d99 1860 Figure 32 1862 See Section 8.2.2 for details on that package. 1864 6.2.2. Augmented Packet Header Diagrams (APHD) 1866 Augmented Packet Header Diagram (APHD) 1867 [I-D.mcquistin-augmented-ascii-diagrams] is a formal language used to 1868 describe an augmented bit diagram in a machine-readable format. 1870 It can be seen as an extension to the self-contained bit diagram in 1871 Section 5.1.3, where more information are extracted from the Idris 1872 type, and more properties are carried in the list of properties: 1874 * From the Idris type: 1876 - The size of a field in the Idris type is converted into the 1877 field's width. 1879 - The size constraints in Idris are converted into a variable 1880 size field (Section 4.1). 1882 - A constraint that reduces the possible values (like for the 1883 version field) is converted into a constraint on field value 1884 (Section 4.4). 1886 - Alternative constructors (i.e., a Sum type) generate a presence 1887 predicate (Section 4.2). 1889 * From the additional structure: 1891 - The name of the PDU. 1893 - The name of each field 1894 - The eventual short name for each field, with the same 1895 constraint than in Section 5. 1897 - The Bit unit to use to display the size for each field. 1899 - The description for each field. 1901 The description for each field is a value of "AsciiDoc" type, which 1902 permits to correctly format it. In addition, it is possible to 1903 insert calculation or even other type representation in the 1904 description by using an "AsciiDoc" type that works similarly than 1905 code embedding. 1907 Reusing the type in Section 6.1.2, the conversion process would 1908 partially look like this: 1910 1911 > ipv4 : AphdPdu 1912 > ipv4 = MkAphd `{{MkInternetHeader}} "IPv4 Header" [ 1913 > MkField "Version" (Just "V") Bit [(MkSentence "This is a" ++ 1914 > "fixed-width field, whose full label is shown in the " ++ 1915 > "diagram. The field's width --), MkCode(`(size version)), 1916 > MkSentence(" bits -- is given in the label of the " ++ 1917 > "description list, separated from the field's label " ++ 1918 > "by a colon.")], 1919 > ... 1920 > ] 1922 {`%runElab toAphd names`} 1923 1925 Figure 33 1927 and is rendered as: 1929 An IPv4 Header is formatted as follows: 1930 0 1 2 3 1931 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 1932 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1933 |Version| IHL | DSCP |ECN| Total Length | 1934 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1935 | Identification |Flags| Fragment Offset | 1936 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1937 | Time to Live | Protocol | Header Checksum | 1938 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1939 | Source Address | 1940 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1941 | Destination Address | 1942 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1943 | Options ... 1944 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1945 | : 1946 : Payload : 1947 : | 1948 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ 1950 where: 1952 Version (V): 4 bits. This is a fixed-width field, whose full label 1953 is shown in the diagram. The field's width -- 4 bits -- is given 1954 in the label of the description list, separated from the field's 1955 label by a colon. 1956 ... 1958 Figure 34 1960 6.2.3. Cosmogol 1962 Cosmogol [I-D.bortzmeyer-language-state-machines] is a formal 1963 language designed to define states machines. The Internet-Draft will 1964 be retrofitted as a computerate specification to provide an internal 1965 Domain Specific Language (DSL) that permits specifying an instance of 1966 that language. 1968 As a Petri Net can be seen as a set of state machines, it will be 1969 possible to extract part of a Petri Net and generate the equivalent 1970 state machine in Cosmogol format. 1972 6.3. Packages for Protocols 1973 6.3.1. Type Transformations 1975 Protocols evolve over time, and the documents that standardize them 1976 also need to evolve with them. Each SDO has a specific set of 1977 methods to do so, from having the possibility of modifying a 1978 document, to systematically releasing a complete new document when a 1979 modification is needed. The IETF uses a combination of methods to 1980 update the documents that define a protocol. 1982 One such method is to release a new document that completely replaces 1983 ("obsoletes") an existing protocol. E.g., TLS 1.2 [RFC5246] was 1984 completely replaced by TLS 1.3 [RFC8446] such as there is no need to 1985 read RFC 5246 to be able to implement RFC 8446. 1987 Alternatively only part of a protocol needs modification, so the 1988 method used in that case is to issue a new document that only updates 1989 that specific part. E.g., RFC 2474 updates only the definition of 1990 the ToS field in the Internet Header defined in RFC 791, so reading 1991 both documents is required to implement the Internet Protocol. These 1992 two methods can be combined together, like was done for RFC 2474. 1993 RFC 2474 obsoleted RFC 1349 and RFC 1349 was the original update for 1994 RFC 791. 1996 Systematically updating a protocol in new documents instead of 1997 replacing it means that sometimes a lot of different documents has to 1998 be read before implementing a modern implementation of a specific 1999 protocol. E.g., the DNS was originally defined in RFC 1034 and 1035, 2000 but was updated by more than 30 documents since, requiring to read 2001 all of them to implement that protocol. 2003 In the DNS example we are not even counting definitions of codepoints 2004 as protocol updates. This is the third method used at the IETF to 2005 evolve a standard, by defining new codepoints and their associated 2006 data. That last method will be explored in more detail in 2007 Section 6.3.2, so the remaining of this section can focus on the two 2008 other methods. 2010 Writing a computerate specification for a new document or a document 2011 that obsoletes another one is straightforward, as the specification 2012 will contain all the types that are needed to formalize it. On the 2013 other hand it is less clear what should go into a specification that 2014 updates another one. 2016 A simplistic solution is to copy the whole Idris content from the 2017 original specification into the new one and modify that new content, 2018 but this creates a few problems: 2020 Firstly the content from the original specification will have to be 2021 copied again each time it was modified, as computerate specifications 2022 are meant to evolve, even if the underlying document did not. 2024 Secondly the size of the code should be roughly proportional to the 2025 size of the document itself, so the actual update is made obvious 2026 from the content. 2028 So instead of manually copying the content, an Idris elaboration can 2029 be used to copy it automatically and apply the minimal modifications 2030 needed at the same time. 2032 But first the specification that will be updated needs to be 2033 prepared, by encapsulating the types in a function that will be used 2034 to generate the types themselves: 2036 2037 export 2038 internetHeader : List Decl 2039 internetHeader = `[ 2040 ||| InternetHeader 2041 export 2042 data InternetHeader : Type where 2043 MkInternetHeader : 2044 (version : BitVector 4) -> version = [O, I, O, O] => 2045 (ihl : (Unsigned 4, Data)) -> snd ihl = tetra => 2046 (tos : Tos) -> 2047 (length : (Unsigned 16, Data)) -> snd length = octet => 2048 (id : Unsigned 16) -> 2049 (flags : Flags) -> 2050 (offset : Unsigned 13, Data)) -> snd offset = octa => 2051 (ttl : (Unsigned 8, Time)) -> snd ttl = second => 2052 (protocol : BitVector 16) -> 2053 (checksum : BitVector 16) -> 2054 (source : BitVector 32) -> 2055 (dest : BitVector 32) -> 2056 (options : List Option) -> 2057 (padding : BitVector n) -> 2058 n = pad 32 options => padding = bitVector => 2059 InternetHeader 2060 ] 2061 %runElab declare internetHeader 2062 2064 Figure 35 2066 This code behaves exactly like the previous definition, with the 2067 major difference that the documentation is not generated for that 2068 type. Idris2 has been enhanced with the possibility to cache the 2069 result of an elaboration directly in the source code, and to 2070 automatically send a warning when the cache needs to be refreshed. 2071 The interactive command ":gc " automatically generates the code 2072 followed by a "%cacheElab" line that indicates where the code 2073 generated ends, something like this: 2075 2076 %runElab declare internetHeader 2077 export 2078 ||| InternetHeader 2079 data InternetHeader : Type where 2080 MkInternetHeader : 2081 (version : BitVector 4) -> version = [O, I, O, O] => 2082 (ihl : (Unsigned 4, Data)) -> snd ihl = tetra => 2083 (tos : Tos) -> 2084 (length : (Unsigned 16, Data)) -> snd length = octet => 2085 (id : Unsigned 16) -> 2086 (flags : Flags) -> 2087 (offset : Unsigned 13, Data)) -> snd offset = octa => 2088 (ttl : (Unsigned 8, Time)) -> snd ttl = second => 2089 (protocol : BitVector 16) -> 2090 (checksum : BitVector 16) -> 2091 (source : BitVector 32) -> 2092 (dest : BitVector 32) -> 2093 (options : List Option) -> 2094 (padding : BitVector n) -> 2095 n = pad 32 options => padding = bitVector => 2096 InternetHeader 2097 %cacheElab 1506359842985480550 1506359842985480550 2098 2100 Figure 36 2102 The numbers on the "%cacheElab" line are hashes of, respectively, the 2103 elaboration code and the generated text and permit to detect if 2104 either were modified since the last time the code was cached. 2106 With that we can import the definition of the "InternetHeader" type 2107 and clone in in our new specification: 2109 2110 import RFC791.IP 2112 %runElab declare internetHeader 2113 2114 Figure 37 2116 The modification needed by the new document can be done by replacing 2117 the "ToS" field by the newly defined "DSField", using the "replace" 2118 function: 2120 2121 import RFC791.IP 2122 import ComputerateSpecifying.Transform 2124 dscp : List Decl 2125 dscp = `[ 2126 public export 2127 data Dscp : Type where 2128 MkDscp : (dscp : BitVector 6) -> 2129 (reserved : BitVector 2) -> reserved = bitVector => 2130 Dscp 2131 ] 2132 %runElab declare dscp 2134 %runElab declare (add mypath internetHeader dcp) 2135 2137 Figure 38 2139 At this point using elaboration caching would permit to check that 2140 the new type indeed uses the "Dscp" type instead of the old "Tos" 2141 type. 2143 6.3.2. Extended Registries 2145 | NOTE: The mechanisms described in this section requires Type 2146 | Providers that are not yet available in Idris2. Until then, 2147 | the constants built by future type providers can be populated 2148 | by hand. 2150 At the difference of the previous section, that describes how to 2151 formalize the unplanned evolution of a protocol, most protocols are 2152 designed with the potentiality of evolution, also known as 2153 extensibility. These potentialities are generally expressed as 2154 values for some fields that will be later assigned to a new meaning. 2156 The meaning for a new value will be defined in a new document, with 2157 all the documents giving new meanings to a field easily locatable in 2158 a registry. 2160 Following up on our previous example, RFC 791 defines IP Options only 2161 for values 0, 1, 7, 68, 131, 136, and 137. These values, together 2162 with new values defined by other documents, are listed in the IP 2163 Option Numbers IANA registry. E.g., that IANA registry also defines, 2164 among others, value 25 in RFC 4782. 2166 The values that are part of a registry are designed to be used with 2167 the protocol that defined that registry, so it makes sense to 2168 synthesise a Sum type of all these values in the computerate 2169 specification for the document that defined that registry. 2171 Building that Sum type can be done by applying transformations to the 2172 original type, just like when modifying a protocol in a new 2173 specification. The difference is that the list of types that will be 2174 used in the Sum type needs be collected from the registry, and 2175 updated each time the registry is updated. 2177 Idris has a mechanism to read external data during type-checking (a 2178 feature known as Type Provider), mechanism that could be used to read 2179 the content of the registry. A registry generally contains the 2180 codepoint that identifies a new value and the name of the document 2181 that defines that value, but unfortunately the protocol registries do 2182 not contain enough information to automatically find the Idris2 type 2183 that matches a specific codepoint. 2185 For instance IANA is the organization that is maintaining the 2186 registries for the IETF. The "IP Option Numbers" is an example of a 2187 registry that contains the list of all the IP Options that can be 2188 carried by the Internet Protocol. E.g., in that registry RFC 1191 2189 contains the description for multiple entries in the registry, and so 2190 an additional mechanism is needed to find the Idris2 type for each of 2191 them. 2193 That additional mechanism is abstracted as an extended registry that 2194 complements the existing registry, but for the sole purpose of 2195 finding the exact type to use for each codepoint to generate that Sum 2196 type. 2198 Building an "InternetHeader" type that contains all the IP Options 2199 defined at the time of type-checking looks like this; 2201 2202 %provide (ipParameter : List (String, Decl)) with registry 2203 ("https://www.iana.org/assignments/ip-parameters/" ++ 2204 "ip-parameters.xhtml#ip-parameters-2") 2206 %runELab traverse (add transform internetHeader Add) (type registry) 2207 2208 Figure 39 2210 The "%provide" statement reads both the IANA registry and its 2211 associated extended registry and stores the result in the 2212 "ipParameter" constant. Then the "%runElab" statement repetitively 2213 adds the types retrieved to the "InternetHeader" type. 2215 Instead of having to manually maintain the extended registries, they 2216 can be automatically updated by information coming from the type- 2217 checking of the types in the respective computerate specifications 2218 that define new values, by binding a specific entry in a registry 2219 with the type in the specification. 2221 The mechanism used is also based on a type provider, but this time to 2222 update the extended registry instead of reading from it: 2224 2225 %provide (mtur: ()) with extendRegistry 2226 ("https://www.iana.org/assignments/ip-parameters/" ++ 2227 "ip-parameters.xhtml#ip-parameters-2") 2228 "11" mtuR 2229 %provide (mtut : ()) with extendRegistry 2230 ("https://www.iana.org/assignments/ip-parameters/" ++ 2231 "ip-parameters.xhtml#ip-parameters-2") 2232 "12" mtuT 2233 2235 Figure 40 2237 Here the statements bind the types defined in "mtuR" and "mtuT" to 2238 codepoints 11 and 12 in the extended registry of IANA's IP Option 2239 Numbers registry. 2241 The next time the code in Figure 39 is type-checked, it will add 2242 constructors for these two IP Options. 2244 7. Exporting Specifications 2246 | NOTE: The infrastructure for sharing the git repositories for 2247 | exported packages is not ready yet. 2249 7.1. Standard Library 2251 Computerate specifications can formalize their content to make it 2252 reusable as a building block for other specifications. A 2253 specification that organizes its content along the guidelines 2254 presented in this section can become a part of the Computerate 2255 Specification Standard Library. 2257 To be part of the Standard Library, specifications must be organized 2258 in 4 components: 2260 Code: This is the formalization of the content of the standard as an 2261 Idris package i.e., a set of Idris modules (i.e. files) that 2262 exports some or all of the types and functions defined in it. The 2263 code of these Idris modules is generally interspersed with the 2264 content of the standard to form literate code. 2266 Tutorial: This is a document section that guides the reader step by 2267 step in the use of the Idris package in a Computerate 2268 Specification. A tutorial may import the package itself to 2269 validate the examples provided as part of the tutorial. This 2270 section is considered informative. 2272 Description: This is a document section that explains the Idris 2273 package as a whole i.e, grouping explanations by feature. 2275 Reference: This is a document section that is auto-generated from 2276 the structured comments in the types and functions of the code 2277 Idris package. It lists all the types and functions in alphabetic 2278 order, including the comments on parameters. 2280 This document is itself an Idris package that is part of the Standard 2281 Library, Section 7 contains the tutorial part of that package, 2282 Section 8.1 forms its description part, and Appendix B contains its 2283 reference. 2285 For a retrofitted document, the code will be mixed with the existing 2286 standard to produce a Computerate Specification but the tutorial, 2287 description and reference parts cannot be added to that standard, so 2288 they have to be part of a separate document. It can be a new 2289 specification written for the express purpose of documenting that 2290 package. This is the case for this specification, which documents a 2291 selection of retrofitted Computerate Specifications that are part of 2292 the Standard Library. E.g., Section 6.2.1, and Section 8.2.2 are 2293 respectively the tutorial and the description for [RFC5234]. 2295 For a new document, the four components should be part of it. E.g., 2296 in this document Section 6.1.5.1, Section 8.1.5, and Appendix B.1.2 2297 are respectively the tutorial, description, and reference for the 2298 "BitDiagram" module. 2300 7.2. Transclusions 2302 RFCs, Internet-Drafts and standard documents published by other SDOs 2303 did not start their life as computerate specifications, so to be able 2304 to use them as Idris packages they will need to be progressively 2305 retrofitted. This is done by converting the documents into an 2306 AsciiDoc documents and then enriching them with code, in the same way 2307 that would have been done if the standard was developed directly as a 2308 computerate specification. 2310 Converting the whole document in AsciiDoc and enriching it with code, 2311 instead of just maintaining a library of code, seems a waste of 2312 resources. The reason for doing so is to be able to verify that the 2313 rendered text is equivalent to the original standard, which will 2314 validate the examples and formal languages. 2316 Retrofitted specifications will also be made available as individual 2317 git repositories as they are converted. 2319 Because the IETF Trust does not permit modifying an RFC as a whole 2320 (except for translation purposes), a retrofitted RFC uses 2321 transclusion, a mechanism that includes parts of a separate document 2322 at runtime. This way, a retrofitted RFC is distributed as two 2323 separate files, the original RFC in text form, and a computerate 2324 specification that contains only code and transclusions. 2325 Transclusions use are explained in Appendix A.2.2. 2327 7.3. Exporting Types and Functions 2329 Types and functions are exported by using the "export" keyword. Type 2330 constructors, interface functions and type functions implementation 2331 can be additionally exported by prepending the keyword "public" to 2332 the "export" keyword. 2334 Additionally, types that may be transformed should be declared as 2335 explained in Section 6.3.2, i.e. by wrapping them first in a exported 2336 function that uses a quote declaration, then generating them locally 2337 using a "declare" elaboration. 2339 8. Standard Library 2341 | NOTE: The libraries described in that section are not yet 2342 | available. 2344 8.1. Internal Modules 2345 8.1.1. AsciiDoc 2347 The AsciiDoc module provides a way to programmatically build an 2348 AsciiDoc document without having to worry about the particular 2349 formatting details. 2351 Note that, at the difference of the AsciiDoc rendering process that 2352 tries very hard to render a document in any circumstances, the types 2353 in this module are meant to only generate a correct document. 2355 E.g., the string "this is {`N "*bold*""}bold` will be rendered as 2356 "this is *bold*". If the intent was to render the "bold" word in 2357 bold, then the string should have been "this is {`Bold "bold""}`. 2359 8.1.2. BitVector 2361 The Computerate Specifying Library provides a number of types and 2362 functions aimed at defining and manipulating the data types that are 2363 commonly found in Protocol Data Units (PDU). The most elementary 2364 type of data is the bit-vector, which is a list of individual bits. 2365 Bit-vectors are not always sufficient to describe the subtleties the 2366 data types carried in a PDU, and several more precise types are built 2367 on top of them. See Section 8.1.3 for unsigned integers. 2369 "BitVector" is a dependent type representing a list of bits, indexed 2370 by the number of bits contained in that list. The type is inspired 2371 by Chapter 6 of [Kroening16] and by [Brinkmann02]. 2373 A value of type "BitVector n" can be built as a series of zeros 2374 ("bitVector") or can be built by using a list of "O" (for 0) and "I" 2375 (for 1) constructors. E.g., "[O, I, O, O]" builds a bit-vector of 2376 type "BitVector 4" with a value equivalent to 0x0100. 2378 Bit-vectors can be compared for equality, but they are not ordered. 2379 They also are not numbers and arithmetics operations cannot be 2380 applied to them. 2382 Bit-vectors can be concatenated ("concat"), a smaller bit-vector can 2383 be extracted from an existing bit-vector ("extract"), or a bit-vector 2384 can be extended by adding a number of zeros in front of it 2385 ("extend"). 2387 The usual unary bitwise ("shiftL", "shiftR", "not") operations are 2388 defined for bit-vectors, as well as binary bitwise operations between 2389 two bit-vectors of the same size ("and", "or", "xor") 2391 Finally it is possible to convert the bit at a specific position in a 2392 bit-vector into a "Bool" value ("test"). 2394 8.1.3. Unsigned 2396 A value of type "Unsigned n" encodes an unsigned integer as a 2397 "BitVector" of length "n". 2399 8.1.4. Dimension 2401 This module permits to manipulate denominate numbers, which are 2402 numbers associated with a unit. Examples of denominate numbers are 2403 "cast (5, meter / second)" (which uses a unit of speed), or "cast 2404 (10, meter * meter * meter)" (which uses a unit of volume). 2406 In this module a denominate number is a value of type "Denominate 2407 xs". It carries one number as a fraction. Its type is indexed over 2408 a list of dimensions, each associated with an exponent number. All 2409 together this type can represent any unit that is based directly or 2410 indirectly from the base dimensions defined in the "Dimension" type. 2412 Denominate numbers are constructed by passing a tuple made of a 2413 number (either an "Integer" or a "Double") and a unit to the "cast" 2414 function. E.g., "cast (5, megabit)" will build the denominate number 2415 5 with the "megabit" unit. 2417 Dimensionless denominate numbers can be constructed by using the 2418 "none" unit, as in "cast (10, none)" 2420 Denominate numbers can be converted back into a tuple with the 2421 "fromDenominate" function. 2423 Denominate numbers can be added, subtracted or negated (respectively 2424 "+", "-", and "neg"). All these operations can only be done on 2425 denominate numbers with the same exact dimension, and the result will 2426 also carry the same dimension. This prevents what is colloquially 2427 known as mixing apples and oranges. 2429 For the same reason, adding a number to a non-dimensionless 2430 denominate number is equally impossible. 2432 The "*", "/", and "recip" operations respectively multiply, divide 2433 and calculate the reciprocal of denominate numbers. These operations 2434 can be done on denominate number that have different types, and the 2435 result dimension will be derived from the dimension of the arguments. 2436 E.g. multiplying "cast (5, meter)" by "cast (6, meter)" will return 2437 the equivalent of "cast (30, meter * meter)". 2439 Also multiplying a denominate number by a (dimensionless) number is 2440 possible e.g., as in multiplying "cast (5, meter)" by "cast (10, 2441 none)", which will return the equivalent of "cast (50, meter)". 2443 Ultimately we want to insert in a computerate specification the value 2444 of a denominate number, together with its unit, as text, which is 2445 done by implementing the "Show" interface on a denominate number in 2446 its tuple form. E.g. "fromDenominate (cast (5, meter / second)) 2447 (kilometer / hour)" can be directly inserted in a document and will 2448 be substituted with the string "18 km/h". 2450 For each dimension we define a list of constants that represents 2451 units of that dimension. Units that uses a prefix are automatically 2452 generated, which is the case for SI units for the "Time" dimension 2453 (i.e., from "yoctosecond" to "yottasecond"), SI units (only positive 2454 powers of 10) for the "Data" dimension (i.e., from "kilobit" to 2455 "yottabit"), and IEC units (positive powers of 2) for the "Data" 2456 dimension (i.e., from "kibibit" to "yobibit"). 2458 Additional constants like "minute", "hour", "day", "byte", "wyde", 2459 "tetra", "octa", etc, complement the standard units. The "byte", 2460 "wyde", "tetra", and "octa" units are defined in page 4 of [TAOCP]. 2462 8.1.5. BitDiagram 2464 A bit diagram displays a graphical representation of a data layout at 2465 the bit level. 2467 The "BitDiagram" type is used to build BitDiagrams values. 2469 The "toAsciiDoc" function converts a "BitDiagram" value into an 2470 AsciiDoc Literal Block which can be inserted directly in the 2471 document. 2473 Adhoc types can also be used to generate a bit diagram, by passing 2474 that type to the "toDiagram" function and the returned value to the 2475 "toAsciiDoc" function. The "toDiagram" function will build a field 2476 only for types that have an implementation for the "Size" interface. 2477 The function "toDiagram" also takes an auxiliary Type "Names" that 2478 associate names with these types. 2480 8.1.6. Transform 2482 This module permits to manipulate values that are in the very generic 2483 form of trees. These manipulations consist of removing, or replacing 2484 a selected value or values in that tree. 2486 The values to manipulate are selected using a path, which is a series 2487 of instructions used to move the focus of the manipulation up, down 2488 and sideway in the tree and to apply a predicate until a set of 2489 values are chosen. 2491 The values selected are then either removed or replaced by a new 2492 value. The rest of the tree stays unmodified. 2494 This mechanism is very generic and can be applied to any tree, but it 2495 is meant to modify the types defined in the 2496 "Language.Reflection.TTImp" and "Language.Reflection.TT" standard 2497 modules, with the goal of generating types that are derived from 2498 existing types. 2500 8.1.7. Tpn 2502 This module permits to build Petri Nets and then derive types from 2503 that Petri net, types that can be used to ensure that a protocol 2504 implementation follows that Petri Net. 2506 8.2. Meta-Language Packages 2508 8.2.1. Augmented Packet Header Diagrams (APHD) 2510 The "augmented-ascii-diagram" Idris package provides a set of modules 2511 that permits to generate parts of AsciiDoc documents that are conform 2512 to the [I-D.mcquistin-augmented-ascii-diagrams] specification. 2514 The "AAD.Pdu" type is used to define a PDU. 2516 8.2.2. RFC 5234 (ABNF) 2518 TBD. 2520 8.3. Protocol Packages 2522 8.3.1. RFC 791 (Internet Protocol) 2524 TBD. 2526 9. Bibliography 2528 [AsciiBib] "AsciiBib", . 2530 [AsciiDoc] "AsciiDoc", . 2532 [Asciidoctor] 2533 "Asciidoctor", . 2535 [Blockquotes] 2536 "Markdown-style blockquotes", 2537 . 2540 [Brinkmann02] 2541 Brinkmann, R. and R. Drechsler, "RTL-datapath verification 2542 using integer linear programming", In Proceedings of the 2543 2002 Asia and South Pacific Design Automation Conference. 2544 IEEE Computer Society, 2002, 2545 . 2547 [CPN] Jensen, K. and L. Kristensen, "Coloured Petri Nets: 2548 Modelling and Validation of Concurrent Systems", Springer 2549 Dordrecht ; New York, 2009. 2551 [Curry-Howard] 2552 "Curry-Howard correspondence", 2553 . 2556 [Elab] Christiansen, D. and E. Brady, "Elaborator reflection: 2557 extending Idris in Idris", In Proceedings of the 21st ACM 2558 SIGPLAN International Conference on Functional 2559 Programming. ACM Press-Association for Computing 2560 Machinery, 2016, . 2564 [I-D.bortzmeyer-language-state-machines] 2565 Bortzmeyer, S., "Cosmogol: a language to describe finite 2566 state machines", Work in Progress, Internet-Draft, draft- 2567 bortzmeyer-language-state-machines-01, November 1, 2006, 2568 . 2571 [I-D.mcquistin-augmented-ascii-diagrams] 2572 McQuistin, S., Band, V., Jacob, D., and C. Perkins, 2573 "Describing Protocol Data Units with Augmented Packet 2574 Header Diagrams", Work in Progress, Internet-Draft, draft- 2575 mcquistin-augmented-ascii-diagrams-06, July 1, 2020, 2576 . 2579 [I-D.ribose-asciirfc] 2580 Tse, R., Nicholas, N., and P. Brasolin, "AsciiRFC: 2581 Authoring Internet-Drafts And RFCs Using AsciiDoc", Work 2582 in Progress, Internet-Draft, draft-ribose-asciirfc-08, 2583 April 1, 2018, . 2586 [Idris2] "Idris2: A Language with Dependent Types", 2587 . 2589 [Knuth92] Knuth, D., "Literate Programming", Center for the Study of 2590 Language and Information, 1992. 2592 [Kroening16] 2593 Kroening, D. and O. Strichman, "Decision Procedures: An 2594 Algorithmic Point of View", Springer Berlin, 2017. 2596 [Linear-Resources] 2597 "Linear Resources", 2598 . 2600 [Literate] "Literate Programming", 2601 . 2604 [Metanorma] 2605 "Metanorma", . 2607 [Metanorma-IETF] 2608 "Metanorma-IETF", 2609 . 2611 [Momot16] Momot, F., Bratus, S., Hallberg, S., and M. Patterson, 2612 "The Seven Turrets of Babel: A Taxonomy of LangSec Errors 2613 and How to Expunge Them.", In: 2016 IEEE Cybersecurity 2614 Development (SecDev), 2016, 2615 . 2617 [RFC-Guide] 2618 "RFC Style Guide", 2619 . 2621 [RFC0791] Postel, J., "Internet Protocol", RFC 0791, 2622 DOI 10.17487/RFC0791, September 1981, 2623 . 2625 [RFC2119] Bradner, S., "Key words for use in RFCs to Indicate 2626 Requirement Levels", BCP 14, RFC 2119, 2627 DOI 10.17487/RFC2119, March 1997, 2628 . 2630 [RFC5234] Crocker, D., Ed. and P. Overell, "Augmented BNF for Syntax 2631 Specifications: ABNF", RFC 5234, DOI 10.17487/RFC5234, 2632 January 2008, . 2634 [RFC5246] Dierks, T. and E. Rescorla, "The Transport Layer Security 2635 (TLS) Protocol Version 1.2", RFC 5246, 2636 DOI 10.17487/RFC5246, August 2008, 2637 . 2639 [RFC761] Postel, J., "DoD standard Transmission Control Protocol", 2640 RFC 0761, DOI 10.17487/RFC0761, January 1980, 2641 . 2643 [RFC7991] Hoffman, P., "The "xml2rfc" Version 3 Vocabulary", 2644 RFC 7991, DOI 10.17487/RFC7991, December 2016, 2645 . 2647 [RFC8446] Rescorla, E., "The Transport Layer Security (TLS) Protocol 2648 Version 1.3", RFC 8446, DOI 10.17487/RFC8446, August 2018, 2649 . 2651 [RFC8489] Petit-Huguenin, M., Salgueiro, G., Rosenberg, J., Wing, 2652 D., Mahy, R., and P. Matthews, "Session Traversal 2653 Utilities for NAT (STUN)", RFC 8489, DOI 10.17487/RFC8489, 2654 February 2020, . 2656 [RFC8656] Reddy, T., Ed., Johnston, A., Ed., Matthews, P., and J. 2657 Rosenberg, "Traversal Using Relays around NAT (TURN): 2658 Relay Extensions to Session Traversal Utilities for NAT 2659 (STUN)", RFC 8656, DOI 10.17487/RFC8656, February 2020, 2660 . 2662 [Stump16] Stump, A., "Verified Functional Programming in Agda", ACM 2663 Books series, 2016. 2665 [TAOCP] Knuth, D., "The Art Of Computer Programming", Addison- 2666 Wesley Pearson Education, 2005. 2668 [TLP5] "Legal Provisions Relating to IETF Documents", 2669 . 2671 [Type-Driven] 2672 Brady, E., "Type-Driven Development with Idris", Manning 2673 Shelter Island, 2017. 2675 [Zave11] Zave, P., "Experiences with Protocol Description", 2676 Workshop on Rigorous Protocol Engineering (WRiPE'11), 2677 2011, . 2681 Appendix A. Command Line Tools 2683 A.1. Installation 2685 The computerate command line tools are run inside a Docker image, so 2686 the first step is to install the Docker software or verify that it is 2687 up to date (https://docs.docker.com/install/). 2689 Note that for the usage described in this document there is no need 2690 for Docker EE or for having a Docker account. 2692 The following instructions assume a Unix based OS, i.e. Linux or 2693 MacOS. Lines separated by a "\" character are meant to be executed 2694 as one single line, with the "\" character removed. 2696 A.1.1. Download the Docker Image 2698 To install the computerate tools, the fastest way is to download and 2699 install the Docker image using a temporary image containing the dat 2700 tool: 2702 docker pull veggiemonk/dat-docker 2703 mkdir computerate 2704 cd computerate 2705 docker run --rm -u $(id -u):$(id -g) -v \ 2706 $(pwd):/tools veggiemonk/dat-docker dat clone \ 2707 dat://6a33cb289d5818e3709f62e95df41be537edba5f4dc26593e2cb870c7982345b \ 2708 tools 2710 Figure 41 2712 After this, the image can be loaded in Docker. The newly installed 2713 Docker image also contains the dat command, so there is no need to 2714 keep the veggiemonk/dat-docker image after this: 2716 docker load -i tools.tar.xz 2717 docker image rm --force veggiemonk/dat-docker 2719 Figure 42 2721 A new version of the tools is released at the same time a new version 2722 of this document is released. After this, running the following 2723 command in the computerate directory will pull any new version of the 2724 tool tar file: 2726 docker run --rm -u $(id -u):$(id -g) \ 2727 -v $(pwd):/computerate computerate/tools dat pull --exit 2728 Figure 43 2730 The docker image can then be loaded as above. 2732 A.2. The "computerate" Command 2734 The Docker image main command is "computerate", which takes the same 2735 parameters as the "metanorma" command from the Metanorma tooling: 2737 docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ 2738 computerate/tools computerate -t ietf -x txt 2740 Figure 44 2742 The differences with the "metanorma" command are explained in the 2743 following sections. 2745 A.2.1. Literate Files 2747 The "computerate" command can process Literate Idris files (files 2748 with a "lidr" extension, aka lidr files), in addition to AsciiDoc 2749 files (files with an "adoc" extension, aka adoc files). When a lidr 2750 file is processed, all embedded code fragments (text between prefix 2751 "{`" and suffix "`}") are evaluated in the context of the Idris code 2752 contained in this file. Each code fragment (including the prefix and 2753 suffix) are then substituted by the result of that evaluation. 2755 The "computerate" command can process included lidr files in the same 2756 way. The embedded code fragments in the imported file are processed 2757 in the context of the included lidr file, not in the context of the 2758 including file. Idris modules (either from an idr or lidr file) can 2759 be imported the usual way. 2761 The literate code (which is all the text that is starting by a ">" 2762 symbol in column 1) in a lidr file will not be part of the rendered 2763 document. 2765 A.2.2. Transclusions 2767 The "computerate" command can process transclusions, a special form 2768 of AsciiDoc "include" that takes a range of lines as parameters: 2770 2771 include::rfc5234.txt[lines=26..35] 2772 2774 Figure 45 2776 Here the "include" macro will be replaced by the content of lines 26 2777 to 35 (included) of [RFC5234]. 2779 The "sub" parameter permits modifying the copied content according to 2780 a regular expression. For instance the following converts references 2781 into the AsciiDoc format: 2783 2784 include::rfc5234.txt[lines=121..131,sub="/\[([^\]])\]/<<\1>>/"] 2785 2787 Figure 46 2789 In the following example, the text is converted into a note: 2791 2792 include::rfc5234.txt[lines=151,sub="/^.*$/NOTE: \0/"] 2793 2795 Figure 47 2797 A.2.3. IdrisDoc Generation 2799 The "computerate" can include in a document the result of the 2800 generation of the IdrisDoc for a package. This is done by including 2801 a line like this: 2803 2804 include::computerate-specifying.ipkg[leveloffset=+2] 2805 2807 Figure 48 2809 The "leveloffset" attribute is used to adjust the level of the 2810 section generated, as the sections generated always have the level 2. 2812 A.2.4. Outputs 2814 Instead of generating a file based on the name of the input file, the 2815 "computerate" command generates a file based on the ":name:" 2816 attribute in the header of the document. 2818 In addition to the "txt", "html", "xml", and "rfc" output formats 2819 supported by "metanorma", the "computerate" command can also be used 2820 to generate for the "pdf" and "json" formats by using these names 2821 with the "-x" command line parameter. 2823 If the type of document passed to the "computerate" command (options 2824 "-t" or "--type") is one of the following, then the document will be 2825 processed directly using "asciidoctor", and not "metanorma": "html, 2826 "html5, "xhtml", "xhtml5", "docbook", "docbook5", "manpage", "pdf", 2827 and "revealjs". The asciidoctor-diagram extension is available in 2828 this mode with the following supported diagram types: "actdiag", 2829 "blockdiag", "ditaa", "graphviz", "meme", "mscgen", "nwdiag", 2830 "plantuml", and "seqdiag". 2832 A.2.5. Extended Registry 2834 The extended registries are stored and shared in a dat repository. 2836 | NOTE: More to come on the exact mechanism used to share the 2837 | extended repositories. 2839 A.2.6. Bibliography 2841 Because most references are stable, there is not much point in 2842 retrieving them each time the document is processed, even with the 2843 help of a cache, so lookup of external references is disabled. 2845 The following command can be used to fetch an RFC reference: 2847 tools relaton fetch "IETF(RFC.2119)" --type IETF >ietf.xml 2849 Figure 49 2851 Then ietf.xml file needs to be edited by removing the first two 2852 lines. After this the xml file can be converted into a AsciiDoc 2853 document: 2855 tools relaton convert ietf.xml -f asciibib 2857 Figure 50 2859 This will generate an ietf.adoc file that can be copied in the 2860 bibliography section. Note that section level of the bibliographic 2861 item needs to be one up the section level of the bibliography 2862 section. 2864 One exception is a reference to a standard document that is under 2865 development, like an Internet-Draft. 2867 In that case the best way is to have a separate script that fetch, 2868 edit and convert Internet-Drafts as separate files. Then these files 2869 can be inserted dynamically in the bibliography section using 2870 includes. 2872 The command to retrieve an Internet-Draft reference is as follow: 2874 tools relaton fetch "IETF(I-D.bortzmeyer-language-state-machines)" \ 2875 --type IETF >bortzmeyer-language-state-machines.adoc 2877 Figure 51 2879 Additionally the following sections show how to manually format some 2880 common types of bibliographic items, most of then adapted from 2881 [RFC-Guide]. 2883 A.2.6.1. Internet-Draft 2885 2886 [%bibitem] 2887 === {blank} 2888 id:: RFC-STYLE 2889 title.content:: RFC Style Guide 2890 contributor:: 2891 contributor.person.name.completename.content:: Heather Flanagan 2892 contributor.role.type:: author 2893 contributor:: 2894 contributor.person.name.completename.content:: Sandy Ginoza 2895 contributor.role.type:: author 2896 date.type:: published 2897 date.on:: 2014-07-20 2898 link:: 2899 link.type:: TXT 2900 link.content:: https://www.ietf.org/.../draft-flanagan-style-03.txt 2901 docid:: 2902 docid.type:: Work 2903 docid.id:: in Progress 2904 docid:: 2905 docid.type:: Internet-Draft 2906 docid.id:: draft-flanagan-style-03 2907 2909 Figure 52 2911 A.2.6.2. RFC 2912 2913 [%bibitem] 2914 === {blank} 2915 id:: RFC-STYLE2 2916 title.content:: RFC Style Guide 2917 contributor:: 2918 contributor.person.name.completename.content:: Heather Flanagan 2919 contributor.role.type:: author 2920 contributor:: 2921 contributor.person.name.completename.content:: Sandy Ginoza 2922 contributor.role.type:: author 2923 date.type:: published 2924 date.on:: 2014-09 2925 link:: 2926 link.type:: src 2927 link.content:: http://www.rfc-editor.org/info/rfc7322 2928 docid:: 2929 docid.type:: RFC 2930 docid.id:: 7322 2931 docid:: 2932 docid.type:: DOI 2933 docid.id:: 10.17487/RFC7322 2934 2936 Figure 53 2938 A.2.6.3. Email 2940 2941 [%bibitem] 2942 === {blank} 2943 id:: reftag 2944 title.content:: Subject: Subject line 2945 contributor:: 2946 contributor.person.name.completename.content:: A. Sender 2947 contributor.role.type:: author 2948 date.type:: published 2949 date.on:: 2014-09-05 2950 link:: 2951 link.type:: src 2952 link.content:: https://mailarchive.ietf.org/.../Ed4OHwozljyjklpAE/ 2953 docid:: 2954 docid.type:: message to the 2955 docid.id:: listname mailing list 2956 2958 Figure 54 2960 A.2.6.4. IANA 2962 2963 [%bibitem] 2964 === {blank} 2965 id:: IANA-IKE 2966 title.content:: Internet Key Exchange (IKE) Attributes 2967 contributor.person.name.completename.content:: IANA 2968 contributor.role.type:: author 2969 link:: 2970 link.type:: src 2971 link.content:: http://www.iana.org/assignments/ipsec-registry 2972 2974 Figure 55 2976 A.2.6.5. Web-Based Public Code Repositories 2978 2979 [%bibitem] 2980 === {blank} 2981 id:: pysaml2 2982 title.content:: Python implementation of SAML2 2983 date.type:: published 2984 date.on:: 2018-03-01 2985 docid:: 2986 docid.type:: commit 2987 docid.id:: 7135d53 2988 link:: 2989 link.type:: src 2990 link.content:: https://github.com/IdentityPython/pysaml2 2991 2993 Figure 56 2995 A.3. Idris REPL 2997 idr and lidr files can be loaded directly in the Idris REPL for 2998 debugging: 3000 docker run --rm -it -u $(id -u):$(id -g) -v $(pwd):/computerate \ 3001 computerate/tools idris2 3003 Figure 57 3005 It is possible to directly modify the source code in the REPL by 3006 entering the ":e" command, which will load the file in an instance of 3007 VIM preconfigured to interact with the REPL. 3009 The "idris2-vim" add-ons (which provides interactive commands and 3010 syntax coloring) is augmented with a feature that permits to use both 3011 Idris and AsciiDoc syntax coloring. To enable it, add the following 3012 line at the end of all lidr file: 3014 > -- vim:filetype=lidris2.asciidoc 3016 Figure 58 3018 A.4. Other Commands 3020 For convenience, the docker image provides the latest version of the 3021 xml2rfc, aspell, and idnits tools. 3023 docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ 3024 computerate/tools xml2rfc 3025 docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ 3026 computerate/tools idnits --help 3027 docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ 3028 computerate/tools aspell 3030 Figure 59 3032 The Docker image also contains a extended version of git that will be 3033 used to retrieve the computerate specifications as explained in 3034 Appendix A.5. 3036 A.5. Source Repositories 3038 The git repositories that compose the Computerate Specification 3039 Standard Library are distributed over a peer-to-peer protocol based 3040 on dat. 3042 This requires an extension to git, extension that is already 3043 installed in the Docker image described in Appendix A.1. The 3044 following command can be used to retrieve a computerate 3045 specification: 3047 docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ 3048 computerate/tools git clone 3050 Figure 60 3052 When available, the for each package is listed in the 3053 header of the Reference documentation for that package. For the 3054 package in the standard library, these are listed in Appendix B. 3056 Updating the repository also requires using the Docker image: 3058 docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ 3059 computerate/tools git pull 3061 Figure 61 3063 All the git commands that do not require access to the remote can be 3064 run natively or from the Docker image. 3066 Note that for the Computerate Specification Standard Library packages 3067 the "computerate" command must be run from the top level directory in 3068 the git repository. The name of the root document is "Main.adoc" or 3069 "Main.lidr": 3071 docker run --rm -u $(id -u):$(id -g) -v $(pwd):/computerate \ 3072 computerate/tools computerate -t ietf -x txt Main.adoc 3074 Figure 62 3076 A.6. Modified Tools 3078 The following sections list the tools distributed in the Docker image 3079 that have been modified for integration with the "computerate" tool. 3081 A.6.1. Idris2 3083 URL: https://github.com/idris-lang/Idris2.git 3084 Version: 0.2.1 commit cdd0d 3085 Modifications: 3087 * The interactive command ":gc" permits to display the result of an 3088 elaboration. 3089 * The types in TTImp can carry the documentation for the types that 3090 will be generated from them. 3091 * The "%cacheElab" directive permits to cache the result of an 3092 elaboration in the source code instead of been regenerated at each 3093 type-checking. 3094 * A new idris2 wrapper sets the correct mappings for recursive 3095 build. 3096 * "--mkdoc " generates the package documentation in 3097 AsciiDoc on stdout. 3098 * Elaborations can be exported and documented. 3099 * "package" and "depends" in ipkg file can use quoted strings. 3100 * "--depends" lists the dependencies. 3101 * "--map =" maps between a package and a directory. 3102 * "--paths" now displays the paths after modification. 3103 * Fix boolean operators precedence. 3104 * Replace the literate processor by a faster one. Remove support 3105 for reversed Bird marks. 3107 A.6.2. xml2rfc 3109 URL: https://svn.tools.ietf.org/svn/tools/xml2rfc/trunk 3110 Version: 3.0.0 3111 Modifications: 3113 * Always paginate the text output for RFC. 3115 A.6.3. asciidoctor 3117 URL: https://github.com/asciidoctor/asciidoctor.git 3118 Version: 2.0.10 3119 Modifications: 3121 * Process lidr and lipkg files. 3122 * Preprocessor for Idris literate source. 3123 * Include processor for transclusions. 3125 A.6.4. metanorma 3127 URL: https://github.com/metanorma/metanorma 3128 Version: 1.1.5 3129 Modifications: 3131 * Generate the filename from the name header attribute. 3132 * Process files with lidr and lipkg extensions. 3134 A.6.5. metanorma-ietf 3136 URL: https://github.com/metanorma/metanorma-ietf 3137 Version: 2.2.2 3138 Modifications: 3140 * Fix the content of the generated so it is displayed 3141 correctly in html and pdf outputs. 3142 * Fix empty RFC number. 3143 * Add generation of json file. 3144 * Generates DOI, RFC and Internet-Draft references. Truncate the 3145 date according to type. 3146 * Do not add content in xrefs. 3148 A.6.6. relaton-bib 3150 URL: https://github.com/relaton/relaton-bib 3151 Version: 1.3.1 3152 Modifications: 3154 * Add month and day to published year. 3156 A.6.7. git 3158 URL: https://github.com/git/git 3159 Version: 2.20.1 3160 Modifications: 3162 * Remote helper for the dat protocol. 3164 A.6.8. idris2-vim 3166 URL: https://github.com/edwinb/idris2-vim 3167 Version: commit 099129e 3168 Modifications: 3170 * the "IdrisGenerateCache" command (mapped to _z) on a 3171 "%runElab line" displays the result of the elaboration. 3172 * Support for lidris2 files. 3173 * Syntax colouring for document language in lidris2. 3175 A.7. Bugs and Workarounds 3177 Installation: 3179 * The current version of Docker in Ubuntu fails, but this can be 3180 fixed with the following commands: 3182 sudo apt-get install containerd.io=1.2.6-3 3183 sudo systemctl restart docker.service 3185 Figure 63 3187 Idris2: 3189 * :gc is currently broken. 3190 * Docstrings are not generated correctly. 3191 * Interactive commands are missing or not working well with literate 3192 code. 3193 * Changing the installation prefix requires two installations. 3194 * Documentation not generated for namespaces and records. 3195 * Recursive build incomplete. 3197 metanorma: 3199 * Mixup between titles and reference id, even with AsciiBib. The 3200 workaround is to prefix the tile with an underscore and then fix 3201 the generated xml2rfc file. 3203 * RFC and I-D references are not correctly generated by relaton. 3204 The workaround is to remove the IETF docid and to add the 3205 following: 3207 docid:: 3208 docid.type:: BCP 3209 docid.id:: 37 3210 docid:: 3211 docid.type:: RFC 3212 docid.id:: 5237 3214 Figure 64 3216 git: 3218 * Tags are not cloned by dat-remote-helper. 3219 * Commit id are modified. 3220 * Dat storage must be shared between submodules. 3221 * Trying to fetch nonexistent new commits on a git repository will 3222 block for 12 seconds. 3224 computerate: 3226 * code blocks escape a '>' in the first column. The workaround is 3227 to insert a space before the '>'. 3229 A.8. TODO List 3231 Idris2: 3233 * Add documentation support for all types in TTImp. 3234 * ":gc!" should update the file. 3235 * "%cacheElab" should check hashes. 3236 * Add a way to generate a hole name. 3237 * Literate ipkg to merge the Main.adoc and ipkg files. 3239 metanorma: 3241 * Merge bibliographies. 3242 * Extract bibliography from computerate specification. 3243 * Generate xml2rfc element. 3244 * Generate .rfc.xml and err file with the same name. 3245 * Generate rfc.xml as xml and xml under another extension so the 3246 xml2rfc file can be directly submitted to the IETF secretariat. 3248 computerate: 3250 * Generate sourcecode blocks from existing code. 3252 * Pass surrounding line for embedded code so the Asciidoc module can 3253 process constrained elements. 3254 * Implement self-inclusion to reorder a document. 3255 * Backport embedded blocks from Coriander. 3257 vim: 3259 * Starting vim in docker often result in an invalid terminal size 3260 when a file is loaded. Using the following command line solves 3261 the problem: 3263 docker run --rm -it -u $(id -u):$(id -g) -e COLUMNS=$(tput cols) \ 3264 -e LINES=$(tput lines) -v $(pwd):/computerate computerate/tools \ 3265 vim 3267 Figure 65 3269 rfc2adoc: 3271 * This future tool will be able to convert an xml2rfc v3 file into 3272 an AsciiDoc file. It will also be able to update an already 3273 converted file without losing the Idris annotations. 3275 Appendix B. Reference 3277 | NOTE: The code for the libraries described in that section is 3278 | not yet ready to be published. 3280 B.1. Package computerate-specifying 3282 The Builtin Computerate Specification Standard Library. 3284 Version: 0.1 3285 Author(s): Marc Petit-Huguenin 3286 Dependencies: augmented-ascii-diagrams, rfc5234 3288 B.1.1. Module ComputerateSpecifying.AsciiDoc 3290 A module to generate valid AsciiDoc. 3292 data Block : Type 3293 A block of text 3295 Implements Show. 3297 Admonition : Block 3299 Example : Block 3300 Listing : Block 3302 Literal : List String -> Block 3304 Passthrough : Block 3306 Quote : Block 3308 Sidebar : Block 3310 Source : (lang : Maybe String) -> List String -> Block 3312 Stem : Block 3314 Table : Block 3316 Verse : Block 3318 Paragraph : (lines : List Line) -> length lines > 0 = True => 3319 Block 3321 data Inline : Type 3322 A type for inline text. 3324 Lit : String -> Inline 3326 Italic : List Inline -> Inline 3328 Bold : List Inline -> Inline 3330 Subscript : List Inline -> Inline 3332 Superscript : List Inline -> Inline 3334 Monospace : List Inline -> Inline 3336 Highlight : List Inline -> Inline 3338 Custom : String -> List Inline -> Inline 3340 Attribute : String -> Inline 3342 Link : (uri : String) -> (text : List Inline) -> 3343 (attributes : List String) -> Inline 3344 uri: The URI 3345 text: The text 3346 attributes: Additional attributes 3348 Xref : String -> List Inline -> List String -> Inline 3350 Code : String -> Inline 3351 Embedded code. 3353 data Line : Type 3354 MkLine : (inlines : List Inline) -> 3355 length inlines > 0 = True => Line 3357 B.1.2. Module ComputerateSpecifying.BitDiagram 3359 data BitDiagram : List String -> Type 3360 Field : (name : String) -> (size : Nat) -> 3361 size > 0 && size * 2 > length name = True => 3362 BitDiagram names -> elem name names = False => 3363 BitDiagram (name :: names) 3365 Last : (name : String) -> (size : Nat) -> 3366 size > 0 && size * 2 > length name = True => BitDiagram [name] 3368 data Names : Type -> Type 3370 toAsciiDoc : BitDiagram names -> Block 3372 toDiagram : (t : Type) -> Names t -> BitDiagram _ 3374 B.1.3. Module ComputerateSpecifying.BitVector 3376 (++) : BitVector n -> BitVector m -> BitVector (n + m) 3377 Concatene the second bit-vector after the first one. 3379 data Bit : Type 3380 O : Bit 3382 I : Bit 3384 data BitVector : Nat -> Type 3385 A vector of bit that can be pattern matched. 3387 Implements DecEq, Eq, Size. 3389 Nil : BitVector Z 3391 (::) : Bit -> BitVector n -> BitVector (S n) 3393 and : BitVector m -> BitVector m -> BitVector m 3394 Bitwise and between bit-vectors of identical size. 3396 bitVector : {m : Nat} -> BitVector m 3397 Build an empty bit-vector 3399 extend : (n : Nat) -> BitVector m -> BitVector (plus n m) 3400 Extend a bit-vector by n zero bits on the left side. 3402 extract : (p : Nat) -> (q : Nat) -> (prf1 : p LTE q) => 3403 BitVector m -> (prf2 : q LTE m) => BitVector (q minus p) 3404 Extract a bit-vector. 3406 p: The position of the first bit to extract. 3407 q: The position of the next to last bit to extract. 3409 not : BitVector m -> BitVector m 3410 Bitwise not of a bit-vector. 3412 or : BitVector m -> BitVector m -> BitVector m 3413 Bitwise or between bit-vector of identical size. 3415 shiftL : (n : Nat) -> BitVector m -> (prf : n LTE m) => 3416 BitVector (plus (minus m n) n) 3417 Shift the bit-vector to the left by n bits, inserting zeros. 3419 shiftR : (n : Nat) -> {m : Nat} -> BitVector m -> 3420 (prf : n LTE m) => BitVector (plus (minus m n) n) 3421 Shift the bit-vector to the right by n bits, inserting zeros. 3423 test : (m : Nat) -> BitVector n -> (prf : m LT n) => Bool 3424 Return a boolean that is True if the bit at position m is set. 3426 xor : BitVector m -> BitVector m -> BitVector m 3427 Bitwise xor between bit-vectors of identical size. 3429 B.1.4. Module ComputerateSpecifying.Dimension 3431 A module that defines types, constants and operations on denominate 3432 numbers. 3434 (*) : Denominate xs -> Denominate ys -> Denominate (merge' xs ys) 3435 The multiplication operation between denominate numbers. 3437 (+) : Denominate xs -> Denominate xs -> Denominate xs 3438 The addition operation between denominate numbers. 3440 (-) : Denominate xs -> Denominate xs -> Denominate xs 3441 The subtraction operation between denominate numbers. 3443 (/) : Denominate xs -> Denominate ys -> 3444 Denominate (merge' xs (recip' ys)) 3445 The division operation between denominate numbers. 3447 Data : Type 3448 The type of a denominate number for the data dimension. 3450 data Denominate : List (Dimension, Int) -> Type 3451 A denominate number. 3453 MkDenominate : (x : Integer) -> (y : Integer) -> 3454 {xs : List (Dimension, Int)} -> Denominate xs 3455 Construct a denominate number as a fraction. 3457 Dimensionless : Type 3458 The type of a dimensionless denominate number 3460 interface Size a 3461 An interface to retrieve the size in bits of a type. 3463 Implemented by List, (s, x). 3465 size : a -> Data 3466 Return the size of a in bit. 3468 Time : Type 3469 The type of a denominate number for the time dimension. 3471 bit : Data 3472 Bit, the base unit of data. 3474 byte : Data 3475 The byte unit, as 8 bits. 3477 day : Time 3478 The day, as unit of time. 3480 fromDenominate : (value : Denominate xs) -> 3481 (unit : Denominate xs) -> (Double, Denominate xs) 3482 Convert a denominate number into a tuple made of the dimensionless 3483 value (as a "Double") calculated after applying a unit, and that 3484 unit. 3486 value: the value to convert. 3487 unit: the unit to use for the conversion. 3489 elaboration generate bin "bit" "Data" 3490 Generate all the IEC units based on the bit, from kibibit to 3491 yobibit. 3493 elaboration generate dec "bit" "Data" 3494 Generate all the SI units based on the bit, from kilobit to 3495 yottabit. 3497 elaboration generate si "second" "Time" 3498 Generates all the SI units based on the second, from yoctosecond 3499 to yottasecond. 3501 hour : Time 3502 The hour, as unit of time. 3504 minute : Time 3505 The minute, as unit of time. 3507 neg : Denominate xs -> Denominate xs 3508 The negation operation of a denominate number. 3510 none : Dimensionless 3511 The unit for a dimensionless denominate number. 3513 octa : Data 3514 The octa unit, as 64 bits. 3516 recip : Denominate xs -> Denominate (recip' xs) 3517 The reciprocal operation of a denominate number. 3519 second : Time 3520 Second, the base unit of time. 3522 tetra : Data 3523 The tetra unit, as 32 bits. 3525 wyde : Data 3526 The wyde unit, as 16 bits. 3528 B.1.5. Module ComputerateSpecifying.Tpn 3530 A module that defines types for Petri Net. 3532 Colour : Place -> Type 3533 Retrieve the type of token that can be stored in the place. 3535 data Input : Type 3536 MkInput : (place : Place) -> (output : Type) -> 3537 (inscription : Colour place -> ND output) -> Input 3538 An input arc. 3540 place: The place from which tokens are removed. 3541 output: The type of the token extracted. 3542 inscription: A function that chooses and converts the tokens 3543 from the place. 3545 InputType : List Input -> Type 3546 Calculate the combined type of a list of inputs. 3548 MS : Type -> Type 3549 A multiset. 3551 ND : Type -> Type 3552 Non-determinism monad. 3554 data Output : Type 3555 MkOutput : (place : Place) -> (input : Type) -> 3556 (inscription : input -> MS (Colour place)) -> Output 3557 An output arc. 3559 place: The place to which tokens are inserted. 3560 inscription: a function that generates the tokens to be 3561 inserted in the place. 3563 OutputType : List Output -> Type 3564 Calculate the combined type of a list of outputs. 3566 data Place : Type 3567 MkPlace : String -> (colour : Type) -> 3568 (init : () -> MS colour) -> Place 3569 A place. 3571 colour: The type of the tokens stored in the place. 3572 init: A function to initialize the place. 3574 data Transition : Type 3575 MkTransition : (inputs : List Input) -> 3576 (outputs : List Output) -> 3577 (transition : InputType inputs -> ND (OutputType outputs)) -> 3578 Transition 3579 A transition. 3581 inputs: The list of inputs. 3582 outputs: The list of outputs. 3583 transition: A function that chooses and converts between a 3584 tuple made of the type of all the inputs into a tuple made 3585 of the type of all the outputs. 3587 Types : List Type -> Type 3588 Convert a list of types into a tuple of types. 3590 B.1.6. Module ComputerateSpecifying.Transform 3592 A module to transform values structured as trees, with specialization 3593 to transform types via elaboration. 3595 data Path : Type 3596 A selection path 3598 add : (tree : a) -> (path : Path) -> (added : b) -> a 3599 Add a value as a sibling to values in a tree that are selected by 3600 a path. 3602 tree: The tree to modify. 3603 path: The path used to select the values. 3604 added: The value to add 3606 extendRegistry : (registry : String) -> (codepoint : String) -> 3607 (type : Decl) -> IO (Provider ()) 3608 Add a binding between a codepoint and a type in an extended 3609 registry 3611 registry: The registry that needs to be extended. 3612 codepoint: The codepoint to bind the type to. 3613 type: The type associated with the codepoint 3615 registry : (registry : String) -> 3616 IO (Provider (List (String, Decl))) 3617 Retrieve an extended registry content, as a list of tuples made of 3618 a codepoint and a type. 3620 registry: The registry to retrieve. 3622 remove : (tree : a) -> (path : Path) -> a 3623 Remove the values in a tree as selected by a path. 3625 tree: The tree to modify. 3626 path: The path used to select the values. 3628 replace : (tree : a) -> (path : Path) -> (replacement : b) -> a 3629 Replace values selected by a path on a tree. 3631 tree: The tree to modify. 3632 path: The path used to select the values. 3633 replacement: The value to used as replacement. 3635 B.1.7. Module ComputerateSpecifying.Unsigned 3637 An unsigned number with a length. 3639 data Unsigned : (m : Nat) -> Type 3640 An unsigned integer is just a wrapper around a bit-vector of the 3641 same size. 3643 For sanity sake, this type always assumes that the value of a bit 3644 is 2 ^ m - 1, with m the size of the unsigned int. In other words 3645 the first bit is the MSB, the last bit (the closer to Nil) is the 3646 LSB. 3648 Implements Num, Integral, Eq, Ord, Size. 3650 MkUnsigned : BitVector m -> Unsigned m 3652 B.2. Package rfc5234 3654 Version: 0.1 3655 Author(s): Marc Petit-Huguenin 3657 B.2.1. Module RFC5234.Core 3659 The ABNF Core rules. 3661 alpha : Rule 3662 An ASCII alphabetic character. 3664 bit : Rule 3665 A "0" or "1" ASCII character. 3667 char : Rule 3668 Any ASCII character, starting at SOH and ending at DEL. 3670 cr : Rule 3671 A Carriage Return ASCII character. 3673 crlf : Rule 3674 A Carriage Return ASCII character, followed by the Line Feed ASCII 3675 character. 3677 ctl : Rule 3678 Any ASCII control character. 3680 digit : Rule 3681 Any ASCII digit. 3683 dquote : Rule 3684 A double-quote ASCII character. 3686 hexdig : Rule 3687 Any hexadecimal ASCII character, in lower and upper case. 3689 htab : Rule 3690 A Horizontal Tab ASCII character. 3692 lf : Rule 3693 A Line Feed ASCII character. 3695 lwsp : Rule 3696 A potentially empty string of space, horizontal tab, or line 3697 terminators, that last one followed by a space or horizontal tab. 3699 octet : Rule 3700 A 8-bit value. 3702 sp : Rule 3703 An ASCII space. 3705 vchar : Rule 3706 A printable ASCII character. 3708 wsp : Rule 3709 A potentially empty string of space, or horizontal tab. 3711 B.2.2. Module RFC5234.Main 3713 A module to generate a valid ABNF. 3715 data Form : Type 3716 Implements Show. 3718 TermName : String -> Form 3720 TermHex : Int -> List Int -> Form 3722 TermDec : Int -> List Int -> Form 3724 TermBin : Int -> List Int -> Form 3726 TermString : String -> Form 3728 Concat : Form -> Form -> List Form -> Form 3730 Altern : Form -> Form -> List Form -> Form 3731 TermHexRange : Int -> Int -> Form 3733 TermDecRange : Int -> Int -> Form 3735 TermBinRange : Int -> Int -> Form 3737 Group : Form -> Form 3739 Repeat : Maybe Int -> Maybe Int -> Form -> Form 3741 Optional : Form -> Form 3743 data Rule : Type 3744 An ABNF rule. 3746 Implements Show. 3748 Eq : (name : String) -> (form : Form) -> Rule 3749 Construct a rule. 3751 Inc : String -> Form -> Rule 3752 Construct an incremental rule. 3754 data Syntax : Type 3755 A list of rules. 3757 Implements Show. 3759 MkSyntax : List Rule -> Syntax 3761 B.3. Package augmented-ascii-diagrams 3763 Version: 0.1 3764 Author(s): Marc Petit-Huguenin 3765 Dependencies: rfc5234 3767 B.3.1. Module AAD.Main 3769 A module to generate augmented packet header diagrams. 3771 data BoolExpr : List Name -> Type 3772 A boolean expression 3774 Implements ShowPrec, Show. 3776 Equ : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) 3778 Neq : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) 3779 Gt : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) 3781 Gte : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) 3783 Lt : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) 3785 Lte : Expr xs -> Expr ys -> BoolExpr (xs ++ ys) 3787 And : BoolExpr xs -> BoolExpr ys -> BoolExpr (xs ++ ys) 3789 Or : BoolExpr xs -> BoolExpr ys -> BoolExpr (xs ++ ys) 3791 Not : BoolExpr xs -> BoolExpr xs 3793 data Expr : List Name -> Type 3794 An expression 3796 Implements ShowPrec, Show. 3798 Val : Nat -> Expr [] 3800 Var : (n : Name) -> Expr [n] 3802 Mul : Expr xs -> Expr ys -> Expr (xs ++ ys) 3804 Div : Expr xs -> Expr ys -> Expr (xs ++ ys) 3806 Mod : Expr xs -> Expr ys -> Expr (xs ++ ys) 3808 Exp : Expr xs -> Expr ys -> Expr (xs ++ ys) 3810 Add : Expr xs -> Expr ys -> Expr (xs ++ ys) 3812 Sub : Expr xs -> Expr ys -> Expr (xs ++ ys) 3814 ITE : BoolExpr xs -> Expr ys -> Expr zs -> 3815 Expr (xs ++ ys ++ zs) 3817 data Name : Type 3818 A name 3820 MkName : Maybe String -> String -> Name 3822 B.4. Package rfc791 3824 Version: 0.1 3825 Author(s): Marc Petit-Huguenin 3826 Dependencies: computerate-specifying 3828 B.4.1. Module RFC791.Address 3830 This module provides types for Internet Protocol Address. 3832 data IP : Type 3833 An IP address. 3835 Implements Size. 3837 A : (h : BitVector 1) -> h = [O] => (net : BitVector 7) -> 3838 (host : BitVector 24) -> IP 3839 A class A address. 3841 B : (h : BitVector 2) -> h = [I, O] => (net : BitVector 14) -> 3842 (host : BitVector 16) -> IP 3843 A class B address. 3845 C : (h : BitVector 3) -> h = [I, I, O] => 3846 (net : BitVector 21) -> (host : BitVector 8) -> IP 3847 A class C address. 3849 B.4.2. Module RFC791.IP 3851 Types for the Internet Protocol. 3853 data Flags : Type 3854 Flags. 3856 Implements Size. 3858 MkFlags : (reserved : BitVector 1) -> reserved = bitVector => 3859 (df : BitVector 1) -> (mf : BitVector 1) -> Flags 3861 data InternetHeader : Type 3862 Internet Protocol Header. 3864 Implements Size. 3866 MkInternetHeader : (version : BitVector 4) -> 3867 version = [O, I, O, O] => (ihl : (Unsigned 4, Data)) -> 3868 snd ihl = tetra => (tos : Tos) -> 3869 (length : (Unsigned 16, Data)) -> snd length = wyde => 3870 (id : Unsigned 16) -> (flags : Flags) -> 3871 (offset : (Unsigned 13, Data)) -> snd offset = octa => 3872 (ttl : (Unsigned 8, Time)) -> snd ttl = second => 3873 (protocol : BitVector 16) -> (checksum : BitVector 16) -> 3874 (source : IP) -> (dest : IP) -> (options : List Option) -> 3875 (padding : BitVector n) -> InternetHeader 3877 data Option : Type 3878 Internet Protocol Header Options. 3880 Implements Size. 3882 Eoo : (flag : BitVector 1) -> flag = [O] => 3883 (class : BitVector 2) -> class = [O, O] => 3884 (number : BitVector 5) -> number = [O, O, O, O, O] => Option 3885 End of Options. 3887 Noop : (flag : BitVector 1) -> flag = [O] => 3888 (class : BitVector 2) -> class = [O, O] => 3889 (number : BitVector 5) -> number = [O, O, O, I, O] => Option 3890 No operation. 3892 Security : (flag : BitVector 1) -> flag = [I] => 3893 (class : BitVector 2) -> class = [O, O] => 3894 (number : BitVector 5) -> number = [O, O, O, I, O] => 3895 (length : Unsigned 8) -> length = 11 => (s : BitVector 16) -> 3896 (c : BitVector 16) -> (h : BitVector 16) -> 3897 (tcc : BitVector 24) -> Option 3898 Security Option. 3900 Lssr : (flag : BitVector 1) -> flag = [I] => 3901 (class : BitVector 2) -> class = [O, O] => 3902 (number : BitVector 5) -> number = [O, O, O, I, I] => 3903 (length : Unsigned 8) -> (pointer : Unsigned 8) -> 3904 pointer >= 4 = True => Option 3905 Loose Source and Record Route Option. 3907 data Tos : Type 3908 Type of Service 3910 Implements Size. 3912 MkTos : (precedence : Unsigned 3) -> (delay : BitVector 1) -> 3913 (throughput : BitVector 1) -> (reliability : BitVector 1) -> 3914 (reserved : BitVector 2) -> reserved = bitVector => Tos 3916 internetHeader : List Decl 3918 Appendix C. Errata Statistics 3920 In an effort to quantify the potential benefits of using formal 3921 methods at the IETF, an effort to relabel the Errata database is 3922 under way. 3924 The relabeling uses the following labels: 3926 +==========+==============================================+ 3927 | Label | Description | 3928 +==========+==============================================+ 3929 | AAD | Error in an ASCII bit diagram | 3930 +----------+----------------------------------------------+ 3931 | ABNF | Error in an ABNF | 3932 +----------+----------------------------------------------+ 3933 | Absent | The errata was probably removed | 3934 +----------+----------------------------------------------+ 3935 | ASN.1 | Error in ASN.1 | 3936 +----------+----------------------------------------------+ 3937 | C | Error in C code | 3938 +----------+----------------------------------------------+ 3939 | Diagram | Error in a generic diagram | 3940 +----------+----------------------------------------------+ 3941 | Example | An example does not match the normative text | 3942 +----------+----------------------------------------------+ 3943 | Formula | Error preventable by using Idris code | 3944 +----------+----------------------------------------------+ 3945 | FSM | Error in a State machine | 3946 +----------+----------------------------------------------+ 3947 | Ladder | Error in a ladder diagram | 3948 +----------+----------------------------------------------+ 3949 | Rejected | The erratum was rejected | 3950 +----------+----------------------------------------------+ 3951 | Text | Error in the text itself, no remedy | 3952 +----------+----------------------------------------------+ 3953 | TLS | Error in the TLS language | 3954 +----------+----------------------------------------------+ 3955 | XML | Error in an XML Schema | 3956 +----------+----------------------------------------------+ 3958 Table 1 3960 At the time of publication the first 1600 errata, which represents 3961 25.93% of the total, have been relabeled. On these, 135 were 3962 rejected and 51 were deleted, leaving 1414 valid errata. 3964 +=========+=======+============+ 3965 | Label | Count | Percentage | 3966 +=========+=======+============+ 3967 | Text | 977 | 69.09% | 3968 +---------+-------+------------+ 3969 | Formula | 118 | 8.34% | 3970 +---------+-------+------------+ 3971 | Example | 112 | 7.92% | 3972 +---------+-------+------------+ 3973 | ABNF | 71 | 5.02% | 3974 +---------+-------+------------+ 3975 | AAD | 49 | 3.46% | 3976 +---------+-------+------------+ 3977 | ASN.1 | 40 | 2.82% | 3978 +---------+-------+------------+ 3979 | C | 13 | 0.91% | 3980 +---------+-------+------------+ 3981 | FSM | 13 | 0.91% | 3982 +---------+-------+------------+ 3983 | XML | 12 | 0.84% | 3984 +---------+-------+------------+ 3985 | Diagram | 6 | 0.42% | 3986 +---------+-------+------------+ 3987 | TLS | 2 | 0.14% | 3988 +---------+-------+------------+ 3989 | Ladder | 1 | 0.07% | 3990 +---------+-------+------------+ 3992 Table 2 3994 Note that as the relabeling is done in in order of erratum number, at 3995 this point it covers mostly older RFCs. A change in tooling (e.g. 3996 ABNF verifiers) means that these numbers may drastically change as 3997 more errata are relabeled. But at this point it seems that 31.89% of 3998 errata could have been prevented with a more pervasive use of formal 3999 methods. 4001 Acknowledgements 4003 Thanks to Jim Kleck, Eric Petit-Huguenin, Nicolas Gironi, Stephen 4004 McQuistin, and Greg Skinner for the comments, suggestions, questions, 4005 and testing that helped improve this document and its associated 4006 tooling. 4008 Thanks to Ronald Tse and the Ribose team for the metanorma and 4009 relaton tools and their diligence in fixing bugs and implementing 4010 improvements. 4012 Contributors 4014 Stephane Bryant 4016 Email: stephane.ml.bryant@gmail.com 4018 Changelog 4020 draft-petithuguenin-computerate-specifying-04: 4022 * Document: 4023 - Sections 2, 3, 4 and 5 have been completely reorganized, 4024 edited, and extended as a tutorial. 4025 - New Terminology section. 4026 - Add a new Standard Library section, that contains the 4027 description of all the Idris modules and external packages that 4028 will be available for developing specifications. 4029 - Improve bibliography. 4030 - Extend the CLI section to cover: 4031 o New features. 4032 o Bibliography templates. 4033 o Complete bugs and TODO lists. 4034 - Generate IdrisDoc of standard library packages and modules as a 4035 new appendix. 4036 - Update errata stats. 4037 - More compact changelog. 4038 - Many modifications following Stephane's reviews. 4040 * Tooling: 4041 - Additional metanorma features: 4042 o Generate json file. 4043 - Various bug fixes in metanorma and relaton. 4044 - Additional Idris2 features: 4045 o Generate elaboration cache command. 4046 o Elaboration cache implementation. 4047 o IdrisDoc generation. 4048 o Some TTImp types can carry comments. 4049 o Quoted package names in ipkg. 4050 o List dependencies. 4051 o Package mapping. 4052 o Faster literate processing. 4053 - Idris2 wrapper to load local packages. 4054 - New include processor to generate IdrisDoc. 4055 - Process multiple fragments on each line. 4056 - Add support for asciidoctor outputs, including revealjs and 4057 diagrams. 4059 - Embedding code must now return a value that implements "Show". 4060 String values are then stripped of their first and last double- 4061 quotes. 4062 - Fix bug where transcluded text is converted into ASCII art. 4063 - Embedded code in examples in lidr files can now be escaped with 4064 "\". 4065 - Replace Idris with Idris2 version 0.2.1. 4066 - Update metanorma to 1.1.4. 4067 - Update metanorma-ietf to 2.2.2. 4068 - Update xml2rfc to 3.0.0. 4069 - Downgrade idnits to 2.16.04. 4070 - Decommission the Docker image in dat://78f80c850af509e0cd3fd7bd 4071 6f5d0dd527a861d783e05574bbd040f0502da3c6. 4072 * Library: 4073 - Decommission the RFC 5234 library for complete rewrite. 4075 draft-petithuguenin-computerate-specifying-03: 4077 * Document: 4078 - Notes are now correctly displayed. 4079 - Add "Implementations Oriented Standards" section. 4080 - Add "Extended Registries" section and appendix. 4081 - Add paragraph about hierarchical petri nets. 4082 - Convert "Verified Code" section into a top level section, and 4083 expand it. 4084 - Add "Implementation-Oriented Standards" section. 4086 * Tooling: 4087 - Many bug fixes in metanorma-ietf. 4088 - Update xml2rfc to 2.40.1. 4089 - Rebuilding text for an RFC with xml2rfc now uses pagination. 4090 - Update metanorma-ietf to version 2.0.5. 4091 - The "computerate" command can directly generate PDF files. 4092 - Add support in xml2rfc for generating PDF files. 4093 - Add asciidoctor-revealjs. 4094 - Update metanorma to version 1.0.0. 4095 - Update metanorma-cli to version 1.2.10.1. 4097 * Library: 4098 - No update 4100 draft-petithuguenin-computerate-specifying-02: 4102 * Document 4103 - Switch to rfcxml3. 4104 - Status is now experimental. 4105 - Many nits. 4106 - Fix incorrect errata stats. 4108 - Move acknowledgment section at the end. 4109 - Rewrite the APHD section (formerly known as AAD) to match 4110 draft-mcquistin-augmented-diagrams-01. 4111 - Fix non-ascii characters in the references. 4112 - Intermediate AsciiDoc representation for serializers. 4114 * Tooling 4115 - xmlrfc3 is now the default extension. 4116 - "docName" and "category" attributes are now generated, and the 4117 "prepTime" is removed. 4118 - Update xml2rfc to 2.35.0. 4119 - Remove LanguageTool. 4120 - Update Metanorma to version 0.3.17. 4121 - Update Asciidoctor to 2.0.10. 4122 - Update list of Working Groups. 4124 * Library 4125 - No update. 4127 draft-petithuguenin-computerate-specifying-01: 4129 * Document 4130 - New changelog appendix. 4131 - Fix incorrect reference, formatting in Idris code. 4132 - Add option to remove container in all "docker run" command. 4133 - Add explanations to use the Idris REPL and VIM inside the 4134 Docker image. 4135 - Add placeholders for ASN.1 and RELAX NG languages. 4136 - New Errata appendix. 4137 - Nits. 4138 - Improve Syntax Examples section. 4140 * Tooling 4141 - Update Metanorma to version 0.3.16 4142 - Update MetaNorma-cli to version 1.2.7.1 4143 - Switch to patched version of Idris 1.3.2 that supports remote 4144 REPL in Docker. 4145 - Add VIM and idris-vim extension. 4146 - Remove some debug statements. 4148 * Library 4149 - No update 4151 Author's Address 4153 Marc Petit-Huguenin 4154 Impedance Mismatch LLC 4155 Email: marc@petit-huguenin.org