Aurantium 1.0

Book Metadata

CREATOR | Mark Raynsford
DATE | 2023-03-26T12:49:04+00:00
DESCRIPTION | Specification for the Aurantium sample map file format.
IDENTIFIER | 440f809f-fa95-4b24-a8cd-f6a7318a5b88
LANGUAGE | en
RIGHTS | Public Domain
TITLE | Aurantium 1.0

Table Of Contents

Cover

Colophon

Table Of Contents

1. Overview

2. Notational Conventions

2.1. Rocq

2.2. Unicode

2.3. Sets

3. The Aurantium Model

3.1. Overview

3.2. Divisibility By 8

3.3. Bits & Octets

3.4. List Intersection

3.5. Interpolation

3.6. Hash

3.7. Descriptors

3.8. Compatibility

3.8.1. Overview

3.8.2. File Format Versioning vs. Data Versioning

3.8.2.1. Overview

3.8.2.2. File Format

3.8.2.3. Data Versioning

3.8.3. Identifiers

3.8.4. Changes

3.9. Clips

3.9.1. Overview

3.9.2. Metadata

3.9.3. Sampling & Channels

3.9.4. Endianness

3.9.5. Formats

3.9.5.1. Uncompressed

3.9.5.1.1. Pulse Code Modulation

3.9.5.1.1.1. Description

3.9.5.1.1.2. Linear PCM

3.9.5.1.1.3. Signedness

3.9.5.2. Compressed

3.9.5.2.1. FLAC

3.9.5.3. Types

3.9.6. Loop Ranges

3.9.7. Clips

3.9.8. Clip Lists

3.9.9. Compatibility

3.9.9.1. Overview

3.9.9.2. Removing A Clip

3.9.9.3. Adding A Clip

3.9.9.4. Changing A Clip

3.10. Key Assignments

3.10.1. Overview

3.10.2. Keys

3.10.2.1. Numbering

3.10.2.2. Velocity

3.10.3. Key Assignments

3.10.3.1. Description

3.10.3.2. Key Assignment Evaluation

3.10.3.2.1. Evaluation

3.10.3.2.2. Matching

3.10.3.2.3. Amplitude

3.10.3.2.3.1. Key

3.10.3.2.3.2. Velocity

3.10.3.2.4. Playback Rate

3.10.3.2.5. Complete Procedure

3.10.3.3. Examples

3.10.3.4. Lists

3.10.4. Compatibility

3.10.4.1. Overview

3.10.4.2. Removing A Key Assignment

3.10.4.3. Adding A Key Assignment

3.10.4.4. Changing A Key Assignment

3.11. Audio Map

3.11.1. Overview

3.11.2. Key/Clip References

3.11.3. Audio Map

3.12. Metadata

4. The Aurantium Binary Encoding

4.1. Binary Expressions

4.1.1. Overview

4.1.2. Expressions

4.2. JSON Expressions

4.2.1. Overview

4.2.2. Expressions

4.2.3. Tokens

4.2.4. Token (Strings)

4.2.5. Serialization

4.2.6. Expression -> String

4.2.7. Clips

4.2.8. Key Assignments

4.2.9. Metadata

4.2.10. Schema

4.3. File Header

4.4. Sections

4.5. Identifier

4.5.1. Description

4.5.2. Cardinality

4.6. Clip Descriptions

4.6.1. Description

4.6.2. Cardinality

4.7. Clip Data

4.7.1. Description

4.7.2. Cardinality

4.8. Key assignments

4.8.1. Description

4.8.2. Cardinality

4.9. Metadata

4.9.1. Description

4.9.2. Cardinality

4.10. End

4.10.1. Description

4.10.2. Cardinality

5. Sources

1. Overview

This specification defines version 1.0 of the aurantium file format. The aurantium format is a carefully designed file format intended for the storage and delivery of audio data for realtime audio applications.

This specification is divided into an abstract model and a separate binary encoding. The purpose of the model is to describe the semantics of aurantium files; the actual meaning of the data within, and to describe properties and invariants that must be true for all valid aurantium files. The purpose of the binary encoding is to describe how the model is transformed to a sequence of bytes/octets; it describes the low-level on-disk format of aurantium files. This layered approach is intended to allow for specifying the format with a level of precision that will allow data in the aurantium format to remain readable for decades into the future, and in a manner that ensures that the format is not dependent on any present-day audio APIs.

Developers wishing to write their own code to read and write aurantium files might find it easiest to view the binary encoding section first. The aurantium format is designed to be straightforward to parse, requiring only a few minimal primitives to express the entirety of the format, and requires no references to external specifications (unlike many other audio file formats) [1]. Once a developer is able to read data from an existing aurantium file, they should consult the model to understand what the data they're receiving actually means. The model chapters are arranged in dependency order starting with the most fundamental concepts, and ending with the top level definitions of the various types.

Footnotes

1

It would be more accurate to say that the aurantium specification does not depend on any other specifications that are at the same level of abstraction. For example, the aurantium specification makes references to Unicode, IEEE-754, and so on. It does not, however, require understanding any other existing audio formats, or depend on any definitions given in the specifications for any rendering APIs.

References to this footnote: 1

2. Notational Conventions

2.1. Rocq

2.2. Unicode

2.3. Sets

2.1. Rocq

The formal specification described here is written in the specification language of the Rocq theorem prover. The language is a total, pure-functional, dependently-typed language allowing for describing systems in rigorous detail including machine-checked proofs of various chosen properties.

Readers are not expected to be able to understand the bodies of the proof texts, and doing so is not in any case required. As long as one can understand the meaning of the propositions being expressed, it suffices to trust that the proofs are correct as they are all machine-checked whenever the specification is published.

The full sources of the entire specification are published at the end of this book.

2.2. Unicode

The specification makes reference to the Unicode character set which, at the time of writing, is at version 15.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 λ.

2.3. Sets

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

2.3.2. ZFC

Notation | Description
ℝ | The real numbers

3. The Aurantium Model

3.1. Overview

3.2. Divisibility By 8

3.3. Bits & Octets

3.4. List Intersection

3.5. Interpolation

3.6. Hash

3.7. Descriptors

3.8. Compatibility

3.8.1. Overview

3.8.2. File Format Versioning vs. Data Versioning

3.8.2.1. Overview

3.8.2.2. File Format

3.8.2.3. Data Versioning

3.8.3. Identifiers

3.8.4. Changes

3.9. Clips

3.9.1. Overview

3.9.2. Metadata

3.9.3. Sampling & Channels

3.9.4. Endianness

3.9.5. Formats

3.9.5.1. Uncompressed

3.9.5.2. Compressed

3.9.5.3. Types

3.9.6. Loop Ranges

3.9.7. Clips

3.9.8. Clip Lists

3.9.9. Compatibility

3.9.9.1. Overview

3.9.9.2. Removing A Clip

3.9.9.3. Adding A Clip

3.9.9.4. Changing A Clip

3.10. Key Assignments

3.10.1. Overview

3.10.2. Keys

3.10.2.1. Numbering

3.10.2.2. Velocity

3.10.3. Key Assignments

3.10.3.1. Description

3.10.3.2. Key Assignment Evaluation

3.10.3.3. Examples

3.10.3.4. Lists

3.10.4. Compatibility

3.10.4.1. Overview

3.10.4.2. Removing A Key Assignment

3.10.4.3. Adding A Key Assignment

3.10.4.4. Changing A Key Assignment

3.11. Audio Map

3.11.1. Overview

3.11.2. Key/Clip References

3.11.3. Audio Map

3.12. Metadata

3.1. Overview

The aurantium file format is optimized for the storage of audio data used for real-time audio applications. The format provides the following features:

3.1.2. Features

Detailed information about the format of audio data is included in all files. Audio data, in the common case, can be introspected without requiring consulting any kind of external specification. The information provided about audio data includes sampling rate, channel depth and type information, and byte ordering for formats that use components larger than a single octet.

Ease of parsing. The binary format is designed to facilitate easy and secure parsing without requiring backtracking or unbounded storage use. A competent developer should be able to implement a full parser within a week or two of work.

Carefully layered metadata. Consumers are not required to understand everything about the underlying audio data in order to make use of it. For example, if audio data is encoded using an unusual and/or proprietary format, consumers can still trivially extract the raw data even if they cannot necessarily understand the data.

Extensibility. The format consists of explicitly-sized sections with a well-defined ordering. Consumers can trivially skip sections that they do not understand. Sections carry unique 64-bit identifiers; if a section has an identifier not recognized by a consumer, the consumer may skip the section. The raw bytes that comprise a section can be extracted regardless of whether or not the consumer understands them. This specification defines a number of "standard" audio data types that consumers are expected to understand, but the format also allows for declaring new self-describing audio data types.

Practical metadata. The format provides a standard section that contains UTF-8 encoded keys and values intended to hold arbitrary metadata. Metadata that cannot be expressed as a UTF-8 string can be included as a custom section that can be skipped by consumers that do not recognize it.

This section of the specification documents the abstract model that the aurantium format uses to express all of the above.

3.2. Divisibility By 8

This specification makes frequent use of values that must be evenly divisible by 8. Formally, a number n is evenly divisible by 8 if n mod 8 = 0.

3.2.2. Divisible8

Definition divisible8 (x : nat) : Prop :=
  modulo x 8 = 0.

The property of being divisible by 8 is preserved over addition. That is, if two numbers n and m are divisible by 8, then n + m is divisible by 8.

3.2.4. Divisible8 Addition

Theorem divisiblity8Add : forall (x y : nat),
  divisible8 x -> divisible8 y -> divisible8 (x + y).
Proof.
  (* Proof omitted for brevity; see Divisible8.v for proofs. *)
Qed.

3.3. Bits & Octets

A bit is a single digit in the base-2 numbering system. A bit may either be 0 or 1:

3.3.2. Bit

Inductive bit : Set :=
  | B0
  | B1.

A sequence of bits may be divided into groups of eight bits known as octets. We avoid the use of the term byte because a byte hasn't consistently been equivalent to eight bits throughout all of computing history. An octet may either be exact or a remainder. An octet may be a remainder if the length of the sequence of bits used to produce it was not evenly divisible by 8. The first n groups of 8 bits consumed from a sequence of bits s will produce octets that are exact, with the remaining k bits (where k < 8) will produce at most one remainder octet. The remainder octet, if any, has it's least significant 8 - k bits set to 0.

3.3.4. Octet

Inductive octet : Set :=
  | OctExact  : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet
  | OctRemain : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet.

The sequence of bits s will be consumed in order such that octets are filled from most significant to least significant bit order.

If the sequence of octets o produced is arranged such that the first bit of s appears as the most significant bit of the first octet in o, then o is said to be in big-endian order.

3.3.7. Big Endian Octets (Aux)

Fixpoint octetsBigEndianAux
  (bits   : list bit)
  (octets : list octet)
: list octet :=
  match bits with
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest) =>
    octets ++ [OctExact b7 b6 b5 b4 b3 b2 b1 b0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 b1 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: rest) =>
    octets ++ [OctRemain b7 b6 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: rest) =>
    octets ++ [OctRemain b7 B0 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | [] =>
    octets
  end.

3.3.8. Big Endian Octets

Definition octetsBigEndian (bits : list bit) : list octet :=
  octetsBigEndianAux bits [].

If the sequence of octets o produced is arranged such that the first bit of s appears as the most significant bit of the last octet in o, then o is said to be in little-endian order.

3.3.10. Little Endian Octets

Definition octetsLittleEndian (bits : list bit) : list octet :=
  rev (octetsBigEndianAux bits []).

A sequence of bits s such that divisible8 (length s) will produce a sequence consisting of entirely exact octets.

3.3.12. Divisible8 Exact Octets (Big endian)

Theorem octetsBigEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsBigEndian b).
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

3.3.13. Divisible8 Exact Octets (Little endian)

Theorem octetsLittleEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsLittleEndian b).
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

A sequence of bits s such that ¬ divisible8 (length s) will produce a remainder octet.

3.3.15. Divisible8 Exact Octets (Big endian)

Theorem octetsBigEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> exists o, In o (octetsBigEndian b) /\ octetIsRemainder o.
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

3.3.16. Divisible8 Exact Octets (Little endian)

Theorem octetsLittleEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> exists o, In o (octetsLittleEndian b) /\ octetIsRemainder o.
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

3.4. List Intersection

This specification makes use of a concept of list intersection. Specifically, the intersectionPairs function. The function takes lists ea and eb, and a function f, and for each element a of ea for which (f a eb) returns Some r, the pair (a, r) is concatenated to a list of results.

3.4.2. intersectionPairs

Fixpoint intersectionPairs
  {A     : Set}
  (f     : A -> list A -> option A)
  (ea eb : list A)
: list (A * A) :=
  match ea with
  | nil => nil
  | cons a ea_rest =>
    match f a eb with
    | Some r => (a, r) :: intersectionPairs f ea_rest eb
    | None   =>           intersectionPairs f ea_rest eb
    end
  end.

In practice, intersectionPairs is essentially used to answer the question "For each of the the elements I have in this list, what are the corresponding elements in this other list, according to f?". The finds proposition specifies a property that f should always have, and the intersectionPairsIn theorem demonstrates that intersectionPairs is correct if f has this property.

3.4.4. finds

Definition finds
  {A  : Set}
  (f  : A -> list A -> option A)
  (x  : A)
  (y  : A)
  (ys : list A)
: Prop :=
  f x ys = Some y <-> In y ys.

3.4.5. intersectionPairsIn

Theorem intersectionPairsIn : forall (A : Set) (ea eb : list A) efa efb f,
  (forall x y ys, finds f x y ys) ->
    In (efa, efb) (intersectionPairs f ea eb) ->
      In efa ea /\ In efb eb.
Proof.
  (* Proof omitted for brevity; see Intersection.v for proofs. *)
Qed.

3.5. Interpolation

This specification makes use of interpolation functions.

A number in ℝ is normalized iff it is in the range [0, 1]:

3.5.3. isNormalized

Definition isNormalized (x : R) : Prop :=
  0 <= x /\ x <= 1.

Normalization is preserved over multiplication:

3.5.5. isNormalized Multiplication

Theorem isNormalizedMult : forall x y,
  isNormalized x -> isNormalized y -> isNormalized (Rmult x y).
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

The between function determines where a number falls between two other numbers, expressed as a normalized number:

3.5.7. Between

Definition between
  (x    : R)
  (low  : R)
  (high : R)
: R :=
  let n := x - low in
  let d := high - low in
    match Reqb d 0 with
    | true  => x
    | false => n / d
    end.

The between function will always return a value in [0, 1] given the appropriate preconditions:

3.5.9. Between Normalized

Theorem betweenNorm : forall x lo hi,
  lo < hi
    -> lo <= x <= hi
      -> isNormalized (between x lo hi).
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

The interpolate function linearly interpolates a value between a lower and upper value based on a normalized number:

3.5.11. Interpolate

Definition interpolate
  (x : R)
  (y : R)
  (f : R)
: R :=
  (x * (1 - f)) + (y * f).

The interpolate function has the following properties when the input is normalized:

3.5.13. Interpolate Range 1

Lemma interpolateRange1 : forall x y f,
  x <= y
    -> isNormalized f
      -> x <= interpolate x y f <= y.
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

3.5.14. Interpolate Range 2

Lemma interpolateRange2 : forall x y f,
  y <= x
    -> isNormalized f
      -> y <= interpolate x y f <= x.
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

3.6. Hash

This specification makes use of cryptographic hash functions.

A hashValue value indicates that some data has been hashed using a cryptographic hash function, and the result has been encoded as an ASCII hexadecimal string.

3.6.3. hashValue

Inductive hashValue : Set := hashValueMake {
  hvAlgorithm : hashAlgorithm;
  hvValue     : string
}.

The hvAlgorithm field indicates the algorithm used to produce the hash.

The hvValue field is the hash value encoded as an ASCII hexadecimal string.

A hashAlgorithm value specifies which hash function was used to produce a particular hash.

3.6.7. hashAlgorithm

Inductive hashAlgorithm : Set :=
  | HA_SHA256
  .

A value of HA_SHA256 specifies SHA-256.

3.7. Descriptors

A descriptor is a UTF-8 encoded string that describes an object in a aurantium file.

3.7.2. Descriptor

Definition descriptor := string.

An object is describable iff it has an associated descriptor.

3.7.4. Describable

Class describable (A : Set) := {
  descriptorOf : A -> descriptor
}.

Descriptors must be Lanark dotted strings. Briefly, descriptor strings must match the following regular expression:

3.7.6. Lanark Strings

([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}

Some areas of this specification allow for structures to contain new, externally-defined descriptors (to allow for third parties to add extensions to the specification). These externally-defined descriptors MUST NOT start with the string com.io7m.aurantium..

This specification defines the descriptors that must be returned for various objects in the specification by giving function definitions that map values to descriptor strings.

3.8. Compatibility

3.8.1. Overview

3.8.2. File Format Versioning vs. Data Versioning

3.8.2.1. Overview

3.8.2.2. File Format

3.8.2.3. Data Versioning

3.8.3. Identifiers

3.8.4. Changes

3.8.1. Overview

The aurantium file format makes a strong commitment to forwards and backwards compatibility. The format attempts to guarantee this commitment with a combination of the following:

3.8.1.2. Compatibility Measures

Use of semantic versioning in the file format definition. The inclusion of major and minor semantic version numbers into the file format itself means that software can know, unambiguously, whether or not it can open a given file based on the contents of the file header alone.

A strict, unambiguous, mathematical specification of the structure and semantics of the format. This means that, long after the aurantium software has died, developers of the future can write new implementations with behaviour that they know correctly handles the format.

The inclusion of unique identifiers and version numbers into each file; once an audio map has been created, it is considered to be immutable. Editing an audio map entails creating a new version of the existing one with an incremented version number. This allows applications to specify exact, versioned dependencies on audio map files in much the same way as software development tools can specify versioned dependencies on software libraries.

An exact and precise description of which changes are considered to be "compatible" changes, and which changes are considered to be "incompatible". This means that new versions of files cannot be released that will silently break compatibility with existing consumers; the tools around the file format will catch these mistakes before publication.

3.8.2. File Format Versioning vs. Data Versioning

3.8.2.1. Overview

The aurantium format has two types of versioning.

3.8.2.2. File Format

The file format itself is versioned using a major and minor version number. This is file format versioning. Informally, the file format is designed such that software that was written to support major version x of the file format is guaranteed to be able to support major version x for any minor version y. The software is not guaranteed to be able to support major version x + 1 or x - 1 without code additions.

File format version changes coincide with new releases of the aurantium specification, and so any compatibility changes are documented in that specification.

3.8.2.3. Data Versioning

Files produced in the aurantium format contain user-specified major and minor version numbers. This allows users to produce audio map files upon which other users can safely specify versioned dependencies. The rules described here in the Compatibility module refer to those version numbers, and not the file format version.

3.8.3. Identifiers

An aurantium audio map file contains an identifier specified by the author of the file. The identifier is described by the following type:

3.8.3.2. Identifier

Inductive identifier : Set := identifierMake {
  idGroup             : string;
  idName              : string;
  idVersionMajor      : nat;
  idVersionMinor      : nat;
  idVersionMajorRange : idVersionMajor <= 4294967295;
  idVersionMinorRange : idVersionMinor <= 4294967295
}.

The idGroup and idName fields specify unique identifiers for this audio map file [1].

Identifiers must be Lanark dotted strings.

The idVersionMajor field specifies a major version number for the file. When an incompatible change is made to a file, the next version of the file that is released must increment the major version number, and reset the minor version number to zero.

The idVersionMinor field specifies a minor version number for the file. When a compatible change is made to a file, the next version of the file that is released must increment the minor version number.

Implementations may choose to relax these rules for major version 0; files with major version 0 should be considered unstable development versions.

3.8.4. Changes

When a change is made to a file, the nature of that change dictates whether the major or minor version number needs to be incremented when a new version of the file is released for public consumption.

The compatVersionChange type encodes the three possible situations:

3.8.4.3. compatVersionChange

Inductive compatVersionChange : Set :=
  (** No version change is required. *)
  | CVersionChangeNone
  (** The change requires a minor version number increment. *)
  | CVersionChangeMinor
  (** The change required a major version number increment. *)
  | CVersionChangeMajor
  .

The compatVersionChangeMax function denotes the significance of changes; a change requiring a major version increment is more significant than a change that requires a minor version increment. Both are more significant than no change at all.

3.8.4.5. compatVersionChangeMax

Definition compatVersionChangeMax
  (x y : compatVersionChange)
: compatVersionChange :=
  match (x, y) with
  | (CVersionChangeMajor , _                  ) => CVersionChangeMajor
  | (_                   , CVersionChangeMajor) => CVersionChangeMajor
  | (CVersionChangeMinor , CVersionChangeNone ) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeMinor , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeNone ) => CVersionChangeNone
  end.

The function is reflexive, commutative, and associative.

3.8.4.7. compatVersionChangeMaxRefl

Theorem compatVersionChangeMaxRefl : forall x,
  compatVersionChangeMax x x = x.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.

3.8.4.8. compatVersionChangeMaxComm

Theorem compatVersionChangeMaxComm : forall x y,
  compatVersionChangeMax x y = compatVersionChangeMax y x.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.

3.8.4.9. compatVersionChangeMaxAssoc

Theorem compatVersionChangeMaxAssoc : forall x y z,
  compatVersionChangeMax x (compatVersionChangeMax y z) = compatVersionChangeMax (compatVersionChangeMax x y) z.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.

Footnotes

1 | The combination of a group, name, and version makes sample maps compatible with software repositories such as Maven Central. References to this footnote: 1

3.9. Clips

3.9.1. Overview

3.9.2. Metadata

3.9.3. Sampling & Channels

3.9.4. Endianness

3.9.5. Formats

3.9.5.1. Uncompressed

3.9.5.1.1. Pulse Code Modulation

3.9.5.2. Compressed

3.9.5.2.1. FLAC

3.9.5.3. Types

3.9.6. Loop Ranges

3.9.7. Clips

3.9.8. Clip Lists

3.9.9. Compatibility

3.9.9.1. Overview

3.9.9.2. Removing A Clip

3.9.9.3. Adding A Clip

3.9.9.4. Changing A Clip

3.9.1. Overview

A clip is a section of audio data along with the metadata required to interpret that audio data correctly.

3.9.2. Metadata

In order to make it possible to interpret the audio data associated with a clip, various pieces of metadata are required. At a minimum, the following values must be known:

3.9.2.2. Required Audio Metadata

The format of the audio data, such as unsigned pulse code modulation, signed pulse code modulation, FLAC, and etc.

The sample rate of the audio data, expressed as samples per second.

The sample depth of the audio data, expressed as bits per sample.

The number of channels in the audio data.

The octet order of the audio data, assuming the sample depth is greater than 8 bits.

The size of the audio data, expressed in octets.

3.9.3. Sampling & Channels

Digital audio signals are broken up into individual values called samples. A sample can intuitively be thought of the amplitude value of a continuous signal at a given point in time. The precise manner in which the amplitude values of the continuous signal are mapped to the digital domain is known as the format of the data.

Digital signals are sampled at a fixed rate known as the sample rate. The sample rate is specified in samples-per-second. For example, a sample rate of 48000 indicates that 48000 sample values comprise one second of audio data.

Audio signals are often divided into multiple channels. For example, stereo audio is divided into left and right channels. In an audio signal with n channels, the individual sample values in each of the channels at a given time are collectively referred to as a sampling frame (or frame, in short). For example, in a stereo audio signal A, the sample value x in the left channel at time 0, and the sample value y in the right channel at time 0 can be viewed as the frame (x, y) at time 0. Conceptually, the audio signal A can be seen as a function A(t) = (p, q), where t is time, and (p, q) is the sampling frame at time t.

For uncompressed formats, the aurantium format mandates that audio be stored in interleaved form. That is, for an audio stream A consisting of n channels, the value of channel 0 at time t is stored, directly followed by the value of channel 1 at time t, continuing up to the value of channel n - 1 at t. The pattern is then repeated for the values at time t + 1, and so on. Note that the interleaving order is irrespective of sample endianness.

3.9.3.5. Interleaving

3.9.4. Endianness

When an encoding scheme is used that encodes amplitude values as values larger than a single octet, the endianness of the encoding must be specified. The aurantium format only supports big-endian and little-endian order for sample values.

3.9.5. Formats

3.9.5.1. Uncompressed

3.9.5.1.1. Pulse Code Modulation

3.9.5.1.1.1. Description

At the time of writing, the most commonly used encoding for digital audio data is so-called pulse code modulation (or PCM). A PCM-encoded audio signal represents a digital approximation of an idealized continuous audio signal produced by sampling the amplitude value of the continuous signal at a constant rate known as the sample rate. The resulting sampled values (typically expressed as values in ℝ in the range [-1, 1]) are scaled and quantized to the most appropriate value allowed by the sample depth. The actual quantized amplitude value chosen is dependent on the exact encoding scheme used, such as linear encoding.

3.9.5.1.1.1.2. PCM

In the above image, the vertical dashed lines represent the sample rate. The horizontal dashed lines represent the sample depth (the number of available quantization levels). The black curve represents the original continuous signal, and the red curve represents the resulting sampled, quantized signal.

The sample rate affects the maximum frequency that can be expressed in the sampled signal; a sample rate of r samples per second can express a frequency of no greater than r / 2 hertz, as demonstrated by the Nyquist–Shannon sampling theorem [1]. The sample depth affects the range of amplitude values that can be expressed in the sampled signal. For example, if each sampled value is quantized and stored as a 16-bit integer, there are exactly 65536 possible values to which amplitude values can be mapped.

3.9.5.1.1.2. Linear PCM

In a linear PCM encoding scheme, quantized amplitude values are mapped linearly across the available range of encoded values. Other schemes such as μ-law encode values according to a logarithmic scale. Linear PCM encoding is by far the most common encoding at the time of writing, and so is the only directly specified and supported PCM encoding in the aurantium format [2].

3.9.5.1.1.3. Signedness

When amplitude values are encoded into an integer-based PCM format, the question of signedness arises. A signed, n-bit linear PCM encoding scheme encodes an amplitude value in the range [-1, 1] to an integer value in the range [-(2 ^ (n - 1)), (2 ^ (n - 1)) - 1]. So, for example, for a 16-bit signed linear PCM encoding:

3.9.5.1.1.3.2. 16-bit Signed Example

An amplitude value of -1 will be encoded as -32768.

An amplitude value of 0 will be encoded as 0.

An amplitude value of 1 will be encoded as 32767.

An unsigned n-bit linear PCM encoding scheme encodes an amplitude value in the range [-1, 1] to an integer value in the range [0, 2 ^ n]. So, for example, for a 16-bit unsigned linear PCM encoding:

3.9.5.1.1.3.4. 16-bit Unsigned Example

An amplitude value of -1 will be encoded as 0.

An amplitude value of 0 will be encoded as 32768.

An amplitude value of 1 will be encoded as 65536.

More formally, the signed encoding function is specified as [3]:

3.9.5.1.1.3.6. Signed Linear Encoding

Definition pcmIntegerEncodeSigned
  (depth     : nat)
  (amplitude : R)
: R :=
  match Rle_dec 0 amplitude with
  | left _  => Rmult amplitude ((pow 2 (depth - 1)) - 1)
  | right _ => Rmult amplitude (pow 2 (depth - 1))
  end.

The unsigned encoding function is specified as:

3.9.5.1.1.3.8. Unsigned Linear Encoding

Definition pcmIntegerEncodeUnsigned
  (depth     : nat)
  (amplitude : R)
: R :=
  let s : R := Rplus (Rdiv amplitude 2%R) 0.5%R in
    Rmult s (pow 2 depth).

3.9.5.2. Compressed

3.9.5.2.1. FLAC

The aurantium format allows audio data to be stored in FLAC format.

A clip encoded in FLAC format has audio data consisting of exactly one FLAC bitstream. That is, a bitstream in FLAC format starting with the marker octets 0x664C6143. Because the FLAC bitstream format duplicates much of the metadata already specified by the aurantium format, implementations should take care to ensure that the metadata specified in the aurantium clip entry matches the relevant metadata in the FLAC bitstream.

3.9.5.3. Types

A number of formats are considered to be "standard" by the aurantium format and are described by the audioFormatType type:

3.9.5.3.2. Audio Format Type

Inductive audioFormatType : Set :=
  (** Pulse code modulation using signed values. *)
  | AFPCMLinearIntegerSigned : audioFormatType
  (** Pulse code modulation using unsigned values. *)
  | AFPCMLinearIntegerUnsigned : audioFormatType
  (** Pulse code modulation using floating point values. *)
  | AFPCMLinearFloat : audioFormatType
  (** FLAC-compressed audio. *)
  | AFFlac : audioFormatType
  (** A format not known by this specification. *)
  | AFUnknown : descriptor -> audioFormatType
  .

A value of AFPCMLinearIntegerSigned indicates linear PCM audio data in a signed integer format.

A value of AFPCMLinearIntegerUnsigned indicates linear PCM audio data in an unsigned integer format.

A value of AFPCMLinearFloat indicates linear PCM audio data in an IEEE-754 floating point format.

A value of AFFlac indicates FLAC audio data.

A value of AFUnknown indicates audio data in a format unknown to this specification. The descriptor associated with the value is expected to uniquely identify a format described by some external specification.

3.9.6. Loop Ranges

A loop range is a pair (f, e) where f is the index of the starting frame in a clip, and e is the index of the ending frame in a clip. The range of frames described by (f, e) are intended to represent a region of audio that can be seamlessly looped.

When a loop range is included in a given clip, implementations should treat the range as advisory. They are a means for the author of an audio map to state "if you wish to produce a sustained sound using this clip, this loop range will result in a seamless loop of audio". Implementations are free to ignore loop ranges entirely.

3.9.7. Clips

A clip is described by the following type:

3.9.7.2. Clip

