Subject: [hackathon] Formal Languages at the Hackathon

From: Stephen McQuistin <[email-masked]>
Date: Wed, 6 Nov 2019 10:09:33 +0000

Hi all,

Marc Petit-Huguenin and I are championing formal languages projects at the hackathon in Singapore. Broadly, these
projects seek to improve the quality of standards by using formal and structured languages in specification documents.
These documents can then be parsed by tooling that can, for example, generate parser code or verify properties for the
protocol being specified.

There will be two formal languages projects being worked on: Augmented Packet Header Diagrams and Computerate
Specifying. Details for both projects are available on the Wiki at https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages <https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages>,
but I'll give a brief outline of the Augmented Packet Header Diagrams project here. I'll let Marc describe his
Computerate Specifying project separately.

The Augmented Packet Header Diagram format (draft-mcquistin-augmented-ascii-diagrams) is a consistent packet header
diagram format and accompanying structured text constructs that allow for the parsing process of protocol headers to be
fully specified. This provides support for the automatic generation of parser code, and for other benefits that follow
from being able to use tooling to process packet header diagrams.

Our goal at the hackathon is to improve both the Augmented Packet Header Diagram format itself, by attempting to rewrite
existing I-Ds and RFCs using its syntax, and to improve the tooling, and in particular, its Rust parser generator.

Please join us: we are particularly interested in examples of packet header diagrams that might be challenging to write
in the format our draft describes, and in how our tooling might fit into existing workflows.

I-D: https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams <https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams>
Getting started information: https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages <https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages>

Thanks,

Stephen

---

From: Marc Petit-Huguenin <[email-masked]>
Date: Wed, 6 Nov 2019 03:13:10 -0800

Hello,

Thanks Stephen for the introduction to the formal languages projects at the hackathon.

The Augmented Packet Header Diagrams project and the Computerate Specifying project complement each other.  As Stephen said, the former aims at structuring a document so information can be extracted from it.  The latter aims at generating documents that are correct by construction.

The idea of Computerate Specifying was born out of the frustration of having examples in RFCs that do not match the normative text, but evolved since as a generic framework to verify various properties about the data layout and protocol described by an RFC.  This is done by combining in a single file a document formatting language and a programming language with dependent and linear types.

Our goal at the hackathon is to learn more about the applicability of that technique by converting existing I-Ds so examples are correct by construction, and to improve the tooling used to process these modified I-Ds.

So bring your I-D and join us to rewrite it as a computerate specification that contains examples that are correct by construction, and help us improve the quality of the tooling.

ID: https://datatracker.ietf.org/doc/draft-petithuguenin-computerate-specifying/
Getting started information:  https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages

Additionally we are planning for an informal side meeting in a bar (place to be announced later) on Thursday 21 at 8pm for discussion on the general topic of Formal Languages at the IETF.

Thanks.

-- 
Marc Petit-Huguenin
Email: [email-masked]
Blog: https://marc.petit-huguenin.org
Profile: https://www.linkedin.com/in/petithug

---

From: Lucas Pardue <[email-masked]>
Date: Wed, 6 Nov 2019 11:24:42 +0000

Hello,

The timing of this is quite good because the QUIC WG have recently been
debating the pros and cons of the bitmap diagram for describing packets and
frames particularly for variable-length fields, see issue #3115 [1].

Cheers
Lucas

[1] https://github.com/quicwg/base-drafts/issues/3115

On Wed, Nov 6, 2019 at 10:09 AM Stephen McQuistin <[email-masked]> wrote:

> projects seek to improve the quality of standards by using formal and
> structured languages in specification documents.
> These documents can then be parsed by tooling that can, for example,
> generate parser code or verify properties for the
> Specifying. Details for both projects are available on the Wiki at
> https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages
> ,
> The Augmented Packet Header Diagram format
> (draft-mcquistin-augmented-ascii-diagrams) is a consistent packet header
> diagram format and accompanying structured text constructs that allow for
> the parsing process of protocol headers to be
> fully specified. This provides support for the automatic generation of
> parser code, and for other benefits that follow
> Our goal at the hackathon is to improve both the Augmented Packet Header
> Diagram format itself, by attempting to rewrite
> existing I-Ds and RFCs using its syntax, and to improve the tooling, and
> in particular, its Rust parser generator.
>
> Please join us: we are particularly interested in examples of packet
> header diagrams that might be challenging to write
> I-D:
> https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams
> Getting started information:
> https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages
>
> Thanks,
>
> Stephen
>
>
>
> _______________________________________________
> hackathon mailing list
> [email-masked]
> https://www.ietf.org/mailman/listinfo/hackathon
>

---

