The Computerate Specifying Paradigm

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

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

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

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

where¶

version:

This field is constrained to always contain the value 4.¶

ihl:

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

others:

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

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

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

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

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

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

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

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

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

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

will generate the equivalent AsciiDoc text:¶

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

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

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

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

Inserting a calculation is easy:¶

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

For instance the IP layer is really 4 different functions:¶

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

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

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

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

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

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

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

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

Section 8.1.1 provides a description of the AsciiDoc module.¶

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

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

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

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

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

BitVector:

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

Unsigned:

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

Dimension:

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

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

version:

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

ihl:

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

tos, flags, protocol, source, dest:

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

length:

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

id:

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

offset:

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

ttl:

This is a denominate number with Time as dimension and second as unit.¶

options:

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

padding:

This is a bit-vector whose length is variable.¶

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

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

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

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

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

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

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

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

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

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

Petri Nets are at the intersection of these two techniques. They are typically graphical representations of concurrent processes, but are based on a well-defined mathematical theory. One way to look at Petri Nets is as a way to group multiple state machines together. A Petri Net also has the advantage that the same graph can be reused to derive other Petri Nets, e.g., Timed Petri Nets (that can be used to collect performance metrics) or Stochastic Petri Nets (which can be seen as a way to group multiple Markov chains together).¶

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

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

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

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

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

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

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

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

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

is rendered as¶

See Section 8.2.2 for details on that package.¶

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

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

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

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

and is rendered as:¶

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

At the difference of the AsciiDoc rendering process that tries very hard to render a document in any circumstances, the types in this module are meant to enforce the generation of AsciiDoc that results in valid xml2rfc v3 document.¶

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

The BitDiagram type is used to build BitDiagrams values.¶

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

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

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

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

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

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

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

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

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

TBD.¶

TBD.¶

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

magnet:?xt=urn:btih:11b4d2a4e20bfc8cd8f3ba1ec21881cfeb8f06d9&dn=tools-10.tar.xz¶

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

URL:

https://github.com/idris-lang/Idris2.git¶

Version:

0.4.0 commit 1e8f9b3¶

Modifications:

URL:

https://github.com/asciidoctor/asciidoctor.git¶

Version:

2.0.16¶

Modifications:

URL:

https://github.com/metanorma/metanorma¶

Version:

1.3.9¶

Modifications:

URL:

https://github.com/metanorma/metanorma-ietf¶

Version:

2.3.6¶

Modifications:

URL:

https://github.com/edwinb/idris2-vim¶

Version:

commit 964cebe¶

Modifications:

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

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

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

¶

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

¶

data List' : (ty : List String -> List String -> Type) -> List String -> List String -> Type

Nil : List' ty [] []

¶

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

¶

data Maybe' : (ty : List String -> List String -> Type) -> (ids : List String) -> (refs : List String) -> Type

An optional value indexed by a list of identifiers and a list of references.¶

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

¶

Nothing : Maybe' ty [] []

¶

data BitDiagram : List String -> Type

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

¶

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

¶

data Names : Type -> Type

¶

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

¶

(++) : BitVector n -> BitVector m -> BitVector (n + m)

Concatene the second bit-vector after the first one.¶

data Bit : Type

O : Bit

¶

I : Bit

¶

data BitVector : Nat -> Type

A vector of bit that can be pattern matched.¶

Implements DecEq, Eq, Size.¶

Nil : BitVector Z

¶

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

¶

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

Bitwise and between bit-vectors of identical size.¶

bitVector : {m : Nat} -> BitVector m

Build an empty bit-vector¶

m:

The length of the bitvector¶

extend : (n : Nat) -> BitVector m -> BitVector (plus n m)

Extend a bit-vector by n zero bits on the left side.¶

extract : (p : Nat) -> (q : Nat) -> (prf1 : p `LTE` q) => BitVector m -> (prf2 : q `LTE` m) => BitVector (q `minus` p)