Inductive clip : Set := clipMake {
  (** The unique identifier for the clip. *)
  clipId : nat;
  (** The clip name, for descriptive purposes. *)
  clipName : string;
  (** The clip audio format name. *)
  clipFormat : audioFormatType;
  (** The sample rate in bits per second. *)
  clipSampleRate : nat;
  (** The clip sample depth in bits per clip. *)
  clipSampleDepth : nat;
  (** The number of channels in the clip. *)
  clipChannels : nat;
  (** The endianness of the audio data. *)
  clipEndianness : octetOrder;
  (** The hash of the audio data. *)
  clipHash : hashValue;
  (** The offset of the first octet of audio data. *)
  clipOffset : nat;
  (** The size of the audio data in octets. *)
  clipSize : nat;
  (** An optional loop region. *)
  clipLoopRange : option loopRange
}.

3.9.7.3. Clip (Invariants)

Definition clipInvariants (c : clip) : Prop :=
     (clipId                        c <= 4294967295)
  /\ (clipSampleRate                c <= 4294967295)
  /\ (clipSampleDepth               c <= 4294967295)
  /\ (clipChannels                  c <= 4294967295)
  /\ (clipOffset                    c <= 18446744073709551615)
  /\ (clipSize                      c <= 18446744073709551615)
  /\ (clipFrameCountLoopRangeOption c (clipLoopRange c))
  .

3.9.7.4. Clip Frame Count

Definition clipFrameCount (c : clip) : nat :=
  (clipSize c) / (clipSampleDepth c / 8).

3.9.7.5. Clip Loop Range

Definition clipFrameCountLoopRange
  (c  : clip)
  (lr : loopRange)
: Prop :=
  (lrFrameEndInclusive lr) < (clipFrameCount c).

3.9.7.6. Clip Loop Range (Optional)

Definition clipFrameCountLoopRangeOption
  (c  : clip)
  (lr : option loopRange)
: Prop :=
  match lr with
  | Some r => clipFrameCountLoopRange c r
  | None   => True
  end.

The clipId field specifies a unique (within the aurantium file) identifier for the clip. This can be used to refer to the clip in other parts of the file.

The clipName field specifies a descriptive name for the clip. Names do not need to be unique, and do not contribute in any significant way to the semantics of the model; they are purely there to provide a descriptive name that can be displayed in editors and other applications.

The clipFormat field specifies the format of the audio data for this clip.

The clipSampleRate field specifies the sample rate of the audio data for this clip.

The clipSampleDepth field specifies the number of bits that comprise a single sample in the audio data.

The clipChannels field specifies the number of channels that are present in the audio data for this clip.

The clipEndianness field specifies the endianness of sample values in the audio data for this clip.

The clipHash field records a cryptographic hash of the audio data for this clip. This field serves both as an integrity check for audio data, and to allow for quickly determining if two audio maps differ in their audio data.

The clipOffset field specifies the offset in octets of the start of the audio data for this clip, relative to the beginning of the file section.

The clipSize field specifies the size in octets of the audio data for this clip.

The clipLoopRange field specifies an optional loop range for this clip.

3.9.8. Clip Lists

All of the clips in an aurantium file are placed into a single list.

3.9.8.2. Clips

Inductive clips : Set := clipsMake {
  clipsList         : list clip;
  clipsIdSorted     : clipsListIdIsSorted clipsList;
  clipsOffsetSorted : clipsListOffsetIsSorted clipsList;
}.

The proposition clipsListIdIsSorted states that the identifiers of clips must provided in ascending order (but are allowed to have gaps).

3.9.8.4. Clip IDs Sorted

Inductive clipsListIdIsSorted : list clip -> Prop :=
  | ClipIdOne  : forall s,
      clipsListIdIsSorted [s]
  | ClipIdCons : forall s0 s1 ss,
    (clipId s0) < (clipId s1) ->
      clipsListIdIsSorted (s0 :: ss) ->
        clipsListIdIsSorted (s1 :: s0 :: ss).

The proposition clipsListOffsetIsSorted states that the offset of the audio data for clips cannot overlap, and must be provided in ascending order.

3.9.8.6. Clip Offsets Sorted

Inductive clipsListOffsetIsSorted : list clip -> Prop :=
  | ClipOffsetOne : forall s,
    clipsListOffsetIsSorted [s]
  | ClipOffsetCons : forall s0 s1 ss,
    ((clipOffset s1) + (clipSize s1)) < clipOffset s0 ->
      clipsListOffsetIsSorted (s0 :: ss) ->
        clipsListOffsetIsSorted (s1 :: s0 :: ss).

It follows that the list of clips within a file is not allowed to be empty.

3.9.8.8. Clips Non-Empty

Lemma clipsNonEmpty : forall (s : clips),
  [] <> clipsList s.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

3.9.9. Compatibility

3.9.9.1. Overview

This section enumerates all of the possible changes that can be made to a set of clips, and describes whether each of the changes is a compatibility-breaking major change, or a minor change.

The complete procedure for determining the compatibility of changes to a list of clips is given by the clipsCompatCompareFull:

3.9.9.1.3. clipsCompatCompareFull

Definition clipsCompatCompareFull
  (ca cb : list clip)
: list compatVersionChangeRecord :=
  let f              := (fun c cs => clipForId (clipId c) cs) in
  let removed        := clipsRemoved ca cb in
  let added          := clipsAdded ca cb in
  let changed        := intersectionPairs f ca cb in
  let removedChanges := clipsCompatCompareRemoved removed in
  let addedChanges   := clipsCompatCompareAdded added in
  let changedChanges := clipsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

This function composes the results of many compatibility checks, and returns a list of all of the changes. The definitions given in the compatibility module can then be used to determine the maximally significant change in the list of changes.

3.9.9.2. Removing A Clip

Removing an existing clip is a major change.

The clipsRemoved function determines the set of clips that were present in the old version of a clip list, but that are not present in the new one:

3.9.9.2.3. clipsRemoved

Definition clipsRemoved
  (ca : list clip)
  (cb : list clip)
: list clip :=
  filter (fun c =>
    match clipForId (clipId c) cb with
    | None   => false
    | Some _ => true
    end) ca.

It follows that if the list of removed elements is non-empty, then the clipsCompatCompareFull function returns at least one major change:

3.9.9.2.5. clipsCompatCompareFull Major

Theorem clipsCompatCompareMajor0 : forall ca cb,
  [] <> clipsRemoved ca cb ->
    compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
      = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

3.9.9.3. Adding A Clip

Adding a new clip is a minor change.

The set of clips that have been added can be expressed in terms of the clipsRemoved function with the arguments applied in reverse order. Intuitively, if ca is the set of old clips, and cb is the set of new clips, the clipsRemoved states which elements of cb must be removed to produce ca; this is the set of newly added clips.

3.9.9.3.3. clipsAdded

Definition clipsAdded
  (ca : list clip)
  (cb : list clip)
: list clip :=
  clipsRemoved cb ca.

It follows that if the only changes are additions, then the clipsCompatCompareFull function returns a minor change:

3.9.9.3.5. clipsCompatCompareFull Minor

Theorem clipsCompatCompareMinor0 : forall ca cb,
  [] = clipsRemoved ca cb ->
    [] <> clipsAdded ca cb ->
      (forall f, [] = intersectionPairs f ca cb) ->
        compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
          = CVersionChangeMinor.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

3.9.9.4. Changing A Clip

Changing an existing clip is a major change.

If ca is the set of old clips, and cb is the set of new clips, the intersectionPairs function determines which clips are in both sets.

Clip equality is decidable:

3.9.9.4.4. Equality Decidable

Theorem clipEqDec : forall (x y : clip),
  {x = y}+{x <> y}.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

Clips are compared using this comparison function:

3.9.9.4.6. Clip Compare

Definition clipCompatCompare
  (c0 c1 : clip)
: compatVersionChangeRecord :=
  match clipEqDec c0 c1 with
  | left _ =>
    CVRMake CVersionChangeNone ""
  | right _ =>
    CVRMake CVersionChangeMajor "The values of the clip were changed."
  end.

3.9.9.4.7. Clip Compare Changed

Definition clipsCompatCompareChanged
  (r : list (clip * clip))
: list compatVersionChangeRecord :=
  map (fun p => clipCompatCompare (fst p) (snd p)) r.

Footnotes

1 | See https://en.wikipedia.org/wiki/Nyquist%E2%80%93Shannon_sampling_theorem. References to this footnote: 1
2 | Implementations are free to provide other encodings as custom extensions, but should not expect good interoperability with other implementations if they do. References to this footnote: 1

3

The functions are specified as returning a value of type R due to limitations in the Rocq standard library's handling of the conversion of real number values to integers. The functions should be understood to have their return values rounded to integer values in practice.

References to this footnote: 1

3.10. Key Assignments

3.10.1. Overview

3.10.2. Keys

3.10.2.1. Numbering

3.10.2.2. Velocity

3.10.3. Key Assignments

3.10.3.1. Description

3.10.3.2. Key Assignment Evaluation

3.10.3.2.1. Evaluation

3.10.3.2.2. Matching

3.10.3.2.3. Amplitude

3.10.3.2.4. Playback Rate

3.10.3.2.5. Complete Procedure

3.10.3.3. Examples

3.10.3.4. Lists

3.10.4. Compatibility

3.10.4.1. Overview

3.10.4.2. Removing A Key Assignment

3.10.4.3. Adding A Key Assignment

3.10.4.4. Changing A Key Assignment

3.10.1. Overview

The aurantium format is intended to be used in sampler applications. As such, it provides a means to map clips to keyboard input.

3.10.2. Keys

3.10.2.1. Numbering

The aurantium format assumes an abstract model of keyboard input where keys are simply assigned ascending natural numbers. This aligns with instrument control protocols such as MIDI and OSC. There is no direct correspondence between MIDI or OSC keys in the aurantium format; applications are expected to perform their own mapping to aurantium keys as needed. Keys are assumed to use the 12-TET tuning system; applications requiring different tuning systems will have to calculate their own clip playback rates.

3.10.2.2. Velocity

The aurantium format assumes the existence of per-key velocity values. A velocity value is a value of type ℝ in the range [0, 1] and can be understood to be a measure of the dynamics of a given note. A velocity value of 0 indicates that a note was played as softly as possible, whilst a velocity value of 1 indicates that a note was played as hard as possible. Velocity values can be used to interpolate between different clips assigned to a key in order to change the timbre of the resulting sound in response to dynamics.

3.10.3. Key Assignments

3.10.3.1. Description

A key assignment associates a clip with a range of keys, over a configurable velocity range. Key assignments allow for relatively complex control over the amplitude of each assigned clip, where amplitude can be dependent on both the position of the key within a specified range, and the velocity of the played note. An arbitrary number of clips can be assigned to overlapping ranges, allowing for complex layering of clips.

A key assignment is described by the following type:

3.10.3.1.3. Key Assignment

Inductive keyAssignment : Set := {
  (** The unique identifier of the key assignment. *)
  kaId : nat;
  (** The lowest key value that will trigger this clip. *)
  kaValueStart : nat;
  (** The key value at which the clip plays at the normal playback rate. *)
  kaValueCenter: nat;
  (** The highest key value that will trigger this clip. *)
  kaValueEnd : nat;
  kaValueEndRange : le kaValueEnd 294967295;
  (** The key values must be ordered. *)
  kaValueStartOrder : le kaValueStart kaValueCenter;
  kaValueCenterOrder : le kaValueCenter kaValueEnd;
  (** The clip that will be triggered. *)
  kaClipId : nat;
  (** The amplitude at which this clip will be played when at the lowest key value. *)
  kaAmplitudeAtKeyStart : R;
  (** The amplitude at which this clip will be played when at the center key value. *)
  kaAmplitudeAtKeyCenter : R;
  (** The amplitude at which this clip will be played when at the highest key value. *)
  kaAmplitudeAtKeyEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtKeyStartNormal : isNormalized kaAmplitudeAtKeyStart;
  kaAmplitudeAtKeyCenterNormal : isNormalized kaAmplitudeAtKeyCenter;
  kaAmplitudeAtKeyEndNormal : isNormalized kaAmplitudeAtKeyEnd;
  (** The velocity value at which this clip starts to be triggered. *)
  kaAtVelocityStart : R;
  (** The velocity value at which the amplitude of this clip is at maximum. *)
  kaAtVelocityCenter : R;
  (** The velocity value at which this clip stops being triggered. *)
  kaAtVelocityEnd : R;
  (** The velocity values are normalized values and are correctly ordered. *)
  kaAtVelocityStartNormal : isNormalized kaAtVelocityStart;
  kaAtVelocityCenterNormal : isNormalized kaAtVelocityCenter;
  kaAtVelocityEndNormal : isNormalized kaAtVelocityEnd;
  kaAtVelocityStartOrder : kaAtVelocityStart <= kaAtVelocityCenter;
  kaAtVelocityCenterOrder : kaAtVelocityCenter <= kaAtVelocityEnd;
  (** The amplitude at which this clip will be played when at the starting velocity value. *)
  kaAmplitudeAtVelocityStart : R;
  (** The amplitude at which this clip will be played when at the center velocity value. *)
  kaAmplitudeAtVelocityCenter : R;
  (** The amplitude at which this clip will be played when at the end velocity value. *)
  kaAmplitudeAtVelocityEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtVelocityStartNormal : isNormalized kaAmplitudeAtVelocityStart;
  kaAmplitudeAtVelocityCenterNormal : isNormalized kaAmplitudeAtVelocityCenter;
  kaAmplitudeAtVelocityEndNormal : isNormalized kaAmplitudeAtVelocityEnd;
  (** The associated key assignment flags. *)
  kaFlags : list keyAssignmentFlag;
  kaFlagsUnique : NoDup kaFlags;
}.

The kaId field specifies a unique (within the aurantium file) identifier for the key assignment. This can be used to refer to the key assignment in other parts of the file.

The kaValueStart, kaValueCenter, and kaValueEnd fields specify the range of keys to which this key assignment applies. This key assignment will only be evaluated if a key falls within this given range.

The values of kaValueStart, kaValueCenter, and kaValueEnd must obey kaValueStart <= kaValueCenter <= kaValueEnd.

The kaId field specifies the clip associated with this key assignment.

The kaAmplitudeAtKeyStart, kaAmplitudeAtKeyCenter, and kaAmplitudeAtKeyEnd fields specify the amplitude values that will be produced by evaluation for each key within the range given by [kaValueStart, kaValueEnd]. The amplitude values must be in the range [0, 1]. The amplitude values for keys within the range [kaValueStart, kaValueCenter] are linearly interpolated between the values (kaAmplitudeAtKeyStart, kaAmplitudeAtKeyCenter), and the amplitude values for keys within the range [kaValueCenter, kaValueEnd] are linearly interpolated between the values (kaAmplitudeAtKeyCenter, kaAmplitudeAtKeyEnd).

All amplitude values must be normalized.

The kaAtVelocityStart, kaAtVelocityCenter, and kaAtVelocityEnd fields specify the range of velocity values to which this key assignment applies. This key assignment will only be evaluated if a key's velocity value falls within this given range.

The kaAtVelocityStart, kaAtVelocityCenter, and kaAtVelocityEnd values must be normalized.

The kaAtVelocityStart, kaAtVelocityCenter, and kaAtVelocityEnd values must obey kaAtVelocityStart <= kaAtVelocityCenter <= kaAtVelocityEnd.

The kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityCenter, and kaAmplitudeAtVelocityEnd fields specify the amplitude values that will be produced by evaluation for each velocity value within the range given by [kaAtVelocityStart, kaAtVelocityEnd]. The amplitude values must be in the range [0, 1]. The amplitude values for velocities within the range [kaAtVelocityStart, kaAtVelocityCenter] are linearly interpolated between the values (kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityCenter), and the amplitude values for keys within the range [kaAtVelocityCenter, kaAtVelocityEnd] are linearly interpolated between the values (kaAmplitudeAtVelocityCenter, kaAmplitudeAtVelocityEnd).

The kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityCenter, and kaAmplitudeAtVelocityEnd values must be normalized.

The kaFlags field specifies a set of extra metadata flags for the key assignment. There must be no duplicate flags in the list.

3.10.3.2. Key Assignment Evaluation

3.10.3.2.1. Evaluation

When a key k is triggered with velocity v, it is necessary to evaluate zero or more key assignments to obtain all of the required audio data for the given note.

Evaluation produces a possibly-empty list of key assignment evaluations represented by the following type:

3.10.3.2.1.3. Key Evaluation

Inductive keyEvaluation : Set := keyEvaluationMake {
  keyEvaluationClipId                  : nat;
  keyEvaluationVelocityAmplitude       : R;
  keyEvaluationVelocityAmplitudeNormal : isNormalized keyEvaluationVelocityAmplitude;
  keyEvaluationKeyAmplitude            : R;
  keyEvaluationKeyAmplitudeNormal      : isNormalized keyEvaluationKeyAmplitude;
  keyEvaluationRate                    : R;
  keyEvaluationRateNonNegative         : 0 <= keyEvaluationRate
}.

The keyEvaluationClipId field specifies the identifier of the clip from which audio data should be sampled.

The keyEvaluationVelocityAmplitude field specifies the resulting amplitude of the clip based on how the key assignment is configured to respond to velocity values.

The keyEvaluationKeyAmplitude field specifies the resulting amplitude of the clip based on how the key assignment is configured to respond to the key value.

Applications are, in practice, expected to multiply keyEvaluationVelocityAmplitude and keyEvaluationKeyAmplitude together and use the resulting amplitude value to scale the values sampled from the associated clip.

The keyEvaluationRate field specifies the playback rate that should be used to access the associated clip based upon the key value.

The following subsections describe how these results are calculated.

3.10.3.2.2. Matching

A key assignment for a given key can only be evaluated if the key assignment matches the key's value and velocity. A key and velocity are said to match a key assignment if the following proposition holds:

3.10.3.2.2.2. Key Assignment Matching

Definition keyAssignmentMatches
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: Prop :=
  let p0 := ((kaValueStart assignment) <= key)%nat in
  let p1 := (key <= (kaValueEnd assignment))%nat in
  let p2 := ((kaAtVelocityStart assignment) <= velocity)%R in
  let p3 := (velocity <= (kaAtVelocityEnd assignment))%R in
    p0 /\ p1 /\ p2 /\ p3.

Determining if the proposition holds is decidable:

3.10.3.2.2.4. Key Assignment Matching Decidability

Theorem keyAssignmentMatchesDecidable : forall k v a,
  {keyAssignmentMatches k v a}+{~keyAssignmentMatches k v a}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.3.2.3. Amplitude

3.10.3.2.3.1. Key

A matching key assignment's key amplitude is calculated by taking the value of the current key k, and returning a value in the range [0, 1] that describes k's position in the range [kaValueStart, kaValueEnd]. A value of 0 indicates that k = kaValueStart, whilst a value of 1 indicates that k = kaValueEnd. This value is calculated using the between function.

The value returned from the between function is then used to linearly interpolate between values in the range [kaAmplitudeAtKeyStart, kaAmplitudeAtKeyEnd]:

3.10.3.2.3.1.3. Key Amplitude Evaluation

Definition keyAssignmentEvaluateAmplitudeForKey
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  let kLow := kaValueStart assignment in
  let kMid := kaValueCenter assignment in
  let kTop := kaValueEnd assignment in
    match Nat.compare key kMid with
    | Eq => kaAmplitudeAtKeyCenter assignment
    | Lt =>
      match Compare_dec.lt_dec kLow kMid with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kLow) (INR kMid) in
          interpolate
            (kaAmplitudeAtKeyStart assignment)
            (kaAmplitudeAtKeyCenter assignment)
            f
      end
    | Gt =>
      match Compare_dec.lt_dec kMid kTop with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kMid) (INR kTop) in
          interpolate
            (kaAmplitudeAtKeyCenter assignment)
            (kaAmplitudeAtKeyEnd assignment)
            f
      end
    end.

This function is guaranteed to produce amplitude values that are in the range [0, 1]:

3.10.3.2.3.1.5. Key Amplitude Evaluation Normalized

Theorem keyAssignmentEvaluateAmplitudeForKeyNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForKey k a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.3.2.3.2. Velocity

A matching key assignment's velocity amplitude is calculated by taking the velocity of the current key v, and returning a value in the range [0, 1] that describes v's position in the range [kaAtVelocityStart, kaAtVelocityEnd]. A value of 0 indicates that v = kaAtVelocityStart, whilst a value of 1 indicates that v = kaAtVelocityEnd. This value is calculated using the between function.

The value returned from the between function is then used to linearly interpolate between values in the range [kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityEnd]:

3.10.3.2.3.2.3. Velocity Amplitude Evaluation

Definition keyAssignmentEvaluateAmplitudeForVelocity
  (velocity   : R)
  (assignment : keyAssignment)
