io7m | single-page | multi-page | epub | Cedarbridge Language Specification 2.0.0

Cedarbridge Language Specification 2.0.0

DATE 2020-12-18T00:00:00+00:00
DESCRIPTION Specification for the Cedarbridge language.
IDENTIFIER c3312787-3be5-430d-a78c-cdd66e271a2b
LANGUAGE en
SOURCE https://www.io7m.com/software/cedarbridge/
TITLE Cedarbridge Language Specification 2.0.0

Table Of Contents

1. Notational Conventions

1.1. Unicode

1
The specification makes reference to the Unicode character set which, at the time of writing, is at version 13.0.0. The specification often references specific Unicode characters, and does so using the standard notation U+NNNN, where N represents a hexadecimal digit. For example, U+03BB corresponds to the lowercase lambda symbol λ.

1.2. EBNF

1
The specification gives grammar definitions in ISO/IEC 14977:1996 Extended Backus-Naur form.
2
Because EBNF was designed prior to the existence of Unicode, it is necessary to extend the syntax to be able to refer to Unicode characters in grammar definitions. This specification makes use of the standard unicode U+NNNN syntax in grammar definitions, to refer to specific Unicode characters. It also makes use of the syntax \p{t} which should be understood to represent any Unicode character with the property t. For example, \p{Lowercase_Letter} describes the set of characters that are both letters and are lowercase. The syntax \P{t} should be understood as the negation of \p{t}; it describes the set of characters without the property t.

1.3. S-Expressions

1
The Cedarbridge language uses s-expressions as the base for all syntax. An s-expression is described by the following EBNF grammar:

1.3.2. S-Expression Syntax

symbol_character =
  ? not (")" | "(" | "[" | "]" | U+0022 | \p{Separator}) ? ;

symbol =
  symbol_character , { symbol_character } ;

quoted_character =
  ? not U+0022 ? ;

quoted_string =
  (quoted_character | escape) , { (quoted_character | escape) } ;

escape =
    escape_carriage
  | escape_newline
  | escape_tab
  | escape_quote
  | escape_unicode4
  | escape_unicode8 ;

escape_carriage =
  "\r" ;

escape_newline =
  "\n" ;

escape_quote =
  "\" , U+0022 ;

escape_tab =
  "\t" ;

escape_unicode4 =
  "\u" ,
  hex_digit , hex_digit , hex_digit , hex_digit ;

escape_unicode8 =
  "\u" ,
  hex_digit , hex_digit , hex_digit , hex_digit ,
  hex_digit , hex_digit , hex_digit , hex_digit ;

hex_digit =
  "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" | "0" |
  "a" | "A" | "b" | "B" | "c" | "C" | "d" | "D" | "e" | "E" | "f" | "F" ;

expression =
    symbol
  | quoted_string
  | "[" , { expression } , "]"
  | "(" , { expression } , ")" ;
3
As shown, the Cedarbridge language uses an extension of basic s-expressions that allow for the optional use of either square brackets or parentheses to increase the readability of large nested expressions. These should be treated as interchangeable, but must be correctly balanced as shown by the grammar. For example, the expression [] is semantically equivalent to (), but the expression [) is invalid.

1.4. Sets

1
Where the specification refers to sets, it is referring to sets as defined in Zermelo-Fraenkel set theory.

1.4.2. ZFC

Notation Description
e ∈ A e is an element of the set A
e ∉ A e is not an element of the set A
{ x₀, x₁, ... xₙ } A set consisting of values from x₀ to xₙ
{ e ∈ A | p(e) } A set consisting of the elements of A for which the proposition p holds
|A| The cardinality of the set A; a measure of the number of elements in A
∅ The empty set
𝔹 The booleans
ℕ The natural numbers
ℝ The real numbers
ℤ The integers
[a, b] A closed interval in a set (given separately or implicit from the types of a and b), from a to b, including a and b
(a, b] A closed interval in a set (given separately or implicit from the types of a and b), from a to b, excluding a but including b
[a, b) A closed interval in a set (given separately or implicit from the types of a and b), from a to b, including a but excluding b
(a, b) A closed interval in a set (given separately or implicit from the types of a and b), from a to b, excluding a and b
A ⊂ B A is a subset of, and is not equal to, B
A ⊆ B A is a subset of, or is equal to, B
A ∩ B The smallest set of elements that appear in both A and B (intersection).

1.5. Logic

1
The specification uses the following notation from propositional logic:

1.5.2. Propositional Logic

Notation Description
∀x. P x Universal quantification; for all x the proposition P holds for x
∃x. P x Existential quantification; there exists some x such that the proposition P holds for x
P ⇒ Q Implication; P implies Q
P ⋀ Q Conjunction; P and Q

1.6. Type Rules

1
Declarative type rules describe the precise rules for assigning types to terms. If no type rule matches a term, then that term is considered ill-typed.
2
Type rules are given as zero or more premises, and a single conclusion, separated by a horizontal line. For a given rule, when all of the premises are true, then the conclusion is true. If a rule has no premises then the rule is taken as an axiom.
3
The gamma symbol Γ (U+0393) represents the current typing environment and can be thought of as a mapping from distinct variables to their types, with the set of variables in environment denoted by dom(Γ) (the domain of Γ). The notation Γ ⊢ P reads "Γ implies P" and is used in type rules to assign types to terms. The empty typing environment is represented by ∅ (U+2205). The diamond symbol ◇ (U+25C7) should be read as "is well-formed", so Γ ⊢ ◇ should be read as "the current typing environment is well-formed". The concept of well-formedness is often type-system-specific and is usually described when the rules are given.

1.6.4. Type Rule Notation

Notation Description Example
Γ The current typing environment Γ
∅ The empty typing environment ∅
Γ, x The typing environment Γ extended with the variable x. Usually accompanied with a side condition that x does not appear in dom(Γ). Γ, x where x ∉ dom(Γ)
dom(Γ) The set of distinct variables in Γ dom((∅, x, y)) = { x, y }
Γ ⊢ P The environment Γ implies P Γ ⊢ 23 : ℕ (in the current typing environment, 23 is of type ℕ)
Γ ⊢ ◇ The environment Γ is well-formed ∅ ⊢ ◇ (the empty typing environment is well-formed)

2. Concepts

2.1. Overview

1
The Cedarbridge language is designed to describe schemas that describe message-based protocols. Schemas consist of a set of packages, each containing types and protocols. Type declarations express the structure of values exchanged in message protocols, and protocol declarations express which types are present in each defined version of a protocol.
2
This version of the specification describes the Cedarbridge language version 1.0. This version of the language can be requested explicitly by schema authors by using the language statement.

2.2. Compilation Units

1
The text of a Cedarbridge schema is a combination of the texts of separate compilation units, where a compilation unit typically corresponds to a file in the operating system under which the compiler is running.
2
Compilation units consist of a series of s-expressions separated by whitespace.

2.3. Schema Context