From: Kent Watsen <[email-masked]>
Date: Wed, 6 Nov 2019 15:07:19 +0000

I posted an I-D back in February on a similar idea.  The draft refers to YANG modules as an example throughout, but the idea applies equally to any structured format.  The draft does not define a "formal language", so much as define steps for a build-time script, to create self-validating submittable xml2rfc documents.  I haven't picked the project up since due to being busy on other things, but I will again if my chair/shepherd effort-level ever spikes again  ;)

	https://tools.ietf.org/html/draft-kwatsen-git-xiax-automation-01 <https://tools.ietf.org/html/draft-kwatsen-git-xiax-automation-01>

Kent

> On Nov 6, 2019, at 6:24 AM, Lucas Pardue <[email-masked]> wrote:
> 
> Hello,
> 
> The timing of this is quite good because the QUIC WG have recently been debating the pros and cons of the bitmap diagram for describing packets and frames particularly for variable-length fields, see issue #3115 [1].
> 
> Cheers
> Lucas
> 
> [1] https://github.com/quicwg/base-drafts/issues/3115 <https://github.com/quicwg/base-drafts/issues/3115>
> On Wed, Nov 6, 2019 at 10:09 AM Stephen McQuistin <[email-masked] <mailto:[email-masked]>> wrote:
> Hi all,
> 
> [email-masked] <mailto:[email-masked]>
> https://www.ietf.org/mailman/listinfo/hackathon <https://www.ietf.org/mailman/listinfo/hackathon>

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Nov 2019 16:40:11 +0100

I’m sharing the below with t2trg as it appears to be highly related to some of our current work.

I’d also like to point out that formal description techniques (FDT) have been used a lot at the IETF and the IRTF:

* we know very well how to use ABNF (RFC 5234) for our text-based protocols.  We don’t really have a good way to work with multiple layers of ABNF, though; see the difference between RFC 5988 and RFC 8288 for some recent improvements (but the link between the layers is not formal).  ABNF tools exist for both checking ABNF specs and for automatically generating instances (examples).

* specific areas have had their FDTs, e.g. RFC 4997 for ROHC, YANG for management, etc.  Specifically YANG is increasingly used not only for its original purpose, describing management information bases, but also for data on the wire (yang-data).  YOUPI [1] is an interesting YANG extension for describing arbitrary binary data.

[1]: https://tools.ietf.org/html/draft-petrov-t2trg-youpi

* some RFCs were to a large extent machine-generated text (e.g., RFC 7400) or machine-verified (e.g., RFC 8428), based on models in various FDTs.  Some of these are very domain-specific, but we could still be better on sharing tools (and long-term preserving the sources that generated those RFCs).

* there is a lively discussion about adding (structural) data modeling (a.k.a. “schemas”) to JSON over at the mailing list of the closed JSON WG (e.g., [2]).  While that discussion is ongoing, we already have CDDL (RFC 8610) for structurally modeling CBOR and JSON data.  Maybe one size does not fit all here.  Similar to ABNF, CDDL tools can check specs, verify instances against a spec, extract/generate code snippets from specs, and generate instances/examples from specs.  One next step here is adding links to application semantics.

[2]: https://tools.ietf.org/html/draft-ucarion-jddf

* the WISHI activity in T2TRG looks at modeling data shapes, interaction modeling, and potentially adding protocol bindings towards the wire and application semantics towards the application.  Several SDOs are providing interesting study subjects, e.g., W3C WoT with their Thing Description (TD) [3] and the still somewhat stealthy OneDM group with the Simple Definition Format (SDF) [4].  We’ll discuss this on the Friday before the IETF [5] and work on tools for it at the Hackathon (look for “WISHI”).

[3]: https://www.w3.org/TR/wot-thing-description/
[4]: https://github.com/one-data-model/language/blob/master/sdf.md
[5]: https://github.com/t2trg/2019-11-singapore
(Yes, you can still register.)

I understand that the “Formal Languages” activity mostly addresses their use in IETF specifications, and I like that angle — there are other uses of formal description techniques that possible have a different set of requirements, which sometimes cause the requirements of spec writers to be forgotten [6].

[6]: https://www.iab.org/wp-content/IAB-uploads/2016/03/Noise-in-specifications-hurts.pdf

So I’m really looking forward to the discussions on Friday, November 15th [5] and at the Hackathon.  Getting something going on cross-pollinating and coordinating the various FDT activities at IETF and IRTF might be a good medium term goal.

Grüße, Carsten

> On Nov 6, 2019, at 11:09, Stephen McQuistin <[email-masked]> wrote:
> 
> Hi all,
> 
> Specifying. Details for both projects are available on the Wiki at https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages,
> I-D: https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams

---