: R :=
  let kLow := kaAtVelocityStart assignment in
  let kMid := kaAtVelocityCenter assignment in
  let kTop := kaAtVelocityEnd assignment in
    match Rcompare velocity kMid with
    | Eq => kaAmplitudeAtVelocityCenter assignment
    | Lt =>
      match Rlt_dec kLow kMid with
      | left _ =>
        let f := between velocity kLow kMid in
          interpolate
            (kaAmplitudeAtVelocityStart assignment)
            (kaAmplitudeAtVelocityCenter assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    | Gt =>
      match Rlt_dec kMid kTop with
      | left _ =>
        let f := between velocity kMid kTop in
          interpolate
            (kaAmplitudeAtVelocityCenter assignment)
            (kaAmplitudeAtVelocityEnd assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    end.

This function is guaranteed to produce amplitude values that are in the range [0, 1]:

3.10.3.2.3.2.5. Velocity Amplitude Evaluation Normalized

Theorem keyAssignmentEvaluateAmplitudeForVelocityNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForVelocity v a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.3.2.4. Playback Rate

The clip associated with this key assignment should be played at normal playback rate when the incoming key is equal to kaValueCenter, and should be pitched up accordingly for keys less than or equal to kaValueEnd, and pitched down accordingly for keys greater than or equal to kaValueStart.

A matching key assignment's playback rate is calculated by taking the value of the current key k and determining how many semitones, if any, k is above or below kaValueCenter. The number of semitones is used to calculate a pitch ratio for the playback rate:

3.10.3.2.4.3. Semitone Pitch Ratio

Definition semitonesPitchRatio (semitones : R) : R :=
  Rpower 2.0 (Rdiv semitones 12.0).

Intuitively, if the difference between k and kaValueCenter is 0, the resulting ratio is 1.0. If the difference between k and kaValueCenter is 12, the resulting ratio is 2.0. If the difference between k and kaValueCenter is -12, the resulting ratio is 0.5.

The pitch ratio is returned by the keyAssignmentEvaluateRate function:

3.10.3.2.4.6. Key Assignment Rate Evaluation

Definition keyAssignmentEvaluateRate
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  match (in_dec keyAssignmentFlagEqDec FlagUnpitched (kaFlags assignment)) with
  | left _  => 1.0
  | right _ =>
    let kLow := kaValueStart assignment in
    let kMid := kaValueCenter assignment in
      match Nat.compare key kMid with
      | Eq => 1
      | Lt =>
        let delta := minus kMid key in
          semitonesPitchRatio (-(INR delta))
      | Gt =>
        let delta := minus key kMid in
          semitonesPitchRatio (INR delta)
      end
  end.

This function is guaranteed to produce a non-negative result:

3.10.3.2.4.8. Key Assignment Rate Evaluation Non-negative

Theorem keyAssignmentEvaluateRateNonNegative : forall k v a,
  keyAssignmentMatches k v a
    -> Rle 0 (keyAssignmentEvaluateRate k a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

If a key assignment has the FlagUnpitched value in its kaFlags field, the playback rate is always 1.0. This flag is intended to be used for samples that should not vary their pitch in response to key values.

3.10.3.2.5. Complete Procedure

The complete evaluation procedure for a key assignment is given by the keyAssignmentEvaluateFull function:

3.10.3.2.5.2. Key Assignment Full Evaluation

Definition keyAssignmentEvaluateFull
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: option keyEvaluation :=
  match keyAssignmentMatchesDecidable key velocity assignment with
  | right _ => None
  | left p  =>
    let clip  := kaClipId assignment in
    let ampV  := keyAssignmentEvaluateAmplitudeForVelocity velocity assignment in
    let ampVP := keyAssignmentEvaluateAmplitudeForVelocityNormalized _ _ _ p in
    let ampK  := keyAssignmentEvaluateAmplitudeForKey key assignment in
    let ampKP := keyAssignmentEvaluateAmplitudeForKeyNormalized _ _ _ p in
    let rate  := keyAssignmentEvaluateRate key assignment in
    let rateP := keyAssignmentEvaluateRateNonNegative _ _ _ p in
      Some (keyEvaluationMake clip ampV ampVP ampK ampKP rate rateP)
  end.

3.10.3.3. Examples

The configurable values exposed by key assignments allow for fairly complex behaviour that can be difficult to visualize. The following graphic shows a few examples of the effects that can be achieved with specific configuration values:

3.10.3.3.2. Examples

The key assignment K1 is configured such that [kaValueStart, kaValueEnd] = [60, 67], and [kaAtVelocityStart, kaAtVelocityEnd] = [0, 1]. This means keys [60, 67] will match it, and all possible velocity values will also match it. K1 has [kaAmplitudeAtKeyStart, kaAmplitudeAtKeyEnd] = [1, 1], which means that the key amplitude is always 1 and doesn't differ based on which key is pressed. It has [kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityCenter] = [0, 1], and [kaAmplitudeAtVelocityCenter, kaAmplitudeAtVelocityEnd] = [1, 0]. This, oddly, means that when a key is pressed at half velocity, the resulting amplitude will be 1. When a key is pressed above half velocity, the resulting amplitude values will trend downwards towards 0. Similarly, when a key is pressed below half velocity, the amplitude values will also trend downwards towards 0. In isolation, this would seem to be of questionable utility, however it becomes useful when considering multiple clips assigned to the same key range; velocity values can be used to blend between different clips to affect the resulting timbre.

The key assignment K2 is configured such that [kaValueStart, kaValueEnd] = [65, 71], and [kaAtVelocityStart, kaAtVelocityEnd] = [0, 0.4]. This means keys [60, 67] will match it, but only velocity values up to and including 0.4 will match it. K2 has [kaAmplitudeAtKeyStart, kaAmplitudeAtKeyEnd] = [1, 1], which means that the key amplitude is always 1 and doesn't differ based on which key is pressed. It has [kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityCenter] = [0, 0.5], and [kaAmplitudeAtVelocityCenter, kaAmplitudeAtVelocityEnd] = [0.5, 1]. This means that when a key is pressed at anything between velocity [0, 0.4], the resulting amplitude will be in the range [0, 1]. At any velocity value over 0.4, however, the key assignment will no longer match. This configuration can be used to produce hard steps between clips assigned to the same keys without any soft interpolation. Note that K2 and K1 have overlapping key ranges, so some combinations of key and velocity will match both and therefore result in evaluating two clips. This is an intended and useful effect that can be used to smoothly vary the timbre of instruments by blending between clips based on the incoming key value.

The key assignment K3 is configured such that [kaValueStart, kaValueEnd] = [72, 77], and [kaAtVelocityStart, kaAtVelocityEnd] = [0, 1]. This means keys [72, 77] will match it, and all possible velocity values will also match it. K3 has [kaAmplitudeAtKeyStart, kaAmplitudeAtKeyEnd] = [1, 1], which means that the key amplitude is always 1 and doesn't differ based on which key is pressed. It has [kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityEnd] = [1, 1] which means that the resulting velocity amplitude is always 1.

The key assignment K4 is configured such that [kaValueStart, kaValueEnd] = [77, 82], and [kaAtVelocityStart, kaAtVelocityEnd] = [0, 1]. This means keys [72, 77] will match it, and all possible velocity values will also match it. K3 has [kaAmplitudeAtKeyStart, kaAmplitudeAtKeyCenter] = [0, 1] and [kaAmplitudeAtKeyCenter, kaAmplitudeAtKeyEnd] = [1, 0], which means that the key amplitude is rises towards 1 the closer the incoming key is to kaValueCenter.

The key assignment K5 is configured such that [kaValueStart, kaValueEnd] = [77, 82], and [kaAtVelocityStart, kaAtVelocityEnd] = [0, 1]. K4 has [kaAmplitudeAtKeyStart, kaAmplitudeAtKeyCenter] = [0, 1] and [kaAmplitudeAtKeyCenter, kaAmplitudeAtKeyEnd] = [1, 0], which means that the key amplitude varies in the same manner as K4. It has It has [kaAmplitudeAtVelocityStart, kaAmplitudeAtVelocityCenter] = [0, 1] and [kaAmplitudeAtVelocityCenter, kaAmplitudeAtVelocityEnd] = [1, 0], which means that the velocity amplitude varies in the same manner as K1. Essentially, the resulting amplitude is only at full amplitude when the velocity is 0.5, and the key is 85.

3.10.3.4. Lists

The set of key assignments in an aurantium file are contained within a single list.

3.10.3.4.2. Key Assignment List

Inductive keyAssignments : Set := {
  kasList       : list keyAssignment;
  kasListSorted : keyAssignmentListIsSorted kasList
}.

The keyAssignmentListIsSorted proposition indicates that the list of key assignments must be provided in ascending order of their identifiers:

3.10.3.4.4. Key Assignment List Sorted

Inductive keyAssignmentListIsSorted : list keyAssignment -> Prop :=
  | kaListNone : keyAssignmentListIsSorted []
  | kaListOne : forall s, keyAssignmentListIsSorted [s]
  | kaListCons : forall s0 s1 s,
    lt (kaId s0) (kaId s1) ->
      keyAssignmentListIsSorted (s0 :: s) ->
        keyAssignmentListIsSorted (s1 :: s0 :: s).

A key assignment with a given ID is located using the keyAssignmentForId function:

3.10.3.4.6. keyAssignmentForId

Fixpoint keyAssignmentForId
  (i  : nat)
  (ka : list keyAssignment)
: option keyAssignment :=
  match ka with
  | nil         => None
  | cons a rest =>
    match Nat.eq_dec (kaId a) i with
    | left _  => Some a
    | right _ => keyAssignmentForId i rest
    end
  end.

3.10.4. Compatibility

3.10.4.1. Overview

This section enumerates all of the possible changes that can be made to a set of key assignments, and describes whether each of the changes is a compatibility-breaking major change, or a minor change.

The complete procedure for determining the compatibility of changes to a list of key assignments is given by the keyAssignmentsCompatCompareFull:

3.10.4.1.3. keyAssignmentsCompatCompareFull

Definition keyAssignmentsCompatCompareFull
  (ka kb : list keyAssignment)
: list compatVersionChangeRecord :=
  let f              := (fun k ks => keyAssignmentForId (kaId k) ks) in
  let removed        := keyAssignmentsRemoved ka kb in
  let added          := keyAssignmentsAdded ka kb in
  let changed        := intersectionPairs f ka kb in
  let removedChanges := keyAssignmentsCompatCompareRemoved removed in
  let addedChanges   := keyAssignmentsCompatCompareAdded added kb in
  let changedChanges := keyAssignmentsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

This function composes the results of many compatibility checks, and returns a list of all of the changes. The definitions given in the compatibility module can then be used to determine the maximally significant change in the list of changes.

3.10.4.2. Removing A Key Assignment

Removing an existing key assignment is a major change. If a piece of music is written using version M of an audio map, and a key assignment is removed from that map, some keys triggered by the music may either sound different (due to fewer key assignments matching), or may now contain notes that do not match any key assignments (effectively resulting in silence).

The keyAssignmentsRemoved function determines the set of key assignments that were present in the old version of a key assignment list, but that are not present in the new one:

3.10.4.2.3. keyAssignmentsRemoved

Fixpoint keyAssignmentsRemoved
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  match ka with
  | nil => []
  | cons a rest =>
    match keyAssignmentForId (kaId a) kb with
    | None   => cons a (keyAssignmentsRemoved rest kb)
    | Some _ => keyAssignmentsRemoved rest kb
    end
  end.

It follows that if the list of removed elements is non-empty, then the keyAssignmentsCompatCompare returns at least one major change:

3.10.4.2.5. keyAssignmentsRemoved Major

Theorem keyAssignmentsCompatCompareMajor0 : forall ka kb,
  [] <> keyAssignmentsRemoved ka kb ->
    compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
      = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.4.3. Adding A Key Assignment

Adding a new key assignment is a major change if the new key assignment overlaps with an existing assignment. If the key assignment does not overlap, then adding it is a minor change. The assumption is that music written against the older version of the audio map will not have been sending key events to nonexistent key assignments.

Two key assignments are said to overlap if their key ranges overlap according to the following proposition:

3.10.4.3.3. Overlaps

Definition keyAssignmentsOverlap (x y : keyAssignment) : Prop :=
  let x1 := kaValueStart x in
  let x2 := kaValueEnd x in
  let y1 := kaValueStart y in
  let y2 := kaValueEnd y in
    ge x2 y1 /\ ge y2 x1.

Overlapping is reflexive, commutative, and decidable:

3.10.4.3.5. Overlaps (Reflexive)

Theorem keyAssignmentsOverlapReflexive : forall x,
  keyAssignmentsOverlap x x.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.4.3.6. Overlaps (Commutative)

Theorem keyAssignmentsOverlapCommutative : forall x y,
  keyAssignmentsOverlap x y -> keyAssignmentsOverlap y x.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.4.3.7. Overlaps (Decidable)

Theorem keyAssignmentsOverlapDecidable : forall x y,
  {keyAssignmentsOverlap x y}+{~keyAssignmentsOverlap x y}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

The list of key assignments that overlap a key assignment k are determined using the keyAssignmentsOverlapping function:

3.10.4.3.9. Key Assignment Overlapping

Definition keyAssignmentsOverlapping
  (k  : keyAssignment)
  (ka : list keyAssignment)
: list keyAssignment :=
  filter (fun j =>
    match keyAssignmentsOverlapDecidable k j with
    | left _ =>
      match Nat.eq_dec (kaId k) (kaId j) with
      | left _  => false
      | right _ => true
      end
    | right _ => false
    end) ka.

The keyAssignmentsOverlapping function never returns k, and correctly finds all assignments:

3.10.4.3.11. Key Assignment Overlapping (No self)

Theorem keyAssignmentsOverlappingNotSelf : forall k ka,
  ~In k (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.4.3.12. Key Assignment Overlapping (Find 0)

Theorem keyAssignmentsOverlappingFind0 : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    -> In p (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.4.3.13. Key Assignment Overlapping (Find 0)

Theorem keyAssignmentsOverlappingFind1 : forall k ka p,
  In p (keyAssignmentsOverlapping k ka) ->
    In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.4.3.14. Key Assignment Overlapping (Find <-> Find)

Theorem keyAssignmentsOverlappingFind : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    <-> In p (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

The set of key assignments that have been added can be expressed in terms of the keyAssignmentsRemoved function with the arguments applied in reverse order. Intuitively, if ka is the set of old assignments, and kb is the set of new assignments, the keyAssignmentsRemoved states which elements of kb must be removed to produce ka; this is the set of newly added assignments.

3.10.4.3.16. Key Assignments Added

Definition keyAssignmentsAdded
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  keyAssignmentsRemoved kb ka.

The keyAssignmentsCompatCompareAdd describes how an added overlapping key assignment yields a major change:

3.10.4.3.18. Key Assignments Added Major

Definition keyAssignmentsCompatCompareAdd
  (k  : keyAssignment)
  (ka : list keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentsOverlapping k ka with
  | nil => CVRMake CVersionChangeMinor "A key assignment was added."
  | _   => CVRMake CVersionChangeMajor "A key assignment was added that overlaps with an existing assignment."
  end.

3.10.4.3.19. Key Assignments Added Major (Theorem)

Theorem keyAssignmentsCompatCompareMajor1 : forall ka kb k,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      In k (keyAssignmentsAdded ka kb) ->
        [] <> (keyAssignmentsOverlapping k kb) ->
        compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
          = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Adding a non-overlapping key assignment is a minor change:

3.10.4.3.21. Key Assignments Added Minor (Theorem)

Theorem keyAssignmentsCompatCompareMinor0 : forall ka kb,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      [] <> (keyAssignmentsAdded ka kb) ->
        Forall (fun j => [] = keyAssignmentsOverlapping j kb) (keyAssignmentsAdded ka kb) ->
          compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
           = CVersionChangeMinor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

3.10.4.4. Changing A Key Assignment

Changing an existing key assignment is a major change.

If ka is the set of old assignments, and kb is the set of new assignments, the intersectionPairs function determines which key assignments are in both sets.

A key assignment k is considered to be equal to a key assignment j iff all the values in the assignments are equal:

3.10.4.4.4. Equality

Definition keyAssignmentValuesEq (x y : keyAssignment) : Prop :=
     (kaId x)                        = (kaId y)
  /\ (kaValueStart x)                = (kaValueStart y)
  /\ (kaValueCenter x)               = (kaValueCenter y)
  /\ (kaValueEnd x)                  = (kaValueEnd y)
  /\ (kaClipId x)                    = (kaClipId y)
  /\ (kaAmplitudeAtKeyStart x)       = (kaAmplitudeAtKeyStart y)
  /\ (kaAmplitudeAtKeyCenter x)      = (kaAmplitudeAtKeyCenter y)
  /\ (kaAmplitudeAtKeyEnd x)         = (kaAmplitudeAtKeyEnd y)
  /\ (kaAtVelocityStart x)           = (kaAtVelocityStart y)
  /\ (kaAtVelocityCenter x)          = (kaAtVelocityCenter y)
  /\ (kaAtVelocityEnd x)             = (kaAtVelocityEnd y)
  /\ (kaAmplitudeAtVelocityStart x)  = (kaAmplitudeAtVelocityStart y)
  /\ (kaAmplitudeAtVelocityCenter x) = (kaAmplitudeAtVelocityCenter y)
  /\ (kaAmplitudeAtVelocityEnd x)    = (kaAmplitudeAtVelocityEnd y)
  /\ (kaFlags x)                     = (kaFlags y)
.

Determining the equality is decidable:

3.10.4.4.6. Equality Decidable

Theorem keyAssignmentValuesEqDec
  (x y : keyAssignment)
: {keyAssignmentValuesEq x y}+{~keyAssignmentValuesEq x y}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Key assignments are compared using this comparison function:

3.10.4.4.8. Key Assignment Compare

Definition keyAssignmentCompatCompare
  (k0 k1 : keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentValuesEqDec k0 k1 with
  | left _ =>
    CVRMake CVersionChangeNone ""
  | right _ =>
    CVRMake CVersionChangeMajor "The values of the key assignment were changed."
  end.

3.10.4.4.9. Key Assignment Compare Changed

Definition keyAssignmentsCompatCompareChanged
  (r : list (keyAssignment * keyAssignment))
: list compatVersionChangeRecord :=
  map (fun p => keyAssignmentCompatCompare (fst p) (snd p)) r.

3.11. Audio Map

3.11.1. Overview

3.11.2. Key/Clip References

3.11.3. Audio Map

3.11.1. Overview

An audio map is the top-level data structure that aggregates all of the various model values together. In practical terms, aurantium files contain exactly one audio map.

3.11.2. Key/Clip References

A key assignment k references a clip c if k's clip field equals c.

3.11.2.2. Key/Clip References

Definition keyAssignmentReferencesClip
  (k : keyAssignment)
  (s : clip)
: Prop :=
  (kaClipId k) = (clipId s).

A key assignment k's reference to a clip is valid if the clip appears in the list of clips s:

3.11.2.4. Key/Clip Reference Exists

Definition keyAssignmentReferencesExists
  (k : keyAssignment)
  (s : clips)
: Prop :=
  exists p, keyAssignmentReferencesClip k p /\ In p (clipsList s).

A proposition that states that all key assignments in a list have valid references to clips:

3.11.2.6. Key/Clip Reference Forall

Definition keyAssignmentsReferences
  (k : keyAssignments)
  (s : clips)
: Prop :=
  forall p, In p (kasList k) -> keyAssignmentReferencesExists p s.

A proposition that states that all clips in a list have at least one reference:

3.11.2.8. Clips Referenced

Definition clipsReferenced
  (k  : keyAssignments)
  (ss : clips)
: Prop :=
  Forall (fun s => exists a, keyAssignmentReferencesClip a s /\ In s (clipsList ss)) (clipsList ss).

3.11.3. Audio Map

The audioMap type aggregates a list of clips, a list of key assignments, and a set of proofs asserting the validity of the references within:

3.11.3.2. Audio Map

Inductive audioMap : Set := {
  amIdentifier               : identifier;
  amClips                    : clips;
  amKeyAssignments           : keyAssignments;
  amKeyAssignmentsReferences : keyAssignmentsReferences amKeyAssignments amClips;
  amClipsReferenced          : clipsReferenced amKeyAssignments amClips;
}.

The amIdentifier field is the identifier for the audio map.

The amClips field is the list of clips for the audio map.

The amKeyAssignments field is the list of clips for the audio map.

All key assignments in an audio map must reference clips that exist in the map. The amKeyAssignmentsReferences field is a proof that all of the key assignments in amKeyAssignments reference existing clips in amClips.

All clips in an audio map must have at least one reference by a key assignment. The amClipsReferenced field is a proof that all of the clips in amClips have at least one key assignment in amKeyAssignments. This ensures that audio maps do not contain redundant audio data.

3.12. Metadata

An audio map file can have associated free-form metadata. This is often used to, for example, express authorship information and indicate which tools were used to produce a given file. The metadata supported directly by aurantium is in the form of UTF-8 encoded keys and values. Metadata that requires more structure than this can be provided by custom sections that will be ignored by software that does not know how to interpret them.

3.12.2. Metadata Value

Inductive metadataValue : Set := MetadataValue {
  mKey   : string;
  mValue : string
}.

3.12.3. Metadata

Inductive metadata : Set := Metadata {
  mValues : list metadataValue
}.

Conceptually, metadata is structured as a function from keys to non-empty lists of values; the values associated with multiple occurrences of a given key are expected to be combined into a list of values for the given key by consumers.

As metadata is purely informative, adding and/or removing metadata values does not affect compatibility. Applications MUST NOT change their behaviour based on the presence (or lack thereof) of particular metadata values.

4. The Aurantium Binary Encoding

4.1. Binary Expressions

4.1.1. Overview

4.1.2. Expressions

4.2. JSON Expressions

4.2.1. Overview

4.2.2. Expressions

4.2.3. Tokens

4.2.4. Token (Strings)

4.2.5. Serialization

4.2.6. Expression -> String

4.2.7. Clips

4.2.8. Key Assignments

4.2.9. Metadata

4.2.10. Schema

4.3. File Header

4.4. Sections

4.5. Identifier

4.5.1. Description

4.5.2. Cardinality

4.6. Clip Descriptions

4.6.1. Description

4.6.2. Cardinality

4.7. Clip Data

4.7.1. Description

4.7.2. Cardinality

4.8. Key assignments

4.8.1. Description

4.8.2. Cardinality

4.9. Metadata

4.9.1. Description

4.9.2. Cardinality

4.10. End

4.10.1. Description

4.10.2. Cardinality

4.1. Binary Expressions

4.1.1. Overview

4.1.2. Expressions

4.1.1. Overview

The aurantium file format has a strict and easy-to-parse binary encoding, defined in terms of a small binary expression language. Terms in this binary expression language, when evaluated, produce streams of octets that are concatenated together to produce the final output file. This section of the specification defines the expression language, whilst subsequent sections describe how the semantic structures given in the model are mapped to binary expressions.

4.1.2. Expressions

A term in the binary expression language is described by the following inductive type:

4.1.2.2. Binary Expression

Inductive binaryExp : Set :=
    (** A 32-bit unsigned integer. *)
    | BiU32     : nat -> binaryExp
    (** A 64-bit unsigned integer. *)
    | BiU64     : nat -> binaryExp
    (** A 64-bit IEEE754 binary64 value. *)
    | BiF64     : R -> binaryExp
    (** A sequence of bytes. *)
    | BiBytes   : list byte -> binaryExp
    (** A sequence of bytes describing UTF-8 encoded text. *)
    | BiUTF8    : list byte -> binaryExp
    (** An array of binary expressions. *)
    | BiArray   : list binaryExp -> binaryExp
    (** A section of reserved space. *)
    | BiReserve : nat -> binaryExp
    (** A record with named binary expression members. *)
    | BiRecord  : list (string * binaryExp) -> binaryExp.

An expression BiU32 n represents an unsigned 32-bit integer n.

An expression BiU64 n represents an unsigned 64-bit integer n.

An expression BiF64 n represents a IEEE754 binary64 value n.

An expression BiBytes xs represents an octet array. Octet arrays are prefixed with an unsigned 32-bit integer value denoting their size in octets, not including any padding. Octet arrays are unconditionally padded with unsigned 8-bit values such that the total size of the array including padding is evenly divisible by 4.

An expression BiUTF8 xs represents a UTF-8 encoded string. Strings are prefixed with an unsigned 32-bit integer value denoting their encoded size in octets, not including any padding. Strings are unconditionally padded with unsigned 8-bit values such that the total size of the string including padding is evenly divisible by 4.

An expression BiArray xs represents an array of binary expressions xs. Arrays are prefixed with an unsigned 32-bit integer value denoting the number of array elements present.

An expression BiReserve n represents a block of reserved data of n octets in length. Data is unconditionally padded with unsigned 8-bit values such that the total size of the string including padding is evenly divisible by 4.

An expression BiRecord fs represents a sequence of named expression values. Intuitively, they can be considered to be fields of a record type. The number of fields is not present in the resulting encoded octet stream, and the names of fields are not included either. Consumers are expected to know, from reading this specification, when to expect a record type in a stream.

All of the possible forms of binary expression have an encoded size that is a multiple of 4. The sizes of each encoded expression form are given by binarySize:

4.1.2.12. Binary Expression Sizes

Fixpoint binarySize (b : binaryExp) : nat :=
  match b with
  | BiU32 _     => 4
  | BiU64 _     => 8
  | BiF64 _     => 8
  | BiBytes s   => 4 + asMultipleOf4 (length s)
  | BiUTF8 s    => 4 + asMultipleOf4 (length s)
  | BiArray f   => 4 + fold_right plus 0 (map binarySize f)
  | BiReserve s => asMultipleOf4 s
  | BiRecord f  => fold_right plus 0 (map (compose binarySize snd) f)
  end.

4.1.2.13. Binary Expression Sizes (multiple of)

Definition asMultipleOf (size q : nat) (Hnz : 0 <> q) : nat :=
  let r := size / q in
    match Nat.ltb_spec0 r q with
    | ReflectT _ _ => (r + 1) * q
    | ReflectF _ _ => r * q
    end.

4.1.2.14. Binary Expression Size Theorem

Theorem binarySizeMultiple4 : forall b, binarySize (b) mod 4 = 0.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.

This specification text makes use of a convenient abbreviation function, binarySizePadded16, to concisely denote the size of binary expressions padded to a size that is a multiple of 16, as well as a partial application of asMultipleOf fixed to a multiple of 4:

4.1.2.16. Binary Expression Size Padded 16

Definition binarySizePadded16 (b : binaryExp) : nat :=
  asMultipleOf16 (binarySize b).

4.1.2.17. asMultipleOf4

Definition asMultipleOf4 (size : nat) : nat :=
  asMultipleOf size 4 p0not4.

Binary expressions are encoded as streams of streamE values:

4.1.2.19. Stream Elements

Inductive streamE : Set :=
  (** A 64-bit IEEE754 binary64 value. *)
  | Vf64 : R -> streamE
  (** A 64-bit unsigned integer. *)
  | Vu64 : nat -> streamE
  (** A 32-bit unsigned integer. *)
  | Vu32 : nat -> streamE
  (** An 8-bit unsigned integer. *)
  | Vu8  : nat -> streamE.

An expression Vf64 n represents an IEEE754 binary64 value in big-endian order.

An expression Vu64 n represents an unsigned 64-bit integer in big-endian order.

An expression Vu32 n represents an unsigned 32-bit integer in big-endian order.

An expression Vu8 n represents an unsigned 8-bit integer.

A given binary expression is transformed to a stream of octets using the following encoding rules:

4.1.2.25. Binary Expression Encoding

Fixpoint binaryEval (b : binaryExp) : list streamE :=
  match b with
  | BiU32 k     => [Vu32 k]
  | BiU64 k     => [Vu64 k]
  | BiF64 k     => [Vf64 k]
  | BiBytes s   => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiUTF8 s    => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiArray f   => (Vu32 (length f)) :: concat (map binaryEval f)
  | BiReserve s => repeat (Vu8 0) (asMultipleOf4 s)
  | BiRecord f  => concat (map (compose binaryEval snd) f)
  end.

4.1.2.26. Binary Expression Encoding (Padding)

Definition binaryEvalPaddedBytes
  (b     : list byte)
  (align : nat)
  (Hneq  : 0 <> align)
: list streamE :=
  let vremaining := length b mod align in
    match vremaining with
    | 0 => map u8byte b
    | _ => map u8byte (b ++ repeat x00 (align - vremaining))
    end.

Informally, a stream s is well-formed if exactly one of the following conditions holds:

4.1.2.28. Well-Formed Stream (Informal rules)

s is empty.

s consists of a single IEEE754 binary64 value.

s consists of a single 64-bit integer.

s consists of a single 32-bit integer.

s consists of a sequence of n 8-bit integers, where n is evenly divisible by 4.

s is the concatenation of a well-formed stream t and a well-formed stream u.

The rules for well-formedness correspond to the following proposition:

4.1.2.30. Well-Formed Stream

Inductive streamWellFormed : list streamE -> Prop :=
  (** An empty stream is well-formed. *)
  | BEPEmpty  : streamWellFormed []
  (** A stream consisting of a single 64-bit float is well-formed. *)
  | BEPVf64   : forall k, streamWellFormed [Vf64 k]
  (** A stream consisting of a single 64-bit integer is well-formed. *)
  | BEPVu64   : forall k, streamWellFormed [Vu64 k]
  (** A stream consisting of a single 32-bit integer is well-formed. *)
  | BEPVu32   : forall k, streamWellFormed [Vu32 k]
  (** A stream consisting of a number of 8-bit values of a length divisible by 4 is well-formed. *)
  | BEPVu8s   : forall es, Forall streamEIsU8 es -> length (es) mod 4 = 0 -> streamWellFormed es
  (** The concatenation of two well-formed streams is well-formed. *)
  | BEPAppend : forall xs ys, streamWellFormed xs -> streamWellFormed ys -> streamWellFormed (xs ++ ys).

The binary expression encoding rules produce well-formed streams. It follows that any well-formed stream has a size that is evenly divisible by 4.

4.1.2.32. Binary Expression Encoding Well-Formed

Theorem binaryEvalStreamsWellFormed : forall b,
  streamWellFormed (binaryEval b).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.

4.1.2.33. Binary Expression Encoding Size Divisible

Theorem streamsWellFormedDivisible4 : forall es,
  streamWellFormed es -> streamSize es mod 4 = 0.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.

4.2. JSON Expressions

4.2.1. Overview

4.2.2. Expressions

4.2.3. Tokens

4.2.4. Token (Strings)

4.2.5. Serialization

4.2.6. Expression -> String

4.2.7. Clips

4.2.8. Key Assignments

4.2.9. Metadata

4.2.10. Schema

4.2.1. Overview

The aurantium binary encoding embeds JSON text into the file format for complex structured data. This section of the specification defines a formal model for JSON expressions, and describes how those expressions are converted to text.

4.2.2. Expressions

A JSON expression is a value of the json type:

4.2.2.2. JSON Expression

Inductive json : Set :=
  (** A boolean constant. *)
  | JsonBoolean : bool -> json
  (** An integer constant. *)
  | JsonInteger : nat -> json
  (** A floating point constant. *)
  | JsonFloat   : json
  (** A string constant. *)
  | JsonString  : string -> json
  (** An object. *)
  | JsonObject  : list (string * json) -> json
  (** An array. *)
  | JsonArray   : list json -> json
  .

An expression JsonBoolean b represents a boolean constant b.

An expression JsonInteger n represents an integer constant n.

An expression JsonFloat represents a floating-point constant [1].

An expression JsonString s represents a string constant s.

An expression JsonObject o represents a JSON object with properties o.

An expression JsonArray a represents a JSON array with values a.

4.2.3. Tokens

In order to serialize a JSON expression , we convert the expression to a sequence of JSON tokens. A JSON token is a value of type jsonToken:

4.2.3.2. JSON Token

Inductive jsonToken : Set :=
  | JTTrue        : jsonToken
  | JTFalse       : jsonToken
  | JTInteger     : nat -> jsonToken
  | JTFloat       : jsonToken
  | JTString      : string -> jsonToken
  | JTObjectStart : jsonToken
  | JTObjectEnd   : jsonToken
  | JTColon       : jsonToken
  | JTComma       : jsonToken
  | JTArrayStart  : jsonToken
  | JTArrayEnd    : jsonToken
  .

An expression JTTrue represents a boolean constant true.

An expression JTFalse represents a boolean constant false .

An expression JTInteger n represents an integer constant n.

An expression JTFloat represents a floating point constant [1].

An expression JTString s represents a string constant s.

An expression JTObjectStart represents a character constant { U+007B.

An expression JTObjectEnd represents a character constant } U+007D.

An expression JTColon represents a character constant : U+003A.

An expression JTComma represents a character constant , U+002C.

An expression JTArrayStart represents a character constant [ U+005B.

An expression JTArrayEnd represents a character constant ] U+005D.

4.2.4. Token (Strings)

A token is converted to a string via the jsonStringOne function:

4.2.4.2. JSON Token String

Definition jsonStringOne (t : jsonToken) : string :=
  match t with
  | JTTrue        => "true"
  | JTFalse       => "false"
  | JTInteger n   => string_of_nat n
  | JTFloat       => "#"
  | JTString s    => """" ++ s ++ """"
  | JTObjectStart => "{"
  | JTObjectEnd   => "}"
  | JTColon       => ":"
  | JTComma       => ","
  | JTArrayStart  => "["
  | JTArrayEnd    => "]"
  end.

4.2.5. Serialization

Given a JSON expression j, we can serialize j to a sequence of JSON tokens by evaluating jsonSerialize j, defined as:

4.2.5.2. JSON Serialize

Fixpoint jsonSerialize (j : json) : list jsonToken :=
  match j with
  | JsonBoolean true  => [JTTrue]
  | JsonBoolean false => [JTFalse]
  | JsonInteger n     => [JTInteger n]
  | JsonFloat         => [JTFloat]
  | JsonString s      => [JTString s]
  | JsonObject o      =>
    let props := map (fun p => JTString (fst p) :: JTColon :: jsonSerialize (snd p)) o in
      JTObjectStart :: (jsonComma props) ++ [JTObjectEnd]
  | JsonArray a       =>
    let values := map jsonSerialize a in
      JTArrayStart :: (jsonComma values) ++ [JTArrayEnd]
  end.

The jsonComma function is defined as:

4.2.5.4. JSON Comma

Fixpoint jsonComma (ss : list (list jsonToken)) : list jsonToken :=
  match ss with
  | []        => []
  | (x :: []) => x
  | (x :: xs) => x ++ JTComma :: (jsonComma xs)
  end.

4.2.6. Expression -> String

Given an initial JSON expression , the full serialization process to convert the expression to text is defined as the jsonSerializeString function:

4.2.6.2. JSON Serialize

Definition jsonSerializeString (j : json) : string :=
  let tokens := jsonSerialize j in
  let texts  := map jsonStringOne tokens in
    fold_left append texts "".

4.2.7. Clips

A clip is serialized to a JSON expression as follows:

4.2.7.2. Clips (JSON)

Definition jsonClip (c : clip) : json :=
  JsonObject (app [
    ("ID",           JsonInteger (clipId c));
    ("Name",         JsonString (clipName c));
    ("Format",       JsonString (audioFormatDescribe (clipFormat c)));
    ("SampleRate",   JsonInteger (clipSampleRate c));
    ("SampleDepth",  JsonInteger (clipSampleDepth c));
    ("Channels",     JsonInteger (clipChannels c));
    ("Endianness",   JsonString (octetOrderDescribe (clipEndianness c)));
    ("Hash",         jsonHash (clipHash c));
    ("Offset",       JsonInteger (clipOffset c));
    ("Size",         JsonInteger (clipSize c))
  ] (jsonLoopRangeOptionProperty (clipLoopRange c))).

A loop range is serialized to a JSON expression as follows:

4.2.7.4. Clips (Loop Range [Optional])

Definition jsonLoopRangeOptionProperty (lr : option loopRange) : list (string * json) :=
  match lr with
  | Some l => [("LoopRange", jsonLoopRange l)]
  | None   => []
  end.

4.2.7.5. Clips (Loop Range)

Definition jsonLoopRange (lr : loopRange) : json :=
  JsonObject [
    ("FrameStart",        JsonInteger (lrFrameStart lr));
    ("FrameEndInclusive", JsonInteger (lrFrameEndInclusive lr))
  ].

A hash value is serialized to a JSON expression as follows:

4.2.7.7. Clips (Hash)

Definition jsonHash (h : hashValue) : json :=
  JsonObject [
    ("Algorithm", JsonString (hashAlgorithmDescribe (hvAlgorithm h)));
    ("Value",     JsonString (hvValue h))
  ].

The top-level object that contains the full set of clips is serialized to a JSON expression as follows:

4.2.7.9. Clips (Container)

Definition jsonClips (c : list clip) : json :=
  JsonObject [
    ("%Schema", JsonString "urn:com.io7m.aurantium:1.0");
    ("Clips",   JsonArray (map jsonClip c))
  ].

4.2.8. Key Assignments

A key assignment is serialized to a JSON expression as follows:

4.2.8.2. Key Assignments (JSON)

Definition jsonKeyAssignment (k : keyAssignment) : json :=
  JsonObject [
    ("ID",                        JsonInteger (kaId k));
    ("KeyValueStart",             JsonInteger (kaValueStart k));
    ("KeyValueCenter",            JsonInteger (kaValueCenter k));
    ("KeyValueEnd",               JsonInteger (kaValueEnd k));
    ("ClipID",                    JsonInteger (kaClipId k));
    ("AmplitudeAtKeyStart",       float (kaAmplitudeAtKeyStart k));
    ("AmplitudeAtKeyCenter",      float (kaAmplitudeAtKeyCenter k));
    ("AmplitudeAtKeyEnd",         float (kaAmplitudeAtKeyEnd k));
    ("AtVelocityStart",           float (kaAtVelocityStart k));
    ("AtVelocityCenter",          float (kaAtVelocityCenter k));
    ("AtVelocityEnd",             float (kaAtVelocityEnd k));
    ("AmplitudeAtVelocityStart",  float (kaAmplitudeAtVelocityStart k));
    ("AmplitudeAtVelocityCenter", float (kaAmplitudeAtVelocityCenter k));
    ("AmplitudeAtVelocityEnd",    float (kaAmplitudeAtVelocityEnd k));
    ("Flags",                     JsonArray (map flagJson (kaFlags k)))
  ].

4.2.8.3. Key Assignments (Flags)

Definition flagJson (f : keyAssignmentFlag) : json :=
  JsonString (keyAssignmentFlagDescribe f).

The top-level object that contains the full set of key assignments is serialized to a JSON expression as follows:

4.2.8.5. Key Assignments (Container)

Definition jsonKeyAssignments (ks : list keyAssignment) : json :=
  JsonObject [
    ("%Schema", JsonString "urn:com.io7m.aurantium:1.0");
    ("Clips",   JsonArray (map jsonKeyAssignment ks))
  ].

4.2.9. Metadata

Metadata is serialized to a JSON expression as follows:

4.2.9.2. Metadata (JSON)

Definition jsonMetadataM (mvs : list metadataValue) : json :=
  JsonObject (map (fun k => (mKey k, JsonString (mValue k))) mvs).

The top-level object that contains the full set of metadata is serialized to a JSON expression as follows:

4.2.9.4. Metadata (Container)

Definition jsonMetadata (m : metadata) : json :=
  JsonObject [
    ("%Schema",  JsonString "urn:com.io7m.aurantium:1.0");
    ("Metadata", jsonMetadataM (mValues m))
  ].

4.2.10. Schema

The serialized objects described in this section will conform to the following JSON schema:

4.2.10.2. Schema

{
  "$schema" : "https://json-schema.org/draft/2020-12/schema",
  "$id" : "urn:com.io7m.aurantium:1.0",
  "title" : "Aurantium 1.0",
  "oneOf" : [ {
    "$ref" : "#/$defs/AU1SchemaObjectType"
  } ],
  "$defs" : {
    "AU1ClipDescription" : {
      "type" : "object",
      "properties" : {
        "Channels" : {
          "description" : "The clip channel count.",
          "$ref" : "#/$defs/BigInteger"
        },
        "Endianness" : {
          "description" : "The clip endianness.",
          "$ref" : "#/$defs/RDottedName"
        },
        "Format" : {
          "description" : "The clip format.",
          "$ref" : "#/$defs/RDottedName"
        },
        "Hash" : {
          "description" : "The clip hash value.",
          "$ref" : "#/$defs/AU1HashValue"
        },
        "ID" : {
          "description" : "The clip ID.",
          "$ref" : "#/$defs/BigInteger"
        },
        "LoopRange" : {
          "description" : "The clip loop range.",
          "$ref" : "#/$defs/Optional<AU1ClipLoopRange>"
        },
        "Name" : {
          "description" : "The clip name.",
          "$ref" : "#/$defs/String"
        },
        "Offset" : {
          "description" : "The clip audio data offset.",
          "$ref" : "#/$defs/BigInteger"
        },
        "SampleDepth" : {
          "description" : "The clip sample depth.",
          "$ref" : "#/$defs/BigInteger"
        },
        "SampleRate" : {
          "description" : "The clip sample rate.",
          "$ref" : "#/$defs/BigInteger"
        },
        "Size" : {
          "description" : "The clip audio data size.",
          "$ref" : "#/$defs/BigInteger"
        }
      },
      "required" : [ "Channels", "Endianness", "Format", "Hash", "ID", "Name", "Offset", "SampleDepth", "SampleRate", "Size" ],
      "additionalProperties" : false
    },
    "AU1ClipDescriptions" : {
      "type" : "object",
      "properties" : {
        "%Schema" : {
          "description" : "The schema identifier.",
          "$ref" : "#/$defs/String"
        },
        "Clips" : {
          "description" : "The clips.",
          "$ref" : "#/$defs/List<AU1ClipDescription>"
        }
      },
      "required" : [ "%Schema" ],
      "additionalProperties" : false
    },
    "AU1ClipLoopRange" : {
      "type" : "object",
      "properties" : {
        "FrameEndInclusive" : {
          "description" : "The end of the loop range in frames (inclusive).",
          "$ref" : "#/$defs/BigInteger"
        },
        "FrameStart" : {
          "description" : "The start of the loop range in frames.",
          "$ref" : "#/$defs/BigInteger"
        }
      },
      "required" : [ "FrameEndInclusive", "FrameStart" ],
      "additionalProperties" : false
    },
    "AU1HashString" : {
      "type" : "string",
      "description" : "A hexadecimal hash string.",
      "pattern" : "[a-f0-9]+"
    },
    "AU1HashValue" : {
      "type" : "object",
      "properties" : {
        "Algorithm" : {
          "description" : "The hash algorithm.",
          "$ref" : "#/$defs/RDottedName"
        },
        "Value" : {
          "description" : "The hash value.",
          "$ref" : "#/$defs/AU1HashString"
        }
      },
      "required" : [ "Algorithm", "Value" ],
      "additionalProperties" : false
    },
    "AU1KeyAssignment" : {
      "type" : "object",
      "properties" : {
        "AmplitudeAtKeyCenter" : {
          "description" : "The amplitude at the center key.",
          "$ref" : "#/$defs/double"
        },
        "AmplitudeAtKeyEnd" : {
          "description" : "The amplitude at the end key.",
          "$ref" : "#/$defs/double"
        },
        "AmplitudeAtKeyStart" : {
          "description" : "The amplitude at the starting key.",
          "$ref" : "#/$defs/double"
        },
        "AmplitudeAtVelocityCenter" : {
          "description" : "The amplitude at the center velocity.",
          "$ref" : "#/$defs/double"
        },
        "AmplitudeAtVelocityEnd" : {
          "description" : "The amplitude at the end velocity.",
          "$ref" : "#/$defs/double"
        },
        "AmplitudeAtVelocityStart" : {
          "description" : "The amplitude at the starting velocity.",
          "$ref" : "#/$defs/double"
        },
        "AtVelocityCenter" : {
          "description" : "The center velocity.",
          "$ref" : "#/$defs/double"
        },
        "AtVelocityEnd" : {
          "description" : "The end velocity.",
          "$ref" : "#/$defs/double"
        },
        "AtVelocityStart" : {
          "description" : "The starting velocity.",
          "$ref" : "#/$defs/double"
        },
        "ClipID" : {
          "description" : "The clip ID.",
          "$ref" : "#/$defs/BigInteger"
        },
        "Flags" : {
          "description" : "The flags.",
          "$ref" : "#/$defs/SortedSet<String>"
        },
        "ID" : {
          "description" : "The key assignment ID.",
          "$ref" : "#/$defs/BigInteger"
        },
        "KeyValueCenter" : {
          "description" : "The center key value.",
          "$ref" : "#/$defs/BigInteger"
        },
        "KeyValueEnd" : {
          "description" : "The end key value.",
          "$ref" : "#/$defs/BigInteger"
        },
        "KeyValueStart" : {
          "description" : "The starting key value.",
          "$ref" : "#/$defs/BigInteger"
        }
      },
      "required" : [ "AmplitudeAtKeyCenter", "AmplitudeAtKeyEnd", "AmplitudeAtKeyStart", "AmplitudeAtVelocityCenter", "AmplitudeAtVelocityEnd", "AmplitudeAtVelocityStart", "AtVelocityCenter", "AtVelocityEnd", "AtVelocityStart", "ClipID", "Flags", "ID", "KeyValueCenter", "KeyValueEnd", "KeyValueStart" ],
      "additionalProperties" : false
    },
    "AU1KeyAssignments" : {
      "type" : "object",
      "properties" : {
        "%Schema" : {
          "description" : "The schema identifier.",
          "$ref" : "#/$defs/String"
        },
        "KeyAssignments" : {
          "description" : "The key assignments.",
          "$ref" : "#/$defs/List<AU1KeyAssignment>"
        }
      },
      "required" : [ "%Schema" ],
      "additionalProperties" : false
    },
    "AU1Metadata" : {
      "type" : "object",
      "properties" : {
        "%Schema" : {
          "description" : "The schema identifier.",
          "$ref" : "#/$defs/String"
        },
        "Metadata" : {
          "description" : "The metadata values.",
          "$ref" : "#/$defs/SortedMap<String,List<String>>"
        }
      },
      "required" : [ "%Schema" ],
      "additionalProperties" : false
    },
    "AU1SchemaObjectType" : {
      "oneOf" : [ {
        "$ref" : "#/$defs/AU1ClipDescription"
      }, {
        "$ref" : "#/$defs/AU1ClipDescriptions"
      }, {
        "$ref" : "#/$defs/AU1ClipLoopRange"
      }, {
        "$ref" : "#/$defs/AU1HashString"
      }, {
        "$ref" : "#/$defs/AU1HashValue"
      }, {
        "$ref" : "#/$defs/AU1KeyAssignment"
      }, {
        "$ref" : "#/$defs/AU1KeyAssignments"
      }, {
        "$ref" : "#/$defs/AU1Metadata"
      } ]
    },
    "BigInteger" : {
      "type" : "integer",
      "description" : "An unsigned integer.",
      "minimum" : 0,
      "exclusiveMaximum" : 18446744073709551616
    },
    "List<AU1ClipDescription>" : {
      "type" : "array",
      "items" : {
        "$ref" : "#/$defs/AU1ClipDescription"
      }
    },
    "List<AU1KeyAssignment>" : {
      "type" : "array",
      "items" : {
        "$ref" : "#/$defs/AU1KeyAssignment"
      }
    },
    "List<String>" : {
      "type" : "array",
      "items" : {
        "$ref" : "#/$defs/String"
      }
    },
    "OffsetDateTime" : {
      "description" : "An ISO 8601 timestamp.",
      "type" : "string",
      "format" : "date-time"
    },
    "Optional<AU1ClipLoopRange>" : {
      "$ref" : "#/$defs/AU1ClipLoopRange"
    },
    "RDottedName" : {
      "type" : "string",
      "description" : "A Lanark dotted name.",
      "pattern" : "([a-z][a-z0-9_-]{0,63})(\\.[a-z][a-z0-9_-]{0,62}){0,15}"
    },
    "SortedMap<String,List<String>>" : {
      "type" : "object",
      "additionalProperties" : {
        "$ref" : "#/$defs/List<String>"
      }
    },
    "SortedSet<String>" : {
      "type" : "array",
      "items" : {
        "$ref" : "#/$defs/String"
      }
    },
    "String" : {
      "type" : "string"
    },
    "double" : {
      "type" : "number",
      "description" : "A normalized floating point value.",
      "minimum" : 0,
      "maximum" : 1
    }
  }
}

Footnotes

1

Please note that, due to limitations in the specification language and libraries, we currently cannot express actual floating point values. We therefore substitute a single JsonFloat value in the specification to conceptually represent the full set of values expressible as IEEE754 binary64 values.

References to this footnote: 1²

4.3. File Header

All aurantium audio map files begin with the following fixed length header:

4.3.2. File Header

Definition binaryExpFileHeader : binaryExp :=
  BiRecord [
    ("id",           u64 0x894155520D0A1A0A);
    ("versionMajor", u32 1);
    ("versionMinor", u32 0)
  ].

The id field must always be set to the 64-bit unsigned big-endian value 0x894155520D0A1A0A.

The versionMajor field must be set to 1 for files targeting this version of the specification.

The versionMinor field must be set to 0 for files targeting this version of the specification.

The media/MIME type for aurantium audio map files is application/vnd.com.io7m.aurantium.sample_map.

4.4. Sections

aurantium audio map files are structured as a sequence of explicitly sized sections. A section consists of a 64-bit identifier i, a 64-bit size value s, followed by s octets of data, followed by zero or more octets of padding such that the next section will begin on a 16 octet boundary. Consumers that do not recognize the identifier of a given section can simply skip the section by seeking forwards by s octets to find the next section.

aurantium audio map files must end with exactly one End section.

Sections must start at offsets that are evenly divisible by 16.

The following standard sections are defined by this version of the specification:

4.4.5. Standard Sections

Identifier | Description
0x4155524D5F494421 | Identifier.
0x4155524D43444553 | Clip descriptions.
0x4155524D434C4950 | Clip data.
0X4155524D4B455953 | Key assignments.
0x4155524D4D455441 | Metadata.
0x4155524D454E4421 | File terminator.

4.5. Identifier

4.5.1. Description

4.5.2. Cardinality

4.5.1. Description

aurantium audio map files must begin with exactly one Identifier section, which has the identifier 0x4155524D5F494421.

Identifiers are encoded as follows:

4.5.1.3. Identifier Encoding

Definition binaryIdentifier (i : identifier) : binaryExp :=
  BiRecord [
    ("group",        utf8 (idGroup i));
    ("name",         utf8 (idName i));
    ("versionMajor", u32 (idVersionMajor i));
    ("versionMinor", u32 (idVersionMinor i))
  ].

Identifier sections are encoded as follows:

4.5.1.5. Identifier Section Encoding

Definition binaryIdentifierSection (i : identifier) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D5F494421);
    ("size", u64 (binarySizePadded16 (binaryIdentifier i)));
    ("data", binaryIdentifier i)
  ].

4.5.2. Cardinality

An Identifier section must appear in a aurantium audio map file exactly once, and must be the first section present in the file.

4.6. Clip Descriptions

4.6.1. Description

4.6.2. Cardinality

4.6.1. Description

The clip descriptions section holds all clip descriptions for clips present in the audio map.

4.6.1.2. Clip Description Section Encoding

Definition binaryClipsDescriptionSection (c : list clip) : binaryExp :=
  let text     := jsonSerializeString (jsonClips c) in
  let textUTF8 := utf8 text in
    BiRecord [
      ("id",   u64 0x4155524D43444553);
      ("size", u64 (binarySizePadded16 textUTF8));
      ("data", textUTF8)
    ].

4.6.2. Cardinality

A clip descriptions section must appear in a aurantium audio map file exactly once.

4.7. Clip Data

4.7.1. Description

4.7.2. Cardinality

4.7.1. Description

The clips data section holds all audio data for clips present in the audio map.

Informally, the audio data for each clip is stored in the order specified by the clip descriptions. For the sake of not formalizing every possible type of audio data, this specification treats the audio data as opaque reserved space:

4.7.1.3. Clip Data Section Encoding

Definition binaryClipsDataSection (c : clips) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D434C4950);
    ("size", u64 (binarySizePadded16 (binaryClipsDataSectionAudio c)));
    ("data", binaryClipsDataSectionAudio c)
  ].

4.7.1.4. Clip Data Section Encoding

Definition binaryClipsDataSectionAudio (c : clips) : binaryExp :=
  let audioDataSize   := clipAudioDataSizeTotal c in
  let audioDataSize16 := asMultipleOf16 audioDataSize in
    BiRecord [
      ("data", BiReserve audioDataSize16)
    ].

4.7.2. Cardinality

A clips data section must appear in a aurantium audio map file exactly once.

4.8. Key assignments

4.8.1. Description

4.8.2. Cardinality

4.8.1. Description

The key assignments section holds all key assignments present in the audio map.

Key assignment sections are encoded as follows:

4.8.1.3. Key Assignment Section Encoding

Definition binaryKeyAssignmentsSection (c : list keyAssignment) : binaryExp :=
  let text     := jsonSerializeString (jsonKeyAssignments c) in
  let textUTF8 := utf8 text in
    BiRecord [
      ("id",   u64 0x4155524D4b455953);
      ("size", u64 (binarySizePadded16 textUTF8));
      ("data", textUTF8)
    ].

4.8.2. Cardinality

A key assignments section must appear in a aurantium audio map file exactly once.

4.9. Metadata

4.9.1. Description

4.9.2. Cardinality

4.9.1. Description

Metadata sections are encoded as follows:

4.9.1.2. Metadata Section Encoding

Definition binaryExpMetadataSection (m : metadata) : binaryExp :=
  let text     := jsonSerializeString (jsonMetadata m) in
  let textUTF8 := utf8 text in
    BiRecord [
      ("id",   u64 0x4155524D4D455441);
      ("size", u64 (binarySizePadded16 textUTF8));
      ("data", textUTF8)
    ].

4.9.2. Cardinality

A Metadata section can appear in a aurantium audio map file at most once.

4.10. End

4.10.1. Description

4.10.2. Cardinality

4.10.1. Description

aurantium audio map files must end with exactly one End section, which has the identifier 0x4155524D454E4421 and must be of size 0.

End sections are encoded as follows:

4.10.1.3. End Encoding

Definition binaryEndSection : binaryExp := BiRecord [
  ("id",   u64 0x4155524D454E4421);
  ("size", u64 0)
].

There should be no trailing data in the audio map file after the End section.

4.10.2. Cardinality

An End section must appear in a aurantium audio map file exactly once, and must be the last section present in the file.

5. Sources

The full sources for the Rocq model underlying this specification are included here.

5.2. Aurantium/Alignment.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Arith.PeanoNat.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Lists.List.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Init.Byte.
From Stdlib Require Import Bool.Bool.
From Stdlib Require Import Program.Basics.

(** * Alignment *)

(** Return _size_ scaled such that it is a multiple of _q_. *)

Definition asMultipleOf (size q : nat) (Hnz : 0 <> q) : nat :=
  let r := size / q in
    match Nat.ltb_spec0 r q with
    | ReflectT _ _ => (r + 1) * q
    | ReflectF _ _ => r * q
    end.

Lemma p0not4 : 0 <> 4.
Proof. discriminate. Qed.

Lemma p0not16 : 0 <> 16.
Proof. discriminate. Qed.

(** Return _size_ scaled such that it is a multiple of 4. *)

Definition asMultipleOf4 (size : nat) : nat :=
  asMultipleOf size 4 p0not4.

(** Return _size_ scaled such that it is a multiple of 6. *)

Definition asMultipleOf16 (size : nat) : nat :=
  asMultipleOf size 16 p0not16.

(** If _n_ is a multiple of _m_, then _n mod m = 0_. *)

Lemma asMultipleOfMod : forall s q (Hneq : 0 <> q), (asMultipleOf s q Hneq) mod q = 0.
Proof.
  intros s q Hneq.
  unfold asMultipleOf.
  destruct (Nat.ltb_spec0 (s / q) q) as [Hlt|H1].
  - apply (Nat.Div0.mod_mul (s / q + 1) q).
  - apply (Nat.Div0.mod_mul (s / q) q).
Qed.

5.3. Aurantium/AudioMap.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Lists.List.
From Stdlib Require Import Init.Nat.

Import ListNotations.

Require Import Aurantium.Compatibility.
Require Import Aurantium.Identifier.
Require Import Aurantium.Clip.
Require Import Aurantium.KeyMapping.

(** The key assignment _k_ references clip _s_. *)
Definition keyAssignmentReferencesClip
  (k : keyAssignment)
  (s : clip)
: Prop :=
  (kaClipId k) = (clipId s).

(** The clip referenced by _k_ exists in _s_. *)
Definition keyAssignmentReferencesExists
  (k : keyAssignment)
  (s : clips)
: Prop :=
  exists p, keyAssignmentReferencesClip k p /\ In p (clipsList s).

(** All key assignment in _k_ reference clips that exist in _s_. *)
Definition keyAssignmentsReferences
  (k : keyAssignments)
  (s : clips)
: Prop :=
  forall p, In p (kasList k) -> keyAssignmentReferencesExists p s.

(** Every clip in _ss_ has at least one reference in _k_. *)
Definition clipsReferenced
  (k  : keyAssignments)
  (ss : clips)
: Prop :=
  Forall (fun s => exists a, keyAssignmentReferencesClip a s /\ In s (clipsList ss)) (clipsList ss).

Inductive audioMap : Set := {
  amIdentifier               : identifier;
  amClips                    : clips;
  amKeyAssignments           : keyAssignments;
  amKeyAssignmentsReferences : keyAssignmentsReferences amKeyAssignments amClips;
  amClipsReferenced          : clipsReferenced amKeyAssignments amClips;
}.

5.4. Aurantium/Binary.v

(*
 * Copyright © 2025 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Arith.PeanoNat.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Lists.List.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Init.Byte.
From Stdlib Require Import Bool.Bool.
From Stdlib Require Import Reals.Reals.
From Stdlib Require Import Program.Basics.

From Stdlib Require Import Psatz.

Require Import Aurantium.Alignment.
Require Import Aurantium.Divisible8.
Require Import Aurantium.Identifier.
Require Import Aurantium.Clip.
Require Import Aurantium.Descriptor.
Require Import Aurantium.Hash.
Require Import Aurantium.OctetOrder.
Require Import Aurantium.KeyMapping.
Require Import Aurantium.AudioMap.
Require Import Aurantium.Metadata.

Import ListNotations.

Local Open Scope string_scope.

Set Mangle Names.

(** The type of stream elements. *)
Inductive streamE : Set :=
  (** A 64-bit IEEE754 binary64 value. *)
  | Vf64 : R -> streamE
  (** A 64-bit unsigned integer. *)
  | Vu64 : nat -> streamE
  (** A 32-bit unsigned integer. *)
  | Vu32 : nat -> streamE
  (** An 8-bit unsigned integer. *)
  | Vu8  : nat -> streamE.

Definition u8byte (b : byte) : streamE :=
  Vu8 (Byte.to_nat b).

Definition streamEIsU8 (e : streamE) : Prop :=
  match e with
  | Vf64 _ => False
  | Vu64 _ => False
  | Vu32 _ => False
  | Vu8  _ => True
  end.

(** A proposition that describes a well-formed stream. *)
Inductive streamWellFormed : list streamE -> Prop :=
  (** An empty stream is well-formed. *)
  | BEPEmpty  : streamWellFormed []
  (** A stream consisting of a single 64-bit float is well-formed. *)
  | BEPVf64   : forall k, streamWellFormed [Vf64 k]
  (** A stream consisting of a single 64-bit integer is well-formed. *)
  | BEPVu64   : forall k, streamWellFormed [Vu64 k]
  (** A stream consisting of a single 32-bit integer is well-formed. *)
  | BEPVu32   : forall k, streamWellFormed [Vu32 k]
  (** A stream consisting of a number of 8-bit values of a length divisible by 4 is well-formed. *)
  | BEPVu8s   : forall es, Forall streamEIsU8 es -> length (es) mod 4 = 0 -> streamWellFormed es
  (** The concatenation of two well-formed streams is well-formed. *)
  | BEPAppend : forall xs ys, streamWellFormed xs -> streamWellFormed ys -> streamWellFormed (xs ++ ys).

Definition streamElementSize (s : streamE) : nat :=
  match s with
  | Vf64 _ => 8
  | Vu64 _ => 8
  | Vu32 _ => 4
  | Vu8  _ => 1
  end.

Definition streamSize (s : list streamE) : nat :=
  fold_right plus 0 (map streamElementSize s).

Section binaryExpressions.

  Local Unset Elimination Schemes.

  (** The binary expression type. *)
  Inductive binaryExp : Set :=
    (** A 32-bit unsigned integer. *)
    | BiU32     : nat -> binaryExp
    (** A 64-bit unsigned integer. *)
    | BiU64     : nat -> binaryExp
    (** A 64-bit IEEE754 binary64 value. *)
    | BiF64     : R -> binaryExp
    (** A sequence of bytes. *)
    | BiBytes   : list byte -> binaryExp
    (** A sequence of bytes describing UTF-8 encoded text. *)
    | BiUTF8    : list byte -> binaryExp
    (** An array of binary expressions. *)
    | BiArray   : list binaryExp -> binaryExp
    (** A section of reserved space. *)
    | BiReserve : nat -> binaryExp
    (** A record with named binary expression members. *)
    | BiRecord  : list (string * binaryExp) -> binaryExp.

  Section binaryExp_rect.
    Variable P             : binaryExp -> Type.
    Variable P_list        : list binaryExp -> Type.
    Hypothesis P_nil       : P_list [].
    Hypothesis P_cons      : forall x xs, P x -> P_list xs -> P_list (x :: xs).
    Hypothesis P_BiU32     : forall x, P (BiU32 x).
    Hypothesis P_BiU64     : forall x, P (BiU64 x).
    Hypothesis P_BiF64     : forall x, P (BiF64 x).
    Hypothesis P_BiBytes   : forall bs, P (BiBytes bs).
    Hypothesis P_BiUTF8    : forall bs, P (BiUTF8 bs).
    Hypothesis P_BiArray   : forall bs, P_list bs -> P (BiArray bs).
    Hypothesis P_BiReserve : forall x, P (BiReserve x).
    Hypothesis P_BiRecord  : forall fs, P_list (map snd fs) -> P (BiRecord fs).

    Fixpoint binaryExp_rect (b : binaryExp) : P b :=
      let
        fix expForAll (xs : list binaryExp) : P_list xs :=
          match xs as rxs return (P_list rxs) with
          | []        => @P_nil
          | (y :: ys) => @P_cons y ys (binaryExp_rect y) (expForAll ys)
          end
      in let
        fix forAllSnd (fs : list (string * binaryExp)) : P_list (map snd fs) :=
          match fs as rf return P_list (map snd rf) with
          | []             => @P_nil
          | ((_, y) :: ys) => @P_cons y (map snd ys) (binaryExp_rect y) (forAllSnd ys)
          end
      in
        match b with
        | BiU32 c     => P_BiU32 c
        | BiU64 c     => P_BiU64 c
        | BiF64 c     => P_BiF64 c
        | BiBytes bs  => P_BiBytes bs
        | BiUTF8 bs   => P_BiUTF8 bs
        | BiArray es  => P_BiArray es (expForAll es)
        | BiReserve c => P_BiReserve c
        | BiRecord fs => P_BiRecord fs (forAllSnd fs)
        end.

  End binaryExp_rect.

  Section binaryExp_ind.
    Variable P             : binaryExp -> Prop.
    Hypothesis P_BiU32     : forall x, P (BiU32 x).
    Hypothesis P_BiU64     : forall x, P (BiU64 x).
    Hypothesis P_BiF64     : forall x, P (BiF64 x).
    Hypothesis P_BiBytes   : forall bs, P (BiBytes bs).
    Hypothesis P_BiUTF8    : forall bs, P (BiUTF8 bs).
    Hypothesis P_BiArray   : forall bs, Forall P bs -> P (BiArray bs).
    Hypothesis P_BiReserve : forall x, P (BiReserve x).
    Hypothesis P_BiRecord  : forall fs, Forall P (map snd fs) -> P (BiRecord fs).

    Definition binaryExp_ind (b : binaryExp) : P b :=
      binaryExp_rect
        P
        (Forall P)
        (Forall_nil P)
        (Forall_cons (P:=P))
        P_BiU32
        P_BiU64
        P_BiF64
        P_BiBytes
        P_BiUTF8
        P_BiArray
        P_BiReserve
        P_BiRecord
        b.

  End binaryExp_ind.
End binaryExpressions.

(** The size of a binary expression in octets. *)
Fixpoint binarySize (b : binaryExp) : nat :=
  match b with
  | BiU32 _     => 4
  | BiU64 _     => 8
  | BiF64 _     => 8
  | BiBytes s   => 4 + asMultipleOf4 (length s)
  | BiUTF8 s    => 4 + asMultipleOf4 (length s)
  | BiArray f   => 4 + fold_right plus 0 (map binarySize f)
  | BiReserve s => asMultipleOf4 s
  | BiRecord f  => fold_right plus 0 (map (compose binarySize snd) f)
  end.

Definition binaryEvalPaddedBytes
  (b     : list byte)
  (align : nat)
  (Hneq  : 0 <> align)
: list streamE :=
  let vremaining := length b mod align in
    match vremaining with
    | 0 => map u8byte b
    | _ => map u8byte (b ++ repeat x00 (align - vremaining))
    end.

(** The binary evaluation function; produces a stream from an expression. *)
Fixpoint binaryEval (b : binaryExp) : list streamE :=
  match b with
  | BiU32 k     => [Vu32 k]
  | BiU64 k     => [Vu64 k]
  | BiF64 k     => [Vf64 k]
  | BiBytes s   => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiUTF8 s    => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiArray f   => (Vu32 (length f)) :: concat (map binaryEval f)
  | BiReserve s => repeat (Vu8 0) (asMultipleOf4 s)
  | BiRecord f  => concat (map (compose binaryEval snd) f)
  end.

Definition binarySizePadded16 (b : binaryExp) : nat :=
  asMultipleOf16 (binarySize b).

Definition utf8 (s : string) : binaryExp :=
  BiUTF8 (list_byte_of_string s).

Definition u32 := BiU32.
Definition u64 := BiU64.
Definition f64 := BiF64.

Lemma fold_right_add_cons : forall x xs,
  x + fold_right plus 0 xs = fold_right plus 0 (x :: xs).
Proof. reflexivity. Qed.

Lemma forall_map_binarySize : forall es,
  Forall (fun b : binaryExp => binarySize b mod 4 = 0) es
    <-> Forall (fun n => n mod 4 = 0) (map binarySize es).
Proof.
  intros es.
  induction es.
  constructor.
  - rewrite Forall_map.
    intros H. trivial.
  - rewrite Forall_map.
    intros H. trivial.
  - rewrite Forall_map.
    constructor.
    intros H; trivial.
    intros H; trivial.
Qed.

(** The size of a binary expression is always divisible by 4. *)
Theorem binarySizeMultiple4 : forall b, binarySize (b) mod 4 = 0.
Proof.
  intros b.
  induction b as [Hbu32|Hbu64|Hbf64|Hbbyte|Hbutf|xs HFA|Hbuns|xs HFF] using binaryExp_ind.
  (* U32 values are of size 4 *)
  - reflexivity.
  (* U64 values are of size 8 *)
  - reflexivity.
  (* F64 values are of size 8 *)
  - reflexivity.

  (* Byte array values are rounded up to a multiple of 4 and prefixed with 4 *)
  - unfold binarySize.
    unfold asMultipleOf4.
    remember (asMultipleOf (Datatypes.length Hbbyte) 4 p0not4) as size eqn:Heqsize.
    rewrite Nat.add_comm.
    rewrite <- (Nat.Div0.add_mod_idemp_l size 4 4).
    assert (size mod 4 = 0) as Hm0. {
      rewrite Heqsize.
      apply (asMultipleOfMod (Datatypes.length Hbbyte) 4 (p0not4)).
    }
    rewrite Hm0.
    reflexivity.

  (* UTF-8 values are rounded up to a multiple of 4 and prefixed with 4 *)
  - unfold binarySize.
    unfold asMultipleOf4.
    remember (asMultipleOf (Datatypes.length Hbutf) 4 p0not4) as size eqn:Heqsize.
    rewrite Nat.add_comm.
    rewrite <- (Nat.Div0.add_mod_idemp_l size 4 4).
    assert (size mod 4 = 0) as Hm0. {
      rewrite Heqsize.
      apply (asMultipleOfMod (Datatypes.length Hbutf) 4 (p0not4)).
    }
    rewrite Hm0.
    reflexivity.

  (* Each element of an array is a multiple of 4, so the entire array is too. *)
  - unfold binarySize.
    fold binarySize.
    induction xs as [|y ys HforAllInd].
    -- reflexivity.
    -- assert (fold_right add 0 (map binarySize (y :: ys)) mod 4 = 0) as HfoldEq. {
         apply (@divisibilityNFoldPlus 4 (map binarySize (y :: ys))).
         discriminate.
         rewrite <- forall_map_binarySize.
         exact HFA.
       }
       rewrite map_cons.
       rewrite map_cons in HfoldEq.
       assert (4 mod 4 = 0) as H4mod40 by (reflexivity).
       assert (0 <> 4) as H0n4 by (discriminate).
       apply (divisiblityNAdd 4 (fold_right add 0 (binarySize y :: map binarySize ys)) 4 H0n4 H4mod40 HfoldEq).

  (* Unspecified values are rounded up. *)
  - unfold binarySize.
    unfold asMultipleOf4.
    rewrite asMultipleOfMod.
    reflexivity.

  (* Each element of an record is a multiple of 4, so the entire record is too. *)
  - unfold binarySize.
    fold binarySize.
    induction xs as [|y ys HforAllInd].
    -- reflexivity.
    -- rewrite map_cons.
       rewrite map_cons in HFF.
       rewrite <- fold_right_add_cons.
       apply divisiblityNAdd.
       discriminate.
       apply (Forall_inv HFF).
       apply HforAllInd.
       apply (Forall_inv_tail HFF).
Qed.

Lemma sub_0_lt_ymx : forall x y,
  0 <= x -> x < y -> 0 < y - x.
Proof.
  intros x y Hle Hlt.
  destruct x as [|a].
  - rewrite Nat.sub_0_r.
    exact Hlt.
  - rewrite <- Nat.lt_add_lt_sub_l.
    rewrite Nat.add_0_r.
    exact Hlt.
Qed.

Lemma mod_sub : forall x m,
  0 < m -> 0 < m - (x mod m) <= m.
Proof.
  intros x m Hlt.
  constructor.
  - assert (0 <= x mod m < m) as HmRange. {
      apply Nat.mod_bound_pos.
      apply Nat.le_0_l.
      exact Hlt.
    }
    destruct HmRange as [HA HB].
    remember (x mod m) as y.
    apply (sub_0_lt_ymx y m HA HB).
  - assert (x mod m < m) as HmRange. {
      apply Nat.mod_upper_bound.
      apply Nat.neq_sym.
      apply Nat.lt_neq.
      exact Hlt.
    }
    apply Nat.le_sub_l.
Qed.

Lemma mod_opposition : forall x a,
  0 <> a -> x mod a + (a - x mod a) = a.
Proof.
  intros x a Hnz.
  assert (x mod a < a) as Hxma. {
    apply (Nat.mod_upper_bound).
    apply Nat.neq_sym.
    exact Hnz.
  }
  remember (x mod a) as y eqn:Heqy.
  lia.
Qed.

Theorem binaryEvalPaddedBytesAligned : forall bs a (Hnz : 0 <> a),
  length (binaryEvalPaddedBytes bs a Hnz) mod a = 0.
Proof.
  intros bs a Hnz.
  unfold binaryEvalPaddedBytes.
  destruct (Datatypes.length bs mod a) eqn:Hlen.
  - rewrite length_map.
    exact Hlen.
  - rewrite length_map.
    rewrite length_app.
    rewrite repeat_length.
    rewrite <- Hlen.
    remember (Datatypes.length bs) as x.
    rewrite <- (Nat.Div0.add_mod_idemp_l x (a - x mod a) a).
    assert ((x mod a + (a - x mod a)) = a) as Heqa. {
      rewrite (mod_opposition x a Hnz).
      reflexivity.
    }
    rewrite Heqa.
    apply Nat.Div0.mod_same.
Qed.

Lemma repeat_eq : forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
  Forall (eq x) (repeat x n).
Proof.
  intros A P n x.
  induction n as [|m Hm].
  - constructor.
  - simpl.
    constructor.
    reflexivity.
    exact Hm.
Qed.

Lemma Forall_implies : forall (A : Type) (P : A -> Prop) (Q : A -> Prop) (xs : list A) (H : forall x, P x -> Q x),
  Forall P xs -> Forall Q xs.
Proof.
  intros A P Q xs Ht HforAll.
  induction HforAll as [|y ys Hpy HfaP HfaQ].
  - constructor.
  - constructor.
    apply (Ht y Hpy).
    exact HfaQ.
Qed.

Theorem binaryEvalPaddedBytesU8 : forall bs a (Hnz : 0 <> a),
  Forall streamEIsU8 (binaryEvalPaddedBytes bs a Hnz).
Proof.
  intros bs a Hnz.
  unfold binaryEvalPaddedBytes.
  destruct (Datatypes.length bs mod a) as [|HB].
  - rewrite Forall_map.
    induction bs as [|r rs Hrs].
    -- constructor.
    -- constructor.
       reflexivity.
       exact Hrs.
  - rewrite map_app.
    assert (Forall streamEIsU8 (map u8byte bs)) as Hmap. {
      rewrite Forall_map.
      induction bs as [|r rs Hrs].
      - constructor.
      - constructor.
        reflexivity.
        exact Hrs.
    }
    assert (Forall streamEIsU8 (map u8byte (repeat "000"%byte (a - S HB)))) as HmapR. {
      rewrite Forall_map.
      assert (Forall (eq "000"%byte) (repeat "000"%byte (a - S HB))) as Hfeq
        by (apply (repeat_eq byte (fun _ : byte => True) (a - S HB) "000"%byte)).
      simpl.
      apply (@Forall_implies byte (eq "000"%byte) (fun _ : byte => True) (repeat "000"%byte (a - S HB))). {
        intros. exact I.
      }
      exact Hfeq.
    }
    apply Forall_app.
    constructor.
    exact Hmap.
    exact HmapR.
Qed.

Lemma app_cons : forall (A : Type) (x : A) (xs : list A),
  x :: xs = app (cons x nil) xs.
Proof.
  intros A x xs.
  reflexivity.
Qed.

(** Streams produced by the _binaryEval_ function are well-formed. *)
Theorem binaryEvalStreamsWellFormed : forall b,
  streamWellFormed (binaryEval b).
Proof.
  intros b.
  induction b as [a0|a1|a2|a3|a4|a5 Hfa|a6|a7 Hfa].
  (* U32 *)
  - apply BEPVu32.
  (* U64 *)
  - apply BEPVu64.
  (* F64 *)
  - apply BEPVf64.
  (* Bytes *)
  - unfold binaryEval.
    rewrite app_cons.
    apply BEPAppend.
    apply BEPVu32.
    assert (length (binaryEvalPaddedBytes a3 4 p0not4) mod 4 = 0) as Hlm
      by (apply (binaryEvalPaddedBytesAligned)).
    apply BEPVu8s.
    apply binaryEvalPaddedBytesU8.
    exact Hlm.
  (* UTF-8 *)
  - unfold binaryEval.
    rewrite app_cons.
    apply BEPAppend.
    apply BEPVu32.
    assert (length (binaryEvalPaddedBytes a4 4 p0not4) mod 4 = 0) as Hlm
      by (apply (binaryEvalPaddedBytesAligned)).
    assert (Forall streamEIsU8 (binaryEvalPaddedBytes a4 4 p0not4)) as Hu8
      by (apply (binaryEvalPaddedBytesU8)).
    apply (BEPVu8s _ Hu8 Hlm).
  (* Array *)
  - simpl.
    rewrite app_cons.
    apply BEPAppend.
    apply BEPVu32.
    induction a5 as [|q qs IHqs].
    -- constructor.
    -- assert (streamWellFormed (concat (map binaryEval qs))) as HqsWF
         by (apply (IHqs (Forall_inv_tail Hfa))).
       assert (streamWellFormed (binaryEval q)) as HqWF
         by (apply (Forall_inv Hfa)).
       simpl.
       apply BEPAppend.
       exact HqWF.
       exact HqsWF.
  (* Reserve *)
  - simpl.
    unfold asMultipleOf4.
    remember (asMultipleOf a6 4 p0not4) as size eqn:Heqsize.
    assert (size mod 4 = 0) as Heqm. {
      rewrite Heqsize.
      apply (asMultipleOfMod).
    }
    assert ((compose Vu8 Byte.to_nat) "000"%byte = (Vu8 0)) as HbyteEq by reflexivity.
    apply BEPVu8s.
    assert (Forall (eq (Vu8 0)) (repeat (Vu8 0) size)) as Hfeq
      by (apply (@repeat_eq streamE streamEIsU8 size (Vu8 0))).
    apply (@Forall_implies streamE (eq (Vu8 0)) streamEIsU8 (repeat (Vu8 0) size)). {
      intros x Hxeq.
      unfold streamEIsU8.
      rewrite <- Hxeq.
      exact I.
    }
    exact Hfeq.
    rewrite repeat_length.
    exact Heqm.
  (* Record *)
  - simpl.
    induction a7 as [|q qs IHqs].
    -- constructor.
    -- assert (Forall (fun b : binaryExp => streamWellFormed (binaryEval b)) (map snd qs)) as Hfqs. {
         apply (@Forall_inv_tail binaryExp (fun b : binaryExp => streamWellFormed (binaryEval b)) (snd q) (map snd qs)). {
           assert ((map snd (q :: qs)) = (snd q :: map snd qs)) as Hmc by reflexivity.
           rewrite <- Hmc.
           exact Hfa.
         }
       }
       assert (streamWellFormed (concat (map (compose binaryEval snd) qs))) as Hconqs by (apply (IHqs Hfqs)).
       rewrite map_cons.
       rewrite concat_cons.
       apply BEPAppend.
       rewrite map_cons in Hfa.
       apply (Forall_inv Hfa).
       exact Hconqs.
Qed.

Lemma fold_right_1_length : forall xs,
  Forall (eq 1) xs -> fold_right add 0 xs = length xs.
Proof.
  intros xs Hfa.
  induction xs as [|y ys IHxs].
  - reflexivity.
  - rewrite <- fold_right_add_cons.
    assert (length (y :: ys) = 1 + length (ys)) as HlenYs by reflexivity.
    rewrite HlenYs.
    assert (1 = y) as Hy1 by (apply (Forall_inv Hfa)).
    rewrite <- Hy1.
    f_equal.
    apply IHxs.
    apply (Forall_inv_tail Hfa).
Qed.

Theorem fold_right_add_app : forall xs ys,
  fold_right add 0 xs + fold_right add 0 ys = fold_right add 0 (xs ++ ys).
Proof.
  intros xs ys.
  rewrite fold_right_app.
  generalize dependent ys.
  induction xs as [|q qs IHqs].
  - reflexivity.
  - intros ys.
    simpl.
    rewrite <- (IHqs ys).
    rewrite Nat.add_assoc.
    reflexivity.
Qed.

Theorem streamSizeApp : forall xs ys,
  streamSize xs + streamSize ys = streamSize (xs ++ ys).
Proof.
  intros xs ys.
  unfold streamSize.
  rewrite map_app.
  rewrite fold_right_add_app.
  reflexivity.
Qed.

(** All well-formed streams have a size divisible by 4. *)
Theorem streamsWellFormedDivisible4 : forall es,
  streamWellFormed es -> streamSize es mod 4 = 0.
Proof.
  intros es Hwf.
  induction Hwf as [|H1|H2|H3|es Hfa Hsize|xs ys Hxswf Hxsize Hyswf Hysize].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - unfold streamSize.
    assert (Forall (fun e => 1 = streamElementSize e) es) as HFaSize. {
      apply (@Forall_implies streamE streamEIsU8 (fun e : streamE => 1 = streamElementSize e) es). {
        intros x His.
        destruct x as [f64|u64|u32|u8].
        - contradiction.
        - contradiction.
        - contradiction.
        - reflexivity.
      }
      exact Hfa.
    }
    assert (Forall (eq 1) (map streamElementSize es)) as Hall1. {
      apply (@Forall_map _ _ _ _ es).
      exact HFaSize.
    }
    assert (fold_right add 0 (map streamElementSize es) = length es) as HlenEq. {
      assert (length es = length (map streamElementSize es)) as HmapLen. {
        rewrite length_map.
        reflexivity.
      }
      rewrite HmapLen.
      apply (fold_right_1_length (map streamElementSize es) Hall1).
    }
    rewrite HlenEq.
    exact Hsize.
  - rewrite <- streamSizeApp.
    apply divisiblityNAdd.
    discriminate.
    exact Hxsize.
    exact Hysize.
Qed.

5.5. Aurantium/BinaryData.v

(*
 * Copyright © 2025 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.
From Stdlib Require Import Lists.List.

Local Open Scope string_scope.

Import ListNotations.

Require Import Aurantium.Alignment.
Require Import Aurantium.AudioMap.
Require Import Aurantium.Binary.
Require Import Aurantium.Identifier.
Require Import Aurantium.KeyMapping.
Require Import Aurantium.Clip.
Require Import Aurantium.Json.
Require Import Aurantium.JsonData.
Require Import Aurantium.Metadata.

(** The file header. *)
Definition binaryExpFileHeader : binaryExp :=
  BiRecord [
    ("id",           u64 0x894155520D0A1A0A);
    ("versionMajor", u32 1);
    ("versionMinor", u32 0)
  ].

(** The binary encoding of an identifier. *)
Definition binaryIdentifier (i : identifier) : binaryExp :=
  BiRecord [
    ("group",        utf8 (idGroup i));
    ("name",         utf8 (idName i));
    ("versionMajor", u32 (idVersionMajor i));
    ("versionMinor", u32 (idVersionMinor i))
  ].

(** The AURM_ID! section. *)
Definition binaryIdentifierSection (i : identifier) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D5F494421);
    ("size", u64 (binarySizePadded16 (binaryIdentifier i)));
    ("data", binaryIdentifier i)
  ].

(** The AURMEND! section. *)
Definition binaryEndSection : binaryExp := BiRecord [
  ("id",   u64 0x4155524D454E4421);
  ("size", u64 0)
].

(** The AURMCDES section. *)
Definition binaryClipsDescriptionSection (c : list clip) : binaryExp :=
  let text     := jsonSerializeString (jsonClips c) in
  let textUTF8 := utf8 text in
    BiRecord [
      ("id",   u64 0x4155524D43444553);
      ("size", u64 (binarySizePadded16 textUTF8));
      ("data", textUTF8)
    ].

Definition binaryClipsDataSectionAudio (c : clips) : binaryExp :=
  let audioDataSize   := clipAudioDataSizeTotal c in
  let audioDataSize16 := asMultipleOf16 audioDataSize in
    BiRecord [
      ("data", BiReserve audioDataSize16)
    ].

(** The AURMCDAT section. *)
Definition binaryClipsDataSection (c : clips) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D434C4950);
    ("size", u64 (binarySizePadded16 (binaryClipsDataSectionAudio c)));
    ("data", binaryClipsDataSectionAudio c)
  ].

(** The AURMKEYS section. *)
Definition binaryKeyAssignmentsSection (c : list keyAssignment) : binaryExp :=
  let text     := jsonSerializeString (jsonKeyAssignments c) in
  let textUTF8 := utf8 text in
    BiRecord [
      ("id",   u64 0x4155524D4b455953);
      ("size", u64 (binarySizePadded16 textUTF8));
      ("data", textUTF8)
    ].

(** The AURMMETA section. *)
Definition binaryExpMetadataSection (m : metadata) : binaryExp :=
  let text     := jsonSerializeString (jsonMetadata m) in
  let textUTF8 := utf8 text in
    BiRecord [
      ("id",   u64 0x4155524D4D455441);
      ("size", u64 (binarySizePadded16 textUTF8));
      ("data", textUTF8)
    ].

(** An example audio map file as a binary expression. *)
Example binaryExampleFile (m : audioMap) : binaryExp :=
  BiRecord [
    ("file",              binaryExpFileHeader);
    ("id",                binaryIdentifierSection (amIdentifier m));
    ("clipsData",         binaryClipsDataSection (amClips m));
    ("clipsDescriptions", binaryClipsDescriptionSection (clipsList (amClips m)));
    ("keys",              binaryKeyAssignmentsSection (kasList (amKeyAssignments m)));
    ("end",               binaryEndSection)
  ].

5.6. Aurantium/Clip.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.
From Stdlib Require Import Lists.List.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Reals.Reals.
From Stdlib Require Import Psatz.

Import ListNotations.

Set Mangle Names.

Require Import Aurantium.Descriptor.
Require Import Aurantium.OctetOrder.
Require Import Aurantium.Compatibility.
Require Import Aurantium.Intersection.
Require Import Aurantium.Hash.

(** The known audio formats. *)
Inductive audioFormatType : Set :=
  (** Pulse code modulation using signed values. *)
  | AFPCMLinearIntegerSigned : audioFormatType
  (** Pulse code modulation using unsigned values. *)
  | AFPCMLinearIntegerUnsigned : audioFormatType
  (** Pulse code modulation using floating point values. *)
  | AFPCMLinearFloat : audioFormatType
  (** FLAC-compressed audio. *)
  | AFFlac : audioFormatType
  (** A format not known by this specification. *)
  | AFUnknown : descriptor -> audioFormatType
  .

Theorem audioFormatTypeEqDec : forall (x y : audioFormatType),
  {x = y}+{x <> y}.
Proof.
  intros x y.
  destruct x; (destruct y; decide equality; apply string_dec).
Qed.

Local Open Scope char_scope.
Local Open Scope string_scope.

Definition audioFormatDescribe (f : audioFormatType) : descriptor :=
  match f with
  | AFPCMLinearIntegerSigned   => "com.io7m.aurantium.pcm_linear_integer_signed"
  | AFPCMLinearIntegerUnsigned => "com.io7m.aurantium.pcm_linear_integer_unsigned"
  | AFPCMLinearFloat           => "com.io7m.aurantium.pcm_linear_float"
  | AFFlac                     => "com.io7m.aurantium.flac"
  | AFUnknown d                => d
  end.

#[export]
Instance audioFormatDescribable : describable audioFormatType := {
  descriptorOf c := audioFormatDescribe c
}.

(**
  A loop range value describes a region of the clip that represents
  a good choice for looping audio.
*)
Inductive loopRange : Set := {
  lrFrameStart        : nat;
  lrFrameEndInclusive : nat
}.

Definition loopRangeInvariants (lr : loopRange) : Prop :=
  (lrFrameStart lr) <= (lrFrameEndInclusive lr).

Theorem loopRangeEqDec : forall (x y : loopRange),
  {x = y}+{x <> y}.
Proof.
  intros x y.
  destruct x; (
    destruct y; (
      try decide equality;
      try decide equality
    )
  ).
Qed.

(** A description of a single audio clip. *)
Inductive clip : Set := clipMake {
  (** The unique identifier for the clip. *)
  clipId : nat;
  (** The clip name, for descriptive purposes. *)
  clipName : string;
  (** The clip audio format name. *)
  clipFormat : audioFormatType;
  (** The sample rate in bits per second. *)
  clipSampleRate : nat;
  (** The clip sample depth in bits per clip. *)
  clipSampleDepth : nat;
  (** The number of channels in the clip. *)
  clipChannels : nat;
  (** The endianness of the audio data. *)
  clipEndianness : octetOrder;
  (** The hash of the audio data. *)
  clipHash : hashValue;
  (** The offset of the first octet of audio data. *)
  clipOffset : nat;
  (** The size of the audio data in octets. *)
  clipSize : nat;
  (** An optional loop region. *)
  clipLoopRange : option loopRange
}.

(**
  The number of frames in a clip is equal to the size of the
  audio in octets divided by the size of a sample in octets.
*)
Definition clipFrameCount (c : clip) : nat :=
  (clipSize c) / (clipSampleDepth c / 8).

(** A loop range is only valid for a given clip if the end frame
    of the loop range is less than the number of frames in the clip. *)
Definition clipFrameCountLoopRange
  (c  : clip)
  (lr : loopRange)
: Prop :=
  (lrFrameEndInclusive lr) < (clipFrameCount c).

(** A restatement of the loop range proposition for optional loop ranges. *)
Definition clipFrameCountLoopRangeOption
  (c  : clip)
  (lr : option loopRange)
: Prop :=
  match lr with
  | Some r => clipFrameCountLoopRange c r
  | None   => True
  end.

Definition clipInvariants (c : clip) : Prop :=
     (clipId                        c <= 4294967295)
  /\ (clipSampleRate                c <= 4294967295)
  /\ (clipSampleDepth               c <= 4294967295)
  /\ (clipChannels                  c <= 4294967295)
  /\ (clipOffset                    c <= 18446744073709551615)
  /\ (clipSize                      c <= 18446744073709551615)
  /\ (clipFrameCountLoopRangeOption c (clipLoopRange c))
  .

Theorem clipEqDec : forall (x y : clip),
  {x = y}+{x <> y}.
Proof.
  intros x y.
  destruct x; (
    destruct y; (
      try decide equality;
      try apply string_dec;
      try decide equality;
      try apply string_dec;
      try apply hashValueEqDec;
      try apply loopRangeEqDec
    )
  ).
  apply hashAlgorithmEqDec.
Qed.

Inductive clipsListIdIsSorted : list clip -> Prop :=
  | ClipIdOne  : forall s,
      clipsListIdIsSorted [s]
  | ClipIdCons : forall s0 s1 ss,
    (clipId s0) < (clipId s1) ->
      clipsListIdIsSorted (s0 :: ss) ->
        clipsListIdIsSorted (s1 :: s0 :: ss).

Inductive clipsListOffsetIsSorted : list clip -> Prop :=
  | ClipOffsetOne : forall s,
    clipsListOffsetIsSorted [s]
  | ClipOffsetCons : forall s0 s1 ss,
    ((clipOffset s1) + (clipSize s1)) < clipOffset s0 ->
      clipsListOffsetIsSorted (s0 :: ss) ->
        clipsListOffsetIsSorted (s1 :: s0 :: ss).

Inductive clips : Set := clipsMake {
  clipsList         : list clip;
  clipsIdSorted     : clipsListIdIsSorted clipsList;
  clipsOffsetSorted : clipsListOffsetIsSorted clipsList;
}.

Lemma clipsNonEmpty : forall (s : clips),
  [] <> clipsList s.
Proof.
  intros s.
  destruct (clipsIdSorted s); discriminate.
Qed.

Definition clipFirst : forall (s : clips), clip.
Proof.
  intro s.
  pose proof (clipsNonEmpty s) as H_ne.
  destruct (clipsList s) eqn:Hs.
  - contradiction.
  - intuition.
Qed.

(** Find the clip with the given ID. *)
Fixpoint clipForId
  (i  : nat)
  (ca : list clip)
: option clip :=
  match ca with
  | nil         => None
  | cons a rest =>
    match Nat.eq_dec (clipId a) i with
    | left _  => Some a
    | right _ => clipForId i rest
    end
  end.

(** Determine all the elements of _ca_ that are not in _cb_. *)
Definition clipsRemoved
  (ca : list clip)
  (cb : list clip)
: list clip :=
  filter (fun c =>
    match clipForId (clipId c) cb with
    | None   => false
    | Some _ => true
    end) ca.

(** Determine all the elements of _cb_ that are not in _ca_. *)
Definition clipsAdded
  (ca : list clip)
  (cb : list clip)
: list clip :=
  clipsRemoved cb ca.

Definition clipsCompatCompareRemoved
  (r : list clip)
: list compatVersionChangeRecord :=
  map (fun a => CVRMake CVersionChangeMajor "A clip was removed.") r.

Lemma clipsCompatCompareRemovedForall : forall r,
  Forall (fun a => cvrChange a = CVersionChangeMajor)
    (clipsCompatCompareRemoved r).
Proof.
  intros r.
  apply Forall_map.
  induction r as [|y ys]; intuition.
Qed.

Definition clipsCompatCompareAdded
  (r : list clip)
: list compatVersionChangeRecord :=
  map (fun a => CVRMake CVersionChangeMinor "A clip was added.") r.

Lemma clipsCompatCompareAddedForall : forall r,
  [] <> r ->
    Forall (fun a => cvrChange a = CVersionChangeMinor)
      (clipsCompatCompareAdded r).
Proof.
  intros r Hneq.
  apply Forall_map.
  induction r as [|y ys IHy]. {
    contradict Hneq; reflexivity.
  } {
    constructor.
    reflexivity.
    destruct ys as [|z zs]. {
      constructor.
    } {
      apply IHy.
      discriminate.
    }
  }
Qed.

(** The rules that define the version number increments required for
    a pair of clips. *)
Definition clipCompatCompare
  (c0 c1 : clip)
: compatVersionChangeRecord :=
  match clipEqDec c0 c1 with
  | left _ =>
    CVRMake CVersionChangeNone ""
  | right _ =>
    CVRMake CVersionChangeMajor "The values of the clip were changed."
  end.

Definition clipsCompatCompareChanged
  (r : list (clip * clip))
: list compatVersionChangeRecord :=
  map (fun p => clipCompatCompare (fst p) (snd p)) r.

Definition clipsCompatCompareFull
  (ca cb : list clip)
: list compatVersionChangeRecord :=
  let f              := (fun c cs => clipForId (clipId c) cs) in
  let removed        := clipsRemoved ca cb in
  let added          := clipsAdded ca cb in
  let changed        := intersectionPairs f ca cb in
  let removedChanges := clipsCompatCompareRemoved removed in
  let addedChanges   := clipsCompatCompareAdded added in
  let changedChanges := clipsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

(** If there's a non-empty list of removed clips, a major version change is required. *)
Theorem clipsCompatCompareMajor0 : forall ca cb,
  [] <> clipsRemoved ca cb ->
    compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
      = CVersionChangeMajor.
Proof.
  intros ca cb H_ne.
  unfold clipsCompatCompareFull.
  apply compatVersionChangesMaximumCorrect0.
  apply in_map_iff.
  destruct (clipsRemoved ca cb) as [|y ys]. {
    contradict H_ne; reflexivity.
  } {
    simpl.
    exists {| cvrChange := CVersionChangeMajor; cvrReason := "A clip was removed." |}.
    intuition.
  }
Qed.

(** Adding a clip is a minor change. *)
Theorem clipsCompatCompareMinor0 : forall ca cb,
  [] = clipsRemoved ca cb ->
    [] <> clipsAdded ca cb ->
      (forall f, [] = intersectionPairs f ca cb) ->
        compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
          = CVersionChangeMinor.
Proof.
  intros ca cb Hrm Hadd Hint.
  unfold clipsCompatCompareFull.
  rewrite <- Hrm.
  rewrite <- Hint.
  simpl.
  rewrite app_nil_r.
  clear Hrm.
  clear Hint.

  destruct (clipsAdded ca cb) as [|y ys]. {
    contradict Hadd; reflexivity.
  } {
    unfold compatVersionChangeRecordsMaximum.
    simpl.

    (* We can show that either one of the arguments _must_ be equal to Minor
       and the other to something minor or less. *)
    rewrite (
      compatVersionChangeMaxMinorInv
        CVersionChangeMinor
          (compatVersionChangesMaximum
            (map (fun r : compatVersionChangeRecord => cvrChange r)
               (clipsCompatCompareAdded ys)))
    ).

    unfold clipsCompatCompareAdded.
    rewrite map_map.
    simpl.

    (* We can prove that all elements map to a minor change. *)
    assert (
      Forall
        (fun c => c = CVersionChangeMinor)
        (map (fun x : clip => CVersionChangeMinor) ys)
    ) as Hfa1. {
      rewrite Forall_map.
      rewrite Forall_forall.
      reflexivity.
    }

    apply CVMMinorLeft.
    constructor. {
      reflexivity.
    } {
      clear Hadd.
      induction (map (fun _ : clip => CVersionChangeMinor) ys) as [|z zs IHz]. {
        right; reflexivity.
      } {
        left.
        pose proof (Forall_inv Hfa1) as Hfb0.
        pose proof (Forall_inv_tail Hfa1) as Hfb1.
        simpl.
        rewrite Hfb0.
        destruct (IHz Hfb1) as [H0|H1]. {
          rewrite H0.
          reflexivity.
        } {
          rewrite H1.
          reflexivity.
        }
      }
    }
  }
Qed.

Fixpoint clipAudioDataSizeTotalAux (c : list clip) : nat :=
  match c with
  | []        => 0
  | (x :: []) => (clipOffset x) + (clipSize x)
  | (x :: xs) => clipAudioDataSizeTotalAux xs
  end.

Definition clipAudioDataSizeTotal (c : clips) : nat :=
  clipAudioDataSizeTotalAux (clipsList c).

Local Open Scope R_scope.

Unset Mangle Names.

Definition pcmIntegerEncodeSigned
  (depth     : nat)
  (amplitude : R)
: R :=
  match Rle_dec 0 amplitude with
  | left _  => Rmult amplitude ((pow 2 (depth - 1)) - 1)
  | right _ => Rmult amplitude (pow 2 (depth - 1))
  end.

Remark pcmIntegerEncodeSigned16_Low : pcmIntegerEncodeSigned 16 (-1) = -32768.
Proof.
  unfold pcmIntegerEncodeSigned.
  destruct (Rle_dec 0 (-1)) as [HL|HR]. {
    contradict HL.
    lra.
  } {
    assert (sub 16 1 = 15%nat) as H0 by lia.
    rewrite H0.
    assert (2 ^ 15 = 32768) as H1 by lra.
    rewrite H1.
    lra.
  }
Qed.

Remark pcmIntegerEncodeSigned16_Mid : pcmIntegerEncodeSigned 16 0 = 0.
Proof.
  unfold pcmIntegerEncodeSigned.
  destruct (Rle_dec 0 0) as [HL|HR]. {
    lra.
  } {
    contradict HR; lra.
  }
Qed.

Remark pcmIntegerEncodeSigned16_High : pcmIntegerEncodeSigned 16 1 = 32767.
Proof.
  unfold pcmIntegerEncodeSigned.
  destruct (Rle_dec 0 1) as [HL|HR]. {
    assert (sub 16 1 = 15%nat) as H0 by lia.
    rewrite H0.
    assert (2 ^ 15 - 1 = 32767) as H1 by lra.
    rewrite H1.
    lra.
  } {
    contradict HR; lra.
  }
Qed.

Definition pcmIntegerEncodeUnsigned
  (depth     : nat)
  (amplitude : R)
: R :=
  let s : R := Rplus (Rdiv amplitude 2%R) 0.5%R in
    Rmult s (pow 2 depth).

Remark pcmIntegerEncodeUnsigned16_Low : pcmIntegerEncodeUnsigned 16 (-1) = 0.
Proof.
  unfold pcmIntegerEncodeUnsigned.
  lra.
Qed.

Remark pcmIntegerEncodeUnsigned16_Mid : pcmIntegerEncodeUnsigned 16 0 = 32768.
Proof.
  unfold pcmIntegerEncodeUnsigned.
  lra.
Qed.

Remark pcmIntegerEncodeUnsigned16_High : pcmIntegerEncodeUnsigned 16 1 = 65536.
Proof.
  unfold pcmIntegerEncodeUnsigned.
  lra.
Qed.

5.7. Aurantium/Compatibility.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

Local Open Scope string_scope.
Local Open Scope char_scope.

(** * Compatibility *)

(** The version number change required for a given comparison. *)
Inductive compatVersionChange : Set :=
  (** No version change is required. *)
  | CVersionChangeNone
  (** The change requires a minor version number increment. *)
  | CVersionChangeMinor
  (** The change required a major version number increment. *)
  | CVersionChangeMajor
  .

(** Change value equality decidable. *)
Theorem compatVersionChangeEqDec : forall (x y : compatVersionChange),
  {x = y}+{~x = y}.
Proof. decide equality. Qed.

(** A record of a change, and a reason why the change was at the given level. *)
Record compatVersionChangeRecord : Set := CVRMake {
  cvrChange : compatVersionChange;
  cvrReason : string
}.

(** The maximum compatibility change required from two version changes. *)
Definition compatVersionChangeMax
  (x y : compatVersionChange)
: compatVersionChange :=
  match (x, y) with
  | (CVersionChangeMajor , _                  ) => CVersionChangeMajor
  | (_                   , CVersionChangeMajor) => CVersionChangeMajor
  | (CVersionChangeMinor , CVersionChangeNone ) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeMinor , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeNone ) => CVersionChangeNone
  end.

(** The maximum function is reflexive. *)
Theorem compatVersionChangeMaxRefl : forall x,
  compatVersionChangeMax x x = x.
Proof.
  intros x.
  destruct x; auto.
Qed.

(** The maximum function is commutative. *)
Theorem compatVersionChangeMaxComm : forall x y,
  compatVersionChangeMax x y = compatVersionChangeMax y x.
Proof.
  intros x y.
  destruct x; auto.
  destruct y; auto.
Qed.

(** The maximum function is associative. *)
Theorem compatVersionChangeMaxAssoc : forall x y z,
  compatVersionChangeMax x (compatVersionChangeMax y z) = compatVersionChangeMax (compatVersionChangeMax x y) z.
Proof.
  intros x y.
  destruct x; (destruct y; destruct z; auto).
Qed.

Theorem compatVersionChangeMaxInv : forall x y,
  compatVersionChangeMax x y = CVersionChangeMajor
    <-> (x = CVersionChangeMajor) \/ (y = CVersionChangeMajor).
Proof.
  intros x y.
  constructor. {
    intros Hmax.
    destruct x. {
      destruct y.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
      right; reflexivity.
    } {
      destruct y.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
      right; reflexivity.
    } {
      destruct y.
      left; reflexivity.
      left; reflexivity.
      left; reflexivity.
    }
  } {
    intros Hmax.
    destruct x. {
      destruct Hmax as [HL|HR].
      contradict HL; discriminate.
      destruct y.
      contradict HR; discriminate.
      contradict HR; discriminate.
      reflexivity.
    } {
      destruct Hmax as [HL|HR].
      contradict HL; discriminate.
      destruct y.
      contradict HR; discriminate.
      contradict HR; discriminate.
      reflexivity.
    } {
      destruct Hmax as [HL|HR].
      destruct y.
      reflexivity.
      reflexivity.
      reflexivity.
      reflexivity.
    }
  }
Qed.

Inductive compatVersionMaxMinor : compatVersionChange -> compatVersionChange -> Prop :=
  | CVMMinorLeft : forall x y,
    x = CVersionChangeMinor /\ (y = CVersionChangeMinor \/ y = CVersionChangeNone) ->
      compatVersionMaxMinor x y
  | CVMMinorRight : forall x y,
    (x = CVersionChangeMinor \/ x = CVersionChangeNone) /\ y = CVersionChangeMinor ->
      compatVersionMaxMinor x y.

Theorem compatVersionChangeMaxMinorInv : forall x y,
  compatVersionChangeMax x y = CVersionChangeMinor
    <-> compatVersionMaxMinor x y.
Proof.
  intros x y.
  constructor. {
    intros Hmax.
    destruct x. {
      destruct y.
      contradict Hmax; discriminate.
      apply CVMMinorRight; intuition.
      contradict Hmax; discriminate.
    } {
      destruct y.
      apply CVMMinorLeft; intuition.
      apply CVMMinorLeft; intuition.
      contradict Hmax; discriminate.
    } {
      destruct y.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
    }
  } {
    intros Hmax.
    destruct Hmax as [p q [Hp Hq]|p q [Hp Hq]]. {
      subst p.
      destruct Hq. {
        subst q. reflexivity.
      } {
        subst q. reflexivity.
      }
    } {
      subst q.
      destruct Hp. {
        subst p. reflexivity.
      } {
        subst p. reflexivity.
      }
    }
  }
Qed.

Fixpoint compatVersionChangesMaximum
  (rs : list compatVersionChange)
: compatVersionChange :=
  match rs with
  | nil       => CVersionChangeNone
  | cons x xs => compatVersionChangeMax x (compatVersionChangesMaximum xs)
  end.

Theorem compatVersionChangesMaximumCorrect0 : forall cs,
  In CVersionChangeMajor cs ->
    compatVersionChangesMaximum cs = CVersionChangeMajor.
Proof.
  induction cs as [|x xs]. {
    intros Hin.
    inversion Hin.
  } {
    intros Hin.
    destruct (in_inv Hin) as [HL|HR]. {
      subst x.
      simpl.
      reflexivity.
    } {
      pose proof (IHxs HR) as Hr.
      simpl.
      rewrite Hr.
      rewrite compatVersionChangeMaxComm.
      reflexivity.
    }
  }
Qed.

Theorem compatVersionChangesMaximumCorrect1 : forall cs,
  ~In CVersionChangeMajor cs ->
    compatVersionChangesMaximum cs <> CVersionChangeMajor.
Proof.
  intros cs.
  induction cs as [|x xs]. {
    intros Hnil.
    discriminate.
  } {
    intros Hnin.
    rewrite not_in_cons in Hnin.
    inversion Hnin as [HL HR].
    pose proof (IHxs HR) as Hind.
    simpl.
    destruct x. {
      destruct (compatVersionChangesMaximum xs). {
        discriminate.
      } {
        discriminate.
      } {
        contradict Hind.
        reflexivity.
      }
    } {
      destruct (compatVersionChangesMaximum xs). {
        discriminate.
      } {
        discriminate.
      } {
        contradict Hind.
        reflexivity.
      }
    } {
      contradict HL.
      reflexivity.
    }
  }
Qed.

Theorem compatVersionChangesMaximumCorrect2 : forall cs,
  ~In CVersionChangeMajor cs ->
    In CVersionChangeMinor cs ->
      compatVersionChangesMaximum cs = CVersionChangeMinor.
Proof.
  induction cs as [|x xs]. {
    intros Hnin Hin.
    inversion Hin.
  } {
    intros Hnin Hin.
    destruct (in_inv Hin) as [HL|HR]. {
      subst x.
      simpl.
      rewrite not_in_cons in Hnin.
      inversion Hnin as [HnL HnR].
      pose proof (compatVersionChangesMaximumCorrect1 _ HnR) as Hne.
      destruct (compatVersionChangesMaximum xs). {
        reflexivity.
      } {
        reflexivity.
      } {
        contradict Hne.
        reflexivity.
      }
    } {
      rewrite not_in_cons in Hnin.
      inversion Hnin as [HnL HnR].
      pose proof (IHxs HnR HR) as Hr.
      simpl.
      rewrite Hr.
      destruct x. {
        reflexivity.
      } {
        reflexivity.
      } {
        contradict HnL.
        reflexivity.
      }
    }
  }
Qed.

Theorem compatVersionChangesMaximumCorrect3 : forall cs,
  ~In CVersionChangeMajor cs ->
    ~In CVersionChangeMinor cs ->
      compatVersionChangesMaximum cs = CVersionChangeNone.
Proof.
  induction cs as [|x xs]. {
    intros Hnin0 Hnin1.
    reflexivity.
  } {
    intros Hnin0 Hnin1.
    simpl.
    rewrite not_in_cons in Hnin0.
    destruct Hnin0 as [HL0 HR0].
    rewrite not_in_cons in Hnin1.
    destruct Hnin1 as [HL1 HR1].
    rewrite (IHxs HR0 HR1).
    destruct x. {
      reflexivity.
    } {
      contradict HL1; reflexivity.
    } {
      contradict HL0; reflexivity.
    }
  }
Qed.

Definition compatVersionChangeRecordsMaximum
  (rs : list compatVersionChangeRecord)
: compatVersionChange :=
  compatVersionChangesMaximum (map (fun r => cvrChange r) rs).

5.8. Aurantium/Descriptor.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.

(** A descriptor string. *)
Definition descriptor := string.

(** The class of objects that can be described by descriptor strings. *)
Class describable (A : Set) := {
  descriptorOf : A -> descriptor
}.

Definition descriptorEqDec : forall (x y : descriptor),
  {x = y}+{x <> y}.
Proof.
  apply string_dec.
Qed.

5.9. Aurantium/Divisible8.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import PArith.PArith.
From Stdlib Require Import Arith.PeanoNat.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Lists.List.

(* Set Mangle Names. *)

(** The property of _x_ being divisible by 8. *)

Definition divisible8 (x : nat) : Prop :=
  modulo x 8 = 0.

(** If _x_ and _y_ are divisible by _z_, then _x + y_ is also divisible by _z_. *)

Theorem divisiblityNAdd : forall (x y z : nat),
  0 <> z -> x mod z = 0 -> y mod z = 0 -> (x + y) mod z = 0.
Proof.
  intros x y z Hz Hx Hy.
  destruct y as [|y].
    (* If y = 0, then this matches one of our assumptions already. *)
    rewrite Nat.add_0_r; exact Hx.
    (* Otherwise, the following property always holds given that the divisor is ≠ 0. *)
    assert ((x mod z + S y) mod z = (x + S y) mod z) as Heq.
      apply (Nat.Div0.add_mod_idemp_l x (S y) z).
    (* x mod z = 0 *)
    rewrite Hx in Heq.
    (* 0 + S y = S y *)
    rewrite Nat.add_0_l in Heq.
    rewrite <- Heq.
    exact Hy.
Qed.

(** Divisibility is preserved over addition. *)

Theorem divisibilityNFoldPlus : forall z xs,
  0 <> z ->
    Forall (fun n => n mod z = 0) xs ->
      (fold_right plus 0 xs) mod z = 0.
Proof.
  intros z xs Hnz HforAll.
  induction xs as [|y ys].
  - apply (Nat.Div0.mod_0_l z).
  - assert (fold_right add 0 (y :: ys) = y + fold_right add 0 ys) as Hfoldeq by reflexivity.
    rewrite Hfoldeq.
    assert (fold_right add 0 ys mod z = 0) as Hfoldeq2. {
      apply IHys.
      apply (@Forall_inv_tail nat (fun n : nat => n mod z = 0) y ys HforAll).
    }
    rewrite divisiblityNAdd.
    reflexivity.
    exact Hnz.
    apply (@Forall_inv nat (fun n : nat => n mod z = 0) y ys HforAll).
    exact Hfoldeq2.
Qed.

(** Divisibility is preserved over addition. *)

Theorem divisiblity8Add : forall (x y : nat),
  divisible8 x -> divisible8 y -> divisible8 (x + y).
Proof.
  intros x y Hx Hy.
  unfold divisible8 in *.
  apply divisiblityNAdd.
  discriminate.
  trivial.
  trivial.
Qed.

5.10. Aurantium/Hash.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.

Require Import Aurantium.Descriptor.

Local Open Scope string_scope.

Inductive hashAlgorithm : Set :=
  | HA_SHA256
  .

Theorem hashAlgorithmEqDec : forall (x y : hashAlgorithm),
  {x = y}+{x <> y}.
Proof.
  intros x.
  destruct x;
    (destruct y;
      try decide equality
    ).
Qed.

Definition hashAlgorithmDescribe (f : hashAlgorithm) : descriptor :=
  match f with
  | HA_SHA256   => "com.io7m.aurantium.sha2_256"
  end.

#[export]
Instance hashAlgorithmDescribable : describable hashAlgorithm := {
  descriptorOf h := hashAlgorithmDescribe h
}.

Inductive hashValue : Set := hashValueMake {
  hvAlgorithm : hashAlgorithm;
  hvValue     : string
}.

Theorem hashValueEqDec : forall (x y : hashValue),
  {x = y}+{x <> y}.
Proof.
  intros x.
  destruct x;
    (destruct y;
      try decide equality;
      try apply string_dec;
      try decide equality
    ).
Qed.

5.11. Aurantium/Identifier.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.

Local Open Scope string_scope.
Local Open Scope char_scope.

Inductive identifier : Set := identifierMake {
  idGroup             : string;
  idName              : string;
  idVersionMajor      : nat;
  idVersionMinor      : nat;
  idVersionMajorRange : idVersionMajor <= 4294967295;
  idVersionMinorRange : idVersionMinor <= 4294967295
}.

5.12. Aurantium/Interpolation.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Reals.Reals.
From Stdlib Require Import Reals.ROrderedType.
From Stdlib Require Import Psatz.

(* Set Mangle Names. *)

Local Open Scope R_scope.

(** A real number is normalized if it is in the range _[0, 1]_ *)
Definition isNormalized (x : R) : Prop :=
  0 <= x /\ x <= 1.

(** Normalization is preserved over multiplication. *)
Theorem isNormalizedMult : forall x y,
  isNormalized x -> isNormalized y -> isNormalized (Rmult x y).
Proof.
  intros x y [Hx0 Hx1] [Hy0 Hy1].
  unfold isNormalized.
  split.
  apply Rmult_le_pos.
  exact Hx0.
  exact Hy0.
  pose proof (Rmult_le_compat _ _ _ _ Hx0 Hy0 Hx1 Hy1) as Hcomp.
  assert (1 * 1 = 1) as Hobvious by apply (Rmult_1_r 1).
  rewrite <- Hobvious.
  exact Hcomp.
Qed.

(** Two real numbers that do not compare as equal according to
    a boolean comparison are not equal. *)
Lemma Reqb_neq : forall x y,
  Reqb x y = false -> x <> y.
Proof.
  intros x y Heqb.
  unfold not.
  intro Heq.
  rewrite Heq in Heqb.
  assert (Reqb y y = true) as Hbt. {
    rewrite Reqb_eq.
    reflexivity.
  }
  rewrite Heqb in Hbt.
  inversion Hbt.
Qed.

(** A supporting lemma that proves LTE ordering over division. *)
Lemma Rdiv_scale_0 : forall x y z,
  0 <= x
    -> 0 < z
      -> 0 < y
        -> x <= y <= z
          -> x / z <= x / y.
Proof.
  intros x y z H0x H0z H0y [Hxy Hyz].
  unfold Rdiv.
  assert (x * / z = / z * x) as H0 by apply Rmult_comm.
  assert (x * / y = / y * x) as H1 by apply Rmult_comm.
  rewrite H0; clear H0.
  rewrite H1; clear H1.
  apply Rmult_le_compat_r.
  apply H0x.
  apply Rle_Rinv.
  exact H0y.
  exact H0z.
  exact Hyz.
Qed.

(** A supporting lemma that proves LTE ordering over division. *)
Lemma Rdiv_le_1 : forall x y,
  0 <= x <= y ->
    0 < y ->
      x / y <= 1.
Proof.
  intros x y [H0x Hxy] H0y.
  unfold Rdiv.
  destruct (Rle_lt_or_eq_dec _ _ H0x) as [Hlt|Heq]. {
    assert (x / y <= x / x) as Hsc. {
      apply (Rdiv_scale_0 x x y H0x H0y Hlt).
      intuition.
    }
    unfold Rdiv in Hsc.
    rewrite <- Rinv_r_sym in Hsc.
    exact Hsc.
    unfold not.
    intro Hcontra.
    rewrite Hcontra in Hlt.
    pose proof (Rlt_irrefl 0) as Hcontra2.
    contradiction.
  } {
    rewrite <- Heq.
    rewrite Rmult_0_l.
    intuition.
  }
Qed.

(**
  The _between_ function returns the amount by which _x_ is
  "between" _y_ and _z_. If the function returns 1, _x = z_.
  If the function returns 0, _x = y_. If the function returns
  0.5, _x_ is exactly halfway between _y_ and _z_.

  If _low = high_, the function returns _x_ unchanged. Arguably,
  a silly question yields a silly answer.
*)

Definition between
  (x    : R)
  (low  : R)
  (high : R)
: R :=
  let n := x - low in
  let d := high - low in
    match Reqb d 0 with
    | true  => x
    | false => n / d
    end.

(** The _between_ function should yield normalized results. *)
Theorem betweenNorm : forall x lo hi,
  lo < hi
    -> lo <= x <= hi
      -> isNormalized (between x lo hi).
Proof.
  intros x lo hi Hlohi [Hlox Hxhi].
  unfold isNormalized.
  unfold between.
  destruct (Reqb (hi - lo) 0) eqn:Heqb. {
    rewrite R_as_OT.eqb_eq in Heqb.
    pose proof (Rlt_Rminus _ _ Hlohi) as Hlt.
    pose proof (Rlt_not_eq _ _ Hlt) as Hneq.
    symmetry in Heqb.
    contradiction.
  } {
    pose proof (Reqb_neq _ _ Heqb) as Heq.
    clear Heqb.
    assert ((x - lo) <= (hi - lo)) as Hrle by lra.
    destruct (Rtotal_order (hi - lo) 0) as [Hlt0|[Hfalse|Hgt0]]. {
      pose proof (Rminus_lt _ _ Hlt0) as Hcontra.
      pose proof (Rlt_asym _ _ Hcontra) as Hfalse.
      contradiction.
    } {
      contradiction.
    } {
      pose proof (Rgt_lt _ _ Hgt0) as H0lt.
      assert (0 <= x - lo) as H0le by lra.
      constructor. {
        apply (Rle_mult_inv_pos _ _ H0le H0lt).
      } {
        assert (0 <= x - lo <= hi - lo) as Hmx by lra.
        apply (Rdiv_le_1 (x-lo) (hi-lo) Hmx H0lt).
      }
    }
  }
Qed.

(** Linearly interpolate between _x_ and _y_ by the (normalized)
    factor _f_. *)
Definition interpolate
  (x : R)
  (y : R)
  (f : R)
: R :=
  (x * (1 - f)) + (y * f).

(** If the interpolation factor is normalized, then _interpolate_
    always returns a value in _[x, y]_. *)
Lemma interpolateRange1 : forall x y f,
  x <= y
    -> isNormalized f
      -> x <= interpolate x y f <= y.
Proof.
  intros x y f Hxy [Hnf0 Hnf1].

  unfold interpolate.
  constructor. {
    replace x with (x * (1 - f) + x * f) at 1 by lra.
    eapply Rplus_le_compat. {
      apply Rle_refl.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      exact Hxy.
    }
  } {
    replace y with (y * (1 - f) + y * f) at 2 by lra.
    eapply Rplus_le_compat. {
      apply Rmult_le_compat_r.
      lra.
      exact Hxy.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      apply Rle_refl.
    }
  }
Qed.

(** If the interpolation factor is normalized, then _interpolate_
    always returns a value in _[x, y]_. *)
Lemma interpolateRange2 : forall x y f,
  y <= x
    -> isNormalized f
      -> y <= interpolate x y f <= x.
Proof.
  intros x y f Hyx [Hnf0 Hnf1].

  unfold interpolate.
  constructor. {
    replace y with (y * (1 - f) + y * f) at 1 by lra.
    eapply Rplus_le_compat. {
      apply Rmult_le_compat_r.
      lra.
      exact Hyx.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      apply Rle_refl.
    }
  } {
    replace x with (x * (1 - f) + x * f) at 2 by lra.
    eapply Rplus_le_compat. {
      apply Rle_refl.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      exact Hyx.
    }
  }
Qed.

5.13. Aurantium/Intersection.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Lists.List.

(** Return the set of elements that are in both _ea_ and _eb_, according to the
    find function _f_. *)
Fixpoint intersectionPairs
  {A     : Set}
  (f     : A -> list A -> option A)
  (ea eb : list A)
: list (A * A) :=
  match ea with
  | nil => nil
  | cons a ea_rest =>
    match f a eb with
    | Some r => (a, r) :: intersectionPairs f ea_rest eb
    | None   =>           intersectionPairs f ea_rest eb
    end
  end.

(** The description of a "find" function; if _f_ applied to _x_ yields _y_,
    then _y_ must have been in _ys_. *)
Definition finds
  {A  : Set}
  (f  : A -> list A -> option A)
  (x  : A)
  (y  : A)
  (ys : list A)
: Prop :=
  f x ys = Some y <-> In y ys.

(** A proof of correctness for the _intersectionPairs_ function. *)
Theorem intersectionPairsIn : forall (A : Set) (ea eb : list A) efa efb f,
  (forall x y ys, finds f x y ys) ->
    In (efa, efb) (intersectionPairs f ea eb) ->
      In efa ea /\ In efb eb.
Proof.
  intros A ea.
  induction ea as [|a ea_rest]. {
    intros eb efa efb f Hfind Hin.
    inversion Hin.
  } {
    intros eb efa efb f Hfind Hin.
    simpl in Hin.
    destruct (f a eb) eqn:Haf. {
      destruct (in_inv Hin) as [Hin0|Hin1]. {
        assert (a = efa) by congruence.
        assert (a0 = efb) by congruence.
        subst a.
        subst a0.
        constructor.
        constructor; reflexivity.
        unfold finds in Hfind.
        rewrite (Hfind efa efb eb) in Haf.
        exact Haf.
      } {
        pose proof (IHea_rest eb efa efb f Hfind Hin1) as H0.
        intuition.
      }
    } {
      pose proof (IHea_rest eb efa efb f Hfind Hin) as H0.
      intuition.
    }
  }
Qed.

5.14. Aurantium/Json.v

(*
 * Copyright © 2025 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Numbers.DecimalString.
From Stdlib Require Import Lists.List.

Local Open Scope string_scope.

Import ListNotations.

(** A JSON expression. *)
Inductive json : Set :=
  (** A boolean constant. *)
  | JsonBoolean : bool -> json
  (** An integer constant. *)
  | JsonInteger : nat -> json
  (** A floating point constant. *)
  | JsonFloat   : json
  (** A string constant. *)
  | JsonString  : string -> json
  (** An object. *)
  | JsonObject  : list (string * json) -> json
  (** An array. *)
  | JsonArray   : list json -> json
  .

(** The string representation of a boolean. *)
Definition boolString (b : bool) : string :=
  match b with
  | true  => "true"
  | false => "false"
  end.

(** The string representation of an integer. *)
Definition string_of_nat (n : nat) : string :=
  NilZero.string_of_uint (Nat.to_uint n).

(** The tokens that make up a serialized JSON expression. *)
Inductive jsonToken : Set :=
  | JTTrue        : jsonToken
  | JTFalse       : jsonToken
  | JTInteger     : nat -> jsonToken
  | JTFloat       : jsonToken
  | JTString      : string -> jsonToken
  | JTObjectStart : jsonToken
  | JTObjectEnd   : jsonToken
  | JTColon       : jsonToken
  | JTComma       : jsonToken
  | JTArrayStart  : jsonToken
  | JTArrayEnd    : jsonToken
  .

(** Insert comma tokens between each element of the list. *)
Fixpoint jsonComma (ss : list (list jsonToken)) : list jsonToken :=
  match ss with
  | []        => []
  | (x :: []) => x
  | (x :: xs) => x ++ JTComma :: (jsonComma xs)
  end.

(** An example empty object. *)
Example objectEmpty0 :=
  JsonObject [

  ].

(** An example simple object. *)
Example objectSimple0 :=
  JsonObject [
    ("x", JsonInteger 23);
    ("y", JsonInteger 24);
    ("z", JsonInteger 25)
  ].

(** An example simple array. *)
Example arraySimple0 :=
  JsonArray [
    (JsonInteger 23);
    (JsonInteger 24);
    (JsonInteger 25)
  ].

(** Serialize a JSON expression to a list of JSON tokens. *)
Fixpoint jsonSerialize (j : json) : list jsonToken :=
  match j with
  | JsonBoolean true  => [JTTrue]
  | JsonBoolean false => [JTFalse]
  | JsonInteger n     => [JTInteger n]
  | JsonFloat         => [JTFloat]
  | JsonString s      => [JTString s]
  | JsonObject o      =>
    let props := map (fun p => JTString (fst p) :: JTColon :: jsonSerialize (snd p)) o in
      JTObjectStart :: (jsonComma props) ++ [JTObjectEnd]
  | JsonArray a       =>
    let values := map jsonSerialize a in
      JTArrayStart :: (jsonComma values) ++ [JTArrayEnd]
  end.

(** Convert a JSON token to a string. *)
Definition jsonStringOne (t : jsonToken) : string :=
  match t with
  | JTTrue        => "true"
  | JTFalse       => "false"
  | JTInteger n   => string_of_nat n
  | JTFloat       => "#"
  | JTString s    => """" ++ s ++ """"
  | JTObjectStart => "{"
  | JTObjectEnd   => "}"
  | JTColon       => ":"
  | JTComma       => ","
  | JTArrayStart  => "["
  | JTArrayEnd    => "]"
  end.

(** Serialize a JSON expression to a string. *)
Definition jsonSerializeString (j : json) : string :=
  let tokens := jsonSerialize j in
  let texts  := map jsonStringOne tokens in
    fold_left append texts "".

5.15. Aurantium/JsonData.v

(*
 * Copyright © 2025 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Numbers.DecimalString.
From Stdlib Require Import Lists.List.
From Stdlib Require Import Reals.Reals.

Local Open Scope R_scope.
Local Open Scope string_scope.

Import ListNotations.

Require Import Aurantium.Hash.
Require Import Aurantium.Metadata.
Require Import Aurantium.OctetOrder.
Require Import Aurantium.Json.
Require Import Aurantium.Clip.
Require Import Aurantium.KeyMapping.

Definition float (r : R) :=
  JsonFloat.

Definition flagJson (f : keyAssignmentFlag) : json :=
  JsonString (keyAssignmentFlagDescribe f).

(** The JSON encoding of a key assignment. *)
Definition jsonKeyAssignment (k : keyAssignment) : json :=
  JsonObject [
    ("ID",                        JsonInteger (kaId k));
    ("KeyValueStart",             JsonInteger (kaValueStart k));
    ("KeyValueCenter",            JsonInteger (kaValueCenter k));
    ("KeyValueEnd",               JsonInteger (kaValueEnd k));
    ("ClipID",                    JsonInteger (kaClipId k));
    ("AmplitudeAtKeyStart",       float (kaAmplitudeAtKeyStart k));
    ("AmplitudeAtKeyCenter",      float (kaAmplitudeAtKeyCenter k));
    ("AmplitudeAtKeyEnd",         float (kaAmplitudeAtKeyEnd k));
    ("AtVelocityStart",           float (kaAtVelocityStart k));
    ("AtVelocityCenter",          float (kaAtVelocityCenter k));
    ("AtVelocityEnd",             float (kaAtVelocityEnd k));
    ("AmplitudeAtVelocityStart",  float (kaAmplitudeAtVelocityStart k));
    ("AmplitudeAtVelocityCenter", float (kaAmplitudeAtVelocityCenter k));
    ("AmplitudeAtVelocityEnd",    float (kaAmplitudeAtVelocityEnd k));
    ("Flags",                     JsonArray (map flagJson (kaFlags k)))
  ].

(** The JSON encoding of a set of key assignments. *)
Definition jsonKeyAssignments (ks : list keyAssignment) : json :=
  JsonObject [
    ("%Schema", JsonString "urn:com.io7m.aurantium:1.0");
    ("Clips",   JsonArray (map jsonKeyAssignment ks))
  ].

(** The JSON encoding of a hash value. *)
Definition jsonHash (h : hashValue) : json :=
  JsonObject [
    ("Algorithm", JsonString (hashAlgorithmDescribe (hvAlgorithm h)));
    ("Value",     JsonString (hvValue h))
  ].

(** The JSON encoding of a loop range. *)
Definition jsonLoopRange (lr : loopRange) : json :=
  JsonObject [
    ("FrameStart",        JsonInteger (lrFrameStart lr));
    ("FrameEndInclusive", JsonInteger (lrFrameEndInclusive lr))
  ].

(** The JSON encoding of an optional loop range. *)
Definition jsonLoopRangeOptionProperty (lr : option loopRange) : list (string * json) :=
  match lr with
  | Some l => [("LoopRange", jsonLoopRange l)]
  | None   => []
  end.

(** The JSON encoding of a clip description. *)
Definition jsonClip (c : clip) : json :=
  JsonObject (app [
    ("ID",           JsonInteger (clipId c));
    ("Name",         JsonString (clipName c));
    ("Format",       JsonString (audioFormatDescribe (clipFormat c)));
    ("SampleRate",   JsonInteger (clipSampleRate c));
    ("SampleDepth",  JsonInteger (clipSampleDepth c));
    ("Channels",     JsonInteger (clipChannels c));
    ("Endianness",   JsonString (octetOrderDescribe (clipEndianness c)));
    ("Hash",         jsonHash (clipHash c));
    ("Offset",       JsonInteger (clipOffset c));
    ("Size",         JsonInteger (clipSize c))
  ] (jsonLoopRangeOptionProperty (clipLoopRange c))).

(** The JSON encoding of a set of clip descriptions. *)
Definition jsonClips (c : list clip) : json :=
  JsonObject [
    ("%Schema", JsonString "urn:com.io7m.aurantium:1.0");
    ("Clips",   JsonArray (map jsonClip c))
  ].

(** The JSON encoding of a list of metadata values. *)
Definition jsonMetadataM (mvs : list metadataValue) : json :=
  JsonObject (map (fun k => (mKey k, JsonString (mValue k))) mvs).

(** The JSON encoding of a list of metadata values. *)
Definition jsonMetadata (m : metadata) : json :=
  JsonObject [
    ("%Schema",  JsonString "urn:com.io7m.aurantium:1.0");
    ("Metadata", jsonMetadataM (mValues m))
  ].

5.16. Aurantium/KeyMapping.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Lists.List.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Arith.Peano_dec.
From Stdlib Require Import Arith.PeanoNat.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.
From Stdlib Require Import Reals.Reals.
From Stdlib Require Import Reals.ROrderedType.

From Stdlib Require Import Psatz.

Require Import Aurantium.Compatibility.
Require Import Aurantium.Intersection.
Require Import Aurantium.Interpolation.
Require Import Aurantium.Descriptor.

Local Open Scope R_scope.
Local Open Scope string_scope.

Import ListNotations.

(* Set Mangle Names. *)

(** The type of key assignment flags.*)
Inductive keyAssignmentFlag : Set :=
  (** The key assignment should treat the clip as unpitched. *)
  | FlagUnpitched : keyAssignmentFlag.

Definition keyAssignmentFlagDescribe (f : keyAssignmentFlag) : descriptor :=
  match f with
  | FlagUnpitched   => "com.io7m.aurantium.unpitched"
  end.

#[export]
Instance keyAssignmentFlagDescribable : describable keyAssignmentFlag := {
  descriptorOf f := keyAssignmentFlagDescribe f
}.

(** Key assignment equality is decidable. *)
Theorem keyAssignmentFlagEqDec
  (x y : keyAssignmentFlag)
: {x = y}+{~x = y}.
Proof. decide equality. Qed.

(**
  A key assignment assigns a clip to a range of keys, and describes
  the amplitude of the clip based on the velocity of the incoming
  note, and the position of the key within the key range.

  A clip that should not vary in amplitude can simply assign a
  value of 1.0 for all values.
*)

Inductive keyAssignment : Set := {
  (** The unique identifier of the key assignment. *)
  kaId : nat;
  (** The lowest key value that will trigger this clip. *)
  kaValueStart : nat;
  (** The key value at which the clip plays at the normal playback rate. *)
  kaValueCenter: nat;
  (** The highest key value that will trigger this clip. *)
  kaValueEnd : nat;
  kaValueEndRange : le kaValueEnd 294967295;
  (** The key values must be ordered. *)
  kaValueStartOrder : le kaValueStart kaValueCenter;
  kaValueCenterOrder : le kaValueCenter kaValueEnd;
  (** The clip that will be triggered. *)
  kaClipId : nat;
  (** The amplitude at which this clip will be played when at the lowest key value. *)
  kaAmplitudeAtKeyStart : R;
  (** The amplitude at which this clip will be played when at the center key value. *)
  kaAmplitudeAtKeyCenter : R;
  (** The amplitude at which this clip will be played when at the highest key value. *)
  kaAmplitudeAtKeyEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtKeyStartNormal : isNormalized kaAmplitudeAtKeyStart;
  kaAmplitudeAtKeyCenterNormal : isNormalized kaAmplitudeAtKeyCenter;
  kaAmplitudeAtKeyEndNormal : isNormalized kaAmplitudeAtKeyEnd;
  (** The velocity value at which this clip starts to be triggered. *)
  kaAtVelocityStart : R;
  (** The velocity value at which the amplitude of this clip is at maximum. *)
  kaAtVelocityCenter : R;
  (** The velocity value at which this clip stops being triggered. *)
  kaAtVelocityEnd : R;
  (** The velocity values are normalized values and are correctly ordered. *)
  kaAtVelocityStartNormal : isNormalized kaAtVelocityStart;
  kaAtVelocityCenterNormal : isNormalized kaAtVelocityCenter;
  kaAtVelocityEndNormal : isNormalized kaAtVelocityEnd;
  kaAtVelocityStartOrder : kaAtVelocityStart <= kaAtVelocityCenter;
  kaAtVelocityCenterOrder : kaAtVelocityCenter <= kaAtVelocityEnd;
  (** The amplitude at which this clip will be played when at the starting velocity value. *)
  kaAmplitudeAtVelocityStart : R;
  (** The amplitude at which this clip will be played when at the center velocity value. *)
  kaAmplitudeAtVelocityCenter : R;
  (** The amplitude at which this clip will be played when at the end velocity value. *)
  kaAmplitudeAtVelocityEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtVelocityStartNormal : isNormalized kaAmplitudeAtVelocityStart;
  kaAmplitudeAtVelocityCenterNormal : isNormalized kaAmplitudeAtVelocityCenter;
  kaAmplitudeAtVelocityEndNormal : isNormalized kaAmplitudeAtVelocityEnd;
  (** The associated key assignment flags. *)
  kaFlags : list keyAssignmentFlag;
  kaFlagsUnique : NoDup kaFlags;
}.

(** The values that make two key assignments "equal". *)
Definition keyAssignmentValuesEq (x y : keyAssignment) : Prop :=
     (kaId x)                        = (kaId y)
  /\ (kaValueStart x)                = (kaValueStart y)
  /\ (kaValueCenter x)               = (kaValueCenter y)
  /\ (kaValueEnd x)                  = (kaValueEnd y)
  /\ (kaClipId x)                    = (kaClipId y)
  /\ (kaAmplitudeAtKeyStart x)       = (kaAmplitudeAtKeyStart y)
  /\ (kaAmplitudeAtKeyCenter x)      = (kaAmplitudeAtKeyCenter y)
  /\ (kaAmplitudeAtKeyEnd x)         = (kaAmplitudeAtKeyEnd y)
  /\ (kaAtVelocityStart x)           = (kaAtVelocityStart y)
  /\ (kaAtVelocityCenter x)          = (kaAtVelocityCenter y)
  /\ (kaAtVelocityEnd x)             = (kaAtVelocityEnd y)
  /\ (kaAmplitudeAtVelocityStart x)  = (kaAmplitudeAtVelocityStart y)
  /\ (kaAmplitudeAtVelocityCenter x) = (kaAmplitudeAtVelocityCenter y)
  /\ (kaAmplitudeAtVelocityEnd x)    = (kaAmplitudeAtVelocityEnd y)
  /\ (kaFlags x)                     = (kaFlags y)
.

(** The proposition that describes how two key assignments can overlap. *)
Definition keyAssignmentsOverlap (x y : keyAssignment) : Prop :=
  let x1 := kaValueStart x in
  let x2 := kaValueEnd x in
  let y1 := kaValueStart y in
  let y2 := kaValueEnd y in
    ge x2 y1 /\ ge y2 x1.

(** Overlapping is reflexive. An object always overlaps itself. *)
Theorem keyAssignmentsOverlapReflexive : forall x,
  keyAssignmentsOverlap x x.
Proof.
  intros x.
  unfold keyAssignmentsOverlap.
  unfold ge.
  pose proof (kaValueStartOrder x) as H0.
  pose proof (kaValueCenterOrder x) as H1.
  intuition.
Qed.

(** Overlapping is commutative. *)
Theorem keyAssignmentsOverlapCommutative : forall x y,
  keyAssignmentsOverlap x y -> keyAssignmentsOverlap y x.
Proof.
  intros x y.
  unfold keyAssignmentsOverlap.
  unfold ge.
  pose proof (kaValueStartOrder x) as H0.
  pose proof (kaValueCenterOrder x) as H1.
  pose proof (kaValueStartOrder y) as H2.
  pose proof (kaValueCenterOrder y) as H3.
  intuition.
Qed.

Lemma nat_le_dec : forall n m,
  {le n m}+{~le n m}.
Proof.
  intros n m.
  destruct (Compare.le_dec n m) as [HL0|HR0]. {
    intuition.
  } {
    destruct (Nat.eq_dec n m); intuition.
  }
Qed.

(** Determining overlap is decidable. *)
Theorem keyAssignmentsOverlapDecidable : forall x y,
  {keyAssignmentsOverlap x y}+{~keyAssignmentsOverlap x y}.
Proof.
  intros x y.
  unfold keyAssignmentsOverlap.
  unfold ge.
  pose proof (kaValueStartOrder x) as H0.
  pose proof (kaValueCenterOrder x) as H1.
  pose proof (kaValueStartOrder y) as H2.
  pose proof (kaValueCenterOrder y) as H3.
  destruct (nat_le_dec (kaValueStart y) (kaValueEnd x)) as [HL0|HR0].
  destruct (nat_le_dec (kaValueStart x) (kaValueEnd y)) as [HL1|HR1].
  intuition.
  right; intuition.
  right; intuition.
Qed.

(** Determine the list of key assignments that overlap _k_ (but that are not _k_). *)
Definition keyAssignmentsOverlapping
  (k  : keyAssignment)
  (ka : list keyAssignment)
: list keyAssignment :=
  filter (fun j =>
    match keyAssignmentsOverlapDecidable k j with
    | left _ =>
      match Nat.eq_dec (kaId k) (kaId j) with
      | left _  => false
      | right _ => true
      end
    | right _ => false
    end) ka.

(** The _keyAssignmentsOverlapping_ function never returns _k_. *)
Theorem keyAssignmentsOverlappingNotSelf : forall k ka,
  ~In k (keyAssignmentsOverlapping k ka).
Proof.
  intros k ka.
  unfold keyAssignmentsOverlapping.
  rewrite filter_In.
  destruct (keyAssignmentsOverlapDecidable k k) as [HodT|HodF]. {
    destruct (Nat.eq_dec (kaId k) (kaId k)) as [HeT|HeF]. {
      intuition.
    } {
      contradict HeF. reflexivity.
    }
  } {
    contradict HodF.
    apply keyAssignmentsOverlapReflexive.
  }
Qed.

(** The _keyAssignmentsOverlapping_ function finds overlapping assignments. *)
Theorem keyAssignmentsOverlappingFind0 : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    -> In p (keyAssignmentsOverlapping k ka).
Proof.
  intros k ka p [HinP [Hover Hneq]].
  unfold keyAssignmentsOverlapping.
  rewrite filter_In.
  destruct (keyAssignmentsOverlapDecidable k p) as [HodT|HodF]. {
    destruct (Nat.eq_dec (kaId k) (kaId p)) as [HeT|HeF]. {
      intuition.
    } {
      intuition.
    }
  } {
    contradiction.
  }
Qed.

(** The _keyAssignmentsOverlapping_ function finds overlapping assignments. *)
Theorem keyAssignmentsOverlappingFind1 : forall k ka p,
  In p (keyAssignmentsOverlapping k ka) ->
    In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p).
Proof.
  intros k ka p HinP.
  unfold keyAssignmentsOverlapping in HinP.
  rewrite filter_In in HinP.
  destruct (keyAssignmentsOverlapDecidable k p) as [HodT|HodF]. {
    destruct (Nat.eq_dec (kaId k) (kaId p)) as [HeT|HeF]. {
      intuition.
    } {
      intuition.
    }
  } {
    destruct HinP as [HL HR].
    contradict HR.
    discriminate.
  }
Qed.

(** The _keyAssignmentsOverlapping_ function finds overlapping assignments. *)
Theorem keyAssignmentsOverlappingFind : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    <-> In p (keyAssignmentsOverlapping k ka).
Proof.
  constructor.
  apply keyAssignmentsOverlappingFind0.
  apply keyAssignmentsOverlappingFind1.
Qed.

(** Whether two key assignments are "equal" is decidable. *)
Theorem keyAssignmentValuesEqDec
  (x y : keyAssignment)
: {keyAssignmentValuesEq x y}+{~keyAssignmentValuesEq x y}.
Proof.
  unfold keyAssignmentValuesEq.
  destruct (Nat.eq_dec (kaId x) (kaId y)).
  destruct (Nat.eq_dec (kaValueStart x) (kaValueStart y)).
  destruct (Nat.eq_dec (kaValueCenter x) (kaValueCenter y)).
  destruct (Nat.eq_dec (kaValueEnd x) (kaValueEnd y)).
  destruct (Nat.eq_dec (kaClipId x) (kaClipId y)).
  destruct (Req_dec (kaAmplitudeAtKeyStart x) (kaAmplitudeAtKeyStart y)).
  destruct (Req_dec (kaAmplitudeAtKeyCenter x) (kaAmplitudeAtKeyCenter y)).
  destruct (Req_dec (kaAmplitudeAtKeyEnd x) (kaAmplitudeAtKeyEnd y)).
  destruct (Req_dec (kaAtVelocityStart x) (kaAtVelocityStart y)).
  destruct (Req_dec (kaAtVelocityCenter x) (kaAtVelocityCenter y)).
  destruct (Req_dec (kaAtVelocityEnd x) (kaAtVelocityEnd y)).
  destruct (Req_dec (kaAmplitudeAtVelocityStart x) (kaAmplitudeAtVelocityStart y)).
  destruct (Req_dec (kaAmplitudeAtVelocityCenter x) (kaAmplitudeAtVelocityCenter y)).
  destruct (Req_dec (kaAmplitudeAtVelocityEnd x) (kaAmplitudeAtVelocityEnd y)).
  destruct (list_eq_dec keyAssignmentFlagEqDec (kaFlags x) (kaFlags y)).
  left; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
Qed.

(** The property that states the conditions under which a key assignment
    matches a key and velocity. *)
Definition keyAssignmentMatches
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: Prop :=
  let p0 := ((kaValueStart assignment) <= key)%nat in
  let p1 := (key <= (kaValueEnd assignment))%nat in
  let p2 := ((kaAtVelocityStart assignment) <= velocity)%R in
  let p3 := (velocity <= (kaAtVelocityEnd assignment))%R in
    p0 /\ p1 /\ p2 /\ p3.

Close Scope R_scope.

Lemma keyAssignmentNoMatchKeyTooLow : forall k v a,
  k < (kaValueStart a) -> ~keyAssignmentMatches k v a.
Proof.
  intros k v a Hlt.
  unfold not; intro Hcontra; inversion Hcontra.
  intuition.
Qed.

Lemma keyAssignmentNoMatchKeyTooHigh : forall k v a,
  (kaValueEnd a) < k -> ~keyAssignmentMatches k v a.
Proof.
  intros k v a Hlt.
  unfold not; intro Hcontra; inversion Hcontra.
  intuition.
Qed.

Local Open Scope R_scope.

Lemma keyAssignmentNoMatchVelocityTooLow : forall k v a,
  v < (kaAtVelocityStart a) -> ~keyAssignmentMatches k v a.
Proof.
  intros k v a Hlt.
  unfold not; intro Hcontra; inversion Hcontra.
  intuition.
  lra.
Qed.

Lemma keyAssignmentNoMatchVelocityTooHigh : forall k v a,
  (kaAtVelocityEnd a) < v -> ~keyAssignmentMatches k v a.
Proof.
  intros k v a Hlt.
  unfold not; intro Hcontra; inversion Hcontra.
  intuition.
  lra.
Qed.

(** Whether or not a key assignment matches is decidable. *)
Theorem keyAssignmentMatchesDecidable : forall k v a,
  {keyAssignmentMatches k v a}+{~keyAssignmentMatches k v a}.
Proof.
  intros k v a.
  destruct (Compare_dec.le_dec (kaValueStart a) k) as [HksL|HksR]. {
    destruct (Compare_dec.le_dec k (kaValueEnd a)) as [HkeL|HkeR]. {
      destruct (Rle_dec (kaAtVelocityStart a) v) as [HvsL|HvsR]. {
        destruct (Rle_dec v (kaAtVelocityEnd a)) as [HveL|HveR]. {
          left; constructor; auto.
        } {
          right.
          apply keyAssignmentNoMatchVelocityTooHigh.
          apply Rnot_le_lt. exact HveR.
        }
      } {
        right.
        apply keyAssignmentNoMatchVelocityTooLow.
        apply Rnot_le_lt. exact HvsR.
      }
    } {
      right.
      apply keyAssignmentNoMatchKeyTooHigh.
      rewrite Nat.nle_gt in HkeR. exact HkeR.
    }
  } {
    right.
    apply keyAssignmentNoMatchKeyTooLow.
    rewrite Nat.nle_gt in HksR. exact HksR.
  }
Qed.

(**
  The result of evaluating a single key assignment.

  When a key is evaluated, a playback rate is returned which is then used by
  applications to speed up or slow down clip playback in order to affect the
  perceived pitch.

  Evaluation also returns a pair of amplitude values. One amplitude is based
  upon the velocity of the original note; this change in amplitude can be used
  by audio map authors to allow instruments to vary their timbre based on how
  soft or hard a note is hit. The other amplitude is based on the key; this
  change in amplitude can be used by audio map authors to allow instruments
  to vary their timbre based on the pitches of notes.

  Normally, applications will multiply these two amplitude values to produce
  a final normalized amplitude.
*)

Inductive keyEvaluation : Set := keyEvaluationMake {
  keyEvaluationClipId                  : nat;
  keyEvaluationVelocityAmplitude       : R;
  keyEvaluationVelocityAmplitudeNormal : isNormalized keyEvaluationVelocityAmplitude;
  keyEvaluationKeyAmplitude            : R;
  keyEvaluationKeyAmplitudeNormal      : isNormalized keyEvaluationKeyAmplitude;
  keyEvaluationRate                    : R;
  keyEvaluationRateNonNegative         : 0 <= keyEvaluationRate
}.

(** Evaluate the amplitude of the given key assignment based on
    the velocity. *)

Definition keyAssignmentEvaluateAmplitudeForVelocity
  (velocity   : R)
  (assignment : keyAssignment)
: R :=
  let kLow := kaAtVelocityStart assignment in
  let kMid := kaAtVelocityCenter assignment in
  let kTop := kaAtVelocityEnd assignment in
    match Rcompare velocity kMid with
    | Eq => kaAmplitudeAtVelocityCenter assignment
    | Lt =>
      match Rlt_dec kLow kMid with
      | left _ =>
        let f := between velocity kLow kMid in
          interpolate
            (kaAmplitudeAtVelocityStart assignment)
            (kaAmplitudeAtVelocityCenter assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    | Gt =>
      match Rlt_dec kMid kTop with
      | left _ =>
        let f := between velocity kMid kTop in
          interpolate
            (kaAmplitudeAtVelocityCenter assignment)
            (kaAmplitudeAtVelocityEnd assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    end.

(** Either _x <= y_ or _y <= x_. *)
Lemma Rle_or : forall x y,
  x <= y \/ y <= x.
Proof.
  intros x y.
  destruct (Rle_lt_dec x y) as [HL|HR]. {
    left; exact HL.
  } {
    right; apply Rlt_le; exact HR.
  }
Qed.

(**
  The amplitude returned by evaluating a key assignment based on
  velocity is always normalized.
*)
Theorem keyAssignmentEvaluateAmplitudeForVelocityNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForVelocity v a).
Proof.
  intros k v a [Hm0 [Hm1 [Hm2 Hm3]]].
  unfold isNormalized.

  unfold keyAssignmentEvaluateAmplitudeForVelocity.
  destruct (Rcompare_spec v (kaAtVelocityCenter a)) as [H0|H1|H2]. {
    (* v = center *)
    destruct (kaAmplitudeAtVelocityCenterNormal a) as [Hk0 Hk1].
    lra.
  } {
    (* v < center *)
    destruct (kaAmplitudeAtVelocityStartNormal a) as [Hk0 Hk1].
    destruct (kaAmplitudeAtVelocityCenterNormal a) as [Hk2 Hk3].
    remember (kaAtVelocityStart a) as kVs.
    remember (kaAtVelocityCenter a) as kVc.
    remember (kaAmplitudeAtVelocityStart a) as kAVs.
    remember (kaAmplitudeAtVelocityCenter a) as kAVc.

    remember (between v kVs kVc) as f.
    assert (kVs <= kVc) as Hscle by lra.

    destruct (Rle_or kAVs kAVc) as [HL|HR]. {
      destruct (Rlt_dec kVs kVc) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVs kVc Hlt).
          lra.
        }
        pose proof (interpolateRange1 kAVs kAVc f HL Hnormf).
        lra.
      } {
        lra.
      }
    } {
      destruct (Rlt_dec kVs kVc) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVs kVc Hlt).
          lra.
        }
        pose proof (interpolateRange2 _ _ _ HR Hnormf).
        lra.
      } {
        lra.
      }
    }
  } {
    (* center < v *)
    destruct (kaAmplitudeAtVelocityCenterNormal a) as [Hk0 Hk1].
    destruct (kaAmplitudeAtVelocityEndNormal a) as [Hk2 Hk3].
    remember (kaAtVelocityCenter a) as kVc.
    remember (kaAtVelocityEnd a) as kVe.
    remember (kaAmplitudeAtVelocityCenter a) as kAVc.
    remember (kaAmplitudeAtVelocityEnd a) as kAVe.

    remember (between v kVc kVe) as f.
    assert (kVc <= kVe) as Hcele by lra.

    destruct (Rle_or kAVc kAVe) as [HL|HR]. {
      destruct (Rlt_dec kVc kVe) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVc kVe Hlt).
          lra.
        }
        pose proof (interpolateRange1 kAVc kAVe f HL Hnormf).
        lra.
      } {
        lra.
      }
    } {
      destruct (Rlt_dec kVc kVe) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVc kVe Hlt).
          lra.
        }
        pose proof (interpolateRange2 _ _ _ HR Hnormf).
        lra.
      } {
        lra.
      }
    }
  }
