# Calino 2.0
| Property | Value |
| --- | --- |
| CREATOR | Mark Raynsford |
| DATE | 2026-05-01T11:32:59+00:00 |
| DESCRIPTION | Specification for the Calino texture file format. |
| IDENTIFIER | ba8fa621-69a4-486d-b5d7-1c31f76eba32 |
| LANGUAGE | en |
| RIGHTS | Public Domain |
| TITLE | Calino 2.0 |
## Table Of Contents
- [1. Overview](#id_64e6eff7-50e5-40d3-bf0b-616710c02581)
- [2. Informal Description](#id_bcaaa010-7ab3-43d5-92a0-df5a2f9f62b8)
- [2.1. Overview](#d0e121)
- [2.2. Assumptions](#d0e164)
- [2.3. Purpose](#id_3a564fef-0f37-4fc8-ba1b-6534c62a1c3e)
- [2.4. Concepts](#id_7d9b1dd1-24dc-4017-8dd0-100dbef51041)
- [2.5. Example](#id_9af37c83-029f-4071-a976-18445121aa17)
- [3. Notational Conventions](#d0e236)
- [3.1. Rocq](#d0e238)
- [3.2. Unicode](#d0e259)
- [3.3. Sets](#d0e280)
- [4. The Calino Model](#id_73066219-7f6d-4809-b87c-897be98b4a6b)
- [4.1. Overview](#d0e588)
- [4.2. Divisibility By 8](#id_90ccdf09-f680-44c2-848f-a352a480abbb)
- [4.3. Bits & Octets](#d0e669)
- [4.4. Descriptors](#d0e841)
- [4.5. Channels](#id_6b4bf0e8-728e-4be4-894c-a0d0fc6e0fc1)
- [4.6. Color Spaces](#id_ef1a7f1b-d076-43e4-8cfc-61b6c7dc40d4)
- [4.7. Compression](#id_bd75557c-d8d2-4522-93b3-e29d78d436b7)
- [4.8. Supercompression](#id_8f83a47a-986e-4dba-bfd7-720641cee3a9)
- [4.9. Coordinate Systems](#id_bf9a3817-5e64-426c-ad91-f408fdcc4a60)
- [4.10. Flags](#id_5cc98cd8-610f-4a6e-a76a-7f00ab987843)
- [4.11. Image Information](#id_4ae63d09-ce2d-46d4-a8eb-f1f9ad382ee8)
- [4.12. Mipmaps](#id_b8d20538-e4ac-4674-aa43-d5ab93c07149)
- [4.13. Array Mipmaps](#id_f4b4fff9-a443-4430-a37b-ed939e606bef)
- [4.14. Cube Mipmaps](#id_e8125add-3c83-47a1-9997-1f15867068dd)
- [4.15. Metadata](#id_eb8b3eb5-29b1-411c-a9ae-754d1a4b2940)
- [4.16. Textures](#id_17b69d69-176f-4db1-bab3-c1666ed58c5c)
- [5. The Calino Binary Encoding](#id_494888da-c85e-42df-8c2b-b789e84586e4)
- [5.1. Binary Expressions](#d0e3147)
- [5.2. File Header](#d0e3412)
- [5.3. File Identifiers](#id_a8147173-6b03-400d-8dc5-d3c68197b325)
- [5.4. Sections](#id_eb66b381-4c70-4246-95e9-d3a61e19ac4c)
- [5.5. Image Information](#id_bc0e7016-7dab-4edb-a4c9-2b1492da0225)
- [5.6. 2D Textures](#id_8321ef71-e529-4764-abf1-e678e42c03af)
- [5.7. Array Textures](#id_a91529c1-d7c4-4e6e-abcb-bfeb3d536aba)
- [5.8. Cube Textures](#id_df607ad1-a586-4a3f-b8bc-f322142056f9)
- [5.9. Metadata](#id_16fddeaf-9d7f-437b-8662-01e6975f6249)
- [5.10. End](#id_40d09b06-b6de-4052-92fe-2829942518c9)
- [5.11. Examples](#d0e3940)
- [6. References](#id_4b9e5329-27a9-4544-b6a4-53b5738e6f34)
- [6.1. Normative References](#d0e3957)
- [6.2. Informative References](#d0e4086)
- [7. Appendix A: History](#id_a058b965-cde6-408f-ae2f-fbd7cdf44126)
- [7.1. Version 2.0](#d0e4156)
- [8. Appendix B: Sources](#id_404d63ad-55e4-463f-8d42-bdf374d78b86)
## 1. Overview
This specification defines version **2.0** of the **calino** file format. The **calino** format is a carefully designed file format intended for the storage and delivery of texture data for realtime 3D rendering applications.
This specification is divided into an abstract [model](#id_73066219-7f6d-4809-b87c-897be98b4a6b) and a separate [binary encoding](#id_494888da-c85e-42df-8c2b-b789e84586e4). The purpose of the model is to describe the semantics of **calino** files; the actual **meaning** of the data within, and to describe properties and invariants that must be true for all valid **calino** 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 **calino** files. This layered approach is intended to allow for specifying the format with a level of precision that will allow data in the **calino** 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 rendering APIs.
Developers wishing to write their own code to read and write **calino** files might find it easiest to view the [binary encoding](#id_494888da-c85e-42df-8c2b-b789e84586e4) section first. The **calino** 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 image/texture file formats) [1](#id_eea4b3e0-3eaa-4f00-8b5c-a3007d9b7061). Once a developer is able to read data from an existing **calino** file, they should consult the [model](#id_73066219-7f6d-4809-b87c-897be98b4a6b) 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 texture types.
## 2. Informal Description
### 2.1. Overview
This section of the specification provides a simple, informal description of the **calino** format. It is intended as the recommended starting point for readers who want to understand the purpose and structure of the format before consulting the [formal model](#id_73066219-7f6d-4809-b87c-897be98b4a6b) or the [binary encoding](#id_494888da-c85e-42df-8c2b-b789e84586e4).
The following subsections walk through the main concepts: the [purpose](#id_3a564fef-0f37-4fc8-ba1b-6534c62a1c3e) of the format and the types of data a **calino** file is designed to store, the [concepts](#id_7d9b1dd1-24dc-4017-8dd0-100dbef51041) that define how that data is described, an outline of the basic rules for packing **data** into files, and the section-based file layout. An annotated [hex dump](#id_9af37c83-029f-4071-a976-18445121aa17) is provided as a concrete illustration of a **calino** file.
The following subsections are **informative**; if any part of the following text disagrees with the rest of the specification, the rest of the specification should be considered the source of truth and this informative text mistaken.
### 2.2. Assumptions
This specification assumes that readers are familiar with the following:
#### 2.2.2. Familiar Concepts
- Basic graphics concepts including GPUs, textures, and mipmaps.
- Byte ordering / endianness.
- The **DEFLATE** and **LZ4** compression algorithms [DEFLATE](#d0e3967) [LZ4](#d0e3967).
- [Unicode](https://www.unicode.org) text and its **UTF-8** byte encoding [UTF-8](#d0e3967).
To read the full formal specification, the reader must be familiar with the [Rocq](https://rocq-prover.org/doc/V9.0.0/refman/index.html) language [Rocq](#d0e3967).
### 2.3. Purpose
...
### 2.4. Concepts
...
### 2.5. Example
An annotated hexdump of an example file is as follows:
#### 2.5.2. Hex Dump
```
The fixed-size file header indicating the type and version of the file:
Format major version 2, minor version 0
|- Calino identifier -| |---------| |---------|
00000000 89 43 4c 4e 0d 0a 1a 0a 00 00 00 02 00 00 00 00 |.CLN............|
The info section containing information about the contents of the file:
|-Identifier CLNIINFO-| |-Section size (192) -|
00000010 43 4c 4e 49 49 4e 46 4f 00 00 00 00 00 00 00 c0 |CLNIINFO........|
00000020 00 00 00 20 00 00 00 20 00 00 00 01 00 00 00 08 |... ... ........|
00000030 52 38 3a 47 38 3a 42 38 00 00 00 1f 46 49 58 45 |R8:G8:B8....FIXE|
00000040 44 5f 50 4f 49 4e 54 5f 4e 4f 52 4d 41 4c 49 5a |D_POINT_NORMALIZ|
00000050 45 44 5f 55 4e 53 49 47 4e 45 44 00 00 00 00 0c |ED_UNSIGNED.....|
00000060 55 4e 43 4f 4d 50 52 45 53 53 45 44 00 00 00 00 |UNCOMPRESSED....|
00000070 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |................|
00000080 00 00 00 0c 55 4e 43 4f 4d 50 52 45 53 53 45 44 |....UNCOMPRESSED|
00000090 00 00 00 00 00 00 00 00 00 00 00 08 52 54 3a 53 |............RT:S|
000000a0 52 3a 54 44 00 00 00 04 53 52 47 42 00 00 00 01 |R:TD....SRGB....|
000000b0 00 00 00 13 41 4c 50 48 41 5f 50 52 45 4d 55 4c |....ALPHA_PREMUL|
000000c0 54 49 50 4c 49 45 44 00 00 00 00 0a 42 49 47 5f |TIPLIED.....BIG_|
000000d0 45 4e 44 49 41 4e 00 00 00 00 00 00 00 00 00 00 |ENDIAN..........|
The metadata section containing arbitrary application-provided text:
|-Identifier CLN_META-| |- Section size (48) -|
000000e0 43 4c 4e 5f 4d 45 54 41 00 00 00 00 00 00 00 30 |CLN_META.......0|
000000f0 00 00 00 02 00 00 00 02 4b 30 00 00 00 00 00 04 |........K0......|
00000100 56 41 4c 30 00 00 00 04 4b 45 59 31 00 00 00 04 |VAL0....KEY1....|
00000110 56 41 4c 31 00 00 00 00 00 00 00 00 00 00 00 00 |VAL1............|
The 2D texture mipmap data:
|-Identifier CLN_I2D!-| |-Section size (3120)-|
00000120 43 4c 4e 5f 49 32 44 21 00 00 00 00 00 00 0c 30 |CLN_I2D!.......0|
00000130 00 00 00 01 00 00 00 00 00 00 00 00 00 00 00 30 |...............0|
00000140 00 00 00 00 00 00 0c 00 00 00 00 00 00 00 0c 00 |................|
00000150 f3 af ee df 00 00 00 00 00 00 00 00 00 00 00 00 |................|
00000160 00 00 fb 00 00 f7 00 00 f4 00 00 ef 00 00 ec 00 |................|
00000170 00 e9 00 00 e5 00 00 e0 00 00 dc 00 00 d7 00 00 |................|
00000180 d3 00 00 ce 00 00 ca 00 00 c5 00 00 c0 00 00 bb |................|
00000190 00 00 b5 00 00 af 00 00 a9 00 00 a4 00 00 9e 00 |................|
000001a0 00 96 00 00 8f 00 00 87 00 00 7e 00 00 75 00 00 |..........~..u..|
000001b0 6d 00 00 60 00 00 53 00 00 42 00 00 2a 00 00 00 |m..`..S..B..*...|
000001c0 00 07 f7 00 00 f4 00 00 ef 00 00 ec 00 00 e9 00 |................|
000001d0 00 e5 00 00 e0 00 00 dc 00 00 d7 00 00 d2 00 00 |................|
000001e0 cd 00 00 ca 00 00 c5 00 00 c0 00 00 bb 00 00 b5 |................|
000001f0 00 00 af 00 00 a9 00 00 a4 00 00 9e 00 00 97 00 |................|
...
00000d30 8d b6 00 95 b1 00 9b ad 00 a3 a7 00 ab 9f 00 b3 |................|
00000d40 99 00 bb 92 00 c3 89 00 ca 81 00 d2 77 00 da 6d |............w..m|
00000d50 00 de 66 00 e7 58 00 ee 49 00 f5 35 00 fd 00 00 |..f..X..I..5....|
The end section:
|-Identifier CLN_END!-| |- Section size (0) -|
00000d60 43 4c 4e 5f 45 4e 44 21 00 00 00 00 00 00 00 00 |CLN_END!........|
00000d70
```
## 3. Notational Conventions
### 3.1. Rocq
The formal specification described here is written in the [specification language of the Rocq theorem prover](https://rocq-prover.org/doc/V9.0.0/refman/index.html) . 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](#id_404d63ad-55e4-463f-8d42-bdf374d78b86).
### 3.2. Unicode
The specification makes reference to the [Unicode](https://www.unicode.org) character set which, at the time of writing, is at version 13.0.0. The specification often references specific Unicode characters, and does so using the standard notation **U+NNNN**, where **N** represents a hexadecimal digit. For example, **U+03BB** corresponds to the lowercase lambda symbol **λ**.
### 3.3. Sets
Where the specification refers to sets, it is referring to sets as defined in [Zermelo-Fraenkel set theory](https://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory) .
#### 3.3.2. ZFC
| Notation | Description |
| --- | --- |
| **e ∈ A** | **e** is an element of the set **A** |
| **e ∉ A** | **e** is not an element of the set **A** |
| **{ x₀, x₁, ... xₙ }** | A set consisting of values from **x₀** to **xₙ** |
| **{ e ∈ A \| p(e) }** | A set consisting of the elements of **A** for which the proposition **p** holds |
| **\|A\|** | The cardinality of the set **A**; a measure of the number of elements in **A** |
| **∅** | The empty set |
| **𝔹** | The booleans |
| **ℕ** | The natural numbers |
| **ℝ** | The real numbers |
| **ℤ** | The integers |
| **[a, b]** | A closed interval in a set (given separately or implicit from the types of **a** and **b**), from **a** to **b**, including **a** and **b** |
| **(a, b]** | A closed interval in a set (given separately or implicit from the types of **a** and **b**), from **a** to **b**, excluding **a** but including **b** |
| **[a, b)** | A closed interval in a set (given separately or implicit from the types of **a** and **b**), from **a** to **b**, including **a** but excluding **b** |
| **(a, b)** | A closed interval in a set (given separately or implicit from the types of **a** and **b**), from **a** to **b**, excluding **a** and **b** |
| **A ⊂ B** | **A** is a subset of, and is not equal to, **B** |
| **A ⊆ B** | **A** is a subset of, or is equal to, **B** |
| **A ∩ B** | The smallest set of elements that appear in both **A** and **B** (intersection). |
## 4. The Calino Model
## 4.1. Overview
The **calino** texture file format is optimized for the storage of textures used for real-time 3D rendering. The format provides the following features:
#### 4.1.2. Features
- Detailed information about the format and layout of image data is included in all files. Image data, in the common case, can be introspected without requiring consulting any kind of external specification. The information provided about image data includes dimensions, full channel layout and type information, compression and supercompression methods, color space, coordinate system, alpha premultiplication, and byte ordering for formats that use components larger than a single octet.
- [Mipmaps](https://en.wikipedia.org/wiki/Mipmap) are natively supported and are not treated differently to textures that do not have mipmaps; an texture without mipmaps is considered to comprise of a single mip level **0**. Mipmaps are exposed in a manner that facilitates efficient **texture streaming**.
- Rendering system independence. The format specification does not require implementers to read the [Vulkan](https://www.vulkan.org), [OpenGL](https://www.opengl.org), [DirectX](https://en.wikipedia.org/wiki/DirectX) specifications in order to parse files.
- 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 image data in order to make use of it. For example, if image data is encoded using an unusual and/or proprietary texture format (such as **A5B3G3R3**), consumers can still trivially extract the raw data of each mipmap even if they cannot necessarily perform rendering with image data of that format. Likewise, the compressed bytes of each mipmap can always be obtained even if the compression method is unknown to the consumer.
- 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" image data types that consumers are expected to understand, but the format also allows for declaring new self-describing image data types.
- Practical metadata. The format provides a standard section that contains [UTF-8](https://en.wikipedia.org/wiki/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 **calino** format uses to express all of the above.
## 4.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**.
#### 4.2.2. Divisible8
```
Definition divisible8 (x : nat) : Prop :=
modulo x 8 = 0.
```
## 4.3. Bits & Octets
A **bit** is a single digit in the [base-2](https://en.wikipedia.org/wiki/Binary_number) numbering system. A bit may either be 0 or 1:
#### 4.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](#id_90ccdf09-f680-44c2-848f-a352a480abbb). 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.
#### 4.3.4. Octet
```
Inductive octetOrder : Set :=
| OctetOrderBig
| OctetOrderLittle.
```
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.
#### 4.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.
```
#### 4.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.
#### 4.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.
#### 4.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.
```
#### 4.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.
#### 4.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.
```
#### 4.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.
```
## 4.4. Descriptors
A **descriptor** is a UTF-8 encoded string of an arbitrary length that describes an object in a **calino** texture file.
#### 4.4.2. Descriptor
```
Definition descriptor := string.
```
An object is **describable** iff it has an associated **descriptor**.
#### 4.4.4. Describable
```
Class describable (A : Set) := {
descriptorOf : A -> descriptor
}.
```
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.
## 4.5. Channels
### 4.5.1. Overview
A **channel** in **calino** corresponds to the traditional definition of a channel in computer graphics: A **channel** consists of a set of intensity values for one of the color components that make up an image. For example, a typical RGB image has a **red** channel, a **green** channel, and a **blue** channel that store the intensity values of each component for each pixel in the image. The following image shows the separate **red**, **green**, and **blue** channels used for the pixels of an RGB image:
#### 4.5.1.2. RGB Example
As the **calino** package is intended for use in real-time 3D graphics, it makes the assumption that for an image consisting of channels **[c₁, cₙ]**, each pixel **Pᵢ** in the image stores channel values **[c₁(ᵢ), cₙ (ᵢ)]** sequentially in memory:
#### 4.5.1.4. Channels Example
A set of channels may be **packed** or **unpacked**. In an **unpacked** set of channels, each channel is of a size in bits that is a multiple of 8. This means that when the set of channels is stored in memory for each pixel, each channel occupies at least one octet in memory, and no two channels in a given pixel occupy the same octet. For channels that are larger than a single octet, the **byte ordering** of the underlying host computer dictates the exact order of the octets that make up a single channel. Otherwise, the groups of octets that comprise the data for a set of channels are ordered according to the channel declaration order. For example, a common unpacked image format in computer graphics, at the time of writing, is **R8G8B8**. In the **R8G8B8** format, each channel occupies 8 bits, and the channels are stored such that **R** comes first in memory, followed by **G**, and then **B**:
#### 4.5.1.6. R8G8B8
Note that, because all of the channels are 8 bits, the mapping from the channels to the underlying host octets does not depend on the byte ordering of the underlying host computer. Another common unpacked image format where the underlying byte ordering of the host computer **does** affect the mapping from channels to octets is the **R16G16B16** format. In the **R16G16B16** format, each channel requires 16 bits and so each channel must be mapped to two octets in memory. If the underlying host byte ordering is **little-endian**, then the **most significant bits** of each channel are stored in the **higher** of the two octets used for the channel. If the underlying host byte ordering is **big-endian**, then the **most significant bits** of each channel are stored in the **lower** of the two octets used for the channel. For example, channels in the **R16G16B16** format are stored as follows on a computer with little-endian byte ordering:
#### 4.5.1.8. R16G16B16 Little Endian
As shown in the diagram, the 8 most significant bits of the **R** channel of pixel 0 are stored in octet 1. The 8 least significant bits of the **R** channel of pixel 0 are stored in octet 0. This pattern continues for each subsequent channel of each subsequent pixel. Note that regardless of the byte ordering, the octets that make up the **R** channel are stored first, followed by the **G** channel, and finally the **B** channel. The same format on a computer with big-endian byte ordering is stored as follows:
#### 4.5.1.10. R16G16B16 Big Endian
As shown in the diagram, the 8 most significant bits of the **R** channel of pixel 0 are stored in octet 0. The 8 least significant bits of the **R** channel of pixel 0 are stored in octet 1. This pattern continues for each subsequent channel of each subsequent pixel. Note that regardless of the byte ordering, the octets that make up the **R** channel are stored first, followed by the **G** channel, and finally the **B** channel.
In a **packed** set of channels, each channel may be of any size in bits (excluding zero) but the sum of the sizes of all of the channels in the set typically must be a multiple of 8. The **calino** package restricts this definition further by stating that the sum of the sizes of the channels must be in the set **{8, 16, 32, 64}**. Conceptually, the bits of all channels are packed into a single integer value, and then this integer value is stored in memory according to the host computer byte ordering. For example, a common packed image format in computer graphics, at the time of writing, is **R5G6B5**. In the **R5G6B5** format, the bits of all of the channels are packed into a single 16-bit integer **k** such that the 5 bits of the **R** channel are packed into the 5 most significant bits of **k**, followed by the 6 bits of the **G** channel, followed by the 5 bits of the **B** channel. The value of **k** is then stored into memory according to the host computer byte ordering:
#### 4.5.1.13. R5G6B5
In the above diagram, it's clear that the 5 bits that make up the **R** channel of pixel 0 are mapped to bits **[11,15]** in **k**. The 6 bits that make up the **G** channel are mapped to bits **[5, 14]** in **k**, and the remaining 5 bits that make up the **B** channel are mapped to bits **[0,4]** in **k**. On a big-endian computer, the two octets that make up **k** are arranged such that the most significant bits of **k** end up in octet 0 in memory, whilst the least significant bits of **k** end up in octet 1 in memory. On a little-endian computer, the two octets that make up **k** are arranged such that the most significant bits of **k** end up in octet 1 in memory, whilst the least significant bits of **k** end up in octet 0 in memory. Note that this means that the **G** channel ends up divided into two pieces with the **R** and **B** channels sandwiched between it. It's also important to note that the ordering of bits does not change between big-endian and little-endian systems. This demonstrates the critical difference between **packed** and **unpacked** formats: In a **packed** format, any given octet may contain bits from more than one channel, whilst in an **unpacked** format, a given octet will contain bits from exactly one channel. At the time of writing, no rendering API appears to have defined any packed image formats that pack channels into an integer value larger than 32 bits.
The information provided about a set of channels largely attempts to answer two main questions: "How do I get image data to and from storage?" and "How do I interpret the image data once I have it?". [Channel semantic](#id_121539df-2316-4f53-bdaa-dae1b8829974) and [channel type](#id_e786563b-f469-4977-bb74-f069cc584ec3) information answers the latter question, whilst [channel descriptions](#id_2e70b32a-1c97-4310-bb14-14f2403e8cd1) answer the former. The aggregates of these values, [channel layouts](#id_499041fb-7c35-4fa6-be6b-895962e6e717), answer a little of both questions.
### 4.5.2. Channel Semantic
A **channel semantic** specifies how a particular channel should be interpreted within the context of an image. A **channel semantic** may be one of the following values:
#### 4.5.2.2. Channel Semantic Values
```
Inductive channelSemantic : Set :=
| CSRed
| CSGreen
| CSBlue
| CSAlpha
| CSDepth
| CSStencil
| CSExponent
| CSUnused.
```
**Channel semantic** values must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.5.2.4. Channel Semantic Description
```
Definition channelSemanticDescribe (c : channelSemantic) : descriptor :=
match c with
| CSRed => "R"
| CSGreen => "G"
| CSBlue => "B"
| CSAlpha => "A"
| CSDepth => "D"
| CSStencil => "S"
| CSExponent => "E"
| CSUnused => "X"
end.
```
#### 4.5.2.5. Channel Semantic Describable
```
Instance channelSemanticDescribable : describable channelSemantic := {
descriptorOf c := channelSemanticDescribe c
}.
```
### 4.5.3. Channel Description
A **channel description** combines a [channel semantic](#id_121539df-2316-4f53-bdaa-dae1b8829974) and a non-zero size value expressed in bits. The size value specifies the number of bits of storage required for a single value in the channel.
#### 4.5.3.2. Channel Description
```
Inductive channelDescription : Set := channelDescriptionMake {
cdSemantic : channelSemantic;
cdBits : nat;
cdBitsNonzero : 0 <> cdBits
}.
```
**Channel descriptions** must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.5.3.4. Channel Description
```
Definition channelDescriptionDescribe (c : channelDescription) : descriptor :=
descriptorOf (cdSemantic c) ++ stringOfNat (cdBits c).
```
#### 4.5.3.5. Channel Describable
```
Instance channelDescriptionDescribable : describable channelDescription := {
descriptorOf c := channelDescriptionDescribe c
}.
```
The descriptors for a set of channel descriptions must be concatenated together with **U+003A ':'**:
#### 4.5.3.7. Channel Descriptions
```
Fixpoint channelDescriptionsDescribe (c : list channelDescription) : descriptor :=
match c with
| nil => ""
| cons d nil => channelDescriptionDescribe d
| cons d e => (channelDescriptionDescribe d) ++ ":" ++ (channelDescriptionsDescribe e)
end.
```
### 4.5.4. Channel Layout
### 4.5.4.1. Description
A **channel layout** describes how a set of channels are ordered. A channel layout may either be **packed** or **unpacked**.
#### 4.5.4.1.2. Channel Layout
```
Inductive channelLayoutDescription : Set :=
| ChannelLayoutDescriptionUnpacked : channelLayoutDescriptionUnpacked -> channelLayoutDescription
| ChannelLayoutDescriptionPacked : channelLayoutDescriptionPacked -> channelLayoutDescription.
```
The total number of bits required by a set of channels is the sum of the sizes of each channel, as given by **channelDescriptionsBitsTotal**:
#### 4.5.4.1.4. Channels Required Bits
```
Fixpoint channelDescriptionsBitsTotal (c : list channelDescription) : nat :=
match c with
| nil => 0
| (x :: rest) => (cdBits x) + (channelDescriptionsBitsTotal rest)
end.
```
Both **packed** and **unpacked** layouts must always have a size in bits that is divisible by 8:
#### 4.5.4.1.6. Channels Required Bits Divisible
```
Theorem channelLayoutDescriptionBitsDivisible8 : forall (c : channelLayoutDescription),
divisible8 (channelLayoutDescriptionBits c).
Proof.
(* Proof omitted for brevity; see ChannelDescription.v for proofs. *)
Qed.
```
### 4.5.4.2. Unpacked Layouts
An **unpacked** layout consists of a non-empty sequence of channels where the size of each channel must be divisible by 8.
#### 4.5.4.2.2. Unpacked Layout
```
Inductive channelLayoutDescriptionUnpacked : Set := CLDUMake {
uChannels : list channelDescription;
uChannelsNonEmpty : [] <> uChannels;
uInvariants : Forall channelDescriptionBitsDivisible8 uChannels;
}.
```
### 4.5.4.3. Packed Layouts
A **packed** layout consists of a non-empty sequence of channels and a **layout packing** value.
#### 4.5.4.3.2. Packed Layout
```
Inductive channelLayoutDescriptionPacked : Set := CLDPMake {
pChannels : list channelDescription;
pChannelsNonEmpty : [] <> pChannels;
pPacking : channelLayoutPacking;
pInvariants : channelDescriptionsBitsTotal pChannels = channelLayoutPackingBits pPacking
}.
```
The **layout packing** value must be one of the following values:
#### 4.5.4.3.4. Layout Packing
```
Inductive channelLayoutPacking : Set :=
| CLPack8
| CLPack16
| CLPack32
| CLPack64.
```
The number of bits associated with a **layout packing** value is given by **channelLayoutPackingBits**:
#### 4.5.4.3.6. Layout Packing Bits
```
Definition channelLayoutPackingBits (c : channelLayoutPacking) : nat :=
match c with
| CLPack8 => 8
| CLPack16 => 16
| CLPack32 => 32
| CLPack64 => 64
end.
```
The number of bits associated with a **layout packing** value is always divisible by 8:
#### 4.5.4.3.8. Layout Packing Bits Divisible 8
```
Theorem channelLayoutPackingBitsDiv8 : forall c, divisible8 (channelLayoutPackingBits (c)).
```
For a **packed** layout, the number of bits required for the channels must equal the number of bits associated with the given **packed** layout.
**Layout packing** values are [describable](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.5.4.3.11. Layout Packing Description
```
Definition channelLayoutPackingDescribe (c : channelLayoutPacking) : descriptor :=
match c with
| CLPack8 => "p8"
| CLPack16 => "p16"
| CLPack32 => "p32"
| CLPack64 => "p64"
end.
```
#### 4.5.4.3.12. Layout Packing Describable
```
Instance channelLayoutPackingDescribable : describable channelLayoutPacking := {
descriptorOf c := channelLayoutPackingDescribe c
}.
```
### 4.5.4.4. Descriptors
**Channel layouts** are [describable](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.5.4.4.2. Unpacked Layout Description
```
Definition channelLayoutDescriptionUnpackedDescribe (c : channelLayoutDescriptionUnpacked) : descriptor :=
channelDescriptionsDescribe (uChannels c).
```
#### 4.5.4.4.3. Unpacked Layout Describable
```
Instance channelLayoutDescriptionUnpackedDescribable : describable channelLayoutDescriptionUnpacked := {
descriptorOf c := channelLayoutDescriptionUnpackedDescribe c
}.
```
#### 4.5.4.4.4. Packed Layout Description
```
Definition channelLayoutDescriptionPackedDescribe (c : channelLayoutDescriptionPacked) : descriptor :=
let packing := descriptorOf (pPacking c) in
let channels := channelDescriptionsDescribe (pChannels c) in
packing ++ "|" ++ channels.
```
#### 4.5.4.4.5. Packed Layout Describable
```
Instance channelLayoutDescriptionPackedDescribable : describable channelLayoutDescriptionPacked := {
descriptorOf c := channelLayoutDescriptionPackedDescribe c
}.
```
#### 4.5.4.4.6. Layout Description
```
Definition channelLayoutDescriptionDescribe (c : channelLayoutDescription) : descriptor :=
match c with
| ChannelLayoutDescriptionPacked p => descriptorOf p
| ChannelLayoutDescriptionUnpacked u => descriptorOf u
end.
```
#### 4.5.4.4.7. Layout Describable
```
Instance channelLayoutDescriptionDescribable : describable channelLayoutDescription := {
descriptorOf c := channelLayoutDescriptionDescribe c
}.
```
### 4.5.5. Channel Type
A **channel type** defines how the sequence of bits that make up a value in a channel should be interpreted numerically. A **channel type** must be one of the following values:
#### 4.5.5.2. Channel Types
```
Inductive channelType : Set :=
| CTFixedPointNormalizedUnsigned
| CTFixedPointNormalizedSigned
| CTScaledUnsigned
| CTScaledSigned
| CTIntegerUnsigned
| CTIntegerSigned
| CTFloatIEEE754
| CTCustom : descriptor -> channelType.
```
A value of **CTFixedPointNormalizedUnsigned** indicates the values in a channel should be interpreted as unsigned fixed-point values. Given a floating point value **f** in the range **[0, 1]**, the corresponding **n**-bit unsigned fixed point value **h** is given by the relation **f = h / (2ⁿ - 1)**.
A value of **CTFixedPointNormalizedSigned** indicates that the values in a channel should be interpreted as signed fixed-point values. Given a floating point value **f** in the range **[-1, 1]**, the corresponding **n**-bit signed fixed point value **h** is given by the relation **f = max (h / (2ⁿ⁻¹ - 1), -1)**.
A value of **CTScaledUnsigned** indicates that the values in a channel should be interpreted as unsigned integers, and then converted to similar floating-point values on use. For example, a channel containing the value **23** would be ideally converted to **23.0** when sampled.
A value of **CTScaledSigned** indicates that the values in a channel should be interpreted as signed integers, and then converted to similar floating-point values on use. For example, a channel containing the value **-23** would be ideally converted to **-23.0** when sampled.
A value of **CTIntegerUnsigned** indicates that the values in a channel should be interpreted as unsigned integers.
A value of **CTIntegerSigned** indicates that the values in a channel should be interpreted as signed integers.
A value of **CTFloatIEEE754** indicates that the values in a channel should be interpreted as [IEEE 754](https://en.wikipedia.org/wiki/IEEE_754) binary floating point values of a size appropriate for the channel (such as **binary16**, **binary32**, **binary64**, and etc).
A value of **CTCustom** indicates that values in a channel should be interpreted in a manner not defined by this specification. **CTCustom** values may be used, for example, to specify exotic platform-specific floating point formats for textures that are intended to be used on a limited range of hardware.
**Channel types** must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.5.5.12. Channel Description
```
Definition channelTypeDescribe (c : channelType) : descriptor :=
match c with
| CTFixedPointNormalizedUnsigned => "FIXED_POINT_NORMALIZED_UNSIGNED"
| CTFixedPointNormalizedSigned => "FIXED_POINT_NORMALIZED_SIGNED"
| CTScaledUnsigned => "SCALED_UNSIGNED"
| CTScaledSigned => "SCALED_SIGNED"
| CTIntegerUnsigned => "INTEGER_UNSIGNED"
| CTIntegerSigned => "INTEGER_SIGNED"
| CTFloatIEEE754 => "FLOATING_POINT_IEEE754"
| CTCustom d => d
end.
```
#### 4.5.5.13. Channel Describable
```
Instance channelTypeDescribable : describable channelType := {
descriptorOf c := channelTypeDescribe c
}.
```
### 4.5.6. Standard Formats
### 4.5.6.1. Overview
The **calino** package considers a number of formats to be **standard** at the time of writing due to their widespread use. In most cases, support for the formats is guaranteed to be present on modern GPUs due to their status of being required formats by specifications such as [Vulkan](https://www.vulkan.org).
Implementations must provide some degree of support for these formats. For example, implementations that provide tools to manipulate images must be able to, at a minimum, manipulate images in all of the standard formats. Packages that provide the ability to read **calino** texture files and upload the contents to a GPU must expect to encounter textures in all of the standard formats.
### 4.5.6.2. R4 G4 B4 A4
An RGBA layout with 4 bits of precision in each channel, packed into a 16-bit integer.
#### 4.5.6.2.2. R4 G4 B4 A4 Definition
```
Definition Layout_R4_G4_B4_A4 : channelLayoutDescription :=
ChannelLayoutDescriptionPacked (CLDPMake R4_G4_B4_A4_Channels R4_G4_B4_A4_NonEmpty CLPack16 eq_refl).
```
### 4.5.6.3. A1 R5 G5 B5
An RGBA layout with 1 bit of precision in the alpha channel, and 5 bits of precision in each of the other channels, packed into a 16-bit integer.
#### 4.5.6.3.2. A1 R5 G5 B5 Definition
```
Definition Layout_A1_R5_G5_B5 : channelLayoutDescription :=
ChannelLayoutDescriptionPacked (CLDPMake A1_R5_G5_B5_Channels A1_R5_G5_B5_NonEmpty CLPack16 eq_refl).
```
### 4.5.6.4. R5 G6 B5
An RGB layout with 5 bits of precision in the red and blue channels, and 6 bits of precision in the green channel, packed into a 16-bit integer.
#### 4.5.6.4.2. R5 G6 B5 Definition
```
Definition Layout_R5_G6_B5 : channelLayoutDescription :=
ChannelLayoutDescriptionPacked (CLDPMake R5_G6_B5_Channels R5_G6_B5_NonEmpty CLPack16 eq_refl).
```
### 4.5.6.5. R8 G8 B8 A8
An unpacked RGBA layout with 8 bits of precision in each channel.
#### 4.5.6.5.2. R8 G8 B8 A8 Definition
```
Definition Layout_R8_G8_B8_A8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_A8_Channels R8_G8_B8_A8_NonEmpty R8_G8_B8_A8_FDiv8).
```
### 4.5.6.6. R8 G8 B8
An unpacked RGB layout with 8 bits of precision in each channel.
#### 4.5.6.6.2. R8 G8 B8 Definition
```
Definition Layout_R8_G8_B8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_Channels R8_G8_B8_NonEmpty R8_G8_B8_FDiv8).
```
### 4.5.6.7. R8 G8
An unpacked RG layout with 8 bits of precision in each channel.
#### 4.5.6.7.2. R8 G8 Definition
```
Definition Layout_R8_G8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_Channels R8_G8_NonEmpty R8_G8_FDiv8).
```
### 4.5.6.8. R8
An unpacked R layout with 8 bits of precision in each channel.
#### 4.5.6.8.2. R8 Definition
```
Definition Layout_R8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_Channels R8_NonEmpty R8_FDiv8).
```
### 4.5.6.9. R16 G16 B16 A16
An unpacked RGBA layout with 16 bits of precision in each channel.
#### 4.5.6.9.2. R16 G16 B16 A16 Definition
```
Definition Layout_R16_G16_B16_A16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_A16_Channels R16_G16_B16_A16_NonEmpty R16_G16_B16_A16_FDiv8).
```
### 4.5.6.10. R16 G16 B16
An unpacked RGB layout with 16 bits of precision in each channel.
#### 4.5.6.10.2. R16 G16 B16 Definition
```
Definition Layout_R16_G16_B16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_Channels R16_G16_B16_NonEmpty R16_G16_B16_FDiv8).
```
### 4.5.6.11. R16 G16
An unpacked RG layout with 16 bits of precision in each channel.
#### 4.5.6.11.2. R16 G16 Definition
```
Definition Layout_R16_G16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_Channels R16_G16_NonEmpty R16_G16_FDiv8).
```
### 4.5.6.12. R16
An unpacked R layout with 16 bits of precision in each channel.
#### 4.5.6.12.2. R16 Definition
```
Definition Layout_R16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_Channels R16_NonEmpty R16_FDiv8).
```
### 4.5.6.13. R32 G32 B32 A32
An unpacked RGBA layout with 32 bits of precision in each channel.
#### 4.5.6.13.2. R32 G32 B32 A32 Definition
```
Definition Layout_R32_G32_B32_A32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_A32_Channels R32_G32_B32_A32_NonEmpty R32_G32_B32_A32_FDiv8).
```
### 4.5.6.14. R32 G32 B32
An unpacked RGB layout with 32 bits of precision in each channel.
#### 4.5.6.14.2. R32 G32 B32 Definition
```
Definition Layout_R32_G32_B32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_Channels R32_G32_B32_NonEmpty R32_G32_B32_FDiv8).
```
### 4.5.6.15. R32 G32
An unpacked RG layout with 32 bits of precision in each channel.
#### 4.5.6.15.2. R32 G32 Definition
```
Definition Layout_R32_G32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_Channels R32_G32_NonEmpty R32_G32_FDiv8).
```
### 4.5.6.16. R32
An unpacked R layout with 32 bits of precision in each channel.
#### 4.5.6.16.2. R32 Definition
```
Definition Layout_R32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_Channels R32_NonEmpty R32_FDiv8).
```
### 4.5.6.17. R64 G64 B64 A64
An unpacked RGBA layout with 64 bits of precision in each channel.
#### 4.5.6.17.2. R64 G64 B64 A64 Definition
```
Definition Layout_R64_G64_B64_A64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_A64_Channels R64_G64_B64_A64_NonEmpty R64_G64_B64_A64_FDiv8).
```
### 4.5.6.18. R64 G64 B64
An unpacked RGB layout with 64 bits of precision in each channel.
#### 4.5.6.18.2. R64 G64 B64 Definition
```
Definition Layout_R64_G64_B64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_Channels R64_G64_B64_NonEmpty R64_G64_B64_FDiv8).
```
### 4.5.6.19. R64 G64
An unpacked RG layout with 64 bits of precision in each channel.
#### 4.5.6.19.2. R64 G64 Definition
```
Definition Layout_R64_G64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_Channels R64_G64_NonEmpty R64_G64_FDiv8).
```
### 4.5.6.20. R64
An unpacked R layout with 64 bits of precision in each channel.
#### 4.5.6.20.2. R64 Definition
```
Definition Layout_R64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_Channels R64_NonEmpty R64_FDiv8).
```
## 4.6. Color Spaces
The values in the **n** color [channels](#id_6b4bf0e8-728e-4be4-894c-a0d0fc6e0fc1) of an image are interpreted as coordinates in an **n**-dimensional **color space**. A **color space** declaration indicates which color space is intended to be used.
#### 4.6.2. Color Space
```
Inductive colorSpace : Set :=
| CSLinear
| CSsRGB
| CSCustom : descriptor -> colorSpace.
```
A value of **CSLinear** indicates that the color values should be interpreted as coordinates in a pure, conceptually linear color space.
A value of **CSsRGB** indicates that the color values should be interpreted as coordinates in the [sRGB](https://en.wikipedia.org/wiki/SRGB) color space.
A value of **CSCustom** indicates that the color values should be interpreted as coordinates in a custom color space. Implementations are permitted to reject files containing unrecognized color spaces.
Color space declarations must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.6.7. Color Space Description
```
Definition colorSpaceDescribe (c : colorSpace) : descriptor :=
match c with
| CSLinear => "LINEAR"
| CSsRGB => "SRGB"
| CSCustom d => d
end.
```
#### 4.6.8. Color Space Describable
```
Instance colorSpaceDescribable : describable colorSpace := {
descriptorOf c := colorSpaceDescribe c
}.
```
## 4.7. Compression
### 4.7.1. Description
A **compression** declaration indicates that image data is compressed in a manner that is expected to interpreted directly by a consuming GPU. This is in contrast to [super compression](#id_8f83a47a-986e-4dba-bfd7-720641cee3a9), where image data must be manually decompressed before it can be consumed by a GPU.
#### 4.7.1.2. Compression Methods
```
Inductive compressionMethod : Set :=
| CompressionUncompressed
| CompressionBC1
| CompressionBC2
| CompressionBC3
| CompressionBC4
| CompressionBC5
| CompressionBC6
| CompressionBC7
| CompressionETC1
| CompressionETC2
| CompressionEAC
| CompressionASTC : nat -> nat -> compressionMethod
| CompressionCustom :
forall (d : descriptor)
(blockSizeX : nat)
(blockSizeY : nat)
(identifier : nat)
(align : nat), 0 < align -> compressionMethod.
```
A value of **CompressionUncompressed** indicates that image data is not compressed.
A value of **CompressionBC1** indicates that image data is compressed using **BC1** compression (also known as **DXT1** compression).
A value of **CompressionBC2** indicates that image data is compressed using **BC2** compression (also known as **DXT3** compression).
A value of **CompressionBC3** indicates that image data is compressed using **BC3** compression (also known as **DXT5** compression).
A value of **CompressionBC4** indicates that image data is compressed using **BC4** compression.
A value of **CompressionBC5** indicates that image data is compressed using **BC5** compression.
A value of **CompressionBC6** indicates that image data is compressed using **BC6** compression.
A value of **CompressionBC7** indicates that image data is compressed using **BC7** compression.
A value of **CompressionETC1** indicates that image data is compressed using [ETC1](https://en.wikipedia.org/wiki/Ericsson_Texture_Compression) compression.
A value of **CompressionETC2** indicates that image data is compressed using [ETC2](https://en.wikipedia.org/wiki/Ericsson_Texture_Compression) compression.
A value of **CompressionEAC** indicates that image data is compressed using [EAC](https://en.wikipedia.org/wiki/Ericsson_Texture_Compression) compression.
A value of **CompressionASTC** indicates that image data is compressed using [ASTC](https://en.wikipedia.org/wiki/Adaptive_scalable_texture_compression) compression.
A value of **CompressionCustom** indicates that image data is compressed using a method not known to this specification.
Compression declarations must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.7.1.17. Compression Description
```
Definition compressionMethodDescriptor (c : compressionMethod) :=
match c with
| CompressionUncompressed => "UNCOMPRESSED"
| CompressionBC1 => "BC1"
| CompressionBC2 => "BC2"
| CompressionBC3 => "BC3"
| CompressionBC4 => "BC4"
| CompressionBC5 => "BC5"
| CompressionBC6 => "BC6"
| CompressionBC7 => "BC7"
| CompressionETC1 => "ETC1"
| CompressionETC2 => "ETC2"
| CompressionEAC => "EAC"
| CompressionASTC _ _ => "ASTC"
| CompressionCustom c _ _ _ _ _ => c
end.
```
#### 4.7.1.18. Compression Describable
```
Instance compressionMethodDescribable : describable compressionMethod := {
descriptorOf c := compressionMethodDescriptor c
}.
```
### 4.7.2. Block Sizes
Compression methods have inherent **block sizes** that typically influence the required alignment in memory of compressed data.
#### 4.7.2.2. Compression Block Size X
```
Definition compressionBlockSizeX (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 4
| CompressionBC2 => 4
| CompressionBC3 => 4
| CompressionBC4 => 4
| CompressionBC5 => 4
| CompressionBC6 => 4
| CompressionBC7 => 4
| CompressionETC1 => 4
| CompressionETC2 => 4
| CompressionEAC => 4
| CompressionASTC x _ => x
| CompressionCustom _ x _ _ _ _ => x
end.
```
#### 4.7.2.3. Compression Block Size Y
```
Definition compressionBlockSizeY (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 4
| CompressionBC2 => 4
| CompressionBC3 => 4
| CompressionBC4 => 4
| CompressionBC5 => 4
| CompressionBC6 => 4
| CompressionBC7 => 4
| CompressionETC1 => 4
| CompressionETC2 => 4
| CompressionEAC => 4
| CompressionASTC _ y => y
| CompressionCustom _ _ y _ _ _ => y
end.
```
#### 4.7.2.4. Compression Block Alignment
```
Definition compressionBlockAlignment (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 8
| CompressionBC2 => 16
| CompressionBC3 => 16
| CompressionBC4 => 8
| CompressionBC5 => 16
| CompressionBC6 => 16
| CompressionBC7 => 16
| CompressionETC1 => 16
| CompressionETC2 => 16
| CompressionEAC => 16
| CompressionASTC _ _ => 16
| CompressionCustom _ _ _ _ a _ => a
end.
```
### 4.7.3. Section Identifiers
Custom compression methods may require including extra metadata in order to allow the data to be decompressed. Compression methods may include a **section identifier** value indicating that consumers should look for a section with the given identifier to locate the metadata.
#### 4.7.3.2. Compression Section Identifier
```
Definition compressionSectionIdentifier (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 0
| CompressionBC2 => 0
| CompressionBC3 => 0
| CompressionBC4 => 0
| CompressionBC5 => 0
| CompressionBC6 => 0
| CompressionBC7 => 0
| CompressionETC1 => 0
| CompressionETC2 => 0
| CompressionEAC => 0
| CompressionASTC _ _ => 0
| CompressionCustom _ _ _ i _ _ => i
end.
```
## 4.8. Supercompression
### 4.8.1. Description
A **super compression** declaration indicates that image data is compressed in a manner that requires it to be decompressed before it can be consumed by a GPU for use. This is in contrast to [compression](#id_bd75557c-d8d2-4522-93b3-e29d78d436b7), where GPUs are expected to consume compressed data directly.
#### 4.8.1.2. Supercompression Methods
```
Inductive superCompressionMethod : Set :=
| SuperCompressionUncompressed
| SuperCompressionLZ4
| SuperCompressionDEFLATE
| SuperCompressionCustom : descriptor -> nat -> superCompressionMethod.
```
A value of **SuperCompressionUncompressed** indicates that image data is not compressed.
A value of **SuperCompressionLZ4** indicates that image data is compressed using [LZ4](http://lz4.github.io/lz4/) compression.
A value of **SuperCompressionDEFLATE** indicates that image data is compressed with the [DEFLATE](https://en.wikipedia.org/wiki/Deflate) algorithm (RFC 1951) and stored in a [zlib container](https://www.rfc-editor.org/rfc/rfc1950.html) (RFC 1950).
A value of **SuperCompressionCustom** indicates that image data is compressed using a method not known to this specification.
Compression declarations must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.8.1.8. Super Compression Description
```
Definition superCompressionMethodDescriptor (c : superCompressionMethod) :=
match c with
| SuperCompressionUncompressed => "UNCOMPRESSED"
| SuperCompressionLZ4 => "LZ4"
| SuperCompressionDEFLATE => "DEFLATE"
| SuperCompressionCustom c _ => c
end.
```
#### 4.8.1.9. Super Compression Describable
```
Instance superCompressionMethodDescribable : describable superCompressionMethod := {
descriptorOf c := superCompressionMethodDescriptor c
}.
```
### 4.8.2. Section Identifiers
Custom super compression methods may require including extra metadata in order to allow the data to be decompressed. Super compression methods may include a **section identifier** value indicating that consumers should look for a section with the given identifier to locate the metadata.
#### 4.8.2.2. Super Compression Section Identifier
```
Definition superCompressionSectionIdentifier (c : superCompressionMethod) : nat :=
match c with
| SuperCompressionUncompressed => 0
| SuperCompressionLZ4 => 0
| SuperCompressionDEFLATE => 0
| SuperCompressionCustom _ i => i
end.
```
## 4.9. Coordinate Systems
All images implicitly have a **coordinate system** such that the locations of pixels are specified relative to some origin point. For example, OpenGL's **screen space** is a coordinate system with the origin at the **bottom left** such that X coordinates increase **rightwards** and Y coordinates increase **upwards**. In contrast, Java2D's coordinate system has the origin at the **top left** such that X coordinates increase **rightwards** and Y coordinates increase **downwards**. Texture coordinates are typically expressed as a 3-tuple **(R, S, T)**, where **S** is analogous to the X axis, **T** is analogous to the Y axis, and **R** is analogous to the Z axis. The **R** coordinate value is only present for 3D textures.
#### 4.9.2. Texture Coordinates
The coordinate system of an image must match the coordinate system of the intended rendering system in order for the image to be rendered correctly. For example, taking an image that was intended for Java2D's system and rendering it directly in OpenGL will result in an image displaying upside down.
Textures in the **calino** package include descriptions of their coordinate systems. A **coordinate system** declaration comprises of three values that describe the orientations of the **R**, **S**, and **T** axes.
#### 4.9.5. Coordinates R
```
Inductive coordinateAxisR : Set :=
| AxisRIncreasingToward
| AxisRIncreasingAway.
```
A value of **AxisRIncreasingToward** indicates that the **R** axis increases **towards** the viewer.
A value of **AxisRIncreasingAway** indicates that the **R** axis increases **away** from the viewer.
#### 4.9.8. Coordinates S
```
Inductive coordinateAxisS : Set :=
| AxisSIncreasingRight
| AxisSIncreasingLeft.
```
A value of **AxisSIncreasingRight** indicates that the **S** axis increases **rightwards**.
A value of **AxisSIncreasingLeft** indicates that the **S** axis increases **leftwards**.
#### 4.9.11. Coordinates T
```
Inductive coordinateAxisT : Set :=
| AxisTIncreasingDown
| AxisTIncreasingUp.
```
A value of **AxisTIncreasingDown** indicates that the **S** axis increases **downwards**.
A value of **AxisTIncreasingUp** indicates that the **S** axis increases **upwards**.
#### 4.9.14. Coordinate System Values
```
Inductive coordinateSystem : Set :=
CoordinateSystem : coordinateAxisR -> coordinateAxisS -> coordinateAxisT -> coordinateSystem.
```
Coordinate system values must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.9.16. Coordinates R Description
```
Definition coordinateAxisRDescribe (c : coordinateAxisR) : descriptor :=
match c with
| AxisRIncreasingToward => "RT"
| AxisRIncreasingAway => "RA"
end.
```
#### 4.9.17. Coordinates R Describable
```
Instance coordinateAxisRDescribable : describable coordinateAxisR := {
descriptorOf c := coordinateAxisRDescribe c
}.
```
#### 4.9.18. Coordinates S Description
```
Definition coordinateAxisSDescribe (c : coordinateAxisS) : descriptor :=
match c with
| AxisSIncreasingRight => "SR"
| AxisSIncreasingLeft => "SL"
end.
```
#### 4.9.19. Coordinates S Describable
```
Instance coordinateAxisSDescribable : describable coordinateAxisS := {
descriptorOf c := coordinateAxisSDescribe c
}.
```
#### 4.9.20. Coordinates T Description
```
Definition coordinateAxisTDescribe (c : coordinateAxisT) : descriptor :=
match c with
| AxisTIncreasingDown => "TD"
| AxisTIncreasingUp => "TU"
end.
```
#### 4.9.21. Coordinates T Describable
```
Instance coordinateAxisTDescribable : describable coordinateAxisT := {
descriptorOf c := coordinateAxisTDescribe c
}.
```
#### 4.9.22. Coordinate System Description
```
Definition coordinateSystemDescribe (c : coordinateSystem) : descriptor :=
match c with
| CoordinateSystem r s t =>
descriptorOf r ++ ":" ++ descriptorOf s ++ ":" ++ descriptorOf t
end.
```
#### 4.9.23. Coordinate System Describable
```
Instance coordinateSystemDescribable : describable coordinateSystem := {
descriptorOf c := coordinateSystemDescribe c
}.
```
## 4.10. Flags
A texture may have one or more boolean **flags** describing metadata that does not fit into any of the other categories of metadata included in **calino** texture files. A given flag may appear at most once in any given texture file.
#### 4.10.2. Flag
```
Inductive flag : Set :=
| FlagAlphaPremultiplied
| FlagCustom : descriptor -> flag.
```
#### 4.10.3. Flags
```
Inductive flagSet : Set := {
flags : list flag;
flagsNoDup : NoDup flags;
}.
```
A value of **FlagAlphaPremultiplied** indicates that the color channels of the image data have been multiplied by the value in the alpha channel of the image.
A value of **FlagCustom** indicates that the texture has flags not known to this specification.
Flags must use the following [descriptors](#id_3d52e6ab-ded8-4b58-b1cc-576ced1fb578):
#### 4.10.7. Flag Description
```
Definition flagDescribe (f : flag) : descriptor :=
match f with
| FlagAlphaPremultiplied => "ALPHA_PREMULTIPLIED"
| FlagCustom d => d
end.
```
#### 4.10.8. Flag Describable
```
Instance flagDescribable : describable flag := {
descriptorOf f := flagDescribe f
}.
```
## 4.11. Image Information
An **image information** value aggregates all of the image metadata described in this specification.
#### 4.11.2. Image Information
```
Record imageInfo : Set := ImageInfo {
imageSize : imageSize3D;
imageChannelsLayout : channelLayoutDescription;
imageChannelsType : channelType;
imageCompressionMethod : compressionMethod;
imageSuperCompressionMethod : superCompressionMethod;
imageCoordinateSystem : coordinateSystem;
imageColorSpace : colorSpace;
imageFlags : flagSet;
imageByteOrder : octetOrder
}.
```
#### 4.11.3. Image Size
```
Record imageSize3D : Set := ImageSize3D {
sizeX : nat;
sizeY : nat;
sizeZ : nat;
sizeXnot0 : 0 <> sizeX;
sizeYnot0 : 0 <> sizeY;
sizeZnot0 : 0 <> sizeZ;
}.
```
The **sizeX**, **sizeY**, and **sizeZ** values declare the size of the image on the **X**, **Y**, and **Z** axes, respectively. All size values must be non-zero, and further restrictions may be placed on the size values by specific [image](#id_17b69d69-176f-4db1-bab3-c1666ed58c5c) types.
The **texel block alignment** is a value in octets to which image data is expected to be aligned. For [compressed](#id_bd75557c-d8d2-4522-93b3-e29d78d436b7) images, this is equal to the declared [block alignment](#id_a1b65dcf-36d1-4519-a765-06a3bd1e68c2). For uncompressed images, this is equal to the total size of all of the channels in bits, divided by 8.
#### 4.11.6. Texel Block Alignment
```
Definition imageInfoTexelBlockAlignment (i : imageInfo) :=
let c := imageCompressionMethod i in
match c with
| CompressionUncompressed => channelLayoutDescriptionBits (imageChannelsLayout i) / 8
| _ => compressionBlockAlignment c
end.
```
## 4.12. Mipmaps
A 2D texture consists of a non-empty sequence of **mipmaps**. A sequence of mipmaps is a sequence of progressively scaled-down copies of a **base image**. Each mipmap **level** is numbered with the base image being at level **0** and the number of each subsequent level is the successor of the number of the previous level. The mipmap image at each level is half the width and height of the previous level.
#### 4.12.2. Mipmaps Arrangement
A mipmap stores an **offset** indicating the start of the actual image data for the mipmap relative to the first octet of the first mipmap declaration. A mipmap also stores the [compressed size](#id_8f83a47a-986e-4dba-bfd7-720641cee3a9) and uncompressed size of the image data, along with a [CRC32](https://en.wikipedia.org/wiki/Cyclic_redundancy_check) checksum of the **uncompressed** data. A CRC32 value of **0** indicates that no checksum is available. For uncompressed data, the compressed and uncompressed sizes must equal the size of the uncompressed data.
#### 4.12.4. MipMap
```
Inductive mipMap : Set := MipMap {
mipMapLevel : nat;
mipMapOffset : nat;
mipMapSizeCompressed : nat;
mipMapSizeUncompressed : nat;
mipMapCRC32 : nat
}.
```
Mipmap sequences are stored such that the data for the mipmap with the highest level is encountered **first**, whilst the data for the mipmap with level **0** is encountered **last**. This facilitates a common implementation pattern where textures are progressively streamed onto the GPU starting with the highest mipmap levels first. The proposition **mipMapOffsetsSorted** declares that, for a given mipmap **m**, the offset of **m** plus the compressed size of **m**, must be less than the offset of the next mipmap in the sequence.
#### 4.12.6. MipMap Sequence Sorting
```
Inductive mipMapListIsSorted : list mipMap -> Prop :=
| MipsOne : forall m, mipMapListIsSorted [m]
| MipsCons : forall mm0 mm1 mxs,
mipMapLevel mm1 = S (mipMapLevel mm0) ->
mipMapListIsSorted (mm0 :: mxs) ->
mipMapListIsSorted (mm1 :: mm0 :: mxs).
```
#### 4.12.7. MipMap Offsets Sorting
```
Inductive mipMapOffsetsSorted : list mipMap -> Prop :=
| MMSizeOne : forall m, mipMapOffsetsSorted [m]
| MMSizeCons : forall mm0 mm1 mxs,
((mipMapOffset mm1) + (mipMapSizeCompressed mm1)) < (mipMapOffset mm0) ->
mipMapOffsetsSorted (mm0 :: mxs) ->
mipMapOffsetsSorted (mm1 :: mm0 :: mxs).
```
#### 4.12.8. MipMap Sequence
```
Inductive mipMapList : Set := MipMapList {
mipMaps : list mipMap;
mipMapListSorted : mipMapListIsSorted mipMaps;
mipMapOffsetSorted : mipMapOffsetsSorted mipMaps;
}.
```
Given a base image of size **(sizeX, sizeY)**, the size of the mipmap at level **n** is given by **(sizeX / 2ⁿ, sizeY / 2ⁿ)**. Mipmap images are required to be of a size **>= 2** on the X and Y axes. Note that this restriction does **not** apply to the base image; a base image with a size of 1 on any axis simply cannot have anything but a level 0 mipmap.
#### 4.12.10. MipMap Size
```
Inductive mipMapImageSize : Set := MipMapImageSize {
mmSizeX : nat;
mmSizeY : nat;
mmSizeXRange : 1 < mmSizeX;
mmSizeYRange : 1 < mmSizeY;
}.
```
#### 4.12.11. MipMap Size Calculation
```
Definition mipMapSize
(level : nat)
(imageSize : imageSize3D)
(levelRange : 0 < level)
: option mipMapImageSize :=
let sx := (sizeX imageSize) / 2 ^ level in
let sy := (sizeY imageSize) / 2 ^ level in
match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with
| (ReflectT _ xt, ReflectT _ yt) => Some (MipMapImageSize sx sy xt yt)
| (_, _) => None
end.
```
The total size required to hold the image data for all mipmaps is effectively equal to the offset of the largest mipmap, plus the compressed size of the mipmap, rounded up to the required alignment of the image data.
#### 4.12.13. MipMap Data Size (Aux)
```
Fixpoint mipMapImageDataSizeTotalAux (m : list mipMap) : nat :=
match m with
| [] => 0
| (x :: []) => (mipMapOffset x) + (mipMapSizeCompressed x)
| (x :: xs) => mipMapImageDataSizeTotalAux xs
end.
```
#### 4.12.14. MipMap Data Size
```
Definition mipMapImageDataSizeTotal (m : mipMapList) : nat :=
mipMapImageDataSizeTotalAux (mipMaps m).
```
The uncompressed size of a mipmap should be non-zero. This property is implicit in the definitions above; images must be of a non-zero width and height, and there are no channel layouts where the sizes of the channels sum to zero.
The compressed size of a mipmap should be non-zero. This property is implicit in the definitions above; images must be of a non-zero width and height, and there are no channel layouts where the sizes of the channels sum to zero.
## 4.13. Array Mipmaps
A 2D array texture consists of a non-empty sequence of **array mipmaps**. Array mipmaps are very similar to [mipmaps](#id_b8d20538-e4ac-4674-aa43-d5ab93c07149) with the primary difference that, for a texture with **n** array **layers**, each array mipmap **level** stores a sequence of **n** images of the same size. This facilitates a common implementation pattern where textures are progressively streamed onto the GPU starting with the array layers in the highest mipmap levels first.
#### 4.13.2. Array Mipmaps Arrangement
An array mipmap is uniquely identified with a **level** and a **layer**.
#### 4.13.4. ArrayMipMap Index
```
Inductive arrayMipMapIndexT : Set := ArrayMipMapIndex {
arrayMipMapLevel : nat;
arrayMipMapLayer : nat;
}.
```
An array mipmap stores an **offset** indicating the start of the actual image data for the mipmap relative to the first octet of the first mipmap declaration. An array mipmap also stores the [compressed size](#id_8f83a47a-986e-4dba-bfd7-720641cee3a9) and uncompressed size of the image data, along with a [CRC32](https://en.wikipedia.org/wiki/Cyclic_redundancy_check) checksum of the **uncompressed** data. A CRC32 value of **0** indicates that no checksum is available. For uncompressed data, the compressed and uncompressed sizes must equal the size of the uncompressed data.
#### 4.13.6. ArrayMipMap
```
Inductive arrayMipMap : Set := ArrayMipMap {
arrayMipMapIndex : arrayMipMapIndexT;
arrayMipMapOffset : nat;
arrayMipMapSizeCompressed : nat;
arrayMipMapSizeUncompressed : nat;
arrayMipMapCRC32 : nat
}.
```
The number of layers present in an array mipmap must equal the **sizeZ** value defined in the [image info](#id_3dde6403-729d-4eaa-9179-17d9a9fbe7a6), and it follows that all array mipmaps must contain the same number of layers.
#### 4.13.8. ArrayMipMap Layer Count For Level
```
Fixpoint arrayMipMapLayerCountForLevel
(level : nat)
(m : list arrayMipMap)
: nat :=
match m with
| [] => 0
| (x :: xs) =>
match Nat.eq_dec (arrayMipMapLevel (arrayMipMapIndex x)) level with
| left _ => 1 + (arrayMipMapLayerCountForLevel level xs)
| right _ => (arrayMipMapLayerCountForLevel level xs)
end
end.
```
#### 4.13.9. ArrayMipMap Levels
```
Definition arrayMipMapLevels (m : list arrayMipMap) : list nat :=
nodup Nat.eq_dec (map (fun k => arrayMipMapLevel (arrayMipMapIndex k)) m).
```
#### 4.13.10. ArrayMipMap Levels Count Equality
```
Definition arrayMipMapsHaveSameLayers : (list arrayMipMap) -> nat -> nat -> Prop :=
fun m level0 level1 =>
In level0 (arrayMipMapLevels m) ->
In level1 (arrayMipMapLevels m) ->
arrayMipMapLayerCountForLevel level0 m = arrayMipMapLayerCountForLevel level1 m.
```
Array mipmap sequences are stored such that the data for the mipmap with the highest level is encountered **first**, whilst the data for the mipmap with level **0** is encountered **last**. Within a given level, images are stored such that the data for layer **0** is encountered **first**, whilst the data for the highest layer is encountered **last**. The proposition **arrayMipMapIndexOrd** formally specifies the ordering for level/layer pairs, whilst the **arrayMipMapIndicesSorted** proposition formally specifies the conditions under which lists of level/layer pairs are considered to be ordered.
#### 4.13.12. ArrayMipMap Index Ordering
```
Inductive arrayMipMapIndexOrd : arrayMipMapIndexT -> arrayMipMapIndexT -> Prop :=
| AMMIOrdEq : forall i0 i1,
i0 = i1 -> arrayMipMapIndexOrd i0 i1
| AMMIOrdLevelEq : forall i0 i1,
arrayMipMapLevel i0 = arrayMipMapLevel i1 ->
arrayMipMapLayer i0 < arrayMipMapLayer i1 ->
arrayMipMapIndexOrd i0 i1
| AMIIOrdLevelLt : forall i0 i1,
arrayMipMapLevel i1 < arrayMipMapLevel i0 ->
arrayMipMapIndexOrd i0 i1.
```
#### 4.13.13. ArrayMipMap Index List Sorted
```
Inductive arrayMipMapIndicesSorted : list arrayMipMapIndexT -> Prop :=
| AMMIOne : forall m, arrayMipMapIndicesSorted [m]
| AMMICons : forall mmx mmy mxs,
arrayMipMapIndexOrd mmx mmy ->
arrayMipMapIndicesSorted (mmy :: mxs) ->
arrayMipMapIndicesSorted (mmx :: mmy :: mxs).
```
#### 4.13.14. ArrayMipMap Sequence
```
Inductive arrayMipMapList : Set := ArrayMipMapList {
arrayMipMaps : list arrayMipMap;
arrayMipMapIndicesAreSorted : arrayMipMapIndicesSorted (map arrayMipMapIndex arrayMipMaps);
arrayMipMapOffsetAreSorted : arrayMipMapOffsetsSorted arrayMipMaps;
arrayMipMapSameLayers : forall level0 level1, arrayMipMapsHaveSameLayers arrayMipMaps level0 level1
}.
```
The proposition **arrayMipMapOffsetsSorted** declares that, for a given array mipmap **m**, the offset of **m** plus the compressed size of **m**, must be less than the offset of the next mipmap in the sequence.
#### 4.13.16. ArrayMipMap Offsets Sorted
```
Inductive arrayMipMapOffsetsSorted : list arrayMipMap -> Prop :=
| AMMSizeOne : forall m, arrayMipMapOffsetsSorted [m]
| AMMSizeCons : forall mm0 mm1 mxs,
((arrayMipMapOffset mm1) + (arrayMipMapSizeCompressed mm1)) < (arrayMipMapOffset mm0) ->
arrayMipMapOffsetsSorted (mm0 :: mxs) ->
arrayMipMapOffsetsSorted (mm1 :: mm0 :: mxs).
```
Given a base image of size **(sizeX, sizeY)**, the size of the mipmap at level **n** is given by **(sizeX / 2ⁿ, sizeY / 2ⁿ)**. Mipmap images are required to be of a size **>= 2** on the X and Y axes. Note that this restriction does **not** apply to the base image; a base image with a size of 1 on any axis simply cannot have anything but a level 0 mipmap.
#### 4.13.18. Array MipMap Size
```
Inductive arrayMipMapImageSize : Set := ArrayMipMapImageSize {
ammSizeX : nat;
ammSizeY : nat;
ammSizeXRange : 1 < ammSizeX;
ammSizeYRange : 1 < ammSizeY;
}.
```
#### 4.13.19. Array MipMap Size Calculation
```
Definition arrayMipMapSize
(level : nat)
(imageSize : imageSize3D)
(levelRange : 0 < level)
: option arrayMipMapImageSize :=
let sx := (sizeX imageSize) / 2 ^ level in
let sy := (sizeY imageSize) / 2 ^ level in
match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with
| (ReflectT _ xt, ReflectT _ yt) => Some (ArrayMipMapImageSize sx sy xt yt)
| (_, _) => None
end.
```
The total size required to hold the image data for all mipmaps is effectively equal to the offset of the largest mipmap, plus the compressed size of the mipmap, rounded up to the required alignment of the image data.
#### 4.13.21. Array MipMap Data Size (Aux)
```
Fixpoint arrayMipMapImageDataSizeTotalAux (m : list arrayMipMap) : nat :=
match m with
| [] => 0
| (x :: []) => (arrayMipMapOffset x) + (arrayMipMapSizeCompressed x)
| (x :: xs) => arrayMipMapImageDataSizeTotalAux xs
end.
```
#### 4.13.22. Array MipMap Data Size
```
Definition arrayMipMapImageDataSizeTotal (m : arrayMipMapList) : nat :=
arrayMipMapImageDataSizeTotalAux (arrayMipMaps m).
```
The uncompressed size of a mipmap should be non-zero. This property is implicit in the definitions above; images must be of a non-zero width and height, and there are no channel layouts where the sizes of the channels sum to zero.
The compressed size of a mipmap should be non-zero. This property is implicit in the definitions above; images must be of a non-zero width and height, and there are no channel layouts where the sizes of the channels sum to zero.
## 4.14. Cube Mipmaps
A cube texture consists of a non-empty sequence of **cube mipmaps**. Cube mipmaps are very similar to [mipmaps](#id_b8d20538-e4ac-4674-aa43-d5ab93c07149) with the primary difference that each cube mipmap **level** stores a sequence of **6** images of the same size representing the faces of the cube.
#### 4.14.2. Cube Mipmaps Arrangement
Cube textures define an axis-aligned cube, with each of the six images in any given mipmap level defining each of the six axis-aligned cube faces. For example, when we refer to the **positive X** face of the cube, we are referring to the face of the cube that points towards positive infinity on the X axis. Each cube map face stores an **offset** indicating the start of the actual image data for the face relative to the first octet of the first mipmap declaration. A face also stores the [compressed size](#id_8f83a47a-986e-4dba-bfd7-720641cee3a9) and uncompressed size of the image data, along with a [CRC32](https://en.wikipedia.org/wiki/Cyclic_redundancy_check) checksum of the **uncompressed** data. A CRC32 value of **0** indicates that no checksum is available. For uncompressed data, the compressed and uncompressed sizes must equal the size of the uncompressed data.
#### 4.14.4. CubeMap Face
```
Inductive cubeMapFace : Set := CubeMapFace {
cubeFaceOffset : nat;
cubeFaceSizeCompressed : nat;
cubeFaceSizeUncompressed : nat;
cubeFaceCRC32 : nat
}.
```
A single cube mipmap level stores the sequence of six cube faces in the following order: **x-positive**, **x-negative**, **y-positive**, **y-negative**, **z-positive**, **z-negative**. Cube mipmap sequences are stored such that the data for the mipmap with the highest level is encountered **first**, whilst the data for the mipmap with level **0** is encountered **last**. This facilitates a common implementation pattern where textures are progressively streamed onto the GPU starting with the highest mipmap levels first. The proposition **cubeMipMapListIsSorted** declares the conditions that indicate that a sequence of cube mipmap levels is correctly ordered.
#### 4.14.6. CubeMap Level
```
Inductive cubeMipMap : Set := CubeMipMap {
cubeMapLevel : nat;
cubeMapFaceXPos : cubeMapFace;
cubeMapFaceXNeg : cubeMapFace;
cubeMapFaceYPos : cubeMapFace;
cubeMapFaceYNeg : cubeMapFace;
cubeMapFaceZPos : cubeMapFace;
cubeMapFaceZNeg : cubeMapFace
}.
```
#### 4.14.7. CubeMap Ordering
```
Inductive cubeMipMapListIsSorted : list cubeMipMap -> Prop :=
| CubeOne : forall m, cubeMipMapListIsSorted [m]
| CubeCons : forall mm0 mm1 mxs,
cubeMapLevel mm1 = S (cubeMapLevel mm0) ->
cubeMipMapListIsSorted (mm0 :: mxs) ->
cubeMipMapListIsSorted (mm1 :: mm0 :: mxs).
```
The **extent** of a cube face is defined as the offset of the face plus the compressed size of the face. The **extent** of a cube mipmap level is the extent of the last face in the sequence (the **z-negative** face). This **extent** is effectively the smallest region that can contain all six faces of a level. The proposition **cubeOffsetsSorted** declares that, for a given cube mipmap **m**, the extents of the faces of **m** must be ordered correctly, and must be less than the offset of the first face of the next mipmap in the sequence.
#### 4.14.9. CubeMap Extent
```
Definition cubeFaceExtent (f : cubeMapFace) : nat :=
cubeFaceOffset f + cubeFaceSizeCompressed f.
```
#### 4.14.10. CubeMap Offset Ordering
```
Inductive cubeOffsetsSorted : list cubeMipMap -> Prop :=
| CMMSizeOne : forall m,
cubeFaceExtent (cubeMapFaceXPos m) < cubeFaceOffset (cubeMapFaceXNeg m) ->
cubeFaceExtent (cubeMapFaceXNeg m) < cubeFaceOffset (cubeMapFaceYPos m) ->
cubeFaceExtent (cubeMapFaceYPos m) < cubeFaceOffset (cubeMapFaceYNeg m) ->
cubeFaceExtent (cubeMapFaceYNeg m) < cubeFaceOffset (cubeMapFaceZPos m) ->
cubeFaceExtent (cubeMapFaceZPos m) < cubeFaceOffset (cubeMapFaceZNeg m) ->
cubeOffsetsSorted [m]
| CMMSizeCons : forall mm0 mm1 mxs,
cubeFaceExtent (cubeMapFaceZNeg mm1) < cubeFaceOffset (cubeMapFaceXPos mm0) ->
cubeOffsetsSorted (mm0 :: mxs) ->
cubeOffsetsSorted (mm1 :: mm0 :: mxs).
```
Given a base image of size **(sizeX, sizeY)**, the size of the mipmap at level **n** is given by **(sizeX / 2ⁿ, sizeY / 2ⁿ)**. Mipmap images are required to be of a size **>= 2** on the X and Y axes. Note that this restriction does **not** apply to the base image; a base image with a size of 1 on any axis simply cannot have anything but a level 0 mipmap.
The total size required to hold the image data for all mipmaps is effectively equal to the extent of the largest mipmap rounded up to the required alignment of the image data.
#### 4.14.13. CubeMap Size (Aux)
```
Fixpoint cubeMipMapImageDataSizeTotalAux (m : list cubeMipMap) : nat :=
match m with
| [] => 0
| (x :: []) => cubeFaceExtent (cubeMapFaceZNeg x)
| (x :: xs) => cubeMipMapImageDataSizeTotalAux xs
end.
```
#### 4.14.14. CubeMap Size
```
Definition cubeMipMapImageDataSizeTotal (m : cubeMipMapList) : nat :=
cubeMipMapImageDataSizeTotalAux (cubeMipMaps m).
```
The uncompressed size of a mipmap should be non-zero. This property is implicit in the definitions above; images must be of a non-zero width and height, and there are no channel layouts where the sizes of the channels sum to zero.
The compressed size of a mipmap should be non-zero. This property is implicit in the definitions above; images must be of a non-zero width and height, and there are no channel layouts where the sizes of the channels sum to zero.
## 4.15. Metadata
A texture 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 **calino** is in the form of UTF-8 encoded keys and values. Metadata that requires more structure than this can be provided by custom [sections](#id_eb66b381-4c70-4246-95e9-d3a61e19ac4c) that will be ignored by software that does not know how to interpret them.
#### 4.15.2. Metadata Value
```
Inductive metadataValue : Set := MetadataValue {
mKey : string;
mValue : string
}.
```
#### 4.15.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.
## 4.16. Textures
### 4.16.1. Textures
An **texture** is a [2D texture](#id_71f3233f-43eb-4ea1-96d4-bc1192553239), an [array texture](#id_60f44a91-49a1-4ee9-9659-45ed94051828), or a [cube texture](#id_63a0f8cf-4a48-47bc-aa83-b35d631ad243).
#### 4.16.1.2. Texture
```
Inductive texture : Set :=
| TTexture2D : texture2d -> texture
| TTextureArray : textureArray -> texture
| TTextureCube : textureCube -> texture.
```
### 4.16.2. 2D Texture
A 2D texture aggregates [image information](#id_4ae63d09-ce2d-46d4-a8eb-f1f9ad382ee8) and a sequence of [mipmaps](#id_b8d20538-e4ac-4674-aa43-d5ab93c07149) for a single two-dimensional texture.
2D textures must have [sizeZ](#id_3dde6403-729d-4eaa-9179-17d9a9fbe7a6) values equal to **1**.
#### 4.16.2.3. 2D Texture
```
Inductive texture2d : Set := Texture2D {
i2dInfo : imageInfo;
i2dMipMaps : mipMapList;
i2dSize : 1 = imageSizeZ i2dInfo
}.
```
### 4.16.3. Array Texture
An array texture aggregates [image information](#id_4ae63d09-ce2d-46d4-a8eb-f1f9ad382ee8) and a sequence of [array mipmaps](#id_f4b4fff9-a443-4430-a37b-ed939e606bef) for a single two-dimensional array texture.
Array textures must have [sizeZ](#id_3dde6403-729d-4eaa-9179-17d9a9fbe7a6) values equal to the number of [array layers](#id_cb73941f-ab0c-46cd-a8a2-94ca912eda3a) in the texture.
#### 4.16.3.3. Array Texture
```
Inductive textureArray : Set := TextureArray {
iaInfo : imageInfo;
iaMipMaps : arrayMipMapList;
iaSize : 1 <= imageSizeZ iaInfo
}.
```
### 4.16.4. 3D Texture
3D textures are not yet specified.
### 4.16.5. Cube Texture
A cube texture aggregates [image information](#id_4ae63d09-ce2d-46d4-a8eb-f1f9ad382ee8) and a sequence of [cube mipmaps](#id_e8125add-3c83-47a1-9997-1f15867068dd) for a single cube texture.
Cube textures must have [sizeZ](#id_3dde6403-729d-4eaa-9179-17d9a9fbe7a6) values equal to **1**.
#### 4.16.5.3. Cube Image
```
Inductive textureCube : Set := TextureCube {
icubeInfo : imageInfo;
icubeMipMaps : cubeMipMapList;
icubeSize : 1 = imageSizeZ icubeInfo
}.
```
## 5. The Calino Binary Encoding
## 5.1. Binary Expressions
### 5.1.1. Overview
The **calino** texture 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](#id_73066219-7f6d-4809-b87c-897be98b4a6b) are mapped to binary expressions.
### 5.1.2. Expressions
A **term** in the binary expression language is described by the following inductive type:
#### 5.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 **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**:
#### 5.1.2.11. 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.
```
#### 5.1.2.12. 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.
```
#### 5.1.2.13. Binary Expression Size Theorem
```
Theorem binarySizeMultiple4 : forall b, binarySize (b) mod 4 = 0.
```
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](#id_1f0b8741-bd88-4925-b880-f5dd6063ccf1) fixed to a multiple of 4:
#### 5.1.2.15. Binary Expression Size Padded 16
```
Definition binarySizePadded16 (b : binaryExp) : nat :=
asMultipleOf16 (binarySize b).
```
#### 5.1.2.16. asMultipleOf4
```
Definition asMultipleOf4 (size : nat) : nat :=
asMultipleOf size 4 p0not4.
```
Binary expressions are encoded as streams of **streamE** values:
#### 5.1.2.18. 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 **Vu64 n** represents an unsigned 64-bit integer in [big-endian](#id_af4e0973-1be2-4b0f-beca-1190cf84aea3) order.
An expression **Vu32 n** represents an unsigned 32-bit integer in [big-endian](#id_af4e0973-1be2-4b0f-beca-1190cf84aea3) 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:
#### 5.1.2.23. 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 Alignment.p0not4)
| BiUTF8 s => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 Alignment.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.
```
#### 5.1.2.24. 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:
#### 5.1.2.26. Well-Formed Stream (Informal rules)
- **s** is empty.
- **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:
#### 5.1.2.28. 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.
#### 5.1.2.30. Binary Expression Encoding Well-Formed
```
Theorem binaryEvalStreamsWellFormed : forall b,
streamWellFormed (binaryEval b).
Proof.
(* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
```
#### 5.1.2.31. 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.
```
## 5.2. File Header
All **calino** texture files begin with the following fixed length header:
#### 5.2.2. File Header
```
Definition binaryExpFileHeader : binaryExp := BiRecord [
("id", u64 0x89434C4E0D0A1A0A);
("versionMajor", u32 2);
("versionMinor", u32 0)
].
```
The **id** field must always be set to the 64-bit unsigned big-endian value **0x89434C4E0D0A1A0A**.
The **versionMajor** field must be set to **2** for files targeting this version of the specification.
The **versionMinor** field must be set to **0** for files targeting this version of the specification.
## 5.3. File Identifiers
By convention, **calino** texture files use the filename suffix **.ctf**. The suffix is advisory only; consumers MUST determine the type of a file by inspecting the file header **id** field, not by the filename.
The media type for **calino** texture files is **application/vnd.io7m.calino**.
## 5.4. Sections
**calino** texture 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 between zero and **15** (inclusive) 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, plus padding, to find the next section.
The first section in a **calino** texture must be an [image information](#id_bc0e7016-7dab-4edb-a4c9-2b1492da0225) section.
Following an [image information](#id_bc0e7016-7dab-4edb-a4c9-2b1492da0225) section, **calino** texture files must contain exactly one of any of the various texture data sections.
**calino** texture files must end with exactly one [End](#id_40d09b06-b6de-4052-92fe-2829942518c9) section.
Sections must start at offsets that are evenly divisible by 16.
The following standard sections are defined by this version of the specification:
#### 5.4.7. Standard Sections
| Identifier | Description |
| --- | --- |
| [0x434C4E49494E464F](#id_bc0e7016-7dab-4edb-a4c9-2b1492da0225) | Image information. |
| [0x434C4E5F49324421](#id_8321ef71-e529-4764-abf1-e678e42c03af) | Image data for 2D textures. |
| [0x434C4E5F41525221](#id_a91529c1-d7c4-4e6e-abcb-bfeb3d536aba) | Image data for array textures. |
| [0x434C4E5F43554245](#id_df607ad1-a586-4a3f-b8bc-f322142056f9) | Image data for cube textures. |
| [0x434C4E5F4D455441](#id_16fddeaf-9d7f-437b-8662-01e6975f6249) | Key/value metadata. |
| [0x434C4E5F454E4421](#id_40d09b06-b6de-4052-92fe-2829942518c9) | File terminator. |
## 5.5. Image Information
### 5.5.1. Description
[Image information](#id_4ae63d09-ce2d-46d4-a8eb-f1f9ad382ee8) values are translated to binary expressions as follows:
#### 5.5.1.2. Image Information Encoding
```
Definition binaryExpImageInfo (i : imageInfo) : binaryExp := BiRecord [
("sizeX", u32 (imageSizeX i));
("sizeY", u32 (imageSizeY i));
("sizeZ", u32 (imageSizeZ i));
("channelsLayout", utf8 (descriptorOf (imageChannelsLayout i)));
("channelsType", utf8 (descriptorOf (imageChannelsType i)));
("compression", binaryExpCompression (imageCompressionMethod i));
("superCompression", binaryExpSuperCompression (imageSuperCompressionMethod i));
("coordinateSystem", utf8 (descriptorOf (imageCoordinateSystem i)));
("colorSpace", utf8 (descriptorOf (imageColorSpace i)));
("flags", BiArray (map (utf8 ∘ descriptorOf) (imageFlagSet i)));
("byteOrder", utf8 (descriptorOf (imageByteOrder i)))
].
```
[Compression](#id_bd75557c-d8d2-4522-93b3-e29d78d436b7) declarations are translated to binary expressions as follows:
#### 5.5.1.4. Compression Encoding
```
Definition binaryExpCompression (c : compressionMethod) : binaryExp := BiRecord [
("descriptor", utf8 (descriptorOf c));
("sectionIdentifier", u64 (compressionSectionIdentifier c));
("blockSizeX", u32 (compressionBlockSizeX c));
("blockSizeY", u32 (compressionBlockSizeY c));
("blockAlignment", u32 (compressionBlockAlignment c))
].
```
[Super compression](#id_8f83a47a-986e-4dba-bfd7-720641cee3a9) declarations are translated to binary expressions as follows:
#### 5.5.1.6. Super Compression Encoding
```
Definition binaryExpSuperCompression (c : superCompressionMethod) : binaryExp := BiRecord [
("descriptor", utf8 (descriptorOf c));
("sectionIdentifier", u64 (superCompressionSectionIdentifier c))
].
```
Image information must be encoded into a [section](#id_eb66b381-4c70-4246-95e9-d3a61e19ac4c) with identifier **0x434C4E49494E464F** as follows:
#### 5.5.1.8. Image Information Section
```
Definition binaryExpImageInfoSection (i : imageInfo) : binaryExp := BiRecord [
("id", u64 0x434C4E49494E464F);
("size", u64 (binarySize (binaryExpImageInfo i)));
("data", binaryExpImageInfo i)
].
```
### 5.5.2. Cardinality
An image information section can appear in a **calino** texture file at most once.
## 5.6. 2D Textures
### 5.6.1. Description
[2D texture](#id_71f3233f-43eb-4ea1-96d4-bc1192553239) values are translated to binary expressions as follows:
#### 5.6.1.2. MipMap Encoding
```
Definition binaryExpMipMap (m : mipMap) : binaryExp := BiRecord [
("mipMapLevel", u32 (mipMapLevel m));
("mipMapDataOffset", u64 (mipMapOffset m));
("mipMapSizeUncompressed", u64 (mipMapSizeUncompressed m));
("mipMapSizeCompressed", u64 (mipMapSizeCompressed m));
("mipMapCRC32", u32 (mipMapCRC32 m))
].
```
#### 5.6.1.3. MipMaps Encoding
```
Definition binaryExpMipMaps (m : mipMapList) : binaryExp :=
BiArray (map binaryExpMipMap (mipMaps m)).
```
#### 5.6.1.4. Image 2D Encoding
```
Definition binaryExpImage2D
(i : imageInfo)
(m : mipMapList)
: binaryExp :=
let imageDataStart := mipMapOffset (mipMapFirst m) in
let encMips := binaryExpMipMaps m in
let encMipsSize := binarySize encMips in
let encMipsPad := imageDataStart - encMipsSize in
let imageSize := mipMapImageDataSizeTotal m in
let imageSize16 := asMultipleOf16 imageSize in
BiRecord [
("mipMaps", encMips);
("mipPad", BiReserve encMipsPad);
("mipData", BiReserve imageSize16)
].
```
Informally, an array of [mipmap](#id_b8d20538-e4ac-4674-aa43-d5ab93c07149) descriptions are serialized, followed by any required padding to reach the offset value declared by the first mipmap, followed by the image data for each mipmap in the order specified by the mipmap descriptions.
2D textures must be encoded into a [section](#id_eb66b381-4c70-4246-95e9-d3a61e19ac4c) with identifier **0x434C4E5F49324421** as follows:
#### 5.6.1.7. Image 2D Section
```
Definition binaryExpImage2DSection
(i : imageInfo)
(m : mipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F49324421);
("size", u64 (binarySize (binaryExpImage2D i m)));
("data", binaryExpImage2D i m)
].
```
### 5.6.2. Cardinality
A 2D texture section can appear in a **calino** texture file at most once.
## 5.7. Array Textures
### 5.7.1. Description
[Array texture](#id_4947de09-7eb6-4439-90e1-1b94adcf8d0a) values are translated to binary expressions as follows:
#### 5.7.1.2. Array MipMap Encoding
```
Definition binaryExpArrayMipMap (m : arrayMipMap) : binaryExp := BiRecord [
("arrayMipMapLevel", u32 (arrayMipMapLevel (arrayMipMapIndex m)));
("arrayMipMapLayer", u32 (arrayMipMapLayer (arrayMipMapIndex m)));
("arrayMipMapDataOffset", u64 (arrayMipMapOffset m));
("arrayMipMapSizeUncompressed", u64 (arrayMipMapSizeUncompressed m));
("arrayMipMapSizeCompressed", u64 (arrayMipMapSizeCompressed m));
("arrayMipMapCRC32", u32 (arrayMipMapCRC32 m))
].
```
#### 5.7.1.3. Array MipMaps Encoding
```
Definition binaryExpArrayMipMaps (m : arrayMipMapList) : binaryExp :=
BiArray (map binaryExpArrayMipMap (arrayMipMaps m)).
```
#### 5.7.1.4. Array Image Encoding
```
Definition binaryExpImageArray
(i : imageInfo)
(m : arrayMipMapList)
: binaryExp :=
let imageDataStart := arrayMipMapOffset (arrayMipMapFirst m) in
let encMips := binaryExpArrayMipMaps m in
let encMipsSize := binarySize encMips in
let encMipsPad := imageDataStart - encMipsSize in
let imageSize := arrayMipMapImageDataSizeTotal m in
let imageSize16 := asMultipleOf16 imageSize in
BiRecord [
("arrayMipMaps", encMips);
("arrayMipPad", BiReserve encMipsPad);
("arrayMipData", BiReserve imageSize16)
].
```
Informally, an array of [array mipmap](#id_f4b4fff9-a443-4430-a37b-ed939e606bef) descriptions are serialized, followed by any required padding to reach the offset value declared by the first mipmap, followed by the image data for each mipmap in the order specified by the mipmap descriptions.
Array textures must be encoded into a [section](#id_eb66b381-4c70-4246-95e9-d3a61e19ac4c) with identifier **0x434C4E5F41525221** as follows:
#### 5.7.1.7. Array Image Section
```
Definition binaryExpImageArraySection
(i : imageInfo)
(m : arrayMipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F41525221);
("size", u64 (binarySize (binaryExpImageArray i m)));
("data", binaryExpImageArray i m)
].
```
### 5.7.2. Cardinality
An array texture section can appear in a **calino** texture file at most once.
## 5.8. Cube Textures
### 5.8.1. Description
[Cube texture](#id_63a0f8cf-4a48-47bc-aa83-b35d631ad243) values are translated to binary expressions as follows:
#### 5.8.1.2. Cube MipMap Face Encoding
```
Definition binaryExpCubeMipMapFace (m : cubeMapFace) : binaryExp := BiRecord [
("cubeFaceDataOffset", u64 (cubeFaceOffset m));
("cubeFaceSizeUncompressed", u64 (cubeFaceSizeUncompressed m));
("cubeFaceSizeCompressed", u64 (cubeFaceSizeCompressed m));
("cubeFaceCRC32", u32 (cubeFaceCRC32 m))
].
```
#### 5.8.1.3. Cube MipMap Encoding
```
Definition binaryExpCubeMipMap (m : cubeMipMap) : binaryExp := BiRecord [
("cubeMipMapLevel", u32 (cubeMapLevel m));
("cubeMipMapFacePosX", binaryExpCubeMipMapFace (cubeMapFaceXPos m));
("cubeMipMapFaceNegX", binaryExpCubeMipMapFace (cubeMapFaceXNeg m));
("cubeMipMapFacePosY", binaryExpCubeMipMapFace (cubeMapFaceYPos m));
("cubeMipMapFaceNegY", binaryExpCubeMipMapFace (cubeMapFaceYNeg m));
("cubeMipMapFacePosZ", binaryExpCubeMipMapFace (cubeMapFaceZPos m));
("cubeMipMapFaceNegZ", binaryExpCubeMipMapFace (cubeMapFaceZNeg m))
].
```
#### 5.8.1.4. Cube MipMaps Encoding
```
Definition binaryExpCubeMipMaps (m : cubeMipMapList) : binaryExp :=
BiArray (map binaryExpCubeMipMap (cubeMipMaps m)).
```
#### 5.8.1.5. Image Cube Encoding
```
Definition binaryExpImageCubeMap
(i : imageInfo)
(m : cubeMipMapList)
: binaryExp :=
let imageDataStart := cubeFaceOffset (cubeMapFaceXPos (cubeMipMapsFirst m)) in
let encMips := binaryExpCubeMipMaps m in
let encMipsSize := binarySize encMips in
let encMipsPad := imageDataStart - encMipsSize in
let imageSize := cubeMipMapImageDataSizeTotal m in
let imageSize16 := asMultipleOf16 imageSize in
BiRecord [
("cubeMipMaps", encMips);
("cubeMipPad", BiReserve encMipsPad);
("cubeMipData", BiReserve imageSize16)
].
```
Informally, an array of [mipmap](#id_e8125add-3c83-47a1-9997-1f15867068dd) descriptions are serialized, followed by any required padding to reach the offset value declared by the first mipmap, followed by the image data for each mipmap in the order specified by the mipmap descriptions.
Cube textures must be encoded into a [section](#id_eb66b381-4c70-4246-95e9-d3a61e19ac4c) with identifier **0x434C4E5F43554245** as follows:
#### 5.8.1.8. Image Cube Section
```
Definition binaryExpImageCubeSection
(i : imageInfo)
(m : cubeMipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F43554245);
("size", u64 (binarySize (binaryExpImageCubeMap i m)));
("data", binaryExpImageCubeMap i m)
].
```
### 5.8.2. Cardinality
A cube texture section can appear in a **calino** texture file at most once.
## 5.9. Metadata
### 5.9.1. Description
[Metadata](#id_eb8b3eb5-29b1-411c-a9ae-754d1a4b2940) values are translated to binary expressions as follows:
#### 5.9.1.2. Metadata Value Encoding
```
Definition binaryExpMetadataValue (m : metadataValue) : binaryExp := BiRecord [
("key", utf8 (mKey m));
("value", utf8 (mValue m))
].
```
#### 5.9.1.3. Metadata Encoding
```
Definition binaryExpMetadata (m : metadata) : binaryExp :=
BiArray (map binaryExpMetadataValue (mValues m)).
```
Metadata must be encoded into a [section](#id_eb66b381-4c70-4246-95e9-d3a61e19ac4c) with identifier **0x434C4E5F4D455441** as follows:
#### 5.9.1.5. Metadata Section
```
Definition binaryExpMetadataSection (m : metadata) : binaryExp := BiRecord [
("id", u64 0x434C4E5F4D455441);
("size", u64 (binarySize (binaryExpMetadata m)));
("data", binaryExpMetadata m)
].
```
### 5.9.2. Cardinality
A metadata section can appear in a **calino** texture file at most once.
## 5.10. End
### 5.10.1. Description
**calino** texture files must end with exactly one **End** section, which has the identifier **0x434C4E5F454E4421** and must be of size **0**.
End sections are encoded as follows:
#### 5.10.1.3. End Encoding
```
Definition binaryEndSection : binaryExp := BiRecord [
("id", u64 0x434c4e5f454e4421);
("size", u64 0)
].
```
There should be no trailing data in the texture file after the **End** section. Implementations must stop consuming data after the **End** section and effectively ignore any trailing data that might be present.
### 5.10.2. Cardinality
An **End** section must appear in a **calino** texture file exactly once, and must be the last section present in the file.
## 5.11. Examples
A metadata section containing the value **Metadata [MetadataValue "K0" "VAL0"; MetadataValue "KEY1" "VAL1"]** will be encoded as the following sequence of octets:
#### 5.11.2. Example Metadata
```
43 4C 4E 5F 4D 45 54 41 ; Identifier 0x434C4E49494E464F
00 00 00 00 00 00 00 30 ; Section is 48 bytes
00 00 00 02 ; Size of metadata array is 2
00 00 00 02 ; Size of first key is 2
4B 30 00 00 ; Key is "K0" plus padding octets
00 00 00 04 ; Size of first value is 4
56 41 4C 30 ; Value is "VAL0", no padding required
00 00 00 04 ; Size of second key is 4
4B 45 59 31 ; Key is "KEY1", no padding required
00 00 00 04 ; Size of second value is 4
56 41 4C 31 ; Value is "VAL1", no padding required
00 00 00 00 00 00 00 00 00 00 00 00 ; 12 padding octets, so the size of the
; section is a multiple of 16
```
## 6. References
### 6.1. Normative References
The following references are normative. A well-formed implementation of the **calino** format must conform to the specifications cited below.
#### 6.1.2. Normative References
| Reference | Description | URI |
| --- | --- | --- |
| **IEEE754** | IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019 (July 2019). Also published as ISO/IEC/IEEE 60559:2020. | [Retrieval URI](https://standards.ieee.org/ieee/754/6210/) |
| **sRGB** | Default RGB colour space - sRGB, IEC 61966-2-1:1999. | [Retrieval URI](https://webstore.iec.ch/en/publication/6169) |
| **zlib** | ZLIB Compressed Data Format Specification, RFC 1950 (May 1996). The container format emitted by the DEFLATE supercompression method. | [Retrieval URI](https://www.rfc-editor.org/rfc/rfc1950.html) |
| **DEFLATE** | DEFLATE Compressed Data Format Specification, RFC 1951 (May 1996). The compression algorithm used within the zlib container. | [Retrieval URI](https://www.rfc-editor.org/rfc/rfc1951.html) |
| **LZ4** | The LZ4 compression algorithm. No published RFC or IEC standard exists; the project page is the primary source. | [Retrieval URI](http://lz4.github.io/lz4/) |
| **Unicode** | The Unicode Standard. String values in the format are Unicode text. | [Retrieval URI](https://www.unicode.org) |
| **UTF-8** | UTF-8, a transformation format of ISO 10646, RFC 3629 (STD 63, November 2003). The byte encoding of Unicode string values. | [Retrieval URI](https://www.rfc-editor.org/rfc/rfc3629.html) |
| **Rocq** | The Rocq Theorem Prover - Reference Manual, Version 9.0.0. The formal model of the format is expressed in Rocq. | [Retrieval URI](https://rocq-prover.org/doc/V9.0.0/refman/index.html) |
### 6.2. Informative References
The following references are informative. They provide context, comparison, or supplementary material but are not requirements for a conformant **calino** implementation.
#### 6.2.2. Informative References
| Reference | Description | URI |
| --- | --- | --- |
| **BCn / DXT** | S3TC block-compression texture formats (BC1, BC2, and BC3, also known as DXT1, DXT3, and DXT5), and the related BC7 format. Proprietary (Microsoft); no public standard. | [Retrieval URI](https://en.wikipedia.org/wiki/S3TC) |
| **ETC** | Ericsson Texture Compression, including ETC1, ETC2, and EAC. | [Retrieval URI](https://en.wikipedia.org/wiki/Ericsson_Texture_Compression) |
| **ASTC** | Adaptive Scalable Texture Compression. | [Retrieval URI](https://en.wikipedia.org/wiki/Adaptive_scalable_texture_compression) |
## 7. Appendix A: History
### 7.1. Version 2.0
Version **2.0** of the specification corrected a mistake in the **1.0** specification with regard to the way that section sizes were specified. In version **1.0** of the specification, section sizes were specified as follows:
#### 7.1.2. Section Padding
```
Definition binaryExpImage2DSection
(i : imageInfo)
(m : mipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F49324421);
("size", u64 (binarySizePadded16 (binaryExpImage2D i m)));
("data", binaryExpImage2D i m)
].
```
However, the actual intention was to specify them as:
#### 7.1.4. Section No Padding
```
Definition binaryExpImage2DSection
(i : imageInfo)
(m : mipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F49324421);
("size", u64 (binarySize (binaryExpImage2D i m)));
("data", binaryExpImage2D i m)
].
```
In other words: Section sizes used to include the padding octets that are used to align the next section to a 16 octet boundary. Unfortunately, this then meant that there was ambiguity with regard to the number of padding octets that were used. In version **2.0** of the specification, the section size no longer includes the padding octets. This is a backwards-incompatible change in a number of places, because **1.0** parsers could fail when encountering corrected section size values.
Worse, the reference implementation of the **calino** specification actually already implemented the **2.0** behaviour. Therefore, the decision was made to release a new format version and deprecate **1.0**.
## 8. Appendix B: Sources
The full sources for the Rocq model underlying this specification are included here.
#### 8.2. Calino.v
```
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.
Require Import Calino.Divisible8.
Require Import Calino.StringUtility.
Require Import Calino.Descriptor.
Require Import Calino.ChannelDescription.
Require Import Calino.ChannelSemantic.
Require Import Calino.ChannelType.
Require Import Calino.Compression.
Require Import Calino.SuperCompression.
Require Import Calino.ColorSpace.
Require Import Calino.Flag.
Require Import Calino.ByteOrder.
Require Import Calino.CoordinateSystem.
Require Import Calino.ImageInfo.
Require Import Calino.MipMap.
Require Import Calino.Image.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.
Open Scope char_scope.
Open Scope nat_scope.
(*
Set Mangle Names.
*)
Example eightNotZero : 8 <> 0 := not_eq_sym (O_S 7).
Example R8 : channelDescription := channelDescriptionMake CSRed 8 eightNotZero.
Example G8 : channelDescription := channelDescriptionMake CSGreen 8 eightNotZero.
Example B8 : channelDescription := channelDescriptionMake CSBlue 8 eightNotZero.
Example A8 : channelDescription := channelDescriptionMake CSAlpha 8 eightNotZero.
Transparent R8.
Transparent G8.
Transparent B8.
Transparent A8.
Example R8_Div8 : channelDescriptionBitsDivisible8 R8 := eq_refl.
Example G8_Div8 : channelDescriptionBitsDivisible8 G8 := eq_refl.
Example B8_Div8 : channelDescriptionBitsDivisible8 B8 := eq_refl.
Example A8_Div8 : channelDescriptionBitsDivisible8 A8 := eq_refl.
Example R8_G8_B8_Channels : list channelDescription := [R8; G8; B8].
Example R8_G8_B8_NonEmpty := nil_cons (x := R8) (l := [G8;B8]).
Example R8_G8_B8_Div8 : Forall channelDescriptionBitsDivisible8 R8_G8_B8_Channels :=
Forall_cons R8 R8_Div8
(Forall_cons G8 G8_Div8
(Forall_cons B8 B8_Div8
(Forall_nil channelDescriptionBitsDivisible8))).
Example R8_G8_B8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked
(CLDUMake R8_G8_B8_Channels R8_G8_B8_NonEmpty R8_G8_B8_Div8).
Example SixteenNotZero : 16 <> 0 := not_eq_sym (O_S 15).
Example OneNotZero : 1 <> 0 := not_eq_sym (O_S 0).
Example ImageInfoR8G8B8 : imageInfo :=
ImageInfo
16
16
1
(conj SixteenNotZero (conj SixteenNotZero OneNotZero))
R8_G8_B8
CTFixedPointNormalizedUnsigned
CompressionUncompressed
SuperCompressionUncompressed
(CoordinateSystem AxisRIncreasingToward AxisSIncreasingRight AxisTIncreasingDown)
CSsRGB
[FlagAlphaPremultiplied]
ByteOrderLittle.
Example mipEx0 : mipMap := MipMap 0 0 3072 3072 0.
Example mipEx1 : mipMap := MipMap 1 0 768 768 0.
Example mipEx2 : mipMap := MipMap 2 0 192 192 0.
Example mipEx3 : mipMap := MipMap 3 0 48 48 0.
Transparent mipEx0.
Transparent mipEx1.
Transparent mipEx2.
Transparent mipEx3.
Example mipExList : list mipMap := [mipEx3; mipEx2; mipEx1; mipEx0].
Transparent mipExList.
Example mipExListSorted : mipMapListIsSorted mipExList.
Proof.
assert (mipMapLevel mipEx3 = S (mipMapLevel mipEx2)) as H3s2 by reflexivity.
assert (mipMapListIsSorted [mipEx2; mipEx1; mipEx0]) as Hs210.
assert (mipMapLevel mipEx2 = S (mipMapLevel mipEx1)) as H2s1 by reflexivity.
assert (mipMapListIsSorted [mipEx1; mipEx0]) as Hs10.
assert (mipMapLevel mipEx1 = S (mipMapLevel mipEx0)) as H1s0 by reflexivity.
assert (mipMapListIsSorted [mipEx0]) as Hs0.
apply MipsOne.
apply (MipsCons mipEx0 mipEx1 [] H1s0 Hs0).
apply (MipsCons mipEx1 mipEx2 [mipEx0] H2s1 Hs10).
apply (MipsCons mipEx2 mipEx3 [mipEx1;mipEx0] H3s2 Hs210).
Qed.
Example mipExListNonEmpty : nil <> mipExList.
Proof. discriminate. Qed.
Example ImageR8G8B8 : image :=
Image2D ImageInfoR8G8B8 (MipMapList mipExList mipExListNonEmpty mipExListSorted).
```
#### 8.3. Calino/ArrayMipMap.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Bool.Bool.
Require Import com.io7m.calino.ImageSize.
Import ListNotations.
Inductive arrayMipMapIndexT : Set := ArrayMipMapIndex {
arrayMipMapLevel : nat;
arrayMipMapLayer : nat;
}.
Inductive arrayMipMapIndexOrd : arrayMipMapIndexT -> arrayMipMapIndexT -> Prop :=
| AMMIOrdEq : forall i0 i1,
i0 = i1 -> arrayMipMapIndexOrd i0 i1
| AMMIOrdLevelEq : forall i0 i1,
arrayMipMapLevel i0 = arrayMipMapLevel i1 ->
arrayMipMapLayer i0 < arrayMipMapLayer i1 ->
arrayMipMapIndexOrd i0 i1
| AMIIOrdLevelLt : forall i0 i1,
arrayMipMapLevel i1 < arrayMipMapLevel i0 ->
arrayMipMapIndexOrd i0 i1.
Inductive arrayMipMapIndicesSorted : list arrayMipMapIndexT -> Prop :=
| AMMIOne : forall m, arrayMipMapIndicesSorted [m]
| AMMICons : forall mmx mmy mxs,
arrayMipMapIndexOrd mmx mmy ->
arrayMipMapIndicesSorted (mmy :: mxs) ->
arrayMipMapIndicesSorted (mmx :: mmy :: mxs).
Inductive arrayMipMap : Set := ArrayMipMap {
arrayMipMapIndex : arrayMipMapIndexT;
arrayMipMapOffset : nat;
arrayMipMapSizeCompressed : nat;
arrayMipMapSizeUncompressed : nat;
arrayMipMapCRC32 : nat
}.
Inductive arrayMipMapOffsetsSorted : list arrayMipMap -> Prop :=
| AMMSizeOne : forall m, arrayMipMapOffsetsSorted [m]
| AMMSizeCons : forall mm0 mm1 mxs,
((arrayMipMapOffset mm1) + (arrayMipMapSizeCompressed mm1)) < (arrayMipMapOffset mm0) ->
arrayMipMapOffsetsSorted (mm0 :: mxs) ->
arrayMipMapOffsetsSorted (mm1 :: mm0 :: mxs).
Fixpoint arrayMipMapLayerCountForLevel
(level : nat)
(m : list arrayMipMap)
: nat :=
match m with
| [] => 0
| (x :: xs) =>
match Nat.eq_dec (arrayMipMapLevel (arrayMipMapIndex x)) level with
| left _ => 1 + (arrayMipMapLayerCountForLevel level xs)
| right _ => (arrayMipMapLayerCountForLevel level xs)
end
end.
Definition arrayMipMapLevels (m : list arrayMipMap) : list nat :=
nodup Nat.eq_dec (map (fun k => arrayMipMapLevel (arrayMipMapIndex k)) m).
Definition arrayMipMapsHaveSameLayers : (list arrayMipMap) -> nat -> nat -> Prop :=
fun m level0 level1 =>
In level0 (arrayMipMapLevels m) ->
In level1 (arrayMipMapLevels m) ->
arrayMipMapLayerCountForLevel level0 m = arrayMipMapLayerCountForLevel level1 m.
Inductive arrayMipMapList : Set := ArrayMipMapList {
arrayMipMaps : list arrayMipMap;
arrayMipMapIndicesAreSorted : arrayMipMapIndicesSorted (map arrayMipMapIndex arrayMipMaps);
arrayMipMapOffsetAreSorted : arrayMipMapOffsetsSorted arrayMipMaps;
arrayMipMapSameLayers : forall level0 level1, arrayMipMapsHaveSameLayers arrayMipMaps level0 level1
}.
Inductive arrayMipMapImageSize : Set := ArrayMipMapImageSize {
ammSizeX : nat;
ammSizeY : nat;
ammSizeXRange : 1 < ammSizeX;
ammSizeYRange : 1 < ammSizeY;
}.
Lemma arrayMipMapsNonEmpty : forall (m : arrayMipMapList),
[] <> arrayMipMaps m.
Proof.
intros m.
destruct (arrayMipMapOffsetAreSorted m).
- discriminate.
- discriminate.
Qed.
Definition arrayMipMapFirst (m : arrayMipMapList) : arrayMipMap.
Proof.
assert ([] <> arrayMipMaps m) as Hneq by (apply (arrayMipMapsNonEmpty)).
destruct (arrayMipMaps m) eqn:Hm.
- contradiction.
- exact a.
Defined.
Lemma lt_neq : forall n, 0 <> n <-> 0 < n.
Proof.
intros n.
constructor.
- intro Hneq.
induction n as [|k].
-- unfold not in Hneq.
assert (0 = 0) as Heq by reflexivity.
contradiction.
-- apply (Nat.lt_0_succ k).
- intro Hneq.
induction n as [|k].
-- inversion Hneq.
-- discriminate.
Qed.
Lemma lt_neq_0 : forall n, 0 <> n -> 0 < n.
Proof.
intros n Hneq.
rewrite <- lt_neq; trivial.
Qed.
Lemma lt_neq_1 : forall n, 0 < n -> 0 <> n.
Proof.
intros n Hneq.
rewrite lt_neq; trivial.
Qed.
Definition arrayMipMapSize
(level : nat)
(imageSize : imageSize3D)
(levelRange : 0 < level)
: option arrayMipMapImageSize :=
let sx := (sizeX imageSize) / 2 ^ level in
let sy := (sizeY imageSize) / 2 ^ level in
match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with
| (ReflectT _ xt, ReflectT _ yt) => Some (ArrayMipMapImageSize sx sy xt yt)
| (_, _) => None
end.
Fixpoint arrayMipMapImageDataSizeTotalAux (m : list arrayMipMap) : nat :=
match m with
| [] => 0
| (x :: []) => (arrayMipMapOffset x) + (arrayMipMapSizeCompressed x)
| (x :: xs) => arrayMipMapImageDataSizeTotalAux xs
end.
Definition arrayMipMapImageDataSizeTotal (m : arrayMipMapList) : nat :=
arrayMipMapImageDataSizeTotalAux (arrayMipMaps m).
Example exampleArrayMipMapsIndices := [
(ArrayMipMapIndex 2 0);
(ArrayMipMapIndex 2 1);
(ArrayMipMapIndex 2 2);
(ArrayMipMapIndex 1 0);
(ArrayMipMapIndex 1 1);
(ArrayMipMapIndex 1 2);
(ArrayMipMapIndex 0 0);
(ArrayMipMapIndex 0 1);
(ArrayMipMapIndex 0 2)
].
Example exampleArrayMipMaps :=
map (fun i => ArrayMipMap i 0 0 0 0) exampleArrayMipMapsIndices.
Example exampleArrayMipMapIndicesSorted : arrayMipMapIndicesSorted exampleArrayMipMapsIndices.
Proof.
apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. }
apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. }
apply AMMICons. { apply AMIIOrdLevelLt. compute; constructor. }
apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. }
apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. }
apply AMMICons. { apply AMIIOrdLevelLt. compute; constructor. }
apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. }
apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. }
apply AMMIOne.
Qed.
Example exampleArrayMipMapsHaveSameLayers0 : arrayMipMapLayerCountForLevel 0 exampleArrayMipMaps = 3.
Proof. reflexivity. Qed.
Example exampleArrayMipMapsHaveSameLayers1 : arrayMipMapLayerCountForLevel 1 exampleArrayMipMaps = 3.
Proof. reflexivity. Qed.
Example exampleArrayMipMapsHaveSameLayers2 : arrayMipMapLayerCountForLevel 2 exampleArrayMipMaps = 3.
Proof. reflexivity. Qed.
Example exampleArrayMipMapsLevel : forall n, In n (arrayMipMapLevels exampleArrayMipMaps) ->
n = 0 \/ n = 1 \/ n = 2.
Proof.
intros n.
simpl.
intros H.
destruct H; auto.
destruct H; auto.
destruct H; auto.
contradiction H.
Qed.
Example exampleArrayMipMapsHaveSameLayers : forall level0 level1, arrayMipMapsHaveSameLayers exampleArrayMipMaps level0 level1.
Proof.
intros level0 level1.
unfold arrayMipMapsHaveSameLayers.
intros H_In0 H_In1.
assert (level0 = 0 \/ level0 = 1 \/ level0 = 2) as Hl0 by (apply (exampleArrayMipMapsLevel level0 H_In0)).
assert (level1 = 0 \/ level1 = 1 \/ level1 = 2) as Hl1 by (apply (exampleArrayMipMapsLevel level1 H_In1)).
destruct Hl0 as [Heq0|Heq0]. {
destruct Hl1 as [Heq1|Heq1]. {
rewrite Heq0.
rewrite Heq1.
reflexivity.
}
destruct Heq1 as [Heq1_0|Heq1_0]. {
rewrite Heq0.
rewrite Heq1_0.
reflexivity.
}
rewrite Heq0.
rewrite Heq1_0.
reflexivity.
}
destruct Heq0 as [Heq0_0|Heq0_0]. {
rewrite Heq0_0.
destruct Hl1 as [Heq1|Heq1]. {
rewrite Heq1.
reflexivity.
}
destruct Heq1 as [Heq1_0|Heq1_0]. {
rewrite Heq1_0.
reflexivity.
}
rewrite Heq1_0.
reflexivity.
}
destruct Hl1 as [Heq1|Heq1]. {
rewrite Heq0_0.
rewrite Heq1.
reflexivity.
}
destruct Heq1 as [Heq1_0|Heq1_0]. {
rewrite Heq0_0.
rewrite Heq1_0.
reflexivity.
}
rewrite Heq0_0.
rewrite Heq1_0.
reflexivity.
Qed.
```
#### 8.4. Calino/Binary.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.Metadata.
Require Import com.io7m.calino.ArrayMipMap.
Require Import com.io7m.calino.CubeMipMap.
Require Import com.io7m.calino.MipMap.
Require Import com.io7m.calino.ImageInfo.
Require Import com.io7m.calino.StringUtility.
Require Import com.io7m.calino.Descriptor.
Require Import com.io7m.calino.ChannelDescription.
Require Import com.io7m.calino.ChannelSemantic.
Require Import com.io7m.calino.ChannelType.
Require Import com.io7m.calino.Compression.
Require Import com.io7m.calino.SuperCompression.
Require Import com.io7m.calino.ColorSpace.
Require Import com.io7m.calino.Flag.
Require Import com.io7m.calino.CoordinateSystem.
Require Import com.io7m.calino.ImageSize.
Require Import com.io7m.octetorder.OctetOrder.
Require Import com.io7m.entomos.Alignment.
Require Import com.io7m.entomos.Binary.
Import ListNotations.
Open Scope program_scope.
Open Scope string_scope.
Set Mangle Names.
Definition byteOrderDescribe (b : octetOrder) : descriptor :=
match b with
| OctetOrderBig => "BIG_ENDIAN"
| OctetOrderLittle => "LITTLE_ENDIAN"
end.
#[export]
Instance byteOrderDescribable : describable octetOrder := {
descriptorOf f := byteOrderDescribe f
}.
Definition binaryExpMipMap (m : mipMap) : binaryExp := BiRecord [
("mipMapLevel", u32 (mipMapLevel m));
("mipMapDataOffset", u64 (mipMapOffset m));
("mipMapSizeUncompressed", u64 (mipMapSizeUncompressed m));
("mipMapSizeCompressed", u64 (mipMapSizeCompressed m));
("mipMapCRC32", u32 (mipMapCRC32 m))
].
Remark binaryExpMipMapSize : forall m, binarySize (binaryExpMipMap m) = 32.
Proof. reflexivity. Qed.
Definition binaryExpMipMaps (m : mipMapList) : binaryExp :=
BiArray (map binaryExpMipMap (mipMaps m)).
Definition binaryExpImage2D
(i : imageInfo)
(m : mipMapList)
: binaryExp :=
let imageDataStart := mipMapOffset (mipMapFirst m) in
let encMips := binaryExpMipMaps m in
let encMipsSize := binarySize encMips in
let encMipsPad := imageDataStart - encMipsSize in
let imageSize := mipMapImageDataSizeTotal m in
let imageSize16 := asMultipleOf16 imageSize in
BiRecord [
("mipMaps", encMips);
("mipPad", BiReserve encMipsPad);
("mipData", BiReserve imageSize16)
].
Definition binaryExpImage2DSection
(i : imageInfo)
(m : mipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F49324421);
("size", u64 (binarySize (binaryExpImage2D i m)));
("data", binaryExpImage2D i m)
].
Definition binaryExpArrayMipMap (m : arrayMipMap) : binaryExp := BiRecord [
("arrayMipMapLevel", u32 (arrayMipMapLevel (arrayMipMapIndex m)));
("arrayMipMapLayer", u32 (arrayMipMapLayer (arrayMipMapIndex m)));
("arrayMipMapDataOffset", u64 (arrayMipMapOffset m));
("arrayMipMapSizeUncompressed", u64 (arrayMipMapSizeUncompressed m));
("arrayMipMapSizeCompressed", u64 (arrayMipMapSizeCompressed m));
("arrayMipMapCRC32", u32 (arrayMipMapCRC32 m))
].
Remark binaryExpArrayMipMapSize : forall m, binarySize (binaryExpArrayMipMap m) = 36.
Proof. reflexivity. Qed.
Definition binaryExpArrayMipMaps (m : arrayMipMapList) : binaryExp :=
BiArray (map binaryExpArrayMipMap (arrayMipMaps m)).
Definition binaryExpImageArray
(i : imageInfo)
(m : arrayMipMapList)
: binaryExp :=
let imageDataStart := arrayMipMapOffset (arrayMipMapFirst m) in
let encMips := binaryExpArrayMipMaps m in
let encMipsSize := binarySize encMips in
let encMipsPad := imageDataStart - encMipsSize in
let imageSize := arrayMipMapImageDataSizeTotal m in
let imageSize16 := asMultipleOf16 imageSize in
BiRecord [
("arrayMipMaps", encMips);
("arrayMipPad", BiReserve encMipsPad);
("arrayMipData", BiReserve imageSize16)
].
Definition binaryExpImageArraySection
(i : imageInfo)
(m : arrayMipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F41525221);
("size", u64 (binarySize (binaryExpImageArray i m)));
("data", binaryExpImageArray i m)
].
Definition binaryExpCubeMipMapFace (m : cubeMapFace) : binaryExp := BiRecord [
("cubeFaceDataOffset", u64 (cubeFaceOffset m));
("cubeFaceSizeUncompressed", u64 (cubeFaceSizeUncompressed m));
("cubeFaceSizeCompressed", u64 (cubeFaceSizeCompressed m));
("cubeFaceCRC32", u32 (cubeFaceCRC32 m))
].
Remark binaryExpCubeMipMapFaceSize : forall m, binarySize (binaryExpCubeMipMapFace m) = 28.
Proof. reflexivity. Qed.
Definition binaryExpCubeMipMap (m : cubeMipMap) : binaryExp := BiRecord [
("cubeMipMapLevel", u32 (cubeMapLevel m));
("cubeMipMapFacePosX", binaryExpCubeMipMapFace (cubeMapFaceXPos m));
("cubeMipMapFaceNegX", binaryExpCubeMipMapFace (cubeMapFaceXNeg m));
("cubeMipMapFacePosY", binaryExpCubeMipMapFace (cubeMapFaceYPos m));
("cubeMipMapFaceNegY", binaryExpCubeMipMapFace (cubeMapFaceYNeg m));
("cubeMipMapFacePosZ", binaryExpCubeMipMapFace (cubeMapFaceZPos m));
("cubeMipMapFaceNegZ", binaryExpCubeMipMapFace (cubeMapFaceZNeg m))
].
Remark binaryExpCubeMipMapSize : forall m, binarySize (binaryExpCubeMipMap m) = 172.
Proof. reflexivity. Qed.
Definition binaryExpCubeMipMaps (m : cubeMipMapList) : binaryExp :=
BiArray (map binaryExpCubeMipMap (cubeMipMaps m)).
Definition binaryExpImageCubeMap
(i : imageInfo)
(m : cubeMipMapList)
: binaryExp :=
let imageDataStart := cubeFaceOffset (cubeMapFaceXPos (cubeMipMapsFirst m)) in
let encMips := binaryExpCubeMipMaps m in
let encMipsSize := binarySize encMips in
let encMipsPad := imageDataStart - encMipsSize in
let imageSize := cubeMipMapImageDataSizeTotal m in
let imageSize16 := asMultipleOf16 imageSize in
BiRecord [
("cubeMipMaps", encMips);
("cubeMipPad", BiReserve encMipsPad);
("cubeMipData", BiReserve imageSize16)
].
Definition binaryExpImageCubeSection
(i : imageInfo)
(m : cubeMipMapList)
: binaryExp := BiRecord [
("id", u64 0x434C4E5F43554245);
("size", u64 (binarySize (binaryExpImageCubeMap i m)));
("data", binaryExpImageCubeMap i m)
].
Definition binaryExpCompression (c : compressionMethod) : binaryExp := BiRecord [
("descriptor", utf8 (descriptorOf c));
("sectionIdentifier", u64 (compressionSectionIdentifier c));
("blockSizeX", u32 (compressionBlockSizeX c));
("blockSizeY", u32 (compressionBlockSizeY c));
("blockAlignment", u32 (compressionBlockAlignment c))
].
Definition binaryExpSuperCompression (c : superCompressionMethod) : binaryExp := BiRecord [
("descriptor", utf8 (descriptorOf c));
("sectionIdentifier", u64 (superCompressionSectionIdentifier c))
].
Definition binaryExpImageInfo (i : imageInfo) : binaryExp := BiRecord [
("sizeX", u32 (imageSizeX i));
("sizeY", u32 (imageSizeY i));
("sizeZ", u32 (imageSizeZ i));
("channelsLayout", utf8 (descriptorOf (imageChannelsLayout i)));
("channelsType", utf8 (descriptorOf (imageChannelsType i)));
("compression", binaryExpCompression (imageCompressionMethod i));
("superCompression", binaryExpSuperCompression (imageSuperCompressionMethod i));
("coordinateSystem", utf8 (descriptorOf (imageCoordinateSystem i)));
("colorSpace", utf8 (descriptorOf (imageColorSpace i)));
("flags", BiArray (map (utf8 ∘ descriptorOf) (imageFlagSet i)));
("byteOrder", utf8 (descriptorOf (imageByteOrder i)))
].
Definition binaryExpFileHeader : binaryExp := BiRecord [
("id", u64 0x89434C4E0D0A1A0A);
("versionMajor", u32 2);
("versionMinor", u32 0)
].
Definition binaryExpImageInfoSection (i : imageInfo) : binaryExp := BiRecord [
("id", u64 0x434C4E49494E464F);
("size", u64 (binarySize (binaryExpImageInfo i)));
("data", binaryExpImageInfo i)
].
Definition binaryExpMetadataValue (m : metadataValue) : binaryExp := BiRecord [
("key", utf8 (mKey m));
("value", utf8 (mValue m))
].
Definition binaryExpMetadata (m : metadata) : binaryExp :=
BiArray (map binaryExpMetadataValue (mValues m)).
Definition binaryExpMetadataSection (m : metadata) : binaryExp := BiRecord [
("id", u64 0x434C4E5F4D455441);
("size", u64 (binarySize (binaryExpMetadata m)));
("data", binaryExpMetadata m)
].
Definition binaryEndSection : binaryExp := BiRecord [
("id", u64 0x434c4e5f454e4421);
("size", u64 0)
].
```
#### 8.5. Calino/ChannelDescription.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.ChannelSemantic.
Require Import com.io7m.calino.Descriptor.
Require Import com.io7m.calino.StringUtility.
Require Import com.io7m.entomos.Divisible.
Import ListNotations.
Set Mangle Names.
Definition divisible8 (x : nat) : Prop :=
modulo x 8 = 0.
Inductive channelDescription : Set := channelDescriptionMake {
cdSemantic : channelSemantic;
cdBits : nat;
cdBitsNonzero : 0 <> cdBits
}.
Definition channelDescriptionDescribe (c : channelDescription) : descriptor :=
descriptorOf (cdSemantic c) ++ stringOfNat (cdBits c).
#[export]
Instance channelDescriptionDescribable : describable channelDescription := {
descriptorOf c := channelDescriptionDescribe c
}.
Fixpoint channelDescriptionsDescribe (c : list channelDescription) : descriptor :=
match c with
| nil => ""
| cons d nil => channelDescriptionDescribe d
| cons d e => (channelDescriptionDescribe d) ++ ":" ++ (channelDescriptionsDescribe e)
end.
(** @annospec 87af76a2-deb2-493b-a98c-762c2b86173d *)
Inductive channelLayoutPacking : Set :=
| CLPack8
| CLPack16
| CLPack32
| CLPack64.
Definition channelLayoutPackingBits (c : channelLayoutPacking) : nat :=
match c with
| CLPack8 => 8
| CLPack16 => 16
| CLPack32 => 32
| CLPack64 => 64
end.
Theorem channelLayoutPackingBitsDiv8 : forall c, divisible8 (channelLayoutPackingBits (c)).
Proof.
intros c.
destruct c; reflexivity.
Qed.
Definition channelLayoutPackingDescribe (c : channelLayoutPacking) : descriptor :=
match c with
| CLPack8 => "p8"
| CLPack16 => "p16"
| CLPack32 => "p32"
| CLPack64 => "p64"
end.
#[export]
Instance channelLayoutPackingDescribable : describable channelLayoutPacking := {
descriptorOf c := channelLayoutPackingDescribe c
}.
Definition channelDescriptionBitsDivisible8 (c : channelDescription) : Prop :=
divisible8 (cdBits c).
Fixpoint channelDescriptionsBitsTotal (c : list channelDescription) : nat :=
match c with
| nil => 0
| (x :: rest) => (cdBits x) + (channelDescriptionsBitsTotal rest)
end.
Lemma natAddNonzero : forall (n m : nat), 0 <> n -> 0 <> m + n.
Proof.
intros n m HnZ.
destruct m; simpl; auto.
Qed.
Lemma channelDescriptionsBitsNonEmptyNonZero : forall (c : list channelDescription),
nil <> c -> 0 <> channelDescriptionsBitsTotal c.
Proof.
intros c HnotNil.
induction c as [|a b]. {
contradiction.
} {
simpl.
assert (0 <> cdBits a) as HbitsNZ
by apply (cdBitsNonzero a).
assert (0 <> channelDescriptionsBitsTotal b + cdBits a) as Hnz2. {
apply natAddNonzero.
exact HbitsNZ.
}
rewrite (Nat.add_comm) in Hnz2.
exact Hnz2.
}
Qed.
Inductive channelLayoutDescriptionUnpacked : Set := CLDUMake {
uChannels : list channelDescription;
uChannelsNonEmpty : [] <> uChannels;
uInvariants : Forall channelDescriptionBitsDivisible8 uChannels;
}.
Definition channelLayoutDescriptionUnpackedDescribe (c : channelLayoutDescriptionUnpacked) : descriptor :=
channelDescriptionsDescribe (uChannels c).
#[export]
Instance channelLayoutDescriptionUnpackedDescribable : describable channelLayoutDescriptionUnpacked := {
descriptorOf c := channelLayoutDescriptionUnpackedDescribe c
}.
Inductive channelLayoutDescriptionPacked : Set := CLDPMake {
pChannels : list channelDescription;
pChannelsNonEmpty : [] <> pChannels;
pPacking : channelLayoutPacking;
pInvariants : channelDescriptionsBitsTotal pChannels = channelLayoutPackingBits pPacking
}.
Definition channelLayoutDescriptionPackedDescribe (c : channelLayoutDescriptionPacked) : descriptor :=
let packing := descriptorOf (pPacking c) in
let channels := channelDescriptionsDescribe (pChannels c) in
packing ++ "|" ++ channels.
#[export]
Instance channelLayoutDescriptionPackedDescribable : describable channelLayoutDescriptionPacked := {
descriptorOf c := channelLayoutDescriptionPackedDescribe c
}.
(** @annospec dbb9f758-635b-4ad5-8b50-10a04bc68d79 *)
Inductive channelLayoutDescription : Set :=
| ChannelLayoutDescriptionUnpacked : channelLayoutDescriptionUnpacked -> channelLayoutDescription
| ChannelLayoutDescriptionPacked : channelLayoutDescriptionPacked -> channelLayoutDescription.
Definition channelLayoutDescriptionDescribe (c : channelLayoutDescription) : descriptor :=
match c with
| ChannelLayoutDescriptionPacked p => descriptorOf p
| ChannelLayoutDescriptionUnpacked u => descriptorOf u
end.
#[export]
Instance channelLayoutDescriptionDescribable : describable channelLayoutDescription := {
descriptorOf c := channelLayoutDescriptionDescribe c
}.
Definition channelLayoutDescriptionBits (c : channelLayoutDescription) : nat :=
match c with
| ChannelLayoutDescriptionUnpacked u =>
channelDescriptionsBitsTotal (uChannels u)
| ChannelLayoutDescriptionPacked p =>
channelDescriptionsBitsTotal (pChannels p)
end.
Lemma channelLayoutDescriptionBitsAdd : forall d ds,
channelDescriptionsBitsTotal (d :: ds) =
(cdBits d) + (channelDescriptionsBitsTotal ds).
Proof. intros d ds. reflexivity. Qed.
Lemma 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.
Theorem channelLayoutDescriptionBitsDivisible8 : forall (c : channelLayoutDescription),
divisible8 (channelLayoutDescriptionBits c).
Proof.
intros c.
destruct c as [u|p]. {
assert (Forall channelDescriptionBitsDivisible8 (uChannels u)) as Hf8
by (apply uInvariants).
unfold channelLayoutDescriptionBits.
induction (uChannels u) as [|d ds IHu]. {
reflexivity.
} {
rewrite channelLayoutDescriptionBitsAdd.
assert (divisible8 (channelDescriptionsBitsTotal ds)) as Hdsdiv8. {
assert (Forall channelDescriptionBitsDivisible8 ds) as Hfac
by (apply (Forall_inv_tail (a := d) (l := ds) Hf8)).
apply (IHu Hfac).
}
assert (divisible8 (cdBits d)) as Hdivbits
by (apply (Forall_inv (a := d) (l := ds) Hf8)).
apply (divisiblity8Add (cdBits d) (channelDescriptionsBitsTotal ds) Hdivbits Hdsdiv8).
}
} {
simpl.
assert (channelDescriptionsBitsTotal (pChannels p) = channelLayoutPackingBits (pPacking p))
as Hbeq by (apply pInvariants).
rewrite Hbeq.
apply channelLayoutPackingBitsDiv8.
}
Qed.
Theorem channelLayoutDescriptionBitsLe8 : forall (c : channelLayoutDescription),
8 <= channelLayoutDescriptionBits c.
Proof.
intros c.
assert (divisible8 (channelLayoutDescriptionBits c)) as Hdiv8
by (apply (channelLayoutDescriptionBitsDivisible8 c)).
unfold divisible8 in Hdiv8.
destruct c as [u|p].
- simpl.
destruct (uChannels u) as [|ch0 chs] eqn:Hcheq.
-- symmetry in Hcheq.
assert ([] <> uChannels u) as Hne by (apply (uChannelsNonEmpty u)).
contradiction.
-- unfold channelLayoutDescriptionBits in Hdiv8.
rewrite Nat.Lcm0.mod_divide in Hdiv8.
rewrite <- Hcheq.
apply (Nat.divide_pos_le 8 (channelDescriptionsBitsTotal (uChannels u))).
rewrite Hcheq.
simpl.
assert (0 < cdBits ch0) as HbitnZ. {
apply Nat.neq_0_lt_0.
symmetry.
apply (cdBitsNonzero ch0).
}
apply Nat.add_pos_l.
exact HbitnZ.
exact Hdiv8.
- simpl.
rewrite (pInvariants p).
destruct (pPacking p) eqn:Hpack.
-- constructor.
-- repeat (constructor).
-- repeat (constructor).
-- repeat (constructor).
Qed.
```
#### 8.6. Calino/ChannelSemantic.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.Descriptor.
(** @annospec 0c1471cb-6336-4c1c-b924-952f2ae87d6b *)
Inductive channelSemantic : Set :=
| CSRed
| CSGreen
| CSBlue
| CSAlpha
| CSDepth
| CSStencil
| CSExponent
| CSUnused.
Definition channelSemanticDescribe (c : channelSemantic) : descriptor :=
match c with
| CSRed => "R"
| CSGreen => "G"
| CSBlue => "B"
| CSAlpha => "A"
| CSDepth => "D"
| CSStencil => "S"
| CSExponent => "E"
| CSUnused => "X"
end.
#[export]
Instance channelSemanticDescribable : describable channelSemantic := {
descriptorOf c := channelSemanticDescribe c
}.
```
#### 8.7. Calino/ChannelType.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.Descriptor.
(** @annospec 5740b7f3-5547-4d27-abcb-8187151b7e3c *)
Inductive channelType : Set :=
| CTFixedPointNormalizedUnsigned
| CTFixedPointNormalizedSigned
| CTScaledUnsigned
| CTScaledSigned
| CTIntegerUnsigned
| CTIntegerSigned
| CTFloatIEEE754
| CTCustom : descriptor -> channelType.
Definition channelTypeDescribe (c : channelType) : descriptor :=
match c with
| CTFixedPointNormalizedUnsigned => "FIXED_POINT_NORMALIZED_UNSIGNED"
| CTFixedPointNormalizedSigned => "FIXED_POINT_NORMALIZED_SIGNED"
| CTScaledUnsigned => "SCALED_UNSIGNED"
| CTScaledSigned => "SCALED_SIGNED"
| CTIntegerUnsigned => "INTEGER_UNSIGNED"
| CTIntegerSigned => "INTEGER_SIGNED"
| CTFloatIEEE754 => "FLOATING_POINT_IEEE754"
| CTCustom d => d
end.
#[export]
Instance channelTypeDescribable : describable channelType := {
descriptorOf c := channelTypeDescribe c
}.
```
#### 8.8. Calino/ColorSpace.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.Descriptor.
(** @annospec 9e5bcc04-24c8-49ec-ba80-1593f20506cd *)
Inductive colorSpace : Set :=
| CSLinear
| CSsRGB
| CSCustom : descriptor -> colorSpace.
Definition colorSpaceDescribe (c : colorSpace) : descriptor :=
match c with
| CSLinear => "LINEAR"
| CSsRGB => "SRGB"
| CSCustom d => d
end.
#[export]
Instance colorSpaceDescribable : describable colorSpace := {
descriptorOf c := colorSpaceDescribe c
}.
```
#### 8.9. Calino/Compression.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.Descriptor.
(** @annospec ce94241f-f6e7-431f-aabc-fd534b5ce004 *)
Inductive compressionMethod : Set :=
| CompressionUncompressed
| CompressionBC1
| CompressionBC2
| CompressionBC3
| CompressionBC4
| CompressionBC5
| CompressionBC6
| CompressionBC7
| CompressionETC1
| CompressionETC2
| CompressionEAC
| CompressionASTC : nat -> nat -> compressionMethod
| CompressionCustom :
forall (d : descriptor)
(blockSizeX : nat)
(blockSizeY : nat)
(identifier : nat)
(align : nat), 0 < align -> compressionMethod.
Definition compressionMethodDescriptor (c : compressionMethod) :=
match c with
| CompressionUncompressed => "UNCOMPRESSED"
| CompressionBC1 => "BC1"
| CompressionBC2 => "BC2"
| CompressionBC3 => "BC3"
| CompressionBC4 => "BC4"
| CompressionBC5 => "BC5"
| CompressionBC6 => "BC6"
| CompressionBC7 => "BC7"
| CompressionETC1 => "ETC1"
| CompressionETC2 => "ETC2"
| CompressionEAC => "EAC"
| CompressionASTC _ _ => "ASTC"
| CompressionCustom c _ _ _ _ _ => c
end.
Definition compressionBlockSizeX (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 4
| CompressionBC2 => 4
| CompressionBC3 => 4
| CompressionBC4 => 4
| CompressionBC5 => 4
| CompressionBC6 => 4
| CompressionBC7 => 4
| CompressionETC1 => 4
| CompressionETC2 => 4
| CompressionEAC => 4
| CompressionASTC x _ => x
| CompressionCustom _ x _ _ _ _ => x
end.
Definition compressionBlockSizeY (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 4
| CompressionBC2 => 4
| CompressionBC3 => 4
| CompressionBC4 => 4
| CompressionBC5 => 4
| CompressionBC6 => 4
| CompressionBC7 => 4
| CompressionETC1 => 4
| CompressionETC2 => 4
| CompressionEAC => 4
| CompressionASTC _ y => y
| CompressionCustom _ _ y _ _ _ => y
end.
Definition compressionSectionIdentifier (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 0
| CompressionBC2 => 0
| CompressionBC3 => 0
| CompressionBC4 => 0
| CompressionBC5 => 0
| CompressionBC6 => 0
| CompressionBC7 => 0
| CompressionETC1 => 0
| CompressionETC2 => 0
| CompressionEAC => 0
| CompressionASTC _ _ => 0
| CompressionCustom _ _ _ i _ _ => i
end.
Definition compressionBlockAlignment (c : compressionMethod) : nat :=
match c with
| CompressionUncompressed => 0
| CompressionBC1 => 8
| CompressionBC2 => 16
| CompressionBC3 => 16
| CompressionBC4 => 8
| CompressionBC5 => 16
| CompressionBC6 => 16
| CompressionBC7 => 16
| CompressionETC1 => 16
| CompressionETC2 => 16
| CompressionEAC => 16
| CompressionASTC _ _ => 16
| CompressionCustom _ _ _ _ a _ => a
end.
Definition compressionIsNotCompressed (c : compressionMethod) : Prop :=
match c with
| CompressionUncompressed => True
| _ => False
end.
#[export]
Instance compressionMethodDescribable : describable compressionMethod := {
descriptorOf c := compressionMethodDescriptor c
}.
```
#### 8.10. Calino/CoordinateSystem.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.Descriptor.
(** @annospec 3f35940c-0e92-4193-9838-fb14e8324f55 *)
Inductive coordinateAxisR : Set :=
| AxisRIncreasingToward
| AxisRIncreasingAway.
(** @annospec 4fc27183-e498-4fd1-a58a-029040e8384a *)
Inductive coordinateAxisS : Set :=
| AxisSIncreasingRight
| AxisSIncreasingLeft.
(** @annospec fe811351-5c2e-4a0c-9044-f1fcc42fbce6 *)
Inductive coordinateAxisT : Set :=
| AxisTIncreasingDown
| AxisTIncreasingUp.
Definition coordinateAxisRDescribe (c : coordinateAxisR) : descriptor :=
match c with
| AxisRIncreasingToward => "RT"
| AxisRIncreasingAway => "RA"
end.
Definition coordinateAxisSDescribe (c : coordinateAxisS) : descriptor :=
match c with
| AxisSIncreasingRight => "SR"
| AxisSIncreasingLeft => "SL"
end.
Definition coordinateAxisTDescribe (c : coordinateAxisT) : descriptor :=
match c with
| AxisTIncreasingDown => "TD"
| AxisTIncreasingUp => "TU"
end.
#[export]
Instance coordinateAxisRDescribable : describable coordinateAxisR := {
descriptorOf c := coordinateAxisRDescribe c
}.
#[export]
Instance coordinateAxisSDescribable : describable coordinateAxisS := {
descriptorOf c := coordinateAxisSDescribe c
}.
#[export]
Instance coordinateAxisTDescribable : describable coordinateAxisT := {
descriptorOf c := coordinateAxisTDescribe c
}.
Inductive coordinateSystem : Set :=
CoordinateSystem : coordinateAxisR -> coordinateAxisS -> coordinateAxisT -> coordinateSystem.
Definition coordinateSystemDescribe (c : coordinateSystem) : descriptor :=
match c with
| CoordinateSystem r s t =>
descriptorOf r ++ ":" ++ descriptorOf s ++ ":" ++ descriptorOf t
end.
#[export]
Instance coordinateSystemDescribable : describable coordinateSystem := {
descriptorOf c := coordinateSystemDescribe c
}.
```
#### 8.11. Calino/CubeMipMap.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Bool.Bool.
Require Import com.io7m.calino.ImageSize.
Import ListNotations.
(** @annospec cf648138-c02a-4b55-b5a7-78ce8e6fee9e *)
Inductive cubeMapFace : Set := CubeMapFace {
cubeFaceOffset : nat;
cubeFaceSizeCompressed : nat;
cubeFaceSizeUncompressed : nat;
cubeFaceCRC32 : nat
}.
Inductive cubeMipMap : Set := CubeMipMap {
cubeMapLevel : nat;
cubeMapFaceXPos : cubeMapFace;
cubeMapFaceXNeg : cubeMapFace;
cubeMapFaceYPos : cubeMapFace;
cubeMapFaceYNeg : cubeMapFace;
cubeMapFaceZPos : cubeMapFace;
cubeMapFaceZNeg : cubeMapFace
}.
Definition cubeFaceExtent (f : cubeMapFace) : nat :=
cubeFaceOffset f + cubeFaceSizeCompressed f.
Inductive cubeOffsetsSorted : list cubeMipMap -> Prop :=
| CMMSizeOne : forall m,
cubeFaceExtent (cubeMapFaceXPos m) < cubeFaceOffset (cubeMapFaceXNeg m) ->
cubeFaceExtent (cubeMapFaceXNeg m) < cubeFaceOffset (cubeMapFaceYPos m) ->
cubeFaceExtent (cubeMapFaceYPos m) < cubeFaceOffset (cubeMapFaceYNeg m) ->
cubeFaceExtent (cubeMapFaceYNeg m) < cubeFaceOffset (cubeMapFaceZPos m) ->
cubeFaceExtent (cubeMapFaceZPos m) < cubeFaceOffset (cubeMapFaceZNeg m) ->
cubeOffsetsSorted [m]
| CMMSizeCons : forall mm0 mm1 mxs,
cubeFaceExtent (cubeMapFaceZNeg mm1) < cubeFaceOffset (cubeMapFaceXPos mm0) ->
cubeOffsetsSorted (mm0 :: mxs) ->
cubeOffsetsSorted (mm1 :: mm0 :: mxs).
Inductive cubeMipMapListIsSorted : list cubeMipMap -> Prop :=
| CubeOne : forall m, cubeMipMapListIsSorted [m]
| CubeCons : forall mm0 mm1 mxs,
cubeMapLevel mm1 = S (cubeMapLevel mm0) ->
cubeMipMapListIsSorted (mm0 :: mxs) ->
cubeMipMapListIsSorted (mm1 :: mm0 :: mxs).
Inductive cubeMipMapList : Set := CubeList {
cubeMipMaps : list cubeMipMap;
cubeMipMapsListSorted : cubeMipMapListIsSorted cubeMipMaps;
cubeMipMapsOffsetsSorted : cubeOffsetsSorted cubeMipMaps;
}.
Lemma cubeMipMapsNonEmpty : forall (m : cubeMipMapList),
[] <> cubeMipMaps m.
Proof.
intros m.
destruct (cubeMipMapsOffsetsSorted m).
- discriminate.
- discriminate.
Qed.
Definition cubeMipMapsFirst (m : cubeMipMapList) : cubeMipMap.
Proof.
assert ([] <> cubeMipMaps m) as Hneq by (apply (cubeMipMapsNonEmpty)).
destruct (cubeMipMaps m) eqn:Hm.
- contradiction.
- exact c.
Defined.
Fixpoint cubeMipMapImageDataSizeTotalAux (m : list cubeMipMap) : nat :=
match m with
| [] => 0
| (x :: []) => cubeFaceExtent (cubeMapFaceZNeg x)
| (x :: xs) => cubeMipMapImageDataSizeTotalAux xs
end.
Definition cubeMipMapImageDataSizeTotal (m : cubeMipMapList) : nat :=
cubeMipMapImageDataSizeTotalAux (cubeMipMaps m).
Example cubeFaceXP0 := CubeMapFace 0 8 8 0.
Example cubeFaceXN0 := CubeMapFace 16 8 8 0.
Example cubeFaceYP0 := CubeMapFace 32 8 8 0.
Example cubeFaceYN0 := CubeMapFace 48 8 8 0.
Example cubeFaceZP0 := CubeMapFace 64 8 8 0.
Example cubeFaceZN0 := CubeMapFace 80 8 8 0.
Example cubeMipMap0 := CubeMipMap 1 cubeFaceXP0 cubeFaceXN0 cubeFaceYP0 cubeFaceYN0 cubeFaceZP0 cubeFaceZN0.
Example cubeFaceXP1 := CubeMapFace 96 8 8 0.
Example cubeFaceXN1 := CubeMapFace 112 8 8 0.
Example cubeFaceYP1 := CubeMapFace 128 8 8 0.
Example cubeFaceYN1 := CubeMapFace 144 8 8 0.
Example cubeFaceZP1 := CubeMapFace 160 8 8 0.
Example cubeFaceZN1 := CubeMapFace 176 8 8 0.
Example cubeMipMap1 := CubeMipMap 0 cubeFaceXP1 cubeFaceXN1 cubeFaceYP1 cubeFaceYN1 cubeFaceZP1 cubeFaceZN1.
Example cubeOffsetsSortedExample0 : cubeOffsetsSorted [cubeMipMap0].
Proof.
apply CMMSizeOne.
compute; repeat constructor.
compute; repeat constructor.
compute; repeat constructor.
compute; repeat constructor.
compute; repeat constructor.
Qed.
Example cubeOffsetsSortedExample1 : cubeOffsetsSorted [cubeMipMap1].
Proof.
apply CMMSizeOne.
compute; repeat constructor.
compute; repeat constructor.
compute; repeat constructor.
compute; repeat constructor.
compute; repeat constructor.
Qed.
Example cubeOffsetsSortedExample2 : cubeOffsetsSorted [cubeMipMap0; cubeMipMap1].
Proof.
apply CMMSizeCons.
compute; repeat constructor.
exact cubeOffsetsSortedExample1.
Qed.
Example cubeLevelSortedExample0 : cubeMipMapListIsSorted [cubeMipMap0].
Proof.
apply CubeOne.
Qed.
Example cubeLevelSortedExample1 : cubeMipMapListIsSorted [cubeMipMap1].
Proof.
apply CubeOne.
Qed.
Example cubeLevelSortedExample2 : cubeMipMapListIsSorted [cubeMipMap0; cubeMipMap1].
Proof.
apply CubeCons.
reflexivity.
apply CubeOne.
Qed.
```
#### 8.12. Calino/Descriptor.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Open Scope string_scope.
Open Scope char_scope.
Definition descriptor := string.
Class describable (A : Set) := {
descriptorOf : A -> descriptor
}.
```
#### 8.13. Calino/Flag.v
```
(*
* Copyright © 2026 Mark Raynsford 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 Lists.List.
Require Import com.io7m.calino.Descriptor.
Import ListNotations.
(** @annospec 1980a36b-8366-440b-b1a0-121be7af7f6a *)
Inductive flag : Set :=
| FlagAlphaPremultiplied
| FlagCustom : descriptor -> flag.
Definition flagDescribe (f : flag) : descriptor :=
match f with
| FlagAlphaPremultiplied => "ALPHA_PREMULTIPLIED"
| FlagCustom d => d
end.
#[export]
Instance flagDescribable : describable flag := {
descriptorOf f := flagDescribe f
}.
Inductive flagSet : Set := {
flags : list flag;
flagsNoDup : NoDup flags;
}.
```
#### 8.14. Calino/ImageInfo.v
```
(*
* Copyright © 2026 Mark Raynsford 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 Program.Basics.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Ascii.
From Stdlib Require Import Lists.List.
From Stdlib Require Import Init.Nat.
Require Import com.io7m.calino.StringUtility.
Require Import com.io7m.calino.Descriptor.
Require Import com.io7m.calino.ChannelDescription.
Require Import com.io7m.calino.ChannelSemantic.
Require Import com.io7m.calino.ChannelType.
Require Import com.io7m.calino.Compression.
Require Import com.io7m.calino.SuperCompression.
Require Import com.io7m.calino.ColorSpace.
Require Import com.io7m.calino.Flag.
Require Import com.io7m.calino.CoordinateSystem.
Require Import com.io7m.calino.ImageSize.
Require Import com.io7m.octetorder.OctetOrder.
Open Scope program_scope.
Record imageInfo : Set := ImageInfo {
imageSize : imageSize3D;
imageChannelsLayout : channelLayoutDescription;
imageChannelsType : channelType;
imageCompressionMethod : compressionMethod;
imageSuperCompressionMethod : superCompressionMethod;
imageCoordinateSystem : coordinateSystem;
imageColorSpace : colorSpace;
imageFlags : flagSet;
imageByteOrder : octetOrder
}.
Definition imageSizeX :=
sizeX ∘ imageSize.
Definition imageSizeY :=
sizeY ∘ imageSize.
Definition imageSizeZ :=
sizeZ ∘ imageSize.
Definition imageFlagSet :=
flags ∘ imageFlags.
Definition imageInfoTexelBlockAlignment (i : imageInfo) :=
let c := imageCompressionMethod i in
match c with
| CompressionUncompressed => channelLayoutDescriptionBits (imageChannelsLayout i) / 8
| _ => compressionBlockAlignment c
end.
Theorem imageInfoTexelBlockAlignmentPositive : forall i,
0 < imageInfoTexelBlockAlignment i.
Proof.
intros i.
unfold imageInfoTexelBlockAlignment.
destruct (imageCompressionMethod i) eqn:Hm.
- assert (8 <= channelLayoutDescriptionBits (imageChannelsLayout i)) as Hle8
by (apply (channelLayoutDescriptionBitsLe8)).
apply (Nat.div_le_lower_bound (channelLayoutDescriptionBits (imageChannelsLayout i)) 8 1).
discriminate.
rewrite Nat.mul_1_r.
exact Hle8.
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- repeat (constructor).
- auto.
Qed.
Theorem imageInfoTexelBlockAlignmentNonZero : forall i,
0 <> imageInfoTexelBlockAlignment i.
Proof.
intros i.
symmetry.
rewrite Nat.neq_0_lt_0.
apply imageInfoTexelBlockAlignmentPositive.
Qed.
```
#### 8.15. Calino/ImageSize.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
*)
Record imageSize3D : Set := ImageSize3D {
sizeX : nat;
sizeY : nat;
sizeZ : nat;
sizeXnot0 : 0 <> sizeX;
sizeYnot0 : 0 <> sizeY;
sizeZnot0 : 0 <> sizeZ;
}.
```
#### 8.16. Calino/Metadata.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Open Scope string_scope.
Import ListNotations.
Inductive metadataValue : Set := MetadataValue {
mKey : string;
mValue : string
}.
Inductive metadata : Set := Metadata {
mValues : list metadataValue
}.
```
#### 8.17. Calino/MipMap.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Bool.Bool.
Require Import com.io7m.calino.ImageSize.
Import ListNotations.
Inductive mipMap : Set := MipMap {
mipMapLevel : nat;
mipMapOffset : nat;
mipMapSizeCompressed : nat;
mipMapSizeUncompressed : nat;
mipMapCRC32 : nat
}.
Inductive mipMapListIsSorted : list mipMap -> Prop :=
| MipsOne : forall m, mipMapListIsSorted [m]
| MipsCons : forall mm0 mm1 mxs,
mipMapLevel mm1 = S (mipMapLevel mm0) ->
mipMapListIsSorted (mm0 :: mxs) ->
mipMapListIsSorted (mm1 :: mm0 :: mxs).
Inductive mipMapOffsetsSorted : list mipMap -> Prop :=
| MMSizeOne : forall m, mipMapOffsetsSorted [m]
| MMSizeCons : forall mm0 mm1 mxs,
((mipMapOffset mm1) + (mipMapSizeCompressed mm1)) < (mipMapOffset mm0) ->
mipMapOffsetsSorted (mm0 :: mxs) ->
mipMapOffsetsSorted (mm1 :: mm0 :: mxs).
Inductive mipMapList : Set := MipMapList {
mipMaps : list mipMap;
mipMapListSorted : mipMapListIsSorted mipMaps;
mipMapOffsetSorted : mipMapOffsetsSorted mipMaps;
}.
Inductive mipMapImageSize : Set := MipMapImageSize {
mmSizeX : nat;
mmSizeY : nat;
mmSizeXRange : 1 < mmSizeX;
mmSizeYRange : 1 < mmSizeY;
}.
Lemma mipMapsNonEmpty : forall (m : mipMapList),
[] <> mipMaps m.
Proof.
intros m.
destruct (mipMapListSorted m).
- discriminate.
- discriminate.
Qed.
Definition mipMapFirst (m : mipMapList) : mipMap.
Proof.
assert ([] <> mipMaps m) as Hneq by (apply (mipMapsNonEmpty)).
destruct (mipMaps m) eqn:Hm.
- contradiction.
- exact m0.
Defined.
Lemma lt_neq : forall n, 0 <> n <-> 0 < n.
Proof.
intros n.
constructor.
- intro Hneq.
induction n as [|k].
-- unfold not in Hneq.
assert (0 = 0) as Heq by reflexivity.
contradiction.
-- apply (Nat.lt_0_succ k).
- intro Hneq.
induction n as [|k].
-- inversion Hneq.
-- discriminate.
Qed.
Lemma lt_neq_0 : forall n, 0 <> n -> 0 < n.
Proof.
intros n Hneq.
rewrite <- lt_neq; trivial.
Qed.
Lemma lt_neq_1 : forall n, 0 < n -> 0 <> n.
Proof.
intros n Hneq.
rewrite lt_neq; trivial.
Qed.
Definition mipMapSize
(level : nat)
(imageSize : imageSize3D)
(levelRange : 0 < level)
: option mipMapImageSize :=
let sx := (sizeX imageSize) / 2 ^ level in
let sy := (sizeY imageSize) / 2 ^ level in
match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with
| (ReflectT _ xt, ReflectT _ yt) => Some (MipMapImageSize sx sy xt yt)
| (_, _) => None
end.
Fixpoint mipMapImageDataSizeTotalAux (m : list mipMap) : nat :=
match m with
| [] => 0
| (x :: []) => (mipMapOffset x) + (mipMapSizeCompressed x)
| (x :: xs) => mipMapImageDataSizeTotalAux xs
end.
Definition mipMapImageDataSizeTotal (m : mipMapList) : nat :=
mipMapImageDataSizeTotalAux (mipMaps m).
```
#### 8.18. Calino/StandardFormats.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.ChannelDescription.
Require Import com.io7m.calino.ChannelSemantic.
Require Import com.io7m.calino.ChannelType.
Import ListNotations.
Declare Scope Forall_scope.
Open Scope Forall_scope.
Definition p0n1 : 0 <> 1 := O_S 0.
Definition p0n4 : 0 <> 4 := O_S 3.
Definition p0n5 : 0 <> 5 := O_S 4.
Definition p0n6 : 0 <> 6 := O_S 5.
Definition p0n8 : 0 <> 8 := O_S 7.
Definition p0n16 : 0 <> 16 := O_S 15.
Definition p0n32 : 0 <> 32 := O_S 31.
Definition p0n64 : 0 <> 64 := O_S 63.
Definition A1 : channelDescription := channelDescriptionMake CSAlpha 1 p0n1.
Definition R5 : channelDescription := channelDescriptionMake CSRed 5 p0n5.
Definition G6 : channelDescription := channelDescriptionMake CSGreen 6 p0n6.
Definition B5 : channelDescription := channelDescriptionMake CSBlue 5 p0n5.
Definition G5 : channelDescription := channelDescriptionMake CSGreen 5 p0n5.
Definition R4 : channelDescription := channelDescriptionMake CSRed 4 p0n4.
Definition G4 : channelDescription := channelDescriptionMake CSGreen 4 p0n4.
Definition B4 : channelDescription := channelDescriptionMake CSBlue 4 p0n4.
Definition A4 : channelDescription := channelDescriptionMake CSAlpha 4 p0n4.
Definition R8 : channelDescription := channelDescriptionMake CSRed 8 p0n8.
Definition G8 : channelDescription := channelDescriptionMake CSGreen 8 p0n8.
Definition B8 : channelDescription := channelDescriptionMake CSBlue 8 p0n8.
Definition A8 : channelDescription := channelDescriptionMake CSAlpha 8 p0n8.
Definition R8_Div8 : channelDescriptionBitsDivisible8 R8 := eq_refl.
Definition G8_Div8 : channelDescriptionBitsDivisible8 G8 := eq_refl.
Definition B8_Div8 : channelDescriptionBitsDivisible8 B8 := eq_refl.
Definition A8_Div8 : channelDescriptionBitsDivisible8 A8 := eq_refl.
Definition R16 : channelDescription := channelDescriptionMake CSRed 16 p0n16.
Definition G16 : channelDescription := channelDescriptionMake CSGreen 16 p0n16.
Definition B16 : channelDescription := channelDescriptionMake CSBlue 16 p0n16.
Definition A16 : channelDescription := channelDescriptionMake CSAlpha 16 p0n16.
Definition R16_Div8 : channelDescriptionBitsDivisible8 R16 := eq_refl.
Definition G16_Div8 : channelDescriptionBitsDivisible8 G16 := eq_refl.
Definition B16_Div8 : channelDescriptionBitsDivisible8 B16 := eq_refl.
Definition A16_Div8 : channelDescriptionBitsDivisible8 A16 := eq_refl.
Definition R32 : channelDescription := channelDescriptionMake CSRed 32 p0n32.
Definition G32 : channelDescription := channelDescriptionMake CSGreen 32 p0n32.
Definition B32 : channelDescription := channelDescriptionMake CSBlue 32 p0n32.
Definition A32 : channelDescription := channelDescriptionMake CSAlpha 32 p0n32.
Definition R32_Div8 : channelDescriptionBitsDivisible8 R32 := eq_refl.
Definition G32_Div8 : channelDescriptionBitsDivisible8 G32 := eq_refl.
Definition B32_Div8 : channelDescriptionBitsDivisible8 B32 := eq_refl.
Definition A32_Div8 : channelDescriptionBitsDivisible8 A32 := eq_refl.
Definition R64 : channelDescription := channelDescriptionMake CSRed 64 p0n64.
Definition G64 : channelDescription := channelDescriptionMake CSGreen 64 p0n64.
Definition B64 : channelDescription := channelDescriptionMake CSBlue 64 p0n64.
Definition A64 : channelDescription := channelDescriptionMake CSAlpha 64 p0n64.
Definition R64_Div8 : channelDescriptionBitsDivisible8 R64 := eq_refl.
Definition G64_Div8 : channelDescriptionBitsDivisible8 G64 := eq_refl.
Definition B64_Div8 : channelDescriptionBitsDivisible8 B64 := eq_refl.
Definition A64_Div8 : channelDescriptionBitsDivisible8 A64 := eq_refl.
(* Packed channels *)
Definition A1_R5_G5_B5_Channels : list channelDescription := [A1; R5; G5; B5].
Definition A1_R5_G5_B5_NonEmpty := nil_cons (x := A1) (l := [R5; G5; B5]).
Definition R4_G4_B4_A4_Channels : list channelDescription := [R4; G4; B4; A4].
Definition R4_G4_B4_A4_NonEmpty := nil_cons (x := R4) (l := [G4; B4; A4]).
Definition R5_G6_B5_Channels : list channelDescription := [R5; G6; B5].
Definition R5_G6_B5_NonEmpty := nil_cons (x := R5) (l := [G6; B5]).
(* 8-bit channels *)
Definition R8_G8_B8_A8_Channels : list channelDescription := [R8; G8; B8; A8].
Definition R8_G8_B8_A8_NonEmpty := nil_cons (x := R8) (l := [G8; B8; A8]).
Definition R8_G8_B8_A8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_G8_B8_A8_Channels :=
Forall_cons R8 R8_Div8
(Forall_cons G8 G8_Div8
(Forall_cons B8 B8_Div8
(Forall_cons A8 A8_Div8
(Forall_nil _)))).
Definition R8_G8_B8_Channels : list channelDescription := [R8; G8; B8].
Definition R8_G8_B8_NonEmpty := nil_cons (x := R8) (l := [G8;B8]).
Definition R8_G8_B8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_G8_B8_Channels :=
Forall_cons R8 R8_Div8
(Forall_cons G8 G8_Div8
(Forall_cons B8 B8_Div8
(Forall_nil _))).
Definition R8_G8_Channels : list channelDescription := [R8; G8].
Definition R8_G8_NonEmpty := nil_cons (x := R8) (l := [G8]).
Definition R8_G8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_G8_Channels :=
Forall_cons R8 R8_Div8
(Forall_cons G8 G8_Div8
(Forall_nil _)).
Definition R8_Channels : list channelDescription := [R8].
Definition R8_NonEmpty := nil_cons (x := R8) (l := []).
Definition R8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_Channels :=
Forall_cons R8 R8_Div8 (Forall_nil _).
(* 16-bit channels *)
Definition R16_G16_B16_A16_Channels : list channelDescription := [R16; G16; B16; A16].
Definition R16_G16_B16_A16_NonEmpty := nil_cons (x := R16) (l := [G16; B16; A16]).
Definition R16_G16_B16_A16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_G16_B16_A16_Channels :=
Forall_cons R16 R16_Div8
(Forall_cons G16 G16_Div8
(Forall_cons B16 B16_Div8
(Forall_cons A16 A16_Div8
(Forall_nil _)))).
Definition R16_G16_B16_Channels : list channelDescription := [R16; G16; B16].
Definition R16_G16_B16_NonEmpty := nil_cons (x := R16) (l := [G16;B16]).
Definition R16_G16_B16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_G16_B16_Channels :=
Forall_cons R16 R16_Div8
(Forall_cons G16 G16_Div8
(Forall_cons B16 B16_Div8
(Forall_nil _))).
Definition R16_G16_Channels : list channelDescription := [R16; G16].
Definition R16_G16_NonEmpty := nil_cons (x := R16) (l := [G16]).
Definition R16_G16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_G16_Channels :=
Forall_cons R16 R16_Div8
(Forall_cons G16 G16_Div8
(Forall_nil _)).
Definition R16_Channels : list channelDescription := [R16].
Definition R16_NonEmpty := nil_cons (x := R16) (l := []).
Definition R16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_Channels :=
Forall_cons R16 R16_Div8 (Forall_nil _).
(* 32-bit channels *)
Definition R32_G32_B32_A32_Channels : list channelDescription := [R32; G32; B32; A32].
Definition R32_G32_B32_A32_NonEmpty := nil_cons (x := R32) (l := [G32; B32; A32]).
Definition R32_G32_B32_A32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_G32_B32_A32_Channels :=
Forall_cons R32 R32_Div8
(Forall_cons G32 G32_Div8
(Forall_cons B32 B32_Div8
(Forall_cons A32 A32_Div8
(Forall_nil _)))).
Definition R32_G32_B32_Channels : list channelDescription := [R32; G32; B32].
Definition R32_G32_B32_NonEmpty := nil_cons (x := R32) (l := [G32;B32]).
Definition R32_G32_B32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_G32_B32_Channels :=
Forall_cons R32 R32_Div8
(Forall_cons G32 G32_Div8
(Forall_cons B32 B32_Div8
(Forall_nil _))).
Definition R32_G32_Channels : list channelDescription := [R32; G32].
Definition R32_G32_NonEmpty := nil_cons (x := R32) (l := [G32]).
Definition R32_G32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_G32_Channels :=
Forall_cons R32 R32_Div8
(Forall_cons G32 G32_Div8
(Forall_nil _)).
Definition R32_Channels : list channelDescription := [R32].
Definition R32_NonEmpty := nil_cons (x := R32) (l := []).
Definition R32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_Channels :=
Forall_cons R32 R32_Div8 (Forall_nil _).
(* 64-bit channels *)
Definition R64_G64_B64_A64_Channels : list channelDescription := [R64; G64; B64; A64].
Definition R64_G64_B64_A64_NonEmpty := nil_cons (x := R64) (l := [G64; B64; A64]).
Definition R64_G64_B64_A64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_G64_B64_A64_Channels :=
Forall_cons R64 R64_Div8
(Forall_cons G64 G64_Div8
(Forall_cons B64 B64_Div8
(Forall_cons A64 A64_Div8
(Forall_nil _)))).
Definition R64_G64_B64_Channels : list channelDescription := [R64; G64; B64].
Definition R64_G64_B64_NonEmpty := nil_cons (x := R64) (l := [G64;B64]).
Definition R64_G64_B64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_G64_B64_Channels :=
Forall_cons R64 R64_Div8
(Forall_cons G64 G64_Div8
(Forall_cons B64 B64_Div8
(Forall_nil _))).
Definition R64_G64_Channels : list channelDescription := [R64; G64].
Definition R64_G64_NonEmpty := nil_cons (x := R64) (l := [G64]).
Definition R64_G64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_G64_Channels :=
Forall_cons R64 R64_Div8
(Forall_cons G64 G64_Div8
(Forall_nil _)).
Definition R64_Channels : list channelDescription := [R64].
Definition R64_NonEmpty := nil_cons (x := R64) (l := []).
Definition R64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_Channels :=
Forall_cons R64 R64_Div8 (Forall_nil _).
(* Layouts *)
Definition Layout_A1_R5_G5_B5 : channelLayoutDescription :=
ChannelLayoutDescriptionPacked (CLDPMake A1_R5_G5_B5_Channels A1_R5_G5_B5_NonEmpty CLPack16 eq_refl).
Definition Layout_R4_G4_B4_A4 : channelLayoutDescription :=
ChannelLayoutDescriptionPacked (CLDPMake R4_G4_B4_A4_Channels R4_G4_B4_A4_NonEmpty CLPack16 eq_refl).
Definition Layout_R5_G6_B5 : channelLayoutDescription :=
ChannelLayoutDescriptionPacked (CLDPMake R5_G6_B5_Channels R5_G6_B5_NonEmpty CLPack16 eq_refl).
Definition Layout_R8_G8_B8_A8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_A8_Channels R8_G8_B8_A8_NonEmpty R8_G8_B8_A8_FDiv8).
Definition Layout_R8_G8_B8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_Channels R8_G8_B8_NonEmpty R8_G8_B8_FDiv8).
Definition Layout_R8_G8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_Channels R8_G8_NonEmpty R8_G8_FDiv8).
Definition Layout_R8 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R8_Channels R8_NonEmpty R8_FDiv8).
Definition Layout_R16_G16_B16_A16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_A16_Channels R16_G16_B16_A16_NonEmpty R16_G16_B16_A16_FDiv8).
Definition Layout_R16_G16_B16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_Channels R16_G16_B16_NonEmpty R16_G16_B16_FDiv8).
Definition Layout_R16_G16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_Channels R16_G16_NonEmpty R16_G16_FDiv8).
Definition Layout_R16 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R16_Channels R16_NonEmpty R16_FDiv8).
Definition Layout_R32_G32_B32_A32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_A32_Channels R32_G32_B32_A32_NonEmpty R32_G32_B32_A32_FDiv8).
Definition Layout_R32_G32_B32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_Channels R32_G32_B32_NonEmpty R32_G32_B32_FDiv8).
Definition Layout_R32_G32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_Channels R32_G32_NonEmpty R32_G32_FDiv8).
Definition Layout_R32 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R32_Channels R32_NonEmpty R32_FDiv8).
Definition Layout_R64_G64_B64_A64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_A64_Channels R64_G64_B64_A64_NonEmpty R64_G64_B64_A64_FDiv8).
Definition Layout_R64_G64_B64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_Channels R64_G64_B64_NonEmpty R64_G64_B64_FDiv8).
Definition Layout_R64_G64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_Channels R64_G64_NonEmpty R64_G64_FDiv8).
Definition Layout_R64 : channelLayoutDescription :=
ChannelLayoutDescriptionUnpacked (CLDUMake R64_Channels R64_NonEmpty R64_FDiv8).
```
#### 8.19. Calino/StringUtility.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Open Scope string_scope.
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 "".
```
#### 8.20. Calino/SuperCompression.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.calino.Descriptor.
(** @annospec c0e7a860-3ab8-44cb-b478-b3ebf97b55aa *)
Inductive superCompressionMethod : Set :=
| SuperCompressionUncompressed
| SuperCompressionLZ4
| SuperCompressionDEFLATE
| SuperCompressionCustom : descriptor -> nat -> superCompressionMethod.
Definition superCompressionMethodDescriptor (c : superCompressionMethod) :=
match c with
| SuperCompressionUncompressed => "UNCOMPRESSED"
| SuperCompressionLZ4 => "LZ4"
| SuperCompressionDEFLATE => "DEFLATE"
| SuperCompressionCustom c _ => c
end.
Definition superCompressionIsNotCompressed (c : superCompressionMethod) : Prop :=
match c with
| SuperCompressionUncompressed => True
| _ => False
end.
Definition superCompressionSectionIdentifier (c : superCompressionMethod) : nat :=
match c with
| SuperCompressionUncompressed => 0
| SuperCompressionLZ4 => 0
| SuperCompressionDEFLATE => 0
| SuperCompressionCustom _ i => i
end.
#[export]
Instance superCompressionMethodDescribable : describable superCompressionMethod := {
descriptorOf c := superCompressionMethodDescriptor c
}.
```
#### 8.21. Calino/Texture.v
```
(*
* Copyright © 2026 Mark Raynsford 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 com.io7m.calino.CubeMipMap.
Require Import com.io7m.calino.ArrayMipMap.
Require Import com.io7m.calino.ImageInfo.
Require Import com.io7m.calino.MipMap.
(** @annospec ffd0b382-ae39-42ed-a31b-9a4adb9a6cfe *)
Inductive texture2d : Set := Texture2D {
i2dInfo : imageInfo;
i2dMipMaps : mipMapList;
i2dSize : 1 = imageSizeZ i2dInfo
}.
(** @annospec e423f742-c242-4389-92d6-198c8f589ba9 *)
Inductive textureArray : Set := TextureArray {
iaInfo : imageInfo;
iaMipMaps : arrayMipMapList;
iaSize : 1 <= imageSizeZ iaInfo
}.
(** @annospec 7029c3e3-e4b0-4b84-a596-216aecb88405 *)
Inductive textureCube : Set := TextureCube {
icubeInfo : imageInfo;
icubeMipMaps : cubeMipMapList;
icubeSize : 1 = imageSizeZ icubeInfo
}.
(** @annospec 17562a57-5189-4346-b271-d7ad4f0fdf6e *)
Inductive texture : Set :=
| TTexture2D : texture2d -> texture
| TTextureArray : textureArray -> texture
| TTextureCube : textureCube -> texture.
Definition imageInfoOf (i : texture) : imageInfo :=
match i with
| TTexture2D (Texture2D i _ _) => i
| TTextureArray (TextureArray i _ _) => i
| TTextureCube (TextureCube i _ _) => i
end.
```
#### 8.22. rentomos/src/main/rocq/Alignment.v
```
(*
* Copyright © 2025 Mark Raynsford 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 Stdlib.Arith.PeanoNat.
(** * 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.
#[local]
Lemma p0not4 : 0 <> 4.
Proof. discriminate. Qed.
#[local]
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.
```
#### 8.23. rentomos/src/main/rocq/Binary.v
```
(*
* Copyright © 2025 Mark Raynsford 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.
From Stdlib Require Import Strings.String.
From Stdlib Require Import Strings.Byte.
From Stdlib Require Import Lists.List.
From Stdlib Require Import Program.Basics.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Psatz.
Import ListNotations.
Local Open Scope string_scope.
Require Import com.io7m.entomos.Alignment.
Require Import com.io7m.entomos.Divisible.
(** 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).
(** The size in octets of a stream element. *)
Definition streamElementSize (s : streamE) : nat :=
match s with
| Vf64 _ => 8
| Vu64 _ => 8
| Vu32 _ => 4
| Vu8 _ => 1
end.
(** The size of a stream is the sum of the size of its elements. *)
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 Alignment.p0not4)
| BiUTF8 s => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 Alignment.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.
(** The size of a binary expression padded to 16 octet alignment. *)
Definition binarySizePadded16 (b : binaryExp) : nat :=
asMultipleOf16 (binarySize b).
(** Shorthand for UTF-8 strings. *)
Definition utf8 (s : string) : binaryExp :=
BiUTF8 (list_byte_of_string s).
(** Shorthand for integer types. *)
Definition u32 := BiU32.
(** Shorthand for integer types. *)
Definition u64 := BiU64.
(** Shorthand for real types. *)
Definition f64 := BiF64.
#[local]
Lemma fold_right_add_cons : forall x xs,
x + fold_right plus 0 xs = fold_right plus 0 (x :: xs).
Proof. reflexivity. Qed.
#[local]
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 Alignment.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 (Alignment.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 Alignment.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 (Alignment.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 Init.Nat.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.
#[local]
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.
#[local]
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.
#[local]
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.
(** The length of an evaluated binary expression padded to _a_ is always divisible by _a_. *)
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.
#[local]
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.
#[local]
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.
(** Evaluating a binary expression results in a series of u8 values. *)
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.
#[local]
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 Alignment.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 Alignment.p0not4) mod 4 = 0) as Hlm
by (apply (binaryEvalPaddedBytesAligned)).
assert (Forall streamEIsU8 (binaryEvalPaddedBytes a4 4 Alignment.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 Alignment.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.
#[local]
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.
#[local]
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.
```
#### 8.24. rentomos/src/main/rocq/Divisible.v
```
(*
* Copyright © 2025 Mark Raynsford 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.
From Stdlib Require Import Init.Nat.
(** 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.
```
#### 8.25. rentomos/src/main/rocq/ExampleFileFormat.v
```
(*
* Copyright © 2026 Mark Raynsford 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.Byte.
From Stdlib Require Import Lists.List.
Require Import com.io7m.entomos.Tags.
Require Import com.io7m.entomos.FileFormat.
Import ListNotations.
Example fileIdentifier : TagT :=
Tag x89 x4d x54 x50 x0d x0a x1a x0a.
Example sectionEndIdentifier : TagT :=
Tag x4d x54 x50 x5f x45 x4e x44 x21.
Example sectionManifestIdentifier : TagT :=
Tag x4d x54 x50 x5f x4d x41 x4e x49.
Example sectionFileIdentifier : TagT :=
Tag x4d x54 x50 x5f x46 x49 x4c x45.
Example sectionManifest : FileSectionDescriptionT :=
FileSectionDescription sectionManifestIdentifier FSO_MustBeFirst FSC_One.
Example sectionFile : FileSectionDescriptionT :=
FileSectionDescription sectionFileIdentifier FSO_AnyOrder FSC_ZeroToN.
Example fileDescriptionExample : FileDescriptionT :=
FileDescription
fileIdentifier
1
0
[sectionManifest; sectionFile]
sectionEndIdentifier
UnknownSectionsPermitted
.
Lemma fileSectionAtMostOneFirstExample : fileSectionAtMostOneFirst (fileSections fileDescriptionExample).
Proof.
unfold fileSectionAtMostOneFirst.
simpl; auto.
Qed.
Lemma fileSectionAtMostOneLastExample : fileSectionAtMostOneLast (fileSections fileDescriptionExample).
Proof.
unfold fileSectionAtMostOneLast.
simpl; auto.
Qed.
Lemma fileSectionTagsUniqueExample : fileSectionTagsUnique (fileSections fileDescriptionExample).
Proof.
unfold fileSectionTagsUnique.
simpl; auto.
constructor.
- unfold not.
intro H.
inversion H.
contradict H0.
discriminate.
inversion H0.
- constructor.
unfold not.
intro H.
inversion H.
constructor.
Qed.
Lemma fileSectionFileNotSectionExample : fileSectionFileNotSection fileDescriptionExample.
Proof.
unfold fileSectionFileNotSection.
simpl.
unfold not.
intro H.
destruct H.
- contradict H.
discriminate.
- destruct H.
contradict H.
discriminate.
auto.
Qed.
Lemma endSectionFileNotSectionExample : endSectionFileNotSection fileDescriptionExample.
Proof.
unfold endSectionFileNotSection.
simpl.
unfold not.
intro H.
destruct H.
- contradict H.
discriminate.
- destruct H.
contradict H.
discriminate.
auto.
Qed.
Theorem fileDescriptionInvariantsExample : fileDescriptionInvariants fileDescriptionExample.
Proof.
constructor.
apply fileSectionAtMostOneFirstExample.
constructor.
apply fileSectionAtMostOneLastExample.
constructor.
apply fileSectionTagsUniqueExample.
constructor.
apply fileSectionFileNotSectionExample.
apply endSectionFileNotSectionExample.
Qed.
```
#### 8.26. rentomos/src/main/rocq/FileFormat.v
```
(*
* Copyright © 2026 Mark Raynsford 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.
Require Import com.io7m.entomos.Tags.
Import ListNotations.
(** The ordering constraints on a file section. *)
Inductive FileSectionOrderingT :=
(** The section must be the first in the file. *)
FSO_MustBeFirst
| (** The section must be the last in the file. *)
FSO_MustBeLast
| (** The section can appear anywhere in the file. *)
FSO_AnyOrder
.
(** The cardinality of a file section. *)
Inductive FileSectionCardinalityT :=
(** The section must appear exactly once. *)
FSC_One
| (** The section can appear at most once. *)
FSC_ZeroToOne
| (** The section can appear any number of times, including not at all. *)
FSC_ZeroToN
| (** The section must appear at least once. *)
FSC_OneToN
.
(** The constraints on unknown sections. *)
Inductive FileSectionsUnknownT :=
| (** Unknown sections are permitted. *)
UnknownSectionsPermitted
| (** Unknown sections are not permitted. *)
UnknownSectionsNotPermitted
.
(** A description of a file section. *)
Inductive FileSectionDescriptionT := FileSectionDescription {
(** The file section tag. *)
fileSectionTag : TagT;
(** The file section ordering constraint. *)
fileSectionOrdering : FileSectionOrderingT;
(** The file section cardinality constraint. *)
fileSectionCardinality : FileSectionCardinalityT
}.
(** The description of a file format version. *)
Inductive FileDescriptionT := FileDescription {
(** The file tag. *)
fileTag : TagT;
(** The major file format version. *)
fileVersionMajor : nat;
(** The minor file format version. *)
fileVersionMinor : nat;
(** The file sections. *)
fileSections : list FileSectionDescriptionT;
(** The file end tag. *)
fileEndTag : TagT;
(** The constraints on unknown file sections. *)
fileSectionsUnknown : FileSectionsUnknownT
}.
(** The number of sections with _FSO_MustBeFirst_. *)
Fixpoint fileSectionOrderingCountFirst
(xs : list FileSectionDescriptionT)
(n : nat)
: nat :=
match xs with
| nil => 0
| cons y ys =>
match (fileSectionOrdering y) with
| FSO_MustBeFirst => fileSectionOrderingCountFirst ys (S n)
| _ => fileSectionOrderingCountFirst ys n
end
end.
(** The number of sections with _FSO_MustBeLast_. *)
Fixpoint fileSectionOrderingCountLast
(xs : list FileSectionDescriptionT)
(n : nat)
: nat :=
match xs with
| nil => 0
| cons y ys =>
match (fileSectionOrdering y) with
| FSO_MustBeLast => fileSectionOrderingCountLast ys (S n)
| _ => fileSectionOrderingCountLast ys n
end
end.
(** At most one section can be _FSO_MustBeFirst_. *)
Definition fileSectionAtMostOneFirst (xs : list FileSectionDescriptionT) : Prop :=
fileSectionOrderingCountFirst xs 0 <= 1.
(** At most one section can be _FSO_MustBeLast_. *)
Definition fileSectionAtMostOneLast (xs : list FileSectionDescriptionT) : Prop :=
fileSectionOrderingCountLast xs 0 <= 1.
(** The file sections must have unique tags. *)
Definition fileSectionTagsUnique (xs : list FileSectionDescriptionT) : Prop :=
NoDup (map (fun s => fileSectionTag s) xs).
(** The file sections cannot contain the file tag. *)
Definition fileSectionFileNotSection (f : FileDescriptionT) : Prop :=
~In (fileTag f) (map (fun s => fileSectionTag s) (fileSections f)).
(** The file sections cannot contain the end tag. *)
Definition endSectionFileNotSection (f : FileDescriptionT) : Prop :=
~In (fileEndTag f) (map (fun s => fileSectionTag s) (fileSections f)).
(** The file format description invariants. *)
Definition fileDescriptionInvariants (f : FileDescriptionT) : Prop :=
fileSectionAtMostOneFirst (fileSections f)
/\ fileSectionAtMostOneLast (fileSections f)
/\ fileSectionTagsUnique (fileSections f)
/\ fileSectionFileNotSection f
/\ endSectionFileNotSection f.
```
#### 8.27. rentomos/src/main/rocq/Tags.v
```
(*
* Copyright © 2026 Mark Raynsford 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 Init.Nat.
From Stdlib Require Import Strings.Byte.
(** A 64-bit section identifier. *)
Inductive TagT : Set := Tag {
tag_byte0 : byte;
tag_byte1 : byte;
tag_byte2 : byte;
tag_byte3 : byte;
tag_byte4 : byte;
tag_byte5 : byte;
tag_byte6 : byte;
tag_byte7 : byte
}.
(** The example PNG file format identifier. *)
Example tagPNG :=
Tag x89 x50 x4e x47 x0d x0a x1a x0a.
```
#### 8.28. roctetorder/src/main/rocq/OctetOrder.v
```
(*
* Copyright © 2025 Mark Raynsford 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 Stdlib.PArith.PArith.
Require Import Stdlib.Init.Nat.
Require Import Stdlib.Arith.PeanoNat.
Require Import Stdlib.Lists.List.
Import ListNotations.
(** The property of _x_ being divisible by 8. *)
Definition divisible8 (x : nat) : Prop :=
modulo x 8 = 0.
(** An octet is either in big or little endian order. *)
Inductive octetOrder : Set :=
| OctetOrderBig
| OctetOrderLittle.
(** A single 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. *)
Inductive octet : Set :=
| OctExact : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet
| OctRemain : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet.
#[local]
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).
#[local]
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.
#[local]
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.
#[local]
Lemma p8notZ : 8 <> 0.
Proof. discriminate. Qed.
#[local]
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.
#[local]
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.
#[local]
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.
#[local]
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.
#[local]
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.
#[local]
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.
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 :: []).
(** 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. *)
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 [].
(** 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. *)
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. *)
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.
(** A sequence of bits s such that divisible8 (length s) will produce a sequence
consisting of entirely exact octets. *)
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.
(** A sequence of bits s such that ¬ divisible8 (length s) will produce a remainder octet. *)
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.
(** A sequence of bits s such that ¬ divisible8 (length s) will produce a remainder octet. *)
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.
```
## Footnotes
1. It would be more accurate to say that the **calino** specification does not depend on any other specifications **that are at the same level of abstraction**. For example, the **calino** specification makes references to [Unicode](https://www.unicode.org), [IEEE 754](https://en.wikipedia.org/wiki/IEEE_754), and so on. It does not, however, require understanding any other existing texture formats, or depend on any definitions given in the specifications for any rendering APIs.