Extract a bit-vector.¶

p:

The position of the first bit to extract.¶

q:

The position of the next to last bit to extract.¶

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

Bitwise not of a bit-vector.¶

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

Bitwise or between bit-vectors of identical size.¶

shiftL : (n : Nat) -> BitVector m -> (prf : n `LTE` m) => BitVector (plus (minus m n) n)

Shift the bit-vector to the left by n bits, inserting zeros.¶

shiftR : (n : Nat) -> {m : Nat} -> BitVector m -> (prf : n `LTE` m) => BitVector (plus (minus m n) n)

Shift the bit-vector to the right by n bits, inserting zeros.¶

test : (1 m : Nat) -> (1 _ : BitVector n) -> (prf : m `LT` n) => Bool

Return a boolean that is True if the bit at position m is set.¶

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

Bitwise xor between bit-vectors of identical size.¶

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

(*) : Denominate xs -> Denominate ys -> Denominate (merge' xs ys)

The multiplication operation between denominate numbers.¶

(+) : Denominate xs -> Denominate xs -> Denominate xs

The addition operation between denominate numbers.¶

(-) : Denominate xs -> Denominate xs -> Denominate xs

The subtraction operation between denominate numbers.¶

(/) : Denominate xs -> Denominate ys -> Denominate (merge' xs (recip' ys))

The division operation between denominate numbers.¶

Data : Type

The type of a denominate number for the data dimension.¶

data Denominate : List (Dimension, Int) -> Type

A denominate number.¶

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

Construct a denominate number as a fraction.¶

Dimensionless : Type

The type of a dimensionless denominate number¶

interface Size a

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

Implemented by List, (s, x).¶

size : a -> Data

Return the size of a in bit.¶

Time : Type

The type of a denominate number for the time dimension.¶

bit : Data

Bit, the base unit of data.¶

byte : Data

The byte unit, as 8 bits.¶

day : Time

The day, as unit of time.¶

fromDenominate : (value : Denominate xs) -> (unit : Denominate xs) -> (Double, Denominate xs)

Convert a denominate number into a tuple made of the dimensionless value (as a Double) calculated after applying a unit, and that unit.¶

value:

the value to convert.¶

unit:

the unit to use for the conversion.¶

elaboration generate bin "bit" "Data"

Generate all the IEC units based on the bit, from kibibit to yobibit.¶

elaboration generate dec "bit" "Data"

Generate all the SI units based on the bit, from kilobit to yottabit.¶

elaboration generate si "second" "Time"

Generates all the SI units based on the second, from yoctosecond to yottasecond.¶

hour : Time

The hour, as unit of time.¶

minute : Time

The minute, as unit of time.¶

neg : Denominate xs -> Denominate xs

The negation operation of a denominate number.¶

none : Dimensionless

The unit for a dimensionless denominate number.¶

octa : Data

The octa unit, as 64 bits.¶