Qed.

(** Evaluate the amplitude of the given key assignment based on
    the key. *)
Definition keyAssignmentEvaluateAmplitudeForKey
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  let kLow := kaValueStart assignment in
  let kMid := kaValueCenter assignment in
  let kTop := kaValueEnd assignment in
    match Nat.compare key kMid with
    | Eq => kaAmplitudeAtKeyCenter assignment
    | Lt =>
      match Compare_dec.lt_dec kLow kMid with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kLow) (INR kMid) in
          interpolate
            (kaAmplitudeAtKeyStart assignment)
            (kaAmplitudeAtKeyCenter assignment)
            f
      end
    | Gt =>
      match Compare_dec.lt_dec kMid kTop with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kMid) (INR kTop) in
          interpolate
            (kaAmplitudeAtKeyCenter assignment)
            (kaAmplitudeAtKeyEnd assignment)
            f
      end
    end.

(**
  The amplitude returned by evaluating a key assignment based on
  key is always normalized.
*)
Theorem keyAssignmentEvaluateAmplitudeForKeyNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForKey k a).
Proof.
  intros k v a [Hm0 [Hm1 [Hm2 Hm3]]].
  unfold isNormalized.

  unfold keyAssignmentEvaluateAmplitudeForKey.
  destruct (Nat.compare_spec k (kaValueCenter a)) as [Heq|Hlt|Hgt]. {
    destruct (kaAmplitudeAtKeyCenterNormal a).
    lra.
  } {
    (* k < center *)
    (* Abbreviations to make the proof context readable. *)
    remember (kaValueStart a) as ks.
    remember (kaValueCenter a) as kc.
    remember (kaAmplitudeAtKeyStart a) as kAKs.
    remember (kaAmplitudeAtKeyCenter a) as kAKc.
    remember (INR k) as rk.
    remember (INR ks) as rks.
    remember (INR kc) as rkc.
    remember (between rk rks rkc) as f.

    (* If the starting key is < the center key... *)
    destruct (Compare_dec.lt_dec ks kc) as [Hklt|Hknlt]. {
      assert (isNormalized f) as Hnorm. {
        rewrite Heqf.
        rewrite Heqrk.
        rewrite Heqrks.
        rewrite Heqrkc.
        apply betweenNorm.
        apply lt_INR.
        exact Hklt.
        pose proof (kaValueStartOrder a) as Hso.
        split.
        apply le_INR.
        exact Hm0.
        apply le_INR.
        apply Nat.lt_le_incl.
        exact Hlt.
      }

      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].

      pose proof (kaAmplitudeAtKeyStartNormal a) as HKASN.
      rewrite <- HeqkAKs in HKASN.
      destruct HKASN as [HKASN0 HKASN1].

      (* Is the starting key amplitude <= the center key amplitude? *)
      destruct (Rle_or kAKs kAKc) as [Hle0|Hle1]. {
         pose proof (interpolateRange1 _ _ _ Hle0 Hnorm) as Hint0.
         lra.
      } {
         pose proof (interpolateRange2 _ _ _ Hle1 Hnorm) as Hint0.
         lra.
      }
    } {
      (* The starting key = the center key. *)
      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].
      lra.
    }
  } {
    (* center < k *)
    (* Abbreviations to make the proof context readable. *)
    remember (kaValueCenter a) as kc.
    remember (kaValueEnd a) as ke.
    remember (kaAmplitudeAtKeyCenter a) as kAKc.
    remember (kaAmplitudeAtKeyEnd a) as kAKe.
    remember (INR k) as rk.
    remember (INR kc) as rkc.
    remember (INR ke) as rke.
    remember (between rk rkc rke) as f.

    (* If the center key is < the end key... *)
    destruct (Compare_dec.lt_dec kc ke) as [Hklt|Hknlt]. {
      assert (isNormalized f) as Hnorm. {
        rewrite Heqf.
        rewrite Heqrk.
        rewrite Heqrkc.
        rewrite Heqrke.
        apply betweenNorm.
        apply lt_INR.
        exact Hklt.
        pose proof (kaValueCenterOrder a) as Hso.
        split.
        apply le_INR.
        apply Nat.lt_le_incl.
        exact Hgt.
        apply le_INR.
        exact Hm1.
      }

      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].

      pose proof (kaAmplitudeAtKeyEndNormal a) as HKAEN.
      rewrite <- HeqkAKe in HKAEN.
      destruct HKAEN as [HKAEN0 HKAEN1].

      (* Is the starting key amplitude <= the center key amplitude? *)
      destruct (Rle_or kAKc kAKe) as [Hle0|Hle1]. {
         pose proof (interpolateRange1 _ _ _ Hle0 Hnorm) as Hint0.
         lra.
      } {
         pose proof (interpolateRange2 _ _ _ Hle1 Hnorm) as Hint0.
         lra.
      }
    } {
      (* The center key = the end key. *)
      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].
      lra.
    }
  }