1
This specification makes references to a schema context. The schema context can be thought of as the current state of the schema being constructed during the execution of the language compiler. For example, the package statement modifies the schema context by introducing a new package name and setting the new package as the current package to which all subsequent statements will apply.

2.4. Statements

1
A statement in the Cedarbridge language can be seen as an instruction that performs some action on the current schema context (such as introducing a new type, introducing a new package, importing a package into the current scope, etc), yielding a new context that may be changed in some manner.

2.5. Packages

1
A package is the top level organizational unit for schema objects. A package has a unique fully-qualified name of the form:

2.5.2. Package Name

package_name_segment =
  [a-z] , { [a-z0-9_] } ;

package_name =
  package_name_segment , { "." , package_name_segment } ;
3
An example of a valid package name is com.io7m.cedarbridge.

2.6. Types

1
A type in the Cedarbridge language is a basic description of the structure of a value. A type has a unique name within a package, and the format of valid type names is as follows:

2.6.2. Type Name

type_name =
  [A-Z] , { [a-z0-9A-Z] } ;

2.7. Protocols

1
A protocol in the Cedarbridge language is a set of versions, each of which contains a set of types. A type can be present in any number of protocols and protocol versions concurrently. A protocol has a unique name within a package, and the format of valid protocol names matches that of types.

2.7.2. Protocol (Type) Name

type_name =
  [A-Z] , { [a-z0-9A-Z] } ;

2.8. Comments

1
The Cedarbridge language uses the U+003B SEMICOLON character to denote line comments. When encountered outside of a quoted string, any text between the ; character and the next end-of-line character is ignored.

3. Statements

3.1. language

3.1.1. Description

1
language - Declare the language that will be used.

3.1.2. Overview

1
The language statement declares which language will be used for the subsequent statements in the compilation unit.

3.1.3. Syntax

3.1.3.1. Language Syntax

language_name =
  [a-z] , { [a-zA-Z0-9_] } ;

language_version =
  [0-9] , { [0-9] } ;

language =
  "(" , "language" , language_name , language_version , language_version ")" ;

3.1.4. Semantics

1
A language statement, if present, MUST be the first statement in a compilation unit.
2
The language statement can appear at most once in a compilation unit.
3
If a language statement names an unrecognized language, parsing of the compilation unit MUST be aborted, and all subsequent statements in the compilation unit ignored.
4
If a language statement names an unrecognized language major version, parsing of the compilation unit MUST be aborted, and all subsequent statements in the compilation unit ignored.
5
If a language statement names an unrecognized language minor version, parsing of the compilation unit MAY produce a warning, but compilation of the unit must continue as if known minor version had been specified [1].

3.1.5. Example

1
The following statement declares that the compilation unit is written in Cedarbridge 1.0:

3.1.5.2. Language Example

(language cedarbridge 1 0)

Footnotes

1
As all minor versions within a given major version are strictly compatible, the assumption is safe.
References to this footnote: 1

3.2. package

3.2.1. Description

1
package - Begin the declaration of a package.

3.2.2. Overview

1
The package statement begins the declaration of a package.

3.2.3. Syntax

3.2.3.1. Package Syntax

package =
  "(" , "package" , package_name , ")" ;

3.2.4. Semantics

1
A package statement that names a package p sets the current package of the schema context to p. There can be at most one current package in the schema context at any given time.
2
If the package statement is evaluated when the schema context already has a current package, the statement is rejected with an error.
3
If the package statement is evaluated with package name r, where r is already defined within the schema context, the statement is rejected with an error.
4
The package named by a package statement is defined iff the compilation of all subsequent statements in the compilation unit succeeds. Once a package is defined, it becomes accessible to other packages via the use of import statements. At the end of the compilation unit, the current package of the schema context becomes unset.

3.2.5. Example

1
The following statement begins the declaration of a package named com.io7m.cedarbridge:

3.2.5.2. Package Example

(package com.io7m.cedarbridge)

3.3. import

3.3.1. Description

1
import - Import a package.

3.3.2. Overview

1
The import statement imports a package for use in the current package.

3.3.3. Syntax

3.3.3.1. Import Syntax

import =
  "(" , "import" , package_name , package_name_segment , ")" ;

3.3.4. Semantics

1
An import statement (import p q) makes the type declarations in package p visible via qualification using the short name q. For example, if a type T was declared in p, it can be used in a type declaration in the current package by referring to the type as q:T. Formally, a package s imports a package t if s contains an (import t x) statement, for any x.
2
It is an error for two import statements to use the same short name.
3
It is an error for any package to import itself directly or indirectly. That is, the graph of packages produced by packages importing other packages must be free of cycles. More formally, it is an error for any of the following conditions to be true:

3.3.4.4. Package Import Cycles

  • The package p imports p.
  • There is a sequence of packages d, d₀, d₁, ..., dₙ such that d imports d₀, and for all m where 0 <= m < n, dₘ imports d₍ₘ₊₁₎, and dₙ imports d.
5
An import statement, if present, MUST occur with a package set in the current schema context. In practical terms, this means that import statements MUST appear after the package statement in a given compilation unit.

3.3.5. Example

1
The following statement imports a package named com.io7m.cedarbridge and makes it accessible as cb:

3.3.5.2. Import Example

(import com.io7m.cedarbridge cb)

3.4. record

3.4.1. Description

1
record - Declare a record type

3.4.2. Overview

1
The record statement declares a new record type.

3.4.3. Syntax

3.4.3.1. Record Syntax

type_parameter_name =
  [A-Z] , { [A-Z0-9_] } ;

field_name =
  [a-z] , { [a-zA-Z0-9] } ;

field_declaration =
  "(" , "field" , field_name , type_expression , ")" ;

type_parameter_declaration =
  "(" , "parameter" , type_parameter_name , ")" ;

record_declaration =
  "(" , "record" , type_name , { field_declaration | type_parameter_declaration | documentation_declaration } , ")" ;

3.4.4. Semantics

1
A record statement, if present, MUST occur with a package set in the current schema context. In practical terms, this means that record statements MUST appear after the package statement in a given compilation unit.
2
A record statement is a type declaration.
3
The statement (record T ...) introduces a new type name T within the current package in the schema context. Type names are unique within a package; it is an error for two or more type declarations to name the same type.
4
The names of fields declared using field declarations within a record statement are unique within that record type. It is an error for two or more fields within a record to have the same name.
5
The declaration order of fields within a record type is significant; changing the order of field declarations will change the semantics and serialized form of values of the record type.
6
The names of type parameters declared using parameter declarations within a record statement are unique within that record type. It is an error for two or more type parameters within a record to have the same name.
7
The declaration order of type parameters with respect to other type parameters within a record type is significant; changing the order of parameter declarations will change the semantics and serialized form of values of the record type. The declaration order of type parameters with respect to field declarations is not significant.
8
The precise type rules for record type declarations are described in the typing rules section for type expressions.
9
For a given field (field x t), the type expression t must have kind *.

3.4.5. Example