recip : Denominate xs -> Denominate (recip' xs)

The reciprocal operation of a denominate number.¶

second : Time

Second, the base unit of time.¶

tetra : Data

The tetra unit, as 32 bits.¶

wyde : Data

The wyde unit, as 16 bits.¶

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

data Block : Type

A block of text¶

Implements Show.¶

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

¶

data CitationFormat : Type

Implements Show.¶

Of : CitationFormat

¶

Comma : CitationFormat

¶

Parens : CitationFormat

¶

Bare : CitationFormat

¶

data CrossFormat : Type

Implements Eq, Show.¶

Counter : CrossFormat

¶

Title : CrossFormat

¶

Default : CrossFormat

¶

data Inline : Type

Type to build inline elements.¶

Implements Show.¶

Text : String -> Inline

Plain text.¶

Must : Inline

¶

MustNot : Inline

¶

Required : Inline

¶

Shall : Inline

¶

ShallNot : Inline

¶

Should : Inline

¶

ShouldNot : Inline

¶

Recommended : Inline

¶

May : Inline

¶

Optional : Inline

¶

HardBreak : Inline

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

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

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

Comment : (anchor : Maybe String) -> (source : Maybe String) -> {default True display : Bool} -> (content : List Inline) -> Inline

A comment. NOTE: Not currently supported by metanorma-ietf.¶

anchor:

An optional anchor.¶

source:

An optional author for the comment.¶

display:

False to prevent the comment to be rendered.¶

content:

The comment itself.¶

Italic : List Inline -> Inline

A list of inline elements to be rendered in italics.¶

Link : (target : String) -> (text : List Inline) -> Inline

An embedded URI.¶

target:

The URI.¶

text:

Optional text to be rendered.¶

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

An indexed term.¶

Citation : (target : String) -> (fragment : Maybe String) -> {default Of format : CitationFormat} -> (content : Maybe String) -> Inline

A citation, i.e. a crossreference to a bibliographic reference. NOTE: Not currently supported by metanorma-ietf.¶

target:

The anchor for the bibliographic reference.¶

Bold : List Inline -> Inline

A list of inline elements to be rendered in bold.¶

Subscript : List Inline -> Inline

A list of inline elements to be rendered in subscript.¶

Superscript : List Inline -> Inline

A list of inline elements to be rendered in superscript.¶

Monospace : List Inline -> Inline

A list of inline elements to be rendered in monospace.¶

Unicode : Inline

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

Cross : (target : String) -> {default Nothing format : Maybe CrossFormat} -> (content : List Inline) -> Inline

A crossreference to an anchor in this document.¶

target:

The URI.¶

Attribute : String -> Inline

An AsciiDoc attribute¶

A module that defines types for Petri Net.¶

data Direction : Type

The direction of the data exchanged between a port and a socket.¶

In : Direction

¶

Out : Direction

¶

Both : Direction

¶

data Ellipse : Type

An Ellipse (named for its drawing shape) is either a place or a port/socket.¶

Implements Eq.¶

Place : (name : String) -> (type : Type) -> (init : Colist type) -> Ellipse

A place.¶

name:

The name of the Place¶

type:

The type of the tokens stored in the place.¶

init:

The initial content of the place.¶

Port : (name : String) -> (type : Type) -> (dir : Direction) -> Ellipse

A port.¶

name:

The name of the port.¶

type:

The type of the tokens stored in the port.¶

dir:

The direction of the port.¶

data InputArc : Type

MkInputArc : (ellipse : Ellipse) -> (output : Type) -> (inscription : TypeOf ellipse -> Maybe output) -> InputArc

An input arc.¶

ellipse:

The ellipse from which tokens are removed.¶

output:

The type of the tokens after applying the inscription.¶

inscription:

A function that converts the tokens from the place into the output type.¶

InputType : List InputArc -> Type

Calculate the combined type of a list of inputs.¶

data Instance : List Ellipse -> Type

A module instance.¶

MkInstance : (mod : Module xs ys) -> (maps : List Ellipse) -> length ys = length maps => Instance maps

An instance of a module¶

mod:

The module.¶

maps:

The list of mapping between sockets and places or ports.¶

data Marking : Vect k Type -> Type

A marking is a heterogeneous list of place content.¶

Nil : Marking []

¶

(::) : Colist t -> Marking ts -> Marking (t :: ts)

¶

data Module : (xs : List Ellipse) -> (ys : List Ellipse) -> Type

A module.¶

MkModule : (name : String) -> Module [] []

Build an empty module.¶

AddPlace : (x : Ellipse) -> Module xs ys -> Module (x :: xs) ys

Declare a new place or port local to this module.¶

AddPort : (x : Ellipse) -> Module xs ys -> Module xs (x :: ys)

¶

AddTransition : (t : Transition) -> Module xs ys -> all (\(MkInputArc s _ _) : ? => elem s (xs ++ ys)) (inputs t) = True => all (\(MkOutputArc _ s _) : ? => elem s (xs ++ ys)) (outputs t) = True => Module xs ys

Declare a new transition, checking that the places used are declared in this module.¶

AddInstance : (i : Instance zs) -> Module xs ys -> all (\x : ? => elem x (xs ++ ys)) zs = True => Module xs ys

Declare a new instance of a module, checking that the places used are declared in this module.¶

data OutputArc : Type

MkOutputArc : (input : Type) -> (ellipse : Ellipse) -> (inscription : input -> List (TypeOf ellipse)) -> OutputArc

An output arc.¶

input:

The type of the values from the transition.¶

inscription:

a function that generates the tokens to be inserted in the place.¶

OutputType : List OutputArc -> Type

Calculate the combined type of a list of outputs.¶

data Transition : Type

MkTransition : (name : String) -> (inputs : List InputArc) -> (outputs : List OutputArc) -> (transition : InputType inputs -> Maybe (OutputType outputs)) -> Transition

A transition.¶

name:

The name of the transition¶

inputs:

The list of input arcs.¶

outputs:

The list of output arcs.¶

transition:

A function that chooses and converts between a tuple made of the type of all the inputs into a tuple made of the type of all the outputs.¶

Tuple : List Type -> Type

Convert a list of types into a tuple of types.¶

TypeOf : Ellipse -> Type

Retrieve the type of the tokens that can be stored in an Ellipse.¶

bindings : Marking xs -> Instance [] -> Transition -> Colist Binding

List all the bindings from a marking and a transition.¶

deriveType : Instance [] -> List Decl

¶

empty : Colist a

An empty colist.¶

enabledTransitions : Marking xs -> Instance [] -> List Transition

List all the enabled transitions from a marking.¶

initialMarking : Instance [] -> Marking xs

Builds an initial marking.¶

input : OutputArc -> Type

¶

inputs : Transition -> List InputArc

¶

isSocket : Ellipse -> Bool

¶

mappings : Instance xs -> List Ellipse

¶

output : InputArc -> Type

¶

outputs : Transition -> List OutputArc

¶

transition : Marking xs -> Instance [] -> Transition -> Binding -> Marking xs

Transition to a new marking¶

(|>) : a -> (a -> b) -> b

Chain functions on the opposite direction of `$'.¶

Fixity: Left associative, precedence 0¶

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

data Path : Type

A selection path¶

add : (tree : a) -> (path : Path) -> (added : b) -> a

Add a value as a sibling to values in a tree that are selected by a path.¶

tree:

The tree to modify.¶

path:

The path used to select the values.¶

added:

The value to add¶

extendRegistry : (registry : String) -> (codepoint : String) -> (type : Decl) -> IO (Provider ())

Add a binding between a codepoint and a type in an extended registry¶

registry:

The registry that needs to be extended.¶

codepoint:

The codepoint to bind the type to.¶

type:

The type associated with the codepoint¶

registry : (registry : String) -> IO (Provider (List (String, Decl)))

Retrieve an extended registry content, as a list of tuples made of a codepoint and a type.¶

registry:

The registry to retrieve.¶

remove : (tree : a) -> (path : Path) -> a

Remove the values in a tree as selected by a path.¶

tree:

The tree to modify.¶

path:

The path used to select the values.¶

replace : (tree : a) -> (path : Path) -> (replacement : b) -> a

Replace values selected by a path on a tree.¶

tree:

The tree to modify.¶

path:

The path used to select the values.¶

replacement:

The value to used as replacement.¶

An unsigned number with a length.¶

data Unsigned : (m : Nat) -> Type

An unsigned integer is just a wrapper around a bit-vector of the same size.¶

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

Implements Num, Integral, Eq, Ord, Size.¶

MkUnsigned : BitVector m -> Unsigned m

¶

The ABNF Core rules.¶

alpha : Rule

An ASCII alphabetic character.¶

bit : Rule

A "0" or "1" ASCII character.¶

char : Rule

Any ASCII character, starting at SOH and ending at DEL.¶

cr : Rule

A Carriage Return ASCII character.¶

crlf : Rule

A Carriage Return ASCII character, followed by the Line Feed ASCII character.¶

ctl : Rule

Any ASCII control character.¶

digit : Rule

Any ASCII digit.¶

dquote : Rule

A double-quote ASCII character.¶

hexdig : Rule

Any hexadecimal ASCII character, in lower and upper case.¶

htab : Rule

A Horizontal Tab ASCII character.¶

lf : Rule

A Line Feed ASCII character.¶

lwsp : Rule

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

octet : Rule

A 8-bit value.¶

sp : Rule

An ASCII space.¶

vchar : Rule

A printable ASCII character.¶

wsp : Rule

A potentially empty string of space, or horizontal tab.¶

A module to generate a valid ABNF.¶

data Form : Type

Implements Show.¶

TermName : String -> Form

¶

TermHex : Int -> List Int -> Form

¶

TermDec : Int -> List Int -> Form

¶

TermBin : Int -> List Int -> Form

¶

TermString : String -> Form

¶

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

¶

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

¶

TermHexRange : Int -> Int -> Form

¶

TermDecRange : Int -> Int -> Form

¶

TermBinRange : Int -> Int -> Form

¶

Group : Form -> Form

¶

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

¶

Optional : Form -> Form

¶

data Rule : Type

An ABNF rule.¶

Implements Show.¶

Eq : (name : String) -> (form : Form) -> Rule

Construct a rule.¶

Inc : String -> Form -> Rule

Construct an incremental rule.¶

data Syntax : Type

A list of rules.¶

Implements Show.¶

MkSyntax : List Rule -> Syntax

¶

A module to generate augmented packet header diagrams.¶

data BoolExpr : List Name -> Type

A boolean expression¶

Implements ShowPrec, Show.¶

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

¶

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

¶

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

¶

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

¶

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

¶

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

¶

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

¶

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

¶

Not : BoolExpr xs -> BoolExpr xs

¶

data Expr : List Name -> Type

An expression¶

Implements ShowPrec, Show.¶

Val : Nat -> Expr []

¶

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

¶

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

¶

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

¶

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

¶

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

¶

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

¶

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

¶

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

¶

data Name : Type

A name¶

MkName : Maybe String -> String -> Name

¶

This module provides types for Internet Protocol Address.¶

data IP : Type

An IP address.¶

Implements Size.¶

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

A class A address.¶

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

A class B address.¶

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

A class C address.¶

Types for the Internet Protocol.¶

data Flags : Type

Flags.¶

Implements Size.¶

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

¶

data InternetHeader : Type

Internet Protocol Header.¶

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

¶

data Option : Type

Internet Protocol Header Options.¶

Implements Size.¶

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

End of Options.¶

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

No operation.¶

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

Security Option.¶

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

Loose Source and Record Route Option.¶

data Tos : Type

Type of Service¶

Implements Size.¶

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

¶

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

¶

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

TBD.¶

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

Each TPN input arc is a value of type InputArc with a constructor that takes 3 parameters: a place, a type, and the function that converts the inscription.¶

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

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

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

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

Each TPN output arc is a value of type OutputArc with a constructor that takes 3 parameters: The domain of the function, a place, and the function that acts as the inscription.¶

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

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

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

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

Each free variable in a CPN transition must be converted into a new place, a new input arc, and a new output arc.¶

The new place is of the type of the variable, and its initial content is all the possible values for that type.¶

The new input arc uses the new place, the same type than the place, and its function is pure.¶

The new output arc uses the same type than the place, the new place, and its function is also pure.¶

Note that places with the same type must not be shared between input arcs that are connected to the same transition.¶

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

TBD.¶

TBD.¶

TBD.¶

TBD.¶

TBD.¶

TBD.¶

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

We can encode this in the Idris type system:¶

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

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

The evidence is easy to find:¶

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

We also touched on the fact that our programming language must be less powerful than usual, and it is also related to the answer No.¶

An implication to a type that contains at least one value is a function that returns that value. But there is two cases where that function could not return that value, and thus acts as if the returned type is empty, and thus represents No instead of Yes.¶

The first case is if the function crashes because it does not know how to handle the value passed as parameter. A simple example example would be a function that divide 1 by the parameter - if the parameter is zero then the function will crashes and for the purpose of our interpretation is equivalent to an evidence of No because no value will be returned. To prevent that problem our programming language should be covering all inputs values, i.e. not typecheck if there is cases not covered.¶

The second case is when, for some reason, the code get stuck inside the function e.g., because of an infinite loop. That would again be equivalent to an evidence of No.¶

Idris prevents these two cases by using the total keyword, which basically turns Idris into a non-Turing Complete language.¶

Note that there is no way to possibility to write code that will detect for any possible code if it will loop or not. That's why Idris may reject some code that will not loop, but it will never accept code that will loop.¶

Because there is not much difference between a No answer without evidence and not finding an answer, it's often useful to check and recheck that the question really expresses what we intended.¶

In the previous section we showed that syllogisms always have an answer of Yes. There is a series of fallacies [Bennett15] that are closely related to syllogisms, and here's one of them:¶

That can be read as "Assuming Socrates is a Human, and assuming that all Mortal are Humans, then is Socrates a Mortal?" It may seems obvious that we cannot answer that question, so we may be able to get a No answer by rewriting the question that way:¶

But in spite of our efforts, we cannot provide an evidence of that, which means that it is time to look closer at our question.¶

The issue is that for this to be a fallacy, we need to assume that there is no evidence that all Humans are Mortals, which the previous question does not say. With this modified question, we can now produce a evidence that it is indeed a fallacy:¶

The Product type permits to combine two or more questions such as the question represented by this type will have an answer of Yes only if all the questions also have an answer of Yes.¶

The simplest Product type in Idris is the tuple, which is represented as a list of types separated by commas and enclosed in parentheses:¶

The evidence has the same form as the type.¶

We can also provide evidence that the form above is equivalent to its curried form in general, and vice-versa:¶

The Sum type is a way to combine two or more questions such as the question represented by the Sum type will have an answer of Yes if at least one of the questions have an answer of Yes.¶

The simplest Sum type for two questions in Idris is Either a b.¶

We can combine Sum and Product types to reorganize a question and show evidence that the answer is general.¶

Sum and Product combined with negation gives us more general answers:¶

TBD.¶

TBD.¶

TBD.¶

TBD.¶

TBD.¶

Among all transport protocols that can be used to fetch commits, the Git protocol is the fastest as it runs directly over a TCP connection. It is directly implemented by the git daemon command. For this reason it is the best choice to make public a git repository in read-only mode.¶

But, although everyone can fetch commits from such a repository, the transfer of the commits themselves is not encrypted. The gits transport protocol solves that issue by replacing the TCP connection by a TLS connection. On the client side, the remote helper git-remote-gits is provided as part of the tooling. On the server side, the simplest solution is to use stunnel together with git daemon.¶

The mgit protocol provides an indirection to a list of git URLs, all pointing to identical mirrors of the same repository. An mgit URL provides scalability, reliability, and the ability of adding and removing git mirrors without having to changing the URL itself. Note that mirrors can use any kind of git URL (http, ssh, git, etc...​), including gits URLs.¶

An mgit URL has the format "mgit://<random>", where <random> is a 40 hexadecimal characters string. Such URL is very stable, and can be published in a document for the purpose of retrieving the git repository holding the computerate specification that was used to generate that document.¶

Internally that string is used as the index to store the list of URLs pointing to the git mirrors in a RELOAD [RFC6940] P2P Overlay. Note that storing such list of URLs in the overlay requires credentials.¶

The remote helper git-remote-mgit is provided as part of the tooling. When used to fetch commit, it first contacts the overlay to retrieve the list of mirrors, then choose one randomly and fetch the commits from there. If the mirror does not respond, then another mirror is randomly selected from the list, until all mirrors have be tried.¶

The 'git-remote-mgits` remote helper behaves similarly, but always excludes URLs that do not encrypt the transport.¶

A specification is a set of files that, together, are used as input to a process that generate a document. The subset of Idris files in that set forms an Idris Package. One and only one Idris package is stored per Git repository.¶

For specifications defined by this document, dependencies to other Idris Packages are defined by adding the Git repositories storing these repositories as Git submodules. This permits to distribute the graph of dependencies between each repository, without requiring a separate way of storing that information. The downside of doing that is that a new commit needs to be created to change the URL of a submodule.¶

In the traditional use of a submodule, 1) the URL to the Git repository together with 2) the commit that needs to be checked out in that repository, are the two pieces of information that are stored.¶