Qed.

(** A small proof to check that Coq's Rpower really means x ^ y. *)
Lemma powCheck : Rpower 2.0 4.0 = 16.0.
Proof.
  assert (2.0 = INR 2%nat) as H2 by (simpl; lra).
  assert (4.0 = INR 4%nat) as H4 by (simpl; lra).
  assert (16.0 = INR 16%nat) as H16 by (simpl; lra).
  rewrite H2.
  rewrite H4.
  rewrite H16.
  rewrite Rpower_pow.
  simpl; lra.
  simpl; lra.
Qed.

(** Determine the pitch ratio for a change in frequency of a given number
    of semitones. *)

Definition semitonesPitchRatio (semitones : R) : R :=
  Rpower 2.0 (Rdiv semitones 12.0).

(** The pitch ratio is always non-negative. *)

Lemma semitonesPitchRatioNonNegative : forall s,
  Rle 0 (semitonesPitchRatio s).
Proof.
  intros s.
  unfold semitonesPitchRatio.
  unfold Rpower.
  remember (s / 12.0 * ln 2.0) as x.
  pose proof (exp_pos x) as Hp.
  lra.
Qed.

(** Evaluate the playback rate of the given key assignment based on
    the key. *)

Definition keyAssignmentEvaluateRate
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  match (in_dec keyAssignmentFlagEqDec FlagUnpitched (kaFlags assignment)) with
  | left _  => 1.0
  | right _ =>
    let kLow := kaValueStart assignment in
    let kMid := kaValueCenter assignment in
      match Nat.compare key kMid with
      | Eq => 1
      | Lt =>
        let delta := minus kMid key in
          semitonesPitchRatio (-(INR delta))
      | Gt =>
        let delta := minus key kMid in
          semitonesPitchRatio (INR delta)
      end
  end.

(** The playback rate returned by evaluating a key assignment
    is always non-negative. *)

Theorem keyAssignmentEvaluateRateNonNegative : forall k v a,
  keyAssignmentMatches k v a
    -> Rle 0 (keyAssignmentEvaluateRate k a).
Proof.
  intros k v a [Hm0 [Hm1 [Hm2 Hm3]]].

  unfold keyAssignmentEvaluateRate.
  destruct (in_dec keyAssignmentFlagEqDec FlagUnpitched (kaFlags a)) as [Hin|Hnin]. {
    lra.
  } {
    destruct (Nat.compare_spec k (kaValueCenter a)) as [Heq|Hlt|Hgt]. {
      intuition.
    } {
      apply semitonesPitchRatioNonNegative.
    } {
      apply semitonesPitchRatioNonNegative.
    }
  }
Qed.

(** Fully evaluate a key assignment. *)

Definition keyAssignmentEvaluateFull
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: option keyEvaluation :=
  match keyAssignmentMatchesDecidable key velocity assignment with
  | right _ => None
  | left p  =>
    let clip  := kaClipId assignment in
    let ampV  := keyAssignmentEvaluateAmplitudeForVelocity velocity assignment in
    let ampVP := keyAssignmentEvaluateAmplitudeForVelocityNormalized _ _ _ p in
    let ampK  := keyAssignmentEvaluateAmplitudeForKey key assignment in
    let ampKP := keyAssignmentEvaluateAmplitudeForKeyNormalized _ _ _ p in
    let rate  := keyAssignmentEvaluateRate key assignment in
    let rateP := keyAssignmentEvaluateRateNonNegative _ _ _ p in
      Some (keyEvaluationMake clip ampV ampVP ampK ampKP rate rateP)
  end.

(** A proposition stating that the list of key assignments is sorted. *)

Inductive keyAssignmentListIsSorted : list keyAssignment -> Prop :=
  | kaListNone : keyAssignmentListIsSorted []
  | kaListOne : forall s, keyAssignmentListIsSorted [s]
  | kaListCons : forall s0 s1 s,
    lt (kaId s0) (kaId s1) ->
      keyAssignmentListIsSorted (s0 :: s) ->
        keyAssignmentListIsSorted (s1 :: s0 :: s).

(** The tail of a sorted list is still sorted. *)

Theorem keyAssignmentListIsSortedTail : forall x xs,
  keyAssignmentListIsSorted (x :: xs) ->
    keyAssignmentListIsSorted xs.
Proof.
  intros x xs Hcons.
  inversion Hcons.
  constructor.
  auto.
Qed.

(** A set of key assignments. *)

Inductive keyAssignments : Set := {
  kasList       : list keyAssignment;
  kasListSorted : keyAssignmentListIsSorted kasList
}.

(** Evaluate all key assignments that match the given key and velocity. *)

Fixpoint keyAssignmentsEvaluateFull
  (key         : nat)
  (velocity    : R)
  (assignments : list keyAssignment)
: list keyEvaluation :=
  match assignments with
  | nil         => []
  | cons a rest =>
    match keyAssignmentEvaluateFull key velocity a with
    | None   => keyAssignmentsEvaluateFull key velocity rest
    | Some r => cons r (keyAssignmentsEvaluateFull key velocity rest)
    end
  end.

(** The rules that define the version number increments required for
    a pair of key assignments. *)

Definition keyAssignmentCompatCompare
  (k0 k1 : keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentValuesEqDec k0 k1 with
  | left _ =>
    CVRMake CVersionChangeNone ""
  | right _ =>
    CVRMake CVersionChangeMajor "The values of the key assignment were changed."
  end.

(** Find the key assignment with the given ID. *)

Fixpoint keyAssignmentForId
  (i  : nat)
  (ka : list keyAssignment)
: option keyAssignment :=
  match ka with
  | nil         => None
  | cons a rest =>
    match Nat.eq_dec (kaId a) i with
    | left _  => Some a
    | right _ => keyAssignmentForId i rest
    end
  end.

Theorem keyAssignmentForIdIn : forall ks i k,
  keyAssignmentListIsSorted ks ->
    Some k = keyAssignmentForId i ks ->
      In k ks.
Proof.
  intros ks.
  induction ks as [|x xs]. {
    intros i k Hsort Hfalse.
    inversion Hfalse.
  } {
    intros i k Hsort Hsome.
    simpl in Hsome.
    destruct (Nat.eq_dec (kaId x) i). {
      assert (k = x) by congruence.
      subst k.
      constructor; reflexivity.
    } {
      pose proof (keyAssignmentListIsSortedTail _ _ Hsort) as HsT.
      pose proof (IHxs i k HsT Hsome) as Hind.
      apply in_cons.
      exact Hind.
    }
  }
Qed.

Theorem keyAssignmentForIdMatches : forall ks i k,
  keyAssignmentListIsSorted ks ->
    Some k = keyAssignmentForId i ks ->
      kaId k = i.
Proof.
  intros ks.
  induction ks as [|x xs]. {
    intros i k Hsort Hfalse.
    inversion Hfalse.
  } {
    intros i k Hsort Hsome.
    simpl in Hsome.
    destruct (Nat.eq_dec (kaId x) i). {
      assert (k = x) by congruence.
      subst k.
      intuition.
    } {
      pose proof (keyAssignmentListIsSortedTail _ _ Hsort) as HsT.
      pose proof (IHxs i k HsT Hsome) as Hind.
      exact Hind.
    }
  }
Qed.

Lemma keyAssignmentIdNeq : forall k0 k1,
  kaId k0 <> kaId k1 ->
    k0 <> k1.
Proof.
  intros k0 k1 Hneq.
  inversion k0.
  inversion k1.
  intuition.
  subst k0.
  apply Hneq.
  reflexivity.
Qed.

Theorem keyAssignmentForIdInNot : forall ks i k,
  keyAssignmentListIsSorted ks ->
    kaId k = i ->
      None = keyAssignmentForId i ks ->
        ~In k ks.
Proof.
  intros ks.
  induction ks as [|x xs]. {
    intros i k Hsort Heq Hnone.
    intuition.
  } {
    intros i k Hsort Heq Hnone.
    simpl in Hnone.
    subst i.
    destruct (Nat.eq_dec (kaId x) (kaId k)). {
      inversion Hnone.
    } {
      pose proof (keyAssignmentListIsSortedTail _ _ Hsort) as HsT.
      pose proof (IHxs (kaId k) k HsT eq_refl Hnone) as Hind.
      rewrite not_in_cons.
      constructor.
      apply keyAssignmentIdNeq.
      intuition.
      exact Hind.
    }
  }
Qed.

(** Determine all the elements of _ka_ that are not in _kb_. *)

Fixpoint keyAssignmentsRemoved
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  match ka with
  | nil => []
  | cons a rest =>
    match keyAssignmentForId (kaId a) kb with
    | None   => cons a (keyAssignmentsRemoved rest kb)
    | Some _ => keyAssignmentsRemoved rest kb
    end
  end.

(** If _k_ is in the list of removed elements, then _k_ must have
    been in _ka_. *)

Theorem keyAssignmentsRemovedIn : forall ka kb k,
  In k (keyAssignmentsRemoved ka kb) -> In k ka.
Proof.
  intros ka.
  induction ka as [|a rest]. {
    intros kb k Hin0.
    inversion Hin0.
  } {
    intros kb k Hin0.
    simpl in Hin0.
    destruct (keyAssignmentForId (kaId a) kb) eqn:Hm. {
      pose proof (IHrest kb k Hin0) as H0.
      apply in_cons.
      exact H0.
    } {
      destruct Hin0 as [HL|HR]. {
        subst a.
        constructor; reflexivity.
      } {
        pose proof (IHrest kb k HR) as H0.
        apply in_cons.
        exact H0.
      }
    }
  }
Qed.

(** If _k_ is in the list of removed elements, then _k_ must not have
    been in _kb_. *)

Theorem keyAssignmentsRemovedInNot : forall ka kb k,
  keyAssignmentListIsSorted kb ->
    In k (keyAssignmentsRemoved ka kb) ->
      ~In k kb.
Proof.
  intros ka.
  induction ka as [|a rest]. {
    intros kb k Hsort Hin0.
    inversion Hin0.
  } {
    intros kb k Hsort Hin0.
    simpl in Hin0.
    destruct (keyAssignmentForId (kaId a) kb) eqn:Hm. {
      apply IHrest.
      exact Hsort.
      exact Hin0.
    } {
      destruct Hin0 as [HL|HR]. {
        subst a.
        apply (keyAssignmentForIdInNot kb (kaId k) k Hsort eq_refl (eq_sym Hm)).
      } {
        apply IHrest.
        exact Hsort.
        exact HR.
      }
    }
  }
Qed.

(** Determine all the elements of _kb_ that are not in _ka_. *)
Definition keyAssignmentsAdded
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  keyAssignmentsRemoved kb ka.

(** If _k_ is in the list of added elements, then _k_ must have
    been in _kb_. *)

Theorem keyAssignmentsAddedIn : forall kb ka k,
  In k (keyAssignmentsAdded ka kb) -> In k kb.
Proof.
  unfold keyAssignmentsAdded.
  apply keyAssignmentsRemovedIn.
Qed.

(** If _k_ is in the list of added elements, then _k_ must not have
    been in _ka_. *)

Theorem keyAssignmentsAddedInNot : forall ka kb k,
  keyAssignmentListIsSorted ka ->
    In k (keyAssignmentsAdded ka kb) ->
      ~In k ka.
Proof.
  intros ka.
  unfold keyAssignmentsAdded.
  intros kb k Hsort Hin.
  apply (keyAssignmentsRemovedInNot _ _ _ Hsort Hin).
Qed.

Definition keyAssignmentsCompatCompareRemoved
  (r : list keyAssignment)
: list compatVersionChangeRecord :=
  map (fun a => CVRMake CVersionChangeMajor "A key assignment was removed.") r.

Lemma keyAssignmentsCompatCompareRemovedForall : forall r,
  Forall (fun a => cvrChange a = CVersionChangeMajor)
    (keyAssignmentsCompatCompareRemoved r).
Proof.
  intros r.
  apply Forall_map.
  induction r as [|y ys]. {
    constructor.
  } {
    simpl.
    constructor. reflexivity.
    apply IHys.
  }
Qed.

Definition keyAssignmentsCompatCompareAdd
  (k  : keyAssignment)
  (ka : list keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentsOverlapping k ka with
  | nil => CVRMake CVersionChangeMinor "A key assignment was added."
  | _   => CVRMake CVersionChangeMajor "A key assignment was added that overlaps with an existing assignment."
  end.

Definition keyAssignmentsCompatCompareAdded
  (added : list keyAssignment)
  (ka    : list keyAssignment)
: list compatVersionChangeRecord :=
  map (fun a => keyAssignmentsCompatCompareAdd a ka) added.

Definition keyAssignmentsCompatCompareChanged
  (r : list (keyAssignment * keyAssignment))
: list compatVersionChangeRecord :=
  map (fun p => keyAssignmentCompatCompare (fst p) (snd p)) r.

Definition keyAssignmentsCompatCompareFull
  (ka kb : list keyAssignment)
: list compatVersionChangeRecord :=
  let f              := (fun k ks => keyAssignmentForId (kaId k) ks) in
  let removed        := keyAssignmentsRemoved ka kb in
  let added          := keyAssignmentsAdded ka kb in
  let changed        := intersectionPairs f ka kb in
  let removedChanges := keyAssignmentsCompatCompareRemoved removed in
  let addedChanges   := keyAssignmentsCompatCompareAdded added kb in
  let changedChanges := keyAssignmentsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

(** If there's a non-empty list of removed elements, a major version change is required. *)
Theorem keyAssignmentsCompatCompareMajor0 : forall ka kb,
  [] <> keyAssignmentsRemoved ka kb ->
    compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
      = CVersionChangeMajor.
Proof.
  intros ka kb H_ne.
  unfold keyAssignmentsCompatCompareFull.
  apply compatVersionChangesMaximumCorrect0.
  apply in_map_iff.
  destruct (keyAssignmentsRemoved ka kb) as [|y ys]. {
    contradict H_ne; reflexivity.
  } {
    simpl.
    exists {| cvrChange := CVersionChangeMajor; cvrReason := "A key assignment was removed." |}.
    intuition.
  }
Qed.

(** Adding an overlapping key assignment is a major change. *)
Theorem keyAssignmentsCompatCompareMajor1 : forall ka kb k,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      In k (keyAssignmentsAdded ka kb) ->
        [] <> (keyAssignmentsOverlapping k kb) ->
        compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
          = CVersionChangeMajor.
Proof.
  intros ka kb k Hrm Hch Hin Hover.
  unfold keyAssignmentsCompatCompareFull.
  rewrite <- Hrm.
  rewrite <- Hch.
  simpl.
  rewrite app_nil_r.

  destruct (keyAssignmentsAdded ka kb) as [|y ys]. {
    inversion Hin.
  } {
    simpl.
    destruct (in_inv Hin) as [HL|HR]. {
      subst k.
      unfold keyAssignmentsCompatCompareAdd.
      destruct (keyAssignmentsOverlapping y kb). {
        contradict Hover. reflexivity.
      } {
        unfold compatVersionChangeRecordsMaximum.
        simpl.
        reflexivity.
      }
    } {
      unfold keyAssignmentsCompatCompareAdded.
      unfold compatVersionChangeRecordsMaximum.
      simpl.

      (* We can show that either one of the arguments _must_ be equal to Major. *)
      rewrite (
        compatVersionChangeMaxInv
          (cvrChange (keyAssignmentsCompatCompareAdd y kb))
          (compatVersionChangesMaximum
            (map (fun r : compatVersionChangeRecord => cvrChange r)
              (map (fun a : keyAssignment => keyAssignmentsCompatCompareAdd a kb) ys)))
      ).

      (* And we know that the right argument _must_ be Major, because k is in
         that part of the list. *)
      right.

      (* We can rewrite the nested maps to something less complicated. *)
      rewrite map_map.

      (* We can prove that k evaluates to a Major change. *)
      assert (
        cvrChange (keyAssignmentsCompatCompareAdd k kb) = CVersionChangeMajor
      ) as Hkmajor. {
        unfold keyAssignmentsCompatCompareAdd.
        destruct (keyAssignmentsOverlapping k kb). {
          contradict Hover; reflexivity.
        } {
          reflexivity.
        }
      }

      (* And we can prove that the result of evaluating k is in the list. *)
      pose proof (
        in_map
          (fun x : keyAssignment => cvrChange (keyAssignmentsCompatCompareAdd x kb))
          ys k HR
      ) as HinM.
      simpl in HinM.
      rewrite Hkmajor in HinM.

      (* We have a lemma that tells us that if anything in the list is Major,
         then the result is Major. *)
      apply compatVersionChangesMaximumCorrect0.
      exact HinM.
    }
  }
Qed.

(** Adding a non-overlapping key assignment is a minor change. *)
Theorem keyAssignmentsCompatCompareMinor0 : forall ka kb,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      [] <> (keyAssignmentsAdded ka kb) ->
        Forall (fun j => [] = keyAssignmentsOverlapping j kb) (keyAssignmentsAdded ka kb) ->
          compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
           = CVersionChangeMinor.
Proof.
  intros ka kb Heq0 Heq1 Hneq0 Hfa.
  unfold keyAssignmentsCompatCompareFull.
  rewrite <- Heq0.
  rewrite <- Heq1.
  simpl.
  rewrite app_nil_r.

  destruct (keyAssignmentsAdded ka kb) as [|y ys]. {
    contradict Hneq0; reflexivity.
  } {
    simpl.
    pose proof (Forall_inv Hfa) as Hfa0.
    simpl in Hfa0.
    unfold keyAssignmentsCompatCompareAdd.
    destruct (keyAssignmentsOverlapping y kb). {
      unfold compatVersionChangeRecordsMaximum.
      simpl.

      (* We can show that either one of the arguments _must_ be equal to Minor
         and the other to something minor or less. *)
      rewrite (
        compatVersionChangeMaxMinorInv
          CVersionChangeMinor
            (compatVersionChangesMaximum
              (map (fun r : compatVersionChangeRecord => cvrChange r)
                 (keyAssignmentsCompatCompareAdded ys kb)))
      ).

      unfold keyAssignmentsCompatCompareAdded.
      rewrite map_map.

      (* We can prove that y evaluates to a Major change. *)
      assert (
        cvrChange (keyAssignmentsCompatCompareAdd y kb) = CVersionChangeMinor
      ) as Hkminor. {
        unfold keyAssignmentsCompatCompareAdd.
        destruct (keyAssignmentsOverlapping y kb) eqn:Hover. {
          reflexivity.
        } {
          contradict Hover.
          pose proof (Forall_inv Hfa) as Hfa1.
          simpl in Hfa1.
          rewrite <- Hfa1.
          discriminate.
        }
      }

      (* We can prove that all elements map to a minor change. *)
      assert (
        Forall
          (fun k => k = CVersionChangeMinor)
          (map (fun x : keyAssignment =>
            cvrChange (keyAssignmentsCompatCompareAdd x kb)) ys)
      ) as Hfa1. {
        rewrite Forall_map.
        rewrite Forall_forall.
        pose proof (Forall_inv_tail Hfa) as Hfat.

        intros j Hj.
        unfold keyAssignmentsCompatCompareAdd.
        rewrite Forall_forall in Hfat.
        rewrite <- (Hfat j Hj).
        reflexivity.
      }

      apply CVMMinorLeft.
      constructor. {
        reflexivity.
      } {
        clear Hneq0.
        clear Hfa.
        clear Hfa0.
        clear Hkminor.
        induction (map (fun x : keyAssignment => cvrChange (keyAssignmentsCompatCompareAdd x kb)) ys) as [|z zs]. {
          right; reflexivity.
        } {
          left.
          pose proof (Forall_inv Hfa1) as Hfb0.
          pose proof (Forall_inv_tail Hfa1) as Hfb1.
          simpl.
          rewrite Hfb0.

          destruct (IHzs Hfb1) as [H0|H1]. {
            rewrite H0.
            reflexivity.
          } {
            rewrite H1.
            reflexivity.
          }
        }
      }
    }
    contradict Hfa0.
    discriminate.
  }
Qed.

5.17. Aurantium/Metadata.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.
From Stdlib Require Import Lists.List.

Local Open Scope string_scope.

Import ListNotations.

Inductive metadataValue : Set := MetadataValue {
  mKey   : string;
  mValue : string
}.

Inductive metadata : Set := Metadata {
  mValues : list metadataValue
}.

5.18. Aurantium/OctetOrder.v

(*
 * Copyright © 2025 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Arith.PeanoNat.
From Stdlib Require Import Lists.List.

Require Import Aurantium.Divisible8.
Require Import Aurantium.Descriptor.

Import ListNotations.

Inductive octetOrder : Set :=
  | OctetOrderBig
  | OctetOrderLittle.

Inductive bit : Set :=
  | B0
  | B1.

Inductive octet : Set :=
  | OctExact  : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet
  | OctRemain : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet.

Definition octetIsRemainder (o : octet): Prop :=
  match o with
  | OctExact  _ _ _ _ _ _ _ _ => False
  | OctRemain _ _ _ _ _ _ _ _ => True
  end.

Definition octetIsExact (o : octet): Prop :=
  match o with
  | OctExact  _ _ _ _ _ _ _ _ => True
  | OctRemain _ _ _ _ _ _ _ _ => False
  end.

Lemma octetIsRemainderNotExact : forall (o : octet), octetIsRemainder o -> ~octetIsExact o.
Proof.
  intros o Hrem Hfalse.
  destruct o; contradiction.
Qed.

Lemma octetIsExactNotRemainder : forall (o : octet), octetIsExact o -> ~octetIsRemainder o.
Proof.
  intros o Hrem Hfalse.
  destruct o; contradiction.
Qed.

Inductive bitsOctetsHasRemainder : list octet -> Prop :=
  | BOHasRemainder : forall (prefix : list octet) (o : octet),
    Forall octetIsExact prefix ->
      octetIsRemainder o ->
        bitsOctetsHasRemainder (prefix ++ o :: []).

Fixpoint octetsBigEndianAux
  (bits   : list bit)
  (octets : list octet)
: list octet :=
  match bits with
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest) =>
    octets ++ [OctExact b7 b6 b5 b4 b3 b2 b1 b0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 b1 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: rest) =>
    octets ++ [OctRemain b7 b6 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: rest) =>
    octets ++ [OctRemain b7 B0 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | [] =>
    octets
  end.

Definition octetsBigEndian (bits : list bit) : list octet :=
  octetsBigEndianAux bits [].

Definition octetsLittleEndian (bits : list bit) : list octet :=
  rev (octetsBigEndianAux bits []).

Definition listInduction8 :
  forall (A : Type),
  forall (P : list A -> Prop),
  P [] ->
  (forall (b0                      : A), P (b0 :: [])) ->
  (forall (b1 b0                   : A), P (b1 :: b0 :: [])) ->
  (forall (b2 b1 b0                : A), P (b2 :: b1 :: b0 :: [])) ->
  (forall (b3 b2 b1 b0             : A), P (b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b4 b3 b2 b1 b0          : A), P (b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b5 b4 b3 b2 b1 b0       : A), P (b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b6 b5 b4 b3 b2 b1 b0    : A), P (b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b7 b6 b5 b4 b3 b2 b1 b0 : A) (rest : list A), P rest -> P (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest)) ->
  forall (L : list A), P L :=
  (fun A P P0 P1 P2 P3 P4 P5 P6 P7 P8 =>
  fix f (l : list A) :=
    match l with
    | []                                                     => P0
    | x0 :: []                                               => P1 x0
    | (x0 :: x1 :: [])                                       => P2 x0 x1
    | (x0 :: x1 :: x2 :: [])                                 => P3 x0 x1 x2
    | (x0 :: x1 :: x2 :: x3 :: [])                           => P4 x0 x1 x2 x3
    | (x0 :: x1 :: x2 :: x3 :: x4 :: [])                     => P5 x0 x1 x2 x3 x4
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: [])               => P6 x0 x1 x2 x3 x4 x5
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: [])         => P7 x0 x1 x2 x3 x4 x5 x6
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: rest) => P8 x0 x1 x2 x3 x4 x5 x6 x7 rest (f rest)
    end).

Lemma app_non_empty : forall (A : Type) (xs : list A) (y : A),
  xs ++ [y] <> [].
Proof.
  intros A xs y.
  unfold not.
  destruct xs as [|z zs].
    intros Hfalse; inversion Hfalse.
    intros Hfalse; inversion Hfalse.
Qed.

Lemma app_list_implies_eq : forall (A : Type) (x y : A) (xs : list A),
  xs ++ [x] = [y] -> xs = [] /\ x = y.
Proof.
  intros A x y xs Happ.
  induction xs as [|z zs] eqn:Hxe.
  - constructor. reflexivity.
    rewrite (app_nil_l [x]) in Happ.
    injection Happ as Heq; exact Heq.
  - inversion Happ.
    assert (zs ++ [x] <> []) by (apply app_non_empty).
    contradiction.
Qed.

Lemma p8notZ : 8 <> 0.
Proof. discriminate. Qed.

Lemma list_mod8_0 : forall (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A),
  divisible8 (length xs) -> divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)).