From: Antoni Przygienda <[email-masked]>
Date: Wed, 6 Nov 2019 16:52:41 +0000

From practical experience (as in, implementing and interoping stuff through schema defined packet formats in a performance critical protocol) I think that it is most practical and  long-term productive to concentrate on a format IDL like yang-data or enhance GRPC or thrift with offset/size provisions to model such data. Trying to kow-tow to "human readers" sprinkling stuff full of natural language in ASCII pictures all over the document was a feasible technique when better tools did not exist and complexity was low and people were "reading the wire". Formalizing it further does IMO a long term disservice to IETF @ this point in time for several reasons. 

Having said that, I made exceedingly good experience working on implementation/interop of a whole protocol in Thrift which we chose for its extremely portable open source compiler, maturity, extensive language backend support and rich set of constructs available (maps of even structures to structures, differentiation between a set and a vector and so on). In fact, my view is that you want to train people to NOT look @ packet bits and count offsets to understand what's going on but serialized data is a "blob" on the wire that can be only read after an IDL is applied to decode it. 

As to "reserved", future extensibility and so on we thought through the issues and with versioning of schemas and couple rules this is entirely feasible. At least Thrift parser does reliably differentiate from IDL between optional, optional with default and mandatory fields which is all that is really needed as we verified. 

Schema in protocol spec appendix on https://datatracker.ietf.org/doc/draft-ietf-rift-rift/?include_text=1

BTW, an interesting problem is how we match a packet IDL onto registries. The IANA section you find in RIFT is entirely generated from the schema and IMO that's a viable approach (interesting topic is versioning of schema and how THAT interacts with registries ultimately). Ultimately I believe the IDL should be the source of truth and the registries should just point to schema elements and enforce registry allocation policies, ensure collision-free extension of schema and validate its versioning but not hold codepoints. 

Glad to talk more about it but I'm coming in Sat nite only ... 

--- tony 

On 11/6/19, 7:40 AM, "hackathon on behalf of Carsten Bormann" <[email-masked] on behalf of [email-masked]> wrote:

    

    [1]: https://urldefense.com/v3/__https://tools.ietf.org/html/draft-petrov-t2trg-youpi__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNKybg7Y9A$ 

    
    [2]: https://urldefense.com/v3/__https://tools.ietf.org/html/draft-ucarion-jddf__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNLGSHOyBg$ 

    [3]: https://urldefense.com/v3/__https://www.w3.org/TR/wot-thing-description/__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNLJDdphMw$ 
    [4]: https://github.com/one-data-model/language/blob/master/sdf.md
    [5]: https://github.com/t2trg/2019-11-singapore
    (Yes, you can still register.)

    [6]: https://urldefense.com/v3/__https://www.iab.org/wp-content/IAB-uploads/2016/03/Noise-in-specifications-hurts.pdf__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNIWiw1ecg$ 

    Grüße, Carsten

    > Specifying. Details for both projects are available on the Wiki at https://urldefense.com/v3/__https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNL8MUCYaQ$ ,
    > I-D: https://urldefense.com/v3/__https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNLmRvlHqA$ 
    > Getting started information: https://urldefense.com/v3/__https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNL8MUCYaQ$ 
    > 
    > Thanks,
    > 
    > Stephen
    > 
    > 
    > 
    > https://urldefense.com/v3/__https://www.ietf.org/mailman/listinfo/hackathon__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNI0zxfnZQ$ 
    
    _______________________________________________
    hackathon mailing list
    [email-masked]
    https://urldefense.com/v3/__https://www.ietf.org/mailman/listinfo/hackathon__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNI0zxfnZQ$

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Nov 2019 18:12:37 +0100

On Nov 6, 2019, at 17:52, Antoni Przygienda <prz=[email-masked]> wrote:
> enhance GRPC or thrift

There are several of these integrated modeling language + encoding scheme ecosystems we could latch ourselves up to.  Actually we did that already with ASN.1 a long time ago, and it is interesting what people who have used it for a few decades now think about it (*).

Obviously there are some requirements for data modeling (mostly around handling evolution) that are better served by using a mature FDT approach than by graphical representation of various encoding stages (the “box notation” we love from RFC79x etc.).  

When the encoding dominates your thinking, they get in the way (e.g., look at how HTTP/2 is encoded).  So being able to describe an arbitrary bespoke encoding with an FDT (like Quentin’s work or YOUPI do, within the limits of their expressibility) may be useful in those spaces.