Instead of using a traditional https URL for the submodule, we use an mgits URL which brings a better reliability and availability, together with the ability to add or remove mirrors without having to create a new commit.¶

We are storing binary artifacts in a distributed cache that is colocated with each git repository.¶

Because the size of a cache cannot be unbounded, we need to be able to rebuild any artifact at any time from any commit in a git repository, and ensure that the artifact built for a commit stays the same regardless of when and where it is built.¶

We solve this issue by making all specification builds reproducible. In that context, reproducible means that building binary artifacts now or in 10 years will result in two sets of artifacts that are bit-exact identical.¶

That property permits to identifies each build by the commit-id of the commit of the source that was used to build it.¶

A clear consequence of this is that the Idris compiler and its runtime (chezscheme) should be available as source on the same commit, and should be part of the build. The simplest way to guarantee that is that these tools are also available as git submodules.¶

We use the git-lfs extension storage, when available, to store the binary artifacts.¶

When a build ends successfully, all the artifacts created in the source tree, which are easily recognizable because they are the files that are not already managed by git (ignoring the content of the .gitignore file), are packed in a file (zip, tar...​) and uploaded into the git-lfs server, using the SHA256 hash of the commit-id of the source tree as OID.¶

The first step of a build is to try to retrieve the artifacts from the git-lfs storage, using the current commit-id. If that succeeds, the zip file retrieved is expanded, such as the artifacts are installed in the source tree exactly as they are after a successful build. If that fails then the build proceeds as usual.¶