Proof.
  intros A xs n7 n6 n5 n4 n3 n2 n1 n0 Hlen8.
  unfold divisible8 in *.
  assert (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs
       = (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: []) ++ xs) as HlistEq
          by reflexivity.
  rewrite HlistEq.
  rewrite length_app.
  assert (length [n7; n6; n5; n4; n3; n2; n1; n0] = 8) as Hprefix8 by reflexivity.
  rewrite Hprefix8.
  rewrite <- (Nat.Div0.add_mod_idemp_l 8 (length xs) 8).
  rewrite (Nat.Div0.mod_same 8).
  rewrite (Nat.add_0_l).
  exact Hlen8.
Qed.

Lemma list_mod8_1 : forall (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A),
  divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)) -> divisible8 (length xs).
Proof.
  intros A xs n7 n6 n5 n4 n3 n2 n1 n0 Hlen8.
  unfold divisible8 in *.
  assert (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs
       = (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: []) ++ xs) as HlistEq
          by reflexivity.
  rewrite HlistEq in Hlen8.
  rewrite length_app in Hlen8.
  assert (length [n7; n6; n5; n4; n3; n2; n1; n0] = 8) as Hprefix8 by reflexivity.
  rewrite Hprefix8 in Hlen8.
  rewrite <- (Nat.Div0.add_mod_idemp_l 8 (length xs) 8) in Hlen8.
  rewrite (Nat.Div0.mod_same 8) in Hlen8.
  rewrite (Nat.add_0_l) in Hlen8.
  exact Hlen8.
