Network Working Group M. PetitHuguenin
InternetDraft Impedance Mismatch LLC
Intended status: Informational 22 May 2024
Expires: 23 November 2024
A Formalization of Symbolic Expressions
draftpetithugueninufmrgformalsexpr04
Abstract
The goal of this document is to show and explain the formal model
developed to guarantee that the examples and ABNF in the "SPKI
Symbolic Expressions" InternetDraft are correct.
Status of This Memo
This InternetDraft is submitted in full conformance with the
provisions of BCP 78 and BCP 79.
InternetDrafts are working documents of the Internet Engineering
Task Force (IETF). Note that other groups may also distribute
working documents as InternetDrafts. The list of current Internet
Drafts is at https://datatracker.ietf.org/drafts/current/.
InternetDrafts are draft documents valid for a maximum of six months
and may be updated, replaced, or obsoleted by other documents at any
time. It is inappropriate to use InternetDrafts as reference
material or to cite them other than as "work in progress."
This InternetDraft will expire on 23 November 2024.
Copyright Notice
Copyright (c) 2024 IETF Trust and the persons identified as the
document authors. All rights reserved.
This document is subject to BCP 78 and the IETF Trust's Legal
Provisions Relating to IETF Documents (https://trustee.ietf.org/
licenseinfo) in effect on the date of publication of this document.
Please review these documents carefully, as they describe your rights
and restrictions with respect to this document.
Table of Contents
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 3
2. Terminology . . . . . . . . . . . . . . . . . . . . . . . . . 4
3. Analysis and Formalization of SExpr . . . . . . . . . . . . 4
PetitHuguenin Expires 23 November 2024 [Page 1]
InternetDraft Formal SPKI SExpr May 2024
3.1. Verbatim Representation . . . . . . . . . . . . . . . . . 6
3.1.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 6
3.1.2. Formalization . . . . . . . . . . . . . . . . . . . . 7
3.1.3. Validation . . . . . . . . . . . . . . . . . . . . . 7
3.2. QuotedString Representation . . . . . . . . . . . . . . 8
3.2.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 8
3.2.2. Formalization . . . . . . . . . . . . . . . . . . . . 10
3.2.3. Validation . . . . . . . . . . . . . . . . . . . . . 14
3.3. Token Representation . . . . . . . . . . . . . . . . . . 16
3.3.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 16
3.3.2. Formalization . . . . . . . . . . . . . . . . . . . . 16
3.3.3. Validation . . . . . . . . . . . . . . . . . . . . . 17
3.4. Hexadecimal Representation . . . . . . . . . . . . . . . 18
3.4.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 18
3.4.2. Formalization . . . . . . . . . . . . . . . . . . . . 19
3.4.3. Validation . . . . . . . . . . . . . . . . . . . . . 21
3.5. Base 64 Representation . . . . . . . . . . . . . . . . . 22
3.5.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 22
3.5.2. Formalization . . . . . . . . . . . . . . . . . . . . 23
3.5.3. Validation . . . . . . . . . . . . . . . . . . . . . 26
3.6. OctetString Representation . . . . . . . . . . . . . . . 27
3.6.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 27
3.6.2. Formalization . . . . . . . . . . . . . . . . . . . . 28
3.7. Displayhint Representation . . . . . . . . . . . . . . . 28
3.7.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 29
3.7.2. Formalization . . . . . . . . . . . . . . . . . . . . 30
3.7.3. Validation . . . . . . . . . . . . . . . . . . . . . 30
3.8. Equality of OctetString . . . . . . . . . . . . . . . . 33
3.8.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 33
3.8.2. Formalization . . . . . . . . . . . . . . . . . . . . 34
3.8.3. Validation . . . . . . . . . . . . . . . . . . . . . 34
3.9. Lists . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.9.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 36
3.9.2. Formalization . . . . . . . . . . . . . . . . . . . . 37
3.9.3. Validation . . . . . . . . . . . . . . . . . . . . . 40
3.10. Advanced SExpr Transport . . . . . . . . . . . . . . . . 41
3.10.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 41
3.10.2. Formalization . . . . . . . . . . . . . . . . . . . 42
3.10.3. Validation . . . . . . . . . . . . . . . . . . . . . 42
3.11. Canonical SExpr Transport . . . . . . . . . . . . . . . 43
3.11.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 43
3.11.2. Formalization . . . . . . . . . . . . . . . . . . . 43
3.11.3. Validation . . . . . . . . . . . . . . . . . . . . . 44
3.12. Basic SExpr Transport . . . . . . . . . . . . . . . . . 45
3.12.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 45
3.12.2. Formalization . . . . . . . . . . . . . . . . . . . 46
3.12.3. Validation . . . . . . . . . . . . . . . . . . . . . 47
3.13. ArrayLayout . . . . . . . . . . . . . . . . . . . . . . 48
PetitHuguenin Expires 23 November 2024 [Page 2]
InternetDraft Formal SPKI SExpr May 2024
3.13.1. Analysis . . . . . . . . . . . . . . . . . . . . . . 48
3.13.2. Formalization . . . . . . . . . . . . . . . . . . . 49
3.13.3. Verification . . . . . . . . . . . . . . . . . . . . 50
4. Informative References . . . . . . . . . . . . . . . . . . . 52
Appendix A. Code Extraction and Verification . . . . . . . . . . 52
Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . 53
Changelog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
Author's Address . . . . . . . . . . . . . . . . . . . . . . . . 53
1. Introduction
 Mathematics is nature's way of letting you know how sloppy your
 writing is.

  Leslie Lamport
A Computerate Specification [ComputerateSpecification] is a mix of a
formal and an informal specification, where parts of the informal
specification are generated from the formal part. The formal
specification is then erased when generating an InternetDraft for
the IETF or a Confluence page for enterprises.
SPKI Symbolic Expressions [SPKISExpr] is a specification for
symbolic expressions ("sexpr") that is the result of editing a
specification originally written back in 1996 by Ronald Rivest. This
is done for the purpose of publishing it as an RFC and thus getting a
stable reference.
This document shows and explains the formal specification as if that
editing was done as a computerate specification. It is not an
analysis and formalization of [SPKISExpr], but rather the
justification for some of its modifications.
This document uses the programming language [Idris2] as a formal
method to build a formal model for sexpr that is sound and complete,
and to build and verify proofs of that model. As a result the whole
text of this document is interspersed with Idris2 code (something
called literate programming), which can be extracted and verified as
explained in Appendix A.
Because the original document is no longer available online, the
relevant parts are quoted instead of being referenced, using the
recommendations in [RFC8792] to wrap long lines.
PetitHuguenin Expires 23 November 2024 [Page 3]
InternetDraft Formal SPKI SExpr May 2024
2. Terminology
The following terminology defines some mathematical terms that are
not used often at the IETF. These terms may have different
definitions outside of this document, but only the definitions listed
here are relevant in the context of this document:
Completeness: describes a formal system that accepts all valid
strings
CurryHoward Isomorphism: a relation that expresses the fact that
computer programs and mathematical proofs are the same thing
Formal Language: a language that have explicit syntax and semantics
Formal Method: the combination of a formal language and a
verification system
Formal Model: a representation of a system using a formal language
Formal Specification: the specification of a system using formal
methods
Isomorphism: the property that two or more structures are carrying
the exact same information
Normalization: the simplification of a proof which, in a program,
corresponds to code reduction (also known as code execution)
Proof: the concrete evidence for a proposition which, in a program,
corresponds to code that typechecks for the type that corresponds
to that proposition
Proposition: a mathematical statement in constructive logic which,
in a program, corresponds to a type
Soundness: describes a formal system that rejects all invalid
strings
Totality: the property of a function that always returns a value in
finite time for any possible input
3. Analysis and Formalization of SExpr
The first subsection of each of the following sections is an analysis
of the original document for ambiguities and contradictions, together
with the resolution of these ambiguities and contradictions.
PetitHuguenin Expires 23 November 2024 [Page 4]
InternetDraft Formal SPKI SExpr May 2024
The second subsection shows and explains the formal model of what is
discussed in the first subsection.
Formalization only guarantees that an instance of the model has
exactly the same bugs that its model, so there is a need for a
validation of that model. The third subsection shows proofs of
correctness for each example in the original document.
First we need to import a module from the Idris2 standard library:
import Data.Bits
We want Idris2 to fail to typecheck the code if totality cannot be
verified for any of the functions, which is done which the following
pragma:
%default total
Note that this pragma actually makes Idris2 nonTuring complete for
the code in that document.
Our type is indexed over a list of octets, which makes it a dependent
type. Per the CurryHoward isomorphism, this type acts as a
proposition that can be read in plain English as "there exists a list
of octets that is a valid sexpr".
Idris's Bits8 is what the IETF calls an octet, so a List Bits8 is a
list of octets. Note that we do not use characters at all in this
formalization, as sexpr are not defined for characters but for
octets, but is it possible to convert a list of octets into an
equivalent characters string in the Idris REPL:
Main> pack $ map (chr . cast) [51, 58, 97, 98, 99]
"3:abc"
Alternatively the show function can be used directly on a list of
octets after loading the code in the REPL:
Show (List Bits8) where
show = pack . map (chr . cast)
Our indexed types are actually families of types, one for each
possible value of the index of type List Bits8. Because there is an
infinite number of values possible for the index, that actually
defines an infinite number of types, one for each possible list of
octets, each either a valid sexpr or not.
PetitHuguenin Expires 23 November 2024 [Page 5]
InternetDraft Formal SPKI SExpr May 2024
Only the types in that family that are indexed over a list of octets
that is a valid sexpr can have an instance that typechecks. Per
the CurryHoward isomorphim, that instance is considered a proof of
the corresponding proposition. Conversely the impossibility of
finding an instance of a specific type is a proof that the index is
not a valid sexpr.
We need a way to extract the underlying octetstring for each
representation that we are going to define. This is done by
declaring an adhoc polymorphic function in an interface:
interface OctetString ty where
octetString : ty > List Bits8
3.1. Verbatim Representation
3.1.1. Analysis
Section 4.1 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
A verbatim encoding of an octet string consists of four parts:
 the length (number of octets) of the octetstring,
given in decimal most significant digit first, with
no leading zeros.
 a colon ":"
 the octet string itself, verbatim.