We are using of one of the properties of a commit-id, which is a hash of the content of a commit, including the date and time, and the commit-id of the previous commit. That property is that a commit-id is a statistically globally unique identifier for the content of that commit, meaning that if the same commit-id lives in different repositories, they will still points to the exact same content. That means that by building an index for all the commit-ids of interest, we can associate each of them with the list of git repositories that contain it.¶

We are doing this indexation again in a distributed way, using the same RELOAD P2P overlay used in Appendix F.1.2.¶

Each time commits for a computerate specification are pushed in a git repository that have a public access, our mgits git remote helper is used as a wrapper for the actual URI:¶

The 'computerate' wrapper stores each commit pushed in the P2P overlay as index, with the gitolite3@example.org:computerate-specifying.git URL in the associated RELOAD Array. If the Array for a specific commit already exist, the URL is added to that Array if the URL is not already there.¶

Before building a submodule, the build process queries the P2P Overlay using the commit-id of the submodule as index. That returns a list of git URLs, each pointing to a git repositories that hold that particular commit. The build process chooses one of these, and tries to download the binary artifacts, as explained in Appendix F.2.2. If the artifacts are not available, the sources files are retrieved from one of the git repositories, and the build is applied to each submodule before building that submodule.¶

The whole process would require to start the typechecking of any specification that is not yet cached by rebuilding the Idris compiler and the chezscheme runtime. This is why it is permitted to pin down some builds in the distributed cache, i.e. they are never candidate for removal, which would make them always available.¶