Qed.

Theorem list_mod8 : forall (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A),
  divisible8 (length xs) <-> divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)).
Proof.
  intros A xs n7 n6 n5 n4 n3 n2 n1 n0.
  constructor.
  - apply list_mod8_0.
  - apply list_mod8_1.
Qed.

Theorem octetsBigEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsBigEndian b).
Proof.
  intros b Hlen8.
  unfold octetsBigEndian.
  induction b using listInduction8.
  - constructor.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - simpl.
    rewrite <- list_mod8 in Hlen8.
    assert (Forall octetIsExact (octetsBigEndianAux b []))   as HallExact by (apply (IHb Hlen8)).
    assert (octetIsExact (OctExact b7 b6 b5 b4 b3 b2 b1 b0)) as Hexact    by constructor.
    apply (@Forall_cons octet octetIsExact (OctExact b7 b6 b5 b4 b3 b2 b1 b0) (octetsBigEndianAux b []) Hexact HallExact).
Qed.

Theorem octetsLittleEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsLittleEndian b).
Proof.
  intros b Hlen8.
  apply (Forall_rev (octetsBigEndianLengthDivisibleAllExact b Hlen8)).
Qed.

Theorem octetsBigEndianLengthDivisibleNoRemainder : forall (b : list bit),
  Forall octetIsExact (octetsBigEndian b) -> ~ bitsOctetsHasRemainder (octetsBigEndian b).