There are no blanks or whitespace separating the parts. No \
\"escape
sequences" are interpreted in the octet string. This \
\encoding is also
called a "binary" or "raw" encoding.
There is a slight confusion here between an octetstring and its
representation as verbatim, which is understandable in this context
because they look exactly the same.
"Blank" is actually a subset of white space, so this is redundant.
There is no possible BNF that is sound for the verbatim
representation.
PetitHuguenin Expires 23 November 2024 [Page 6]
InternetDraft Formal SPKI SExpr May 2024
3.1.2. Formalization
We need first to reimplement the Idris2 function that is used to
convert a number into an equivalent list of octets using the ASCII
encoding, as we generally cannot use functions that uses primitives
in types because they do not reduce:
base10 : Nat > List Bits8
base10 0 = [48]
base10 x = base' [] x where
base' : List Bits8 > Nat > List Bits8
base' xs 0 = xs
base' xs n =
let (d, m) = divmodNatNZ n 10 SIsNonZero
m' = cast (m + 0x30)
in assert_total $ base' (m' :: xs) d
Then the Verbatim type is defined for the verbatim representation of
an octetstring:
data Verbatim : List Bits8 > Type where
MkVerbatim : (xs : List Bits8) >
Verbatim (base10 (length xs) ++ [58] ++ xs)
Then we define the octetString function for the Verbatim type:
OctetString (Verbatim _) where
octetString (MkVerbatim xs) = xs
3.1.3. Validation
Idris2 is expressive enough to allow embedding unit tests in the same
source and run them as part of the typechecking.
Here we prove that all the examples in section 4.1 of the original
document are valid instances of the Verbatim type:
Here are some sample verbatim encodings:
3:abc
7:subject
4:::::
12:hello world!
10:abcdefghij
0:
* 3:abc
PetitHuguenin Expires 23 November 2024 [Page 7]
InternetDraft Formal SPKI SExpr May 2024
testVerbatim1 : Verbatim [51, 58, 97, 98, 99]
testVerbatim1 = MkVerbatim [97, 98, 99]
* 7:subject
testVerbatim2 : Verbatim [55, 58, 115, 117, 98, 106, 101, 99,
116]
testVerbatim2 = MkVerbatim [115, 117, 98, 106, 101, 99, 116]
* 4:::::
testVerbatim3 : Verbatim [52, 58, 58, 58, 58, 58]
testVerbatim3 = MkVerbatim [58, 58, 58, 58]
* 12:hello world!
testVerbatim4 : Verbatim [49, 50, 58, 104, 101, 108, 108, 111,
32, 119, 111, 114, 108, 100, 33]
testVerbatim4 = MkVerbatim [104, 101, 108, 108, 111, 32, 119,
111, 114, 108, 100, 33]
* 10:abcdefghij
testVerbatim5 : Verbatim [49, 48, 58, 97, 98, 99, 100, 101,
102, 103, 104, 105, 106]
testVerbatim5 = MkVerbatim [97, 98, 99, 100, 101, 102, 103,
104, 105, 106]
* 0:
testVerbatim6 : Verbatim [48, 58]
testVerbatim6 = MkVerbatim []
3.2. QuotedString Representation
3.2.1. Analysis
Section 4.2 of the original sexpr document states:
PetitHuguenin Expires 23 November 2024 [Page 8]
InternetDraft Formal SPKI SExpr May 2024
NOTE: '\\' line wrapping per RFC 8792
The quotedstring representation of an octetstring consists of:
 an optional decimal length field
 an initial doublequote (")
 the octet string with "C" escape conventions (\n,etc)
 a final doublequote (")
The specified length is the length of the resulting string after \
\any
escape sequences have been handled. The string does not have any
"terminating NULL" that C includes, and the length does not \
\count such
a character.
The length is optional.
There is no possible BNF that is sound for the quotedstring
representation when preceded with the length.
Section 4.2 continues with:
PetitHuguenin Expires 23 November 2024 [Page 9]
InternetDraft Formal SPKI SExpr May 2024
NOTE: '\\' line wrapping per RFC 8792
The escape conventions within the quoted string are as follows \
\(these follow
the "C" programming language conventions, with an extension for
ignoring line terminators of just LF or CRLF):
\b  backspace
\t  horizontal tab
\v  vertical tab
\n  newline
\f  formfeed
\r  carriagereturn
\"  doublequote
\'  singlequote
\\  backslash
\ooo  character with octal value ooo (all \
\three digits
must be present)
\xhh  character with hexadecimal value hh (\
\both digits
must be present)
\  causes carriagereturn to be \
\ignored.
\  causes linefeed to be ignored
\  causes CRLF to be \
\ignored.
\  causes LFCR to be \
\ignored.
Here the first sentence does not match the list of line terminators
below it. We assume that there are four line terminators, not two.
In C the escape sequence '\0' is defined for character, but not for
strings as a 0 value can never appear in a C string. But that is not
true of a quotedstring and it would even be useful to have a shorter
encoding than "\x00". We assume that is was not an oversight, and do
not add "\0" as escape sequence.
On the other hand the C Programming Language [KandR] book defines the
additional escape sequence "\?" but we are not going to change that.
3.2.2. Formalization
There is between four and seven different ways to represent an octet
in a quotedstring: ASCII, escaped, octal, and hexadecimal, with that
last one taking up to 4 different different representations depending
on the combination of uppercase and lowercase symbols.
PetitHuguenin Expires 23 November 2024 [Page 10]
InternetDraft Formal SPKI SExpr May 2024
We first define a function for each of the different type of
encodings that returns either a nonempty list of octets if the octet
is representable in that encoding, or an empty list if it is not:
* The octets of value 32, 33, 3591, and 93126 can be represented
as the equivalent ASCII character:
ascii : Bits8 > List Bits8
ascii m =
if m < 32 then empty
else if m == 34 then empty
else if m == 92 then empty
else if m > 126 then empty
else [m]
* The octets of value 7, 8, 9, 10, 11, 12, 13, 34, 39, and 92 can be
represented respectively as the ASCII sequences "\a", "\b", "\t",
"\n", "\v", "\f", "\r", "\"", "\'", and "\\":
escaped : Bits8 > List Bits8
escaped 7 = [92, 97]
escaped 8 = [92, 98]
escaped 9 = [92, 116]
escaped 10 = [92, 110]
escaped 11 = [92, 118]
escaped 12 = [92, 102]
escaped 13 = [92, 114]
escaped 34 = [92, 34]
escaped 39 = [92, 39]
escaped 92 = [92, 92]
escaped _ = empty
* All octets can be represented as the "\" ASCII character followed
by the octal encoding of that octet in ASCII:
octal : Bits8 > List Bits8
octal x =
let m = x `shiftR` 6
n = (x `shiftR` 3) .&. 7
o = x .&. 7
in [92, m + 48, n + 48, o + 48]
* All octets can be represented as the "\x" ASCII sequence followed
by the hexadecimal encoding of that octet. Because alphabetic
hexadecimal symbols can be encoded as lowercase or uppercase
symbols, we get two different encodings for each half of an octet:
PetitHuguenin Expires 23 November 2024 [Page 11]
InternetDraft Formal SPKI SExpr May 2024
halfl : Bits8 > Bits8
halfl x = if x < 10 then x + 48 else x + 87
halfu : Bits8 > Bits8
halfu x = if x < 10 then x + 48 else x + 55
Which then gives us four different hexadecimal encodings for an
octet:
hexll : Bits8 > List Bits8
hexll x = [92, 120, halfl (x `shiftR` 4), halfl (x .&. 15)]
hexlu : Bits8 > List Bits8
hexlu x = [92, 120, halfl (x `shiftR` 4), halfu (x .&. 15)]
hexul : Bits8 > List Bits8
hexul x = [92, 120, halfu (x `shiftR` 4), halfl (x .&. 15)]
hexuu : Bits8 > List Bits8
hexuu x = [92, 120, halfu (x `shiftR` 4), halfu (x .&. 15)]
We then define a Quoted type indexed over the quotedstring
representation of a single octet, using one constructor for each
possible type of representation for an octet.
A boolean expression is used to restrict the possible values of the
octet when encoded as an ASCII or escaped value, preventing the
corresponding constructors to be instantiated.
We also have four additional constructors for the four types of line
breaks. These are purely cosmetic and do not encode an octet.
PetitHuguenin Expires 23 November 2024 [Page 12]
InternetDraft Formal SPKI SExpr May 2024
data Quoted : List Bits8 > Type where
Ascii :
(x : Bits8) > (prf : (x >= 32 && x <= 127 && x /= 34 &&
x /= 92) === True) >
Quoted (ascii x)
Escaped : (x : Bits8) >
(prf : (x >= 7 && x <= 13
 x == 34  x == 39  x == 92) === True) >
Quoted (escaped x)
HexLL : (x : Bits8) > Quoted (hexll x)
HexUL : (x : Bits8) > Quoted (hexul x)
HexLU : (x : Bits8) > Quoted (hexlu x)
HexUU : (x : Bits8) > Quoted (hexuu x)
Octal : (x : Bits8) > Quoted (octal x)
Cr : Quoted [92, 13]
Lf : Quoted [92, 10]
CrLf : Quoted [92, 13, 10]
LfCr : Quoted [92, 10, 13]
We can then use that type to build a type indexed over a complete
quotedstring. Here we use an Idris2 namespace so we can use the
syntactic sugar for a list multiple times in the same source:
namespace QuotedString
public export
data QuotedList : List Bits8 > Type where
Nil : QuotedList []
(::) : Quoted xs > QuotedList ys >
QuotedList (xs ++ ys)
We can then define the octetString function for the QuotedList type:
OctetString (QuotedList _) where
octetString [] = []
octetString (Ascii x _ :: y) = x :: octetString y
octetString (Escaped x _ :: y) = x :: octetString y
octetString (HexLL x :: y) = x :: octetString y
octetString (HexUL x :: y) = x :: octetString y
octetString (HexLU x :: y) = x :: octetString y
octetString (HexUU x :: y) = x :: octetString y
octetString (Octal x :: y) = x :: octetString y
octetString (Cr :: y) = octetString y
octetString (Lf :: y) = octetString y
octetString (CrLf :: y) = octetString y
octetString (LfCr :: y) = octetString y
The type for a quotedstring:
PetitHuguenin Expires 23 November 2024 [Page 13]
InternetDraft Formal SPKI SExpr May 2024
data QuotedString : List Bits8 > Type where
MkQuotedString : QuotedList xs >
QuotedString (34 :: xs ++ [34])
And the function to retrieve its octetstring:
OctetString (QuotedString _) where
octetString (MkQuotedString q) = octetString q
We then define an alternative type for the quotedstring
representation that is preceded by the length of its octetstring:
data QuotedStringLength : List Bits8 > Type where
MkQuotedStringLength : (q : QuotedList xs) >
QuotedStringLength (base10 (length (octetString q)) ++
[34] ++ xs ++ [34])
And the function to retrieve its octetstring:
OctetString (QuotedStringLength _) where
octetString (MkQuotedStringLength q) = octetString q
3.2.3. Validation
Here we prove that all the examples in section 4.2 of the original
document are valid instances of the QuotedString or
QuotedStringLength types:
Here are some examples of quotedstring encodings:
"subject"
"hi there"
7"subject"
3"\n\n\n"
"This has\n two lines."
"This has\
one."
""
* "subject"
testQuotedString1 : QuotedString [34, 115, 117, 98, 106, 101,
99, 116, 34]
testQuotedString1 = MkQuotedString [Ascii 115 Refl,
Ascii 117 Refl, Ascii 98 Refl, Ascii 106 Refl,
Ascii 101 Refl, Ascii 99 Refl, Ascii 116 Refl]
* "hi there"
PetitHuguenin Expires 23 November 2024 [Page 14]
InternetDraft Formal SPKI SExpr May 2024
testQuotedString2 : QuotedString [34, 104, 105, 32, 116, 104,
101, 114, 101, 34]
testQuotedString2 = MkQuotedString [Ascii 104 Refl,
Ascii 105 Refl, Ascii 32 Refl, Ascii 116 Refl,
Ascii 104 Refl, Ascii 101 Refl, Ascii 114 Refl,
Ascii 101 Refl]
* 7"subject"
testQuotedString3 : QuotedStringLength [55, 34, 115, 117, 98,
106, 101, 99, 116, 34]
testQuotedString3 = MkQuotedStringLength [Ascii 115 Refl,
Ascii 117 Refl, Ascii 98 Refl, Ascii 106 Refl,
Ascii 101 Refl, Ascii 99 Refl, Ascii 116 Refl]
* 3"\n\n\n"
testQuotedString4 : QuotedStringLength [51, 34, 92, 110, 92,
110, 92, 110, 34]
testQuotedString4 = MkQuotedStringLength [Escaped 10 Refl,
Escaped 10 Refl, Escaped 10 Refl]
* "This has\n two lines."
testQuotedString5 : QuotedString [34, 84, 104, 105, 115, 32,
104, 97, 115, 92, 110, 32, 116, 119, 111, 32, 108, 105,
110, 101, 115, 46, 34]
testQuotedString5 = MkQuotedString [Ascii 84 Refl,
Ascii 104 Refl, Ascii 105 Refl, Ascii 115 Refl,
Ascii 32 Refl, Ascii 104 Refl, Ascii 97 Refl, Ascii 115 Refl,
Escaped 10 Refl, Ascii 32 Refl, Ascii 116 Refl,
Ascii 119 Refl, Ascii 111 Refl, Ascii 32 Refl,
Ascii 108 Refl, Ascii 105 Refl, Ascii 110 Refl,
Ascii 101 Refl, Ascii 115 Refl, Ascii 46 Refl]
* "This has\ one." (actually on two lines)
testQuotedString6 : QuotedString [34, 84, 104, 105, 115, 32,
104, 97, 115, 92, 10, 111, 110, 101, 46, 34]
testQuotedString6 = MkQuotedString [Ascii 84 Refl,
Ascii 104 Refl, Ascii 105 Refl, Ascii 115 Refl,
Ascii 32 Refl, Ascii 104 Refl, Ascii 97 Refl,
Ascii 115 Refl, Lf, Ascii 111 Refl, Ascii 110 Refl,
Ascii 101 Refl, Ascii 46 Refl]
* ""
PetitHuguenin Expires 23 November 2024 [Page 15]
InternetDraft Formal SPKI SExpr May 2024
testQuotedString7 : QuotedString [34, 34]
testQuotedString7 = MkQuotedString []
3.3. Token Representation
3.3.1. Analysis
Section 4.3 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
An octet string that meets the following conditions may be given
directly as a "token".
 it does not begin with a digit
 it contains only characters that are
 alphabetic (upper or lower case),
 numeric, or
 one of the eight "pseudoalphabetic" \
\punctuation marks:
 . / _ : * + =
(Note: upper and lower case are not equivalent.)
(Note: A token may begin with punctuation, including ":").
3.3.2. Formalization
At the difference of all the other encodings, a token element can
represent only a subset of all possible octets so we first define a
type that constrains any octets but the first in a token:
data TokenChar : Bits8 > Type where
MkTokenChar : (x : Bits8) >
(prf : (x >= 65 && x <= 90  x >= 97 && x <= 122 
x >= 48 && x <= 57  x == 45  x == 46  x == 47 
x == 95  x == 58  x == 42  x == 43  x == 61)
=== True) >
TokenChar x
Then we define a type for a list of these:
namespace Token
public export
data TokenCharList : List Bits8 > Type where
Nil : TokenCharList []
(::) : TokenChar x > TokenCharList xs >
TokenCharList (x :: xs)
PetitHuguenin Expires 23 November 2024 [Page 16]
InternetDraft Formal SPKI SExpr May 2024
Then a type that represents a complete token as a constrained first
octet followed by a list of constrained octets:
data Token : List Bits8 > Type where
MkToken : (x : Bits8) >
(prf : (x >= 65 && x <= 90  x >= 97 && x <= 122 
x == 45  x == 46  x == 95  x == 58  x == 42 
x == 47  x == 43  x == 61) === True) >
TokenCharList xs > Token (x :: xs)
We can then define the octetString function for the Token type:
OctetString (Token _) where
octetString (MkToken x _ xs) = x :: octetString' xs where
octetString' : TokenCharList _ > List Bits8
octetString' [] = []
octetString' (MkTokenChar x _ :: xs) = x :: octetString' xs
3.3.3. Validation
Here we prove that all the examples in section 4.3 of the original
document are valid instances of the Token type:
Here are some examples of token representations:
subject
notbefore
classof1997
//microsoft.com/names/smith
*
* subject
testToken1 : Token [115, 117, 98, 106, 101, 99, 116]
testToken1 = MkToken 115 Refl [MkTokenChar 117 Refl,
MkTokenChar 98 Refl, MkTokenChar 106 Refl,
MkTokenChar 101 Refl, MkTokenChar 99 Refl,
MkTokenChar 116 Refl]
* notbefore
testToken2 : Token [110, 111, 116, 45, 98, 101, 102, 111, 114,
101]
testToken2 = MkToken 110 Refl [MkTokenChar 111 Refl,
MkTokenChar 116 Refl, MkTokenChar 45 Refl,
MkTokenChar 98 Refl, MkTokenChar 101 Refl,
MkTokenChar 102 Refl, MkTokenChar 111 Refl,
MkTokenChar 114 Refl, MkTokenChar 101 Refl]
PetitHuguenin Expires 23 November 2024 [Page 17]
InternetDraft Formal SPKI SExpr May 2024
* classof1997
testToken3 : Token [99, 108, 97, 115, 115, 45, 111, 102, 45,
49, 57, 57, 55]
testToken3 = MkToken 99 Refl [MkTokenChar 108 Refl,
MkTokenChar 97 Refl, MkTokenChar 115 Refl,
MkTokenChar 115 Refl, MkTokenChar 45 Refl,
MkTokenChar 111 Refl, MkTokenChar 102 Refl,
MkTokenChar 45 Refl, MkTokenChar 49 Refl,
MkTokenChar 57 Refl, MkTokenChar 57 Refl,
MkTokenChar 55 Refl]
* //microsoft.com/names/smith
testToken4 : Token [47, 47, 109, 105, 99, 114, 111, 115, 111,
102, 116, 46, 99, 111, 109, 47, 110, 97, 109, 101, 115, 47,
115, 109, 105, 116, 104]
testToken4 = MkToken 47 Refl [MkTokenChar 47 Refl,
MkTokenChar 109 Refl, MkTokenChar 105 Refl,
MkTokenChar 99 Refl, MkTokenChar 114 Refl,
MkTokenChar 111 Refl, MkTokenChar 115 Refl,
MkTokenChar 111 Refl, MkTokenChar 102 Refl,
MkTokenChar 116 Refl, MkTokenChar 46 Refl,
MkTokenChar 99 Refl, MkTokenChar 111 Refl,
MkTokenChar 109 Refl, MkTokenChar 47 Refl,
MkTokenChar 110 Refl, MkTokenChar 97 Refl,
MkTokenChar 109 Refl, MkTokenChar 101 Refl,
MkTokenChar 115 Refl, MkTokenChar 47 Refl,
MkTokenChar 115 Refl, MkTokenChar 109 Refl,
MkTokenChar 105 Refl, MkTokenChar 116 Refl,
MkTokenChar 104 Refl]
* *
testToken5 : Token [42]
testToken5 = MkToken 42 Refl []
3.4. Hexadecimal Representation
3.4.1. Analysis
Section 4.4 of the original sexpr document states:
PetitHuguenin Expires 23 November 2024 [Page 18]
InternetDraft Formal SPKI SExpr May 2024
NOTE: '\\' line wrapping per RFC 8792
An octetstring may be represented with a hexadecimal encoding \
\consisting of:
 an (optional) decimal length of the octet string
 a sharpsign "#"
 a hexadecimal encoding of the octet string, with each \
\octet
represented with two hexadecimal digits, most \
\significant
digit first.
 a sharpsign "#"
There may be whitespace inserted in the midst of the hexadecimal
encoding arbitrarily; it is ignored. It is an error to have
characters other than whitespace and hexadecimal digits.
There is no possible BNF that is sound for the hexadecimal
representation when preceded with the length.
"hexadecimal encoding" is understood as allowing either case for each
hexadecimal half of the encoding for a single octet.
3.4.2. Formalization
The hexadecimal representation encodes each octet of an octetstring
as two octets in ASCII, each followed by zero or more white spaces.
First we built a type for a white space:
data Whitespace : Bits8 > Type where
MkWhitespace : (x : Bits8) >
(prf : (x == 32  x == 9  x == 11 
x == 12  x == 13  x == 10) === True) >
Whitespace x
And then a type for a list of white spaces:
namespace Whitespace
public export
data WhitespaceList : List Bits8 > Type where
Nil : WhitespaceList []
(::) : Whitespace x > WhitespaceList xs >
WhitespaceList (x :: xs)
PetitHuguenin Expires 23 November 2024 [Page 19]
InternetDraft Formal SPKI SExpr May 2024
Note that white spaces are purely cosmetic, so they do not encode
octets in an octetstring. That means that there no octetString
function for these.
With that we can build the hexadecimal representation of an octet.
We have four constructors, each corresponding to one of the four
possible variants for an hexadecimal encoding:
data Hex : List Bits8 > Type where
HexLL' : (x : Bits8) > WhitespaceList xs >
WhitespaceList ys >
Hex ([halfl (x `shiftR` 4)] ++ xs ++ [halfl (x .&. 15)] ++
ys)
HexLU' : (x : Bits8) > WhitespaceList xs >
WhitespaceList ys >
Hex ([halfl (x `shiftR` 4)] ++ xs ++ [halfu (x .&. 15)] ++
ys)
HexUL' : (x : Bits8) > WhitespaceList xs >
WhitespaceList ys >
Hex ([halfu (x `shiftR` 4)] ++ xs ++ [halfl (x .&. 15)] ++
ys)
HexUU' : (x : Bits8) > WhitespaceList xs >
WhitespaceList ys >
Hex ([halfu (x `shiftR` 4)] ++ xs ++ [halfu (x .&. 15)] ++
ys)
Then we can build a type for the hexadecimal representation of an
octetstring:
namespace Hexadecimal
public export
data HexList : List Bits8 > Type where
Nil : HexList []
(::) : Hex xs > HexList ys > HexList (xs ++ ys)
And a function octetString for that type:
OctetString (HexList _) where
octetString [] = []
octetString (HexLL' x _ _ :: xs) = x :: octetString xs
octetString (HexLU' x _ _ :: xs) = x :: octetString xs
octetString (HexUL' x _ _ :: xs) = x :: octetString xs
octetString (HexUU' x _ _ :: xs) = x :: octetString xs
With that we can build an Hexadecimal type:
PetitHuguenin Expires 23 November 2024 [Page 20]
InternetDraft Formal SPKI SExpr May 2024
data Hexadecimal : List Bits8 > Type where
MkHexadecimal : WhitespaceList xs > HexList ys >
Hexadecimal (35 :: xs ++ ys ++ [35])
And its octetString function:
OctetString (Hexadecimal _) where
octetString (MkHexadecimal _ y) = octetString y
We then define an alternative type for the hexadecimal representation
that is preceded by the length of its octetstring:
data HexadecimalLength : List Bits8 > Type where
MkHexadecimalLength : WhitespaceList xs >
(h : HexList ys) >
HexadecimalLength (base10 (length (octetString h)) ++
[35] ++ xs ++ ys ++ [35])
And the function to retrieve its octetstring:
OctetString (HexadecimalLength _) where
octetString (MkHexadecimalLength _ h) = octetString h
3.4.3. Validation
Here we prove that all the examples in section 4.4 of the original
document are valid instances of the Hexadecimal type:
Here are some examples of hexadecimal encodings:
#616263#  represents "abc"
3#616263#  also represents "abc"
# 616
263 #  also represents "abc"
* #616263#
testHexadecimal1 : Hexadecimal [35, 54, 49, 54, 50, 54, 51, 35]
testHexadecimal1 = MkHexadecimal [] [HexLL' 97 [] [],
HexLL' 98 [] [], HexLL' 99 [] []]
* 3#616263#
testHexadecimal2 : HexadecimalLength [51, 35, 54, 49, 54, 50,
54, 51, 35]
testHexadecimal2 = MkHexadecimalLength [] [HexLL' 97 [] [],
HexLL' 98 [] [], HexLL' 99 [] []]
PetitHuguenin Expires 23 November 2024 [Page 21]
InternetDraft Formal SPKI SExpr May 2024
* # 616 263 #
testHexadecimal3 : Hexadecimal [35, 32, 54, 49, 54, 10, 32, 32,
50, 54, 51, 32, 35]
testHexadecimal3 = MkHexadecimal [MkWhitespace 32 Refl] [
HexLL' 97 [] [],
HexLL' 98 [MkWhitespace 10 Refl, MkWhitespace 32 Refl,
MkWhitespace 32 Refl] [],
HexLL' 99 [] [MkWhitespace 32 Refl]]
3.5. Base 64 Representation
3.5.1. Analysis
Section 4.5 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
An octetstring may be represented in a base64 coding \
\consisting of:
 an (optional) decimal length of the octet string
 a vertical bar ""
 the rfc 1521 base64 encoding of the octet string.
 a final vertical bar ""
The base64 encoding uses only the characters
AZ az 09 + / =
It produces four characters of output for each three octets of \
\input.
If the input has one or two leftover octets of input, it \
\produces an
output block of length four ending in two or one equals signs, \
\respectively.
Output routines compliant with this standard MUST output the \
\equals signs
as specified. Input routines MAY accept inputs where the equals \
\signs are
dropped.
There may be whitespace inserted in the midst of the base64 \
\encoding
arbitrarily; it is ignored. It is an error to have characters \
\other
than whitespace and base64 characters.
PetitHuguenin Expires 23 November 2024 [Page 22]
InternetDraft Formal SPKI SExpr May 2024
There is no possible BNF that is sound for the base 64 representation
when preceded with the length.
The fragment "...where the equals signs are dropped" is ambiguous as
it does not state if it is one or two equals signs that can be
dropped, or all equals signs. Here we encode types to support the
former interpretation.
3.5.2. Formalization
First we need a function that will return a base 64 octet from the
six lower bits of an octet:
b64 : Bits8 > Bits8
b64 x = if x < 26 then x + 65
else if x < 52 then x + 71
else if x < 62 then x  4
else if x == 62 then 43
else if x == 63 then 47
else 0x3D
Next we need four functions that return respectively the first,
second, third, and fourth ASCII octet for a group of three octets
from the octetstring:
b641 : Bits8 > List Bits8
b641 x1 = [b64 (x1 `shiftR` 2)]
b642 : Bits8 > Bits8 > List Bits8
b642 x1 x2 = [b64 (((x1 .&. 0b11) `shiftL` 4) ..
(x2 `shiftR` 4))]
b643 : Bits8 > Bits8 > List Bits8
b643 x2 x3 = [b64 (((x2 .&. 0b1111) `shiftL` 2) ..
(x3 `shiftR` 6))]
b644 : Bits8 > List Bits8
b644 x3 = [b64 (x3 .&. 0b111111)]
Our first type for the base 64 representation is for a group of three
octets from the octetstring:
PetitHuguenin Expires 23 November 2024 [Page 23]
InternetDraft Formal SPKI SExpr May 2024
data Base64Full : List Bits8 > Type where
MkBase64Full : (x1 : Bits8) > (x2 : Bits8) >
(x3 : Bits8) >
WhitespaceList xs > WhitespaceList ys >
WhitespaceList zs > WhitespaceList ws >
Base64Full (b641 x1 ++ xs ++ b642 x1 x2 ++ ys ++
b643 x2 x3 ++ zs ++ b644 x3 ++ ws)
Then we can build a type for the base 64 representation of an octet
string whose length is a multiple of three:
namespace Base64
public export
data Base64List : List Bits8 > Type where
Nil : Base64List []
(::) : Base64Full xs > Base64List ys >
Base64List (xs ++ ys)
We build another type for the octetstrings that have a length that
is not a multiple of three. There is additional constructors to
account for the fact that the padding is optional.
data Base64End : List Bits8 > Type where
EndOnePadPad : (x1 : Bits8) >
WhitespaceList xs > WhitespaceList ys >
WhitespaceList zs > WhitespaceList ws >
Base64End (b641 x1 ++ xs ++ b642 x1 0 ++ ys ++ [61] ++ zs
++ [61] ++ ws)
EndOnePad : (x1 : Bits8) >
WhitespaceList xs > WhitespaceList ys >
WhitespaceList zs >
Base64End (b641 x1 ++ xs ++ b642 x1 0 ++ ys ++ [61] ++ zs)
EndOne : (x1 : Bits8) >
WhitespaceList xs > WhitespaceList ys >
Base64End (b641 x1 ++ xs ++ b642 x1 0 ++ ys)
EndTwoPad : (x1 : Bits8) > (x2 : Bits8) >
WhitespaceList xs > WhitespaceList ys >
WhitespaceList zs > WhitespaceList ws >
Base64End (b641 x1 ++ xs ++ b642 x1 x2 ++ ys ++ b643 x2 0
++ zs ++ [61] ++ ws)
EndTwo : (x1 : Bits8) > (x2 : Bits8) >
WhitespaceList xs > WhitespaceList ys >
WhitespaceList zs >
Base64End (b641 x1 ++ xs ++ b642 x1 x2 ++ ys ++ b643 x2 0
++ zs)
PetitHuguenin Expires 23 November 2024 [Page 24]
InternetDraft Formal SPKI SExpr May 2024
We then put all these together into a type for base 64 encoding with
two constructors, one for octetstrings whose length is a multiple of
3, and one for the others:
data Base64' : List Bits8 > Type where
Base64Mult3 : Base64List xs > Base64' xs
Base64Non : Base64List xs > Base64End ys >
Base64' (xs ++ ys)
We can then define the octetString function for the Base64' type:
octetString' : Base64List _ > List Bits8
octetString' [] = []
octetString' (MkBase64Full x1 x2 x3 _ _ _ _ :: xs) =
x1 :: x2 :: x3 :: octetString' xs
OctetString (Base64' _) where
octetString (Base64Mult3 xs) = octetString' xs
octetString (Base64Non xs (EndOnePadPad x1 _ _ _ _)) =
octetString' xs ++ [x1]
octetString (Base64Non xs (EndOnePad x1 _ _ _)) =
octetString' xs ++ [x1]
octetString (Base64Non xs (EndOne x1 _ _)) =
octetString' xs ++ [x1]
octetString (Base64Non xs (EndTwoPad x1 x2 _ _ _ _)) =
octetString' xs ++ [x1, x2]
octetString (Base64Non xs (EndTwo x1 x2 _ _ _)) =
octetString' xs ++ [x1, x2]
Finally we can define the Base64 type:
data Base64 : List Bits8 > Type where
MkBase64 : WhitespaceList xs > Base64' ys >
Base64 (124 :: xs ++ ys ++ [124])
And its octetString function:
OctetString (Base64 _) where
octetString (MkBase64 _ y) = octetString y
We then reuse the Base64' type to define one more type for the base
64 representation that is preceded by the length of its octetstring:
data Base64Length : List Bits8 > Type where
MkBase64Length : WhitespaceList xs > (b : Base64' ys) >
Base64Length (base10 (length (octetString b)) ++ [124]
++ xs ++ ys ++ [124])
PetitHuguenin Expires 23 November 2024 [Page 25]
InternetDraft Formal SPKI SExpr May 2024
And its octetString function:
OctetString (Base64Length _) where
octetString (MkBase64Length _ b) = octetString b
3.5.3. Validation
Here we prove that all the examples in section 4.5 of the original
document are valid instances of the Base64 type:
Here are some examples of base64 encodings:
YWJj  represents "abc"
 Y W
J j   also represents "abc"
3YWJj  also represents "abc"
YWJjZA==  represents "abcd"
YWJjZA  also represents "abcd"
* YWJj
testBase641 : Base64 [124, 89, 87, 74, 106, 124]
testBase641 = MkBase64 [] (Base64Mult3
[MkBase64Full 97 98 99 [] [] [] []])
*  Y W J j 
testBase642 : Base64 [124, 32, 89, 32, 87, 32, 74, 32, 106,
32, 124]
testBase642 = MkBase64 [MkWhitespace 32 Refl]
(Base64Mult3 [MkBase64Full 97 98 99 [MkWhitespace 32 Refl]
[MkWhitespace 32 Refl] [MkWhitespace 32 Refl]
[MkWhitespace 32 Refl]])
* 3YWJj
testBase643 : Base64Length [51, 124, 89, 87, 74, 106, 124]
testBase643 = MkBase64Length [] (Base64Mult3
[MkBase64Full 97 98 99 [] [] [] []])
* YWJjZA==
testBase644 : Base64 [124, 89, 87, 74, 106, 90, 65, 61, 61,
124]
testBase644 = MkBase64 [] (Base64Non
[MkBase64Full 97 98 99 [] [] [] []]
(EndOnePadPad 100 [] [] [] []))
PetitHuguenin Expires 23 November 2024 [Page 26]
InternetDraft Formal SPKI SExpr May 2024
* YWJjZA
testBase645 : Base64 [124, 89, 87, 74, 106, 90, 65, 124]
testBase645 = MkBase64 [] (Base64Non
[MkBase64Full 97 98 99 [] [] [] []]
(EndOne 100 [] []))
3.6. OctetString Representation
3.6.1. Analysis
Before going further we have to address the case of the brace
notation for base 64.
Section 6.2 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
There is a difference between the brace notation for base64 \
\used here
and the  notation for base64'd octetstrings described above. \
\ Here
the base64 contents are converted to octets, and then \
\rescanned as
if they were given originally as octets. With the  notation, \
\the
contents are just turned into an octetstring.
It is not clear from that text if the octets that are to be re
scanned are for the representation of an octetstring, or for a whole
sexpr. Additionally this text seems to ignore the fact that
examples using that notation were provided in section 2 and section 5
of the original sexpr document.
So the first ambiguity would about about the usage of the brace
notation in a displayhint. Obviously it would not make sense to
have a sexpr inside a displayhint so at best it encodes an octet
string. But if that's the case, does it encodes any of the other
representations (maybe including itself) or just the verbatim
representation, as examples in section 2 and 5 show?
The same can be said of the use of the brace notation as simple
string. There again it would not make sense to encode an sexpr with
it, because then it would be possible to associate it with a display
hint, which does not make sense. Then if it is only the encoding of
the representation of an octetstring then the same ambiguity than
above is present about the representations permitted.
PetitHuguenin Expires 23 November 2024 [Page 27]
InternetDraft Formal SPKI SExpr May 2024
To add to the issue, the brace notation for base 64 on an octet
string is largely redundant with the quotedstring, hexadecimal, and
base 64 representations, because these already handle the problem of
representing any sexpr using ASCII characters. That is only
required for the basic transport.
Here we chose to use the brace notation for base 64 exclusively in
the basic transport, restricting the octetstring inside as verbatim
representations. That makes the examples in section 2 and 5
incorrect unless used as sexpr in the basic transport.
3.6.2. Formalization
With that in mind we can define a type that covers all possible
representation for an octetstring, excluding the brace notation for
base 64.
data Representation : List Bits8 > Type where
RepresentationVerbatim : (v : Verbatim xs) >
Representation xs
RepresentationQuoted : QuotedString xs >
Representation xs
RepresentationQuotedLength : QuotedStringLength xs >
Representation xs
RepresentationToken : Token xs > Representation xs
RepresentationHexadecimal : Hexadecimal xs >
Representation xs
RepresentationHexadecimalLength : HexadecimalLength xs >
Representation xs
RepresentationBase64 : Base64 xs > Representation xs
RepresentationBase64Length : Base64Length xs >
Representation xs
And its matching octetString function:
OctetString (Representation _) where
octetString (RepresentationVerbatim v) = octetString v
octetString (RepresentationQuoted x) = octetString x
octetString (RepresentationQuotedLength x) = octetString x
octetString (RepresentationToken x) = octetString x
octetString (RepresentationHexadecimal x) = octetString x
octetString (RepresentationHexadecimalLength x) =
octetString x
octetString (RepresentationBase64 x) = octetString x
octetString (RepresentationBase64Length x) = octetString x
3.7. Displayhint Representation
PetitHuguenin Expires 23 November 2024 [Page 28]
InternetDraft Formal SPKI SExpr May 2024
3.7.1. Analysis
Section 4.6 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
Any octet string may be preceded by a single "display hint".
The purposes of the display hint is to provide information on how
to display the octet string to a user. It has no other function.
Many of the MIME types work here.
A displayhint is an octet string surrounded by square brackets.
There may be whitespace separating the octet string from the
surrounding brackets. Any of the legal formats may be used for \
\the
octet string.
The uses of "octet string" in this fragment are all incorrect. "octet
string representation" should be used instead.
The text uses singular "whitespace", not the plural "whitespaces".
The text also does not say if white spaces can separate the display
hint from the octetstring it provides information to. We assume
that multiple white spaces can be used after the opening bracket,
before the closing bracket, and between the closing bracket and the
following octetstring.
Following the argument in the argument in the previous section,
"legal formats" does not include the brace notation for base 64.
Section 4.6 of the original sexpr document ends with:
NOTE: '\\' line wrapping per RFC 8792
In applications an octetstring that is untyped may be \
\considered to have
a prespecified "default" mime type. The mime type
"text/plain; charset=iso88591"
is the standard default.
At first glance using the UTF8 charset seemed more aligned to
current practices, but not all octetstrings are valid UTF8
character strings. Instead the MIME type "application/octetstream"
has the advantage of been neutral.
PetitHuguenin Expires 23 November 2024 [Page 29]
InternetDraft Formal SPKI SExpr May 2024
3.7.2. Formalization
We first build a type for a displayhint:
data DisplayHint : List Bits8 > Type where
MkDisplayHint : WhitespaceList xs > Representation ys >
WhitespaceList zs >
DisplayHint (91 :: xs ++ ys ++ zs ++ [93])
Then define octetString for that type:
OctetString (DisplayHint _) where
octetString (MkDisplayHint _ x _) = octetString x
Then a type for the association of a displayhint and the
representation of an octetstring:
data WithHint : List Bits8 > Type where
MkWithHint : DisplayHint xs > WhitespaceList ys >
Representation zs > WithHint (xs ++ ys ++ zs)
We finally define the default displayhint as the token application/
octetstream:
defaultHint : Representation [97, 112, 112, 108, 105, 99, 97,
116, 105, 111, 110, 47, 111, 99, 116, 101, 116, 45, 115,
116, 114, 101, 97, 109]
defaultHint = RepresentationToken (MkToken 97 Refl
[MkTokenChar 112 Refl, MkTokenChar 112 Refl,
MkTokenChar 108 Refl, MkTokenChar 105 Refl,
MkTokenChar 99 Refl, MkTokenChar 97 Refl,
MkTokenChar 116 Refl, MkTokenChar 105 Refl,
MkTokenChar 111 Refl, MkTokenChar 110 Refl,
MkTokenChar 47 Refl, MkTokenChar 111 Refl,
MkTokenChar 99 Refl, MkTokenChar 116 Refl,
MkTokenChar 101 Refl, MkTokenChar 116 Refl,
MkTokenChar 45 Refl, MkTokenChar 115 Refl,
MkTokenChar 116 Refl, MkTokenChar 114 Refl,
MkTokenChar 101 Refl, MkTokenChar 97 Refl,
MkTokenChar 109 Refl])
3.7.3. Validation
Here we prove that all the examples in section 4.6 of the original
document are valid instances of the DisplayHint type:
PetitHuguenin Expires 23 November 2024 [Page 30]
InternetDraft Formal SPKI SExpr May 2024
Here are some examples of displayhints:
[image/gif]
[URI]
[charset=unicode11]
[text/richtext]
[application/postscript]
[audio/basic]
["http://abc.com/displaytypes/funky.html"]
* [image/gif]
testHint1 : DisplayHint [91, 105, 109, 97, 103, 101, 47, 103,
105, 102, 93]
testHint1 = MkDisplayHint [] (RepresentationToken
(MkToken 105 Refl [MkTokenChar 109 Refl,
MkTokenChar 97 Refl, MkTokenChar 103 Refl,
MkTokenChar 101 Refl, MkTokenChar 47 Refl,
MkTokenChar 103 Refl, MkTokenChar 105 Refl,
MkTokenChar 102 Refl])) []
* [URI]
testHint2 : DisplayHint [91, 85, 82, 73, 93]
testHint2 = MkDisplayHint [] (RepresentationToken
(MkToken 85 Refl [MkTokenChar 82 Refl,
MkTokenChar 73 Refl])) []
* [charset=unicode11]
testHint3 : DisplayHint [91, 99, 104, 97, 114, 115, 101, 116,
61, 117, 110, 105, 99, 111, 100, 101, 45, 49, 45, 49, 93]
testHint3 = MkDisplayHint [] (RepresentationToken
(MkToken 99 Refl [MkTokenChar 104 Refl,
MkTokenChar 97 Refl, MkTokenChar 114 Refl,
MkTokenChar 115 Refl, MkTokenChar 101 Refl,
MkTokenChar 116 Refl, MkTokenChar 61 Refl,
MkTokenChar 117 Refl, MkTokenChar 110 Refl,
MkTokenChar 105 Refl, MkTokenChar 99 Refl,
MkTokenChar 111 Refl, MkTokenChar 100 Refl,
MkTokenChar 101 Refl, MkTokenChar 45 Refl,
MkTokenChar 49 Refl, MkTokenChar 45 Refl,
MkTokenChar 49 Refl])) []
* [text/richtext]
PetitHuguenin Expires 23 November 2024 [Page 31]
InternetDraft Formal SPKI SExpr May 2024
testHint4 : DisplayHint [91, 116, 101, 120, 116, 47, 114, 105,
99, 104, 116, 101, 120, 116, 93]
testHint4 = MkDisplayHint [] (RepresentationToken
(MkToken 116 Refl [MkTokenChar 101 Refl,
MkTokenChar 120 Refl, MkTokenChar 116 Refl,
MkTokenChar 47 Refl, MkTokenChar 114 Refl,
MkTokenChar 105 Refl, MkTokenChar 99 Refl,
MkTokenChar 104 Refl, MkTokenChar 116 Refl,
MkTokenChar 101 Refl, MkTokenChar 120 Refl,
MkTokenChar 116 Refl])) []
* [application/postscript]
testHint5 : DisplayHint [91, 97, 112, 112, 108, 105, 99, 97,
116, 105, 111, 110, 47, 112, 111, 115, 116, 115, 99, 114,
105, 112, 116, 93]
testHint5 = MkDisplayHint [] (RepresentationToken
(MkToken 97 Refl [MkTokenChar 112 Refl,
MkTokenChar 112 Refl, MkTokenChar 108 Refl,
MkTokenChar 105 Refl, MkTokenChar 99 Refl,
MkTokenChar 97 Refl, MkTokenChar 116 Refl,
MkTokenChar 105 Refl, MkTokenChar 111 Refl,
MkTokenChar 110 Refl, MkTokenChar 47 Refl,
MkTokenChar 112 Refl, MkTokenChar 111 Refl,
MkTokenChar 115 Refl, MkTokenChar 116 Refl,
MkTokenChar 115 Refl, MkTokenChar 99 Refl,
MkTokenChar 114 Refl, MkTokenChar 105 Refl,
MkTokenChar 112 Refl, MkTokenChar 116 Refl])) []
* [audio/basic]
testHint6 : DisplayHint [91, 97, 117, 100, 105, 111, 47, 98,
97, 115, 105, 99, 93]
testHint6 = MkDisplayHint [] (RepresentationToken
(MkToken 97 Refl [MkTokenChar 117 Refl,
MkTokenChar 100 Refl, MkTokenChar 105 Refl,
MkTokenChar 111 Refl, MkTokenChar 47 Refl,
MkTokenChar 98 Refl, MkTokenChar 97 Refl,
MkTokenChar 115 Refl, MkTokenChar 105 Refl,
MkTokenChar 99 Refl])) []
* ["http://abc.com/displaytypes/funky.html"]
PetitHuguenin Expires 23 November 2024 [Page 32]
InternetDraft Formal SPKI SExpr May 2024
testHint7 : DisplayHint [91, 34, 104, 116, 116, 112, 58, 47,
47, 97, 98, 99, 46, 99, 111, 109, 47, 100, 105, 115, 112,
108, 97, 121, 45, 116, 121, 112, 101, 115, 47, 102, 117,
110, 107, 121, 46, 104, 116, 109, 108, 34, 93]
testHint7 = MkDisplayHint [] (RepresentationQuoted
(MkQuotedString [Ascii 104 Refl, Ascii 116 Refl,
Ascii 116 Refl, Ascii 112 Refl, Ascii 58 Refl,
Ascii 47 Refl, Ascii 47 Refl, Ascii 97 Refl, Ascii 98 Refl,
Ascii 99 Refl, Ascii 46 Refl, Ascii 99 Refl, Ascii 111 Refl,
Ascii 109 Refl, Ascii 47 Refl, Ascii 100 Refl,
Ascii 105 Refl, Ascii 115 Refl, Ascii 112 Refl,
Ascii 108 Refl, Ascii 97 Refl, Ascii 121 Refl,
Ascii 45 Refl, Ascii 116 Refl, Ascii 121 Refl,
Ascii 112 Refl, Ascii 101 Refl, Ascii 115 Refl,
Ascii 47 Refl, Ascii 102 Refl, Ascii 117 Refl,
Ascii 110 Refl, Ascii 107 Refl, Ascii 121 Refl,
Ascii 46 Refl, Ascii 104 Refl, Ascii 116 Refl,
Ascii 109 Refl, Ascii 108 Refl])) []
3.8. Equality of OctetString
3.8.1. Analysis
Section 4.7 of the original sexpr document states:
Two octet strings are considered to be "equal" if and only if they
have the same display hint and the same data octet strings.
Note that octetstrings are "casesensitive"; the octetstring \
\"abc"
is not equal to the octetstring "ABC".
An untyped octetstring can be compared to another octetstring \
\(typed
or not) by considering it as a typed octetstring with the default
mimetype.
The term "octet string" here is incorrect as it is described as the
combination of a display hint and a "data octet strings", the latter
being actually an "octet string representation".
Consequently the terms "equal" or "equality" are incorrect, and the
terms "equivalent" or "equivalences" should be used instead. Here
the term "equivalent" means "carrying the same information", i.e. the
same octetstring. Two octetstring representations can be
equivalent, but not equal, e.g, the token abc and the quotedstring
"abc" are equivalent but not equal.
PetitHuguenin Expires 23 November 2024 [Page 33]
InternetDraft Formal SPKI SExpr May 2024
The same reasoning is applied when comparing typed octetstring
representations, or a typed octetstring representation with an
untyped octetstring representation.
3.8.2. Formalization
We first define a type that carries either a typed or and untyped
octetstring representation:
data Element : Type where
Untyped : Representation _ > Element
Typed : Representation _ > Representation _ > Element
Then we define the type alias Equivalence as a relation between two
elements. Equivalence is already declared in the standard library,
so we have to hide that declaration first:
%hide Control.Relation.Equivalence
Equivalence : Element > Element > Type
Equivalence (Untyped x) (Untyped x') =
octetString x === octetString x'
Equivalence (Untyped x) (Typed h x') =
(octetString defaultHint === octetString h,
octetString x === octetString x')
Equivalence (Typed h x) (Untyped x') =
(octetString h === octetString defaultHint,
octetString x === octetString x')
Equivalence (Typed h x) (Typed h' x') =
(octetString h === octetString h',
octetString x === octetString x')
3.8.3. Validation
Here we prove that a subset of the examples in section 1 of the
original document are equivalent. Proving the other equivalences is
trivial:
PetitHuguenin Expires 23 November 2024 [Page 34]
InternetDraft Formal SPKI SExpr May 2024
NOTE: '\\' line wrapping per RFC 8792
An octetstring is a finite sequence of eightbit octets. There /
/may be
many different but equivalent ways of representing an \
\octetstring
abc  as a token
"abc"  as a quoted string
#616263#  as a hexadecimal string
3:abc  as a lengthprefixed "verbatim" \
\encoding
{MzphYmM=}  as a base64 encoding of the verbatim \
\encoding
(that is, an encoding of "3:abc")
YWJj  as a base64 encoding of the \
\octetstring "abc"
These encodings are all equivalent; they all denote the same \
\octet string.
We first proves that the 3 first representations are correct:
abcToken : Representation [97, 98, 99]
abcToken = RepresentationToken (MkToken 97 Refl
[MkTokenChar 98 Refl, MkTokenChar 99 Refl])
abcQuoted : Representation [34, 97, 98, 99, 34]
abcQuoted = RepresentationQuoted (MkQuotedString
[Ascii 97 Refl, Ascii 98 Refl, Ascii 99 Refl])
abcHex : Representation [35, 54, 49, 54, 50, 54, 51, 35]
abcHex = RepresentationHexadecimal (MkHexadecimal []
[HexLL' 97 [] [], HexLL' 98 [] [], HexLL' 99 [] []])
We can then prove that abc is equivalent to "abc", and that "abc" is
equivalent to #616263#:
PetitHuguenin Expires 23 November 2024 [Page 35]
InternetDraft Formal SPKI SExpr May 2024
testEq1 : Equivalence (Untyped Main.abcToken)
(Untyped Main.abcQuoted)
testEq1 = Refl
testEq2 : Equivalence (Untyped Main.abcQuoted)
(Untyped Main.abcHex)
testEq2 = Refl
By transitivity we can then prove that abc is equivalent to #616263#:
testEq3 : Equivalence (Untyped Main.abcToken)
(Untyped Main.abcHex)
testEq3 = trans testEq1 testEq2
We can also use symmetry to prove that if a first octetstring
representation is equivalent to a second octetstring representation,
then the second is also equivalent to the first one.
testEq4 : Equivalence (Untyped Main.abcHex)
(Untyped Main.abcToken)
testEq4 = sym testEq3
3.9. Lists
3.9.1. Analysis
Section 5 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
Just as with octetstrings, there are several ways to represent an
Sexpression. Whitespace may be used to separate list elements, \
\but
they are only required to separate two octet strings when \
\otherwise
the two octet strings might be interpreted as one, as when one \
\token
follows another. Also, whitespace may follow the initial left
parenthesis, or precede the final right parenthesis.
The first sentence should say that there are different ways to
represent a list.
But the issue is really that in some cases the separation between
some representations of an octetstring is ambiguous. The actual
rules for mandatory separation are:
PetitHuguenin Expires 23 November 2024 [Page 36]
InternetDraft Formal SPKI SExpr May 2024
* a token must be separated from a quotedstring, hexadecimal, or
base 64 representation that is prefixed with the length
* a token must be separated from the next token
* a token must be separated from the next verbatim representation
Additionally section 2 states:
NOTE: '\\' line wrapping per RFC 8792
A list is a finite sequence of zero or more simpler \
\Sexpressions. A list
may be represented by using parentheses to surround the sequence \
\of encodings
of its elements, as in:
(abc (de #6667#) "ghi jkl")
Parentheses are not optional when representing a list, so "may be"
should be "are".
3.9.2. Formalization
To represent the various ways to separate representations we need
four mutually inductive types, that we first declare as abstract
types:
data TokenList : List Bits8 > Type
data SeparateList : List Bits8 > Type
data OtherList : List Bits8 > Type
data Lists : List Bits8 > Type
TokenList is the type of a list of octetstring representations that
starts with a token:
data TokenList : List Bits8 > Type where
TokenNil : Token xs > TokenList xs
TokenConsToken : Token xs > Whitespace y >
WhitespaceList ys > TokenList zs >
TokenList (xs ++ (y :: ys) ++ zs)
TokenConsSeparate : Token xs > Whitespace y >
WhitespaceList ys > SeparateList zs >
TokenList (xs ++ (y :: ys) ++ zs)
TokenConsOther : Token xs > WhitespaceList ys >
OtherList zs > TokenList (xs ++ ys ++ zs)
PetitHuguenin Expires 23 November 2024 [Page 37]
InternetDraft Formal SPKI SExpr May 2024
SeparateList is the type of a list of octetstring representations
that starts with an octetstring representation that when inserted
after a token will require it to be separated:
data SeparateList : List Bits8 > Type where
SeparateVerbatim : Verbatim xs > SeparateList xs
SeparateVerbatimToken : Verbatim xs > WhitespaceList ys >
TokenList zs > SeparateList (xs ++ ys ++ zs)
SeparateVerbatimSeparate : Verbatim xs >
WhitespaceList ys > SeparateList zs >
SeparateList (xs ++ ys ++ zs)
SeparateVerbatimOther : Verbatim xs > WhitespaceList ys >
OtherList zs > SeparateList (xs ++ ys ++ zs)
SeparateQuotedStringLength : QuotedStringLength xs >
SeparateList xs
SeparateQuotedStringLengthToken : QuotedStringLength xs >
WhitespaceList ys > TokenList zs >
SeparateList (xs ++ ys ++ zs)
SeparateQuotedStringLengthSeparate : QuotedStringLength xs >
WhitespaceList ys > SeparateList zs >
SeparateList (xs ++ ys ++ zs)
SeparateQuotedStringLengthOther : QuotedStringLength xs >
WhitespaceList ys > OtherList zs >
SeparateList (xs ++ ys ++ zs)
SeparateHexadecimal : HexadecimalLength xs >
SeparateList xs
SeparateHexadecimalLengthToken : HexadecimalLength xs >
WhitespaceList ys > TokenList zs >
SeparateList (xs ++ ys ++ zs)
SeparateHexadecimalLengthSeparate : HexadecimalLength xs >
WhitespaceList ys > SeparateList zs >
SeparateList (xs ++ ys ++ zs)
SeparateHexadecimalLengthOther : HexadecimalLength xs >
WhitespaceList ys > OtherList zs >
SeparateList (xs ++ ys ++ zs)
SeparateBase64 : Base64Length xs >
SeparateList xs
SeparateBase64LengthToken : Base64Length xs >
WhitespaceList ys > TokenList zs >
SeparateList (xs ++ ys ++ zs)
SeparateBase64LengthSeparate : Base64Length xs >
WhitespaceList ys > SeparateList zs >
SeparateList (xs ++ ys ++ zs)
SeparateBase64LengthOther : Base64Length xs >
WhitespaceList ys > OtherList zs >
SeparateList (xs ++ ys ++ zs)
PetitHuguenin Expires 23 November 2024 [Page 38]
InternetDraft Formal SPKI SExpr May 2024
OtherList is the type of a list of octetstring representations that
starts with an octetstring representations that when inserted after
a token will not require it to be separated:
data OtherList : List Bits8 > Type where
OtherQuotedString : QuotedString xs > OtherList xs
OtherQuotedStringToken : QuotedString xs >
WhitespaceList ys > TokenList zs >
OtherList (xs ++ ys ++ zs)
OtherQuotedStringSeparate : QuotedString xs >
WhitespaceList ys > SeparateList zs >
OtherList (xs ++ ys ++ zs)
OtherQuotedStringOther : QuotedString xs >
WhitespaceList ys > OtherList zs >
OtherList (xs ++ ys ++ zs)
OtherHexadecimal : Hexadecimal xs > OtherList xs
OtherHexadecimalToken : Hexadecimal xs >
WhitespaceList ys > TokenList zs >
OtherList (xs ++ ys ++ zs)
OtherHexadecimalSeparate : Hexadecimal xs >
WhitespaceList ys > SeparateList zs >
OtherList (xs ++ ys ++ zs)
OtherHexadecimalOther : Hexadecimal xs >
WhitespaceList ys > OtherList zs >
OtherList (xs ++ ys ++ zs)
OtherBase64 : Base64 xs > OtherList xs
OtherBase64Token : Base64 xs > WhitespaceList ys >
TokenList zs > OtherList (xs ++ ys ++ zs)
OtherBase64Separate : Base64 xs >
WhitespaceList ys > SeparateList zs >
OtherList (xs ++ ys ++ zs)
OtherBase64Other : Base64 xs > WhitespaceList ys >
OtherList zs > OtherList (xs ++ ys ++ zs)
OtherHint : WithHint xs > OtherList xs
OtherHintToken : WithHint xs >
WhitespaceList ys > TokenList zs >
OtherList (xs ++ ys ++ zs)
OtherHintSeparate : WithHint xs >
WhitespaceList ys > SeparateList zs >
OtherList (xs ++ ys ++ zs)
OtherHintOther : WithHint xs >
WhitespaceList ys > OtherList zs >
OtherList (xs ++ ys ++ zs)
OtherLists : Lists xs > OtherList xs
OtherListsToken : Lists xs >
WhitespaceList ys > TokenList zs >
OtherList (xs ++ ys ++ zs)
OtherListsSeparate : Lists xs >
PetitHuguenin Expires 23 November 2024 [Page 39]
InternetDraft Formal SPKI SExpr May 2024
WhitespaceList ys > SeparateList zs >
OtherList (xs ++ ys ++ zs)
OtherListsOther : Lists xs >
WhitespaceList ys > OtherList zs >
OtherList (xs ++ ys ++ zs)
And finally the Lists type groups all the possible lists in a sexpr.
data Lists : List Bits8 > Type where
ListsTokenList : WhitespaceList xs > TokenList ys >
WhitespaceList zs > Lists (40 :: xs ++ ys ++ zs ++ [41])
ListsSeparateList : WhitespaceList xs > SeparateList ys >
WhitespaceList zs > Lists (40 :: xs ++ ys ++ zs ++ [41])
ListsOtherList : WhitespaceList xs > OtherList ys >
WhitespaceList zs > Lists (40 :: xs ++ ys ++ zs ++ [41])
ListsEmptyList : WhitespaceList xs >
Lists (40 :: xs ++ [41])
3.9.3. Validation
Here we prove that all the examples in section 5 of the original
document except the last one are valid instances of the Lists type:
Here are some examples of encodings of lists:
(a b c)
( a ( b c ) ( ( d e ) ( e f ) ) )
(11:certificate(6:issuer3:bob)(7:subject5:alice))
({3Rt=} "1997" murphy 3:{XC++})
* (a b c)
testLists1 : Lists [40, 97, 32, 98, 32, 99, 41]
testLists1 = ListsTokenList []
(TokenConsToken (MkToken 97 Refl []) (MkWhitespace 32 Refl)
[] (TokenConsToken (MkToken 98 Refl [])
(MkWhitespace 32 Refl) [] (TokenNil (MkToken 99 Refl []))))
[]
* ( a ( b c ) ( ( d e ) ( e f ) ) )
PetitHuguenin Expires 23 November 2024 [Page 40]
InternetDraft Formal SPKI SExpr May 2024
testLists2 : Lists [40, 32, 97, 32, 40, 32, 98, 32, 99, 32, 41,
32, 40, 32, 40, 32, 100, 32, 101, 32, 41, 32, 40, 32, 101,
32, 102, 32, 41, 32, 41, 32, 32, 41]
testLists2 = ListsTokenList[MkWhitespace 32 Refl]
(TokenConsOther (MkToken 97 Refl []) [MkWhitespace 32 Refl]
(OtherListsOther (ListsTokenList [MkWhitespace 32 Refl]
(TokenConsToken (MkToken 98 Refl []) (MkWhitespace 32 Refl)
[] (TokenNil (MkToken 99 Refl []))) [MkWhitespace 32 Refl])
[MkWhitespace 32 Refl] (OtherLists (ListsOtherList
[MkWhitespace 32 Refl] (OtherListsOther (ListsTokenList
[MkWhitespace 32 Refl] (TokenConsToken (MkToken 100 Refl [])
(MkWhitespace 32 Refl) [] (TokenNil (MkToken 101 Refl [])))
[MkWhitespace 32 Refl]) [MkWhitespace 32 Refl] (OtherLists
(ListsTokenList [MkWhitespace 32 Refl] (TokenConsToken
(MkToken 101 Refl []) (MkWhitespace 32 Refl) [] (TokenNil
(MkToken 102 Refl []))) [MkWhitespace 32 Refl])))
[MkWhitespace 32 Refl])))) [MkWhitespace 32 Refl,
MkWhitespace 32 Refl]
* (11:certificate(6:issuer3:bob)(7:subject5:alice))
testLists3 : Lists [40, 49, 49, 58, 99, 101, 114, 116, 105,
102, 105, 99, 97, 116, 101, 40, 54, 58, 105, 115, 115,
117, 101, 114, 51, 58, 98, 111, 98, 41, 40, 55, 58, 115,
117, 98, 106, 101, 99, 116, 53, 58, 97, 108, 105, 99,
101, 41, 41]
testLists3 = ListsSeparateList [] (SeparateVerbatimOther
(MkVerbatim [99, 101, 114, 116, 105, 102, 105, 99, 97,
116, 101]) [] (OtherListsOther (ListsSeparateList []
(SeparateVerbatimSeparate (MkVerbatim [105, 115, 115,
117, 101, 114]) [] (SeparateVerbatim (MkVerbatim [98,
111, 98]))) []) [] (OtherLists (ListsSeparateList []
(SeparateVerbatimSeparate (MkVerbatim [115, 117, 98,
106, 101, 99, 116]) [] (SeparateVerbatim (MkVerbatim
[97, 108, 105, 99, 101]))) [])))) []
3.10. Advanced SExpr Transport
3.10.1. Analysis
Section 6.3 of the original sexpr document states:
PetitHuguenin Expires 23 November 2024 [Page 41]
InternetDraft Formal SPKI SExpr May 2024
NOTE: '\\' line wrapping per RFC 8792
The "advanced transport" representation is intended to provide
\more
flexible and readable notations for documentation, design, \
\debugging,
and (in some cases) user interface.
The advanced transport representation allows all of the \
\representation
forms described above, include quoted strings, base64 and \
\hexadecimal
representation of strings, tokens, representations of strings with
omitted lengths, and so on.
Because this transport is aimed at users, we also permit to add white
spaces before and after a sexpr.
3.10.2. Formalization
SExpr is the type of advanced transport for valid sexpr:
data SExpr : List Bits8 > Type where
SExprRepresentation : WhitespaceList xs >
Representation ys > WhitespaceList zs >
SExpr (xs ++ ys ++ zs)
SExprWithHint : WhitespaceList xs > WithHint ys >
WhitespaceList zs > SExpr (xs ++ ys ++ zs)
SExprList : WhitespaceList xs > Lists ys >
WhitespaceList zs > SExpr (xs ++ ys ++ zs)
3.10.3. Validation
Here we prove that the example in section 5 of the original document
is a valid instance of the SExpr type:
NOTE: '\\' line wrapping per RFC 8792
A list is a finite sequence of zero or more simpler \
\Sexpressions. A list
may be represented by using parentheses to surround the \
\sequence of encodings
of its elements, as in:
(abc (de #6667#) "ghi jkl")
* (abc (de #6667#) "ghi jkl")
PetitHuguenin Expires 23 November 2024 [Page 42]
InternetDraft Formal SPKI SExpr May 2024
testSExpr1 : SExpr [40, 97, 98, 99, 32, 40, 100, 101, 32, 35,
54, 54, 54, 55, 35, 41, 32, 34, 103, 104, 105, 32, 106, 107,
108, 34, 41]
testSExpr1 = SExprList [] (ListsTokenList [] (TokenConsOther
(MkToken 97 Refl [MkTokenChar 98 Refl, MkTokenChar 99 Refl])
[MkWhitespace 32 Refl] (OtherListsOther (ListsTokenList []
(TokenConsOther (MkToken 100 Refl [MkTokenChar 101 Refl])
[MkWhitespace 32 Refl] (OtherHexadecimal (MkHexadecimal []
[HexLL' 102 [] [], HexLL' 103 [][]]))) [])
[MkWhitespace 32 Refl] (OtherQuotedString (MkQuotedString
[Ascii 103 Refl, Ascii 104 Refl, Ascii 105 Refl,
Ascii 32 Refl, Ascii 106 Refl, Ascii 107 Refl,
Ascii 108 Refl])))) []) []
3.11. Canonical SExpr Transport
3.11.1. Analysis
Section 6.1 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
This canonical representation is used for digital signature \
\purposes,
transmission, etc. It is uniquely defined for each \
\Sexpression. It
is not particularly readable, but that is not the point. \
\It is
intended to be very easy to parse, to be reasonably economical, \
\and to
be unique for any Sexpression.
The "canonical" form of an Sexpression represents each \
\octetstring
in verbatim mode, and represents each list with no blanks \
\separating
elements from each other or from the surrounding parentheses.
3.11.2. Formalization
The canonical transport is actually a profile of the advanced
transport, so we can reuse our previous types:
First we declare an abstract type for the canonical sexpr, as it is
an inductive type:
data CanonicalSExpr : List Bits8 > Type
PetitHuguenin Expires 23 November 2024 [Page 43]
InternetDraft Formal SPKI SExpr May 2024
Then a type for a list of canonical sexpr:
data CanonicalSExprList : List Bits8 > Type where
Nil : CanonicalSExprList []
(::) : CanonicalSExpr xs > CanonicalSExprList ys >
CanonicalSExprList (xs ++ ys)
And finally our concrete type for a canonical sexpr:
data CanonicalSExpr : List Bits8 > Type where
MkCanonical : Verbatim xs > CanonicalSExpr xs
MkCanonicalHint : Verbatim xs > Verbatim ys >
CanonicalSExpr (91 :: xs ++ [93] ++ ys)
MkCanonicalList : CanonicalSExprList xs >
CanonicalSExpr (40 :: xs ++ [41])
3.11.3. Validation
Here we prove that all the examples in section 6.1 of the original
document are valid instances of the Canonical type:
NOTE: '\\' line wrapping per RFC 8792
Here are some examples of canonical representations of \
\Sexpressions:
(6:issuer3:bob)
(4:icon[12:image/bitmap]9:xxxxxxxxx)
(7:subject(3:ref5:alice6:mother))
* (6:issuer3:bob)
testCanonical1 : CanonicalSExpr [40, 54, 58, 105, 115, 115,
117, 101, 114, 51, 58, 98, 111, 98, 41]
testCanonical1 = MkCanonicalList [MkCanonical
(MkVerbatim [105, 115, 115, 117, 101, 114]),
MkCanonical (MkVerbatim [98, 111, 98])]
* (4:icon[12:image/bitmap]9:xxxxxxxxx)
PetitHuguenin Expires 23 November 2024 [Page 44]
InternetDraft Formal SPKI SExpr May 2024
testCanonical2 : CanonicalSExpr [40, 52, 58, 105, 99, 111, 110,
91, 49, 50, 58, 105, 109, 97, 103, 101, 47, 98, 105, 116,
109, 97, 112, 93, 57, 58, 120, 120, 120, 120, 120, 120,
120, 120, 120, 41]
testCanonical2 = MkCanonicalList [MkCanonical
(MkVerbatim [105, 99, 111, 110]), MkCanonicalHint
(MkVerbatim [105, 109, 97, 103, 101, 47, 98, 105, 116,
109, 97, 112]) (MkVerbatim [120, 120, 120, 120, 120, 120,
120, 120, 120])]
* (7:subject(3:ref5:alice6:mother))
testCanonical3 : CanonicalSExpr [40, 55, 58, 115, 117, 98, 106,
101, 99, 116, 40, 51, 58, 114, 101, 102, 53, 58, 97, 108,
105, 99, 101, 54, 58, 109, 111, 116, 104, 101, 114, 41, 41]
testCanonical3 = MkCanonicalList [MkCanonical
(MkVerbatim [115, 117, 98, 106, 101, 99, 116]),
MkCanonicalList [MkCanonical (MkVerbatim [114, 101, 102]),
MkCanonical (MkVerbatim [97, 108, 105, 99, 101]),
MkCanonical (MkVerbatim [109, 111, 116, 104, 101, 114])]]
3.12. Basic SExpr Transport
3.12.1. Analysis
Section 6.2 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
There are two forms of the "basic transport" representation:
 the canonical representation
 an rfc2045 base64 representation of the canonical \
\representation,
surrounded by braces.
The transport mechanism is intended to provide a universal means \
\of
representing Sexpressions for transport from one machine to \
\another.
There is no possible BNF that is sound for a base 64 representation
of an underlying sexpr.
PetitHuguenin Expires 23 November 2024 [Page 45]
InternetDraft Formal SPKI SExpr May 2024
3.12.2. Formalization
The basic transport is also a profile of the advanced transport, so
we can reuse some previous types:
We first redefine Base64Full without white spaces:
data BasicBase64Full : List Bits8 > Type where
MkBasicBase64Full : (x1 : Bits8) > (x2 : Bits8) >
(x3 : Bits8) >
BasicBase64Full (b641 x1 ++ b642 x1 x2 ++ b643 x2 x3 ++
b644 x3s)
Then a list of these:
namespace BasicBase64
public export
data BasicBase64List : List Bits8 > Type where
Nil : BasicBase64List []
(::) : BasicBase64Full xs > BasicBase64List ys >
BasicBase64List (xs ++ ys)
And a type for a base 64 encoding for lengths that are not a multiple
of 3:
data BasicBase64End : List Bits8 > Type where
BasicEndOnePadPad : (x1 : Bits8) >
BasicBase64End (b641 x1 ++ b642 x1 0 ++ [61, 61])
BasicEndOnePad : (x1 : Bits8) >
BasicBase64End (b641 x1 ++ b642 x1 0 ++ [61])
BasicEndOne : (x1 : Bits8) >
BasicBase64End (b641 x1 ++ b642 x1 0)
BasicEndTwoPad : (x1 : Bits8) > (x2 : Bits8) >
BasicBase64End (b641 x1 ++ b642 x1 x2 ++ b643 x2 0 ++ [61])
BasicEndTwo : (x1 : Bits8) > (x2 : Bits8) >
BasicBase64End (b641 x1 ++ b642 x1 x2 ++ b643 x2 0)
And a basic base 64 type:
data BasicBase64 : List Bits8 > Type where
BasicBase64Mult3 : BasicBase64List xs > BasicBase64 xs
BasicBase64Non : BasicBase64List xs > BasicBase64End ys >
BasicBase64 (xs ++ ys)
Then we need to define three base64 encoding functions, one for each
variant:
PetitHuguenin Expires 23 November 2024 [Page 46]
InternetDraft Formal SPKI SExpr May 2024
base64 : List Bits8 > List Bits8
base64 [] = []
base64 [x1] = b641 x1 ++ b642 x1 0 ++ [61, 61]
base64 [x1, x2] = b641 x1 ++ b642 x1 x2 ++ b643 x2 0 ++ [61]
base64 (x1 :: x2 :: x3 :: xs) = b641 x1 ++ b642 x1 x2 ++
b643 x2 x3 ++ b644 x3 ++ base64 xs
base64OnePad : List Bits8 > List Bits8
base64OnePad [] = []
base64OnePad [x1] = b641 x1 ++ b642 x1 0 ++ [61]
base64OnePad [x1, x2] = b641 x1 ++ b642 x1 x2 ++ b643 x2 0
base64OnePad (x1 :: x2 :: x3 :: xs) = b641 x1 ++ b642 x1 x2 ++
b643 x2 x3 ++ b644 x3 ++ base64OnePad xs
base64NoPad : List Bits8 > List Bits8
base64NoPad [] = []
base64NoPad [x1] = b641 x1 ++ b642 x1 0
base64NoPad [x1, x2] = b641 x1 ++ b642 x1 x2 ++ b643 x2 0
base64NoPad (x1 :: x2 :: x3 :: xs) = b641 x1 ++ b642 x1 x2 ++
b643 x2 x3 ++ b644 x3 ++ base64NoPad xs
And finally our type for a brace notation for base 64:
data BasicSExpr : List Bits8 > Type where
MkBasicCanonical : CanonicalSExpr xs > BasicSExpr xs
MkBasicBase64 : CanonicalSExpr xs > BasicBase64 ys >
(prf : (base64 xs == ys) === True) >
BasicSExpr (123 :: ys ++ [123])
MkBasicBase64OnePad : CanonicalSExpr xs > BasicBase64 ys >
(prf : (base64OnePad xs == ys) === True) >
BasicSExpr (123 :: ys ++ [123])
MkBasicBase64NoPad : CanonicalSExpr xs > BasicBase64 ys >
(prf : (base64NoPad xs == ys) === True) >
BasicSExpr (123 :: ys ++ [123])
3.12.3. Validation
Here we prove that the first example in section 6.2 of the original
document is a valid instance of the Basic type:
Here are some examples of an Sexpression represented in basic
transport mode:
(1:a1:b1:c)
{KDE6YTE6YjE6YykA}
(this is the same Sexpression encoded in base64)
PetitHuguenin Expires 23 November 2024 [Page 47]
InternetDraft Formal SPKI SExpr May 2024
* (1:a1:b1:c)
testBasic1 : BasicSExpr [40, 49, 58, 97, 49, 58, 98, 49, 58,
99, 41]
testBasic1 = MkBasicCanonical (MkCanonicalList [MkCanonical
(MkVerbatim [97]), MkCanonical (MkVerbatim [98]), MkCanonical
(MkVerbatim [99])])
3.13. ArrayLayout
3.13.1. Analysis
Section 8.2 of the original sexpr document states:
NOTE: '\\' line wrapping per RFC 8792
Here each Sexpression is represented as a contiguous array of \
\bytes.
The first byte codes the "type" of the Sexpression:
01 octetstring
02 octetstring with displayhint
03 beginning of list (and 00 is used for "end of
\list")
Each of the three types is immediately followed by a kbyte \
\integer
indicating the size (in bytes) of the following representation.\
\ Here
k is an integer that depends on the implementation, it might be
anywhere from 2 to 8, but would be fixed for a given \
\implementation;
it determines the size of the objects that can be handled. The \
\transport
and canonical representations are independent of the choice of \
\k made by
the implementation.
Although the length of lists are not given in the usual \
\Sexpression
notations, it is easy to fill them in when parsing; when you \
\reach a
rightparenthesis you know how long the list representation \
\was, and
where to go back to fill in the missing length.
PetitHuguenin Expires 23 November 2024 [Page 48]
InternetDraft Formal SPKI SExpr May 2024
The endianness of the length field is not specified, so we assume
that both little and big endianness can be used.
Furthermore section 8.2.1 states:
This is represented as follows:
01
Section 8.2.2 states:
This is represented as follows:
02
01 /* for displaytype */
01 /* for octetstring */
And section 8.2.3 states:
This is represented as
03 ... 00
3.13.2. Formalization
First we define a type for the endianness of the length:
data Endianness = Big  Little
Then a function that converts a natural number into a memory
representation of a specified endianness and length:
convert' : Nat > Nat > List Bits8
convert' 0 _ = []
convert' (S k) n =
let (d, m) = divmodNatNZ n 256 SIsNonZero
in cast m :: convert' k d
convert : Endianness > Nat > Nat > List Bits8
convert Big k j = convert' k j
convert Little k j = reverse (convert' k j)
Then we define a type for the array representation of an octet
string:
PetitHuguenin Expires 23 November 2024 [Page 49]
InternetDraft Formal SPKI SExpr May 2024
data ArrayOctetString :
Endianness > Nat > List Bits8 > Type where
MkArrayOctetString : (xs : List Bits8) >
ArrayOctetString e l (1 :: convert e l (length xs) ++ xs)
Then for an octetstring with displayhint:
data ArrayWithHint : Endianness > Nat > List Bits8 >
Type where
MkArrayWithHint : ArrayOctetString e l xs >
ArrayOctetString e l ys >
ArrayWithHint e l (2 :: convert e l (length xs +
length ys) ++ xs ++ ys)
As usual an abstract type for an inductive type:
data ArraySExpr : Endianness > Nat > List Bits8 > Type
Then a list of memory array:
namespace Array
public export
data ArrayList : Endianness > Nat > List Bits8 >
Type where
Nil : ArrayList e l []
(::) : ArraySExpr e l xs > ArrayList e l ys >
ArrayList e l (xs ++ ys)
And finally the array memory type:
data ArraySExpr : Endianness > Nat > List Bits8 > Type where
ArraySExprOctetString : ArrayOctetString e l xs >
ArraySExpr e l xs
ArraySExprWithHint : ArrayWithHint e l xs >
ArraySExpr e l xs
ArraySExprList : ArrayList e l xs >
ArraySExpr e l (3 :: convert e l (1 + length xs) ++
xs ++ [0])
3.13.3. Verification
Here we prove that all the examples in section 8.2 of the original
document are valid instances of the ArraySExpr type:
* abc
PetitHuguenin Expires 23 November 2024 [Page 50]
InternetDraft Formal SPKI SExpr May 2024
For example (here k = 2)
01 0003 a b c
testArray1 : ArraySExpr Little 2 [1, 0, 3, 97, 98, 99]
testArray1 = ArraySExprOctetString
(MkArrayOctetString [97, 98, 99])
* [gif] #61626364#
For example, the Sexpression
[gif] #61626364#
would be represented as (with k = 2)
02 000d
01 0003 g i f
01 0004 61 62 63 64
testArray2 : ArraySExpr Little 2 [2, 0, 13, 1, 0, 3, 103,
105, 102, 1, 0, 4, 97, 98, 99, 100]
testArray2 = ArraySExprWithHint (MkArrayWithHint
(MkArrayOctetString [103, 105, 102])
(MkArrayOctetString [97, 98, 99, 100]))
* (abc [d]ef (g))
NOTE: '\\' line wrapping per RFC 8792
For example, the list (abc [d]ef (g)) is represented in memory \
\as (with k=2)
03 001b
01 0003 a b c
02 0009
01 0001 d
01 0002 e f
03 0005
01 0001 g
00
00
PetitHuguenin Expires 23 November 2024 [Page 51]
InternetDraft Formal SPKI SExpr May 2024
testArray3 : ArraySExpr Little 2 [3, 0, 27, 1, 0, 3, 97, 98,
99, 2, 0, 9, 1, 0, 1, 100, 1, 0, 2, 101, 102, 3, 0, 5, 1,
0, 1, 103, 0, 0]
testArray3 = ArraySExprList [ArraySExprOctetString
(MkArrayOctetString [97, 98, 99]), ArraySExprWithHint
(MkArrayWithHint (MkArrayOctetString [100])
(MkArrayOctetString [101, 102])), ArraySExprList
[ArraySExprOctetString (MkArrayOctetString [103])]]
4. Informative References
[ComputerateSpecification]
PetitHuguenin, M., "Computerate Specification", Work in
Progress, InternetDraft, draftpetithuguenincomputerate
specification, 3 February 2024,
.
[Idris2] "Documentation for the Idris 2 Language — Idris2 0.0
documentation", Accessed 31 January 2023,
.
[KandR] Kernighan, B. W. and D. M. Ritchie, "The C programming
language", 1 January 1988.
[RFC8792] Watsen, K., Auerswald, E., Farrel, A., and Q. Wu,
"Handling Long Lines in Content of InternetDrafts and
RFCs", RFC 8792, DOI 10.17487/RFC8792, June 2020,
.
[SPKISExpr]
Rivest, R. L. and D. E. Eastlake 3rd, "SPKI
SExpressions", Work in Progress, InternetDraft, draft
rivestsexp, 16 April 2024,
.
Appendix A. Code Extraction and Verification
To verify that the proofs in this document are correct, the first
step is to install [Idris2].
Then the various Idris2 fragments in this document can be extracted
as a complete file by running the following command:
xmllint noent nocdata \
xpath "//sourcecode[@name='formalsexpr.idr']/text()" \
draftpetithugueninufmrgformalsexpr04.xml \
 sed "s/<//g; s/amp;//g" >formalsexpr.idr
PetitHuguenin Expires 23 November 2024 [Page 52]
InternetDraft Formal SPKI SExpr May 2024
And finally the proofs can be validated by using the following
command
idris2 q c formalsexpr.idr
Acknowledgements
Thanks to Erik Auerswald and Stephane Bryant for the comments,
suggestions and questions that helped improve this document.
No technology that cannot explain its own results (LLM, AI/ML) have
been involved in the creation of this document.
Changelog
Since draftpetithugueninufmrgformalsexpr03:
* more nits and clarifications
* add proof of equivalence using symmetry
* change default displayhint to application/octetstream
Since draftpetithugueninufmrgformalsexpr02:
* fix another instance of incorrect rendering
* reformat some example for clarity
* add "Equality of OctetString" section
* nits and some clarification
Since draftpetithugueninufmrgformalsexpr01:
* incorrect rendering of a string with #
* add RFC 8792 headers
* remove a comment about tokens that was incorrect
* add REPL example to display octetstrings
Since draftpetithugueninufmrgformalsexpr00:
* add forgotten proofs for testList2 and testList3
* some editing for clarity
* many nit fixes
Author's Address
Marc PetitHuguenin
Impedance Mismatch LLC
Email: marc@petithuguenin.org
PetitHuguenin Expires 23 November 2024 [Page 53]