When the complexity of the data being modeled dominates your thinking, you want a solid encoding scheme such as XML or JSON or CBOR (or you can do the latch-up alluded to above).
For standards that are expected to live for a while (“design for decades”), I prefer situations where the encoding scheme has a life of its own, independent of the FDT, so you can swap your FDT if the old one is broken (just as we moved from W3C XSD to Relax-NG for most XML work).  The integrated approaches may have their own advantages, especially in the time-to-market department, while usually wedding you to a specific toolchain (or tool ecosystem, as with ASN.1).

Grüße, Carsten

(*) Especially after you compensate for the inevitable occurrence of Stockholm syndrome.

---

From: Antoni Przygienda <[email-masked]>
Date: Wed, 6 Nov 2019 17:20:57 +0000

>    When the complexity of the data being modeled dominates your thinking …

Tony’s dogma: “Complexity of any successful technology _always_ goes up with time” 😉 😉

--- tony

---

From: "Timothy B. Terriberry" <[email-masked]>
Date: Wed, 6 Nov 2019 12:46:45 -0800

> in the format our draft describes, and in how our tooling might fit into 

I haven't reviewed the full draft, but one thing that stands out is the 
limitation, "A packet can contain only one unspecified length field, to 
ensure there is no ambiguity" in Section 4.1.

As a counter-example, I offer "code 1 packets" from RFC 6716 Section 
3.2.3: https://tools.ietf.org/html/rfc6716#section-3.2.3

These packets have two fields where the length is determined by the 
total size of the packet, under the restriction that they must be equal.

I didn't see a lot of detail on _how_ "the size of a field is ... 
derived from the value of some previous field", and if there are any 
restrictions on this derivation, but in general for Opus this can be 
somewhat involved, so I am certainly curious about structured text that 
allows for the parsing process to be fully specified.

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Nov 2019 22:02:23 +0100

> Tony’s dogma: “Complexity of any successful technology _always_ goes up with time” 😉 😉

Indeed, that’s why I talked about “dominates your thinking” (as opposed to “should dominate your thinking”).

An interesting effect of having a great FDT technique is that it becomes much easier to handle complexity.
A follow-on effect is that, as it is so much easier to put in complexity, you do put in more of that.
Which will hurt you sooner than you think (*)…

So I strongly believe that a prerequisite of using FDT successfully is that the formal model of your shiny new RFC should now fit on one slide.  (Which actually works out for RFC 7071 (+)!)

Grüße, Carsten

(*) I still remember when I first read the ASN.1 for GSM MAP.  All 950 pages [IIRC] of it…
(+) https://tools.ietf.org/html/rfc8610#page-61

---

From: Ted Lemon <[email-masked]>
Date: Wed, 6 Nov 2019 22:11:38 +0100

This is getting kind of long for the hackathon mailing list (not that I object to formal languages!).

> On Nov 6, 2019, at 10:02 PM, Carsten Bormann <[email-masked]> wrote:
>

---

From: Marc Petit-Huguenin <[email-masked]>
Date: Wed, 6 Nov 2019 13:13:49 -0800

Maybe we need a new mailing-list to discuss formal languages...

---

From: Antoni Przygienda <[email-masked]>
Date: Wed, 6 Nov 2019 21:15:51 +0000

All correct, except the "fit on one slide" for the whole model is probably working for anything that is not a real world problem __ unless I misunderstood ... 

--- tony 

On 11/6/19, 1:02 PM, "Carsten Bormann" <[email-masked]> wrote:

    

    Grüße, Carsten
    
    (*) I still remember when I first read the ASN.1 for GSM MAP.  All 950 pages [IIRC] of it…
    (+) https://urldefense.com/v3/__https://tools.ietf.org/html/rfc8610*page-61__;Iw!8WoA6RjC81c!TwrWiCR6j8RDlcPfaISIxVV7xjRnaS04YL0LnKZkf3XxaHeXxM53msCyp2QMaA$

---

From: Stephen McQuistin <[email-masked]>
Date: Mon, 18 Nov 2019 15:06:19 +0800

Hi all,

Given the amount of discussion about this, a new mailing list has been created:

	https://www.ietf.org/mailman/listinfo/fdt <https://www.ietf.org/mailman/listinfo/fdt> ([email-masked] <mailto:[email-masked]>)

The list is for the discussion of formal languages, as they pertain to IETF documents. This includes discussion of the requirements of these techniques, and of their adoption within the IETF.

In addition, a reminder that we’re holding an informal side meeting on Thursday at 8pm. This’ll be at The Winery at CHIJMES (Google Maps: https://g.page/thewinerysg <https://g.page/thewinerysg>) — CHIJMES is across the road from the meeting hotel; once there, The Winery is downstairs. If you’re planning to come along, let us know so that we don’t miss anyone.

Thanks,

Stephen

> On 7 Nov 2019, at 05:13, Marc Petit-Huguenin <[email-masked]> wrote:
>