1
The following statement declares a parameterized Pair type with two fields:

3.4.5.2. Record Example

(record Pair
  (parameter A)
  (parameter B)
  (field f0 A)
  (field f1 B))

3.5. variant

3.5.1. Description

1
variant - Declare a variant type

3.5.2. Overview

1
The variant statement declares a new variant type.

3.5.3. Syntax

3.5.3.1. Variant Syntax

type_parameter_name =
  [A-Z] , { [A-Z0-9_] } ;

case_name =
  [A-Z] , { [a-zA-Z0-9] } ;

case_declaration =
  "(" , "case" , case_name , { field_declaration | documentation_declaration } , ")" ;

variant_declaration =
  "(" , "variant" , type_name , { case_declaration | type_parameter_declaration | documentation_declaration } , ")" ;

3.5.4. Semantics

1
A variant statement, if present, MUST occur with a package set in the current schema context. In practical terms, this means that variant statements MUST appear after the package statement in a given compilation unit.
2
A variant statement is a type declaration.
3
The statement (variant T ...) introduces a new type name T within the current package in the schema context. Type names are unique within a package; it is an error for two or more type declarations to name the same type.
4
The names of cases declared using case declarations within a variant statement are unique within that variant type. It is an error for two or more cases within a variant to have the same name.
5
The declaration order of cases within a variant type is significant; changing the order of case declarations will change the semantics and serialized form of values of the variant type.
6
The names of type parameters declared using parameter declarations within a variant statement are unique within that variant type. It is an error for two or more type parameters within a variant to have the same name.
7
The declaration order of type parameters with respect to other type parameters within a variant type is significant; changing the order of parameter declarations will change the semantics and serialized form of values of the variant type. The declaration order of type parameters with respect to case declarations is not significant.
8
The precise type rules for variant type declarations are described in the typing rules section for type expressions.
9
For a given field (field x t) within a case declaration, the type expression t must have kind *.

3.5.5. Example

1
The following statement declares a parameterized Option type:

3.5.5.2. Option Example

(variant Option
  (parameter A)
  (case None)
  (case Some (field x A)))
3
The following type declarations are equivalent:

3.5.5.4. Equivalent Example

(variant T
  (parameter A)
  (case C [field x A]))

(variant T
  (case C [field x A])
  (parameter A))

3.6. protocol

3.6.1. Description

1
protocol - Declare a protocol

3.6.2. Overview

1
The protocol statement declares a new protocol.

3.6.3. Syntax

3.6.3.1. Protocol Syntax

protocol_name =
  [A-Z] , { [a-z0-9A-Z] } ;

version_number =
  [0-9] , { [0-9] } ;

types_added_declaration =
  "(" , "types-added" , { type_name } , ")" ;

types_removed_declaration =
  "(" , "types-removed" , { type_name } , ")" ;

types_removed_all_declaration =
  "(" , "types-removed-all" ")" ;

version_modification_declaration =
  types_added_declaration | types_removed_declaration | types_removed_all_declaration;

version_declaration =
  "(" , "version" , version_number , { version_modification_declaration } , ")" ;

protocol_declaration =
  "(" , "protocol" , protocol_name , { version_declaration } , ")" ;

3.6.4. Semantics

1
A protocol statement, if present, MUST occur with a package set in the current schema context. In practical terms, this means that protocol statements MUST appear after the package statement in a given compilation unit.
2
The statement (protocol T ...) introduces a new protocol name T within the current package in the schema context. Protocol names are unique within a package; it is an error for two or more protocol declarations to name the same protocol.
3
A protocol statement declares a contiguous ordered set of versions, with each version naming a set of types that are included within that version by nature of being added to or removed from the previous version. Accordingly, the intersections of the sets of types between versions are allowed to be non-empty. That is, for versions v and w, if P(v) is the set of types in version v and P(w) is the set of types in version w, then it is not an error if P(v) ∩ P(w) ≠ ∅.
4
A (types-added ...) declaration adds a set of types to a protocol version relative to the previous version.
5
A (types-removed ...) declaration removes a set of types from a protocol version relative to the previous version.
6
A (types-removed-all) declaration is a convenient declaration that removes all types from a protocol version. It is equivalent to a (types-removed ...) declaration where the declaration names all the types that are present in the previous version.
7
Each type named in each protocol version must have kind *.
8
For each protocol version vc, additions and removals are processed as follows: Let tp be the set of types present in the version vp that is the version immediately previous to vc. If vc is the first version in the protocol, tp = ∅. All the types in all of the (types-added ...) declarations in vc are collected into the addition set ta. All the types in all of the (types-removed ...) declarations in vc are collected into the removal set tr. If a (types-removed-all) declaration is present, then tr = tp. Then, for each type r in tr, r is removed from tp. Then, for each type a in ta, a is added to tp. tp is now considered to be the set of types present in vc.
9
It is an error if the set of types in a version is empty after all additions and removals have been processed.
10
It is an error if a type named by a (types-removed ...) declaration is not present in the protocol version prior to additions and removals being processed. That is, it is not valid to attempt to remove a type from a protocol version when that type is not present in the protocol version in the first place.
11
It is an error if a type named by a (types-added ...) declaration is already present in the protocol version prior to additions and removals being processed. That is, it is not valid to attempt to redundantly add a type to a protocol version when that type is already present in the protocol version.
12
The declaration order of type additions and removals within a version is NOT significant; changing the order of version declarations will not change the semantics or serialized form of the protocol as the declarations MUST be reordered by the compiler into ascending lexicographical order of the type names.
13
The first version in a protocol cannot have any (types-removed ...) declarations.
14
The declaration order of versions within a protocol is NOT significant; changing the order of version declarations will not change the semantics or serialized form of the protocol as the declarations MUST be reordered by the compiler into ascending order by their declared version number.

3.6.5. Example

1
The following statements declare a simple Echo protocol with two versions:

3.6.5.2. Protocol Example

(import com.io7m.cedarbridge cb)

(record Hello
  [field name cb:String])

(record Hello2
  [field name cb:String]
  [field id   cb:IntegerUnsigned32])

(record Speak
  [field message cb:String])

(record Goodbye)

(protocol Echo
  [version 1
    [types-added Hello Speak Goodbye]]
  [version 2
    [types-removed Hello]
    [types-added Hello2]])
3
The first version consists of types { Hello, Speak, Goodbye } whilst the second version consists of types { Hello2, Speak, Goodbye }.

3.7. documentation

3.7.1. Description

1
documentation - Add documentation to an element

3.7.2. Overview

1
The documentation statement specifies a paragraph of documentation for an element.

3.7.3. Syntax

3.7.3.1. Documentation Syntax

documentation_declaration =
  "(" , "documentation" , symbol , quoted_string , ")" ;

3.7.4. Semantics

1
A documentation statement (documentation T s) adds the documentation string s to the object T.
2
The documentation statement may appear:

3.7.4.3. Documentation Locations

  • Inside packages, where the target objects may be types or protocols.
  • Inside record definitions, where the target objects may be fields within the record, or type parameters on the record.
  • Inside variant definitions, where the target objects may be the cases of the variant, or type parameters on the variant.
  • Inside variant cases, where the target objects may be fields within the variant case.
4
Documentation statements may refer to objects that are yet to be defined. For example, it is possible to specify documentation for a record field before that record field is defined. However, it is an error to refer to objects that are never defined. Implementations are encouraged to perform binding analyses of documentation statements in a separate pass after the definitions of other objects are checked.

3.7.5. Example

1
The following statement adds documentation to a Color record type:

3.7.5.2. Package Example

(package com.io7m.cedarbridge)

(documentation Color "The type of linear RGB color vectors.")
(record Color
  (documentation red "The red channel.")
  (field red Float64)
  (documentation green "The red channel.")
  (field green Float64)
  (documentation blue "The red channel.")
  (field blue Float64))

4. Type Expressions

4.1. Overview

1
A type expression yields a type when evaluated.

4.2. Syntax

4.2.1. Type Expression Syntax

type_path =
  [ package_name_segment , ":" ] , type_name ;

type_application =
  type_path , { type_expression } ;

type_expression =
    type_path
  | type_parameter_name
  | type_application
  ;

4.3. Semantics

1
A type expression is an expression that, when evaluated, yields a type. The evaluation of type expressions, ultimately, terminates in the evaluation of a type constructor that can take zero or more type parameters. record and variant statements declare new type constructors. Evaluation of type expressions implicitly occurs as part of type-checking during compilation.
2
Types are categorized by kind; a type constructor that takes no parameters has kind *. A type constructor that takes one parameter has kind * → *. Applying a type constructor to arguments conceptually reduces the kind: A type constructor with kind * → * -> * -> * applied to three arguments has kind *.
3
The partial application of type constructors is not supported: It is an error if the number of arguments supplied to a type constructor does not match the number of declared parameters for the type constructor.

4.4. Type Rules

1
The initial, empty type environment is well-formed, and adding a type to the environment that does not already exist results in a well-formed type environment.

4.4.2. Initial

─────
Γ ⊢ ◇

Empty


Γ ⊢ ◇
x ∉ dom(Γ)
──────────
Γ, x ⊢ ◇

Extension
3
A record T declared with n type parameters and any number of fields has kind *₀ → ... → *ₙ and introduces T into the environment:

4.4.4. Record Type Rules

Γ ⊢ p = { t₀ : *, t₁ : *, ... tₙ : * }
Γ ⊢ f = { ... }
T ∉ dom(Γ)
──────────────────────────────────────────
Γ, T ⊢ [record T p f] : *₀ → *₁ → ... → *ₙ

TypeDeclareRecord
5
A variant T declared with n type parameters any number of cases has kind *₀ → ... → *ₙ and introduces T into the environment:

4.4.6. Variant Type Rules

Γ ⊢ p = { t₀ : *, t₁ : *, ... tₙ : * }
Γ ⊢ c = { ... }
T ∉ dom(Γ)
───────────────────────────────────────────
Γ, T ⊢ [variant T p f] : *₀ → *₁ → ... → *ₙ

TypeDeclareVariant
7
The application of a type constructor f that takes n-1 parameters to n-1 type expressions (each of kind *) is well-formed:

4.4.8. Type Application Rules

Γ ⊢ S = { t₀ : *, t₁ : *, ... tₙ : * }
Γ ⊢ f : * → *₀ → *₁ → ... → *ₙ
|S| ≠ 0
──────────────────────────────────
Γ ⊢ [f t₀ t₁ ... tₙ] : *

TypeApplication
9
The list of provided arguments must be non-empty.

4.5. Examples

4.5.1. Type Expressions Example

(record T
  [parameter A]
  [parameter B]
  [field f0 A]
  [field f1 B])

(record U)

T              ; Has kind * → * → *
(T)            ; Error: T has kind * → * → * but no parameters were supplied
(T U)          ; Error: T has kind * → * → * but only one parameter was supplied
(T U U)        ; Has kind *

5. Standard Library

5.1. Overview

1
The Cedarbridge language defines a set of standard packages that all implementations of the language are required to provide.

5.2. Package com.io7m.cedarbridge

5.2.1. Overview

1
The com.io7m.cedarbridge package declares a set of generally useful types.

5.2.2. Boolean

5.2.2.1. Description

Boolean : *
2
The Boolean type holds simple true or false values.

5.2.2.3. Boolean Type

(variant Boolean
  [case False]
  [case True])

5.2.3. IntegerUnsigned8

5.2.3.1. Description

IntegerUnsigned8 : *
2
The IntegerUnsigned8 type is an opaque type that can hold values in the range [0, 255].

5.2.4. IntegerUnsigned16

5.2.4.1. Description

IntegerUnsigned16 : *
2
The IntegerUnsigned16 type is an opaque type that can hold values in the range [0, 65535].

5.2.5. IntegerUnsigned32

5.2.5.1. Description

IntegerUnsigned32 : *
2
The IntegerUnsigned32 type is an opaque type that can hold values in the range [0, 4294967295].

5.2.6. IntegerUnsigned64

5.2.6.1. Description

IntegerUnsigned64 : *
2
The IntegerUnsigned64 type is an opaque type that can hold values in the range [0, 18446744073709551615].

5.2.7. IntegerSigned8

5.2.7.1. Description

IntegerSigned8 : *
2
The IntegerSigned8 type is an opaque type that can hold values in the range [-128, 127].

5.2.8. IntegerSigned16

5.2.8.1. Description

IntegerSigned16 : *
2
The IntegerSigned16 type is an opaque type that can hold values in the range [-32768, 32767].

5.2.9. IntegerSigned32

5.2.9.1. Description

IntegerSigned32 : *
2
The IntegerSigned32 type is an opaque type that can hold values in the range [-2147483648, 2147483647].

5.2.10. IntegerSigned64

5.2.10.1. Description

IntegerSigned64 : *
2
The IntegerSigned64 type is an opaque type that can hold values in the range [-9223372036854775808, 9223372036854775807].

5.2.11. String

5.2.11.1. Description

String : *
2
The String type is an opaque type that can hold a sequence of at most 4294967295 octets of UTF-8 encoded data.

5.2.12. ByteArray

5.2.12.1. Description

ByteArray : *
2
The ByteArray type is an opaque type that can hold a sequence of at most 4294967295 octets of data.

5.2.13. Float16

5.2.13.1. Description

Float16 : *
2
The Float16 type is an opaque type that can hold a single IEEE-754 Binary16 [1] value.

5.2.14. Float32

5.2.14.1. Description

Float32 : *
2
The Float32 type is an opaque type that can hold a single IEEE-754 Binary32 [1] value.

5.2.15. Float64

5.2.15.1. Description

Float64 : *
2
The Float64 type is an opaque type that can hold a single IEEE-754 Binary64 [1] value.

5.2.16. List

5.2.16.1. Description