Proof.
  intros b HallExact.
  unfold octetsBigEndian.
  intro Hfalse.
  inversion Hfalse as [prefix o HprefixAllExact HoIsRemainder HprefixEq].
  unfold octetsBigEndian in HallExact.
  (* We know that everything in the list is exact. *)
  (* We can show that o must be in this list according to HprefixEq. *)
  assert (In o (octetsBigEndianAux b [])) as HoInB. {
    assert (In o (prefix ++ [o])) as HoInPrefix by (apply (in_elt o prefix [])).
    rewrite HprefixEq in HoInPrefix.
    exact HoInPrefix.
  }
  (* And because o is in the list, it must be exact. *)
  assert (octetIsExact o) as HoIsExact. {
    rewrite Forall_forall in HallExact.
    apply (HallExact o HoInB).
  }
  (* There is a contradiction; o cannot be both exact and a remainder. *)
  apply (octetIsExactNotRemainder o HoIsExact HoIsRemainder).
Qed.

Lemma mod_8_lt_0 : forall (m : nat),
  0 < m mod 8 -> 0 < (m + 8) mod 8.
Proof.
  intros m Hlt.
  rewrite (Nat.Div0.add_mod m 8 8).
  rewrite (Nat.Div0.mod_same).
  rewrite (Nat.add_0_r).
  rewrite (Nat.Div0.mod_mod).
  exact Hlt.
Qed.

Lemma mod_8_lt_1 : forall (m : nat),
  0 < (m + 8) mod 8 -> 0 < m mod 8.
Proof.
  intros m Hlt.
  rewrite (Nat.Div0.add_mod m 8 8) in Hlt.
  rewrite (Nat.Div0.mod_same)      in Hlt.
  rewrite (Nat.add_0_r)            in Hlt.
  rewrite (Nat.Div0.mod_mod)       in Hlt.
  exact Hlt.
Qed.

Lemma mod_8_lt : forall (m : nat),
  0 < (m + 8) mod 8 <-> 0 < m mod 8.
Proof.
  constructor.
  apply mod_8_lt_1.
  apply mod_8_lt_0.
Qed.

Theorem octetsBigEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> exists o, In o (octetsBigEndian b) /\ octetIsRemainder o.
Proof.
  intros b Hlength.
  induction b using listInduction8.
  - inversion Hlength.
  - exists (OctRemain b0 B0 B0 B0 B0 B0 B0 B0).
    constructor.
    left. reflexivity.
    constructor.
  - exists (OctRemain b1 b0 B0 B0 B0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b2 b1 b0 B0 B0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b3 b2 b1 b0 B0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b4 b3 b2 b1 b0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b5 b4 b3 b2 b1 b0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b6 b5 b4 b3 b2 b1 b0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - assert (0 < length b mod 8) as Hlt. {
      assert (length (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: b) = length b + 8) as Heq
        by (rewrite Nat.add_comm; reflexivity).
      rewrite Heq in Hlength.
      rewrite <- (mod_8_lt (length b)).
      exact Hlength.
    }
    assert (exists o : octet, In o (octetsBigEndian b) /\ octetIsRemainder o) as HEx
      by (apply (IHb Hlt)).
    destruct HEx as [ox [HoxIn HoxRem]].
    simpl.
    exists ox.
    constructor.
    right.
    exact HoxIn.
    exact HoxRem.
Qed.

Theorem octetsLittleEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> exists o, In o (octetsLittleEndian b) /\ octetIsRemainder o.
Proof.
  unfold octetsLittleEndian.
  intros b Hlen.
  assert (exists o, In o (octetsBigEndian b) /\ octetIsRemainder o) as Hexists
    by (apply (octetsBigEndianLengthIndivisibleRemainder b Hlen)).
  destruct Hexists as [ox [HoxIn HoxRem]].
  exists ox.
  rewrite <- (in_rev (octetsBigEndianAux b [])).
  constructor.
  exact HoxIn.
  exact HoxRem.
Qed.

From Stdlib Require Import Strings.String.

Local Open Scope string_scope.

Definition octetOrderDescribe (b : octetOrder) : descriptor :=
  match b with
  | OctetOrderBig    => "com.io7m.aurantium.endian_big"
  | OctetOrderLittle => "com.io7m.aurantium.endian_little"
  end.

#[export]
Instance octetOrderDescribable : describable octetOrder := {
  descriptorOf f := octetOrderDescribe f
}.

5.19. Aurantium/StringUtility.v

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

From Stdlib Require Import Arith.PeanoNat.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.

Local Open Scope string_scope.
Local Open Scope char_scope.

Set Mangle Names.

Definition digitOfNat (n : nat) : ascii :=
  match n with
  | 0 => "0"
  | 1 => "1"
  | 2 => "2"
  | 3 => "3"
  | 4 => "4"
  | 5 => "5"
  | 6 => "6"
  | 7 => "7"
  | 8 => "8"
  | _ => "9"
  end.

Fixpoint stringOfNatAux (time n : nat) (acc : string) : string :=
  let acc' := String (digitOfNat (n mod 10)) acc in
  match time with
  | 0 => acc'
  | S time' =>
    match n / 10 with
    | 0 => acc'
    | n' => stringOfNatAux time' n' acc'
    end
  end.

Definition stringOfNat (n : nat) : string :=
  stringOfNatAux n n "".