List : * → *
2
The List type is an opaque type that can hold a sequence of values of a type equal to the single type parameter.

5.2.17. Option

5.2.17.1. Description

Option : * → *
2
The Option type is a type that can hold zero or one values of a type equal to the single type parameter. The type is equivalent to the following variant declaration:

5.2.17.3. Option Type

(variant Option
  [parameter A]
  [case None]
  [case Some (field value A)])

5.2.18. MapEntry

5.2.18.1. Description

MapEntry : * → * → *
2
The MapEntry type is a type used to hold a single entry in a Map. The type is equivalent to the following record declaration:

5.2.18.3. MapEntry Type

(record MapEntry
  [parameter K]
  [parameter V]
  [field key K]
  [field value V])

5.2.19. Map

5.2.19.1. Description

Map : * → * → *
2
The Map type is a type used to hold a sequence of entries. The type is equivalent to the following record declaration:

5.2.19.3. Map Type

(record Map
  [parameter K]
  [parameter V]
  [field entries (List [MapEntry K V])])

5.2.20. UUID

5.2.20.1. Description

UUID : *
2
The UUID type represents an RFC 4122 universally unique identifier value. The type is equivalent to the following record declaration:

5.2.20.3. UUID Type

(record UUID
  [field msb cb:IntegerUnsigned64]
  [field lsb cb:IntegerUnsigned64]
)
4
The 64 most significant bits are held in the msb field, and the 64 least significant bits are held in the lsb field.

5.2.21. URI

5.2.21.1. Description

URI : *
2
The URI type represents an RFC 3986 URI value. The type is equivalent to the following record declaration:

5.2.21.3. UUID Type

(record URI
  [field value cb:String]
)
4
The value field holds the UTF-8 encoded string representation of the URI.

Footnotes

1
IEEE Standard for Floating-Point Arithmetic (IEEE 754), or equivalently ISO/IEC 60559:2020.
References to this footnote: 123

5.3. Package com.io7m.cedarbridge.time

5.3.1. Overview

1
The com.io7m.cedarbridge.time package declares a set of types related to times and dates.

5.3.2. Duration

5.3.2.1. Description

Duration : *
2
The Duration type holds a quantity of time in terms of seconds and nanoseconds.

5.3.2.3. Duration Type

(import com.io7m.cedarbridge cb)

(record Duration
  [field seconds cb:IntegerUnsigned64]
  [field nanos   cb:IntegerUnsigned32]
)
4
The seconds field holds the number of seconds in the duration.
5
The nanoseconds field holds the number of nanoseconds in the duration. This value is added to the seconds field to produce the full duration. The value of the nanoseconds field may only be in the range [0, 999999999].

5.3.3. LocalDate

5.3.3.1. Description

LocalDate : *
2
The LocalDate type represents a date in an unspecified time zone.

5.3.3.3. LocalDate Type

(import com.io7m.cedarbridge cb)

(record LocalDate
  [field year  cb:IntegerUnsigned32]
  [field month cb:IntegerUnsigned8]
  [field day   cb:IntegerUnsigned8]
)
4
The year field holds the year.
5
The month field holds the month of the year in the range [1, 12].
6
The day field holds the day of the month in the range [1, 31].
7
Not all combinations of month field and day field values are guaranteed to produce valid dates. Implementations are expected to validate dates after deserialization.

5.3.4. LocalTime

5.3.4.1. Description

LocalTime : *
2
The LocalTime type represents a time in an unspecified time zone.

5.3.4.3. LocalDate Type

(import com.io7m.cedarbridge cb)

(record LocalTime
  [field hour   cb:Unsigned8]
  [field minute cb:Unsigned8]
  [field second cb:Unsigned8]
  [field nanos  cb:Unsigned32]
)
4
The hour field holds the hour in the range [0, 23].
5
The minute field holds the minute in the range [0, 59].
6
The second field holds the second in the range [0, 59].
7
The nanos field holds the nanosecond in the range [0, 999999999].

5.3.5. LocalDateTime

5.3.5.1. Description

LocalDateTime : *
2
The LocalDateTime type represents a date and time in an unspecified time zone.

5.3.5.3. LocalDate Type

(record LocalDateTime
  [field date LocalDate]
  [field time LocalTime]
)

5.3.6. ZoneOffset

5.3.6.1. Description

ZoneOffset : *
2
The ZoneOffset type represents a timezone offset.

5.3.6.3. LocalDate Type

(record ZoneOffset
  [field seconds cb:IntegerSigned32]
)
4
The seconds field holds the offset in the range [-64800, 64800].

5.3.7. OffsetDateTime

5.3.7.1. Description

OffsetDateTime : *
2
The OffsetDateTime type represents a date and time in a specific time zone.

5.3.7.3. LocalDate Type

(record OffsetDateTime
  [field localDateTime LocalDateTime]
  [field zoneOffset    ZoneOffset]
)

6. CCBE

6.1. Overview

1
The Cedarbridge language is defined without reference to any particular set of rules for actually encoding values of the various user-defined types for transmission. This specification section defines a canonical format for binary encoding, CCBE, that all implementations are expected to be able to understand.
2
The CCBE is defined as following:

6.1.3. CCBE

  1. A simple base type system with descriptions of how values of those types are serialized to a binary format.
  2. The rules for translating values in the Cedarbridge language to the base type system.

6.2. Bytes

1
A byte is an eight-bit quantity with the individual bits written to the transmission medium in decreasing order of significance. That is, the most signficant bit is written to the output first, and the least signficant bit is written last. When the individual bits of an N-bit value are enumerated, it is to be understood that the most signficant bit is numbered 0 and the least signficant bit is numbered N-1. A byte can therefore be described as the following product type:

6.2.2. Byte Type

Byte : (bit0 : 𝔹, bit1 : 𝔹, bit2 : 𝔹, bit3 : 𝔹, bit4 : 𝔹, bit5 : 𝔹, bit6 : 𝔹, bit7 : 𝔹)
3
For the purposes of specification, we assume the existence of a function bit(n, x) : ℕ → α → 𝔹 that, given an arbitrary input value x of type α, returns the value of bit n of the input value according to the above ordering and bit numbering rules. This is merely a notational aid and should be understood to be something that implementations are actually required to implement.

6.3. Byte Sequences

1
A byte sequence is, unsuprisingly, a sequence of bytes. The notation [] denotes a sequence of length 0, and the operator ⊕ prepends a byte to a byte sequence. The operator ⊕ is right-associative, so ∀x y z. x ⊕ y ⊕ z = x ⊕ (y ⊕ z).

6.3.2. Byte Type

ByteSequence : *

([]) : ByteSequence
(⊕)  : Byte → ByteSequence → ByteSequence

6.4. Base Types

6.4.1. CCBE

1
The kind CCBE denotes the disjoint set of types present in the encoding rules. The definition is as follows:

6.4.1.2. CCBE

CCBE = { S8, S16, S32, S64, U8, U16, U32, U64, F16, F32, F64, ByteArray }
3
For each of the types in CCBE, we describe a function encode(x) : (τ : CCBE) → (α : τ) → ByteSequence (where τ is an implicit parameter that can be inferred from α). The purpose of the encode function is to describe how to transform a value of a given type to a byte sequence that can be written to the destination transmission medium.

6.4.2. S8

6.4.2.1. Description

S8 : { e ∈ ℤ | e ≥ -128 ⋀ e ≤ 127 }
2
The S8 type is an opaque type that can hold a value in the range [-128, 127].
3
Values of type S8 are encoded as follows:

6.4.2.4. S8 Bytes

encode(S8, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
  in
    byte0 ⊕ []

6.4.3. S16

6.4.3.1. Description

S16 : { e ∈ ℤ | e ≥ -32768 ⋀ e ≤ 32767 }
2
The S16 type is an opaque type that can hold a value in the range [-32768, 32767].
3
Values of type S16 are encoded as follows:

6.4.3.4. S16 Bytes

encode(S16, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
  in
    byte0 ⊕ byte1 ⊕ []

6.4.4. S32

6.4.4.1. Description

S32 : { e ∈ ℤ | e ≥ -2147483648 ⋀ e ≤ 2147483647 }
2
The S32 type is an opaque type that can hold a value in the range [-2147483648, 2147483647].
3
Values of type S32 are encoded as follows:

6.4.4.4. S32 Bytes

encode(S32, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
    byte2 = (bit(16, x), bit(17, x), bit(18, x), bit(19, x), bit(20, x), bit(21, x), bit(22, x), bit(23, x))
    byte3 = (bit(24, x), bit(25, x), bit(26, x), bit(27, x), bit(28, x), bit(29, x), bit(30, x), bit(31, x))
  in
    byte0 ⊕ byte1 ⊕ byte2 ⊕ byte3 ⊕ []

6.4.5. S64

6.4.5.1. Description

S64 : { e ∈ ℤ | e ≥ -9223372036854775808 ⋀ e ≤ 9223372036854775807 }
2
The S64 type is an opaque type that can hold a value in the range [-9223372036854775808, 9223372036854775807].
3
Values of type S64 are encoded as follows:

6.4.5.4. S64 Bytes

encode(S64, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
    byte2 = (bit(16, x), bit(17, x), bit(18, x), bit(19, x), bit(20, x), bit(21, x), bit(22, x), bit(23, x))
    byte3 = (bit(24, x), bit(25, x), bit(26, x), bit(27, x), bit(28, x), bit(29, x), bit(30, x), bit(31, x))
    byte4 = (bit(32, x), bit(33, x), bit(34, x), bit(35, x), bit(36, x), bit(37, x), bit(38, x), bit(39, x))
    byte5 = (bit(40, x), bit(41, x), bit(42, x), bit(43, x), bit(44, x), bit(45, x), bit(46, x), bit(47, x))
    byte6 = (bit(48, x), bit(49, x), bit(50, x), bit(51, x), bit(52, x), bit(53, x), bit(54, x), bit(55, x))
    byte7 = (bit(56, x), bit(57, x), bit(58, x), bit(59, x), bit(60, x), bit(61, x), bit(62, x), bit(63, x))
  in
    byte0 ⊕ byte1 ⊕ byte2 ⊕ byte3 ⊕ byte4 ⊕ byte5 ⊕ byte6 ⊕ byte7 ⊕ []

6.4.6. U8

6.4.6.1. Description

U8 : { e ∈ ℤ | e ≥ 0 ⋀ e ≤ 255 }
2
The U8 type is an opaque type that can hold a value in the range [0, 255].
3
Values of type U8 are encoded as follows:

6.4.6.4. U8 Bytes

encode(U8, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
  in
    byte0 ⊕ []

6.4.7. U16

6.4.7.1. Description

U16 : { e ∈ ℤ | e ≥ 0 ⋀ e ≤ 65535 }
2
The U16 type is an opaque type that can hold a value in the range [0, 65535].
3
Values of type U16 are encoded as follows:

6.4.7.4. U16 Bytes

encode(U16, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
  in
    byte0 ⊕ byte1 ⊕ []

6.4.8. U32

6.4.8.1. Description

U32 : { e ∈ ℤ | e ≥ 0 ⋀ e ≤ 4294967295 }
2
The U32 type is an opaque type that can hold a value in the range [0, 4294967295].
3
Values of type U32 are encoded as follows:

6.4.8.4. U32 Bytes

encode(U32, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
    byte2 = (bit(16, x), bit(17, x), bit(18, x), bit(19, x), bit(20, x), bit(21, x), bit(22, x), bit(23, x))
    byte3 = (bit(24, x), bit(25, x), bit(26, x), bit(27, x), bit(28, x), bit(29, x), bit(30, x), bit(31, x))
  in
    byte0 ⊕ byte1 ⊕ byte2 ⊕ byte3 ⊕ []

6.4.9. U64

6.4.9.1. Description

U64 : { e ∈ ℤ | e ≥ 0 ⋀ e ≤ 18446744073709551615 }
2
The U64 type is an opaque type that can hold a value in the range [0, 18446744073709551615].
3
Values of type U64 are encoded as follows:

6.4.9.4. U64 Bytes

encode(U64, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
    byte2 = (bit(16, x), bit(17, x), bit(18, x), bit(19, x), bit(20, x), bit(21, x), bit(22, x), bit(23, x))
    byte3 = (bit(24, x), bit(25, x), bit(26, x), bit(27, x), bit(28, x), bit(29, x), bit(30, x), bit(31, x))
    byte4 = (bit(32, x), bit(33, x), bit(34, x), bit(35, x), bit(36, x), bit(37, x), bit(38, x), bit(39, x))
    byte5 = (bit(40, x), bit(41, x), bit(42, x), bit(43, x), bit(44, x), bit(45, x), bit(46, x), bit(47, x))
    byte6 = (bit(48, x), bit(49, x), bit(50, x), bit(51, x), bit(52, x), bit(53, x), bit(54, x), bit(55, x))
    byte7 = (bit(56, x), bit(57, x), bit(58, x), bit(59, x), bit(60, x), bit(61, x), bit(62, x), bit(63, x))
  in
    byte0 ⊕ byte1 ⊕ byte2 ⊕ byte3 ⊕ byte4 ⊕ byte5 ⊕ byte6 ⊕ byte7 ⊕ []

6.4.10. F16

6.4.10.1. Description

F16 : ℝ
2
The F16 type is an opaque type that can hold a value in the value set of the IEEE 754 binary16 [1] type.
3
Values of type F16 are encoded as follows:

6.4.10.4. F16 Bytes

encode(F16, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
  in
    byte0 ⊕ byte1 ⊕ []

6.4.11. F32

6.4.11.1. Description

F32 : ℝ
2
The F32 type is an opaque type that can hold a value in the value set of the IEEE 754 binary32 [1] type.
3
Values of type F32 are encoded as follows:

6.4.11.4. F32 Bytes

encode(F32, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
    byte2 = (bit(16, x), bit(17, x), bit(18, x), bit(19, x), bit(20, x), bit(21, x), bit(22, x), bit(23, x))
    byte3 = (bit(24, x), bit(25, x), bit(26, x), bit(27, x), bit(28, x), bit(29, x), bit(30, x), bit(31, x))
  in
    byte0 ⊕ byte1 ⊕ byte2 ⊕ byte3 ⊕ []

6.4.12. F64

6.4.12.1. Description

F64 : ℝ
2
The F64 type is an opaque type that can hold a value in the value set of the IEEE 754 binary64 [1] type.
3
Values of type F64 are encoded as follows:

6.4.12.4. F64 Bytes

encode(F64, x) =
  let
    byte0 = (bit(0, x),  bit(1, x),  bit(2, x),  bit(3, x),  bit(4, x),  bit(5, x),  bit(6, x),  bit(7, x))
    byte1 = (bit(8, x),  bit(9, x),  bit(10, x), bit(11, x), bit(12, x), bit(13, x), bit(14, x), bit(15, x))
    byte2 = (bit(16, x), bit(17, x), bit(18, x), bit(19, x), bit(20, x), bit(21, x), bit(22, x), bit(23, x))
    byte3 = (bit(24, x), bit(25, x), bit(26, x), bit(27, x), bit(28, x), bit(29, x), bit(30, x), bit(31, x))
    byte4 = (bit(32, x), bit(33, x), bit(34, x), bit(35, x), bit(36, x), bit(37, x), bit(38, x), bit(39, x))
    byte5 = (bit(40, x), bit(41, x), bit(42, x), bit(43, x), bit(44, x), bit(45, x), bit(46, x), bit(47, x))
    byte6 = (bit(48, x), bit(49, x), bit(50, x), bit(51, x), bit(52, x), bit(53, x), bit(54, x), bit(55, x))
    byte7 = (bit(56, x), bit(57, x), bit(58, x), bit(59, x), bit(60, x), bit(61, x), bit(62, x), bit(63, x))
  in
    byte0 ⊕ byte1 ⊕ byte2 ⊕ byte3 ⊕ byte4 ⊕ byte5 ⊕ byte6 ⊕ byte7 ⊕ []

6.4.13. ByteArray

1
The ByteArray type is an opaque sequence of bytes. A value b of type ByteArray has a fixed length n denoted length(b) : ℕ = n. The property ∀x. 0 ≤ length(x) ≤ 4294967295 always holds. The byte at position m (where 0 ≤ m < n) is denoted byte(m, b) : Byte.
2
Values of type ByteArray are encoded as follows: For a value x, a byte sequence k ⊕ p ⊕ [] is constructed, where k is the result of encoding length(x) as if it were a value of type U32, and p is simply byte(m, x) for all m | 0 ≤ m < length(x).

6.4.14. List

1
The List type is parameterized type describing a sequence of values. A value x of type List α has a fixed length n denoted length(x) : ℕ = n. The property ∀x. 0 ≤ length(x) ≤ 4294967295 always holds. The value at position m (where 0 ≤ m < n) is denoted value(m, x) : α.
2
Values of type List are encoded as follows: For a value x, a byte sequence k ⊕ p ⊕ [] is constructed, where k is the result of encoding length(x) as if it were a value of type U32, and p is the byte sequence obtained by concatenating the results of encoding value(m, x) for all m | 0 ≤ m < length(x).

6.5. Encoding com.io7m.cedarbridge Types

1
Most of the types declared in the com.io7m.cedarbridge package are designed to map directly to the types in CCBE:

6.5.2. Cedarbridge ↔ CCBE

Cedarbridge CCBE
IntegerSigned8 S8
IntegerSigned16 S16
IntegerSigned32 S32
IntegerSigned64 S64
IntegerUnsigned8 U8
IntegerUnsigned16 U16
IntegerUnsigned32 U32
IntegerUnsigned64 U64
ByteArray ByteArray
List List
Float16 F16
Float32 F32
Float64 F64
3
The Cedarbridge String type is encoded as if it were a ByteArray after having first converted the sequence of characters to a sequence of UTF-8 encoded bytes.

6.6. Encoding Record Types

1
A value of a record type r is encoded by concatenating the byte sequences produced by encoding the fields of r in the order that the fields were declared in the type of r.
2
A field f is encoded by encoding the value of f as is appropriate for a record type, variant type, or one of the base types.

6.7. Encoding Variant Types

1
A value of a variant type r is encoded by first determining the variant index v of r. The variant index is the number of the case that was used to construct r, assuming that cases are numbered in declaration order starting at 0. For the case c that was used to construct r, the byte sequence produced for r is k ⊕ p ⊕ [], where k is the result of encoding v as if it were a value of type U32, and p is the concatenation of the byte sequences produced by encoding the fields of r in the order that the fields were declared in the declaration of c.

6.8. Encoding Protocols

1
Conceptually, each type present in a protocol version is added to one effectively anonymous variant type per version. The cases of the variant are ordered lexicographically by the names of the types. This anonymous variant type is then encoded exactly as regular variant types are normally encoded.
2
For example, assuming the following definitions:

6.8.3. Vector3f

[import com.io7m.cedarbridge cb]

[record A [field x cb:IntegerUnsigned8]]

[record B [field x cb:IntegerUnsigned8]]

[variant C
  [case C0 [field x cb:IntegerUnsigned8]]
  [case C1 [field x cb:IntegerUnsigned8]]
]

[protocol P
  [version 1 [types-added A B]]
  [version 2 [types-added C]]
  [version 3 [types-removed A]]
]
4
When a message M is encoded in versioned form, we use the notation V(M) to refer to the versioned nature of the message.
5
In protocol version 1, the expression V(A 23) : A is encoded as the byte sequence 0x00 0x00 0x00 0x00 0x17. That is, the first four bytes specify the type at case 0 of the anonymous variant implicitly defined by the [version 1 ...] declaration, followed by the encoded form of (A 23) : A.
6
In protocol version 2, the expression V(C1 23) : C is encoded as the byte sequence 0x00 0x00 0x00 0x02 0x00 0x00 0x00 0x01 0x17. That is, the first four bytes specify the type at case 2 of the anonymous variant implicitly defined by the [version 2 ...] declaration, followed by the encoded form of (C1 23) : C.
7
In protocol version 3, the expression P (B 23) : B is encoded as the byte sequence 0x00 0x00 0x00 0x00 0x17. That is, the first four bytes specify the type at case 0 of the anonymous variant implicitly defined by the [version 3 ...] declaration. Because the type A was removed in version 3, B is now the type at case 0, whereas it was previously the type at case 1 in versions 1 and 2.

6.9. Encoding Examples

1
The expression (Some 23) : [Option IntegerUnsigned32] is encoded as the byte sequence 0x00 0x00 0x00 0x01 0x00 0x00 0x00 0x17. This encoding comes from the fact that Option is a variant type, Some is case number 1, and the value of the one and only field of Some is 23 (0x17).
2
The expression None : [Option IntegerUnsigned32] is encoded as the byte sequence 0x00 0x00 0x00 0x00. This encoding comes from the fact that Option is a variant type, None is case number 0, and there are no fields in the case.
3
Assuming the following type:

6.9.4. Vector3f

[import com.io7m.cedarbridge cb]

[record Vector3f
  [field x cb:Float32]
  [field y cb:Float32]
  [field z cb:Float32]]
5
The expression [Vector3f 17.0 199.0 1.00781238] is encoded as the byte sequence 0x41 0x88 0x00 0x00 0x43 0x47 0x00 0x00 0x3f 0x80 0xff 0xff. This is simply three IEEE 754 binary32 values.
6
The string "hello" is encoded as the byte sequence 0x00 0x00 0x00 0x05 0x68 0x65 0x6c 0x6c 0x6f. This is the number of UTF-8 encoded bytes (5) followed by the UTF-8 encoded bytes of the string.
7
The expression [List 17038 27297 17288] : List IntegerSigned16 is encoded as the byte sequence 0x00 0x00 0x00 0x03 0x42 0x8e 0x6a 0xa1 0x43 0x88. This is the length of the list (3) followed by the encoded forms of 17038 (0x428e), 27297 (0x6aa1), and 17288 (0x4388), respectively.

Footnotes

1
IEEE Standard for Floating-Point Arithmetic (IEEE 754), or equivalently ISO/IEC 60559:2020.
References to this footnote: 123

7. Container Protocol

7.1. Overview

1
This specification section defines a simple protocol for performing version negotiation for application protocols.

7.2. Dialogue

1
The protocol assumes a configuration analogous to a client and server. That is, one party (the client) initiates a connection to the other party (the server). The two parties can then communicate over the created two-way connection. A server and client communicating over the open internet using TCP would satisfy this configuration. Alternatively, two microcontrollers communicating over UART could also be made to satisfy this configuration. For the purposes of keeping the specification straightforward, the initiator of the connection will be referred to as the client, and the other party will be referred to as the server.
2
The dialogue between a client c and server s is as follows:

7.2.3. Dialogue

  1. c opens a connection p to s.
  2. s sends an Available message to c over p.
  3. c inspects the Available message and picks an appropriate protocol version. If no protocol version is acceptable, c terminates p. If there is a protocol version that c is prepared to accept, c sends a Use message to s over p.
  4. s inspects the Use message and checks that the requested version appears in the list that was presented in the original Available message. If the Use message is unacceptable, s sends a Response message indicating the error over p and terminates p. If the Use message is acceptable, s sends a Response message indicating success over p and, from this point onwards, c and s communicate exclusively using the negotiated protocol.

7.3. Binary Format

1
The messages described here are expected to be encoded to binary using CCBE. However, certain exceptions have been made in order to keep each message type at a fixed size. Protocols such as this container protocol constitute a bootstrapping problem in that, if all of the messages were defined in Cedarbridge, the two communicating parties would have to speak Cedarbridge in order to ask each other if they can both speak Cedarbridge. We instead use the Cedarbridge language to document the basic structure of the messages, but assume that the protocol messages will be manually read, written, and parsed without necessarily using Cedarbridge compiler generated code. For this reason, the protocol does not use Cedarbridge's versioning facilities.

7.4. Message: Available

7.4.1. Available

[import com.io7m.cedarbridge c]

[record ApplicationProtocolID
  [field msb c:IntegerUnsigned64]
  [field lsb c:IntegerUnsigned64]]

[record Available
  [field code                     c:IntegerUnsigned32]
  [field containerProtocolMinimum c:IntegerUnsigned32]
  [field containerProtocolMaximum c:IntegerUnsigned32]
  [field reserved0                c:IntegerUnsigned32]

  [field reserved1                c:IntegerUnsigned32]
  [field reserved2                c:IntegerUnsigned32]
  [field reserved3                c:IntegerUnsigned32]
  [field reserved4                c:IntegerUnsigned32]

  [field appProtocolId            c:ApplicationProtocolID]
  [field appProtocolMinimum       c:IntegerUnsigned64]
  [field appProtocolMaximum       c:IntegerUnsigned64]]
2
The value of the code field MUST be exactly 0x43420000.
3
The values of the containerProtocolMinimum and containerProtocolMaximum fields define a half-open range describing the range of supported container protocol versions. Currently, the only supported values of containerProtocolMinimum and containerProtocolMaximum are 1 and 1, respectively. The value of the containerProtocolMinimum field MUST be ≤ containerProtocolMaximum.
4
The values of the reserved0, reserved1, reserved2, reserved3, and reserved4 fields MUST be 0.
5
The appProtocolId specifies the bits of a UUID value that uniquely identifies the application protocol. The Cedarbridge compiler automatically generates these values for protocol declarations.
6
The values of the appProtocolMinimum and appProtocolMaximum fields define a half-open range describing the range of supported container protocol versions. The value of the appProtocolMinimum field MUST be ≤ appProtocolMaximum.
7
The size of the Available message, when encoded as a byte sequence, MUST be exactly 64 bytes.

7.5. Message: Use

7.5.1. Use

[import com.io7m.cedarbridge c]

[record Use
  [field code              c:IntegerUnsigned32]
  [field containerProtocol c:IntegerUnsigned32]
  [field appProtocolId     c:ApplicationProtocolID]
  [field appProtocol       c:IntegerUnsigned64]]
2
The value of the code field MUST be exactly 0x43420001.
3
The value of the containerProtocol specifies the container protocol to be used. Currently, the only supported value of containerProtocol is 1.
4
The appProtocolId specifies the bits of a UUID value that uniquely identifies the application protocol. The Cedarbridge compiler automatically generates these values for protocol declarations.
5
The value of the appProtocol field specifies the version of the application protocol that will be used. The value of this field MUST be appProtocolMinimum ≤ appProtocol ≤ appProtocolMaximum.
6
The size of the Available message, when encoded as a byte sequence, MUST be exactly 32 bytes.

7.6. Message: Response

7.6.1. Response

[import com.io7m.cedarbridge c]

[record Response
  [field code    c:IntegerUnsigned32]
  [field ok      c:IntegerUnsigned32]
  [field message c:String]]
2
The value of the code field MUST be exactly 0x43420002.
3
The value of the ok field MUST be exactly 0 if the client tried to use an unsupported protocol. The value of the ok field MUST be exactly 1 if the client tried to use a supported protocol.
4
The value of the message field provides a humanly-readable message explaining why version negotiation failed.
5
The size of the Response message, when encoded as a byte sequence, MUST be exactly 256 bytes. Padding bytes with values equal to 0x00 must be appended to the end of the structure if the message field is shorter than 244 bytes.
io7m | single-page | multi-page | epub | Cedarbridge Language Specification 2.0.0